some new ZF/UNITY material from Sidi Ehmety
authorpaulson
Wed May 28 18:13:41 2003 +0200 (2003-05-28)
changeset 14052e9c9f69e4f63
parent 14051 4b61bbb0dcab
child 14053 4daa384f4fd7
some new ZF/UNITY material from Sidi Ehmety
src/ZF/IsaMakefile
src/ZF/OrderType.thy
src/ZF/UNITY/AllocBase.ML
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/Distributor.ML
src/ZF/UNITY/Distributor.thy
src/ZF/UNITY/Follows.ML
src/ZF/UNITY/Follows.thy
src/ZF/UNITY/Increasing.ML
src/ZF/UNITY/Increasing.thy
src/ZF/UNITY/Monotonicity.ML
src/ZF/UNITY/Monotonicity.thy
src/ZF/UNITY/MultisetSum.ML
src/ZF/UNITY/MultisetSum.thy
src/ZF/UNITY/ROOT.ML
     1.1 --- a/src/ZF/IsaMakefile	Wed May 28 10:48:20 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Wed May 28 18:13:41 2003 +0200
     1.3 @@ -120,6 +120,12 @@
     1.4    UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
     1.5    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
     1.6    UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
     1.7 +  UNITY/AllocBase.ML UNITY/AllocBase.thy\
     1.8 +  UNITY/Distributor.ML UNITY/Distributor.thy\
     1.9 +  UNITY/Follows.ML UNITY/Follows.thy\
    1.10 +  UNITY/Increasing.ML UNITY/Increasing.thy\
    1.11 +  UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
    1.12 +  UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
    1.13    UNITY/WFair.ML UNITY/WFair.thy
    1.14  	@$(ISATOOL) usedir $(OUT)/ZF UNITY
    1.15  
     2.1 --- a/src/ZF/OrderType.thy	Wed May 28 10:48:20 2003 +0200
     2.2 +++ b/src/ZF/OrderType.thy	Wed May 28 18:13:41 2003 +0200
     2.3 @@ -1003,6 +1003,9 @@
     2.4  lemma tot_ord_Lt: "tot_ord(nat,Lt)"
     2.5  by (simp add: tot_ord_def linear_Lt part_ord_Lt)
     2.6  
     2.7 +lemma well_ord_Lt: "well_ord(nat,Lt)"
     2.8 +by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt)
     2.9 +
    2.10  
    2.11  
    2.12  ML {*
    2.13 @@ -1117,6 +1120,7 @@
    2.14  val part_ord_Lt = thm "part_ord_Lt";
    2.15  val linear_Lt = thm "linear_Lt";
    2.16  val tot_ord_Lt = thm "tot_ord_Lt";
    2.17 +val well_ord_Lt = thm "well_ord_Lt";
    2.18  *}
    2.19  
    2.20  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/UNITY/AllocBase.ML	Wed May 28 18:13:41 2003 +0200
     3.3 @@ -0,0 +1,436 @@
     3.4 +(*  Title:      ZF/UNITY/AllocBase.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3.7 +    Copyright   2001  University of Cambridge
     3.8 +
     3.9 +Common declarations for Chandy and Charpentier's Allocator
    3.10 +*)
    3.11 +
    3.12 +(*????remove from Union.ML:AddSEs [not_emptyE];*)
    3.13 +Delrules [not_emptyE];
    3.14 +
    3.15 +Goal "0 < Nclients & 0 < NbT";
    3.16 +by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    3.17 +by (auto_tac (claset() addIs [Ord_0_lt], simpset()));
    3.18 +qed "Nclients_NbT_gt_0";
    3.19 +Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
    3.20 +
    3.21 +Goal "Nclients ~= 0 & NbT ~= 0";
    3.22 +by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    3.23 +by Auto_tac;
    3.24 +qed "Nclients_NbT_not_0";
    3.25 +Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0  RS conjunct2];
    3.26 +
    3.27 +Goal "Nclients:nat & NbT:nat";
    3.28 +by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
    3.29 +by Auto_tac;
    3.30 +qed "Nclients_NbT_type";
    3.31 +Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    3.32 +AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
    3.33 +
    3.34 +Goal "b:Inter(RepFun(Nclients, B)) <-> (ALL x:Nclients. b:B(x))";
    3.35 +by (auto_tac (claset(), simpset() addsimps [INT_iff]));
    3.36 +by (res_inst_tac [("x", "0")] exI 1);
    3.37 +by (rtac ltD 1); 
    3.38 +by Auto_tac; 
    3.39 +qed "INT_Nclient_iff";
    3.40 +AddIffs [INT_Nclient_iff];
    3.41 +
    3.42 +val succ_def = thm "succ_def";
    3.43 +
    3.44 +Goal "n:nat ==> \
    3.45 +\     (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
    3.46 +\     setsum(f, n) $<= setsum(g,n)";
    3.47 +by (induct_tac "n" 1);
    3.48 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [])));
    3.49 +by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
    3.50 +by (Clarify_tac 1);
    3.51 +by (Asm_simp_tac 1);
    3.52 +by (subgoal_tac "ALL i:nat. i<x--> f(i) $<= g(i)" 1);
    3.53 +by (resolve_tac [zadd_zle_mono] 1);
    3.54 +by (thin_tac "succ(x)=cons(x,x)" 1);
    3.55 +by (ALLGOALS(Asm_simp_tac));
    3.56 +by (thin_tac "succ(x)=cons(x, x)" 1);
    3.57 +by (Clarify_tac 1);
    3.58 +by (dtac leI 1);
    3.59 +by (Asm_simp_tac 1);
    3.60 +by (asm_simp_tac (simpset() addsimps [nat_into_Finite,
    3.61 +                                      mem_not_refl, succ_def]) 1);
    3.62 +qed_spec_mp "setsum_fun_mono";
    3.63 +
    3.64 +Goal "l:list(A) ==> tokens(l):nat";
    3.65 +by (etac list.induct 1);
    3.66 +by Auto_tac;
    3.67 +qed "tokens_type";
    3.68 +AddTCs [tokens_type];
    3.69 +Addsimps [tokens_type];
    3.70 +
    3.71 +Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
    3.72 +\  --> tokens(xs) le tokens(ys)";
    3.73 +by (induct_tac "xs" 1);
    3.74 +by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], 
    3.75 +              simpset() addsimps [prefix_def]));
    3.76 +qed_spec_mp "tokens_mono_aux";
    3.77 +
    3.78 +Goal "[| <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
    3.79 +\     tokens(xs) le tokens(ys)";
    3.80 +by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
    3.81 +qed "tokens_mono";
    3.82 +
    3.83 +Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le ,tokens)";
    3.84 +by (auto_tac (claset() addIs [tokens_mono],
    3.85 +             simpset() addsimps [Le_def]));
    3.86 +qed "mono_tokens";
    3.87 +Addsimps [mono_tokens];
    3.88 +AddIs [mono_tokens];
    3.89 +
    3.90 +Goal 
    3.91 +"[| xs:list(A); ys:list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
    3.92 +by (induct_tac "xs" 1);
    3.93 +by Auto_tac;
    3.94 +qed "tokens_append";
    3.95 +Addsimps [tokens_append];
    3.96 +
    3.97 +Goal "l:list(A) ==> ALL n:nat. length(take(n, l))=min(n, length(l))";
    3.98 +by (induct_tac "l" 1);
    3.99 +by Safe_tac;
   3.100 +by (ALLGOALS(Asm_simp_tac));
   3.101 +by (etac natE 1);
   3.102 +by (ALLGOALS(Asm_simp_tac));
   3.103 +qed "length_take";
   3.104 +
   3.105 +(** bag_of **)
   3.106 +
   3.107 +Goal "l:list(A) ==>bag_of(l):Mult(A)";
   3.108 +by (induct_tac "l" 1);
   3.109 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   3.110 +qed "bag_of_type";
   3.111 +AddTCs [bag_of_type];
   3.112 +Addsimps [bag_of_type];
   3.113 +
   3.114 +Goal "l:list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
   3.115 +by (dtac bag_of_type 1);
   3.116 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   3.117 +qed "bag_of_multiset";
   3.118 +
   3.119 +Goal "[| xs:list(A); ys:list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
   3.120 +by (induct_tac "xs" 1);
   3.121 +by (auto_tac (claset(), simpset() 
   3.122 +       addsimps [bag_of_multiset, munion_assoc]));
   3.123 +qed "bag_of_append";
   3.124 +Addsimps [bag_of_append];
   3.125 +
   3.126 +Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
   3.127 +\  --> <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
   3.128 +by (induct_tac "xs" 1);
   3.129 +by (ALLGOALS(Clarify_tac));
   3.130 +by (ftac bag_of_multiset 1);
   3.131 +by (forw_inst_tac [("l", "ys")] bag_of_multiset 2);
   3.132 +by (auto_tac (claset() addIs [empty_le_MultLe], 
   3.133 +              simpset() addsimps [prefix_def]));
   3.134 +by (rtac munion_mono 1);
   3.135 +by (force_tac (claset(), simpset() addsimps 
   3.136 +               [MultLe_def, Mult_iff_multiset]) 1);
   3.137 +by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
   3.138 +qed_spec_mp "bag_of_mono_aux";
   3.139 +
   3.140 +Goal "[|  <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
   3.141 +\  <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
   3.142 +by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
   3.143 +qed "bag_of_mono";
   3.144 +AddIs [bag_of_mono];
   3.145 +
   3.146 +Goalw [mono1_def]
   3.147 + "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)";
   3.148 +by (auto_tac (claset(), simpset() addsimps [bag_of_type]));
   3.149 +qed "mono_bag_of";
   3.150 +Addsimps [mono_bag_of];
   3.151 +
   3.152 +
   3.153 +(** msetsum **)
   3.154 +
   3.155 +bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
   3.156 +
   3.157 +Goal "l : list(A) ==> C Int length(l) : Fin(length(l))";
   3.158 +by (dtac length_type 1); 
   3.159 +by (rtac Fin_subset 1); 
   3.160 +by (rtac Int_lower2 1);
   3.161 +by (etac nat_into_Fin 1); 
   3.162 +qed "list_Int_length_Fin";
   3.163 +
   3.164 +
   3.165 +
   3.166 +Goal "[|xs \\<in> list(A); k \\<in> C \\<inter> length(xs)|] ==> k < length(xs)"; 
   3.167 +by (asm_full_simp_tac (simpset() addsimps [ltI]) 1); 
   3.168 +qed "mem_Int_imp_lt_length";
   3.169 +
   3.170 +
   3.171 +Goal "[|C \\<subseteq> nat; x \\<in> A; xs \\<in> list(A)|]  \
   3.172 +\ ==>  msetsum(\\<lambda>i. {#nth(i, xs @ [x])#}, C \\<inter> succ(length(xs)), A) = \
   3.173 +\      (if length(xs) \\<in> C then \
   3.174 +\         {#x#} +# msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A) \
   3.175 +\       else msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A))"; 
   3.176 +by (asm_full_simp_tac (simpset() addsimps [subsetD, nth_append, lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   3.177 +by (asm_full_simp_tac (simpset() addsimps [Int_succ_right]) 1);
   3.178 +by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   3.179 +by (Clarify_tac 1);
   3.180 +by (stac msetsum_cons 1);
   3.181 +by (rtac succI1 3);  
   3.182 +by (blast_tac (claset() addIs [list_Int_length_Fin, subset_succI RS Fin_mono RS subsetD]) 1); 
   3.183 +by (asm_full_simp_tac (simpset() addsimps [mem_not_refl]) 1); 
   3.184 +by (asm_full_simp_tac (simpset() addsimps [nth_type, lt_not_refl]) 1); 
   3.185 +by (blast_tac (claset() addIs [nat_into_Ord, ltI, length_type]) 1);
   3.186 +by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
   3.187 +qed "bag_of_sublist_lemma";
   3.188 +
   3.189 +Goal "l:list(A) ==> \
   3.190 +\ C <= nat ==> \
   3.191 +\ bag_of(sublist(l, C)) = \
   3.192 +\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   3.193 +by (etac list_append_induct  1);
   3.194 +by (Simp_tac 1);
   3.195 +by (asm_simp_tac (simpset() addsimps [sublist_append, nth_append, 
   3.196 +          bag_of_sublist_lemma, munion_commute, bag_of_sublist_lemma, 
   3.197 +          msetsum_multiset, munion_0]) 1);  
   3.198 +qed "bag_of_sublist_lemma2";
   3.199 +
   3.200 +
   3.201 +Goal "l \\<in> list(A) ==> nat \\<inter> length(l) = length(l)";
   3.202 +by (rtac Int_absorb1 1);
   3.203 +by (rtac OrdmemD 1);  
   3.204 +by Auto_tac; 
   3.205 +qed "nat_Int_length_eq";
   3.206 +
   3.207 +(*eliminating the assumption C<=nat*)
   3.208 +Goal "l:list(A) ==> \
   3.209 +\ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
   3.210 +by (subgoal_tac
   3.211 +      " bag_of(sublist(l, C Int nat)) = \
   3.212 +\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)" 1);
   3.213 +by (asm_full_simp_tac (simpset() addsimps [sublist_Int_eq]) 1); 
   3.214 +by (asm_full_simp_tac (simpset() addsimps [bag_of_sublist_lemma2, Int_lower2, Int_assoc, nat_Int_length_eq]) 1); 
   3.215 +qed "bag_of_sublist";
   3.216 +
   3.217 +Goal 
   3.218 +"l:list(A) ==> \
   3.219 +\ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
   3.220 +\     bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
   3.221 +by (subgoal_tac
   3.222 +      "B Int C Int length(l) = \
   3.223 +\      (B Int length(l)) Int (C Int length(l))" 1);
   3.224 +by (blast_tac (claset() addIs []) 2);
   3.225 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist, 
   3.226 +                                      Int_Un_distrib2, msetsum_Un_Int]) 1); 
   3.227 +by (resolve_tac [msetsum_Un_Int] 1);
   3.228 +by (REPEAT (etac list_Int_length_Fin 1)); 
   3.229 + by (asm_full_simp_tac (simpset() addsimps [ltI, nth_type]) 1); 
   3.230 +qed "bag_of_sublist_Un_Int";
   3.231 +
   3.232 +
   3.233 +Goal "[| l:list(A); B Int C = 0  |]\
   3.234 +\     ==> bag_of(sublist(l, B Un C)) = \
   3.235 +\         bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; 
   3.236 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym, 
   3.237 +                  sublist_type,  bag_of_multiset]) 1);
   3.238 +qed "bag_of_sublist_Un_disjoint";
   3.239 +
   3.240 +Goal "[| Finite(I); ALL i:I. ALL j:I. i~=j --> A(i) Int A(j) = 0; \
   3.241 +\ l:list(B) |] \
   3.242 +\     ==> bag_of(sublist(l, UN i:I. A(i))) =  \
   3.243 +\         (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";  
   3.244 +by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
   3.245 +                            addsimps [bag_of_sublist]) 1);
   3.246 +by (stac (inst "A" "length(l)" msetsum_UN_disjoint) 1);
   3.247 +by (dresolve_tac [Finite_into_Fin] 1);
   3.248 +by (assume_tac 1);
   3.249 +by (Force_tac 3);
   3.250 +by (auto_tac (claset() addSIs [Fin_IntI2, Finite_into_Fin], 
   3.251 +              simpset() addsimps [ltI, nth_type, length_type, nat_into_Finite]));
   3.252 +qed_spec_mp "bag_of_sublist_UN_disjoint";
   3.253 +
   3.254 +
   3.255 +Goalw [part_ord_def, Lt_def, irrefl_def, trans_on_def]
   3.256 +  "part_ord(nat, Lt)";
   3.257 +by (auto_tac (claset() addIs [lt_trans], simpset()));
   3.258 +qed "part_ord_Lt";
   3.259 +Addsimps [part_ord_Lt];
   3.260 +
   3.261 +
   3.262 +(** all_distinct **)
   3.263 +
   3.264 +Goalw [all_distinct_def] "all_distinct(Nil)";
   3.265 +by Auto_tac;
   3.266 +qed "all_distinct_Nil";
   3.267 +
   3.268 +Goalw [all_distinct_def] 
   3.269 +"all_distinct(Cons(a, l)) <-> \
   3.270 +\ (a:set_of_list(l) --> False) & (a ~: set_of_list(l) --> all_distinct(l))";
   3.271 +by (auto_tac (claset() addEs [list.elim], simpset()));
   3.272 +qed "all_distinct_Cons";
   3.273 +Addsimps [all_distinct_Nil, all_distinct_Cons];
   3.274 +
   3.275 +(** state_of **)
   3.276 +Goalw [state_of_def] "s:state ==> state_of(s)=s";
   3.277 +by Auto_tac;
   3.278 +qed "state_of_state";
   3.279 +Addsimps [state_of_state];
   3.280 +
   3.281 +
   3.282 +Goalw [state_of_def] "state_of(state_of(s))=state_of(s)";
   3.283 +by Auto_tac;
   3.284 +qed "state_of_idem";
   3.285 +Addsimps [state_of_idem];
   3.286 +
   3.287 +
   3.288 +Goalw [state_of_def] "state_of(s):state";
   3.289 +by Auto_tac;
   3.290 +qed "state_of_type";
   3.291 +Addsimps [state_of_type];
   3.292 +AddTCs [state_of_type];
   3.293 +
   3.294 +Goalw [lift_def] "lift(x, s)=s`x";
   3.295 +by (Simp_tac 1);
   3.296 +qed "lift_apply";
   3.297 +Addsimps [lift_apply];
   3.298 +
   3.299 +(** Used in ClientImp **)
   3.300 +
   3.301 +Goalw [Increasing_def]
   3.302 +"Increasing(A, r, %s. f(state_of(s))) = \
   3.303 +\ Increasing(A, r, f)";
   3.304 +by Auto_tac;
   3.305 +qed "gen_Increains_state_of_eq";
   3.306 +bind_thm("Increasing_state_ofD1", 
   3.307 +gen_Increains_state_of_eq RS equalityD1 RS subsetD);
   3.308 +bind_thm("Increasing_state_ofD2", 
   3.309 +gen_Increains_state_of_eq RS equalityD2 RS subsetD);
   3.310 +
   3.311 +Goalw [Follows_def, Increasing_def] 
   3.312 +"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =  \
   3.313 +\ Follows(A, r, f, g)";
   3.314 +by Auto_tac;
   3.315 +qed "Follows_state_of_eq";
   3.316 +bind_thm("Follows_state_ofD1", Follows_state_of_eq RS equalityD1 RS subsetD);
   3.317 +bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
   3.318 +
   3.319 +(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
   3.320 +fun list_of_Int th = 
   3.321 +    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
   3.322 +    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
   3.323 +    handle THM _ => (list_of_Int (th RS InterD))
   3.324 +    handle THM _ => (list_of_Int (th RS bspec))
   3.325 +    handle THM _ => [th];
   3.326 +
   3.327 +(*Used just once, for Alloc_Increasing*)
   3.328 +
   3.329 +fun normalize th = 
   3.330 +     normalize (th RS spec
   3.331 +                handle THM _ => th RS bspec
   3.332 +                handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
   3.333 +     handle THM _ => th;
   3.334 +
   3.335 +Goal "n:nat ==> nat_list_inj(n):list(nat)";
   3.336 +by (induct_tac "n" 1);
   3.337 +by Auto_tac;
   3.338 +qed "nat_list_inj_type";
   3.339 +
   3.340 +Goal "n:nat ==> length(nat_list_inj(n)) = n";
   3.341 +by (induct_tac "n" 1);
   3.342 +by Auto_tac;
   3.343 +qed "length_nat_list_inj";
   3.344 +
   3.345 +Goalw [nat_var_inj_def]
   3.346 +  "(lam x:nat. nat_var_inj(x)):inj(nat, var)";
   3.347 +by (res_inst_tac [("d", "var_inj")] lam_injective 1); 
   3.348 +by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
   3.349 +by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
   3.350 +qed "var_infinite_lemma";
   3.351 +
   3.352 +Goalw [lepoll_def] "nat lepoll var";
   3.353 +by (res_inst_tac [("x", "(lam x:nat. nat_var_inj(x))")] exI 1);
   3.354 +by (rtac var_infinite_lemma 1);
   3.355 +qed "nat_lepoll_var";
   3.356 +
   3.357 +Goalw [Finite_def] "~Finite(var)";
   3.358 +by Auto_tac;
   3.359 +by (dtac eqpoll_imp_lepoll 1);
   3.360 +by (cut_facts_tac [nat_lepoll_var] 1);
   3.361 +by (subgoal_tac "nat lepoll x" 1);
   3.362 +by (blast_tac (claset() addIs [lepoll_trans]) 2);
   3.363 +by (dres_inst_tac [("i", "x"), ("A", "nat")] lepoll_cardinal_le 1);
   3.364 +by Auto_tac;
   3.365 +by (subgoal_tac "Card(nat)" 1);
   3.366 +by (rewrite_goal_tac [Card_def] 1);
   3.367 +by (dtac sym 1);
   3.368 +by Auto_tac;
   3.369 +by (dtac le_imp_subset 1);
   3.370 +by (dtac subsetD 1);
   3.371 +by (auto_tac (claset(), simpset() addsimps [Card_nat]));
   3.372 +by (blast_tac (claset() addEs [mem_irrefl]) 1);
   3.373 +qed "var_not_Finite";
   3.374 +
   3.375 +Goal "~Finite(A) ==> EX x. x:A";
   3.376 +by (etac swap 1);
   3.377 +by Auto_tac;
   3.378 +by (subgoal_tac "A=0" 1);
   3.379 +by (auto_tac (claset(), simpset() addsimps [Finite_0]));
   3.380 +qed "not_Finite_imp_exist";
   3.381 +
   3.382 +Goal "Finite(A) ==> b:(Inter(RepFun(var-A, B))) <-> (ALL x:var-A. b:B(x))";
   3.383 +by (subgoal_tac "EX x. x:var-A" 1);
   3.384 +by Auto_tac;
   3.385 +by (subgoal_tac "~Finite(var-A)" 1);
   3.386 +by (dtac not_Finite_imp_exist 1);
   3.387 +by Auto_tac;
   3.388 +by (cut_facts_tac [var_not_Finite] 1);
   3.389 +by (etac swap  1);
   3.390 +by (res_inst_tac [("B", "A")] Diff_Finite 1);
   3.391 +by Auto_tac;
   3.392 +qed "Inter_Diff_var_iff";
   3.393 +
   3.394 +Goal "[| b:Inter(RepFun(var-A, B)); Finite(A); x:var-A |] ==> b:B(x)";
   3.395 +by (rotate_tac 1 1);
   3.396 +by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
   3.397 +qed "Inter_var_DiffD";
   3.398 +
   3.399 +(* [| Finite(A); (ALL x:var-A. b:B(x)) |] ==> b:Inter(RepFun(var-A, B)) *)
   3.400 +bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
   3.401 +
   3.402 +AddSIs [Inter_var_DiffI];
   3.403 +Addsimps [Finite_0, Finite_cons];
   3.404 +
   3.405 +Goal "Acts(F)<= A Int Pow(state*state)  <-> Acts(F)<=A";
   3.406 +by (cut_facts_tac [inst "F" "F" Acts_type] 1);
   3.407 +by Auto_tac;
   3.408 +qed "Acts_subset_Int_Pow_simp";
   3.409 +Addsimps [Acts_subset_Int_Pow_simp];
   3.410 +
   3.411 +Goal "cons(x, A Int B) = cons(x, A) Int cons(x, B)";
   3.412 +by Auto_tac;
   3.413 +qed "cons_Int_distrib";
   3.414 +
   3.415 +
   3.416 +(* Currently not used, but of potential interest *)
   3.417 +Goal 
   3.418 +"[| Finite(A); ALL x:A. g(x):nat |] ==> \
   3.419 +\ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
   3.420 +by (etac Finite_induct 1);
   3.421 +by (auto_tac (claset(), simpset() addsimps [int_of_add]));
   3.422 +qed "setsum_nsetsum_eq";
   3.423 +
   3.424 +Goal 
   3.425 +"[| A=B;  ALL x:A. f(x)=g(x);  ALL x:A. g(x):nat; \
   3.426 +\     Finite(A) |]  ==> nsetsum(f, A) = nsetsum(g, B)";
   3.427 +by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
   3.428 +by (rtac trans 2);
   3.429 +by (rtac setsum_nsetsum_eq 3);
   3.430 +by (rtac trans 2);
   3.431 +by (rtac (setsum_nsetsum_eq RS sym) 2);
   3.432 +by Auto_tac;
   3.433 +by (rtac setsum_cong 1);
   3.434 +by Auto_tac;
   3.435 +qed "nsetsum_cong";  
   3.436 +
   3.437 +
   3.438 +
   3.439 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/UNITY/AllocBase.thy	Wed May 28 18:13:41 2003 +0200
     4.3 @@ -0,0 +1,72 @@
     4.4 +(*  Title:      ZF/UNITY/AllocBase.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     4.7 +    Copyright   2001  University of Cambridge
     4.8 +
     4.9 +Common declarations for Chandy and Charpentier's Allocator
    4.10 +*)
    4.11 +
    4.12 +AllocBase = Follows + MultisetSum + Guar + New +
    4.13 +
    4.14 +consts
    4.15 +  tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
    4.16 +  NbT      :: i  (* Number of tokens in system *)
    4.17 +  Nclients :: i  (* Number of clients *)
    4.18 +translations
    4.19 +"tokbag" => "nat" 
    4.20 +rules
    4.21 +  NbT_pos  "NbT:nat-{0}"
    4.22 +  Nclients_pos "Nclients:nat-{0}"
    4.23 +  
    4.24 +(*This function merely sums the elements of a list*)
    4.25 +consts tokens     :: i =>i
    4.26 +       item :: i (* Items to be merged/distributed *)
    4.27 +primrec 
    4.28 +  "tokens(Nil) = 0"
    4.29 +  "tokens (Cons(x,xs)) = x #+ tokens(xs)"
    4.30 +
    4.31 +consts
    4.32 +  bag_of :: i => i
    4.33 +
    4.34 +primrec
    4.35 +  "bag_of(Nil)    = 0"
    4.36 +  "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
    4.37 +
    4.38 +(* definitions needed in Client.thy *)
    4.39 +consts
    4.40 +  all_distinct0:: i=>i
    4.41 +  all_distinct:: i=>o
    4.42 +  
    4.43 +primrec
    4.44 +  "all_distinct0(Nil) = 1"
    4.45 +  "all_distinct0(Cons(a, l)) =
    4.46 +     (if a:set_of_list(l) then 0 else all_distinct0(l))"
    4.47 +
    4.48 +defs
    4.49 +all_distinct_def
    4.50 +  "all_distinct(l) == all_distinct0(l)=1"
    4.51 +  
    4.52 +constdefs  
    4.53 +  (* coersion from anyting to state *)
    4.54 +  state_of :: i =>i
    4.55 +  "state_of(s) == if s:state then s else st0"
    4.56 +
    4.57 +  (* simplifies the expression of programs  *)
    4.58 +
    4.59 +  lift :: "i =>(i=>i)"
    4.60 +  "lift(x) == %s. s`x"
    4.61 +
    4.62 +consts (* to show that the set of variables is infinite *)
    4.63 +  nat_list_inj :: i=>i
    4.64 +  nat_var_inj  :: i=>i
    4.65 +  var_inj :: i=>i
    4.66 +defs
    4.67 +  nat_var_inj_def "nat_var_inj(n) == Var(nat_list_inj(n))"
    4.68 +primrec
    4.69 +  "nat_list_inj(0) = Nil"
    4.70 +  "nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
    4.71 +
    4.72 +primrec
    4.73 +  "var_inj(Var(l)) = length(l)"
    4.74 +
    4.75 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/UNITY/Distributor.ML	Wed May 28 18:13:41 2003 +0200
     5.3 @@ -0,0 +1,169 @@
     5.4 +(*  Title: ZF/UNITY/Distributor
     5.5 +    ID:         $Id$
     5.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     5.7 +    Copyright   2002  University of Cambridge
     5.8 +
     5.9 +A multiple-client allocator from a single-client allocator:
    5.10 +Distributor specification
    5.11 +*)
    5.12 +
    5.13 +Open_locale "Distributor";
    5.14 +val all_distinct_vars = thm "all_distinct_vars";
    5.15 +val var_assumes = thm "var_assumes";
    5.16 +val type_assumes = thm "type_assumes";
    5.17 +val default_val_assumes  = thm "default_val_assumes";
    5.18 +
    5.19 +Addsimps [var_assumes, default_val_assumes,  type_assumes];
    5.20 +
    5.21 +Goalw [state_def]
    5.22 +"s:state ==> s`In:list(A)";
    5.23 +by (dres_inst_tac [("a", "In")] apply_type 1);
    5.24 +by Auto_tac;
    5.25 +qed "In_value_type";
    5.26 +AddTCs [In_value_type];
    5.27 +Addsimps [In_value_type];
    5.28 +
    5.29 +Goalw [state_def]
    5.30 +"s:state ==> s`iIn:list(nat)";
    5.31 +by (dres_inst_tac [("a", "iIn")] apply_type 1);
    5.32 +by Auto_tac;
    5.33 +qed "iIn_value_type";
    5.34 +AddTCs [iIn_value_type];
    5.35 +Addsimps [iIn_value_type];
    5.36 +
    5.37 +Goalw [state_def]
    5.38 +"s:state ==> s`Out(n):list(A)";
    5.39 +by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
    5.40 +by Auto_tac;
    5.41 +qed "Out_value_type";
    5.42 +AddTCs [Out_value_type];
    5.43 +Addsimps [Out_value_type];
    5.44 +
    5.45 +val distrib = thm "distr_spec";
    5.46 +
    5.47 +Goal "D:program";
    5.48 +by (cut_facts_tac [distrib] 1);
    5.49 +by (auto_tac (claset(), simpset() addsimps 
    5.50 +           [distr_spec_def, distr_allowed_acts_def]));
    5.51 +qed "D_in_program";
    5.52 +Addsimps [D_in_program];
    5.53 +AddTCs [D_in_program];
    5.54 +
    5.55 +Goal "G:program ==> \
    5.56 +\   D ok G <-> \
    5.57 +\  ((ALL n:nat. G:preserves(lift(Out(n)))) & D:Allowed(G))";
    5.58 +by (cut_facts_tac [distrib] 1);
    5.59 +by (auto_tac (claset(), 
    5.60 +     simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def, 
    5.61 +                         Allowed_def, ok_iff_Allowed]));
    5.62 +by (rotate_tac ~1 2);
    5.63 +by (dres_inst_tac [("x", "G")] bspec 2);
    5.64 +by Auto_tac;
    5.65 +by (dresolve_tac [rotate_prems 1 (safety_prop_Acts_iff RS iffD1)] 1);
    5.66 +by (auto_tac (claset() addIs [safety_prop_Inter], simpset()));
    5.67 +qed "D_ok_iff";
    5.68 +
    5.69 +Goal 
    5.70 +"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
    5.71 +\     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
    5.72 +\     Always({s:state. ALL elt:set_of_list(s`iIn). elt<Nclients})) \
    5.73 +\     guarantees \
    5.74 +\         (INT n: Nclients. lift(Out(n)) IncreasingWrt \
    5.75 +\                           prefix(A)/list(A))";
    5.76 +by (cut_facts_tac [D_in_program, distrib] 1);
    5.77 +by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
    5.78 +by (auto_tac (claset() addSIs [guaranteesI]  addIs [Follows_imp_Increasing_left]
    5.79 +                        addSDs [guaranteesD], 
    5.80 +               simpset() addsimps []));
    5.81 +qed "distr_Increasing_Out";
    5.82 +
    5.83 +val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
    5.84 +
    5.85 +Goal
    5.86 +"[| ALL n:nat. G:preserves(lift(Out(n))); \
    5.87 +\  D Join G:Always({s:state. \
    5.88 +\         ALL elt:set_of_list(s`iIn). elt < Nclients}) |] \
    5.89 +\ ==> D Join G : Always \
    5.90 +\         ({s:state. msetsum(%n. bag_of (sublist(s`In, \
    5.91 +\                      {k:nat. k < length(s`iIn) &\
    5.92 +\                         nth(k, s`iIn)= n})), \
    5.93 +\                        Nclients, A) = \
    5.94 +\             bag_of(sublist(s`In, length(s`iIn)))})";
    5.95 +by (cut_facts_tac [D_in_program] 1);
    5.96 +by (subgoal_tac "G:program" 1);
    5.97 +by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
    5.98 +by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
    5.99 +by Auto_tac;
   5.100 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
   5.101 +by (asm_simp_tac (simpset() addsimps [nat_into_Finite]) 1); 
   5.102 +by (Blast_tac 1); 
   5.103 +by (Asm_simp_tac 1);
   5.104 +by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1); 
   5.105 +by (subgoal_tac
   5.106 +    "(UN i: Nclients. {k:nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
   5.107 +\    length(x`iIn)" 1);
   5.108 +by (Asm_simp_tac 1);
   5.109 +by (resolve_tac [equalityI] 1);
   5.110 +by Safe_tac;
   5.111 +by (asm_full_simp_tac (simpset() addsimps [ltD]) 1);
   5.112 +by (subgoal_tac "length(x ` iIn) : nat" 1);
   5.113 +by Typecheck_tac; 
   5.114 +by (subgoal_tac "xa : nat" 1); 
   5.115 +by (dres_inst_tac [("x", "nth(xa, x`iIn)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec  1);
   5.116 +by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
   5.117 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
   5.118 +by (blast_tac (claset() addDs [ltD]) 1); 
   5.119 +by (blast_tac (claset() addIs [lt_trans]) 1);
   5.120 +qed "distr_bag_Follows_lemma";
   5.121 +
   5.122 +
   5.123 +val prems =
   5.124 +Goal "[|A=A'; r=r'; !!x. x:state ==> f(x)=f'(x); !!x. x:state ==> g(x)=g'(x)|] ==> Follows(A, r, f, g) = Follows(A', r', f', g')";
   5.125 +by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
   5.126 +qed "Follows_cong";
   5.127 +(*????????????????*)
   5.128 +
   5.129 +Goal
   5.130 + "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
   5.131 +\      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
   5.132 +\       Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})) \
   5.133 +\     guarantees  \
   5.134 +\      (INT n: Nclients. \
   5.135 +\       (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A)) \
   5.136 +\       Fols \
   5.137 +\       (%s. bag_of(sublist(s`In, length(s`iIn)))) \
   5.138 +\       Wrt MultLe(A, r)/Mult(A))";
   5.139 +by (cut_facts_tac [distrib] 1);
   5.140 +by (rtac guaranteesI 1);
   5.141 +by (Clarify_tac 1); 
   5.142 +by (Simp_tac 2);
   5.143 +by (rtac (distr_bag_Follows_lemma RS Always_Follows2) 1);
   5.144 +by Auto_tac;  
   5.145 +by (rtac Follows_state_ofD1 2);
   5.146 +by (rtac Follows_msetsum_UN 2);
   5.147 +by (ALLGOALS(Clarify_tac));
   5.148 +by (resolve_tac [conjI] 3);
   5.149 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 3);
   5.150 +by (resolve_tac [conjI] 4);
   5.151 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 4);
   5.152 +by (resolve_tac [conjI] 5);
   5.153 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
   5.154 +by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
   5.155 +by (Clarify_tac 4);
   5.156 +by (asm_full_simp_tac (simpset() addsimps []) 3);
   5.157 +by (asm_full_simp_tac (simpset() addsimps []) 3);
   5.158 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
   5.159 +by (rotate_tac 2 1);
   5.160 +by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
   5.161 +by (auto_tac (claset(), 
   5.162 +              simpset() addsimps [distr_spec_def, distr_follows_def]));
   5.163 +by (dtac guaranteesD 1); 
   5.164 +by (assume_tac 1);
   5.165 +by (force_tac (claset(), simpset() addsimps []) 1); 
   5.166 +by (force_tac (claset(), simpset() addsimps []) 1); 
   5.167 +by (asm_full_simp_tac
   5.168 +    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
   5.169 +             refl_prefix, trans_on_MultLe] 
   5.170 +            addcongs [Follows_cong]) 1); 
   5.171 +qed  "distr_bag_Follows";
   5.172 +Close_locale "Distributor";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/UNITY/Distributor.thy	Wed May 28 18:13:41 2003 +0200
     6.3 @@ -0,0 +1,50 @@
     6.4 +(*  Title: ZF/UNITY/Distributor
     6.5 +    ID:         $Id$
     6.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     6.7 +    Copyright   2002  University of Cambridge
     6.8 +
     6.9 +A multiple-client allocator from a single-client allocator:
    6.10 +Distributor specification
    6.11 +*)
    6.12 +Distributor = AllocBase + Follows +  Guar + GenPrefix +
    6.13 +(** Distributor specification (the number of outputs is Nclients) ***)
    6.14 + (*spec (14)*)
    6.15 +constdefs  
    6.16 +  distr_follows :: [i, i, i, i =>i] =>i
    6.17 +    "distr_follows(A, In, iIn, Out) ==
    6.18 +     (lift(In) IncreasingWrt prefix(A)/list(A)) Int
    6.19 +     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
    6.20 +     Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})
    6.21 +         guarantees
    6.22 +         (INT n: Nclients.
    6.23 +          lift(Out(n))
    6.24 +              Fols
    6.25 +          (%s. sublist(s`In, 
    6.26 +                       {k:nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
    6.27 +	  Wrt prefix(A)/list(A))"
    6.28 +  
    6.29 + distr_allowed_acts :: [i=>i]=>i
    6.30 +  "distr_allowed_acts(Out) ==
    6.31 +   {D:program. AllowedActs(D) =
    6.32 +   cons(id(state), UN G:(INT n:nat. preserves(lift(Out(n)))). Acts(G))}"
    6.33 +
    6.34 +  distr_spec :: [i, i, i, i =>i]=>i
    6.35 +  "distr_spec(A, In, iIn, Out) ==
    6.36 +   distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)"
    6.37 +
    6.38 +locale Distributor =
    6.39 +  fixes In :: i  (*items to distribute*)
    6.40 +        iIn :: i (*destinations of items to distribute*)
    6.41 +        Out :: i=>i  (*distributed items*)
    6.42 +        A :: i   (*the type of items being distributed *)
    6.43 +        D :: i
    6.44 + assumes
    6.45 +    var_assumes       "In:var & iIn:var & (ALL n. Out(n):var)"
    6.46 +    all_distinct_vars "ALL n. all_distinct([In, iIn, iOut(n)])"
    6.47 +    type_assumes      "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
    6.48 +                       (ALL n. type_of(Out(n))=list(A))"
    6.49 +   default_val_assumes "default_val(In)=Nil &
    6.50 +                        default_val(iIn)=Nil &
    6.51 +                        (ALL n. default_val(Out(n))=Nil)"
    6.52 +   distr_spec  "D:distr_spec(A, In, iIn, Out)"
    6.53 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/UNITY/Follows.ML	Wed May 28 18:13:41 2003 +0200
     7.3 @@ -0,0 +1,510 @@
     7.4 +(*  Title:      ZF/UNITY/Follows
     7.5 +    ID:         $Id$
     7.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     7.7 +    Copyright   2001  University of Cambridge
     7.8 + 
     7.9 +The Follows relation of Charpentier and Sivilotte
    7.10 +*)
    7.11 + 
    7.12 +(*Does this hold for "invariant"?*)
    7.13 +
    7.14 +
    7.15 +Goalw [mono1_def, comp_def] 
    7.16 +"[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
    7.17 +\  Always({x:state. <f(x), g(x)>:r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
    7.18 +by (auto_tac (claset(), simpset() addsimps 
    7.19 +         [Always_eq_includes_reachable]));
    7.20 +qed "subset_Always_comp";
    7.21 +
    7.22 +Goal 
    7.23 +"[| F:Always({x:state. <f(x), g(x)>:r}); \
    7.24 +\   mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
    7.25 +\   F:Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
    7.26 +by (blast_tac (claset() addIs [subset_Always_comp RS subsetD]) 1);
    7.27 +qed "imp_Always_comp";
    7.28 +
    7.29 +Goal 
    7.30 +"[| F:Always({x:state. <f1(x), f(x)>:r});  \
    7.31 +\   F:Always({x:state. <g1(x), g(x)>:s}); \
    7.32 +\   mono2(A, r, B, s, C, t, h); \
    7.33 +\   ALL x:state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \
    7.34 +\ ==> F:Always({x:state. <h(f1(x), g1(x)), h(f(x), g(x))>:t})";
    7.35 +by (auto_tac (claset(), simpset() addsimps 
    7.36 +         [Always_eq_includes_reachable, mono2_def]));
    7.37 +by (auto_tac (claset() addSDs [subsetD], simpset()));
    7.38 +qed "imp_Always_comp2";
    7.39 +
    7.40 +(* comp LeadsTo *)
    7.41 +
    7.42 +Goalw [mono1_def, comp_def]
    7.43 +"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
    7.44 +\       ALL x:state. f(x):A & g(x):A |] ==> \
    7.45 +\ (INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}) <= \
    7.46 +\(INT k:B. {x:state. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
    7.47 +by (Clarify_tac 1);
    7.48 +by (ALLGOALS(full_simp_tac (simpset() addsimps [INT_iff])));
    7.49 +by Auto_tac;
    7.50 +by (rtac single_LeadsTo_I 1);
    7.51 +by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]) 2);
    7.52 +by Auto_tac;
    7.53 +by (rotate_tac 5 1);
    7.54 +by (dres_inst_tac [("x", "g(sa)")] bspec 1);
    7.55 +by (etac LeadsTo_weaken 2);
    7.56 +by (auto_tac (claset(), simpset() addsimps [part_order_def, refl_def]));
    7.57 +by (res_inst_tac [("b", "h(g(sa))")] trans_onD 1);
    7.58 +by (Blast_tac 1);
    7.59 +by Auto_tac;
    7.60 +qed "subset_LeadsTo_comp";
    7.61 +
    7.62 +Goal
    7.63 +"[| F:(INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}); \
    7.64 +\   mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
    7.65 +\   ALL x:state. f(x):A & g(x):A |] ==> \
    7.66 +\  F:(INT k:B. {x:state. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
    7.67 +by (rtac (subset_LeadsTo_comp RS subsetD) 1);
    7.68 +by Auto_tac;
    7.69 +qed "imp_LeadsTo_comp";
    7.70 +
    7.71 +Goalw [mono2_def, Increasing_def]
    7.72 +"[| F:Increasing(B, s, g); \
    7.73 +\ ALL j:A. F: {s:state. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
    7.74 +\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t); \
    7.75 +\ ALL x:state. f1(x):A & f(x):A & g(x):B; k:C |] ==> \
    7.76 +\ F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g(x))>:t}";
    7.77 +by (rtac single_LeadsTo_I 1);
    7.78 +by Auto_tac;
    7.79 +by (dres_inst_tac [("x", "g(sa)"), ("A","B")] bspec 1);
    7.80 +by Auto_tac;
    7.81 +by (dres_inst_tac [("x", "f(sa)"),("P","%j. F \\<in> ?X(j) \\<longmapsto>w ?Y(j)")] bspec 1);
    7.82 +by Auto_tac;
    7.83 +by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
    7.84 +by (Blast_tac 1);
    7.85 +by (Blast_tac 1);
    7.86 +by Auto_tac;
    7.87 +by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
    7.88 +by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
    7.89 +by (dres_inst_tac [("x", "f1(x)"), ("x1", "f(sa)"), 
    7.90 +                   ("P2", "%x y. \\<forall>u\\<in>B. ?P(x,y,u)")] (bspec RS bspec) 1);
    7.91 +by (dres_inst_tac [("x", "g(x)"), ("x1", "g(sa)"), 
    7.92 +                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
    7.93 +by Auto_tac;
    7.94 +by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
    7.95 +by (auto_tac (claset(), simpset() addsimps [part_order_def]));
    7.96 +qed "imp_LeadsTo_comp_right";
    7.97 +
    7.98 +Goalw [mono2_def, Increasing_def]
    7.99 +"[| F:Increasing(A, r, f); \
   7.100 +\ ALL j:B. F: {x:state. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
   7.101 +\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
   7.102 +\ ALL x:state. f(x):A & g1(x):B & g(x):B; k:C |] ==> \
   7.103 +\ F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f(x), g1(x))>:t}";
   7.104 +by (rtac single_LeadsTo_I 1);
   7.105 +by Auto_tac;
   7.106 +by (dres_inst_tac [("x", "f(sa)"),("P","%k. F \\<in> Stable(?X(k))")] bspec 1);
   7.107 +by Auto_tac;
   7.108 +by (dres_inst_tac [("x", "g(sa)")] bspec 1);
   7.109 +by Auto_tac;
   7.110 +by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
   7.111 +by (Blast_tac 1);
   7.112 +by (Blast_tac 1);
   7.113 +by Auto_tac;
   7.114 +by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
   7.115 +by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
   7.116 +by (dres_inst_tac [("x", "f(x)"), ("x1", "f(sa)")] (bspec RS bspec) 1);
   7.117 +by (dres_inst_tac [("x", "g1(x)"), ("x1", "g(sa)"), 
   7.118 +                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
   7.119 +by Auto_tac;
   7.120 +by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
   7.121 +by (auto_tac (claset(), simpset() addsimps [part_order_def]));
   7.122 +qed "imp_LeadsTo_comp_left";
   7.123 +
   7.124 +(**  This general result is used to prove Follows Un, munion, etc. **)
   7.125 +Goal
   7.126 +"[| F:Increasing(A, r, f1) Int  Increasing(B, s, g); \
   7.127 +\ ALL j:A. F: {s:state. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
   7.128 +\ ALL j:B. F: {x:state. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
   7.129 +\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
   7.130 +\ ALL x:state. f(x):A & g1(x):B & f1(x):A &g(x):B; k:C |]\
   7.131 +\ ==> F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g1(x))>:t}";
   7.132 +by (res_inst_tac [("B", "{x:state. <k, h(f1(x), g(x))>:t}")] LeadsTo_Trans 1);
   7.133 +by (blast_tac (claset() addIs [imp_LeadsTo_comp_right]) 1);
   7.134 +by (blast_tac (claset() addIs [imp_LeadsTo_comp_left]) 1);
   7.135 +qed "imp_LeadsTo_comp2";
   7.136 +
   7.137 +(* Follows type *)
   7.138 +Goalw [Follows_def] "Follows(A, r, f, g)<=program";
   7.139 +by (blast_tac (claset() addDs [Increasing_type RS subsetD]) 1);
   7.140 +qed "Follows_type";
   7.141 +
   7.142 +Goal "F:Follows(A, r, f, g) ==> F:program";
   7.143 +by (blast_tac (claset() addDs [Follows_type RS subsetD]) 1);
   7.144 +qed "Follows_into_program";
   7.145 +AddTCs [Follows_into_program];
   7.146 +
   7.147 +Goalw [Follows_def] 
   7.148 +"F:Follows(A, r, f, g)==> \
   7.149 +\ F:program & (EX a. a:A) & (ALL x:state. f(x):A & g(x):A)";
   7.150 +by (blast_tac (claset() addDs [IncreasingD]) 1);
   7.151 +qed "FollowsD";
   7.152 +
   7.153 +Goalw [Follows_def]
   7.154 + "[| F:program; c:A; refl(A, r) |] ==> F:Follows(A, r, %x. c, %x. c)";
   7.155 +by Auto_tac;
   7.156 +by (auto_tac (claset(), simpset() addsimps [refl_def]));
   7.157 +qed "Follows_constantI";
   7.158 +
   7.159 +Goalw [Follows_def] 
   7.160 +"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
   7.161 +\  ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)";
   7.162 +by (Clarify_tac 1);
   7.163 +by (forw_inst_tac [("f", "g")] IncreasingD 1);
   7.164 +by (forw_inst_tac [("f", "f")] IncreasingD 1);
   7.165 +by (rtac IntI 1);
   7.166 +by (res_inst_tac [("h", "h")] imp_LeadsTo_comp 2);
   7.167 +by (assume_tac 5);
   7.168 +by (auto_tac (claset() addIs  [imp_Increasing_comp, imp_Always_comp], 
   7.169 +             simpset() delsimps INT_simps));
   7.170 +qed "subset_Follows_comp";
   7.171 +
   7.172 +Goal
   7.173 +"[| F:Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
   7.174 +\ ==>  F:Follows(B, s,  h comp f, h comp g)";
   7.175 +by (blast_tac (claset() addIs [subset_Follows_comp RS subsetD]) 1);
   7.176 +qed "imp_Follows_comp";
   7.177 +
   7.178 +(* 2-place monotone operation: this general result is used to prove Follows_Un, Follows_munion *)
   7.179 +
   7.180 +(* 2-place monotone operation: this general result is 
   7.181 +   used to prove Follows_Un, Follows_munion *)
   7.182 +Goalw [Follows_def] 
   7.183 +"[| F:Follows(A, r, f1, f);  F:Follows(B, s, g1, g); \
   7.184 +\  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |] \
   7.185 +\  ==> F:Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))";
   7.186 +by (Clarify_tac 1);
   7.187 +by (forw_inst_tac [("f", "g")] IncreasingD 1);
   7.188 +by (forw_inst_tac [("f", "f")] IncreasingD 1);
   7.189 +by (rtac IntI 1);
   7.190 +by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 2);
   7.191 +by Safe_tac;
   7.192 +by (res_inst_tac [("h", "h")] imp_Always_comp2 3);
   7.193 +by (assume_tac 5);
   7.194 +by (res_inst_tac [("h", "h")] imp_Increasing_comp2 2);
   7.195 +by (assume_tac 4);
   7.196 +by (res_inst_tac [("h", "h")] imp_Increasing_comp2 1);
   7.197 +by (assume_tac 3);
   7.198 +by (TRYALL(assume_tac));
   7.199 +by (ALLGOALS(Asm_full_simp_tac)); 
   7.200 +by (blast_tac (claset() addSDs [IncreasingD]) 1);
   7.201 +by (res_inst_tac [("h", "h")] imp_LeadsTo_comp2 1);
   7.202 +by (assume_tac 4);
   7.203 +by Auto_tac;
   7.204 +by (rewrite_goal_tac [mono2_def] 3);
   7.205 +by (REPEAT(blast_tac (claset() addDs [IncreasingD]) 1));
   7.206 +qed "imp_Follows_comp2";
   7.207 +
   7.208 +Goal "[| F : Follows(A, r, f, g);  F: Follows(A,r, g, h); \
   7.209 +\        trans[A](r) |] ==> F : Follows(A, r, f, h)";
   7.210 +by (forw_inst_tac [("f", "f")] FollowsD 1);
   7.211 +by (forw_inst_tac [("f", "g")] FollowsD 1);
   7.212 +by (rewrite_goal_tac [Follows_def] 1);
   7.213 +by (asm_full_simp_tac (simpset() 
   7.214 +                 addsimps [Always_eq_includes_reachable, INT_iff]) 1);
   7.215 +by Auto_tac;
   7.216 +by (res_inst_tac [("B", "{s:state. <k, g(s)>:r}")] LeadsTo_Trans 2);
   7.217 +by (res_inst_tac [("b", "g(x)")] trans_onD 1);
   7.218 +by (REPEAT(Blast_tac 1));
   7.219 +qed "Follows_trans";
   7.220 +
   7.221 +(** Destruction rules for Follows **)
   7.222 +
   7.223 +Goalw [Follows_def]
   7.224 +     "F : Follows(A, r, f,g) ==> F:Increasing(A, r, f)";
   7.225 +by (Blast_tac 1);
   7.226 +qed "Follows_imp_Increasing_left";
   7.227 +
   7.228 +Goalw [Follows_def]
   7.229 +     "F : Follows(A, r, f,g) ==> F:Increasing(A, r, g)";
   7.230 +by (Blast_tac 1);
   7.231 +qed "Follows_imp_Increasing_right";
   7.232 +
   7.233 +Goalw [Follows_def]
   7.234 + "F :Follows(A, r, f, g) ==> F:Always({s:state. <f(s),g(s)>:r})";
   7.235 +by (Blast_tac 1);
   7.236 +qed "Follows_imp_Always";
   7.237 +
   7.238 +Goalw [Follows_def]
   7.239 + "[| F:Follows(A, r, f, g); k:A |]  ==> \
   7.240 +\ F: {s:state. <k,g(s)>:r } LeadsTo {s:state. <k,f(s)>:r}";
   7.241 +by (Blast_tac 1);
   7.242 +qed "Follows_imp_LeadsTo";
   7.243 +
   7.244 +Goal "[| F : Follows(list(nat), gen_prefix(nat, Le), f, g); k:list(nat) |] \
   7.245 +\  ==> F : {s:state. k pfixLe g(s)} LeadsTo {s:state. k pfixLe f(s)}";
   7.246 +by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
   7.247 +qed "Follows_LeadsTo_pfixLe";
   7.248 +
   7.249 +Goal "[| F : Follows(list(nat), gen_prefix(nat, Ge), f, g); k:list(nat) |] \
   7.250 +\  ==> F : {s:state. k pfixGe g(s)} LeadsTo {s:state. k pfixGe f(s)}";
   7.251 +by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
   7.252 +qed "Follows_LeadsTo_pfixGe";
   7.253 +
   7.254 +Goalw  [Follows_def, Increasing_def, Stable_def]
   7.255 +"[| F:Always({s:state. f(s) = g(s)}); F:Follows(A, r, f, h);  \
   7.256 +\   ALL x:state. g(x):A |] ==> F : Follows(A, r, g, h)";
   7.257 +by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
   7.258 +by Auto_tac;
   7.259 +by (res_inst_tac [("C", "{s:state. f(s)=g(s)}"),
   7.260 +                 ("A", "{s:state. <ka, h(s)>:r}"),
   7.261 +                 ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
   7.262 +by (eres_inst_tac [("A", "{s:state. <ka,f(s)>:r}"), 
   7.263 +                   ("A'", "{s:state. <ka,f(s)>:r}")] 
   7.264 +                  Always_Constrains_weaken 1);
   7.265 +by Auto_tac;
   7.266 +by (dtac Always_Int_I 1);
   7.267 +by (assume_tac 1);
   7.268 +by (eres_inst_tac [("A","{s \\<in> state . f(s) = g(s)} \\<inter> {s \\<in> state . \\<langle>f(s), h(s)\\<rangle> \\<in> r}")] Always_weaken 1); 
   7.269 +by Auto_tac;
   7.270 +qed "Always_Follows1";
   7.271 +
   7.272 +Goalw [Follows_def, Increasing_def, Stable_def]
   7.273 +"[| F : Always({s:state. g(s) = h(s)}); \
   7.274 +\ F: Follows(A, r, f, g); ALL x:state. h(x):A |] ==> F : Follows(A, r, f, h)";
   7.275 +by (full_simp_tac (simpset() addsimps [INT_iff]) 1);
   7.276 +by Auto_tac;
   7.277 +by (thin_tac "k:A" 3);
   7.278 +by (res_inst_tac [("C", "{s:state. g(s)=h(s)}"),
   7.279 +                  ("A", "{s:state. <ka, g(s)>:r}"),
   7.280 +                  ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
   7.281 +by (eres_inst_tac [("A", "{s:state. <ka, g(s)>:r}"), 
   7.282 +                   ("A'", "{s:state. <ka, g(s)>:r}")] 
   7.283 +                  Always_Constrains_weaken 1);
   7.284 +by Auto_tac;
   7.285 +by (dtac Always_Int_I 1);
   7.286 +by (assume_tac 1);
   7.287 +by (eres_inst_tac [("A","{s \\<in> state . g(s) = h(s)} \\<inter> {s \\<in> state . \\<langle>f(s), g(s)\\<rangle> \\<in> r}")] Always_weaken 1); 
   7.288 +by Auto_tac;
   7.289 +qed "Always_Follows2";
   7.290 +
   7.291 +(** Union properties (with the subset ordering) **)
   7.292 +
   7.293 +Goalw [refl_def, SetLe_def] "refl(Pow(A), SetLe(A))";
   7.294 +by Auto_tac;
   7.295 +qed "refl_SetLe";
   7.296 +Addsimps [refl_SetLe];
   7.297 +
   7.298 +Goalw [trans_on_def, SetLe_def] "trans[Pow(A)](SetLe(A))";
   7.299 +by Auto_tac;
   7.300 +qed "trans_on_SetLe";
   7.301 +Addsimps [trans_on_SetLe];
   7.302 +
   7.303 +Goalw [antisym_def, SetLe_def] "antisym(SetLe(A))";
   7.304 +by Auto_tac;
   7.305 +qed "antisym_SetLe";
   7.306 +Addsimps [antisym_SetLe];
   7.307 +
   7.308 +Goalw [part_order_def] "part_order(Pow(A), SetLe(A))";
   7.309 +by Auto_tac;
   7.310 +qed "part_order_SetLe";
   7.311 +Addsimps [part_order_SetLe];
   7.312 +
   7.313 +Goal "[| F: Increasing.increasing(Pow(A), SetLe(A), f);  \
   7.314 +\        F: Increasing.increasing(Pow(A), SetLe(A), g) |] \
   7.315 +\    ==> F : Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
   7.316 +by (res_inst_tac [("h", "op Un")] imp_increasing_comp2 1);
   7.317 +by Auto_tac;
   7.318 +qed "increasing_Un";
   7.319 +
   7.320 +Goal "[| F: Increasing(Pow(A), SetLe(A), f);  \
   7.321 +\        F: Increasing(Pow(A), SetLe(A), g) |] \
   7.322 +\    ==> F : Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
   7.323 +by (res_inst_tac [("h", "op Un")] imp_Increasing_comp2 1);
   7.324 +by Auto_tac;
   7.325 +qed "Increasing_Un";
   7.326 +
   7.327 +Goal "[| F:Always({s:state. f1(s) <= f(s)}); \
   7.328 +\    F : Always({s:state. g1(s) <= g(s)}) |] \
   7.329 +\     ==> F : Always({s:state. f1(s) Un g1(s) <= f(s) Un g(s)})";
   7.330 +by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
   7.331 +by (Blast_tac 1);
   7.332 +qed "Always_Un";
   7.333 +
   7.334 +Goal
   7.335 +"[| F:Follows(Pow(A), SetLe(A), f1, f); \
   7.336 +\    F:Follows(Pow(A), SetLe(A), g1, g) |] \
   7.337 +\    ==> F:Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))";
   7.338 +by (res_inst_tac [("h", "op Un")] imp_Follows_comp2 1);
   7.339 +by Auto_tac;
   7.340 +qed "Follows_Un";
   7.341 +
   7.342 +(** Multiset union properties (with the MultLe ordering) **)
   7.343 +
   7.344 +Goalw [MultLe_def, refl_def] "refl(Mult(A), MultLe(A,r))";
   7.345 +by Auto_tac;
   7.346 +qed "refl_MultLe";
   7.347 +Addsimps [refl_MultLe];
   7.348 +
   7.349 +Goalw [MultLe_def, id_def, lam_def]
   7.350 + "[| multiset(M); mset_of(M)<=A |] ==> <M, M>:MultLe(A, r)";
   7.351 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   7.352 +qed "MultLe_refl1";
   7.353 +Addsimps [MultLe_refl1];
   7.354 +
   7.355 +Goalw [MultLe_def, id_def, lam_def]
   7.356 + "M:Mult(A) ==> <M, M>:MultLe(A, r)";
   7.357 +by Auto_tac;
   7.358 +qed "MultLe_refl2";
   7.359 +Addsimps [MultLe_refl2];
   7.360 +
   7.361 +Goalw [MultLe_def, trans_on_def] "trans[Mult(A)](MultLe(A,r))";
   7.362 +by (auto_tac (claset() addIs [trancl_trans], simpset() addsimps [multirel_def]));
   7.363 +qed "trans_on_MultLe";
   7.364 +Addsimps [trans_on_MultLe];
   7.365 +
   7.366 +Goalw [MultLe_def] "MultLe(A, r)<= (Mult(A) * Mult(A))";
   7.367 +by Auto_tac;
   7.368 +by (dtac (multirel_type RS subsetD) 1);
   7.369 +by Auto_tac;
   7.370 +qed "MultLe_type";
   7.371 +
   7.372 +Goal "[| <M, K>:MultLe(A, r); <K, N>:MultLe(A, r) |] ==> <M, N>:MultLe(A,r)";
   7.373 +by (cut_facts_tac [inst "A" "A" trans_on_MultLe] 1);
   7.374 +by (dtac trans_onD 1);
   7.375 +by (assume_tac 1);
   7.376 +by (auto_tac (claset() addDs [MultLe_type RS subsetD], simpset()));
   7.377 +qed "MultLe_trans";
   7.378 +
   7.379 +Goalw [part_order_def, part_ord_def]
   7.380 +"part_order(A, r) ==> part_ord(A, r-id(A))";
   7.381 +by (rewrite_goal_tac [refl_def, id_def, lam_def, irrefl_def] 1);
   7.382 +by Auto_tac;
   7.383 +by (simp_tac (simpset() addsimps [trans_on_def]) 1);
   7.384 +by Auto_tac;
   7.385 +by (blast_tac (claset() addDs [trans_onD]) 1);
   7.386 +by (full_simp_tac (simpset() addsimps [antisym_def]) 1);
   7.387 +by Auto_tac;
   7.388 +qed "part_order_imp_part_ord";
   7.389 +
   7.390 +Goalw [MultLe_def, antisym_def]
   7.391 +  "part_order(A, r) ==> antisym(MultLe(A,r))";
   7.392 +by (dtac part_order_imp_part_ord 1);
   7.393 +by Auto_tac;
   7.394 +by (dtac irrefl_on_multirel 1);
   7.395 +by (forward_tac [multirel_type RS subsetD] 1);
   7.396 +by (dtac multirel_trans 1);
   7.397 +by (auto_tac (claset(), simpset() addsimps [irrefl_def]));
   7.398 +qed "antisym_MultLe";
   7.399 +Addsimps [antisym_MultLe];
   7.400 +
   7.401 +Goal  "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))";
   7.402 +by (ftac antisym_MultLe 1);
   7.403 +by (auto_tac (claset(), simpset() addsimps [part_order_def]));
   7.404 +qed "part_order_MultLe";
   7.405 +Addsimps [part_order_MultLe];
   7.406 +
   7.407 +Goalw [MultLe_def]
   7.408 +"[| multiset(M); mset_of(M)<= A|] ==> <0, M>:MultLe(A, r)";
   7.409 +by (case_tac "M=0" 1);
   7.410 +by (auto_tac (claset(), simpset() addsimps (thms"FiniteFun.intros")));
   7.411 +by (subgoal_tac "<0 +# 0, 0 +# M>:multirel(A, r - id(A))" 1);
   7.412 +by (rtac one_step_implies_multirel 2);
   7.413 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   7.414 +qed "empty_le_MultLe";
   7.415 +Addsimps [empty_le_MultLe];
   7.416 +
   7.417 +Goal "M:Mult(A) ==> <0, M>:MultLe(A, r)";
   7.418 +by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
   7.419 +qed "empty_le_MultLe2";
   7.420 +Addsimps [empty_le_MultLe2];
   7.421 +
   7.422 +Goalw [MultLe_def] 
   7.423 +"[| <M, N>:MultLe(A, r); <K, L>:MultLe(A, r) |] ==>\
   7.424 +\ <M +# K, N +# L>:MultLe(A, r)";
   7.425 +by (auto_tac (claset() addIs [munion_multirel_mono1, 
   7.426 +                              munion_multirel_mono2,
   7.427 +                              munion_multirel_mono,
   7.428 +                              multiset_into_Mult], 
   7.429 +               simpset() addsimps [Mult_iff_multiset]));
   7.430 +qed "munion_mono";
   7.431 +
   7.432 +Goal "[| F:Increasing.increasing(Mult(A), MultLe(A,r), f);  \
   7.433 +\        F:Increasing.increasing(Mult(A), MultLe(A,r), g) |] \
   7.434 +\    ==> F : Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
   7.435 +by (res_inst_tac [("h", "munion")] imp_increasing_comp2 1);
   7.436 +by Auto_tac;
   7.437 +qed "increasing_munion";
   7.438 +
   7.439 +Goal "[| F:Increasing(Mult(A), MultLe(A,r), f);  \
   7.440 +\        F:Increasing(Mult(A), MultLe(A,r), g)|] \
   7.441 +\    ==> F : Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
   7.442 +by (res_inst_tac [("h", "munion")] imp_Increasing_comp2 1);
   7.443 +by Auto_tac;
   7.444 +qed "Increasing_munion";
   7.445 +
   7.446 +Goal
   7.447 +"[| F:Always({s:state. <f1(s),f(s)>:MultLe(A,r)}); \
   7.448 +\         F:Always({s:state. <g1(s), g(s)>:MultLe(A,r)});\
   7.449 +\ ALL x:state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \
   7.450 +\     ==> F : Always({s:state. <f1(s) +# g1(s), f(s) +# g(s)>:MultLe(A,r)})";
   7.451 +by (res_inst_tac [("h", "munion")] imp_Always_comp2 1);
   7.452 +by (ALLGOALS(Asm_full_simp_tac));
   7.453 +by (blast_tac (claset() addIs [munion_mono]) 1);
   7.454 +by (ALLGOALS(Asm_full_simp_tac));
   7.455 +qed "Always_munion";
   7.456 +
   7.457 +Goal
   7.458 +"[| F:Follows(Mult(A), MultLe(A, r), f1, f); \
   7.459 +\   F:Follows(Mult(A), MultLe(A, r), g1, g) |] \
   7.460 +\ ==> F:Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))";
   7.461 +by (res_inst_tac [("h", "munion")] imp_Follows_comp2 1);
   7.462 +by Auto_tac;
   7.463 +qed "Follows_munion";
   7.464 +
   7.465 +(** Used in ClientImp **)
   7.466 +
   7.467 +Goal 
   7.468 +"!!f. [| ALL i:I. F : Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \
   7.469 +\ ALL s. ALL i:I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & \
   7.470 +\                       multiset(f(i, s)) & mset_of(f(i, s))<=A ; \
   7.471 +\  Finite(I); F:program |] \
   7.472 +\       ==> F : Follows(Mult(A), \
   7.473 +\                       MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A), \
   7.474 +\                                     %x. msetsum(%i. f(i,  x), I, A))";
   7.475 +by (etac rev_mp 1);
   7.476 +by (dtac Finite_into_Fin 1);
   7.477 +by (etac Fin_induct 1);
   7.478 +by (Asm_simp_tac 1);
   7.479 +by (rtac Follows_constantI 1);
   7.480 +by (ALLGOALS(asm_simp_tac (simpset() addsimps  (thms"FiniteFun.intros"))));
   7.481 +by Auto_tac;
   7.482 +by (resolve_tac [Follows_munion] 1);
   7.483 +by Auto_tac;
   7.484 +qed "Follows_msetsum_UN";
   7.485 +
   7.486 +Goalw [refl_def, Le_def] "refl(nat, Le)";
   7.487 +by Auto_tac;
   7.488 +qed "refl_Le";
   7.489 +Addsimps [refl_Le];
   7.490 +
   7.491 +Goalw [trans_on_def, Le_def] "trans[nat](Le)";
   7.492 +by Auto_tac;
   7.493 +by (blast_tac (claset() addIs [le_trans]) 1);
   7.494 +qed "trans_on_Le";
   7.495 +Addsimps [trans_on_Le];
   7.496 +
   7.497 +Goalw [trans_def, Le_def] "trans(Le)";
   7.498 +by Auto_tac;
   7.499 +by (blast_tac (claset() addIs [le_trans]) 1);
   7.500 +qed "trans_Le";
   7.501 +Addsimps [trans_Le];
   7.502 +
   7.503 +Goalw [antisym_def, Le_def] "antisym(Le)";
   7.504 +by Auto_tac;
   7.505 +by (dtac le_imp_not_lt 1);
   7.506 +by (auto_tac (claset(), simpset() addsimps [le_iff]));
   7.507 +qed "antisym_Le";
   7.508 +Addsimps [antisym_Le];
   7.509 +
   7.510 +Goalw [part_order_def] "part_order(nat, Le)";
   7.511 +by Auto_tac;
   7.512 +qed "part_order_Le";
   7.513 +Addsimps [part_order_Le];
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/UNITY/Follows.thy	Wed May 28 18:13:41 2003 +0200
     8.3 @@ -0,0 +1,40 @@
     8.4 +(*  Title:      ZF/UNITY/Follows
     8.5 +    ID:         $Id$
     8.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     8.7 +    Copyright   2002  University of Cambridge
     8.8 +
     8.9 +The "Follows" relation of Charpentier and Sivilotte
    8.10 +
    8.11 +Theory ported from HOL.
    8.12 +*)
    8.13 +
    8.14 +Follows = SubstAx + Increasing +
    8.15 +constdefs
    8.16 +  Follows :: "[i, i, i=>i, i=>i] => i"
    8.17 +  "Follows(A, r, f, g) == 
    8.18 +            Increasing(A, r, g) Int
    8.19 +            Increasing(A, r,f) Int
    8.20 +            Always({s:state. <f(s), g(s)>:r}) Int
    8.21 +           (INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"
    8.22 +consts
    8.23 +  Incr :: [i=>i]=>i   
    8.24 +  n_Incr :: [i=>i]=>i
    8.25 +  m_Incr :: [i=>i]=>i
    8.26 +  s_Incr :: [i=>i]=>i
    8.27 +  n_Fols :: [i=>i, i=>i]=>i   (infixl "n'_Fols" 65)
    8.28 +
    8.29 +syntax
    8.30 +  Follows' :: "[i=>i, i=>i, i, i] => i"
    8.31 +        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)
    8.32 +
    8.33 +  
    8.34 +translations
    8.35 +  "Incr(f)" == "Increasing(list(nat), prefix(nat), f)"
    8.36 +  "n_Incr(f)" == "Increasing(nat, Le, f)"
    8.37 +  "s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"
    8.38 +  "m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"
    8.39 +  
    8.40 +  "f n_Fols g" == "Follows(nat, Le, f, g)"
    8.41 +
    8.42 +  "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
    8.43 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/ZF/UNITY/Increasing.ML	Wed May 28 18:13:41 2003 +0200
     9.3 @@ -0,0 +1,229 @@
     9.4 +(*  Title:      ZF/UNITY/GenIncreasing
     9.5 +    ID:         $Id$
     9.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     9.7 +    Copyright   1998  University of Cambridge
     9.8 +
     9.9 +A general form of the `Increasing' relation of Charpentier
    9.10 +*)
    9.11 +
    9.12 +(** increasing **)
    9.13 +
    9.14 +Goalw [increasing_def] "increasing[A](r, f) <= program";
    9.15 +by (Blast_tac 1);
    9.16 +qed "increasing_type";
    9.17 +
    9.18 +Goalw [increasing_def] "F:increasing[A](r, f) ==> F:program";
    9.19 +by (Blast_tac 1);
    9.20 +qed "increasing_into_program";
    9.21 +
    9.22 +Goalw [increasing_def]
    9.23 +"[| F:increasing[A](r, f); x:A |] ==>F:stable({s:state. <x, f(s)>:r})";
    9.24 +by (Blast_tac 1);
    9.25 +qed "increasing_imp_stable";
    9.26 +
    9.27 +Goalw [increasing_def]
    9.28 +"F:increasing[A](r,f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)";
    9.29 +by (subgoal_tac "EX x. x:state" 1);
    9.30 +by (auto_tac (claset() addDs [stable_type RS subsetD]
    9.31 +                       addIs [st0_in_state], simpset()));
    9.32 +qed "increasingD";
    9.33 +
    9.34 +Goalw [increasing_def, stable_def]
    9.35 + "F:increasing[A](r, %s. c) <-> F:program & c:A";
    9.36 +by (subgoal_tac "EX x. x:state" 1);
    9.37 +by (auto_tac (claset() addDs [stable_type RS subsetD]
    9.38 +                       addIs [st0_in_state], simpset()));
    9.39 +qed "increasing_constant";
    9.40 +Addsimps [increasing_constant];
    9.41 +
    9.42 +Goalw [increasing_def, stable_def, part_order_def, 
    9.43 +       constrains_def, mono1_def, comp_def]
    9.44 +"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==> \
    9.45 +\  increasing[A](r, f) <= increasing[B](s, g comp f)";
    9.46 +by (Clarify_tac 1);
    9.47 +by (Asm_full_simp_tac 1);
    9.48 +by (Clarify_tac 1);
    9.49 +by (subgoal_tac "xa:state" 1);
    9.50 +by (blast_tac (claset() addSDs [ActsD]) 2);
    9.51 +by (subgoal_tac "<f(xb), f(xb)>:r" 1);
    9.52 +by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
    9.53 +by (rotate_tac 5 1);
    9.54 +by (dres_inst_tac [("x", "f(xb)")] bspec 1);
    9.55 +by (rotate_tac ~1 2);
    9.56 +by (dres_inst_tac [("x", "act")] bspec 2);
    9.57 +by (ALLGOALS(Asm_full_simp_tac));
    9.58 +by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
    9.59 +by (Blast_tac 1);
    9.60 +by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
    9.61 +by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
    9.62 +by (ALLGOALS(Asm_simp_tac));
    9.63 +qed "subset_increasing_comp";
    9.64 +
    9.65 +Goal "[| F:increasing[A](r, f); mono1(A, r, B, s, g); \
    9.66 +\        refl(A, r); trans[B](s) |] ==> F:increasing[B](s, g comp f)";
    9.67 +by (rtac (subset_increasing_comp RS subsetD) 1);
    9.68 +by Auto_tac;
    9.69 +qed "imp_increasing_comp";
    9.70 +
    9.71 +Goalw [increasing_def, Le_def, Lt_def]
    9.72 +   "increasing[nat](Le, f) <= increasing[nat](Lt, f)";
    9.73 +by Auto_tac;
    9.74 +qed "strict_increasing";
    9.75 +
    9.76 +Goalw [increasing_def, Gt_def, Ge_def]
    9.77 +   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)";
    9.78 +by Auto_tac;
    9.79 +by (etac natE 1);
    9.80 +by (auto_tac (claset(), simpset() addsimps [stable_def]));
    9.81 +qed "strict_gt_increasing";
    9.82 +
    9.83 +(** Increasing **)
    9.84 +
    9.85 +Goalw [increasing_def, Increasing_def]
    9.86 +     "F : increasing[A](r, f) ==> F : Increasing[A](r, f)";
    9.87 +by (auto_tac (claset() addIs [stable_imp_Stable], simpset())); 
    9.88 +qed "increasing_imp_Increasing";
    9.89 +
    9.90 +Goalw [Increasing_def] "Increasing[A](r, f) <= program";
    9.91 +by Auto_tac;
    9.92 +qed "Increasing_type";
    9.93 +
    9.94 +Goalw [Increasing_def] "F:Increasing[A](r, f) ==> F:program";
    9.95 +by Auto_tac;
    9.96 +qed "Increasing_into_program";
    9.97 +
    9.98 +Goalw [Increasing_def]
    9.99 +"[| F:Increasing[A](r, f); a:A |] ==> F: Stable({s:state. <a,f(s)>:r})";
   9.100 +by (Blast_tac 1);
   9.101 +qed "Increasing_imp_Stable";
   9.102 +
   9.103 +Goalw [Increasing_def]
   9.104 +"F:Increasing[A](r, f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)";
   9.105 +by (subgoal_tac "EX x. x:state" 1);
   9.106 +by (auto_tac (claset() addIs [st0_in_state], simpset()));
   9.107 +qed "IncreasingD";
   9.108 +
   9.109 +Goal
   9.110 +"F:Increasing[A](r, %s. c) <-> F:program & (c:A)";
   9.111 +by (subgoal_tac "EX x. x:state" 1);
   9.112 +by (auto_tac (claset() addSDs [IncreasingD]
   9.113 +                       addIs [st0_in_state,
   9.114 +                   increasing_imp_Increasing], simpset()));
   9.115 +qed "Increasing_constant";
   9.116 +Addsimps [Increasing_constant];
   9.117 +
   9.118 +Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def, 
   9.119 +       constrains_def, mono1_def, comp_def]
   9.120 +"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
   9.121 +\  Increasing[A](r, f) <= Increasing[B](s, g comp f)";
   9.122 +by Safe_tac;
   9.123 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
   9.124 +by (subgoal_tac "xb:state & xa:state" 1);
   9.125 +by (asm_simp_tac (simpset() addsimps [ActsD]) 2);
   9.126 +by (subgoal_tac "<f(xb), f(xb)>:r" 1);
   9.127 +by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   9.128 +by (rotate_tac 5 1);
   9.129 +by (dres_inst_tac [("x", "f(xb)")] bspec 1);
   9.130 +by (ALLGOALS(Asm_full_simp_tac));
   9.131 +by (Clarify_tac 1);
   9.132 +by (rotate_tac ~2 1);
   9.133 +by (dres_inst_tac [("x", "act")] bspec 1);
   9.134 +by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
   9.135 +by (ALLGOALS(Asm_full_simp_tac));
   9.136 +by (Blast_tac 1);
   9.137 +by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
   9.138 +by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
   9.139 +by (ALLGOALS(Asm_full_simp_tac));
   9.140 +qed "subset_Increasing_comp";
   9.141 +
   9.142 +Goal "[| F:Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |]  \
   9.143 +\ ==> F:Increasing[B](s, g comp f)";
   9.144 +by (rtac (subset_Increasing_comp RS subsetD) 1);
   9.145 +by Auto_tac;
   9.146 +qed "imp_Increasing_comp";
   9.147 +  
   9.148 +Goalw [Increasing_def, Le_def, Lt_def]
   9.149 +"Increasing[nat](Le, f) <= Increasing[nat](Lt, f)";
   9.150 +by Auto_tac;
   9.151 +qed "strict_Increasing";
   9.152 +
   9.153 +Goalw [Increasing_def, Ge_def, Gt_def] 
   9.154 +"Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)";
   9.155 +by Auto_tac;
   9.156 +by (etac natE 1);
   9.157 +by (auto_tac (claset(), simpset() addsimps [Stable_def]));
   9.158 +qed "strict_gt_Increasing";
   9.159 +
   9.160 +(** Two-place monotone operations **)
   9.161 +
   9.162 +Goalw [increasing_def, stable_def, 
   9.163 +       part_order_def, constrains_def, mono2_def]
   9.164 +"[| F:increasing[A](r, f); F:increasing[B](s, g); \
   9.165 +\   mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
   9.166 +\  F:increasing[C](t, %x. h(f(x), g(x)))";
   9.167 +by (Clarify_tac 1);
   9.168 +by (Asm_full_simp_tac 1);
   9.169 +by (Clarify_tac 1);
   9.170 +by (rename_tac "xa xb" 1);
   9.171 +by (subgoal_tac "xb:state & xa:state" 1);
   9.172 +by (blast_tac (claset() addSDs [ActsD]) 2);
   9.173 +by (subgoal_tac "<f(xb), f(xb)>:r & <g(xb), g(xb)>:s" 1);
   9.174 +by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   9.175 +by (rotate_tac 6 1);
   9.176 +by (dres_inst_tac [("x", "f(xb)")] bspec 1);
   9.177 +by (rotate_tac 1 2);
   9.178 +by (dres_inst_tac [("x", "g(xb)")] bspec 2);
   9.179 +by (ALLGOALS(Asm_simp_tac));
   9.180 +by (rotate_tac ~1 1);
   9.181 +by (dres_inst_tac [("x", "act")] bspec 1);
   9.182 +by (rotate_tac ~3 2);
   9.183 +by (dres_inst_tac [("x", "act")] bspec 2);
   9.184 +by (ALLGOALS(Asm_full_simp_tac));
   9.185 +by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
   9.186 +by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
   9.187 +by (Blast_tac 1);
   9.188 +by (Blast_tac 1);
   9.189 +by (rotate_tac ~4 1);
   9.190 +by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
   9.191 +by (rotate_tac ~1 3);
   9.192 +by (dres_inst_tac [("x", "g(xa)"), ("x1", "g(xb)")] (bspec RS bspec) 3);
   9.193 +by (ALLGOALS(Asm_full_simp_tac));
   9.194 +by (res_inst_tac [("b", "h(f(xb), g(xb))"), ("A", "C")] trans_onD 1);
   9.195 +by (ALLGOALS(Asm_full_simp_tac));
   9.196 +qed "imp_increasing_comp2";
   9.197 +
   9.198 +Goalw [Increasing_def, stable_def, 
   9.199 +       part_order_def, constrains_def, mono2_def, Stable_def, Constrains_def]
   9.200 +"[| F:Increasing[A](r, f); F:Increasing[B](s, g); \
   9.201 +\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
   9.202 +\ F:Increasing[C](t, %x. h(f(x), g(x)))";
   9.203 +by Safe_tac;
   9.204 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
   9.205 +by (subgoal_tac "xa:state & x:state" 1);
   9.206 +by (blast_tac (claset() addSDs [ActsD]) 2);
   9.207 +by (subgoal_tac "<f(xa), f(xa)>:r & <g(xa), g(xa)>:s" 1);
   9.208 +by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
   9.209 +by (rotate_tac 6 1);
   9.210 +by (dres_inst_tac [("x", "f(xa)")] bspec 1);
   9.211 +by (rotate_tac 1 2);
   9.212 +by (dres_inst_tac [("x", "g(xa)")] bspec 2);
   9.213 +by (ALLGOALS(Asm_simp_tac));
   9.214 +by (Clarify_tac 1);
   9.215 +by (rotate_tac ~2 1);
   9.216 +by (dres_inst_tac [("x", "act")] bspec 1);
   9.217 +by (rotate_tac ~3 2);
   9.218 +by (dres_inst_tac [("x", "act")] bspec 2);
   9.219 +by (ALLGOALS(Asm_full_simp_tac));
   9.220 +by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 1);
   9.221 +by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 2);
   9.222 +by (Blast_tac 1);
   9.223 +by (Blast_tac 1);
   9.224 +by (rotate_tac ~9 1);
   9.225 +by (dres_inst_tac [("x", "f(x)"), ("x1", "f(xa)")] (bspec RS bspec) 1);
   9.226 +by (rotate_tac ~1 3);
   9.227 +by (dres_inst_tac [("x", "g(x)"), ("x1", "g(xa)")] (bspec RS bspec) 3);
   9.228 +by (ALLGOALS(Asm_full_simp_tac));
   9.229 +by (res_inst_tac [("b", "h(f(xa), g(xa))"), ("A", "C")] trans_onD 1);
   9.230 +by (ALLGOALS(Asm_full_simp_tac));
   9.231 +qed "imp_Increasing_comp2";
   9.232 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/ZF/UNITY/Increasing.thy	Wed May 28 18:13:41 2003 +0200
    10.3 @@ -0,0 +1,35 @@
    10.4 +(*  Title:      ZF/UNITY/Increasing
    10.5 +    ID:         $Id$
    10.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    10.7 +    Copyright   2001  University of Cambridge
    10.8 +
    10.9 +The "Increasing" relation of Charpentier.
   10.10 +
   10.11 +Increasing's parameters are a state function f, a domain A and an order
   10.12 +relation r over the domain A. 
   10.13 +*)
   10.14 +
   10.15 +Increasing = Constrains + Monotonicity +
   10.16 +constdefs
   10.17 +
   10.18 +  part_order :: [i, i] => o
   10.19 +  "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
   10.20 +
   10.21 +  increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')")
   10.22 +  "increasing[A](r, f) ==
   10.23 +    {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) &
   10.24 +                (ALL x:state. f(x):A)}"
   10.25 +  
   10.26 +  Increasing :: [i, i, i=>i] => i ("Increasing[_]'(_, _')")
   10.27 +  "Increasing[A](r, f) ==
   10.28 +    {F:program. (ALL k:A. F:Stable({s:state. <k, f(s)>:r})) &
   10.29 +                (ALL x:state. f(x):A)}"
   10.30 +
   10.31 +syntax
   10.32 +  IncWrt      ::  [i=>i, i, i] => i ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
   10.33 +
   10.34 +translations
   10.35 +  "IncWrt(f,r,A)" => "Increasing[A](r,f)"
   10.36 +
   10.37 +  
   10.38 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/ZF/UNITY/Monotonicity.ML	Wed May 28 18:13:41 2003 +0200
    11.3 @@ -0,0 +1,121 @@
    11.4 +(*  Title:      ZF/UNITY/Monotonicity.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    11.7 +    Copyright   2002  University of Cambridge
    11.8 +
    11.9 +Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
   11.10 +*)
   11.11 +
   11.12 +
   11.13 +(*TOO SLOW as a default simprule????
   11.14 +Addsimps [append_left_is_Nil_iff,append_left_is_Nil_iff2];
   11.15 +*)
   11.16 +
   11.17 +Goalw [mono1_def]
   11.18 +  "[| mono1(A, r, B, s, f); <x, y>:r; x:A; y:A |] ==> <f(x), f(y)>:s";
   11.19 +by Auto_tac;
   11.20 +qed "mono1D";
   11.21 +
   11.22 +Goalw [mono2_def]
   11.23 +"[| mono2(A, r, B, s, C, t, f);  <x, y>:r; <u,v>:s; x:A; y:A; u:B; v:B |] ==> \
   11.24 +\  <f(x, u), f(y,v)>:t";
   11.25 +by Auto_tac;
   11.26 +qed "mono2D";
   11.27 +
   11.28 +
   11.29 +(** Monotonicity of take **)
   11.30 +
   11.31 +Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
   11.32 +\   take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]";
   11.33 +by (induct_tac "xs" 1);
   11.34 +by (Asm_full_simp_tac 1);
   11.35 +by (Clarify_tac 1);
   11.36 +by (Asm_full_simp_tac 1);
   11.37 +by (etac natE 1);
   11.38 +by Auto_tac;
   11.39 +qed_spec_mp "take_succ";
   11.40 +
   11.41 +
   11.42 +Goal "[|xs:list(A); j:nat|] ==> ALL i:nat.  i #+ j le length(xs) --> \
   11.43 +\   take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))";
   11.44 +by (induct_tac "xs" 1);
   11.45 +by (ALLGOALS(Asm_full_simp_tac));
   11.46 +by (Clarify_tac 1); 
   11.47 +by (eres_inst_tac [("n","i")] natE 1); 
   11.48 +by (ALLGOALS(Asm_full_simp_tac));
   11.49 +qed_spec_mp "take_add";
   11.50 +
   11.51 +Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
   11.52 +by (case_tac "length(xs) le i" 1);
   11.53 +by (subgoal_tac "length(xs) le j" 1);
   11.54 +by (blast_tac (claset() addIs [le_trans]) 2);
   11.55 +by (Asm_simp_tac 1);
   11.56 +by (dtac not_lt_imp_le 1);
   11.57 +by Auto_tac;
   11.58 +by (case_tac "length(xs) le j" 1);
   11.59 +by (auto_tac (claset(), simpset() addsimps [take_prefix]));
   11.60 +by (dtac not_lt_imp_le 1);
   11.61 +by Auto_tac;
   11.62 +by (dres_inst_tac [("m", "i")] less_imp_succ_add 1);
   11.63 +by Auto_tac;
   11.64 +by (subgoal_tac "i #+ k le length(xs)" 1);
   11.65 +by (blast_tac (claset() addIs [leI]) 2);
   11.66 +by (asm_full_simp_tac (simpset() addsimps [take_add, prefix_iff, take_type, drop_type]) 1);
   11.67 +qed "take_mono_left";
   11.68 +
   11.69 +Goal "[| <xs, ys>:prefix(A); i:nat |] ==> <take(i, xs), take(i, ys)>:prefix(A)"; 
   11.70 +by (auto_tac (claset(), simpset() addsimps [prefix_iff]));
   11.71 +qed "take_mono_right";
   11.72 +
   11.73 +Goal "[| i le j; <xs, ys>:prefix(A); i:nat; j:nat |] ==> <take(i, xs), take(j, ys)>:prefix(A)";
   11.74 +by (res_inst_tac [("b", "take(j, xs)")] prefix_trans 1);
   11.75 +by (auto_tac (claset() addDs [prefix_type RS subsetD]
   11.76 +                       addIs [take_mono_left, take_mono_right], simpset()));
   11.77 +qed "take_mono";
   11.78 +
   11.79 +Goalw [mono2_def, Le_def] "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)";
   11.80 +by Auto_tac;
   11.81 +by (blast_tac (claset() addIs [take_mono]) 1);
   11.82 +qed "mono_take";
   11.83 +Addsimps [mono_take];
   11.84 +AddIs [mono_take];
   11.85 +
   11.86 +(** Monotonicity of length **)
   11.87 +
   11.88 +bind_thm("length_mono", prefix_length_le);
   11.89 +
   11.90 +Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le, length)";
   11.91 +by (auto_tac (claset() addDs [prefix_length_le],
   11.92 +             simpset() addsimps [Le_def]));
   11.93 +qed "mono_length";
   11.94 +Addsimps [mono_length];
   11.95 +AddIs [mono_length];
   11.96 +
   11.97 +(** Monotonicity of Un **)
   11.98 +
   11.99 +Goalw [mono2_def, SetLe_def]  
  11.100 + "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)";
  11.101 +by Auto_tac;
  11.102 +qed "mono_Un";
  11.103 +Addsimps [mono_Un];
  11.104 +AddIs [mono_Un];
  11.105 +
  11.106 +(* Monotonicity of multiset union *)
  11.107 +
  11.108 +Goalw [mono2_def, MultLe_def]  
  11.109 +   "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)";
  11.110 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  11.111 +by (REPEAT(blast_tac (claset() addIs [munion_multirel_mono,
  11.112 +                                munion_multirel_mono1,
  11.113 +                                munion_multirel_mono2,
  11.114 +                                multiset_into_Mult]) 1));
  11.115 +qed "mono_munion";
  11.116 +Addsimps [mono_munion];
  11.117 +AddIs [mono_munion];
  11.118 +
  11.119 +Goalw [mono1_def, Le_def] "mono1(nat, Le, nat, Le, succ)";
  11.120 +by Auto_tac;
  11.121 +qed "mono_succ";
  11.122 +Addsimps [mono_succ];
  11.123 +AddIs [mono_succ];
  11.124 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/ZF/UNITY/Monotonicity.thy	Wed May 28 18:13:41 2003 +0200
    12.3 @@ -0,0 +1,30 @@
    12.4 +(*  Title:      ZF/UNITY/Monotonicity.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
    12.7 +    Copyright   2002  University of Cambridge
    12.8 +
    12.9 +Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
   12.10 +*)
   12.11 +
   12.12 +Monotonicity =  GenPrefix  +  MultisetSum +
   12.13 +constdefs
   12.14 +mono1 :: [i, i, i, i, i=>i] => o
   12.15 +"mono1(A, r, B, s, f) ==
   12.16 + (ALL x:A. ALL y:A. <x, y>:r --> <f(x), f(y)>:s) & (ALL x:A. f(x):B)"
   12.17 +
   12.18 +  (* monotonicity of a 2-place meta-function f *)
   12.19 +
   12.20 +  mono2 :: [i, i, i, i, i, i, [i,i]=>i] => o
   12.21 +  "mono2(A, r, B, s, C, t, f) == (ALL x:A. ALL y:A. ALL u:B. ALL v:B.
   12.22 +    <x, y>:r & <u,v>:s --> <f(x, u), f(y,v)>:t) &
   12.23 +    (ALL x:A. ALL y:B. f(x,y):C)"
   12.24 +
   12.25 + (* Internalized relations on sets and multisets *)
   12.26 +
   12.27 +  SetLe :: i =>i
   12.28 +  "SetLe(A) == {<x, y>:Pow(A)*Pow(A). x <= y}"
   12.29 +
   12.30 +  MultLe :: [i,i] =>i
   12.31 +  "MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
   12.32 +
   12.33 +end
   12.34 \ No newline at end of file
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/ZF/UNITY/MultisetSum.ML	Wed May 28 18:13:41 2003 +0200
    13.3 @@ -0,0 +1,200 @@
    13.4 +(*  Title:      ZF/UNITY/MultusetSum.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Sidi O Ehmety
    13.7 +    Copyright:  2002 University of Cambridge
    13.8 +Setsum for multisets.
    13.9 +*)
   13.10 +
   13.11 +Goal "mset_of(normalize(M)) <= mset_of(M)";
   13.12 +by (auto_tac (claset(), simpset() addsimps [mset_of_def,normalize_def])); 
   13.13 +qed "mset_of_normalize";
   13.14 +
   13.15 +Goalw [general_setsum_def]
   13.16 +"general_setsum(0, B, e, f, g) = e";
   13.17 +by Auto_tac;
   13.18 +qed "general_setsum_0";
   13.19 +Addsimps [general_setsum_0];
   13.20 +
   13.21 +Goalw [general_setsum_def] 
   13.22 +"[| C:Fin(A); a:A; a~:C; e:B; ALL x:A. g(x):B; lcomm(B, B, f) |] ==> \
   13.23 +\ general_setsum(cons(a, C), B, e, f, g) = \
   13.24 +\   f(g(a), general_setsum(C, B, e, f,g))";
   13.25 +by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
   13.26 +                                             cons_absorb]));
   13.27 +by (blast_tac (claset() addDs [Fin_into_Finite]) 2);
   13.28 +by (resolve_tac [fold_cons] 1);
   13.29 +by (auto_tac (claset(), simpset() addsimps [lcomm_def]));
   13.30 +qed "general_setsum_cons";
   13.31 +Addsimps [general_setsum_cons];
   13.32 +
   13.33 +(** lcomm **)
   13.34 +
   13.35 +Goalw [lcomm_def]
   13.36 +"[| C<=A; lcomm(A, B, f) |] ==> lcomm(C, B,f)";
   13.37 +by Auto_tac;
   13.38 +by (Blast_tac 1);
   13.39 +qed "lcomm_mono";
   13.40 +
   13.41 +Goalw [lcomm_def]
   13.42 +  "lcomm(Mult(A), Mult(A), op +#)";
   13.43 +by (auto_tac (claset(), simpset() 
   13.44 +    addsimps [Mult_iff_multiset, munion_lcommute]));
   13.45 +qed "munion_lcomm";
   13.46 +Addsimps [munion_lcomm];
   13.47 +
   13.48 +(** msetsum **)
   13.49 +
   13.50 +Goal
   13.51 +"[| C:Fin(A); ALL x:A. multiset(g(x))& mset_of(g(x))<=B  |]  \
   13.52 +\  ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\<lambda>u v. u +# v, g))";
   13.53 +by (etac Fin_induct 1);
   13.54 +by Auto_tac;
   13.55 +by (stac general_setsum_cons 1); 
   13.56 +by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   13.57 +qed "multiset_general_setsum";
   13.58 +
   13.59 +Goalw [msetsum_def] "msetsum(g, 0, B) = 0";
   13.60 +by Auto_tac;
   13.61 +qed "msetsum_0";
   13.62 +Addsimps [msetsum_0];
   13.63 +
   13.64 +Goalw [msetsum_def]
   13.65 +"[| C:Fin(A); a~:C; a:A; ALL x:A. multiset(g(x)) & mset_of(g(x))<=B  |]  \
   13.66 +\  ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)";
   13.67 +by (stac general_setsum_cons 1); 
   13.68 +by (auto_tac (claset(), simpset() addsimps [multiset_general_setsum, Mult_iff_multiset]));
   13.69 +qed "msetsum_cons";
   13.70 +Addsimps [msetsum_cons];
   13.71 +
   13.72 +(* msetsum type *)
   13.73 +
   13.74 +Goal "multiset(msetsum(g, C, B))";
   13.75 +by (asm_full_simp_tac (simpset() addsimps [msetsum_def]) 1); 
   13.76 +qed "msetsum_multiset";
   13.77 +
   13.78 +Goal 
   13.79 +"[| C:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ 
   13.80 +\ ==> mset_of(msetsum(g, C, B))<=B";
   13.81 +by (etac Fin_induct 1);
   13.82 +by Auto_tac;
   13.83 +qed "mset_of_msetsum";
   13.84 +
   13.85 +
   13.86 +
   13.87 +(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
   13.88 +Goal 
   13.89 +"[| C:Fin(A); D:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
   13.90 +\     ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) \
   13.91 +\       = msetsum(g, C, B) +# msetsum(g, D, B)";
   13.92 +by (etac Fin_induct 1);
   13.93 +by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 2);
   13.94 +by (auto_tac (claset(), simpset() addsimps [msetsum_multiset]));
   13.95 +by (subgoal_tac "y Un D:Fin(A) & y Int D : Fin(A)" 1);
   13.96 +by (Clarify_tac 1);
   13.97 +by (case_tac "x:D" 1);
   13.98 +by (subgoal_tac "cons(x, y) Int D = y Int D" 2);
   13.99 +by (subgoal_tac "cons(x, y) Int D = cons(x, y Int D)" 1);
  13.100 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_absorb,
  13.101 +                munion_assoc, msetsum_multiset])));
  13.102 +by (asm_simp_tac (simpset() addsimps [munion_lcommute, msetsum_multiset]) 1);
  13.103 +by Auto_tac;
  13.104 +qed "msetsum_Un_Int";
  13.105 +
  13.106 +
  13.107 +Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; \
  13.108 +\  ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
  13.109 +\     ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)";  
  13.110 +by (stac (msetsum_Un_Int RS sym) 1);
  13.111 +by (auto_tac (claset(),  simpset() addsimps [msetsum_multiset]));
  13.112 +qed "msetsum_Un_disjoint";
  13.113 +
  13.114 +Goal "I:Fin(A) ==> (ALL i:I. C(i):Fin(B)) --> (UN i:I. C(i)):Fin(B)";
  13.115 +by (etac Fin_induct 1);
  13.116 +by Auto_tac;
  13.117 +qed_spec_mp "UN_Fin_lemma";
  13.118 + 
  13.119 +Goal "!!I. [| I:Fin(K); ALL i:K. C(i):Fin(A) |] ==> \
  13.120 +\ (ALL x:A. multiset(f(x)) & mset_of(f(x))<=B) -->  \
  13.121 +\ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
  13.122 +\   msetsum(f, UN i:I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; 
  13.123 +by (etac Fin_induct 1);
  13.124 +by (ALLGOALS(Clarify_tac));
  13.125 +by Auto_tac;
  13.126 +by (subgoal_tac "ALL i:y. x ~= i" 1);
  13.127 + by (Blast_tac 2); 
  13.128 +by (subgoal_tac "C(x) Int (UN i:y. C(i)) = 0" 1);
  13.129 + by (Blast_tac 2);
  13.130 +by (subgoal_tac " (UN i:y. C(i)):Fin(A) & C(x):Fin(A)" 1);
  13.131 +by (blast_tac (claset() addIs [UN_Fin_lemma] addDs [FinD]) 2);
  13.132 +by (Clarify_tac 1);
  13.133 +by (asm_simp_tac (simpset() addsimps [msetsum_Un_disjoint]) 1);
  13.134 +by (subgoal_tac "ALL x:K. multiset(msetsum(f, C(x), B)) &\
  13.135 +                \ mset_of(msetsum(f, C(x), B)) <= B" 1);
  13.136 +by (Asm_simp_tac 1);
  13.137 +by (Clarify_tac 1);
  13.138 +by (dres_inst_tac [("x", "xa")] bspec 1);
  13.139 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [msetsum_multiset, mset_of_msetsum])));
  13.140 +qed_spec_mp "msetsum_UN_disjoint";
  13.141 +
  13.142 +Goal 
  13.143 +"[| C:Fin(A); \
  13.144 +\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B; \
  13.145 +\ ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\
  13.146 +\ msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)";
  13.147 +by (subgoal_tac "ALL x:A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1);
  13.148 +by (etac Fin_induct 1);
  13.149 +by (ALLGOALS(Asm_simp_tac));
  13.150 +by (resolve_tac [trans] 1);
  13.151 +by (resolve_tac [msetsum_cons] 1);
  13.152 +by (assume_tac 1);
  13.153 +by (auto_tac (claset(), simpset() addsimps [msetsum_multiset, munion_assoc]));
  13.154 +by (asm_simp_tac (simpset() addsimps [msetsum_multiset, munion_lcommute]) 1);
  13.155 +qed "msetsum_addf";
  13.156 +
  13.157 +
  13.158 +val prems = Goal
  13.159 + "[| C=D; !!x. x:D ==> f(x) = g(x) |] ==> \
  13.160 +\    msetsum(f, C, B) = msetsum(g, D, B)";
  13.161 +by (asm_full_simp_tac (simpset() addsimps [msetsum_def, general_setsum_def]@prems addcongs [fold_cong]) 1);
  13.162 +qed  "msetsum_cong";
  13.163 +
  13.164 +Goal "[| multiset(M); multiset(N) |] ==> M +# N -# N = M";
  13.165 +by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
  13.166 +qed "multiset_union_diff";
  13.167 +
  13.168 +
  13.169 +Goal "[| C:Fin(A); D:Fin(A); \
  13.170 +\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B  |] \
  13.171 +\  ==> msetsum(f, C Un D, B) = \
  13.172 +\         msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)";
  13.173 +by (subgoal_tac "C Un D:Fin(A) & C Int D:Fin(A)" 1);
  13.174 +by (Clarify_tac 1);
  13.175 +by (stac (msetsum_Un_Int RS sym) 1);
  13.176 +by (ALLGOALS(asm_simp_tac (simpset() addsimps 
  13.177 +         [msetsum_multiset,multiset_union_diff])));
  13.178 +by (blast_tac (claset() addDs [FinD]) 1);
  13.179 +qed "msetsum_Un";
  13.180 +
  13.181 +
  13.182 +Goalw [nsetsum_def] "nsetsum(g, 0)=0";
  13.183 +by Auto_tac;
  13.184 +qed "nsetsum_0";
  13.185 +Addsimps [nsetsum_0];
  13.186 +
  13.187 +Goalw [nsetsum_def, general_setsum_def] 
  13.188 +"[| Finite(C); x~:C |] \
  13.189 +\  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
  13.190 +by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
  13.191 +by (res_inst_tac [("A", "cons(x, C)")] fold_cons 1);
  13.192 +by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
  13.193 +qed "nsetsum_cons";
  13.194 +Addsimps [nsetsum_cons];
  13.195 +
  13.196 +Goal "nsetsum(g, C):nat";
  13.197 +by (case_tac "Finite(C)" 1);
  13.198 +by (asm_simp_tac (simpset() addsimps [nsetsum_def, general_setsum_def]) 2);
  13.199 +by (etac Finite_induct 1);
  13.200 +by Auto_tac;
  13.201 +qed "nsetsum_type";
  13.202 +Addsimps [nsetsum_type];  
  13.203 +AddTCs [nsetsum_type];
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/ZF/UNITY/MultisetSum.thy	Wed May 28 18:13:41 2003 +0200
    14.3 @@ -0,0 +1,26 @@
    14.4 +(*  Title:      ZF/UNITY/MultusetSum.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:     Sidi O Ehmety
    14.7 +
    14.8 +Setsum for multisets.
    14.9 +*)
   14.10 +
   14.11 +MultisetSum = Multiset +
   14.12 +constdefs
   14.13 +
   14.14 +  lcomm :: "[i, i, [i,i]=>i]=>o"
   14.15 +  "lcomm(A, B, f) ==
   14.16 +   (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))= f(y, f(x, z)))  &
   14.17 +   (ALL x:A. ALL y:B. f(x, y):B)"
   14.18 +
   14.19 +  general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i"
   14.20 +   "general_setsum(C, B, e, f, g) ==
   14.21 +    if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e"
   14.22 +
   14.23 +  msetsum :: "[i=>i, i, i]=>i"
   14.24 +  "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))"
   14.25 +
   14.26 +  (* sum for naturals *)
   14.27 +  nsetsum :: "[i=>i, i] =>i"
   14.28 +  "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
   14.29 +end
   14.30 \ No newline at end of file
    15.1 --- a/src/ZF/UNITY/ROOT.ML	Wed May 28 10:48:20 2003 +0200
    15.2 +++ b/src/ZF/UNITY/ROOT.ML	Wed May 28 18:13:41 2003 +0200
    15.3 @@ -8,12 +8,14 @@
    15.4  
    15.5  add_path "../Induct";  (*for Multisets*)
    15.6  
    15.7 +(*Simple examples: no composition*)
    15.8 +time_use_thy"Mutex";
    15.9 +
   15.10  (*Basic meta-theory*)
   15.11  time_use_thy "Guar";
   15.12  
   15.13  (* Prefix relation; part of the Allocator example *)
   15.14  time_use_thy "GenPrefix";
   15.15  
   15.16 -(*Simple examples: no composition*)
   15.17 -time_use_thy"Mutex";
   15.18 +time_use_thy "Distributor";
   15.19