# Theory Proof_Terms

theory Proof_Terms
imports Main
```(*  Title:      HOL/Proofs/ex/Proof_Terms.thy
Author:     Makarius

Basic examples involving proof terms.
*)

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
```