# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1391619971 0
# Node ID 5d45fb978d5ac6453878c3bd61eaa28d585450b3
# Parent  5f5104069b3339d9a1448e3d82e69116587b895a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.

diff -r 5f5104069b33 -r 5d45fb978d5a src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 05 17:06:11 2014 +0000
@@ -504,7 +504,7 @@
   apply (drule_tac x = "a - 1" in spec)
   apply force
   apply (cases "a = 0")
-  apply (auto simp add: cong_0_1_nat') [1]
+  apply (metis add_is_0 cong_0_1_nat zero_neq_one)
   apply (rule iffI)
   apply (drule cong_to_1_nat)
   apply (unfold dvd_def)
@@ -605,7 +605,7 @@
   done
 
 lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
-  apply (auto intro: cong_solve_coprime_nat)
+  apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
   apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
   apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
       gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
diff -r 5f5104069b33 -r 5d45fb978d5a src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 05 17:06:11 2014 +0000
@@ -280,7 +280,8 @@
     \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
     m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
   case True then show ?thesis
-    apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
+    apply (auto simp add: One_nat_def numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
+        dest: prime_gt_Suc_0_nat)
     apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
     apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
     done
diff -r 5f5104069b33 -r 5d45fb978d5a src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 05 17:06:11 2014 +0000
@@ -37,9 +37,9 @@
       {assume "q = p" hence ?lhs using q(1) by blast}
       moreover
       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
-        from H[rule_format, of q] qplt q0 have "coprime p q" by arith
-       hence ?lhs
-         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat q(1) q(2))}
+        from H qplt q0 have "coprime p q" by arith
+       hence ?lhs using q
+         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}
       ultimately have ?lhs by blast}
     ultimately have ?thesis by blast}
   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
@@ -65,7 +65,7 @@
   from dxy(1,2) have d1: "d = 1"
     by (metis assms coprime_nat) 
   hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
-  hence "a*(x*b) = n*(y*b) + b"
+  hence "a*(x*b) = n*(y*b) + b" 
     by (auto simp add: algebra_simps)
   hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
   hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
@@ -112,7 +112,6 @@
 qed
 
 lemma cong_unique_inverse_prime:
-  fixes p::nat 
   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
 by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
@@ -158,8 +157,7 @@
     by auto
   also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
     apply (rule card_mono) using assms
-    apply (auto simp add: )
-    by (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
+    by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
   also have "... = phi n"
     by (simp add: phi_def)
   finally show ?thesis .
@@ -220,16 +218,7 @@
 qed
 
 lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?rhs thus ?lhs by blast
-next
-  assume H: ?lhs then obtain n where n: "P n" by blast
-  let ?x = "Least P"
-  {fix m assume m: "m < ?x"
-    from not_less_Least[OF m] have "\<not> P m" .}
-  with LeastI_ex[OF H] show ?rhs by blast
-qed
+  by (metis ex_least_nat_le not_less0)
 
 lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -288,13 +277,15 @@
     hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
     have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
       by (simp add: power_mult)
-    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" 
+      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: cong_nat_def power_Suc_0)
+    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..
+    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)
     finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
       using onen by (simp add: cong_nat_def)
-    with pn[rule_format, OF th] have False by blast}
+    with pn th have False by blast}
   hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
   from lucas_weak[OF n2 an1 th] show ?thesis .
 qed
@@ -333,7 +324,7 @@
   shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
 apply (cases "coprime n a")
 using coprime_ord[of n a]
-by (blast, simp add: ord_def cong_nat_def)
+by (auto simp add: ord_def cong_nat_def)
 
 lemma ord:
   fixes n::nat
@@ -378,8 +369,9 @@
       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
         by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
       hence "a ^ d + n * q1 - n * q2 = 1" by simp
-      with dvd_diff_nat [OF dvd_add [OF divides_rexp[OF p(2), of d'] dvd_mult2[OF p(1), of q1]] dvd_mult2[OF p(1), of q2]] d' 
-      have "p dvd 1" by simp
+      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
+      have "p dvd 1"
+        by metis
       with p(3) have False by simp
       hence ?rhs ..}
     ultimately have ?rhs by blast}
@@ -453,31 +445,24 @@
 subsection{*Another trivial primality characterization*}
 
 lemma prime_prime_factor:
-  "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
-proof-
-  {assume n: "n=0 \<or> n=1" 
-   hence ?thesis
-     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) }
-  moreover
-  {assume n: "n\<noteq>0" "n\<noteq>1"
-    {assume pn: "prime n"
-
-      from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
-        using n
-        apply (cases "n = 0 \<or> n=1",simp)
-        by (clarsimp, erule_tac x="p" in allE, auto)}
-    moreover
-    {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
-      from n have n1: "n > 1" by arith
-      {fix m assume m: "m dvd n" "m\<noteq>1"
-       then obtain p where p: "prime p" "p dvd m"
-         by (metis prime_factor_nat) 
-       from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
-       with p(2) have "n dvd m"  by simp
-       hence "m=n"  using dvd_antisym[OF m(1)] by simp }
-      with n1 have "prime n"  unfolding prime_def by auto }
-    ultimately have ?thesis using n by blast}
-  ultimately       show ?thesis by auto
+  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof (cases "n=0 \<or> n=1")
+  case True
+  then show ?thesis
+     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
+next
+  case False
+  show ?thesis
+  proof
+    assume "prime n"
+    then show ?rhs
+      by (metis one_not_prime_nat prime_nat_def)
+  next
+    assume ?rhs
+    with False show "prime n"
+      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)
+  qed
 qed
 
 lemma prime_divisor_sqrt:
@@ -528,19 +513,14 @@
     {assume H: ?lhs
       from H[unfolded prime_divisor_sqrt] n
       have ?rhs
-        apply clarsimp
-        apply (erule_tac x="p" in allE)
-        apply simp
-        done
-    }
+        by (metis prime_prime_factor) }
     moreover
     {assume H: ?rhs
       {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
         then obtain p where p: "prime p" "p dvd d"
           by (metis prime_factor_nat) 
-        from n have np: "n > 0" by arith
-        from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
-        hence dp: "d > 0" by arith
+        from d(1) n have dp: "d > 0"
+          by (metis dvd_0_left neq0_conv) 
         from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
         have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
         with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
@@ -589,10 +569,8 @@
       by (metis mult_assoc mult_commute)
     hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
       by (simp only: power_mult)
-    have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)"
-      by (metis cong_exp_nat ord)
     then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
-      by simp
+      by (metis cong_exp_nat ord power_one)
     have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
       by (metis cong_to_1_nat exps th)
     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
@@ -613,7 +591,8 @@
     by (metis coprime_exp_nat cpa gcd_nat.commute) 
   from euler_theorem_nat[OF arp, simplified ord_divides] o phip
   have "q dvd (p - 1)" by simp
-  then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast
+  then obtain d where d:"p - 1 = q * d" 
+    unfolding dvd_def by blast
   have p0:"p \<noteq> 0"
     by (metis p01(1)) 
   from p0 d have "p + q * 0 = 1 + q * d" by simp
@@ -769,7 +748,8 @@
 proof-
   from bqn psp qrn
   have bqn: "a ^ (n - 1) mod n = 1"
-    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  unfolding arnb[symmetric] power_mod
+    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  
+    unfolding arnb[symmetric] power_mod 
     by (simp_all add: power_mult[symmetric] algebra_simps)
   from n  have n0: "n > 0" by arith
   from mod_div_equality[of "a^(n - 1)" n]
diff -r 5f5104069b33 -r 5d45fb978d5a src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 11:47:56 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 17:06:11 2014 +0000
@@ -31,7 +31,6 @@
 imports "~~/src/HOL/GCD"
 begin
 
-declare One_nat_def [simp]
 declare [[coercion int]]
 declare [[coercion_enabled]]
 
@@ -408,9 +407,7 @@
   let ?q2 = "v * y1 + u * x2"
   from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
-    apply (auto simp add: algebra_simps) 
-    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
-    done
+    by algebra+
   thus ?thesis by blast
 qed