src/HOL/Library/Pocklington.thy

--- a/src/HOL/Library/Pocklington.thy	Wed Nov 19 17:54:55 2008 +0100
+++ b/src/HOL/Library/Pocklington.thy	Wed Nov 19 17:55:18 2008 +0100
@@ -554,11 +554,11 @@
 
 (* Fermat's Little theorem / Fermat-Euler theorem.                           *)
 
-lemma (in comm_monoid_mult) fold_related: 
+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 (op *) h e S) (fold (op *) g e S)"
+  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:
@@ -571,7 +571,7 @@
     [x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)"
     by blast
   have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def)
-  from fold_related[where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis unfolding setprod_def by (simp add: fS)
+  from fold_image_related[where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis unfolding setprod_def by (simp add: fS)
 qed
 
 lemma nproduct_cmul:
@@ -586,21 +586,21 @@
     (insert Sn, auto simp add: coprime_mul)
 
 lemma (in comm_monoid_mult) 
-  fold_eq_general:
+  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 (op *) f1 e S = fold (op *) f2 e S'"
+  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 (op *) f2 e S' = fold (op *) f2 e (h ` S)" by simp
-  also have "\<dots> = fold (op *) (f2 o h) e S" 
-    using fold_reindex[OF fS hinj, of f2 e] .
-  also have "\<dots> = fold (op *) f1 e S " using th fold_cong[OF fS, of "f2 o h" f1 e]
+  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
@@ -633,9 +633,9 @@
       have "a\<noteq>0" using an n1 nz apply- apply (rule ccontr) by simp
       hence inj: "inj_on (op * a) ?S" unfolding inj_on_def by simp
       
-      have eq0: "fold op * (?h \<circ> op * a) 1 {m. coprime m n \<and> m < n} =
-     fold op * (\<lambda>m. m) 1 {m. coprime m n \<and> m < n}"
-      proof (rule fold_eq_general[where h="?h o (op * a)"])
+      have eq0: "fold_image op * (?h \<circ> op * a) 1 {m. coprime m n \<and> m < n} =
+     fold_image op * (\<lambda>m. m) 1 {m. coprime m n \<and> m < n}"
+      proof (rule fold_image_eq_general[where h="?h o (op * a)"])
 	show "finite ?S" using fS .
       next
 	{fix y assume yS: "y \<in> ?S" hence y: "coprime y n" "y < n" by simp_all