Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Silly problem with maps and

Email Gateway (Aug 18 2022 at 13:48):

From: John Ridgway <john@jacelridge.com>
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

Email Gateway (Aug 18 2022 at 13:48):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

Email Gateway (Aug 18 2022 at 13:49):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Email Gateway (Aug 18 2022 at 13:49):

From: John Ridgway <john@jacelridge.com>
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

Email Gateway (Aug 18 2022 at 13:49):

From: Tjark Weber <webertj@in.tum.de>
Well, to obtain a counterexample to an implication, one must not just
falsify the conclusion, but also satisfy the premises. In the original
this requires 'a to have (at least) 2 elements. In contrast, the range
type 'b of M may be a singleton. That's just what the message "Size of
types: 'b: 1 'a: 2" indicates.

Regards,
Tjark

Last updated: May 03 2024 at 12:27 UTC