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