# HG changeset patch
# User chaieb
# Date 1204119592 -3600
# Node ID 9dc286ee452b34f16109813a4392b1ce4be2721b
# Parent  4d9d0a26c32a14b591162b364b4f4d9fd3174fa8
Fixed proofs

diff -r 4d9d0a26c32a -r 9dc286ee452b src/HOL/Library/Pocklington.thy
--- a/src/HOL/Library/Pocklington.thy	Wed Feb 27 14:39:51 2008 +0100
+++ b/src/HOL/Library/Pocklington.thy	Wed Feb 27 14:39:52 2008 +0100
@@ -825,7 +825,8 @@
 	by (simp add: ring_simps power_mult)
       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n" 
 	using power_mod[of "a^m" n "(n - 1) div m"] by simp
-      also have "\<dots> = 1" using m(3)[unfolded modeq_def onen] onen by simp
+      also have "\<dots> = 1" using m(3)[unfolded modeq_def onen] onen 
+	by (simp add: power_Suc0)
       finally have th3: "?y mod n = 1"  . 
       have th2: "[?y * a ^ ((n - 1) mod m) = ?y* 1] (mod n)" 
 	using an1[unfolded modeq_def onen] onen
@@ -847,7 +848,7 @@
     also have "\<dots> = (a^(m*(r div p))) mod n" using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] by simp
     also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
     also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..
-    also have "\<dots> = 1" using m(3) onen by (simp add: modeq_def)
+    also have "\<dots> = 1" using m(3) onen by (simp add: modeq_def power_Suc0)
     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)" 
       using onen by (simp add: modeq_def)
     with pn[rule_format, OF th] have False by blast}
@@ -899,7 +900,8 @@
   hence "[a ^ d = (a ^ (ord n a) mod n)^k] (mod n)"
     by (simp add : modeq_def power_mult power_mod)
   also have "[(a ^ (ord n a) mod n)^k = 1] (mod n)" 
-    using ord[of a n, unfolded modeq_def] by (simp add: modeq_def power_mod)
+    using ord[of a n, unfolded modeq_def] 
+    by (simp add: modeq_def power_mod power_Suc0)
   finally  show ?lhs .
 next 
   assume lh: ?lhs
@@ -923,7 +925,7 @@
     let ?q = "d div ord n a"
     let ?r = "d mod ord n a"
     from cong_exp[OF ord[of a n], of ?q] 
-    have eqo: "[(a^?o)^?q = 1] (mod n)"  by (simp add: modeq_def)
+    have eqo: "[(a^?o)^?q = 1] (mod n)"  by (simp add: modeq_def power_Suc0)
     from H have onz: "?o \<noteq> 0" by (simp add: ord_eq_0)
     hence op: "?o > 0" by simp
     from mod_div_equality[of d "ord n a"] lh
@@ -1105,7 +1107,8 @@
       by (simp only: power_mult)
     have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)" 
       by (rule cong_exp, rule ord)
-    then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" by simp
+    then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)" 
+      by (simp add: power_Suc0)
     from cong_1_divides[OF th] exps have pd0: "p dvd a^(ord p (a^r) * t*r) - 1" by simp
     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
     with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp