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