Email Gateway (Aug 18 2022 at 15:23): Email Gateway (Aug 18 2022 at 15:23):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 15:25):From: Brian Huffman <brianh@cs.pdx.edu>
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".
Email Gateway (Aug 18 2022 at 15:34):From: Steve W <s.wong.731@gmail.com>
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
Last updated: Apr 23 2024 at 04:18 UTC