Fix more name-rebinding problems

build -t2 now goes through

examples/computability/kolmog/boolListsScript.sml

@@ -1243,7 +1243,7 @@ Proof
        rw[primrec_rules, primrec_pr_nblsnd0, primrec_ell])
 QED
 
-Theorem checkpair_i_def[simp] = new_specification(
+Theorem checkpair_i_def[simp,allow_rebind] = new_specification(
   "checkpair_i_def", ["checkpair_i"],
   MATCH_MP unary_rec_fns_phi recfn_checkpair)
 

examples/computability/kolmog/kraft_ineqScript.sml

@@ -360,12 +360,12 @@ Proof
   Cases_on‘y=e’>> fsr[] >> RES_TAC >> fsr[]
 QED
 
-Theorem maxr_set_def = new_specification(
+val maxr_set_def = new_specification(
   "maxr_set_def",["maxr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] max_rs_lemma
   );
 
-Theorem minr_set_def = new_specification(
+val minr_set_def = new_specification(
   "minr_set_def",["minr_set"],
   SIMP_RULE(srw_ss() )[SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM] min_rs_lemma);
 

examples/computability/turing/turing_machine_primeqScript.sml

@@ -1200,10 +1200,6 @@ rpt strip_tac >> qexists_tac`Cn (pr2 nel) [proj 0;Cn (pr1 (list_rec_comb c n)) [
 rpt conj_tac >- (rpt (irule primrec_cn >> rw[primrec_rules,primrec_nel,primrec_list_rec_comb]))>>
  simp[list_rec_comb_def] >> simp[list_rec_comb_corr,nel_nlist_of,LIST_REC_def] )
 
-val nleng_thm = new_specification("nleng_def", ["nleng"],
-list_num_rec_thm |> SPECL[``0n``,``Cn succ [proj 2]``]
-                 |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
-
 val nrev_thm = new_specification("nrev_def", ["nrev"],
 list_num_rec_thm |> SPECL[``0n``,``Cn (pr2 napp) [proj 2;Cn (pr2 ncons) [proj 0;zerof] ]``]
                  |> SIMP_RULE (srw_ss())[primrec_cn, primrec_rules])
@@ -1270,12 +1266,6 @@ val primrec_pr_INITIAL_TAPE_TM_NUM = Q.store_thm(
        rw[primrec_rules,primrec_pr_eq,primrec_nsnd,primrec_nfst]) >>
   fs[primrec_proj]);
 
-val pr_INITIAL_TM_NUM_def = Define`
-pr_INITIAL_TM_NUM = Cn (pr2 npair) [zerof;Cn tape_encode
- [Cn (pr1 nfst) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]];
-  Cn (pr1 nfst) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]];
-  Cn (pr1 nsnd) [Cn (pr1 nsnd) [Cn pr_INITIAL_TAPE_TM_NUM [zerof;Cn concatWith_Z [proj 0]]]]]]`;
-
 val pr_ODD_def = Define`pr_ODD = pr_cond (Cn pr_eq [Cn pr_mod [proj 0;twof];onef]) onef zerof`
 
 val pr_ODD_corr = Q.store_thm("pr_ODD_corr",
@@ -1490,7 +1480,6 @@ Cases_on `A` >> fs[])
 val recfn_rulesl = CONJUNCTS recfn_rules
 val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3))
 val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4))
-val recfnMin = save_thm("recfnMin", List.nth(recfn_rulesl, 5))
 
 (* Probably need to include a 'tape reset' type function, ie tm_return_num *)
 val recfn_tm_def = Define`

examples/decidable_separationLogic/src/decidable_separationLogicLibScript.sml

@@ -1341,47 +1341,23 @@ REPEAT STRIP_TAC THEN (
 
 
 
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
-   ASM_SIMP_TAC list_ss [],
-   ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
-
-
-
-val INFERENCE_STAR_INTRODUCTION___EVAL1 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL1",
- ``!sfL'' c1 c2 pfL sfL pfL' sfL'.
-         (LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
-         LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL''))``,
-
-
-REPEAT STRIP_TAC THEN
-`LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
- LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')` by (
-   MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
-   SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
-) THEN
-ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
-
-Induct_on `sfL''` THENL [
+Theorem INFERENCE_STAR_INTRODUCTION___EVAL1:
+ !sfL'' c1 c2 pfL sfL pfL' sfL'.
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL) (pfL',sfL') ==>
+   LIST_DS_ENTAILS (c1,c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'')
+Proof
+  REPEAT STRIP_TAC THEN
+  ‘LIST_DS_ENTAILS (c1, c2) (pfL,sfL++sfL'') (pfL',sfL'++sfL'') =
+   LIST_DS_ENTAILS (c1, c2) (pfL,sfL''++sfL) (pfL',sfL''++sfL')’
+    by (MATCH_MP_TAC LIST_DS_ENTAILS___PERM THEN
+        SIMP_TAC std_ss [PERM_REFL, PERM_APPEND]
+       ) THEN
+  ASM_REWRITE_TAC[] THEN POP_ASSUM (K ALL_TAC) THEN
+  Induct_on ‘sfL''’ THENL [
    ASM_SIMP_TAC list_ss [],
    ASM_SIMP_TAC list_ss [INFERENCE_STAR_INTRODUCTION___IMPL]
-])
-
+  ]
+QED
 
 val INFERENCE_STAR_INTRODUCTION___EVAL2 = store_thm ("INFERENCE_STAR_INTRODUCTION___EVAL2",
  ``!x n1 n2 c1 c2 pfL sfL pfL' sfL'.

examples/formal-languages/regular/regexpScript.sml

@@ -130,15 +130,15 @@ Datatype
     | Neg regexp`
 ;
 
-Theorem regexp_induction :
+Theorem regexp_induction[allow_rebind] :
  !P Q.
      (!cs. P (Chset cs)) /\
      (!r r0. P r /\ P r0 ==> P (Cat r r0)) /\
      (!r. P r ==> P (Star r)) /\ (!l. Q l ==> P (Or l)) /\
      (!r. P r ==> P (Neg r)) /\ Q [] /\ (!r l. P r /\ Q l ==> Q (r::l)) ==>
      (!r. P r) /\ !l. Q l
 Proof
- ACCEPT_TAC (fetch "-" "regexp_induction")
+  ACCEPT_TAC (fetch "-" "regexp_induction")
 QED
 
 Triviality regexp_distinct = fetch "-" "regexp_distinct";

examples/fun-op-sem/cbv-lc/logrelScript.sml

@@ -119,7 +119,7 @@ val state_rel_rw =
 Theorem state_rel_rw = state_rel_rw
 
 (* Convert the if-then-else to ⇒ *)
-Theorem val_rel_def = SIMP_RULE (srw_ss()) [] val_rel_def
+Theorem val_rel_def[allow_rebind] = SIMP_RULE (srw_ss()) [] val_rel_def
 
 (* Package up exec_rel nicely in terms of res_rel. *)
 Theorem exec_rel_rw:

examples/fun-op-sem/ml/typeSoundScript.sml

@@ -280,8 +280,9 @@ val sem_clock = store_thm("sem_clock",
 val r = term_rewrite [``check_clock s1 s = s1``,
     ``s.clock <> 0 /\ s1.clock <> 0 <=> s1.clock <> 0``]
 
-val sem_def = store_thm("sem_def",
-  sem_def |> concl |> r,
+Theorem sem_def[allow_rebind]:
+  ^(sem_def |> concl |> r)
+Proof
   rpt strip_tac >>
   rw[Once sem_def] >>
   BasicProvers.CASE_TAC >>
@@ -294,10 +295,12 @@ val sem_def = store_thm("sem_def",
   imp_res_tac sem_clock >>
   simp[check_clock_id] >>
   `F` suffices_by rw[] >>
-  DECIDE_TAC)
+  DECIDE_TAC
+QED
 
-val sem_ind = store_thm("sem_ind",
-  sem_ind |> concl |> r,
+Theorem sem_ind[allow_rebind]:
+  ^(sem_ind |> concl |> r)
+Proof
   ntac 2 strip_tac >>
   ho_match_mp_tac sem_ind >>
   rw[] >>
@@ -306,7 +309,8 @@ val sem_ind = store_thm("sem_ind",
   res_tac >>
   imp_res_tac sem_clock >>
   fsrw_tac[ARITH_ss][check_clock_id] >> rfs[] >>
-  fsrw_tac[ARITH_ss][check_clock_id])
+  fsrw_tac[ARITH_ss][check_clock_id]
+QED
 
 (* alternative un-clocked relational big-step semantics for comparison *)
 

examples/l3-machine-code/arm/decompiler/arm_decomp_demoScript.sml

@@ -283,7 +283,6 @@ val (PID_C2_cert, PID_C2_def) = core_decompilerLib.core_decompile "PID_C2" `
     edc37a00             (* vstr       s15, [r3]                *)
     e8bd0010             (* pop        {r4}                     *)`;
 
-val _ = save_thm("PID_C2_def",PID_C2_def);
 val _ = save_thm("PID_C2_cert",PID_C2_cert);
 
 val () = export_theory()

examples/l3-machine-code/m0/step/m0_stepScript.sml

@@ -741,13 +741,6 @@ val Decode_simps = save_thm("Decode_simps",
                      blastLib.BBLAST_CONV ``v2w [a; b; c] = ^w``
                   end)) |> Drule.LIST_CONJ);
 
-val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt",
-   `!imm2 w C s.
-        Shift_C (w: word32, SRType_LSL, imm2, C) s =
-        ((w << imm2, if imm2 = 0 then C else testbit 32 (shiftl (w2v w) imm2)),
-         s)`,
-   lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F])
-
 local
    val lem =
     (SIMP_RULE (srw_ss()) [] o Q.SPECL [`v`, `32`] o

examples/l3-machine-code/x64/decompiler/x64_decomp_demoScript.sml

@@ -38,7 +38,10 @@ val _ = save_thm("decomp_cert",decomp_cert);
 
 val () = Feedback.set_trace "x64 spec" 2
 
-val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
+val (decomp1_cert,decomp1_def) =
+  Feedback.trace ("Theory.allow_rebinds", 1)
+     (x64_decompLib.x64_decompile "decomp1")
+  ‘
   (*  0: *) 55              (* push   %rbp *)
   (*  1: *) 4889e5          (* mov    %rsp,%rbp *)
   (*  4: *) 4883ec20        (* sub    $0x20,%rsp *)
@@ -62,7 +65,7 @@ val (decomp1_cert,decomp1_def) = x64_decompLib.x64_decompile "decomp1" `
   (* 3b: *) 84c0            (* test   %al,%al *)
   (* 3d: *) 75d7            (* jne    16 <transform+0x16> *)
   (* 3f: *) 488b45e8        (* mov    -0x18(%rbp),%rax *)
-  (* 43: *) c9              (* leaveq  *) `
+  (* 43: *) c9              (* leaveq  *) ’
 
 val _ = save_thm("decomp1_cert",decomp1_cert);
 

examples/machine-code/decompiler/decompilerLib.sml

@@ -1642,7 +1642,7 @@ fun extract_function name th entry exit function_in_out = let
   val main_thm = finalise main_thm
   val pre_thm = finalise pre_thm
   (* define temporary abbreviation *)
-  val silly_string = Theory.temp_binding "(( step ))"
+  val silly_string = Theory.temp_binding "((step))"
   val step_def =
      new_definition
         (silly_string,mk_eq(mk_var(silly_string,type_of step_fun),step_fun))

examples/separationLogic/src/generalHelpersScript.sml

@@ -113,36 +113,12 @@ val EL_LUPDATE___NO_COND = store_thm ("EL_LUPDATE___NO_COND",
 SIMP_TAC std_ss [EL_LUPDATE]);
 
 
-val TAKE_LUPDATE = store_thm ("TAKE_LUPDATE",
-``!n1 n2 e l. TAKE n1 (LUPDATE e n2 l) =
-  if (n1 <= n2) then TAKE n1 l else
-  LUPDATE e n2 (TAKE n1 l)``,
-
-Induct_on `n1` THEN
-Cases_on `n2` THEN
-Cases_on `l` THEN
-ASM_SIMP_TAC list_ss [LUPDATE_def,
-  COND_RAND, COND_RATOR])
-
-
 val TAKE_LUPDATE___SIMPLE = store_thm ("TAKE_LUPDATE___SIMPLE",
 ``!n1 n2 e l. TAKE n1 (LUPDATE e n2 l) =
   LUPDATE e n2 (TAKE n1 l)``,
 Induct_on `n1` THEN Cases_on `n2` THEN Cases_on `l` THEN
 ASM_SIMP_TAC list_ss [LUPDATE_def])
 
-
-val DROP_LUPDATE = store_thm ("DROP_LUPDATE",
-``!n1 n2 e l. DROP n1 (LUPDATE e n2 l) =
-   if (n2 < n1) then DROP n1 l else
-  LUPDATE e (n2-n1) (DROP n1 l)``,
-
-Induct_on `n1` THEN
-Cases_on `n2` THEN
-Cases_on `l` THEN
-ASM_SIMP_TAC list_ss [LUPDATE_def]);
-
-
 val LUPDATE_APPEND1 = store_thm ("LUPDATE_APPEND1",
 ``!n l1 l2. n < LENGTH l1 ==> (
      LUPDATE e n (l1 ++ l2) =
@@ -1059,10 +1035,6 @@ val IMAGE_ABS2 = store_thm ("IMAGE_ABS2",
 ``IMAGE f P = (\x. ?y. (x = f y) /\ y IN P)``,
 SIMP_TAC std_ss [EXTENSION, IN_IMAGE, IN_ABS]);
 
-val IMAGE_ABS = store_thm ("IMAGE_ABS",
-``IMAGE f (\x. P x) = (\x. ?y. (x = f y) /\ P y)``,
-SIMP_TAC std_ss [IMAGE_ABS2, IN_ABS]);
-
 val IN_ABS2 = store_thm ("IN_ABS2",
         ``(!t. (t IN X = Q t)) = (X = \t. Q t)``,
 SIMP_TAC std_ss [EXTENSION, IN_ABS]);

examples/temporal_deep/src/deep_embeddings/ctl_starScript.sml

@@ -441,39 +441,6 @@ val LTL_TO_CTL_STAR_def =
    (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))`;
 
 
-val LTL_TO_CTL_STAR_THM =
-  store_thm ("LTL_TO_CTL_STAR_THM",
-    ``!b f c f1 f2.
-   (LTL_TO_CTL_STAR (LTL_PROP b) = (CTL_STAR_PROP b)) /\
-   (LTL_TO_CTL_STAR (LTL_NOT f) = (CTL_STAR_NOT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_OR (f1, f2)) = (CTL_STAR_OR (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_IMPL (f1, f2)) = (CTL_STAR_IMPL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_COND (c, f1, f2)) = (CTL_STAR_COND (LTL_TO_CTL_STAR c, LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_EQUIV (f1, f2)) = (CTL_STAR_EQUIV (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_NEXT f) = (CTL_STAR_NEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_EVENTUAL f) = (CTL_STAR_EVENTUAL (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_ALWAYS f) = (CTL_STAR_ALWAYS (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_UNTIL (f1, f2)) = (CTL_STAR_UNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_BEFORE (f1, f2)) = (CTL_STAR_BEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_SBEFORE (f1, f2)) = (CTL_STAR_SBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_WHILE (f1, f2)) = (CTL_STAR_WHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_SWHILE (f1, f2)) = (CTL_STAR_SWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSNEXT f) = (CTL_STAR_PSNEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PNEXT f) = (CTL_STAR_PNEXT (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PEVENTUAL f) = (CTL_STAR_PEVENTUAL (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PALWAYS f) = (CTL_STAR_PALWAYS (LTL_TO_CTL_STAR f))) /\
-   (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PUNTIL (f1, f2)) = (CTL_STAR_PUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PBEFORE (f1, f2)) = (CTL_STAR_PBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSBEFORE (f1, f2)) = (CTL_STAR_PSBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PWHILE (f1, f2)) = (CTL_STAR_PWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
-   (LTL_TO_CTL_STAR (LTL_PSWHILE (f1, f2)) = (CTL_STAR_PSWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))``,
-
-   EVAL_TAC THEN PROVE_TAC[]);
-
-
 val LTL_FORMULAS_ARE_PATH_FORMULAS =
   store_thm (
     "LTL_FORMULAS_ARE_PATH_FORMULAS",

examples/temporal_deep/src/deep_embeddings/infinite_pathScript.sml

@@ -403,35 +403,6 @@ val BEFORE_ON_PATH_STRONG___BEFORE_ON_PATH =
    EXISTS_TAC ``u:num`` THEN
    FULL_SIMP_TAC arith_ss []);
 
-
-val BEFORE_ON_PATH___SUC =
- store_thm
-  ("BEFORE_ON_PATH___SUC",
-   ``!v t a b. ((BEFORE_ON_PATH_RESTN t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN (SUC t) v a b)``,
-   REWRITE_TAC [BEFORE_ON_PATH_RESTN_def] THEN
-   REPEAT STRIP_TAC THEN
-   `t <= t'` by DECIDE_TAC THEN
-   RES_TAC THEN
-   EXISTS_TAC ``u:num`` THEN
-   ASM_REWRITE_TAC[] THEN
-   `~(u = t)` by METIS_TAC[] THEN
-   DECIDE_TAC);
-
-
-val BEFORE_ON_PATH_STRONG___SUC =
- store_thm
-  ("BEFORE_ON_PATH_STRONG___SUC",
-   ``!v t a b. ((BEFORE_ON_PATH_RESTN_STRONG t v a b) /\ ~(P_SEM (v t) a)) ==> (BEFORE_ON_PATH_RESTN_STRONG (SUC t) v a b)``,
-   REWRITE_TAC [BEFORE_ON_PATH_RESTN_STRONG_def] THEN
-   REPEAT STRIP_TAC THEN
-   `t <= t'` by DECIDE_TAC THEN
-   RES_TAC THEN
-   EXISTS_TAC ``u:num`` THEN
-   ASM_REWRITE_TAC[] THEN
-   `~(u = t)` by METIS_TAC[] THEN
-   DECIDE_TAC);
-
-
 val NOT_ON_PATH___IMP_ON_PATH =
  store_thm
   ("NOT_ON_PATH___IMP_ON_PATH",