src/HOL/Number_Theory/Factorial_Ring.thy
author haftmann
Thu Mar 03 08:33:55 2016 +0100 (2016-03-03)
changeset 62499 4a5b81ff5992
parent 62366 95c6cf433c91
child 63040 eb4ddd18d635
permissions -rw-r--r--
constructive formulation of factorization
     1 (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 section \<open>Factorial (semi)rings\<close>
     6 
     7 theory Factorial_Ring
     8 imports Main Primes "~~/src/HOL/Library/Multiset"
     9 begin
    10 
    11 context algebraic_semidom
    12 begin
    13 
    14 lemma dvd_mult_imp_div:
    15   assumes "a * c dvd b"
    16   shows "a dvd b div c"
    17 proof (cases "c = 0")
    18   case True then show ?thesis by simp
    19 next
    20   case False
    21   from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
    22   with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
    23 qed
    24 
    25 end
    26 
    27 class factorial_semiring = normalization_semidom +
    28   assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
    29   fixes is_prime :: "'a \<Rightarrow> bool"
    30   assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
    31     and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
    32     and no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
    33   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"
    34     and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    35 begin
    36 
    37 lemma not_is_prime_one [simp]:
    38   "\<not> is_prime 1"
    39   by (auto dest: is_prime_not_unit)
    40 
    41 lemma is_prime_not_zeroI:
    42   assumes "is_prime p"
    43   shows "p \<noteq> 0"
    44   using assms by (auto intro: ccontr)
    45 
    46 lemma is_prime_multD:
    47   assumes "is_prime (a * b)"
    48   shows "is_unit a \<or> is_unit b"
    49 proof -
    50   from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
    51   moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
    52     by auto
    53   ultimately show ?thesis
    54     using dvd_times_left_cancel_iff [of a b 1]
    55       dvd_times_right_cancel_iff [of b a 1]
    56     by auto
    57 qed
    58 
    59 lemma is_primeD2:
    60   assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
    61   shows "p dvd a"
    62 proof -
    63   from \<open>a dvd p\<close> obtain b where "p = a * b" ..
    64   with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
    65   with \<open>p = a * b\<close> show ?thesis
    66     by (auto simp add: mult_unit_dvd_iff)
    67 qed
    68 
    69 lemma is_prime_mult_unit_left:
    70   assumes "is_prime p"
    71     and "is_unit a"
    72   shows "is_prime (a * p)"
    73 proof (rule is_primeI)
    74   from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
    75     by (auto simp add: is_unit_mult_iff is_prime_not_unit)
    76   show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
    77   proof -
    78     from that \<open>is_unit a\<close> have "b dvd p"
    79       using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
    80     with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
    81       using is_primeD2 [of p b] by auto
    82     with \<open>is_unit a\<close> show ?thesis
    83       using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
    84   qed
    85 qed
    86 
    87 lemma is_primeI2:
    88   assumes "p \<noteq> 0"
    89   assumes "\<not> is_unit p"
    90   assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
    91   shows "is_prime p"
    92 using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
    93   fix a
    94   assume "a dvd p"
    95   then obtain b where "p = a * b" ..
    96   with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
    97   moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
    98   moreover assume "\<not> is_unit a"
    99   ultimately show "p dvd a"
   100     using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
   101 qed    
   102 
   103 lemma not_is_prime_divisorE:
   104   assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
   105   obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
   106 proof -
   107   from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
   108     by (auto intro: is_primeI)
   109   with that show thesis by blast
   110 qed
   111 
   112 lemma is_prime_normalize_iff [simp]:
   113   "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
   114 proof
   115   assume ?Q show ?P
   116     by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
   117 next
   118   assume ?P show ?Q
   119     by (rule is_primeI)
   120       (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)
   121 qed  
   122 
   123 lemma no_prime_divisorsI:
   124   assumes "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime b"
   125   shows "is_unit a"
   126 proof (rule no_prime_divisorsI2)
   127   fix b
   128   assume "b dvd a"
   129   then have "normalize b dvd a"
   130     by simp
   131   moreover have "normalize (normalize b) = normalize b"
   132     by simp
   133   ultimately have "\<not> is_prime (normalize b)"
   134     by (rule assms)
   135   then show "\<not> is_prime b"
   136     by simp
   137 qed
   138 
   139 lemma prime_divisorE:
   140   assumes "a \<noteq> 0" and "\<not> is_unit a" 
   141   obtains p where "is_prime p" and "p dvd a"
   142   using assms no_prime_divisorsI [of a] by blast
   143 
   144 lemma is_prime_associated:
   145   assumes "is_prime p" and "is_prime q" and "q dvd p"
   146   shows "normalize q = normalize p"
   147 using \<open>q dvd p\<close> proof (rule associatedI)
   148   from \<open>is_prime q\<close> have "\<not> is_unit q"
   149     by (simp add: is_prime_not_unit)
   150   with \<open>is_prime p\<close> \<open>q dvd p\<close> show "p dvd q"
   151     by (blast intro: is_primeD2)
   152 qed
   153 
   154 lemma prime_dvd_mult_iff:  
   155   assumes "is_prime p"
   156   shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   157   using assms by (auto dest: is_primeD)
   158 
   159 lemma prime_dvd_msetprod:
   160   assumes "is_prime p"
   161   assumes dvd: "p dvd msetprod A"
   162   obtains a where "a \<in># A" and "p dvd a"
   163 proof -
   164   from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   165   proof (induct A)
   166     case empty then show ?case
   167     using \<open>is_prime p\<close> by (simp add: is_prime_not_unit)
   168   next
   169     case (add A a)
   170     then have "p dvd msetprod A * a" by simp
   171     with \<open>is_prime p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
   172       by (blast dest: is_primeD)
   173     then show ?case proof cases
   174       case B then show ?thesis by auto
   175     next
   176       case A
   177       with add.hyps obtain b where "b \<in># A" "p dvd b"
   178         by auto
   179       then show ?thesis by auto
   180     qed
   181   qed
   182   with that show thesis by blast
   183 qed
   184 
   185 lemma msetprod_eq_iff:
   186   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"
   187   shows "msetprod P = msetprod Q \<longleftrightarrow> P = Q" (is "?R \<longleftrightarrow> ?S")
   188 proof
   189   assume ?S then show ?R by simp
   190 next
   191   assume ?R then show ?S using assms proof (induct P arbitrary: Q)
   192     case empty then have Q: "msetprod Q = 1" by simp
   193     have "Q = {#}"
   194     proof (rule ccontr)
   195       assume "Q \<noteq> {#}"
   196       then obtain r R where "Q = R + {#r#}"
   197         using multi_nonempty_split by blast 
   198       moreover with empty have "is_prime r" by simp
   199       ultimately have "msetprod Q = msetprod R * r"
   200         by simp
   201       with Q have "msetprod R * r = 1"
   202         by simp
   203       then have "is_unit r"
   204         by (metis local.dvd_triv_right)
   205       with \<open>is_prime r\<close> show False by (simp add: is_prime_not_unit)
   206     qed
   207     then show ?case by simp
   208   next
   209     case (add P p)
   210     then have "is_prime p" and "normalize p = p"
   211       and "msetprod Q = msetprod P * p" and "p dvd msetprod Q"
   212       by auto (metis local.dvd_triv_right)
   213     with prime_dvd_msetprod
   214       obtain q where "q \<in># Q" and "p dvd q"
   215       by blast
   216     with add.prems have "is_prime q" and "normalize q = q"
   217       by simp_all
   218     from \<open>is_prime p\<close> have "p \<noteq> 0"
   219       by auto 
   220     from \<open>is_prime q\<close> \<open>is_prime p\<close> \<open>p dvd q\<close>
   221       have "normalize p = normalize q"
   222       by (rule is_prime_associated)
   223     from \<open>normalize p = p\<close> \<open>normalize q = q\<close> have "p = q"
   224       unfolding \<open>normalize p = normalize q\<close> by simp
   225     with \<open>q \<in># Q\<close> have "p \<in># Q" by simp
   226     have "msetprod P = msetprod (Q - {#p#})"
   227       using \<open>p \<in># Q\<close> \<open>p \<noteq> 0\<close> \<open>msetprod Q = msetprod P * p\<close>
   228       by (simp add: msetprod_minus)
   229     then have "P = Q - {#p#}"
   230       using add.prems(2-3)
   231       by (auto intro: add.hyps dest: in_diffD)
   232     with \<open>p \<in># Q\<close> show ?case by simp
   233   qed
   234 qed
   235 
   236 lemma prime_dvd_power_iff:
   237   assumes "is_prime p"
   238   shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   239   using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
   240 
   241 lemma prime_power_dvd_multD:
   242   assumes "is_prime p"
   243   assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   244   shows "p ^ n dvd b"
   245 using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
   246   case 0 then show ?case by simp
   247 next
   248   case (Suc n) show ?case
   249   proof (cases "n = 0")
   250     case True with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   251       by (simp add: prime_dvd_mult_iff)
   252   next
   253     case False then have "n > 0" by simp
   254     from \<open>is_prime p\<close> have "p \<noteq> 0" by auto
   255     from Suc.prems have *: "p * p ^ n dvd a * b"
   256       by simp
   257     then have "p dvd a * b"
   258       by (rule dvd_mult_left)
   259     with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   260       by (simp add: prime_dvd_mult_iff)
   261     moreover def c \<equiv> "b div p"
   262     ultimately have b: "b = p * c" by simp
   263     with * have "p * p ^ n dvd p * (a * c)"
   264       by (simp add: ac_simps)
   265     with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c"
   266       by simp
   267     with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c"
   268       by blast
   269     with \<open>p \<noteq> 0\<close> show ?thesis
   270       by (simp add: b)
   271   qed
   272 qed
   273 
   274 lemma is_prime_inj_power:
   275   assumes "is_prime p"
   276   shows "inj (op ^ p)"
   277 proof (rule injI, rule ccontr)
   278   fix m n :: nat
   279   have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
   280   proof
   281     assume ?Q then show ?P by simp
   282   next
   283     assume ?P then have "is_unit (p ^ q)" by simp
   284     with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
   285   qed
   286   have *: False if "p ^ m = p ^ n" and "m > n" for m n
   287   proof -
   288     from assms have "p \<noteq> 0"
   289       by (rule is_prime_not_zeroI)
   290     then have "p ^ n \<noteq> 0"
   291       by (induct n) simp_all
   292     from that have "m = n + (m - n)" and "m - n > 0" by arith+
   293     then obtain q where "m = n + q" and "q > 0" ..
   294     with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
   295     with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
   296       using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
   297     with \<open>q > 0\<close> show ?thesis by simp
   298   qed 
   299   assume "m \<noteq> n"
   300   then have "m > n \<or> m < n" by arith
   301   moreover assume "p ^ m = p ^ n"
   302   ultimately show False using * [of m n] * [of n m] by auto
   303 qed
   304 
   305 definition factorization :: "'a \<Rightarrow> 'a multiset option"
   306   where "factorization a = (if a = 0 then None
   307     else Some (setsum (\<lambda>p. replicate_mset (Max {n. p ^ n dvd a}) p)
   308       {p. p dvd a \<and> is_prime p \<and> normalize p = p}))"
   309 
   310 lemma factorization_normalize [simp]:
   311   "factorization (normalize a) = factorization a"
   312   by (simp add: factorization_def)
   313 
   314 lemma factorization_0 [simp]:
   315   "factorization 0 = None"
   316   by (simp add: factorization_def)
   317 
   318 lemma factorization_eq_None_iff [simp]:
   319   "factorization a = None \<longleftrightarrow> a = 0"
   320   by (simp add: factorization_def)
   321 
   322 lemma factorization_eq_Some_iff:
   323   "factorization a = Some P \<longleftrightarrow>
   324    normalize a = msetprod P \<and> 0 \<notin># P \<and> (\<forall>p \<in> set_mset P. is_prime p \<and> normalize p = p)"
   325 proof (cases "a = 0")
   326   have [simp]: "0 = msetprod P \<longleftrightarrow> 0 \<in># P"
   327     using msetprod_zero_iff [of P] by blast
   328   case True
   329   then show ?thesis by auto
   330 next
   331   case False    
   332   let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
   333   have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}"
   334     by auto
   335   moreover from \<open>a \<noteq> 0\<close> have "finite {b. b dvd a \<and> normalize b = b}"
   336     by (rule finite_divisors)
   337   ultimately have "finite (?prime_factors a)"
   338     by (rule finite_subset)
   339   then show ?thesis using \<open>a \<noteq> 0\<close>
   340   proof (induct "?prime_factors a" arbitrary: a P)
   341     case empty then have
   342       *: "{p. p dvd a \<and> is_prime p \<and> normalize p = p} = {}"
   343         and "a \<noteq> 0"
   344       by auto
   345     from \<open>a \<noteq> 0\<close> have "factorization a = Some {#}"
   346       by (simp only: factorization_def *) simp
   347     from * have "normalize a = 1"
   348       by (auto intro: is_unit_normalize no_prime_divisorsI)
   349     show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
   350       assume ?lhs with \<open>factorization a = Some {#}\<close> \<open>normalize a = 1\<close>
   351       show ?rhs by simp
   352     next
   353       assume ?rhs have "P = {#}"
   354       proof (rule ccontr)
   355         assume "P \<noteq> {#}"
   356         then obtain q Q where "P = Q + {#q#}"
   357           using multi_nonempty_split by blast
   358         with \<open>?rhs\<close> \<open>normalize a = 1\<close>
   359         have "1 = q * msetprod Q" and "is_prime q"
   360           by (simp_all add: ac_simps)
   361         then have "is_unit q" by (auto intro: dvdI)
   362         with \<open>is_prime q\<close> show False
   363           using is_prime_not_unit by blast
   364       qed
   365       with \<open>factorization a = Some {#}\<close> show ?lhs by simp
   366     qed
   367   next
   368     case (insert p F)
   369     from \<open>insert p F = ?prime_factors a\<close>
   370     have "?prime_factors a = insert p F"
   371       by simp
   372     then have "p dvd a" and "is_prime p" and "normalize p = p" and "p \<noteq> 0"
   373       by (auto intro!: is_prime_not_zeroI)
   374     def n \<equiv> "Max {n. p ^ n dvd a}"
   375     then have "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
   376     proof -
   377       def N \<equiv> "{n. p ^ n dvd a}"
   378       then have n_M: "n = Max N" by (simp add: n_def)
   379       from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
   380       then have "inj_on (op ^ p) U" for U
   381         by (rule subset_inj_on) simp
   382       moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
   383         by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
   384       ultimately have "finite N"
   385         by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
   386       from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
   387       then have "N \<noteq> {}" by blast
   388       note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
   389       from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
   390       with * have "Max N > 0"
   391         by (auto simp add: Max_gr_iff)
   392       then show "n > 0" by (simp add: n_M)
   393       from * have "Max N \<in> N" by (rule Max_in)
   394       then have "p ^ Max N dvd a" by (simp add: N_def)
   395       then show "p ^ n dvd a" by (simp add: n_M)
   396       from * have "\<forall>n\<in>N. n \<le> Max N"
   397         by (simp add: Max_le_iff [symmetric])
   398       then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
   399         by (rule bspec) (simp add: N_def)
   400       then have "\<not> p ^ Suc (Max N) dvd a"
   401         by auto
   402       then show "\<not> p ^ Suc n dvd a"
   403         by (simp add: n_M)
   404     qed
   405     def b \<equiv> "a div p ^ n"
   406     with \<open>p ^ n dvd a\<close> have a: "a = p ^ n * b"
   407       by simp
   408     with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd b" and "b \<noteq> 0"
   409       by (auto elim: dvdE simp add: ac_simps)
   410     have "?prime_factors a = insert p (?prime_factors b)"
   411     proof (rule set_eqI)
   412       fix q
   413       show "q \<in> ?prime_factors a \<longleftrightarrow> q \<in> insert p (?prime_factors b)"
   414       using \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close>
   415         by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff)
   416           (auto dest: is_prime_associated)
   417     qed
   418     with \<open>\<not> p dvd b\<close> have "?prime_factors a - {p} = ?prime_factors b"
   419       by auto
   420     with insert.hyps have "F = ?prime_factors b"
   421       by auto
   422     then have "?prime_factors b = F"
   423       by simp
   424     with \<open>?prime_factors a = insert p (?prime_factors b)\<close> have "?prime_factors a = insert p F"
   425       by simp
   426     have equiv: "(\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p) =
   427       (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p)"
   428     using refl proof (rule Groups_Big.setsum.cong)
   429       fix q
   430       assume "q \<in> F"
   431       have "{n. q ^ n dvd a} = {n. q ^ n dvd b}"
   432       proof -
   433         have "q ^ m dvd a \<longleftrightarrow> q ^ m dvd b" (is "?R \<longleftrightarrow> ?S")
   434           for m
   435         proof (cases "m = 0")
   436           case True then show ?thesis by simp
   437         next
   438           case False then have "m > 0" by simp
   439           show ?thesis
   440           proof
   441             assume ?S then show ?R by (simp add: a)
   442           next
   443             assume ?R
   444             then have *: "q ^ m dvd p ^ n * b" by (simp add: a)
   445             from insert.hyps \<open>q \<in> F\<close>
   446             have "is_prime q" "normalize q = q" "p \<noteq> q" "q dvd p ^ n * b"
   447               by (auto simp add: a)
   448             from \<open>is_prime q\<close> * \<open>m > 0\<close> show ?S
   449             proof (rule prime_power_dvd_multD)
   450               have "\<not> q dvd p"
   451               proof
   452                 assume "q dvd p"
   453                 with \<open>is_prime q\<close> \<open>is_prime p\<close> have "normalize q = normalize p"
   454                   by (blast intro: is_prime_associated)
   455                 with \<open>normalize p = p\<close> \<open>normalize q = q\<close> \<open>p \<noteq> q\<close> show False
   456                   by simp
   457               qed
   458               with \<open>is_prime q\<close> show "\<not> q dvd p ^ n"
   459                 by (simp add: prime_dvd_power_iff)
   460             qed
   461           qed
   462         qed
   463         then show ?thesis by auto
   464       qed
   465       then show
   466         "replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q"
   467         by simp
   468     qed
   469     def Q \<equiv> "the (factorization b)"
   470     with \<open>b \<noteq> 0\<close> have [simp]: "factorization b = Some Q"
   471       by simp
   472     from \<open>a \<noteq> 0\<close> have "factorization a =
   473       Some (\<Sum>p\<in>?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)"
   474       by (simp add: factorization_def)
   475     also have "\<dots> =
   476       Some (\<Sum>p\<in>insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)"
   477       by (simp add: \<open>?prime_factors a = insert p F\<close>)
   478     also have "\<dots> =
   479       Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p))"
   480       using \<open>finite F\<close> \<open>p \<notin> F\<close> n_def by simp
   481     also have "\<dots> =
   482       Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p))"
   483       using equiv by simp
   484     also have "\<dots> = Some (replicate_mset n p + the (factorization b))"
   485       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>)
   486     finally have fact_a: "factorization a = 
   487       Some (replicate_mset n p + Q)"
   488       by simp
   489     moreover have "factorization b = Some Q \<longleftrightarrow>
   490       normalize b = msetprod Q \<and>
   491       0 \<notin># Q \<and>
   492       (\<forall>p\<in>#Q. is_prime p \<and> normalize p = p)"
   493       using \<open>F = ?prime_factors b\<close> \<open>b \<noteq> 0\<close> by (rule insert.hyps)
   494     ultimately have
   495       norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and
   496       prime_Q: "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
   497       by (simp_all add: a normalize_mult normalize_power \<open>normalize p = p\<close>)
   498     show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
   499       assume ?lhs with fact_a
   500       have "P = replicate_mset n p + Q" by simp
   501       with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> prime_Q
   502         show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI)
   503     next
   504       assume ?rhs
   505       with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close> prime_Q
   506       have "msetprod P = msetprod (replicate_mset n p + Q)"
   507         and "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p"
   508         and "\<forall>p\<in>set_mset (replicate_mset n p + Q). is_prime p \<and> normalize p = p"
   509         by (simp_all add: norm_a)
   510       then have "P = replicate_mset n p + Q"
   511         by (simp only: msetprod_eq_iff)
   512       then show ?lhs
   513         by (simp add: fact_a)
   514     qed
   515   qed
   516 qed
   517 
   518 lemma factorization_cases [case_names 0 factorization]:
   519   assumes "0": "a = 0 \<Longrightarrow> P"
   520   assumes factorization: "\<And>A. a \<noteq> 0 \<Longrightarrow> factorization a = Some A \<Longrightarrow> msetprod A = normalize a
   521     \<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"
   522   shows P
   523 proof (cases "a = 0")
   524   case True with 0 show P .
   525 next
   526   case False
   527   then have "factorization a \<noteq> None" by simp
   528   then obtain A where "factorization a = Some A" by blast
   529   moreover from this have "msetprod A = normalize a"
   530     "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
   531     by (auto simp add: factorization_eq_Some_iff)
   532   ultimately show P using \<open>a \<noteq> 0\<close> factorization by blast
   533 qed
   534 
   535 lemma factorizationE:
   536   assumes "a \<noteq> 0"
   537   obtains A u where "factorization a = Some A" "normalize a = msetprod A"
   538     "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
   539   using assms by (cases a rule: factorization_cases) simp_all
   540 
   541 lemma prime_dvd_mset_prod_iff:
   542   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"
   543   shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
   544 using assms proof (induct A)
   545   case empty then show ?case by (auto dest: is_prime_not_unit)
   546 next
   547   case (add A q) then show ?case
   548     using is_prime_associated [of q p]
   549     by (simp_all add: prime_dvd_mult_iff, safe, simp_all)
   550 qed
   551 
   552 end
   553 
   554 class factorial_semiring_gcd = factorial_semiring + gcd +
   555   assumes gcd_unfold: "gcd a b =
   556     (if a = 0 then normalize b
   557      else if b = 0 then normalize a
   558      else msetprod (the (factorization a) #\<inter> the (factorization b)))"
   559   and lcm_unfold: "lcm a b =
   560     (if a = 0 \<or> b = 0 then 0
   561      else msetprod (the (factorization a) #\<union> the (factorization b)))"
   562 begin
   563 
   564 subclass semiring_gcd
   565 proof
   566   fix a b
   567   have comm: "gcd a b = gcd b a" for a b
   568    by (simp add: gcd_unfold ac_simps)
   569   have "gcd a b dvd a" for a b
   570   proof (cases a rule: factorization_cases)
   571     case 0 then show ?thesis by simp
   572   next
   573     case (factorization A) note fact_A = this
   574     then have non_zero: "\<And>p. p \<in>#A \<Longrightarrow> p \<noteq> 0"
   575       using normalize_0 not_is_prime_zero by blast
   576     show ?thesis
   577     proof (cases b rule: factorization_cases)
   578       case 0 then show ?thesis by (simp add: gcd_unfold)
   579     next
   580       case (factorization B) note fact_B = this
   581       have "msetprod (A #\<inter> B) dvd msetprod A"
   582       using non_zero proof (induct B arbitrary: A)
   583         case empty show ?case by simp
   584       next
   585         case (add B p) show ?case
   586         proof (cases "p \<in># A")
   587           case True then obtain C where "A = C + {#p#}"
   588             by (metis insert_DiffM2)
   589           moreover with True add have "p \<noteq> 0" and "\<And>p. p \<in># C \<Longrightarrow> p \<noteq> 0"
   590             by auto
   591           ultimately show ?thesis
   592             using True add.hyps [of C]
   593             by (simp add: inter_union_distrib_left [symmetric])
   594         next
   595           case False with add.prems add.hyps [of A] show ?thesis
   596             by (simp add: inter_add_right1)
   597         qed
   598       qed
   599       with fact_A fact_B show ?thesis by (simp add: gcd_unfold)
   600     qed
   601   qed
   602   then have "gcd a b dvd a" and "gcd b a dvd b"
   603     by simp_all
   604   then show "gcd a b dvd a" and "gcd a b dvd b"
   605     by (simp_all add: comm)
   606   show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c
   607   proof (cases "a = 0 \<or> b = 0 \<or> c = 0")
   608     case True with that show ?thesis by (auto simp add: gcd_unfold)
   609   next
   610     case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
   611       by simp_all
   612     then obtain A B C where fact:
   613       "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
   614       and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
   615       and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
   616       and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
   617       and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
   618       by (blast elim!: factorizationE)
   619     moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
   620       by simp_all
   621     ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B"
   622       by simp_all
   623     with A B C have "msetprod C dvd msetprod (A #\<inter> B)"
   624     proof (induct C arbitrary: A B)
   625       case empty then show ?case by simp
   626     next
   627       case add: (add C p)
   628       from add.prems
   629         have p: "p \<noteq> 0" "is_prime p" "normalize p = p" by auto
   630       from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B"
   631         by simp_all
   632       then have "p dvd msetprod A" "p dvd msetprod B"
   633         by (auto dest: dvd_mult_imp_div dvd_mult_right)
   634       with p add.prems have "p \<in># A" "p \<in># B"
   635         by (simp_all add: prime_dvd_mset_prod_iff)
   636       then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'"
   637         by (auto dest!: multi_member_split simp add: ac_simps)
   638       with add.prems prems p have "msetprod C dvd msetprod (A' #\<inter> B')"
   639         by (auto intro: add.hyps simp add: ac_simps)
   640       with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #\<inter> ({#p#} + B'))"
   641         by (simp add: inter_union_distrib_right [symmetric])
   642       then show ?case by (simp add: ABp ac_simps)
   643     qed
   644     with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> that fact have "normalize c dvd gcd a b"
   645       by (simp add: norm [symmetric] gcd_unfold fact)
   646     then show ?thesis by simp
   647   qed
   648   show "normalize (gcd a b) = gcd a b"
   649     apply (simp add: gcd_unfold)
   650     apply safe
   651     apply (rule normalized_msetprodI)
   652     apply (auto elim: factorizationE)
   653     done
   654   show "lcm a b = normalize (a * b) div gcd a b"
   655     by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult
   656       union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union)
   657 qed
   658 
   659 end
   660 
   661 instantiation nat :: factorial_semiring
   662 begin
   663 
   664 definition is_prime_nat :: "nat \<Rightarrow> bool"
   665 where
   666   "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
   667 
   668 lemma is_prime_eq_prime:
   669   "is_prime = prime"
   670   by (simp add: fun_eq_iff prime_def is_prime_nat_def)
   671 
   672 instance proof
   673   show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
   674   show "\<not> is_unit p" if "is_prime p" for p :: nat
   675     using that by (simp add: is_prime_nat_def)
   676 next
   677   fix p :: nat
   678   assume "p \<noteq> 0" and "\<not> is_unit p"
   679   then have "p > 1" by simp
   680   assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
   681   have "n = 1" if "n dvd p" "n \<noteq> p" for n
   682   proof (rule ccontr)
   683     assume "n \<noteq> 1"
   684     with that P have "p dvd n" by auto
   685     with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
   686     with that show False by simp
   687   qed
   688   with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
   689 next
   690   fix p m n :: nat
   691   assume "is_prime p"
   692   then have "prime p" by (simp add: is_prime_eq_prime)
   693   moreover assume "p dvd m * n"
   694   ultimately show "p dvd m \<or> p dvd n"
   695     by (rule prime_dvd_mult_nat)
   696 next
   697   fix n :: nat
   698   show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
   699     using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
   700 qed simp
   701 
   702 end
   703 
   704 instantiation int :: factorial_semiring
   705 begin
   706 
   707 definition is_prime_int :: "int \<Rightarrow> bool"
   708 where
   709   "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
   710 
   711 lemma is_prime_int_iff [simp]:
   712   "is_prime (int n) \<longleftrightarrow> is_prime n"
   713   by (simp add: is_prime_int_def)
   714 
   715 lemma is_prime_nat_abs_iff [simp]:
   716   "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
   717   by (simp add: is_prime_int_def)
   718 
   719 instance proof
   720   show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
   721   show "\<not> is_unit p" if "is_prime p" for p :: int
   722     using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
   723 next
   724   fix p :: int
   725   assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
   726   have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
   727   proof -
   728     from that have "int n dvd p" by (simp add: int_dvd_iff)
   729     moreover from that have "\<not> is_unit (int n)" by simp
   730     ultimately have "p dvd int n" by (rule P)
   731     with that have "p dvd int n" by auto
   732     then show ?thesis by (simp add: dvd_int_iff)
   733   qed
   734   moreover assume "p \<noteq> 0" and "\<not> is_unit p"
   735   ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
   736   then show "is_prime p" by simp
   737 next
   738   fix p k l :: int
   739   assume "is_prime p"
   740   then have *: "is_prime (nat \<bar>p\<bar>)" by simp
   741   assume "p dvd k * l"
   742   then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
   743     by (simp add: dvd_int_unfold_dvd_nat)
   744   then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
   745     by (simp add: abs_mult nat_mult_distrib)
   746   with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
   747     using is_primeD [of "nat \<bar>p\<bar>"] by auto
   748   then show "p dvd k \<or> p dvd l"
   749     by (simp add: dvd_int_unfold_dvd_nat)
   750 next
   751   fix k :: int
   752   assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
   753   have "is_unit (nat \<bar>k\<bar>)"
   754   proof (rule no_prime_divisorsI)
   755     fix m
   756     assume "m dvd nat \<bar>k\<bar>"
   757     then have "int m dvd k" by (simp add: int_dvd_iff)
   758     then have "\<not> is_prime (int m)" by (rule P)
   759     then show "\<not> is_prime m" by simp
   760   qed
   761   then show "is_unit k" by simp
   762 qed simp
   763 
   764 end
   765 
   766 end