equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Export and re-import of global proof terms\<close> |
12 subsection \<open>Export and re-import of global proof terms\<close> |
13 |
13 |
14 ML \<open> |
14 ML \<open> |
15 fun export_proof thy thm = |
15 fun export_proof ctxt thm = |
16 let |
16 let |
|
17 val thy = Proof_Context.theory_of ctxt; |
17 val (_, prop) = |
18 val (_, prop) = |
18 Logic.unconstrainT (Thm.shyps_of thm) |
19 Logic.unconstrainT (Thm.shyps_of thm) |
19 (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); |
20 (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); |
20 val prf = |
21 val prf = |
21 Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> |
22 Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> |
22 Reconstruct.reconstruct_proof thy prop |> |
23 Reconstruct.reconstruct_proof ctxt prop |> |
23 Reconstruct.expand_proof thy [("", NONE)] |> |
24 Reconstruct.expand_proof ctxt [("", NONE)] |> |
24 Proofterm.rew_proof thy |> |
25 Proofterm.rew_proof thy |> |
25 Proofterm.no_thm_proofs; |
26 Proofterm.no_thm_proofs; |
26 in Proofterm.encode prf end; |
27 in Proofterm.encode prf end; |
27 |
28 |
28 fun import_proof thy xml = |
29 fun import_proof thy xml = |
38 ML \<open>val thy1 = @{theory}\<close> |
39 ML \<open>val thy1 = @{theory}\<close> |
39 |
40 |
40 lemma ex: "A \<longrightarrow> A" .. |
41 lemma ex: "A \<longrightarrow> A" .. |
41 |
42 |
42 ML_val \<open> |
43 ML_val \<open> |
43 val xml = export_proof @{theory} @{thm ex}; |
44 val xml = export_proof @{context} @{thm ex}; |
44 val thm = import_proof thy1 xml; |
45 val thm = import_proof thy1 xml; |
45 \<close> |
46 \<close> |
46 |
47 |
47 ML_val \<open> |
48 ML_val \<open> |
48 val xml = export_proof @{theory} @{thm de_Morgan}; |
49 val xml = export_proof @{context} @{thm de_Morgan}; |
49 val thm = import_proof thy1 xml; |
50 val thm = import_proof thy1 xml; |
50 \<close> |
51 \<close> |
51 |
52 |
52 ML_val \<open> |
53 ML_val \<open> |
53 val xml = export_proof @{theory} @{thm Drinker's_Principle}; |
54 val xml = export_proof @{context} @{thm Drinker's_Principle}; |
54 val thm = import_proof thy1 xml; |
55 val thm = import_proof thy1 xml; |
55 \<close> |
56 \<close> |
56 |
57 |
57 text \<open>Some fairly large proof:\<close> |
58 text \<open>Some fairly large proof:\<close> |
58 |
59 |
59 ML_val \<open> |
60 ML_val \<open> |
60 val xml = export_proof @{theory} @{thm abs_less_iff}; |
61 val xml = export_proof @{context} @{thm abs_less_iff}; |
61 val thm = import_proof thy1 xml; |
62 val thm = import_proof thy1 xml; |
62 @{assert} (size (YXML.string_of_body xml) > 1000000); |
63 @{assert} (size (YXML.string_of_body xml) > 1000000); |
63 \<close> |
64 \<close> |
64 |
65 |
65 end |
66 end |