Conversion of UNITY/Distributor to Isar script. General tidy-up.
authorpaulson
Wed Jun 25 13:17:26 2003 +0200 (2003-06-25)
changeset 14072f932be305381
parent 14071 373806545656
child 14073 21e2ff495d81
Conversion of UNITY/Distributor to Isar script. General tidy-up.
src/ZF/IsaMakefile
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/ClientImpl.thy
src/ZF/UNITY/Distributor.ML
src/ZF/UNITY/Distributor.thy
src/ZF/UNITY/UNITYMisc.ML
src/ZF/UNITY/UNITYMisc.thy
     1.1 --- a/src/ZF/IsaMakefile	Tue Jun 24 16:32:59 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed Jun 25 13:17:26 2003 +0200
     1.3 @@ -121,8 +121,7 @@
     1.4    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     1.5    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
     1.6    UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     1.7 -  UNITY/ClientImpl.thy\
     1.8 -  UNITY/Distributor.ML UNITY/Distributor.thy\
     1.9 +  UNITY/ClientImpl.thy UNITY/Distributor.thy\
    1.10    UNITY/Follows.ML UNITY/Follows.thy\
    1.11    UNITY/Increasing.ML UNITY/Increasing.thy\
    1.12    UNITY/Merge.ML UNITY/Merge.thy\
     2.1 --- a/src/ZF/UNITY/AllocImpl.thy	Tue Jun 24 16:32:59 2003 +0200
     2.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Wed Jun 25 13:17:26 2003 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  constdefs
     2.5    alloc_giv_act :: i
     2.6    "alloc_giv_act ==
     2.7 -       {<s, t> : state*state.
     2.8 +       {<s, t> \<in> state*state.
     2.9  	\<exists>k. k = length(s`giv) &
    2.10              t = s(giv := s`giv @ [nth(k, s`ask)],
    2.11  		  available_tok := s`available_tok #- nth(k, s`ask)) &
    2.12 @@ -36,13 +36,13 @@
    2.13  
    2.14    alloc_rel_act :: i
    2.15    "alloc_rel_act ==
    2.16 -       {<s, t> : state*state.
    2.17 +       {<s, t> \<in> state*state.
    2.18          t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
    2.19  	      NbR := succ(s`NbR)) &
    2.20    	s`NbR < length(s`rel)}"
    2.21  
    2.22    (*The initial condition s`giv=[] is missing from the
    2.23 -    original definition -- S. O. Ehmety *)
    2.24 +    original definition: S. O. Ehmety *)
    2.25    alloc_prog :: i
    2.26    "alloc_prog ==
    2.27         mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
    2.28 @@ -146,8 +146,8 @@
    2.29  done
    2.30  
    2.31  lemma giv_Bounded_lemma2:
    2.32 -"[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
    2.33 -  ==> alloc_prog Join G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
    2.34 +"[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
    2.35 +  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
    2.36     {s\<in>state. s`available_tok #+ tokens(s`giv) =
    2.37      NbT #+ tokens(take(s`NbR, s`rel))})"
    2.38  apply (cut_tac giv_Bounded_lamma1)
    2.39 @@ -203,11 +203,11 @@
    2.40    asked for*)
    2.41  lemma alloc_prog_ask_prefix_giv:
    2.42       "alloc_prog \<in> Incr(lift(ask)) guarantees
    2.43 -                   Always({s\<in>state. <s`giv, s`ask>:prefix(tokbag)})"
    2.44 +                   Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})"
    2.45  apply (auto intro!: AlwaysI simp add: guar_def)
    2.46  apply (subgoal_tac "G \<in> preserves (lift (giv))")
    2.47   prefer 2 apply (simp add: alloc_prog_ok_iff)
    2.48 -apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
    2.49 +apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
    2.50         in stable_Join_Stable)
    2.51  apply constrains
    2.52   prefer 2 apply (simp add: lift_def, clarify)
    2.53 @@ -220,7 +220,7 @@
    2.54  
    2.55  lemma alloc_prog_transient_lemma:
    2.56       "[|G \<in> program; k\<in>nat|]
    2.57 -      ==> alloc_prog Join G \<in>
    2.58 +      ==> alloc_prog \<squnion> G \<in>
    2.59               transient({s\<in>state. k \<le> length(s`rel)} \<inter>
    2.60               {s\<in>state. succ(s`NbR) = k})"
    2.61  apply auto
    2.62 @@ -238,7 +238,7 @@
    2.63  
    2.64  lemma alloc_prog_rel_Stable_NbR_lemma:
    2.65      "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
    2.66 -     ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
    2.67 +     ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
    2.68  apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
    2.69  apply (blast intro: le_trans leI)
    2.70  apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
    2.71 @@ -250,11 +250,11 @@
    2.72  
    2.73  lemma alloc_prog_NbR_LeadsTo_lemma:
    2.74       "[| G \<in> program; alloc_prog ok G;
    2.75 -	 alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
    2.76 -      ==> alloc_prog Join G \<in>
    2.77 +	 alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
    2.78 +      ==> alloc_prog \<squnion> G \<in>
    2.79  	    {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
    2.80  	    LeadsTo {s\<in>state. k \<le> s`NbR}"
    2.81 -apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
    2.82 +apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
    2.83  apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
    2.84  apply (rule_tac [2] mono_length)
    2.85      prefer 3 apply simp
    2.86 @@ -269,9 +269,9 @@
    2.87  done
    2.88  
    2.89  lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
    2.90 -    "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
    2.91 +    "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
    2.92          k\<in>nat; n \<in> nat; n < k |]
    2.93 -      ==> alloc_prog Join G \<in>
    2.94 +      ==> alloc_prog \<squnion> G \<in>
    2.95  	    {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
    2.96  	       LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
    2.97  		 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
    2.98 @@ -279,7 +279,7 @@
    2.99  apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
   2.100         in LeadsTo_weaken_R)
   2.101  apply safe
   2.102 -apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   2.103 +apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   2.104  apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   2.105  apply (rule_tac [2] mono_length)
   2.106      prefer 3 apply simp
   2.107 @@ -301,9 +301,9 @@
   2.108  (* Lemma 49, page 28 *)
   2.109  
   2.110  lemma alloc_prog_NbR_LeadsTo_lemma3:
   2.111 -  "[|G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
   2.112 +  "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
   2.113       k\<in>nat|]
   2.114 -   ==> alloc_prog Join G \<in>
   2.115 +   ==> alloc_prog \<squnion> G \<in>
   2.116             {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
   2.117  (* Proof by induction over the difference between k and n *)
   2.118  apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
   2.119 @@ -326,8 +326,8 @@
   2.120  
   2.121  lemma alloc_prog_giv_Ensures_lemma:
   2.122  "[| G \<in> program; k\<in>nat; alloc_prog ok G;
   2.123 -  alloc_prog Join G \<in> Incr(lift(ask)) |] ==>
   2.124 -  alloc_prog Join G \<in>
   2.125 +  alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
   2.126 +  alloc_prog \<squnion> G \<in>
   2.127    {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   2.128    {s\<in>state.  k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
   2.129    Ensures {s\<in>state. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
   2.130 @@ -360,7 +360,7 @@
   2.131  
   2.132  lemma alloc_prog_giv_Stable_lemma:
   2.133  "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   2.134 -  ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
   2.135 +  ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
   2.136  apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
   2.137  apply (auto intro: leI)
   2.138  apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
   2.139 @@ -374,15 +374,15 @@
   2.140  
   2.141  lemma alloc_prog_giv_LeadsTo_lemma:
   2.142  "[| G \<in> program; alloc_prog ok G;
   2.143 -    alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
   2.144 - ==> alloc_prog Join G \<in>
   2.145 +    alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
   2.146 + ==> alloc_prog \<squnion> G \<in>
   2.147  	{s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   2.148  	{s\<in>state.  k < length(s`ask)} \<inter>
   2.149  	{s\<in>state. length(s`giv) = k}
   2.150  	LeadsTo {s\<in>state. k < length(s`giv)}"
   2.151 -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}")
   2.152 +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}")
   2.153  prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
   2.154 -apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
   2.155 +apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
   2.156  apply (drule PSP_Stable, assumption)
   2.157  apply (rule LeadsTo_weaken)
   2.158  apply (rule PSP_Stable)
   2.159 @@ -400,12 +400,12 @@
   2.160    (NbT) does not exceed the number currently available.*)
   2.161  lemma alloc_prog_Always_lemma:
   2.162  "[| G \<in> program; alloc_prog ok G;
   2.163 -    alloc_prog Join G \<in> Incr(lift(ask));
   2.164 -    alloc_prog Join G \<in> Incr(lift(rel)) |]
   2.165 -  ==> alloc_prog Join G \<in>
   2.166 +    alloc_prog \<squnion> G \<in> Incr(lift(ask));
   2.167 +    alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
   2.168 +  ==> alloc_prog \<squnion> G \<in>
   2.169          Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
   2.170                  NbT \<le> s`available_tok})"
   2.171 -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))}) ")
   2.172 +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))}) ")
   2.173  apply (rule_tac [2] AlwaysI)
   2.174  apply (rule_tac [3] giv_Bounded_lemma2, auto)
   2.175  apply (rule Always_weaken, assumption, auto)
   2.176 @@ -448,11 +448,11 @@
   2.177   fixes G
   2.178   assumes Gprog [intro,simp]: "G \<in> program"
   2.179       and okG [iff]:          "alloc_prog ok G"
   2.180 -     and Incr_rel [intro]:   "alloc_prog Join G \<in> Incr(lift(rel))"
   2.181 -     and Incr_ask [intro]:   "alloc_prog Join G \<in> Incr(lift(ask))"
   2.182 -     and safety:   "alloc_prog Join G
   2.183 +     and Incr_rel [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(rel))"
   2.184 +     and Incr_ask [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(ask))"
   2.185 +     and safety:   "alloc_prog \<squnion> G
   2.186                        \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
   2.187 -     and progress: "alloc_prog Join G
   2.188 +     and progress: "alloc_prog \<squnion> G
   2.189                        \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
   2.190                          {s\<in>state. k \<le> tokens(s`rel)})"
   2.191  
   2.192 @@ -461,7 +461,7 @@
   2.193    will eventually recognize that they've been released.*)
   2.194  lemma (in alloc_progress) tokens_take_NbR_lemma:
   2.195   "k \<in> tokbag
   2.196 -  ==> alloc_prog Join G \<in>
   2.197 +  ==> alloc_prog \<squnion> G \<in>
   2.198          {s\<in>state. k \<le> tokens(s`rel)}
   2.199          LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   2.200  apply (rule single_LeadsTo_I, safe)
   2.201 @@ -480,7 +480,7 @@
   2.202    LeadsTo *)
   2.203  lemma (in alloc_progress) tokens_take_NbR_lemma2:
   2.204       "k \<in> tokbag
   2.205 -      ==> alloc_prog Join G \<in>
   2.206 +      ==> alloc_prog \<squnion> G \<in>
   2.207  	    {s\<in>state. tokens(s`giv) = k}
   2.208  	    LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   2.209  apply (rule LeadsTo_Trans)
   2.210 @@ -493,7 +493,7 @@
   2.211  (*Third step in proof of (31): by PSP with the fact that giv increases *)
   2.212  lemma (in alloc_progress) length_giv_disj:
   2.213       "[| k \<in> tokbag; n \<in> nat |]
   2.214 -      ==> alloc_prog Join G \<in>
   2.215 +      ==> alloc_prog \<squnion> G \<in>
   2.216  	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   2.217  	    LeadsTo
   2.218  	      {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
   2.219 @@ -513,7 +513,7 @@
   2.220  (*Fourth step in proof of (31): we apply lemma (51) *)
   2.221  lemma (in alloc_progress) length_giv_disj2:
   2.222       "[|k \<in> tokbag; n \<in> nat|]
   2.223 -      ==> alloc_prog Join G \<in>
   2.224 +      ==> alloc_prog \<squnion> G \<in>
   2.225  	    {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   2.226  	    LeadsTo
   2.227  	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   2.228 @@ -526,7 +526,7 @@
   2.229    k\<in>nat *)
   2.230  lemma (in alloc_progress) length_giv_disj3:
   2.231       "n \<in> nat
   2.232 -      ==> alloc_prog Join G \<in>
   2.233 +      ==> alloc_prog \<squnion> G \<in>
   2.234  	    {s\<in>state. length(s`giv) = n}
   2.235  	    LeadsTo
   2.236  	      {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   2.237 @@ -541,7 +541,7 @@
   2.238    assumption that ask increases *)
   2.239  lemma (in alloc_progress) length_ask_giv:
   2.240   "[|k \<in> nat;  n < k|]
   2.241 -  ==> alloc_prog Join G \<in>
   2.242 +  ==> alloc_prog \<squnion> G \<in>
   2.243          {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   2.244          LeadsTo
   2.245            {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   2.246 @@ -564,7 +564,7 @@
   2.247  (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   2.248  lemma (in alloc_progress) length_ask_giv2:
   2.249       "[|k \<in> nat;  n < k|]
   2.250 -      ==> alloc_prog Join G \<in>
   2.251 +      ==> alloc_prog \<squnion> G \<in>
   2.252  	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   2.253  	    LeadsTo
   2.254  	      {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   2.255 @@ -581,7 +581,7 @@
   2.256  (*Eighth step in proof of (31): by 50, we get |giv| > n. *)
   2.257  lemma (in alloc_progress) extend_giv:
   2.258       "[| k \<in> nat;  n < k|]
   2.259 -      ==> alloc_prog Join G \<in>
   2.260 +      ==> alloc_prog \<squnion> G \<in>
   2.261  	    {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   2.262  	    LeadsTo {s\<in>state. n < length(s`giv)}"
   2.263  apply (rule LeadsTo_Un_duplicate)
   2.264 @@ -597,7 +597,7 @@
   2.265    we can't expect |ask| to remain fixed until |giv| increases.*)
   2.266  lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
   2.267   "k \<in> nat
   2.268 -  ==> alloc_prog Join G \<in>
   2.269 +  ==> alloc_prog \<squnion> G \<in>
   2.270          {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
   2.271  (* Proof by induction over the difference between k and n *)
   2.272  apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct)
   2.273 @@ -622,9 +622,9 @@
   2.274  (*Final lemma: combine previous result with lemma (30)*)
   2.275  lemma (in alloc_progress) final:
   2.276       "h \<in> list(tokbag)
   2.277 -      ==> alloc_prog Join G \<in>
   2.278 -	    {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   2.279 -	    {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   2.280 +      ==> alloc_prog \<squnion> G
   2.281 +            \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   2.282 +	      {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   2.283  apply (rule single_LeadsTo_I)
   2.284   prefer 2 apply simp
   2.285  apply (rename_tac s0)
     3.1 --- a/src/ZF/UNITY/ClientImpl.thy	Tue Jun 24 16:32:59 2003 +0200
     3.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Wed Jun 25 13:17:26 2003 +0200
     3.3 @@ -8,6 +8,22 @@
     3.4  
     3.5  
     3.6  theory ClientImpl = AllocBase + Guar:
     3.7 +
     3.8 +(*????MOVE UP*)
     3.9 +method_setup constrains = {*
    3.10 +    Method.ctxt_args (fn ctxt =>
    3.11 +        Method.METHOD (fn facts =>
    3.12 +            gen_constrains_tac (Classical.get_local_claset ctxt,
    3.13 +                               Simplifier.get_local_simpset ctxt) 1)) *}
    3.14 +    "for proving safety properties"
    3.15 +
    3.16 +(*For using "disjunction" (union over an index set) to eliminate a variable.
    3.17 +  ????move way up*)
    3.18 +lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
    3.19 +      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
    3.20 +by blast
    3.21 +
    3.22 +
    3.23  consts
    3.24    ask :: i (* input history:  tokens requested *)
    3.25    giv :: i (* output history: tokens granted *)
    3.26 @@ -66,20 +82,6 @@
    3.27  declare type_assumes [simp] default_val_assumes [simp]
    3.28  (* This part should be automated *)
    3.29  
    3.30 -(*????MOVE UP*)
    3.31 -method_setup constrains = {*
    3.32 -    Method.ctxt_args (fn ctxt =>
    3.33 -        Method.METHOD (fn facts =>
    3.34 -            gen_constrains_tac (Classical.get_local_claset ctxt,
    3.35 -                               Simplifier.get_local_simpset ctxt) 1)) *}
    3.36 -    "for proving safety properties"
    3.37 -
    3.38 -(*For using "disjunction" (union over an index set) to eliminate a variable.
    3.39 -  ????move way up*)
    3.40 -lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
    3.41 -      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
    3.42 -by blast
    3.43 -
    3.44  lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
    3.45  apply (unfold state_def)
    3.46  apply (drule_tac a = ask in apply_type, auto)
    3.47 @@ -164,7 +166,7 @@
    3.48  
    3.49  lemma ask_Bounded_lemma: 
    3.50  "[| client_prog ok G; G \<in> program |] 
    3.51 -      ==> client_prog Join G \<in>    
    3.52 +      ==> client_prog \<squnion> G \<in>    
    3.53                Always({s \<in> state. s`tok \<le> NbT}  Int   
    3.54                        {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
    3.55  apply (rotate_tac -1)
    3.56 @@ -194,15 +196,15 @@
    3.57  by (constrains, auto)
    3.58  
    3.59  lemma client_prog_Join_Stable_rel_le_giv: 
    3.60 -"[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
    3.61 -    ==> client_prog Join G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
    3.62 +"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
    3.63 +    ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
    3.64  apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
    3.65  apply (auto simp add: lift_def)
    3.66  done
    3.67  
    3.68  lemma client_prog_Join_Always_rel_le_giv:
    3.69 -     "[| client_prog Join G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
    3.70 -    ==> client_prog Join G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
    3.71 +     "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]  
    3.72 +    ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
    3.73  by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
    3.74  
    3.75  lemma def_act_eq:
    3.76 @@ -243,8 +245,8 @@
    3.77  done
    3.78  
    3.79  lemma induct_lemma: 
    3.80 -"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
    3.81 -  ==> client_prog Join G \<in>  
    3.82 +"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
    3.83 +  ==> client_prog \<squnion> G \<in>  
    3.84    {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)  
    3.85     & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
    3.86          LeadsTo {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)  
    3.87 @@ -272,8 +274,8 @@
    3.88  done
    3.89  
    3.90  lemma rel_progress_lemma: 
    3.91 -"[| client_prog Join G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
    3.92 -  ==> client_prog Join G  \<in>  
    3.93 +"[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]  
    3.94 +  ==> client_prog \<squnion> G  \<in>  
    3.95       {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)  
    3.96             & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
    3.97                        LeadsTo {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
    3.98 @@ -301,11 +303,12 @@
    3.99  done
   3.100  
   3.101  lemma progress_lemma: 
   3.102 -"[| client_prog Join G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
   3.103 - ==> client_prog Join G  \<in>  
   3.104 -      {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
   3.105 -      LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
   3.106 -apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], assumption)
   3.107 +"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |] 
   3.108 + ==> client_prog \<squnion> G
   3.109 +       \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}   
   3.110 +         LeadsTo  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
   3.111 +apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], 
   3.112 +       assumption)
   3.113  apply (force simp add: client_prog_ok_iff)
   3.114  apply (rule LeadsTo_weaken_L) 
   3.115  apply (rule LeadsTo_Un [OF rel_progress_lemma 
   3.116 @@ -331,4 +334,4 @@
   3.117                        cons_Int_distrib safety_prop_Acts_iff)
   3.118  done
   3.119  
   3.120 -end
   3.121 \ No newline at end of file
   3.122 +end
     4.1 --- a/src/ZF/UNITY/Distributor.ML	Tue Jun 24 16:32:59 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,162 +0,0 @@
     4.4 -(*  Title: ZF/UNITY/Distributor
     4.5 -    ID:         $Id$
     4.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 -    Copyright   2002  University of Cambridge
     4.8 -
     4.9 -A multiple-client allocator from a single-client allocator:
    4.10 -Distributor specification
    4.11 -*)
    4.12 -
    4.13 -Open_locale "Distributor";
    4.14 -val all_distinct_vars = thm "all_distinct_vars";
    4.15 -val var_assumes = thm "var_assumes";
    4.16 -val type_assumes = thm "type_assumes";
    4.17 -val default_val_assumes  = thm "default_val_assumes";
    4.18 -
    4.19 -Addsimps [var_assumes, default_val_assumes,  type_assumes];
    4.20 -
    4.21 -Goalw [state_def]
    4.22 -"s \\<in> state ==> s`In \\<in> list(A)";
    4.23 -by (dres_inst_tac [("a", "In")] apply_type 1);
    4.24 -by Auto_tac;
    4.25 -qed "In_value_type";
    4.26 -AddTCs [In_value_type];
    4.27 -Addsimps [In_value_type];
    4.28 -
    4.29 -Goalw [state_def]
    4.30 -"s \\<in> state ==> s`iIn \\<in> list(nat)";
    4.31 -by (dres_inst_tac [("a", "iIn")] apply_type 1);
    4.32 -by Auto_tac;
    4.33 -qed "iIn_value_type";
    4.34 -AddTCs [iIn_value_type];
    4.35 -Addsimps [iIn_value_type];
    4.36 -
    4.37 -Goalw [state_def]
    4.38 -"s \\<in> state ==> s`Out(n):list(A)";
    4.39 -by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
    4.40 -by Auto_tac;
    4.41 -qed "Out_value_type";
    4.42 -AddTCs [Out_value_type];
    4.43 -Addsimps [Out_value_type];
    4.44 -
    4.45 -val distrib = thm "distr_spec";
    4.46 -
    4.47 -Goal "D \\<in> program";
    4.48 -by (cut_facts_tac [distrib] 1);
    4.49 -by (auto_tac (claset(), simpset() addsimps 
    4.50 -           [distr_spec_def, distr_allowed_acts_def]));
    4.51 -qed "D_in_program";
    4.52 -Addsimps [D_in_program];
    4.53 -AddTCs [D_in_program];
    4.54 -
    4.55 -Goal "G \\<in> program ==> \
    4.56 -\   D ok G <-> \
    4.57 -\  ((\\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n)))) & D \\<in> Allowed(G))";
    4.58 -by (cut_facts_tac [distrib] 1);
    4.59 -by (auto_tac (claset(), 
    4.60 -     simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def, 
    4.61 -                         Allowed_def, ok_iff_Allowed]));
    4.62 -by (rotate_tac ~1 2);
    4.63 -by (dres_inst_tac [("x", "G")] bspec 2);
    4.64 -by Auto_tac;
    4.65 -by (dresolve_tac [rotate_prems 1 (safety_prop_Acts_iff RS iffD1)] 1);
    4.66 -by (auto_tac (claset() addIs [safety_prop_Inter], simpset()));
    4.67 -qed "D_ok_iff";
    4.68 -
    4.69 -Goal 
    4.70 -"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
    4.71 -\     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
    4.72 -\     Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt<Nclients})) \
    4.73 -\     guarantees \
    4.74 -\         (\\<Inter>n \\<in> Nclients. lift(Out(n)) IncreasingWrt \
    4.75 -\                           prefix(A)/list(A))";
    4.76 -by (cut_facts_tac [D_in_program, distrib] 1);
    4.77 -by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
    4.78 -by (auto_tac (claset() addSIs [guaranteesI]  addIs [Follows_imp_Increasing_left]
    4.79 -                        addSDs [guaranteesD], 
    4.80 -               simpset()));
    4.81 -qed "distr_Increasing_Out";
    4.82 -
    4.83 -val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
    4.84 -
    4.85 -Goal
    4.86 -"[| \\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n))); \
    4.87 -\  D Join G \\<in> Always({s \\<in> state. \
    4.88 -\         \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |] \
    4.89 -\ ==> D Join G : Always \
    4.90 -\         ({s \\<in> state. msetsum(%n. bag_of (sublist(s`In, \
    4.91 -\                      {k \\<in> nat. k < length(s`iIn) &\
    4.92 -\                         nth(k, s`iIn)= n})), \
    4.93 -\                        Nclients, A) = \
    4.94 -\             bag_of(sublist(s`In, length(s`iIn)))})";
    4.95 -by (cut_facts_tac [D_in_program] 1);
    4.96 -by (subgoal_tac "G \\<in> program" 1);
    4.97 -by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
    4.98 -by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
    4.99 -by Auto_tac;
   4.100 -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
   4.101 -by (asm_simp_tac (simpset() addsimps [nat_into_Finite]) 1); 
   4.102 -by (Blast_tac 1); 
   4.103 -by (Asm_simp_tac 1);
   4.104 -by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1); 
   4.105 -by (subgoal_tac
   4.106 -    "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
   4.107 -\    length(x`iIn)" 1);
   4.108 -by (Asm_simp_tac 1);
   4.109 -by (resolve_tac [equalityI] 1);
   4.110 -by Safe_tac;
   4.111 -by (asm_full_simp_tac (simpset() addsimps [ltD]) 1);
   4.112 -by (subgoal_tac "length(x ` iIn) : nat" 1);
   4.113 -by Typecheck_tac; 
   4.114 -by (subgoal_tac "xa : nat" 1); 
   4.115 -by (dres_inst_tac [("x", "nth(xa, x`iIn)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec  1);
   4.116 -by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
   4.117 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
   4.118 -by (blast_tac (claset() addDs [ltD]) 1); 
   4.119 -by (blast_tac (claset() addIs [lt_trans]) 1);
   4.120 -qed "distr_bag_Follows_lemma";
   4.121 -
   4.122 -Goal
   4.123 - "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
   4.124 -\      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
   4.125 -\       Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})) \
   4.126 -\     guarantees  \
   4.127 -\      (\\<Inter>n \\<in> Nclients. \
   4.128 -\       (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A)) \
   4.129 -\       Fols \
   4.130 -\       (%s. bag_of(sublist(s`In, length(s`iIn)))) \
   4.131 -\       Wrt MultLe(A, r)/Mult(A))";
   4.132 -by (cut_facts_tac [distrib] 1);
   4.133 -by (rtac guaranteesI 1);
   4.134 -by (Clarify_tac 1); 
   4.135 -by (Simp_tac 2);
   4.136 -by (rtac (distr_bag_Follows_lemma RS Always_Follows2) 1);
   4.137 -by Auto_tac;  
   4.138 -by (rtac Follows_state_ofD1 2);
   4.139 -by (rtac Follows_msetsum_UN 2);
   4.140 -by (ALLGOALS(Clarify_tac));
   4.141 -by (resolve_tac [conjI] 3);
   4.142 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 3);
   4.143 -by (resolve_tac [conjI] 4);
   4.144 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 4);
   4.145 -by (resolve_tac [conjI] 5);
   4.146 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
   4.147 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
   4.148 -by (Clarify_tac 4);
   4.149 -by (Asm_full_simp_tac 3);
   4.150 -by (Asm_full_simp_tac 3);
   4.151 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
   4.152 -by (rotate_tac 2 1);
   4.153 -by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
   4.154 -by (auto_tac (claset(), 
   4.155 -              simpset() addsimps [distr_spec_def, distr_follows_def]));
   4.156 -by (dtac guaranteesD 1); 
   4.157 -by (assume_tac 1);
   4.158 -by (Force_tac 1); 
   4.159 -by (Force_tac 1); 
   4.160 -by (asm_full_simp_tac
   4.161 -    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
   4.162 -             refl_prefix, trans_on_MultLe] 
   4.163 -            addcongs [Follows_cong]) 1); 
   4.164 -qed  "distr_bag_Follows";
   4.165 -Close_locale "Distributor";
     5.1 --- a/src/ZF/UNITY/Distributor.thy	Tue Jun 24 16:32:59 2003 +0200
     5.2 +++ b/src/ZF/UNITY/Distributor.thy	Wed Jun 25 13:17:26 2003 +0200
     5.3 @@ -6,44 +6,160 @@
     5.4  A multiple-client allocator from a single-client allocator:
     5.5  Distributor specification
     5.6  *)
     5.7 -Distributor = AllocBase + Follows +  Guar + GenPrefix +
     5.8 -(** Distributor specification (the number of outputs is Nclients) ***)
     5.9 - (*spec (14)*)
    5.10 -constdefs  
    5.11 -  distr_follows :: [i, i, i, i =>i] =>i
    5.12 +
    5.13 +theory Distributor = AllocBase + Follows +  Guar + GenPrefix:
    5.14 +
    5.15 +text{*Distributor specification (the number of outputs is Nclients)*}
    5.16 +
    5.17 +text{*spec (14)*}
    5.18 +constdefs
    5.19 +  distr_follows :: "[i, i, i, i =>i] =>i"
    5.20      "distr_follows(A, In, iIn, Out) ==
    5.21 -     (lift(In) IncreasingWrt prefix(A)/list(A)) Int
    5.22 -     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
    5.23 -     Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})
    5.24 +     (lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
    5.25 +     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
    5.26 +     Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients})
    5.27           guarantees
    5.28 -         (\\<Inter>n \\<in> Nclients.
    5.29 +         (\<Inter>n \<in> Nclients.
    5.30            lift(Out(n))
    5.31                Fols
    5.32 -          (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
    5.33 +          (%s. sublist(s`In, {k \<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
    5.34  	  Wrt prefix(A)/list(A))"
    5.35 -  
    5.36 - distr_allowed_acts :: [i=>i]=>i
    5.37 -  "distr_allowed_acts(Out) ==
    5.38 -   {D:program. AllowedActs(D) =
    5.39 -   cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
    5.40 +
    5.41 +  distr_allowed_acts :: "[i=>i]=>i"
    5.42 +    "distr_allowed_acts(Out) ==
    5.43 +     {D \<in> program. AllowedActs(D) =
    5.44 +     cons(id(state), \<Union>G \<in> (\<Inter>n\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
    5.45 +
    5.46 +  distr_spec :: "[i, i, i, i =>i]=>i"
    5.47 +    "distr_spec(A, In, iIn, Out) ==
    5.48 +     distr_follows(A, In, iIn, Out) \<inter> distr_allowed_acts(Out)"
    5.49 +
    5.50 +locale distr =
    5.51 +  fixes In  --{*items to distribute*}
    5.52 +    and iIn --{*destinations of items to distribute*}
    5.53 +    and Out --{*distributed items*}
    5.54 +    and A   --{*the type of items being distributed *}
    5.55 +    and D
    5.56 + assumes
    5.57 +     var_assumes [simp]:  "In \<in> var & iIn \<in> var & (\<forall>n. Out(n):var)"
    5.58 + and all_distinct_vars:   "\<forall>n. all_distinct([In, iIn, iOut(n)])"
    5.59 + and type_assumes [simp]: "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
    5.60 +                          (\<forall>n. type_of(Out(n))=list(A))"
    5.61 + and default_val_assumes [simp]:
    5.62 +                         "default_val(In)=Nil &
    5.63 +                          default_val(iIn)=Nil &
    5.64 +                          (\<forall>n. default_val(Out(n))=Nil)"
    5.65 + and distr_spec:  "D \<in> distr_spec(A, In, iIn, Out)"
    5.66 +
    5.67  
    5.68 -  distr_spec :: [i, i, i, i =>i]=>i
    5.69 -  "distr_spec(A, In, iIn, Out) ==
    5.70 -   distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)"
    5.71 +lemma (in distr) In_value_type [simp,TC]: "s \<in> state ==> s`In \<in> list(A)"
    5.72 +apply (unfold state_def)
    5.73 +apply (drule_tac a = In in apply_type, auto)
    5.74 +done
    5.75 +
    5.76 +lemma (in distr) iIn_value_type [simp,TC]:
    5.77 +     "s \<in> state ==> s`iIn \<in> list(nat)"
    5.78 +apply (unfold state_def)
    5.79 +apply (drule_tac a = iIn in apply_type, auto)
    5.80 +done
    5.81 +
    5.82 +lemma (in distr) Out_value_type [simp,TC]:
    5.83 +     "s \<in> state ==> s`Out(n):list(A)"
    5.84 +apply (unfold state_def)
    5.85 +apply (drule_tac a = "Out (n)" in apply_type)
    5.86 +apply auto
    5.87 +done
    5.88 +
    5.89 +lemma (in distr) D_in_program [simp,TC]: "D \<in> program"
    5.90 +apply (cut_tac distr_spec)
    5.91 +apply (auto simp add: distr_spec_def distr_allowed_acts_def)
    5.92 +done
    5.93 +
    5.94 +lemma (in distr) D_ok_iff:
    5.95 +     "G \<in> program ==>
    5.96 +	D ok G <-> ((\<forall>n \<in> nat. G \<in> preserves(lift(Out(n)))) & D \<in> Allowed(G))"
    5.97 +apply (cut_tac distr_spec)
    5.98 +apply (auto simp add: INT_iff distr_spec_def distr_allowed_acts_def
    5.99 +                      Allowed_def ok_iff_Allowed)
   5.100 +apply (drule_tac [2] x = G and P = "%y. x \<notin> Acts(y)" in bspec)
   5.101 +apply auto
   5.102 +apply (drule safety_prop_Acts_iff [THEN [2] rev_iffD1])
   5.103 +apply (auto intro: safety_prop_Inter)
   5.104 +done
   5.105  
   5.106 -locale Distributor =
   5.107 -  fixes In :: i  (*items to distribute*)
   5.108 -        iIn :: i (*destinations of items to distribute*)
   5.109 -        Out :: i=>i  (*distributed items*)
   5.110 -        A :: i   (*the type of items being distributed *)
   5.111 -        D :: i
   5.112 - assumes
   5.113 -    var_assumes       "In:var & iIn:var & (\\<forall>n. Out(n):var)"
   5.114 -    all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])"
   5.115 -    type_assumes      "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
   5.116 -                       (\\<forall>n. type_of(Out(n))=list(A))"
   5.117 -   default_val_assumes "default_val(In)=Nil &
   5.118 -                        default_val(iIn)=Nil &
   5.119 -                        (\\<forall>n. default_val(Out(n))=Nil)"
   5.120 -   distr_spec  "D:distr_spec(A, In, iIn, Out)"
   5.121 +lemma (in distr) distr_Increasing_Out:
   5.122 +"D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
   5.123 +      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
   5.124 +      Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt<Nclients}))
   5.125 +      guarantees
   5.126 +          (\<Inter>n \<in> Nclients. lift(Out(n)) IncreasingWrt
   5.127 +                            prefix(A)/list(A))"
   5.128 +apply (cut_tac D_in_program distr_spec)
   5.129 +apply (simp (no_asm_use) add: distr_spec_def distr_follows_def)
   5.130 +apply (auto intro!: guaranteesI intro: Follows_imp_Increasing_left 
   5.131 +            dest!: guaranteesD)
   5.132 +done
   5.133 +
   5.134 +lemma (in distr) distr_bag_Follows_lemma:
   5.135 +"[| \<forall>n \<in> nat. G \<in> preserves(lift(Out(n)));
   5.136 +   D \<squnion> G \<in> Always({s \<in> state.
   5.137 +          \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}) |]
   5.138 +  ==> D \<squnion> G \<in> Always
   5.139 +          ({s \<in> state. msetsum(%n. bag_of (sublist(s`In,
   5.140 +                       {k \<in> nat. k < length(s`iIn) &
   5.141 +                          nth(k, s`iIn)= n})),
   5.142 +                         Nclients, A) =
   5.143 +              bag_of(sublist(s`In, length(s`iIn)))})"
   5.144 +apply (cut_tac D_in_program)
   5.145 +apply (subgoal_tac "G \<in> program")
   5.146 + prefer 2 apply (blast dest: preserves_type [THEN subsetD])
   5.147 +apply (erule Always_Diff_Un_eq [THEN iffD1])
   5.148 +apply (rule state_AlwaysI [THEN Always_weaken], auto)
   5.149 +apply (rename_tac s)
   5.150 +apply (subst bag_of_sublist_UN_disjoint [symmetric])
   5.151 +   apply (simp (no_asm_simp) add: nat_into_Finite)
   5.152 +  apply blast
   5.153 + apply (simp (no_asm_simp))
   5.154 +apply (simp add: set_of_list_conv_nth [of _ nat])
   5.155 +apply (subgoal_tac
   5.156 +       "(\<Union>i \<in> Nclients. {k\<in>nat. k < length(s`iIn) & nth(k, s`iIn) = i}) =
   5.157 +        length(s`iIn) ")
   5.158 +apply (simp (no_asm_simp))
   5.159 +apply (rule equalityI)
   5.160 +apply (force simp add: ltD, safe)
   5.161 +apply (rename_tac m)
   5.162 +apply (subgoal_tac "length (s ` iIn) \<in> nat")
   5.163 +apply typecheck
   5.164 +apply (subgoal_tac "m \<in> nat")
   5.165 +apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
   5.166 +apply (simp add: ltI)
   5.167 +apply (simp_all add: Ord_mem_iff_lt)
   5.168 +apply (blast dest: ltD)
   5.169 +apply (blast intro: lt_trans)
   5.170 +done
   5.171 +
   5.172 +theorem (in distr) distr_bag_Follows:
   5.173 + "D \<in> ((lift(In) IncreasingWrt prefix(A)/list(A)) \<inter>
   5.174 +       (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) \<inter>
   5.175 +        Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iIn). elt < Nclients}))
   5.176 +      guarantees
   5.177 +       (\<Inter>n \<in> Nclients.
   5.178 +        (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A))
   5.179 +        Fols
   5.180 +        (%s. bag_of(sublist(s`In, length(s`iIn))))
   5.181 +        Wrt MultLe(A, r)/Mult(A))"
   5.182 +apply (cut_tac distr_spec)
   5.183 +apply (rule guaranteesI, clarify)
   5.184 +apply (rule distr_bag_Follows_lemma [THEN Always_Follows2])
   5.185 +apply (simp add: D_ok_iff, auto)
   5.186 +apply (rule Follows_state_ofD1)
   5.187 +apply (rule Follows_msetsum_UN)
   5.188 +   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
   5.189 +apply (auto simp add: distr_spec_def distr_follows_def)
   5.190 +apply (drule guaranteesD, assumption)
   5.191 +apply (simp_all cong add: Follows_cong
   5.192 +    add: refl_prefix
   5.193 +       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
   5.194 +done
   5.195 +
   5.196  end
     6.1 --- a/src/ZF/UNITY/UNITYMisc.ML	Tue Jun 24 16:32:59 2003 +0200
     6.2 +++ b/src/ZF/UNITY/UNITYMisc.ML	Wed Jun 25 13:17:26 2003 +0200
     6.3 @@ -7,11 +7,6 @@
     6.4  
     6.5  *)
     6.6  
     6.7 -Goalw [greaterThan_def]
     6.8 -"i:greaterThan(k,A) <-> i:A & k<i";
     6.9 -by Auto_tac;
    6.10 -qed "greaterThan_iff";
    6.11 -
    6.12  (** Ad-hoc set-theory rules **)
    6.13  
    6.14  Goal "Union(B) Int A = (UN b:B. b Int A)";
    6.15 @@ -22,11 +17,6 @@
    6.16  by Auto_tac;
    6.17  qed "Int_Union_Union2";
    6.18  
    6.19 -Goal "A Un B - (A - B) = B";
    6.20 -by (Blast_tac 1);
    6.21 -qed "Un_Diff_Diff";
    6.22 -AddIffs [Un_Diff_Diff];
    6.23 -
    6.24  
    6.25  (** Needed in State theory for the current definition of variables 
    6.26  where they are indexed by lists  **)
    6.27 @@ -38,22 +28,17 @@
    6.28  qed "list_nat_into_univ";
    6.29  
    6.30  
    6.31 -(** Simplication rules for Collect; ????
    6.32 -  At least change to "{x:A. P(x)} Int A = {x : A Int B. P(x)} **)
    6.33 -
    6.34 -Goal "{x:A. P(x)} Int A = {x:A. P(x)}";
    6.35 -by Auto_tac;
    6.36 -qed "Collect_Int2";
    6.37 +(** Simplication rules for Collect **)
    6.38  
    6.39 -Goal "A Int {x:A. P(x)} = {x:A. P(x)}";
    6.40 +(*Currently unused*)
    6.41 +Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}";
    6.42  by Auto_tac;
    6.43 -qed "Collect_Int3";
    6.44 +qed "Collect_Int_left";
    6.45  
    6.46 -(*????????????????*)
    6.47 -AddIffs [Collect_Int2, Collect_Int3];
    6.48 -
    6.49 -
    6.50 -(*for main ZF????*)
    6.51 +(*Currently unused*)
    6.52 +Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}";
    6.53 +by Auto_tac;
    6.54 +qed "Collect_Int_right";
    6.55  
    6.56  Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
    6.57  by Auto_tac;
     7.1 --- a/src/ZF/UNITY/UNITYMisc.thy	Tue Jun 24 16:32:59 2003 +0200
     7.2 +++ b/src/ZF/UNITY/UNITYMisc.thy	Wed Jun 25 13:17:26 2003 +0200
     7.3 @@ -8,8 +8,4 @@
     7.4  
     7.5  
     7.6  
     7.7 -UNITYMisc = Main +
     7.8 -constdefs
     7.9 -  greaterThan :: [i,i]=> i
    7.10 -  "greaterThan(u,A) == {x:A. u<x}"
    7.11 -end
    7.12 \ No newline at end of file
    7.13 +UNITYMisc = Main
    7.14 \ No newline at end of file