theory Proof_Terms
imports Main
begin
text ‹
Detailed proof information of a theorem may be retrieved as follows:
›
lemma ex: "A ∧ B ⟶ B ∧ A"
proof
assume "A ∧ B"
then obtain B and A ..
then show "B ∧ A" ..
qed
ML_val ‹
val thm = @{thm ex};
(*proof body with digest*)
val body = Proofterm.strip_thm (Thm.proof_body_of thm);
(*proof term only*)
val prf = Proofterm.proof_of body;
(*clean output*)
Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} false thm);
Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} true thm);
(*all theorems used in the graph of nested proofs*)
val all_thms =
Proofterm.fold_body_thms
(fn {name, ...} => insert (op =) name) [body] [];
›
text ‹
The result refers to various basic facts of Isabelle/HOL: @{thm [source]
HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The
combinator @{ML Proofterm.fold_body_thms} recursively explores the graph of
the proofs of all theorems being used here.
┉
Alternatively, we may produce a proof term manually, and turn it into a
theorem as follows:
›
ML_val ‹
val thy = @{theory};
val ctxt = @{context};
val prf =
Proof_Syntax.read_proof thy true false
"impI ⋅ _ ⋅ _ ∙ \
\ (❙λH: _. \
\ conjE ⋅ _ ⋅ _ ⋅ _ ∙ H ∙ \
\ (❙λ(H: _) Ha: _. conjI ⋅ _ ⋅ _ ∙ Ha ∙ H))";
val thm =
prf
|> Reconstruct.reconstruct_proof ctxt @{prop "A ∧ B ⟶ B ∧ A"}
|> Proof_Checker.thm_of_proof thy
|> Drule.export_without_context;
›
end