src/HOL/NumberTheory/Primes.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10142 d1d61d13e461
child 10789 260fa2c67e3e
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9944
diff changeset
     1
(*  Title:      HOL/NumberTheory/Primes.thy
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     2
    ID:         $Id$
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     3
    Author:     Christophe Tabacznyj and Lawrence C Paulson
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     5
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     6
The Greatest Common Divisor and Euclid's algorithm
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     7
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     8
See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     9
*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    10
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    11
theory Primes = Main:
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    12
consts
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    13
  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    14
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    15
recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    16
    "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    17
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    18
constdefs
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    19
  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    20
    "is_gcd p m n == p dvd m  &  p dvd n  &
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    21
                     (ALL d. d dvd m & d dvd n --> d dvd p)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    22
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    23
  coprime :: "[nat,nat]=>bool"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    24
    "coprime m n == gcd(m,n) = 1"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    25
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    26
  prime   :: "nat set"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    27
    "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    28
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    29
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    30
(************************************************)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    31
(** Greatest Common Divisor                    **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    32
(************************************************)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    33
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    34
(*** Euclid's Algorithm ***)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    35
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    36
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    37
lemma gcd_induct:
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    38
     "[| !!m. P m 0;     
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    39
         !!m n. [| 0<n;  P n (m mod n) |] ==> P m n  
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    40
      |] ==> P (m::nat) (n::nat)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    41
  apply (induct_tac m n rule: gcd.induct)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    42
  apply (case_tac "n=0")
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    43
  apply (simp_all)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    44
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    45
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    46
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    47
lemma gcd_0 [simp]: "gcd(m,0) = m"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    48
  apply (simp);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    49
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    50
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    51
lemma gcd_non_0: "0<n ==> gcd(m,n) = gcd (n, m mod n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    52
  apply (simp)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    53
  done;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    54
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    55
declare gcd.simps [simp del];
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    56
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    57
lemma gcd_1 [simp]: "gcd(m,1) = 1"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    58
  apply (simp add: gcd_non_0)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    59
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    60
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    61
(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    62
lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    63
  apply (induct_tac m n rule: gcd_induct)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    64
  apply (simp_all add: gcd_non_0)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    65
  apply (blast dest: dvd_mod_imp_dvd)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    66
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    67
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    68
lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    69
lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    70
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    71
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    72
(*Maximality: for all m,n,k naturals, 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    73
                if k divides m and k divides n then k divides gcd(m,n)*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    74
lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    75
  apply (induct_tac m n rule: gcd_induct)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    76
  apply (simp_all add: gcd_non_0 dvd_mod);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    77
  done;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    78
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    79
lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    80
  apply (blast intro!: gcd_greatest intro: dvd_trans);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    81
  done;
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    82
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    83
(*Function gcd yields the Greatest Common Divisor*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    84
lemma is_gcd: "is_gcd (gcd(m,n)) m n"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    85
  apply (simp add: is_gcd_def gcd_greatest)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    86
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    87
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    88
(*uniqueness of GCDs*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    89
lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    90
  apply (simp add: is_gcd_def);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    91
  apply (blast intro: dvd_anti_sym)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    92
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    93
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    94
lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    95
  apply (auto simp add: is_gcd_def);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    96
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    97
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    98
(** Commutativity **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    99
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   100
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   101
  apply (auto simp add: is_gcd_def);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   102
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   103
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   104
lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   105
  apply (rule is_gcd_unique)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   106
  apply (rule is_gcd)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   107
  apply (subst is_gcd_commute)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   108
  apply (simp add: is_gcd)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   109
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   110
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   111
lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   112
  apply (rule is_gcd_unique)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   113
  apply (rule is_gcd)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   114
  apply (simp add: is_gcd_def);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   115
  apply (blast intro: dvd_trans);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   116
  done 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   117
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   118
lemma gcd_0_left [simp]: "gcd(0,m) = m"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   119
  apply (simp add: gcd_commute [of 0])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   120
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   121
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   122
lemma gcd_1_left [simp]: "gcd(1,m) = 1"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   123
  apply (simp add: gcd_commute [of 1])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   124
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   125
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   126
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   127
(** Multiplication laws **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   128
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   129
(*Davenport, page 27*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   130
lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   131
  apply (induct_tac m n rule: gcd_induct)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   132
  apply (simp)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   133
  apply (case_tac "k=0")
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   134
  apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   135
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   136
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   137
lemma gcd_mult [simp]: "gcd(k, k*n) = k"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   138
  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   139
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   140
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   141
lemma gcd_self [simp]: "gcd(k,k) = k"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   142
  apply (rule gcd_mult [of k 1, simplified])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   143
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   144
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   145
lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   146
  apply (insert gcd_mult_distrib2 [of m k n])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   147
  apply (simp)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   148
  apply (erule_tac t="m" in ssubst);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   149
  apply (simp)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   150
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   151
10142
d1d61d13e461 unsymbolized;
wenzelm
parents: 9944
diff changeset
   152
lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> k dvd (m*n) = k dvd m";
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   153
  apply (blast intro: relprime_dvd_mult dvd_trans)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   154
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   155
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   156
lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   157
  apply (auto simp add: prime_def)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   158
  apply (drule_tac x="gcd(p,n)" in spec)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   159
  apply auto
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   160
  apply (insert gcd_dvd2 [of p n])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   161
  apply (simp)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   162
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   163
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   164
(*This theorem leads immediately to a proof of the uniqueness of factorization.
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   165
  If p divides a product of primes then it is one of those primes.*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   166
lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   167
  apply (blast intro: relprime_dvd_mult prime_imp_relprime)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   168
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   169
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   170
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   171
(** Addition laws **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   172
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   173
lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   174
  apply (case_tac "n=0")
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   175
  apply (simp_all add: gcd_non_0)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   176
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   177
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   178
lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   179
  apply (rule gcd_commute [THEN trans])
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   180
  apply (subst add_commute)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   181
  apply (simp add: gcd_add1)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   182
  apply (rule gcd_commute)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   183
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   184
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   185
lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   186
  apply (subst add_commute)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   187
  apply (rule gcd_add2)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   188
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   189
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   190
lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   191
  apply (induct_tac "k")
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   192
  apply (simp_all add: gcd_add2 add_assoc)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   193
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   194
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   195
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   196
(** More multiplication laws **)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   197
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   198
lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   199
  apply (rule dvd_anti_sym)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   200
   apply (rule gcd_greatest)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   201
    apply (rule_tac n="k" in relprime_dvd_mult)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   202
     apply (simp add: gcd_assoc)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   203
     apply (simp add: gcd_commute)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   204
    apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   205
  apply (blast intro: gcd_dvd1 dvd_trans);
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   206
  done
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   207
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
   208
end