Commit eb84cd10 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Update transScript

parent 0b96b0da
open preamble open preamble
open simpLib realTheory realLib RealArith stringTheory open simpLib realTheory realLib RealArith stringTheory
...@@ -190,7 +189,7 @@ val precond_validErrorbound_true = prove (`` ...@@ -190,7 +189,7 @@ val precond_validErrorbound_true = prove (``
\\ first_x_assum irule \\ first_x_assum irule
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ rw_asm_star `absenv _ = _` \\ rw_asm_star `absenv _ = _`
\\ Cases_on `absenv x12` \\ Cases_on `absenv x15`
\\ fs []) \\ fs [])
\\ conj_tac \\ conj_tac
>- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm) >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
...@@ -240,6 +239,10 @@ val precond_validErrorbound_true = prove (`` ...@@ -240,6 +239,10 @@ val precond_validErrorbound_true = prove (``
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm]) \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
\\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def] \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
\\ REAL_ASM_ARITH_TAC)) \\ REAL_ASM_ARITH_TAC))
\\ conj_tac
>- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ rpt conj_tac \\ first_x_assum match_mp_tac
\\ fs [Once validIntervalbounds_def])
\\ rpt strip_tac \\ rpt strip_tac
\\ rveq \\ rveq
\\ fs[] \\ fs[]
......
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