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