merged

--- a/src/Doc/IsarImplementation/Logic.thy	Fri Jul 12 21:07:34 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Fri Jul 12 21:14:54 2013 +0200
@@ -1455,58 +1455,9 @@
     |> Drule.export_without_context;
 *}
 
-text {* \medskip The subsequent example illustrates the use of various
-  key operations on proof terms: the proof term of an existing theorem
-  is reconstructed and turned again into a theorem using the proof
-  checker; some informative output is printed as well.  *}
-
-ML {*
-  fun recheck ctxt0 thm0 =
-    let
-      (*formal transfer and import -- avoid schematic variables*)
-      val thy = Proof_Context.theory_of ctxt0;
-      val ((_, [thm]), ctxt) =
-        Variable.import true [Thm.transfer thy thm0] ctxt0;
-
-      (*main proof information*)
-      val prop = Thm.prop_of thm;
-      val prf =
-        Proofterm.proof_of
-          (Proofterm.strip_thm (Thm.proof_body_of thm));
-      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
-
-      (*informative output*)
-      fun pretty_item name prt =
-        Pretty.block [Pretty.str name, Pretty.brk 1, prt];
-      val _ =
-        [pretty_item "proposition:" (Syntax.pretty_term ctxt prop),
-         pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf),
-         pretty_item "full proof:"
-          (Proof_Syntax.pretty_proof ctxt full_prf)]
-        |> Pretty.chunks |> Pretty.writeln;
-    in
-      (*rechecked theorem*)
-      Proof_Checker.thm_of_proof thy full_prf
-      |> singleton (Proof_Context.export ctxt ctxt0)
-    end;
-*}
-
-text {* As anticipated, the rechecked theorem establishes the same
-  proposition: *}
-
-ML_val {*
-  val thm = @{thm ex};
-  val thm' = recheck @{context} thm;
-  @{assert} (Thm.eq_thm_prop (thm, thm'));
-*}
-
-text {* More precise theorem equality is achieved by adjusting a few
-  accidental details of the theorems involved here: *}
-
-ML_val {*
-  val thm = Thm.map_tags (K []) @{thm ex};
-  val thm' = Thm.strip_shyps (recheck @{context} thm);
-  @{assert} (Thm.eq_thm (thm, thm'));
+text {* \medskip See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"}
+  for further examples, with export and import of proof terms via
+  XML/ML data representation.
 *}
 
 end

--- a/src/HOL/Proofs/ex/XML_Data.thy	Fri Jul 12 21:07:34 2013 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Fri Jul 12 21:14:54 2013 +0200
@@ -1,47 +1,66 @@
 (*  Title:      HOL/Proofs/ex/XML_Data.thy
     Author:     Makarius
+    Author:     Stefan Berghofer
 
 XML data representation of proof terms.
 *)
 
 theory XML_Data
-imports Main
+imports "~~/src/HOL/Isar_Examples/Drinker"
 begin
 
 subsection {* Export and re-import of global proof terms *}
 
 ML {*
-  fun export_proof thm0 =
+  fun export_proof thm =
     let
-      val thy = Thm.theory_of_thm thm0;
-      val ctxt0 = Proof_Context.init_global thy;
-      val thy = Proof_Context.theory_of ctxt0;
-      val ((_, [thm]), ctxt) = Variable.import true [Thm.transfer thy thm0] ctxt0;
-
-      val prop = Thm.prop_of thm;  (* FIXME proper prop (wrt. import / strip) (!??) *)
+      val thy = Thm.theory_of_thm thm;
+      val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
+      val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
       val prf =
-        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
-        |> Proofterm.no_thm_proofs;
-    in XML.Encode.pair Term_XML.Encode.term Proofterm.encode (prop, prf) end;
+        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
+        Reconstruct.reconstruct_proof thy prop |>
+        Reconstruct.expand_proof thy [("", NONE)] |>
+        Proofterm.rew_proof thy |>
+        Proofterm.no_thm_proofs;
+    in Proofterm.encode prf end;
 
   fun import_proof thy xml =
     let
-      val (prop, prf) = XML.Decode.pair Term_XML.Decode.term Proofterm.decode xml;
-      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
-    in Drule.export_without_context (Proof_Checker.thm_of_proof thy full_prf) end;
+      val prf = Proofterm.decode xml;
+      val (prf', _) = Proofterm.freeze_thaw_prf prf;
+    in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
 *}
 
 
-subsection {* Example *}
+subsection {* Examples *}
 
 ML {* val thy1 = @{theory} *}
 
 lemma ex: "A \<longrightarrow> A" ..
 
-ML {*
+ML_val {*
   val xml = export_proof @{thm ex};
   val thm = import_proof thy1 xml;
 *}
 
+ML_val {*
+  val xml = export_proof @{thm de_Morgan};
+  val thm = import_proof thy1 xml;
+*}
+
+ML_val {*
+  val xml = export_proof @{thm Drinker's_Principle};
+  val thm = import_proof thy1 xml;
+*}
+
+text {* Some fairly large proof: *}
+
+ML_val {*
+  val xml = export_proof @{thm Int.times_int.abs_eq};
+  val thm = import_proof thy1 xml;
+  @{assert} (size (YXML.string_of_body xml) > 50000000);
+*}
+
 end