[isabelle] missing function in Word library?


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.