Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Reading a proof

view this post on Zulip Email Gateway (Aug 18 2022 at 18:19):

From: Makarius <makarius@sketis.net>
For full proofs the basic HOL image needs to provide them already and
they need to be enabled for your own session.

For some years we used to have HOL with proof terms by default, but it
became to huge. You need to build your own image, e.g. like this:

Isabelle2011/build -m HOL-Proofs

This logic image then needs to be selected in PG when starting up.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 18:19):

From: John Munroe <munddr@gmail.com>

For full proofs the basic HOL image needs to provide them already and they
need to be enabled for your own session.

For some years we used to have HOL with proof terms by default, but it
became to huge.  You need to build your own image, e.g. like this:

Isabelle2011/build -m HOL-Proofs

This logic image then needs to be selected in PG when starting up.

Thanks. I can start it up with the HOL-Proofs image, but I can't seem
to import RealVector, Real, etc. It says that "Could not find file
"RealVector.thy". Can one use the reals with the HOL-Proofs image?

Thanks

John

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 18:29):

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

Suppose I have the following:

axiomatization
f :: "nat => nat"
where ax: "f 0 = 0"

lemma "f 0 = 0 | f 0 = 1"
using ax
apply auto
done

Clearly, auto finds a proof because the first disjunct can be
inferred. I'm trying to dig into the proof and see which disjunct is
actually proved by auto (or simp, when appropriate). I've tried
switching on 'Full Proof' from the Isabelle menu in PG and sticking
'full_prf' after 'apply auto', but I get an error saying
"reconstruct_proof: minimal proof object'. Is there a way to see which
disjunct is proved in either Isar or ML level? Could one see which
disjunct is proved by looking at the proof term? How to retrieve the
proof term?

Any help will be appreciated. Thanks.

John

view this post on Zulip Email Gateway (Aug 18 2022 at 18:35):

From: Makarius <makarius@sketis.net>
The HOL-Proofs target in the IsaMakefile merely uses the content of the
HOL-Main session, without type real and complex.

The include the latter you can rebuild the image by imitating the
IsaMakefile entry for it:

cd Isabelle2011/src/HOL
isabelle usedir -b -g true -p 2 -q 0 Pure HOL-Proofs

Makarius

Last updated: Apr 19 2024 at 20:15 UTC