src/HOL/Code_Numeral.thy
changeset 68028 1f9f973eed2a
parent 68010 3f223b9a0066
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -516,6 +516,20 @@
     1.4    "k mod l = snd (divmod_integer k l)"
     1.5    by simp
     1.6  
     1.7 +definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool"
     1.8 +  where "bit_cut_integer k = (k div 2, odd k)"
     1.9 +
    1.10 +lemma bit_cut_integer_code [code]:
    1.11 +  "bit_cut_integer k = (if k = 0 then (0, False)
    1.12 +     else let (r, s) = Code_Numeral.divmod_abs k 2
    1.13 +       in (if k > 0 then r else - r - s, s = 1))"
    1.14 +proof -
    1.15 +  have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))"
    1.16 +    by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one)
    1.17 +  then show ?thesis
    1.18 +    by (simp add: divmod_integer_code) (auto simp add: split_def)
    1.19 +qed
    1.20 +
    1.21  lemma equal_integer_code [code]:
    1.22    "HOL.equal 0 (0::integer) \<longleftrightarrow> True"
    1.23    "HOL.equal 0 (Pos l) \<longleftrightarrow> False"