src/HOL/Proofs/ex/XML_Data.thy
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61986 2461779da2b8
child 62922 96691631c1eb
permissions -rw-r--r--
proper syntax;
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
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
     9
imports "~~/src/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>
60360
f585b1f0b4c3 clarified context;
wenzelm
parents: 60157
diff changeset
    15
  fun export_proof thy thm =
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    16
    let
61039
80f40d89dab6 tuned signature;
wenzelm
parents: 60360
diff changeset
    17
      val (_, prop) =
80f40d89dab6 tuned signature;
wenzelm
parents: 60360
diff changeset
    18
        Logic.unconstrainT (Thm.shyps_of thm)
80f40d89dab6 tuned signature;
wenzelm
parents: 60360
diff changeset
    19
          (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    20
      val prf =
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    21
        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    22
        Reconstruct.reconstruct_proof thy prop |>
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    23
        Reconstruct.expand_proof thy [("", NONE)] |>
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    24
        Proofterm.rew_proof thy |>
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    25
        Proofterm.no_thm_proofs;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    26
    in Proofterm.encode prf end;
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    27
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    28
  fun import_proof thy xml =
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    29
    let
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    30
      val prf = Proofterm.decode xml;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    31
      val (prf', _) = Proofterm.freeze_thaw_prf prf;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    32
    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
    33
\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    34
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    35
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    36
subsection \<open>Examples\<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 \<open>val thy1 = @{theory}\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    39
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    40
lemma ex: "A \<longrightarrow> A" ..
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    41
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    42
ML_val \<open>
60360
f585b1f0b4c3 clarified context;
wenzelm
parents: 60157
diff changeset
    43
  val xml = export_proof @{theory} @{thm ex};
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    44
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    45
\<close>
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    46
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    47
ML_val \<open>
60360
f585b1f0b4c3 clarified context;
wenzelm
parents: 60157
diff changeset
    48
  val xml = export_proof @{theory} @{thm de_Morgan};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    49
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    50
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    51
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    52
ML_val \<open>
60360
f585b1f0b4c3 clarified context;
wenzelm
parents: 60157
diff changeset
    53
  val xml = export_proof @{theory} @{thm Drinker's_Principle};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    54
  val thm = import_proof thy1 xml;
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    55
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    56
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    57
text \<open>Some fairly large proof:\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    58
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    59
ML_val \<open>
60360
f585b1f0b4c3 clarified context;
wenzelm
parents: 60157
diff changeset
    60
  val xml = export_proof @{theory} @{thm abs_less_iff};
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    61
  val thm = import_proof thy1 xml;
60157
ccf9241af217 use smaller example that fits into 64MB string limit of Poly/ML x86 platform;
wenzelm
parents: 58372
diff changeset
    62
  @{assert} (size (YXML.string_of_body xml) > 1000000);
61986
2461779da2b8 isabelle update_cartouches -c -t;
wenzelm
parents: 61039
diff changeset
    63
\<close>
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    64
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    65
end