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