(*  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, framework rules (including lifting and

resolution), oracles.

*)

signature BASIC_THM =

  sig

  (*certified types*)

  type ctyp

  val rep_ctyp: ctyp ->

   {thy_ref: theory_ref,

    T: typ,

    maxidx: int,

    sorts: sort Ord_List.T}

  val theory_of_ctyp: ctyp -> theory

  val typ_of: ctyp -> typ

  val ctyp_of: theory -> typ -> ctyp

  (*certified terms*)

  type cterm

  exception CTERM of string * cterm list

  val rep_cterm: cterm ->

   {thy_ref: theory_ref,

    t: term,

    T: typ,

    maxidx: int,

    sorts: sort Ord_List.T}

  val crep_cterm: cterm ->

    {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}

  val theory_of_cterm: cterm -> theory

  val term_of: cterm -> term

  val cterm_of: theory -> term -> cterm

  val ctyp_of_term: cterm -> ctyp

  (*theorems*)

  type thm

  type conv = cterm -> thm

  val rep_thm: thm ->

   {thy_ref: theory_ref,

    tags: Properties.T,

    maxidx: int,

    shyps: sort Ord_List.T,

    hyps: term Ord_List.T,

    tpairs: (term * term) list,

    prop: term}

  val crep_thm: thm ->

   {thy_ref: theory_ref,

    tags: Properties.T,

    maxidx: int,

    shyps: sort Ord_List.T,

    hyps: cterm Ord_List.T,

    tpairs: (cterm * cterm) list,

    prop: cterm}

  exception THM of string * int * thm list

  val theory_of_thm: thm -> theory

  val prop_of: thm -> term

  val concl_of: thm -> term

  val prems_of: thm -> term list

  val nprems_of: thm -> int

  val cprop_of: thm -> cterm

  val cprem_of: thm -> int -> cterm

end;

signature THM =

sig

  include BASIC_THM

  val dest_ctyp: ctyp -> ctyp list

  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: string option -> cterm -> cterm * cterm

  val capply: cterm -> cterm -> cterm

  val cabs_name: string * cterm -> cterm -> cterm

  val cabs: cterm -> cterm -> cterm

  val adjust_maxidx_cterm: int -> cterm -> cterm

  val incr_indexes_cterm: int -> cterm -> cterm

  val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list

  val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list

  val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a

  val terms_of_tpairs: (term * term) list -> term list

  val full_prop_of: thm -> term

  val maxidx_of: thm -> int

  val maxidx_thm: thm -> int -> int

  val hyps_of: thm -> term list

  val tpairs_of: thm -> (term * term) list

  val no_prems: thm -> bool

  val major_prem_of: thm -> term

  val transfer: theory -> thm -> thm

  val weaken: cterm -> thm -> thm

  val weaken_sorts: sort list -> cterm -> cterm

  val extra_shyps: thm -> sort list

  val join_proofs: thm list -> unit

  val proof_body_of: thm -> proof_body

  val proof_of: thm -> proof

  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}

  val future: thm future -> cterm -> thm

  val derivation_name: thm -> string

  val name_derivation: string -> thm -> thm

  val axiom: theory -> string -> thm

  val 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

  (*meta rules*)

  val assume: cterm -> thm

  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 flexflex_rule: thm -> thm Seq.seq

  val generalize: string list * string list -> int -> thm -> thm

  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm

  val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm

  val trivial: cterm -> thm

  val of_class: ctyp * class -> thm

  val strip_shyps: thm -> thm

  val unconstrainT: thm -> thm

  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm

  val varifyT_global: thm -> thm

  val legacy_freezeT: thm -> thm

  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: 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 rename_params_rule: string list * int -> thm -> thm

  val rename_boundvars: term -> term -> thm -> thm

  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq

  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq

  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq

  val extern_oracles: Proof.context -> xstring list

  val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory

end;

structure Thm: THM =

struct

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

(** certified types **)

abstype ctyp = Ctyp of

 {thy_ref: theory_ref,

  T: typ,

  maxidx: int,

  sorts: sort Ord_List.T}

with

fun rep_ctyp (Ctyp args) = args;

fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;

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

fun 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 {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end;

fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) =

      map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts

  | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);

(** certified terms **)

(*certified terms with checked typ, maxidx, and sorts*)

abstype cterm = Cterm of

 {thy_ref: theory_ref,

  t: term,

  T: typ,

  maxidx: int,

  sorts: sort Ord_List.T}

with

exception CTERM of string * cterm list;

fun rep_cterm (Cterm args) = args;

fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =

  {thy_ref = thy_ref, t = t, maxidx = maxidx, sorts = sorts,

    T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}};

fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;

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

fun ctyp_of_term (Cterm {thy_ref, T, maxidx, sorts, ...}) =

  Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts};

fun cterm_of thy tm =

  let

    val (t, T, maxidx) = Sign.certify_term thy tm;

    val sorts = Sorts.insert_term t [];

  in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;

fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =

  Theory.merge_refs (r1, r2);

(* destructors *)

fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =

      let val A = Term.argument_type_of c 0 in

        (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},

         Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})

      end

  | dest_comb ct = raise CTERM ("dest_comb", [ct]);

fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =

      let val A = Term.argument_type_of c 0

      in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end

  | dest_fun ct = raise CTERM ("dest_fun", [ct]);

fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =

      let val A = Term.argument_type_of c 0

      in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end

  | dest_arg ct = raise CTERM ("dest_arg", [ct]);

fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, 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, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end

  | dest_fun2 ct = raise CTERM ("dest_fun2", [ct]);

fun dest_arg1 (Cterm {t = c $ a $ _, T = _, thy_ref, maxidx, sorts}) =

      let val A = Term.argument_type_of c 0

      in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end

  | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);

fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =

      let val (y', t') = Term.dest_abs (the_default x a, T, t) in

        (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},

          Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})

      end

  | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);

(* constructors *)

fun capply

  (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 {thy_ref = merge_thys0 cf cx,

        t = f $ x,

        T = rty,

        maxidx = Int.max (maxidx1, maxidx2),

        sorts = Sorts.union sorts1 sorts2}

      else raise CTERM ("capply: types don't agree", [cf, cx])

  | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);

fun cabs_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 {thy_ref = merge_thys0 ct1 ct2,

        t = t, T = T1 --> T2,

        maxidx = Int.max (maxidx1, maxidx2),

        sorts = Sorts.union sorts1 sorts2}

    end;

fun cabs t u = cabs_name ("", t) u;

(* indexes *)

fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =

  if maxidx = i then ct

  else if maxidx < i then

    Cterm {maxidx = i, thy_ref = thy_ref, t = t, T = T, sorts = sorts}

  else

    Cterm {maxidx = Int.max (maxidx_of_term t, i), thy_ref = thy_ref, t = t, T = T, sorts = sorts};

fun incr_indexes_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =

  if i < 0 then raise CTERM ("negative increment", [ct])

  else if i = 0 then ct

  else Cterm {thy_ref = thy_ref, t = Logic.incr_indexes ([], i) t,

    T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};

(* matching *)

local

fun gen_match match

    (ct1 as Cterm {t = t1, sorts = sorts1, ...},

     ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) =

  let

    val thy = Theory.deref (merge_thys0 ct1 ct2);

    val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);

    val sorts = Sorts.union sorts1 sorts2;

    fun mk_cTinst ((a, i), (S, T)) =

      (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts},

       Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts});

    fun mk_ctinst ((x, i), (T, t)) =

      let val T = Envir.subst_type Tinsts T in

        (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy,

          maxidx = i, sorts = sorts},

         Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts})

      end;

  in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;

in

val match = gen_match Pattern.match;

val first_order_match = gen_match Pattern.first_order_match;

end;

(*** Derivations and Theorems ***)

abstype thm = Thm of

 deriv *                        (*derivation*)

 {thy_ref: theory_ref,          (*dynamic reference to theory*)

  tags: Properties.T,           (*additional annotations/comments*)

  maxidx: int,                  (*maximum index of any Var or TVar*)

  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}

with

type conv = cterm -> thm;

(*errors involving theorems*)

exception THM of string * int * thm list;

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

fun crep_thm (Thm (_, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =

  let fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps} in

   {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps,

    hyps = map (cterm ~1) hyps,

    tpairs = map (pairself (cterm maxidx)) tpairs,

    prop = cterm maxidx prop}

  end;

fun fold_terms f (Thm (_, {tpairs, prop, hyps, ...})) =

  fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps;

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;

(* merge theories of cterms/thms -- trivial absorption only *)

fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) =

  Theory.merge_refs (r1, r2);

fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) =

  Theory.merge_refs (r1, r2);

(* basic components *)

val theory_of_thm = Theory.deref o #thy_ref o rep_thm;

val maxidx_of = #maxidx o rep_thm;

fun maxidx_thm th i = Int.max (maxidx_of th, i);

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;

val nprems_of = Logic.count_prems o prop_of;

fun no_prems th = nprems_of th = 0;

fun major_prem_of th =

  (case prems_of th of

    prem :: _ => Logic.strip_assums_concl prem

  | [] => raise THM ("major_prem_of: rule with no premises", 0, [th]));

(*the statement of any thm is a cterm*)

fun cprop_of (Thm (_, {thy_ref, maxidx, shyps, prop, ...})) =

  Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps};

fun cprem_of (th as Thm (_, {thy_ref, maxidx, shyps, prop, ...})) i =

  Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps,

    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};

(*explicit transfer to a super theory*)

fun transfer thy' thm =

  let

    val Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop}) = thm;

    val thy = Theory.deref thy_ref;

    val _ = Theory.subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]);

    val is_eq = Theory.eq_thy (thy, thy');

    val _ = Theory.check_thy thy;

  in

    if is_eq then thm

    else

      Thm (der,

       {thy_ref = Theory.check_thy thy',

        tags = tags,

        maxidx = maxidx,

        shyps = shyps,

        hyps = hyps,

        tpairs = tpairs,

        prop = prop})

  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, 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,

       {thy_ref = merge_thys1 ct th,

        tags = tags,

        maxidx = maxidx,

        shyps = Sorts.union sorts shyps,

        hyps = insert_hyps A hyps,

        tpairs = tpairs,

        prop = prop})

  end;

fun weaken_sorts raw_sorts ct =

  let

    val Cterm {thy_ref, t, T, maxidx, sorts} = ct;

    val thy = Theory.deref thy_ref;

    val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts);

    val sorts' = Sorts.union sorts more_sorts;

  in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts'} end;

(*dangling sort constraints of a thm*)

fun extra_shyps (th as Thm (_, {shyps, ...})) =

  Sorts.subtract (fold_terms Sorts.insert_term th []) shyps;

(** derivations and promised proofs **)

fun make_deriv promises oracles thms proof =

  Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};

val empty_deriv = make_deriv [] [] [] Proofterm.MinProof;

(* inference rules *)

fun promise_ord ((i, _), (j, _)) = int_ord (j, i);

fun deriv_rule2 f

    (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})

    (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =

  let

    val ps = Ord_List.union promise_ord ps1 ps2;

    val oras = Proofterm.merge_oracles oras1 oras2;

    val thms = Proofterm.merge_thms thms1 thms2;

    val prf =

      (case ! Proofterm.proofs of

        2 => f prf1 prf2

      | 1 => MinProof

      | 0 => MinProof

      | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));

  in make_deriv ps oras thms prf end;

fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;

fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);

fun deriv_rule_unconditional f (Deriv {promises, body = PBody {oracles, thms, proof}}) =

  make_deriv promises oracles thms (f proof);

(* fulfilled proofs *)

fun raw_body (Thm (Deriv {body, ...}, _)) = body;

fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =

  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)

    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body

and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));

val join_proofs = Proofterm.join_bodies o map fulfill_body;

fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);

val proof_of = Proofterm.proof_of o proof_body_of;

(* derivation status *)

fun status_of (Thm (Deriv {promises, body}, _)) =

  let

    val ps = map (Future.peek o snd) promises;

    val bodies = body ::

      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;

    val {oracle, unfinished, failed} = Proofterm.status_of bodies;

  in

   {oracle = oracle,

    unfinished = unfinished orelse exists is_none ps,

    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}

  end;

(* future rule *)

fun future_result i orig_thy orig_shyps orig_prop thm =

  let

    fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);

    val Thm (Deriv {promises, ...}, {thy_ref, shyps, hyps, tpairs, prop, ...}) = thm;

    val _ = Theory.eq_thy (Theory.deref thy_ref, orig_thy) orelse err "bad theory";

    val _ = Theory.check_thy orig_thy;

    val _ = prop aconv orig_prop orelse err "bad prop";

    val _ = null tpairs orelse err "bad tpairs";

    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 _ = fulfill_bodies (map #2 promises);

  in thm end;

fun future future_thm ct =

  let

    val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;

    val thy = Context.reject_draft (Theory.deref thy_ref);

    val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);

    val i = serial ();

    val future = future_thm |> Future.map (future_result i thy sorts prop);

  in

    Thm (make_deriv [(i, future)] [] [] (Proofterm.promise_proof thy i prop),

     {thy_ref = thy_ref,

      tags = [],

      maxidx = maxidx,

      shyps = sorts,

      hyps = [],

      tpairs = [],

      prop = prop})

  end;

(* closed derivations with official name *)

(*non-deterministic, depends on unknown promises*)

fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =

  Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);

fun name_derivation name (thm as Thm (der, args)) =

  let

    val Deriv {promises, body} = der;

    val {thy_ref, shyps, hyps, prop, tpairs, ...} = args;

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

    val ps = map (apsnd (Future.map fulfill_body)) promises;

    val thy = Theory.deref thy_ref;

    val (pthm, proof) = Proofterm.thm_proof thy name shyps hyps prop ps body;

    val der' = make_deriv [] [] [pthm] proof;

    val _ = Theory.check_thy thy;

  in Thm (der', args) end;

(** Axioms **)

fun axiom theory name =

  let

    fun get_ax thy =

      Symtab.lookup (Theory.axiom_table thy) name

      |> Option.map (fn prop =>

           let

             val der = deriv_rule0 (Proofterm.axm_proof name prop);

             val maxidx = maxidx_of_term prop;

             val shyps = Sorts.insert_term prop [];

           in

             Thm (der, {thy_ref = Theory.check_thy thy, tags = [],

               maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop})

           end);

  in

    (case get_first get_ax (Theory.nodes_of theory) of

      SOME thm => thm

    | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))

  end;

(*return additional axioms of this theory node*)

fun axioms_of thy =

  map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));

(* tags *)

val get_tags = #tags o rep_thm;

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

  Thm (der, {thy_ref = thy_ref, tags = f tags, maxidx = maxidx,

    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});

fun norm_proof (Thm (der, args as {thy_ref, ...})) =

  let

    val thy = Theory.deref thy_ref;

    val der' = deriv_rule1 (Proofterm.rew_proof thy) der;

    val _ = Theory.check_thy thy;

  in Thm (der', args) end;

fun adjust_maxidx_thm i (th as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =

  if maxidx = i then th

  else if maxidx < i then

    Thm (der, {maxidx = i, thy_ref = thy_ref, tags = tags, shyps = shyps,

      hyps = hyps, tpairs = tpairs, prop = prop})

  else

    Thm (der, {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref,

      tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop});

(*** Meta rules ***)

(** primitive rules **)

(*The assumption rule A |- A*)

fun assume raw_ct =

  let val Cterm {thy_ref, 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 Thm (deriv_rule0 (Proofterm.Hyp prop),

     {thy_ref = thy_ref,

      tags = [],

      maxidx = ~1,

      shyps = sorts,

      hyps = [prop],

      tpairs = [],

      prop = prop})

  end;

(*Implication introduction

    [A]

     :

     B

  -------

  A ==> B

*)

fun implies_intr

    (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})

    (th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) =

  if T <> propT then

    raise THM ("implies_intr: assumptions must have type prop", 0, [th])

  else

    Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,

     {thy_ref = merge_thys1 ct th,

      tags = [],

      maxidx = Int.max (maxidxA, maxidx),

      shyps = Sorts.union sorts shyps,

      hyps = remove_hyps A hyps,

      tpairs = tpairs,

      prop = Logic.mk_implies (A, prop)});

(*Implication elimination

  A ==> B    A

  ------------

        B

*)

fun implies_elim thAB thA =

  let

    val Thm (derA, {maxidx = maxA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,

      prop = propA, ...}) = thA

    and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB;

    fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);

  in

    case prop of

      Const ("==>", _) $ A $ B =>

        if A aconv propA then

          Thm (deriv_rule2 (curry Proofterm.%%) der derA,

           {thy_ref = merge_thys2 thAB thA,

            tags = [],

            maxidx = Int.max (maxA, maxidx),

            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

  ------

  !!x. A

*)

fun forall_intr

    (ct as Cterm {t = x, T, sorts, ...})

    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =

  let

    fun result a =

      Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,

       {thy_ref = merge_thys1 ct th,

        tags = [],

        maxidx = maxidx,

        shyps = Sorts.union sorts shyps,

        hyps = hyps,

        tpairs = tpairs,

        prop = Term.all T $ Abs (a, T, abstract_over (x, prop))});

    fun check_occs a x ts =

      if exists (fn t => Logic.occs (x, t)) ts then

        raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])

      else ();

  in

    case x of

      Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)

    | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a)

    | _ => raise THM ("forall_intr: not a variable", 0, [th])

  end;

(*Forall elimination

  !!x. A

  ------

  A[t/x]

*)

fun forall_elim

    (ct as Cterm {t, T, maxidx = maxt, sorts, ...})

    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =

  (case prop of

    Const ("all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>

      if T <> qary then

        raise THM ("forall_elim: type mismatch", 0, [th])

      else

        Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,

         {thy_ref = merge_thys1 ct th,

          tags = [],

          maxidx = Int.max (maxidx, maxt),

          shyps = Sorts.union sorts shyps,

          hyps = hyps,

          tpairs = tpairs,

          prop = Term.betapply (A, t)})

  | _ => raise THM ("forall_elim: not quantified", 0, [th]));

(* Equality *)

(*Reflexivity

  t == t

*)

fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =

  Thm (deriv_rule0 Proofterm.reflexive,

   {thy_ref = thy_ref,

    tags = [],

    maxidx = maxidx,

    shyps = sorts,

    hyps = [],

    tpairs = [],

    prop = Logic.mk_equals (t, t)});

(*Symmetry

  t == u

  ------

  u == t

*)

fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =

  (case prop of

    (eq as Const ("==", _)) $ t $ u =>

      Thm (deriv_rule1 Proofterm.symmetric der,

       {thy_ref = thy_ref,

        tags = [],

        maxidx = maxidx,

        shyps = shyps,

        hyps = hyps,

        tpairs = tpairs,

        prop = eq $ u $ t})

    | _ => raise THM ("symmetric", 0, [th]));

(*Transitivity

  t1 == u    u == t2

  ------------------

       t1 == t2

*)

fun transitive th1 th2 =

  let

    val Thm (der1, {maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,

      prop = prop1, ...}) = th1

    and Thm (der2, {maxidx = max2, hyps = hyps2, 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 ("==", Type (_, [T, _]))) $ t1 $ u, Const ("==", _) $ u' $ t2) =>

        if not (u aconv u') then err "middle term"

        else

          Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,

           {thy_ref = merge_thys2 th1 th2,

            tags = [],

            maxidx = Int.max (max1, max2),

            shyps = Sorts.union shyps1 shyps2,

            hyps = union_hyps hyps1 hyps2,

            tpairs = union_tpairs tpairs1 tpairs2,

            prop = eq $ t1 $ t2})

     | _ =>  err "premises"

  end;

(*Beta-conversion

  (%x. t)(u) == t[u/x]

  fully beta-reduces the term if full = true

*)

fun beta_conversion full (Cterm {thy_ref, 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, []));

  in

    Thm (deriv_rule0 Proofterm.reflexive,

     {thy_ref = thy_ref,

      tags = [],

      maxidx = maxidx,

      shyps = sorts,

      hyps = [],

      tpairs = [],

      prop = Logic.mk_equals (t, t')})

  end;

fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =

  Thm (deriv_rule0 Proofterm.reflexive,

   {thy_ref = thy_ref,

    tags = [],

    maxidx = maxidx,

    shyps = sorts,

    hyps = [],

    tpairs = [],

    prop = Logic.mk_equals (t, Envir.eta_contract t)});

fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =

  Thm (deriv_rule0 Proofterm.reflexive,

   {thy_ref = thy_ref,

    tags = [],

    maxidx = maxidx,

    shyps = sorts,

    hyps = [],

    tpairs = [],

    prop = Logic.mk_equals (t, Pattern.eta_long [] t)});

(*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 == u

  --------------

  %x. t == %x. u

*)

fun abstract_rule a

    (Cterm {t = x, T, sorts, ...})

    (th as Thm (der, {thy_ref, maxidx, hyps, shyps, tpairs, prop, ...})) =

  let

    val (t, u) = Logic.dest_equals prop

      handle TERM _ => raise THM ("abstract_rule: premise not an equality", 0, [th]);

    val result =

      Thm (deriv_rule1 (Proofterm.abstract_rule x a) der,

       {thy_ref = thy_ref,

        tags = [],

        maxidx = maxidx,

        shyps = Sorts.union sorts shyps,

        hyps = hyps,

        tpairs = tpairs,

        prop = Logic.mk_equals

          (Abs (a, T, abstract_over (x, t)), Abs (a, T, abstract_over (x, u)))});

    fun check_occs a x ts =

      if exists (fn t => Logic.occs (x, t)) ts then

        raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])

      else ();

  in

    case x of

      Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result)

    | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result)

    | _ => raise THM ("abstract_rule: not a variable", 0, [th])

  end;

(*The combination rule

  f == g  t == u

  --------------

    f t == g u

*)

fun combination th1 th2 =

  let

    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,

      prop = prop1, ...}) = th1

    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,

      prop = prop2, ...}) = th2;

    fun chktypes fT tT =

      (case fT of

        Type ("fun", [T1, _]) =>

          if T1 <> tT then

            raise THM ("combination: types", 0, [th1, th2])

          else ()

      | _ => raise THM ("combination: not function type", 0, [th1, th2]));

  in

    case (prop1, prop2) of

      (Const ("==", Type ("fun", [fT, _])) $ f $ g,

       Const ("==", Type ("fun", [tT, _])) $ t $ u) =>

        (chktypes fT tT;

          Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,

           {thy_ref = merge_thys2 th1 th2,

            tags = [],

            maxidx = Int.max (max1, max2),

            shyps = Sorts.union shyps1 shyps2,

            hyps = union_hyps hyps1 hyps2,

            tpairs = union_tpairs tpairs1 tpairs2,

            prop = Logic.mk_equals (f $ t, g $ u)}))

     | _ => raise THM ("combination: premises", 0, [th1, th2])

  end;

(*Equality introduction

  A ==> B  B ==> A

  ----------------

       A == B

*)

fun equal_intr th1 th2 =

  let

    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,

      prop = prop1, ...}) = th1

    and Thm (der2, {maxidx = max2, 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("==>", _) $ A $ B, Const("==>", _) $ B' $ A') =>

        if A aconv A' andalso B aconv B' then

          Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,

           {thy_ref = merge_thys2 th1 th2,

            tags = [],

            maxidx = Int.max (max1, max2),

            shyps = Sorts.union shyps1 shyps2,

            hyps = union_hyps hyps1 hyps2,

            tpairs = union_tpairs tpairs1 tpairs2,

            prop = Logic.mk_equals (A, B)})

        else err "not equal"

    | _ =>  err "premises"

  end;

(*The equal propositions rule

  A == B  A

  ---------

      B

*)

fun equal_elim th1 th2 =

  let

    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1,

      tpairs = tpairs1, prop = prop1, ...}) = th1

    and Thm (der2, {maxidx = max2, 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 ("==", _) $ A $ B =>

        if prop2 aconv A then

          Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,

           {thy_ref = merge_thys2 th1 th2,

            tags = [],

            maxidx = Int.max (max1, max2),