author | paulson |
Tue, 17 Oct 2000 10:21:12 +0200 | |
changeset 10231 | 178a272bceeb |
parent 9747 | 043098ba5098 |
permissions | -rw-r--r-- |
5628 | 1 |
(* Title: HOL/Induct/Multiset.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
*) |
|
6 |
||
8952 | 7 |
Addsimps [Abs_multiset_inverse, Rep_multiset_inverse, Rep_multiset, |
8 |
Zero_def]; |
|
5628 | 9 |
|
10 |
(** Preservation of representing set `multiset' **) |
|
11 |
||
12 |
Goalw [multiset_def] "(%a. 0) : multiset"; |
|
6162 | 13 |
by (Simp_tac 1); |
5628 | 14 |
qed "const0_in_multiset"; |
15 |
Addsimps [const0_in_multiset]; |
|
16 |
||
17 |
Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset"; |
|
6162 | 18 |
by (Simp_tac 1); |
5628 | 19 |
qed "only1_in_multiset"; |
20 |
Addsimps [only1_in_multiset]; |
|
21 |
||
22 |
Goalw [multiset_def] |
|
23 |
"[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset"; |
|
6162 | 24 |
by (Asm_full_simp_tac 1); |
25 |
by (dtac finite_UnI 1); |
|
26 |
by (assume_tac 1); |
|
27 |
by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1); |
|
5628 | 28 |
qed "union_preserves_multiset"; |
29 |
Addsimps [union_preserves_multiset]; |
|
30 |
||
31 |
Goalw [multiset_def] |
|
32 |
"[| M : multiset |] ==> (%a. M a - N a) : multiset"; |
|
6162 | 33 |
by (Asm_full_simp_tac 1); |
34 |
by (etac (rotate_prems 1 finite_subset) 1); |
|
8952 | 35 |
by Auto_tac; |
5628 | 36 |
qed "diff_preserves_multiset"; |
37 |
Addsimps [diff_preserves_multiset]; |
|
38 |
||
39 |
(** Injectivity of Rep_multiset **) |
|
40 |
||
41 |
Goal "(M = N) = (Rep_multiset M = Rep_multiset N)"; |
|
6162 | 42 |
by (rtac iffI 1); |
43 |
by (Asm_simp_tac 1); |
|
44 |
by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1); |
|
45 |
by (Asm_full_simp_tac 1); |
|
5628 | 46 |
qed "multiset_eq_conv_Rep_eq"; |
47 |
Addsimps [multiset_eq_conv_Rep_eq]; |
|
48 |
Addsimps [expand_fun_eq]; |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
49 |
|
5628 | 50 |
(* |
51 |
Goal |
|
52 |
"[| f : multiset; g : multiset |] ==> \ |
|
53 |
\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)"; |
|
6162 | 54 |
by (rtac iffI 1); |
55 |
by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1); |
|
56 |
by (Asm_full_simp_tac 1); |
|
57 |
by (subgoal_tac "f = g" 1); |
|
58 |
by (Asm_simp_tac 1); |
|
59 |
by (rtac ext 1); |
|
60 |
by (Blast_tac 1); |
|
5628 | 61 |
qed "Abs_multiset_eq"; |
62 |
Addsimps [Abs_multiset_eq]; |
|
63 |
*) |
|
64 |
||
65 |
(** Equations **) |
|
66 |
||
67 |
(* union *) |
|
68 |
||
69 |
Goalw [union_def,empty_def] |
|
70 |
"M + {#} = M & {#} + M = M"; |
|
6162 | 71 |
by (Simp_tac 1); |
5628 | 72 |
qed "union_empty"; |
73 |
Addsimps [union_empty]; |
|
74 |
||
75 |
Goalw [union_def] |
|
76 |
"(M::'a multiset) + N = N + M"; |
|
6162 | 77 |
by (simp_tac (simpset() addsimps add_ac) 1); |
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
78 |
qed "union_commute"; |
5628 | 79 |
|
80 |
Goalw [union_def] |
|
81 |
"((M::'a multiset)+N)+K = M+(N+K)"; |
|
6162 | 82 |
by (simp_tac (simpset() addsimps add_ac) 1); |
5628 | 83 |
qed "union_assoc"; |
84 |
||
9266 | 85 |
Goal "M+(N+K) = N+((M+K)::'a multiset)"; |
86 |
by (rtac (union_commute RS trans) 1); |
|
87 |
by (rtac (union_assoc RS trans) 1); |
|
88 |
by (rtac (union_commute RS arg_cong) 1); |
|
89 |
qed "union_lcomm"; |
|
5628 | 90 |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
91 |
bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]); |
5628 | 92 |
|
93 |
(* diff *) |
|
94 |
||
95 |
Goalw [empty_def,diff_def] |
|
96 |
"M-{#} = M & {#}-M = {#}"; |
|
6162 | 97 |
by (Simp_tac 1); |
5628 | 98 |
qed "diff_empty"; |
99 |
Addsimps [diff_empty]; |
|
100 |
||
101 |
Goalw [union_def,diff_def] |
|
102 |
"M+{#a#}-{#a#} = M"; |
|
6162 | 103 |
by (Simp_tac 1); |
5628 | 104 |
qed "diff_union_inverse2"; |
105 |
Addsimps [diff_union_inverse2]; |
|
106 |
||
107 |
(* count *) |
|
108 |
||
109 |
Goalw [count_def,empty_def] |
|
110 |
"count {#} a = 0"; |
|
6162 | 111 |
by (Simp_tac 1); |
5628 | 112 |
qed "count_empty"; |
113 |
Addsimps [count_empty]; |
|
114 |
||
115 |
Goalw [count_def,single_def] |
|
116 |
"count {#b#} a = (if b=a then 1 else 0)"; |
|
6162 | 117 |
by (Simp_tac 1); |
5628 | 118 |
qed "count_single"; |
119 |
Addsimps [count_single]; |
|
120 |
||
121 |
Goalw [count_def,union_def] |
|
122 |
"count (M+N) a = count M a + count N a"; |
|
6162 | 123 |
by (Simp_tac 1); |
5628 | 124 |
qed "count_union"; |
125 |
Addsimps [count_union]; |
|
126 |
||
5772 | 127 |
Goalw [count_def,diff_def] |
128 |
"count (M-N) a = count M a - count N a"; |
|
6162 | 129 |
by (Simp_tac 1); |
5772 | 130 |
qed "count_diff"; |
131 |
Addsimps [count_diff]; |
|
132 |
||
5628 | 133 |
(* set_of *) |
134 |
||
135 |
Goalw [set_of_def] "set_of {#} = {}"; |
|
6162 | 136 |
by (Simp_tac 1); |
5628 | 137 |
qed "set_of_empty"; |
138 |
Addsimps [set_of_empty]; |
|
139 |
||
140 |
Goalw [set_of_def] |
|
141 |
"set_of {#b#} = {b}"; |
|
6162 | 142 |
by (Simp_tac 1); |
5628 | 143 |
qed "set_of_single"; |
144 |
Addsimps [set_of_single]; |
|
145 |
||
146 |
Goalw [set_of_def] |
|
147 |
"set_of(M+N) = set_of M Un set_of N"; |
|
8952 | 148 |
by Auto_tac; |
5628 | 149 |
qed "set_of_union"; |
150 |
Addsimps [set_of_union]; |
|
151 |
||
8914 | 152 |
Goalw [set_of_def, empty_def, count_def] "(set_of M = {}) = (M = {#})"; |
153 |
by Auto_tac; |
|
154 |
qed "set_of_eq_empty_iff"; |
|
155 |
||
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
156 |
Goalw [set_of_def] "(x : set_of M) = (x :# M)"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
157 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
158 |
qed "mem_set_of_iff"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
159 |
|
5628 | 160 |
(* size *) |
161 |
||
162 |
Goalw [size_def] "size {#} = 0"; |
|
6162 | 163 |
by (Simp_tac 1); |
5628 | 164 |
qed "size_empty"; |
165 |
Addsimps [size_empty]; |
|
166 |
||
8914 | 167 |
Goalw [size_def] "size {#b#} = 1"; |
6162 | 168 |
by (Simp_tac 1); |
5628 | 169 |
qed "size_single"; |
170 |
Addsimps [size_single]; |
|
171 |
||
8914 | 172 |
Goal "finite (set_of M)"; |
173 |
by (cut_inst_tac [("x", "M")] Rep_multiset 1); |
|
174 |
by (asm_full_simp_tac |
|
175 |
(simpset() addsimps [multiset_def, set_of_def, count_def]) 1); |
|
176 |
qed "finite_set_of"; |
|
177 |
AddIffs [finite_set_of]; |
|
178 |
||
179 |
Goal "finite A ==> setsum (count N) (A Int set_of N) = setsum (count N) A"; |
|
180 |
by (etac finite_induct 1); |
|
181 |
by (Simp_tac 1); |
|
182 |
by (asm_full_simp_tac (simpset() addsimps [Int_insert_left, set_of_def]) 1); |
|
183 |
qed "setsum_count_Int"; |
|
184 |
||
185 |
Goalw [size_def] "size (M+N::'a multiset) = size M + size N"; |
|
186 |
by (subgoal_tac "count (M+N) = (%a. count M a + count N a)" 1); |
|
187 |
by (rtac ext 2); |
|
188 |
by (Simp_tac 2); |
|
189 |
by (asm_simp_tac |
|
190 |
(simpset() addsimps [setsum_Un, setsum_addf, setsum_count_Int]) 1); |
|
191 |
by (stac Int_commute 1); |
|
192 |
by (asm_simp_tac (simpset() addsimps [setsum_count_Int]) 1); |
|
193 |
qed "size_union"; |
|
194 |
Addsimps [size_union]; |
|
195 |
||
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
196 |
Goalw [size_def, empty_def, count_def] "(size M = 0) = (M = {#})"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
197 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
198 |
by (asm_full_simp_tac (simpset() addsimps [set_of_def, count_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
199 |
qed "size_eq_0_iff_empty"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
200 |
AddIffs [size_eq_0_iff_empty]; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
201 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
202 |
Goalw [size_def] "size M = Suc n ==> EX a. a :# M"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
203 |
by (dtac setsum_SucD 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
204 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
205 |
qed "size_eq_Suc_imp_elem"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
206 |
|
5628 | 207 |
|
208 |
(* equalities *) |
|
209 |
||
5772 | 210 |
Goalw [count_def] "(M = N) = (!a. count M a = count N a)"; |
6162 | 211 |
by (Simp_tac 1); |
5772 | 212 |
qed "multiset_eq_conv_count_eq"; |
213 |
||
5628 | 214 |
Goalw [single_def,empty_def] "{#a#} ~= {#} & {#} ~= {#a#}"; |
6162 | 215 |
by (Simp_tac 1); |
5628 | 216 |
qed "single_not_empty"; |
217 |
Addsimps [single_not_empty]; |
|
218 |
||
219 |
Goalw [single_def] "({#a#}={#b#}) = (a=b)"; |
|
8952 | 220 |
by Auto_tac; |
5628 | 221 |
qed "single_eq_single"; |
222 |
Addsimps [single_eq_single]; |
|
223 |
||
224 |
Goalw [union_def,empty_def] |
|
225 |
"(M+N = {#}) = (M = {#} & N = {#})"; |
|
6162 | 226 |
by (Simp_tac 1); |
227 |
by (Blast_tac 1); |
|
5628 | 228 |
qed "union_eq_empty"; |
229 |
AddIffs [union_eq_empty]; |
|
230 |
||
231 |
Goalw [union_def,empty_def] |
|
232 |
"({#} = M+N) = (M = {#} & N = {#})"; |
|
6162 | 233 |
by (Simp_tac 1); |
234 |
by (Blast_tac 1); |
|
5628 | 235 |
qed "empty_eq_union"; |
236 |
AddIffs [empty_eq_union]; |
|
237 |
||
238 |
Goalw [union_def] |
|
239 |
"(M+K = N+K) = (M=(N::'a multiset))"; |
|
6162 | 240 |
by (Simp_tac 1); |
5628 | 241 |
qed "union_right_cancel"; |
242 |
Addsimps [union_right_cancel]; |
|
243 |
||
244 |
Goalw [union_def] |
|
245 |
"(K+M = K+N) = (M=(N::'a multiset))"; |
|
6162 | 246 |
by (Simp_tac 1); |
5628 | 247 |
qed "union_left_cancel"; |
248 |
Addsimps [union_left_cancel]; |
|
249 |
||
250 |
Goalw [empty_def,single_def,union_def] |
|
251 |
"(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})"; |
|
6162 | 252 |
by (simp_tac (simpset() addsimps [add_is_1]) 1); |
253 |
by (Blast_tac 1); |
|
5628 | 254 |
qed "union_is_single"; |
255 |
||
256 |
Goalw [empty_def,single_def,union_def] |
|
257 |
"({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)"; |
|
6162 | 258 |
by (simp_tac (simpset() addsimps [one_is_add]) 1); |
259 |
by (blast_tac (claset() addDs [sym]) 1); |
|
5628 | 260 |
qed "single_is_union"; |
261 |
||
262 |
Goalw [single_def,union_def,diff_def] |
|
263 |
"(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})"; |
|
6162 | 264 |
by (Simp_tac 1); |
265 |
by (rtac conjI 1); |
|
266 |
by (Force_tac 1); |
|
267 |
by (Clarify_tac 1); |
|
268 |
by (rtac conjI 1); |
|
269 |
by (Blast_tac 1); |
|
270 |
by (Clarify_tac 1); |
|
271 |
by (rtac iffI 1); |
|
272 |
by (rtac conjI 1); |
|
273 |
by (Clarify_tac 1); |
|
274 |
by (rtac conjI 1); |
|
275 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
5628 | 276 |
(* PROOF FAILED: |
6162 | 277 |
by (Blast_tac 1); |
5628 | 278 |
*) |
6162 | 279 |
by (Fast_tac 1); |
280 |
by (Asm_simp_tac 1); |
|
281 |
by (Force_tac 1); |
|
5628 | 282 |
qed "add_eq_conv_diff"; |
283 |
||
284 |
(* FIXME |
|
285 |
val prems = Goal |
|
286 |
"[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F"; |
|
6162 | 287 |
by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")] |
5628 | 288 |
measure_induct 1); |
6162 | 289 |
by (Clarify_tac 1); |
290 |
by (resolve_tac prems 1); |
|
291 |
by (assume_tac 1); |
|
292 |
by (Clarify_tac 1); |
|
293 |
by (subgoal_tac "finite G" 1); |
|
294 |
by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); |
|
295 |
by (etac allE 1); |
|
296 |
by (etac impE 1); |
|
297 |
by (Blast_tac 2); |
|
298 |
by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); |
|
7454 | 299 |
no_qed(); |
5628 | 300 |
val lemma = result(); |
301 |
||
302 |
val prems = Goal |
|
303 |
"[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F"; |
|
6162 | 304 |
by (rtac (lemma RS mp) 1); |
5628 | 305 |
by (REPEAT(ares_tac prems 1)); |
306 |
qed "finite_psubset_induct"; |
|
307 |
||
308 |
Better: use wf_finite_psubset in WF_Rel |
|
309 |
*) |
|
310 |
||
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
311 |
|
5628 | 312 |
(** Towards the induction rule **) |
313 |
||
314 |
Goal "[| finite F; 0 < f a |] ==> \ |
|
315 |
\ setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)"; |
|
6162 | 316 |
by (etac finite_induct 1); |
8952 | 317 |
by Auto_tac; |
6162 | 318 |
by (asm_simp_tac (simpset() addsimps add_ac) 1); |
319 |
by (dres_inst_tac [("a","a")] mk_disjoint_insert 1); |
|
8952 | 320 |
by Auto_tac; |
5628 | 321 |
qed "setsum_decr"; |
322 |
||
323 |
val prems = Goalw [multiset_def] |
|
324 |
"[| P(%a.0); \ |
|
325 |
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \ |
|
326 |
\ ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)"; |
|
6162 | 327 |
by (induct_tac "n" 1); |
328 |
by (Asm_simp_tac 1); |
|
329 |
by (Clarify_tac 1); |
|
330 |
by (subgoal_tac "f = (%a.0)" 1); |
|
331 |
by (Asm_simp_tac 1); |
|
332 |
by (resolve_tac prems 1); |
|
333 |
by (rtac ext 1); |
|
334 |
by (Force_tac 1); |
|
335 |
by (Clarify_tac 1); |
|
7499 | 336 |
by (ftac setsum_SucD 1); |
6162 | 337 |
by (Clarify_tac 1); |
338 |
by (rename_tac "a" 1); |
|
339 |
by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1); |
|
340 |
by (etac (rotate_prems 1 finite_subset) 2); |
|
341 |
by (Simp_tac 2); |
|
342 |
by (Blast_tac 2); |
|
343 |
by (subgoal_tac |
|
5628 | 344 |
"f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1); |
6162 | 345 |
by (rtac ext 2); |
346 |
by (Asm_simp_tac 2); |
|
347 |
by (EVERY1[etac ssubst, resolve_tac prems]); |
|
348 |
by (Blast_tac 1); |
|
349 |
by (EVERY[etac allE 1, etac impE 1, etac mp 2]); |
|
350 |
by (Blast_tac 1); |
|
351 |
by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1); |
|
352 |
by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1); |
|
353 |
by (Blast_tac 2); |
|
354 |
by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1); |
|
355 |
by (Blast_tac 2); |
|
356 |
by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1] |
|
5983 | 357 |
addcongs [conj_cong]) 1); |
7454 | 358 |
no_qed(); |
5628 | 359 |
val lemma = result(); |
360 |
||
361 |
val major::prems = Goal |
|
362 |
"[| f : multiset; \ |
|
363 |
\ P(%a.0); \ |
|
364 |
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)"; |
|
6162 | 365 |
by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1); |
366 |
by (REPEAT(ares_tac (refl::prems) 1)); |
|
5628 | 367 |
qed "Rep_multiset_induct"; |
368 |
||
369 |
val [prem1,prem2] = Goalw [union_def,single_def,empty_def] |
|
370 |
"[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)"; |
|
371 |
by (rtac (Rep_multiset_inverse RS subst) 1); |
|
372 |
by (rtac (Rep_multiset RS Rep_multiset_induct) 1); |
|
6162 | 373 |
by (rtac prem1 1); |
374 |
by (Clarify_tac 1); |
|
375 |
by (subgoal_tac |
|
5628 | 376 |
"f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1); |
6162 | 377 |
by (Simp_tac 2); |
378 |
by (etac ssubst 1); |
|
379 |
by (etac (Abs_multiset_inverse RS subst) 1); |
|
380 |
by (etac(simplify (simpset()) prem2)1); |
|
5628 | 381 |
qed "multiset_induct"; |
382 |
||
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
383 |
Goal "M : multiset ==> (%x. if P x then M x else 0) : multiset"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
384 |
by (asm_full_simp_tac (simpset() addsimps [multiset_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
385 |
by (rtac finite_subset 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
386 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
387 |
qed "MCollect_preserves_multiset"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
388 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
389 |
Goalw [count_def,MCollect_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
390 |
"count {# x:M. P x #} a = (if P a then count M a else 0)"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
391 |
by (asm_full_simp_tac (simpset() addsimps [MCollect_preserves_multiset]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
392 |
qed "count_MCollect"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
393 |
Addsimps [count_MCollect]; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
394 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
395 |
Goalw [set_of_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
396 |
"set_of {# x:M. P x #} = set_of M Int {x. P x}"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
397 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
398 |
qed "set_of_MCollect"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
399 |
Addsimps [set_of_MCollect]; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
400 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
401 |
Goal "M = {# x:M. P x #} + {# x:M. ~ P x #}"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
402 |
by (stac multiset_eq_conv_count_eq 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
403 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
404 |
qed "multiset_partition"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
405 |
|
5628 | 406 |
Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq]; |
407 |
Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset]; |
|
408 |
||
409 |
Goal |
|
410 |
"(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))"; |
|
6162 | 411 |
by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1); |
8952 | 412 |
by Auto_tac; |
5628 | 413 |
qed "add_eq_conv_ex"; |
414 |
||
415 |
(** order **) |
|
416 |
||
417 |
Goalw [mult1_def] "(M, {#}) ~: mult1(r)"; |
|
6162 | 418 |
by (Simp_tac 1); |
5628 | 419 |
qed "not_less_empty"; |
420 |
AddIffs [not_less_empty]; |
|
421 |
||
422 |
Goalw [mult1_def] |
|
423 |
"(N,M0 + {#a#}) : mult1(r) = \ |
|
424 |
\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \ |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
425 |
\ (? K. (!b. b :# K --> (b,a) : r) & N = M0 + K))"; |
6162 | 426 |
by (rtac iffI 1); |
427 |
by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1); |
|
428 |
by (Clarify_tac 1); |
|
429 |
by (etac disjE 1); |
|
430 |
by (Blast_tac 1); |
|
431 |
by (Clarify_tac 1); |
|
432 |
by (res_inst_tac [("x","Ka+K")] exI 1); |
|
433 |
by (simp_tac (simpset() addsimps union_ac) 1); |
|
434 |
by (Blast_tac 1); |
|
435 |
by (etac disjE 1); |
|
436 |
by (Clarify_tac 1); |
|
437 |
by (res_inst_tac [("x","aa")] exI 1); |
|
438 |
by (res_inst_tac [("x","M0+{#a#}")] exI 1); |
|
439 |
by (res_inst_tac [("x","K")] exI 1); |
|
440 |
by (simp_tac (simpset() addsimps union_ac) 1); |
|
441 |
by (Blast_tac 1); |
|
5628 | 442 |
qed "less_add_conv"; |
443 |
||
444 |
Open_locale "MSOrd"; |
|
445 |
||
446 |
val W_def = thm "W_def"; |
|
447 |
||
448 |
Goalw [W_def] |
|
449 |
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \ |
|
450 |
\ !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \ |
|
451 |
\ ==> M0+{#a#} : W"; |
|
6162 | 452 |
by (rtac accI 1); |
453 |
by (rename_tac "N" 1); |
|
454 |
by (full_simp_tac (simpset() addsimps [less_add_conv]) 1); |
|
455 |
by (etac disjE 1); |
|
456 |
by (Blast_tac 1); |
|
457 |
by (Clarify_tac 1); |
|
458 |
by (rotate_tac ~1 1); |
|
459 |
by (etac rev_mp 1); |
|
9747 | 460 |
by (induct_thm_tac multiset_induct "K" 1); |
6162 | 461 |
by (Asm_simp_tac 1); |
462 |
by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1); |
|
463 |
by (Blast_tac 1); |
|
5628 | 464 |
qed "lemma1"; |
465 |
||
466 |
Goalw [W_def] |
|
467 |
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W"; |
|
6162 | 468 |
by (etac acc_induct 1); |
469 |
by (blast_tac (claset() addIs [export lemma1]) 1); |
|
5628 | 470 |
qed "lemma2"; |
471 |
||
472 |
Goalw [W_def] |
|
473 |
"wf(r) ==> !M:W. M+{#a#} : W"; |
|
6162 | 474 |
by (eres_inst_tac [("a","a")] wf_induct 1); |
475 |
by (blast_tac (claset() addIs [export lemma2]) 1); |
|
5628 | 476 |
qed "lemma3"; |
477 |
||
478 |
Goalw [W_def] "wf(r) ==> M : W"; |
|
9747 | 479 |
by (induct_thm_tac multiset_induct "M" 1); |
6162 | 480 |
by (rtac accI 1); |
481 |
by (Asm_full_simp_tac 1); |
|
482 |
by (blast_tac (claset() addDs [export lemma3]) 1); |
|
5628 | 483 |
qed "all_accessible"; |
484 |
||
6024 | 485 |
Close_locale "MSOrd"; |
5628 | 486 |
|
487 |
Goal "wf(r) ==> wf(mult1 r)"; |
|
6162 | 488 |
by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1); |
5628 | 489 |
qed "wf_mult1"; |
490 |
||
491 |
Goalw [mult_def] "wf(r) ==> wf(mult r)"; |
|
6162 | 492 |
by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1); |
5628 | 493 |
qed "wf_mult"; |
494 |
||
5772 | 495 |
(** Equivalence of mult with the usual (closure-free) def **) |
496 |
||
497 |
(* Badly needed: a linear arithmetic tactic for multisets *) |
|
498 |
||
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
499 |
Goal "a :# J ==> I+J - {#a#} = I + (J-{#a#})"; |
6162 | 500 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1); |
5772 | 501 |
qed "diff_union_single_conv"; |
5628 | 502 |
|
5772 | 503 |
(* One direction *) |
504 |
Goalw [mult_def,mult1_def,set_of_def] |
|
505 |
"trans r ==> \ |
|
506 |
\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \ |
|
507 |
\ (!k : set_of K. ? j : set_of J. (k,j) : r))"; |
|
6162 | 508 |
by (etac converse_trancl_induct 1); |
509 |
by (Clarify_tac 1); |
|
510 |
by (res_inst_tac [("x","M0")] exI 1); |
|
511 |
by (Simp_tac 1); |
|
512 |
by (Clarify_tac 1); |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
513 |
by (case_tac "a :# K" 1); |
6162 | 514 |
by (res_inst_tac [("x","I")] exI 1); |
515 |
by (Simp_tac 1); |
|
516 |
by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1); |
|
517 |
by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1); |
|
518 |
by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1); |
|
519 |
by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1); |
|
520 |
by (full_simp_tac (simpset() addsimps [trans_def]) 1); |
|
521 |
by (Blast_tac 1); |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
522 |
by (subgoal_tac "a :# I" 1); |
6162 | 523 |
by (res_inst_tac [("x","I-{#a#}")] exI 1); |
524 |
by (res_inst_tac [("x","J+{#a#}")] exI 1); |
|
525 |
by (res_inst_tac [("x","K + Ka")] exI 1); |
|
526 |
by (rtac conjI 1); |
|
527 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq] |
|
5772 | 528 |
addsplits [nat_diff_split]) 1); |
6162 | 529 |
by (rtac conjI 1); |
530 |
by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1); |
|
531 |
by (Asm_full_simp_tac 1); |
|
532 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq] |
|
5772 | 533 |
addsplits [nat_diff_split]) 1); |
6162 | 534 |
by (full_simp_tac (simpset() addsimps [trans_def]) 1); |
535 |
by (Blast_tac 1); |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
536 |
by (subgoal_tac "a :# (M0 +{#a#})" 1); |
6162 | 537 |
by (Asm_full_simp_tac 1); |
538 |
by (Simp_tac 1); |
|
5772 | 539 |
qed "mult_implies_one_step"; |
8914 | 540 |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
541 |
Goal "a :# M ==> M = M - {#a#} + {#a#}"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
542 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
543 |
qed "elem_imp_eq_diff_union"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
544 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
545 |
Goal "size M = Suc n ==> EX a N. M = N + {#a#}"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
546 |
by (etac (size_eq_Suc_imp_elem RS exE) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
547 |
by (dtac elem_imp_eq_diff_union 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
548 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
549 |
qed "size_eq_Suc_imp_eq_union"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
550 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
551 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
552 |
Goal "trans r ==> \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
553 |
\ ALL I J K. \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
554 |
\ (size J = n & J ~= {#} & \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
555 |
\ (! k : set_of K. ? j : set_of J. (k,j) : r)) --> (I+K, I+J) : mult r"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
556 |
by (induct_tac "n" 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
557 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
558 |
by (ftac size_eq_Suc_imp_eq_union 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
559 |
by (Clarify_tac 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
560 |
ren "J'" 1; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
561 |
by (Asm_full_simp_tac 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
562 |
by (etac notE 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
563 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
564 |
by (case_tac "J' = {#}" 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
565 |
by (asm_full_simp_tac (simpset() addsimps [mult_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
566 |
by (rtac r_into_trancl 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
567 |
by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
568 |
by (Blast_tac 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
569 |
(*Now we know J' ~= {#}*) |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
570 |
by (cut_inst_tac [("M","K"),("P", "%x. (x,a):r")] multiset_partition 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
571 |
by (eres_inst_tac [("P", "ALL k : set_of K. ?P k")] rev_mp 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
572 |
by (etac ssubst 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
573 |
by (asm_full_simp_tac (simpset() addsimps [Ball_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
574 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
575 |
by (subgoal_tac "((I + {# x : K. (x, a) : r#}) + {# x : K. (x, a) ~: r#}, \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
576 |
\ (I + {# x : K. (x, a) : r#}) + J') : mult r" 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
577 |
by (Force_tac 2); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
578 |
by (full_simp_tac (simpset() addsimps [union_assoc RS sym, mult_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
579 |
by (etac trancl_trans 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
580 |
by (rtac r_into_trancl 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
581 |
by (asm_full_simp_tac (simpset() addsimps [mult1_def,set_of_def]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
582 |
by (res_inst_tac [("x", "a")] exI 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
583 |
by (res_inst_tac [("x", "I + J'")] exI 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
584 |
by (asm_simp_tac (simpset() addsimps union_ac) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
585 |
qed_spec_mp "one_step_implies_mult_lemma"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
586 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
587 |
Goal "[| trans r; J ~= {#}; \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
588 |
\ ALL k : set_of K. EX j : set_of J. (k,j) : r |] \ |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
589 |
\ ==> (I+K, I+J) : mult r"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
590 |
by (rtac one_step_implies_mult_lemma 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
591 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
592 |
qed "one_step_implies_mult"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
593 |
|
8914 | 594 |
|
595 |
(** Proving that multisets are partially ordered **) |
|
596 |
||
597 |
Goalw [trans_def] "trans {(x',x). x' < (x::'a::order)}"; |
|
598 |
by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
599 |
qed "trans_base_order"; |
|
600 |
||
601 |
Goal "finite A ==> (ALL x: A. EX y : A. x < (y::'a::order)) --> A={}"; |
|
602 |
by (etac finite_induct 1); |
|
603 |
by Auto_tac; |
|
604 |
by (blast_tac (claset() addIs [order_less_trans]) 1); |
|
605 |
qed_spec_mp "mult_irrefl_lemma"; |
|
606 |
||
607 |
(*irreflexivity*) |
|
608 |
Goalw [mult_less_def] "~ M < (M :: ('a::order)multiset)"; |
|
609 |
by Auto_tac; |
|
610 |
by (dtac (trans_base_order RS mult_implies_one_step) 1); |
|
611 |
by Auto_tac; |
|
612 |
by (dtac (finite_set_of RS mult_irrefl_lemma) 1); |
|
613 |
by (asm_full_simp_tac (simpset() addsimps [set_of_eq_empty_iff]) 1); |
|
614 |
qed "mult_less_not_refl"; |
|
615 |
||
616 |
(* N<N ==> R *) |
|
617 |
bind_thm ("mult_less_irrefl", mult_less_not_refl RS notE); |
|
618 |
AddSEs [mult_less_irrefl]; |
|
619 |
||
620 |
(*transitivity*) |
|
621 |
Goalw [mult_less_def, mult_def] |
|
622 |
"[| K < M; M < N |] ==> K < (N :: ('a::order)multiset)"; |
|
623 |
by (blast_tac (claset() addIs [trancl_trans]) 1); |
|
624 |
qed "mult_less_trans"; |
|
625 |
||
626 |
(*asymmetry*) |
|
627 |
Goal "M < N ==> ~ N < (M :: ('a::order)multiset)"; |
|
628 |
by Auto_tac; |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
629 |
by (rtac (mult_less_not_refl RS notE) 1); |
8914 | 630 |
by (etac mult_less_trans 1); |
631 |
by (assume_tac 1); |
|
632 |
qed "mult_less_not_sym"; |
|
633 |
||
634 |
(* [| M<N; ~P ==> N<M |] ==> P *) |
|
10231 | 635 |
bind_thm ("mult_less_asym", mult_less_not_sym RS contrapos_np); |
8914 | 636 |
|
637 |
Goalw [mult_le_def] "M <= (M :: ('a::order)multiset)"; |
|
638 |
by Auto_tac; |
|
639 |
qed "mult_le_refl"; |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
640 |
AddIffs [mult_le_refl]; |
8914 | 641 |
|
642 |
(*anti-symmetry*) |
|
643 |
Goalw [mult_le_def] "[| M <= N; N <= M |] ==> M = (N :: ('a::order)multiset)"; |
|
644 |
by (blast_tac (claset() addDs [mult_less_not_sym]) 1); |
|
645 |
qed "mult_le_antisym"; |
|
646 |
||
647 |
(*transitivity*) |
|
648 |
Goalw [mult_le_def] |
|
649 |
"[| K <= M; M <= N |] ==> K <= (N :: ('a::order)multiset)"; |
|
650 |
by (blast_tac (claset() addIs [mult_less_trans]) 1); |
|
651 |
qed "mult_le_trans"; |
|
652 |
||
653 |
Goalw [mult_le_def] "M < N = (M <= N & M ~= (N :: ('a::order)multiset))"; |
|
654 |
by Auto_tac; |
|
655 |
qed "mult_less_le"; |
|
9017
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
656 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
657 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
658 |
(** Monotonicity of multiset union **) |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
659 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
660 |
Goalw [mult1_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
661 |
"[| (B,D) : mult1 r; trans r |] ==> (C + B, C + D) : mult1 r"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
662 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
663 |
by (res_inst_tac [("x", "a")] exI 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
664 |
by (res_inst_tac [("x", "C+M0")] exI 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
665 |
by (asm_simp_tac (simpset() addsimps [union_assoc]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
666 |
qed "mult1_union"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
667 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
668 |
Goalw [mult_less_def, mult_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
669 |
"!!C:: ('a::order) multiset. B<D ==> C+B < C+D"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
670 |
by (etac trancl_induct 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
671 |
by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
672 |
r_into_trancl]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
673 |
by (blast_tac (claset() addIs [mult1_union, transI, order_less_trans, |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
674 |
r_into_trancl, trancl_trans]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
675 |
qed "union_less_mono2"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
676 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
677 |
Goal "!!C:: ('a::order) multiset. B<D ==> B+C < D+C"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
678 |
by (simp_tac (simpset() addsimps [union_commute]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
679 |
by (etac union_less_mono2 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
680 |
qed "union_less_mono1"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
681 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
682 |
Goal "!!C:: ('a::order) multiset. [| A<C; B<D |] ==> A+B < C+D"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
683 |
by (blast_tac (claset() addIs [union_less_mono1, union_less_mono2, |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
684 |
mult_less_trans]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
685 |
qed "union_less_mono"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
686 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
687 |
Goalw [mult_le_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
688 |
"!!D:: ('a::order) multiset. [| A<=C; B<=D |] ==> A+B <= C+D"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
689 |
by (blast_tac (claset() addIs [union_less_mono, union_less_mono1, |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
690 |
union_less_mono2]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
691 |
qed "union_le_mono"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
692 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
693 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
694 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
695 |
Goalw [mult_le_def, mult_less_def] |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
696 |
"{#} <= (M :: ('a::order) multiset)"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
697 |
by (case_tac "M={#}" 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
698 |
by (subgoal_tac "({#} + {#}, {#} + M) : mult(Collect (split op <))" 2); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
699 |
by (rtac one_step_implies_mult 3); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
700 |
bw trans_def; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
701 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
702 |
by (blast_tac (claset() addIs [order_less_trans]) 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
703 |
qed "empty_leI"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
704 |
AddIffs [empty_leI]; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
705 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
706 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
707 |
Goal "!!A:: ('a::order) multiset. A <= A+B"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
708 |
by (subgoal_tac "A+{#} <= A+B" 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
709 |
by (rtac union_le_mono 2); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
710 |
by Auto_tac; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
711 |
qed "union_upper1"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
712 |
|
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
713 |
Goal "!!A:: ('a::order) multiset. B <= A+B"; |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
714 |
by (stac union_commute 1 THEN rtac union_upper1 1); |
ff259b415c4d
Many new theorems about multisets and their ordering, including basic
paulson
parents:
9004
diff
changeset
|
715 |
qed "union_upper2"; |