--- a/src/HOL/Word/Bits_Int.thy Sat Dec 28 21:06:25 2013 +0100
+++ b/src/HOL/Word/Bits_Int.thy Sat Dec 28 21:06:26 2013 +0100
@@ -384,14 +384,14 @@
subsection {* Setting and clearing bits *}
+(** nth bit, set/clear **)
+
primrec
bin_sc :: "nat => bool => int => int"
where
Z: "bin_sc 0 b w = bin_rest w BIT b"
| Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
-(** nth bit, set/clear **)
-
lemma bin_nth_sc [simp]:
"bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
by (induct n arbitrary: w) auto
--- a/src/HOL/Word/Bool_List_Representation.thy Sat Dec 28 21:06:25 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Sat Dec 28 21:06:26 2013 +0100
@@ -9,7 +9,7 @@
header "Bool lists and integers"
theory Bool_List_Representation
-imports Bits_Int
+imports Main Bits_Int
begin
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -1141,4 +1141,42 @@
apply (rule refl)
done
+
+text {* Even more bit operations *}
+
+instantiation int :: bitss
+begin
+
+definition [iff]:
+ "i !! n \<longleftrightarrow> bin_nth i n"
+
+definition
+ "lsb i = (i :: int) !! 0"
+
+definition
+ "set_bit i n b = bin_sc n b i"
+
+definition
+ "set_bits f =
+ (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+ in bl_to_bin (rev (map f [0..<n]))
+ else if \<exists>n. \<forall>n'\<ge>n. f n' then
+ let n = LEAST n. \<forall>n'\<ge>n. f n'
+ in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+ else 0 :: int)"
+
+definition
+ "shiftl x n = (x :: int) * 2 ^ n"
+
+definition
+ "shiftr x n = (x :: int) div 2 ^ n"
+
+definition
+ "msb x \<longleftrightarrow> (x :: int) < 0"
+
+instance ..
+
end
+
+end