5628
|
1 |
(* Title: HOL/Induct/Multiset.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1998 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
Addsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
|
|
8 |
|
|
9 |
(** Preservation of representing set `multiset' **)
|
|
10 |
|
|
11 |
Goalw [multiset_def] "(%a. 0) : multiset";
|
6162
|
12 |
by (Simp_tac 1);
|
5628
|
13 |
qed "const0_in_multiset";
|
|
14 |
Addsimps [const0_in_multiset];
|
|
15 |
|
|
16 |
Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
|
6162
|
17 |
by (Simp_tac 1);
|
5628
|
18 |
qed "only1_in_multiset";
|
|
19 |
Addsimps [only1_in_multiset];
|
|
20 |
|
|
21 |
Goalw [multiset_def]
|
|
22 |
"[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
|
6162
|
23 |
by (Asm_full_simp_tac 1);
|
|
24 |
by (dtac finite_UnI 1);
|
|
25 |
by (assume_tac 1);
|
|
26 |
by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
|
5628
|
27 |
qed "union_preserves_multiset";
|
|
28 |
Addsimps [union_preserves_multiset];
|
|
29 |
|
|
30 |
Goalw [multiset_def]
|
|
31 |
"[| M : multiset |] ==> (%a. M a - N a) : multiset";
|
6162
|
32 |
by (Asm_full_simp_tac 1);
|
|
33 |
by (etac (rotate_prems 1 finite_subset) 1);
|
|
34 |
by (Auto_tac);
|
5628
|
35 |
qed "diff_preserves_multiset";
|
|
36 |
Addsimps [diff_preserves_multiset];
|
|
37 |
|
|
38 |
(** Injectivity of Rep_multiset **)
|
|
39 |
|
|
40 |
Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
|
6162
|
41 |
by (rtac iffI 1);
|
|
42 |
by (Asm_simp_tac 1);
|
|
43 |
by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
|
|
44 |
by (Asm_full_simp_tac 1);
|
5628
|
45 |
qed "multiset_eq_conv_Rep_eq";
|
|
46 |
Addsimps [multiset_eq_conv_Rep_eq];
|
|
47 |
Addsimps [expand_fun_eq];
|
|
48 |
(*
|
|
49 |
Goal
|
|
50 |
"[| f : multiset; g : multiset |] ==> \
|
|
51 |
\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
|
6162
|
52 |
by (rtac iffI 1);
|
|
53 |
by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
|
|
54 |
by (Asm_full_simp_tac 1);
|
|
55 |
by (subgoal_tac "f = g" 1);
|
|
56 |
by (Asm_simp_tac 1);
|
|
57 |
by (rtac ext 1);
|
|
58 |
by (Blast_tac 1);
|
5628
|
59 |
qed "Abs_multiset_eq";
|
|
60 |
Addsimps [Abs_multiset_eq];
|
|
61 |
*)
|
|
62 |
|
|
63 |
(** Equations **)
|
|
64 |
|
|
65 |
(* union *)
|
|
66 |
|
|
67 |
Goalw [union_def,empty_def]
|
|
68 |
"M + {#} = M & {#} + M = M";
|
6162
|
69 |
by (Simp_tac 1);
|
5628
|
70 |
qed "union_empty";
|
|
71 |
Addsimps [union_empty];
|
|
72 |
|
|
73 |
Goalw [union_def]
|
|
74 |
"(M::'a multiset) + N = N + M";
|
6162
|
75 |
by (simp_tac (simpset() addsimps add_ac) 1);
|
5628
|
76 |
qed "union_comm";
|
|
77 |
|
|
78 |
Goalw [union_def]
|
|
79 |
"((M::'a multiset)+N)+K = M+(N+K)";
|
6162
|
80 |
by (simp_tac (simpset() addsimps add_ac) 1);
|
5628
|
81 |
qed "union_assoc";
|
|
82 |
|
|
83 |
qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
|
|
84 |
(fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1,
|
|
85 |
rtac (union_comm RS arg_cong) 1]);
|
|
86 |
|
7454
|
87 |
bind_thms ("union_ac", [union_assoc, union_comm, union_lcomm]);
|
5628
|
88 |
|
|
89 |
(* diff *)
|
|
90 |
|
|
91 |
Goalw [empty_def,diff_def]
|
|
92 |
"M-{#} = M & {#}-M = {#}";
|
6162
|
93 |
by (Simp_tac 1);
|
5628
|
94 |
qed "diff_empty";
|
|
95 |
Addsimps [diff_empty];
|
|
96 |
|
|
97 |
Goalw [union_def,diff_def]
|
|
98 |
"M+{#a#}-{#a#} = M";
|
6162
|
99 |
by (Simp_tac 1);
|
5628
|
100 |
qed "diff_union_inverse2";
|
|
101 |
Addsimps [diff_union_inverse2];
|
|
102 |
|
|
103 |
(* count *)
|
|
104 |
|
|
105 |
Goalw [count_def,empty_def]
|
|
106 |
"count {#} a = 0";
|
6162
|
107 |
by (Simp_tac 1);
|
5628
|
108 |
qed "count_empty";
|
|
109 |
Addsimps [count_empty];
|
|
110 |
|
|
111 |
Goalw [count_def,single_def]
|
|
112 |
"count {#b#} a = (if b=a then 1 else 0)";
|
6162
|
113 |
by (Simp_tac 1);
|
5628
|
114 |
qed "count_single";
|
|
115 |
Addsimps [count_single];
|
|
116 |
|
|
117 |
Goalw [count_def,union_def]
|
|
118 |
"count (M+N) a = count M a + count N a";
|
6162
|
119 |
by (Simp_tac 1);
|
5628
|
120 |
qed "count_union";
|
|
121 |
Addsimps [count_union];
|
|
122 |
|
5772
|
123 |
Goalw [count_def,diff_def]
|
|
124 |
"count (M-N) a = count M a - count N a";
|
6162
|
125 |
by (Simp_tac 1);
|
5772
|
126 |
qed "count_diff";
|
|
127 |
Addsimps [count_diff];
|
|
128 |
|
5628
|
129 |
(* set_of *)
|
|
130 |
|
|
131 |
Goalw [set_of_def] "set_of {#} = {}";
|
6162
|
132 |
by (Simp_tac 1);
|
5628
|
133 |
qed "set_of_empty";
|
|
134 |
Addsimps [set_of_empty];
|
|
135 |
|
|
136 |
Goalw [set_of_def]
|
|
137 |
"set_of {#b#} = {b}";
|
6162
|
138 |
by (Simp_tac 1);
|
5628
|
139 |
qed "set_of_single";
|
|
140 |
Addsimps [set_of_single];
|
|
141 |
|
|
142 |
Goalw [set_of_def]
|
|
143 |
"set_of(M+N) = set_of M Un set_of N";
|
6162
|
144 |
by (Auto_tac);
|
5628
|
145 |
qed "set_of_union";
|
|
146 |
Addsimps [set_of_union];
|
|
147 |
|
|
148 |
(* size *)
|
|
149 |
|
|
150 |
Goalw [size_def] "size {#} = 0";
|
6162
|
151 |
by (Simp_tac 1);
|
5628
|
152 |
qed "size_empty";
|
|
153 |
Addsimps [size_empty];
|
|
154 |
|
|
155 |
Goalw [size_def]
|
|
156 |
"size {#b#} = 1";
|
6162
|
157 |
by (Simp_tac 1);
|
5628
|
158 |
qed "size_single";
|
|
159 |
Addsimps [size_single];
|
|
160 |
|
|
161 |
(* Some other day...
|
|
162 |
Goalw [size_def]
|
|
163 |
"size (M+N::'a multiset) = size M + size N";
|
|
164 |
*)
|
|
165 |
|
|
166 |
(* equalities *)
|
|
167 |
|
5772
|
168 |
Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
|
6162
|
169 |
by (Simp_tac 1);
|
5772
|
170 |
qed "multiset_eq_conv_count_eq";
|
|
171 |
|
5628
|
172 |
Goalw [single_def,empty_def] "{#a#} ~= {#} & {#} ~= {#a#}";
|
6162
|
173 |
by (Simp_tac 1);
|
5628
|
174 |
qed "single_not_empty";
|
|
175 |
Addsimps [single_not_empty];
|
|
176 |
|
|
177 |
Goalw [single_def] "({#a#}={#b#}) = (a=b)";
|
6162
|
178 |
by (Auto_tac);
|
5628
|
179 |
qed "single_eq_single";
|
|
180 |
Addsimps [single_eq_single];
|
|
181 |
|
|
182 |
Goalw [union_def,empty_def]
|
|
183 |
"(M+N = {#}) = (M = {#} & N = {#})";
|
6162
|
184 |
by (Simp_tac 1);
|
|
185 |
by (Blast_tac 1);
|
5628
|
186 |
qed "union_eq_empty";
|
|
187 |
AddIffs [union_eq_empty];
|
|
188 |
|
|
189 |
Goalw [union_def,empty_def]
|
|
190 |
"({#} = M+N) = (M = {#} & N = {#})";
|
6162
|
191 |
by (Simp_tac 1);
|
|
192 |
by (Blast_tac 1);
|
5628
|
193 |
qed "empty_eq_union";
|
|
194 |
AddIffs [empty_eq_union];
|
|
195 |
|
|
196 |
Goalw [union_def]
|
|
197 |
"(M+K = N+K) = (M=(N::'a multiset))";
|
6162
|
198 |
by (Simp_tac 1);
|
5628
|
199 |
qed "union_right_cancel";
|
|
200 |
Addsimps [union_right_cancel];
|
|
201 |
|
|
202 |
Goalw [union_def]
|
|
203 |
"(K+M = K+N) = (M=(N::'a multiset))";
|
6162
|
204 |
by (Simp_tac 1);
|
5628
|
205 |
qed "union_left_cancel";
|
|
206 |
Addsimps [union_left_cancel];
|
|
207 |
|
|
208 |
Goalw [empty_def,single_def,union_def]
|
|
209 |
"(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
|
6162
|
210 |
by (simp_tac (simpset() addsimps [add_is_1]) 1);
|
|
211 |
by (Blast_tac 1);
|
5628
|
212 |
qed "union_is_single";
|
|
213 |
|
|
214 |
Goalw [empty_def,single_def,union_def]
|
|
215 |
"({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
|
6162
|
216 |
by (simp_tac (simpset() addsimps [one_is_add]) 1);
|
|
217 |
by (blast_tac (claset() addDs [sym]) 1);
|
5628
|
218 |
qed "single_is_union";
|
|
219 |
|
|
220 |
Goalw [single_def,union_def,diff_def]
|
|
221 |
"(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
|
6162
|
222 |
by (Simp_tac 1);
|
|
223 |
by (rtac conjI 1);
|
|
224 |
by (Force_tac 1);
|
|
225 |
by (Clarify_tac 1);
|
|
226 |
by (rtac conjI 1);
|
|
227 |
by (Blast_tac 1);
|
|
228 |
by (Clarify_tac 1);
|
|
229 |
by (rtac iffI 1);
|
|
230 |
by (rtac conjI 1);
|
|
231 |
by (Clarify_tac 1);
|
|
232 |
by (rtac conjI 1);
|
|
233 |
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
|
5628
|
234 |
(* PROOF FAILED:
|
6162
|
235 |
by (Blast_tac 1);
|
5628
|
236 |
*)
|
6162
|
237 |
by (Fast_tac 1);
|
|
238 |
by (Asm_simp_tac 1);
|
|
239 |
by (Force_tac 1);
|
5628
|
240 |
qed "add_eq_conv_diff";
|
|
241 |
|
|
242 |
(* FIXME
|
|
243 |
val prems = Goal
|
|
244 |
"[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
|
6162
|
245 |
by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
|
5628
|
246 |
measure_induct 1);
|
6162
|
247 |
by (Clarify_tac 1);
|
|
248 |
by (resolve_tac prems 1);
|
|
249 |
by (assume_tac 1);
|
|
250 |
by (Clarify_tac 1);
|
|
251 |
by (subgoal_tac "finite G" 1);
|
|
252 |
by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
|
|
253 |
by (etac allE 1);
|
|
254 |
by (etac impE 1);
|
|
255 |
by (Blast_tac 2);
|
|
256 |
by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
|
7454
|
257 |
no_qed();
|
5628
|
258 |
val lemma = result();
|
|
259 |
|
|
260 |
val prems = Goal
|
|
261 |
"[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
|
6162
|
262 |
by (rtac (lemma RS mp) 1);
|
5628
|
263 |
by (REPEAT(ares_tac prems 1));
|
|
264 |
qed "finite_psubset_induct";
|
|
265 |
|
|
266 |
Better: use wf_finite_psubset in WF_Rel
|
|
267 |
*)
|
|
268 |
|
|
269 |
(** Towards the induction rule **)
|
|
270 |
|
|
271 |
Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
|
6162
|
272 |
by (etac finite_induct 1);
|
|
273 |
by (Auto_tac);
|
5628
|
274 |
qed "setsum_0";
|
|
275 |
Addsimps [setsum_0];
|
|
276 |
|
|
277 |
Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
|
6162
|
278 |
by (etac finite_induct 1);
|
|
279 |
by (Auto_tac);
|
7454
|
280 |
no_qed();
|
5628
|
281 |
val lemma = result();
|
|
282 |
|
|
283 |
Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
|
6162
|
284 |
by (dtac lemma 1);
|
|
285 |
by (Fast_tac 1);
|
5628
|
286 |
qed "setsum_SucD";
|
|
287 |
|
|
288 |
Goal "[| finite F; 0 < f a |] ==> \
|
|
289 |
\ setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
|
6162
|
290 |
by (etac finite_induct 1);
|
|
291 |
by (Auto_tac);
|
|
292 |
by (asm_simp_tac (simpset() addsimps add_ac) 1);
|
|
293 |
by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
|
|
294 |
by (Auto_tac);
|
5628
|
295 |
qed "setsum_decr";
|
|
296 |
|
|
297 |
val prems = Goalw [multiset_def]
|
|
298 |
"[| P(%a.0); \
|
|
299 |
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
|
|
300 |
\ ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
|
6162
|
301 |
by (induct_tac "n" 1);
|
|
302 |
by (Asm_simp_tac 1);
|
|
303 |
by (Clarify_tac 1);
|
|
304 |
by (subgoal_tac "f = (%a.0)" 1);
|
|
305 |
by (Asm_simp_tac 1);
|
|
306 |
by (resolve_tac prems 1);
|
|
307 |
by (rtac ext 1);
|
|
308 |
by (Force_tac 1);
|
|
309 |
by (Clarify_tac 1);
|
7499
|
310 |
by (ftac setsum_SucD 1);
|
6162
|
311 |
by (assume_tac 1);
|
|
312 |
by (Clarify_tac 1);
|
|
313 |
by (rename_tac "a" 1);
|
|
314 |
by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
|
|
315 |
by (etac (rotate_prems 1 finite_subset) 2);
|
|
316 |
by (Simp_tac 2);
|
|
317 |
by (Blast_tac 2);
|
|
318 |
by (subgoal_tac
|
5628
|
319 |
"f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
|
6162
|
320 |
by (rtac ext 2);
|
|
321 |
by (Asm_simp_tac 2);
|
|
322 |
by (EVERY1[etac ssubst, resolve_tac prems]);
|
|
323 |
by (Blast_tac 1);
|
|
324 |
by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
|
|
325 |
by (Blast_tac 1);
|
|
326 |
by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
|
|
327 |
by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
|
|
328 |
by (Blast_tac 2);
|
|
329 |
by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
|
|
330 |
by (Blast_tac 2);
|
|
331 |
by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
|
5983
|
332 |
addcongs [conj_cong]) 1);
|
7454
|
333 |
no_qed();
|
5628
|
334 |
val lemma = result();
|
|
335 |
|
|
336 |
val major::prems = Goal
|
|
337 |
"[| f : multiset; \
|
|
338 |
\ P(%a.0); \
|
|
339 |
\ !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
|
6162
|
340 |
by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
|
|
341 |
by (REPEAT(ares_tac (refl::prems) 1));
|
5628
|
342 |
qed "Rep_multiset_induct";
|
|
343 |
|
|
344 |
val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
|
|
345 |
"[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
|
|
346 |
by (rtac (Rep_multiset_inverse RS subst) 1);
|
|
347 |
by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
|
6162
|
348 |
by (rtac prem1 1);
|
|
349 |
by (Clarify_tac 1);
|
|
350 |
by (subgoal_tac
|
5628
|
351 |
"f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
|
6162
|
352 |
by (Simp_tac 2);
|
|
353 |
by (etac ssubst 1);
|
|
354 |
by (etac (Abs_multiset_inverse RS subst) 1);
|
|
355 |
by (etac(simplify (simpset()) prem2)1);
|
5628
|
356 |
qed "multiset_induct";
|
|
357 |
|
|
358 |
Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
|
|
359 |
Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
|
|
360 |
|
|
361 |
Goal
|
|
362 |
"(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
|
6162
|
363 |
by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
|
|
364 |
by (Auto_tac);
|
5628
|
365 |
qed "add_eq_conv_ex";
|
|
366 |
|
|
367 |
(** order **)
|
|
368 |
|
|
369 |
Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
|
6162
|
370 |
by (Simp_tac 1);
|
5628
|
371 |
qed "not_less_empty";
|
|
372 |
AddIffs [not_less_empty];
|
|
373 |
|
|
374 |
Goalw [mult1_def]
|
|
375 |
"(N,M0 + {#a#}) : mult1(r) = \
|
|
376 |
\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
|
|
377 |
\ (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
|
6162
|
378 |
by (rtac iffI 1);
|
|
379 |
by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
|
|
380 |
by (Clarify_tac 1);
|
|
381 |
by (etac disjE 1);
|
|
382 |
by (Blast_tac 1);
|
|
383 |
by (Clarify_tac 1);
|
|
384 |
by (res_inst_tac [("x","Ka+K")] exI 1);
|
|
385 |
by (simp_tac (simpset() addsimps union_ac) 1);
|
|
386 |
by (Blast_tac 1);
|
|
387 |
by (etac disjE 1);
|
|
388 |
by (Clarify_tac 1);
|
|
389 |
by (res_inst_tac [("x","aa")] exI 1);
|
|
390 |
by (res_inst_tac [("x","M0+{#a#}")] exI 1);
|
|
391 |
by (res_inst_tac [("x","K")] exI 1);
|
|
392 |
by (simp_tac (simpset() addsimps union_ac) 1);
|
|
393 |
by (Blast_tac 1);
|
5628
|
394 |
qed "less_add_conv";
|
|
395 |
|
|
396 |
Open_locale "MSOrd";
|
|
397 |
|
|
398 |
val W_def = thm "W_def";
|
|
399 |
|
|
400 |
Goalw [W_def]
|
|
401 |
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
|
|
402 |
\ !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
|
|
403 |
\ ==> M0+{#a#} : W";
|
6162
|
404 |
by (rtac accI 1);
|
|
405 |
by (rename_tac "N" 1);
|
|
406 |
by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
|
|
407 |
by (etac disjE 1);
|
|
408 |
by (Blast_tac 1);
|
|
409 |
by (Clarify_tac 1);
|
|
410 |
by (rotate_tac ~1 1);
|
|
411 |
by (etac rev_mp 1);
|
|
412 |
by (res_inst_tac [("M","K")] multiset_induct 1);
|
|
413 |
by (Asm_simp_tac 1);
|
|
414 |
by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
|
|
415 |
by (Blast_tac 1);
|
5628
|
416 |
qed "lemma1";
|
|
417 |
|
|
418 |
Goalw [W_def]
|
|
419 |
"[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
|
6162
|
420 |
by (etac acc_induct 1);
|
|
421 |
by (blast_tac (claset() addIs [export lemma1]) 1);
|
5628
|
422 |
qed "lemma2";
|
|
423 |
|
|
424 |
Goalw [W_def]
|
|
425 |
"wf(r) ==> !M:W. M+{#a#} : W";
|
6162
|
426 |
by (eres_inst_tac [("a","a")] wf_induct 1);
|
|
427 |
by (blast_tac (claset() addIs [export lemma2]) 1);
|
5628
|
428 |
qed "lemma3";
|
|
429 |
|
|
430 |
Goalw [W_def] "wf(r) ==> M : W";
|
6162
|
431 |
by (res_inst_tac [("M","M")] multiset_induct 1);
|
|
432 |
by (rtac accI 1);
|
|
433 |
by (Asm_full_simp_tac 1);
|
|
434 |
by (blast_tac (claset() addDs [export lemma3]) 1);
|
5628
|
435 |
qed "all_accessible";
|
|
436 |
|
6024
|
437 |
Close_locale "MSOrd";
|
5628
|
438 |
|
|
439 |
Goal "wf(r) ==> wf(mult1 r)";
|
6162
|
440 |
by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
|
5628
|
441 |
qed "wf_mult1";
|
|
442 |
|
|
443 |
Goalw [mult_def] "wf(r) ==> wf(mult r)";
|
6162
|
444 |
by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
|
5628
|
445 |
qed "wf_mult";
|
|
446 |
|
5772
|
447 |
(** Equivalence of mult with the usual (closure-free) def **)
|
|
448 |
|
|
449 |
(* Badly needed: a linear arithmetic tactic for multisets *)
|
|
450 |
|
|
451 |
Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
|
6162
|
452 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
|
5772
|
453 |
qed "diff_union_single_conv";
|
5628
|
454 |
|
5772
|
455 |
(* One direction *)
|
|
456 |
Goalw [mult_def,mult1_def,set_of_def]
|
|
457 |
"trans r ==> \
|
|
458 |
\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
|
|
459 |
\ (!k : set_of K. ? j : set_of J. (k,j) : r))";
|
6162
|
460 |
by (etac converse_trancl_induct 1);
|
|
461 |
by (Clarify_tac 1);
|
|
462 |
by (res_inst_tac [("x","M0")] exI 1);
|
|
463 |
by (Simp_tac 1);
|
|
464 |
by (Clarify_tac 1);
|
|
465 |
by (case_tac "elem K a" 1);
|
|
466 |
by (res_inst_tac [("x","I")] exI 1);
|
|
467 |
by (Simp_tac 1);
|
|
468 |
by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
|
|
469 |
by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
|
|
470 |
by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
|
|
471 |
by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
|
|
472 |
by (full_simp_tac (simpset() addsimps [trans_def]) 1);
|
|
473 |
by (Blast_tac 1);
|
|
474 |
by (subgoal_tac "elem I a" 1);
|
|
475 |
by (res_inst_tac [("x","I-{#a#}")] exI 1);
|
|
476 |
by (res_inst_tac [("x","J+{#a#}")] exI 1);
|
|
477 |
by (res_inst_tac [("x","K + Ka")] exI 1);
|
|
478 |
by (rtac conjI 1);
|
|
479 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
|
5772
|
480 |
addsplits [nat_diff_split]) 1);
|
6162
|
481 |
by (rtac conjI 1);
|
|
482 |
by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
|
|
483 |
by (Asm_full_simp_tac 1);
|
|
484 |
by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
|
5772
|
485 |
addsplits [nat_diff_split]) 1);
|
6162
|
486 |
by (full_simp_tac (simpset() addsimps [trans_def]) 1);
|
|
487 |
by (Blast_tac 1);
|
|
488 |
by (subgoal_tac "elem (M0 +{#a#}) a" 1);
|
|
489 |
by (Asm_full_simp_tac 1);
|
|
490 |
by (Simp_tac 1);
|
5772
|
491 |
qed "mult_implies_one_step";
|