Re: [isabelle] A simple lemma
On Fri, Sep 7, 2012 at 9:25 AM, John Munroe <munddr at gmail.com> wrote:
> 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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and