src/Pure/thm.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 1160 8845eb5f0e5e
child 1195 686e3eb613b9
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
     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, theories, meta rules (including resolution and
     8 simplification).
     9 *)
    10 
    11 signature THM =
    12 sig
    13   structure Envir 	: ENVIR
    14   structure Sequence 	: SEQUENCE
    15   structure Sign 	: SIGN
    16 
    17   (*certified types*)
    18   type ctyp
    19   val rep_ctyp		: ctyp -> {sign: Sign.sg, T: typ}
    20   val typ_of		: ctyp -> typ
    21   val ctyp_of		: Sign.sg -> typ -> ctyp
    22   val read_ctyp		: Sign.sg -> string -> ctyp
    23 
    24   (*certified terms*)
    25   type cterm
    26   val rep_cterm		: cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    27   val term_of		: cterm -> term
    28   val cterm_of		: Sign.sg -> term -> cterm
    29   val read_cterm	: Sign.sg -> string * typ -> cterm
    30   val cterm_fun		: (term -> term) -> (cterm -> cterm)
    31   val dest_cimplies	: cterm -> cterm * cterm
    32   val read_def_cterm 	:
    33     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    34     string list -> bool -> string * typ -> cterm * (indexname * typ) list
    35 
    36   (*meta theorems*)
    37   type thm
    38   exception THM of string * int * thm list
    39   val rep_thm		: thm ->
    40     {sign: Sign.sg, maxidx: int, hyps: term list, prop: term};
    41   val stamps_of_thm	: thm -> string ref list
    42   val tpairs_of		: thm -> (term * term) list
    43   val prems_of		: thm -> term list
    44   val nprems_of		: thm -> int
    45   val concl_of		: thm -> term
    46   val cprop_of		: thm -> cterm
    47   val cert_axm		: Sign.sg -> string * term -> string * term
    48   val read_axm		: Sign.sg -> string * string -> string * term
    49   val inferT_axm	: Sign.sg -> string * term -> string * term
    50 
    51   (*theories*)
    52   type theory
    53   exception THEORY of string * theory list
    54   val rep_theory	: theory ->
    55     {sign: Sign.sg, new_axioms: term Sign.Symtab.table, parents: theory list}
    56   val sign_of		: theory -> Sign.sg
    57   val syn_of		: theory -> Sign.Syntax.syntax
    58   val stamps_of_thy	: theory -> string ref list
    59   val parents_of	: theory -> theory list
    60   val subthy		: theory * theory -> bool
    61   val eq_thy		: theory * theory -> bool
    62   val get_axiom		: theory -> string -> thm
    63   val axioms_of		: theory -> (string * thm) list
    64   val proto_pure_thy	: theory
    65   val pure_thy		: theory
    66   val cpure_thy		: theory
    67   local open Sign.Syntax in
    68     val add_classes	: (class * class list) list -> theory -> theory
    69     val add_classrel	: (class * class) list -> theory -> theory
    70     val add_defsort	: sort -> theory -> theory
    71     val add_types	: (string * int * mixfix) list -> theory -> theory
    72     val add_tyabbrs	: (string * string list * string * mixfix) list
    73       -> theory -> theory
    74     val add_tyabbrs_i	: (string * string list * typ * mixfix) list
    75       -> theory -> theory
    76     val add_arities	: (string * sort list * sort) list -> theory -> theory
    77     val add_consts	: (string * string * mixfix) list -> theory -> theory
    78     val add_consts_i	: (string * typ * mixfix) list -> theory -> theory
    79     val add_syntax	: (string * string * mixfix) list -> theory -> theory
    80     val add_syntax_i	: (string * typ * mixfix) list -> theory -> theory
    81     val add_trfuns	:
    82       (string * (ast list -> ast)) list *
    83       (string * (term list -> term)) list *
    84       (string * (term list -> term)) list *
    85       (string * (ast list -> ast)) list -> theory -> theory
    86     val add_trrules	: (string * string) trrule list -> theory -> theory
    87     val add_trrules_i	: ast trrule list -> theory -> theory
    88     val add_axioms	: (string * string) list -> theory -> theory
    89     val add_axioms_i	: (string * term) list -> theory -> theory
    90     val add_thyname	: string -> theory -> theory
    91   end
    92   val merge_theories	: theory * theory -> theory
    93   val merge_thy_list	: bool -> theory list -> theory
    94 
    95   (*meta rules*)
    96   val assume		: cterm -> thm
    97   val implies_intr	: cterm -> thm -> thm
    98   val implies_elim	: thm -> thm -> thm
    99   val forall_intr	: cterm -> thm -> thm
   100   val forall_elim	: cterm -> thm -> thm
   101   val flexpair_def	: thm
   102   val reflexive		: cterm -> thm
   103   val symmetric		: thm -> thm
   104   val transitive	: thm -> thm -> thm
   105   val beta_conversion	: cterm -> thm
   106   val extensional	: thm -> thm
   107   val abstract_rule	: string -> cterm -> thm -> thm
   108   val combination	: thm -> thm -> thm
   109   val equal_intr	: thm -> thm -> thm
   110   val equal_elim	: thm -> thm -> thm
   111   val implies_intr_hyps	: thm -> thm
   112   val flexflex_rule	: thm -> thm Sequence.seq
   113   val instantiate	:
   114     (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
   115   val trivial		: cterm -> thm
   116   val class_triv	: theory -> class -> thm
   117   val varifyT		: thm -> thm
   118   val freezeT		: thm -> thm
   119   val dest_state	: thm * int ->
   120     (term * term) list * term list * term * term
   121   val lift_rule		: (thm * int) -> thm -> thm
   122   val assumption	: int -> thm -> thm Sequence.seq
   123   val eq_assumption	: int -> thm -> thm
   124   val rename_params_rule: string list * int -> thm -> thm
   125   val bicompose		: bool -> bool * thm * int ->
   126     int -> thm -> thm Sequence.seq
   127   val biresolution	: bool -> (bool * thm) list ->
   128     int -> thm -> thm Sequence.seq
   129 
   130   (*meta simplification*)
   131   type meta_simpset
   132   exception SIMPLIFIER of string * thm
   133   val empty_mss		: meta_simpset
   134   val add_simps		: meta_simpset * thm list -> meta_simpset
   135   val del_simps		: meta_simpset * thm list -> meta_simpset
   136   val mss_of		: thm list -> meta_simpset
   137   val add_congs		: meta_simpset * thm list -> meta_simpset
   138   val add_prems		: meta_simpset * thm list -> meta_simpset
   139   val prems_of_mss	: meta_simpset -> thm list
   140   val set_mk_rews	: meta_simpset * (thm -> thm list) -> meta_simpset
   141   val mk_rews_of_mss	: meta_simpset -> thm -> thm list
   142   val trace_simp	: bool ref
   143   val rewrite_cterm	: bool * bool -> meta_simpset ->
   144     (meta_simpset -> thm -> thm option) -> cterm -> thm
   145 end;
   146 
   147 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN
   148   and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM =
   149 struct
   150 
   151 structure Sequence = Unify.Sequence;
   152 structure Envir = Unify.Envir;
   153 structure Sign = Unify.Sign;
   154 structure Type = Sign.Type;
   155 structure Syntax = Sign.Syntax;
   156 structure Symtab = Sign.Symtab;
   157 
   158 
   159 (*** Certified terms and types ***)
   160 
   161 (** certified types **)
   162 
   163 (*certified typs under a signature*)
   164 
   165 datatype ctyp = Ctyp of {sign: Sign.sg, T: typ};
   166 
   167 fun rep_ctyp (Ctyp args) = args;
   168 fun typ_of (Ctyp {T, ...}) = T;
   169 
   170 fun ctyp_of sign T =
   171   Ctyp {sign = sign, T = Sign.certify_typ sign T};
   172 
   173 fun read_ctyp sign s =
   174   Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s};
   175 
   176 
   177 
   178 (** certified terms **)
   179 
   180 (*certified terms under a signature, with checked typ and maxidx of Vars*)
   181 
   182 datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int};
   183 
   184 fun rep_cterm (Cterm args) = args;
   185 fun term_of (Cterm {t, ...}) = t;
   186 
   187 (*create a cterm by checking a "raw" term with respect to a signature*)
   188 fun cterm_of sign tm =
   189   let val (t, T, maxidx) = Sign.certify_term sign tm
   190   in Cterm {sign = sign, t = t, T = T, maxidx = maxidx}
   191   end handle TYPE (msg, _, _)
   192     => raise TERM ("Term not in signature\n" ^ msg, [tm]);
   193 
   194 fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t);
   195 
   196 
   197 (*dest_implies for cterms. Note T=prop below*)
   198 fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) =
   199        (Cterm{sign=sign, T=T, maxidx=maxidx, t=A},
   200         Cterm{sign=sign, T=T, maxidx=maxidx, t=B})
   201   | dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]);
   202 
   203 
   204 
   205 (** read cterms **)   (*exception ERROR*)
   206 
   207 (*read term, infer types, certify term*)
   208 fun read_def_cterm (sign, types, sorts) used freeze (a, T) =
   209   let
   210     val T' = Sign.certify_typ sign T
   211       handle TYPE (msg, _, _) => error msg;
   212     val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
   213     val (_, t', tye) =
   214           Sign.infer_types sign types sorts used freeze (ts, T');
   215     val ct = cterm_of sign t'
   216       handle TERM (msg, _) => error msg;
   217   in (ct, tye) end;
   218 
   219 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
   220 
   221 
   222 
   223 (*** Meta theorems ***)
   224 
   225 datatype thm = Thm of
   226   {sign: Sign.sg, maxidx: int, hyps: term list, prop: term};
   227 
   228 fun rep_thm (Thm args) = args;
   229 
   230 (*errors involving theorems*)
   231 exception THM of string * int * thm list;
   232 
   233 
   234 val sign_of_thm = #sign o rep_thm;
   235 val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
   236 
   237 (*merge signatures of two theorems; raise exception if incompatible*)
   238 fun merge_thm_sgs (th1, th2) =
   239   Sign.merge (pairself sign_of_thm (th1, th2))
   240     handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   241 
   242 
   243 (*maps object-rule to tpairs*)
   244 fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
   245 
   246 (*maps object-rule to premises*)
   247 fun prems_of (Thm {prop, ...}) =
   248   Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   249 
   250 (*counts premises in a rule*)
   251 fun nprems_of (Thm {prop, ...}) =
   252   Logic.count_prems (Logic.skip_flexpairs prop, 0);
   253 
   254 (*maps object-rule to conclusion*)
   255 fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   256 
   257 (*the statement of any thm is a cterm*)
   258 fun cprop_of (Thm {sign, maxidx, prop, ...}) =
   259   Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop};
   260 
   261 
   262 
   263 (*** Theories ***)
   264 
   265 datatype theory =
   266   Theory of {
   267     sign: Sign.sg,
   268     new_axioms: term Symtab.table,
   269     parents: theory list};
   270 
   271 fun rep_theory (Theory args) = args;
   272 
   273 (*errors involving theories*)
   274 exception THEORY of string * theory list;
   275 
   276 
   277 val sign_of = #sign o rep_theory;
   278 val syn_of = #syn o Sign.rep_sg o sign_of;
   279 
   280 (*stamps associated with a theory*)
   281 val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
   282 
   283 (*return the immediate ancestors*)
   284 val parents_of = #parents o rep_theory;
   285 
   286 
   287 (*compare theories*)
   288 val subthy = Sign.subsig o pairself sign_of;
   289 val eq_thy = Sign.eq_sg o pairself sign_of;
   290 
   291 
   292 (*look up the named axiom in the theory*)
   293 fun get_axiom theory name =
   294   let
   295     fun get_ax [] = raise Match
   296       | get_ax (Theory {sign, new_axioms, parents} :: thys) =
   297           (case Symtab.lookup (new_axioms, name) of
   298             Some t =>
   299               Thm {sign = sign, maxidx = maxidx_of_term t, hyps = [], prop = t}
   300           | None => get_ax parents handle Match => get_ax thys);
   301   in
   302     get_ax [theory] handle Match
   303       => raise THEORY ("get_axiom: no axiom " ^ quote name, [theory])
   304   end;
   305 
   306 (*return additional axioms of this theory node*)
   307 fun axioms_of thy =
   308   map (fn (s, _) => (s, get_axiom thy s))
   309     (Symtab.dest (#new_axioms (rep_theory thy)));
   310 
   311 
   312 (* the Pure theories *)
   313 
   314 val proto_pure_thy =
   315   Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []};
   316 
   317 val pure_thy =
   318   Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []};
   319 
   320 val cpure_thy =
   321   Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []};
   322 
   323 
   324 
   325 (** extend theory **)
   326 
   327 fun err_dup_axms names =
   328   error ("Duplicate axiom name(s) " ^ commas_quote names);
   329 
   330 fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms =
   331   let
   332     val draft = Sign.is_draft sign;
   333     val new_axioms1 =
   334       Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms)
   335         handle Symtab.DUPS names => err_dup_axms names;
   336     val parents1 = if draft then parents else [thy];
   337   in
   338     Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1}
   339   end;
   340 
   341 
   342 (* extend signature of a theory *)
   343 
   344 fun ext_sg extfun decls (thy as Theory {sign, ...}) =
   345   ext_thy thy (extfun decls sign) [];
   346 
   347 val add_classes   = ext_sg Sign.add_classes;
   348 val add_classrel  = ext_sg Sign.add_classrel;
   349 val add_defsort   = ext_sg Sign.add_defsort;
   350 val add_types     = ext_sg Sign.add_types;
   351 val add_tyabbrs   = ext_sg Sign.add_tyabbrs;
   352 val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i;
   353 val add_arities   = ext_sg Sign.add_arities;
   354 val add_consts    = ext_sg Sign.add_consts;
   355 val add_consts_i  = ext_sg Sign.add_consts_i;
   356 val add_syntax    = ext_sg Sign.add_syntax;
   357 val add_syntax_i  = ext_sg Sign.add_syntax_i;
   358 val add_trfuns    = ext_sg Sign.add_trfuns;
   359 val add_trrules   = ext_sg Sign.add_trrules;
   360 val add_trrules_i = ext_sg Sign.add_trrules_i;
   361 val add_thyname   = ext_sg Sign.add_name;
   362 
   363 
   364 (* prepare axioms *)
   365 
   366 fun err_in_axm name =
   367   error ("The error(s) above occurred in axiom " ^ quote name);
   368 
   369 fun no_vars tm =
   370   if null (term_vars tm) andalso null (term_tvars tm) then tm
   371   else error "Illegal schematic variable(s) in term";
   372 
   373 fun cert_axm sg (name, raw_tm) =
   374   let
   375     val Cterm {t, T, ...} = cterm_of sg raw_tm
   376       handle TERM (msg, _) => error msg;
   377   in
   378     assert (T = propT) "Term not of type prop";
   379     (name, no_vars t)
   380   end
   381   handle ERROR => err_in_axm name;
   382 
   383 fun read_axm sg (name, str) =
   384   (name, no_vars (term_of (read_cterm sg (str, propT))))
   385     handle ERROR => err_in_axm name;
   386 
   387 fun inferT_axm sg (name, pre_tm) =
   388   let val t = #2(Sign.infer_types sg (K None) (K None) [] true
   389                                      ([pre_tm], propT))
   390   in  (name, no_vars t) end
   391   handle ERROR => err_in_axm name;
   392 
   393 
   394 (* extend axioms of a theory *)
   395 
   396 fun ext_axms prep_axm axms (thy as Theory {sign, ...}) =
   397   let
   398     val sign1 = Sign.make_draft sign;
   399     val axioms = map (apsnd Logic.varify o prep_axm sign) axms;
   400   in
   401     ext_thy thy sign1 axioms
   402   end;
   403 
   404 val add_axioms = ext_axms read_axm;
   405 val add_axioms_i = ext_axms cert_axm;
   406 
   407 
   408 
   409 (** merge theories **)
   410 
   411 fun merge_thy_list mk_draft thys =
   412   let
   413     fun is_union thy = forall (fn t => subthy (t, thy)) thys;
   414     val is_draft = Sign.is_draft o sign_of;
   415 
   416     fun add_sign (sg, Theory {sign, ...}) =
   417       Sign.merge (sg, sign) handle TERM (msg, _) => error msg;
   418   in
   419     (case (find_first is_union thys, exists is_draft thys) of
   420       (Some thy, _) => thy
   421     | (None, true) => raise THEORY ("Illegal merge of draft theories", thys)
   422     | (None, false) => Theory {
   423         sign =
   424           (if mk_draft then Sign.make_draft else I)
   425           (foldl add_sign (Sign.proto_pure, thys)),
   426         new_axioms = Symtab.null,
   427         parents = thys})
   428   end;
   429 
   430 fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2];
   431 
   432 
   433 
   434 (**** Primitive rules ****)
   435 
   436 (* discharge all assumptions t from ts *)
   437 val disch = gen_rem (op aconv);
   438 
   439 (*The assumption rule A|-A in a theory  *)
   440 fun assume ct : thm =
   441   let val {sign, t=prop, T, maxidx} = rep_cterm ct
   442   in  if T<>propT then
   443         raise THM("assume: assumptions must have type prop", 0, [])
   444       else if maxidx <> ~1 then
   445         raise THM("assume: assumptions may not contain scheme variables",
   446                   maxidx, [])
   447       else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop}
   448   end;
   449 
   450 (* Implication introduction
   451               A |- B
   452               -------
   453               A ==> B    *)
   454 fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
   455   let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
   456   in  if T<>propT then
   457         raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   458       else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx],
   459              hyps= disch(hyps,A),  prop= implies$A$prop}
   460       handle TERM _ =>
   461         raise THM("implies_intr: incompatible signatures", 0, [thB])
   462   end;
   463 
   464 (* Implication elimination
   465         A ==> B       A
   466         ---------------
   467                 B      *)
   468 fun implies_elim thAB thA : thm =
   469     let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA
   470         and Thm{sign, maxidx, hyps, prop,...} = thAB;
   471         fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   472     in  case prop of
   473             imp$A$B =>
   474                 if imp=implies andalso  A aconv propA
   475                 then  Thm{sign= merge_thm_sgs(thAB,thA),
   476                           maxidx= max[maxA,maxidx],
   477                           hyps= hypsA union hyps,  (*dups suppressed*)
   478                           prop= B}
   479                 else err("major premise")
   480           | _ => err("major premise")
   481     end;
   482 
   483 (* Forall introduction.  The Free or Var x must not be free in the hypotheses.
   484      A
   485    ------
   486    !!x.A       *)
   487 fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
   488   let val x = term_of cx;
   489       fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   490                             prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   491   in  case x of
   492         Free(a,T) =>
   493           if exists (apl(x, Logic.occs)) hyps
   494           then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   495           else  result(a,T)
   496       | Var((a,_),T) => result(a,T)
   497       | _ => raise THM("forall_intr: not a variable", 0, [th])
   498   end;
   499 
   500 (* Forall elimination
   501               !!x.A
   502              --------
   503               A[t/x]     *)
   504 fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
   505   let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
   506   in  case prop of
   507           Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   508             if T<>qary then
   509                 raise THM("forall_elim: type mismatch", 0, [th])
   510             else Thm{sign= Sign.merge(sign,signt),
   511                      maxidx= max[maxidx, maxt],
   512                      hyps= hyps,  prop= betapply(A,t)}
   513         | _ => raise THM("forall_elim: not quantified", 0, [th])
   514   end
   515   handle TERM _ =>
   516          raise THM("forall_elim: incompatible signatures", 0, [th]);
   517 
   518 
   519 (*** Equality ***)
   520 
   521 (*Definition of the relation =?= *)
   522 val flexpair_def =
   523   Thm{sign= Sign.proto_pure, hyps= [], maxidx= 0,
   524       prop= term_of
   525               (read_cterm Sign.proto_pure
   526                  ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   527 
   528 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   529 fun reflexive ct =
   530   let val {sign, t, T, maxidx} = rep_cterm ct
   531   in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
   532   end;
   533 
   534 (*The symmetry rule
   535     t==u
   536     ----
   537     u==t         *)
   538 fun symmetric (th as Thm{sign,hyps,prop,maxidx}) =
   539   case prop of
   540       (eq as Const("==",_)) $ t $ u =>
   541           Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t}
   542     | _ => raise THM("symmetric", 0, [th]);
   543 
   544 (*The transitive rule
   545     t1==u    u==t2
   546     ------------
   547         t1==t2      *)
   548 fun transitive th1 th2 =
   549   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   550       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   551       fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   552   in case (prop1,prop2) of
   553        ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   554           if not (u aconv u') then err"middle term"  else
   555               Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
   556                   maxidx= max[max1,max2], prop= eq$t1$t2}
   557      | _ =>  err"premises"
   558   end;
   559 
   560 (*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
   561 fun beta_conversion ct =
   562   let val {sign, t, T, maxidx} = rep_cterm ct
   563   in  case t of
   564           Abs(_,_,bodt) $ u =>
   565             Thm{sign= sign,  hyps= [],
   566                 maxidx= maxidx_of_term t,
   567                 prop= Logic.mk_equals(t, subst_bounds([u],bodt))}
   568         | _ =>  raise THM("beta_conversion: not a redex", 0, [])
   569   end;
   570 
   571 (*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
   572     f(x) == g(x)
   573     ------------
   574        f == g    *)
   575 fun extensional (th as Thm{sign,maxidx,hyps,prop}) =
   576   case prop of
   577     (Const("==",_)) $ (f$x) $ (g$y) =>
   578       let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
   579       in (if x<>y then err"different variables" else
   580           case y of
   581                 Free _ =>
   582                   if exists (apl(y, Logic.occs)) (f::g::hyps)
   583                   then err"variable free in hyps or functions"    else  ()
   584               | Var _ =>
   585                   if Logic.occs(y,f)  orelse  Logic.occs(y,g)
   586                   then err"variable free in functions"   else  ()
   587               | _ => err"not a variable");
   588           Thm{sign=sign, hyps=hyps, maxidx=maxidx,
   589               prop= Logic.mk_equals(f,g)}
   590       end
   591  | _ =>  raise THM("extensional: premise", 0, [th]);
   592 
   593 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   594   The bound variable will be named "a" (since x will be something like x320)
   595           t == u
   596     ----------------
   597       %(x)t == %(x)u     *)
   598 fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
   599   let val x = term_of cx;
   600       val (t,u) = Logic.dest_equals prop
   601             handle TERM _ =>
   602                 raise THM("abstract_rule: premise not an equality", 0, [th])
   603       fun result T =
   604             Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   605                 prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   606                                       Abs(a, T, abstract_over (x,u)))}
   607   in  case x of
   608         Free(_,T) =>
   609          if exists (apl(x, Logic.occs)) hyps
   610          then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   611          else result T
   612       | Var(_,T) => result T
   613       | _ => raise THM("abstract_rule: not a variable", 0, [th])
   614   end;
   615 
   616 (*The combination rule
   617     f==g    t==u
   618     ------------
   619      f(t)==g(u)      *)
   620 fun combination th1 th2 =
   621   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   622       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2
   623   in  case (prop1,prop2)  of
   624        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   625               Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
   626                   maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
   627      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   628   end;
   629 
   630 
   631 (*The equal propositions rule
   632     A==B    A
   633     ---------
   634         B          *)
   635 fun equal_elim th1 th2 =
   636   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   637       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   638       fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   639   in  case prop1  of
   640        Const("==",_) $ A $ B =>
   641           if not (prop2 aconv A) then err"not equal"  else
   642               Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
   643                   maxidx= max[max1,max2], prop= B}
   644      | _ =>  err"major premise"
   645   end;
   646 
   647 
   648 (* Equality introduction
   649     A==>B    B==>A
   650     -------------
   651          A==B            *)
   652 fun equal_intr th1 th2 =
   653 let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   654     and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   655     fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   656 in case (prop1,prop2) of
   657      (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   658         if A aconv A' andalso B aconv B'
   659         then Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2,
   660                  maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}
   661         else err"not equal"
   662    | _ =>  err"premises"
   663 end;
   664 
   665 (**** Derived rules ****)
   666 
   667 (*Discharge all hypotheses (need not verify cterms)
   668   Repeated hypotheses are discharged only once;  fold cannot do this*)
   669 fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) =
   670       implies_intr_hyps
   671             (Thm{sign=sign,  maxidx=maxidx,
   672                  hyps= disch(As,A),  prop= implies$A$prop})
   673   | implies_intr_hyps th = th;
   674 
   675 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   676   Instantiates the theorem and deletes trivial tpairs.
   677   Resulting sequence may contain multiple elements if the tpairs are
   678     not all flex-flex. *)
   679 fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) =
   680   let fun newthm env =
   681           let val (tpairs,horn) =
   682                         Logic.strip_flexpairs (Envir.norm_term env prop)
   683                 (*Remove trivial tpairs, of the form t=t*)
   684               val distpairs = filter (not o op aconv) tpairs
   685               val newprop = Logic.list_flexpairs(distpairs, horn)
   686           in  Thm{sign= sign, hyps= hyps,
   687                   maxidx= maxidx_of_term newprop, prop= newprop}
   688           end;
   689       val (tpairs,_) = Logic.strip_flexpairs prop
   690   in Sequence.maps newthm
   691             (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
   692   end;
   693 
   694 (*Instantiation of Vars
   695                       A
   696              --------------------
   697               A[t1/v1,....,tn/vn]     *)
   698 
   699 (*Check that all the terms are Vars and are distinct*)
   700 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   701 
   702 (*For instantiate: process pair of cterms, merge theories*)
   703 fun add_ctpair ((ct,cu), (sign,tpairs)) =
   704   let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
   705       and {sign=signu, t=u, T= U, ...} = rep_cterm cu
   706   in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   707       else raise TYPE("add_ctpair", [T,U], [t,u])
   708   end;
   709 
   710 fun add_ctyp ((v,ctyp), (sign',vTs)) =
   711   let val {T,sign} = rep_ctyp ctyp
   712   in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   713 
   714 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   715   Instantiates distinct Vars by terms of same type.
   716   Normalizes the new theorem! *)
   717 fun instantiate (vcTs,ctpairs)  (th as Thm{sign,maxidx,hyps,prop}) =
   718   let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
   719       val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
   720       val newprop =
   721             Envir.norm_term (Envir.empty 0)
   722               (subst_atomic tpairs
   723                (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop))
   724       val newth = Thm{sign= newsign, hyps= hyps,
   725                       maxidx= maxidx_of_term newprop, prop= newprop}
   726   in  if not(instl_ok(map #1 tpairs))
   727       then raise THM("instantiate: variables not distinct", 0, [th])
   728       else if not(null(findrep(map #1 vTs)))
   729       then raise THM("instantiate: type variables not distinct", 0, [th])
   730       else (*Check types of Vars for agreement*)
   731       case findrep (map (#1 o dest_Var) (term_vars newprop)) of
   732           ix::_ => raise THM("instantiate: conflicting types for variable " ^
   733                              Syntax.string_of_vname ix ^ "\n", 0, [newth])
   734         | [] =>
   735              case findrep (map #1 (term_tvars newprop)) of
   736              ix::_ => raise THM
   737                     ("instantiate: conflicting sorts for type variable " ^
   738                      Syntax.string_of_vname ix ^ "\n", 0, [newth])
   739         | [] => newth
   740   end
   741   handle TERM _ =>
   742            raise THM("instantiate: incompatible signatures",0,[th])
   743        | TYPE _ => raise THM("instantiate: type conflict", 0, [th]);
   744 
   745 (*The trivial implication A==>A, justified by assume and forall rules.
   746   A can contain Vars, not so for assume!   *)
   747 fun trivial ct : thm =
   748   let val {sign, t=A, T, maxidx} = rep_cterm ct
   749   in  if T<>propT then
   750             raise THM("trivial: the term must have type prop", 0, [])
   751       else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   752   end;
   753 
   754 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" --
   755   essentially an instance of A==>A.*)
   756 fun class_triv thy c =
   757   let
   758     val sign = sign_of thy;
   759     val Cterm {t, maxidx, ...} =
   760       cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
   761         handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   762   in
   763     Thm {sign = sign, maxidx = maxidx, hyps = [], prop = t}
   764   end;
   765 
   766 
   767 (* Replace all TFrees not in the hyps by new TVars *)
   768 fun varifyT(Thm{sign,maxidx,hyps,prop}) =
   769   let val tfrees = foldr add_term_tfree_names (hyps,[])
   770   in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps,
   771          prop= Type.varify(prop,tfrees)}
   772   end;
   773 
   774 (* Replace all TVars by new TFrees *)
   775 fun freezeT(Thm{sign,maxidx,hyps,prop}) =
   776   let val prop' = Type.freeze prop
   777   in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;
   778 
   779 
   780 (*** Inference rules for tactics ***)
   781 
   782 (*Destruct proof state into constraints, other goals, goal(i), rest *)
   783 fun dest_state (state as Thm{prop,...}, i) =
   784   let val (tpairs,horn) = Logic.strip_flexpairs prop
   785   in  case  Logic.strip_prems(i, [], horn) of
   786           (B::rBs, C) => (tpairs, rev rBs, B, C)
   787         | _ => raise THM("dest_state", i, [state])
   788   end
   789   handle TERM _ => raise THM("dest_state", i, [state]);
   790 
   791 (*Increment variables and parameters of orule as required for
   792   resolution with goal i of state. *)
   793 fun lift_rule (state, i) orule =
   794   let val Thm{prop=sprop,maxidx=smax,...} = state;
   795       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
   796         handle TERM _ => raise THM("lift_rule", i, [orule,state]);
   797       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1);
   798       val (Thm{sign,maxidx,hyps,prop}) = orule
   799       val (tpairs,As,B) = Logic.strip_horn prop
   800   in  Thm{hyps=hyps, sign= merge_thm_sgs(state,orule),
   801           maxidx= maxidx+smax+1,
   802           prop= Logic.rule_of(map (pairself lift_abs) tpairs,
   803                               map lift_all As,    lift_all B)}
   804   end;
   805 
   806 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   807 fun assumption i state =
   808   let val Thm{sign,maxidx,hyps,prop} = state;
   809       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   810       fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
   811           Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   812             if Envir.is_empty env then (*avoid wasted normalizations*)
   813               Logic.rule_of (tpairs, Bs, C)
   814             else (*normalize the new rule fully*)
   815               Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))};
   816       fun addprfs [] = Sequence.null
   817         | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   818              (Sequence.mapp newth
   819                 (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs))
   820                 (addprfs apairs)))
   821   in  addprfs (Logic.assum_pairs Bi)  end;
   822 
   823 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
   824   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
   825 fun eq_assumption i state =
   826   let val Thm{sign,maxidx,hyps,prop} = state;
   827       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   828   in  if exists (op aconv) (Logic.assum_pairs Bi)
   829       then Thm{sign=sign, hyps=hyps, maxidx=maxidx,
   830                prop=Logic.rule_of(tpairs, Bs, C)}
   831       else  raise THM("eq_assumption", 0, [state])
   832   end;
   833 
   834 
   835 (** User renaming of parameters in a subgoal **)
   836 
   837 (*Calls error rather than raising an exception because it is intended
   838   for top-level use -- exception handling would not make sense here.
   839   The names in cs, if distinct, are used for the innermost parameters;
   840    preceding parameters may be renamed to make all params distinct.*)
   841 fun rename_params_rule (cs, i) state =
   842   let val Thm{sign,maxidx,hyps,prop} = state
   843       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   844       val iparams = map #1 (Logic.strip_params Bi)
   845       val short = length iparams - length cs
   846       val newnames =
   847             if short<0 then error"More names than abstractions!"
   848             else variantlist(take (short,iparams), cs) @ cs
   849       val freenames = map (#1 o dest_Free) (term_frees prop)
   850       val newBi = Logic.list_rename_params (newnames, Bi)
   851   in
   852   case findrep cs of
   853      c::_ => error ("Bound variables not distinct: " ^ c)
   854    | [] => (case cs inter freenames of
   855        a::_ => error ("Bound/Free variable clash: " ^ a)
   856      | [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   857                     Logic.rule_of(tpairs, Bs@[newBi], C)})
   858   end;
   859 
   860 (*** Preservation of bound variable names ***)
   861 
   862 (*Scan a pair of terms; while they are similar,
   863   accumulate corresponding bound vars in "al"*)
   864 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)
   865   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   866   | match_bvs(_,_,al) = al;
   867 
   868 (* strip abstractions created by parameters *)
   869 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   870 
   871 
   872 (* strip_apply f A(,B) strips off all assumptions/parameters from A
   873    introduced by lifting over B, and applies f to remaining part of A*)
   874 fun strip_apply f =
   875   let fun strip(Const("==>",_)$ A1 $ B1,
   876                 Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
   877         | strip((c as Const("all",_)) $ Abs(a,T,t1),
   878                       Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
   879         | strip(A,_) = f A
   880   in strip end;
   881 
   882 (*Use the alist to rename all bound variables and some unknowns in a term
   883   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
   884   Preserves unknowns in tpairs and on lhs of dpairs. *)
   885 fun rename_bvs([],_,_,_) = I
   886   | rename_bvs(al,dpairs,tpairs,B) =
   887     let val vars = foldr add_term_vars
   888                         (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
   889         (*unknowns appearing elsewhere be preserved!*)
   890         val vids = map (#1 o #1 o dest_Var) vars;
   891         fun rename(t as Var((x,i),T)) =
   892                 (case assoc(al,x) of
   893                    Some(y) => if x mem vids orelse y mem vids then t
   894                               else Var((y,i),T)
   895                  | None=> t)
   896           | rename(Abs(x,T,t)) =
   897               Abs(case assoc(al,x) of Some(y) => y | None => x,
   898                   T, rename t)
   899           | rename(f$t) = rename f $ rename t
   900           | rename(t) = t;
   901         fun strip_ren Ai = strip_apply rename (Ai,B)
   902     in strip_ren end;
   903 
   904 (*Function to rename bounds/unknowns in the argument, lifted over B*)
   905 fun rename_bvars(dpairs, tpairs, B) =
   906         rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
   907 
   908 
   909 (*** RESOLUTION ***)
   910 
   911 (** Lifting optimizations **)
   912 
   913 (*strip off pairs of assumptions/parameters in parallel -- they are
   914   identical because of lifting*)
   915 fun strip_assums2 (Const("==>", _) $ _ $ B1,
   916                    Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
   917   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
   918                    Const("all",_)$Abs(_,_,t2)) =
   919       let val (B1,B2) = strip_assums2 (t1,t2)
   920       in  (Abs(a,T,B1), Abs(a,T,B2))  end
   921   | strip_assums2 BB = BB;
   922 
   923 
   924 (*Faster normalization: skip assumptions that were lifted over*)
   925 fun norm_term_skip env 0 t = Envir.norm_term env t
   926   | norm_term_skip env n (Const("all",_)$Abs(a,T,t)) =
   927         let val Envir.Envir{iTs, ...} = env
   928 	    val T' = typ_subst_TVars iTs T
   929 	    (*Must instantiate types of parameters because they are flattened;
   930               this could be a NEW parameter*)
   931         in  all T' $ Abs(a, T', norm_term_skip env n t)  end
   932   | norm_term_skip env n (Const("==>", _) $ A $ B) =
   933 	implies $ A $ norm_term_skip env (n-1) B
   934   | norm_term_skip env n t = error"norm_term_skip: too few assumptions??";
   935 
   936 
   937 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
   938   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)
   939   If match then forbid instantiations in proof state
   940   If lifted then shorten the dpair using strip_assums2.
   941   If eres_flg then simultaneously proves A1 by assumption.
   942   nsubgoal is the number of new subgoals (written m above).
   943   Curried so that resolution calls dest_state only once.
   944 *)
   945 local open Sequence; exception Bicompose
   946 in
   947 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
   948                         (eres_flg, orule, nsubgoal) =
   949  let val Thm{maxidx=smax, hyps=shyps, ...} = state
   950      and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule
   951 	     (*How many hyps to skip over during normalization*)
   952      and nlift = Logic.count_prems(strip_all_body Bi, 
   953 				   if eres_flg then ~1 else 0)
   954      val sign = merge_thm_sgs(state,orule);
   955      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
   956      fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
   957        let val normt = Envir.norm_term env;
   958            (*perform minimal copying here by examining env*)
   959            val normp =
   960              if Envir.is_empty env then (tpairs, Bs @ As, C)
   961              else
   962              let val ntps = map (pairself normt) tpairs
   963              in if the (Envir.minidx env) > smax then 
   964 		  (*no assignments in state; normalize the rule only*)
   965                   if lifted 
   966 		  then (ntps, Bs @ map (norm_term_skip env nlift) As, C)
   967 		  else (ntps, Bs @ map normt As, C)
   968                 else if match then raise Bicompose
   969                 else (*normalize the new rule fully*)
   970                   (ntps, map normt (Bs @ As), normt C)
   971              end
   972            val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx,
   973                         prop= Logic.rule_of normp}
   974         in  cons(th, thq)  end  handle Bicompose => thq
   975      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
   976      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
   977        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
   978      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
   979      fun newAs(As0, n, dpairs, tpairs) =
   980        let val As1 = if !Logic.auto_rename orelse not lifted then As0
   981                      else map (rename_bvars(dpairs,tpairs,B)) As0
   982        in (map (Logic.flatten_params n) As1)
   983           handle TERM _ =>
   984           raise THM("bicompose: 1st premise", 0, [orule])
   985        end;
   986      val env = Envir.empty(max[rmax,smax]);
   987      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
   988      val dpairs = BBi :: (rtpairs@stpairs);
   989      (*elim-resolution: try each assumption in turn.  Initially n=1*)
   990      fun tryasms (_, _, []) = null
   991        | tryasms (As, n, (t,u)::apairs) =
   992           (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
   993                None                   => tryasms (As, n+1, apairs)
   994              | cell as Some((_,tpairs),_) =>
   995                    its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
   996                        (seqof (fn()=> cell),
   997                         seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
   998      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
   999        | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
  1000      (*ordinary resolution*)
  1001      fun res(None) = null
  1002        | res(cell as Some((_,tpairs),_)) =
  1003              its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
  1004                        (seqof (fn()=> cell), null)
  1005  in  if eres_flg then eres(rev rAs)
  1006      else res(pull(Unify.unifiers(sign, env, dpairs)))
  1007  end;
  1008 end;  (*open Sequence*)
  1009 
  1010 
  1011 fun bicompose match arg i state =
  1012     bicompose_aux match (state, dest_state(state,i), false) arg;
  1013 
  1014 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1015   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1016 fun could_bires (Hs, B, eres_flg, rule) =
  1017     let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
  1018           | could_reshyp [] = false;  (*no premise -- illegal*)
  1019     in  could_unify(concl_of rule, B) andalso
  1020         (not eres_flg  orelse  could_reshyp (prems_of rule))
  1021     end;
  1022 
  1023 (*Bi-resolution of a state with a list of (flag,rule) pairs.
  1024   Puts the rule above:  rule/state.  Renames vars in the rules. *)
  1025 fun biresolution match brules i state =
  1026     let val lift = lift_rule(state, i);
  1027         val (stpairs, Bs, Bi, C) = dest_state(state,i)
  1028         val B = Logic.strip_assums_concl Bi;
  1029         val Hs = Logic.strip_assums_hyp Bi;
  1030         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
  1031         fun res [] = Sequence.null
  1032           | res ((eres_flg, rule)::brules) =
  1033               if could_bires (Hs, B, eres_flg, rule)
  1034               then Sequence.seqof (*delay processing remainder till needed*)
  1035                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
  1036                                res brules))
  1037               else res brules
  1038     in  Sequence.flats (res brules)  end;
  1039 
  1040 
  1041 
  1042 (*** Meta simp sets ***)
  1043 
  1044 type rrule = {thm:thm, lhs:term, perm:bool};
  1045 type cong = {thm:thm, lhs:term};
  1046 datatype meta_simpset =
  1047   Mss of {net:rrule Net.net, congs:(string * cong)list, bounds:string list,
  1048           prems: thm list, mk_rews: thm -> thm list};
  1049 
  1050 (*A "mss" contains data needed during conversion:
  1051   net: discrimination net of rewrite rules
  1052   congs: association list of congruence rules
  1053   bounds: names of bound variables already used;
  1054           for generating new names when rewriting under lambda abstractions
  1055   mk_rews: used when local assumptions are added
  1056 *)
  1057 
  1058 val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [],
  1059                     mk_rews = K[]};
  1060 
  1061 exception SIMPLIFIER of string * thm;
  1062 
  1063 fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
  1064 
  1065 val trace_simp = ref false;
  1066 
  1067 fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
  1068 
  1069 fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
  1070 
  1071 fun vperm(Var _, Var _) = true
  1072   | vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t)
  1073   | vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2)
  1074   | vperm(t,u) = (t=u);
  1075 
  1076 fun var_perm(t,u) = vperm(t,u) andalso
  1077                     eq_set(add_term_vars(t,[]), add_term_vars(u,[]))
  1078 
  1079 (*simple test for looping rewrite*)
  1080 fun loops sign prems (lhs,rhs) =
  1081    is_Var(lhs)
  1082   orelse
  1083    (exists (apl(lhs, Logic.occs)) (rhs::prems))
  1084   orelse
  1085    (null(prems) andalso
  1086     Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs));
  1087 (* the condition "null(prems)" in the last case is necessary because
  1088    conditional rewrites with extra variables in the conditions may terminate
  1089    although the rhs is an instance of the lhs. Example:
  1090    ?m < ?n ==> f(?n) == f(?m)
  1091 *)
  1092 
  1093 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
  1094   let val prems = Logic.strip_imp_prems prop
  1095       val concl = Logic.strip_imp_concl prop
  1096       val (lhs,_) = Logic.dest_equals concl handle TERM _ =>
  1097                       raise SIMPLIFIER("Rewrite rule not a meta-equality",thm)
  1098       val econcl = Pattern.eta_contract concl
  1099       val (elhs,erhs) = Logic.dest_equals econcl
  1100       val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs)
  1101                                      andalso not(is_Var(elhs))
  1102   in if not perm andalso loops sign prems (elhs,erhs)
  1103      then (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
  1104      else Some{thm=thm,lhs=lhs,perm=perm}
  1105   end;
  1106 
  1107 local
  1108  fun eq({thm=Thm{prop=p1,...},...}:rrule,
  1109         {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
  1110 in
  1111 
  1112 fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews},
  1113              thm as Thm{sign,prop,...}) =
  1114   case mk_rrule thm of
  1115     None => mss
  1116   | Some(rrule as {lhs,...}) =>
  1117       (trace_thm "Adding rewrite rule:" thm;
  1118        Mss{net= (Net.insert_term((lhs,rrule),net,eq)
  1119                  handle Net.INSERT =>
  1120                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
  1121                    net)),
  1122            congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews});
  1123 
  1124 fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews},
  1125              thm as Thm{sign,prop,...}) =
  1126   case mk_rrule thm of
  1127     None => mss
  1128   | Some(rrule as {lhs,...}) =>
  1129       Mss{net= (Net.delete_term((lhs,rrule),net,eq)
  1130                 handle Net.INSERT =>
  1131                  (prtm "Warning: rewrite rule not in simpset" sign prop;
  1132                   net)),
  1133              congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}
  1134 
  1135 end;
  1136 
  1137 val add_simps = foldl add_simp;
  1138 val del_simps = foldl del_simp;
  1139 
  1140 fun mss_of thms = add_simps(empty_mss,thms);
  1141 
  1142 fun add_cong(Mss{net,congs,bounds,prems,mk_rews},thm) =
  1143   let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ =>
  1144                     raise SIMPLIFIER("Congruence not a meta-equality",thm)
  1145 (*      val lhs = Pattern.eta_contract lhs*)
  1146       val (a,_) = dest_Const (head_of lhs) handle TERM _ =>
  1147                   raise SIMPLIFIER("Congruence must start with a constant",thm)
  1148   in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds,
  1149          prems=prems, mk_rews=mk_rews}
  1150   end;
  1151 
  1152 val (op add_congs) = foldl add_cong;
  1153 
  1154 fun add_prems(Mss{net,congs,bounds,prems,mk_rews},thms) =
  1155   Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews};
  1156 
  1157 fun prems_of_mss(Mss{prems,...}) = prems;
  1158 
  1159 fun set_mk_rews(Mss{net,congs,bounds,prems,...},mk_rews) =
  1160   Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews};
  1161 fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews;
  1162 
  1163 
  1164 (*** Meta-level rewriting
  1165      uses conversions, omitting proofs for efficiency.  See
  1166         L C Paulson, A higher-order implementation of rewriting,
  1167         Science of Computer Programming 3 (1983), pages 119-149. ***)
  1168 
  1169 type prover = meta_simpset -> thm -> thm option;
  1170 type termrec = (Sign.sg * term list) * term;
  1171 type conv = meta_simpset -> termrec -> termrec;
  1172 
  1173 datatype order = LESS | EQUAL | GREATER;
  1174 
  1175 fun stringord(a,b:string) = if a<b then LESS  else
  1176                             if a=b then EQUAL else GREATER;
  1177 
  1178 fun intord(i,j:int) = if i<j then LESS  else
  1179                       if i=j then EQUAL else GREATER;
  1180 
  1181 (* NB: non-linearity of the ordering is not a soundness problem *)
  1182 
  1183 (* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
  1184 fun string_of_hd(Const(a,_)) = a
  1185   | string_of_hd(Free(a,_))  = a
  1186   | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
  1187   | string_of_hd(Bound i)    = string_of_int i
  1188   | string_of_hd(Abs _)      = "***ABSTRACTION***";
  1189 
  1190 (* a strict (not reflexive) linear well-founded AC-compatible ordering
  1191  * for terms:
  1192  * s < t <=> 1. size(s) < size(t) or
  1193              2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
  1194              3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
  1195                 (s1..sn) < (t1..tn) (lexicographically)
  1196  *)
  1197 
  1198 (* FIXME: should really take types into account as well.
  1199  * Otherwise non-linear *)
  1200 fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
  1201   | termord(t,u) =
  1202       (case intord(size_of_term t,size_of_term u) of
  1203          EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
  1204                   in case stringord(string_of_hd f, string_of_hd g) of
  1205                        EQUAL => lextermord(ts,us)
  1206                      | ord   => ord
  1207                   end
  1208        | ord => ord)
  1209 and lextermord(t::ts,u::us) =
  1210       (case termord(t,u) of
  1211          EQUAL => lextermord(ts,us)
  1212        | ord   => ord)
  1213   | lextermord([],[]) = EQUAL
  1214   | lextermord _ = error("lextermord");
  1215 
  1216 fun termless tu = (termord tu = LESS);
  1217 
  1218 fun check_conv(thm as Thm{hyps,prop,sign,maxidx,...}, prop0) =
  1219   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm;
  1220                    trace_term "Should have proved" sign prop0;
  1221                    None)
  1222       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
  1223   in case prop of
  1224        Const("==",_) $ lhs $ rhs =>
  1225          if (lhs = lhs0) orelse
  1226             (lhs aconv Envir.norm_term (Envir.empty 0) lhs0)
  1227          then (trace_thm "SUCCEEDED" thm; Some(hyps,maxidx,rhs))
  1228          else err()
  1229      | _ => err()
  1230   end;
  1231 
  1232 fun ren_inst(insts,prop,pat,obj) =
  1233   let val ren = match_bvs(pat,obj,[])
  1234       fun renAbs(Abs(x,T,b)) =
  1235             Abs(case assoc(ren,x) of None => x | Some(y) => y, T, renAbs(b))
  1236         | renAbs(f$t) = renAbs(f) $ renAbs(t)
  1237         | renAbs(t) = t
  1238   in subst_vars insts (if null(ren) then prop else renAbs(prop)) end;
  1239 
  1240 
  1241 (*Conversion to apply the meta simpset to a term*)
  1242 fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,maxidxt,t) =
  1243   let val etat = Pattern.eta_contract t;
  1244       fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} =
  1245         let val unit = if Sign.subsig(sign,signt) then ()
  1246                   else (trace_thm"Warning: rewrite rule from different theory"
  1247                           thm;
  1248                         raise Pattern.MATCH)
  1249             val rprop = if maxidxt = ~1 then prop
  1250                         else Logic.incr_indexes([],maxidxt+1) prop;
  1251             val rlhs = if maxidxt = ~1 then lhs
  1252                        else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
  1253             val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat)
  1254             val prop' = ren_inst(insts,rprop,rlhs,t);
  1255             val hyps' = hyps union hypst;
  1256             val maxidx' = maxidx_of_term prop'
  1257             val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx'}
  1258             val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop')
  1259         in if perm andalso not(termless(rhs',lhs')) then None else
  1260            if Logic.count_prems(prop',0) = 0
  1261            then (trace_thm "Rewriting:" thm'; Some(hyps',maxidx',rhs'))
  1262            else (trace_thm "Trying to rewrite:" thm';
  1263                  case prover mss thm' of
  1264                    None       => (trace_thm "FAILED" thm'; None)
  1265                  | Some(thm2) => check_conv(thm2,prop'))
  1266         end
  1267 
  1268       fun rews [] = None
  1269         | rews (rrule::rrules) =
  1270             let val opt = rew rrule handle Pattern.MATCH => None
  1271             in case opt of None => rews rrules | some => some end;
  1272 
  1273   in case etat of
  1274        Abs(_,_,body) $ u => Some(hypst, maxidxt, subst_bounds([u], body))
  1275      | _                 => rews(Net.match_term net etat)
  1276   end;
  1277 
  1278 (*Conversion to apply a congruence rule to a term*)
  1279 fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,maxidxt,t) =
  1280   let val Thm{sign,hyps,maxidx,prop,...} = cong
  1281       val unit = if Sign.subsig(sign,signt) then ()
  1282                  else error("Congruence rule from different theory")
  1283       val tsig = #tsig(Sign.rep_sg signt)
  1284       val rprop = if maxidxt = ~1 then prop
  1285                   else Logic.incr_indexes([],maxidxt+1) prop;
  1286       val rlhs = if maxidxt = ~1 then lhs
  1287                  else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
  1288       val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH =>
  1289                   error("Congruence rule did not match")
  1290       val prop' = ren_inst(insts,rprop,rlhs,t);
  1291       val thm' = Thm{sign=signt, hyps=hyps union hypst,
  1292                      prop=prop', maxidx=maxidx_of_term prop'}
  1293       val unit = trace_thm "Applying congruence rule" thm';
  1294       fun err() = error("Failed congruence proof!")
  1295 
  1296   in case prover thm' of
  1297        None => err()
  1298      | Some(thm2) => (case check_conv(thm2,prop') of
  1299                         None => err() | some => some)
  1300   end;
  1301 
  1302 
  1303 
  1304 fun bottomc ((simprem,useprem),prover,sign) =
  1305   let fun botc fail mss trec =
  1306             (case subc mss trec of
  1307                some as Some(trec1) =>
  1308                  (case rewritec (prover,sign) mss trec1 of
  1309                     Some(trec2) => botc false mss trec2
  1310                   | None => some)
  1311              | None =>
  1312                  (case rewritec (prover,sign) mss trec of
  1313                     Some(trec2) => botc false mss trec2
  1314                   | None => if fail then None else Some(trec)))
  1315 
  1316       and try_botc mss trec = (case botc true mss trec of
  1317                                  Some(trec1) => trec1
  1318                                | None => trec)
  1319 
  1320       and subc (mss as Mss{net,congs,bounds,prems,mk_rews})
  1321                (trec as (hyps,maxidx,t)) =
  1322         (case t of
  1323             Abs(a,T,t) =>
  1324               let val b = variant bounds a
  1325                   val v = Free("." ^ b,T)
  1326                   val mss' = Mss{net=net, congs=congs, bounds=b::bounds,
  1327                                  prems=prems,mk_rews=mk_rews}
  1328               in case botc true mss' (hyps,maxidx,subst_bounds([v],t)) of
  1329                    Some(hyps',maxidx',t') =>
  1330                      Some(hyps', maxidx', Abs(a, T, abstract_over(v,t')))
  1331                  | None => None
  1332               end
  1333           | t$u => (case t of
  1334               Const("==>",_)$s  => Some(impc(hyps,maxidx,s,u,mss))
  1335             | Abs(_,_,body) =>
  1336                 let val trec = (hyps,maxidx,subst_bounds([u], body))
  1337                 in case subc mss trec of
  1338                      None => Some(trec)
  1339                    | trec => trec
  1340                 end
  1341             | _  =>
  1342                 let fun appc() =
  1343                           (case botc true mss (hyps,maxidx,t) of
  1344                              Some(hyps1,maxidx1,t1) =>
  1345                                (case botc true mss (hyps1,maxidx,u) of
  1346                                   Some(hyps2,maxidx2,u1) =>
  1347                                     Some(hyps2,max[maxidx1,maxidx2],t1$u1)
  1348                                 | None =>
  1349                                     Some(hyps1,max[maxidx1,maxidx],t1$u))
  1350                            | None =>
  1351                                (case botc true mss (hyps,maxidx,u) of
  1352                                   Some(hyps1,maxidx1,u1) =>
  1353                                     Some(hyps1,max[maxidx,maxidx1],t$u1)
  1354                                 | None => None))
  1355                     val (h,ts) = strip_comb t
  1356                 in case h of
  1357                      Const(a,_) =>
  1358                        (case assoc(congs,a) of
  1359                           None => appc()
  1360                         | Some(cong) => congc (prover mss,sign) cong trec)
  1361                    | _ => appc()
  1362                 end)
  1363           | _ => None)
  1364 
  1365       and impc(hyps,maxidx,s,u,mss as Mss{mk_rews,...}) =
  1366         let val (hyps1,_,s1) = if simprem then try_botc mss (hyps,maxidx,s)
  1367                                else (hyps,0,s);
  1368             val maxidx1 = maxidx_of_term s1
  1369             val mss1 =
  1370               if not useprem orelse maxidx1 <> ~1 then mss
  1371               else let val thm = Thm{sign=sign,hyps=[s1],prop=s1,maxidx= ~1}
  1372                    in add_simps(add_prems(mss,[thm]), mk_rews thm) end
  1373             val (hyps2,maxidx2,u1) = try_botc mss1 (hyps1,maxidx,u)
  1374             val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1
  1375         in (hyps3, max[maxidx1,maxidx2], Logic.mk_implies(s1,u1)) end
  1376 
  1377   in try_botc end;
  1378 
  1379 
  1380 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
  1381 (* Parameters:
  1382    mode = (simplify A, use A in simplifying B) when simplifying A ==> B
  1383    mss: contains equality theorems of the form [|p1,...|] ==> t==u
  1384    prover: how to solve premises in conditional rewrites and congruences
  1385 *)
  1386 
  1387 (*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***)
  1388 fun rewrite_cterm mode mss prover ct =
  1389   let val {sign, t, T, maxidx} = rep_cterm ct;
  1390       val (hyps,maxidxu,u) = bottomc (mode,prover,sign) mss ([],maxidx,t);
  1391       val prop = Logic.mk_equals(t,u)
  1392   in  Thm{sign= sign, hyps= hyps, maxidx= max[maxidx,maxidxu], prop= prop}
  1393   end
  1394 
  1395 end;
  1396