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