Re: [isabelle] Silly problem with maps and

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


> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.