--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/FoldSet.ML Wed Nov 07 18:12:12 2001 +0100
@@ -0,0 +1,412 @@
+(* Title: ZF/UNITY/FoldSet.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+
+A "fold" functional for finite sets. For n non-negative we have
+fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at
+least left-commutative.
+*)
+
+(** foldSet **)
+
+bind_thm("empty_fold_setE",
+ fold_set.mk_cases "<0, x> : fold_set(A, B, f,e)");
+bind_thm("cons_fold_setE",
+ fold_set.mk_cases "<cons(x,C), y> : fold_set(A, B, f,e)");
+
+bind_thm("fold_set_lhs", fold_set.dom_subset RS subsetD RS SigmaD1);
+bind_thm("fold_set_rhs", fold_set.dom_subset RS subsetD RS SigmaD2);
+
+(* add-hoc lemmas *)
+
+Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C";
+by (auto_tac (claset() addEs [equalityE], simpset()));
+qed "cons_lemma1";
+
+Goal "[| cons(x, B)=cons(y, C); x~=y; x~:B; y~:C |] \
+\ ==> B - {y} = C-{x} & x:C & y:B";
+by (auto_tac (claset() addEs [equalityE], simpset()));
+qed "cons_lemma2";
+
+
+Open_locale "LC";
+val f_lcomm = thm "lcomm";
+val f_type = thm "ftype";
+
+Goal "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A |] \
+\ ==> <C, f(x,y)> : fold_set(A, B, f, e)";
+by (forward_tac [fold_set_rhs] 1);
+by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1);
+by (auto_tac (claset() addIs [f_type], simpset()));
+qed "Diff1_fold_set";
+
+Goal "[| C:Fin(A); e:B |] ==> EX x. <C, x> : fold_set(A, B, f,e)";
+by (etac Fin_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (forward_tac [fold_set_rhs] 2);
+by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2);
+by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1));
+qed_spec_mp "Fin_imp_fold_set";
+
+
+Goal "n:nat \
+\ ==> ALL C x. |C|<n --> e:B --> <C, x> : fold_set(A, B, f,e)-->\
+\ (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x)";
+by (etac nat_induct 1);
+by (auto_tac (claset(), simpset() addsimps [le_iff]));
+by (etac fold_set.elim 1);
+by (blast_tac (claset() addEs [empty_fold_setE]) 1);
+by (etac fold_set.elim 1);
+by (blast_tac (claset() addEs [empty_fold_setE]) 1);
+by (Clarify_tac 1);
+(*force simplification of "|C| < |cons(...)|"*)
+by (rotate_tac 2 1);
+by (etac rev_mp 1);
+by (forw_inst_tac [("a", "Ca")] fold_set_lhs 1);
+by (forw_inst_tac [("a", "Cb")] fold_set_lhs 1);
+by (asm_simp_tac (simpset() addsimps [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1);
+by (rtac impI 1);
+(** LEVEL 10 **)
+by (case_tac "x=xb" 1 THEN Auto_tac);
+by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1);
+by (Blast_tac 1);
+(*case x ~= xb*)
+by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac);
+by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1);
+by (blast_tac (claset() addEs [equalityE]) 2);
+(** LEVEL 20 **)
+by (subgoal_tac "|Ca| le |Cb|" 1);
+by (rtac succ_le_imp_le 2);
+by (hyp_subst_tac 2);
+by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2);
+by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff,
+ Fin_into_Finite RS Finite_imp_cardinal_cons]) 2);
+by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2);
+by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A")]
+ (Fin_imp_fold_set RS exE) 1);
+by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1);
+by (Blast_tac 1);
+(** LEVEL 28 **)
+by (ftac Diff1_fold_set 1 THEN assume_tac 1 THEN assume_tac 1);
+by (subgoal_tac "ya = f(xb, xa)" 1);
+by (blast_tac (claset() delrules [equalityCE]) 2);
+by (subgoal_tac "<Cb-{x}, xa>: fold_set(A, B, f, e)" 1);
+ by (Asm_full_simp_tac 2);
+by (subgoal_tac "yb = f(x, xa)" 1);
+ by (blast_tac (claset() delrules [equalityCE]
+ addDs [Diff1_fold_set]) 2);
+by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1);
+qed_spec_mp "lemma";
+
+
+Goal "[| <C, x> : fold_set(A, B, f, e); \
+\ <C, y> : fold_set(A, B, f, e); e:B |] ==> y=x";
+by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1);
+by (rewrite_goals_tac [Finite_def]);
+by (Clarify_tac 1);
+by (res_inst_tac [("n", "succ(n)")] lemma 1);
+by (auto_tac (claset() addIs
+ [eqpoll_imp_lepoll RS lepoll_cardinal_le],
+ simpset()));
+qed "fold_set_determ";
+
+Goalw [fold_def]
+ "[| <C,y> : fold_set(C, B, f, e); e:B |] ==> fold[B](f,e,C) = y";
+by (rtac the_equality 1);
+by (rtac fold_set_determ 2);
+by Auto_tac;
+qed "fold_equality";
+
+Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e";
+by (blast_tac (claset() addSEs [empty_fold_setE]
+ addIs fold_set.intrs) 1);
+qed "fold_0";
+Addsimps [fold_0];
+
+Goal "[| x ~: C; x:A; e:B |] \
+\ ==> <cons(x, C), v> : fold_set(A, B, f, e) <-> \
+\ (EX y. <C, y> : fold_set(A, B, f, e) & v = f(x, y))";
+by Auto_tac;
+by (res_inst_tac [("A1", "A"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1);
+by (res_inst_tac [("x", "xa")] exI 3);
+by (res_inst_tac [("b", "cons(x, C)")] Fin_subset 1);
+by (auto_tac (claset() addDs [fold_set_lhs]
+ addIs [f_type]@fold_set.intrs, simpset()));
+by (blast_tac (claset() addIs [fold_set_determ, f_type]@fold_set.intrs) 1);
+val lemma = result();
+
+Goal "<D, x> : fold_set(C, B, f, e) \
+\ ==> ALL A. C<=A --> <D, x> : fold_set(A, B, f, e)";
+by (etac fold_set.induct 1);
+by (auto_tac (claset() addIs fold_set.intrs, simpset()));
+qed "lemma2";
+
+Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)";
+by (Clarify_tac 1);
+by (forward_tac [impOfSubs fold_set.dom_subset] 1);
+by (Clarify_tac 1);
+by (auto_tac (claset() addDs [lemma2], simpset()));
+qed "fold_set_mono";
+
+Goal "<C,x> : fold_set(A, B, f, e) ==> <C, x> : fold_set(C,B, f,e)";
+by (etac fold_set.induct 1);
+by (auto_tac (claset() addSIs fold_set.intrs, simpset()));
+by (res_inst_tac [("C1", "C"), ("A1", "cons(x, C)")]
+ (fold_set_mono RS subsetD) 1);
+by Auto_tac;
+qed "fold_set_mono2";
+
+
+Goalw [fold_def]
+ "[| Finite(C); x ~: C; e:B |] \
+\ ==> fold[B](f, e, cons(x, C)) = f(x, fold[B](f,e, C))";
+by (asm_simp_tac (simpset() addsimps [lemma]) 1);
+by (dtac Finite_into_Fin 1);
+by (rtac the_equality 1);
+by (dtac Fin_imp_fold_set 1);
+by Auto_tac;
+by (res_inst_tac [("x", "xa")] exI 1);
+by Auto_tac;
+by (resolve_tac [fold_set_mono RS subsetD] 1);
+by (Blast_tac 2);
+by (dresolve_tac [fold_set_mono2] 3);
+by (auto_tac (claset() addIs [Fin_imp_fold_set],
+ simpset() addsimps [symmetric fold_def, fold_equality]));
+qed "fold_cons";
+
+
+Goal "Finite(C) \
+\ ==> ALL e:B. f(x, fold[B](f, e, C)) = fold[B](f, f(x, e), C)";
+by (etac Finite_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (asm_full_simp_tac (simpset() addsimps [f_type]) 1);
+by (asm_simp_tac (simpset()
+ addsimps [f_lcomm, fold_cons, f_type]) 1);
+qed_spec_mp "fold_commute";
+
+
+Goal "Finite(C) ==> e:B -->fold[B](f, e, C):B";
+by (etac Finite_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [fold_cons, f_type]) 1);
+qed_spec_mp "fold_type";
+
+Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)";
+by Auto_tac;
+qed "cons_Int_right_lemma1";
+
+Goal "x~:D ==> cons(x, C) Int D = C Int D";
+by Auto_tac;
+qed "cons_Int_right_lemma2";
+
+Goal "[| Finite(C); Finite(D); e:B|] \
+\ ==> fold[B](f, fold[B](f, e, D), C) \
+\ = fold[B](f, fold[B](f, e, (C Int D)), C Un D)";
+by (etac Finite_induct 1);
+by (asm_full_simp_tac (simpset() addsimps [f_type, fold_type]) 1);
+by (subgoal_tac "Finite(Ba Int D) & \
+ \cons(x, Ba) Un D = cons(x, Ba Un D) & \
+ \Finite(Ba Un D)" 1);
+by (auto_tac (claset()
+ addIs [Finite_Un,Int_lower1 RS subset_Finite], simpset()));
+by (case_tac "x:D" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps
+ [cons_Int_right_lemma1,cons_Int_right_lemma2,
+ fold_type, fold_cons,fold_commute,cons_absorb, f_type])));
+qed "fold_nest_Un_Int";
+
+
+Goal "[| Finite(C); Finite(D); C Int D = 0; e:B |] \
+\ ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)";
+by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1);
+qed "fold_nest_Un_disjoint";
+
+Close_locale "LC";
+
+
+(** setsum **)
+
+Goalw [setsum_def] "setsum(g, 0) = #0";
+by (Simp_tac 1);
+qed "setsum_0";
+Addsimps [setsum_0];
+
+Goalw [setsum_def]
+ "[| Finite(C); c~:C |] \
+\ ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)";
+by (asm_simp_tac (simpset() addsimps [Finite_cons,export fold_cons]) 1);
+qed "setsum_cons";
+Addsimps [setsum_cons];
+
+Goal "setsum((%i. #0), C) = #0";
+by (case_tac "Finite(C)" 1);
+by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
+by (etac Finite_induct 1);
+by Auto_tac;
+qed "setsum_0";
+
+(*The reversed orientation looks more natural, but LOOPS as a simprule!*)
+Goal "[| Finite(C); Finite(D) |] \
+\ ==> setsum(g, C Un D) $+ setsum(g, C Int D) \
+\ = setsum(g, C) $+ setsum(g, D)";
+by (etac Finite_induct 1);
+by (subgoal_tac "cons(x, B) Un D = cons(x, B Un D) & \
+ \ Finite(B Un D) & Finite(B Int D)" 2);
+by (auto_tac (claset() addIs [Finite_Un, Int_lower1 RS subset_Finite],
+ simpset()));
+by (case_tac "x:D" 1);
+by (subgoal_tac "cons(x, B) Int D = B Int D" 2);
+by (subgoal_tac "cons(x, B) Int D = cons(x, B Int D)" 1);
+by Auto_tac;
+by (subgoal_tac "cons(x, B Un D) = B Un D" 1);
+by Auto_tac;
+qed "setsum_Un_Int";
+
+Goal "setsum(g, C):int";
+by (case_tac "Finite(C)" 1);
+by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
+by (etac Finite_induct 1);
+by Auto_tac;
+qed "setsum_type";
+Addsimps [setsum_type]; AddTCs [setsum_type];
+
+Goal "[| Finite(C); Finite(D); C Int D = 0 |] \
+\ ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)";
+by (stac (setsum_Un_Int RS sym) 1);
+by (subgoal_tac "Finite(C Un D)" 3);
+by (auto_tac (claset() addIs [Finite_Un], simpset()));
+qed "setsum_Un_disjoint";
+
+Goal "Finite(I) ==> (ALL i:I. Finite(C(i))) --> Finite(RepFun(I, C))";
+by (etac Finite_induct 1);
+by (auto_tac (claset(), simpset() addsimps [Finite_0]));
+by (stac (cons_eq RS sym) 1);
+by (auto_tac (claset() addIs [Finite_Un, Finite_cons, Finite_0], simpset()));
+qed_spec_mp "Finite_RepFun";
+
+Goal "!!I. Finite(I) \
+\ ==> (ALL i:I. Finite(C(i))) --> \
+\ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \
+\ setsum(f, UN i:I. C(i)) = setsum (%i. setsum(f, C(i)), I)";
+by (etac Finite_induct 1);
+by (ALLGOALS(Clarify_tac));
+by Auto_tac;
+by (subgoal_tac "ALL i:B. x ~= i" 1);
+ by (Blast_tac 2);
+by (subgoal_tac "C(x) Int (UN i:B. C(i)) = 0" 1);
+ by (Blast_tac 2);
+by (subgoal_tac "Finite(UN i:B. C(i)) & Finite(C(x)) & Finite(B)" 1);
+by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1);
+by (auto_tac (claset() addIs [Finite_Union, Finite_RepFun], simpset()));
+qed_spec_mp "setsum_UN_disjoint";
+
+
+Goal "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)";
+by (case_tac "Finite(C)" 1);
+by (asm_simp_tac (simpset() addsimps [setsum_def]) 2);
+by (etac Finite_induct 1);
+by Auto_tac;
+qed "setsum_addf";
+
+
+val major::prems = Goal
+ "[| A=B; !!x. x:B ==> f(x) = g(x) |] ==> \
+\ setsum(f, A) = setsum(g, B)";
+by (case_tac "Finite(B)" 1);
+by (asm_simp_tac (simpset() addsimps [setsum_def, major]) 2);
+by (subgoal_tac "ALL C. C <= B --> (ALL x:C. f(x) = g(x)) \
+ \ --> setsum(f,C) = setsum(g, C)" 1);
+by (cut_facts_tac [major] 1);
+ by (asm_full_simp_tac (simpset() addsimps [major]@prems) 1);
+by (etac Finite_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (subgoal_tac "C=0" 1);
+by (Force_tac 1);
+by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [major,subset_cons_iff]@prems) 1);
+by Safe_tac;
+by (forward_tac [subset_Finite] 1);
+by (assume_tac 1);
+by (Blast_tac 1);
+by (forward_tac [subset_Finite] 1);
+by (assume_tac 1);
+by (subgoal_tac "C = cons(x, C - {x})" 1);
+by (Blast_tac 2);
+by (etac ssubst 1);
+by (dtac spec 1);
+by (mp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [Ball_def, major]@prems) 1);
+qed_spec_mp "setsum_cong";
+
+(** For the natural numbers, we have subtraction **)
+
+Goal "[| Finite(A); Finite(B) |] \
+\ ==> setsum(f, A Un B) = \
+\ setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)";
+by (stac (setsum_Un_Int RS sym) 1);
+by Auto_tac;
+qed "setsum_Un";
+
+
+Goal "Finite(A) ==> (ALL x:A. g(x) $<= #0) --> setsum(g, A) $<= #0";
+by (etac Finite_induct 1);
+by (auto_tac (claset() addIs [zneg_or_0_add_zneg_or_0_imp_zneg_or_0], simpset()));
+qed_spec_mp "setsum_zneg_or_0";
+
+Goal "Finite(A) \
+\ ==> ALL n:nat. setsum(f,A) = $# succ(n) --> (EX a:A. #0 $< f(a))";
+by (etac Finite_induct 1);
+by (auto_tac (claset(), simpset()
+ delsimps [int_of_0, int_of_succ]
+ addsimps [not_zless_iff_zle, int_of_0 RS sym]));
+by (subgoal_tac "setsum(f, B) $<= #0" 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (blast_tac (claset() addIs [setsum_zneg_or_0]) 2);
+by (subgoal_tac "$# 1 $<= f(x) $+ setsum(f, B)" 1);
+by (dtac (zdiff_zle_iff RS iffD2) 1);
+by (subgoal_tac "$# 1 $<= $# 1 $- setsum(f,B)" 1);
+by (dres_inst_tac [("x", "$# 1")] zle_trans 1);
+by (res_inst_tac [("j", "#1")] zless_zle_trans 2);
+by Auto_tac;
+qed "setsum_succD_lemma";
+
+Goal "[| setsum(f, A) = $# succ(n); n:nat |]==> EX a:A. #0 $< f(a)";
+by (case_tac "Finite(A)" 1);
+by (blast_tac (claset()
+ addIs [setsum_succD_lemma RS bspec RS mp]) 1);
+by (rewrite_goals_tac [setsum_def]);
+by (auto_tac (claset(),
+ simpset() delsimps [int_of_0, int_of_succ]
+ addsimps [int_succ_int_1 RS sym, int_of_0 RS sym]));
+qed "setsum_succD";
+
+Goal "Finite(A) ==> (ALL x:A. #0 $<= g(x)) --> #0 $<= setsum(g, A)";
+by (etac Finite_induct 1);
+by (Simp_tac 1);
+by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset()));
+qed_spec_mp "g_zpos_imp_setsum_zpos";
+
+Goal "[| Finite(A); ALL x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)";
+by (etac Finite_induct 1);
+by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset()));
+qed_spec_mp "g_zpos_imp_setsum_zpos2";
+
+Goal "Finite(A) \
+\ ==> (ALL x:A. #0 $< g(x)) --> A ~= 0 --> (#0 $< setsum(g, A))";
+by (etac Finite_induct 1);
+by (auto_tac (claset() addIs [zspos_add_zspos_imp_zspos],simpset()));
+qed_spec_mp "g_zspos_imp_setsum_zspos";
+
+Goal "Finite(A) \
+\ ==> ALL a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})";
+by (etac Finite_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (Simp_tac 1);
+by (case_tac "x=a" 1);
+by (subgoal_tac "cons(x, B) - {a} = cons(x, B -{a}) & Finite(B - {a})" 2);
+by (subgoal_tac "cons(a, B) - {a} = B" 1);
+by (auto_tac (claset() addIs [Finite_Diff], simpset()));
+qed_spec_mp "setsum_Diff";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Multiset.ML Wed Nov 07 18:12:12 2001 +0100
@@ -0,0 +1,1515 @@
+(* Title: ZF/UNITY/Multiset.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+
+A definitional theory of multisets, including a wellfoundedness
+proof for the multiset order.
+
+The theory features ordinal multisets and the usual ordering.
+
+*)
+
+Addsimps [domain_of_fun];
+Delrules [domainE];
+
+(* The following tactic moves the condition `simp_cond' to the begining
+ of the list of hypotheses and then makes simplifications accordingly *)
+
+fun rotate_simp_tac simp_cond i =
+(dres_inst_tac [("psi", simp_cond)] asm_rl i THEN rotate_tac ~1 i
+ THEN Asm_full_simp_tac i);
+
+(* A useful simplification rule *)
+
+Goal "(f:A -> nat-{0}) <-> f:A->nat&(ALL a:A. f`a:nat & 0 < f`a)";
+by Safe_tac;
+by (res_inst_tac [("B1", "range(f)")] (Pi_mono RS subsetD) 4);
+by (auto_tac (claset() addSIs [Ord_0_lt]
+ addDs [apply_type, Diff_subset RS Pi_mono RS subsetD],
+ simpset() addsimps [range_of_fun, apply_iff]));
+qed "multiset_fun_iff";
+
+(** multiset and multiset_on **)
+
+Goalw [multiset_on_def, multiset_def]
+"multiset[A](M) ==> multiset(M)";
+by Auto_tac;
+qed "multiset_on_imp_multiset";
+
+Goalw [multiset_on_def, multiset_def]
+"multiset(M) ==> multiset[mset_of(M)](M)";
+by Auto_tac;
+qed "multiset_imp_multiset_on_set_of";
+
+Goal "multiset(M) <-> multiset[mset_of(M)](M)";
+by (blast_tac (claset() addIs [multiset_on_imp_multiset,
+ multiset_imp_multiset_on_set_of]) 1);
+qed "multiset_iff_multiset_on_set_of";
+
+Goalw [multiset_on_def]
+ "[| A<= B; multiset[A](M) |] ==> multiset[B](M)";
+by Auto_tac;
+qed "subset_multiset_on";
+
+(* the empty multiset is 0 *)
+
+Goalw [multiset_def, mset_of_def]
+ "multiset(0)";
+by Auto_tac;
+by (res_inst_tac [("x", "0")] exI 1);
+by (simp_tac (simpset() addsimps [Finite_0]) 1);
+qed "multiset_0";
+AddIffs [multiset_0];
+
+(** mset_of **)
+
+Goalw [multiset_def, mset_of_def]
+"multiset(M) ==> Finite(mset_of(M))";
+by Auto_tac;
+qed "multiset_set_of_Finite";
+Addsimps [multiset_set_of_Finite];
+
+Goalw [mset_of_def]
+"mset_of(0) = 0";
+by Auto_tac;
+qed "mset_of_0";
+AddIffs [mset_of_0];
+
+Goalw [multiset_def, mset_of_def]
+"multiset(M) ==> mset_of(M)=0 <-> M=0";
+by Auto_tac;
+qed "mset_is_0_iff";
+
+Goalw [msingle_def, mset_of_def]
+ "mset_of({#a#}) = {a}";
+by Auto_tac;
+qed "mset_of_single";
+AddIffs [mset_of_single];
+
+Goalw [mset_of_def, munion_def]
+ "mset_of(M +# N) = mset_of(M) Un mset_of(N)";
+by Auto_tac;
+qed "mset_of_union";
+AddIffs [mset_of_union];
+
+Goalw [multiset_def]
+"multiset(M) ==> \
+\ k:mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k~= a & k:mset_of(M))";
+by (rewrite_goals_tac [normalize_def, mset_of_def, msingle_def,
+ mdiff_def, mcount_def]);
+by (auto_tac (claset() addDs [domain_type]
+ addIs [zero_less_diff RS iffD1],
+ simpset() addsimps
+ [multiset_fun_iff, apply_iff]));
+qed "melem_diff_single";
+
+Goalw [mdiff_def, multiset_def]
+ "[| multiset(M); mset_of(M)<=A |] ==> mset_of(M -# N) <= A";
+by (auto_tac (claset(), simpset() addsimps [normalize_def]));
+by (rewrite_goals_tac [mset_of_def]);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(rotate_simp_tac "M:?u"));
+by Auto_tac;
+qed "mset_of_diff";
+Addsimps [mset_of_diff];
+
+(* msingle *)
+
+Goalw [msingle_def]
+ "{#a#} ~= 0 & 0 ~= {#a#}";
+by Auto_tac;
+qed "msingle_not_0";
+AddIffs [msingle_not_0];
+
+Goalw [msingle_def]
+ "({#a#} = {#b#}) <-> (a = b)";
+by (auto_tac (claset() addEs [equalityE], simpset()));
+qed "msingle_eq_iff";
+AddIffs [msingle_eq_iff];
+
+Goalw [multiset_def, msingle_def] "multiset({#a#})";
+by (res_inst_tac [("x", "{a}")] exI 1);
+by (auto_tac (claset() addIs [Finite_cons, Finite_0,
+ fun_extend3], simpset()));
+qed "msingle_multiset";
+AddIffs [msingle_multiset];
+
+(** normalize **)
+
+Goalw [normalize_def, restrict_def, mset_of_def]
+ "normalize(normalize(f)) = normalize(f)";
+by Auto_tac;
+qed "normalize_idem";
+AddIffs [normalize_idem];
+
+Goalw [multiset_def]
+ "multiset(M) ==> normalize(M) = M";
+by (rewrite_goals_tac [normalize_def, mset_of_def]);
+by (auto_tac (claset(), simpset()
+ addsimps [restrict_def, multiset_fun_iff]));
+qed "normalize_multiset";
+Addsimps [normalize_multiset];
+
+Goalw [multiset_def, multiset_on_def]
+"[| f:A -> nat; Finite(A) |] ==> multiset(normalize(f))";
+by (rewrite_goals_tac [normalize_def, mset_of_def]);
+by Auto_tac;
+by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
+by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
+ restrict_type], simpset()));
+qed "normalize_multiset";
+
+(** Typechecking rules for union and difference of multisets **)
+
+Goal "[| n:nat; m:nat |] ==> 0 < m #+ n <-> (0 < m | 0 < n)";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed "zero_less_add";
+
+(* union *)
+
+Goalw [multiset_def]
+"[| multiset(M); multiset(N) |] ==> multiset(M +# N)";
+by (rewrite_goals_tac [munion_def, mset_of_def]);
+by Auto_tac;
+by (res_inst_tac [("x", "A Un Aa")] exI 1);
+by (auto_tac (claset() addSIs [lam_type] addIs [Finite_Un],
+ simpset() addsimps [multiset_fun_iff, zero_less_add]));
+qed "munion_multiset";
+Addsimps [munion_multiset];
+
+(* difference *)
+
+Goalw [mdiff_def]
+"multiset(M) ==> multiset(M -# N)";
+by (res_inst_tac [("A", "mset_of(M)")] normalize_multiset 1);
+by (asm_simp_tac (simpset() addsimps [multiset_set_of_Finite]) 2);
+by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def]));
+by (auto_tac (claset() addSIs [lam_type],
+ simpset() addsimps [multiset_fun_iff]));
+qed "mdiff_multiset";
+Addsimps [mdiff_multiset];
+
+(** Algebraic properties of multisets **)
+
+(* Union *)
+
+Goalw [multiset_def]
+ "multiset(M) ==> M +# 0 = M & 0 +# M = M";
+by (auto_tac (claset(), simpset() addsimps [munion_def, mset_of_def]));
+qed "munion_0";
+Addsimps [munion_0];
+
+Goalw [multiset_def]
+ "[| multiset(M); multiset(N) |] ==> M +# N = N +# M";
+by (rewrite_goals_tac [munion_def, mset_of_def]);
+by (auto_tac (claset() addSIs [lam_cong], simpset()));
+qed "munion_commute";
+
+Goalw [multiset_def]
+"[|multiset(M); multiset(N); multiset(K)|] ==> (M +# N) +# K = M +# (N +# K)";
+by (rewrite_goals_tac [munion_def, mset_of_def]);
+by (rtac lam_cong 1);
+by Auto_tac;
+qed "munion_assoc";
+
+Goalw [multiset_def]
+"[|multiset(M); multiset(N); multiset(K)|]==> M +# (N +# K) = N +# (M +# K)";
+by (rewrite_goals_tac [munion_def, mset_of_def]);
+by (rtac lam_cong 1);
+by Auto_tac;
+qed "munion_lcommute";
+
+val munion_ac = [munion_commute, munion_assoc, munion_lcommute];
+
+(* Difference *)
+
+Goalw [mdiff_def] "M -# M = 0";
+by (simp_tac (simpset() addsimps
+ [diff_self_eq_0, normalize_def, mset_of_def]) 1);
+qed "mdiff_self_eq_0";
+AddIffs [mdiff_self_eq_0];
+
+Goalw [multiset_def] "multiset(M) ==> M -# 0 = M & 0 -# M = 0";
+by (rewrite_goals_tac [mdiff_def, normalize_def]);
+by (auto_tac (claset(), simpset()
+ addsimps [multiset_fun_iff, mset_of_def, restrict_def]));
+qed "mdiff_0";
+Addsimps [mdiff_0];
+
+Goalw [multiset_def] "multiset(M) ==> M +# {#a#} -# {#a#} = M";
+by (rewrite_goals_tac [munion_def, mdiff_def,
+ msingle_def, normalize_def, mset_of_def]);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (resolve_tac [fun_extension] 1);
+by Auto_tac;
+by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1);
+by (rtac restrict_type 2);
+by (rtac equalityI 1);
+by (ALLGOALS(Clarify_tac));
+by Auto_tac;
+by (res_inst_tac [("Pa", "~(1<?u)")] swap 1);
+by (case_tac "x=a" 3);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "mdiff_union_inverse2";
+Addsimps [mdiff_union_inverse2];
+
+(** Count of elements **)
+
+Goalw [multiset_def] "multiset(M) ==> mcount(M, a):nat";
+by (rewrite_goals_tac [mcount_def, mset_of_def]);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+qed "mcount_type";
+AddIs [mcount_type];
+Addsimps [mcount_type];
+
+Goalw [mcount_def] "mcount(0, a) = 0";
+by Auto_tac;
+qed "mcount_0";
+AddIffs [mcount_0];
+
+Goalw [mcount_def, mset_of_def, msingle_def]
+"mcount({#b#}, a) = (if a=b then 1 else 0)";
+by Auto_tac;
+qed "mcount_single";
+Addsimps [mcount_single];
+
+Goalw [multiset_def]
+"[| multiset(M); multiset(N) |] \
+\ ==> mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)";
+by (auto_tac (claset(), simpset() addsimps
+ [multiset_fun_iff, mcount_def,
+ munion_def, mset_of_def ]));
+qed "mcount_union";
+Addsimps [mcount_union];
+
+Goalw [multiset_def]
+"[| multiset(M); multiset(N) |] \
+\ ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)";
+by (auto_tac (claset() addSDs [not_lt_imp_le],
+ simpset() addsimps [mdiff_def, multiset_fun_iff,
+ mcount_def, normalize_def, mset_of_def]));
+qed "mcount_diff";
+Addsimps [mcount_diff];
+
+Goalw [multiset_def]
+ "[| multiset(M); a:mset_of(M) |] ==> 0 < mcount(M, a)";
+by (Clarify_tac 1);
+by (rewrite_goals_tac [mcount_def, mset_of_def]);
+by (rotate_simp_tac "M:?u" 1);
+by (asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]) 1);
+qed "mcount_elem";
+
+(** msize **)
+
+Goalw [msize_def] "msize(0) = #0";
+by Auto_tac;
+qed "msize_0";
+AddIffs [msize_0];
+
+Goalw [msize_def] "msize({#a#}) = #1";
+by (rewrite_goals_tac [msingle_def, mcount_def, mset_of_def]);
+by (auto_tac (claset(), simpset() addsimps [Finite_0]));
+qed "msize_single";
+AddIffs [msize_single];
+
+Goalw [msize_def] "msize(M):int";
+by Auto_tac;
+qed "msize_type";
+Addsimps [msize_type];
+AddTCs [msize_type];
+AddIs [msize_type];
+
+
+Goalw [msize_def] "multiset(M)==> #0 $<= msize(M)";
+by (auto_tac (claset() addIs [g_zpos_imp_setsum_zpos], simpset()));
+qed "msize_zpositive";
+
+Goal "multiset(M) ==> EX n:nat. msize(M)= $# n";
+by (rtac not_zneg_int_of 1);
+by (ALLGOALS(asm_simp_tac
+ (simpset() addsimps [msize_type RS znegative_iff_zless_0,
+ not_zless_iff_zle,msize_zpositive])));
+qed "msize_int_of_nat";
+
+Goalw [multiset_def]
+ "[| M~=0; multiset(M) |] ==> EX a:mset_of(M). 0 < mcount(M, a)";
+by (etac not_emptyE 1);
+by (rewrite_goal_tac [mset_of_def, mcount_def] 1);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (blast_tac (claset() addSDs [fun_is_rel]) 1);
+qed "not_empty_multiset_imp_exist";
+
+Goalw [msize_def] "multiset(M) ==> msize(M)=#0 <-> M=0";
+by Auto_tac;
+by (res_inst_tac [("Pa", "setsum(?u,?v) ~= #0")] swap 1);
+by (Blast_tac 1);
+by (dtac not_empty_multiset_imp_exist 1);
+by (ALLGOALS(Clarify_tac));
+by (subgoal_tac "Finite(mset_of(M) - {a})" 1);
+by (asm_simp_tac (simpset() addsimps [Finite_Diff]) 2);
+by (subgoal_tac "setsum(%x. $# mcount(M, x), cons(a, mset_of(M)-{a}))=#0" 1);
+by (asm_simp_tac (simpset() addsimps [cons_Diff]) 2);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "#0 $<= setsum(%x. $# mcount(M, x), mset_of(M) - {a})" 1);
+by (rtac g_zpos_imp_setsum_zpos 2);
+by (auto_tac (claset(), simpset()
+ addsimps [Finite_Diff, not_zless_iff_zle RS iff_sym,
+ znegative_iff_zless_0 RS iff_sym]));
+by (dtac (rotate_prems 1 not_zneg_int_of) 1);
+by (auto_tac (claset(), simpset() delsimps [int_of_0]
+ addsimps [int_of_add RS sym, int_of_0 RS sym]));
+qed "msize_eq_0_iff";
+
+Goal
+"cons(x, A) Int B = (if x:B then cons(x, A Int B) else A Int B)";
+by Auto_tac;
+qed "cons_Int_right_cases";
+
+Goal
+"Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N)) \
+\ = setsum(%a. $# mcount(N, a), A)";
+by (etac Finite_induct 1);
+by Auto_tac;
+by (subgoal_tac "Finite(B Int mset_of(N))" 1);
+by (blast_tac (claset() addIs [subset_Finite]) 2);
+by (auto_tac (claset(),
+ simpset() addsimps [mcount_def, cons_Int_right_cases]));
+qed "setsum_mcount_Int";
+
+Goalw [msize_def]
+"[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)";
+by (asm_simp_tac (simpset() addsimps
+ [setsum_Un , setsum_addf, int_of_add, setsum_mcount_Int]) 1);
+by (stac Int_commute 1);
+by (asm_simp_tac (simpset() addsimps [setsum_mcount_Int]) 1);
+qed "msize_union";
+Addsimps [msize_union];
+
+Goalw [msize_def] "[|msize(M)= $# succ(n); n:nat|] ==> EX a. a:mset_of(M)";
+by (blast_tac (claset() addDs [setsum_succD]) 1);
+qed "msize_eq_succ_imp_elem";
+
+(** Equality of multisets **)
+
+Goalw [multiset_def]
+"[| multiset(M); multiset(N); ALL a. mcount(M, a)=mcount(N, a) |] \
+\ ==> mset_of(M)=mset_of(N)";
+by (rtac sym 1 THEN rtac equalityI 1);
+by (rewrite_goals_tac [mcount_def, mset_of_def]);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (ALLGOALS(rotate_simp_tac "M:?u"));
+by (ALLGOALS(rotate_simp_tac "N:?u"));
+by (ALLGOALS(dres_inst_tac [("x", "x")] spec));
+by (case_tac "x:Aa" 2 THEN case_tac "x:A" 1);
+by Auto_tac;
+qed "equality_lemma";
+
+Goal
+"[| multiset(M); multiset(N) |]==> M=N<->(ALL a. mcount(M, a)=mcount(N, a))";
+by Auto_tac;
+by (subgoal_tac "mset_of(M) = mset_of(N)" 1);
+by (blast_tac (claset() addIs [equality_lemma]) 2);
+by (rewrite_goals_tac [multiset_def, mset_of_def]);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (rotate_simp_tac "M:?u" 1);
+by (rotate_simp_tac "N:?u" 1);
+by (rtac fun_extension 1);
+by (Blast_tac 1 THEN Blast_tac 1);
+by (dres_inst_tac [("x", "x")] spec 1);
+by (auto_tac (claset(), simpset() addsimps [mcount_def, mset_of_def]));
+qed "multiset_equality";
+
+(** More algebraic properties of multisets **)
+
+Goal "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)";
+by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
+qed "munion_eq_0_iff";
+Addsimps [munion_eq_0_iff];
+
+Goal "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)";
+by (rtac iffI 1 THEN dtac sym 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_equality])));
+qed "empty_eq_munion_iff";
+Addsimps [empty_eq_munion_iff];
+
+Goal
+"[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)";
+by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
+qed "munion_right_cancel";
+Addsimps [munion_right_cancel];
+
+Goal
+"[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)";
+by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
+qed "munion_left_cancel";
+Addsimps [munion_left_cancel];
+
+Goal "[| m:nat; n:nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)";
+by (induct_tac "n" 1 THEN Auto_tac);
+qed "nat_add_eq_1_cases";
+
+Goal "[|multiset(M); multiset(N)|] \
+\ ==> (M +# N = {#a#}) <-> (M={#a#} & N=0) | (M = 0 & N = {#a#})";
+by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
+by Safe_tac;
+by (ALLGOALS(Asm_full_simp_tac));
+by (case_tac "aa=a" 1);
+by (dres_inst_tac [("x", "aa")] spec 2);
+by (dres_inst_tac [("x", "a")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases]) 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "aaa=aa" 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x", "aa")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases]) 1);
+by (case_tac "aaa=a" 1);
+by (dres_inst_tac [("x", "aa")] spec 4);
+by (dres_inst_tac [("x", "a")] spec 3);
+by (dres_inst_tac [("x", "aaa")] spec 2);
+by (dres_inst_tac [("x", "aa")] spec 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases])));
+qed "munion_is_single";
+
+Goal "[| multiset(M); multiset(N) |] \
+\ ==> ({#a#} = M +# N) <-> ({#a#} = M & N=0 | M = 0 & {#a#} = N)";
+by (simp_tac (simpset() addsimps [sym]) 1);
+by (subgoal_tac "({#a#} = M +# N) <-> (M +# N = {#a#})" 1);
+by (asm_simp_tac (simpset() addsimps [munion_is_single]) 1);
+by (REPEAT(blast_tac (claset() addDs [sym]) 1));
+qed "msingle_is_union";
+
+(** Towards induction over multisets **)
+
+Goalw [multiset_def]
+"Finite(A) \
+\ ==> (ALL M. multiset(M) --> \
+\ (ALL a:mset_of(M). setsum(%x. $# mcount(M(a:=M`a #- 1), x), A) = \
+\ (if a:A then setsum(%x. $# mcount(M, x), A) $- #1 \
+\ else setsum(%x. $# mcount(M, x), A))))";
+by (etac Finite_induct 1);
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (rewrite_goals_tac [mset_of_def, mcount_def]);
+by (case_tac "x:A" 1);
+by Auto_tac;
+by (rotate_simp_tac "M:?u" 2);
+by (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1" 1);
+by (etac ssubst 1);
+by (rtac int_of_diff 1);
+by Auto_tac;
+qed "setsum_decr";
+
+(*FIXME: we should not have to rename x to x' below! There's a bug in the
+ interaction between simproc inteq_cancel_numerals and the simplifier.*)
+Goalw [multiset_def]
+ "Finite(A) \
+\ ==> ALL M. multiset(M) --> (ALL a:mset_of(M). \
+\ setsum(%x'. $# mcount(restrict(M, mset_of(M)-{a}), x'), A) = \
+\ (if a:A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a \
+\ else setsum(%x'. $# mcount(M, x'), A)))";
+by (etac Finite_induct 1);
+by (auto_tac (claset(),
+ simpset() addsimps [multiset_fun_iff,
+ mcount_def, mset_of_def]));
+qed "setsum_decr2";
+
+Goal "[| Finite(A); multiset(M); a:mset_of(M) |] \
+\ ==> setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}), x), A - {a}) = \
+\ (if a:A then setsum(%x. $# mcount(M, x), A) $- $# M`a\
+\ else setsum(%x. $# mcount(M, x), A))";
+by (subgoal_tac "setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A-{a}) = \
+\ setsum(%x. $# mcount(restrict(M, mset_of(M)-{a}),x),A)" 1);
+by (rtac (setsum_Diff RS sym) 2);
+by (REPEAT(asm_simp_tac (simpset() addsimps [mcount_def, mset_of_def]) 2));
+by (rtac sym 1 THEN rtac ssubst 1);
+by (Blast_tac 1);
+by (rtac sym 1 THEN dtac setsum_decr2 1);
+by Auto_tac;
+qed "setsum_decr3";
+
+Goal "n:nat ==> n le 1 <-> (n=0 | n=1)";
+by (auto_tac (claset() addEs [natE], simpset()));
+qed "nat_le_1_cases";
+
+Goal "[| 0<n; n:nat |] ==> succ(n #- 1) = n";
+by (subgoal_tac "1 le n" 1);
+by (dtac add_diff_inverse2 1);
+by Auto_tac;
+qed "succ_pred_eq_self";
+
+val major::prems = Goal
+ "[| n:nat; P(0); \
+\ (!!M a. [| multiset(M); a~:mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))); \
+\ (!!M b. [| multiset(M); b:mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))) |] \
+ \ ==> (ALL M. multiset(M)--> \
+\ (setsum(%x. $# mcount(M, x), {x:mset_of(M). 0 < M`x}) = $# n) --> P(M))";
+by (rtac (major RS nat_induct) 1);
+by (ALLGOALS(Clarify_tac));
+by (forward_tac [msize_eq_0_iff] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [mset_of_def, multiset_def,
+ multiset_fun_iff, msize_def]@prems));
+by (rotate_simp_tac "M:?u" 1);
+by (rotate_simp_tac "M:?u" 2);
+by (rotate_simp_tac "ALL a:A. ?u(a)" 1);
+by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1);
+by (dtac setsum_succD 1 THEN Auto_tac);
+by (case_tac "1 <M`xa" 1);
+by (dtac not_lt_imp_le 2);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_le_1_cases])));
+by (subgoal_tac "M=(M(xa:=M`xa #- 1))(xa:=(M(xa:=M`xa #- 1))`xa #+ 1)" 1);
+by (res_inst_tac [("A","A"),("B","%x. nat"),("D","%x. nat")] fun_extension 2);
+by (REPEAT(rtac update_type 3));
+by (ALLGOALS(Asm_simp_tac));
+by (Clarify_tac 2);
+by (rtac (succ_pred_eq_self RS sym) 2);
+by (ALLGOALS(Asm_simp_tac));
+by (rtac subst 1 THEN rtac sym 1 THEN Blast_tac 1 THEN resolve_tac prems 1);
+by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
+by (res_inst_tac [("x", "A")] exI 1);
+by (force_tac (claset() addIs [update_type], simpset()) 1);
+by (asm_simp_tac (simpset() addsimps [mset_of_def, mcount_def]) 1);
+by (dres_inst_tac [("x", "M(xa := M ` xa #- 1)")] spec 1);
+by (dtac mp 1 THEN dtac mp 2);
+by (ALLGOALS(Asm_full_simp_tac));
+by (res_inst_tac [("x", "A")] exI 1);
+by (auto_tac (claset() addIs [update_type], simpset()));
+by (subgoal_tac "Finite({x:cons(xa, A). x~=xa-->0<M`x})" 1);
+by (blast_tac(claset() addIs [Collect_subset RS subset_Finite,Finite_cons])2);
+by (dres_inst_tac [("A", "{x:cons(xa, A). x~=xa-->0<M`x}")] setsum_decr 1);
+by (dres_inst_tac [("x", "M")] spec 1);
+by (subgoal_tac "multiset(M)" 1);
+by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
+by (res_inst_tac [("x", "A")] exI 2);
+by (Force_tac 2);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [mset_of_def])));
+by (dres_inst_tac [("psi", "ALL x:A. ?u(x)")] asm_rl 1);
+by (dres_inst_tac [("x", "xa")] bspec 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "cons(xa, A)= A" 1);
+by (Blast_tac 2);
+by (rotate_simp_tac "cons(xa, A) = A" 1);
+by (rotate_simp_tac "ALL x:A. ?u(x)" 1);
+by (rotate_simp_tac "ALL x:A. ?u(x)" 2);
+by (subgoal_tac "M=cons(<xa, M`xa>, restrict(M, A-{xa}))" 1);
+by (rtac fun_cons_restrict_eq 2);
+by (subgoal_tac "cons(xa, A-{xa}) = A" 2);
+by (REPEAT(Force_tac 2));
+by (res_inst_tac [("a", "cons(<xa, 1>, restrict(M, A - {xa}))")] ssubst 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "multiset(restrict(M, A - {xa}))" 1);
+by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
+by (res_inst_tac [("x", "A-{xa}")] exI 2);
+by Safe_tac;
+by (res_inst_tac [("A", "A-{xa}")] apply_type 3);
+by (asm_simp_tac (simpset() addsimps [restrict]) 5);
+by (REPEAT(blast_tac (claset() addIs [Finite_Diff, restrict_type]) 2));;
+by (resolve_tac prems 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
+by (dres_inst_tac [("x", "restrict(M, A-{xa})")] spec 1);
+by (dtac mp 1);
+by (res_inst_tac [("x", "A-{xa}")] exI 1);
+by (auto_tac (claset() addIs [Finite_Diff, restrict_type],
+ simpset() addsimps [restrict]));
+by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "xa")] setsum_decr3 1);
+by (asm_simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
+by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
+by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
+by (ALLGOALS(rotate_simp_tac "ALL x:A. ?u(x)"));
+by (subgoal_tac "{x:A - {xa} . 0 < restrict(M, A - {x}) ` x} = A - {xa}" 1);
+by (auto_tac (claset() addSIs [setsum_cong],
+ simpset() addsimps [zdiff_eq_iff,
+ zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
+qed "multiset_induct_aux";
+
+val major::prems = Goal
+ "[| multiset(M); P(0); \
+\ (!!M a. [| multiset(M); a~:mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))); \
+\ (!!M b. [| multiset(M); b:mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))) |] \
+ \ ==> P(M)";
+by (subgoal_tac "EX n:nat. setsum(\\<lambda>x. $# mcount(M, x), \
+ \ {x : mset_of(M) . 0 < M ` x}) = $# n" 1);
+by (resolve_tac [not_zneg_int_of] 2);
+by (ALLGOALS(asm_simp_tac (simpset()
+ addsimps [znegative_iff_zless_0, not_zless_iff_zle])));
+by (rtac g_zpos_imp_setsum_zpos 2);
+by (blast_tac (claset() addIs [major RS multiset_set_of_Finite,
+ Collect_subset RS subset_Finite]) 2);
+by (asm_full_simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
+by (Clarify_tac 1);
+by (rtac (multiset_induct_aux RS spec RS mp RS mp) 1);
+by (resolve_tac prems 4);
+by (resolve_tac prems 3);
+by (auto_tac (claset(), simpset() addsimps major::prems));
+qed "multiset_induct2";
+
+Goalw [multiset_def, msingle_def]
+ "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)";
+by (auto_tac (claset(), simpset() addsimps [munion_def]));
+by (rewrite_goals_tac [mset_of_def]);
+by (rotate_simp_tac "M:?u" 1);
+by (rtac fun_extension 1 THEN rtac lam_type 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (auto_tac (claset(), simpset()
+ addsimps [multiset_fun_iff,
+ fun_extend_apply1,
+ fun_extend_apply2]));
+by (dres_inst_tac [("c", "a"), ("b", "1")] fun_extend3 1);
+by (stac Un_commute 3);
+by (auto_tac (claset(), simpset() addsimps [cons_eq]));
+qed "munion_single_case1";
+
+Goalw [multiset_def]
+"[| multiset(M); a:mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)";
+by (auto_tac (claset(), simpset()
+ addsimps [munion_def, multiset_fun_iff, msingle_def]));
+by (rewrite_goals_tac [mset_of_def]);
+by (rotate_simp_tac "M:?u" 1);
+by (subgoal_tac "A Un {a} = A" 1);
+by (rtac fun_extension 1);
+by (auto_tac (claset() addDs [domain_type]
+ addIs [lam_type, update_type], simpset()));
+qed "munion_single_case2";
+
+(* Induction principle for multisets *)
+
+val major::prems = Goal
+ "[| multiset(M); P(0); \
+\ (!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})) |] \
+ \ ==> P(M)";
+by (rtac multiset_induct2 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps major::prems)));
+by (forw_inst_tac [("a1", "b")] (munion_single_case2 RS sym) 2);
+by (forw_inst_tac [("a1", "a")] (munion_single_case1 RS sym) 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (REPEAT(blast_tac (claset() addIs prems ) 1));
+qed "multiset_induct";
+
+(** MCollect **)
+
+Goalw [MCollect_def, multiset_def, mset_of_def]
+ "multiset(M) ==> multiset({# x:M. P(x)#})";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "{x:A. P(x)}")] exI 1);
+by (auto_tac (claset() addDs [CollectD1 RSN (2,apply_type)]
+ addIs [Collect_subset RS subset_Finite,
+ restrict_type],
+ simpset()));
+qed "MCollect_multiset";
+Addsimps [MCollect_multiset];
+
+Goalw [mset_of_def, MCollect_def]
+ "multiset(M) ==> mset_of({# x:M. P(x) #}) <= mset_of(M)";
+by (auto_tac (claset(),
+ simpset() addsimps [multiset_def, restrict_def]));
+qed "mset_of_MCollect";
+Addsimps [mset_of_MCollect];
+
+Goalw [MCollect_def, mset_of_def]
+ "x:mset_of({#x:M. P(x)#}) <-> x:mset_of(M) & P(x)";
+by Auto_tac;
+qed "MCollect_mem_iff";
+AddIffs [MCollect_mem_iff];
+
+Goalw [mcount_def, MCollect_def, mset_of_def]
+ "mcount({# x:M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)";
+by Auto_tac;
+qed "mcount_MCollect";
+Addsimps [mcount_MCollect];
+
+Goal "multiset(M) ==> M = {# x:M. P(x) #} +# {# x:M. ~ P(x) #}";
+by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
+qed "multiset_partition";
+
+Goalw [multiset_def, mset_of_def]
+ "[| multiset(M); a:mset_of(M) |] ==> natify(M`a) = M`a";
+by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
+by (rotate_simp_tac "M:?u" 1);
+qed "natify_elem_is_self";
+Addsimps [natify_elem_is_self];
+
+(* and more algebraic laws on multisets *)
+
+Goal "[| multiset(M); multiset(N) |] \
+\ ==> (M +# {#a#} = N +# {#b#}) <-> (M = N & a = b | \
+\ M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})";
+by (asm_full_simp_tac (simpset() delsimps [mcount_single]
+ addsimps [multiset_equality]) 1);
+by (rtac iffI 1 THEN etac disjE 2 THEN etac conjE 3);
+by (case_tac "a=b" 1);
+by Auto_tac;
+by (dres_inst_tac [("x", "a")] spec 1);
+by (dres_inst_tac [("x", "b")] spec 2);
+by (dres_inst_tac [("x", "aa")] spec 3);
+by (dres_inst_tac [("x", "a")] spec 4);
+by Auto_tac;
+by (ALLGOALS(subgoal_tac "mcount(N,a):nat"));
+by (etac natE 3 THEN etac natE 1);
+by Auto_tac;
+qed "munion_eq_conv_diff";
+
+Goalw [multiset_on_def]
+"[| multiset[A](M); multiset[A](N) |] \
+\ ==> (M +# {#a#} = N +# {#b#}) <-> \
+\ (M=N & a=b | (EX K. multiset[A](K)& M= K +# {#b#} & N=K +# {#a#}))";
+by (auto_tac (claset(),
+ simpset() addsimps [melem_diff_single, munion_eq_conv_diff]));
+qed "munion_eq_conv_exist";
+
+(** multiset orderings **)
+
+(* multiset on a domain A are finite functions from A to nat-{0} *)
+
+Goalw [multiset_on_def, multiset_def]
+ "multiset[A](M) ==> M:A-||>nat-{0}";
+by (auto_tac (claset(), simpset()
+ addsimps [multiset_fun_iff, mset_of_def]));
+by (rotate_simp_tac "M:?u" 1);
+by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1);
+by (ALLGOALS(Asm_simp_tac));
+by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff])));
+qed "multiset_on_is_FiniteFun";
+
+Goalw [multiset_on_def, multiset_def, mset_of_def]
+ "M:A-||>nat-{0} ==> multiset[A](M)";
+by (forward_tac [FiniteFun_is_fun] 1);
+by (dtac FiniteFun_domain_Fin 1);
+by (forward_tac [FinD] 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "domain(M)")] exI 1);
+by (blast_tac (claset() addIs [Fin_into_Finite]) 1);
+qed "FiniteFun_is_multiset_on";
+
+Goal "M:A-||>nat-{0} <-> multiset[A](M)";
+by (blast_tac (claset() addDs [FiniteFun_is_multiset_on]
+ addIs [multiset_on_is_FiniteFun]) 1);
+qed "FiniteFun_iff_multiset_on";
+
+(* multirel1 type *)
+
+Goalw [multirel1_def]
+"multirel1(A, r) <= (A-||>nat-{0})*(A-||>nat-{0})";
+by Auto_tac;
+qed "multirel1_type";
+
+Goal "<M, N>:multirel1(A, r) ==> multiset[A](M) & multiset[A](N)";
+by (dtac (multirel1_type RS subsetD) 1);
+by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
+qed "multirel1D";
+
+Goalw [multirel1_def] "multirel1(0, r) =0";
+by Auto_tac;
+qed "multirel1_0";
+AddIffs [multirel1_0];
+
+Goalw [multirel1_def, Ball_def, Bex_def]
+" <N, M>:multirel1(A, r) <-> \
+\ (EX a. a:A & \
+\ (EX M0. multiset[A](M0) & (EX K. multiset[A](K) & \
+\ M=M0 +# {#a#} & N=M0 +# K & (ALL b:mset_of(K). <b,a>:r))))";
+by (auto_tac (claset(), simpset()
+ addsimps [FiniteFun_iff_multiset_on, multiset_on_def]));
+qed "multirel1_iff";
+
+(* Monotonicity of multirel1 *)
+
+Goalw [multirel1_def] "A<=B ==> multirel1(A, r)<=multirel1(B, r)";
+by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on]));
+by (ALLGOALS(asm_full_simp_tac(simpset()
+ addsimps [Un_subset_iff, multiset_on_def])));
+by (res_inst_tac [("x", "x")] bexI 3);
+by (res_inst_tac [("x", "xb")] bexI 3);
+by (Asm_simp_tac 3);
+by (res_inst_tac [("x", "xc")] bexI 3);
+by (ALLGOALS(asm_simp_tac (simpset()
+ addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
+by Auto_tac;
+qed "multirel1_mono1";
+
+Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)";
+by (auto_tac (claset(), simpset() addsimps [FiniteFun_iff_multiset_on]));
+by (res_inst_tac [("x", "x")] bexI 1);
+by (res_inst_tac [("x", "xb")] bexI 1);
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [FiniteFun_iff_multiset_on, multiset_on_def])));
+by (res_inst_tac [("x", "xc")] bexI 1);
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [FiniteFun_iff_multiset_on,multiset_on_def])));
+by Auto_tac;
+qed "multirel1_mono2";
+
+Goal
+ "[| A<=B; r<=s |] ==> multirel1(A, r) <= multirel1(B, s)";
+by (rtac subset_trans 1);
+by (rtac multirel1_mono1 1);
+by (rtac multirel1_mono2 2);
+by Auto_tac;
+qed "multirel1_mono";
+
+(* Towards the proof of well-foundedness of multirel1 *)
+
+Goalw [multirel1_def] "<M,0>~:multirel1(A, r)";
+by (auto_tac (claset(), simpset()
+ addsimps [FiniteFun_iff_multiset_on, multiset_on_def]));
+qed "not_less_0";
+AddIffs [not_less_0];
+
+Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); multiset[A](M0) |] ==> \
+\ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
+\ (EX K. multiset[A](K) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
+by (forward_tac [multirel1D] 1);
+by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1);
+by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist]));
+by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI));
+by Auto_tac;
+by (rewrite_goals_tac [multiset_on_def]);
+by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1);
+by (auto_tac (claset(), simpset() addsimps [munion_commute]));
+qed "less_munion";
+
+Goal "[| multiset[A](M); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
+by (auto_tac (claset(), simpset() addsimps [multirel1_iff]));
+by (rewrite_goals_tac [multiset_on_def]);
+by (res_inst_tac [("x", "a")] exI 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "M")] exI 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("x", "0")] exI 1);
+by Auto_tac;
+qed "multirel1_base";
+
+Goal "acc(0)=0";
+by (auto_tac (claset() addSIs [equalityI]
+ addDs [acc.dom_subset RS subsetD], simpset()));
+qed "acc_0";
+
+Goal "[| ALL b:A. <b,a>:r --> \
+\ (ALL M:acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r))); \
+\ M0:acc(multirel1(A, r)); a:A; \
+\ ALL M. <M,M0> : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \
+\ ==> M0 +# {#a#} : acc(multirel1(A, r))";
+by (subgoal_tac "multiset[A](M0)" 1);
+by (etac acc.elim 2);
+by (etac fieldE 2);
+by (REPEAT(blast_tac (claset() addDs [multirel1D]) 2));
+by (rtac accI 1);
+by (rename_tac "N" 1);
+by (dtac less_munion 1);
+by (Blast_tac 1);
+by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
+by (eres_inst_tac [("P", "ALL x:mset_of(K). <x, a>:r")] rev_mp 1);
+by (eres_inst_tac [("P", "mset_of(K)<=A")] rev_mp 1);
+by (eres_inst_tac [("M", "K")] multiset_induct 1);
+(* three subgoals *)
+(* subgoal 1: the induction base case *)
+by (Asm_simp_tac 1);
+(* subgoal 2: the induction general case *)
+by (asm_full_simp_tac (simpset() addsimps [Ball_def, Un_subset_iff]) 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "aa")] spec 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "aa:A" 1);
+by (Blast_tac 2);
+by (dres_inst_tac [("psi", "ALL x. x:acc(?u)-->?v(x)")] asm_rl 1);
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "M0 +# M")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1);
+(* subgoal 3: additional conditions *)
+by (auto_tac (claset() addSIs [multirel1_base RS fieldI2],
+ simpset() addsimps [multiset_on_def]));
+qed "lemma1";
+
+Goal "[| ALL b:A. <b,a>:r \
+\ --> (ALL M : acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r))); \
+\ M:acc(multirel1(A, r)); a:A|] ==> M +# {#a#} : acc(multirel1(A, r))";
+by (etac acc_induct 1);
+by (blast_tac (claset() addIs [lemma1]) 1);
+qed "lemma2";
+
+Goal
+ "[| wf[A](r); a:A |] ==> \
+\ ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
+by (eres_inst_tac [("a","a")] wf_on_induct 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [lemma2]) 1);
+qed "lemma3";
+
+Goal "multiset(M) ==> mset_of(M)<=A --> \
+\ wf[A](r) --> M:field(multirel1(A, r)) --> M:acc(multirel1(A, r))";
+by (etac multiset_induct 1);
+by (ALLGOALS(Clarify_tac));
+(* proving the base case *)
+by (rtac accI 1);
+by (cut_inst_tac [("M", "b"), ("r", "r")] not_less_0 1);
+by (Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [multirel1_def]) 1);
+(* Proving the general case *)
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "mset_of(M)<=A" 1);
+by (Blast_tac 2);
+by (Clarify_tac 1);
+by (dres_inst_tac [("a", "a")] lemma3 1);
+by (Blast_tac 1);
+by (subgoal_tac "M:field(multirel1(A,r))" 1);
+by (rtac (multirel1_base RS fieldI1) 2);
+by (rewrite_goal_tac [multiset_on_def] 2);
+by (REPEAT(Blast_tac 1));
+qed "lemma4";
+
+Goal "[| wf[A](r); multiset[A](M); A ~= 0|] ==> M:acc(multirel1(A, r))";
+by (etac not_emptyE 1);
+by (rtac (lemma4 RS mp RS mp RS mp) 1);
+by (rtac (multirel1_base RS fieldI1) 4);
+by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
+qed "all_accessible";
+
+Goal "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))";
+by (case_tac "A=0" 1);
+by (Asm_simp_tac 1);
+by (rtac wf_imp_wf_on 1);
+by (rtac wf_on_field_imp_wf 1);
+by (asm_simp_tac (simpset() addsimps [wf_on_0]) 1);
+by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1);
+by (rtac wf_on_acc 1);
+by (Clarify_tac 1);
+by (full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
+by (blast_tac (claset() addIs [all_accessible]) 1);
+qed "wf_on_multirel1";
+
+Goal "wf(r) ==>wf(multirel1(field(r), r))";
+by (full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
+by (dtac wf_on_multirel1 1);
+by (res_inst_tac [("A", "field(r) -||> nat - {0}")] wf_on_subset_A 1);
+by (Asm_simp_tac 1);
+by (rtac field_rel_subset 1);
+by (rtac multirel1_type 1);
+qed "wf_multirel1";
+
+(** multirel **)
+
+Goalw [multirel_def]
+ "multirel(A, r) <= (A-||>nat-{0}) * (A-||>nat-{0})";
+by (rtac (trancl_type RS subset_trans) 1);
+by (Clarify_tac 1);
+by (auto_tac (claset() addDs [multirel1D],
+ simpset() addsimps [FiniteFun_iff_multiset_on]));
+qed "multirel_type";
+
+Goal "<M, N>:multirel(A, r) ==> multiset[A](M) & multiset[A](N)";
+by (dtac (multirel_type RS subsetD) 1);
+by (asm_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on RS iff_sym]) 1);
+by Auto_tac;
+qed "multirelD";
+
+(* Monotonicity of multirel *)
+
+Goalw [multirel_def]
+ "[| A<=B; r<=s |] ==> multirel(A, r)<=multirel(B,s)";
+by (rtac trancl_mono 1);
+by (rtac multirel1_mono 1);
+by Auto_tac;
+qed "multirel_mono";
+
+(* Equivalence of multirel with the usual (closure-free) def *)
+
+Goal "k:nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)";
+by (etac nat_induct 1 THEN Auto_tac);
+qed "lemma";
+
+Goal "[|a:mset_of(J); multiset(I); multiset(J) |] \
+\ ==> I +# J -# {#a#} = I +# (J-# {#a#})";
+by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
+by (case_tac "a ~: mset_of(I)" 1);
+by (auto_tac (claset(), simpset() addsimps
+ [mcount_def, mset_of_def, multiset_def, multiset_fun_iff]));
+by (rotate_simp_tac "I:?u" 1);
+by (rotate_simp_tac "J:?u" 1);
+by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma]));
+qed "mdiff_union_single_conv";
+
+Goal
+"[| n le m; m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
+by (auto_tac (claset(), simpset() addsimps
+ [le_iff, diff_self_eq_0, less_iff_succ_add]));
+qed "diff_add_commute";
+
+(* One direction *)
+
+Goalw [multirel_def, Ball_def, Bex_def]
+"<M,N>:multirel(A, r) ==> \
+\ trans[A](r) --> \
+\ (EX I J K. \
+\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \
+\ N = I +# J & M = I +# K & J ~= 0 & \
+\ (ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r))";
+by (etac converse_trancl_induct 1);
+by (ALLGOALS(asm_full_simp_tac (simpset()
+ addsimps [multirel1_iff, multiset_on_def])));
+by (ALLGOALS(Clarify_tac));
+(* Two subgoals remain *)
+(* Subgoal 1 *)
+by (res_inst_tac [("x","M0")] exI 1);
+by (Force_tac 1);
+(* Subgoal 2 *)
+by (case_tac "a:mset_of(Ka)" 1);
+by (res_inst_tac [("x","I")] exI 1 THEN Asm_simp_tac 1);
+by (res_inst_tac [("x", "J")] exI 1 THEN Asm_simp_tac 1);
+by (res_inst_tac [("x","(Ka -# {#a#}) +# K")] exI 1 THEN Asm_simp_tac 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Un_subset_iff])));
+by (asm_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1);
+by (dres_inst_tac[("t","%M. M-#{#a#}")] subst_context 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [mdiff_union_single_conv, melem_diff_single]) 1);
+by (Clarify_tac 1);
+by (etac disjE 1);
+by (Asm_full_simp_tac 1);
+by (etac disjE 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("psi", "ALL x. x:#Ka -->?u(x)")] asm_rl 1);
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "a")] spec 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "xa")] exI 1);
+by (Asm_simp_tac 1);
+by (dres_inst_tac [("a", "x"), ("b", "a"), ("c", "xa")] trans_onD 1);
+by (ALLGOALS(Asm_simp_tac));
+by (Blast_tac 1);
+by (Blast_tac 1);
+(* new we know that a~:mset_of(Ka) *)
+by (subgoal_tac "a :# I" 1);
+by (res_inst_tac [("x","I-#{#a#}")] exI 1 THEN Asm_simp_tac 1);
+by (res_inst_tac [("x","J+#{#a#}")] exI 1);
+by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
+by (res_inst_tac [("x","Ka +# K")] exI 1);
+by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
+by (rtac conjI 1);
+by (asm_simp_tac (simpset() addsimps
+ [multiset_equality, mcount_elem RS succ_pred_eq_self]) 1);
+by (rtac conjI 1);
+by (dres_inst_tac[("t","%M. M-#{#a#}")] subst_context 1);
+by (asm_full_simp_tac (simpset() addsimps [mdiff_union_inverse2]) 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_equality])));
+by (rtac (diff_add_commute RS sym) 1);
+by (auto_tac (claset() addIs [mcount_elem], simpset()));
+by (subgoal_tac "a:mset_of(I +# Ka)" 1);
+by (dtac sym 2 THEN Auto_tac);
+qed "multirel_implies_one_step";
+
+Goal "[| a:mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M";
+by (asm_simp_tac (simpset()
+ addsimps [multiset_equality, mcount_elem RS succ_pred_eq_self]) 1);
+qed "melem_imp_eq_diff_union";
+Addsimps [melem_imp_eq_diff_union];
+
+Goal
+"[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
+\ ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
+by (dtac msize_eq_succ_imp_elem 1);
+by Auto_tac;
+by (res_inst_tac [("x", "a")] exI 1);
+by (res_inst_tac [("x", "M -# {#a#}")] exI 1);
+by (forward_tac [multiset_on_imp_multiset] 1);
+by (Asm_simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
+qed "msize_eq_succ_imp_eq_union";
+
+(* The second direction *)
+
+Goalw [multiset_on_def]
+"n:nat ==> \
+\ (ALL I J K. \
+\ multiset[A](I) & multiset[A](J) & multiset[A](K) & \
+\ (msize(J) = $# n & J ~=0 & (ALL k:mset_of(K). EX j:mset_of(J). <k, j>:r)) \
+\ --> <I +# K, I +# J>:multirel(A, r))";
+by (etac nat_induct 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("M", "J")] msize_eq_0_iff 1);
+by Auto_tac;
+(* one subgoal remains *)
+by (subgoal_tac "msize(J)=$# succ(x)" 1);
+by (Asm_simp_tac 2);
+by (forw_inst_tac [("A", "A")] msize_eq_succ_imp_eq_union 1);
+by (rewrite_goals_tac [multiset_on_def]);
+by (Clarify_tac 3 THEN rotate_tac ~1 3);
+by (ALLGOALS(Asm_full_simp_tac));
+by (rename_tac "J'" 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "J' = 0" 1);
+by (asm_full_simp_tac (simpset() addsimps [multirel_def]) 1);
+by (rtac r_into_trancl 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1);
+by (Force_tac 1);
+(*Now we know J' ~= 0*)
+by (rotate_simp_tac "multiset(J')" 1);
+by (dtac sym 1 THEN rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (thin_tac "$# x = msize(J')" 1);
+by (forw_inst_tac [("M","K"),("P", "%x. <x,a>:r")] multiset_partition 1);
+by (eres_inst_tac [("P", "ALL k:mset_of(K). ?P(k)")] rev_mp 1);
+by (etac ssubst 1);
+by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1);
+by Auto_tac;
+by (subgoal_tac "<(I +# {# x : K. <x, a> : r#}) +# {# x:K. <x, a> ~: r#}, \
+ \ (I +# {# x : K. <x, a> : r#}) +# J'>:multirel(A, r)" 1);
+by (dres_inst_tac [("x", "I +# {# x : K. <x, a>: r#}")] spec 2);
+by (rotate_tac ~1 2);
+by (dres_inst_tac [("x", "J'")] spec 2);
+by (rotate_tac ~1 2);
+by (dres_inst_tac [("x", "{# x : K. <x, a>~:r#}")] spec 2);
+by (Clarify_tac 2);
+by (Asm_full_simp_tac 2);
+by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym, multirel_def]) 1);
+by (res_inst_tac [("b", "I +# {# x:K. <x, a>:r#} +# J'")] trancl_trans 1);
+by (Blast_tac 1);
+by (rtac r_into_trancl 1);
+by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, multiset_on_def]) 1);
+by (res_inst_tac [("x", "a")] exI 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("x", "I +# J'")] exI 1);
+by (asm_simp_tac (simpset() addsimps munion_ac@[Un_subset_iff]) 1);
+by (rtac conjI 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT(Blast_tac 1));
+qed_spec_mp "one_step_implies_multirel_lemma";
+
+Goal "[| J ~= 0; ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r;\
+\ multiset[A](I); multiset[A](J); multiset[A](K) |] \
+\ ==> <I+#K, I+#J> : multirel(A, r)";
+by (subgoal_tac "multiset(J)" 1);
+by (asm_full_simp_tac (simpset() addsimps [multiset_on_def]) 2);
+by (forw_inst_tac [("M", "J")] msize_int_of_nat 1);
+by (auto_tac (claset() addIs [one_step_implies_multirel_lemma], simpset()));
+qed "one_step_implies_multirel";
+
+(** Proving that multisets are partially ordered **)
+
+(*irreflexivity*)
+
+Goal "Finite(A) ==> \
+\ part_ord(A, r) --> (ALL x:A. EX y:A. <x,y>:r) -->A=0";
+by (etac Finite_induct 1);
+by (auto_tac (claset() addDs
+ [subset_consI RSN (2, part_ord_subset)], simpset()));
+by (auto_tac (claset(), simpset() addsimps [part_ord_def, irrefl_def]));
+by (dres_inst_tac [("x", "xa")] bspec 1);
+by (dres_inst_tac [("a", "xa"), ("b", "x")] trans_onD 2);
+by Auto_tac;
+qed "multirel_irrefl_lemma";
+
+Goalw [irrefl_def]
+"part_ord(A, r) ==> irrefl(A-||>nat-{0}, multirel(A, r))";
+by (subgoal_tac "trans[A](r)" 1);
+by (asm_full_simp_tac (simpset() addsimps [part_ord_def]) 2);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
+by (dtac multirel_implies_one_step 1);
+by (Clarify_tac 1);
+by (rewrite_goal_tac [multiset_on_def] 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "Finite(mset_of(K))" 1);
+by (forw_inst_tac [("r", "r")] multirel_irrefl_lemma 1);
+by (forw_inst_tac [("B", "mset_of(K)")] part_ord_subset 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (auto_tac (claset(), simpset() addsimps [multiset_def, mset_of_def]));
+by (rotate_simp_tac "K:?u" 1);
+qed "irrefl_on_multirel";
+
+Goalw [multirel_def, trans_on_def]
+"trans[A-||>nat-{0}](multirel(A, r))";
+by (blast_tac (claset() addIs [trancl_trans]) 1);
+qed "trans_on_multirel";
+
+Goalw [multirel_def]
+ "[| <M, N>:multirel(A, r); <N, K>:multirel(A, r) |] ==> <M, K>:multirel(A,r)";
+by (blast_tac (claset() addIs [trancl_trans]) 1);
+qed "multirel_trans";
+
+Goalw [multirel_def] "trans(multirel(A,r))";
+by (rtac trans_trancl 1);
+qed "trans_multirel";
+
+Goal "part_ord(A,r) ==> part_ord(A-||>nat-{0}, multirel(A, r))";
+by (simp_tac (simpset() addsimps [part_ord_def]) 1);
+by (blast_tac (claset() addIs [irrefl_on_multirel, trans_on_multirel]) 1);
+qed "part_ord_multirel";
+
+(** Monotonicity of multiset union **)
+
+Goal
+"[|<M,N>:multirel1(A, r); multiset[A](K)|] ==> <K +# M, K +# N>: multirel1(A, r)";
+by (forward_tac [multirel1D] 1);
+by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def]));
+by (res_inst_tac [("x", "a")] exI 1);
+by (Asm_simp_tac 1);
+by (res_inst_tac [("x", "K+#M0")] exI 1);
+by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
+by (res_inst_tac [("x", "Ka")] exI 1);
+by (asm_simp_tac (simpset() addsimps [munion_assoc]) 1);
+qed "munion_multirel1_mono";
+
+
+Goal
+ "[| <M, N>:multirel(A, r); multiset[A](K) |]==><K +# M, K +# N>:multirel(A, r)";
+by (forward_tac [multirelD] 1);
+by (full_simp_tac (simpset() addsimps [multirel_def]) 1);
+by (Clarify_tac 1);
+by (dres_inst_tac [("psi", "<M,N>:multirel1(A, r)^+")] asm_rl 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (etac trancl_induct 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [munion_multirel1_mono, r_into_trancl]) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "multiset[A](y)" 1);
+by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirelD]) 2);
+by (subgoal_tac "<K +# y, K +# z>:multirel1(A, r)" 1);
+by (blast_tac (claset() addIs [munion_multirel1_mono]) 2);
+by (blast_tac (claset() addIs [r_into_trancl, trancl_trans]) 1);
+qed "munion_multirel_mono2";
+
+Goal
+"[|<M, N>:multirel(A, r); multiset[A](K)|] ==> <M +# K, N +# K>:multirel(A, r)";
+by (forward_tac [multirelD] 1);
+by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
+by (stac (munion_commute RS sym) 3);
+by (rtac munion_multirel_mono2 5);
+by (rewrite_goals_tac [multiset_on_def]);
+by Auto_tac;
+qed "munion_multirel_mono1";
+
+Goal
+"[|<M,K>:multirel(A, r); <N,L>:multirel(A, r)|]==><M +# N, K +# L>:multirel(A, r)";
+by (subgoal_tac "multiset[A](M)& multiset[A](N) & \
+\ multiset[A](K)& multiset[A](L)" 1);
+by (blast_tac (claset() addDs [multirelD]) 2);
+by (blast_tac (claset()
+ addIs [munion_multirel_mono1, multirel_trans, munion_multirel_mono2]) 1);
+qed "munion_multirel_mono";
+
+(** Ordinal multisets **)
+
+(* A <= B ==> field(Memrel(A)) \\<subseteq> field(Memrel(B)) *)
+bind_thm("field_Memrel_mono", Memrel_mono RS field_mono);
+
+(*
+[| Aa <= Ba; A <= B |] ==>
+multirel(field(Memrel(Aa)), Memrel(A))<= multirel(field(Memrel(Ba)), Memrel(B))
+*)
+bind_thm ("multirel_Memrel_mono",
+ [field_Memrel_mono, Memrel_mono]MRS multirel_mono);
+
+Goalw [omultiset_def, multiset_on_def] "omultiset(M) ==> multiset(M)";
+by Auto_tac;
+qed "omultiset_is_multiset";
+Addsimps [omultiset_is_multiset];
+
+Goalw [omultiset_def] "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "i Un ia")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
+by (blast_tac (claset() addIs [field_Memrel_mono]) 1);
+qed "munion_omultiset";
+Addsimps [munion_omultiset];
+
+Goalw [omultiset_def] "omultiset(M) ==> omultiset(M -# N)";
+by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
+by (res_inst_tac [("x", "i")] exI 1);
+by (Asm_simp_tac 1);
+qed "mdiff_omultiset";
+Addsimps [mdiff_omultiset];
+
+(** Proving that Memrel is a partial order **)
+
+Goal "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))";
+by (rtac irreflI 1);
+by (Clarify_tac 1);
+by (subgoal_tac "Ord(x)" 1);
+by (blast_tac (claset() addIs [Ord_in_Ord]) 2);
+by (dres_inst_tac [("i", "x")] (ltI RS lt_irrefl) 1);
+by Auto_tac;
+qed "irrefl_Memrel";
+
+Goalw [trans_on_def, trans_def]
+ "trans(r) <-> trans[field(r)](r)";
+by Auto_tac;
+qed "trans_iff_trans_on";
+
+Goalw [part_ord_def]
+ "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))";
+by (simp_tac (simpset() addsimps [trans_iff_trans_on RS iff_sym]) 1);
+by (blast_tac (claset() addIs [trans_Memrel, irrefl_Memrel]) 1);
+qed "part_ord_Memrel";
+
+(*
+ Ord(i) ==>
+ part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
+*)
+
+bind_thm("part_ord_mless", part_ord_Memrel RS part_ord_multirel);
+
+(*irreflexivity*)
+
+Goalw [mless_def] "~(M <# M)";
+by (Clarify_tac 1);
+by (forward_tac [multirel_type RS subsetD] 1);
+by (dtac part_ord_mless 1);
+by (rewrite_goals_tac [part_ord_def, irrefl_def]);
+by (Blast_tac 1);
+qed "mless_not_refl";
+
+(* N<N ==> R *)
+bind_thm ("mless_irrefl", mless_not_refl RS notE);
+AddSEs [mless_irrefl];
+
+(*transitivity*)
+Goalw [mless_def]
+ "[| K <# M; M <# N |] ==> K <# N";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "i Un ia")] exI 1);
+by (blast_tac (claset() addDs
+ [[Un_upper1, Un_upper1] MRS multirel_Memrel_mono RS subsetD,
+ [Un_upper2, Un_upper2] MRS multirel_Memrel_mono RS subsetD]
+ addIs [multirel_trans, Ord_Un]) 1);
+qed "mless_trans";
+
+(*asymmetry*)
+Goal "M <# N ==> ~ N <# M";
+by (Clarify_tac 1);
+by (rtac (mless_not_refl RS notE) 1);
+by (etac mless_trans 1);
+by (assume_tac 1);
+qed "mless_not_sym";
+
+val major::prems =
+Goal "[| M <# N; ~P ==> N <# M |] ==> P";
+by (cut_facts_tac [major] 1);
+by (dtac mless_not_sym 1);
+by (dres_inst_tac [("P", "P")] swap 1);
+by (auto_tac (claset() addIs prems, simpset()));
+qed "mless_asym";
+
+Goalw [mle_def] "omultiset(M) ==> M <#= M";
+by Auto_tac;
+qed "mle_refl";
+Addsimps [mle_refl];
+
+(*anti-symmetry*)
+Goalw [mle_def]
+"[| M <#= N; N <#= M |] ==> M = N";
+by (blast_tac (claset() addDs [mless_not_sym]) 1);
+qed "mle_antisym";
+
+(*transitivity*)
+Goalw [mle_def]
+ "[| K <#= M; M <#= N |] ==> K <#= N";
+by (blast_tac (claset() addIs [mless_trans]) 1);
+qed "mle_trans";
+
+Goalw [mle_def] "M <# N <-> (M <#= N & M ~= N)";
+by Auto_tac;
+qed "mless_le_iff";
+
+(** Monotonicity of mless **)
+
+Goalw [mless_def, omultiset_def]
+ "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "i Un ia")] exI 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
+by (rtac munion_multirel_mono2 1);
+by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2);
+by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
+by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
+qed "munion_less_mono2";
+
+Goalw [mless_def, omultiset_def]
+ "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K";
+by (Clarify_tac 1);
+by (res_inst_tac [("x", "i Un ia")] exI 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [multiset_on_def, Ord_Un, Un_subset_iff]) 1);
+by (rtac munion_multirel_mono1 1);
+by (asm_simp_tac (simpset() addsimps [multiset_on_def]) 2);
+by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
+by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
+qed "munion_less_mono1";
+
+Goalw [mless_def, omultiset_def]
+ "M <# N ==> omultiset(M) & omultiset(N)";
+by (auto_tac (claset() addDs [multirelD], simpset()));
+qed "mless_imp_omultiset";
+
+Goal "[| M <# K; N <# L |] ==> M +# N <# K +# L";
+by (forw_inst_tac [("M", "M")] mless_imp_omultiset 1);
+by (forw_inst_tac [("M", "N")] mless_imp_omultiset 1);
+by (blast_tac (claset() addIs
+ [munion_less_mono1, munion_less_mono2, mless_trans]) 1);
+qed "munion_less_mono";
+
+(* <#= *)
+
+Goalw [mle_def]
+ "M <#= N ==> omultiset(M) & omultiset(N)";
+by (auto_tac (claset(), simpset() addsimps [mless_imp_omultiset]));
+qed "mle_imp_omultiset";
+
+Goal
+ "[| M <#= K; N <#= L |] ==> M +# N <#= K +# L";
+by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1);
+by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1);
+by (rewrite_goals_tac [mle_def]);
+by (ALLGOALS(Asm_full_simp_tac));
+by (REPEAT(etac disjE 1));
+by (etac disjE 3);
+by (ALLGOALS(Asm_full_simp_tac));
+by (ALLGOALS(rtac disjI2));
+by (auto_tac (claset() addIs [munion_less_mono1, munion_less_mono2,
+ munion_less_mono], simpset()));
+qed "mle_mono";
+
+Goalw [omultiset_def, multiset_on_def] "omultiset(0)";
+by Auto_tac;
+qed "omultiset_0";
+AddIffs [omultiset_0];
+
+Goalw [mle_def, mless_def]
+ "omultiset(M) ==> 0 <#= M";
+by (subgoal_tac "EX i. Ord(i) & multiset[field(Memrel(i))](M)" 1);
+by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2);
+by (case_tac "M=0" 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Clarify_tac 1);
+by (subgoal_tac "<0 +# 0, 0 +# M>: multirel(field(Memrel(i)), Memrel(i))" 1);
+by (rtac one_step_implies_multirel 2);
+by Auto_tac;
+by (dres_inst_tac [("x", "i")] spec 1);
+by (auto_tac (claset(), simpset() addsimps [multiset_on_def]));
+qed "empty_leI";
+Addsimps [empty_leI];
+
+Goal "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N";
+by (subgoal_tac "M +# 0 <#= M +# N" 1);
+by (rtac mle_mono 2);
+by Auto_tac;
+qed "munion_upper1";
+
+
+Goal "[| omultiset(M); omultiset(N) |] ==> N <#= M +# N";
+by (stac munion_commute 1);
+by (rtac munion_upper1 3);
+by Auto_tac;
+qed "munion_upper2";
+
+Delsimps [domain_of_fun];
+AddSEs [domainE];