author | wenzelm |
Tue, 02 Jun 2015 10:12:29 +0200 | |
changeset 60360 | f585b1f0b4c3 |
parent 60157 | ccf9241af217 |
child 61039 | 80f40d89dab6 |
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 |
|
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
9 |
imports "~~/src/HOL/Isar_Examples/Drinker" |
52424 | 10 |
begin |
11 |
||
12 |
subsection {* Export and re-import of global proof terms *} |
|
13 |
||
14 |
ML {* |
|
60360 | 15 |
fun export_proof thy thm = |
52424 | 16 |
let |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
17 |
val {prop, hyps, shyps, ...} = Thm.rep_thm thm; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
18 |
val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)); |
52424 | 19 |
val prf = |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
20 |
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
|
21 |
Reconstruct.reconstruct_proof thy prop |> |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
22 |
Reconstruct.expand_proof thy [("", NONE)] |> |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
23 |
Proofterm.rew_proof thy |> |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
24 |
Proofterm.no_thm_proofs; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
25 |
in Proofterm.encode prf end; |
52424 | 26 |
|
27 |
fun import_proof thy xml = |
|
28 |
let |
|
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
29 |
val prf = Proofterm.decode xml; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
30 |
val (prf', _) = Proofterm.freeze_thaw_prf prf; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
31 |
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; |
52424 | 32 |
*} |
33 |
||
34 |
||
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
35 |
subsection {* Examples *} |
52424 | 36 |
|
37 |
ML {* val thy1 = @{theory} *} |
|
38 |
||
39 |
lemma ex: "A \<longrightarrow> A" .. |
|
40 |
||
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
41 |
ML_val {* |
60360 | 42 |
val xml = export_proof @{theory} @{thm ex}; |
52424 | 43 |
val thm = import_proof thy1 xml; |
44 |
*} |
|
45 |
||
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
46 |
ML_val {* |
60360 | 47 |
val xml = export_proof @{theory} @{thm de_Morgan}; |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
48 |
val thm = import_proof thy1 xml; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
49 |
*} |
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 |
ML_val {* |
60360 | 52 |
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
|
53 |
val thm = import_proof thy1 xml; |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
54 |
*} |
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 |
text {* Some fairly large proof: *} |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
57 |
|
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
58 |
ML_val {* |
60360 | 59 |
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
|
60 |
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
|
61 |
@{assert} (size (YXML.string_of_body xml) > 1000000); |
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
62 |
*} |
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset
|
63 |
|
52424 | 64 |
end |