Fix rebinds

CakeML · Oct 16, 2023 · 6773c63 · 6773c63
1 parent 833024c
commit 6773c63
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 15 deletions.
diff --git a/compiler/bootstrap/translation/inferProgScript.sml b/compiler/bootstrap/translation/inferProgScript.sml
@@ -89,7 +89,7 @@ val _ = translate
     |> SIMP_RULE std_ss [PULL_FORALL] |> SPEC_ALL
     |> MATCH_MP PRECONDITION_INTRO);
 
-Theorem t_vwalk_side_def = Q.prove(`
+Theorem t_vwalk_side_def[allow_rebind] = Q.prove(`
   !s v. t_vwalk_side s v <=> t_wfs s`,
   STRIP_TAC THEN reverse (Cases_on `t_wfs s`) THEN FULL_SIMP_TAC std_ss []
   THEN1 (ONCE_REWRITE_TAC [fetch "-" "t_vwalk_side_def"]
@@ -123,7 +123,7 @@ val _ = translate
     |> RW1 [expand_lemma] |> SIMP_RULE std_ss [PULL_FORALL]
     |> SPEC_ALL |> MATCH_MP PRECONDITION_INTRO)
 
-Theorem t_walkstar_side_def = Q.prove(`
+Theorem t_walkstar_side_def[allow_rebind] = Q.prove(`
   !s v. t_walkstar_side s v <=> t_wfs s`,
   STRIP_TAC THEN reverse (Cases_on `t_wfs s`) THEN FULL_SIMP_TAC std_ss []
   THEN1 (ONCE_REWRITE_TAC [fetch "-" "t_walkstar_side_def"]
@@ -166,7 +166,7 @@ val t_oc_side_lemma = Q.prove(
   THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) [])
   |> SIMP_RULE std_ss [];
 
-Theorem t_oc_side_def = Q.prove(`
+Theorem t_oc_side_def[allow_rebind] = Q.prove(`
   !s t v. t_oc_side s t v <=> t_wfs s`,
   STRIP_TAC THEN Cases_on `t_wfs s`
   THEN FULL_SIMP_TAC std_ss [t_oc_side_lemma]
@@ -225,15 +225,15 @@ val t_unify_side_lemma = Q.prove(
   THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []
   THEN METIS_TAC [unifyTheory.t_unify_unifier]) |> SIMP_RULE std_ss [];
 
-Theorem t_unify_side_def = Q.prove(`
+Theorem t_unify_side_def[allow_rebind] = Q.prove(`
   !s t v. t_unify_side s t v <=> t_wfs s`,
   STRIP_TAC THEN Cases_on `t_wfs s`
   THEN FULL_SIMP_TAC std_ss [t_unify_side_lemma]
   THEN ONCE_REWRITE_TAC [t_unify_side_rw]
   THEN FULL_SIMP_TAC std_ss [])
   |> update_precondition;
 
-Theorem ts_unify_side_def = Q.prove(`
+Theorem ts_unify_side_def[allow_rebind] = Q.prove(`
   !s t v. ts_unify_side s t v <=> t_wfs s`,
   STRIP_TAC THEN Cases_on `t_wfs s`
   THEN FULL_SIMP_TAC std_ss [t_unify_side_lemma]

diff --git a/examples/lpr_checker/array/lpr_composeProgScript.sml b/examples/lpr_checker/array/lpr_composeProgScript.sml
@@ -392,7 +392,7 @@ Proof
   rw[]>>qexists_tac`notfound_string lines_fname`>>xsimpl
 QED
 
-Theorem is_adjacent_build_sets:
+Theorem is_adjacent_build_sets_lemma:
   ∀xs t m n.
     is_adjacent (build_sets xs t) m n ⇔
     MEM (m,n) xs ∨ is_adjacent t m n
@@ -408,7 +408,7 @@ QED
 Theorem is_adjacent_build_sets:
   is_adjacent (build_sets xs LN) m n = MEM (m,n) xs
 Proof
-  fs [is_adjacent_build_sets]
+  fs [is_adjacent_build_sets_lemma]
   \\ fs [is_adjacent_def,lookup_def]
 QED
 

diff --git a/examples/lpr_checker/array/lpr_listScript.sml b/examples/lpr_checker/array/lpr_listScript.sml
@@ -1434,13 +1434,6 @@ Proof
   IF_CASES_TAC>>simp[]
 QED
 
-Theorem index_11:
-  index i = index x ⇔ i = x
-Proof
-  rw[index_def,EQ_IMP_THM]>>
-  intLib.ARITH_TAC
-QED
-
 Theorem earliest_rel_resize_update_list0_pre:
   ∀l earliest n z.
     list_lookup (update_earliest earliest n l) NONE (index z) =

diff --git a/translator/monadic/examples/README.md b/translator/monadic/examples/README.md
@@ -13,7 +13,7 @@ references, arrays and exceptions.
 An example showing how to use the monadic translator to translate monadic
 array search functions, including exceptions.
 
-[doubleProgScript.sml](doubleProgScript.sml):
+[doubleArgProgScript.sml](doubleArgProgScript.sml):
 An example showing how to use the monadic translator to translate monadic
 doubling functions, including using references (no arrays, no exceptions).