1 (* Title: Summation Operator for Abelian Groups |
|
2 ID: $Id$ |
|
3 Author: Clemens Ballarin, started 19 November 2002 |
|
4 |
|
5 This file is largely based on HOL/Finite_Set.thy. |
|
6 *) |
|
7 |
|
8 header {* Summation Operator *} |
|
9 |
|
10 theory Summation = Group: |
|
11 |
|
12 (* Instantiation of LC from Finite_Set.thy is not possible, |
|
13 because here we have explicit typing rules like x : carrier G. |
|
14 We introduce an explicit argument for the domain D *) |
|
15 |
|
16 consts |
|
17 foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set" |
|
18 |
|
19 inductive "foldSetD D f e" |
|
20 intros |
|
21 emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e" |
|
22 insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==> |
|
23 (insert x A, f x y) : foldSetD D f e" |
|
24 |
|
25 inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e" |
|
26 |
|
27 constdefs |
|
28 foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" |
|
29 "foldD D f e A == THE x. (A, x) : foldSetD D f e" |
|
30 |
|
31 lemma foldSetD_closed: |
|
32 "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |
|
33 |] ==> z : D"; |
|
34 by (erule foldSetD.elims) auto |
|
35 |
|
36 lemma Diff1_foldSetD: |
|
37 "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==> |
|
38 (A, f x y) : foldSetD D f e" |
|
39 apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
|
40 apply auto |
|
41 done |
|
42 |
|
43 lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A" |
|
44 by (induct set: foldSetD) auto |
|
45 |
|
46 lemma finite_imp_foldSetD: |
|
47 "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==> |
|
48 EX x. (A, x) : foldSetD D f e" |
|
49 proof (induct set: Finites) |
|
50 case empty then show ?case by auto |
|
51 next |
|
52 case (insert F x) |
|
53 then obtain y where y: "(F, y) : foldSetD D f e" by auto |
|
54 with insert have "y : D" by (auto dest: foldSetD_closed) |
|
55 with y and insert have "(insert x F, f x y) : foldSetD D f e" |
|
56 by (intro foldSetD.intros) auto |
|
57 then show ?case .. |
|
58 qed |
|
59 |
|
60 subsection {* Left-commutative operations *} |
|
61 |
|
62 locale LCD = |
|
63 fixes B :: "'b set" |
|
64 and D :: "'a set" |
|
65 and f :: "'b => 'a => 'a" (infixl "\<cdot>" 70) |
|
66 assumes left_commute: "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
67 and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D" |
|
68 |
|
69 lemma (in LCD) foldSetD_closed [dest]: |
|
70 "(A, z) : foldSetD D f e ==> z : D"; |
|
71 by (erule foldSetD.elims) auto |
|
72 |
|
73 lemma (in LCD) Diff1_foldSetD: |
|
74 "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==> |
|
75 (A, f x y) : foldSetD D f e" |
|
76 apply (subgoal_tac "x : B") |
|
77 prefer 2 apply fast |
|
78 apply (erule insert_Diff [THEN subst], rule foldSetD.intros) |
|
79 apply auto |
|
80 done |
|
81 |
|
82 lemma (in LCD) foldSetD_imp_finite [simp]: |
|
83 "(A, x) : foldSetD D f e ==> finite A" |
|
84 by (induct set: foldSetD) auto |
|
85 |
|
86 lemma (in LCD) finite_imp_foldSetD: |
|
87 "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e" |
|
88 proof (induct set: Finites) |
|
89 case empty then show ?case by auto |
|
90 next |
|
91 case (insert F x) |
|
92 then obtain y where y: "(F, y) : foldSetD D f e" by auto |
|
93 with insert have "y : D" by auto |
|
94 with y and insert have "(insert x F, f x y) : foldSetD D f e" |
|
95 by (intro foldSetD.intros) auto |
|
96 then show ?case .. |
|
97 qed |
|
98 |
|
99 lemma (in LCD) foldSetD_determ_aux: |
|
100 "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e --> |
|
101 (ALL y. (A, y) : foldSetD D f e --> y = x)" |
|
102 apply (induct n) |
|
103 apply (auto simp add: less_Suc_eq) |
|
104 apply (erule foldSetD.cases) |
|
105 apply blast |
|
106 apply (erule foldSetD.cases) |
|
107 apply blast |
|
108 apply clarify |
|
109 txt {* force simplification of @{text "card A < card (insert ...)"}. *} |
|
110 apply (erule rev_mp) |
|
111 apply (simp add: less_Suc_eq_le) |
|
112 apply (rule impI) |
|
113 apply (rename_tac Aa xa ya Ab xb yb, case_tac "xa = xb") |
|
114 apply (subgoal_tac "Aa = Ab") |
|
115 prefer 2 apply (blast elim!: equalityE) |
|
116 apply blast |
|
117 txt {* case @{prop "xa \<notin> xb"}. *} |
|
118 apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab") |
|
119 prefer 2 apply (blast elim!: equalityE) |
|
120 apply clarify |
|
121 apply (subgoal_tac "Aa = insert xb Ab - {xa}") |
|
122 prefer 2 apply blast |
|
123 apply (subgoal_tac "card Aa <= card Ab") |
|
124 prefer 2 |
|
125 apply (rule Suc_le_mono [THEN subst]) |
|
126 apply (simp add: card_Suc_Diff1) |
|
127 apply (rule_tac A1 = "Aa - {xb}" in finite_imp_foldSetD [THEN exE]) |
|
128 apply (blast intro: foldSetD_imp_finite finite_Diff) |
|
129 (* new subgoal from finite_imp_foldSetD *) |
|
130 apply best (* blast doesn't seem to solve this *) |
|
131 apply assumption |
|
132 apply (frule (1) Diff1_foldSetD) |
|
133 (* new subgoal from Diff1_foldSetD *) |
|
134 apply best |
|
135 (* |
|
136 apply (best del: foldSetD_closed elim: foldSetD_closed) |
|
137 apply (rule f_closed) apply assumption apply (rule foldSetD_closed) |
|
138 prefer 3 apply assumption apply (rule e_closed) |
|
139 apply (rule f_closed) apply force apply assumption |
|
140 *) |
|
141 apply (subgoal_tac "ya = f xb x") |
|
142 prefer 2 |
|
143 (* new subgoal to make IH applicable *) |
|
144 apply (subgoal_tac "Aa <= B") |
|
145 prefer 2 apply best |
|
146 apply (blast del: equalityCE) |
|
147 apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e") |
|
148 prefer 2 apply simp |
|
149 apply (subgoal_tac "yb = f xa x") |
|
150 prefer 2 |
|
151 (* apply (drule_tac x = xa in Diff1_foldSetD) |
|
152 apply assumption |
|
153 apply (rule f_closed) apply best apply (rule foldSetD_closed) |
|
154 prefer 3 apply assumption apply (rule e_closed) |
|
155 apply (rule f_closed) apply best apply assumption |
|
156 *) |
|
157 apply (blast del: equalityCE dest: Diff1_foldSetD) |
|
158 apply (simp (no_asm_simp)) |
|
159 apply (rule left_commute) |
|
160 apply assumption apply best apply best |
|
161 done |
|
162 |
|
163 lemma (in LCD) foldSetD_determ: |
|
164 "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |] |
|
165 ==> y = x" |
|
166 by (blast intro: foldSetD_determ_aux [rule_format]) |
|
167 |
|
168 lemma (in LCD) foldD_equality: |
|
169 "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y" |
|
170 by (unfold foldD_def) (blast intro: foldSetD_determ) |
|
171 |
|
172 lemma foldD_empty [simp]: |
|
173 "e : D ==> foldD D f e {} = e" |
|
174 by (unfold foldD_def) blast |
|
175 |
|
176 lemma (in LCD) foldD_insert_aux: |
|
177 "[| x ~: A; x : B; e : D; A <= B |] ==> |
|
178 ((insert x A, v) : foldSetD D f e) = |
|
179 (EX y. (A, y) : foldSetD D f e & v = f x y)" |
|
180 apply auto |
|
181 apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE]) |
|
182 apply (fastsimp dest: foldSetD_imp_finite) |
|
183 (* new subgoal by finite_imp_foldSetD *) |
|
184 apply assumption |
|
185 apply assumption |
|
186 apply (blast intro: foldSetD_determ) |
|
187 done |
|
188 |
|
189 lemma (in LCD) foldD_insert: |
|
190 "[| finite A; x ~: A; x : B; e : D; A <= B |] ==> |
|
191 foldD D f e (insert x A) = f x (foldD D f e A)" |
|
192 apply (unfold foldD_def) |
|
193 apply (simp add: foldD_insert_aux) |
|
194 apply (rule the_equality) |
|
195 apply (auto intro: finite_imp_foldSetD |
|
196 cong add: conj_cong simp add: foldD_def [symmetric] foldD_equality) |
|
197 done |
|
198 |
|
199 lemma (in LCD) foldD_closed [simp]: |
|
200 "[| finite A; e : D; A <= B |] ==> foldD D f e A : D" |
|
201 proof (induct set: Finites) |
|
202 case empty then show ?case by (simp add: foldD_empty) |
|
203 next |
|
204 case insert then show ?case by (simp add: foldD_insert) |
|
205 qed |
|
206 |
|
207 lemma (in LCD) foldD_commute: |
|
208 "[| finite A; x : B; e : D; A <= B |] ==> |
|
209 f x (foldD D f e A) = foldD D f (f x e) A" |
|
210 apply (induct set: Finites) |
|
211 apply simp |
|
212 apply (auto simp add: left_commute foldD_insert) |
|
213 done |
|
214 |
|
215 lemma Int_mono2: |
|
216 "[| A <= C; B <= C |] ==> A Int B <= C" |
|
217 by blast |
|
218 |
|
219 lemma (in LCD) foldD_nest_Un_Int: |
|
220 "[| finite A; finite C; e : D; A <= B; C <= B |] ==> |
|
221 foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)" |
|
222 apply (induct set: Finites) |
|
223 apply simp |
|
224 apply (simp add: foldD_insert foldD_commute Int_insert_left insert_absorb |
|
225 Int_mono2 Un_subset_iff) |
|
226 done |
|
227 |
|
228 lemma (in LCD) foldD_nest_Un_disjoint: |
|
229 "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |] |
|
230 ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A" |
|
231 by (simp add: foldD_nest_Un_Int) |
|
232 |
|
233 -- {* Delete rules to do with @{text foldSetD} relation. *} |
|
234 |
|
235 declare foldSetD_imp_finite [simp del] |
|
236 empty_foldSetDE [rule del] |
|
237 foldSetD.intros [rule del] |
|
238 declare (in LCD) |
|
239 foldSetD_closed [rule del] |
|
240 |
|
241 subsection {* Commutative monoids *} |
|
242 |
|
243 text {* |
|
244 We enter a more restrictive context, with @{text "f :: 'a => 'a => 'a"} |
|
245 instead of @{text "'b => 'a => 'a"}. |
|
246 *} |
|
247 |
|
248 locale ACeD = |
|
249 fixes D :: "'a set" |
|
250 and f :: "'a => 'a => 'a" (infixl "\<cdot>" 70) |
|
251 and e :: 'a |
|
252 assumes ident [simp]: "x : D ==> x \<cdot> e = x" |
|
253 and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x" |
|
254 and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
255 and e_closed [simp]: "e : D" |
|
256 and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D" |
|
257 |
|
258 lemma (in ACeD) left_commute: |
|
259 "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" |
|
260 proof - |
|
261 assume D: "x : D" "y : D" "z : D" |
|
262 then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute) |
|
263 also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc) |
|
264 also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute) |
|
265 finally show ?thesis . |
|
266 qed |
|
267 |
|
268 lemmas (in ACeD) AC = assoc commute left_commute |
|
269 |
|
270 lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x" |
|
271 proof - |
|
272 assume D: "x : D" |
|
273 have "x \<cdot> e = x" by (rule ident) |
|
274 with D show ?thesis by (simp add: commute) |
|
275 qed |
|
276 |
|
277 lemma (in ACeD) foldD_Un_Int: |
|
278 "[| finite A; finite B; A <= D; B <= D |] ==> |
|
279 foldD D f e A \<cdot> foldD D f e B = |
|
280 foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)" |
|
281 apply (induct set: Finites) |
|
282 apply (simp add: left_commute LCD.foldD_closed [OF LCD.intro [of D]]) |
|
283 (* left_commute is required to show premise of LCD.intro *) |
|
284 apply (simp add: AC insert_absorb Int_insert_left |
|
285 LCD.foldD_insert [OF LCD.intro [of D]] |
|
286 LCD.foldD_closed [OF LCD.intro [of D]] |
|
287 Int_mono2 Un_subset_iff) |
|
288 done |
|
289 |
|
290 lemma (in ACeD) foldD_Un_disjoint: |
|
291 "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==> |
|
292 foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B" |
|
293 by (simp add: foldD_Un_Int |
|
294 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
|
295 |
|
296 subsection {* Products over Finite Sets *} |
|
297 |
|
298 constdefs |
|
299 finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" |
|
300 "finprod G f A == if finite A |
|
301 then foldD (carrier G) (mult G o f) (one G) A |
|
302 else arbitrary" |
|
303 |
|
304 (* |
|
305 locale finite_prod = abelian_monoid + var prod + |
|
306 defines "prod == (%f A. if finite A |
|
307 then foldD (carrier G) (op \<otimes> o f) \<one> A |
|
308 else arbitrary)" |
|
309 *) |
|
310 (* TODO: nice syntax for the summation operator inside the locale |
|
311 like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *) |
|
312 |
|
313 ML_setup {* |
|
314 |
|
315 Context.>> (fn thy => (simpset_ref_of thy := |
|
316 simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *} |
|
317 |
|
318 lemma (in abelian_monoid) finprod_empty [simp]: |
|
319 "finprod G f {} = \<one>" |
|
320 by (simp add: finprod_def) |
|
321 |
|
322 ML_setup {* |
|
323 |
|
324 Context.>> (fn thy => (simpset_ref_of thy := |
|
325 simpset_of thy setsubgoaler asm_simp_tac; thy)) *} |
|
326 |
|
327 declare funcsetI [intro] |
|
328 funcset_mem [dest] |
|
329 |
|
330 lemma (in abelian_monoid) finprod_insert [simp]: |
|
331 "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==> |
|
332 finprod G f (insert a F) = f a \<otimes> finprod G f F" |
|
333 apply (rule trans) |
|
334 apply (simp add: finprod_def) |
|
335 apply (rule trans) |
|
336 apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) |
|
337 apply simp |
|
338 apply (rule m_lcomm) |
|
339 apply fast apply fast apply assumption |
|
340 apply (fastsimp intro: m_closed) |
|
341 apply simp+ apply fast |
|
342 apply (auto simp add: finprod_def) |
|
343 done |
|
344 |
|
345 lemma (in abelian_monoid) finprod_one: |
|
346 "finite A ==> finprod G (%i. \<one>) A = \<one>" |
|
347 proof (induct set: Finites) |
|
348 case empty show ?case by simp |
|
349 next |
|
350 case (insert A a) |
|
351 have "(%i. \<one>) \<in> A -> carrier G" by auto |
|
352 with insert show ?case by simp |
|
353 qed |
|
354 |
|
355 lemma (in abelian_monoid) finprod_closed [simp]: |
|
356 fixes A |
|
357 assumes fin: "finite A" and f: "f \<in> A -> carrier G" |
|
358 shows "finprod G f A \<in> carrier G" |
|
359 using fin f |
|
360 proof induct |
|
361 case empty show ?case by simp |
|
362 next |
|
363 case (insert A a) |
|
364 then have a: "f a \<in> carrier G" by fast |
|
365 from insert have A: "f \<in> A -> carrier G" by fast |
|
366 from insert A a show ?case by simp |
|
367 qed |
|
368 |
|
369 lemma funcset_Int_left [simp, intro]: |
|
370 "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C" |
|
371 by fast |
|
372 |
|
373 lemma funcset_Un_left [iff]: |
|
374 "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)" |
|
375 by fast |
|
376 |
|
377 lemma (in abelian_monoid) finprod_Un_Int: |
|
378 "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==> |
|
379 finprod G g (A Un B) \<otimes> finprod G g (A Int B) = |
|
380 finprod G g A \<otimes> finprod G g B" |
|
381 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
382 proof (induct set: Finites) |
|
383 case empty then show ?case by (simp add: finprod_closed) |
|
384 next |
|
385 case (insert A a) |
|
386 then have a: "g a \<in> carrier G" by fast |
|
387 from insert have A: "g \<in> A -> carrier G" by fast |
|
388 from insert A a show ?case |
|
389 by (simp add: ac Int_insert_left insert_absorb finprod_closed |
|
390 Int_mono2 Un_subset_iff) |
|
391 qed |
|
392 |
|
393 lemma (in abelian_monoid) finprod_Un_disjoint: |
|
394 "[| finite A; finite B; A Int B = {}; |
|
395 g \<in> A -> carrier G; g \<in> B -> carrier G |] |
|
396 ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B" |
|
397 apply (subst finprod_Un_Int [symmetric]) |
|
398 apply (auto simp add: finprod_closed) |
|
399 done |
|
400 |
|
401 lemma (in abelian_monoid) finprod_multf: |
|
402 "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==> |
|
403 finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)" |
|
404 proof (induct set: Finites) |
|
405 case empty show ?case by simp |
|
406 next |
|
407 case (insert A a) then |
|
408 have fA: "f : A -> carrier G" by fast |
|
409 from insert have fa: "f a : carrier G" by fast |
|
410 from insert have gA: "g : A -> carrier G" by fast |
|
411 from insert have ga: "g a : carrier G" by fast |
|
412 from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def) |
|
413 from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G" |
|
414 by (simp add: Pi_def) |
|
415 show ?case (* check if all simps are really necessary *) |
|
416 by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff) |
|
417 qed |
|
418 |
|
419 lemma (in abelian_monoid) finprod_cong': |
|
420 "[| A = B; g : B -> carrier G; |
|
421 !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
|
422 proof - |
|
423 assume prems: "A = B" "g : B -> carrier G" |
|
424 "!!i. i : B ==> f i = g i" |
|
425 show ?thesis |
|
426 proof (cases "finite B") |
|
427 case True |
|
428 then have "!!A. [| A = B; g : B -> carrier G; |
|
429 !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
|
430 proof induct |
|
431 case empty thus ?case by simp |
|
432 next |
|
433 case (insert B x) |
|
434 then have "finprod G f A = finprod G f (insert x B)" by simp |
|
435 also from insert have "... = f x \<otimes> finprod G f B" |
|
436 proof (intro finprod_insert) |
|
437 show "finite B" . |
|
438 next |
|
439 show "x ~: B" . |
|
440 next |
|
441 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
|
442 "g \<in> insert x B \<rightarrow> carrier G" |
|
443 thus "f : B -> carrier G" by fastsimp |
|
444 next |
|
445 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
|
446 "g \<in> insert x B \<rightarrow> carrier G" |
|
447 thus "f x \<in> carrier G" by fastsimp |
|
448 qed |
|
449 also from insert have "... = g x \<otimes> finprod G g B" by fastsimp |
|
450 also from insert have "... = finprod G g (insert x B)" |
|
451 by (intro finprod_insert [THEN sym]) auto |
|
452 finally show ?case . |
|
453 qed |
|
454 with prems show ?thesis by simp |
|
455 next |
|
456 case False with prems show ?thesis by (simp add: finprod_def) |
|
457 qed |
|
458 qed |
|
459 |
|
460 lemma (in abelian_monoid) finprod_cong: |
|
461 "[| A = B; !!i. i : B ==> f i = g i; |
|
462 g : B -> carrier G = True |] ==> finprod G f A = finprod G g B" |
|
463 by (rule finprod_cong') fast+ |
|
464 |
|
465 text {*Usually, if this rule causes a failed congruence proof error, |
|
466 the reason is that the premise @{text "g : B -> carrier G"} cannot be shown. |
|
467 Adding @{thm [source] Pi_def} to the simpset is often useful. |
|
468 For this reason, @{thm [source] abelian_monoid.finprod_cong} |
|
469 is not added to the simpset by default. |
|
470 *} |
|
471 |
|
472 declare funcsetI [rule del] |
|
473 funcset_mem [rule del] |
|
474 |
|
475 lemma (in abelian_monoid) finprod_0 [simp]: |
|
476 "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0" |
|
477 by (simp add: Pi_def) |
|
478 |
|
479 lemma (in abelian_monoid) finprod_Suc [simp]: |
|
480 "f : {..Suc n} -> carrier G ==> |
|
481 finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})" |
|
482 by (simp add: Pi_def atMost_Suc) |
|
483 |
|
484 lemma (in abelian_monoid) finprod_Suc2: |
|
485 "f : {..Suc n} -> carrier G ==> |
|
486 finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)" |
|
487 proof (induct n) |
|
488 case 0 thus ?case by (simp add: Pi_def) |
|
489 next |
|
490 case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed) |
|
491 qed |
|
492 |
|
493 lemma (in abelian_monoid) finprod_mult [simp]: |
|
494 "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==> |
|
495 finprod G (%i. f i \<otimes> g i) {..n::nat} = |
|
496 finprod G f {..n} \<otimes> finprod G g {..n}" |
|
497 by (induct n) (simp_all add: ac Pi_def finprod_closed) |
|
498 |
|
499 end |
|
500 |
|