Fix more duplicated rewrites after breakage caused by 705d331

examples/CCS/ObsCongrScript.sml

@@ -592,25 +592,6 @@ val STRONG_IMP_OBS_CONGR = store_thm (
                    |    \/       \/   \/
                    |    E1'  ~~    ?E2'
  *)
-val OBS_CONGR_EPS = store_thm ((* NEW *)
-   "OBS_CONGR_EPS",
-  ``!E E'. OBS_CONGR E E' ==>
-           !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2``,
-    REPEAT STRIP_TAC
- >> PAT_X_ASSUM ``OBS_CONGR E E'`` MP_TAC
- >> POP_ASSUM MP_TAC
- >> Q.SPEC_TAC (`E1`, `E1`)
- >> Q.SPEC_TAC (`E`, `E`)
- >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
- >> REPEAT STRIP_TAC (* 2 sub-goals here *)
- >| [ (* goal 1 (of 2) *)
-      Q.EXISTS_TAC `E'` >> RW_TAC std_ss [EPS_REFL] \\
-      IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV,
-      (* goal 2 (of 2) *)
-      RES_TAC \\
-      IMP_RES_TAC WEAK_EQUIV_TRANS_tau \\
-      Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\
-      IMP_RES_TAC EPS_TRANS ]);
 
 val OBS_CONGR_EPS' = store_thm ((* NEW *)
    "OBS_CONGR_EPS'",
@@ -625,28 +606,6 @@ val OBS_CONGR_EPS' = store_thm ((* NEW *)
  >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC []
  >> IMP_RES_TAC WEAK_EQUIV_SYM);
 
-val OBS_CONGR_WEAK_TRANS = store_thm ((* NEW *)
-   "OBS_CONGR_WEAK_TRANS",
-  ``!E E'. OBS_CONGR E E' ==>
-           !u E1. WEAK_TRANS E u E1 ==> ?E2. WEAK_TRANS E' u E2 /\ WEAK_EQUIV E1 E2``,
-    REPEAT STRIP_TAC
- >> Cases_on `u` (* 2 sub-goals here *)
- >| [ (* goal 1 (of 2) *)
-      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS_TAU])) \\
-      IMP_RES_TAC OBS_CONGR_TRANS_LEFT \\
-      IMP_RES_TAC WEAK_EQUIV_EPS \\
-      Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\
-      MATCH_MP_TAC EPS_WEAK_EPS \\
-      take [`E'`, `E2`] >> ASM_REWRITE_TAC [EPS_REFL],
-      (* goal 2 (of 2) *)
-      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\
-      IMP_RES_TAC OBS_CONGR_EPS \\
-      IMP_RES_TAC WEAK_EQUIV_TRANS_label \\
-      IMP_RES_TAC WEAK_EQUIV_EPS \\
-      Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] \\
-      MATCH_MP_TAC EPS_WEAK_EPS \\
-      take [`E2'`, `E2''`] >> ASM_REWRITE_TAC [] ]);
-
 val OBS_CONGR_WEAK_TRANS' = store_thm ((* NEW *)
    "OBS_CONGR_WEAK_TRANS'",
   ``!E E'. OBS_CONGR E E' ==>

examples/arm/armv8-memory-model/relation_extraScript.sml

@@ -157,27 +157,6 @@ Proof
   xsimp []
 QED
 
-Theorem dom_dom:
-  r = diag r1 ⨾ r ⨾ diag r2 ==> !x y. r x y ==> r1 x /\ r2 y
-Proof
-  xsimp []
-  \\ metis_tac []
-QED
-
-Theorem dom_l:
-  r = diag r1 ⨾ r ⨾ diag r2 ==> r = diag r1 ⨾ r
-Proof
-  xsimp []
-  \\ metis_tac []
-QED
-
-Theorem dom_r:
-  r = diag r1 ⨾ r ⨾ diag r2 ==> r = r ⨾ diag r2
-Proof
-  xsimp []
-  \\ metis_tac []
-QED
-
 (* - seq ------------------------------------------------------------------- *)
 
 Theorem seq_assoc:
@@ -206,20 +185,6 @@ Proof
   xsimp []
 QED
 
-Theorem seq_runion_l:
-  r1 ⨾ (r2 RUNION r3) = r1 ⨾ r2 RUNION r1 ⨾ r3
-Proof
-  xsimp []
-  \\ metis_tac []
-QED
-
-Theorem seq_runion_r:
-  (r1 RUNION r2) ⨾ r3 = r1 ⨾ r3 RUNION r2 ⨾ r3
-Proof
-  xsimp []
-  \\ metis_tac []
-QED
-
 Theorem irreflexive_seq:
   irreflexive (r1 ⨾ r2) = irreflexive (r2 ⨾ r1)
 Proof

examples/arm/v7/arm_stepScript.sml

@@ -3110,9 +3110,9 @@ val ARM_WRITE_REG_MODE = save_thm("ARM_WRITE_REG_MODE",
   SIMP_RULE (srw_ss()) [ARM_WRITE_REG_FROM_MODE]
     (arm_reg_rule ARM_WRITE_REG_MODE_def));
 
-val ARM_WRITE_REG_o = save_thm("ARM_WRITE_REG_o",
+Theorem ARM_WRITE_REG_o[allow_rebind] =
   SIMP_RULE (srw_ss()) [ARM_WRITE_REG_FROM_MODE]
-    (arm_reg_rule ARM_WRITE_REG_o));
+            (arm_reg_rule ARM_WRITE_REG_o);
 
 (* ------------------------------------------------------------------------- *)
 

examples/dependability/AvailabilityScript.sml

@@ -1181,7 +1181,7 @@ RW_TAC std_ss[]
 QED
 
 (*-------------------*)
-Theorem lim_inst_OR_tend_steady :
+Theorem lim_inst_OR_tend_steady0 :
 !p L M. prob_space p /\
             (!z. MEM z M ==> (0 < FST z /\ 0 < SND z)) /\
             (LENGTH L = LENGTH M) /\
@@ -1289,7 +1289,7 @@ RW_TAC std_ss[]
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_SUB
    >> RW_TAC std_ss[SEQ_CONST]
-   >> MATCH_MP_TAC lim_inst_OR_tend_steady
+   >> MATCH_MP_TAC lim_inst_OR_tend_steady0
    >> RW_TAC std_ss[])
 >> (`(\t.
    1 −
@@ -1303,7 +1303,7 @@ RW_TAC std_ss[]
    >> POP_ORW
    >> MATCH_MP_TAC SEQ_SUB
    >> RW_TAC std_ss[SEQ_CONST]
->> MATCH_MP_TAC lim_inst_OR_tend_steady
+>> MATCH_MP_TAC lim_inst_OR_tend_steady0
 >> RW_TAC std_ss[]
 QED
 (*------------------------------------*)
@@ -1342,9 +1342,9 @@ RW_TAC std_ss[NOR_unavail_FT_gate_def]
          (one_minus_list (list_prob p (union_unavail_event_list p L (&t)))))``)
 >> RW_TAC std_ss[GSYM SEQ_LIM,convergent]
 >- (EXISTS_TAC (``list_prod (one_minus_list (steady_state_unavail_list M))``)
-   >> MATCH_MP_TAC lim_inst_OR_tend_steady
+   >> MATCH_MP_TAC lim_inst_OR_tend_steady0
    >> RW_TAC std_ss[])
->> MATCH_MP_TAC lim_inst_OR_tend_steady
+>> MATCH_MP_TAC lim_inst_OR_tend_steady0
 >> RW_TAC std_ss[]
 QED
 (*------------------------*)

examples/dependability/FT/FT_deepScript.sml

@@ -1174,75 +1174,7 @@ Induct_on `n`
 >> RW_TAC arith_ss [binomial_def]
 >> RW_TAC arith_ss [binomial_def]
 QED
-(* --------------------------------------------------- *)
-(*      BINOMIAL_FACT                                  *)
-(* --------------------------------------------------- *)
-Theorem BINOMIAL_FACT :
-!a b. binomial (a+b) b * (FACT a * FACT b) = FACT (a+b)
-Proof
-Induct_on `b`
- >- (REWRITE_TAC[BINOMIAL_DEF1,FACT,ADD_CLAUSES,MULT_CLAUSES])
->> Induct_on `a`
->- (REWRITE_TAC[BINOMIAL_DEF3,FACT,ADD_CLAUSES,MULT_CLAUSES])
->> `SUC a + SUC b = SUC (SUC a + b)` by RW_TAC arith_ss [ADD_CLAUSES]
->> ASM_REWRITE_TAC[BINOMIAL_DEF4,RIGHT_ADD_DISTRIB]
->> POP_ORW
->> `binomial (SUC a + b) (SUC b) * (FACT (SUC a) * FACT (SUC b)) =
-                   (binomial (a + SUC b) (SUC b) * (FACT a * FACT (SUC b))) * SUC a`
-by REWRITE_TAC[FACT,ADD_CLAUSES]
->- (PROVE_TAC[MULT_ASSOC,MULT_SYM])
->> ASM_REWRITE_TAC[]
->> POP_ORW
->> `binomial (SUC a + b) b * (FACT (SUC a) * FACT (SUC b)) =
-                       (binomial (SUC a + b) b * (FACT (SUC a) * FACT b)) * SUC b`
-by REWRITE_TAC[FACT,ADD_CLAUSES]
->- (PROVE_TAC[MULT_ASSOC,MULT_SYM])
->> ASM_REWRITE_TAC [ADD_CLAUSES, FACT]
->> REWRITE_TAC[GSYM LEFT_ADD_DISTRIB]
->> `SUC a + SUC b = SUC (SUC (a + b))` by RW_TAC arith_ss [ADD_CLAUSES]
->> ASM_REWRITE_TAC[]
->> RW_TAC arith_ss []
-QED
-(* -----------------BINOMIAL_DEF2--------------------------- *)
-Theorem BINOMIAL_DEF2 :
-!n k. n < k ==> (binomial n k = 0)
-Proof
-Induct_on `n`
->- (Cases_on `k`
-   >- (RW_TAC real_ss [])
-   >> REWRITE_TAC [binomial_def])
->> Cases_on `k`
->- (RW_TAC real_ss [])
->> RW_TAC arith_ss [binomial_def]
-QED
-(* -----------------BINOMIAL_DEF3--------------------------- *)
-Theorem BINOMIAL_DEF3 :
-!n. (binomial n n = 1)
-Proof
-Induct_on `n` THEN REWRITE_TAC [binomial_def] THEN RW_TAC arith_ss [BINOMIAL_DEF2]
-QED
-(* -----------------BINOMIAL_DEF4--------------------------- *)
-Theorem BINOMIAL_DEF4 :
-!n k. (binomial (SUC n) (SUC k) = binomial n (SUC k) + binomial n k)
-Proof
-REWRITE_TAC [binomial_def]
-QED
-(* -----------------BINOMIAL_DEF6--------------------------- *)
-Theorem BINOMIAL_DEF6 :
-!n. (binomial (SUC n) 1 = SUC n)
-Proof
-RW_TAC std_ss []
->> ONCE_REWRITE_TAC[ONE]
->> (MP_TAC o Q.SPECL [`n`,`SUC 0`]) BINOMIAL_FACT
->> ONCE_REWRITE_TAC[FACT]
->> ONCE_REWRITE_TAC[GSYM ONE]
->> ONCE_REWRITE_TAC[ADD_COMM]
->> ONCE_REWRITE_TAC[GSYM SUC_ONE_ADD]
->> ONCE_REWRITE_TAC[FACT]
->> STRIP_TAC
->> FULL_SIMP_TAC real_ss [EQ_MULT_LCANCEL]
->> METIS_TAC [FACT_LESS, NOT_ZERO_LT_ZERO]
-QED
+
 (* --------------------------------------------------------- *)
 (*      EXP_PASCAL_REAL                                      *)
 (* --------------------------------------------------------- *)

examples/dependability/RBD/RBDScript.sml

@@ -1236,7 +1236,7 @@ RW_TAC std_ss[mutual_indep_def]
 >> FULL_SIMP_TAC std_ss[]
 QED
 (*------------mutual_indep_flat_cons3-----------------*)
-Theorem mutual_indep_flat_cons3 :
+Theorem mutual_indep_flat_cons3_0 :
 !L L1 L2 p.  mutual_indep p (FLAT (L1::L2::L)) ==>  mutual_indep p ((L1))
 Proof
 RW_TAC std_ss[mutual_indep_def]
@@ -1265,7 +1265,7 @@ QED
 
 (*-------mutual_indep_flat_cons3---*)
 Theorem mutual_indep_flat_cons3 :
-!L1 h L p.  mutual_indep p (FLAT (L1::h::L)) ==> mutual_indep p (FLAT (L1::L))
+  !L1 h L p. mutual_indep p (FLAT (L1::h::L)) ==> mutual_indep p (FLAT (L1::L))
 Proof
 RW_TAC std_ss[mutual_indep_def]
 >> NTAC 3 (POP_ASSUM MP_TAC)

examples/fun-op-sem/for/forScript.sml

@@ -215,11 +215,12 @@ val sem_t_def_with_stop = store_thm ("sem_t_def_with_stop",
  fs [] >>
  `F` by decide_tac);
 
-Theorem sem_t_def[compute] = REWRITE_RULE [STOP_def] sem_t_def_with_stop;
+Theorem sem_t_def[compute,allow_rebind] =
+  REWRITE_RULE [STOP_def] sem_t_def_with_stop;
 
 (* We also remove the redundant checks from the induction theorem. *)
 
-val sem_t_ind = store_thm("sem_t_ind",
+val sem_t_ind = store_thm("sem_t_ind[allow_rebind]",
   fetch "-" "sem_t_ind"
     |> concl |> term_rewrite [``check_clock s3 s = s3``,
     ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``],
@@ -1449,11 +1450,11 @@ val _ = Parse.add_infix("DOWNARROWt",450,Parse.NONASSOC)
 val DOWNARROWe_def = Define `$DOWNARROWe (y,x) z = sem_e_reln x y z`;
 val DOWNARROWt_def = Define `$DOWNARROWt (y,x) z = simple_sem_t_reln x y z`;
 
-val simple_sem_t_reln_rules = save_thm("simple_sem_t_reln_rules",
-  simple_sem_t_reln_rules |> REWRITE_RULE [GSYM DOWNARROWe_def,
-                                           GSYM DOWNARROWt_def]);
+Theorem simple_sem_t_reln_rules[allow_rebind] =
+  simple_sem_t_reln_rules
+    |> REWRITE_RULE [GSYM DOWNARROWe_def, GSYM DOWNARROWt_def];
 
-val simple_sem_t_reln_ind = save_thm("simple_sem_t_reln_ind",
+Theorem simple_sem_t_reln_ind[allow_rebind] =
   simple_sem_t_reln_ind
     |> REWRITE_RULE [GSYM DOWNARROWe_def, GSYM DOWNARROWt_def]
     |> Q.SPEC `P` |> UNDISCH_ALL
@@ -1478,7 +1479,7 @@ val simple_sem_t_reln_ind = save_thm("simple_sem_t_reln_ind",
     |> SIMP_RULE std_ss []
     |> DISCH_ALL
     |> Q.GEN `P`
-    |> REWRITE_RULE [GSYM CONJ_ASSOC]);
+    |> REWRITE_RULE [GSYM CONJ_ASSOC];
 
 val lemma = prove(
   ``b1 \/ b2 \/ b3 \/ b4 \/ b5 \/ b6 <=>

examples/fun-op-sem/for/for_nd_semScript.sml

@@ -231,15 +231,15 @@ val sem_t_def_with_stop = store_thm ("sem_t_def_with_stop",
  imp_res_tac sem_e_clock >>
  fs [] >> `F` by decide_tac);
 
-val sem_t_def =
-  save_thm("sem_t_def",REWRITE_RULE [STOP_def] sem_t_def_with_stop);
+Theorem sem_t_def[allow_rebind] = REWRITE_RULE [STOP_def] sem_t_def_with_stop
 
 (* We also remove the redundant checks from the induction theorem. *)
 
-val sem_t_ind = store_thm ("sem_t_ind",
-  fetch "-" "sem_t_ind"
-    |> concl |> term_rewrite [``check_clock s3 s = s3``,
-    ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``],
+Theorem sem_t_ind[allow_rebind]:
+  ^(fetch "-" "sem_t_ind"
+    |> concl |> term_rewrite [“check_clock s3 s = s3”,
+    “s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0”])
+Proof
  ntac 2 strip_tac >>
  ho_match_mp_tac (fetch "-" "sem_t_ind") >> rw [] >>
  first_x_assum match_mp_tac >>
@@ -248,7 +248,8 @@ val sem_t_ind = store_thm ("sem_t_ind",
  imp_res_tac sem_e_clock >>
  fs [dec_clock_def, check_clock_id, LET_THM] >>
  first_x_assum match_mp_tac >>
- decide_tac);
+ decide_tac
+QED
 
 (* The top-level semantics defines what is externally observable. *)
 

examples/hardware/port-full/tamarack2/tamarackScript.sml

@@ -869,7 +869,8 @@ ASM_SIMP_TAC std_ss [NextState_def, LET_DEF, Inst_def, Opc_def,
 (* - Proofs 3                - *)
 (* --------------------------- *)
 
-val MicroCycles_def = Define ‘MicroCycles n (mem,pc,acc) =
+Definition MicroCycles_def[allow_rebind]:
+  MicroCycles n (mem,pc,acc) =
   let opc = Opc n (Inst n (mem,pc)) in
   (if (opc = 0) then (if (acc = 0) then 5 else 6) else
    if (opc = 1) then 4 else
@@ -878,13 +879,15 @@ val MicroCycles_def = Define ‘MicroCycles n (mem,pc,acc) =
    if (opc = 4) then 6 else
    if (opc = 5) then 6 else
    if (opc = 6) then 6 else
-                     5)’;
+                     5)
+End
 
-val TimeOfCycle_def = Define ‘
+Definition TimeOfCycle_def[allow_rebind]:
   (TimeOfCycle n (mem,pc,acc) 0 = 0) /\
   (TimeOfCycle n (mem,pc,acc) (SUC t) =
      let prev = TimeOfCycle n (mem, pc, acc) t in
-     (prev + (MicroCycles n (mem prev,pc prev,acc prev))))’;
+     (prev + (MicroCycles n (mem prev,pc prev,acc prev))))
+End
 
 
 Theorem EVERY_INST_THM: