Commit 2d2ea6b1 authored by Heiko Becker's avatar Heiko Becker

Resolve cheated lemmas

parent 210a23a8
......@@ -227,18 +227,27 @@ fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER]
by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\
REAL_ASM_ARITH_TAC));
val iv_inv_preserves_valid = store_thm ("iv_neg_preserves_valid",
val iv_inv_preserves_valid = store_thm ("iv_inv_preserves_valid",
``!iv.
(IVhi iv < 0 \/ 0 < IVlo iv) /\
valid iv ==> valid (invertInterval iv)``,
fs [valid_def, invertInterval_def, IVlo_def, IVhi_def]
\\ rpt strip_tac
>- (cheat)
>- (fs [GSYM REAL_INV_1OVER]
\\ `- (inv (FST iv)) <= - (inv (SND iv))` suffices_by fs []
\\ `0 < - SND iv` by REAL_ASM_ARITH_TAC
\\ `- (inv (FST iv)) = inv (- (FST iv))` by (match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- (inv (SND iv)) = inv (- (SND iv))` by (match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ rpt (qpat_x_assum `- (inv _) = _` (fn thm => rewrite_tac [thm]))
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ rpt CONJ_TAC \\ fs []
\\ match_mp_tac REAL_LET_TRANS
\\ asm_exists_tac \\ fs [])
>- (fs[GSYM REAL_INV_1OVER]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ rpt CONJ_TAC \\ fs[]
\\ rpt CONJ_TAC \\ fs []
\\ match_mp_tac REAL_LTE_TRANS
\\ asm_exists_tac \\ fs[]));
\\ asm_exists_tac \\ fs []));
val interval_addition_valid = store_thm ("interval_addition_valid",
``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``,
......@@ -254,6 +263,17 @@ fs iv_ss \\ rpt strip_tac
match_mp_tac REAL_LE_TRANS \\
HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX]));
val iv_add_preserves_valid = store_thm ("iv_add_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (addInterval iv1 iv2)``,
fs [valid_def, addInterval_def, IVlo_def, IVhi_def, absIntvUpd_def, min4_def, max4_def]
\\ rpt strip_tac
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_MIN_LE1]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 + FST iv2` \\ fs [REAL_LE_MAX1]);
val interval_subtraction_valid = store_thm ("interval_subtraction_valid",
``!iv1 iv2.
validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``,
......@@ -263,6 +283,17 @@ rpt gen_tac \\ strip_tac \\
match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\
fs []);
val iv_sub_preserves_valid = store_thm ("iv_sub_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (subtractInterval iv1 iv2)``,
once_rewrite_tac [subtractInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_add_preserves_valid
\\ conj_tac \\ fs []
\\ match_mp_tac iv_neg_preserves_valid \\ fs []);
val interval_multiplication_valid = store_thm ("interval_multiplication_valid",
``!iv1 iv2 a b.
contained a iv1 /\ contained b iv2 ==> contained (a * b) (multInterval iv1 iv2)``,
......@@ -402,6 +433,19 @@ fs iv_ss \\ rpt strip_tac
rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)])
max4_correct)))));
val iv_mult_preserves_valid = store_thm ("iv_mult_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 ==>
valid (multInterval iv1 iv2)``,
fs [valid_def, multInterval_def, IVlo_def, IVhi_def, absIntvUpd_def, min4_def, max4_def]
\\ rpt strip_tac
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 * FST iv2`
\\ fs [REAL_MIN_LE1]
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `FST iv1 * FST iv2`
\\ fs [REAL_LE_MAX1]);
val interval_division_valid = store_thm ( "interval_division_valid",
``!(iv1:interval) (iv2:interval) (a:real) (b:real).
(IVhi iv2 < 0 \/ 0 < IVlo iv2) /\
......@@ -420,6 +464,17 @@ match_mp_tac
(iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid)) \\
fs[]);
val iv_div_preserves_valid = store_thm ("iv_div_preserves_valid",
``!iv1 iv2.
valid iv1 /\ valid iv2 /\ (IVhi iv2 < 0 \/ 0 < IVlo iv2) ==>
valid (divideInterval iv1 iv2)``,
once_rewrite_tac [divideInterval_def]
\\ rpt strip_tac
\\ match_mp_tac iv_mult_preserves_valid
\\ fs []
\\ match_mp_tac iv_inv_preserves_valid
\\ fs []);
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
``!a iv. contained a iv ==> abs a <= maxAbs iv``,
......
......@@ -393,45 +393,94 @@ val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzer
\\ Cases_on `absenv f2` \\ Cases_on `absenv f1` \\ Cases_on `absenv (Binop Div f1 f2)`
\\ fs [Once validIntervalbounds_def, noDivzero_def, IVhi_def, IVlo_def]);
val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
``!(f:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
(!v. v IN domain dVars ==>
valid (FST (absenv (Var v)))) /\
validIntervalbounds f absenv P dVars ==>
valid (FST (absenv f))``,
cheat
(* Induct
\\ rpt strip_tac \\ fs [Once validIntervalbounds_def]
Induct
\\ rpt strip_tac
>- (first_x_assum (fn thm => qspecl_then [`n`] ASSUME_TAC thm)
\\ Cases_on `absenv (Var n)` \\ fs[])
>- (Cases_on `absenv (Param n)` \\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ TRY (simp[])
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ CONJ_TAC \\ simp[])
>- (Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def]
\\ Cases_on `absenv (Var n)`
\\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
\\ REAL_ASM_ARITH_TAC)
>- (rpt strip_tac
\\ Cases_on `absenv (Const v)` \\ fs[isSupersetInterval_def, valid_def, validIntervalbounds_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ CONJ_TAC \\ fs[IVlo_def, IVhi_def])
>- (Cases_on `absenv (Unop u f)` \\ fs[]
\\ qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
>- (qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Unop u f)` \\ fs[]
\\ `valid (FST (absenv f))`
by (first_x_assum match_mp_tac \\
qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f` \\ fs[]
\\ Cases_on `u` \\ fs[isSupersetInterval_def]
>- (`valid (negateInterval q')` by (match_mp_tac iv_neg_preserves_valid \\ fs[])
\\ fs[valid_def]
\\ Cases_on `u`
>- (`valid (negateInterval q')`
by (match_mp_tac iv_neg_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
>- (cheat) (* FIXME: ONLY TWO CASES! *)
>- (cheat))
>- (cheat) *)
);
>- (`valid (invertInterval q')`
by (match_mp_tac iv_inv_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
>- (match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])))
>- (rename1 `Binop b f1 f2`
\\ qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Binop b f1 f2)` \\ rename1 `absenv (Binop b f1 f2) = (iv,err)`
\\ fs[]
\\ `valid (FST (absenv f1))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ `valid (FST (absenv f2))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
\\ rename1 `absenv f1 = (iv_f1, err_f1)`
\\ rename1 `absenv f2 = (iv_f2, err_f2)`
\\ fs[]
\\ Cases_on `b`
>- (`valid (addInterval iv_f1 iv_f2)`
by (match_mp_tac iv_add_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (subtractInterval iv_f1 iv_f2)`
by (match_mp_tac iv_sub_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (multInterval iv_f1 iv_f2)`
by (match_mp_tac iv_mult_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (`valid (divideInterval iv_f1 iv_f2)`
by (match_mp_tac iv_div_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])));
val _ = export_theory();
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