6 A "fold" functional for finite sets. For n non-negative we have |
6 A "fold" functional for finite sets. For n non-negative we have |
7 fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at |
7 fold f e {x1,...,xn} = f x1 (... (f xn e)) where f is at |
8 least left-commutative. |
8 least left-commutative. |
9 *) |
9 *) |
10 |
10 |
11 FoldSet = Main + |
11 theory FoldSet = Main: |
12 |
12 |
13 consts fold_set :: "[i, i, [i,i]=>i, i] => i" |
13 consts fold_set :: "[i, i, [i,i]=>i, i] => i" |
14 |
14 |
15 inductive |
15 inductive |
16 domains "fold_set(A, B, f,e)" <= "Fin(A)*B" |
16 domains "fold_set(A, B, f,e)" <= "Fin(A)*B" |
17 intrs |
17 intros |
18 emptyI "e:B ==> <0, e>:fold_set(A, B, f,e)" |
18 emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)" |
19 consI "[| x:A; x ~:C; <C,y> : fold_set(A, B,f,e); f(x,y):B |] |
19 consI: "[| x\<in>A; x \<notin>C; <C,y> : fold_set(A, B,f,e); f(x,y):B |] |
20 ==> <cons(x,C), f(x,y)>:fold_set(A, B, f, e)" |
20 ==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)" |
21 type_intrs "Fin_intros" |
21 type_intros Fin.intros |
22 |
22 |
23 constdefs |
23 constdefs |
24 |
24 |
25 fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") |
25 fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") |
26 "fold[B](f,e, A) == THE x. <A, x>:fold_set(A, B, f,e)" |
26 "fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)" |
27 |
27 |
28 setsum :: "[i=>i, i] => i" |
28 setsum :: "[i=>i, i] => i" |
29 "setsum(g, C) == if Finite(C) then |
29 "setsum(g, C) == if Finite(C) then |
30 fold[int](%x y. g(x) $+ y, #0, C) else #0" |
30 fold[int](%x y. g(x) $+ y, #0, C) else #0" |
|
31 |
|
32 (** foldSet **) |
|
33 |
|
34 inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)" |
|
35 inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)" |
|
36 |
|
37 (* add-hoc lemmas *) |
|
38 |
|
39 lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C" |
|
40 by (auto elim: equalityE) |
|
41 |
|
42 lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |] |
|
43 ==> B - {y} = C-{x} & x\<in>C & y\<in>B" |
|
44 apply (auto elim: equalityE) |
|
45 done |
|
46 |
|
47 (* fold_set monotonicity *) |
|
48 lemma fold_set_mono_lemma: |
|
49 "<C, x> : fold_set(A, B, f, e) |
|
50 ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)" |
|
51 apply (erule fold_set.induct) |
|
52 apply (auto intro: fold_set.intros) |
|
53 done |
|
54 |
|
55 lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)" |
|
56 apply clarify |
|
57 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
|
58 apply (auto dest: fold_set_mono_lemma) |
|
59 done |
|
60 |
|
61 lemma fold_set_lemma: |
|
62 "<C, x>\<in>fold_set(A, B, f, e) ==> <C, x>\<in>fold_set(C, B, f, e) & C<=A" |
|
63 apply (erule fold_set.induct) |
|
64 apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD]) |
|
65 done |
|
66 |
|
67 (* Proving that fold_set is deterministic *) |
|
68 lemma Diff1_fold_set: |
|
69 "[| <C-{x},y> : fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |] |
|
70 ==> <C, f(x, y)> : fold_set(A, B, f, e)" |
|
71 apply (frule fold_set.dom_subset [THEN subsetD]) |
|
72 apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto) |
|
73 done |
|
74 |
|
75 |
|
76 locale fold_typing = |
|
77 fixes A and B and e and f |
|
78 assumes ftype [intro,simp]: "[|x \<in> A; y \<in> B|] ==> f(x,y) \<in> B" |
|
79 and etype [intro,simp]: "e \<in> B" |
|
80 and fcomm: "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))" |
|
81 |
|
82 |
|
83 lemma (in fold_typing) Fin_imp_fold_set: |
|
84 "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))" |
|
85 apply (erule Fin_induct) |
|
86 apply (auto dest: fold_set.dom_subset [THEN subsetD] |
|
87 intro: fold_set.intros etype ftype) |
|
88 done |
|
89 |
|
90 lemma Diff_sing_imp: |
|
91 "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}" |
|
92 by (blast elim: equalityE) |
|
93 |
|
94 lemma (in fold_typing) fold_set_determ_lemma [rule_format]: |
|
95 "n\<in>nat |
|
96 ==> ALL C. |C|<n --> |
|
97 (ALL x. <C, x> : fold_set(A, B, f,e)--> |
|
98 (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))" |
|
99 apply (erule nat_induct) |
|
100 apply (auto simp add: le_iff) |
|
101 apply (erule fold_set.cases) |
|
102 apply (force elim!: empty_fold_setE) |
|
103 apply (erule fold_set.cases) |
|
104 apply (force elim!: empty_fold_setE, clarify) |
|
105 (*force simplification of "|C| < |cons(...)|"*) |
|
106 apply (frule_tac a = Ca in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
|
107 apply (frule_tac a = Cb in fold_set.dom_subset [THEN subsetD, THEN SigmaD1]) |
|
108 apply (simp add: Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
|
109 apply (case_tac "x=xb", auto) |
|
110 apply (simp add: cons_lemma1, blast) |
|
111 txt{*case @{term "x\<noteq>xb"}*} |
|
112 apply (drule cons_lemma2, safe) |
|
113 apply (frule Diff_sing_imp, assumption+) |
|
114 txt{** LEVEL 17*} |
|
115 apply (subgoal_tac "|Ca| le |Cb|") |
|
116 prefer 2 |
|
117 apply (rule succ_le_imp_le) |
|
118 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff |
|
119 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
|
120 apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) |
|
121 apply (blast intro: Diff_subset [THEN Fin_subset]) |
|
122 txt{** LEVEL 24 **} |
|
123 apply (frule Diff1_fold_set, blast, blast) |
|
124 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) |
|
125 apply (subgoal_tac "ya = f(xb,xa) ") |
|
126 prefer 2 apply (blast del: equalityCE) |
|
127 apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)") |
|
128 prefer 2 apply simp |
|
129 apply (subgoal_tac "yb = f (x, xa) ") |
|
130 apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all) |
|
131 apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD]) |
|
132 apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) |
|
133 done |
|
134 |
|
135 lemma (in fold_typing) fold_set_determ: |
|
136 "[| <C, x>\<in>fold_set(A, B, f, e); |
|
137 <C, y>\<in>fold_set(A, B, f, e)|] ==> y=x" |
|
138 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
|
139 apply (drule Fin_into_Finite) |
|
140 apply (unfold Finite_def, clarify) |
|
141 apply (rule_tac n = "succ (n)" in fold_set_determ_lemma) |
|
142 apply (auto intro: eqpoll_imp_lepoll [THEN lepoll_cardinal_le]) |
|
143 done |
|
144 |
|
145 (** The fold function **) |
|
146 |
|
147 lemma (in fold_typing) fold_equality: |
|
148 "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y" |
|
149 apply (unfold fold_def) |
|
150 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
|
151 apply (rule the_equality) |
|
152 apply (rule_tac [2] A=C in fold_typing.fold_set_determ) |
|
153 apply (force dest: fold_set_lemma) |
|
154 apply (auto dest: fold_set_lemma) |
|
155 apply (simp add: fold_typing_def, auto) |
|
156 apply (auto dest: fold_set_lemma intro: ftype etype fcomm) |
|
157 done |
|
158 |
|
159 lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e" |
|
160 apply (unfold fold_def) |
|
161 apply (blast elim!: empty_fold_setE intro: fold_set.intros) |
|
162 done |
|
163 |
|
164 text{*This result is the right-to-left direction of the subsequent result*} |
|
165 lemma (in fold_typing) fold_set_imp_cons: |
|
166 "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |] |
|
167 ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)" |
|
168 apply (frule FinD [THEN fold_set_mono, THEN subsetD]) |
|
169 apply assumption |
|
170 apply (frule fold_set.dom_subset [of A, THEN subsetD]) |
|
171 apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD]) |
|
172 done |
|
173 |
|
174 lemma (in fold_typing) fold_cons_lemma [rule_format]: |
|
175 "[| C : Fin(A); c : A; c\<notin>C |] |
|
176 ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <-> |
|
177 (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))" |
|
178 apply auto |
|
179 prefer 2 apply (blast intro: fold_set_imp_cons) |
|
180 apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+) |
|
181 apply (frule_tac fold_set.dom_subset [of A, THEN subsetD]) |
|
182 apply (drule FinD) |
|
183 apply (rule_tac A1 = "cons(c,C)" and f1=f and B1=B and C1=C and e1=e in fold_typing.Fin_imp_fold_set [THEN exE]) |
|
184 apply (blast intro: fold_typing.intro ftype etype fcomm) |
|
185 apply (blast intro: Fin_subset [of _ "cons(c,C)"] Finite_into_Fin |
|
186 dest: Fin_into_Finite) |
|
187 apply (rule_tac x = x in exI) |
|
188 apply (auto intro: fold_set.intros) |
|
189 apply (drule_tac fold_set_lemma [of C], blast) |
|
190 apply (blast intro!: fold_set.consI |
|
191 intro: fold_set_determ fold_set_mono [THEN subsetD] |
|
192 dest: fold_set.dom_subset [THEN subsetD]) |
|
193 done |
|
194 |
|
195 lemma (in fold_typing) fold_cons: |
|
196 "[| C\<in>Fin(A); c\<in>A; c\<notin>C|] |
|
197 ==> fold[B](f, e, cons(c, C)) = f(c, fold[B](f, e, C))" |
|
198 apply (unfold fold_def) |
|
199 apply (simp add: fold_cons_lemma) |
|
200 apply (rule the_equality, auto) |
|
201 apply (subgoal_tac [2] "\<langle>C, y\<rangle> \<in> fold_set(A, B, f, e)") |
|
202 apply (drule Fin_imp_fold_set) |
|
203 apply (auto dest: fold_set_lemma simp add: fold_def [symmetric] fold_equality) |
|
204 apply (blast intro: fold_set_mono [THEN subsetD] dest!: FinD) |
|
205 done |
|
206 |
|
207 lemma (in fold_typing) fold_type [simp,TC]: |
|
208 "C\<in>Fin(A) ==> fold[B](f,e,C):B" |
|
209 apply (erule Fin_induct) |
|
210 apply (simp_all add: fold_cons ftype etype) |
|
211 done |
|
212 |
|
213 lemma (in fold_typing) fold_commute [rule_format]: |
|
214 "[| C\<in>Fin(A); c\<in>A |] |
|
215 ==> (\<forall>y\<in>B. f(c, fold[B](f, y, C)) = fold[B](f, f(c, y), C))" |
|
216 apply (erule Fin_induct) |
|
217 apply (simp_all add: fold_typing.fold_cons [of A B _ f] |
|
218 fold_typing.fold_type [of A B _ f] |
|
219 fold_typing_def fcomm) |
|
220 done |
|
221 |
|
222 lemma (in fold_typing) fold_nest_Un_Int: |
|
223 "[| C\<in>Fin(A); D\<in>Fin(A) |] |
|
224 ==> fold[B](f, fold[B](f, e, D), C) = |
|
225 fold[B](f, fold[B](f, e, (C Int D)), C Un D)" |
|
226 apply (erule Fin_induct, auto) |
|
227 apply (simp add: Un_cons Int_cons_left fold_type fold_commute |
|
228 fold_typing.fold_cons [of A _ _ f] |
|
229 fold_typing_def fcomm cons_absorb) |
|
230 done |
|
231 |
|
232 lemma (in fold_typing) fold_nest_Un_disjoint: |
|
233 "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |] |
|
234 ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)" |
|
235 by (simp add: fold_nest_Un_Int) |
|
236 |
|
237 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" |
|
238 apply (drule Finite_into_Fin) |
|
239 apply (blast intro: Fin_mono [THEN subsetD]) |
|
240 done |
|
241 |
|
242 subsection{*The Operator @{term setsum}*} |
|
243 |
|
244 lemma setsum_0 [simp]: "setsum(g, 0) = #0" |
|
245 by (simp add: setsum_def) |
|
246 |
|
247 lemma setsum_cons [simp]: |
|
248 "Finite(C) ==> |
|
249 setsum(g, cons(c,C)) = |
|
250 (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))" |
|
251 apply (auto simp add: setsum_def Finite_cons cons_absorb) |
|
252 apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons) |
|
253 apply (auto intro: fold_typing.intro Finite_cons_lemma) |
|
254 done |
|
255 |
|
256 lemma setsum_K0: "setsum((%i. #0), C) = #0" |
|
257 apply (case_tac "Finite (C) ") |
|
258 prefer 2 apply (simp add: setsum_def) |
|
259 apply (erule Finite_induct, auto) |
|
260 done |
|
261 |
|
262 (*The reversed orientation looks more natural, but LOOPS as a simprule!*) |
|
263 lemma setsum_Un_Int: |
|
264 "[| Finite(C); Finite(D) |] |
|
265 ==> setsum(g, C Un D) $+ setsum(g, C Int D) |
|
266 = setsum(g, C) $+ setsum(g, D)" |
|
267 apply (erule Finite_induct) |
|
268 apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un |
|
269 Int_lower1 [THEN subset_Finite]) |
|
270 done |
|
271 |
|
272 lemma setsum_type [simp,TC]: "setsum(g, C):int" |
|
273 apply (case_tac "Finite (C) ") |
|
274 prefer 2 apply (simp add: setsum_def) |
|
275 apply (erule Finite_induct, auto) |
|
276 done |
|
277 |
|
278 lemma setsum_Un_disjoint: |
|
279 "[| Finite(C); Finite(D); C Int D = 0 |] |
|
280 ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)" |
|
281 apply (subst setsum_Un_Int [symmetric]) |
|
282 apply (subgoal_tac [3] "Finite (C Un D) ") |
|
283 apply (auto intro: Finite_Un) |
|
284 done |
|
285 |
|
286 lemma Finite_RepFun [rule_format (no_asm)]: |
|
287 "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))" |
|
288 apply (erule Finite_induct, auto) |
|
289 done |
|
290 |
|
291 lemma setsum_UN_disjoint [rule_format (no_asm)]: |
|
292 "Finite(I) |
|
293 ==> (\<forall>i\<in>I. Finite(C(i))) --> |
|
294 (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) --> |
|
295 setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)" |
|
296 apply (erule Finite_induct, auto) |
|
297 apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i") |
|
298 prefer 2 apply blast |
|
299 apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0") |
|
300 prefer 2 apply blast |
|
301 apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ") |
|
302 apply (simp (no_asm_simp) add: setsum_Un_disjoint) |
|
303 apply (auto intro: Finite_Union Finite_RepFun) |
|
304 done |
|
305 |
|
306 |
|
307 lemma setsum_addf: "setsum(%x. f(x) $+ g(x),C) = setsum(f, C) $+ setsum(g, C)" |
|
308 apply (case_tac "Finite (C) ") |
|
309 prefer 2 apply (simp add: setsum_def) |
|
310 apply (erule Finite_induct, auto) |
|
311 done |
|
312 |
|
313 |
|
314 lemma fold_set_cong: |
|
315 "[| A=A'; B=B'; e=e'; (\<forall>x\<in>A'. \<forall>y\<in>B'. f(x,y) = f'(x,y)) |] |
|
316 ==> fold_set(A,B,f,e) = fold_set(A',B',f',e')" |
|
317 apply (simp add: fold_set_def) |
|
318 apply (intro refl iff_refl lfp_cong Collect_cong disj_cong ex_cong, auto) |
|
319 done |
|
320 |
|
321 lemma fold_cong: |
|
322 "[| B=B'; A=A'; e=e'; |
|
323 !!x y. [|x\<in>A'; y\<in>B'|] ==> f(x,y) = f'(x,y) |] ==> |
|
324 fold[B](f,e,A) = fold[B'](f', e', A')" |
|
325 apply (simp add: fold_def) |
|
326 apply (subst fold_set_cong) |
|
327 apply (rule_tac [5] refl, simp_all) |
|
328 done |
|
329 |
|
330 lemma setsum_cong: |
|
331 "[| A=B; !!x. x\<in>B ==> f(x) = g(x) |] ==> |
|
332 setsum(f, A) = setsum(g, B)" |
|
333 by (simp add: setsum_def cong add: fold_cong) |
|
334 |
|
335 lemma setsum_Un: |
|
336 "[| Finite(A); Finite(B) |] |
|
337 ==> setsum(f, A Un B) = |
|
338 setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)" |
|
339 apply (subst setsum_Un_Int [symmetric], auto) |
|
340 done |
|
341 |
|
342 |
|
343 lemma setsum_zneg_or_0 [rule_format (no_asm)]: |
|
344 "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0" |
|
345 apply (erule Finite_induct) |
|
346 apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0) |
|
347 done |
|
348 |
|
349 lemma setsum_succD_lemma [rule_format]: |
|
350 "Finite(A) |
|
351 ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))" |
|
352 apply (erule Finite_induct) |
|
353 apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric]) |
|
354 apply (subgoal_tac "setsum (f, B) $<= #0") |
|
355 apply simp_all |
|
356 prefer 2 apply (blast intro: setsum_zneg_or_0) |
|
357 apply (subgoal_tac "$# 1 $<= f (x) $+ setsum (f, B) ") |
|
358 apply (drule zdiff_zle_iff [THEN iffD2]) |
|
359 apply (subgoal_tac "$# 1 $<= $# 1 $- setsum (f,B) ") |
|
360 apply (drule_tac x = "$# 1" in zle_trans) |
|
361 apply (rule_tac [2] j = "#1" in zless_zle_trans, auto) |
|
362 done |
|
363 |
|
364 lemma setsum_succD: |
|
365 "[| setsum(f, A) = $# succ(n); n\<in>nat |]==> \<exists>a\<in>A. #0 $< f(a)" |
|
366 apply (case_tac "Finite (A) ") |
|
367 apply (blast intro: setsum_succD_lemma) |
|
368 apply (unfold setsum_def) |
|
369 apply (auto simp del: int_of_0 int_of_succ simp add: int_succ_int_1 [symmetric] int_of_0 [symmetric]) |
|
370 done |
|
371 |
|
372 lemma g_zpos_imp_setsum_zpos [rule_format]: |
|
373 "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)" |
|
374 apply (erule Finite_induct) |
|
375 apply (simp (no_asm)) |
|
376 apply (auto intro: zpos_add_zpos_imp_zpos) |
|
377 done |
|
378 |
|
379 lemma g_zpos_imp_setsum_zpos2 [rule_format]: |
|
380 "[| Finite(A); \<forall>x. #0 $<= g(x) |] ==> #0 $<= setsum(g, A)" |
|
381 apply (erule Finite_induct) |
|
382 apply (auto intro: zpos_add_zpos_imp_zpos) |
|
383 done |
|
384 |
|
385 lemma g_zspos_imp_setsum_zspos [rule_format]: |
|
386 "Finite(A) |
|
387 ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))" |
|
388 apply (erule Finite_induct) |
|
389 apply (auto intro: zspos_add_zspos_imp_zspos) |
|
390 done |
|
391 |
|
392 lemma setsum_Diff [rule_format]: |
|
393 "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})" |
|
394 apply (erule Finite_induct) |
|
395 apply (simp_all add: Diff_cons_eq Finite_Diff) |
|
396 done |
|
397 |
|
398 ML |
|
399 {* |
|
400 val fold_set_mono = thm "fold_set_mono"; |
|
401 val Diff1_fold_set = thm "Diff1_fold_set"; |
|
402 val Diff_sing_imp = thm "Diff_sing_imp"; |
|
403 val fold_0 = thm "fold_0"; |
|
404 val setsum_0 = thm "setsum_0"; |
|
405 val setsum_cons = thm "setsum_cons"; |
|
406 val setsum_K0 = thm "setsum_K0"; |
|
407 val setsum_Un_Int = thm "setsum_Un_Int"; |
|
408 val setsum_type = thm "setsum_type"; |
|
409 val setsum_Un_disjoint = thm "setsum_Un_disjoint"; |
|
410 val Finite_RepFun = thm "Finite_RepFun"; |
|
411 val setsum_UN_disjoint = thm "setsum_UN_disjoint"; |
|
412 val setsum_addf = thm "setsum_addf"; |
|
413 val fold_set_cong = thm "fold_set_cong"; |
|
414 val fold_cong = thm "fold_cong"; |
|
415 val setsum_cong = thm "setsum_cong"; |
|
416 val setsum_Un = thm "setsum_Un"; |
|
417 val setsum_zneg_or_0 = thm "setsum_zneg_or_0"; |
|
418 val setsum_succD = thm "setsum_succD"; |
|
419 val g_zpos_imp_setsum_zpos = thm "g_zpos_imp_setsum_zpos"; |
|
420 val g_zpos_imp_setsum_zpos2 = thm "g_zpos_imp_setsum_zpos2"; |
|
421 val g_zspos_imp_setsum_zspos = thm "g_zspos_imp_setsum_zspos"; |
|
422 val setsum_Diff = thm "setsum_Diff"; |
|
423 *} |
|
424 |
|
425 |
31 end |
426 end |