equal
deleted
inserted
replaced
99 Goal "even(n) ==> even(m*n)"; |
99 Goal "even(n) ==> even(m*n)"; |
100 by (auto_tac (claset(), |
100 by (auto_tac (claset(), |
101 simpset() addsimps [add_mult_distrib2, even_mult_two_ex])); |
101 simpset() addsimps [add_mult_distrib2, even_mult_two_ex])); |
102 qed "even_mult_even"; |
102 qed "even_mult_even"; |
103 Addsimps [even_mult_even]; |
103 Addsimps [even_mult_even]; |
104 |
|
105 Goal "(m*2) div 2 = (m::nat)"; |
|
106 by (rtac div_mult_self_is_m 1); |
|
107 by (Simp_tac 1); |
|
108 qed "div_mult_self_two_is_m"; |
|
109 |
104 |
110 Goal "(m + m) div 2 = (m::nat)"; |
105 Goal "(m + m) div 2 = (m::nat)"; |
111 by (asm_full_simp_tac (simpset() addsimps [m_add_m_eq2]) 1); |
106 by (asm_full_simp_tac (simpset() addsimps [m_add_m_eq2]) 1); |
112 qed "div_add_self_two_is_m"; |
107 qed "div_add_self_two_is_m"; |
113 Addsimps [div_add_self_two_is_m]; |
108 Addsimps [div_add_self_two_is_m]; |