Quelle  Proof_Terms.thy

(*  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_body (Thm.proof_body_of thm);

  (*proof term only*)
  val prf = Proofterm.proof_of body;

  (*clean output*)
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of 🍋 false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of 🍋 true thm);

  (*all theorems used in the graph of nested proofs*)
  val all_thms =
    Proofterm.fold_body_thms
      (fn {thm_name, ...} => insert (op =) thm_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 🪙‹Proofterm.fold_body_thms› r
  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 = 🍋;
  val prf =
  Proof_Syntax.read_proof thy true false
java.lang.NullPointerException
java.lang.NullPointerException
java.lang.NullPointerException
  \       (🪙λ(H: _) Ha: _. conjI ⋅ _ ⋅ _ ∙ Ha ∙ H))";
  val thm =
  Proofterm.reconstruct_proof thy 🍋‹A ∧ B ⟶ B ∧ A› p
    |> Proof_Checker.thm_of_proof thy
    |> Drule.export_without_context;
›

end