Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lemma like shiftr_bl but for sshiftr in Word L...

view this post on Zulip Email Gateway (Apr 18 2021 at 18:35):

From: Florian Märkl <isabelle-users@florianmaerkl.de>
Hello,

I noticed the Word Library has lemmas to give a list representation for both bit shifts (<<) and (>>) in Reversed_Bit_Lists.thy, which I made use of in my current project, e.g.:

lemma shiftr_bl: "x >> n ≡ of_bl (take (LENGTH('a) - n) (to_bl x))“
…

I also needed a similar equation for signed right shift (>>>), but could not find it, so I formalized it myself (see the attachment).
Should something like this be added to the library? Or did I maybe not search hard enough?

Florian Märkl
Sshiftr.thy

view this post on Zulip Email Gateway (Apr 18 2021 at 22:22):

From: Gerwin Klein <kleing@unsw.edu.au>
Nice! Thanks for the contribution, I'll add it to Word_Lib in the afp.

Cheers,
Gerwin

Last updated: Apr 19 2024 at 12:27 UTC