equal
deleted
inserted
replaced
|
1 (* Title: HOL/Proofs/ex/XML_Data.thy |
|
2 Author: Makarius |
|
3 |
|
4 XML data representation of proof terms. |
|
5 *) |
|
6 |
|
7 theory XML_Data |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 subsection {* Export and re-import of global proof terms *} |
|
12 |
|
13 ML {* |
|
14 fun export_proof thm0 = |
|
15 let |
|
16 val thy = Thm.theory_of_thm thm0; |
|
17 val ctxt0 = Proof_Context.init_global thy; |
|
18 val thy = Proof_Context.theory_of ctxt0; |
|
19 val ((_, [thm]), ctxt) = Variable.import true [Thm.transfer thy thm0] ctxt0; |
|
20 |
|
21 val prop = Thm.prop_of thm; (* FIXME proper prop (wrt. import / strip) (!??) *) |
|
22 val prf = |
|
23 Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |
|
24 |> Proofterm.no_thm_proofs; |
|
25 in XML.Encode.pair Term_XML.Encode.term Proofterm.encode (prop, prf) end; |
|
26 |
|
27 fun import_proof thy xml = |
|
28 let |
|
29 val (prop, prf) = XML.Decode.pair Term_XML.Decode.term Proofterm.decode xml; |
|
30 val full_prf = Reconstruct.reconstruct_proof thy prop prf; |
|
31 in Drule.export_without_context (Proof_Checker.thm_of_proof thy full_prf) end; |
|
32 *} |
|
33 |
|
34 |
|
35 subsection {* Example *} |
|
36 |
|
37 ML {* val thy1 = @{theory} *} |
|
38 |
|
39 lemma ex: "A \<longrightarrow> A" .. |
|
40 |
|
41 ML {* |
|
42 val xml = export_proof @{thm ex}; |
|
43 val thm = import_proof thy1 xml; |
|
44 *} |
|
45 |
|
46 end |
|
47 |