Merge pull request #975 from CakeML/byte

Move byteTheory to HOL
CakeML · Dec 1, 2023 · 37aeb0e · 37aeb0e
2 parents 8ac36a2 + a3cf8bb
commit 37aeb0e
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 842 deletions.
diff --git a/compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml b/compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml
@@ -947,7 +947,7 @@ Proof
       \\ TRY PURE_CASE_TAC \\ fs[CaseEq"option"]
       \\ rveq \\ fs[] \\ rfs[]
       >- ( first_x_assum drule \\ simp[OPTREL_def] )
-      >- metis_tac[]
+      >- ( first_x_assum drule \\ simp[OPTREL_def] )
       >- metis_tac[])
     >- (
       reverse(fs[fsFFITheory.ffi_close_def, OPTION_CHOICE_EQUALS_OPTION] \\ rveq \\ fs[])
@@ -1073,6 +1073,9 @@ Proof
   \\ first_x_assum irule
   \\ fs[fsFFIPropsTheory.inFS_fname_def]
   \\ rw[] \\ PURE_CASE_TAC \\ fs[]
+  >- (
+    first_x_assum drule>>
+    fs[])
   \\ metis_tac[]
 QED
 

diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
@@ -341,7 +341,7 @@ Theorem pmatch_update:
           match_res_rel (λenv env'.
             LIST_REL (λ(n,v) (m,w). n = m ∧ v_rel fr ft fe v w)
                      env env') res res')
-Proof
+Proof[exclude_simps = option.OPTREL_NONE]
   ho_match_mp_tac pmatch_ind \\ rw [] \\ gvs [pmatch_def, v_rel_def, SF SFY_ss]
   >- (rw [] \\ gs [])
   >- (

diff --git a/misc/README.md b/misc/README.md
@@ -4,9 +4,6 @@ and what we want to use for CakeML development.
 [basicComputeLib.sml](basicComputeLib.sml):
 Build a basic compset for evaluation in the logic.
 
-[byteScript.sml](byteScript.sml):
-A theory about byte-level manipulation of machine words.
-
 [induct_tweakLib.sml](induct_tweakLib.sml):
 Code for adjusting and improving induction theorems.