src/Pure/proofterm.ML
author wenzelm
Thu Aug 15 19:35:17 2019 +0200 (4 weeks ago)
changeset 70540 04ef5ee3dd4d
parent 70538 fc9ba6fe367f
child 70541 f3fbc7f3559d
permissions -rw-r--r--
more careful treatment of standard_vars: rename apart from existing frees and avoid approximative Name.declared, proper application of unvarifyT within terms of proof;
     1 (*  Title:      Pure/proofterm.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 LF style proof terms.
     5 *)
     6 
     7 infix 8 % %% %>;
     8 
     9 signature BASIC_PROOFTERM =
    10 sig
    11   type thm_node
    12   type proof_serial = int
    13   type thm_header =
    14     {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
    15       prop: term, types: typ list option}
    16   type thm_body
    17   datatype proof =
    18      MinProof
    19    | PBound of int
    20    | Abst of string * typ option * proof
    21    | AbsP of string * term option * proof
    22    | % of proof * term option
    23    | %% of proof * proof
    24    | Hyp of term
    25    | PAxm of string * term * typ list option
    26    | OfClass of typ * class
    27    | Oracle of string * term * typ list option
    28    | PThm of thm_header * thm_body
    29   and proof_body = PBody of
    30     {oracles: (string * term) Ord_List.T,
    31      thms: (proof_serial * thm_node) Ord_List.T,
    32      proof: proof}
    33   val %> : proof * term -> proof
    34 end;
    35 
    36 signature PROOFTERM =
    37 sig
    38   include BASIC_PROOFTERM
    39   val proofs: int Unsynchronized.ref
    40   type pthm = proof_serial * thm_node
    41   type oracle = string * term
    42   val proof_of: proof_body -> proof
    43   val map_proof_of: (proof -> proof) -> proof_body -> proof_body
    44   val thm_header: proof_serial -> Position.T list -> string -> string -> term -> typ list option ->
    45     thm_header
    46   val thm_body: proof_body -> thm_body
    47   val thm_body_proof_raw: thm_body -> proof
    48   val thm_body_proof_open: thm_body -> proof
    49   val thm_node_name: thm_node -> string
    50   val thm_node_prop: thm_node -> term
    51   val thm_node_body: thm_node -> proof_body future
    52   val join_proof: proof_body future -> proof
    53   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    54   val fold_body_thms:
    55     ({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
    56     proof_body list -> 'a -> 'a
    57   val consolidate: proof_body list -> unit
    58   val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    59 
    60   val oracle_ord: oracle * oracle -> order
    61   val thm_ord: pthm * pthm -> order
    62   val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
    63   val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
    64   val all_oracles_of: proof_body -> oracle Ord_List.T
    65   val approximate_proof_body: proof -> proof_body
    66   val no_proof_body: proof -> proof_body
    67   val no_thm_proofs: proof -> proof
    68   val no_body_proofs: proof -> proof
    69 
    70   val encode: proof XML.Encode.T
    71   val encode_body: proof_body XML.Encode.T
    72   val encode_full: proof XML.Encode.T
    73   val decode: proof XML.Decode.T
    74   val decode_body: proof_body XML.Decode.T
    75 
    76   (*primitive operations*)
    77   val proofs_enabled: unit -> bool
    78   val atomic_proof: proof -> bool
    79   val compact_proof: proof -> bool
    80   val proof_combt: proof * term list -> proof
    81   val proof_combt': proof * term option list -> proof
    82   val proof_combP: proof * proof list -> proof
    83   val strip_combt: proof -> proof * term option list
    84   val strip_combP: proof -> proof * proof list
    85   val strip_thm: proof_body -> proof_body
    86   val map_proof_same: term Same.operation -> typ Same.operation
    87     -> (typ * class -> proof) -> proof Same.operation
    88   val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
    89   val map_proof_types_same: typ Same.operation -> proof Same.operation
    90   val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
    91   val map_proof_types: (typ -> typ) -> proof -> proof
    92   val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
    93   val maxidx_proof: proof -> int -> int
    94   val size_of_proof: proof -> int
    95   val change_types: typ list option -> proof -> proof
    96   val prf_abstract_over: term -> proof -> proof
    97   val prf_incr_bv: int -> int -> int -> int -> proof -> proof
    98   val incr_pboundvars: int -> int -> proof -> proof
    99   val prf_loose_bvar1: proof -> int -> bool
   100   val prf_loose_Pbvar1: proof -> int -> bool
   101   val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list
   102   val norm_proof: Envir.env -> proof -> proof
   103   val norm_proof': Envir.env -> proof -> proof
   104   val prf_subst_bounds: term list -> proof -> proof
   105   val prf_subst_pbounds: proof list -> proof -> proof
   106   val freeze_thaw_prf: proof -> proof * (proof -> proof)
   107   val proofT: typ
   108   val term_of_proof: proof -> term
   109 
   110   (*proof terms for specific inference rules*)
   111   val implies_intr_proof: term -> proof -> proof
   112   val implies_intr_proof': term -> proof -> proof
   113   val forall_intr_proof: term -> string -> proof -> proof
   114   val forall_intr_proof': term -> proof -> proof
   115   val varify_proof: term -> (string * sort) list -> proof -> proof
   116   val legacy_freezeT: term -> proof -> proof
   117   val rotate_proof: term list -> term -> int -> proof -> proof
   118   val permute_prems_proof: term list -> int -> int -> proof -> proof
   119   val generalize: string list * string list -> int -> proof -> proof
   120   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
   121     -> proof -> proof
   122   val lift_proof: term -> int -> term -> proof -> proof
   123   val incr_indexes: int -> proof -> proof
   124   val assumption_proof: term list -> term -> int -> proof -> proof
   125   val bicompose_proof: bool -> term list -> term list -> term list -> term option ->
   126     int -> int -> proof -> proof -> proof
   127   val equality_axms: (string * term) list
   128   val reflexive_axm: proof
   129   val symmetric_axm: proof
   130   val transitive_axm: proof
   131   val equal_intr_axm: proof
   132   val equal_elim_axm: proof
   133   val abstract_rule_axm: proof
   134   val combination_axm: proof
   135   val reflexive: proof
   136   val symmetric: proof -> proof
   137   val transitive: term -> typ -> proof -> proof -> proof
   138   val abstract_rule: term -> string -> proof -> proof
   139   val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof
   140   val equal_intr: term -> term -> proof -> proof -> proof
   141   val equal_elim: term -> term -> proof -> proof -> proof
   142   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
   143     sort list -> proof -> proof
   144   val of_sort_proof: Sorts.algebra ->
   145     (class * class -> proof) ->
   146     (string * class list list * class -> proof) ->
   147     (typ * class -> proof) -> typ * sort -> proof list
   148   val axm_proof: string -> term -> proof
   149   val oracle_proof: string -> term -> oracle * proof
   150   val shrink_proof: proof -> proof
   151 
   152   (*rewriting on proof terms*)
   153   val add_prf_rrule: proof * proof -> theory -> theory
   154   val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
   155   val no_skel: proof
   156   val normal_skel: proof
   157   val rewrite_proof: theory -> (proof * proof) list *
   158     (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   159   val rewrite_proof_notypes: (proof * proof) list *
   160     (typ list -> term option list -> proof -> (proof * proof) option) list -> proof -> proof
   161   val rew_proof: theory -> proof -> proof
   162 
   163   val reconstruct_proof: theory -> term -> proof -> proof
   164   val prop_of': term list -> proof -> term
   165   val prop_of: proof -> term
   166   val expand_proof: theory -> (string * term option) list -> proof -> proof
   167 
   168   val standard_vars: Name.context -> term list * proof list -> term list * proof list
   169   val standard_vars_term: Name.context -> term -> term
   170   val standard_vars_proof: Name.context -> proof -> proof
   171 
   172   val proof_serial: unit -> proof_serial
   173   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   174   val thm_proof: theory -> (class * class -> proof) ->
   175     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
   176     term list -> term -> (serial * proof_body future) list -> proof_body -> pthm * proof
   177   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
   178     (string * class list list * class -> proof) -> sort list -> term ->
   179     (serial * proof_body future) list -> proof_body -> pthm * proof
   180   val get_name: sort list -> term list -> term -> proof -> string
   181 end
   182 
   183 structure Proofterm : PROOFTERM =
   184 struct
   185 
   186 (** datatype proof **)
   187 
   188 type proof_serial = int;
   189 
   190 type thm_header =
   191   {serial: proof_serial, pos: Position.T list, theory_name: string, name: string,
   192     prop: term, types: typ list option};
   193 
   194 datatype proof =
   195    MinProof
   196  | PBound of int
   197  | Abst of string * typ option * proof
   198  | AbsP of string * term option * proof
   199  | op % of proof * term option
   200  | op %% of proof * proof
   201  | Hyp of term
   202  | PAxm of string * term * typ list option
   203  | OfClass of typ * class
   204  | Oracle of string * term * typ list option
   205  | PThm of thm_header * thm_body
   206 and proof_body = PBody of
   207   {oracles: (string * term) Ord_List.T,
   208    thms: (proof_serial * thm_node) Ord_List.T,
   209    proof: proof}
   210 and thm_body =
   211   Thm_Body of {export_proof: unit lazy, open_proof: proof -> proof, body: proof_body future}
   212 and thm_node =
   213   Thm_Node of {name: string, prop: term, body: proof_body future, consolidate: unit lazy};
   214 
   215 type oracle = string * term;
   216 type pthm = proof_serial * thm_node;
   217 
   218 fun proof_of (PBody {proof, ...}) = proof;
   219 val join_proof = Future.join #> proof_of;
   220 
   221 fun map_proof_of f (PBody {oracles, thms, proof}) =
   222   PBody {oracles = oracles, thms = thms, proof = f proof};
   223 
   224 fun thm_header serial pos theory_name name prop types : thm_header =
   225   {serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
   226 
   227 val no_export_proof = Lazy.value ();
   228 
   229 fun thm_body body =
   230   Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body};
   231 fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof;
   232 fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body;
   233 fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body);
   234 
   235 fun rep_thm_node (Thm_Node args) = args;
   236 val thm_node_name = #name o rep_thm_node;
   237 val thm_node_prop = #prop o rep_thm_node;
   238 val thm_node_body = #body o rep_thm_node;
   239 val thm_node_consolidate = #consolidate o rep_thm_node;
   240 
   241 fun join_thms (thms: pthm list) =
   242   Future.joins (map (thm_node_body o #2) thms);
   243 
   244 val consolidate =
   245   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   246   #> Lazy.consolidate #> map Lazy.force #> ignore;
   247 
   248 fun make_thm_node name prop body =
   249   Thm_Node {name = name, prop = prop, body = body,
   250     consolidate =
   251       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>
   252         let val PBody {thms, ...} = Future.join body
   253         in consolidate (join_thms thms) end)};
   254 
   255 
   256 (* proof atoms *)
   257 
   258 fun fold_proof_atoms all f =
   259   let
   260     fun app (Abst (_, _, prf)) = app prf
   261       | app (AbsP (_, _, prf)) = app prf
   262       | app (prf % _) = app prf
   263       | app (prf1 %% prf2) = app prf1 #> app prf2
   264       | app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) =>
   265           if Inttab.defined seen i then (x, seen)
   266           else
   267             let val (x', seen') =
   268               (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
   269             in (f prf x', seen') end)
   270       | app prf = (fn (x, seen) => (f prf x, seen));
   271   in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
   272 
   273 fun fold_body_thms f =
   274   let
   275     fun app (PBody {thms, ...}) =
   276       tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
   277         if Inttab.defined seen i then (x, seen)
   278         else
   279           let
   280             val name = thm_node_name thm_node;
   281             val prop = thm_node_prop thm_node;
   282             val body = Future.join (thm_node_body thm_node);
   283             val (x', seen') = app body (x, Inttab.update (i, ()) seen);
   284           in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
   285   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
   286 
   287 fun peek_status bodies =
   288   let
   289     fun status (PBody {oracles, thms, ...}) x =
   290       let
   291         val ((oracle, unfinished, failed), seen) =
   292           (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
   293             if Inttab.defined seen i then (st, seen)
   294             else
   295               let val seen' = Inttab.update (i, ()) seen in
   296                 (case Future.peek (thm_node_body thm_node) of
   297                   SOME (Exn.Res body') => status body' (st, seen')
   298                 | SOME (Exn.Exn _) =>
   299                     let val (oracle, unfinished, _) = st
   300                     in ((oracle, unfinished, true), seen') end
   301                 | NONE =>
   302                     let val (oracle, _, failed) = st
   303                     in ((oracle, true, failed), seen') end)
   304               end);
   305       in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
   306     val (oracle, unfinished, failed) =
   307       #1 (fold status bodies ((false, false, false), Inttab.empty));
   308   in {oracle = oracle, unfinished = unfinished, failed = failed} end;
   309 
   310 
   311 (* proof body *)
   312 
   313 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
   314 fun thm_ord ((i, _): pthm, (j, _): pthm) = int_ord (j, i);
   315 
   316 val unions_oracles = Ord_List.unions oracle_ord;
   317 val unions_thms = Ord_List.unions thm_ord;
   318 
   319 val all_oracles_of =
   320   let
   321     fun collect (PBody {oracles, thms, ...}) =
   322       (if null oracles then I else apfst (cons oracles)) #>
   323       (tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
   324         if Inttab.defined seen i then (x, seen)
   325         else
   326           let val body = Future.join (thm_node_body thm_node)
   327           in collect body (x, Inttab.update (i, ()) seen) end));
   328   in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
   329 
   330 fun approximate_proof_body prf =
   331   let
   332     val (oracles, thms) = fold_proof_atoms false
   333       (fn Oracle (s, prop, _) => apfst (cons (s, prop))
   334         | PThm ({serial = i, name, prop, ...}, Thm_Body {body, ...}) =>
   335             apsnd (cons (i, make_thm_node name prop body))
   336         | _ => I) [prf] ([], []);
   337   in
   338     PBody
   339      {oracles = Ord_List.make oracle_ord oracles,
   340       thms = Ord_List.make thm_ord thms,
   341       proof = prf}
   342   end;
   343 
   344 fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
   345 val no_thm_body = thm_body (no_proof_body MinProof);
   346 
   347 fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
   348   | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf)
   349   | no_thm_proofs (prf % t) = no_thm_proofs prf % t
   350   | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2
   351   | no_thm_proofs (PThm (header, _)) = PThm (header, no_thm_body)
   352   | no_thm_proofs a = a;
   353 
   354 fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf)
   355   | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf)
   356   | no_body_proofs (prf % t) = no_body_proofs prf % t
   357   | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
   358   | no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) =
   359       let
   360         val body' = Future.value (no_proof_body (join_proof body));
   361         val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
   362       in PThm (header, thm_body') end
   363   | no_body_proofs a = a;
   364 
   365 
   366 
   367 (** XML data representation **)
   368 
   369 (* encode *)
   370 
   371 local
   372 
   373 open XML.Encode Term_XML.Encode;
   374 
   375 fun proof prf = prf |> variant
   376  [fn MinProof => ([], []),
   377   fn PBound a => ([int_atom a], []),
   378   fn Abst (a, b, c) => ([a], pair (option typ) proof (b, c)),
   379   fn AbsP (a, b, c) => ([a], pair (option term) proof (b, c)),
   380   fn a % b => ([], pair proof (option term) (a, b)),
   381   fn a %% b => ([], pair proof proof (a, b)),
   382   fn Hyp a => ([], term a),
   383   fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
   384   fn OfClass (a, b) => ([b], typ a),
   385   fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
   386   fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
   387     ([int_atom serial, theory_name, name],
   388       pair (list properties) (pair term (pair (option (list typ)) proof_body))
   389         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
   390 and proof_body (PBody {oracles, thms, proof = prf}) =
   391   triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
   392 and pthm (a, thm_node) =
   393   pair int (triple string term proof_body)
   394     (a, (thm_node_name thm_node, thm_node_prop thm_node, Future.join (thm_node_body thm_node)));
   395 
   396 fun full_proof prf = prf |> variant
   397  [fn MinProof => ([], []),
   398   fn PBound a => ([int_atom a], []),
   399   fn Abst (a, SOME b, c) => ([a], pair typ full_proof (b, c)),
   400   fn AbsP (a, SOME b, c) => ([a], pair term full_proof (b, c)),
   401   fn a % SOME b => ([], pair full_proof term (a, b)),
   402   fn a %% b => ([], pair full_proof full_proof (a, b)),
   403   fn Hyp a => ([], term a),
   404   fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
   405   fn OfClass (T, c) => ([c], typ T),
   406   fn Oracle (name, prop, SOME Ts) => ([name], pair term (list typ) (prop, Ts)),
   407   fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) =>
   408     ([int_atom serial, theory_name, name], list typ Ts)];
   409 
   410 in
   411 
   412 val encode = proof;
   413 val encode_body = proof_body;
   414 val encode_full = full_proof;
   415 
   416 end;
   417 
   418 
   419 (* decode *)
   420 
   421 local
   422 
   423 open XML.Decode Term_XML.Decode;
   424 
   425 fun proof prf = prf |> variant
   426  [fn ([], []) => MinProof,
   427   fn ([a], []) => PBound (int_atom a),
   428   fn ([a], b) => let val (c, d) = pair (option typ) proof b in Abst (a, c, d) end,
   429   fn ([a], b) => let val (c, d) = pair (option term) proof b in AbsP (a, c, d) end,
   430   fn ([], a) => op % (pair proof (option term) a),
   431   fn ([], a) => op %% (pair proof proof a),
   432   fn ([], a) => Hyp (term a),
   433   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
   434   fn ([b], a) => OfClass (typ a, b),
   435   fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
   436   fn ([a, b, c], d) =>
   437     let
   438       val ((e, (f, (g, h)))) =
   439         pair (list properties) (pair term (pair (option (list typ)) proof_body)) d;
   440       val header = thm_header (int_atom a) (map Position.of_properties e) b c f g;
   441     in PThm (header, thm_body h) end]
   442 and proof_body x =
   443   let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
   444   in PBody {oracles = a, thms = b, proof = c} end
   445 and pthm x =
   446   let val (a, (b, c, d)) = pair int (triple string term proof_body) x
   447   in (a, make_thm_node b c (Future.value d)) end;
   448 
   449 in
   450 
   451 val decode = proof;
   452 val decode_body = proof_body;
   453 
   454 end;
   455 
   456 
   457 (** proof objects with different levels of detail **)
   458 
   459 fun atomic_proof prf =
   460   (case prf of
   461     Abst _ => false
   462   | AbsP _ => false
   463   | op % _ => false
   464   | op %% _ => false
   465   | MinProof => false
   466   | _ => true);
   467 
   468 fun compact_proof (prf % _) = compact_proof prf
   469   | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1
   470   | compact_proof prf = atomic_proof prf;
   471 
   472 fun (prf %> t) = prf % SOME t;
   473 
   474 val proof_combt = Library.foldl (op %>);
   475 val proof_combt' = Library.foldl (op %);
   476 val proof_combP = Library.foldl (op %%);
   477 
   478 fun strip_combt prf =
   479     let fun stripc (prf % t, ts) = stripc (prf, t::ts)
   480           | stripc  x =  x
   481     in  stripc (prf, [])  end;
   482 
   483 fun strip_combP prf =
   484     let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
   485           | stripc  x =  x
   486     in  stripc (prf, [])  end;
   487 
   488 fun strip_thm (body as PBody {proof, ...}) =
   489   (case fst (strip_combt (fst (strip_combP proof))) of
   490     PThm (_, Thm_Body {body = body', ...}) => Future.join body'
   491   | _ => body);
   492 
   493 val mk_Abst = fold_rev (fn (s, _: typ) => fn prf => Abst (s, NONE, prf));
   494 fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
   495 
   496 fun map_proof_same term typ ofclass =
   497   let
   498     val typs = Same.map typ;
   499 
   500     fun proof (Abst (s, T, prf)) =
   501           (Abst (s, Same.map_option typ T, Same.commit proof prf)
   502             handle Same.SAME => Abst (s, T, proof prf))
   503       | proof (AbsP (s, t, prf)) =
   504           (AbsP (s, Same.map_option term t, Same.commit proof prf)
   505             handle Same.SAME => AbsP (s, t, proof prf))
   506       | proof (prf % t) =
   507           (proof prf % Same.commit (Same.map_option term) t
   508             handle Same.SAME => prf % Same.map_option term t)
   509       | proof (prf1 %% prf2) =
   510           (proof prf1 %% Same.commit proof prf2
   511             handle Same.SAME => prf1 %% proof prf2)
   512       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
   513       | proof (OfClass T_c) = ofclass T_c
   514       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
   515       | proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) =
   516           PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body)
   517       | proof _ = raise Same.SAME;
   518   in proof end;
   519 
   520 fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
   521 fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
   522 
   523 fun same eq f x =
   524   let val x' = f x
   525   in if eq (x, x') then raise Same.SAME else x' end;
   526 
   527 fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
   528 fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
   529 
   530 fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
   531   | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
   532   | fold_proof_terms f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f g prf
   533   | fold_proof_terms f g (AbsP (_, NONE, prf)) = fold_proof_terms f g prf
   534   | fold_proof_terms f g (prf % SOME t) = fold_proof_terms f g prf #> f t
   535   | fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf
   536   | fold_proof_terms f g (prf1 %% prf2) =
   537       fold_proof_terms f g prf1 #> fold_proof_terms f g prf2
   538   | fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts
   539   | fold_proof_terms _ g (OfClass (T, _)) = g T
   540   | fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts
   541   | fold_proof_terms _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts
   542   | fold_proof_terms _ _ _ = I;
   543 
   544 fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf;
   545 
   546 fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
   547   | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf
   548   | size_of_proof (prf % _) = 1 + size_of_proof prf
   549   | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
   550   | size_of_proof _ = 1;
   551 
   552 fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
   553   | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
   554   | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
   555   | change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) =
   556       PThm (thm_header serial pos theory_name name prop types, thm_body)
   557   | change_types _ prf = prf;
   558 
   559 
   560 (* utilities *)
   561 
   562 fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t
   563   | strip_abs _ t = t;
   564 
   565 fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts);
   566 
   567 
   568 (*Abstraction of a proof term over its occurrences of v,
   569     which must contain no loose bound variables.
   570   The resulting proof term is ready to become the body of an Abst.*)
   571 
   572 fun prf_abstract_over v =
   573   let
   574     fun abst' lev u = if v aconv u then Bound lev else
   575       (case u of
   576          Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t)
   577        | f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t)
   578        | _ => raise Same.SAME)
   579     and absth' lev t = (abst' lev t handle Same.SAME => t);
   580 
   581     fun abst lev (AbsP (a, t, prf)) =
   582           (AbsP (a, Same.map_option (abst' lev) t, absth lev prf)
   583            handle Same.SAME => AbsP (a, t, abst lev prf))
   584       | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf)
   585       | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2
   586           handle Same.SAME => prf1 %% abst lev prf2)
   587       | abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t
   588           handle Same.SAME => prf % Same.map_option (abst' lev) t)
   589       | abst _ _ = raise Same.SAME
   590     and absth lev prf = (abst lev prf handle Same.SAME => prf);
   591 
   592   in absth 0 end;
   593 
   594 
   595 (*increments a proof term's non-local bound variables
   596   required when moving a proof term within abstractions
   597      inc is  increment for bound variables
   598      lev is  level at which a bound variable is considered 'loose'*)
   599 
   600 fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
   601 
   602 fun prf_incr_bv' incP _ Plev _ (PBound i) =
   603       if i >= Plev then PBound (i+incP) else raise Same.SAME
   604   | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
   605       (AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t,
   606          prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME =>
   607            AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
   608   | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
   609       Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
   610   | prf_incr_bv' incP inct Plev tlev (prf %% prf') =
   611       (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
   612        handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
   613   | prf_incr_bv' incP inct Plev tlev (prf % t) =
   614       (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
   615        handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t)
   616   | prf_incr_bv' _ _ _ _ _ = raise Same.SAME
   617 and prf_incr_bv incP inct Plev tlev prf =
   618       (prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf);
   619 
   620 fun incr_pboundvars  0 0 prf = prf
   621   | incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf;
   622 
   623 
   624 fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k
   625   | prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k)
   626   | prf_loose_bvar1 (_ % NONE) _ = true
   627   | prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k
   628   | prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true
   629   | prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1)
   630   | prf_loose_bvar1 _ _ = false;
   631 
   632 fun prf_loose_Pbvar1 (PBound i) k = i = k
   633   | prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k
   634   | prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k
   635   | prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1)
   636   | prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k
   637   | prf_loose_Pbvar1 _ _ = false;
   638 
   639 fun prf_add_loose_bnos plev _ (PBound i) (is, js) =
   640       if i < plev then (is, js) else (insert (op =) (i-plev) is, js)
   641   | prf_add_loose_bnos plev tlev (prf1 %% prf2) p =
   642       prf_add_loose_bnos plev tlev prf2
   643         (prf_add_loose_bnos plev tlev prf1 p)
   644   | prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
   645       prf_add_loose_bnos plev tlev prf
   646         (case opt of
   647           NONE => (is, insert (op =) ~1 js)
   648         | SOME t => (is, add_loose_bnos (t, tlev, js)))
   649   | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
   650       prf_add_loose_bnos (plev+1) tlev prf
   651         (case opt of
   652           NONE => (is, insert (op =) ~1 js)
   653         | SOME t => (is, add_loose_bnos (t, tlev, js)))
   654   | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
   655       prf_add_loose_bnos plev (tlev+1) prf p
   656   | prf_add_loose_bnos _ _ _ _ = ([], []);
   657 
   658 
   659 (* substitutions *)
   660 
   661 fun del_conflicting_tvars envT T = Term_Subst.instantiateT
   662   (map_filter (fn ixnS as (_, S) =>
   663      (Type.lookup envT ixnS; NONE) handle TYPE _ =>
   664         SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T;
   665 
   666 fun del_conflicting_vars env t = Term_Subst.instantiate
   667   (map_filter (fn ixnS as (_, S) =>
   668      (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
   669         SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []),
   670    map_filter (fn (ixnT as (_, T)) =>
   671      (Envir.lookup env ixnT; NONE) handle TYPE _ =>
   672         SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
   673 
   674 fun norm_proof env =
   675   let
   676     val envT = Envir.type_env env;
   677     fun msg s = warning ("type conflict in norm_proof:\n" ^ s);
   678     fun htype f t = f env t handle TYPE (s, _, _) =>
   679       (msg s; f env (del_conflicting_vars env t));
   680     fun htypeT f T = f envT T handle TYPE (s, _, _) =>
   681       (msg s; f envT (del_conflicting_tvars envT T));
   682     fun htypeTs f Ts = f envT Ts handle TYPE (s, _, _) =>
   683       (msg s; f envT (map (del_conflicting_tvars envT) Ts));
   684 
   685     fun norm (Abst (s, T, prf)) =
   686           (Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf)
   687             handle Same.SAME => Abst (s, T, norm prf))
   688       | norm (AbsP (s, t, prf)) =
   689           (AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf)
   690             handle Same.SAME => AbsP (s, t, norm prf))
   691       | norm (prf % t) =
   692           (norm prf % Option.map (htype Envir.norm_term) t
   693             handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t)
   694       | norm (prf1 %% prf2) =
   695           (norm prf1 %% Same.commit norm prf2
   696             handle Same.SAME => prf1 %% norm prf2)
   697       | norm (PAxm (s, prop, Ts)) =
   698           PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
   699       | norm (OfClass (T, c)) =
   700           OfClass (htypeT Envir.norm_type_same T, c)
   701       | norm (Oracle (s, prop, Ts)) =
   702           Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts)
   703       | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
   704           PThm (thm_header i p theory_name a t
   705             (Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body)
   706       | norm _ = raise Same.SAME;
   707   in Same.commit norm end;
   708 
   709 
   710 (* remove some types in proof term (to save space) *)
   711 
   712 fun remove_types (Abs (s, _, t)) = Abs (s, dummyT, remove_types t)
   713   | remove_types (t $ u) = remove_types t $ remove_types u
   714   | remove_types (Const (s, _)) = Const (s, dummyT)
   715   | remove_types t = t;
   716 
   717 fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
   718   Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv};
   719 
   720 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
   721 
   722 
   723 (* substitution of bound variables *)
   724 
   725 fun prf_subst_bounds args prf =
   726   let
   727     val n = length args;
   728     fun subst' lev (Bound i) =
   729          (if i<lev then raise Same.SAME    (*var is locally bound*)
   730           else  incr_boundvars lev (nth args (i-lev))
   731                   handle General.Subscript => Bound (i-n))  (*loose: change it*)
   732       | subst' lev (Abs (a, T, body)) = Abs (a, T,  subst' (lev+1) body)
   733       | subst' lev (f $ t) = (subst' lev f $ substh' lev t
   734           handle Same.SAME => f $ subst' lev t)
   735       | subst' _ _ = raise Same.SAME
   736     and substh' lev t = (subst' lev t handle Same.SAME => t);
   737 
   738     fun subst lev (AbsP (a, t, body)) =
   739         (AbsP (a, Same.map_option (subst' lev) t, substh lev body)
   740           handle Same.SAME => AbsP (a, t, subst lev body))
   741       | subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body)
   742       | subst lev (prf %% prf') = (subst lev prf %% substh lev prf'
   743           handle Same.SAME => prf %% subst lev prf')
   744       | subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t
   745           handle Same.SAME => prf % Same.map_option (subst' lev) t)
   746       | subst _ _ = raise Same.SAME
   747     and substh lev prf = (subst lev prf handle Same.SAME => prf);
   748   in (case args of [] => prf | _ => substh 0 prf) end;
   749 
   750 fun prf_subst_pbounds args prf =
   751   let
   752     val n = length args;
   753     fun subst (PBound i) Plev tlev =
   754          (if i < Plev then raise Same.SAME    (*var is locally bound*)
   755           else incr_pboundvars Plev tlev (nth args (i-Plev))
   756                  handle General.Subscript => PBound (i-n)  (*loose: change it*))
   757       | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
   758       | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
   759       | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev
   760           handle Same.SAME => prf %% subst prf' Plev tlev)
   761       | subst (prf % t) Plev tlev = subst prf Plev tlev % t
   762       | subst  _ _ _ = raise Same.SAME
   763     and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
   764   in (case args of [] => prf | _ => substh prf 0 0) end;
   765 
   766 
   767 (* freezing and thawing of variables in proof terms *)
   768 
   769 local
   770 
   771 fun frzT names =
   772   map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S));
   773 
   774 fun thawT names =
   775   map_type_tfree (fn (a, S) =>
   776     (case AList.lookup (op =) names a of
   777       NONE => TFree (a, S)
   778     | SOME ixn => TVar (ixn, S)));
   779 
   780 fun freeze names names' (t $ u) =
   781       freeze names names' t $ freeze names names' u
   782   | freeze names names' (Abs (s, T, t)) =
   783       Abs (s, frzT names' T, freeze names names' t)
   784   | freeze _ names' (Const (s, T)) = Const (s, frzT names' T)
   785   | freeze _ names' (Free (s, T)) = Free (s, frzT names' T)
   786   | freeze names names' (Var (ixn, T)) =
   787       Free (the (AList.lookup (op =) names ixn), frzT names' T)
   788   | freeze _ _ t = t;
   789 
   790 fun thaw names names' (t $ u) =
   791       thaw names names' t $ thaw names names' u
   792   | thaw names names' (Abs (s, T, t)) =
   793       Abs (s, thawT names' T, thaw names names' t)
   794   | thaw _ names' (Const (s, T)) = Const (s, thawT names' T)
   795   | thaw names names' (Free (s, T)) =
   796       let val T' = thawT names' T in
   797         (case AList.lookup (op =) names s of
   798           NONE => Free (s, T')
   799         | SOME ixn => Var (ixn, T'))
   800       end
   801   | thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T)
   802   | thaw _ _ t = t;
   803 
   804 in
   805 
   806 fun freeze_thaw_prf prf =
   807   let
   808     val (fs, Tfs, vs, Tvs) = fold_proof_terms
   809       (fn t => fn (fs, Tfs, vs, Tvs) =>
   810          (Term.add_free_names t fs, Term.add_tfree_names t Tfs,
   811           Term.add_var_names t vs, Term.add_tvar_names t Tvs))
   812       (fn T => fn (fs, Tfs, vs, Tvs) =>
   813          (fs, Term.add_tfree_namesT T Tfs,
   814           vs, Term.add_tvar_namesT T Tvs))
   815       prf ([], [], [], []);
   816     val names = vs ~~ Name.variant_list fs (map fst vs);
   817     val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
   818     val rnames = map swap names;
   819     val rnames' = map swap names';
   820   in
   821     (map_proof_terms (freeze names names') (frzT names') prf,
   822      map_proof_terms (thaw rnames rnames') (thawT rnames'))
   823   end;
   824 
   825 end;
   826 
   827 
   828 
   829 (** proof terms as pure terms **)
   830 
   831 val proofT = Type ("Pure.proof", []);
   832 
   833 local
   834 
   835 val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
   836 val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
   837 val Hypt = Const ("Pure.Hyp", propT --> proofT);
   838 val Oraclet = Const ("Pure.Oracle", propT --> proofT);
   839 val MinProoft = Const ("Pure.MinProof", proofT);
   840 
   841 fun AppT T prf =
   842   Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
   843 
   844 fun OfClasst (T, c) =
   845   let val U = Term.itselfT T --> propT
   846   in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
   847 
   848 fun term_of _ (PThm ({name, types = Ts, ...}, _)) =
   849       fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT))
   850   | term_of _ (PAxm (name, _, Ts)) =
   851       fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
   852   | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
   853   | term_of _ (PBound i) = Bound i
   854   | term_of Ts (Abst (s, opT, prf)) =
   855       let val T = the_default dummyT opT in
   856         Const ("Pure.Abst", (T --> proofT) --> proofT) $
   857           Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
   858       end
   859   | term_of Ts (AbsP (s, t, prf)) =
   860       AbsPt $ the_default Term.dummy_prop t $
   861         Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   862   | term_of Ts (prf1 %% prf2) =
   863       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   864   | term_of Ts (prf % opt) =
   865       let
   866         val t = the_default Term.dummy opt;
   867         val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
   868       in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
   869   | term_of _ (Hyp t) = Hypt $ t
   870   | term_of _ (Oracle (_, t, _)) = Oraclet $ t
   871   | term_of _ MinProof = MinProoft;
   872 
   873 in
   874 
   875 val term_of_proof = term_of [];
   876 
   877 end;
   878 
   879 
   880 
   881 (** inference rules **)
   882 
   883 (* implication introduction *)
   884 
   885 fun gen_implies_intr_proof f h prf =
   886   let
   887     fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME
   888       | abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf)
   889       | abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf)
   890       | abshyp i (prf % t) = abshyp i prf % t
   891       | abshyp i (prf1 %% prf2) =
   892           (abshyp i prf1 %% abshyph i prf2
   893             handle Same.SAME => prf1 %% abshyp i prf2)
   894       | abshyp _ _ = raise Same.SAME
   895     and abshyph i prf = (abshyp i prf handle Same.SAME => prf);
   896   in
   897     AbsP ("H", f h, abshyph 0 prf)
   898   end;
   899 
   900 val implies_intr_proof = gen_implies_intr_proof (K NONE);
   901 val implies_intr_proof' = gen_implies_intr_proof SOME;
   902 
   903 
   904 (* forall introduction *)
   905 
   906 fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
   907 
   908 fun forall_intr_proof' t prf =
   909   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   910   in Abst (a, SOME T, prf_abstract_over t prf) end;
   911 
   912 
   913 (* varify *)
   914 
   915 fun varify_proof t fixed prf =
   916   let
   917     val fs = Term.fold_types (Term.fold_atyps
   918       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
   919     val used = Name.context
   920       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
   921     val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
   922     fun thaw (a, S) =
   923       (case AList.lookup (op =) fmap (a, S) of
   924         NONE => TFree (a, S)
   925       | SOME b => TVar ((b, 0), S));
   926   in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end;
   927 
   928 
   929 local
   930 
   931 fun new_name ix (pairs, used) =
   932   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
   933   in ((ix, v) :: pairs, v :: used) end;
   934 
   935 fun freeze_one alist (ix, sort) =
   936   (case AList.lookup (op =) alist ix of
   937     NONE => TVar (ix, sort)
   938   | SOME name => TFree (name, sort));
   939 
   940 in
   941 
   942 fun legacy_freezeT t prf =
   943   let
   944     val used = Term.add_tfree_names t [];
   945     val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used);
   946   in
   947     (case alist of
   948       [] => prf (*nothing to do!*)
   949     | _ =>
   950         let val frzT = map_type_tvar (freeze_one alist)
   951         in map_proof_terms (map_types frzT) frzT prf end)
   952   end;
   953 
   954 end;
   955 
   956 
   957 (* rotate assumptions *)
   958 
   959 fun rotate_proof Bs Bi m prf =
   960   let
   961     val params = Term.strip_all_vars Bi;
   962     val asms = Logic.strip_imp_prems (Term.strip_all_body Bi);
   963     val i = length asms;
   964     val j = length Bs;
   965   in
   966     mk_AbsP (j+1, proof_combP (prf, map PBound
   967       (j downto 1) @ [mk_Abst params (mk_AbsP (i,
   968         proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
   969           map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   970   end;
   971 
   972 
   973 (* permute premises *)
   974 
   975 fun permute_prems_proof prems j k prf =
   976   let val n = length prems
   977   in mk_AbsP (n, proof_combP (prf,
   978     map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
   979   end;
   980 
   981 
   982 (* generalization *)
   983 
   984 fun generalize (tfrees, frees) idx =
   985   Same.commit (map_proof_terms_same
   986     (Term_Subst.generalize_same (tfrees, frees) idx)
   987     (Term_Subst.generalizeT_same tfrees idx));
   988 
   989 
   990 (* instantiation *)
   991 
   992 fun instantiate (instT, inst) =
   993   Same.commit (map_proof_terms_same
   994     (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
   995     (Term_Subst.instantiateT_same instT));
   996 
   997 
   998 (* lifting *)
   999 
  1000 fun lift_proof Bi inc prop prf =
  1001   let
  1002     fun lift'' Us Ts t =
  1003       strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
  1004 
  1005     fun lift' Us Ts (Abst (s, T, prf)) =
  1006           (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
  1007            handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
  1008       | lift' Us Ts (AbsP (s, t, prf)) =
  1009           (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
  1010            handle Same.SAME => AbsP (s, t, lift' Us Ts prf))
  1011       | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
  1012           handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t)
  1013       | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
  1014           handle Same.SAME => prf1 %% lift' Us Ts prf2)
  1015       | lift' _ _ (PAxm (s, prop, Ts)) =
  1016           PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
  1017       | lift' _ _ (OfClass (T, c)) =
  1018           OfClass (Logic.incr_tvar_same inc T, c)
  1019       | lift' _ _ (Oracle (s, prop, Ts)) =
  1020           Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
  1021       | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
  1022           PThm (thm_header i p theory_name s prop
  1023             ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
  1024       | lift' _ _ _ = raise Same.SAME
  1025     and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
  1026 
  1027     val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
  1028     val k = length ps;
  1029 
  1030     fun mk_app b (i, j, prf) =
  1031           if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
  1032 
  1033     fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
  1034             AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
  1035       | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
  1036             Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
  1037       | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
  1038             map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
  1039               (i + k - 1 downto i));
  1040   in
  1041     mk_AbsP (k, lift [] [] 0 0 Bi)
  1042   end;
  1043 
  1044 fun incr_indexes i =
  1045   Same.commit (map_proof_terms_same
  1046     (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
  1047 
  1048 
  1049 (* proof by assumption *)
  1050 
  1051 fun mk_asm_prf t i m =
  1052   let
  1053     fun imp_prf _ i 0 = PBound i
  1054       | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
  1055       | imp_prf _ i _ = PBound i;
  1056     fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
  1057       | all_prf t = imp_prf t (~i) m
  1058   in all_prf t end;
  1059 
  1060 fun assumption_proof Bs Bi n prf =
  1061   mk_AbsP (length Bs, proof_combP (prf,
  1062     map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
  1063 
  1064 
  1065 (* composition of object rule with proof state *)
  1066 
  1067 fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
  1068       AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
  1069   | flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) =
  1070       Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k))
  1071   | flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i),
  1072       map Bound (j-1 downto 0)), map PBound (remove (op =) (i-n) (i-1 downto 0)));
  1073 
  1074 fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf =
  1075   let
  1076     val la = length newAs;
  1077     val lb = length Bs;
  1078   in
  1079     mk_AbsP (lb+la, proof_combP (sprf,
  1080       map PBound (lb + la - 1 downto la)) %%
  1081         proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @
  1082           map (if flatten then flatten_params_proof 0 0 n else PBound o snd)
  1083             (oldAs ~~ (la - 1 downto 0))))
  1084   end;
  1085 
  1086 
  1087 
  1088 (** type classes **)
  1089 
  1090 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
  1091   let
  1092     fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE;
  1093     val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts;
  1094     val replacements = present @ extra @ witnessed;
  1095     fun replace T =
  1096       if exists (fn (T', _) => T' = T) present then raise Same.SAME
  1097       else
  1098         (case get_first (get (Type.sort_of_atyp T)) replacements of
  1099           SOME T' => T'
  1100         | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term");
  1101   in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
  1102 
  1103 fun of_sort_proof algebra classrel_proof arity_proof hyps =
  1104   Sorts.of_sort_derivation algebra
  1105    {class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 =>
  1106       if c1 = c2 then prf else classrel_proof (c1, c2) %% prf,
  1107     type_constructor = fn (a, _) => fn dom => fn c =>
  1108       let val Ss = map (map snd) dom and prfs = maps (map fst) dom
  1109       in proof_combP (arity_proof (a, Ss, c), prfs) end,
  1110     type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
  1111 
  1112 
  1113 
  1114 (** axioms and theorems **)
  1115 
  1116 val proofs = Unsynchronized.ref 2;
  1117 fun proofs_enabled () = ! proofs >= 2;
  1118 
  1119 fun vars_of t = map Var (rev (Term.add_vars t []));
  1120 fun frees_of t = map Free (rev (Term.add_frees t []));
  1121 
  1122 fun test_args _ [] = true
  1123   | test_args is (Bound i :: ts) =
  1124       not (member (op =) is i) andalso test_args (i :: is) ts
  1125   | test_args _ _ = false;
  1126 
  1127 fun is_fun (Type ("fun", _)) = true
  1128   | is_fun (TVar _) = true
  1129   | is_fun _ = false;
  1130 
  1131 fun add_funvars Ts (vs, t) =
  1132   if is_fun (fastype_of1 (Ts, t)) then
  1133     union (op =) vs (map_filter (fn Var (ixn, T) =>
  1134       if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
  1135   else vs;
  1136 
  1137 fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) =
  1138       add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u)
  1139   | add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) =
  1140       add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
  1141   | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
  1142   | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
  1143 and add_npvars' Ts (vs, t) =
  1144   (case strip_comb t of
  1145     (Var (ixn, _), ts) => if test_args [] ts then vs
  1146       else Library.foldl (add_npvars' Ts)
  1147         (AList.update (op =) (ixn,
  1148           Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts)
  1149   | (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
  1150   | (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
  1151 
  1152 fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
  1153   | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
  1154   | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []);
  1155 
  1156 fun is_proj t =
  1157   let
  1158     fun is_p i t =
  1159       (case strip_comb t of
  1160         (Bound _, []) => false
  1161       | (Bound j, ts) => j >= i orelse exists (is_p i) ts
  1162       | (Abs (_, _, u), _) => is_p (i+1) u
  1163       | (_, ts) => exists (is_p i) ts)
  1164   in
  1165     (case strip_abs_body t of
  1166       Bound _ => true
  1167     | t' => is_p 0 t')
  1168   end;
  1169 
  1170 fun prop_args prop =
  1171   let
  1172     val needed_vars =
  1173       union (op =) (Library.foldl (uncurry (union (op =)))
  1174         ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))))
  1175       (prop_vars prop);
  1176     val vars =
  1177       vars_of prop |> map (fn (v as Var (ixn, _)) =>
  1178         if member (op =) needed_vars ixn then SOME v else NONE);
  1179     val frees = map SOME (frees_of prop);
  1180   in vars @ frees end;
  1181 
  1182 fun gen_axm_proof c name prop =
  1183   proof_combt' (c (name, prop, NONE), prop_args prop);
  1184 
  1185 val axm_proof = gen_axm_proof PAxm;
  1186 
  1187 fun oracle_proof name prop =
  1188   if ! proofs = 0 then ((name, Term.dummy), Oracle (name, Term.dummy, NONE))
  1189   else ((name, prop), gen_axm_proof Oracle name prop);
  1190 
  1191 val shrink_proof =
  1192   let
  1193     fun shrink ls lev (prf as Abst (a, T, body)) =
  1194           let val (b, is, ch, body') = shrink ls (lev+1) body
  1195           in (b, is, ch, if ch then Abst (a, T, body') else prf) end
  1196       | shrink ls lev (prf as AbsP (a, t, body)) =
  1197           let val (b, is, ch, body') = shrink (lev::ls) lev body
  1198           in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
  1199             ch, if ch then AbsP (a, t, body') else prf)
  1200           end
  1201       | shrink ls lev prf =
  1202           let val (is, ch, _, prf') = shrink' ls lev [] [] prf
  1203           in (false, is, ch, prf') end
  1204     and shrink' ls lev ts prfs (prf as prf1 %% prf2) =
  1205           let
  1206             val p as (_, is', ch', prf') = shrink ls lev prf2;
  1207             val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
  1208           in (union (op =) is is', ch orelse ch', ts',
  1209               if ch orelse ch' then prf'' %% prf' else prf)
  1210           end
  1211       | shrink' ls lev ts prfs (prf as prf1 % t) =
  1212           let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
  1213           in (is, ch orelse ch', ts',
  1214               if ch orelse ch' then prf' % t' else prf) end
  1215       | shrink' ls lev ts prfs (prf as PBound i) =
  1216           (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
  1217              orelse has_duplicates (op =)
  1218                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
  1219              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
  1220       | shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t)
  1221       | shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf)
  1222       | shrink' _ _ ts _ (prf as OfClass _) = ([], false, map (pair false) ts, prf)
  1223       | shrink' _ _ ts prfs prf =
  1224           let
  1225             val prop =
  1226               (case prf of
  1227                 PAxm (_, prop, _) => prop
  1228               | Oracle (_, prop, _) => prop
  1229               | PThm ({prop, ...}, _) => prop
  1230               | _ => raise Fail "shrink: proof not in normal form");
  1231             val vs = vars_of prop;
  1232             val (ts', ts'') = chop (length vs) ts;
  1233             val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
  1234             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
  1235               insert (op =) ixn
  1236                 (case AList.lookup (op =) insts ixn of
  1237                   SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
  1238                 | _ => union (op =) ixns ixns'))
  1239                   (needed prop ts'' prfs, add_npvars false true [] ([], prop));
  1240             val insts' = map
  1241               (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
  1242                 | (_, x) => (false, x)) insts
  1243           in ([], false, insts' @ map (pair false) ts'', prf) end
  1244     and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) =
  1245           union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
  1246       | needed (Var (ixn, _)) (_::_) _ = [ixn]
  1247       | needed _ _ _ = [];
  1248   in fn prf => #4 (shrink [] 0 prf) end;
  1249 
  1250 
  1251 
  1252 (** axioms for equality **)
  1253 
  1254 val aT = TFree ("'a", []);
  1255 val bT = TFree ("'b", []);
  1256 val x = Free ("x", aT);
  1257 val y = Free ("y", aT);
  1258 val z = Free ("z", aT);
  1259 val A = Free ("A", propT);
  1260 val B = Free ("B", propT);
  1261 val f = Free ("f", aT --> bT);
  1262 val g = Free ("g", aT --> bT);
  1263 
  1264 val equality_axms =
  1265  [("reflexive", Logic.mk_equals (x, x)),
  1266   ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
  1267   ("transitive",
  1268     Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
  1269   ("equal_intr",
  1270     Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
  1271   ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
  1272   ("abstract_rule",
  1273     Logic.mk_implies
  1274       (Logic.all x
  1275         (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
  1276   ("combination", Logic.list_implies
  1277     ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
  1278 
  1279 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
  1280   equal_elim_axm, abstract_rule_axm, combination_axm] =
  1281     map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
  1282 
  1283 val reflexive = reflexive_axm % NONE;
  1284 
  1285 fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf
  1286   | symmetric prf = symmetric_axm % NONE % NONE %% prf;
  1287 
  1288 fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2
  1289   | transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1
  1290   | transitive u (Type ("prop", [])) prf1 prf2 =
  1291       transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2
  1292   | transitive _ _ prf1 prf2 = transitive_axm % NONE % NONE % NONE %% prf1 %% prf2;
  1293 
  1294 fun abstract_rule x a prf =
  1295   abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
  1296 
  1297 fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) =
  1298       is_some f orelse check_comb prf
  1299   | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
  1300       check_comb prf1 andalso check_comb prf2
  1301   | check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
  1302   | check_comb _ = false;
  1303 
  1304 fun combination f g t u (Type (_, [T, U])) prf1 prf2 =
  1305   let
  1306     val f = Envir.beta_norm f;
  1307     val g = Envir.beta_norm g;
  1308     val prf =
  1309       if check_comb prf1 then
  1310         combination_axm % NONE % NONE
  1311       else
  1312         (case prf1 of
  1313           PAxm ("Pure.reflexive", _, _) % _ =>
  1314             combination_axm %> remove_types f % NONE
  1315         | _ => combination_axm %> remove_types f %> remove_types g)
  1316   in
  1317     (case T of
  1318       Type ("fun", _) => prf %
  1319         (case head_of f of
  1320           Abs _ => SOME (remove_types t)
  1321         | Var _ => SOME (remove_types t)
  1322         | _ => NONE) %
  1323         (case head_of g of
  1324           Abs _ => SOME (remove_types u)
  1325         | Var _ => SOME (remove_types u)
  1326         | _ => NONE) %% prf1 %% prf2
  1327      | _ => prf % NONE % NONE %% prf1 %% prf2)
  1328   end;
  1329 
  1330 fun equal_intr A B prf1 prf2 =
  1331   equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
  1332 
  1333 fun equal_elim A B prf1 prf2 =
  1334   equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
  1335 
  1336 
  1337 
  1338 (** rewriting on proof terms **)
  1339 
  1340 (* simple first order matching functions for terms and proofs (see pattern.ML) *)
  1341 
  1342 exception PMatch;
  1343 
  1344 fun flt (i: int) = filter (fn n => n < i);
  1345 
  1346 fun fomatch Ts tymatch j instsp p =
  1347   let
  1348     fun mtch (instsp as (tyinsts, insts)) = fn
  1349         (Var (ixn, T), t)  =>
  1350           if j>0 andalso not (null (flt j (loose_bnos t)))
  1351           then raise PMatch
  1352           else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))),
  1353             (ixn, t) :: insts)
  1354       | (Free (a, T), Free (b, U)) =>
  1355           if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
  1356       | (Const (a, T), Const (b, U))  =>
  1357           if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch
  1358       | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
  1359       | (Bound i, Bound j) => if i=j then instsp else raise PMatch
  1360       | _ => raise PMatch
  1361   in mtch instsp (apply2 Envir.beta_eta_contract p) end;
  1362 
  1363 fun match_proof Ts tymatch =
  1364   let
  1365     fun optmatch _ inst (NONE, _) = inst
  1366       | optmatch _ _ (SOME _, NONE) = raise PMatch
  1367       | optmatch mtch inst (SOME x, SOME y) = mtch inst (x, y)
  1368 
  1369     fun matcht Ts j (pinst, tinst) (t, u) =
  1370       (pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u));
  1371     fun matchT (pinst, (tyinsts, insts)) p =
  1372       (pinst, (tymatch (tyinsts, K p), insts));
  1373     fun matchTs inst (Ts, Us) = Library.foldl (uncurry matchT) (inst, Ts ~~ Us);
  1374 
  1375     fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
  1376           if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst)
  1377           else
  1378             (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of
  1379               ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
  1380             | ([], _) =>
  1381                 if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
  1382                 else raise PMatch
  1383             | _ => raise PMatch)
  1384       | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
  1385           optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
  1386       | mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') =
  1387           mtch Ts i j (mtch Ts i j inst (prf1, prf1')) (prf2, prf2')
  1388       | mtch Ts i j inst (Abst (_, opT, prf1), Abst (_, opU, prf2)) =
  1389           mtch (the_default dummyT opU :: Ts) i (j+1)
  1390             (optmatch matchT inst (opT, opU)) (prf1, prf2)
  1391       | mtch Ts i j inst (prf1, Abst (_, opU, prf2)) =
  1392           mtch (the_default dummyT opU :: Ts) i (j+1) inst
  1393             (incr_pboundvars 0 1 prf1 %> Bound 0, prf2)
  1394       | mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) =
  1395           mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2)
  1396       | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
  1397           mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
  1398       | mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) =
  1399           if s1 = s2 then optmatch matchTs inst (opTs, opUs)
  1400           else raise PMatch
  1401       | mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) =
  1402           if c1 = c2 then matchT inst (T1, T2)
  1403           else raise PMatch
  1404       | mtch Ts i j inst
  1405             (PThm ({name = name1, prop = prop1, types = types1, ...}, _),
  1406               PThm ({name = name2, prop = prop2, types = types2, ...}, _)) =
  1407           if name1 = name2 andalso prop1 = prop2
  1408           then optmatch matchTs inst (types1, types2)
  1409           else raise PMatch
  1410       | mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch
  1411       | mtch _ _ _ _ _ = raise PMatch
  1412   in mtch Ts 0 0 end;
  1413 
  1414 fun prf_subst (pinst, (tyinsts, insts)) =
  1415   let
  1416     val substT = Envir.subst_type_same tyinsts;
  1417     val substTs = Same.map substT;
  1418 
  1419     fun subst' lev (Var (xi, _)) =
  1420         (case AList.lookup (op =) insts xi of
  1421           NONE => raise Same.SAME
  1422         | SOME u => incr_boundvars lev u)
  1423       | subst' _ (Const (s, T)) = Const (s, substT T)
  1424       | subst' _ (Free (s, T)) = Free (s, substT T)
  1425       | subst' lev (Abs (a, T, body)) =
  1426           (Abs (a, substT T, Same.commit (subst' (lev + 1)) body)
  1427             handle Same.SAME => Abs (a, T, subst' (lev + 1) body))
  1428       | subst' lev (f $ t) =
  1429           (subst' lev f $ Same.commit (subst' lev) t
  1430             handle Same.SAME => f $ subst' lev t)
  1431       | subst' _ _ = raise Same.SAME;
  1432 
  1433     fun subst plev tlev (AbsP (a, t, body)) =
  1434           (AbsP (a, Same.map_option (subst' tlev) t, Same.commit (subst (plev + 1) tlev) body)
  1435             handle Same.SAME => AbsP (a, t, subst (plev + 1) tlev body))
  1436       | subst plev tlev (Abst (a, T, body)) =
  1437           (Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body)
  1438             handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body))
  1439       | subst plev tlev (prf %% prf') =
  1440           (subst plev tlev prf %% Same.commit (subst plev tlev) prf'
  1441             handle Same.SAME => prf %% subst plev tlev prf')
  1442       | subst plev tlev (prf % t) =
  1443           (subst plev tlev prf % Same.commit (Same.map_option (subst' tlev)) t
  1444             handle Same.SAME => prf % Same.map_option (subst' tlev) t)
  1445       | subst plev tlev (Hyp (Var (xi, _))) =
  1446           (case AList.lookup (op =) pinst xi of
  1447             NONE => raise Same.SAME
  1448           | SOME prf' => incr_pboundvars plev tlev prf')
  1449       | subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
  1450       | subst _ _ (OfClass (T, c)) = OfClass (substT T, c)
  1451       | subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
  1452       | subst _ _ (PThm ({serial = i, pos = p, theory_name, name = id, prop, types}, thm_body)) =
  1453           PThm (thm_header i p theory_name id prop (Same.map_option substTs types), thm_body)
  1454       | subst _ _ _ = raise Same.SAME;
  1455   in fn t => subst 0 0 t handle Same.SAME => t end;
  1456 
  1457 (*A fast unification filter: true unless the two terms cannot be unified.
  1458   Terms must be NORMAL.  Treats all Vars as distinct. *)
  1459 fun could_unify prf1 prf2 =
  1460   let
  1461     fun matchrands (prf1 %% prf2) (prf1' %% prf2') =
  1462           could_unify prf2 prf2' andalso matchrands prf1 prf1'
  1463       | matchrands (prf % SOME t) (prf' % SOME t') =
  1464           Term.could_unify (t, t') andalso matchrands prf prf'
  1465       | matchrands (prf % _) (prf' % _) = matchrands prf prf'
  1466       | matchrands _ _ = true
  1467 
  1468     fun head_of (prf %% _) = head_of prf
  1469       | head_of (prf % _) = head_of prf
  1470       | head_of prf = prf
  1471 
  1472   in case (head_of prf1, head_of prf2) of
  1473         (_, Hyp (Var _)) => true
  1474       | (Hyp (Var _), _) => true
  1475       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
  1476       | (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2
  1477       | (PThm ({name = a, prop = propa, ...}, _), PThm ({name = b, prop = propb, ...}, _)) =>
  1478           a = b andalso propa = propb andalso matchrands prf1 prf2
  1479       | (PBound i, PBound j) => i = j andalso matchrands prf1 prf2
  1480       | (AbsP _, _) =>  true   (*because of possible eta equality*)
  1481       | (Abst _, _) =>  true
  1482       | (_, AbsP _) =>  true
  1483       | (_, Abst _) =>  true
  1484       | _ => false
  1485   end;
  1486 
  1487 
  1488 (* rewrite proof *)
  1489 
  1490 val no_skel = PBound 0;
  1491 val normal_skel = Hyp (Var ((Name.uu, 0), propT));
  1492 
  1493 fun rewrite_prf tymatch (rules, procs) prf =
  1494   let
  1495     fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
  1496       | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
  1497       | rew Ts hs prf =
  1498           (case get_first (fn r => r Ts hs prf) procs of
  1499             NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
  1500               (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
  1501                  handle PMatch => NONE) (filter (could_unify prf o fst) rules)
  1502           | some => some);
  1503 
  1504     fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) =
  1505           if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf
  1506           else
  1507             let val prf'' = incr_pboundvars (~1) 0 prf'
  1508             in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
  1509       | rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) =
  1510           if prf_loose_bvar1 prf' 0 then rew Ts hs prf
  1511           else
  1512             let val prf'' = incr_pboundvars 0 (~1) prf'
  1513             in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end
  1514       | rew0 Ts hs prf = rew Ts hs prf;
  1515 
  1516     fun rew1 _ _ (Hyp (Var _)) _ = NONE
  1517       | rew1 Ts hs skel prf =
  1518           (case rew2 Ts hs skel prf of
  1519             SOME prf1 =>
  1520               (case rew0 Ts hs prf1 of
  1521                 SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
  1522               | NONE => SOME prf1)
  1523           | NONE =>
  1524               (case rew0 Ts hs prf of
  1525                 SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
  1526               | NONE => NONE))
  1527 
  1528     and rew2 Ts hs skel (prf % SOME t) =
  1529           (case prf of
  1530             Abst (_, _, body) =>
  1531               let val prf' = prf_subst_bounds [t] body
  1532               in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  1533           | _ =>
  1534               (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
  1535                 SOME prf' => SOME (prf' % SOME t)
  1536               | NONE => NONE))
  1537       | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
  1538           (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
  1539       | rew2 Ts hs skel (prf1 %% prf2) =
  1540           (case prf1 of
  1541             AbsP (_, _, body) =>
  1542               let val prf' = prf_subst_pbounds [prf2] body
  1543               in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
  1544           | _ =>
  1545             let
  1546               val (skel1, skel2) =
  1547                 (case skel of
  1548                   skel1 %% skel2 => (skel1, skel2)
  1549                 | _ => (no_skel, no_skel))
  1550             in
  1551               (case rew1 Ts hs skel1 prf1 of
  1552                 SOME prf1' =>
  1553                   (case rew1 Ts hs skel2 prf2 of
  1554                     SOME prf2' => SOME (prf1' %% prf2')
  1555                   | NONE => SOME (prf1' %% prf2))
  1556               | NONE =>
  1557                   (case rew1 Ts hs skel2 prf2 of
  1558                     SOME prf2' => SOME (prf1 %% prf2')
  1559                   | NONE => NONE))
  1560             end)
  1561       | rew2 Ts hs skel (Abst (s, T, prf)) =
  1562           (case rew1 (the_default dummyT T :: Ts) hs
  1563               (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
  1564             SOME prf' => SOME (Abst (s, T, prf'))
  1565           | NONE => NONE)
  1566       | rew2 Ts hs skel (AbsP (s, t, prf)) =
  1567           (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
  1568             SOME prf' => SOME (AbsP (s, t, prf'))
  1569           | NONE => NONE)
  1570       | rew2 _ _ _ _ = NONE;
  1571 
  1572   in the_default prf (rew1 [] [] no_skel prf) end;
  1573 
  1574 fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
  1575   Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
  1576 
  1577 fun rewrite_proof_notypes rews = rewrite_prf fst rews;
  1578 
  1579 
  1580 (* theory data *)
  1581 
  1582 structure Data = Theory_Data
  1583 (
  1584   type T =
  1585     (stamp * (proof * proof)) list *
  1586     (stamp * (typ list -> term option list -> proof -> (proof * proof) option)) list;
  1587 
  1588   val empty = ([], []);
  1589   val extend = I;
  1590   fun merge ((rules1, procs1), (rules2, procs2)) : T =
  1591     (AList.merge (op =) (K true) (rules1, rules2),
  1592       AList.merge (op =) (K true) (procs1, procs2));
  1593 );
  1594 
  1595 fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
  1596 fun rew_proof thy = rewrite_prf fst (get_data thy);
  1597 
  1598 fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
  1599 fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
  1600 
  1601 
  1602 
  1603 (** reconstruction of partial proof terms **)
  1604 
  1605 local
  1606 
  1607 fun vars_of t = map Var (rev (Term.add_vars t []));
  1608 fun frees_of t = map Free (rev (Term.add_frees t []));
  1609 fun variables_of t = vars_of t @ frees_of t;
  1610 
  1611 fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
  1612 fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
  1613 
  1614 fun app_types shift prop Ts prf =
  1615   let
  1616     val tvars = rev (Term.add_tvars prop []);
  1617     val tfrees = rev (Term.add_tfrees prop []);
  1618     val vs = map (fn ((a, i), _) => (a, i + shift)) tvars @ map (fn (a, _) => (a, ~1)) tfrees;
  1619     fun varify (v as (a, S)) = if member (op =) tfrees v then TVar ((a, ~1), S) else TFree v;
  1620   in map_proof_types (typ_subst_TVars (vs ~~ Ts) o map_type_tfree varify) prf end;
  1621 
  1622 fun guess_name (PThm ({name, ...}, _)) = name
  1623   | guess_name (prf %% Hyp _) = guess_name prf
  1624   | guess_name (prf %% OfClass _) = guess_name prf
  1625   | guess_name (prf % NONE) = guess_name prf
  1626   | guess_name (prf % SOME (Var _)) = guess_name prf
  1627   | guess_name _ = "";
  1628 
  1629 
  1630 (* generate constraints for proof term *)
  1631 
  1632 fun mk_var env Ts T =
  1633   let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
  1634   in (list_comb (v, map Bound (length Ts - 1 downto 0)), env') end;
  1635 
  1636 fun mk_tvar S (Envir.Envir {maxidx, tenv, tyenv}) =
  1637   (TVar (("'t", maxidx + 1), S),
  1638     Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv});
  1639 
  1640 val mk_abs = fold (fn T => fn u => Abs ("", T, u));
  1641 
  1642 fun unifyT thy env T U =
  1643   let
  1644     val Envir.Envir {maxidx, tenv, tyenv} = env;
  1645     val (tyenv', maxidx') = Sign.typ_unify thy (T, U) (tyenv, maxidx);
  1646   in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end;
  1647 
  1648 fun chaseT env (T as TVar v) =
  1649       (case Type.lookup (Envir.type_env env) v of
  1650         NONE => T
  1651       | SOME T' => chaseT env T')
  1652   | chaseT _ T = T;
  1653 
  1654 fun infer_type thy (env as Envir.Envir {maxidx, tenv, tyenv}) _ vTs
  1655       (t as Const (s, T)) = if T = dummyT then
  1656         (case Sign.const_type thy s of
  1657           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
  1658         | SOME T =>
  1659             let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
  1660             in (Const (s, T'), T', vTs,
  1661               Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
  1662             end)
  1663       else (t, T, vTs, env)
  1664   | infer_type _ env _ vTs (t as Free (s, T)) =
  1665       if T = dummyT then (case Symtab.lookup vTs s of
  1666           NONE =>
  1667             let val (T, env') = mk_tvar [] env
  1668             in (Free (s, T), T, Symtab.update_new (s, T) vTs, env') end
  1669         | SOME T => (Free (s, T), T, vTs, env))
  1670       else (t, T, vTs, env)
  1671   | infer_type _ _ _ _ (Var _) = error "reconstruct_proof: internal error"
  1672   | infer_type thy env Ts vTs (Abs (s, T, t)) =
  1673       let
  1674         val (T', env') = if T = dummyT then mk_tvar [] env else (T, env);
  1675         val (t', U, vTs', env'') = infer_type thy env' (T' :: Ts) vTs t
  1676       in (Abs (s, T', t'), T' --> U, vTs', env'') end
  1677   | infer_type thy env Ts vTs (t $ u) =
  1678       let
  1679         val (t', T, vTs1, env1) = infer_type thy env Ts vTs t;
  1680         val (u', U, vTs2, env2) = infer_type thy env1 Ts vTs1 u;
  1681       in (case chaseT env2 T of
  1682           Type ("fun", [U', V]) => (t' $ u', V, vTs2, unifyT thy env2 U U')
  1683         | _ =>
  1684           let val (V, env3) = mk_tvar [] env2
  1685           in (t' $ u', V, vTs2, unifyT thy env3 T (U --> V)) end)
  1686       end
  1687   | infer_type _ env Ts vTs (t as Bound i) = ((t, nth Ts i, vTs, env)
  1688       handle General.Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
  1689 
  1690 fun cantunify thy (t, u) =
  1691   error ("Non-unifiable terms:\n" ^
  1692     Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
  1693 
  1694 fun decompose thy Ts (p as (t, u)) env =
  1695   let
  1696     fun rigrig (a, T) (b, U) uT ts us =
  1697       if a <> b then cantunify thy p
  1698       else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
  1699   in
  1700     case apply2 (strip_comb o Envir.head_norm env) p of
  1701       ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
  1702     | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
  1703     | ((Bound i, ts), (Bound j, us)) =>
  1704         rigrig (i, dummyT) (j, dummyT) (K o K) ts us
  1705     | ((Abs (_, T, t), []), (Abs (_, U, u), [])) =>
  1706         decompose thy (T::Ts) (t, u) (unifyT thy env T U)
  1707     | ((Abs (_, T, t), []), _) =>
  1708         decompose thy (T::Ts) (t, incr_boundvars 1 u $ Bound 0) env
  1709     | (_, (Abs (_, T, u), [])) =>
  1710         decompose thy (T::Ts) (incr_boundvars 1 t $ Bound 0, u) env
  1711     | _ => ([(mk_abs Ts t, mk_abs Ts u)], env)
  1712   end;
  1713 
  1714 fun make_constraints_cprf thy env cprf =
  1715   let
  1716     fun add_cnstrt Ts prop prf cs env vTs (t, u) =
  1717       let
  1718         val t' = mk_abs Ts t;
  1719         val u' = mk_abs Ts u
  1720       in
  1721         (prop, prf, cs, Pattern.unify (Context.Theory thy) (t', u') env, vTs)
  1722           handle Pattern.Pattern =>
  1723             let val (cs', env') = decompose thy [] (t', u') env
  1724             in (prop, prf, cs @ cs', env', vTs) end
  1725           | Pattern.Unif => cantunify thy (Envir.norm_term env t', Envir.norm_term env u')
  1726       end;
  1727 
  1728     fun mk_cnstrts_atom env vTs prop opTs prf =
  1729           let
  1730             val tvars = Term.add_tvars prop [] |> rev;
  1731             val tfrees = Term.add_tfrees prop [] |> rev;
  1732             val (Ts, env') =
  1733               (case opTs of
  1734                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
  1735               | SOME Ts => (Ts, env));
  1736             val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
  1737               (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
  1738                 error ("Wrong number of type arguments for " ^ quote (guess_name prf))
  1739           in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
  1740 
  1741     fun head_norm (prop, prf, cnstrts, env, vTs) =
  1742       (Envir.head_norm env prop, prf, cnstrts, env, vTs);
  1743 
  1744     fun mk_cnstrts env _ Hs vTs (PBound i) = ((nth Hs i, PBound i, [], env, vTs)
  1745           handle General.Subscript => error ("mk_cnstrts: bad variable index " ^ string_of_int i))
  1746       | mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
  1747           let
  1748             val (T, env') =
  1749               (case opT of
  1750                 NONE => mk_tvar [] env
  1751               | SOME T => (T, env));
  1752             val (t, prf, cnstrts, env'', vTs') =
  1753               mk_cnstrts env' (T::Ts) (map (incr_boundvars 1) Hs) vTs cprf;
  1754           in
  1755             (Const ("Pure.all", (T --> propT) --> propT) $ Abs (s, T, t), Abst (s, SOME T, prf),
  1756               cnstrts, env'', vTs')
  1757           end
  1758       | mk_cnstrts env Ts Hs vTs (AbsP (s, SOME t, cprf)) =
  1759           let
  1760             val (t', _, vTs', env') = infer_type thy env Ts vTs t;
  1761             val (u, prf, cnstrts, env'', vTs'') = mk_cnstrts env' Ts (t'::Hs) vTs' cprf;
  1762           in (Logic.mk_implies (t', u), AbsP (s, SOME t', prf), cnstrts, env'', vTs'')
  1763           end
  1764       | mk_cnstrts env Ts Hs vTs (AbsP (s, NONE, cprf)) =
  1765           let
  1766             val (t, env') = mk_var env Ts propT;
  1767             val (u, prf, cnstrts, env'', vTs') = mk_cnstrts env' Ts (t::Hs) vTs cprf;
  1768           in (Logic.mk_implies (t, u), AbsP (s, SOME t, prf), cnstrts, env'', vTs')
  1769           end
  1770       | mk_cnstrts env Ts Hs vTs (cprf1 %% cprf2) =
  1771           let val (u, prf2, cnstrts, env', vTs') = mk_cnstrts env Ts Hs vTs cprf2
  1772           in (case head_norm (mk_cnstrts env' Ts Hs vTs' cprf1) of
  1773               (Const ("Pure.imp", _) $ u' $ t', prf1, cnstrts', env'', vTs'') =>
  1774                 add_cnstrt Ts t' (prf1 %% prf2) (cnstrts' @ cnstrts)
  1775                   env'' vTs'' (u, u')
  1776             | (t, prf1, cnstrts', env'', vTs'') =>
  1777                 let val (v, env''') = mk_var env'' Ts propT
  1778                 in add_cnstrt Ts v (prf1 %% prf2) (cnstrts' @ cnstrts)
  1779                   env''' vTs'' (t, Logic.mk_implies (u, v))
  1780                 end)
  1781           end
  1782       | mk_cnstrts env Ts Hs vTs (cprf % SOME t) =
  1783           let val (t', U, vTs1, env1) = infer_type thy env Ts vTs t
  1784           in (case head_norm (mk_cnstrts env1 Ts Hs vTs1 cprf) of
  1785              (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
  1786                  prf, cnstrts, env2, vTs2) =>
  1787                let val env3 = unifyT thy env2 T U
  1788                in (betapply (f, t'), prf % SOME t', cnstrts, env3, vTs2)
  1789                end
  1790            | (u, prf, cnstrts, env2, vTs2) =>
  1791                let val (v, env3) = mk_var env2 Ts (U --> propT);
  1792                in
  1793                  add_cnstrt Ts (v $ t') (prf % SOME t') cnstrts env3 vTs2
  1794                    (u, Const ("Pure.all", (U --> propT) --> propT) $ v)
  1795                end)
  1796           end
  1797       | mk_cnstrts env Ts Hs vTs (cprf % NONE) =
  1798           (case head_norm (mk_cnstrts env Ts Hs vTs cprf) of
  1799              (Const ("Pure.all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
  1800                  prf, cnstrts, env', vTs') =>
  1801                let val (t, env'') = mk_var env' Ts T
  1802                in (betapply (f, t), prf % SOME t, cnstrts, env'', vTs')
  1803                end
  1804            | (u, prf, cnstrts, env', vTs') =>
  1805                let
  1806                  val (T, env1) = mk_tvar [] env';
  1807                  val (v, env2) = mk_var env1 Ts (T --> propT);
  1808                  val (t, env3) = mk_var env2 Ts T
  1809                in
  1810                  add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
  1811                    (u, Const ("Pure.all", (T --> propT) --> propT) $ v)
  1812                end)
  1813       | mk_cnstrts env _ _ vTs (prf as PThm ({prop, types = opTs, ...}, _)) =
  1814           mk_cnstrts_atom env vTs prop opTs prf
  1815       | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
  1816           mk_cnstrts_atom env vTs prop opTs prf
  1817       | mk_cnstrts env _ _ vTs (prf as OfClass (T, c)) =
  1818           mk_cnstrts_atom env vTs (Logic.mk_of_class (T, c)) NONE prf
  1819       | mk_cnstrts env _ _ vTs (prf as Oracle (_, prop, opTs)) =
  1820           mk_cnstrts_atom env vTs prop opTs prf
  1821       | mk_cnstrts env _ _ vTs (Hyp t) = (t, Hyp t, [], env, vTs)
  1822       | mk_cnstrts _ _ _ _ MinProof = error "reconstruct_proof: minimal proof object"
  1823   in mk_cnstrts env [] [] Symtab.empty cprf end;
  1824 
  1825 
  1826 (* update list of free variables of constraints *)
  1827 
  1828 fun upd_constrs env cs =
  1829   let
  1830     val tenv = Envir.term_env env;
  1831     val tyenv = Envir.type_env env;
  1832     val dom = []
  1833       |> Vartab.fold (cons o #1) tenv
  1834       |> Vartab.fold (cons o #1) tyenv;
  1835     val vran = []
  1836       |> Vartab.fold (Term.add_var_names o #2 o #2) tenv
  1837       |> Vartab.fold (Term.add_tvar_namesT o #2 o #2) tyenv;
  1838     fun check_cs [] = []
  1839       | check_cs ((u, p, vs) :: ps) =
  1840           let val vs' = subtract (op =) dom vs in
  1841             if vs = vs' then (u, p, vs) :: check_cs ps
  1842             else (true, p, fold (insert op =) vs' vran) :: check_cs ps
  1843           end;
  1844   in check_cs cs end;
  1845 
  1846 
  1847 (* solution of constraints *)
  1848 
  1849 fun solve _ [] bigenv = bigenv
  1850   | solve thy cs bigenv =
  1851       let
  1852         fun search _ [] =
  1853               error ("Unsolvable constraints:\n" ^
  1854                 Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
  1855                   Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
  1856                     (apply2 (Envir.norm_term bigenv) p)) cs)))
  1857           | search env ((u, p as (t1, t2), vs)::ps) =
  1858               if u then
  1859                 let
  1860                   val tn1 = Envir.norm_term bigenv t1;
  1861                   val tn2 = Envir.norm_term bigenv t2
  1862                 in
  1863                   if Pattern.pattern tn1 andalso Pattern.pattern tn2 then
  1864                     (Pattern.unify (Context.Theory thy) (tn1, tn2) env, ps)
  1865                       handle Pattern.Unif => cantunify thy (tn1, tn2)
  1866                   else
  1867                     let val (cs', env') = decompose thy [] (tn1, tn2) env
  1868                     in if cs' = [(tn1, tn2)] then
  1869                          apsnd (cons (false, (tn1, tn2), vs)) (search env ps)
  1870                        else search env' (map (fn q => (true, q, vs)) cs' @ ps)
  1871                     end
  1872                 end
  1873               else apsnd (cons (false, p, vs)) (search env ps);
  1874         val Envir.Envir {maxidx, ...} = bigenv;
  1875         val (env, cs') = search (Envir.empty maxidx) cs;
  1876       in
  1877         solve thy (upd_constrs env cs') (Envir.merge (bigenv, env))
  1878       end;
  1879 
  1880 in
  1881 
  1882 
  1883 (* reconstruction of proofs *)
  1884 
  1885 fun reconstruct_proof thy prop cprf =
  1886   let
  1887     val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
  1888     val (t, prf, cs, env, _) = make_constraints_cprf thy
  1889       (Envir.empty (maxidx_proof cprf ~1)) cprf';
  1890     val cs' =
  1891       map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
  1892       |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
  1893     val env' = solve thy cs' env
  1894   in thawf (norm_proof env' prf) end;
  1895 
  1896 fun prop_of_atom prop Ts = subst_atomic_types
  1897   (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
  1898   (forall_intr_vfs prop);
  1899 
  1900 val head_norm = Envir.head_norm Envir.init;
  1901 
  1902 fun prop_of0 Hs (PBound i) = nth Hs i
  1903   | prop_of0 Hs (Abst (s, SOME T, prf)) =
  1904       Logic.all_const T $ (Abs (s, T, prop_of0 Hs prf))
  1905   | prop_of0 Hs (AbsP (_, SOME t, prf)) =
  1906       Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
  1907   | prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
  1908       Const ("Pure.all", _) $ f => f $ t
  1909     | _ => error "prop_of: all expected")
  1910   | prop_of0 Hs (prf1 %% _) = (case head_norm (prop_of0 Hs prf1) of
  1911       Const ("Pure.imp", _) $ _ $ Q => Q
  1912     | _ => error "prop_of: ==> expected")
  1913   | prop_of0 _ (Hyp t) = t
  1914   | prop_of0 _ (PThm ({prop, types = SOME Ts, ...}, _)) = prop_of_atom prop Ts
  1915   | prop_of0 _ (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
  1916   | prop_of0 _ (OfClass (T, c)) = Logic.mk_of_class (T, c)
  1917   | prop_of0 _ (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
  1918   | prop_of0 _ _ = error "prop_of: partial proof object";
  1919 
  1920 val prop_of' = Envir.beta_eta_contract oo prop_of0;
  1921 val prop_of = prop_of' [];
  1922 
  1923 
  1924 (* expand and reconstruct subproofs *)
  1925 
  1926 fun expand_proof thy thms prf =
  1927   let
  1928     fun expand maxidx prfs (AbsP (s, t, prf)) =
  1929           let val (maxidx', prfs', prf') = expand maxidx prfs prf
  1930           in (maxidx', prfs', AbsP (s, t, prf')) end
  1931       | expand maxidx prfs (Abst (s, T, prf)) =
  1932           let val (maxidx', prfs', prf') = expand maxidx prfs prf
  1933           in (maxidx', prfs', Abst (s, T, prf')) end
  1934       | expand maxidx prfs (prf1 %% prf2) =
  1935           let
  1936             val (maxidx', prfs', prf1') = expand maxidx prfs prf1;
  1937             val (maxidx'', prfs'', prf2') = expand maxidx' prfs' prf2;
  1938           in (maxidx'', prfs'', prf1' %% prf2') end
  1939       | expand maxidx prfs (prf % t) =
  1940           let val (maxidx', prfs', prf') = expand maxidx prfs prf
  1941           in (maxidx', prfs', prf' % t) end
  1942       | expand maxidx prfs (prf as PThm ({name = a, prop, types = SOME Ts, ...}, thm_body)) =
  1943           if not (exists
  1944             (fn (b, NONE) => a = b
  1945               | (b, SOME prop') => a = b andalso prop = prop') thms)
  1946           then (maxidx, prfs, prf) else
  1947           let
  1948             val (maxidx', prf, prfs') =
  1949               (case AList.lookup (op =) prfs (a, prop) of
  1950                 NONE =>
  1951                   let
  1952                     val prf' =
  1953                       thm_body_proof_open thm_body
  1954                       |> reconstruct_proof thy prop
  1955                       |> forall_intr_vfs_prf prop;
  1956                     val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf'
  1957                   in
  1958                     (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
  1959                       ((a, prop), (maxidx', prf)) :: prfs')
  1960                   end
  1961               | SOME (maxidx', prf) =>
  1962                   (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf, prfs));
  1963           in (maxidx', prfs', app_types (maxidx + 1) prop Ts prf) end
  1964       | expand maxidx prfs prf = (maxidx, prfs, prf);
  1965 
  1966   in #3 (expand (maxidx_proof prf ~1) [] prf) end;
  1967 
  1968 end;
  1969 
  1970 
  1971 
  1972 (** promises **)
  1973 
  1974 fun fulfill_norm_proof thy ps body0 =
  1975   let
  1976     val _ = consolidate (map #2 ps @ [body0]);
  1977     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
  1978     val oracles =
  1979       unions_oracles
  1980         (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
  1981     val thms =
  1982       unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
  1983     val proof = rew_proof thy proof0;
  1984   in PBody {oracles = oracles, thms = thms, proof = proof} end;
  1985 
  1986 fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
  1987   let
  1988     fun fulfill () =
  1989       postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
  1990   in
  1991     if null promises then Future.map postproc body
  1992     else if Future.is_finished body andalso length promises = 1 then
  1993       Future.map (fn _ => fulfill ()) (snd (hd promises))
  1994     else
  1995       (singleton o Future.forks)
  1996         {name = "Proofterm.fulfill_proof_future", group = NONE,
  1997           deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 1,
  1998           interrupts = true}
  1999         fulfill
  2000   end;
  2001 
  2002 
  2003 
  2004 (** theorems **)
  2005 
  2006 (* standardization of variables for export: only frees and named bounds *)
  2007 
  2008 local
  2009 
  2010 val declare_names_term = Term.declare_term_frees;
  2011 val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
  2012 
  2013 fun declare_names_proof (Abst (_, _, prf)) = declare_names_proof prf
  2014   | declare_names_proof (AbsP (_, t, prf)) = declare_names_term' t #> declare_names_proof prf
  2015   | declare_names_proof (prf % t) = declare_names_proof prf #> declare_names_term' t
  2016   | declare_names_proof (prf1 %% prf2) = declare_names_proof prf1 #> declare_names_proof prf2
  2017   | declare_names_proof _ = I;
  2018 
  2019 fun variant names bs x =
  2020   #1 (Name.variant x (fold Name.declare bs names));
  2021 
  2022 fun variant_term bs (Abs (x, T, t)) =
  2023       let
  2024         val x' = variant (declare_names_term t Name.context) bs x;
  2025         val t' = variant_term (x' :: bs) t;
  2026       in Abs (x', T, t') end
  2027   | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
  2028   | variant_term _ t = t;
  2029 
  2030 fun variant_proof bs (Abst (x, T, prf)) =
  2031       let
  2032         val x' = variant (declare_names_proof prf Name.context) bs x;
  2033         val prf' = variant_proof (x' :: bs) prf;
  2034       in Abst (x', T, prf') end
  2035   | variant_proof bs (AbsP (x, t, prf)) =
  2036       let
  2037         val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
  2038         val t' = Option.map (variant_term bs) t;
  2039         val prf' = variant_proof (x' :: bs) prf;
  2040       in AbsP (x', t', prf') end
  2041   | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
  2042   | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
  2043   | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
  2044   | variant_proof _ prf = prf;
  2045 
  2046 val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
  2047 fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
  2048 val used_frees_proof = fold_proof_terms used_frees_term used_frees_type;
  2049 
  2050 val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
  2051 val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
  2052 
  2053 in
  2054 
  2055 fun standard_vars used (terms, proofs) =
  2056   let
  2057     val used' = used
  2058       |> fold used_frees_term terms
  2059       |> fold used_frees_proof proofs;
  2060     val proof_terms = rev ((fold (fold_proof_terms cons (cons o Logic.mk_type))) proofs []);
  2061     val inst = Term_Subst.zero_var_indexes_inst used' (terms @ proof_terms);
  2062 
  2063     val terms' = terms
  2064       |> map (Term_Subst.instantiate inst #> unvarify #> variant_term []);
  2065     val proofs' = proofs
  2066       |> map (instantiate inst #> map_proof_terms unvarify unvarifyT #> variant_proof []);
  2067   in (terms', proofs') end;
  2068 
  2069 fun standard_vars_term used t = standard_vars used ([t], []) |> #1 |> the_single;
  2070 fun standard_vars_proof used prf = standard_vars used ([], [prf]) |> #2 |> the_single;
  2071 
  2072 end;
  2073 
  2074 
  2075 (* PThm nodes *)
  2076 
  2077 val proof_serial = Counter.make ();
  2078 
  2079 local
  2080 
  2081 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
  2082   let
  2083     fun hyp_map hyp =
  2084       (case AList.lookup (op =) (#constraints ucontext) hyp of
  2085         SOME t => Hyp t
  2086       | NONE => raise Fail "unconstrainT_proof: missing constraint");
  2087 
  2088     val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
  2089     fun ofclass (ty, c) =
  2090       let val ty' = Term.map_atyps (#atyp_map ucontext) ty;
  2091       in the_single (of_sort_proof algebra classrel_proof arity_proof  hyp_map (ty', [c])) end;
  2092   in
  2093     Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
  2094     #> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
  2095   end;
  2096 
  2097 fun clean_proof thy = rew_proof thy #> shrink_proof;
  2098 
  2099 fun encode_export prop prf =
  2100   let open XML.Encode Term_XML.Encode
  2101   in pair term encode_full (prop, prf) end;
  2102 
  2103 fun export_proof thy i prop prf =
  2104   let
  2105     val ([prop'], [prf']) = standard_vars Name.context ([prop], [reconstruct_proof thy prop prf]);
  2106     val xml = encode_export prop' prf';
  2107     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
  2108   in
  2109     chunks |> Export.export_params
  2110      {theory = thy,
  2111       binding = Path.binding0 (Path.make ["proofs", string_of_int i]),
  2112       executable = false,
  2113       compress = true,
  2114       strict = false}
  2115   end;
  2116 
  2117 fun export_proof_boxes proof =
  2118   let
  2119     fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
  2120       | export_boxes (Abst (_, _, prf)) = export_boxes prf
  2121       | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
  2122       | export_boxes (prf % _) = export_boxes prf
  2123       | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
  2124           (fn boxes =>
  2125             if Inttab.defined boxes i then boxes
  2126             else
  2127               let
  2128                 val prf = thm_body_proof_raw thm_body;
  2129                 val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
  2130               in export_boxes prf boxes' end)
  2131       | export_boxes _ = I;
  2132     val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
  2133   in List.app (Lazy.force o #2) boxes end;
  2134 
  2135 fun export_enabled () = Options.default_bool "export_proofs";
  2136 
  2137 fun export thy i prop prf =
  2138   if export_enabled () then (export_proof_boxes prf; export_proof thy i prop prf) else ();
  2139 
  2140 fun prune proof =
  2141   if Options.default_bool "prune_proofs" then MinProof
  2142   else proof;
  2143 
  2144 fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
  2145     (name, pos) shyps hyps concl promises body =
  2146   let
  2147     val named = name <> "";
  2148 
  2149     val prop = Logic.list_implies (hyps, concl);
  2150     val args = prop_args prop;
  2151 
  2152     val (ucontext, prop1) = Logic.unconstrainT shyps prop;
  2153 
  2154     val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
  2155     val body0 =
  2156       Future.value
  2157         (PBody {oracles = oracles0, thms = thms0,
  2158           proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
  2159 
  2160     fun publish i = map_proof_of (clean_proof thy #> tap (export thy i prop1) #> prune);
  2161     val open_proof = not named ? clean_proof thy;
  2162 
  2163     fun new_prf () =
  2164       let
  2165         val i = proof_serial ();
  2166         val unconstrainT =
  2167           unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
  2168         val postproc = map_proof_of unconstrainT #> named ? publish i;
  2169       in (i, fulfill_proof_future thy promises postproc body0) end;
  2170 
  2171     val (i, body') =
  2172       (*non-deterministic, depends on unknown promises*)
  2173       (case strip_combt (fst (strip_combP prf)) of
  2174         (PThm ({serial = i, name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
  2175           if (a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
  2176             let val Thm_Body {body = body', ...} = thm_body';
  2177             in (i, body' |> (a = "" andalso named) ? Future.map (publish i)) end
  2178           else new_prf ()
  2179       | _ => new_prf ());
  2180 
  2181     val export_proof =
  2182       if named orelse not (export_enabled ()) then no_export_proof
  2183       else Lazy.lazy (fn () => join_proof body' |> open_proof |> export_proof thy i prop1);
  2184 
  2185     val pthm = (i, make_thm_node name prop1 body');
  2186 
  2187     val header =
  2188       thm_header i ([pos, Position.thread_data ()]) (Context.theory_long_name thy) name prop1 NONE;
  2189     val thm_body = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'};
  2190     val head = PThm (header, thm_body);
  2191     val proof =
  2192       if unconstrain then
  2193         proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args)
  2194       else
  2195         proof_combP (proof_combt' (head, args),
  2196           map OfClass (#outer_constraints ucontext) @ map Hyp hyps);
  2197   in (pthm, proof) end;
  2198 
  2199 in
  2200 
  2201 val thm_proof = prepare_thm_proof false;
  2202 
  2203 fun unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
  2204   prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)
  2205     shyps [] concl promises body;
  2206 
  2207 end;
  2208 
  2209 
  2210 (* approximative PThm name *)
  2211 
  2212 fun get_name shyps hyps prop prf =
  2213   let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
  2214     (case fst (strip_combt (fst (strip_combP prf))) of
  2215       PThm ({name, prop = prop', ...}, _) => if prop = prop' then name else ""
  2216     | _ => "")
  2217   end;
  2218 
  2219 end;
  2220 
  2221 structure Basic_Proofterm : BASIC_PROOFTERM = Proofterm;
  2222 open Basic_Proofterm;