# HG changeset patch
# User paulson
# Date 1054138421 -7200
# Node ID e9c9f69e4f63a7bd4862907bde8ee027088e26b9
# Parent  4b61bbb0dcab35cb0a34310ea5aa6b51259e9057
some new ZF/UNITY material from Sidi Ehmety

diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Wed May 28 10:48:20 2003 +0200
+++ b/src/ZF/IsaMakefile	Wed May 28 18:13:41 2003 +0200
@@ -120,6 +120,12 @@
   UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
   UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \
   UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
+  UNITY/AllocBase.ML UNITY/AllocBase.thy\
+  UNITY/Distributor.ML UNITY/Distributor.thy\
+  UNITY/Follows.ML UNITY/Follows.thy\
+  UNITY/Increasing.ML UNITY/Increasing.thy\
+  UNITY/Monotonicity.ML UNITY/Monotonicity.thy\
+  UNITY/MultisetSum.ML UNITY/MultisetSum.thy\
   UNITY/WFair.ML UNITY/WFair.thy
 	@$(ISATOOL) usedir $(OUT)/ZF UNITY
 
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Wed May 28 10:48:20 2003 +0200
+++ b/src/ZF/OrderType.thy	Wed May 28 18:13:41 2003 +0200
@@ -1003,6 +1003,9 @@
 lemma tot_ord_Lt: "tot_ord(nat,Lt)"
 by (simp add: tot_ord_def linear_Lt part_ord_Lt)
 
+lemma well_ord_Lt: "well_ord(nat,Lt)"
+by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt)
+
 
 
 ML {*
@@ -1117,6 +1120,7 @@
 val part_ord_Lt = thm "part_ord_Lt";
 val linear_Lt = thm "linear_Lt";
 val tot_ord_Lt = thm "tot_ord_Lt";
+val well_ord_Lt = thm "well_ord_Lt";
 *}
 
 end
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/AllocBase.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/AllocBase.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,436 @@
+(*  Title:      ZF/UNITY/AllocBase.ML
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+
+Common declarations for Chandy and Charpentier's Allocator
+*)
+
+(*????remove from Union.ML:AddSEs [not_emptyE];*)
+Delrules [not_emptyE];
+
+Goal "0 < Nclients & 0 < NbT";
+by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
+by (auto_tac (claset() addIs [Ord_0_lt], simpset()));
+qed "Nclients_NbT_gt_0";
+Addsimps [Nclients_NbT_gt_0 RS conjunct1, Nclients_NbT_gt_0 RS conjunct2];
+
+Goal "Nclients ~= 0 & NbT ~= 0";
+by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
+by Auto_tac;
+qed "Nclients_NbT_not_0";
+Addsimps [Nclients_NbT_not_0 RS conjunct1, Nclients_NbT_not_0  RS conjunct2];
+
+Goal "Nclients:nat & NbT:nat";
+by (cut_facts_tac [Nclients_pos, NbT_pos] 1);
+by Auto_tac;
+qed "Nclients_NbT_type";
+Addsimps [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
+AddTCs [Nclients_NbT_type RS conjunct1, Nclients_NbT_type RS conjunct2];
+
+Goal "b:Inter(RepFun(Nclients, B)) <-> (ALL x:Nclients. b:B(x))";
+by (auto_tac (claset(), simpset() addsimps [INT_iff]));
+by (res_inst_tac [("x", "0")] exI 1);
+by (rtac ltD 1); 
+by Auto_tac; 
+qed "INT_Nclient_iff";
+AddIffs [INT_Nclient_iff];
+
+val succ_def = thm "succ_def";
+
+Goal "n:nat ==> \
+\     (ALL i:nat. i<n --> f(i) $<= g(i)) --> \
+\     setsum(f, n) $<= setsum(g,n)";
+by (induct_tac "n" 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [])));
+by (subgoal_tac "succ(x)=cons(x, x) & Finite(x) & x~:x" 1);
+by (Clarify_tac 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "ALL i:nat. i<x--> f(i) $<= g(i)" 1);
+by (resolve_tac [zadd_zle_mono] 1);
+by (thin_tac "succ(x)=cons(x,x)" 1);
+by (ALLGOALS(Asm_simp_tac));
+by (thin_tac "succ(x)=cons(x, x)" 1);
+by (Clarify_tac 1);
+by (dtac leI 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [nat_into_Finite,
+                                      mem_not_refl, succ_def]) 1);
+qed_spec_mp "setsum_fun_mono";
+
+Goal "l:list(A) ==> tokens(l):nat";
+by (etac list.induct 1);
+by Auto_tac;
+qed "tokens_type";
+AddTCs [tokens_type];
+Addsimps [tokens_type];
+
+Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
+\  --> tokens(xs) le tokens(ys)";
+by (induct_tac "xs" 1);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], 
+              simpset() addsimps [prefix_def]));
+qed_spec_mp "tokens_mono_aux";
+
+Goal "[| <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
+\     tokens(xs) le tokens(ys)";
+by (blast_tac (claset() addIs [tokens_mono_aux]) 1);
+qed "tokens_mono";
+
+Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le ,tokens)";
+by (auto_tac (claset() addIs [tokens_mono],
+             simpset() addsimps [Le_def]));
+qed "mono_tokens";
+Addsimps [mono_tokens];
+AddIs [mono_tokens];
+
+Goal 
+"[| xs:list(A); ys:list(A) |] ==> tokens(xs@ys) = tokens(xs) #+ tokens(ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "tokens_append";
+Addsimps [tokens_append];
+
+Goal "l:list(A) ==> ALL n:nat. length(take(n, l))=min(n, length(l))";
+by (induct_tac "l" 1);
+by Safe_tac;
+by (ALLGOALS(Asm_simp_tac));
+by (etac natE 1);
+by (ALLGOALS(Asm_simp_tac));
+qed "length_take";
+
+(** bag_of **)
+
+Goal "l:list(A) ==>bag_of(l):Mult(A)";
+by (induct_tac "l" 1);
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+qed "bag_of_type";
+AddTCs [bag_of_type];
+Addsimps [bag_of_type];
+
+Goal "l:list(A) ==> multiset(bag_of(l)) & mset_of(bag_of(l))<=A";
+by (dtac bag_of_type 1);
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+qed "bag_of_multiset";
+
+Goal "[| xs:list(A); ys:list(A)|] ==> bag_of(xs@ys) = bag_of(xs) +# bag_of(ys)";
+by (induct_tac "xs" 1);
+by (auto_tac (claset(), simpset() 
+       addsimps [bag_of_multiset, munion_assoc]));
+qed "bag_of_append";
+Addsimps [bag_of_append];
+
+Goal "xs:list(A) ==> ALL ys:list(A). <xs, ys>:prefix(A) \
+\  --> <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
+by (induct_tac "xs" 1);
+by (ALLGOALS(Clarify_tac));
+by (ftac bag_of_multiset 1);
+by (forw_inst_tac [("l", "ys")] bag_of_multiset 2);
+by (auto_tac (claset() addIs [empty_le_MultLe], 
+              simpset() addsimps [prefix_def]));
+by (rtac munion_mono 1);
+by (force_tac (claset(), simpset() addsimps 
+               [MultLe_def, Mult_iff_multiset]) 1);
+by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 1);
+qed_spec_mp "bag_of_mono_aux";
+
+Goal "[|  <xs, ys>:prefix(A); xs:list(A); ys:list(A) |] ==> \
+\  <bag_of(xs), bag_of(ys)>:MultLe(A, r)";
+by (blast_tac (claset() addIs [bag_of_mono_aux]) 1);
+qed "bag_of_mono";
+AddIs [bag_of_mono];
+
+Goalw [mono1_def]
+ "mono1(list(A), prefix(A), Mult(A), MultLe(A,r), bag_of)";
+by (auto_tac (claset(), simpset() addsimps [bag_of_type]));
+qed "mono_bag_of";
+Addsimps [mono_bag_of];
+
+
+(** msetsum **)
+
+bind_thm("nat_into_Fin", eqpoll_refl RSN (2,thm"Fin_lemma"));
+
+Goal "l : list(A) ==> C Int length(l) : Fin(length(l))";
+by (dtac length_type 1); 
+by (rtac Fin_subset 1); 
+by (rtac Int_lower2 1);
+by (etac nat_into_Fin 1); 
+qed "list_Int_length_Fin";
+
+
+
+Goal "[|xs \\<in> list(A); k \\<in> C \\<inter> length(xs)|] ==> k < length(xs)"; 
+by (asm_full_simp_tac (simpset() addsimps [ltI]) 1); 
+qed "mem_Int_imp_lt_length";
+
+
+Goal "[|C \\<subseteq> nat; x \\<in> A; xs \\<in> list(A)|]  \
+\ ==>  msetsum(\\<lambda>i. {#nth(i, xs @ [x])#}, C \\<inter> succ(length(xs)), A) = \
+\      (if length(xs) \\<in> C then \
+\         {#x#} +# msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A) \
+\       else msetsum(\\<lambda>x. {#nth(x, xs)#}, C \\<inter> length(xs), A))"; 
+by (asm_full_simp_tac (simpset() addsimps [subsetD, nth_append, lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [Int_succ_right]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
+by (Clarify_tac 1);
+by (stac msetsum_cons 1);
+by (rtac succI1 3);  
+by (blast_tac (claset() addIs [list_Int_length_Fin, subset_succI RS Fin_mono RS subsetD]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [mem_not_refl]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [nth_type, lt_not_refl]) 1); 
+by (blast_tac (claset() addIs [nat_into_Ord, ltI, length_type]) 1);
+by (asm_full_simp_tac (simpset() addsimps [lt_not_refl, mem_Int_imp_lt_length] addcongs [msetsum_cong]) 1); 
+qed "bag_of_sublist_lemma";
+
+Goal "l:list(A) ==> \
+\ C <= nat ==> \
+\ bag_of(sublist(l, C)) = \
+\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
+by (etac list_append_induct  1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [sublist_append, nth_append, 
+          bag_of_sublist_lemma, munion_commute, bag_of_sublist_lemma, 
+          msetsum_multiset, munion_0]) 1);  
+qed "bag_of_sublist_lemma2";
+
+
+Goal "l \\<in> list(A) ==> nat \\<inter> length(l) = length(l)";
+by (rtac Int_absorb1 1);
+by (rtac OrdmemD 1);  
+by Auto_tac; 
+qed "nat_Int_length_eq";
+
+(*eliminating the assumption C<=nat*)
+Goal "l:list(A) ==> \
+\ bag_of(sublist(l, C)) = msetsum(%i. {#nth(i, l)#}, C Int length(l), A)";
+by (subgoal_tac
+      " bag_of(sublist(l, C Int nat)) = \
+\     msetsum(%i. {#nth(i, l)#}, C Int length(l), A)" 1);
+by (asm_full_simp_tac (simpset() addsimps [sublist_Int_eq]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [bag_of_sublist_lemma2, Int_lower2, Int_assoc, nat_Int_length_eq]) 1); 
+qed "bag_of_sublist";
+
+Goal 
+"l:list(A) ==> \
+\ bag_of(sublist(l, B Un C)) +# bag_of(sublist(l, B Int C)) = \
+\     bag_of(sublist(l, B)) +# bag_of(sublist(l, C))";
+by (subgoal_tac
+      "B Int C Int length(l) = \
+\      (B Int length(l)) Int (C Int length(l))" 1);
+by (blast_tac (claset() addIs []) 2);
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist, 
+                                      Int_Un_distrib2, msetsum_Un_Int]) 1); 
+by (resolve_tac [msetsum_Un_Int] 1);
+by (REPEAT (etac list_Int_length_Fin 1)); 
+ by (asm_full_simp_tac (simpset() addsimps [ltI, nth_type]) 1); 
+qed "bag_of_sublist_Un_Int";
+
+
+Goal "[| l:list(A); B Int C = 0  |]\
+\     ==> bag_of(sublist(l, B Un C)) = \
+\         bag_of(sublist(l, B)) +# bag_of(sublist(l, C))"; 
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym, 
+                  sublist_type,  bag_of_multiset]) 1);
+qed "bag_of_sublist_Un_disjoint";
+
+Goal "[| Finite(I); ALL i:I. ALL j:I. i~=j --> A(i) Int A(j) = 0; \
+\ l:list(B) |] \
+\     ==> bag_of(sublist(l, UN i:I. A(i))) =  \
+\         (msetsum(%i. bag_of(sublist(l, A(i))), I, B)) ";  
+by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
+                            addsimps [bag_of_sublist]) 1);
+by (stac (inst "A" "length(l)" msetsum_UN_disjoint) 1);
+by (dresolve_tac [Finite_into_Fin] 1);
+by (assume_tac 1);
+by (Force_tac 3);
+by (auto_tac (claset() addSIs [Fin_IntI2, Finite_into_Fin], 
+              simpset() addsimps [ltI, nth_type, length_type, nat_into_Finite]));
+qed_spec_mp "bag_of_sublist_UN_disjoint";
+
+
+Goalw [part_ord_def, Lt_def, irrefl_def, trans_on_def]
+  "part_ord(nat, Lt)";
+by (auto_tac (claset() addIs [lt_trans], simpset()));
+qed "part_ord_Lt";
+Addsimps [part_ord_Lt];
+
+
+(** all_distinct **)
+
+Goalw [all_distinct_def] "all_distinct(Nil)";
+by Auto_tac;
+qed "all_distinct_Nil";
+
+Goalw [all_distinct_def] 
+"all_distinct(Cons(a, l)) <-> \
+\ (a:set_of_list(l) --> False) & (a ~: set_of_list(l) --> all_distinct(l))";
+by (auto_tac (claset() addEs [list.elim], simpset()));
+qed "all_distinct_Cons";
+Addsimps [all_distinct_Nil, all_distinct_Cons];
+
+(** state_of **)
+Goalw [state_of_def] "s:state ==> state_of(s)=s";
+by Auto_tac;
+qed "state_of_state";
+Addsimps [state_of_state];
+
+
+Goalw [state_of_def] "state_of(state_of(s))=state_of(s)";
+by Auto_tac;
+qed "state_of_idem";
+Addsimps [state_of_idem];
+
+
+Goalw [state_of_def] "state_of(s):state";
+by Auto_tac;
+qed "state_of_type";
+Addsimps [state_of_type];
+AddTCs [state_of_type];
+
+Goalw [lift_def] "lift(x, s)=s`x";
+by (Simp_tac 1);
+qed "lift_apply";
+Addsimps [lift_apply];
+
+(** Used in ClientImp **)
+
+Goalw [Increasing_def]
+"Increasing(A, r, %s. f(state_of(s))) = \
+\ Increasing(A, r, f)";
+by Auto_tac;
+qed "gen_Increains_state_of_eq";
+bind_thm("Increasing_state_ofD1", 
+gen_Increains_state_of_eq RS equalityD1 RS subsetD);
+bind_thm("Increasing_state_ofD2", 
+gen_Increains_state_of_eq RS equalityD2 RS subsetD);
+
+Goalw [Follows_def, Increasing_def] 
+"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =  \
+\ Follows(A, r, f, g)";
+by Auto_tac;
+qed "Follows_state_of_eq";
+bind_thm("Follows_state_ofD1", Follows_state_of_eq RS equalityD1 RS subsetD);
+bind_thm("Follows_state_ofD2", Follows_state_of_eq RS equalityD2 RS subsetD);
+
+(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
+fun list_of_Int th = 
+    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
+    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+    handle THM _ => (list_of_Int (th RS InterD))
+    handle THM _ => (list_of_Int (th RS bspec))
+    handle THM _ => [th];
+
+(*Used just once, for Alloc_Increasing*)
+
+fun normalize th = 
+     normalize (th RS spec
+                handle THM _ => th RS bspec
+                handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
+     handle THM _ => th;
+
+Goal "n:nat ==> nat_list_inj(n):list(nat)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "nat_list_inj_type";
+
+Goal "n:nat ==> length(nat_list_inj(n)) = n";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "length_nat_list_inj";
+
+Goalw [nat_var_inj_def]
+  "(lam x:nat. nat_var_inj(x)):inj(nat, var)";
+by (res_inst_tac [("d", "var_inj")] lam_injective 1); 
+by (asm_simp_tac (simpset() addsimps [length_nat_list_inj]) 2);
+by (auto_tac (claset(), simpset() addsimps var.intrs@[nat_list_inj_type]));
+qed "var_infinite_lemma";
+
+Goalw [lepoll_def] "nat lepoll var";
+by (res_inst_tac [("x", "(lam x:nat. nat_var_inj(x))")] exI 1);
+by (rtac var_infinite_lemma 1);
+qed "nat_lepoll_var";
+
+Goalw [Finite_def] "~Finite(var)";
+by Auto_tac;
+by (dtac eqpoll_imp_lepoll 1);
+by (cut_facts_tac [nat_lepoll_var] 1);
+by (subgoal_tac "nat lepoll x" 1);
+by (blast_tac (claset() addIs [lepoll_trans]) 2);
+by (dres_inst_tac [("i", "x"), ("A", "nat")] lepoll_cardinal_le 1);
+by Auto_tac;
+by (subgoal_tac "Card(nat)" 1);
+by (rewrite_goal_tac [Card_def] 1);
+by (dtac sym 1);
+by Auto_tac;
+by (dtac le_imp_subset 1);
+by (dtac subsetD 1);
+by (auto_tac (claset(), simpset() addsimps [Card_nat]));
+by (blast_tac (claset() addEs [mem_irrefl]) 1);
+qed "var_not_Finite";
+
+Goal "~Finite(A) ==> EX x. x:A";
+by (etac swap 1);
+by Auto_tac;
+by (subgoal_tac "A=0" 1);
+by (auto_tac (claset(), simpset() addsimps [Finite_0]));
+qed "not_Finite_imp_exist";
+
+Goal "Finite(A) ==> b:(Inter(RepFun(var-A, B))) <-> (ALL x:var-A. b:B(x))";
+by (subgoal_tac "EX x. x:var-A" 1);
+by Auto_tac;
+by (subgoal_tac "~Finite(var-A)" 1);
+by (dtac not_Finite_imp_exist 1);
+by Auto_tac;
+by (cut_facts_tac [var_not_Finite] 1);
+by (etac swap  1);
+by (res_inst_tac [("B", "A")] Diff_Finite 1);
+by Auto_tac;
+qed "Inter_Diff_var_iff";
+
+Goal "[| b:Inter(RepFun(var-A, B)); Finite(A); x:var-A |] ==> b:B(x)";
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() addsimps [Inter_Diff_var_iff]) 1);
+qed "Inter_var_DiffD";
+
+(* [| Finite(A); (ALL x:var-A. b:B(x)) |] ==> b:Inter(RepFun(var-A, B)) *)
+bind_thm("Inter_var_DiffI", Inter_Diff_var_iff RS iffD2);
+
+AddSIs [Inter_var_DiffI];
+Addsimps [Finite_0, Finite_cons];
+
+Goal "Acts(F)<= A Int Pow(state*state)  <-> Acts(F)<=A";
+by (cut_facts_tac [inst "F" "F" Acts_type] 1);
+by Auto_tac;
+qed "Acts_subset_Int_Pow_simp";
+Addsimps [Acts_subset_Int_Pow_simp];
+
+Goal "cons(x, A Int B) = cons(x, A) Int cons(x, B)";
+by Auto_tac;
+qed "cons_Int_distrib";
+
+
+(* Currently not used, but of potential interest *)
+Goal 
+"[| Finite(A); ALL x:A. g(x):nat |] ==> \
+\ setsum(%x. $#(g(x)), A) = $# nsetsum(%x. g(x), A)";
+by (etac Finite_induct 1);
+by (auto_tac (claset(), simpset() addsimps [int_of_add]));
+qed "setsum_nsetsum_eq";
+
+Goal 
+"[| A=B;  ALL x:A. f(x)=g(x);  ALL x:A. g(x):nat; \
+\     Finite(A) |]  ==> nsetsum(f, A) = nsetsum(g, B)";
+by (subgoal_tac "$# nsetsum(f, A) = $# nsetsum(g, B)" 1);
+by (rtac trans 2);
+by (rtac setsum_nsetsum_eq 3);
+by (rtac trans 2);
+by (rtac (setsum_nsetsum_eq RS sym) 2);
+by Auto_tac;
+by (rtac setsum_cong 1);
+by Auto_tac;
+qed "nsetsum_cong";  
+
+
+
+
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/AllocBase.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/AllocBase.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,72 @@
+(*  Title:      ZF/UNITY/AllocBase.thy
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+
+Common declarations for Chandy and Charpentier's Allocator
+*)
+
+AllocBase = Follows + MultisetSum + Guar + New +
+
+consts
+  tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
+  NbT      :: i  (* Number of tokens in system *)
+  Nclients :: i  (* Number of clients *)
+translations
+"tokbag" => "nat" 
+rules
+  NbT_pos  "NbT:nat-{0}"
+  Nclients_pos "Nclients:nat-{0}"
+  
+(*This function merely sums the elements of a list*)
+consts tokens     :: i =>i
+       item :: i (* Items to be merged/distributed *)
+primrec 
+  "tokens(Nil) = 0"
+  "tokens (Cons(x,xs)) = x #+ tokens(xs)"
+
+consts
+  bag_of :: i => i
+
+primrec
+  "bag_of(Nil)    = 0"
+  "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
+
+(* definitions needed in Client.thy *)
+consts
+  all_distinct0:: i=>i
+  all_distinct:: i=>o
+  
+primrec
+  "all_distinct0(Nil) = 1"
+  "all_distinct0(Cons(a, l)) =
+     (if a:set_of_list(l) then 0 else all_distinct0(l))"
+
+defs
+all_distinct_def
+  "all_distinct(l) == all_distinct0(l)=1"
+  
+constdefs  
+  (* coersion from anyting to state *)
+  state_of :: i =>i
+  "state_of(s) == if s:state then s else st0"
+
+  (* simplifies the expression of programs  *)
+
+  lift :: "i =>(i=>i)"
+  "lift(x) == %s. s`x"
+
+consts (* to show that the set of variables is infinite *)
+  nat_list_inj :: i=>i
+  nat_var_inj  :: i=>i
+  var_inj :: i=>i
+defs
+  nat_var_inj_def "nat_var_inj(n) == Var(nat_list_inj(n))"
+primrec
+  "nat_list_inj(0) = Nil"
+  "nat_list_inj(succ(n)) = Cons(n, nat_list_inj(n))"
+
+primrec
+  "var_inj(Var(l)) = length(l)"
+
+end
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Distributor.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Distributor.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,169 @@
+(*  Title: ZF/UNITY/Distributor
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Distributor specification
+*)
+
+Open_locale "Distributor";
+val all_distinct_vars = thm "all_distinct_vars";
+val var_assumes = thm "var_assumes";
+val type_assumes = thm "type_assumes";
+val default_val_assumes  = thm "default_val_assumes";
+
+Addsimps [var_assumes, default_val_assumes,  type_assumes];
+
+Goalw [state_def]
+"s:state ==> s`In:list(A)";
+by (dres_inst_tac [("a", "In")] apply_type 1);
+by Auto_tac;
+qed "In_value_type";
+AddTCs [In_value_type];
+Addsimps [In_value_type];
+
+Goalw [state_def]
+"s:state ==> s`iIn:list(nat)";
+by (dres_inst_tac [("a", "iIn")] apply_type 1);
+by Auto_tac;
+qed "iIn_value_type";
+AddTCs [iIn_value_type];
+Addsimps [iIn_value_type];
+
+Goalw [state_def]
+"s:state ==> s`Out(n):list(A)";
+by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
+by Auto_tac;
+qed "Out_value_type";
+AddTCs [Out_value_type];
+Addsimps [Out_value_type];
+
+val distrib = thm "distr_spec";
+
+Goal "D:program";
+by (cut_facts_tac [distrib] 1);
+by (auto_tac (claset(), simpset() addsimps 
+           [distr_spec_def, distr_allowed_acts_def]));
+qed "D_in_program";
+Addsimps [D_in_program];
+AddTCs [D_in_program];
+
+Goal "G:program ==> \
+\   D ok G <-> \
+\  ((ALL n:nat. G:preserves(lift(Out(n)))) & D:Allowed(G))";
+by (cut_facts_tac [distrib] 1);
+by (auto_tac (claset(), 
+     simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def, 
+                         Allowed_def, ok_iff_Allowed]));
+by (rotate_tac ~1 2);
+by (dres_inst_tac [("x", "G")] bspec 2);
+by Auto_tac;
+by (dresolve_tac [rotate_prems 1 (safety_prop_Acts_iff RS iffD1)] 1);
+by (auto_tac (claset() addIs [safety_prop_Inter], simpset()));
+qed "D_ok_iff";
+
+Goal 
+"D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
+\     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int \
+\     Always({s:state. ALL elt:set_of_list(s`iIn). elt<Nclients})) \
+\     guarantees \
+\         (INT n: Nclients. lift(Out(n)) IncreasingWrt \
+\                           prefix(A)/list(A))";
+by (cut_facts_tac [D_in_program, distrib] 1);
+by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
+by (auto_tac (claset() addSIs [guaranteesI]  addIs [Follows_imp_Increasing_left]
+                        addSDs [guaranteesD], 
+               simpset() addsimps []));
+qed "distr_Increasing_Out";
+
+val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
+
+Goal
+"[| ALL n:nat. G:preserves(lift(Out(n))); \
+\  D Join G:Always({s:state. \
+\         ALL elt:set_of_list(s`iIn). elt < Nclients}) |] \
+\ ==> D Join G : Always \
+\         ({s:state. msetsum(%n. bag_of (sublist(s`In, \
+\                      {k:nat. k < length(s`iIn) &\
+\                         nth(k, s`iIn)= n})), \
+\                        Nclients, A) = \
+\             bag_of(sublist(s`In, length(s`iIn)))})";
+by (cut_facts_tac [D_in_program] 1);
+by (subgoal_tac "G:program" 1);
+by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
+by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
+by Auto_tac;
+by (stac (bag_of_sublist_UN_disjoint RS sym) 1); 
+by (asm_simp_tac (simpset() addsimps [nat_into_Finite]) 1); 
+by (Blast_tac 1); 
+by (Asm_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1); 
+by (subgoal_tac
+    "(UN i: Nclients. {k:nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
+\    length(x`iIn)" 1);
+by (Asm_simp_tac 1);
+by (resolve_tac [equalityI] 1);
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [ltD]) 1);
+by (subgoal_tac "length(x ` iIn) : nat" 1);
+by Typecheck_tac; 
+by (subgoal_tac "xa : nat" 1); 
+by (dres_inst_tac [("x", "nth(xa, x`iIn)"),("P","%elt. ?X(elt) --> elt<Nclients")] bspec  1);
+by (asm_full_simp_tac (simpset() addsimps [ltI, nat_into_Ord]) 1); 
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_mem_iff_lt]))); 
+by (blast_tac (claset() addDs [ltD]) 1); 
+by (blast_tac (claset() addIs [lt_trans]) 1);
+qed "distr_bag_Follows_lemma";
+
+
+val prems =
+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')";
+by (asm_full_simp_tac (simpset() addsimps [Increasing_def,Follows_def]@prems) 1);
+qed "Follows_cong";
+(*????????????????*)
+
+Goal
+ "D : ((lift(In) IncreasingWrt prefix(A)/list(A)) Int \
+\      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int  \
+\       Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})) \
+\     guarantees  \
+\      (INT n: Nclients. \
+\       (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A)) \
+\       Fols \
+\       (%s. bag_of(sublist(s`In, length(s`iIn)))) \
+\       Wrt MultLe(A, r)/Mult(A))";
+by (cut_facts_tac [distrib] 1);
+by (rtac guaranteesI 1);
+by (Clarify_tac 1); 
+by (Simp_tac 2);
+by (rtac (distr_bag_Follows_lemma RS Always_Follows2) 1);
+by Auto_tac;  
+by (rtac Follows_state_ofD1 2);
+by (rtac Follows_msetsum_UN 2);
+by (ALLGOALS(Clarify_tac));
+by (resolve_tac [conjI] 3);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 3);
+by (resolve_tac [conjI] 4);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 4);
+by (resolve_tac [conjI] 5);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct1] 5);
+by (resolve_tac [inst "A" "A" bag_of_multiset RS conjunct2] 6);
+by (Clarify_tac 4);
+by (asm_full_simp_tac (simpset() addsimps []) 3);
+by (asm_full_simp_tac (simpset() addsimps []) 3);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [nat_into_Finite])));
+by (rotate_tac 2 1);
+by (asm_full_simp_tac (simpset() addsimps [D_ok_iff]) 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [distr_spec_def, distr_follows_def]));
+by (dtac guaranteesD 1); 
+by (assume_tac 1);
+by (force_tac (claset(), simpset() addsimps []) 1); 
+by (force_tac (claset(), simpset() addsimps []) 1); 
+by (asm_full_simp_tac
+    (simpset() addsimps [rewrite_rule [comp_def] (mono_bag_of RS subset_Follows_comp RS subsetD), 
+             refl_prefix, trans_on_MultLe] 
+            addcongs [Follows_cong]) 1); 
+qed  "distr_bag_Follows";
+Close_locale "Distributor";
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Distributor.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Distributor.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,50 @@
+(*  Title: ZF/UNITY/Distributor
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+A multiple-client allocator from a single-client allocator:
+Distributor specification
+*)
+Distributor = AllocBase + Follows +  Guar + GenPrefix +
+(** Distributor specification (the number of outputs is Nclients) ***)
+ (*spec (14)*)
+constdefs  
+  distr_follows :: [i, i, i, i =>i] =>i
+    "distr_follows(A, In, iIn, Out) ==
+     (lift(In) IncreasingWrt prefix(A)/list(A)) Int
+     (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
+     Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})
+         guarantees
+         (INT n: Nclients.
+          lift(Out(n))
+              Fols
+          (%s. sublist(s`In, 
+                       {k:nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
+	  Wrt prefix(A)/list(A))"
+  
+ distr_allowed_acts :: [i=>i]=>i
+  "distr_allowed_acts(Out) ==
+   {D:program. AllowedActs(D) =
+   cons(id(state), UN G:(INT n:nat. preserves(lift(Out(n)))). Acts(G))}"
+
+  distr_spec :: [i, i, i, i =>i]=>i
+  "distr_spec(A, In, iIn, Out) ==
+   distr_follows(A, In, iIn, Out) Int distr_allowed_acts(Out)"
+
+locale Distributor =
+  fixes In :: i  (*items to distribute*)
+        iIn :: i (*destinations of items to distribute*)
+        Out :: i=>i  (*distributed items*)
+        A :: i   (*the type of items being distributed *)
+        D :: i
+ assumes
+    var_assumes       "In:var & iIn:var & (ALL n. Out(n):var)"
+    all_distinct_vars "ALL n. all_distinct([In, iIn, iOut(n)])"
+    type_assumes      "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
+                       (ALL n. type_of(Out(n))=list(A))"
+   default_val_assumes "default_val(In)=Nil &
+                        default_val(iIn)=Nil &
+                        (ALL n. default_val(Out(n))=Nil)"
+   distr_spec  "D:distr_spec(A, In, iIn, Out)"
+end
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Follows.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Follows.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,510 @@
+(*  Title:      ZF/UNITY/Follows
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+ 
+The Follows relation of Charpentier and Sivilotte
+*)
+ 
+(*Does this hold for "invariant"?*)
+
+
+Goalw [mono1_def, comp_def] 
+"[| mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
+\  Always({x:state. <f(x), g(x)>:r})<=Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
+by (auto_tac (claset(), simpset() addsimps 
+         [Always_eq_includes_reachable]));
+qed "subset_Always_comp";
+
+Goal 
+"[| F:Always({x:state. <f(x), g(x)>:r}); \
+\   mono1(A, r, B, s, h); ALL x:state. f(x):A & g(x):A |] ==> \
+\   F:Always({x:state. <(h comp f)(x), (h comp g)(x)>:s})";
+by (blast_tac (claset() addIs [subset_Always_comp RS subsetD]) 1);
+qed "imp_Always_comp";
+
+Goal 
+"[| F:Always({x:state. <f1(x), f(x)>:r});  \
+\   F:Always({x:state. <g1(x), g(x)>:s}); \
+\   mono2(A, r, B, s, C, t, h); \
+\   ALL x:state. f1(x):A & f(x):A & g1(x):B & g(x):B |] \
+\ ==> F:Always({x:state. <h(f1(x), g1(x)), h(f(x), g(x))>:t})";
+by (auto_tac (claset(), simpset() addsimps 
+         [Always_eq_includes_reachable, mono2_def]));
+by (auto_tac (claset() addSDs [subsetD], simpset()));
+qed "imp_Always_comp2";
+
+(* comp LeadsTo *)
+
+Goalw [mono1_def, comp_def]
+"[| mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
+\       ALL x:state. f(x):A & g(x):A |] ==> \
+\ (INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}) <= \
+\(INT k:B. {x:state. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
+by (Clarify_tac 1);
+by (ALLGOALS(full_simp_tac (simpset() addsimps [INT_iff])));
+by Auto_tac;
+by (rtac single_LeadsTo_I 1);
+by (blast_tac (claset() addDs [LeadsTo_type RS subsetD]) 2);
+by Auto_tac;
+by (rotate_tac 5 1);
+by (dres_inst_tac [("x", "g(sa)")] bspec 1);
+by (etac LeadsTo_weaken 2);
+by (auto_tac (claset(), simpset() addsimps [part_order_def, refl_def]));
+by (res_inst_tac [("b", "h(g(sa))")] trans_onD 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "subset_LeadsTo_comp";
+
+Goal
+"[| F:(INT j:A. {s:state. <j, g(s)>:r} LeadsTo {s:state. <j,f(s)>:r}); \
+\   mono1(A, r, B, s, h); refl(A,r); trans[B](s); \
+\   ALL x:state. f(x):A & g(x):A |] ==> \
+\  F:(INT k:B. {x:state. <k, (h comp g)(x)>:s} LeadsTo {x:state. <k, (h comp f)(x)>:s})";
+by (rtac (subset_LeadsTo_comp RS subsetD) 1);
+by Auto_tac;
+qed "imp_LeadsTo_comp";
+
+Goalw [mono2_def, Increasing_def]
+"[| F:Increasing(B, s, g); \
+\ ALL j:A. F: {s:state. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
+\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t); \
+\ ALL x:state. f1(x):A & f(x):A & g(x):B; k:C |] ==> \
+\ F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g(x))>:t}";
+by (rtac single_LeadsTo_I 1);
+by Auto_tac;
+by (dres_inst_tac [("x", "g(sa)"), ("A","B")] bspec 1);
+by Auto_tac;
+by (dres_inst_tac [("x", "f(sa)"),("P","%j. F \\<in> ?X(j) \\<longmapsto>w ?Y(j)")] bspec 1);
+by Auto_tac;
+by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by Auto_tac;
+by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
+by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
+by (dres_inst_tac [("x", "f1(x)"), ("x1", "f(sa)"), 
+                   ("P2", "%x y. \\<forall>u\\<in>B. ?P(x,y,u)")] (bspec RS bspec) 1);
+by (dres_inst_tac [("x", "g(x)"), ("x1", "g(sa)"), 
+                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
+by Auto_tac;
+by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
+by (auto_tac (claset(), simpset() addsimps [part_order_def]));
+qed "imp_LeadsTo_comp_right";
+
+Goalw [mono2_def, Increasing_def]
+"[| F:Increasing(A, r, f); \
+\ ALL j:B. F: {x:state. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
+\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
+\ ALL x:state. f(x):A & g1(x):B & g(x):B; k:C |] ==> \
+\ F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f(x), g1(x))>:t}";
+by (rtac single_LeadsTo_I 1);
+by Auto_tac;
+by (dres_inst_tac [("x", "f(sa)"),("P","%k. F \\<in> Stable(?X(k))")] bspec 1);
+by Auto_tac;
+by (dres_inst_tac [("x", "g(sa)")] bspec 1);
+by Auto_tac;
+by (rtac (PSP_Stable RS LeadsTo_weaken) 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by Auto_tac;
+by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
+by (force_tac (claset(), simpset() addsimps [part_order_def, refl_def]) 1);
+by (dres_inst_tac [("x", "f(x)"), ("x1", "f(sa)")] (bspec RS bspec) 1);
+by (dres_inst_tac [("x", "g1(x)"), ("x1", "g(sa)"), 
+                 ("P2", "%x y. ?P(x,y) --> ?d(x,y) \\<in> t")] (bspec RS bspec) 3);
+by Auto_tac;
+by (res_inst_tac [("b", "h(f(sa), g(sa))"), ("A", "C")] trans_onD 1);
+by (auto_tac (claset(), simpset() addsimps [part_order_def]));
+qed "imp_LeadsTo_comp_left";
+
+(**  This general result is used to prove Follows Un, munion, etc. **)
+Goal
+"[| F:Increasing(A, r, f1) Int  Increasing(B, s, g); \
+\ ALL j:A. F: {s:state. <j, f(s)>:r} LeadsTo {s:state. <j,f1(s)>:r}; \
+\ ALL j:B. F: {x:state. <j, g(x)>:s} LeadsTo {x:state. <j,g1(x)>:s}; \
+\ mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t); \
+\ ALL x:state. f(x):A & g1(x):B & f1(x):A &g(x):B; k:C |]\
+\ ==> F:{x:state. <k, h(f(x), g(x))>:t} LeadsTo {x:state. <k, h(f1(x), g1(x))>:t}";
+by (res_inst_tac [("B", "{x:state. <k, h(f1(x), g(x))>:t}")] LeadsTo_Trans 1);
+by (blast_tac (claset() addIs [imp_LeadsTo_comp_right]) 1);
+by (blast_tac (claset() addIs [imp_LeadsTo_comp_left]) 1);
+qed "imp_LeadsTo_comp2";
+
+(* Follows type *)
+Goalw [Follows_def] "Follows(A, r, f, g)<=program";
+by (blast_tac (claset() addDs [Increasing_type RS subsetD]) 1);
+qed "Follows_type";
+
+Goal "F:Follows(A, r, f, g) ==> F:program";
+by (blast_tac (claset() addDs [Follows_type RS subsetD]) 1);
+qed "Follows_into_program";
+AddTCs [Follows_into_program];
+
+Goalw [Follows_def] 
+"F:Follows(A, r, f, g)==> \
+\ F:program & (EX a. a:A) & (ALL x:state. f(x):A & g(x):A)";
+by (blast_tac (claset() addDs [IncreasingD]) 1);
+qed "FollowsD";
+
+Goalw [Follows_def]
+ "[| F:program; c:A; refl(A, r) |] ==> F:Follows(A, r, %x. c, %x. c)";
+by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [refl_def]));
+qed "Follows_constantI";
+
+Goalw [Follows_def] 
+"[| mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
+\  ==> Follows(A, r, f, g) <= Follows(B, s,  h comp f, h comp g)";
+by (Clarify_tac 1);
+by (forw_inst_tac [("f", "g")] IncreasingD 1);
+by (forw_inst_tac [("f", "f")] IncreasingD 1);
+by (rtac IntI 1);
+by (res_inst_tac [("h", "h")] imp_LeadsTo_comp 2);
+by (assume_tac 5);
+by (auto_tac (claset() addIs  [imp_Increasing_comp, imp_Always_comp], 
+             simpset() delsimps INT_simps));
+qed "subset_Follows_comp";
+
+Goal
+"[| F:Follows(A, r, f, g);  mono1(A, r, B, s, h); refl(A, r); trans[B](s) |] \
+\ ==>  F:Follows(B, s,  h comp f, h comp g)";
+by (blast_tac (claset() addIs [subset_Follows_comp RS subsetD]) 1);
+qed "imp_Follows_comp";
+
+(* 2-place monotone operation: this general result is used to prove Follows_Un, Follows_munion *)
+
+(* 2-place monotone operation: this general result is 
+   used to prove Follows_Un, Follows_munion *)
+Goalw [Follows_def] 
+"[| F:Follows(A, r, f1, f);  F:Follows(B, s, g1, g); \
+\  mono2(A, r, B, s, C, t, h); refl(A,r); refl(B, s); trans[C](t) |] \
+\  ==> F:Follows(C, t, %x. h(f1(x), g1(x)), %x. h(f(x), g(x)))";
+by (Clarify_tac 1);
+by (forw_inst_tac [("f", "g")] IncreasingD 1);
+by (forw_inst_tac [("f", "f")] IncreasingD 1);
+by (rtac IntI 1);
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 2);
+by Safe_tac;
+by (res_inst_tac [("h", "h")] imp_Always_comp2 3);
+by (assume_tac 5);
+by (res_inst_tac [("h", "h")] imp_Increasing_comp2 2);
+by (assume_tac 4);
+by (res_inst_tac [("h", "h")] imp_Increasing_comp2 1);
+by (assume_tac 3);
+by (TRYALL(assume_tac));
+by (ALLGOALS(Asm_full_simp_tac)); 
+by (blast_tac (claset() addSDs [IncreasingD]) 1);
+by (res_inst_tac [("h", "h")] imp_LeadsTo_comp2 1);
+by (assume_tac 4);
+by Auto_tac;
+by (rewrite_goal_tac [mono2_def] 3);
+by (REPEAT(blast_tac (claset() addDs [IncreasingD]) 1));
+qed "imp_Follows_comp2";
+
+Goal "[| F : Follows(A, r, f, g);  F: Follows(A,r, g, h); \
+\        trans[A](r) |] ==> F : Follows(A, r, f, h)";
+by (forw_inst_tac [("f", "f")] FollowsD 1);
+by (forw_inst_tac [("f", "g")] FollowsD 1);
+by (rewrite_goal_tac [Follows_def] 1);
+by (asm_full_simp_tac (simpset() 
+                 addsimps [Always_eq_includes_reachable, INT_iff]) 1);
+by Auto_tac;
+by (res_inst_tac [("B", "{s:state. <k, g(s)>:r}")] LeadsTo_Trans 2);
+by (res_inst_tac [("b", "g(x)")] trans_onD 1);
+by (REPEAT(Blast_tac 1));
+qed "Follows_trans";
+
+(** Destruction rules for Follows **)
+
+Goalw [Follows_def]
+     "F : Follows(A, r, f,g) ==> F:Increasing(A, r, f)";
+by (Blast_tac 1);
+qed "Follows_imp_Increasing_left";
+
+Goalw [Follows_def]
+     "F : Follows(A, r, f,g) ==> F:Increasing(A, r, g)";
+by (Blast_tac 1);
+qed "Follows_imp_Increasing_right";
+
+Goalw [Follows_def]
+ "F :Follows(A, r, f, g) ==> F:Always({s:state. <f(s),g(s)>:r})";
+by (Blast_tac 1);
+qed "Follows_imp_Always";
+
+Goalw [Follows_def]
+ "[| F:Follows(A, r, f, g); k:A |]  ==> \
+\ F: {s:state. <k,g(s)>:r } LeadsTo {s:state. <k,f(s)>:r}";
+by (Blast_tac 1);
+qed "Follows_imp_LeadsTo";
+
+Goal "[| F : Follows(list(nat), gen_prefix(nat, Le), f, g); k:list(nat) |] \
+\  ==> F : {s:state. k pfixLe g(s)} LeadsTo {s:state. k pfixLe f(s)}";
+by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
+qed "Follows_LeadsTo_pfixLe";
+
+Goal "[| F : Follows(list(nat), gen_prefix(nat, Ge), f, g); k:list(nat) |] \
+\  ==> F : {s:state. k pfixGe g(s)} LeadsTo {s:state. k pfixGe f(s)}";
+by (blast_tac (claset() addIs [Follows_imp_LeadsTo]) 1);
+qed "Follows_LeadsTo_pfixGe";
+
+Goalw  [Follows_def, Increasing_def, Stable_def]
+"[| F:Always({s:state. f(s) = g(s)}); F:Follows(A, r, f, h);  \
+\   ALL x:state. g(x):A |] ==> F : Follows(A, r, g, h)";
+by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by Auto_tac;
+by (res_inst_tac [("C", "{s:state. f(s)=g(s)}"),
+                 ("A", "{s:state. <ka, h(s)>:r}"),
+                 ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s:state. <ka,f(s)>:r}"), 
+                   ("A'", "{s:state. <ka,f(s)>:r}")] 
+                  Always_Constrains_weaken 1);
+by Auto_tac;
+by (dtac Always_Int_I 1);
+by (assume_tac 1);
+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); 
+by Auto_tac;
+qed "Always_Follows1";
+
+Goalw [Follows_def, Increasing_def, Stable_def]
+"[| F : Always({s:state. g(s) = h(s)}); \
+\ F: Follows(A, r, f, g); ALL x:state. h(x):A |] ==> F : Follows(A, r, f, h)";
+by (full_simp_tac (simpset() addsimps [INT_iff]) 1);
+by Auto_tac;
+by (thin_tac "k:A" 3);
+by (res_inst_tac [("C", "{s:state. g(s)=h(s)}"),
+                  ("A", "{s:state. <ka, g(s)>:r}"),
+                  ("A'", "{s:state. <ka, f(s)>:r}")] Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s:state. <ka, g(s)>:r}"), 
+                   ("A'", "{s:state. <ka, g(s)>:r}")] 
+                  Always_Constrains_weaken 1);
+by Auto_tac;
+by (dtac Always_Int_I 1);
+by (assume_tac 1);
+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); 
+by Auto_tac;
+qed "Always_Follows2";
+
+(** Union properties (with the subset ordering) **)
+
+Goalw [refl_def, SetLe_def] "refl(Pow(A), SetLe(A))";
+by Auto_tac;
+qed "refl_SetLe";
+Addsimps [refl_SetLe];
+
+Goalw [trans_on_def, SetLe_def] "trans[Pow(A)](SetLe(A))";
+by Auto_tac;
+qed "trans_on_SetLe";
+Addsimps [trans_on_SetLe];
+
+Goalw [antisym_def, SetLe_def] "antisym(SetLe(A))";
+by Auto_tac;
+qed "antisym_SetLe";
+Addsimps [antisym_SetLe];
+
+Goalw [part_order_def] "part_order(Pow(A), SetLe(A))";
+by Auto_tac;
+qed "part_order_SetLe";
+Addsimps [part_order_SetLe];
+
+Goal "[| F: Increasing.increasing(Pow(A), SetLe(A), f);  \
+\        F: Increasing.increasing(Pow(A), SetLe(A), g) |] \
+\    ==> F : Increasing.increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
+by (res_inst_tac [("h", "op Un")] imp_increasing_comp2 1);
+by Auto_tac;
+qed "increasing_Un";
+
+Goal "[| F: Increasing(Pow(A), SetLe(A), f);  \
+\        F: Increasing(Pow(A), SetLe(A), g) |] \
+\    ==> F : Increasing(Pow(A), SetLe(A), %x. f(x) Un g(x))";
+by (res_inst_tac [("h", "op Un")] imp_Increasing_comp2 1);
+by Auto_tac;
+qed "Increasing_Un";
+
+Goal "[| F:Always({s:state. f1(s) <= f(s)}); \
+\    F : Always({s:state. g1(s) <= g(s)}) |] \
+\     ==> F : Always({s:state. f1(s) Un g1(s) <= f(s) Un g(s)})";
+by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
+by (Blast_tac 1);
+qed "Always_Un";
+
+Goal
+"[| F:Follows(Pow(A), SetLe(A), f1, f); \
+\    F:Follows(Pow(A), SetLe(A), g1, g) |] \
+\    ==> F:Follows(Pow(A), SetLe(A), %s. f1(s) Un g1(s), %s. f(s) Un g(s))";
+by (res_inst_tac [("h", "op Un")] imp_Follows_comp2 1);
+by Auto_tac;
+qed "Follows_Un";
+
+(** Multiset union properties (with the MultLe ordering) **)
+
+Goalw [MultLe_def, refl_def] "refl(Mult(A), MultLe(A,r))";
+by Auto_tac;
+qed "refl_MultLe";
+Addsimps [refl_MultLe];
+
+Goalw [MultLe_def, id_def, lam_def]
+ "[| multiset(M); mset_of(M)<=A |] ==> <M, M>:MultLe(A, r)";
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+qed "MultLe_refl1";
+Addsimps [MultLe_refl1];
+
+Goalw [MultLe_def, id_def, lam_def]
+ "M:Mult(A) ==> <M, M>:MultLe(A, r)";
+by Auto_tac;
+qed "MultLe_refl2";
+Addsimps [MultLe_refl2];
+
+Goalw [MultLe_def, trans_on_def] "trans[Mult(A)](MultLe(A,r))";
+by (auto_tac (claset() addIs [trancl_trans], simpset() addsimps [multirel_def]));
+qed "trans_on_MultLe";
+Addsimps [trans_on_MultLe];
+
+Goalw [MultLe_def] "MultLe(A, r)<= (Mult(A) * Mult(A))";
+by Auto_tac;
+by (dtac (multirel_type RS subsetD) 1);
+by Auto_tac;
+qed "MultLe_type";
+
+Goal "[| <M, K>:MultLe(A, r); <K, N>:MultLe(A, r) |] ==> <M, N>:MultLe(A,r)";
+by (cut_facts_tac [inst "A" "A" trans_on_MultLe] 1);
+by (dtac trans_onD 1);
+by (assume_tac 1);
+by (auto_tac (claset() addDs [MultLe_type RS subsetD], simpset()));
+qed "MultLe_trans";
+
+Goalw [part_order_def, part_ord_def]
+"part_order(A, r) ==> part_ord(A, r-id(A))";
+by (rewrite_goal_tac [refl_def, id_def, lam_def, irrefl_def] 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [trans_on_def]) 1);
+by Auto_tac;
+by (blast_tac (claset() addDs [trans_onD]) 1);
+by (full_simp_tac (simpset() addsimps [antisym_def]) 1);
+by Auto_tac;
+qed "part_order_imp_part_ord";
+
+Goalw [MultLe_def, antisym_def]
+  "part_order(A, r) ==> antisym(MultLe(A,r))";
+by (dtac part_order_imp_part_ord 1);
+by Auto_tac;
+by (dtac irrefl_on_multirel 1);
+by (forward_tac [multirel_type RS subsetD] 1);
+by (dtac multirel_trans 1);
+by (auto_tac (claset(), simpset() addsimps [irrefl_def]));
+qed "antisym_MultLe";
+Addsimps [antisym_MultLe];
+
+Goal  "part_order(A, r) ==>  part_order(Mult(A), MultLe(A, r))";
+by (ftac antisym_MultLe 1);
+by (auto_tac (claset(), simpset() addsimps [part_order_def]));
+qed "part_order_MultLe";
+Addsimps [part_order_MultLe];
+
+Goalw [MultLe_def]
+"[| multiset(M); mset_of(M)<= A|] ==> <0, M>:MultLe(A, r)";
+by (case_tac "M=0" 1);
+by (auto_tac (claset(), simpset() addsimps (thms"FiniteFun.intros")));
+by (subgoal_tac "<0 +# 0, 0 +# M>:multirel(A, r - id(A))" 1);
+by (rtac one_step_implies_multirel 2);
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+qed "empty_le_MultLe";
+Addsimps [empty_le_MultLe];
+
+Goal "M:Mult(A) ==> <0, M>:MultLe(A, r)";
+by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
+qed "empty_le_MultLe2";
+Addsimps [empty_le_MultLe2];
+
+Goalw [MultLe_def] 
+"[| <M, N>:MultLe(A, r); <K, L>:MultLe(A, r) |] ==>\
+\ <M +# K, N +# L>:MultLe(A, r)";
+by (auto_tac (claset() addIs [munion_multirel_mono1, 
+                              munion_multirel_mono2,
+                              munion_multirel_mono,
+                              multiset_into_Mult], 
+               simpset() addsimps [Mult_iff_multiset]));
+qed "munion_mono";
+
+Goal "[| F:Increasing.increasing(Mult(A), MultLe(A,r), f);  \
+\        F:Increasing.increasing(Mult(A), MultLe(A,r), g) |] \
+\    ==> F : Increasing.increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
+by (res_inst_tac [("h", "munion")] imp_increasing_comp2 1);
+by Auto_tac;
+qed "increasing_munion";
+
+Goal "[| F:Increasing(Mult(A), MultLe(A,r), f);  \
+\        F:Increasing(Mult(A), MultLe(A,r), g)|] \
+\    ==> F : Increasing(Mult(A),MultLe(A,r), %x. f(x) +# g(x))";
+by (res_inst_tac [("h", "munion")] imp_Increasing_comp2 1);
+by Auto_tac;
+qed "Increasing_munion";
+
+Goal
+"[| F:Always({s:state. <f1(s),f(s)>:MultLe(A,r)}); \
+\         F:Always({s:state. <g1(s), g(s)>:MultLe(A,r)});\
+\ ALL x:state. f1(x):Mult(A)&f(x):Mult(A) & g1(x):Mult(A) & g(x):Mult(A)|] \
+\     ==> F : Always({s:state. <f1(s) +# g1(s), f(s) +# g(s)>:MultLe(A,r)})";
+by (res_inst_tac [("h", "munion")] imp_Always_comp2 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (blast_tac (claset() addIs [munion_mono]) 1);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "Always_munion";
+
+Goal
+"[| F:Follows(Mult(A), MultLe(A, r), f1, f); \
+\   F:Follows(Mult(A), MultLe(A, r), g1, g) |] \
+\ ==> F:Follows(Mult(A), MultLe(A, r), %s. f1(s) +# g1(s), %s. f(s) +# g(s))";
+by (res_inst_tac [("h", "munion")] imp_Follows_comp2 1);
+by Auto_tac;
+qed "Follows_munion";
+
+(** Used in ClientImp **)
+
+Goal 
+"!!f. [| ALL i:I. F : Follows(Mult(A), MultLe(A, r), f'(i), f(i)); \
+\ ALL s. ALL i:I. multiset(f'(i, s)) & mset_of(f'(i, s))<=A & \
+\                       multiset(f(i, s)) & mset_of(f(i, s))<=A ; \
+\  Finite(I); F:program |] \
+\       ==> F : Follows(Mult(A), \
+\                       MultLe(A, r), %x. msetsum(%i. f'(i, x), I, A), \
+\                                     %x. msetsum(%i. f(i,  x), I, A))";
+by (etac rev_mp 1);
+by (dtac Finite_into_Fin 1);
+by (etac Fin_induct 1);
+by (Asm_simp_tac 1);
+by (rtac Follows_constantI 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps  (thms"FiniteFun.intros"))));
+by Auto_tac;
+by (resolve_tac [Follows_munion] 1);
+by Auto_tac;
+qed "Follows_msetsum_UN";
+
+Goalw [refl_def, Le_def] "refl(nat, Le)";
+by Auto_tac;
+qed "refl_Le";
+Addsimps [refl_Le];
+
+Goalw [trans_on_def, Le_def] "trans[nat](Le)";
+by Auto_tac;
+by (blast_tac (claset() addIs [le_trans]) 1);
+qed "trans_on_Le";
+Addsimps [trans_on_Le];
+
+Goalw [trans_def, Le_def] "trans(Le)";
+by Auto_tac;
+by (blast_tac (claset() addIs [le_trans]) 1);
+qed "trans_Le";
+Addsimps [trans_Le];
+
+Goalw [antisym_def, Le_def] "antisym(Le)";
+by Auto_tac;
+by (dtac le_imp_not_lt 1);
+by (auto_tac (claset(), simpset() addsimps [le_iff]));
+qed "antisym_Le";
+Addsimps [antisym_Le];
+
+Goalw [part_order_def] "part_order(nat, Le)";
+by Auto_tac;
+qed "part_order_Le";
+Addsimps [part_order_Le];
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Follows.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Follows.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,40 @@
+(*  Title:      ZF/UNITY/Follows
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+The "Follows" relation of Charpentier and Sivilotte
+
+Theory ported from HOL.
+*)
+
+Follows = SubstAx + Increasing +
+constdefs
+  Follows :: "[i, i, i=>i, i=>i] => i"
+  "Follows(A, r, f, g) == 
+            Increasing(A, r, g) Int
+            Increasing(A, r,f) Int
+            Always({s:state. <f(s), g(s)>:r}) Int
+           (INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"
+consts
+  Incr :: [i=>i]=>i   
+  n_Incr :: [i=>i]=>i
+  m_Incr :: [i=>i]=>i
+  s_Incr :: [i=>i]=>i
+  n_Fols :: [i=>i, i=>i]=>i   (infixl "n'_Fols" 65)
+
+syntax
+  Follows' :: "[i=>i, i=>i, i, i] => i"
+        ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)
+
+  
+translations
+  "Incr(f)" == "Increasing(list(nat), prefix(nat), f)"
+  "n_Incr(f)" == "Increasing(nat, Le, f)"
+  "s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"
+  "m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"
+  
+  "f n_Fols g" == "Follows(nat, Le, f, g)"
+
+  "Follows'(f,g,r,A)" == "Follows(A,r,f,g)"
+end
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Increasing.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Increasing.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,229 @@
+(*  Title:      ZF/UNITY/GenIncreasing
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+A general form of the `Increasing' relation of Charpentier
+*)
+
+(** increasing **)
+
+Goalw [increasing_def] "increasing[A](r, f) <= program";
+by (Blast_tac 1);
+qed "increasing_type";
+
+Goalw [increasing_def] "F:increasing[A](r, f) ==> F:program";
+by (Blast_tac 1);
+qed "increasing_into_program";
+
+Goalw [increasing_def]
+"[| F:increasing[A](r, f); x:A |] ==>F:stable({s:state. <x, f(s)>:r})";
+by (Blast_tac 1);
+qed "increasing_imp_stable";
+
+Goalw [increasing_def]
+"F:increasing[A](r,f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)";
+by (subgoal_tac "EX x. x:state" 1);
+by (auto_tac (claset() addDs [stable_type RS subsetD]
+                       addIs [st0_in_state], simpset()));
+qed "increasingD";
+
+Goalw [increasing_def, stable_def]
+ "F:increasing[A](r, %s. c) <-> F:program & c:A";
+by (subgoal_tac "EX x. x:state" 1);
+by (auto_tac (claset() addDs [stable_type RS subsetD]
+                       addIs [st0_in_state], simpset()));
+qed "increasing_constant";
+Addsimps [increasing_constant];
+
+Goalw [increasing_def, stable_def, part_order_def, 
+       constrains_def, mono1_def, comp_def]
+"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s)  |] ==> \
+\  increasing[A](r, f) <= increasing[B](s, g comp f)";
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "xa:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by (subgoal_tac "<f(xb), f(xb)>:r" 1);
+by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
+by (rotate_tac 5 1);
+by (dres_inst_tac [("x", "f(xb)")] bspec 1);
+by (rotate_tac ~1 2);
+by (dres_inst_tac [("x", "act")] bspec 2);
+by (ALLGOALS(Asm_full_simp_tac));
+by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
+by (Blast_tac 1);
+by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
+by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
+by (ALLGOALS(Asm_simp_tac));
+qed "subset_increasing_comp";
+
+Goal "[| F:increasing[A](r, f); mono1(A, r, B, s, g); \
+\        refl(A, r); trans[B](s) |] ==> F:increasing[B](s, g comp f)";
+by (rtac (subset_increasing_comp RS subsetD) 1);
+by Auto_tac;
+qed "imp_increasing_comp";
+
+Goalw [increasing_def, Le_def, Lt_def]
+   "increasing[nat](Le, f) <= increasing[nat](Lt, f)";
+by Auto_tac;
+qed "strict_increasing";
+
+Goalw [increasing_def, Gt_def, Ge_def]
+   "increasing[nat](Ge, f) <= increasing[nat](Gt, f)";
+by Auto_tac;
+by (etac natE 1);
+by (auto_tac (claset(), simpset() addsimps [stable_def]));
+qed "strict_gt_increasing";
+
+(** Increasing **)
+
+Goalw [increasing_def, Increasing_def]
+     "F : increasing[A](r, f) ==> F : Increasing[A](r, f)";
+by (auto_tac (claset() addIs [stable_imp_Stable], simpset())); 
+qed "increasing_imp_Increasing";
+
+Goalw [Increasing_def] "Increasing[A](r, f) <= program";
+by Auto_tac;
+qed "Increasing_type";
+
+Goalw [Increasing_def] "F:Increasing[A](r, f) ==> F:program";
+by Auto_tac;
+qed "Increasing_into_program";
+
+Goalw [Increasing_def]
+"[| F:Increasing[A](r, f); a:A |] ==> F: Stable({s:state. <a,f(s)>:r})";
+by (Blast_tac 1);
+qed "Increasing_imp_Stable";
+
+Goalw [Increasing_def]
+"F:Increasing[A](r, f) ==> F:program & (EX a. a:A) & (ALL s:state. f(s):A)";
+by (subgoal_tac "EX x. x:state" 1);
+by (auto_tac (claset() addIs [st0_in_state], simpset()));
+qed "IncreasingD";
+
+Goal
+"F:Increasing[A](r, %s. c) <-> F:program & (c:A)";
+by (subgoal_tac "EX x. x:state" 1);
+by (auto_tac (claset() addSDs [IncreasingD]
+                       addIs [st0_in_state,
+                   increasing_imp_Increasing], simpset()));
+qed "Increasing_constant";
+Addsimps [Increasing_constant];
+
+Goalw [Increasing_def, Stable_def, Constrains_def, part_order_def, 
+       constrains_def, mono1_def, comp_def]
+"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> \
+\  Increasing[A](r, f) <= Increasing[B](s, g comp f)";
+by Safe_tac;
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
+by (subgoal_tac "xb:state & xa:state" 1);
+by (asm_simp_tac (simpset() addsimps [ActsD]) 2);
+by (subgoal_tac "<f(xb), f(xb)>:r" 1);
+by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
+by (rotate_tac 5 1);
+by (dres_inst_tac [("x", "f(xb)")] bspec 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Clarify_tac 1);
+by (rotate_tac ~2 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Blast_tac 1);
+by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
+by (res_inst_tac [("b", "g(f(xb))"), ("A", "B")] trans_onD 3);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "subset_Increasing_comp";
+
+Goal "[| F:Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |]  \
+\ ==> F:Increasing[B](s, g comp f)";
+by (rtac (subset_Increasing_comp RS subsetD) 1);
+by Auto_tac;
+qed "imp_Increasing_comp";
+  
+Goalw [Increasing_def, Le_def, Lt_def]
+"Increasing[nat](Le, f) <= Increasing[nat](Lt, f)";
+by Auto_tac;
+qed "strict_Increasing";
+
+Goalw [Increasing_def, Ge_def, Gt_def] 
+"Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)";
+by Auto_tac;
+by (etac natE 1);
+by (auto_tac (claset(), simpset() addsimps [Stable_def]));
+qed "strict_gt_Increasing";
+
+(** Two-place monotone operations **)
+
+Goalw [increasing_def, stable_def, 
+       part_order_def, constrains_def, mono2_def]
+"[| F:increasing[A](r, f); F:increasing[B](s, g); \
+\   mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
+\  F:increasing[C](t, %x. h(f(x), g(x)))";
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "xa xb" 1);
+by (subgoal_tac "xb:state & xa:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by (subgoal_tac "<f(xb), f(xb)>:r & <g(xb), g(xb)>:s" 1);
+by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
+by (rotate_tac 6 1);
+by (dres_inst_tac [("x", "f(xb)")] bspec 1);
+by (rotate_tac 1 2);
+by (dres_inst_tac [("x", "g(xb)")] bspec 2);
+by (ALLGOALS(Asm_simp_tac));
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by (rotate_tac ~3 2);
+by (dres_inst_tac [("x", "act")] bspec 2);
+by (ALLGOALS(Asm_full_simp_tac));
+by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 1);
+by (dres_inst_tac [("A", "act``?u"), ("c", "xa")] subsetD 2);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (rotate_tac ~4 1);
+by (dres_inst_tac [("x", "f(xa)"), ("x1", "f(xb)")] (bspec RS bspec) 1);
+by (rotate_tac ~1 3);
+by (dres_inst_tac [("x", "g(xa)"), ("x1", "g(xb)")] (bspec RS bspec) 3);
+by (ALLGOALS(Asm_full_simp_tac));
+by (res_inst_tac [("b", "h(f(xb), g(xb))"), ("A", "C")] trans_onD 1);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "imp_increasing_comp2";
+
+Goalw [Increasing_def, stable_def, 
+       part_order_def, constrains_def, mono2_def, Stable_def, Constrains_def]
+"[| F:Increasing[A](r, f); F:Increasing[B](s, g); \
+\ mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> \
+\ F:Increasing[C](t, %x. h(f(x), g(x)))";
+by Safe_tac;
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [ActsD])));
+by (subgoal_tac "xa:state & x:state" 1);
+by (blast_tac (claset() addSDs [ActsD]) 2);
+by (subgoal_tac "<f(xa), f(xa)>:r & <g(xa), g(xa)>:s" 1);
+by (force_tac (claset(), simpset() addsimps [refl_def]) 2);
+by (rotate_tac 6 1);
+by (dres_inst_tac [("x", "f(xa)")] bspec 1);
+by (rotate_tac 1 2);
+by (dres_inst_tac [("x", "g(xa)")] bspec 2);
+by (ALLGOALS(Asm_simp_tac));
+by (Clarify_tac 1);
+by (rotate_tac ~2 1);
+by (dres_inst_tac [("x", "act")] bspec 1);
+by (rotate_tac ~3 2);
+by (dres_inst_tac [("x", "act")] bspec 2);
+by (ALLGOALS(Asm_full_simp_tac));
+by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 1);
+by (dres_inst_tac [("A", "act``?u"), ("c", "x")] subsetD 2);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (rotate_tac ~9 1);
+by (dres_inst_tac [("x", "f(x)"), ("x1", "f(xa)")] (bspec RS bspec) 1);
+by (rotate_tac ~1 3);
+by (dres_inst_tac [("x", "g(x)"), ("x1", "g(xa)")] (bspec RS bspec) 3);
+by (ALLGOALS(Asm_full_simp_tac));
+by (res_inst_tac [("b", "h(f(xa), g(xa))"), ("A", "C")] trans_onD 1);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "imp_Increasing_comp2";
+
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Increasing.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Increasing.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,35 @@
+(*  Title:      ZF/UNITY/Increasing
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2001  University of Cambridge
+
+The "Increasing" relation of Charpentier.
+
+Increasing's parameters are a state function f, a domain A and an order
+relation r over the domain A. 
+*)
+
+Increasing = Constrains + Monotonicity +
+constdefs
+
+  part_order :: [i, i] => o
+  "part_order(A, r) == refl(A,r) & trans[A](r) & antisym(r)"
+
+  increasing :: [i, i, i=>i] => i ("increasing[_]'(_, _')")
+  "increasing[A](r, f) ==
+    {F:program. (ALL k:A. F: stable({s:state. <k, f(s)>:r})) &
+                (ALL x:state. f(x):A)}"
+  
+  Increasing :: [i, i, i=>i] => i ("Increasing[_]'(_, _')")
+  "Increasing[A](r, f) ==
+    {F:program. (ALL k:A. F:Stable({s:state. <k, f(s)>:r})) &
+                (ALL x:state. f(x):A)}"
+
+syntax
+  IncWrt      ::  [i=>i, i, i] => i ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
+
+translations
+  "IncWrt(f,r,A)" => "Increasing[A](r,f)"
+
+  
+end
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Monotonicity.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Monotonicity.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,121 @@
+(*  Title:      ZF/UNITY/Monotonicity.ML
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
+*)
+
+
+(*TOO SLOW as a default simprule????
+Addsimps [append_left_is_Nil_iff,append_left_is_Nil_iff2];
+*)
+
+Goalw [mono1_def]
+  "[| mono1(A, r, B, s, f); <x, y>:r; x:A; y:A |] ==> <f(x), f(y)>:s";
+by Auto_tac;
+qed "mono1D";
+
+Goalw [mono2_def]
+"[| mono2(A, r, B, s, C, t, f);  <x, y>:r; <u,v>:s; x:A; y:A; u:B; v:B |] ==> \
+\  <f(x, u), f(y,v)>:t";
+by Auto_tac;
+qed "mono2D";
+
+
+(** Monotonicity of take **)
+
+Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
+\   take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]";
+by (induct_tac "xs" 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (etac natE 1);
+by Auto_tac;
+qed_spec_mp "take_succ";
+
+
+Goal "[|xs:list(A); j:nat|] ==> ALL i:nat.  i #+ j le length(xs) --> \
+\   take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))";
+by (induct_tac "xs" 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Clarify_tac 1); 
+by (eres_inst_tac [("n","i")] natE 1); 
+by (ALLGOALS(Asm_full_simp_tac));
+qed_spec_mp "take_add";
+
+Goal "[| i le j; xs:list(A); i:nat; j:nat |] ==> <take(i, xs), take(j, xs)>:prefix(A)";
+by (case_tac "length(xs) le i" 1);
+by (subgoal_tac "length(xs) le j" 1);
+by (blast_tac (claset() addIs [le_trans]) 2);
+by (Asm_simp_tac 1);
+by (dtac not_lt_imp_le 1);
+by Auto_tac;
+by (case_tac "length(xs) le j" 1);
+by (auto_tac (claset(), simpset() addsimps [take_prefix]));
+by (dtac not_lt_imp_le 1);
+by Auto_tac;
+by (dres_inst_tac [("m", "i")] less_imp_succ_add 1);
+by Auto_tac;
+by (subgoal_tac "i #+ k le length(xs)" 1);
+by (blast_tac (claset() addIs [leI]) 2);
+by (asm_full_simp_tac (simpset() addsimps [take_add, prefix_iff, take_type, drop_type]) 1);
+qed "take_mono_left";
+
+Goal "[| <xs, ys>:prefix(A); i:nat |] ==> <take(i, xs), take(i, ys)>:prefix(A)"; 
+by (auto_tac (claset(), simpset() addsimps [prefix_iff]));
+qed "take_mono_right";
+
+Goal "[| i le j; <xs, ys>:prefix(A); i:nat; j:nat |] ==> <take(i, xs), take(j, ys)>:prefix(A)";
+by (res_inst_tac [("b", "take(j, xs)")] prefix_trans 1);
+by (auto_tac (claset() addDs [prefix_type RS subsetD]
+                       addIs [take_mono_left, take_mono_right], simpset()));
+qed "take_mono";
+
+Goalw [mono2_def, Le_def] "mono2(nat, Le, list(A), prefix(A), list(A), prefix(A), take)";
+by Auto_tac;
+by (blast_tac (claset() addIs [take_mono]) 1);
+qed "mono_take";
+Addsimps [mono_take];
+AddIs [mono_take];
+
+(** Monotonicity of length **)
+
+bind_thm("length_mono", prefix_length_le);
+
+Goalw [mono1_def] "mono1(list(A), prefix(A), nat, Le, length)";
+by (auto_tac (claset() addDs [prefix_length_le],
+             simpset() addsimps [Le_def]));
+qed "mono_length";
+Addsimps [mono_length];
+AddIs [mono_length];
+
+(** Monotonicity of Un **)
+
+Goalw [mono2_def, SetLe_def]  
+ "mono2(Pow(A), SetLe(A), Pow(A), SetLe(A), Pow(A), SetLe(A), op Un)";
+by Auto_tac;
+qed "mono_Un";
+Addsimps [mono_Un];
+AddIs [mono_Un];
+
+(* Monotonicity of multiset union *)
+
+Goalw [mono2_def, MultLe_def]  
+   "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)";
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+by (REPEAT(blast_tac (claset() addIs [munion_multirel_mono,
+                                munion_multirel_mono1,
+                                munion_multirel_mono2,
+                                multiset_into_Mult]) 1));
+qed "mono_munion";
+Addsimps [mono_munion];
+AddIs [mono_munion];
+
+Goalw [mono1_def, Le_def] "mono1(nat, Le, nat, Le, succ)";
+by Auto_tac;
+qed "mono_succ";
+Addsimps [mono_succ];
+AddIs [mono_succ];
+
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/Monotonicity.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/Monotonicity.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,30 @@
+(*  Title:      ZF/UNITY/Monotonicity.thy
+    ID:         $Id$
+    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
+*)
+
+Monotonicity =  GenPrefix  +  MultisetSum +
+constdefs
+mono1 :: [i, i, i, i, i=>i] => o
+"mono1(A, r, B, s, f) ==
+ (ALL x:A. ALL y:A. <x, y>:r --> <f(x), f(y)>:s) & (ALL x:A. f(x):B)"
+
+  (* monotonicity of a 2-place meta-function f *)
+
+  mono2 :: [i, i, i, i, i, i, [i,i]=>i] => o
+  "mono2(A, r, B, s, C, t, f) == (ALL x:A. ALL y:A. ALL u:B. ALL v:B.
+    <x, y>:r & <u,v>:s --> <f(x, u), f(y,v)>:t) &
+    (ALL x:A. ALL y:B. f(x,y):C)"
+
+ (* Internalized relations on sets and multisets *)
+
+  SetLe :: i =>i
+  "SetLe(A) == {<x, y>:Pow(A)*Pow(A). x <= y}"
+
+  MultLe :: [i,i] =>i
+  "MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
+
+end
\ No newline at end of file
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/MultisetSum.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/MultisetSum.ML	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,200 @@
+(*  Title:      ZF/UNITY/MultusetSum.thy
+    ID:         $Id$
+    Author:     Sidi O Ehmety
+    Copyright:  2002 University of Cambridge
+Setsum for multisets.
+*)
+
+Goal "mset_of(normalize(M)) <= mset_of(M)";
+by (auto_tac (claset(), simpset() addsimps [mset_of_def,normalize_def])); 
+qed "mset_of_normalize";
+
+Goalw [general_setsum_def]
+"general_setsum(0, B, e, f, g) = e";
+by Auto_tac;
+qed "general_setsum_0";
+Addsimps [general_setsum_0];
+
+Goalw [general_setsum_def] 
+"[| C:Fin(A); a:A; a~:C; e:B; ALL x:A. g(x):B; lcomm(B, B, f) |] ==> \
+\ general_setsum(cons(a, C), B, e, f, g) = \
+\   f(g(a), general_setsum(C, B, e, f,g))";
+by  (auto_tac (claset(), simpset() addsimps [Fin_into_Finite RS Finite_cons, 
+                                             cons_absorb]));
+by (blast_tac (claset() addDs [Fin_into_Finite]) 2);
+by (resolve_tac [fold_cons] 1);
+by (auto_tac (claset(), simpset() addsimps [lcomm_def]));
+qed "general_setsum_cons";
+Addsimps [general_setsum_cons];
+
+(** lcomm **)
+
+Goalw [lcomm_def]
+"[| C<=A; lcomm(A, B, f) |] ==> lcomm(C, B,f)";
+by Auto_tac;
+by (Blast_tac 1);
+qed "lcomm_mono";
+
+Goalw [lcomm_def]
+  "lcomm(Mult(A), Mult(A), op +#)";
+by (auto_tac (claset(), simpset() 
+    addsimps [Mult_iff_multiset, munion_lcommute]));
+qed "munion_lcomm";
+Addsimps [munion_lcomm];
+
+(** msetsum **)
+
+Goal
+"[| C:Fin(A); ALL x:A. multiset(g(x))& mset_of(g(x))<=B  |]  \
+\  ==> multiset(general_setsum(C, B -||> nat - {0}, 0, \\<lambda>u v. u +# v, g))";
+by (etac Fin_induct 1);
+by Auto_tac;
+by (stac general_setsum_cons 1); 
+by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
+qed "multiset_general_setsum";
+
+Goalw [msetsum_def] "msetsum(g, 0, B) = 0";
+by Auto_tac;
+qed "msetsum_0";
+Addsimps [msetsum_0];
+
+Goalw [msetsum_def]
+"[| C:Fin(A); a~:C; a:A; ALL x:A. multiset(g(x)) & mset_of(g(x))<=B  |]  \
+\  ==> msetsum(g, cons(a, C), B) = g(a) +#  msetsum(g, C, B)";
+by (stac general_setsum_cons 1); 
+by (auto_tac (claset(), simpset() addsimps [multiset_general_setsum, Mult_iff_multiset]));
+qed "msetsum_cons";
+Addsimps [msetsum_cons];
+
+(* msetsum type *)
+
+Goal "multiset(msetsum(g, C, B))";
+by (asm_full_simp_tac (simpset() addsimps [msetsum_def]) 1); 
+qed "msetsum_multiset";
+
+Goal 
+"[| C:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \ 
+\ ==> mset_of(msetsum(g, C, B))<=B";
+by (etac Fin_induct 1);
+by Auto_tac;
+qed "mset_of_msetsum";
+
+
+
+(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
+Goal 
+"[| C:Fin(A); D:Fin(A); ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
+\     ==> msetsum(g, C Un D, B) +# msetsum(g, C Int D, B) \
+\       = msetsum(g, C, B) +# msetsum(g, D, B)";
+by (etac Fin_induct 1);
+by (subgoal_tac "cons(x, y) Un D = cons(x, y Un D)" 2);
+by (auto_tac (claset(), simpset() addsimps [msetsum_multiset]));
+by (subgoal_tac "y Un D:Fin(A) & y Int D : Fin(A)" 1);
+by (Clarify_tac 1);
+by (case_tac "x:D" 1);
+by (subgoal_tac "cons(x, y) Int D = y Int D" 2);
+by (subgoal_tac "cons(x, y) Int D = cons(x, y Int D)" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [cons_absorb,
+                munion_assoc, msetsum_multiset])));
+by (asm_simp_tac (simpset() addsimps [munion_lcommute, msetsum_multiset]) 1);
+by Auto_tac;
+qed "msetsum_Un_Int";
+
+
+Goal "[| C:Fin(A); D:Fin(A); C Int D = 0; \
+\  ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] \
+\     ==> msetsum(g, C Un D, B) = msetsum(g, C, B) +# msetsum(g,D, B)";  
+by (stac (msetsum_Un_Int RS sym) 1);
+by (auto_tac (claset(),  simpset() addsimps [msetsum_multiset]));
+qed "msetsum_Un_disjoint";
+
+Goal "I:Fin(A) ==> (ALL i:I. C(i):Fin(B)) --> (UN i:I. C(i)):Fin(B)";
+by (etac Fin_induct 1);
+by Auto_tac;
+qed_spec_mp "UN_Fin_lemma";
+ 
+Goal "!!I. [| I:Fin(K); ALL i:K. C(i):Fin(A) |] ==> \
+\ (ALL x:A. multiset(f(x)) & mset_of(f(x))<=B) -->  \
+\ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
+\   msetsum(f, UN i:I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"; 
+by (etac Fin_induct 1);
+by (ALLGOALS(Clarify_tac));
+by Auto_tac;
+by (subgoal_tac "ALL i:y. x ~= i" 1);
+ by (Blast_tac 2); 
+by (subgoal_tac "C(x) Int (UN i:y. C(i)) = 0" 1);
+ by (Blast_tac 2);
+by (subgoal_tac " (UN i:y. C(i)):Fin(A) & C(x):Fin(A)" 1);
+by (blast_tac (claset() addIs [UN_Fin_lemma] addDs [FinD]) 2);
+by (Clarify_tac 1);
+by (asm_simp_tac (simpset() addsimps [msetsum_Un_disjoint]) 1);
+by (subgoal_tac "ALL x:K. multiset(msetsum(f, C(x), B)) &\
+                \ mset_of(msetsum(f, C(x), B)) <= B" 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "xa")] bspec 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [msetsum_multiset, mset_of_msetsum])));
+qed_spec_mp "msetsum_UN_disjoint";
+
+Goal 
+"[| C:Fin(A); \
+\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B; \
+\ ALL x:A. multiset(g(x)) & mset_of(g(x))<=B |] ==>\
+\ msetsum(%x. f(x) +# g(x), C, B) = msetsum(f, C, B) +# msetsum(g, C, B)";
+by (subgoal_tac "ALL x:A. multiset(f(x) +# g(x)) & mset_of(f(x) +# g(x))<=B" 1);
+by (etac Fin_induct 1);
+by (ALLGOALS(Asm_simp_tac));
+by (resolve_tac [trans] 1);
+by (resolve_tac [msetsum_cons] 1);
+by (assume_tac 1);
+by (auto_tac (claset(), simpset() addsimps [msetsum_multiset, munion_assoc]));
+by (asm_simp_tac (simpset() addsimps [msetsum_multiset, munion_lcommute]) 1);
+qed "msetsum_addf";
+
+
+val prems = Goal
+ "[| C=D; !!x. x:D ==> f(x) = g(x) |] ==> \
+\    msetsum(f, C, B) = msetsum(g, D, B)";
+by (asm_full_simp_tac (simpset() addsimps [msetsum_def, general_setsum_def]@prems addcongs [fold_cong]) 1);
+qed  "msetsum_cong";
+
+Goal "[| multiset(M); multiset(N) |] ==> M +# N -# N = M";
+by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
+qed "multiset_union_diff";
+
+
+Goal "[| C:Fin(A); D:Fin(A); \
+\ ALL x:A. multiset(f(x)) & mset_of(f(x))<=B  |] \
+\  ==> msetsum(f, C Un D, B) = \
+\         msetsum(f, C, B) +# msetsum(f, D, B) -# msetsum(f, C Int D, B)";
+by (subgoal_tac "C Un D:Fin(A) & C Int D:Fin(A)" 1);
+by (Clarify_tac 1);
+by (stac (msetsum_Un_Int RS sym) 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps 
+         [msetsum_multiset,multiset_union_diff])));
+by (blast_tac (claset() addDs [FinD]) 1);
+qed "msetsum_Un";
+
+
+Goalw [nsetsum_def] "nsetsum(g, 0)=0";
+by Auto_tac;
+qed "nsetsum_0";
+Addsimps [nsetsum_0];
+
+Goalw [nsetsum_def, general_setsum_def] 
+"[| Finite(C); x~:C |] \
+\  ==> nsetsum(g, cons(x, C))= g(x) #+ nsetsum(g, C)";
+by (auto_tac (claset(), simpset() addsimps [Finite_cons]));
+by (res_inst_tac [("A", "cons(x, C)")] fold_cons 1);
+by (auto_tac (claset() addIs [Finite_cons_lemma], simpset()));
+qed "nsetsum_cons";
+Addsimps [nsetsum_cons];
+
+Goal "nsetsum(g, C):nat";
+by (case_tac "Finite(C)" 1);
+by (asm_simp_tac (simpset() addsimps [nsetsum_def, general_setsum_def]) 2);
+by (etac Finite_induct 1);
+by Auto_tac;
+qed "nsetsum_type";
+Addsimps [nsetsum_type];  
+AddTCs [nsetsum_type];
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/MultisetSum.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/MultisetSum.thy	Wed May 28 18:13:41 2003 +0200
@@ -0,0 +1,26 @@
+(*  Title:      ZF/UNITY/MultusetSum.thy
+    ID:         $Id$
+    Author:     Sidi O Ehmety
+
+Setsum for multisets.
+*)
+
+MultisetSum = Multiset +
+constdefs
+
+  lcomm :: "[i, i, [i,i]=>i]=>o"
+  "lcomm(A, B, f) ==
+   (ALL x:A. ALL y:A. ALL z:B. f(x, f(y, z))= f(y, f(x, z)))  &
+   (ALL x:A. ALL y:B. f(x, y):B)"
+
+  general_setsum :: "[i,i,i, [i,i]=>i, i=>i] =>i"
+   "general_setsum(C, B, e, f, g) ==
+    if Finite(C) then fold[cons(e, B)](%x y. f(g(x), y), e, C) else e"
+
+  msetsum :: "[i=>i, i, i]=>i"
+  "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))"
+
+  (* sum for naturals *)
+  nsetsum :: "[i=>i, i] =>i"
+  "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
+end
\ No newline at end of file
diff -r 4b61bbb0dcab -r e9c9f69e4f63 src/ZF/UNITY/ROOT.ML
--- a/src/ZF/UNITY/ROOT.ML	Wed May 28 10:48:20 2003 +0200
+++ b/src/ZF/UNITY/ROOT.ML	Wed May 28 18:13:41 2003 +0200
@@ -8,12 +8,14 @@
 
 add_path "../Induct";  (*for Multisets*)
 
+(*Simple examples: no composition*)
+time_use_thy"Mutex";
+
 (*Basic meta-theory*)
 time_use_thy "Guar";
 
 (* Prefix relation; part of the Allocator example *)
 time_use_thy "GenPrefix";
 
-(*Simple examples: no composition*)
-time_use_thy"Mutex";
+time_use_thy "Distributor";