Email Gateway (Aug 18 2022 at 13:07): Email Gateway (Aug 18 2022 at 13:07):From: Nadja Levitan <inftech@gmx.de>
Hello,
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!
Regards,
Maria
Email Gateway (Aug 18 2022 at 13:09):From: Brian Huffman <brianh@cs.pdx.edu>
Using theorem search (C-x C-f in ProofGeneral), searching for "_ AND
_" and "uint" turned up the following lemma:
WordShift.mask_eq_iff: "(w AND mask n = w) = (uint w < 2 ^ n)"
Using mask_eq_iff it is straighforward to prove your lemma:
lemma "[| uint w < 256 |] ==> (w :: 16 word) AND 0x00FF = w"
proof -
assume "uint w < 256"
then have "uint w < 2^8" by simp
then have "w AND mask 8 = w" by (simp only: mask_eq_iff)
then show "w AND 0x00FF = w" by (simp add: mask_def)
qed
Quoting Nadja Levitan <inftech@gmx.de>:
Last updated: May 03 2024 at 12:27 UTC