src/Pure/thm.ML
author nipkow
Fri Jan 14 08:09:07 1994 +0100 (1994-01-14)
changeset 225 76f60e6400e8
parent 222 5eb3020f7a03
child 229 4002c4cd450c
permissions -rw-r--r--
optimized net for matching of abstractions to speed up simplifier
     1 (*  Title: 	thm
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 The abstract types "theory" and "thm"
     7 *)
     8 
     9 signature THM = 
    10   sig
    11   structure Envir : ENVIR
    12   structure Sequence : SEQUENCE
    13   structure Sign : SIGN
    14   type meta_simpset
    15   type theory
    16   type thm
    17   exception THM of string * int * thm list
    18   exception THEORY of string * theory list
    19   exception SIMPLIFIER of string * thm
    20   val abstract_rule: string -> Sign.cterm -> thm -> thm
    21   val add_congs: meta_simpset * thm list -> meta_simpset
    22   val add_prems: meta_simpset * thm list -> meta_simpset
    23   val add_simps: meta_simpset * thm list -> meta_simpset
    24   val assume: Sign.cterm -> thm
    25   val assumption: int -> thm -> thm Sequence.seq   
    26   val axioms_of: theory -> (string * thm) list
    27   val beta_conversion: Sign.cterm -> thm   
    28   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq   
    29   val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
    30   val combination: thm -> thm -> thm   
    31   val concl_of: thm -> term   
    32   val del_simps: meta_simpset * thm list -> meta_simpset
    33   val dest_state: thm * int -> (term*term)list * term list * term * term
    34   val empty_mss: meta_simpset
    35   val eq_assumption: int -> thm -> thm   
    36   val equal_intr: thm -> thm -> thm
    37   val equal_elim: thm -> thm -> thm
    38   val extend_theory: theory -> string
    39 	-> (class * class list) list * sort
    40 	   * (string list * int)list
    41            * (string * indexname list * string) list
    42 	   * (string list * (sort list * class))list
    43 	   * (string list * string)list * Sign.Syntax.sext option
    44 	-> (string*string)list -> theory
    45   val extensional: thm -> thm   
    46   val flexflex_rule: thm -> thm Sequence.seq  
    47   val flexpair_def: thm 
    48   val forall_elim: Sign.cterm -> thm -> thm
    49   val forall_intr: Sign.cterm -> thm -> thm
    50   val freezeT: thm -> thm
    51   val get_axiom: theory -> string -> thm
    52   val implies_elim: thm -> thm -> thm
    53   val implies_intr: Sign.cterm -> thm -> thm
    54   val implies_intr_hyps: thm -> thm
    55   val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list 
    56                    -> thm -> thm
    57   val lift_rule: (thm * int) -> thm -> thm
    58   val merge_theories: theory * theory -> theory
    59   val mk_rews_of_mss: meta_simpset -> thm -> thm list
    60   val mss_of: thm list -> meta_simpset
    61   val nprems_of: thm -> int
    62   val parents_of: theory -> theory list
    63   val prems_of: thm -> term list
    64   val prems_of_mss: meta_simpset -> thm list
    65   val pure_thy: theory
    66   val reflexive: Sign.cterm -> thm 
    67   val rename_params_rule: string list * int -> thm -> thm
    68   val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
    69   val rewrite_cterm:
    70          bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
    71            -> Sign.cterm -> thm
    72   val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
    73   val sign_of: theory -> Sign.sg   
    74   val syn_of: theory -> Sign.Syntax.syntax
    75   val stamps_of_thm: thm -> string ref list
    76   val stamps_of_thy: theory -> string ref list
    77   val symmetric: thm -> thm   
    78   val tpairs_of: thm -> (term*term)list
    79   val trace_simp: bool ref
    80   val transitive: thm -> thm -> thm
    81   val trivial: Sign.cterm -> thm
    82   val varifyT: thm -> thm
    83   end;
    84 
    85 
    86 
    87 functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN
    88                       and Net:NET
    89                 sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)
    90         (*: THM*) = (* FIXME *)
    91 struct
    92 structure Sequence = Unify.Sequence;
    93 structure Envir = Unify.Envir;
    94 structure Sign = Unify.Sign;
    95 structure Type = Sign.Type;
    96 structure Syntax = Sign.Syntax;
    97 structure Symtab = Sign.Symtab;
    98 
    99 
   100 (*Meta-theorems*)
   101 datatype thm = Thm of
   102     {sign: Sign.sg,  maxidx: int,  hyps: term list,  prop: term};
   103 
   104 fun rep_thm (Thm x) = x;
   105 
   106 (*Errors involving theorems*)
   107 exception THM of string * int * thm list;
   108 
   109 (*maps object-rule to tpairs *)
   110 fun tpairs_of (Thm{prop,...}) = #1 (Logic.strip_flexpairs prop);
   111 
   112 (*maps object-rule to premises *)
   113 fun prems_of (Thm{prop,...}) =
   114     Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   115 
   116 (*counts premises in a rule*)
   117 fun nprems_of (Thm{prop,...}) =
   118     Logic.count_prems (Logic.skip_flexpairs prop, 0);
   119 
   120 (*maps object-rule to conclusion *)
   121 fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;
   122 
   123 (*Stamps associated with a signature*)
   124 val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
   125 
   126 (*Theories.  There is one pure theory.
   127   A theory can be extended.  Two theories can be merged.*)
   128 datatype theory =
   129     Pure of {sign: Sign.sg}
   130   | Extend of {sign: Sign.sg,  axioms: thm Symtab.table,  thy: theory}
   131   | Merge of {sign: Sign.sg,  thy1: theory,  thy2: theory};
   132 
   133 (*Errors involving theories*)
   134 exception THEORY of string * theory list;
   135 
   136 fun sign_of (Pure {sign}) = sign
   137   | sign_of (Extend {sign,...}) = sign
   138   | sign_of (Merge {sign,...}) = sign;
   139 
   140 val syn_of = #syn o Sign.rep_sg o sign_of;
   141 
   142 (*return the axioms of a theory and its ancestors*)
   143 fun axioms_of (Pure _) = []
   144   | axioms_of (Extend{axioms,thy,...}) = Symtab.alist_of axioms
   145   | axioms_of (Merge{thy1,thy2,...}) = axioms_of thy1  @  axioms_of thy2;
   146 
   147 (*return the immediate ancestors -- also distinguishes the kinds of theories*)
   148 fun parents_of (Pure _) = []
   149   | parents_of (Extend{thy,...}) = [thy]
   150   | parents_of (Merge{thy1,thy2,...}) = [thy1,thy2];
   151 
   152 
   153 (*Merge theories of two theorems.  Raise exception if incompatible.
   154   Prefers (via Sign.merge) the signature of th1.  *)
   155 fun merge_theories(th1,th2) =
   156   let val Thm{sign=sign1,...} = th1 and Thm{sign=sign2,...} = th2
   157   in  Sign.merge (sign1,sign2)  end
   158   handle TERM _ => raise THM("incompatible signatures", 0, [th1,th2]);
   159 
   160 (*Stamps associated with a theory*)
   161 val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
   162 
   163 
   164 (**** Primitive rules ****)
   165 
   166 (* discharge all assumptions t from ts *)
   167 val disch = gen_rem (op aconv);
   168 
   169 (*The assumption rule A|-A in a theory  *)
   170 fun assume ct : thm = 
   171   let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct
   172   in  if T<>propT then  
   173 	raise THM("assume: assumptions must have type prop", 0, [])
   174       else if maxidx <> ~1 then
   175 	raise THM("assume: assumptions may not contain scheme variables", 
   176 		  maxidx, [])
   177       else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop}
   178   end;
   179 
   180 (* Implication introduction  
   181 	      A |- B
   182 	      -------
   183 	      A ==> B    *)
   184 fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
   185   let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA
   186   in  if T<>propT then
   187 	raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   188       else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx], 
   189 	     hyps= disch(hyps,A),  prop= implies$A$prop}
   190       handle TERM _ =>
   191         raise THM("implies_intr: incompatible signatures", 0, [thB])
   192   end;
   193 
   194 (* Implication elimination
   195 	A ==> B       A
   196 	---------------
   197 		B      *)
   198 fun implies_elim thAB thA : thm =
   199     let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA
   200 	and Thm{sign, maxidx, hyps, prop,...} = thAB;
   201 	fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   202     in  case prop of
   203 	    imp$A$B => 
   204 		if imp=implies andalso  A aconv propA
   205 		then  Thm{sign= merge_theories(thAB,thA),
   206 			  maxidx= max[maxA,maxidx], 
   207 			  hyps= hypsA union hyps,  (*dups suppressed*)
   208 			  prop= B}
   209 		else err("major premise")
   210 	  | _ => err("major premise")
   211     end;
   212       
   213 (* Forall introduction.  The Free or Var x must not be free in the hypotheses.
   214      A
   215    ------
   216    !!x.A       *)
   217 fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
   218   let val x = Sign.term_of cx;
   219       fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   220 	                    prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   221   in  case x of
   222 	Free(a,T) => 
   223 	  if exists (apl(x, Logic.occs)) hyps 
   224 	  then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   225 	  else  result(a,T)
   226       | Var((a,_),T) => result(a,T)
   227       | _ => raise THM("forall_intr: not a variable", 0, [th])
   228   end;
   229 
   230 (* Forall elimination
   231 	      !!x.A
   232 	     --------
   233 	      A[t/x]     *)
   234 fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
   235   let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct
   236   in  case prop of
   237 	  Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   238 	    if T<>qary then
   239 		raise THM("forall_elim: type mismatch", 0, [th])
   240 	    else Thm{sign= Sign.merge(sign,signt), 
   241 		     maxidx= max[maxidx, maxt],
   242 		     hyps= hyps,  prop= betapply(A,t)}
   243 	| _ => raise THM("forall_elim: not quantified", 0, [th])
   244   end
   245   handle TERM _ =>
   246 	 raise THM("forall_elim: incompatible signatures", 0, [th]);
   247 
   248 
   249 (*** Equality ***)
   250 
   251 (*Definition of the relation =?= *)
   252 val flexpair_def =
   253   Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
   254       prop= Sign.term_of 
   255 	      (Sign.read_cterm Sign.pure 
   256 	         ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   257 
   258 (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   259 fun reflexive ct = 
   260   let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   261   in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
   262   end;
   263 
   264 (*The symmetry rule
   265     t==u
   266     ----
   267     u==t         *)
   268 fun symmetric (th as Thm{sign,hyps,prop,maxidx}) =
   269   case prop of
   270       (eq as Const("==",_)) $ t $ u =>
   271 	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
   272     | _ => raise THM("symmetric", 0, [th]);
   273 
   274 (*The transitive rule
   275     t1==u    u==t2
   276     ------------
   277         t1==t2      *)
   278 fun transitive th1 th2 =
   279   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   280       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   281       fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   282   in case (prop1,prop2) of
   283        ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   284 	  if not (u aconv u') then err"middle term"  else
   285 	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   286 		  maxidx= max[max1,max2], prop= eq$t1$t2}
   287      | _ =>  err"premises"
   288   end;
   289 
   290 (*Beta-conversion: maps (%(x)t)(u) to the theorem  (%(x)t)(u) == t[u/x]   *)
   291 fun beta_conversion ct = 
   292   let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   293   in  case t of
   294 	  Abs(_,_,bodt) $ u => 
   295 	    Thm{sign= sign,  hyps= [],  
   296 		maxidx= maxidx_of_term t, 
   297 		prop= Logic.mk_equals(t, subst_bounds([u],bodt))}
   298 	| _ =>  raise THM("beta_conversion: not a redex", 0, [])
   299   end;
   300 
   301 (*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
   302     f(x) == g(x)
   303     ------------
   304        f == g    *)
   305 fun extensional (th as Thm{sign,maxidx,hyps,prop}) =
   306   case prop of
   307     (Const("==",_)) $ (f$x) $ (g$y) =>
   308       let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
   309       in (if x<>y then err"different variables" else
   310           case y of
   311 		Free _ => 
   312 		  if exists (apl(y, Logic.occs)) (f::g::hyps) 
   313 		  then err"variable free in hyps or functions"    else  ()
   314 	      | Var _ => 
   315 		  if Logic.occs(y,f)  orelse  Logic.occs(y,g) 
   316 		  then err"variable free in functions"   else  ()
   317 	      | _ => err"not a variable");
   318 	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
   319 	      prop= Logic.mk_equals(f,g)} 
   320       end
   321  | _ =>  raise THM("extensional: premise", 0, [th]);
   322 
   323 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   324   The bound variable will be named "a" (since x will be something like x320)
   325           t == u
   326     ----------------
   327       %(x)t == %(x)u     *)
   328 fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
   329   let val x = Sign.term_of cx;
   330       val (t,u) = Logic.dest_equals prop  
   331 	    handle TERM _ =>
   332 		raise THM("abstract_rule: premise not an equality", 0, [th])
   333       fun result T =
   334             Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   335 	        prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   336 		  	              Abs(a, T, abstract_over (x,u)))}
   337   in  case x of
   338 	Free(_,T) => 
   339 	 if exists (apl(x, Logic.occs)) hyps 
   340 	 then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   341 	 else result T
   342       | Var(_,T) => result T
   343       | _ => raise THM("abstract_rule: not a variable", 0, [th])
   344   end;
   345 
   346 (*The combination rule
   347     f==g    t==u
   348     ------------
   349      f(t)==g(u)      *)
   350 fun combination th1 th2 =
   351   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   352       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2
   353   in  case (prop1,prop2)  of
   354        (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   355 	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   356 		  maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
   357      | _ =>  raise THM("combination: premises", 0, [th1,th2])
   358   end;
   359 
   360 
   361 (*The equal propositions rule
   362     A==B    A
   363     ---------
   364         B          *)
   365 fun equal_elim th1 th2 =
   366   let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   367       and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   368       fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   369   in  case prop1  of
   370        Const("==",_) $ A $ B =>
   371 	  if not (prop2 aconv A) then err"not equal"  else
   372 	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   373 		  maxidx= max[max1,max2], prop= B}
   374      | _ =>  err"major premise"
   375   end;
   376 
   377 
   378 (* Equality introduction
   379     A==>B    B==>A
   380     -------------
   381          A==B            *)
   382 fun equal_intr th1 th2 =
   383 let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   384     and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   385     fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   386 in case (prop1,prop2) of
   387      (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   388 	if A aconv A' andalso B aconv B'
   389 	then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   390 		 maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}
   391 	else err"not equal"
   392    | _ =>  err"premises"
   393 end;
   394 
   395 (**** Derived rules ****)
   396 
   397 (*Discharge all hypotheses (need not verify cterms)
   398   Repeated hypotheses are discharged only once;  fold cannot do this*)
   399 fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) =
   400       implies_intr_hyps
   401 	    (Thm{sign=sign,  maxidx=maxidx, 
   402 	         hyps= disch(As,A),  prop= implies$A$prop})
   403   | implies_intr_hyps th = th;
   404 
   405 (*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   406   Instantiates the theorem and deletes trivial tpairs. 
   407   Resulting sequence may contain multiple elements if the tpairs are
   408     not all flex-flex. *)
   409 fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) =
   410   let fun newthm env = 
   411 	  let val (tpairs,horn) = 
   412 			Logic.strip_flexpairs (Envir.norm_term env prop)
   413 	        (*Remove trivial tpairs, of the form t=t*)
   414 	      val distpairs = filter (not o op aconv) tpairs
   415 	      val newprop = Logic.list_flexpairs(distpairs, horn)
   416 	  in  Thm{sign= sign, hyps= hyps, 
   417 		  maxidx= maxidx_of_term newprop, prop= newprop}
   418 	  end;
   419       val (tpairs,_) = Logic.strip_flexpairs prop
   420   in Sequence.maps newthm
   421 	    (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
   422   end;
   423 
   424 (*Instantiation of Vars
   425 		      A
   426 	     --------------------
   427 	      A[t1/v1,....,tn/vn]     *)
   428 
   429 (*Check that all the terms are Vars and are distinct*)
   430 fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   431 
   432 (*For instantiate: process pair of cterms, merge theories*)
   433 fun add_ctpair ((ct,cu), (sign,tpairs)) =
   434   let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
   435       and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
   436   in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   437       else raise TYPE("add_ctpair", [T,U], [t,u])
   438   end;
   439 
   440 fun add_ctyp ((v,ctyp), (sign',vTs)) =
   441   let val {T,sign} = Sign.rep_ctyp ctyp
   442   in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   443 
   444 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   445   Instantiates distinct Vars by terms of same type.
   446   Normalizes the new theorem! *)
   447 fun instantiate (vcTs,ctpairs)  (th as Thm{sign,maxidx,hyps,prop}) = 
   448   let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
   449       val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
   450       val newprop = 
   451 	    Envir.norm_term (Envir.empty 0) 
   452 	      (subst_atomic tpairs 
   453 	       (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop))
   454       val newth = Thm{sign= newsign, hyps= hyps,
   455 		      maxidx= maxidx_of_term newprop, prop= newprop}
   456   in  if not(instl_ok(map #1 tpairs)) 
   457       then raise THM("instantiate: variables not distinct", 0, [th])
   458       else if not(null(findrep(map #1 vTs)))
   459       then raise THM("instantiate: type variables not distinct", 0, [th])
   460       else (*Check types of Vars for agreement*)
   461       case findrep (map (#1 o dest_Var) (term_vars newprop)) of
   462 	  ix::_ => raise THM("instantiate: conflicting types for variable " ^
   463 			     Syntax.string_of_vname ix ^ "\n", 0, [newth])
   464 	| [] => 
   465 	     case findrep (map #1 (term_tvars newprop)) of
   466 	     ix::_ => raise THM
   467 		    ("instantiate: conflicting sorts for type variable " ^
   468 		     Syntax.string_of_vname ix ^ "\n", 0, [newth])
   469         | [] => newth
   470   end
   471   handle TERM _ => 
   472            raise THM("instantiate: incompatible signatures",0,[th])
   473        | TYPE _ => raise THM("instantiate: type conflict", 0, [th]);
   474 
   475 (*The trivial implication A==>A, justified by assume and forall rules.
   476   A can contain Vars, not so for assume!   *)
   477 fun trivial ct : thm = 
   478   let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct
   479   in  if T<>propT then  
   480 	    raise THM("trivial: the term must have type prop", 0, [])
   481       else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   482   end;
   483 
   484 (* Replace all TFrees not in the hyps by new TVars *)
   485 fun varifyT(Thm{sign,maxidx,hyps,prop}) =
   486   let val tfrees = foldr add_term_tfree_names (hyps,[])
   487   in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps,
   488 	 prop= Type.varify(prop,tfrees)}
   489   end;
   490 
   491 (* Replace all TVars by new TFrees *)
   492 fun freezeT(Thm{sign,maxidx,hyps,prop}) =
   493   let val prop' = Type.freeze (K true) prop
   494   in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;
   495 
   496 
   497 (*** Inference rules for tactics ***)
   498 
   499 (*Destruct proof state into constraints, other goals, goal(i), rest *)
   500 fun dest_state (state as Thm{prop,...}, i) =
   501   let val (tpairs,horn) = Logic.strip_flexpairs prop
   502   in  case  Logic.strip_prems(i, [], horn) of
   503           (B::rBs, C) => (tpairs, rev rBs, B, C)
   504         | _ => raise THM("dest_state", i, [state])
   505   end
   506   handle TERM _ => raise THM("dest_state", i, [state]);
   507 
   508 (*Increment variables and parameters of rule as required for
   509   resolution with goal i of state. *)
   510 fun lift_rule (state, i) orule =
   511   let val Thm{prop=sprop,maxidx=smax,...} = state;
   512       val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
   513 	handle TERM _ => raise THM("lift_rule", i, [orule,state]);
   514       val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1);
   515       val (Thm{sign,maxidx,hyps,prop}) = orule
   516       val (tpairs,As,B) = Logic.strip_horn prop
   517   in  Thm{hyps=hyps, sign= merge_theories(state,orule),
   518 	  maxidx= maxidx+smax+1,
   519 	  prop= Logic.rule_of(map (pairself lift_abs) tpairs,
   520 			      map lift_all As,    lift_all B)}
   521   end;
   522 
   523 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   524 fun assumption i state =
   525   let val Thm{sign,maxidx,hyps,prop} = state;
   526       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   527       fun newth (env as Envir.Envir{maxidx,asol,iTs}, tpairs) =
   528 	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   529 	    case (Envir.alist_of_olist asol, iTs) of
   530 		(*avoid wasted normalizations*)
   531 	        ([],[]) => Logic.rule_of(tpairs, Bs, C)
   532 	      | _ => (*normalize the new rule fully*)
   533 		      Envir.norm_term env (Logic.rule_of(tpairs, Bs, C))};
   534       fun addprfs [] = Sequence.null
   535         | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   536              (Sequence.mapp newth
   537 	        (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 
   538 	        (addprfs apairs)))
   539   in  addprfs (Logic.assum_pairs Bi)  end;
   540 
   541 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
   542   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
   543 fun eq_assumption i state =
   544   let val Thm{sign,maxidx,hyps,prop} = state;
   545       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   546   in  if exists (op aconv) (Logic.assum_pairs Bi)
   547       then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
   548 	       prop=Logic.rule_of(tpairs, Bs, C)}
   549       else  raise THM("eq_assumption", 0, [state])
   550   end;
   551 
   552 
   553 (** User renaming of parameters in a subgoal **)
   554 
   555 (*Calls error rather than raising an exception because it is intended
   556   for top-level use -- exception handling would not make sense here.
   557   The names in cs, if distinct, are used for the innermost parameters;
   558    preceding parameters may be renamed to make all params distinct.*)
   559 fun rename_params_rule (cs, i) state =
   560   let val Thm{sign,maxidx,hyps,prop} = state
   561       val (tpairs, Bs, Bi, C) = dest_state(state,i)
   562       val iparams = map #1 (Logic.strip_params Bi)
   563       val short = length iparams - length cs
   564       val newnames = 
   565 	    if short<0 then error"More names than abstractions!"
   566 	    else variantlist(take (short,iparams), cs) @ cs
   567       val freenames = map (#1 o dest_Free) (term_frees prop)
   568       val newBi = Logic.list_rename_params (newnames, Bi)
   569   in  
   570   case findrep cs of
   571      c::_ => error ("Bound variables not distinct: " ^ c)
   572    | [] => (case cs inter freenames of
   573        a::_ => error ("Bound/Free variable clash: " ^ a)
   574      | [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   575 		    Logic.rule_of(tpairs, Bs@[newBi], C)})
   576   end;
   577 
   578 (*** Preservation of bound variable names ***)
   579 
   580 (*Scan a pair of terms; while they are similar, 
   581   accumulate corresponding bound vars in "al"*)
   582 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)
   583   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   584   | match_bvs(_,_,al) = al;
   585 
   586 (* strip abstractions created by parameters *)
   587 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   588 
   589 
   590 (* strip_apply f A(,B) strips off all assumptions/parameters from A 
   591    introduced by lifting over B, and applies f to remaining part of A*)
   592 fun strip_apply f =
   593   let fun strip(Const("==>",_)$ A1 $ B1,
   594 		Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
   595 	| strip((c as Const("all",_)) $ Abs(a,T,t1),
   596 		      Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
   597 	| strip(A,_) = f A
   598   in strip end;
   599 
   600 (*Use the alist to rename all bound variables and some unknowns in a term
   601   dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
   602   Preserves unknowns in tpairs and on lhs of dpairs. *)
   603 fun rename_bvs([],_,_,_) = I
   604   | rename_bvs(al,dpairs,tpairs,B) =
   605     let val vars = foldr add_term_vars 
   606 			(map fst dpairs @ map fst tpairs @ map snd tpairs, [])
   607 	(*unknowns appearing elsewhere be preserved!*)
   608 	val vids = map (#1 o #1 o dest_Var) vars;
   609 	fun rename(t as Var((x,i),T)) =
   610 		(case assoc(al,x) of
   611 		   Some(y) => if x mem vids orelse y mem vids then t
   612 			      else Var((y,i),T)
   613 		 | None=> t)
   614           | rename(Abs(x,T,t)) =
   615 	      Abs(case assoc(al,x) of Some(y) => y | None => x,
   616 		  T, rename t)
   617           | rename(f$t) = rename f $ rename t
   618           | rename(t) = t;
   619 	fun strip_ren Ai = strip_apply rename (Ai,B)
   620     in strip_ren end;
   621 
   622 (*Function to rename bounds/unknowns in the argument, lifted over B*)
   623 fun rename_bvars(dpairs, tpairs, B) =
   624 	rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
   625 
   626 
   627 (*** RESOLUTION ***)
   628 
   629 (*strip off pairs of assumptions/parameters in parallel -- they are
   630   identical because of lifting*)
   631 fun strip_assums2 (Const("==>", _) $ _ $ B1, 
   632 		   Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
   633   | strip_assums2 (Const("all",_)$Abs(a,T,t1),
   634 		   Const("all",_)$Abs(_,_,t2)) = 
   635       let val (B1,B2) = strip_assums2 (t1,t2)
   636       in  (Abs(a,T,B1), Abs(a,T,B2))  end
   637   | strip_assums2 BB = BB;
   638 
   639 
   640 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
   641   Unifies B with Bi, replacing subgoal i    (1 <= i <= n)  
   642   If match then forbid instantiations in proof state
   643   If lifted then shorten the dpair using strip_assums2.
   644   If eres_flg then simultaneously proves A1 by assumption.
   645   nsubgoal is the number of new subgoals (written m above). 
   646   Curried so that resolution calls dest_state only once.
   647 *)
   648 local open Sequence; exception Bicompose
   649 in
   650 fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
   651                         (eres_flg, orule, nsubgoal) =
   652  let val Thm{maxidx=smax, hyps=shyps, ...} = state
   653      and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule;
   654      val sign = merge_theories(state,orule);
   655      (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
   656      fun addth As ((env as Envir.Envir{maxidx,asol,iTs}, tpairs), thq) =
   657        let val minenv = case Envir.alist_of_olist asol of
   658 			  [] => ~1  |  ((_,i),_) :: _ => i;
   659 	   val minx = min (minenv :: map (fn ((_,i),_) => i) iTs);
   660 	   val normt = Envir.norm_term env;
   661 	   (*Perform minimal copying here by examining env*)
   662 	   val normp = if minx = ~1 then (tpairs, Bs@As, C) 
   663 		       else 
   664 		       let val ntps = map (pairself normt) tpairs
   665 		       in if minx>smax then (*no assignments in state*)
   666 			    (ntps, Bs @ map normt As, C)
   667 			  else if match then raise Bicompose
   668 			  else (*normalize the new rule fully*)
   669 			    (ntps, map normt (Bs @ As), normt C)
   670 		       end
   671 	   val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx,
   672 			prop= Logic.rule_of normp}
   673         in  cons(th, thq)  end  handle Bicompose => thq
   674      val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
   675      val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
   676        handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
   677      (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
   678      fun newAs(As0, n, dpairs, tpairs) =
   679        let val As1 = if !Logic.auto_rename orelse not lifted then As0
   680 		     else map (rename_bvars(dpairs,tpairs,B)) As0
   681        in (map (Logic.flatten_params n) As1)
   682 	  handle TERM _ =>
   683 	  raise THM("bicompose: 1st premise", 0, [orule])
   684        end;
   685      val env = Envir.empty(max[rmax,smax]);
   686      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
   687      val dpairs = BBi :: (rtpairs@stpairs);
   688      (*elim-resolution: try each assumption in turn.  Initially n=1*)
   689      fun tryasms (_, _, []) = null
   690        | tryasms (As, n, (t,u)::apairs) =
   691 	  (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
   692 	       None                   => tryasms (As, n+1, apairs)
   693 	     | cell as Some((_,tpairs),_) => 
   694 		   its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
   695 		       (seqof (fn()=> cell),
   696 		        seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
   697      fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
   698        | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
   699      (*ordinary resolution*)
   700      fun res(None) = null
   701        | res(cell as Some((_,tpairs),_)) = 
   702 	     its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
   703 	 	       (seqof (fn()=> cell), null)
   704  in  if eres_flg then eres(rev rAs)
   705      else res(pull(Unify.unifiers(sign, env, dpairs)))
   706  end;
   707 end;  (*open Sequence*)
   708 
   709 
   710 fun bicompose match arg i state =
   711     bicompose_aux match (state, dest_state(state,i), false) arg;
   712 
   713 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   714   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
   715 fun could_bires (Hs, B, eres_flg, rule) =
   716     let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
   717 	  | could_reshyp [] = false;  (*no premise -- illegal*)
   718     in  could_unify(concl_of rule, B) andalso 
   719 	(not eres_flg  orelse  could_reshyp (prems_of rule))
   720     end;
   721 
   722 (*Bi-resolution of a state with a list of (flag,rule) pairs.
   723   Puts the rule above:  rule/state.  Renames vars in the rules. *)
   724 fun biresolution match brules i state = 
   725     let val lift = lift_rule(state, i);
   726 	val (stpairs, Bs, Bi, C) = dest_state(state,i)
   727 	val B = Logic.strip_assums_concl Bi;
   728 	val Hs = Logic.strip_assums_hyp Bi;
   729 	val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
   730 	fun res [] = Sequence.null
   731 	  | res ((eres_flg, rule)::brules) = 
   732 	      if could_bires (Hs, B, eres_flg, rule)
   733 	      then Sequence.seqof (*delay processing remainder til needed*)
   734 	          (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
   735 			       res brules))
   736 	      else res brules
   737     in  Sequence.flats (res brules)  end;
   738 
   739 
   740 (**** THEORIES ****)
   741 
   742 val pure_thy = Pure{sign = Sign.pure};
   743 
   744 (*Look up the named axiom in the theory*)
   745 fun get_axiom thy axname =
   746     let fun get (Pure _) = raise Match
   747 	  | get (Extend{axioms,thy,...}) =
   748 	     (case Symtab.lookup(axioms,axname) of
   749 		  Some th => th
   750 		| None => get thy)
   751  	 | get (Merge{thy1,thy2,...}) = 
   752 		get thy1  handle Match => get thy2
   753     in  get thy
   754 	handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy])
   755     end;
   756 
   757 (*Converts Frees to Vars: axioms can be written without question marks*)
   758 fun prepare_axiom sign sP =
   759     Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));
   760 
   761 (*Read an axiom for a new theory*)
   762 fun read_ax sign (a, sP) : string*thm =
   763   let val prop = prepare_axiom sign sP
   764   in  (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop}) 
   765   end
   766   handle ERROR =>
   767 	error("extend_theory: The error above occurred in axiom " ^ a);
   768 
   769 fun mk_axioms sign axpairs =
   770 	Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null)
   771 	handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a);
   772 
   773 (*Extension of a theory with given classes, types, constants and syntax.
   774   Reads the axioms from strings: axpairs have the form (axname, axiom). *)
   775 fun extend_theory thy thyname ext axpairs =
   776   let val sign = Sign.extend (sign_of thy) thyname ext;
   777       val axioms= mk_axioms sign axpairs
   778   in  Extend{sign=sign, axioms= axioms, thy = thy}  end;
   779 
   780 (*The union of two theories*)
   781 fun merge_theories (thy1,thy2) =
   782     Merge{sign = Sign.merge(sign_of thy1, sign_of thy2),
   783 	  thy1 = thy1, thy2 = thy2};
   784 
   785 
   786 (*** Meta simp sets ***)
   787 
   788 type rrule = {thm:thm, lhs:term};
   789 datatype meta_simpset =
   790   Mss of {net:rrule Net.net, congs:(string * rrule)list, primes:string,
   791           prems: thm list, mk_rews: thm -> thm list};
   792 
   793 (*A "mss" contains data needed during conversion:
   794   net: discrimination net of rewrite rules
   795   congs: association list of congruence rules
   796   primes: offset for generating unique new names
   797           for rewriting under lambda abstractions
   798   mk_rews: used when local assumptions are added
   799 *)
   800 
   801 val empty_mss = Mss{net= Net.empty, congs= [], primes="", prems= [],
   802                     mk_rews = K[]};
   803 
   804 exception SIMPLIFIER of string * thm;
   805 
   806 fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
   807 
   808 val trace_simp = ref false;
   809 
   810 fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
   811 
   812 fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
   813 
   814 (*simple test for looping rewrite*)
   815 fun loops sign prems (lhs,rhs) =
   816   null(prems) andalso
   817   Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs);
   818 
   819 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
   820   let val prems = Logic.strip_imp_prems prop
   821       val concl = Pattern.eta_contract (Logic.strip_imp_concl prop)
   822       val (lhs,rhs) = Logic.dest_equals concl handle TERM _ =>
   823                       raise SIMPLIFIER("Rewrite rule not a meta-equality",thm)
   824   in if loops sign prems (lhs,rhs)
   825      then (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
   826      else Some{thm=thm,lhs=lhs}
   827   end;
   828 
   829 local
   830  fun eq({thm=Thm{prop=p1,...},...}:rrule,
   831         {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
   832 in
   833 
   834 fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews},
   835              thm as Thm{sign,prop,...}) =
   836   case mk_rrule thm of
   837     None => mss
   838   | Some(rrule as {lhs,...}) =>
   839       (trace_thm "Adding rewrite rule:" thm;
   840        Mss{net= (Net.insert_term((lhs,rrule),net,eq)
   841                  handle Net.INSERT =>
   842                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
   843                    net)),
   844            congs=congs, primes=primes, prems=prems,mk_rews=mk_rews});
   845 
   846 fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews},
   847              thm as Thm{sign,prop,...}) =
   848   case mk_rrule thm of
   849     None => mss
   850   | Some(rrule as {lhs,...}) =>
   851       Mss{net= (Net.delete_term((lhs,rrule),net,eq)
   852                 handle Net.INSERT =>
   853                  (prtm "Warning: rewrite rule not in simpset" sign prop;
   854                   net)),
   855              congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}
   856 
   857 end;
   858 
   859 val add_simps = foldl add_simp;
   860 val del_simps = foldl del_simp;
   861 
   862 fun mss_of thms = add_simps(empty_mss,thms);
   863 
   864 fun add_cong(Mss{net,congs,primes,prems,mk_rews},thm) =
   865   let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ =>
   866                     raise SIMPLIFIER("Congruence not a meta-equality",thm)
   867       val lhs = Pattern.eta_contract lhs
   868       val (a,_) = dest_Const (head_of lhs) handle TERM _ =>
   869                   raise SIMPLIFIER("Congruence must start with a constant",thm)
   870   in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, primes=primes,
   871          prems=prems, mk_rews=mk_rews}
   872   end;
   873 
   874 val (op add_congs) = foldl add_cong;
   875 
   876 fun add_prems(Mss{net,congs,primes,prems,mk_rews},thms) =
   877   Mss{net=net, congs=congs, primes=primes, prems=thms@prems, mk_rews=mk_rews};
   878 
   879 fun prems_of_mss(Mss{prems,...}) = prems;
   880 
   881 fun set_mk_rews(Mss{net,congs,primes,prems,...},mk_rews) =
   882   Mss{net=net, congs=congs, primes=primes, prems=prems, mk_rews=mk_rews};
   883 fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews;
   884 
   885 
   886 (*** Meta-level rewriting 
   887      uses conversions, omitting proofs for efficiency.  See
   888 	L C Paulson, A higher-order implementation of rewriting,
   889 	Science of Computer Programming 3 (1983), pages 119-149. ***)
   890 
   891 type prover = meta_simpset -> thm -> thm option;
   892 type termrec = (Sign.sg * term list) * term;
   893 type conv = meta_simpset -> termrec -> termrec;
   894 
   895 fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
   896   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)
   897       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
   898   in case prop of
   899        Const("==",_) $ lhs $ rhs =>
   900          if (lhs = lhs0) orelse
   901             (lhs aconv (Envir.norm_term (Envir.empty 0) lhs0))
   902          then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs))
   903          else err()
   904      | _ => err()
   905   end;
   906 
   907 (*Conversion to apply the meta simpset to a term*)
   908 fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) =
   909   let val t = Pattern.eta_contract t;
   910       fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} =
   911 	let val unit = if Sign.subsig(sign,signt) then ()
   912                   else (writeln"Warning: rewrite rule from different theory";
   913                         raise Pattern.MATCH)
   914             val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t)
   915             val prop' = subst_vars insts prop;
   916             val hyps' = hyps union hypst;
   917             val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx}
   918         in if nprems_of thm' = 0
   919            then let val (_,rhs) = Logic.dest_equals prop'
   920                 in trace_thm "Rewriting:" thm'; Some(hyps',rhs) end
   921            else (trace_thm "Trying to rewrite:" thm';
   922                  case prover mss thm' of
   923                    None       => (trace_thm "FAILED" thm'; None)
   924                  | Some(thm2) => check_conv(thm2,prop'))
   925         end
   926 
   927       fun rews [] = None
   928         | rews (rrule::rrules) =
   929             let val opt = rew rrule handle Pattern.MATCH => None
   930             in case opt of None => rews rrules | some => some end;
   931 
   932   in case t of
   933        Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body))
   934      | _                 => rews(Net.match_term net t)
   935   end;
   936 
   937 (*Conversion to apply a congruence rule to a term*)
   938 fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) =
   939   let val Thm{sign,hyps,maxidx,prop,...} = cong
   940       val unit = if Sign.subsig(sign,signt) then ()
   941                  else error("Congruence rule from different theory")
   942       val tsig = #tsig(Sign.rep_sg signt)
   943       val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH =>
   944                   error("Congruence rule did not match")
   945       val prop' = subst_vars insts prop;
   946       val thm' = Thm{sign=signt, hyps=hyps union hypst,
   947                      prop=prop', maxidx=maxidx}
   948       val unit = trace_thm "Applying congruence rule" thm';
   949       fun err() = error("Failed congruence proof!")
   950 
   951   in case prover thm' of
   952        None => err()
   953      | Some(thm2) => (case check_conv(thm2,prop') of
   954                         None => err() | Some(x) => x)
   955   end;
   956 
   957 
   958 fun bottomc ((simprem,useprem),prover,sign) =
   959   let fun botc mss trec = let val trec1 = subc mss trec
   960                           in case rewritec (prover,sign) mss trec1 of
   961                                None => trec1
   962                              | Some(trec2) => botc mss trec2
   963                           end
   964 
   965       and subc (mss as Mss{net,congs,primes,prems,mk_rews})
   966                (trec as (hyps,t)) =
   967         (case t of
   968             Abs(a,T,t) =>
   969               let val v = Free(".subc." ^ primes,T)
   970                   val mss' = Mss{net=net, congs=congs, primes=primes^"'",
   971                                  prems=prems,mk_rews=mk_rews}
   972                   val (hyps',t') = botc mss' (hyps,subst_bounds([v],t))
   973               in  (hyps', Abs(a, T, abstract_over(v,t')))  end
   974           | t$u => (case t of
   975               Const("==>",_)$s  => impc(hyps,s,u,mss)
   976             | Abs(_,_,body)     => subc mss (hyps,subst_bounds([u], body))
   977             | _                 =>
   978                 let fun appc() = let val (hyps1,t1) = botc mss (hyps,t)
   979                                      val (hyps2,u1) = botc mss (hyps1,u)
   980                                  in (hyps2,t1$u1) end
   981                     val (h,ts) = strip_comb t
   982                 in case h of
   983                      Const(a,_) =>
   984                        (case assoc(congs,a) of
   985                           None => appc()
   986                         | Some(cong) => congc (prover mss,sign) cong trec)
   987                    | _ => appc()
   988                 end)
   989           | _ => trec)
   990 
   991       and impc(hyps,s,u,mss as Mss{mk_rews,...}) =
   992         let val (hyps1,s') = if simprem then botc mss (hyps,s) else (hyps,s)
   993             val mss' =
   994               if not useprem orelse maxidx_of_term s' <> ~1 then mss
   995               else let val thm = Thm{sign=sign,hyps=[s'],prop=s',maxidx= ~1}
   996                    in add_simps(add_prems(mss,[thm]), mk_rews thm) end
   997             val (hyps2,u') = botc mss' (hyps1,u)
   998             val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s'
   999         in (hyps2', Logic.mk_implies(s',u')) end
  1000 
  1001   in botc end;
  1002 
  1003 
  1004 (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
  1005 (* Parameters:
  1006    mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
  1007    mss: contains equality theorems of the form [|p1,...|] ==> t==u
  1008    prover: how to solve premises in conditional rewrites and congruences
  1009 *)
  1010 
  1011 (*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
  1012 fun rewrite_cterm mode mss prover ct =
  1013   let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
  1014       val (hyps,u) = bottomc (mode,prover,sign) mss ([],t);
  1015       val prop = Logic.mk_equals(t,u)
  1016   in  Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}
  1017   end
  1018 
  1019 end;