author  wenzelm 
Mon, 04 Nov 2019 15:15:56 +0100  
changeset 71021  b697dd74221a 
parent 71020  4003da7e6a79 
child 71088  4b45d592ce29 
permissions  rwrr 
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
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
64986
diff
changeset

9 
imports "HOLIsar_Examples.Drinker" 
52424  10 
begin 
11 

61986  12 
subsection \<open>Export and reimport of global proof terms\<close> 
52424  13 

61986  14 
ML \<open> 
71021  15 
fun export_proof thy thm = thm 
16 
> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} 

17 
> Proofterm.encode (Sign.consts_of thy); 

52424  18 

19 
fun import_proof thy xml = 

20 
let 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset

21 
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

22 
val (prf', _) = Proofterm.freeze_thaw_prf prf; 
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

23 
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end; 
61986  24 
\<close> 
52424  25 

26 

61986  27 
subsection \<open>Examples\<close> 
52424  28 

69597  29 
ML \<open>val thy1 = \<^theory>\<close> 
52424  30 

31 
lemma ex: "A \<longrightarrow> A" .. 

32 

61986  33 
ML_val \<open> 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset

34 
val xml = export_proof thy1 @{thm ex}; 
52424  35 
val thm = import_proof thy1 xml; 
61986  36 
\<close> 
52424  37 

61986  38 
ML_val \<open> 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset

39 
val xml = export_proof thy1 @{thm de_Morgan}; 
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

40 
val thm = import_proof thy1 xml; 
61986  41 
\<close> 
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

42 

61986  43 
ML_val \<open> 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset

44 
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

45 
val thm = import_proof thy1 xml; 
61986  46 
\<close> 
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

47 

61986  48 
text \<open>Some fairly large proof:\<close> 
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

49 

61986  50 
ML_val \<open> 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70449
diff
changeset

51 
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

52 
val thm = import_proof thy1 xml; 
71020  53 

54 
val xml_size = size (YXML.string_of_body xml); 

55 
\<^assert> (xml_size > 400000); 

61986  56 
\<close> 
52630
fe411c1dc180
more robust proof export / import due to Stefan Berghofer;
wenzelm
parents:
52424
diff
changeset

57 

52424  58 
end 