164 |
164 |
165 lemma unique_xi_sol: |
165 lemma unique_xi_sol: |
166 "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf |
166 "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf |
167 ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)" |
167 ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)" |
168 apply (rule zcong_lineq_unique) |
168 apply (rule zcong_lineq_unique) |
169 apply (tactic {* stac @{thm zgcd_zmult_cancel} 2 *}) |
169 apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 2 *}) |
170 apply (unfold m_cond_def km_cond_def mhf_def) |
170 apply (unfold m_cond_def km_cond_def mhf_def) |
171 apply (simp_all (no_asm_simp)) |
171 apply (simp_all (no_asm_simp)) |
172 apply safe |
172 apply safe |
173 apply (tactic {* stac @{thm zgcd_zmult_cancel} 3 *}) |
173 apply (tactic {* stac @{context} @{thm zgcd_zmult_cancel} 3 *}) |
174 apply (rule_tac [!] funprod_zgcd) |
174 apply (rule_tac [!] funprod_zgcd) |
175 apply safe |
175 apply safe |
176 apply simp_all |
176 apply simp_all |
177 apply (subgoal_tac "ia<n") |
177 apply (subgoal_tac "ia<n") |
178 prefer 2 |
178 prefer 2 |
226 apply (rule_tac [6] zcong_funprod) |
226 apply (rule_tac [6] zcong_funprod) |
227 apply auto |
227 apply auto |
228 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
228 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
229 apply (unfold lincong_sol_def) |
229 apply (unfold lincong_sol_def) |
230 apply safe |
230 apply safe |
231 apply (tactic {* stac @{thm zcong_zmod} 3 *}) |
231 apply (tactic {* stac @{context} @{thm zcong_zmod} 3 *}) |
232 apply (tactic {* stac @{thm mod_mult_eq} 3 *}) |
232 apply (tactic {* stac @{context} @{thm mod_mult_eq} 3 *}) |
233 apply (tactic {* stac @{thm mod_mod_cancel} 3 *}) |
233 apply (tactic {* stac @{context} @{thm mod_mod_cancel} 3 *}) |
234 apply (tactic {* stac @{thm x_sol_lin} 4 *}) |
234 apply (tactic {* stac @{context} @{thm x_sol_lin} 4 *}) |
235 apply (tactic {* stac (@{thm mod_mult_eq} RS sym) 6 *}) |
235 apply (tactic {* stac @{context} (@{thm mod_mult_eq} RS sym) 6 *}) |
236 apply (tactic {* stac (@{thm zcong_zmod} RS sym) 6 *}) |
236 apply (tactic {* stac @{context} (@{thm zcong_zmod} RS sym) 6 *}) |
237 apply (subgoal_tac [6] |
237 apply (subgoal_tac [6] |
238 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
238 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
239 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
239 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
240 prefer 6 |
240 prefer 6 |
241 apply (simp add: ac_simps) |
241 apply (simp add: ac_simps) |