# HG changeset patch
# User paulson
# Date 1095430132 -7200
# Node ID d73f9d49d835e3b567170d26e41af51f9452f270
# Parent  09489fe6989f5469b3318acc910aad92765d15d1
converted ZF/Induct/Multiset to Isar script

diff -r 09489fe6989f -r d73f9d49d835 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Mon Sep 13 09:57:25 2004 +0200
+++ b/src/ZF/Arith.thy	Fri Sep 17 16:08:52 2004 +0200
@@ -307,6 +307,9 @@
 lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
 by (drule add_lt_elim1_natify, auto)
 
+lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
+by (induct_tac "n", auto)
+
 
 subsection{*Monotonicity of Addition*}
 
diff -r 09489fe6989f -r d73f9d49d835 src/ZF/Induct/Multiset.ML
--- a/src/ZF/Induct/Multiset.ML	Mon Sep 13 09:57:25 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1483 +0,0 @@
-(*  Title:      ZF/Induct/Multiset
-    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.
-
-*)
-
-(* Properties of the original "restrict" from ZF.thy. *)
-
-Goalw [funrestrict_def,lam_def]
-    "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) <= f";
-by (blast_tac (claset() addIs [apply_Pair]) 1);
-qed "funrestrict_subset";
-
-val prems = Goalw [funrestrict_def]
-    "[| !!x. x:A ==> f`x: B(x) |] ==> funrestrict(f,A) : Pi(A,B)";  
-by (rtac lam_type 1);
-by (eresolve_tac prems 1);
-qed "funrestrict_type";
-
-Goal "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) : Pi(A,B)";  
-by (blast_tac (claset() addIs [apply_type, funrestrict_type]) 1);
-qed "funrestrict_type2";
-
-Goalw [funrestrict_def] "a : A ==> funrestrict(f,A) ` a = f`a";
-by (etac beta 1);
-qed "funrestrict";
-
-Goalw [funrestrict_def] "funrestrict(f,0) = 0";
-by (Simp_tac 1);
-qed "funrestrict_empty";
-
-Addsimps [funrestrict, funrestrict_empty];
-
-Goalw [funrestrict_def, lam_def] "domain(funrestrict(f,C)) = C";
-by (Blast_tac 1);
-qed "domain_funrestrict";
-Addsimps [domain_funrestrict];
-
-Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))";
-by (rtac equalityI 1);
-by (blast_tac (claset() addIs [apply_Pair, impOfSubs funrestrict_subset]) 2);
-by (auto_tac (claset() addSDs [Pi_memberD],
-	       simpset() addsimps [funrestrict_def, lam_def]));
-qed "fun_cons_funrestrict_eq";
-
-Addsimps [domain_of_fun];
-Delrules [domainE];
-
-(* 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";
-
-(** The multiset space  **)
-Goalw [multiset_def]
- "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)";
-by (auto_tac (claset(), simpset()
-             addsimps [multiset_fun_iff, mset_of_def]));
-by (Asm_full_simp_tac 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_into_Mult";
-
-Goalw [multiset_def, mset_of_def]
- "M:Mult(A) ==> multiset(M) & mset_of(M)<=A";
-by (ftac FiniteFun_is_fun 1);
-by (dtac FiniteFun_domain_Fin 1);
-by (ftac 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 "Mult_into_multiset";
-
-Goal "M:Mult(A) <-> multiset(M) & mset_of(M)<=A";
-by (blast_tac (claset() addDs [Mult_into_multiset]
-                        addIs [multiset_into_Mult]) 1);
-qed "Mult_iff_multiset";
-
-Goal "multiset(M) <-> M:Mult(mset_of(M))";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-qed "multiset_iff_Mult_mset_of";
-
-(** multiset  **)
-
-(* the empty multiset is 0 *)
-
-Goal "multiset(0)";
-by (auto_tac (claset() addIs (thms"FiniteFun.intros"), 
-        simpset()  addsimps [multiset_iff_Mult_mset_of]));
-qed "multiset_0";
-Addsimps [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 [mdiff_def, multiset_def]
- "mset_of(M)<=A ==> mset_of(M -# N) <= A";
-by (auto_tac (claset(), simpset() addsimps [normalize_def]));
-by (rewtac mset_of_def);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
-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];
-AddTCs [msingle_multiset];
-
-(** normalize **)
-
-bind_thm("Collect_Finite", Collect_subset RS subset_Finite);
-
-Goalw [normalize_def, funrestrict_def, mset_of_def]
- "normalize(normalize(f)) = normalize(f)";
-by (case_tac "EX A. f : A -> nat & Finite(A)" 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1); 
-by (Clarify_tac 1); 
-by (dres_inst_tac [("x","{x: domain(f) . 0 < f ` x}")] spec 1); 
-by (force_tac (claset() addSIs [lam_type], simpset() addsimps [Collect_Finite]) 1);  
-by (Asm_simp_tac 1); 
-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 [funrestrict_def, multiset_fun_iff]));
-qed "normalize_multiset";
-Addsimps [normalize_multiset];
-
-Goal "multiset(normalize(f))";
-by (asm_full_simp_tac (simpset() addsimps [normalize_def]) 1); 
-by (rewrite_goals_tac [normalize_def, mset_of_def, multiset_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,
-                              funrestrict_type], simpset()));
-qed "multiset_normalize";
-Addsimps [multiset_normalize];
-
-(** Typechecking rules for union and difference of multisets **)
-
-(*????????????????move to Arith??*)
-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 *)
-
-Goal "multiset(M -# N)";
-by (asm_full_simp_tac (simpset() addsimps [mdiff_def]) 1); 
-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] "M +# N = N +# M";
-by (auto_tac (claset() addSIs [lam_cong],  simpset() addsimps [munion_def]));
-qed "munion_commute";
-
-Goalw [multiset_def] "(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] "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 [normalize_def, mset_of_def]) 1);
-qed "mdiff_self_eq_0";
-Addsimps [mdiff_self_eq_0];
-
-Goalw [multiset_def] "0 -# M = 0";
-by (rewrite_goals_tac [mdiff_def, normalize_def]);
-by (auto_tac (claset(), simpset() 
-         addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
-qed "mdiff_0";
-Addsimps [mdiff_0]; 
-
-Goalw [multiset_def] "multiset(M) ==> M -# 0 = M";
-by (rewrite_goals_tac [mdiff_def, normalize_def]);
-by (auto_tac (claset(), simpset() 
-         addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
-qed "mdiff_0_right";
-Addsimps [mdiff_0_right]; 
-
-Goal "multiset(M) ==> M +# {#a#} -# {#a#} = M";
-by (rewrite_goals_tac [multiset_def, munion_def, mdiff_def, 
-                       msingle_def, normalize_def, mset_of_def]);
-by (auto_tac (claset(), 
-       simpset() addcongs [if_cong]
-		 addsimps [ltD, multiset_fun_iff,
-                           funrestrict_def, subset_Un_iff2 RS iffD1]));
-by (force_tac (claset() addSIs [lam_type], simpset()) 2);   
-by (subgoal_tac "{x \\<in> A \\<union> {a} . x \\<noteq> a \\<and> x \\<in> A} = A" 2);
-by (rtac fun_extension 1);
-by Auto_tac; 
-by (dres_inst_tac [("x","A Un {a}")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [Finite_Un]) 1); 
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-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";
-AddTCs [mcount_type];
-Addsimps [mcount_type];
-
-Goalw [mcount_def]  "mcount(0, a) = 0";
-by Auto_tac;
-qed "mcount_0";
-Addsimps [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) ==> 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]));
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-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 (Asm_full_simp_tac 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];
-
-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
-"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, Int_cons_left]));
-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(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 (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 (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(funrestrict(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(funrestrict(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(funrestrict(M, mset_of(M)-{a}),x),A-{a}) = \
-\                setsum(%x. $# mcount(funrestrict(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 (ftac msize_eq_0_iff 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [mset_of_def, multiset_def,  
-                                  multiset_fun_iff, msize_def]@prems));
-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`a" 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(a:=M`a #- 1))(a:=(M(a:=M`a #- 1))`a #+ 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(a := M ` a #- 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(a, A). x~=a-->0<M`x})" 1);
-by (blast_tac(claset() addIs [Collect_subset RS subset_Finite,Finite_cons])2);
-by (dres_inst_tac [("A", "{x:cons(a, A). x~=a-->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", "a")] bspec 1);
-by (Asm_simp_tac 1);
-by (subgoal_tac "cons(a, A)= A" 1);
-by (Blast_tac 2);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "M=cons(<a, M`a>, funrestrict(M, A-{a}))" 1);
-by (rtac  fun_cons_funrestrict_eq 2);
-by (subgoal_tac "cons(a, A-{a}) = A" 2);
-by (REPEAT(Force_tac 2));
-by (res_inst_tac [("a", "cons(<a, 1>, funrestrict(M, A - {a}))")] ssubst 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "multiset(funrestrict(M, A - {a}))" 1);
-by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
-by (res_inst_tac [("x", "A-{a}")] exI 2);
-by Safe_tac;
-by (res_inst_tac [("A", "A-{a}")] apply_type 3);
-by (asm_simp_tac (simpset() addsimps [funrestrict]) 5);
-by (REPEAT(blast_tac (claset() addIs [Finite_Diff, funrestrict_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", "funrestrict(M, A-{a})")] spec 1);
-by (dtac mp 1);
-by (res_inst_tac [("x", "A-{a}")] exI 1);
-by (auto_tac (claset() addIs [Finite_Diff, funrestrict_type], 
-             simpset() addsimps [funrestrict]));
-by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] 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 Asm_full_simp_tac);
-by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 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 (rtac 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 (rewtac mset_of_def);
-by (Asm_full_simp_tac 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_apply]));
-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 (rewtac mset_of_def);
-by (Asm_full_simp_tac 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,
-                               funrestrict_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, funrestrict_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]));
-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_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]));
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
-qed "melem_diff_single";
-
-Goal
-"[| M:Mult(A); N:Mult(A) |] \
-\ ==> (M +# {#a#} = N +# {#b#}) <-> \
-\     (M=N & a=b | (EX K:Mult(A). M= K +# {#b#} & N=K +# {#a#}))";
-by (auto_tac (claset(), 
-              simpset() addsimps [Bex_def, Mult_iff_multiset,
-                  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} *)
-
-
-(* multirel1 type *)
-
-Goalw [multirel1_def]
-"multirel1(A, r) <= Mult(A)*Mult(A)";
-by Auto_tac;
-qed "multirel1_type";
-
-Goalw [multirel1_def] "multirel1(0, r) =0";
-by Auto_tac;
-qed "multirel1_0";
-AddIffs [multirel1_0];
-
-Goalw [multirel1_def]
-" <N, M>:multirel1(A, r) <-> \
-\ (EX a. a:A &                                       \
-\ (EX M0. M0:Mult(A) & (EX K. K:Mult(A) &  \
-\  M=M0 +# {#a#} & N=M0 +# K & (ALL b:mset_of(K). <b,a>:r))))";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset, Ball_def, Bex_def]));
-qed "multirel1_iff";
-
-(* Monotonicity of multirel1 *)
-
-Goalw [multirel1_def]  "A<=B ==> multirel1(A, r)<=multirel1(B, r)";
-by (auto_tac (claset(), simpset() addsimps []));
-by (ALLGOALS(asm_full_simp_tac(simpset() 
-    addsimps [Un_subset_iff, Mult_iff_multiset])));
-by (res_inst_tac [("x", "a")] bexI 3);
-by (res_inst_tac [("x", "M0")] bexI 3);
-by (Asm_simp_tac 3);
-by (res_inst_tac [("x", "K")] bexI 3);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset])));
-by Auto_tac;
-qed "multirel1_mono1";
-
-Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)";
-by (auto_tac (claset(), simpset() addsimps []));
-by (res_inst_tac [("x", "a")] bexI 1);
-by (res_inst_tac [("x", "M0")] bexI 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
-by (res_inst_tac [("x", "K")] bexI 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
-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 [Mult_iff_multiset]));
-qed "not_less_0";
-AddIffs [not_less_0];
-
-Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); M0:Mult(A) |] ==> \
-\ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
-\ (EX K. K:Mult(A) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
-by (forward_tac [multirel1_type RS subsetD] 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 (rewtac (Mult_iff_multiset RS iff_reflection));
-by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1);
-by (auto_tac (claset(), simpset() addsimps [munion_commute]));
-qed "less_munion";
-
-Goal "[| M:Mult(A); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
-by (auto_tac (claset(), simpset() addsimps [multirel1_iff]));
-by (rewrite_goals_tac [Mult_iff_multiset RS iff_reflection]);
-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  [thm "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 "M0:Mult(A)" 1);
-by (etac (thm "acc.cases") 2);
-by (etac fieldE 2);
-by (REPEAT(blast_tac (claset() addDs [multirel1_type RS subsetD]) 2));
-by (rtac (thm "accI") 1);
-by (rename_tac "N" 1);
-by (dtac less_munion 1);
-by (Blast_tac 1);
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-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 [Mult_iff_multiset]));
-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 (thm "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 (thm "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 [Mult_iff_multiset RS iff_reflection] 2);
-by (REPEAT(Blast_tac 1));
-qed "lemma4";
-
-Goal "[| wf[A](r); M:Mult(A); 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 [Mult_iff_multiset]));
-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 (thm "wf_on_acc") 1);
-by (Clarify_tac 1);
-by (full_simp_tac (simpset() addsimps []) 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) <= Mult(A)*Mult(A)";
-by (rtac (trancl_type RS subset_trans) 1);
-by (Clarify_tac 1);
-by (auto_tac (claset() addDs [multirel1_type RS subsetD], 
-              simpset() addsimps []));
-qed "multirel_type";
-
-(* 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 (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, 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. \
-\        I:Mult(A) & J:Mult(A) &  K:Mult(A) & \
-\        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, Mult_iff_multiset])));
-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); M:Mult(A); n:nat |] \
-\     ==> EX a N. M = N +# {#a#} & N:Mult(A) & 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 (ftac Mult_into_multiset 1);
-by (Asm_simp_tac 1);
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-qed "msize_eq_succ_imp_eq_union";
-
-(* The second direction *)
-
-Goalw [Mult_iff_multiset RS iff_reflection] 
-"n:nat ==> \
-\  (ALL I J K.  \
-\   I:Mult(A) & J:Mult(A) & K:Mult(A) & \
-\  (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 (rewtac (Mult_iff_multiset RS iff_reflection));
-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, Mult_iff_multiset]) 1);
-by (Force_tac 1);
-(*Now we know J' ~=  0*)
-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, Mult_iff_multiset]) 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;\
-\         I:Mult(A); J:Mult(A); K:Mult(A) |] \
-\         ==> <I+#K, I+#J> : multirel(A, r)";
-by (subgoal_tac "multiset(J)" 1);
-by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 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(Mult(A), 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 []) 1);
-by (dtac multirel_implies_one_step 1);
-by (Clarify_tac 1);
-by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 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]));
-qed "irrefl_on_multirel";
-
-Goalw [multirel_def, trans_on_def] "trans[Mult(A)](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(Mult(A), 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); K:Mult(A) |] ==> <K +# M, K +# N>:multirel1(A, r)";
-by (ftac (multirel1_type RS subsetD) 1);
-by (auto_tac (claset(), simpset() addsimps [multirel1_iff, Mult_iff_multiset]));
-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); K:Mult(A) |]==><K +# M, K +# N>:multirel(A, r)";
-by (ftac (multirel_type RS subsetD) 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 "y:Mult(A)" 1);
-by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirel_type RS subsetD]) 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); K:Mult(A)|] ==> <M +# K, N +# K>:multirel(A, r)";
-by (ftac (multirel_type RS subsetD) 1);
-by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
-by (stac (munion_commute RS sym) 1);
-by (rtac munion_multirel_mono2 1);
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-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 "M:Mult(A)& N:Mult(A) & K:Mult(A)& L:Mult(A)" 1);
-by (blast_tac (claset() addDs [multirel_type RS subsetD]) 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] "omultiset(M) ==> multiset(M)";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-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
-            [Mult_iff_multiset, 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 (Clarify_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
-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 [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
-by (rtac munion_multirel_mono2 1);
-by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 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 [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
-by (rtac munion_multirel_mono1 1);
-by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 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 [multirel_type RS subsetD], 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 (rewtac 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]  "omultiset(0)";
-by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
-qed "omultiset_0";
-AddIffs [omultiset_0];
-
-Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M";
-by (subgoal_tac "EX i. Ord(i) & M:Mult(field(Memrel(i)))" 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 (claset(), simpset() addsimps [Mult_iff_multiset]));
-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";
-
-
-
-
diff -r 09489fe6989f -r d73f9d49d835 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Mon Sep 13 09:57:25 2004 +0200
+++ b/src/ZF/Induct/Multiset.thy	Fri Sep 17 16:08:52 2004 +0200
@@ -8,91 +8,1424 @@
 The theory features ordinal multisets and the usual ordering.
 *)
 
-Multiset =  FoldSet + Acc +
+theory Multiset
+imports FoldSet Acc
+begin
+
 consts
   (* Short cut for multiset space *)
-  Mult :: i=>i 
-translations 
+  Mult :: "i=>i"
+translations
   "Mult(A)" => "A -||> nat-{0}"
-  
+
 constdefs
-  
+
   (* This is the original "restrict" from ZF.thy.
-     Restricts the function f to the domain A 
+     Restricts the function f to the domain A
      FIXME: adapt Multiset to the new "restrict". *)
 
   funrestrict :: "[i,i] => i"
-  "funrestrict(f,A) == lam x:A. f`x"
+  "funrestrict(f,A) == \<lambda>x \<in> A. f`x"
 
   (* M is a multiset *)
-  multiset :: i => o
-  "multiset(M) == EX A. M : A -> nat-{0} & Finite(A)"
+  multiset :: "i => o"
+  "multiset(M) == \<exists>A. M \<in> A -> nat-{0} & Finite(A)"
 
   mset_of :: "i=>i"
   "mset_of(M) == domain(M)"
 
   munion    :: "[i, i] => i" (infixl "+#" 65)
-  "M +# N == lam x:mset_of(M) Un mset_of(N).
-     if x:mset_of(M) Int mset_of(N) then  (M`x) #+ (N`x)
-     else (if x:mset_of(M) then M`x else N`x)"
+  "M +# N == \<lambda>x \<in> mset_of(M) Un mset_of(N).
+     if x \<in> mset_of(M) Int mset_of(N) then  (M`x) #+ (N`x)
+     else (if x \<in> mset_of(M) then M`x else N`x)"
 
   (*convert a function to a multiset by eliminating 0*)
-  normalize :: i => i   
+  normalize :: "i => i"
   "normalize(f) ==
-       if (EX A. f : A -> nat & Finite(A)) then
-            funrestrict(f, {x:mset_of(f). 0 < f`x})
+       if (\<exists>A. f \<in> A -> nat & Finite(A)) then
+            funrestrict(f, {x \<in> mset_of(f). 0 < f`x})
        else 0"
 
   mdiff  :: "[i, i] => i" (infixl "-#" 65)
-  "M -# N ==  normalize(lam x:mset_of(M).
-			if x:mset_of(N) then M`x #- N`x else M`x)"
+  "M -# N ==  normalize(\<lambda>x \<in> mset_of(M).
+			if x \<in> mset_of(N) then M`x #- N`x else M`x)"
 
   (* set of elements of a multiset *)
   msingle :: "i => i"    ("{#_#}")
   "{#a#} == {<a, 1>}"
-  
-  MCollect :: [i, i=>o] => i (*comprehension*)
-  "MCollect(M, P) == funrestrict(M, {x:mset_of(M). P(x)})"
+
+  MCollect :: "[i, i=>o] => i"  (*comprehension*)
+  "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})"
 
   (* Counts the number of occurences of an element in a multiset *)
-  mcount :: [i, i] => i
-  "mcount(M, a) == if a:mset_of(M) then  M`a else 0"
-  
-  msize :: i => i
-  "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"  
+  mcount :: "[i, i] => i"
+  "mcount(M, a) == if a \<in> mset_of(M) then  M`a else 0"
+
+  msize :: "i => i"
+  "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
 
 syntax
-  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)  
+  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)
   "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
 
+syntax (xsymbols)
+  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+
 translations
-  "a :# M" == "a:mset_of(M)"
-  "{#x:M. P#}" == "MCollect(M, %x. P)"
+  "a :# M" == "a \<in> mset_of(M)"
+  "{#x \<in> M. P#}" == "MCollect(M, %x. P)"
 
   (* multiset orderings *)
-  
+
 constdefs
    (* multirel1 has to be a set (not a predicate) so that we can form
       its transitive closure and reason about wf(.) and acc(.) *)
-  
+
   multirel1 :: "[i,i]=>i"
   "multirel1(A, r) ==
-     {<M, N> : Mult(A)*Mult(A).
-      EX a:A. EX M0:Mult(A). EX K:Mult(A).
-      N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). <b,a>:r)}"
-  
+     {<M, N> \<in> Mult(A)*Mult(A).
+      \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A).
+      N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}"
+
   multirel :: "[i, i] => i"
-  "multirel(A, r) == multirel1(A, r)^+" 		    
+  "multirel(A, r) == multirel1(A, r)^+" 		
 
   (* ordinal multiset orderings *)
-  
-  omultiset :: i => o
-  "omultiset(M) == EX i. Ord(i) & M:Mult(field(Memrel(i)))"
-  
-  mless :: [i, i] => o (infixl "<#" 50)
-  "M <# N ==  EX i. Ord(i) & <M, N>:multirel(field(Memrel(i)), Memrel(i))"
+
+  omultiset :: "i => o"
+  "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))"
+
+  mless :: "[i, i] => o" (infixl "<#" 50)
+  "M <# N ==  \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))"
+
+  mle  :: "[i, i] => o"  (infixl "<#=" 50)
+  "M <#= N == (omultiset(M) & M = N) | M <# N"
+
+
+subsection{*Properties of the original "restrict" from ZF.thy*}
+
+lemma funrestrict_subset: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<subseteq> f"
+by (auto simp add: funrestrict_def lam_def intro: apply_Pair)
+
+lemma funrestrict_type:
+    "[| !!x. x \<in> A ==> f`x \<in> B(x) |] ==> funrestrict(f,A) \<in> Pi(A,B)"
+by (simp add: funrestrict_def lam_type)
+
+lemma funrestrict_type2: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<in> Pi(A,B)"
+by (blast intro: apply_type funrestrict_type)
+
+lemma funrestrict [simp]: "a \<in> A ==> funrestrict(f,A) ` a = f`a"
+by (simp add: funrestrict_def)
+
+lemma funrestrict_empty [simp]: "funrestrict(f,0) = 0"
+by (simp add: funrestrict_def)
+
+lemma domain_funrestrict [simp]: "domain(funrestrict(f,C)) = C"
+by (auto simp add: funrestrict_def lam_def)
+
+lemma fun_cons_funrestrict_eq:
+     "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))"
+apply (rule equalityI)
+prefer 2 apply (blast intro: apply_Pair funrestrict_subset [THEN subsetD])
+apply (auto dest!: Pi_memberD simp add: funrestrict_def lam_def)
+done
+
+declare domain_of_fun [simp]
+declare domainE [rule del]
+
+
+text{* A useful simplification rule *}
+lemma multiset_fun_iff:
+     "(f \<in> A -> nat-{0}) <-> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
+apply safe
+apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD])
+apply (auto intro!: Ord_0_lt
+            dest: apply_type Diff_subset [THEN Pi_mono, THEN subsetD]
+            simp add: range_of_fun apply_iff)
+done
+
+(** The multiset space  **)
+lemma multiset_into_Mult: "[| multiset(M); mset_of(M)\<subseteq>A |] ==> M \<in> Mult(A)"
+apply (simp add: multiset_def)
+apply (auto simp add: multiset_fun_iff mset_of_def)
+apply (rule_tac B1 = "nat-{0}" in FiniteFun_mono [THEN subsetD], simp_all)
+apply (rule Finite_into_Fin [THEN [2] Fin_mono [THEN subsetD], THEN fun_FiniteFunI])
+apply (simp_all (no_asm_simp) add: multiset_fun_iff)
+done
+
+lemma Mult_into_multiset: "M \<in> Mult(A) ==> multiset(M) & mset_of(M)\<subseteq>A"
+apply (simp add: multiset_def mset_of_def)
+apply (frule FiniteFun_is_fun)
+apply (drule FiniteFun_domain_Fin)
+apply (frule FinD, clarify)
+apply (rule_tac x = "domain (M) " in exI)
+apply (blast intro: Fin_into_Finite)
+done
+
+lemma Mult_iff_multiset: "M \<in> Mult(A) <-> multiset(M) & mset_of(M)\<subseteq>A"
+by (blast dest: Mult_into_multiset intro: multiset_into_Mult)
+
+lemma multiset_iff_Mult_mset_of: "multiset(M) <-> M \<in> Mult(mset_of(M))"
+by (auto simp add: Mult_iff_multiset)
+
+
+text{*The @{term multiset} operator*}
+
+(* the empty multiset is 0 *)
+
+lemma multiset_0 [simp]: "multiset(0)"
+by (auto intro: FiniteFun.intros simp add: multiset_iff_Mult_mset_of)
+
+
+text{*The @{term mset_of} operator*}
+
+lemma multiset_set_of_Finite [simp]: "multiset(M) ==> Finite(mset_of(M))"
+by (simp add: multiset_def mset_of_def, auto)
+
+lemma mset_of_0 [iff]: "mset_of(0) = 0"
+by (simp add: mset_of_def)
+
+lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 <-> M=0"
+by (auto simp add: multiset_def mset_of_def)
+
+lemma mset_of_single [iff]: "mset_of({#a#}) = {a}"
+by (simp add: msingle_def mset_of_def)
+
+lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) Un mset_of(N)"
+by (simp add: mset_of_def munion_def)
+
+lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A"
+by (auto simp add: mdiff_def multiset_def normalize_def mset_of_def)
+
+(* msingle *)
+
+lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}"
+by (simp add: msingle_def)
+
+lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) <->  (a = b)"
+by (simp add: msingle_def)
+
+lemma msingle_multiset [iff,TC]: "multiset({#a#})"
+apply (simp add: multiset_def msingle_def)
+apply (rule_tac x = "{a}" in exI)
+apply (auto intro: Finite_cons Finite_0 fun_extend3)
+done
+
+(** normalize **)
+
+lemmas Collect_Finite = Collect_subset [THEN subset_Finite, standard]
+
+lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)"
+apply (simp add: normalize_def funrestrict_def mset_of_def)
+apply (case_tac "\<exists>A. f \<in> A -> nat & Finite (A) ")
+apply clarify
+apply (drule_tac x = "{x \<in> domain (f) . 0 < f ` x}" in spec)
+apply auto
+apply (auto  intro!: lam_type simp add: Collect_Finite)
+done
+
+lemma normalize_multiset [simp]: "multiset(M) ==> normalize(M) = M"
+by (auto simp add: multiset_def normalize_def mset_of_def funrestrict_def multiset_fun_iff)
+
+lemma multiset_normalize [simp]: "multiset(normalize(f))"
+apply (simp add: normalize_def)
+apply (simp add: normalize_def mset_of_def multiset_def, auto)
+apply (rule_tac x = "{x \<in> A . 0<f`x}" in exI)
+apply (auto intro: Collect_subset [THEN subset_Finite] funrestrict_type)
+done
+
+(** Typechecking rules for union and difference of multisets **)
+
+(* union *)
+
+lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)"
+apply (unfold multiset_def munion_def mset_of_def, auto)
+apply (rule_tac x = "A Un Aa" in exI)
+apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add)
+done
+
+(* difference *)
+
+lemma mdiff_multiset [simp]: "multiset(M -# N)"
+by (simp add: mdiff_def)
+
+(** Algebraic properties of multisets **)
+
+(* Union *)
+
+lemma munion_0 [simp]: "multiset(M) ==> M +# 0 = M & 0 +# M = M"
+apply (simp add: multiset_def)
+apply (auto simp add: munion_def mset_of_def)
+done
+
+lemma munion_commute: "M +# N = N +# M"
+by (auto intro!: lam_cong simp add: munion_def)
+
+lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
+apply (unfold munion_def mset_of_def)
+apply (rule lam_cong, auto)
+done
+
+lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
+apply (unfold munion_def mset_of_def)
+apply (rule lam_cong, auto)
+done
+
+lemmas munion_ac = munion_commute munion_assoc munion_lcommute
+
+(* Difference *)
+
+lemma mdiff_self_eq_0 [simp]: "M -# M = 0"
+by (simp add: mdiff_def normalize_def mset_of_def)
+
+lemma mdiff_0 [simp]: "0 -# M = 0"
+by (simp add: mdiff_def normalize_def)
+
+lemma mdiff_0_right [simp]: "multiset(M) ==> M -# 0 = M"
+by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
+
+lemma mdiff_union_inverse2 [simp]: "multiset(M) ==> M +# {#a#} -# {#a#} = M"
+apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
+apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
+prefer 2 apply (force intro!: lam_type)
+apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
+apply (rule fun_extension, auto)
+apply (drule_tac x = "A Un {a}" in spec)
+apply (simp add: Finite_Un)
+apply (force intro!: lam_type)
+done
+
+(** Count of elements **)
+
+lemma mcount_type [simp,TC]: "multiset(M) ==> mcount(M, a) \<in> nat"
+by (auto simp add: multiset_def mcount_def mset_of_def multiset_fun_iff)
+
+lemma mcount_0 [simp]: "mcount(0, a) = 0"
+by (simp add: mcount_def)
+
+lemma mcount_single [simp]: "mcount({#b#}, a) = (if a=b then 1 else 0)"
+by (simp add: mcount_def mset_of_def msingle_def)
+
+lemma mcount_union [simp]: "[| multiset(M); multiset(N) |]
+                     ==>  mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)"
+apply (auto simp add: multiset_def multiset_fun_iff mcount_def munion_def mset_of_def)
+done
+
+lemma mcount_diff [simp]:
+     "multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)"
+apply (simp add: multiset_def)
+apply (auto dest!: not_lt_imp_le
+     simp add: mdiff_def multiset_fun_iff mcount_def normalize_def mset_of_def)
+apply (force intro!: lam_type)
+apply (force intro!: lam_type)
+done
+
+lemma mcount_elem: "[| multiset(M); a \<in> mset_of(M) |] ==> 0 < mcount(M, a)"
+apply (simp add: multiset_def, clarify)
+apply (simp add: mcount_def mset_of_def)
+apply (simp add: multiset_fun_iff)
+done
+
+(** msize **)
+
+lemma msize_0 [simp]: "msize(0) = #0"
+by (simp add: msize_def)
+
+lemma msize_single [simp]: "msize({#a#}) = #1"
+by (simp add: msize_def)
+
+lemma msize_type [simp,TC]: "msize(M) \<in> int"
+by (simp add: msize_def)
+
+lemma msize_zpositive: "multiset(M)==> #0 $\<le> msize(M)"
+by (auto simp add: msize_def intro: g_zpos_imp_setsum_zpos)
+
+lemma msize_int_of_nat: "multiset(M) ==> \<exists>n \<in> nat. msize(M)= $# n"
+apply (rule not_zneg_int_of)
+apply (simp_all (no_asm_simp) add: msize_type [THEN znegative_iff_zless_0] not_zless_iff_zle msize_zpositive)
+done
+
+lemma not_empty_multiset_imp_exist:
+     "[| M\<noteq>0; multiset(M) |] ==> \<exists>a \<in> mset_of(M). 0 < mcount(M, a)"
+apply (simp add: multiset_def)
+apply (erule not_emptyE)
+apply (auto simp add: mset_of_def mcount_def multiset_fun_iff)
+apply (blast dest!: fun_is_rel)
+done
+
+lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 <-> M=0"
+apply (simp add: msize_def, auto)
+apply (rule_tac Pa = "setsum (?u,?v) \<noteq> #0" in swap)
+apply blast
+apply (drule not_empty_multiset_imp_exist, assumption, clarify)
+apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
+ prefer 2 apply (simp add: Finite_Diff)
+apply (subgoal_tac "setsum (%x. $# mcount (M, x), cons (a, mset_of (M) -{a}))=#0")
+ prefer 2 apply (simp add: cons_Diff, simp)
+apply (subgoal_tac "#0 $\<le> setsum (%x. $# mcount (M, x), mset_of (M) - {a}) ")
+apply (rule_tac [2] g_zpos_imp_setsum_zpos)
+apply (auto simp add: Finite_Diff not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
+apply (rule not_zneg_int_of [THEN bexE])
+apply (auto simp del: int_of_0 simp add: int_of_add [symmetric] int_of_0 [symmetric])
+done
+
+lemma setsum_mcount_Int:
+     "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
+		  = setsum(%a. $# mcount(N, a), A)"
+apply (erule Finite_induct, auto)
+apply (subgoal_tac "Finite (B Int mset_of (N))")
+prefer 2 apply (blast intro: subset_Finite)
+apply (auto simp add: mcount_def Int_cons_left)
+done
+
+lemma msize_union [simp]:
+     "[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)"
+apply (simp add: msize_def setsum_Un setsum_addf int_of_add setsum_mcount_Int)
+apply (subst Int_commute)
+apply (simp add: setsum_mcount_Int)
+done
+
+lemma msize_eq_succ_imp_elem: "[|msize(M)= $# succ(n); n \<in> nat|] ==> \<exists>a. a \<in> mset_of(M)"
+apply (unfold msize_def)
+apply (blast dest: setsum_succD)
+done
+
+(** Equality of multisets **)
+
+lemma equality_lemma:
+     "[| multiset(M); multiset(N); \<forall>a. mcount(M, a)=mcount(N, a) |]
+      ==> mset_of(M)=mset_of(N)"
+apply (simp add: multiset_def)
+apply (rule sym, rule equalityI)
+apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
+apply (drule_tac [!] x=x in spec)
+apply (case_tac [2] "x \<in> Aa", case_tac "x \<in> A", auto)
+done
+
+lemma multiset_equality:
+  "[| multiset(M); multiset(N) |]==> M=N<->(\<forall>a. mcount(M, a)=mcount(N, a))"
+apply auto
+apply (subgoal_tac "mset_of (M) = mset_of (N) ")
+prefer 2 apply (blast intro: equality_lemma)
+apply (simp add: multiset_def mset_of_def)
+apply (auto simp add: multiset_fun_iff)
+apply (rule fun_extension)
+apply (blast, blast)
+apply (drule_tac x = x in spec)
+apply (auto simp add: mcount_def mset_of_def)
+done
+
+(** More algebraic properties of multisets **)
+
+lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)"
+by (auto simp add: multiset_equality)
+
+lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)"
+apply (rule iffI, drule sym)
+apply (simp_all add: multiset_equality)
+done
+
+lemma munion_right_cancel [simp]:
+     "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)"
+by (auto simp add: multiset_equality)
+
+lemma munion_left_cancel [simp]:
+  "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)"
+by (auto simp add: multiset_equality)
+
+lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)"
+by (induct_tac "n", auto)
+
+lemma munion_is_single:
+     "[|multiset(M); multiset(N)|] 
+      ==> (M +# N = {#a#}) <->  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
+apply (simp (no_asm_simp) add: multiset_equality)
+apply safe
+apply simp_all
+apply (case_tac "aa=a")
+apply (drule_tac [2] x = aa in spec)
+apply (drule_tac x = a in spec)
+apply (simp add: nat_add_eq_1_cases, simp)
+apply (case_tac "aaa=aa", simp)
+apply (drule_tac x = aa in spec)
+apply (simp add: nat_add_eq_1_cases)
+apply (case_tac "aaa=a")
+apply (drule_tac [4] x = aa in spec)
+apply (drule_tac [3] x = a in spec)
+apply (drule_tac [2] x = aaa in spec)
+apply (drule_tac x = aa in spec)
+apply (simp_all add: nat_add_eq_1_cases)
+done
+
+lemma msingle_is_union: "[| multiset(M); multiset(N) |]
+  ==> ({#a#} = M +# N) <-> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)"
+apply (subgoal_tac " ({#a#} = M +# N) <-> (M +# N = {#a#}) ")
+apply (simp (no_asm_simp) add: munion_is_single)
+apply blast
+apply (blast dest: sym)
+done
+
+(** Towards induction over multisets **)
+
+lemma setsum_decr:
+"Finite(A)
+  ==>  (\<forall>M. multiset(M) -->
+  (\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) =
+  (if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1
+           else setsum(%z. $# mcount(M, z), A))))"
+apply (unfold multiset_def)
+apply (erule Finite_induct)
+apply (auto simp add: multiset_fun_iff)
+apply (unfold mset_of_def mcount_def)
+apply (case_tac "x \<in> A", auto)
+apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
+apply (erule ssubst)
+apply (rule int_of_diff, auto)
+done
+
+(*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.*)
+lemma setsum_decr2:
+     "Finite(A)
+      ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
+           setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) =
+           (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a
+            else setsum(%x'. $# mcount(M, x'), A)))"
+apply (simp add: multiset_def)
+apply (erule Finite_induct)
+apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
+done
+
+lemma setsum_decr3: "[| Finite(A); multiset(M); a \<in> mset_of(M) |]
+      ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) =
+          (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
+           else setsum(%x. $# mcount(M, x), A))"
+apply (subgoal_tac "setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A-{a}) = setsum (%x. $# mcount (funrestrict (M, mset_of (M) -{a}),x),A) ")
+apply (rule_tac [2] setsum_Diff [symmetric])
+apply (rule sym, rule ssubst, blast)
+apply (rule sym, drule setsum_decr2, auto)
+apply (simp add: mcount_def mset_of_def)
+done
+
+lemma nat_le_1_cases: "n \<in> nat ==> n le 1 <-> (n=0 | n=1)"
+by (auto elim: natE)
+
+lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n"
+apply (subgoal_tac "1 le n")
+apply (drule add_diff_inverse2, auto)
+done
+
+text{*Specialized for use in the proof below.*}
+lemma multiset_funrestict:
+     "\<lbrakk>\<forall>a\<in>A. M ` a \<in> nat \<and> 0 < M ` a; Finite(A)\<rbrakk>
+      \<Longrightarrow> multiset(funrestrict(M, A - {a}))"
+apply (simp add: multiset_def multiset_fun_iff)
+apply (rule_tac x="A-{a}" in exI)
+apply (auto intro: Finite_Diff funrestrict_type)
+done
+
+lemma multiset_induct_aux:
+  assumes prem1: "!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))"
+      and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))"
+  shows
+  "[| n \<in> nat; P(0) |]
+     ==> (\<forall>M. multiset(M)-->
+  (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) --> P(M))"
+apply (erule nat_induct, clarify)
+apply (frule msize_eq_0_iff)
+apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def)
+apply (subgoal_tac "setsum (%x. $# mcount (M, x), A) =$# succ (x) ")
+apply (drule setsum_succD, auto)
+apply (case_tac "1 <M`a")
+apply (drule_tac [2] not_lt_imp_le)
+apply (simp_all add: nat_le_1_cases)
+apply (subgoal_tac "M= (M (a:=M`a #- 1)) (a:= (M (a:=M`a #- 1))`a #+ 1) ")
+apply (rule_tac [2] A = A and B = "%x. nat" and D = "%x. nat" in fun_extension)
+apply (rule_tac [3] update_type)+
+apply (simp_all (no_asm_simp))
+ apply (rule_tac [2] impI)
+ apply (rule_tac [2] succ_pred_eq_self [symmetric])
+apply (simp_all (no_asm_simp))
+apply (rule subst, rule sym, blast, rule prem2)
+apply (simp (no_asm) add: multiset_def multiset_fun_iff)
+apply (rule_tac x = A in exI)
+apply (force intro: update_type)
+apply (simp (no_asm_simp) add: mset_of_def mcount_def)
+apply (drule_tac x = "M (a := M ` a #- 1) " in spec)
+apply (drule mp, drule_tac [2] mp, simp_all)
+apply (rule_tac x = A in exI)
+apply (auto intro: update_type)
+apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a-->0<M`x}) ")
+prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons)
+apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a-->0<M`x}" in setsum_decr)
+apply (drule_tac x = M in spec)
+apply (subgoal_tac "multiset (M) ")
+ prefer 2
+ apply (simp add: multiset_def multiset_fun_iff)
+ apply (rule_tac x = A in exI, force)
+apply (simp_all add: mset_of_def)
+apply (drule_tac psi = "\<forall>x \<in> A. ?u (x) " in asm_rl)
+apply (drule_tac x = a in bspec)
+apply (simp (no_asm_simp))
+apply (subgoal_tac "cons (a, A) = A")
+prefer 2 apply blast
+apply simp
+apply (subgoal_tac "M=cons (<a, M`a>, funrestrict (M, A-{a}))")
+ prefer 2
+ apply (rule fun_cons_funrestrict_eq)
+ apply (subgoal_tac "cons (a, A-{a}) = A")
+  apply force
+  apply force
+apply (rule_tac a = "cons (<a, 1>, funrestrict (M, A - {a}))" in ssubst)
+apply simp
+apply (frule multiset_funrestict, assumption)
+apply (rule prem1, assumption)
+apply (simp add: mset_of_def)
+apply (drule_tac x = "funrestrict (M, A-{a}) " in spec)
+apply (drule mp)
+apply (rule_tac x = "A-{a}" in exI)
+apply (auto intro: Finite_Diff funrestrict_type simp add: funrestrict)
+apply (frule_tac A = A and M = M and a = a in setsum_decr3)
+apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
+apply blast
+apply (simp (no_asm_simp) add: mset_of_def)
+apply (drule_tac b = "if ?u then ?v else ?w" in sym, simp_all)
+apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
+apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
+done
+
+lemma multiset_induct2:
+  "[| multiset(M); P(0);
+    (!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M)));
+    (!!M b. [| multiset(M); b \<in> mset_of(M);  P(M) |] ==> P(M(b:= M`b #+ 1))) |]
+     ==> P(M)"
+apply (subgoal_tac "\<exists>n \<in> nat. setsum (\<lambda>x. $# mcount (M, x), {x \<in> mset_of (M) . 0 < M ` x}) = $# n")
+apply (rule_tac [2] not_zneg_int_of)
+apply (simp_all (no_asm_simp) add: znegative_iff_zless_0 not_zless_iff_zle)
+apply (rule_tac [2] g_zpos_imp_setsum_zpos)
+prefer 2 apply (blast intro:  multiset_set_of_Finite Collect_subset [THEN subset_Finite])
+ prefer 2 apply (simp add: multiset_def multiset_fun_iff, clarify)
+apply (rule multiset_induct_aux [rule_format], auto)
+done
+
+lemma munion_single_case1:
+     "[| multiset(M); a \<notin>mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)"
+apply (simp add: multiset_def msingle_def)
+apply (auto simp add: munion_def)
+apply (unfold mset_of_def, simp)
+apply (rule fun_extension, rule lam_type, simp_all)
+apply (auto simp add: multiset_fun_iff fun_extend_apply)
+apply (drule_tac c = a and b = 1 in fun_extend3)
+apply (auto simp add: cons_eq Un_commute [of _ "{a}"])
+done
+
+lemma munion_single_case2:
+     "[| multiset(M); a \<in> mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)"
+apply (simp add: multiset_def)
+apply (auto simp add: munion_def multiset_fun_iff msingle_def)
+apply (unfold mset_of_def, simp)
+apply (subgoal_tac "A Un {a} = A")
+apply (rule fun_extension)
+apply (auto dest: domain_type intro: lam_type update_type)
+done
+
+(* Induction principle for multisets *)
+
+lemma multiset_induct:
+  assumes M: "multiset(M)"
+      and P0: "P(0)"
+      and step: "!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})"
+  shows "P(M)"
+apply (rule multiset_induct2 [OF M])
+apply (simp_all add: P0)
+apply (frule_tac [2] a1 = b in munion_single_case2 [symmetric])
+apply (frule_tac a1 = a in munion_single_case1 [symmetric])
+apply (auto intro: step)
+done
+
+(** MCollect **)
+
+lemma MCollect_multiset [simp]:
+     "multiset(M) ==> multiset({# x \<in> M. P(x)#})"
+apply (simp add: MCollect_def multiset_def mset_of_def, clarify)
+apply (rule_tac x = "{x \<in> A. P (x) }" in exI)
+apply (auto dest: CollectD1 [THEN [2] apply_type]
+            intro: Collect_subset [THEN subset_Finite] funrestrict_type)
+done
+
+lemma mset_of_MCollect [simp]:
+     "multiset(M) ==> mset_of({# x \<in> M. P(x) #}) \<subseteq> mset_of(M)"
+by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def)
+
+lemma MCollect_mem_iff [iff]:
+     "x \<in> mset_of({#x \<in> M. P(x)#}) <->  x \<in> mset_of(M) & P(x)"
+by (simp add: MCollect_def mset_of_def)
+
+lemma mcount_MCollect [simp]:
+     "mcount({# x \<in> M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)"
+by (simp add: mcount_def MCollect_def mset_of_def)
+
+lemma multiset_partition: "multiset(M) ==> M = {# x \<in> M. P(x) #} +# {# x \<in> M. ~ P(x) #}"
+by (simp add: multiset_equality)
+
+lemma natify_elem_is_self [simp]:
+     "[| multiset(M); a \<in> mset_of(M) |] ==> natify(M`a) = M`a"
+by (auto simp add: multiset_def mset_of_def multiset_fun_iff)
+
+(* and more algebraic laws on multisets *)
+
+lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |]
+  ==>  (M +# {#a#} = N +# {#b#}) <->  (M = N & a = b |
+       M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})"
+apply (simp del: mcount_single add: multiset_equality)
+apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE)
+apply (case_tac "a=b", auto)
+apply (drule_tac x = a in spec)
+apply (drule_tac [2] x = b in spec)
+apply (drule_tac [3] x = aa in spec)
+apply (drule_tac [4] x = a in spec, auto)
+apply (subgoal_tac [!] "mcount (N,a) :nat")
+apply (erule_tac [3] natE, erule natE, auto)
+done
+
+lemma melem_diff_single:
+"multiset(M) ==>
+  k \<in> mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
+apply (simp add: multiset_def)
+apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def)
+apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1]
+            simp add: multiset_fun_iff apply_iff)
+apply (force intro!: lam_type)
+apply (force intro!: lam_type)
+apply (force intro!: lam_type)
+done
+
+lemma munion_eq_conv_exist:
+"[| M \<in> Mult(A); N \<in> Mult(A) |]
+  ==> (M +# {#a#} = N +# {#b#}) <->
+      (M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))"
+by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff)
+
+
+subsection{*Multiset Orderings*}
+
+(* multiset on a domain A are finite functions from A to nat-{0} *)
+
+
+(* multirel1 type *)
+
+lemma multirel1_type: "multirel1(A, r) \<subseteq> Mult(A)*Mult(A)"
+by (auto simp add: multirel1_def)
+
+lemma multirel1_0 [simp]: "multirel1(0, r) =0"
+by (auto simp add: multirel1_def)
+
+lemma multirel1_iff:
+" <N, M> \<in> multirel1(A, r) <->
+  (\<exists>a. a \<in> A &
+  (\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) &
+   M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))"
+by (auto simp add: multirel1_def Mult_iff_multiset Bex_def)
+
+
+text{*Monotonicity of @{term multirel1}*}
+
+lemma multirel1_mono1: "A\<subseteq>B ==> multirel1(A, r)\<subseteq>multirel1(B, r)"
+apply (auto simp add: multirel1_def)
+apply (auto simp add: Un_subset_iff Mult_iff_multiset)
+apply (rule_tac x = a in bexI)
+apply (rule_tac x = M0 in bexI, simp)
+apply (rule_tac x = K in bexI)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma multirel1_mono2: "r\<subseteq>s ==> multirel1(A,r)\<subseteq>multirel1(A, s)"
+apply (simp add: multirel1_def, auto) 
+apply (rule_tac x = a in bexI)
+apply (rule_tac x = M0 in bexI)
+apply (simp_all add: Mult_iff_multiset)
+apply (rule_tac x = K in bexI)
+apply (simp_all add: Mult_iff_multiset, auto)
+done
+
+lemma multirel1_mono:
+     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel1(A, r) \<subseteq> multirel1(B, s)"
+apply (rule subset_trans)
+apply (rule multirel1_mono1)
+apply (rule_tac [2] multirel1_mono2, auto)
+done
+
+subsection{* Toward the proof of well-foundedness of multirel1 *}
+
+lemma not_less_0 [iff]: "<M,0> \<notin> multirel1(A, r)"
+by (auto simp add: multirel1_def Mult_iff_multiset)
 
-  mle  :: [i, i] => o  (infixl "<#=" 50)
-  "M <#= N == (omultiset(M) & M = N) | M <# N"
-  
+lemma less_munion: "[| <N, M0 +# {#a#}> \<in> multirel1(A, r); M0 \<in> Mult(A) |] ==>
+  (\<exists>M. <M, M0> \<in> multirel1(A, r) & N = M +# {#a#}) |
+  (\<exists>K. K \<in> Mult(A) & (\<forall>b \<in> mset_of(K). <b, a> \<in> r) & N = M0 +# K)"
+apply (frule multirel1_type [THEN subsetD])
+apply (simp add: multirel1_iff)
+apply (auto simp add: munion_eq_conv_exist)
+apply (rule_tac x="Ka +# K" in exI, auto, simp add: Mult_iff_multiset)
+apply (simp (no_asm_simp) add: munion_left_cancel munion_assoc)
+apply (auto simp add: munion_commute)
+done
+
+lemma multirel1_base: "[| M \<in> Mult(A); a \<in> A |] ==> <M, M +# {#a#}> \<in> multirel1(A, r)"
+apply (auto simp add: multirel1_iff)
+apply (simp add: Mult_iff_multiset)
+apply (rule_tac x = a in exI, clarify)
+apply (rule_tac x = M in exI, simp)
+apply (rule_tac x = 0 in exI, auto)
+done
+
+lemma acc_0: "acc(0)=0"
+by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD])
+
+lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r -->
+    (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r)));
+    M0 \<in> acc(multirel1(A, r)); a \<in> A;
+    \<forall>M. <M,M0> \<in> multirel1(A, r) --> M +# {#a#} \<in> acc(multirel1(A, r)) |]
+  ==> M0 +# {#a#} \<in> acc(multirel1(A, r))"
+apply (subgoal_tac "M0 \<in> Mult (A) ")
+ prefer 2
+ apply (erule acc.cases)
+ apply (erule fieldE)
+ apply (auto dest: multirel1_type [THEN subsetD])
+apply (rule accI)
+apply (rename_tac "N")
+apply (drule less_munion, blast)
+apply (auto simp add: Mult_iff_multiset)
+apply (erule_tac P = "\<forall>x \<in> mset_of (K) . <x, a> \<in> r" in rev_mp)
+apply (erule_tac P = "mset_of (K) \<subseteq>A" in rev_mp)
+apply (erule_tac M = K in multiset_induct)
+(* three subgoals *)
+(* subgoal 1: the induction base case *)
+apply (simp (no_asm_simp))
+(* subgoal 2: the induction general case *)
+apply (simp add: Ball_def Un_subset_iff, clarify)
+apply (drule_tac x = aa in spec, simp)
+apply (subgoal_tac "aa \<in> A")
+prefer 2 apply blast
+apply (drule_tac x = "M0 +# M" and P =
+       "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
+apply (simp add: munion_assoc [symmetric])
+(* subgoal 3: additional conditions *)
+apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
+done
+
+lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
+   --> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
+        M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))"
+apply (erule acc_induct)
+apply (blast intro: lemma1)
+done
+
+lemma lemma3: "[| wf[A](r); a \<in> A |]
+      ==> \<forall>M \<in> acc(multirel1(A, r)). M +# {#a#} \<in> acc(multirel1(A, r))"
+apply (erule_tac a = a in wf_on_induct, blast)
+apply (blast intro: lemma2)
+done
+
+lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A -->
+   wf[A](r) --> M \<in> field(multirel1(A, r)) --> M \<in> acc(multirel1(A, r))"
+apply (erule multiset_induct)
+(* proving the base case *)
+apply clarify
+apply (rule accI, force)
+apply (simp add: multirel1_def)
+(* Proving the general case *)
+apply clarify
+apply simp
+apply (subgoal_tac "mset_of (M) \<subseteq>A")
+prefer 2 apply blast
+apply clarify
+apply (drule_tac a = a in lemma3, blast)
+apply (subgoal_tac "M \<in> field (multirel1 (A,r))")
+apply blast
+apply (rule multirel1_base [THEN fieldI1])
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma all_accessible: "[| wf[A](r); M \<in> Mult(A); A \<noteq> 0|] ==> M \<in> acc(multirel1(A, r))"
+apply (erule not_emptyE)
+apply  (rule lemma4 [THEN mp, THEN mp, THEN mp])
+apply (rule_tac [4] multirel1_base [THEN fieldI1])
+apply  (auto simp add: Mult_iff_multiset)
+done
+
+lemma wf_on_multirel1: "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))"
+apply (case_tac "A=0")
+apply (simp (no_asm_simp))
+apply (rule wf_imp_wf_on)
+apply (rule wf_on_field_imp_wf)
+apply (simp (no_asm_simp) add: wf_on_0)
+apply (rule_tac A = "acc (multirel1 (A,r))" in wf_on_subset_A)
+apply (rule wf_on_acc)
+apply (blast intro: all_accessible)
+done
+
+lemma wf_multirel1: "wf(r) ==>wf(multirel1(field(r), r))"
+apply (simp (no_asm_use) add: wf_iff_wf_on_field)
+apply (drule wf_on_multirel1)
+apply (rule_tac A = "field (r) -||> nat - {0}" in wf_on_subset_A)
+apply (simp (no_asm_simp))
+apply (rule field_rel_subset)
+apply (rule multirel1_type)
+done
+
+(** multirel **)
+
+lemma multirel_type: "multirel(A, r) \<subseteq> Mult(A)*Mult(A)"
+apply (simp add: multirel_def)
+apply (rule trancl_type [THEN subset_trans])
+apply (auto dest: multirel1_type [THEN subsetD])
+done
+
+(* Monotonicity of multirel *)
+lemma multirel_mono:
+     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel(A, r)\<subseteq>multirel(B,s)"
+apply (simp add: multirel_def)
+apply (rule trancl_mono)
+apply (rule multirel1_mono, auto)
+done
+
+(* Equivalence of multirel with the usual (closure-free) def *)
+
+lemma add_diff_eq: "k \<in> nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)"
+by (erule nat_induct, auto)
+
+lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]
+   ==> I +# J -# {#a#} = I +# (J-# {#a#})"
+apply (simp (no_asm_simp) add: multiset_equality)
+apply (case_tac "a \<notin> mset_of (I) ")
+apply (auto simp add: mcount_def mset_of_def multiset_def multiset_fun_iff)
+apply (auto dest: domain_type simp add: add_diff_eq)
+done
+
+lemma diff_add_commute: "[| n le m;  m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
+by (auto simp add: le_iff less_iff_succ_add)
+
+(* One direction *)
+
+lemma multirel_implies_one_step:
+"<M,N> \<in> multirel(A, r) ==>
+     trans[A](r) -->
+     (\<exists>I J K.
+         I \<in> Mult(A) & J \<in> Mult(A) &  K \<in> Mult(A) &
+         N = I +# J & M = I +# K & J \<noteq> 0 &
+        (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r))"
+apply (simp add: multirel_def Ball_def Bex_def)
+apply (erule converse_trancl_induct)
+apply (simp_all add: multirel1_iff Mult_iff_multiset)
+(* Two subgoals remain *)
+(* Subgoal 1 *)
+apply clarify
+apply (rule_tac x = M0 in exI, force)
+(* Subgoal 2 *)
+apply clarify
+apply (case_tac "a \<in> mset_of (Ka) ")
+apply (rule_tac x = I in exI, simp (no_asm_simp))
+apply (rule_tac x = J in exI, simp (no_asm_simp))
+apply (rule_tac x = " (Ka -# {#a#}) +# K" in exI, simp (no_asm_simp))
+apply (simp_all add: Un_subset_iff)
+apply (simp (no_asm_simp) add: munion_assoc [symmetric])
+apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
+apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
+apply (erule disjE, simp)
+apply (erule disjE, simp)
+apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> ?Q(x)" in spec)
+apply clarify
+apply (rule_tac x = xa in exI)
+apply (simp (no_asm_simp))
+apply (blast dest: trans_onD)
+(* new we know that  a\<notin>mset_of(Ka) *)
+apply (subgoal_tac "a :# I")
+apply (rule_tac x = "I-#{#a#}" in exI, simp (no_asm_simp))
+apply (rule_tac x = "J+#{#a#}" in exI)
+apply (simp (no_asm_simp) add: Un_subset_iff)
+apply (rule_tac x = "Ka +# K" in exI)
+apply (simp (no_asm_simp) add: Un_subset_iff)
+apply (rule conjI)
+apply (simp (no_asm_simp) add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
+apply (rule conjI)
+apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
+apply (simp add: mdiff_union_inverse2)
+apply (simp_all (no_asm_simp) add: multiset_equality)
+apply (rule diff_add_commute [symmetric])
+apply (auto intro: mcount_elem)
+apply (subgoal_tac "a \<in> mset_of (I +# Ka) ")
+apply (drule_tac [2] sym, auto)
+done
+
+lemma melem_imp_eq_diff_union [simp]: "[| a \<in> mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M"
+by (simp add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
+
+lemma msize_eq_succ_imp_eq_union:
+     "[| msize(M)=$# succ(n); M \<in> Mult(A); n \<in> nat |]
+      ==> \<exists>a N. M = N +# {#a#} & N \<in> Mult(A) & a \<in> A"
+apply (drule msize_eq_succ_imp_elem, auto)
+apply (rule_tac x = a in exI)
+apply (rule_tac x = "M -# {#a#}" in exI)
+apply (frule Mult_into_multiset)
+apply (simp (no_asm_simp))
+apply (auto simp add: Mult_iff_multiset)
+done
+
+(* The second direction *)
+
+lemma one_step_implies_multirel_lemma [rule_format (no_asm)]:
+"n \<in> nat ==>
+   (\<forall>I J K.
+    I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
+   (msize(J) = $# n & J \<noteq>0 &  (\<forall>k \<in> mset_of(K).  \<exists>j \<in> mset_of(J). <k, j> \<in> r))
+    --> <I +# K, I +# J> \<in> multirel(A, r))"
+apply (simp add: Mult_iff_multiset)
+apply (erule nat_induct, clarify)
+apply (drule_tac M = J in msize_eq_0_iff, auto)
+(* one subgoal remains *)
+apply (subgoal_tac "msize (J) =$# succ (x) ")
+ prefer 2 apply simp
+apply (frule_tac A = A in msize_eq_succ_imp_eq_union)
+apply (simp_all add: Mult_iff_multiset, clarify)
+apply (rename_tac "J'", simp)
+apply (case_tac "J' = 0")
+apply (simp add: multirel_def)
+apply (rule r_into_trancl, clarify)
+apply (simp add: multirel1_iff Mult_iff_multiset, force)
+(*Now we know J' \<noteq>  0*)
+apply (drule sym, rotate_tac -1, simp)
+apply (erule_tac V = "$# x = msize (J') " in thin_rl)
+apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
+apply (erule_tac P = "\<forall>k \<in> mset_of (K) . ?P (k) " in rev_mp)
+apply (erule ssubst)
+apply (simp add: Ball_def, auto)
+apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel (A, r) ")
+ prefer 2
+ apply (drule_tac x = "I +# {# x \<in> K. <x, a> \<in> r#}" in spec)
+ apply (rotate_tac -1)
+ apply (drule_tac x = "J'" in spec)
+ apply (rotate_tac -1)
+ apply (drule_tac x = "{# x \<in> K. <x, a> \<notin> r#}" in spec, simp) apply blast
+apply (simp add: munion_assoc [symmetric] multirel_def)
+apply (rule_tac b = "I +# {# x \<in> K. <x, a> \<in> r#} +# J'" in trancl_trans, blast)
+apply (rule r_into_trancl)
+apply (simp add: multirel1_iff Mult_iff_multiset)
+apply (rule_tac x = a in exI)
+apply (simp (no_asm_simp))
+apply (rule_tac x = "I +# J'" in exI)
+apply (auto simp add: munion_ac Un_subset_iff)
+done
+
+lemma one_step_implies_multirel:
+     "[| J \<noteq> 0;  \<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r;
+         I \<in> Mult(A); J \<in> Mult(A); K \<in> Mult(A) |]
+      ==> <I+#K, I+#J> \<in> multirel(A, r)"
+apply (subgoal_tac "multiset (J) ")
+ prefer 2 apply (simp add: Mult_iff_multiset)
+apply (frule_tac M = J in msize_int_of_nat)
+apply (auto intro: one_step_implies_multirel_lemma)
+done
+
+(** Proving that multisets are partially ordered **)
+
+(*irreflexivity*)
+
+lemma multirel_irrefl_lemma:
+     "Finite(A) ==> part_ord(A, r) --> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) -->A=0"
+apply (erule Finite_induct)
+apply (auto dest: subset_consI [THEN [2] part_ord_subset])
+apply (auto simp add: part_ord_def irrefl_def)
+apply (drule_tac x = xa in bspec)
+apply (drule_tac [2] a = xa and b = x in trans_onD, auto)
+done
+
+lemma irrefl_on_multirel:
+     "part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))"
+apply (simp add: irrefl_def)
+apply (subgoal_tac "trans[A](r) ")
+ prefer 2 apply (simp add: part_ord_def, clarify)
+apply (drule multirel_implies_one_step, clarify)
+apply (simp add: Mult_iff_multiset, clarify)
+apply (subgoal_tac "Finite (mset_of (K))")
+apply (frule_tac r = r in multirel_irrefl_lemma)
+apply (frule_tac B = "mset_of (K) " in part_ord_subset)
+apply simp_all
+apply (auto simp add: multiset_def mset_of_def)
+done
+
+lemma trans_on_multirel: "trans[Mult(A)](multirel(A, r))"
+apply (simp add: multirel_def trans_on_def)
+apply (blast intro: trancl_trans)
+done
+
+lemma multirel_trans:
+ "[| <M, N> \<in> multirel(A, r); <N, K> \<in> multirel(A, r) |] ==>  <M, K> \<in> multirel(A,r)"
+apply (simp add: multirel_def)
+apply (blast intro: trancl_trans)
+done
+
+lemma trans_multirel: "trans(multirel(A,r))"
+apply (simp add: multirel_def)
+apply (rule trans_trancl)
+done
+
+lemma part_ord_multirel: "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))"
+apply (simp (no_asm) add: part_ord_def)
+apply (blast intro: irrefl_on_multirel trans_on_multirel)
+done
+
+(** Monotonicity of multiset union **)
+
+lemma munion_multirel1_mono:
+"[|<M,N> \<in> multirel1(A, r); K \<in> Mult(A) |] ==> <K +# M, K +# N> \<in> multirel1(A, r)"
+apply (frule multirel1_type [THEN subsetD])
+apply (auto simp add: multirel1_iff Mult_iff_multiset)
+apply (rule_tac x = a in exI)
+apply (simp (no_asm_simp))
+apply (rule_tac x = "K+#M0" in exI)
+apply (simp (no_asm_simp) add: Un_subset_iff)
+apply (rule_tac x = Ka in exI)
+apply (simp (no_asm_simp) add: munion_assoc)
+done
+
+lemma munion_multirel_mono2:
+ "[| <M, N> \<in> multirel(A, r); K \<in> Mult(A) |]==><K +# M, K +# N> \<in> multirel(A, r)"
+apply (frule multirel_type [THEN subsetD])
+apply (simp (no_asm_use) add: multirel_def)
+apply clarify
+apply (drule_tac psi = "<M,N> \<in> multirel1 (A, r) ^+" in asm_rl)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule trancl_induct, clarify)
+apply (blast intro: munion_multirel1_mono r_into_trancl, clarify)
+apply (subgoal_tac "y \<in> Mult (A) ")
+ prefer 2
+ apply (blast dest: multirel_type [unfolded multirel_def, THEN subsetD])
+apply (subgoal_tac "<K +# y, K +# z> \<in> multirel1 (A, r) ")
+prefer 2 apply (blast intro: munion_multirel1_mono)
+apply (blast intro: r_into_trancl trancl_trans)
+done
+
+lemma munion_multirel_mono1:
+     "[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
+apply (frule multirel_type [THEN subsetD])
+apply (rule_tac P = "%x. <x,?u> \<in> multirel (A, r) " in munion_commute [THEN subst])
+apply (subst munion_commute [symmetric])
+apply (rule munion_multirel_mono2)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma munion_multirel_mono:
+     "[|<M,K> \<in> multirel(A, r); <N,L> \<in> multirel(A, r)|]
+      ==> <M +# N, K +# L> \<in> multirel(A, r)"
+apply (subgoal_tac "M \<in> Mult (A) & N \<in> Mult (A) & K \<in> Mult (A) & L \<in> Mult (A) ")
+prefer 2 apply (blast dest: multirel_type [THEN subsetD])
+apply (blast intro: munion_multirel_mono1 multirel_trans munion_multirel_mono2)
+done
+
+
+subsection{*Ordinal Multisets*}
+
+(* A \<subseteq> B ==>  field(Memrel(A)) \<subseteq> field(Memrel(B)) *)
+lemmas field_Memrel_mono = Memrel_mono [THEN field_mono, standard]
+
+(*
+[| Aa \<subseteq> Ba; A \<subseteq> B |] ==>
+multirel(field(Memrel(Aa)), Memrel(A))\<subseteq> multirel(field(Memrel(Ba)), Memrel(B))
+*)
+
+lemmas multirel_Memrel_mono = multirel_mono [OF field_Memrel_mono Memrel_mono]
+
+lemma omultiset_is_multiset [simp]: "omultiset(M) ==> multiset(M)"
+apply (simp add: omultiset_def)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)"
+apply (simp add: omultiset_def, clarify)
+apply (rule_tac x = "i Un ia" in exI)
+apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
+apply (blast intro: field_Memrel_mono)
+done
+
+lemma mdiff_omultiset [simp]: "omultiset(M) ==> omultiset(M -# N)"
+apply (simp add: omultiset_def, clarify)
+apply (simp add: Mult_iff_multiset)
+apply (rule_tac x = i in exI)
+apply (simp (no_asm_simp))
+done
+
+(** Proving that Memrel is a partial order **)
+
+lemma irrefl_Memrel: "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))"
+apply (rule irreflI, clarify)
+apply (subgoal_tac "Ord (x) ")
+prefer 2 apply (blast intro: Ord_in_Ord)
+apply (drule_tac i = x in ltI [THEN lt_irrefl], auto)
+done
+
+lemma trans_iff_trans_on: "trans(r) <-> trans[field(r)](r)"
+by (simp add: trans_on_def trans_def, auto)
+
+lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))"
+apply (simp add: part_ord_def)
+apply (simp (no_asm) add: trans_iff_trans_on [THEN iff_sym])
+apply (blast intro: trans_Memrel irrefl_Memrel)
+done
+
+(*
+  Ord(i) ==>
+  part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
+*)
+
+lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel, standard]
+
+(*irreflexivity*)
+
+lemma mless_not_refl: "~(M <# M)"
+apply (simp add: mless_def, clarify)
+apply (frule multirel_type [THEN subsetD])
+apply (drule part_ord_mless)
+apply (simp add: part_ord_def irrefl_def)
+done
+
+(* N<N ==> R *)
+lemmas mless_irrefl = mless_not_refl [THEN notE, standard, elim!]
+
+(*transitivity*)
+lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
+apply (simp add: mless_def, clarify)
+apply (rule_tac x = "i Un ia" in exI)
+apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD]
+                   multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD]
+        intro: multirel_trans Ord_Un)
+done
+
+(*asymmetry*)
+lemma mless_not_sym: "M <# N ==> ~ N <# M"
+apply clarify
+apply (rule mless_not_refl [THEN notE])
+apply (erule mless_trans, assumption)
+done
+
+lemma mless_asym: "[| M <# N; ~P ==> N <# M |] ==> P"
+by (blast dest: mless_not_sym)
+
+lemma mle_refl [simp]: "omultiset(M) ==> M <#= M"
+by (simp add: mle_def)
+
+(*anti-symmetry*)
+lemma mle_antisym:
+     "[| M <#= N;  N <#= M |] ==> M = N"
+apply (simp add: mle_def)
+apply (blast dest: mless_not_sym)
+done
+
+(*transitivity*)
+lemma mle_trans: "[| K <#= M; M <#= N |] ==> K <#= N"
+apply (simp add: mle_def)
+apply (blast intro: mless_trans)
+done
+
+lemma mless_le_iff: "M <# N <-> (M <#= N & M \<noteq> N)"
+by (simp add: mle_def, auto)
+
+(** Monotonicity of mless **)
+
+lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N"
+apply (simp add: mless_def omultiset_def, clarify)
+apply (rule_tac x = "i Un ia" in exI)
+apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
+apply (rule munion_multirel_mono2)
+ apply (blast intro: multirel_Memrel_mono [THEN subsetD])
+apply (simp add: Mult_iff_multiset)
+apply (blast intro: field_Memrel_mono [THEN subsetD])
+done
+
+lemma munion_less_mono1: "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K"
+by (force dest: munion_less_mono2 simp add: munion_commute)
+
+lemma mless_imp_omultiset: "M <# N ==> omultiset(M) & omultiset(N)"
+by (auto simp add: mless_def omultiset_def dest: multirel_type [THEN subsetD])
+
+lemma munion_less_mono: "[| M <# K; N <# L |] ==> M +# N <# K +# L"
+apply (frule_tac M = M in mless_imp_omultiset)
+apply (frule_tac M = N in mless_imp_omultiset)
+apply (blast intro: munion_less_mono1 munion_less_mono2 mless_trans)
+done
+
+(* <#= *)
+
+lemma mle_imp_omultiset: "M <#= N ==> omultiset(M) & omultiset(N)"
+by (auto simp add: mle_def mless_imp_omultiset)
+
+lemma mle_mono: "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L"
+apply (frule_tac M = M in mle_imp_omultiset)
+apply (frule_tac M = N in mle_imp_omultiset)
+apply (auto simp add: mle_def intro: munion_less_mono1 munion_less_mono2 munion_less_mono)
+done
+
+lemma omultiset_0 [iff]: "omultiset(0)"
+by (auto simp add: omultiset_def Mult_iff_multiset)
+
+lemma empty_leI [simp]: "omultiset(M) ==> 0 <#= M"
+apply (simp add: mle_def mless_def)
+apply (subgoal_tac "\<exists>i. Ord (i) & M \<in> Mult (field (Memrel (i))) ")
+ prefer 2 apply (simp add: omultiset_def)
+apply (case_tac "M=0", simp_all, clarify)
+apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (field (Memrel (i)), Memrel (i))")
+apply (rule_tac [2] one_step_implies_multirel)
+apply (auto simp add: Mult_iff_multiset)
+done
+
+lemma munion_upper1: "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N"
+apply (subgoal_tac "M +# 0 <#= M +# N")
+apply (rule_tac [2] mle_mono, auto)
+done
+
+ML
+{*
+val munion_ac = thms "munion_ac";
+val funrestrict_subset = thm "funrestrict_subset";
+val funrestrict_type = thm "funrestrict_type";
+val funrestrict_type2 = thm "funrestrict_type2";
+val funrestrict = thm "funrestrict";
+val funrestrict_empty = thm "funrestrict_empty";
+val domain_funrestrict = thm "domain_funrestrict";
+val fun_cons_funrestrict_eq = thm "fun_cons_funrestrict_eq";
+val multiset_fun_iff = thm "multiset_fun_iff";
+val multiset_into_Mult = thm "multiset_into_Mult";
+val Mult_into_multiset = thm "Mult_into_multiset";
+val Mult_iff_multiset = thm "Mult_iff_multiset";
+val multiset_iff_Mult_mset_of = thm "multiset_iff_Mult_mset_of";
+val multiset_0 = thm "multiset_0";
+val multiset_set_of_Finite = thm "multiset_set_of_Finite";
+val mset_of_0 = thm "mset_of_0";
+val mset_is_0_iff = thm "mset_is_0_iff";
+val mset_of_single = thm "mset_of_single";
+val mset_of_union = thm "mset_of_union";
+val mset_of_diff = thm "mset_of_diff";
+val msingle_not_0 = thm "msingle_not_0";
+val msingle_eq_iff = thm "msingle_eq_iff";
+val msingle_multiset = thm "msingle_multiset";
+val Collect_Finite = thms "Collect_Finite";
+val normalize_idem = thm "normalize_idem";
+val normalize_multiset = thm "normalize_multiset";
+val multiset_normalize = thm "multiset_normalize";
+val munion_multiset = thm "munion_multiset";
+val mdiff_multiset = thm "mdiff_multiset";
+val munion_0 = thm "munion_0";
+val munion_commute = thm "munion_commute";
+val munion_assoc = thm "munion_assoc";
+val munion_lcommute = thm "munion_lcommute";
+val mdiff_self_eq_0 = thm "mdiff_self_eq_0";
+val mdiff_0 = thm "mdiff_0";
+val mdiff_0_right = thm "mdiff_0_right";
+val mdiff_union_inverse2 = thm "mdiff_union_inverse2";
+val mcount_type = thm "mcount_type";
+val mcount_0 = thm "mcount_0";
+val mcount_single = thm "mcount_single";
+val mcount_union = thm "mcount_union";
+val mcount_diff = thm "mcount_diff";
+val mcount_elem = thm "mcount_elem";
+val msize_0 = thm "msize_0";
+val msize_single = thm "msize_single";
+val msize_type = thm "msize_type";
+val msize_zpositive = thm "msize_zpositive";
+val msize_int_of_nat = thm "msize_int_of_nat";
+val not_empty_multiset_imp_exist = thm "not_empty_multiset_imp_exist";
+val msize_eq_0_iff = thm "msize_eq_0_iff";
+val setsum_mcount_Int = thm "setsum_mcount_Int";
+val msize_union = thm "msize_union";
+val msize_eq_succ_imp_elem = thm "msize_eq_succ_imp_elem";
+val multiset_equality = thm "multiset_equality";
+val munion_eq_0_iff = thm "munion_eq_0_iff";
+val empty_eq_munion_iff = thm "empty_eq_munion_iff";
+val munion_right_cancel = thm "munion_right_cancel";
+val munion_left_cancel = thm "munion_left_cancel";
+val nat_add_eq_1_cases = thm "nat_add_eq_1_cases";
+val munion_is_single = thm "munion_is_single";
+val msingle_is_union = thm "msingle_is_union";
+val setsum_decr = thm "setsum_decr";
+val setsum_decr2 = thm "setsum_decr2";
+val setsum_decr3 = thm "setsum_decr3";
+val nat_le_1_cases = thm "nat_le_1_cases";
+val succ_pred_eq_self = thm "succ_pred_eq_self";
+val multiset_funrestict = thm "multiset_funrestict";
+val multiset_induct_aux = thm "multiset_induct_aux";
+val multiset_induct2 = thm "multiset_induct2";
+val munion_single_case1 = thm "munion_single_case1";
+val munion_single_case2 = thm "munion_single_case2";
+val multiset_induct = thm "multiset_induct";
+val MCollect_multiset = thm "MCollect_multiset";
+val mset_of_MCollect = thm "mset_of_MCollect";
+val MCollect_mem_iff = thm "MCollect_mem_iff";
+val mcount_MCollect = thm "mcount_MCollect";
+val multiset_partition = thm "multiset_partition";
+val natify_elem_is_self = thm "natify_elem_is_self";
+val munion_eq_conv_diff = thm "munion_eq_conv_diff";
+val melem_diff_single = thm "melem_diff_single";
+val munion_eq_conv_exist = thm "munion_eq_conv_exist";
+val multirel1_type = thm "multirel1_type";
+val multirel1_0 = thm "multirel1_0";
+val multirel1_iff = thm "multirel1_iff";
+val multirel1_mono1 = thm "multirel1_mono1";
+val multirel1_mono2 = thm "multirel1_mono2";
+val multirel1_mono = thm "multirel1_mono";
+val not_less_0 = thm "not_less_0";
+val less_munion = thm "less_munion";
+val multirel1_base = thm "multirel1_base";
+val acc_0 = thm "acc_0";
+val all_accessible = thm "all_accessible";
+val wf_on_multirel1 = thm "wf_on_multirel1";
+val wf_multirel1 = thm "wf_multirel1";
+val multirel_type = thm "multirel_type";
+val multirel_mono = thm "multirel_mono";
+val add_diff_eq = thm "add_diff_eq";
+val mdiff_union_single_conv = thm "mdiff_union_single_conv";
+val diff_add_commute = thm "diff_add_commute";
+val multirel_implies_one_step = thm "multirel_implies_one_step";
+val melem_imp_eq_diff_union = thm "melem_imp_eq_diff_union";
+val msize_eq_succ_imp_eq_union = thm "msize_eq_succ_imp_eq_union";
+val one_step_implies_multirel = thm "one_step_implies_multirel";
+val irrefl_on_multirel = thm "irrefl_on_multirel";
+val trans_on_multirel = thm "trans_on_multirel";
+val multirel_trans = thm "multirel_trans";
+val trans_multirel = thm "trans_multirel";
+val part_ord_multirel = thm "part_ord_multirel";
+val munion_multirel1_mono = thm "munion_multirel1_mono";
+val munion_multirel_mono2 = thm "munion_multirel_mono2";
+val munion_multirel_mono1 = thm "munion_multirel_mono1";
+val munion_multirel_mono = thm "munion_multirel_mono";
+val field_Memrel_mono = thms "field_Memrel_mono";
+val multirel_Memrel_mono = thms "multirel_Memrel_mono";
+val omultiset_is_multiset = thm "omultiset_is_multiset";
+val munion_omultiset = thm "munion_omultiset";
+val mdiff_omultiset = thm "mdiff_omultiset";
+val irrefl_Memrel = thm "irrefl_Memrel";
+val trans_iff_trans_on = thm "trans_iff_trans_on";
+val part_ord_Memrel = thm "part_ord_Memrel";
+val part_ord_mless = thms "part_ord_mless";
+val mless_not_refl = thm "mless_not_refl";
+val mless_irrefl = thms "mless_irrefl";
+val mless_trans = thm "mless_trans";
+val mless_not_sym = thm "mless_not_sym";
+val mless_asym = thm "mless_asym";
+val mle_refl = thm "mle_refl";
+val mle_antisym = thm "mle_antisym";
+val mle_trans = thm "mle_trans";
+val mless_le_iff = thm "mless_le_iff";
+val munion_less_mono2 = thm "munion_less_mono2";
+val munion_less_mono1 = thm "munion_less_mono1";
+val mless_imp_omultiset = thm "mless_imp_omultiset";
+val munion_less_mono = thm "munion_less_mono";
+val mle_imp_omultiset = thm "mle_imp_omultiset";
+val mle_mono = thm "mle_mono";
+val omultiset_0 = thm "omultiset_0";
+val empty_leI = thm "empty_leI";
+val munion_upper1 = thm "munion_upper1";
+*}
+
 end
diff -r 09489fe6989f -r d73f9d49d835 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Mon Sep 13 09:57:25 2004 +0200
+++ b/src/ZF/IsaMakefile	Fri Sep 17 16:08:52 2004 +0200
@@ -135,7 +135,7 @@
 $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.thy \
   Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
   Induct/Datatypes.thy Induct/FoldSet.thy \
-  Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
+  Induct/ListN.thy Induct/Multiset.thy Induct/Mutil.thy \
   Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/ZF Induct