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