src/HOL/Number_Theory/Primes.thy
 changeset 55130 70db8d380d62 parent 54228 229282d53781 child 55215 b6c926e67350
```     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Thu Jan 23 16:09:28 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Jan 24 15:21:00 2014 +0000
1.3 @@ -31,6 +31,8 @@
1.4  imports "~~/src/HOL/GCD"
1.5  begin
1.6
1.7 +declare One_nat_def [simp]
1.8 +
1.9  class prime = one +
1.10    fixes prime :: "'a \<Rightarrow> bool"
1.11
1.12 @@ -172,10 +174,7 @@
1.13    by (induct n) auto
1.14
1.15  lemma prime_dvd_power_int: "prime (p::int) \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
1.16 -  apply (induct n)
1.17 -  apply (frule prime_ge_0_int)
1.18 -  apply auto
1.19 -  done
1.20 +  by (induct n) (auto simp: prime_ge_0_int)
1.21
1.22  lemma prime_dvd_power_nat_iff: "prime (p::nat) \<Longrightarrow> n > 0 \<Longrightarrow>
1.23      p dvd x^n \<longleftrightarrow> p dvd x"
1.24 @@ -198,7 +197,7 @@
1.26
1.27  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
1.28 -  by (simp add: prime_nat_def One_nat_def)
1.29 +  by (simp add: prime_nat_def)
1.30
1.31  lemma one_not_prime_int [simp]: "~prime (1::int)"
1.33 @@ -206,7 +205,7 @@
1.34  lemma prime_nat_code [code]:
1.35      "prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
1.37 -  apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
1.38 +  apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
1.39    done
1.40
1.41  lemma prime_nat_simp:
1.42 @@ -246,28 +245,16 @@
1.43
1.44
1.45  lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.46 -  apply (rule coprime_exp_nat)
1.47 -  apply (subst gcd_commute_nat)
1.48 -  apply (erule (1) prime_imp_coprime_nat)
1.49 -  done
1.50 +  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
1.51
1.52  lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
1.53 -  apply (rule coprime_exp_int)
1.54 -  apply (subst gcd_commute_int)
1.55 -  apply (erule (1) prime_imp_coprime_int)
1.56 -  done
1.57 +  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
1.58
1.59  lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.60 -  apply (rule prime_imp_coprime_nat, assumption)
1.61 -  apply (unfold prime_nat_def)
1.62 -  apply auto
1.63 -  done
1.64 +  by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
1.65
1.66  lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.67 -  apply (rule prime_imp_coprime_int, assumption)
1.68 -  apply (unfold prime_int_altdef)
1.69 -  apply (metis int_one_le_iff_zero_less less_le)
1.70 -  done
1.71 +  by (metis leD linear prime_gt_0_int prime_imp_coprime_int prime_int_altdef)
1.72
1.73  lemma primes_imp_powers_coprime_nat:
1.74      "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
1.75 @@ -286,46 +273,6 @@
1.76      nat_dvd_not_less neq0_conv prime_nat_def)
1.77    done
1.78
1.79 -(* An Isar version:
1.80 -
1.81 -lemma prime_factor_b_nat:
1.82 -  fixes n :: nat
1.83 -  assumes "n \<noteq> 1"
1.84 -  shows "\<exists>p. prime p \<and> p dvd n"
1.85 -
1.86 -using `n ~= 1`
1.87 -proof (induct n rule: less_induct_nat)
1.88 -  fix n :: nat
1.89 -  assume "n ~= 1" and
1.90 -    ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
1.91 -  then show "\<exists>p. prime p \<and> p dvd n"
1.92 -  proof -
1.93 -  {
1.94 -    assume "n = 0"
1.95 -    moreover note two_is_prime_nat
1.96 -    ultimately have ?thesis
1.97 -      by (auto simp del: two_is_prime_nat)
1.98 -  }
1.99 -  moreover
1.100 -  {
1.101 -    assume "prime n"
1.102 -    then have ?thesis by auto
1.103 -  }
1.104 -  moreover
1.105 -  {
1.106 -    assume "n ~= 0" and "~ prime n"
1.107 -    with `n ~= 1` have "n > 1" by auto
1.108 -    with `~ prime n` and not_prime_eq_prod_nat obtain m k where
1.109 -      "n = m * k" and "1 < m" and "m < n" by blast
1.110 -    with ih obtain p where "prime p" and "p dvd m" by blast
1.111 -    with `n = m * k` have ?thesis by auto
1.112 -  }
1.113 -  ultimately show ?thesis by blast
1.114 -  qed
1.115 -qed
1.116 -
1.117 -*)
1.118 -
1.119  text {* One property of coprimality is easier to prove via prime factors. *}
1.120
1.121  lemma prime_divprod_pow_nat:
```