Fix rebinds

CakeML · Oct 17, 2023 · 4d4db90 · 4d4db90
1 parent c9a59de
commit 4d4db90
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 16 deletions.
diff --git a/compiler/backend/languages/relations/pure_presScript.sml b/compiler/backend/languages/relations/pure_presScript.sml
@@ -231,9 +231,9 @@ End
 Overload "<-->" = “bidir”
 val _ = set_fixity "<-->" (Infixl 480);
 
-Theorem bidir_refl[simp] = bidir_refl;
+Theorem bidir_refl[allow_rebind,simp] = bidir_refl;
 
-Theorem bidir_sym:
+Theorem bidir_sym[allow_rebind]:
   ∀x y. (x <--> y) ⇔ (y <--> x)
 Proof
   metis_tac [bidir_sym]
@@ -300,7 +300,7 @@ End
 Overload "~~>" = “pres”
 val _ = set_fixity "~~>" (Infixl 480);
 
-Theorem pres_refl[simp] = pres_refl;
+Theorem pres_refl[simp,allow_rebind] = pres_refl;
 
 (*----------------------------------------------------------------------------*
    Proof of preservation of well-formedness

diff --git a/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml b/compiler/backend/passes/proofs/thunk_case_d2bProofScript.sml
@@ -1482,7 +1482,8 @@ Proof
   >- (strip_tac >> rw[Once exp_rel_cases] >> gvs[eval_to_def])
 QED
 
-Theorem exp_rel_eval_to = REWRITE_RULE [d2b_goal_def] exp_rel_eval_to;
+Theorem exp_rel_eval_to[allow_rebind] =
+  REWRITE_RULE [d2b_goal_def] exp_rel_eval_to;
 
 Theorem exp_rel_eval:
   exp_rel x y ∧

diff --git a/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml b/compiler/backend/passes/proofs/thunk_combine_Forcing_LambdasScript.sml
@@ -516,12 +516,6 @@ Proof
   Induct >> gvs [combine_rel_def]
 QED
 
-Theorem combine_rel_Apps:
-  ∀l1 l2 x y. combine_rel x y ∧ LIST_REL combine_rel l1 l2 ⇒ combine_rel (Apps x l1) (Apps y l2)
-Proof
-  Induct >> gvs [combine_rel_def, PULL_EXISTS]
-QED
-
 Theorem combine_rel_freevars:
   ∀x y. combine_rel x y ⇒ freevars x = freevars y
 Proof
@@ -1280,12 +1274,6 @@ Proof
   \\ CASE_TAC \\ gs []
 QED
 
-Theorem combine_rel_Lams:
-  ∀vL x y. combine_rel x y ⇒ combine_rel (Lams vL x) (Lams vL y)
-Proof
-  Induct \\ gs [combine_rel_def]
-QED
-
 Theorem combine_rel_Apps:
   ∀eL1 eL2 x y. LIST_REL combine_rel eL1 eL2 ∧ combine_rel x y ⇒ combine_rel (Apps x eL1) (Apps y eL2)
 Proof