# HG changeset patch
# User paulson
# Date 902411246 -7200
# Node ID e4297d03e5d288a85cc78f0c535027127cad0dfd
# Parent  dd99b958b3064039125e5b045d7dc29ebbaf9f0c
A higher-level treatment of LeadsTo, minimizing use of "reachable"

diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Channel.ML
--- 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;
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Common.ML
--- 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";
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Common.thy
--- 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
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Handshake.ML
--- 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}*)
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Lift.ML
--- /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();
+
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Lift.thy
--- /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
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Mutex.ML
--- 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";
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/SubstAx.ML
--- 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 
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/SubstAx.thy
--- 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
 
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Token.ML
--- 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";
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Token.thy
--- 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
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/Traces.ML
--- 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 **)
 
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/UNITY.ML
--- 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";
 
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/WFair.ML
--- 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);
diff -r dd99b958b306 -r e4297d03e5d2 src/HOL/UNITY/WFair.thy
--- 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