Re: [isabelle] A simple lemma



On Fri, Sep 7, 2012 at 9:25 AM, John Munroe <munddr at gmail.com> wrote:
> Hi,
>
> Does anyone know why the following lemma is provable?
>
> lemma "F = G --> (EX a b. a ~= b --> F a = G a & F b ~= G b)"
> by auto
>
> If F and G are equal, then F x = G x for all x. So how come the above
> is provable?

Your lemma is provable even without the "F = G":

lemma "EX a b. a ~= b --> F a = G a & F b ~= G b"
by auto

The proof is by instantiating "a" and "b" with the same value. Then
you get "False --> something", which simplifies to True.

I think you may have meant to say this instead:

lemma "F = G --> (EX a b. a ~= b & F a = G a & F b ~= G b)"

which is indeed unprovable.

- Brian





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