|
1 (* Title: ZF/UNITY/FoldSet.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 |
|
7 A "fold" functional for finite sets. For n non-negative we have |
|
8 fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at |
|
9 least left-commutative. |
|
10 *) |
|
11 |
|
12 (** foldSet **) |
|
13 |
|
14 bind_thm("empty_fold_setE", |
|
15 fold_set.mk_cases "<0, x> : fold_set(A, B, f,e)"); |
|
16 bind_thm("cons_fold_setE", |
|
17 fold_set.mk_cases "<cons(x,C), y> : fold_set(A, B, f,e)"); |
|
18 |
|
19 bind_thm("fold_set_lhs", fold_set.dom_subset RS subsetD RS SigmaD1); |
|
20 bind_thm("fold_set_rhs", fold_set.dom_subset RS subsetD RS SigmaD2); |
|
21 |
|
22 (* add-hoc lemmas *) |
|
23 |
|
24 Goal "[| x~:C; x~:B |] ==> cons(x,B)=cons(x,C) <-> B = C"; |
|
25 by (auto_tac (claset() addEs [equalityE], simpset())); |
|
26 qed "cons_lemma1"; |
|
27 |
|
28 Goal "[| cons(x, B)=cons(y, C); x~=y; x~:B; y~:C |] \ |
|
29 \ ==> B - {y} = C-{x} & x:C & y:B"; |
|
30 by (auto_tac (claset() addEs [equalityE], simpset())); |
|
31 qed "cons_lemma2"; |
|
32 |
|
33 |
|
34 Open_locale "LC"; |
|
35 val f_lcomm = thm "lcomm"; |
|
36 val f_type = thm "ftype"; |
|
37 |
|
38 Goal "[| <C-{x},y> : fold_set(A, B, f,e); x:C; x:A |] \ |
|
39 \ ==> <C, f(x,y)> : fold_set(A, B, f, e)"; |
|
40 by (forward_tac [fold_set_rhs] 1); |
|
41 by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1); |
|
42 by (auto_tac (claset() addIs [f_type], simpset())); |
|
43 qed "Diff1_fold_set"; |
|
44 |
|
45 Goal "[| C:Fin(A); e:B |] ==> EX x. <C, x> : fold_set(A, B, f,e)"; |
|
46 by (etac Fin_induct 1); |
|
47 by (ALLGOALS(Clarify_tac)); |
|
48 by (forward_tac [fold_set_rhs] 2); |
|
49 by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2); |
|
50 by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1)); |
|
51 qed_spec_mp "Fin_imp_fold_set"; |
|
52 |
|
53 |
|
54 Goal "n:nat \ |
|
55 \ ==> ALL C x. |C|<n --> e:B --> <C, x> : fold_set(A, B, f,e)-->\ |
|
56 \ (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x)"; |
|
57 by (etac nat_induct 1); |
|
58 by (auto_tac (claset(), simpset() addsimps [le_iff])); |
|
59 by (etac fold_set.elim 1); |
|
60 by (blast_tac (claset() addEs [empty_fold_setE]) 1); |
|
61 by (etac fold_set.elim 1); |
|
62 by (blast_tac (claset() addEs [empty_fold_setE]) 1); |
|
63 by (Clarify_tac 1); |
|
64 (*force simplification of "|C| < |cons(...)|"*) |
|
65 by (rotate_tac 2 1); |
|
66 by (etac rev_mp 1); |
|
67 by (forw_inst_tac [("a", "Ca")] fold_set_lhs 1); |
|
68 by (forw_inst_tac [("a", "Cb")] fold_set_lhs 1); |
|
69 by (asm_simp_tac (simpset() addsimps [Fin_into_Finite RS Finite_imp_cardinal_cons]) 1); |
|
70 by (rtac impI 1); |
|
71 (** LEVEL 10 **) |
|
72 by (case_tac "x=xb" 1 THEN Auto_tac); |
|
73 by (asm_full_simp_tac (simpset() addsimps [cons_lemma1]) 1); |
|
74 by (Blast_tac 1); |
|
75 (*case x ~= xb*) |
|
76 by (dtac cons_lemma2 1 THEN ALLGOALS Clarify_tac); |
|
77 by (subgoal_tac "Ca = cons(xb, Cb) - {x}" 1); |
|
78 by (blast_tac (claset() addEs [equalityE]) 2); |
|
79 (** LEVEL 20 **) |
|
80 by (subgoal_tac "|Ca| le |Cb|" 1); |
|
81 by (rtac succ_le_imp_le 2); |
|
82 by (hyp_subst_tac 2); |
|
83 by (subgoal_tac "Finite(cons(xb, Cb)) & x:cons(xb, Cb) " 2); |
|
84 by (asm_simp_tac (simpset() addsimps [Finite_imp_succ_cardinal_Diff, |
|
85 Fin_into_Finite RS Finite_imp_cardinal_cons]) 2); |
|
86 by (asm_simp_tac (simpset() addsimps [Fin.consI RS Fin_into_Finite]) 2); |
|
87 by (res_inst_tac [("C1", "Ca-{xb}"), ("e1","e"), ("A1", "A")] |
|
88 (Fin_imp_fold_set RS exE) 1); |
|
89 by (blast_tac (claset() addIs [Diff_subset RS Fin_subset]) 1); |
|
90 by (Blast_tac 1); |
|
91 (** LEVEL 28 **) |
|
92 by (ftac Diff1_fold_set 1 THEN assume_tac 1 THEN assume_tac 1); |
|
93 by (subgoal_tac "ya = f(xb, xa)" 1); |
|
94 by (blast_tac (claset() delrules [equalityCE]) 2); |
|
95 by (subgoal_tac "<Cb-{x}, xa>: fold_set(A, B, f, e)" 1); |
|
96 by (Asm_full_simp_tac 2); |
|
97 by (subgoal_tac "yb = f(x, xa)" 1); |
|
98 by (blast_tac (claset() delrules [equalityCE] |
|
99 addDs [Diff1_fold_set]) 2); |
|
100 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); |
|
101 qed_spec_mp "lemma"; |
|
102 |
|
103 |
|
104 Goal "[| <C, x> : fold_set(A, B, f, e); \ |
|
105 \ <C, y> : fold_set(A, B, f, e); e:B |] ==> y=x"; |
|
106 by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1); |
|
107 by (rewrite_goals_tac [Finite_def]); |
|
108 by (Clarify_tac 1); |
|
109 by (res_inst_tac [("n", "succ(n)")] lemma 1); |
|
110 by (auto_tac (claset() addIs |
|
111 [eqpoll_imp_lepoll RS lepoll_cardinal_le], |
|
112 simpset())); |
|
113 qed "fold_set_determ"; |
|
114 |
|
115 Goalw [fold_def] |
|
116 "[| <C,y> : fold_set(C, B, f, e); e:B |] ==> fold[B](f,e,C) = y"; |
|
117 by (rtac the_equality 1); |
|
118 by (rtac fold_set_determ 2); |
|
119 by Auto_tac; |
|
120 qed "fold_equality"; |
|
121 |
|
122 Goalw [fold_def] "e:B ==> fold[B](f,e,0) = e"; |
|
123 by (blast_tac (claset() addSEs [empty_fold_setE] |
|
124 addIs fold_set.intrs) 1); |
|
125 qed "fold_0"; |
|
126 Addsimps [fold_0]; |
|
127 |
|
128 Goal "[| x ~: C; x:A; e:B |] \ |
|
129 \ ==> <cons(x, C), v> : fold_set(A, B, f, e) <-> \ |
|
130 \ (EX y. <C, y> : fold_set(A, B, f, e) & v = f(x, y))"; |
|
131 by Auto_tac; |
|
132 by (res_inst_tac [("A1", "A"), ("C1", "C")] (Fin_imp_fold_set RS exE) 1); |
|
133 by (res_inst_tac [("x", "xa")] exI 3); |
|
134 by (res_inst_tac [("b", "cons(x, C)")] Fin_subset 1); |
|
135 by (auto_tac (claset() addDs [fold_set_lhs] |
|
136 addIs [f_type]@fold_set.intrs, simpset())); |
|
137 by (blast_tac (claset() addIs [fold_set_determ, f_type]@fold_set.intrs) 1); |
|
138 val lemma = result(); |
|
139 |
|
140 Goal "<D, x> : fold_set(C, B, f, e) \ |
|
141 \ ==> ALL A. C<=A --> <D, x> : fold_set(A, B, f, e)"; |
|
142 by (etac fold_set.induct 1); |
|
143 by (auto_tac (claset() addIs fold_set.intrs, simpset())); |
|
144 qed "lemma2"; |
|
145 |
|
146 Goal " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"; |
|
147 by (Clarify_tac 1); |
|
148 by (forward_tac [impOfSubs fold_set.dom_subset] 1); |
|
149 by (Clarify_tac 1); |
|
150 by (auto_tac (claset() addDs [lemma2], simpset())); |
|
151 qed "fold_set_mono"; |
|
152 |
|
153 Goal "<C,x> : fold_set(A, B, f, e) ==> <C, x> : fold_set(C,B, f,e)"; |
|
154 by (etac fold_set.induct 1); |
|
155 by (auto_tac (claset() addSIs fold_set.intrs, simpset())); |
|
156 by (res_inst_tac [("C1", "C"), ("A1", "cons(x, C)")] |
|
157 (fold_set_mono RS subsetD) 1); |
|
158 by Auto_tac; |
|
159 qed "fold_set_mono2"; |
|
160 |
|
161 |
|
162 Goalw [fold_def] |
|
163 "[| Finite(C); x ~: C; e:B |] \ |
|
164 \ ==> fold[B](f, e, cons(x, C)) = f(x, fold[B](f,e, C))"; |
|
165 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
|
166 by (dtac Finite_into_Fin 1); |
|
167 by (rtac the_equality 1); |
|
168 by (dtac Fin_imp_fold_set 1); |
|
169 by Auto_tac; |
|
170 by (res_inst_tac [("x", "xa")] exI 1); |
|
171 by Auto_tac; |
|
172 by (resolve_tac [fold_set_mono RS subsetD] 1); |
|
173 by (Blast_tac 2); |
|
174 by (dresolve_tac [fold_set_mono2] 3); |
|
175 by (auto_tac (claset() addIs [Fin_imp_fold_set], |
|
176 simpset() addsimps [symmetric fold_def, fold_equality])); |
|
177 qed "fold_cons"; |
|
178 |
|
179 |
|
180 Goal "Finite(C) \ |
|
181 \ ==> ALL e:B. f(x, fold[B](f, e, C)) = fold[B](f, f(x, e), C)"; |
|
182 by (etac Finite_induct 1); |
|
183 by (ALLGOALS(Clarify_tac)); |
|
184 by (asm_full_simp_tac (simpset() addsimps [f_type]) 1); |
|
185 by (asm_simp_tac (simpset() |
|
186 addsimps [f_lcomm, fold_cons, f_type]) 1); |
|
187 qed_spec_mp "fold_commute"; |
|
188 |
|
189 |
|
190 Goal "Finite(C) ==> e:B -->fold[B](f, e, C):B"; |
|
191 by (etac Finite_induct 1); |
|
192 by (ALLGOALS(Clarify_tac)); |
|
193 by (Asm_simp_tac 1); |
|
194 by (asm_simp_tac (simpset() addsimps [fold_cons, f_type]) 1); |
|
195 qed_spec_mp "fold_type"; |
|
196 |
|
197 Goal "x:D ==> cons(x, C) Int D = cons(x, C Int D)"; |
|
198 by Auto_tac; |
|
199 qed "cons_Int_right_lemma1"; |
|
200 |
|
201 Goal "x~:D ==> cons(x, C) Int D = C Int D"; |
|
202 by Auto_tac; |
|
203 qed "cons_Int_right_lemma2"; |
|
204 |
|
205 Goal "[| Finite(C); Finite(D); e:B|] \ |
|
206 \ ==> fold[B](f, fold[B](f, e, D), C) \ |
|
207 \ = fold[B](f, fold[B](f, e, (C Int D)), C Un D)"; |
|
208 by (etac Finite_induct 1); |
|
209 by (asm_full_simp_tac (simpset() addsimps [f_type, fold_type]) 1); |
|
210 by (subgoal_tac "Finite(Ba Int D) & \ |
|
211 \cons(x, Ba) Un D = cons(x, Ba Un D) & \ |
|
212 \Finite(Ba Un D)" 1); |
|
213 by (auto_tac (claset() |
|
214 addIs [Finite_Un,Int_lower1 RS subset_Finite], simpset())); |
|
215 by (case_tac "x:D" 1); |
|
216 by (ALLGOALS(asm_simp_tac (simpset() addsimps |
|
217 [cons_Int_right_lemma1,cons_Int_right_lemma2, |
|
218 fold_type, fold_cons,fold_commute,cons_absorb, f_type]))); |
|
219 qed "fold_nest_Un_Int"; |
|
220 |
|
221 |
|
222 Goal "[| Finite(C); Finite(D); C Int D = 0; e:B |] \ |
|
223 \ ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)"; |
|
224 by (asm_simp_tac (simpset() addsimps [fold_nest_Un_Int]) 1); |
|
225 qed "fold_nest_Un_disjoint"; |
|
226 |
|
227 Close_locale "LC"; |
|
228 |
|
229 |
|
230 (** setsum **) |
|
231 |
|
232 Goalw [setsum_def] "setsum(g, 0) = #0"; |
|
233 by (Simp_tac 1); |
|
234 qed "setsum_0"; |
|
235 Addsimps [setsum_0]; |
|
236 |
|
237 Goalw [setsum_def] |
|
238 "[| Finite(C); c~:C |] \ |
|
239 \ ==> setsum(g, cons(c, C)) = g(c) $+ setsum(g, C)"; |
|
240 by (asm_simp_tac (simpset() addsimps [Finite_cons,export fold_cons]) 1); |
|
241 qed "setsum_cons"; |
|
242 Addsimps [setsum_cons]; |
|
243 |
|
244 Goal "setsum((%i. #0), C) = #0"; |
|
245 by (case_tac "Finite(C)" 1); |
|
246 by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
247 by (etac Finite_induct 1); |
|
248 by Auto_tac; |
|
249 qed "setsum_0"; |
|
250 |
|
251 (*The reversed orientation looks more natural, but LOOPS as a simprule!*) |
|
252 Goal "[| Finite(C); Finite(D) |] \ |
|
253 \ ==> setsum(g, C Un D) $+ setsum(g, C Int D) \ |
|
254 \ = setsum(g, C) $+ setsum(g, D)"; |
|
255 by (etac Finite_induct 1); |
|
256 by (subgoal_tac "cons(x, B) Un D = cons(x, B Un D) & \ |
|
257 \ Finite(B Un D) & Finite(B Int D)" 2); |
|
258 by (auto_tac (claset() addIs [Finite_Un, Int_lower1 RS subset_Finite], |
|
259 simpset())); |
|
260 by (case_tac "x:D" 1); |
|
261 by (subgoal_tac "cons(x, B) Int D = B Int D" 2); |
|
262 by (subgoal_tac "cons(x, B) Int D = cons(x, B Int D)" 1); |
|
263 by Auto_tac; |
|
264 by (subgoal_tac "cons(x, B Un D) = B Un D" 1); |
|
265 by Auto_tac; |
|
266 qed "setsum_Un_Int"; |
|
267 |
|
268 Goal "setsum(g, C):int"; |
|
269 by (case_tac "Finite(C)" 1); |
|
270 by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
271 by (etac Finite_induct 1); |
|
272 by Auto_tac; |
|
273 qed "setsum_type"; |
|
274 Addsimps [setsum_type]; AddTCs [setsum_type]; |
|
275 |
|
276 Goal "[| Finite(C); Finite(D); C Int D = 0 |] \ |
|
277 \ ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"; |
|
278 by (stac (setsum_Un_Int RS sym) 1); |
|
279 by (subgoal_tac "Finite(C Un D)" 3); |
|
280 by (auto_tac (claset() addIs [Finite_Un], simpset())); |
|
281 qed "setsum_Un_disjoint"; |
|
282 |
|
283 Goal "Finite(I) ==> (ALL i:I. Finite(C(i))) --> Finite(RepFun(I, C))"; |
|
284 by (etac Finite_induct 1); |
|
285 by (auto_tac (claset(), simpset() addsimps [Finite_0])); |
|
286 by (stac (cons_eq RS sym) 1); |
|
287 by (auto_tac (claset() addIs [Finite_Un, Finite_cons, Finite_0], simpset())); |
|
288 qed_spec_mp "Finite_RepFun"; |
|
289 |
|
290 Goal "!!I. Finite(I) \ |
|
291 \ ==> (ALL i:I. Finite(C(i))) --> \ |
|
292 \ (ALL i:I. ALL j:I. i~=j --> C(i) Int C(j) = 0) --> \ |
|
293 \ setsum(f, UN i:I. C(i)) = setsum (%i. setsum(f, C(i)), I)"; |
|
294 by (etac Finite_induct 1); |
|
295 by (ALLGOALS(Clarify_tac)); |
|
296 by Auto_tac; |
|
297 by (subgoal_tac "ALL i:B. x ~= i" 1); |
|
298 by (Blast_tac 2); |
|
299 by (subgoal_tac "C(x) Int (UN i:B. C(i)) = 0" 1); |
|
300 by (Blast_tac 2); |
|
301 by (subgoal_tac "Finite(UN i:B. C(i)) & Finite(C(x)) & Finite(B)" 1); |
|
302 by (asm_simp_tac (simpset() addsimps [setsum_Un_disjoint]) 1); |
|
303 by (auto_tac (claset() addIs [Finite_Union, Finite_RepFun], simpset())); |
|
304 qed_spec_mp "setsum_UN_disjoint"; |
|
305 |
|
306 |
|
307 Goal "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)"; |
|
308 by (case_tac "Finite(C)" 1); |
|
309 by (asm_simp_tac (simpset() addsimps [setsum_def]) 2); |
|
310 by (etac Finite_induct 1); |
|
311 by Auto_tac; |
|
312 qed "setsum_addf"; |
|
313 |
|
314 |
|
315 val major::prems = Goal |
|
316 "[| A=B; !!x. x:B ==> f(x) = g(x) |] ==> \ |
|
317 \ setsum(f, A) = setsum(g, B)"; |
|
318 by (case_tac "Finite(B)" 1); |
|
319 by (asm_simp_tac (simpset() addsimps [setsum_def, major]) 2); |
|
320 by (subgoal_tac "ALL C. C <= B --> (ALL x:C. f(x) = g(x)) \ |
|
321 \ --> setsum(f,C) = setsum(g, C)" 1); |
|
322 by (cut_facts_tac [major] 1); |
|
323 by (asm_full_simp_tac (simpset() addsimps [major]@prems) 1); |
|
324 by (etac Finite_induct 1); |
|
325 by (ALLGOALS(Clarify_tac)); |
|
326 by (subgoal_tac "C=0" 1); |
|
327 by (Force_tac 1); |
|
328 by (Blast_tac 1); |
|
329 by (asm_full_simp_tac (simpset() addsimps [major,subset_cons_iff]@prems) 1); |
|
330 by Safe_tac; |
|
331 by (forward_tac [subset_Finite] 1); |
|
332 by (assume_tac 1); |
|
333 by (Blast_tac 1); |
|
334 by (forward_tac [subset_Finite] 1); |
|
335 by (assume_tac 1); |
|
336 by (subgoal_tac "C = cons(x, C - {x})" 1); |
|
337 by (Blast_tac 2); |
|
338 by (etac ssubst 1); |
|
339 by (dtac spec 1); |
|
340 by (mp_tac 1); |
|
341 by (asm_full_simp_tac (simpset() addsimps [Ball_def, major]@prems) 1); |
|
342 qed_spec_mp "setsum_cong"; |
|
343 |
|
344 (** For the natural numbers, we have subtraction **) |
|
345 |
|
346 Goal "[| Finite(A); Finite(B) |] \ |
|
347 \ ==> setsum(f, A Un B) = \ |
|
348 \ setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"; |
|
349 by (stac (setsum_Un_Int RS sym) 1); |
|
350 by Auto_tac; |
|
351 qed "setsum_Un"; |
|
352 |
|
353 |
|
354 Goal "Finite(A) ==> (ALL x:A. g(x) $<= #0) --> setsum(g, A) $<= #0"; |
|
355 by (etac Finite_induct 1); |
|
356 by (auto_tac (claset() addIs [zneg_or_0_add_zneg_or_0_imp_zneg_or_0], simpset())); |
|
357 qed_spec_mp "setsum_zneg_or_0"; |
|
358 |
|
359 Goal "Finite(A) \ |
|
360 \ ==> ALL n:nat. setsum(f,A) = $# succ(n) --> (EX a:A. #0 $< f(a))"; |
|
361 by (etac Finite_induct 1); |
|
362 by (auto_tac (claset(), simpset() |
|
363 delsimps [int_of_0, int_of_succ] |
|
364 addsimps [not_zless_iff_zle, int_of_0 RS sym])); |
|
365 by (subgoal_tac "setsum(f, B) $<= #0" 1); |
|
366 by (ALLGOALS(Asm_full_simp_tac)); |
|
367 by (blast_tac (claset() addIs [setsum_zneg_or_0]) 2); |
|
368 by (subgoal_tac "$# 1 $<= f(x) $+ setsum(f, B)" 1); |
|
369 by (dtac (zdiff_zle_iff RS iffD2) 1); |
|
370 by (subgoal_tac "$# 1 $<= $# 1 $- setsum(f,B)" 1); |
|
371 by (dres_inst_tac [("x", "$# 1")] zle_trans 1); |
|
372 by (res_inst_tac [("j", "#1")] zless_zle_trans 2); |
|
373 by Auto_tac; |
|
374 qed "setsum_succD_lemma"; |
|
375 |
|
376 Goal "[| setsum(f, A) = $# succ(n); n:nat |]==> EX a:A. #0 $< f(a)"; |
|
377 by (case_tac "Finite(A)" 1); |
|
378 by (blast_tac (claset() |
|
379 addIs [setsum_succD_lemma RS bspec RS mp]) 1); |
|
380 by (rewrite_goals_tac [setsum_def]); |
|
381 by (auto_tac (claset(), |
|
382 simpset() delsimps [int_of_0, int_of_succ] |
|
383 addsimps [int_succ_int_1 RS sym, int_of_0 RS sym])); |
|
384 qed "setsum_succD"; |
|
385 |
|
386 Goal "Finite(A) ==> (ALL x:A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"; |
|
387 by (etac Finite_induct 1); |
|
388 by (Simp_tac 1); |
|
389 by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset())); |
|
390 qed_spec_mp "g_zpos_imp_setsum_zpos"; |
|
391 |
|
392 Goal "[| Finite(A); ALL x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)"; |
|
393 by (etac Finite_induct 1); |
|
394 by (auto_tac (claset() addIs [zpos_add_zpos_imp_zpos], simpset())); |
|
395 qed_spec_mp "g_zpos_imp_setsum_zpos2"; |
|
396 |
|
397 Goal "Finite(A) \ |
|
398 \ ==> (ALL x:A. #0 $< g(x)) --> A ~= 0 --> (#0 $< setsum(g, A))"; |
|
399 by (etac Finite_induct 1); |
|
400 by (auto_tac (claset() addIs [zspos_add_zspos_imp_zspos],simpset())); |
|
401 qed_spec_mp "g_zspos_imp_setsum_zspos"; |
|
402 |
|
403 Goal "Finite(A) \ |
|
404 \ ==> ALL a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"; |
|
405 by (etac Finite_induct 1); |
|
406 by (ALLGOALS(Clarify_tac)); |
|
407 by (Simp_tac 1); |
|
408 by (case_tac "x=a" 1); |
|
409 by (subgoal_tac "cons(x, B) - {a} = cons(x, B -{a}) & Finite(B - {a})" 2); |
|
410 by (subgoal_tac "cons(a, B) - {a} = B" 1); |
|
411 by (auto_tac (claset() addIs [Finite_Diff], simpset())); |
|
412 qed_spec_mp "setsum_Diff"; |