constructive formulation of factorization
authorhaftmann
Thu Mar 03 08:33:55 2016 +0100 (2016-03-03)
changeset 624994a5b81ff5992
parent 62498 5dfcc9697f29
child 62500 ff99681b3fd8
constructive formulation of factorization
CONTRIBUTORS
src/HOL/Number_Theory/Factorial_Ring.thy
     1.1 --- a/CONTRIBUTORS	Wed Mar 02 19:43:31 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Mar 03 08:33:55 2016 +0100
     1.3 @@ -10,6 +10,9 @@
     1.4    Abolition of compound operators INFIMUM and SUPREMUM
     1.5    for complete lattices.
     1.6  
     1.7 +* March 2016: Florian Haftmann
     1.8 +  Abstract factorial rings with unique factorization.
     1.9 +
    1.10  
    1.11  Contributions to Isabelle2016
    1.12  -----------------------------
     2.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Mar 02 19:43:31 2016 +0100
     2.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Mar 03 08:33:55 2016 +0100
     2.3 @@ -5,15 +5,31 @@
     2.4  section \<open>Factorial (semi)rings\<close>
     2.5  
     2.6  theory Factorial_Ring
     2.7 -imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
     2.8 +imports Main Primes "~~/src/HOL/Library/Multiset"
     2.9 +begin
    2.10 +
    2.11 +context algebraic_semidom
    2.12  begin
    2.13  
    2.14 +lemma dvd_mult_imp_div:
    2.15 +  assumes "a * c dvd b"
    2.16 +  shows "a dvd b div c"
    2.17 +proof (cases "c = 0")
    2.18 +  case True then show ?thesis by simp
    2.19 +next
    2.20 +  case False
    2.21 +  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
    2.22 +  with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
    2.23 +qed
    2.24 +
    2.25 +end
    2.26 +
    2.27  class factorial_semiring = normalization_semidom +
    2.28    assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
    2.29    fixes is_prime :: "'a \<Rightarrow> bool"
    2.30    assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
    2.31      and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
    2.32 -    and no_prime_divisorsI: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
    2.33 +    and no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
    2.34    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"
    2.35      and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    2.36  begin
    2.37 @@ -93,21 +109,6 @@
    2.38    with that show thesis by blast
    2.39  qed
    2.40  
    2.41 -lemma prime_divisorE:
    2.42 -  assumes "a \<noteq> 0" and "\<not> is_unit a" 
    2.43 -  obtains p where "is_prime p" and "p dvd a"
    2.44 -  using assms no_prime_divisorsI [of a] by blast
    2.45 -
    2.46 -lemma prime_dvd_mult_iff:  
    2.47 -  assumes "is_prime p"
    2.48 -  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
    2.49 -  using assms by (auto dest: is_primeD)
    2.50 -
    2.51 -lemma prime_dvd_power_iff:
    2.52 -  assumes "is_prime p"
    2.53 -  shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
    2.54 -  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
    2.55 -
    2.56  lemma is_prime_normalize_iff [simp]:
    2.57    "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
    2.58  proof
    2.59 @@ -119,6 +120,157 @@
    2.60        (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)
    2.61  qed  
    2.62  
    2.63 +lemma no_prime_divisorsI:
    2.64 +  assumes "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime b"
    2.65 +  shows "is_unit a"
    2.66 +proof (rule no_prime_divisorsI2)
    2.67 +  fix b
    2.68 +  assume "b dvd a"
    2.69 +  then have "normalize b dvd a"
    2.70 +    by simp
    2.71 +  moreover have "normalize (normalize b) = normalize b"
    2.72 +    by simp
    2.73 +  ultimately have "\<not> is_prime (normalize b)"
    2.74 +    by (rule assms)
    2.75 +  then show "\<not> is_prime b"
    2.76 +    by simp
    2.77 +qed
    2.78 +
    2.79 +lemma prime_divisorE:
    2.80 +  assumes "a \<noteq> 0" and "\<not> is_unit a" 
    2.81 +  obtains p where "is_prime p" and "p dvd a"
    2.82 +  using assms no_prime_divisorsI [of a] by blast
    2.83 +
    2.84 +lemma is_prime_associated:
    2.85 +  assumes "is_prime p" and "is_prime q" and "q dvd p"
    2.86 +  shows "normalize q = normalize p"
    2.87 +using \<open>q dvd p\<close> proof (rule associatedI)
    2.88 +  from \<open>is_prime q\<close> have "\<not> is_unit q"
    2.89 +    by (simp add: is_prime_not_unit)
    2.90 +  with \<open>is_prime p\<close> \<open>q dvd p\<close> show "p dvd q"
    2.91 +    by (blast intro: is_primeD2)
    2.92 +qed
    2.93 +
    2.94 +lemma prime_dvd_mult_iff:  
    2.95 +  assumes "is_prime p"
    2.96 +  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
    2.97 +  using assms by (auto dest: is_primeD)
    2.98 +
    2.99 +lemma prime_dvd_msetprod:
   2.100 +  assumes "is_prime p"
   2.101 +  assumes dvd: "p dvd msetprod A"
   2.102 +  obtains a where "a \<in># A" and "p dvd a"
   2.103 +proof -
   2.104 +  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   2.105 +  proof (induct A)
   2.106 +    case empty then show ?case
   2.107 +    using \<open>is_prime p\<close> by (simp add: is_prime_not_unit)
   2.108 +  next
   2.109 +    case (add A a)
   2.110 +    then have "p dvd msetprod A * a" by simp
   2.111 +    with \<open>is_prime p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
   2.112 +      by (blast dest: is_primeD)
   2.113 +    then show ?case proof cases
   2.114 +      case B then show ?thesis by auto
   2.115 +    next
   2.116 +      case A
   2.117 +      with add.hyps obtain b where "b \<in># A" "p dvd b"
   2.118 +        by auto
   2.119 +      then show ?thesis by auto
   2.120 +    qed
   2.121 +  qed
   2.122 +  with that show thesis by blast
   2.123 +qed
   2.124 +
   2.125 +lemma msetprod_eq_iff:
   2.126 +  assumes "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p" and "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
   2.127 +  shows "msetprod P = msetprod Q \<longleftrightarrow> P = Q" (is "?R \<longleftrightarrow> ?S")
   2.128 +proof
   2.129 +  assume ?S then show ?R by simp
   2.130 +next
   2.131 +  assume ?R then show ?S using assms proof (induct P arbitrary: Q)
   2.132 +    case empty then have Q: "msetprod Q = 1" by simp
   2.133 +    have "Q = {#}"
   2.134 +    proof (rule ccontr)
   2.135 +      assume "Q \<noteq> {#}"
   2.136 +      then obtain r R where "Q = R + {#r#}"
   2.137 +        using multi_nonempty_split by blast 
   2.138 +      moreover with empty have "is_prime r" by simp
   2.139 +      ultimately have "msetprod Q = msetprod R * r"
   2.140 +        by simp
   2.141 +      with Q have "msetprod R * r = 1"
   2.142 +        by simp
   2.143 +      then have "is_unit r"
   2.144 +        by (metis local.dvd_triv_right)
   2.145 +      with \<open>is_prime r\<close> show False by (simp add: is_prime_not_unit)
   2.146 +    qed
   2.147 +    then show ?case by simp
   2.148 +  next
   2.149 +    case (add P p)
   2.150 +    then have "is_prime p" and "normalize p = p"
   2.151 +      and "msetprod Q = msetprod P * p" and "p dvd msetprod Q"
   2.152 +      by auto (metis local.dvd_triv_right)
   2.153 +    with prime_dvd_msetprod
   2.154 +      obtain q where "q \<in># Q" and "p dvd q"
   2.155 +      by blast
   2.156 +    with add.prems have "is_prime q" and "normalize q = q"
   2.157 +      by simp_all
   2.158 +    from \<open>is_prime p\<close> have "p \<noteq> 0"
   2.159 +      by auto 
   2.160 +    from \<open>is_prime q\<close> \<open>is_prime p\<close> \<open>p dvd q\<close>
   2.161 +      have "normalize p = normalize q"
   2.162 +      by (rule is_prime_associated)
   2.163 +    from \<open>normalize p = p\<close> \<open>normalize q = q\<close> have "p = q"
   2.164 +      unfolding \<open>normalize p = normalize q\<close> by simp
   2.165 +    with \<open>q \<in># Q\<close> have "p \<in># Q" by simp
   2.166 +    have "msetprod P = msetprod (Q - {#p#})"
   2.167 +      using \<open>p \<in># Q\<close> \<open>p \<noteq> 0\<close> \<open>msetprod Q = msetprod P * p\<close>
   2.168 +      by (simp add: msetprod_minus)
   2.169 +    then have "P = Q - {#p#}"
   2.170 +      using add.prems(2-3)
   2.171 +      by (auto intro: add.hyps dest: in_diffD)
   2.172 +    with \<open>p \<in># Q\<close> show ?case by simp
   2.173 +  qed
   2.174 +qed
   2.175 +
   2.176 +lemma prime_dvd_power_iff:
   2.177 +  assumes "is_prime p"
   2.178 +  shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   2.179 +  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
   2.180 +
   2.181 +lemma prime_power_dvd_multD:
   2.182 +  assumes "is_prime p"
   2.183 +  assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   2.184 +  shows "p ^ n dvd b"
   2.185 +using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
   2.186 +  case 0 then show ?case by simp
   2.187 +next
   2.188 +  case (Suc n) show ?case
   2.189 +  proof (cases "n = 0")
   2.190 +    case True with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   2.191 +      by (simp add: prime_dvd_mult_iff)
   2.192 +  next
   2.193 +    case False then have "n > 0" by simp
   2.194 +    from \<open>is_prime p\<close> have "p \<noteq> 0" by auto
   2.195 +    from Suc.prems have *: "p * p ^ n dvd a * b"
   2.196 +      by simp
   2.197 +    then have "p dvd a * b"
   2.198 +      by (rule dvd_mult_left)
   2.199 +    with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   2.200 +      by (simp add: prime_dvd_mult_iff)
   2.201 +    moreover def c \<equiv> "b div p"
   2.202 +    ultimately have b: "b = p * c" by simp
   2.203 +    with * have "p * p ^ n dvd p * (a * c)"
   2.204 +      by (simp add: ac_simps)
   2.205 +    with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c"
   2.206 +      by simp
   2.207 +    with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c"
   2.208 +      by blast
   2.209 +    with \<open>p \<noteq> 0\<close> show ?thesis
   2.210 +      by (simp add: b)
   2.211 +  qed
   2.212 +qed
   2.213 +
   2.214  lemma is_prime_inj_power:
   2.215    assumes "is_prime p"
   2.216    shows "inj (op ^ p)"
   2.217 @@ -150,47 +302,80 @@
   2.218    ultimately show False using * [of m n] * [of n m] by auto
   2.219  qed
   2.220  
   2.221 -lemma prime_unique:
   2.222 -  assumes "is_prime q" and "is_prime p" and "q dvd p"
   2.223 -  shows "normalize q = normalize p"
   2.224 -proof -
   2.225 -  from assms have "p dvd q"
   2.226 -    by (auto dest: is_primeD2 [of p] is_prime_not_unit [of q])
   2.227 -  with assms show ?thesis
   2.228 -    by (auto intro: associatedI)
   2.229 -qed  
   2.230 +definition factorization :: "'a \<Rightarrow> 'a multiset option"
   2.231 +  where "factorization a = (if a = 0 then None
   2.232 +    else Some (setsum (\<lambda>p. replicate_mset (Max {n. p ^ n dvd a}) p)
   2.233 +      {p. p dvd a \<and> is_prime p \<and> normalize p = p}))"
   2.234 +
   2.235 +lemma factorization_normalize [simp]:
   2.236 +  "factorization (normalize a) = factorization a"
   2.237 +  by (simp add: factorization_def)
   2.238 +
   2.239 +lemma factorization_0 [simp]:
   2.240 +  "factorization 0 = None"
   2.241 +  by (simp add: factorization_def)
   2.242 +
   2.243 +lemma factorization_eq_None_iff [simp]:
   2.244 +  "factorization a = None \<longleftrightarrow> a = 0"
   2.245 +  by (simp add: factorization_def)
   2.246  
   2.247 -lemma exists_factorization:
   2.248 -  assumes "a \<noteq> 0"
   2.249 -  obtains P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize a"
   2.250 -proof -
   2.251 +lemma factorization_eq_Some_iff:
   2.252 +  "factorization a = Some P \<longleftrightarrow>
   2.253 +   normalize a = msetprod P \<and> 0 \<notin># P \<and> (\<forall>p \<in> set_mset P. is_prime p \<and> normalize p = p)"
   2.254 +proof (cases "a = 0")
   2.255 +  have [simp]: "0 = msetprod P \<longleftrightarrow> 0 \<in># P"
   2.256 +    using msetprod_zero_iff [of P] by blast
   2.257 +  case True
   2.258 +  then show ?thesis by auto
   2.259 +next
   2.260 +  case False    
   2.261    let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
   2.262 -  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}" by auto
   2.263 -  moreover from assms have "finite {b. b dvd a \<and> normalize b = b}"
   2.264 +  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}"
   2.265 +    by auto
   2.266 +  moreover from \<open>a \<noteq> 0\<close> have "finite {b. b dvd a \<and> normalize b = b}"
   2.267      by (rule finite_divisors)
   2.268 -  ultimately have "finite (?prime_factors a)" by (rule finite_subset)
   2.269 -  then show thesis using \<open>a \<noteq> 0\<close> that proof (induct "?prime_factors a" arbitrary: thesis a)
   2.270 +  ultimately have "finite (?prime_factors a)"
   2.271 +    by (rule finite_subset)
   2.272 +  then show ?thesis using \<open>a \<noteq> 0\<close>
   2.273 +  proof (induct "?prime_factors a" arbitrary: a P)
   2.274      case empty then have
   2.275 -      P: "\<And>b. is_prime b \<Longrightarrow> b dvd a \<Longrightarrow> normalize b \<noteq> b" and "a \<noteq> 0"
   2.276 +      *: "{p. p dvd a \<and> is_prime p \<and> normalize p = p} = {}"
   2.277 +        and "a \<noteq> 0"
   2.278        by auto
   2.279 -    have "is_unit a"
   2.280 -    proof (rule no_prime_divisorsI)
   2.281 -      fix b
   2.282 -      assume "b dvd a"
   2.283 -      then show "\<not> is_prime b"
   2.284 -        using P [of "normalize b"] by auto
   2.285 +    from \<open>a \<noteq> 0\<close> have "factorization a = Some {#}"
   2.286 +      by (simp only: factorization_def *) simp
   2.287 +    from * have "normalize a = 1"
   2.288 +      by (auto intro: is_unit_normalize no_prime_divisorsI)
   2.289 +    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
   2.290 +      assume ?lhs with \<open>factorization a = Some {#}\<close> \<open>normalize a = 1\<close>
   2.291 +      show ?rhs by simp
   2.292 +    next
   2.293 +      assume ?rhs have "P = {#}"
   2.294 +      proof (rule ccontr)
   2.295 +        assume "P \<noteq> {#}"
   2.296 +        then obtain q Q where "P = Q + {#q#}"
   2.297 +          using multi_nonempty_split by blast
   2.298 +        with \<open>?rhs\<close> \<open>normalize a = 1\<close>
   2.299 +        have "1 = q * msetprod Q" and "is_prime q"
   2.300 +          by (simp_all add: ac_simps)
   2.301 +        then have "is_unit q" by (auto intro: dvdI)
   2.302 +        with \<open>is_prime q\<close> show False
   2.303 +          using is_prime_not_unit by blast
   2.304 +      qed
   2.305 +      with \<open>factorization a = Some {#}\<close> show ?lhs by simp
   2.306      qed
   2.307 -    then have "\<And>p. p \<in># {#} \<Longrightarrow> is_prime p" and "msetprod {#} = normalize a"
   2.308 -      by (simp_all add: is_unit_normalize)
   2.309 -    with empty show thesis by blast
   2.310    next
   2.311 -    case (insert p P)
   2.312 -    from \<open>insert p P = ?prime_factors a\<close>
   2.313 -    have "p dvd a" and "is_prime p" and "normalize p = p"
   2.314 -      by auto
   2.315 -    obtain n where "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
   2.316 -    proof (rule that)
   2.317 +    case (insert p F)
   2.318 +    from \<open>insert p F = ?prime_factors a\<close>
   2.319 +    have "?prime_factors a = insert p F"
   2.320 +      by simp
   2.321 +    then have "p dvd a" and "is_prime p" and "normalize p = p" and "p \<noteq> 0"
   2.322 +      by (auto intro!: is_prime_not_zeroI)
   2.323 +    def n \<equiv> "Max {n. p ^ n dvd a}"
   2.324 +    then have "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
   2.325 +    proof -
   2.326        def N \<equiv> "{n. p ^ n dvd a}"
   2.327 +      then have n_M: "n = Max N" by (simp add: n_def)
   2.328        from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
   2.329        then have "inj_on (op ^ p) U" for U
   2.330          by (rule subset_inj_on) simp
   2.331 @@ -202,43 +387,275 @@
   2.332        then have "N \<noteq> {}" by blast
   2.333        note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
   2.334        from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
   2.335 -      with * show "Max N > 0"
   2.336 +      with * have "Max N > 0"
   2.337          by (auto simp add: Max_gr_iff)
   2.338 +      then show "n > 0" by (simp add: n_M)
   2.339        from * have "Max N \<in> N" by (rule Max_in)
   2.340 -      then show "p ^ Max N dvd a" by (simp add: N_def)
   2.341 +      then have "p ^ Max N dvd a" by (simp add: N_def)
   2.342 +      then show "p ^ n dvd a" by (simp add: n_M)
   2.343        from * have "\<forall>n\<in>N. n \<le> Max N"
   2.344          by (simp add: Max_le_iff [symmetric])
   2.345        then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
   2.346          by (rule bspec) (simp add: N_def)
   2.347 -      then show "\<not> p ^ Suc (Max N) dvd a"
   2.348 +      then have "\<not> p ^ Suc (Max N) dvd a"
   2.349          by auto
   2.350 +      then show "\<not> p ^ Suc n dvd a"
   2.351 +        by (simp add: n_M)
   2.352      qed
   2.353 -    from \<open>p ^ n dvd a\<close> obtain c where "a = p ^ n * c" ..
   2.354 -    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd c"
   2.355 +    def b \<equiv> "a div p ^ n"
   2.356 +    with \<open>p ^ n dvd a\<close> have a: "a = p ^ n * b"
   2.357 +      by simp
   2.358 +    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd b" and "b \<noteq> 0"
   2.359        by (auto elim: dvdE simp add: ac_simps)
   2.360 -    have "?prime_factors a - {p} = ?prime_factors c" (is "?A = ?B")
   2.361 +    have "?prime_factors a = insert p (?prime_factors b)"
   2.362      proof (rule set_eqI)
   2.363        fix q
   2.364 -      show "q \<in> ?A \<longleftrightarrow> q \<in> ?B"
   2.365 -      using \<open>normalize p = p\<close> \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>\<not> p dvd c\<close>
   2.366 -        prime_unique [of q p]
   2.367 -        by (auto simp add: prime_dvd_power_iff prime_dvd_mult_iff)
   2.368 +      show "q \<in> ?prime_factors a \<longleftrightarrow> q \<in> insert p (?prime_factors b)"
   2.369 +      using \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close>
   2.370 +        by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff)
   2.371 +          (auto dest: is_prime_associated)
   2.372      qed
   2.373 -    moreover from insert have "P = ?prime_factors a - {p}"
   2.374 +    with \<open>\<not> p dvd b\<close> have "?prime_factors a - {p} = ?prime_factors b"
   2.375 +      by auto
   2.376 +    with insert.hyps have "F = ?prime_factors b"
   2.377        by auto
   2.378 -    ultimately have "P = ?prime_factors c"
   2.379 +    then have "?prime_factors b = F"
   2.380 +      by simp
   2.381 +    with \<open>?prime_factors a = insert p (?prime_factors b)\<close> have "?prime_factors a = insert p F"
   2.382        by simp
   2.383 -    moreover from \<open>a \<noteq> 0\<close> \<open>a = p ^ n * c\<close> have "c \<noteq> 0"
   2.384 -      by auto
   2.385 -    ultimately obtain P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize c"
   2.386 -      using insert(3) by blast 
   2.387 -    with \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>normalize p = p\<close>
   2.388 -    have "\<And>q. q \<in># P + (replicate_mset n p) \<longrightarrow> is_prime q" "msetprod (P + replicate_mset n p) = normalize a"
   2.389 -      by (auto simp add: ac_simps normalize_mult normalize_power)
   2.390 -    with insert(6) show thesis by blast
   2.391 +    have equiv: "(\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p) =
   2.392 +      (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p)"
   2.393 +    using refl proof (rule Groups_Big.setsum.cong)
   2.394 +      fix q
   2.395 +      assume "q \<in> F"
   2.396 +      have "{n. q ^ n dvd a} = {n. q ^ n dvd b}"
   2.397 +      proof -
   2.398 +        have "q ^ m dvd a \<longleftrightarrow> q ^ m dvd b" (is "?R \<longleftrightarrow> ?S")
   2.399 +          for m
   2.400 +        proof (cases "m = 0")
   2.401 +          case True then show ?thesis by simp
   2.402 +        next
   2.403 +          case False then have "m > 0" by simp
   2.404 +          show ?thesis
   2.405 +          proof
   2.406 +            assume ?S then show ?R by (simp add: a)
   2.407 +          next
   2.408 +            assume ?R
   2.409 +            then have *: "q ^ m dvd p ^ n * b" by (simp add: a)
   2.410 +            from insert.hyps \<open>q \<in> F\<close>
   2.411 +            have "is_prime q" "normalize q = q" "p \<noteq> q" "q dvd p ^ n * b"
   2.412 +              by (auto simp add: a)
   2.413 +            from \<open>is_prime q\<close> * \<open>m > 0\<close> show ?S
   2.414 +            proof (rule prime_power_dvd_multD)
   2.415 +              have "\<not> q dvd p"
   2.416 +              proof
   2.417 +                assume "q dvd p"
   2.418 +                with \<open>is_prime q\<close> \<open>is_prime p\<close> have "normalize q = normalize p"
   2.419 +                  by (blast intro: is_prime_associated)
   2.420 +                with \<open>normalize p = p\<close> \<open>normalize q = q\<close> \<open>p \<noteq> q\<close> show False
   2.421 +                  by simp
   2.422 +              qed
   2.423 +              with \<open>is_prime q\<close> show "\<not> q dvd p ^ n"
   2.424 +                by (simp add: prime_dvd_power_iff)
   2.425 +            qed
   2.426 +          qed
   2.427 +        qed
   2.428 +        then show ?thesis by auto
   2.429 +      qed
   2.430 +      then show
   2.431 +        "replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q"
   2.432 +        by simp
   2.433 +    qed
   2.434 +    def Q \<equiv> "the (factorization b)"
   2.435 +    with \<open>b \<noteq> 0\<close> have [simp]: "factorization b = Some Q"
   2.436 +      by simp
   2.437 +    from \<open>a \<noteq> 0\<close> have "factorization a =
   2.438 +      Some (\<Sum>p\<in>?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)"
   2.439 +      by (simp add: factorization_def)
   2.440 +    also have "\<dots> =
   2.441 +      Some (\<Sum>p\<in>insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)"
   2.442 +      by (simp add: \<open>?prime_factors a = insert p F\<close>)
   2.443 +    also have "\<dots> =
   2.444 +      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p))"
   2.445 +      using \<open>finite F\<close> \<open>p \<notin> F\<close> n_def by simp
   2.446 +    also have "\<dots> =
   2.447 +      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p))"
   2.448 +      using equiv by simp
   2.449 +    also have "\<dots> = Some (replicate_mset n p + the (factorization b))"
   2.450 +      using \<open>b \<noteq> 0\<close> by (simp add: factorization_def \<open>?prime_factors a = insert p F\<close> \<open>?prime_factors b = F\<close>)
   2.451 +    finally have fact_a: "factorization a = 
   2.452 +      Some (replicate_mset n p + Q)"
   2.453 +      by simp
   2.454 +    moreover have "factorization b = Some Q \<longleftrightarrow>
   2.455 +      normalize b = msetprod Q \<and>
   2.456 +      0 \<notin># Q \<and>
   2.457 +      (\<forall>p\<in>#Q. is_prime p \<and> normalize p = p)"
   2.458 +      using \<open>F = ?prime_factors b\<close> \<open>b \<noteq> 0\<close> by (rule insert.hyps)
   2.459 +    ultimately have
   2.460 +      norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and
   2.461 +      prime_Q: "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
   2.462 +      by (simp_all add: a normalize_mult normalize_power \<open>normalize p = p\<close>)
   2.463 +    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
   2.464 +      assume ?lhs with fact_a
   2.465 +      have "P = replicate_mset n p + Q" by simp
   2.466 +      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> prime_Q
   2.467 +        show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI)
   2.468 +    next
   2.469 +      assume ?rhs
   2.470 +      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close> prime_Q
   2.471 +      have "msetprod P = msetprod (replicate_mset n p + Q)"
   2.472 +        and "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p"
   2.473 +        and "\<forall>p\<in>set_mset (replicate_mset n p + Q). is_prime p \<and> normalize p = p"
   2.474 +        by (simp_all add: norm_a)
   2.475 +      then have "P = replicate_mset n p + Q"
   2.476 +        by (simp only: msetprod_eq_iff)
   2.477 +      then show ?lhs
   2.478 +        by (simp add: fact_a)
   2.479 +    qed
   2.480    qed
   2.481  qed
   2.482 -  
   2.483 +
   2.484 +lemma factorization_cases [case_names 0 factorization]:
   2.485 +  assumes "0": "a = 0 \<Longrightarrow> P"
   2.486 +  assumes factorization: "\<And>A. a \<noteq> 0 \<Longrightarrow> factorization a = Some A \<Longrightarrow> msetprod A = normalize a
   2.487 +    \<Longrightarrow> 0 \<notin># A \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> normalize p = p) \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> P"
   2.488 +  shows P
   2.489 +proof (cases "a = 0")
   2.490 +  case True with 0 show P .
   2.491 +next
   2.492 +  case False
   2.493 +  then have "factorization a \<noteq> None" by simp
   2.494 +  then obtain A where "factorization a = Some A" by blast
   2.495 +  moreover from this have "msetprod A = normalize a"
   2.496 +    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
   2.497 +    by (auto simp add: factorization_eq_Some_iff)
   2.498 +  ultimately show P using \<open>a \<noteq> 0\<close> factorization by blast
   2.499 +qed
   2.500 +
   2.501 +lemma factorizationE:
   2.502 +  assumes "a \<noteq> 0"
   2.503 +  obtains A u where "factorization a = Some A" "normalize a = msetprod A"
   2.504 +    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
   2.505 +  using assms by (cases a rule: factorization_cases) simp_all
   2.506 +
   2.507 +lemma prime_dvd_mset_prod_iff:
   2.508 +  assumes "is_prime p" "normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
   2.509 +  shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
   2.510 +using assms proof (induct A)
   2.511 +  case empty then show ?case by (auto dest: is_prime_not_unit)
   2.512 +next
   2.513 +  case (add A q) then show ?case
   2.514 +    using is_prime_associated [of q p]
   2.515 +    by (simp_all add: prime_dvd_mult_iff, safe, simp_all)
   2.516 +qed
   2.517 +
   2.518 +end
   2.519 +
   2.520 +class factorial_semiring_gcd = factorial_semiring + gcd +
   2.521 +  assumes gcd_unfold: "gcd a b =
   2.522 +    (if a = 0 then normalize b
   2.523 +     else if b = 0 then normalize a
   2.524 +     else msetprod (the (factorization a) #\<inter> the (factorization b)))"
   2.525 +  and lcm_unfold: "lcm a b =
   2.526 +    (if a = 0 \<or> b = 0 then 0
   2.527 +     else msetprod (the (factorization a) #\<union> the (factorization b)))"
   2.528 +begin
   2.529 +
   2.530 +subclass semiring_gcd
   2.531 +proof
   2.532 +  fix a b
   2.533 +  have comm: "gcd a b = gcd b a" for a b
   2.534 +   by (simp add: gcd_unfold ac_simps)
   2.535 +  have "gcd a b dvd a" for a b
   2.536 +  proof (cases a rule: factorization_cases)
   2.537 +    case 0 then show ?thesis by simp
   2.538 +  next
   2.539 +    case (factorization A) note fact_A = this
   2.540 +    then have non_zero: "\<And>p. p \<in>#A \<Longrightarrow> p \<noteq> 0"
   2.541 +      using normalize_0 not_is_prime_zero by blast
   2.542 +    show ?thesis
   2.543 +    proof (cases b rule: factorization_cases)
   2.544 +      case 0 then show ?thesis by (simp add: gcd_unfold)
   2.545 +    next
   2.546 +      case (factorization B) note fact_B = this
   2.547 +      have "msetprod (A #\<inter> B) dvd msetprod A"
   2.548 +      using non_zero proof (induct B arbitrary: A)
   2.549 +        case empty show ?case by simp
   2.550 +      next
   2.551 +        case (add B p) show ?case
   2.552 +        proof (cases "p \<in># A")
   2.553 +          case True then obtain C where "A = C + {#p#}"
   2.554 +            by (metis insert_DiffM2)
   2.555 +          moreover with True add have "p \<noteq> 0" and "\<And>p. p \<in># C \<Longrightarrow> p \<noteq> 0"
   2.556 +            by auto
   2.557 +          ultimately show ?thesis
   2.558 +            using True add.hyps [of C]
   2.559 +            by (simp add: inter_union_distrib_left [symmetric])
   2.560 +        next
   2.561 +          case False with add.prems add.hyps [of A] show ?thesis
   2.562 +            by (simp add: inter_add_right1)
   2.563 +        qed
   2.564 +      qed
   2.565 +      with fact_A fact_B show ?thesis by (simp add: gcd_unfold)
   2.566 +    qed
   2.567 +  qed
   2.568 +  then have "gcd a b dvd a" and "gcd b a dvd b"
   2.569 +    by simp_all
   2.570 +  then show "gcd a b dvd a" and "gcd a b dvd b"
   2.571 +    by (simp_all add: comm)
   2.572 +  show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c
   2.573 +  proof (cases "a = 0 \<or> b = 0 \<or> c = 0")
   2.574 +    case True with that show ?thesis by (auto simp add: gcd_unfold)
   2.575 +  next
   2.576 +    case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
   2.577 +      by simp_all
   2.578 +    then obtain A B C where fact:
   2.579 +      "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
   2.580 +      and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
   2.581 +      and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
   2.582 +      and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
   2.583 +      and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
   2.584 +      by (blast elim!: factorizationE)
   2.585 +    moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
   2.586 +      by simp_all
   2.587 +    ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B"
   2.588 +      by simp_all
   2.589 +    with A B C have "msetprod C dvd msetprod (A #\<inter> B)"
   2.590 +    proof (induct C arbitrary: A B)
   2.591 +      case empty then show ?case by simp
   2.592 +    next
   2.593 +      case add: (add C p)
   2.594 +      from add.prems
   2.595 +        have p: "p \<noteq> 0" "is_prime p" "normalize p = p" by auto
   2.596 +      from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B"
   2.597 +        by simp_all
   2.598 +      then have "p dvd msetprod A" "p dvd msetprod B"
   2.599 +        by (auto dest: dvd_mult_imp_div dvd_mult_right)
   2.600 +      with p add.prems have "p \<in># A" "p \<in># B"
   2.601 +        by (simp_all add: prime_dvd_mset_prod_iff)
   2.602 +      then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'"
   2.603 +        by (auto dest!: multi_member_split simp add: ac_simps)
   2.604 +      with add.prems prems p have "msetprod C dvd msetprod (A' #\<inter> B')"
   2.605 +        by (auto intro: add.hyps simp add: ac_simps)
   2.606 +      with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #\<inter> ({#p#} + B'))"
   2.607 +        by (simp add: inter_union_distrib_right [symmetric])
   2.608 +      then show ?case by (simp add: ABp ac_simps)
   2.609 +    qed
   2.610 +    with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> that fact have "normalize c dvd gcd a b"
   2.611 +      by (simp add: norm [symmetric] gcd_unfold fact)
   2.612 +    then show ?thesis by simp
   2.613 +  qed
   2.614 +  show "normalize (gcd a b) = gcd a b"
   2.615 +    apply (simp add: gcd_unfold)
   2.616 +    apply safe
   2.617 +    apply (rule normalized_msetprodI)
   2.618 +    apply (auto elim: factorizationE)
   2.619 +    done
   2.620 +  show "lcm a b = normalize (a * b) div gcd a b"
   2.621 +    by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult
   2.622 +      union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union)
   2.623 +qed
   2.624 +
   2.625  end
   2.626  
   2.627  instantiation nat :: factorial_semiring