43 x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" |
43 x_sol :: "nat => (nat => int) => (nat => int) => (nat => int) => int" |
44 |
44 |
45 defs |
45 defs |
46 m_cond_def: |
46 m_cond_def: |
47 "m_cond n mf == |
47 "m_cond n mf == |
48 (\<forall>i. i \<le> n --> Numeral0 < mf i) \<and> |
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) = Numeral1)" |
49 (\<forall>i j. i \<le> n \<and> j \<le> n \<and> i \<noteq> j --> zgcd (mf i, mf j) = 1)" |
50 |
50 |
51 km_cond_def: |
51 km_cond_def: |
52 "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = Numeral1" |
52 "km_cond n kf mf == \<forall>i. i \<le> n --> zgcd (kf i, mf i) = 1" |
53 |
53 |
54 lincong_sol_def: |
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)" |
55 "lincong_sol n kf bf mf x == \<forall>i. i \<le> n --> zcong (kf i * x) (bf i) (mf i)" |
56 |
56 |
57 mhf_def: |
57 mhf_def: |
61 else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)" |
61 else funprod mf 0 (i - Suc 0) * funprod mf (Suc i) (n - Suc 0 - i)" |
62 |
62 |
63 xilin_sol_def: |
63 xilin_sol_def: |
64 "xilin_sol i n kf bf mf == |
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 |
65 if 0 < n \<and> i \<le> n \<and> m_cond n mf \<and> km_cond n kf mf then |
66 (SOME x. Numeral0 \<le> x \<and> x < mf i \<and> zcong (kf i * mhf mf n i * x) (bf i) (mf i)) |
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 Numeral0" |
67 else 0" |
68 |
68 |
69 x_sol_def: |
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" |
70 "x_sol n kf bf mf == funsum (\<lambda>i. xilin_sol i n kf bf mf * mhf mf n i) 0 n" |
71 |
71 |
72 |
72 |
73 text {* \medskip @{term funprod} and @{term funsum} *} |
73 text {* \medskip @{term funprod} and @{term funsum} *} |
74 |
74 |
75 lemma funprod_pos: "(\<forall>i. i \<le> n --> Numeral0 < mf i) ==> Numeral0 < funprod mf 0 n" |
75 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n" |
76 apply (induct n) |
76 apply (induct n) |
77 apply auto |
77 apply auto |
78 apply (simp add: int_0_less_mult_iff) |
78 apply (simp add: int_0_less_mult_iff) |
79 done |
79 done |
80 |
80 |
81 lemma funprod_zgcd [rule_format (no_asm)]: |
81 lemma funprod_zgcd [rule_format (no_asm)]: |
82 "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i, mf m) = Numeral1) --> |
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) = Numeral1" |
83 zgcd (funprod mf k l, mf m) = 1" |
84 apply (induct l) |
84 apply (induct l) |
85 apply simp_all |
85 apply simp_all |
86 apply (rule impI)+ |
86 apply (rule impI)+ |
87 apply (subst zgcd_zmult_cancel) |
87 apply (subst zgcd_zmult_cancel) |
88 apply auto |
88 apply auto |
108 apply simp |
108 apply simp |
109 apply (rule zmod_zadd_right_eq [symmetric]) |
109 apply (rule zmod_zadd_right_eq [symmetric]) |
110 done |
110 done |
111 |
111 |
112 lemma funsum_zero [rule_format (no_asm)]: |
112 lemma funsum_zero [rule_format (no_asm)]: |
113 "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = Numeral0) --> (funsum f k l) = Numeral0" |
113 "(\<forall>i. k \<le> i \<and> i \<le> k + l --> f i = 0) --> (funsum f k l) = 0" |
114 apply (induct l) |
114 apply (induct l) |
115 apply auto |
115 apply auto |
116 done |
116 done |
117 |
117 |
118 lemma funsum_oneelem [rule_format (no_asm)]: |
118 lemma funsum_oneelem [rule_format (no_asm)]: |
119 "k \<le> j --> j \<le> k + l --> |
119 "k \<le> j --> j \<le> k + l --> |
120 (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = Numeral0) --> |
120 (\<forall>i. k \<le> i \<and> i \<le> k + l \<and> i \<noteq> j --> f i = 0) --> |
121 funsum f k l = f j" |
121 funsum f k l = f j" |
122 apply (induct l) |
122 apply (induct l) |
123 prefer 2 |
123 prefer 2 |
124 apply clarify |
124 apply clarify |
125 defer |
125 defer |
126 apply clarify |
126 apply clarify |
127 apply (subgoal_tac "k = j") |
127 apply (subgoal_tac "k = j") |
128 apply (simp_all (no_asm_simp)) |
128 apply (simp_all (no_asm_simp)) |
129 apply (case_tac "Suc (k + n) = j") |
129 apply (case_tac "Suc (k + n) = j") |
130 apply (subgoal_tac "funsum f k n = Numeral0") |
130 apply (subgoal_tac "funsum f k n = 0") |
131 apply (rule_tac [2] funsum_zero) |
131 apply (rule_tac [2] funsum_zero) |
132 apply (subgoal_tac [3] "f (Suc (k + n)) = Numeral0") |
132 apply (subgoal_tac [3] "f (Suc (k + n)) = 0") |
133 apply (subgoal_tac [3] "j \<le> k + n") |
133 apply (subgoal_tac [3] "j \<le> k + n") |
134 prefer 4 |
134 prefer 4 |
135 apply arith |
135 apply arith |
136 apply auto |
136 apply auto |
137 done |
137 done |
173 |
173 |
174 subsection {* Chinese: existence *} |
174 subsection {* Chinese: existence *} |
175 |
175 |
176 lemma unique_xi_sol: |
176 lemma unique_xi_sol: |
177 "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf |
177 "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf |
178 ==> \<exists>!x. Numeral0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)" |
178 ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)" |
179 apply (rule zcong_lineq_unique) |
179 apply (rule zcong_lineq_unique) |
180 apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) |
180 apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) |
181 apply (unfold m_cond_def km_cond_def mhf_def) |
181 apply (unfold m_cond_def km_cond_def mhf_def) |
182 apply (simp_all (no_asm_simp)) |
182 apply (simp_all (no_asm_simp)) |
183 apply safe |
183 apply safe |
225 |
225 |
226 subsection {* Chinese *} |
226 subsection {* Chinese *} |
227 |
227 |
228 lemma chinese_remainder: |
228 lemma chinese_remainder: |
229 "0 < n ==> m_cond n mf ==> km_cond n kf mf |
229 "0 < n ==> m_cond n mf ==> km_cond n kf mf |
230 ==> \<exists>!x. Numeral0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x" |
230 ==> \<exists>!x. 0 \<le> x \<and> x < funprod mf 0 n \<and> lincong_sol n kf bf mf x" |
231 apply safe |
231 apply safe |
232 apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq) |
232 apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq) |
233 apply (rule_tac [6] zcong_funprod) |
233 apply (rule_tac [6] zcong_funprod) |
234 apply auto |
234 apply auto |
235 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
235 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
240 apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) |
240 apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) |
241 apply (tactic {* stac (thm "x_sol_lin") 5 *}) |
241 apply (tactic {* stac (thm "x_sol_lin") 5 *}) |
242 apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) |
242 apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) |
243 apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) |
243 apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) |
244 apply (subgoal_tac [7] |
244 apply (subgoal_tac [7] |
245 "Numeral0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
245 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
246 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
246 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
247 prefer 7 |
247 prefer 7 |
248 apply (simp add: zmult_ac) |
248 apply (simp add: zmult_ac) |
249 apply (unfold xilin_sol_def) |
249 apply (unfold xilin_sol_def) |
250 apply (tactic {* Asm_simp_tac 7 *}) |
250 apply (tactic {* Asm_simp_tac 7 *}) |