src/HOL/Code_Numeral.thy
changeset 66886 960509bfd47e
parent 66839 909ba5ed93dd
child 67332 cb96edae56ef
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Oct 19 17:16:13 2017 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Oct 20 07:46:10 2017 +0200
     1.3 @@ -578,16 +578,15 @@
     1.4         l'' = l' + l'
     1.5       in if j = 0 then l'' else l'' + 1)"
     1.6  proof -
     1.7 -  obtain j where "k = integer_of_int j"
     1.8 +  obtain j where k: "k = integer_of_int j"
     1.9    proof
    1.10      show "k = integer_of_int (int_of_integer k)" by simp
    1.11    qed
    1.12 -  moreover have "2 * (j div 2) = j - j mod 2"
    1.13 -    by (simp add: minus_mod_eq_mult_div [symmetric] mult.commute)
    1.14 -  ultimately show ?thesis
    1.15 -    by (auto simp add: split_def Let_def modulo_integer_def nat_of_integer_def not_le
    1.16 -      nat_add_distrib [symmetric] Suc_nat_eq_nat_zadd1)
    1.17 -      (auto simp add: mult_2 [symmetric])
    1.18 +  have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \<ge> 0"
    1.19 +    using that by transfer (simp add: nat_mod_distrib)
    1.20 +  from k show ?thesis
    1.21 +    by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric]
    1.22 +      minus_mod_eq_mult_div [symmetric] *)
    1.23  qed
    1.24  
    1.25  lemma int_of_integer_code [code]: