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