Commit d620d76e authored by Heiko Becker's avatar Heiko Becker
Browse files

Update translation files

parent a90304a5
......@@ -4,8 +4,6 @@ val _ = new_theory "checkerBinary"
val checker_compiled = save_thm("checker_compiled",
compile_x64
1000 (* stack size in MB *)
1000 (* heap size in MB *)
"checker"
main_prog_def);
......
......@@ -30,7 +30,7 @@ val real_div_side = prove(
val check_def = Define `
check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
case n of
| SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
| SUC n' => (case CertificateCheckerCmd f A P Gamma of | SOME _ => T |_ => F)/\ check f P A Gamma n'
| _ => T`
val check_all_def = Define `
......@@ -303,7 +303,9 @@ val precond_validErrorbound_true = prove (``
\\ rveq
\\ fs[]
\\ first_x_assum irule
\\ Flover_compute ``validIntervalbounds``)
\\ qpat_x_assum `validIntervalbounds _ _ _ _` mp_tac
\\ simp[SimpL $==>, Once validIntervalbounds_def]
\\ ntac 2 (TOP_CASE_TAC \\ gs[]))
\\ conj_tac
>- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
\\ conj_tac
......@@ -351,11 +353,13 @@ val precond_validErrorbound_true = prove (``
\\ conj_tac
>- (rpt strip_tac
\\ rveq
\\ Flover_compute ``validIntervalbounds``
\\ first_x_assum irule \\ fs[])
\\ qpat_x_assum `validIntervalbounds _ _ _ _` mp_tac
\\ simp[SimpL $==>, Once validIntervalbounds_def]
\\ ntac 2 (TOP_CASE_TAC \\ gs[]))
\\ rpt strip_tac
\\ rveq \\ Flover_compute ``validIntervalbounds``
\\ first_x_assum irule \\ fs[]);
\\ qpat_x_assum `validIntervalbounds _ _ _ _` mp_tac
\\ simp[SimpL $==>, Once validIntervalbounds_def]
\\ ntac 2 (TOP_CASE_TAC \\ gs[]));
val precond_errorbounds_true = prove (``
!P f exprTypes A dVars.
......
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