src/HOL/Number_Theory/Factorial_Ring.thy
 changeset 63633 2accfb71e33b parent 63547 00521f181510 child 63793 e68a0b651eb5
```     1.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Aug 08 14:13:14 2016 +0200
1.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Aug 08 17:47:51 2016 +0200
1.3 @@ -54,51 +54,51 @@
1.4  lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
1.6
1.7 -definition is_prime_elem :: "'a \<Rightarrow> bool" where
1.8 -  "is_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)"
1.9 +definition prime_elem :: "'a \<Rightarrow> bool" where
1.10 +  "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)"
1.11
1.12 -lemma not_is_prime_elem_zero [simp]: "\<not>is_prime_elem 0"
1.13 -  by (simp add: is_prime_elem_def)
1.14 +lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0"
1.15 +  by (simp add: prime_elem_def)
1.16
1.17 -lemma is_prime_elem_not_unit: "is_prime_elem p \<Longrightarrow> \<not>p dvd 1"
1.18 -  by (simp add: is_prime_elem_def)
1.19 +lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1"
1.20 +  by (simp add: prime_elem_def)
1.21
1.22 -lemma is_prime_elemI:
1.23 -    "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> is_prime_elem p"
1.24 -  by (simp add: is_prime_elem_def)
1.25 +lemma prime_elemI:
1.26 +    "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"
1.27 +  by (simp add: prime_elem_def)
1.28
1.29 -lemma prime_divides_productD:
1.30 -    "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
1.31 -  by (simp add: is_prime_elem_def)
1.32 +lemma prime_elem_dvd_multD:
1.33 +    "prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
1.34 +  by (simp add: prime_elem_def)
1.35
1.36 -lemma prime_dvd_mult_iff:
1.37 -  "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
1.38 -  by (auto simp: is_prime_elem_def)
1.39 +lemma prime_elem_dvd_mult_iff:
1.40 +  "prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
1.41 +  by (auto simp: prime_elem_def)
1.42
1.43 -lemma not_is_prime_elem_one [simp]:
1.44 -  "\<not> is_prime_elem 1"
1.45 -  by (auto dest: is_prime_elem_not_unit)
1.46 +lemma not_prime_elem_one [simp]:
1.47 +  "\<not> prime_elem 1"
1.48 +  by (auto dest: prime_elem_not_unit)
1.49
1.50 -lemma is_prime_elem_not_zeroI:
1.51 -  assumes "is_prime_elem p"
1.52 +lemma prime_elem_not_zeroI:
1.53 +  assumes "prime_elem p"
1.54    shows "p \<noteq> 0"
1.55    using assms by (auto intro: ccontr)
1.56
1.57
1.58 -lemma is_prime_elem_dvd_power:
1.59 -  "is_prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
1.60 -  by (induction n) (auto dest: prime_divides_productD intro: dvd_trans[of _ 1])
1.61 +lemma prime_elem_dvd_power:
1.62 +  "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
1.63 +  by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
1.64
1.65 -lemma is_prime_elem_dvd_power_iff:
1.66 -  "is_prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
1.67 -  by (auto dest: is_prime_elem_dvd_power intro: dvd_trans)
1.68 +lemma prime_elem_dvd_power_iff:
1.69 +  "prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
1.70 +  by (auto dest: prime_elem_dvd_power intro: dvd_trans)
1.71
1.72 -lemma is_prime_elem_imp_nonzero [simp]:
1.73 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
1.74 -  unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
1.75 +lemma prime_elem_imp_nonzero [simp]:
1.76 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0"
1.77 +  unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
1.78
1.79 -lemma is_prime_elem_imp_not_one [simp]:
1.80 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 1"
1.81 +lemma prime_elem_imp_not_one [simp]:
1.82 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1"
1.83    unfolding ASSUMPTION_def by auto
1.84
1.85  end
1.86 @@ -110,42 +110,42 @@
1.87  lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
1.88    by (subst mult.commute) (rule mult_unit_dvd_iff)
1.89
1.90 -lemma prime_imp_irreducible:
1.91 -  assumes "is_prime_elem p"
1.92 +lemma prime_elem_imp_irreducible:
1.93 +  assumes "prime_elem p"
1.94    shows   "irreducible p"
1.95  proof (rule irreducibleI)
1.96    fix a b
1.97    assume p_eq: "p = a * b"
1.98    with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
1.99    from p_eq have "p dvd a * b" by simp
1.100 -  with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
1.101 +  with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
1.102    with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
1.103    thus "a dvd 1 \<or> b dvd 1"
1.104      by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
1.105 -qed (insert assms, simp_all add: is_prime_elem_def)
1.106 +qed (insert assms, simp_all add: prime_elem_def)
1.107
1.108 -lemma is_prime_elem_mono:
1.109 -  assumes "is_prime_elem p" "\<not>q dvd 1" "q dvd p"
1.110 -  shows   "is_prime_elem q"
1.111 +lemma prime_elem_mono:
1.112 +  assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
1.113 +  shows   "prime_elem q"
1.114  proof -
1.115    from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
1.116    hence "p dvd q * r" by simp
1.117 -  with \<open>is_prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_divides_productD)
1.118 +  with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD)
1.119    hence "p dvd q"
1.120    proof
1.121      assume "p dvd r"
1.122      then obtain s where s: "r = p * s" by (elim dvdE)
1.123      from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
1.124 -    with \<open>is_prime_elem p\<close> have "q dvd 1"
1.125 +    with \<open>prime_elem p\<close> have "q dvd 1"
1.126        by (subst (asm) mult_cancel_left) auto
1.127      with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
1.128    qed
1.129
1.130    show ?thesis
1.131 -  proof (rule is_prime_elemI)
1.132 +  proof (rule prime_elemI)
1.133      fix a b assume "q dvd (a * b)"
1.134      with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
1.135 -    with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
1.136 +    with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
1.137      with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
1.138    qed (insert assms, auto)
1.139  qed
1.140 @@ -178,12 +178,12 @@
1.141    "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)"
1.142    using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
1.143
1.144 -lemma is_prime_elem_multD:
1.145 -  assumes "is_prime_elem (a * b)"
1.146 +lemma prime_elem_multD:
1.147 +  assumes "prime_elem (a * b)"
1.148    shows "is_unit a \<or> is_unit b"
1.149  proof -
1.150 -  from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: is_prime_elem_not_zeroI)
1.151 -  moreover from assms prime_divides_productD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
1.152 +  from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI)
1.153 +  moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
1.154      by auto
1.155    ultimately show ?thesis
1.156      using dvd_times_left_cancel_iff [of a b 1]
1.157 @@ -191,36 +191,62 @@
1.158      by auto
1.159  qed
1.160
1.161 -lemma is_prime_elemD2:
1.162 -  assumes "is_prime_elem p" and "a dvd p" and "\<not> is_unit a"
1.163 +lemma prime_elemD2:
1.164 +  assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a"
1.165    shows "p dvd a"
1.166  proof -
1.167    from \<open>a dvd p\<close> obtain b where "p = a * b" ..
1.168 -  with \<open>is_prime_elem p\<close> is_prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
1.169 +  with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
1.170    with \<open>p = a * b\<close> show ?thesis
1.171      by (auto simp add: mult_unit_dvd_iff)
1.172  qed
1.173
1.174 +lemma prime_elem_dvd_msetprodE:
1.175 +  assumes "prime_elem p"
1.176 +  assumes dvd: "p dvd msetprod A"
1.177 +  obtains a where "a \<in># A" and "p dvd a"
1.178 +proof -
1.179 +  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
1.180 +  proof (induct A)
1.181 +    case empty then show ?case
1.182 +    using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
1.183 +  next
1.184 +    case (add A a)
1.185 +    then have "p dvd msetprod A * a" by simp
1.186 +    with \<open>prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
1.187 +      by (blast dest: prime_elem_dvd_multD)
1.188 +    then show ?case proof cases
1.189 +      case B then show ?thesis by auto
1.190 +    next
1.191 +      case A
1.192 +      with add.hyps obtain b where "b \<in># A" "p dvd b"
1.193 +        by auto
1.194 +      then show ?thesis by auto
1.195 +    qed
1.196 +  qed
1.197 +  with that show thesis by blast
1.198 +qed
1.199 +
1.200  context
1.201  begin
1.202
1.203 -private lemma is_prime_elem_powerD:
1.204 -  assumes "is_prime_elem (p ^ n)"
1.205 -  shows   "is_prime_elem p \<and> n = 1"
1.206 +private lemma prime_elem_powerD:
1.207 +  assumes "prime_elem (p ^ n)"
1.208 +  shows   "prime_elem p \<and> n = 1"
1.209  proof (cases n)
1.210    case (Suc m)
1.211    note assms
1.212    also from Suc have "p ^ n = p * p^m" by simp
1.213 -  finally have "is_unit p \<or> is_unit (p^m)" by (rule is_prime_elem_multD)
1.214 -  moreover from assms have "\<not>is_unit p" by (simp add: is_prime_elem_def is_unit_power_iff)
1.215 +  finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD)
1.216 +  moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
1.217    ultimately have "is_unit (p ^ m)" by simp
1.218    with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
1.219    with Suc assms show ?thesis by simp
1.220  qed (insert assms, simp_all)
1.221
1.222 -lemma is_prime_elem_power_iff:
1.223 -  "is_prime_elem (p ^ n) \<longleftrightarrow> is_prime_elem p \<and> n = 1"
1.224 -  by (auto dest: is_prime_elem_powerD)
1.225 +lemma prime_elem_power_iff:
1.226 +  "prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1"
1.227 +  by (auto dest: prime_elem_powerD)
1.228
1.229  end
1.230
1.231 @@ -229,17 +255,17 @@
1.232    by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
1.233          mult_unit_dvd_iff dvd_mult_unit_iff)
1.234
1.235 -lemma is_prime_elem_mult_unit_left:
1.236 -  "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
1.237 -  by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
1.238 +lemma prime_elem_mult_unit_left:
1.239 +  "is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p"
1.240 +  by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
1.241
1.242 -lemma prime_dvd_cases:
1.243 -  assumes pk: "p*k dvd m*n" and p: "is_prime_elem p"
1.244 +lemma prime_elem_dvd_cases:
1.245 +  assumes pk: "p*k dvd m*n" and p: "prime_elem p"
1.246    shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
1.247  proof -
1.248    have "p dvd m*n" using dvd_mult_left pk by blast
1.249    then consider "p dvd m" | "p dvd n"
1.250 -    using p prime_dvd_mult_iff by blast
1.251 +    using p prime_elem_dvd_mult_iff by blast
1.252    then show ?thesis
1.253    proof cases
1.254      case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
1.255 @@ -254,8 +280,8 @@
1.256    qed
1.257  qed
1.258
1.259 -lemma prime_power_dvd_prod:
1.260 -  assumes pc: "p^c dvd m*n" and p: "is_prime_elem p"
1.261 +lemma prime_elem_power_dvd_prod:
1.262 +  assumes pc: "p^c dvd m*n" and p: "prime_elem p"
1.263    shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
1.264  using pc
1.265  proof (induct c arbitrary: m n)
1.266 @@ -263,7 +289,7 @@
1.267  next
1.268    case (Suc c)
1.269    consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
1.270 -    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
1.271 +    using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
1.272    then show ?case
1.273    proof cases
1.274      case (1 x)
1.275 @@ -284,217 +310,40 @@
1.276  lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
1.277    by arith
1.278
1.279 -lemma prime_power_dvd_cases:
1.280 -     "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
1.281 -  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
1.282 -
1.283 -end
1.284 -
1.285 -context normalization_semidom
1.286 -begin
1.287 -
1.288 -lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
1.289 -  using irreducible_mult_unit_left[of "1 div unit_factor x" x]
1.290 -  by (cases "x = 0") (simp_all add: unit_div_commute)
1.291 -
1.292 -lemma is_prime_elem_normalize_iff [simp]: "is_prime_elem (normalize x) = is_prime_elem x"
1.293 -  using is_prime_elem_mult_unit_left[of "1 div unit_factor x" x]
1.294 -  by (cases "x = 0") (simp_all add: unit_div_commute)
1.295 -
1.296 -definition is_prime :: "'a \<Rightarrow> bool" where
1.297 -  "is_prime p \<longleftrightarrow> is_prime_elem p \<and> normalize p = p"
1.298 -
1.299 -lemma not_is_prime_0 [simp]: "\<not>is_prime 0" by (simp add: is_prime_def)
1.300 -
1.301 -lemma not_is_prime_unit: "is_unit x \<Longrightarrow> \<not>is_prime x"
1.302 -  using is_prime_elem_not_unit[of x] by (auto simp add: is_prime_def)
1.303 -
1.304 -lemma not_is_prime_1 [simp]: "\<not>is_prime 1" by (simp add: not_is_prime_unit)
1.305 -
1.306 -lemma is_primeI: "is_prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> is_prime x"
1.307 -  by (simp add: is_prime_def)
1.308 -
1.309 -lemma prime_imp_prime_elem [dest]: "is_prime p \<Longrightarrow> is_prime_elem p"
1.310 -  by (simp add: is_prime_def)
1.311 -
1.312 -lemma normalize_is_prime: "is_prime p \<Longrightarrow> normalize p = p"
1.313 -  by (simp add: is_prime_def)
1.314 -
1.315 -lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
1.316 -  by (auto simp add: is_prime_def)
1.317 -
1.318 -lemma is_prime_power_iff:
1.319 -  "is_prime (p ^ n) \<longleftrightarrow> is_prime p \<and> n = 1"
1.320 -  by (auto simp: is_prime_def is_prime_elem_power_iff)
1.321 -
1.322 -lemma is_prime_elem_not_unit' [simp]:
1.323 -  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
1.324 -  unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
1.325 -
1.326 -lemma is_prime_imp_nonzero [simp]:
1.327 -  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 0"
1.328 -  unfolding ASSUMPTION_def is_prime_def by auto
1.329 -
1.330 -lemma is_prime_imp_not_one [simp]:
1.331 -  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 1"
1.332 -  unfolding ASSUMPTION_def by auto
1.333 -
1.334 -lemma is_prime_not_unit' [simp]:
1.335 -  "ASSUMPTION (is_prime x) \<Longrightarrow> \<not>is_unit x"
1.336 -  unfolding ASSUMPTION_def is_prime_def by auto
1.337 -
1.338 -lemma is_prime_normalize' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> normalize x = x"
1.339 -  unfolding ASSUMPTION_def is_prime_def by simp
1.340 -
1.341 -lemma unit_factor_is_prime: "is_prime x \<Longrightarrow> unit_factor x = 1"
1.342 -  using unit_factor_normalize[of x] unfolding is_prime_def by auto
1.343 -
1.344 -lemma unit_factor_is_prime' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> unit_factor x = 1"
1.345 -  unfolding ASSUMPTION_def by (rule unit_factor_is_prime)
1.346 -
1.347 -lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> is_prime_elem x"
1.348 -  by (simp add: is_prime_def ASSUMPTION_def)
1.349 -
1.350 - lemma is_prime_elem_associated:
1.351 -  assumes "is_prime_elem p" and "is_prime_elem q" and "q dvd p"
1.352 -  shows "normalize q = normalize p"
1.353 -using \<open>q dvd p\<close> proof (rule associatedI)
1.354 -  from \<open>is_prime_elem q\<close> have "\<not> is_unit q"
1.355 -    by (simp add: is_prime_elem_not_unit)
1.356 -  with \<open>is_prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
1.357 -    by (blast intro: is_prime_elemD2)
1.358 -qed
1.359 -
1.360 -lemma is_prime_dvd_multD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
1.361 -  by (intro prime_divides_productD) simp_all
1.362 -
1.363 -lemma is_prime_dvd_mult_iff [simp]: "is_prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
1.364 -  by (auto dest: is_prime_dvd_multD)
1.365 -
1.366 -lemma is_prime_dvd_power:
1.367 -  "is_prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
1.368 -  by (auto dest!: is_prime_elem_dvd_power simp: is_prime_def)
1.369 -
1.370 -lemma is_prime_dvd_power_iff:
1.371 -  "is_prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
1.372 -  by (intro is_prime_elem_dvd_power_iff) simp_all
1.373 +lemma prime_elem_power_dvd_cases:
1.374 +     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
1.375 +  using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem)
1.376
1.377 -lemma prime_dvd_msetprodE:
1.378 -  assumes "is_prime_elem p"
1.379 -  assumes dvd: "p dvd msetprod A"
1.380 -  obtains a where "a \<in># A" and "p dvd a"
1.381 -proof -
1.382 -  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
1.383 -  proof (induct A)
1.384 -    case empty then show ?case
1.385 -    using \<open>is_prime_elem p\<close> by (simp add: is_prime_elem_not_unit)
1.386 -  next
1.387 -    case (add A a)
1.388 -    then have "p dvd msetprod A * a" by simp
1.389 -    with \<open>is_prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
1.390 -      by (blast dest: prime_divides_productD)
1.391 -    then show ?case proof cases
1.392 -      case B then show ?thesis by auto
1.393 -    next
1.394 -      case A
1.395 -      with add.hyps obtain b where "b \<in># A" "p dvd b"
1.396 -        by auto
1.397 -      then show ?thesis by auto
1.398 -    qed
1.399 -  qed
1.400 -  with that show thesis by blast
1.401 -qed
1.402 -
1.403 -lemma msetprod_subset_imp_dvd:
1.404 -  assumes "A \<subseteq># B"
1.405 -  shows   "msetprod A dvd msetprod B"
1.406 -proof -
1.407 -  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
1.408 -  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
1.409 -  also have "msetprod A dvd \<dots>" by simp
1.410 -  finally show ?thesis .
1.411 -qed
1.412 -
1.413 -lemma prime_dvd_msetprod_iff: "is_prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
1.414 -  by (induction A) (simp_all add: prime_dvd_mult_iff prime_imp_prime_elem, blast+)
1.415 +lemma prime_elem_not_unit' [simp]:
1.416 +  "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
1.417 +  unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
1.418
1.419 -lemma primes_dvd_imp_eq:
1.420 -  assumes "is_prime p" "is_prime q" "p dvd q"
1.421 -  shows   "p = q"
1.422 -proof -
1.423 -  from assms have "irreducible q" by (simp add: prime_imp_irreducible is_prime_def)
1.424 -  from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
1.425 -  with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
1.426 -  with assms show "p = q" by simp
1.427 -qed
1.428 -
1.429 -lemma prime_dvd_msetprod_primes_iff:
1.430 -  assumes "is_prime p" "\<And>q. q \<in># A \<Longrightarrow> is_prime q"
1.431 -  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
1.432 -proof -
1.433 -  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
1.434 -  also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
1.435 -  finally show ?thesis .
1.436 -qed
1.437 -
1.438 -lemma msetprod_primes_dvd_imp_subset:
1.439 -  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
1.440 -  shows   "A \<subseteq># B"
1.441 -using assms
1.442 -proof (induction A arbitrary: B)
1.443 -  case empty
1.444 -  thus ?case by simp
1.445 -next
1.446 -  case (add A p B)
1.447 -  hence p: "is_prime p" by simp
1.448 -  define B' where "B' = B - {#p#}"
1.449 -  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
1.450 -  with add.prems have "p \<in># B"
1.451 -    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
1.452 -  hence B: "B = B' + {#p#}" by (simp add: B'_def)
1.454 -  thus ?case by (simp add: B)
1.455 -qed
1.456 -
1.457 -lemma normalize_msetprod_primes:
1.458 -  "(\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
1.459 -proof (induction A)
1.460 -  case (add A p)
1.461 -  hence "is_prime p" by simp
1.462 -  hence "normalize p = p" by simp
1.464 -qed simp_all
1.465 -
1.466 -lemma msetprod_dvd_msetprod_primes_iff:
1.467 -  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
1.468 -  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
1.469 -  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
1.470 -
1.471 -lemma prime_dvd_power_iff:
1.472 -  assumes "is_prime_elem p"
1.473 +lemma prime_elem_dvd_power_iff:
1.474 +  assumes "prime_elem p"
1.475    shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
1.476 -  using assms by (induct n) (auto dest: is_prime_elem_not_unit prime_divides_productD)
1.477 +  using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
1.478
1.479  lemma prime_power_dvd_multD:
1.480 -  assumes "is_prime_elem p"
1.481 +  assumes "prime_elem p"
1.482    assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
1.483    shows "p ^ n dvd b"
1.484 -using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
1.485 +  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close>
1.486 +proof (induct n arbitrary: b)
1.487    case 0 then show ?case by simp
1.488  next
1.489    case (Suc n) show ?case
1.490    proof (cases "n = 0")
1.491 -    case True with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
1.492 -      by (simp add: prime_dvd_mult_iff)
1.493 +    case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
1.494 +      by (simp add: prime_elem_dvd_mult_iff)
1.495    next
1.496      case False then have "n > 0" by simp
1.497 -    from \<open>is_prime_elem p\<close> have "p \<noteq> 0" by auto
1.498 +    from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto
1.499      from Suc.prems have *: "p * p ^ n dvd a * b"
1.500        by simp
1.501      then have "p dvd a * b"
1.502        by (rule dvd_mult_left)
1.503 -    with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
1.504 -      by (simp add: prime_dvd_mult_iff)
1.505 +    with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
1.506 +      by (simp add: prime_elem_dvd_mult_iff)
1.507      moreover define c where "c = b div p"
1.508      ultimately have b: "b = p * c" by simp
1.509      with * have "p * p ^ n dvd p * (a * c)"
1.510 @@ -508,6 +357,158 @@
1.511    qed
1.512  qed
1.513
1.514 +end
1.515 +
1.516 +context normalization_semidom
1.517 +begin
1.518 +
1.519 +lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
1.520 +  using irreducible_mult_unit_left[of "1 div unit_factor x" x]
1.521 +  by (cases "x = 0") (simp_all add: unit_div_commute)
1.522 +
1.523 +lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
1.524 +  using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
1.525 +  by (cases "x = 0") (simp_all add: unit_div_commute)
1.526 +
1.527 +lemma prime_elem_associated:
1.528 +  assumes "prime_elem p" and "prime_elem q" and "q dvd p"
1.529 +  shows "normalize q = normalize p"
1.530 +using \<open>q dvd p\<close> proof (rule associatedI)
1.531 +  from \<open>prime_elem q\<close> have "\<not> is_unit q"
1.532 +    by (auto simp add: prime_elem_not_unit)
1.533 +  with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
1.534 +    by (blast intro: prime_elemD2)
1.535 +qed
1.536 +
1.537 +definition prime :: "'a \<Rightarrow> bool" where
1.538 +  "prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p"
1.539 +
1.540 +lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def)
1.541 +
1.542 +lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x"
1.543 +  using prime_elem_not_unit[of x] by (auto simp add: prime_def)
1.544 +
1.545 +lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit)
1.546 +
1.547 +lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x"
1.548 +  by (simp add: prime_def)
1.549 +
1.550 +lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p"
1.551 +  by (simp add: prime_def)
1.552 +
1.553 +lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p"
1.554 +  by (simp add: prime_def)
1.555 +
1.556 +lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p"
1.557 +  by (auto simp add: prime_def)
1.558 +
1.559 +lemma prime_power_iff:
1.560 +  "prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1"
1.561 +  by (auto simp: prime_def prime_elem_power_iff)
1.562 +
1.563 +lemma prime_imp_nonzero [simp]:
1.564 +  "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0"
1.565 +  unfolding ASSUMPTION_def prime_def by auto
1.566 +
1.567 +lemma prime_imp_not_one [simp]:
1.568 +  "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1"
1.569 +  unfolding ASSUMPTION_def by auto
1.570 +
1.571 +lemma prime_not_unit' [simp]:
1.572 +  "ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x"
1.573 +  unfolding ASSUMPTION_def prime_def by auto
1.574 +
1.575 +lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x"
1.576 +  unfolding ASSUMPTION_def prime_def by simp
1.577 +
1.578 +lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1"
1.579 +  using unit_factor_normalize[of x] unfolding prime_def by auto
1.580 +
1.581 +lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1"
1.582 +  unfolding ASSUMPTION_def by (rule unit_factor_prime)
1.583 +
1.584 +lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x"
1.585 +  by (simp add: prime_def ASSUMPTION_def)
1.586 +
1.587 +lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
1.588 +  by (intro prime_elem_dvd_multD) simp_all
1.589 +
1.590 +lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
1.591 +  by (auto dest: prime_dvd_multD)
1.592 +
1.593 +lemma prime_dvd_power:
1.594 +  "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
1.595 +  by (auto dest!: prime_elem_dvd_power simp: prime_def)
1.596 +
1.597 +lemma prime_dvd_power_iff:
1.598 +  "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
1.599 +  by (subst prime_elem_dvd_power_iff) simp_all
1.600 +
1.601 +lemma msetprod_subset_imp_dvd:
1.602 +  assumes "A \<subseteq># B"
1.603 +  shows   "msetprod A dvd msetprod B"
1.604 +proof -
1.605 +  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
1.606 +  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
1.607 +  also have "msetprod A dvd \<dots>" by simp
1.608 +  finally show ?thesis .
1.609 +qed
1.610 +
1.611 +lemma prime_dvd_msetprod_iff: "prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
1.612 +  by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
1.613 +
1.614 +lemma primes_dvd_imp_eq:
1.615 +  assumes "prime p" "prime q" "p dvd q"
1.616 +  shows   "p = q"
1.617 +proof -
1.618 +  from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
1.619 +  from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
1.620 +  with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
1.621 +  with assms show "p = q" by simp
1.622 +qed
1.623 +
1.624 +lemma prime_dvd_msetprod_primes_iff:
1.625 +  assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
1.626 +  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
1.627 +proof -
1.628 +  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
1.629 +  also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
1.630 +  finally show ?thesis .
1.631 +qed
1.632 +
1.633 +lemma msetprod_primes_dvd_imp_subset:
1.634 +  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
1.635 +  shows   "A \<subseteq># B"
1.636 +using assms
1.637 +proof (induction A arbitrary: B)
1.638 +  case empty
1.639 +  thus ?case by simp
1.640 +next
1.641 +  case (add A p B)
1.642 +  hence p: "prime p" by simp
1.643 +  define B' where "B' = B - {#p#}"
1.644 +  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
1.645 +  with add.prems have "p \<in># B"
1.646 +    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
1.647 +  hence B: "B = B' + {#p#}" by (simp add: B'_def)
1.649 +  thus ?case by (simp add: B)
1.650 +qed
1.651 +
1.652 +lemma normalize_msetprod_primes:
1.653 +  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
1.654 +proof (induction A)
1.655 +  case (add A p)
1.656 +  hence "prime p" by simp
1.657 +  hence "normalize p = p" by simp
1.659 +qed simp_all
1.660 +
1.661 +lemma msetprod_dvd_msetprod_primes_iff:
1.662 +  assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
1.663 +  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
1.664 +  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
1.665 +
1.666  lemma is_unit_msetprod_iff:
1.667    "is_unit (msetprod A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
1.668    by (induction A) (auto simp: is_unit_mult_iff)
1.669 @@ -516,7 +517,7 @@
1.670    by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
1.671
1.672  lemma is_unit_msetprod_primes_iff:
1.673 -  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
1.674 +  assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
1.675    shows   "is_unit (msetprod A) \<longleftrightarrow> A = {#}"
1.676  proof
1.677    assume unit: "is_unit (msetprod A)"
1.678 @@ -524,16 +525,16 @@
1.679    proof (intro multiset_emptyI notI)
1.680      fix x assume "x \<in># A"
1.681      with unit have "is_unit x" by (subst (asm) is_unit_msetprod_iff) blast
1.682 -    moreover from \<open>x \<in># A\<close> have "is_prime x" by (rule assms)
1.683 +    moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
1.684      ultimately show False by simp
1.685    qed
1.686  qed simp_all
1.687
1.688  lemma msetprod_primes_irreducible_imp_prime:
1.689    assumes irred: "irreducible (msetprod A)"
1.690 -  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
1.691 -  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
1.692 -  assumes C: "\<And>x. x \<in># C \<Longrightarrow> is_prime x"
1.693 +  assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
1.694 +  assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
1.695 +  assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
1.696    assumes dvd: "msetprod A dvd msetprod B * msetprod C"
1.697    shows   "msetprod A dvd msetprod B \<or> msetprod A dvd msetprod C"
1.698  proof -
1.699 @@ -564,8 +565,8 @@
1.700  qed
1.701
1.702  lemma msetprod_primes_finite_divisor_powers:
1.703 -  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
1.704 -  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
1.705 +  assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
1.706 +  assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
1.707    assumes "A \<noteq> {#}"
1.708    shows   "finite {n. msetprod A ^ n dvd msetprod B}"
1.709  proof -
1.710 @@ -594,10 +595,10 @@
1.711  context semiring_gcd
1.712  begin
1.713
1.714 -lemma irreducible_imp_prime_gcd:
1.715 +lemma irreducible_imp_prime_elem_gcd:
1.716    assumes "irreducible x"
1.717 -  shows   "is_prime_elem x"
1.718 -proof (rule is_prime_elemI)
1.719 +  shows   "prime_elem x"
1.720 +proof (rule prime_elemI)
1.721    fix a b assume "x dvd a * b"
1.722    from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
1.723    from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
1.724 @@ -605,77 +606,77 @@
1.725      by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
1.726  qed (insert assms, auto simp: irreducible_not_unit)
1.727
1.728 -lemma is_prime_elem_imp_coprime:
1.729 -  assumes "is_prime_elem p" "\<not>p dvd n"
1.730 +lemma prime_elem_imp_coprime:
1.731 +  assumes "prime_elem p" "\<not>p dvd n"
1.732    shows   "coprime p n"
1.733  proof (rule coprimeI)
1.734    fix d assume "d dvd p" "d dvd n"
1.735    show "is_unit d"
1.736    proof (rule ccontr)
1.737      assume "\<not>is_unit d"
1.738 -    from \<open>is_prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
1.739 -      by (rule is_prime_elemD2)
1.740 +    from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
1.741 +      by (rule prime_elemD2)
1.742      from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
1.743      with \<open>\<not>p dvd n\<close> show False by contradiction
1.744    qed
1.745  qed
1.746
1.747 -lemma is_prime_imp_coprime:
1.748 -  assumes "is_prime p" "\<not>p dvd n"
1.749 +lemma prime_imp_coprime:
1.750 +  assumes "prime p" "\<not>p dvd n"
1.751    shows   "coprime p n"
1.752 -  using assms by (simp add: is_prime_elem_imp_coprime)
1.753 +  using assms by (simp add: prime_elem_imp_coprime)
1.754
1.755 -lemma is_prime_elem_imp_power_coprime:
1.756 -  "is_prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.757 -  by (auto intro!: coprime_exp dest: is_prime_elem_imp_coprime simp: gcd.commute)
1.758 +lemma prime_elem_imp_power_coprime:
1.759 +  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.760 +  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
1.761
1.762 -lemma is_prime_imp_power_coprime:
1.763 -  "is_prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.764 -  by (simp add: is_prime_elem_imp_power_coprime)
1.765 +lemma prime_imp_power_coprime:
1.766 +  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.767 +  by (simp add: prime_elem_imp_power_coprime)
1.768
1.769 -lemma prime_divprod_pow:
1.770 -  assumes p: "is_prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.771 +lemma prime_elem_divprod_pow:
1.772 +  assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.773    shows   "p^n dvd a \<or> p^n dvd b"
1.774    using assms
1.775  proof -
1.776    from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
1.777 -    by (auto simp: coprime is_prime_elem_def)
1.778 +    by (auto simp: coprime prime_elem_def)
1.779    with p have "coprime (p^n) a \<or> coprime (p^n) b"
1.780 -    by (auto intro: is_prime_elem_imp_coprime coprime_exp_left)
1.781 +    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
1.782    with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
1.783  qed
1.784
1.785  lemma primes_coprime:
1.786 -  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.787 -  using is_prime_imp_coprime primes_dvd_imp_eq by blast
1.788 +  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1.789 +  using prime_imp_coprime primes_dvd_imp_eq by blast
1.790
1.791  end
1.792
1.793
1.794  class factorial_semiring = normalization_semidom +
1.795    assumes prime_factorization_exists:
1.796 -            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
1.797 +            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
1.798  begin
1.799
1.800  lemma prime_factorization_exists':
1.801    assumes "x \<noteq> 0"
1.802 -  obtains A where "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "msetprod A = normalize x"
1.803 +  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "msetprod A = normalize x"
1.804  proof -
1.805    from prime_factorization_exists[OF assms] obtain A
1.806 -    where A: "\<And>x. x \<in># A \<Longrightarrow> is_prime_elem x" "msetprod A = normalize x" by blast
1.807 +    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "msetprod A = normalize x" by blast
1.808    define A' where "A' = image_mset normalize A"
1.809    have "msetprod A' = normalize (msetprod A)"
1.810      by (simp add: A'_def normalize_msetprod)
1.811    also note A(2)
1.812    finally have "msetprod A' = normalize x" by simp
1.813 -  moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> is_prime x" by (auto simp: is_prime_def A'_def)
1.814 +  moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
1.815    ultimately show ?thesis by (intro that[of A']) blast
1.816  qed
1.817
1.818 -lemma irreducible_imp_prime:
1.819 +lemma irreducible_imp_prime_elem:
1.820    assumes "irreducible x"
1.821 -  shows   "is_prime_elem x"
1.822 -proof (rule is_prime_elemI)
1.823 +  shows   "prime_elem x"
1.824 +proof (rule prime_elemI)
1.825    fix a b assume dvd: "x dvd a * b"
1.826    from assms have "x \<noteq> 0" by auto
1.827    show "x dvd a \<or> x dvd b"
1.828 @@ -708,12 +709,12 @@
1.829
1.830  lemma finite_prime_divisors:
1.831    assumes "x \<noteq> 0"
1.832 -  shows   "finite {p. is_prime p \<and> p dvd x}"
1.833 +  shows   "finite {p. prime p \<and> p dvd x}"
1.834  proof -
1.835    from prime_factorization_exists'[OF assms] guess A . note A = this
1.836 -  have "{p. is_prime p \<and> p dvd x} \<subseteq> set_mset A"
1.837 +  have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
1.838    proof safe
1.839 -    fix p assume p: "is_prime p" and dvd: "p dvd x"
1.840 +    fix p assume p: "prime p" and dvd: "p dvd x"
1.841      from dvd have "p dvd normalize x" by simp
1.842      also from A have "normalize x = msetprod A" by simp
1.843      finally show "p \<in># A" using p A by (subst (asm) prime_dvd_msetprod_primes_iff)
1.844 @@ -722,23 +723,23 @@
1.845    ultimately show ?thesis by (rule finite_subset)
1.846  qed
1.847
1.848 -lemma prime_iff_irreducible: "is_prime_elem x \<longleftrightarrow> irreducible x"
1.849 -  by (blast intro: irreducible_imp_prime prime_imp_irreducible)
1.850 +lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
1.851 +  by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
1.852
1.853  lemma prime_divisor_exists:
1.854    assumes "a \<noteq> 0" "\<not>is_unit a"
1.855 -  shows   "\<exists>b. b dvd a \<and> is_prime b"
1.856 +  shows   "\<exists>b. b dvd a \<and> prime b"
1.857  proof -
1.858    from prime_factorization_exists'[OF assms(1)] guess A . note A = this
1.859    moreover from A and assms have "A \<noteq> {#}" by auto
1.860    then obtain x where "x \<in># A" by blast
1.861 -  with A(1) have *: "x dvd msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
1.862 +  with A(1) have *: "x dvd msetprod A" "prime x" by (auto simp: dvd_msetprod)
1.863    with A have "x dvd a" by simp
1.864    with * show ?thesis by blast
1.865  qed
1.866
1.867  lemma prime_divisors_induct [case_names zero unit factor]:
1.868 -  assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
1.869 +  assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
1.870    shows   "P x"
1.871  proof (cases "x = 0")
1.872    case False
1.873 @@ -746,7 +747,7 @@
1.874    from A(1) have "P (unit_factor x * msetprod A)"
1.875    proof (induction A)
1.877 -    from add.prems have "is_prime p" by simp
1.878 +    from add.prems have "prime p" by simp
1.879      moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
1.880      ultimately have "P (p * (unit_factor x * msetprod A))" by (rule assms(3))
1.881      thus ?case by (simp add: mult_ac)
1.882 @@ -755,18 +756,18 @@
1.884
1.885  lemma no_prime_divisors_imp_unit:
1.886 -  assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime_elem b"
1.887 +  assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b"
1.888    shows "is_unit a"
1.889  proof (rule ccontr)
1.890    assume "\<not>is_unit a"
1.891    from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
1.892 -  with assms(2)[of b] show False by (simp add: is_prime_def)
1.893 +  with assms(2)[of b] show False by (simp add: prime_def)
1.894  qed
1.895
1.896  lemma prime_divisorE:
1.897    assumes "a \<noteq> 0" and "\<not> is_unit a"
1.898 -  obtains p where "is_prime p" and "p dvd a"
1.899 -  using assms no_prime_divisors_imp_unit unfolding is_prime_def by blast
1.900 +  obtains p where "prime p" and "p dvd a"
1.901 +  using assms no_prime_divisors_imp_unit unfolding prime_def by blast
1.902
1.903  definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
1.904    "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
1.905 @@ -864,17 +865,17 @@
1.906  lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
1.908
1.909 -lemma prime_multiplicity_eq_zero_iff:
1.910 -  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
1.911 +lemma prime_elem_multiplicity_eq_zero_iff:
1.912 +  "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
1.913    by (rule multiplicity_eq_zero_iff) simp_all
1.914
1.915  lemma prime_multiplicity_other:
1.916 -  assumes "is_prime p" "is_prime q" "p \<noteq> q"
1.917 +  assumes "prime p" "prime q" "p \<noteq> q"
1.918    shows   "multiplicity p q = 0"
1.919 -  using assms by (subst prime_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
1.920 +  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
1.921
1.922  lemma prime_multiplicity_gt_zero_iff:
1.923 -  "is_prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
1.924 +  "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
1.925    by (rule multiplicity_gt_zero_iff) simp_all
1.926
1.927  lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
1.928 @@ -943,8 +944,8 @@
1.929    "p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
1.931
1.932 -lemma multiplicity_prime_times_other:
1.933 -  assumes "is_prime_elem p" "\<not>p dvd q"
1.934 +lemma multiplicity_prime_elem_times_other:
1.935 +  assumes "prime_elem p" "\<not>p dvd q"
1.936    shows   "multiplicity p (q * x) = multiplicity p x"
1.937  proof (cases "x = 0")
1.938    case False
1.939 @@ -959,38 +960,38 @@
1.940      from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
1.941      from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
1.942      also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
1.943 -    also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_dvd_mult_iff) fact+
1.944 +    also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
1.945      also from assms y have "\<dots> \<longleftrightarrow> False" by simp
1.946      finally show "\<not>(p ^ Suc n dvd q * x)" by blast
1.947    qed
1.948  qed simp_all
1.949
1.950  lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
1.951 -  "\<lambda>x p. if is_prime p then multiplicity p x else 0"
1.952 +  "\<lambda>x p. if prime p then multiplicity p x else 0"
1.953    unfolding multiset_def
1.954  proof clarify
1.955    fix x :: 'a
1.956 -  show "finite {p. 0 < (if is_prime p then multiplicity p x else 0)}" (is "finite ?A")
1.957 +  show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
1.958    proof (cases "x = 0")
1.959      case False
1.960 -    from False have "?A \<subseteq> {p. is_prime p \<and> p dvd x}"
1.961 +    from False have "?A \<subseteq> {p. prime p \<and> p dvd x}"
1.962        by (auto simp: multiplicity_gt_zero_iff)
1.963 -    moreover from False have "finite {p. is_prime p \<and> p dvd x}"
1.964 +    moreover from False have "finite {p. prime p \<and> p dvd x}"
1.965        by (rule finite_prime_divisors)
1.966      ultimately show ?thesis by (rule finite_subset)
1.967    qed simp_all
1.968  qed
1.969
1.970  lemma count_prime_factorization_nonprime:
1.971 -  "\<not>is_prime p \<Longrightarrow> count (prime_factorization x) p = 0"
1.972 +  "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
1.973    by transfer simp
1.974
1.975  lemma count_prime_factorization_prime:
1.976 -  "is_prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
1.977 +  "prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
1.978    by transfer simp
1.979
1.980  lemma count_prime_factorization:
1.981 -  "count (prime_factorization x) p = (if is_prime p then multiplicity p x else 0)"
1.982 +  "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
1.983    by transfer simp
1.984
1.985  lemma unit_imp_no_irreducible_divisors:
1.986 @@ -999,9 +1000,9 @@
1.987    using assms dvd_unit_imp_unit irreducible_not_unit by blast
1.988
1.989  lemma unit_imp_no_prime_divisors:
1.990 -  assumes "is_unit x" "is_prime_elem p"
1.991 +  assumes "is_unit x" "prime_elem p"
1.992    shows   "\<not>p dvd x"
1.993 -  using unit_imp_no_irreducible_divisors[OF assms(1) prime_imp_irreducible[OF assms(2)]] .
1.994 +  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
1.995
1.996  lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
1.997    by (simp add: multiset_eq_iff count_prime_factorization)
1.998 @@ -1013,7 +1014,7 @@
1.999    {
1.1000      assume x: "x \<noteq> 0" "\<not>is_unit x"
1.1001      {
1.1002 -      fix p assume p: "is_prime p"
1.1003 +      fix p assume p: "prime p"
1.1004        have "count (prime_factorization x) p = 0" by (simp add: *)
1.1005        also from p have "count (prime_factorization x) p = multiplicity p x"
1.1006          by (rule count_prime_factorization_prime)
1.1007 @@ -1029,7 +1030,7 @@
1.1008    proof
1.1009      assume x: "is_unit x"
1.1010      {
1.1011 -      fix p assume p: "is_prime p"
1.1012 +      fix p assume p: "prime p"
1.1013        from p x have "multiplicity p x = 0"
1.1014          by (subst multiplicity_eq_zero_iff)
1.1015             (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
1.1016 @@ -1044,7 +1045,7 @@
1.1017  proof (rule multiset_eqI)
1.1018    fix p :: 'a
1.1019    show "count (prime_factorization x) p = count {#} p"
1.1020 -  proof (cases "is_prime p")
1.1021 +  proof (cases "prime p")
1.1022      case True
1.1023      with assms have "multiplicity p x = 0"
1.1024        by (subst multiplicity_eq_zero_iff)
1.1025 @@ -1057,17 +1058,17 @@
1.1027
1.1028  lemma prime_factorization_times_prime:
1.1029 -  assumes "x \<noteq> 0" "is_prime p"
1.1030 +  assumes "x \<noteq> 0" "prime p"
1.1031    shows   "prime_factorization (p * x) = {#p#} + prime_factorization x"
1.1032  proof (rule multiset_eqI)
1.1033    fix q :: 'a
1.1034 -  consider "\<not>is_prime q" | "p = q" | "is_prime q" "p \<noteq> q" by blast
1.1035 +  consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast
1.1036    thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
1.1037    proof cases
1.1038 -    assume q: "is_prime q" "p \<noteq> q"
1.1039 +    assume q: "prime q" "p \<noteq> q"
1.1040      with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
1.1041      with q assms show ?thesis
1.1042 -      by (simp add: multiplicity_prime_times_other count_prime_factorization)
1.1043 +      by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
1.1044    qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
1.1045  qed
1.1046
1.1047 @@ -1080,17 +1081,17 @@
1.1048                      is_unit_normalize normalize_mult)
1.1049
1.1050  lemma in_prime_factorization_iff:
1.1051 -  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
1.1052 +  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
1.1053  proof -
1.1054    have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
1.1055 -  also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
1.1056 +  also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
1.1057     by (subst count_prime_factorization, cases "x = 0")
1.1058        (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
1.1059    finally show ?thesis .
1.1060  qed
1.1061
1.1062  lemma in_prime_factorization_imp_prime:
1.1063 -  "p \<in># prime_factorization x \<Longrightarrow> is_prime p"
1.1064 +  "p \<in># prime_factorization x \<Longrightarrow> prime p"
1.1066
1.1067  lemma in_prime_factorization_imp_dvd:
1.1068 @@ -1111,18 +1112,18 @@
1.1069  qed
1.1070
1.1071  lemma prime_factorization_prime:
1.1072 -  assumes "is_prime p"
1.1073 +  assumes "prime p"
1.1074    shows   "prime_factorization p = {#p#}"
1.1075  proof (rule multiset_eqI)
1.1076    fix q :: 'a
1.1077 -  consider "\<not>is_prime q" | "q = p" | "is_prime q" "q \<noteq> p" by blast
1.1078 +  consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast
1.1079    thus "count (prime_factorization p) q = count {#p#} q"
1.1080      by cases (insert assms, auto dest: primes_dvd_imp_eq
1.1081                  simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
1.1082  qed
1.1083
1.1084  lemma prime_factorization_msetprod_primes:
1.1085 -  assumes "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
1.1086 +  assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
1.1087    shows   "prime_factorization (msetprod A) = A"
1.1088    using assms
1.1089  proof (induction A)
1.1090 @@ -1204,7 +1205,7 @@
1.1091  qed
1.1092
1.1093  lemma prime_factorization_prime_power:
1.1094 -  "is_prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
1.1095 +  "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
1.1096    by (induction n)
1.1097       (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
1.1098
1.1099 @@ -1242,8 +1243,8 @@
1.1100    by (auto dest: in_prime_factorization_imp_prime)
1.1101
1.1102
1.1103 -lemma prime_multiplicity_mult_distrib:
1.1104 -  assumes "is_prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
1.1105 +lemma prime_elem_multiplicity_mult_distrib:
1.1106 +  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
1.1107    shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
1.1108  proof -
1.1109    have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
1.1110 @@ -1259,23 +1260,23 @@
1.1111    finally show ?thesis .
1.1112  qed
1.1113
1.1114 -lemma prime_multiplicity_power_distrib:
1.1115 -  assumes "is_prime_elem p" "x \<noteq> 0"
1.1116 +lemma prime_elem_multiplicity_power_distrib:
1.1117 +  assumes "prime_elem p" "x \<noteq> 0"
1.1118    shows   "multiplicity p (x ^ n) = n * multiplicity p x"
1.1119 -  by (induction n) (simp_all add: assms prime_multiplicity_mult_distrib)
1.1120 +  by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
1.1121
1.1122 -lemma prime_multiplicity_msetprod_distrib:
1.1123 -  assumes "is_prime_elem p" "0 \<notin># A"
1.1124 +lemma prime_elem_multiplicity_msetprod_distrib:
1.1125 +  assumes "prime_elem p" "0 \<notin># A"
1.1126    shows   "multiplicity p (msetprod A) = msetsum (image_mset (multiplicity p) A)"
1.1127 -  using assms by (induction A) (auto simp: prime_multiplicity_mult_distrib)
1.1128 +  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
1.1129
1.1130 -lemma prime_multiplicity_setprod_distrib:
1.1131 -  assumes "is_prime_elem p" "0 \<notin> f ` A" "finite A"
1.1132 +lemma prime_elem_multiplicity_setprod_distrib:
1.1133 +  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
1.1134    shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
1.1135  proof -
1.1136    have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
1.1137      using assms by (subst setprod_unfold_msetprod)
1.1138 -                   (simp_all add: prime_multiplicity_msetprod_distrib setsum_unfold_msetsum
1.1139 +                   (simp_all add: prime_elem_multiplicity_msetprod_distrib setsum_unfold_msetsum
1.1140                        multiset.map_comp o_def)
1.1141    also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
1.1142      by (induction A rule: finite_induct) simp_all
1.1143 @@ -1292,10 +1293,10 @@
1.1145
1.1146  lemma prime_factorsI:
1.1147 -  "x \<noteq> 0 \<Longrightarrow> is_prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
1.1148 +  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
1.1149    by (auto simp: prime_factors_def in_prime_factorization_iff)
1.1150
1.1151 -lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> is_prime p"
1.1152 +lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> prime p"
1.1153    by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
1.1154
1.1155  lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
1.1156 @@ -1306,7 +1307,7 @@
1.1157    unfolding prime_factors_def by simp
1.1158
1.1159  lemma prime_factors_altdef_multiplicity:
1.1160 -  "prime_factors n = {p. is_prime p \<and> multiplicity p n > 0}"
1.1161 +  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
1.1162    by (cases "n = 0")
1.1163       (auto simp: prime_factors_def prime_multiplicity_gt_zero_iff
1.1164          prime_imp_prime_elem in_prime_factorization_iff)
1.1165 @@ -1335,8 +1336,8 @@
1.1166  lemma prime_factorization_unique'':
1.1167    assumes S_eq: "S = {p. 0 < f p}"
1.1168      and "finite S"
1.1169 -    and S: "\<forall>p\<in>S. is_prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
1.1170 -  shows "S = prime_factors n \<and> (\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
1.1171 +    and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
1.1172 +  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
1.1173  proof
1.1174    define A where "A = Abs_multiset f"
1.1175    from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
1.1176 @@ -1357,15 +1358,15 @@
1.1177      by (intro prime_factorization_msetprod_primes) (auto dest: in_prime_factorization_imp_prime)
1.1178    finally show "S = prime_factors n" by (simp add: prime_factors_def set_mset_A [symmetric])
1.1179
1.1180 -  show "(\<forall>p. is_prime p \<longrightarrow> f p = multiplicity p n)"
1.1181 +  show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
1.1182    proof safe
1.1183 -    fix p :: 'a assume p: "is_prime p"
1.1184 +    fix p :: 'a assume p: "prime p"
1.1185      have "multiplicity p n = multiplicity p (normalize n)" by simp
1.1186      also have "normalize n = msetprod A"
1.1187        by (simp add: msetprod_multiplicity S_eq set_mset_A count_A S)
1.1188      also from p set_mset_A S(1)
1.1189      have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
1.1190 -      by (intro prime_multiplicity_msetprod_distrib) auto
1.1191 +      by (intro prime_elem_multiplicity_msetprod_distrib) auto
1.1192      also from S(1) p
1.1193      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
1.1194        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
1.1195 @@ -1374,10 +1375,10 @@
1.1196    qed
1.1197  qed
1.1198
1.1199 -lemma multiplicity_prime [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p p = 1"
1.1200 +lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
1.1201    by (rule multiplicity_self) auto
1.1202
1.1203 -lemma multiplicity_prime_power [simp]: "is_prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
1.1204 +lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
1.1205    by (subst multiplicity_same_power') auto
1.1206
1.1207  lemma prime_factors_product:
1.1208 @@ -1385,8 +1386,8 @@
1.1209    by (simp add: prime_factors_def prime_factorization_mult)
1.1210
1.1211  lemma multiplicity_distinct_prime_power:
1.1212 -  "is_prime p \<Longrightarrow> is_prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
1.1213 -  by (subst prime_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
1.1214 +  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
1.1215 +  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
1.1216
1.1217  lemma dvd_imp_multiplicity_le:
1.1218    assumes "a dvd b" "b \<noteq> 0"
1.1219 @@ -1404,7 +1405,7 @@
1.1220
1.1221  (* RENAMED multiplicity_dvd *)
1.1222  lemma multiplicity_le_imp_dvd:
1.1223 -  assumes "x \<noteq> 0" "\<And>p. is_prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
1.1224 +  assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
1.1225    shows   "x dvd y"
1.1226  proof (cases "y = 0")
1.1227    case False
1.1228 @@ -1417,17 +1418,17 @@
1.1229    "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
1.1230    by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
1.1231
1.1232 -lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. is_prime p \<and> p dvd x}"
1.1233 +lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
1.1234    by (auto intro: prime_factorsI)
1.1235
1.1236  lemma multiplicity_eq_imp_eq:
1.1237    assumes "x \<noteq> 0" "y \<noteq> 0"
1.1238 -  assumes "\<And>p. is_prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.1239 +  assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
1.1240    shows   "normalize x = normalize y"
1.1241    using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
1.1242
1.1243  lemma prime_factorization_unique':
1.1244 -  assumes "\<forall>p \<in># M. is_prime p" "\<forall>p \<in># N. is_prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
1.1245 +  assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
1.1246    shows   "M = N"
1.1247  proof -
1.1248    have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
1.1249 @@ -1504,7 +1505,7 @@
1.1250    hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
1.1251      by (auto dest: mset_subset_eqD)
1.1252    with in_prime_factorization_imp_prime[of _ x]
1.1253 -    have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> is_prime p" by blast
1.1254 +    have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
1.1255    with assms show ?thesis
1.1256      by (simp add: Gcd_factorial_def prime_factorization_msetprod_primes)
1.1257  qed
1.1258 @@ -1519,7 +1520,7 @@
1.1259    finally show ?thesis by (simp add: Lcm_factorial_def)
1.1260  next
1.1261    case False
1.1262 -  have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> is_prime y"
1.1263 +  have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
1.1264      by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
1.1265    with assms False show ?thesis
1.1266      by (simp add: Lcm_factorial_def prime_factorization_msetprod_primes)
1.1267 @@ -1586,7 +1587,7 @@
1.1268    then obtain x where "x \<in> A" "x \<noteq> 0" by blast
1.1269    hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
1.1270      by (intro subset_mset.cInf_lower) auto
1.1271 -  hence "is_prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
1.1272 +  hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
1.1273      using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
1.1274    with False show ?thesis
1.1275      by (auto simp add: Gcd_factorial_def normalize_msetprod_primes)
1.1276 @@ -1692,9 +1693,9 @@
1.1277
1.1278  lemma (in normalization_semidom) factorial_semiring_altI_aux:
1.1279    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
1.1280 -  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
1.1281 +  assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
1.1282    assumes "(x::'a) \<noteq> 0"
1.1283 -  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
1.1284 +  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize x"
1.1285  using \<open>x \<noteq> 0\<close>
1.1286  proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
1.1287    case (less a)
1.1288 @@ -1709,7 +1710,7 @@
1.1289      proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
1.1290        case False
1.1291        with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
1.1292 -      hence "is_prime_elem a" by (rule irreducible_imp_prime)
1.1293 +      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
1.1294        thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
1.1295      next
1.1296        case True
1.1297 @@ -1722,7 +1723,7 @@
1.1298        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
1.1299          by (rule psubset_card_mono)
1.1300        moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
1.1301 -      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize b"
1.1302 +      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize b"
1.1303          by (intro less) auto
1.1304        then guess A .. note A = this
1.1305
1.1306 @@ -1741,7 +1742,7 @@
1.1307        ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
1.1308        with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
1.1309          by (rule psubset_card_mono)
1.1310 -      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize c"
1.1311 +      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> msetprod A = normalize c"
1.1312          by (intro less) auto
1.1313        then guess B .. note B = this
1.1314
1.1315 @@ -1752,7 +1753,7 @@
1.1316
1.1317  lemma factorial_semiring_altI:
1.1318    assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
1.1319 -  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
1.1320 +  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
1.1321    shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
1.1322    by intro_classes (rule factorial_semiring_altI_aux[OF assms])
1.1323
1.1324 @@ -1816,7 +1817,7 @@
1.1325  qed
1.1326
1.1327  lemma
1.1328 -  assumes "x \<noteq> 0" "y \<noteq> 0" "is_prime p"
1.1329 +  assumes "x \<noteq> 0" "y \<noteq> 0" "prime p"
1.1330    shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
1.1331      and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
1.1332  proof -
```