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