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
```