src/HOL/Library/Pocklington.thy

   ultimately show ?thesis by auto
 qed
 
 (* 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"
   shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)"
 proof-

 lemma coprime_nproduct:
   assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
   shows "coprime n (setprod a S)"
   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-
   {assume "n=0" hence ?thesis by simp}

     have "coprime (a ^ ((n - 1) div p) - 1) n" by (simp add: coprime_commute) }
   with pocklington[OF n qrn[symmetric] nq2 an1]
   show ?thesis by blast    
 qed
 
-
 end