Conversion of "Merge" to Isar format
authorpaulson
Thu Jun 26 15:48:33 2003 +0200 (2003-06-26)
changeset 1407321e2ff495d81
parent 14072 f932be305381
child 14074 93dfce3b6f86
Conversion of "Merge" to Isar format
src/ZF/IsaMakefile
src/ZF/UNITY/AllocBase.ML
src/ZF/UNITY/Merge.ML
src/ZF/UNITY/Merge.thy
src/ZF/UNITY/Monotonicity.ML
     1.1 --- a/src/ZF/IsaMakefile	Wed Jun 25 13:17:26 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Thu Jun 26 15:48:33 2003 +0200
     1.3 @@ -123,8 +123,7 @@
     1.4    UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\
     1.5    UNITY/ClientImpl.thy UNITY/Distributor.thy\
     1.6    UNITY/Follows.ML UNITY/Follows.thy\
     1.7 -  UNITY/Increasing.ML UNITY/Increasing.thy\
     1.8 -  UNITY/Merge.ML UNITY/Merge.thy\
     1.9 +  UNITY/Increasing.ML UNITY/Increasing.thy UNITY/Merge.thy\
    1.10    UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
    1.11    UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
    1.12    UNITY/WFair.ML UNITY/WFair.thy
     2.1 --- a/src/ZF/UNITY/AllocBase.ML	Wed Jun 25 13:17:26 2003 +0200
     2.2 +++ b/src/ZF/UNITY/AllocBase.ML	Thu Jun 26 15:48:33 2003 +0200
     2.3 @@ -90,6 +90,7 @@
     2.4  qed "tokens_append";
     2.5  Addsimps [tokens_append];
     2.6  
     2.7 +(*????????????????List.thy*)
     2.8  Goal "l\\<in>list(A) ==> \\<forall>n\\<in>nat. length(take(n, l))=min(n, length(l))";
     2.9  by (induct_tac "l" 1);
    2.10  by Safe_tac;
     3.1 --- a/src/ZF/UNITY/Merge.ML	Wed Jun 25 13:17:26 2003 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,163 +0,0 @@
     3.4 -(*  Title: ZF/UNITY/Merge
     3.5 -    ID:         $Id$
     3.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3.7 -    Copyright   2002  University of Cambridge
     3.8 -
     3.9 -A multiple-client allocator from a single-client allocator:
    3.10 -Merge specification
    3.11 -*)
    3.12 -Open_locale "Merge";
    3.13 -val all_distinct_vars = thm "all_distinct_vars";
    3.14 -val var_assumes = thm "var_assumes";
    3.15 -val type_assumes = thm "type_assumes";
    3.16 -val default_val_assumes  = thm "default_val_assumes";
    3.17 -
    3.18 -Addsimps [var_assumes, default_val_assumes,  type_assumes];
    3.19 -
    3.20 -Goalw [state_def]
    3.21 -"s \\<in> state ==> s`In(n):list(A)";
    3.22 -by (dres_inst_tac [("a", "In(n)")] apply_type 1);
    3.23 -by Auto_tac;
    3.24 -qed "In_value_type";
    3.25 -AddTCs [In_value_type];
    3.26 -Addsimps [In_value_type];
    3.27 -
    3.28 -Goalw [state_def]
    3.29 -"s \\<in> state ==> s`Out \\<in> list(A)";
    3.30 -by (dres_inst_tac [("a", "Out")] apply_type 1);
    3.31 -by Auto_tac;
    3.32 -qed "Out_value_type";
    3.33 -AddTCs [Out_value_type];
    3.34 -Addsimps [Out_value_type];
    3.35 -
    3.36 -Goalw [state_def]
    3.37 -"s \\<in> state ==> s`iOut \\<in> list(nat)";
    3.38 -by (dres_inst_tac [("a", "iOut")] apply_type 1);
    3.39 -by Auto_tac;
    3.40 -qed "Out_value_type";
    3.41 -AddTCs [Out_value_type];
    3.42 -Addsimps [Out_value_type];
    3.43 -
    3.44 -
    3.45 -val merge = thm "merge_spec";
    3.46 -
    3.47 -Goal "M \\<in> program";
    3.48 -by (cut_facts_tac [merge] 1);
    3.49 -by (auto_tac (claset() addDs [guarantees_type RS subsetD], 
    3.50 -              simpset() addsimps [merge_spec_def, merge_increasing_def]));
    3.51 -qed "M_in_program";
    3.52 -Addsimps [M_in_program];
    3.53 -AddTCs [M_in_program];
    3.54 -
    3.55 -Goal 
    3.56 -"Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))";
    3.57 -by (cut_facts_tac [merge, inst "v"  "lift(Out)" preserves_type] 1);
    3.58 -by (auto_tac (claset(), simpset() addsimps 
    3.59 -         [merge_spec_def, merge_allowed_acts_def, 
    3.60 -          Allowed_def,  safety_prop_Acts_iff]));
    3.61 -qed "merge_Allowed";
    3.62 -
    3.63 -Goal 
    3.64 -"G \\<in> program ==> \
    3.65 -\ M ok G <-> (G \\<in> preserves(lift(Out)) &  \
    3.66 -\      G \\<in> preserves(lift(iOut)) & M \\<in> Allowed(G))";
    3.67 -by (cut_facts_tac [merge] 1); 
    3.68 -by (auto_tac (claset(), simpset() 
    3.69 -         addsimps [merge_Allowed, ok_iff_Allowed]));  
    3.70 -qed "M_ok_iff";
    3.71 -
    3.72 -Goal
    3.73 -"[| G \\<in> preserves(lift(Out)); G \\<in> preserves(lift(iOut)); \
    3.74 -\  M \\<in> Allowed(G) |] ==> \
    3.75 -\ M Join G \\<in> Always({s \\<in> state. length(s`Out)=length(s`iOut)})";
    3.76 -by (ftac (preserves_type RS subsetD) 1);
    3.77 -by (subgoal_tac "G \\<in> program" 1);
    3.78 -by (assume_tac 2);
    3.79 -by (ftac M_ok_iff 1);
    3.80 -by (cut_facts_tac [merge] 1);
    3.81 -by (force_tac (claset() addDs [guaranteesD], 
    3.82 -               simpset() addsimps [merge_spec_def, merge_eq_Out_def]) 1); 
    3.83 -qed "merge_Always_Out_eq_iOut";
    3.84 -
    3.85 -Goal 
    3.86 -"[| G \\<in> preserves(lift(iOut)); G \\<in> preserves(lift(Out)); \
    3.87 -\   M \\<in> Allowed(G) |] ==> \
    3.88 -\ M Join G: Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})";
    3.89 -by (ftac (preserves_type RS subsetD) 1);
    3.90 -by (ftac M_ok_iff 1);
    3.91 -by (cut_facts_tac [merge] 1);
    3.92 -by (force_tac (claset() addDs [guaranteesD], 
    3.93 -               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
    3.94 -qed "merge_Bounded";
    3.95 -
    3.96 -Goal 
    3.97 -"[| G \\<in> preserves(lift(iOut)); \
    3.98 -\   G: preserves(lift(Out)); M \\<in> Allowed(G) |] \
    3.99 -\ ==> M Join G : Always \
   3.100 -\   ({s \\<in> state. msetsum(%i. bag_of(sublist(s`Out, \
   3.101 -\     {k \\<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
   3.102 -\                  Nclients, A) = bag_of(s`Out)})";
   3.103 -by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
   3.104 -           state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
   3.105 -;
   3.106 -by Auto_tac; 
   3.107 -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
   3.108 -by (auto_tac (claset(), simpset() 
   3.109 -              addsimps [nat_into_Finite, set_of_list_conv_nth])); 
   3.110 -by (subgoal_tac
   3.111 -    "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
   3.112 -by Auto_tac;
   3.113 -by (resolve_tac [equalityI] 1);
   3.114 -by (blast_tac (claset() addDs [ltD]) 1); 
   3.115 -by (Clarify_tac 1); 
   3.116 -by (subgoal_tac "length(x ` iOut) : nat" 1);
   3.117 -by (Asm_full_simp_tac 2);
   3.118 -by (subgoal_tac "xa : nat" 1); 
   3.119 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
   3.120 -by (blast_tac (claset() addIs [lt_trans]) 2);
   3.121 -by (dres_inst_tac [("x", "nth(xa, x`iOut)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec 1);
   3.122 -by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
   3.123 -by (blast_tac (claset() addDs [ltD]) 1); 
   3.124 -qed "merge_bag_Follows_lemma";
   3.125 -
   3.126 -Goal
   3.127 -"M : (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
   3.128 -\       guarantees  \
   3.129 -\ (%s. bag_of(s`Out)) Fols \
   3.130 -\ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
   3.131 -by (cut_facts_tac [merge] 1);
   3.132 -by (rtac (merge_bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
   3.133 -by (ALLGOALS(rotate_tac ~1 ));
   3.134 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [M_ok_iff])));
   3.135 -by Auto_tac;
   3.136 -by (rtac Follows_state_ofD1 1);
   3.137 -by (rtac Follows_msetsum_UN 1);
   3.138 -by (ALLGOALS(Clarify_tac));
   3.139 -by (resolve_tac [conjI] 2);
   3.140 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 2);
   3.141 -by (resolve_tac [conjI] 3);
   3.142 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 3);
   3.143 -by (resolve_tac [conjI] 4);
   3.144 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 4);
   3.145 -by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 5);
   3.146 -by (ALLGOALS(Asm_simp_tac));
   3.147 -by (resolve_tac [nat_into_Finite] 2);
   3.148 -by (Asm_simp_tac 2);
   3.149 -by (asm_full_simp_tac (simpset() addsimps [INT_iff,
   3.150 -                      merge_spec_def, merge_follows_def]) 1);
   3.151 -by Auto_tac;
   3.152 -by (cut_facts_tac [merge] 1);
   3.153 -by (subgoal_tac "M ok G" 1);
   3.154 -by (dtac guaranteesD 1); 
   3.155 -by (assume_tac 1);
   3.156 -by (force_tac (claset() addIs[M_ok_iff RS iffD2], simpset()) 4);
   3.157 -by (rewrite_goal_tac [merge_spec_def, merge_follows_def] 1);
   3.158 -by (Blast_tac 1);
   3.159 -by (Asm_simp_tac 1);
   3.160 -by (asm_full_simp_tac
   3.161 -    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
   3.162 -             refl_prefix, trans_on_MultLe] 
   3.163 -            addcongs [Follows_cong]) 1); 
   3.164 -qed "merge_bag_Follows";
   3.165 -Close_locale "Merge";
   3.166 -
     4.1 --- a/src/ZF/UNITY/Merge.thy	Wed Jun 25 13:17:26 2003 +0200
     4.2 +++ b/src/ZF/UNITY/Merge.thy	Thu Jun 26 15:48:33 2003 +0200
     4.3 @@ -7,72 +7,194 @@
     4.4  Merge specification
     4.5  *)
     4.6  
     4.7 -Merge = AllocBase + Follows +  Guar + GenPrefix +
     4.8 +theory Merge = AllocBase + Follows +  Guar + GenPrefix:
     4.9 +
    4.10  (** Merge specification (the number of inputs is Nclients) ***)
    4.11  (** Parameter A represents the type of items to Merge **)
    4.12 +
    4.13  constdefs
    4.14    (*spec (10)*)
    4.15 -  merge_increasing :: [i, i, i] =>i
    4.16 +  merge_increasing :: "[i, i, i] =>i"
    4.17      "merge_increasing(A, Out, iOut) == program guarantees
    4.18           (lift(Out) IncreasingWrt  prefix(A)/list(A)) Int
    4.19           (lift(iOut) IncreasingWrt prefix(nat)/list(nat))"
    4.20  
    4.21    (*spec (11)*)
    4.22 -  merge_eq_Out :: [i, i] =>i
    4.23 +  merge_eq_Out :: "[i, i] =>i"
    4.24    "merge_eq_Out(Out, iOut) == program guarantees
    4.25 -         Always({s \\<in> state. length(s`Out) = length(s`iOut)})"
    4.26 +         Always({s \<in> state. length(s`Out) = length(s`iOut)})"
    4.27  
    4.28    (*spec (12)*)
    4.29 -  merge_bounded :: i=>i
    4.30 +  merge_bounded :: "i=>i"
    4.31    "merge_bounded(iOut) == program guarantees
    4.32 -         Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})"
    4.33 +         Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
    4.34    
    4.35    (*spec (13)*)
    4.36    (* Parameter A represents the type of tokens *)
    4.37 -  merge_follows :: [i, i=>i, i, i] =>i
    4.38 +  merge_follows :: "[i, i=>i, i, i] =>i"
    4.39      "merge_follows(A, In, Out, iOut) ==
    4.40 -     (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
    4.41 +     (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
    4.42  		   guarantees
    4.43 -     (\\<Inter>n \\<in> Nclients. 
    4.44 -        (%s. sublist(s`Out, {k \\<in> nat. k < length(s`iOut) &
    4.45 +     (\<Inter>n \<in> Nclients. 
    4.46 +        (%s. sublist(s`Out, {k \<in> nat. k < length(s`iOut) &
    4.47                        nth(k, s`iOut) = n})) Fols lift(In(n))
    4.48           Wrt prefix(A)/list(A))"
    4.49  
    4.50    (*spec: preserves part*)
    4.51 -  merge_preserves :: [i=>i] =>i
    4.52 -    "merge_preserves(In) == \\<Inter>n \\<in> nat. preserves(lift(In(n)))"
    4.53 +  merge_preserves :: "[i=>i] =>i"
    4.54 +    "merge_preserves(In) == \<Inter>n \<in> nat. preserves(lift(In(n)))"
    4.55  
    4.56  (* environmental constraints*)
    4.57 -  merge_allowed_acts :: [i, i] =>i
    4.58 +  merge_allowed_acts :: "[i, i] =>i"
    4.59    "merge_allowed_acts(Out, iOut) ==
    4.60 -         {F \\<in> program. AllowedActs(F) =
    4.61 -            cons(id(state), (\\<Union>G \\<in> preserves(lift(Out)) \\<inter>
    4.62 +         {F \<in> program. AllowedActs(F) =
    4.63 +            cons(id(state), (\<Union>G \<in> preserves(lift(Out)) \<inter>
    4.64                                     preserves(lift(iOut)). Acts(G)))}"
    4.65    
    4.66 -  merge_spec :: [i, i =>i, i, i]=>i
    4.67 +  merge_spec :: "[i, i =>i, i, i]=>i"
    4.68    "merge_spec(A, In, Out, iOut) ==
    4.69 -   merge_increasing(A, Out, iOut) \\<inter> merge_eq_Out(Out, iOut) \\<inter>
    4.70 -   merge_bounded(iOut) \\<inter>  merge_follows(A, In, Out, iOut)
    4.71 -   \\<inter> merge_allowed_acts(Out, iOut) \\<inter> merge_preserves(In)"
    4.72 +   merge_increasing(A, Out, iOut) \<inter> merge_eq_Out(Out, iOut) \<inter>
    4.73 +   merge_bounded(iOut) \<inter>  merge_follows(A, In, Out, iOut)
    4.74 +   \<inter> merge_allowed_acts(Out, iOut) \<inter> merge_preserves(In)"
    4.75  
    4.76  (** State definitions.  OUTPUT variables are locals **)
    4.77 -locale Merge =
    4.78 -  fixes In :: i=>i (*merge's INPUT histories: streams to merge*)
    4.79 -        Out :: i   (*merge's OUTPUT history: merged items*)
    4.80 -        iOut :: i  (*merge's OUTPUT history: origins of merged items*)
    4.81 -        A  :: i    (*the type of items being merged *)
    4.82 -        M :: i
    4.83 - assumes
    4.84 -    var_assumes       "(\\<forall>n. In(n):var) & Out \\<in> var & iOut \\<in> var"
    4.85 -    all_distinct_vars "\\<forall>n. all_distinct([In(n), Out, iOut])"
    4.86 -    type_assumes      "(\\<forall>n. type_of(In(n))=list(A))&
    4.87 -		       type_of(Out)=list(A) &
    4.88 -                       type_of(iOut)=list(nat)"
    4.89 -   default_val_assumes "(\\<forall>n. default_val(In(n))=Nil) &
    4.90 -                        default_val(Out)=Nil &
    4.91 -                        default_val(iOut)=Nil"
    4.92 +locale merge =
    4.93 +  fixes In   --{*merge's INPUT histories: streams to merge*}
    4.94 +    and Out  --{*merge's OUTPUT history: merged items*}
    4.95 +    and iOut --{*merge's OUTPUT history: origins of merged items*}
    4.96 +    and A    --{*the type of items being merged *}
    4.97 +    and M
    4.98 + assumes var_assumes [simp]:
    4.99 +           "(\<forall>n. In(n):var) & Out \<in> var & iOut \<in> var"
   4.100 +     and all_distinct_vars:
   4.101 +           "\<forall>n. all_distinct([In(n), Out, iOut])"
   4.102 +     and type_assumes [simp]:
   4.103 +           "(\<forall>n. type_of(In(n))=list(A)) &
   4.104 +            type_of(Out)=list(A) &
   4.105 +            type_of(iOut)=list(nat)"
   4.106 +     and default_val_assumes [simp]: 
   4.107 +           "(\<forall>n. default_val(In(n))=Nil) &
   4.108 +            default_val(Out)=Nil &
   4.109 +            default_val(iOut)=Nil"
   4.110 +     and merge_spec:  "M \<in> merge_spec(A, In, Out, iOut)"
   4.111 +
   4.112 +
   4.113 +lemma (in merge) In_value_type [TC,simp]: "s \<in> state ==> s`In(n) \<in> list(A)"
   4.114 +apply (unfold state_def)
   4.115 +apply (drule_tac a = "In (n)" in apply_type)
   4.116 +apply auto
   4.117 +done
   4.118 +
   4.119 +lemma (in merge) Out_value_type [TC,simp]: "s \<in> state ==> s`Out \<in> list(A)"
   4.120 +apply (unfold state_def)
   4.121 +apply (drule_tac a = "Out" in apply_type)
   4.122 +apply auto
   4.123 +done
   4.124 +
   4.125 +lemma (in merge) iOut_value_type [TC,simp]: "s \<in> state ==> s`iOut \<in> list(nat)"
   4.126 +apply (unfold state_def)
   4.127 +apply (drule_tac a = "iOut" in apply_type)
   4.128 +apply auto
   4.129 +done
   4.130 +
   4.131 +lemma (in merge) M_in_program [intro,simp]: "M \<in> program"
   4.132 +apply (cut_tac merge_spec)
   4.133 +apply (auto dest: guarantees_type [THEN subsetD]
   4.134 +            simp add: merge_spec_def merge_increasing_def)
   4.135 +done
   4.136 +
   4.137 +lemma (in merge) merge_Allowed: 
   4.138 +     "Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))"
   4.139 +apply (insert merge_spec preserves_type [of "lift (Out)"])
   4.140 +apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
   4.141 +done
   4.142 +
   4.143 +lemma (in merge) M_ok_iff: 
   4.144 +     "G \<in> program ==>  
   4.145 +       M ok G <-> (G \<in> preserves(lift(Out)) &   
   4.146 + 	           G \<in> preserves(lift(iOut)) & M \<in> Allowed(G))"
   4.147 +apply (cut_tac merge_spec)
   4.148 +apply (auto simp add: merge_Allowed ok_iff_Allowed)
   4.149 +done
   4.150  
   4.151 -   merge_spec  "M \\<in> merge_spec(A, In, Out, iOut)"
   4.152 +lemma (in merge) merge_Always_Out_eq_iOut: 
   4.153 +     "[| G \<in> preserves(lift(Out)); G \<in> preserves(lift(iOut));  
   4.154 + 	 M \<in> Allowed(G) |]
   4.155 +      ==> M \<squnion> G \<in> Always({s \<in> state. length(s`Out)=length(s`iOut)})"
   4.156 +apply (frule preserves_type [THEN subsetD])
   4.157 +apply (subgoal_tac "G \<in> program")
   4.158 + prefer 2 apply (assumption)
   4.159 +apply (frule M_ok_iff)
   4.160 +apply (cut_tac merge_spec)
   4.161 +apply (force dest: guaranteesD simp add: merge_spec_def merge_eq_Out_def)
   4.162 +done
   4.163 +
   4.164 +lemma (in merge) merge_Bounded: 
   4.165 +     "[| G \<in> preserves(lift(iOut)); G \<in> preserves(lift(Out));  
   4.166 +	 M \<in> Allowed(G) |] ==>  
   4.167 +       M \<squnion> G: Always({s \<in> state. \<forall>elt \<in> set_of_list(s`iOut). elt<Nclients})"
   4.168 +apply (frule preserves_type [THEN subsetD])
   4.169 +apply (frule M_ok_iff)
   4.170 +apply (cut_tac merge_spec)
   4.171 +apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
   4.172 +done
   4.173 +
   4.174 +lemma (in merge) merge_bag_Follows_lemma: 
   4.175 +"[| G \<in> preserves(lift(iOut));  
   4.176 +    G: preserves(lift(Out)); M \<in> Allowed(G) |]  
   4.177 +  ==> M \<squnion> G \<in> Always  
   4.178 +    ({s \<in> state. msetsum(%i. bag_of(sublist(s`Out,  
   4.179 +      {k \<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})),  
   4.180 +                   Nclients, A) = bag_of(s`Out)})"
   4.181 +apply (rule Always_Diff_Un_eq [THEN iffD1]) 
   4.182 +apply (rule_tac [2] state_AlwaysI [THEN Always_weaken]) 
   4.183 +apply (rule Always_Int_I [OF merge_Always_Out_eq_iOut merge_Bounded]) 
   4.184 +apply auto
   4.185 +apply (subst bag_of_sublist_UN_disjoint [symmetric])
   4.186 +apply (auto simp add: nat_into_Finite set_of_list_conv_nth  [OF iOut_value_type])
   4.187 +apply (subgoal_tac " (\<Union>i \<in> Nclients. {k \<in> nat. k < length (x`iOut) & nth (k, x`iOut) = i}) = length (x`iOut) ")
   4.188 +apply (auto simp add: sublist_upt_eq_take [OF Out_value_type] 
   4.189 +                      length_type  [OF iOut_value_type]  
   4.190 +                      take_all [OF _ Out_value_type] 
   4.191 +                      length_type [OF iOut_value_type])
   4.192 +apply (rule equalityI)
   4.193 +apply (blast dest: ltD)
   4.194 +apply clarify
   4.195 +apply (subgoal_tac "length (x ` iOut) \<in> nat")
   4.196 + prefer 2 apply (simp add: length_type [OF iOut_value_type]); 
   4.197 +apply (subgoal_tac "xa \<in> nat")
   4.198 +apply (simp_all add: Ord_mem_iff_lt)
   4.199 +prefer 2 apply (blast intro: lt_trans)
   4.200 +apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
   4.201 +apply (simp add: ltI nat_into_Ord)
   4.202 +apply (blast dest: ltD)
   4.203 +done
   4.204 +
   4.205 +theorem (in merge) merge_bag_Follows: 
   4.206 +    "M \<in> (\<Inter>n \<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))  
   4.207 +	    guarantees   
   4.208 +      (%s. bag_of(s`Out)) Fols  
   4.209 +      (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)"
   4.210 +apply (cut_tac merge_spec)
   4.211 +apply (rule merge_bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI])
   4.212 +     apply (simp_all add: M_ok_iff)
   4.213 +apply clarify
   4.214 +apply (rule Follows_state_ofD1 [OF Follows_msetsum_UN])
   4.215 +   apply (simp_all add: nat_into_Finite bag_of_multiset [of _ A])
   4.216 +apply (simp add: INT_iff merge_spec_def merge_follows_def)
   4.217 +apply clarify
   4.218 +apply (cut_tac merge_spec)
   4.219 +apply (subgoal_tac "M ok G")
   4.220 + prefer 2 apply (force intro: M_ok_iff [THEN iffD2])
   4.221 +apply (drule guaranteesD)
   4.222 +apply assumption
   4.223 +  apply (simp add: merge_spec_def merge_follows_def)
   4.224 + apply blast
   4.225 +apply (simp cong add: Follows_cong
   4.226 +    add: refl_prefix
   4.227 +       mono_bag_of [THEN subset_Follows_comp, THEN subsetD, unfolded comp_def])
   4.228 +done
   4.229 +
   4.230  end
   4.231  
   4.232    
   4.233 \ No newline at end of file
     5.1 --- a/src/ZF/UNITY/Monotonicity.ML	Wed Jun 25 13:17:26 2003 +0200
     5.2 +++ b/src/ZF/UNITY/Monotonicity.ML	Thu Jun 26 15:48:33 2003 +0200
     5.3 @@ -25,26 +25,7 @@
     5.4  
     5.5  (** Monotonicity of take **)
     5.6  
     5.7 -Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
     5.8 -\   take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]";
     5.9 -by (induct_tac "xs" 1);
    5.10 -by (Asm_full_simp_tac 1);
    5.11 -by (Clarify_tac 1);
    5.12 -by (Asm_full_simp_tac 1);
    5.13 -by (etac natE 1);
    5.14 -by Auto_tac;
    5.15 -qed_spec_mp "take_succ";
    5.16 -
    5.17 -
    5.18 -Goal "[|xs:list(A); j:nat|] ==> ALL i:nat.  i #+ j le length(xs) --> \
    5.19 -\   take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))";
    5.20 -by (induct_tac "xs" 1);
    5.21 -by (ALLGOALS(Asm_full_simp_tac));
    5.22 -by (Clarify_tac 1); 
    5.23 -by (eres_inst_tac [("n","i")] natE 1); 
    5.24 -by (ALLGOALS(Asm_full_simp_tac));
    5.25 -qed_spec_mp "take_add";
    5.26 -
    5.27 +(*????premises too strong*)
    5.28  Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
    5.29  by (case_tac "length(xs) le i" 1);
    5.30  by (subgoal_tac "length(xs) le j" 1);