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"
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".
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and