src/HOL/Number_Theory/Factorial_Ring.thy
author haftmann
Mon Jul 27 22:44:02 2015 +0200 (2015-07-27)
changeset 60804 080a979a985b
child 62348 9a5f43dac883
permissions -rw-r--r--
formal class for factorial (semi)rings
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@60804
     8
imports Main Primes "~~/src/HOL/Library/Multiset" (*"~~/src/HOL/Library/Polynomial"*)
haftmann@60804
     9
begin
haftmann@60804
    10
haftmann@60804
    11
context algebraic_semidom
haftmann@60804
    12
begin
haftmann@60804
    13
haftmann@60804
    14
lemma is_unit_mult_iff:
haftmann@60804
    15
  "is_unit (a * b) \<longleftrightarrow> is_unit a \<and> is_unit b" (is "?P \<longleftrightarrow> ?Q")
haftmann@60804
    16
  by (auto dest: dvd_mult_left dvd_mult_right)
haftmann@60804
    17
haftmann@60804
    18
lemma is_unit_power_iff:
haftmann@60804
    19
  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
haftmann@60804
    20
  by (induct n) (auto simp add: is_unit_mult_iff)
haftmann@60804
    21
  
haftmann@60804
    22
lemma subset_divisors_dvd:
haftmann@60804
    23
  "{c. c dvd a} \<subseteq> {c. c dvd b} \<longleftrightarrow> a dvd b"
haftmann@60804
    24
  by (auto simp add: subset_iff intro: dvd_trans)
haftmann@60804
    25
haftmann@60804
    26
lemma strict_subset_divisors_dvd:
haftmann@60804
    27
  "{c. c dvd a} \<subset> {c. c dvd b} \<longleftrightarrow> a dvd b \<and> \<not> b dvd a"
haftmann@60804
    28
  by (auto simp add: subset_iff intro: dvd_trans)
haftmann@60804
    29
haftmann@60804
    30
end
haftmann@60804
    31
haftmann@60804
    32
class factorial_semiring = normalization_semidom +
haftmann@60804
    33
  assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
haftmann@60804
    34
  fixes is_prime :: "'a \<Rightarrow> bool"
haftmann@60804
    35
  assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
haftmann@60804
    36
    and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
haftmann@60804
    37
    and no_prime_divisorsI: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
haftmann@60804
    38
  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
    39
    and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
haftmann@60804
    40
begin
haftmann@60804
    41
haftmann@60804
    42
lemma not_is_prime_one [simp]:
haftmann@60804
    43
  "\<not> is_prime 1"
haftmann@60804
    44
  by (auto dest: is_prime_not_unit)
haftmann@60804
    45
haftmann@60804
    46
lemma is_prime_not_zeroI:
haftmann@60804
    47
  assumes "is_prime p"
haftmann@60804
    48
  shows "p \<noteq> 0"
haftmann@60804
    49
  using assms by (auto intro: ccontr)
haftmann@60804
    50
haftmann@60804
    51
lemma is_prime_multD:
haftmann@60804
    52
  assumes "is_prime (a * b)"
haftmann@60804
    53
  shows "is_unit a \<or> is_unit b"
haftmann@60804
    54
proof -
haftmann@60804
    55
  from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
haftmann@60804
    56
  moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
haftmann@60804
    57
    by auto
haftmann@60804
    58
  ultimately show ?thesis
haftmann@60804
    59
    using dvd_times_left_cancel_iff [of a b 1]
haftmann@60804
    60
      dvd_times_right_cancel_iff [of b a 1]
haftmann@60804
    61
    by auto
haftmann@60804
    62
qed
haftmann@60804
    63
haftmann@60804
    64
lemma is_primeD2:
haftmann@60804
    65
  assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
haftmann@60804
    66
  shows "p dvd a"
haftmann@60804
    67
proof -
haftmann@60804
    68
  from \<open>a dvd p\<close> obtain b where "p = a * b" ..
haftmann@60804
    69
  with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
haftmann@60804
    70
  with \<open>p = a * b\<close> show ?thesis
haftmann@60804
    71
    by (auto simp add: mult_unit_dvd_iff)
haftmann@60804
    72
qed
haftmann@60804
    73
haftmann@60804
    74
lemma is_prime_mult_unit_left:
haftmann@60804
    75
  assumes "is_prime p"
haftmann@60804
    76
    and "is_unit a"
haftmann@60804
    77
  shows "is_prime (a * p)"
haftmann@60804
    78
proof (rule is_primeI)
haftmann@60804
    79
  from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
haftmann@60804
    80
    by (auto simp add: is_unit_mult_iff is_prime_not_unit)
haftmann@60804
    81
  show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
haftmann@60804
    82
  proof -
haftmann@60804
    83
    from that \<open>is_unit a\<close> have "b dvd p"
haftmann@60804
    84
      using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
haftmann@60804
    85
    with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
haftmann@60804
    86
      using is_primeD2 [of p b] by auto
haftmann@60804
    87
    with \<open>is_unit a\<close> show ?thesis
haftmann@60804
    88
      using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
haftmann@60804
    89
  qed
haftmann@60804
    90
qed
haftmann@60804
    91
haftmann@60804
    92
lemma is_primeI2:
haftmann@60804
    93
  assumes "p \<noteq> 0"
haftmann@60804
    94
  assumes "\<not> is_unit p"
haftmann@60804
    95
  assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
haftmann@60804
    96
  shows "is_prime p"
haftmann@60804
    97
using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
haftmann@60804
    98
  fix a
haftmann@60804
    99
  assume "a dvd p"
haftmann@60804
   100
  then obtain b where "p = a * b" ..
haftmann@60804
   101
  with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
haftmann@60804
   102
  moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
haftmann@60804
   103
  moreover assume "\<not> is_unit a"
haftmann@60804
   104
  ultimately show "p dvd a"
haftmann@60804
   105
    using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
haftmann@60804
   106
qed    
haftmann@60804
   107
haftmann@60804
   108
lemma not_is_prime_divisorE:
haftmann@60804
   109
  assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
haftmann@60804
   110
  obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
haftmann@60804
   111
proof -
haftmann@60804
   112
  from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
haftmann@60804
   113
    by (auto intro: is_primeI)
haftmann@60804
   114
  with that show thesis by blast
haftmann@60804
   115
qed
haftmann@60804
   116
haftmann@60804
   117
lemma prime_divisorE:
haftmann@60804
   118
  assumes "a \<noteq> 0" and "\<not> is_unit a" 
haftmann@60804
   119
  obtains p where "is_prime p" and "p dvd a"
haftmann@60804
   120
  using assms no_prime_divisorsI [of a] by blast
haftmann@60804
   121
haftmann@60804
   122
lemma prime_dvd_mult_iff:  
haftmann@60804
   123
  assumes "is_prime p"
haftmann@60804
   124
  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
haftmann@60804
   125
  using assms by (auto dest: is_primeD)
haftmann@60804
   126
haftmann@60804
   127
lemma prime_dvd_power_iff:
haftmann@60804
   128
  assumes "is_prime p"
haftmann@60804
   129
  shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
haftmann@60804
   130
  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
haftmann@60804
   131
haftmann@60804
   132
lemma is_prime_normalize_iff [simp]:
haftmann@60804
   133
  "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
haftmann@60804
   134
proof
haftmann@60804
   135
  assume ?Q show ?P
haftmann@60804
   136
    by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
haftmann@60804
   137
next
haftmann@60804
   138
  assume ?P show ?Q
haftmann@60804
   139
    by (rule is_primeI)
haftmann@60804
   140
      (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
   141
qed  
haftmann@60804
   142
haftmann@60804
   143
lemma is_prime_inj_power:
haftmann@60804
   144
  assumes "is_prime p"
haftmann@60804
   145
  shows "inj (op ^ p)"
haftmann@60804
   146
proof (rule injI, rule ccontr)
haftmann@60804
   147
  fix m n :: nat
haftmann@60804
   148
  have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
haftmann@60804
   149
  proof
haftmann@60804
   150
    assume ?Q then show ?P by simp
haftmann@60804
   151
  next
haftmann@60804
   152
    assume ?P then have "is_unit (p ^ q)" by simp
haftmann@60804
   153
    with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
haftmann@60804
   154
  qed
haftmann@60804
   155
  have *: False if "p ^ m = p ^ n" and "m > n" for m n
haftmann@60804
   156
  proof -
haftmann@60804
   157
    from assms have "p \<noteq> 0"
haftmann@60804
   158
      by (rule is_prime_not_zeroI)
haftmann@60804
   159
    then have "p ^ n \<noteq> 0"
haftmann@60804
   160
      by (induct n) simp_all
haftmann@60804
   161
    from that have "m = n + (m - n)" and "m - n > 0" by arith+
haftmann@60804
   162
    then obtain q where "m = n + q" and "q > 0" ..
haftmann@60804
   163
    with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
haftmann@60804
   164
    with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
haftmann@60804
   165
      using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
haftmann@60804
   166
    with \<open>q > 0\<close> show ?thesis by simp
haftmann@60804
   167
  qed 
haftmann@60804
   168
  assume "m \<noteq> n"
haftmann@60804
   169
  then have "m > n \<or> m < n" by arith
haftmann@60804
   170
  moreover assume "p ^ m = p ^ n"
haftmann@60804
   171
  ultimately show False using * [of m n] * [of n m] by auto
haftmann@60804
   172
qed
haftmann@60804
   173
haftmann@60804
   174
lemma prime_unique:
haftmann@60804
   175
  assumes "is_prime q" and "is_prime p" and "q dvd p"
haftmann@60804
   176
  shows "normalize q = normalize p"
haftmann@60804
   177
proof -
haftmann@60804
   178
  from assms have "p dvd q"
haftmann@60804
   179
    by (auto dest: is_primeD2 [of p] is_prime_not_unit [of q])
haftmann@60804
   180
  with assms show ?thesis
haftmann@60804
   181
    by (auto intro: associatedI)
haftmann@60804
   182
qed  
haftmann@60804
   183
haftmann@60804
   184
lemma exists_factorization:
haftmann@60804
   185
  assumes "a \<noteq> 0"
haftmann@60804
   186
  obtains P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize a"
haftmann@60804
   187
proof -
haftmann@60804
   188
  let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
haftmann@60804
   189
  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}" by auto
haftmann@60804
   190
  moreover from assms have "finite {b. b dvd a \<and> normalize b = b}"
haftmann@60804
   191
    by (rule finite_divisors)
haftmann@60804
   192
  ultimately have "finite (?prime_factors a)" by (rule finite_subset)
haftmann@60804
   193
  then show thesis using \<open>a \<noteq> 0\<close> that proof (induct "?prime_factors a" arbitrary: thesis a)
haftmann@60804
   194
    case empty then have
haftmann@60804
   195
      P: "\<And>b. is_prime b \<Longrightarrow> b dvd a \<Longrightarrow> normalize b \<noteq> b" and "a \<noteq> 0"
haftmann@60804
   196
      by auto
haftmann@60804
   197
    have "is_unit a"
haftmann@60804
   198
    proof (rule no_prime_divisorsI)
haftmann@60804
   199
      fix b
haftmann@60804
   200
      assume "b dvd a"
haftmann@60804
   201
      then show "\<not> is_prime b"
haftmann@60804
   202
        using P [of "normalize b"] by auto
haftmann@60804
   203
    qed
haftmann@60804
   204
    then have "\<And>p. p \<in># {#} \<Longrightarrow> is_prime p" and "msetprod {#} = normalize a"
haftmann@60804
   205
      by (simp_all add: is_unit_normalize)
haftmann@60804
   206
    with empty show thesis by blast
haftmann@60804
   207
  next
haftmann@60804
   208
    case (insert p P)
haftmann@60804
   209
    from \<open>insert p P = ?prime_factors a\<close>
haftmann@60804
   210
    have "p dvd a" and "is_prime p" and "normalize p = p"
haftmann@60804
   211
      by auto
haftmann@60804
   212
    obtain n where "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
haftmann@60804
   213
    proof (rule that)
haftmann@60804
   214
      def N \<equiv> "{n. p ^ n dvd a}"
haftmann@60804
   215
      from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
haftmann@60804
   216
      then have "inj_on (op ^ p) U" for U
haftmann@60804
   217
        by (rule subset_inj_on) simp
haftmann@60804
   218
      moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
haftmann@60804
   219
        by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
haftmann@60804
   220
      ultimately have "finite N"
haftmann@60804
   221
        by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
haftmann@60804
   222
      from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
haftmann@60804
   223
      then have "N \<noteq> {}" by blast
haftmann@60804
   224
      note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
haftmann@60804
   225
      from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
haftmann@60804
   226
      with * show "Max N > 0"
haftmann@60804
   227
        by (auto simp add: Max_gr_iff)
haftmann@60804
   228
      from * have "Max N \<in> N" by (rule Max_in)
haftmann@60804
   229
      then show "p ^ Max N dvd a" by (simp add: N_def)
haftmann@60804
   230
      from * have "\<forall>n\<in>N. n \<le> Max N"
haftmann@60804
   231
        by (simp add: Max_le_iff [symmetric])
haftmann@60804
   232
      then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
haftmann@60804
   233
        by (rule bspec) (simp add: N_def)
haftmann@60804
   234
      then show "\<not> p ^ Suc (Max N) dvd a"
haftmann@60804
   235
        by auto
haftmann@60804
   236
    qed
haftmann@60804
   237
    from \<open>p ^ n dvd a\<close> obtain c where "a = p ^ n * c" ..
haftmann@60804
   238
    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd c"
haftmann@60804
   239
      by (auto elim: dvdE simp add: ac_simps)
haftmann@60804
   240
    have "?prime_factors a - {p} = ?prime_factors c" (is "?A = ?B")
haftmann@60804
   241
    proof (rule set_eqI)
haftmann@60804
   242
      fix q
haftmann@60804
   243
      show "q \<in> ?A \<longleftrightarrow> q \<in> ?B"
haftmann@60804
   244
      using \<open>normalize p = p\<close> \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>\<not> p dvd c\<close>
haftmann@60804
   245
        prime_unique [of q p]
haftmann@60804
   246
        by (auto simp add: prime_dvd_power_iff prime_dvd_mult_iff)
haftmann@60804
   247
    qed
haftmann@60804
   248
    moreover from insert have "P = ?prime_factors a - {p}"
haftmann@60804
   249
      by auto
haftmann@60804
   250
    ultimately have "P = ?prime_factors c"
haftmann@60804
   251
      by simp
haftmann@60804
   252
    moreover from \<open>a \<noteq> 0\<close> \<open>a = p ^ n * c\<close> have "c \<noteq> 0"
haftmann@60804
   253
      by auto
haftmann@60804
   254
    ultimately obtain P where "\<And>p. p \<in># P \<Longrightarrow> is_prime p" "msetprod P = normalize c"
haftmann@60804
   255
      using insert(3) by blast 
haftmann@60804
   256
    with \<open>is_prime p\<close> \<open>a = p ^ n * c\<close> \<open>normalize p = p\<close>
haftmann@60804
   257
    have "\<And>q. q \<in># P + (replicate_mset n p) \<longrightarrow> is_prime q" "msetprod (P + replicate_mset n p) = normalize a"
haftmann@60804
   258
      by (auto simp add: ac_simps normalize_mult normalize_power)
haftmann@60804
   259
    with insert(6) show thesis by blast
haftmann@60804
   260
  qed
haftmann@60804
   261
qed
haftmann@60804
   262
  
haftmann@60804
   263
end
haftmann@60804
   264
haftmann@60804
   265
instantiation nat :: factorial_semiring
haftmann@60804
   266
begin
haftmann@60804
   267
haftmann@60804
   268
definition is_prime_nat :: "nat \<Rightarrow> bool"
haftmann@60804
   269
where
haftmann@60804
   270
  "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
haftmann@60804
   271
haftmann@60804
   272
lemma is_prime_eq_prime:
haftmann@60804
   273
  "is_prime = prime"
haftmann@60804
   274
  by (simp add: fun_eq_iff prime_def is_prime_nat_def)
haftmann@60804
   275
haftmann@60804
   276
instance proof
haftmann@60804
   277
  show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
haftmann@60804
   278
  show "\<not> is_unit p" if "is_prime p" for p :: nat
haftmann@60804
   279
    using that by (simp add: is_prime_nat_def)
haftmann@60804
   280
next
haftmann@60804
   281
  fix p :: nat
haftmann@60804
   282
  assume "p \<noteq> 0" and "\<not> is_unit p"
haftmann@60804
   283
  then have "p > 1" by simp
haftmann@60804
   284
  assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
haftmann@60804
   285
  have "n = 1" if "n dvd p" "n \<noteq> p" for n
haftmann@60804
   286
  proof (rule ccontr)
haftmann@60804
   287
    assume "n \<noteq> 1"
haftmann@60804
   288
    with that P have "p dvd n" by auto
haftmann@60804
   289
    with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
haftmann@60804
   290
    with that show False by simp
haftmann@60804
   291
  qed
haftmann@60804
   292
  with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
haftmann@60804
   293
next
haftmann@60804
   294
  fix p m n :: nat
haftmann@60804
   295
  assume "is_prime p"
haftmann@60804
   296
  then have "prime p" by (simp add: is_prime_eq_prime)
haftmann@60804
   297
  moreover assume "p dvd m * n"
haftmann@60804
   298
  ultimately show "p dvd m \<or> p dvd n"
haftmann@60804
   299
    by (rule prime_dvd_mult_nat)
haftmann@60804
   300
next
haftmann@60804
   301
  fix n :: nat
haftmann@60804
   302
  show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
haftmann@60804
   303
    using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
haftmann@60804
   304
qed simp
haftmann@60804
   305
haftmann@60804
   306
end
haftmann@60804
   307
haftmann@60804
   308
instantiation int :: factorial_semiring
haftmann@60804
   309
begin
haftmann@60804
   310
haftmann@60804
   311
definition is_prime_int :: "int \<Rightarrow> bool"
haftmann@60804
   312
where
haftmann@60804
   313
  "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
haftmann@60804
   314
haftmann@60804
   315
lemma is_prime_int_iff [simp]:
haftmann@60804
   316
  "is_prime (int n) \<longleftrightarrow> is_prime n"
haftmann@60804
   317
  by (simp add: is_prime_int_def)
haftmann@60804
   318
haftmann@60804
   319
lemma is_prime_nat_abs_iff [simp]:
haftmann@60804
   320
  "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
haftmann@60804
   321
  by (simp add: is_prime_int_def)
haftmann@60804
   322
haftmann@60804
   323
instance proof
haftmann@60804
   324
  show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
haftmann@60804
   325
  show "\<not> is_unit p" if "is_prime p" for p :: int
haftmann@60804
   326
    using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
haftmann@60804
   327
next
haftmann@60804
   328
  fix p :: int
haftmann@60804
   329
  assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
haftmann@60804
   330
  have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
haftmann@60804
   331
  proof -
haftmann@60804
   332
    from that have "int n dvd p" by (simp add: int_dvd_iff)
haftmann@60804
   333
    moreover from that have "\<not> is_unit (int n)" by simp
haftmann@60804
   334
    ultimately have "p dvd int n" by (rule P)
haftmann@60804
   335
    with that have "p dvd int n" by auto
haftmann@60804
   336
    then show ?thesis by (simp add: dvd_int_iff)
haftmann@60804
   337
  qed
haftmann@60804
   338
  moreover assume "p \<noteq> 0" and "\<not> is_unit p"
haftmann@60804
   339
  ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
haftmann@60804
   340
  then show "is_prime p" by simp
haftmann@60804
   341
next
haftmann@60804
   342
  fix p k l :: int
haftmann@60804
   343
  assume "is_prime p"
haftmann@60804
   344
  then have *: "is_prime (nat \<bar>p\<bar>)" by simp
haftmann@60804
   345
  assume "p dvd k * l"
haftmann@60804
   346
  then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
haftmann@60804
   347
    by (simp add: dvd_int_iff)
haftmann@60804
   348
  then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
haftmann@60804
   349
    by (simp add: abs_mult nat_mult_distrib)
haftmann@60804
   350
  with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
haftmann@60804
   351
    using is_primeD [of "nat \<bar>p\<bar>"] by auto
haftmann@60804
   352
  then show "p dvd k \<or> p dvd l"
haftmann@60804
   353
    by (simp add: dvd_int_iff)
haftmann@60804
   354
next
haftmann@60804
   355
  fix k :: int
haftmann@60804
   356
  assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
haftmann@60804
   357
  have "is_unit (nat \<bar>k\<bar>)"
haftmann@60804
   358
  proof (rule no_prime_divisorsI)
haftmann@60804
   359
    fix m
haftmann@60804
   360
    assume "m dvd nat \<bar>k\<bar>"
haftmann@60804
   361
    then have "int m dvd k" by (simp add: int_dvd_iff)
haftmann@60804
   362
    then have "\<not> is_prime (int m)" by (rule P)
haftmann@60804
   363
    then show "\<not> is_prime m" by simp
haftmann@60804
   364
  qed
haftmann@60804
   365
  then show "is_unit k" by simp
haftmann@60804
   366
qed simp
haftmann@60804
   367
haftmann@60804
   368
end
haftmann@60804
   369
haftmann@60804
   370
end