equal
deleted
inserted
replaced
272 have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" |
272 have "(nat_of k div 2) * 2 + nat_of k mod 2 = nat_of k" |
273 by (rule mod_div_equality) |
273 by (rule mod_div_equality) |
274 then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" |
274 then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" |
275 by simp |
275 by simp |
276 then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" |
276 then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" |
277 unfolding int_mult zadd_int [symmetric] by simp |
277 unfolding of_nat_mult of_nat_add by simp |
278 then show ?thesis by (auto simp add: int_of_def mult_ac) |
278 then show ?thesis by (auto simp add: int_of_def mult_ac) |
279 qed |
279 qed |
280 |
280 |
281 hide_const (open) of_nat nat_of int_of |
281 hide_const (open) of_nat nat_of int_of |
282 |
282 |