--- 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
--- 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
--- /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";
+
+
+
+
--- /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
--- /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";
--- /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
--- /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];
--- /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
--- /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";
+
--- /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
--- /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];
+
--- /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
--- /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];
--- /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
--- 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";