9 theory FoldSet imports Main begin |
9 theory FoldSet imports Main begin |
10 |
10 |
11 consts fold_set :: "[i, i, [i,i]=>i, i] => i" |
11 consts fold_set :: "[i, i, [i,i]=>i, i] => i" |
12 |
12 |
13 inductive |
13 inductive |
14 domains "fold_set(A, B, f,e)" <= "Fin(A)*B" |
14 domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B" |
15 intros |
15 intros |
16 emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)" |
16 emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)" |
17 consI: "[| x\<in>A; x \<notin>C; <C,y> : fold_set(A, B,f,e); f(x,y):B |] |
17 consI: "[| x\<in>A; x \<notin>C; <C,y> \<in> fold_set(A, B,f,e); f(x,y):B |] |
18 ==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)" |
18 ==> <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)" |
19 type_intros Fin.intros |
19 type_intros Fin.intros |
20 |
20 |
21 definition |
21 definition |
22 fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") where |
22 fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") where |
27 "setsum(g, C) == if Finite(C) then |
27 "setsum(g, C) == if Finite(C) then |
28 fold[int](%x y. g(x) $+ y, #0, C) else #0" |
28 fold[int](%x y. g(x) $+ y, #0, C) else #0" |
29 |
29 |
30 (** foldSet **) |
30 (** foldSet **) |
31 |
31 |
32 inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)" |
32 inductive_cases empty_fold_setE: "<0, x> \<in> fold_set(A, B, f,e)" |
33 inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)" |
33 inductive_cases cons_fold_setE: "<cons(x,C), y> \<in> fold_set(A, B, f,e)" |
34 |
34 |
35 (* add-hoc lemmas *) |
35 (* add-hoc lemmas *) |
36 |
36 |
37 lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C" |
37 lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) \<longleftrightarrow> B = C" |
38 by (auto elim: equalityE) |
38 by (auto elim: equalityE) |
39 |
39 |
40 lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |] |
40 lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |] |
41 ==> B - {y} = C-{x} & x\<in>C & y\<in>B" |
41 ==> B - {y} = C-{x} & x\<in>C & y\<in>B" |
42 apply (auto elim: equalityE) |
42 apply (auto elim: equalityE) |
43 done |
43 done |
44 |
44 |
45 (* fold_set monotonicity *) |
45 (* fold_set monotonicity *) |
46 lemma fold_set_mono_lemma: |
46 lemma fold_set_mono_lemma: |
47 "<C, x> : fold_set(A, B, f, e) |
47 "<C, x> \<in> fold_set(A, B, f, e) |
48 ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)" |
48 ==> \<forall>D. A<=D \<longrightarrow> <C, x> \<in> fold_set(D, B, f, e)" |
49 apply (erule fold_set.induct) |
49 apply (erule fold_set.induct) |
50 apply (auto intro: fold_set.intros) |
50 apply (auto intro: fold_set.intros) |
51 done |
51 done |
52 |
52 |
53 lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)" |
53 lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) \<subseteq> fold_set(A, B, f, e)" |
54 apply clarify |
54 apply clarify |
55 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
55 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
56 apply (auto dest: fold_set_mono_lemma) |
56 apply (auto dest: fold_set_mono_lemma) |
57 done |
57 done |
58 |
58 |
62 apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD]) |
62 apply (auto intro!: fold_set.intros intro: fold_set_mono [THEN subsetD]) |
63 done |
63 done |
64 |
64 |
65 (* Proving that fold_set is deterministic *) |
65 (* Proving that fold_set is deterministic *) |
66 lemma Diff1_fold_set: |
66 lemma Diff1_fold_set: |
67 "[| <C-{x},y> : fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |] |
67 "[| <C-{x},y> \<in> fold_set(A, B, f,e); x\<in>C; x\<in>A; f(x, y):B |] |
68 ==> <C, f(x, y)> : fold_set(A, B, f, e)" |
68 ==> <C, f(x, y)> \<in> fold_set(A, B, f, e)" |
69 apply (frule fold_set.dom_subset [THEN subsetD]) |
69 apply (frule fold_set.dom_subset [THEN subsetD]) |
70 apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto) |
70 apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto) |
71 done |
71 done |
72 |
72 |
73 |
73 |
77 and etype [intro,simp]: "e \<in> B" |
77 and etype [intro,simp]: "e \<in> B" |
78 and fcomm: "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))" |
78 and fcomm: "[|x \<in> A; y \<in> A; z \<in> B|] ==> f(x, f(y, z))=f(y, f(x, z))" |
79 |
79 |
80 |
80 |
81 lemma (in fold_typing) Fin_imp_fold_set: |
81 lemma (in fold_typing) Fin_imp_fold_set: |
82 "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))" |
82 "C\<in>Fin(A) ==> (\<exists>x. <C, x> \<in> fold_set(A, B, f,e))" |
83 apply (erule Fin_induct) |
83 apply (erule Fin_induct) |
84 apply (auto dest: fold_set.dom_subset [THEN subsetD] |
84 apply (auto dest: fold_set.dom_subset [THEN subsetD] |
85 intro: fold_set.intros etype ftype) |
85 intro: fold_set.intros etype ftype) |
86 done |
86 done |
87 |
87 |
89 "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}" |
89 "[|C - {b} = D - {a}; a \<noteq> b; b \<in> C|] ==> C = cons(b,D) - {a}" |
90 by (blast elim: equalityE) |
90 by (blast elim: equalityE) |
91 |
91 |
92 lemma (in fold_typing) fold_set_determ_lemma [rule_format]: |
92 lemma (in fold_typing) fold_set_determ_lemma [rule_format]: |
93 "n\<in>nat |
93 "n\<in>nat |
94 ==> ALL C. |C|<n --> |
94 ==> \<forall>C. |C|<n \<longrightarrow> |
95 (ALL x. <C, x> : fold_set(A, B, f,e)--> |
95 (\<forall>x. <C, x> \<in> fold_set(A, B, f,e)\<longrightarrow> |
96 (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))" |
96 (\<forall>y. <C, y> \<in> fold_set(A, B, f,e) \<longrightarrow> y=x))" |
97 apply (erule nat_induct) |
97 apply (erule nat_induct) |
98 apply (auto simp add: le_iff) |
98 apply (auto simp add: le_iff) |
99 apply (erule fold_set.cases) |
99 apply (erule fold_set.cases) |
100 apply (force elim!: empty_fold_setE) |
100 apply (force elim!: empty_fold_setE) |
101 apply (erule fold_set.cases) |
101 apply (erule fold_set.cases) |
108 apply (simp add: cons_lemma1, blast) |
108 apply (simp add: cons_lemma1, blast) |
109 txt{*case @{term "x\<noteq>xb"}*} |
109 txt{*case @{term "x\<noteq>xb"}*} |
110 apply (drule cons_lemma2, safe) |
110 apply (drule cons_lemma2, safe) |
111 apply (frule Diff_sing_imp, assumption+) |
111 apply (frule Diff_sing_imp, assumption+) |
112 txt{** LEVEL 17*} |
112 txt{** LEVEL 17*} |
113 apply (subgoal_tac "|Ca| le |Cb|") |
113 apply (subgoal_tac "|Ca| \<le> |Cb|") |
114 prefer 2 |
114 prefer 2 |
115 apply (rule succ_le_imp_le) |
115 apply (rule succ_le_imp_le) |
116 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff |
116 apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff |
117 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
117 Fin_into_Finite [THEN Finite_imp_cardinal_cons]) |
118 apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) |
118 apply (rule_tac C1 = "Ca-{xb}" in Fin_imp_fold_set [THEN exE]) |
120 txt{** LEVEL 24 **} |
120 txt{** LEVEL 24 **} |
121 apply (frule Diff1_fold_set, blast, blast) |
121 apply (frule Diff1_fold_set, blast, blast) |
122 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) |
122 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD]) |
123 apply (subgoal_tac "ya = f(xb,xa) ") |
123 apply (subgoal_tac "ya = f(xb,xa) ") |
124 prefer 2 apply (blast del: equalityCE) |
124 prefer 2 apply (blast del: equalityCE) |
125 apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)") |
125 apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)") |
126 prefer 2 apply simp |
126 prefer 2 apply simp |
127 apply (subgoal_tac "yb = f (x, xa) ") |
127 apply (subgoal_tac "yb = f (x, xa) ") |
128 apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all) |
128 apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all) |
129 apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD]) |
129 apply (blast intro: fcomm dest!: fold_set.dom_subset [THEN subsetD]) |
130 apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) |
130 apply (blast intro: ftype dest!: fold_set.dom_subset [THEN subsetD], blast) |
141 done |
141 done |
142 |
142 |
143 (** The fold function **) |
143 (** The fold function **) |
144 |
144 |
145 lemma (in fold_typing) fold_equality: |
145 lemma (in fold_typing) fold_equality: |
146 "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y" |
146 "<C,y> \<in> fold_set(A,B,f,e) ==> fold[B](f,e,C) = y" |
147 apply (unfold fold_def) |
147 apply (unfold fold_def) |
148 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
148 apply (frule fold_set.dom_subset [THEN subsetD], clarify) |
149 apply (rule the_equality) |
149 apply (rule the_equality) |
150 apply (rule_tac [2] A=C in fold_typing.fold_set_determ) |
150 apply (rule_tac [2] A=C in fold_typing.fold_set_determ) |
151 apply (force dest: fold_set_lemma) |
151 apply (force dest: fold_set_lemma) |
152 apply (auto dest: fold_set_lemma) |
152 apply (auto dest: fold_set_lemma) |
153 apply (simp add: fold_typing_def, auto) |
153 apply (simp add: fold_typing_def, auto) |
154 apply (auto dest: fold_set_lemma intro: ftype etype fcomm) |
154 apply (auto dest: fold_set_lemma intro: ftype etype fcomm) |
155 done |
155 done |
156 |
156 |
157 lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e" |
157 lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e" |
158 apply (unfold fold_def) |
158 apply (unfold fold_def) |
159 apply (blast elim!: empty_fold_setE intro: fold_set.intros) |
159 apply (blast elim!: empty_fold_setE intro: fold_set.intros) |
160 done |
160 done |
161 |
161 |
162 text{*This result is the right-to-left direction of the subsequent result*} |
162 text{*This result is the right-to-left direction of the subsequent result*} |
163 lemma (in fold_typing) fold_set_imp_cons: |
163 lemma (in fold_typing) fold_set_imp_cons: |
164 "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |] |
164 "[| <C, y> \<in> fold_set(C, B, f, e); C \<in> Fin(A); c \<in> A; c\<notin>C |] |
165 ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)" |
165 ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)" |
166 apply (frule FinD [THEN fold_set_mono, THEN subsetD]) |
166 apply (frule FinD [THEN fold_set_mono, THEN subsetD]) |
167 apply assumption |
167 apply assumption |
168 apply (frule fold_set.dom_subset [of A, THEN subsetD]) |
168 apply (frule fold_set.dom_subset [of A, THEN subsetD]) |
169 apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD]) |
169 apply (blast intro!: fold_set.consI intro: fold_set_mono [THEN subsetD]) |
170 done |
170 done |
171 |
171 |
172 lemma (in fold_typing) fold_cons_lemma [rule_format]: |
172 lemma (in fold_typing) fold_cons_lemma [rule_format]: |
173 "[| C : Fin(A); c : A; c\<notin>C |] |
173 "[| C \<in> Fin(A); c \<in> A; c\<notin>C |] |
174 ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <-> |
174 ==> <cons(c, C), v> \<in> fold_set(cons(c, C), B, f, e) \<longleftrightarrow> |
175 (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))" |
175 (\<exists>y. <C, y> \<in> fold_set(C, B, f, e) & v = f(c, y))" |
176 apply auto |
176 apply auto |
177 prefer 2 apply (blast intro: fold_set_imp_cons) |
177 prefer 2 apply (blast intro: fold_set_imp_cons) |
178 apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+) |
178 apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+) |
179 apply (frule_tac fold_set.dom_subset [of A, THEN subsetD]) |
179 apply (frule_tac fold_set.dom_subset [of A, THEN subsetD]) |
180 apply (drule FinD) |
180 apply (drule FinD) |
218 done |
218 done |
219 |
219 |
220 lemma (in fold_typing) fold_nest_Un_Int: |
220 lemma (in fold_typing) fold_nest_Un_Int: |
221 "[| C\<in>Fin(A); D\<in>Fin(A) |] |
221 "[| C\<in>Fin(A); D\<in>Fin(A) |] |
222 ==> fold[B](f, fold[B](f, e, D), C) = |
222 ==> fold[B](f, fold[B](f, e, D), C) = |
223 fold[B](f, fold[B](f, e, (C Int D)), C Un D)" |
223 fold[B](f, fold[B](f, e, (C \<inter> D)), C \<union> D)" |
224 apply (erule Fin_induct, auto) |
224 apply (erule Fin_induct, auto) |
225 apply (simp add: Un_cons Int_cons_left fold_type fold_commute |
225 apply (simp add: Un_cons Int_cons_left fold_type fold_commute |
226 fold_typing.fold_cons [of A _ _ f] |
226 fold_typing.fold_cons [of A _ _ f] |
227 fold_typing_def fcomm cons_absorb) |
227 fold_typing_def fcomm cons_absorb) |
228 done |
228 done |
229 |
229 |
230 lemma (in fold_typing) fold_nest_Un_disjoint: |
230 lemma (in fold_typing) fold_nest_Un_disjoint: |
231 "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |] |
231 "[| C\<in>Fin(A); D\<in>Fin(A); C \<inter> D = 0 |] |
232 ==> fold[B](f,e,C Un D) = fold[B](f, fold[B](f,e,D), C)" |
232 ==> fold[B](f,e,C \<union> D) = fold[B](f, fold[B](f,e,D), C)" |
233 by (simp add: fold_nest_Un_Int) |
233 by (simp add: fold_nest_Un_Int) |
234 |
234 |
235 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" |
235 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))" |
236 apply (drule Finite_into_Fin) |
236 apply (drule Finite_into_Fin) |
237 apply (blast intro: Fin_mono [THEN subsetD]) |
237 apply (blast intro: Fin_mono [THEN subsetD]) |
258 done |
258 done |
259 |
259 |
260 (*The reversed orientation looks more natural, but LOOPS as a simprule!*) |
260 (*The reversed orientation looks more natural, but LOOPS as a simprule!*) |
261 lemma setsum_Un_Int: |
261 lemma setsum_Un_Int: |
262 "[| Finite(C); Finite(D) |] |
262 "[| Finite(C); Finite(D) |] |
263 ==> setsum(g, C Un D) $+ setsum(g, C Int D) |
263 ==> setsum(g, C \<union> D) $+ setsum(g, C \<inter> D) |
264 = setsum(g, C) $+ setsum(g, D)" |
264 = setsum(g, C) $+ setsum(g, D)" |
265 apply (erule Finite_induct) |
265 apply (erule Finite_induct) |
266 apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un |
266 apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un |
267 Int_lower1 [THEN subset_Finite]) |
267 Int_lower1 [THEN subset_Finite]) |
268 done |
268 done |
272 prefer 2 apply (simp add: setsum_def) |
272 prefer 2 apply (simp add: setsum_def) |
273 apply (erule Finite_induct, auto) |
273 apply (erule Finite_induct, auto) |
274 done |
274 done |
275 |
275 |
276 lemma setsum_Un_disjoint: |
276 lemma setsum_Un_disjoint: |
277 "[| Finite(C); Finite(D); C Int D = 0 |] |
277 "[| Finite(C); Finite(D); C \<inter> D = 0 |] |
278 ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)" |
278 ==> setsum(g, C \<union> D) = setsum(g, C) $+ setsum(g,D)" |
279 apply (subst setsum_Un_Int [symmetric]) |
279 apply (subst setsum_Un_Int [symmetric]) |
280 apply (subgoal_tac [3] "Finite (C Un D) ") |
280 apply (subgoal_tac [3] "Finite (C \<union> D) ") |
281 apply (auto intro: Finite_Un) |
281 apply (auto intro: Finite_Un) |
282 done |
282 done |
283 |
283 |
284 lemma Finite_RepFun [rule_format (no_asm)]: |
284 lemma Finite_RepFun [rule_format (no_asm)]: |
285 "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))" |
285 "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> Finite(RepFun(I, C))" |
286 apply (erule Finite_induct, auto) |
286 apply (erule Finite_induct, auto) |
287 done |
287 done |
288 |
288 |
289 lemma setsum_UN_disjoint [rule_format (no_asm)]: |
289 lemma setsum_UN_disjoint [rule_format (no_asm)]: |
290 "Finite(I) |
290 "Finite(I) |
291 ==> (\<forall>i\<in>I. Finite(C(i))) --> |
291 ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> |
292 (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) --> |
292 (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow> |
293 setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)" |
293 setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)" |
294 apply (erule Finite_induct, auto) |
294 apply (erule Finite_induct, auto) |
295 apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i") |
295 apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i") |
296 prefer 2 apply blast |
296 prefer 2 apply blast |
297 apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0") |
297 apply (subgoal_tac "C (x) \<inter> (\<Union>i\<in>B. C (i)) = 0") |
298 prefer 2 apply blast |
298 prefer 2 apply blast |
299 apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ") |
299 apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ") |
300 apply (simp (no_asm_simp) add: setsum_Un_disjoint) |
300 apply (simp (no_asm_simp) add: setsum_Un_disjoint) |
301 apply (auto intro: Finite_Union Finite_RepFun) |
301 apply (auto intro: Finite_Union Finite_RepFun) |
302 done |
302 done |
330 setsum(f, A) = setsum(g, B)" |
330 setsum(f, A) = setsum(g, B)" |
331 by (simp add: setsum_def cong add: fold_cong) |
331 by (simp add: setsum_def cong add: fold_cong) |
332 |
332 |
333 lemma setsum_Un: |
333 lemma setsum_Un: |
334 "[| Finite(A); Finite(B) |] |
334 "[| Finite(A); Finite(B) |] |
335 ==> setsum(f, A Un B) = |
335 ==> setsum(f, A \<union> B) = |
336 setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)" |
336 setsum(f, A) $+ setsum(f, B) $- setsum(f, A \<inter> B)" |
337 apply (subst setsum_Un_Int [symmetric], auto) |
337 apply (subst setsum_Un_Int [symmetric], auto) |
338 done |
338 done |
339 |
339 |
340 |
340 |
341 lemma setsum_zneg_or_0 [rule_format (no_asm)]: |
341 lemma setsum_zneg_or_0 [rule_format (no_asm)]: |
342 "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0" |
342 "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) \<longrightarrow> setsum(g, A) $<= #0" |
343 apply (erule Finite_induct) |
343 apply (erule Finite_induct) |
344 apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0) |
344 apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0) |
345 done |
345 done |
346 |
346 |
347 lemma setsum_succD_lemma [rule_format]: |
347 lemma setsum_succD_lemma [rule_format]: |
348 "Finite(A) |
348 "Finite(A) |
349 ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))" |
349 ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) \<longrightarrow> (\<exists>a\<in>A. #0 $< f(a))" |
350 apply (erule Finite_induct) |
350 apply (erule Finite_induct) |
351 apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric]) |
351 apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric]) |
352 apply (subgoal_tac "setsum (f, B) $<= #0") |
352 apply (subgoal_tac "setsum (f, B) $<= #0") |
353 apply simp_all |
353 apply simp_all |
354 prefer 2 apply (blast intro: setsum_zneg_or_0) |
354 prefer 2 apply (blast intro: setsum_zneg_or_0) |
380 apply (auto intro: zpos_add_zpos_imp_zpos) |
380 apply (auto intro: zpos_add_zpos_imp_zpos) |
381 done |
381 done |
382 |
382 |
383 lemma g_zspos_imp_setsum_zspos [rule_format]: |
383 lemma g_zspos_imp_setsum_zspos [rule_format]: |
384 "Finite(A) |
384 "Finite(A) |
385 ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))" |
385 ==> (\<forall>x\<in>A. #0 $< g(x)) \<longrightarrow> A \<noteq> 0 \<longrightarrow> (#0 $< setsum(g, A))" |
386 apply (erule Finite_induct) |
386 apply (erule Finite_induct) |
387 apply (auto intro: zspos_add_zspos_imp_zspos) |
387 apply (auto intro: zspos_add_zspos_imp_zspos) |
388 done |
388 done |
389 |
389 |
390 lemma setsum_Diff [rule_format]: |
390 lemma setsum_Diff [rule_format]: |
391 "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})" |
391 "Finite(A) ==> \<forall>a. M(a) = #0 \<longrightarrow> setsum(M, A) = setsum(M, A-{a})" |
392 apply (erule Finite_induct) |
392 apply (erule Finite_induct) |
393 apply (simp_all add: Diff_cons_eq Finite_Diff) |
393 apply (simp_all add: Diff_cons_eq Finite_Diff) |
394 done |
394 done |
395 |
395 |
396 end |
396 end |