[isabelle] And mask


sorry for my english. I would be delighted if you could help me.
I use theory WordMain and i would like to show the following lemma:

lemma "[| uint w < 256 |] ==> (w :: 16 word) AND 0x00FF = w"

w is a word with length 16 and if the value of w is < as 256, then after application of mask the value don't change.

Thanks in advance!

Computer Bild Tarifsieger! GMX FreeDSL - Telefonanschluss + DSL
für nur 17,95 ¿/mtl.!* http://dsl.gmx.de/?ac=OM.AD.PD003K11308T4569a

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