isabelle: src/HOL/Proofs/ex/XML_Data.thy@799437173553 (annotated)

52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	1	(* Title: HOL/Proofs/ex/XML_Data.thy
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	2	Author: Makarius
52630 fe411c1dc180 more robust proof export / import due to Stefan Berghofer; wenzelm parents: 52424 diff changeset	3	Author: Stefan Berghofer
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	4
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	5	XML data representation of proof terms.
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	6	*)
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	7
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	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 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	10	begin
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	11
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	12	subsection \<open>Export and re-import of global proof terms\<close>
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	13
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	17
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	18	fun import_proof thy xml =
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	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 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	23	\<close>
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	24
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	25
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	26	subsection \<open>Examples\<close>
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	27
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 66453 diff changeset	28	ML \<open>val thy1 = \<^theory>\<close>
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	29
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	30	lemma ex: "A \<longrightarrow> A" ..
77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	31
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	34	val thm = import_proof thy1 xml;
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	35	\<close>
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	36
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	40	\<close>
52630 fe411c1dc180 more robust proof export / import due to Stefan Berghofer; wenzelm parents: 52424 diff changeset	41
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	45	\<close>
52630 fe411c1dc180 more robust proof export / import due to Stefan Berghofer; wenzelm parents: 52424 diff changeset	46
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	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 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 diff changeset	53	\<close>
52630 fe411c1dc180 more robust proof export / import due to Stefan Berghofer; wenzelm parents: 52424 diff changeset	54
52424 77075c576d4c support for XML data representation of proof terms; wenzelm parents: diff changeset	55	end

author	wenzelm
	Fri, 04 Oct 2019 15:30:52 +0200
changeset 70784	799437173553
parent 70449	6e34025981be
child 70839	2136e4670ad2
permissions	-rw-r--r--