# HG changeset patch
# User paulson
# Date 1057248470 -7200
# Node ID 7b34f58b1b81894b14816f8e2227beb415caa84d
# Parent  61bd46feb919d7b428aa63f0453734fe64c5ff4c
converted UNITY/Comp/{AllocImpl,Client} to Isar scripts

diff -r 61bd46feb919 -r 7b34f58b1b81 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 03 18:07:50 2003 +0200
@@ -389,8 +389,7 @@
   UNITY/Simple/Network.thy\
   UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
   UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \
-  UNITY/Comp/AllocBase.thy \
-  UNITY/Comp/Client.ML UNITY/Comp/Client.thy \
+  UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
   UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \
   UNITY/Comp/PriorityAux.thy \
   UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
diff -r 61bd46feb919 -r 7b34f58b1b81 src/HOL/UNITY/Comp/AllocImpl.ML
--- a/src/HOL/UNITY/Comp/AllocImpl.ML	Thu Jul 03 12:56:48 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(*  Title:      HOL/UNITY/AllocImpl
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2000  University of Cambridge
-
-Implementation of a multiple-client allocator from a single-client allocator
-*)
-
-AddIs [impOfSubs subset_preserves_o];
-Addsimps [funPair_o_distrib];
-Addsimps [Always_INT_distrib];
-Delsimps [o_apply];
-
-Open_locale "Merge";
-
-val Merge = thm "Merge_spec";
-
-Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
-by (cut_facts_tac [Merge] 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [merge_spec_def, merge_allowed_acts_def, 
-                                  Allowed_def, safety_prop_Acts_iff]));  
-qed "Merge_Allowed";
-
-Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
-\                    M : Allowed G)";
-by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));  
-qed "M_ok_iff";
-AddIffs [M_ok_iff];
-
-Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
-\     ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
-by (cut_facts_tac [Merge] 1);
-by (force_tac (claset() addDs [guaranteesD], 
-               simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); 
-qed "Merge_Always_Out_eq_iOut";
-
-Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
-\     ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
-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 merge.iOut; G: preserves merge.Out; M : Allowed G |] \
-\ ==> M Join G : Always \
-\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s) \
-\                                 {k. k < length (iOut s) & iOut s ! k = i})) = \
-\             (bag_of o merge.Out) s}";
-by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
-	   UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
-     by Auto_tac; 
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
-  by (Simp_tac 1);
- by (Blast_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); 
-by (subgoal_tac
-    "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
-\    lessThan (length (iOut x))" 1);
- by (Blast_tac 2); 
-by (asm_simp_tac (simpset() addsimps [o_def]) 1); 
-qed "Merge_Bag_Follows_lemma";
-
-Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
-\         guarantees  \
-\            (bag_of o merge.Out) Fols \
-\            (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)";
-by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
-by Auto_tac;  
-by (rtac Follows_setsum 1);
-by (cut_facts_tac [Merge] 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
-by (dtac guaranteesD 1); 
-by (best_tac
-    (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
-by Auto_tac;  
-qed "Merge_Bag_Follows";
-
-Close_locale "Merge";
-
-
-(** Distributor **)
-
-Open_locale "Distrib";
-
-val Distrib = thm "Distrib_spec";
-  
-
-Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
-\         Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\         guarantees \
-\         (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
-by (cut_facts_tac [Distrib] 1);
-by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
-by (Clarify_tac 1); 
-by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
-                        addDs [guaranteesD]) 1);
-qed "Distr_Increasing_Out";
-
-Goal "[| G : preserves distr.Out; \
-\        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
-\ ==> D Join G : Always \
-\         {s. (\\<Sum>i: lessThan Nclients. bag_of (sublist (distr.In s) \
-\                                 {k. k < length (iIn s) & iIn s ! k = i})) = \
-\             bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
-by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
-by Auto_tac; 
-by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
-  by (Simp_tac 1);
- by (Blast_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); 
-by (subgoal_tac
-    "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
-\    lessThan (length (iIn x))" 1);
- by (Blast_tac 2); 
-by (Asm_simp_tac 1); 
-qed "Distr_Bag_Follows_lemma";
-
-Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
-by (cut_facts_tac [Distrib] 1);
-by (auto_tac (claset(), 
-     simpset() addsimps [distr_spec_def, distr_allowed_acts_def, 
-                         Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
-qed "D_ok_iff";
-AddIffs [D_ok_iff];
-
-Goal
- "D : Increasing distr.In Int Increasing distr.iIn Int \
-\     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\     guarantees  \
-\      (INT i : lessThan Nclients. \
-\       (%s. \\<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s) \
-\       Fols \
-\       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1); 
-by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;  
-by (rtac Follows_setsum 1);
-by (cut_facts_tac [Distrib] 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
-by (dtac guaranteesD 1); 
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
-by Auto_tac;  
-qed "Distr_Bag_Follows";
-
-Close_locale "Distrib";
-
-
-Goal "!!f::nat=>nat. (INT i: lessThan n. {s. f i <= g i s})  \
-\     <= {s. (\\<Sum>x: lessThan n. f x) <= (\\<Sum>x: lessThan n. g x s)}";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
-qed "alloc_refinement_lemma";
-
-Goal
-"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int  \
-\                            Increasing (sub i o allocRel))     \
-\ Int   \
-\ Always {s. ALL i. i<Nclients -->      \
-\             (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}       \
-\ Int   \
-\ (INT i : lessThan Nclients.   \
-\  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}  \
-\          LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})        \
-\ <=     \
-\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int  \
-\                            Increasing (sub i o allocRel))     \
-\ Int   \
-\ Always {s. ALL i. i<Nclients -->      \
-\             (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}       \
-\ Int   \
-\ (INT hf. (INT i : lessThan Nclients.  \
-\        {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
-\ LeadsTo {s. (\\<Sum>i: lessThan Nclients. tokens (hf i)) <=         \
-\   (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})";
-by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));  
-by (rename_tac "F hf" 1);
-by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
-          MRS LeadsTo_weaken_R) 1);
-  by (Blast_tac 1); 
- by (Blast_tac 1); 
-by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1);
- by (blast_tac
-     (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1);
-qed "alloc_refinement";
-
-
diff -r 61bd46feb919 -r 7b34f58b1b81 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 03 18:07:50 2003 +0200
@@ -2,42 +2,42 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
-
-Implementation of a multiple-client allocator from a single-client allocator
 *)
 
-AllocImpl = AllocBase + Follows + PPROD + 
+header{*Implementation of a multiple-client allocator from a single-client allocator*}
+
+theory AllocImpl = AllocBase + Follows + PPROD:
 
 
 (** State definitions.  OUTPUT variables are locals **)
 
 (*Type variable 'b is the type of items being merged*)
 record 'b merge =
-  In   :: nat => 'b list   (*merge's INPUT histories: streams to merge*)
-  Out  :: 'b list          (*merge's OUTPUT history: merged items*)
-  iOut :: nat list         (*merge's OUTPUT history: origins of merged items*)
+  In   :: "nat => 'b list"   (*merge's INPUT histories: streams to merge*)
+  Out  :: "'b list"          (*merge's OUTPUT history: merged items*)
+  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)
 
 record ('a,'b) merge_d =
-  'b merge +
+  "'b merge" +
   dummy :: 'a       (*dummy field for new variables*)
 
 constdefs
-  non_dummy :: ('a,'b) merge_d => 'b merge
+  non_dummy :: "('a,'b) merge_d => 'b merge"
     "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
 
 record 'b distr =
-  In  :: 'b list          (*items to distribute*)
-  iIn :: nat list         (*destinations of items to distribute*)
-  Out :: nat => 'b list   (*distributed items*)
+  In  :: "'b list"          (*items to distribute*)
+  iIn :: "nat list"         (*destinations of items to distribute*)
+  Out :: "nat => 'b list"   (*distributed items*)
 
 record ('a,'b) distr_d =
-  'b distr +
+  "'b distr" +
   dummy :: 'a       (*dummy field for new variables*)
 
 record allocState =
-  giv :: nat list   (*OUTPUT history: source of tokens*)
-  ask :: nat list   (*INPUT: tokens requested from allocator*)
-  rel :: nat list   (*INPUT: tokens released to allocator*)
+  giv :: "nat list"   (*OUTPUT history: source of tokens*)
+  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
+  rel :: "nat list"   (*INPUT: tokens released to allocator*)
 
 record 'a allocState_d =
   allocState +
@@ -45,9 +45,9 @@
 
 record 'a systemState =
   allocState +
-  mergeRel :: nat merge
-  mergeAsk :: nat merge
-  distr    :: nat distr
+  mergeRel :: "nat merge"
+  mergeAsk :: "nat merge"
+  distr    :: "nat distr"
   dummy    :: 'a                  (*dummy field for new variables*)
 
 
@@ -56,154 +56,152 @@
 (** Merge specification (the number of inputs is Nclients) ***)
 
   (*spec (10)*)
-  merge_increasing :: ('a,'b) merge_d program set
+  merge_increasing :: "('a,'b) merge_d program set"
     "merge_increasing ==
          UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
 
   (*spec (11)*)
-  merge_eqOut :: ('a,'b) merge_d program set
+  merge_eqOut :: "('a,'b) merge_d program set"
     "merge_eqOut ==
          UNIV guarantees
          Always {s. length (merge.Out s) = length (merge.iOut s)}"
 
   (*spec (12)*)
-  merge_bounded :: ('a,'b) merge_d program set
+  merge_bounded :: "('a,'b) merge_d program set"
     "merge_bounded ==
          UNIV guarantees
-         Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
+         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
 
   (*spec (13)*)
-  merge_follows :: ('a,'b) merge_d program set
+  merge_follows :: "('a,'b) merge_d program set"
     "merge_follows ==
-	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
+	 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
 	 guarantees
-	 (INT i : lessThan Nclients. 
+	 (\<Inter>i \<in> lessThan Nclients. 
 	  (%s. sublist (merge.Out s) 
                        {k. k < size(merge.iOut s) & merge.iOut s! k = i})
 	  Fols (sub i o merge.In))"
 
   (*spec: preserves part*)
-  merge_preserves :: ('a,'b) merge_d program set
+  merge_preserves :: "('a,'b) merge_d program set"
     "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
 
   (*environmental constraints*)
-  merge_allowed_acts :: ('a,'b) merge_d program set
+  merge_allowed_acts :: "('a,'b) merge_d program set"
     "merge_allowed_acts ==
        {F. AllowedActs F =
 	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
 
-  merge_spec :: ('a,'b) merge_d program set
+  merge_spec :: "('a,'b) merge_d program set"
     "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                    merge_follows Int merge_allowed_acts Int merge_preserves"
 
 (** Distributor specification (the number of outputs is Nclients) ***)
 
   (*spec (14)*)
-  distr_follows :: ('a,'b) distr_d program set
+  distr_follows :: "('a,'b) distr_d program set"
     "distr_follows ==
 	 Increasing distr.In Int Increasing distr.iIn Int
-	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
+	 Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
 	 guarantees
-	 (INT i : lessThan Nclients. 
+	 (\<Inter>i \<in> lessThan Nclients. 
 	  (sub i o distr.Out) Fols
 	  (%s. sublist (distr.In s) 
                        {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
 
-  distr_allowed_acts :: ('a,'b) distr_d program set
+  distr_allowed_acts :: "('a,'b) distr_d program set"
     "distr_allowed_acts ==
        {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
 
-  distr_spec :: ('a,'b) distr_d program set
+  distr_spec :: "('a,'b) distr_d program set"
     "distr_spec == distr_follows Int distr_allowed_acts"
 
 (** Single-client allocator specification (required) ***)
 
   (*spec (18)*)
-  alloc_increasing :: 'a allocState_d program set
+  alloc_increasing :: "'a allocState_d program set"
     "alloc_increasing == UNIV  guarantees  Increasing giv"
 
   (*spec (19)*)
-  alloc_safety :: 'a allocState_d program set
+  alloc_safety :: "'a allocState_d program set"
     "alloc_safety ==
 	 Increasing rel
          guarantees  Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
 
   (*spec (20)*)
-  alloc_progress :: 'a allocState_d program set
+  alloc_progress :: "'a allocState_d program set"
     "alloc_progress ==
 	 Increasing ask Int Increasing rel Int
-         Always {s. ALL elt : set (ask s). elt <= NbT}
+         Always {s. \<forall>elt \<in> set (ask s). elt <= NbT}
          Int
-         (INT h. {s. h <= giv s & h pfixGe (ask s)}
+         (\<Inter>h. {s. h <= giv s & h pfixGe (ask s)}
 		 LeadsTo
 	         {s. tokens h <= tokens (rel s)})
-         guarantees  (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+         guarantees  (\<Inter>h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
 
   (*spec: preserves part*)
-  alloc_preserves :: 'a allocState_d program set
+  alloc_preserves :: "'a allocState_d program set"
     "alloc_preserves == preserves rel Int
                         preserves ask Int
                         preserves allocState_d.dummy"
   
 
   (*environmental constraints*)
-  alloc_allowed_acts :: 'a allocState_d program set
+  alloc_allowed_acts :: "'a allocState_d program set"
     "alloc_allowed_acts ==
        {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
 
-  alloc_spec :: 'a allocState_d program set
+  alloc_spec :: "'a allocState_d program set"
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
 locale Merge =
-  fixes 
-    M   :: ('a,'b::order) merge_d program
+  fixes M :: "('a,'b::order) merge_d program"
   assumes
-    Merge_spec  "M  : merge_spec"
+    Merge_spec:  "M  \<in> merge_spec"
 
 locale Distrib =
-  fixes 
-    D   :: ('a,'b::order) distr_d program
+  fixes D :: "('a,'b::order) distr_d program"
   assumes
-    Distrib_spec  "D : distr_spec"
+    Distrib_spec:  "D \<in> distr_spec"
 
 
 (****
-#  (** Network specification ***)
+#  {** Network specification ***}
 
-#    (*spec (9.1)*)
-#    network_ask :: 'a systemState program set
-#	"network_ask == INT i : lessThan Nclients.
+#    {*spec (9.1)*}
+#    network_ask :: "'a systemState program set
+#	"network_ask == \<Inter>i \<in> lessThan Nclients.
 #			    Increasing (ask o sub i o client)
 #			    guarantees[ask]
 #			    (ask  Fols (ask o sub i o client))"
 
-#    (*spec (9.2)*)
-#    network_giv :: 'a systemState program set
-#	"network_giv == INT i : lessThan Nclients.
+#    {*spec (9.2)*}
+#    network_giv :: "'a systemState program set
+#	"network_giv == \<Inter>i \<in> lessThan Nclients.
 #			    Increasing giv 
 #			    guarantees[giv o sub i o client]
-#			    ((giv o sub i o client) Fols giv )"
+#			    ((giv o sub i o client) Fols giv)"
 
-#    (*spec (9.3)*)
-#    network_rel :: 'a systemState program set
-#	"network_rel == INT i : lessThan Nclients.
+#    {*spec (9.3)*}
+#    network_rel :: "'a systemState program set
+#	"network_rel == \<Inter>i \<in> lessThan Nclients.
 #			    Increasing (rel o sub i o client)
 #			    guarantees[rel]
 #			    (rel  Fols (rel o sub i o client))"
 
-#    (*spec: preserves part*)
-#	network_preserves :: 'a systemState program set
+#    {*spec: preserves part*}
+#	network_preserves :: "'a systemState program set
 #	"network_preserves == preserves giv  Int
-#			      (INT i : lessThan Nclients.
+#			      (\<Inter>i \<in> lessThan Nclients.
 #			       preserves (funPair rel ask o sub i o client))"
 
-#    network_spec :: 'a systemState program set
+#    network_spec :: "'a systemState program set
 #	"network_spec == network_ask Int network_giv Int
 #			 network_rel Int network_preserves"
 
 
-#  (** State mappings **)
+#  {** State mappings **}
 #    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
 #	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
 #			   in (| giv = giv s,
@@ -221,4 +219,171 @@
 #				     systemState.dummy = allocState_d.dummy al|)"
 ****)
 
+
+declare subset_preserves_o [THEN subsetD, intro]
+declare funPair_o_distrib [simp]
+declare Always_INT_distrib [simp]
+declare o_apply [simp del]
+
+
+subsection{*Theorems for Merge*}
+
+lemma (in Merge) Merge_Allowed:
+     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
+apply (cut_tac Merge_spec)
+apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
+done
+
+lemma (in Merge) M_ok_iff [iff]:
+     "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &  
+                     M \<in> Allowed G)"
+by (auto simp add: Merge_Allowed ok_iff_Allowed)
+
+
+lemma (in Merge) Merge_Always_Out_eq_iOut:
+     "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]  
+      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
+apply (cut_tac Merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
+done
+
+lemma (in Merge) Merge_Bounded:
+     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]  
+      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
+apply (cut_tac Merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
+done
+
+lemma (in Merge) Merge_Bag_Follows_lemma:
+     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]  
+  ==> M Join G \<in> Always  
+          {s. (\<Sum>i: lessThan Nclients. bag_of (sublist (merge.Out s)  
+                                  {k. k < length (iOut s) & iOut s ! k = i})) =  
+              (bag_of o merge.Out) s}"
+apply (rule Always_Compl_Un_eq [THEN iffD1]) 
+apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded]) 
+apply (rule UNIV_AlwaysI, clarify) 
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+  apply (simp)
+ apply blast
+apply (simp add: set_conv_nth)
+apply (subgoal_tac
+       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
+       lessThan (length (iOut x))")
+ apply (simp (no_asm_simp) add: o_def)
+apply blast
+done
+
+lemma (in Merge) Merge_Bag_Follows:
+     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))  
+          guarantees   
+             (bag_of o merge.Out) Fols  
+             (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o merge.In) s)"
+apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
+apply (rule Follows_setsum)
+apply (cut_tac Merge_spec)
+apply (auto simp add: merge_spec_def merge_follows_def o_def)
+apply (drule guaranteesD) 
+  prefer 3
+  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
+done
+
+
+subsection{*Theorems for Distributor*}
+
+lemma (in Distrib) Distr_Increasing_Out:
+     "D \<in> Increasing distr.In Int Increasing distr.iIn Int  
+          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}  
+          guarantees  
+          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
+apply (cut_tac Distrib_spec)
+apply (simp add: distr_spec_def distr_follows_def)
+apply clarify
+apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
+done
+
+lemma (in Distrib) Distr_Bag_Follows_lemma:
+     "[| G \<in> preserves distr.Out;  
+         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]  
+  ==> D Join G \<in> Always  
+          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)  
+                                  {k. k < length (iIn s) & iIn s ! k = i})) =  
+              bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
+apply (erule Always_Compl_Un_eq [THEN iffD1])
+apply (rule UNIV_AlwaysI, clarify)
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+  apply (simp (no_asm))
+ apply blast
+apply (simp add: set_conv_nth)
+apply (subgoal_tac
+       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = 
+        lessThan (length (iIn x))")
+ apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma (in Distrib) D_ok_iff [iff]:
+     "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
+apply (cut_tac Distrib_spec)
+apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def 
+                      safety_prop_Acts_iff ok_iff_Allowed)
+done
+
+lemma (in Distrib) Distr_Bag_Follows: 
+ "D \<in> Increasing distr.In Int Increasing distr.iIn Int  
+      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}  
+      guarantees   
+       (\<Inter>i \<in> lessThan Nclients.  
+        (%s. \<Sum>i: lessThan Nclients. (bag_of o sub i o distr.Out) s)  
+        Fols  
+        (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
+apply (rule guaranteesI, clarify)
+apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
+apply (rule Follows_setsum)
+apply (cut_tac Distrib_spec)
+apply (auto simp add: distr_spec_def distr_follows_def o_def)
+apply (drule guaranteesD)
+  prefer 3
+  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
+done
+
+
+subsection{*Theorems for Allocator*}
+
+lemma alloc_refinement_lemma:
+     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i <= g i s})   
+      <= {s. (\<Sum>x \<in> lessThan n. f x) <= (\<Sum>x: lessThan n. g x s)}"
+apply (induct_tac "n")
+apply (auto simp add: lessThan_Suc)
+done
+
+lemma alloc_refinement: 
+"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int   
+                             Increasing (sub i o allocRel))      
+  Int    
+  Always {s. \<forall>i. i<Nclients -->       
+              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}        
+  Int    
+  (\<Inter>i \<in> lessThan Nclients.    
+   \<Inter>h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}   
+           LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})         
+  <=      
+ (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int   
+                             Increasing (sub i o allocRel))      
+  Int    
+  Always {s. \<forall>i. i<Nclients -->       
+              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt <= NbT)}        
+  Int    
+  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.   
+         {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})  
+  LeadsTo {s. (\<Sum>i: lessThan Nclients. tokens (hf i)) <=          
+    (\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)})"
+apply (auto simp add: ball_conj_distrib)
+apply (rename_tac F hf)
+apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
+apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
+ apply (simp add: Increasing_def o_assoc)
+apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
+done
+
 end
diff -r 61bd46feb919 -r 7b34f58b1b81 src/HOL/UNITY/Comp/Client.ML
--- a/src/HOL/UNITY/Comp/Client.ML	Thu Jul 03 12:56:48 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-(*  Title:      HOL/UNITY/Client
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Distributed Resource Management System: the Client
-*)
-
-Addsimps [Client_def RS def_prg_Init, 
-          Client_def RS def_prg_AllowedActs];
-Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
-
-Goal "(Client ok G) = \
-\     (G : preserves rel & G : preserves ask & G : preserves tok &\
-\      Client : Allowed G)";
-by (auto_tac (claset(), 
-    simpset() addsimps [ok_iff_Allowed, Client_def RS def_total_prg_Allowed]));
-qed "Client_ok_iff";
-AddIffs [Client_ok_iff];
-
-
-(*Safety property 1: ask, rel are increasing*)
-Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
-by (auto_tac
-    (claset() addSIs [increasing_imp_Increasing],
-     simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
-by (auto_tac (claset(), simpset() addsimps [Client_def, increasing_def]));
-by (ALLGOALS constrains_tac);
-by Auto_tac;
-qed "increasing_ask_rel";
-
-Addsimps [nth_append, append_one_prefix];
-
-
-(*Safety property 2: the client never requests too many tokens.
-      With no Substitution Axiom, we must prove the two invariants 
-  simultaneously.
-*)
-Goal "Client ok G  \
-\     ==> Client Join G :  \
-\             Always ({s. tok s <= NbT}  Int  \
-\                     {s. ALL elt : set (ask s). elt <= NbT})";
-by Auto_tac;  
-by (rtac (invariantI RS stable_Join_Always2) 1);
-by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
-		       addSIs [stable_Int]) 3);
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 2);
-by (constrains_tac 2);
-by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
-by Auto_tac;
-qed "ask_bounded_lemma";
-
-(*export version, with no mention of tok in the postcondition, but
-  unfortunately tok must be declared local.*)
-Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
-by (rtac guaranteesI 1);
-by (etac (ask_bounded_lemma RS Always_weaken) 1);
-by (rtac Int_lower2 1);
-qed "ask_bounded";
-
-
-(*** Towards proving the liveness property ***)
-
-Goal "Client: stable {s. rel s <= giv s}";
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1); 
-by (constrains_tac 1);
-by Auto_tac;
-qed "stable_rel_le_giv";
-
-Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
-\     ==> Client Join G : Stable {s. rel s <= giv s}";
-by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
-by Auto_tac;
-qed "Join_Stable_rel_le_giv";
-
-Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
-\     ==> Client Join G : Always {s. rel s <= giv s}";
-by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
-qed "Join_Always_rel_le_giv";
-
-Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
-by (simp_tac (simpset() addsimps [Client_def, mk_total_program_def]) 1);
-by (res_inst_tac [("act", "rel_act")] totalize_transientI 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [Domain_def, Client_def]));
-by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
-			       strict_prefix_length_less]) 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
-by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
-qed "transient_lemma";
-
-
-Goal "[| Client Join G : Increasing giv;  Client ok G |] \
-\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
-\                     LeadsTo {s. k < rel s & rel s <= giv s & \
-\                                 h <= giv s & h pfixGe ask s}";
-by (rtac single_LeadsTo_I 1);
-by (ftac (increasing_ask_rel RS guaranteesD) 1);
-by Auto_tac;
-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", "giv"), ("x", "giv s")] IncreasingD 1);
-by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
-by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
-by (etac Join_Stable_rel_le_giv 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [sym, order_less_le RS iffD2, 
-			       order_trans, prefix_imp_pfixGe, 
-			       pfixGe_trans]) 2);
-by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
-qed "induct_lemma";
-
-
-Goal "[| Client Join G : Increasing giv;  Client ok G |] \
-\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
-\                     LeadsTo {s. h <= rel s}";
-by (res_inst_tac [("f", "%s. size h - size (rel s)")] 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 (blast_tac (claset() addIs [order_less_le RS iffD2]
-			addDs [common_prefix_linear]) 1);
-by (REPEAT (dtac strict_prefix_length_less 1));
-by (arith_tac 1);
-qed "rel_progress_lemma";
-
-
-Goal "[| Client Join G : Increasing giv;  Client ok G |] \
-\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
-\                     LeadsTo {s. h <= rel s}";
-by (rtac (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 (blast_tac (claset() addIs [order_less_le RS iffD2]
-			addDs [common_prefix_linear]) 1);
-qed "client_progress_lemma";
-
-(*Progress property: all tokens that are given will be released*)
-Goal "Client : \
-\      Increasing giv  guarantees  \
-\      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
-by (rtac guaranteesI 1);
-by (Clarify_tac 1);
-by (blast_tac (claset() addIs [client_progress_lemma]) 1);
-qed "client_progress";
-
-(*This shows that the Client won't alter other variables in any state
-  that it is combined with*)
-Goal "Client : preserves dummy";
-by (asm_full_simp_tac (simpset() addsimps [Client_def, preserves_def]) 1);
-by (Clarify_tac 1); 
-by (constrains_tac 1);
-by Auto_tac;
-qed "client_preserves_dummy";
-
-
-(** Obsolete lemmas from first version of the Client **)
-
-Goal "Client: stable {s. size (rel s) <= size (giv s)}";
-by (asm_full_simp_tac (simpset() addsimps [Client_def]) 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "stable_size_rel_le_giv";
-
-(*clients return the right number of tokens*)
-Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
-by (rtac guaranteesI 1);
-by (rtac AlwaysI 1);
-by (Force_tac 1);
-by (blast_tac (claset() addIs [Increasing_preserves_Stable, 
-			       stable_rel_le_giv]) 1);
-qed "ok_guar_rel_prefix_giv";
diff -r 61bd46feb919 -r 7b34f58b1b81 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Thu Jul 03 12:56:48 2003 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Thu Jul 03 18:07:50 2003 +0200
@@ -2,24 +2,24 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
-
-Distributed Resource Management System: the Client
 *)
 
-Client = Rename + AllocBase +
+header{*Distributed Resource Management System: the Client*}
+
+theory Client = Rename + AllocBase:
 
 types
-  tokbag = nat	   (*tokbags could be multisets...or any ordered type?*)
+  tokbag = nat	   --{*tokbags could be multisets...or any ordered type?*}
 
 record state =
-  giv :: tokbag list   (*input history: tokens granted*)
-  ask :: tokbag list   (*output history: tokens requested*)
-  rel :: tokbag list   (*output history: tokens released*)
-  tok :: tokbag	       (*current token request*)
+  giv :: "tokbag list" --{*input history: tokens granted*}
+  ask :: "tokbag list" --{*output history: tokens requested*}
+  rel :: "tokbag list" --{*output history: tokens released*}
+  tok :: tokbag	       --{*current token request*}
 
 record 'a state_d =
   state +  
-  dummy :: 'a          (*new variables*)
+  dummy :: 'a          --{*new variables*}
 
 
 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -30,10 +30,10 @@
   
   rel_act :: "('a state_d * 'a state_d) set"
     "rel_act == {(s,s').
-		  \\<exists>nrel. nrel = size (rel s) &
+		  \<exists>nrel. nrel = size (rel s) &
 		         s' = s (| rel := rel s @ [giv s!nrel] |) &
 		         nrel < size (giv s) &
-		         ask s!nrel <= giv s!nrel}"
+		         ask s!nrel \<le> giv s!nrel}"
 
   (** Choose a new token requirement **)
 
@@ -47,21 +47,172 @@
     "ask_act == {(s,s'). s'=s |
 		         (s' = s (|ask := ask s @ [tok s]|))}"
 
-  Client :: 'a state_d program
+  Client :: "'a state_d program"
     "Client ==
        mk_total_program
-            ({s. tok s : atMost NbT &
+            ({s. tok s \<in> atMost NbT &
 		 giv s = [] & ask s = [] & rel s = []},
 	     {rel_act, tok_act, ask_act},
-	     \\<Union>G \\<in> preserves rel Int preserves ask Int preserves tok.
+	     \<Union>G \<in> preserves rel Int preserves ask Int preserves tok.
 		   Acts G)"
 
   (*Maybe want a special theory section to declare such maps*)
-  non_dummy :: 'a state_d => state
+  non_dummy :: "'a state_d => state"
     "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
 
   (*Renaming map to put a Client into the standard form*)
   client_map :: "'a state_d => state*'a"
     "client_map == funPair non_dummy dummy"
 
+
+declare Client_def [THEN def_prg_Init, simp]
+declare Client_def [THEN def_prg_AllowedActs, simp]
+declare rel_act_def [THEN def_act_simp, simp]
+declare tok_act_def [THEN def_act_simp, simp]
+declare ask_act_def [THEN def_act_simp, simp]
+
+lemma Client_ok_iff [iff]:
+     "(Client ok G) =  
+      (G \<in> preserves rel & G \<in> preserves ask & G \<in> preserves tok & 
+       Client \<in> Allowed G)"
+by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
+
+
+text{*Safety property 1: ask, rel are increasing*}
+lemma increasing_ask_rel:
+     "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
+apply (auto simp add: Client_def increasing_def)
+apply (constrains, auto)+
+done
+
+declare nth_append [simp] append_one_prefix [simp]
+
+
+text{*Safety property 2: the client never requests too many tokens.
+      With no Substitution Axiom, we must prove the two invariants 
+      simultaneously. *}
+lemma ask_bounded_lemma:
+     "Client ok G   
+      ==> Client Join G \<in>   
+              Always ({s. tok s \<le> NbT}  Int   
+                      {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
+apply auto
+apply (rule invariantI [THEN stable_Join_Always2], force) 
+ prefer 2
+ apply (fast elim!: preserves_subset_stable [THEN subsetD] intro!: stable_Int) 
+apply (simp add: Client_def, constrains)
+apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
+done
+
+text{*export version, with no mention of tok in the postcondition, but
+  unfortunately tok must be declared local.*}
+lemma ask_bounded:
+     "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
+apply (rule guaranteesI)
+apply (erule ask_bounded_lemma [THEN Always_weaken])
+apply (rule Int_lower2)
+done
+
+
+text{*** Towards proving the liveness property ***}
+
+lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
+by (simp add: Client_def, constrains, auto)
+
+lemma Join_Stable_rel_le_giv:
+     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
+by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
+
+lemma Join_Always_rel_le_giv:
+     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
+by (force intro: AlwaysI Join_Stable_rel_le_giv)
+
+lemma transient_lemma:
+     "Client \<in> transient {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}"
+apply (simp add: Client_def mk_total_program_def)
+apply (rule_tac act = rel_act in totalize_transientI)
+  apply (auto simp add: Domain_def Client_def)
+ apply (blast intro: less_le_trans prefix_length_le strict_prefix_length_less)
+apply (auto simp add: prefix_def genPrefix_iff_nth Ge_def)
+apply (blast intro: strict_prefix_length_less)
+done
+
+
+lemma induct_lemma:
+     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
+  ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
+                      LeadsTo {s. k < rel s & rel s \<le> giv s &  
+                                  h \<le> giv s & h pfixGe ask s}"
+apply (rule single_LeadsTo_I)
+apply (frule increasing_ask_rel [THEN guaranteesD], auto)
+apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
+  apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
+     apply (erule_tac f = giv and x = "giv s" in IncreasingD)
+    apply (erule_tac f = ask and x = "ask s" in IncreasingD)
+   apply (erule_tac f = rel and x = "rel s" in IncreasingD)
+  apply (erule Join_Stable_rel_le_giv, blast)
+ apply (blast intro: order_less_imp_le order_trans)
+apply (blast intro: sym order_less_le [THEN iffD2] order_trans
+                    prefix_imp_pfixGe pfixGe_trans)
+done
+
+
+lemma rel_progress_lemma:
+     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
+  ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
+                      LeadsTo {s. h \<le> rel s}"
+apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
+apply (auto simp add: vimage_def)
+apply (rule single_LeadsTo_I)
+apply (rule induct_lemma [THEN LeadsTo_weaken], auto)
+ apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
+apply (drule strict_prefix_length_less)+
+apply arith
+done
+
+
+lemma client_progress_lemma:
+     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
+      ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
+                          LeadsTo {s. h \<le> rel s}"
+apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
+apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
+  apply (blast intro: rel_progress_lemma) 
+ apply (rule subset_refl [THEN subset_imp_LeadsTo])
+apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
+done
+
+text{*Progress property: all tokens that are given will be released*}
+lemma client_progress:
+     "Client \<in>  
+       Increasing giv  guarantees   
+       (INT h. {s. h \<le> giv s & h pfixGe ask s} LeadsTo {s. h \<le> rel s})"
+apply (rule guaranteesI, clarify)
+apply (blast intro: client_progress_lemma)
+done
+
+text{*This shows that the Client won't alter other variables in any state
+  that it is combined with*}
+lemma client_preserves_dummy: "Client \<in> preserves dummy"
+by (simp add: Client_def preserves_def, clarify, constrains, auto)
+
+
+text{** Obsolete lemmas from first version of the Client **}
+
+lemma stable_size_rel_le_giv:
+     "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
+by (simp add: Client_def, constrains, auto)
+
+text{*clients return the right number of tokens*}
+lemma ok_guar_rel_prefix_giv:
+     "Client \<in> Increasing giv  guarantees  Always {s. rel s \<le> giv s}"
+apply (rule guaranteesI)
+apply (rule AlwaysI, force)
+apply (blast intro: Increasing_preserves_Stable stable_rel_le_giv)
+done
+
+
 end