Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
authorpaulson <lp15@cam.ac.uk>
Wed Feb 05 17:06:11 2014 +0000 (2014-02-05)
changeset 553375d45fb978d5a
parent 55334 5f5104069b33
child 55338 6e8eff6208dc
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 05 11:47:56 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 05 17:06:11 2014 +0000
     1.3 @@ -504,7 +504,7 @@
     1.4    apply (drule_tac x = "a - 1" in spec)
     1.5    apply force
     1.6    apply (cases "a = 0")
     1.7 -  apply (auto simp add: cong_0_1_nat') [1]
     1.8 +  apply (metis add_is_0 cong_0_1_nat zero_neq_one)
     1.9    apply (rule iffI)
    1.10    apply (drule cong_to_1_nat)
    1.11    apply (unfold dvd_def)
    1.12 @@ -605,7 +605,7 @@
    1.13    done
    1.14  
    1.15  lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
    1.16 -  apply (auto intro: cong_solve_coprime_nat)
    1.17 +  apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
    1.18    apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
    1.19    apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
    1.20        gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
     2.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 05 11:47:56 2014 +0100
     2.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 05 17:06:11 2014 +0000
     2.3 @@ -280,7 +280,8 @@
     2.4      \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
     2.5      m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
     2.6    case True then show ?thesis
     2.7 -    apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
     2.8 +    apply (auto simp add: One_nat_def numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
     2.9 +        dest: prime_gt_Suc_0_nat)
    2.10      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
    2.11      apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
    2.12      done
     3.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 05 11:47:56 2014 +0100
     3.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 05 17:06:11 2014 +0000
     3.3 @@ -37,9 +37,9 @@
     3.4        {assume "q = p" hence ?lhs using q(1) by blast}
     3.5        moreover
     3.6        {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
     3.7 -        from H[rule_format, of q] qplt q0 have "coprime p q" by arith
     3.8 -       hence ?lhs
     3.9 -         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat q(1) q(2))}
    3.10 +        from H qplt q0 have "coprime p q" by arith
    3.11 +       hence ?lhs using q
    3.12 +         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}
    3.13        ultimately have ?lhs by blast}
    3.14      ultimately have ?thesis by blast}
    3.15    ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
    3.16 @@ -65,7 +65,7 @@
    3.17    from dxy(1,2) have d1: "d = 1"
    3.18      by (metis assms coprime_nat) 
    3.19    hence "a*x*b = (n*y + 1)*b" using dxy(3) by simp
    3.20 -  hence "a*(x*b) = n*(y*b) + b"
    3.21 +  hence "a*(x*b) = n*(y*b) + b" 
    3.22      by (auto simp add: algebra_simps)
    3.23    hence "a*(x*b) mod n = (n*(y*b) + b) mod n" by simp
    3.24    hence "a*(x*b) mod n = b mod n" by (simp add: mod_add_left_eq)
    3.25 @@ -112,7 +112,6 @@
    3.26  qed
    3.27  
    3.28  lemma cong_unique_inverse_prime:
    3.29 -  fixes p::nat 
    3.30    assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
    3.31    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
    3.32  by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
    3.33 @@ -158,8 +157,7 @@
    3.34      by auto
    3.35    also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
    3.36      apply (rule card_mono) using assms
    3.37 -    apply (auto simp add: )
    3.38 -    by (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
    3.39 +    by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
    3.40    also have "... = phi n"
    3.41      by (simp add: phi_def)
    3.42    finally show ?thesis .
    3.43 @@ -220,16 +218,7 @@
    3.44  qed
    3.45  
    3.46  lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
    3.47 -  (is "?lhs \<longleftrightarrow> ?rhs")
    3.48 -proof
    3.49 -  assume ?rhs thus ?lhs by blast
    3.50 -next
    3.51 -  assume H: ?lhs then obtain n where n: "P n" by blast
    3.52 -  let ?x = "Least P"
    3.53 -  {fix m assume m: "m < ?x"
    3.54 -    from not_less_Least[OF m] have "\<not> P m" .}
    3.55 -  with LeastI_ex[OF H] show ?rhs by blast
    3.56 -qed
    3.57 +  by (metis ex_least_nat_le not_less0)
    3.58  
    3.59  lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> (P (Least P) \<and> (\<forall>m < (Least P). \<not> P m))"
    3.60    (is "?lhs \<longleftrightarrow> ?rhs")
    3.61 @@ -288,13 +277,15 @@
    3.62      hence th: "prime p \<and> p dvd n - 1" unfolding r by (auto intro: dvd_mult)
    3.63      have "(a ^ ((n - 1) div p)) mod n = (a^(m*r div p)) mod n" using r
    3.64        by (simp add: power_mult)
    3.65 -    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
    3.66 +    also have "\<dots> = (a^(m*(r div p))) mod n" 
    3.67 +      using div_mult1_eq[of m r p] p(2)[unfolded dvd_eq_mod_eq_0] 
    3.68 +      by simp
    3.69      also have "\<dots> = ((a^m)^(r div p)) mod n" by (simp add: power_mult)
    3.70 -    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod[of "a^m" "n" "r div p" ] ..
    3.71 -    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def power_Suc_0)
    3.72 +    also have "\<dots> = ((a^m mod n)^(r div p)) mod n" using power_mod ..
    3.73 +    also have "\<dots> = 1" using m(3) onen by (simp add: cong_nat_def)
    3.74      finally have "[(a ^ ((n - 1) div p))= 1] (mod n)"
    3.75        using onen by (simp add: cong_nat_def)
    3.76 -    with pn[rule_format, OF th] have False by blast}
    3.77 +    with pn th have False by blast}
    3.78    hence th: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)" by blast
    3.79    from lucas_weak[OF n2 an1 th] show ?thesis .
    3.80  qed
    3.81 @@ -333,7 +324,7 @@
    3.82    shows "[a ^ (ord n a) = 1] (mod n) \<and> (\<forall>m. 0 < m \<and> m < ord n a \<longrightarrow> ~[a^ m = 1] (mod n))"
    3.83  apply (cases "coprime n a")
    3.84  using coprime_ord[of n a]
    3.85 -by (blast, simp add: ord_def cong_nat_def)
    3.86 +by (auto simp add: ord_def cong_nat_def)
    3.87  
    3.88  lemma ord:
    3.89    fixes n::nat
    3.90 @@ -378,8 +369,9 @@
    3.91        obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
    3.92          by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
    3.93        hence "a ^ d + n * q1 - n * q2 = 1" by simp
    3.94 -      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' 
    3.95 -      have "p dvd 1" by simp
    3.96 +      with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
    3.97 +      have "p dvd 1"
    3.98 +        by metis
    3.99        with p(3) have False by simp
   3.100        hence ?rhs ..}
   3.101      ultimately have ?rhs by blast}
   3.102 @@ -453,31 +445,24 @@
   3.103  subsection{*Another trivial primality characterization*}
   3.104  
   3.105  lemma prime_prime_factor:
   3.106 -  "prime n \<longleftrightarrow> n \<noteq> 1\<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)"
   3.107 -proof-
   3.108 -  {assume n: "n=0 \<or> n=1" 
   3.109 -   hence ?thesis
   3.110 -     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat) }
   3.111 -  moreover
   3.112 -  {assume n: "n\<noteq>0" "n\<noteq>1"
   3.113 -    {assume pn: "prime n"
   3.114 -
   3.115 -      from pn[unfolded prime_def] have "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
   3.116 -        using n
   3.117 -        apply (cases "n = 0 \<or> n=1",simp)
   3.118 -        by (clarsimp, erule_tac x="p" in allE, auto)}
   3.119 -    moreover
   3.120 -    {assume H: "\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n"
   3.121 -      from n have n1: "n > 1" by arith
   3.122 -      {fix m assume m: "m dvd n" "m\<noteq>1"
   3.123 -       then obtain p where p: "prime p" "p dvd m"
   3.124 -         by (metis prime_factor_nat) 
   3.125 -       from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
   3.126 -       with p(2) have "n dvd m"  by simp
   3.127 -       hence "m=n"  using dvd_antisym[OF m(1)] by simp }
   3.128 -      with n1 have "prime n"  unfolding prime_def by auto }
   3.129 -    ultimately have ?thesis using n by blast}
   3.130 -  ultimately       show ?thesis by auto
   3.131 +  "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>p. prime p \<and> p dvd n \<longrightarrow> p = n)" 
   3.132 +  (is "?lhs \<longleftrightarrow> ?rhs")
   3.133 +proof (cases "n=0 \<or> n=1")
   3.134 +  case True
   3.135 +  then show ?thesis
   3.136 +     by (metis bigger_prime dvd_0_right one_not_prime_nat zero_not_prime_nat)
   3.137 +next
   3.138 +  case False
   3.139 +  show ?thesis
   3.140 +  proof
   3.141 +    assume "prime n"
   3.142 +    then show ?rhs
   3.143 +      by (metis one_not_prime_nat prime_nat_def)
   3.144 +  next
   3.145 +    assume ?rhs
   3.146 +    with False show "prime n"
   3.147 +      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)
   3.148 +  qed
   3.149  qed
   3.150  
   3.151  lemma prime_divisor_sqrt:
   3.152 @@ -528,19 +513,14 @@
   3.153      {assume H: ?lhs
   3.154        from H[unfolded prime_divisor_sqrt] n
   3.155        have ?rhs
   3.156 -        apply clarsimp
   3.157 -        apply (erule_tac x="p" in allE)
   3.158 -        apply simp
   3.159 -        done
   3.160 -    }
   3.161 +        by (metis prime_prime_factor) }
   3.162      moreover
   3.163      {assume H: ?rhs
   3.164        {fix d assume d: "d dvd n" "d\<^sup>2 \<le> n" "d\<noteq>1"
   3.165          then obtain p where p: "prime p" "p dvd d"
   3.166            by (metis prime_factor_nat) 
   3.167 -        from n have np: "n > 0" by arith
   3.168 -        from d(1) n have "d \<noteq> 0" by - (rule ccontr, auto)
   3.169 -        hence dp: "d > 0" by arith
   3.170 +        from d(1) n have dp: "d > 0"
   3.171 +          by (metis dvd_0_left neq0_conv) 
   3.172          from mult_mono[OF dvd_imp_le[OF p(2) dp] dvd_imp_le[OF p(2) dp]] d(2)
   3.173          have "p\<^sup>2 \<le> n" unfolding power2_eq_square by arith
   3.174          with H n p(1) dvd_trans[OF p(2) d(1)] have False  by blast}
   3.175 @@ -589,10 +569,8 @@
   3.176        by (metis mult_assoc mult_commute)
   3.177      hence exps: "a^(ord p (a^r) * t*r) = ((a ^ r) ^ ord p (a^r)) ^ t"
   3.178        by (simp only: power_mult)
   3.179 -    have "[((a ^ r) ^ ord p (a^r)) ^ t= 1^t] (mod p)"
   3.180 -      by (metis cong_exp_nat ord)
   3.181      then have th: "[((a ^ r) ^ ord p (a^r)) ^ t= 1] (mod p)"
   3.182 -      by simp
   3.183 +      by (metis cong_exp_nat ord power_one)
   3.184      have pd0: "p dvd a^(ord p (a^r) * t*r) - 1"
   3.185        by (metis cong_to_1_nat exps th)
   3.186      from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r" using P0 by simp
   3.187 @@ -613,7 +591,8 @@
   3.188      by (metis coprime_exp_nat cpa gcd_nat.commute) 
   3.189    from euler_theorem_nat[OF arp, simplified ord_divides] o phip
   3.190    have "q dvd (p - 1)" by simp
   3.191 -  then obtain d where d:"p - 1 = q * d" unfolding dvd_def by blast
   3.192 +  then obtain d where d:"p - 1 = q * d" 
   3.193 +    unfolding dvd_def by blast
   3.194    have p0:"p \<noteq> 0"
   3.195      by (metis p01(1)) 
   3.196    from p0 d have "p + q * 0 = 1 + q * d" by simp
   3.197 @@ -769,7 +748,8 @@
   3.198  proof-
   3.199    from bqn psp qrn
   3.200    have bqn: "a ^ (n - 1) mod n = 1"
   3.201 -    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
   3.202 +    and psp: "list_all (\<lambda>p. prime p \<and> coprime (a^(r *(q div p)) mod n - 1) n) ps"  
   3.203 +    unfolding arnb[symmetric] power_mod 
   3.204      by (simp_all add: power_mult[symmetric] algebra_simps)
   3.205    from n  have n0: "n > 0" by arith
   3.206    from mod_div_equality[of "a^(n - 1)" n]
     4.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 11:47:56 2014 +0100
     4.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 05 17:06:11 2014 +0000
     4.3 @@ -31,7 +31,6 @@
     4.4  imports "~~/src/HOL/GCD"
     4.5  begin
     4.6  
     4.7 -declare One_nat_def [simp]
     4.8  declare [[coercion int]]
     4.9  declare [[coercion_enabled]]
    4.10  
    4.11 @@ -408,9 +407,7 @@
    4.12    let ?q2 = "v * y1 + u * x2"
    4.13    from dxy2(3)[simplified d12] dxy1(3)[simplified d12] 
    4.14    have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
    4.15 -    apply (auto simp add: algebra_simps) 
    4.16 -    apply (metis mult_Suc_right nat_mult_assoc nat_mult_commute)+
    4.17 -    done
    4.18 +    by algebra+
    4.19    thus ?thesis by blast
    4.20  qed
    4.21