equal
deleted
inserted
replaced
88 |
88 |
89 lemma funprod_zdvd [rule_format]: |
89 lemma funprod_zdvd [rule_format]: |
90 "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l" |
90 "k \<le> i --> i \<le> k + l --> mf i dvd funprod mf k l" |
91 apply (induct l) |
91 apply (induct l) |
92 apply auto |
92 apply auto |
93 apply (rule_tac [1] zdvd_zmult2) |
93 apply (subgoal_tac "i = Suc (k + l)") |
94 apply (rule_tac [2] zdvd_zmult) |
94 apply (simp_all (no_asm_simp)) |
95 apply (subgoal_tac "i = Suc (k + l)") |
|
96 apply (simp_all (no_asm_simp)) |
|
97 done |
95 done |
98 |
96 |
99 lemma funsum_mod: |
97 lemma funsum_mod: |
100 "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m" |
98 "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m" |
101 apply (induct l) |
99 apply (induct l) |
194 apply (unfold mhf_def) |
192 apply (unfold mhf_def) |
195 apply (case_tac "i = 0") |
193 apply (case_tac "i = 0") |
196 apply (case_tac [2] "i = n") |
194 apply (case_tac [2] "i = n") |
197 apply (simp_all (no_asm_simp)) |
195 apply (simp_all (no_asm_simp)) |
198 apply (case_tac [3] "j < i") |
196 apply (case_tac [3] "j < i") |
199 apply (rule_tac [3] zdvd_zmult2) |
197 apply (rule_tac [3] dvd_mult2) |
200 apply (rule_tac [4] zdvd_zmult) |
198 apply (rule_tac [4] dvd_mult) |
201 apply (rule_tac [!] funprod_zdvd) |
199 apply (rule_tac [!] funprod_zdvd) |
202 apply arith |
200 apply arith |
203 apply arith |
201 apply arith |
204 apply arith |
202 apply arith |
205 apply arith |
203 apply arith |
215 xilin_sol i n kf bf mf * mhf mf n i mod mf i" |
213 xilin_sol i n kf bf mf * mhf mf n i mod mf i" |
216 apply (unfold x_sol_def) |
214 apply (unfold x_sol_def) |
217 apply (subst funsum_mod) |
215 apply (subst funsum_mod) |
218 apply (subst funsum_oneelem) |
216 apply (subst funsum_oneelem) |
219 apply auto |
217 apply auto |
220 apply (subst zdvd_iff_zmod_eq_0 [symmetric]) |
218 apply (subst dvd_eq_mod_eq_0 [symmetric]) |
221 apply (rule zdvd_zmult) |
219 apply (rule dvd_mult) |
222 apply (rule x_sol_lin_aux) |
220 apply (rule x_sol_lin_aux) |
223 apply auto |
221 apply auto |
224 done |
222 done |
225 |
223 |
226 |
224 |