src/Pure/thm.ML
author nipkow
Tue Mar 10 13:24:11 1998 +0100 (1998-03-10)
changeset 4713 bea2ab2e360b
parent 4684 eb712fef644b
child 4716 a291e858061c
permissions -rw-r--r--
New simplifier flag for mutual simplification.
     1 (*  Title:      Pure/thm.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 The core of Isabelle's Meta Logic: certified types and terms, meta
     7 theorems, meta rules (including resolution and simplification).
     8 *)
     9 
    10 signature THM =
    11   sig
    12   (*certified types*)
    13   type ctyp
    14   val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
    15   val typ_of            : ctyp -> typ
    16   val ctyp_of           : Sign.sg -> typ -> ctyp
    17   val read_ctyp         : Sign.sg -> string -> ctyp
    18 
    19   (*certified terms*)
    20   type cterm
    21   exception CTERM of string
    22   val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    23   val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
    24   val term_of           : cterm -> term
    25   val cterm_of          : Sign.sg -> term -> cterm
    26   val ctyp_of_term      : cterm -> ctyp
    27   val read_cterm        : Sign.sg -> string * typ -> cterm
    28   val cterm_fun         : (term -> term) -> (cterm -> cterm)
    29   val dest_comb         : cterm -> cterm * cterm
    30   val dest_abs          : cterm -> cterm * cterm
    31   val adjust_maxidx     : cterm -> cterm
    32   val capply            : cterm -> cterm -> cterm
    33   val cabs              : cterm -> cterm -> cterm
    34   val read_def_cterm    :
    35     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    36     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    37   val read_def_cterms   :
    38     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    39     string list -> bool -> (string * typ)list
    40     -> cterm list * (indexname * typ)list
    41 
    42   (*proof terms [must DUPLICATE declaration as a specification]*)
    43   datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
    44   val keep_derivs       : deriv_kind ref
    45   datatype rule = 
    46       MinProof                          
    47     | Oracle		  of string * Sign.sg * object
    48     | Axiom               of string
    49     | Theorem             of string       
    50     | Assume              of cterm
    51     | Implies_intr        of cterm
    52     | Implies_intr_shyps
    53     | Implies_intr_hyps
    54     | Implies_elim 
    55     | Forall_intr         of cterm
    56     | Forall_elim         of cterm
    57     | Reflexive           of cterm
    58     | Symmetric 
    59     | Transitive
    60     | Beta_conversion     of cterm
    61     | Extensional
    62     | Abstract_rule       of string * cterm
    63     | Combination
    64     | Equal_intr
    65     | Equal_elim
    66     | Trivial             of cterm
    67     | Lift_rule           of cterm * int 
    68     | Assumption          of int * Envir.env option
    69     | Rotate_rule         of int * int
    70     | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
    71     | Bicompose           of bool * bool * int * int * Envir.env
    72     | Flexflex_rule       of Envir.env            
    73     | Class_triv          of class       
    74     | VarifyT
    75     | FreezeT
    76     | RewriteC            of cterm
    77     | CongC               of cterm
    78     | Rewrite_cterm       of cterm
    79     | Rename_params_rule  of string list * int;
    80 
    81   type deriv   (* = rule mtree *)
    82 
    83   (*meta theorems*)
    84   type thm
    85   exception THM of string * int * thm list
    86   val rep_thm           : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    87                                   shyps: sort list, hyps: term list, 
    88                                   prop: term}
    89   val crep_thm          : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
    90                                   shyps: sort list, hyps: cterm list, 
    91                                   prop: cterm}
    92   val eq_thm		: thm * thm -> bool
    93   val sign_of_thm       : thm -> Sign.sg
    94   val transfer_sg	: Sign.sg -> thm -> thm
    95   val transfer		: theory -> thm -> thm
    96   val tpairs_of         : thm -> (term * term) list
    97   val prems_of          : thm -> term list
    98   val nprems_of         : thm -> int
    99   val concl_of          : thm -> term
   100   val cprop_of          : thm -> cterm
   101   val extra_shyps       : thm -> sort list
   102   val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   103   val strip_shyps       : thm -> thm
   104   val implies_intr_shyps: thm -> thm
   105   val get_axiom         : theory -> xstring -> thm
   106   val name_thm          : string * thm -> thm
   107   val name_of_thm	: thm -> string
   108   val axioms_of         : theory -> (string * thm) list
   109 
   110   (*meta rules*)
   111   val assume            : cterm -> thm
   112   val compress          : thm -> thm
   113   val implies_intr      : cterm -> thm -> thm
   114   val implies_elim      : thm -> thm -> thm
   115   val forall_intr       : cterm -> thm -> thm
   116   val forall_elim       : cterm -> thm -> thm
   117   val reflexive         : cterm -> thm
   118   val symmetric         : thm -> thm
   119   val transitive        : thm -> thm -> thm
   120   val beta_conversion   : cterm -> thm
   121   val extensional       : thm -> thm
   122   val abstract_rule     : string -> cterm -> thm -> thm
   123   val combination       : thm -> thm -> thm
   124   val equal_intr        : thm -> thm -> thm
   125   val equal_elim        : thm -> thm -> thm
   126   val implies_intr_hyps : thm -> thm
   127   val flexflex_rule     : thm -> thm Seq.seq
   128   val instantiate       :
   129     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   130   val trivial           : cterm -> thm
   131   val class_triv        : theory -> class -> thm
   132   val varifyT           : thm -> thm
   133   val freezeT           : thm -> thm
   134   val dest_state        : thm * int ->
   135     (term * term) list * term list * term * term
   136   val lift_rule         : (thm * int) -> thm -> thm
   137   val assumption        : int -> thm -> thm Seq.seq
   138   val eq_assumption     : int -> thm -> thm
   139   val rotate_rule       : int -> int -> thm -> thm
   140   val rename_params_rule: string list * int -> thm -> thm
   141   val bicompose         : bool -> bool * thm * int ->
   142     int -> thm -> thm Seq.seq
   143   val biresolution      : bool -> (bool * thm) list ->
   144     int -> thm -> thm Seq.seq
   145 
   146   (*meta simplification*)
   147   exception SIMPLIFIER of string * thm
   148   type meta_simpset
   149   val dest_mss		: meta_simpset ->
   150     {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   151   val empty_mss         : meta_simpset
   152   val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
   153   val add_simps         : meta_simpset * thm list -> meta_simpset
   154   val del_simps         : meta_simpset * thm list -> meta_simpset
   155   val mss_of            : thm list -> meta_simpset
   156   val add_congs         : meta_simpset * thm list -> meta_simpset
   157   val del_congs         : meta_simpset * thm list -> meta_simpset
   158   val add_simprocs	: meta_simpset *
   159     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
   160       -> meta_simpset
   161   val del_simprocs	: meta_simpset *
   162     (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
   163       -> meta_simpset
   164   val add_prems         : meta_simpset * thm list -> meta_simpset
   165   val prems_of_mss      : meta_simpset -> thm list
   166   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
   167   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   168   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   169   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   170   val trace_simp        : bool ref
   171   val rewrite_cterm     : bool * bool * bool -> meta_simpset ->
   172                           (meta_simpset -> thm -> thm option) -> cterm -> thm
   173 
   174   val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
   175 end;
   176 
   177 structure Thm: THM =
   178 struct
   179 
   180 (*** Certified terms and types ***)
   181 
   182 (** certified types **)
   183 
   184 (*certified typs under a signature*)
   185 
   186 datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
   187 
   188 fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
   189 fun typ_of (Ctyp {T, ...}) = T;
   190 
   191 fun ctyp_of sign T =
   192   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
   193 
   194 fun read_ctyp sign s =
   195   Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
   196 
   197 
   198 
   199 (** certified terms **)
   200 
   201 (*certified terms under a signature, with checked typ and maxidx of Vars*)
   202 
   203 datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
   204 
   205 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   206   {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
   207 
   208 fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   209   {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
   210     maxidx = maxidx};
   211 
   212 fun term_of (Cterm {t, ...}) = t;
   213 
   214 fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
   215 
   216 (*create a cterm by checking a "raw" term with respect to a signature*)
   217 fun cterm_of sign tm =
   218   let val (t, T, maxidx) = Sign.certify_term sign tm
   219   in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
   220   end;
   221 
   222 fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
   223 
   224 
   225 exception CTERM of string;
   226 
   227 (*Destruct application in cterms*)
   228 fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
   229       let val typeA = fastype_of A;
   230           val typeB =
   231             case typeA of Type("fun",[S,T]) => S
   232                         | _ => error "Function type expected in dest_comb";
   233       in
   234       (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
   235        Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
   236       end
   237   | dest_comb _ = raise CTERM "dest_comb";
   238 
   239 (*Destruct abstraction in cterms*)
   240 fun dest_abs (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
   241       let val (y,N) = variant_abs (x,ty,M)
   242       in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
   243           Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
   244       end
   245   | dest_abs _ = raise CTERM "dest_abs";
   246 
   247 (*Makes maxidx precise: it is often too big*)
   248 fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
   249   if maxidx = ~1 then ct 
   250   else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
   251 
   252 (*Form cterm out of a function and an argument*)
   253 fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   254            (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
   255       if T = dty then Cterm{t=f$x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
   256                             maxidx=Int.max(maxidx1, maxidx2)}
   257       else raise CTERM "capply: types don't agree"
   258   | capply _ _ = raise CTERM "capply: first arg is not a function"
   259 
   260 fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
   261          (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
   262       Cterm {t=absfree(a,ty,t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
   263              T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   264   | cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
   265 
   266 
   267 
   268 (** read cterms **)   (*exception ERROR*)
   269 
   270 (*read terms, infer types, certify terms*)
   271 fun read_def_cterms (sign, types, sorts) used freeze sTs =
   272   let
   273     val syn = #syn (Sign.rep_sg sign)
   274     fun read(s,T) =
   275       let val T' = Sign.certify_typ sign T
   276                    handle TYPE (msg, _, _) => error msg
   277       in (Syntax.read syn T' s, T') end
   278     val tsTs = map read sTs
   279     val (ts',tye) = Sign.infer_types_simult sign types sorts used freeze tsTs;
   280     val cts = map (cterm_of sign) ts'
   281       handle TYPE (msg, _, _) => error msg
   282            | TERM (msg, _) => error msg;
   283   in (cts, tye) end;
   284 
   285 (*read term, infer types, certify term*)
   286 fun read_def_cterm args used freeze aT =
   287   let val ([ct],tye) = read_def_cterms args used freeze [aT]
   288   in (ct,tye) end;
   289 
   290 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
   291 
   292 
   293 
   294 (*** Derivations ***)
   295 
   296 (*Names of rules in derivations.  Includes logically trivial rules, if 
   297   executed in ML.*)
   298 datatype rule = 
   299     MinProof                            (*for building minimal proof terms*)
   300   | Oracle              of string * Sign.sg * object       (*oracles*)
   301 (*Axioms/theorems*)
   302   | Axiom               of string
   303   | Theorem             of string
   304 (*primitive inferences and compound versions of them*)
   305   | Assume              of cterm
   306   | Implies_intr        of cterm
   307   | Implies_intr_shyps
   308   | Implies_intr_hyps
   309   | Implies_elim 
   310   | Forall_intr         of cterm
   311   | Forall_elim         of cterm
   312   | Reflexive           of cterm
   313   | Symmetric 
   314   | Transitive
   315   | Beta_conversion     of cterm
   316   | Extensional
   317   | Abstract_rule       of string * cterm
   318   | Combination
   319   | Equal_intr
   320   | Equal_elim
   321 (*derived rules for tactical proof*)
   322   | Trivial             of cterm
   323         (*For lift_rule, the proof state is not a premise.
   324           Use cterm instead of thm to avoid mutual recursion.*)
   325   | Lift_rule           of cterm * int 
   326   | Assumption          of int * Envir.env option (*includes eq_assumption*)
   327   | Rotate_rule         of int * int
   328   | Instantiate         of (indexname * ctyp) list * (cterm * cterm) list
   329   | Bicompose           of bool * bool * int * int * Envir.env
   330   | Flexflex_rule       of Envir.env            (*identifies unifier chosen*)
   331 (*other derived rules*)
   332   | Class_triv          of class
   333   | VarifyT
   334   | FreezeT
   335 (*for the simplifier*)
   336   | RewriteC            of cterm
   337   | CongC               of cterm
   338   | Rewrite_cterm       of cterm
   339 (*Logical identities, recorded since they are part of the proof process*)
   340   | Rename_params_rule  of string list * int;
   341 
   342 
   343 type deriv = rule mtree;
   344 
   345 datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
   346 
   347 val keep_derivs = ref MinDeriv;
   348 
   349 
   350 (*Build a minimal derivation.  Keep oracles; suppress atomic inferences;
   351   retain Theorems or their underlying links; keep anything else*)
   352 fun squash_derivs [] = []
   353   | squash_derivs (der::ders) =
   354      (case der of
   355           Join (Oracle _, _) => der :: squash_derivs ders
   356         | Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
   357                                       then der :: squash_derivs ders
   358                                       else squash_derivs (der'::ders)
   359         | Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
   360                                then der :: squash_derivs ders
   361                                else squash_derivs ders
   362         | Join (_, [])      => squash_derivs ders
   363         | _                 => der :: squash_derivs ders);
   364 
   365 
   366 (*Ensure sharing of the most likely derivation, the empty one!*)
   367 val min_infer = Join (MinProof, []);
   368 
   369 (*Make a minimal inference*)
   370 fun make_min_infer []    = min_infer
   371   | make_min_infer [der] = der
   372   | make_min_infer ders  = Join (MinProof, ders);
   373 
   374 fun infer_derivs (rl, [])   = Join (rl, [])
   375   | infer_derivs (rl, ders) =
   376     if !keep_derivs=FullDeriv then Join (rl, ders)
   377     else make_min_infer (squash_derivs ders);
   378 
   379 
   380 
   381 (*** Meta theorems ***)
   382 
   383 datatype thm = Thm of
   384  {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
   385   der: deriv,                  (*derivation*)
   386   maxidx: int,                 (*maximum index of any Var or TVar*)
   387   shyps: sort list,            (*sort hypotheses*)
   388   hyps: term list,             (*hypotheses*)
   389   prop: term};                 (*conclusion*)
   390 
   391 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   392   {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
   393     shyps = shyps, hyps = hyps, prop = prop};
   394 
   395 (*Version of rep_thm returning cterms instead of terms*)
   396 fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   397   let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
   398   in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
   399       hyps = map (ctermf ~1) hyps,
   400       prop = ctermf maxidx prop}
   401   end;
   402 
   403 (*errors involving theorems*)
   404 exception THM of string * int * thm list;
   405 
   406 (*equality of theorems uses equality of signatures and the
   407   a-convertible test for terms*)
   408 fun eq_thm (th1, th2) =
   409   let
   410     val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1;
   411     val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2;
   412   in
   413     Sign.eq_sg (sg1, sg2) andalso
   414     eq_set_sort (shyps1, shyps2) andalso
   415     aconvs (hyps1, hyps2) andalso
   416     prop1 aconv prop2
   417   end;
   418 
   419 fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   420 
   421 (*merge signatures of two theorems; raise exception if incompatible*)
   422 fun merge_thm_sgs
   423     (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   424   Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   425 
   426 (*transfer thm to super theory (non-destructive)*)
   427 fun transfer_sg sign' thm =
   428   let
   429     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   430     val sign = Sign.deref sign_ref;
   431   in
   432     if Sign.eq_sg (sign, sign') then thm
   433     else if Sign.subsig (sign, sign') then
   434       Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
   435         shyps = shyps, hyps = hyps, prop = prop}
   436     else raise THM ("transfer: not a super theory", 0, [thm])
   437   end;
   438 
   439 val transfer = transfer_sg o sign_of;
   440 
   441 (*maps object-rule to tpairs*)
   442 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
   443 
   444 (*maps object-rule to premises*)
   445 fun prems_of (Thm {prop, ...}) =
   446   Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   447 
   448 (*counts premises in a rule*)
   449 fun nprems_of (Thm {prop, ...}) =
   450   Logic.count_prems (Logic.skip_flexpairs prop, 0);
   451 
   452 (*maps object-rule to conclusion*)
   453 fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   454 
   455 (*the statement of any thm is a cterm*)
   456 fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
   457   Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
   458 
   459 
   460 
   461 (** sort contexts of theorems **)
   462 
   463 (* basic utils *)
   464 
   465 (*accumulate sorts suppressing duplicates; these are coded low levelly
   466   to improve efficiency a bit*)
   467 
   468 fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss)
   469   | add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss)
   470   | add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss)
   471 and add_typs_sorts ([], Ss) = Ss
   472   | add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss));
   473 
   474 fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss)
   475   | add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss)
   476   | add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss)
   477   | add_term_sorts (Bound _, Ss) = Ss
   478   | add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss))
   479   | add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss));
   480 
   481 fun add_terms_sorts ([], Ss) = Ss
   482   | add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss));
   483 
   484 fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs;
   485 
   486 fun add_env_sorts (env, Ss) =
   487   add_terms_sorts (map snd (Envir.alist_of env),
   488     add_typs_sorts (env_codT env, Ss));
   489 
   490 fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) =
   491   add_terms_sorts (hyps, add_term_sorts (prop, Ss));
   492 
   493 fun add_thms_shyps ([], Ss) = Ss
   494   | add_thms_shyps (Thm {shyps, ...} :: ths, Ss) =
   495       add_thms_shyps (ths, union_sort(shyps,Ss));
   496 
   497 
   498 (*get 'dangling' sort constraints of a thm*)
   499 fun extra_shyps (th as Thm {shyps, ...}) =
   500   shyps \\ add_thm_sorts (th, []);
   501 
   502 
   503 (* fix_shyps *)
   504 
   505 (*preserve sort contexts of rule premises and substituted types*)
   506 fun fix_shyps thms Ts thm =
   507   let
   508     val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm;
   509     val shyps =
   510       add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
   511   in
   512     Thm {sign_ref = sign_ref,
   513          der = der,             (*No new derivation, as other rules call this*)
   514          maxidx = maxidx,
   515          shyps = shyps, hyps = hyps, prop = prop}
   516   end;
   517 
   518 
   519 (* strip_shyps *)       (* FIXME improve? (e.g. only minimal extra sorts) *)
   520 
   521 val force_strip_shyps = ref true;  (* FIXME tmp (since 1995/08/01) *)
   522 
   523 (*remove extra sorts that are known to be syntactically non-empty*)
   524 fun strip_shyps thm =
   525   let
   526     val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   527     val sorts = add_thm_sorts (thm, []);
   528     val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts;
   529     val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
   530   in
   531     Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
   532          shyps =
   533          (if eq_set_sort (shyps',sorts) orelse 
   534              not (!force_strip_shyps) then shyps'
   535           else    (* FIXME tmp (since 1995/08/01) *)
   536               (warning ("Removed sort hypotheses: " ^
   537                         commas (map Sorts.str_of_sort (shyps' \\ sorts)));
   538                warning "Let's hope these sorts are non-empty!";
   539            sorts)),
   540       hyps = hyps, 
   541       prop = prop}
   542   end;
   543 
   544 
   545 (* implies_intr_shyps *)
   546 
   547 (*discharge all extra sort hypotheses*)
   548 fun implies_intr_shyps thm =
   549   (case extra_shyps thm of
   550     [] => thm
   551   | xshyps =>
   552       let
   553         val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
   554         val shyps' = ins_sort (logicS, shyps \\ xshyps);
   555         val used_names = foldr add_term_tfree_names (prop :: hyps, []);
   556         val names =
   557           tl (variantlist (replicate (length xshyps + 1) "'", used_names));
   558         val tfrees = map (TFree o rpair logicS) names;
   559 
   560         fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
   561         val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
   562       in
   563         Thm {sign_ref = sign_ref, 
   564              der = infer_derivs (Implies_intr_shyps, [der]), 
   565              maxidx = maxidx, 
   566              shyps = shyps',
   567              hyps = hyps, 
   568              prop = Logic.list_implies (sort_hyps, prop)}
   569       end);
   570 
   571 
   572 (** Axioms **)
   573 
   574 (*look up the named axiom in the theory*)
   575 fun get_axiom theory raw_name =
   576   let
   577     val name = Sign.intern (sign_of theory) Theory.axiomK raw_name;
   578     fun get_ax [] = raise Match
   579       | get_ax (thy :: thys) =
   580           let val {sign, axioms, parents, ...} = rep_theory thy
   581           in case Symtab.lookup (axioms, name) of
   582                 Some t => fix_shyps [] []
   583                            (Thm {sign_ref = Sign.self_ref sign,
   584                                  der = infer_derivs (Axiom name, []),
   585                                  maxidx = maxidx_of_term t,
   586                                  shyps = [], 
   587                                  hyps = [], 
   588                                  prop = t})
   589               | None => get_ax parents handle Match => get_ax thys
   590           end;
   591   in
   592     get_ax [theory] handle Match
   593       => raise THEORY ("No axiom " ^ quote name, [theory])
   594   end;
   595 
   596 
   597 (*return additional axioms of this theory node*)
   598 fun axioms_of thy =
   599   map (fn (s, _) => (s, get_axiom thy s))
   600     (Symtab.dest (#axioms (rep_theory thy)));
   601 
   602 (*Attach a label to a theorem to make proof objects more readable*)
   603 fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   604   (case der of
   605     Join (Theorem _, _) => th
   606   | Join (Axiom _, _) => th
   607   | _ => Thm {sign_ref = sign_ref, der = Join (Theorem name, [der]),
   608       maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop});
   609 
   610 fun name_of_thm (Thm {der, ...}) =
   611   (case der of
   612     Join (Theorem name, _) => name
   613   | Join (Axiom name, _) => name
   614   | _ => "");
   615 
   616 
   617 (*Compression of theorems -- a separate rule, not integrated with the others,
   618   as it could be slow.*)
   619 fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
   620     Thm {sign_ref = sign_ref, 
   621          der = der,     (*No derivation recorded!*)
   622          maxidx = maxidx,
   623          shyps = shyps, 
   624          hyps = map Term.compress_term hyps, 
   625          prop = Term.compress_term prop};
   626 
   627 
   628 
   629 (*** Meta rules ***)
   630 
   631 (*Check that term does not contain same var with different typing/sorting.
   632   If this check must be made, recalculate maxidx in hope of preventing its
   633   recurrence.*)
   634 fun nodup_Vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
   635   (Sign.nodup_Vars prop; 
   636    Thm {sign_ref = sign_ref, 
   637          der = der,     
   638          maxidx = maxidx_of_term prop,
   639          shyps = shyps, 
   640          hyps = hyps, 
   641          prop = prop})
   642   handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts);
   643 
   644 (** 'primitive' rules **)
   645 
   646 (*discharge all assumptions t from ts*)
   647 val disch = gen_rem (op aconv);
   648 
   649 (*The assumption rule A|-A in a theory*)
   650 fun assume ct : thm =
   651   let val Cterm {sign_ref, t=prop, T, maxidx} = ct
   652   in  if T<>propT then
   653         raise THM("assume: assumptions must have type prop", 0, [])
   654       else if maxidx <> ~1 then
   655         raise THM("assume: assumptions may not contain scheme variables",
   656                   maxidx, [])
   657       else Thm{sign_ref   = sign_ref,
   658                der    = infer_derivs (Assume ct, []), 
   659                maxidx = ~1, 
   660                shyps  = add_term_sorts(prop,[]), 
   661                hyps   = [prop], 
   662                prop   = prop}
   663   end;
   664 
   665 (*Implication introduction
   666     [A]
   667      :
   668      B
   669   -------
   670   A ==> B
   671 *)
   672 fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   673   let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
   674   in  if T<>propT then
   675         raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   676       else fix_shyps [thB] []
   677         (Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
   678              der = infer_derivs (Implies_intr cA, [der]),
   679              maxidx = Int.max(maxidxA, maxidx),
   680              shyps = [],
   681              hyps = disch(hyps,A),
   682              prop = implies$A$prop})
   683       handle TERM _ =>
   684         raise THM("implies_intr: incompatible signatures", 0, [thB])
   685   end;
   686 
   687 
   688 (*Implication elimination
   689   A ==> B    A
   690   ------------
   691         B
   692 *)
   693 fun implies_elim thAB thA : thm =
   694     let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA
   695         and Thm{sign_ref, der, maxidx, hyps, prop,...} = thAB;
   696         fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   697     in  case prop of
   698             imp$A$B =>
   699                 if imp=implies andalso  A aconv propA
   700                 then fix_shyps [thAB, thA] []
   701                        (Thm{sign_ref= merge_thm_sgs(thAB,thA),
   702                             der = infer_derivs (Implies_elim, [der,derA]),
   703                             maxidx = Int.max(maxA,maxidx),
   704                             shyps = [],
   705                             hyps = union_term(hypsA,hyps),  (*dups suppressed*)
   706                             prop = B})
   707                 else err("major premise")
   708           | _ => err("major premise")
   709     end;
   710 
   711 (*Forall introduction.  The Free or Var x must not be free in the hypotheses.
   712     A
   713   -----
   714   !!x.A
   715 *)
   716 fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   717   let val x = term_of cx;
   718       fun result(a,T) = fix_shyps [th] []
   719         (Thm{sign_ref = sign_ref, 
   720              der = infer_derivs (Forall_intr cx, [der]),
   721              maxidx = maxidx,
   722              shyps = [],
   723              hyps = hyps,
   724              prop = all(T) $ Abs(a, T, abstract_over (x,prop))})
   725   in  case x of
   726         Free(a,T) =>
   727           if exists (apl(x, Logic.occs)) hyps
   728           then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   729           else  result(a,T)
   730       | Var((a,_),T) => result(a,T)
   731       | _ => raise THM("forall_intr: not a variable", 0, [th])
   732   end;
   733 
   734 (*Forall elimination
   735   !!x.A
   736   ------
   737   A[t/x]
   738 *)
   739 fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
   740   let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
   741   in  case prop of
   742         Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   743           if T<>qary then
   744               raise THM("forall_elim: type mismatch", 0, [th])
   745           else let val thm = fix_shyps [th] []
   746                     (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   747                          der = infer_derivs (Forall_elim ct, [der]),
   748                          maxidx = Int.max(maxidx, maxt),
   749                          shyps = [],
   750                          hyps = hyps,  
   751                          prop = betapply(A,t)})
   752                in if maxt >= 0 andalso maxidx >= 0
   753                   then nodup_Vars thm "forall_elim" 
   754                   else thm (*no new Vars: no expensive check!*)
   755                end
   756       | _ => raise THM("forall_elim: not quantified", 0, [th])
   757   end
   758   handle TERM _ =>
   759          raise THM("forall_elim: incompatible signatures", 0, [th]);
   760 
   761 
   762 (* Equality *)
   763 
   764 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   765 fun reflexive ct =
   766   let val Cterm {sign_ref, t, T, maxidx} = ct
   767   in  fix_shyps [] []
   768        (Thm{sign_ref= sign_ref, 
   769             der = infer_derivs (Reflexive ct, []),
   770             shyps = [],
   771             hyps = [], 
   772             maxidx = maxidx,
   773             prop = Logic.mk_equals(t,t)})
   774   end;
   775 
   776 (*The symmetry rule
   777   t==u
   778   ----
   779   u==t
   780 *)
   781 fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
   782   case prop of
   783       (eq as Const("==",_)) $ t $ u =>
   784         (*no fix_shyps*)
   785           Thm{sign_ref = sign_ref,
   786               der = infer_derivs (Symmetric, [der]),
   787               maxidx = maxidx,
   788               shyps = shyps,
   789               hyps = hyps,
   790               prop = eq$u$t}
   791     | _ => raise THM("symmetric", 0, [th]);
   792 
   793 (*The transitive rule
   794   t1==u    u==t2
   795   --------------
   796       t1==t2
   797 *)
   798 fun transitive th1 th2 =
   799   let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   800       and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   801       fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   802   in case (prop1,prop2) of
   803        ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   804           if not (u aconv u') then err"middle term"
   805           else let val thm =      
   806               fix_shyps [th1, th2] []
   807                 (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   808                      der = infer_derivs (Transitive, [der1, der2]),
   809                      maxidx = Int.max(max1,max2), 
   810                      shyps = [],
   811                      hyps = union_term(hyps1,hyps2),
   812                      prop = eq$t1$t2})
   813                  in if max1 >= 0 andalso max2 >= 0
   814                     then nodup_Vars thm "transitive" 
   815                     else thm (*no new Vars: no expensive check!*)
   816                  end
   817      | _ =>  err"premises"
   818   end;
   819 
   820 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
   821 fun beta_conversion ct =
   822   let val Cterm {sign_ref, t, T, maxidx} = ct
   823   in  case t of
   824           Abs(_,_,bodt) $ u => fix_shyps [] []
   825             (Thm{sign_ref = sign_ref,  
   826                  der = infer_derivs (Beta_conversion ct, []),
   827                  maxidx = maxidx,
   828                  shyps = [],
   829                  hyps = [],
   830                  prop = Logic.mk_equals(t, subst_bound (u,bodt))})
   831         | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   832   end;
   833 
   834 (*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
   835   f(x) == g(x)
   836   ------------
   837      f == g
   838 *)
   839 fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) =
   840   case prop of
   841     (Const("==",_)) $ (f$x) $ (g$y) =>
   842       let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
   843       in (if x<>y then err"different variables" else
   844           case y of
   845                 Free _ =>
   846                   if exists (apl(y, Logic.occs)) (f::g::hyps)
   847                   then err"variable free in hyps or functions"    else  ()
   848               | Var _ =>
   849                   if Logic.occs(y,f)  orelse  Logic.occs(y,g)
   850                   then err"variable free in functions"   else  ()
   851               | _ => err"not a variable");
   852           (*no fix_shyps*)
   853           Thm{sign_ref = sign_ref,
   854               der = infer_derivs (Extensional, [der]),
   855               maxidx = maxidx,
   856               shyps = shyps,
   857               hyps = hyps, 
   858               prop = Logic.mk_equals(f,g)}
   859       end
   860  | _ =>  raise THM("extensional: premise", 0, [th]);
   861 
   862 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   863   The bound variable will be named "a" (since x will be something like x320)
   864      t == u
   865   ------------
   866   %x.t == %x.u
   867 *)
   868 fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
   869   let val x = term_of cx;
   870       val (t,u) = Logic.dest_equals prop
   871             handle TERM _ =>
   872                 raise THM("abstract_rule: premise not an equality", 0, [th])
   873       fun result T = fix_shyps [th] []
   874           (Thm{sign_ref = sign_ref,
   875                der = infer_derivs (Abstract_rule (a,cx), [der]),
   876                maxidx = maxidx, 
   877                shyps = [], 
   878                hyps = hyps,
   879                prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   880                                       Abs(a, T, abstract_over (x,u)))})
   881   in  case x of
   882         Free(_,T) =>
   883          if exists (apl(x, Logic.occs)) hyps
   884          then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   885          else result T
   886       | Var(_,T) => result T
   887       | _ => raise THM("abstract_rule: not a variable", 0, [th])
   888   end;
   889 
   890 (*The combination rule
   891   f == g  t == u
   892   --------------
   893    f(t) == g(u)
   894 *)
   895 fun combination th1 th2 =
   896   let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   897               prop=prop1,...} = th1
   898       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   899               prop=prop2,...} = th2
   900       fun chktypes (f,t) =
   901             (case fastype_of f of
   902                 Type("fun",[T1,T2]) => 
   903                     if T1 <> fastype_of t then
   904                          raise THM("combination: types", 0, [th1,th2])
   905                     else ()
   906                 | _ => raise THM("combination: not function type", 0, 
   907                                  [th1,th2]))
   908   in case (prop1,prop2)  of
   909        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   910           let val _   = chktypes (f,t)
   911               val thm = (*no fix_shyps*)
   912                         Thm{sign_ref = merge_thm_sgs(th1,th2), 
   913                             der = infer_derivs (Combination, [der1, der2]),
   914                             maxidx = Int.max(max1,max2), 
   915                             shyps = union_sort(shyps1,shyps2),
   916                             hyps = union_term(hyps1,hyps2),
   917                             prop = Logic.mk_equals(f$t, g$u)}
   918           in if max1 >= 0 andalso max2 >= 0
   919              then nodup_Vars thm "combination" 
   920              else thm (*no new Vars: no expensive check!*)  
   921           end
   922      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   923   end;
   924 
   925 
   926 (* Equality introduction
   927   A ==> B  B ==> A
   928   ----------------
   929        A == B
   930 *)
   931 fun equal_intr th1 th2 =
   932   let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
   933               prop=prop1,...} = th1
   934       and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   935               prop=prop2,...} = th2;
   936       fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   937   in case (prop1,prop2) of
   938        (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   939           if A aconv A' andalso B aconv B'
   940           then
   941             (*no fix_shyps*)
   942               Thm{sign_ref = merge_thm_sgs(th1,th2),
   943                   der = infer_derivs (Equal_intr, [der1, der2]),
   944                   maxidx = Int.max(max1,max2),
   945                   shyps = union_sort(shyps1,shyps2),
   946                   hyps = union_term(hyps1,hyps2),
   947                   prop = Logic.mk_equals(A,B)}
   948           else err"not equal"
   949      | _ =>  err"premises"
   950   end;
   951 
   952 
   953 (*The equal propositions rule
   954   A == B  A
   955   ---------
   956       B
   957 *)
   958 fun equal_elim th1 th2 =
   959   let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   960       and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   961       fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   962   in  case prop1  of
   963        Const("==",_) $ A $ B =>
   964           if not (prop2 aconv A) then err"not equal"  else
   965             fix_shyps [th1, th2] []
   966               (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   967                    der = infer_derivs (Equal_elim, [der1, der2]),
   968                    maxidx = Int.max(max1,max2),
   969                    shyps = [],
   970                    hyps = union_term(hyps1,hyps2),
   971                    prop = B})
   972      | _ =>  err"major premise"
   973   end;
   974 
   975 
   976 
   977 (**** Derived rules ****)
   978 
   979 (*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
   980   Repeated hypotheses are discharged only once;  fold cannot do this*)
   981 fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) =
   982       implies_intr_hyps (*no fix_shyps*)
   983             (Thm{sign_ref = sign_ref, 
   984                  der = infer_derivs (Implies_intr_hyps, [der]), 
   985                  maxidx = maxidx, 
   986                  shyps = shyps,
   987                  hyps = disch(As,A),  
   988                  prop = implies$A$prop})
   989   | implies_intr_hyps th = th;
   990 
   991 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   992   Instantiates the theorem and deletes trivial tpairs.
   993   Resulting sequence may contain multiple elements if the tpairs are
   994     not all flex-flex. *)
   995 fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) =
   996   let fun newthm env =
   997           if Envir.is_empty env then th
   998           else
   999           let val (tpairs,horn) =
  1000                         Logic.strip_flexpairs (Envir.norm_term env prop)
  1001                 (*Remove trivial tpairs, of the form t=t*)
  1002               val distpairs = filter (not o op aconv) tpairs
  1003               val newprop = Logic.list_flexpairs(distpairs, horn)
  1004           in  fix_shyps [th] (env_codT env)
  1005                 (Thm{sign_ref = sign_ref, 
  1006                      der = infer_derivs (Flexflex_rule env, [der]), 
  1007                      maxidx = maxidx_of_term newprop, 
  1008                      shyps = [], 
  1009                      hyps = hyps,
  1010                      prop = newprop})
  1011           end;
  1012       val (tpairs,_) = Logic.strip_flexpairs prop
  1013   in Seq.map newthm
  1014             (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
  1015   end;
  1016 
  1017 (*Instantiation of Vars
  1018            A
  1019   -------------------
  1020   A[t1/v1,....,tn/vn]
  1021 *)
  1022 
  1023 (*Check that all the terms are Vars and are distinct*)
  1024 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
  1025 
  1026 (*For instantiate: process pair of cterms, merge theories*)
  1027 fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
  1028   let val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
  1029       and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu
  1030   in
  1031     if T=U then
  1032       (Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)), (t,u)::tpairs)
  1033     else raise TYPE("add_ctpair", [T,U], [t,u])
  1034   end;
  1035 
  1036 fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
  1037   let val Ctyp {T,sign_ref} = ctyp
  1038   in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
  1039 
  1040 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
  1041   Instantiates distinct Vars by terms of same type.
  1042   Normalizes the new theorem! *)
  1043 fun instantiate ([], []) th = th
  1044   | instantiate (vcTs,ctpairs)  (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
  1045   let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
  1046       val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
  1047       val newprop =
  1048             Envir.norm_term (Envir.empty 0)
  1049               (subst_atomic tpairs
  1050                (Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop))
  1051       val newth =
  1052             fix_shyps [th] (map snd vTs)
  1053               (Thm{sign_ref = newsign_ref, 
  1054                    der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
  1055                    maxidx = maxidx_of_term newprop, 
  1056                    shyps = [],
  1057                    hyps = hyps,
  1058                    prop = newprop})
  1059   in  if not(instl_ok(map #1 tpairs))
  1060       then raise THM("instantiate: variables not distinct", 0, [th])
  1061       else if not(null(findrep(map #1 vTs)))
  1062       then raise THM("instantiate: type variables not distinct", 0, [th])
  1063       else nodup_Vars newth "instantiate"
  1064   end
  1065   handle TERM _ =>
  1066            raise THM("instantiate: incompatible signatures",0,[th])
  1067        | TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, 
  1068 				     0, [th]);
  1069 
  1070 (*The trivial implication A==>A, justified by assume and forall rules.
  1071   A can contain Vars, not so for assume!   *)
  1072 fun trivial ct : thm =
  1073   let val Cterm {sign_ref, t=A, T, maxidx} = ct
  1074   in  if T<>propT then
  1075             raise THM("trivial: the term must have type prop", 0, [])
  1076       else fix_shyps [] []
  1077         (Thm{sign_ref = sign_ref, 
  1078              der = infer_derivs (Trivial ct, []), 
  1079              maxidx = maxidx, 
  1080              shyps = [], 
  1081              hyps = [],
  1082              prop = implies$A$A})
  1083   end;
  1084 
  1085 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
  1086 fun class_triv thy c =
  1087   let val sign = sign_of thy;
  1088       val Cterm {sign_ref, t, maxidx, ...} =
  1089           cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
  1090             handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
  1091   in
  1092     fix_shyps [] []
  1093       (Thm {sign_ref = sign_ref, 
  1094             der = infer_derivs (Class_triv c, []), 
  1095             maxidx = maxidx, 
  1096             shyps = [], 
  1097             hyps = [], 
  1098             prop = t})
  1099   end;
  1100 
  1101 
  1102 (* Replace all TFrees not in the hyps by new TVars *)
  1103 fun varifyT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  1104   let val tfrees = foldr add_term_tfree_names (hyps,[])
  1105   in let val thm = (*no fix_shyps*)
  1106     Thm{sign_ref = sign_ref, 
  1107         der = infer_derivs (VarifyT, [der]), 
  1108         maxidx = Int.max(0,maxidx), 
  1109         shyps = shyps, 
  1110         hyps = hyps,
  1111         prop = Type.varify(prop,tfrees)}
  1112      in nodup_Vars thm "varifyT" end
  1113 (* this nodup_Vars check can be removed if thms are guaranteed not to contain
  1114 duplicate TVars with differnt sorts *)
  1115   end;
  1116 
  1117 (* Replace all TVars by new TFrees *)
  1118 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
  1119   let val (prop',_) = Type.freeze_thaw prop
  1120   in (*no fix_shyps*)
  1121     Thm{sign_ref = sign_ref, 
  1122         der = infer_derivs (FreezeT, [der]),
  1123         maxidx = maxidx_of_term prop',
  1124         shyps = shyps,
  1125         hyps = hyps,
  1126         prop = prop'}
  1127   end;
  1128 
  1129 
  1130 (*** Inference rules for tactics ***)
  1131 
  1132 (*Destruct proof state into constraints, other goals, goal(i), rest *)
  1133 fun dest_state (state as Thm{prop,...}, i) =
  1134   let val (tpairs,horn) = Logic.strip_flexpairs prop
  1135   in  case  Logic.strip_prems(i, [], horn) of
  1136           (B::rBs, C) => (tpairs, rev rBs, B, C)
  1137         | _ => raise THM("dest_state", i, [state])
  1138   end
  1139   handle TERM _ => raise THM("dest_state", i, [state]);
  1140 
  1141 (*Increment variables and parameters of orule as required for
  1142   resolution with goal i of state. *)
  1143 fun lift_rule (state, i) orule =
  1144   let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
  1145       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
  1146         handle TERM _ => raise THM("lift_rule", i, [orule,state])
  1147       val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
  1148       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
  1149       val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule
  1150       val (tpairs,As,B) = Logic.strip_horn prop
  1151   in  (*no fix_shyps*)
  1152       Thm{sign_ref = merge_thm_sgs(state,orule),
  1153           der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
  1154           maxidx = maxidx+smax+1,
  1155           shyps=union_sort(sshyps,shyps), 
  1156           hyps=hyps, 
  1157           prop = Logic.rule_of (map (pairself lift_abs) tpairs,
  1158                                 map lift_all As,    
  1159                                 lift_all B)}
  1160   end;
  1161 
  1162 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  1163 fun assumption i state =
  1164   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1165       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1166       fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
  1167         fix_shyps [state] (env_codT env)
  1168           (Thm{sign_ref = sign_ref, 
  1169                der = infer_derivs (Assumption (i, Some env), [der]),
  1170                maxidx = maxidx,
  1171                shyps = [],
  1172                hyps = hyps,
  1173                prop = 
  1174                if Envir.is_empty env then (*avoid wasted normalizations*)
  1175                    Logic.rule_of (tpairs, Bs, C)
  1176                else (*normalize the new rule fully*)
  1177                    Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))});
  1178       fun addprfs [] = Seq.empty
  1179         | addprfs ((t,u)::apairs) = Seq.make (fn()=> Seq.pull
  1180              (Seq.mapp newth
  1181                 (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
  1182                 (addprfs apairs)))
  1183   in  addprfs (Logic.assum_pairs Bi)  end;
  1184 
  1185 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  1186   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  1187 fun eq_assumption i state =
  1188   let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  1189       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1190   in  if exists (op aconv) (Logic.assum_pairs Bi)
  1191       then fix_shyps [state] []
  1192              (Thm{sign_ref = sign_ref, 
  1193                   der = infer_derivs (Assumption (i,None), [der]),
  1194                   maxidx = maxidx,
  1195                   shyps = [],
  1196                   hyps = hyps,
  1197                   prop = Logic.rule_of(tpairs, Bs, C)})
  1198       else  raise THM("eq_assumption", 0, [state])
  1199   end;
  1200 
  1201 
  1202 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  1203 fun rotate_rule k i state =
  1204   let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
  1205       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1206       val params = Logic.strip_params Bi
  1207       and asms   = Logic.strip_assums_hyp Bi
  1208       and concl  = Logic.strip_assums_concl Bi
  1209       val n      = length asms
  1210       fun rot m  = if 0=m orelse m=n then Bi
  1211 		   else if 0<m andalso m<n 
  1212 		   then list_all 
  1213 			   (params, 
  1214 			    Logic.list_implies(List.drop(asms, m) @ 
  1215 					       List.take(asms, m),
  1216 					       concl))
  1217 		   else raise THM("rotate_rule", m, [state])
  1218   in  Thm{sign_ref = sign_ref, 
  1219 	  der = infer_derivs (Rotate_rule (k,i), [der]),
  1220 	  maxidx = maxidx,
  1221 	  shyps = shyps,
  1222 	  hyps = hyps,
  1223 	  prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)}
  1224   end;
  1225 
  1226 
  1227 (** User renaming of parameters in a subgoal **)
  1228 
  1229 (*Calls error rather than raising an exception because it is intended
  1230   for top-level use -- exception handling would not make sense here.
  1231   The names in cs, if distinct, are used for the innermost parameters;
  1232    preceding parameters may be renamed to make all params distinct.*)
  1233 fun rename_params_rule (cs, i) state =
  1234   let val Thm{sign_ref,der,maxidx,hyps,...} = state
  1235       val (tpairs, Bs, Bi, C) = dest_state(state,i)
  1236       val iparams = map #1 (Logic.strip_params Bi)
  1237       val short = length iparams - length cs
  1238       val newnames =
  1239             if short<0 then error"More names than abstractions!"
  1240             else variantlist(take (short,iparams), cs) @ cs
  1241       val freenames = map (#1 o dest_Free) (term_frees Bi)
  1242       val newBi = Logic.list_rename_params (newnames, Bi)
  1243   in
  1244   case findrep cs of
  1245      c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
  1246 	      state)
  1247    | [] => (case cs inter_string freenames of
  1248        a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
  1249 		state)
  1250      | [] => fix_shyps [state] []
  1251                 (Thm{sign_ref = sign_ref,
  1252                      der = infer_derivs (Rename_params_rule(cs,i), [der]),
  1253                      maxidx = maxidx,
  1254                      shyps = [],
  1255                      hyps = hyps,
  1256                      prop = Logic.rule_of(tpairs, Bs@[newBi], C)}))
  1257   end;
  1258 
  1259 (*** Preservation of bound variable names ***)
  1260 
  1261 (*Scan a pair of terms; while they are similar,
  1262   accumulate corresponding bound vars in "al"*)
  1263 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
  1264       match_bvs(s, t, if x="" orelse y="" then al
  1265                                           else (x,y)::al)
  1266   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
  1267   | match_bvs(_,_,al) = al;
  1268 
  1269 (* strip abstractions created by parameters *)
  1270 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
  1271 
  1272 
  1273 (* strip_apply f A(,B) strips off all assumptions/parameters from A
  1274    introduced by lifting over B, and applies f to remaining part of A*)
  1275 fun strip_apply f =
  1276   let fun strip(Const("==>",_)$ A1 $ B1,
  1277                 Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
  1278         | strip((c as Const("all",_)) $ Abs(a,T,t1),
  1279                       Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
  1280         | strip(A,_) = f A
  1281   in strip end;
  1282 
  1283 (*Use the alist to rename all bound variables and some unknowns in a term
  1284   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
  1285   Preserves unknowns in tpairs and on lhs of dpairs. *)
  1286 fun rename_bvs([],_,_,_) = I
  1287   | rename_bvs(al,dpairs,tpairs,B) =
  1288     let val vars = foldr add_term_vars
  1289                         (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
  1290         (*unknowns appearing elsewhere be preserved!*)
  1291         val vids = map (#1 o #1 o dest_Var) vars;
  1292         fun rename(t as Var((x,i),T)) =
  1293                 (case assoc(al,x) of
  1294                    Some(y) => if x mem_string vids orelse y mem_string vids then t
  1295                               else Var((y,i),T)
  1296                  | None=> t)
  1297           | rename(Abs(x,T,t)) =
  1298               Abs(case assoc_string(al,x) of Some(y) => y | None => x,
  1299                   T, rename t)
  1300           | rename(f$t) = rename f $ rename t
  1301           | rename(t) = t;
  1302         fun strip_ren Ai = strip_apply rename (Ai,B)
  1303     in strip_ren end;
  1304 
  1305 (*Function to rename bounds/unknowns in the argument, lifted over B*)
  1306 fun rename_bvars(dpairs, tpairs, B) =
  1307         rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
  1308 
  1309 
  1310 (*** RESOLUTION ***)
  1311 
  1312 (** Lifting optimizations **)
  1313 
  1314 (*strip off pairs of assumptions/parameters in parallel -- they are
  1315   identical because of lifting*)
  1316 fun strip_assums2 (Const("==>", _) $ _ $ B1,
  1317                    Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
  1318   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
  1319                    Const("all",_)$Abs(_,_,t2)) =
  1320       let val (B1,B2) = strip_assums2 (t1,t2)
  1321       in  (Abs(a,T,B1), Abs(a,T,B2))  end
  1322   | strip_assums2 BB = BB;
  1323 
  1324 
  1325 (*Faster normalization: skip assumptions that were lifted over*)
  1326 fun norm_term_skip env 0 t = Envir.norm_term env t
  1327   | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
  1328         let val Envir.Envir{iTs, ...} = env
  1329             val T' = typ_subst_TVars iTs T
  1330             (*Must instantiate types of parameters because they are flattened;
  1331               this could be a NEW parameter*)
  1332         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
  1333   | norm_term_skip env n (Const("==>", _) $ A $ B) =
  1334         implies $ A $ norm_term_skip env (n-1) B
  1335   | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
  1336 
  1337 
  1338 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
  1339   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
  1340   If match then forbid instantiations in proof state
  1341   If lifted then shorten the dpair using strip_assums2.
  1342   If eres_flg then simultaneously proves A1 by assumption.
  1343   nsubgoal is the number of new subgoals (written m above).
  1344   Curried so that resolution calls dest_state only once.
  1345 *)
  1346 local exception COMPOSE
  1347 in
  1348 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
  1349                         (eres_flg, orule, nsubgoal) =
  1350  let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
  1351      and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
  1352              prop=rprop,...} = orule
  1353          (*How many hyps to skip over during normalization*)
  1354      and nlift = Logic.count_prems(strip_all_body Bi,
  1355                                    if eres_flg then ~1 else 0)
  1356      val sign_ref = merge_thm_sgs(state,orule);
  1357      val sign = Sign.deref sign_ref;
  1358      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  1359      fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
  1360        let val normt = Envir.norm_term env;
  1361            (*perform minimal copying here by examining env*)
  1362            val normp =
  1363              if Envir.is_empty env then (tpairs, Bs @ As, C)
  1364              else
  1365              let val ntps = map (pairself normt) tpairs
  1366              in if Envir.above (smax, env) then
  1367                   (*no assignments in state; normalize the rule only*)
  1368                   if lifted
  1369                   then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
  1370                   else (ntps, Bs @ map normt As, C)
  1371                 else if match then raise COMPOSE
  1372                 else (*normalize the new rule fully*)
  1373                   (ntps, map normt (Bs @ As), normt C)
  1374              end
  1375            val th = (*tuned fix_shyps*)
  1376              Thm{sign_ref = sign_ref,
  1377                  der = infer_derivs (Bicompose(match, eres_flg,
  1378                                                1 + length Bs, nsubgoal, env),
  1379                                      [rder,sder]),
  1380                  maxidx = maxidx,
  1381                  shyps = add_env_sorts (env, union_sort(rshyps,sshyps)),
  1382                  hyps = union_term(rhyps,shyps),
  1383                  prop = Logic.rule_of normp}
  1384         in  Seq.cons(th, thq)  end  handle COMPOSE => thq
  1385      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
  1386      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
  1387        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
  1388      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
  1389      fun newAs(As0, n, dpairs, tpairs) =
  1390        let val As1 = if !Logic.auto_rename orelse not lifted then As0
  1391                      else map (rename_bvars(dpairs,tpairs,B)) As0
  1392        in (map (Logic.flatten_params n) As1)
  1393           handle TERM _ =>
  1394           raise THM("bicompose: 1st premise", 0, [orule])
  1395        end;
  1396      val env = Envir.empty(Int.max(rmax,smax));
  1397      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
  1398      val dpairs = BBi :: (rtpairs@stpairs);
  1399      (*elim-resolution: try each assumption in turn.  Initially n=1*)
  1400      fun tryasms (_, _, []) = Seq.empty
  1401        | tryasms (As, n, (t,u)::apairs) =
  1402           (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
  1403                None                   => tryasms (As, n+1, apairs)
  1404              | cell as Some((_,tpairs),_) =>
  1405                    Seq.it_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
  1406                        (Seq.make (fn()=> cell),
  1407                         Seq.make (fn()=> Seq.pull (tryasms (As, n+1, apairs)))));
  1408      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
  1409        | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
  1410      (*ordinary resolution*)
  1411      fun res(None) = Seq.empty
  1412        | res(cell as Some((_,tpairs),_)) =
  1413              Seq.it_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  1414                        (Seq.make (fn()=> cell), Seq.empty)
  1415  in  if eres_flg then eres(rev rAs)
  1416      else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  1417  end;
  1418 end;  (*open Sequence*)
  1419 
  1420 
  1421 fun bicompose match arg i state =
  1422     bicompose_aux match (state, dest_state(state,i), false) arg;
  1423 
  1424 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1425   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1426 fun could_bires (Hs, B, eres_flg, rule) =
  1427     let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
  1428           | could_reshyp [] = false;  (*no premise -- illegal*)
  1429     in  could_unify(concl_of rule, B) andalso
  1430         (not eres_flg  orelse  could_reshyp (prems_of rule))
  1431     end;
  1432 
  1433 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  1434   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  1435 fun biresolution match brules i state =
  1436     let val lift = lift_rule(state, i);
  1437         val (stpairs, Bs, Bi, C) = dest_state(state,i)
  1438         val B = Logic.strip_assums_concl Bi;
  1439         val Hs = Logic.strip_assums_hyp Bi;
  1440         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
  1441         fun res [] = Seq.empty
  1442           | res ((eres_flg, rule)::brules) =
  1443               if could_bires (Hs, B, eres_flg, rule)
  1444               then Seq.make (*delay processing remainder till needed*)
  1445                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
  1446                                res brules))
  1447               else res brules
  1448     in  Seq.flat (res brules)  end;
  1449 
  1450 
  1451 
  1452 (*** Meta Simplification ***)
  1453 
  1454 (** diagnostics **)
  1455 
  1456 exception SIMPLIFIER of string * thm;
  1457 
  1458 fun prnt warn a = if warn then warning a else writeln a;
  1459 
  1460 fun prtm warn a sign t =
  1461   (prnt warn a; prnt warn (Sign.string_of_term sign t));
  1462 
  1463 fun prthm warn a (thm as Thm{sign_ref, prop, ...}) =
  1464   (prtm warn a (Sign.deref sign_ref) prop);
  1465 
  1466 val trace_simp = ref false;
  1467 
  1468 fun trace warn a = if !trace_simp then prnt warn a else ();
  1469 
  1470 fun trace_term warn a sign t =
  1471   if !trace_simp then prtm warn a sign t else ();
  1472 
  1473 fun trace_thm warn a (thm as Thm{sign_ref, prop, ...}) =
  1474   (trace_term warn a (Sign.deref sign_ref) prop);
  1475 
  1476 
  1477 
  1478 (** meta simp sets **)
  1479 
  1480 (* basic components *)
  1481 
  1482 type rrule = {thm: thm, lhs: term, perm: bool};
  1483 type cong = {thm: thm, lhs: term};
  1484 type simproc =
  1485  {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
  1486 
  1487 fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
  1488   {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
  1489 
  1490 fun eq_cong ({thm = Thm {prop = p1, ...}, ...}: cong,
  1491   {thm = Thm {prop = p2, ...}, ...}: cong) = p1 aconv p2;
  1492 
  1493 fun eq_prem (Thm {prop = p1, ...}, Thm {prop = p2, ...}) = p1 aconv p2;
  1494 
  1495 fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
  1496 
  1497 fun mk_simproc (name, proc, lhs, id) =
  1498   {name = name, proc = proc, lhs = lhs, id = id};
  1499 
  1500 
  1501 (* datatype mss *)
  1502 
  1503 (*
  1504   A "mss" contains data needed during conversion:
  1505     rules: discrimination net of rewrite rules;
  1506     congs: association list of congruence rules;
  1507     procs: discrimination net of simplification procedures
  1508       (functions that prove rewrite rules on the fly);
  1509     bounds: names of bound variables already used
  1510       (for generating new names when rewriting under lambda abstractions);
  1511     prems: current premises;
  1512     mk_rews: mk: turns simplification thms into rewrite rules;
  1513              mk_sym: turns == around; (needs Drule!)
  1514              mk_eq_True: turns P into P == True - logic specific;
  1515     termless: relation for ordered rewriting;
  1516 *)
  1517 
  1518 datatype meta_simpset =
  1519   Mss of {
  1520     rules: rrule Net.net,
  1521     congs: (string * cong) list,
  1522     procs: simproc Net.net,
  1523     bounds: string list,
  1524     prems: thm list,
  1525     mk_rews: {mk: thm -> thm list,
  1526               mk_sym: thm -> thm option,
  1527               mk_eq_True: thm -> thm option},
  1528     termless: term * term -> bool};
  1529 
  1530 fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) =
  1531   Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
  1532        prems=prems, mk_rews=mk_rews, termless=termless};
  1533 
  1534 fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless}, rules') =
  1535   mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless);
  1536 
  1537 val empty_mss =
  1538   let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
  1539   in mk_mss (Net.empty, [], Net.empty, [], [], mk_rews, Term.termless) end;
  1540 
  1541 
  1542 
  1543 (** simpset operations **)
  1544 
  1545 (* dest_mss *)
  1546 
  1547 fun dest_mss (Mss {rules, congs, procs, ...}) =
  1548   {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
  1549    congs = map (fn (_, {thm, ...}) => thm) congs,
  1550    procs =
  1551      map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
  1552      |> partition_eq eq_snd
  1553      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))};
  1554 
  1555 
  1556 (* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)
  1557 
  1558 fun merge_mss
  1559  (Mss {rules = rules1, congs = congs1, procs = procs1, bounds = bounds1,
  1560     prems = prems1, mk_rews, termless},
  1561   Mss {rules = rules2, congs = congs2, procs = procs2, bounds = bounds2,
  1562     prems = prems2, ...}) =
  1563       mk_mss
  1564        (Net.merge (rules1, rules2, eq_rrule),
  1565         generic_merge (eq_cong o pairself snd) I I congs1 congs2,
  1566         Net.merge (procs1, procs2, eq_simproc),
  1567         merge_lists bounds1 bounds2,
  1568         generic_merge eq_prem I I prems1 prems2,
  1569         mk_rews, termless);
  1570 
  1571 (* add_simps *)
  1572 
  1573 fun insert_rrule(mss as Mss {rules,...},
  1574                  rrule as {thm = thm, lhs = lhs, perm = perm}) =
  1575   (trace_thm false "Adding rewrite rule:" thm;
  1576    let val rules' = Net.insert_term ((lhs, rrule), rules, eq_rrule)
  1577    in upd_rules(mss,rules') end
  1578    handle Net.INSERT =>
  1579      (prthm true "Ignoring duplicate rewrite rule" thm; mss));
  1580 
  1581 fun vperm (Var _, Var _) = true
  1582   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
  1583   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
  1584   | vperm (t, u) = (t = u);
  1585 
  1586 fun var_perm (t, u) =
  1587   vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
  1588 
  1589 (* FIXME: it seems that the conditions on extra variables are too liberal if
  1590 prems are nonempty: does solving the prems really guarantee instantiation of
  1591 all its Vars? Better: a dynamic check each time a rule is applied.
  1592 *)
  1593 fun rewrite_rule_extra_vars prems elhs erhs =
  1594   not ((term_vars erhs) subset
  1595        (union_term (term_vars elhs, List.concat(map term_vars prems))))
  1596   orelse
  1597   not ((term_tvars erhs) subset
  1598        (term_tvars elhs  union  List.concat(map term_tvars prems)));
  1599 
  1600 (*simple test for looping rewrite*)
  1601 fun looptest sign prems lhs rhs =
  1602    rewrite_rule_extra_vars prems lhs rhs
  1603   orelse
  1604    is_Var (head_of lhs)
  1605   orelse
  1606    (exists (apl (lhs, Logic.occs)) (rhs :: prems))
  1607   orelse
  1608    (null prems andalso
  1609     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
  1610 (*the condition "null prems" in the last cases is necessary because
  1611   conditional rewrites with extra variables in the conditions may terminate
  1612   although the rhs is an instance of the lhs. Example:
  1613   ?m < ?n ==> f(?n) == f(?m)*)
  1614 
  1615 fun decomp_simp(thm as Thm {sign_ref, prop, ...}) =
  1616   let val sign = Sign.deref sign_ref;
  1617       val prems = Logic.strip_imp_prems prop;
  1618       val concl = Logic.strip_imp_concl prop;
  1619       val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
  1620         raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
  1621       val elhs = Pattern.eta_contract lhs;
  1622       val erhs = Pattern.eta_contract rhs;
  1623       val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
  1624                  andalso not (is_Var elhs)
  1625   in (sign,prems,lhs,rhs,perm) end;
  1626 
  1627 fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) thm =
  1628   case mk_eq_True thm of
  1629     None => []
  1630   | Some eq_True => let val (_,_,lhs,_,_) = decomp_simp eq_True
  1631                     in [{thm=eq_True, lhs=lhs, perm=false}] end;
  1632 
  1633 (* create the rewrite rule and possibly also the ==True variant,
  1634    in case there are extra vars on the rhs *)
  1635 fun rrule_eq_True(thm,lhs,rhs,mss,thm2) =
  1636   let val rrule = {thm=thm, lhs=lhs, perm=false}
  1637   in if (term_vars rhs)  subset (term_vars lhs) andalso
  1638         (term_tvars rhs) subset (term_tvars lhs)
  1639      then [rrule]
  1640      else mk_eq_True mss thm2 @ [rrule]
  1641   end;
  1642 
  1643 fun mk_rrule mss thm =
  1644   let val (_,prems,lhs,rhs,perm) = decomp_simp thm
  1645   in if perm then [{thm=thm, lhs=lhs, perm=true}] else
  1646      (* weak test for loops: *)
  1647      if rewrite_rule_extra_vars prems lhs rhs orelse
  1648         is_Var (head_of lhs) (* mk_cases may do this! *)
  1649      then mk_eq_True mss thm
  1650      else rrule_eq_True(thm,lhs,rhs,mss,thm)
  1651   end;
  1652 
  1653 fun orient_rrule mss thm =
  1654   let val (sign,prems,lhs,rhs,perm) = decomp_simp thm
  1655   in if perm then [{thm=thm,lhs=lhs,perm=true}]
  1656      else if looptest sign prems lhs rhs
  1657           then if looptest sign prems rhs lhs
  1658                then mk_eq_True mss thm
  1659                else let val Mss{mk_rews={mk_sym,...},...} = mss
  1660                     in case mk_sym thm of
  1661                          None => []
  1662                        | Some thm' => rrule_eq_True(thm',rhs,lhs,mss,thm)
  1663                     end
  1664           else rrule_eq_True(thm,lhs,rhs,mss,thm)
  1665   end;
  1666 
  1667 fun extract_rews(Mss{mk_rews = {mk,...},...},thms) = flat(map mk thms);
  1668 
  1669 fun orient_comb_simps comb mk_rrule (mss,thms) =
  1670   let val rews = extract_rews(mss,thms)
  1671       val rrules = flat (map mk_rrule rews)
  1672   in foldl comb (mss,rrules) end
  1673 
  1674 (* Add rewrite rules explicitly; do not reorient! *)
  1675 fun add_simps(mss,thms) =
  1676   orient_comb_simps insert_rrule (mk_rrule mss) (mss,thms);
  1677 
  1678 fun mss_of thms =
  1679   foldl insert_rrule (empty_mss, flat(map (mk_rrule empty_mss) thms));
  1680 
  1681 fun extract_safe_rrules(mss,thm) =
  1682   flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
  1683 
  1684 (* del_simps *)
  1685 
  1686 fun del_rrule(mss as Mss {rules,...},
  1687               rrule as {thm = thm, lhs = lhs, perm = perm}) =
  1688   (upd_rules(mss, Net.delete_term ((lhs, rrule), rules, eq_rrule))
  1689    handle Net.DELETE =>
  1690      (prthm true "rewrite rule not in simpset" thm; mss));
  1691 
  1692 fun del_simps(mss,thms) =
  1693   orient_comb_simps del_rrule (mk_rrule mss) (mss,thms);
  1694 
  1695 
  1696 (* add_congs *)
  1697 
  1698 fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
  1699   let
  1700     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
  1701       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  1702 (*   val lhs = Pattern.eta_contract lhs; *)
  1703     val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
  1704       raise SIMPLIFIER ("Congruence must start with a constant", thm);
  1705   in
  1706     mk_mss (rules, (a, {lhs = lhs, thm = thm}) :: congs, procs, bounds,
  1707       prems, mk_rews, termless)
  1708   end;
  1709 
  1710 val (op add_congs) = foldl add_cong;
  1711 
  1712 
  1713 (* del_congs *)
  1714 
  1715 fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thm) =
  1716   let
  1717     val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
  1718       raise SIMPLIFIER ("Congruence not a meta-equality", thm);
  1719 (*   val lhs = Pattern.eta_contract lhs; *)
  1720     val (a, _) = dest_Const (head_of lhs) handle TERM _ =>
  1721       raise SIMPLIFIER ("Congruence must start with a constant", thm);
  1722   in
  1723     mk_mss (rules, filter (fn (x,_)=> x<>a) congs, procs, bounds,
  1724       prems, mk_rews, termless)
  1725   end;
  1726 
  1727 val (op del_congs) = foldl del_cong;
  1728 
  1729 
  1730 (* add_simprocs *)
  1731 
  1732 fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
  1733     (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
  1734   (trace_term false ("Adding simplification procedure " ^ quote name ^ " for:")
  1735       (Sign.deref sign_ref) t;
  1736     mk_mss (rules, congs,
  1737       Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
  1738         handle Net.INSERT => (trace true "ignored duplicate"; procs),
  1739         bounds, prems, mk_rews, termless));
  1740 
  1741 fun add_simproc (mss, (name, lhss, proc, id)) =
  1742   foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
  1743 
  1744 val add_simprocs = foldl add_simproc;
  1745 
  1746 
  1747 (* del_simprocs *)
  1748 
  1749 fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless},
  1750     (name, lhs as Cterm {t, ...}, proc, id)) =
  1751   mk_mss (rules, congs,
  1752     Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
  1753       handle Net.DELETE => (trace true "simplification procedure not in simpset"; procs),
  1754       bounds, prems, mk_rews, termless);
  1755 
  1756 fun del_simproc (mss, (name, lhss, proc, id)) =
  1757   foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
  1758 
  1759 val del_simprocs = foldl del_simproc;
  1760 
  1761 
  1762 (* prems *)
  1763 
  1764 fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless}, thms) =
  1765   mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless);
  1766 
  1767 fun prems_of_mss (Mss {prems, ...}) = prems;
  1768 
  1769 
  1770 (* mk_rews *)
  1771 
  1772 fun set_mk_rews
  1773   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk) =
  1774     mk_mss (rules, congs, procs, bounds, prems,
  1775             {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
  1776             termless);
  1777 
  1778 fun set_mk_sym
  1779   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_sym) =
  1780     mk_mss (rules, congs, procs, bounds, prems,
  1781             {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
  1782             termless);
  1783 
  1784 fun set_mk_eq_True
  1785   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, mk_eq_True) =
  1786     mk_mss (rules, congs, procs, bounds, prems,
  1787             {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
  1788             termless);
  1789 
  1790 (* termless *)
  1791 
  1792 fun set_termless
  1793   (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) =
  1794     mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless);
  1795 
  1796 
  1797 
  1798 (** rewriting **)
  1799 
  1800 (*
  1801   Uses conversions, omitting proofs for efficiency.  See:
  1802     L C Paulson, A higher-order implementation of rewriting,
  1803     Science of Computer Programming 3 (1983), pages 119-149.
  1804 *)
  1805 
  1806 type prover = meta_simpset -> thm -> thm option;
  1807 type termrec = (Sign.sg_ref * term list) * term;
  1808 type conv = meta_simpset -> termrec -> termrec;
  1809 
  1810 fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,...}, prop0, ders) =
  1811   let fun err() = (trace_thm false "Proved wrong thm (Check subgoaler?)" thm;
  1812                    trace_term false "Should have proved" (Sign.deref sign_ref) prop0;
  1813                    None)
  1814       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
  1815   in case prop of
  1816        Const("==",_) $ lhs $ rhs =>
  1817          if (lhs = lhs0) orelse
  1818             (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
  1819          then (trace_thm false "SUCCEEDED" thm; 
  1820                Some(rhs, (shyps, hyps, der::ders)))
  1821          else err()
  1822      | _ => err()
  1823   end;
  1824 
  1825 fun ren_inst(insts,prop,pat,obj) =
  1826   let val ren = match_bvs(pat,obj,[])
  1827       fun renAbs(Abs(x,T,b)) =
  1828             Abs(case assoc_string(ren,x) of None => x | Some(y) => y, T, renAbs(b))
  1829         | renAbs(f$t) = renAbs(f) $ renAbs(t)
  1830         | renAbs(t) = t
  1831   in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
  1832 
  1833 fun add_insts_sorts ((iTs, is), Ss) =
  1834   add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss));
  1835 
  1836 
  1837 (* mk_procrule *)
  1838 
  1839 fun mk_procrule thm =
  1840   let val (_,prems,lhs,rhs,_) = decomp_simp thm
  1841   in if rewrite_rule_extra_vars prems lhs rhs
  1842      then (prthm true "Extra vars on rhs" thm; [])
  1843      else [{thm = thm, lhs = lhs, perm = false}]
  1844   end;
  1845 
  1846 
  1847 (* conversion to apply the meta simpset to a term *)
  1848 
  1849 (*
  1850   we try in order:
  1851     (1) beta reduction
  1852     (2) unconditional rewrite rules
  1853     (3) conditional rewrite rules
  1854     (4) simplification procedures
  1855 
  1856   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  1857 
  1858 *)
  1859 
  1860 fun rewritec (prover,sign_reft,maxt)
  1861              (mss as Mss{rules, procs, termless, prems, ...}) 
  1862              (t:term,etc as (shypst,hypst,ders)) =
  1863   let
  1864     val signt = Sign.deref sign_reft;
  1865     val tsigt = Sign.tsig_of signt;
  1866     fun rew{thm as Thm{sign_ref,der,shyps,hyps,prop,maxidx,...}, lhs, perm} =
  1867       let
  1868         val _ = if Sign.subsig (Sign.deref sign_ref, signt) then ()
  1869                 else (trace_thm true "rewrite rule from different theory" thm;
  1870                       raise Pattern.MATCH);
  1871         val rprop = if maxt = ~1 then prop
  1872                     else Logic.incr_indexes([],maxt+1) prop;
  1873         val rlhs = if maxt = ~1 then lhs
  1874                    else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
  1875         val insts = Pattern.match tsigt (rlhs,t);
  1876         val prop' = ren_inst(insts,rprop,rlhs,t);
  1877         val hyps' = union_term(hyps,hypst);
  1878         val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
  1879         val unconditional = (Logic.count_prems(prop',0) = 0);
  1880         val maxidx' = if unconditional then maxt else maxidx+maxt+1
  1881         val ct' = Cterm{sign_ref = sign_reft,       (*used for deriv only*)
  1882                         t = prop', T = propT, maxidx = maxidx'}
  1883         val der' = infer_derivs (RewriteC ct', [der]);
  1884         val thm' = Thm{sign_ref = sign_reft, der = der', shyps = shyps',
  1885                        hyps = hyps', prop = prop', maxidx = maxidx'}
  1886         val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
  1887       in
  1888         if perm andalso not(termless(rhs',lhs')) then None
  1889         else (trace_thm false "Applying instance of rewrite rule:" thm;
  1890               if unconditional
  1891               then (trace_thm false "Rewriting:" thm'; 
  1892                     Some(rhs', (shyps', hyps', der'::ders)))
  1893               else (trace_thm false "Trying to rewrite:" thm';
  1894                     case prover mss thm' of
  1895                       None       => (trace_thm false "FAILED" thm'; None)
  1896                     | Some(thm2) => check_conv(thm2,prop',ders)))
  1897       end
  1898 
  1899     fun rews [] = None
  1900       | rews (rrule :: rrules) =
  1901           let val opt = rew rrule handle Pattern.MATCH => None
  1902           in case opt of None => rews rrules | some => some end;
  1903 
  1904     fun sort_rrules rrs = let
  1905       fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
  1906                                       Const("==",_) $ _ $ _ => true
  1907                                       | _                   => false 
  1908       fun sort []        (re1,re2) = re1 @ re2
  1909         | sort (rr::rrs) (re1,re2) = if is_simple rr 
  1910                                      then sort rrs (rr::re1,re2)
  1911                                      else sort rrs (re1,rr::re2)
  1912     in sort rrs ([],[]) end
  1913 
  1914     fun proc_rews _ ([]:simproc list) = None
  1915       | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
  1916           if Pattern.matches tsigt (plhs, t) then
  1917             (trace_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
  1918              case proc signt prems eta_t of
  1919                None => (trace false "FAILED"; proc_rews eta_t ps)
  1920              | Some raw_thm =>
  1921                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
  1922                   (case rews (mk_procrule raw_thm) of
  1923                     None => (trace false "IGNORED"; proc_rews eta_t ps)
  1924                   | some => some)))
  1925           else proc_rews eta_t ps;
  1926   in case t of
  1927        Abs (_, _, body) $ u =>
  1928          Some (subst_bound (u, body), etc)
  1929      | _ => (case rews (sort_rrules (Net.match_term rules t)) of
  1930                None => proc_rews (Pattern.eta_contract t)
  1931                                  (Net.match_term procs t)
  1932              | some => some)
  1933   end;
  1934 
  1935 
  1936 (* conversion to apply a congruence rule to a term *)
  1937 
  1938 fun congc (prover,sign_reft,maxt) {thm=cong,lhs=lhs} (t,(shypst,hypst,ders)) =
  1939   let val signt = Sign.deref sign_reft;
  1940       val tsig = Sign.tsig_of signt;
  1941       val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
  1942       val _ = if Sign.subsig(Sign.deref sign_ref,signt) then ()
  1943                  else error("Congruence rule from different theory")
  1944       val rprop = if maxt = ~1 then prop
  1945                   else Logic.incr_indexes([],maxt+1) prop;
  1946       val rlhs = if maxt = ~1 then lhs
  1947                  else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
  1948       val insts = Pattern.match tsig (rlhs,t)
  1949       (* Pattern.match can raise Pattern.MATCH;
  1950          is handled when congc is called *)
  1951       val prop' = ren_inst(insts,rprop,rlhs,t);
  1952       val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
  1953       val maxidx' = maxidx_of_term prop'
  1954       val ct' = Cterm{sign_ref = sign_reft,     (*used for deriv only*)
  1955                       t = prop',
  1956                       T = propT,
  1957                       maxidx = maxidx'}
  1958       val thm' = Thm{sign_ref = sign_reft, 
  1959                      der = infer_derivs (CongC ct', [der]),
  1960                      shyps = shyps',
  1961                      hyps = union_term(hyps,hypst),
  1962                      prop = prop',
  1963                      maxidx = maxidx'};
  1964       val unit = trace_thm false "Applying congruence rule" thm';
  1965       fun err() = error("Failed congruence proof!")
  1966 
  1967   in case prover thm' of
  1968        None => err()
  1969      | Some(thm2) => (case check_conv(thm2,prop',ders) of
  1970                         None => err() | some => some)
  1971   end;
  1972 
  1973 fun bottomc ((simprem,useprem,mutsimp),prover,sign_ref,maxidx) =
  1974   let
  1975     fun botc fail mss trec =
  1976           (case subc mss trec of
  1977              some as Some(trec1) =>
  1978                (case rewritec (prover,sign_ref,maxidx) mss trec1 of
  1979                   Some(trec2) => botc false mss trec2
  1980                 | None => some)
  1981            | None =>
  1982                (case rewritec (prover,sign_ref,maxidx) mss trec of
  1983                   Some(trec2) => botc false mss trec2
  1984                 | None => if fail then None else Some(trec)))
  1985 
  1986     and try_botc mss trec = (case botc true mss trec of
  1987                                 Some(trec1) => trec1
  1988                               | None => trec)
  1989 
  1990     and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless})
  1991              (trec as (t0:term,etc:sort list*term list * rule mtree list)) =
  1992        (case t0 of
  1993            Abs(a,T,t) =>
  1994              let val b = variant bounds a
  1995                  val v = Free("." ^ b,T)
  1996                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)
  1997              in case botc true mss' (subst_bound(v,t),etc) of
  1998                   Some(t',etc') => Some(Abs(a, T, abstract_over(v,t')), etc')
  1999                 | None => None
  2000              end
  2001          | t$u => (case t of
  2002              Const("==>",_)$s  => Some(snd(impc([],s,u,mss,etc)))
  2003            | Abs(_,_,body) =>
  2004                let val trec = (subst_bound(u,body), etc)
  2005                in case subc mss trec of
  2006                     None => Some(trec)
  2007                   | trec => trec
  2008                end
  2009            | _  =>
  2010                let fun appc() =
  2011                      (case botc true mss (t,etc) of
  2012                         Some(t1,etc1) =>
  2013                           (case botc true mss (u,etc1) of
  2014                              Some(u1,etc2) => Some(t1$u1, etc2)
  2015                            | None => Some(t1$u, etc1))
  2016                       | None =>
  2017                           (case botc true mss (u,etc) of
  2018                              Some(u1,etc1) => Some(t$u1, etc1)
  2019                            | None => None))
  2020                    val (h,ts) = strip_comb t
  2021                in case h of
  2022                     Const(a,_) =>
  2023                       (case assoc_string(congs,a) of
  2024                          None => appc()
  2025                        | Some(cong) =>
  2026                            (congc (prover mss,sign_ref,maxidx) cong trec
  2027                             handle Pattern.MATCH => appc() ) )
  2028                   | _ => appc()
  2029                end)
  2030          | _ => None)
  2031 
  2032     and impc(prems, prem, conc, mss, etc) =
  2033       let val (prem1,etc1) = if simprem then try_botc mss (prem,etc)
  2034                              else (prem,etc)
  2035       in impc1(prems, prem1, conc, mss, etc1) end
  2036 
  2037     and impc1(prems, prem1, conc, mss, etc1 as (_,hyps1,_)) =
  2038       let
  2039         fun uncond({thm,lhs,...}:rrule) =
  2040           if nprems_of thm = 0 then Some lhs else None
  2041 
  2042         val (rrules1,lhss1,mss1) =
  2043           if not useprem then ([],[],mss) else
  2044           if maxidx_of_term prem1 <> ~1
  2045           then (trace_term true "Cannot add premise as rewrite rule because it contains (type) unknowns:"
  2046                            (Sign.deref sign_ref) prem1;
  2047                 ([],[],mss))
  2048           else let val thm = assume (Cterm{sign_ref=sign_ref, t=prem1, 
  2049                                            T=propT, maxidx= ~1})
  2050                    val rrules1 = extract_safe_rrules(mss,thm)
  2051                    val lhss1 = if mutsimp then mapfilter uncond rrules1 else []
  2052                    val mss1 = foldl insert_rrule (add_prems(mss,[thm]),rrules1)
  2053                in (rrules1, lhss1, mss1) end
  2054 
  2055         fun rebuild(conc2,(shyps2,hyps2,ders2)) =
  2056           let val hyps2' = if gen_mem (op aconv) (prem1, hyps1)
  2057                            then hyps2 else hyps2\prem1
  2058               val trec = (Logic.mk_implies(prem1,conc2),
  2059                           (shyps2,hyps2',ders2))
  2060           in case rewritec (prover,sign_ref,maxidx) mss trec of
  2061                None => (None,trec)
  2062              | Some(Const("==>",_)$prem$conc,etc) =>
  2063                  impc(prems,prem,conc,mss,etc)
  2064              | Some(trec') => (None,trec')
  2065           end
  2066 
  2067         fun simpconc() =
  2068           case conc of
  2069             Const("==>",_)$s$t =>
  2070               (case impc(prems@[prem1],s,t,mss1,etc1) of
  2071                  (Some(i,prem),(conc2,etc2)) =>
  2072                     let val impl = Logic.mk_implies(prem1,conc2)
  2073                     in if i=0 then impc1(prems,prem,impl,mss,etc2)
  2074                        else (Some(i-1,prem),(impl,etc2))
  2075                     end
  2076                | (None,trec) => rebuild(trec))
  2077           | _ => rebuild(try_botc mss1 (conc,etc1))
  2078 
  2079       in if mutsimp
  2080          then let val sg = Sign.deref sign_ref
  2081                   val tsig = #tsig(Sign.rep_sg sg)
  2082                   fun reducible t =
  2083                     exists (fn lhs => Pattern.matches_subterm tsig (lhs,t))
  2084                            lhss1;
  2085               in case dropwhile (not o reducible) prems of
  2086                    [] => simpconc()
  2087                  | red::rest => (trace_term false "Can now reduce premise" sg
  2088                                             red;
  2089                                  (Some(length rest,prem1),(conc,etc1)))
  2090               end
  2091          else simpconc()
  2092       end
  2093 
  2094  in try_botc end;
  2095 
  2096 
  2097 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
  2098 
  2099 (*
  2100   Parameters:
  2101     mode = (simplify A,
  2102             use A in simplifying B,
  2103             use prems of B (if B is again a meta-impl.) to simplify A)
  2104            when simplifying A ==> B
  2105     mss: contains equality theorems of the form [|p1,...|] ==> t==u
  2106     prover: how to solve premises in conditional rewrites and congruences
  2107 *)
  2108 
  2109 (* FIXME: check that #bounds(mss) does not "occur" in ct alread *)
  2110 
  2111 fun rewrite_cterm mode mss prover ct =
  2112   let val Cterm {sign_ref, t, T, maxidx} = ct;
  2113       val (u,(shyps,hyps,ders)) = bottomc (mode,prover, sign_ref, maxidx) mss 
  2114                                           (t, (add_term_sorts(t,[]), [], []));
  2115       val prop = Logic.mk_equals(t,u)
  2116   in
  2117       Thm{sign_ref = sign_ref, 
  2118           der = infer_derivs (Rewrite_cterm ct, ders),
  2119           maxidx = maxidx,
  2120           shyps = shyps, 
  2121           hyps = hyps, 
  2122           prop = prop}
  2123   end;
  2124 
  2125 
  2126 
  2127 (*** Oracles ***)
  2128 
  2129 fun invoke_oracle thy raw_name =
  2130   let
  2131     val {sign = sg, oracles, ...} = rep_theory thy;
  2132     val name = Sign.intern sg Theory.oracleK raw_name;
  2133     val oracle =
  2134       (case Symtab.lookup (oracles, name) of
  2135         None => raise THM ("Unknown oracle: " ^ name, 0, [])
  2136       | Some (f, _) => f);
  2137   in
  2138     fn (sign, exn) =>
  2139       let
  2140         val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
  2141         val sign' = Sign.deref sign_ref';
  2142         val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
  2143       in
  2144         if T <> propT then
  2145           raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  2146         else fix_shyps [] []
  2147           (Thm {sign_ref = sign_ref', 
  2148             der = Join (Oracle (name, sign, exn), []),
  2149             maxidx = maxidx,
  2150             shyps = [], 
  2151             hyps = [], 
  2152             prop = prop})
  2153       end
  2154   end;
  2155 
  2156 
  2157 end;
  2158 
  2159 open Thm;