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