From 326d0b091271480638fb978fa2a0960606b5d692 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Sat, 9 Sep 2023 11:07:07 +1000 Subject: [PATCH] Fix more duplicated rewrites after breakage caused by 705d331db97 --- examples/CCS/ObsCongrScript.sml | 41 ----------- .../relation_extraScript.sml | 35 ---------- examples/arm/v7/arm_stepScript.sml | 4 +- examples/dependability/AvailabilityScript.sml | 10 +-- examples/dependability/FT/FT_deepScript.sml | 70 +------------------ examples/dependability/RBD/RBDScript.sml | 4 +- examples/fun-op-sem/for/forScript.sml | 15 ++-- examples/fun-op-sem/for/for_nd_semScript.sml | 15 ++-- .../port-full/tamarack2/tamarackScript.sml | 11 +-- .../barendregt/finite_developmentsScript.sml | 63 ++++++++--------- .../barendregt/standardisationScript.sml | 26 ------- examples/lambda/basics/termScript.sml | 45 ++++++------ .../lambda/other-models/MPlambdaScript.sml | 11 +-- examples/lambda/other-models/dBScript.sml | 17 ++--- examples/lambda/other-models/ncScript.sml | 8 ++- src/quotient/examples/sigma/liftScript.sml | 16 ++--- .../examples/sigma/semanticsScript.sml | 12 ++-- 17 files changed, 114 insertions(+), 289 deletions(-) diff --git a/examples/CCS/ObsCongrScript.sml b/examples/CCS/ObsCongrScript.sml index 67fa260b8b..51436ce5a6 100644 --- a/examples/CCS/ObsCongrScript.sml +++ b/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' ==> diff --git a/examples/arm/armv8-memory-model/relation_extraScript.sml b/examples/arm/armv8-memory-model/relation_extraScript.sml index 30a8151c28..69cb784bdb 100644 --- a/examples/arm/armv8-memory-model/relation_extraScript.sml +++ b/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 diff --git a/examples/arm/v7/arm_stepScript.sml b/examples/arm/v7/arm_stepScript.sml index 95da379c50..ed162561aa 100644 --- a/examples/arm/v7/arm_stepScript.sml +++ b/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); (* ------------------------------------------------------------------------- *) diff --git a/examples/dependability/AvailabilityScript.sml b/examples/dependability/AvailabilityScript.sml index 75c1404595..3e4db2a205 100644 --- a/examples/dependability/AvailabilityScript.sml +++ b/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 (*------------------------*) diff --git a/examples/dependability/FT/FT_deepScript.sml b/examples/dependability/FT/FT_deepScript.sml index 36f845f44a..a1c52f7e80 100644 --- a/examples/dependability/FT/FT_deepScript.sml +++ b/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 *) (* --------------------------------------------------------- *) diff --git a/examples/dependability/RBD/RBDScript.sml b/examples/dependability/RBD/RBDScript.sml index 21127db75a..e21770cf6e 100644 --- a/examples/dependability/RBD/RBDScript.sml +++ b/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) diff --git a/examples/fun-op-sem/for/forScript.sml b/examples/fun-op-sem/for/forScript.sml index fdfcc2fb46..48a8ef4170 100644 --- a/examples/fun-op-sem/for/forScript.sml +++ b/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 <=> diff --git a/examples/fun-op-sem/for/for_nd_semScript.sml b/examples/fun-op-sem/for/for_nd_semScript.sml index a1d7c52ccb..afc6061dfd 100644 --- a/examples/fun-op-sem/for/for_nd_semScript.sml +++ b/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. *) diff --git a/examples/hardware/port-full/tamarack2/tamarackScript.sml b/examples/hardware/port-full/tamarack2/tamarackScript.sml index 36780b5e43..dd3ca121cf 100644 --- a/examples/hardware/port-full/tamarack2/tamarackScript.sml +++ b/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: diff --git a/examples/lambda/barendregt/finite_developmentsScript.sml b/examples/lambda/barendregt/finite_developmentsScript.sml index 52c9033f31..79e2dc1848 100644 --- a/examples/lambda/barendregt/finite_developmentsScript.sml +++ b/examples/lambda/barendregt/finite_developmentsScript.sml @@ -477,12 +477,13 @@ val lift_path_exists = prove( val lift_path_def = new_specification ( "lift_path_def", ["lift_path"], lift_path_exists); -val first_lift_path = store_thm( - "first_lift_path", - ``!M' p. first (lift_path M' p) = M'``, +Theorem first_lift_path: + !M p. first (lift_path M p) = M +Proof REPEAT GEN_TAC THEN Q.ISPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN - SRW_TAC [][lift_path_def]); + SRW_TAC [][lift_path_def] +QED val strip_path_label_lift_path = store_thm( "strip_path_label_lift_path", @@ -1674,11 +1675,6 @@ val term_development_thm = store_thm( ``sigma IN development M <=> sigma IN development M (redex_posns M)``, SRW_TAC [][SPECIFICATION, term_development_def]); -val first_lift_path = store_thm( - "first_lift_path", - ``!p M. first (lift_path M p) = M``, - SIMP_TAC (srw_ss()) [Once FORALL_path, lift_path_def]); - val lrcc_RUNION = store_thm( "lrcc_RUNION", ``!R M r N. lrcc R M r N ==> lrcc (R RUNION R') M r N``, @@ -1865,28 +1861,29 @@ val (update_weighing_def, update_weighing_swap) = \rp w p. update_weighing t (TL rp) (\p. w (In::p)) (TL p)) `; -val update_weighing_thm = store_thm( - "update_weighing_thm", - ``(update_weighing (t @@ u) [] w = - let vps = IMAGE TL (bv_posns t) - in - \p. if ?vp l. vp IN vps /\ (APPEND vp l = p) then - w (Rt :: @l. ?vp. vp IN vps /\ (APPEND vp l = p)) - else - w (Lt::In::p)) /\ - (update_weighing (LAM v t) (In::pos0) w = - let w0 = update_weighing t pos0 (\p. w (In::p)) - in - \p. w0 (TL p)) /\ - (update_weighing (t @@ u) (Lt::pos0) w = - let w0 = update_weighing t pos0 (\p. w (Lt::p)) - in - \p. if HD p = Lt then w0 (TL p) else w p) /\ - (update_weighing (t @@ u) (Rt::pos0) w = - let w0 = update_weighing u pos0 (\p. w (Rt::p)) - in - \p. if HD p = Rt then w0 (TL p) else w p)``, - SRW_TAC [][update_weighing_def]); +Theorem update_weighing_thm[allow_rebind]: + (update_weighing (t @@ u) [] w = + let vps = IMAGE TL (bv_posns t) + in + \p. if ?vp l. vp IN vps /\ (APPEND vp l = p) then + w (Rt :: @l. ?vp. vp IN vps /\ (APPEND vp l = p)) + else + w (Lt::In::p)) /\ + (update_weighing (LAM v t) (In::pos0) w = + let w0 = update_weighing t pos0 (\p. w (In::p)) + in + \p. w0 (TL p)) /\ + (update_weighing (t @@ u) (Lt::pos0) w = + let w0 = update_weighing t pos0 (\p. w (Lt::p)) + in + \p. if HD p = Lt then w0 (TL p) else w p) /\ + (update_weighing (t @@ u) (Rt::pos0) w = + let w0 = update_weighing u pos0 (\p. w (Rt::p)) + in + \p. if HD p = Rt then w0 (TL p) else w p) +Proof + SRW_TAC [][update_weighing_def] +QED val update_weighing_vsubst = store_thm( "update_weighing_vsubst", @@ -1904,10 +1901,6 @@ val beta0_redex_posn = store_thm( SIMP_TAC (srw_ss() ++ DNF_ss) [redex_posns_thm, strip_label_thm, beta0_def]); -val nonzero_def = Define` - nonzero (t:lterm) w = !p. p IN lvar_posns t ==> 0 < w p -`; - val term_weight_def = Define` term_weight (t:term) w = SUM_IMAGE w (var_posns t) `; diff --git a/examples/lambda/barendregt/standardisationScript.sml b/examples/lambda/barendregt/standardisationScript.sml index dcc159b106..a83415ef0c 100644 --- a/examples/lambda/barendregt/standardisationScript.sml +++ b/examples/lambda/barendregt/standardisationScript.sml @@ -1016,32 +1016,6 @@ val i1_reduces_i_reduces = prove( ``M i1_reduces N ==> M i_reduces N``, SRW_TAC [][i1_reduces_def, i_reduces_def] THEN PROVE_TAC []); -val i_reduces_RTC_i_reduce1 = store_thm( - "i_reduces_RTC_i_reduce1", - ``(i_reduces) = RTC (i_reduce1)``, - SIMP_TAC (srw_ss()) [FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM, - FUN_EQ_THM, i_reduces_def, EQ_IMP_THM] THEN - CONJ_TAC THENL [ - Q_TAC SUFF_TAC - `!s. okpath (labelled_redn beta) s /\ finite s ==> - (!i. i + 1 IN PL s ==> nth_label i s is_internal_redex el i s) ==> - RTC (i_reduce1) (first s) (last s)` THEN1 PROVE_TAC [] THEN - HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN - SRW_TAC [][GSYM ADD1, relationTheory.RTC_RULES] THEN - MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES)) THEN - POP_ASSUM (fn th => - MAP_EVERY (MP_TAC o GEN_ALL o C SPEC th) - [``0``,``SUC i``]) THEN - SRW_TAC [][i_reduce1_def] THEN PROVE_TAC [], - HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN - SRW_TAC [][i_reduce1_def, GSYM ADD1] THENL [ - Q.EXISTS_TAC `stopped_at x` THEN SRW_TAC [][], - Q.EXISTS_TAC `pcons x r s` THEN - SRW_TAC [][] THEN Cases_on `i` THEN SRW_TAC [][] - ] - ]); - - val _ = augment_srw_ss [rewrites [REWRITE_CONV [EMPTY_SUBSET, redex_occurrences_SUBSET] ``{} SUBSET (M:term)``]] diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml index bced0ff417..6f74dc1818 100644 --- a/examples/lambda/basics/termScript.sml +++ b/examples/lambda/basics/termScript.sml @@ -297,11 +297,6 @@ val tm_recursion = save_thm( |> SIMP_RULE (srw_ss() ++ CONJ_ss) [supp_unitfn] |> Q.INST [`apu` |-> `ap`, `lmu` |-> `lm`, `vru` |-> `vr`]) -val tm_recursion_nosideset = save_thm( - "tm_recursion_nosideset", - tm_recursion |> Q.INST [`A` |-> `{}`] - |> REWRITE_RULE [NOT_IN_EMPTY, FINITE_EMPTY]); - val FV_tpm = Save_thm("FV_tpm", ``x ∈ FV (tpm p t)`` |> REWRITE_CONV [perm_supp,pmact_IN] @@ -310,14 +305,14 @@ val FV_tpm = Save_thm("FV_tpm", val _ = set_mapped_fixity { term_name = "APP", tok = "@@", fixity = Infixl 901} -val FRESH_APP = Store_thm( - "FRESH_APP", - ``v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N``, - SRW_TAC [][]); -val FRESH_LAM = Store_thm( - "FRESH_LAM", - ``u NOTIN FV (LAM v M) <=> (u <> v ==> u NOTIN FV M)``, - SRW_TAC [][] THEN METIS_TAC []); +Theorem FRESH_APP[simp]: v NOTIN FV (M @@ N) <=> v NOTIN FV M /\ v NOTIN FV N +Proof SRW_TAC [][] +QED + +Theorem FRESH_LAM[simp]: + u NOTIN FV (LAM v M) <=> (u <> v ==> u NOTIN FV M) +Proof SRW_TAC [][] THEN METIS_TAC [] +QED val FV_EMPTY = store_thm( "FV_EMPTY", ``(FV t = {}) <=> !v. v NOTIN FV t``, @@ -354,19 +349,21 @@ val term_CASES = store_thm( HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN METIS_TAC []); (* should derive automatically *) -val term_distinct = Store_thm( - "term_distinct", - ``VAR s ≠ APP t1 t2 ∧ VAR s ≠ LAM v t ∧ APP t1 t2 ≠ LAM v t``, +Theorem term_distinct[simp]: + VAR s ≠ APP t1 t2 ∧ VAR s ≠ LAM v t ∧ APP t1 t2 ≠ LAM v t +Proof srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP, - term_ABS_pseudo11, gterm_distinct, GLAM_eq_thm]); + term_ABS_pseudo11, gterm_distinct, GLAM_eq_thm] +QED -val term_11 = Store_thm( - "term_11", - ``((VAR s1 = VAR s2) <=> (s1 = s2)) ∧ - ((t11 @@ t12 = t21 @@ t22) <=> (t11 = t21) ∧ (t12 = t22)) ∧ - ((LAM v t1 = LAM v t2) <=> (t1 = t2))``, +Theorem term_11[simp]: + (VAR s1 = VAR s2 <=> s1 = s2) ∧ + (t11 @@ t12 = t21 @@ t22 <=> t11 = t21 ∧ t12 = t22) ∧ + (LAM v t1 = LAM v t2 <=> t1 = t2) +Proof srw_tac [][VAR_def, APP_def, LAM_def, LAM_termP, VAR_termP, APP_termP, - term_ABS_pseudo11, gterm_11, term_REP_11]); + term_ABS_pseudo11, gterm_11, term_REP_11] +QED (* "acyclicity" *) val APP_acyclic = store_thm( @@ -549,7 +546,7 @@ val size_exists = `lm` |-> `\m v t. m + 1`] |> SIMP_RULE (srw_ss()) [] -val size_def = new_specification("size_thm", ["size"], size_exists) +val size_def = new_specification("size_def", ["size"], size_exists) Theorem size_thm[simp] = CONJUNCT1 size_def Theorem size_tpm[simp] = GSYM (CONJUNCT2 size_def) diff --git a/examples/lambda/other-models/MPlambdaScript.sml b/examples/lambda/other-models/MPlambdaScript.sml index 1760c21051..220f05b1f8 100644 --- a/examples/lambda/other-models/MPlambdaScript.sml +++ b/examples/lambda/other-models/MPlambdaScript.sml @@ -50,10 +50,11 @@ val FINITE_allvars = Store_thm( ``!t. FINITE (allvars t)``, Induct THEN SRW_TAC [][]); -val vsub_14a = Store_thm( - "vsub_14a", - ``~(v IN allvars t) ==> (vsub N v t = t)``, - Induct_on `t` THEN SRW_TAC [][]); +Theorem vsub_14a_allvars[simp]: + v NOTIN allvars t ==> (vsub N v t = t) +Proof + Induct_on `t` THEN SRW_TAC [][] +QED val pvsub_vsub_collapse = store_thm( "pvsub_vsub_collapse", @@ -732,7 +733,7 @@ val vsub_vclosed = store_thm( "vsub_vclosed", ``!t. vclosed t ==> (vsub t' v t = t)``, REPEAT STRIP_TAC THEN IMP_RES_TAC vclosed_empty_vars THEN - SRW_TAC [][vsub_14a]); + SRW_TAC [][]); val general_vsub_commute = store_thm( "general_vsub_commute", diff --git a/examples/lambda/other-models/dBScript.sml b/examples/lambda/other-models/dBScript.sml index ba5f4dcbba..e9c5c6ef1e 100644 --- a/examples/lambda/other-models/dBScript.sml +++ b/examples/lambda/other-models/dBScript.sml @@ -174,14 +174,15 @@ RW_TAC std_ss [dFV, dLAMBDA, dFV_dLAMBDA_lemma]); (* Inductive definition of proper terms. *) (* --------------------------------------------------------------------- *) -val (dOK_DEF, dOK_ind, dOK_cases) = Hol_reln - `(!x. dOK (dVAR x)) /\ - (!x. dOK (dCON x)) /\ - (!x t. dOK t ==> dOK (dLAMBDA x t)) /\ - (!t u. dOK t /\ dOK u ==> dOK (dAPP t u))`; - -val _ = save_thm("dOK_DEF", dOK_DEF); -val _ = save_thm("dOK_ind", dOK_ind); +Inductive dOK: + (!x. dOK (dVAR x)) /\ + (!x. dOK (dCON x)) /\ + (!x t. dOK t ==> dOK (dLAMBDA x t)) /\ + (!t u. dOK t /\ dOK u ==> dOK (dAPP t u)) +End + +Theorem dOK_DEF = dOK_rules + (* --------------------------------------------------------------------- *) diff --git a/examples/lambda/other-models/ncScript.sml b/examples/lambda/other-models/ncScript.sml index dc2b889987..c7e042c1fc 100644 --- a/examples/lambda/other-models/ncScript.sml +++ b/examples/lambda/other-models/ncScript.sml @@ -837,11 +837,13 @@ val lemma14b = Q.store_thm( force an unnecessary case split. ---------------------------------------------------------------------- *) -val lemma14b = Q.store_thm("lemma14b", - `!t u x. ~(x IN FV u) ==> ([t/x]u = u)`, +Theorem lemma14b[allow_rebind]: + !t u x. ~(x IN FV u) ==> ([t/x]u = u) +Proof GEN_TAC THEN nc_INDUCT_TAC2 `FV t` THEN SRW_TAC [][SUB_THM, SUB_VAR] THEN SRW_TAC [][SUB_THM] THEN - Cases_on `x = y` THEN SRW_TAC [][SUB_THM]); + Cases_on `x = y` THEN SRW_TAC [][SUB_THM] +QED (* --------------------------------------------------------------------- *) (* The remaining Hindley and Seldin theorems. *) diff --git a/src/quotient/examples/sigma/liftScript.sml b/src/quotient/examples/sigma/liftScript.sml index 32126e0225..e0e4354109 100644 --- a/src/quotient/examples/sigma/liftScript.sml +++ b/src/quotient/examples/sigma/liftScript.sml @@ -1545,7 +1545,7 @@ val [HEIGHT, old_thms = old_thms}; -val _ = map save_thm +val _ = map (Feedback.trace ("Theory.allow_rebinds", 1) save_thm) [("HEIGHT",HEIGHT), ("HEIGHT_LESS_EQ_ZERO",HEIGHT_LESS_EQ_ZERO), ("FV_object",FV_object), (* AXIOM 1 of Gordon and Melham *) @@ -1626,12 +1626,12 @@ val method = ty_antiq( ==`:method`== ); (* Now test the lifted induction principle: *) -val HEIGHT_LESS_EQ_ZERO = store_thm - ("HEIGHT_LESS_EQ_ZERO", - “(!o'. (HEIGHT_obj o' <= 0) = (?x. o' = OVAR x)) /\ - (!d. (HEIGHT_dict d <= 0) = (d = NIL)) /\ - (!e. (HEIGHT_entry e <= 0) = F) /\ - (!m. (HEIGHT_method m <= 0) = F)”, +Theorem HEIGHT_LESS_EQ_ZERO[allow_rebind]: + (!o'. (HEIGHT_obj o' <= 0) = (?x. o' = OVAR x)) /\ + (!d. (HEIGHT_dict d <= 0) = (d = NIL)) /\ + (!e. (HEIGHT_entry e <= 0) = F) /\ + (!m. (HEIGHT_method m <= 0) = F) +Proof MUTUAL_INDUCT_THEN object_induct ASSUME_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[HEIGHT] @@ -1640,7 +1640,7 @@ val HEIGHT_LESS_EQ_ZERO = store_thm THEN REWRITE_TAC[object_one_one] THEN EXISTS_TAC “v:var” THEN REWRITE_TAC[] - ); +QED (* We will sometimes wish to induct on the height of an object. *) diff --git a/src/quotient/examples/sigma/semanticsScript.sml b/src/quotient/examples/sigma/semanticsScript.sml index f189b3b9b4..638a9f1be6 100644 --- a/src/quotient/examples/sigma/semanticsScript.sml +++ b/src/quotient/examples/sigma/semanticsScript.sml @@ -1,7 +1,4 @@ open HolKernel Parse boolLib; -infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; -infixr -->; - (* --------------------------------------------------------------------- *) (* Embedding the semantaics of objects as a foundational layer, *) @@ -171,10 +168,9 @@ val TC_DIAMOND = store_thm val invoke_method = invoke_method_def; -val FV_invoke_method = store_thm - ("FV_invoke_method", - “!m o'. FV_obj (invoke_method m o') SUBSET - (FV_method m UNION FV_obj o')”, +Theorem FV_invoke_method: + !m o'. FV_obj (invoke_method m o') SUBSET (FV_method m UNION FV_obj o') +Proof MUTUAL_INDUCT_THEN object_induct ASSUME_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[invoke_method] @@ -200,7 +196,7 @@ val FV_invoke_method = store_thm THEN DISCH_THEN REWRITE_THM THEN ASM_REWRITE_TAC[] ] - ); +QED val SUB_invoke_method = store_thm ("SUB_invoke_method",