1804
|
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 |
|