291 "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==> |
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" |
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 |
293 by (simp add: foldD_Un_Int |
294 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
294 left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff) |
295 |
295 |
296 subsection {* A Product Operator for Finite Sets *} |
296 subsection {* Products over Finite Sets *} |
297 |
297 |
298 text {* |
298 constdefs |
299 Definition of product (or summation, if the monoid is written addivitively) |
299 finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" |
300 operator. |
300 "finprod G f A == if finite A |
301 *} |
301 then foldD (carrier G) (mult G o f) (one G) A |
302 |
302 else arbitrary" |
|
303 |
|
304 (* |
303 locale finite_prod = abelian_monoid + var prod + |
305 locale finite_prod = abelian_monoid + var prod + |
304 defines "prod == (%f A. if finite A |
306 defines "prod == (%f A. if finite A |
305 then foldD (carrier G) (op \<otimes> o f) \<one> A |
307 then foldD (carrier G) (op \<otimes> o f) \<one> A |
306 else arbitrary)" |
308 else arbitrary)" |
307 |
309 *) |
308 (* TODO: nice syntax for the summation operator inside the locale |
310 (* TODO: nice syntax for the summation operator inside the locale |
309 like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *) |
311 like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *) |
310 |
312 |
311 ML_setup {* |
313 ML_setup {* |
312 |
314 |
313 Context.>> (fn thy => (simpset_ref_of thy := |
315 Context.>> (fn thy => (simpset_ref_of thy := |
314 simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *} |
316 simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *} |
315 |
317 |
316 lemma (in finite_prod) prod_empty [simp]: |
318 lemma (in abelian_monoid) finprod_empty [simp]: |
317 "prod f {} = \<one>" |
319 "finprod G f {} = \<one>" |
318 by (simp add: prod_def) |
320 by (simp add: finprod_def) |
319 |
321 |
320 ML_setup {* |
322 ML_setup {* |
321 |
323 |
322 Context.>> (fn thy => (simpset_ref_of thy := |
324 Context.>> (fn thy => (simpset_ref_of thy := |
323 simpset_of thy setsubgoaler asm_simp_tac; thy)) *} |
325 simpset_of thy setsubgoaler asm_simp_tac; thy)) *} |
324 |
326 |
325 declare funcsetI [intro] |
327 declare funcsetI [intro] |
326 funcset_mem [dest] |
328 funcset_mem [dest] |
327 |
329 |
328 lemma (in finite_prod) prod_insert [simp]: |
330 lemma (in abelian_monoid) finprod_insert [simp]: |
329 "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==> |
331 "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==> |
330 prod f (insert a F) = f a \<otimes> prod f F" |
332 finprod G f (insert a F) = f a \<otimes> finprod G f F" |
331 apply (rule trans) |
333 apply (rule trans) |
332 apply (simp add: prod_def) |
334 apply (simp add: finprod_def) |
333 apply (rule trans) |
335 apply (rule trans) |
334 apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) |
336 apply (rule LCD.foldD_insert [OF LCD.intro [of "insert a F"]]) |
335 apply simp |
337 apply simp |
336 apply (rule m_lcomm) |
338 apply (rule m_lcomm) |
337 apply fast apply fast apply assumption |
339 apply fast apply fast apply assumption |
338 apply (fastsimp intro: m_closed) |
340 apply (fastsimp intro: m_closed) |
339 apply simp+ apply fast |
341 apply simp+ apply fast |
340 apply (auto simp add: prod_def) |
342 apply (auto simp add: finprod_def) |
341 done |
343 done |
342 |
344 |
343 lemma (in finite_prod) prod_one: |
345 lemma (in abelian_monoid) finprod_one: |
344 "finite A ==> prod (%i. \<one>) A = \<one>" |
346 "finite A ==> finprod G (%i. \<one>) A = \<one>" |
345 proof (induct set: Finites) |
347 proof (induct set: Finites) |
346 case empty show ?case by simp |
348 case empty show ?case by simp |
347 next |
349 next |
348 case (insert A a) |
350 case (insert A a) |
349 have "(%i. \<one>) \<in> A -> carrier G" by auto |
351 have "(%i. \<one>) \<in> A -> carrier G" by auto |
350 with insert show ?case by simp |
352 with insert show ?case by simp |
351 qed |
353 qed |
352 |
354 |
353 (* |
355 lemma (in abelian_monoid) finprod_closed [simp]: |
354 lemma prod_eq_0_iff [simp]: |
|
355 "finite F ==> (prod f F = 0) = (ALL a:F. f a = (0::nat))" |
|
356 by (induct set: Finites) auto |
|
357 |
|
358 lemma prod_SucD: "prod f A = Suc n ==> EX a:A. 0 < f a" |
|
359 apply (case_tac "finite A") |
|
360 prefer 2 apply (simp add: prod_def) |
|
361 apply (erule rev_mp) |
|
362 apply (erule finite_induct) |
|
363 apply auto |
|
364 done |
|
365 |
|
366 lemma card_eq_prod: "finite A ==> card A = prod (\<lambda>x. 1) A" |
|
367 *) -- {* Could allow many @{text "card"} proofs to be simplified. *} |
|
368 (* |
|
369 by (induct set: Finites) auto |
|
370 *) |
|
371 |
|
372 lemma (in finite_prod) prod_closed: |
|
373 fixes A |
356 fixes A |
374 assumes fin: "finite A" and f: "f \<in> A -> carrier G" |
357 assumes fin: "finite A" and f: "f \<in> A -> carrier G" |
375 shows "prod f A \<in> carrier G" |
358 shows "finprod G f A \<in> carrier G" |
376 using fin f |
359 using fin f |
377 proof induct |
360 proof induct |
378 case empty show ?case by simp |
361 case empty show ?case by simp |
379 next |
362 next |
380 case (insert A a) |
363 case (insert A a) |
389 |
372 |
390 lemma funcset_Un_left [iff]: |
373 lemma funcset_Un_left [iff]: |
391 "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)" |
374 "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)" |
392 by fast |
375 by fast |
393 |
376 |
394 lemma (in finite_prod) prod_Un_Int: |
377 lemma (in abelian_monoid) finprod_Un_Int: |
395 "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==> |
378 "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==> |
396 prod g (A Un B) \<otimes> prod g (A Int B) = prod g A \<otimes> prod g B" |
379 finprod G g (A Un B) \<otimes> finprod G g (A Int B) = |
|
380 finprod G g A \<otimes> finprod G g B" |
397 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
381 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
398 proof (induct set: Finites) |
382 proof (induct set: Finites) |
399 case empty then show ?case by (simp add: prod_closed) |
383 case empty then show ?case by (simp add: finprod_closed) |
400 next |
384 next |
401 case (insert A a) |
385 case (insert A a) |
402 then have a: "g a \<in> carrier G" by fast |
386 then have a: "g a \<in> carrier G" by fast |
403 from insert have A: "g \<in> A -> carrier G" by fast |
387 from insert have A: "g \<in> A -> carrier G" by fast |
404 from insert A a show ?case |
388 from insert A a show ?case |
405 by (simp add: ac Int_insert_left insert_absorb prod_closed |
389 by (simp add: ac Int_insert_left insert_absorb finprod_closed |
406 Int_mono2 Un_subset_iff) |
390 Int_mono2 Un_subset_iff) |
407 qed |
391 qed |
408 |
392 |
409 lemma (in finite_prod) prod_Un_disjoint: |
393 lemma (in abelian_monoid) finprod_Un_disjoint: |
410 "[| finite A; finite B; A Int B = {}; |
394 "[| finite A; finite B; A Int B = {}; |
411 g \<in> A -> carrier G; g \<in> B -> carrier G |] |
395 g \<in> A -> carrier G; g \<in> B -> carrier G |] |
412 ==> prod g (A Un B) = prod g A \<otimes> prod g B" |
396 ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B" |
413 apply (subst prod_Un_Int [symmetric]) |
397 apply (subst finprod_Un_Int [symmetric]) |
414 apply (auto simp add: prod_closed) |
398 apply (auto simp add: finprod_closed) |
415 done |
399 done |
416 |
400 |
417 (* |
401 lemma (in abelian_monoid) finprod_multf: |
418 lemma prod_UN_disjoint: |
|
419 fixes f :: "'a => 'b::plus_ac0" |
|
420 shows |
|
421 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
422 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
423 prod f (UNION I A) = prod (\<lambda>i. prod f (A i)) I" |
|
424 apply (induct set: Finites) |
|
425 apply simp |
|
426 apply atomize |
|
427 apply (subgoal_tac "ALL i:F. x \<noteq> i") |
|
428 prefer 2 apply blast |
|
429 apply (subgoal_tac "A x Int UNION F A = {}") |
|
430 prefer 2 apply blast |
|
431 apply (simp add: prod_Un_disjoint) |
|
432 done |
|
433 *) |
|
434 |
|
435 lemma (in finite_prod) prod_addf: |
|
436 "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==> |
402 "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==> |
437 prod (%x. f x \<otimes> g x) A = (prod f A \<otimes> prod g A)" |
403 finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)" |
438 proof (induct set: Finites) |
404 proof (induct set: Finites) |
439 case empty show ?case by simp |
405 case empty show ?case by simp |
440 next |
406 next |
441 case (insert A a) then |
407 case (insert A a) then |
442 have fA: "f : A -> carrier G" by fast |
408 have fA: "f : A -> carrier G" by fast |
445 from insert have ga: "g a : carrier G" by fast |
411 from insert have ga: "g a : carrier G" by fast |
446 from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def) |
412 from insert have fga: "(%x. f x \<otimes> g x) a : carrier G" by (simp add: Pi_def) |
447 from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G" |
413 from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G" |
448 by (simp add: Pi_def) |
414 by (simp add: Pi_def) |
449 show ?case (* check if all simps are really necessary *) |
415 show ?case (* check if all simps are really necessary *) |
450 by (simp add: insert fA fa gA ga fgA fga ac prod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff) |
416 by (simp add: insert fA fa gA ga fgA fga ac finprod_closed Int_insert_left insert_absorb Int_mono2 Un_subset_iff) |
451 qed |
417 qed |
452 |
418 |
453 (* |
419 lemma (in abelian_monoid) finprod_cong: |
454 lemma prod_Un: "finite A ==> finite B ==> |
420 "[| A = B; g : B -> carrier G; |
455 (prod f (A Un B) :: nat) = prod f A + prod f B - prod f (A Int B)" |
421 !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
456 apply (subst prod_Un_Int [symmetric]) |
|
457 apply auto |
|
458 done |
|
459 |
|
460 lemma prod_diff1: "(prod f (A - {a}) :: nat) = |
|
461 (if a:A then prod f A - f a else prod f A)" |
|
462 apply (case_tac "finite A") |
|
463 prefer 2 apply (simp add: prod_def) |
|
464 apply (erule finite_induct) |
|
465 apply (auto simp add: insert_Diff_if) |
|
466 apply (drule_tac a = a in mk_disjoint_insert) |
|
467 apply auto |
|
468 done |
|
469 *) |
|
470 |
|
471 text {* |
|
472 Congruence rule. The simplifier requires the rule to be in this form. |
|
473 *} |
|
474 (* |
|
475 lemma (in finite_prod) prod_cong [cong]: |
|
476 "[| A = B; !!i. i \<in> B ==> f i = g i; |
|
477 g \<in> B -> carrier G = True |] ==> prod f A = prod g B" |
|
478 *) |
|
479 lemma (in finite_prod) prod_cong: |
|
480 "[| A = B; g \<in> B -> carrier G; |
|
481 !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B" |
|
482 |
|
483 proof - |
422 proof - |
484 assume prems: "A = B" |
423 assume prems: "A = B" "g : B -> carrier G" |
485 "!!i. i \<in> B ==> f i = g i" |
424 "!!i. i : B ==> f i = g i" |
486 "g \<in> B -> carrier G" |
|
487 show ?thesis |
425 show ?thesis |
488 proof (cases "finite B") |
426 proof (cases "finite B") |
489 case True |
427 case True |
490 then have "!!A. [| A = B; g \<in> B -> carrier G; |
428 then have "!!A. [| A = B; g : B -> carrier G; |
491 !!i. i \<in> B ==> f i = g i |] ==> prod f A = prod g B" |
429 !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B" |
492 proof induct |
430 proof induct |
493 case empty thus ?case by simp |
431 case empty thus ?case by simp |
494 next |
432 next |
495 case (insert B x) |
433 case (insert B x) |
496 then have "prod f A = prod f (insert x B)" by simp |
434 then have "finprod G f A = finprod G f (insert x B)" by simp |
497 also from insert have "... = f x \<otimes> prod f B" |
435 also from insert have "... = f x \<otimes> finprod G f B" |
498 proof (intro prod_insert) |
436 proof (intro finprod_insert) |
499 show "finite B" . |
437 show "finite B" . |
500 next |
438 next |
501 show "x \<notin> B" . |
439 show "x ~: B" . |
502 next |
440 next |
503 assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
441 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
504 "g \<in> insert x B \<rightarrow> carrier G" |
442 "g \<in> insert x B \<rightarrow> carrier G" |
505 thus "f \<in> B -> carrier G" by fastsimp |
443 thus "f : B -> carrier G" by fastsimp |
506 next |
444 next |
507 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
445 assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i" |
508 "g \<in> insert x B \<rightarrow> carrier G" |
446 "g \<in> insert x B \<rightarrow> carrier G" |
509 thus "f x \<in> carrier G" by fastsimp |
447 thus "f x \<in> carrier G" by fastsimp |
510 qed |
448 qed |
511 also from insert have "... = g x \<otimes> prod g B" by fastsimp |
449 also from insert have "... = g x \<otimes> finprod G g B" by fastsimp |
512 also from insert have "... = prod g (insert x B)" |
450 also from insert have "... = finprod G g (insert x B)" |
513 by (intro prod_insert [THEN sym]) auto |
451 by (intro finprod_insert [THEN sym]) auto |
514 finally show ?case . |
452 finally show ?case . |
515 qed |
453 qed |
516 with prems show ?thesis by simp |
454 with prems show ?thesis by simp |
517 next |
455 next |
518 case False with prems show ?thesis by (simp add: prod_def) |
456 case False with prems show ?thesis by (simp add: finprod_def) |
519 qed |
457 qed |
520 qed |
458 qed |
521 |
459 |
522 lemma (in finite_prod) prod_cong1 [cong]: |
460 lemma (in abelian_monoid) finprod_cong' [cong]: |
523 "[| A = B; !!i. i \<in> B ==> f i = g i; |
461 "[| A = B; !!i. i : B ==> f i = g i; |
524 g \<in> B -> carrier G = True |] ==> prod f A = prod g B" |
462 g : B -> carrier G = True |] ==> finprod G f A = finprod G g B" |
525 by (rule prod_cong) fast+ |
463 by (rule finprod_cong) fast+ |
526 |
464 |
527 text {* |
465 text {*Usually, if this rule causes a failed congruence proof error, |
528 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. |
529 the reason is that the premise @{text "g \<in> B -> carrier G"} could not |
467 Adding @{thm [source] Pi_def} to the simpset is often useful. *} |
530 be shown. Adding @{thm [source] Pi_def} to the simpset is often useful. |
|
531 *} |
|
532 |
468 |
533 declare funcsetI [rule del] |
469 declare funcsetI [rule del] |
534 funcset_mem [rule del] |
470 funcset_mem [rule del] |
535 |
471 |
536 subsection {* Summation over the integer interval @{term "{..n}"} *} |
472 lemma (in abelian_monoid) finprod_0 [simp]: |
537 |
473 "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0" |
538 text {* |
|
539 A new locale where the index set is restricted to @{term "nat"} is |
|
540 necessary, because currently locales demand types in theorems to be as |
|
541 general as in the locale's definition. |
|
542 *} |
|
543 |
|
544 locale finite_prod_nat = finite_prod + |
|
545 assumes "False ==> prod f (A::nat set) = prod f A" |
|
546 |
|
547 lemma (in finite_prod_nat) natSum_0 [simp]: |
|
548 "f \<in> {0::nat} -> carrier G ==> prod f {..0} = f 0" |
|
549 by (simp add: Pi_def) |
474 by (simp add: Pi_def) |
550 |
475 |
551 lemma (in finite_prod_nat) natsum_Suc [simp]: |
476 lemma (in abelian_monoid) finprod_Suc [simp]: |
552 "f \<in> {..Suc n} -> carrier G ==> |
477 "f : {..Suc n} -> carrier G ==> |
553 prod f {..Suc n} = (f (Suc n) \<otimes> prod f {..n})" |
478 finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})" |
554 by (simp add: Pi_def atMost_Suc) |
479 by (simp add: Pi_def atMost_Suc) |
555 |
480 |
556 lemma (in finite_prod_nat) natsum_Suc2: |
481 lemma (in abelian_monoid) finprod_Suc2: |
557 "f \<in> {..Suc n} -> carrier G ==> |
482 "f : {..Suc n} -> carrier G ==> |
558 prod f {..Suc n} = (prod (%i. f (Suc i)) {..n} \<otimes> f 0)" |
483 finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)" |
559 proof (induct n) |
484 proof (induct n) |
560 case 0 thus ?case by (simp add: Pi_def) |
485 case 0 thus ?case by (simp add: Pi_def) |
561 next |
486 next |
562 case Suc thus ?case by (simp add: m_assoc Pi_def prod_closed) |
487 case Suc thus ?case by (simp add: m_assoc Pi_def finprod_closed) |
563 qed |
488 qed |
564 |
489 |
565 lemma (in finite_prod_nat) natsum_zero [simp]: |
490 lemma (in abelian_monoid) finprod_mult [simp]: |
566 "prod (%i. \<one>) {..n::nat} = \<one>" |
491 "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==> |
567 by (induct n) (simp_all add: Pi_def) |
492 finprod G (%i. f i \<otimes> g i) {..n::nat} = |
568 |
493 finprod G f {..n} \<otimes> finprod G g {..n}" |
569 lemma (in finite_prod_nat) natsum_add [simp]: |
494 by (induct n) (simp_all add: ac Pi_def finprod_closed) |
570 "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==> |
|
571 prod (%i. f i \<otimes> g i) {..n::nat} = prod f {..n} \<otimes> prod g {..n}" |
|
572 by (induct n) (simp_all add: ac Pi_def prod_closed) |
|
573 |
|
574 ML_setup {* |
|
575 |
|
576 Context.>> (fn thy => (simpset_ref_of thy := |
|
577 simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *} |
|
578 |
|
579 ML_setup {* |
|
580 |
|
581 Context.>> (fn thy => (simpset_ref_of thy := |
|
582 simpset_of thy setsubgoaler asm_simp_tac; thy)) *} |
|
583 |
495 |
584 end |
496 end |
|
497 |