239 by Safe_tac; |
239 by Safe_tac; |
240 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
240 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); |
241 qed "mod2_Suc_Suc"; |
241 qed "mod2_Suc_Suc"; |
242 Addsimps [mod2_Suc_Suc]; |
242 Addsimps [mod2_Suc_Suc]; |
243 |
243 |
244 (* FIXME: this thm is subsumed by the next one. Get rid of it. *) |
244 goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)"; |
245 goal thy "!!m. m mod 2 ~= 0 ==> m mod 2 = 1"; |
|
246 by (subgoal_tac "m mod 2 < 2" 1); |
245 by (subgoal_tac "m mod 2 < 2" 1); |
247 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
246 by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); |
248 by (Asm_full_simp_tac 1); |
247 by (Auto_tac()); |
249 by (trans_tac 1); |
|
250 qed "mod2_neq_0"; |
|
251 |
|
252 goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)"; |
|
253 by (rtac iffI 1); |
|
254 by(ALLGOALS (asm_full_simp_tac (simpset() addsimps [mod2_neq_0]))); |
|
255 qed "mod2_gr_0"; |
248 qed "mod2_gr_0"; |
256 Addsimps [mod2_gr_0]; |
249 Addsimps [mod2_gr_0]; |
257 |
250 |
258 goal thy "(m+m) mod 2 = 0"; |
251 goal thy "(m+m) mod 2 = 0"; |
|
252 by (induct_tac "m" 1); |
|
253 by (simp_tac (simpset() addsimps [mod_less]) 1); |
|
254 by (Asm_simp_tac 1); |
|
255 qed "mod2_add_self_eq_0"; |
|
256 Addsimps [mod2_add_self_eq_0]; |
|
257 |
|
258 goal thy "((m+m)+n) mod 2 = n mod 2"; |
259 by (induct_tac "m" 1); |
259 by (induct_tac "m" 1); |
260 by (simp_tac (simpset() addsimps [mod_less]) 1); |
260 by (simp_tac (simpset() addsimps [mod_less]) 1); |
261 by (Asm_simp_tac 1); |
261 by (Asm_simp_tac 1); |
262 qed "mod2_add_self"; |
262 qed "mod2_add_self"; |
263 Addsimps [mod2_add_self]; |
263 Addsimps [mod2_add_self]; |