Re: [isabelle] Silly problem with maps and



That is correct, except that I mistranscribed the proposition and corrected it in my second post. 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.