*To*: Nadja Levitan <inftech at gmx.de>*Subject*: Re: [isabelle] And mask*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Mon, 02 Mar 2009 08:28:44 -0800*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20090301205553.93780@gmx.net>*References*: <20090301205553.93780@gmx.net>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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, thenafter 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

**References**:**[isabelle] And mask***From:*Nadja Levitan

- Previous by Date: Re: [isabelle] Problem with overloading and inductive
- Next by Date: Re: [isabelle] Problem with overloading and inductive
- Previous by Thread: [isabelle] And mask
- Next by Thread: Re: [isabelle] Problem with overloading and inductive
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list