Re: [isabelle] And mask



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

- Brian


Quoting Nadja Levitan <inftech at 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
--
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.