converted ZF/Induct/Multiset to Isar script
authorpaulson
Fri Sep 17 16:08:52 2004 +0200 (2004-09-17)
changeset 15201d73f9d49d835
parent 15200 09489fe6989f
child 15202 d14a6e421a65
converted ZF/Induct/Multiset to Isar script
src/ZF/Arith.thy
src/ZF/Induct/Multiset.ML
src/ZF/Induct/Multiset.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Arith.thy	Mon Sep 13 09:57:25 2004 +0200
     1.2 +++ b/src/ZF/Arith.thy	Fri Sep 17 16:08:52 2004 +0200
     1.3 @@ -307,6 +307,9 @@
     1.4  lemma add_lt_elim1: "[| k#+m < k#+n; m \<in> nat; n \<in> nat |] ==> m < n"
     1.5  by (drule add_lt_elim1_natify, auto)
     1.6  
     1.7 +lemma zero_less_add: "[| n \<in> nat; m \<in> nat |] ==> 0 < m #+ n <-> (0<m | 0<n)"
     1.8 +by (induct_tac "n", auto)
     1.9 +
    1.10  
    1.11  subsection{*Monotonicity of Addition*}
    1.12  
     2.1 --- a/src/ZF/Induct/Multiset.ML	Mon Sep 13 09:57:25 2004 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1483 +0,0 @@
     2.4 -(*  Title:      ZF/Induct/Multiset
     2.5 -    ID:         $Id$
     2.6 -    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     2.7 -
     2.8 -A definitional theory of multisets, including a wellfoundedness 
     2.9 -proof for the multiset order.
    2.10 -
    2.11 -The theory features ordinal multisets and the usual ordering.
    2.12 -
    2.13 -*)
    2.14 -
    2.15 -(* Properties of the original "restrict" from ZF.thy. *)
    2.16 -
    2.17 -Goalw [funrestrict_def,lam_def]
    2.18 -    "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) <= f";
    2.19 -by (blast_tac (claset() addIs [apply_Pair]) 1);
    2.20 -qed "funrestrict_subset";
    2.21 -
    2.22 -val prems = Goalw [funrestrict_def]
    2.23 -    "[| !!x. x:A ==> f`x: B(x) |] ==> funrestrict(f,A) : Pi(A,B)";  
    2.24 -by (rtac lam_type 1);
    2.25 -by (eresolve_tac prems 1);
    2.26 -qed "funrestrict_type";
    2.27 -
    2.28 -Goal "[| f: Pi(C,B);  A<=C |] ==> funrestrict(f,A) : Pi(A,B)";  
    2.29 -by (blast_tac (claset() addIs [apply_type, funrestrict_type]) 1);
    2.30 -qed "funrestrict_type2";
    2.31 -
    2.32 -Goalw [funrestrict_def] "a : A ==> funrestrict(f,A) ` a = f`a";
    2.33 -by (etac beta 1);
    2.34 -qed "funrestrict";
    2.35 -
    2.36 -Goalw [funrestrict_def] "funrestrict(f,0) = 0";
    2.37 -by (Simp_tac 1);
    2.38 -qed "funrestrict_empty";
    2.39 -
    2.40 -Addsimps [funrestrict, funrestrict_empty];
    2.41 -
    2.42 -Goalw [funrestrict_def, lam_def] "domain(funrestrict(f,C)) = C";
    2.43 -by (Blast_tac 1);
    2.44 -qed "domain_funrestrict";
    2.45 -Addsimps [domain_funrestrict];
    2.46 -
    2.47 -Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))";
    2.48 -by (rtac equalityI 1);
    2.49 -by (blast_tac (claset() addIs [apply_Pair, impOfSubs funrestrict_subset]) 2);
    2.50 -by (auto_tac (claset() addSDs [Pi_memberD],
    2.51 -	       simpset() addsimps [funrestrict_def, lam_def]));
    2.52 -qed "fun_cons_funrestrict_eq";
    2.53 -
    2.54 -Addsimps [domain_of_fun];
    2.55 -Delrules [domainE];
    2.56 -
    2.57 -(* A useful simplification rule *)
    2.58 -
    2.59 -Goal "(f:A -> nat-{0}) <-> f:A->nat&(ALL a:A. f`a:nat & 0 < f`a)";
    2.60 -by Safe_tac;
    2.61 -by (res_inst_tac [("B1", "range(f)")] (Pi_mono RS subsetD) 4);
    2.62 -by (auto_tac (claset()  addSIs [Ord_0_lt]
    2.63 -                        addDs [apply_type, Diff_subset RS Pi_mono RS subsetD],
    2.64 -              simpset() addsimps [range_of_fun, apply_iff]));
    2.65 -qed "multiset_fun_iff";
    2.66 -
    2.67 -(** The multiset space  **)
    2.68 -Goalw [multiset_def]
    2.69 - "[| multiset(M); mset_of(M)<=A |] ==> M:Mult(A)";
    2.70 -by (auto_tac (claset(), simpset()
    2.71 -             addsimps [multiset_fun_iff, mset_of_def]));
    2.72 -by (Asm_full_simp_tac 1);
    2.73 -by (res_inst_tac [("B1","nat-{0}")] (FiniteFun_mono RS subsetD) 1);
    2.74 -by (ALLGOALS(Asm_simp_tac));
    2.75 -by (rtac (Finite_into_Fin RSN (2, Fin_mono RS subsetD) RS fun_FiniteFunI) 1);
    2.76 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_fun_iff])));
    2.77 -qed "multiset_into_Mult";
    2.78 -
    2.79 -Goalw [multiset_def, mset_of_def]
    2.80 - "M:Mult(A) ==> multiset(M) & mset_of(M)<=A";
    2.81 -by (ftac FiniteFun_is_fun 1);
    2.82 -by (dtac FiniteFun_domain_Fin 1);
    2.83 -by (ftac FinD 1);
    2.84 -by (Clarify_tac 1);
    2.85 -by (res_inst_tac [("x", "domain(M)")] exI 1);
    2.86 -by (blast_tac (claset() addIs [Fin_into_Finite]) 1);
    2.87 -qed "Mult_into_multiset";
    2.88 -
    2.89 -Goal "M:Mult(A) <-> multiset(M) & mset_of(M)<=A";
    2.90 -by (blast_tac (claset() addDs [Mult_into_multiset]
    2.91 -                        addIs [multiset_into_Mult]) 1);
    2.92 -qed "Mult_iff_multiset";
    2.93 -
    2.94 -Goal "multiset(M) <-> M:Mult(mset_of(M))";
    2.95 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
    2.96 -qed "multiset_iff_Mult_mset_of";
    2.97 -
    2.98 -(** multiset  **)
    2.99 -
   2.100 -(* the empty multiset is 0 *)
   2.101 -
   2.102 -Goal "multiset(0)";
   2.103 -by (auto_tac (claset() addIs (thms"FiniteFun.intros"), 
   2.104 -        simpset()  addsimps [multiset_iff_Mult_mset_of]));
   2.105 -qed "multiset_0";
   2.106 -Addsimps [multiset_0];
   2.107 -
   2.108 -(** mset_of **)
   2.109 -
   2.110 -Goalw [multiset_def, mset_of_def]
   2.111 -"multiset(M) ==> Finite(mset_of(M))";
   2.112 -by Auto_tac;
   2.113 -qed "multiset_set_of_Finite";
   2.114 -Addsimps [multiset_set_of_Finite];
   2.115 -
   2.116 -Goalw [mset_of_def]
   2.117 -"mset_of(0) = 0";
   2.118 -by Auto_tac;
   2.119 -qed "mset_of_0";
   2.120 -AddIffs [mset_of_0];
   2.121 -
   2.122 -Goalw [multiset_def, mset_of_def]
   2.123 -"multiset(M) ==> mset_of(M)=0 <-> M=0";
   2.124 -by Auto_tac;
   2.125 -qed "mset_is_0_iff";
   2.126 -
   2.127 -Goalw [msingle_def, mset_of_def] 
   2.128 -  "mset_of({#a#}) = {a}";
   2.129 -by Auto_tac;
   2.130 -qed "mset_of_single";
   2.131 -AddIffs [mset_of_single];
   2.132 -
   2.133 -Goalw [mset_of_def, munion_def]
   2.134 - "mset_of(M +# N) = mset_of(M) Un mset_of(N)";
   2.135 -by Auto_tac;
   2.136 -qed "mset_of_union";
   2.137 -AddIffs [mset_of_union];
   2.138 -
   2.139 -Goalw [mdiff_def, multiset_def]
   2.140 - "mset_of(M)<=A ==> mset_of(M -# N) <= A";
   2.141 -by (auto_tac (claset(), simpset() addsimps [normalize_def]));
   2.142 -by (rewtac mset_of_def);
   2.143 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff])));
   2.144 -by Auto_tac;
   2.145 -qed "mset_of_diff";
   2.146 -Addsimps [mset_of_diff];
   2.147 -
   2.148 -(* msingle *)
   2.149 -
   2.150 -Goalw [msingle_def] 
   2.151 -  "{#a#} ~= 0 & 0 ~= {#a#}";
   2.152 -by Auto_tac;
   2.153 -qed "msingle_not_0";
   2.154 -AddIffs [msingle_not_0];
   2.155 -
   2.156 -Goalw [msingle_def]
   2.157 - "({#a#} = {#b#}) <->  (a = b)";
   2.158 -by (auto_tac (claset() addEs [equalityE], simpset()));
   2.159 -qed "msingle_eq_iff";
   2.160 -AddIffs [msingle_eq_iff];
   2.161 -
   2.162 -Goalw [multiset_def, msingle_def]  "multiset({#a#})";
   2.163 -by (res_inst_tac [("x", "{a}")] exI 1);
   2.164 -by (auto_tac (claset() addIs [Finite_cons, Finite_0, 
   2.165 -                              fun_extend3], simpset()));
   2.166 -qed "msingle_multiset";
   2.167 -AddIffs [msingle_multiset];
   2.168 -AddTCs [msingle_multiset];
   2.169 -
   2.170 -(** normalize **)
   2.171 -
   2.172 -bind_thm("Collect_Finite", Collect_subset RS subset_Finite);
   2.173 -
   2.174 -Goalw [normalize_def, funrestrict_def, mset_of_def]
   2.175 - "normalize(normalize(f)) = normalize(f)";
   2.176 -by (case_tac "EX A. f : A -> nat & Finite(A)" 1);
   2.177 -by (asm_full_simp_tac (simpset() addsimps []) 1); 
   2.178 -by (Clarify_tac 1); 
   2.179 -by (dres_inst_tac [("x","{x: domain(f) . 0 < f ` x}")] spec 1); 
   2.180 -by (force_tac (claset() addSIs [lam_type], simpset() addsimps [Collect_Finite]) 1);  
   2.181 -by (Asm_simp_tac 1); 
   2.182 -qed "normalize_idem";
   2.183 -
   2.184 -AddIffs [normalize_idem];
   2.185 -
   2.186 -Goalw [multiset_def] 
   2.187 - "multiset(M) ==> normalize(M) = M";
   2.188 -by (rewrite_goals_tac [normalize_def, mset_of_def]);
   2.189 -by (auto_tac (claset(), simpset() 
   2.190 -          addsimps [funrestrict_def, multiset_fun_iff]));
   2.191 -qed "normalize_multiset";
   2.192 -Addsimps [normalize_multiset];
   2.193 -
   2.194 -Goal "multiset(normalize(f))";
   2.195 -by (asm_full_simp_tac (simpset() addsimps [normalize_def]) 1); 
   2.196 -by (rewrite_goals_tac [normalize_def, mset_of_def, multiset_def]);
   2.197 -by Auto_tac;
   2.198 -by (res_inst_tac [("x", "{x:A . 0<f`x}")] exI 1);
   2.199 -by (auto_tac (claset() addIs [Collect_subset RS subset_Finite,
   2.200 -                              funrestrict_type], simpset()));
   2.201 -qed "multiset_normalize";
   2.202 -Addsimps [multiset_normalize];
   2.203 -
   2.204 -(** Typechecking rules for union and difference of multisets **)
   2.205 -
   2.206 -(*????????????????move to Arith??*)
   2.207 -Goal "[| n:nat; m:nat |] ==> 0 < m #+ n <-> (0 < m | 0 < n)";
   2.208 -by (induct_tac "n" 1);
   2.209 -by Auto_tac;
   2.210 -qed "zero_less_add";
   2.211 -
   2.212 -(* union *)
   2.213 -
   2.214 -Goalw [multiset_def]
   2.215 -"[| multiset(M); multiset(N) |] ==> multiset(M +# N)";
   2.216 -by (rewrite_goals_tac [munion_def, mset_of_def]);
   2.217 -by Auto_tac;
   2.218 -by (res_inst_tac [("x", "A Un Aa")] exI 1);
   2.219 -by (auto_tac (claset() addSIs [lam_type] addIs [Finite_Un], 
   2.220 -    simpset() addsimps [multiset_fun_iff, zero_less_add]));
   2.221 -qed "munion_multiset";
   2.222 -Addsimps [munion_multiset];
   2.223 -
   2.224 -(* difference *)
   2.225 -
   2.226 -Goal "multiset(M -# N)";
   2.227 -by (asm_full_simp_tac (simpset() addsimps [mdiff_def]) 1); 
   2.228 -qed "mdiff_multiset";
   2.229 -Addsimps [mdiff_multiset];
   2.230 -
   2.231 -(** Algebraic properties of multisets **)
   2.232 -
   2.233 -(* Union *)
   2.234 -
   2.235 -Goalw [multiset_def]
   2.236 -  "multiset(M) ==> M +# 0 = M & 0 +# M = M";
   2.237 -by (auto_tac (claset(), simpset() addsimps [munion_def, mset_of_def]));
   2.238 -qed "munion_0";
   2.239 -Addsimps [munion_0];
   2.240 -
   2.241 -Goalw [multiset_def] "M +# N = N +# M";
   2.242 -by (auto_tac (claset() addSIs [lam_cong],  simpset() addsimps [munion_def]));
   2.243 -qed "munion_commute";
   2.244 -
   2.245 -Goalw [multiset_def] "(M +# N) +# K = M +# (N +# K)";
   2.246 -by (rewrite_goals_tac [munion_def, mset_of_def]);
   2.247 -by (rtac lam_cong 1);
   2.248 -by Auto_tac;
   2.249 -qed "munion_assoc";
   2.250 -
   2.251 -Goalw [multiset_def] "M +# (N +# K) = N +# (M +# K)";
   2.252 -by (rewrite_goals_tac [munion_def, mset_of_def]); 
   2.253 -by (rtac lam_cong 1);
   2.254 -by Auto_tac;
   2.255 -qed "munion_lcommute";
   2.256 -
   2.257 -val munion_ac = [munion_commute, munion_assoc, munion_lcommute];
   2.258 -
   2.259 -(* Difference *)
   2.260 -
   2.261 -Goalw [mdiff_def] "M -# M = 0";
   2.262 -by (simp_tac (simpset() addsimps [normalize_def, mset_of_def]) 1);
   2.263 -qed "mdiff_self_eq_0";
   2.264 -Addsimps [mdiff_self_eq_0];
   2.265 -
   2.266 -Goalw [multiset_def] "0 -# M = 0";
   2.267 -by (rewrite_goals_tac [mdiff_def, normalize_def]);
   2.268 -by (auto_tac (claset(), simpset() 
   2.269 -         addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
   2.270 -qed "mdiff_0";
   2.271 -Addsimps [mdiff_0]; 
   2.272 -
   2.273 -Goalw [multiset_def] "multiset(M) ==> M -# 0 = M";
   2.274 -by (rewrite_goals_tac [mdiff_def, normalize_def]);
   2.275 -by (auto_tac (claset(), simpset() 
   2.276 -         addsimps [multiset_fun_iff, mset_of_def, funrestrict_def]));
   2.277 -qed "mdiff_0_right";
   2.278 -Addsimps [mdiff_0_right]; 
   2.279 -
   2.280 -Goal "multiset(M) ==> M +# {#a#} -# {#a#} = M";
   2.281 -by (rewrite_goals_tac [multiset_def, munion_def, mdiff_def, 
   2.282 -                       msingle_def, normalize_def, mset_of_def]);
   2.283 -by (auto_tac (claset(), 
   2.284 -       simpset() addcongs [if_cong]
   2.285 -		 addsimps [ltD, multiset_fun_iff,
   2.286 -                           funrestrict_def, subset_Un_iff2 RS iffD1]));
   2.287 -by (force_tac (claset() addSIs [lam_type], simpset()) 2);   
   2.288 -by (subgoal_tac "{x \\<in> A \\<union> {a} . x \\<noteq> a \\<and> x \\<in> A} = A" 2);
   2.289 -by (rtac fun_extension 1);
   2.290 -by Auto_tac; 
   2.291 -by (dres_inst_tac [("x","A Un {a}")] spec 1);
   2.292 -by (asm_full_simp_tac (simpset() addsimps [Finite_Un]) 1); 
   2.293 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.294 -qed "mdiff_union_inverse2";
   2.295 -Addsimps [mdiff_union_inverse2];
   2.296 -
   2.297 -(** Count of elements **)
   2.298 -
   2.299 -Goalw [multiset_def] "multiset(M) ==> mcount(M, a):nat";
   2.300 -by (rewrite_goals_tac [mcount_def, mset_of_def]);
   2.301 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.302 -qed "mcount_type";
   2.303 -AddTCs [mcount_type];
   2.304 -Addsimps [mcount_type];
   2.305 -
   2.306 -Goalw [mcount_def]  "mcount(0, a) = 0";
   2.307 -by Auto_tac;
   2.308 -qed "mcount_0";
   2.309 -Addsimps [mcount_0];
   2.310 -
   2.311 -Goalw [mcount_def, mset_of_def, msingle_def]
   2.312 -"mcount({#b#}, a) = (if a=b then 1 else 0)";
   2.313 -by Auto_tac;
   2.314 -qed "mcount_single";
   2.315 -Addsimps [mcount_single];
   2.316 -
   2.317 -Goalw [multiset_def]
   2.318 -"[| multiset(M); multiset(N) |] \
   2.319 -\ ==>  mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)";
   2.320 -by (auto_tac (claset(), simpset() addsimps 
   2.321 -                      [multiset_fun_iff, mcount_def, 
   2.322 -                       munion_def, mset_of_def ]));
   2.323 -qed "mcount_union";
   2.324 -Addsimps [mcount_union];
   2.325 -
   2.326 -Goalw [multiset_def]
   2.327 -"multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)";
   2.328 -by (auto_tac (claset() addSDs [not_lt_imp_le], 
   2.329 -      simpset() addsimps [mdiff_def, multiset_fun_iff, 
   2.330 -                          mcount_def, normalize_def, mset_of_def]));
   2.331 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.332 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.333 -qed "mcount_diff";
   2.334 -Addsimps [mcount_diff];
   2.335 -
   2.336 -
   2.337 -Goalw [multiset_def]
   2.338 - "[| multiset(M); a:mset_of(M) |] ==> 0 < mcount(M, a)";
   2.339 -by (Clarify_tac 1);
   2.340 -by (rewrite_goals_tac [mcount_def, mset_of_def]);
   2.341 -by (Asm_full_simp_tac 1);
   2.342 -by (asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]) 1); 
   2.343 -qed "mcount_elem";
   2.344 -
   2.345 -(** msize **)
   2.346 -
   2.347 -Goalw [msize_def] "msize(0) = #0";
   2.348 -by Auto_tac;
   2.349 -qed "msize_0";
   2.350 -AddIffs [msize_0];
   2.351 -
   2.352 -Goalw [msize_def] "msize({#a#}) = #1";
   2.353 -by (rewrite_goals_tac [msingle_def, mcount_def, mset_of_def]);
   2.354 -by (auto_tac (claset(), simpset() addsimps [Finite_0]));
   2.355 -qed "msize_single";
   2.356 -AddIffs [msize_single];
   2.357 -
   2.358 -Goalw [msize_def] "msize(M):int";
   2.359 -by Auto_tac;
   2.360 -qed "msize_type";
   2.361 -Addsimps [msize_type];
   2.362 -AddTCs [msize_type];
   2.363 -
   2.364 -Goalw [msize_def] "multiset(M)==> #0 $<= msize(M)";
   2.365 -by (auto_tac (claset() addIs [g_zpos_imp_setsum_zpos], simpset()));
   2.366 -qed "msize_zpositive";
   2.367 -
   2.368 -Goal "multiset(M) ==> EX n:nat. msize(M)= $# n";
   2.369 -by (rtac not_zneg_int_of 1);
   2.370 -by (ALLGOALS(asm_simp_tac 
   2.371 -      (simpset() addsimps [msize_type RS znegative_iff_zless_0,
   2.372 -                          not_zless_iff_zle,msize_zpositive])));
   2.373 -qed "msize_int_of_nat";
   2.374 -
   2.375 -Goalw [multiset_def]
   2.376 - "[| M~=0; multiset(M) |] ==> EX a:mset_of(M). 0 < mcount(M, a)";
   2.377 -by (etac not_emptyE 1);
   2.378 -by (rewrite_goal_tac [mset_of_def, mcount_def] 1);
   2.379 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.380 -by (blast_tac (claset() addSDs [fun_is_rel]) 1);
   2.381 -qed "not_empty_multiset_imp_exist";
   2.382 -
   2.383 -Goalw [msize_def] "multiset(M) ==> msize(M)=#0 <-> M=0";
   2.384 -by Auto_tac;
   2.385 -by (res_inst_tac [("Pa", "setsum(?u,?v) ~= #0")] swap 1);
   2.386 -by (Blast_tac 1);
   2.387 -by (dtac not_empty_multiset_imp_exist 1);
   2.388 -by (ALLGOALS(Clarify_tac));
   2.389 -by (subgoal_tac "Finite(mset_of(M) - {a})" 1);
   2.390 -by (asm_simp_tac (simpset() addsimps [Finite_Diff]) 2);
   2.391 -by (subgoal_tac "setsum(%x. $# mcount(M, x), cons(a, mset_of(M)-{a}))=#0" 1);
   2.392 -by (asm_simp_tac (simpset() addsimps [cons_Diff]) 2);
   2.393 -by (Asm_full_simp_tac 1);
   2.394 -by (subgoal_tac "#0 $<= setsum(%x. $# mcount(M, x), mset_of(M) - {a})" 1);
   2.395 -by (rtac g_zpos_imp_setsum_zpos 2);
   2.396 -by (auto_tac (claset(), simpset() 
   2.397 -              addsimps [Finite_Diff, not_zless_iff_zle RS iff_sym, 
   2.398 -                        znegative_iff_zless_0 RS iff_sym]));
   2.399 -by (dtac (rotate_prems 1 not_zneg_int_of) 1);
   2.400 -by (auto_tac (claset(), simpset() delsimps [int_of_0]
   2.401 -       addsimps [int_of_add RS sym, int_of_0 RS sym]));
   2.402 -qed "msize_eq_0_iff";
   2.403 -
   2.404 -Goal
   2.405 -"Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N)) \
   2.406 -\            = setsum(%a. $# mcount(N, a), A)";
   2.407 -by (etac Finite_induct 1);
   2.408 -by Auto_tac;
   2.409 -by (subgoal_tac "Finite(B Int mset_of(N))" 1);
   2.410 -by (blast_tac (claset() addIs [subset_Finite]) 2);
   2.411 -by (auto_tac (claset(), 
   2.412 -         simpset() addsimps [mcount_def, Int_cons_left]));
   2.413 -qed "setsum_mcount_Int";
   2.414 -
   2.415 -Goalw [msize_def]
   2.416 -"[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)";
   2.417 -by (asm_simp_tac (simpset() addsimps
   2.418 -        [setsum_Un , setsum_addf, int_of_add, setsum_mcount_Int]) 1);
   2.419 -by (stac Int_commute 1);
   2.420 -by (asm_simp_tac (simpset() addsimps [setsum_mcount_Int]) 1);
   2.421 -qed "msize_union"; 
   2.422 -Addsimps [msize_union];
   2.423 -
   2.424 -Goalw [msize_def] "[|msize(M)= $# succ(n); n:nat|] ==> EX a. a:mset_of(M)";
   2.425 -by (blast_tac (claset() addDs [setsum_succD]) 1);
   2.426 -qed "msize_eq_succ_imp_elem";
   2.427 -
   2.428 -(** Equality of multisets **)
   2.429 -
   2.430 -Goalw [multiset_def] 
   2.431 -"[| multiset(M); multiset(N); ALL a. mcount(M, a)=mcount(N, a) |] \
   2.432 -\   ==> mset_of(M)=mset_of(N)";
   2.433 -by (rtac sym 1 THEN rtac equalityI 1);
   2.434 -by (rewrite_goals_tac [mcount_def, mset_of_def]);
   2.435 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.436 -by (ALLGOALS(dres_inst_tac [("x", "x")] spec));
   2.437 -by (case_tac "x:Aa" 2 THEN case_tac "x:A" 1);
   2.438 -by Auto_tac;
   2.439 -qed "equality_lemma";
   2.440 -
   2.441 -Goal  
   2.442 -"[| multiset(M); multiset(N) |]==> M=N<->(ALL a. mcount(M, a)=mcount(N, a))";
   2.443 -by Auto_tac;
   2.444 -by (subgoal_tac "mset_of(M) = mset_of(N)" 1);
   2.445 -by (blast_tac (claset() addIs [equality_lemma]) 2);
   2.446 -by (rewrite_goals_tac [multiset_def, mset_of_def]);
   2.447 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.448 -by (rtac fun_extension 1);
   2.449 -by (Blast_tac 1 THEN Blast_tac 1);
   2.450 -by (dres_inst_tac [("x", "x")] spec 1);
   2.451 -by (auto_tac (claset(), simpset() addsimps [mcount_def, mset_of_def]));
   2.452 -qed "multiset_equality";
   2.453 -
   2.454 -(** More algebraic properties of multisets **)
   2.455 -
   2.456 -Goal "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)";
   2.457 -by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
   2.458 -qed "munion_eq_0_iff";
   2.459 -Addsimps [munion_eq_0_iff];
   2.460 -
   2.461 -Goal "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)";
   2.462 -by (rtac iffI 1 THEN dtac sym 1);
   2.463 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_equality])));
   2.464 -qed "empty_eq_munion_iff";
   2.465 -Addsimps [empty_eq_munion_iff];
   2.466 -
   2.467 -Goal 
   2.468 -"[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)";
   2.469 -by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
   2.470 -qed "munion_right_cancel";
   2.471 -Addsimps [munion_right_cancel];
   2.472 -
   2.473 -Goal 
   2.474 -"[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)";
   2.475 -by (auto_tac (claset(), simpset() addsimps [multiset_equality]));
   2.476 -qed "munion_left_cancel";
   2.477 -Addsimps [munion_left_cancel];
   2.478 -
   2.479 -Goal "[| m:nat; n:nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)";
   2.480 -by (induct_tac "n" 1 THEN Auto_tac);
   2.481 -qed "nat_add_eq_1_cases";
   2.482 -
   2.483 -Goal "[|multiset(M); multiset(N)|]                                     \
   2.484 -\ ==> (M +# N = {#a#}) <->  (M={#a#} & N=0) | (M = 0 & N = {#a#})";
   2.485 -by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
   2.486 -by Safe_tac;
   2.487 -by (ALLGOALS(Asm_full_simp_tac));
   2.488 -by (case_tac "aa=a" 1);
   2.489 -by (dres_inst_tac [("x", "aa")] spec 2);
   2.490 -by (dres_inst_tac [("x", "a")] spec 1);
   2.491 -by (asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases]) 1);
   2.492 -by (Asm_full_simp_tac 1);
   2.493 -by (case_tac "aaa=aa" 1);
   2.494 -by (Asm_full_simp_tac 1);
   2.495 -by (dres_inst_tac [("x", "aa")] spec 1);
   2.496 -by (asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases]) 1);
   2.497 -by (case_tac "aaa=a" 1);
   2.498 -by (dres_inst_tac [("x", "aa")] spec 4);
   2.499 -by (dres_inst_tac [("x", "a")] spec 3);
   2.500 -by (dres_inst_tac [("x", "aaa")] spec 2);
   2.501 -by (dres_inst_tac [("x", "aa")] spec 1);
   2.502 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_add_eq_1_cases])));
   2.503 -qed "munion_is_single";
   2.504 -
   2.505 -Goal "[| multiset(M); multiset(N) |] \
   2.506 -\ ==> ({#a#} = M +# N) <-> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)";
   2.507 -by (simp_tac (simpset() addsimps [sym]) 1);
   2.508 -by (subgoal_tac "({#a#} = M +# N) <-> (M +# N = {#a#})" 1);
   2.509 -by (asm_simp_tac (simpset() addsimps [munion_is_single]) 1);
   2.510 -by (REPEAT(blast_tac (claset() addDs [sym]) 1));
   2.511 -qed "msingle_is_union";
   2.512 -
   2.513 -(** Towards induction over multisets **)
   2.514 -
   2.515 -Goalw [multiset_def]  
   2.516 -"Finite(A) \
   2.517 -\ ==>  (ALL M. multiset(M) -->                                     \
   2.518 -\ (ALL a:mset_of(M). setsum(%x. $# mcount(M(a:=M`a #- 1), x), A) = \
   2.519 -\ (if a:A then setsum(%x. $# mcount(M, x), A) $- #1                \
   2.520 -\          else setsum(%x. $# mcount(M, x), A))))";
   2.521 -by (etac Finite_induct 1);
   2.522 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.523 -by (rewrite_goals_tac [mset_of_def, mcount_def]);
   2.524 -by (case_tac "x:A" 1);
   2.525 -by Auto_tac;
   2.526 -by (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1" 1);
   2.527 -by (etac ssubst 1);
   2.528 -by (rtac int_of_diff 1);
   2.529 -by Auto_tac;
   2.530 -qed "setsum_decr";
   2.531 -
   2.532 -(*FIXME: we should not have to rename x to x' below!  There's a bug in the
   2.533 -  interaction between simproc inteq_cancel_numerals and the simplifier.*)
   2.534 -Goalw [multiset_def]
   2.535 -     "Finite(A) \
   2.536 -\     ==> ALL M. multiset(M) --> (ALL a:mset_of(M).            \
   2.537 -\          setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) = \
   2.538 -\          (if a:A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a     \
   2.539 -\           else setsum(%x'. $# mcount(M, x'), A)))";
   2.540 -by (etac Finite_induct 1);
   2.541 -by (auto_tac (claset(), 
   2.542 -              simpset() addsimps [multiset_fun_iff, 
   2.543 -                                  mcount_def, mset_of_def]));
   2.544 -qed "setsum_decr2";
   2.545 -
   2.546 -Goal "[| Finite(A); multiset(M); a:mset_of(M) |] \
   2.547 -\     ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) = \
   2.548 -\         (if a:A then setsum(%x. $# mcount(M, x), A) $- $# M`a\
   2.549 -\          else setsum(%x. $# mcount(M, x), A))";
   2.550 -by (subgoal_tac "setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A-{a}) = \
   2.551 -\                setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}),x),A)" 1);
   2.552 -by (rtac (setsum_Diff RS sym) 2);
   2.553 -by (REPEAT(asm_simp_tac (simpset() addsimps [mcount_def, mset_of_def]) 2));
   2.554 -by (rtac sym 1 THEN rtac ssubst 1);
   2.555 -by (Blast_tac 1);
   2.556 -by (rtac sym 1 THEN dtac setsum_decr2 1);
   2.557 -by Auto_tac;
   2.558 -qed "setsum_decr3";
   2.559 -
   2.560 -Goal "n:nat ==> n le 1 <-> (n=0 | n=1)";
   2.561 -by (auto_tac (claset() addEs [natE], simpset()));
   2.562 -qed "nat_le_1_cases";
   2.563 -
   2.564 -Goal "[| 0<n; n:nat |] ==> succ(n #- 1) = n";
   2.565 -by (subgoal_tac "1 le n" 1);
   2.566 -by (dtac add_diff_inverse2 1);
   2.567 -by Auto_tac;
   2.568 -qed "succ_pred_eq_self";
   2.569 -
   2.570 -val major::prems = Goal
   2.571 -  "[| n:nat; P(0); \
   2.572 -\   (!!M a. [| multiset(M); a~:mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))); \
   2.573 -\   (!!M b. [| multiset(M); b:mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))) |] \
   2.574 - \   ==> (ALL M. multiset(M)--> \
   2.575 -\ (setsum(%x. $# mcount(M, x), {x:mset_of(M). 0 < M`x}) = $# n) --> P(M))";
   2.576 -by (rtac (major RS nat_induct) 1);
   2.577 -by (ALLGOALS(Clarify_tac));
   2.578 -by (ftac msize_eq_0_iff 1);
   2.579 -by (auto_tac (claset(), 
   2.580 -              simpset() addsimps [mset_of_def, multiset_def,  
   2.581 -                                  multiset_fun_iff, msize_def]@prems));
   2.582 -by (subgoal_tac "setsum(%x. $# mcount(M, x), A)=$# succ(x)" 1);
   2.583 -by (dtac setsum_succD 1 THEN Auto_tac);
   2.584 -by (case_tac "1 <M`a" 1);
   2.585 -by (dtac not_lt_imp_le 2);
   2.586 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nat_le_1_cases])));
   2.587 -by (subgoal_tac "M=(M(a:=M`a #- 1))(a:=(M(a:=M`a #- 1))`a #+ 1)" 1);
   2.588 -by (res_inst_tac [("A","A"),("B","%x. nat"),("D","%x. nat")] fun_extension 2);
   2.589 -by (REPEAT(rtac update_type 3));
   2.590 -by (ALLGOALS(Asm_simp_tac));
   2.591 -by (Clarify_tac 2);
   2.592 -by (rtac (succ_pred_eq_self RS sym) 2);
   2.593 -by (ALLGOALS(Asm_simp_tac));
   2.594 -by (rtac subst 1 THEN rtac sym 1 THEN Blast_tac 1 THEN resolve_tac prems 1);
   2.595 -by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
   2.596 -by (res_inst_tac [("x", "A")] exI 1);
   2.597 -by (force_tac (claset() addIs [update_type], simpset()) 1);
   2.598 -by (asm_simp_tac (simpset() addsimps [mset_of_def, mcount_def]) 1);
   2.599 -by (dres_inst_tac [("x", "M(a := M ` a #- 1)")] spec 1);
   2.600 -by (dtac mp 1 THEN dtac mp 2);
   2.601 -by (ALLGOALS(Asm_full_simp_tac));
   2.602 -by (res_inst_tac [("x", "A")] exI 1);
   2.603 -by (auto_tac (claset() addIs [update_type], simpset()));
   2.604 -by (subgoal_tac "Finite({x:cons(a, A). x~=a-->0<M`x})" 1);
   2.605 -by (blast_tac(claset() addIs [Collect_subset RS subset_Finite,Finite_cons])2);
   2.606 -by (dres_inst_tac [("A", "{x:cons(a, A). x~=a-->0<M`x}")] setsum_decr 1);
   2.607 -by (dres_inst_tac [("x", "M")] spec 1);
   2.608 -by (subgoal_tac "multiset(M)" 1);
   2.609 -by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
   2.610 -by (res_inst_tac [("x", "A")] exI 2);
   2.611 -by (Force_tac 2);
   2.612 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [mset_of_def])));
   2.613 -by (dres_inst_tac [("psi", "ALL x:A. ?u(x)")] asm_rl 1);
   2.614 -by (dres_inst_tac [("x", "a")] bspec 1);
   2.615 -by (Asm_simp_tac 1);
   2.616 -by (subgoal_tac "cons(a, A)= A" 1);
   2.617 -by (Blast_tac 2);
   2.618 -by (Asm_full_simp_tac 1);
   2.619 -by (subgoal_tac "M=cons(<a, M`a>, funrestrict(M, A-{a}))" 1);
   2.620 -by (rtac  fun_cons_funrestrict_eq 2);
   2.621 -by (subgoal_tac "cons(a, A-{a}) = A" 2);
   2.622 -by (REPEAT(Force_tac 2));
   2.623 -by (res_inst_tac [("a", "cons(<a, 1>, funrestrict(M, A - {a}))")] ssubst 1);
   2.624 -by (Asm_full_simp_tac 1);
   2.625 -by (subgoal_tac "multiset(funrestrict(M, A - {a}))" 1);
   2.626 -by (simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
   2.627 -by (res_inst_tac [("x", "A-{a}")] exI 2);
   2.628 -by Safe_tac;
   2.629 -by (res_inst_tac [("A", "A-{a}")] apply_type 3);
   2.630 -by (asm_simp_tac (simpset() addsimps [funrestrict]) 5);
   2.631 -by (REPEAT(blast_tac (claset() addIs [Finite_Diff, funrestrict_type]) 2));;
   2.632 -by (resolve_tac prems 1);
   2.633 -by (assume_tac 1);
   2.634 -by (asm_full_simp_tac (simpset() addsimps [mset_of_def]) 1);
   2.635 -by (dres_inst_tac [("x", "funrestrict(M, A-{a})")] spec 1);
   2.636 -by (dtac mp 1);
   2.637 -by (res_inst_tac [("x", "A-{a}")] exI 1);
   2.638 -by (auto_tac (claset() addIs [Finite_Diff, funrestrict_type], 
   2.639 -             simpset() addsimps [funrestrict]));
   2.640 -by (forw_inst_tac [("A", "A"), ("M", "M"), ("a", "a")] setsum_decr3 1);
   2.641 -by (asm_simp_tac  (simpset() addsimps [multiset_def, multiset_fun_iff]) 1);
   2.642 -by (Blast_tac 1);
   2.643 -by (asm_simp_tac (simpset() addsimps [mset_of_def]) 1);
   2.644 -by (dres_inst_tac [("b", "if ?u then ?v else ?w")] sym 1);
   2.645 -by (ALLGOALS Asm_full_simp_tac);
   2.646 -by (subgoal_tac "{x:A - {a} . 0 < funrestrict(M, A - {x}) ` x} = A - {a}" 1);
   2.647 -by (auto_tac (claset() addSIs [setsum_cong], 
   2.648 -              simpset() addsimps [zdiff_eq_iff, 
   2.649 -               zadd_commute, multiset_def, multiset_fun_iff,mset_of_def]));
   2.650 -qed "multiset_induct_aux";
   2.651 -
   2.652 -val major::prems = Goal
   2.653 -  "[| multiset(M); P(0); \
   2.654 -\   (!!M a. [| multiset(M); a~:mset_of(M); P(M) |] ==> P(cons(<a, 1>, M)));  \
   2.655 -\   (!!M b. [| multiset(M); b:mset_of(M);  P(M) |] ==> P(M(b:= M`b #+ 1))) |] \
   2.656 - \   ==> P(M)";
   2.657 -by (subgoal_tac "EX n:nat. setsum(\\<lambda>x. $# mcount(M, x), \
   2.658 -              \ {x : mset_of(M) . 0 < M ` x}) = $# n" 1);
   2.659 -by (rtac not_zneg_int_of 2);
   2.660 -by (ALLGOALS(asm_simp_tac (simpset() 
   2.661 -        addsimps [znegative_iff_zless_0, not_zless_iff_zle])));
   2.662 -by (rtac g_zpos_imp_setsum_zpos 2);
   2.663 -by (blast_tac (claset() addIs [major RS multiset_set_of_Finite, 
   2.664 -                              Collect_subset RS subset_Finite]) 2);
   2.665 -by (asm_full_simp_tac (simpset() addsimps [multiset_def, multiset_fun_iff]) 2);
   2.666 -by (Clarify_tac 1);
   2.667 -by (rtac (multiset_induct_aux RS spec RS mp RS mp) 1);
   2.668 -by (resolve_tac prems 4);
   2.669 -by (resolve_tac prems 3);
   2.670 -by (auto_tac (claset(), simpset() addsimps major::prems));
   2.671 -qed "multiset_induct2";
   2.672 -
   2.673 -Goalw [multiset_def, msingle_def] 
   2.674 - "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)";
   2.675 -by (auto_tac (claset(), simpset() addsimps [munion_def]));
   2.676 -by (rewtac mset_of_def);
   2.677 -by (Asm_full_simp_tac 1);
   2.678 -by (rtac fun_extension 1 THEN rtac lam_type 1);
   2.679 -by (ALLGOALS(Asm_full_simp_tac));
   2.680 -by (auto_tac (claset(), simpset()  
   2.681 -        addsimps [multiset_fun_iff, fun_extend_apply]));
   2.682 -by (dres_inst_tac [("c", "a"), ("b", "1")] fun_extend3 1);
   2.683 -by (stac Un_commute 3);
   2.684 -by (auto_tac (claset(), simpset() addsimps [cons_eq]));
   2.685 -qed "munion_single_case1";
   2.686 -
   2.687 -Goalw [multiset_def]
   2.688 -"[| multiset(M); a:mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)";
   2.689 -by (auto_tac (claset(),  simpset() 
   2.690 -     addsimps [munion_def, multiset_fun_iff, msingle_def]));
   2.691 -by (rewtac mset_of_def);
   2.692 -by (Asm_full_simp_tac 1);
   2.693 -by (subgoal_tac "A Un {a} = A" 1);
   2.694 -by (rtac fun_extension 1);
   2.695 -by (auto_tac (claset() addDs [domain_type] 
   2.696 -                       addIs [lam_type, update_type], simpset()));
   2.697 -qed "munion_single_case2";
   2.698 -
   2.699 -(* Induction principle for multisets *)
   2.700 -
   2.701 -val major::prems = Goal
   2.702 -  "[| multiset(M); P(0); \
   2.703 -\   (!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})) |] \
   2.704 - \   ==> P(M)";
   2.705 -by (rtac multiset_induct2 1);
   2.706 -by (ALLGOALS(asm_simp_tac (simpset() addsimps major::prems)));
   2.707 -by (forw_inst_tac [("a1", "b")] (munion_single_case2 RS sym) 2);
   2.708 -by (forw_inst_tac [("a1", "a")] (munion_single_case1 RS sym) 1);
   2.709 -by (ALLGOALS(Asm_full_simp_tac));
   2.710 -by (REPEAT(blast_tac (claset() addIs prems ) 1));
   2.711 -qed "multiset_induct";
   2.712 -
   2.713 -(** MCollect **)
   2.714 -
   2.715 -Goalw [MCollect_def, multiset_def, mset_of_def]
   2.716 -  "multiset(M) ==> multiset({# x:M. P(x)#})";
   2.717 -by (Clarify_tac 1);
   2.718 -by (res_inst_tac [("x", "{x:A. P(x)}")] exI 1);
   2.719 -by (auto_tac (claset()  addDs [CollectD1 RSN (2,apply_type)]
   2.720 -                        addIs [Collect_subset RS subset_Finite,
   2.721 -                               funrestrict_type],
   2.722 -              simpset()));
   2.723 -qed "MCollect_multiset";
   2.724 -Addsimps [MCollect_multiset];
   2.725 -
   2.726 -Goalw [mset_of_def, MCollect_def]
   2.727 - "multiset(M) ==> mset_of({# x:M. P(x) #}) <= mset_of(M)";
   2.728 -by (auto_tac (claset(), 
   2.729 -              simpset() addsimps [multiset_def, funrestrict_def]));
   2.730 -qed "mset_of_MCollect";
   2.731 -Addsimps [mset_of_MCollect];
   2.732 -
   2.733 -Goalw [MCollect_def, mset_of_def]
   2.734 - "x:mset_of({#x:M. P(x)#}) <->  x:mset_of(M) & P(x)";
   2.735 -by Auto_tac;
   2.736 -qed "MCollect_mem_iff";
   2.737 -AddIffs [MCollect_mem_iff];
   2.738 - 
   2.739 -Goalw [mcount_def, MCollect_def, mset_of_def]
   2.740 - "mcount({# x:M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)";
   2.741 -by Auto_tac;
   2.742 -qed "mcount_MCollect";
   2.743 -Addsimps [mcount_MCollect];
   2.744 -
   2.745 -Goal "multiset(M) ==> M = {# x:M. P(x) #} +# {# x:M. ~ P(x) #}";
   2.746 -by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
   2.747 -qed "multiset_partition";
   2.748 -
   2.749 -Goalw [multiset_def, mset_of_def]
   2.750 - "[| multiset(M); a:mset_of(M) |] ==> natify(M`a) = M`a";
   2.751 -by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff]));
   2.752 -qed "natify_elem_is_self";
   2.753 -Addsimps [natify_elem_is_self];
   2.754 -
   2.755 -(* and more algebraic laws on multisets *)
   2.756 -
   2.757 -Goal "[| multiset(M); multiset(N) |] \
   2.758 -\ ==>  (M +# {#a#} = N +# {#b#}) <->  (M = N & a = b | \
   2.759 -\      M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})";
   2.760 -by (asm_full_simp_tac (simpset() delsimps [mcount_single]
   2.761 -                                 addsimps [multiset_equality]) 1);
   2.762 -by (rtac iffI 1 THEN etac disjE 2 THEN etac conjE 3);
   2.763 -by (case_tac "a=b" 1);
   2.764 -by Auto_tac;
   2.765 -by (dres_inst_tac [("x", "a")] spec 1);
   2.766 -by (dres_inst_tac [("x", "b")] spec 2);
   2.767 -by (dres_inst_tac [("x", "aa")] spec 3);
   2.768 -by (dres_inst_tac [("x", "a")] spec 4);
   2.769 -by Auto_tac;
   2.770 -by (ALLGOALS(subgoal_tac "mcount(N,a):nat"));
   2.771 -by (etac natE 3 THEN etac natE 1);
   2.772 -by Auto_tac;
   2.773 -qed "munion_eq_conv_diff";
   2.774 -
   2.775 -Goalw [multiset_def]
   2.776 -"multiset(M) ==> \
   2.777 -\ k:mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k~= a & k:mset_of(M))";
   2.778 -by (rewrite_goals_tac [normalize_def, mset_of_def, msingle_def, 
   2.779 -                        mdiff_def, mcount_def]);
   2.780 -by (auto_tac (claset() addDs [domain_type] 
   2.781 -                       addIs [zero_less_diff RS iffD1],
   2.782 -              simpset() addsimps 
   2.783 -                     [multiset_fun_iff, apply_iff]));
   2.784 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.785 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.786 -by (force_tac (claset() addSIs [lam_type], simpset()) 1);   
   2.787 -qed "melem_diff_single";
   2.788 -
   2.789 -Goal
   2.790 -"[| M:Mult(A); N:Mult(A) |] \
   2.791 -\ ==> (M +# {#a#} = N +# {#b#}) <-> \
   2.792 -\     (M=N & a=b | (EX K:Mult(A). M= K +# {#b#} & N=K +# {#a#}))";
   2.793 -by (auto_tac (claset(), 
   2.794 -              simpset() addsimps [Bex_def, Mult_iff_multiset,
   2.795 -                  melem_diff_single, munion_eq_conv_diff]));
   2.796 -qed "munion_eq_conv_exist";
   2.797 -
   2.798 -(** multiset orderings **)
   2.799 -
   2.800 -(* multiset on a domain A are finite functions from A to nat-{0} *)
   2.801 -
   2.802 -
   2.803 -(* multirel1 type *)
   2.804 -
   2.805 -Goalw [multirel1_def]
   2.806 -"multirel1(A, r) <= Mult(A)*Mult(A)";
   2.807 -by Auto_tac;
   2.808 -qed "multirel1_type";
   2.809 -
   2.810 -Goalw [multirel1_def] "multirel1(0, r) =0";
   2.811 -by Auto_tac;
   2.812 -qed "multirel1_0";
   2.813 -AddIffs [multirel1_0];
   2.814 -
   2.815 -Goalw [multirel1_def]
   2.816 -" <N, M>:multirel1(A, r) <-> \
   2.817 -\ (EX a. a:A &                                       \
   2.818 -\ (EX M0. M0:Mult(A) & (EX K. K:Mult(A) &  \
   2.819 -\  M=M0 +# {#a#} & N=M0 +# K & (ALL b:mset_of(K). <b,a>:r))))";
   2.820 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset, Ball_def, Bex_def]));
   2.821 -qed "multirel1_iff";
   2.822 -
   2.823 -(* Monotonicity of multirel1 *)
   2.824 -
   2.825 -Goalw [multirel1_def]  "A<=B ==> multirel1(A, r)<=multirel1(B, r)";
   2.826 -by (auto_tac (claset(), simpset() addsimps []));
   2.827 -by (ALLGOALS(asm_full_simp_tac(simpset() 
   2.828 -    addsimps [Un_subset_iff, Mult_iff_multiset])));
   2.829 -by (res_inst_tac [("x", "a")] bexI 3);
   2.830 -by (res_inst_tac [("x", "M0")] bexI 3);
   2.831 -by (Asm_simp_tac 3);
   2.832 -by (res_inst_tac [("x", "K")] bexI 3);
   2.833 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [Mult_iff_multiset])));
   2.834 -by Auto_tac;
   2.835 -qed "multirel1_mono1";
   2.836 -
   2.837 -Goalw [multirel1_def] "r<=s ==> multirel1(A,r)<=multirel1(A, s)";
   2.838 -by (auto_tac (claset(), simpset() addsimps []));
   2.839 -by (res_inst_tac [("x", "a")] bexI 1);
   2.840 -by (res_inst_tac [("x", "M0")] bexI 1);
   2.841 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
   2.842 -by (res_inst_tac [("x", "K")] bexI 1);
   2.843 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset])));
   2.844 -by Auto_tac;
   2.845 -qed "multirel1_mono2";
   2.846 -
   2.847 -Goal
   2.848 - "[| A<=B; r<=s |] ==> multirel1(A, r) <= multirel1(B, s)";
   2.849 -by (rtac subset_trans 1);
   2.850 -by (rtac multirel1_mono1 1);
   2.851 -by (rtac multirel1_mono2 2);
   2.852 -by Auto_tac;
   2.853 -qed "multirel1_mono";
   2.854 -
   2.855 -(* Towards the proof of well-foundedness of multirel1 *)
   2.856 -
   2.857 -Goalw [multirel1_def]  "<M,0>~:multirel1(A, r)";
   2.858 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   2.859 -qed "not_less_0";
   2.860 -AddIffs [not_less_0];
   2.861 -
   2.862 -Goal "[| <N, M0 +# {#a#}>:multirel1(A, r); M0:Mult(A) |] ==> \
   2.863 -\ (EX M. <M, M0>:multirel1(A, r) & N = M +# {#a#}) | \
   2.864 -\ (EX K. K:Mult(A) & (ALL b:mset_of(K). <b, a>:r) & N = M0 +# K)";
   2.865 -by (forward_tac [multirel1_type RS subsetD] 1);
   2.866 -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1);
   2.867 -by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist]));
   2.868 -by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI));
   2.869 -by Auto_tac;
   2.870 -by (rewtac (Mult_iff_multiset RS iff_reflection));
   2.871 -by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1);
   2.872 -by (auto_tac (claset(), simpset() addsimps [munion_commute]));
   2.873 -qed "less_munion";
   2.874 -
   2.875 -Goal "[| M:Mult(A); a:A |] ==> <M, M +# {#a#}>: multirel1(A, r)";
   2.876 -by (auto_tac (claset(), simpset() addsimps [multirel1_iff]));
   2.877 -by (rewrite_goals_tac [Mult_iff_multiset RS iff_reflection]);
   2.878 -by (res_inst_tac [("x", "a")] exI 1);
   2.879 -by (Clarify_tac 1);
   2.880 -by (res_inst_tac [("x", "M")] exI 1);
   2.881 -by (Asm_simp_tac 1);
   2.882 -by (res_inst_tac [("x", "0")] exI 1);
   2.883 -by Auto_tac;
   2.884 -qed "multirel1_base";
   2.885 -
   2.886 -Goal "acc(0)=0";
   2.887 -by (auto_tac (claset()  addSIs [equalityI]
   2.888 -    addDs  [thm "acc.dom_subset" RS subsetD], simpset()));
   2.889 -qed "acc_0";
   2.890 -
   2.891 -Goal "[| ALL b:A. <b,a>:r --> \
   2.892 -\   (ALL M:acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r))); \
   2.893 -\   M0:acc(multirel1(A, r)); a:A; \
   2.894 -\   ALL M. <M,M0> : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \
   2.895 -\ ==> M0 +# {#a#} : acc(multirel1(A, r))";
   2.896 -by (subgoal_tac "M0:Mult(A)" 1);
   2.897 -by (etac (thm "acc.cases") 2);
   2.898 -by (etac fieldE 2);
   2.899 -by (REPEAT(blast_tac (claset() addDs [multirel1_type RS subsetD]) 2));
   2.900 -by (rtac (thm "accI") 1);
   2.901 -by (rename_tac "N" 1);
   2.902 -by (dtac less_munion 1);
   2.903 -by (Blast_tac 1);
   2.904 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   2.905 -by (eres_inst_tac [("P", "ALL x:mset_of(K). <x, a>:r")] rev_mp 1);
   2.906 -by (eres_inst_tac [("P", "mset_of(K)<=A")] rev_mp 1);
   2.907 -by (eres_inst_tac [("M", "K")] multiset_induct 1);
   2.908 -(* three subgoals *)
   2.909 -(* subgoal 1: the induction base case *)
   2.910 -by (Asm_simp_tac 1);
   2.911 -(* subgoal 2: the induction general case *)
   2.912 -by (asm_full_simp_tac (simpset() addsimps [Ball_def, Un_subset_iff]) 1);
   2.913 -by (Clarify_tac 1);
   2.914 -by (dres_inst_tac [("x", "aa")] spec 1);
   2.915 -by (Asm_full_simp_tac 1);
   2.916 -by (subgoal_tac "aa:A" 1);
   2.917 -by (Blast_tac 2);
   2.918 -by (dres_inst_tac [("psi", "ALL x. x:acc(?u)-->?v(x)")] asm_rl 1);
   2.919 -by (rotate_tac ~1 1);
   2.920 -by (dres_inst_tac [("x", "M0 +# M")] spec 1);
   2.921 -by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1);
   2.922 -(* subgoal 3: additional conditions *)
   2.923 -by (auto_tac (claset() addSIs [multirel1_base RS fieldI2], 
   2.924 -              simpset() addsimps [Mult_iff_multiset]));
   2.925 -qed "lemma1";
   2.926 -
   2.927 -Goal  "[| ALL b:A. <b,a>:r  \
   2.928 -\  --> (ALL M : acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r))); \
   2.929 -\       M:acc(multirel1(A, r)); a:A|] ==> M +# {#a#} : acc(multirel1(A, r))";
   2.930 -by (etac (thm "acc_induct") 1);
   2.931 -by (blast_tac (claset() addIs [lemma1]) 1);
   2.932 -qed "lemma2";
   2.933 -
   2.934 -Goal "[| wf[A](r); a:A |] \
   2.935 -\     ==> ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
   2.936 -by (eres_inst_tac [("a","a")] wf_on_induct 1);
   2.937 -by (Blast_tac 1);
   2.938 -by (blast_tac (claset() addIs [lemma2]) 1);
   2.939 -qed "lemma3";
   2.940 -
   2.941 -Goal "multiset(M) ==> mset_of(M)<=A --> \
   2.942 -\  wf[A](r) --> M:field(multirel1(A, r)) --> M:acc(multirel1(A, r))";
   2.943 -by (etac  multiset_induct 1);
   2.944 -by (ALLGOALS(Clarify_tac));
   2.945 -(* proving the base case *)
   2.946 -by (rtac (thm "accI") 1);
   2.947 -by (cut_inst_tac [("M", "b"), ("r", "r")] not_less_0 1);
   2.948 -by (Force_tac 1);
   2.949 -by (asm_full_simp_tac (simpset() addsimps [multirel1_def]) 1);
   2.950 -(* Proving the general case *)
   2.951 -by (Asm_full_simp_tac 1);
   2.952 -by (subgoal_tac "mset_of(M)<=A" 1);
   2.953 -by (Blast_tac 2);
   2.954 -by (Clarify_tac 1);
   2.955 -by (dres_inst_tac [("a", "a")] lemma3 1);
   2.956 -by (Blast_tac 1);
   2.957 -by (subgoal_tac "M:field(multirel1(A,r))" 1);
   2.958 -by (rtac (multirel1_base RS fieldI1) 2);
   2.959 -by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 2);
   2.960 -by (REPEAT(Blast_tac 1));
   2.961 -qed "lemma4";
   2.962 -
   2.963 -Goal "[| wf[A](r); M:Mult(A); A ~= 0|] ==> M:acc(multirel1(A, r))";
   2.964 -by (etac not_emptyE 1);
   2.965 -by  (rtac (lemma4 RS mp RS mp RS mp) 1);
   2.966 -by (rtac (multirel1_base RS fieldI1) 4);
   2.967 -by  (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
   2.968 -qed "all_accessible";
   2.969 -
   2.970 -Goal "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))";
   2.971 -by (case_tac "A=0" 1);
   2.972 -by (Asm_simp_tac 1);
   2.973 -by (rtac wf_imp_wf_on 1);
   2.974 -by (rtac wf_on_field_imp_wf 1);
   2.975 -by (asm_simp_tac (simpset() addsimps [wf_on_0]) 1);
   2.976 -by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1);
   2.977 -by (rtac (thm "wf_on_acc") 1);
   2.978 -by (Clarify_tac 1);
   2.979 -by (full_simp_tac (simpset() addsimps []) 1);
   2.980 -by (blast_tac (claset() addIs [all_accessible]) 1);
   2.981 -qed "wf_on_multirel1";
   2.982 -
   2.983 -Goal "wf(r) ==>wf(multirel1(field(r), r))";
   2.984 -by (full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
   2.985 -by (dtac wf_on_multirel1 1);
   2.986 -by (res_inst_tac [("A", "field(r) -||> nat - {0}")] wf_on_subset_A 1);
   2.987 -by (Asm_simp_tac 1);
   2.988 -by (rtac field_rel_subset 1);
   2.989 -by (rtac multirel1_type 1);
   2.990 -qed "wf_multirel1";
   2.991 -
   2.992 -(** multirel **)
   2.993 -
   2.994 -Goalw [multirel_def]
   2.995 - "multirel(A, r) <= Mult(A)*Mult(A)";
   2.996 -by (rtac (trancl_type RS subset_trans) 1);
   2.997 -by (Clarify_tac 1);
   2.998 -by (auto_tac (claset() addDs [multirel1_type RS subsetD], 
   2.999 -              simpset() addsimps []));
  2.1000 -qed "multirel_type";
  2.1001 -
  2.1002 -(* Monotonicity of multirel *)
  2.1003 -Goalw [multirel_def]
  2.1004 - "[| A<=B; r<=s |] ==> multirel(A, r)<=multirel(B,s)";
  2.1005 -by (rtac trancl_mono 1);
  2.1006 -by (rtac multirel1_mono 1);
  2.1007 -by Auto_tac;
  2.1008 -qed "multirel_mono";
  2.1009 -
  2.1010 -(* Equivalence of multirel with the usual (closure-free) def *)
  2.1011 -
  2.1012 -Goal "k:nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)";
  2.1013 -by (etac nat_induct 1 THEN Auto_tac);
  2.1014 -qed "lemma";
  2.1015 -
  2.1016 -Goal "[|a:mset_of(J); multiset(I); multiset(J) |] \
  2.1017 -\  ==> I +# J -# {#a#} = I +# (J-# {#a#})";
  2.1018 -by (asm_simp_tac (simpset() addsimps [multiset_equality]) 1);
  2.1019 -by (case_tac "a ~: mset_of(I)" 1);
  2.1020 -by (auto_tac (claset(), simpset() addsimps 
  2.1021 -             [mcount_def, mset_of_def, multiset_def, multiset_fun_iff]));
  2.1022 -by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma]));
  2.1023 -qed "mdiff_union_single_conv";
  2.1024 -
  2.1025 -Goal "[| n le m;  m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
  2.1026 -by (auto_tac (claset(), simpset() addsimps [le_iff, less_iff_succ_add]));
  2.1027 -qed "diff_add_commute";
  2.1028 -
  2.1029 -(* One direction *)
  2.1030 -
  2.1031 -Goalw [multirel_def, Ball_def, Bex_def]
  2.1032 -"<M,N>:multirel(A, r) ==> \
  2.1033 -\    trans[A](r) --> \
  2.1034 -\    (EX I J K. \
  2.1035 -\        I:Mult(A) & J:Mult(A) &  K:Mult(A) & \
  2.1036 -\        N = I +# J & M = I +# K & J ~= 0 & \
  2.1037 -\       (ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r))";
  2.1038 -by (etac converse_trancl_induct 1);
  2.1039 -by (ALLGOALS(asm_full_simp_tac (simpset() 
  2.1040 -        addsimps [multirel1_iff, Mult_iff_multiset])));
  2.1041 -by (ALLGOALS(Clarify_tac));
  2.1042 -(* Two subgoals remain *)
  2.1043 -(* Subgoal 1 *)
  2.1044 -by (res_inst_tac [("x","M0")] exI 1);
  2.1045 -by (Force_tac 1);
  2.1046 -(* Subgoal 2 *)
  2.1047 -by (case_tac "a:mset_of(Ka)" 1);
  2.1048 -by (res_inst_tac [("x","I")] exI 1 THEN Asm_simp_tac 1);
  2.1049 -by (res_inst_tac [("x", "J")] exI 1  THEN Asm_simp_tac 1);
  2.1050 -by (res_inst_tac [("x","(Ka -# {#a#}) +# K")] exI 1 THEN Asm_simp_tac 1);
  2.1051 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [Un_subset_iff])));
  2.1052 -by (asm_simp_tac (simpset() addsimps [munion_assoc RS sym]) 1);
  2.1053 -by (dres_inst_tac[("t","%M. M-#{#a#}")] subst_context 1);
  2.1054 -by (asm_full_simp_tac (simpset() 
  2.1055 -    addsimps [mdiff_union_single_conv, melem_diff_single]) 1);
  2.1056 -by (Clarify_tac 1);
  2.1057 -by (etac disjE 1);
  2.1058 -by (Asm_full_simp_tac 1);
  2.1059 -by (etac disjE 1);
  2.1060 -by (Asm_full_simp_tac 1);
  2.1061 -by (dres_inst_tac [("psi", "ALL x. x:#Ka -->?u(x)")] asm_rl 1);
  2.1062 -by (rotate_tac ~1 1);
  2.1063 -by (dres_inst_tac [("x", "a")] spec 1);
  2.1064 -by (Clarify_tac 1);
  2.1065 -by (res_inst_tac [("x", "xa")] exI 1);
  2.1066 -by (Asm_simp_tac 1);
  2.1067 -by (dres_inst_tac [("a", "x"), ("b", "a"), ("c", "xa")] trans_onD 1);
  2.1068 -by (ALLGOALS(Asm_simp_tac));
  2.1069 -by (Blast_tac 1);
  2.1070 -by (Blast_tac 1);
  2.1071 -(* new we know that  a~:mset_of(Ka) *)
  2.1072 -by (subgoal_tac "a :# I" 1);
  2.1073 -by (res_inst_tac [("x","I-#{#a#}")] exI 1 THEN Asm_simp_tac 1);
  2.1074 -by (res_inst_tac [("x","J+#{#a#}")] exI 1);
  2.1075 -by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
  2.1076 -by (res_inst_tac [("x","Ka +# K")] exI 1);
  2.1077 -by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
  2.1078 -by (rtac conjI 1);
  2.1079 -by (asm_simp_tac (simpset() addsimps
  2.1080 -        [multiset_equality, mcount_elem RS succ_pred_eq_self]) 1);
  2.1081 -by (rtac conjI 1);
  2.1082 -by (dres_inst_tac[("t","%M. M-#{#a#}")] subst_context 1);
  2.1083 -by (asm_full_simp_tac (simpset() addsimps [mdiff_union_inverse2]) 1);
  2.1084 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [multiset_equality])));
  2.1085 -by (rtac (diff_add_commute RS sym) 1);
  2.1086 -by (auto_tac (claset() addIs [mcount_elem], simpset()));
  2.1087 -by (subgoal_tac "a:mset_of(I +# Ka)" 1);
  2.1088 -by (dtac sym 2 THEN Auto_tac);
  2.1089 -qed "multirel_implies_one_step";
  2.1090 -
  2.1091 -Goal "[| a:mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M";
  2.1092 -by (asm_simp_tac (simpset() 
  2.1093 -    addsimps [multiset_equality, mcount_elem RS succ_pred_eq_self]) 1);
  2.1094 -qed "melem_imp_eq_diff_union";
  2.1095 -Addsimps [melem_imp_eq_diff_union];
  2.1096 -    
  2.1097 -Goal "[| msize(M)=$# succ(n); M:Mult(A); n:nat |] \
  2.1098 -\     ==> EX a N. M = N +# {#a#} & N:Mult(A) & a:A";
  2.1099 -by (dtac msize_eq_succ_imp_elem 1);
  2.1100 -by Auto_tac;
  2.1101 -by (res_inst_tac [("x", "a")] exI 1);
  2.1102 -by (res_inst_tac [("x", "M -# {#a#}")] exI 1);
  2.1103 -by (ftac Mult_into_multiset 1);
  2.1104 -by (Asm_simp_tac 1);
  2.1105 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  2.1106 -qed "msize_eq_succ_imp_eq_union";
  2.1107 -
  2.1108 -(* The second direction *)
  2.1109 -
  2.1110 -Goalw [Mult_iff_multiset RS iff_reflection] 
  2.1111 -"n:nat ==> \
  2.1112 -\  (ALL I J K.  \
  2.1113 -\   I:Mult(A) & J:Mult(A) & K:Mult(A) & \
  2.1114 -\  (msize(J) = $# n & J ~=0 &  (ALL k:mset_of(K).  EX j:mset_of(J). <k, j>:r)) \
  2.1115 -\   --> <I +# K, I +# J>:multirel(A, r))";
  2.1116 -by (etac nat_induct 1);
  2.1117 -by (Clarify_tac 1);
  2.1118 -by (dres_inst_tac [("M", "J")] msize_eq_0_iff 1);
  2.1119 -by Auto_tac;
  2.1120 -(* one subgoal remains *)
  2.1121 -by (subgoal_tac "msize(J)=$# succ(x)" 1);
  2.1122 -by (Asm_simp_tac 2);
  2.1123 -by (forw_inst_tac [("A", "A")]  msize_eq_succ_imp_eq_union 1);
  2.1124 -by (rewtac (Mult_iff_multiset RS iff_reflection));
  2.1125 -by (Clarify_tac 3 THEN rotate_tac ~1 3);
  2.1126 -by (ALLGOALS(Asm_full_simp_tac));
  2.1127 -by (rename_tac  "J'" 1);
  2.1128 -by (Asm_full_simp_tac 1); 
  2.1129 -by (case_tac "J' = 0" 1);
  2.1130 -by (asm_full_simp_tac (simpset() addsimps [multirel_def]) 1); 
  2.1131 -by (rtac r_into_trancl 1);
  2.1132 -by (Clarify_tac 1);
  2.1133 -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1);
  2.1134 -by (Force_tac 1);
  2.1135 -(*Now we know J' ~=  0*)
  2.1136 -by (dtac sym 1 THEN rotate_tac ~1 1);
  2.1137 -by (Asm_full_simp_tac 1);
  2.1138 -by (thin_tac "$# x = msize(J')" 1);
  2.1139 -by (forw_inst_tac [("M","K"),("P", "%x. <x,a>:r")] multiset_partition 1);
  2.1140 -by (eres_inst_tac [("P", "ALL k:mset_of(K). ?P(k)")] rev_mp 1);
  2.1141 -by (etac ssubst 1); 
  2.1142 -by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); 
  2.1143 -by Auto_tac;
  2.1144 -by (subgoal_tac "<(I +# {# x : K. <x, a> : r#}) +# {# x:K. <x, a> ~: r#}, \
  2.1145 -               \  (I +# {# x : K. <x, a> : r#}) +# J'>:multirel(A, r)" 1);
  2.1146 -by (dres_inst_tac [("x", "I +# {# x : K. <x, a>: r#}")] spec 2);
  2.1147 -by (rotate_tac ~1 2);
  2.1148 -by (dres_inst_tac [("x", "J'")] spec 2);
  2.1149 -by (rotate_tac ~1 2);
  2.1150 -by (dres_inst_tac [("x", "{# x : K. <x, a>~:r#}")] spec 2);
  2.1151 -by (Clarify_tac 2);
  2.1152 -by (Asm_full_simp_tac 2);
  2.1153 -by (Blast_tac 2);
  2.1154 -by (asm_full_simp_tac (simpset() addsimps [munion_assoc RS sym, multirel_def]) 1);
  2.1155 -by (res_inst_tac [("b", "I +# {# x:K. <x, a>:r#} +# J'")] trancl_trans 1); 
  2.1156 -by (Blast_tac 1);
  2.1157 -by (rtac r_into_trancl 1); 
  2.1158 -by (asm_full_simp_tac (simpset() addsimps [multirel1_iff, Mult_iff_multiset]) 1); 
  2.1159 -by (res_inst_tac [("x", "a")] exI 1); 
  2.1160 -by (Asm_simp_tac 1);
  2.1161 -by (res_inst_tac [("x", "I +# J'")] exI 1); 
  2.1162 -by (asm_simp_tac (simpset() addsimps munion_ac@[Un_subset_iff]) 1); 
  2.1163 -by (rtac conjI 1);
  2.1164 -by (Clarify_tac 1);
  2.1165 -by (Asm_full_simp_tac 1);
  2.1166 -by (REPEAT(Blast_tac 1));
  2.1167 -qed_spec_mp "one_step_implies_multirel_lemma";
  2.1168 -
  2.1169 -Goal  "[| J ~= 0;  ALL k:mset_of(K). EX j:mset_of(J). <k,j>:r;\
  2.1170 -\         I:Mult(A); J:Mult(A); K:Mult(A) |] \
  2.1171 -\         ==> <I+#K, I+#J> : multirel(A, r)";
  2.1172 -by (subgoal_tac "multiset(J)" 1);
  2.1173 -by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
  2.1174 -by (forw_inst_tac [("M", "J")] msize_int_of_nat 1);
  2.1175 -by (auto_tac (claset() addIs [one_step_implies_multirel_lemma], simpset()));
  2.1176 -qed "one_step_implies_multirel";
  2.1177 -
  2.1178 -(** Proving that multisets are partially ordered **)
  2.1179 -
  2.1180 -(*irreflexivity*)
  2.1181 -
  2.1182 -Goal "Finite(A) ==> \
  2.1183 -\ part_ord(A, r) --> (ALL x:A. EX y:A. <x,y>:r) -->A=0";
  2.1184 -by (etac Finite_induct 1);
  2.1185 -by (auto_tac (claset() addDs 
  2.1186 -           [subset_consI RSN (2, part_ord_subset)], simpset()));
  2.1187 -by (auto_tac (claset(), simpset() addsimps [part_ord_def, irrefl_def]));
  2.1188 -by (dres_inst_tac [("x", "xa")] bspec 1);
  2.1189 -by (dres_inst_tac [("a", "xa"), ("b", "x")] trans_onD 2);
  2.1190 -by Auto_tac;
  2.1191 -qed "multirel_irrefl_lemma";
  2.1192 -
  2.1193 -Goalw [irrefl_def] 
  2.1194 -"part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))";
  2.1195 -by (subgoal_tac "trans[A](r)" 1);
  2.1196 -by (asm_full_simp_tac (simpset() addsimps [part_ord_def]) 2);
  2.1197 -by (Clarify_tac 1);
  2.1198 -by (asm_full_simp_tac (simpset() addsimps []) 1);
  2.1199 -by (dtac multirel_implies_one_step 1);
  2.1200 -by (Clarify_tac 1);
  2.1201 -by (rewrite_goal_tac [Mult_iff_multiset RS iff_reflection] 1);
  2.1202 -by (Asm_full_simp_tac 1);
  2.1203 -by (Clarify_tac 1);
  2.1204 -by (subgoal_tac "Finite(mset_of(K))" 1);
  2.1205 -by (forw_inst_tac [("r", "r")] multirel_irrefl_lemma 1);
  2.1206 -by (forw_inst_tac [("B", "mset_of(K)")] part_ord_subset 1);
  2.1207 -by (ALLGOALS(Asm_full_simp_tac));
  2.1208 -by (auto_tac (claset(), simpset() addsimps [multiset_def, mset_of_def]));
  2.1209 -qed "irrefl_on_multirel";
  2.1210 -
  2.1211 -Goalw [multirel_def, trans_on_def] "trans[Mult(A)](multirel(A, r))";
  2.1212 -by (blast_tac (claset() addIs [trancl_trans]) 1);
  2.1213 -qed "trans_on_multirel";
  2.1214 -
  2.1215 -Goalw [multirel_def]
  2.1216 - "[| <M, N>:multirel(A, r); <N, K>:multirel(A, r) |] ==>  <M, K>:multirel(A,r)";
  2.1217 -by (blast_tac (claset() addIs [trancl_trans]) 1);
  2.1218 -qed "multirel_trans";
  2.1219 -
  2.1220 -Goalw [multirel_def]  "trans(multirel(A,r))";
  2.1221 -by (rtac trans_trancl 1);
  2.1222 -qed "trans_multirel";
  2.1223 -
  2.1224 -Goal "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))";
  2.1225 -by (simp_tac (simpset() addsimps [part_ord_def]) 1);
  2.1226 -by (blast_tac (claset() addIs [irrefl_on_multirel, trans_on_multirel]) 1);
  2.1227 -qed "part_ord_multirel";
  2.1228 -
  2.1229 -(** Monotonicity of multiset union **)
  2.1230 -
  2.1231 -Goal
  2.1232 -"[|<M,N>:multirel1(A, r); K:Mult(A) |] ==> <K +# M, K +# N>:multirel1(A, r)";
  2.1233 -by (ftac (multirel1_type RS subsetD) 1);
  2.1234 -by (auto_tac (claset(), simpset() addsimps [multirel1_iff, Mult_iff_multiset]));
  2.1235 -by (res_inst_tac [("x", "a")] exI 1); 
  2.1236 -by (Asm_simp_tac 1);
  2.1237 -by (res_inst_tac [("x", "K+#M0")] exI 1); 
  2.1238 -by (asm_simp_tac (simpset() addsimps [Un_subset_iff]) 1);
  2.1239 -by (res_inst_tac [("x", "Ka")] exI 1); 
  2.1240 -by (asm_simp_tac (simpset() addsimps [munion_assoc]) 1); 
  2.1241 -qed "munion_multirel1_mono";
  2.1242 -
  2.1243 -Goal
  2.1244 - "[| <M, N>:multirel(A, r); K:Mult(A) |]==><K +# M, K +# N>:multirel(A, r)";
  2.1245 -by (ftac (multirel_type RS subsetD) 1);
  2.1246 -by (full_simp_tac (simpset() addsimps [multirel_def]) 1);
  2.1247 -by (Clarify_tac 1);
  2.1248 -by (dres_inst_tac [("psi", "<M,N>:multirel1(A, r)^+")] asm_rl 1);
  2.1249 -by (etac rev_mp 1);
  2.1250 -by (etac rev_mp 1);
  2.1251 -by (etac rev_mp 1);
  2.1252 -by (etac trancl_induct 1); 
  2.1253 -by (Clarify_tac 1);
  2.1254 -by (blast_tac (claset() addIs [munion_multirel1_mono, r_into_trancl]) 1);
  2.1255 -by (Clarify_tac 1);
  2.1256 -by (subgoal_tac "y:Mult(A)" 1);
  2.1257 -by (blast_tac (claset() addDs [rewrite_rule [multirel_def] multirel_type RS subsetD]) 2);
  2.1258 -by (subgoal_tac "<K +# y, K +# z>:multirel1(A, r)" 1);
  2.1259 -by (blast_tac (claset() addIs [munion_multirel1_mono]) 2);
  2.1260 -by (blast_tac (claset() addIs [r_into_trancl, trancl_trans]) 1);
  2.1261 -qed "munion_multirel_mono2";
  2.1262 -
  2.1263 -Goal 
  2.1264 -"[|<M, N>:multirel(A, r); K:Mult(A)|] ==> <M +# K, N +# K>:multirel(A, r)";
  2.1265 -by (ftac (multirel_type RS subsetD) 1);
  2.1266 -by (res_inst_tac [("P", "%x. <x,?u>:multirel(A, r)")] (munion_commute RS subst) 1);
  2.1267 -by (stac (munion_commute RS sym) 1);
  2.1268 -by (rtac munion_multirel_mono2 1);
  2.1269 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  2.1270 -qed "munion_multirel_mono1";
  2.1271 -
  2.1272 -Goal 
  2.1273 -"[|<M,K>:multirel(A, r); <N,L>:multirel(A, r)|]==><M +# N, K +# L>:multirel(A, r)";
  2.1274 -by (subgoal_tac "M:Mult(A)& N:Mult(A) & K:Mult(A)& L:Mult(A)" 1);
  2.1275 -by (blast_tac (claset() addDs [multirel_type RS subsetD]) 2);
  2.1276 -by (blast_tac (claset() 
  2.1277 -    addIs [munion_multirel_mono1, multirel_trans, munion_multirel_mono2]) 1);
  2.1278 -qed "munion_multirel_mono";
  2.1279 -
  2.1280 -(** Ordinal multisets **)
  2.1281 -
  2.1282 -(* A <= B ==>  field(Memrel(A)) \\<subseteq> field(Memrel(B)) *)
  2.1283 -bind_thm("field_Memrel_mono", Memrel_mono RS field_mono);
  2.1284 -
  2.1285 -(* 
  2.1286 -[| Aa <= Ba; A <= B |] ==>
  2.1287 -multirel(field(Memrel(Aa)), Memrel(A))<= multirel(field(Memrel(Ba)), Memrel(B)) 
  2.1288 -*) 
  2.1289 -bind_thm ("multirel_Memrel_mono",
  2.1290 -         [field_Memrel_mono, Memrel_mono]MRS multirel_mono);
  2.1291 -
  2.1292 -Goalw [omultiset_def] "omultiset(M) ==> multiset(M)";
  2.1293 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  2.1294 -qed "omultiset_is_multiset";
  2.1295 -Addsimps [omultiset_is_multiset];
  2.1296 -
  2.1297 -Goalw [omultiset_def] "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)";
  2.1298 -by (Clarify_tac 1);
  2.1299 -by (res_inst_tac [("x", "i Un ia")] exI 1);
  2.1300 -by (asm_full_simp_tac (simpset() addsimps
  2.1301 -            [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
  2.1302 -by (blast_tac (claset() addIs [field_Memrel_mono]) 1);
  2.1303 -qed "munion_omultiset";
  2.1304 -Addsimps [munion_omultiset];
  2.1305 -
  2.1306 -Goalw [omultiset_def] "omultiset(M) ==> omultiset(M -# N)";
  2.1307 -by (Clarify_tac 1); 
  2.1308 -by (asm_full_simp_tac (simpset() addsimps [Mult_iff_multiset]) 1);
  2.1309 -by (res_inst_tac [("x", "i")] exI 1);
  2.1310 -by (Asm_simp_tac 1);
  2.1311 -qed "mdiff_omultiset";
  2.1312 -Addsimps [mdiff_omultiset];
  2.1313 -
  2.1314 -(** Proving that Memrel is a partial order **)
  2.1315 -
  2.1316 -Goal "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))";
  2.1317 -by (rtac irreflI 1);
  2.1318 -by (Clarify_tac 1);
  2.1319 -by (subgoal_tac "Ord(x)" 1);
  2.1320 -by (blast_tac (claset() addIs [Ord_in_Ord]) 2);
  2.1321 -by (dres_inst_tac [("i", "x")] (ltI RS lt_irrefl) 1);
  2.1322 -by Auto_tac;
  2.1323 -qed "irrefl_Memrel";
  2.1324 -
  2.1325 -Goalw [trans_on_def, trans_def]
  2.1326 - "trans(r) <-> trans[field(r)](r)";
  2.1327 -by Auto_tac;
  2.1328 -qed "trans_iff_trans_on";
  2.1329 -
  2.1330 -Goalw [part_ord_def]
  2.1331 - "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))";
  2.1332 -by (simp_tac (simpset() addsimps [trans_iff_trans_on RS iff_sym]) 1);
  2.1333 -by (blast_tac (claset() addIs [trans_Memrel, irrefl_Memrel]) 1);
  2.1334 -qed "part_ord_Memrel";
  2.1335 -
  2.1336 -(*
  2.1337 -  Ord(i) ==> 
  2.1338 -  part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i))) 
  2.1339 -*)
  2.1340 -
  2.1341 -bind_thm("part_ord_mless", part_ord_Memrel RS part_ord_multirel);
  2.1342 -
  2.1343 -(*irreflexivity*)
  2.1344 -
  2.1345 -Goalw [mless_def] "~(M <# M)";
  2.1346 -by (Clarify_tac 1);
  2.1347 -by (forward_tac [multirel_type RS subsetD] 1);
  2.1348 -by (dtac part_ord_mless 1);
  2.1349 -by (rewrite_goals_tac [part_ord_def, irrefl_def]);
  2.1350 -by (Blast_tac 1);
  2.1351 -qed "mless_not_refl";
  2.1352 -
  2.1353 -(* N<N ==> R *)
  2.1354 -bind_thm ("mless_irrefl", mless_not_refl RS notE);
  2.1355 -AddSEs [mless_irrefl];
  2.1356 -
  2.1357 -(*transitivity*)
  2.1358 -Goalw [mless_def] "[| K <# M; M <# N |] ==> K <# N";
  2.1359 -by (Clarify_tac 1);
  2.1360 -by (res_inst_tac [("x", "i Un ia")] exI 1);
  2.1361 -by (blast_tac (claset() addDs 
  2.1362 -            [[Un_upper1, Un_upper1] MRS multirel_Memrel_mono RS subsetD,
  2.1363 -            [Un_upper2, Un_upper2] MRS multirel_Memrel_mono RS subsetD]
  2.1364 -            addIs [multirel_trans, Ord_Un]) 1);
  2.1365 -qed "mless_trans";
  2.1366 -
  2.1367 -(*asymmetry*)
  2.1368 -Goal "M <# N ==> ~ N <# M";
  2.1369 -by (Clarify_tac 1);
  2.1370 -by (rtac (mless_not_refl RS notE) 1);
  2.1371 -by (etac mless_trans 1);
  2.1372 -by (assume_tac 1);
  2.1373 -qed "mless_not_sym";
  2.1374 -
  2.1375 -val major::prems =
  2.1376 -Goal "[| M <# N; ~P ==> N <# M |] ==> P";
  2.1377 -by (cut_facts_tac [major] 1);
  2.1378 -by (dtac  mless_not_sym 1);
  2.1379 -by (dres_inst_tac [("P", "P")] swap 1);
  2.1380 -by (auto_tac (claset() addIs prems, simpset()));
  2.1381 -qed "mless_asym";
  2.1382 -
  2.1383 -Goalw [mle_def] "omultiset(M) ==> M <#= M";
  2.1384 -by Auto_tac;
  2.1385 -qed "mle_refl";
  2.1386 -Addsimps [mle_refl];
  2.1387 -
  2.1388 -(*anti-symmetry*)
  2.1389 -Goalw [mle_def] 
  2.1390 -"[| M <#= N;  N <#= M |] ==> M = N";
  2.1391 -by (blast_tac (claset() addDs [mless_not_sym]) 1);
  2.1392 -qed "mle_antisym";
  2.1393 -
  2.1394 -(*transitivity*)
  2.1395 -Goalw [mle_def]
  2.1396 -     "[| K <#= M; M <#= N |] ==> K <#= N";
  2.1397 -by (blast_tac (claset() addIs [mless_trans]) 1);
  2.1398 -qed "mle_trans";
  2.1399 -
  2.1400 -Goalw [mle_def] "M <# N <-> (M <#= N & M ~= N)";
  2.1401 -by Auto_tac;
  2.1402 -qed "mless_le_iff";
  2.1403 -
  2.1404 -(** Monotonicity of mless **)
  2.1405 -
  2.1406 -Goalw [mless_def, omultiset_def]
  2.1407 - "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N";
  2.1408 -by (Clarify_tac 1);
  2.1409 -by (res_inst_tac [("x", "i Un ia")] exI 1);
  2.1410 -by (asm_full_simp_tac (simpset() 
  2.1411 -    addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
  2.1412 -by (rtac munion_multirel_mono2 1);
  2.1413 -by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
  2.1414 -by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
  2.1415 -by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
  2.1416 -qed "munion_less_mono2";
  2.1417 -
  2.1418 -Goalw [mless_def, omultiset_def]
  2.1419 - "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K";
  2.1420 -by (Clarify_tac 1);
  2.1421 -by (res_inst_tac [("x", "i Un ia")] exI 1);
  2.1422 -by (asm_full_simp_tac (simpset() 
  2.1423 -    addsimps [Mult_iff_multiset, Ord_Un, Un_subset_iff]) 1);
  2.1424 -by (rtac munion_multirel_mono1 1);
  2.1425 -by (asm_simp_tac (simpset() addsimps [Mult_iff_multiset]) 2);
  2.1426 -by (blast_tac (claset() addIs [multirel_Memrel_mono RS subsetD]) 1);
  2.1427 -by (blast_tac (claset() addIs [field_Memrel_mono RS subsetD]) 1);
  2.1428 -qed "munion_less_mono1";
  2.1429 -
  2.1430 -Goalw [mless_def, omultiset_def]
  2.1431 - "M <# N ==> omultiset(M) & omultiset(N)";
  2.1432 -by (auto_tac (claset() addDs [multirel_type RS subsetD], simpset()));
  2.1433 -qed "mless_imp_omultiset";
  2.1434 -
  2.1435 -Goal "[| M <# K; N <# L |] ==> M +# N <# K +# L";
  2.1436 -by (forw_inst_tac [("M", "M")] mless_imp_omultiset 1);
  2.1437 -by (forw_inst_tac [("M", "N")] mless_imp_omultiset 1);
  2.1438 -by (blast_tac (claset() addIs 
  2.1439 -       [munion_less_mono1, munion_less_mono2, mless_trans]) 1); 
  2.1440 -qed "munion_less_mono";
  2.1441 -
  2.1442 -(* <#= *)
  2.1443 -
  2.1444 -Goalw [mle_def] "M <#= N ==> omultiset(M) & omultiset(N)";
  2.1445 -by (auto_tac (claset(), simpset() addsimps [mless_imp_omultiset]));
  2.1446 -qed "mle_imp_omultiset";
  2.1447 -
  2.1448 -Goal "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L";
  2.1449 -by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1);
  2.1450 -by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1);
  2.1451 -by (rewtac mle_def);
  2.1452 -by (ALLGOALS(Asm_full_simp_tac));
  2.1453 -by (REPEAT(etac disjE 1));
  2.1454 -by (etac disjE 3);
  2.1455 -by (ALLGOALS(Asm_full_simp_tac));
  2.1456 -by (ALLGOALS(rtac  disjI2));
  2.1457 -by (auto_tac (claset() addIs [munion_less_mono1, munion_less_mono2, 
  2.1458 -                              munion_less_mono], simpset()));
  2.1459 -qed "mle_mono";
  2.1460 -
  2.1461 -Goalw [omultiset_def]  "omultiset(0)";
  2.1462 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  2.1463 -qed "omultiset_0";
  2.1464 -AddIffs [omultiset_0];
  2.1465 -
  2.1466 -Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M";
  2.1467 -by (subgoal_tac "EX i. Ord(i) & M:Mult(field(Memrel(i)))" 1);
  2.1468 -by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2);
  2.1469 -by (case_tac "M=0" 1);
  2.1470 -by (ALLGOALS(Asm_full_simp_tac));
  2.1471 -by (Clarify_tac 1);
  2.1472 -by (subgoal_tac "<0 +# 0, 0 +# M>: multirel(field(Memrel(i)), Memrel(i))" 1);
  2.1473 -by (rtac one_step_implies_multirel 2);
  2.1474 -by (auto_tac (claset(), simpset() addsimps [Mult_iff_multiset]));
  2.1475 -qed "empty_leI";
  2.1476 -Addsimps [empty_leI];
  2.1477 -
  2.1478 -Goal "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N";
  2.1479 -by (subgoal_tac "M +# 0 <#= M +# N" 1);
  2.1480 -by (rtac mle_mono 2); 
  2.1481 -by Auto_tac;
  2.1482 -qed "munion_upper1";
  2.1483 -
  2.1484 -
  2.1485 -
  2.1486 -
     3.1 --- a/src/ZF/Induct/Multiset.thy	Mon Sep 13 09:57:25 2004 +0200
     3.2 +++ b/src/ZF/Induct/Multiset.thy	Fri Sep 17 16:08:52 2004 +0200
     3.3 @@ -8,91 +8,1424 @@
     3.4  The theory features ordinal multisets and the usual ordering.
     3.5  *)
     3.6  
     3.7 -Multiset =  FoldSet + Acc +
     3.8 +theory Multiset
     3.9 +imports FoldSet Acc
    3.10 +begin
    3.11 +
    3.12  consts
    3.13    (* Short cut for multiset space *)
    3.14 -  Mult :: i=>i 
    3.15 -translations 
    3.16 +  Mult :: "i=>i"
    3.17 +translations
    3.18    "Mult(A)" => "A -||> nat-{0}"
    3.19 -  
    3.20 +
    3.21  constdefs
    3.22 -  
    3.23 +
    3.24    (* This is the original "restrict" from ZF.thy.
    3.25 -     Restricts the function f to the domain A 
    3.26 +     Restricts the function f to the domain A
    3.27       FIXME: adapt Multiset to the new "restrict". *)
    3.28  
    3.29    funrestrict :: "[i,i] => i"
    3.30 -  "funrestrict(f,A) == lam x:A. f`x"
    3.31 +  "funrestrict(f,A) == \<lambda>x \<in> A. f`x"
    3.32  
    3.33    (* M is a multiset *)
    3.34 -  multiset :: i => o
    3.35 -  "multiset(M) == EX A. M : A -> nat-{0} & Finite(A)"
    3.36 +  multiset :: "i => o"
    3.37 +  "multiset(M) == \<exists>A. M \<in> A -> nat-{0} & Finite(A)"
    3.38  
    3.39    mset_of :: "i=>i"
    3.40    "mset_of(M) == domain(M)"
    3.41  
    3.42    munion    :: "[i, i] => i" (infixl "+#" 65)
    3.43 -  "M +# N == lam x:mset_of(M) Un mset_of(N).
    3.44 -     if x:mset_of(M) Int mset_of(N) then  (M`x) #+ (N`x)
    3.45 -     else (if x:mset_of(M) then M`x else N`x)"
    3.46 +  "M +# N == \<lambda>x \<in> mset_of(M) Un mset_of(N).
    3.47 +     if x \<in> mset_of(M) Int mset_of(N) then  (M`x) #+ (N`x)
    3.48 +     else (if x \<in> mset_of(M) then M`x else N`x)"
    3.49  
    3.50    (*convert a function to a multiset by eliminating 0*)
    3.51 -  normalize :: i => i   
    3.52 +  normalize :: "i => i"
    3.53    "normalize(f) ==
    3.54 -       if (EX A. f : A -> nat & Finite(A)) then
    3.55 -            funrestrict(f, {x:mset_of(f). 0 < f`x})
    3.56 +       if (\<exists>A. f \<in> A -> nat & Finite(A)) then
    3.57 +            funrestrict(f, {x \<in> mset_of(f). 0 < f`x})
    3.58         else 0"
    3.59  
    3.60    mdiff  :: "[i, i] => i" (infixl "-#" 65)
    3.61 -  "M -# N ==  normalize(lam x:mset_of(M).
    3.62 -			if x:mset_of(N) then M`x #- N`x else M`x)"
    3.63 +  "M -# N ==  normalize(\<lambda>x \<in> mset_of(M).
    3.64 +			if x \<in> mset_of(N) then M`x #- N`x else M`x)"
    3.65  
    3.66    (* set of elements of a multiset *)
    3.67    msingle :: "i => i"    ("{#_#}")
    3.68    "{#a#} == {<a, 1>}"
    3.69 -  
    3.70 -  MCollect :: [i, i=>o] => i (*comprehension*)
    3.71 -  "MCollect(M, P) == funrestrict(M, {x:mset_of(M). P(x)})"
    3.72 +
    3.73 +  MCollect :: "[i, i=>o] => i"  (*comprehension*)
    3.74 +  "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})"
    3.75  
    3.76    (* Counts the number of occurences of an element in a multiset *)
    3.77 -  mcount :: [i, i] => i
    3.78 -  "mcount(M, a) == if a:mset_of(M) then  M`a else 0"
    3.79 -  
    3.80 -  msize :: i => i
    3.81 -  "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"  
    3.82 +  mcount :: "[i, i] => i"
    3.83 +  "mcount(M, a) == if a \<in> mset_of(M) then  M`a else 0"
    3.84 +
    3.85 +  msize :: "i => i"
    3.86 +  "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
    3.87  
    3.88  syntax
    3.89 -  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)  
    3.90 +  melem :: "[i,i] => o"    ("(_/ :# _)" [50, 51] 50)
    3.91    "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
    3.92  
    3.93 +syntax (xsymbols)
    3.94 +  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
    3.95 +
    3.96  translations
    3.97 -  "a :# M" == "a:mset_of(M)"
    3.98 -  "{#x:M. P#}" == "MCollect(M, %x. P)"
    3.99 +  "a :# M" == "a \<in> mset_of(M)"
   3.100 +  "{#x \<in> M. P#}" == "MCollect(M, %x. P)"
   3.101  
   3.102    (* multiset orderings *)
   3.103 -  
   3.104 +
   3.105  constdefs
   3.106     (* multirel1 has to be a set (not a predicate) so that we can form
   3.107        its transitive closure and reason about wf(.) and acc(.) *)
   3.108 -  
   3.109 +
   3.110    multirel1 :: "[i,i]=>i"
   3.111    "multirel1(A, r) ==
   3.112 -     {<M, N> : Mult(A)*Mult(A).
   3.113 -      EX a:A. EX M0:Mult(A). EX K:Mult(A).
   3.114 -      N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). <b,a>:r)}"
   3.115 -  
   3.116 +     {<M, N> \<in> Mult(A)*Mult(A).
   3.117 +      \<exists>a \<in> A. \<exists>M0 \<in> Mult(A). \<exists>K \<in> Mult(A).
   3.118 +      N=M0 +# {#a#} & M=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r)}"
   3.119 +
   3.120    multirel :: "[i, i] => i"
   3.121 -  "multirel(A, r) == multirel1(A, r)^+" 		    
   3.122 +  "multirel(A, r) == multirel1(A, r)^+" 		
   3.123  
   3.124    (* ordinal multiset orderings *)
   3.125 -  
   3.126 -  omultiset :: i => o
   3.127 -  "omultiset(M) == EX i. Ord(i) & M:Mult(field(Memrel(i)))"
   3.128 -  
   3.129 -  mless :: [i, i] => o (infixl "<#" 50)
   3.130 -  "M <# N ==  EX i. Ord(i) & <M, N>:multirel(field(Memrel(i)), Memrel(i))"
   3.131 +
   3.132 +  omultiset :: "i => o"
   3.133 +  "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))"
   3.134 +
   3.135 +  mless :: "[i, i] => o" (infixl "<#" 50)
   3.136 +  "M <# N ==  \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))"
   3.137 +
   3.138 +  mle  :: "[i, i] => o"  (infixl "<#=" 50)
   3.139 +  "M <#= N == (omultiset(M) & M = N) | M <# N"
   3.140 +
   3.141 +
   3.142 +subsection{*Properties of the original "restrict" from ZF.thy*}
   3.143 +
   3.144 +lemma funrestrict_subset: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<subseteq> f"
   3.145 +by (auto simp add: funrestrict_def lam_def intro: apply_Pair)
   3.146 +
   3.147 +lemma funrestrict_type:
   3.148 +    "[| !!x. x \<in> A ==> f`x \<in> B(x) |] ==> funrestrict(f,A) \<in> Pi(A,B)"
   3.149 +by (simp add: funrestrict_def lam_type)
   3.150 +
   3.151 +lemma funrestrict_type2: "[| f \<in> Pi(C,B);  A\<subseteq>C |] ==> funrestrict(f,A) \<in> Pi(A,B)"
   3.152 +by (blast intro: apply_type funrestrict_type)
   3.153 +
   3.154 +lemma funrestrict [simp]: "a \<in> A ==> funrestrict(f,A) ` a = f`a"
   3.155 +by (simp add: funrestrict_def)
   3.156 +
   3.157 +lemma funrestrict_empty [simp]: "funrestrict(f,0) = 0"
   3.158 +by (simp add: funrestrict_def)
   3.159 +
   3.160 +lemma domain_funrestrict [simp]: "domain(funrestrict(f,C)) = C"
   3.161 +by (auto simp add: funrestrict_def lam_def)
   3.162 +
   3.163 +lemma fun_cons_funrestrict_eq:
   3.164 +     "f \<in> cons(a, b) -> B ==> f = cons(<a, f ` a>, funrestrict(f, b))"
   3.165 +apply (rule equalityI)
   3.166 +prefer 2 apply (blast intro: apply_Pair funrestrict_subset [THEN subsetD])
   3.167 +apply (auto dest!: Pi_memberD simp add: funrestrict_def lam_def)
   3.168 +done
   3.169 +
   3.170 +declare domain_of_fun [simp]
   3.171 +declare domainE [rule del]
   3.172 +
   3.173 +
   3.174 +text{* A useful simplification rule *}
   3.175 +lemma multiset_fun_iff:
   3.176 +     "(f \<in> A -> nat-{0}) <-> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
   3.177 +apply safe
   3.178 +apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD])
   3.179 +apply (auto intro!: Ord_0_lt
   3.180 +            dest: apply_type Diff_subset [THEN Pi_mono, THEN subsetD]
   3.181 +            simp add: range_of_fun apply_iff)
   3.182 +done
   3.183 +
   3.184 +(** The multiset space  **)
   3.185 +lemma multiset_into_Mult: "[| multiset(M); mset_of(M)\<subseteq>A |] ==> M \<in> Mult(A)"
   3.186 +apply (simp add: multiset_def)
   3.187 +apply (auto simp add: multiset_fun_iff mset_of_def)
   3.188 +apply (rule_tac B1 = "nat-{0}" in FiniteFun_mono [THEN subsetD], simp_all)
   3.189 +apply (rule Finite_into_Fin [THEN [2] Fin_mono [THEN subsetD], THEN fun_FiniteFunI])
   3.190 +apply (simp_all (no_asm_simp) add: multiset_fun_iff)
   3.191 +done
   3.192 +
   3.193 +lemma Mult_into_multiset: "M \<in> Mult(A) ==> multiset(M) & mset_of(M)\<subseteq>A"
   3.194 +apply (simp add: multiset_def mset_of_def)
   3.195 +apply (frule FiniteFun_is_fun)
   3.196 +apply (drule FiniteFun_domain_Fin)
   3.197 +apply (frule FinD, clarify)
   3.198 +apply (rule_tac x = "domain (M) " in exI)
   3.199 +apply (blast intro: Fin_into_Finite)
   3.200 +done
   3.201 +
   3.202 +lemma Mult_iff_multiset: "M \<in> Mult(A) <-> multiset(M) & mset_of(M)\<subseteq>A"
   3.203 +by (blast dest: Mult_into_multiset intro: multiset_into_Mult)
   3.204 +
   3.205 +lemma multiset_iff_Mult_mset_of: "multiset(M) <-> M \<in> Mult(mset_of(M))"
   3.206 +by (auto simp add: Mult_iff_multiset)
   3.207 +
   3.208 +
   3.209 +text{*The @{term multiset} operator*}
   3.210 +
   3.211 +(* the empty multiset is 0 *)
   3.212 +
   3.213 +lemma multiset_0 [simp]: "multiset(0)"
   3.214 +by (auto intro: FiniteFun.intros simp add: multiset_iff_Mult_mset_of)
   3.215 +
   3.216 +
   3.217 +text{*The @{term mset_of} operator*}
   3.218 +
   3.219 +lemma multiset_set_of_Finite [simp]: "multiset(M) ==> Finite(mset_of(M))"
   3.220 +by (simp add: multiset_def mset_of_def, auto)
   3.221 +
   3.222 +lemma mset_of_0 [iff]: "mset_of(0) = 0"
   3.223 +by (simp add: mset_of_def)
   3.224 +
   3.225 +lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 <-> M=0"
   3.226 +by (auto simp add: multiset_def mset_of_def)
   3.227 +
   3.228 +lemma mset_of_single [iff]: "mset_of({#a#}) = {a}"
   3.229 +by (simp add: msingle_def mset_of_def)
   3.230 +
   3.231 +lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) Un mset_of(N)"
   3.232 +by (simp add: mset_of_def munion_def)
   3.233 +
   3.234 +lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A"
   3.235 +by (auto simp add: mdiff_def multiset_def normalize_def mset_of_def)
   3.236 +
   3.237 +(* msingle *)
   3.238 +
   3.239 +lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}"
   3.240 +by (simp add: msingle_def)
   3.241 +
   3.242 +lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) <->  (a = b)"
   3.243 +by (simp add: msingle_def)
   3.244 +
   3.245 +lemma msingle_multiset [iff,TC]: "multiset({#a#})"
   3.246 +apply (simp add: multiset_def msingle_def)
   3.247 +apply (rule_tac x = "{a}" in exI)
   3.248 +apply (auto intro: Finite_cons Finite_0 fun_extend3)
   3.249 +done
   3.250 +
   3.251 +(** normalize **)
   3.252 +
   3.253 +lemmas Collect_Finite = Collect_subset [THEN subset_Finite, standard]
   3.254 +
   3.255 +lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)"
   3.256 +apply (simp add: normalize_def funrestrict_def mset_of_def)
   3.257 +apply (case_tac "\<exists>A. f \<in> A -> nat & Finite (A) ")
   3.258 +apply clarify
   3.259 +apply (drule_tac x = "{x \<in> domain (f) . 0 < f ` x}" in spec)
   3.260 +apply auto
   3.261 +apply (auto  intro!: lam_type simp add: Collect_Finite)
   3.262 +done
   3.263 +
   3.264 +lemma normalize_multiset [simp]: "multiset(M) ==> normalize(M) = M"
   3.265 +by (auto simp add: multiset_def normalize_def mset_of_def funrestrict_def multiset_fun_iff)
   3.266 +
   3.267 +lemma multiset_normalize [simp]: "multiset(normalize(f))"
   3.268 +apply (simp add: normalize_def)
   3.269 +apply (simp add: normalize_def mset_of_def multiset_def, auto)
   3.270 +apply (rule_tac x = "{x \<in> A . 0<f`x}" in exI)
   3.271 +apply (auto intro: Collect_subset [THEN subset_Finite] funrestrict_type)
   3.272 +done
   3.273 +
   3.274 +(** Typechecking rules for union and difference of multisets **)
   3.275 +
   3.276 +(* union *)
   3.277 +
   3.278 +lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)"
   3.279 +apply (unfold multiset_def munion_def mset_of_def, auto)
   3.280 +apply (rule_tac x = "A Un Aa" in exI)
   3.281 +apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add)
   3.282 +done
   3.283 +
   3.284 +(* difference *)
   3.285 +
   3.286 +lemma mdiff_multiset [simp]: "multiset(M -# N)"
   3.287 +by (simp add: mdiff_def)
   3.288 +
   3.289 +(** Algebraic properties of multisets **)
   3.290 +
   3.291 +(* Union *)
   3.292 +
   3.293 +lemma munion_0 [simp]: "multiset(M) ==> M +# 0 = M & 0 +# M = M"
   3.294 +apply (simp add: multiset_def)
   3.295 +apply (auto simp add: munion_def mset_of_def)
   3.296 +done
   3.297 +
   3.298 +lemma munion_commute: "M +# N = N +# M"
   3.299 +by (auto intro!: lam_cong simp add: munion_def)
   3.300 +
   3.301 +lemma munion_assoc: "(M +# N) +# K = M +# (N +# K)"
   3.302 +apply (unfold munion_def mset_of_def)
   3.303 +apply (rule lam_cong, auto)
   3.304 +done
   3.305 +
   3.306 +lemma munion_lcommute: "M +# (N +# K) = N +# (M +# K)"
   3.307 +apply (unfold munion_def mset_of_def)
   3.308 +apply (rule lam_cong, auto)
   3.309 +done
   3.310 +
   3.311 +lemmas munion_ac = munion_commute munion_assoc munion_lcommute
   3.312 +
   3.313 +(* Difference *)
   3.314 +
   3.315 +lemma mdiff_self_eq_0 [simp]: "M -# M = 0"
   3.316 +by (simp add: mdiff_def normalize_def mset_of_def)
   3.317 +
   3.318 +lemma mdiff_0 [simp]: "0 -# M = 0"
   3.319 +by (simp add: mdiff_def normalize_def)
   3.320 +
   3.321 +lemma mdiff_0_right [simp]: "multiset(M) ==> M -# 0 = M"
   3.322 +by (auto simp add: multiset_def mdiff_def normalize_def multiset_fun_iff mset_of_def funrestrict_def)
   3.323 +
   3.324 +lemma mdiff_union_inverse2 [simp]: "multiset(M) ==> M +# {#a#} -# {#a#} = M"
   3.325 +apply (unfold multiset_def munion_def mdiff_def msingle_def normalize_def mset_of_def)
   3.326 +apply (auto cong add: if_cong simp add: ltD multiset_fun_iff funrestrict_def subset_Un_iff2 [THEN iffD1])
   3.327 +prefer 2 apply (force intro!: lam_type)
   3.328 +apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
   3.329 +apply (rule fun_extension, auto)
   3.330 +apply (drule_tac x = "A Un {a}" in spec)
   3.331 +apply (simp add: Finite_Un)
   3.332 +apply (force intro!: lam_type)
   3.333 +done
   3.334 +
   3.335 +(** Count of elements **)
   3.336 +
   3.337 +lemma mcount_type [simp,TC]: "multiset(M) ==> mcount(M, a) \<in> nat"
   3.338 +by (auto simp add: multiset_def mcount_def mset_of_def multiset_fun_iff)
   3.339 +
   3.340 +lemma mcount_0 [simp]: "mcount(0, a) = 0"
   3.341 +by (simp add: mcount_def)
   3.342 +
   3.343 +lemma mcount_single [simp]: "mcount({#b#}, a) = (if a=b then 1 else 0)"
   3.344 +by (simp add: mcount_def mset_of_def msingle_def)
   3.345 +
   3.346 +lemma mcount_union [simp]: "[| multiset(M); multiset(N) |]
   3.347 +                     ==>  mcount(M +# N, a) = mcount(M, a) #+ mcount (N, a)"
   3.348 +apply (auto simp add: multiset_def multiset_fun_iff mcount_def munion_def mset_of_def)
   3.349 +done
   3.350 +
   3.351 +lemma mcount_diff [simp]:
   3.352 +     "multiset(M) ==> mcount(M -# N, a) = mcount(M, a) #- mcount(N, a)"
   3.353 +apply (simp add: multiset_def)
   3.354 +apply (auto dest!: not_lt_imp_le
   3.355 +     simp add: mdiff_def multiset_fun_iff mcount_def normalize_def mset_of_def)
   3.356 +apply (force intro!: lam_type)
   3.357 +apply (force intro!: lam_type)
   3.358 +done
   3.359 +
   3.360 +lemma mcount_elem: "[| multiset(M); a \<in> mset_of(M) |] ==> 0 < mcount(M, a)"
   3.361 +apply (simp add: multiset_def, clarify)
   3.362 +apply (simp add: mcount_def mset_of_def)
   3.363 +apply (simp add: multiset_fun_iff)
   3.364 +done
   3.365 +
   3.366 +(** msize **)
   3.367 +
   3.368 +lemma msize_0 [simp]: "msize(0) = #0"
   3.369 +by (simp add: msize_def)
   3.370 +
   3.371 +lemma msize_single [simp]: "msize({#a#}) = #1"
   3.372 +by (simp add: msize_def)
   3.373 +
   3.374 +lemma msize_type [simp,TC]: "msize(M) \<in> int"
   3.375 +by (simp add: msize_def)
   3.376 +
   3.377 +lemma msize_zpositive: "multiset(M)==> #0 $\<le> msize(M)"
   3.378 +by (auto simp add: msize_def intro: g_zpos_imp_setsum_zpos)
   3.379 +
   3.380 +lemma msize_int_of_nat: "multiset(M) ==> \<exists>n \<in> nat. msize(M)= $# n"
   3.381 +apply (rule not_zneg_int_of)
   3.382 +apply (simp_all (no_asm_simp) add: msize_type [THEN znegative_iff_zless_0] not_zless_iff_zle msize_zpositive)
   3.383 +done
   3.384 +
   3.385 +lemma not_empty_multiset_imp_exist:
   3.386 +     "[| M\<noteq>0; multiset(M) |] ==> \<exists>a \<in> mset_of(M). 0 < mcount(M, a)"
   3.387 +apply (simp add: multiset_def)
   3.388 +apply (erule not_emptyE)
   3.389 +apply (auto simp add: mset_of_def mcount_def multiset_fun_iff)
   3.390 +apply (blast dest!: fun_is_rel)
   3.391 +done
   3.392 +
   3.393 +lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 <-> M=0"
   3.394 +apply (simp add: msize_def, auto)
   3.395 +apply (rule_tac Pa = "setsum (?u,?v) \<noteq> #0" in swap)
   3.396 +apply blast
   3.397 +apply (drule not_empty_multiset_imp_exist, assumption, clarify)
   3.398 +apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
   3.399 + prefer 2 apply (simp add: Finite_Diff)
   3.400 +apply (subgoal_tac "setsum (%x. $# mcount (M, x), cons (a, mset_of (M) -{a}))=#0")
   3.401 + prefer 2 apply (simp add: cons_Diff, simp)
   3.402 +apply (subgoal_tac "#0 $\<le> setsum (%x. $# mcount (M, x), mset_of (M) - {a}) ")
   3.403 +apply (rule_tac [2] g_zpos_imp_setsum_zpos)
   3.404 +apply (auto simp add: Finite_Diff not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
   3.405 +apply (rule not_zneg_int_of [THEN bexE])
   3.406 +apply (auto simp del: int_of_0 simp add: int_of_add [symmetric] int_of_0 [symmetric])
   3.407 +done
   3.408 +
   3.409 +lemma setsum_mcount_Int:
   3.410 +     "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
   3.411 +		  = setsum(%a. $# mcount(N, a), A)"
   3.412 +apply (erule Finite_induct, auto)
   3.413 +apply (subgoal_tac "Finite (B Int mset_of (N))")
   3.414 +prefer 2 apply (blast intro: subset_Finite)
   3.415 +apply (auto simp add: mcount_def Int_cons_left)
   3.416 +done
   3.417 +
   3.418 +lemma msize_union [simp]:
   3.419 +     "[| multiset(M); multiset(N) |] ==> msize(M +# N) = msize(M) $+ msize(N)"
   3.420 +apply (simp add: msize_def setsum_Un setsum_addf int_of_add setsum_mcount_Int)
   3.421 +apply (subst Int_commute)
   3.422 +apply (simp add: setsum_mcount_Int)
   3.423 +done
   3.424 +
   3.425 +lemma msize_eq_succ_imp_elem: "[|msize(M)= $# succ(n); n \<in> nat|] ==> \<exists>a. a \<in> mset_of(M)"
   3.426 +apply (unfold msize_def)
   3.427 +apply (blast dest: setsum_succD)
   3.428 +done
   3.429 +
   3.430 +(** Equality of multisets **)
   3.431 +
   3.432 +lemma equality_lemma:
   3.433 +     "[| multiset(M); multiset(N); \<forall>a. mcount(M, a)=mcount(N, a) |]
   3.434 +      ==> mset_of(M)=mset_of(N)"
   3.435 +apply (simp add: multiset_def)
   3.436 +apply (rule sym, rule equalityI)
   3.437 +apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
   3.438 +apply (drule_tac [!] x=x in spec)
   3.439 +apply (case_tac [2] "x \<in> Aa", case_tac "x \<in> A", auto)
   3.440 +done
   3.441 +
   3.442 +lemma multiset_equality:
   3.443 +  "[| multiset(M); multiset(N) |]==> M=N<->(\<forall>a. mcount(M, a)=mcount(N, a))"
   3.444 +apply auto
   3.445 +apply (subgoal_tac "mset_of (M) = mset_of (N) ")
   3.446 +prefer 2 apply (blast intro: equality_lemma)
   3.447 +apply (simp add: multiset_def mset_of_def)
   3.448 +apply (auto simp add: multiset_fun_iff)
   3.449 +apply (rule fun_extension)
   3.450 +apply (blast, blast)
   3.451 +apply (drule_tac x = x in spec)
   3.452 +apply (auto simp add: mcount_def mset_of_def)
   3.453 +done
   3.454 +
   3.455 +(** More algebraic properties of multisets **)
   3.456 +
   3.457 +lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)"
   3.458 +by (auto simp add: multiset_equality)
   3.459 +
   3.460 +lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)"
   3.461 +apply (rule iffI, drule sym)
   3.462 +apply (simp_all add: multiset_equality)
   3.463 +done
   3.464 +
   3.465 +lemma munion_right_cancel [simp]:
   3.466 +     "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)"
   3.467 +by (auto simp add: multiset_equality)
   3.468 +
   3.469 +lemma munion_left_cancel [simp]:
   3.470 +  "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)"
   3.471 +by (auto simp add: multiset_equality)
   3.472 +
   3.473 +lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)"
   3.474 +by (induct_tac "n", auto)
   3.475 +
   3.476 +lemma munion_is_single:
   3.477 +     "[|multiset(M); multiset(N)|] 
   3.478 +      ==> (M +# N = {#a#}) <->  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
   3.479 +apply (simp (no_asm_simp) add: multiset_equality)
   3.480 +apply safe
   3.481 +apply simp_all
   3.482 +apply (case_tac "aa=a")
   3.483 +apply (drule_tac [2] x = aa in spec)
   3.484 +apply (drule_tac x = a in spec)
   3.485 +apply (simp add: nat_add_eq_1_cases, simp)
   3.486 +apply (case_tac "aaa=aa", simp)
   3.487 +apply (drule_tac x = aa in spec)
   3.488 +apply (simp add: nat_add_eq_1_cases)
   3.489 +apply (case_tac "aaa=a")
   3.490 +apply (drule_tac [4] x = aa in spec)
   3.491 +apply (drule_tac [3] x = a in spec)
   3.492 +apply (drule_tac [2] x = aaa in spec)
   3.493 +apply (drule_tac x = aa in spec)
   3.494 +apply (simp_all add: nat_add_eq_1_cases)
   3.495 +done
   3.496 +
   3.497 +lemma msingle_is_union: "[| multiset(M); multiset(N) |]
   3.498 +  ==> ({#a#} = M +# N) <-> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)"
   3.499 +apply (subgoal_tac " ({#a#} = M +# N) <-> (M +# N = {#a#}) ")
   3.500 +apply (simp (no_asm_simp) add: munion_is_single)
   3.501 +apply blast
   3.502 +apply (blast dest: sym)
   3.503 +done
   3.504 +
   3.505 +(** Towards induction over multisets **)
   3.506 +
   3.507 +lemma setsum_decr:
   3.508 +"Finite(A)
   3.509 +  ==>  (\<forall>M. multiset(M) -->
   3.510 +  (\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) =
   3.511 +  (if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1
   3.512 +           else setsum(%z. $# mcount(M, z), A))))"
   3.513 +apply (unfold multiset_def)
   3.514 +apply (erule Finite_induct)
   3.515 +apply (auto simp add: multiset_fun_iff)
   3.516 +apply (unfold mset_of_def mcount_def)
   3.517 +apply (case_tac "x \<in> A", auto)
   3.518 +apply (subgoal_tac "$# M ` x $+ #-1 = $# M ` x $- $# 1")
   3.519 +apply (erule ssubst)
   3.520 +apply (rule int_of_diff, auto)
   3.521 +done
   3.522 +
   3.523 +(*FIXME: we should not have to rename x to x' below!  There's a bug in the
   3.524 +  interaction between simproc inteq_cancel_numerals and the simplifier.*)
   3.525 +lemma setsum_decr2:
   3.526 +     "Finite(A)
   3.527 +      ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
   3.528 +           setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) =
   3.529 +           (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a
   3.530 +            else setsum(%x'. $# mcount(M, x'), A)))"
   3.531 +apply (simp add: multiset_def)
   3.532 +apply (erule Finite_induct)
   3.533 +apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
   3.534 +done
   3.535 +
   3.536 +lemma setsum_decr3: "[| Finite(A); multiset(M); a \<in> mset_of(M) |]
   3.537 +      ==> setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A - {a}) =
   3.538 +          (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
   3.539 +           else setsum(%x. $# mcount(M, x), A))"
   3.540 +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) ")
   3.541 +apply (rule_tac [2] setsum_Diff [symmetric])
   3.542 +apply (rule sym, rule ssubst, blast)
   3.543 +apply (rule sym, drule setsum_decr2, auto)
   3.544 +apply (simp add: mcount_def mset_of_def)
   3.545 +done
   3.546 +
   3.547 +lemma nat_le_1_cases: "n \<in> nat ==> n le 1 <-> (n=0 | n=1)"
   3.548 +by (auto elim: natE)
   3.549 +
   3.550 +lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n"
   3.551 +apply (subgoal_tac "1 le n")
   3.552 +apply (drule add_diff_inverse2, auto)
   3.553 +done
   3.554 +
   3.555 +text{*Specialized for use in the proof below.*}
   3.556 +lemma multiset_funrestict:
   3.557 +     "\<lbrakk>\<forall>a\<in>A. M ` a \<in> nat \<and> 0 < M ` a; Finite(A)\<rbrakk>
   3.558 +      \<Longrightarrow> multiset(funrestrict(M, A - {a}))"
   3.559 +apply (simp add: multiset_def multiset_fun_iff)
   3.560 +apply (rule_tac x="A-{a}" in exI)
   3.561 +apply (auto intro: Finite_Diff funrestrict_type)
   3.562 +done
   3.563 +
   3.564 +lemma multiset_induct_aux:
   3.565 +  assumes prem1: "!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M))"
   3.566 +      and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))"
   3.567 +  shows
   3.568 +  "[| n \<in> nat; P(0) |]
   3.569 +     ==> (\<forall>M. multiset(M)-->
   3.570 +  (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) --> P(M))"
   3.571 +apply (erule nat_induct, clarify)
   3.572 +apply (frule msize_eq_0_iff)
   3.573 +apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def)
   3.574 +apply (subgoal_tac "setsum (%x. $# mcount (M, x), A) =$# succ (x) ")
   3.575 +apply (drule setsum_succD, auto)
   3.576 +apply (case_tac "1 <M`a")
   3.577 +apply (drule_tac [2] not_lt_imp_le)
   3.578 +apply (simp_all add: nat_le_1_cases)
   3.579 +apply (subgoal_tac "M= (M (a:=M`a #- 1)) (a:= (M (a:=M`a #- 1))`a #+ 1) ")
   3.580 +apply (rule_tac [2] A = A and B = "%x. nat" and D = "%x. nat" in fun_extension)
   3.581 +apply (rule_tac [3] update_type)+
   3.582 +apply (simp_all (no_asm_simp))
   3.583 + apply (rule_tac [2] impI)
   3.584 + apply (rule_tac [2] succ_pred_eq_self [symmetric])
   3.585 +apply (simp_all (no_asm_simp))
   3.586 +apply (rule subst, rule sym, blast, rule prem2)
   3.587 +apply (simp (no_asm) add: multiset_def multiset_fun_iff)
   3.588 +apply (rule_tac x = A in exI)
   3.589 +apply (force intro: update_type)
   3.590 +apply (simp (no_asm_simp) add: mset_of_def mcount_def)
   3.591 +apply (drule_tac x = "M (a := M ` a #- 1) " in spec)
   3.592 +apply (drule mp, drule_tac [2] mp, simp_all)
   3.593 +apply (rule_tac x = A in exI)
   3.594 +apply (auto intro: update_type)
   3.595 +apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a-->0<M`x}) ")
   3.596 +prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons)
   3.597 +apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a-->0<M`x}" in setsum_decr)
   3.598 +apply (drule_tac x = M in spec)
   3.599 +apply (subgoal_tac "multiset (M) ")
   3.600 + prefer 2
   3.601 + apply (simp add: multiset_def multiset_fun_iff)
   3.602 + apply (rule_tac x = A in exI, force)
   3.603 +apply (simp_all add: mset_of_def)
   3.604 +apply (drule_tac psi = "\<forall>x \<in> A. ?u (x) " in asm_rl)
   3.605 +apply (drule_tac x = a in bspec)
   3.606 +apply (simp (no_asm_simp))
   3.607 +apply (subgoal_tac "cons (a, A) = A")
   3.608 +prefer 2 apply blast
   3.609 +apply simp
   3.610 +apply (subgoal_tac "M=cons (<a, M`a>, funrestrict (M, A-{a}))")
   3.611 + prefer 2
   3.612 + apply (rule fun_cons_funrestrict_eq)
   3.613 + apply (subgoal_tac "cons (a, A-{a}) = A")
   3.614 +  apply force
   3.615 +  apply force
   3.616 +apply (rule_tac a = "cons (<a, 1>, funrestrict (M, A - {a}))" in ssubst)
   3.617 +apply simp
   3.618 +apply (frule multiset_funrestict, assumption)
   3.619 +apply (rule prem1, assumption)
   3.620 +apply (simp add: mset_of_def)
   3.621 +apply (drule_tac x = "funrestrict (M, A-{a}) " in spec)
   3.622 +apply (drule mp)
   3.623 +apply (rule_tac x = "A-{a}" in exI)
   3.624 +apply (auto intro: Finite_Diff funrestrict_type simp add: funrestrict)
   3.625 +apply (frule_tac A = A and M = M and a = a in setsum_decr3)
   3.626 +apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
   3.627 +apply blast
   3.628 +apply (simp (no_asm_simp) add: mset_of_def)
   3.629 +apply (drule_tac b = "if ?u then ?v else ?w" in sym, simp_all)
   3.630 +apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
   3.631 +apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
   3.632 +done
   3.633 +
   3.634 +lemma multiset_induct2:
   3.635 +  "[| multiset(M); P(0);
   3.636 +    (!!M a. [| multiset(M); a\<notin>mset_of(M); P(M) |] ==> P(cons(<a, 1>, M)));
   3.637 +    (!!M b. [| multiset(M); b \<in> mset_of(M);  P(M) |] ==> P(M(b:= M`b #+ 1))) |]
   3.638 +     ==> P(M)"
   3.639 +apply (subgoal_tac "\<exists>n \<in> nat. setsum (\<lambda>x. $# mcount (M, x), {x \<in> mset_of (M) . 0 < M ` x}) = $# n")
   3.640 +apply (rule_tac [2] not_zneg_int_of)
   3.641 +apply (simp_all (no_asm_simp) add: znegative_iff_zless_0 not_zless_iff_zle)
   3.642 +apply (rule_tac [2] g_zpos_imp_setsum_zpos)
   3.643 +prefer 2 apply (blast intro:  multiset_set_of_Finite Collect_subset [THEN subset_Finite])
   3.644 + prefer 2 apply (simp add: multiset_def multiset_fun_iff, clarify)
   3.645 +apply (rule multiset_induct_aux [rule_format], auto)
   3.646 +done
   3.647 +
   3.648 +lemma munion_single_case1:
   3.649 +     "[| multiset(M); a \<notin>mset_of(M) |] ==> M +# {#a#} = cons(<a, 1>, M)"
   3.650 +apply (simp add: multiset_def msingle_def)
   3.651 +apply (auto simp add: munion_def)
   3.652 +apply (unfold mset_of_def, simp)
   3.653 +apply (rule fun_extension, rule lam_type, simp_all)
   3.654 +apply (auto simp add: multiset_fun_iff fun_extend_apply)
   3.655 +apply (drule_tac c = a and b = 1 in fun_extend3)
   3.656 +apply (auto simp add: cons_eq Un_commute [of _ "{a}"])
   3.657 +done
   3.658 +
   3.659 +lemma munion_single_case2:
   3.660 +     "[| multiset(M); a \<in> mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)"
   3.661 +apply (simp add: multiset_def)
   3.662 +apply (auto simp add: munion_def multiset_fun_iff msingle_def)
   3.663 +apply (unfold mset_of_def, simp)
   3.664 +apply (subgoal_tac "A Un {a} = A")
   3.665 +apply (rule fun_extension)
   3.666 +apply (auto dest: domain_type intro: lam_type update_type)
   3.667 +done
   3.668 +
   3.669 +(* Induction principle for multisets *)
   3.670 +
   3.671 +lemma multiset_induct:
   3.672 +  assumes M: "multiset(M)"
   3.673 +      and P0: "P(0)"
   3.674 +      and step: "!!M a. [| multiset(M); P(M) |] ==> P(M +# {#a#})"
   3.675 +  shows "P(M)"
   3.676 +apply (rule multiset_induct2 [OF M])
   3.677 +apply (simp_all add: P0)
   3.678 +apply (frule_tac [2] a1 = b in munion_single_case2 [symmetric])
   3.679 +apply (frule_tac a1 = a in munion_single_case1 [symmetric])
   3.680 +apply (auto intro: step)
   3.681 +done
   3.682 +
   3.683 +(** MCollect **)
   3.684 +
   3.685 +lemma MCollect_multiset [simp]:
   3.686 +     "multiset(M) ==> multiset({# x \<in> M. P(x)#})"
   3.687 +apply (simp add: MCollect_def multiset_def mset_of_def, clarify)
   3.688 +apply (rule_tac x = "{x \<in> A. P (x) }" in exI)
   3.689 +apply (auto dest: CollectD1 [THEN [2] apply_type]
   3.690 +            intro: Collect_subset [THEN subset_Finite] funrestrict_type)
   3.691 +done
   3.692 +
   3.693 +lemma mset_of_MCollect [simp]:
   3.694 +     "multiset(M) ==> mset_of({# x \<in> M. P(x) #}) \<subseteq> mset_of(M)"
   3.695 +by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def)
   3.696 +
   3.697 +lemma MCollect_mem_iff [iff]:
   3.698 +     "x \<in> mset_of({#x \<in> M. P(x)#}) <->  x \<in> mset_of(M) & P(x)"
   3.699 +by (simp add: MCollect_def mset_of_def)
   3.700 +
   3.701 +lemma mcount_MCollect [simp]:
   3.702 +     "mcount({# x \<in> M. P(x) #}, a) = (if P(a) then mcount(M,a) else 0)"
   3.703 +by (simp add: mcount_def MCollect_def mset_of_def)
   3.704 +
   3.705 +lemma multiset_partition: "multiset(M) ==> M = {# x \<in> M. P(x) #} +# {# x \<in> M. ~ P(x) #}"
   3.706 +by (simp add: multiset_equality)
   3.707 +
   3.708 +lemma natify_elem_is_self [simp]:
   3.709 +     "[| multiset(M); a \<in> mset_of(M) |] ==> natify(M`a) = M`a"
   3.710 +by (auto simp add: multiset_def mset_of_def multiset_fun_iff)
   3.711 +
   3.712 +(* and more algebraic laws on multisets *)
   3.713 +
   3.714 +lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |]
   3.715 +  ==>  (M +# {#a#} = N +# {#b#}) <->  (M = N & a = b |
   3.716 +       M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})"
   3.717 +apply (simp del: mcount_single add: multiset_equality)
   3.718 +apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE)
   3.719 +apply (case_tac "a=b", auto)
   3.720 +apply (drule_tac x = a in spec)
   3.721 +apply (drule_tac [2] x = b in spec)
   3.722 +apply (drule_tac [3] x = aa in spec)
   3.723 +apply (drule_tac [4] x = a in spec, auto)
   3.724 +apply (subgoal_tac [!] "mcount (N,a) :nat")
   3.725 +apply (erule_tac [3] natE, erule natE, auto)
   3.726 +done
   3.727 +
   3.728 +lemma melem_diff_single:
   3.729 +"multiset(M) ==>
   3.730 +  k \<in> mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
   3.731 +apply (simp add: multiset_def)
   3.732 +apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def)
   3.733 +apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1]
   3.734 +            simp add: multiset_fun_iff apply_iff)
   3.735 +apply (force intro!: lam_type)
   3.736 +apply (force intro!: lam_type)
   3.737 +apply (force intro!: lam_type)
   3.738 +done
   3.739 +
   3.740 +lemma munion_eq_conv_exist:
   3.741 +"[| M \<in> Mult(A); N \<in> Mult(A) |]
   3.742 +  ==> (M +# {#a#} = N +# {#b#}) <->
   3.743 +      (M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))"
   3.744 +by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff)
   3.745 +
   3.746 +
   3.747 +subsection{*Multiset Orderings*}
   3.748 +
   3.749 +(* multiset on a domain A are finite functions from A to nat-{0} *)
   3.750 +
   3.751 +
   3.752 +(* multirel1 type *)
   3.753 +
   3.754 +lemma multirel1_type: "multirel1(A, r) \<subseteq> Mult(A)*Mult(A)"
   3.755 +by (auto simp add: multirel1_def)
   3.756 +
   3.757 +lemma multirel1_0 [simp]: "multirel1(0, r) =0"
   3.758 +by (auto simp add: multirel1_def)
   3.759 +
   3.760 +lemma multirel1_iff:
   3.761 +" <N, M> \<in> multirel1(A, r) <->
   3.762 +  (\<exists>a. a \<in> A &
   3.763 +  (\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) &
   3.764 +   M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))"
   3.765 +by (auto simp add: multirel1_def Mult_iff_multiset Bex_def)
   3.766 +
   3.767 +
   3.768 +text{*Monotonicity of @{term multirel1}*}
   3.769 +
   3.770 +lemma multirel1_mono1: "A\<subseteq>B ==> multirel1(A, r)\<subseteq>multirel1(B, r)"
   3.771 +apply (auto simp add: multirel1_def)
   3.772 +apply (auto simp add: Un_subset_iff Mult_iff_multiset)
   3.773 +apply (rule_tac x = a in bexI)
   3.774 +apply (rule_tac x = M0 in bexI, simp)
   3.775 +apply (rule_tac x = K in bexI)
   3.776 +apply (auto simp add: Mult_iff_multiset)
   3.777 +done
   3.778 +
   3.779 +lemma multirel1_mono2: "r\<subseteq>s ==> multirel1(A,r)\<subseteq>multirel1(A, s)"
   3.780 +apply (simp add: multirel1_def, auto) 
   3.781 +apply (rule_tac x = a in bexI)
   3.782 +apply (rule_tac x = M0 in bexI)
   3.783 +apply (simp_all add: Mult_iff_multiset)
   3.784 +apply (rule_tac x = K in bexI)
   3.785 +apply (simp_all add: Mult_iff_multiset, auto)
   3.786 +done
   3.787 +
   3.788 +lemma multirel1_mono:
   3.789 +     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel1(A, r) \<subseteq> multirel1(B, s)"
   3.790 +apply (rule subset_trans)
   3.791 +apply (rule multirel1_mono1)
   3.792 +apply (rule_tac [2] multirel1_mono2, auto)
   3.793 +done
   3.794 +
   3.795 +subsection{* Toward the proof of well-foundedness of multirel1 *}
   3.796 +
   3.797 +lemma not_less_0 [iff]: "<M,0> \<notin> multirel1(A, r)"
   3.798 +by (auto simp add: multirel1_def Mult_iff_multiset)
   3.799  
   3.800 -  mle  :: [i, i] => o  (infixl "<#=" 50)
   3.801 -  "M <#= N == (omultiset(M) & M = N) | M <# N"
   3.802 -  
   3.803 +lemma less_munion: "[| <N, M0 +# {#a#}> \<in> multirel1(A, r); M0 \<in> Mult(A) |] ==>
   3.804 +  (\<exists>M. <M, M0> \<in> multirel1(A, r) & N = M +# {#a#}) |
   3.805 +  (\<exists>K. K \<in> Mult(A) & (\<forall>b \<in> mset_of(K). <b, a> \<in> r) & N = M0 +# K)"
   3.806 +apply (frule multirel1_type [THEN subsetD])
   3.807 +apply (simp add: multirel1_iff)
   3.808 +apply (auto simp add: munion_eq_conv_exist)
   3.809 +apply (rule_tac x="Ka +# K" in exI, auto, simp add: Mult_iff_multiset)
   3.810 +apply (simp (no_asm_simp) add: munion_left_cancel munion_assoc)
   3.811 +apply (auto simp add: munion_commute)
   3.812 +done
   3.813 +
   3.814 +lemma multirel1_base: "[| M \<in> Mult(A); a \<in> A |] ==> <M, M +# {#a#}> \<in> multirel1(A, r)"
   3.815 +apply (auto simp add: multirel1_iff)
   3.816 +apply (simp add: Mult_iff_multiset)
   3.817 +apply (rule_tac x = a in exI, clarify)
   3.818 +apply (rule_tac x = M in exI, simp)
   3.819 +apply (rule_tac x = 0 in exI, auto)
   3.820 +done
   3.821 +
   3.822 +lemma acc_0: "acc(0)=0"
   3.823 +by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD])
   3.824 +
   3.825 +lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r -->
   3.826 +    (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r)));
   3.827 +    M0 \<in> acc(multirel1(A, r)); a \<in> A;
   3.828 +    \<forall>M. <M,M0> \<in> multirel1(A, r) --> M +# {#a#} \<in> acc(multirel1(A, r)) |]
   3.829 +  ==> M0 +# {#a#} \<in> acc(multirel1(A, r))"
   3.830 +apply (subgoal_tac "M0 \<in> Mult (A) ")
   3.831 + prefer 2
   3.832 + apply (erule acc.cases)
   3.833 + apply (erule fieldE)
   3.834 + apply (auto dest: multirel1_type [THEN subsetD])
   3.835 +apply (rule accI)
   3.836 +apply (rename_tac "N")
   3.837 +apply (drule less_munion, blast)
   3.838 +apply (auto simp add: Mult_iff_multiset)
   3.839 +apply (erule_tac P = "\<forall>x \<in> mset_of (K) . <x, a> \<in> r" in rev_mp)
   3.840 +apply (erule_tac P = "mset_of (K) \<subseteq>A" in rev_mp)
   3.841 +apply (erule_tac M = K in multiset_induct)
   3.842 +(* three subgoals *)
   3.843 +(* subgoal 1: the induction base case *)
   3.844 +apply (simp (no_asm_simp))
   3.845 +(* subgoal 2: the induction general case *)
   3.846 +apply (simp add: Ball_def Un_subset_iff, clarify)
   3.847 +apply (drule_tac x = aa in spec, simp)
   3.848 +apply (subgoal_tac "aa \<in> A")
   3.849 +prefer 2 apply blast
   3.850 +apply (drule_tac x = "M0 +# M" and P =
   3.851 +       "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
   3.852 +apply (simp add: munion_assoc [symmetric])
   3.853 +(* subgoal 3: additional conditions *)
   3.854 +apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
   3.855 +done
   3.856 +
   3.857 +lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
   3.858 +   --> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
   3.859 +        M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))"
   3.860 +apply (erule acc_induct)
   3.861 +apply (blast intro: lemma1)
   3.862 +done
   3.863 +
   3.864 +lemma lemma3: "[| wf[A](r); a \<in> A |]
   3.865 +      ==> \<forall>M \<in> acc(multirel1(A, r)). M +# {#a#} \<in> acc(multirel1(A, r))"
   3.866 +apply (erule_tac a = a in wf_on_induct, blast)
   3.867 +apply (blast intro: lemma2)
   3.868 +done
   3.869 +
   3.870 +lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A -->
   3.871 +   wf[A](r) --> M \<in> field(multirel1(A, r)) --> M \<in> acc(multirel1(A, r))"
   3.872 +apply (erule multiset_induct)
   3.873 +(* proving the base case *)
   3.874 +apply clarify
   3.875 +apply (rule accI, force)
   3.876 +apply (simp add: multirel1_def)
   3.877 +(* Proving the general case *)
   3.878 +apply clarify
   3.879 +apply simp
   3.880 +apply (subgoal_tac "mset_of (M) \<subseteq>A")
   3.881 +prefer 2 apply blast
   3.882 +apply clarify
   3.883 +apply (drule_tac a = a in lemma3, blast)
   3.884 +apply (subgoal_tac "M \<in> field (multirel1 (A,r))")
   3.885 +apply blast
   3.886 +apply (rule multirel1_base [THEN fieldI1])
   3.887 +apply (auto simp add: Mult_iff_multiset)
   3.888 +done
   3.889 +
   3.890 +lemma all_accessible: "[| wf[A](r); M \<in> Mult(A); A \<noteq> 0|] ==> M \<in> acc(multirel1(A, r))"
   3.891 +apply (erule not_emptyE)
   3.892 +apply  (rule lemma4 [THEN mp, THEN mp, THEN mp])
   3.893 +apply (rule_tac [4] multirel1_base [THEN fieldI1])
   3.894 +apply  (auto simp add: Mult_iff_multiset)
   3.895 +done
   3.896 +
   3.897 +lemma wf_on_multirel1: "wf[A](r) ==> wf[A-||>nat-{0}](multirel1(A, r))"
   3.898 +apply (case_tac "A=0")
   3.899 +apply (simp (no_asm_simp))
   3.900 +apply (rule wf_imp_wf_on)
   3.901 +apply (rule wf_on_field_imp_wf)
   3.902 +apply (simp (no_asm_simp) add: wf_on_0)
   3.903 +apply (rule_tac A = "acc (multirel1 (A,r))" in wf_on_subset_A)
   3.904 +apply (rule wf_on_acc)
   3.905 +apply (blast intro: all_accessible)
   3.906 +done
   3.907 +
   3.908 +lemma wf_multirel1: "wf(r) ==>wf(multirel1(field(r), r))"
   3.909 +apply (simp (no_asm_use) add: wf_iff_wf_on_field)
   3.910 +apply (drule wf_on_multirel1)
   3.911 +apply (rule_tac A = "field (r) -||> nat - {0}" in wf_on_subset_A)
   3.912 +apply (simp (no_asm_simp))
   3.913 +apply (rule field_rel_subset)
   3.914 +apply (rule multirel1_type)
   3.915 +done
   3.916 +
   3.917 +(** multirel **)
   3.918 +
   3.919 +lemma multirel_type: "multirel(A, r) \<subseteq> Mult(A)*Mult(A)"
   3.920 +apply (simp add: multirel_def)
   3.921 +apply (rule trancl_type [THEN subset_trans])
   3.922 +apply (auto dest: multirel1_type [THEN subsetD])
   3.923 +done
   3.924 +
   3.925 +(* Monotonicity of multirel *)
   3.926 +lemma multirel_mono:
   3.927 +     "[| A\<subseteq>B; r\<subseteq>s |] ==> multirel(A, r)\<subseteq>multirel(B,s)"
   3.928 +apply (simp add: multirel_def)
   3.929 +apply (rule trancl_mono)
   3.930 +apply (rule multirel1_mono, auto)
   3.931 +done
   3.932 +
   3.933 +(* Equivalence of multirel with the usual (closure-free) def *)
   3.934 +
   3.935 +lemma add_diff_eq: "k \<in> nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)"
   3.936 +by (erule nat_induct, auto)
   3.937 +
   3.938 +lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]
   3.939 +   ==> I +# J -# {#a#} = I +# (J-# {#a#})"
   3.940 +apply (simp (no_asm_simp) add: multiset_equality)
   3.941 +apply (case_tac "a \<notin> mset_of (I) ")
   3.942 +apply (auto simp add: mcount_def mset_of_def multiset_def multiset_fun_iff)
   3.943 +apply (auto dest: domain_type simp add: add_diff_eq)
   3.944 +done
   3.945 +
   3.946 +lemma diff_add_commute: "[| n le m;  m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
   3.947 +by (auto simp add: le_iff less_iff_succ_add)
   3.948 +
   3.949 +(* One direction *)
   3.950 +
   3.951 +lemma multirel_implies_one_step:
   3.952 +"<M,N> \<in> multirel(A, r) ==>
   3.953 +     trans[A](r) -->
   3.954 +     (\<exists>I J K.
   3.955 +         I \<in> Mult(A) & J \<in> Mult(A) &  K \<in> Mult(A) &
   3.956 +         N = I +# J & M = I +# K & J \<noteq> 0 &
   3.957 +        (\<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r))"
   3.958 +apply (simp add: multirel_def Ball_def Bex_def)
   3.959 +apply (erule converse_trancl_induct)
   3.960 +apply (simp_all add: multirel1_iff Mult_iff_multiset)
   3.961 +(* Two subgoals remain *)
   3.962 +(* Subgoal 1 *)
   3.963 +apply clarify
   3.964 +apply (rule_tac x = M0 in exI, force)
   3.965 +(* Subgoal 2 *)
   3.966 +apply clarify
   3.967 +apply (case_tac "a \<in> mset_of (Ka) ")
   3.968 +apply (rule_tac x = I in exI, simp (no_asm_simp))
   3.969 +apply (rule_tac x = J in exI, simp (no_asm_simp))
   3.970 +apply (rule_tac x = " (Ka -# {#a#}) +# K" in exI, simp (no_asm_simp))
   3.971 +apply (simp_all add: Un_subset_iff)
   3.972 +apply (simp (no_asm_simp) add: munion_assoc [symmetric])
   3.973 +apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
   3.974 +apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
   3.975 +apply (erule disjE, simp)
   3.976 +apply (erule disjE, simp)
   3.977 +apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> ?Q(x)" in spec)
   3.978 +apply clarify
   3.979 +apply (rule_tac x = xa in exI)
   3.980 +apply (simp (no_asm_simp))
   3.981 +apply (blast dest: trans_onD)
   3.982 +(* new we know that  a\<notin>mset_of(Ka) *)
   3.983 +apply (subgoal_tac "a :# I")
   3.984 +apply (rule_tac x = "I-#{#a#}" in exI, simp (no_asm_simp))
   3.985 +apply (rule_tac x = "J+#{#a#}" in exI)
   3.986 +apply (simp (no_asm_simp) add: Un_subset_iff)
   3.987 +apply (rule_tac x = "Ka +# K" in exI)
   3.988 +apply (simp (no_asm_simp) add: Un_subset_iff)
   3.989 +apply (rule conjI)
   3.990 +apply (simp (no_asm_simp) add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
   3.991 +apply (rule conjI)
   3.992 +apply (drule_tac t = "%M. M-#{#a#}" in subst_context)
   3.993 +apply (simp add: mdiff_union_inverse2)
   3.994 +apply (simp_all (no_asm_simp) add: multiset_equality)
   3.995 +apply (rule diff_add_commute [symmetric])
   3.996 +apply (auto intro: mcount_elem)
   3.997 +apply (subgoal_tac "a \<in> mset_of (I +# Ka) ")
   3.998 +apply (drule_tac [2] sym, auto)
   3.999 +done
  3.1000 +
  3.1001 +lemma melem_imp_eq_diff_union [simp]: "[| a \<in> mset_of(M); multiset(M) |] ==> M -# {#a#} +# {#a#} = M"
  3.1002 +by (simp add: multiset_equality mcount_elem [THEN succ_pred_eq_self])
  3.1003 +
  3.1004 +lemma msize_eq_succ_imp_eq_union:
  3.1005 +     "[| msize(M)=$# succ(n); M \<in> Mult(A); n \<in> nat |]
  3.1006 +      ==> \<exists>a N. M = N +# {#a#} & N \<in> Mult(A) & a \<in> A"
  3.1007 +apply (drule msize_eq_succ_imp_elem, auto)
  3.1008 +apply (rule_tac x = a in exI)
  3.1009 +apply (rule_tac x = "M -# {#a#}" in exI)
  3.1010 +apply (frule Mult_into_multiset)
  3.1011 +apply (simp (no_asm_simp))
  3.1012 +apply (auto simp add: Mult_iff_multiset)
  3.1013 +done
  3.1014 +
  3.1015 +(* The second direction *)
  3.1016 +
  3.1017 +lemma one_step_implies_multirel_lemma [rule_format (no_asm)]:
  3.1018 +"n \<in> nat ==>
  3.1019 +   (\<forall>I J K.
  3.1020 +    I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
  3.1021 +   (msize(J) = $# n & J \<noteq>0 &  (\<forall>k \<in> mset_of(K).  \<exists>j \<in> mset_of(J). <k, j> \<in> r))
  3.1022 +    --> <I +# K, I +# J> \<in> multirel(A, r))"
  3.1023 +apply (simp add: Mult_iff_multiset)
  3.1024 +apply (erule nat_induct, clarify)
  3.1025 +apply (drule_tac M = J in msize_eq_0_iff, auto)
  3.1026 +(* one subgoal remains *)
  3.1027 +apply (subgoal_tac "msize (J) =$# succ (x) ")
  3.1028 + prefer 2 apply simp
  3.1029 +apply (frule_tac A = A in msize_eq_succ_imp_eq_union)
  3.1030 +apply (simp_all add: Mult_iff_multiset, clarify)
  3.1031 +apply (rename_tac "J'", simp)
  3.1032 +apply (case_tac "J' = 0")
  3.1033 +apply (simp add: multirel_def)
  3.1034 +apply (rule r_into_trancl, clarify)
  3.1035 +apply (simp add: multirel1_iff Mult_iff_multiset, force)
  3.1036 +(*Now we know J' \<noteq>  0*)
  3.1037 +apply (drule sym, rotate_tac -1, simp)
  3.1038 +apply (erule_tac V = "$# x = msize (J') " in thin_rl)
  3.1039 +apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
  3.1040 +apply (erule_tac P = "\<forall>k \<in> mset_of (K) . ?P (k) " in rev_mp)
  3.1041 +apply (erule ssubst)
  3.1042 +apply (simp add: Ball_def, auto)
  3.1043 +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) ")
  3.1044 + prefer 2
  3.1045 + apply (drule_tac x = "I +# {# x \<in> K. <x, a> \<in> r#}" in spec)
  3.1046 + apply (rotate_tac -1)
  3.1047 + apply (drule_tac x = "J'" in spec)
  3.1048 + apply (rotate_tac -1)
  3.1049 + apply (drule_tac x = "{# x \<in> K. <x, a> \<notin> r#}" in spec, simp) apply blast
  3.1050 +apply (simp add: munion_assoc [symmetric] multirel_def)
  3.1051 +apply (rule_tac b = "I +# {# x \<in> K. <x, a> \<in> r#} +# J'" in trancl_trans, blast)
  3.1052 +apply (rule r_into_trancl)
  3.1053 +apply (simp add: multirel1_iff Mult_iff_multiset)
  3.1054 +apply (rule_tac x = a in exI)
  3.1055 +apply (simp (no_asm_simp))
  3.1056 +apply (rule_tac x = "I +# J'" in exI)
  3.1057 +apply (auto simp add: munion_ac Un_subset_iff)
  3.1058 +done
  3.1059 +
  3.1060 +lemma one_step_implies_multirel:
  3.1061 +     "[| J \<noteq> 0;  \<forall>k \<in> mset_of(K). \<exists>j \<in> mset_of(J). <k,j> \<in> r;
  3.1062 +         I \<in> Mult(A); J \<in> Mult(A); K \<in> Mult(A) |]
  3.1063 +      ==> <I+#K, I+#J> \<in> multirel(A, r)"
  3.1064 +apply (subgoal_tac "multiset (J) ")
  3.1065 + prefer 2 apply (simp add: Mult_iff_multiset)
  3.1066 +apply (frule_tac M = J in msize_int_of_nat)
  3.1067 +apply (auto intro: one_step_implies_multirel_lemma)
  3.1068 +done
  3.1069 +
  3.1070 +(** Proving that multisets are partially ordered **)
  3.1071 +
  3.1072 +(*irreflexivity*)
  3.1073 +
  3.1074 +lemma multirel_irrefl_lemma:
  3.1075 +     "Finite(A) ==> part_ord(A, r) --> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) -->A=0"
  3.1076 +apply (erule Finite_induct)
  3.1077 +apply (auto dest: subset_consI [THEN [2] part_ord_subset])
  3.1078 +apply (auto simp add: part_ord_def irrefl_def)
  3.1079 +apply (drule_tac x = xa in bspec)
  3.1080 +apply (drule_tac [2] a = xa and b = x in trans_onD, auto)
  3.1081 +done
  3.1082 +
  3.1083 +lemma irrefl_on_multirel:
  3.1084 +     "part_ord(A, r) ==> irrefl(Mult(A), multirel(A, r))"
  3.1085 +apply (simp add: irrefl_def)
  3.1086 +apply (subgoal_tac "trans[A](r) ")
  3.1087 + prefer 2 apply (simp add: part_ord_def, clarify)
  3.1088 +apply (drule multirel_implies_one_step, clarify)
  3.1089 +apply (simp add: Mult_iff_multiset, clarify)
  3.1090 +apply (subgoal_tac "Finite (mset_of (K))")
  3.1091 +apply (frule_tac r = r in multirel_irrefl_lemma)
  3.1092 +apply (frule_tac B = "mset_of (K) " in part_ord_subset)
  3.1093 +apply simp_all
  3.1094 +apply (auto simp add: multiset_def mset_of_def)
  3.1095 +done
  3.1096 +
  3.1097 +lemma trans_on_multirel: "trans[Mult(A)](multirel(A, r))"
  3.1098 +apply (simp add: multirel_def trans_on_def)
  3.1099 +apply (blast intro: trancl_trans)
  3.1100 +done
  3.1101 +
  3.1102 +lemma multirel_trans:
  3.1103 + "[| <M, N> \<in> multirel(A, r); <N, K> \<in> multirel(A, r) |] ==>  <M, K> \<in> multirel(A,r)"
  3.1104 +apply (simp add: multirel_def)
  3.1105 +apply (blast intro: trancl_trans)
  3.1106 +done
  3.1107 +
  3.1108 +lemma trans_multirel: "trans(multirel(A,r))"
  3.1109 +apply (simp add: multirel_def)
  3.1110 +apply (rule trans_trancl)
  3.1111 +done
  3.1112 +
  3.1113 +lemma part_ord_multirel: "part_ord(A,r) ==> part_ord(Mult(A), multirel(A, r))"
  3.1114 +apply (simp (no_asm) add: part_ord_def)
  3.1115 +apply (blast intro: irrefl_on_multirel trans_on_multirel)
  3.1116 +done
  3.1117 +
  3.1118 +(** Monotonicity of multiset union **)
  3.1119 +
  3.1120 +lemma munion_multirel1_mono:
  3.1121 +"[|<M,N> \<in> multirel1(A, r); K \<in> Mult(A) |] ==> <K +# M, K +# N> \<in> multirel1(A, r)"
  3.1122 +apply (frule multirel1_type [THEN subsetD])
  3.1123 +apply (auto simp add: multirel1_iff Mult_iff_multiset)
  3.1124 +apply (rule_tac x = a in exI)
  3.1125 +apply (simp (no_asm_simp))
  3.1126 +apply (rule_tac x = "K+#M0" in exI)
  3.1127 +apply (simp (no_asm_simp) add: Un_subset_iff)
  3.1128 +apply (rule_tac x = Ka in exI)
  3.1129 +apply (simp (no_asm_simp) add: munion_assoc)
  3.1130 +done
  3.1131 +
  3.1132 +lemma munion_multirel_mono2:
  3.1133 + "[| <M, N> \<in> multirel(A, r); K \<in> Mult(A) |]==><K +# M, K +# N> \<in> multirel(A, r)"
  3.1134 +apply (frule multirel_type [THEN subsetD])
  3.1135 +apply (simp (no_asm_use) add: multirel_def)
  3.1136 +apply clarify
  3.1137 +apply (drule_tac psi = "<M,N> \<in> multirel1 (A, r) ^+" in asm_rl)
  3.1138 +apply (erule rev_mp)
  3.1139 +apply (erule rev_mp)
  3.1140 +apply (erule rev_mp)
  3.1141 +apply (erule trancl_induct, clarify)
  3.1142 +apply (blast intro: munion_multirel1_mono r_into_trancl, clarify)
  3.1143 +apply (subgoal_tac "y \<in> Mult (A) ")
  3.1144 + prefer 2
  3.1145 + apply (blast dest: multirel_type [unfolded multirel_def, THEN subsetD])
  3.1146 +apply (subgoal_tac "<K +# y, K +# z> \<in> multirel1 (A, r) ")
  3.1147 +prefer 2 apply (blast intro: munion_multirel1_mono)
  3.1148 +apply (blast intro: r_into_trancl trancl_trans)
  3.1149 +done
  3.1150 +
  3.1151 +lemma munion_multirel_mono1:
  3.1152 +     "[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
  3.1153 +apply (frule multirel_type [THEN subsetD])
  3.1154 +apply (rule_tac P = "%x. <x,?u> \<in> multirel (A, r) " in munion_commute [THEN subst])
  3.1155 +apply (subst munion_commute [symmetric])
  3.1156 +apply (rule munion_multirel_mono2)
  3.1157 +apply (auto simp add: Mult_iff_multiset)
  3.1158 +done
  3.1159 +
  3.1160 +lemma munion_multirel_mono:
  3.1161 +     "[|<M,K> \<in> multirel(A, r); <N,L> \<in> multirel(A, r)|]
  3.1162 +      ==> <M +# N, K +# L> \<in> multirel(A, r)"
  3.1163 +apply (subgoal_tac "M \<in> Mult (A) & N \<in> Mult (A) & K \<in> Mult (A) & L \<in> Mult (A) ")
  3.1164 +prefer 2 apply (blast dest: multirel_type [THEN subsetD])
  3.1165 +apply (blast intro: munion_multirel_mono1 multirel_trans munion_multirel_mono2)
  3.1166 +done
  3.1167 +
  3.1168 +
  3.1169 +subsection{*Ordinal Multisets*}
  3.1170 +
  3.1171 +(* A \<subseteq> B ==>  field(Memrel(A)) \<subseteq> field(Memrel(B)) *)
  3.1172 +lemmas field_Memrel_mono = Memrel_mono [THEN field_mono, standard]
  3.1173 +
  3.1174 +(*
  3.1175 +[| Aa \<subseteq> Ba; A \<subseteq> B |] ==>
  3.1176 +multirel(field(Memrel(Aa)), Memrel(A))\<subseteq> multirel(field(Memrel(Ba)), Memrel(B))
  3.1177 +*)
  3.1178 +
  3.1179 +lemmas multirel_Memrel_mono = multirel_mono [OF field_Memrel_mono Memrel_mono]
  3.1180 +
  3.1181 +lemma omultiset_is_multiset [simp]: "omultiset(M) ==> multiset(M)"
  3.1182 +apply (simp add: omultiset_def)
  3.1183 +apply (auto simp add: Mult_iff_multiset)
  3.1184 +done
  3.1185 +
  3.1186 +lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)"
  3.1187 +apply (simp add: omultiset_def, clarify)
  3.1188 +apply (rule_tac x = "i Un ia" in exI)
  3.1189 +apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
  3.1190 +apply (blast intro: field_Memrel_mono)
  3.1191 +done
  3.1192 +
  3.1193 +lemma mdiff_omultiset [simp]: "omultiset(M) ==> omultiset(M -# N)"
  3.1194 +apply (simp add: omultiset_def, clarify)
  3.1195 +apply (simp add: Mult_iff_multiset)
  3.1196 +apply (rule_tac x = i in exI)
  3.1197 +apply (simp (no_asm_simp))
  3.1198 +done
  3.1199 +
  3.1200 +(** Proving that Memrel is a partial order **)
  3.1201 +
  3.1202 +lemma irrefl_Memrel: "Ord(i) ==> irrefl(field(Memrel(i)), Memrel(i))"
  3.1203 +apply (rule irreflI, clarify)
  3.1204 +apply (subgoal_tac "Ord (x) ")
  3.1205 +prefer 2 apply (blast intro: Ord_in_Ord)
  3.1206 +apply (drule_tac i = x in ltI [THEN lt_irrefl], auto)
  3.1207 +done
  3.1208 +
  3.1209 +lemma trans_iff_trans_on: "trans(r) <-> trans[field(r)](r)"
  3.1210 +by (simp add: trans_on_def trans_def, auto)
  3.1211 +
  3.1212 +lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))"
  3.1213 +apply (simp add: part_ord_def)
  3.1214 +apply (simp (no_asm) add: trans_iff_trans_on [THEN iff_sym])
  3.1215 +apply (blast intro: trans_Memrel irrefl_Memrel)
  3.1216 +done
  3.1217 +
  3.1218 +(*
  3.1219 +  Ord(i) ==>
  3.1220 +  part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
  3.1221 +*)
  3.1222 +
  3.1223 +lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel, standard]
  3.1224 +
  3.1225 +(*irreflexivity*)
  3.1226 +
  3.1227 +lemma mless_not_refl: "~(M <# M)"
  3.1228 +apply (simp add: mless_def, clarify)
  3.1229 +apply (frule multirel_type [THEN subsetD])
  3.1230 +apply (drule part_ord_mless)
  3.1231 +apply (simp add: part_ord_def irrefl_def)
  3.1232 +done
  3.1233 +
  3.1234 +(* N<N ==> R *)
  3.1235 +lemmas mless_irrefl = mless_not_refl [THEN notE, standard, elim!]
  3.1236 +
  3.1237 +(*transitivity*)
  3.1238 +lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
  3.1239 +apply (simp add: mless_def, clarify)
  3.1240 +apply (rule_tac x = "i Un ia" in exI)
  3.1241 +apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD]
  3.1242 +                   multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD]
  3.1243 +        intro: multirel_trans Ord_Un)
  3.1244 +done
  3.1245 +
  3.1246 +(*asymmetry*)
  3.1247 +lemma mless_not_sym: "M <# N ==> ~ N <# M"
  3.1248 +apply clarify
  3.1249 +apply (rule mless_not_refl [THEN notE])
  3.1250 +apply (erule mless_trans, assumption)
  3.1251 +done
  3.1252 +
  3.1253 +lemma mless_asym: "[| M <# N; ~P ==> N <# M |] ==> P"
  3.1254 +by (blast dest: mless_not_sym)
  3.1255 +
  3.1256 +lemma mle_refl [simp]: "omultiset(M) ==> M <#= M"
  3.1257 +by (simp add: mle_def)
  3.1258 +
  3.1259 +(*anti-symmetry*)
  3.1260 +lemma mle_antisym:
  3.1261 +     "[| M <#= N;  N <#= M |] ==> M = N"
  3.1262 +apply (simp add: mle_def)
  3.1263 +apply (blast dest: mless_not_sym)
  3.1264 +done
  3.1265 +
  3.1266 +(*transitivity*)
  3.1267 +lemma mle_trans: "[| K <#= M; M <#= N |] ==> K <#= N"
  3.1268 +apply (simp add: mle_def)
  3.1269 +apply (blast intro: mless_trans)
  3.1270 +done
  3.1271 +
  3.1272 +lemma mless_le_iff: "M <# N <-> (M <#= N & M \<noteq> N)"
  3.1273 +by (simp add: mle_def, auto)
  3.1274 +
  3.1275 +(** Monotonicity of mless **)
  3.1276 +
  3.1277 +lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N"
  3.1278 +apply (simp add: mless_def omultiset_def, clarify)
  3.1279 +apply (rule_tac x = "i Un ia" in exI)
  3.1280 +apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
  3.1281 +apply (rule munion_multirel_mono2)
  3.1282 + apply (blast intro: multirel_Memrel_mono [THEN subsetD])
  3.1283 +apply (simp add: Mult_iff_multiset)
  3.1284 +apply (blast intro: field_Memrel_mono [THEN subsetD])
  3.1285 +done
  3.1286 +
  3.1287 +lemma munion_less_mono1: "[| M <# N; omultiset(K) |] ==> M +# K <# N +# K"
  3.1288 +by (force dest: munion_less_mono2 simp add: munion_commute)
  3.1289 +
  3.1290 +lemma mless_imp_omultiset: "M <# N ==> omultiset(M) & omultiset(N)"
  3.1291 +by (auto simp add: mless_def omultiset_def dest: multirel_type [THEN subsetD])
  3.1292 +
  3.1293 +lemma munion_less_mono: "[| M <# K; N <# L |] ==> M +# N <# K +# L"
  3.1294 +apply (frule_tac M = M in mless_imp_omultiset)
  3.1295 +apply (frule_tac M = N in mless_imp_omultiset)
  3.1296 +apply (blast intro: munion_less_mono1 munion_less_mono2 mless_trans)
  3.1297 +done
  3.1298 +
  3.1299 +(* <#= *)
  3.1300 +
  3.1301 +lemma mle_imp_omultiset: "M <#= N ==> omultiset(M) & omultiset(N)"
  3.1302 +by (auto simp add: mle_def mless_imp_omultiset)
  3.1303 +
  3.1304 +lemma mle_mono: "[| M <#= K;  N <#= L |] ==> M +# N <#= K +# L"
  3.1305 +apply (frule_tac M = M in mle_imp_omultiset)
  3.1306 +apply (frule_tac M = N in mle_imp_omultiset)
  3.1307 +apply (auto simp add: mle_def intro: munion_less_mono1 munion_less_mono2 munion_less_mono)
  3.1308 +done
  3.1309 +
  3.1310 +lemma omultiset_0 [iff]: "omultiset(0)"
  3.1311 +by (auto simp add: omultiset_def Mult_iff_multiset)
  3.1312 +
  3.1313 +lemma empty_leI [simp]: "omultiset(M) ==> 0 <#= M"
  3.1314 +apply (simp add: mle_def mless_def)
  3.1315 +apply (subgoal_tac "\<exists>i. Ord (i) & M \<in> Mult (field (Memrel (i))) ")
  3.1316 + prefer 2 apply (simp add: omultiset_def)
  3.1317 +apply (case_tac "M=0", simp_all, clarify)
  3.1318 +apply (subgoal_tac "<0 +# 0, 0 +# M> \<in> multirel (field (Memrel (i)), Memrel (i))")
  3.1319 +apply (rule_tac [2] one_step_implies_multirel)
  3.1320 +apply (auto simp add: Mult_iff_multiset)
  3.1321 +done
  3.1322 +
  3.1323 +lemma munion_upper1: "[| omultiset(M); omultiset(N) |] ==> M <#= M +# N"
  3.1324 +apply (subgoal_tac "M +# 0 <#= M +# N")
  3.1325 +apply (rule_tac [2] mle_mono, auto)
  3.1326 +done
  3.1327 +
  3.1328 +ML
  3.1329 +{*
  3.1330 +val munion_ac = thms "munion_ac";
  3.1331 +val funrestrict_subset = thm "funrestrict_subset";
  3.1332 +val funrestrict_type = thm "funrestrict_type";
  3.1333 +val funrestrict_type2 = thm "funrestrict_type2";
  3.1334 +val funrestrict = thm "funrestrict";
  3.1335 +val funrestrict_empty = thm "funrestrict_empty";
  3.1336 +val domain_funrestrict = thm "domain_funrestrict";
  3.1337 +val fun_cons_funrestrict_eq = thm "fun_cons_funrestrict_eq";
  3.1338 +val multiset_fun_iff = thm "multiset_fun_iff";
  3.1339 +val multiset_into_Mult = thm "multiset_into_Mult";
  3.1340 +val Mult_into_multiset = thm "Mult_into_multiset";
  3.1341 +val Mult_iff_multiset = thm "Mult_iff_multiset";
  3.1342 +val multiset_iff_Mult_mset_of = thm "multiset_iff_Mult_mset_of";
  3.1343 +val multiset_0 = thm "multiset_0";
  3.1344 +val multiset_set_of_Finite = thm "multiset_set_of_Finite";
  3.1345 +val mset_of_0 = thm "mset_of_0";
  3.1346 +val mset_is_0_iff = thm "mset_is_0_iff";
  3.1347 +val mset_of_single = thm "mset_of_single";
  3.1348 +val mset_of_union = thm "mset_of_union";
  3.1349 +val mset_of_diff = thm "mset_of_diff";
  3.1350 +val msingle_not_0 = thm "msingle_not_0";
  3.1351 +val msingle_eq_iff = thm "msingle_eq_iff";
  3.1352 +val msingle_multiset = thm "msingle_multiset";
  3.1353 +val Collect_Finite = thms "Collect_Finite";
  3.1354 +val normalize_idem = thm "normalize_idem";
  3.1355 +val normalize_multiset = thm "normalize_multiset";
  3.1356 +val multiset_normalize = thm "multiset_normalize";
  3.1357 +val munion_multiset = thm "munion_multiset";
  3.1358 +val mdiff_multiset = thm "mdiff_multiset";
  3.1359 +val munion_0 = thm "munion_0";
  3.1360 +val munion_commute = thm "munion_commute";
  3.1361 +val munion_assoc = thm "munion_assoc";
  3.1362 +val munion_lcommute = thm "munion_lcommute";
  3.1363 +val mdiff_self_eq_0 = thm "mdiff_self_eq_0";
  3.1364 +val mdiff_0 = thm "mdiff_0";
  3.1365 +val mdiff_0_right = thm "mdiff_0_right";
  3.1366 +val mdiff_union_inverse2 = thm "mdiff_union_inverse2";
  3.1367 +val mcount_type = thm "mcount_type";
  3.1368 +val mcount_0 = thm "mcount_0";
  3.1369 +val mcount_single = thm "mcount_single";
  3.1370 +val mcount_union = thm "mcount_union";
  3.1371 +val mcount_diff = thm "mcount_diff";
  3.1372 +val mcount_elem = thm "mcount_elem";
  3.1373 +val msize_0 = thm "msize_0";
  3.1374 +val msize_single = thm "msize_single";
  3.1375 +val msize_type = thm "msize_type";
  3.1376 +val msize_zpositive = thm "msize_zpositive";
  3.1377 +val msize_int_of_nat = thm "msize_int_of_nat";
  3.1378 +val not_empty_multiset_imp_exist = thm "not_empty_multiset_imp_exist";
  3.1379 +val msize_eq_0_iff = thm "msize_eq_0_iff";
  3.1380 +val setsum_mcount_Int = thm "setsum_mcount_Int";
  3.1381 +val msize_union = thm "msize_union";
  3.1382 +val msize_eq_succ_imp_elem = thm "msize_eq_succ_imp_elem";
  3.1383 +val multiset_equality = thm "multiset_equality";
  3.1384 +val munion_eq_0_iff = thm "munion_eq_0_iff";
  3.1385 +val empty_eq_munion_iff = thm "empty_eq_munion_iff";
  3.1386 +val munion_right_cancel = thm "munion_right_cancel";
  3.1387 +val munion_left_cancel = thm "munion_left_cancel";
  3.1388 +val nat_add_eq_1_cases = thm "nat_add_eq_1_cases";
  3.1389 +val munion_is_single = thm "munion_is_single";
  3.1390 +val msingle_is_union = thm "msingle_is_union";
  3.1391 +val setsum_decr = thm "setsum_decr";
  3.1392 +val setsum_decr2 = thm "setsum_decr2";
  3.1393 +val setsum_decr3 = thm "setsum_decr3";
  3.1394 +val nat_le_1_cases = thm "nat_le_1_cases";
  3.1395 +val succ_pred_eq_self = thm "succ_pred_eq_self";
  3.1396 +val multiset_funrestict = thm "multiset_funrestict";
  3.1397 +val multiset_induct_aux = thm "multiset_induct_aux";
  3.1398 +val multiset_induct2 = thm "multiset_induct2";
  3.1399 +val munion_single_case1 = thm "munion_single_case1";
  3.1400 +val munion_single_case2 = thm "munion_single_case2";
  3.1401 +val multiset_induct = thm "multiset_induct";
  3.1402 +val MCollect_multiset = thm "MCollect_multiset";
  3.1403 +val mset_of_MCollect = thm "mset_of_MCollect";
  3.1404 +val MCollect_mem_iff = thm "MCollect_mem_iff";
  3.1405 +val mcount_MCollect = thm "mcount_MCollect";
  3.1406 +val multiset_partition = thm "multiset_partition";
  3.1407 +val natify_elem_is_self = thm "natify_elem_is_self";
  3.1408 +val munion_eq_conv_diff = thm "munion_eq_conv_diff";
  3.1409 +val melem_diff_single = thm "melem_diff_single";
  3.1410 +val munion_eq_conv_exist = thm "munion_eq_conv_exist";
  3.1411 +val multirel1_type = thm "multirel1_type";
  3.1412 +val multirel1_0 = thm "multirel1_0";
  3.1413 +val multirel1_iff = thm "multirel1_iff";
  3.1414 +val multirel1_mono1 = thm "multirel1_mono1";
  3.1415 +val multirel1_mono2 = thm "multirel1_mono2";
  3.1416 +val multirel1_mono = thm "multirel1_mono";
  3.1417 +val not_less_0 = thm "not_less_0";
  3.1418 +val less_munion = thm "less_munion";
  3.1419 +val multirel1_base = thm "multirel1_base";
  3.1420 +val acc_0 = thm "acc_0";
  3.1421 +val all_accessible = thm "all_accessible";
  3.1422 +val wf_on_multirel1 = thm "wf_on_multirel1";
  3.1423 +val wf_multirel1 = thm "wf_multirel1";
  3.1424 +val multirel_type = thm "multirel_type";
  3.1425 +val multirel_mono = thm "multirel_mono";
  3.1426 +val add_diff_eq = thm "add_diff_eq";
  3.1427 +val mdiff_union_single_conv = thm "mdiff_union_single_conv";
  3.1428 +val diff_add_commute = thm "diff_add_commute";
  3.1429 +val multirel_implies_one_step = thm "multirel_implies_one_step";
  3.1430 +val melem_imp_eq_diff_union = thm "melem_imp_eq_diff_union";
  3.1431 +val msize_eq_succ_imp_eq_union = thm "msize_eq_succ_imp_eq_union";
  3.1432 +val one_step_implies_multirel = thm "one_step_implies_multirel";
  3.1433 +val irrefl_on_multirel = thm "irrefl_on_multirel";
  3.1434 +val trans_on_multirel = thm "trans_on_multirel";
  3.1435 +val multirel_trans = thm "multirel_trans";
  3.1436 +val trans_multirel = thm "trans_multirel";
  3.1437 +val part_ord_multirel = thm "part_ord_multirel";
  3.1438 +val munion_multirel1_mono = thm "munion_multirel1_mono";
  3.1439 +val munion_multirel_mono2 = thm "munion_multirel_mono2";
  3.1440 +val munion_multirel_mono1 = thm "munion_multirel_mono1";
  3.1441 +val munion_multirel_mono = thm "munion_multirel_mono";
  3.1442 +val field_Memrel_mono = thms "field_Memrel_mono";
  3.1443 +val multirel_Memrel_mono = thms "multirel_Memrel_mono";
  3.1444 +val omultiset_is_multiset = thm "omultiset_is_multiset";
  3.1445 +val munion_omultiset = thm "munion_omultiset";
  3.1446 +val mdiff_omultiset = thm "mdiff_omultiset";
  3.1447 +val irrefl_Memrel = thm "irrefl_Memrel";
  3.1448 +val trans_iff_trans_on = thm "trans_iff_trans_on";
  3.1449 +val part_ord_Memrel = thm "part_ord_Memrel";
  3.1450 +val part_ord_mless = thms "part_ord_mless";
  3.1451 +val mless_not_refl = thm "mless_not_refl";
  3.1452 +val mless_irrefl = thms "mless_irrefl";
  3.1453 +val mless_trans = thm "mless_trans";
  3.1454 +val mless_not_sym = thm "mless_not_sym";
  3.1455 +val mless_asym = thm "mless_asym";
  3.1456 +val mle_refl = thm "mle_refl";
  3.1457 +val mle_antisym = thm "mle_antisym";
  3.1458 +val mle_trans = thm "mle_trans";
  3.1459 +val mless_le_iff = thm "mless_le_iff";
  3.1460 +val munion_less_mono2 = thm "munion_less_mono2";
  3.1461 +val munion_less_mono1 = thm "munion_less_mono1";
  3.1462 +val mless_imp_omultiset = thm "mless_imp_omultiset";
  3.1463 +val munion_less_mono = thm "munion_less_mono";
  3.1464 +val mle_imp_omultiset = thm "mle_imp_omultiset";
  3.1465 +val mle_mono = thm "mle_mono";
  3.1466 +val omultiset_0 = thm "omultiset_0";
  3.1467 +val empty_leI = thm "empty_leI";
  3.1468 +val munion_upper1 = thm "munion_upper1";
  3.1469 +*}
  3.1470 +
  3.1471  end
     4.1 --- a/src/ZF/IsaMakefile	Mon Sep 13 09:57:25 2004 +0200
     4.2 +++ b/src/ZF/IsaMakefile	Fri Sep 17 16:08:52 2004 +0200
     4.3 @@ -135,7 +135,7 @@
     4.4  $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.thy \
     4.5    Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
     4.6    Induct/Datatypes.thy Induct/FoldSet.thy \
     4.7 -  Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
     4.8 +  Induct/ListN.thy Induct/Multiset.thy Induct/Mutil.thy \
     4.9    Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
    4.10    Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
    4.11  	@$(ISATOOL) usedir $(OUT)/ZF Induct