# HG changeset patch
# User paulson
# Date 901903615 -7200
# Node ID e5a7cdd07ea59207822c2eee0ec8a629abf5b7f8
# Parent  2a454140ae2414ed168134b52864a6b33239868e
Tidied; uses records

diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Channel.ML
--- a/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,11 +8,8 @@
 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
 *)
 
-open Channel;
-
 AddIffs [skip];
 
-
 (*None represents "infinity" while Some represents proper integers*)
 Goalw [minSet_def] "minSet A = Some x --> x : A";
 by (Simp_tac 1);
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Deadlock.ML
--- a/src/HOL/UNITY/Deadlock.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Traces
+(*  Title:      HOL/UNITY/Deadlock
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/FP.ML
--- a/src/HOL/UNITY/FP.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/FP.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,12 +8,6 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-Goal "Union(B) Int A = (UN C:B. C Int A)";
-by (Blast_tac 1);
-qed "Int_Union2";
-
-open FP;
-
 Goalw [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
 by (stac Int_Union2 1);
 by (rtac ball_constrains_UN 1);
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -7,9 +7,6 @@
 *)
 
 
-open LessThan;
-
-
 (*** lessThan ***)
 
 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
@@ -144,3 +141,55 @@
 qed "atMost_Int_atLeast";
 
 
+
+
+(*** Finally, a few set-theoretic laws...
+     CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)
+
+context Set.thy;
+
+(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
+    be any set including A Int C and contained in A Un C, such as B=A or B=C.
+**)
+
+Goal "[| A Int C <= B; B <= A Un C |] \
+\     ==> (A Int B) Un (Compl A Int C) = B Un C";
+by (Blast_tac 1);
+
+Goal "[| A Int C <= B; B <= A Un C |] \
+\     ==> (A Un B) Int (Compl A Un C) = B Int C";
+by (Blast_tac 1);
+
+(*The base B=A*)
+Goal "A Un (Compl A Int C) = A Un C";
+by (Blast_tac 1);
+
+Goal "A Int (Compl A Un C) = A Int C";
+by (Blast_tac 1);
+
+(*The base B=C*)
+Goal "(A Int C) Un (Compl A Int C) = C";
+by (Blast_tac 1);
+
+Goal "(A Un C) Int (Compl A Un C) = C";
+by (Blast_tac 1);
+
+
+(** More ad-hoc rules **)
+
+Goal "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+
+Goal "A Int (B - C) Un C = A Int B Un C";
+by (Blast_tac 1);
+qed "Int_Diff_Un";
+
+Goal "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
+Goal "Union(B) Int A = Union((%C. C Int A)``B)";
+by (Blast_tac 1);
+qed "Int_Union_Union";
+
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/LessThan.thy
--- a/src/HOL/UNITY/LessThan.thy	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/LessThan.thy	Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
 lessThan, greaterThan, atLeast, atMost
 *)
 
-LessThan = List +
+LessThan = Main +
 
 constdefs
 
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -6,10 +6,12 @@
 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
 *)
 
-open Mutex;
+(*split_all_tac causes a big blow-up*)
+claset_ref() := claset() delSWrapper "split_all_tac";
 
-val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
-		cmd2_def, cmd3_def, cmd4_def];
+val cmd_defs = [mutex_def, 
+		cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, 
+		cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def];
 
 Goalw [mutex_def] "id : mutex";
 by (Simp_tac 1);
@@ -17,7 +19,16 @@
 AddIffs [id_in_mutex];
 
 
-(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+(*Simplification for records*)
+val select_defs = thms"state.select_defs"
+and update_defs = thms"state.update_defs"
+and dest_defs   = thms"state.dest_defs";
+
+Addsimps update_defs;
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS
+     [They have free occurrences of mutex_def and cmd_defs] **)
 
 (*proves "constrains" properties when the program is specified*)
 val constrains_tac = 
@@ -32,82 +43,67 @@
 (*proves "ensures" properties when the program is specified*)
 fun ensures_tac sact = 
     SELECT_GOAL
-      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+      (EVERY [etac reachable_LeadsTo_Basis 1 
+	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
+		  REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, 
+				    ensuresI] 1),
 	      res_inst_tac [("act", sact)] transient_mem 2,
-	      Simp_tac 2,
+	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
+	      simp_tac (simpset() addsimps [mutex_def]) 2,
 	      constrains_tac 1,
 	      rewrite_goals_tac cmd_defs,
+	      ALLGOALS Clarify_tac,
 	      Auto_tac]);
 
 
-(*The booleans p, u, v are always either 0 or 1*)
-Goalw [stable_def, boolVars_def]
-    "stable mutex boolVars";
+Goalw [stable_def, invariantU_def] "stable mutex invariantU";
 by (constrains_tac 1);
-by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "stable_boolVars";
+qed "stable_invariantU";
 
-Goal "reachable (MInit,mutex) <= boolVars";
-by (rtac strongest_invariant 1);
-by (rtac stable_boolVars 2);
-by (rewrite_goals_tac [MInit_def, boolVars_def]);
-by Auto_tac;
-qed "reachable_subset_boolVars";
-
-val reachable_subset_boolVars' = 
-    rewrite_rule [boolVars_def] reachable_subset_boolVars;
+Goalw [stable_def, invariantV_def] "stable mutex invariantV";
+by (constrains_tac 1);
+qed "stable_invariantV";
 
-Goalw [stable_def, invariant_def]
-    "stable mutex (invariant 0 UU MM)";
-by (constrains_tac 1);
-qed "stable_invar_0um";
+Goalw [MInit_def, invariantU_def] "MInit <= invariantU";
+by Auto_tac;
+qed "MInit_invariantU";
 
-Goalw [stable_def, invariant_def]
-    "stable mutex (invariant 1 VV NN)";
-by (constrains_tac 1);
-qed "stable_invar_1vn";
-
-Goalw [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
+Goalw [MInit_def, invariantV_def] "MInit <= invariantV";
 by Auto_tac;
-qed "MInit_invar_0um";
-
-Goalw [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
-by Auto_tac;
-qed "MInit_invar_1vn";
+qed "MInit_invariantV";
 
 (*The intersection is an invariant of the system*)
-Goal "reachable (MInit,mutex) <= invariant 0 UU MM Int invariant 1 VV NN";
+Goal "reachable (MInit,mutex) <= invariantU Int invariantV";
 by (simp_tac (simpset() addsimps
 	      [strongest_invariant, Int_greatest, stable_Int, 
-	       stable_invar_0um, stable_invar_1vn, 
-	       MInit_invar_0um,MInit_invar_1vn]) 1); 
+	       stable_invariantU, stable_invariantV, 
+	       MInit_invariantU,MInit_invariantV]) 1); 
 qed "reachable_subset_invariant";
 
 val reachable_subset_invariant' = 
-    rewrite_rule [invariant_def] reachable_subset_invariant;
+    rewrite_rule [invariantU_def, invariantV_def] reachable_subset_invariant;
 
 
 (*The safety property (mutual exclusion) follows from the claimed invar_s*)
-Goalw [invariant_def]
-    "{s. s MM = 3 & s NN = 3} <= \
-\    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
+Goalw [invariantU_def, invariantV_def]
+    "{s. MM s = 3 & NN s = 3} <= Compl (invariantU Int invariantV)";
 by Auto_tac;
 val lemma = result();
 
-Goal "{s. s MM = 3 & s NN = 3} <= Compl (reachable (MInit,mutex))";
-by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
+Goal "{s. MM s = 3 & NN s = 3} <= Compl (reachable (MInit,mutex))";
+by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] 
+	  MRS subset_trans) 1);
 qed "mutual_exclusion";
 
 
-(*The bad invariant FAILS in cmd1v*)
-Goalw [stable_def, bad_invariant_def]
-    "stable mutex (bad_invariant 0 UU MM)";
+(*The bad invariant FAILS in cmd1V*)
+Goalw [stable_def, bad_invariantU_def] "stable mutex bad_invariantU";
 by (constrains_tac 1);
-by (trans_tac 1);
+by (REPEAT (trans_tac 1));
 by (safe_tac (claset() addSEs [le_SucE]));
 by (Asm_full_simp_tac 1);
 (*Resulting state: n=1, p=false, m=4, u=false.  
-  Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
+  Execution of cmd1V (the command of process v guarded by n=1) sets p:=true,
   violating the invariant!*)
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
@@ -115,42 +111,40 @@
 
 (*** Progress for U ***)
 
-Goalw [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
+Goalw [unless_def] "unless mutex {s. MM s=2} {s. MM s=3}";
 by (constrains_tac 1);
 qed "U_F0";
 
-Goal "LeadsTo(MInit,mutex) {s. s MM=1} {s. s PP = s VV & s MM = 2}";
-by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
-by (ensures_tac "cmd1u" 1);
+Goal "LeadsTo(MInit,mutex) {s. MM s=1} {s. PP s = VV s & MM s = 2}";
+by (ensures_tac "cmd1U" 1);
 qed "U_F1";
 
-Goal "LeadsTo(MInit,mutex) {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. ~ PP s & MM s = 2} {s. MM s = 3}";
 by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2 0 MM" 1);
+by (ensures_tac "cmd2U" 1);
 qed "U_F2";
 
-Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s MM = 3} {s. s PP = 1}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. MM s = 3} {s. PP s}";
 by (rtac leadsTo_imp_LeadsTo 1); 
-by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4 1 MM" 2);
-by (ensures_tac "cmd3 UU MM" 1);
+by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4U" 2);
+by (ensures_tac "cmd3U" 1);
 qed "U_F3";
 
-Goal "LeadsTo(MInit,mutex) {s. s MM = 2} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {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 (cut_facts_tac [reachable_subset_boolVars'] 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val lemma2 = result();
 
-Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. PP s}";
 by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val lemma1 = result();
 
 
-Goal "LeadsTo(MInit,mutex) {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= MM s & MM s <= 3} {s. PP s}";
 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
 	                addcongs [rev_conj_cong]) 1);
 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -159,7 +153,7 @@
 
 
 (*Misra's F4*)
-Goal "LeadsTo(MInit,mutex) {s. s UU = 1} {s. s PP = 1}";
+Goal "LeadsTo(MInit,mutex) {s. UU s} {s. PP s}";
 by (rtac LeadsTo_weaken_L 1);
 by (rtac lemma123 1);
 by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -170,42 +164,40 @@
 (*** Progress for V ***)
 
 
-Goalw [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
+Goalw [unless_def] "unless mutex {s. NN s=2} {s. NN s=3}";
 by (constrains_tac 1);
 qed "V_F0";
 
-Goal "LeadsTo(MInit,mutex) {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
-by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
-by (ensures_tac "cmd1v" 1);
+Goal "LeadsTo(MInit,mutex) {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
+by (ensures_tac "cmd1V" 1);
 qed "V_F1";
 
-Goal "LeadsTo(MInit,mutex) {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. PP s & NN s = 2} {s. NN s = 3}";
 by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2 1 NN" 1);
+by (ensures_tac "cmd2V" 1);
 qed "V_F2";
 
-Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. s NN = 3} {s. s PP = 0}";
+Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. NN s = 3} {s. ~ PP s}";
 by (rtac leadsTo_imp_LeadsTo 1); 
-by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4 0 NN" 2);
-by (ensures_tac "cmd3 VV NN" 1);
+by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
+by (ensures_tac "cmd4V" 2);
+by (ensures_tac "cmd3V" 1);
 qed "V_F3";
 
-Goal "LeadsTo(MInit,mutex) {s. s NN = 2} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 2} {s. ~ PP s}";
 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
 	  MRS LeadsTo_Diff) 1);
 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 val lemma2 = result();
 
-Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. ~ PP s}";
 by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
 by (Blast_tac 1);
 val lemma1 = result();
 
 
-Goal "LeadsTo(MInit,mutex) {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
 	                addcongs [rev_conj_cong]) 1);
 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
@@ -214,7 +206,7 @@
 
 
 (*Misra's F4*)
-Goal "LeadsTo(MInit,mutex) {s. s VV = 1} {s. s PP = 0}";
+Goal "LeadsTo(MInit,mutex) {s. VV s} {s. ~ PP s}";
 by (rtac LeadsTo_weaken_L 1);
 by (rtac lemma123 1);
 by (cut_facts_tac [reachable_subset_invariant'] 1);
@@ -225,7 +217,7 @@
 (** Absence of starvation **)
 
 (*Misra's F6*)
-Goal "LeadsTo(MInit,mutex) {s. s MM = 1} {s. s MM = 3}";
+Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. MM s = 3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac U_F2 2);
@@ -234,13 +226,12 @@
 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 (U_F1 RS LeadsTo_weaken_R) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "m1_leadsto_3";
 
 
 (*The same for V*)
-Goal "LeadsTo(MInit,mutex) {s. s NN = 1} {s. s NN = 3}";
+Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. NN s = 3}";
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac LeadsTo_cancel2 1);
 by (rtac V_F2 2);
@@ -249,6 +240,5 @@
 by (rtac LeadsTo_Un_duplicate 1);
 by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
-by (cut_facts_tac [reachable_subset_boolVars'] 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "n1_leadsto_3";
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
 *)
 
-Mutex = Update + UNITY + Traces + SubstAx +
+Mutex = UNITY + Traces + SubstAx +
 
 (*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
 syntax
@@ -18,57 +18,66 @@
    "4"  == "Suc 3"
 
 
-(*program variables*)
-datatype pvar = PP | MM | NN | UU | VV
-
-(*No booleans; instead True=1 and False=0*)
-types state = pvar => nat
+record state =
+  PP :: bool
+  MM :: nat
+  NN :: nat
+  UU :: bool
+  VV :: bool
 
 constdefs
-  cmd0 :: "[pvar,pvar] => (state*state) set"
-    "cmd0 u m == {(s,s'). s' = s(u:=1,m:=1) & s m = 0}"
+  cmd0U :: "(state*state) set"
+    "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}"
+
+  cmd1U :: "(state*state) set"
+    "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}"
 
-  cmd1u :: "(state*state) set"
-    "cmd1u == {(s,s'). s' = s(PP:= s VV,MM:=2) & s MM = 1}"
+  cmd2U :: "(state*state) set"
+    "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}"
 
-  cmd1v :: "(state*state) set"
-    "cmd1v == {(s,s'). s' = s(PP:= 1 - s UU,NN:=2) & s NN = 1}"
+  cmd3U :: "(state*state) set"
+    "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}"
+
+  cmd4U :: "(state*state) set"
+    "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}"
 
-  (*Put pv=0 for u's program and pv=1 for v's program*)
-  cmd2 :: "[nat,pvar] => (state*state) set"
-    "cmd2 pv m == {(s,s'). s' = s(m:=3) & s PP = pv & s m = 2}"
+  cmd0V :: "(state*state) set"
+    "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}"
+
+  cmd1V :: "(state*state) set"
+    "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}"
 
-  cmd3 :: "[pvar,pvar] => (state*state) set"
-    "cmd3 u m == {(s,s'). s' = s(u:=0,m:=4) & s m = 3}"
+  cmd2V :: "(state*state) set"
+    "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}"
 
-  (*Put pv=1 for u's program and pv=0 for v's program*)
-  cmd4 :: "[nat,pvar] => (state*state) set"
-    "cmd4 pv m == {(s,s'). s' = s(PP:=pv,m:=0) & s m = 4}"
+  cmd3V :: "(state*state) set"
+    "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}"
+
+  cmd4V :: "(state*state) set"
+    "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}"
 
   mutex :: "(state*state) set set"
     "mutex == {id,
-	       cmd0 UU MM, cmd0 VV NN,
-	       cmd1u, cmd1v,
-	       cmd2 0 MM, cmd2 1 NN,
-	       cmd3 UU MM, cmd3 VV NN,
-	       cmd4 1 MM, cmd4 0 NN}"
+	       cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, 
+	       cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}"
+
+  (** The correct invariants **)
+
+  invariantU :: "state set"
+    "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
+		       (MM s = 3 --> ~ PP s)}"
+
+  invariantV :: "state set"
+    "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) &
+		       (NN s = 3 --> PP s)}"
+
+  (** The faulty invariant (for U alone) **)
+
+  bad_invariantU :: "state set"
+    "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) &
+		           (3 <= MM s & MM s <= 4 --> ~ PP s)}"
 
   MInit :: "state set"
-    "MInit == {s. s PP < 2 & s UU = 0 & s VV = 0 & s MM = 0 & s NN = 0}"
-
-  boolVars :: "state set"
-    "boolVars == {s. s PP<2 & s UU < 2 & s VV < 2}"
-
-  (*Put pv=0 for u's program and pv=1 for v's program*)
-  invariant :: "[nat,pvar,pvar] => state set"
-    "invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
-			     (s m = 3 --> s PP = pv)}"
-
-  bad_invariant :: "[nat,pvar,pvar] => state set"
-    "bad_invariant pv u m == {s. ((s u=1) = (1 <= s m & s m <= 3)) &
-			         (3 <= s m & s m <= 4 --> s PP = pv)}"
-
-
-  
+    "MInit == {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}"
 
 end
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Network.ML
--- a/src/HOL/UNITY/Network.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Network.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,8 +8,6 @@
 From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
 *)
 
-open Network;
-
 val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = 
 Goalw [stable_def]
    "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -7,8 +7,6 @@
 	[ this example took only four days!]
 *)
 
-open Reach;
-
 (*TO SIMPDATA.ML??  FOR CLASET??  *)
 val major::prems = goal thy 
     "[| if P then Q else R;    \
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Reach.thy
--- a/src/HOL/UNITY/Reach.thy	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy	Fri Jul 31 18:46:55 1998 +0200
@@ -6,7 +6,7 @@
 Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
 *)
 
-Reach = Update + FP + Traces + SubstAx +
+Reach = FP + Traces + SubstAx +
 
 types   vertex
         state = "vertex=>bool"
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,8 +8,6 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-open SubstAx;
-
 (*constrains Acts B B' ==> constrains Acts (reachable(Init,Acts) Int B)
                                            (reachable(Init,Acts) Int B') *)
 bind_thm ("constrains_reachable",
@@ -24,9 +22,9 @@
 qed "leadsTo_imp_LeadsTo";
 
 Goal "[| constrains Acts (reachable(Init,Acts) Int (A - A'))   \
-\                               (A Un A'); \
-\               transient  Acts (reachable(Init,Acts) Int (A-A')) |]   \
-\           ==> LeadsTo(Init,Acts) A A'";
+\                         (A Un A'); \
+\         transient  Acts (reachable(Init,Acts) Int (A-A')) |]   \
+\     ==> LeadsTo(Init,Acts) A A'";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
 by (assume_tac 2);
@@ -36,7 +34,7 @@
 qed "LeadsTo_Basis";
 
 Goal "[| LeadsTo(Init,Acts) A B;  LeadsTo(Init,Acts) B C |] \
-\            ==> LeadsTo(Init,Acts) A C";
+\      ==> LeadsTo(Init,Acts) A C";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
 qed "LeadsTo_Trans";
@@ -75,15 +73,14 @@
 qed "LeadsTo_UN";
 
 (*Binary union introduction rule*)
-Goal
-  "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
+Goal "[| LeadsTo(Init,Acts) A C; LeadsTo(Init,Acts) B C |] ==> LeadsTo(Init,Acts) (A Un B) C";
 by (stac Un_eq_Union 1);
 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
 qed "LeadsTo_Un";
 
 
 Goal "[| reachable(Init,Acts) Int A <= B;  id: Acts |] \
-\            ==> LeadsTo(Init,Acts) A B";
+\     ==> LeadsTo(Init,Acts) A B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "Int_subset_imp_LeadsTo";
@@ -97,55 +94,51 @@
 Addsimps [empty_LeadsTo];
 
 Goal "[| reachable(Init,Acts) Int A = {};  id: Acts |] \
-\            ==> LeadsTo(Init,Acts) A B";
+\     ==> LeadsTo(Init,Acts) A B";
 by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
 qed "Int_empty_LeadsTo";
 
 
 Goal "[| LeadsTo(Init,Acts) A A';   \
-\                reachable(Init,Acts) Int A' <= B' |] \
-\             ==> LeadsTo(Init,Acts) A B'";
+\        reachable(Init,Acts) Int A' <= B' |] \
+\     ==> LeadsTo(Init,Acts) 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(Init,Acts) A A'; \
-\                reachable(Init,Acts) Int B <= A; id: Acts |]  \
-\             ==> LeadsTo(Init,Acts) B A'";
+\        reachable(Init,Acts) Int B <= A; id: Acts |]  \
+\     ==> LeadsTo(Init,Acts) B A'";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
 qed_spec_mp "LeadsTo_weaken_L";
 
 
 (*Distributes over binary unions*)
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       LeadsTo(Init,Acts) (A Un B) C  =  \
 \       (LeadsTo(Init,Acts) A C & LeadsTo(Init,Acts) B C)";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Un_distrib";
 
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       LeadsTo(Init,Acts) (UN i:I. A i) B  =  \
 \       (ALL i : I. LeadsTo(Init,Acts) (A i) B)";
 by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_UN_distrib";
 
-Goal
-  "id: Acts ==> \
+Goal "id: Acts ==> \
 \       LeadsTo(Init,Acts) (Union S) B  =  \
 \       (ALL A : S. LeadsTo(Init,Acts) A B)";
 by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
 qed "LeadsTo_Union_distrib";
 
 
-Goal 
-   "[| LeadsTo(Init,Acts) A A'; id: Acts;   \
-\               reachable(Init,Acts) Int B  <= A;     \
-\               reachable(Init,Acts) Int A' <= B' |] \
-\           ==> LeadsTo(Init,Acts) B B'";
+Goal "[| LeadsTo(Init,Acts) A A'; id: Acts;   \
+\        reachable(Init,Acts) Int B  <= A;     \
+\        reachable(Init,Acts) Int A' <= B' |] \
+\     ==> LeadsTo(Init,Acts) B B'";
 (*PROOF FAILED: why?*)
 by (blast_tac (claset() addIs [LeadsTo_Trans, LeadsTo_weaken_R,
 			       LeadsTo_weaken_L]) 1);
@@ -153,8 +146,7 @@
 
 
 (*Set difference: maybe combine with leadsTo_weaken_L??*)
-Goal
-  "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) (A-B) C; LeadsTo(Init,Acts) B C; id: Acts |] \
 \       ==> LeadsTo(Init,Acts) A C";
 by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
 qed "LeadsTo_Diff";
@@ -181,8 +173,7 @@
 qed "LeadsTo_UN_UN_noindex";
 
 (*Version with no index set*)
-Goal
-   "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
+Goal "ALL i. LeadsTo(Init,Acts) (A i) (A' i) \
 \           ==> LeadsTo(Init,Acts) (UN i. A i) (UN i. A' i)";
 by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
 qed "all_LeadsTo_UN_UN";
@@ -198,31 +189,27 @@
 
 (** The cancellation law **)
 
-Goal
-   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
+Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) B B'; \
 \              id: Acts |]    \
 \           ==> LeadsTo(Init,Acts) A (A' Un B')";
 by (blast_tac (claset() addIs [LeadsTo_Un_Un, 
 			       subset_imp_LeadsTo, LeadsTo_Trans]) 1);
 qed "LeadsTo_cancel2";
 
-Goal
-   "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (A' Un B); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
 \           ==> LeadsTo(Init,Acts) A (A' Un B')";
 by (rtac LeadsTo_cancel2 1);
 by (assume_tac 2);
 by (ALLGOALS Asm_simp_tac);
 qed "LeadsTo_cancel_Diff2";
 
-Goal
-   "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) B B'; id: Acts |] \
 \           ==> LeadsTo(Init,Acts) 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(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A (B Un A'); LeadsTo(Init,Acts) (B-A') B'; id: Acts |] \
 \           ==> LeadsTo(Init,Acts) A (B' Un A')";
 by (rtac LeadsTo_cancel1 1);
 by (assume_tac 2);
@@ -263,8 +250,7 @@
 by (ALLGOALS Blast_tac);
 qed "R_PSP";
 
-Goal
-   "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
+Goal "[| LeadsTo(Init,Acts) A A'; constrains Acts B B'; id: Acts |] \
 \           ==> LeadsTo(Init,Acts) (B Int A) ((B Int A') Un (B' - B))";
 by (asm_simp_tac (simpset() addsimps (R_PSP::Int_ac)) 1);
 qed "R_PSP2";
@@ -285,8 +271,7 @@
 (*** Induction rules ***)
 
 (** Meta or object quantifier ????? **)
-Goal
-   "[| wf r;     \
+Goal "[| wf r;     \
 \              ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
 \                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
 \              id: Acts |] \
@@ -298,12 +283,11 @@
 qed "LeadsTo_wf_induct";
 
 
-Goal
-   "[| wf r;     \
-\              ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m})                   \
-\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
-\              id: Acts |] \
-\           ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
+Goal "[| wf r;     \
+\        ALL m:I. LeadsTo(Init,Acts) (A Int f-``{m})                   \
+\                                    ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\        id: Acts |] \
+\     ==> LeadsTo(Init,Acts) A ((A - (f-``I)) Un B)";
 by (etac LeadsTo_wf_induct 1);
 by Safe_tac;
 by (case_tac "m:I" 1);
@@ -312,18 +296,16 @@
 qed "R_bounded_induct";
 
 
-Goal
-   "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
+Goal "[| ALL m. LeadsTo(Init,Acts) (A Int f-``{m})                     \
 \                                  ((A Int f-``(lessThan m)) Un B);   \
-\              id: Acts |] \
-\           ==> LeadsTo(Init,Acts) A B";
+\        id: Acts |] \
+\     ==> LeadsTo(Init,Acts) 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";
 
-Goal
-   "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
+Goal "[| ALL m:(greaterThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
 \                                        ((A Int f-``(lessThan m)) Un B);   \
 \              id: Acts |] \
 \           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atMost l))) Un B)";
@@ -333,11 +315,10 @@
 by (Asm_simp_tac 1);
 qed "R_lessThan_bounded_induct";
 
-Goal
-   "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
-\                                    ((A Int f-``(greaterThan m)) Un B);   \
-\              id: Acts |] \
-\           ==> LeadsTo(Init,Acts) A ((A Int (f-``(atLeast l))) Un B)";
+Goal "[| ALL m:(lessThan l). LeadsTo(Init,Acts) (A Int f-``{m})   \
+\                              ((A Int f-``(greaterThan m)) Un B);   \
+\        id: Acts |] \
+\     ==> LeadsTo(Init,Acts) 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);
 by (assume_tac 2);
@@ -352,10 +333,9 @@
 
 (*** Completion: Binary and General Finite versions ***)
 
-Goal
-   "[| LeadsTo(Init,Acts) A A';  stable Acts A';   \
-\              LeadsTo(Init,Acts) B B';  stable Acts B';  id: Acts |] \
-\           ==> LeadsTo(Init,Acts) (A Int B) (A' Int B')";
+Goal "[| LeadsTo(Init,Acts) A A';  stable Acts A';   \
+\        LeadsTo(Init,Acts) B B';  stable Acts B';  id: Acts |] \
+\     ==> LeadsTo(Init,Acts) (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);
@@ -363,9 +343,9 @@
 
 
 Goal "[| finite I;  id: Acts |]                     \
-\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) -->  \
-\               (ALL i:I. stable Acts (A' i)) -->         \
-\               LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
+\     ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i)) -->  \
+\         (ALL i:I. stable Acts (A' i)) -->         \
+\         LeadsTo(Init,Acts) (INT i:I. A i) (INT i:I. A' i)";
 by (etac finite_induct 1);
 by (Asm_simp_tac 1);
 by (asm_simp_tac 
@@ -374,12 +354,10 @@
 qed_spec_mp "R_finite_stable_completion";
 
 
-Goal
- "[| LeadsTo(Init,Acts) A (A' Un C);  constrains Acts A' (A' Un C); \
-\            LeadsTo(Init,Acts) B (B' Un C);  constrains Acts B' (B' Un C); \
-\            id: Acts |] \
-\         ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
-
+Goal "[| LeadsTo(Init,Acts) A (A' Un C);  constrains Acts A' (A' Un C); \
+\        LeadsTo(Init,Acts) B (B' Un C);  constrains Acts B' (B' Un C); \
+\        id: Acts |] \
+\     ==> LeadsTo(Init,Acts) (A Int B) ((A' Int B') Un C)";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
 by (dtac completion 1);
 by (assume_tac 2);
@@ -390,11 +368,10 @@
 qed "R_completion";
 
 
-Goal
-   "[| finite I;  id: Acts |] \
-\           ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) -->  \
-\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
-\               LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
+Goal "[| finite I;  id: Acts |] \
+\     ==> (ALL i:I. LeadsTo(Init,Acts) (A i) (A' i Un C)) -->  \
+\         (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
+\         LeadsTo(Init,Acts) (INT i:I. A i) ((INT i:I. A' i) Un C)";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
@@ -402,3 +379,29 @@
 by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
 qed "R_finite_completion";
 
+
+
+(*** Specialized laws for handling invariants ***)
+
+Goalw [transient_def]
+    "[| reachable(Init,Acts) <= INV;  transient Acts (INV Int A) |]  \
+\    ==> transient Acts (reachable(Init,Acts) Int A)";
+by (Clarify_tac 1);
+by (rtac bexI 1); 
+by (assume_tac 2);
+by (Blast_tac 1);
+qed "reachable_transient";
+
+(*Eliminates the set "reachable (Init,Acts)" from the subgoals.  This boosts
+  efficiency because the term contains a full copy of the program.*)
+Goal "[| reachable (Init,Acts) <= INV;      \
+\        constrains Acts (INV Int (A - A')) (A Un A'); \
+\        transient  Acts (INV Int (A-A')) |]   \
+\     ==> LeadsTo(Init,Acts) A A'";
+by (rtac LeadsTo_Basis 1);
+by (blast_tac (claset() addSIs [reachable_transient]) 2);
+by (rewtac constrains_def);
+by (Blast_tac 1);
+qed "reachable_LeadsTo_Basis";
+
+
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Token.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,11 +8,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
 *)
 
-
-open Token;
-
-
-val Token_defs = [WellTyped_def, Token_def, HasTok_def, H_def, E_def, T_def];
+val Token_defs = [HasTok_def, H_def, E_def, T_def];
 
 AddIffs [N_positive, skip];
 
@@ -20,33 +16,14 @@
 by Auto_tac;
 qed "HasToK_partition";
 
-Goalw Token_defs "s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
 by (Simp_tac 1);
-by (exhaust_tac "s (Suc i)" 1);
+by (exhaust_tac "proc s i" 1);
 by Auto_tac;
 qed "not_E_eq";
 
-(** We should be able to prove WellTyped as a separate Invariant.  Then
-    the Invariant rule should let us assume that the initial
-    state is reachable, and therefore contained in any Invariant.  Then
-    we'd not have to mention WellTyped in the statement of this theorem.
-**)
-
-Goalw [stable_def]
-    "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
-by (rtac (stable_WT RS stable_constrains_Int) 1);
-by (cut_facts_tac [TR2,TR4,TR5] 1);
-by (asm_full_simp_tac (simpset() addsimps [constrains_def]) 1);
-by (REPEAT_FIRST (rtac ballI ORELSE' (dtac bspec THEN' assume_tac)));
-by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
-by (case_tac "xa : HasTok i" 1);
-by (auto_tac (claset(), simpset() addsimps [H_def, E_def, T_def]));
-qed "token_stable";
-
 (*This proof is in the "massaging" style and is much faster! *)
-Goalw [stable_def]
-    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
-by (rtac (stable_WT RS stable_constrains_Int) 1);
+Goalw [stable_def] "stable Acts (Compl(E i) Un (HasTok i))";
 by (rtac constrains_weaken 1);
 by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
 by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
@@ -99,9 +76,8 @@
 
 (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
-Goal
- "[| i<N; j<N |] ==> \
-\      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
+Goal "[| i<N; j<N |] ==>   \
+\     leadsTo Acts (HasTok i) ({s. (token s, i) : nodeOrder j} Un HasTok j)";
 by (case_tac "i=j" 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 by (rtac (TR7 RS leadsTo_weaken_R) 1);
@@ -111,27 +87,25 @@
 
 
 (*Chapter 4 variant, the one actually used below.*)
-Goal
- "[| i<N; j<N; i~=j |] ==> \
-\      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
+Goal "[| i<N; j<N; i~=j |]    \
+\     ==> leadsTo Acts (HasTok i) {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);
 qed "TR7_aux";
 
-Goal "({s. Token s < N} Int Token -`` {m}) = \
-\         (if m<N then Token -`` {m} else {})";
+Goal "({s. token s < N} Int token -`` {m}) = \
+\     (if m<N then token -`` {m} else {})";
 by Auto_tac;
-val Token_lemma = result();
+val token_lemma = result();
 
 
 (*Misra's TR9: the token reaches an arbitrary node*)
-Goal
- "j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
+Goal "j<N ==> leadsTo Acts {s. token s < N} (HasTok j)";
 by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
+by (res_inst_tac [("I", "Compl{j}"), ("f", "token"), ("B", "{}")]
      (wf_nodeOrder RS bounded_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
 						HasTok_def])));
 by (Blast_tac 2);
 by (Clarify_tac 1);
@@ -141,10 +115,10 @@
 qed "leadsTo_j";
 
 (*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+Goal "j<N ==> leadsTo Acts ({s. token s < N} Int H j) (E j)";
 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 (ALLGOALS Blast_tac);
-qed "Token_progress";
+qed "token_progress";
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Token.thy
--- a/src/HOL/UNITY/Token.thy	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Token.thy	Fri Jul 31 18:46:55 1998 +0200
@@ -12,9 +12,11 @@
 Token = WFair +
 
 (*process states*)
-datatype pstate = Hungry | Eating | Thinking | Pnum nat
+datatype pstate = Hungry | Eating | Thinking
 
-types state = nat => pstate
+record state =
+  token :: nat
+  proc  :: nat => pstate
 
 consts
   N :: nat	(*number of nodes in the ring*)
@@ -27,33 +29,21 @@
   next      :: nat => nat
     "next i == (Suc i) mod N"
 
-  WellTyped :: state set
-    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"
-
-  Token :: state => nat
-    "Token s == case s 0 of 
-                    Hungry => 0
-                  | Eating => 0
-                  | Thinking => 0
-                  | Pnum i => i"
-
   HasTok :: nat => state set
-    "HasTok i == Token -`` {i}"
+    "HasTok i == {s. token s = i}"
 
   H :: nat => state set
-    "H i == {s. s (Suc i) = Hungry}"
+    "H i == {s. proc s i = Hungry}"
 
   E :: nat => state set
-    "E i == {s. s (Suc i) = Eating}"
+    "E i == {s. proc s i = Eating}"
 
   T :: nat => state set
-    "T i == {s. s (Suc i) = Thinking}"
+    "T i == {s. proc s i = Thinking}"
 
 rules
   N_positive "0<N"
 
-  stable_WT  "stable Acts WellTyped"
-
   skip "id: Acts"
 
   TR2  "constrains Acts (T i) (T i Un H i)"
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -9,9 +9,6 @@
 
 *)
 
-open Traces;
-
-
 (****
 Now simulate the inductive definition (illegal due to paired arguments)
 
@@ -38,7 +35,7 @@
 \     ==> (s,s'): act --> s' : reachable(Init,Acts)";
 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1);
 by (etac exE 1);
-be traces.induct 1;
+by (etac traces.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS (blast_tac (claset() addIs traces.intrs)));
 qed_spec_mp "reachable_Acts";
@@ -54,7 +51,7 @@
 \  ==> P za";
 by (cut_facts_tac [major] 1);
 by Auto_tac;
-be traces.induct 1;
+by (etac traces.induct 1);
 by (ALLGOALS (blast_tac (claset() addIs prems)));
 qed "reachable_induct";
 
@@ -71,7 +68,7 @@
 Goalw [stable_def, constrains_def]
     "[| Init<=A;  stable Acts A |] ==> reachable(Init,Acts) <= A";
 by (rtac subsetI 1);
-be reachable.induct 1;
+by (etac reachable.induct 1);
 by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
 qed "strongest_invariant";
 
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -12,49 +12,6 @@
 HOL_quantifiers := false;
 
 
-(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
-
-(** Rewrites rules to eliminate A.  Conditions can be satisfied by letting B
-    be any set including A Int C and contained in A Un C, such as B=A or B=C.
-**)
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\              ==> (A Int B) Un (Compl A Int C) = B Un C";
-by (Blast_tac 1);
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\              ==> (A Un B) Int (Compl A Un C) = B Int C";
-by (Blast_tac 1);
-
-(*The base B=A*)
-Goal "A Un (Compl A Int C) = A Un C";
-by (Blast_tac 1);
-
-Goal "A Int (Compl A Un C) = A Int C";
-by (Blast_tac 1);
-
-(*The base B=C*)
-Goal "(A Int C) Un (Compl A Int C) = C";
-by (Blast_tac 1);
-
-Goal "(A Un C) Int (Compl A Un C) = C";
-by (Blast_tac 1);
-
-
-(** More ad-hoc rules **)
-
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-
-Goal "A Int (B - C) Un C = A Int B Un C";
-by (Blast_tac 1);
-qed "Int_Diff_Un";
-
-
-open UNITY;
-
-
 (*** constrains ***)
 
 val prems = goalw thy [constrains_def]
diff -r 2a454140ae24 -r e5a7cdd07ea5 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Fri Jul 31 18:46:28 1998 +0200
+++ b/src/HOL/UNITY/WFair.ML	Fri Jul 31 18:46:55 1998 +0200
@@ -8,12 +8,6 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-open WFair;
-
-Goal "Union(B) Int A = Union((%C. C Int A)``B)";
-by (Blast_tac 1);
-qed "Int_Union_Union";
-
 
 (*** transient ***)
 
@@ -121,7 +115,7 @@
 \              ==> P A C; \
 \     !!B S. ALL A:S. leadsTo Acts A B & P A B ==> P (Union S) B \
 \  |] ==> P za zb";
-br (major RS leadsto.induct) 1;
+by (rtac (major RS leadsto.induct) 1);
 by (REPEAT (blast_tac (claset() addIs prems) 1));
 qed "leadsTo_induct";