src/HOL/Number_Theory/Primes.thy
 changeset 59669 de7792ea4090 parent 59667 651ea265d568 child 59730 b7c394c7a619
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 15:21:26 2015 +0000
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 16:12:35 2015 +0000
1.3 @@ -28,7 +28,7 @@
1.4  section {* Primes *}
1.5
1.6  theory Primes
1.7 -imports "~~/src/HOL/GCD" "~~/src/HOL/Fact"
1.8 +imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
1.9  begin
1.10
1.11  declare [[coercion int]]
1.12 @@ -72,7 +72,7 @@
1.13    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
1.14    done
1.15
1.16 -lemma prime_int_altdef:
1.17 +lemma prime_int_altdef:
1.18    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
1.19      m = 1 \<or> m = p))"
1.20    apply (simp add: prime_def)
1.21 @@ -90,7 +90,7 @@
1.22  lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.23    by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
1.24
1.25 -lemma prime_dvd_mult_int:
1.26 +lemma prime_dvd_mult_int:
1.27    fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1.28    by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
1.29
1.30 @@ -99,7 +99,7 @@
1.31    by (rule iffI, rule prime_dvd_mult_nat, auto)
1.32
1.33  lemma prime_dvd_mult_eq_int [simp]:
1.34 -  fixes n::int
1.35 +  fixes n::int
1.36    shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
1.37    by (rule iffI, rule prime_dvd_mult_int, auto)
1.38
1.39 @@ -121,7 +121,7 @@
1.40    by (cases n) (auto elim: prime_dvd_power_nat)
1.41
1.42  lemma prime_dvd_power_int_iff:
1.43 -  fixes x::int
1.44 +  fixes x::int
1.45    shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
1.46    by (cases n) (auto elim: prime_dvd_power_int)
1.47
1.48 @@ -226,14 +226,14 @@
1.49
1.50  lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
1.51  proof-
1.52 -  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
1.53 +  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
1.54    from prime_factor_nat [OF f1]
1.55    obtain p where "prime p" and "p dvd fact n + 1" by auto
1.56    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
1.57    { assume "p \<le> n"
1.58 -    from `prime p` have "p \<ge> 1"
1.59 +    from `prime p` have "p \<ge> 1"
1.60        by (cases p, simp_all)
1.61 -    with `p <= n` have "p dvd fact n"
1.62 +    with `p <= n` have "p dvd fact n"
1.63        by (intro dvd_fact_nat)
1.64      with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
1.65        by (rule dvd_diff_nat)
1.66 @@ -245,7 +245,7 @@
1.67    with `prime p` and `p <= fact n + 1` show ?thesis by auto
1.68  qed
1.69
1.70 -lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
1.71 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
1.72    using next_prime_bound by auto
1.73
1.74  lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
1.75 @@ -263,12 +263,12 @@
1.76
1.77  text{*Versions for type nat only*}
1.78
1.79 -lemma prime_product:
1.80 +lemma prime_product:
1.81    fixes p::nat
1.82    assumes "prime (p * q)"
1.83    shows "p = 1 \<or> q = 1"
1.84  proof -
1.85 -  from assms have
1.86 +  from assms have
1.87      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
1.88      unfolding prime_nat_def by auto
1.89    from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
1.90 @@ -278,7 +278,7 @@
1.91    then show ?thesis by (simp add: Q)
1.92  qed
1.93
1.94 -lemma prime_exp:
1.95 +lemma prime_exp:
1.96    fixes p::nat
1.97    shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
1.98  proof(induct n)
1.99 @@ -301,7 +301,7 @@
1.100    ultimately show ?case by blast
1.101  qed
1.102
1.103 -lemma prime_power_mult:
1.104 +lemma prime_power_mult:
1.105    fixes p::nat
1.106    assumes p: "prime p" and xy: "x * y = p ^ k"
1.107    shows "\<exists>i j. x = p ^i \<and> y = p^ j"
1.108 @@ -312,28 +312,28 @@
1.109    case (Suc k x y)
1.110    from Suc.prems have pxy: "p dvd x*y" by auto
1.111    from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
1.112 -  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
1.113 +  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
1.114    {assume px: "p dvd x"
1.115      then obtain d where d: "x = p*d" unfolding dvd_def by blast
1.116      from Suc.prems d  have "p*d*y = p^Suc k" by simp
1.117      hence th: "d*y = p^k" using p0 by simp
1.118      from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
1.119 -    with d have "x = p^Suc i" by simp
1.120 +    with d have "x = p^Suc i" by simp
1.121      with ij(2) have ?case by blast}
1.122 -  moreover
1.123 +  moreover
1.124    {assume px: "p dvd y"
1.125      then obtain d where d: "y = p*d" unfolding dvd_def by blast
1.126      from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
1.127      hence th: "d*x = p^k" using p0 by simp
1.128      from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
1.129 -    with d have "y = p^Suc i" by simp
1.130 +    with d have "y = p^Suc i" by simp
1.131      with ij(2) have ?case by blast}
1.132    ultimately show ?case  using pxyc by blast
1.133  qed
1.134
1.135 -lemma prime_power_exp:
1.136 +lemma prime_power_exp:
1.137    fixes p::nat
1.138 -  assumes p: "prime p" and n: "n \<noteq> 0"
1.139 +  assumes p: "prime p" and n: "n \<noteq> 0"
1.140      and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
1.141    using n xn
1.142  proof(induct n arbitrary: k)
1.143 @@ -343,7 +343,7 @@
1.144    {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
1.145    moreover
1.146    {assume n: "n \<noteq> 0"
1.147 -    from prime_power_mult[OF p th]
1.148 +    from prime_power_mult[OF p th]
1.149      obtain i j where ij: "x = p^i" "x^n = p^j"by blast
1.150      from Suc.hyps[OF n ij(2)] have ?case .}
1.151    ultimately show ?case by blast
1.152 @@ -351,14 +351,14 @@
1.153
1.154  lemma divides_primepow:
1.155    fixes p::nat
1.156 -  assumes p: "prime p"
1.157 +  assumes p: "prime p"
1.158    shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
1.159  proof
1.160 -  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
1.161 +  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
1.162      unfolding dvd_def  apply (auto simp add: mult.commute) by blast
1.163    from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
1.164    from e ij have "p^(i + j) = p^k" by (simp add: power_add)
1.165 -  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
1.166 +  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
1.167    hence "i \<le> k" by arith
1.168    with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
1.169  next
1.170 @@ -375,16 +375,16 @@
1.171  lemma bezout_gcd_nat:
1.172    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
1.173    using bezout_nat[of a b]
1.174 -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
1.175 -  gcd_nat.right_neutral mult_0)
1.176 +by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
1.177 +  gcd_nat.right_neutral mult_0)
1.178
1.179  lemma gcd_bezout_sum_nat:
1.180 -  fixes a::nat
1.181 -  assumes "a * x + b * y = d"
1.182 +  fixes a::nat
1.183 +  assumes "a * x + b * y = d"
1.184    shows "gcd a b dvd d"
1.185  proof-
1.186    let ?g = "gcd a b"
1.187 -    have dv: "?g dvd a*x" "?g dvd b * y"
1.188 +    have dv: "?g dvd a*x" "?g dvd b * y"
1.189        by simp_all
1.190      from dvd_add[OF dv] assms
1.191      show ?thesis by auto
1.192 @@ -393,19 +393,19 @@
1.193
1.194  text {* A binary form of the Chinese Remainder Theorem. *}
1.195
1.196 -lemma chinese_remainder:
1.197 +lemma chinese_remainder:
1.198    fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
1.199    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
1.200  proof-
1.201    from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
1.202 -  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
1.203 +  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
1.204      and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
1.205    then have d12: "d1 = 1" "d2 =1"
1.206      by (metis ab coprime_nat)+
1.207    let ?x = "v * a * x1 + u * b * x2"
1.208    let ?q1 = "v * x1 + u * y2"
1.209    let ?q2 = "v * y1 + u * x2"
1.210 -  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
1.211 +  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
1.212    have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
1.213      by algebra+
1.214    thus ?thesis by blast
1.215 @@ -418,14 +418,14 @@
1.216    shows "\<exists>x y. a * x = b * y + 1"
1.217  by (metis assms bezout_nat gcd_nat.left_neutral)
1.218
1.219 -lemma bezout_prime:
1.220 +lemma bezout_prime:
1.221    assumes p: "prime p" and pa: "\<not> p dvd a"
1.222    shows "\<exists>x y. a*x = Suc (p*y)"
1.223  proof-
1.224    have ap: "coprime a p"
1.225 -    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
1.226 +    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
1.227    from coprime_bezout_strong[OF ap] show ?thesis
1.228 -    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
1.229 +    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
1.230  qed
1.231
1.232  end
```