src/HOL/Word/Bit_Representation.thy
changeset 45846 518a245a1ab6
parent 45845 4158f35a5c6f
child 45847 b4254b2e2b4a
equal deleted inserted replaced
45845:4158f35a5c6f 45846:518a245a1ab6
   294   bin_nth_minus_Bit0 bin_nth_minus_Bit1
   294   bin_nth_minus_Bit0 bin_nth_minus_Bit1
   295 
   295 
   296 
   296 
   297 subsection {* Truncating binary integers *}
   297 subsection {* Truncating binary integers *}
   298 
   298 
   299 definition
   299 definition bin_sign :: "int \<Rightarrow> int" where
   300   bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
   300   bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
   301 
   301 
   302 lemma bin_sign_simps [simp]:
   302 lemma bin_sign_simps [simp]:
   303   "bin_sign Int.Pls = Int.Pls"
   303   "bin_sign Int.Pls = Int.Pls"
   304   "bin_sign Int.Min = Int.Min"
   304   "bin_sign Int.Min = Int.Min"