# HG changeset patch
# User wenzelm
# Date 1565878017 -7200
# Node ID fb876ebbf5a711ef4c9a0fa27d0965038f49cd71
# Parent  031620901fcdad8c7030e2580e02bc71a2a03819
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;

diff -r 031620901fcd -r fb876ebbf5a7 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:02:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:06:57 2019 +0200
@@ -220,40 +220,43 @@
 
     (* axioms and facts *)
 
-    fun prop_of raw_thm =
+    fun standard_prop used extra_shyps raw_prop raw_proof =
       let
-        val thm = raw_thm
-          |> Thm.transfer thy
-          |> Thm.check_hyps (Context.Theory thy)
-          |> Thm.strip_shyps;
-        val prop = thm
-          |> Thm.full_prop_of;
-      in (Thm.extra_shyps thm, prop) end;
+        val raw_proofs = the_list raw_proof;
+        val used_proofs = used |> fold Proofterm.used_frees_proof raw_proofs;
+        val ([prop], proofs) = ([raw_prop], raw_proofs) |> Proofterm.standard_vars used_proofs;
 
-    fun encode_prop used (Ss, raw_prop) =
-      let
-        val prop = Proofterm.standard_vars_term used raw_prop;
         val args = rev (add_frees used prop []);
         val typargs = rev (add_tfrees used prop []);
-        val used' = fold (Name.declare o #1) typargs used;
-        val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
-      in
-        (sorts @ typargs, args, prop) |>
-          let open XML.Encode Term_XML.Encode
-          in triple (list (pair string sort)) (list (pair string typ)) term end
-      end;
+        val used_typargs = fold (Name.declare o #1) typargs used;
+        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
+      in ((sorts @ typargs, args, prop), try hd proofs) end;
+
+    val encode_prop =
+      let open XML.Encode Term_XML.Encode
+      in triple (list (pair string sort)) (list (pair string typ)) term end;
+
+    fun encode_axiom used prop =
+      encode_prop (#1 (standard_prop used [] prop NONE));
 
-    fun encode_axiom used t = encode_prop used ([], t);
+    val clean_thm =
+      Thm.transfer thy
+      #> Thm.check_hyps (Context.Theory thy)
+      #> Thm.strip_shyps;
 
-    val encode_fact = encode_prop Name.context;
-    val encode_fact_single = encode_fact o prop_of;
-    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
+    val encode_fact = clean_thm #> (fn thm =>
+      standard_prop Name.context
+        (Thm.extra_shyps thm)
+        (Thm.full_prop_of thm)
+        (try Thm.reconstruct_proof_of thm) |>
+      let open XML.Encode Term_XML.Encode
+      in pair encode_prop (option Proofterm.encode_full) end);
 
     val _ =
       export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
         Theory.axiom_space (Theory.axioms_of thy);
     val _ =
-      export_entities "facts" (K (SOME o encode_fact_multi))
+      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
         (Facts.space_of o Global_Theory.facts_of)
         (Facts.dest_static true [] (Global_Theory.facts_of thy));
 
@@ -262,12 +265,12 @@
 
     val encode_class =
       let open XML.Encode Term_XML.Encode
-      in pair (list (pair string typ)) (list encode_fact_single) end;
+      in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
 
     fun export_class name =
       (case try (Axclass.get_info thy) name of
         NONE => ([], [])
-      | SOME {params, axioms, ...} => (params, axioms))
+      | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
       |> encode_class |> SOME;
 
     val _ =
diff -r 031620901fcd -r fb876ebbf5a7 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:02:47 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:06:57 2019 +0200
@@ -284,7 +284,7 @@
       })
 
 
-  /* facts */
+  /* axioms and facts */
 
   sealed case class Prop(
     typargs: List[(String, Term.Sort)],
@@ -309,23 +309,45 @@
     Prop(typargs, args, t)
   }
 
-  sealed case class Fact_Single(entity: Entity, prop: Prop)
+
+  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
+  {
+    def cache(cache: Term.Cache): Fact =
+      Fact(prop.cache(cache), proof.map(cache.proof _))
+  }
+
+  def decode_fact(body: XML.Body): Fact =
+  {
+    val (prop, proof) =
+    {
+      import XML.Decode._
+      pair(decode_prop _, option(Term_XML.Decode.proof))(body)
+    }
+    Fact(prop, proof)
+  }
+
+  sealed case class Fact_Single(entity: Entity, fact: Fact)
   {
     def cache(cache: Term.Cache): Fact_Single =
-      Fact_Single(entity.cache(cache), prop.cache(cache))
+      Fact_Single(entity.cache(cache), fact.cache(cache))
+
+    def prop: Prop = fact.prop
+    def proof: Option[Term.Proof] = fact.proof
   }
 
-  sealed case class Fact_Multi(entity: Entity, props: List[Prop])
+  sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
   {
     def cache(cache: Term.Cache): Fact_Multi =
-      Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
+      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
+
+    def props: List[Prop] = facts.map(_.prop)
 
     def split: List[Fact_Single] =
-      props match {
-        case List(prop) => List(Fact_Single(entity, prop))
+      facts match {
+        case List(fact) => List(Fact_Single(entity, fact))
         case _ =>
-          for ((prop, i) <- props.zipWithIndex)
-          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
+          for ((fact, i) <- facts.zipWithIndex)
+          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
       }
   }
 
@@ -334,15 +356,15 @@
       {
         val (entity, body) = decode_entity(Kind.AXIOM, tree)
         val prop = decode_prop(body)
-        Fact_Single(entity, prop)
+        Fact_Single(entity, Fact(prop, None))
       })
 
   def read_facts(provider: Export.Provider): List[Fact_Multi] =
     provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.FACT, tree)
-        val props = XML.Decode.list(decode_prop)(body)
-        Fact_Multi(entity, props)
+        val facts = XML.Decode.list(decode_fact)(body)
+        Fact_Multi(entity, facts)
       })
 
 
diff -r 031620901fcd -r fb876ebbf5a7 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Aug 15 16:02:47 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Aug 15 16:06:57 2019 +0200
@@ -67,6 +67,7 @@
 
   val encode: proof XML.Encode.T
   val encode_body: proof_body XML.Encode.T
+  val encode_full: proof XML.Encode.T
   val decode: proof XML.Decode.T
   val decode_body: proof_body XML.Decode.T
 
@@ -165,6 +166,9 @@
   val standard_vars: Name.context -> term list * proof list -> term list * proof list
   val standard_vars_term: Name.context -> term -> term
   val standard_vars_proof: Name.context -> proof -> proof
+  val used_frees_type: typ -> Name.context -> Name.context
+  val used_frees_term: term -> Name.context -> Name.context
+  val used_frees_proof: proof -> Name.context -> Name.context
 
   val proof_serial: unit -> proof_serial
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
@@ -389,10 +393,24 @@
   pair int (triple string term proof_body)
     (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
 
+fun full_proof prf = prf |> variant
+ [fn MinProof => ([], []),
+  fn PBound a => ([int_atom a], []),
+  fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
+  fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
+  fn a % SOME b => ([], pair full_proof term (a, b)),
+  fn a %% b => ([], pair full_proof full_proof (a, b)),
+  fn Hyp a => ([], term a),
+  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
+  fn OfClass (T, c) => ([c], typ T),
+  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
+  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
+
 in
 
 val encode = proof;
 val encode_body = proof_body;
+val encode_full = full_proof;
 
 end;
 
@@ -2051,6 +2069,10 @@
 
 end;
 
+val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
+fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
+val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
+
 
 (* PThm nodes *)
 
@@ -2076,30 +2098,9 @@
 
 fun clean_proof thy = rew_proof thy #> shrink_proof;
 
-
-local open XML.Encode Term_XML.Encode in
-
-fun proof prf = prf |> variant
- [fn MinProof => ([], []),
-  fn PBound a => ([int_atom a], []),
-  fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
-  fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
-  fn a % SOME b => ([], pair proof term (a, b)),
-  fn a %% b => ([], pair proof proof (a, b)),
-  fn Hyp a => ([], term a),
-  fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
-  fn OfClass (T, c) => ([c], typ T),
-  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
-  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
-
-fun encode_export prop prf = pair term proof (prop, prf);
-
-
-val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
-val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
-
-end;
+fun encode_export prop prf =
+  let open XML.Encode Term_XML.Encode
+  in pair term encode_full (prop, prf) end;
 
 fun export_proof thy i prop prf =
   let