src/HOL/Code_Numeral.thy
 changeset 64246 15d1ee6e847b parent 64241 430d74089d4d child 64592 7759f1766189
```     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:05 2016 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Oct 16 09:31:06 2016 +0200
1.3 @@ -534,7 +534,7 @@
1.4      show "k = integer_of_int (int_of_integer k)" by simp
1.5    qed
1.6    moreover have "2 * (j div 2) = j - j mod 2"
1.7 -    by (simp add: zmult_div_cancel mult.commute)
1.8 +    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
1.9    ultimately show ?thesis
1.10      by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
1.12 @@ -548,7 +548,7 @@
1.13         (l, j) = divmod_integer k 2;
1.14         l' = 2 * int_of_integer l
1.15       in if j = 0 then l' else l' + 1)"
1.16 -  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
1.17 +  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
1.18
1.19  lemma integer_of_int_code [code]:
1.20    "integer_of_int k = (if k < 0 then - (integer_of_int (- k))
1.21 @@ -557,7 +557,7 @@
1.22         l = 2 * integer_of_int (k div 2);
1.23         j = k mod 2
1.24       in if j = 0 then l else l + 1)"
1.25 -  by (auto simp add: split_def Let_def integer_eq_iff zmult_div_cancel)
1.26 +  by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric])
1.27
1.28  hide_const (open) Pos Neg sub dup divmod_abs
1.29
```