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
full_prf

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 cam.ac.uk> 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.