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```