# Re: [isabelle] missing function in Word library?

Hi Sascha,
Here is the bit-segment extraction operator I've been using:
text {* Bit segment extraction operator: Given lb, mb :: int, where
lb = the least significant bit to extract, and mb = the most significant
bit to extract, then
@{term "(sliceLH lb mb w)"} extracts
bit segment [mb:lb] from bitvector w (assuming the result bitwidth
type @{typ 'b} is large enough to hold it). *}
definition

` sliceLH :: "nat \<Rightarrow> nat \<Rightarrow> 'a::len word
``\<Rightarrow> 'b::len word" where
` "sliceLH lb mb w \<equiv> ucast ((w AND mask (mb + 1)) >> lb)"
Hope this helps,
-john
On Feb 26, 2008, at 6:28 AM, Sascha Boehme wrote:

Hello,

`while studying the current (most recent) Word library, I didn't
``find a function which extracts a part from a word. I started to
``implement a function on my own, but I'm sure there must be a better
``version (especially wrt. to doing proofs on it).
`
Here is my solution:

`definition word_extract :: "'a::len0 word => int => int => 'b::len
``word"
``where "word_extract w from to = (of_bl o rev o drop (nat from) o
``take (nat to) o rev o to_bl) w"
`
I'm grateful for any hints how to improve this.
Regards,
Sascha

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*