src/HOL/NumberTheory/Chinese.thy
 author wenzelm Fri Mar 28 19:43:54 2008 +0100 (2008-03-28) changeset 26462 dac4e2bce00d parent 23894 1a4167d761ac child 27556 292098f2efdf permissions -rw-r--r--
avoid rebinding of existing facts;
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 definition
35   m_cond :: "nat => (nat => int) => bool" where
36   "m_cond n mf =
37     ((\<forall>i. i \<le> n --> 0 < mf i) \<and>
38       (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1))"
40 definition
41   km_cond :: "nat => (nat => int) => (nat => int) => bool" where
42   "km_cond n kf mf = (\<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1)"
44 definition
45   lincong_sol ::
46     "nat => (nat => int) => (nat => int) => (nat => int) => int => bool" where
47   "lincong_sol n kf bf mf x = (\<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i))"
49 definition
50   mhf :: "(nat => int) => nat => nat => int" where
51   "mhf mf n i =
52     (if i = 0 then funprod mf (Suc 0) (n - Suc 0)
53      else if i = n then funprod mf 0 (n - Suc 0)
54      else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i))"
56 definition
57   xilin_sol ::
58     "nat => nat => (nat => int) => (nat => int) => (nat => int) => int" where
59   "xilin_sol i n kf bf mf =
60     (if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then
61         (SOME x. 0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i))
62      else 0)"
64 definition
65   x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" where
66   "x_sol n kf bf mf = funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n"
69 text {* \medskip @{term funprod} and @{term funsum} *}
71 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
72   apply (induct n)
73    apply auto
75   done
77 lemma funprod_zgcd [rule_format (no_asm)]:
78   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = 1) -->
79     zgcd (funprod mf k l, mf m) = 1"
80   apply (induct l)
81    apply simp_all
82   apply (rule impI)+
83   apply (subst zgcd_zmult_cancel)
84   apply auto
85   done
87 lemma funprod_zdvd [rule_format]:
88     "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l"
89   apply (induct l)
90    apply auto
91     apply (rule_tac [1] zdvd_zmult2)
92     apply (rule_tac [2] zdvd_zmult)
93     apply (subgoal_tac "i = Suc (k + l)")
94     apply (simp_all (no_asm_simp))
95   done
97 lemma funsum_mod:
98     "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m"
99   apply (induct l)
100    apply auto
101   apply (rule trans)
103   apply simp
105   done
107 lemma funsum_zero [rule_format (no_asm)]:
108     "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0"
109   apply (induct l)
110    apply auto
111   done
113 lemma funsum_oneelem [rule_format (no_asm)]:
114   "k \<le> j --> j \<le> k + l -->
115     (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) -->
116     funsum f k l = f j"
117   apply (induct l)
118    prefer 2
119    apply clarify
120    defer
121    apply clarify
122    apply (subgoal_tac "k = j")
123     apply (simp_all (no_asm_simp))
124   apply (case_tac "Suc (k + l) = j")
125    apply (subgoal_tac "funsum f k l = 0")
126     apply (rule_tac [2] funsum_zero)
127     apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
128      apply (subgoal_tac [3] "j \<le> k + l")
129       prefer 4
130       apply arith
131      apply auto
132   done
135 subsection {* Chinese: uniqueness *}
137 lemma zcong_funprod_aux:
138   "m_cond n mf ==> km_cond n kf mf
139     ==> lincong_sol n kf bf mf x ==> lincong_sol n kf bf mf y
140     ==> [x = y] (mod mf n)"
141   apply (unfold m_cond_def km_cond_def lincong_sol_def)
142   apply (rule iffD1)
143    apply (rule_tac k = "kf n" in zcong_cancel2)
144     apply (rule_tac [3] b = "bf n" in zcong_trans)
145      prefer 4
146      apply (subst zcong_sym)
147      defer
148      apply (rule order_less_imp_le)
149      apply simp_all
150   done
152 lemma zcong_funprod [rule_format]:
153   "m_cond n mf --> km_cond n kf mf -->
154     lincong_sol n kf bf mf x --> lincong_sol n kf bf mf y -->
155     [x = y] (mod funprod mf 0 n)"
156   apply (induct n)
157    apply (simp_all (no_asm))
158    apply (blast intro: zcong_funprod_aux)
159   apply (rule impI)+
160   apply (rule zcong_zgcd_zmult_zmod)
161     apply (blast intro: zcong_funprod_aux)
162     prefer 2
163     apply (subst zgcd_commute)
164     apply (rule funprod_zgcd)
165    apply (auto simp add: m_cond_def km_cond_def lincong_sol_def)
166   done
169 subsection {* Chinese: existence *}
171 lemma unique_xi_sol:
172   "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
173     ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
174   apply (rule zcong_lineq_unique)
175    apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
176     apply (unfold m_cond_def km_cond_def mhf_def)
177     apply (simp_all (no_asm_simp))
178   apply safe
179     apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
180      apply (rule_tac [!] funprod_zgcd)
181      apply safe
182      apply simp_all
183    apply (subgoal_tac "i<n")
184     prefer 2
185     apply arith
186    apply (case_tac [2] i)
187     apply simp_all
188   done
190 lemma x_sol_lin_aux:
191     "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i"
192   apply (unfold mhf_def)
193   apply (case_tac "i = 0")
194    apply (case_tac [2] "i = n")
195     apply (simp_all (no_asm_simp))
196     apply (case_tac [3] "j < i")
197      apply (rule_tac [3] zdvd_zmult2)
198      apply (rule_tac [4] zdvd_zmult)
199      apply (rule_tac [!] funprod_zdvd)
200      apply arith
201      apply arith
202      apply arith
203      apply arith
204      apply arith
205      apply arith
206      apply arith
207      apply arith
208   done
210 lemma x_sol_lin:
211   "0 < n ==> i \<le> n
212     ==> x_sol n kf bf mf mod mf i =
213       xilin_sol i n kf bf mf * mhf mf n i mod mf i"
214   apply (unfold x_sol_def)
215   apply (subst funsum_mod)
216   apply (subst funsum_oneelem)
217      apply auto
218   apply (subst zdvd_iff_zmod_eq_0 [symmetric])
219   apply (rule zdvd_zmult)
220   apply (rule x_sol_lin_aux)
221   apply auto
222   done
225 subsection {* Chinese *}
227 lemma chinese_remainder:
228   "0 < n ==> m_cond n mf ==> km_cond n kf mf
229     ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x"
230   apply safe
231    apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq)
232        apply (rule_tac [6] zcong_funprod)
233           apply auto
234   apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
235   apply (unfold lincong_sol_def)
236   apply safe
237     apply (tactic {* stac (thm "zcong_zmod") 3 *})
238     apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *})
239     apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *})
240       apply (tactic {* stac (thm "x_sol_lin") 5 *})
241         apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *})
242         apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *})
243         apply (subgoal_tac [7]
244           "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
245           \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
246          prefer 7