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