515 using not0_implies_Suc by blast |
515 using not0_implies_Suc by blast |
516 thus ?thesis |
516 thus ?thesis |
517 using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp |
517 using finprod_Suc[of f k] assms atMost_Suc lessThan_Suc_atMost by simp |
518 qed |
518 qed |
519 |
519 |
520 (* The following two were contributed by Jeremy Avigad. *) |
520 lemma finprod_reindex: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close> |
521 |
|
522 lemma finprod_reindex: |
|
523 "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow> |
521 "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow> |
524 inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A" |
522 inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A" |
525 proof (induct A rule: infinite_finite_induct) |
523 proof (induct A rule: infinite_finite_induct) |
526 case (infinite A) |
524 case (infinite A) |
527 hence "\<not> finite (h ` A)" |
525 hence "\<not> finite (h ` A)" |
528 using finite_imageD by blast |
526 using finite_imageD by blast |
529 with \<open>\<not> finite A\<close> show ?case by simp |
527 with \<open>\<not> finite A\<close> show ?case by simp |
530 qed (auto simp add: Pi_def) |
528 qed (auto simp add: Pi_def) |
531 |
529 |
532 lemma finprod_const: |
530 lemma finprod_const: \<^marker>\<open>contributor \<open>Jeremy Avigad\<close>\<close> |
533 assumes a [simp]: "a \<in> carrier G" |
531 assumes a [simp]: "a \<in> carrier G" |
534 shows "finprod G (\<lambda>x. a) A = a [^] card A" |
532 shows "finprod G (\<lambda>x. a) A = a [^] card A" |
535 proof (induct A rule: infinite_finite_induct) |
533 proof (induct A rule: infinite_finite_induct) |
536 case (insert b A) |
534 case (insert b A) |
537 show ?case |
535 show ?case |
539 show "a \<otimes> (\<Otimes>x\<in>A. a) = a [^] card (insert b A)" |
537 show "a \<otimes> (\<Otimes>x\<in>A. a) = a [^] card (insert b A)" |
540 by (insert insert, auto, subst m_comm, auto) |
538 by (insert insert, auto, subst m_comm, auto) |
541 qed auto |
539 qed auto |
542 qed auto |
540 qed auto |
543 |
541 |
544 (* The following lemma was contributed by Jesus Aransay. *) |
542 lemma finprod_singleton: \<^marker>\<open>contributor \<open>Jesus Aransay\<close>\<close> |
545 |
|
546 lemma finprod_singleton: |
|
547 assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G" |
543 assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G" |
548 shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i" |
544 shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i" |
549 using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"] |
545 using i_in_A finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"] |
550 fin_A f_Pi finprod_one [of "A - {i}"] |
546 fin_A f_Pi finprod_one [of "A - {i}"] |
551 finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] |
547 finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] |