src/HOL/GCD.thy
changeset 32007 a2a3685f61c3
parent 31996 1d93369079c4
child 32045 efc5f4806cd5
     1.1 --- a/src/HOL/GCD.thy	Wed Jul 15 15:09:33 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Wed Jul 15 20:34:58 2009 +0200
     1.3 @@ -159,7 +159,6 @@
     1.4      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
     1.5  
     1.6  
     1.7 -
     1.8  subsection {* GCD *}
     1.9  
    1.10  (* was gcd_induct *)
    1.11 @@ -1553,32 +1552,6 @@
    1.12      apply (case_tac "p >= 0")
    1.13      by (blast, auto simp add: prime_ge_0_int)
    1.14  
    1.15 -(* To do: determine primality of any numeral *)
    1.16 -
    1.17 -lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
    1.18 -  by (simp add: prime_nat_def)
    1.19 -
    1.20 -lemma zero_not_prime_int [simp]: "~prime (0::int)"
    1.21 -  by (simp add: prime_int_def)
    1.22 -
    1.23 -lemma one_not_prime_nat [simp]: "~prime (1::nat)"
    1.24 -  by (simp add: prime_nat_def)
    1.25 -
    1.26 -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
    1.27 -  by (simp add: prime_nat_def One_nat_def)
    1.28 -
    1.29 -lemma one_not_prime_int [simp]: "~prime (1::int)"
    1.30 -  by (simp add: prime_int_def)
    1.31 -
    1.32 -lemma two_is_prime_nat [simp]: "prime (2::nat)"
    1.33 -  apply (auto simp add: prime_nat_def)
    1.34 -  apply (case_tac m)
    1.35 -  apply (auto dest!: dvd_imp_le)
    1.36 -  done
    1.37 -
    1.38 -lemma two_is_prime_int [simp]: "prime (2::int)"
    1.39 -  by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
    1.40 -
    1.41  lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
    1.42    apply (unfold prime_nat_def)
    1.43    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
    1.44 @@ -1625,15 +1598,70 @@
    1.45    apply auto
    1.46  done
    1.47  
    1.48 -lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
    1.49 -    coprime a (p^m)"
    1.50 +subsubsection{* Make prime naively executable *}
    1.51 +
    1.52 +lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
    1.53 +  by (simp add: prime_nat_def)
    1.54 +
    1.55 +lemma zero_not_prime_int [simp]: "~prime (0::int)"
    1.56 +  by (simp add: prime_int_def)
    1.57 +
    1.58 +lemma one_not_prime_nat [simp]: "~prime (1::nat)"
    1.59 +  by (simp add: prime_nat_def)
    1.60 +
    1.61 +lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
    1.62 +  by (simp add: prime_nat_def One_nat_def)
    1.63 +
    1.64 +lemma one_not_prime_int [simp]: "~prime (1::int)"
    1.65 +  by (simp add: prime_int_def)
    1.66 +
    1.67 +lemma prime_nat_code[code]:
    1.68 + "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
    1.69 +apply(simp add: Ball_def)
    1.70 +apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
    1.71 +done
    1.72 +
    1.73 +lemma prime_nat_simp:
    1.74 + "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
    1.75 +apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
    1.76 +apply(simp add:nat_number One_nat_def)
    1.77 +done
    1.78 +
    1.79 +lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
    1.80 +
    1.81 +lemma prime_int_code[code]:
    1.82 +  "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
    1.83 +proof
    1.84 +  assume "?L" thus "?R"
    1.85 +    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
    1.86 +next
    1.87 +    assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
    1.88 +qed
    1.89 +
    1.90 +lemma prime_int_simp:
    1.91 +  "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
    1.92 +apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
    1.93 +apply simp
    1.94 +done
    1.95 +
    1.96 +lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
    1.97 +
    1.98 +declare successor_int_def[simp]
    1.99 +
   1.100 +lemma two_is_prime_nat [simp]: "prime (2::nat)"
   1.101 +by simp
   1.102 +
   1.103 +lemma two_is_prime_int [simp]: "prime (2::int)"
   1.104 +by simp
   1.105 +
   1.106 +
   1.107 +lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   1.108    apply (rule coprime_exp_nat)
   1.109    apply (subst gcd_commute_nat)
   1.110    apply (erule (1) prime_imp_coprime_nat)
   1.111  done
   1.112  
   1.113 -lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
   1.114 -    coprime a (p^m)"
   1.115 +lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   1.116    apply (rule coprime_exp_int)
   1.117    apply (subst gcd_commute_int)
   1.118    apply (erule (1) prime_imp_coprime_int)
   1.119 @@ -1652,12 +1680,10 @@
   1.120    apply auto
   1.121  done
   1.122  
   1.123 -lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
   1.124 -    coprime (p^m) (q^n)"
   1.125 +lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   1.126    by (rule coprime_exp2_nat, rule primes_coprime_nat)
   1.127  
   1.128 -lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
   1.129 -    coprime (p^m) (q^n)"
   1.130 +lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   1.131    by (rule coprime_exp2_int, rule primes_coprime_int)
   1.132  
   1.133  lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"