How to see step-by-step reasoning of Isabelle 'proofs'

Question

I started to learn Isabelle recently and I cound not find an answer to a very important question: how can one see step-by-step reasoning of 'proofs' found by Isabelle? I am not satisfied with lines like "by auto" or "using Theorem_A by blast", I want to check step-by-step deduction. Of course, I learned about Isar 'proofs' but 1. such Isar proofs cannot always be found by Sledgehammer and 2. even Isar proofs do not always give step-by-step reasoning. For example, an Isar proof of one of my theorems generated by Sledgehammer looks like this:

     proof -
  have "... here is my formula ...."
    using My_Theorem_1 My_axiom_2 by blast
  thus ?thesis
    by metis
qed

Of course, one cannot call such a proof 'a human readable proof' as Isabelle and Isar's enthusiasts do. Now my question: is it possible to generate step-by-step deduction from 'proofs' found by Isabelle? Or at least is it possible to transform 'proofs' like "by auto" into Isar proofs? A situation where step-by-step deduction is needed is e.g. proofs of existence theorems, they often provide useful explicit constructions. I look through several tutorials but I could not find an answer...

Answer 1

First of all, I will explain why your problem is typically not considered as important as you think it is; then I will answer your actual question.

Isabelle is designed so that you do not have to ‘trust’ its proof methods (like simp, auto, metis) at all. All proofs have to go through Isabelle's inference kernel, since the kernel is the only part in Isabelle that can produce theorems: if you trust the (relatively small) kernel, you can trust all proof methods. Proof methods just directly or indirectly call functions the kernel exports to manipulate theorems.

The kernel contains functions that mirror the axioms of Isabelle/Pure, which is, I think, just natural deduction. Then you have axioms of the object logic (HOL in most cases) and definitions and typedefs. All Isabelle theorems have proofs that are basically proof trees consisting of these reasoning steps.

The ‘step-by-step’ proof you are looking for is therefore this tree, and it is called a proof object or proof term. The problem with these things is that they are very large and very unreadable (cf. the Principia Mathematica by Russell and Whitehead to get an idea of just how large and unreadable). I think you can tell Isabelle to generate these proof terms somehow, but I have no idea how. I did find a set of slides by Stefan Berghofer though.

I do not understand why you would say the example you gave is not human-readable. There is some detail that is hidden from the reader, yes, but the same is true of pretty much every ordinary mathematical proof as well. blast and metis do not work magic; blast is a first-order tableau prover, metis is a resolution prover. If blast and metis can prove something in a single step, a mathematician would probably not go into more detail on that step either.

As for explicit constructions with existentials: Isabelle/HOL is not a constructive logic. Program extraction from classical proofs is ongoing research and very difficult. If you want an explicit construction of something in Isabelle/HOL, my advice would be not to prove the existential, but to prove your explicit construction directly. If your existential can be proven in a single step by auto, I would wager that the construction is very simple.

Answer 2

You can view the internal proof terms for facts using:

prf lemma_name

For example, the following lemma from Pure

thm Pure.conjunction_imp
> (PROP ?A &&& PROP ?B ⟹ PROP ?C) ≡ (PROP ?A ⟹ PROP ?B ⟹ PROP ?C)

has the as its proof term output:

prf Pure.conjunction_imp
> equal_intr ⋅ _ ⋅ _ ● (❙λ(H: _) (Ha: _) Hb: _. H ● (conjunctionI ⋅ _ ⋅ _ ● Ha ● Hb)) ●
  (❙λ(H: _) Ha: _. H ● (conjunctionD1 ⋅ _ ⋅ _ ● Ha) ● (conjunctionD2 ⋅ _ ⋅ _ ● Ha))

With full_prf, the output becomes even more verbose.

The slides referenced in Manuel Eberl's answer give some more info concerning the meaning of the symbols. Even if one does not understand the proof lambda terms, the prf-terms quite clearly expose the facts used to proof the lemma.

In the default HOL session, the output will look quite boring because the internal proof parts are not compiled into the session image (cf. Makarius's post there). For the desired output, you'll have to switch to the HOL-Proofs session. (In jEdit: Select HOL-Proofs from the theories panel and restart jEdit. Building of the special session image should start automatically. (...Well, in theory it should work like this... I just tried to build the HOL-Proofs session in Isabelle2015, but it took indefinitely long on my computer...))