# HG changeset patch
# User paulson
# Date 1056635313 -7200
# Node ID 21e2ff495d81ded0f6c6dc68aa9a20e835fc1800
# Parent  f932be305381d8526a4522da73927f5bb750a5fa
Conversion of "Merge" to Isar format

diff -r f932be305381 -r 21e2ff495d81 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/IsaMakefile	Thu Jun 26 15:48:33 2003 +0200
@@ -123,8 +123,7 @@
   UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
   UNITY/ClientImpl.thy UNITY/Distributor.thy\
   UNITY/Follows.ML UNITY/Follows.thy\
-  UNITY/Increasing.ML UNITY/Increasing.thy\
-  UNITY/Merge.ML UNITY/Merge.thy\
+  UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
   UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
   UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
   UNITY/WFair.ML UNITY/WFair.thy
diff -r f932be305381 -r 21e2ff495d81 src/ZF/UNITY/AllocBase.ML
--- a/src/ZF/UNITY/AllocBase.ML	Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/AllocBase.ML	Thu Jun 26 15:48:33 2003 +0200
@@ -90,6 +90,7 @@
 qed "tokens_append";
 Addsimps [tokens_append];
 
+(*????????????????List.thy*)
 Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
 by (induct_tac "l" 1);
 by Safe_tac;
diff -r f932be305381 -r 21e2ff495d81 src/ZF/UNITY/Merge.ML
--- a/src/ZF/UNITY/Merge.ML	Wed Jun 25 13:17:26 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,163 +0,0 @@
-(*  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 \\<in> 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 \\<in> state ==> s`Out \\<in> 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 \\<in> state ==> s`iOut \\<in> 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 \\<in> 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 \\<in> program ==> \
-\ M ok G <-> (G \\<in> preserves(lift(Out)) &  \
-\      G \\<in> preserves(lift(iOut)) & M \\<in> 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 \\<in> preserves(lift(Out)); G \\<in> preserves(lift(iOut)); \
-\  M \\<in> Allowed(G) |] ==> \
-\ M Join G \\<in> Always({s \\<in> state. length(s`Out)=length(s`iOut)})";
-by (ftac (preserves_type RS subsetD) 1);
-by (subgoal_tac "G \\<in> 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 \\<in> preserves(lift(iOut)); G \\<in> preserves(lift(Out)); \
-\   M \\<in> Allowed(G) |] ==> \
-\ M Join G: Always({s \\<in> state. \\<forall>elt \\<in> 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 \\<in> preserves(lift(iOut)); \
-\   G: preserves(lift(Out)); M \\<in> Allowed(G) |] \
-\ ==> M Join G : Always \
-\   ({s \\<in> state. msetsum(%i. bag_of(sublist(s`Out, \
-\     {k \\<in> 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
-    "(\\<Union>i \\<in> Nclients. {k \\<in> 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 (Asm_full_simp_tac 2);
-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 : (\\<Inter>n \\<in> 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 f932be305381 -r 21e2ff495d81 src/ZF/UNITY/Merge.thy
--- a/src/ZF/UNITY/Merge.thy	Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy	Thu Jun 26 15:48:33 2003 +0200
@@ -7,72 +7,194 @@
 Merge specification
 *)
 
-Merge = AllocBase + Follows +  Guar + GenPrefix +
+theory 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 :: "[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 :: "[i, i] =>i"
   "merge_eq_Out(Out, iOut) == program guarantees
-         Always({s \\<in> state. length(s`Out) = length(s`iOut)})"
+         Always({s \<in> state. length(s`Out) = length(s`iOut)})"
 
   (*spec (12)*)
-  merge_bounded :: i=>i
+  merge_bounded :: "i=>i"
   "merge_bounded(iOut) == program guarantees
-         Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})"
+         Always({s \<in> state. \<forall>elt \<in> 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 :: "[i, i=>i, i, i] =>i"
     "merge_follows(A, In, Out, iOut) ==
-     (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+     (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
 		   guarantees
-     (\\<Inter>n \\<in> Nclients. 
-        (%s. sublist(s`Out, {k \\<in> nat. k < length(s`iOut) &
+     (\<Inter>n \<in> Nclients. 
+        (%s. sublist(s`Out, {k \<in> 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) == \\<Inter>n \\<in> nat. preserves(lift(In(n)))"
+  merge_preserves :: "[i=>i] =>i"
+    "merge_preserves(In) == \<Inter>n \<in> nat. preserves(lift(In(n)))"
 
 (* environmental constraints*)
-  merge_allowed_acts :: [i, i] =>i
+  merge_allowed_acts :: "[i, i] =>i"
   "merge_allowed_acts(Out, iOut) ==
-         {F \\<in> program. AllowedActs(F) =
-            cons(id(state), (\\<Union>G \\<in> preserves(lift(Out)) \\<inter>
+         {F \<in> program. AllowedActs(F) =
+            cons(id(state), (\<Union>G \<in> preserves(lift(Out)) \<inter>
                                    preserves(lift(iOut)). Acts(G)))}"
   
-  merge_spec :: [i, i =>i, i, i]=>i
+  merge_spec :: "[i, i =>i, i, i]=>i"
   "merge_spec(A, In, Out, iOut) ==
-   merge_increasing(A, Out, iOut) \\<inter> merge_eq_Out(Out, iOut) \\<inter>
-   merge_bounded(iOut) \\<inter>  merge_follows(A, In, Out, iOut)
-   \\<inter> merge_allowed_acts(Out, iOut) \\<inter> merge_preserves(In)"
+   merge_increasing(A, Out, iOut) \<inter> merge_eq_Out(Out, iOut) \<inter>
+   merge_bounded(iOut) \<inter>  merge_follows(A, In, Out, iOut)
+   \<inter> merge_allowed_acts(Out, iOut) \<inter> 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       "(\\<forall>n. In(n):var) & Out \\<in> var & iOut \\<in> var"
-    all_distinct_vars "\\<forall>n. all_distinct([In(n), Out, iOut])"
-    type_assumes      "(\\<forall>n. type_of(In(n))=list(A))&
-		       type_of(Out)=list(A) &
-                       type_of(iOut)=list(nat)"
-   default_val_assumes "(\\<forall>n. default_val(In(n))=Nil) &
-                        default_val(Out)=Nil &
-                        default_val(iOut)=Nil"
+locale merge =
+  fixes In   --{*merge's INPUT histories: streams to merge*}
+    and Out  --{*merge's OUTPUT history: merged items*}
+    and iOut --{*merge's OUTPUT history: origins of merged items*}
+    and A    --{*the type of items being merged *}
+    and M
+ assumes var_assumes [simp]:
+           "(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
+     and all_distinct_vars:
+           "\<forall>n. all_distinct([In(n), Out, iOut])"
+     and type_assumes [simp]:
+           "(\<forall>n. type_of(In(n))=list(A)) &
+            type_of(Out)=list(A) &
+            type_of(iOut)=list(nat)"
+     and default_val_assumes [simp]: 
+           "(\<forall>n. default_val(In(n))=Nil) &
+            default_val(Out)=Nil &
+            default_val(iOut)=Nil"
+     and merge_spec:  "M \<in> merge_spec(A, In, Out, iOut)"
+
+
+lemma (in merge) In_value_type [TC,simp]: "s \<in> state ==> s`In(n) \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "In (n)" in apply_type)
+apply auto
+done
+
+lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
+apply (unfold state_def)
+apply (drule_tac a = "Out" in apply_type)
+apply auto
+done
+
+lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
+apply (unfold state_def)
+apply (drule_tac a = "iOut" in apply_type)
+apply auto
+done
+
+lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
+apply (cut_tac merge_spec)
+apply (auto dest: guarantees_type [THEN subsetD]
+            simp add: merge_spec_def merge_increasing_def)
+done
+
+lemma (in merge) merge_Allowed: 
+     "Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))"
+apply (insert merge_spec preserves_type [of "lift (Out)"])
+apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
+done
+
+lemma (in merge) M_ok_iff: 
+     "G \<in> program ==>  
+       M ok G <-> (G \<in> preserves(lift(Out)) &   
+ 	           G \<in> preserves(lift(iOut)) & M \<in> Allowed(G))"
+apply (cut_tac merge_spec)
+apply (auto simp add: merge_Allowed ok_iff_Allowed)
+done
 
-   merge_spec  "M \\<in> merge_spec(A, In, Out, iOut)"
+lemma (in merge) merge_Always_Out_eq_iOut: 
+     "[| G \<in> preserves(lift(Out)); G \<in> preserves(lift(iOut));  
+ 	 M \<in> Allowed(G) |]
+      ==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
+apply (frule preserves_type [THEN subsetD])
+apply (subgoal_tac "G \<in> program")
+ prefer 2 apply (assumption)
+apply (frule M_ok_iff)
+apply (cut_tac merge_spec)
+apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
+done
+
+lemma (in merge) merge_Bounded: 
+     "[| G \<in> preserves(lift(iOut)); G \<in> preserves(lift(Out));  
+	 M \<in> Allowed(G) |] ==>  
+       M \<squnion> G: Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
+apply (frule preserves_type [THEN subsetD])
+apply (frule M_ok_iff)
+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(lift(iOut));  
+    G: preserves(lift(Out)); M \<in> Allowed(G) |]  
+  ==> M \<squnion> G \<in> Always  
+    ({s \<in> state. msetsum(%i. bag_of(sublist(s`Out,  
+      {k \<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})),  
+                   Nclients, A) = bag_of(s`Out)})"
+apply (rule Always_Diff_Un_eq [THEN iffD1]) 
+apply (rule_tac [2] state_AlwaysI [THEN Always_weaken]) 
+apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded]) 
+apply auto
+apply (subst bag_of_sublist_UN_disjoint [symmetric])
+apply (auto simp add: nat_into_Finite set_of_list_conv_nth  [OF iOut_value_type])
+apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
+apply (auto simp add: sublist_upt_eq_take [OF Out_value_type] 
+                      length_type  [OF iOut_value_type]  
+                      take_all [OF _ Out_value_type] 
+                      length_type [OF iOut_value_type])
+apply (rule equalityI)
+apply (blast dest: ltD)
+apply clarify
+apply (subgoal_tac "length (x ` iOut) \<in> nat")
+ prefer 2 apply (simp add: length_type [OF iOut_value_type]); 
+apply (subgoal_tac "xa \<in> nat")
+apply (simp_all add: Ord_mem_iff_lt)
+prefer 2 apply (blast intro: lt_trans)
+apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
+apply (simp add: ltI nat_into_Ord)
+apply (blast dest: ltD)
+done
+
+theorem (in merge) merge_bag_Follows: 
+    "M \<in> (\<Inter>n \<in> 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)"
+apply (cut_tac merge_spec)
+apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
+     apply (simp_all add: M_ok_iff)
+apply clarify
+apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
+   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
+apply (simp add: INT_iff merge_spec_def merge_follows_def)
+apply clarify
+apply (cut_tac merge_spec)
+apply (subgoal_tac "M ok G")
+ prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
+apply (drule guaranteesD)
+apply assumption
+  apply (simp add: merge_spec_def merge_follows_def)
+ apply blast
+apply (simp cong add: Follows_cong
+    add: refl_prefix
+       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
+done
+
 end
 
   
\ No newline at end of file
diff -r f932be305381 -r 21e2ff495d81 src/ZF/UNITY/Monotonicity.ML
--- a/src/ZF/UNITY/Monotonicity.ML	Wed Jun 25 13:17:26 2003 +0200
+++ b/src/ZF/UNITY/Monotonicity.ML	Thu Jun 26 15:48:33 2003 +0200
@@ -25,26 +25,7 @@
 
 (** Monotonicity of take **)
 
-Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
-\   take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]";
-by (induct_tac "xs" 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (etac natE 1);
-by Auto_tac;
-qed_spec_mp "take_succ";
-
-
-Goal "[|xs:list(A); j:nat|] ==> ALL i:nat.  i #+ j le length(xs) --> \
-\   take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))";
-by (induct_tac "xs" 1);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Clarify_tac 1); 
-by (eres_inst_tac [("n","i")] natE 1); 
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "take_add";
-
+(*????premises too strong*)
 Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
 by (case_tac "length(xs) le i" 1);
 by (subgoal_tac "length(xs) le j" 1);