Quelle thm.ML Sprache: SML

(*  Title:      Pure/thm.ML
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Makarius

The very core of Isabelle's Meta Logic: certified types and terms,
derivations, theorems, inference rules (including lifting and
resolution), oracles.
*)

infix 0 RS RSN;

signature BASIC_THM =
sig
  type ctyp
  type cterm
  exception CTERM of string * cterm list
  type thm
  type conv = cterm -> thm
  exception THM of string * int * thm list
  val RSN: thm * (int * thm) -> thm
  val RS: thm * thm -> thm
end;

signature THM =
sig
  include BASIC_THM
  (*certified types*)
  val typ_of: ctyp -> typ
  val global_ctyp_of: theory -> typ -> ctyp
  val ctyp_of: Proof.context -> typ -> ctyp
  val dest_ctyp: ctyp -> ctyp list
  val dest_ctypN: int -> ctyp -> ctyp
  val make_ctyp: ctyp -> ctyp list -> ctyp
  val maxidx_of_ctyp: ctyp -> int
  (*certified terms*)
  val term_of: cterm -> term
  val typ_of_cterm: cterm -> typ
  val ctyp_of_cterm: cterm -> ctyp
  val maxidx_of_cterm: cterm -> int
  val global_cterm_of: theory -> term -> cterm
  val cterm_of: Proof.context -> term -> cterm
  val renamed_term: term -> cterm -> cterm
  val fast_term_ord: cterm ord
  val term_ord: cterm ord
  val dest_comb: cterm -> cterm * cterm
  val dest_fun: cterm -> cterm
  val dest_arg: cterm -> cterm
  val dest_fun2: cterm -> cterm
  val dest_arg1: cterm -> cterm
  val dest_abs_fresh: string -> cterm -> cterm * cterm
  val dest_abs_global: cterm -> cterm * cterm
  val rename_tvar: indexname -> ctyp -> ctyp
  val free: string * ctyp -> cterm
  val var: indexname * ctyp -> cterm
  val apply: cterm -> cterm -> cterm
  val lambda_name: string * cterm -> cterm -> cterm
  val lambda: cterm -> cterm -> cterm
  val adjust_maxidx_cterm: int -> cterm -> cterm
  val incr_indexes_cterm: int -> cterm -> cterm
  val match: cterm * cterm -> ctyp TVars.table * cterm Vars.table
  val first_order_match: cterm * cterm -> ctyp TVars.table * cterm Vars.table
  (*theorems*)
  val fold_terms: {hyps: bool} -> (term -> 'a -> 'a) -> thm -> 'a -> 'a
  val fold_atomic_ctyps: {hyps: bool} ->
    ('a -> typ -> bool) -> (ctyp -> 'a -> 'a) -> thm -> 'a -> 'a
  val fold_atomic_cterms: {hyps: bool} ->
    ('a -> term -> bool) -> (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
  val terms_of_tpairs: (term * term) list -> term list
  val full_prop_of: thm -> term
  val theory_id: thm -> Context.theory_id
  val theory_name: {long: bool} -> thm -> string
  val theory_long_name: thm -> string
  val theory_base_name: thm -> string
  val maxidx_of: thm -> int
  val maxidx_thm: thm -> int -> int
  val shyps_of: thm -> sort Ord_List.T
  val hyps_of: thm -> term list
  val prop_of: thm -> term
  val tpairs_of: thm -> (term * term) list
  val concl_of: thm -> term
  val prems_of: thm -> term list
  val take_prems_of: int -> thm -> term list
  val nprems_of: thm -> int
  val no_prems: thm -> bool
  val one_prem: thm -> bool
  val prem_of: thm -> int -> term
  val major_prem_of: thm -> term
  val cprop_of: thm -> cterm
  val cprem_of: thm -> int -> cterm
  val cconcl_of: thm -> cterm
  val cprems_of: thm -> cterm list
  val take_cprems_of: int -> thm -> cterm list
  val chyps_of: thm -> cterm list
  val thm_ord: thm ord
  exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
  val theory_of_cterm: cterm -> theory
  val theory_of_thm: thm -> theory
  val trim_context_ctyp: ctyp -> ctyp
  val trim_context_cterm: cterm -> cterm
  val transfer_ctyp: theory -> ctyp -> ctyp
  val transfer_ctyp': Proof.context -> ctyp -> ctyp
  val transfer_ctyp'': Context.generic -> ctyp -> ctyp
  val transfer_cterm: theory -> cterm -> cterm
  val transfer_cterm': Proof.context -> cterm -> cterm
  val transfer_cterm'': Context.generic -> cterm -> cterm
  val transfer: theory -> thm -> thm
  val transfer': Proof.context -> thm -> thm
  val transfer'': Context.generic -> thm -> thm
  val join_transfer: theory -> thm -> thm
  val join_transfer_context: Proof.context * thm -> Proof.context * thm
  val renamed_prop: term -> thm -> thm
  val weaken: cterm -> thm -> thm
  val weaken_sorts: sort list -> cterm -> cterm
  val proof_bodies_of: thm list -> proof_body list
  val proof_body_of: thm -> proof_body
  val zproof_of: thm -> zproof
  val proof_of: thm -> proof
  val reconstruct_proof_of: thm -> Proofterm.proof
  val consolidate: thm list -> unit
  val expose_proofs: theory -> thm list -> unit
  val expose_proof: theory -> thm -> unit
  val future: thm future -> cterm -> thm
  val thm_deps: thm -> Proofterm.thm Ord_List.T
  val extra_shyps: thm -> sort list
  val strip_shyps: thm -> thm
  val derivation_closed: thm -> bool
  val derivation_name: thm -> Thm_Name.T
  val derivation_id: thm -> Proofterm.thm_id option
  val raw_derivation_name: thm -> Thm_Name.P
  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option
  val name_derivation: Thm_Name.P -> thm -> thm
  val close_derivation: Position.T -> thm -> thm
  val trim_context: thm -> thm
  val axiom: theory -> string -> thm
  val all_axioms_of: theory -> (string * thm) list
  val get_tags: thm -> Properties.T
  val map_tags: (Properties.T -> Properties.T) -> thm -> thm
  val norm_proof: thm -> thm
  val adjust_maxidx_thm: int -> thm -> thm
  (*type classes*)
  val the_classrel: theory -> class * class -> thm
  val the_arity: theory -> string * sort list * class -> thm
  val sorts_zproof: theory -> ZTerm.sorts_proof
  val sorts_proof: theory -> Proofterm.sorts_proof
  (*oracles*)
  val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
  val oracle_space: theory -> Name_Space.T
  val pretty_oracle: Proof.context -> string -> Pretty.T
  val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
  val check_oracle: Proof.context -> xstring * Position.T -> string
  (*inference rules*)
  val assume: cterm -> thm  (*exception THM*)
  val assume_cterm: cterm -> thm  (*exception CTERM*)
  val implies_intr: cterm -> thm -> thm
  val implies_elim: thm -> thm -> thm
  val forall_intr: cterm -> thm -> thm
  val forall_elim: cterm -> thm -> thm
  val reflexive: cterm -> thm
  val symmetric: thm -> thm
  val transitive: thm -> thm -> thm
  val beta_conversion: bool -> conv
  val eta_conversion: conv
  val eta_long_conversion: conv
  val abstract_rule: string -> cterm -> thm -> thm
  val combination: thm -> thm -> thm
  val equal_intr: thm -> thm -> thm
  val equal_elim: thm -> thm -> thm
  val solve_constraints: thm -> thm
  val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
  val generalize: Names.set * Names.set -> int -> thm -> thm
  val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm
  val generalize_ctyp: Names.set -> int -> ctyp -> ctyp
  val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm
  val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm
  val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
  val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
  val trivial: cterm -> thm
  val of_class: ctyp * class -> thm
  val unconstrainT: thm -> thm
  val varifyT_global': TFrees.set -> thm -> ((string * sort) * (indexname * sort)) list * thm
  val varifyT_global: thm -> thm
  val legacy_freezeT: thm -> thm
  val plain_prop_of: thm -> term
  val get_zproof_serials: theory -> serial list
  val get_zproof: theory -> serial ->
    {name: Thm_Name.P, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option
  val store_zproof: Thm_Name.P -> thm -> theory -> thm * theory
  val dest_state: thm * int -> (term * term) list * term list * term * term
  val lift_rule: cterm -> thm -> thm
  val incr_indexes: int -> thm -> thm
  val assumption: Proof.context option -> int -> thm -> thm Seq.seq
  val eq_assumption: int -> thm -> thm
  val rotate_rule: int -> int -> thm -> thm
  val permute_prems: int -> int -> thm -> thm
  val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
    bool * thm * int -> int -> thm -> thm Seq.seq
  val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
  val theory_names_of_arity: {long: bool} -> theory -> string * class -> string list
  val add_classrel: thm -> theory -> theory
  val add_arity: thm -> theory -> theory
end;

structure Thm: THM =
struct

(*** Certified terms and types ***)

(** certified types **)

datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T};

fun typ_of (Ctyp {T, ...}) = T;

fun maxidx_of_ctyp (Ctyp {maxidx, ...}) = maxidx;

fun global_ctyp_of thy raw_T =
  let
    val T = Sign.certify_typ thy raw_T;
    val maxidx = Term.maxidx_of_typ T;
    val sorts = Sorts.insert_typ T [];
  in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end;

val ctyp_of = global_ctyp_of o Proof_Context.theory_of;

fun dest_ctyp (Ctyp {cert, T = Type (_, Ts), maxidx, sorts}) =
      map (fn T => Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts}) Ts
  | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);

fun dest_ctypN n (Ctyp {cert, T, maxidx, sorts}) =
  let fun err () = raise TYPE ("dest_ctypN", [T], []) in
    (case T of
      Type (_, Ts) =>
        Ctyp {cert = cert, T = nth Ts n handle General.Subscript => err (),
          maxidx = maxidx, sorts = sorts}
    | _ => err ())
  end;

fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert);
fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts;
fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx);

fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs =
  let
    val As = map typ_of cargs;
    fun err () = raise TYPE ("make_ctyp", T :: As, []);
  in
    (case T of
      Type (a, args) =>
        Ctyp {
          cert = fold join_certificate_ctyp cargs cert,
          maxidx = fold maxidx_ctyp cargs ~1,
          sorts = fold union_sorts_ctyp cargs [],
          T = if length args = length cargs then Type (a, As) else err ()}
    | _ => err ())
  end;

(** certified terms **)

(*certified terms with checked typ, maxidx, and sorts*)
datatype cterm =
  Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T};

exception CTERM of string * cterm list;

fun term_of (Cterm {t, ...}) = t;

fun typ_of_cterm (Cterm {T, ...}) = T;

fun ctyp_of_cterm (Cterm {cert, T, maxidx, sorts, ...}) =
  Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = sorts};

fun maxidx_of_cterm (Cterm {maxidx, ...}) = maxidx;

fun global_cterm_of thy tm =
  let
    val (t, T) = Sign.certify_term thy tm;
    val maxidx = Term.maxidx_of_term t;
    val sorts = Sorts.insert_term t [];
  in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;

val cterm_of = global_cterm_of o Proof_Context.theory_of;

fun join_certificate0 (Cterm {cert = cert1, ...}, Cterm {cert = cert2, ...}) =
  Context.join_certificate (cert1, cert2);

fun renamed_term t' (Cterm {cert, t, T, maxidx, sorts}) =
  if t aconv t' then Cterm {cert = cert, t = t', T = T, maxidx = maxidx, sorts = sorts}
  else raise TERM ("renamed_term: terms disagree", [t, t']);

val fast_term_ord = Term_Ord.fast_term_ord o apply2 term_of;
val term_ord = Term_Ord.term_ord o apply2 term_of;

(* destructors *)

fun dest_comb (Cterm {t = c $ a, T, cert, maxidx, sorts}) =
      let val A = Term.argument_type_of c 0 in
        (Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts},
         Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts})
      end
  | dest_comb ct = raise CTERM ("dest_comb", [ct]);

fun dest_fun (Cterm {t = c $ _, T, cert, maxidx, sorts}) =
      let val A = Term.argument_type_of c 0
      in Cterm {t = c, T = A --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
  | dest_fun ct = raise CTERM ("dest_fun", [ct]);

fun dest_arg (Cterm {t = c $ a, T = _, cert, maxidx, sorts}) =
      let val A = Term.argument_type_of c 0
      in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
  | dest_arg ct = raise CTERM ("dest_arg", [ct]);

fun dest_fun2 (Cterm {t = c $ _ $ _, T, cert, maxidx, sorts}) =
      let
        val A = Term.argument_type_of c 0;
        val B = Term.argument_type_of c 1;
      in Cterm {t = c, T = A --> B --> T, cert = cert, maxidx = maxidx, sorts = sorts} end
  | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]);

fun dest_arg1 (Cterm {t = c $ a $ _, T = _, cert, maxidx, sorts}) =
      let val A = Term.argument_type_of c 0
      in Cterm {t = a, T = A, cert = cert, maxidx = maxidx, sorts = sorts} end
  | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);

fun gen_dest_abs dest ct =
  (case ct of
    Cterm {t = t as Abs _, T = Type ("fun", [_, U]), cert, maxidx, sorts} =>
      let
        val ((x', T), t') = dest t;
        val v = Cterm {t = Free (x', T), T = T, cert = cert, maxidx = maxidx, sorts = sorts};
        val body = Cterm {t = t', T = U, cert = cert, maxidx = maxidx, sorts = sorts};
      in (v, body) end
  | _ => raise CTERM ("dest_abs", [ct]));

val dest_abs_fresh = gen_dest_abs o Term.dest_abs_fresh;
val dest_abs_global = gen_dest_abs Term.dest_abs_global;

(* constructors *)

fun rename_tvar (a, i) (Ctyp {cert, T, maxidx, sorts}) =
  let
    val S =
      (case T of
        TFree (_, S) => S
      | TVar (_, S) => S
      | _ => raise TYPE ("rename_tvar: no variable", [T], []));
    val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
  in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;

fun free (x, Ctyp {cert, T, maxidx, sorts}) =
  Cterm {cert = cert, t = Free (x, T), T = T, maxidx = maxidx, sorts = sorts};

fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) =
  if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
  else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};

fun apply
  (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
  (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
    if T = dty then
      Cterm {cert = join_certificate0 (cf, cx),
        t = f $ x,
        T = rty,
        maxidx = Int.max (maxidx1, maxidx2),
        sorts = Sorts.union sorts1 sorts2}
      else raise CTERM ("apply: types don't agree", [cf, cx])
  | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);

fun lambda_name
  (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
  (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
    let val t = Term.lambda_name (x, t1) t2 in
      Cterm {cert = join_certificate0 (ct1, ct2),
        t = t, T = T1 --> T2,
        maxidx = Int.max (maxidx1, maxidx2),
        sorts = Sorts.union sorts1 sorts2}
    end;

fun lambda t u = lambda_name ("", t) u;

(* indexes *)

fun adjust_maxidx_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) =
  if maxidx = i then ct
  else if maxidx < i then
    Cterm {maxidx = i, cert = cert, t = t, T = T, sorts = sorts}
  else
    Cterm {maxidx = Int.max (maxidx_of_term t, i), cert = cert, t = t, T = T, sorts = sorts};

fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) =
  if i < 0 then raise CTERM ("negative increment", [ct])
  else if i = 0 then ct
  else Cterm {cert = cert, t = Logic.incr_indexes ([], i) t,
    T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};

(*** Derivations and Theorems ***)

(* sort constraints *)

type constraint = {theory: theory, typ: typ, sort: sort};

local

val constraint_ord : constraint ord =
  Context.theory_id_ord o apply2 (Context.theory_id o #theory)
  ||| Term_Ord.typ_ord o apply2 #typ
  ||| Term_Ord.sort_ord o apply2 #sort;

val smash_atyps =
  map_atyps (fn TVar (_, S) => Term.aT S | TFree (_, S) => Term.aT S | T => T);

in

val union_constraints = Ord_List.union constraint_ord;

fun insert_constraints _ (_, []) = I
  | insert_constraints thy (T, S) =
      let
        val ignored =
          (case T of
            TFree (_, S') => S = S'
          | TVar (_, S') => S = S'
          | _ => false);
      in
        if ignored then I
        else Ord_List.insert constraint_ord {theory = thy, typ = smash_atyps T, sort = S}
      end;

fun insert_constraints_env thy env =
  let
    val tyenv = Envir.type_env env;
    val normT = Envir.norm_type tyenv;
    fun insert ([], _) = I
      | insert (S, T) = insert_constraints thy (normT T, S);
  in tyenv |> Vartab.fold (insert o #2) end;

end;

(* datatype thm *)

datatype thm = Thm of
deriv *                        (*derivation*)
{cert: Context.certificate,    (*background theory certificate*)
  tags: Properties.T,           (*additional annotations/comments*)
  maxidx: int,                  (*maximum index of any Var or TVar*)
  constraints: constraint Ord_List.T,  (*implicit proof obligations for sort constraints*)
  shyps: sort Ord_List.T,       (*sort hypotheses*)
  hyps: term Ord_List.T,        (*hypotheses*)
  tpairs: (term * term) list,   (*flex-flex pairs*)
  prop: term}                   (*conclusion*)
and deriv = Deriv of
{promises: (serial * thm future) Ord_List.T,
  body: Proofterm.proof_body};

type conv = cterm -> thm;

(*errors involving theorems*)
exception THM of string * int * thm list;

fun rep_thm (Thm (_, args)) = args;

fun fold_terms h f (Thm (_, {tpairs, prop, hyps, ...})) =
  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> #hyps h ? fold f hyps;

fun fold_atomic_ctyps h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
  let
    fun ctyp T = Ctyp {cert = cert, T = T, maxidx = maxidx, sorts = shyps};
    fun apply T a = if g a T then f (ctyp T) a else a;
  in (fold_terms h o fold_types o fold_atyps) apply th end;

fun fold_atomic_cterms h g f (th as Thm (_, {cert, maxidx, shyps, ...})) =
  let
    fun cterm t T = Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = shyps};
    fun apply t T a = if g a t then f (cterm t T) a else a;
  in
    (fold_terms h o fold_aterms)
      (fn t as Const (_, T) => apply t T
        | t as Free (_, T) => apply t T
        | t as Var (_, T) => apply t T
        | _ => I) th
  end;

fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];

fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
fun union_tpairs ts us = Library.merge eq_tpairs (ts, us);
val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);

fun attach_tpairs tpairs prop =
  Logic.list_implies (map Logic.mk_equals tpairs, prop);

fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;

val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;

fun join_certificate1 (Cterm {cert = cert1, ...}, Thm (_, {cert = cert2, ...})) =
  Context.join_certificate (cert1, cert2);

fun join_certificate2 (Thm (_, {cert = cert1, ...}), Thm (_, {cert = cert2, ...})) =
  Context.join_certificate (cert1, cert2);

(* basic components *)

val cert_of = #cert o rep_thm;
val theory_id = Context.certificate_theory_id o cert_of;

fun theory_name long = Context.theory_id_name long o theory_id;
val theory_long_name = theory_name {long = true};
val theory_base_name = theory_name {long = false};

val maxidx_of = #maxidx o rep_thm;
fun maxidx_thm th i = Int.max (maxidx_of th, i);
val shyps_of = #shyps o rep_thm;
val hyps_of = #hyps o rep_thm;
val prop_of = #prop o rep_thm;
val tpairs_of = #tpairs o rep_thm;

val concl_of = Logic.strip_imp_concl o prop_of;
val prems_of = Logic.strip_imp_prems o prop_of;
fun take_prems_of n = Logic.take_imp_prems n o prop_of;
val nprems_of = Logic.count_prems o prop_of;
val no_prems = Logic.no_prems o prop_of;
val one_prem = Logic.one_prem o prop_of;

fun prem_of th i =
  Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]);

fun major_prem_of th =
  (case take_prems_of 1 th of
    prem :: _ => Logic.strip_assums_concl prem
  | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));

fun cprop_of (Thm (_, {cert, maxidx, shyps, prop, ...})) =
  Cterm {cert = cert, maxidx = maxidx, T = propT, t = prop, sorts = shyps};

fun cprem_of (th as Thm (_, {cert, maxidx, shyps, prop, ...})) i =
  Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps,
    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};

fun cconcl_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
  Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = concl_of th};

fun cprems_of (th as Thm (_, {cert, maxidx, shyps, ...})) =
  map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
    (prems_of th);

fun take_cprems_of n (th as Thm (_, {cert, maxidx, shyps, ...})) =
  map (fn t => Cterm {cert = cert, maxidx = maxidx, T = propT, sorts = shyps, t = t})
    (take_prems_of n th);

fun chyps_of (Thm (_, {cert, shyps, hyps, ...})) =
  map (fn t => Cterm {cert = cert, maxidx = ~1, T = propT, sorts = shyps, t = t}) hyps;

(* thm order: ignores theory context! *)

val thm_ord =
  pointer_eq_ord
    (Term_Ord.fast_term_ord o apply2 prop_of
      ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of
      ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of
      ||| list_ord Term_Ord.sort_ord o apply2 shyps_of);

(* implicit theory context *)

exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option;

fun theory_of_cterm (ct as Cterm {cert, ...}) =
  Context.certificate_theory cert
    handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE);

fun theory_of_thm th =
  Context.certificate_theory (cert_of th)
    handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);

fun trim_context_ctyp cT =
  (case cT of
    Ctyp {cert = Context.Certificate_Id _, ...} => cT
  | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} =>
      Ctyp {cert = Context.Certificate_Id (Context.theory_id thy),
        T = T, maxidx = maxidx, sorts = sorts});

fun trim_context_cterm ct =
  (case ct of
    Cterm {cert = Context.Certificate_Id _, ...} => ct
  | Cterm {cert = Context.Certificate thy, t, T, maxidx, sorts} =>
      Cterm {cert = Context.Certificate_Id (Context.theory_id thy),
        t = t, T = T, maxidx = maxidx, sorts = sorts});

fun trim_context_thm th =
  (case th of
    Thm (_, {constraints = _ :: _, ...}) =>
      raise THM ("trim_context: pending sort constraints", 0, [th])
  | Thm (_, {cert = Context.Certificate_Id _, ...}) => th
  | Thm (der,
      {cert = Context.Certificate thy, tags, maxidx, constraints = [], shyps, hyps,
        tpairs, prop}) =>
      Thm (der,
       {cert = Context.Certificate_Id (Context.theory_id thy),
        tags = tags, maxidx = maxidx, constraints = [], shyps = shyps, hyps = hyps,
        tpairs = tpairs, prop = prop}));

fun transfer_ctyp thy' cT =
  let
    val Ctyp {cert, T, maxidx, sorts} = cT;
    val _ =
      Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
        raise CONTEXT ("Cannot transfer: not a super theory", [cT], [], [],
          SOME (Context.Theory thy'));
    val cert' = Context.join_certificate (Context.Certificate thy', cert);
  in
    if Context.eq_certificate (cert, cert') then cT
    else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts}
  end;

val transfer_ctyp' = transfer_ctyp o Proof_Context.theory_of;
val transfer_ctyp'' = transfer_ctyp o Context.theory_of;

fun transfer_cterm thy' ct =
  let
    val Cterm {cert, t, T, maxidx, sorts} = ct;
    val _ =
      Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
        raise CONTEXT ("Cannot transfer: not a super theory", [], [ct], [],
          SOME (Context.Theory thy'));
    val cert' = Context.join_certificate (Context.Certificate thy', cert);
  in
    if Context.eq_certificate (cert, cert') then ct
    else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts}
  end;

val transfer_cterm' = transfer_cterm o Proof_Context.theory_of;
val transfer_cterm'' = transfer_cterm o Context.theory_of;

fun transfer thy' th =
  let
    val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th;
    val _ =
      Context.subthy_id (Context.certificate_theory_id cert, Context.theory_id thy') orelse
        raise CONTEXT ("Cannot transfer: not a super theory", [], [], [th],
          SOME (Context.Theory thy'));
    val cert' = Context.join_certificate (Context.Certificate thy', cert);
  in
    if Context.eq_certificate (cert, cert') then th
    else
      Thm (der,
       {cert = cert',
        tags = tags,
        maxidx = maxidx,
        constraints = constraints,
        shyps = shyps,
        hyps = hyps,
        tpairs = tpairs,
        prop = prop})
  end;

val transfer' = transfer o Proof_Context.theory_of;
val transfer'' = transfer o Context.theory_of;

fun join_transfer thy th =
  (Context.subthy_id (theory_id th, Context.theory_id thy) ? transfer thy) th;

fun join_transfer_context (ctxt, th) =
  if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt))
  then (ctxt, transfer' ctxt th)
  else (Context.raw_transfer (theory_of_thm th) ctxt, th);

(* matching *)

local

fun gen_match match
    (ct1 as Cterm {t = t1, sorts = sorts1, ...},
     ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) =
  let
    val cert = join_certificate0 (ct1, ct2);
    val thy = Context.certificate_theory cert
      handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE);
    val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
    val sorts = Sorts.union sorts1 sorts2;
    fun mk_cTinst ((a, i), (S, T)) =
      (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts});
    fun mk_ctinst ((x, i), (U, t)) =
      let val T = Envir.subst_type Tinsts U in
        (((x, i), T), Cterm {t = t, T = T, cert = cert, maxidx = maxidx2, sorts = sorts})
      end;
  in
    (TVars.build (Vartab.fold (TVars.add o mk_cTinst) Tinsts),
     Vars.build (Vartab.fold (Vars.add o mk_ctinst) tinsts))
  end;

in

val match = gen_match Pattern.match;
val first_order_match = gen_match Pattern.first_order_match;

end;

(*implicit alpha-conversion*)
fun renamed_prop prop' (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
  if prop aconv prop' then
    Thm (der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps,
      hyps = hyps, tpairs = tpairs, prop = prop'})
  else raise TERM ("renamed_prop: props disagree", [prop, prop']);

fun make_context ths NONE cert =
      (Context.Theory (Context.certificate_theory cert)
        handle ERROR msg => raise CONTEXT (msg, [], [], ths, NONE))
  | make_context ths (SOME ctxt) cert =
      let
        val thy_id = Context.certificate_theory_id cert;
        val thy_id' = Context.theory_id (Proof_Context.theory_of ctxt);
      in
        if Context.subthy_id (thy_id, thy_id') then Context.Proof ctxt
        else raise CONTEXT ("Bad context", [], [], ths, SOME (Context.Proof ctxt))
      end;

fun make_context_certificate ths opt_ctxt cert =
  let
    val context = make_context ths opt_ctxt cert;
    val cert' = Context.Certificate (Context.theory_of context);
  in (context, cert') end;

(*explicit weakening: maps |- B to A |- B*)
fun weaken raw_ct th =
  let
    val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct;
    val Thm (der, {tags, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
  in
    if T <> propT then
      raise THM ("weaken: assumptions must have type prop", 0, [])
    else if maxidxA <> ~1 then
      raise THM ("weaken: assumptions may not contain schematic variables", maxidxA, [])
    else
      Thm (der,
       {cert = join_certificate1 (ct, th),
        tags = tags,
        maxidx = maxidx,
        constraints = constraints,
        shyps = Sorts.union sorts shyps,
        hyps = insert_hyps A hyps,
        tpairs = tpairs,
        prop = prop})
  end;

fun weaken_sorts raw_sorts ct =
  let
    val Cterm {cert, t, T, maxidx, sorts} = ct;
    val thy = theory_of_cterm ct;
    val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);
    val sorts' = Sorts.union sorts more_sorts;
  in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;

(** derivations and promised proofs **)

fun make_deriv0 promises body = Deriv {promises = promises, body = body};

fun make_deriv promises oracles thms zboxes zproof proof =
  make_deriv0 promises
    (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof});

val empty_deriv = make_deriv [] [] [] [] ZNop MinProof;

(* inference rules *)

val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);

fun deriv_rule2 zproof proof
    (Deriv {promises = ps1, body = PBody body1})
    (Deriv {promises = ps2, body = PBody body2}) =
  let
    val ps' = Ord_List.union promise_ord ps1 ps2;

    val {oracles = oracles1, thms = thms1, zboxes = zboxes1, zproof = zprf1, proof = prf1} = body1;
    val {oracles = oracles2, thms = thms2, zboxes = zboxes2, zproof = zprf2, proof = prf2} = body2;

    val oracles' = Proofterm.union_oracles oracles1 oracles2;
    val thms' = Proofterm.union_thms thms1 thms2;
    val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2;

    val proofs = Proofterm.get_proofs_level ();
    val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZNop;
    val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof;
  in make_deriv ps' oracles' thms' zboxes' zproof' proof' end;

fun deriv_rule1 zproof proof = deriv_rule2 (K zproof) (K proof) empty_deriv;

fun deriv_rule0 zproof proof =
  let val proofs = Proofterm.get_proofs_level () in
    if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
      deriv_rule1 I I (make_deriv [] [] [] []
       (if Proofterm.zproof_enabled proofs then zproof () else ZNop)
       (if Proofterm.proof_enabled proofs then proof () else MinProof))
    else empty_deriv
  end;

(* fulfilled proofs *)

fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;

fun join_promises [] = ()
  | join_promises promises = join_promises_of (Future.joins (map snd promises))
and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));

fun fulfill_body (th as Thm (Deriv {promises, body}, _)) =
  let val fulfilled_promises = map #1 promises ~~ map fulfill_body (Future.joins (map #2 promises))
  in Proofterm.fulfill_norm_proof (theory_of_thm th) fulfilled_promises body end;

fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
val proof_body_of = singleton proof_bodies_of;

val zproof_of = Proofterm.zproof_of o proof_body_of;
val proof_of = Proofterm.proof_of o proof_body_of;

fun reconstruct_proof_of thm =
  Proofterm.reconstruct_proof (theory_of_thm thm) (prop_of thm) (proof_of thm);

val consolidate = ignore o proof_bodies_of;

fun expose_proofs thy thms =
  if Proofterm.export_proof_boxes_required thy then
    Proofterm.export_proof_boxes (proof_bodies_of (map (transfer thy) thms))
  else ();

fun expose_proof thy = expose_proofs thy o single;

(* future rule *)

fun future_result i orig_cert orig_shyps orig_prop thm =
  let
    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
    val Thm (Deriv {promises, ...}, {cert, constraints, shyps, hyps, tpairs, prop, ...}) = thm;

    val _ = Context.eq_certificate (cert, orig_cert) orelse err "bad theory";
    val _ = prop aconv orig_prop orelse err "bad prop";
    val _ = null constraints orelse err "bad sort constraints";
    val _ = null tpairs orelse err "bad flex-flex constraints";
    val _ = null hyps orelse err "bad hyps";
    val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
    val _ = join_promises promises;
  in thm end;

fun future future_thm ct =
  let
    val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
    val _ =
      if Proofterm.any_proofs_enabled ()
      then raise CTERM ("future: proof terms enabled", [ct]) else ();

    val i = serial ();
    val future = future_thm |> Future.map (future_result i cert sorts prop);
  in
    Thm (make_deriv [(i, future)] [] [] [] ZNop MinProof,
     {cert = cert,
      tags = [],
      maxidx = maxidx,
      constraints = [],
      shyps = sorts,
      hyps = [],
      tpairs = [],
      prop = prop})
  end;

(** Axioms **)

fun axiom thy name =
  (case Name_Space.lookup (Theory.axiom_table thy) name of
    SOME prop =>
      let
        fun zproof () = ZTerm.axiom_proof thy name prop;
        fun proof () = Proofterm.axiom_proof name prop;
        val cert = Context.Certificate thy;
        val maxidx = maxidx_of_term prop;
        val shyps = Sorts.insert_term prop [];
      in
        Thm (deriv_rule0 zproof proof,
          {cert = cert, tags = [], maxidx = maxidx,
            constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop})
      end
  | NONE => raise THEORY ("No axiom " ^ quote name, [thy]));

fun all_axioms_of thy =
  map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy);

(* tags *)

val get_tags = #tags o rep_thm;

fun map_tags f (Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
  Thm (der, {cert = cert, tags = f tags, maxidx = maxidx, constraints = constraints,
    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});

(* technical adjustments *)

fun norm_proof (th as Thm (der, args)) =
  Thm (deriv_rule1 I (Proofterm.rew_proof (theory_of_thm th)) der, args);

fun adjust_maxidx_thm i
    (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
  if maxidx = i then th
  else if maxidx < i then
    Thm (der, {maxidx = i, cert = cert, tags = tags, constraints = constraints, shyps = shyps,
      hyps = hyps, tpairs = tpairs, prop = prop})
  else
    Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i),
      cert = cert, tags = tags, constraints = constraints, shyps = shyps,
      hyps = hyps, tpairs = tpairs, prop = prop});

(*** Theory data ***)

(* type classes *)

structure Aritytab =
  Table(
    type key = string * sort list * class;
    val ord =
      fast_string_ord o apply2 #1
      ||| fast_string_ord o apply2 #3
      ||| list_ord Term_Ord.sort_ord o apply2 #2;
  );

datatype classes = Classes of
{classrels: thm Symreltab.table,
  arities: (thm * string * serial) Aritytab.table};

fun make_classes (classrels, arities) = Classes {classrels = classrels, arities = arities};

val empty_classes = make_classes (Symreltab.empty, Aritytab.empty);

(*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
fun merge_classes
   (Classes {classrels = classrels1, arities = arities1},
    Classes {classrels = classrels2, arities = arities2}) =
  let
    val classrels' = Symreltab.merge (K true) (classrels1, classrels2);
    val arities' = Aritytab.merge (K true) (arities1, arities2);
  in make_classes (classrels', arities') end;

(* data *)

structure Data = Theory_Data
(
  type T =
    {name: Thm_Name.P, thm: thm} Inttab.table *  (*stored zproof thms*)
    unit Name_Space.table *  (*oracles: authentic derivation names*)
    classes;  (*type classes within the logic*)

  val empty : T = (Inttab.empty, Name_Space.empty_table Markup.oracleN, empty_classes);
  fun merge ((_, oracles1, sorts1), (_, oracles2, sorts2)) : T =
   (Inttab.empty,
    Name_Space.merge_tables (oracles1, oracles2),
    merge_classes (sorts1, sorts2));
);

val get_zproofs = #1 o Data.get;
fun map_zproofs f = Data.map (fn (a, b, c) => (f a, b, c));

val get_oracles = #2 o Data.get;
fun map_oracles f = Data.map (fn (a, b, c) => (a, f b, c));

val get_classes = (fn (_, _, Classes args) => args) o Data.get;
val get_classrels = #classrels o get_classes;
val get_arities = #arities o get_classes;

fun map_classes f =
  Data.map (fn (a, b, Classes {classrels, arities}) =>
    (a, b, make_classes (f (classrels, arities))));
fun map_classrels f = map_classes (fn (classrels, arities) => (f classrels, arities));
fun map_arities f = map_classes (fn (classrels, arities) => (classrels, f arities));

val _ =
  (Theory.setup o Theory.at_begin) (fn thy =>
    if Inttab.is_empty (get_zproofs thy) then NONE
    else SOME (map_zproofs (K Inttab.empty) thy));

(* type classes *)

fun the_classrel thy (c1, c2) =
  (case Symreltab.lookup (get_classrels thy) (c1, c2) of
    SOME thm => transfer thy thm
  | NONE => error ("Unproven class relation " ^
      Syntax.string_of_classrel (Proof_Context.init_global thy) [c1, c2]));

fun the_arity thy (a, Ss, c) =
  (case Aritytab.lookup (get_arities thy) (a, Ss, c) of
    SOME (thm, _, _) => transfer thy thm
  | NONE => error ("Unproven type arity " ^
      Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));

fun sorts_zproof thy = (zproof_of o the_classrel thy, zproof_of o the_arity thy);
fun sorts_proof thy = (proof_of o the_classrel thy, proof_of o the_arity thy);

(* solve sort constraints by pro-forma proof *)

local

fun union_digest (oracles1, thms1) (oracles2, thms2) =
  (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2);

fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) = (oracles, thms);

fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
  Sorts.of_sort_derivation (Sign.classes_of thy)
   {class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
      if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
    type_constructor = fn (a, _) => fn dom => fn c =>
      let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
      in (fold o fold) (union_digest o #1) dom arity_digest end,
    type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
   (typ, sort);

fun bad_constraint_theory cert ({theory = thy, ...}: constraint) =
  if Context.eq_thy_id (Context.certificate_theory_id cert, Context.theory_id thy)
  then NONE else SOME thy;

in

fun solve_constraints (thm as Thm (der, args)) =
  let
    val {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop} = args;

    val bad_thys = map_filter (bad_constraint_theory cert) constraints;
    val _ =
      if null bad_thys then ()
      else
        raise THEORY ("solve_constraints: bad theories for theorem\n" ^
          Syntax.string_of_term_global (hd bad_thys) (prop_of thm), bad_thys);

    val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
    val (oracles', thms') = (oracles, thms)
      |> fold (fold union_digest o constraint_digest) constraints;
    val zproof' = ZTerm.beta_norm_prooft zproof;
  in
    Thm (make_deriv promises oracles' thms' zboxes zproof' proof,
      {constraints = [], cert = cert, tags = tags, maxidx = maxidx,
        shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop})
  end;

end;

(*Dangling sort constraints of a thm*)
fun extra_shyps (th as Thm (_, {shyps, ...})) =
  Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps;

(*Remove extra sorts that are witnessed by type signature information*)
fun strip_shyps thm =
  (case thm of
    Thm (_, {shyps = [], ...}) => thm
  | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) =>
      let
        val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;

        val thy = theory_of_thm thm;
        val algebra = Sign.classes_of thy;
        val le = Sorts.sort_le algebra;
        fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
        fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];

        val present_set = Types.build (thm |> fold_terms {hyps = true} Types.add_atyps);
        val {present, extra} = Logic.present_sorts shyps present_set;

        val (witnessed, non_witnessed) =
          Sign.witness_sorts thy present extra ||> map (`(Sorts.minimize_sort algebra));

        val extra' =
          non_witnessed |> map_filter (fn (S, _) =>
            if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
          |> Sorts.make;

        val non_witnessed_constraints =
          non_witnessed |> maps (fn (S1, S2) =>
            let val S0 = the (find_first (fn S => le (S, S1)) extra')
            in rel (S0, S1) @ rel (S1, S2) end);

        val constraints' = constraints
          |> fold (insert_constraints thy) witnessed
          |> fold (insert_constraints thy) non_witnessed_constraints;

        val shyps' = fold (Sorts.insert_sort o #2) present extra';

        val types = present @ witnessed @ map (`Logic.dummy_tfree) extra';
        fun get_type S = types |> get_first (fn (T', S') => if le (S', S) then SOME T' else NONE);
        val map_atyp =
          Same.function_eq (op =) (fn T =>
            if Types.defined present_set T then raise Same.SAME
            else
              (case get_type (Type.sort_of_atyp T) of
                SOME T' => T'
              | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
        val map_ztyp =
          ZTypes.apply_unsynchronized_cache
            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));

        val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
        val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
      in
        Thm (make_deriv promises oracles thms zboxes zproof' proof',
         {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
          shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
      end)
  |> solve_constraints;

(*** Closed theorems with official name ***)

(*non-deterministic, depends on unknown promises*)
fun derivation_closed (Thm (Deriv {body, ...}, _)) =
  Proofterm.compact_proof (Proofterm.proof_of body);

(*non-deterministic, depends on unknown promises*)
fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
  Proofterm.get_approximative_name shyps hyps prop (Proofterm.proof_of body);

fun expand_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
  let
    val self_id =
      (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
        NONE => K false
      | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
    fun expand header =
      if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header))
      then SOME Thm_Name.none else NONE;
  in expand end;

(*deterministic name of finished proof*)
fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
  #1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm));

(*identified PThm node*)
fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
  Proofterm.get_id shyps hyps prop (proof_of thm);

(*dependencies of PThm node*)
fun thm_deps (thm as Thm (Deriv {promises = [], body = PBody {thms, ...}, ...}, _)) =
      (case (derivation_id thm, thms) of
        (SOME {serial = i, ...}, [(j, thm_node)]) =>
          if i = j then Proofterm.thm_node_thms thm_node else thms
      | _ => thms)
  | thm_deps thm = raise THM ("thm_deps: bad promises", 0, [thm]);

fun name_derivation name_pos =
  strip_shyps #> (fn thm as Thm (der, args) =>
    let
      val thy = theory_of_thm thm;

      val Deriv {promises, body} = der;
      val {shyps, hyps, prop, tpairs, ...} = args;

      val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);

      val ps = map (apsnd (Future.map fulfill_body)) promises;
      val body' = Proofterm.thm_proof thy (sorts_proof thy) name_pos shyps hyps prop ps body;
    in Thm (make_deriv0 [] body', args) end);

fun close_derivation pos =
  solve_constraints #> (fn thm =>
    if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
    else name_derivation (Thm_Name.empty, pos) thm);

val trim_context = solve_constraints #> trim_context_thm;

(*** Oracles ***)

fun add_oracle (b, oracle_fn) thy1 =
  let
    val (name, oracles') = Name_Space.define (Context.Theory thy1) true (b, ()) (get_oracles thy1);
    val thy2 = map_oracles (K oracles') thy1;
    val cert2 = Context.Certificate_Id (Context.theory_id thy2);
    fun invoke_oracle arg =
      let val ct as Cterm {cert = cert3, t = prop, T, maxidx, sorts} = oracle_fn arg in
        if T <> propT then
          raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
        else
          let
            val cert = Context.join_certificate (cert2, cert3);
            val proofs = Proofterm.get_proofs_level ();
            val oracle =
              if Proofterm.oracle_enabled proofs
              then ((name, Position.thread_data ()), SOME prop)
              else ((name, Position.none), NONE);
            val proof =
              if Proofterm.proof_enabled proofs
              then Proofterm.oracle_proof name prop
              else MinProof;
            val zproof =
              if Proofterm.zproof_enabled proofs then
                let
                  val thy = Context.certificate_theory cert handle ERROR msg =>
                    raise CONTEXT (msg, [], [ct], [], NONE);
                in ZTerm.oracle_proof thy name prop end
              else ZNop;
          in
            Thm (make_deriv [] [oracle] [] [] zproof proof,
             {cert = cert,
              tags = [],
              maxidx = maxidx,
              constraints = [],
              shyps = sorts,
              hyps = [],
              tpairs = [],
              prop = prop})
          end
      end;
  in ((name, invoke_oracle), thy2) end;

val oracle_space = Name_Space.space_of_table o get_oracles;

fun pretty_oracle ctxt =
  Name_Space.pretty ctxt (oracle_space (Proof_Context.theory_of ctxt));

fun extern_oracles verbose ctxt =
  map #1 (Name_Space.markup_table verbose ctxt (get_oracles (Proof_Context.theory_of ctxt)));

fun check_oracle ctxt =
  Name_Space.check (Context.Proof ctxt) (get_oracles (Proof_Context.theory_of ctxt)) #> #1;

(*** Meta rules ***)

(** primitive rules **)

(*The assumption rule A |- A*)
fun assume raw_ct =
  let val ct as Cterm {cert, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
    if T <> propT then
      raise THM ("assume: prop", 0, [])
    else if maxidx <> ~1 then
      raise THM ("assume: variables", maxidx, [])
    else
      let
        fun zproof () =
          let
            val thy = Context.certificate_theory cert handle ERROR msg =>
              raise CONTEXT (msg, [], [ct], [], NONE);
          in ZTerm.assume_proof thy prop end;
        fun proof () = Proofterm.Hyp prop;
      in
        Thm (deriv_rule0 zproof proof,
         {cert = cert,
          tags = [],
          maxidx = ~1,
          constraints = [],
          shyps = sorts,
          hyps = [prop],
          tpairs = [],
          prop = prop})
      end
  end;

fun assume_cterm A = assume A
  handle THM (msg, _, _) => raise CTERM (msg, [A]);

(*Implication introduction
    [A]
     :
     B
  -------
  A \<Longrightarrow> B
*)
fun implies_intr
    (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...})
    (th as Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...})) =
  if T <> propT then
    raise THM ("implies_intr: assumptions must have type prop", 0, [th])
  else
    let
      val cert = join_certificate1 (ct, th);
      fun zproof p =
        let
          val thy = Context.certificate_theory cert handle ERROR msg =>
            raise CONTEXT (msg, [], [ct], [th], NONE);
        in ZTerm.implies_intr_proof thy A p end
      fun proof p = Proofterm.implies_intr_proof A p;
    in
      Thm (deriv_rule1 zproof proof der,
       {cert = cert,
        tags = [],
        maxidx = Int.max (maxidx1, maxidx2),
        constraints = constraints,
        shyps = Sorts.union sorts shyps,
        hyps = remove_hyps A hyps,
        tpairs = tpairs,
        prop = Logic.mk_implies (A, prop)})
    end;

(*Implication elimination
  A \<Longrightarrow> B    A
  ------------
        B
*)
fun implies_elim thAB thA =
  let
    val Thm (derA,
      {maxidx = maxidx1, hyps = hypsA, constraints = constraintsA, shyps = shypsA,
        tpairs = tpairsA, prop = propA, ...}) = thA
    and Thm (der, {maxidx = maxidx2, hyps, constraints, shyps, tpairs, prop, ...}) = thAB;
    fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
  in
    (case prop of
      Const ("Pure.imp", _) $ A $ B =>
        if A aconv propA then
          Thm (deriv_rule2 (curry ZAppp) (curry Proofterm.%%) der derA,
           {cert = join_certificate2 (thAB, thA),
            tags = [],
            maxidx = Int.max (maxidx1, maxidx2),
            constraints = union_constraints constraintsA constraints,
            shyps = Sorts.union shypsA shyps,
            hyps = union_hyps hypsA hyps,
            tpairs = union_tpairs tpairsA tpairs,
            prop = B})
        else err ()
    | _ => err ())
  end;

(*Forall introduction.  The Free or Var x must not be free in the hypotheses.
    [x]
     :
     A
  ------
  \<And>x. A
*)
fun occs x ts tpairs =
  let fun occs t = Logic.occs (x, t)
  in exists occs ts orelse exists (occs o fst) tpairs orelse exists (occs o snd) tpairs end;

fun forall_intr
    (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
    (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
  let
    fun check_result a ts =
      if occs x ts tpairs then
        raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
      else
        let
          val cert = join_certificate1 (ct, th);
          fun zproof p =
            let
              val thy = Context.certificate_theory cert handle ERROR msg =>
                raise CONTEXT (msg, [], [ct], [th], NONE);
            in ZTerm.forall_intr_proof thy T (a, x) p end;
          fun proof p = Proofterm.forall_intr_proof (a, x) NONE p;
        in
          Thm (deriv_rule1 zproof proof der,
           {cert = cert,
            tags = [],
            maxidx = Int.max (maxidx1, maxidx2),
            constraints = constraints,
            shyps = Sorts.union sorts shyps,
            hyps = hyps,
            tpairs = tpairs,
            prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))})
        end;
  in
    (case x of
      Free (a, _) => check_result a hyps
    | Var ((a, _), _) => check_result a []
    | _ => raise THM ("forall_intr: not a variable", 0, [th]))
  end;

(*Forall elimination
  \<And>x. A
  ------
  A[t/x]
*)
fun forall_elim
    (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...})
    (th as Thm (der, {maxidx = maxidx2, constraints, shyps, hyps, tpairs, prop, ...})) =
  (case prop of
    Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
      if T <> qary then
        raise THM ("forall_elim: type mismatch", 0, [th])
      else
        let
          val cert = join_certificate1 (ct, th);
          fun zproof p =
            let
              val thy = Context.certificate_theory cert handle ERROR msg =>
                raise CONTEXT (msg, [], [ct], [th], NONE);
            in ZTerm.forall_elim_proof thy t p end;
          fun proof p = p % SOME t;
        in
          Thm (deriv_rule1 zproof proof der,
           {cert = cert,
            tags = [],
            maxidx = Int.max (maxidx1, maxidx2),
            constraints = constraints,
            shyps = Sorts.union sorts shyps,
            hyps = hyps,
            tpairs = tpairs,
            prop = Term.betapply (A, t)})
        end
  | _ => raise THM ("forall_elim: not quantified", 0, [th]));

(* Equality *)

(*Reflexivity
  t \<equiv> t
*)
fun reflexive (ct as Cterm {cert, t, T, maxidx, sorts}) =
  let
    fun zproof () =
      let
        val thy = Context.certificate_theory cert handle ERROR msg =>
          raise CONTEXT (msg, [], [ct], [], NONE);
      in ZTerm.reflexive_proof thy T t end;
    fun proof () = Proofterm.reflexive_proof;
  in
    Thm (deriv_rule0 zproof proof,
     {cert = cert,
      tags = [],
      maxidx = maxidx,
      constraints = [],
      shyps = sorts,
      hyps = [],
      tpairs = [],
      prop = Logic.mk_equals (t, t)})
  end;

(*Symmetry
  t \<equiv> u
  ------
  u \<equiv> t
*)
fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
  (case prop of
    (eq as Const ("Pure.eq", Type ("fun", [T, _]))) $ t $ u =>
      let
        fun zproof p =
          let
            val thy = Context.certificate_theory cert handle ERROR msg =>
              raise CONTEXT (msg, [], [], [th], NONE);
          in ZTerm.symmetric_proof thy T t u p end;
      in
        Thm (deriv_rule1 zproof Proofterm.symmetric_proof der,
         {cert = cert,
          tags = [],
          maxidx = maxidx,
          constraints = constraints,
          shyps = shyps,
          hyps = hyps,
          tpairs = tpairs,
          prop = eq $ u $ t})
      end
    | _ => raise THM ("symmetric", 0, [th]));

(*Transitivity
  t1 \<equiv> u    u \<equiv> t2
  ------------------
       t1 \<equiv> t2
*)
fun transitive th1 th2 =
  let
    val Thm (der1, {maxidx = maxidx1, hyps = hyps1, constraints = constraints1, shyps = shyps1,
        tpairs = tpairs1, prop = prop1, ...}) = th1
    and Thm (der2, {maxidx = maxidx2, hyps = hyps2, constraints = constraints2, shyps = shyps2,
        tpairs = tpairs2, prop = prop2, ...}) = th2;
    fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
  in
    case (prop1, prop2) of
      ((eq as Const ("Pure.eq", Type (_, [T, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
        if not (u aconv u') then err "middle term"
        else
          let
            val cert = join_certificate2 (th1, th2);
            fun zproof p q =
              let
                val thy = Context.certificate_theory cert handle ERROR msg =>
                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
              in ZTerm.transitive_proof thy T t1 u t2 p q end;
            fun proof p = Proofterm.transitive_proof T u p;
          in
            Thm (deriv_rule2 zproof proof der1 der2,
             {cert = cert,
              tags = [],
              maxidx = Int.max (maxidx1, maxidx2),
              constraints = union_constraints constraints1 constraints2,
              shyps = Sorts.union shyps1 shyps2,
              hyps = union_hyps hyps1 hyps2,
              tpairs = union_tpairs tpairs1 tpairs2,
              prop = eq $ t1 $ t2})
          end
     | _ => err "premises"
  end;

(*Beta-conversion
  (\<lambda>x. t) u \<equiv> t[u/x]
  fully beta-reduces the term if full = true
*)
fun beta_conversion full (ct as Cterm {cert, t, T, maxidx, sorts}) =
  let
    val t' =
      if full then Envir.beta_norm t
      else
        (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
        | _ => raise THM ("beta_conversion: not a redex", 0, []));
    fun zproof () =
      let
        val thy = Context.certificate_theory cert handle ERROR msg =>
          raise CONTEXT (msg, [], [ct], [], NONE);
      in ZTerm.reflexive_proof thy T t end;
    fun proof () = Proofterm.reflexive_proof;
  in
    Thm (deriv_rule0 zproof proof,
     {cert = cert,
      tags = [],
      maxidx = maxidx,
      constraints = [],
      shyps = sorts,
      hyps = [],
      tpairs = [],
      prop = Logic.mk_equals (t, t')})
  end;

fun eta_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) =
  let
    fun zproof () =
      let
        val thy = Context.certificate_theory cert handle ERROR msg =>
          raise CONTEXT (msg, [], [ct], [], NONE);
      in ZTerm.reflexive_proof thy T t end;
    fun proof () = Proofterm.reflexive_proof;
  in
    Thm (deriv_rule0 zproof proof,
     {cert = cert,
      tags = [],
      maxidx = maxidx,
      constraints = [],
      shyps = sorts,
      hyps = [],
      tpairs = [],
      prop = Logic.mk_equals (t, Envir.eta_contract t)})
  end;

fun eta_long_conversion (ct as Cterm {cert, t, T, maxidx, sorts}) =
  let
    fun zproof () =
      let
        val thy = Context.certificate_theory cert handle ERROR msg =>
          raise CONTEXT (msg, [], [ct], [], NONE);
      in ZTerm.reflexive_proof thy T t end;
    fun proof () = Proofterm.reflexive_proof;
  in
    Thm (deriv_rule0 zproof proof,
     {cert = cert,
      tags = [],
      maxidx = maxidx,
      constraints = [],
      shyps = sorts,
      hyps = [],
      tpairs = [],
      prop = Logic.mk_equals (t, Envir.eta_long [] t)})
  end;

(*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
  The bound variable will be named "a" (since x will be something like x320)
      t \<equiv> u
  --------------
  \<lambda>x. t \<equiv> \<lambda>x. u
*)
fun abstract_rule b
    (ct as Cterm {t = x, T, sorts, ...})
    (th as Thm (der, {cert, maxidx, hyps, constraints, shyps, tpairs, prop, ...})) =
  let
    val (U, t, u) =
      (case prop of
        Const ("Pure.eq", Type ("fun", [U, _])) $ t $ u => (U, t, u)
      | _ => raise THM ("abstract_rule: premise not an equality", 0, [th]));
    fun check_result a ts =
      if occs x ts tpairs then
        raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
      else
        let
          val f = Abs (b, T, abstract_over (x, t));
          val g = Abs (b, T, abstract_over (x, u));
          fun zproof p =
            let
              val thy = Context.certificate_theory cert handle ERROR msg =>
                raise CONTEXT (msg, [], [ct], [th], NONE);
            in ZTerm.abstract_rule_proof thy T U (b, x) f g p end;
          fun proof p = Proofterm.abstract_rule_proof (b, x) p
        in
          Thm (deriv_rule1 zproof proof der,
           {cert = cert,
            tags = [],
            maxidx = maxidx,
            constraints = constraints,
            shyps = Sorts.union sorts shyps,
            hyps = hyps,
            tpairs = tpairs,
            prop = Logic.mk_equals (f, g)})
        end;
  in
    (case x of
      Free (a, _) => check_result a hyps
    | Var ((a, _), _) => check_result a []
    | _ => raise THM ("abstract_rule: not a variable", 0, [th]))
  end;

(*The combination rule
  f \<equiv> g  t \<equiv> u
  -------------
    f t \<equiv> g u
*)
fun combination th1 th2 =
  let
    val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
        hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
    and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
        hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
  in
    (case (prop1, prop2) of
      (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
       Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
        let
          val U =
            (case fT of
              Type ("fun", [T1, U]) =>
                if T1 = tT then U
                else raise THM ("combination: types", 0, [th1, th2])
            | _ => raise THM ("combination: not function type", 0, [th1, th2]));
          val cert = join_certificate2 (th1, th2);
          fun zproof p q =
            let
              val thy = Context.certificate_theory cert handle ERROR msg =>
                raise CONTEXT (msg, [], [], [th1, th2], NONE);
            in ZTerm.combination_proof thy fT U f g t u p q end;
          fun proof p q = Proofterm.combination_proof f g t u p q;
        in
          Thm (deriv_rule2 zproof proof der1 der2,
           {cert = cert,
            tags = [],
            maxidx = Int.max (maxidx1, maxidx2),
            constraints = union_constraints constraints1 constraints2,
            shyps = Sorts.union shyps1 shyps2,
            hyps = union_hyps hyps1 hyps2,
            tpairs = union_tpairs tpairs1 tpairs2,
            prop = Logic.mk_equals (f $ t, g $ u)})
        end
     | _ => raise THM ("combination: premises", 0, [th1, th2]))
  end;

(*Equality introduction
  A \<Longrightarrow> B  B \<Longrightarrow> A
  ----------------
       A \<equiv> B
*)
fun equal_intr th1 th2 =
  let
    val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
      hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
    and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
      hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
    fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
  in
    (case (prop1, prop2) of
      (Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
        if A aconv A' andalso B aconv B' then
          let
            val cert = join_certificate2 (th1, th2);
            fun proof p q = Proofterm.equal_intr_proof A B p q;
            fun zproof p q =
              let
                val thy = Context.certificate_theory cert handle ERROR msg =>
                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
              in ZTerm.equal_intr_proof thy A B p q end;
          in
            Thm (deriv_rule2 zproof proof der1 der2,
             {cert = cert,
              tags = [],
              maxidx = Int.max (maxidx1, maxidx2),
              constraints = union_constraints constraints1 constraints2,
              shyps = Sorts.union shyps1 shyps2,
              hyps = union_hyps hyps1 hyps2,
              tpairs = union_tpairs tpairs1 tpairs2,
              prop = Logic.mk_equals (A, B)})
          end
        else err "not equal"
    | _ =>  err "premises")
  end;

(*The equal propositions rule
  A \<equiv> B  A
  ---------
      B
*)
fun equal_elim th1 th2 =
  let
    val Thm (der1, {maxidx = maxidx1, constraints = constraints1, shyps = shyps1,
      hyps = hyps1, tpairs = tpairs1, prop = prop1, ...}) = th1
    and Thm (der2, {maxidx = maxidx2, constraints = constraints2, shyps = shyps2,
      hyps = hyps2, tpairs = tpairs2, prop = prop2, ...}) = th2;
    fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
  in
    (case prop1 of
      Const ("Pure.eq", _) $ A $ B =>
        if prop2 aconv A then
          let
            val cert = join_certificate2 (th1, th2);
            fun proof p q = Proofterm.equal_elim_proof A B p q;
            fun zproof p q =
              let
                val thy = Context.certificate_theory cert handle ERROR msg =>
                  raise CONTEXT (msg, [], [], [th1, th2], NONE);
              in ZTerm.equal_elim_proof thy A B p q end;
          in
            Thm (deriv_rule2 zproof proof der1 der2,
             {cert = cert,
              tags = [],
              maxidx = Int.max (maxidx1, maxidx2),
              constraints = union_constraints constraints1 constraints2,
              shyps = Sorts.union shyps1 shyps2,
              hyps = union_hyps hyps1 hyps2,
              tpairs = union_tpairs tpairs1 tpairs2,
              prop = B})
          end
        else err "not equal"
     | _ =>  err "major premise")
  end;

(**** Derived rules ****)

(*Smash unifies the list of term pairs leaving no flex-flex pairs.
  Instantiates the theorem and deletes trivial tpairs.  Resulting
  sequence may contain multiple elements if the tpairs are not all
  flex-flex.*)
fun flexflex_rule opt_ctxt =
  solve_constraints #> (fn th =>
    let
      val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
      val (context, cert') = make_context_certificate [th] opt_ctxt cert;
    in
      Unify.smash_unifiers context tpairs (Envir.empty maxidx)
      |> Seq.map (fn env =>
          if Envir.is_empty env then th
          else
            let
              val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
                (*remove trivial tpairs, of the form t \<equiv> t*)
                |> filter_out (op aconv);
              val prop' = Envir.norm_term env prop;
              val thy' = Context.certificate_theory cert' handle ERROR msg =>
                raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);

              fun zproof p = ZTerm.norm_proof thy' env [full_prop_of th] p;
              fun proof p = Proofterm.norm_proof_remove_types env p;
            in
              Thm (deriv_rule1 zproof proof der,
               {cert = cert',
                tags = [],
                maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
                constraints = insert_constraints_env thy' env constraints,
                shyps = Envir.insert_sorts env shyps,
                hyps = hyps,
                tpairs = tpairs',
                prop = prop'})
            end)
    end);

(*Generalization of fixed variables
           A
  --------------------
  A[?'a/'a, ?x/x, ...]
*)

fun generalize (tfrees, frees) idx th =
  if Names.is_empty tfrees andalso Names.is_empty frees then th
  else
    let
      val Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...}) = th;
      val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);

      val bad_type =
        if Names.is_empty tfrees then K false
        else Term.exists_subtype (fn TFree (a, _) => Names.defined tfrees a | _ => false);
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.42 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.