clarified PThm: theory_name simplifies retrieval from exports;
authorwenzelm
Thu Aug 15 16:57:09 2019 +0200 (4 days ago)
changeset 70538fc9ba6fe367f
parent 70537 17160e0a60b6
child 70539 30b3c58a1933
clarified PThm: theory_name simplifies retrieval from exports;
src/Pure/Proof/extraction.ML
src/Pure/proofterm.ML
src/Pure/term.scala
src/Pure/term_xml.scala
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 15 16:38:55 2019 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 15 16:57:09 2019 +0200
     1.3 @@ -597,7 +597,7 @@
     1.4  
     1.5        | corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
     1.6            let
     1.7 -            val {pos, name, prop, ...} = thm_header;
     1.8 +            val {pos, theory_name, name, prop, ...} = thm_header;
     1.9              val prf = Proofterm.thm_body_proof_open thm_body;
    1.10              val (vs', tye) = find_inst prop Ts ts vs;
    1.11              val shyps = mk_shyps tye;
    1.12 @@ -622,8 +622,9 @@
    1.13                      val corr_prf = mkabsp shyps corr_prf0;
    1.14                      val corr_prop = Proofterm.prop_of corr_prf;
    1.15                      val corr_header =
    1.16 -                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name name vs')
    1.17 -                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    1.18 +                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
    1.19 +                        (corr_name name vs') corr_prop
    1.20 +                        (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    1.21                      val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf);
    1.22                      val corr_prf' =
    1.23                        Proofterm.proof_combP
    1.24 @@ -698,7 +699,7 @@
    1.25  
    1.26        | extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
    1.27            let
    1.28 -            val {pos, name = s, prop, ...} = thm_header;
    1.29 +            val {pos, theory_name, name = s, prop, ...} = thm_header;
    1.30              val prf = Proofterm.thm_body_proof_open thm_body;
    1.31              val (vs', tye) = find_inst prop Ts ts vs;
    1.32              val shyps = mk_shyps tye;
    1.33 @@ -742,8 +743,9 @@
    1.34                               SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
    1.35                      val corr_prop = Proofterm.prop_of corr_prf';
    1.36                      val corr_header =
    1.37 -                      Proofterm.thm_header (Proofterm.proof_serial ()) pos (corr_name s vs')
    1.38 -                        corr_prop (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    1.39 +                      Proofterm.thm_header (Proofterm.proof_serial ()) pos theory_name
    1.40 +                        (corr_name s vs') corr_prop
    1.41 +                        (SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
    1.42                      val corr_body = Proofterm.thm_body (Proofterm.approximate_proof_body corr_prf');
    1.43                      val corr_prf'' =
    1.44                        Proofterm.proof_combP (Proofterm.proof_combt
     2.1 --- a/src/Pure/proofterm.ML	Thu Aug 15 16:38:55 2019 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Thu Aug 15 16:57:09 2019 +0200
     2.3 @@ -11,7 +11,8 @@
     2.4    type thm_node
     2.5    type proof_serial = int
     2.6    type thm_header =
     2.7 -    {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option}
     2.8 +    {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
     2.9 +      prop: term, types: typ list option}
    2.10    type thm_body
    2.11    datatype proof =
    2.12       MinProof
    2.13 @@ -40,7 +41,8 @@
    2.14    type oracle = string * term
    2.15    val proof_of: proof_body -> proof
    2.16    val map_proof_of: (proof -> proof) -> proof_body -> proof_body
    2.17 -  val thm_header: proof_serial -> Position.T list -> string -> term -> typ list option -> thm_header
    2.18 +  val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
    2.19 +    thm_header
    2.20    val thm_body: proof_body -> thm_body
    2.21    val thm_body_proof_raw: thm_body -> proof
    2.22    val thm_body_proof_open: thm_body -> proof
    2.23 @@ -189,7 +191,8 @@
    2.24  type proof_serial = int;
    2.25  
    2.26  type thm_header =
    2.27 -  {serial: proof_serial, pos: Position.T list, name: string, prop: term, types: typ list option};
    2.28 +  {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
    2.29 +    prop: term, types: typ list option};
    2.30  
    2.31  datatype proof =
    2.32     MinProof
    2.33 @@ -221,8 +224,8 @@
    2.34  fun map_proof_of f (PBody {oracles, thms, proof}) =
    2.35    PBody {oracles = oracles, thms = thms, proof = f proof};
    2.36  
    2.37 -fun thm_header serial pos name prop types : thm_header =
    2.38 -  {serial = serial, pos = pos, name = name, prop = prop, types = types};
    2.39 +fun thm_header serial pos theory_name name prop types : thm_header =
    2.40 +  {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
    2.41  
    2.42  val no_export_proof = Lazy.value ();
    2.43  
    2.44 @@ -383,8 +386,8 @@
    2.45    fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    2.46    fn OfClass (a, b) => ([b], typ a),
    2.47    fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    2.48 -  fn PThm ({serial, pos, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
    2.49 -    ([int_atom serial, name],
    2.50 +  fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
    2.51 +    ([int_atom serial, theory_name, name],
    2.52        pair (list properties) (pair term (pair (option (list typ)) proof_body))
    2.53          (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
    2.54  and proof_body (PBody {oracles, thms, proof = prf}) =
    2.55 @@ -404,7 +407,8 @@
    2.56    fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
    2.57    fn OfClass (T, c) => ([c], typ T),
    2.58    fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
    2.59 -  fn PThm ({serial, name, types = SOME Ts, ...}, _) => ([int_atom serial, name], list typ Ts)];
    2.60 +  fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
    2.61 +    ([int_atom serial, theory_name, name], list typ Ts)];
    2.62  
    2.63  in
    2.64  
    2.65 @@ -432,12 +436,12 @@
    2.66    fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
    2.67    fn ([b], a) => OfClass (typ a, b),
    2.68    fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
    2.69 -  fn ([a, b], c) =>
    2.70 +  fn ([a, b, c], d) =>
    2.71      let
    2.72 -      val ((d, (e, (f, g)))) =
    2.73 -        pair (list properties) (pair term (pair (option (list typ)) proof_body)) c;
    2.74 -      val header = thm_header (int_atom a) (map Position.of_properties d) b e f;
    2.75 -    in PThm (header, thm_body g) end]
    2.76 +      val ((e, (f, (g, h)))) =
    2.77 +        pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
    2.78 +      val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
    2.79 +    in PThm (header, thm_body h) end]
    2.80  and proof_body x =
    2.81    let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
    2.82    in PBody {oracles = a, thms = b, proof = c} end
    2.83 @@ -511,8 +515,8 @@
    2.84        | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
    2.85        | proof (OfClass T_c) = ofclass T_c
    2.86        | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
    2.87 -      | proof (PThm ({serial, pos, name, prop, types = SOME Ts}, thm_body)) =
    2.88 -          PThm (thm_header serial pos name prop (SOME (typs Ts)), thm_body)
    2.89 +      | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
    2.90 +          PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
    2.91        | proof _ = raise Same.SAME;
    2.92    in proof end;
    2.93  
    2.94 @@ -551,8 +555,8 @@
    2.95  fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
    2.96    | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
    2.97    | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
    2.98 -  | change_types types (PThm ({serial, pos, name, prop, types = _}, thm_body)) =
    2.99 -      PThm (thm_header serial pos name prop types, thm_body)
   2.100 +  | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
   2.101 +      PThm (thm_header serial pos theory_name name prop types, thm_body)
   2.102    | change_types _ prf = prf;
   2.103  
   2.104  
   2.105 @@ -699,8 +703,9 @@
   2.106            OfClass (htypeT Envir.norm_type_same T, c)
   2.107        | norm (Oracle (s, prop, Ts)) =
   2.108            Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
   2.109 -      | norm (PThm ({serial = i, pos = p, name = a, prop = t, types = Ts}, thm_body)) =
   2.110 -          PThm (thm_header i p a t (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
   2.111 +      | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
   2.112 +          PThm (thm_header i p theory_name a t
   2.113 +            (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
   2.114        | norm _ = raise Same.SAME;
   2.115    in Same.commit norm end;
   2.116  
   2.117 @@ -1016,9 +1021,9 @@
   2.118            OfClass (Logic.incr_tvar_same inc T, c)
   2.119        | lift' _ _ (Oracle (s, prop, Ts)) =
   2.120            Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
   2.121 -      | lift' _ _ (PThm ({serial = i, pos = p, name = s, prop, types = Ts}, thm_body)) =
   2.122 -          PThm (thm_header i p s prop ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts),
   2.123 -            thm_body)
   2.124 +      | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
   2.125 +          PThm (thm_header i p theory_name s prop
   2.126 +            ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
   2.127        | lift' _ _ _ = raise Same.SAME
   2.128      and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
   2.129  
   2.130 @@ -1447,8 +1452,8 @@
   2.131        | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
   2.132        | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
   2.133        | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
   2.134 -      | subst _ _ (PThm ({serial = i, pos = p, name = id, prop, types}, thm_body)) =
   2.135 -          PThm (thm_header i p id prop (Same.map_option substTs types), thm_body)
   2.136 +      | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
   2.137 +          PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
   2.138        | subst _ _ _ = raise Same.SAME;
   2.139    in fn t => subst 0 0 t handle Same.SAME => t end;
   2.140  
   2.141 @@ -2189,7 +2194,8 @@
   2.142  
   2.143      val pthm = (i, make_thm_node name prop1 body');
   2.144  
   2.145 -    val header = thm_header i ([pos, Position.thread_data ()]) name prop1 NONE;
   2.146 +    val header =
   2.147 +      thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
   2.148      val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
   2.149      val head = PThm (header, thm_body);
   2.150      val proof =
     3.1 --- a/src/Pure/term.scala	Thu Aug 15 16:38:55 2019 +0200
     3.2 +++ b/src/Pure/term.scala	Thu Aug 15 16:57:09 2019 +0200
     3.3 @@ -58,7 +58,8 @@
     3.4    case class PAxm(name: String, types: List[Typ]) extends Proof
     3.5    case class OfClass(typ: Typ, cls: String) extends Proof
     3.6    case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof
     3.7 -  case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof
     3.8 +  case class PThm(serial: Long, theory_name: String, pseudo_name: String, types: List[Typ])
     3.9 +    extends Proof
    3.10  
    3.11  
    3.12    /* Pure logic */
    3.13 @@ -184,8 +185,8 @@
    3.14                case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls)))
    3.15                case Oracle(name, prop, types) =>
    3.16                  store(Oracle(cache_string(name), cache_term(prop), cache_typs(types)))
    3.17 -              case PThm(serial, name, types) =>
    3.18 -                store(PThm(serial, cache_string(name), cache_typs(types)))
    3.19 +              case PThm(serial, theory_name, name, types) =>
    3.20 +                store(PThm(serial, cache_string(theory_name), cache_string(name), cache_typs(types)))
    3.21              }
    3.22          }
    3.23        }
     4.1 --- a/src/Pure/term_xml.scala	Thu Aug 15 16:38:55 2019 +0200
     4.2 +++ b/src/Pure/term_xml.scala	Thu Aug 15 16:57:09 2019 +0200
     4.3 @@ -66,6 +66,6 @@
     4.4          { case (List(a), b) => PAxm(a, list(typ)(b)) },
     4.5          { case (List(a), b) => OfClass(typ(b), a) },
     4.6          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
     4.7 -        { case (List(a, b), c) => PThm(long_atom(a), b, list(typ)(c)) }))
     4.8 +        { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
     4.9    }
    4.10  }