Commit 235966b1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Rework infrastructure a bit

parent 646df7a0
This diff is collapsed.
......@@ -13,7 +13,8 @@ open BasicProvers Defn HolKernel Parse Tactic monadsyntax
listTheory llistTheory markerLib
optionTheory pairLib pairTheory pred_setTheory
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory;
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory simpLib;
open ExpressionsTheory CommandsTheory;
fun elim_conj thm =
let val (hypl, concl) = dest_thm thm in
......@@ -29,18 +30,14 @@ fun elim_conj thm =
fun elim_exist1 thm =
let val (hypl, concl) = dest_thm thm in
if is_exists concl
then
CHOOSE_THEN elim_exist thm
else
elim_conj thm
then CHOOSE_THEN elim_exist thm
else elim_conj thm
end
and elim_exist thm =
let val (hypl, concl) = dest_thm thm in
if is_exists concl
then
CHOOSE_THEN elim_exist1 thm
else
elim_conj thm
then CHOOSE_THEN elim_exist1 thm
else elim_conj thm
end;
fun inversion pattern cases_thm =
......@@ -81,13 +78,9 @@ fun rw_thm_asm pat_asm thm =
(* Destruct like tactic, by Michael Norrish, see HOL-info **)
(* Given theorem
P x y z ==> ?w. Q w
introduce P x y z as a subgoal and Q w for some w as hypothesis *)
fun destruct th =
let
val hyp_to_prove = lhand (concl th)
......@@ -112,92 +105,6 @@ val flover_eval_tac :tactic=
\\ EVAL_TAC
end;
(* Flover Compute Tactic as in Coq dev to simplify goals involving computations *)
fun iter n s f =
if n = 0 then s
else iter (n - 1) (f s) f;
fun getArgTypeList t num lst =
let val (name, list) = dest_type t in
case name of
"fun" =>
let
val (hdty, tylist) = (hd list, tl list) in
getArgTypeList (hd tylist) (num + 1) (hdty :: lst)
end
| _ => (num, rev lst)
end
exception ERR of string;
fun getPatTerm t =
let
val decl_list = decls (term_to_string t);
val argTypes_list = map (fn t => getArgTypeList (#Ty (dest_thy_const t)) 0 []) decl_list in
if length decl_list = 1
then
let
val (cnt, tyList) = hd argTypes_list
in
iter cnt (hd decl_list, tyList)
(fn (t,tyList) =>
let
val var = mk_var ("_",hd tyList) in
(* val _ = print_term var; *)
(* val _ = print_term t in *)
(mk_comb (t, var), tl tyList)
end)
end
else raise ERR "Too many constants"
end;
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];
(* open TextIO; *)
(* val t = TextIO.openIn("/home/hbecker/Downloads/test.txt"); *)
(* inputLine(t); *)
(* closeIn(t); *)
(* val t2 = openIn("./test.txt"); *)
(* inputLine(t2); *)
(* output(t2, "ABC\n"); *)
(* closeOut(t2); *)
fun add_unevaluated_function (t:term) :unit =
let
val add_t = "val _ = FloverTactics.eval_funs :=``" ^ term_to_string t ^ "`` :: (!FloverTactics.eval_funs);"
val _ = adjoin_to_theory
{ sig_ps = NONE,
struct_ps =
SOME (fn _ => PP.add_string add_t)};
in
eval_funs := t :: (!eval_funs)
end;
fun Flover_compute t =
let
val eval_thm = fst (snd (hd (DB.find ((term_to_string t)^"_def"))));
val (pat,_) = getPatTerm t in
TRY (
Tactical.PAT_X_ASSUM
pat
(fn thm =>
let
val rwthm = ONCE_REWRITE_RULE [eval_thm] thm;
val compute_thm = computeLib.RESTR_EVAL_RULE (!eval_funs) rwthm in
assume_tac compute_thm end)
\\ fs[]
\\ TRY (
REPEAT (
((qpat_assum `option_CASE _ _ _`
(fn thm =>
let
val (t,t2,_) = optionSyntax.dest_option_case (concl thm) in
Cases_on `^t2` \\ fs[] end))
ORELSE
(split_pair_case_tac)) \\ fs[])))
end;
fun iter_exists_tac ind n =
fn tm =>
if ind < n
......@@ -219,15 +126,22 @@ val try_all:term -> tactic =
val find_exists_tac =
first_assum (try_all o concl);
(* val Flover_compute:tactic = *)
(* fn (g:goal) => *)
(* let *)
(* val terms_to_eval = !eval_funs in *)
(* if (length terms_to_eval = 0) *)
(* then let val _ = print "Nothing to evaluate" in ALL_TAC g end *)
(* else *)
(* Flover_compute_steps terms_to_eval g *)
(* end; *)
val bool_simps = Q.prove (
( P. (P F) = F)
( P. (F P) = P)
( P Q. (if P then Q else F) = (P Q)), fs[]);
val cond_simp = Q.prove (
(if P then Q else R) = (P /\ Q \/ ~P /\ R),
TOP_CASE_TAC);
val flover_ss =
(mk_simpset ([DatatypeSimps.case_cong_ss [:real expr, :real cmd]]
@ ssfrags_of bool_ss))
&& [option_case_eq |> GEN v:'b |> Q.ISPEC T |> SIMP_RULE bool_ss [],
pair_case_eq |> GEN v:'a |> Q.ISPEC T |> SIMP_RULE bool_ss [],
expr_case_eq |> GEN v:'a |> Q.ISPEC T |> SIMP_RULE bool_ss [],
cmd_case_eq |> GEN v:'a |> Q.ISPEC T |> SIMP_RULE bool_ss [],
bool_simps, cond_simp, PULL_EXISTS];
end
INCLUDES = Infra
INCLUDES = Infra semantics
OPTIONS = QUIT_ON_FAILURE
open RealArith;
open realTheory realLib;
open FloverTactics;
open preambleFloVer;
(*
val _ = ParseExtras.temp_tight_equality() *)
......@@ -99,7 +98,7 @@ Theorem REAL_LE_ABS_TRANS:
a <= b
Proof
rpt strip_tac \\ irule REAL_LE_TRANS
\\ find_exists_tac \\ fs[ABS_LE]
\\ fsrw_tac [SATISFY_ss] [ABS_LE]
QED
Theorem REAL_POW_1OVER_POS[simp]:
......
......@@ -96,26 +96,18 @@ Definition addInterval_def:
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2
End
add_unevaluated_function ``addInterval``;
Definition subtractInterval_def:
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)
End
add_unevaluated_function ``subtractInterval``;
Definition multInterval_def:
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2
End
add_unevaluated_function ``multInterval``;
Definition divideInterval_def:
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)
End
add_unevaluated_function ``divideInterval``;
Definition minAbsFun_def:
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))
End
......@@ -490,8 +482,8 @@ val distance_gives_iv = store_thm ("distance_gives_iv",
val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
``!(a b:real).
(0 < a) /\
(a <= b) ==>
(minAbsFun (a,b) = a)``,
(a <= b) ==>
(minAbsFun (a,b) = a)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
......@@ -501,8 +493,8 @@ val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
``!(a b:real).
(b < 0) /\
(a <= b) ==>
(minAbsFun (a,b) = - b)``,
(a <= b) ==>
(minAbsFun (a,b) = - b)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
......
......@@ -22,7 +22,7 @@ val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
val validIntervalbounds_def = Define `
Definition validIntervalbounds_def:
validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
case (FloverMapTree_find f absenv) of
| SOME (intv, _) =>
......@@ -93,11 +93,13 @@ val validIntervalbounds_def = Define `
isSupersetInterval new_iv intv
| _, _, _ => F
else F))
| _ => F`;
| _ => F
End
add_unevaluated_function ``validIntervalbounds``;
Theorem validIntervalbounds_eq =
SIMP_CONV flover_ss [Once validIntervalbounds_def] (Parse.Term validIntervalbounds e A P v)
val validIntervalboundsCmd_def = Define `
Definition validIntervalboundsCmd_def:
validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
case f of
| Let m x e g =>
......@@ -108,25 +110,23 @@ val validIntervalboundsCmd_def = Define `
else F
|_,_ => F)
| Ret e =>
(validIntervalbounds e absenv P validVars)`;
(validIntervalbounds e absenv P validVars)
End
add_unevaluated_function ``validIntervalboundsCmd``;
Theorem validIntervalboundsCmd_eq =
SIMP_CONV flover_ss [Once validIntervalboundsCmd_def] (Parse.Term validIntervalboundsCmd f A P v)
val cond_simpl = store_thm (
"cond_simpl[simp]",
``!a b. (if a then T else b) <=> (a \/ (~ a /\ b))``,
rpt strip_tac \\ metis_tac[]);
Theorem cond_simpl:
a b. (if a then T else b) <=> (a \/ (~ a /\ b))
Proof
rpt strip_tac \\ metis_tac[]
QED
val real_prove =
rpt (qpat_x_assum `!x. _` kall_tac)
\\ rpt (qpat_x_assum `_ ==> ! x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
val _ = add_unevaluated_function addInterval
val _ = add_unevaluated_function subtractInterval
val _ = add_unevaluated_function multInterval
val _ = add_unevaluated_function divideInterval
Theorem validIntervalbounds_sound:
!(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
(dVars:num_set) E Gamma.
......@@ -138,9 +138,12 @@ Theorem validIntervalbounds_sound:
validTypes f Gamma ==>
validRanges f A E (toRTMap (toRExpMap Gamma))
Proof
Induct_on `f`
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac \\ rveq
\\ Flover_compute ``validIntervalbounds`` \\ rveq
Induct_on `f` \\ rpt strip_tac
\\ qpat_x_assum domain (usedVars _) DIFF _ SUBSET _
(assume_tac o (SIMP_RULE flover_ss [Once usedVars_def]))
\\ qpat_x_assum validIntervalbounds _ _ _ _
(assume_tac o (ONCE_REWRITE_RULE [validIntervalbounds_eq]))
\\ fs[]
(* Defined variable case *)
>- (rw_thm_asm `dVars_range_valid _ _ _` dVars_range_valid_def
\\ specialize `!v. v IN domain dVars ==> _` `n`
......@@ -165,7 +168,7 @@ Proof
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[])
(* Const case *)
>- (simp[validRanges_def]
\\ qexists_tac `v` \\ fs[toREval_def]
\\ qexists_tac `v` \\ fs[toREval_def, isSupersetInterval_def]
\\ irule Const_dist' \\ fs[perturb_def, mTypeToR_def])
(* Unary operator case *)
>- (rw_thm_asm `validTypes _ _` validTypes_def
......@@ -349,10 +352,9 @@ Theorem validIntervalboundsCmd_sound:
validTypesCmd f Gamma ==>
validRangesCmd f A E (toRTMap (toRExpMap Gamma))
Proof
Induct_on `f`
Induct_on `f` \\ simp[Once validIntervalboundsCmd_eq]
\\ once_rewrite_tac [toREvalCmd_def, getRetExp_def, validTypesCmd_def]
\\ rpt strip_tac
\\ Flover_compute ``validIntervalboundsCmd``
>- (
inversion `ssa _ _ _` ssa_cases \\ rveq
\\ drule validIntervalbounds_sound
......@@ -424,9 +426,8 @@ Theorem validIntervalbounds_validates_iv:
FloverMapTree_find f A = SOME (iv, err) /\
valid iv
Proof
Induct_on `f`
Induct_on `f` \\ simp[Once validIntervalbounds_eq]
\\ rpt strip_tac
\\ Flover_compute ``validIntervalbounds``
>- (first_x_assum (qspecl_then [`n`] destruct)
\\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
\\ rveq \\ fs[])
......@@ -434,7 +435,7 @@ Proof
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ conj_tac \\ fs[IVlo_def, IVhi_def]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
>- (fs[valid_def, IVlo_def, IVhi_def]
>- (fs[isSupersetInterval_def, valid_def, IVlo_def, IVhi_def]
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
>- (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct)
\\ fs[]
......@@ -512,7 +513,8 @@ Proof
\\ rveq
\\ `FST iv = FST intv` by (metis_tac[REAL_LE_ANTISYM])
\\ `SND iv = SND intv` by (metis_tac[REAL_LE_ANTISYM])
\\ fs[valid_def, IVlo_def, IVhi_def]));
\\ fs[valid_def, IVlo_def, IVhi_def])
QED
val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
``!(f1 f2:real expr) A (P:precond) (dVars:num_set).
......@@ -520,7 +522,7 @@ val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzer
?iv err.
FloverMapTree_find f2 A = SOME (iv,err) /\
noDivzero (SND iv) (FST iv)``,
rpt strip_tac \\ Flover_compute ``validIntervalbounds``
rpt strip_tac \\ fs[Once validIntervalbounds_eq]
\\ fs[noDivzero_def, IVhi_def, IVlo_def]);
val validRanges_validates_iv = store_thm (
......
......@@ -204,8 +204,6 @@ Definition getValidMap_def:
od
End
add_unevaluated_function ``getValidMap``;
val tMap_def = FloverMapTree_correct;
val toRExpMap_char = store_thm (
......
......@@ -33,6 +33,7 @@ val toRTMap_def = Define `
|_ => NONE) /\
toRTMap tMap e = SOME REAL`;
val no_cycle_unop = store_thm (
"no_cycle_unop",
``!e u. e <> Unop u e``,
......
......@@ -2,7 +2,7 @@
Formalization of the base expression language for the flover framework
**)
open realTheory realLib sptreeTheory;
open AbbrevsTheory MachineTypeTheory FloverTactics ExpressionsTheory;
open AbbrevsTheory MachineTypeTheory ExpressionsTheory;
open ExpressionAbbrevsTheory;
open preambleFloVer;
......@@ -206,8 +206,7 @@ Theorem toRTMap_eval_REAL:
e v E Gamma m.
eval_expr E (toRTMap Gamma) (toREval e) v m ==> m = REAL
Proof
Induct_on `e` \\ rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
Induct_on `e` \\ rpt strip_tac \\ fs[toREval_def, Once eval_expr_cases]
\\ fs[toRTMap_def, option_case_eq]
\\ res_tac \\ fs[]
QED
......
......@@ -2,7 +2,7 @@
Formalization of the base expression language for the flover framework
**)
open realTheory realLib sptreeTheory
open AbbrevsTheory MachineTypeTheory FloverTactics
open AbbrevsTheory MachineTypeTheory
open preambleFloVer;
val _ = new_theory "Expressions";
......
open MachineTypeTheory ExpressionsTheory FloverTactics
open MachineTypeTheory ExpressionsTheory;
open preambleFloVer;
val _ = new_theory "FloverMap";
......
INCLUDES = ../Infra
OPTIONS = QUIT_ON_FAILURE
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment