# HG changeset patch
# User paulson
# Date 1054221000 -7200
# Node ID 4daa384f4fd7f58c4093fb3412eb8cc415e1f394
# Parent  e9c9f69e4f63a7bd4862907bde8ee027088e26b9
Introduction of the theories UNITY/Merge, UNITY/ClientImpl

diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/IsaMakefile	Thu May 29 17:10:00 2003 +0200
@@ -121,9 +121,11 @@
   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/ClientImpl.ML UNITY/ClientImpl.thy\
   UNITY/Distributor.ML UNITY/Distributor.thy\
   UNITY/Follows.ML UNITY/Follows.thy\
   UNITY/Increasing.ML UNITY/Increasing.thy\
+  UNITY/Merge.ML UNITY/Merge.thy\
   UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
   UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
   UNITY/WFair.ML UNITY/WFair.thy
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/AllocBase.ML
--- a/src/ZF/UNITY/AllocBase.ML	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.ML	Thu May 29 17:10:00 2003 +0200
@@ -42,7 +42,7 @@
 \     (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
 \     setsum(f, n) $<= setsum(g,n)";
 by (induct_tac "n" 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [])));
+by (ALLGOALS Asm_full_simp_tac);
 by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
 by (Clarify_tac 1);
 by (Asm_simp_tac 1);
@@ -54,8 +54,7 @@
 by (Clarify_tac 1);
 by (dtac leI 1);
 by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [nat_into_Finite,
-                                      mem_not_refl, succ_def]) 1);
+by (asm_simp_tac (simpset() addsimps [nat_into_Finite, mem_not_refl, succ_def]) 1);
 qed_spec_mp "setsum_fun_mono";
 
 Goal "l:list(A) ==> tokens(l):nat";
@@ -218,7 +217,7 @@
 by (subgoal_tac
       "B Int C Int length(l) = \
 \      (B Int length(l)) Int (C Int length(l))" 1);
-by (blast_tac (claset() addIs []) 2);
+by (Blast_tac 2);
 by (asm_simp_tac (simpset() addsimps [bag_of_sublist, 
                                       Int_Un_distrib2, msetsum_Un_Int]) 1); 
 by (resolve_tac [msetsum_Un_Int] 1);
@@ -314,7 +313,8 @@
 bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
 
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
-fun list_of_Int th = 
+fun list_of_Int th = list_of_Int_aux (Drule.freeze_all th)
+and list_of_Int_aux th =
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
     handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
     handle THM _ => (list_of_Int (th RS InterD))
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/ClientImpl.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ClientImpl.ML	Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,309 @@
+(*  Title:      ZF/UNITY/Client.ML
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Distributed Resource Management System: the Client
+*)
+Addsimps [type_assumes, default_val_assumes];
+(* This part should be automated *)
+
+Goalw [state_def] "s:state ==> s`ask:list(nat)";
+by (dres_inst_tac [("a", "ask")] apply_type 1);
+by Auto_tac;
+qed "ask_value_type";
+AddTCs [ask_value_type];
+Addsimps [ask_value_type];
+
+Goalw [state_def] "s:state ==> s`giv:list(nat)";
+by (dres_inst_tac [("a", "giv")] apply_type 1);
+by Auto_tac;
+qed "giv_value_type";
+AddTCs [giv_value_type];
+Addsimps [giv_value_type];
+
+Goalw [state_def]
+"s:state ==> s`rel:list(nat)";
+by (dres_inst_tac [("a", "rel")] apply_type 1);
+by Auto_tac;
+qed "rel_value_type";
+AddTCs [rel_value_type];
+Addsimps [rel_value_type];
+
+Goalw [state_def] "s:state ==> s`tok:nat";
+by (dres_inst_tac [("a", "tok")] apply_type 1);
+by Auto_tac;
+qed "tok_value_type";
+AddTCs [tok_value_type];
+Addsimps [tok_value_type];
+
+(** The Client Program **)
+
+Goalw [client_prog_def] "client_prog:program";
+by (Simp_tac 1);
+qed "client_type";
+Addsimps [client_type];
+AddTCs [client_type];
+
+Addsimps [client_prog_def RS def_prg_Init, 
+          client_prog_def RS def_prg_AllowedActs];
+program_defs_ref := [client_prog_def];
+
+Addsimps (map simp_of_act [client_rel_act_def, 
+client_tok_act_def, client_ask_act_def]);
+
+Goal "ALL G:program. (client_prog ok G) <-> \
+\  (G:preserves(lift(rel)) & G:preserves(lift(ask)) & \
+\   G:preserves(lift(tok)) &  client_prog:Allowed(G))";
+by (auto_tac (claset(), 
+     simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed]));  
+qed "client_prog_ok_iff";
+
+Goal "client_prog:(INT x:var-{ask, rel, tok}. preserves(lift(x)))";
+by (rtac Inter_var_DiffI 1);
+by (rtac ballI 2);
+by (rtac preservesI 2);
+by (constrains_tac 2);
+by Auto_tac;
+qed "client_prog_preserves";
+
+
+(*Safety property 1: ask, rel are increasing : (24) *)
+Goalw [guar_def]
+"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))";
+by (auto_tac (claset() addSIs [increasing_imp_Increasing],
+        simpset() addsimps [client_prog_ok_iff, increasing_def]));
+by (ALLGOALS(constrains_tac));
+by (ALLGOALS(thin_tac "mk_program(?u, ?v, ?w):Allowed(?x)"));
+by (auto_tac (claset() addDs [ActsD], simpset()));
+by (dres_inst_tac [("f", "lift(rel)")] preserves_imp_eq 2);
+by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_eq 1);
+by (TRYALL(assume_tac));
+by (ALLGOALS(dtac ActsD));
+by (TRYALL(assume_tac));
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(rotate_tac ~2));
+by Auto_tac;
+qed "client_prog_Increasing_ask_rel";
+
+Addsimps [nth_append, append_one_prefix];
+
+Goal  "0<NbT";
+by (cut_facts_tac [NbT_pos] 1);
+by (resolve_tac [Ord_0_lt] 1);
+by Auto_tac;
+qed "NbT_pos2";
+
+(*Safety property 2: the client never requests too many tokens.
+With no Substitution Axiom, we must prove the two invariants simultaneously. *)
+
+Goal 
+"[| client_prog ok G; G:program |]\
+\     ==> client_prog Join G :  \
+\             Always({s:state. s`tok le NbT}  Int  \
+\                     {s:state. ALL elt:set_of_list(s`ask). elt le NbT})";
+by (rotate_tac ~1 1);
+by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
+by (rtac (invariantI RS stable_Join_Always2) 1);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Asm_full_simp_tac)); 
+by (rtac stable_Int 2);
+by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_stable 3);
+by (dres_inst_tac [("f", "lift(tok)")] preserves_imp_stable 2);
+by (REPEAT(Force_tac 2));
+by (constrains_tac 1);
+by (auto_tac (claset() addDs [ActsD], simpset()));
+by (cut_facts_tac [NbT_pos] 1);
+by (resolve_tac [NbT_pos2 RS mod_less_divisor] 1);
+by (auto_tac (claset() addDs [ActsD, preserves_imp_eq], 
+               simpset() addsimps [set_of_list_append]));
+qed "ask_Bounded_lemma";
+
+(* Export version, with no mention of tok in the postcondition, but
+  unfortunately tok must be declared local.*)
+Goal 
+"client_prog: program guarantees \
+\            Always({s:state. ALL elt: set_of_list(s`ask). elt le NbT})";
+by (rtac guaranteesI 1);
+by (etac (ask_Bounded_lemma RS Always_weaken) 1);
+by Auto_tac;
+qed "client_prog_ask_Bounded";
+
+(*** Towards proving the liveness property ***)
+
+Goal 
+"client_prog: stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (constrains_tac 1);
+by Auto_tac;
+qed "client_prog_stable_rel_le_giv";
+
+Goal
+"[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
+\   ==> client_prog Join G:  Stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1);
+by (auto_tac (claset(), simpset() addsimps [lift_def]));
+qed "client_prog_Join_Stable_rel_le_giv";
+
+Goal "[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
+\   ==> client_prog Join G : Always({s:state. <s`rel, s`giv>:prefix(nat)})";
+by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv], 
+            simpset()) 1);
+qed "client_prog_Join_Always_rel_le_giv";
+
+Goal "xs:list(A) ==> xs@[a]=xs --> False";
+by (etac list.induct 1);
+by Auto_tac;
+qed "list_app_lemma";
+
+Goal "A == {<s, t>:state*state. P(s, t)} ==> A={<s, t>:state*state. P(s, t)}";
+by Auto_tac;
+qed "def_act_eq";
+
+Goal "A={<s,t>:state*state. P(s, t)} ==> A<=state*state";
+by Auto_tac;
+qed "act_subset";
+
+Goal 
+"client_prog: \
+\ transient({s:state. s`rel = k & <k, h>:strict_prefix(nat) \
+\  & <h, s`giv>:prefix(nat) & h pfixGe s`ask})";
+by (res_inst_tac [("act", "client_rel_act")] transientI 1);
+by (simp_tac (simpset() addsimps 
+                 [client_prog_def RS def_prg_Acts]) 1);
+by (simp_tac (simpset() addsimps 
+             [client_rel_act_def RS def_act_eq RS act_subset]) 1);
+by (auto_tac (claset(),
+              simpset() addsimps [client_prog_def RS def_prg_Acts,domain_def]));
+by (resolve_tac [ReplaceI] 1);
+by (res_inst_tac [("x", "x(rel:= x`rel @\
+        \            [nth(length(x`rel), x`giv)])")] exI 1);
+by (auto_tac (claset() addSIs [state_update_type, 
+                               app_type, length_type, nth_type], 
+              simpset()));
+by Auto_tac;
+by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
+                               strict_prefix_length_lt]) 1);
+by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
+                               strict_prefix_length_lt]) 1);
+by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
+by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
+by (auto_tac (claset(), 
+              simpset() addsimps [prefix_def, Ge_def]));
+by (dtac strict_prefix_length_lt 1);
+by (dres_inst_tac [("x", "length(x`rel)")] bspec 1);
+by Auto_tac;
+by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
+by (auto_tac (claset(), simpset() addsimps [id_def, lam_def]));
+qed "transient_lemma";
+
+Goalw [strict_prefix_def,id_def, lam_def]
+"<xs, ys>:strict_prefix(A) <->  <xs, ys>:prefix(A) & xs~=ys";
+by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset()));
+qed "strict_prefix_is_prefix";
+
+Goal 
+"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] \
+\ ==> client_prog Join G: \
+\ {s:state. s`rel = k & <k,h>:strict_prefix(nat) \
+\  & <h , s`giv>:prefix(nat) & h pfixGe s`ask}  \
+\       LeadsTo {s:state. <k, s`rel>:strict_prefix(nat) \
+\                         & <s`rel, s`giv>:prefix(nat) & \
+\                                 <h, s`giv>:prefix(nat) & \
+\               h pfixGe s`ask}";
+by (rtac single_LeadsTo_I 1);
+by (Asm_simp_tac 2);
+by (ftac (client_prog_Increasing_ask_rel RS guaranteesD) 1);
+by (rotate_tac 2 3);
+by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
+by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS 
+          leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
+by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
+by (eres_inst_tac [("f", "lift(giv)"), ("a", "s`giv")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (eres_inst_tac [("f", "lift(ask)"), ("a", "s`ask")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (eres_inst_tac [("f", "lift(rel)"), ("a", "s`rel")] Increasing_imp_Stable 1);
+by (Asm_simp_tac 1);
+by (etac client_prog_Join_Stable_rel_le_giv 1);
+by (Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 2);
+by (blast_tac (claset() addIs [sym, strict_prefix_is_prefix RS iffD2, 
+                               prefix_trans, prefix_imp_pfixGe, 
+                               pfixGe_trans]) 2);
+by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD1 RS conjunct1, 
+                               prefix_trans], simpset()));
+qed "induct_lemma";
+
+Goal 
+"[| client_prog Join G : Incr(lift(giv)); client_prog ok G; G:program |] \
+\ ==> client_prog Join G : \
+\    {s:state. <s`rel, h>:strict_prefix(nat) \
+\          & <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
+\                     LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+by (res_inst_tac [("f", "lam x:state. length(h) #- length(x`rel)")] 
+                                 LessThan_induct 1);
+by (auto_tac (claset(), simpset() addsimps [vimage_def]));
+by (rtac single_LeadsTo_I 1);
+by (rtac (induct_lemma RS LeadsTo_weaken) 1);
+by Auto_tac;
+by (resolve_tac [imageI] 3);
+by (resolve_tac [converseI] 3);
+by (asm_simp_tac (simpset() addsimps [lam_def]) 3);
+by (asm_simp_tac (simpset() addsimps [length_type]) 3);
+by (etac swap 2);
+by (resolve_tac [imageI] 2);
+by (resolve_tac [converseI] 2);
+by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2);
+by (REPEAT (dtac strict_prefix_length_lt 2));
+by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2);
+by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
+by (dtac less_imp_succ_add 2);
+by (dtac less_imp_succ_add 3);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Asm_simp_tac));
+by (etac (diff_le_self RS ltD) 2); 
+by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 1);
+by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
+                        addDs [rotate_prems 2 common_prefix_linear,
+                               prefix_type RS subsetD], simpset()));
+qed "rel_progress_lemma";
+
+Goal 
+"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] ==> \
+\ client_prog Join G : \
+\  {s:state. <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
+\              LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+by (rtac (client_prog_Join_Always_rel_le_giv RS Always_LeadsToI) 1);
+by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
+    LeadsTo_Un RS LeadsTo_weaken_L) 3);
+by Auto_tac;
+by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2]
+                        addDs [rotate_prems 3 common_prefix_linear,
+                               prefix_type RS subsetD], simpset()));
+by (rotate_tac ~1 1);
+by (force_tac (claset(), simpset() addsimps [client_prog_ok_iff]) 1);
+qed "progress_lemma";
+
+(*Progress property: all tokens that are given will be released*)
+Goal 
+"client_prog: Incr(lift(giv))  guarantees  \
+\     (INT h:list(nat). {s:state. <h, s`giv>:prefix(nat) &\
+\             h pfixGe s`ask} LeadsTo {s:state. <h, s`rel>:prefix(nat)})";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [progress_lemma]) 1);
+by Auto_tac;
+qed "client_prog_progress";
+
+Goal "Allowed(client_prog) = \
+\ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))";
+by (cut_facts_tac [inst "v"  "lift(ask)" preserves_type] 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [Allowed_def, 
+               client_prog_def RS def_prg_Allowed, 
+                  cons_Int_distrib, safety_prop_Acts_iff]));
+qed "client_prog_Allowed";
+
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/ClientImpl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ClientImpl.thy	Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,63 @@
+(*  Title:      ZF/UNITY/ClientImpl.thy
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Distributed Resource Management System:  Client Implementation
+*)
+
+
+ClientImpl = AllocBase + Guar +
+consts
+  ask :: i (* input history:  tokens requested *)
+  giv :: i (* output history: tokens granted *)
+  rel :: i (* input history: tokens released *)
+  tok :: i (* the number of available tokens *)
+
+translations
+  "ask" == "Var(Nil)"
+  "giv" == "Var([0])"
+  "rel" == "Var([1])"
+  "tok" == "Var([2])"
+
+rules
+  type_assumes
+  "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
+   type_of(rel) = list(tokbag) & type_of(tok) = nat"
+  default_val_assumes
+  "default_val(ask) = Nil & default_val(giv)  = Nil & 
+   default_val(rel)  = Nil & default_val(tok)  = 0"
+
+
+(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
+
+constdefs
+ (** Release some client_tokens **)
+  
+  client_rel_act ::i
+    "client_rel_act ==
+     {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
+		    &  t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
+                  nrel < length(s`giv) &
+                  nth(nrel, s`ask) le nth(nrel, s`giv)}"
+  
+  (** Choose a new token requirement **)
+  (** Including s'=s suppresses fairness, allowing the non-trivial part
+      of the action to be ignored **)
+
+  client_tok_act :: i
+ "client_tok_act == {<s,t>:state*state. t=s |
+		 (t = s(tok:=succ(s`tok mod NbT)))}"
+
+  client_ask_act :: i
+  "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+  
+  client_prog :: i
+  "client_prog ==
+   mk_program({s:state. s`tok le NbT & s`giv = Nil &
+	               s`ask = Nil & s`rel = Nil},
+                    {client_rel_act, client_tok_act, client_ask_act},
+                   UN G: preserves(lift(rel)) Int
+			 preserves(lift(ask)) Int
+	                 preserves(lift(tok)).  Acts(G))"
+end
\ No newline at end of file
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/Distributor.ML
--- a/src/ZF/UNITY/Distributor.ML	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/Distributor.ML	Thu May 29 17:10:00 2003 +0200
@@ -74,7 +74,7 @@
 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() addsimps []));
+               simpset()));
 qed "distr_Increasing_Out";
 
 val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
@@ -116,13 +116,6 @@
 by (blast_tac (claset() addIs [lt_trans]) 1);
 qed "distr_bag_Follows_lemma";
 
-
-val prems =
-Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
-by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
-qed "Follows_cong";
-(*????????????????*)
-
 Goal
  "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
 \      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
@@ -150,8 +143,8 @@
 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 (simpset() addsimps []) 3);
-by (asm_full_simp_tac (simpset() addsimps []) 3);
+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);
@@ -159,8 +152,8 @@
               simpset() addsimps [distr_spec_def, distr_follows_def]));
 by (dtac guaranteesD 1); 
 by (assume_tac 1);
-by (force_tac (claset(), simpset() addsimps []) 1); 
-by (force_tac (claset(), simpset() addsimps []) 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] 
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/Follows.ML
--- a/src/ZF/UNITY/Follows.ML	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/Follows.ML	Thu May 29 17:10:00 2003 +0200
@@ -8,6 +8,10 @@
  
 (*Does this hold for "invariant"?*)
 
+val prems =
+Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
+by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
+qed "Follows_cong";
 
 Goalw [mono1_def, comp_def] 
 "[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/Merge.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Merge.ML	Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,163 @@
+(*  Title: ZF/UNITY/Merge
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Merge specification
+*)
+Open_locale "Merge";
+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:state ==> s`In(n):list(A)";
+by (dres_inst_tac [("a", "In(n)")] apply_type 1);
+by Auto_tac;
+qed "In_value_type";
+AddTCs [In_value_type];
+Addsimps [In_value_type];
+
+Goalw [state_def]
+"s:state ==> s`Out:list(A)";
+by (dres_inst_tac [("a", "Out")] apply_type 1);
+by Auto_tac;
+qed "Out_value_type";
+AddTCs [Out_value_type];
+Addsimps [Out_value_type];
+
+Goalw [state_def]
+"s:state ==> s`iOut:list(nat)";
+by (dres_inst_tac [("a", "iOut")] apply_type 1);
+by Auto_tac;
+qed "Out_value_type";
+AddTCs [Out_value_type];
+Addsimps [Out_value_type];
+
+
+val merge = thm "merge_spec";
+
+Goal "M:program";
+by (cut_facts_tac [merge] 1);
+by (auto_tac (claset() addDs [guarantees_type RS subsetD], 
+              simpset() addsimps [merge_spec_def, merge_increasing_def]));
+qed "M_in_program";
+Addsimps [M_in_program];
+AddTCs [M_in_program];
+
+Goal 
+"Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))";
+by (cut_facts_tac [merge, inst "v"  "lift(Out)" preserves_type] 1);
+by (auto_tac (claset(), simpset() addsimps 
+         [merge_spec_def, merge_allowed_acts_def, 
+          Allowed_def,  safety_prop_Acts_iff]));
+qed "merge_Allowed";
+
+Goal 
+"G:program ==> \
+\ M ok G <-> (G:preserves(lift(Out)) &  \
+\      G:preserves(lift(iOut)) & M:Allowed(G))";
+by (cut_facts_tac [merge] 1); 
+by (auto_tac (claset(), simpset() 
+         addsimps [merge_Allowed, ok_iff_Allowed]));  
+qed "M_ok_iff";
+
+Goal
+"[| G:preserves(lift(Out)); G:preserves(lift(iOut)); \
+\  M:Allowed(G) |] ==> \
+\ M Join G:Always({s:state. length(s`Out)=length(s`iOut)})";
+by (ftac (preserves_type RS subsetD) 1);
+by (subgoal_tac "G:program" 1);
+by (assume_tac 2);
+by (ftac M_ok_iff 1);
+by (cut_facts_tac [merge] 1);
+by (force_tac (claset() addDs [guaranteesD], 
+               simpset() addsimps [merge_spec_def, merge_eq_Out_def]) 1); 
+qed "merge_Always_Out_eq_iOut";
+
+Goal 
+"[| G:preserves(lift(iOut)); G:preserves(lift(Out)); \
+\   M:Allowed(G) |] ==> \
+\ M Join G: Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})";
+by (ftac (preserves_type RS subsetD) 1);
+by (ftac M_ok_iff 1);
+by (cut_facts_tac [merge] 1);
+by (force_tac (claset() addDs [guaranteesD], 
+               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
+qed "merge_Bounded";
+
+Goal 
+"[| G:preserves(lift(iOut)); \
+\   G: preserves(lift(Out)); M:Allowed(G) |] \
+\ ==> M Join G : Always \
+\   ({s:state. msetsum(%i. bag_of(sublist(s`Out, \
+\     {k:nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
+\                  Nclients, A) = bag_of(s`Out)})";
+by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
+           state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
+;
+by Auto_tac; 
+by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
+by (auto_tac (claset(), simpset() 
+              addsimps [nat_into_Finite, set_of_list_conv_nth])); 
+by (subgoal_tac
+    "(UN i:Nclients. {k:nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
+by Auto_tac;
+by (resolve_tac [equalityI] 1);
+by (blast_tac (claset() addDs [ltD]) 1); 
+by (Clarify_tac 1); 
+by (subgoal_tac "length(x ` iOut) : nat" 1);
+by Typecheck_tac; 
+by (subgoal_tac "xa : nat" 1); 
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
+by (blast_tac (claset() addIs [lt_trans]) 2);
+by (dres_inst_tac [("x", "nth(xa, x`iOut)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
+by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
+by (blast_tac (claset() addDs [ltD]) 1); 
+qed "merge_bag_Follows_lemma";
+
+Goal
+"M : (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
+\       guarantees  \
+\ (%s. bag_of(s`Out)) Fols \
+\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
+by (cut_facts_tac [merge] 1);
+by (rtac (merge_bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
+by (ALLGOALS(rotate_tac ~1 ));
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [M_ok_iff])));
+by Auto_tac;
+by (rtac Follows_state_ofD1 1);
+by (rtac Follows_msetsum_UN 1);
+by (ALLGOALS(Clarify_tac));
+by (resolve_tac [conjI] 2);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 2);
+by (resolve_tac [conjI] 3);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 3);
+by (resolve_tac [conjI] 4);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 4);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 5);
+by (ALLGOALS(Asm_simp_tac));
+by (resolve_tac [nat_into_Finite] 2);
+by (Asm_simp_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff,
+                      merge_spec_def, merge_follows_def]) 1);
+by Auto_tac;
+by (cut_facts_tac [merge] 1);
+by (subgoal_tac "M ok G" 1);
+by (dtac guaranteesD 1); 
+by (assume_tac 1);
+by (force_tac (claset() addIs[M_ok_iff RS iffD2], simpset()) 4);
+by (rewrite_goal_tac [merge_spec_def, merge_follows_def] 1);
+by (Blast_tac 1);
+by (Asm_simp_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 "merge_bag_Follows";
+Close_locale "Merge";
+
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/Merge.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Merge.thy	Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,78 @@
+(*  Title: ZF/UNITY/Merge
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Merge specification
+*)
+
+Merge = AllocBase + Follows +  Guar + GenPrefix +
+(** Merge specification (the number of inputs is Nclients) ***)
+(** Parameter A represents the type of items to Merge **)
+constdefs
+  (*spec (10)*)
+  merge_increasing :: [i, i, i] =>i
+    "merge_increasing(A, Out, iOut) == program guarantees
+         (lift(Out) IncreasingWrt  prefix(A)/list(A)) Int
+         (lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
+
+  (*spec (11)*)
+  merge_eq_Out :: [i, i] =>i
+  "merge_eq_Out(Out, iOut) == program guarantees
+         Always({s:state. length(s`Out) = length(s`iOut)})"
+
+  (*spec (12)*)
+  merge_bounded :: i=>i
+  "merge_bounded(iOut) == program guarantees
+         Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})"
+  
+  (*spec (13)*)
+  (* Parameter A represents the type of tokens *)
+  merge_follows :: [i, i=>i, i, i] =>i
+    "merge_follows(A, In, Out, iOut) ==
+     (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+		   guarantees
+     (INT n:Nclients. 
+        (%s. sublist(s`Out, {k:nat. k < length(s`iOut) &
+                      nth(k, s`iOut) = n})) Fols lift(In(n))
+         Wrt prefix(A)/list(A))"
+
+  (*spec: preserves part*)
+  merge_preserves :: [i=>i] =>i
+    "merge_preserves(In) == INT n:nat. preserves(lift(In(n)))"
+
+(* environmental constraints*)
+  merge_allowed_acts :: [i, i] =>i
+  "merge_allowed_acts(Out, iOut) ==
+         {F:program. AllowedActs(F) =
+            cons(id(state), (UN G:preserves(lift(Out)) Int
+                                  preserves(lift(iOut)). Acts(G)))}"
+  
+  merge_spec :: [i, i =>i, i, i]=>i
+  "merge_spec(A, In, Out, iOut) ==
+   merge_increasing(A, Out, iOut) Int merge_eq_Out(Out, iOut) Int
+   merge_bounded(iOut) Int  merge_follows(A, In, Out, iOut)
+   Int merge_allowed_acts(Out, iOut) Int merge_preserves(In)"
+
+(** State definitions.  OUTPUT variables are locals **)
+locale Merge =
+  fixes In :: i=>i (*merge's INPUT histories: streams to merge*)
+        Out :: i   (*merge's OUTPUT history: merged items*)
+        iOut :: i  (*merge's OUTPUT history: origins of merged items*)
+        A  :: i    (*the type of items being merged *)
+        M :: i
+ assumes
+    var_assumes       "(ALL n. In(n):var) & Out:var & iOut:var"
+    all_distinct_vars "ALL n. all_distinct([In(n), Out, iOut])"
+    type_assumes      "(ALL n. type_of(In(n))=list(A))&
+		       type_of(Out)=list(A) &
+                       type_of(iOut)=list(nat)"
+   default_val_assumes "(ALL n. default_val(In(n))=Nil) &
+                        default_val(Out)=Nil &
+                        default_val(iOut)=Nil"
+
+   merge_spec  "M:merge_spec(A, In, Out, iOut)"
+end
+
+  
\ No newline at end of file
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/ROOT.ML
--- a/src/ZF/UNITY/ROOT.ML	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/ROOT.ML	Thu May 29 17:10:00 2003 +0200
@@ -18,4 +18,5 @@
 time_use_thy "GenPrefix";
 
 time_use_thy "Distributor";
-
+time_use_thy "Merge";
+time_use_thy "ClientImpl";
diff -r e9c9f69e4f63 -r 4daa384f4fd7 src/ZF/UNITY/WFair.ML
--- a/src/ZF/UNITY/WFair.ML	Wed May 28 18:13:41 2003 +0200
+++ b/src/ZF/UNITY/WFair.ML	Thu May 29 17:10:00 2003 +0200
@@ -544,7 +544,7 @@
 by (auto_tac (claset(), simpset() addsimps [measure_def]));
 by (blast_tac (claset() addIs [ltD]) 1); 
 by (rtac vimageI 1); 
-by (blast_tac (claset() addIs []) 2); 
+by (Blast_tac 2); 
 by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1); 
 by (blast_tac (claset() addIs [lt_trans]) 1); 
 qed "Image_inverse_lessThan";