src/HOL/NumberTheory/Chinese.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 19670 2e4a143c73c5 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
1 (*  Title:      HOL/NumberTheory/Chinese.thy
2     ID:         \$Id\$
3     Author:     Thomas M. Rasmussen
4     Copyright   2000  University of Cambridge
5 *)
7 header {* The Chinese Remainder Theorem *}
9 theory Chinese imports IntPrimes begin
11 text {*
12   The Chinese Remainder Theorem for an arbitrary finite number of
13   equations.  (The one-equation case is included in theory @{text
14   IntPrimes}.  Uses functions for indexing.\footnote{Maybe @{term
15   funprod} and @{term funsum} should be based on general @{term fold}
16   on indices?}
17 *}
20 subsection {* Definitions *}
22 consts
23   funprod :: "(nat => int) => nat => nat => int"
24   funsum :: "(nat => int) => nat => nat => int"
26 primrec
27   "funprod f i 0 = f i"
28   "funprod f i (Suc n) = f (Suc (i + n)) * funprod f i n"
30 primrec
31   "funsum f i 0 = f i"
32   "funsum f i (Suc n) = f (Suc (i + n)) + funsum f i n"
34 consts
35   m_cond :: "nat => (nat => int) => bool"
36   km_cond :: "nat => (nat => int) => (nat => int) => bool"
37   lincong_sol ::
38     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool"
40   mhf :: "(nat => int) => nat => nat => int"
41   xilin_sol ::
42     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int"
43   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int"
45 defs
46   m_cond_def:
47     "m_cond n mf ==
48       (\<forall>i. i \<le> n --> 0 < mf i) \<and>
49       (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)"
51   km_cond_def:
52     "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1"
54   lincong_sol_def:
55     "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)"
57   mhf_def:
58     "mhf mf n i ==
59       if i = 0 then funprod mf (Suc 0) (n - Suc 0)
60       else if i = n then funprod mf 0 (n - Suc 0)
61       else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)"
63   xilin_sol_def:
64     "xilin_sol i n kf bf mf ==
65       if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
66         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
67       else 0"
69   x_sol_def:
70     "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
73 text {* \medskip @{term funprod} and @{term funsum} *}
75 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
76   apply (induct n)
77    apply auto
79   done
81 lemma funprod_zgcd [rule_format (no_asm)]:
82   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
83     zgcd (funprod mf k l, mf m) = 1"
84   apply (induct l)
85    apply simp_all
86   apply (rule impI)+
87   apply (subst zgcd_zmult_cancel)
88   apply auto
89   done
91 lemma funprod_zdvd [rule_format]:
92     "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
93   apply (induct l)
94    apply auto
95     apply (rule_tac [1] zdvd_zmult2)
96     apply (rule_tac [2] zdvd_zmult)
97     apply (subgoal_tac "i = Suc (k + l)")
98     apply (simp_all (no_asm_simp))
99   done
101 lemma funsum_mod:
102     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
103   apply (induct l)
104    apply auto
105   apply (rule trans)
107   apply simp
109   done
111 lemma funsum_zero [rule_format (no_asm)]:
112     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
113   apply (induct l)
114    apply auto
115   done
117 lemma funsum_oneelem [rule_format (no_asm)]:
118   "k \<le> j --> j \<le> k + l -->
119     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
120     funsum f k l = f j"
121   apply (induct l)
122    prefer 2
123    apply clarify
124    defer
125    apply clarify
126    apply (subgoal_tac "k = j")
127     apply (simp_all (no_asm_simp))
128   apply (case_tac "Suc (k + l) = j")
129    apply (subgoal_tac "funsum f k l = 0")
130     apply (rule_tac [2] funsum_zero)
131     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
132      apply (subgoal_tac [3] "j \<le> k + l")
133       prefer 4
134       apply arith
135      apply auto
136   done
139 subsection {* Chinese: uniqueness *}
141 lemma zcong_funprod_aux:
142   "m_cond n mf ==> km_cond n kf mf
143     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
144     ==> [x = y] (mod mf n)"
145   apply (unfold m_cond_def km_cond_def lincong_sol_def)
146   apply (rule iffD1)
147    apply (rule_tac k = "kf n" in zcong_cancel2)
148     apply (rule_tac [3] b = "bf n" in zcong_trans)
149      prefer 4
150      apply (subst zcong_sym)
151      defer
152      apply (rule order_less_imp_le)
153      apply simp_all
154   done
156 lemma zcong_funprod [rule_format]:
157   "m_cond n mf --> km_cond n kf mf -->
158     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
159     [x = y] (mod funprod mf 0 n)"
160   apply (induct n)
161    apply (simp_all (no_asm))
162    apply (blast intro: zcong_funprod_aux)
163   apply (rule impI)+
164   apply (rule zcong_zgcd_zmult_zmod)
165     apply (blast intro: zcong_funprod_aux)
166     prefer 2
167     apply (subst zgcd_commute)
168     apply (rule funprod_zgcd)
169    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
170   done
173 subsection {* Chinese: existence *}
175 lemma unique_xi_sol:
176   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
177     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
178   apply (rule zcong_lineq_unique)
179    apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
180     apply (unfold m_cond_def km_cond_def mhf_def)
181     apply (simp_all (no_asm_simp))
182   apply safe
183     apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
184      apply (rule_tac [!] funprod_zgcd)
185      apply safe
186      apply simp_all
187    apply (subgoal_tac "i<n")
188     prefer 2
189     apply arith
190    apply (case_tac [2] i)
191     apply simp_all
192   done
194 lemma x_sol_lin_aux:
195     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
196   apply (unfold mhf_def)
197   apply (case_tac "i = 0")
198    apply (case_tac [2] "i = n")
199     apply (simp_all (no_asm_simp))
200     apply (case_tac [3] "j < i")
201      apply (rule_tac [3] zdvd_zmult2)
202      apply (rule_tac [4] zdvd_zmult)
203      apply (rule_tac [!] funprod_zdvd)
204           apply arith+
205   done
207 lemma x_sol_lin:
208   "0 < n ==> i \<le> n
209     ==> x_sol n kf bf mf mod mf i =
210       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
211   apply (unfold x_sol_def)
212   apply (subst funsum_mod)
213   apply (subst funsum_oneelem)
214      apply auto
215   apply (subst zdvd_iff_zmod_eq_0 [symmetric])
216   apply (rule zdvd_zmult)
217   apply (rule x_sol_lin_aux)
218   apply auto
219   done
222 subsection {* Chinese *}
224 lemma chinese_remainder:
225   "0 < n ==> m_cond n mf ==> km_cond n kf mf
226     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
227   apply safe
228    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
229        apply (rule_tac [6] zcong_funprod)
230           apply auto
231   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
232   apply (unfold lincong_sol_def)
233   apply safe
234     apply (tactic {* stac (thm "zcong_zmod") 3 *})
235     apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
236     apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
237       apply (tactic {* stac (thm "x_sol_lin") 5 *})
238         apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
239         apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
240         apply (subgoal_tac [7]
241           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
242           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
243          prefer 7