src/HOL/Number_Theory/Factorial_Ring.thy
author haftmann
Thu Mar 03 08:33:55 2016 +0100 (2016-03-03)
changeset 62499 4a5b81ff5992
parent 62366 95c6cf433c91
child 63040 eb4ddd18d635
permissions -rw-r--r--
constructive formulation of factorization
haftmann@60804
     1
(*  Title:      HOL/Number_Theory/Factorial_Ring.thy
haftmann@60804
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@60804
     3
*)
haftmann@60804
     4
haftmann@60804
     5
section \<open>Factorial (semi)rings\<close>
haftmann@60804
     6
haftmann@60804
     7
theory Factorial_Ring
haftmann@62499
     8
imports Main Primes "~~/src/HOL/Library/Multiset"
haftmann@62499
     9
begin
haftmann@62499
    10
haftmann@62499
    11
context algebraic_semidom
haftmann@60804
    12
begin
haftmann@60804
    13
haftmann@62499
    14
lemma dvd_mult_imp_div:
haftmann@62499
    15
  assumes "a * c dvd b"
haftmann@62499
    16
  shows "a dvd b div c"
haftmann@62499
    17
proof (cases "c = 0")
haftmann@62499
    18
  case True then show ?thesis by simp
haftmann@62499
    19
next
haftmann@62499
    20
  case False
haftmann@62499
    21
  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
haftmann@62499
    22
  with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
haftmann@62499
    23
qed
haftmann@62499
    24
haftmann@62499
    25
end
haftmann@62499
    26
haftmann@60804
    27
class factorial_semiring = normalization_semidom +
haftmann@60804
    28
  assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
haftmann@60804
    29
  fixes is_prime :: "'a \<Rightarrow> bool"
haftmann@60804
    30
  assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
haftmann@60804
    31
    and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
haftmann@62499
    32
    and no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
haftmann@60804
    33
  assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
haftmann@60804
    34
    and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
haftmann@60804
    35
begin
haftmann@60804
    36
haftmann@60804
    37
lemma not_is_prime_one [simp]:
haftmann@60804
    38
  "\<not> is_prime 1"
haftmann@60804
    39
  by (auto dest: is_prime_not_unit)
haftmann@60804
    40
haftmann@60804
    41
lemma is_prime_not_zeroI:
haftmann@60804
    42
  assumes "is_prime p"
haftmann@60804
    43
  shows "p \<noteq> 0"
haftmann@60804
    44
  using assms by (auto intro: ccontr)
haftmann@60804
    45
haftmann@60804
    46
lemma is_prime_multD:
haftmann@60804
    47
  assumes "is_prime (a * b)"
haftmann@60804
    48
  shows "is_unit a \<or> is_unit b"
haftmann@60804
    49
proof -
haftmann@60804
    50
  from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
haftmann@60804
    51
  moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
haftmann@60804
    52
    by auto
haftmann@60804
    53
  ultimately show ?thesis
haftmann@60804
    54
    using dvd_times_left_cancel_iff [of a b 1]
haftmann@60804
    55
      dvd_times_right_cancel_iff [of b a 1]
haftmann@60804
    56
    by auto
haftmann@60804
    57
qed
haftmann@60804
    58
haftmann@60804
    59
lemma is_primeD2:
haftmann@60804
    60
  assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
haftmann@60804
    61
  shows "p dvd a"
haftmann@60804
    62
proof -
haftmann@60804
    63
  from \<open>a dvd p\<close> obtain b where "p = a * b" ..
haftmann@60804
    64
  with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
haftmann@60804
    65
  with \<open>p = a * b\<close> show ?thesis
haftmann@60804
    66
    by (auto simp add: mult_unit_dvd_iff)
haftmann@60804
    67
qed
haftmann@60804
    68
haftmann@60804
    69
lemma is_prime_mult_unit_left:
haftmann@60804
    70
  assumes "is_prime p"
haftmann@60804
    71
    and "is_unit a"
haftmann@60804
    72
  shows "is_prime (a * p)"
haftmann@60804
    73
proof (rule is_primeI)
haftmann@60804
    74
  from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
haftmann@60804
    75
    by (auto simp add: is_unit_mult_iff is_prime_not_unit)
haftmann@60804
    76
  show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
haftmann@60804
    77
  proof -
haftmann@60804
    78
    from that \<open>is_unit a\<close> have "b dvd p"
haftmann@60804
    79
      using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
haftmann@60804
    80
    with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
haftmann@60804
    81
      using is_primeD2 [of p b] by auto
haftmann@60804
    82
    with \<open>is_unit a\<close> show ?thesis
haftmann@60804
    83
      using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
haftmann@60804
    84
  qed
haftmann@60804
    85
qed
haftmann@60804
    86
haftmann@60804
    87
lemma is_primeI2:
haftmann@60804
    88
  assumes "p \<noteq> 0"
haftmann@60804
    89
  assumes "\<not> is_unit p"
haftmann@60804
    90
  assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
haftmann@60804
    91
  shows "is_prime p"
haftmann@60804
    92
using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
haftmann@60804
    93
  fix a
haftmann@60804
    94
  assume "a dvd p"
haftmann@60804
    95
  then obtain b where "p = a * b" ..
haftmann@60804
    96
  with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
haftmann@60804
    97
  moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
haftmann@60804
    98
  moreover assume "\<not> is_unit a"
haftmann@60804
    99
  ultimately show "p dvd a"
haftmann@60804
   100
    using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
haftmann@60804
   101
qed    
haftmann@60804
   102
haftmann@60804
   103
lemma not_is_prime_divisorE:
haftmann@60804
   104
  assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
haftmann@60804
   105
  obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
haftmann@60804
   106
proof -
haftmann@60804
   107
  from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
haftmann@60804
   108
    by (auto intro: is_primeI)
haftmann@60804
   109
  with that show thesis by blast
haftmann@60804
   110
qed
haftmann@60804
   111
haftmann@60804
   112
lemma is_prime_normalize_iff [simp]:
haftmann@60804
   113
  "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
haftmann@60804
   114
proof
haftmann@60804
   115
  assume ?Q show ?P
haftmann@60804
   116
    by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
haftmann@60804
   117
next
haftmann@60804
   118
  assume ?P show ?Q
haftmann@60804
   119
    by (rule is_primeI)
haftmann@60804
   120
      (insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \<open>?P\<close>, simp_all)
haftmann@60804
   121
qed  
haftmann@60804
   122
haftmann@62499
   123
lemma no_prime_divisorsI:
haftmann@62499
   124
  assumes "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime b"
haftmann@62499
   125
  shows "is_unit a"
haftmann@62499
   126
proof (rule no_prime_divisorsI2)
haftmann@62499
   127
  fix b
haftmann@62499
   128
  assume "b dvd a"
haftmann@62499
   129
  then have "normalize b dvd a"
haftmann@62499
   130
    by simp
haftmann@62499
   131
  moreover have "normalize (normalize b) = normalize b"
haftmann@62499
   132
    by simp
haftmann@62499
   133
  ultimately have "\<not> is_prime (normalize b)"
haftmann@62499
   134
    by (rule assms)
haftmann@62499
   135
  then show "\<not> is_prime b"
haftmann@62499
   136
    by simp
haftmann@62499
   137
qed
haftmann@62499
   138
haftmann@62499
   139
lemma prime_divisorE:
haftmann@62499
   140
  assumes "a \<noteq> 0" and "\<not> is_unit a" 
haftmann@62499
   141
  obtains p where "is_prime p" and "p dvd a"
haftmann@62499
   142
  using assms no_prime_divisorsI [of a] by blast
haftmann@62499
   143
haftmann@62499
   144
lemma is_prime_associated:
haftmann@62499
   145
  assumes "is_prime p" and "is_prime q" and "q dvd p"
haftmann@62499
   146
  shows "normalize q = normalize p"
haftmann@62499
   147
using \<open>q dvd p\<close> proof (rule associatedI)
haftmann@62499
   148
  from \<open>is_prime q\<close> have "\<not> is_unit q"
haftmann@62499
   149
    by (simp add: is_prime_not_unit)
haftmann@62499
   150
  with \<open>is_prime p\<close> \<open>q dvd p\<close> show "p dvd q"
haftmann@62499
   151
    by (blast intro: is_primeD2)
haftmann@62499
   152
qed
haftmann@62499
   153
haftmann@62499
   154
lemma prime_dvd_mult_iff:  
haftmann@62499
   155
  assumes "is_prime p"
haftmann@62499
   156
  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
haftmann@62499
   157
  using assms by (auto dest: is_primeD)
haftmann@62499
   158
haftmann@62499
   159
lemma prime_dvd_msetprod:
haftmann@62499
   160
  assumes "is_prime p"
haftmann@62499
   161
  assumes dvd: "p dvd msetprod A"
haftmann@62499
   162
  obtains a where "a \<in># A" and "p dvd a"
haftmann@62499
   163
proof -
haftmann@62499
   164
  from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
haftmann@62499
   165
  proof (induct A)
haftmann@62499
   166
    case empty then show ?case
haftmann@62499
   167
    using \<open>is_prime p\<close> by (simp add: is_prime_not_unit)
haftmann@62499
   168
  next
haftmann@62499
   169
    case (add A a)
haftmann@62499
   170
    then have "p dvd msetprod A * a" by simp
haftmann@62499
   171
    with \<open>is_prime p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
haftmann@62499
   172
      by (blast dest: is_primeD)
haftmann@62499
   173
    then show ?case proof cases
haftmann@62499
   174
      case B then show ?thesis by auto
haftmann@62499
   175
    next
haftmann@62499
   176
      case A
haftmann@62499
   177
      with add.hyps obtain b where "b \<in># A" "p dvd b"
haftmann@62499
   178
        by auto
haftmann@62499
   179
      then show ?thesis by auto
haftmann@62499
   180
    qed
haftmann@62499
   181
  qed
haftmann@62499
   182
  with that show thesis by blast
haftmann@62499
   183
qed
haftmann@62499
   184
haftmann@62499
   185
lemma msetprod_eq_iff:
haftmann@62499
   186
  assumes "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p" and "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
haftmann@62499
   187
  shows "msetprod P = msetprod Q \<longleftrightarrow> P = Q" (is "?R \<longleftrightarrow> ?S")
haftmann@62499
   188
proof
haftmann@62499
   189
  assume ?S then show ?R by simp
haftmann@62499
   190
next
haftmann@62499
   191
  assume ?R then show ?S using assms proof (induct P arbitrary: Q)
haftmann@62499
   192
    case empty then have Q: "msetprod Q = 1" by simp
haftmann@62499
   193
    have "Q = {#}"
haftmann@62499
   194
    proof (rule ccontr)
haftmann@62499
   195
      assume "Q \<noteq> {#}"
haftmann@62499
   196
      then obtain r R where "Q = R + {#r#}"
haftmann@62499
   197
        using multi_nonempty_split by blast 
haftmann@62499
   198
      moreover with empty have "is_prime r" by simp
haftmann@62499
   199
      ultimately have "msetprod Q = msetprod R * r"
haftmann@62499
   200
        by simp
haftmann@62499
   201
      with Q have "msetprod R * r = 1"
haftmann@62499
   202
        by simp
haftmann@62499
   203
      then have "is_unit r"
haftmann@62499
   204
        by (metis local.dvd_triv_right)
haftmann@62499
   205
      with \<open>is_prime r\<close> show False by (simp add: is_prime_not_unit)
haftmann@62499
   206
    qed
haftmann@62499
   207
    then show ?case by simp
haftmann@62499
   208
  next
haftmann@62499
   209
    case (add P p)
haftmann@62499
   210
    then have "is_prime p" and "normalize p = p"
haftmann@62499
   211
      and "msetprod Q = msetprod P * p" and "p dvd msetprod Q"
haftmann@62499
   212
      by auto (metis local.dvd_triv_right)
haftmann@62499
   213
    with prime_dvd_msetprod
haftmann@62499
   214
      obtain q where "q \<in># Q" and "p dvd q"
haftmann@62499
   215
      by blast
haftmann@62499
   216
    with add.prems have "is_prime q" and "normalize q = q"
haftmann@62499
   217
      by simp_all
haftmann@62499
   218
    from \<open>is_prime p\<close> have "p \<noteq> 0"
haftmann@62499
   219
      by auto 
haftmann@62499
   220
    from \<open>is_prime q\<close> \<open>is_prime p\<close> \<open>p dvd q\<close>
haftmann@62499
   221
      have "normalize p = normalize q"
haftmann@62499
   222
      by (rule is_prime_associated)
haftmann@62499
   223
    from \<open>normalize p = p\<close> \<open>normalize q = q\<close> have "p = q"
haftmann@62499
   224
      unfolding \<open>normalize p = normalize q\<close> by simp
haftmann@62499
   225
    with \<open>q \<in># Q\<close> have "p \<in># Q" by simp
haftmann@62499
   226
    have "msetprod P = msetprod (Q - {#p#})"
haftmann@62499
   227
      using \<open>p \<in># Q\<close> \<open>p \<noteq> 0\<close> \<open>msetprod Q = msetprod P * p\<close>
haftmann@62499
   228
      by (simp add: msetprod_minus)
haftmann@62499
   229
    then have "P = Q - {#p#}"
haftmann@62499
   230
      using add.prems(2-3)
haftmann@62499
   231
      by (auto intro: add.hyps dest: in_diffD)
haftmann@62499
   232
    with \<open>p \<in># Q\<close> show ?case by simp
haftmann@62499
   233
  qed
haftmann@62499
   234
qed
haftmann@62499
   235
haftmann@62499
   236
lemma prime_dvd_power_iff:
haftmann@62499
   237
  assumes "is_prime p"
haftmann@62499
   238
  shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
haftmann@62499
   239
  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
haftmann@62499
   240
haftmann@62499
   241
lemma prime_power_dvd_multD:
haftmann@62499
   242
  assumes "is_prime p"
haftmann@62499
   243
  assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
haftmann@62499
   244
  shows "p ^ n dvd b"
haftmann@62499
   245
using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
haftmann@62499
   246
  case 0 then show ?case by simp
haftmann@62499
   247
next
haftmann@62499
   248
  case (Suc n) show ?case
haftmann@62499
   249
  proof (cases "n = 0")
haftmann@62499
   250
    case True with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> show ?thesis
haftmann@62499
   251
      by (simp add: prime_dvd_mult_iff)
haftmann@62499
   252
  next
haftmann@62499
   253
    case False then have "n > 0" by simp
haftmann@62499
   254
    from \<open>is_prime p\<close> have "p \<noteq> 0" by auto
haftmann@62499
   255
    from Suc.prems have *: "p * p ^ n dvd a * b"
haftmann@62499
   256
      by simp
haftmann@62499
   257
    then have "p dvd a * b"
haftmann@62499
   258
      by (rule dvd_mult_left)
haftmann@62499
   259
    with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
haftmann@62499
   260
      by (simp add: prime_dvd_mult_iff)
haftmann@62499
   261
    moreover def c \<equiv> "b div p"
haftmann@62499
   262
    ultimately have b: "b = p * c" by simp
haftmann@62499
   263
    with * have "p * p ^ n dvd p * (a * c)"
haftmann@62499
   264
      by (simp add: ac_simps)
haftmann@62499
   265
    with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c"
haftmann@62499
   266
      by simp
haftmann@62499
   267
    with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c"
haftmann@62499
   268
      by blast
haftmann@62499
   269
    with \<open>p \<noteq> 0\<close> show ?thesis
haftmann@62499
   270
      by (simp add: b)
haftmann@62499
   271
  qed
haftmann@62499
   272
qed
haftmann@62499
   273
haftmann@60804
   274
lemma is_prime_inj_power:
haftmann@60804
   275
  assumes "is_prime p"
haftmann@60804
   276
  shows "inj (op ^ p)"
haftmann@60804
   277
proof (rule injI, rule ccontr)
haftmann@60804
   278
  fix m n :: nat
haftmann@60804
   279
  have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
haftmann@60804
   280
  proof
haftmann@60804
   281
    assume ?Q then show ?P by simp
haftmann@60804
   282
  next
haftmann@60804
   283
    assume ?P then have "is_unit (p ^ q)" by simp
haftmann@60804
   284
    with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
haftmann@60804
   285
  qed
haftmann@60804
   286
  have *: False if "p ^ m = p ^ n" and "m > n" for m n
haftmann@60804
   287
  proof -
haftmann@60804
   288
    from assms have "p \<noteq> 0"
haftmann@60804
   289
      by (rule is_prime_not_zeroI)
haftmann@60804
   290
    then have "p ^ n \<noteq> 0"
haftmann@60804
   291
      by (induct n) simp_all
haftmann@60804
   292
    from that have "m = n + (m - n)" and "m - n > 0" by arith+
haftmann@60804
   293
    then obtain q where "m = n + q" and "q > 0" ..
haftmann@60804
   294
    with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
haftmann@60804
   295
    with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
haftmann@60804
   296
      using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
haftmann@60804
   297
    with \<open>q > 0\<close> show ?thesis by simp
haftmann@60804
   298
  qed 
haftmann@60804
   299
  assume "m \<noteq> n"
haftmann@60804
   300
  then have "m > n \<or> m < n" by arith
haftmann@60804
   301
  moreover assume "p ^ m = p ^ n"
haftmann@60804
   302
  ultimately show False using * [of m n] * [of n m] by auto
haftmann@60804
   303
qed
haftmann@60804
   304
haftmann@62499
   305
definition factorization :: "'a \<Rightarrow> 'a multiset option"
haftmann@62499
   306
  where "factorization a = (if a = 0 then None
haftmann@62499
   307
    else Some (setsum (\<lambda>p. replicate_mset (Max {n. p ^ n dvd a}) p)
haftmann@62499
   308
      {p. p dvd a \<and> is_prime p \<and> normalize p = p}))"
haftmann@62499
   309
haftmann@62499
   310
lemma factorization_normalize [simp]:
haftmann@62499
   311
  "factorization (normalize a) = factorization a"
haftmann@62499
   312
  by (simp add: factorization_def)
haftmann@62499
   313
haftmann@62499
   314
lemma factorization_0 [simp]:
haftmann@62499
   315
  "factorization 0 = None"
haftmann@62499
   316
  by (simp add: factorization_def)
haftmann@62499
   317
haftmann@62499
   318
lemma factorization_eq_None_iff [simp]:
haftmann@62499
   319
  "factorization a = None \<longleftrightarrow> a = 0"
haftmann@62499
   320
  by (simp add: factorization_def)
haftmann@60804
   321
haftmann@62499
   322
lemma factorization_eq_Some_iff:
haftmann@62499
   323
  "factorization a = Some P \<longleftrightarrow>
haftmann@62499
   324
   normalize a = msetprod P \<and> 0 \<notin># P \<and> (\<forall>p \<in> set_mset P. is_prime p \<and> normalize p = p)"
haftmann@62499
   325
proof (cases "a = 0")
haftmann@62499
   326
  have [simp]: "0 = msetprod P \<longleftrightarrow> 0 \<in># P"
haftmann@62499
   327
    using msetprod_zero_iff [of P] by blast
haftmann@62499
   328
  case True
haftmann@62499
   329
  then show ?thesis by auto
haftmann@62499
   330
next
haftmann@62499
   331
  case False    
haftmann@60804
   332
  let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
haftmann@62499
   333
  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}"
haftmann@62499
   334
    by auto
haftmann@62499
   335
  moreover from \<open>a \<noteq> 0\<close> have "finite {b. b dvd a \<and> normalize b = b}"
haftmann@60804
   336
    by (rule finite_divisors)
haftmann@62499
   337
  ultimately have "finite (?prime_factors a)"
haftmann@62499
   338
    by (rule finite_subset)
haftmann@62499
   339
  then show ?thesis using \<open>a \<noteq> 0\<close>
haftmann@62499
   340
  proof (induct "?prime_factors a" arbitrary: a P)
haftmann@60804
   341
    case empty then have
haftmann@62499
   342
      *: "{p. p dvd a \<and> is_prime p \<and> normalize p = p} = {}"
haftmann@62499
   343
        and "a \<noteq> 0"
haftmann@60804
   344
      by auto
haftmann@62499
   345
    from \<open>a \<noteq> 0\<close> have "factorization a = Some {#}"
haftmann@62499
   346
      by (simp only: factorization_def *) simp
haftmann@62499
   347
    from * have "normalize a = 1"
haftmann@62499
   348
      by (auto intro: is_unit_normalize no_prime_divisorsI)
haftmann@62499
   349
    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
haftmann@62499
   350
      assume ?lhs with \<open>factorization a = Some {#}\<close> \<open>normalize a = 1\<close>
haftmann@62499
   351
      show ?rhs by simp
haftmann@62499
   352
    next
haftmann@62499
   353
      assume ?rhs have "P = {#}"
haftmann@62499
   354
      proof (rule ccontr)
haftmann@62499
   355
        assume "P \<noteq> {#}"
haftmann@62499
   356
        then obtain q Q where "P = Q + {#q#}"
haftmann@62499
   357
          using multi_nonempty_split by blast
haftmann@62499
   358
        with \<open>?rhs\<close> \<open>normalize a = 1\<close>
haftmann@62499
   359
        have "1 = q * msetprod Q" and "is_prime q"
haftmann@62499
   360
          by (simp_all add: ac_simps)
haftmann@62499
   361
        then have "is_unit q" by (auto intro: dvdI)
haftmann@62499
   362
        with \<open>is_prime q\<close> show False
haftmann@62499
   363
          using is_prime_not_unit by blast
haftmann@62499
   364
      qed
haftmann@62499
   365
      with \<open>factorization a = Some {#}\<close> show ?lhs by simp
haftmann@60804
   366
    qed
haftmann@60804
   367
  next
haftmann@62499
   368
    case (insert p F)
haftmann@62499
   369
    from \<open>insert p F = ?prime_factors a\<close>
haftmann@62499
   370
    have "?prime_factors a = insert p F"
haftmann@62499
   371
      by simp
haftmann@62499
   372
    then have "p dvd a" and "is_prime p" and "normalize p = p" and "p \<noteq> 0"
haftmann@62499
   373
      by (auto intro!: is_prime_not_zeroI)
haftmann@62499
   374
    def n \<equiv> "Max {n. p ^ n dvd a}"
haftmann@62499
   375
    then have "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
haftmann@62499
   376
    proof -
haftmann@60804
   377
      def N \<equiv> "{n. p ^ n dvd a}"
haftmann@62499
   378
      then have n_M: "n = Max N" by (simp add: n_def)
haftmann@60804
   379
      from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
haftmann@60804
   380
      then have "inj_on (op ^ p) U" for U
haftmann@60804
   381
        by (rule subset_inj_on) simp
haftmann@60804
   382
      moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
haftmann@60804
   383
        by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
haftmann@60804
   384
      ultimately have "finite N"
haftmann@60804
   385
        by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
haftmann@60804
   386
      from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
haftmann@60804
   387
      then have "N \<noteq> {}" by blast
haftmann@60804
   388
      note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
haftmann@60804
   389
      from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
haftmann@62499
   390
      with * have "Max N > 0"
haftmann@60804
   391
        by (auto simp add: Max_gr_iff)
haftmann@62499
   392
      then show "n > 0" by (simp add: n_M)
haftmann@60804
   393
      from * have "Max N \<in> N" by (rule Max_in)
haftmann@62499
   394
      then have "p ^ Max N dvd a" by (simp add: N_def)
haftmann@62499
   395
      then show "p ^ n dvd a" by (simp add: n_M)
haftmann@60804
   396
      from * have "\<forall>n\<in>N. n \<le> Max N"
haftmann@60804
   397
        by (simp add: Max_le_iff [symmetric])
haftmann@60804
   398
      then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
haftmann@60804
   399
        by (rule bspec) (simp add: N_def)
haftmann@62499
   400
      then have "\<not> p ^ Suc (Max N) dvd a"
haftmann@60804
   401
        by auto
haftmann@62499
   402
      then show "\<not> p ^ Suc n dvd a"
haftmann@62499
   403
        by (simp add: n_M)
haftmann@60804
   404
    qed
haftmann@62499
   405
    def b \<equiv> "a div p ^ n"
haftmann@62499
   406
    with \<open>p ^ n dvd a\<close> have a: "a = p ^ n * b"
haftmann@62499
   407
      by simp
haftmann@62499
   408
    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd b" and "b \<noteq> 0"
haftmann@60804
   409
      by (auto elim: dvdE simp add: ac_simps)
haftmann@62499
   410
    have "?prime_factors a = insert p (?prime_factors b)"
haftmann@60804
   411
    proof (rule set_eqI)
haftmann@60804
   412
      fix q
haftmann@62499
   413
      show "q \<in> ?prime_factors a \<longleftrightarrow> q \<in> insert p (?prime_factors b)"
haftmann@62499
   414
      using \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close>
haftmann@62499
   415
        by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff)
haftmann@62499
   416
          (auto dest: is_prime_associated)
haftmann@60804
   417
    qed
haftmann@62499
   418
    with \<open>\<not> p dvd b\<close> have "?prime_factors a - {p} = ?prime_factors b"
haftmann@62499
   419
      by auto
haftmann@62499
   420
    with insert.hyps have "F = ?prime_factors b"
haftmann@60804
   421
      by auto
haftmann@62499
   422
    then have "?prime_factors b = F"
haftmann@62499
   423
      by simp
haftmann@62499
   424
    with \<open>?prime_factors a = insert p (?prime_factors b)\<close> have "?prime_factors a = insert p F"
haftmann@60804
   425
      by simp
haftmann@62499
   426
    have equiv: "(\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p) =
haftmann@62499
   427
      (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p)"
haftmann@62499
   428
    using refl proof (rule Groups_Big.setsum.cong)
haftmann@62499
   429
      fix q
haftmann@62499
   430
      assume "q \<in> F"
haftmann@62499
   431
      have "{n. q ^ n dvd a} = {n. q ^ n dvd b}"
haftmann@62499
   432
      proof -
haftmann@62499
   433
        have "q ^ m dvd a \<longleftrightarrow> q ^ m dvd b" (is "?R \<longleftrightarrow> ?S")
haftmann@62499
   434
          for m
haftmann@62499
   435
        proof (cases "m = 0")
haftmann@62499
   436
          case True then show ?thesis by simp
haftmann@62499
   437
        next
haftmann@62499
   438
          case False then have "m > 0" by simp
haftmann@62499
   439
          show ?thesis
haftmann@62499
   440
          proof
haftmann@62499
   441
            assume ?S then show ?R by (simp add: a)
haftmann@62499
   442
          next
haftmann@62499
   443
            assume ?R
haftmann@62499
   444
            then have *: "q ^ m dvd p ^ n * b" by (simp add: a)
haftmann@62499
   445
            from insert.hyps \<open>q \<in> F\<close>
haftmann@62499
   446
            have "is_prime q" "normalize q = q" "p \<noteq> q" "q dvd p ^ n * b"
haftmann@62499
   447
              by (auto simp add: a)
haftmann@62499
   448
            from \<open>is_prime q\<close> * \<open>m > 0\<close> show ?S
haftmann@62499
   449
            proof (rule prime_power_dvd_multD)
haftmann@62499
   450
              have "\<not> q dvd p"
haftmann@62499
   451
              proof
haftmann@62499
   452
                assume "q dvd p"
haftmann@62499
   453
                with \<open>is_prime q\<close> \<open>is_prime p\<close> have "normalize q = normalize p"
haftmann@62499
   454
                  by (blast intro: is_prime_associated)
haftmann@62499
   455
                with \<open>normalize p = p\<close> \<open>normalize q = q\<close> \<open>p \<noteq> q\<close> show False
haftmann@62499
   456
                  by simp
haftmann@62499
   457
              qed
haftmann@62499
   458
              with \<open>is_prime q\<close> show "\<not> q dvd p ^ n"
haftmann@62499
   459
                by (simp add: prime_dvd_power_iff)
haftmann@62499
   460
            qed
haftmann@62499
   461
          qed
haftmann@62499
   462
        qed
haftmann@62499
   463
        then show ?thesis by auto
haftmann@62499
   464
      qed
haftmann@62499
   465
      then show
haftmann@62499
   466
        "replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q"
haftmann@62499
   467
        by simp
haftmann@62499
   468
    qed
haftmann@62499
   469
    def Q \<equiv> "the (factorization b)"
haftmann@62499
   470
    with \<open>b \<noteq> 0\<close> have [simp]: "factorization b = Some Q"
haftmann@62499
   471
      by simp
haftmann@62499
   472
    from \<open>a \<noteq> 0\<close> have "factorization a =
haftmann@62499
   473
      Some (\<Sum>p\<in>?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)"
haftmann@62499
   474
      by (simp add: factorization_def)
haftmann@62499
   475
    also have "\<dots> =
haftmann@62499
   476
      Some (\<Sum>p\<in>insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)"
haftmann@62499
   477
      by (simp add: \<open>?prime_factors a = insert p F\<close>)
haftmann@62499
   478
    also have "\<dots> =
haftmann@62499
   479
      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p))"
haftmann@62499
   480
      using \<open>finite F\<close> \<open>p \<notin> F\<close> n_def by simp
haftmann@62499
   481
    also have "\<dots> =
haftmann@62499
   482
      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p))"
haftmann@62499
   483
      using equiv by simp
haftmann@62499
   484
    also have "\<dots> = Some (replicate_mset n p + the (factorization b))"
haftmann@62499
   485
      using \<open>b \<noteq> 0\<close> by (simp add: factorization_def \<open>?prime_factors a = insert p F\<close> \<open>?prime_factors b = F\<close>)
haftmann@62499
   486
    finally have fact_a: "factorization a = 
haftmann@62499
   487
      Some (replicate_mset n p + Q)"
haftmann@62499
   488
      by simp
haftmann@62499
   489
    moreover have "factorization b = Some Q \<longleftrightarrow>
haftmann@62499
   490
      normalize b = msetprod Q \<and>
haftmann@62499
   491
      0 \<notin># Q \<and>
haftmann@62499
   492
      (\<forall>p\<in>#Q. is_prime p \<and> normalize p = p)"
haftmann@62499
   493
      using \<open>F = ?prime_factors b\<close> \<open>b \<noteq> 0\<close> by (rule insert.hyps)
haftmann@62499
   494
    ultimately have
haftmann@62499
   495
      norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and
haftmann@62499
   496
      prime_Q: "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
haftmann@62499
   497
      by (simp_all add: a normalize_mult normalize_power \<open>normalize p = p\<close>)
haftmann@62499
   498
    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
haftmann@62499
   499
      assume ?lhs with fact_a
haftmann@62499
   500
      have "P = replicate_mset n p + Q" by simp
haftmann@62499
   501
      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> prime_Q
haftmann@62499
   502
        show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI)
haftmann@62499
   503
    next
haftmann@62499
   504
      assume ?rhs
haftmann@62499
   505
      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close> prime_Q
haftmann@62499
   506
      have "msetprod P = msetprod (replicate_mset n p + Q)"
haftmann@62499
   507
        and "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p"
haftmann@62499
   508
        and "\<forall>p\<in>set_mset (replicate_mset n p + Q). is_prime p \<and> normalize p = p"
haftmann@62499
   509
        by (simp_all add: norm_a)
haftmann@62499
   510
      then have "P = replicate_mset n p + Q"
haftmann@62499
   511
        by (simp only: msetprod_eq_iff)
haftmann@62499
   512
      then show ?lhs
haftmann@62499
   513
        by (simp add: fact_a)
haftmann@62499
   514
    qed
haftmann@60804
   515
  qed
haftmann@60804
   516
qed
haftmann@62499
   517
haftmann@62499
   518
lemma factorization_cases [case_names 0 factorization]:
haftmann@62499
   519
  assumes "0": "a = 0 \<Longrightarrow> P"
haftmann@62499
   520
  assumes factorization: "\<And>A. a \<noteq> 0 \<Longrightarrow> factorization a = Some A \<Longrightarrow> msetprod A = normalize a
haftmann@62499
   521
    \<Longrightarrow> 0 \<notin># A \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> normalize p = p) \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> P"
haftmann@62499
   522
  shows P
haftmann@62499
   523
proof (cases "a = 0")
haftmann@62499
   524
  case True with 0 show P .
haftmann@62499
   525
next
haftmann@62499
   526
  case False
haftmann@62499
   527
  then have "factorization a \<noteq> None" by simp
haftmann@62499
   528
  then obtain A where "factorization a = Some A" by blast
haftmann@62499
   529
  moreover from this have "msetprod A = normalize a"
haftmann@62499
   530
    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
haftmann@62499
   531
    by (auto simp add: factorization_eq_Some_iff)
haftmann@62499
   532
  ultimately show P using \<open>a \<noteq> 0\<close> factorization by blast
haftmann@62499
   533
qed
haftmann@62499
   534
haftmann@62499
   535
lemma factorizationE:
haftmann@62499
   536
  assumes "a \<noteq> 0"
haftmann@62499
   537
  obtains A u where "factorization a = Some A" "normalize a = msetprod A"
haftmann@62499
   538
    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
haftmann@62499
   539
  using assms by (cases a rule: factorization_cases) simp_all
haftmann@62499
   540
haftmann@62499
   541
lemma prime_dvd_mset_prod_iff:
haftmann@62499
   542
  assumes "is_prime p" "normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
haftmann@62499
   543
  shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
haftmann@62499
   544
using assms proof (induct A)
haftmann@62499
   545
  case empty then show ?case by (auto dest: is_prime_not_unit)
haftmann@62499
   546
next
haftmann@62499
   547
  case (add A q) then show ?case
haftmann@62499
   548
    using is_prime_associated [of q p]
haftmann@62499
   549
    by (simp_all add: prime_dvd_mult_iff, safe, simp_all)
haftmann@62499
   550
qed
haftmann@62499
   551
haftmann@62499
   552
end
haftmann@62499
   553
haftmann@62499
   554
class factorial_semiring_gcd = factorial_semiring + gcd +
haftmann@62499
   555
  assumes gcd_unfold: "gcd a b =
haftmann@62499
   556
    (if a = 0 then normalize b
haftmann@62499
   557
     else if b = 0 then normalize a
haftmann@62499
   558
     else msetprod (the (factorization a) #\<inter> the (factorization b)))"
haftmann@62499
   559
  and lcm_unfold: "lcm a b =
haftmann@62499
   560
    (if a = 0 \<or> b = 0 then 0
haftmann@62499
   561
     else msetprod (the (factorization a) #\<union> the (factorization b)))"
haftmann@62499
   562
begin
haftmann@62499
   563
haftmann@62499
   564
subclass semiring_gcd
haftmann@62499
   565
proof
haftmann@62499
   566
  fix a b
haftmann@62499
   567
  have comm: "gcd a b = gcd b a" for a b
haftmann@62499
   568
   by (simp add: gcd_unfold ac_simps)
haftmann@62499
   569
  have "gcd a b dvd a" for a b
haftmann@62499
   570
  proof (cases a rule: factorization_cases)
haftmann@62499
   571
    case 0 then show ?thesis by simp
haftmann@62499
   572
  next
haftmann@62499
   573
    case (factorization A) note fact_A = this
haftmann@62499
   574
    then have non_zero: "\<And>p. p \<in>#A \<Longrightarrow> p \<noteq> 0"
haftmann@62499
   575
      using normalize_0 not_is_prime_zero by blast
haftmann@62499
   576
    show ?thesis
haftmann@62499
   577
    proof (cases b rule: factorization_cases)
haftmann@62499
   578
      case 0 then show ?thesis by (simp add: gcd_unfold)
haftmann@62499
   579
    next
haftmann@62499
   580
      case (factorization B) note fact_B = this
haftmann@62499
   581
      have "msetprod (A #\<inter> B) dvd msetprod A"
haftmann@62499
   582
      using non_zero proof (induct B arbitrary: A)
haftmann@62499
   583
        case empty show ?case by simp
haftmann@62499
   584
      next
haftmann@62499
   585
        case (add B p) show ?case
haftmann@62499
   586
        proof (cases "p \<in># A")
haftmann@62499
   587
          case True then obtain C where "A = C + {#p#}"
haftmann@62499
   588
            by (metis insert_DiffM2)
haftmann@62499
   589
          moreover with True add have "p \<noteq> 0" and "\<And>p. p \<in># C \<Longrightarrow> p \<noteq> 0"
haftmann@62499
   590
            by auto
haftmann@62499
   591
          ultimately show ?thesis
haftmann@62499
   592
            using True add.hyps [of C]
haftmann@62499
   593
            by (simp add: inter_union_distrib_left [symmetric])
haftmann@62499
   594
        next
haftmann@62499
   595
          case False with add.prems add.hyps [of A] show ?thesis
haftmann@62499
   596
            by (simp add: inter_add_right1)
haftmann@62499
   597
        qed
haftmann@62499
   598
      qed
haftmann@62499
   599
      with fact_A fact_B show ?thesis by (simp add: gcd_unfold)
haftmann@62499
   600
    qed
haftmann@62499
   601
  qed
haftmann@62499
   602
  then have "gcd a b dvd a" and "gcd b a dvd b"
haftmann@62499
   603
    by simp_all
haftmann@62499
   604
  then show "gcd a b dvd a" and "gcd a b dvd b"
haftmann@62499
   605
    by (simp_all add: comm)
haftmann@62499
   606
  show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c
haftmann@62499
   607
  proof (cases "a = 0 \<or> b = 0 \<or> c = 0")
haftmann@62499
   608
    case True with that show ?thesis by (auto simp add: gcd_unfold)
haftmann@62499
   609
  next
haftmann@62499
   610
    case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
haftmann@62499
   611
      by simp_all
haftmann@62499
   612
    then obtain A B C where fact:
haftmann@62499
   613
      "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
haftmann@62499
   614
      and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
haftmann@62499
   615
      and A: "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
haftmann@62499
   616
      and B: "0 \<notin># B" "\<And>p. p \<in># B \<Longrightarrow> normalize p = p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
haftmann@62499
   617
      and C: "0 \<notin># C" "\<And>p. p \<in># C \<Longrightarrow> normalize p = p" "\<And>p. p \<in># C \<Longrightarrow> is_prime p"
haftmann@62499
   618
      by (blast elim!: factorizationE)
haftmann@62499
   619
    moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
haftmann@62499
   620
      by simp_all
haftmann@62499
   621
    ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B"
haftmann@62499
   622
      by simp_all
haftmann@62499
   623
    with A B C have "msetprod C dvd msetprod (A #\<inter> B)"
haftmann@62499
   624
    proof (induct C arbitrary: A B)
haftmann@62499
   625
      case empty then show ?case by simp
haftmann@62499
   626
    next
haftmann@62499
   627
      case add: (add C p)
haftmann@62499
   628
      from add.prems
haftmann@62499
   629
        have p: "p \<noteq> 0" "is_prime p" "normalize p = p" by auto
haftmann@62499
   630
      from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B"
haftmann@62499
   631
        by simp_all
haftmann@62499
   632
      then have "p dvd msetprod A" "p dvd msetprod B"
haftmann@62499
   633
        by (auto dest: dvd_mult_imp_div dvd_mult_right)
haftmann@62499
   634
      with p add.prems have "p \<in># A" "p \<in># B"
haftmann@62499
   635
        by (simp_all add: prime_dvd_mset_prod_iff)
haftmann@62499
   636
      then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'"
haftmann@62499
   637
        by (auto dest!: multi_member_split simp add: ac_simps)
haftmann@62499
   638
      with add.prems prems p have "msetprod C dvd msetprod (A' #\<inter> B')"
haftmann@62499
   639
        by (auto intro: add.hyps simp add: ac_simps)
haftmann@62499
   640
      with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #\<inter> ({#p#} + B'))"
haftmann@62499
   641
        by (simp add: inter_union_distrib_right [symmetric])
haftmann@62499
   642
      then show ?case by (simp add: ABp ac_simps)
haftmann@62499
   643
    qed
haftmann@62499
   644
    with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> that fact have "normalize c dvd gcd a b"
haftmann@62499
   645
      by (simp add: norm [symmetric] gcd_unfold fact)
haftmann@62499
   646
    then show ?thesis by simp
haftmann@62499
   647
  qed
haftmann@62499
   648
  show "normalize (gcd a b) = gcd a b"
haftmann@62499
   649
    apply (simp add: gcd_unfold)
haftmann@62499
   650
    apply safe
haftmann@62499
   651
    apply (rule normalized_msetprodI)
haftmann@62499
   652
    apply (auto elim: factorizationE)
haftmann@62499
   653
    done
haftmann@62499
   654
  show "lcm a b = normalize (a * b) div gcd a b"
haftmann@62499
   655
    by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult
haftmann@62499
   656
      union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union)
haftmann@62499
   657
qed
haftmann@62499
   658
haftmann@60804
   659
end
haftmann@60804
   660
haftmann@60804
   661
instantiation nat :: factorial_semiring
haftmann@60804
   662
begin
haftmann@60804
   663
haftmann@60804
   664
definition is_prime_nat :: "nat \<Rightarrow> bool"
haftmann@60804
   665
where
haftmann@60804
   666
  "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
haftmann@60804
   667
haftmann@60804
   668
lemma is_prime_eq_prime:
haftmann@60804
   669
  "is_prime = prime"
haftmann@60804
   670
  by (simp add: fun_eq_iff prime_def is_prime_nat_def)
haftmann@60804
   671
haftmann@60804
   672
instance proof
haftmann@60804
   673
  show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
haftmann@60804
   674
  show "\<not> is_unit p" if "is_prime p" for p :: nat
haftmann@60804
   675
    using that by (simp add: is_prime_nat_def)
haftmann@60804
   676
next
haftmann@60804
   677
  fix p :: nat
haftmann@60804
   678
  assume "p \<noteq> 0" and "\<not> is_unit p"
haftmann@60804
   679
  then have "p > 1" by simp
haftmann@60804
   680
  assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
haftmann@60804
   681
  have "n = 1" if "n dvd p" "n \<noteq> p" for n
haftmann@60804
   682
  proof (rule ccontr)
haftmann@60804
   683
    assume "n \<noteq> 1"
haftmann@60804
   684
    with that P have "p dvd n" by auto
haftmann@60804
   685
    with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
haftmann@60804
   686
    with that show False by simp
haftmann@60804
   687
  qed
haftmann@60804
   688
  with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
haftmann@60804
   689
next
haftmann@60804
   690
  fix p m n :: nat
haftmann@60804
   691
  assume "is_prime p"
haftmann@60804
   692
  then have "prime p" by (simp add: is_prime_eq_prime)
haftmann@60804
   693
  moreover assume "p dvd m * n"
haftmann@60804
   694
  ultimately show "p dvd m \<or> p dvd n"
haftmann@60804
   695
    by (rule prime_dvd_mult_nat)
haftmann@60804
   696
next
haftmann@60804
   697
  fix n :: nat
haftmann@60804
   698
  show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
haftmann@60804
   699
    using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
haftmann@60804
   700
qed simp
haftmann@60804
   701
haftmann@60804
   702
end
haftmann@60804
   703
haftmann@60804
   704
instantiation int :: factorial_semiring
haftmann@60804
   705
begin
haftmann@60804
   706
haftmann@60804
   707
definition is_prime_int :: "int \<Rightarrow> bool"
haftmann@60804
   708
where
haftmann@60804
   709
  "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
haftmann@60804
   710
haftmann@60804
   711
lemma is_prime_int_iff [simp]:
haftmann@60804
   712
  "is_prime (int n) \<longleftrightarrow> is_prime n"
haftmann@60804
   713
  by (simp add: is_prime_int_def)
haftmann@60804
   714
haftmann@60804
   715
lemma is_prime_nat_abs_iff [simp]:
haftmann@60804
   716
  "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
haftmann@60804
   717
  by (simp add: is_prime_int_def)
haftmann@60804
   718
haftmann@60804
   719
instance proof
haftmann@60804
   720
  show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
haftmann@60804
   721
  show "\<not> is_unit p" if "is_prime p" for p :: int
haftmann@60804
   722
    using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
haftmann@60804
   723
next
haftmann@60804
   724
  fix p :: int
haftmann@60804
   725
  assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
haftmann@60804
   726
  have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
haftmann@60804
   727
  proof -
haftmann@60804
   728
    from that have "int n dvd p" by (simp add: int_dvd_iff)
haftmann@60804
   729
    moreover from that have "\<not> is_unit (int n)" by simp
haftmann@60804
   730
    ultimately have "p dvd int n" by (rule P)
haftmann@60804
   731
    with that have "p dvd int n" by auto
haftmann@60804
   732
    then show ?thesis by (simp add: dvd_int_iff)
haftmann@60804
   733
  qed
haftmann@60804
   734
  moreover assume "p \<noteq> 0" and "\<not> is_unit p"
haftmann@60804
   735
  ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
haftmann@60804
   736
  then show "is_prime p" by simp
haftmann@60804
   737
next
haftmann@60804
   738
  fix p k l :: int
haftmann@60804
   739
  assume "is_prime p"
haftmann@60804
   740
  then have *: "is_prime (nat \<bar>p\<bar>)" by simp
haftmann@60804
   741
  assume "p dvd k * l"
haftmann@60804
   742
  then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
haftmann@62348
   743
    by (simp add: dvd_int_unfold_dvd_nat)
haftmann@60804
   744
  then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
haftmann@60804
   745
    by (simp add: abs_mult nat_mult_distrib)
haftmann@60804
   746
  with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
haftmann@60804
   747
    using is_primeD [of "nat \<bar>p\<bar>"] by auto
haftmann@60804
   748
  then show "p dvd k \<or> p dvd l"
haftmann@62348
   749
    by (simp add: dvd_int_unfold_dvd_nat)
haftmann@60804
   750
next
haftmann@60804
   751
  fix k :: int
haftmann@60804
   752
  assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
haftmann@60804
   753
  have "is_unit (nat \<bar>k\<bar>)"
haftmann@60804
   754
  proof (rule no_prime_divisorsI)
haftmann@60804
   755
    fix m
haftmann@60804
   756
    assume "m dvd nat \<bar>k\<bar>"
haftmann@60804
   757
    then have "int m dvd k" by (simp add: int_dvd_iff)
haftmann@60804
   758
    then have "\<not> is_prime (int m)" by (rule P)
haftmann@60804
   759
    then show "\<not> is_prime m" by simp
haftmann@60804
   760
  qed
haftmann@60804
   761
  then show "is_unit k" by simp
haftmann@60804
   762
qed simp
haftmann@60804
   763
haftmann@60804
   764
end
haftmann@60804
   765
haftmann@60804
   766
end