# HG changeset patch
# User haftmann
# Date 1388261186 -3600
# Node ID c55c5dacd6a1af601621636538e77d3b7ce580df
# Parent  c92a0e6ba828974f2b76826153f28d69bc6b22ab
move instantiation here from AFP/Native_Word

diff -r c92a0e6ba828 -r c55c5dacd6a1 src/HOL/Word/Bits_Int.thy
--- 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
diff -r c92a0e6ba828 -r c55c5dacd6a1 src/HOL/Word/Bool_List_Representation.thy
--- 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