author paulson Wed Feb 05 17:06:11 2014 +0000 (2014-02-05) changeset 55337 5d45fb978d5a 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 file | annotate | diff | revisions src/HOL/Number_Theory/Eratosthenes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Pocklington.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions
```     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.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.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.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
```