Re: [isabelle] Silly problem with maps and

This is the counterexample that command "refute" gave me:

Size of types: 'b: 1, 'a: 2
l: a0
M: {(a0, Some b0), (a1, None)}


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.