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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Proofs/ex/XML_Data.thy
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
     3
    Author:     Stefan Berghofer
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     4
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     5
XML data representation of proof terms.
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     6
*)
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     7
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
     8
theory XML_Data
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 64986
diff changeset
     9
  imports "HOL-Isar_Examples.Drinker"
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    10
begin
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    11
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    12
subsection \<open>Export and re-import of global proof terms\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    13
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    14
ML \<open>
71021
wenzelm
parents: 71020
diff changeset
    15
  fun export_proof thy thm = thm
wenzelm
parents: 71020
diff changeset
    16
    |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
wenzelm
parents: 71020
diff changeset
    17
    |> Proofterm.encode (Sign.consts_of thy);
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    18
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    19
  fun import_proof thy xml =
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    20
    let
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70449
diff changeset
    21
      val prf = Proofterm.decode (Sign.consts_of thy) xml;
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    22
      val (prf', _) = Proofterm.freeze_thaw_prf prf;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    23
    in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    24
\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    25
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    26
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    27
subsection \<open>Examples\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    28
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    29
ML \<open>val thy1 = \<^theory>\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    30
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    31
lemma ex: "A \<longrightarrow> A" ..
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    32
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    33
ML_val \<open>
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70449
diff changeset
    34
  val xml = export_proof thy1 @{thm ex};
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    35
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    36
\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    37
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    38
ML_val \<open>
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70449
diff changeset
    39
  val xml = export_proof thy1 @{thm de_Morgan};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    40
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    41
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    42
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    43
ML_val \<open>
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70449
diff changeset
    44
  val xml = export_proof thy1 @{thm Drinker's_Principle};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    45
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    46
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    47
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    48
text \<open>Some fairly large proof:\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    49
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    50
ML_val \<open>
70784
799437173553 Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents: 70449
diff changeset
    51
  val xml = export_proof thy1 @{thm abs_less_iff};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    52
  val thm = import_proof thy1 xml;
71020
4003da7e6a79 updated xml_size;
wenzelm
parents: 70915
diff changeset
    53
4003da7e6a79 updated xml_size;
wenzelm
parents: 70915
diff changeset
    54
  val xml_size = size (YXML.string_of_body xml);
4003da7e6a79 updated xml_size;
wenzelm
parents: 70915
diff changeset
    55
  \<^assert> (xml_size > 400000);
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    56
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    57
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    58
end