|
1 (* Title: Chinese.ML |
|
2 ID: $Id$ |
|
3 Author: Thomas M. Rasmussen |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 The Chinese Remainder Theorem for an arbitrary finite number of equations. |
|
7 (The one-equation case is included in 'IntPrimes') |
|
8 |
|
9 Uses functions for indexing. Maybe 'funprod' and 'funsum' |
|
10 should be based on general 'fold' on indices? |
|
11 *) |
|
12 |
|
13 |
|
14 (*** extra nat theorems ***) |
|
15 |
|
16 Goal "[| k <= i; i <= k |] ==> i = (k::nat)"; |
|
17 by (rtac diffs0_imp_equal 1); |
|
18 by (ALLGOALS (stac diff_is_0_eq)); |
|
19 by Auto_tac; |
|
20 qed "le_le_imp_eq"; |
|
21 |
|
22 Goal "m~=n --> m<=n --> m<(n::nat)"; |
|
23 by (induct_tac "n" 1); |
|
24 by Auto_tac; |
|
25 by (subgoal_tac "m = Suc n" 1); |
|
26 by (rtac le_le_imp_eq 2); |
|
27 by Auto_tac; |
|
28 qed_spec_mp "neq_le_imp_less"; |
|
29 |
|
30 |
|
31 (*** funprod and funsum ***) |
|
32 |
|
33 Goal "(ALL i. i <= n --> #0 < mf i) --> #0 < funprod mf 0 n"; |
|
34 by (induct_tac "n" 1); |
|
35 by Auto_tac; |
|
36 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
|
37 qed_spec_mp "funprod_pos"; |
|
38 |
|
39 Goal "(ALL i. k<=i & i<=(k+l) --> zgcd (mf i, mf m) = #1) --> \ |
|
40 \ #0 < mf m --> zgcd (funprod mf k l, mf m) = #1"; |
|
41 by (induct_tac "l" 1); |
|
42 by (ALLGOALS Simp_tac); |
|
43 by (REPEAT (rtac impI 1)); |
|
44 by (stac zgcd_zmult_cancel 1); |
|
45 by Auto_tac; |
|
46 qed_spec_mp "funprod_zgcd"; |
|
47 |
|
48 Goal "k<=i --> i<=(k+l) --> (mf i) dvd (funprod mf k l)"; |
|
49 by (induct_tac "l" 1); |
|
50 by Auto_tac; |
|
51 by (rtac zdvd_zmult2 2); |
|
52 by (rtac zdvd_zmult 3); |
|
53 by (subgoal_tac "i=k" 1); |
|
54 by (subgoal_tac "i=Suc (k + n)" 3); |
|
55 by (ALLGOALS Asm_simp_tac); |
|
56 qed_spec_mp "funprod_zdvd"; |
|
57 |
|
58 Goal "(funsum f k l) mod m = (funsum (%i. (f i) mod m) k l) mod m"; |
|
59 by (induct_tac "l" 1); |
|
60 by Auto_tac; |
|
61 by (rtac trans 1); |
|
62 by (rtac zmod_zadd1_eq 1); |
|
63 by (Asm_simp_tac 1); |
|
64 by (rtac (zmod_zadd_right_eq RS sym) 1); |
|
65 qed "funsum_mod"; |
|
66 |
|
67 Goal "(ALL i. k<=i & i<=(k+l) --> (f i) = #0) --> (funsum f k l) = #0"; |
|
68 by (induct_tac "l" 1); |
|
69 by Auto_tac; |
|
70 qed_spec_mp "funsum_zero"; |
|
71 |
|
72 Goal "k<=j --> j<=(k+l) --> \ |
|
73 \ (ALL i. k<=i & i<=(k+l) & i~=j --> (f i) = #0) --> \ |
|
74 \ (funsum f k l) = (f j)"; |
|
75 by (induct_tac "l" 1); |
|
76 by (ALLGOALS Simp_tac); |
|
77 by (ALLGOALS (REPEAT o (rtac impI))); |
|
78 by (case_tac "Suc (k+n) = j" 2); |
|
79 by (subgoal_tac "funsum f k n = #0" 2); |
|
80 by (rtac funsum_zero 3); |
|
81 by (subgoal_tac "f (Suc (k+n)) = #0" 4); |
|
82 by (subgoal_tac "k=j" 1); |
|
83 by (Clarify_tac 4); |
|
84 by (subgoal_tac "j<=k+n" 5); |
|
85 by (subgoal_tac "j<Suc (k+n)" 6); |
|
86 by (rtac neq_le_imp_less 7); |
|
87 by (ALLGOALS Asm_simp_tac); |
|
88 by Auto_tac; |
|
89 qed_spec_mp "funsum_oneelem"; |
|
90 |
|
91 |
|
92 (*** Chinese: Uniqueness ***) |
|
93 |
|
94 Goalw [m_cond_def,km_cond_def,lincong_sol_def] |
|
95 "[| m_cond n mf; km_cond n kf mf; \ |
|
96 \ lincong_sol n kf bf mf x; lincong_sol n kf bf mf y |] \ |
|
97 \ ==> [x=y] (mod mf n)"; |
|
98 by (rtac iffD1 1); |
|
99 by (res_inst_tac [("k","kf n")] zcong_cancel2 1); |
|
100 by (res_inst_tac [("b","bf n")] zcong_trans 3); |
|
101 by (stac zcong_sym 4); |
|
102 by (rtac zless_imp_zle 1); |
|
103 by (ALLGOALS Asm_simp_tac); |
|
104 val lemma = result(); |
|
105 |
|
106 Goal "m_cond n mf --> km_cond n kf mf --> \ |
|
107 \ lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y --> \ |
|
108 \ [x=y] (mod funprod mf 0 n)"; |
|
109 by (induct_tac "n" 1); |
|
110 by (ALLGOALS Simp_tac); |
|
111 by (blast_tac (claset() addIs [lemma]) 1); |
|
112 by (REPEAT (rtac impI 1)); |
|
113 by (rtac zcong_zgcd_zmult_zmod 1); |
|
114 by (blast_tac (claset() addIs [lemma]) 3); |
|
115 by (stac zgcd_commute 4); |
|
116 by (rtac funprod_zgcd 6); |
|
117 by (rtac funprod_pos 5); |
|
118 by (rtac funprod_pos 2); |
|
119 by (rewrite_goals_tac [m_cond_def,km_cond_def,lincong_sol_def]); |
|
120 by Auto_tac; |
|
121 qed_spec_mp "zcong_funprod"; |
|
122 |
|
123 |
|
124 (* Chinese: Existence *) |
|
125 |
|
126 Goal "[| 0<n; i<n |] ==> Suc (i+(n-Suc(i))) = n"; |
|
127 by (subgoal_tac "Suc (i+(n-1-i)) = n" 1); |
|
128 by (stac le_add_diff_inverse 2); |
|
129 by (stac le_pred_eq 2); |
|
130 by Auto_tac; |
|
131 val suclemma = result(); |
|
132 |
|
133 Goal "[| 0<n; i<=n; m_cond n mf; km_cond n kf mf |] \ |
|
134 \ ==> EX! x. #0<=x & x<(mf i) & \ |
|
135 \ [(kf i)*(mhf mf n i)*x = bf i] (mod mf i)"; |
|
136 by (rtac zcong_lineq_unique 1); |
|
137 by (stac zgcd_zmult_cancel 2); |
|
138 by (rewrite_goals_tac [m_cond_def,km_cond_def,mhf_def]); |
|
139 by (case_tac "i=0" 4); |
|
140 by (case_tac "i=n" 5); |
|
141 by (ALLGOALS Asm_simp_tac); |
|
142 by (stac zgcd_zmult_cancel 3); |
|
143 by (Asm_simp_tac 3); |
|
144 by (ALLGOALS (rtac funprod_zgcd)); |
|
145 by Safe_tac; |
|
146 by (ALLGOALS Asm_full_simp_tac); |
|
147 by (subgoal_tac "i<=n" 1); |
|
148 by (res_inst_tac [("j","n-1")] le_trans 2); |
|
149 by (subgoal_tac "i~=n" 1); |
|
150 by (subgoal_tac "ia<=n" 5); |
|
151 by (res_inst_tac [("j","i-1")] le_trans 6); |
|
152 by (res_inst_tac [("j","n-1")] le_trans 7); |
|
153 by (subgoal_tac "ia~=i" 5); |
|
154 by (subgoal_tac "ia<=n" 10); |
|
155 by (stac (suclemma RS sym) 11); |
|
156 by (assume_tac 13); |
|
157 by (rtac neq_le_imp_less 12); |
|
158 by (rtac diff_le_mono 8); |
|
159 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [le_pred_eq]))); |
|
160 qed "unique_xi_sol"; |
|
161 |
|
162 Goalw [mhf_def] "[| 0<n; i<=n; j<=n; j~=i |] ==> (mf j) dvd (mhf mf n i)"; |
|
163 by (case_tac "i=0" 1); |
|
164 by (case_tac "i=n" 2); |
|
165 by (ALLGOALS Asm_simp_tac); |
|
166 by (case_tac "j<i" 3); |
|
167 by (rtac zdvd_zmult2 3); |
|
168 by (rtac zdvd_zmult 4); |
|
169 by (ALLGOALS (rtac funprod_zdvd)); |
|
170 by Auto_tac; |
|
171 by (stac suclemma 4); |
|
172 by (stac le_pred_eq 2); |
|
173 by (stac le_pred_eq 1); |
|
174 by (rtac neq_le_imp_less 2); |
|
175 by (rtac neq_le_imp_less 8); |
|
176 by (rtac pred_less_imp_le 6); |
|
177 by (rtac neq_le_imp_less 6); |
|
178 by Auto_tac; |
|
179 val lemma = result(); |
|
180 |
|
181 Goalw [x_sol_def] "[| 0<n; i<=n |] \ |
|
182 \ ==> (x_sol n kf bf mf) mod (mf i) = \ |
|
183 \ (xilin_sol i n kf bf mf)*(mhf mf n i) mod (mf i)"; |
|
184 by (stac funsum_mod 1); |
|
185 by (stac funsum_oneelem 1); |
|
186 by Auto_tac; |
|
187 by (stac (zdvd_iff_zmod_eq_0 RS sym) 1); |
|
188 by (rtac zdvd_zmult 1); |
|
189 by (rtac lemma 1); |
|
190 by Auto_tac; |
|
191 qed "x_sol_lin"; |
|
192 |
|
193 |
|
194 (* Chinese *) |
|
195 |
|
196 Goal "EX! a. P a ==> P (@ a. P a)"; |
|
197 by Auto_tac; |
|
198 by (stac select_equality 1); |
|
199 by Auto_tac; |
|
200 val delemma = result(); |
|
201 |
|
202 Goal "[| 0<n; m_cond n mf; km_cond n kf mf |] \ |
|
203 \ ==> (EX! x. #0 <= x & x < (funprod mf 0 n) & \ |
|
204 \ (lincong_sol n kf bf mf x))"; |
|
205 by Safe_tac; |
|
206 by (res_inst_tac [("m","funprod mf 0 n")] zcong_zless_imp_eq 2); |
|
207 by (rtac zcong_funprod 6); |
|
208 by Auto_tac; |
|
209 by (res_inst_tac [("x","(x_sol n kf bf mf) mod (funprod mf 0 n)")] exI 1); |
|
210 by (rewtac lincong_sol_def); |
|
211 by Safe_tac; |
|
212 by (stac zcong_zmod 3); |
|
213 by (stac zmod_zmult_distrib 3); |
|
214 by (stac zmod_zdvd_zmod 3); |
|
215 by (stac x_sol_lin 5); |
|
216 by (stac (zmod_zmult_distrib RS sym) 7); |
|
217 by (stac (zcong_zmod RS sym) 7); |
|
218 by (subgoal_tac "#0<=(xilin_sol i n kf bf mf) & \ |
|
219 \ (xilin_sol i n kf bf mf)<(mf i) & \ |
|
220 \ [(kf i)*(mhf mf n i)*(xilin_sol i n kf bf mf) = bf i] \ |
|
221 \ (mod mf i)" 7); |
|
222 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7); |
|
223 by (rewtac xilin_sol_def); |
|
224 by (Asm_simp_tac 7); |
|
225 by (rtac delemma 7); |
|
226 by (rtac unique_xi_sol 7); |
|
227 by (rtac funprod_zdvd 4); |
|
228 by (rewtac m_cond_def); |
|
229 by (rtac (funprod_pos RS pos_mod_sign) 1); |
|
230 by (rtac (funprod_pos RS pos_mod_bound) 2); |
|
231 by Auto_tac; |
|
232 qed "chinese_remainder"; |