From d620d76ec5daa5f15e545b74afdb334f4e30a92e Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 9 Mar 2021 13:08:12 +0100
Subject: [PATCH] Update translation files
---
hol4/binary/checkerBinaryScript.sml | 2 --
hol4/binary/transScript.sml | 16 ++++++++++------
2 files changed, 10 insertions(+), 8 deletions(-)
diff --git a/hol4/binary/checkerBinaryScript.sml b/hol4/binary/checkerBinaryScript.sml
index 50a515b2..bdbff08c 100644
--- a/hol4/binary/checkerBinaryScript.sml
+++ b/hol4/binary/checkerBinaryScript.sml
@@ -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);
diff --git a/hol4/binary/transScript.sml b/hol4/binary/transScript.sml
index ffd59486..a8a27846 100644
--- a/hol4/binary/transScript.sml
+++ b/hol4/binary/transScript.sml
@@ -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.
--
GitLab