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.5    by (simp add: irreducible_def)
     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.453 -  from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   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.463 -  with add show ?case by (simp add: normalize_mult)
   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.648 +  from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   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.658 +  with add show ?case by (simp add: normalize_mult)
   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.876      case (add A p)
   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.883  qed (simp_all add: assms(1))
   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.907    by (simp add: multiplicity_def)
   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.930    by (simp add: multiplicity_same_power')
   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.1026    by (simp add: prime_factorization_unit)
  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.1065    by (simp add: in_prime_factorization_iff)
  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.1144    by (simp add: prime_factors_def)
  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 -