Commit 024abf5d authored by Heiko Becker's avatar Heiko Becker

WIP state of IV validator

parent b1a6c8eb
......@@ -109,6 +109,6 @@ val DaisyMapTree_empty_def = Define `
DaisyMapTree_empty = LeafN `;
val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``);
val _ = type_abbrev ("DaisyMap", ``:(real exp # ((real # real) # real)) binTree``);
val _ = type_abbrev ("analysisResult", ``:(real exp # ((real # real) # real)) binTree``);
val _ = export_theory();
......@@ -11,6 +11,7 @@ val _ = new_theory "ExpressionAbbrevs"
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``);
(* val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``); *)
val _ = export_theory()
......@@ -112,61 +112,80 @@ fun daisy_eval_tac t :tactic=
\\ fs[sptreeTheory.lookup_def]
end;
fun case_destruct_tac thm =
let
val conclusion = concl thm;
val caseTerm = find_term TypeBase.is_case conclusion;
val (_, caseOn, _) = TypeBase.dest_case caseTerm
val _ = print ("Case analysis on ")
val _ = print_term caseOn in
BasicProvers.Cases_on `^caseOn`
end;
fun case_compute_tac pat =
qpat_x_assum pat
(fn thm => REPEAT (case_destruct_tac thm \\ fs[]));
fun type_manip f cst =
let
val holObj = dest_thy_const cst;
val t = #Ty holObj;
val (_, typeParamsList) = dest_type t in
f typeParamsList
end
(* Daisy 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 id x = x
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
fun foo t =
fun getPatTerm t =
let
val decl_list = decls (term_to_string t);
val num_list = map (type_manip length) decl_list;
val type_list = map (type_manip id) decl_list in
if length num_list = 1
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 = hd num_list;
val ty = hd(hd type_list) in
iter cnt (t, ty)
(fn (t,ty) =>
let val (name, tyList) = dest_type ty;
val var = mk_var ("_",hd tyList);
val _ = print_term var;
val _ = print_term t in
(mk_comb (t, var), hd(tl tyList))
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;
(* TODO PATTERN GENERATION!*)
foo ``typeCheck``
dest_comb (mk_comb (``typeCheck``,``_:real exp``))
dest_type (#Ty (dest_thy_const ``typeCheck``));
(* dest_term ``typeCheck _`` *)
(* This variable is supposed to hold all defined functions *)
val eval_funs:term list ref = ref [];
fun add_unevaluated_function (t:term) :unit =
eval_funs := t :: (!eval_funs);
fun Daisy_compute t =
let
val eval_thm = DB.theorem ((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)
\\ split_pair_case_tac \\ fs[])))
end;
(* val Daisy_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 *)
(* Daisy_compute_steps terms_to_eval g *)
(* end; *)
end
......@@ -8,8 +8,8 @@
open preamble
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
open sptreeLib sptreeTheory
ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
sptreeLib sptreeTheory DaisyMapTheory
val _ = new_theory "IntervalValidation";
......@@ -20,15 +20,17 @@ val _ = temp_overload_on("min",``real$min``);
val validIntervalbounds_def = Define `
validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
let (intv, _) = absenv f in
case f of
case (DaisyMapTree_find f absenv) of
| SOME (intv, _) =>
(case f of
| Var v =>
if (lookup v validVars = SOME ())
then T
else (isSupersetInterval (P v) intv /\ IVlo (P v) <= IVhi (P v))
| Const m n => isSupersetInterval (n,n) intv
| Unop op f1 =>
let (iv, _) = absenv f1 in
(case (DaisyMapTree_find f1 absenv) of
| SOME (iv, _) =>
(if validIntervalbounds f1 absenv P validVars
then
case op of
......@@ -42,219 +44,156 @@ val validIntervalbounds_def = Define `
isSupersetInterval new_iv intv
else
F
else F)
else F)
| _ => F)
| Downcast m f1 =>
(let (iv1, _) = absenv f1 in
if (validIntervalbounds f1 absenv P validVars) then
(case (DaisyMapTree_find f1 absenv) of
| SOME (iv1, _) =>
(if (validIntervalbounds f1 absenv P validVars) then
((isSupersetInterval intv iv1) /\ (isSupersetInterval iv1 intv))
else F)
| _ => F)
| Binop op f1 f2 =>
(if (validIntervalbounds f1 absenv P validVars /\ validIntervalbounds f2 absenv P validVars)
(if (validIntervalbounds f1 absenv P validVars /\
validIntervalbounds f2 absenv P validVars)
then
let (iv1, _ ) = absenv f1 in
let (iv2, _) = absenv f2 in
case op of
| Plus =>
let new_iv = addInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Sub =>
let new_iv = subtractInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Mult =>
let new_iv = multInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Div =>
if (IVhi iv2 < 0 \/ 0 < IVlo iv2)
then
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv
else F
else F)`;
(case (DaisyMapTree_find f1 absenv, DaisyMapTree_find f2 absenv) of
| (SOME (iv1, _), SOME (iv2, _)) =>
(case op of
| Plus =>
let new_iv = addInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Sub =>
let new_iv = subtractInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Mult =>
let new_iv = multInterval iv1 iv2 in
isSupersetInterval new_iv intv
| Div =>
if (IVhi iv2 < 0 \/ 0 < IVlo iv2)
then
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv
else F)
| _ => F)
else F))
| _ => F`;
add_unevaluated_function ``validIntervalbounds``;
val validIntervalboundsCmd_def = Define `
validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
case f of
| Let m x e g =>
if (validIntervalbounds e absenv P validVars /\
(FST (absenv e) = FST (absenv (Var x))))
then validIntervalboundsCmd g absenv P (insert x () validVars)
else F
(case (DaisyMapTree_find e absenv, DaisyMapTree_find (Var x) absenv) of
| SOME (iv_e,_), SOME (iv_x, _) =>
if (validIntervalbounds e absenv P validVars /\ (iv_e = iv_x))
then validIntervalboundsCmd g absenv P (insert x () validVars)
else F
|_,_ => F)
| Ret e =>
(validIntervalbounds e absenv P validVars)`;
val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecond_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) (V:num_set).
validIntervalbounds f absenv P V ==>
(!(v:num). v IN ((domain (usedVars f)) DIFF (domain V)) ==>
isSupersetInterval (P v) (FST (absenv (Var v))))``,
Induct_on `f` \\ once_rewrite_tac [usedVars_def] \\ rpt strip_tac \\ fs[]
>- (rule_assum_tac (ONCE_REWRITE_RULE [validIntervalbounds_def])
\\ fs [domain_lookup, usedVars_def, lookup_insert]
\\ `v = n` by (Cases_on `v = n` \\ fs[lookup_def])
\\ rveq
\\ Cases_on `absenv (Var n)`
\\ Cases_on `lookup n V`
\\ fs[])
>- (rpt (
first_x_assum
(fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
\\ `validIntervalbounds f absenv P V`
by ( Cases_on `absenv (Unop u f)` \\ Cases_on `absenv f` \\ fs [Once validIntervalbounds_def])
\\ fs [])
>- (rpt (
first_x_assum
(fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
\\ rename1 `Binop b f1 f2`
\\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V`
by (Cases_on `absenv (Binop b f1 f2)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ fs [Once validIntervalbounds_def])
\\ fs [domain_union])
>- (rpt (
first_x_assum
(fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
\\ `validIntervalbounds f absenv P V`
by (Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs [Once validIntervalbounds_def])
\\ fs []));
add_unevaluated_function ``validIntervalboundsCmd``;
val dVars_range_valid_def = Define `
dVars_range_valid (dVars:num_set) (E:num -> real option) (A:analysisResult) =
!(v:num). v IN domain dVars ==>
?vR iv err.
E v = SOME vR /\
(DaisyMapTree_find ((Var v):real exp) A = SOME (iv, err)) /\
(FST iv) <= vR /\ vR <= (SND iv)`;
val fVars_P_sound_def = Define `
fVars_P_sound (fVars:num_set) (E:env) (P:precond) =
!(v:num).
v IN domain fVars ==>
?vR. E v = SOME vR /\
FST (P v) <= vR /\ vR <= SND (P v)`;
val vars_typed_def = Define `
vars_typed (S:num set) (Gamma:num -> mType option) =
!v. v IN S ==>
?m. Gamma v = SOME m`;
val cond_simpl = store_thm (
"cond_simpl[simp]",
``!a b. (if a then T else b) <=> (a \/ (~ a /\ b))``,
rpt strip_tac \\ metis_tac[]);
val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) (fVars:num_set) (dVars:num_set) E Gamma.
validIntervalbounds f absenv P dVars /\ (* The checker succeeded *)
``!(f:real exp) (A:analysisResult) (P:precond) (fVars:num_set) (dVars:num_set) E Gamma.
validIntervalbounds f A P dVars /\ (* The checker succeeded *)
(* All defined vars have already been analyzed *)
(!v. v IN (domain dVars) ==>
(?vR. (E v = SOME vR) /\
(FST (FST (absenv (Var v))) <= vR /\ vR <= SND (FST (absenv (Var v)))))) /\
(* The variables in term f without the the defined variable set are a subset of the free variables *)
dVars_range_valid dVars E A /\
(((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
(* All free variables are defined in the execution environment and
the values respect the precondition *)
(!v. v IN (domain fVars) ==>
(?vR. (E v = SOME vR) /\
(FST (P v) <= vR /\ vR <= SND (P v)))) /\
(* All variables that are either free or defined have a type *)
(!v. v IN ((domain fVars) UNION (domain dVars)) ==>
?m. Gamma v = SOME m) ==>
? vR.
fVars_P_sound fVars E P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma ==>
? iv err vR.
DaisyMapTree_find f A = SOME(iv, err) /\
eval_exp E (toRMap Gamma) (toREval f) vR M0 /\
(FST (FST (absenv f))) <= vR /\ vR <= (SND (FST (absenv f)))``,
Induct_on `f` \\ once_rewrite_tac [toREval_def,eval_exp_cases] \\ rpt strip_tac
(* Variable case *)
>- (rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Var n)` \\ Cases_on `lookup n dVars` \\ fs[]
>- (specialize `!v. v IN domain fVars ==> _` `n`
\\ fs [usedVars_def]
\\ `~ (n IN (domain dVars))` by (fs[domain_lookup])
\\ `n IN domain fVars` by fs[]
\\ fs [isSupersetInterval_def, IVlo_def, IVhi_def]
\\ `?m. Gamma n = SOME m`
by (first_x_assum match_mp_tac \\fs [])
\\ `eval_exp E (toRMap Gamma) (toREval (Var n)) vR M0`
by (fs[toREval_def] \\ match_mp_tac Var_load \\ fs[toRMap_def])
\\ qexists_tac `vR` \\ fs [toREval_def]
\\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [] \\ rveq
\\ conj_tac
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ fs [] \\ rveq \\ simp[])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `SND (P n)`
\\ fs [] \\ rveq \\ simp []))
>- (specialize `!v. v IN domain dVars ==> _` `n`
\\ `n IN domain dVars` by (fs [domain_lookup])
\\ `?m. Gamma n = SOME m` by (first_x_assum match_mp_tac \\ fs[])
\\ fs[]
\\ `eval_exp E (toRMap Gamma) (toREval (Var n)) vR M0`
by (fs [toREval_def] \\ match_mp_tac Var_load \\ fs[toRMap_def])
\\ qexists_tac `vR` \\ fs[]
\\ qpat_x_assum `absenv (Var n) = _` (fn thm => fs[thm, toREval_def])))
(FST iv) <= vR /\ vR <= (SND iv)``,
Induct_on `f`
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac
\\ Daisy_compute ``validIntervalbounds``
(* Defined variable case *)
>- (rw_thm_asm `dVars_range_valid _ _ _` dVars_range_valid_def
\\ specialize `!v. v IN domain dVars ==> _` `n`
\\ first_x_assum destruct
>- (fs [domain_lookup])
\\ qexists_tac `vR` \\ fs[] \\ rveq \\ fs[]
\\ irule Var_load \\ TRY (fs[])
\\ rw_thm_asm `vars_typed _ _` vars_typed_def
\\ first_x_assum (qspec_then `n` destruct)
\\ fs[toRMap_def, domain_lookup])
(* Free variable case *)
>- (rw_thm_asm `fVars_P_sound _ _ _` fVars_P_sound_def
\\ specialize `!v. v IN domain fVars ==> _` `n`
\\ `lookup n dVars = NONE` by (Cases_on `lookup n dVars` \\ fs [])
\\ first_x_assum destruct
>- (fs[usedVars_def, lookup_NONE_domain])
\\ qexists_tac `vR`
\\ fs [isSupersetInterval_def, IVlo_def, IVhi_def]
\\ rpt conj_tac
>- (irule Var_load \\ TRY (fs[])
\\ rw_thm_asm `vars_typed _ _` vars_typed_def
\\ first_x_assum (qspec_then `n` destruct)
\\ fs[toRMap_def, domain_lookup])
\\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[])
(* Const case *)
>- (Cases_on `absenv (Const m v)`
\\ fs []
\\ `eval_exp E (toRMap Gamma) (toREval (Const m v)) v M0`
by (fs [toREval_def] \\ match_mp_tac Const_dist'
\\ fs[mTypeToQ_def]
\\ fs[perturb_def])
\\ qexists_tac `v`
\\ fs [mTypeToQ_def]
\\ fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def, toREval_def])
>- (qexists_tac `v` \\ fs[]
\\ irule Const_dist' \\ fs[]
\\ qexists_tac `0` \\ fs[perturb_def]
\\ irule mTypeToQ_pos)
(* Unary operator case *)
>- (simp[evalUnop_def]
\\ fs []
\\ `?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\ FST (FST (absenv f)) <= v /\ v <= SND (FST (absenv f))`
by (first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `fVars`, `dVars`]
\\ fs []
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Unop u f)` \\ Cases_on `absenv f` \\ fs[Once usedVars_def]
\\ rpt strip_tac \\ first_x_assum match_mp_tac \\ fs[])
>- (first_x_assum (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct)
\\ fs[]
\\ rveq
\\ Cases_on `u`
>- (rw_thm_asm `validIntervalbounds (Unop Neg f) absenv P dVars` validIntervalbounds_def
\\ Cases_on `absenv (Unop Neg f)`
\\ qmatch_assum_rename_tac `absenv (Unop Neg f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, negateInterval_def]
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`,`v1`] assume_tac thm)
\\ qpat_x_assum `absenv f = _` (fn thm => fs[thm])
\\ `eval_exp E (toRMap Gamma) (Unop Neg (toREval f)) (evalUnop Neg v) M0`
by (fs[] \\ match_mp_tac Unop_neg'
\\ qexistsl_tac [`M0`, `v`] \\ fs[])
\\ qexists_tac `(evalUnop Neg v)` \\ fs[]
\\ fs[evalUnop_def, Once toREval_def] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `- SND iv_f` \\ conj_tac \\ simp [])
>- (qexists_tac `- FST iv_f` \\ conj_tac \\ simp []))
(* Inversion case *)
>- (`eval_exp E (toRMap Gamma) (Unop Inv (toREval f)) (evalUnop Inv v) M0`
by (fs[]
\\ match_mp_tac Unop_inv'
\\ qexistsl_tac [`M0`, `v`,`0`] \\ fs[mTypeToQ_def, perturb_def, evalUnop_def]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Unop Inv f)` \\ Cases_on `absenv f` \\ fs[IVhi_def, IVlo_def]
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ CCONTR_TAC \\ fs[] \\ rveq
>- (`0 < 0:real` by (match_mp_tac REAL_LET_TRANS \\ qexists_tac `SND iv_f` \\ fs[]) \\ fs[] )
>- (`0 < 0:real` by (match_mp_tac REAL_LTE_TRANS \\ qexists_tac `FST iv_f` \\fs[]) \\ fs[]))
\\ qexists_tac `evalUnop Inv v` \\ fs []
\\ fs [mTypeToQ_def]
\\ simp[evalUnop_def]
\\ rw_thm_asm `validIntervalbounds a b c d` validIntervalbounds_def
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `Gamma`] assume_tac thm)
\\ Cases_on `absenv (Unop Inv f)`
\\ qmatch_assum_rename_tac `absenv (Unop Inv f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ rpt (qpat_x_assum `!v. _ ==> _` kall_tac)
\\ rpt (qpat_x_assum `validIntervalbounds f absenv P dVars /\ _ /\ _ /\ _ /\ _ ==> _` kall_tac)
\\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `inv (SND iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v` by REAL_ASM_ARITH_TAC
\\ `-SND iv_f <= -v` by REAL_ASM_ARITH_TAC
\\ `inv (-v) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(-v) = - (inv v)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv v) <= - (inv (SND iv_f))` by fs []
\\ fs[])
>- (`0 < v` by REAL_ASM_ARITH_TAC \\
`0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))
>- (qexists_tac `inv (FST iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v` by REAL_ASM_ARITH_TAC
\\ `0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `- v <= - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `inv (- FST iv_f) <= inv (- v)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(- v) = - (inv v)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv (FST iv_f)) <= - (inv v)` by fs []
\\ fs[])
>- (`0 < v` by REAL_ASM_ARITH_TAC \\
`0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))))
(* Negation case *)
>- (qexists_tac `- vR` \\ fs[negateInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
\\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ irule Unop_neg' \\ qexistsl_tac [`M0`, `vR`] \\ fs[evalUnop_def])
(* Inversion case *)
(* MARKER *)
\\ qexists_tac `1 / vR` \\ fs[invertInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
\\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC
>- (irule Unop_inv' \\ fs[] \\ qexistsl_tac [`0`, `vR`]
\\ fs[evalUnop_def, perturb_def, REAL_INV_1OVER, mTypeToQ_pos]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ `0 < 0:real` by (irule REAL_LET_TRANS \\ qexists_tac `r` \\ fs[])
\\ fs[])
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / r` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ irule REAL_LE_TRANS \\ qexists_tac `1/q` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
(* Binary operator case *)
>- (rename1 `Binop b f1 f2`
\\ `?v1. eval_exp E (toRMap Gamma) (toREval f1) v1 M0 /\
(FST (FST (absenv f1))) <= v1 /\ (v1 <= SND (FST (absenv f1)))`
by (first_x_assum match_mp_tac
......@@ -455,10 +394,8 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ conj_tac \\ fs []));
val getRetExp_def = Define `
getRetExp (f:'a cmd) =
case f of
|Let m x e g => getRetExp g
|Ret e => e`;
(getRetExp (Let m x e g) = getRetExp g) /\
(getRetExp (Ret e) = e)`;
val Rmap_updVars_comm = store_thm (
"Rmap_updVars_comm",
......
......@@ -27,6 +27,15 @@ val REAL_INV_LE_ANTIMONO_IMPR = store_thm ("REAL_INV_LE_ANTIMONO_IMPR",
``! x y. 0 < x /\ 0 < y /\ y <= x ==> inv x <= inv y``,
rpt strip_tac \\ fs[REAL_INV_LE_ANTIMONO]);
val REAL_INV_LE_ANTIMONO_IMPL = store_thm ("REAL_INV_LE_ANTIMONO_IMPL",
``! x y. x <0 /\ y < 0 /\ y <= x ==> inv x <= inv y``,
rpt strip_tac
\\ once_rewrite_tac [GSYM REAL_LE_NEG]
\\ `- inv y = inv (- y)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- inv x = inv (- x)` by (irule REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ ntac 2(FIRST_X_ASSUM (fn thm => once_rewrite_tac [ thm]))
\\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]);
val REAL_MUL_LE_COMPAT_NEG_L = store_thm( "REAL_MUL_LE_COMPAT_NEG_L",
``!(a:real) b c. a <= &0 /\ b <= c ==> a * c <= a * b``,
rpt strip_tac
......
open preamble miscTheory
open DaisyTactics
open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
CommandsTheory DaisyMapTheory
IntervalValidationTheory CommandsTheory DaisyMapTheory
val _ = new_theory "Typing";
val typeExpression_def = Define `
val typeExpression_def = FDefine ``typeExpression`` `
typeExpression (Gamma: num -> mType option) (e: real exp) : mType option =
case e of
| Var v => Gamma v
......@@ -21,7 +21,7 @@ val typeExpression_def = Define `
let tm1 = typeExpression Gamma e1 in
case tm1 of
| SOME m1 => if (morePrecise m1 m) then SOME m else NONE
| NONE => NONE`
| NONE => NONE`;
(* val typeMap_def = Define ` *)
(* typeMap (Gamma: num -> mType option) (e: real exp) (e': real exp) : mType option = *)
......@@ -37,7 +37,7 @@ val typeExpression_def = Define `
(* | NONE, NONE => NONE) *)
(* | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'` *)
val typeMap_def = Define `
val typeMap_def = FDefine ``typeMap`` `
typeMap (Gamma:num -> mType option) (e:real exp) (tMap:typeMap) =
if (DaisyMapTree_mem e tMap)
then tMap
......@@ -70,7 +70,7 @@ val typeMap_def = Define `
else DaisyMapTree_empty)