src/HOL/Proofs/ex/XML_Data.thy
author wenzelm
Mon, 04 Nov 2019 15:15:56 +0100
changeset 71021 b697dd74221a
parent 71020 4003da7e6a79
child 71088 4b45d592ce29
permissions -rw-r--r--
tuned;

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

XML data representation of proof terms.
*)

theory XML_Data
  imports "HOL-Isar_Examples.Drinker"
begin

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

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

  fun import_proof thy xml =
    let
      val prf = Proofterm.decode (Sign.consts_of 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 \<longrightarrow> 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 abs_less_iff};
  val thm = import_proof thy1 xml;

  val xml_size = size (YXML.string_of_body xml);
  \<^assert> (xml_size > 400000);
\<close>

end