summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | chaieb |

Wed, 04 Mar 2009 19:21:56 +0000 | |

changeset 30264 | 2e8a7d86321e |

parent 30263 | c88af4619a73 |

child 30265 | 2ec2df1a1665 |

Moved general theorems about sums and products to FiniteSet.thy

--- a/src/HOL/Library/Pocklington.thy Wed Mar 04 19:21:56 2009 +0000 +++ b/src/HOL/Library/Pocklington.thy Wed Mar 04 19:21:56 2009 +0000 @@ -554,12 +554,6 @@ (* Fermat's Little theorem / Fermat-Euler theorem. *) -lemma (in comm_monoid_mult) fold_image_related: - assumes Re: "R e e" - and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" - and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)" - shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)" - using fS by (rule finite_subset_induct) (insert assms, auto) lemma nproduct_mod: assumes fS: "finite S" and n0: "n \<noteq> 0" @@ -585,26 +579,6 @@ using fS unfolding setprod_def by (rule finite_subset_induct) (insert Sn, auto simp add: coprime_mul) -lemma (in comm_monoid_mult) - fold_image_eq_general: - assumes fS: "finite S" - and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" - and f12: "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x" - shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'" -proof- - from h f12 have hS: "h ` S = S'" by auto - {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y" - from f12 h H have "x = y" by auto } - hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast - from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto - from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp - also have "\<dots> = fold_image (op *) (f2 o h) e S" - using fold_image_reindex[OF fS hinj, of f2 e] . - also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e] - by blast - finally show ?thesis .. -qed - lemma fermat_little: assumes an: "coprime a n" shows "[a ^ (\<phi> n) = 1] (mod n)" proof- @@ -1287,5 +1261,4 @@ show ?thesis by blast qed - end