# HG changeset patch
# User paulson
# Date 1056539846 -7200
# Node ID f932be305381d8526a4522da73927f5bb750a5fa
# Parent  3738065456569b4692f9a1eef9d3b704da9afe58
Conversion of UNITY/Distributor to Isar script.  General tidy-up.

diff -r 373806545656 -r f932be305381 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/IsaMakefile	Wed Jun 25 13:17:26 2003 +0200
@@ -121,8 +121,7 @@
   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
   UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
   UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
-  UNITY/ClientImpl.thy\
-  UNITY/Distributor.ML UNITY/Distributor.thy\
+  UNITY/ClientImpl.thy UNITY/Distributor.thy\
   UNITY/Follows.ML UNITY/Follows.thy\
   UNITY/Increasing.ML UNITY/Increasing.thy\
   UNITY/Merge.ML UNITY/Merge.thy\
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy	Wed Jun 25 13:17:26 2003 +0200
@@ -28,7 +28,7 @@
 constdefs
   alloc_giv_act :: i
   "alloc_giv_act ==
-       {<s, t> : state*state.
+       {<s, t> \<in> state*state.
 	\<exists>k. k = length(s`giv) &
             t = s(giv := s`giv @ [nth(k, s`ask)],
 		  available_tok := s`available_tok #- nth(k, s`ask)) &
@@ -36,13 +36,13 @@
 
   alloc_rel_act :: i
   "alloc_rel_act ==
-       {<s, t> : state*state.
+       {<s, t> \<in> state*state.
         t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
 	      NbR := succ(s`NbR)) &
   	s`NbR < length(s`rel)}"
 
   (*The initial condition s`giv=[] is missing from the
-    original definition -- S. O. Ehmety *)
+    original definition: S. O. Ehmety *)
   alloc_prog :: i
   "alloc_prog ==
        mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
@@ -146,8 +146,8 @@
 done
 
 lemma giv_Bounded_lemma2:
-"[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
-  ==> alloc_prog Join G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
+"[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
+  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
    {s\<in>state. s`available_tok #+ tokens(s`giv) =
     NbT #+ tokens(take(s`NbR, s`rel))})"
 apply (cut_tac giv_Bounded_lamma1)
@@ -203,11 +203,11 @@
   asked for*)
 lemma alloc_prog_ask_prefix_giv:
      "alloc_prog \<in> Incr(lift(ask)) guarantees
-                   Always({s\<in>state. <s`giv, s`ask>:prefix(tokbag)})"
+                   Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})"
 apply (auto intro!: AlwaysI simp add: guar_def)
 apply (subgoal_tac "G \<in> preserves (lift (giv))")
  prefer 2 apply (simp add: alloc_prog_ok_iff)
-apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
+apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
        in stable_Join_Stable)
 apply constrains
  prefer 2 apply (simp add: lift_def, clarify)
@@ -220,7 +220,7 @@
 
 lemma alloc_prog_transient_lemma:
      "[|G \<in> program; k\<in>nat|]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
              transient({s\<in>state. k \<le> length(s`rel)} \<inter>
              {s\<in>state. succ(s`NbR) = k})"
 apply auto
@@ -238,7 +238,7 @@
 
 lemma alloc_prog_rel_Stable_NbR_lemma:
     "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
-     ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
+     ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
 apply (blast intro: le_trans leI)
 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
@@ -250,11 +250,11 @@
 
 lemma alloc_prog_NbR_LeadsTo_lemma:
      "[| G \<in> program; alloc_prog ok G;
-	 alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
-      ==> alloc_prog Join G \<in>
+	 alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
 	    LeadsTo {s\<in>state. k \<le> s`NbR}"
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
 apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
 apply (rule_tac [2] mono_length)
     prefer 3 apply simp
@@ -269,9 +269,9 @@
 done
 
 lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
-    "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+    "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
         k\<in>nat; n \<in> nat; n < k |]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
 	       LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
 		 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
@@ -279,7 +279,7 @@
 apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
        in LeadsTo_weaken_R)
 apply safe
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
 apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
 apply (rule_tac [2] mono_length)
     prefer 3 apply simp
@@ -301,9 +301,9 @@
 (* Lemma 49, page 28 *)
 
 lemma alloc_prog_NbR_LeadsTo_lemma3:
-  "[|G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+  "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
      k\<in>nat|]
-   ==> alloc_prog Join G \<in>
+   ==> alloc_prog \<squnion> G \<in>
            {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
 (* Proof by induction over the difference between k and n *)
 apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
@@ -326,8 +326,8 @@
 
 lemma alloc_prog_giv_Ensures_lemma:
 "[| G \<in> program; k\<in>nat; alloc_prog ok G;
-  alloc_prog Join G \<in> Incr(lift(ask)) |] ==>
-  alloc_prog Join G \<in>
+  alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
+  alloc_prog \<squnion> G \<in>
   {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
   Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
@@ -360,7 +360,7 @@
 
 lemma alloc_prog_giv_Stable_lemma:
 "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
-  ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
+  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
 apply (auto intro: leI)
 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
@@ -374,15 +374,15 @@
 
 lemma alloc_prog_giv_LeadsTo_lemma:
 "[| G \<in> program; alloc_prog ok G;
-    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
- ==> alloc_prog Join G \<in>
+    alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
+ ==> alloc_prog \<squnion> G \<in>
 	{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
 	{s\<in>state.  k < length(s`ask)} \<inter>
 	{s\<in>state. length(s`giv) = k}
 	LeadsTo {s\<in>state. k < length(s`giv)}"
-apply (subgoal_tac "alloc_prog Join G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {s\<in>state. length(s`giv) \<noteq> k}")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {s\<in>state. length(s`giv) \<noteq> k}")
 prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
 apply (drule PSP_Stable, assumption)
 apply (rule LeadsTo_weaken)
 apply (rule PSP_Stable)
@@ -400,12 +400,12 @@
   (NbT) does not exceed the number currently available.*)
 lemma alloc_prog_Always_lemma:
 "[| G \<in> program; alloc_prog ok G;
-    alloc_prog Join G \<in> Incr(lift(ask));
-    alloc_prog Join G \<in> Incr(lift(rel)) |]
-  ==> alloc_prog Join G \<in>
+    alloc_prog \<squnion> G \<in> Incr(lift(ask));
+    alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
+  ==> alloc_prog \<squnion> G \<in>
         Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
                 NbT \<le> s`available_tok})"
-apply (subgoal_tac "alloc_prog Join G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ")
+apply (subgoal_tac "alloc_prog \<squnion> G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> {s\<in>state. s`available_tok #+ tokens(s`giv) = NbT #+ tokens(take (s`NbR, s`rel))}) ")
 apply (rule_tac [2] AlwaysI)
 apply (rule_tac [3] giv_Bounded_lemma2, auto)
 apply (rule Always_weaken, assumption, auto)
@@ -448,11 +448,11 @@
  fixes G
  assumes Gprog [intro,simp]: "G \<in> program"
      and okG [iff]:          "alloc_prog ok G"
-     and Incr_rel [intro]:   "alloc_prog Join G \<in> Incr(lift(rel))"
-     and Incr_ask [intro]:   "alloc_prog Join G \<in> Incr(lift(ask))"
-     and safety:   "alloc_prog Join G
+     and Incr_rel [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(rel))"
+     and Incr_ask [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(ask))"
+     and safety:   "alloc_prog \<squnion> G
                       \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
-     and progress: "alloc_prog Join G
+     and progress: "alloc_prog \<squnion> G
                       \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
                         {s\<in>state. k \<le> tokens(s`rel)})"
 
@@ -461,7 +461,7 @@
   will eventually recognize that they've been released.*)
 lemma (in alloc_progress) tokens_take_NbR_lemma:
  "k \<in> tokbag
-  ==> alloc_prog Join G \<in>
+  ==> alloc_prog \<squnion> G \<in>
         {s\<in>state. k \<le> tokens(s`rel)}
         LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
 apply (rule single_LeadsTo_I, safe)
@@ -480,7 +480,7 @@
   LeadsTo *)
 lemma (in alloc_progress) tokens_take_NbR_lemma2:
      "k \<in> tokbag
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. tokens(s`giv) = k}
 	    LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
 apply (rule LeadsTo_Trans)
@@ -493,7 +493,7 @@
 (*Third step in proof of (31): by PSP with the fact that giv increases *)
 lemma (in alloc_progress) length_giv_disj:
      "[| k \<in> tokbag; n \<in> nat |]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
 	    LeadsTo
 	      {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
@@ -513,7 +513,7 @@
 (*Fourth step in proof of (31): we apply lemma (51) *)
 lemma (in alloc_progress) length_giv_disj2:
      "[|k \<in> tokbag; n \<in> nat|]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
 	    LeadsTo
 	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
@@ -526,7 +526,7 @@
   k\<in>nat *)
 lemma (in alloc_progress) length_giv_disj3:
      "n \<in> nat
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. length(s`giv) = n}
 	    LeadsTo
 	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
@@ -541,7 +541,7 @@
   assumption that ask increases *)
 lemma (in alloc_progress) length_ask_giv:
  "[|k \<in> nat;  n < k|]
-  ==> alloc_prog Join G \<in>
+  ==> alloc_prog \<squnion> G \<in>
         {s\<in>state. length(s`ask) = k & length(s`giv) = n}
         LeadsTo
           {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
@@ -564,7 +564,7 @@
 (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
 lemma (in alloc_progress) length_ask_giv2:
      "[|k \<in> nat;  n < k|]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
 	    LeadsTo
 	      {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
@@ -581,7 +581,7 @@
 (*Eighth step in proof of (31): by 50, we get |giv| > n. *)
 lemma (in alloc_progress) extend_giv:
      "[| k \<in> nat;  n < k|]
-      ==> alloc_prog Join G \<in>
+      ==> alloc_prog \<squnion> G \<in>
 	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
 	    LeadsTo {s\<in>state. n < length(s`giv)}"
 apply (rule LeadsTo_Un_duplicate)
@@ -597,7 +597,7 @@
   we can't expect |ask| to remain fixed until |giv| increases.*)
 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
  "k \<in> nat
-  ==> alloc_prog Join G \<in>
+  ==> alloc_prog \<squnion> G \<in>
         {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
 (* Proof by induction over the difference between k and n *)
 apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
@@ -622,9 +622,9 @@
 (*Final lemma: combine previous result with lemma (30)*)
 lemma (in alloc_progress) final:
      "h \<in> list(tokbag)
-      ==> alloc_prog Join G \<in>
-	    {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
-	    {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
+      ==> alloc_prog \<squnion> G
+            \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+	      {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
 apply (rule single_LeadsTo_I)
  prefer 2 apply simp
 apply (rename_tac s0)
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Wed Jun 25 13:17:26 2003 +0200
@@ -8,6 +8,22 @@
 
 
 theory ClientImpl = AllocBase + Guar:
+
+(*????MOVE UP*)
+method_setup constrains = {*
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts =>
+            gen_constrains_tac (Classical.get_local_claset ctxt,
+                               Simplifier.get_local_simpset ctxt) 1)) *}
+    "for proving safety properties"
+
+(*For using "disjunction" (union over an index set) to eliminate a variable.
+  ????move way up*)
+lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
+      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
+by blast
+
+
 consts
   ask :: i (* input history:  tokens requested *)
   giv :: i (* output history: tokens granted *)
@@ -66,20 +82,6 @@
 declare type_assumes [simp] default_val_assumes [simp]
 (* This part should be automated *)
 
-(*????MOVE UP*)
-method_setup constrains = {*
-    Method.ctxt_args (fn ctxt =>
-        Method.METHOD (fn facts =>
-            gen_constrains_tac (Classical.get_local_claset ctxt,
-                               Simplifier.get_local_simpset ctxt) 1)) *}
-    "for proving safety properties"
-
-(*For using "disjunction" (union over an index set) to eliminate a variable.
-  ????move way up*)
-lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
-      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
-by blast
-
 lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
 apply (unfold state_def)
 apply (drule_tac a = ask in apply_type, auto)
@@ -164,7 +166,7 @@
 
 lemma ask_Bounded_lemma: 
 "[| client_prog ok G; G \<in> program |] 
-      ==> client_prog Join G \<in>    
+      ==> client_prog \<squnion> G \<in>    
               Always({s \<in> state. s`tok \<le> NbT}  Int   
                       {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
 apply (rotate_tac -1)
@@ -194,15 +196,15 @@
 by (constrains, auto)
 
 lemma client_prog_Join_Stable_rel_le_giv: 
-"[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
-    ==> client_prog Join G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
+    ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
 apply (auto simp add: lift_def)
 done
 
 lemma client_prog_Join_Always_rel_le_giv:
-     "[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
-    ==> client_prog Join G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+     "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
+    ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
 
 lemma def_act_eq:
@@ -243,8 +245,8 @@
 done
 
 lemma induct_lemma: 
-"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
-  ==> client_prog Join G \<in>  
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
+  ==> client_prog \<squnion> G \<in>  
   {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)  
    & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
         LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)  
@@ -272,8 +274,8 @@
 done
 
 lemma rel_progress_lemma: 
-"[| client_prog Join G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
-  ==> client_prog Join G  \<in>  
+"[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
+  ==> client_prog \<squnion> G  \<in>  
      {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)  
            & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
                       LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
@@ -301,11 +303,12 @@
 done
 
 lemma progress_lemma: 
-"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
- ==> client_prog Join G  \<in>  
-      {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
-      LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
-apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], assumption)
+"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
+ ==> client_prog \<squnion> G
+       \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
+         LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
+apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], 
+       assumption)
 apply (force simp add: client_prog_ok_iff)
 apply (rule LeadsTo_weaken_L) 
 apply (rule LeadsTo_Un [OF rel_progress_lemma 
@@ -331,4 +334,4 @@
                       cons_Int_distrib safety_prop_Acts_iff)
 done
 
-end
\ No newline at end of file
+end
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/Distributor.ML
--- a/src/ZF/UNITY/Distributor.ML	Tue Jun 24 16:32:59 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(*  Title: ZF/UNITY/Distributor
-    ID:         $Id$
-    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
-    Copyright   2002  University of Cambridge
-
-A multiple-client allocator from a single-client allocator:
-Distributor specification
-*)
-
-Open_locale "Distributor";
-val all_distinct_vars = thm "all_distinct_vars";
-val var_assumes = thm "var_assumes";
-val type_assumes = thm "type_assumes";
-val default_val_assumes  = thm "default_val_assumes";
-
-Addsimps [var_assumes, default_val_assumes,  type_assumes];
-
-Goalw [state_def]
-"s \\<in> state ==> s`In \\<in> list(A)";
-by (dres_inst_tac [("a", "In")] apply_type 1);
-by Auto_tac;
-qed "In_value_type";
-AddTCs [In_value_type];
-Addsimps [In_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`iIn \\<in> list(nat)";
-by (dres_inst_tac [("a", "iIn")] apply_type 1);
-by Auto_tac;
-qed "iIn_value_type";
-AddTCs [iIn_value_type];
-Addsimps [iIn_value_type];
-
-Goalw [state_def]
-"s \\<in> state ==> s`Out(n):list(A)";
-by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
-by Auto_tac;
-qed "Out_value_type";
-AddTCs [Out_value_type];
-Addsimps [Out_value_type];
-
-val distrib = thm "distr_spec";
-
-Goal "D \\<in> program";
-by (cut_facts_tac [distrib] 1);
-by (auto_tac (claset(), simpset() addsimps 
-           [distr_spec_def, distr_allowed_acts_def]));
-qed "D_in_program";
-Addsimps [D_in_program];
-AddTCs [D_in_program];
-
-Goal "G \\<in> program ==> \
-\   D ok G <-> \
-\  ((\\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n)))) & D \\<in> Allowed(G))";
-by (cut_facts_tac [distrib] 1);
-by (auto_tac (claset(), 
-     simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def, 
-                         Allowed_def, ok_iff_Allowed]));
-by (rotate_tac ~1 2);
-by (dres_inst_tac [("x", "G")] bspec 2);
-by Auto_tac;
-by (dresolve_tac [rotate_prems 1 (safety_prop_Acts_iff RS iffD1)] 1);
-by (auto_tac (claset() addIs [safety_prop_Inter], simpset()));
-qed "D_ok_iff";
-
-Goal 
-"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
-\     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
-\     Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt<Nclients})) \
-\     guarantees \
-\         (\\<Inter>n \\<in> Nclients. lift(Out(n)) IncreasingWrt \
-\                           prefix(A)/list(A))";
-by (cut_facts_tac [D_in_program, distrib] 1);
-by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
-by (auto_tac (claset() addSIs [guaranteesI]  addIs [Follows_imp_Increasing_left]
-                        addSDs [guaranteesD], 
-               simpset()));
-qed "distr_Increasing_Out";
-
-val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
-
-Goal
-"[| \\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n))); \
-\  D Join G \\<in> Always({s \\<in> state. \
-\         \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |] \
-\ ==> D Join G : Always \
-\         ({s \\<in> state. msetsum(%n. bag_of (sublist(s`In, \
-\                      {k \\<in> nat. k < length(s`iIn) &\
-\                         nth(k, s`iIn)= n})), \
-\                        Nclients, A) = \
-\             bag_of(sublist(s`In, length(s`iIn)))})";
-by (cut_facts_tac [D_in_program] 1);
-by (subgoal_tac "G \\<in> program" 1);
-by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
-by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
-by Auto_tac;
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
-by (asm_simp_tac (simpset() addsimps [nat_into_Finite]) 1); 
-by (Blast_tac 1); 
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1); 
-by (subgoal_tac
-    "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
-\    length(x`iIn)" 1);
-by (Asm_simp_tac 1);
-by (resolve_tac [equalityI] 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [ltD]) 1);
-by (subgoal_tac "length(x ` iIn) : nat" 1);
-by Typecheck_tac; 
-by (subgoal_tac "xa : nat" 1); 
-by (dres_inst_tac [("x", "nth(xa, x`iIn)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec  1);
-by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
-by (blast_tac (claset() addDs [ltD]) 1); 
-by (blast_tac (claset() addIs [lt_trans]) 1);
-qed "distr_bag_Follows_lemma";
-
-Goal
- "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
-\      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
-\       Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})) \
-\     guarantees  \
-\      (\\<Inter>n \\<in> Nclients. \
-\       (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A)) \
-\       Fols \
-\       (%s. bag_of(sublist(s`In, length(s`iIn)))) \
-\       Wrt MultLe(A, r)/Mult(A))";
-by (cut_facts_tac [distrib] 1);
-by (rtac guaranteesI 1);
-by (Clarify_tac 1); 
-by (Simp_tac 2);
-by (rtac (distr_bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;  
-by (rtac Follows_state_ofD1 2);
-by (rtac Follows_msetsum_UN 2);
-by (ALLGOALS(Clarify_tac));
-by (resolve_tac [conjI] 3);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 3);
-by (resolve_tac [conjI] 4);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 4);
-by (resolve_tac [conjI] 5);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
-by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
-by (Clarify_tac 4);
-by (Asm_full_simp_tac 3);
-by (Asm_full_simp_tac 3);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
-by (rotate_tac 2 1);
-by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [distr_spec_def, distr_follows_def]));
-by (dtac guaranteesD 1); 
-by (assume_tac 1);
-by (Force_tac 1); 
-by (Force_tac 1); 
-by (asm_full_simp_tac
-    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
-             refl_prefix, trans_on_MultLe] 
-            addcongs [Follows_cong]) 1); 
-qed  "distr_bag_Follows";
-Close_locale "Distributor";
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/Distributor.thy
--- a/src/ZF/UNITY/Distributor.thy	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/Distributor.thy	Wed Jun 25 13:17:26 2003 +0200
@@ -6,44 +6,160 @@
 A multiple-client allocator from a single-client allocator:
 Distributor specification
 *)
-Distributor = AllocBase + Follows +  Guar + GenPrefix +
-(** Distributor specification (the number of outputs is Nclients) ***)
- (*spec (14)*)
-constdefs  
-  distr_follows :: [i, i, i, i =>i] =>i
+
+theory Distributor = AllocBase + Follows +  Guar + GenPrefix:
+
+text{*Distributor specification (the number of outputs is Nclients)*}
+
+text{*spec (14)*}
+constdefs
+  distr_follows :: "[i, i, i, i =>i] =>i"
     "distr_follows(A, In, iIn, Out) ==
-     (lift(In) IncreasingWrt prefix(A)/list(A)) Int
-     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
-     Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})
+     (lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+     Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients})
          guarantees
-         (\\<Inter>n \\<in> Nclients.
+         (\<Inter>n \<in> Nclients.
           lift(Out(n))
               Fols
-          (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
+          (%s. sublist(s`In, {k \<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
 	  Wrt prefix(A)/list(A))"
-  
- distr_allowed_acts :: [i=>i]=>i
-  "distr_allowed_acts(Out) ==
-   {D:program. AllowedActs(D) =
-   cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
+
+  distr_allowed_acts :: "[i=>i]=>i"
+    "distr_allowed_acts(Out) ==
+     {D \<in> program. AllowedActs(D) =
+     cons(id(state), \<Union>G \<in> (\<Inter>n\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
+
+  distr_spec :: "[i, i, i, i =>i]=>i"
+    "distr_spec(A, In, iIn, Out) ==
+     distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
+
+locale distr =
+  fixes In  --{*items to distribute*}
+    and iIn --{*destinations of items to distribute*}
+    and Out --{*distributed items*}
+    and A   --{*the type of items being distributed *}
+    and D
+ assumes
+     var_assumes [simp]:  "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
+ and all_distinct_vars:   "\<forall>n. all_distinct([In, iIn, iOut(n)])"
+ and type_assumes [simp]: "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
+                          (\<forall>n. type_of(Out(n))=list(A))"
+ and default_val_assumes [simp]:
+                         "default_val(In)=Nil &
+                          default_val(iIn)=Nil &
+                          (\<forall>n. default_val(Out(n))=Nil)"
+ and distr_spec:  "D \<in> distr_spec(A, In, iIn, Out)"
+
 
-  distr_spec :: [i, i, i, i =>i]=>i
-  "distr_spec(A, In, iIn, Out) ==
-   distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)"
+lemma (in distr) In_value_type [simp,TC]: "s \<in> state ==> s`In \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = In in apply_type, auto)
+done
+
+lemma (in distr) iIn_value_type [simp,TC]:
+     "s \<in> state ==> s`iIn \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = iIn in apply_type, auto)
+done
+
+lemma (in distr) Out_value_type [simp,TC]:
+     "s \<in> state ==> s`Out(n):list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "Out (n)" in apply_type)
+apply auto
+done
+
+lemma (in distr) D_in_program [simp,TC]: "D \<in> program"
+apply (cut_tac distr_spec)
+apply (auto simp add: distr_spec_def distr_allowed_acts_def)
+done
+
+lemma (in distr) D_ok_iff:
+     "G \<in> program ==>
+	D ok G <-> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))"
+apply (cut_tac distr_spec)
+apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def
+                      Allowed_def ok_iff_Allowed)
+apply (drule_tac [2] x = G and P = "%y. x \<notin> Acts(y)" in bspec)
+apply auto
+apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1])
+apply (auto intro: safety_prop_Inter)
+done
 
-locale Distributor =
-  fixes In :: i  (*items to distribute*)
-        iIn :: i (*destinations of items to distribute*)
-        Out :: i=>i  (*distributed items*)
-        A :: i   (*the type of items being distributed *)
-        D :: i
- assumes
-    var_assumes       "In:var & iIn:var & (\\<forall>n. Out(n):var)"
-    all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])"
-    type_assumes      "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
-                       (\\<forall>n. type_of(Out(n))=list(A))"
-   default_val_assumes "default_val(In)=Nil &
-                        default_val(iIn)=Nil &
-                        (\\<forall>n. default_val(Out(n))=Nil)"
-   distr_spec  "D:distr_spec(A, In, iIn, Out)"
+lemma (in distr) distr_Increasing_Out:
+"D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+      Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt<Nclients}))
+      guarantees
+          (\<Inter>n \<in> Nclients. lift(Out(n)) IncreasingWrt
+                            prefix(A)/list(A))"
+apply (cut_tac D_in_program distr_spec)
+apply (simp (no_asm_use) add: distr_spec_def distr_follows_def)
+apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left 
+            dest!: guaranteesD)
+done
+
+lemma (in distr) distr_bag_Follows_lemma:
+"[| \<forall>n \<in> nat. G \<in> preserves(lift(Out(n)));
+   D \<squnion> G \<in> Always({s \<in> state.
+          \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}) |]
+  ==> D \<squnion> G \<in> Always
+          ({s \<in> state. msetsum(%n. bag_of (sublist(s`In,
+                       {k \<in> nat. k < length(s`iIn) &
+                          nth(k, s`iIn)= n})),
+                         Nclients, A) =
+              bag_of(sublist(s`In, length(s`iIn)))})"
+apply (cut_tac D_in_program)
+apply (subgoal_tac "G \<in> program")
+ prefer 2 apply (blast dest: preserves_type [THEN subsetD])
+apply (erule Always_Diff_Un_eq [THEN iffD1])
+apply (rule state_AlwaysI [THEN Always_weaken], auto)
+apply (rename_tac s)
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+   apply (simp (no_asm_simp) add: nat_into_Finite)
+  apply blast
+ apply (simp (no_asm_simp))
+apply (simp add: set_of_list_conv_nth [of _ nat])
+apply (subgoal_tac
+       "(\<Union>i \<in> Nclients. {k\<in>nat. k < length(s`iIn) & nth(k, s`iIn) = i}) =
+        length(s`iIn) ")
+apply (simp (no_asm_simp))
+apply (rule equalityI)
+apply (force simp add: ltD, safe)
+apply (rename_tac m)
+apply (subgoal_tac "length (s ` iIn) \<in> nat")
+apply typecheck
+apply (subgoal_tac "m \<in> nat")
+apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
+apply (simp add: ltI)
+apply (simp_all add: Ord_mem_iff_lt)
+apply (blast dest: ltD)
+apply (blast intro: lt_trans)
+done
+
+theorem (in distr) distr_bag_Follows:
+ "D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
+       (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
+        Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}))
+      guarantees
+       (\<Inter>n \<in> Nclients.
+        (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A))
+        Fols
+        (%s. bag_of(sublist(s`In, length(s`iIn))))
+        Wrt MultLe(A, r)/Mult(A))"
+apply (cut_tac distr_spec)
+apply (rule guaranteesI, clarify)
+apply (rule distr_bag_Follows_lemma [THEN Always_Follows2])
+apply (simp add: D_ok_iff, auto)
+apply (rule Follows_state_ofD1)
+apply (rule Follows_msetsum_UN)
+   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
+apply (auto simp add: distr_spec_def distr_follows_def)
+apply (drule guaranteesD, assumption)
+apply (simp_all cong add: Follows_cong
+    add: refl_prefix
+       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+done
+
 end
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/UNITYMisc.ML
--- a/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.ML	Wed Jun 25 13:17:26 2003 +0200
@@ -7,11 +7,6 @@
 
 *)
 
-Goalw [greaterThan_def]
-"i:greaterThan(k,A) <-> i:A & k<i";
-by Auto_tac;
-qed "greaterThan_iff";
-
 (** Ad-hoc set-theory rules **)
 
 Goal "Union(B) Int A = (UN b:B. b Int A)";
@@ -22,11 +17,6 @@
 by Auto_tac;
 qed "Int_Union_Union2";
 
-Goal "A Un B - (A - B) = B";
-by (Blast_tac 1);
-qed "Un_Diff_Diff";
-AddIffs [Un_Diff_Diff];
-
 
 (** Needed in State theory for the current definition of variables 
 where they are indexed by lists  **)
@@ -38,22 +28,17 @@
 qed "list_nat_into_univ";
 
 
-(** Simplication rules for Collect; ????
-  At least change to "{x:A. P(x)} Int A = {x : A Int B. P(x)} **)
-
-Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
-by Auto_tac;
-qed "Collect_Int2";
+(** Simplication rules for Collect **)
 
-Goal "A Int {x:A. P(x)} = {x:A. P(x)}";
+(*Currently unused*)
+Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}";
 by Auto_tac;
-qed "Collect_Int3";
+qed "Collect_Int_left";
 
-(*????????????????*)
-AddIffs [Collect_Int2, Collect_Int3];
-
-
-(*for main ZF????*)
+(*Currently unused*)
+Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}";
+by Auto_tac;
+qed "Collect_Int_right";
 
 Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
 by Auto_tac;
diff -r 373806545656 -r f932be305381 src/ZF/UNITY/UNITYMisc.thy
--- a/src/ZF/UNITY/UNITYMisc.thy	Tue Jun 24 16:32:59 2003 +0200
+++ b/src/ZF/UNITY/UNITYMisc.thy	Wed Jun 25 13:17:26 2003 +0200
@@ -8,8 +8,4 @@
 
 
 
-UNITYMisc = Main +
-constdefs
-  greaterThan :: [i,i]=> i
-  "greaterThan(u,A) == {x:A. u<x}"
-end
\ No newline at end of file
+UNITYMisc = Main
\ No newline at end of file