Quellcode-Bibliothek 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 ‹Export and re-import of global proof terms›

ML ‹
  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;
›


subsection ‹Examples›

ML ‹val thy1 = 🍋›

lemma ex: "A \ A" ..

ML_val ‹
  val xml = export_proof thy1 @{thm ex};
  val thm = import_proof thy1 xml;
›

ML_val ‹
  val xml = export_proof thy1 @{thm de_Morgan};
  val thm = import_proof thy1 xml;
›

ML_val ‹
  val xml = export_proof thy1 @{thm Drinker's_Principle};
  val thm = import_proof thy1 xml;
›

text ‹Some fairly large proof:›

ML_val ‹
  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);
  🍋 (xml_size > 10000000);
›

end