src/HOL/Induct/Multiset.ML
changeset 10258 d549f2534e6d
parent 10257 21055ac27708
child 10259 93ec82d535f2
     1.1 --- a/src/HOL/Induct/Multiset.ML	Wed Oct 18 23:35:56 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,715 +0,0 @@
     1.4 -(*  Title:      HOL/Induct/Multiset.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow
     1.7 -    Copyright   1998 TUM
     1.8 -*)
     1.9 -
    1.10 -Addsimps [Abs_multiset_inverse, Rep_multiset_inverse, Rep_multiset,
    1.11 -	  Zero_def];
    1.12 -
    1.13 -(** Preservation of representing set `multiset' **)
    1.14 -
    1.15 -Goalw [multiset_def] "(%a. 0) : multiset";
    1.16 -by (Simp_tac 1);
    1.17 -qed "const0_in_multiset";
    1.18 -Addsimps [const0_in_multiset];
    1.19 -
    1.20 -Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
    1.21 -by (Simp_tac 1);
    1.22 -qed "only1_in_multiset";
    1.23 -Addsimps [only1_in_multiset];
    1.24 -
    1.25 -Goalw [multiset_def]
    1.26 - "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
    1.27 -by (Asm_full_simp_tac 1);
    1.28 -by (dtac finite_UnI 1);
    1.29 -by (assume_tac 1);
    1.30 -by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
    1.31 -qed "union_preserves_multiset";
    1.32 -Addsimps [union_preserves_multiset];
    1.33 -
    1.34 -Goalw [multiset_def]
    1.35 - "[| M : multiset |] ==> (%a. M a - N a) : multiset";
    1.36 -by (Asm_full_simp_tac 1);
    1.37 -by (etac (rotate_prems 1 finite_subset) 1);
    1.38 -by Auto_tac;
    1.39 -qed "diff_preserves_multiset";
    1.40 -Addsimps [diff_preserves_multiset];
    1.41 -
    1.42 -(** Injectivity of Rep_multiset **)
    1.43 -
    1.44 -Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
    1.45 -by (rtac iffI 1);
    1.46 - by (Asm_simp_tac 1);
    1.47 -by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
    1.48 -by (Asm_full_simp_tac 1);
    1.49 -qed "multiset_eq_conv_Rep_eq";
    1.50 -Addsimps [multiset_eq_conv_Rep_eq];
    1.51 -Addsimps [expand_fun_eq];
    1.52 -
    1.53 -(*
    1.54 -Goal
    1.55 - "[| f : multiset; g : multiset |] ==> \
    1.56 -\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
    1.57 -by (rtac iffI 1);
    1.58 - by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    1.59 - by (Asm_full_simp_tac 1);
    1.60 -by (subgoal_tac "f = g" 1);
    1.61 - by (Asm_simp_tac 1);
    1.62 -by (rtac ext 1);
    1.63 -by (Blast_tac 1);
    1.64 -qed "Abs_multiset_eq";
    1.65 -Addsimps [Abs_multiset_eq];
    1.66 -*)
    1.67 -
    1.68 -(** Equations **)
    1.69 -
    1.70 -(* union *)
    1.71 -
    1.72 -Goalw [union_def,empty_def]
    1.73 - "M + {#} = M & {#} + M = M";
    1.74 -by (Simp_tac 1);
    1.75 -qed "union_empty";
    1.76 -Addsimps [union_empty];
    1.77 -
    1.78 -Goalw [union_def]
    1.79 - "(M::'a multiset) + N = N + M";
    1.80 -by (simp_tac (simpset() addsimps add_ac) 1);
    1.81 -qed "union_commute";
    1.82 -
    1.83 -Goalw [union_def]
    1.84 - "((M::'a multiset)+N)+K = M+(N+K)";
    1.85 -by (simp_tac (simpset() addsimps add_ac) 1);
    1.86 -qed "union_assoc";
    1.87 -
    1.88 -Goal "M+(N+K) = N+((M+K)::'a multiset)";
    1.89 -by (rtac (union_commute RS trans) 1);
    1.90 -by (rtac (union_assoc RS trans) 1);
    1.91 -by (rtac (union_commute RS arg_cong) 1);
    1.92 -qed "union_lcomm";
    1.93 -
    1.94 -bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]);
    1.95 -
    1.96 -(* diff *)
    1.97 -
    1.98 -Goalw [empty_def,diff_def]
    1.99 - "M-{#} = M & {#}-M = {#}";
   1.100 -by (Simp_tac 1);
   1.101 -qed "diff_empty";
   1.102 -Addsimps [diff_empty];
   1.103 -
   1.104 -Goalw [union_def,diff_def]
   1.105 - "M+{#a#}-{#a#} = M";
   1.106 -by (Simp_tac 1);
   1.107 -qed "diff_union_inverse2";
   1.108 -Addsimps [diff_union_inverse2];
   1.109 -
   1.110 -(* count *)
   1.111 -
   1.112 -Goalw [count_def,empty_def]
   1.113 - "count {#} a = 0";
   1.114 -by (Simp_tac 1);
   1.115 -qed "count_empty";
   1.116 -Addsimps [count_empty];
   1.117 -
   1.118 -Goalw [count_def,single_def]
   1.119 - "count {#b#} a = (if b=a then 1 else 0)";
   1.120 -by (Simp_tac 1);
   1.121 -qed "count_single";
   1.122 -Addsimps [count_single];
   1.123 -
   1.124 -Goalw [count_def,union_def]
   1.125 - "count (M+N) a = count M a + count N a";
   1.126 -by (Simp_tac 1);
   1.127 -qed "count_union";
   1.128 -Addsimps [count_union];
   1.129 -
   1.130 -Goalw [count_def,diff_def]
   1.131 - "count (M-N) a = count M a - count N a";
   1.132 -by (Simp_tac 1);
   1.133 -qed "count_diff";
   1.134 -Addsimps [count_diff];
   1.135 -
   1.136 -(* set_of *)
   1.137 -
   1.138 -Goalw [set_of_def] "set_of {#} = {}";
   1.139 -by (Simp_tac 1);
   1.140 -qed "set_of_empty";
   1.141 -Addsimps [set_of_empty];
   1.142 -
   1.143 -Goalw [set_of_def]
   1.144 - "set_of {#b#} = {b}";
   1.145 -by (Simp_tac 1);
   1.146 -qed "set_of_single";
   1.147 -Addsimps [set_of_single];
   1.148 -
   1.149 -Goalw [set_of_def]
   1.150 - "set_of(M+N) = set_of M Un set_of N";
   1.151 -by Auto_tac;
   1.152 -qed "set_of_union";
   1.153 -Addsimps [set_of_union];
   1.154 -
   1.155 -Goalw [set_of_def, empty_def, count_def] "(set_of M = {}) = (M = {#})";
   1.156 -by Auto_tac;
   1.157 -qed "set_of_eq_empty_iff";
   1.158 -
   1.159 -Goalw [set_of_def] "(x : set_of M) = (x :# M)";
   1.160 -by Auto_tac; 
   1.161 -qed "mem_set_of_iff";
   1.162 -
   1.163 -(* size *)
   1.164 -
   1.165 -Goalw [size_def] "size {#} = 0";
   1.166 -by (Simp_tac 1);
   1.167 -qed "size_empty";
   1.168 -Addsimps [size_empty];
   1.169 -
   1.170 -Goalw [size_def] "size {#b#} = 1";
   1.171 -by (Simp_tac 1);
   1.172 -qed "size_single";
   1.173 -Addsimps [size_single];
   1.174 -
   1.175 -Goal "finite (set_of M)";
   1.176 -by (cut_inst_tac [("x", "M")] Rep_multiset 1);
   1.177 -by (asm_full_simp_tac
   1.178 -    (simpset() addsimps [multiset_def, set_of_def, count_def]) 1);
   1.179 -qed "finite_set_of";
   1.180 -AddIffs [finite_set_of];
   1.181 -
   1.182 -Goal "finite A ==> setsum (count N) (A Int set_of N) = setsum (count N) A";
   1.183 -by (etac finite_induct 1);
   1.184 -by (Simp_tac 1);
   1.185 -by (asm_full_simp_tac (simpset() addsimps [Int_insert_left, set_of_def]) 1);
   1.186 -qed "setsum_count_Int";
   1.187 -
   1.188 -Goalw [size_def] "size (M+N::'a multiset) = size M + size N";
   1.189 -by (subgoal_tac "count (M+N) = (%a. count M a + count N a)" 1);
   1.190 -by (rtac ext 2);
   1.191 -by (Simp_tac 2);
   1.192 -by (asm_simp_tac
   1.193 -    (simpset() addsimps [setsum_Un, setsum_addf, setsum_count_Int]) 1);
   1.194 -by (stac Int_commute 1);
   1.195 -by (asm_simp_tac (simpset() addsimps [setsum_count_Int]) 1);
   1.196 -qed "size_union";
   1.197 -Addsimps [size_union];
   1.198 -
   1.199 -Goalw [size_def, empty_def, count_def] "(size M = 0) = (M = {#})";
   1.200 -by Auto_tac; 
   1.201 -by (asm_full_simp_tac (simpset() addsimps [set_of_def, count_def]) 1); 
   1.202 -qed "size_eq_0_iff_empty";
   1.203 -AddIffs [size_eq_0_iff_empty];
   1.204 -
   1.205 -Goalw [size_def] "size M = Suc n ==> EX a. a :# M";
   1.206 -by (dtac setsum_SucD 1);
   1.207 -by Auto_tac; 
   1.208 -qed "size_eq_Suc_imp_elem";
   1.209 -
   1.210 -
   1.211 -(* equalities *)
   1.212 -
   1.213 -Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
   1.214 -by (Simp_tac 1);
   1.215 -qed "multiset_eq_conv_count_eq";
   1.216 -
   1.217 -Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
   1.218 -by (Simp_tac 1);
   1.219 -qed "single_not_empty";
   1.220 -Addsimps [single_not_empty];
   1.221 -
   1.222 -Goalw [single_def] "({#a#}={#b#}) = (a=b)";
   1.223 -by Auto_tac;
   1.224 -qed "single_eq_single";
   1.225 -Addsimps [single_eq_single];
   1.226 -
   1.227 -Goalw [union_def,empty_def]
   1.228 - "(M+N = {#}) = (M = {#} & N = {#})";
   1.229 -by (Simp_tac 1);
   1.230 -by (Blast_tac 1);
   1.231 -qed "union_eq_empty";
   1.232 -AddIffs [union_eq_empty];
   1.233 -
   1.234 -Goalw [union_def,empty_def]
   1.235 - "({#} = M+N) = (M = {#} & N = {#})";
   1.236 -by (Simp_tac 1);
   1.237 -by (Blast_tac 1);
   1.238 -qed "empty_eq_union";
   1.239 -AddIffs [empty_eq_union];
   1.240 -
   1.241 -Goalw [union_def]
   1.242 - "(M+K = N+K) = (M=(N::'a multiset))";
   1.243 -by (Simp_tac 1);
   1.244 -qed "union_right_cancel";
   1.245 -Addsimps [union_right_cancel];
   1.246 -
   1.247 -Goalw [union_def]
   1.248 - "(K+M = K+N) = (M=(N::'a multiset))";
   1.249 -by (Simp_tac 1);
   1.250 -qed "union_left_cancel";
   1.251 -Addsimps [union_left_cancel];
   1.252 -
   1.253 -Goalw [empty_def,single_def,union_def]
   1.254 - "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
   1.255 -by (simp_tac (simpset() addsimps [add_is_1]) 1);
   1.256 -by (Blast_tac 1);
   1.257 -qed "union_is_single";
   1.258 -
   1.259 -Goalw [empty_def,single_def,union_def]
   1.260 - "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
   1.261 -by (simp_tac (simpset() addsimps [one_is_add]) 1);
   1.262 -by (blast_tac (claset() addDs [sym]) 1);
   1.263 -qed "single_is_union";
   1.264 -
   1.265 -Goalw [single_def,union_def,diff_def]
   1.266 - "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
   1.267 -by (Simp_tac 1);
   1.268 -by (rtac conjI 1);
   1.269 - by (Force_tac 1);
   1.270 -by (Clarify_tac 1);
   1.271 -by (rtac conjI 1);
   1.272 - by (Blast_tac 1);
   1.273 -by (Clarify_tac 1);
   1.274 -by (rtac iffI 1);
   1.275 - by (rtac conjI 1);
   1.276 - by (Clarify_tac 1);
   1.277 -  by (rtac conjI 1);
   1.278 -   by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   1.279 -(* PROOF FAILED:
   1.280 -by (Blast_tac 1);
   1.281 -*)
   1.282 -  by (Fast_tac 1);
   1.283 - by (Asm_simp_tac 1);
   1.284 -by (Force_tac 1);
   1.285 -qed "add_eq_conv_diff";
   1.286 -
   1.287 -(* FIXME
   1.288 -val prems = Goal
   1.289 - "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   1.290 -by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
   1.291 -     measure_induct 1);
   1.292 -by (Clarify_tac 1);
   1.293 -by (resolve_tac prems 1);
   1.294 - by (assume_tac 1);
   1.295 -by (Clarify_tac 1);
   1.296 -by (subgoal_tac "finite G" 1);
   1.297 - by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   1.298 -by (etac allE 1);
   1.299 -by (etac impE 1);
   1.300 - by (Blast_tac 2);
   1.301 -by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   1.302 -no_qed();
   1.303 -val lemma = result();
   1.304 -
   1.305 -val prems = Goal
   1.306 - "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
   1.307 -by (rtac (lemma RS mp) 1);
   1.308 -by (REPEAT(ares_tac prems 1));
   1.309 -qed "finite_psubset_induct";
   1.310 -
   1.311 -Better: use wf_finite_psubset in WF_Rel
   1.312 -*)
   1.313 -
   1.314 -
   1.315 -(** Towards the induction rule **)
   1.316 -
   1.317 -Goal "[| finite F; 0 < f a |] ==> \
   1.318 -\     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
   1.319 -by (etac finite_induct 1);
   1.320 -by Auto_tac;
   1.321 - by (asm_simp_tac (simpset() addsimps add_ac) 1);
   1.322 -by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   1.323 -by Auto_tac;
   1.324 -qed "setsum_decr";
   1.325 -
   1.326 -val prems = Goalw [multiset_def]
   1.327 - "[| P(%a.0); \
   1.328 -\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
   1.329 -\  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
   1.330 -by (induct_tac "n" 1);
   1.331 - by (Asm_simp_tac 1);
   1.332 - by (Clarify_tac 1);
   1.333 - by (subgoal_tac "f = (%a.0)" 1);
   1.334 -  by (Asm_simp_tac 1);
   1.335 -  by (resolve_tac prems 1);
   1.336 - by (rtac ext 1);
   1.337 - by (Force_tac 1);
   1.338 -by (Clarify_tac 1);
   1.339 -by (ftac setsum_SucD 1);
   1.340 -by (Clarify_tac 1);
   1.341 -by (rename_tac "a" 1);
   1.342 -by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
   1.343 - by (etac (rotate_prems 1 finite_subset) 2);
   1.344 - by (Simp_tac 2);
   1.345 - by (Blast_tac 2);
   1.346 -by (subgoal_tac
   1.347 -   "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
   1.348 - by (rtac ext 2);
   1.349 - by (Asm_simp_tac 2);
   1.350 -by (EVERY1[etac ssubst, resolve_tac prems]);
   1.351 - by (Blast_tac 1);
   1.352 -by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
   1.353 - by (Blast_tac 1);
   1.354 -by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
   1.355 -by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
   1.356 - by (Blast_tac 2);
   1.357 -by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
   1.358 - by (Blast_tac 2);
   1.359 -by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
   1.360 -                           addcongs [conj_cong]) 1);
   1.361 -no_qed();
   1.362 -val lemma = result();
   1.363 -
   1.364 -val major::prems = Goal
   1.365 - "[| f : multiset; \
   1.366 -\    P(%a.0); \
   1.367 -\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
   1.368 -by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
   1.369 -by (REPEAT(ares_tac (refl::prems) 1));
   1.370 -qed "Rep_multiset_induct";
   1.371 -
   1.372 -val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
   1.373 - "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
   1.374 -by (rtac (Rep_multiset_inverse RS subst) 1);
   1.375 -by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
   1.376 - by (rtac prem1 1);
   1.377 -by (Clarify_tac 1);
   1.378 -by (subgoal_tac
   1.379 -    "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
   1.380 - by (Simp_tac 2);
   1.381 -by (etac ssubst 1);
   1.382 -by (etac (Abs_multiset_inverse RS subst) 1);
   1.383 -by (etac(simplify (simpset()) prem2)1);
   1.384 -qed "multiset_induct";
   1.385 -
   1.386 -Goal "M : multiset ==> (%x. if P x then M x else 0) : multiset";
   1.387 -by (asm_full_simp_tac (simpset() addsimps [multiset_def]) 1);
   1.388 -by (rtac finite_subset 1);
   1.389 -by Auto_tac; 
   1.390 -qed "MCollect_preserves_multiset";
   1.391 -
   1.392 -Goalw [count_def,MCollect_def]
   1.393 - "count {# x:M. P x #} a = (if P a then count M a else 0)";
   1.394 -by (asm_full_simp_tac (simpset() addsimps [MCollect_preserves_multiset]) 1); 
   1.395 -qed "count_MCollect";
   1.396 -Addsimps [count_MCollect];
   1.397 -
   1.398 -Goalw [set_of_def]
   1.399 - "set_of {# x:M. P x #} = set_of M Int {x. P x}";
   1.400 -by Auto_tac; 
   1.401 -qed "set_of_MCollect";
   1.402 -Addsimps [set_of_MCollect];
   1.403 -
   1.404 -Goal "M = {# x:M. P x #} + {# x:M. ~ P x #}";
   1.405 -by (stac multiset_eq_conv_count_eq 1);
   1.406 -by Auto_tac; 
   1.407 -qed "multiset_partition";
   1.408 -
   1.409 -Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
   1.410 -Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
   1.411 -
   1.412 -Goal
   1.413 - "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
   1.414 -by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
   1.415 -by Auto_tac;
   1.416 -qed "add_eq_conv_ex";
   1.417 -
   1.418 -(** order **)
   1.419 -
   1.420 -Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
   1.421 -by (Simp_tac 1);
   1.422 -qed "not_less_empty";
   1.423 -AddIffs [not_less_empty];
   1.424 -
   1.425 -Goalw [mult1_def]
   1.426 - "(N,M0 + {#a#}) : mult1(r) = \
   1.427 -\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
   1.428 -\  (? K. (!b. b :# K --> (b,a) : r) & N = M0 + K))";
   1.429 -by (rtac iffI 1);
   1.430 - by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
   1.431 - by (Clarify_tac 1);
   1.432 - by (etac disjE 1);
   1.433 -  by (Blast_tac 1);
   1.434 - by (Clarify_tac 1);
   1.435 - by (res_inst_tac [("x","Ka+K")] exI 1);
   1.436 - by (simp_tac (simpset() addsimps union_ac) 1);
   1.437 - by (Blast_tac 1);
   1.438 -by (etac disjE 1);
   1.439 - by (Clarify_tac 1);
   1.440 - by (res_inst_tac [("x","aa")] exI 1);
   1.441 - by (res_inst_tac [("x","M0+{#a#}")] exI 1);
   1.442 - by (res_inst_tac [("x","K")] exI 1);
   1.443 - by (simp_tac (simpset() addsimps union_ac) 1);
   1.444 -by (Blast_tac 1);
   1.445 -qed "less_add_conv";
   1.446 -
   1.447 -Open_locale "MSOrd";
   1.448 -
   1.449 -val W_def = thm "W_def";
   1.450 -
   1.451 -Goalw [W_def]
   1.452 - "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
   1.453 -\    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
   1.454 -\ ==> M0+{#a#} : W";
   1.455 -by (rtac accI 1);
   1.456 -by (rename_tac "N" 1);
   1.457 -by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
   1.458 -by (etac disjE 1);
   1.459 - by (Blast_tac 1);
   1.460 -by (Clarify_tac 1);
   1.461 -by (rotate_tac ~1 1);
   1.462 -by (etac rev_mp 1);
   1.463 -by (induct_thm_tac multiset_induct "K" 1);
   1.464 - by (Asm_simp_tac 1);
   1.465 -by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   1.466 -by (Blast_tac 1);
   1.467 -qed "lemma1";
   1.468 -
   1.469 -Goalw [W_def]
   1.470 - "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
   1.471 -by (etac acc_induct 1);
   1.472 -by (blast_tac (claset() addIs [export lemma1]) 1);
   1.473 -qed "lemma2";
   1.474 -
   1.475 -Goalw [W_def]
   1.476 - "wf(r) ==> !M:W. M+{#a#} : W";
   1.477 -by (eres_inst_tac [("a","a")] wf_induct 1);
   1.478 -by (blast_tac (claset() addIs [export lemma2]) 1);
   1.479 -qed "lemma3";
   1.480 -
   1.481 -Goalw [W_def] "wf(r) ==> M : W";
   1.482 -by (induct_thm_tac multiset_induct "M" 1);
   1.483 - by (rtac accI 1);
   1.484 - by (Asm_full_simp_tac 1);
   1.485 -by (blast_tac (claset() addDs [export lemma3]) 1);
   1.486 -qed "all_accessible";
   1.487 -
   1.488 -Close_locale "MSOrd";
   1.489 -
   1.490 -Goal "wf(r) ==> wf(mult1 r)";
   1.491 -by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
   1.492 -qed "wf_mult1";
   1.493 -
   1.494 -Goalw [mult_def] "wf(r) ==> wf(mult r)";
   1.495 -by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
   1.496 -qed "wf_mult";
   1.497 -
   1.498 -(** Equivalence of mult with the usual (closure-free) def **)
   1.499 -
   1.500 -(* Badly needed: a linear arithmetic tactic for multisets *)
   1.501 -
   1.502 -Goal "a :# J ==> I+J - {#a#} = I + (J-{#a#})";
   1.503 -by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   1.504 -qed "diff_union_single_conv";
   1.505 -
   1.506 -(* One direction *)
   1.507 -Goalw [mult_def,mult1_def,set_of_def]
   1.508 - "trans r ==> \
   1.509 -\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
   1.510 -\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
   1.511 -by (etac converse_trancl_induct 1);
   1.512 - by (Clarify_tac 1);
   1.513 - by (res_inst_tac [("x","M0")] exI 1);
   1.514 - by (Simp_tac 1);
   1.515 -by (Clarify_tac 1);
   1.516 -by (case_tac "a :# K" 1);
   1.517 - by (res_inst_tac [("x","I")] exI 1);
   1.518 - by (Simp_tac 1);
   1.519 - by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
   1.520 - by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   1.521 - by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   1.522 - by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
   1.523 - by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   1.524 - by (Blast_tac 1);
   1.525 -by (subgoal_tac "a :# I" 1);
   1.526 - by (res_inst_tac [("x","I-{#a#}")] exI 1);
   1.527 - by (res_inst_tac [("x","J+{#a#}")] exI 1);
   1.528 - by (res_inst_tac [("x","K + Ka")] exI 1);
   1.529 - by (rtac conjI 1);
   1.530 -  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   1.531 -                             addsplits [nat_diff_split]) 1);
   1.532 - by (rtac conjI 1);
   1.533 -  by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   1.534 -  by (Asm_full_simp_tac 1);
   1.535 -  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   1.536 -                             addsplits [nat_diff_split]) 1);
   1.537 - by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   1.538 - by (Blast_tac 1);
   1.539 -by (subgoal_tac "a :# (M0 +{#a#})" 1);
   1.540 - by (Asm_full_simp_tac 1);
   1.541 -by (Simp_tac 1);
   1.542 -qed "mult_implies_one_step";
   1.543 -
   1.544 -Goal "a :# M ==> M = M - {#a#} + {#a#}";
   1.545 -by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   1.546 -qed "elem_imp_eq_diff_union";
   1.547 -
   1.548 -Goal "size M = Suc n ==> EX a N. M = N + {#a#}";
   1.549 -by (etac (size_eq_Suc_imp_elem RS exE) 1);
   1.550 -by (dtac elem_imp_eq_diff_union 1); 
   1.551 -by Auto_tac; 
   1.552 -qed "size_eq_Suc_imp_eq_union";
   1.553 -
   1.554 -
   1.555 -Goal  "trans r ==> \
   1.556 -\ ALL I J K. \
   1.557 -\  (size J = n & J ~= {#} & \
   1.558 -\   (! k : set_of K. ? j : set_of J. (k,j) : r)) --> (I+K, I+J) : mult r";
   1.559 -by (induct_tac "n" 1);
   1.560 -by Auto_tac; 
   1.561 -by (ftac size_eq_Suc_imp_eq_union 1);
   1.562 -by (Clarify_tac 1); 
   1.563 -ren "J'" 1;
   1.564 -by (Asm_full_simp_tac 1); 
   1.565 -by (etac notE 1); 
   1.566 -by Auto_tac; 
   1.567 -by (case_tac "J' = {#}" 1);
   1.568 - by (asm_full_simp_tac (simpset() addsimps [mult_def]) 1); 
   1.569 - by (rtac r_into_trancl 1); 
   1.570 - by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1);
   1.571 - by (Blast_tac 1); 
   1.572 -(*Now we know J' ~= {#}*)
   1.573 -by (cut_inst_tac [("M","K"),("P", "%x. (x,a):r")] multiset_partition 1);
   1.574 -by (eres_inst_tac [("P", "ALL k : set_of K. ?P k")] rev_mp 1); 
   1.575 -by (etac ssubst 1); 
   1.576 -by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); 
   1.577 -by Auto_tac; 
   1.578 -by (subgoal_tac "((I + {# x : K. (x, a) : r#}) + {# x : K. (x, a) ~: r#}, \
   1.579 -\                 (I + {# x : K. (x, a) : r#}) + J') : mult r" 1);
   1.580 - by (Force_tac 2);
   1.581 -by (full_simp_tac (simpset() addsimps [union_assoc RS sym, mult_def]) 1); 
   1.582 -by (etac trancl_trans 1); 
   1.583 -by (rtac r_into_trancl 1); 
   1.584 -by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); 
   1.585 -by (res_inst_tac [("x", "a")] exI 1); 
   1.586 -by (res_inst_tac [("x", "I + J'")] exI 1); 
   1.587 -by (asm_simp_tac (simpset() addsimps union_ac) 1); 
   1.588 -qed_spec_mp "one_step_implies_mult_lemma";
   1.589 -
   1.590 -Goal  "[| trans r;  J ~= {#};  \
   1.591 -\         ALL k : set_of K. EX j : set_of J. (k,j) : r |] \
   1.592 -\      ==> (I+K, I+J) : mult r";
   1.593 -by (rtac one_step_implies_mult_lemma 1); 
   1.594 -by Auto_tac; 
   1.595 -qed "one_step_implies_mult";
   1.596 -
   1.597 -
   1.598 -(** Proving that multisets are partially ordered **)
   1.599 -
   1.600 -Goalw [trans_def] "trans {(x',x). x' < (x::'a::order)}";
   1.601 -by (blast_tac (claset() addIs [order_less_trans]) 1);
   1.602 -qed "trans_base_order";
   1.603 -
   1.604 -Goal "finite A ==> (ALL x: A. EX y : A. x < (y::'a::order)) --> A={}";
   1.605 -by (etac finite_induct 1);
   1.606 -by Auto_tac;
   1.607 -by (blast_tac (claset() addIs [order_less_trans]) 1);
   1.608 -qed_spec_mp "mult_irrefl_lemma";
   1.609 -
   1.610 -(*irreflexivity*)
   1.611 -Goalw [mult_less_def] "~ M < (M :: ('a::order)multiset)";
   1.612 -by Auto_tac;
   1.613 -by (dtac (trans_base_order RS mult_implies_one_step) 1);
   1.614 -by Auto_tac;
   1.615 -by (dtac (finite_set_of RS mult_irrefl_lemma) 1);
   1.616 -by (asm_full_simp_tac (simpset() addsimps [set_of_eq_empty_iff]) 1);
   1.617 -qed "mult_less_not_refl";
   1.618 -
   1.619 -(* N<N ==> R *)
   1.620 -bind_thm ("mult_less_irrefl", mult_less_not_refl RS notE);
   1.621 -AddSEs [mult_less_irrefl];
   1.622 -
   1.623 -(*transitivity*)
   1.624 -Goalw [mult_less_def, mult_def]
   1.625 -     "[| K < M; M < N |] ==> K < (N :: ('a::order)multiset)";
   1.626 -by (blast_tac (claset() addIs [trancl_trans]) 1);
   1.627 -qed "mult_less_trans";
   1.628 -
   1.629 -(*asymmetry*)
   1.630 -Goal "M < N ==> ~ N < (M :: ('a::order)multiset)";
   1.631 -by Auto_tac;
   1.632 -by (rtac (mult_less_not_refl RS notE) 1);
   1.633 -by (etac mult_less_trans 1);
   1.634 -by (assume_tac 1);
   1.635 -qed "mult_less_not_sym";
   1.636 -
   1.637 -(* [| M<N;  ~P ==> N<M |] ==> P *)
   1.638 -bind_thm ("mult_less_asym", mult_less_not_sym RS contrapos_np);
   1.639 -
   1.640 -Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)";
   1.641 -by Auto_tac;
   1.642 -qed "mult_le_refl";
   1.643 -AddIffs [mult_le_refl];
   1.644 -
   1.645 -(*anti-symmetry*)
   1.646 -Goalw [mult_le_def] "[| M <= N;  N <= M |] ==> M = (N :: ('a::order)multiset)";
   1.647 -by (blast_tac (claset() addDs [mult_less_not_sym]) 1);
   1.648 -qed "mult_le_antisym";
   1.649 -
   1.650 -(*transitivity*)
   1.651 -Goalw [mult_le_def]
   1.652 -     "[| K <= M; M <= N |] ==> K <= (N :: ('a::order)multiset)";
   1.653 -by (blast_tac (claset() addIs [mult_less_trans]) 1);
   1.654 -qed "mult_le_trans";
   1.655 -
   1.656 -Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))";
   1.657 -by Auto_tac;
   1.658 -qed "mult_less_le";
   1.659 -
   1.660 -
   1.661 -(** Monotonicity of multiset union **)
   1.662 -
   1.663 -Goalw [mult1_def]
   1.664 -     "[| (B,D) : mult1 r; trans r |] ==> (C + B, C + D) : mult1 r";
   1.665 -by Auto_tac; 
   1.666 -by (res_inst_tac [("x", "a")] exI 1); 
   1.667 -by (res_inst_tac [("x", "C+M0")] exI 1); 
   1.668 -by (asm_simp_tac (simpset() addsimps [union_assoc]) 1); 
   1.669 -qed "mult1_union";
   1.670 -
   1.671 -Goalw [mult_less_def, mult_def]
   1.672 -     "!!C:: ('a::order) multiset. B<D ==> C+B < C+D";
   1.673 -by (etac trancl_induct 1); 
   1.674 -by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
   1.675 -                               r_into_trancl]) 1); 
   1.676 -by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, 
   1.677 -                               r_into_trancl, trancl_trans]) 1); 
   1.678 -qed "union_less_mono2";
   1.679 -
   1.680 -Goal "!!C:: ('a::order) multiset. B<D ==> B+C < D+C";
   1.681 -by (simp_tac (simpset() addsimps [union_commute]) 1); 
   1.682 -by (etac union_less_mono2 1); 
   1.683 -qed "union_less_mono1";
   1.684 -
   1.685 -Goal "!!C:: ('a::order) multiset. [| A<C; B<D |] ==> A+B < C+D";
   1.686 -by (blast_tac (claset() addIs [union_less_mono1, union_less_mono2,
   1.687 -                               mult_less_trans]) 1); 
   1.688 -qed "union_less_mono";
   1.689 -
   1.690 -Goalw [mult_le_def]
   1.691 -     "!!D:: ('a::order) multiset. [| A<=C;  B<=D |] ==> A+B <= C+D";
   1.692 -by (blast_tac (claset() addIs [union_less_mono, union_less_mono1, 
   1.693 -                               union_less_mono2]) 1); 
   1.694 -qed "union_le_mono";
   1.695 -
   1.696 -
   1.697 -
   1.698 -Goalw [mult_le_def, mult_less_def]
   1.699 -     "{#} <= (M :: ('a::order) multiset)";
   1.700 -by (case_tac "M={#}" 1);
   1.701 -by (subgoal_tac "({#} + {#}, {#} + M) : mult(Collect (split op <))" 2);
   1.702 -by (rtac one_step_implies_mult 3);
   1.703 -bw trans_def;
   1.704 -by Auto_tac; 
   1.705 -by (blast_tac (claset() addIs [order_less_trans]) 1); 
   1.706 -qed "empty_leI";
   1.707 -AddIffs [empty_leI];
   1.708 -
   1.709 -
   1.710 -Goal "!!A:: ('a::order) multiset. A <= A+B";
   1.711 -by (subgoal_tac "A+{#} <= A+B" 1);
   1.712 -by (rtac union_le_mono 2); 
   1.713 -by Auto_tac; 
   1.714 -qed "union_upper1";
   1.715 -
   1.716 -Goal "!!A:: ('a::order) multiset. B <= A+B";
   1.717 -by (stac union_commute 1 THEN rtac union_upper1 1);
   1.718 -qed "union_upper2";