--- a/src/HOL/UNITY/Channel.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Channel.ML Wed Sep 01 11:16:02 1999 +0200
@@ -20,8 +20,7 @@
Addsimps [minSet_empty];
Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)";
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
+by Auto_tac;
qed_spec_mp "minSet_nonempty";
Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))";
@@ -53,6 +52,6 @@
by (rtac (lemma RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (forward_tac [minSet_nonempty] 1);
-by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
-by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
+by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least],
+ simpset()));
qed "Channel_progress";
--- a/src/HOL/UNITY/Constrains.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML Wed Sep 01 11:16:02 1999 +0200
@@ -43,7 +43,8 @@
(*** Co ***)
-overload_1st_set "Constrains.op Co";
+(*Needed because its operands are sets*)
+overload_1st_set "Constrains.Constrains";
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
bind_thm ("constrains_reachable_Int",
@@ -341,11 +342,18 @@
(*proves "co" properties when the program is specified*)
fun constrains_tac i =
SELECT_GOAL
- (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1,
- REPEAT (resolve_tac [StableI, stableI,
+ (EVERY [REPEAT (Always_Int_tac 1),
+ REPEAT (etac Always_ConstrainsI 1
+ ORELSE
+ resolve_tac [StableI, stableI,
constrains_imp_Constrains] 1),
rtac constrainsI 1,
- Full_simp_tac 1,
+ full_simp_tac (simpset() addsimps !program_defs_ref) 1,
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS Clarify_tac,
ALLGOALS Asm_full_simp_tac]) i;
+
+
+(*For proving invariants*)
+fun always_tac i =
+ rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
--- a/src/HOL/UNITY/Handshake.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML Wed Sep 01 11:16:02 1999 +0200
@@ -30,14 +30,12 @@
by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac "cmdG" 2);
by (constrains_tac 1);
-by Auto_tac;
qed "lemma2_1";
Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac 2);
by (ensures_tac "cmdF" 1);
-by Auto_tac;
qed "lemma2_2";
@@ -45,11 +43,8 @@
by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
GreaterThan_bounded_induct 1);
-by (auto_tac (claset(), simpset() addsimps [vimage_def]));
-(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
-by (rtac LeadsTo_Diff 1);
-by (rtac lemma2_2 2);
-by (rtac LeadsTo_Trans 1);
-by (rtac lemma2_2 2);
-by (rtac lemma2_1 1);
+(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+by (auto_tac (claset() addSIs [lemma2_1, lemma2_2]
+ addIs[LeadsTo_Trans, LeadsTo_Diff],
+ simpset() addsimps [vimage_def]));
qed "progress";
--- a/src/HOL/UNITY/Lift.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML Wed Sep 01 11:16:02 1999 +0200
@@ -47,14 +47,9 @@
req_up_def, req_down_def, move_up_def, move_down_def,
button_press_def]);
-val always_defs = [above_def, below_def, queueing_def,
- goingup_def, goingdown_def, ready_def];
-
-Addsimps (map simp_of_set always_defs);
-
-
-val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
+(*The ALWAYS properties*)
+Addsimps (map simp_of_set [above_def, below_def, queueing_def,
+ goingup_def, goingdown_def, ready_def]);
Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
@@ -64,47 +59,33 @@
Goal "Lift : Always open_stop";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
+by (always_tac 1);
qed "open_stop";
Goal "Lift : Always stop_floor";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
+by (always_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
Goal "Lift : Always open_move";
-by (rtac AlwaysI 1);
-by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2);
-by (Force_tac 1);
-by (constrains_tac 1);
+by (cut_facts_tac [open_stop] 1);
+by (always_tac 1);
qed "open_move";
Goal "Lift : Always moving_up";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
-by (auto_tac (claset(),
+by (always_tac 1);
+by (auto_tac (claset() addDs [zle_imp_zless_or_eq],
simpset() addsimps [add1_zle_eq]));
-by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_up";
Goal "Lift : Always moving_down";
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
+by (always_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_down";
Goal "Lift : Always bounded";
-by (rtac AlwaysI 1);
-by (rtac (Always_Int_rule [moving_up, moving_down] RS
- Always_ConstrainsI RS StableI) 2);
-by (Force_tac 1);
-by (constrains_tac 1);
+by (cut_facts_tac [moving_up, moving_down] 1);
+by (always_tac 1);
by (ALLGOALS Clarify_tac);
by (REPEAT_FIRST distinct_tac);
by Auto_tac;
@@ -170,8 +151,8 @@
Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \
\ LeadsTo ((closed Int goingup Int Req n) Un \
\ (closed Int goingdown Int Req n))";
-by (rtac subset_imp_LeadsTo 1);
-by (auto_tac (claset() addSEs [int_neqE], simpset()));
+by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE],
+ simpset()));
qed "E_thm05c";
(*lift_2*)
@@ -198,15 +179,12 @@
by Safe_tac;
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
by (etac (linorder_leI RS order_antisym RS sym) 1);
-by (REPEAT_FIRST (eresolve_tac mov_metrics));
-by (REPEAT_FIRST distinct_tac);
+by (REPEAT_FIRST (eresolve_tac mov_metrics ORELSE' distinct_tac));
(** LEVEL 6 **)
-by (ALLGOALS (asm_simp_tac (simpset() addsimps
- [zle_def] @ metric_simps @ zcompare_rls)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
qed "E_thm12a";
-
(*lem_lift_4_3 *)
Goal "#0 < N ==> \
\ Lift : (moving Int Req n Int {s. metric n s = N} Int \
@@ -217,8 +195,7 @@
by Safe_tac;
(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
by (etac (linorder_leI RS order_antisym RS sym) 1);
-by (REPEAT_FIRST (eresolve_tac mov_metrics));
-by (REPEAT_FIRST distinct_tac);
+by (REPEAT_FIRST (eresolve_tac mov_metrics ORELSE' distinct_tac));
(** LEVEL 6 **)
by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls)));
qed "E_thm12b";
@@ -227,10 +204,9 @@
Goal "#0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
\ {s. floor s ~: req s}) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
-by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
-by (etac E_thm12b 3);
-by (etac E_thm12a 2);
-by (Blast_tac 1);
+by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
+by Auto_tac;
qed "lift_4";
@@ -278,11 +254,10 @@
(*lift_5*)
Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \
\ (moving Int Req n Int {s. metric n s < N})";
-by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
-by (etac E_thm16b 3);
-by (etac E_thm16a 2);
+by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
by (dtac E_thm16c 1);
-by (Blast_tac 1);
+by Auto_tac;
qed "lift_5";
@@ -357,35 +332,33 @@
by (rtac (Always_nonneg RS integ_0_le_induct) 1);
by (case_tac "#0 < z" 1);
(*If z <= #0 then actually z = #0*)
-by (fold_tac [zle_def]);
-by (force_tac (claset() addIs [R_thm11, order_antisym], simpset()) 2);
+by (force_tac (claset() addIs [R_thm11, order_antisym],
+ simpset() addsimps [linorder_not_less]) 2);
by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
-by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1);
-by (rtac lift_3_Req 3);
-by (rtac lift_4 2);
+by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
by Auto_tac;
qed "lift_3";
+val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
+(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
+
Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
by (rtac LeadsTo_Trans 1);
-by (rtac (E_thm04 RS LeadsTo_Un) 2);
-by (rtac LeadsTo_Un_post 2);
+by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2);
by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
-by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
-by (rtac E_thm02 2);
+by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2);
by (rtac (open_move RS Always_LeadsToI) 1);
-by (rtac (open_stop RS Always_LeadsToI) 1);
-by (rtac subset_imp_LeadsTo 1);
+by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1);
by (Clarify_tac 1);
(*The case split is not essential but makes Blast_tac much faster.
- Must also be careful to prevent simplification from looping*)
+ Calling rotate_tac prevents simplification from looping*)
by (case_tac "open x" 1);
by (ALLGOALS (rotate_tac ~1));
-by (ALLGOALS Asm_full_simp_tac);
-by (Blast_tac 1);
+by Auto_tac;
qed "lift_1";
Close_locale "floor";
--- a/src/HOL/UNITY/Mutex.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML Wed Sep 01 11:16:02 1999 +0200
@@ -17,15 +17,11 @@
Goal "Mutex : Always IU";
-by (rtac AlwaysI 1);
-by (constrains_tac 2);
-by Auto_tac;
+by (always_tac 1);
qed "IU";
Goal "Mutex : Always IV";
-by (rtac AlwaysI 1);
-by (constrains_tac 2);
-by Auto_tac;
+by (always_tac 1);
qed "IV";
(*The safety property: mutual exclusion*)
@@ -38,8 +34,7 @@
(*The bad invariant FAILS in V1*)
Goal "Mutex : Always bad_IU";
-by (rtac AlwaysI 1);
-by (constrains_tac 2);
+by (always_tac 1);
by Auto_tac;
(*Resulting state: n=1, p=false, m=4, u=false.
Execution of V1 (the command of process v guarded by n=1) sets p:=true,
--- a/src/HOL/UNITY/Reach.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Reach.ML Wed Sep 01 11:16:02 1999 +0200
@@ -30,9 +30,7 @@
Addsimps [simp_of_set reach_invariant_def];
Goal "Rprg : Always reach_invariant";
-by (rtac AlwaysI 1);
-by Auto_tac; (*for the initial state; proof of stability remains*)
-by (constrains_tac 1);
+by (always_tac 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
qed "reach_invariant";
--- a/src/HOL/UNITY/Token.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/Token.ML Wed Sep 01 11:16:02 1999 +0200
@@ -71,8 +71,7 @@
by (case_tac "i=j" 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
by (rtac (TR7 RS leadsTo_weaken_R) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
qed "TR7_nodeOrder";
@@ -80,8 +79,7 @@
Goal "[| i<N; j<N; i~=j |] \
\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
by (rtac (TR7 RS leadsTo_weaken_R) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
qed "TR7_aux";
Goal "({s. token s < N} Int token -`` {m}) = \
@@ -100,15 +98,13 @@
by (Blast_tac 2);
by (Clarify_tac 1);
by (rtac (TR7_aux RS leadsTo_weaken) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
-by (ALLGOALS Blast_tac);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
qed "leadsTo_j";
(*Misra's TR8: a hungry process eventually eats*)
Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
by (rtac TR6 2);
-by (rtac leadsTo_weaken 1);
-by (rtac ([leadsTo_j, TR3] MRS psp) 1);
+by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
by (ALLGOALS Blast_tac);
qed "token_progress";
--- a/src/HOL/UNITY/UNITY.ML Wed Sep 01 11:15:35 1999 +0200
+++ b/src/HOL/UNITY/UNITY.ML Wed Sep 01 11:16:02 1999 +0200
@@ -112,7 +112,9 @@
(*** co ***)
-overload_1st_set "UNITY.op co";
+(*These operators are not overloaded, but their operands are sets, and
+ ultimately there's a risk of reaching equality, which IS overloaded*)
+overload_1st_set "UNITY.constrains";
overload_1st_set "UNITY.stable";
overload_1st_set "UNITY.unless";