*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Silly problem with maps and*From*: John Ridgway <john at jacelridge.com>*Date*: Wed, 15 Jul 2009 10:46:00 -0400*Cc*: John Ridgway <john at jacelridge.com>, isabelle-users at cl.cam.ac.uk*In-reply-to*: <4A5D845F.4070806@in.tum.de>*References*: <41424E38-C3E7-41DB-B567-40B64CDE6CB0@jacelridge.com> <4A5D845F.4070806@in.tum.de>

Peace - John On Jul 15, 2009, at 3:25 AM, Tobias Nipkow wrote:

This is the counterexample that command "refute" gave me: Size of types: 'b: 1, 'a: 2 l: a0 M: {(a0, Some b0), (a1, None)} Tobias John Ridgway schrieb:How do I prove the following? M is a map, l is just a type, which is why I explicitly included the premise that there was an l not in the domain. !! l . [| \<exists> l . l \<notin> dom M; l \<in> dom M |] ==> l \<noteq> (SOME l. l \<in> dom M)I expect that I'm going to feel silly when somebody solves this forme(or explains why it's false), but, oh well. :-) Peace - John

**Follow-Ups**:**Re: [isabelle] Silly problem with maps and***From:*Tobias Nipkow

**Re: [isabelle] Silly problem with maps and***From:*Tjark Weber

**References**:**[isabelle] Silly problem with maps and***From:*John Ridgway

**Re: [isabelle] Silly problem with maps and***From:*Tobias Nipkow

- Previous by Date: [isabelle] x-symbols and AFS?
- Next by Date: [isabelle] now online: HOL-Boogie --- An Interactive Prover-Backend for the Verified C Compiler
- Previous by Thread: Re: [isabelle] Silly problem with maps and
- Next by Thread: Re: [isabelle] Silly problem with maps and
- Cl-isabelle-users July 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