equal
deleted
inserted
replaced
99 lemma funsum_mod: |
99 lemma funsum_mod: |
100 "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m" |
100 "funsum f k l mod m = funsum (\<lambda>i. (f i) mod m) k l mod m" |
101 apply (induct l) |
101 apply (induct l) |
102 apply auto |
102 apply auto |
103 apply (rule trans) |
103 apply (rule trans) |
104 apply (rule zmod_zadd1_eq) |
104 apply (rule mod_add_eq) |
105 apply simp |
105 apply simp |
106 apply (rule zmod_zadd_right_eq [symmetric]) |
106 apply (rule zmod_zadd_right_eq [symmetric]) |
107 done |
107 done |
108 |
108 |
109 lemma funsum_zero [rule_format (no_asm)]: |
109 lemma funsum_zero [rule_format (no_asm)]: |
235 apply auto |
235 apply auto |
236 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
236 apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) |
237 apply (unfold lincong_sol_def) |
237 apply (unfold lincong_sol_def) |
238 apply safe |
238 apply safe |
239 apply (tactic {* stac (thm "zcong_zmod") 3 *}) |
239 apply (tactic {* stac (thm "zcong_zmod") 3 *}) |
240 apply (tactic {* stac (thm "zmod_zmult_distrib") 3 *}) |
240 apply (tactic {* stac (thm "mod_mult_eq") 3 *}) |
241 apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) |
241 apply (tactic {* stac (thm "zmod_zdvd_zmod") 3 *}) |
242 apply (tactic {* stac (thm "x_sol_lin") 5 *}) |
242 apply (tactic {* stac (thm "x_sol_lin") 5 *}) |
243 apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) |
243 apply (tactic {* stac (thm "mod_mult_eq" RS sym) 7 *}) |
244 apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) |
244 apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) |
245 apply (subgoal_tac [7] |
245 apply (subgoal_tac [7] |
246 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
246 "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i |
247 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
247 \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") |
248 prefer 7 |
248 prefer 7 |