src/HOL/ex/Primes.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4356 0dfd34f0d33d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
paulson@1804
     1
(*  Title:      HOL/ex/Primes.ML
paulson@1804
     2
    ID:         $Id$
paulson@1804
     3
    Author:     Christophe Tabacznyj and Lawrence C Paulson
paulson@1804
     4
    Copyright   1996  University of Cambridge
paulson@1804
     5
paulson@1804
     6
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson@3377
     7
paulson@3377
     8
See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
paulson@1804
     9
*)
paulson@1804
    10
paulson@1804
    11
eta_contract:=false;
paulson@1804
    12
paulson@1804
    13
open Primes;
paulson@1804
    14
paulson@1804
    15
(************************************************)
paulson@1804
    16
(** Greatest Common Divisor                    **)
paulson@1804
    17
(************************************************)
paulson@1804
    18
paulson@3495
    19
(*** Euclid's Algorithm ***)
paulson@3242
    20
paulson@1804
    21
paulson@3495
    22
(** Prove the termination condition and remove it from the recursion equations
paulson@3495
    23
    and induction rule **)
paulson@3495
    24
paulson@3242
    25
Tfl.tgoalw thy [] gcd.rules;
wenzelm@4089
    26
by (simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq]) 1);
paulson@3242
    27
val tc = result();
paulson@1804
    28
paulson@3242
    29
val gcd_eq = tc RS hd gcd.rules;
paulson@3270
    30
val gcd_induct = tc RS gcd.induct;
paulson@1804
    31
paulson@3242
    32
goal thy "gcd(m,0) = m";
paulson@3242
    33
by (rtac (gcd_eq RS trans) 1);
paulson@3242
    34
by (Simp_tac 1);
paulson@3242
    35
qed "gcd_0";
paulson@1804
    36
paulson@3242
    37
goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
paulson@3242
    38
by (rtac (gcd_eq RS trans) 1);
wenzelm@4089
    39
by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
paulson@3242
    40
qed "gcd_less_0";
paulson@3242
    41
Addsimps [gcd_0, gcd_less_0];
paulson@1804
    42
paulson@3242
    43
goal thy "gcd(m,0) dvd m";
paulson@1804
    44
by (Simp_tac 1);
paulson@3242
    45
qed "gcd_0_dvd_m";
paulson@1804
    46
paulson@3242
    47
goal thy "gcd(m,0) dvd 0";
paulson@1804
    48
by (Simp_tac 1);
paulson@3242
    49
qed "gcd_0_dvd_0";
paulson@1804
    50
paulson@3242
    51
(*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
paulson@3242
    52
goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
paulson@3301
    53
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
paulson@2102
    54
by (case_tac "n=0" 1);
paulson@3242
    55
by (ALLGOALS 
wenzelm@4089
    56
    (asm_simp_tac (simpset() addsimps [mod_less_divisor,zero_less_eq])));
wenzelm@4089
    57
by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
paulson@3242
    58
qed "gcd_divides_both";
paulson@1804
    59
paulson@3242
    60
(*Maximality: for all m,n,f naturals, 
paulson@3242
    61
                if f divides m and f divides n then f divides gcd(m,n)*)
paulson@3377
    62
goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
paulson@3301
    63
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
paulson@2102
    64
by (case_tac "n=0" 1);
paulson@3242
    65
by (ALLGOALS 
wenzelm@4089
    66
    (asm_simp_tac (simpset() addsimps [dvd_mod, mod_less_divisor,
paulson@3242
    67
				      zero_less_eq])));
paulson@3242
    68
qed_spec_mp "gcd_greatest";
paulson@1804
    69
paulson@3377
    70
(*Function gcd yields the Greatest Common Divisor*)
paulson@3242
    71
goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n";
wenzelm@4089
    72
by (asm_simp_tac (simpset() addsimps [gcd_greatest, gcd_divides_both]) 1);
paulson@3242
    73
qed "is_gcd";
paulson@1804
    74
paulson@3377
    75
(*uniqueness of GCDs*)
paulson@3242
    76
goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n";
wenzelm@4089
    77
by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
paulson@3242
    78
qed "is_gcd_unique";
paulson@1804
    79
paulson@3377
    80
(*Davenport, page 27*)
paulson@3377
    81
goal thy "k * gcd(m,n) = gcd(k*m, k*n)";
paulson@3377
    82
by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
paulson@3377
    83
by (case_tac "k=0" 1);
paulson@3377
    84
by (case_tac "n=0" 2);
paulson@3377
    85
by (ALLGOALS 
wenzelm@4089
    86
    (asm_simp_tac (simpset() addsimps [mod_less_divisor, zero_less_eq,
paulson@3377
    87
				      mod_geq, mod_mult_distrib2])));
paulson@3377
    88
qed "gcd_mult_distrib2";
paulson@3377
    89
paulson@3377
    90
(*This theorem leads immediately to a proof of the uniqueness of factorization.
paulson@3377
    91
  If p divides a product of primes then it is one of those primes.*)
paulson@3377
    92
goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
paulson@3718
    93
by (Clarify_tac 1);
paulson@3377
    94
by (subgoal_tac "m = gcd(m*p, m*n)" 1);
paulson@3457
    95
by (etac ssubst 1);
paulson@3457
    96
by (rtac gcd_greatest 1);
wenzelm@4089
    97
by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_mult_distrib2 RS sym])));
paulson@3377
    98
(*Now deduce  gcd(p,n)=1  to finish the proof*)
paulson@3377
    99
by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
wenzelm@4089
   100
by (fast_tac (claset() addSss (simpset())) 1);
paulson@3377
   101
qed "prime_dvd_mult";