Email Gateway (Aug 18 2022 at 13:22): Email Gateway (Aug 18 2022 at 13:22):From: Stephy Wong <s.wong.731@googlemail.com>
Hi all,
Given the trivial proof for EX x. x >' 0' by using the axiom 1' >' 0', is
there a way to see by which term x is instantiated (by 1' in this case)? Can
this be done in PG? If not, how can this be done in ML?
Thanks
Steph
Email Gateway (Aug 18 2022 at 13:22):From: Tobias Nipkow <nipkow@in.tum.de>
Stephy Wong wrote:
If your goal is an EX, you can provide the witness by instantiating the
exI thm before use:
apply(rule_tac x = "1'" in exI)
Pls read Section 5.9, Quantifiers, of the Tutorial.
Tobias
Email Gateway (Aug 18 2022 at 13:23):From: Stephy Wong <s.wong.731@googlemail.com>
On Wed, Apr 15, 2009 at 10:53 AM, Tobias Nipkow <nipkow@in.tum.de> wrote:
Stephy Wong wrote:
Hi all,
Given the trivial proof for EX x. x >' 0' by using the axiom 1' >' 0', is
there a way to see by which term x is instantiated (by 1' in this case)?
Can
this be done in PG? If not, how can this be done in ML?Thanks
Steph
If your goal is an EX, you can provide the witness by instantiating the
exI thm before use:apply(rule_tac x = "1'" in exI)
Pls read Section 5.9, Quantifiers, of the Tutorial.
Thanks. What I actually meant is that is it possible to obtain the
instantiation(s) that Isabelle has found automatically? The example I gave
is a trivial one that Isabelle can proof automatically, but I'm interested
in seeing how Isabelle instantiates the theorem. Does this need to be done
in ML? Sorry for the confusion.
Thanks
Steph
Tobias
Email Gateway (Aug 18 2022 at 13:23):From: Makarius <makarius@sketis.net>
You need some tiny bit of ML, namely:
ML "proofs := 2";
Now you can inspect what happens internally, although the details of
automated tools are often hard to follow. For example:
lemma a: "EX x::nat. x > 0" by auto
full_prf a
ccontr % EX x. 0 < x %%
(Lam H: ~ (EX x. 0 < x).
HOL.swap % EX x. 0 < x % False %% H %%
(Lam H: ~ False.
exI % TYPE(nat) % op < 0 % Suc ?a2 %% (zero_less_Suc % ?a2)))
This is nat too bad: it says in the last line that exI was used with the
term "Suc ?a2", for an arbitrary ?a2. If you try this with "by arith"
instead, you get less satisfactory output, though.
Makarius
Email Gateway (Aug 18 2022 at 13:59):From: John Munroe <munddr@googlemail.com>
Hi Makarius,
I'm trying out some instructions you gave earlier, but I keep getting
an error saying:
"*** reconstruct_proof: minimal proof object
*** At command "full_prf"."
prf a works for me though and gives:
ccontr % _ %% (Lam H: _. ? %% H %% (Lam H: _. zero_less_Suc % _))
Thanks
John
Makarius wrote:
Last updated: Nov 21 2024 at 12:39 UTC