isabelle: src/HOL/Proofs/ex/XML_Data.thy@caedabd2771c (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>
62922 96691631c1eb clarified context; wenzelm parents: 61986 diff changeset	15	fun export_proof ctxt thm =
64986 b81a048960a3 more uniform use of Reconstruct.clean_proof_of; wenzelm parents: 62922 diff changeset	16	Proofterm.encode (Reconstruct.clean_proof_of ctxt 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
52630 fe411c1dc180 more robust proof export / import due to Stefan Berghofer; wenzelm parents: 52424 diff changeset	20	val prf = Proofterm.decode xml;
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
61986 2461779da2b8 isabelle update_cartouches -c -t; wenzelm parents: 61039 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>
62922 96691631c1eb clarified context; wenzelm parents: 61986 diff changeset	33	val xml = export_proof @{context} @{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>
62922 96691631c1eb clarified context; wenzelm parents: 61986 diff changeset	38	val xml = export_proof @{context} @{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>
62922 96691631c1eb clarified context; wenzelm parents: 61986 diff changeset	43	val xml = export_proof @{context} @{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>
62922 96691631c1eb clarified context; wenzelm parents: 61986 diff changeset	50	val xml = export_proof @{context} @{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;
60157 ccf9241af217 use smaller example that fits into 64MB string limit of Poly/ML x86 platform; wenzelm parents: 58372 diff changeset	52	@{assert} (size (YXML.string_of_body xml) > 1000000);
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	nipkow
	Thu, 13 Sep 2018 06:36:00 +0200
changeset 68983	caedabd2771c
parent 66453	cc19f7ca2ed6
child 69597	ff784d5a5bfb
permissions	-rw-r--r--