author paulson Fri Jan 31 16:58:58 2014 +0000 (2014-01-31) changeset 55215 b6c926e67350 parent 55214 48a347b40629 child 55216 77953325d5f1 child 55225 22a1f3813d67
Restoring some proofs from the equivalent file in Old_Number_Theory.
```     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"