merged
authorwenzelm
Thu Aug 15 21:46:43 2019 +0200 (4 days ago)
changeset 70542011196c029e1
parent 70532 fcf3b891ccb1
parent 70541 f3fbc7f3559d
child 70543 33749040b6f8
child 70547 7ce95a5c4aa8
merged
     1.1 --- a/src/Pure/General/cache.scala	Thu Aug 15 16:11:56 2019 +0100
     1.2 +++ b/src/Pure/General/cache.scala	Thu Aug 15 21:46:43 2019 +0200
     1.3 @@ -37,9 +37,6 @@
     1.4      x
     1.5    }
     1.6  
     1.7 -  protected def cache_int(x: Int): Int =
     1.8 -    lookup(x) getOrElse store(x)
     1.9 -
    1.10    protected def cache_string(x: String): String =
    1.11    {
    1.12      if (x == "") ""
    1.13 @@ -58,6 +55,5 @@
    1.14    }
    1.15  
    1.16    // main methods
    1.17 -  def int(x: Int): Int = synchronized { cache_int(x) }
    1.18    def string(x: String): String = synchronized { cache_string(x) }
    1.19  }
     2.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 15 16:11:56 2019 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 15 21:46:43 2019 +0200
     2.3 @@ -390,6 +390,9 @@
     2.4      def iterator: Iterator[(Node.Name, Node)] =
     2.5        graph.iterator.map({ case (name, (node, _)) => (name, node) })
     2.6  
     2.7 +    def theory_name(theory: String): Option[Node.Name] =
     2.8 +      graph.keys_iterator.find(name => name.theory == theory)
     2.9 +
    2.10      def commands_loading(file_name: Node.Name): List[Command] =
    2.11        (for {
    2.12          (_, node) <- iterator
     3.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 15 16:11:56 2019 +0100
     3.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 15 21:46:43 2019 +0200
     3.3 @@ -597,7 +597,7 @@
     3.4  
     3.5        | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
     3.6            let
     3.7 -            val {pos, name, prop, ...} = thm_header;
     3.8 +            val {pos, theory_name, name, prop, ...} = thm_header;
     3.9              val prf = Proofterm.thm_body_proof_open thm_body;
    3.10              val (vs', tye) = find_inst prop Ts ts vs;
    3.11              val shyps = mk_shyps tye;
    3.12 @@ -622,8 +622,9 @@
    3.13                      val corr_prf = mkabsp shyps corr_prf0;
    3.14                      val corr_prop = Proofterm.prop_of corr_prf;
    3.15                      val corr_header =
    3.16 -                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs')
    3.17 -                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    3.18 +                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
    3.19 +                        (corr_name name vs') corr_prop
    3.20 +                        (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    3.21                      val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
    3.22                      val corr_prf' =
    3.23                        Proofterm.proof_combP
    3.24 @@ -698,7 +699,7 @@
    3.25  
    3.26        | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
    3.27            let
    3.28 -            val {pos, name = s, prop, ...} = thm_header;
    3.29 +            val {pos, theory_name, name = s, prop, ...} = thm_header;
    3.30              val prf = Proofterm.thm_body_proof_open thm_body;
    3.31              val (vs', tye) = find_inst prop Ts ts vs;
    3.32              val shyps = mk_shyps tye;
    3.33 @@ -742,8 +743,9 @@
    3.34                               SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
    3.35                      val corr_prop = Proofterm.prop_of corr_prf';
    3.36                      val corr_header =
    3.37 -                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs')
    3.38 -                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    3.39 +                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
    3.40 +                        (corr_name s vs') corr_prop
    3.41 +                        (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    3.42                      val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
    3.43                      val corr_prf'' =
    3.44                        Proofterm.proof_combP (Proofterm.proof_combt
     4.1 --- a/src/Pure/Thy/export.scala	Thu Aug 15 16:11:56 2019 +0100
     4.2 +++ b/src/Pure/Thy/export.scala	Thu Aug 15 21:46:43 2019 +0200
     4.3 @@ -226,6 +226,10 @@
     4.4          def apply(export_name: String): Option[Entry] =
     4.5            read_entry(db, session_name, theory_name, export_name)
     4.6  
     4.7 +        def focus(other_theory: String): Provider =
     4.8 +          if (other_theory == theory_name) this
     4.9 +          else Provider.database(db, session_name, other_theory)
    4.10 +
    4.11          override def toString: String = db.toString
    4.12        }
    4.13  
    4.14 @@ -234,6 +238,15 @@
    4.15          def apply(export_name: String): Option[Entry] =
    4.16            snapshot.exports_map.get(export_name)
    4.17  
    4.18 +        def focus(other_theory: String): Provider =
    4.19 +          if (other_theory == snapshot.node_name.theory) this
    4.20 +          else {
    4.21 +            val node_name =
    4.22 +              snapshot.version.nodes.theory_name(other_theory) getOrElse
    4.23 +                error("Bad theory " + quote(other_theory))
    4.24 +            Provider.snapshot(snapshot.state.snapshot(node_name))
    4.25 +          }
    4.26 +
    4.27          override def toString: String = snapshot.toString
    4.28        }
    4.29  
    4.30 @@ -242,6 +255,10 @@
    4.31          def apply(export_name: String): Option[Entry] =
    4.32            read_entry(dir, session_name, theory_name, export_name)
    4.33  
    4.34 +        def focus(other_theory: String): Provider =
    4.35 +          if (other_theory == theory_name) this
    4.36 +          else Provider.directory(dir, session_name, other_theory)
    4.37 +
    4.38          override def toString: String = dir.toString
    4.39        }
    4.40    }
    4.41 @@ -255,6 +272,8 @@
    4.42          case Some(entry) => entry.uncompressed_yxml(cache = cache)
    4.43          case None => Nil
    4.44        }
    4.45 +
    4.46 +    def focus(other_theory: String): Provider
    4.47    }
    4.48  
    4.49  
     5.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 15 16:11:56 2019 +0100
     5.2 +++ b/src/Pure/Thy/export_theory.ML	Thu Aug 15 21:46:43 2019 +0200
     5.3 @@ -220,40 +220,40 @@
     5.4  
     5.5      (* axioms and facts *)
     5.6  
     5.7 -    fun prop_of raw_thm =
     5.8 +    fun standard_prop used extra_shyps raw_prop raw_proof =
     5.9        let
    5.10 -        val thm = raw_thm
    5.11 -          |> Thm.transfer thy
    5.12 -          |> Thm.check_hyps (Context.Theory thy)
    5.13 -          |> Thm.strip_shyps;
    5.14 -        val prop = thm
    5.15 -          |> Thm.full_prop_of;
    5.16 -      in (Thm.extra_shyps thm, prop) end;
    5.17 -
    5.18 -    fun encode_prop used (Ss, raw_prop) =
    5.19 -      let
    5.20 -        val prop = Proofterm.standard_vars_term used raw_prop;
    5.21 +        val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
    5.22          val args = rev (add_frees used prop []);
    5.23          val typargs = rev (add_tfrees used prop []);
    5.24 -        val used' = fold (Name.declare o #1) typargs used;
    5.25 -        val sorts = Name.invent used' Name.aT (length Ss) ~~ Ss;
    5.26 -      in
    5.27 -        (sorts @ typargs, args, prop) |>
    5.28 -          let open XML.Encode Term_XML.Encode
    5.29 -          in triple (list (pair string sort)) (list (pair string typ)) term end
    5.30 -      end;
    5.31 +        val used_typargs = fold (Name.declare o #1) typargs used;
    5.32 +        val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
    5.33 +      in ((sorts @ typargs, args, prop), proof) end;
    5.34 +
    5.35 +    val encode_prop =
    5.36 +      let open XML.Encode Term_XML.Encode
    5.37 +      in triple (list (pair string sort)) (list (pair string typ)) term end;
    5.38 +
    5.39 +    fun encode_axiom used prop =
    5.40 +      encode_prop (#1 (standard_prop used [] prop NONE));
    5.41  
    5.42 -    fun encode_axiom used t = encode_prop used ([], t);
    5.43 +    val clean_thm =
    5.44 +      Thm.transfer thy
    5.45 +      #> Thm.check_hyps (Context.Theory thy)
    5.46 +      #> Thm.strip_shyps;
    5.47  
    5.48 -    val encode_fact = encode_prop Name.context;
    5.49 -    val encode_fact_single = encode_fact o prop_of;
    5.50 -    val encode_fact_multi = XML.Encode.list encode_fact o map prop_of;
    5.51 +    val encode_fact = clean_thm #> (fn thm =>
    5.52 +      standard_prop Name.context
    5.53 +        (Thm.extra_shyps thm)
    5.54 +        (Thm.full_prop_of thm)
    5.55 +        (try Thm.reconstruct_proof_of thm) |>
    5.56 +      let open XML.Encode Term_XML.Encode
    5.57 +      in pair encode_prop (option Proofterm.encode_full) end);
    5.58  
    5.59      val _ =
    5.60        export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t))
    5.61          Theory.axiom_space (Theory.axioms_of thy);
    5.62      val _ =
    5.63 -      export_entities "facts" (K (SOME o encode_fact_multi))
    5.64 +      export_entities "facts" (K (SOME o XML.Encode.list encode_fact))
    5.65          (Facts.space_of o Global_Theory.facts_of)
    5.66          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    5.67  
    5.68 @@ -262,12 +262,12 @@
    5.69  
    5.70      val encode_class =
    5.71        let open XML.Encode Term_XML.Encode
    5.72 -      in pair (list (pair string typ)) (list encode_fact_single) end;
    5.73 +      in pair (list (pair string typ)) (list (encode_axiom Name.context)) end;
    5.74  
    5.75      fun export_class name =
    5.76        (case try (Axclass.get_info thy) name of
    5.77          NONE => ([], [])
    5.78 -      | SOME {params, axioms, ...} => (params, axioms))
    5.79 +      | SOME {params, axioms, ...} => (params, map (Thm.plain_prop_of o clean_thm) axioms))
    5.80        |> encode_class |> SOME;
    5.81  
    5.82      val _ =
     6.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 15 16:11:56 2019 +0100
     6.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 15 21:46:43 2019 +0200
     6.3 @@ -65,6 +65,7 @@
     6.4    /** theory content **/
     6.5  
     6.6    val export_prefix: String = "theory/"
     6.7 +  val export_prefix_proofs: String = "proofs/"
     6.8  
     6.9    sealed case class Theory(name: String, parents: List[String],
    6.10      types: List[Type],
    6.11 @@ -284,7 +285,7 @@
    6.12        })
    6.13  
    6.14  
    6.15 -  /* facts */
    6.16 +  /* axioms and facts */
    6.17  
    6.18    sealed case class Prop(
    6.19      typargs: List[(String, Term.Sort)],
    6.20 @@ -309,23 +310,45 @@
    6.21      Prop(typargs, args, t)
    6.22    }
    6.23  
    6.24 -  sealed case class Fact_Single(entity: Entity, prop: Prop)
    6.25 +
    6.26 +  sealed case class Fact(prop: Prop, proof: Option[Term.Proof])
    6.27 +  {
    6.28 +    def cache(cache: Term.Cache): Fact =
    6.29 +      Fact(prop.cache(cache), proof.map(cache.proof _))
    6.30 +  }
    6.31 +
    6.32 +  def decode_fact(body: XML.Body): Fact =
    6.33 +  {
    6.34 +    val (prop, proof) =
    6.35 +    {
    6.36 +      import XML.Decode._
    6.37 +      pair(decode_prop _, option(Term_XML.Decode.proof))(body)
    6.38 +    }
    6.39 +    Fact(prop, proof)
    6.40 +  }
    6.41 +
    6.42 +  sealed case class Fact_Single(entity: Entity, fact: Fact)
    6.43    {
    6.44      def cache(cache: Term.Cache): Fact_Single =
    6.45 -      Fact_Single(entity.cache(cache), prop.cache(cache))
    6.46 +      Fact_Single(entity.cache(cache), fact.cache(cache))
    6.47 +
    6.48 +    def prop: Prop = fact.prop
    6.49 +    def proof: Option[Term.Proof] = fact.proof
    6.50    }
    6.51  
    6.52 -  sealed case class Fact_Multi(entity: Entity, props: List[Prop])
    6.53 +  sealed case class Fact_Multi(entity: Entity, facts: List[Fact])
    6.54    {
    6.55      def cache(cache: Term.Cache): Fact_Multi =
    6.56 -      Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
    6.57 +      Fact_Multi(entity.cache(cache), facts.map(_.cache(cache)))
    6.58 +
    6.59 +    def props: List[Prop] = facts.map(_.prop)
    6.60  
    6.61      def split: List[Fact_Single] =
    6.62 -      props match {
    6.63 -        case List(prop) => List(Fact_Single(entity, prop))
    6.64 +      facts match {
    6.65 +        case List(fact) => List(Fact_Single(entity, fact))
    6.66          case _ =>
    6.67 -          for ((prop, i) <- props.zipWithIndex)
    6.68 -          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
    6.69 +          for ((fact, i) <- facts.zipWithIndex)
    6.70 +          yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact)
    6.71        }
    6.72    }
    6.73  
    6.74 @@ -334,17 +357,32 @@
    6.75        {
    6.76          val (entity, body) = decode_entity(Kind.AXIOM, tree)
    6.77          val prop = decode_prop(body)
    6.78 -        Fact_Single(entity, prop)
    6.79 +        Fact_Single(entity, Fact(prop, None))
    6.80        })
    6.81  
    6.82    def read_facts(provider: Export.Provider): List[Fact_Multi] =
    6.83      provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
    6.84        {
    6.85          val (entity, body) = decode_entity(Kind.FACT, tree)
    6.86 -        val props = XML.Decode.list(decode_prop)(body)
    6.87 -        Fact_Multi(entity, props)
    6.88 +        val facts = XML.Decode.list(decode_fact)(body)
    6.89 +        Fact_Multi(entity, facts)
    6.90        })
    6.91  
    6.92 +  def read_proof(
    6.93 +    provider: Export.Provider,
    6.94 +    theory_name: String,
    6.95 +    serial: Long,
    6.96 +    cache: Option[Term.Cache] = None): (Term.Term, Term.Proof) =
    6.97 +  {
    6.98 +    val body = provider.focus(theory_name).uncompressed_yxml(export_prefix_proofs + serial)
    6.99 +    if (body.isEmpty) error("Bad proof export " + serial)
   6.100 +    val (prop, proof) = XML.Decode.pair(Term_XML.Decode.term, Term_XML.Decode.proof)(body)
   6.101 +    cache match {
   6.102 +      case None => (prop, proof)
   6.103 +      case Some(cache) => (cache.term(prop), cache.proof(proof))
   6.104 +    }
   6.105 +  }
   6.106 +
   6.107  
   6.108    /* type classes */
   6.109  
     7.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 16:11:56 2019 +0100
     7.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 21:46:43 2019 +0200
     7.3 @@ -11,7 +11,8 @@
     7.4    type thm_node
     7.5    type proof_serial = int
     7.6    type thm_header =
     7.7 -    {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option}
     7.8 +    {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
     7.9 +      prop: term, types: typ list option}
    7.10    type thm_body
    7.11    datatype proof =
    7.12       MinProof
    7.13 @@ -40,7 +41,8 @@
    7.14    type oracle = string * term
    7.15    val proof_of: proof_body -> proof
    7.16    val map_proof_of: (proof -> proof) -> proof_body -> proof_body
    7.17 -  val thm_header: proof_serial -> Position.T list -> string -> term -> typ list option -> thm_header
    7.18 +  val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
    7.19 +    thm_header
    7.20    val thm_body: proof_body -> thm_body
    7.21    val thm_body_proof_raw: thm_body -> proof
    7.22    val thm_body_proof_open: thm_body -> proof
    7.23 @@ -67,6 +69,7 @@
    7.24  
    7.25    val encode: proof XML.Encode.T
    7.26    val encode_body: proof_body XML.Encode.T
    7.27 +  val encode_full: proof XML.Encode.T
    7.28    val decode: proof XML.Decode.T
    7.29    val decode_body: proof_body XML.Decode.T
    7.30  
    7.31 @@ -162,9 +165,8 @@
    7.32    val prop_of: proof -> term
    7.33    val expand_proof: theory -> (string * term option) list -> proof -> proof
    7.34  
    7.35 -  val standard_vars: Name.context -> term list * proof list -> term list * proof list
    7.36 +  val standard_vars: Name.context -> term * proof option -> term * proof option
    7.37    val standard_vars_term: Name.context -> term -> term
    7.38 -  val standard_vars_proof: Name.context -> proof -> proof
    7.39  
    7.40    val proof_serial: unit -> proof_serial
    7.41    val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    7.42 @@ -185,7 +187,8 @@
    7.43  type proof_serial = int;
    7.44  
    7.45  type thm_header =
    7.46 -  {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option};
    7.47 +  {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
    7.48 +    prop: term, types: typ list option};
    7.49  
    7.50  datatype proof =
    7.51     MinProof
    7.52 @@ -217,8 +220,8 @@
    7.53  fun map_proof_of f (PBody {oracles, thms, proof}) =
    7.54    PBody {oracles = oracles, thms = thms, proof = f proof};
    7.55  
    7.56 -fun thm_header serial pos name prop types : thm_header =
    7.57 -  {serial = serial, pos = pos, name = name, prop = prop, types = types};
    7.58 +fun thm_header serial pos theory_name name prop types : thm_header =
    7.59 +  {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
    7.60  
    7.61  val no_export_proof = Lazy.value ();
    7.62  
    7.63 @@ -379,8 +382,8 @@
    7.64    fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    7.65    fn OfClass (a, b) => ([b], typ a),
    7.66    fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    7.67 -  fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
    7.68 -    ([int_atom serial, name],
    7.69 +  fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
    7.70 +    ([int_atom serial, theory_name, name],
    7.71        pair (list properties) (pair term (pair (option (list typ)) proof_body))
    7.72          (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
    7.73  and proof_body (PBody {oracles, thms, proof = prf}) =
    7.74 @@ -389,10 +392,25 @@
    7.75    pair int (triple string term proof_body)
    7.76      (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
    7.77  
    7.78 +fun full_proof prf = prf |> variant
    7.79 + [fn MinProof => ([], []),
    7.80 +  fn PBound a => ([int_atom a], []),
    7.81 +  fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
    7.82 +  fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
    7.83 +  fn a % SOME b => ([], pair full_proof term (a, b)),
    7.84 +  fn a %% b => ([], pair full_proof full_proof (a, b)),
    7.85 +  fn Hyp a => ([], term a),
    7.86 +  fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
    7.87 +  fn OfClass (T, c) => ([c], typ T),
    7.88 +  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
    7.89 +  fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
    7.90 +    ([int_atom serial, theory_name, name], list typ Ts)];
    7.91 +
    7.92  in
    7.93  
    7.94  val encode = proof;
    7.95  val encode_body = proof_body;
    7.96 +val encode_full = full_proof;
    7.97  
    7.98  end;
    7.99  
   7.100 @@ -414,12 +432,12 @@
   7.101    fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
   7.102    fn ([b], a) => OfClass (typ a, b),
   7.103    fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
   7.104 -  fn ([a, b], c) =>
   7.105 +  fn ([a, b, c], d) =>
   7.106      let
   7.107 -      val ((d, (e, (f, g)))) =
   7.108 -        pair (list properties) (pair term (pair (option (list typ)) proof_body)) c;
   7.109 -      val header = thm_header (int_atom a) (map Position.of_properties d) b e f;
   7.110 -    in PThm (header, thm_body g) end]
   7.111 +      val ((e, (f, (g, h)))) =
   7.112 +        pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
   7.113 +      val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
   7.114 +    in PThm (header, thm_body h) end]
   7.115  and proof_body x =
   7.116    let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
   7.117    in PBody {oracles = a, thms = b, proof = c} end
   7.118 @@ -493,8 +511,8 @@
   7.119        | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
   7.120        | proof (OfClass T_c) = ofclass T_c
   7.121        | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
   7.122 -      | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
   7.123 -          PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
   7.124 +      | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
   7.125 +          PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
   7.126        | proof _ = raise Same.SAME;
   7.127    in proof end;
   7.128  
   7.129 @@ -533,8 +551,8 @@
   7.130  fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   7.131    | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   7.132    | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
   7.133 -  | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
   7.134 -      PThm (thm_header serial pos name prop types, thm_body)
   7.135 +  | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
   7.136 +      PThm (thm_header serial pos theory_name name prop types, thm_body)
   7.137    | change_types _ prf = prf;
   7.138  
   7.139  
   7.140 @@ -681,8 +699,9 @@
   7.141            OfClass (htypeT Envir.norm_type_same T, c)
   7.142        | norm (Oracle (s, prop, Ts)) =
   7.143            Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
   7.144 -      | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
   7.145 -          PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
   7.146 +      | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
   7.147 +          PThm (thm_header i p theory_name a t
   7.148 +            (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
   7.149        | norm _ = raise Same.SAME;
   7.150    in Same.commit norm end;
   7.151  
   7.152 @@ -998,9 +1017,9 @@
   7.153            OfClass (Logic.incr_tvar_same inc T, c)
   7.154        | lift' _ _ (Oracle (s, prop, Ts)) =
   7.155            Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
   7.156 -      | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
   7.157 -          PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
   7.158 -            thm_body)
   7.159 +      | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
   7.160 +          PThm (thm_header i p theory_name s prop
   7.161 +            ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
   7.162        | lift' _ _ _ = raise Same.SAME
   7.163      and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
   7.164  
   7.165 @@ -1429,8 +1448,8 @@
   7.166        | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
   7.167        | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
   7.168        | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
   7.169 -      | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
   7.170 -          PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
   7.171 +      | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
   7.172 +          PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
   7.173        | subst _ _ _ = raise Same.SAME;
   7.174    in fn t => subst 0 0 t handle Same.SAME => t end;
   7.175  
   7.176 @@ -2023,31 +2042,43 @@
   7.177    | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
   7.178    | variant_proof _ prf = prf;
   7.179  
   7.180 +val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   7.181 +fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
   7.182 +val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
   7.183 +
   7.184 +val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
   7.185 +val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
   7.186 +val unvarify_proof = map_proof_terms unvarify unvarifyT;
   7.187 +
   7.188 +fun hidden_types prop proof =
   7.189 +  let
   7.190 +    val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
   7.191 +    val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
   7.192 +  in rev (fold_proof_terms (fold_types add_hiddenT) add_hiddenT proof []) end;
   7.193 +
   7.194 +fun standard_hidden_types term proof =
   7.195 +  let
   7.196 +    val hidden = hidden_types term proof;
   7.197 +    val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
   7.198 +    fun smash T = if member (op =) hidden T then TVar (("'", idx), Type.sort_of_atyp T) else T;
   7.199 +    val smashT = map_atyps smash;
   7.200 +  in map_proof_terms (map_types smashT) smashT proof end;
   7.201 +
   7.202  in
   7.203  
   7.204 -fun standard_vars used (terms, proofs) =
   7.205 +fun standard_vars used (term, opt_proof) =
   7.206    let
   7.207 -    val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
   7.208 -    val inst = Term_Subst.zero_var_indexes_inst used (terms @ proof_terms);
   7.209 +    val proofs = the_list (Option.map (standard_hidden_types term) opt_proof);
   7.210 +    val proof_terms = rev (fold (fold_proof_terms cons (cons o Logic.mk_type)) proofs []);
   7.211 +    val used_frees = used
   7.212 +      |> used_frees_term term
   7.213 +      |> fold used_frees_proof proofs;
   7.214 +    val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
   7.215 +    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
   7.216 +    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
   7.217 +  in (term', try hd proofs') end;
   7.218  
   7.219 -    val is_used = Name.is_declared used o Name.clean;
   7.220 -    fun unvarifyT ty = ty |> Term.map_atyps
   7.221 -      (fn TVar ((a, _), S) => TFree (a, S)
   7.222 -        | T as TFree (a, _) => if is_used a then T else raise TYPE (Logic.bad_fixed a, [ty], [])
   7.223 -        | T => T);
   7.224 -    fun unvarify tm = tm |> Term.map_aterms
   7.225 -      (fn Var ((x, _), T) => Free (x, T)
   7.226 -        | t as Free (x, _) => if is_used x then t else raise TERM (Logic.bad_fixed x, [tm])
   7.227 -        | t => t);
   7.228 -
   7.229 -    val terms' = terms
   7.230 -      |> map (Term_Subst.instantiate inst #> unvarify #> map_types unvarifyT #> variant_term []);
   7.231 -    val proofs' = proofs
   7.232 -      |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
   7.233 -  in (terms', proofs') end;
   7.234 -
   7.235 -fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
   7.236 -fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
   7.237 +fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
   7.238  
   7.239  end;
   7.240  
   7.241 @@ -2076,37 +2107,14 @@
   7.242  
   7.243  fun clean_proof thy = rew_proof thy #> shrink_proof;
   7.244  
   7.245 -
   7.246 -local open XML.Encode Term_XML.Encode in
   7.247 -
   7.248 -fun proof prf = prf |> variant
   7.249 - [fn MinProof => ([], []),
   7.250 -  fn PBound a => ([int_atom a], []),
   7.251 -  fn Abst (a, SOME b, c) => ([a], pair typ proof (b, c)),
   7.252 -  fn AbsP (a, SOME b, c) => ([a], pair term proof (b, c)),
   7.253 -  fn a % SOME b => ([], pair proof term (a, b)),
   7.254 -  fn a %% b => ([], pair proof proof (a, b)),
   7.255 -  fn Hyp a => ([], term a),
   7.256 -  fn PAxm (name, b, SOME Ts) => ([name], list typ Ts),
   7.257 -  fn OfClass (T, c) => ([c], typ T),
   7.258 -  fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
   7.259 -  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
   7.260 -
   7.261 -fun encode_export prop prf = pair term proof (prop, prf);
   7.262 -
   7.263 -
   7.264 -val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   7.265 -fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
   7.266 -val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
   7.267 -
   7.268 -end;
   7.269 +fun encode_export prop prf =
   7.270 +  let open XML.Encode Term_XML.Encode
   7.271 +  in pair term encode_full (prop, prf) end;
   7.272  
   7.273  fun export_proof thy i prop prf =
   7.274    let
   7.275 -    val free_names = Name.context
   7.276 -      |> used_frees_term prop
   7.277 -      |> used_frees_proof prf;
   7.278 -    val ([prop'], [prf']) = standard_vars free_names ([prop], [reconstruct_proof thy prop prf]);
   7.279 +    val (prop', SOME prf') =
   7.280 +      standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
   7.281      val xml = encode_export prop' prf';
   7.282      val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
   7.283    in
   7.284 @@ -2188,7 +2196,8 @@
   7.285  
   7.286      val pthm = (i, make_thm_node name prop1 body');
   7.287  
   7.288 -    val header = thm_header i ([pos, Position.thread_data ()]) name prop1 NONE;
   7.289 +    val header =
   7.290 +      thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
   7.291      val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
   7.292      val head = PThm (header, thm_body);
   7.293      val proof =
     8.1 --- a/src/Pure/term.scala	Thu Aug 15 16:11:56 2019 +0100
     8.2 +++ b/src/Pure/term.scala	Thu Aug 15 21:46:43 2019 +0200
     8.3 @@ -13,7 +13,22 @@
     8.4  {
     8.5    /* types and terms */
     8.6  
     8.7 -  type Indexname = (String, Int)
     8.8 +  sealed case class Indexname(name: String, index: Int)
     8.9 +  {
    8.10 +    override def toString: String =
    8.11 +      if (index == -1) name
    8.12 +      else {
    8.13 +        val dot =
    8.14 +          Symbol.explode(name).reverse match {
    8.15 +            case _ :: s :: _ if s == Symbol.sub_decoded || s == Symbol.sub => false
    8.16 +            case c :: _ => Symbol.is_digit(c)
    8.17 +            case _ => true
    8.18 +          }
    8.19 +        if (dot) "?" + name + "." + index
    8.20 +        else if (index != 0) "?" + name + index
    8.21 +        else "?" + name
    8.22 +      }
    8.23 +  }
    8.24  
    8.25    type Sort = List[String]
    8.26    val dummyS: Sort = List("")
    8.27 @@ -32,6 +47,20 @@
    8.28    case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
    8.29    case class App(fun: Term, arg: Term) extends Term
    8.30  
    8.31 +  sealed abstract class Proof
    8.32 +  case object MinProof extends Proof
    8.33 +  case class PBound(index: Int) extends Proof
    8.34 +  case class Abst(name: String, typ: Typ, body: Proof) extends Proof
    8.35 +  case class AbsP(name: String, hyp: Term, body: Proof) extends Proof
    8.36 +  case class Appt(fun: Proof, arg: Term) extends Proof
    8.37 +  case class AppP(fun: Proof, arg: Proof) extends Proof
    8.38 +  case class Hyp(hyp: Term) extends Proof
    8.39 +  case class PAxm(name: String, types: List[Typ]) extends Proof
    8.40 +  case class OfClass(typ: Typ, cls: String) extends Proof
    8.41 +  case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
    8.42 +  case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
    8.43 +    extends Proof
    8.44 +
    8.45  
    8.46    /* Pure logic */
    8.47  
    8.48 @@ -87,7 +116,7 @@
    8.49      extends isabelle.Cache(initial_size, max_string)
    8.50    {
    8.51      protected def cache_indexname(x: Indexname): Indexname =
    8.52 -      lookup(x) getOrElse store(cache_string(x._1), cache_int(x._2))
    8.53 +      lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
    8.54  
    8.55      protected def cache_sort(x: Sort): Sort =
    8.56        if (x == dummyS) dummyS
    8.57 @@ -101,13 +130,24 @@
    8.58            case Some(y) => y
    8.59            case None =>
    8.60              x match {
    8.61 -              case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_))))
    8.62 +              case Type(name, args) => store(Type(cache_string(name), cache_typs(args)))
    8.63                case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort)))
    8.64                case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort)))
    8.65              }
    8.66          }
    8.67      }
    8.68  
    8.69 +    protected def cache_typs(x: List[Typ]): List[Typ] =
    8.70 +    {
    8.71 +      if (x.isEmpty) Nil
    8.72 +      else {
    8.73 +        lookup(x) match {
    8.74 +          case Some(y) => y
    8.75 +          case None => store(x.map(cache_typ(_)))
    8.76 +        }
    8.77 +      }
    8.78 +    }
    8.79 +
    8.80      protected def cache_term(x: Term): Term =
    8.81      {
    8.82        lookup(x) match {
    8.83 @@ -117,7 +157,7 @@
    8.84              case Const(name, typ) => store(Const(cache_string(name), cache_typ(typ)))
    8.85              case Free(name, typ) => store(Free(cache_string(name), cache_typ(typ)))
    8.86              case Var(name, typ) => store(Var(cache_indexname(name), cache_typ(typ)))
    8.87 -            case Bound(index) => store(Bound(cache_int(index)))
    8.88 +            case Bound(_) => store(x)
    8.89              case Abs(name, typ, body) =>
    8.90                store(Abs(cache_string(name), cache_typ(typ), cache_term(body)))
    8.91              case App(fun, arg) => store(App(cache_term(fun), cache_term(arg)))
    8.92 @@ -125,11 +165,39 @@
    8.93        }
    8.94      }
    8.95  
    8.96 +    protected def cache_proof(x: Proof): Proof =
    8.97 +    {
    8.98 +      if (x == MinProof) MinProof
    8.99 +      else {
   8.100 +        lookup(x) match {
   8.101 +          case Some(y) => y
   8.102 +          case None =>
   8.103 +            x match {
   8.104 +              case PBound(_) => store(x)
   8.105 +              case Abst(name, typ, body) =>
   8.106 +                store(Abst(cache_string(name), cache_typ(typ), cache_proof(body)))
   8.107 +              case AbsP(name, hyp, body) =>
   8.108 +                store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body)))
   8.109 +              case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg)))
   8.110 +              case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg)))
   8.111 +              case Hyp(hyp) => store(Hyp(cache_term(hyp)))
   8.112 +              case PAxm(name, types) => store(PAxm(cache_string(name), cache_typs(types)))
   8.113 +              case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
   8.114 +              case Oracle(name, prop, types) =>
   8.115 +                store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
   8.116 +              case PThm(serial, theory_name, name, types) =>
   8.117 +                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
   8.118 +            }
   8.119 +        }
   8.120 +      }
   8.121 +    }
   8.122 +
   8.123      // main methods
   8.124      def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) }
   8.125      def sort(x: Sort): Sort = synchronized { cache_sort(x) }
   8.126      def typ(x: Typ): Typ = synchronized { cache_typ(x) }
   8.127      def term(x: Term): Term = synchronized { cache_term(x) }
   8.128 +    def proof(x: Proof): Proof = synchronized { cache_proof(x) }
   8.129  
   8.130      def position(x: Position.T): Position.T =
   8.131        synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) }
     9.1 --- a/src/Pure/term_xml.scala	Thu Aug 15 16:11:56 2019 +0100
     9.2 +++ b/src/Pure/term_xml.scala	Thu Aug 15 21:46:43 2019 +0200
     9.3 @@ -21,13 +21,13 @@
     9.4        variant[Typ](List(
     9.5          { case Type(a, b) => (List(a), list(typ)(b)) },
     9.6          { case TFree(a, b) => (List(a), sort(b)) },
     9.7 -        { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
     9.8 +        { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
     9.9  
    9.10      def term: T[Term] =
    9.11        variant[Term](List(
    9.12          { case Const(a, b) => (List(a), typ(b)) },
    9.13          { case Free(a, b) => (List(a), typ(b)) },
    9.14 -        { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
    9.15 +        { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
    9.16          { case Bound(a) => (List(int_atom(a)), Nil) },
    9.17          { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
    9.18          { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
    9.19 @@ -43,15 +43,29 @@
    9.20        variant[Typ](List(
    9.21          { case (List(a), b) => Type(a, list(typ)(b)) },
    9.22          { case (List(a), b) => TFree(a, sort(b)) },
    9.23 -        { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
    9.24 +        { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
    9.25  
    9.26      def term: T[Term] =
    9.27        variant[Term](List(
    9.28          { case (List(a), b) => Const(a, typ(b)) },
    9.29          { case (List(a), b) => Free(a, typ(b)) },
    9.30 -        { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
    9.31 +        { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
    9.32          { case (List(a), Nil) => Bound(int_atom(a)) },
    9.33          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
    9.34          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
    9.35 +
    9.36 +    def proof: T[Proof] =
    9.37 +      variant[Proof](List(
    9.38 +        { case (Nil, Nil) => MinProof },
    9.39 +        { case (List(a), Nil) => PBound(int_atom(a)) },
    9.40 +        { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
    9.41 +        { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
    9.42 +        { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
    9.43 +        { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
    9.44 +        { case (Nil, a) => Hyp(term(a)) },
    9.45 +        { case (List(a), b) => PAxm(a, list(typ)(b)) },
    9.46 +        { case (List(a), b) => OfClass(typ(b), a) },
    9.47 +        { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
    9.48 +        { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
    9.49    }
    9.50  }