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). *}

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,

On Feb 26, 2008, at 6:28 AM, Sascha Boehme wrote:


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.


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