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.25    by (simp add: prime_nat_def)
    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.32    by (simp add: prime_int_def)
    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.36    apply (simp add: Ball_def)
    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: