Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Obtaining the instantiation of variables in a ...


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 12:29 UTC