formal class for factorial (semi)rings
authorhaftmann
Mon Jul 27 22:44:02 2015 +0200 (2015-07-27)
changeset 60804080a979a985b
parent 60803 e11f47dd0786
child 60806 622d45ca75ee
formal class for factorial (semi)rings
CONTRIBUTORS
src/HOL/Library/Multiset.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/ROOT
     1.1 --- a/CONTRIBUTORS	Mon Jul 27 22:08:46 2015 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Jul 27 22:44:02 2015 +0200
     1.3 @@ -18,6 +18,9 @@
     1.4    (semi)domains like units, associated elements and normalization
     1.5    wrt. units.
     1.6  
     1.7 +* Summer 2015: Florian Haftmann, TUM
     1.8 +  Fundamentals of abstract type class for factorial rings.
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2015
    1.12  -----------------------------
     2.1 --- a/src/HOL/Library/Multiset.thy	Mon Jul 27 22:08:46 2015 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 27 22:44:02 2015 +0200
     2.3 @@ -1140,6 +1140,36 @@
     2.4  by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
     2.5  
     2.6  
     2.7 +subsection \<open>Replicate operation\<close>
     2.8 +
     2.9 +definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
    2.10 +  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
    2.11 +
    2.12 +lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
    2.13 +  unfolding replicate_mset_def by simp
    2.14 +
    2.15 +lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
    2.16 +  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
    2.17 +
    2.18 +lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
    2.19 +  unfolding replicate_mset_def by (induct n) simp_all
    2.20 +
    2.21 +lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
    2.22 +  unfolding replicate_mset_def by (induct n) simp_all
    2.23 +
    2.24 +lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
    2.25 +  by (auto split: if_splits)
    2.26 +
    2.27 +lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
    2.28 +  by (induct n, simp_all)
    2.29 +
    2.30 +lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
    2.31 +  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
    2.32 +
    2.33 +lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
    2.34 +  by (induct D) simp_all
    2.35 +
    2.36 +
    2.37  subsection \<open>Big operators\<close>
    2.38  
    2.39  no_notation times (infixl "*" 70)
    2.40 @@ -1195,6 +1225,10 @@
    2.41    from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
    2.42  qed
    2.43  
    2.44 +lemma (in semiring_1) msetsum_replicate_mset [simp]:
    2.45 +  "msetsum (replicate_mset n a) = of_nat n * a"
    2.46 +  by (induct n) (simp_all add: algebra_simps)
    2.47 +
    2.48  lemma setsum_unfold_msetsum:
    2.49    "setsum f A = msetsum (image_mset f (mset_set A))"
    2.50    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    2.51 @@ -1267,6 +1301,10 @@
    2.52    "msetprod (A + B) = msetprod A * msetprod B"
    2.53    by (fact msetprod.union)
    2.54  
    2.55 +lemma msetprod_replicate_mset [simp]:
    2.56 +  "msetprod (replicate_mset n a) = a ^ n"
    2.57 +  by (induct n) (simp_all add: ac_simps)
    2.58 +
    2.59  lemma setprod_unfold_msetprod:
    2.60    "setprod f A = msetprod (image_mset f (mset_set A))"
    2.61    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    2.62 @@ -1302,37 +1340,6 @@
    2.63  qed
    2.64  
    2.65  
    2.66 -subsection \<open>Replicate operation\<close>
    2.67 -
    2.68 -definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
    2.69 -  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
    2.70 -
    2.71 -lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
    2.72 -  unfolding replicate_mset_def by simp
    2.73 -
    2.74 -lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
    2.75 -  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
    2.76 -
    2.77 -lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
    2.78 -  unfolding replicate_mset_def by (induct n) simp_all
    2.79 -
    2.80 -lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
    2.81 -  unfolding replicate_mset_def by (induct n) simp_all
    2.82 -
    2.83 -lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
    2.84 -  by (auto split: if_splits)
    2.85 -
    2.86 -lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
    2.87 -  by (induct n, simp_all)
    2.88 -
    2.89 -lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
    2.90 -  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
    2.91 -
    2.92 -
    2.93 -lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
    2.94 -  by (induct D) simp_all
    2.95 -
    2.96 -
    2.97  subsection \<open>Alternative representations\<close>
    2.98  
    2.99  subsubsection \<open>Lists\<close>
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Jul 27 22:44:02 2015 +0200
     3.3 @@ -0,0 +1,370 @@
     3.4 +(*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +section \<open>Factorial (semi)rings\<close>
     3.9 +
    3.10 +theory Factorial_Ring
    3.11 +imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
    3.12 +begin
    3.13 +
    3.14 +context algebraic_semidom
    3.15 +begin
    3.16 +
    3.17 +lemma is_unit_mult_iff:
    3.18 +  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
    3.19 +  by (auto dest: dvd_mult_left dvd_mult_right)
    3.20 +
    3.21 +lemma is_unit_power_iff:
    3.22 +  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
    3.23 +  by (induct n) (auto simp add: is_unit_mult_iff)
    3.24 +  
    3.25 +lemma subset_divisors_dvd:
    3.26 +  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
    3.27 +  by (auto simp add: subset_iff intro: dvd_trans)
    3.28 +
    3.29 +lemma strict_subset_divisors_dvd:
    3.30 +  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
    3.31 +  by (auto simp add: subset_iff intro: dvd_trans)
    3.32 +
    3.33 +end
    3.34 +
    3.35 +class factorial_semiring = normalization_semidom +
    3.36 +  assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
    3.37 +  fixes is_prime :: "'a \<Rightarrow> bool"
    3.38 +  assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
    3.39 +    and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
    3.40 +    and no_prime_divisorsI: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
    3.41 +  assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
    3.42 +    and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    3.43 +begin
    3.44 +
    3.45 +lemma not_is_prime_one [simp]:
    3.46 +  "\<not> is_prime 1"
    3.47 +  by (auto dest: is_prime_not_unit)
    3.48 +
    3.49 +lemma is_prime_not_zeroI:
    3.50 +  assumes "is_prime p"
    3.51 +  shows "p \<noteq> 0"
    3.52 +  using assms by (auto intro: ccontr)
    3.53 +
    3.54 +lemma is_prime_multD:
    3.55 +  assumes "is_prime (a * b)"
    3.56 +  shows "is_unit a \<or> is_unit b"
    3.57 +proof -
    3.58 +  from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
    3.59 +  moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
    3.60 +    by auto
    3.61 +  ultimately show ?thesis
    3.62 +    using dvd_times_left_cancel_iff [of a b 1]
    3.63 +      dvd_times_right_cancel_iff [of b a 1]
    3.64 +    by auto
    3.65 +qed
    3.66 +
    3.67 +lemma is_primeD2:
    3.68 +  assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
    3.69 +  shows "p dvd a"
    3.70 +proof -
    3.71 +  from \<open>a dvd p\<close> obtain b where "p = a * b" ..
    3.72 +  with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
    3.73 +  with \<open>p = a * b\<close> show ?thesis
    3.74 +    by (auto simp add: mult_unit_dvd_iff)
    3.75 +qed
    3.76 +
    3.77 +lemma is_prime_mult_unit_left:
    3.78 +  assumes "is_prime p"
    3.79 +    and "is_unit a"
    3.80 +  shows "is_prime (a * p)"
    3.81 +proof (rule is_primeI)
    3.82 +  from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
    3.83 +    by (auto simp add: is_unit_mult_iff is_prime_not_unit)
    3.84 +  show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
    3.85 +  proof -
    3.86 +    from that \<open>is_unit a\<close> have "b dvd p"
    3.87 +      using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
    3.88 +    with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
    3.89 +      using is_primeD2 [of p b] by auto
    3.90 +    with \<open>is_unit a\<close> show ?thesis
    3.91 +      using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
    3.92 +  qed
    3.93 +qed
    3.94 +
    3.95 +lemma is_primeI2:
    3.96 +  assumes "p \<noteq> 0"
    3.97 +  assumes "\<not> is_unit p"
    3.98 +  assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    3.99 +  shows "is_prime p"
   3.100 +using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
   3.101 +  fix a
   3.102 +  assume "a dvd p"
   3.103 +  then obtain b where "p = a * b" ..
   3.104 +  with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
   3.105 +  moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
   3.106 +  moreover assume "\<not> is_unit a"
   3.107 +  ultimately show "p dvd a"
   3.108 +    using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
   3.109 +qed    
   3.110 +
   3.111 +lemma not_is_prime_divisorE:
   3.112 +  assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
   3.113 +  obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
   3.114 +proof -
   3.115 +  from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
   3.116 +    by (auto intro: is_primeI)
   3.117 +  with that show thesis by blast
   3.118 +qed
   3.119 +
   3.120 +lemma prime_divisorE:
   3.121 +  assumes "a \<noteq> 0" and "\<not> is_unit a" 
   3.122 +  obtains p where "is_prime p" and "p dvd a"
   3.123 +  using assms no_prime_divisorsI [of a] by blast
   3.124 +
   3.125 +lemma prime_dvd_mult_iff:  
   3.126 +  assumes "is_prime p"
   3.127 +  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   3.128 +  using assms by (auto dest: is_primeD)
   3.129 +
   3.130 +lemma prime_dvd_power_iff:
   3.131 +  assumes "is_prime p"
   3.132 +  shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   3.133 +  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
   3.134 +
   3.135 +lemma is_prime_normalize_iff [simp]:
   3.136 +  "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
   3.137 +proof
   3.138 +  assume ?Q show ?P
   3.139 +    by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
   3.140 +next
   3.141 +  assume ?P show ?Q
   3.142 +    by (rule is_primeI)
   3.143 +      (insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \<open>?P\<close>, simp_all)
   3.144 +qed  
   3.145 +
   3.146 +lemma is_prime_inj_power:
   3.147 +  assumes "is_prime p"
   3.148 +  shows "inj (op ^ p)"
   3.149 +proof (rule injI, rule ccontr)
   3.150 +  fix m n :: nat
   3.151 +  have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
   3.152 +  proof
   3.153 +    assume ?Q then show ?P by simp
   3.154 +  next
   3.155 +    assume ?P then have "is_unit (p ^ q)" by simp
   3.156 +    with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
   3.157 +  qed
   3.158 +  have *: False if "p ^ m = p ^ n" and "m > n" for m n
   3.159 +  proof -
   3.160 +    from assms have "p \<noteq> 0"
   3.161 +      by (rule is_prime_not_zeroI)
   3.162 +    then have "p ^ n \<noteq> 0"
   3.163 +      by (induct n) simp_all
   3.164 +    from that have "m = n + (m - n)" and "m - n > 0" by arith+
   3.165 +    then obtain q where "m = n + q" and "q > 0" ..
   3.166 +    with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
   3.167 +    with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
   3.168 +      using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
   3.169 +    with \<open>q > 0\<close> show ?thesis by simp
   3.170 +  qed 
   3.171 +  assume "m \<noteq> n"
   3.172 +  then have "m > n \<or> m < n" by arith
   3.173 +  moreover assume "p ^ m = p ^ n"
   3.174 +  ultimately show False using * [of m n] * [of n m] by auto
   3.175 +qed
   3.176 +
   3.177 +lemma prime_unique:
   3.178 +  assumes "is_prime q" and "is_prime p" and "q dvd p"
   3.179 +  shows "normalize q = normalize p"
   3.180 +proof -
   3.181 +  from assms have "p dvd q"
   3.182 +    by (auto dest: is_primeD2 [of p] is_prime_not_unit [of q])
   3.183 +  with assms show ?thesis
   3.184 +    by (auto intro: associatedI)
   3.185 +qed  
   3.186 +
   3.187 +lemma exists_factorization:
   3.188 +  assumes "a \<noteq> 0"
   3.189 +  obtains P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize a"
   3.190 +proof -
   3.191 +  let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
   3.192 +  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}" by auto
   3.193 +  moreover from assms have "finite {b. b dvd a \<and> normalize b = b}"
   3.194 +    by (rule finite_divisors)
   3.195 +  ultimately have "finite (?prime_factors a)" by (rule finite_subset)
   3.196 +  then show thesis using \<open>a \<noteq> 0\<close> that proof (induct "?prime_factors a" arbitrary: thesis a)
   3.197 +    case empty then have
   3.198 +      P: "\<And>b. is_prime b \<Longrightarrow> b dvd a \<Longrightarrow> normalize b \<noteq> b" and "a \<noteq> 0"
   3.199 +      by auto
   3.200 +    have "is_unit a"
   3.201 +    proof (rule no_prime_divisorsI)
   3.202 +      fix b
   3.203 +      assume "b dvd a"
   3.204 +      then show "\<not> is_prime b"
   3.205 +        using P [of "normalize b"] by auto
   3.206 +    qed
   3.207 +    then have "\<And>p. p \<in># {#} \<Longrightarrow> is_prime p" and "msetprod {#} = normalize a"
   3.208 +      by (simp_all add: is_unit_normalize)
   3.209 +    with empty show thesis by blast
   3.210 +  next
   3.211 +    case (insert p P)
   3.212 +    from \<open>insert p P = ?prime_factors a\<close>
   3.213 +    have "p dvd a" and "is_prime p" and "normalize p = p"
   3.214 +      by auto
   3.215 +    obtain n where "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
   3.216 +    proof (rule that)
   3.217 +      def N \<equiv> "{n. p ^ n dvd a}"
   3.218 +      from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
   3.219 +      then have "inj_on (op ^ p) U" for U
   3.220 +        by (rule subset_inj_on) simp
   3.221 +      moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
   3.222 +        by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
   3.223 +      ultimately have "finite N"
   3.224 +        by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
   3.225 +      from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
   3.226 +      then have "N \<noteq> {}" by blast
   3.227 +      note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
   3.228 +      from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
   3.229 +      with * show "Max N > 0"
   3.230 +        by (auto simp add: Max_gr_iff)
   3.231 +      from * have "Max N \<in> N" by (rule Max_in)
   3.232 +      then show "p ^ Max N dvd a" by (simp add: N_def)
   3.233 +      from * have "\<forall>n\<in>N. n \<le> Max N"
   3.234 +        by (simp add: Max_le_iff [symmetric])
   3.235 +      then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
   3.236 +        by (rule bspec) (simp add: N_def)
   3.237 +      then show "\<not> p ^ Suc (Max N) dvd a"
   3.238 +        by auto
   3.239 +    qed
   3.240 +    from \<open>p ^ n dvd a\<close> obtain c where "a = p ^ n * c" ..
   3.241 +    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd c"
   3.242 +      by (auto elim: dvdE simp add: ac_simps)
   3.243 +    have "?prime_factors a - {p} = ?prime_factors c" (is "?A = ?B")
   3.244 +    proof (rule set_eqI)
   3.245 +      fix q
   3.246 +      show "q \<in> ?A \<longleftrightarrow> q \<in> ?B"
   3.247 +      using \<open>normalize p = p\<close> \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>\<not> p dvd c\<close>
   3.248 +        prime_unique [of q p]
   3.249 +        by (auto simp add: prime_dvd_power_iff prime_dvd_mult_iff)
   3.250 +    qed
   3.251 +    moreover from insert have "P = ?prime_factors a - {p}"
   3.252 +      by auto
   3.253 +    ultimately have "P = ?prime_factors c"
   3.254 +      by simp
   3.255 +    moreover from \<open>a \<noteq> 0\<close> \<open>a = p ^ n * c\<close> have "c \<noteq> 0"
   3.256 +      by auto
   3.257 +    ultimately obtain P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize c"
   3.258 +      using insert(3) by blast 
   3.259 +    with \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>normalize p = p\<close>
   3.260 +    have "\<And>q. q \<in># P + (replicate_mset n p) \<longrightarrow> is_prime q" "msetprod (P + replicate_mset n p) = normalize a"
   3.261 +      by (auto simp add: ac_simps normalize_mult normalize_power)
   3.262 +    with insert(6) show thesis by blast
   3.263 +  qed
   3.264 +qed
   3.265 +  
   3.266 +end
   3.267 +
   3.268 +instantiation nat :: factorial_semiring
   3.269 +begin
   3.270 +
   3.271 +definition is_prime_nat :: "nat \<Rightarrow> bool"
   3.272 +where
   3.273 +  "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
   3.274 +
   3.275 +lemma is_prime_eq_prime:
   3.276 +  "is_prime = prime"
   3.277 +  by (simp add: fun_eq_iff prime_def is_prime_nat_def)
   3.278 +
   3.279 +instance proof
   3.280 +  show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
   3.281 +  show "\<not> is_unit p" if "is_prime p" for p :: nat
   3.282 +    using that by (simp add: is_prime_nat_def)
   3.283 +next
   3.284 +  fix p :: nat
   3.285 +  assume "p \<noteq> 0" and "\<not> is_unit p"
   3.286 +  then have "p > 1" by simp
   3.287 +  assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
   3.288 +  have "n = 1" if "n dvd p" "n \<noteq> p" for n
   3.289 +  proof (rule ccontr)
   3.290 +    assume "n \<noteq> 1"
   3.291 +    with that P have "p dvd n" by auto
   3.292 +    with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
   3.293 +    with that show False by simp
   3.294 +  qed
   3.295 +  with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
   3.296 +next
   3.297 +  fix p m n :: nat
   3.298 +  assume "is_prime p"
   3.299 +  then have "prime p" by (simp add: is_prime_eq_prime)
   3.300 +  moreover assume "p dvd m * n"
   3.301 +  ultimately show "p dvd m \<or> p dvd n"
   3.302 +    by (rule prime_dvd_mult_nat)
   3.303 +next
   3.304 +  fix n :: nat
   3.305 +  show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
   3.306 +    using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
   3.307 +qed simp
   3.308 +
   3.309 +end
   3.310 +
   3.311 +instantiation int :: factorial_semiring
   3.312 +begin
   3.313 +
   3.314 +definition is_prime_int :: "int \<Rightarrow> bool"
   3.315 +where
   3.316 +  "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
   3.317 +
   3.318 +lemma is_prime_int_iff [simp]:
   3.319 +  "is_prime (int n) \<longleftrightarrow> is_prime n"
   3.320 +  by (simp add: is_prime_int_def)
   3.321 +
   3.322 +lemma is_prime_nat_abs_iff [simp]:
   3.323 +  "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
   3.324 +  by (simp add: is_prime_int_def)
   3.325 +
   3.326 +instance proof
   3.327 +  show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
   3.328 +  show "\<not> is_unit p" if "is_prime p" for p :: int
   3.329 +    using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
   3.330 +next
   3.331 +  fix p :: int
   3.332 +  assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
   3.333 +  have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
   3.334 +  proof -
   3.335 +    from that have "int n dvd p" by (simp add: int_dvd_iff)
   3.336 +    moreover from that have "\<not> is_unit (int n)" by simp
   3.337 +    ultimately have "p dvd int n" by (rule P)
   3.338 +    with that have "p dvd int n" by auto
   3.339 +    then show ?thesis by (simp add: dvd_int_iff)
   3.340 +  qed
   3.341 +  moreover assume "p \<noteq> 0" and "\<not> is_unit p"
   3.342 +  ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
   3.343 +  then show "is_prime p" by simp
   3.344 +next
   3.345 +  fix p k l :: int
   3.346 +  assume "is_prime p"
   3.347 +  then have *: "is_prime (nat \<bar>p\<bar>)" by simp
   3.348 +  assume "p dvd k * l"
   3.349 +  then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
   3.350 +    by (simp add: dvd_int_iff)
   3.351 +  then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
   3.352 +    by (simp add: abs_mult nat_mult_distrib)
   3.353 +  with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
   3.354 +    using is_primeD [of "nat \<bar>p\<bar>"] by auto
   3.355 +  then show "p dvd k \<or> p dvd l"
   3.356 +    by (simp add: dvd_int_iff)
   3.357 +next
   3.358 +  fix k :: int
   3.359 +  assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
   3.360 +  have "is_unit (nat \<bar>k\<bar>)"
   3.361 +  proof (rule no_prime_divisorsI)
   3.362 +    fix m
   3.363 +    assume "m dvd nat \<bar>k\<bar>"
   3.364 +    then have "int m dvd k" by (simp add: int_dvd_iff)
   3.365 +    then have "\<not> is_prime (int m)" by (rule P)
   3.366 +    then show "\<not> is_prime m" by simp
   3.367 +  qed
   3.368 +  then show "is_unit k" by simp
   3.369 +qed simp
   3.370 +
   3.371 +end
   3.372 +
   3.373 +end
     4.1 --- a/src/HOL/Number_Theory/Primes.thy	Mon Jul 27 22:08:46 2015 +0200
     4.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Jul 27 22:44:02 2015 +0200
     4.3 @@ -35,7 +35,7 @@
     4.4  declare [[coercion_enabled]]
     4.5  
     4.6  definition prime :: "nat \<Rightarrow> bool"
     4.7 -  where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
     4.8 +  where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
     4.9  
    4.10  lemmas prime_nat_def = prime_def
    4.11  
     5.1 --- a/src/HOL/ROOT	Mon Jul 27 22:08:46 2015 +0200
     5.2 +++ b/src/HOL/ROOT	Mon Jul 27 22:44:02 2015 +0200
     5.3 @@ -188,6 +188,7 @@
     5.4      Gauss
     5.5      Number_Theory
     5.6      Euclidean_Algorithm
     5.7 +    Factorial_Ring
     5.8    document_files
     5.9      "root.tex"
    5.10