more generic algebraic lemmas
authorhaftmann
Sun Sep 18 17:57:55 2016 +0200 (2016-09-18)
changeset 63924f91766530e13
parent 63923 c9bba9dba73b
child 63925 500646ef617a
more generic algebraic lemmas
src/HOL/GCD.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Multiset.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Power.thy
src/HOL/Rings.thy
     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.414    by (simp add: in_prime_factors_iff)
   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.626    by (simp add: prime_factorization_mult)
   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