Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Aligning full_prf with proof term

Email Gateway (Aug 18 2022 at 18:29):

From: Makarius <makarius@sketis.net>
The expert on these things is Stefan Berghofer.

Makarius

Email Gateway (Aug 18 2022 at 18:29):

From: Stefan Berghofer <berghofe@in.tum.de>
Quoting John Munroe <munddr@gmail.com>:

I'm trying to find a clause that is displayed by 'full_prf' in a proof
term. For instance:

[...]

Now if I do:

ML {*
val thm = @{thm "lem1"};
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([],[]) prf;
val prf'' = Reconstruct.reconstruct_proof @{theory} prop prf'
*}

I get a massive proof term. If I want to find the line "(transitive %
TYPE(bool) % f 0 = 1 | f 0 = 0 % False | True % True %%", how do I
extract it from the proof term? I'm just trying to see which disjunct
is proved, so I thought if I could extract "False | True" then I can
infer that the second disjunct is proved.

Hi John,

since your theorem has already been stored in the theorem database,
the proof returned by Thm.proof_of has simply the form

PThm (..., (("Theory_Name.lem1", ..., ...), body))

so you have to use Proofterm.strip_thm to obtain the actual proof. You can
then search for the desired subproof by recursion on the structure of the
proof term datatype (see attached theory).

Greetings,
Stefan

Any assistance or opinions will be much appreciated. Thanks.

John

Munroe.thy

Email Gateway (Aug 18 2022 at 18:31):

From: John Munroe <munddr@gmail.com>
Hi,

I'm trying to find a clause that is displayed by 'full_prf' in a proof
term. For instance:

axiomatization
f :: "nat => nat"
where ax: "f 0 = 0"
and ax': "f 0 = 1"

lemma lem1: "f 0 = 1 | f 0 = 0"
using ax
by auto

full_prf lem1

gives the following proof:

equal_elim % True % f 0 = 1 | f 0 = 0 %%
(symmetric % TYPE(prop) % f 0 = 1 | f 0 = 0 % True %%
(combination % TYPE(bool) % TYPE(prop) % Trueprop % Trueprop %
f 0 = 1 | f 0 = 0 %
True %%
(reflexive % TYPE(bool => prop) % Trueprop) %%
(transitive % TYPE(bool) % f 0 = 1 | f 0 = 0 % False | True % True %% ...

Now if I do:

ML {*
val thm = @{thm "lem1"};
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
val prf' = Proofterm.rewrite_proof_notypes ([],[]) prf;
val prf'' = Reconstruct.reconstruct_proof @{theory} prop prf'
*}

I get a massive proof term. If I want to find the line "(transitive %
TYPE(bool) % f 0 = 1 | f 0 = 0 % False | True % True %%", how do I
extract it from the proof term? I'm just trying to see which disjunct
is proved, so I thought if I could extract "False | True" then I can
infer that the second disjunct is proved.

Any assistance or opinions will be much appreciated. Thanks.

John

Email Gateway (Aug 18 2022 at 18:37):

From: John Munroe <munddr@gmail.com>
Anyone got any idea?

Thanks
John

Email Gateway (Aug 18 2022 at 18:37):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi John,

From the little I understand about proof terms, they inline all referenced lemmas, which would explain why they can be so huge when you print them at the ML level. The trick would be to write your own traversal function on proof terms that does not enter the lemmas. Hopefully somebody who knows them better can comment further on this.

Regards,

Jasmin

Last updated: Apr 19 2024 at 12:27 UTC