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