src/HOL/Proofs/ex/XML_Data.thy
author wenzelm
Fri, 12 Jul 2013 21:13:57 +0200
changeset 52630 fe411c1dc180
parent 52424 77075c576d4c
child 58372 bfd497f2f4c2
permissions -rw-r--r--
more robust proof export / import due to Stefan Berghofer; eliminated musing in the manual that is not quite right;
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
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    12
subsection {* Export and re-import of global proof terms *}
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    13
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    14
ML {*
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    15
  fun export_proof thm =
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    16
    let
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    17
      val thy = Thm.theory_of_thm thm;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    18
      val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    19
      val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
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;
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    33
*}
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
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    36
subsection {* Examples *}
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    37
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    38
ML {* val thy1 = @{theory} *}
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
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    42
ML_val {*
52424
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    43
  val xml = export_proof @{thm ex};
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    44
  val thm = import_proof thy1 xml;
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    45
*}
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    46
52630
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    47
ML_val {*
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    48
  val xml = export_proof @{thm de_Morgan};
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    49
  val thm = import_proof thy1 xml;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    50
*}
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    51
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    52
ML_val {*
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    53
  val xml = export_proof @{thm Drinker's_Principle};
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    54
  val thm = import_proof thy1 xml;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    55
*}
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    56
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    57
text {* Some fairly large proof: *}
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    58
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    59
ML_val {*
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    60
  val xml = export_proof @{thm Int.times_int.abs_eq};
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    61
  val thm = import_proof thy1 xml;
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    62
  @{assert} (size (YXML.string_of_body xml) > 50000000);
fe411c1dc180 more robust proof export / import due to Stefan Berghofer;
wenzelm
parents: 52424
diff changeset
    63
*}
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
77075c576d4c support for XML data representation of proof terms;
wenzelm
parents:
diff changeset
    66