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.11        nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    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