src/HOL/Number_Theory/Primes.thy
changeset 55215 b6c926e67350
parent 55130 70db8d380d62
child 55238 7ddb889e23bd
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Jan 31 16:41:54 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Jan 31 16:58:58 2014 +0000
     1.3 @@ -351,4 +351,115 @@
     1.4      by auto
     1.5  qed
     1.6  
     1.7 +subsection{*Powers of Primes*}
     1.8 +
     1.9 +text{*Versions for type nat only*}
    1.10 +
    1.11 +lemma prime_product: 
    1.12 +  fixes p::nat
    1.13 +  assumes "prime (p * q)"
    1.14 +  shows "p = 1 \<or> q = 1"
    1.15 +proof -
    1.16 +  from assms have 
    1.17 +    "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
    1.18 +    unfolding prime_nat_def by auto
    1.19 +  from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
    1.20 +  then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
    1.21 +  have "p dvd p * q" by simp
    1.22 +  then have "p = 1 \<or> p = p * q" by (rule P)
    1.23 +  then show ?thesis by (simp add: Q)
    1.24 +qed
    1.25 +
    1.26 +lemma prime_exp: 
    1.27 +  fixes p::nat
    1.28 +  shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
    1.29 +proof(induct n)
    1.30 +  case 0 thus ?case by simp
    1.31 +next
    1.32 +  case (Suc n)
    1.33 +  {assume "p = 0" hence ?case by simp}
    1.34 +  moreover
    1.35 +  {assume "p=1" hence ?case by simp}
    1.36 +  moreover
    1.37 +  {assume p: "p \<noteq> 0" "p\<noteq>1"
    1.38 +    {assume pp: "prime (p^Suc n)"
    1.39 +      hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
    1.40 +      with p have n: "n = 0"
    1.41 +        by (metis One_nat_def nat_power_eq_Suc_0_iff)
    1.42 +      with pp have "prime p \<and> Suc n = 1" by simp}
    1.43 +    moreover
    1.44 +    {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
    1.45 +    ultimately have ?case by blast}
    1.46 +  ultimately show ?case by blast
    1.47 +qed
    1.48 +
    1.49 +lemma prime_power_mult: 
    1.50 +  fixes p::nat
    1.51 +  assumes p: "prime p" and xy: "x * y = p ^ k"
    1.52 +  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
    1.53 +using xy
    1.54 +proof(induct k arbitrary: x y)
    1.55 +  case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
    1.56 +next
    1.57 +  case (Suc k x y)
    1.58 +  from Suc.prems have pxy: "p dvd x*y" by auto
    1.59 +  from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
    1.60 +  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp) 
    1.61 +  {assume px: "p dvd x"
    1.62 +    then obtain d where d: "x = p*d" unfolding dvd_def by blast
    1.63 +    from Suc.prems d  have "p*d*y = p^Suc k" by simp
    1.64 +    hence th: "d*y = p^k" using p0 by simp
    1.65 +    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
    1.66 +    with d have "x = p^Suc i" by simp 
    1.67 +    with ij(2) have ?case by blast}
    1.68 +  moreover 
    1.69 +  {assume px: "p dvd y"
    1.70 +    then obtain d where d: "y = p*d" unfolding dvd_def by blast
    1.71 +    from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult_commute)
    1.72 +    hence th: "d*x = p^k" using p0 by simp
    1.73 +    from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
    1.74 +    with d have "y = p^Suc i" by simp 
    1.75 +    with ij(2) have ?case by blast}
    1.76 +  ultimately show ?case  using pxyc by blast
    1.77 +qed
    1.78 +
    1.79 +lemma prime_power_exp: 
    1.80 +  fixes p::nat
    1.81 +  assumes p: "prime p" and n: "n \<noteq> 0" 
    1.82 +    and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
    1.83 +  using n xn
    1.84 +proof(induct n arbitrary: k)
    1.85 +  case 0 thus ?case by simp
    1.86 +next
    1.87 +  case (Suc n k) hence th: "x*x^n = p^k" by simp
    1.88 +  {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
    1.89 +  moreover
    1.90 +  {assume n: "n \<noteq> 0"
    1.91 +    from prime_power_mult[OF p th] 
    1.92 +    obtain i j where ij: "x = p^i" "x^n = p^j"by blast
    1.93 +    from Suc.hyps[OF n ij(2)] have ?case .}
    1.94 +  ultimately show ?case by blast
    1.95 +qed
    1.96 +
    1.97 +lemma divides_primepow:
    1.98 +  fixes p::nat
    1.99 +  assumes p: "prime p" 
   1.100 +  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
   1.101 +proof
   1.102 +  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k" 
   1.103 +    unfolding dvd_def  apply (auto simp add: mult_commute) by blast
   1.104 +  from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
   1.105 +  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
   1.106 +  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp 
   1.107 +  hence "i \<le> k" by arith
   1.108 +  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
   1.109 +next
   1.110 +  {fix i assume H: "i \<le> k" "d = p^i"
   1.111 +    then obtain j where j: "k = i + j"
   1.112 +      by (metis le_add_diff_inverse)
   1.113 +    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
   1.114 +    hence "d dvd p^k" unfolding dvd_def by auto}
   1.115 +  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
   1.116 +qed
   1.117 +
   1.118  end