Re: [isabelle] missing function in Word library?



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"

If that is your current definition, John's version is probably what you want (reasoning about mask and shift is easier than type conversions).

There is also the built-in "slice :: nat => 'a word => 'b word". The nat says from where to slice, the target type length says how much to slice.

Cheers,
Gerwin





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