--- a/src/HOL/UNITY/Channel.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML Thu Aug 06 15:47:26 1998 +0200
@@ -28,7 +28,7 @@
Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
by (rtac leadsTo_weaken 1);
-by (rtac ([UC2, UC1] MRS PSP) 1);
+by (rtac ([UC2, UC1] MRS psp) 1);
by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
by Safe_tac;
--- a/src/HOL/UNITY/Common.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Thu Aug 06 15:47:26 1998 +0200
@@ -71,8 +71,7 @@
Addsimps [atMost_Int_atLeast];
-Goal
- "[| ALL m. constrains acts {m} (maxfg m); \
+Goal "[| ALL m. constrains acts {m} (maxfg m); \
\ ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
\ n: common; id: acts |] \
\ ==> leadsTo acts (atMost n) common";
@@ -80,13 +79,12 @@
by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
by (ALLGOALS Asm_simp_tac);
by (rtac subset_refl 2);
-by (blast_tac (claset() addDs [PSP_stable2]
+by (blast_tac (claset() addDs [psp_stable2]
addIs [common_stable, leadsTo_weaken_R]) 1);
val lemma = result();
(*The "ALL m: Compl common" form echoes CMT6.*)
-Goal
- "[| ALL m. constrains acts {m} (maxfg m); \
+Goal "[| ALL m. constrains acts {m} (maxfg m); \
\ ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
\ n: common; id: acts |] \
\ ==> leadsTo acts (atMost (LEAST n. n: common)) common";
--- a/src/HOL/UNITY/Common.thy Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Common.thy Thu Aug 06 15:47:26 1998 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-Common = WFair +
+Common = WFair + Traces +
consts
ftime,gtime :: nat=>nat
--- a/src/HOL/UNITY/Handshake.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Thu Aug 06 15:47:26 1998 +0200
@@ -48,7 +48,7 @@
Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
br LeadsTo_weaken_R 1;
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
- R_greaterThan_bounded_induct 1);
+ GreaterThan_bounded_induct 1);
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
by (trans_tac 2);
(*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Lift.ML Thu Aug 06 15:47:26 1998 +0200
@@ -0,0 +1,142 @@
+(* Title: HOL/UNITY/Lift
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Lift-Control Example
+*)
+
+val always_defs = [above_def, below_def, queueing_def,
+ goingup_def, goingdown_def, ready_def];
+
+val cmd_defs = [Lprg_def,
+ request_act_def, open_act_def, close_act_def,
+ req_up_act_def, req_down_act_def, move_up_def, move_down_def];
+
+AddIffs [min_le_max];
+
+Goalw [Lprg_def] "id : Acts Lprg";
+by (Simp_tac 1);
+qed "id_in_Acts";
+AddIffs [id_in_Acts];
+
+
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
+
+(*Simplification for records*)
+Addsimps (thms"state.update_defs");
+
+Addsimps [Suc_le_eq];
+
+Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
+ moving_up_def, moving_down_def];
+
+
+Goal "0 < n ==> (m <= n-1) = (m<n)";
+by (exhaust_tac "n" 1);
+by Auto_tac;
+by (REPEAT_FIRST trans_tac);
+qed "le_pred_eq";
+
+Goal "m < n ==> m <= n-1";
+by (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq]) 1);
+qed "less_imp_le_pred";
+
+
+Goalw [Lprg_def] "invariant Lprg open_stop";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+qed "open_stop";
+
+Goalw [Lprg_def] "invariant Lprg stop_floor";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+qed "stop_floor";
+
+(*Should not have to prove open_stop concurrently!!*)
+Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+qed "open_move";
+
+Goalw [Lprg_def] "invariant Lprg moving_up";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
+qed "moving_up";
+
+Goalw [Lprg_def] "invariant Lprg moving_down";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
+by (auto_tac (claset(),
+ simpset() addsimps [gr_implies_gr0 RS le_pred_eq]));
+qed "moving_down";
+
+
+xxxxxxxxxxxxxxxx;
+
+Goalw [Lprg_def] "invariant Lprg bounded";
+by (rtac invariantI 1);
+by (Force_tac 1);
+by (constrains_tac (cmd_defs@always_defs) 1);
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps [gr_implies_gr0 RS le_pred_eq])));
+by (REPEAT_FIRST trans_tac);
+by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
+by (blast_tac (claset() addIs [diff_le_self, le_trans]) 1);
+by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
+qed "bounded";
+
+Goalw [Lprg_def] "invariant Lprg invariantV";
+by (rtac invariantI 1);
+by (constrains_tac cmd_defs 2);
+by Auto_tac;
+qed "invariantV";
+
+val invariantUV = invariant_Int_rule [invariantU, invariantV];
+
+
+(*The safety property: mutual exclusion*)
+Goal "(reachable Lprg) Int {s. MM s = 3 & NN s = 3} = {}";
+by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
+by Auto_tac;
+qed "mutual_exclusion";
+
+
+(*** Progress for U ***)
+
+Goalw [unless_def] "unless (Acts Lprg) {s. MM s=2} {s. MM s=3}";
+by (constrains_tac cmd_defs 1);
+qed "U_F0";
+
+Goal "LeadsTo Lprg {s. MM s=1} {s. PP s = VV s & MM s = 2}";
+by (ensures_tac cmd_defs "cmd1U" 1);
+qed "U_F1";
+
+Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
+by (cut_facts_tac [invariantUV] 1);
+bw Lprg_def;
+by (ensures_tac cmd_defs "cmd2U" 1);
+qed "U_F2";
+
+Goal "LeadsTo Lprg {s. MM s = 3} {s. PP s}";
+by (rtac leadsTo_imp_LeadsTo 1);
+by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
+by (ensures_tac cmd_defs "cmd4U" 2);
+by (ensures_tac cmd_defs "cmd3U" 1);
+qed "U_F3";
+
+Goal "LeadsTo Lprg {s. MM s = 2} {s. PP s}";
+by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+val U_lemma2 = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Lift.thy Thu Aug 06 15:47:26 1998 +0200
@@ -0,0 +1,127 @@
+(* Title: HOL/UNITY/Lift.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Lift-Control Example
+*)
+
+Lift = SubstAx +
+
+record state =
+ floor :: nat (*current position of the lift*)
+ open :: bool (*whether the door is open at floor*)
+ stop :: bool (*whether the lift is stopped at floor*)
+ req :: nat set (*for each floor, whether the lift is requested*)
+ up :: bool (*current direction of movement*)
+ move :: bool (*whether moving takes precedence over opening*)
+
+consts
+ min, max :: nat (*least and greatest floors*)
+
+rules
+ min_le_max "min <= max"
+
+
+constdefs
+
+ (** Abbreviations: the "always" part **)
+
+ above :: "state set"
+ "above == {s. EX i. floor s < i & i <= max & i : req s}"
+
+ below :: "state set"
+ "below == {s. EX i. min <= i & i < floor s & i : req s}"
+
+ queueing :: "state set"
+ "queueing == above Un below"
+
+ goingup :: "state set"
+ "goingup == above Int ({s. up s} Un Compl below)"
+
+ goingdown :: "state set"
+ "goingdown == below Int ({s. ~ up s} Un Compl above)"
+
+ ready :: "state set"
+ "ready == {s. stop s & ~ open s & move s}"
+
+
+ (** The program **)
+
+ request_act :: "(state*state) set"
+ "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
+ & ~ stop s & floor s : req s}"
+
+ open_act :: "(state*state) set"
+ "open_act ==
+ {(s,s'). s' = s (|open :=True,
+ req := req s - {floor s},
+ move := True|)
+ & stop s & ~ open s & floor s : req s
+ & ~(move s & s: queueing)}"
+
+ close_act :: "(state*state) set"
+ "close_act == {(s,s'). s' = s (|open := False|) & open s}"
+
+ req_up_act :: "(state*state) set"
+ "req_up_act ==
+ {(s,s'). s' = s (|stop :=False,
+ floor := Suc (floor s),
+ up := True|)
+ & s : (ready Int goingup)}"
+
+ req_down_act :: "(state*state) set"
+ "req_down_act ==
+ {(s,s'). s' = s (|stop :=False,
+ floor := floor s - 1,
+ up := False|)
+ & s : (ready Int goingdown)}"
+
+ move_up :: "(state*state) set"
+ "move_up ==
+ {(s,s'). s' = s (|floor := Suc (floor s)|)
+ & ~ stop s & up s & floor s ~: req s}"
+
+ move_down :: "(state*state) set"
+ "move_down ==
+ {(s,s'). s' = s (|floor := floor s - 1|)
+ & ~ stop s & ~ up s & floor s ~: req s}"
+
+ Lprg :: state program
+ "Lprg == (|Init = {s. floor s = min & ~ up s & move s & stop s &
+ ~ open s & req s = {}},
+ Acts = {id, request_act, open_act, close_act,
+ req_up_act, req_down_act, move_up, move_down}|)"
+
+
+ (** Invariants **)
+
+ bounded :: state set
+ "bounded == {s. min <= floor s & floor s <= max}"
+
+ (** ???
+ (~ stop s & up s --> floor s < max) &
+ (~ stop s & ~ up s --> min < floor s)}"
+ **)
+
+ open_stop :: state set
+ "open_stop == {s. open s --> stop s}"
+
+ open_move :: state set
+ "open_move == {s. open s --> move s}"
+
+ stop_floor :: state set
+ "stop_floor == {s. open s & ~ move s --> floor s : req s}"
+
+ moving_up :: state set
+ "moving_up == {s. ~ stop s & up s -->
+ (EX f. floor s <= f & f <= max & f : req s)}"
+
+ moving_down :: state set
+ "moving_down == {s. ~ stop s & ~ up s -->
+ (EX f. min <= f & f <= floor s & f : req s)}"
+
+ valid :: "state set"
+ "valid == bounded Int open_stop Int open_move"
+
+end
--- a/src/HOL/UNITY/Mutex.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Aug 06 15:47:26 1998 +0200
@@ -174,7 +174,7 @@
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
by (stac Un_commute 1);
by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
qed "m1_leadsto_3";
@@ -188,7 +188,7 @@
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
by (stac Un_commute 1);
by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
qed "n1_leadsto_3";
--- a/src/HOL/UNITY/SubstAx.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Aug 06 15:47:26 1998 +0200
@@ -3,39 +3,54 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Weak Fairness versions of transient, ensures, LeadsTo.
-
-From Misra, "A Logic for Concurrent Programming", 1994
+LeadsTo relation, restricted to the set of reachable states.
*)
-(*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
- (reachable(Init,Acts) Int B') *)
+
+(*constrains (Acts prg) B B'
+ ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
bind_thm ("constrains_reachable",
rewrite_rule [stable_def] stable_reachable RS constrains_Int);
+(*** Specialized laws for handling invariants ***)
+
+Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
+bd invariant_includes_reachable 1;
+by (Blast_tac 1);
+qed "reachable_Int_INV";
+
+Goal "[| invariant prg INV; LeadsTo prg (INV Int A) A' |] \
+\ ==> LeadsTo prg A A'";
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
+ Int_assoc RS sym]) 1);
+qed "invariant_LeadsToI";
+
+Goal "[| invariant prg INV; LeadsTo prg A A' |] \
+\ ==> LeadsTo prg A (INV Int A')";
+by (asm_full_simp_tac
+ (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
+ Int_assoc RS sym]) 1);
+qed "invariant_LeadsToD";
+
+
(*** Introduction rules: Basis, Trans, Union ***)
Goal "leadsTo (Acts prg) A B ==> LeadsTo prg A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
+by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
qed "leadsTo_imp_LeadsTo";
-Goal "ensures (Acts prg) (reachable prg Int A) (reachable prg Int A') \
-\ ==> LeadsTo prg A A'";
-by (full_simp_tac (simpset() addsimps [ensures_def, LeadsTo_def]) 1);
-by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib])));
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "LeadsTo_Basis";
+(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
+bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
-Goal "[| LeadsTo prg A B; LeadsTo prg B C |] \
-\ ==> LeadsTo prg A C";
+Goal "[| LeadsTo prg A B; LeadsTo prg B C |] ==> LeadsTo prg A C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
qed "LeadsTo_Trans";
-val [prem] = goalw thy [LeadsTo_def]
+val [prem] = Goalw [LeadsTo_def]
"(!!A. A : S ==> LeadsTo prg A B) ==> LeadsTo prg (Union S) B";
by (Simp_tac 1);
by (stac Int_Union 1);
@@ -46,7 +61,7 @@
(*** Derived rules ***)
-Goal "id: (Acts prg) ==> LeadsTo prg A UNIV";
+Goal "id: Acts prg ==> LeadsTo prg A UNIV";
by (asm_simp_tac (simpset() addsimps [LeadsTo_def,
Int_lower1 RS subset_imp_leadsTo]) 1);
qed "LeadsTo_UNIV";
@@ -61,9 +76,8 @@
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
qed "LeadsTo_Un_duplicate2";
-val prems = goal thy
- "(!!i. i : I ==> LeadsTo prg (A i) B) \
-\ ==> LeadsTo prg (UN i:I. A i) B";
+val prems =
+Goal "(!!i. i : I ==> LeadsTo prg (A i) B) ==> LeadsTo prg (UN i:I. A i) B";
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
qed "LeadsTo_UN";
@@ -74,14 +88,7 @@
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
-
-Goal "[| reachable prg Int A <= B; id: (Acts prg) |] \
-\ ==> LeadsTo prg A B";
-by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
-qed "Int_subset_imp_LeadsTo";
-
-Goal "[| A <= B; id: (Acts prg) |] ==> LeadsTo prg A B";
+Goal "[| A <= B; id: Acts prg |] ==> LeadsTo prg A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
@@ -89,22 +96,13 @@
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
Addsimps [empty_LeadsTo];
-Goal "[| reachable prg Int A = {}; id: (Acts prg) |] \
-\ ==> LeadsTo prg A B";
-by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
-qed "Int_empty_LeadsTo";
-
-
-Goal "[| LeadsTo prg A A'; \
-\ reachable prg Int A' <= B' |] \
-\ ==> LeadsTo prg A B'";
+Goal "[| LeadsTo prg A A'; A' <= B' |] ==> LeadsTo prg A B'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
qed_spec_mp "LeadsTo_weaken_R";
-Goal "[| LeadsTo prg A A'; \
-\ reachable prg Int B <= A; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A A'; B <= A; id: Acts prg |] \
\ ==> LeadsTo prg B A'";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
@@ -112,49 +110,74 @@
(*Distributes over binary unions*)
-Goal "id: (Acts prg) ==> \
+Goal "id: Acts prg ==> \
\ LeadsTo prg (A Un B) C = \
\ (LeadsTo prg A C & LeadsTo prg B C)";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Un_distrib";
-Goal "id: (Acts prg) ==> \
+Goal "id: Acts prg ==> \
\ LeadsTo prg (UN i:I. A i) B = \
\ (ALL i : I. LeadsTo prg (A i) B)";
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
qed "LeadsTo_UN_distrib";
-Goal "id: (Acts prg) ==> \
+Goal "id: Acts prg ==> \
\ LeadsTo prg (Union S) B = \
\ (ALL A : S. LeadsTo prg A B)";
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
qed "LeadsTo_Union_distrib";
-Goal "[| LeadsTo prg A A'; id: (Acts prg); \
-\ reachable prg Int B <= A; \
-\ reachable prg Int A' <= B' |] \
+Goal "[| LeadsTo prg A A'; id: Acts prg; \
+\ B <= A; A' <= B' |] \
\ ==> LeadsTo prg B B'";
-(*PROOF FAILED: why?*)
+(*PROOF FAILED*)
by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
LeadsTo_weaken_L]) 1);
qed "LeadsTo_weaken";
+(** More rules using the premise "invariant prg" **)
+
+Goal "[| invariant prg INV; \
+\ constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
+\ transient (Acts prg) (INV Int (A-A')) |] \
+\ ==> LeadsTo prg A A'";
+br invariant_LeadsToI 1;
+ba 1;
+by (rtac (ensuresI RS LeadsTo_Basis) 1);
+by (ALLGOALS
+ (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym,
+ Diff_Int_distrib RS sym])));
+be invariantE 1;
+by (blast_tac (claset() addSDs [stable_constrains_Int]
+ addIs [constrains_weaken]) 1);
+qed "invariant_LeadsTo_Basis";
+
+Goal "[| invariant prg INV; \
+\ LeadsTo prg A A'; id: Acts prg; \
+\ INV Int B <= A; INV Int A' <= B' |] \
+\ ==> LeadsTo prg B B'";
+br invariant_LeadsToI 1;
+ba 1;
+bd invariant_LeadsToD 1;
+ba 1;
+by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
+qed "invariant_LeadsTo_weaken";
+
+
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
-Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: (Acts prg) |] \
+Goal "[| LeadsTo prg (A-B) C; LeadsTo prg B C; id: Acts prg |] \
\ ==> LeadsTo prg A C";
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";
-(** Meta or object quantifier ???????????????????
- see ball_constrains_UN in UNITY.ML***)
-
-val prems = goal thy
- "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
-\ ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
+val prems =
+Goal "(!! i. i:I ==> LeadsTo prg (A i) (A' i)) \
+\ ==> LeadsTo prg (UN i:I. A i) (UN i:I. A' i)";
by (simp_tac (simpset() addsimps [Union_image_eq RS sym]) 1);
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R]
addIs prems) 1);
@@ -187,26 +210,26 @@
(** The cancellation law **)
Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg B B'; \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A (A' Un B')";
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
qed "LeadsTo_cancel2";
-Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A (A' Un B); LeadsTo prg (B-A') B'; id: Acts prg |] \
\ ==> LeadsTo prg A (A' Un B')";
by (rtac LeadsTo_cancel2 1);
by (assume_tac 2);
by (ALLGOALS Asm_simp_tac);
qed "LeadsTo_cancel_Diff2";
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg B B'; id: Acts prg |] \
\ ==> LeadsTo prg A (B' Un A')";
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
qed "LeadsTo_cancel1";
-Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A (B Un A'); LeadsTo prg (B-A') B'; id: Acts prg |] \
\ ==> LeadsTo prg A (B' Un A')";
by (rtac LeadsTo_cancel1 1);
by (assume_tac 2);
@@ -217,7 +240,8 @@
(** The impossibility law **)
-Goal "LeadsTo prg A {} ==> reachable prg Int A = {}";
+(*The set "A" may be non-empty, but it contains no reachable states*)
+Goal "LeadsTo prg A {} ==> reachable prg Int A = {}";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_empty 1);
qed "LeadsTo_empty";
@@ -229,40 +253,40 @@
Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
\ ==> LeadsTo prg (A Int B) (A' Int B)";
by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym,
- PSP_stable]) 1);
-qed "R_PSP_stable";
+ psp_stable]) 1);
+qed "PSP_stable";
Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
-\ ==> LeadsTo prg (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
-qed "R_PSP_stable2";
+\ ==> LeadsTo prg (B Int A) (B Int A')";
+by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
+qed "PSP_stable2";
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (dtac PSP 1);
+by (dtac psp 1);
by (etac constrains_reachable 1);
by (etac leadsTo_weaken 2);
by (ALLGOALS Blast_tac);
-qed "R_PSP";
+qed "PSP";
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: (Acts prg) |] \
+Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
-qed "R_PSP2";
+by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
+qed "PSP2";
Goalw [unless_def]
- "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: (Acts prg) |] \
+ "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
-by (dtac R_PSP 1);
+by (dtac PSP 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
by (etac LeadsTo_Diff 2);
by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
by Auto_tac;
-qed "R_PSP_unless";
+qed "PSP_unless";
(*** Induction rules ***)
@@ -271,7 +295,7 @@
Goal "[| wf r; \
\ ALL m. LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (etac leadsTo_wf_induct 1);
@@ -283,38 +307,38 @@
Goal "[| wf r; \
\ ALL m:I. LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A ((A - (f-``I)) Un B)";
by (etac LeadsTo_wf_induct 1);
by Safe_tac;
by (case_tac "m:I" 1);
by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
-qed "R_bounded_induct";
+qed "Bounded_induct";
Goal "[| ALL m. LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A B";
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
by (assume_tac 2);
by (Asm_simp_tac 1);
-qed "R_lessThan_induct";
+qed "LessThan_induct";
Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(lessThan m)) Un B); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A ((A Int (f-``(atMost l))) Un B)";
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
-by (rtac (wf_less_than RS R_bounded_induct) 1);
+by (rtac (wf_less_than RS Bounded_induct) 1);
by (assume_tac 2);
by (Asm_simp_tac 1);
-qed "R_lessThan_bounded_induct";
+qed "LessThan_bounded_induct";
Goal "[| ALL m:(lessThan l). LeadsTo prg (A Int f-``{m}) \
\ ((A Int f-``(greaterThan m)) Un B); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg A ((A Int (f-``(atLeast l))) Un B)";
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
@@ -324,36 +348,35 @@
by (case_tac "m<l" 1);
by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
-qed "R_greaterThan_bounded_induct";
-
+qed "GreaterThan_bounded_induct";
(*** Completion: Binary and General Finite versions ***)
Goal "[| LeadsTo prg A A'; stable (Acts prg) A'; \
-\ LeadsTo prg B B'; stable (Acts prg) B'; id: (Acts prg) |] \
+\ LeadsTo prg B B'; stable (Acts prg) B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) (A' Int B')";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken]
addSIs [stable_Int, stable_reachable]) 1);
-qed "R_stable_completion";
+qed "Stable_completion";
-Goal "[| finite I; id: (Acts prg) |] \
+Goal "[| finite I; id: Acts prg |] \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i)) --> \
\ (ALL i:I. stable (Acts prg) (A' i)) --> \
\ LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac
- (simpset() addsimps [R_stable_completion, stable_def,
+ (simpset() addsimps [Stable_completion, stable_def,
ball_constrains_INT]) 1);
-qed_spec_mp "R_finite_stable_completion";
+qed_spec_mp "Finite_stable_completion";
Goal "[| LeadsTo prg A (A' Un C); constrains (Acts prg) A' (A' Un C); \
\ LeadsTo prg B (B' Un C); constrains (Acts prg) B' (B' Un C); \
-\ id: (Acts prg) |] \
+\ id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
by (dtac completion 1);
@@ -362,10 +385,10 @@
(asm_simp_tac
(simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
-qed "R_completion";
+qed "Completion";
-Goal "[| finite I; id: (Acts prg) |] \
+Goal "[| finite I; id: Acts prg |] \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) --> \
\ (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
\ LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
@@ -373,48 +396,8 @@
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
by (dtac ball_constrains_INT 1);
-by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1);
-qed "R_finite_completion";
-
-
-
-(*** Specialized laws for handling invariants ***)
-
-Goalw [transient_def]
- "[| reachable prg <= INV; transient (Acts prg) (INV Int A) |] \
-\ ==> transient (Acts prg) (reachable prg Int A)";
-by (Clarify_tac 1);
-by (rtac bexI 1);
-by (assume_tac 2);
-by (Blast_tac 1);
-qed "reachable_transient";
-
-(*Uses the premise "invariant prg". Raw theorem-proving on this
- inclusion is slow: the term contains a copy of the program.*)
-Goal "[| invariant prg INV; \
-\ constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
-\ transient (Acts prg) (INV Int (A-A')) |] \
-\ ==> ensures (Acts prg) (reachable prg Int A) (reachable prg Int A')";
-bd invariant_includes_reachable 1;
-by (rtac ensuresI 1);
-by (ALLGOALS
- (full_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym])));
-by (blast_tac (claset() addSIs [reachable_transient]) 2);
-br (stable_reachable RS stable_constrains_Int) 1;
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
-qed "invariant_ensuresI";
-
-bind_thm ("invariant_LeadsTo_Basis", invariant_ensuresI RS LeadsTo_Basis);
-
-
-Goal "[| invariant prg INV; \
-\ LeadsTo prg A A'; id: (Acts prg); \
-\ INV Int B <= A; INV Int A' <= B' |] \
-\ ==> LeadsTo prg B B'";
-by (blast_tac (claset() addDs [invariant_includes_reachable]
- addIs [LeadsTo_weaken]) 1);
-qed "invariant_LeadsTo_weaken";
+by (asm_full_simp_tac (simpset() addsimps [Completion]) 1);
+qed "Finite_completion";
(** Constrains/Ensures tactics
--- a/src/HOL/UNITY/SubstAx.thy Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Thu Aug 06 15:47:26 1998 +0200
@@ -3,10 +3,10 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-My treatment of the Substitution Axiom -- not as an axiom!
+LeadsTo relation: restricted to the set of reachable states.
*)
-SubstAx = WFair +
+SubstAx = WFair + Traces +
constdefs
--- a/src/HOL/UNITY/Token.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Token.ML Thu Aug 06 15:47:26 1998 +0200
@@ -119,6 +119,6 @@
by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
by (rtac TR6 2);
by (rtac leadsTo_weaken_R 1);
-by (rtac ([leadsTo_j, TR3] MRS PSP) 1);
+by (rtac ([leadsTo_j, TR3] MRS psp) 1);
by (ALLGOALS Blast_tac);
qed "token_progress";
--- a/src/HOL/UNITY/Token.thy Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Token.thy Thu Aug 06 15:47:26 1998 +0200
@@ -9,7 +9,7 @@
*)
-Token = WFair +
+Token = WFair +
(*process states*)
datatype pstate = Hungry | Eating | Thinking
--- a/src/HOL/UNITY/Traces.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Thu Aug 06 15:47:26 1998 +0200
@@ -35,12 +35,19 @@
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
qed "invariant_includes_reachable";
-(*If "A" includes the initial states and is stable then "A" is invariant.
- Result is trivial from the definition, but it is handy.*)
+
+(** Natural deduction rules for "invariant prg A" **)
+
Goal "[| (Init prg)<=A; stable (Acts prg) A |] ==> invariant prg A";
by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
qed "invariantI";
+Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
+by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
+qed "invariantD";
+
+bind_thm ("invariantE", invariantD RS conjE);
+
(** Conjoining invariants **)
--- a/src/HOL/UNITY/UNITY.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Thu Aug 06 15:47:26 1998 +0200
@@ -14,7 +14,7 @@
(*** constrains ***)
-val prems = goalw thy [constrains_def]
+val prems = Goalw [constrains_def]
"(!!act s s'. [| act: acts; (s,s') : act; s: A |] ==> s': A') \
\ ==> constrains acts A A'";
by (blast_tac (claset() addIs prems) 1);
@@ -50,18 +50,11 @@
by (Blast_tac 1);
qed "constrains_weaken";
-(*Set difference: UNUSED*)
-Goalw [constrains_def]
- "[| constrains acts (A-B) C; constrains acts B C |] \
-\ ==> constrains acts A C";
-by (Blast_tac 1);
-qed "constrains_Diff";
-
(** Union **)
Goalw [constrains_def]
"[| constrains acts A A'; constrains acts B B' |] \
-\ ==> constrains acts (A Un B) (A' Un B')";
+\ ==> constrains acts (A Un B) (A' Un B')";
by (Blast_tac 1);
qed "constrains_Un";
@@ -73,7 +66,7 @@
Goalw [constrains_def]
"[| ALL i. constrains acts (A i) (A' i) |] \
-\ ==> constrains acts (UN i. A i) (UN i. A' i)";
+\ ==> constrains acts (UN i. A i) (UN i. A' i)";
by (Blast_tac 1);
qed "all_constrains_UN";
@@ -81,7 +74,7 @@
Goalw [constrains_def]
"[| constrains acts A A'; constrains acts B B' |] \
-\ ==> constrains acts (A Int B) (A' Int B')";
+\ ==> constrains acts (A Int B) (A' Int B')";
by (Blast_tac 1);
qed "constrains_Int";
@@ -93,21 +86,20 @@
Goalw [constrains_def]
"[| ALL i. constrains acts (A i) (A' i) |] \
-\ ==> constrains acts (INT i. A i) (INT i. A' i)";
+\ ==> constrains acts (INT i. A i) (INT i. A' i)";
by (Blast_tac 1);
qed "all_constrains_INT";
-Goalw [stable_def, constrains_def]
- "[| stable acts C; constrains acts A (C Un A') |] \
-\ ==> constrains acts (C Un A) (C Un A')";
+Goalw [constrains_def]
+ "[| constrains acts A A'; id: acts |] ==> A<=A'";
by (Blast_tac 1);
-qed "stable_constrains_Un";
+qed "constrains_imp_subset";
-Goalw [stable_def, constrains_def]
- "[| stable acts C; constrains acts (C Int A) A' |] \
-\ ==> constrains acts (C Int A) (C Int A')";
+Goalw [constrains_def]
+ "[| id: acts; constrains acts A B; constrains acts B C |] \
+\ ==> constrains acts A C";
by (Blast_tac 1);
-qed "stable_constrains_Int";
+qed "constrains_trans";
(*** stable ***)
@@ -124,27 +116,27 @@
Goalw [stable_def]
"[| stable acts A; stable acts A' |] \
-\ ==> stable acts (A Un A')";
+\ ==> stable acts (A Un A')";
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "stable_Un";
Goalw [stable_def]
"[| stable acts A; stable acts A' |] \
-\ ==> stable acts (A Int A')";
+\ ==> stable acts (A Int A')";
by (blast_tac (claset() addIs [constrains_Int]) 1);
qed "stable_Int";
-Goalw [constrains_def]
- "[| constrains acts A A'; id: acts |] ==> A<=A'";
+Goalw [stable_def, constrains_def]
+ "[| stable acts C; constrains acts A (C Un A') |] \
+\ ==> constrains acts (C Un A) (C Un A')";
by (Blast_tac 1);
-qed "constrains_imp_subset";
-
+qed "stable_constrains_Un";
-Goalw [constrains_def]
- "[| id: acts; constrains acts A B; constrains acts B C |] \
-\ ==> constrains acts A C";
+Goalw [stable_def, constrains_def]
+ "[| stable acts C; constrains acts (C Int A) A' |] \
+\ ==> constrains acts (C Int A) (C Int A')";
by (Blast_tac 1);
-qed "constrains_trans";
+qed "stable_constrains_Int";
(*The Elimination Theorem. The "free" m has become universally quantified!
@@ -152,7 +144,7 @@
in forward proof.*)
Goalw [constrains_def]
"[| ALL m. constrains acts {s. s x = m} (B m) |] \
-\ ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
+\ ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
by (Blast_tac 1);
qed "elimination";
@@ -160,14 +152,14 @@
state is identified with its one variable.*)
Goalw [constrains_def]
"[| ALL m. constrains acts {m} (B m) |] \
-\ ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
+\ ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
by (Blast_tac 1);
qed "elimination_sing";
Goalw [constrains_def]
"[| constrains acts A (A' Un B); constrains acts B B'; id: acts |] \
-\ ==> constrains acts A (A' Un B')";
+\ ==> constrains acts A (A' Un B')";
by (Blast_tac 1);
qed "constrains_cancel";
--- a/src/HOL/UNITY/WFair.ML Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML Thu Aug 06 15:47:26 1998 +0200
@@ -272,23 +272,18 @@
(simpset() addsimps [ensures_def,
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1);
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1);
-qed "PSP_stable";
+qed "psp_stable";
Goal "[| leadsTo acts A A'; stable acts B |] \
\ ==> leadsTo acts (B Int A) (B Int A')";
-by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
-qed "PSP_stable2";
+by (asm_simp_tac (simpset() addsimps (psp_stable::Int_ac)) 1);
+qed "psp_stable2";
-
-Goalw [ensures_def]
+Goalw [ensures_def, constrains_def]
"[| ensures acts A A'; constrains acts B B' |] \
\ ==> ensures acts (A Int B) ((A' Int B) Un (B' - B))";
-by Safe_tac;
-by (blast_tac (claset() addIs [constrainsI] addDs [constrainsD]) 1);
-by (etac transient_strengthen 1);
-by (Blast_tac 1);
-qed "PSP_ensures";
-
+by (blast_tac (claset() addIs [transient_strengthen]) 1);
+qed "psp_ensures";
Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
\ ==> leadsTo acts (A Int B) ((A' Int B) Un (B' - B))";
@@ -301,26 +296,26 @@
by (assume_tac 3);
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2);
(*Basis case*)
-by (blast_tac (claset() addIs [leadsTo_Basis, PSP_ensures]) 1);
-qed "PSP";
+by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1);
+qed "psp";
Goal "[| leadsTo acts A A'; constrains acts B B'; id: acts |] \
\ ==> leadsTo acts (B Int A) ((B Int A') Un (B' - B))";
-by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
-qed "PSP2";
+by (asm_simp_tac (simpset() addsimps (psp::Int_ac)) 1);
+qed "psp2";
Goalw [unless_def]
"[| leadsTo acts A A'; unless acts B B'; id: acts |] \
\ ==> leadsTo acts (A Int B) ((A' Int B) Un B')";
-by (dtac PSP 1);
+by (dtac psp 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
by (etac leadsTo_Diff 2);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 2);
by Auto_tac;
-qed "PSP_unless";
+qed "psp_unless";
(*** Proving the induction rules ***)
@@ -482,9 +477,9 @@
fast_tac (claset() addEs [wlt_increasing RSN (2,rev_subsetD)]) 3,
Blast_tac 2]);
by (subgoal_tac "leadsTo acts (A Int wlt acts B') (A' Int wlt acts B')" 1);
-by (blast_tac (claset() addIs [PSP_stable]) 2);
+by (blast_tac (claset() addIs [psp_stable]) 2);
by (subgoal_tac "leadsTo acts (A' Int wlt acts B') (A' Int B')" 1);
-by (blast_tac (claset() addIs [wlt_leadsTo, PSP_stable2]) 2);
+by (blast_tac (claset() addIs [wlt_leadsTo, psp_stable2]) 2);
by (subgoal_tac "leadsTo acts (A Int B) (A Int wlt acts B')" 1);
by (blast_tac (claset() addIs [leadsTo_subset RS subsetD,
subset_imp_leadsTo]) 2);
@@ -518,10 +513,10 @@
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2);
by (subgoal_tac "leadsTo acts (A Int W - C) (A' Int W Un C)" 1);
by (simp_tac (simpset() addsimps [Int_Diff]) 2);
-by (blast_tac (claset() addIs [wlt_leadsTo, PSP RS leadsTo_weaken_R]) 2);
+by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken_R]) 2);
by (subgoal_tac "leadsTo acts (A' Int W Un C) (A' Int B' Un C)" 1);
by (blast_tac (claset() addIs [wlt_leadsTo, leadsTo_Un_Un,
- PSP2 RS leadsTo_weaken_R,
+ psp2 RS leadsTo_weaken_R,
subset_refl RS subset_imp_leadsTo,
leadsTo_Un_duplicate2]) 2);
by (dtac leadsTo_Diff 1);
--- a/src/HOL/UNITY/WFair.thy Thu Aug 06 14:04:49 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy Thu Aug 06 15:47:26 1998 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-WFair = Traces + Vimage +
+WFair = UNITY +
constdefs