src/HOL/Library/Code_Target_Int.thy
changeset 60868 dd18c33c001e
parent 60500 903bb1495239
child 61275 053ec04ea866
     1.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Aug 06 23:56:48 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sat Aug 08 10:51:33 2015 +0200
     1.3 @@ -71,11 +71,6 @@
     1.4    by simp
     1.5  
     1.6  lemma [code]:
     1.7 -  "Divides.divmod_abs k l = map_prod int_of_integer int_of_integer
     1.8 -    (Code_Numeral.divmod_abs (of_int k) (of_int l))"
     1.9 -  by (simp add: prod_eq_iff)
    1.10 -
    1.11 -lemma [code]:
    1.12    "k div l = int_of_integer (of_int k div of_int l)"
    1.13    by simp
    1.14  
    1.15 @@ -100,14 +95,13 @@
    1.16    "of_int k = (if k = 0 then 0
    1.17       else if k < 0 then - of_int (- k)
    1.18       else let
    1.19 -       (l, j) = divmod_int k 2;
    1.20 -       l' = 2 * of_int l
    1.21 -     in if j = 0 then l' else l' + 1)"
    1.22 +       l = 2 * of_int (k div 2);
    1.23 +       j = k mod 2
    1.24 +     in if j = 0 then l else l + 1)"
    1.25  proof -
    1.26    from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
    1.27    show ?thesis
    1.28 -    by (simp add: Let_def divmod_int_mod_div of_int_add [symmetric])
    1.29 -      (simp add: * mult.commute)
    1.30 +    by (simp add: Let_def of_int_add [symmetric]) (simp add: * mult.commute)
    1.31  qed
    1.32  
    1.33  declare of_int_code_if [code]
    1.34 @@ -121,4 +115,3 @@
    1.35      (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.36  
    1.37  end
    1.38 -