|
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 |
|
9 eta_contract:=false; |
|
10 |
|
11 open Primes; |
|
12 |
|
13 (************************************************) |
|
14 (** Divides Relation **) |
|
15 (************************************************) |
|
16 |
|
17 goalw thy [dvd_def] "m dvd 0"; |
|
18 by (fast_tac (!claset addIs [mult_0_right RS sym]) 1); |
|
19 qed "dvd_0_right"; |
|
20 Addsimps [dvd_0_right]; |
|
21 |
|
22 goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0"; |
|
23 by (fast_tac (!claset addss !simpset) 1); |
|
24 qed "dvd_0_left"; |
|
25 |
|
26 goalw thy [dvd_def] "m dvd m"; |
|
27 by (fast_tac (!claset addIs [mult_1_right RS sym]) 1); |
|
28 qed "dvd_refl"; |
|
29 Addsimps [dvd_refl]; |
|
30 |
|
31 goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p"; |
|
32 by (fast_tac (!claset addIs [mult_assoc] ) 1); |
|
33 qed "dvd_trans"; |
|
34 |
|
35 goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n"; |
|
36 by (fast_tac (!claset addDs [mult_eq_self_implies_10] |
|
37 addss (!simpset addsimps [mult_assoc, mult_eq_1_iff])) 1); |
|
38 qed "dvd_anti_sym"; |
|
39 |
|
40 |
|
41 (************************************************) |
|
42 (** Greatest Common Divisor **) |
|
43 (************************************************) |
|
44 |
|
45 (* GCD by Euclid's Algorithm *) |
|
46 |
|
47 val [rew] = goal HOL.thy "x==y ==> x=y"; |
|
48 by (rewtac rew); |
|
49 by (rtac refl 1); |
|
50 qed "equals_reflection"; |
|
51 |
|
52 goal thy "(%n m. egcd m n) = wfrec (pred_nat^+) \ |
|
53 \ (%f n m. if n=0 then m else f (m mod n) n)"; |
|
54 by (simp_tac (HOL_ss addsimps [egcd_def]) 1); |
|
55 val egcd_def1 = result() RS eq_reflection; |
|
56 |
|
57 goalw thy [egcd_def] "egcd m 0 = m"; |
|
58 by (simp_tac (!simpset addsimps [wf_pred_nat RS wf_trancl RS wfrec]) 1); |
|
59 qed "egcd_0"; |
|
60 |
|
61 goal thy "!!m. 0<n ==> egcd m n = egcd n (m mod n)"; |
|
62 by (rtac (egcd_def1 RS wf_less_trans RS fun_cong) 1); |
|
63 by (asm_simp_tac (!simpset addsimps [mod_less_divisor, cut_apply, less_eq]) 1); |
|
64 qed "egcd_less_0"; |
|
65 Addsimps [egcd_0, egcd_less_0]; |
|
66 |
|
67 goal thy "(egcd m 0) dvd m"; |
|
68 by (Simp_tac 1); |
|
69 qed "egcd_0_dvd_m"; |
|
70 |
|
71 goal thy "(egcd m 0) dvd 0"; |
|
72 by (Simp_tac 1); |
|
73 qed "egcd_0_dvd_0"; |
|
74 |
|
75 goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)"; |
|
76 by (fast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1); |
|
77 qed "dvd_add"; |
|
78 |
|
79 goalw thy [dvd_def] "!!k. k dvd m ==> k dvd (q * m)"; |
|
80 by (fast_tac (!claset addIs [mult_left_commute]) 1); |
|
81 qed "dvd_mult"; |
|
82 |
|
83 goal thy "!!k. [| k dvd n; k dvd (m mod n); 0 < n |] ==> k dvd m"; |
|
84 by (deepen_tac |
|
85 (!claset addIs [mod_div_equality RS subst] |
|
86 addSIs [dvd_add, dvd_mult]) 0 1); |
|
87 qed "gcd_ind"; |
|
88 |
|
89 |
|
90 (* Property 1: egcd m n divides m and n *) |
|
91 |
|
92 goal thy "ALL m. (egcd m n dvd m) & (egcd m n dvd n)"; |
|
93 by (res_inst_tac [("n","n")] less_induct 1); |
|
94 by (rtac allI 1); |
|
95 by (excluded_middle_tac "n=0" 1); |
|
96 (* case n = 0 *) |
|
97 by (Asm_simp_tac 2); |
|
98 (* case n > 0 *) |
|
99 by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1); |
|
100 by (eres_inst_tac [("x","m mod n")] allE 1); |
|
101 by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1); |
|
102 by (fast_tac (!claset addIs [gcd_ind]) 1); |
|
103 qed "egcd_prop1"; |
|
104 |
|
105 |
|
106 (* if f divides m and n then f divides egcd m n *) |
|
107 |
|
108 Delsimps [add_mult_distrib,add_mult_distrib2]; |
|
109 |
|
110 |
|
111 goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)"; |
|
112 by (Step_tac 1); |
|
113 by (rtac (zero_less_mult_iff RS iffD1 RS conjE) 1); |
|
114 by (REPEAT_SOME assume_tac); |
|
115 by (res_inst_tac |
|
116 [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] |
|
117 exI 1); |
|
118 by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, div_cancel, |
|
119 mult_mod_distrib, add_mult_distrib2, |
|
120 diff_add_inverse]) 1); |
|
121 qed "dvd_mod"; |
|
122 |
|
123 |
|
124 (* Property 2: for all m,n,f naturals, |
|
125 if f divides m and f divides n then f divides egcd m n*) |
|
126 goal thy "!!k. ALL m. (f dvd m) & (f dvd k) --> f dvd egcd m k"; |
|
127 by (res_inst_tac [("n","k")] less_induct 1); |
|
128 by (rtac allI 1); |
|
129 by (excluded_middle_tac "n=0" 1); |
|
130 (* case n = 0 *) |
|
131 by (Asm_simp_tac 2); |
|
132 (* case n > 0 *) |
|
133 by (Step_tac 1); |
|
134 by (asm_full_simp_tac (!simpset addsimps [zero_less_eq RS sym]) 1); |
|
135 by (eres_inst_tac [("x","m mod n")] allE 1); |
|
136 by (asm_full_simp_tac (!simpset addsimps [mod_less_divisor]) 1); |
|
137 by (fast_tac (!claset addSIs [dvd_mod]) 1); |
|
138 qed "egcd_prop2"; |
|
139 |
|
140 (* GCD PROOF : GCD exists and egcd fits the definition *) |
|
141 |
|
142 goalw thy [gcd_def] "gcd (egcd m n) m n"; |
|
143 by (asm_simp_tac (!simpset addsimps [egcd_prop1]) 1); |
|
144 by (fast_tac (!claset addIs [egcd_prop2 RS spec RS mp]) 1); |
|
145 qed "gcd"; |
|
146 |
|
147 (* GCD is unique *) |
|
148 |
|
149 goalw thy [gcd_def] "gcd m a b & gcd n a b --> m=n"; |
|
150 by (fast_tac (!claset addIs [dvd_anti_sym]) 1); |
|
151 qed "gcd_unique"; |
|
152 |