*To*: John Ridgway <john at jacelridge.com>*Subject*: Re: [isabelle] Silly problem with maps and*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 15 Jul 2009 22:25:08 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <5847CEEF-B8F5-4783-BD3E-C08D78CA2F56@jacelridge.com>*References*: <41424E38-C3E7-41DB-B567-40B64CDE6CB0@jacelridge.com> <4A5D845F.4070806@in.tum.de> <5847CEEF-B8F5-4783-BD3E-C08D78CA2F56@jacelridge.com>*User-agent*: Thunderbird 2.0.0.22 (Macintosh/20090605)

John Ridgway schrieb: > That is correct, except that I mistranscribed the proposition and > corrected it in my second post. I only received your first post, which is not your fault. I frequently do not get some of the emails on isabelle-users (and no, it is not my spam filter). I tried sledgehammer on your example, and it did indeed find a proof, apply (metis COMBB_def Collect_def Collect_mem_eq Collect_neg_eq ComplD ComplI exE_some mem_def) but unfortunately that proof leads to *** metis error (inst_inf): Ill-typed instantiation So here is a traditional hand-crafted proof: apply (erule someI2_ex) apply blast Tobias > The final \<in> should have been > \<notin> which does not lead to a quick refutal. In the original you > don't even need to play with sizes; all you need to do is assume that > SOME l is l. > > 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 for me >>> (or explains why it's false), but, oh well. :-) >>> >>> Peace >>> - John >>> >>>

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

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

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

- Previous by Date: Re: [isabelle] x-symbols and AFS?
- Next by Date: [isabelle] FLoC 2010: Final Call for Workshop Proposals
- 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