<commit_before>(*  Title:      Pure/thm.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

The core of Isabelle's Meta Logic: certified types and terms, meta
theorems, meta rules (including resolution and simplification).
*)

signature BASIC_THM =
  sig
  (*certified types*)
  type ctyp
  val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
  val typ_of            : ctyp -> typ
  val ctyp_of           : Sign.sg -> typ -> ctyp
  val read_ctyp         : Sign.sg -> string -> ctyp

  (*certified terms*)
  type cterm
  exception CTERM of string
  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
  val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
  val sign_of_cterm	: cterm -> Sign.sg
  val term_of           : cterm -> term
  val cterm_of          : Sign.sg -> term -> cterm
  val ctyp_of_term      : cterm -> ctyp
  val read_cterm        : Sign.sg -> string * typ -> cterm
  val cterm_fun         : (term -> term) -> (cterm -> cterm)
  val dest_comb         : cterm -> cterm * cterm
  val dest_abs          : string option -> cterm -> cterm * cterm
  val adjust_maxidx     : cterm -> cterm
  val capply            : cterm -> cterm -> cterm
  val cabs              : cterm -> cterm -> cterm
  val read_def_cterm    :
    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    string list -> bool -> string * typ -> cterm * (indexname * typ) list
  val read_def_cterms   :
    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    string list -> bool -> (string * typ)list
    -> cterm list * (indexname * typ)list

  (*proof terms [must DUPLICATE declaration as a specification]*)
  datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
  type tag		(* = string * string list *)
  val keep_derivs       : deriv_kind ref
  datatype rule = 
      MinProof                          
    | Oracle		  of string * Sign.sg * Object.T
    | Axiom               of string * tag list
    | Theorem             of string * tag list
    | Assume              of cterm
    | Implies_intr        of cterm
    | Implies_intr_hyps
    | Implies_elim 
    | Forall_intr         of cterm
    | Forall_elim         of cterm
    | Reflexive           of cterm
    | Symmetric 
    | Transitive
    | Beta_conversion     of cterm
    | Eta_conversion      of cterm
    | Extensional
    | Abstract_rule       of string * cterm
    | Combination
    | Equal_intr
    | Equal_elim
    | Trivial             of cterm
    | Lift_rule           of cterm * int 
    | Assumption          of int * Envir.env option
    | Rotate_rule         of int * int
    | Permute_prems       of int * int
    | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    | Bicompose           of bool * bool * int * int * Envir.env
    | Flexflex_rule       of Envir.env            
    | Class_triv          of class       
    | VarifyT		  of string list
    | FreezeT
    | RewriteC            of cterm
    | CongC               of cterm
    | Rewrite_cterm       of cterm
    | Rename_params_rule  of string list * int;
  type deriv	(* = rule mtree *)

  (*meta theorems*)
  type thm
  val rep_thm           : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                  shyps: sort list, hyps: term list, 
                                  prop: term}
  val crep_thm          : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                  shyps: sort list, hyps: cterm list, 
                                  prop: cterm}
  exception THM of string * int * thm list
  type 'a attribute 	(* = 'a * thm -> 'a * thm *)
  val eq_thm		: thm * thm -> bool
  val sign_of_thm       : thm -> Sign.sg
  val transfer_sg	: Sign.sg -> thm -> thm
  val transfer		: theory -> thm -> thm
  val tpairs_of         : thm -> (term * term) list
  val prems_of          : thm -> term list
  val nprems_of         : thm -> int
  val concl_of          : thm -> term
  val cprop_of          : thm -> cterm
  val extra_shyps       : thm -> sort list
  val strip_shyps       : thm -> thm
  val get_axiom         : theory -> xstring -> thm
  val def_name		: string -> string
  val get_def           : theory -> xstring -> thm
  val axioms_of         : theory -> (string * thm) list

  (*meta rules*)
  val assume            : cterm -> thm
  val compress          : thm -> 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 -> cterm -> thm
  val eta_conversion    : cterm -> thm
  val extensional       : thm -> thm
  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 implies_intr_hyps : thm -> thm
  val flexflex_rule     : thm -> thm Seq.seq
  val instantiate       :
    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
  val trivial           : cterm -> thm
  val class_triv        : Sign.sg -> class -> thm
  val varifyT           : thm -> thm
  val varifyT'          : string list -> thm -> thm
  val freezeT           : thm -> thm
  val dest_state        : thm * int ->
    (term * term) list * term list * term * term
  val lift_rule         : (thm * int) -> 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 bicompose         : bool -> bool * thm * int ->
    int -> thm -> thm Seq.seq
  val biresolution      : bool -> (bool * thm) list ->
    int -> thm -> thm Seq.seq
  val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
end;

signature THM =
sig
  include BASIC_THM
  val major_prem_of	: thm -> term
  val no_prems		: thm -> bool
  val no_attributes	: 'a -> 'a * 'b attribute list
  val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
  val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
  val get_name_tags	: thm -> string * tag list
  val put_name_tags	: string * tag list -> thm -> thm
  val name_of_thm	: thm -> string
  val tags_of_thm	: thm -> tag list
  val name_thm		: string * thm -> thm
  val rename_boundvars  : term -> term -> thm -> thm
  val cterm_match       : cterm * cterm ->
    (indexname * ctyp) list * (cterm * cterm) list
  val cterm_first_order_match : cterm * cterm ->
    (indexname * ctyp) list * (cterm * cterm) list
  val cterm_incr_indexes : int -> cterm -> cterm
end;

structure Thm: THM =
struct

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

(** certified types **)

(*certified typs under a signature*)

datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};

fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
fun typ_of (Ctyp {T, ...}) = T;

fun ctyp_of sign T =
  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};

fun read_ctyp sign s =
  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};



(** certified terms **)

(*certified terms under a signature, with checked typ and maxidx of Vars*)

datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};

fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
  {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};

fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
  {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
    maxidx = maxidx};

fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;

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

fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};

(*create a cterm by checking a "raw" term with respect to a signature*)
fun cterm_of sign tm =
  let val (t, T, maxidx) = Sign.certify_term sign tm
  in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
  end;

fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);


exception CTERM of string;

(*Destruct application in cterms*)
fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
      let val typeA = fastype_of A;
          val typeB =
            case typeA of Type("fun",[S,T]) => S
                        | _ => error "Function type expected in dest_comb";
      in
      (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
       Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
      end
  | dest_comb _ = raise CTERM "dest_comb";

(*Destruct abstraction in cterms*)
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
      let val (y,N) = variant_abs (if_none a x,ty,M)
      in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
          Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
      end
  | dest_abs _ _ = raise CTERM "dest_abs";

(*Makes maxidx precise: it is often too big*)
fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
  if maxidx = ~1 then ct 
  else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};

(*Form cterm out of a function and an argument*)
fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
           (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
      if T = dty then
        Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
          maxidx=Int.max(maxidx1, maxidx2)}
      else raise CTERM "capply: types don't agree"
  | capply _ _ = raise CTERM "capply: first arg is not a function"

fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
         (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
      Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
             T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
  | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";

(*Matching of cterms*)
fun gen_cterm_match mtch
      (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...},
       Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) =
  let
    val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2);
    val tsig = Sign.tsig_of (Sign.deref sign_ref);
    val (Tinsts, tinsts) = mtch tsig (t1, t2);
    val maxidx = Int.max (maxidx1, maxidx2);
    val vars = map dest_Var (term_vars t1);
    fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T});
    fun mk_ctinsts (ixn, t) =
      let val T = typ_subst_TVars Tinsts (the (assoc (vars, ixn)))
      in
        (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
         Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
      end;
  in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end;

val cterm_match = gen_cterm_match Pattern.match;
val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;

(*Incrementing indexes*)
fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) =
  if i < 0 then raise CTERM "negative increment" else 
  if i = 0 then ct else
    Cterm {sign_ref = sign_ref, maxidx = maxidx + i,
      t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};



(** read cterms **)   (*exception ERROR*)

(*read terms, infer types, certify terms*)
fun read_def_cterms (sign, types, sorts) used freeze sTs =
  let
    val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
    val cts = map (cterm_of sign) ts'
      handle TYPE (msg, _, _) => error msg
           | TERM (msg, _) => error msg;
  in (cts, tye) end;

(*read term, infer types, certify term*)
fun read_def_cterm args used freeze aT =
  let val ([ct],tye) = read_def_cterms args used freeze [aT]
  in (ct,tye) end;

fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;



(*** Derivations ***)

(*tags provide additional comment, apart from the axiom/theorem name*)
type tag = string * string list;

(*Names of rules in derivations.  Includes logically trivial rules, if 
  executed in ML.*)
datatype rule = 
    MinProof                            (*for building minimal proof terms*)
  | Oracle              of string * Sign.sg * Object.T       (*oracles*)
(*Axioms/theorems*)
  | Axiom               of string * tag list
  | Theorem             of string * tag list
(*primitive inferences and compound versions of them*)
  | Assume              of cterm
  | Implies_intr        of cterm
  | Implies_intr_hyps
  | Implies_elim 
  | Forall_intr         of cterm
  | Forall_elim         of cterm
  | Reflexive           of cterm
  | Symmetric 
  | Transitive
  | Beta_conversion     of cterm
  | Eta_conversion      of cterm
  | Extensional
  | Abstract_rule       of string * cterm
  | Combination
  | Equal_intr
  | Equal_elim
(*derived rules for tactical proof*)
  | Trivial             of cterm
        (*For lift_rule, the proof state is not a premise.
          Use cterm instead of thm to avoid mutual recursion.*)
  | Lift_rule           of cterm * int 
  | Assumption          of int * Envir.env option (*includes eq_assumption*)
  | Rotate_rule         of int * int
  | Permute_prems       of int * int
  | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
  | Bicompose           of bool * bool * int * int * Envir.env
  | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
(*other derived rules*)
  | Class_triv          of class
  | VarifyT		of string list
  | FreezeT
(*for the simplifier*)
  | RewriteC            of cterm
  | CongC               of cterm
  | Rewrite_cterm       of cterm
(*Logical identities, recorded since they are part of the proof process*)
  | Rename_params_rule  of string list * int;


type deriv = rule mtree;

datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;

val keep_derivs = ref MinDeriv;

local

(*Build a minimal derivation.  Keep oracles; suppress atomic inferences;
  retain Theorems or their underlying links; keep anything else*)
fun squash_derivs [] = []
  | squash_derivs (der::ders) =
     (case der of
          Join (Oracle _, _) => der :: squash_derivs ders
        | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
                                      then der :: squash_derivs ders
                                      else squash_derivs (der'::ders)
        | Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
                               then der :: squash_derivs ders
                               else squash_derivs ders
        | Join (_, [])      => squash_derivs ders
        | _                 => der :: squash_derivs ders);

(*Ensure sharing of the most likely derivation, the empty one!*)
val min_infer = Join (MinProof, []);

(*Make a minimal inference*)
fun make_min_infer []    = min_infer
  | make_min_infer [der] = der
  | make_min_infer ders  = Join (MinProof, ders);

fun is_oracle (Oracle _) = true
  | is_oracle _ = false;

in

fun infer_derivs (rl, []: (bool * deriv) list)   = (is_oracle rl, Join (rl, []))
  | infer_derivs (rl, ders) =
      (is_oracle rl orelse exists #1 ders,
        if !keep_derivs=FullDeriv then Join (rl, map #2 ders)
        else make_min_infer (squash_derivs (map #2 ders)));

end;



(*** Meta theorems ***)

datatype thm = Thm of
 {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
  der: bool * deriv,           (*derivation*)
  maxidx: int,                 (*maximum index of any Var or TVar*)
  shyps: sort list,            (*sort hypotheses*)
  hyps: term list,             (*hypotheses*)
  prop: term};                 (*conclusion*)

fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
  {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
    shyps = shyps, hyps = hyps, prop = prop};

(*Version of rep_thm returning cterms instead of terms*)
fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
  let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
  in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
      hyps = map (ctermf ~1) hyps,
      prop = ctermf maxidx prop}
  end;

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

(*attributes subsume any kind of rules or addXXXs modifiers*)
type 'a attribute = 'a * thm -> 'a * thm;

fun no_attributes x = (x, []);
fun apply_attributes (x_th, atts) = Library.apply atts x_th;
fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;

fun eq_thm (th1, th2) =
  let
    val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, maxidx = _, der = _} =
      rep_thm th1;
    val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, maxidx = _, der = _} =
      rep_thm th2;
  in
    Sign.joinable (sg1, sg2) andalso
    eq_set_sort (shyps1, shyps2) andalso
    aconvs (hyps1, hyps2) andalso
    prop1 aconv prop2
  end;

fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;

(*merge signatures of two theorems; raise exception if incompatible*)
fun merge_thm_sgs
    (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
  Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);

(*transfer thm to super theory (non-destructive)*)
fun transfer_sg sign' thm =
  let
    val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
    val sign = Sign.deref sign_ref;
  in
    if Sign.eq_sg (sign, sign') then thm
    else if Sign.subsig (sign, sign') then
      Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
        shyps = shyps, hyps = hyps, prop = prop}
    else raise THM ("transfer: not a super theory", 0, [thm])
  end;

val transfer = transfer_sg o Theory.sign_of;

(*maps object-rule to tpairs*)
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);

(*maps object-rule to premises*)
fun prems_of (Thm {prop, ...}) =
  Logic.strip_imp_prems (Logic.skip_flexpairs prop);

(*counts premises in a rule*)
fun nprems_of (Thm {prop, ...}) =
  Logic.count_prems (Logic.skip_flexpairs prop, 0);

fun major_prem_of thm =
  (case prems_of thm of
    prem :: _ => prem
  | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));

fun no_prems thm = nprems_of thm = 0;

(*maps object-rule to conclusion*)
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;

(*the statement of any thm is a cterm*)
fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
  Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};



(** sort contexts of theorems **)

(* basic utils *)

(*accumulate sorts suppressing duplicates; these are coded low levelly
  to improve efficiency a bit*)

fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
  | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
  | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
and add_typs_sorts ([], Ss) = Ss
  | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));

fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Bound _, Ss) = Ss
  | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
  | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));

fun add_terms_sorts ([], Ss) = Ss
  | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));

fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);

fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
  Vartab.foldl (add_term_sorts o swap o apsnd snd)
    (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);

fun add_insts_sorts ((iTs, is), Ss) =
  add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));

fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
  add_terms_sorts (hyps, add_term_sorts (prop, Ss));

fun add_thms_shyps ([], Ss) = Ss
  | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
      add_thms_shyps (ths, union_sort (shyps, Ss));


(*get 'dangling' sort constraints of a thm*)
fun extra_shyps (th as Thm {shyps, ...}) =
  Term.rems_sort (shyps, add_thm_sorts (th, []));


(* fix_shyps *)

fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref));

(*preserve sort contexts of rule premises and substituted types*)
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) =
  Thm
   {sign_ref = sign_ref,
    der = der,             (*no new derivation, as other rules call this*)
    maxidx = maxidx,
    shyps =
      if all_sorts_nonempty sign_ref then []
      else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
    hyps = hyps, prop = prop}


(* strip_shyps *)

(*remove extra sorts that are non-empty by virtue of type signature information*)
fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
  | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
      let
        val sign = Sign.deref sign_ref;

        val present_sorts = add_thm_sorts (thm, []);
        val extra_shyps = Term.rems_sort (shyps, present_sorts);
        val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
      in
        Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
             shyps = Term.rems_sort (shyps, map #2 witnessed_shyps),
             hyps = hyps, prop = prop}
      end;



(** Axioms **)

(*look up the named axiom in the theory*)
fun get_axiom theory raw_name =
  let
    val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;

    fun get_ax [] = None
      | get_ax (thy :: thys) =
          let val {sign, axioms, ...} = Theory.rep_theory thy in
            (case Symtab.lookup (axioms, name) of
              Some t =>
                Some (fix_shyps [] []
                  (Thm {sign_ref = Sign.self_ref sign,
                    der = infer_derivs (Axiom (name, []), []),
                    maxidx = maxidx_of_term t,
                    shyps = [], 
                    hyps = [], 
                    prop = t}))
            | None => get_ax thys)
          end;
  in
    (case get_ax (theory :: Theory.ancestors_of theory) of
      Some thm => thm
    | None => raise THEORY ("No axiom " ^ quote name, [theory]))
  end;

fun def_name name = name ^ "_def";
fun get_def thy = get_axiom thy o def_name;


(*return additional axioms of this theory node*)
fun axioms_of thy =
  map (fn (s, _) => (s, get_axiom thy s))
    (Symtab.dest (#axioms (Theory.rep_theory thy)));


(* name and tags -- make proof objects more readable *)

fun get_name_tags (Thm {der, ...}) =
  (case #2 der of
    Join (Theorem x, _) => x
  | Join (Axiom x, _) => x
  | _ => ("", []));

fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) =
  let
    val der' =
      (case der of
        Join (Theorem _, ds) => Join (Theorem x, ds)
      | Join (Axiom _, ds) => Join (Axiom x, ds)
      | _ => Join (Theorem x, [der]));
  in
    Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx,
      shyps = shyps, hyps = hyps, prop = prop}
  end;

val name_of_thm = #1 o get_name_tags;
val tags_of_thm = #2 o get_name_tags;

fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;


(*Compression of theorems -- a separate rule, not integrated with the others,
  as it could be slow.*)
fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
    Thm {sign_ref = sign_ref, 
         der = der,     (*No derivation recorded!*)
         maxidx = maxidx,
         shyps = shyps, 
         hyps = map Term.compress_term hyps, 
         prop = Term.compress_term prop};



(*** Meta rules ***)

(*Check that term does not contain same var with different typing/sorting.
  If this check must be made, recalculate maxidx in hope of preventing its
  recurrence.*)
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
  Thm {sign_ref = sign_ref, 
         der = der,     
         maxidx = maxidx_of_term prop,
         shyps = shyps, 
         hyps = hyps, 
         prop = Sign.nodup_vars prop}
  handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);


(** 'primitive' rules **)

(*discharge all assumptions t from ts*)
val disch = gen_rem (op aconv);

(*The assumption rule A|-A in a theory*)
fun assume raw_ct : thm =
  let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
  in  if T<>propT then
        raise THM("assume: assumptions must have type prop", 0, [])
      else if maxidx <> ~1 then
        raise THM("assume: assumptions may not contain scheme variables",
                  maxidx, [])
      else Thm{sign_ref   = sign_ref,
               der    = infer_derivs (Assume ct, []),
               maxidx = ~1, 
               shyps  = add_term_sorts(prop,[]), 
               hyps   = [prop], 
               prop   = prop}
  end;

(*Implication introduction
    [A]
     :
     B
  -------
  A ==> B
*)
fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,prop}) : thm =
  let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
  in  if T<>propT then
        raise THM("implies_intr: assumptions must have type prop", 0, [thB])
      else
         Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
             der = infer_derivs (Implies_intr cA, [der]),
             maxidx = Int.max(maxidxA, maxidx),
             shyps = add_term_sorts (A, shyps),
             hyps = disch(hyps,A),
             prop = implies$A$prop}
      handle TERM _ =>
        raise THM("implies_intr: incompatible signatures", 0, [thB])
  end;


(*Implication elimination
  A ==> B    A
  ------------
        B
*)
fun implies_elim thAB thA : thm =
    let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, prop=propA, ...} = thA
        and Thm{der, maxidx, hyps, shyps, prop, ...} = thAB;
        fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
    in  case prop of
            imp$A$B =>
                if imp=implies andalso  A aconv propA
                then
                  Thm{sign_ref= merge_thm_sgs(thAB,thA),
                      der = infer_derivs (Implies_elim, [der,derA]),
                      maxidx = Int.max(maxA,maxidx),
                      shyps = union_sort (shypsA, shyps),
                      hyps = union_term(hypsA,hyps),  (*dups suppressed*)
                      prop = B}
                else err("major premise")
          | _ => err("major premise")
    end;

(*Forall introduction.  The Free or Var x must not be free in the hypotheses.
    A
  -----
  !!x.A
*)
fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
  let val x = term_of cx;
      fun result(a,T) = fix_shyps [th] []
        (Thm{sign_ref = sign_ref, 
             der = infer_derivs (Forall_intr cx, [der]),
             maxidx = maxidx,
             shyps = [],
             hyps = hyps,
             prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
  in  case x of
        Free(a,T) =>
          if exists (apl(x, Logic.occs)) hyps
          then  raise THM("forall_intr: variable free in assumptions", 0, [th])
          else  result(a,T)
      | Var((a,_),T) => result(a,T)
      | _ => raise THM("forall_intr: not a variable", 0, [th])
  end;

(*Forall elimination
  !!x.A
  ------
  A[t/x]
*)
fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
  let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
  in  case prop of
        Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
          if T<>qary then
              raise THM("forall_elim: type mismatch", 0, [th])
          else let val thm = fix_shyps [th] []
                    (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
                         der = infer_derivs (Forall_elim ct, [der]),
                         maxidx = Int.max(maxidx, maxt),
                         shyps = [],
                         hyps = hyps,  
                         prop = betapply(A,t)})
               in if maxt >= 0 andalso maxidx >= 0
                  then nodup_vars thm "forall_elim" 
                  else thm (*no new Vars: no expensive check!*)
               end
      | _ => raise THM("forall_elim: not quantified", 0, [th])
  end
  handle TERM _ =>
         raise THM("forall_elim: incompatible signatures", 0, [th]);


(* Equality *)

(*The reflexivity rule: maps  t   to the theorem   t==t   *)
fun reflexive ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm{sign_ref= sign_ref, 
         der = infer_derivs (Reflexive ct, []),
         shyps = add_term_sorts (t, []),
         hyps = [], 
         maxidx = maxidx,
         prop = Logic.mk_equals(t,t)}
  end;

(*The symmetry rule
  t==u
  ----
  u==t
*)
fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  case prop of
      (eq as Const("==",_)) $ t $ u =>
        (*no fix_shyps*)
          Thm{sign_ref = sign_ref,
              der = infer_derivs (Symmetric, [der]),
              maxidx = maxidx,
              shyps = shyps,
              hyps = hyps,
              prop = eq$u$t}
    | _ => raise THM("symmetric", 0, [th]);

(*The transitive rule
  t1==u    u==t2
  --------------
      t1==t2
*)
fun transitive th1 th2 =
  let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, prop=prop1,...} = th1
      and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, prop=prop2,...} = th2;
      fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
  in case (prop1,prop2) of
       ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
          if not (u aconv u') then err"middle term"
          else let val thm =      
                 Thm{sign_ref= merge_thm_sgs(th1,th2), 
                     der = infer_derivs (Transitive, [der1, der2]),
                     maxidx = Int.max(max1,max2), 
                     shyps = union_sort (shyps1, shyps2),
                     hyps = union_term(hyps1,hyps2),
                     prop = eq$t1$t2}
                 in if max1 >= 0 andalso max2 >= 0
                    then nodup_vars thm "transitive" 
                    else thm (*no new Vars: no expensive check!*)
                 end
     | _ =>  err"premises"
  end;

(*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x]
  Fully beta-reduces the term if full=true
*)
fun beta_conversion full ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm
    {sign_ref = sign_ref,  
     der = infer_derivs (Beta_conversion ct, []),
     maxidx = maxidx,
     shyps = add_term_sorts (t, []),
     hyps = [],
     prop = Logic.mk_equals (t, if full then Envir.norm_term (Envir.empty 0) t
       else case t of
          Abs(_, _, bodt) $ u => subst_bound (u, bodt)
        | _ => raise THM ("beta_conversion: not a redex", 0, []))}
  end;

fun eta_conversion ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm
    {sign_ref = sign_ref,  
     der = infer_derivs (Eta_conversion ct, []),
     maxidx = maxidx,<commit_msg>Envir.beta_norm;<commit_after>(*  Title:      Pure/thm.ML
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

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

signature BASIC_THM =
  sig
  (*certified types*)
  type ctyp
  val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
  val typ_of            : ctyp -> typ
  val ctyp_of           : Sign.sg -> typ -> ctyp
  val read_ctyp         : Sign.sg -> string -> ctyp

  (*certified terms*)
  type cterm
  exception CTERM of string
  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
  val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
  val sign_of_cterm	: cterm -> Sign.sg
  val term_of           : cterm -> term
  val cterm_of          : Sign.sg -> term -> cterm
  val ctyp_of_term      : cterm -> ctyp
  val read_cterm        : Sign.sg -> string * typ -> cterm
  val cterm_fun         : (term -> term) -> (cterm -> cterm)
  val dest_comb         : cterm -> cterm * cterm
  val dest_abs          : string option -> cterm -> cterm * cterm
  val adjust_maxidx     : cterm -> cterm
  val capply            : cterm -> cterm -> cterm
  val cabs              : cterm -> cterm -> cterm
  val read_def_cterm    :
    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    string list -> bool -> string * typ -> cterm * (indexname * typ) list
  val read_def_cterms   :
    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    string list -> bool -> (string * typ)list
    -> cterm list * (indexname * typ)list

  (*proof terms [must DUPLICATE declaration as a specification]*)
  datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
  type tag		(* = string * string list *)
  val keep_derivs       : deriv_kind ref
  datatype rule = 
      MinProof                          
    | Oracle		  of string * Sign.sg * Object.T
    | Axiom               of string * tag list
    | Theorem             of string * tag list
    | Assume              of cterm
    | Implies_intr        of cterm
    | Implies_intr_hyps
    | Implies_elim 
    | Forall_intr         of cterm
    | Forall_elim         of cterm
    | Reflexive           of cterm
    | Symmetric 
    | Transitive
    | Beta_conversion     of cterm
    | Eta_conversion      of cterm
    | Extensional
    | Abstract_rule       of string * cterm
    | Combination
    | Equal_intr
    | Equal_elim
    | Trivial             of cterm
    | Lift_rule           of cterm * int 
    | Assumption          of int * Envir.env option
    | Rotate_rule         of int * int
    | Permute_prems       of int * int
    | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    | Bicompose           of bool * bool * int * int * Envir.env
    | Flexflex_rule       of Envir.env            
    | Class_triv          of class       
    | VarifyT		  of string list
    | FreezeT
    | RewriteC            of cterm
    | CongC               of cterm
    | Rewrite_cterm       of cterm
    | Rename_params_rule  of string list * int;
  type deriv	(* = rule mtree *)

  (*meta theorems*)
  type thm
  val rep_thm           : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                  shyps: sort list, hyps: term list, 
                                  prop: term}
  val crep_thm          : thm -> {sign: Sign.sg, der: bool * deriv, maxidx: int,
                                  shyps: sort list, hyps: cterm list, 
                                  prop: cterm}
  exception THM of string * int * thm list
  type 'a attribute 	(* = 'a * thm -> 'a * thm *)
  val eq_thm		: thm * thm -> bool
  val sign_of_thm       : thm -> Sign.sg
  val transfer_sg	: Sign.sg -> thm -> thm
  val transfer		: theory -> thm -> thm
  val tpairs_of         : thm -> (term * term) list
  val prems_of          : thm -> term list
  val nprems_of         : thm -> int
  val concl_of          : thm -> term
  val cprop_of          : thm -> cterm
  val extra_shyps       : thm -> sort list
  val strip_shyps       : thm -> thm
  val get_axiom         : theory -> xstring -> thm
  val def_name		: string -> string
  val get_def           : theory -> xstring -> thm
  val axioms_of         : theory -> (string * thm) list

  (*meta rules*)
  val assume            : cterm -> thm
  val compress          : thm -> 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 -> cterm -> thm
  val eta_conversion    : cterm -> thm
  val extensional       : thm -> thm
  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 implies_intr_hyps : thm -> thm
  val flexflex_rule     : thm -> thm Seq.seq
  val instantiate       :
    (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
  val trivial           : cterm -> thm
  val class_triv        : Sign.sg -> class -> thm
  val varifyT           : thm -> thm
  val varifyT'          : string list -> thm -> thm
  val freezeT           : thm -> thm
  val dest_state        : thm * int ->
    (term * term) list * term list * term * term
  val lift_rule         : (thm * int) -> 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 bicompose         : bool -> bool * thm * int ->
    int -> thm -> thm Seq.seq
  val biresolution      : bool -> (bool * thm) list ->
    int -> thm -> thm Seq.seq
  val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
end;

signature THM =
sig
  include BASIC_THM
  val major_prem_of	: thm -> term
  val no_prems		: thm -> bool
  val no_attributes	: 'a -> 'a * 'b attribute list
  val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
  val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
  val get_name_tags	: thm -> string * tag list
  val put_name_tags	: string * tag list -> thm -> thm
  val name_of_thm	: thm -> string
  val tags_of_thm	: thm -> tag list
  val name_thm		: string * thm -> thm
  val rename_boundvars  : term -> term -> thm -> thm
  val cterm_match       : cterm * cterm ->
    (indexname * ctyp) list * (cterm * cterm) list
  val cterm_first_order_match : cterm * cterm ->
    (indexname * ctyp) list * (cterm * cterm) list
  val cterm_incr_indexes : int -> cterm -> cterm
end;

structure Thm: THM =
struct

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

(** certified types **)

(*certified typs under a signature*)

datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};

fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
fun typ_of (Ctyp {T, ...}) = T;

fun ctyp_of sign T =
  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};

fun read_ctyp sign s =
  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};



(** certified terms **)

(*certified terms under a signature, with checked typ and maxidx of Vars*)

datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};

fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
  {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};

fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
  {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
    maxidx = maxidx};

fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;

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

fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};

(*create a cterm by checking a "raw" term with respect to a signature*)
fun cterm_of sign tm =
  let val (t, T, maxidx) = Sign.certify_term sign tm
  in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
  end;

fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);


exception CTERM of string;

(*Destruct application in cterms*)
fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
      let val typeA = fastype_of A;
          val typeB =
            case typeA of Type("fun",[S,T]) => S
                        | _ => error "Function type expected in dest_comb";
      in
      (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
       Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
      end
  | dest_comb _ = raise CTERM "dest_comb";

(*Destruct abstraction in cterms*)
fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
      let val (y,N) = variant_abs (if_none a x,ty,M)
      in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
          Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
      end
  | dest_abs _ _ = raise CTERM "dest_abs";

(*Makes maxidx precise: it is often too big*)
fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
  if maxidx = ~1 then ct 
  else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};

(*Form cterm out of a function and an argument*)
fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
           (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
      if T = dty then
        Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
          maxidx=Int.max(maxidx1, maxidx2)}
      else raise CTERM "capply: types don't agree"
  | capply _ _ = raise CTERM "capply: first arg is not a function"

fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
         (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
      Cterm {t=Sign.nodup_vars (absfree(a,ty,t2)), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
             T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
  | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";

(*Matching of cterms*)
fun gen_cterm_match mtch
      (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...},
       Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) =
  let
    val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2);
    val tsig = Sign.tsig_of (Sign.deref sign_ref);
    val (Tinsts, tinsts) = mtch tsig (t1, t2);
    val maxidx = Int.max (maxidx1, maxidx2);
    val vars = map dest_Var (term_vars t1);
    fun mk_cTinsts (ixn, T) = (ixn, Ctyp {sign_ref = sign_ref, T = T});
    fun mk_ctinsts (ixn, t) =
      let val T = typ_subst_TVars Tinsts (the (assoc (vars, ixn)))
      in
        (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
         Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
      end;
  in (map mk_cTinsts Tinsts, map mk_ctinsts tinsts) end;

val cterm_match = gen_cterm_match Pattern.match;
val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;

(*Incrementing indexes*)
fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) =
  if i < 0 then raise CTERM "negative increment" else 
  if i = 0 then ct else
    Cterm {sign_ref = sign_ref, maxidx = maxidx + i,
      t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};



(** read cterms **)   (*exception ERROR*)

(*read terms, infer types, certify terms*)
fun read_def_cterms (sign, types, sorts) used freeze sTs =
  let
    val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
    val cts = map (cterm_of sign) ts'
      handle TYPE (msg, _, _) => error msg
           | TERM (msg, _) => error msg;
  in (cts, tye) end;

(*read term, infer types, certify term*)
fun read_def_cterm args used freeze aT =
  let val ([ct],tye) = read_def_cterms args used freeze [aT]
  in (ct,tye) end;

fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;



(*** Derivations ***)

(*tags provide additional comment, apart from the axiom/theorem name*)
type tag = string * string list;

(*Names of rules in derivations.  Includes logically trivial rules, if 
  executed in ML.*)
datatype rule = 
    MinProof                            (*for building minimal proof terms*)
  | Oracle              of string * Sign.sg * Object.T       (*oracles*)
(*Axioms/theorems*)
  | Axiom               of string * tag list
  | Theorem             of string * tag list
(*primitive inferences and compound versions of them*)
  | Assume              of cterm
  | Implies_intr        of cterm
  | Implies_intr_hyps
  | Implies_elim 
  | Forall_intr         of cterm
  | Forall_elim         of cterm
  | Reflexive           of cterm
  | Symmetric 
  | Transitive
  | Beta_conversion     of cterm
  | Eta_conversion      of cterm
  | Extensional
  | Abstract_rule       of string * cterm
  | Combination
  | Equal_intr
  | Equal_elim
(*derived rules for tactical proof*)
  | Trivial             of cterm
        (*For lift_rule, the proof state is not a premise.
          Use cterm instead of thm to avoid mutual recursion.*)
  | Lift_rule           of cterm * int 
  | Assumption          of int * Envir.env option (*includes eq_assumption*)
  | Rotate_rule         of int * int
  | Permute_prems       of int * int
  | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
  | Bicompose           of bool * bool * int * int * Envir.env
  | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
(*other derived rules*)
  | Class_triv          of class
  | VarifyT		of string list
  | FreezeT
(*for the simplifier*)
  | RewriteC            of cterm
  | CongC               of cterm
  | Rewrite_cterm       of cterm
(*Logical identities, recorded since they are part of the proof process*)
  | Rename_params_rule  of string list * int;


type deriv = rule mtree;

datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;

val keep_derivs = ref MinDeriv;

local

(*Build a minimal derivation.  Keep oracles; suppress atomic inferences;
  retain Theorems or their underlying links; keep anything else*)
fun squash_derivs [] = []
  | squash_derivs (der::ders) =
     (case der of
          Join (Oracle _, _) => der :: squash_derivs ders
        | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
                                      then der :: squash_derivs ders
                                      else squash_derivs (der'::ders)
        | Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
                               then der :: squash_derivs ders
                               else squash_derivs ders
        | Join (_, [])      => squash_derivs ders
        | _                 => der :: squash_derivs ders);

(*Ensure sharing of the most likely derivation, the empty one!*)
val min_infer = Join (MinProof, []);

(*Make a minimal inference*)
fun make_min_infer []    = min_infer
  | make_min_infer [der] = der
  | make_min_infer ders  = Join (MinProof, ders);

fun is_oracle (Oracle _) = true
  | is_oracle _ = false;

in

fun infer_derivs (rl, []: (bool * deriv) list)   = (is_oracle rl, Join (rl, []))
  | infer_derivs (rl, ders) =
      (is_oracle rl orelse exists #1 ders,
        if !keep_derivs=FullDeriv then Join (rl, map #2 ders)
        else make_min_infer (squash_derivs (map #2 ders)));

end;



(*** Meta theorems ***)

datatype thm = Thm of
 {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
  der: bool * deriv,           (*derivation*)
  maxidx: int,                 (*maximum index of any Var or TVar*)
  shyps: sort list,            (*sort hypotheses*)
  hyps: term list,             (*hypotheses*)
  prop: term};                 (*conclusion*)

fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
  {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
    shyps = shyps, hyps = hyps, prop = prop};

(*Version of rep_thm returning cterms instead of terms*)
fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
  let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
  in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
      hyps = map (ctermf ~1) hyps,
      prop = ctermf maxidx prop}
  end;

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

(*attributes subsume any kind of rules or addXXXs modifiers*)
type 'a attribute = 'a * thm -> 'a * thm;

fun no_attributes x = (x, []);
fun apply_attributes (x_th, atts) = Library.apply atts x_th;
fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;

fun eq_thm (th1, th2) =
  let
    val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, maxidx = _, der = _} =
      rep_thm th1;
    val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, maxidx = _, der = _} =
      rep_thm th2;
  in
    Sign.joinable (sg1, sg2) andalso
    eq_set_sort (shyps1, shyps2) andalso
    aconvs (hyps1, hyps2) andalso
    prop1 aconv prop2
  end;

fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;

(*merge signatures of two theorems; raise exception if incompatible*)
fun merge_thm_sgs
    (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
  Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);

(*transfer thm to super theory (non-destructive)*)
fun transfer_sg sign' thm =
  let
    val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
    val sign = Sign.deref sign_ref;
  in
    if Sign.eq_sg (sign, sign') then thm
    else if Sign.subsig (sign, sign') then
      Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
        shyps = shyps, hyps = hyps, prop = prop}
    else raise THM ("transfer: not a super theory", 0, [thm])
  end;

val transfer = transfer_sg o Theory.sign_of;

(*maps object-rule to tpairs*)
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);

(*maps object-rule to premises*)
fun prems_of (Thm {prop, ...}) =
  Logic.strip_imp_prems (Logic.skip_flexpairs prop);

(*counts premises in a rule*)
fun nprems_of (Thm {prop, ...}) =
  Logic.count_prems (Logic.skip_flexpairs prop, 0);

fun major_prem_of thm =
  (case prems_of thm of
    prem :: _ => prem
  | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm]));

fun no_prems thm = nprems_of thm = 0;

(*maps object-rule to conclusion*)
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;

(*the statement of any thm is a cterm*)
fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
  Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};



(** sort contexts of theorems **)

(* basic utils *)

(*accumulate sorts suppressing duplicates; these are coded low levelly
  to improve efficiency a bit*)

fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
  | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
  | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
and add_typs_sorts ([], Ss) = Ss
  | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));

fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
  | add_term_sorts (Bound _, Ss) = Ss
  | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
  | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));

fun add_terms_sorts ([], Ss) = Ss
  | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));

fun env_codT (Envir.Envir {iTs, ...}) = map snd (Vartab.dest iTs);

fun add_env_sorts (Envir.Envir {iTs, asol, ...}, Ss) =
  Vartab.foldl (add_term_sorts o swap o apsnd snd)
    (Vartab.foldl (add_typ_sorts o swap o apsnd snd) (Ss, iTs), asol);

fun add_insts_sorts ((iTs, is), Ss) =
  add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));

fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
  add_terms_sorts (hyps, add_term_sorts (prop, Ss));

fun add_thms_shyps ([], Ss) = Ss
  | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
      add_thms_shyps (ths, union_sort (shyps, Ss));


(*get 'dangling' sort constraints of a thm*)
fun extra_shyps (th as Thm {shyps, ...}) =
  Term.rems_sort (shyps, add_thm_sorts (th, []));


(* fix_shyps *)

fun all_sorts_nonempty sign_ref = is_some (Sign.univ_witness (Sign.deref sign_ref));

(*preserve sort contexts of rule premises and substituted types*)
fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, prop, ...}) =
  Thm
   {sign_ref = sign_ref,
    der = der,             (*no new derivation, as other rules call this*)
    maxidx = maxidx,
    shyps =
      if all_sorts_nonempty sign_ref then []
      else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
    hyps = hyps, prop = prop}


(* strip_shyps *)

(*remove extra sorts that are non-empty by virtue of type signature information*)
fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
  | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
      let
        val sign = Sign.deref sign_ref;

        val present_sorts = add_thm_sorts (thm, []);
        val extra_shyps = Term.rems_sort (shyps, present_sorts);
        val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
      in
        Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
             shyps = Term.rems_sort (shyps, map #2 witnessed_shyps),
             hyps = hyps, prop = prop}
      end;



(** Axioms **)

(*look up the named axiom in the theory*)
fun get_axiom theory raw_name =
  let
    val name = Sign.intern (Theory.sign_of theory) Theory.axiomK raw_name;

    fun get_ax [] = None
      | get_ax (thy :: thys) =
          let val {sign, axioms, ...} = Theory.rep_theory thy in
            (case Symtab.lookup (axioms, name) of
              Some t =>
                Some (fix_shyps [] []
                  (Thm {sign_ref = Sign.self_ref sign,
                    der = infer_derivs (Axiom (name, []), []),
                    maxidx = maxidx_of_term t,
                    shyps = [], 
                    hyps = [], 
                    prop = t}))
            | None => get_ax thys)
          end;
  in
    (case get_ax (theory :: Theory.ancestors_of theory) of
      Some thm => thm
    | None => raise THEORY ("No axiom " ^ quote name, [theory]))
  end;

fun def_name name = name ^ "_def";
fun get_def thy = get_axiom thy o def_name;


(*return additional axioms of this theory node*)
fun axioms_of thy =
  map (fn (s, _) => (s, get_axiom thy s))
    (Symtab.dest (#axioms (Theory.rep_theory thy)));


(* name and tags -- make proof objects more readable *)

fun get_name_tags (Thm {der, ...}) =
  (case #2 der of
    Join (Theorem x, _) => x
  | Join (Axiom x, _) => x
  | _ => ("", []));

fun put_name_tags x (Thm {sign_ref, der = (ora, der), maxidx, shyps, hyps, prop}) =
  let
    val der' =
      (case der of
        Join (Theorem _, ds) => Join (Theorem x, ds)
      | Join (Axiom _, ds) => Join (Axiom x, ds)
      | _ => Join (Theorem x, [der]));
  in
    Thm {sign_ref = sign_ref, der = (ora, der'), maxidx = maxidx,
      shyps = shyps, hyps = hyps, prop = prop}
  end;

val name_of_thm = #1 o get_name_tags;
val tags_of_thm = #2 o get_name_tags;

fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;


(*Compression of theorems -- a separate rule, not integrated with the others,
  as it could be slow.*)
fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
    Thm {sign_ref = sign_ref, 
         der = der,     (*No derivation recorded!*)
         maxidx = maxidx,
         shyps = shyps, 
         hyps = map Term.compress_term hyps, 
         prop = Term.compress_term prop};



(*** Meta rules ***)

(*Check that term does not contain same var with different typing/sorting.
  If this check must be made, recalculate maxidx in hope of preventing its
  recurrence.*)
fun nodup_vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
  Thm {sign_ref = sign_ref, 
         der = der,     
         maxidx = maxidx_of_term prop,
         shyps = shyps, 
         hyps = hyps, 
         prop = Sign.nodup_vars prop}
  handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);


(** 'primitive' rules **)

(*discharge all assumptions t from ts*)
val disch = gen_rem (op aconv);

(*The assumption rule A|-A in a theory*)
fun assume raw_ct : thm =
  let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
  in  if T<>propT then
        raise THM("assume: assumptions must have type prop", 0, [])
      else if maxidx <> ~1 then
        raise THM("assume: assumptions may not contain scheme variables",
                  maxidx, [])
      else Thm{sign_ref   = sign_ref,
               der    = infer_derivs (Assume ct, []),
               maxidx = ~1, 
               shyps  = add_term_sorts(prop,[]), 
               hyps   = [prop], 
               prop   = prop}
  end;

(*Implication introduction
    [A]
     :
     B
  -------
  A ==> B
*)
fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,prop}) : thm =
  let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
  in  if T<>propT then
        raise THM("implies_intr: assumptions must have type prop", 0, [thB])
      else
         Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
             der = infer_derivs (Implies_intr cA, [der]),
             maxidx = Int.max(maxidxA, maxidx),
             shyps = add_term_sorts (A, shyps),
             hyps = disch(hyps,A),
             prop = implies$A$prop}
      handle TERM _ =>
        raise THM("implies_intr: incompatible signatures", 0, [thB])
  end;


(*Implication elimination
  A ==> B    A
  ------------
        B
*)
fun implies_elim thAB thA : thm =
    let val Thm{maxidx=maxA, der=derA, hyps=hypsA, shyps=shypsA, prop=propA, ...} = thA
        and Thm{der, maxidx, hyps, shyps, prop, ...} = thAB;
        fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
    in  case prop of
            imp$A$B =>
                if imp=implies andalso  A aconv propA
                then
                  Thm{sign_ref= merge_thm_sgs(thAB,thA),
                      der = infer_derivs (Implies_elim, [der,derA]),
                      maxidx = Int.max(maxA,maxidx),
                      shyps = union_sort (shypsA, shyps),
                      hyps = union_term(hypsA,hyps),  (*dups suppressed*)
                      prop = B}
                else err("major premise")
          | _ => err("major premise")
    end;

(*Forall introduction.  The Free or Var x must not be free in the hypotheses.
    A
  -----
  !!x.A
*)
fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
  let val x = term_of cx;
      fun result(a,T) = fix_shyps [th] []
        (Thm{sign_ref = sign_ref, 
             der = infer_derivs (Forall_intr cx, [der]),
             maxidx = maxidx,
             shyps = [],
             hyps = hyps,
             prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
  in  case x of
        Free(a,T) =>
          if exists (apl(x, Logic.occs)) hyps
          then  raise THM("forall_intr: variable free in assumptions", 0, [th])
          else  result(a,T)
      | Var((a,_),T) => result(a,T)
      | _ => raise THM("forall_intr: not a variable", 0, [th])
  end;

(*Forall elimination
  !!x.A
  ------
  A[t/x]
*)
fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
  let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
  in  case prop of
        Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
          if T<>qary then
              raise THM("forall_elim: type mismatch", 0, [th])
          else let val thm = fix_shyps [th] []
                    (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
                         der = infer_derivs (Forall_elim ct, [der]),
                         maxidx = Int.max(maxidx, maxt),
                         shyps = [],
                         hyps = hyps,  
                         prop = betapply(A,t)})
               in if maxt >= 0 andalso maxidx >= 0
                  then nodup_vars thm "forall_elim" 
                  else thm (*no new Vars: no expensive check!*)
               end
      | _ => raise THM("forall_elim: not quantified", 0, [th])
  end
  handle TERM _ =>
         raise THM("forall_elim: incompatible signatures", 0, [th]);


(* Equality *)

(*The reflexivity rule: maps  t   to the theorem   t==t   *)
fun reflexive ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm{sign_ref= sign_ref, 
         der = infer_derivs (Reflexive ct, []),
         shyps = add_term_sorts (t, []),
         hyps = [], 
         maxidx = maxidx,
         prop = Logic.mk_equals(t,t)}
  end;

(*The symmetry rule
  t==u
  ----
  u==t
*)
fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  case prop of
      (eq as Const("==",_)) $ t $ u =>
        (*no fix_shyps*)
          Thm{sign_ref = sign_ref,
              der = infer_derivs (Symmetric, [der]),
              maxidx = maxidx,
              shyps = shyps,
              hyps = hyps,
              prop = eq$u$t}
    | _ => raise THM("symmetric", 0, [th]);

(*The transitive rule
  t1==u    u==t2
  --------------
      t1==t2
*)
fun transitive th1 th2 =
  let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, prop=prop1,...} = th1
      and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, prop=prop2,...} = th2;
      fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
  in case (prop1,prop2) of
       ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
          if not (u aconv u') then err"middle term"
          else let val thm =      
                 Thm{sign_ref= merge_thm_sgs(th1,th2), 
                     der = infer_derivs (Transitive, [der1, der2]),
                     maxidx = Int.max(max1,max2), 
                     shyps = union_sort (shyps1, shyps2),
                     hyps = union_term(hyps1,hyps2),
                     prop = eq$t1$t2}
                 in if max1 >= 0 andalso max2 >= 0
                    then nodup_vars thm "transitive" 
                    else thm (*no new Vars: no expensive check!*)
                 end
     | _ =>  err"premises"
  end;

(*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x]
  Fully beta-reduces the term if full=true
*)
fun beta_conversion full ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm
    {sign_ref = sign_ref,  
     der = infer_derivs (Beta_conversion ct, []),
     maxidx = maxidx,
     shyps = add_term_sorts (t, []),
     hyps = [],
     prop = Logic.mk_equals (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, []))}
  end;

fun eta_conversion ct =
  let val Cterm {sign_ref, t, T, maxidx} = ct
  in Thm
    {sign_ref = sign_ref,  
     der = infer_derivs (Eta_conversion ct, []),
     maxidx = maxidx,
{'fraction_non_alphanumeric': 0.12287646644015641, 'fraction_numerical': 0.004535547150458363, 'mean_word_length': 2.2866473531735583, 'pattern_counts': {'":': 2, '<': 15, '<?xml version=': 0, '>': 395, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '298074', 'n_tokens_mistral': 23126, 'n_tokens_neox': 22373, 'n_words': 6773}