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