# HG changeset patch
# User paulson
# Date 1058350181 -7200
# Node ID e97ca1034caa65e0577abfff7fd706ac9d712185
# Parent  7b3513ba0f8644994059140fcc263101dce70f1e
tidying

diff -r 7b3513ba0f86 -r e97ca1034caa src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Jul 15 15:20:54 2003 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 16 12:09:41 2003 +0200
@@ -71,14 +71,13 @@
 declare setsum_cong [cong]
 
 lemma bag_of_sublist_lemma:
-     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
-      (\<Sum>i: A Int lessThan k. {#f i#})"
-apply (rule setsum_cong, auto)
-done
+     "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
+      (\\<Sum>i: A Int lessThan k. {#f i#})"
+by (rule setsum_cong, auto)
 
 lemma bag_of_sublist:
      "bag_of (sublist l A) =  
-      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
+      (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
 apply (rule_tac xs = l in rev_induct, simp)
 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
                  bag_of_sublist_lemma plus_ac0)
@@ -88,7 +87,8 @@
 lemma bag_of_sublist_Un_Int:
      "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =  
       bag_of (sublist l A) + bag_of (sublist l B)"
-apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (subgoal_tac "A Int B Int {..length l (} =
+	            (A Int {..length l (}) Int (B Int {..length l (}) ")
 apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
 done
 
@@ -96,13 +96,12 @@
      "A Int B = {}  
       ==> bag_of (sublist l (A Un B)) =  
           bag_of (sublist l A) + bag_of (sublist l B)"
-apply (simp add: bag_of_sublist_Un_Int [symmetric])
-done
+by (simp add: bag_of_sublist_Un_Int [symmetric])
 
 lemma bag_of_sublist_UN_disjoint [rule_format]:
      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
       ==> bag_of (sublist l (UNION I A)) =   
-          (\<Sum>i:I. bag_of (sublist l (A i)))"
+          (\\<Sum>i:I. bag_of (sublist l (A i)))"
 apply (simp del: UN_simps 
             add: UN_simps [symmetric] add: bag_of_sublist)
 apply (subst setsum_UN_disjoint, auto)
diff -r 7b3513ba0f86 -r e97ca1034caa src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Tue Jul 15 15:20:54 2003 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Wed Jul 16 12:09:41 2003 +0200
@@ -13,8 +13,8 @@
 
 (*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*)
+  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 =
@@ -77,8 +77,8 @@
     "merge_follows ==
 	 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
 	 guarantees
-	 (\<Inter>i \<in> lessThan Nclients. 
-	  (%s. sublist (merge.Out s) 
+	 (\<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))"
 
@@ -104,9 +104,9 @@
 	 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. 
+	 (\<Inter>i \<in> lessThan Nclients.
 	  (sub i o distr.Out) Fols
-	  (%s. sublist (distr.In s) 
+	  (%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"
@@ -126,25 +126,25 @@
   alloc_safety :: "'a allocState_d program set"
     "alloc_safety ==
 	 Increasing rel
-         guarantees  Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
+         guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"
 
   (*spec (20)*)
   alloc_progress :: "'a allocState_d program set"
     "alloc_progress ==
 	 Increasing ask Int Increasing rel Int
-         Always {s. \<forall>elt \<in> set (ask s). elt <= NbT}
+         Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
          Int
-         (\<Inter>h. {s. h <= giv s & h pfixGe (ask s)}
+         (\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)}
 		 LeadsTo
-	         {s. tokens h <= tokens (rel s)})
-         guarantees  (\<Inter>h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+	         {s. tokens h \<le> tokens (rel s)})
+         guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"
 
   (*spec: preserves part*)
   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"
@@ -179,7 +179,7 @@
 #    {*spec (9.2)*}
 #    network_giv :: "'a systemState program set
 #	"network_giv == \<Inter>i \<in> lessThan Nclients.
-#			    Increasing giv 
+#			    Increasing giv
 #			    guarantees[giv o sub i o client]
 #			    ((giv o sub i o client) Fols giv)"
 
@@ -231,38 +231,39 @@
 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)
+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 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 |]  
+     "[| 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 |]  
+     "[| 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})) =  
+     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
+  ==> M Join G \<in> Always
+          {s. (\<Sum>i \<in> 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 (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
@@ -275,15 +276,15 @@
 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)"
+     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
+          guarantees
+             (bag_of o merge.Out) Fols
+             (%s. \<Sum>i \<in> 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) 
+apply (drule guaranteesD)
   prefer 3
   apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
 done
@@ -292,9 +293,9 @@
 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  
+     "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)
@@ -303,11 +304,11 @@
 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})) =  
+     "[| 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)
@@ -316,7 +317,7 @@
  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}) = 
+       "(\<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
@@ -325,17 +326,17 @@
 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 
+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  
+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 \<in> 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)
@@ -351,33 +352,33 @@
 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)}"
+     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
+      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<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)})"
+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 \<le> NbT)}
+  Int
+  (\<Inter>i \<in> lessThan Nclients.
+   \<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
+        LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s})
+  \<subseteq>
+ (\<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 \<le> NbT)}
+  Int
+  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
+         {s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
+  LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le>
+              (\<Sum>i \<in> 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)