diff -r c88af4619a73 -r 2e8a7d86321e src/HOL/Library/Pocklington.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