src/HOL/Computational_Algebra/Factorial_Ring.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 66938 c78ff0aeba4c
child 67051 e7e54a0b9197
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Computational_Algebra/Factorial_Ring.thy
     2     Author:     Manuel Eberl, TU Muenchen
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 section \<open>Factorial (semi)rings\<close>
     7 
     8 theory Factorial_Ring
     9 imports
    10   Main
    11   "HOL-Library.Multiset"
    12 begin
    13 
    14 subsection \<open>Irreducible and prime elements\<close>
    15 
    16 (* TODO: Move ? *)
    17 lemma (in semiring_gcd) prod_coprime' [rule_format]: 
    18     "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
    19   using prod_coprime[of A f a] by (simp add: gcd.commute)
    20 
    21 
    22 context comm_semiring_1
    23 begin
    24 
    25 definition irreducible :: "'a \<Rightarrow> bool" where
    26   "irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)"
    27 
    28 lemma not_irreducible_zero [simp]: "\<not>irreducible 0"
    29   by (simp add: irreducible_def)
    30 
    31 lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1"
    32   by (simp add: irreducible_def)
    33 
    34 lemma not_irreducible_one [simp]: "\<not>irreducible 1"
    35   by (simp add: irreducible_def)
    36 
    37 lemma irreducibleI:
    38   "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p"
    39   by (simp add: irreducible_def)
    40 
    41 lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
    42   by (simp add: irreducible_def)
    43 
    44 definition prime_elem :: "'a \<Rightarrow> bool" where
    45   "prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
    46 
    47 lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0"
    48   by (simp add: prime_elem_def)
    49 
    50 lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1"
    51   by (simp add: prime_elem_def)
    52 
    53 lemma prime_elemI:
    54     "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> prime_elem p"
    55   by (simp add: prime_elem_def)
    56 
    57 lemma prime_elem_dvd_multD:
    58     "prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
    59   by (simp add: prime_elem_def)
    60 
    61 lemma prime_elem_dvd_mult_iff:
    62   "prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
    63   by (auto simp: prime_elem_def)
    64 
    65 lemma not_prime_elem_one [simp]:
    66   "\<not> prime_elem 1"
    67   by (auto dest: prime_elem_not_unit)
    68 
    69 lemma prime_elem_not_zeroI:
    70   assumes "prime_elem p"
    71   shows "p \<noteq> 0"
    72   using assms by (auto intro: ccontr)
    73 
    74 lemma prime_elem_dvd_power:
    75   "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    76   by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
    77 
    78 lemma prime_elem_dvd_power_iff:
    79   "prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    80   by (auto dest: prime_elem_dvd_power intro: dvd_trans)
    81 
    82 lemma prime_elem_imp_nonzero [simp]:
    83   "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0"
    84   unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
    85 
    86 lemma prime_elem_imp_not_one [simp]:
    87   "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1"
    88   unfolding ASSUMPTION_def by auto
    89 
    90 end
    91 
    92 context algebraic_semidom
    93 begin
    94 
    95 lemma prime_elem_imp_irreducible:
    96   assumes "prime_elem p"
    97   shows   "irreducible p"
    98 proof (rule irreducibleI)
    99   fix a b
   100   assume p_eq: "p = a * b"
   101   with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
   102   from p_eq have "p dvd a * b" by simp
   103   with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
   104   with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
   105   thus "a dvd 1 \<or> b dvd 1"
   106     by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
   107 qed (insert assms, simp_all add: prime_elem_def)
   108 
   109 lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors:
   110   assumes "is_unit x" "irreducible p"
   111   shows   "\<not>p dvd x"
   112 proof (rule notI)
   113   assume "p dvd x"
   114   with \<open>is_unit x\<close> have "is_unit p"
   115     by (auto intro: dvd_trans)
   116   with \<open>irreducible p\<close> show False
   117     by (simp add: irreducible_not_unit)
   118 qed
   119 
   120 lemma unit_imp_no_prime_divisors:
   121   assumes "is_unit x" "prime_elem p"
   122   shows   "\<not>p dvd x"
   123   using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
   124 
   125 lemma prime_elem_mono:
   126   assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
   127   shows   "prime_elem q"
   128 proof -
   129   from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
   130   hence "p dvd q * r" by simp
   131   with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD)
   132   hence "p dvd q"
   133   proof
   134     assume "p dvd r"
   135     then obtain s where s: "r = p * s" by (elim dvdE)
   136     from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
   137     with \<open>prime_elem p\<close> have "q dvd 1"
   138       by (subst (asm) mult_cancel_left) auto
   139     with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
   140   qed
   141 
   142   show ?thesis
   143   proof (rule prime_elemI)
   144     fix a b assume "q dvd (a * b)"
   145     with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
   146     with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
   147     with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
   148   qed (insert assms, auto)
   149 qed
   150 
   151 lemma irreducibleD':
   152   assumes "irreducible a" "b dvd a"
   153   shows   "a dvd b \<or> is_unit b"
   154 proof -
   155   from assms obtain c where c: "a = b * c" by (elim dvdE)
   156   from irreducibleD[OF assms(1) this] have "is_unit b \<or> is_unit c" .
   157   thus ?thesis by (auto simp: c mult_unit_dvd_iff)
   158 qed
   159 
   160 lemma irreducibleI':
   161   assumes "a \<noteq> 0" "\<not>is_unit a" "\<And>b. b dvd a \<Longrightarrow> a dvd b \<or> is_unit b"
   162   shows   "irreducible a"
   163 proof (rule irreducibleI)
   164   fix b c assume a_eq: "a = b * c"
   165   hence "a dvd b \<or> is_unit b" by (intro assms) simp_all
   166   thus "is_unit b \<or> is_unit c"
   167   proof
   168     assume "a dvd b"
   169     hence "b * c dvd b * 1" by (simp add: a_eq)
   170     moreover from \<open>a \<noteq> 0\<close> a_eq have "b \<noteq> 0" by auto
   171     ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto
   172   qed blast
   173 qed (simp_all add: assms(1,2))
   174 
   175 lemma irreducible_altdef:
   176   "irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)"
   177   using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
   178 
   179 lemma prime_elem_multD:
   180   assumes "prime_elem (a * b)"
   181   shows "is_unit a \<or> is_unit b"
   182 proof -
   183   from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI)
   184   moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
   185     by auto
   186   ultimately show ?thesis
   187     using dvd_times_left_cancel_iff [of a b 1]
   188       dvd_times_right_cancel_iff [of b a 1]
   189     by auto
   190 qed
   191 
   192 lemma prime_elemD2:
   193   assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a"
   194   shows "p dvd a"
   195 proof -
   196   from \<open>a dvd p\<close> obtain b where "p = a * b" ..
   197   with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
   198   with \<open>p = a * b\<close> show ?thesis
   199     by (auto simp add: mult_unit_dvd_iff)
   200 qed
   201 
   202 lemma prime_elem_dvd_prod_msetE:
   203   assumes "prime_elem p"
   204   assumes dvd: "p dvd prod_mset A"
   205   obtains a where "a \<in># A" and "p dvd a"
   206 proof -
   207   from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   208   proof (induct A)
   209     case empty then show ?case
   210     using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
   211   next
   212     case (add a A)
   213     then have "p dvd a * prod_mset A" by simp
   214     with \<open>prime_elem p\<close> consider (A) "p dvd prod_mset A" | (B) "p dvd a"
   215       by (blast dest: prime_elem_dvd_multD)
   216     then show ?case proof cases
   217       case B then show ?thesis by auto
   218     next
   219       case A
   220       with add.hyps obtain b where "b \<in># A" "p dvd b"
   221         by auto
   222       then show ?thesis by auto
   223     qed
   224   qed
   225   with that show thesis by blast
   226 
   227 qed
   228 
   229 context
   230 begin
   231 
   232 private lemma prime_elem_powerD:
   233   assumes "prime_elem (p ^ n)"
   234   shows   "prime_elem p \<and> n = 1"
   235 proof (cases n)
   236   case (Suc m)
   237   note assms
   238   also from Suc have "p ^ n = p * p^m" by simp
   239   finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD)
   240   moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
   241   ultimately have "is_unit (p ^ m)" by simp
   242   with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
   243   with Suc assms show ?thesis by simp
   244 qed (insert assms, simp_all)
   245 
   246 lemma prime_elem_power_iff:
   247   "prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1"
   248   by (auto dest: prime_elem_powerD)
   249 
   250 end
   251 
   252 lemma irreducible_mult_unit_left:
   253   "is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
   254   by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
   255         mult_unit_dvd_iff dvd_mult_unit_iff)
   256 
   257 lemma prime_elem_mult_unit_left:
   258   "is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p"
   259   by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
   260 
   261 lemma prime_elem_dvd_cases:
   262   assumes pk: "p*k dvd m*n" and p: "prime_elem p"
   263   shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
   264 proof -
   265   have "p dvd m*n" using dvd_mult_left pk by blast
   266   then consider "p dvd m" | "p dvd n"
   267     using p prime_elem_dvd_mult_iff by blast
   268   then show ?thesis
   269   proof cases
   270     case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
   271       then have "\<exists>x. k dvd x * n \<and> m = p * x"
   272         using p pk by (auto simp: mult.assoc)
   273     then show ?thesis ..
   274   next
   275     case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
   276     with p pk have "\<exists>y. k dvd m*y \<and> n = p*y"
   277       by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
   278     then show ?thesis ..
   279   qed
   280 qed
   281 
   282 lemma prime_elem_power_dvd_prod:
   283   assumes pc: "p^c dvd m*n" and p: "prime_elem p"
   284   shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
   285 using pc
   286 proof (induct c arbitrary: m n)
   287   case 0 show ?case by simp
   288 next
   289   case (Suc c)
   290   consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
   291     using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
   292   then show ?case
   293   proof cases
   294     case (1 x)
   295     with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
   296     with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
   297       by (auto intro: mult_dvd_mono)
   298     thus ?thesis by blast
   299   next
   300     case (2 y)
   301     with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
   302     with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
   303       by (auto intro: mult_dvd_mono)
   304     with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
   305       by force
   306   qed
   307 qed
   308 
   309 lemma prime_elem_power_dvd_cases:
   310   assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p"
   311   shows "p ^ a dvd m \<or> p ^ b dvd n"
   312 proof -
   313   from assms obtain r s
   314     where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n"
   315     by (blast dest: prime_elem_power_dvd_prod)
   316   moreover with assms have
   317     "a \<le> r \<or> b \<le> s" by arith
   318   ultimately show ?thesis by (auto intro: power_le_dvd)
   319 qed
   320 
   321 lemma prime_elem_not_unit' [simp]:
   322   "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
   323   unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
   324 
   325 lemma prime_elem_dvd_power_iff:
   326   assumes "prime_elem p"
   327   shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   328   using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
   329 
   330 lemma prime_power_dvd_multD:
   331   assumes "prime_elem p"
   332   assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   333   shows "p ^ n dvd b"
   334   using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close>
   335 proof (induct n arbitrary: b)
   336   case 0 then show ?case by simp
   337 next
   338   case (Suc n) show ?case
   339   proof (cases "n = 0")
   340     case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   341       by (simp add: prime_elem_dvd_mult_iff)
   342   next
   343     case False then have "n > 0" by simp
   344     from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto
   345     from Suc.prems have *: "p * p ^ n dvd a * b"
   346       by simp
   347     then have "p dvd a * b"
   348       by (rule dvd_mult_left)
   349     with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   350       by (simp add: prime_elem_dvd_mult_iff)
   351     moreover define c where "c = b div p"
   352     ultimately have b: "b = p * c" by simp
   353     with * have "p * p ^ n dvd p * (a * c)"
   354       by (simp add: ac_simps)
   355     with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c"
   356       by simp
   357     with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c"
   358       by blast
   359     with \<open>p \<noteq> 0\<close> show ?thesis
   360       by (simp add: b)
   361   qed
   362 qed
   363 
   364 end
   365 
   366 
   367 subsection \<open>Generalized primes: normalized prime elements\<close>
   368 
   369 context normalization_semidom
   370 begin
   371 
   372 lemma irreducible_normalized_divisors:
   373   assumes "irreducible x" "y dvd x" "normalize y = y"
   374   shows   "y = 1 \<or> y = normalize x"
   375 proof -
   376   from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
   377   thus ?thesis
   378   proof (elim disjE)
   379     assume "is_unit y"
   380     hence "normalize y = 1" by (simp add: is_unit_normalize)
   381     with assms show ?thesis by simp
   382   next
   383     assume "x dvd y"
   384     with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
   385     with assms show ?thesis by simp
   386   qed
   387 qed
   388 
   389 lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
   390   using irreducible_mult_unit_left[of "1 div unit_factor x" x]
   391   by (cases "x = 0") (simp_all add: unit_div_commute)
   392 
   393 lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
   394   using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
   395   by (cases "x = 0") (simp_all add: unit_div_commute)
   396 
   397 lemma prime_elem_associated:
   398   assumes "prime_elem p" and "prime_elem q" and "q dvd p"
   399   shows "normalize q = normalize p"
   400 using \<open>q dvd p\<close> proof (rule associatedI)
   401   from \<open>prime_elem q\<close> have "\<not> is_unit q"
   402     by (auto simp add: prime_elem_not_unit)
   403   with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
   404     by (blast intro: prime_elemD2)
   405 qed
   406 
   407 definition prime :: "'a \<Rightarrow> bool" where
   408   "prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p"
   409 
   410 lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def)
   411 
   412 lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x"
   413   using prime_elem_not_unit[of x] by (auto simp add: prime_def)
   414 
   415 lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit)
   416 
   417 lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x"
   418   by (simp add: prime_def)
   419 
   420 lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p"
   421   by (simp add: prime_def)
   422 
   423 lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p"
   424   by (simp add: prime_def)
   425 
   426 lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p"
   427   by (auto simp add: prime_def)
   428 
   429 lemma prime_power_iff:
   430   "prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1"
   431   by (auto simp: prime_def prime_elem_power_iff)
   432 
   433 lemma prime_imp_nonzero [simp]:
   434   "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0"
   435   unfolding ASSUMPTION_def prime_def by auto
   436 
   437 lemma prime_imp_not_one [simp]:
   438   "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1"
   439   unfolding ASSUMPTION_def by auto
   440 
   441 lemma prime_not_unit' [simp]:
   442   "ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x"
   443   unfolding ASSUMPTION_def prime_def by auto
   444 
   445 lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x"
   446   unfolding ASSUMPTION_def prime_def by simp
   447 
   448 lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1"
   449   using unit_factor_normalize[of x] unfolding prime_def by auto
   450 
   451 lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1"
   452   unfolding ASSUMPTION_def by (rule unit_factor_prime)
   453 
   454 lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x"
   455   by (simp add: prime_def ASSUMPTION_def)
   456 
   457 lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
   458   by (intro prime_elem_dvd_multD) simp_all
   459 
   460 lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   461   by (auto dest: prime_dvd_multD)
   462 
   463 lemma prime_dvd_power:
   464   "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   465   by (auto dest!: prime_elem_dvd_power simp: prime_def)
   466 
   467 lemma prime_dvd_power_iff:
   468   "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
   469   by (subst prime_elem_dvd_power_iff) simp_all
   470 
   471 lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
   472   by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
   473 
   474 lemma prime_dvd_prod_iff: "finite A \<Longrightarrow> prime p \<Longrightarrow> p dvd prod f A \<longleftrightarrow> (\<exists>x\<in>A. p dvd f x)"
   475   by (auto simp: prime_dvd_prod_mset_iff prod_unfold_prod_mset)
   476 
   477 lemma primes_dvd_imp_eq:
   478   assumes "prime p" "prime q" "p dvd q"
   479   shows   "p = q"
   480 proof -
   481   from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
   482   from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
   483   with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
   484   with assms show "p = q" by simp
   485 qed
   486 
   487 lemma prime_dvd_prod_mset_primes_iff:
   488   assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
   489   shows   "p dvd prod_mset A \<longleftrightarrow> p \<in># A"
   490 proof -
   491   from assms(1) have "p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_prod_mset_iff)
   492   also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
   493   finally show ?thesis .
   494 qed
   495 
   496 lemma prod_mset_primes_dvd_imp_subset:
   497   assumes "prod_mset A dvd prod_mset B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
   498   shows   "A \<subseteq># B"
   499 using assms
   500 proof (induction A arbitrary: B)
   501   case empty
   502   thus ?case by simp
   503 next
   504   case (add p A B)
   505   hence p: "prime p" by simp
   506   define B' where "B' = B - {#p#}"
   507   from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left)
   508   with add.prems have "p \<in># B"
   509     by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all
   510   hence B: "B = B' + {#p#}" by (simp add: B'_def)
   511   from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   512   thus ?case by (simp add: B)
   513 qed
   514 
   515 lemma normalize_prod_mset_primes:
   516   "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
   517 proof (induction A)
   518   case (add p A)
   519   hence "prime p" by simp
   520   hence "normalize p = p" by simp
   521   with add show ?case by (simp add: normalize_mult)
   522 qed simp_all
   523 
   524 lemma prod_mset_dvd_prod_mset_primes_iff:
   525   assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
   526   shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
   527   using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)
   528 
   529 lemma is_unit_prod_mset_primes_iff:
   530   assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
   531   shows   "is_unit (prod_mset A) \<longleftrightarrow> A = {#}"
   532   by (auto simp add: is_unit_prod_mset_iff)
   533     (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff)
   534 
   535 lemma prod_mset_primes_irreducible_imp_prime:
   536   assumes irred: "irreducible (prod_mset A)"
   537   assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   538   assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   539   assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
   540   assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C"
   541   shows   "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C"
   542 proof -
   543   from dvd have "prod_mset A dvd prod_mset (B + C)"
   544     by simp
   545   with A B C have subset: "A \<subseteq># B + C"
   546     by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto
   547   define A1 and A2 where "A1 = A \<inter># B" and "A2 = A - A1"
   548   have "A = A1 + A2" unfolding A1_def A2_def
   549     by (rule sym, intro subset_mset.add_diff_inverse) simp_all
   550   from subset have "A1 \<subseteq># B" "A2 \<subseteq># C"
   551     by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute)
   552   from \<open>A = A1 + A2\<close> have "prod_mset A = prod_mset A1 * prod_mset A2" by simp
   553   from irred and this have "is_unit (prod_mset A1) \<or> is_unit (prod_mset A2)"
   554     by (rule irreducibleD)
   555   with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def
   556     by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD)
   557   with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis
   558     by (auto intro: prod_mset_subset_imp_dvd)
   559 qed
   560 
   561 lemma prod_mset_primes_finite_divisor_powers:
   562   assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   563   assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   564   assumes "A \<noteq> {#}"
   565   shows   "finite {n. prod_mset A ^ n dvd prod_mset B}"
   566 proof -
   567   from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast
   568   define m where "m = count B x"
   569   have "{n. prod_mset A ^ n dvd prod_mset B} \<subseteq> {..m}"
   570   proof safe
   571     fix n assume dvd: "prod_mset A ^ n dvd prod_mset B"
   572     from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset)
   573     also note dvd
   574     also have "x ^ n = prod_mset (replicate_mset n x)" by simp
   575     finally have "replicate_mset n x \<subseteq># B"
   576       by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
   577     thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def)
   578   qed
   579   moreover have "finite {..m}" by simp
   580   ultimately show ?thesis by (rule finite_subset)
   581 qed
   582 
   583 end
   584 
   585 
   586 subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
   587 
   588 context semiring_gcd
   589 begin
   590 
   591 lemma irreducible_imp_prime_elem_gcd:
   592   assumes "irreducible x"
   593   shows   "prime_elem x"
   594 proof (rule prime_elemI)
   595   fix a b assume "x dvd a * b"
   596   from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
   597   from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
   598   with yz show "x dvd a \<or> x dvd b"
   599     by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
   600 qed (insert assms, auto simp: irreducible_not_unit)
   601 
   602 lemma prime_elem_imp_coprime:
   603   assumes "prime_elem p" "\<not>p dvd n"
   604   shows   "coprime p n"
   605 proof (rule coprimeI)
   606   fix d assume "d dvd p" "d dvd n"
   607   show "is_unit d"
   608   proof (rule ccontr)
   609     assume "\<not>is_unit d"
   610     from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
   611       by (rule prime_elemD2)
   612     from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
   613     with \<open>\<not>p dvd n\<close> show False by contradiction
   614   qed
   615 qed
   616 
   617 lemma prime_imp_coprime:
   618   assumes "prime p" "\<not>p dvd n"
   619   shows   "coprime p n"
   620   using assms by (simp add: prime_elem_imp_coprime)
   621 
   622 lemma prime_elem_imp_power_coprime:
   623   "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   624   by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
   625 
   626 lemma prime_imp_power_coprime:
   627   "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   628   by (simp add: prime_elem_imp_power_coprime)
   629 
   630 lemma prime_elem_divprod_pow:
   631   assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   632   shows   "p^n dvd a \<or> p^n dvd b"
   633   using assms
   634 proof -
   635   from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
   636     by (auto simp: coprime prime_elem_def)
   637   with p have "coprime (p^n) a \<or> coprime (p^n) b"
   638     by (auto intro: prime_elem_imp_coprime coprime_exp_left)
   639   with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
   640 qed
   641 
   642 lemma primes_coprime:
   643   "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   644   using prime_imp_coprime primes_dvd_imp_eq by blast
   645 
   646 end
   647 
   648 
   649 subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close>
   650 
   651 class factorial_semiring = normalization_semidom +
   652   assumes prime_factorization_exists:
   653     "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   654 
   655 text \<open>Alternative characterization\<close>
   656 
   657 lemma (in normalization_semidom) factorial_semiring_altI_aux:
   658   assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   659   assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
   660   assumes "x \<noteq> 0"
   661   shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   662 using \<open>x \<noteq> 0\<close>
   663 proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
   664   case (less a)
   665   let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
   666   show ?case
   667   proof (cases "is_unit a")
   668     case True
   669     thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
   670   next
   671     case False
   672     show ?thesis
   673     proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
   674       case False
   675       with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
   676       hence "prime_elem a" by (rule irreducible_imp_prime_elem)
   677       thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
   678     next
   679       case True
   680       then guess b by (elim exE conjE) note b = this
   681 
   682       from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
   683       moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
   684       hence "?fctrs b \<noteq> ?fctrs a" by blast
   685       ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
   686       with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
   687         by (rule psubset_card_mono)
   688       moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
   689       ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
   690         by (intro less) auto
   691       then guess A .. note A = this
   692 
   693       define c where "c = a div b"
   694       from b have c: "a = b * c" by (simp add: c_def)
   695       from less.prems c have "c \<noteq> 0" by auto
   696       from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
   697       moreover have "normalize a \<notin> ?fctrs c"
   698       proof safe
   699         assume "normalize a dvd c"
   700         hence "b * c dvd 1 * c" by (simp add: c)
   701         hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
   702         with b show False by simp
   703       qed
   704       with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
   705       ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
   706       with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
   707         by (rule psubset_card_mono)
   708       with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
   709         by (intro less) auto
   710       then guess B .. note B = this
   711 
   712       from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
   713     qed
   714   qed
   715 qed
   716 
   717 lemma factorial_semiring_altI:
   718   assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   719   assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
   720   shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
   721   by intro_classes (rule factorial_semiring_altI_aux[OF assms])
   722 
   723 text \<open>Properties\<close>
   724 
   725 context factorial_semiring
   726 begin
   727 
   728 lemma prime_factorization_exists':
   729   assumes "x \<noteq> 0"
   730   obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x"
   731 proof -
   732   from prime_factorization_exists[OF assms] obtain A
   733     where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast
   734   define A' where "A' = image_mset normalize A"
   735   have "prod_mset A' = normalize (prod_mset A)"
   736     by (simp add: A'_def normalize_prod_mset)
   737   also note A(2)
   738   finally have "prod_mset A' = normalize x" by simp
   739   moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
   740   ultimately show ?thesis by (intro that[of A']) blast
   741 qed
   742 
   743 lemma irreducible_imp_prime_elem:
   744   assumes "irreducible x"
   745   shows   "prime_elem x"
   746 proof (rule prime_elemI)
   747   fix a b assume dvd: "x dvd a * b"
   748   from assms have "x \<noteq> 0" by auto
   749   show "x dvd a \<or> x dvd b"
   750   proof (cases "a = 0 \<or> b = 0")
   751     case False
   752     hence "a \<noteq> 0" "b \<noteq> 0" by blast+
   753     note nz = \<open>x \<noteq> 0\<close> this
   754     from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
   755     from assms ABC have "irreducible (prod_mset A)" by simp
   756     from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
   757       show ?thesis by (simp add: normalize_mult [symmetric])
   758   qed auto
   759 qed (insert assms, simp_all add: irreducible_def)
   760 
   761 lemma finite_divisor_powers:
   762   assumes "y \<noteq> 0" "\<not>is_unit x"
   763   shows   "finite {n. x ^ n dvd y}"
   764 proof (cases "x = 0")
   765   case True
   766   with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left)
   767   thus ?thesis by simp
   768 next
   769   case False
   770   note nz = this \<open>y \<noteq> 0\<close>
   771   from nz[THEN prime_factorization_exists'] guess A B . note AB = this
   772   from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
   773   from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
   774     show ?thesis by (simp add: normalize_power [symmetric])
   775 qed
   776 
   777 lemma finite_prime_divisors:
   778   assumes "x \<noteq> 0"
   779   shows   "finite {p. prime p \<and> p dvd x}"
   780 proof -
   781   from prime_factorization_exists'[OF assms] guess A . note A = this
   782   have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
   783   proof safe
   784     fix p assume p: "prime p" and dvd: "p dvd x"
   785     from dvd have "p dvd normalize x" by simp
   786     also from A have "normalize x = prod_mset A" by simp
   787     finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff)
   788   qed
   789   moreover have "finite (set_mset A)" by simp
   790   ultimately show ?thesis by (rule finite_subset)
   791 qed
   792 
   793 lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
   794   by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
   795 
   796 lemma prime_divisor_exists:
   797   assumes "a \<noteq> 0" "\<not>is_unit a"
   798   shows   "\<exists>b. b dvd a \<and> prime b"
   799 proof -
   800   from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   801   moreover from A and assms have "A \<noteq> {#}" by auto
   802   then obtain x where "x \<in># A" by blast
   803   with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset)
   804   with A have "x dvd a" by simp
   805   with * show ?thesis by blast
   806 qed
   807 
   808 lemma prime_divisors_induct [case_names zero unit factor]:
   809   assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
   810   shows   "P x"
   811 proof (cases "x = 0")
   812   case False
   813   from prime_factorization_exists'[OF this] guess A . note A = this
   814   from A(1) have "P (unit_factor x * prod_mset A)"
   815   proof (induction A)
   816     case (add p A)
   817     from add.prems have "prime p" by simp
   818     moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all
   819     ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3))
   820     thus ?case by (simp add: mult_ac)
   821   qed (simp_all add: assms False)
   822   with A show ?thesis by simp
   823 qed (simp_all add: assms(1))
   824 
   825 lemma no_prime_divisors_imp_unit:
   826   assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b"
   827   shows "is_unit a"
   828 proof (rule ccontr)
   829   assume "\<not>is_unit a"
   830   from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
   831   with assms(2)[of b] show False by (simp add: prime_def)
   832 qed
   833 
   834 lemma prime_divisorE:
   835   assumes "a \<noteq> 0" and "\<not> is_unit a"
   836   obtains p where "prime p" and "p dvd a"
   837   using assms no_prime_divisors_imp_unit unfolding prime_def by blast
   838 
   839 definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
   840   "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
   841 
   842 lemma multiplicity_dvd: "p ^ multiplicity p x dvd x"
   843 proof (cases "finite {n. p ^ n dvd x}")
   844   case True
   845   hence "multiplicity p x = Max {n. p ^ n dvd x}"
   846     by (simp add: multiplicity_def)
   847   also have "\<dots> \<in> {n. p ^ n dvd x}"
   848     by (rule Max_in) (auto intro!: True exI[of _ "0::nat"])
   849   finally show ?thesis by simp
   850 qed (simp add: multiplicity_def)
   851 
   852 lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x"
   853   by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])
   854 
   855 context
   856   fixes x p :: 'a
   857   assumes xp: "x \<noteq> 0" "\<not>is_unit p"
   858 begin
   859 
   860 lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}"
   861   using finite_divisor_powers[OF xp] by (simp add: multiplicity_def)
   862 
   863 lemma multiplicity_geI:
   864   assumes "p ^ n dvd x"
   865   shows   "multiplicity p x \<ge> n"
   866 proof -
   867   from assms have "n \<le> Max {n. p ^ n dvd x}"
   868     by (intro Max_ge finite_divisor_powers xp) simp_all
   869   thus ?thesis by (subst multiplicity_eq_Max)
   870 qed
   871 
   872 lemma multiplicity_lessI:
   873   assumes "\<not>p ^ n dvd x"
   874   shows   "multiplicity p x < n"
   875 proof (rule ccontr)
   876   assume "\<not>(n > multiplicity p x)"
   877   hence "p ^ n dvd x" by (intro multiplicity_dvd') simp
   878   with assms show False by contradiction
   879 qed
   880 
   881 lemma power_dvd_iff_le_multiplicity:
   882   "p ^ n dvd x \<longleftrightarrow> n \<le> multiplicity p x"
   883   using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
   884 
   885 lemma multiplicity_eq_zero_iff:
   886   shows   "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   887   using power_dvd_iff_le_multiplicity[of 1] by auto
   888 
   889 lemma multiplicity_gt_zero_iff:
   890   shows   "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   891   using power_dvd_iff_le_multiplicity[of 1] by auto
   892 
   893 lemma multiplicity_decompose:
   894   "\<not>p dvd (x div p ^ multiplicity p x)"
   895 proof
   896   assume *: "p dvd x div p ^ multiplicity p x"
   897   have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)"
   898     using multiplicity_dvd[of p x] by simp
   899   also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp
   900   also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x =
   901                x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)"
   902     by (simp add: mult_assoc)
   903   also have "p ^ Suc (multiplicity p x) dvd \<dots>" by (rule dvd_triv_right)
   904   finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp
   905 qed
   906 
   907 lemma multiplicity_decompose':
   908   obtains y where "x = p ^ multiplicity p x * y" "\<not>p dvd y"
   909   using that[of "x div p ^ multiplicity p x"]
   910   by (simp add: multiplicity_decompose multiplicity_dvd)
   911 
   912 end
   913 
   914 lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
   915   by (simp add: multiplicity_def)
   916 
   917 lemma prime_elem_multiplicity_eq_zero_iff:
   918   "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   919   by (rule multiplicity_eq_zero_iff) simp_all
   920 
   921 lemma prime_multiplicity_other:
   922   assumes "prime p" "prime q" "p \<noteq> q"
   923   shows   "multiplicity p q = 0"
   924   using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
   925 
   926 lemma prime_multiplicity_gt_zero_iff:
   927   "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   928   by (rule multiplicity_gt_zero_iff) simp_all
   929 
   930 lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
   931   by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
   932 
   933 lemma multiplicity_unit_right:
   934   assumes "is_unit x"
   935   shows   "multiplicity p x = 0"
   936 proof (cases "is_unit p \<or> x = 0")
   937   case False
   938   with multiplicity_lessI[of x p 1] this assms
   939     show ?thesis by (auto dest: dvd_unit_imp_unit)
   940 qed (auto simp: multiplicity_unit_left)
   941 
   942 lemma multiplicity_one [simp]: "multiplicity p 1 = 0"
   943   by (rule multiplicity_unit_right) simp_all
   944 
   945 lemma multiplicity_eqI:
   946   assumes "p ^ n dvd x" "\<not>p ^ Suc n dvd x"
   947   shows   "multiplicity p x = n"
   948 proof -
   949   consider "x = 0" | "is_unit p" | "x \<noteq> 0" "\<not>is_unit p" by blast
   950   thus ?thesis
   951   proof cases
   952     assume xp: "x \<noteq> 0" "\<not>is_unit p"
   953     from xp assms(1) have "multiplicity p x \<ge> n" by (intro multiplicity_geI)
   954     moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI)
   955     ultimately show ?thesis by simp
   956   next
   957     assume "is_unit p"
   958     hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc)
   959     hence "p ^ Suc n dvd x" by (rule unit_imp_dvd)
   960     with \<open>\<not>p ^ Suc n dvd x\<close> show ?thesis by contradiction
   961   qed (insert assms, simp_all)
   962 qed
   963 
   964 
   965 context
   966   fixes x p :: 'a
   967   assumes xp: "x \<noteq> 0" "\<not>is_unit p"
   968 begin
   969 
   970 lemma multiplicity_times_same:
   971   assumes "p \<noteq> 0"
   972   shows   "multiplicity p (p * x) = Suc (multiplicity p x)"
   973 proof (rule multiplicity_eqI)
   974   show "p ^ Suc (multiplicity p x) dvd p * x"
   975     by (auto intro!: mult_dvd_mono multiplicity_dvd)
   976   from xp assms show "\<not> p ^ Suc (Suc (multiplicity p x)) dvd p * x"
   977     using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp
   978 qed
   979 
   980 end
   981 
   982 lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \<or> is_unit p then 0 else n)"
   983 proof -
   984   consider "p = 0" | "is_unit p" |"p \<noteq> 0" "\<not>is_unit p" by blast
   985   thus ?thesis
   986   proof cases
   987     assume "p \<noteq> 0" "\<not>is_unit p"
   988     thus ?thesis by (induction n) (simp_all add: multiplicity_times_same)
   989   qed (simp_all add: power_0_left multiplicity_unit_left)
   990 qed
   991 
   992 lemma multiplicity_same_power:
   993   "p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
   994   by (simp add: multiplicity_same_power')
   995 
   996 lemma multiplicity_prime_elem_times_other:
   997   assumes "prime_elem p" "\<not>p dvd q"
   998   shows   "multiplicity p (q * x) = multiplicity p x"
   999 proof (cases "x = 0")
  1000   case False
  1001   show ?thesis
  1002   proof (rule multiplicity_eqI)
  1003     have "1 * p ^ multiplicity p x dvd q * x"
  1004       by (intro mult_dvd_mono multiplicity_dvd) simp_all
  1005     thus "p ^ multiplicity p x dvd q * x" by simp
  1006   next
  1007     define n where "n = multiplicity p x"
  1008     from assms have "\<not>is_unit p" by simp
  1009     from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
  1010     from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
  1011     also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
  1012     also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
  1013     also from assms y have "\<dots> \<longleftrightarrow> False" by simp
  1014     finally show "\<not>(p ^ Suc n dvd q * x)" by blast
  1015   qed
  1016 qed simp_all
  1017 
  1018 lemma multiplicity_self:
  1019   assumes "p \<noteq> 0" "\<not>is_unit p"
  1020   shows   "multiplicity p p = 1"
  1021 proof -
  1022   from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
  1023     by (simp add: multiplicity_eq_Max)
  1024   also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
  1025     using dvd_power_iff[of p n 1] by auto
  1026   hence "{n. p ^ n dvd p} = {..1}" by auto
  1027   also have "\<dots> = {0,1}" by auto
  1028   finally show ?thesis by simp
  1029 qed
  1030 
  1031 lemma multiplicity_times_unit_left:
  1032   assumes "is_unit c"
  1033   shows   "multiplicity (c * p) x = multiplicity p x"
  1034 proof -
  1035   from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
  1036     by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
  1037   thus ?thesis by (simp add: multiplicity_def)
  1038 qed
  1039 
  1040 lemma multiplicity_times_unit_right:
  1041   assumes "is_unit c"
  1042   shows   "multiplicity p (c * x) = multiplicity p x"
  1043 proof -
  1044   from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
  1045     by (subst mult.commute) (simp add: dvd_mult_unit_iff)
  1046   thus ?thesis by (simp add: multiplicity_def)
  1047 qed
  1048 
  1049 lemma multiplicity_normalize_left [simp]:
  1050   "multiplicity (normalize p) x = multiplicity p x"
  1051 proof (cases "p = 0")
  1052   case [simp]: False
  1053   have "normalize p = (1 div unit_factor p) * p"
  1054     by (simp add: unit_div_commute is_unit_unit_factor)
  1055   also have "multiplicity \<dots> x = multiplicity p x"
  1056     by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
  1057   finally show ?thesis .
  1058 qed simp_all
  1059 
  1060 lemma multiplicity_normalize_right [simp]:
  1061   "multiplicity p (normalize x) = multiplicity p x"
  1062 proof (cases "x = 0")
  1063   case [simp]: False
  1064   have "normalize x = (1 div unit_factor x) * x"
  1065     by (simp add: unit_div_commute is_unit_unit_factor)
  1066   also have "multiplicity p \<dots> = multiplicity p x"
  1067     by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
  1068   finally show ?thesis .
  1069 qed simp_all
  1070 
  1071 lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
  1072   by (rule multiplicity_self) auto
  1073 
  1074 lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
  1075   by (subst multiplicity_same_power') auto
  1076 
  1077 lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
  1078   "\<lambda>x p. if prime p then multiplicity p x else 0"
  1079   unfolding multiset_def
  1080 proof clarify
  1081   fix x :: 'a
  1082   show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
  1083   proof (cases "x = 0")
  1084     case False
  1085     from False have "?A \<subseteq> {p. prime p \<and> p dvd x}"
  1086       by (auto simp: multiplicity_gt_zero_iff)
  1087     moreover from False have "finite {p. prime p \<and> p dvd x}"
  1088       by (rule finite_prime_divisors)
  1089     ultimately show ?thesis by (rule finite_subset)
  1090   qed simp_all
  1091 qed
  1092 
  1093 abbreviation prime_factors :: "'a \<Rightarrow> 'a set" where
  1094   "prime_factors a \<equiv> set_mset (prime_factorization a)"
  1095 
  1096 lemma count_prime_factorization_nonprime:
  1097   "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
  1098   by transfer simp
  1099 
  1100 lemma count_prime_factorization_prime:
  1101   "prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
  1102   by transfer simp
  1103 
  1104 lemma count_prime_factorization:
  1105   "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
  1106   by transfer simp
  1107 
  1108 lemma dvd_imp_multiplicity_le:
  1109   assumes "a dvd b" "b \<noteq> 0"
  1110   shows   "multiplicity p a \<le> multiplicity p b"
  1111 proof (cases "is_unit p")
  1112   case False
  1113   with assms show ?thesis
  1114     by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
  1115 qed (insert assms, auto simp: multiplicity_unit_left)
  1116 
  1117 lemma prime_power_inj:
  1118   assumes "prime a" "a ^ m = a ^ n"
  1119   shows   "m = n"
  1120 proof -
  1121   have "multiplicity a (a ^ m) = multiplicity a (a ^ n)" by (simp only: assms)
  1122   thus ?thesis using assms by (subst (asm) (1 2) multiplicity_prime_power) simp_all
  1123 qed
  1124 
  1125 lemma prime_power_inj':
  1126   assumes "prime p" "prime q"
  1127   assumes "p ^ m = q ^ n" "m > 0" "n > 0"
  1128   shows   "p = q" "m = n"
  1129 proof -
  1130   from assms have "p ^ 1 dvd p ^ m" by (intro le_imp_power_dvd) simp
  1131   also have "p ^ m = q ^ n" by fact
  1132   finally have "p dvd q ^ n" by simp
  1133   with assms have "p dvd q" using prime_dvd_power[of p q] by simp
  1134   with assms show "p = q" by (simp add: primes_dvd_imp_eq)
  1135   with assms show "m = n" by (simp add: prime_power_inj)
  1136 qed
  1137 
  1138 lemma prime_power_eq_one_iff [simp]: "prime p \<Longrightarrow> p ^ n = 1 \<longleftrightarrow> n = 0"
  1139   using prime_power_inj[of p n 0] by auto
  1140 
  1141 lemma one_eq_prime_power_iff [simp]: "prime p \<Longrightarrow> 1 = p ^ n \<longleftrightarrow> n = 0"
  1142   using prime_power_inj[of p 0 n] by auto
  1143 
  1144 lemma prime_power_inj'':
  1145   assumes "prime p" "prime q"
  1146   shows   "p ^ m = q ^ n \<longleftrightarrow> (m = 0 \<and> n = 0) \<or> (p = q \<and> m = n)"
  1147   using assms 
  1148   by (cases "m = 0"; cases "n = 0")
  1149      (auto dest: prime_power_inj'[OF assms])
  1150 
  1151 lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
  1152   by (simp add: multiset_eq_iff count_prime_factorization)
  1153 
  1154 lemma prime_factorization_empty_iff:
  1155   "prime_factorization x = {#} \<longleftrightarrow> x = 0 \<or> is_unit x"
  1156 proof
  1157   assume *: "prime_factorization x = {#}"
  1158   {
  1159     assume x: "x \<noteq> 0" "\<not>is_unit x"
  1160     {
  1161       fix p assume p: "prime p"
  1162       have "count (prime_factorization x) p = 0" by (simp add: *)
  1163       also from p have "count (prime_factorization x) p = multiplicity p x"
  1164         by (rule count_prime_factorization_prime)
  1165       also from x p have "\<dots> = 0 \<longleftrightarrow> \<not>p dvd x" by (simp add: multiplicity_eq_zero_iff)
  1166       finally have "\<not>p dvd x" .
  1167     }
  1168     with prime_divisor_exists[OF x] have False by blast
  1169   }
  1170   thus "x = 0 \<or> is_unit x" by blast
  1171 next
  1172   assume "x = 0 \<or> is_unit x"
  1173   thus "prime_factorization x = {#}"
  1174   proof
  1175     assume x: "is_unit x"
  1176     {
  1177       fix p assume p: "prime p"
  1178       from p x have "multiplicity p x = 0"
  1179         by (subst multiplicity_eq_zero_iff)
  1180            (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
  1181     }
  1182     thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization)
  1183   qed simp_all
  1184 qed
  1185 
  1186 lemma prime_factorization_unit:
  1187   assumes "is_unit x"
  1188   shows   "prime_factorization x = {#}"
  1189 proof (rule multiset_eqI)
  1190   fix p :: 'a
  1191   show "count (prime_factorization x) p = count {#} p"
  1192   proof (cases "prime p")
  1193     case True
  1194     with assms have "multiplicity p x = 0"
  1195       by (subst multiplicity_eq_zero_iff)
  1196          (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
  1197     with True show ?thesis by (simp add: count_prime_factorization_prime)
  1198   qed (simp_all add: count_prime_factorization_nonprime)
  1199 qed
  1200 
  1201 lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}"
  1202   by (simp add: prime_factorization_unit)
  1203 
  1204 lemma prime_factorization_times_prime:
  1205   assumes "x \<noteq> 0" "prime p"
  1206   shows   "prime_factorization (p * x) = {#p#} + prime_factorization x"
  1207 proof (rule multiset_eqI)
  1208   fix q :: 'a
  1209   consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast
  1210   thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
  1211   proof cases
  1212     assume q: "prime q" "p \<noteq> q"
  1213     with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
  1214     with q assms show ?thesis
  1215       by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
  1216   qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
  1217 qed
  1218 
  1219 lemma prod_mset_prime_factorization:
  1220   assumes "x \<noteq> 0"
  1221   shows   "prod_mset (prime_factorization x) = normalize x"
  1222   using assms
  1223   by (induction x rule: prime_divisors_induct)
  1224      (simp_all add: prime_factorization_unit prime_factorization_times_prime
  1225                     is_unit_normalize normalize_mult)
  1226 
  1227 lemma in_prime_factors_iff:
  1228   "p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  1229 proof -
  1230   have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
  1231   also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  1232    by (subst count_prime_factorization, cases "x = 0")
  1233       (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
  1234   finally show ?thesis .
  1235 qed
  1236 
  1237 lemma in_prime_factors_imp_prime [intro]:
  1238   "p \<in> prime_factors x \<Longrightarrow> prime p"
  1239   by (simp add: in_prime_factors_iff)
  1240 
  1241 lemma in_prime_factors_imp_dvd [dest]:
  1242   "p \<in> prime_factors x \<Longrightarrow> p dvd x"
  1243   by (simp add: in_prime_factors_iff)
  1244 
  1245 lemma prime_factorsI:
  1246   "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
  1247   by (auto simp: in_prime_factors_iff)
  1248 
  1249 lemma prime_factors_dvd:
  1250   "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
  1251   by (auto intro: prime_factorsI)
  1252 
  1253 lemma prime_factors_multiplicity:
  1254   "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
  1255   by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff)
  1256 
  1257 lemma prime_factorization_prime:
  1258   assumes "prime p"
  1259   shows   "prime_factorization p = {#p#}"
  1260 proof (rule multiset_eqI)
  1261   fix q :: 'a
  1262   consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast
  1263   thus "count (prime_factorization p) q = count {#p#} q"
  1264     by cases (insert assms, auto dest: primes_dvd_imp_eq
  1265                 simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
  1266 qed
  1267 
  1268 lemma prime_factorization_prod_mset_primes:
  1269   assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
  1270   shows   "prime_factorization (prod_mset A) = A"
  1271   using assms
  1272 proof (induction A)
  1273   case (add p A)
  1274   from add.prems[of 0] have "0 \<notin># A" by auto
  1275   hence "prod_mset A \<noteq> 0" by auto
  1276   with add show ?case
  1277     by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
  1278 qed simp_all
  1279 
  1280 lemma prime_factorization_cong:
  1281   "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
  1282   by (simp add: multiset_eq_iff count_prime_factorization
  1283                 multiplicity_normalize_right [of _ x, symmetric]
  1284                 multiplicity_normalize_right [of _ y, symmetric]
  1285            del:  multiplicity_normalize_right)
  1286 
  1287 lemma prime_factorization_unique:
  1288   assumes "x \<noteq> 0" "y \<noteq> 0"
  1289   shows   "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y"
  1290 proof
  1291   assume "prime_factorization x = prime_factorization y"
  1292   hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
  1293   with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
  1294 qed (rule prime_factorization_cong)
  1295 
  1296 lemma prime_factorization_mult:
  1297   assumes "x \<noteq> 0" "y \<noteq> 0"
  1298   shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
  1299 proof -
  1300   have "prime_factorization (prod_mset (prime_factorization (x * y))) =
  1301           prime_factorization (prod_mset (prime_factorization x + prime_factorization y))"
  1302     by (simp add: prod_mset_prime_factorization assms normalize_mult)
  1303   also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
  1304                prime_factorization (x * y)"
  1305     by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime)
  1306   also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
  1307                prime_factorization x + prime_factorization y"
  1308     by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime)
  1309   finally show ?thesis .
  1310 qed
  1311 
  1312 lemma prime_factorization_prod:
  1313   assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
  1314   shows   "prime_factorization (prod f A) = (\<Sum>n\<in>A. prime_factorization (f n))"
  1315   using assms by (induction A rule: finite_induct)
  1316                  (auto simp: Sup_multiset_empty prime_factorization_mult)
  1317 
  1318 lemma prime_elem_multiplicity_mult_distrib:
  1319   assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
  1320   shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
  1321 proof -
  1322   have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
  1323     by (subst count_prime_factorization_prime) (simp_all add: assms)
  1324   also from assms
  1325     have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
  1326       by (intro prime_factorization_mult)
  1327   also have "count \<dots> (normalize p) =
  1328     count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
  1329     by simp
  1330   also have "\<dots> = multiplicity p x + multiplicity p y"
  1331     by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
  1332   finally show ?thesis .
  1333 qed
  1334 
  1335 lemma prime_elem_multiplicity_prod_mset_distrib:
  1336   assumes "prime_elem p" "0 \<notin># A"
  1337   shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
  1338   using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
  1339 
  1340 lemma prime_elem_multiplicity_power_distrib:
  1341   assumes "prime_elem p" "x \<noteq> 0"
  1342   shows   "multiplicity p (x ^ n) = n * multiplicity p x"
  1343   using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
  1344   by simp
  1345 
  1346 lemma prime_elem_multiplicity_prod_distrib:
  1347   assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
  1348   shows   "multiplicity p (prod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
  1349 proof -
  1350   have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
  1351     using assms by (subst prod_unfold_prod_mset)
  1352                    (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset
  1353                       multiset.map_comp o_def)
  1354   also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
  1355     by (induction A rule: finite_induct) simp_all
  1356   finally show ?thesis .
  1357 qed
  1358 
  1359 lemma multiplicity_distinct_prime_power:
  1360   "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
  1361   by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
  1362 
  1363 lemma prime_factorization_prime_power:
  1364   "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
  1365   by (induction n)
  1366      (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
  1367 
  1368 lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
  1369   by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
  1370 
  1371 lemma prime_factorization_subset_iff_dvd:
  1372   assumes [simp]: "x \<noteq> 0" "y \<noteq> 0"
  1373   shows   "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y"
  1374 proof -
  1375   have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
  1376     by (simp add: prod_mset_prime_factorization)
  1377   also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
  1378     by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd)
  1379   finally show ?thesis ..
  1380 qed
  1381 
  1382 lemma prime_factorization_subset_imp_dvd:
  1383   "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
  1384   by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
  1385 
  1386 lemma prime_factorization_divide:
  1387   assumes "b dvd a"
  1388   shows   "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
  1389 proof (cases "a = 0")
  1390   case [simp]: False
  1391   from assms have [simp]: "b \<noteq> 0" by auto
  1392   have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b"
  1393     by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE)
  1394   with assms show ?thesis by simp
  1395 qed simp_all
  1396 
  1397 lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x"
  1398   by (auto dest: in_prime_factors_imp_prime)
  1399 
  1400 lemma prime_prime_factors:
  1401   "prime p \<Longrightarrow> prime_factors p = {p}"
  1402   by (drule prime_factorization_prime) simp
  1403 
  1404 lemma prod_prime_factors:
  1405   assumes "x \<noteq> 0"
  1406   shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
  1407 proof -
  1408   have "normalize x = prod_mset (prime_factorization x)"
  1409     by (simp add: prod_mset_prime_factorization assms)
  1410   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
  1411     by (subst prod_mset_multiplicity) simp_all
  1412   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
  1413     by (intro prod.cong)
  1414       (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
  1415   finally show ?thesis ..
  1416 qed
  1417 
  1418 lemma prime_factorization_unique'':
  1419   assumes S_eq: "S = {p. 0 < f p}"
  1420     and "finite S"
  1421     and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
  1422   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  1423 proof
  1424   define A where "A = Abs_multiset f"
  1425   from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
  1426   with S(2) have nz: "n \<noteq> 0" by auto
  1427   from S_eq \<open>finite S\<close> have count_A: "count A = f"
  1428     unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
  1429   from S_eq count_A have set_mset_A: "set_mset A = S"
  1430     by (simp only: set_mset_def)
  1431   from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
  1432   also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
  1433   also from nz have "normalize n = prod_mset (prime_factorization n)"
  1434     by (simp add: prod_mset_prime_factorization)
  1435   finally have "prime_factorization (prod_mset A) =
  1436                   prime_factorization (prod_mset (prime_factorization n))" by simp
  1437   also from S(1) have "prime_factorization (prod_mset A) = A"
  1438     by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
  1439   also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
  1440     by (intro prime_factorization_prod_mset_primes) auto
  1441   finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
  1442 
  1443   show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  1444   proof safe
  1445     fix p :: 'a assume p: "prime p"
  1446     have "multiplicity p n = multiplicity p (normalize n)" by simp
  1447     also have "normalize n = prod_mset A"
  1448       by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
  1449     also from p set_mset_A S(1)
  1450     have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
  1451       by (intro prime_elem_multiplicity_prod_mset_distrib) auto
  1452     also from S(1) p
  1453     have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
  1454       by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
  1455     also have "sum_mset \<dots> = f p"
  1456       by (simp add: semiring_1_class.sum_mset_delta' count_A)
  1457     finally show "f p = multiplicity p n" ..
  1458   qed
  1459 qed
  1460 
  1461 lemma prime_factors_product:
  1462   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
  1463   by (simp add: prime_factorization_mult)
  1464 
  1465 lemma dvd_prime_factors [intro]:
  1466   "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
  1467   by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
  1468 
  1469 (* RENAMED multiplicity_dvd *)
  1470 lemma multiplicity_le_imp_dvd:
  1471   assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  1472   shows   "x dvd y"
  1473 proof (cases "y = 0")
  1474   case False
  1475   from assms this have "prime_factorization x \<subseteq># prime_factorization y"
  1476     by (intro mset_subset_eqI) (auto simp: count_prime_factorization)
  1477   with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd)
  1478 qed auto
  1479 
  1480 lemma dvd_multiplicity_eq:
  1481   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
  1482   by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
  1483 
  1484 lemma multiplicity_eq_imp_eq:
  1485   assumes "x \<noteq> 0" "y \<noteq> 0"
  1486   assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  1487   shows   "normalize x = normalize y"
  1488   using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
  1489 
  1490 lemma prime_factorization_unique':
  1491   assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
  1492   shows   "M = N"
  1493 proof -
  1494   have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
  1495     by (simp only: assms)
  1496   also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
  1497     by (subst prime_factorization_prod_mset_primes) simp_all
  1498   also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
  1499     by (subst prime_factorization_prod_mset_primes) simp_all
  1500   finally show ?thesis .
  1501 qed
  1502 
  1503 lemma multiplicity_cong:
  1504   "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
  1505   by (simp add: multiplicity_def)
  1506 
  1507 lemma not_dvd_imp_multiplicity_0:
  1508   assumes "\<not>p dvd x"
  1509   shows   "multiplicity p x = 0"
  1510 proof -
  1511   from assms have "multiplicity p x < 1"
  1512     by (intro multiplicity_lessI) auto
  1513   thus ?thesis by simp
  1514 qed
  1515 
  1516 lemma inj_on_Prod_primes:
  1517   assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p"
  1518   assumes "\<And>P. P \<in> A \<Longrightarrow> finite P"
  1519   shows   "inj_on Prod A"
  1520 proof (rule inj_onI)
  1521   fix P Q assume PQ: "P \<in> A" "Q \<in> A" "\<Prod>P = \<Prod>Q"
  1522   with prime_factorization_unique'[of "mset_set P" "mset_set Q"] assms[of P] assms[of Q]
  1523     have "mset_set P = mset_set Q" by (auto simp: prod_unfold_prod_mset)
  1524     with assms[of P] assms[of Q] PQ show "P = Q" by simp
  1525 qed
  1526 
  1527 
  1528 
  1529 subsection \<open>GCD and LCM computation with unique factorizations\<close>
  1530 
  1531 definition "gcd_factorial a b = (if a = 0 then normalize b
  1532      else if b = 0 then normalize a
  1533      else prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1534 
  1535 definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
  1536      else prod_mset (prime_factorization a \<union># prime_factorization b))"
  1537 
  1538 definition "Gcd_factorial A =
  1539   (if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))"
  1540 
  1541 definition "Lcm_factorial A =
  1542   (if A = {} then 1
  1543    else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then
  1544      prod_mset (Sup (prime_factorization ` A))
  1545    else
  1546      0)"
  1547 
  1548 lemma prime_factorization_gcd_factorial:
  1549   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1550   shows   "prime_factorization (gcd_factorial a b) = prime_factorization a \<inter># prime_factorization b"
  1551 proof -
  1552   have "prime_factorization (gcd_factorial a b) =
  1553           prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1554     by (simp add: gcd_factorial_def)
  1555   also have "\<dots> = prime_factorization a \<inter># prime_factorization b"
  1556     by (subst prime_factorization_prod_mset_primes) auto
  1557   finally show ?thesis .
  1558 qed
  1559 
  1560 lemma prime_factorization_lcm_factorial:
  1561   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1562   shows   "prime_factorization (lcm_factorial a b) = prime_factorization a \<union># prime_factorization b"
  1563 proof -
  1564   have "prime_factorization (lcm_factorial a b) =
  1565           prime_factorization (prod_mset (prime_factorization a \<union># prime_factorization b))"
  1566     by (simp add: lcm_factorial_def)
  1567   also have "\<dots> = prime_factorization a \<union># prime_factorization b"
  1568     by (subst prime_factorization_prod_mset_primes) auto
  1569   finally show ?thesis .
  1570 qed
  1571 
  1572 lemma prime_factorization_Gcd_factorial:
  1573   assumes "\<not>A \<subseteq> {0}"
  1574   shows   "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
  1575 proof -
  1576   from assms obtain x where x: "x \<in> A - {0}" by auto
  1577   hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
  1578     by (intro subset_mset.cInf_lower) simp_all
  1579   hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> prime_factors x"
  1580     by (auto dest: mset_subset_eqD)
  1581   with in_prime_factors_imp_prime[of _ x]
  1582     have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
  1583   with assms show ?thesis
  1584     by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes)
  1585 qed
  1586 
  1587 lemma prime_factorization_Lcm_factorial:
  1588   assumes "0 \<notin> A" "subset_mset.bdd_above (prime_factorization ` A)"
  1589   shows   "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
  1590 proof (cases "A = {}")
  1591   case True
  1592   hence "prime_factorization ` A = {}" by auto
  1593   also have "Sup \<dots> = {#}" by (simp add: Sup_multiset_empty)
  1594   finally show ?thesis by (simp add: Lcm_factorial_def)
  1595 next
  1596   case False
  1597   have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
  1598     by (auto simp: in_Sup_multiset_iff assms)
  1599   with assms False show ?thesis
  1600     by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes)
  1601 qed
  1602 
  1603 lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a"
  1604   by (simp add: gcd_factorial_def multiset_inter_commute)
  1605 
  1606 lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a"
  1607 proof (cases "a = 0 \<or> b = 0")
  1608   case False
  1609   hence "gcd_factorial a b \<noteq> 0" by (auto simp: gcd_factorial_def)
  1610   with False show ?thesis
  1611     by (subst prime_factorization_subset_iff_dvd [symmetric])
  1612        (auto simp: prime_factorization_gcd_factorial)
  1613 qed (auto simp: gcd_factorial_def)
  1614 
  1615 lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b"
  1616   by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1)
  1617 
  1618 lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b"
  1619 proof -
  1620   have "normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)) =
  1621           prod_mset (prime_factorization a \<inter># prime_factorization b)"
  1622     by (intro normalize_prod_mset_primes) auto
  1623   thus ?thesis by (simp add: gcd_factorial_def)
  1624 qed
  1625 
  1626 lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c
  1627 proof (cases "a = 0 \<or> b = 0")
  1628   case False
  1629   with that have [simp]: "c \<noteq> 0" by auto
  1630   let ?p = "prime_factorization"
  1631   from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b"
  1632     by (simp_all add: prime_factorization_subset_iff_dvd)
  1633   hence "prime_factorization c \<subseteq>#
  1634            prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1635     using False by (subst prime_factorization_prod_mset_primes) auto
  1636   with False show ?thesis
  1637     by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric])
  1638 qed (auto simp: gcd_factorial_def that)
  1639 
  1640 lemma lcm_factorial_gcd_factorial:
  1641   "lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b
  1642 proof (cases "a = 0 \<or> b = 0")
  1643   case False
  1644   let ?p = "prime_factorization"
  1645   from False have "prod_mset (?p (a * b)) div gcd_factorial a b =
  1646                      prod_mset (?p a + ?p b - ?p a \<inter># ?p b)"
  1647     by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def
  1648                                 prime_factorization_mult subset_mset.le_infI1)
  1649   also from False have "prod_mset (?p (a * b)) = normalize (a * b)"
  1650     by (intro prod_mset_prime_factorization) simp_all
  1651   also from False have "prod_mset (?p a + ?p b - ?p a \<inter># ?p b) = lcm_factorial a b"
  1652     by (simp add: union_diff_inter_eq_sup lcm_factorial_def)
  1653   finally show ?thesis ..
  1654 qed (auto simp: lcm_factorial_def)
  1655 
  1656 lemma normalize_Gcd_factorial:
  1657   "normalize (Gcd_factorial A) = Gcd_factorial A"
  1658 proof (cases "A \<subseteq> {0}")
  1659   case False
  1660   then obtain x where "x \<in> A" "x \<noteq> 0" by blast
  1661   hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
  1662     by (intro subset_mset.cInf_lower) auto
  1663   hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
  1664     using that by (auto dest: mset_subset_eqD)
  1665   with False show ?thesis
  1666     by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
  1667 qed (simp_all add: Gcd_factorial_def)
  1668 
  1669 lemma Gcd_factorial_eq_0_iff:
  1670   "Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}"
  1671   by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits)
  1672 
  1673 lemma Gcd_factorial_dvd:
  1674   assumes "x \<in> A"
  1675   shows   "Gcd_factorial A dvd x"
  1676 proof (cases "x = 0")
  1677   case False
  1678   with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
  1679     by (intro prime_factorization_Gcd_factorial) auto
  1680   also from False assms have "\<dots> \<subseteq># prime_factorization x"
  1681     by (intro subset_mset.cInf_lower) auto
  1682   finally show ?thesis
  1683     by (subst (asm) prime_factorization_subset_iff_dvd)
  1684        (insert assms False, auto simp: Gcd_factorial_eq_0_iff)
  1685 qed simp_all
  1686 
  1687 lemma Gcd_factorial_greatest:
  1688   assumes "\<And>y. y \<in> A \<Longrightarrow> x dvd y"
  1689   shows   "x dvd Gcd_factorial A"
  1690 proof (cases "A \<subseteq> {0}")
  1691   case False
  1692   from False obtain y where "y \<in> A" "y \<noteq> 0" by auto
  1693   with assms[of y] have nz: "x \<noteq> 0" by auto
  1694   from nz assms have "prime_factorization x \<subseteq># prime_factorization y" if "y \<in> A - {0}" for y
  1695     using that by (subst prime_factorization_subset_iff_dvd) auto
  1696   with False have "prime_factorization x \<subseteq># Inf (prime_factorization ` (A - {0}))"
  1697     by (intro subset_mset.cInf_greatest) auto
  1698   also from False have "\<dots> = prime_factorization (Gcd_factorial A)"
  1699     by (rule prime_factorization_Gcd_factorial [symmetric])
  1700   finally show ?thesis
  1701     by (subst (asm) prime_factorization_subset_iff_dvd)
  1702        (insert nz False, auto simp: Gcd_factorial_eq_0_iff)
  1703 qed (simp_all add: Gcd_factorial_def)
  1704 
  1705 lemma normalize_Lcm_factorial:
  1706   "normalize (Lcm_factorial A) = Lcm_factorial A"
  1707 proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
  1708   case True
  1709   hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
  1710            prod_mset (Sup (prime_factorization ` A))"
  1711     by (intro normalize_prod_mset_primes)
  1712        (auto simp: in_Sup_multiset_iff)
  1713   with True show ?thesis by (simp add: Lcm_factorial_def)
  1714 qed (auto simp: Lcm_factorial_def)
  1715 
  1716 lemma Lcm_factorial_eq_0_iff:
  1717   "Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)"
  1718   by (auto simp: Lcm_factorial_def in_Sup_multiset_iff)
  1719 
  1720 lemma dvd_Lcm_factorial:
  1721   assumes "x \<in> A"
  1722   shows   "x dvd Lcm_factorial A"
  1723 proof (cases "0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` A)")
  1724   case True
  1725   with assms have [simp]: "0 \<notin> A" "x \<noteq> 0" "A \<noteq> {}" by auto
  1726   from assms True have "prime_factorization x \<subseteq># Sup (prime_factorization ` A)"
  1727     by (intro subset_mset.cSup_upper) auto
  1728   also have "\<dots> = prime_factorization (Lcm_factorial A)"
  1729     by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all)
  1730   finally show ?thesis
  1731     by (subst (asm) prime_factorization_subset_iff_dvd)
  1732        (insert True, auto simp: Lcm_factorial_eq_0_iff)
  1733 qed (insert assms, auto simp: Lcm_factorial_def)
  1734 
  1735 lemma Lcm_factorial_least:
  1736   assumes "\<And>y. y \<in> A \<Longrightarrow> y dvd x"
  1737   shows   "Lcm_factorial A dvd x"
  1738 proof -
  1739   consider "A = {}" | "0 \<in> A" | "x = 0" | "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" by blast
  1740   thus ?thesis
  1741   proof cases
  1742     assume *: "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0"
  1743     hence nz: "x \<noteq> 0" if "x \<in> A" for x using that by auto
  1744     from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)"
  1745       by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"])
  1746          (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
  1747     have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
  1748       by (rule prime_factorization_Lcm_factorial) fact+
  1749     also from * have "\<dots> \<subseteq># prime_factorization x"
  1750       by (intro subset_mset.cSup_least)
  1751          (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
  1752     finally show ?thesis
  1753       by (subst (asm) prime_factorization_subset_iff_dvd)
  1754          (insert * bdd, auto simp: Lcm_factorial_eq_0_iff)
  1755   qed (auto simp: Lcm_factorial_def dest: assms)
  1756 qed
  1757 
  1758 lemmas gcd_lcm_factorial =
  1759   gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest
  1760   normalize_gcd_factorial lcm_factorial_gcd_factorial
  1761   normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest
  1762   normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least
  1763 
  1764 end
  1765 
  1766 class factorial_semiring_gcd = factorial_semiring + gcd + Gcd +
  1767   assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b"
  1768   and     lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b"
  1769   and     Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A"
  1770   and     Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A"
  1771 begin
  1772 
  1773 lemma prime_factorization_gcd:
  1774   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1775   shows   "prime_factorization (gcd a b) = prime_factorization a \<inter># prime_factorization b"
  1776   by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial)
  1777 
  1778 lemma prime_factorization_lcm:
  1779   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1780   shows   "prime_factorization (lcm a b) = prime_factorization a \<union># prime_factorization b"
  1781   by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial)
  1782 
  1783 lemma prime_factorization_Gcd:
  1784   assumes "Gcd A \<noteq> 0"
  1785   shows   "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))"
  1786   using assms
  1787   by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff)
  1788 
  1789 lemma prime_factorization_Lcm:
  1790   assumes "Lcm A \<noteq> 0"
  1791   shows   "prime_factorization (Lcm A) = Sup (prime_factorization ` A)"
  1792   using assms
  1793   by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff)
  1794 
  1795 lemma prime_factors_gcd [simp]: 
  1796   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (gcd a b) = 
  1797      prime_factors a \<inter> prime_factors b"
  1798   by (subst prime_factorization_gcd) auto
  1799 
  1800 lemma prime_factors_lcm [simp]: 
  1801   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> prime_factors (lcm a b) = 
  1802      prime_factors a \<union> prime_factors b"
  1803   by (subst prime_factorization_lcm) auto
  1804 
  1805 subclass semiring_gcd
  1806   by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial)
  1807      (rule gcd_lcm_factorial; assumption)+
  1808 
  1809 subclass semiring_Gcd
  1810   by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
  1811      (rule gcd_lcm_factorial; assumption)+
  1812 
  1813 lemma
  1814   assumes "x \<noteq> 0" "y \<noteq> 0"
  1815   shows gcd_eq_factorial':
  1816           "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
  1817                           p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
  1818     and lcm_eq_factorial':
  1819           "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
  1820                           p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
  1821 proof -
  1822   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
  1823   also have "\<dots> = ?rhs1"
  1824     by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
  1825           count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
  1826   finally show "gcd x y = ?rhs1" .
  1827   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
  1828   also have "\<dots> = ?rhs2"
  1829     by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
  1830           count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
  1831   finally show "lcm x y = ?rhs2" .
  1832 qed
  1833 
  1834 lemma
  1835   assumes "x \<noteq> 0" "y \<noteq> 0" "prime p"
  1836   shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
  1837     and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
  1838 proof -
  1839   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
  1840   also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)"
  1841     by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial)
  1842   finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" .
  1843   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
  1844   also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)"
  1845     by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial)
  1846   finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" .
  1847 qed
  1848 
  1849 lemma gcd_lcm_distrib:
  1850   "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
  1851 proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
  1852   case True
  1853   thus ?thesis
  1854     by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
  1855 next
  1856   case False
  1857   hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
  1858     by (intro associatedI prime_factorization_subset_imp_dvd)
  1859        (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
  1860           subset_mset.inf_sup_distrib1)
  1861   thus ?thesis by simp
  1862 qed
  1863 
  1864 lemma lcm_gcd_distrib:
  1865   "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)"
  1866 proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
  1867   case True
  1868   thus ?thesis
  1869     by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
  1870 next
  1871   case False
  1872   hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
  1873     by (intro associatedI prime_factorization_subset_imp_dvd)
  1874        (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
  1875           subset_mset.sup_inf_distrib1)
  1876   thus ?thesis by simp
  1877 qed
  1878 
  1879 end
  1880 
  1881 class factorial_ring_gcd = factorial_semiring_gcd + idom
  1882 begin
  1883 
  1884 subclass ring_gcd ..
  1885 
  1886 subclass idom_divide ..
  1887 
  1888 end
  1889 
  1890 end