Re: [isabelle] Proofability of a simple existential statement

You can see how auto instantiated the existentials using the full_prf
command. (Make sure you enable Isabelle > Settings > Full Proofs in
ProofGeneral, or it won't work.)

lemma "EX func arg. func arg = 0"
apply auto

The proof object shows that the goal was solved by two applications of
rule exI, followed by rule refl. The arguments to rule exI include the
predicate and the witness. In this case, you can see that "func" was
instantiated as the constant function "%a. 0".

- Brian

On Thu, Jun 3, 2010 at 4:06 AM, Lawrence Paulson <lp15 at> wrote:
> Isabelle uses higher-order unification to solve such problems. I expect that Isabelle instantiates func with the identity function and arg with 0. You might want to try more complicated examples to see the extent of what can be done automatically.
> Larry Paulson
> On 3 Jun 2010, at 01:35, Steve W wrote:
>> I have a quick, basic question: How come the following is provable, without
>> the need of any fact:
>> lemma exzero: "EX func arg. func arg = 0"
>> by auto
>> How are func and arg instantiated?
>> Thank you for any help in advance.
>> Steve

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