Multisets at last!
authornipkow
Fri Oct 09 11:16:04 1998 +0200 (1998-10-09)
changeset 562815b7f12ad919
parent 5627 ac627075b808
child 5629 9baad17accb9
Multisets at last!
src/HOL/Induct/Multiset.ML
src/HOL/Induct/Multiset.thy
src/HOL/Induct/Multiset0.ML
src/HOL/Induct/Multiset0.thy
src/HOL/Induct/Mutil.ML
src/HOL/Induct/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Oct 09 11:16:04 1998 +0200
     1.3 @@ -0,0 +1,448 @@
     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 +
    1.12 +(** Preservation of representing set `multiset' **)
    1.13 +
    1.14 +Goalw [multiset_def] "(%a. 0) : multiset";
    1.15 +by(Simp_tac 1);
    1.16 +qed "const0_in_multiset";
    1.17 +Addsimps [const0_in_multiset];
    1.18 +
    1.19 +Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
    1.20 +by(Simp_tac 1);
    1.21 +qed "only1_in_multiset";
    1.22 +Addsimps [only1_in_multiset];
    1.23 +
    1.24 +Goalw [multiset_def]
    1.25 + "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
    1.26 +by(Asm_full_simp_tac 1);
    1.27 +bd finite_UnI 1;
    1.28 +ba 1;
    1.29 +by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
    1.30 +qed "union_preserves_multiset";
    1.31 +Addsimps [union_preserves_multiset];
    1.32 +
    1.33 +Goalw [multiset_def]
    1.34 + "[| M : multiset |] ==> (%a. M a - N a) : multiset";
    1.35 +by(Asm_full_simp_tac 1);
    1.36 +be (rotate_prems 1 finite_subset) 1;
    1.37 +by(Auto_tac);
    1.38 +qed "diff_preserves_multiset";
    1.39 +Addsimps [diff_preserves_multiset];
    1.40 +
    1.41 +(** Injectivity of Rep_multiset **)
    1.42 +
    1.43 +Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
    1.44 +br iffI 1;
    1.45 + by(Asm_simp_tac 1);
    1.46 +by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
    1.47 +by(Asm_full_simp_tac 1);
    1.48 +qed "multiset_eq_conv_Rep_eq";
    1.49 +Addsimps [multiset_eq_conv_Rep_eq];
    1.50 +Addsimps [expand_fun_eq];
    1.51 +(*
    1.52 +Goal
    1.53 + "[| f : multiset; g : multiset |] ==> \
    1.54 +\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
    1.55 +br iffI 1;
    1.56 + by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    1.57 + by(Asm_full_simp_tac 1);
    1.58 +by(subgoal_tac "f = g" 1);
    1.59 + by(Asm_simp_tac 1);
    1.60 +br ext 1;
    1.61 +by(Blast_tac 1);
    1.62 +qed "Abs_multiset_eq";
    1.63 +Addsimps [Abs_multiset_eq];
    1.64 +*)
    1.65 +
    1.66 +(** Equations **)
    1.67 +
    1.68 +(* union *)
    1.69 +
    1.70 +Goalw [union_def,empty_def]
    1.71 + "M + {#} = M & {#} + M = M";
    1.72 +by(Simp_tac 1);
    1.73 +qed "union_empty";
    1.74 +Addsimps [union_empty];
    1.75 +
    1.76 +Goalw [union_def]
    1.77 + "(M::'a multiset) + N = N + M";
    1.78 +by(simp_tac (simpset() addsimps add_ac) 1);
    1.79 +qed "union_comm";
    1.80 +
    1.81 +Goalw [union_def]
    1.82 + "((M::'a multiset)+N)+K = M+(N+K)";
    1.83 +by(simp_tac (simpset() addsimps add_ac) 1);
    1.84 +qed "union_assoc";
    1.85 +
    1.86 +qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
    1.87 + (fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1,
    1.88 +           rtac (union_comm RS arg_cong) 1]);
    1.89 +
    1.90 +val union_ac = [union_assoc, union_comm, union_lcomm];
    1.91 +
    1.92 +(* diff *)
    1.93 +
    1.94 +Goalw [empty_def,diff_def]
    1.95 + "M-{#} = M & {#}-M = {#}";
    1.96 +by(Simp_tac 1);
    1.97 +qed "diff_empty";
    1.98 +Addsimps [diff_empty];
    1.99 +
   1.100 +Goalw [union_def,diff_def]
   1.101 + "M+{#a#}-{#a#} = M";
   1.102 +by(Simp_tac 1);
   1.103 +qed "diff_union_inverse2";
   1.104 +Addsimps [diff_union_inverse2];
   1.105 +
   1.106 +(* count *)
   1.107 +
   1.108 +Goalw [count_def,empty_def]
   1.109 + "count {#} a = 0";
   1.110 +by(Simp_tac 1);
   1.111 +qed "count_empty";
   1.112 +Addsimps [count_empty];
   1.113 +
   1.114 +Goalw [count_def,single_def]
   1.115 + "count {#b#} a = (if b=a then 1 else 0)";
   1.116 +by(Simp_tac 1);
   1.117 +qed "count_single";
   1.118 +Addsimps [count_single];
   1.119 +
   1.120 +Goalw [count_def,union_def]
   1.121 + "count (M+N) a = count M a + count N a";
   1.122 +by(Simp_tac 1);
   1.123 +qed "count_union";
   1.124 +Addsimps [count_union];
   1.125 +
   1.126 +(* set_of *)
   1.127 +
   1.128 +Goalw [set_of_def] "set_of {#} = {}";
   1.129 +by(Simp_tac 1);
   1.130 +qed "set_of_empty";
   1.131 +Addsimps [set_of_empty];
   1.132 +
   1.133 +Goalw [set_of_def]
   1.134 + "set_of {#b#} = {b}";
   1.135 +by(Simp_tac 1);
   1.136 +qed "set_of_single";
   1.137 +Addsimps [set_of_single];
   1.138 +
   1.139 +Goalw [set_of_def]
   1.140 + "set_of(M+N) = set_of M Un set_of N";
   1.141 +by(Auto_tac);
   1.142 +qed "set_of_union";
   1.143 +Addsimps [set_of_union];
   1.144 +
   1.145 +(* size *)
   1.146 +
   1.147 +Goalw [size_def] "size {#} = 0";
   1.148 +by(Simp_tac 1);
   1.149 +qed "size_empty";
   1.150 +Addsimps [size_empty];
   1.151 +
   1.152 +Goalw [size_def]
   1.153 + "size {#b#} = 1";
   1.154 +by(Simp_tac 1);
   1.155 +qed "size_single";
   1.156 +Addsimps [size_single];
   1.157 +
   1.158 +(* Some other day...
   1.159 +Goalw [size_def]
   1.160 + "size (M+N::'a multiset) = size M + size N";
   1.161 +*)
   1.162 +
   1.163 +(* equalities *)
   1.164 +
   1.165 +Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
   1.166 +by(Simp_tac 1);
   1.167 +qed "single_not_empty";
   1.168 +Addsimps [single_not_empty];
   1.169 +
   1.170 +Goalw [single_def] "({#a#}={#b#}) = (a=b)";
   1.171 +by(Auto_tac);
   1.172 +qed "single_eq_single";
   1.173 +Addsimps [single_eq_single];
   1.174 +
   1.175 +Goalw [union_def,empty_def]
   1.176 + "(M+N = {#}) = (M = {#} & N = {#})";
   1.177 +by(Simp_tac 1);
   1.178 +by(Blast_tac 1);
   1.179 +qed "union_eq_empty";
   1.180 +AddIffs [union_eq_empty];
   1.181 +
   1.182 +Goalw [union_def,empty_def]
   1.183 + "({#} = M+N) = (M = {#} & N = {#})";
   1.184 +by(Simp_tac 1);
   1.185 +by(Blast_tac 1);
   1.186 +qed "empty_eq_union";
   1.187 +AddIffs [empty_eq_union];
   1.188 +
   1.189 +Goalw [union_def]
   1.190 + "(M+K = N+K) = (M=(N::'a multiset))";
   1.191 +by(Simp_tac 1);
   1.192 +qed "union_right_cancel";
   1.193 +Addsimps [union_right_cancel];
   1.194 +
   1.195 +Goalw [union_def]
   1.196 + "(K+M = K+N) = (M=(N::'a multiset))";
   1.197 +by(Simp_tac 1);
   1.198 +qed "union_left_cancel";
   1.199 +Addsimps [union_left_cancel];
   1.200 +
   1.201 +Goalw [empty_def,single_def,union_def]
   1.202 + "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
   1.203 +by(simp_tac (simpset() addsimps [add_is_1]) 1);
   1.204 +by(Blast_tac 1);
   1.205 +qed "union_is_single";
   1.206 +
   1.207 +Goalw [empty_def,single_def,union_def]
   1.208 + "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
   1.209 +by(simp_tac (simpset() addsimps [one_is_add]) 1);
   1.210 +by(blast_tac (claset() addDs [sym]) 1);
   1.211 +qed "single_is_union";
   1.212 +
   1.213 +Goalw [single_def,union_def,diff_def]
   1.214 + "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
   1.215 +by(Simp_tac 1);
   1.216 +br conjI 1;
   1.217 + by(Force_tac 1);
   1.218 +by(Clarify_tac 1);
   1.219 +br conjI 1;
   1.220 + by(Blast_tac 1);
   1.221 +by(Clarify_tac 1);
   1.222 +br iffI 1;
   1.223 + br conjI 1;
   1.224 + by(Clarify_tac 1);
   1.225 +  br conjI 1;
   1.226 +   by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   1.227 +(* PROOF FAILED:
   1.228 +by(Blast_tac 1);
   1.229 +*)
   1.230 +  by(Fast_tac 1);
   1.231 + by(Asm_simp_tac 1);
   1.232 +by(Force_tac 1);
   1.233 +qed "add_eq_conv_diff";
   1.234 +
   1.235 +(* FIXME
   1.236 +val prems = Goal
   1.237 + "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   1.238 +by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
   1.239 +     measure_induct 1);
   1.240 +by(Clarify_tac 1);
   1.241 +brs prems 1;
   1.242 + ba 1;
   1.243 +by(Clarify_tac 1);
   1.244 +by(subgoal_tac "finite G" 1);
   1.245 + by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   1.246 +be allE 1;
   1.247 +be impE 1;
   1.248 + by(Blast_tac 2);
   1.249 +by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   1.250 +val lemma = result();
   1.251 +
   1.252 +val prems = Goal
   1.253 + "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
   1.254 +br (lemma RS mp) 1;
   1.255 +by (REPEAT(ares_tac prems 1));
   1.256 +qed "finite_psubset_induct";
   1.257 +
   1.258 +Better: use wf_finite_psubset in WF_Rel
   1.259 +*)
   1.260 +
   1.261 +(** Towards the induction rule **)
   1.262 +
   1.263 +Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
   1.264 +be finite_induct 1;
   1.265 +by(Auto_tac);
   1.266 +qed "setsum_0";
   1.267 +Addsimps [setsum_0];
   1.268 +
   1.269 +Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
   1.270 +be finite_induct 1;
   1.271 +by(Auto_tac);
   1.272 +by(asm_full_simp_tac
   1.273 +    (simpset() delsimps [setsum_0] addsimps [setsum_0 RS sym]) 1);
   1.274 +val lemma = result();
   1.275 +
   1.276 +Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
   1.277 +bd lemma 1;
   1.278 +by(Fast_tac 1);
   1.279 +qed "setsum_SucD";
   1.280 +
   1.281 +Goal "[| finite F; 0 < f a |] ==> \
   1.282 +\     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
   1.283 +be finite_induct 1;
   1.284 +by(Auto_tac);
   1.285 + by(asm_simp_tac (simpset() addsimps add_ac) 1);
   1.286 +by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   1.287 +by(Auto_tac);
   1.288 +qed "setsum_decr";
   1.289 +
   1.290 +val prems = Goalw [multiset_def]
   1.291 + "[| P(%a.0); \
   1.292 +\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
   1.293 +\  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
   1.294 +by(induct_tac "n" 1);
   1.295 + by(Asm_simp_tac 1);
   1.296 + by(Clarify_tac 1);
   1.297 + by(subgoal_tac "f = (%a.0)" 1);
   1.298 +  by(Asm_simp_tac 1);
   1.299 +  brs prems 1;
   1.300 + br ext 1;
   1.301 + by(Force_tac 1);
   1.302 +by(Clarify_tac 1);
   1.303 +by(forward_tac [setsum_SucD] 1);
   1.304 + ba 1;
   1.305 +by(Clarify_tac 1);
   1.306 +by(rename_tac "a" 1);
   1.307 +by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
   1.308 + be (rotate_prems 1 finite_subset) 2;
   1.309 + by(Simp_tac 2);
   1.310 + by(Blast_tac 2);
   1.311 +by(subgoal_tac
   1.312 +   "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
   1.313 + br ext 2;
   1.314 + by(Asm_simp_tac 2);
   1.315 +by(EVERY1[etac ssubst, resolve_tac prems]);
   1.316 + by(Blast_tac 1);
   1.317 +by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
   1.318 + by(Blast_tac 1);
   1.319 +by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
   1.320 +by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
   1.321 + by(Blast_tac 2);
   1.322 +by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
   1.323 + by(Blast_tac 2);
   1.324 +by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
   1.325 +                           addcongs [conj_cong]
   1.326 +                           addSolver cut_trans_tac) 1);
   1.327 +val lemma = result();
   1.328 +
   1.329 +val major::prems = Goal
   1.330 + "[| f : multiset; \
   1.331 +\    P(%a.0); \
   1.332 +\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
   1.333 +by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
   1.334 +by(REPEAT(ares_tac (refl::prems) 1));
   1.335 +qed "Rep_multiset_induct";
   1.336 +
   1.337 +val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
   1.338 + "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
   1.339 +by (rtac (Rep_multiset_inverse RS subst) 1);
   1.340 +by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
   1.341 + by(rtac prem1 1);
   1.342 +by(Clarify_tac 1);
   1.343 +by(subgoal_tac
   1.344 +    "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
   1.345 + by(Simp_tac 2);
   1.346 +be ssubst 1;
   1.347 +by(etac (Abs_multiset_inverse RS subst) 1);
   1.348 +by(etac(simplify (simpset()) prem2)1);
   1.349 +qed "multiset_induct";
   1.350 +
   1.351 +Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
   1.352 +Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
   1.353 +
   1.354 +Goal
   1.355 + "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
   1.356 +by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
   1.357 +by(Auto_tac);
   1.358 +qed "add_eq_conv_ex";
   1.359 +
   1.360 +(** order **)
   1.361 +
   1.362 +Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
   1.363 +by(Simp_tac 1);
   1.364 +qed "not_less_empty";
   1.365 +AddIffs [not_less_empty];
   1.366 +
   1.367 +Goalw [mult1_def]
   1.368 + "(N,M0 + {#a#}) : mult1(r) = \
   1.369 +\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
   1.370 +\  (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
   1.371 +br iffI 1;
   1.372 + by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
   1.373 + by(Clarify_tac 1);
   1.374 + be disjE 1;
   1.375 +  by(Blast_tac 1);
   1.376 + by(Clarify_tac 1);
   1.377 + by(res_inst_tac [("x","Ka+K")] exI 1);
   1.378 + by(simp_tac (simpset() addsimps union_ac) 1);
   1.379 + by(Blast_tac 1);
   1.380 +be disjE 1;
   1.381 + by(Clarify_tac 1);
   1.382 + by(res_inst_tac [("x","aa")] exI 1);
   1.383 + by(res_inst_tac [("x","M0+{#a#}")] exI 1);
   1.384 + by(res_inst_tac [("x","K")] exI 1);
   1.385 + by(simp_tac (simpset() addsimps union_ac) 1);
   1.386 +by(Blast_tac 1);
   1.387 +qed "less_add_conv";
   1.388 +
   1.389 +Open_locale "MSOrd";
   1.390 +
   1.391 +val W_def = thm "W_def";
   1.392 +
   1.393 +Goalw [W_def]
   1.394 + "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
   1.395 +\    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
   1.396 +\ ==> M0+{#a#} : W";
   1.397 +br accI 1;
   1.398 +by(rename_tac "N" 1);
   1.399 +by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
   1.400 +be disjE 1;
   1.401 + by(Blast_tac 1);
   1.402 +by(Clarify_tac 1);
   1.403 +by(rotate_tac ~1 1);
   1.404 +be rev_mp 1;
   1.405 +by(res_inst_tac [("M","K")] multiset_induct 1);
   1.406 + by(Asm_simp_tac 1);
   1.407 +by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   1.408 +by(Blast_tac 1);
   1.409 +qed "lemma1";
   1.410 +
   1.411 +Goalw [W_def]
   1.412 + "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
   1.413 +be acc_induct 1;
   1.414 +by(blast_tac (claset() addIs [export lemma1]) 1);
   1.415 +qed "lemma2";
   1.416 +
   1.417 +Goalw [W_def]
   1.418 + "wf(r) ==> !M:W. M+{#a#} : W";
   1.419 +by(eres_inst_tac [("a","a")] wf_induct 1);
   1.420 +by(blast_tac (claset() addIs [export lemma2]) 1);
   1.421 +qed "lemma3";
   1.422 +
   1.423 +Goalw [W_def] "wf(r) ==> M : W";
   1.424 +by(res_inst_tac [("M","M")] multiset_induct 1);
   1.425 + br accI 1;
   1.426 + by(Asm_full_simp_tac 1);
   1.427 +by(blast_tac (claset() addDs [export lemma3]) 1);
   1.428 +qed "all_accessible";
   1.429 +
   1.430 +Close_locale();
   1.431 +
   1.432 +Goal "wf(r) ==> wf(mult1 r)";
   1.433 +by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
   1.434 +qed "wf_mult1";
   1.435 +
   1.436 +Goalw [mult_def] "wf(r) ==> wf(mult r)";
   1.437 +by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
   1.438 +qed "wf_mult";
   1.439 +
   1.440 +Goalw [mult_def,set_of_def]
   1.441 + "(M,N) : mult r = (? I J K. N = I+J & M = I+K & \
   1.442 +\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
   1.443 +br iffI 1;
   1.444 +
   1.445 +be trancl_induct 1;
   1.446 +by(asm_full_simp_tac (simpset() addsimps [mult1_def]) 1);
   1.447 +
   1.448 +by(Clarify_tac 1);
   1.449 +by(res_inst_tac [("x","M0")] exI 1);
   1.450 +by(Simp_tac 1);
   1.451 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Induct/Multiset.thy	Fri Oct 09 11:16:04 1998 +0200
     2.3 @@ -0,0 +1,56 @@
     2.4 +(*  Title:      HOL/Induct/Multiset.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1998 TUM
     2.8 +
     2.9 +A definitional theory of multisets,
    2.10 +including a wellfoundedness proof for the multiset order.
    2.11 +use_thy"Multiset";
    2.12 +
    2.13 +*)
    2.14 +
    2.15 +Multiset = Multiset0 + Acc +
    2.16 +
    2.17 +typedef
    2.18 +  'a multiset = "{f :: 'a => nat . finite{x . 0 < f x}}" (multiset_witness)
    2.19 +
    2.20 +instance multiset :: (term){ord,plus,minus}
    2.21 +
    2.22 +consts
    2.23 +  "{#}"  :: 'a multiset                        ("{#}")
    2.24 +  single :: 'a                => 'a multiset   ("{#_#}")
    2.25 +  count  :: ['a multiset, 'a] => nat
    2.26 +  set_of :: 'a multiset => 'a set
    2.27 +
    2.28 +syntax
    2.29 +  elem   :: ['a multiset, 'a] => bool
    2.30 +translations
    2.31 +  "elem M a" == "0 < count M a"
    2.32 +
    2.33 +defs
    2.34 +  count_def  "count == Rep_multiset"
    2.35 +  empty_def  "{#}   == Abs_multiset(%a. 0)"
    2.36 +  single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)"
    2.37 +  union_def  "M+N   == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)"
    2.38 +  diff_def  "M-N    == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)"
    2.39 +  set_of_def "set_of M == {x. elem M x}"
    2.40 +  size_def "size (M) == setsum (count M) (set_of M)"
    2.41 +
    2.42 +constdefs
    2.43 +  mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set"
    2.44 + "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K &
    2.45 +                                 (!b. elem K b --> (b,a) : r)}"
    2.46 +
    2.47 +  mult :: "('a * 'a)set => ('a multiset * 'a multiset)set"
    2.48 + "mult(r) == (mult1 r)^+"
    2.49 +
    2.50 +locale MSOrd =
    2.51 +  fixes
    2.52 +    r :: "('a * 'a)set"
    2.53 +    W :: "'a multiset set"
    2.54 +
    2.55 +  assumes
    2.56 +
    2.57 +  defines
    2.58 +    W_def       "W == acc(mult1 r)"
    2.59 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Induct/Multiset0.ML	Fri Oct 09 11:16:04 1998 +0200
     3.3 @@ -0,0 +1,11 @@
     3.4 +(*  Title:      HOL/Induct/Multiset0.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow
     3.7 +    Copyright   1998 TUM
     3.8 +
     3.9 +This theory merely proves that the representation of multisets is nonempty.
    3.10 +*)
    3.11 +
    3.12 +Goal "(%x.0) : {f. finite {x. 0 < f x}}";
    3.13 +by(Simp_tac 1);
    3.14 +qed "multiset_witness";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Induct/Multiset0.thy	Fri Oct 09 11:16:04 1998 +0200
     4.3 @@ -0,0 +1,9 @@
     4.4 +(*  Title:      HOL/Induct/Multiset0.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow
     4.7 +    Copyright   1998 TUM
     4.8 +
     4.9 +This theory merely proves that the representation of multisets is nonempty.
    4.10 +*)
    4.11 +
    4.12 +Multiset0 = Main
     5.1 --- a/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:15:39 1998 +0200
     5.2 +++ b/src/HOL/Induct/Mutil.ML	Fri Oct 09 11:16:04 1998 +0200
     5.3 @@ -152,7 +152,7 @@
     5.4  (*Cardinality is smaller because of the two elements fewer*)
     5.5  by (rtac less_trans 1);
     5.6  by (REPEAT
     5.7 -    (rtac card_Diff 1 
     5.8 +    (rtac card_Diff1_less 1 
     5.9       THEN asm_simp_tac (simpset() addsimps [tiling_domino_finite]) 1 
    5.10       THEN asm_simp_tac (simpset() addsimps [mod_less, evnodd_iff]) 1));
    5.11  qed "mutil_not_tiling";
     6.1 --- a/src/HOL/Induct/ROOT.ML	Fri Oct 09 11:15:39 1998 +0200
     6.2 +++ b/src/HOL/Induct/ROOT.ML	Fri Oct 09 11:16:04 1998 +0200
     6.3 @@ -14,6 +14,7 @@
     6.4  time_use_thy "Comb";
     6.5  time_use_thy "Mutil";
     6.6  time_use_thy "Acc";
     6.7 +time_use_thy "Multiset";
     6.8  time_use_thy "PropLog";
     6.9  time_use_thy "SList";
    6.10  time_use_thy "LFilter";