Quelle XML_Data.thy Sprache: Isabelle

(*  Title:      HOL/Proofs/ex/XML_Data.thy
    Author:     Makarius
    Author:     Stefan Berghofer

XML data representation of proof terms.
*)

theory XML_Data
  imports "HOL-Examples.Drinker"
begin

subsection \<open>Export and re-import of global proof terms\<close>

ML \<open>
  fun export_proof thy thm = thm
    |> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
    |> Proofterm.encode thy;

  fun import_proof thy xml =
    let
      val prf = Proofterm.decode thy xml;
      val (prf', _) = Proofterm.freeze_thaw_prf prf;
    in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
\<close>

subsection \<open>Examples\<close>

ML \<open>val thy1 = \<^theory>\<close>

lemma ex: "A \ A" ..

ML_val \<open>
  val xml = export_proof thy1 @{thm ex};
  val thm = import_proof thy1 xml;
\<close>

ML_val \<open>
  val xml = export_proof thy1 @{thm de_Morgan};
  val thm = import_proof thy1 xml;
\<close>

ML_val \<open>
  val xml = export_proof thy1 @{thm Drinker's_Principle};
  val thm = import_proof thy1 xml;
\<close>

text \<open>Some fairly large proof:\<close>

ML_val \<open>
  val xml = export_proof thy1 @{thm Int.times_int.abs_eq};
  val thm = import_proof thy1 xml;

  val xml_size = Bytes.size (YXML.bytes_of_body xml);
  \<^assert> (xml_size > 10000000);
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.