[isabelle] Lemma like shiftr_bl but for sshiftr in Word Library


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

Attachment: Sshiftr.thy
Description: Binary data

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