Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Proofs/ex/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle Proof_Terms.thy Sprache: Isabelle

(*  Title:      HOL/Proofs/ex/Proof_Terms.thy
    Author:     Makarius

Basic examples involving proof terms.
*)

theory Proof_Terms
imports Main
begin

text \<open>
  Detailed proof information of a theorem may be retrieved as follows:
\<close>

lemma ex: "A \ B \ B \ A"
proof
  assume "A \ B"
  then obtain B and A ..
  then show "B \ A" ..
qed

ML_val \<open>
  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 \<^context> false thm);
  Pretty.writeln (Proof_Syntax.pretty_standard_proof_of \<^context> 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] [];
\<close>

text \<open>
  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>\<open>Proofterm.fold_body_thms\<close> recursively explores the graph of
  the proofs of all theorems being used here.

  \<^medskip>
  Alternatively, we may produce a proof term manually, and turn it into a
  theorem as follows:
\<close>

ML_val \<open>
  val thy = \<^theory>;
  val prf =
    Proof_Syntax.read_proof thy true false
      "impI \ _ \ _ \ \
      \   (\<^bold>\<lambda>H: _. \
      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
      \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
  val thm =
    Proofterm.reconstruct_proof thy \<^prop>\<open>A \<and> B \<longrightarrow> B \<and> A\<close> prf
    |> Proof_Checker.thm_of_proof thy
    |> Drule.export_without_context;
\<close>

end

quality95%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.