src/HOL/Word/Bit_Representation.thy

 imports Misc_Numeric
 begin
 
 subsection {* Constructors and destructors for binary integers *}
 
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) where
+definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
+where
   "k BIT b = (if b then 1 else 0) + k + k"
 
 lemma Bit_B0:
   "k BIT False = k + k"
    by (unfold Bit_def) simp

   by (rule trans, rule Bit_B0) simp
 
 lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
   by (rule trans, rule Bit_B1) simp
 
-definition bin_last :: "int \<Rightarrow> bool" where
+definition bin_last :: "int \<Rightarrow> bool"
+where
   "bin_last w \<longleftrightarrow> w mod 2 = 1"
 
 lemma bin_last_odd:
   "bin_last = odd"
   by (rule ext) (simp add: bin_last_def even_def)
 
-definition bin_rest :: "int \<Rightarrow> int" where
+definition bin_rest :: "int \<Rightarrow> int"
+where
   "bin_rest w = w div 2"
 
 lemma bin_rl_simp [simp]:
   "bin_rest w BIT bin_last w = w"
   unfolding bin_rest_def bin_last_def Bit_def

   bin_nth_numeral_simps
 
 
 subsection {* Truncating binary integers *}
 
-definition bin_sign :: "int \<Rightarrow> int" where
+definition bin_sign :: "int \<Rightarrow> int"
+where
   bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
 
 lemma bin_sign_simps [simp]:
   "bin_sign 0 = 0"
   "bin_sign 1 = 0"