src/HOL/Number_Theory/UniqueFactorization.thy
author wenzelm
Sat Sep 10 23:27:32 2011 +0200 (2011-09-10)
changeset 44872 a98ef45122f3
parent 44821 a92f65e174cf
child 48822 21d4ed91912f
permissions -rw-r--r--
misc tuning;
wenzelm@41959
     1
(*  Title:      HOL/Number_Theory/UniqueFactorization.thy
nipkow@31719
     2
    Author:     Jeremy Avigad
nipkow@31719
     3
wenzelm@41541
     4
Unique factorization for the natural numbers and the integers.
nipkow@31719
     5
wenzelm@41541
     6
Note: there were previous Isabelle formalizations of unique
wenzelm@41541
     7
factorization due to Thomas Marthedal Rasmussen, and, building on
wenzelm@41541
     8
that, by Jeremy Avigad and David Gray.  
nipkow@31719
     9
*)
nipkow@31719
    10
nipkow@31719
    11
header {* UniqueFactorization *}
nipkow@31719
    12
nipkow@31719
    13
theory UniqueFactorization
wenzelm@41413
    14
imports Cong "~~/src/HOL/Library/Multiset"
nipkow@31719
    15
begin
nipkow@31719
    16
nipkow@31719
    17
(* inherited from Multiset *)
nipkow@31719
    18
declare One_nat_def [simp del] 
nipkow@31719
    19
nipkow@31719
    20
(* As a simp or intro rule,
nipkow@31719
    21
nipkow@31719
    22
     prime p \<Longrightarrow> p > 0
nipkow@31719
    23
nipkow@31719
    24
   wreaks havoc here. When the premise includes ALL x :# M. prime x, it 
nipkow@31719
    25
   leads to the backchaining
nipkow@31719
    26
nipkow@31719
    27
     x > 0  
nipkow@31719
    28
     prime x 
nipkow@31719
    29
     x :# M   which is, unfortunately,
nipkow@31719
    30
     count M x > 0
nipkow@31719
    31
*)
nipkow@31719
    32
nipkow@31719
    33
nipkow@31719
    34
(* useful facts *)
nipkow@31719
    35
nipkow@31719
    36
lemma setsum_Un2: "finite (A Un B) \<Longrightarrow> 
nipkow@31719
    37
    setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) + 
nipkow@31719
    38
      setsum f (A Int B)"
nipkow@31719
    39
  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
nipkow@31719
    40
  apply (erule ssubst)
nipkow@31719
    41
  apply (subst setsum_Un_disjoint)
nipkow@31719
    42
  apply auto
nipkow@31719
    43
  apply (subst setsum_Un_disjoint)
nipkow@31719
    44
  apply auto
wenzelm@44872
    45
  done
nipkow@31719
    46
nipkow@31719
    47
lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 
nipkow@31719
    48
    setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) * 
nipkow@31719
    49
      setprod f (A Int B)"
nipkow@31719
    50
  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
nipkow@31719
    51
  apply (erule ssubst)
nipkow@31719
    52
  apply (subst setprod_Un_disjoint)
nipkow@31719
    53
  apply auto
nipkow@31719
    54
  apply (subst setprod_Un_disjoint)
nipkow@31719
    55
  apply auto
wenzelm@44872
    56
  done
nipkow@31719
    57
 
nipkow@31719
    58
(* Here is a version of set product for multisets. Is it worth moving
nipkow@31719
    59
   to multiset.thy? If so, one should similarly define msetsum for abelian 
nipkow@31719
    60
   semirings, using of_nat. Also, is it worth developing bounded quantifiers 
nipkow@31719
    61
   "ALL i :# M. P i"? 
nipkow@31719
    62
*)
nipkow@31719
    63
haftmann@35416
    64
definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where
nipkow@31719
    65
  "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
nipkow@31719
    66
nipkow@31719
    67
syntax
nipkow@31719
    68
  "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
nipkow@31719
    69
      ("(3PROD _:#_. _)" [0, 51, 10] 10)
nipkow@31719
    70
nipkow@31719
    71
translations
wenzelm@35054
    72
  "PROD i :# A. b" == "CONST msetprod (%i. b) A"
nipkow@31719
    73
wenzelm@44872
    74
lemma msetprod_empty: "msetprod f {#} = 1"
haftmann@37290
    75
  by (simp add: msetprod_def)
haftmann@37290
    76
wenzelm@44872
    77
lemma msetprod_singleton: "msetprod f {#x#} = f x"
haftmann@37290
    78
  by (simp add: msetprod_def)
haftmann@37290
    79
nipkow@31719
    80
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
nipkow@31719
    81
  apply (simp add: msetprod_def power_add)
nipkow@31719
    82
  apply (subst setprod_Un2)
nipkow@31719
    83
  apply auto
nipkow@31719
    84
  apply (subgoal_tac 
nipkow@31719
    85
      "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
nipkow@31719
    86
       (PROD x:set_of A - set_of B. f x ^ count A x)")
nipkow@31719
    87
  apply (erule ssubst)
nipkow@31719
    88
  apply (subgoal_tac 
nipkow@31719
    89
      "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
nipkow@31719
    90
       (PROD x:set_of B - set_of A. f x ^ count B x)")
nipkow@31719
    91
  apply (erule ssubst)
nipkow@31719
    92
  apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
nipkow@31719
    93
    (PROD x:set_of A - set_of B. f x ^ count A x) *
nipkow@31719
    94
    (PROD x:set_of A Int set_of B. f x ^ count A x)")
nipkow@31719
    95
  apply (erule ssubst)
nipkow@31719
    96
  apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
nipkow@31719
    97
    (PROD x:set_of B - set_of A. f x ^ count B x) *
nipkow@31719
    98
    (PROD x:set_of A Int set_of B. f x ^ count B x)")
nipkow@31719
    99
  apply (erule ssubst)
nipkow@31719
   100
  apply (subst setprod_timesf)
nipkow@31719
   101
  apply (force simp add: mult_ac)
nipkow@31719
   102
  apply (subst setprod_Un_disjoint [symmetric])
nipkow@31719
   103
  apply (auto intro: setprod_cong)
nipkow@31719
   104
  apply (subst setprod_Un_disjoint [symmetric])
nipkow@31719
   105
  apply (auto intro: setprod_cong)
wenzelm@44872
   106
  done
nipkow@31719
   107
nipkow@31719
   108
nipkow@31719
   109
subsection {* unique factorization: multiset version *}
nipkow@31719
   110
nipkow@31719
   111
lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
nipkow@31719
   112
    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
nipkow@31719
   113
proof (rule nat_less_induct, clarify)
nipkow@31719
   114
  fix n :: nat
nipkow@31719
   115
  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
nipkow@31719
   116
      (PROD i :# M. i))"
nipkow@31719
   117
  assume "(n::nat) > 0"
nipkow@31719
   118
  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
nipkow@31719
   119
    by arith
wenzelm@44872
   120
  moreover {
nipkow@31719
   121
    assume "n = 1"
nipkow@31719
   122
    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
nipkow@31719
   123
        by (auto simp add: msetprod_def)
wenzelm@44872
   124
  } moreover {
nipkow@31719
   125
    assume "n > 1" and "prime n"
nipkow@31719
   126
    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
nipkow@31719
   127
      by (auto simp add: msetprod_def)
wenzelm@44872
   128
  } moreover {
nipkow@31719
   129
    assume "n > 1" and "~ prime n"
wenzelm@44872
   130
    with not_prime_eq_prod_nat
wenzelm@44872
   131
    obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
wenzelm@44872
   132
      by blast
nipkow@31719
   133
    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
nipkow@31719
   134
        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
nipkow@31719
   135
      by blast
wenzelm@44872
   136
    then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
wenzelm@41541
   137
      by (auto simp add: n msetprod_Un)
nipkow@31719
   138
    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
nipkow@31719
   139
  }
nipkow@31719
   140
  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
nipkow@31719
   141
    by blast
nipkow@31719
   142
qed
nipkow@31719
   143
nipkow@31719
   144
lemma multiset_prime_factorization_unique_aux:
nipkow@31719
   145
  fixes a :: nat
nipkow@31719
   146
  assumes "(ALL p : set_of M. prime p)" and
nipkow@31719
   147
    "(ALL p : set_of N. prime p)" and
nipkow@31719
   148
    "(PROD i :# M. i) dvd (PROD i:# N. i)"
nipkow@31719
   149
  shows
nipkow@31719
   150
    "count M a <= count N a"
nipkow@31719
   151
proof cases
wenzelm@41541
   152
  assume M: "a : set_of M"
wenzelm@41541
   153
  with assms have a: "prime a" by auto
wenzelm@41541
   154
  with M have "a ^ count M a dvd (PROD i :# M. i)"
nipkow@31719
   155
    by (auto intro: dvd_setprod simp add: msetprod_def)
wenzelm@41541
   156
  also have "... dvd (PROD i :# N. i)" by (rule assms)
nipkow@31719
   157
  also have "... = (PROD i : (set_of N). i ^ (count N i))"
nipkow@31719
   158
    by (simp add: msetprod_def)
wenzelm@44872
   159
  also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
wenzelm@44872
   160
  proof (cases)
wenzelm@44872
   161
    assume "a : set_of N"
wenzelm@44872
   162
    then have b: "set_of N = {a} Un (set_of N - {a})"
wenzelm@44872
   163
      by auto
wenzelm@44872
   164
    then show ?thesis
wenzelm@44872
   165
      by (subst (1) b, subst setprod_Un_disjoint, auto)
wenzelm@44872
   166
  next
wenzelm@44872
   167
    assume "a ~: set_of N" 
wenzelm@44872
   168
    then show ?thesis by auto
wenzelm@44872
   169
  qed
nipkow@31719
   170
  finally have "a ^ count M a dvd 
nipkow@31719
   171
      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
wenzelm@44872
   172
  moreover
wenzelm@44872
   173
  have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
nipkow@31952
   174
    apply (subst gcd_commute_nat)
nipkow@31952
   175
    apply (rule setprod_coprime_nat)
nipkow@31952
   176
    apply (rule primes_imp_powers_coprime_nat)
wenzelm@41541
   177
    using assms M
wenzelm@41541
   178
    apply auto
nipkow@31719
   179
    done
nipkow@31719
   180
  ultimately have "a ^ count M a dvd a^(count N a)"
nipkow@31952
   181
    by (elim coprime_dvd_mult_nat)
nipkow@31719
   182
  with a show ?thesis 
wenzelm@44872
   183
    apply (intro power_dvd_imp_le)
wenzelm@44872
   184
    apply auto
wenzelm@44872
   185
    done
nipkow@31719
   186
next
nipkow@31719
   187
  assume "a ~: set_of M"
wenzelm@44872
   188
  then show ?thesis by auto
nipkow@31719
   189
qed
nipkow@31719
   190
nipkow@31719
   191
lemma multiset_prime_factorization_unique:
nipkow@31719
   192
  assumes "(ALL (p::nat) : set_of M. prime p)" and
nipkow@31719
   193
    "(ALL p : set_of N. prime p)" and
nipkow@31719
   194
    "(PROD i :# M. i) = (PROD i:# N. i)"
nipkow@31719
   195
  shows
nipkow@31719
   196
    "M = N"
nipkow@31719
   197
proof -
nipkow@31719
   198
  {
nipkow@31719
   199
    fix a
wenzelm@41541
   200
    from assms have "count M a <= count N a"
nipkow@31719
   201
      by (intro multiset_prime_factorization_unique_aux, auto) 
wenzelm@41541
   202
    moreover from assms have "count N a <= count M a"
nipkow@31719
   203
      by (intro multiset_prime_factorization_unique_aux, auto) 
nipkow@31719
   204
    ultimately have "count M a = count N a"
nipkow@31719
   205
      by auto
nipkow@31719
   206
  }
wenzelm@44872
   207
  then show ?thesis by (simp add:multiset_eq_iff)
nipkow@31719
   208
qed
nipkow@31719
   209
wenzelm@44872
   210
definition multiset_prime_factorization :: "nat => nat multiset"
wenzelm@44872
   211
where
nipkow@31719
   212
  "multiset_prime_factorization n ==
nipkow@31719
   213
     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
nipkow@31719
   214
       n = (PROD i :# M. i)))
nipkow@31719
   215
     else {#}"
nipkow@31719
   216
nipkow@31719
   217
lemma multiset_prime_factorization: "n > 0 ==>
nipkow@31719
   218
    (ALL p : set_of (multiset_prime_factorization n). prime p) &
nipkow@31719
   219
       n = (PROD i :# (multiset_prime_factorization n). i)"
nipkow@31719
   220
  apply (unfold multiset_prime_factorization_def)
nipkow@31719
   221
  apply clarsimp
nipkow@31719
   222
  apply (frule multiset_prime_factorization_exists)
nipkow@31719
   223
  apply clarify
nipkow@31719
   224
  apply (rule theI)
nipkow@31719
   225
  apply (insert multiset_prime_factorization_unique, blast)+
nipkow@31719
   226
done
nipkow@31719
   227
nipkow@31719
   228
nipkow@31719
   229
subsection {* Prime factors and multiplicity for nats and ints *}
nipkow@31719
   230
nipkow@31719
   231
class unique_factorization =
wenzelm@44872
   232
  fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
wenzelm@44872
   233
    and prime_factors :: "'a \<Rightarrow> 'a set"
nipkow@31719
   234
nipkow@31719
   235
(* definitions for the natural numbers *)
nipkow@31719
   236
nipkow@31719
   237
instantiation nat :: unique_factorization
nipkow@31719
   238
begin
nipkow@31719
   239
wenzelm@44872
   240
definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
wenzelm@44872
   241
  where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
nipkow@31719
   242
wenzelm@44872
   243
definition prime_factors_nat :: "nat \<Rightarrow> nat set"
wenzelm@44872
   244
  where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
nipkow@31719
   245
wenzelm@44872
   246
instance ..
nipkow@31719
   247
nipkow@31719
   248
end
nipkow@31719
   249
nipkow@31719
   250
(* definitions for the integers *)
nipkow@31719
   251
nipkow@31719
   252
instantiation int :: unique_factorization
nipkow@31719
   253
begin
nipkow@31719
   254
wenzelm@44872
   255
definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
wenzelm@44872
   256
  where "multiplicity_int p n = multiplicity (nat p) (nat n)"
nipkow@31719
   257
wenzelm@44872
   258
definition prime_factors_int :: "int \<Rightarrow> int set"
wenzelm@44872
   259
  where "prime_factors_int n = int ` (prime_factors (nat n))"
nipkow@31719
   260
wenzelm@44872
   261
instance ..
nipkow@31719
   262
nipkow@31719
   263
end
nipkow@31719
   264
nipkow@31719
   265
nipkow@31719
   266
subsection {* Set up transfer *}
nipkow@31719
   267
wenzelm@44872
   268
lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
wenzelm@44872
   269
  unfolding prime_factors_int_def
wenzelm@44872
   270
  apply auto
wenzelm@44872
   271
  apply (subst transfer_int_nat_set_return_embed)
wenzelm@44872
   272
  apply assumption
wenzelm@44872
   273
  done
nipkow@31719
   274
wenzelm@44872
   275
lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
nipkow@31719
   276
  by (auto simp add: nat_set_def prime_factors_int_def)
nipkow@31719
   277
nipkow@31719
   278
lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
wenzelm@44872
   279
    multiplicity (nat p) (nat n) = multiplicity p n"
nipkow@31719
   280
  by (auto simp add: multiplicity_int_def)
nipkow@31719
   281
haftmann@35644
   282
declare transfer_morphism_nat_int[transfer add return: 
nipkow@31719
   283
  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
nipkow@31719
   284
  transfer_nat_int_multiplicity]
nipkow@31719
   285
nipkow@31719
   286
wenzelm@44872
   287
lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
nipkow@31719
   288
  unfolding prime_factors_int_def by auto
nipkow@31719
   289
nipkow@31719
   290
lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
nipkow@31719
   291
    nat_set (prime_factors n)"
nipkow@31719
   292
  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
nipkow@31719
   293
nipkow@31719
   294
lemma transfer_int_nat_multiplicity: 
nipkow@31719
   295
    "multiplicity (int p) (int n) = multiplicity p n"
nipkow@31719
   296
  by (auto simp add: multiplicity_int_def)
nipkow@31719
   297
haftmann@35644
   298
declare transfer_morphism_int_nat[transfer add return: 
nipkow@31719
   299
  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
nipkow@31719
   300
  transfer_int_nat_multiplicity]
nipkow@31719
   301
nipkow@31719
   302
nipkow@31719
   303
subsection {* Properties of prime factors and multiplicity for nats and ints *}
nipkow@31719
   304
nipkow@31952
   305
lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
wenzelm@44872
   306
  unfolding prime_factors_int_def by auto
nipkow@31719
   307
nipkow@31952
   308
lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
wenzelm@44872
   309
  apply (cases "n = 0")
nipkow@31719
   310
  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
nipkow@31719
   311
  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
wenzelm@41541
   312
  done
nipkow@31719
   313
nipkow@31952
   314
lemma prime_factors_prime_int [intro]:
nipkow@31719
   315
  assumes "n >= 0" and "p : prime_factors (n::int)"
nipkow@31719
   316
  shows "prime p"
nipkow@31952
   317
  apply (rule prime_factors_prime_nat [transferred, of n p])
wenzelm@41541
   318
  using assms apply auto
wenzelm@41541
   319
  done
nipkow@31719
   320
nipkow@31952
   321
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
wenzelm@44872
   322
  apply (frule prime_factors_prime_nat)
wenzelm@44872
   323
  apply auto
wenzelm@44872
   324
  done
nipkow@31719
   325
nipkow@31952
   326
lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
nipkow@31719
   327
    p > (0::int)"
wenzelm@44872
   328
  apply (frule (1) prime_factors_prime_int)
wenzelm@44872
   329
  apply auto
wenzelm@44872
   330
  done
nipkow@31719
   331
nipkow@31952
   332
lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
wenzelm@44872
   333
  unfolding prime_factors_nat_def by auto
nipkow@31719
   334
nipkow@31952
   335
lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
wenzelm@44872
   336
  unfolding prime_factors_int_def by auto
nipkow@31719
   337
nipkow@31952
   338
lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
nipkow@31719
   339
    {p. multiplicity p n > 0}"
nipkow@31719
   340
  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
nipkow@31719
   341
nipkow@31952
   342
lemma prime_factors_altdef_int: "prime_factors (n::int) = 
nipkow@31719
   343
    {p. p >= 0 & multiplicity p n > 0}"
nipkow@31719
   344
  apply (unfold prime_factors_int_def multiplicity_int_def)
nipkow@31952
   345
  apply (subst prime_factors_altdef_nat)
nipkow@31719
   346
  apply (auto simp add: image_def)
wenzelm@41541
   347
  done
nipkow@31719
   348
nipkow@31952
   349
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
nipkow@31719
   350
    n = (PROD p : prime_factors n. p^(multiplicity p n))"
wenzelm@44872
   351
  apply (frule multiset_prime_factorization)
wenzelm@44872
   352
  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
wenzelm@44872
   353
  done
nipkow@31719
   354
nipkow@31952
   355
lemma prime_factorization_int: 
nipkow@31719
   356
  assumes "(n::int) > 0"
nipkow@31719
   357
  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
nipkow@31952
   358
  apply (rule prime_factorization_nat [transferred, of n])
wenzelm@41541
   359
  using assms apply auto
wenzelm@41541
   360
  done
nipkow@31719
   361
nipkow@31952
   362
lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
nipkow@31719
   363
  by auto
nipkow@31719
   364
nipkow@31952
   365
lemma prime_factorization_unique_nat: 
nipkow@31719
   366
    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
nipkow@31719
   367
      n = (PROD p : S. p^(f p)) \<Longrightarrow>
nipkow@31719
   368
        S = prime_factors n & (ALL p. f p = multiplicity p n)"
wenzelm@44872
   369
  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
nipkow@31719
   370
  apply (unfold prime_factors_nat_def multiplicity_nat_def)
haftmann@34947
   371
  apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
nipkow@31719
   372
  apply (unfold multiset_prime_factorization_def)
nipkow@31719
   373
  apply (subgoal_tac "n > 0")
nipkow@31719
   374
  prefer 2
nipkow@31719
   375
  apply force
nipkow@31719
   376
  apply (subst if_P, assumption)
nipkow@31719
   377
  apply (rule the1_equality)
nipkow@31719
   378
  apply (rule ex_ex1I)
nipkow@31719
   379
  apply (rule multiset_prime_factorization_exists, assumption)
nipkow@31719
   380
  apply (rule multiset_prime_factorization_unique)
nipkow@31719
   381
  apply force
nipkow@31719
   382
  apply force
nipkow@31719
   383
  apply force
haftmann@34947
   384
  unfolding set_of_def msetprod_def
nipkow@31719
   385
  apply (subgoal_tac "f : multiset")
nipkow@31719
   386
  apply (auto simp only: Abs_multiset_inverse)
nipkow@31719
   387
  unfolding multiset_def apply force 
wenzelm@44872
   388
  done
nipkow@31719
   389
nipkow@31952
   390
lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
nipkow@31719
   391
    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
nipkow@31719
   392
      prime_factors n = S"
wenzelm@44872
   393
  apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
wenzelm@44872
   394
  apply assumption+
wenzelm@44872
   395
  done
nipkow@31719
   396
nipkow@31952
   397
lemma prime_factors_characterization'_nat: 
nipkow@31719
   398
  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
nipkow@31719
   399
    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
nipkow@31719
   400
      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
nipkow@31952
   401
  apply (rule prime_factors_characterization_nat)
nipkow@31719
   402
  apply auto
wenzelm@44872
   403
  done
nipkow@31719
   404
nipkow@31719
   405
(* A minor glitch:*)
nipkow@31719
   406
nipkow@31952
   407
thm prime_factors_characterization'_nat 
nipkow@31719
   408
    [where f = "%x. f (int (x::nat))", 
nipkow@31719
   409
      transferred direction: nat "op <= (0::int)", rule_format]
nipkow@31719
   410
nipkow@31719
   411
(*
nipkow@31719
   412
  Transfer isn't smart enough to know that the "0 < f p" should 
nipkow@31719
   413
  remain a comparison between nats. But the transfer still works. 
nipkow@31719
   414
*)
nipkow@31719
   415
nipkow@31952
   416
lemma primes_characterization'_int [rule_format]: 
nipkow@31719
   417
    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
nipkow@31719
   418
      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
nipkow@31719
   419
        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
nipkow@31719
   420
          {p. p >= 0 & 0 < f p}"
nipkow@31719
   421
nipkow@31952
   422
  apply (insert prime_factors_characterization'_nat 
nipkow@31719
   423
    [where f = "%x. f (int (x::nat))", 
nipkow@31719
   424
    transferred direction: nat "op <= (0::int)"])
nipkow@31719
   425
  apply auto
wenzelm@44872
   426
  done
nipkow@31719
   427
nipkow@31952
   428
lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
nipkow@31719
   429
    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
nipkow@31719
   430
      prime_factors n = S"
nipkow@31719
   431
  apply simp
nipkow@31719
   432
  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
nipkow@31719
   433
  apply (simp only:)
nipkow@31952
   434
  apply (subst primes_characterization'_int)
nipkow@31719
   435
  apply auto
nipkow@31952
   436
  apply (auto simp add: prime_ge_0_int)
wenzelm@44872
   437
  done
nipkow@31719
   438
nipkow@31952
   439
lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
nipkow@31719
   440
    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
nipkow@31719
   441
      multiplicity p n = f p"
wenzelm@44872
   442
  apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
wenzelm@44872
   443
  apply auto
wenzelm@44872
   444
  done
nipkow@31719
   445
nipkow@31952
   446
lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
nipkow@31719
   447
    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
nipkow@31719
   448
      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
wenzelm@44872
   449
  apply (intro impI)
nipkow@31952
   450
  apply (rule multiplicity_characterization_nat)
nipkow@31719
   451
  apply auto
wenzelm@44872
   452
  done
nipkow@31719
   453
nipkow@31952
   454
lemma multiplicity_characterization'_int [rule_format]: 
nipkow@31719
   455
  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
nipkow@31719
   456
    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
nipkow@31719
   457
      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
nipkow@31952
   458
  apply (insert multiplicity_characterization'_nat 
nipkow@31719
   459
    [where f = "%x. f (int (x::nat))", 
nipkow@31719
   460
      transferred direction: nat "op <= (0::int)", rule_format])
nipkow@31719
   461
  apply auto
wenzelm@44872
   462
  done
nipkow@31719
   463
nipkow@31952
   464
lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
nipkow@31719
   465
    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
nipkow@31719
   466
      p >= 0 \<Longrightarrow> multiplicity p n = f p"
nipkow@31719
   467
  apply simp
nipkow@31719
   468
  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
nipkow@31719
   469
  apply (simp only:)
nipkow@31952
   470
  apply (subst multiplicity_characterization'_int)
nipkow@31719
   471
  apply auto
nipkow@31952
   472
  apply (auto simp add: prime_ge_0_int)
wenzelm@44872
   473
  done
nipkow@31719
   474
nipkow@31952
   475
lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
nipkow@31719
   476
  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
nipkow@31719
   477
nipkow@31952
   478
lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
nipkow@31719
   479
  by (simp add: multiplicity_int_def) 
nipkow@31719
   480
nipkow@31952
   481
lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
nipkow@31952
   482
  by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
nipkow@31719
   483
nipkow@31952
   484
lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
nipkow@31719
   485
  by (simp add: multiplicity_int_def)
nipkow@31719
   486
nipkow@31952
   487
lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
wenzelm@44872
   488
  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
nipkow@31719
   489
  apply auto
nipkow@31719
   490
  apply (case_tac "x = p")
nipkow@31719
   491
  apply auto
wenzelm@44872
   492
  done
nipkow@31719
   493
nipkow@31952
   494
lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
nipkow@31719
   495
  unfolding prime_int_def multiplicity_int_def by auto
nipkow@31719
   496
wenzelm@44872
   497
lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
wenzelm@44872
   498
  apply (cases "n = 0")
nipkow@31719
   499
  apply auto
wenzelm@44872
   500
  apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
nipkow@31719
   501
  apply auto
nipkow@31719
   502
  apply (case_tac "x = p")
nipkow@31719
   503
  apply auto
wenzelm@44872
   504
  done
nipkow@31719
   505
wenzelm@44872
   506
lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
nipkow@31952
   507
  apply (frule prime_ge_0_int)
nipkow@31719
   508
  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
wenzelm@44872
   509
  done
nipkow@31719
   510
wenzelm@44872
   511
lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
wenzelm@44872
   512
  apply (cases "n = 0")
nipkow@31719
   513
  apply auto
nipkow@31719
   514
  apply (frule multiset_prime_factorization)
nipkow@31719
   515
  apply (auto simp add: set_of_def multiplicity_nat_def)
wenzelm@44872
   516
  done
nipkow@31719
   517
nipkow@31952
   518
lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
wenzelm@44872
   519
  unfolding multiplicity_int_def prime_int_def by auto
nipkow@31719
   520
nipkow@31952
   521
lemma multiplicity_not_factor_nat [simp]: 
nipkow@31719
   522
    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
wenzelm@44872
   523
  apply (subst (asm) prime_factors_altdef_nat)
wenzelm@44872
   524
  apply auto
wenzelm@44872
   525
  done
nipkow@31719
   526
nipkow@31952
   527
lemma multiplicity_not_factor_int [simp]: 
nipkow@31719
   528
    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
wenzelm@44872
   529
  apply (subst (asm) prime_factors_altdef_int)
wenzelm@44872
   530
  apply auto
wenzelm@44872
   531
  done
nipkow@31719
   532
nipkow@31952
   533
lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
nipkow@31719
   534
    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
nipkow@31719
   535
    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
nipkow@31952
   536
  apply (rule prime_factorization_unique_nat)
nipkow@31952
   537
  apply (simp only: prime_factors_altdef_nat)
nipkow@31719
   538
  apply auto
nipkow@31719
   539
  apply (subst power_add)
nipkow@31719
   540
  apply (subst setprod_timesf)
nipkow@31719
   541
  apply (rule arg_cong2)back back
nipkow@31719
   542
  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
nipkow@31719
   543
      (prime_factors l - prime_factors k)")
nipkow@31719
   544
  apply (erule ssubst)
nipkow@31719
   545
  apply (subst setprod_Un_disjoint)
nipkow@31719
   546
  apply auto
nipkow@31719
   547
  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
nipkow@31719
   548
      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
nipkow@31719
   549
  apply (erule ssubst)
nipkow@31719
   550
  apply (simp add: setprod_1)
nipkow@31952
   551
  apply (erule prime_factorization_nat)
nipkow@31719
   552
  apply (rule setprod_cong, auto)
nipkow@31719
   553
  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
nipkow@31719
   554
      (prime_factors k - prime_factors l)")
nipkow@31719
   555
  apply (erule ssubst)
nipkow@31719
   556
  apply (subst setprod_Un_disjoint)
nipkow@31719
   557
  apply auto
nipkow@31719
   558
  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
nipkow@31719
   559
      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
nipkow@31719
   560
  apply (erule ssubst)
nipkow@31719
   561
  apply (simp add: setprod_1)
nipkow@31952
   562
  apply (erule prime_factorization_nat)
nipkow@31719
   563
  apply (rule setprod_cong, auto)
wenzelm@44872
   564
  done
nipkow@31719
   565
nipkow@31719
   566
(* transfer doesn't have the same problem here with the right 
nipkow@31719
   567
   choice of rules. *)
nipkow@31719
   568
nipkow@31952
   569
lemma multiplicity_product_aux_int: 
nipkow@31719
   570
  assumes "(k::int) > 0" and "l > 0"
nipkow@31719
   571
  shows 
nipkow@31719
   572
    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
nipkow@31719
   573
    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
nipkow@31952
   574
  apply (rule multiplicity_product_aux_nat [transferred, of l k])
wenzelm@41541
   575
  using assms apply auto
wenzelm@41541
   576
  done
nipkow@31719
   577
nipkow@31952
   578
lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
nipkow@31719
   579
    prime_factors k Un prime_factors l"
nipkow@31952
   580
  by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
nipkow@31719
   581
nipkow@31952
   582
lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
nipkow@31719
   583
    prime_factors k Un prime_factors l"
nipkow@31952
   584
  by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
nipkow@31719
   585
nipkow@31952
   586
lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
nipkow@31719
   587
    multiplicity p k + multiplicity p l"
nipkow@31952
   588
  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
nipkow@31719
   589
      symmetric])
nipkow@31719
   590
nipkow@31952
   591
lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
nipkow@31719
   592
    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
nipkow@31952
   593
  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
nipkow@31719
   594
      symmetric])
nipkow@31719
   595
nipkow@31952
   596
lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
nipkow@31719
   597
    multiplicity (p::nat) (PROD x : S. f x) = 
nipkow@31719
   598
      (SUM x : S. multiplicity p (f x))"
nipkow@31719
   599
  apply (induct set: finite)
nipkow@31719
   600
  apply auto
nipkow@31952
   601
  apply (subst multiplicity_product_nat)
nipkow@31719
   602
  apply auto
wenzelm@44872
   603
  done
nipkow@31719
   604
nipkow@31719
   605
(* Transfer is delicate here for two reasons: first, because there is
nipkow@31719
   606
   an implicit quantifier over functions (f), and, second, because the 
nipkow@31719
   607
   product over the multiplicity should not be translated to an integer 
nipkow@31719
   608
   product.
nipkow@31719
   609
nipkow@31719
   610
   The way to handle the first is to use quantifier rules for functions.
nipkow@31719
   611
   The way to handle the second is to turn off the offending rule.
nipkow@31719
   612
*)
nipkow@31719
   613
nipkow@31719
   614
lemma transfer_nat_int_sum_prod_closure3:
nipkow@31719
   615
  "(SUM x : A. int (f x)) >= 0"
nipkow@31719
   616
  "(PROD x : A. int (f x)) >= 0"
nipkow@31719
   617
  apply (rule setsum_nonneg, auto)
nipkow@31719
   618
  apply (rule setprod_nonneg, auto)
wenzelm@44872
   619
  done
nipkow@31719
   620
haftmann@35644
   621
declare transfer_morphism_nat_int[transfer 
nipkow@31719
   622
  add return: transfer_nat_int_sum_prod_closure3
nipkow@31719
   623
  del: transfer_nat_int_sum_prod2 (1)]
nipkow@31719
   624
nipkow@31952
   625
lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
nipkow@31719
   626
  (ALL x : S. f x > 0) \<Longrightarrow> 
nipkow@31719
   627
    multiplicity (p::int) (PROD x : S. f x) = 
nipkow@31719
   628
      (SUM x : S. multiplicity p (f x))"
nipkow@31719
   629
nipkow@31952
   630
  apply (frule multiplicity_setprod_nat
nipkow@31719
   631
    [where f = "%x. nat(int(nat(f x)))", 
nipkow@31719
   632
      transferred direction: nat "op <= (0::int)"])
nipkow@31719
   633
  apply auto
nipkow@31719
   634
  apply (subst (asm) setprod_cong)
nipkow@31719
   635
  apply (rule refl)
nipkow@31719
   636
  apply (rule if_P)
nipkow@31719
   637
  apply auto
nipkow@31719
   638
  apply (rule setsum_cong)
nipkow@31719
   639
  apply auto
wenzelm@44872
   640
  done
nipkow@31719
   641
haftmann@35644
   642
declare transfer_morphism_nat_int[transfer 
nipkow@31719
   643
  add return: transfer_nat_int_sum_prod2 (1)]
nipkow@31719
   644
nipkow@31952
   645
lemma multiplicity_prod_prime_powers_nat:
nipkow@31719
   646
    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
nipkow@31719
   647
       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
nipkow@31719
   648
  apply (subgoal_tac "(PROD p : S. p ^ f p) = 
nipkow@31719
   649
      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
nipkow@31719
   650
  apply (erule ssubst)
nipkow@31952
   651
  apply (subst multiplicity_characterization_nat)
nipkow@31719
   652
  prefer 5 apply (rule refl)
nipkow@31719
   653
  apply (rule refl)
nipkow@31719
   654
  apply auto
nipkow@31719
   655
  apply (subst setprod_mono_one_right)
nipkow@31719
   656
  apply assumption
nipkow@31719
   657
  prefer 3
nipkow@31719
   658
  apply (rule setprod_cong)
nipkow@31719
   659
  apply (rule refl)
nipkow@31719
   660
  apply auto
nipkow@31719
   661
done
nipkow@31719
   662
nipkow@31719
   663
(* Here the issue with transfer is the implicit quantifier over S *)
nipkow@31719
   664
nipkow@31952
   665
lemma multiplicity_prod_prime_powers_int:
nipkow@31719
   666
    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
nipkow@31719
   667
       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
nipkow@31719
   668
  apply (subgoal_tac "int ` nat ` S = S")
nipkow@31952
   669
  apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
nipkow@31719
   670
    and S = "nat ` S", transferred])
nipkow@31719
   671
  apply auto
paulson@40461
   672
  apply (metis prime_int_def)
paulson@40461
   673
  apply (metis prime_ge_0_int)
paulson@40461
   674
  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
wenzelm@44872
   675
  done
nipkow@31719
   676
nipkow@31952
   677
lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
nipkow@31719
   678
    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
nipkow@31719
   679
  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
nipkow@31719
   680
  apply (erule ssubst)
nipkow@31952
   681
  apply (subst multiplicity_prod_prime_powers_nat)
nipkow@31719
   682
  apply auto
wenzelm@44872
   683
  done
nipkow@31719
   684
nipkow@31952
   685
lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
nipkow@31719
   686
    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
nipkow@31952
   687
  apply (frule prime_ge_0_int [of q])
nipkow@31952
   688
  apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
nipkow@31719
   689
  prefer 4
nipkow@31719
   690
  apply assumption
nipkow@31719
   691
  apply auto
wenzelm@44872
   692
  done
nipkow@31719
   693
wenzelm@44872
   694
lemma dvd_multiplicity_nat:
nipkow@31719
   695
    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
wenzelm@44872
   696
  apply (cases "x = 0")
nipkow@31952
   697
  apply (auto simp add: dvd_def multiplicity_product_nat)
wenzelm@44872
   698
  done
nipkow@31719
   699
nipkow@31952
   700
lemma dvd_multiplicity_int: 
nipkow@31719
   701
    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
nipkow@31719
   702
      multiplicity p x <= multiplicity p y"
wenzelm@44872
   703
  apply (cases "x = 0")
nipkow@31719
   704
  apply (auto simp add: dvd_def)
nipkow@31719
   705
  apply (subgoal_tac "0 < k")
nipkow@31952
   706
  apply (auto simp add: multiplicity_product_int)
nipkow@31719
   707
  apply (erule zero_less_mult_pos)
nipkow@31719
   708
  apply arith
wenzelm@44872
   709
  done
nipkow@31719
   710
nipkow@31952
   711
lemma dvd_prime_factors_nat [intro]:
nipkow@31719
   712
    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
nipkow@31952
   713
  apply (simp only: prime_factors_altdef_nat)
nipkow@31719
   714
  apply auto
paulson@40461
   715
  apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
wenzelm@44872
   716
  done
nipkow@31719
   717
nipkow@31952
   718
lemma dvd_prime_factors_int [intro]:
nipkow@31719
   719
    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
nipkow@31952
   720
  apply (auto simp add: prime_factors_altdef_int)
paulson@40461
   721
  apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
wenzelm@44872
   722
  done
nipkow@31719
   723
nipkow@31952
   724
lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
wenzelm@44872
   725
    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
nipkow@31952
   726
  apply (subst prime_factorization_nat [of x], assumption)
nipkow@31952
   727
  apply (subst prime_factorization_nat [of y], assumption)
nipkow@31719
   728
  apply (rule setprod_dvd_setprod_subset2)
nipkow@31719
   729
  apply force
nipkow@31952
   730
  apply (subst prime_factors_altdef_nat)+
nipkow@31719
   731
  apply auto
paulson@40461
   732
  apply (metis gr0I le_0_eq less_not_refl)
paulson@40461
   733
  apply (metis le_imp_power_dvd)
wenzelm@44872
   734
  done
nipkow@31719
   735
nipkow@31952
   736
lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
wenzelm@44872
   737
    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
nipkow@31952
   738
  apply (subst prime_factorization_int [of x], assumption)
nipkow@31952
   739
  apply (subst prime_factorization_int [of y], assumption)
nipkow@31719
   740
  apply (rule setprod_dvd_setprod_subset2)
nipkow@31719
   741
  apply force
nipkow@31952
   742
  apply (subst prime_factors_altdef_int)+
nipkow@31719
   743
  apply auto
paulson@40461
   744
  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
wenzelm@44872
   745
  done
nipkow@31719
   746
nipkow@31952
   747
lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
nipkow@31719
   748
    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
wenzelm@44872
   749
  by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
wenzelm@44872
   750
      multiplicity_nonprime_nat neq0_conv)
nipkow@31719
   751
nipkow@31952
   752
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
nipkow@31719
   753
    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
wenzelm@44872
   754
  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
wenzelm@44872
   755
      multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
wenzelm@44872
   756
      less_le)
nipkow@31719
   757
nipkow@31952
   758
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
nipkow@31719
   759
    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
nipkow@31952
   760
  by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
nipkow@31719
   761
nipkow@31952
   762
lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
nipkow@31719
   763
    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
nipkow@31952
   764
  by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
nipkow@31719
   765
nipkow@31952
   766
lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
nipkow@31719
   767
    (p : prime_factors n) = (prime p & p dvd n)"
wenzelm@44872
   768
  apply (cases "prime p")
nipkow@31719
   769
  apply auto
nipkow@31952
   770
  apply (subst prime_factorization_nat [where n = n], assumption)
nipkow@31719
   771
  apply (rule dvd_trans) 
nipkow@31719
   772
  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
nipkow@31952
   773
  apply (subst (asm) prime_factors_altdef_nat, force)
nipkow@31719
   774
  apply (rule dvd_setprod)
nipkow@31719
   775
  apply auto
paulson@40461
   776
  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
wenzelm@44872
   777
  done
nipkow@31719
   778
nipkow@31952
   779
lemma prime_factors_altdef2_int: 
nipkow@31719
   780
  assumes "(n::int) > 0" 
nipkow@31719
   781
  shows "(p : prime_factors n) = (prime p & p dvd n)"
wenzelm@44872
   782
  apply (cases "p >= 0")
nipkow@31952
   783
  apply (rule prime_factors_altdef2_nat [transferred])
wenzelm@41541
   784
  using assms apply auto
nipkow@31952
   785
  apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
wenzelm@41541
   786
  done
nipkow@31719
   787
nipkow@31952
   788
lemma multiplicity_eq_nat:
nipkow@31719
   789
  fixes x and y::nat 
nipkow@31719
   790
  assumes [arith]: "x > 0" "y > 0" and
nipkow@31719
   791
    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
nipkow@31719
   792
  shows "x = y"
nipkow@33657
   793
  apply (rule dvd_antisym)
nipkow@31952
   794
  apply (auto intro: multiplicity_dvd'_nat) 
wenzelm@44872
   795
  done
nipkow@31719
   796
nipkow@31952
   797
lemma multiplicity_eq_int:
nipkow@31719
   798
  fixes x and y::int 
nipkow@31719
   799
  assumes [arith]: "x > 0" "y > 0" and
nipkow@31719
   800
    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
nipkow@31719
   801
  shows "x = y"
nipkow@33657
   802
  apply (rule dvd_antisym [transferred])
nipkow@31952
   803
  apply (auto intro: multiplicity_dvd'_int) 
wenzelm@44872
   804
  done
nipkow@31719
   805
nipkow@31719
   806
nipkow@31719
   807
subsection {* An application *}
nipkow@31719
   808
nipkow@31952
   809
lemma gcd_eq_nat: 
nipkow@31719
   810
  assumes pos [arith]: "x > 0" "y > 0"
nipkow@31719
   811
  shows "gcd (x::nat) y = 
nipkow@31719
   812
    (PROD p: prime_factors x Un prime_factors y. 
nipkow@31719
   813
      p ^ (min (multiplicity p x) (multiplicity p y)))"
nipkow@31719
   814
proof -
nipkow@31719
   815
  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
nipkow@31719
   816
      p ^ (min (multiplicity p x) (multiplicity p y)))"
nipkow@31719
   817
  have [arith]: "z > 0"
nipkow@31719
   818
    unfolding z_def by (rule setprod_pos_nat, auto)
nipkow@31719
   819
  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
nipkow@31719
   820
      min (multiplicity p x) (multiplicity p y)"
nipkow@31719
   821
    unfolding z_def
nipkow@31952
   822
    apply (subst multiplicity_prod_prime_powers_nat)
wenzelm@41541
   823
    apply auto
nipkow@31719
   824
    done
nipkow@31719
   825
  have "z dvd x" 
nipkow@31952
   826
    by (intro multiplicity_dvd'_nat, auto simp add: aux)
nipkow@31719
   827
  moreover have "z dvd y" 
nipkow@31952
   828
    by (intro multiplicity_dvd'_nat, auto simp add: aux)
nipkow@31719
   829
  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
nipkow@31719
   830
    apply auto
nipkow@31719
   831
    apply (case_tac "w = 0", auto)
nipkow@31952
   832
    apply (erule multiplicity_dvd'_nat)
nipkow@31952
   833
    apply (auto intro: dvd_multiplicity_nat simp add: aux)
nipkow@31719
   834
    done
nipkow@31719
   835
  ultimately have "z = gcd x y"
nipkow@31952
   836
    by (subst gcd_unique_nat [symmetric], blast)
wenzelm@44872
   837
  then show ?thesis
nipkow@31719
   838
    unfolding z_def by auto
nipkow@31719
   839
qed
nipkow@31719
   840
nipkow@31952
   841
lemma lcm_eq_nat: 
nipkow@31719
   842
  assumes pos [arith]: "x > 0" "y > 0"
nipkow@31719
   843
  shows "lcm (x::nat) y = 
nipkow@31719
   844
    (PROD p: prime_factors x Un prime_factors y. 
nipkow@31719
   845
      p ^ (max (multiplicity p x) (multiplicity p y)))"
nipkow@31719
   846
proof -
nipkow@31719
   847
  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
nipkow@31719
   848
      p ^ (max (multiplicity p x) (multiplicity p y)))"
nipkow@31719
   849
  have [arith]: "z > 0"
nipkow@31719
   850
    unfolding z_def by (rule setprod_pos_nat, auto)
nipkow@31719
   851
  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
nipkow@31719
   852
      max (multiplicity p x) (multiplicity p y)"
nipkow@31719
   853
    unfolding z_def
nipkow@31952
   854
    apply (subst multiplicity_prod_prime_powers_nat)
wenzelm@41541
   855
    apply auto
nipkow@31719
   856
    done
nipkow@31719
   857
  have "x dvd z" 
nipkow@31952
   858
    by (intro multiplicity_dvd'_nat, auto simp add: aux)
nipkow@31719
   859
  moreover have "y dvd z" 
nipkow@31952
   860
    by (intro multiplicity_dvd'_nat, auto simp add: aux)
nipkow@31719
   861
  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
nipkow@31719
   862
    apply auto
nipkow@31719
   863
    apply (case_tac "w = 0", auto)
nipkow@31952
   864
    apply (rule multiplicity_dvd'_nat)
nipkow@31952
   865
    apply (auto intro: dvd_multiplicity_nat simp add: aux)
nipkow@31719
   866
    done
nipkow@31719
   867
  ultimately have "z = lcm x y"
nipkow@31952
   868
    by (subst lcm_unique_nat [symmetric], blast)
wenzelm@44872
   869
  then show ?thesis
nipkow@31719
   870
    unfolding z_def by auto
nipkow@31719
   871
qed
nipkow@31719
   872
nipkow@31952
   873
lemma multiplicity_gcd_nat: 
nipkow@31719
   874
  assumes [arith]: "x > 0" "y > 0"
wenzelm@44872
   875
  shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
nipkow@31952
   876
  apply (subst gcd_eq_nat)
nipkow@31719
   877
  apply auto
nipkow@31952
   878
  apply (subst multiplicity_prod_prime_powers_nat)
nipkow@31719
   879
  apply auto
wenzelm@44872
   880
  done
nipkow@31719
   881
nipkow@31952
   882
lemma multiplicity_lcm_nat: 
nipkow@31719
   883
  assumes [arith]: "x > 0" "y > 0"
wenzelm@44872
   884
  shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
nipkow@31952
   885
  apply (subst lcm_eq_nat)
nipkow@31719
   886
  apply auto
nipkow@31952
   887
  apply (subst multiplicity_prod_prime_powers_nat)
nipkow@31719
   888
  apply auto
wenzelm@44872
   889
  done
nipkow@31719
   890
nipkow@31952
   891
lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
wenzelm@44872
   892
  apply (cases "x = 0 | y = 0 | z = 0") 
nipkow@31719
   893
  apply auto
nipkow@31952
   894
  apply (rule multiplicity_eq_nat)
wenzelm@44872
   895
  apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
wenzelm@44872
   896
  done
nipkow@31719
   897
nipkow@31952
   898
lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
nipkow@31952
   899
  apply (subst (1 2 3) gcd_abs_int)
nipkow@31952
   900
  apply (subst lcm_abs_int)
nipkow@31719
   901
  apply (subst (2) abs_of_nonneg)
nipkow@31719
   902
  apply force
nipkow@31952
   903
  apply (rule gcd_lcm_distrib_nat [transferred])
nipkow@31719
   904
  apply auto
wenzelm@44872
   905
  done
nipkow@31719
   906
nipkow@31719
   907
end