author | wenzelm |
Fri, 04 Oct 2019 15:30:52 +0200 | |
changeset 70784 | 799437173553 |
parent 70449 | 6e34025981be |
child 70839 | 2136e4670ad2 |
permissions | -rw-r--r-- |
52424 | 1 |
(* Title: HOL/Proofs/ex/XML_Data.thy |
2 |
Author: Makarius |
|
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
3 |
Author: Stefan Berghofer |
52424 | 4 |
|
5 |
XML data representation of proof terms. |
|
6 |
*) |
|
7 |
||
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 | 10 |
begin |
11 |
||
61986 | 12 |
subsection \<open>Export and re-import of global proof terms\<close> |
52424 | 13 |
|
61986 | 14 |
ML \<open> |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
15 |
fun export_proof thy thm = |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
16 |
Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm); |
52424 | 17 |
|
18 |
fun import_proof thy xml = |
|
19 |
let |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
20 |
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
|
21 |
val (prf', _) = Proofterm.freeze_thaw_prf prf; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
22 |
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; |
61986 | 23 |
\<close> |
52424 | 24 |
|
25 |
||
61986 | 26 |
subsection \<open>Examples\<close> |
52424 | 27 |
|
69597 | 28 |
ML \<open>val thy1 = \<^theory>\<close> |
52424 | 29 |
|
30 |
lemma ex: "A \<longrightarrow> A" .. |
|
31 |
||
61986 | 32 |
ML_val \<open> |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
33 |
val xml = export_proof thy1 @{thm ex}; |
52424 | 34 |
val thm = import_proof thy1 xml; |
61986 | 35 |
\<close> |
52424 | 36 |
|
61986 | 37 |
ML_val \<open> |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
38 |
val xml = export_proof thy1 @{thm de_Morgan}; |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
39 |
val thm = import_proof thy1 xml; |
61986 | 40 |
\<close> |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
41 |
|
61986 | 42 |
ML_val \<open> |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
43 |
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
|
44 |
val thm = import_proof thy1 xml; |
61986 | 45 |
\<close> |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
46 |
|
61986 | 47 |
text \<open>Some fairly large proof:\<close> |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
48 |
|
61986 | 49 |
ML_val \<open> |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
50 |
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
|
51 |
val thm = import_proof thy1 xml; |
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset
|
52 |
\<^assert> (size (YXML.string_of_body xml) > 500000); |
61986 | 53 |
\<close> |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
54 |
|
52424 | 55 |
end |