# HG changeset patch
# User paulson
# Date 891599673 -7200
# Node ID 1f9362e769c190e25e04b41a53a83a49c67aeec1
# Parent  66b1a7c42d9495f347539b419955f659f62edbd0
New UNITY theory

diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Channel.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Channel.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,67 @@
+(*  Title:      HOL/UNITY/Channel
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+open Channel;
+
+AddIffs [skip];
+
+
+(*None represents "infinity" while Some represents proper integers*)
+goalw thy [minSet_def] "!!A. minSet A = Some x --> x : A";
+by (Simp_tac 1);
+by (fast_tac (claset() addIs [LeastI]) 1);
+qed_spec_mp "minSet_eq_SomeD";
+
+goalw thy [minSet_def] " minSet{} = None";
+by (Asm_simp_tac 1);
+qed_spec_mp "minSet_empty";
+Addsimps [minSet_empty];
+
+goalw thy [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+qed_spec_mp "minSet_nonempty";
+
+goal thy
+    "leadsTo Acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
+by (rtac leadsTo_weaken 1);
+by (rtac ([UC2, UC1] MRS PSP) 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by Safe_tac;
+by (auto_tac (claset() addDs [minSet_eq_SomeD], 
+	      simpset() addsimps [le_def, nat_neq_iff]));
+qed "minSet_greaterThan";
+
+
+(*The induction*)
+goal thy "leadsTo Acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
+by (rtac leadsTo_weaken_R 1);
+by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
+     greaterThan_bounded_induct 1);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+by (dtac minSet_nonempty 2);
+by (Asm_full_simp_tac 2);
+by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
+by Safe_tac;
+by (ALLGOALS Asm_full_simp_tac);
+by (dtac minSet_nonempty 1);
+by (Asm_full_simp_tac 1);
+val lemma = result();
+
+
+goal thy "!!y::nat. leadsTo Acts (UNIV-{{}}) {s. y ~: s}";
+by (rtac (lemma RS leadsTo_weaken_R) 1);
+by (Clarify_tac 1);
+by (forward_tac [minSet_nonempty] 1);
+by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
+by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
+qed "Channel_progress";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Channel.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Channel.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,29 @@
+(*  Title:      HOL/UNITY/Channel
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+Channel = WFair + Option + 
+
+types state = nat set
+
+constdefs
+  minSet :: nat set => nat option
+    "minSet A == if A={} then None else Some (LEAST x. x:A)"
+
+rules
+
+  skip "id: Acts"
+
+  UC1  "constrains Acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
+
+  (*  UC1  "constrains Acts {s. minSet s = x} {s. x <= minSet s}"  *)
+
+  UC2  "leadsTo Acts (minSet -`` {Some x}) {s. x ~: s}"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Common.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Common.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,102 @@
+(*  Title:      HOL/UNITY/Common
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+
+open Common;
+
+(*Misra's property CMT4: t exceeds no common meeting time*)
+goal thy
+  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\           ==> stable Acts (atMost n)";
+by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
+			 constrains_def, le_max_iff_disj]) 1);
+by (Clarify_tac 1);
+by (dtac bspec 1);
+by (assume_tac 1);
+by (blast_tac (claset() addSEs [subsetCE]
+			addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
+qed "common_stable";
+
+goal thy
+  "!!Acts. [| ALL m. constrains Acts {m} (maxfg m); n: common |] \
+\           ==> reachable {0} Acts <= atMost n";
+by (rtac strongest_invariant 1);
+by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
+by (simp_tac (simpset() addsimps [atMost_def]) 1);
+qed "common_invariant";
+
+
+(*** Some programs that implement the safety property above ***)
+
+(*This one is just Skip*)
+goal thy "constrains {id} {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
+				  fasc, gasc]) 1);
+result();
+
+(*This one is  t := ftime t || t := gtime t    really needs Skip too*)
+goal thy "constrains {range(%t.(t,ftime t)), range(%t.(t,gtime t))} \
+\                    {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
+				  le_max_iff_disj]) 1);
+by (Blast_tac 1);
+result();
+
+(*This one is  t := max (ftime t) (gtime t)    really needs Skip too*)
+goal thy "constrains {range(%t.(t, max (ftime t) (gtime t)))} \
+\                    {m} (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def]) 1);
+by (Blast_tac 1);
+result();
+
+(*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
+goalw thy [constrains_def, maxfg_def] 
+    "constrains { {(t, Suc t) | t. t < max (ftime t) (gtime t)} } \
+\               {m} (maxfg m)";
+by (blast_tac (claset() addIs [Suc_leI]) 1);
+result();
+
+
+(*It remans to prove that they satisfy CMT3': t does not decrease,
+  and that CMT3' implies that t stops changing once common(t) holds.*)
+
+
+(*** Progress under weak fairness ***)
+
+Addsimps [atMost_Int_atLeast];
+
+goal thy
+    "!!Acts. [| 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";
+by (rtac leadsTo_weaken_R 1);
+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] 
+                        addIs [common_stable, leadsTo_weaken_R]) 1);
+val lemma = result();
+
+(*The "ALL m: Compl common" form echoes CMT6.*)
+goal thy
+    "!!Acts. [| 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";
+by (rtac lemma 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac LeastI 2);
+by (blast_tac (claset() addSDs [not_less_Least]) 1);
+qed "leadsTo_common";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Common.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Common.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,32 @@
+(*  Title:      HOL/UNITY/Common
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+Common = WFair +
+
+consts
+  ftime,gtime :: nat=>nat
+
+rules
+  fmono "m <= n ==> ftime m <= ftime n"
+  gmono "m <= n ==> gtime m <= gtime n"
+
+  fasc  "m <= ftime n"
+  gasc  "m <= gtime n"
+
+constdefs
+  common :: nat set
+    "common == {n. ftime n = n & gtime n = n}"
+
+  maxfg :: nat => nat set
+    "maxfg m == {t. t <= max (ftime m) (gtime m)}"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Deadlock.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Deadlock.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,90 @@
+
+
+(*** Deadlock examples from section 5.6 ***)
+
+(*Trivial, two-process case*)
+goalw thy [constrains_def, stable_def]
+    "!!Acts. [| constrains Acts (A Int B) A;  constrains Acts (B Int A) B |] \
+\           ==> stable Acts (A Int B)";
+by (Blast_tac 1);
+result();
+
+
+goal thy "{i. i < Suc n} = insert n {i. i < n}";
+by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
+qed "Collect_less_Suc_insert";
+
+
+goal thy "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
+by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
+qed "Collect_le_Suc_insert";
+
+
+(*a simplification step*)
+goal thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
+\         (INT i:{i. i <= Suc n}. A i)";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
+by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
+qed "Collect_le_Int_equals";
+
+
+(*Dual of the required property.  Converse inclusion fails.*)
+goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <=  \
+\         (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
+by (Blast_tac 1);
+qed "UN_Int_Compl_subset";
+
+
+(*Converse inclusion fails.*)
+goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i))  <= \
+\         (INT i:{i. i < n}. Compl(A i)) Un A n";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [Collect_less_Suc_insert]) 1);
+by (Blast_tac 1);
+qed "INT_Un_Compl_subset";
+
+
+(*Specialized rewriting*)
+goal thy "A 0 Int (Compl (A n) Int \
+\                  (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}";
+by (blast_tac (claset() addIs [gr0I]
+		        addDs [impOfSubs INT_Un_Compl_subset]) 1);
+val lemma = result();
+
+(*Reverse direction makes it harder to invoke the ind hyp*)
+goal thy "(INT i:{i. i <= n}. A i) = \
+\         A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac
+    (simpset() addsimps (Int_ac @
+			 [Int_Un_distrib, Int_Un_distrib2, lemma,
+			  Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
+qed "INT_le_equals_Int";
+
+goal thy "(INT i:{i. i <= Suc n}. A i) = \
+\         A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
+by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym, 
+				  INT_le_equals_Int]) 1);
+qed "INT_le_Suc_equals_Int";
+
+
+(*The final deadlock example*)
+val [zeroprem, allprem] = goalw thy [stable_def]
+    "[| constrains Acts (A 0 Int A (Suc n)) (A 0);  \
+\       ALL i:{i. i <= n}. constrains Acts (A(Suc i) Int A i) \
+\                                         (Compl(A i) Un A(Suc i)) |] \
+\    ==> stable Acts (INT i:{i. i <= Suc n}. A i)";
+
+by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
+    constrains_Int RS constrains_weaken) 1);
+by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
+				  Int_assoc, INT_absorb]) 1);
+by (simp_tac (simpset() addsimps ([INT_le_Suc_equals_Int])) 1);
+result();
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Deadlock.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Deadlock.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,1 @@
+Deadlock = UNITY
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/FP.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/FP.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,66 @@
+(*  Title:      HOL/UNITY/FP
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+goal thy "Union(B) Int A = (UN C:B. C Int A)";
+by (Blast_tac 1);
+qed "Int_Union2";
+
+open FP;
+
+goalw thy [FP_Orig_def, stable_def] "stable Acts (FP_Orig Acts Int B)";
+by (stac Int_Union2 1);
+by (rtac ball_constrains_UN 1);
+by (Simp_tac 1);
+qed "stable_FP_Orig_Int";
+
+
+val prems = goalw thy [FP_Orig_def, stable_def]
+    "(!!B. stable Acts (A Int B)) ==> A <= FP_Orig Acts";
+by (blast_tac (claset() addIs prems) 1);
+qed "FP_Orig_weakest";
+
+
+goal thy "stable Acts (FP Acts Int B)";
+by (subgoal_tac "FP Acts Int B = (UN x:B. FP Acts Int {x})" 1);
+by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [Int_insert_right]) 1);
+by (rewrite_goals_tac [FP_def, stable_def]);
+by (rtac ball_constrains_UN 1);
+by (Simp_tac 1);
+qed "stable_FP_Int";
+
+goal thy "FP Acts <= FP_Orig Acts";
+by (rtac (stable_FP_Int RS FP_Orig_weakest) 1);
+val lemma1 = result();
+
+goalw thy [FP_Orig_def, FP_def] "FP_Orig Acts <= FP Acts";
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "{x}")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [Int_insert_right]) 1);
+val lemma2 = result();
+
+goal thy "FP Acts = FP_Orig Acts";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+qed "FP_equivalence";
+
+val [prem] = goal thy
+    "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
+by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
+qed "FP_weakest";
+
+goalw thy [FP_def, stable_def, constrains_def]
+    "Compl (FP Acts) = (UN act:Acts. Compl{s. act^^{s} <= {s}})";
+by (Blast_tac 1);
+qed "Compl_FP";
+
+goal thy "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
+by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
+qed "Diff_FP";
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/FP.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/FP.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/UNITY/FP
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Fixed Point of a Program
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+FP = UNITY +
+
+constdefs
+
+  FP_Orig :: "('a * 'a)set set => 'a set"
+    "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
+
+  FP :: "('a * 'a)set set => 'a set"
+    "FP Acts == {s. stable Acts {s}}"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/LessThan.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/LessThan.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,146 @@
+(*  Title:      HOL/LessThan/LessThan
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+lessThan, greaterThan, atLeast, atMost
+*)
+
+
+open LessThan;
+
+
+(*** lessThan ***)
+
+goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
+by (Blast_tac 1);
+qed "lessThan_iff";
+AddIffs [lessThan_iff];
+
+goalw thy [lessThan_def] "lessThan 0 = {}";
+by (Simp_tac 1);
+qed "lessThan_0";
+Addsimps [lessThan_0];
+
+goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
+by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+by (Blast_tac 1);
+qed "lessThan_Suc";
+
+goal thy "(UN m. lessThan m) = UNIV";
+by (Blast_tac 1);
+qed "UN_lessThan_UNIV";
+
+goalw thy [lessThan_def, atLeast_def, le_def]
+    "Compl(lessThan k) = atLeast k";
+by (Blast_tac 1);
+qed "Compl_lessThan";
+
+
+(*** greaterThan ***)
+
+goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
+by (Blast_tac 1);
+qed "greaterThan_iff";
+AddIffs [greaterThan_iff];
+
+goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
+by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
+qed "greaterThan_0";
+Addsimps [greaterThan_0];
+
+goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
+by Safe_tac;
+by (blast_tac (claset() addIs [less_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
+qed "greaterThan_Suc";
+
+goal thy "(INT m. greaterThan m) = {}";
+by (Blast_tac 1);
+qed "INT_greaterThan_UNIV";
+
+goalw thy [greaterThan_def, atMost_def, le_def]
+    "Compl(greaterThan k) = atMost k";
+by (Blast_tac 1);
+qed "Compl_greaterThan";
+
+goalw thy [greaterThan_def, atMost_def, le_def]
+    "Compl(atMost k) = greaterThan k";
+by (Blast_tac 1);
+qed "Compl_atMost";
+
+goal thy "less_than ^^ {k} = greaterThan k";
+by (Blast_tac 1);
+qed "Image_less_than";
+
+Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
+
+(*** atLeast ***)
+
+goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
+by (Blast_tac 1);
+qed "atLeast_iff";
+AddIffs [atLeast_iff];
+
+goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
+by (Simp_tac 1);
+qed "atLeast_0";
+Addsimps [atLeast_0];
+
+goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
+by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
+by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (Blast_tac 1);
+qed "atLeast_Suc";
+
+goal thy "(UN m. atLeast m) = UNIV";
+by (Blast_tac 1);
+qed "UN_atLeast_UNIV";
+
+goalw thy [lessThan_def, atLeast_def, le_def]
+    "Compl(atLeast k) = lessThan k";
+by (Blast_tac 1);
+qed "Compl_atLeast";
+
+goal thy "less_than^-1 ^^ {k} = lessThan k";
+by (Blast_tac 1);
+qed "Image_inverse_less_than";
+
+Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
+
+(*** atMost ***)
+
+goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
+by (Blast_tac 1);
+qed "atMost_iff";
+AddIffs [atMost_iff];
+
+goalw thy [atMost_def] "atMost 0 = {0}";
+by (Simp_tac 1);
+qed "atMost_0";
+Addsimps [atMost_0];
+
+goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
+by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
+by (Blast_tac 1);
+qed "atMost_Suc";
+
+goal thy "(UN m. atMost m) = UNIV";
+by (Blast_tac 1);
+qed "UN_atMost_UNIV";
+
+goalw thy [atMost_def, le_def]
+    "Compl(atMost k) = greaterThan k";
+by (Blast_tac 1);
+qed "Compl_atMost";
+Addsimps [Compl_atMost];
+
+
+(*** Combined properties ***)
+
+goal thy "atMost n Int atLeast n = {n}";
+by (blast_tac (claset() addIs [le_anti_sym]) 1);
+qed "atMost_Int_atLeast";
+
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/LessThan.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/LessThan.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/UNITY/LessThan
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+lessThan, greaterThan, atLeast, atMost
+*)
+
+LessThan = List +
+
+constdefs
+
+  lessThan   :: "nat => nat set"
+     "lessThan n == {i. i<n}"
+
+  atMost   :: "nat => nat set"
+     "atMost n == {i. i<=n}"
+ 
+  greaterThan   :: "nat => nat set"
+     "greaterThan n == {i. n<i}"
+
+  atLeast   :: "nat => nat set"
+     "atLeast n == {i. n<=i}"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Mutex.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Mutex.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,254 @@
+(*  Title:      HOL/UNITY/Mutex.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+open Mutex;
+
+val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
+		cmd2_def, cmd3_def, cmd4_def];
+
+goalw thy [mutex_def] "id : mutex";
+by (Simp_tac 1);
+qed "id_in_mutex";
+AddIffs [id_in_mutex];
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+
+(*proves "constrains" properties when the program is specified*)
+val constrains_tac = 
+   SELECT_GOAL
+      (EVERY [rtac constrainsI 1,
+	      rewtac mutex_def,
+	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
+	      rewrite_goals_tac cmd_defs,
+	      ALLGOALS (SELECT_GOAL Auto_tac)]);
+
+
+(*proves "ensures" properties when the program is specified*)
+fun ensures_tac sact = 
+    SELECT_GOAL
+      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+	      res_inst_tac [("act", sact)] transient_mem 2,
+	      Simp_tac 2,
+	      constrains_tac 1,
+	      rewrite_goals_tac cmd_defs,
+	      Auto_tac]);
+
+
+(*The booleans p, u, v are always either 0 or 1*)
+goalw thy [stable_def, boolVars_def]
+    "stable mutex boolVars";
+by (constrains_tac 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+qed "stable_boolVars";
+
+goal thy "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 thy [stable_def, invariant_def]
+    "stable mutex (invariant 0 UU MM)";
+by (constrains_tac 1);
+qed "stable_invar_0um";
+
+goalw thy [stable_def, invariant_def]
+    "stable mutex (invariant 1 VV NN)";
+by (constrains_tac 1);
+qed "stable_invar_1vn";
+
+goalw thy [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
+by Auto_tac;
+qed "MInit_invar_0um";
+
+goalw thy [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
+by Auto_tac;
+qed "MInit_invar_1vn";
+
+(*The intersection is an invariant of the system*)
+goal thy "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
+by (simp_tac (simpset() addsimps
+	      [strongest_invariant, Int_greatest, stable_Int, 
+	       stable_invar_0um, stable_invar_1vn, 
+	       MInit_invar_0um,MInit_invar_1vn]) 1); 
+qed "reachable_subset_invariant";
+
+val reachable_subset_invariant' = 
+    rewrite_rule [invariant_def] reachable_subset_invariant;
+
+
+(*The safety property (mutual exclusion) follows from the claimed invar_s*)
+goalw thy [invariant_def]
+    "{s. s MM = 3 & s NN = 3} <= \
+\    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
+by Auto_tac;
+val lemma = result();
+
+goal thy "{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);
+qed "mutual_exclusion";
+
+
+(*The bad invariant FAILS in cmd1v*)
+goalw thy [stable_def, bad_invariant_def]
+    "stable mutex (bad_invariant 0 UU MM)";
+by (constrains_tac 1);
+by (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,
+  violating the invariant!*)
+(*Check that subgoals remain: proof failed.*)
+getgoal 1;  
+
+
+(*** Progress for U ***)
+
+goalw thy [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
+by (constrains_tac 1);
+qed "U_F0";
+
+goal thy "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);
+qed "U_F1";
+
+goal thy "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (ensures_tac "cmd2 0 MM" 1);
+qed "U_F2";
+
+goalw thy [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
+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);
+qed "U_F3";
+
+goal thy "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
+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 thy "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
+by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val lemma1 = result();
+
+
+goal thy "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
+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,
+				  lemma1, lemma2, U_F3] ) 1);
+val lemma123 = result();
+
+
+(*Misra's F4*)
+goal thy "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
+by (rtac LeadsTo_weaken_L 1);
+by (rtac lemma123 1);
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by Auto_tac;
+qed "u_leadsto_p";
+
+
+(*** Progress for V ***)
+
+
+goalw thy [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
+by (constrains_tac 1);
+qed "V_F0";
+
+goal thy "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);
+qed "V_F1";
+
+goal thy "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (ensures_tac "cmd2 1 NN" 1);
+qed "V_F2";
+
+goalw thy [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
+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);
+qed "V_F3";
+
+goal thy "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
+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 thy "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
+by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val lemma1 = result();
+
+
+goal thy "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
+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,
+				  lemma1, lemma2, V_F3] ) 1);
+val lemma123 = result();
+
+
+(*Misra's F4*)
+goal thy "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
+by (rtac LeadsTo_weaken_L 1);
+by (rtac lemma123 1);
+by (cut_facts_tac [reachable_subset_invariant'] 1);
+by Auto_tac;
+qed "v_leadsto_not_p";
+
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac LeadsTo_cancel2 1);
+by (rtac U_F2 2);
+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 (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 thy "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
+by (rtac LeadsTo_Un_duplicate 1);
+by (rtac LeadsTo_cancel2 1);
+by (rtac V_F2 2);
+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 (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 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Mutex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Mutex.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,74 @@
+(*  Title:      HOL/UNITY/Mutex.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+Mutex = Update + UNITY + Traces + SubstAx +
+
+(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
+syntax
+  "3"       :: nat                ("3")
+  "4"       :: nat                ("4")
+
+translations
+   "3"  == "Suc 2"
+   "4"  == "Suc 3"
+
+
+(*program variables*)
+datatype pvar = PP | MM | NN | UU | VV
+
+(*No booleans; instead True=1 and False=0*)
+types state = pvar => nat
+
+constdefs
+  cmd0 :: "[pvar,pvar] => (state*state) set"
+    "cmd0 u m == {(s,s'). s' = s[u|->1][m|->1] & s m = 0}"
+
+  cmd1u :: "(state*state) set"
+    "cmd1u == {(s,s'). s' = s[PP|-> s VV][MM|->2] & s MM = 1}"
+
+  cmd1v :: "(state*state) set"
+    "cmd1v == {(s,s'). s' = s[PP|-> 1 - s UU][NN|->2] & s NN = 1}"
+
+  (*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}"
+
+  cmd3 :: "[pvar,pvar] => (state*state) set"
+    "cmd3 u m == {(s,s'). s' = s[u|->0][m|->4] & s m = 3}"
+
+  (*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}"
+
+  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}"
+
+  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)}"
+
+
+  
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Network.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Network.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,61 @@
+(*  Title:      HOL/UNITY/Network
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Communication Network
+
+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 thy [stable_def]
+   "[| !! m. stable Acts {s. s(Bproc,Rcvd) <= s(Aproc,Sent)};  \
+\      !! m. stable Acts {s. s(Aproc,Rcvd) <= s(Bproc,Sent)};  \
+\      !! m proc. stable Acts {s. m <= s(proc,Sent)};  \
+\      !! n proc. stable Acts {s. n <= s(proc,Rcvd)};  \
+\      !! m proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} \
+\                                 {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
+\      !! n proc. constrains Acts {s. s(proc,Idle) = 1 & s(proc,Sent) = n} \
+\                                 {s. s(proc,Sent) = n} \
+\   |] ==> stable Acts {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
+\                         s(Aproc,Sent) = s(Bproc,Rcvd) & \
+\                         s(Bproc,Sent) = s(Aproc,Rcvd) & \
+\                         s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
+
+val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
+val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
+val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
+val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
+val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
+val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
+val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
+val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
+
+val rs_AB = [rsA, rsB] MRS constrains_Int;
+val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
+val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
+val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
+val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
+val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
+val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
+val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
+
+by (rtac constrainsI 1);
+by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
+by (assume_tac 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (Blast_tac 1);
+by (Clarify_tac 1);
+by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
+		  "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
+by (REPEAT (blast_tac (claset() addIs [le_anti_sym, le_trans, eq_imp_le]) 2));
+
+by (Asm_simp_tac 1);
+result();
+
+
+
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Network.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Network.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,9 @@
+Network = UNITY +
+
+datatype pvar = Sent | Rcvd | Idle
+
+datatype pname = Aproc | Bproc
+
+types state = "pname * pvar => nat"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/README.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/README.html	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,51 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
+
+<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
+(Addison-Wesley, 1988) presents UNITY, which consists of an abstract
+programming language of guarded assignments and an associated calculus.
+Misra's 1994 paper "A Logic for Concurrent Programming" presents "New UNITY",
+giving more elegant foundations for a more general class of languages.
+
+<P> This directory is a preliminary formalization of New UNITY.  The Isabelle
+examples may not represent the most natural treatment of UNITY style.  Hand
+UNITY proofs tend to be written in the forwards direction, as in informal
+mathematics, while Isabelle works best in a backwards (goal-directed) style.
+
+<P>
+The syntax, also, is rather unnatural.   Programs are expressed as sets of 
+commands, where each command is a relation on states.  Quantification over 
+commands using [] is easily expressed.  At present, there are no examples of
+quantification using ||.
+
+<P>
+The directory presents a few small examples, mostly taken from Misra's 1994
+paper:
+<UL>
+<LI>common meeting time
+
+<LI>the token ring
+
+<LI>the communication network
+
+<LI><EM>n</EM>-process deadlock
+
+<LI>unordered channel
+
+<LI>reachability in directed graphs (section 6.4 of the book)
+</UL>
+
+<P> Safety proofs (invariants) are often proved automatically.  Progress
+proofs involving ENSURES can sometimes be proved automatically.  The
+level of automation appears to be about the same as in HOL-UNITY by Flemming
+Andersen et al.
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ROOT.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/UNITY/ROOT
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Root file for UNITY proofs.
+*)
+
+HOL_build_completed;    (*Make examples fail if HOL did*)
+
+writeln"Root file for HOL/UNITY";
+set proof_timing;
+time_use_thy "Deadlock";
+time_use_thy "WFair";
+time_use_thy "Common";
+time_use_thy "Network";
+time_use_thy "Token";
+time_use_thy "Channel";
+time_use_thy "Mutex";
+time_use_thy "FP";
+time_use_thy "Reach";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Reach.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reach.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,188 @@
+(*  Title:      HOL/UNITY/Reach.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
+*)
+
+open Reach;
+
+(*TO SIMPDATA.ML??  FOR CLASET??  *)
+val major::prems = goal thy 
+    "[| if P then Q else R;    \
+\       [| P;   Q |] ==> S;    \
+\       [| ~ P; R |] ==> S |] ==> S";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
+qed "ifE";
+
+AddSEs [ifE];
+
+
+val cmd_defs = [racts_def, asgt_def, update_def];
+
+goalw thy [racts_def] "id : racts";
+by (Simp_tac 1);
+qed "id_in_racts";
+AddIffs [id_in_racts];
+
+(*All vertex sets are finite*)
+AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
+
+
+(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
+
+(*proves "constrains" properties when the program is specified*)
+val constrains_tac = 
+   SELECT_GOAL
+      (EVERY [rtac constrainsI 1,
+	      rewtac racts_def,
+	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
+	      rewrite_goals_tac [racts_def, asgt_def],
+	      ALLGOALS (SELECT_GOAL Auto_tac)]);
+
+
+(*proves "ensures" properties when the program is specified*)
+fun ensures_tac sact = 
+    SELECT_GOAL
+      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
+	      res_inst_tac [("act", sact)] transient_mem 2,
+	      Simp_tac 2,
+	      constrains_tac 1,
+	      rewrite_goals_tac [racts_def, asgt_def],
+	      Auto_tac]);
+
+
+goalw thy [stable_def, invariant_def]
+    "stable racts invariant";
+by (constrains_tac 1);
+by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "stable_invariant";
+
+goalw thy [rinit_def, invariant_def] "rinit <= invariant";
+by Auto_tac;
+qed "rinit_invariant";
+
+goal thy "reachable rinit racts <= invariant";
+by (simp_tac (simpset() addsimps
+	      [strongest_invariant, stable_invariant, rinit_invariant]) 1); 
+qed "reachable_subset_invariant";
+
+val reachable_subset_invariant' = 
+    rewrite_rule [invariant_def] reachable_subset_invariant;
+
+
+(*** Fixedpoint ***)
+
+(*If it reaches a fixedpoint, it has found a solution*)
+goalw thy [fixedpoint_def, invariant_def]
+    "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
+by (rtac equalityI 1);
+by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
+by (auto_tac (claset() addSIs [ext], simpset()));
+by (etac rtrancl_induct 1);
+by Auto_tac;
+qed "fixedpoint_invariant_correct";
+
+goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
+    "FP racts <= fixedpoint";
+by Auto_tac;
+by (dtac bspec 1); 
+by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
+by (dtac fun_cong 1);
+by Auto_tac;
+val lemma1 = result();
+
+goalw thy (cmd_defs @ [FP_def, fixedpoint_def, stable_def, constrains_def])
+    "fixedpoint <= FP racts";
+by (auto_tac (claset() addIs [ext], simpset()));
+val lemma2 = result();
+
+goal thy "FP racts = fixedpoint";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+qed "FP_fixedpoint";
+
+
+(*If we haven't reached a fixedpoint then there is some edge for which u but
+  not v holds.  Progress will be proved via an ENSURES assertion that the
+  metric will decrease for each suitable edge.  A union over all edges proves
+  a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
+  *)
+
+goal thy "Compl fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps
+	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
+		racts_def, asgt_def])) 1);
+by Safe_tac;
+by (rtac update_idem 1);
+by (Blast_tac 1);
+by (Full_simp_tac 1);
+by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
+by (dtac subsetD 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
+qed "Compl_fixedpoint";
+
+goal thy "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
+by (Blast_tac 1);
+qed "Diff_fixedpoint";
+
+
+(*** Progress ***)
+
+goalw thy [metric_def] "!!s. ~ s x ==> Suc (metric (s[x|->True])) = metric s";
+by (subgoal_tac "{v. ~ (s[x|->True]) v} = {v. ~ s v} - {x}" 1);
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
+qed "Suc_metric";
+
+goal thy "!!s. ~ s x ==> metric (s[x|->True]) < metric s";
+by (etac (Suc_metric RS subst) 1);
+by (Blast_tac 1);
+qed "metric_less";
+AddSIs [metric_less];
+
+goal thy "metric (s[y|->s x | s y]) <= metric s";
+by (case_tac "s x --> s y" 1);
+by (auto_tac (claset() addIs [less_imp_le],
+	      simpset() addsimps [update_idem]));
+qed "metric_le";
+
+goal thy "!!m. (u,v): edges ==> \
+\              ensures racts ((metric-``{m}) Int {s. s u & ~ s v})  \
+\                            (metric-``(lessThan m))";
+by (ensures_tac "asgt u v" 1);
+by (cut_facts_tac [metric_le] 1);
+by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
+qed "edges_ensures";
+
+goal thy "leadsTo racts ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
+by (rtac leadsTo_UN 1);
+by (split_all_tac 1);
+by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
+qed "leadsTo_Diff_fixedpoint";
+
+goal thy "leadsTo racts (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
+qed "leadsTo_Un_fixedpoint";
+
+
+(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
+goal thy "leadsTo racts UNIV fixedpoint";
+by (rtac lessThan_induct 1);
+by Auto_tac;
+by (rtac leadsTo_Un_fixedpoint 1);
+qed "leadsTo_fixedpoint";
+
+goal thy "LeadsTo rinit racts UNIV { %v. (init, v) : edges^* }";
+by (stac (fixedpoint_invariant_correct RS sym) 1);
+by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1); 
+by (cut_facts_tac [reachable_subset_invariant] 1);
+by (Blast_tac 1);
+qed "LeadsTo_correct";
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Reach.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Reach.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,46 @@
+(*  Title:      HOL/UNITY/Reach.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Reachability in Directed Graphs.  From Chandy and Misra, section 6.4.
+*)
+
+Reach = Update + FP + Traces + SubstAx +
+
+types   vertex
+        state = "vertex=>bool"
+
+arities vertex :: term
+
+consts
+  init ::  "vertex"
+
+  edges :: "(vertex*vertex) set"
+
+constdefs
+
+  asgt  :: "[vertex,vertex] => (state*state) set"
+    "asgt u v == {(s,s'). s' = s[v|-> s u | s v]}"
+
+  racts :: "(state*state) set set"
+    "racts == insert id (UN (u,v): edges. {asgt u v})"
+
+  rinit :: "state set"
+    "rinit == {%v. v=init}"
+
+  invariant :: state set
+    "invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+
+  fixedpoint :: state set
+    "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
+
+  metric :: state => nat
+    "metric == (%s. card {v. ~ s v})"
+
+rules
+
+  (*We assume that the set of vertices is finite*)
+  finite_graph "finite (UNIV :: vertex set)"
+  
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/SubstAx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/SubstAx.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,405 @@
+(*  Title:      HOL/UNITY/SubstAx
+    ID:         $Id$
+    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
+*)
+
+open SubstAx;
+
+(*constrains Acts B B' ==> constrains Acts (reachable Init Acts Int B)
+                                           (reachable Init Acts Int B') *)
+bind_thm ("constrains_reachable",
+	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
+
+
+(*** Introduction rules: Basis, Trans, Union ***)
+
+goalw thy [LeadsTo_def]
+    "!!Acts. leadsTo Acts A B ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [PSP_stable2, stable_reachable]) 1);
+qed "leadsTo_imp_LeadsTo";
+
+goalw thy [LeadsTo_def]
+    "!!Acts. [| constrains Acts (reachable Init Acts Int (A - A'))   \
+\                               (A Un A'); \
+\               transient  Acts (reachable Init Acts Int (A-A')) |]   \
+\           ==> LeadsTo Init Acts A A'";
+by (rtac (stable_reachable RS stable_ensures_Int RS leadsTo_Basis) 1);
+by (assume_tac 2);
+by (asm_simp_tac 
+    (simpset() addsimps [Int_Un_distrib RS sym, Diff_Int_distrib RS sym,
+			 stable_constrains_Int]) 1);
+qed "LeadsTo_Basis";
+
+goalw thy [LeadsTo_def]
+    "!!Acts. [| LeadsTo Init Acts A B;  LeadsTo Init Acts B C |] \
+\            ==> LeadsTo Init Acts A C";
+by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
+qed "LeadsTo_Trans";
+
+val prems = goalw thy [LeadsTo_def]
+ "(!!A. A : S ==> LeadsTo Init Acts A B) ==> LeadsTo Init Acts (Union S) B";
+by (stac Int_Union 1);
+by (blast_tac (claset() addIs (leadsTo_UN::prems)) 1);
+qed "LeadsTo_Union";
+
+
+(*** Derived rules ***)
+
+goal thy "!!Acts. id: Acts ==> LeadsTo Init Acts A UNIV";
+by (asm_simp_tac (simpset() addsimps [LeadsTo_def, 
+				      Int_lower1 RS subset_imp_leadsTo]) 1);
+qed "LeadsTo_UNIV";
+Addsimps [LeadsTo_UNIV];
+
+(*Useful with cancellation, disjunction*)
+goal thy "!!Acts. LeadsTo Init Acts A (A' Un A') ==> LeadsTo Init Acts A A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate";
+
+goal thy "!!Acts. LeadsTo Init Acts A (A' Un C Un C) ==> LeadsTo Init Acts A (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "LeadsTo_Un_duplicate2";
+
+val prems = goal thy
+   "(!!i. i : I ==> LeadsTo Init Acts (A i) B) \
+\   ==> LeadsTo Init Acts (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";
+
+(*Binary union introduction rule*)
+goal thy
+  "!!C. [| 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";
+
+
+goalw thy [LeadsTo_def]
+    "!!A B. [| reachable Init Acts Int A <= B;  id: Acts |] \
+\           ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "Int_subset_imp_LeadsTo";
+
+goalw thy [LeadsTo_def]
+    "!!A B. [| A <= B;  id: Acts |] \
+\           ==> LeadsTo Init Acts A B";
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+qed "subset_imp_LeadsTo";
+
+bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
+Addsimps [empty_LeadsTo];
+
+goal thy
+    "!!A B. [| reachable Init Acts Int A = {};  id: Acts |] \
+\           ==> LeadsTo Init Acts A B";
+by (asm_simp_tac (simpset() addsimps [Int_subset_imp_LeadsTo]) 1);
+qed "Int_empty_LeadsTo";
+
+
+goalw thy [LeadsTo_def]
+    "!!Acts. [| LeadsTo Init Acts A A';   \
+\               reachable Init Acts Int A' <= B' |] \
+\            ==> LeadsTo Init Acts A B'";
+by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
+qed_spec_mp "LeadsTo_weaken_R";
+
+
+goalw thy [LeadsTo_def]
+    "!!Acts. [| LeadsTo Init Acts A A'; \
+     \               reachable Init Acts Int B <= A; id: Acts |]  \
+\            ==> LeadsTo Init Acts B A'";
+by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
+qed_spec_mp "LeadsTo_weaken_L";
+
+
+(*Distributes over binary unions*)
+goal thy
+  "!!C. 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 thy
+  "!!C. 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 thy
+  "!!C. 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 thy 
+   "!!Acts. [| 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);
+qed "LeadsTo_weaken";
+
+
+(*Set difference: maybe combine with leadsTo_weaken_L??*)
+goal thy
+  "!!C. [| 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";
+
+
+(** Meta or object quantifier ???????????????????
+    see ball_constrains_UN in UNITY.ML***)
+
+val prems = goal thy
+   "(!! i. i:I ==> LeadsTo Init Acts (A i) (A' i)) \
+\   ==> LeadsTo Init Acts (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);
+qed "LeadsTo_UN_UN";
+
+
+(*Version with no index set*)
+val prems = goal thy
+   "(!! 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] 
+                        addIs prems) 1);
+qed "LeadsTo_UN_UN_noindex";
+
+(*Version with no index set*)
+goal thy
+   "!!Acts. 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";
+
+
+(*Binary union version*)
+goal thy "!!Acts. [| LeadsTo Init Acts A A'; LeadsTo Init Acts B B' |] \
+\                 ==> LeadsTo Init Acts (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [LeadsTo_Un, 
+			       LeadsTo_weaken_R]) 1);
+qed "LeadsTo_Un_Un";
+
+
+(** The cancellation law **)
+
+goal thy
+   "!!Acts. [| 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 thy
+   "!!Acts. [| 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 thy
+   "!!Acts. [| 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 thy
+   "!!Acts. [| 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);
+by (ALLGOALS Asm_simp_tac);
+qed "LeadsTo_cancel_Diff1";
+
+
+
+(** The impossibility law **)
+
+goalw thy [LeadsTo_def]
+    "!!Acts. LeadsTo Init Acts A {} ==> reachable Init Acts Int A  = {}";
+by (Full_simp_tac 1);
+by (etac leadsTo_empty 1);
+qed "LeadsTo_empty";
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
+goalw thy [LeadsTo_def]
+   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
+\           ==> LeadsTo Init Acts (A Int B) (A' Int B)";
+by (asm_simp_tac (simpset() addsimps [Int_assoc RS sym, PSP_stable]) 1);
+qed "R_PSP_stable";
+
+goal thy
+   "!!Acts. [| LeadsTo Init Acts A A'; stable Acts B |] \
+\           ==> LeadsTo Init Acts (B Int A) (B Int A')";
+by (asm_simp_tac (simpset() addsimps (R_PSP_stable::Int_ac)) 1);
+qed "R_PSP_stable2";
+
+
+goalw thy [LeadsTo_def]
+   "!!Acts. [| LeadsTo Init Acts A A'; constrains Acts B B'; id: Acts |] \
+\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un (B' - B))";
+by (dtac PSP 1);
+by (etac constrains_reachable 1);
+by (etac leadsTo_weaken 2);
+by (ALLGOALS Blast_tac);
+qed "R_PSP";
+
+goal thy
+   "!!Acts. [| 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";
+
+goalw thy [unless_def]
+   "!!Acts. [| LeadsTo Init Acts A A'; unless Acts B B'; id: Acts |] \
+\           ==> LeadsTo Init Acts (A Int B) ((A' Int B) Un B')";
+by (dtac R_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";
+
+
+(*** Induction rules ***)
+
+(** Meta or object quantifier ????? **)
+goalw thy [LeadsTo_def]
+   "!!Acts. [| wf r;     \
+\              ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
+\                                       ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\              id: Acts |] \
+\           ==> LeadsTo Init Acts A B";
+by (etac leadsTo_wf_induct 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+qed "LeadsTo_wf_induct";
+
+
+goal thy
+   "!!Acts. [| 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);
+by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
+by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
+qed "R_bounded_induct";
+
+
+goal thy
+   "!!Acts. [| ALL m. LeadsTo Init Acts (A Int f-``{m})                     \
+\                                  ((A Int f-``(lessThan m)) Un 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 thy
+   "!!Acts. [| 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)";
+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 (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "R_lessThan_bounded_induct";
+
+goal thy
+   "!!Acts. [| 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);
+by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
+by (Clarify_tac 1);
+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";
+
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+goalw thy [LeadsTo_def]
+   "!!Acts. [| 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 (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
+                        addSIs [stable_Int, stable_reachable]) 1);
+qed "R_stable_completion";
+
+
+goal thy
+   "!!Acts. [| 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)";
+by (etac finite_induct 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac 
+    (simpset() addsimps [R_stable_completion, stable_def, 
+			 ball_constrains_INT]) 1);
+qed_spec_mp "R_finite_stable_completion";
+
+
+goalw thy [LeadsTo_def]
+ "!!Acts. [| 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 [Int_Un_distrib]) 1);
+by (dtac completion 1);
+by (assume_tac 2);
+by (ALLGOALS 
+    (asm_simp_tac 
+     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
+by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+qed "R_completion";
+
+
+goal thy
+   "!!Acts. [| 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);
+by (dtac ball_constrains_INT 1);
+by (asm_full_simp_tac (simpset() addsimps [R_completion]) 1); 
+qed "R_finite_completion";
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/SubstAx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/SubstAx.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/UNITY/SubstAx
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+My treatment of the Substitution Axiom -- not as an axiom!
+*)
+
+SubstAx = WFair +
+
+constdefs
+
+   LeadsTo :: "['a set, ('a * 'a)set set, 'a set, 'a set] => bool"
+    "LeadsTo Init Acts A B ==
+     leadsTo Acts (reachable Init Acts Int A)
+                  (reachable Init Acts Int B)"
+
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Token.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,150 @@
+(*  Title:      HOL/UNITY/Token
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Token Ring.
+
+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];
+
+AddIffs [N_positive, skip];
+
+goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
+by Auto_tac;
+qed "HasToK_partition";
+
+goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+by (Simp_tac 1);
+by (exhaust_tac "s (Suc 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 thy [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 thy [stable_def]
+    "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
+by (rtac (stable_WT RS stable_constrains_Int) 1);
+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]));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
+qed "token_stable";
+
+
+(*** Progress under weak fairness ***)
+
+goalw thy [nodeOrder_def] "wf(nodeOrder j)";
+by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
+by (Blast_tac 1);
+qed"wf_nodeOrder";
+
+    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+    by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+    by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
+    qed "Suc_lessI";
+
+goalw thy [nodeOrder_def, next_def, inv_image_def]
+    "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+by (auto_tac (claset(),
+	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
+by (dtac sym 1);
+(*The next two lines...**)
+by (REPEAT (eres_inst_tac [("P", "?a<N")] rev_mp 1));
+by (etac ssubst 1);
+(*were with the previous version of asm_full_simp_tac...
+  by (rotate_tac ~1 1);
+*)
+by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv, mod_Suc, mod_less]) 1);
+by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, less_imp_le, Suc_leI, 
+                                      diff_add_assoc]) 2);
+by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1);
+(*including less_asym here would slow things down*)
+by (auto_tac (claset() delrules [notI], 
+              simpset() addsimps [diff_add_assoc2, Suc_leI,
+                                  less_imp_diff_less, 
+                                  mod_less, mod_geq, nat_neq_iff]));
+by (REPEAT (blast_tac (claset() addEs [less_asym]) 3));
+by (asm_simp_tac (simpset() addsimps [less_imp_diff_less,
+				      Suc_diff_n RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less, mod_less]) 1);
+by (etac subst 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_less]) 1);
+qed "nodeOrder_eq";
+
+
+(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
+  Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
+goal thy
+ "!!i. [| 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);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
+qed "TR7_nodeOrder";
+
+
+(*Chapter 4 variant, the one actually used below.*)
+goal thy
+ "!!i. [| 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 thy "({s. Token s < N} Int Token -`` {m}) = \
+\         (if m<N then Token -`` {m} else {})";
+by Auto_tac;
+val Token_lemma = result();
+
+
+(*Misra's TR9: the token reaches an arbitrary node*)
+goal thy
+ "!!i. 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", "{}")]
+     (wf_nodeOrder RS bounded_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Token_lemma, vimage_Diff,
+						HasTok_def])));
+by (Blast_tac 2);
+by (Clarify_tac 1);
+by (rtac (TR7_aux RS leadsTo_weaken) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def])));
+by (ALLGOALS Blast_tac);
+qed "leadsTo_j";
+
+(*Misra's TR8: a hungry process eventually eats*)
+goal thy "!!i. 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";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Token.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Token.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,71 @@
+(*  Title:      HOL/UNITY/Token
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+Token = WFair +
+
+(*process states*)
+datatype pstate = Hungry | Eating | Thinking | Pnum nat
+
+types state = nat => pstate
+
+consts
+  N :: nat	(*number of nodes in the ring*)
+
+constdefs
+  nodeOrder :: "nat => (nat*nat)set"
+    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
+                    (lessThan N Times lessThan N)"
+
+  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}"
+
+  H :: nat => state set
+    "H i == {s. s (Suc i) = Hungry}"
+
+  E :: nat => state set
+    "E i == {s. s (Suc i) = Eating}"
+
+  T :: nat => state set
+    "T i == {s. s (Suc 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)"
+
+  TR3  "constrains Acts (H i) (H i Un E i)"
+
+  TR4  "constrains Acts (H i - HasTok i) (H i)"
+
+  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
+
+  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
+
+  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Traces.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Traces.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,39 @@
+open Traces;
+
+goal thy "reachable Init Acts <= {s. EX evs. s#evs: traces Init Acts}";
+by (rtac subsetI 1);
+be reachable.induct 1;
+by (REPEAT (blast_tac (claset() addIs traces.intrs) 1));
+val lemma1 = result();
+
+goal thy "!!evs. evs : traces Init Acts \
+\                ==> ALL s evs'. evs = s#evs' --> s: reachable Init Acts";
+be traces.induct 1;
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+val lemma2 = normalize_thm [RSmp, RSspec] (result());
+
+goal thy "{s. EX evs. s#evs: traces Init Acts} <= reachable Init Acts";
+by (blast_tac (claset() addIs [lemma2]) 1);
+val lemma3 = result();
+
+goal thy "reachable Init Acts = {s. EX evs. s#evs: traces Init Acts}";
+by (rtac ([lemma1,lemma3] MRS equalityI) 1);
+qed "reachable_eq_traces";
+
+
+(*Could/should this be proved?*)
+goal thy "reachable Init Acts = (UN evs: traces Init Acts. set evs)";
+
+
+(*The strongest invariant is the set of all reachable states!*)
+goalw thy [stable_def, constrains_def]
+    "!!A. [| Init<=A;  stable Acts A |] ==> reachable Init Acts <= A";
+by (rtac subsetI 1);
+be reachable.induct 1;
+by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
+qed "strongest_invariant";
+
+goal thy "stable Acts (reachable Init Acts)";
+by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
+				addIs reachable.intrs) 1));
+qed "stable_reachable";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Traces.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Traces.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,24 @@
+Traces = UNITY +
+
+consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
+
+inductive "traces Init Acts"
+  intrs 
+         (*Initial trace is empty*)
+    Init  "s: Init ==> [s] : traces Init Acts"
+
+    Acts  "[| act: Acts;  s#evs : traces Init Acts;  (s,s'): act |]
+	   ==> s'#s#evs : traces Init Acts"
+
+
+consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
+
+inductive "reachable Init Acts"
+  intrs 
+         (*Initial trace is empty*)
+    Init  "s: Init ==> s : reachable Init Acts"
+
+    Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
+	   ==> s' : reachable Init Acts"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/UNITY.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,229 @@
+(*  Title:      HOL/UNITY/UNITY
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+set proof_timing;
+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 thy "!!x. [| A Int C <= B; B <= A Un C |] \
+\              ==> (A Int B) Un (Compl A Int C) = B Un C";
+by (Blast_tac 1);
+
+goal thy "!!x. [| 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 thy "A Un (Compl A Int C) = A Un C";
+by (Blast_tac 1);
+
+goal thy "A Int (Compl A Un C) = A Int C";
+by (Blast_tac 1);
+
+(*The base B=C*)
+goal thy "(A Int C) Un (Compl A Int C) = C";
+by (Blast_tac 1);
+
+goal thy "(A Un C) Int (Compl A Un C) = C";
+by (Blast_tac 1);
+
+
+(** More ad-hoc rules **)
+
+goal thy "A Un B - (A - B) = B";
+by (Blast_tac 1);
+qed "Un_Diff_Diff";
+
+goal thy "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]
+    "(!!act s s'. [| act: Acts;  (s,s') : act;  s: A |] ==> s': A') \
+\    ==> constrains Acts A A'";
+by (blast_tac (claset() addIs prems) 1);
+qed "constrainsI";
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; act: Acts;  (s,s'): act;  s: A |] \
+\            ==> s': A'";
+by (Blast_tac 1);
+qed "constrainsD";
+
+goalw thy [constrains_def] "constrains Acts {} B";
+by (Blast_tac 1);
+qed "constrains_empty";
+
+goalw thy [constrains_def] "constrains Acts A UNIV";
+by (Blast_tac 1);
+qed "constrains_UNIV";
+AddIffs [constrains_empty, constrains_UNIV];
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
+by (Blast_tac 1);
+qed "constrains_weaken_R";
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
+by (Blast_tac 1);
+qed "constrains_weaken_L";
+
+goalw thy [constrains_def]
+   "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
+by (Blast_tac 1);
+qed "constrains_weaken";
+
+(*Set difference: UNUSED*)
+goalw thy [constrains_def]
+  "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
+\       ==> constrains Acts A C";
+by (Blast_tac 1);
+qed "constrains_Diff";
+
+(** Union **)
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
+\           ==> constrains Acts (A Un B) (A' Un B')";
+by (Blast_tac 1);
+qed "constrains_Un";
+
+goalw thy [constrains_def]
+    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+\    ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
+by (Blast_tac 1);
+qed "ball_constrains_UN";
+
+goalw thy [constrains_def]
+    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+\           ==> constrains Acts (UN i. A i) (UN i. A' i)";
+by (Blast_tac 1);
+qed "all_constrains_UN";
+
+(** Intersection **)
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; constrains Acts B B' |]   \
+\           ==> constrains Acts (A Int B) (A' Int B')";
+by (Blast_tac 1);
+qed "constrains_Int";
+
+goalw thy [constrains_def]
+    "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
+\    ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
+by (Blast_tac 1);
+qed "ball_constrains_INT";
+
+goalw thy [constrains_def]
+    "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
+\           ==> constrains Acts (INT i. A i) (INT i. A' i)";
+by (Blast_tac 1);
+qed "all_constrains_INT";
+
+goalw thy [stable_def, constrains_def]
+    "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |]   \
+\           ==> constrains Acts (C Un A) (C Un A')";
+by (Blast_tac 1);
+qed "stable_constrains_Un";
+
+goalw thy [stable_def, constrains_def]
+    "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |]   \
+\           ==> constrains Acts (C Int A) (C Int A')";
+by (Blast_tac 1);
+qed "stable_constrains_Int";
+
+
+(*** stable ***)
+
+goalw thy [stable_def]
+    "!!Acts. constrains Acts A A ==> stable Acts A";
+by (assume_tac 1);
+qed "stableI";
+
+goalw thy [stable_def]
+    "!!Acts. stable Acts A ==> constrains Acts A A";
+by (assume_tac 1);
+qed "stableD";
+
+goalw thy [stable_def]
+    "!!Acts. [| stable Acts A; stable Acts A' |]   \
+\           ==> stable Acts (A Un A')";
+by (blast_tac (claset() addIs [constrains_Un]) 1);
+qed "stable_Un";
+
+goalw thy [stable_def]
+    "!!Acts. [| stable Acts A; stable Acts A' |]   \
+\           ==> stable Acts (A Int A')";
+by (blast_tac (claset() addIs [constrains_Int]) 1);
+qed "stable_Int";
+
+goalw thy [constrains_def]
+    "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
+by (Blast_tac 1);
+qed "constrains_imp_subset";
+
+
+goalw thy [constrains_def]
+    "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |]   \
+\           ==> constrains Acts A C";
+by (Blast_tac 1);
+qed "constrains_trans";
+
+
+(*The Elimination Theorem.  The "free" m has become universally quantified!
+  Should the premise be !!m instead of ALL m ?  Would make it harder to use
+  in forward proof.*)
+goalw thy [constrains_def]
+    "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
+\           ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
+by (Blast_tac 1);
+qed "elimination";
+
+(*As above, but for the trivial case of a one-variable state, in which the
+  state is identified with its one variable.*)
+goalw thy [constrains_def]
+    "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
+\           ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
+by (Blast_tac 1);
+qed "elimination_sing";
+
+
+goalw thy [constrains_def]
+   "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
+\           ==> constrains Acts A (A' Un B')";
+by (Blast_tac 1);
+qed "constrains_cancel";
+
+
+
+(*** Theoretical Results from Section 6 ***)
+
+goalw thy [constrains_def, strongest_rhs_def]
+    "constrains Acts A (strongest_rhs Acts A )";
+by (Blast_tac 1);
+qed "constrains_strongest_rhs";
+
+goalw thy [constrains_def, strongest_rhs_def]
+    "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
+by (Blast_tac 1);
+qed "strongest_rhs_is_strongest";
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/UNITY.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/UNITY.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/UNITY/UNITY
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+The basic UNITY theory (revised version, based upon the "co" operator)
+
+From Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+UNITY = LessThan +
+
+constdefs
+
+  constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+    "constrains Acts A B == ALL act:Acts. act^^A <= B"
+
+  stable     :: "('a * 'a)set set => 'a set => bool"
+    "stable Acts A == constrains Acts A A"
+
+  strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
+    "strongest_rhs Acts A == Inter {B. constrains Acts A B}"
+
+  unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+    "unless mutex A B == constrains mutex (A-B) (A Un B)"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Update.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Update.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,26 @@
+(*  Title:      HOL/UNITY/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+open Update;
+
+goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
+by Safe_tac;
+by (etac subst 1);
+by (rtac ext 2);
+by Auto_tac;
+qed "update_idem_iff";
+
+(* f x = y ==> f[x|->y] = f *)
+bind_thm("update_idem", update_idem_iff RS iffD2);
+
+AddIffs [refl RS update_idem];
+
+goal thy "(f[x|->y])z = (if x=z then y else f z)";
+by (simp_tac (simpset() addsimps [update_def]) 1);
+qed "update_apply";
+Addsimps [update_apply];
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/Update.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Update.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/UNITY/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like the standard theory Map, but for ordinary functions
+*)
+
+Update = Fun +
+
+consts
+  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+           ("_/[_/|->/_]" [900,0,0] 900)
+
+syntax (symbols)
+  update    :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+
+defs
+  update_def "f[a|->b] == %x. if x=a then b else f x"
+
+end
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/WFair.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/WFair.ML	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,576 @@
+(*  Title:      HOL/UNITY/WFair
+    ID:         $Id$
+    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
+*)
+
+open WFair;
+
+goal thy "Union(B) Int A = Union((%C. C Int A)``B)";
+by (Blast_tac 1);
+qed "Int_Union_Union";
+
+
+(*** transient ***)
+
+goalw thy [stable_def, constrains_def, transient_def]
+    "!!A. [| stable Acts A; transient Acts A |] ==> A = {}";
+by (Blast_tac 1);
+qed "stable_transient_empty";
+
+goalw thy [transient_def]
+    "!!A. [| transient Acts A; B<=A |] ==> transient Acts B";
+by (Clarify_tac 1);
+by (rtac bexI 1 THEN assume_tac 2);
+by (Blast_tac 1);
+qed "transient_strengthen";
+
+goalw thy [transient_def]
+    "!!A. [| act:Acts;  A <= Domain act;  act^^A <= Compl A |] \
+\         ==> transient Acts A";
+by (Blast_tac 1);
+qed "transient_mem";
+
+
+(*** ensures ***)
+
+goalw thy [ensures_def]
+    "!!Acts. [| constrains Acts (A-B) (A Un B); transient Acts (A-B) |] \
+\            ==> ensures Acts A B";
+by (Blast_tac 1);
+qed "ensuresI";
+
+goalw thy [ensures_def]
+    "!!Acts. ensures Acts A B  \
+\            ==> constrains Acts (A-B) (A Un B) & transient Acts (A-B)";
+by (Blast_tac 1);
+qed "ensuresD";
+
+(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
+goalw thy [ensures_def]
+    "!!Acts. [| ensures Acts A A'; A'<=B' |] ==> ensures Acts A B'";
+by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
+qed "ensures_weaken_R";
+
+goalw thy [ensures_def, constrains_def, transient_def]
+    "!!Acts. Acts ~= {} ==> ensures Acts A UNIV";
+by (Asm_simp_tac 1);  (*omitting this causes PROOF FAILED, even with Safe_tac*)
+by (Blast_tac 1);
+qed "ensures_UNIV";
+
+goalw thy [ensures_def]
+    "!!Acts. [| stable Acts C; \
+\               constrains Acts (C Int (A - A')) (A Un A'); \
+\               transient  Acts (C Int (A-A')) |]   \
+\           ==> ensures Acts (C Int A) (C Int A')";
+by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
+				      Diff_Int_distrib RS sym,
+				      stable_constrains_Int]) 1);
+qed "stable_ensures_Int";
+
+
+(*** leadsTo ***)
+
+(*Synonyms for the theorems produced by the inductive defn package*)
+bind_thm ("leadsTo_Basis", leadsto.Basis);
+bind_thm ("leadsTo_Trans", leadsto.Trans);
+
+goal thy "!!Acts. act: Acts ==> leadsTo Acts A UNIV";
+by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
+qed "leadsTo_UNIV";
+Addsimps [leadsTo_UNIV];
+
+(*Useful with cancellation, disjunction*)
+goal thy "!!Acts. leadsTo Acts A (A' Un A') ==> leadsTo Acts A A'";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsTo_Un_duplicate";
+
+goal thy "!!Acts. leadsTo Acts A (A' Un C Un C) ==> leadsTo Acts A (A' Un C)";
+by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
+qed "leadsTo_Un_duplicate2";
+
+(*The Union introduction rule as we should have liked to state it*)
+val prems = goal thy
+    "(!!A. A : S ==> leadsTo Acts A B) ==> leadsTo Acts (Union S) B";
+by (blast_tac (claset() addIs (leadsto.Union::prems)) 1);
+qed "leadsTo_Union";
+
+val prems = goal thy
+    "(!!i. i : I ==> leadsTo Acts (A i) B) ==> leadsTo Acts (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";
+
+(*Binary union introduction rule*)
+goal thy
+  "!!C. [| leadsTo Acts A C; leadsTo Acts B C |] ==> leadsTo Acts (A Un B) C";
+by (stac Un_eq_Union 1);
+by (blast_tac (claset() addIs [leadsTo_Union]) 1);
+qed "leadsTo_Un";
+
+
+(*The INDUCTION rule as we should have liked to state it*)
+val major::prems = goal thy
+  "[| leadsTo Acts za zb;  \
+\     !!A B. ensures Acts A B ==> P A B; \
+\     !!A B C. [| leadsTo Acts A B; P A B; leadsTo Acts B C; P B C |] \
+\              ==> 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 (REPEAT (blast_tac (claset() addIs prems) 1));
+qed "leadsTo_induct";
+
+
+goal thy "!!A B. [| A<=B;  id: Acts |] ==> leadsTo Acts A B";
+by (rtac leadsTo_Basis 1);
+by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
+by (Blast_tac 1);
+qed "subset_imp_leadsTo";
+
+bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
+Addsimps [empty_leadsTo];
+
+
+(*There's a direct proof by leadsTo_Trans and subset_imp_leadsTo, but it
+  needs the extra premise id:Acts*)
+goal thy "!!Acts. leadsTo Acts A A' ==> A'<=B' --> leadsTo Acts A B'";
+by (etac leadsTo_induct 1);
+by (Clarify_tac 3);
+by (blast_tac (claset() addIs [leadsTo_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsTo_Basis, ensures_weaken_R]) 1);
+qed_spec_mp "leadsTo_weaken_R";
+
+
+goal thy "!!Acts. [| leadsTo Acts A A'; B<=A; id: Acts |] ==>  \
+\                 leadsTo Acts B A'";
+by (blast_tac (claset() addIs [leadsTo_Basis, leadsTo_Trans, 
+			       subset_imp_leadsTo]) 1);
+qed_spec_mp "leadsTo_weaken_L";
+
+(*Distributes over binary unions*)
+goal thy
+  "!!C. id: Acts ==> \
+\       leadsTo Acts (A Un B) C  =  (leadsTo Acts A C & leadsTo Acts B C)";
+by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1);
+qed "leadsTo_Un_distrib";
+
+goal thy
+  "!!C. id: Acts ==> \
+\       leadsTo Acts (UN i:I. A i) B  =  (ALL i : I. leadsTo Acts (A i) B)";
+by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1);
+qed "leadsTo_UN_distrib";
+
+goal thy
+  "!!C. id: Acts ==> \
+\       leadsTo Acts (Union S) B  =  (ALL A : S. leadsTo Acts A B)";
+by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1);
+qed "leadsTo_Union_distrib";
+
+
+goal thy
+   "!!Acts. [| leadsTo Acts A A'; id: Acts; B<=A; A'<=B' |] \
+\           ==> leadsTo Acts B B'";
+(*PROOF FAILED: why?*)
+by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_weaken_R,
+			       leadsTo_weaken_L]) 1);
+qed "leadsTo_weaken";
+
+
+(*Set difference: maybe combine with leadsTo_weaken_L??*)
+goal thy
+  "!!C. [| leadsTo Acts (A-B) C; leadsTo Acts B C; id: Acts |] \
+\       ==> leadsTo Acts 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 Acts (A i) (A' i)) \
+\   ==> leadsTo Acts (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);
+qed "leadsTo_UN_UN";
+
+
+(*Version with no index set*)
+val prems = goal thy
+   "(!! i. leadsTo Acts (A i) (A' i)) \
+\   ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
+by (blast_tac (claset() addIs [leadsTo_UN_UN] 
+                        addIs prems) 1);
+qed "leadsTo_UN_UN_noindex";
+
+(*Version with no index set*)
+goal thy
+   "!!Acts. ALL i. leadsTo Acts (A i) (A' i) \
+\           ==> leadsTo Acts (UN i. A i) (UN i. A' i)";
+by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
+qed "all_leadsTo_UN_UN";
+
+
+(*Binary union version*)
+goal thy "!!Acts. [| leadsTo Acts A A'; leadsTo Acts B B' |] \
+\                 ==> leadsTo Acts (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [leadsTo_Un, 
+			       leadsTo_weaken_R]) 1);
+qed "leadsTo_Un_Un";
+
+
+(** The cancellation law **)
+
+goal thy
+   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts B B'; id: Acts |] \
+\           ==> leadsTo Acts A (A' Un B')";
+by (blast_tac (claset() addIs [leadsTo_Un_Un, 
+			       subset_imp_leadsTo, leadsTo_Trans]) 1);
+qed "leadsTo_cancel2";
+
+goal thy
+   "!!Acts. [| leadsTo Acts A (A' Un B); leadsTo Acts (B-A') B'; id: Acts |] \
+\           ==> leadsTo Acts A (A' Un B')";
+by (rtac leadsTo_cancel2 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "leadsTo_cancel_Diff2";
+
+goal thy
+   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts B B'; id: Acts |] \
+\           ==> leadsTo 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 thy
+   "!!Acts. [| leadsTo Acts A (B Un A'); leadsTo Acts (B-A') B'; id: Acts |] \
+\           ==> leadsTo Acts A (B' Un A')";
+by (rtac leadsTo_cancel1 1);
+by (assume_tac 2);
+by (ALLGOALS Asm_simp_tac);
+qed "leadsTo_cancel_Diff1";
+
+
+
+(** The impossibility law **)
+
+goal thy "!!Acts. leadsTo Acts A B ==> B={} --> A={}";
+by (etac leadsTo_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]);
+by (Blast_tac 1);
+val lemma = result() RS mp;
+
+goal thy "!!Acts. leadsTo Acts A {} ==> A={}";
+by (blast_tac (claset() addSIs [lemma]) 1);
+qed "leadsTo_empty";
+
+
+(** PSP: Progress-Safety-Progress **)
+
+(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
+goalw thy [stable_def]
+   "!!Acts. [| leadsTo Acts A A'; stable Acts B |] \
+\           ==> leadsTo Acts (A Int B) (A' Int B)";
+by (etac leadsTo_induct 1);
+by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (rtac leadsTo_Basis 1);
+by (asm_full_simp_tac
+    (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";
+
+goal thy
+   "!!Acts. [| 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";
+
+
+goalw thy [ensures_def]
+   "!!Acts. [| 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";
+
+
+goal thy
+   "!!Acts. [| leadsTo Acts A A'; constrains Acts B B'; id: Acts |] \
+\           ==> leadsTo Acts (A Int B) ((A' Int B) Un (B' - B))";
+by (etac leadsTo_induct 1);
+by (simp_tac (simpset() addsimps [Int_Union_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Union]) 3);
+(*Transitivity case has a delicate argument involving "cancellation"*)
+by (rtac leadsTo_Un_duplicate2 2);
+by (etac leadsTo_cancel_Diff1 2);
+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";
+
+goal thy
+   "!!Acts. [| 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";
+
+
+goalw thy [unless_def]
+   "!!Acts. [| 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 (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";
+
+
+(*** Proving the induction rules ***)
+
+goal thy
+   "!!Acts. [| wf r;     \
+\              ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts (A Int f-``{m}) B";
+by (eres_inst_tac [("a","m")] wf_induct 1);
+by (subgoal_tac "leadsTo Acts (A Int (f -`` (r^-1 ^^ {x}))) B" 1);
+by (stac vimage_eq_UN 2);
+by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2);
+by (blast_tac (claset() addIs [leadsTo_UN]) 2);
+by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1);
+val lemma = result();
+
+
+(** Meta or object quantifier ????? **)
+goal thy
+   "!!Acts. [| wf r;     \
+\              ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts A B";
+by (res_inst_tac [("t", "A")] subst 1);
+by (rtac leadsTo_UN 2);
+by (etac lemma 2);
+by (REPEAT (assume_tac 2));
+by (Fast_tac 1);    (*Blast_tac: Function unknown's argument not a parameter*)
+qed "leadsTo_wf_induct";
+
+
+goal thy
+   "!!Acts. [| wf r;     \
+\              ALL m:I. leadsTo Acts (A Int f-``{m})                   \
+\                                  ((A Int f-``(r^-1 ^^ {m})) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts 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 "bounded_induct";
+
+
+(*Alternative proof is via the lemma leadsTo Acts (A Int f-``(lessThan m)) B*)
+goal thy
+   "!!Acts. [| ALL m. leadsTo Acts (A Int f-``{m})                     \
+\                                  ((A Int f-``(lessThan m)) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts A B";
+by (rtac (wf_less_than RS leadsTo_wf_induct) 1);
+by (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "lessThan_induct";
+
+goal thy
+   "!!Acts. [| ALL m:(greaterThan l). leadsTo Acts (A Int f-``{m})   \
+\                                        ((A Int f-``(lessThan m)) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts 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 bounded_induct) 1);
+by (assume_tac 2);
+by (Asm_simp_tac 1);
+qed "lessThan_bounded_induct";
+
+goal thy
+   "!!Acts. [| ALL m:(lessThan l). leadsTo Acts (A Int f-``{m})   \
+\                                    ((A Int f-``(greaterThan m)) Un B);   \
+\              id: Acts |] \
+\           ==> leadsTo 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);
+by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
+by (Clarify_tac 1);
+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 "greaterThan_bounded_induct";
+
+
+
+(*** wlt ****)
+
+(*Misra's property W3*)
+goalw thy [wlt_def] "leadsTo Acts (wlt Acts B) B";
+by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
+qed "wlt_leadsTo";
+
+goalw thy [wlt_def] "!!Acts. leadsTo Acts A B ==> A <= wlt Acts B";
+by (blast_tac (claset() addSIs [leadsTo_Union]) 1);
+qed "leadsTo_subset";
+
+(*Misra's property W2*)
+goal thy "!!Acts. id: Acts ==> leadsTo Acts A B = (A <= wlt Acts B)";
+by (blast_tac (claset() addSIs [leadsTo_subset, 
+				wlt_leadsTo RS leadsTo_weaken_L]) 1);
+qed "leadsTo_eq_subset_wlt";
+
+(*Misra's property W4*)
+goal thy "!!Acts. id: Acts ==> B <= wlt Acts B";
+by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym,
+				      subset_imp_leadsTo]) 1);
+qed "wlt_increasing";
+
+
+(*Used in the Trans case below*)
+goalw thy [constrains_def]
+   "!!Acts. [| B <= A2;  \
+\              constrains Acts (A1 - B) (A1 Un B); \
+\              constrains Acts (A2 - C) (A2 Un C) |] \
+\           ==> constrains Acts (A1 Un A2 - C) (A1 Un A2 Un C)";
+by (Clarify_tac 1);
+by (blast_tac (claset() addSDs [bspec]) 1);
+val lemma1 = result();
+
+
+(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
+goal thy
+   "!!Acts. [| leadsTo Acts A A';  id: Acts |] ==> \
+\      EX B. A<=B & leadsTo Acts B A' & constrains Acts (B-A') (B Un A')";
+by (etac leadsTo_induct 1);
+(*Basis*)
+by (blast_tac (claset() addIs [leadsTo_Basis]
+                        addDs [ensuresD]) 1);
+(*Trans*)
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "Ba Un Bb")] exI 1);
+by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1,
+			       leadsTo_Un_duplicate]) 1);
+(*Union*)
+by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1,
+				  bchoice, ball_constrains_UN]) 1);;
+by (res_inst_tac [("x", "UN A:S. f A")] exI 1);
+by (blast_tac (claset() addIs [leadsTo_UN, constrains_weaken]) 1);
+qed "leadsTo_123";
+
+
+(*Misra's property W5*)
+goal thy "!!Acts. id: Acts ==> constrains Acts (wlt Acts B - B) (wlt Acts B)";
+by (forward_tac [wlt_leadsTo RS leadsTo_123] 1);
+by (Clarify_tac 1);
+by (subgoal_tac "Ba = wlt Acts B" 1);
+by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt]) 2);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1);
+qed "wlt_constrains_wlt";
+
+
+(*** Completion: Binary and General Finite versions ***)
+
+goal thy
+   "!!Acts. [| leadsTo Acts A A';  stable Acts A';   \
+\              leadsTo Acts B B';  stable Acts B';  id: Acts |] \
+\           ==> leadsTo Acts (A Int B) (A' Int B')";
+by (subgoal_tac "stable Acts (wlt Acts B')" 1);
+by (asm_full_simp_tac (simpset() addsimps [stable_def]) 2);
+by (EVERY [etac (constrains_Un RS constrains_weaken) 2,
+	   etac wlt_constrains_wlt 2,
+	   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 (subgoal_tac "leadsTo Acts (A' Int wlt Acts B') (A' Int B')" 1);
+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);
+(*Blast_tac gives PROOF FAILED*)
+by (best_tac (claset() addIs [leadsTo_Trans]) 1);
+qed "stable_completion";
+
+
+goal thy
+   "!!Acts. [| finite I;  id: Acts |]                     \
+\           ==> (ALL i:I. leadsTo Acts (A i) (A' i)) -->  \
+\               (ALL i:I. stable Acts (A' i)) -->         \
+\               leadsTo 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 
+    (simpset() addsimps [stable_completion, stable_def, 
+			 ball_constrains_INT]) 1);
+qed_spec_mp "finite_stable_completion";
+
+
+goal thy
+   "!!Acts. [| W = wlt Acts (B' Un C);     \
+\              leadsTo Acts A (A' Un C);  constrains Acts A' (A' Un C);   \
+\              leadsTo Acts B (B' Un C);  constrains Acts B' (B' Un C);   \
+\              id: Acts |] \
+\           ==> leadsTo Acts (A Int B) ((A' Int B') Un C)";
+by (subgoal_tac "constrains Acts (W-C) (W Un B' Un C)" 1);
+by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] 
+			       MRS constrains_Un RS constrains_weaken]) 2);
+by (subgoal_tac "constrains Acts (W-C) W" 1);
+by (asm_full_simp_tac 
+    (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 (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, 
+			       subset_refl RS subset_imp_leadsTo, 
+			       leadsTo_Un_duplicate2]) 2);
+by (dtac leadsTo_Diff 1);
+by (assume_tac 2);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+by (subgoal_tac "A Int B <= A Int W" 1);
+by (blast_tac (claset() addIs [leadsTo_subset, Int_mono] 
+	                delrules [subsetI]) 2);
+by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1);
+bind_thm("completion", refl RS result());
+
+
+goal thy
+   "!!Acts. [| finite I;  id: Acts |] \
+\           ==> (ALL i:I. leadsTo Acts (A i) (A' i Un C)) -->  \
+\               (ALL i:I. constrains Acts (A' i) (A' i Un C)) --> \
+\               leadsTo 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);
+by (dtac ball_constrains_INT 1);
+by (asm_full_simp_tac (simpset() addsimps [completion]) 1); 
+qed "finite_completion";
+
diff -r 66b1a7c42d94 -r 1f9362e769c1 src/HOL/UNITY/WFair.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/WFair.thy	Fri Apr 03 12:34:33 1998 +0200
@@ -0,0 +1,43 @@
+(*  Title:      HOL/UNITY/WFair
+    ID:         $Id$
+    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
+*)
+
+WFair = Traces + Vimage +
+
+constdefs
+
+  transient :: "[('a * 'a)set set, 'a set] => bool"
+    "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A"
+
+  ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+    "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)"
+
+consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool"
+       leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set"
+  
+translations
+  "leadsTo Acts A B" == "(A,B) : leadsto Acts"
+
+inductive "leadsto Acts"
+  intrs 
+
+    Basis  "ensures Acts A B ==> leadsTo Acts A B"
+
+    Trans  "[| leadsTo Acts A B;  leadsTo Acts B C |]
+	   ==> leadsTo Acts A C"
+
+    Union  "(UN A:S. {(A,B)}) : Pow (leadsto Acts)
+	   ==> leadsTo Acts (Union S) B"
+
+  monos "[Pow_mono]"
+
+constdefs wlt :: "[('a * 'a)set set, 'a set] => 'a set"
+  "wlt Acts B == Union {A. leadsTo Acts A B}"
+
+end