Re: [isabelle] Reading a proof

On Fri, 30 Sep 2011, John Munroe wrote:

Suppose I have the following:

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

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

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?

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.