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