author haftmann Sun Sep 18 17:57:55 2016 +0200 (2016-09-18) changeset 63924 f91766530e13 parent 63923 c9bba9dba73b child 63925 500646ef617a
more generic algebraic lemmas
 src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Groups_Big.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | revisions src/HOL/Number_Theory/Factorial_Ring.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/GCD.thy	Tue Sep 20 14:51:58 2016 +0200
1.2 +++ b/src/HOL/GCD.thy	Sun Sep 18 17:57:55 2016 +0200
1.3 @@ -939,6 +939,25 @@
1.4  lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
1.5    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
1.6
1.7 +lemma dvd_productE:
1.8 +  assumes "p dvd (a * b)"
1.9 +  obtains x y where "p = x * y" "x dvd a" "y dvd b"
1.10 +proof (cases "a = 0")
1.11 +  case True
1.12 +  thus ?thesis by (intro that[of p 1]) simp_all
1.13 +next
1.14 +  case False
1.15 +  define x y where "x = gcd a p" and "y = p div x"
1.16 +  have "p = x * y" by (simp add: x_def y_def)
1.17 +  moreover have "x dvd a" by (simp add: x_def)
1.18 +  moreover from assms have "p dvd gcd (b * a) (b * p)"
1.19 +    by (intro gcd_greatest) (simp_all add: mult.commute)
1.20 +  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
1.21 +  with False have "y dvd b"
1.22 +    by (simp add: x_def y_def div_dvd_iff_mult assms)
1.23 +  ultimately show ?thesis by (rule that)
1.24 +qed
1.25 +
1.26  end
1.27
1.28  class ring_gcd = comm_ring_1 + semiring_gcd
```
```     2.1 --- a/src/HOL/Groups_Big.thy	Tue Sep 20 14:51:58 2016 +0200
2.2 +++ b/src/HOL/Groups_Big.thy	Sun Sep 18 17:57:55 2016 +0200
2.3 @@ -1130,8 +1130,8 @@
2.4
2.5  end
2.6
2.7 -lemma setprod_zero_iff [simp]:
2.8 -  fixes f :: "'b \<Rightarrow> 'a::semidom"
2.9 +lemma (in semidom) setprod_zero_iff [simp]:
2.10 +  fixes f :: "'b \<Rightarrow> 'a"
2.11    assumes "finite A"
2.12    shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
2.13    using assms by (induct A) (auto simp: no_zero_divisors)
```
```     3.1 --- a/src/HOL/Library/Multiset.thy	Tue Sep 20 14:51:58 2016 +0200
3.2 +++ b/src/HOL/Library/Multiset.thy	Sun Sep 18 17:57:55 2016 +0200
3.3 @@ -247,6 +247,14 @@
3.4    by (auto simp del: count_greater_eq_Suc_zero_iff
3.5        simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
3.6
3.7 +lemma multiset_nonemptyE [elim]:
3.8 +  assumes "A \<noteq> {#}"
3.9 +  obtains x where "x \<in># A"
3.10 +proof -
3.11 +  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
3.12 +  with that show ?thesis by blast
3.13 +qed
3.14 +
3.15
3.16  subsubsection \<open>Union\<close>
3.17
3.18 @@ -2041,6 +2049,10 @@
3.19  lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
3.20    by (auto simp: multiset_eq_iff)
3.21
3.22 +lemma image_replicate_mset [simp]:
3.23 +  "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
3.24 +  by (induct n) simp_all
3.25 +
3.26
3.27  subsection \<open>Big operators\<close>
3.28
3.29 @@ -2209,14 +2221,20 @@
3.30  translations
3.31    "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
3.32
3.33 -lemma (in comm_semiring_1) dvd_prod_mset:
3.34 +lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
3.35 +  assumes "A \<subseteq># B"
3.36 +  shows   "prod_mset A dvd prod_mset B"
3.37 +proof -
3.38 +  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
3.39 +  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
3.40 +  also have "prod_mset A dvd \<dots>" by simp
3.41 +  finally show ?thesis .
3.42 +qed
3.43 +
3.44 +lemma (in comm_monoid_mult) dvd_prod_mset:
3.45    assumes "x \<in># A"
3.46    shows "x dvd prod_mset A"
3.47 -proof -
3.48 -  from assms have "A = add_mset x (A - {#x#})" by simp
3.49 -  then obtain B where "A = add_mset x B" ..
3.50 -  then show ?thesis by simp
3.51 -qed
3.52 +  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
3.53
3.54  lemma (in semidom) prod_mset_zero_iff [iff]:
3.55    "prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
3.56 @@ -2236,10 +2254,22 @@
3.57    shows "prod_mset (A - {#a#}) = prod_mset A div a"
3.58    using assms prod_mset_diff [of "{#a#}" A] by auto
3.59
3.60 +lemma (in algebraic_semidom) is_unit_prod_mset_iff:
3.61 +  "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x \<in># A. is_unit x)"
3.62 +  by (induct A) (auto simp: is_unit_mult_iff)
3.63 +
3.64 +lemma (in normalization_semidom) normalize_prod_mset:
3.65 +  "normalize (prod_mset A) = prod_mset (image_mset normalize A)"
3.66 +  by (induct A) (simp_all add: normalize_mult)
3.67 +
3.68  lemma (in normalization_semidom) normalized_prod_msetI:
3.69    assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
3.70    shows "normalize (prod_mset A) = prod_mset A"
3.71 -  using assms by (induct A) (simp_all add: normalize_mult)
3.72 +proof -
3.73 +  from assms have "image_mset normalize A = A"
3.74 +    by (induct A) simp_all
3.75 +  then show ?thesis by (simp add: normalize_prod_mset)
3.76 +qed
3.77
3.78
3.79  subsection \<open>Alternative representations\<close>
```
```     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Sep 20 14:51:58 2016 +0200
4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Sep 18 17:57:55 2016 +0200
4.3 @@ -112,23 +112,6 @@
4.4      by (auto intro!: euclidean_size_times_nonunit simp: )
4.5  qed
4.6
4.7 -lemma irreducible_normalized_divisors:
4.8 -  assumes "irreducible x" "y dvd x" "normalize y = y"
4.9 -  shows   "y = 1 \<or> y = normalize x"
4.10 -proof -
4.11 -  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
4.12 -  thus ?thesis
4.13 -  proof (elim disjE)
4.14 -    assume "is_unit y"
4.15 -    hence "normalize y = 1" by (simp add: is_unit_normalize)
4.16 -    with assms show ?thesis by simp
4.17 -  next
4.18 -    assume "x dvd y"
4.19 -    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
4.20 -    with assms show ?thesis by simp
4.21 -  qed
4.22 -qed
4.23 -
4.24  function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
4.25  where
4.26    "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
4.27 @@ -720,4 +703,4 @@
4.28            semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
4.29  qed
4.30
4.31 -end
4.32 \ No newline at end of file
4.33 +end
```
```     5.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Sep 20 14:51:58 2016 +0200
5.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Sun Sep 18 17:57:55 2016 +0200
5.3 @@ -1,4 +1,5 @@
5.4  (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
5.5 +    Author:     Manuel Eberl, TU Muenchen
5.6      Author:     Florian Haftmann, TU Muenchen
5.7  *)
5.8
5.9 @@ -7,29 +8,11 @@
5.10  theory Factorial_Ring
5.11  imports
5.12    Main
5.13 -  "../GCD"
5.14 +  "~~/src/HOL/GCD"
5.15    "~~/src/HOL/Library/Multiset"
5.16  begin
5.17
5.18 -lemma (in semiring_gcd) dvd_productE:
5.19 -  assumes "p dvd (a * b)"
5.20 -  obtains x y where "p = x * y" "x dvd a" "y dvd b"
5.21 -proof (cases "a = 0")
5.22 -  case True
5.23 -  thus ?thesis by (intro that[of p 1]) simp_all
5.24 -next
5.25 -  case False
5.26 -  define x y where "x = gcd a p" and "y = p div x"
5.27 -  have "p = x * y" by (simp add: x_def y_def)
5.28 -  moreover have "x dvd a" by (simp add: x_def)
5.29 -  moreover from assms have "p dvd gcd (b * a) (b * p)"
5.30 -    by (intro gcd_greatest) (simp_all add: mult.commute)
5.31 -  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
5.32 -  with False have "y dvd b"
5.33 -    by (simp add: x_def y_def div_dvd_iff_mult assms)
5.34 -  ultimately show ?thesis by (rule that)
5.35 -qed
5.36 -
5.37 +subsection \<open>Irreducible and prime elements\<close>
5.38
5.39  context comm_semiring_1
5.40  begin
5.41 @@ -83,7 +66,6 @@
5.42    shows "p \<noteq> 0"
5.43    using assms by (auto intro: ccontr)
5.44
5.45 -
5.46  lemma prime_elem_dvd_power:
5.47    "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
5.48    by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
5.49 @@ -105,10 +87,6 @@
5.50  context algebraic_semidom
5.51  begin
5.52
5.53 -(* TODO Move *)
5.54 -lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
5.55 -  by (subst mult.commute) (rule mult_unit_dvd_iff)
5.56 -
5.57  lemma prime_elem_imp_irreducible:
5.58    assumes "prime_elem p"
5.59    shows   "irreducible p"
5.60 @@ -123,6 +101,22 @@
5.61      by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
5.62  qed (insert assms, simp_all add: prime_elem_def)
5.63
5.64 +lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors:
5.65 +  assumes "is_unit x" "irreducible p"
5.66 +  shows   "\<not>p dvd x"
5.67 +proof (rule notI)
5.68 +  assume "p dvd x"
5.69 +  with \<open>is_unit x\<close> have "is_unit p"
5.70 +    by (auto intro: dvd_trans)
5.71 +  with \<open>irreducible p\<close> show False
5.72 +    by (simp add: irreducible_not_unit)
5.73 +qed
5.74 +
5.75 +lemma unit_imp_no_prime_divisors:
5.76 +  assumes "is_unit x" "prime_elem p"
5.77 +  shows   "\<not>p dvd x"
5.78 +  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
5.79 +
5.80  lemma prime_elem_mono:
5.81    assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
5.82    shows   "prime_elem q"
5.83 @@ -306,12 +300,17 @@
5.84    qed
5.85  qed
5.86
5.87 -lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
5.88 -  by arith
5.89 -
5.90  lemma prime_elem_power_dvd_cases:
5.91 -     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
5.92 -  using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem)
5.93 +  assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p"
5.94 +  shows "p ^ a dvd m \<or> p ^ b dvd n"
5.95 +proof -
5.96 +  from assms obtain r s
5.97 +    where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n"
5.98 +    by (blast dest: prime_elem_power_dvd_prod)
5.99 +  moreover with assms have
5.100 +    "a \<le> r \<or> b \<le> s" by arith
5.101 +  ultimately show ?thesis by (auto intro: power_le_dvd)
5.102 +qed
5.103
5.104  lemma prime_elem_not_unit' [simp]:
5.105    "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
5.106 @@ -358,9 +357,29 @@
5.107
5.108  end
5.109
5.110 +
5.111 +subsection \<open>Generalized primes: normalized prime elements\<close>
5.112 +
5.113  context normalization_semidom
5.114  begin
5.115
5.116 +lemma irreducible_normalized_divisors:
5.117 +  assumes "irreducible x" "y dvd x" "normalize y = y"
5.118 +  shows   "y = 1 \<or> y = normalize x"
5.119 +proof -
5.120 +  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
5.121 +  thus ?thesis
5.122 +  proof (elim disjE)
5.123 +    assume "is_unit y"
5.124 +    hence "normalize y = 1" by (simp add: is_unit_normalize)
5.125 +    with assms show ?thesis by simp
5.126 +  next
5.127 +    assume "x dvd y"
5.128 +    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
5.129 +    with assms show ?thesis by simp
5.130 +  qed
5.131 +qed
5.132 +
5.133  lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
5.134    using irreducible_mult_unit_left[of "1 div unit_factor x" x]
5.135    by (cases "x = 0") (simp_all add: unit_div_commute)
5.136 @@ -443,16 +462,6 @@
5.137    "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
5.138    by (subst prime_elem_dvd_power_iff) simp_all
5.139
5.140 -lemma prod_mset_subset_imp_dvd:
5.141 -  assumes "A \<subseteq># B"
5.142 -  shows   "prod_mset A dvd prod_mset B"
5.143 -proof -
5.144 -  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
5.145 -  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
5.146 -  also have "prod_mset A dvd \<dots>" by simp
5.147 -  finally show ?thesis .
5.148 -qed
5.149 -
5.150  lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
5.151    by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
5.152
5.153 @@ -508,26 +517,11 @@
5.154    shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
5.155    using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)
5.156
5.157 -lemma is_unit_prod_mset_iff:
5.158 -  "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
5.159 -  by (induction A) (auto simp: is_unit_mult_iff)
5.160 -
5.161 -lemma multiset_emptyI: "(\<And>x. x \<notin># A) \<Longrightarrow> A = {#}"
5.162 -  by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
5.163 -
5.164  lemma is_unit_prod_mset_primes_iff:
5.165    assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
5.166    shows   "is_unit (prod_mset A) \<longleftrightarrow> A = {#}"
5.167 -proof
5.168 -  assume unit: "is_unit (prod_mset A)"
5.169 -  show "A = {#}"
5.170 -  proof (intro multiset_emptyI notI)
5.171 -    fix x assume "x \<in># A"
5.172 -    with unit have "is_unit x" by (subst (asm) is_unit_prod_mset_iff) blast
5.173 -    moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
5.174 -    ultimately show False by simp
5.175 -  qed
5.176 -qed simp_all
5.177 +  by (auto simp add: is_unit_prod_mset_iff)
5.178 +    (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff)
5.179
5.180  lemma prod_mset_primes_irreducible_imp_prime:
5.181    assumes irred: "irreducible (prod_mset A)"
5.182 @@ -555,14 +549,6 @@
5.183      by (auto intro: prod_mset_subset_imp_dvd)
5.184  qed
5.185
5.186 -lemma multiset_nonemptyE [elim]:
5.187 -  assumes "A \<noteq> {#}"
5.188 -  obtains x where "x \<in># A"
5.189 -proof -
5.190 -  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
5.191 -  with that show ?thesis by blast
5.192 -qed
5.193 -
5.194  lemma prod_mset_primes_finite_divisor_powers:
5.195    assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
5.196    assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
5.197 @@ -585,11 +571,10 @@
5.198    ultimately show ?thesis by (rule finite_subset)
5.199  qed
5.200
5.201 -lemma normalize_prod_mset:
5.202 -  "normalize (prod_mset A) = prod_mset (image_mset normalize A)"
5.203 -  by (induction A) (simp_all add: normalize_mult mult_ac)
5.204 +end
5.205
5.206 -end
5.207 +
5.208 +subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
5.209
5.210  context semiring_gcd
5.211  begin
5.212 @@ -652,9 +637,83 @@
5.213  end
5.214
5.215
5.216 +subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close>
5.217 +
5.218  class factorial_semiring = normalization_semidom +
5.219    assumes prime_factorization_exists:
5.220 -            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
5.221 +    "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
5.222 +
5.223 +text \<open>Alternative characterization\<close>
5.224 +
5.225 +lemma (in normalization_semidom) factorial_semiring_altI_aux:
5.226 +  assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
5.227 +  assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
5.228 +  assumes "x \<noteq> 0"
5.229 +  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
5.230 +using \<open>x \<noteq> 0\<close>
5.231 +proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
5.232 +  case (less a)
5.233 +  let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
5.234 +  show ?case
5.235 +  proof (cases "is_unit a")
5.236 +    case True
5.237 +    thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
5.238 +  next
5.239 +    case False
5.240 +    show ?thesis
5.241 +    proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
5.242 +      case False
5.243 +      with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
5.244 +      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
5.245 +      thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
5.246 +    next
5.247 +      case True
5.248 +      then guess b by (elim exE conjE) note b = this
5.249 +
5.250 +      from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
5.251 +      moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
5.252 +      hence "?fctrs b \<noteq> ?fctrs a" by blast
5.253 +      ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
5.254 +      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
5.255 +        by (rule psubset_card_mono)
5.256 +      moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
5.257 +      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
5.258 +        by (intro less) auto
5.259 +      then guess A .. note A = this
5.260 +
5.261 +      define c where "c = a div b"
5.262 +      from b have c: "a = b * c" by (simp add: c_def)
5.263 +      from less.prems c have "c \<noteq> 0" by auto
5.264 +      from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
5.265 +      moreover have "normalize a \<notin> ?fctrs c"
5.266 +      proof safe
5.267 +        assume "normalize a dvd c"
5.268 +        hence "b * c dvd 1 * c" by (simp add: c)
5.269 +        hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
5.270 +        with b show False by simp
5.271 +      qed
5.272 +      with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
5.273 +      ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
5.274 +      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
5.275 +        by (rule psubset_card_mono)
5.276 +      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
5.277 +        by (intro less) auto
5.278 +      then guess B .. note B = this
5.279 +
5.280 +      from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
5.281 +    qed
5.282 +  qed
5.283 +qed
5.284 +
5.285 +lemma factorial_semiring_altI:
5.286 +  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
5.287 +  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
5.288 +  shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
5.289 +  by intro_classes (rule factorial_semiring_altI_aux[OF assms])
5.290 +
5.291 +text \<open>Properties\<close>
5.292 +
5.293 +context factorial_semiring
5.294  begin
5.295
5.296  lemma prime_factorization_exists':
5.297 @@ -784,24 +843,6 @@
5.298  lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x"
5.299    by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])
5.300
5.301 -lemma dvd_power_iff:
5.302 -  assumes "x \<noteq> 0"
5.303 -  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
5.304 -proof
5.305 -  assume *: "x ^ m dvd x ^ n"
5.306 -  {
5.307 -    assume "m > n"
5.308 -    note *
5.309 -    also have "x ^ n = x ^ n * 1" by simp
5.310 -    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
5.311 -    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
5.312 -    finally have "x ^ (m - n) dvd 1"
5.313 -      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
5.314 -    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
5.315 -  }
5.316 -  thus "is_unit x \<or> m \<le> n" by force
5.317 -qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
5.318 -
5.319  context
5.320    fixes x p :: 'a
5.321    assumes xp: "x \<noteq> 0" "\<not>is_unit p"
5.322 @@ -965,6 +1006,65 @@
5.323    qed
5.324  qed simp_all
5.325
5.326 +lemma multiplicity_self:
5.327 +  assumes "p \<noteq> 0" "\<not>is_unit p"
5.328 +  shows   "multiplicity p p = 1"
5.329 +proof -
5.330 +  from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
5.331 +    by (simp add: multiplicity_eq_Max)
5.332 +  also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
5.333 +    using dvd_power_iff[of p n 1] by auto
5.334 +  hence "{n. p ^ n dvd p} = {..1}" by auto
5.335 +  also have "\<dots> = {0,1}" by auto
5.336 +  finally show ?thesis by simp
5.337 +qed
5.338 +
5.339 +lemma multiplicity_times_unit_left:
5.340 +  assumes "is_unit c"
5.341 +  shows   "multiplicity (c * p) x = multiplicity p x"
5.342 +proof -
5.343 +  from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
5.344 +    by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
5.345 +  thus ?thesis by (simp add: multiplicity_def)
5.346 +qed
5.347 +
5.348 +lemma multiplicity_times_unit_right:
5.349 +  assumes "is_unit c"
5.350 +  shows   "multiplicity p (c * x) = multiplicity p x"
5.351 +proof -
5.352 +  from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
5.353 +    by (subst mult.commute) (simp add: dvd_mult_unit_iff)
5.354 +  thus ?thesis by (simp add: multiplicity_def)
5.355 +qed
5.356 +
5.357 +lemma multiplicity_normalize_left [simp]:
5.358 +  "multiplicity (normalize p) x = multiplicity p x"
5.359 +proof (cases "p = 0")
5.360 +  case [simp]: False
5.361 +  have "normalize p = (1 div unit_factor p) * p"
5.362 +    by (simp add: unit_div_commute is_unit_unit_factor)
5.363 +  also have "multiplicity \<dots> x = multiplicity p x"
5.364 +    by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
5.365 +  finally show ?thesis .
5.366 +qed simp_all
5.367 +
5.368 +lemma multiplicity_normalize_right [simp]:
5.369 +  "multiplicity p (normalize x) = multiplicity p x"
5.370 +proof (cases "x = 0")
5.371 +  case [simp]: False
5.372 +  have "normalize x = (1 div unit_factor x) * x"
5.373 +    by (simp add: unit_div_commute is_unit_unit_factor)
5.374 +  also have "multiplicity p \<dots> = multiplicity p x"
5.375 +    by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
5.376 +  finally show ?thesis .
5.377 +qed simp_all
5.378 +
5.379 +lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
5.380 +  by (rule multiplicity_self) auto
5.381 +
5.382 +lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
5.383 +  by (subst multiplicity_same_power') auto
5.384 +
5.385  lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
5.386    "\<lambda>x p. if prime p then multiplicity p x else 0"
5.387    unfolding multiset_def
5.388 @@ -996,15 +1096,14 @@
5.389    "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
5.390    by transfer simp
5.391
5.392 -lemma unit_imp_no_irreducible_divisors:
5.393 -  assumes "is_unit x" "irreducible p"
5.394 -  shows   "\<not>p dvd x"
5.395 -  using assms dvd_unit_imp_unit irreducible_not_unit by blast
5.396 -
5.397 -lemma unit_imp_no_prime_divisors:
5.398 -  assumes "is_unit x" "prime_elem p"
5.399 -  shows   "\<not>p dvd x"
5.400 -  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
5.401 +lemma dvd_imp_multiplicity_le:
5.402 +  assumes "a dvd b" "b \<noteq> 0"
5.403 +  shows   "multiplicity p a \<le> multiplicity p b"
5.404 +proof (cases "is_unit p")
5.405 +  case False
5.406 +  with assms show ?thesis
5.407 +    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
5.408 +qed (insert assms, auto simp: multiplicity_unit_left)
5.409
5.410  lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
5.411    by (simp add: multiset_eq_iff count_prime_factorization)
5.412 @@ -1100,18 +1199,17 @@
5.413    "p \<in> prime_factors x \<Longrightarrow> p dvd x"
5.415
5.416 -lemma multiplicity_self:
5.417 -  assumes "p \<noteq> 0" "\<not>is_unit p"
5.418 -  shows   "multiplicity p p = 1"
5.419 -proof -
5.420 -  from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
5.421 -    by (simp add: multiplicity_eq_Max)
5.422 -  also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
5.423 -    using dvd_power_iff[of p n 1] by auto
5.424 -  hence "{n. p ^ n dvd p} = {..1}" by auto
5.425 -  also have "\<dots> = {0,1}" by auto
5.426 -  finally show ?thesis by simp
5.427 -qed
5.428 +lemma prime_factorsI:
5.429 +  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
5.430 +  by (auto simp: in_prime_factors_iff)
5.431 +
5.432 +lemma prime_factors_dvd:
5.433 +  "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
5.434 +  by (auto intro: prime_factorsI)
5.435 +
5.436 +lemma prime_factors_multiplicity:
5.437 +  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
5.438 +  by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff)
5.439
5.440  lemma prime_factorization_prime:
5.441    assumes "prime p"
5.442 @@ -1136,44 +1234,6 @@
5.443      by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
5.444  qed simp_all
5.445
5.446 -lemma multiplicity_times_unit_left:
5.447 -  assumes "is_unit c"
5.448 -  shows   "multiplicity (c * p) x = multiplicity p x"
5.449 -proof -
5.450 -  from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
5.451 -    by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
5.452 -  thus ?thesis by (simp add: multiplicity_def)
5.453 -qed
5.454 -
5.455 -lemma multiplicity_times_unit_right:
5.456 -  assumes "is_unit c"
5.457 -  shows   "multiplicity p (c * x) = multiplicity p x"
5.458 -proof -
5.459 -  from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
5.460 -    by (subst mult.commute) (simp add: dvd_mult_unit_iff)
5.461 -  thus ?thesis by (simp add: multiplicity_def)
5.462 -qed
5.463 -
5.464 -lemma multiplicity_normalize_left [simp]: "multiplicity (normalize p) x = multiplicity p x"
5.465 -proof (cases "p = 0")
5.466 -  case [simp]: False
5.467 -  have "normalize p = (1 div unit_factor p) * p"
5.468 -    by (simp add: unit_div_commute is_unit_unit_factor)
5.469 -  also have "multiplicity \<dots> x = multiplicity p x"
5.470 -    by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
5.471 -  finally show ?thesis .
5.472 -qed simp_all
5.473 -
5.474 -lemma multiplicity_normalize_right [simp]: "multiplicity p (normalize x) = multiplicity p x"
5.475 -proof (cases "x = 0")
5.476 -  case [simp]: False
5.477 -  have "normalize x = (1 div unit_factor x) * x"
5.478 -    by (simp add: unit_div_commute is_unit_unit_factor)
5.479 -  also have "multiplicity p \<dots> = multiplicity p x"
5.480 -    by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
5.481 -  finally show ?thesis .
5.482 -qed simp_all
5.483 -
5.484  lemma prime_factorization_cong:
5.485    "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
5.486    by (simp add: multiset_eq_iff count_prime_factorization
5.487 @@ -1206,6 +1266,51 @@
5.488    finally show ?thesis .
5.489  qed
5.490
5.491 +lemma prime_elem_multiplicity_mult_distrib:
5.492 +  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
5.493 +  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
5.494 +proof -
5.495 +  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
5.496 +    by (subst count_prime_factorization_prime) (simp_all add: assms)
5.497 +  also from assms
5.498 +    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
5.499 +      by (intro prime_factorization_mult)
5.500 +  also have "count \<dots> (normalize p) =
5.501 +    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
5.502 +    by simp
5.503 +  also have "\<dots> = multiplicity p x + multiplicity p y"
5.504 +    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
5.505 +  finally show ?thesis .
5.506 +qed
5.507 +
5.508 +lemma prime_elem_multiplicity_prod_mset_distrib:
5.509 +  assumes "prime_elem p" "0 \<notin># A"
5.510 +  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
5.511 +  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
5.512 +
5.513 +lemma prime_elem_multiplicity_power_distrib:
5.514 +  assumes "prime_elem p" "x \<noteq> 0"
5.515 +  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
5.516 +  using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
5.517 +  by simp
5.518 +
5.519 +lemma prime_elem_multiplicity_setprod_distrib:
5.520 +  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
5.521 +  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
5.522 +proof -
5.523 +  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
5.524 +    using assms by (subst setprod_unfold_prod_mset)
5.525 +                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib setsum_unfold_sum_mset
5.526 +                      multiset.map_comp o_def)
5.527 +  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
5.528 +    by (induction A rule: finite_induct) simp_all
5.529 +  finally show ?thesis .
5.530 +qed
5.531 +
5.532 +lemma multiplicity_distinct_prime_power:
5.533 +  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
5.534 +  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
5.535 +
5.536  lemma prime_factorization_prime_power:
5.537    "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
5.538    by (induction n)
5.539 @@ -1243,60 +1348,10 @@
5.540  lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x"
5.541    by (auto dest: in_prime_factors_imp_prime)
5.542
5.543 -
5.544 -lemma prime_elem_multiplicity_mult_distrib:
5.545 -  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
5.546 -  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
5.547 -proof -
5.548 -  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
5.549 -    by (subst count_prime_factorization_prime) (simp_all add: assms)
5.550 -  also from assms
5.551 -    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
5.552 -      by (intro prime_factorization_mult)
5.553 -  also have "count \<dots> (normalize p) =
5.554 -    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
5.555 -    by simp
5.556 -  also have "\<dots> = multiplicity p x + multiplicity p y"
5.557 -    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
5.558 -  finally show ?thesis .
5.559 -qed
5.560 -
5.561 -lemma prime_elem_multiplicity_power_distrib:
5.562 -  assumes "prime_elem p" "x \<noteq> 0"
5.563 -  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
5.564 -  by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
5.565 -
5.566 -lemma prime_elem_multiplicity_prod_mset_distrib:
5.567 -  assumes "prime_elem p" "0 \<notin># A"
5.568 -  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
5.569 -  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
5.570 -
5.571 -lemma prime_elem_multiplicity_setprod_distrib:
5.572 -  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
5.573 -  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
5.574 -proof -
5.575 -  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
5.576 -    using assms by (subst setprod_unfold_prod_mset)
5.577 -                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib setsum_unfold_sum_mset
5.578 -                      multiset.map_comp o_def)
5.579 -  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
5.580 -    by (induction A rule: finite_induct) simp_all
5.581 -  finally show ?thesis .
5.582 -qed
5.583 -
5.584 -lemma prime_factorsI:
5.585 -  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
5.586 -  by (auto simp: in_prime_factors_iff)
5.587 -
5.588  lemma prime_prime_factors:
5.589    "prime p \<Longrightarrow> prime_factors p = {p}"
5.590    by (drule prime_factorization_prime) simp
5.591
5.592 -lemma prime_factors_altdef_multiplicity:
5.593 -  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
5.594 -  by (cases "n = 0")
5.595 -     (auto simp: prime_multiplicity_gt_zero_iff in_prime_factors_iff)
5.596 -
5.597  lemma setprod_prime_factors:
5.598    assumes "x \<noteq> 0"
5.599    shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
5.600 @@ -1311,13 +1366,6 @@
5.601    finally show ?thesis ..
5.602  qed
5.603
5.604 -(* TODO Move *)
5.605 -lemma (in semidom) setprod_zero_iff [simp]:
5.606 -  assumes "finite A"
5.607 -  shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
5.608 -  using assms by (induct A) (auto simp: no_zero_divisors)
5.609 -(* END TODO *)
5.610 -
5.611  lemma prime_factorization_unique'':
5.612    assumes S_eq: "S = {p. 0 < f p}"
5.613      and "finite S"
5.614 @@ -1360,29 +1408,10 @@
5.615    qed
5.616  qed
5.617
5.618 -lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
5.619 -  by (rule multiplicity_self) auto
5.620 -
5.621 -lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
5.622 -  by (subst multiplicity_same_power') auto
5.623 -
5.624  lemma prime_factors_product:
5.625    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
5.627
5.628 -lemma multiplicity_distinct_prime_power:
5.629 -  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
5.630 -  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
5.631 -
5.632 -lemma dvd_imp_multiplicity_le:
5.633 -  assumes "a dvd b" "b \<noteq> 0"
5.634 -  shows   "multiplicity p a \<le> multiplicity p b"
5.635 -proof (cases "is_unit p")
5.636 -  case False
5.637 -  with assms show ?thesis
5.638 -    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
5.639 -qed (insert assms, auto simp: multiplicity_unit_left)
5.640 -
5.641  lemma dvd_prime_factors [intro]:
5.642    "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
5.643    by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
5.644 @@ -1402,9 +1431,6 @@
5.645    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
5.646    by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
5.647
5.648 -lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
5.649 -  by (auto intro: prime_factorsI)
5.650 -
5.651  lemma multiplicity_eq_imp_eq:
5.652    assumes "x \<noteq> 0" "y \<noteq> 0"
5.653    assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
5.654 @@ -1438,6 +1464,8 @@
5.655  qed
5.656
5.657
5.658 +subsection \<open>GCD and LCM computation with unique factorizations\<close>
5.659 +
5.660  definition "gcd_factorial a b = (if a = 0 then normalize b
5.661       else if b = 0 then normalize a
5.662       else prod_mset (prime_factorization a \<inter># prime_factorization b))"
5.663 @@ -1674,73 +1702,6 @@
5.664
5.665  end
5.666
5.667 -lemma (in normalization_semidom) factorial_semiring_altI_aux:
5.668 -  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
5.669 -  assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
5.670 -  assumes "(x::'a) \<noteq> 0"
5.671 -  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
5.672 -using \<open>x \<noteq> 0\<close>
5.673 -proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
5.674 -  case (less a)
5.675 -  let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
5.676 -  show ?case
5.677 -  proof (cases "is_unit a")
5.678 -    case True
5.679 -    thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
5.680 -  next
5.681 -    case False
5.682 -    show ?thesis
5.683 -    proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
5.684 -      case False
5.685 -      with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
5.686 -      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
5.687 -      thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
5.688 -    next
5.689 -      case True
5.690 -      then guess b by (elim exE conjE) note b = this
5.691 -
5.692 -      from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
5.693 -      moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
5.694 -      hence "?fctrs b \<noteq> ?fctrs a" by blast
5.695 -      ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
5.696 -      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
5.697 -        by (rule psubset_card_mono)
5.698 -      moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
5.699 -      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
5.700 -        by (intro less) auto
5.701 -      then guess A .. note A = this
5.702 -
5.703 -      define c where "c = a div b"
5.704 -      from b have c: "a = b * c" by (simp add: c_def)
5.705 -      from less.prems c have "c \<noteq> 0" by auto
5.706 -      from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
5.707 -      moreover have "normalize a \<notin> ?fctrs c"
5.708 -      proof safe
5.709 -        assume "normalize a dvd c"
5.710 -        hence "b * c dvd 1 * c" by (simp add: c)
5.711 -        hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
5.712 -        with b show False by simp
5.713 -      qed
5.714 -      with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
5.715 -      ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
5.716 -      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
5.717 -        by (rule psubset_card_mono)
5.718 -      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
5.719 -        by (intro less) auto
5.720 -      then guess B .. note B = this
5.721 -
5.722 -      from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
5.723 -    qed
5.724 -  qed
5.725 -qed
5.726 -
5.727 -lemma factorial_semiring_altI:
5.728 -  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
5.729 -  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
5.730 -  shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
5.731 -  by intro_classes (rule factorial_semiring_altI_aux[OF assms])
5.732 -
5.733 -
5.734  class factorial_semiring_gcd = factorial_semiring + gcd + Gcd +
5.735    assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b"
5.736    and     lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b"
5.737 @@ -1846,7 +1807,6 @@
5.738
5.739  end
5.740
5.741 -
5.742  class factorial_ring_gcd = factorial_semiring_gcd + idom
5.743  begin
5.744
```
```     6.1 --- a/src/HOL/Power.thy	Tue Sep 20 14:51:58 2016 +0200
6.2 +++ b/src/HOL/Power.thy	Sun Sep 18 17:57:55 2016 +0200
6.3 @@ -297,6 +297,25 @@
6.4  lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
6.5    by (induct n) (auto simp add: is_unit_mult_iff)
6.6
6.7 +lemma dvd_power_iff:
6.8 +  assumes "x \<noteq> 0"
6.9 +  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
6.10 +proof
6.11 +  assume *: "x ^ m dvd x ^ n"
6.12 +  {
6.13 +    assume "m > n"
6.14 +    note *
6.15 +    also have "x ^ n = x ^ n * 1" by simp
6.16 +    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
6.17 +    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
6.18 +    finally have "x ^ (m - n) dvd 1"
6.19 +      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
6.20 +    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
6.21 +  }
6.22 +  thus "is_unit x \<or> m \<le> n" by force
6.23 +qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
6.24 +
6.25 +
6.26  end
6.27
6.28  context normalization_semidom
```
```     7.1 --- a/src/HOL/Rings.thy	Tue Sep 20 14:51:58 2016 +0200
7.2 +++ b/src/HOL/Rings.thy	Sun Sep 18 17:57:55 2016 +0200
7.3 @@ -862,6 +862,9 @@
7.4    then show "a * b dvd c" by (rule dvdI)
7.5  qed
7.6
7.7 +lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
7.8 +  using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
7.9 +
7.10  lemma dvd_mult_unit_iff:
7.11    assumes "is_unit b"
7.12    shows "a dvd c * b \<longleftrightarrow> a dvd c"
7.13 @@ -878,14 +881,18 @@
7.14    then show "a dvd c * b" by simp
7.15  qed
7.16
7.17 +lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
7.18 +  using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
7.19 +
7.20  lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
7.21    by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
7.22
7.23  lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
7.24    by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
7.25
7.26 -lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
7.27 -  dvd_mult_unit_iff dvd_div_unit_iff  (* FIXME consider named_theorems *)
7.28 +lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
7.29 +  dvd_mult_unit_iff dvd_mult_unit_iff'
7.30 +  div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)
7.31
7.32  lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
7.33    by (erule is_unitE [of _ b]) simp
```