src/Pure/thm.ML
changeset 0 a5a9c433f639
child 87 c378e56d4a4b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/thm.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,990 @@
     1.4 +(*  Title: 	thm
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +The abstract types "theory" and "thm"
    1.10 +*)
    1.11 +
    1.12 +signature THM = 
    1.13 +  sig
    1.14 +  structure Envir : ENVIR
    1.15 +  structure Sequence : SEQUENCE
    1.16 +  structure Sign : SIGN
    1.17 +  type meta_simpset
    1.18 +  type theory
    1.19 +  type thm
    1.20 +  exception THM of string * int * thm list
    1.21 +  exception THEORY of string * theory list
    1.22 +  exception SIMPLIFIER of string * thm
    1.23 +  val abstract_rule: string -> Sign.cterm -> thm -> thm
    1.24 +  val add_congs: meta_simpset * thm list -> meta_simpset
    1.25 +  val add_prems: meta_simpset * thm list -> meta_simpset
    1.26 +  val add_simps: meta_simpset * thm list -> meta_simpset
    1.27 +  val assume: Sign.cterm -> thm
    1.28 +  val assumption: int -> thm -> thm Sequence.seq   
    1.29 +  val axioms_of: theory -> (string * thm) list
    1.30 +  val beta_conversion: Sign.cterm -> thm   
    1.31 +  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Sequence.seq   
    1.32 +  val biresolution: bool -> (bool*thm)list -> int -> thm -> thm Sequence.seq   
    1.33 +  val combination: thm -> thm -> thm   
    1.34 +  val concl_of: thm -> term   
    1.35 +  val dest_state: thm * int -> (term*term)list * term list * term * term
    1.36 +  val empty_mss: meta_simpset
    1.37 +  val eq_assumption: int -> thm -> thm   
    1.38 +  val equal_intr: thm -> thm -> thm
    1.39 +  val equal_elim: thm -> thm -> thm
    1.40 +  val extend_theory: theory -> string
    1.41 +	-> (class * class list) list * sort
    1.42 +	   * (string list * int)list
    1.43 +	   * (string list * (sort list * class))list
    1.44 +	   * (string list * string)list * Sign.Syntax.sext option
    1.45 +	-> (string*string)list -> theory
    1.46 +  val extensional: thm -> thm   
    1.47 +  val flexflex_rule: thm -> thm Sequence.seq  
    1.48 +  val flexpair_def: thm 
    1.49 +  val forall_elim: Sign.cterm -> thm -> thm
    1.50 +  val forall_intr: Sign.cterm -> thm -> thm
    1.51 +  val freezeT: thm -> thm
    1.52 +  val get_axiom: theory -> string -> thm
    1.53 +  val implies_elim: thm -> thm -> thm
    1.54 +  val implies_intr: Sign.cterm -> thm -> thm
    1.55 +  val implies_intr_hyps: thm -> thm
    1.56 +  val instantiate: (indexname*Sign.ctyp)list * (Sign.cterm*Sign.cterm)list 
    1.57 +                   -> thm -> thm
    1.58 +  val lift_rule: (thm * int) -> thm -> thm
    1.59 +  val merge_theories: theory * theory -> theory
    1.60 +  val mk_rews_of_mss: meta_simpset -> thm -> thm list
    1.61 +  val mss_of: thm list -> meta_simpset
    1.62 +  val nprems_of: thm -> int
    1.63 +  val parents_of: theory -> theory list
    1.64 +  val prems_of: thm -> term list
    1.65 +  val prems_of_mss: meta_simpset -> thm list
    1.66 +  val pure_thy: theory
    1.67 +  val reflexive: Sign.cterm -> thm 
    1.68 +  val rename_params_rule: string list * int -> thm -> thm
    1.69 +  val rep_thm: thm -> {prop: term, hyps: term list, maxidx: int, sign: Sign.sg}
    1.70 +  val rewrite_cterm: meta_simpset -> (meta_simpset -> thm -> thm option)
    1.71 +                     -> Sign.cterm -> thm
    1.72 +  val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
    1.73 +  val sign_of: theory -> Sign.sg   
    1.74 +  val syn_of: theory -> Sign.Syntax.syntax
    1.75 +  val stamps_of_thm: thm -> string ref list
    1.76 +  val stamps_of_thy: theory -> string ref list
    1.77 +  val symmetric: thm -> thm   
    1.78 +  val tpairs_of: thm -> (term*term)list
    1.79 +  val trace_simp: bool ref
    1.80 +  val transitive: thm -> thm -> thm
    1.81 +  val trivial: Sign.cterm -> thm
    1.82 +  val varifyT: thm -> thm
    1.83 +  end;
    1.84 +
    1.85 +
    1.86 +
    1.87 +functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern:PATTERN
    1.88 +                      and Net:NET
    1.89 +                sharing type Pattern.type_sig = Unify.Sign.Type.type_sig)
    1.90 +        : THM = 
    1.91 +struct
    1.92 +structure Sequence = Unify.Sequence;
    1.93 +structure Envir = Unify.Envir;
    1.94 +structure Sign = Unify.Sign;
    1.95 +structure Type = Sign.Type;
    1.96 +structure Syntax = Sign.Syntax;
    1.97 +structure Symtab = Sign.Symtab;
    1.98 +
    1.99 +
   1.100 +(*Meta-theorems*)
   1.101 +datatype thm = Thm of
   1.102 +    {sign: Sign.sg,  maxidx: int,  hyps: term list,  prop: term};
   1.103 +
   1.104 +fun rep_thm (Thm x) = x;
   1.105 +
   1.106 +(*Errors involving theorems*)
   1.107 +exception THM of string * int * thm list;
   1.108 +
   1.109 +(*maps object-rule to tpairs *)
   1.110 +fun tpairs_of (Thm{prop,...}) = #1 (Logic.strip_flexpairs prop);
   1.111 +
   1.112 +(*maps object-rule to premises *)
   1.113 +fun prems_of (Thm{prop,...}) =
   1.114 +    Logic.strip_imp_prems (Logic.skip_flexpairs prop);
   1.115 +
   1.116 +(*counts premises in a rule*)
   1.117 +fun nprems_of (Thm{prop,...}) =
   1.118 +    Logic.count_prems (Logic.skip_flexpairs prop, 0);
   1.119 +
   1.120 +(*maps object-rule to conclusion *)
   1.121 +fun concl_of (Thm{prop,...}) = Logic.strip_imp_concl prop;
   1.122 +
   1.123 +(*Stamps associated with a signature*)
   1.124 +val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
   1.125 +
   1.126 +(*Theories.  There is one pure theory.
   1.127 +  A theory can be extended.  Two theories can be merged.*)
   1.128 +datatype theory =
   1.129 +    Pure of {sign: Sign.sg}
   1.130 +  | Extend of {sign: Sign.sg,  axioms: thm Symtab.table,  thy: theory}
   1.131 +  | Merge of {sign: Sign.sg,  thy1: theory,  thy2: theory};
   1.132 +
   1.133 +(*Errors involving theories*)
   1.134 +exception THEORY of string * theory list;
   1.135 +
   1.136 +fun sign_of (Pure {sign}) = sign
   1.137 +  | sign_of (Extend {sign,...}) = sign
   1.138 +  | sign_of (Merge {sign,...}) = sign;
   1.139 +
   1.140 +val syn_of = #syn o Sign.rep_sg o sign_of;
   1.141 +
   1.142 +(*return the axioms of a theory and its ancestors*)
   1.143 +fun axioms_of (Pure _) = []
   1.144 +  | axioms_of (Extend{axioms,thy,...}) = Symtab.alist_of axioms
   1.145 +  | axioms_of (Merge{thy1,thy2,...}) = axioms_of thy1  @  axioms_of thy2;
   1.146 +
   1.147 +(*return the immediate ancestors -- also distinguishes the kinds of theories*)
   1.148 +fun parents_of (Pure _) = []
   1.149 +  | parents_of (Extend{thy,...}) = [thy]
   1.150 +  | parents_of (Merge{thy1,thy2,...}) = [thy1,thy2];
   1.151 +
   1.152 +
   1.153 +(*Merge theories of two theorems.  Raise exception if incompatible.
   1.154 +  Prefers (via Sign.merge) the signature of th1.  *)
   1.155 +fun merge_theories(th1,th2) =
   1.156 +  let val Thm{sign=sign1,...} = th1 and Thm{sign=sign2,...} = th2
   1.157 +  in  Sign.merge (sign1,sign2)  end
   1.158 +  handle TERM _ => raise THM("incompatible signatures", 0, [th1,th2]);
   1.159 +
   1.160 +(*Stamps associated with a theory*)
   1.161 +val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;
   1.162 +
   1.163 +
   1.164 +(**** Primitive rules ****)
   1.165 +
   1.166 +(* discharge all assumptions t from ts *)
   1.167 +val disch = gen_rem (op aconv);
   1.168 +
   1.169 +(*The assumption rule A|-A in a theory  *)
   1.170 +fun assume ct : thm = 
   1.171 +  let val {sign, t=prop, T, maxidx} = Sign.rep_cterm ct
   1.172 +  in  if T<>propT then  
   1.173 +	raise THM("assume: assumptions must have type prop", 0, [])
   1.174 +      else if maxidx <> ~1 then
   1.175 +	raise THM("assume: assumptions may not contain scheme variables", 
   1.176 +		  maxidx, [])
   1.177 +      else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop}
   1.178 +  end;
   1.179 +
   1.180 +(* Implication introduction  
   1.181 +	      A |- B
   1.182 +	      -------
   1.183 +	      A ==> B    *)
   1.184 +fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop}) : thm =
   1.185 +  let val {sign=signA, t=A, T, maxidx=maxidxA} = Sign.rep_cterm cA
   1.186 +  in  if T<>propT then
   1.187 +	raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   1.188 +      else Thm{sign= Sign.merge (sign,signA),  maxidx= max[maxidxA, maxidx], 
   1.189 +	     hyps= disch(hyps,A),  prop= implies$A$prop}
   1.190 +      handle TERM _ =>
   1.191 +        raise THM("implies_intr: incompatible signatures", 0, [thB])
   1.192 +  end;
   1.193 +
   1.194 +(* Implication elimination
   1.195 +	A ==> B       A
   1.196 +	---------------
   1.197 +		B      *)
   1.198 +fun implies_elim thAB thA : thm =
   1.199 +    let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA
   1.200 +	and Thm{sign, maxidx, hyps, prop,...} = thAB;
   1.201 +	fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
   1.202 +    in  case prop of
   1.203 +	    imp$A$B => 
   1.204 +		if imp=implies andalso  A aconv propA
   1.205 +		then  Thm{sign= merge_theories(thAB,thA),
   1.206 +			  maxidx= max[maxA,maxidx], 
   1.207 +			  hyps= hypsA union hyps,  (*dups suppressed*)
   1.208 +			  prop= B}
   1.209 +		else err("major premise")
   1.210 +	  | _ => err("major premise")
   1.211 +    end;
   1.212 +      
   1.213 +(* Forall introduction.  The Free or Var x must not be free in the hypotheses.
   1.214 +     A
   1.215 +   ------
   1.216 +   !!x.A       *)
   1.217 +fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop}) =
   1.218 +  let val x = Sign.term_of cx;
   1.219 +      fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   1.220 +	                    prop= all(T) $ Abs(a, T, abstract_over (x,prop))}
   1.221 +  in  case x of
   1.222 +	Free(a,T) => 
   1.223 +	  if exists (apl(x, Logic.occs)) hyps 
   1.224 +	  then  raise THM("forall_intr: variable free in assumptions", 0, [th])
   1.225 +	  else  result(a,T)
   1.226 +      | Var((a,_),T) => result(a,T)
   1.227 +      | _ => raise THM("forall_intr: not a variable", 0, [th])
   1.228 +  end;
   1.229 +
   1.230 +(* Forall elimination
   1.231 +	      !!x.A
   1.232 +	     --------
   1.233 +	      A[t/x]     *)
   1.234 +fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop}) : thm =
   1.235 +  let val {sign=signt, t, T, maxidx=maxt} = Sign.rep_cterm ct
   1.236 +  in  case prop of
   1.237 +	  Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   1.238 +	    if T<>qary then
   1.239 +		raise THM("forall_elim: type mismatch", 0, [th])
   1.240 +	    else Thm{sign= Sign.merge(sign,signt), 
   1.241 +		     maxidx= max[maxidx, maxt],
   1.242 +		     hyps= hyps,  prop= betapply(A,t)}
   1.243 +	| _ => raise THM("forall_elim: not quantified", 0, [th])
   1.244 +  end
   1.245 +  handle TERM _ =>
   1.246 +	 raise THM("forall_elim: incompatible signatures", 0, [th]);
   1.247 +
   1.248 +
   1.249 +(*** Equality ***)
   1.250 +
   1.251 +(*Definition of the relation =?= *)
   1.252 +val flexpair_def =
   1.253 +  Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
   1.254 +      prop= Sign.term_of 
   1.255 +	      (Sign.read_cterm Sign.pure 
   1.256 +	         ("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))};
   1.257 +
   1.258 +(*The reflexivity rule: maps  t   to the theorem   t==t   *)
   1.259 +fun reflexive ct = 
   1.260 +  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   1.261 +  in  Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)}
   1.262 +  end;
   1.263 +
   1.264 +(*The symmetry rule
   1.265 +    t==u
   1.266 +    ----
   1.267 +    u==t         *)
   1.268 +fun symmetric (th as Thm{sign,hyps,prop,maxidx}) =
   1.269 +  case prop of
   1.270 +      (eq as Const("==",_)) $ t $ u =>
   1.271 +	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
   1.272 +    | _ => raise THM("symmetric", 0, [th]);
   1.273 +
   1.274 +(*The transitive rule
   1.275 +    t1==u    u==t2
   1.276 +    ------------
   1.277 +        t1==t2      *)
   1.278 +fun transitive th1 th2 =
   1.279 +  let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   1.280 +      and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   1.281 +      fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   1.282 +  in case (prop1,prop2) of
   1.283 +       ((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   1.284 +	  if not (u aconv u') then err"middle term"  else
   1.285 +	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   1.286 +		  maxidx= max[max1,max2], prop= eq$t1$t2}
   1.287 +     | _ =>  err"premises"
   1.288 +  end;
   1.289 +
   1.290 +(*Beta-conversion: maps (%(x)t)(u) to the theorem  (%(x)t)(u) == t[u/x]   *)
   1.291 +fun beta_conversion ct = 
   1.292 +  let val {sign, t, T, maxidx} = Sign.rep_cterm ct
   1.293 +  in  case t of
   1.294 +	  Abs(_,_,bodt) $ u => 
   1.295 +	    Thm{sign= sign,  hyps= [],  
   1.296 +		maxidx= maxidx_of_term t, 
   1.297 +		prop= Logic.mk_equals(t, subst_bounds([u],bodt))}
   1.298 +	| _ =>  raise THM("beta_conversion: not a redex", 0, [])
   1.299 +  end;
   1.300 +
   1.301 +(*The extensionality rule   (proviso: x not free in f, g, or hypotheses)
   1.302 +    f(x) == g(x)
   1.303 +    ------------
   1.304 +       f == g    *)
   1.305 +fun extensional (th as Thm{sign,maxidx,hyps,prop}) =
   1.306 +  case prop of
   1.307 +    (Const("==",_)) $ (f$x) $ (g$y) =>
   1.308 +      let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
   1.309 +      in (if x<>y then err"different variables" else
   1.310 +          case y of
   1.311 +		Free _ => 
   1.312 +		  if exists (apl(y, Logic.occs)) (f::g::hyps) 
   1.313 +		  then err"variable free in hyps or functions"    else  ()
   1.314 +	      | Var _ => 
   1.315 +		  if Logic.occs(y,f)  orelse  Logic.occs(y,g) 
   1.316 +		  then err"variable free in functions"   else  ()
   1.317 +	      | _ => err"not a variable");
   1.318 +	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
   1.319 +	      prop= Logic.mk_equals(f,g)} 
   1.320 +      end
   1.321 + | _ =>  raise THM("extensional: premise", 0, [th]);
   1.322 +
   1.323 +(*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   1.324 +  The bound variable will be named "a" (since x will be something like x320)
   1.325 +          t == u
   1.326 +    ----------------
   1.327 +      %(x)t == %(x)u     *)
   1.328 +fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop}) =
   1.329 +  let val x = Sign.term_of cx;
   1.330 +      val (t,u) = Logic.dest_equals prop  
   1.331 +	    handle TERM _ =>
   1.332 +		raise THM("abstract_rule: premise not an equality", 0, [th])
   1.333 +      fun result T =
   1.334 +            Thm{sign= sign, maxidx= maxidx, hyps= hyps,
   1.335 +	        prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   1.336 +		  	              Abs(a, T, abstract_over (x,u)))}
   1.337 +  in  case x of
   1.338 +	Free(_,T) => 
   1.339 +	 if exists (apl(x, Logic.occs)) hyps 
   1.340 +	 then raise THM("abstract_rule: variable free in assumptions", 0, [th])
   1.341 +	 else result T
   1.342 +      | Var(_,T) => result T
   1.343 +      | _ => raise THM("abstract_rule: not a variable", 0, [th])
   1.344 +  end;
   1.345 +
   1.346 +(*The combination rule
   1.347 +    f==g    t==u
   1.348 +    ------------
   1.349 +     f(t)==g(u)      *)
   1.350 +fun combination th1 th2 =
   1.351 +  let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   1.352 +      and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2
   1.353 +  in  case (prop1,prop2)  of
   1.354 +       (Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
   1.355 +	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   1.356 +		  maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)}
   1.357 +     | _ =>  raise THM("combination: premises", 0, [th1,th2])
   1.358 +  end;
   1.359 +
   1.360 +
   1.361 +(*The equal propositions rule
   1.362 +    A==B    A
   1.363 +    ---------
   1.364 +        B          *)
   1.365 +fun equal_elim th1 th2 =
   1.366 +  let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   1.367 +      and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   1.368 +      fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2])
   1.369 +  in  case prop1  of
   1.370 +       Const("==",_) $ A $ B =>
   1.371 +	  if not (prop2 aconv A) then err"not equal"  else
   1.372 +	      Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   1.373 +		  maxidx= max[max1,max2], prop= B}
   1.374 +     | _ =>  err"major premise"
   1.375 +  end;
   1.376 +
   1.377 +
   1.378 +(* Equality introduction
   1.379 +    A==>B    B==>A
   1.380 +    -------------
   1.381 +         A==B            *)
   1.382 +fun equal_intr th1 th2 =
   1.383 +let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1
   1.384 +    and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2;
   1.385 +    fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   1.386 +in case (prop1,prop2) of
   1.387 +     (Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A')  =>
   1.388 +	if A aconv A' andalso B aconv B'
   1.389 +	then Thm{sign= merge_theories(th1,th2), hyps= hyps1 union hyps2, 
   1.390 +		 maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)}
   1.391 +	else err"not equal"
   1.392 +   | _ =>  err"premises"
   1.393 +end;
   1.394 +
   1.395 +(**** Derived rules ****)
   1.396 +
   1.397 +(*Discharge all hypotheses (need not verify cterms)
   1.398 +  Repeated hypotheses are discharged only once;  fold cannot do this*)
   1.399 +fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) =
   1.400 +      implies_intr_hyps
   1.401 +	    (Thm{sign=sign,  maxidx=maxidx, 
   1.402 +	         hyps= disch(As,A),  prop= implies$A$prop})
   1.403 +  | implies_intr_hyps th = th;
   1.404 +
   1.405 +(*Smash" unifies the list of term pairs leaving no flex-flex pairs.
   1.406 +  Instantiates the theorem and deletes trivial tpairs. 
   1.407 +  Resulting sequence may contain multiple elements if the tpairs are
   1.408 +    not all flex-flex. *)
   1.409 +fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) =
   1.410 +  let fun newthm env = 
   1.411 +	  let val (tpairs,horn) = 
   1.412 +			Logic.strip_flexpairs (Envir.norm_term env prop)
   1.413 +	        (*Remove trivial tpairs, of the form t=t*)
   1.414 +	      val distpairs = filter (not o op aconv) tpairs
   1.415 +	      val newprop = Logic.list_flexpairs(distpairs, horn)
   1.416 +	  in  Thm{sign= sign, hyps= hyps, 
   1.417 +		  maxidx= maxidx_of_term newprop, prop= newprop}
   1.418 +	  end;
   1.419 +      val (tpairs,_) = Logic.strip_flexpairs prop
   1.420 +  in Sequence.maps newthm
   1.421 +	    (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
   1.422 +  end;
   1.423 +
   1.424 +
   1.425 +(*Instantiation of Vars
   1.426 +		      A
   1.427 +	     --------------------
   1.428 +	      A[t1/v1,....,tn/vn]     *)
   1.429 +
   1.430 +(*Check that all the terms are Vars and are distinct*)
   1.431 +fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   1.432 +
   1.433 +(*For instantiate: process pair of cterms, merge theories*)
   1.434 +fun add_ctpair ((ct,cu), (sign,tpairs)) =
   1.435 +  let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct
   1.436 +      and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu
   1.437 +  in  if T=U  then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
   1.438 +      else raise TYPE("add_ctpair", [T,U], [t,u])
   1.439 +  end;
   1.440 +
   1.441 +fun add_ctyp ((v,ctyp), (sign',vTs)) =
   1.442 +  let val {T,sign} = Sign.rep_ctyp ctyp
   1.443 +  in (Sign.merge(sign,sign'), (v,T)::vTs) end;
   1.444 +
   1.445 +fun duplicates t = findrep (map (#1 o dest_Var) (term_vars t));
   1.446 +
   1.447 +(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
   1.448 +  Instantiates distinct Vars by terms of same type.
   1.449 +  Normalizes the new theorem! *)
   1.450 +fun instantiate (vcTs,ctpairs)  (th as Thm{sign,maxidx,hyps,prop}) = 
   1.451 +  let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
   1.452 +      val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
   1.453 +      val prop = Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop;
   1.454 +      val newprop = Envir.norm_term (Envir.empty 0) (subst_atomic tpairs prop)
   1.455 +      val newth = Thm{sign= newsign, hyps= hyps,
   1.456 +		      maxidx= maxidx_of_term newprop, prop= newprop}
   1.457 +  in  if not(instl_ok(map #1 tpairs)) orelse not(null(findrep(map #1 vTs)))
   1.458 +      then raise THM("instantiate: not distinct Vars", 0, [th])
   1.459 +      else case duplicates newprop of
   1.460 +	     [] => newth
   1.461 +	   | ix::_ => raise THM("instantiate: conflicting types for " ^
   1.462 +				Syntax.string_of_vname ix ^ "\n", 0, [newth])
   1.463 +  end
   1.464 +  handle TERM _ => 
   1.465 +           raise THM("instantiate: incompatible signatures",0,[th])
   1.466 +       | TYPE _ => raise THM("instantiate: types", 0, [th]);
   1.467 +
   1.468 +
   1.469 +(*The trivial implication A==>A, justified by assume and forall rules.
   1.470 +  A can contain Vars, not so for assume!   *)
   1.471 +fun trivial ct : thm = 
   1.472 +  let val {sign, t=A, T, maxidx} = Sign.rep_cterm ct
   1.473 +  in  if T<>propT then  
   1.474 +	    raise THM("trivial: the term must have type prop", 0, [])
   1.475 +      else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A}
   1.476 +  end;
   1.477 +
   1.478 +(* Replace all TFrees not in the hyps by new TVars *)
   1.479 +fun varifyT(Thm{sign,maxidx,hyps,prop}) =
   1.480 +  let val tfrees = foldr add_term_tfree_names (hyps,[])
   1.481 +  in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps,
   1.482 +	 prop= Type.varify(prop,tfrees)}
   1.483 +  end;
   1.484 +
   1.485 +(* Replace all TVars by new TFrees *)
   1.486 +fun freezeT(Thm{sign,maxidx,hyps,prop}) =
   1.487 +  let val prop' = Type.freeze (K true) prop
   1.488 +  in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end;
   1.489 +
   1.490 +
   1.491 +(*** Inference rules for tactics ***)
   1.492 +
   1.493 +(*Destruct proof state into constraints, other goals, goal(i), rest *)
   1.494 +fun dest_state (state as Thm{prop,...}, i) =
   1.495 +  let val (tpairs,horn) = Logic.strip_flexpairs prop
   1.496 +  in  case  Logic.strip_prems(i, [], horn) of
   1.497 +          (B::rBs, C) => (tpairs, rev rBs, B, C)
   1.498 +        | _ => raise THM("dest_state", i, [state])
   1.499 +  end
   1.500 +  handle TERM _ => raise THM("dest_state", i, [state]);
   1.501 +
   1.502 +(*Increment variables and parameters of rule as required for
   1.503 +  resolution with goal i of state. *)
   1.504 +fun lift_rule (state, i) orule =
   1.505 +  let val Thm{prop=sprop,maxidx=smax,...} = state;
   1.506 +      val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
   1.507 +	handle TERM _ => raise THM("lift_rule", i, [orule,state]);
   1.508 +      val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1);
   1.509 +      val (Thm{sign,maxidx,hyps,prop}) = orule
   1.510 +      val (tpairs,As,B) = Logic.strip_horn prop
   1.511 +  in  Thm{hyps=hyps, sign= merge_theories(state,orule),
   1.512 +	  maxidx= maxidx+smax+1,
   1.513 +	  prop= Logic.rule_of(map (pairself lift_abs) tpairs,
   1.514 +			      map lift_all As,    lift_all B)}
   1.515 +  end;
   1.516 +
   1.517 +(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
   1.518 +fun assumption i state =
   1.519 +  let val Thm{sign,maxidx,hyps,prop} = state;
   1.520 +      val (tpairs, Bs, Bi, C) = dest_state(state,i)
   1.521 +      fun newth (env as Envir.Envir{maxidx,asol,iTs}, tpairs) =
   1.522 +	  Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   1.523 +	    case (Envir.alist_of_olist asol, iTs) of
   1.524 +		(*avoid wasted normalizations*)
   1.525 +	        ([],[]) => Logic.rule_of(tpairs, Bs, C)
   1.526 +	      | _ => (*normalize the new rule fully*)
   1.527 +		      Envir.norm_term env (Logic.rule_of(tpairs, Bs, C))};
   1.528 +      fun addprfs [] = Sequence.null
   1.529 +        | addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
   1.530 +             (Sequence.mapp newth
   1.531 +	        (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 
   1.532 +	        (addprfs apairs)))
   1.533 +  in  addprfs (Logic.assum_pairs Bi)  end;
   1.534 +
   1.535 +(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
   1.536 +  Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
   1.537 +fun eq_assumption i state =
   1.538 +  let val Thm{sign,maxidx,hyps,prop} = state;
   1.539 +      val (tpairs, Bs, Bi, C) = dest_state(state,i)
   1.540 +  in  if exists (op aconv) (Logic.assum_pairs Bi)
   1.541 +      then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
   1.542 +	       prop=Logic.rule_of(tpairs, Bs, C)}
   1.543 +      else  raise THM("eq_assumption", 0, [state])
   1.544 +  end;
   1.545 +
   1.546 +
   1.547 +(** User renaming of parameters in a subgoal **)
   1.548 +
   1.549 +(*Calls error rather than raising an exception because it is intended
   1.550 +  for top-level use -- exception handling would not make sense here.
   1.551 +  The names in cs, if distinct, are used for the innermost parameters;
   1.552 +   preceding parameters may be renamed to make all params distinct.*)
   1.553 +fun rename_params_rule (cs, i) state =
   1.554 +  let val Thm{sign,maxidx,hyps,prop} = state
   1.555 +      val (tpairs, Bs, Bi, C) = dest_state(state,i)
   1.556 +      val iparams = map #1 (Logic.strip_params Bi)
   1.557 +      val short = length iparams - length cs
   1.558 +      val newnames = 
   1.559 +	    if short<0 then error"More names than abstractions!"
   1.560 +	    else variantlist(take (short,iparams), cs) @ cs
   1.561 +      val freenames = map (#1 o dest_Free) (term_frees prop)
   1.562 +      val newBi = Logic.list_rename_params (newnames, Bi)
   1.563 +  in  
   1.564 +  case findrep cs of
   1.565 +     c::_ => error ("Bound variables not distinct: " ^ c)
   1.566 +   | [] => (case cs inter freenames of
   1.567 +       a::_ => error ("Bound/Free variable clash: " ^ a)
   1.568 +     | [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop=
   1.569 +		    Logic.rule_of(tpairs, Bs@[newBi], C)})
   1.570 +  end;
   1.571 +
   1.572 +(*** Preservation of bound variable names ***)
   1.573 +
   1.574 +(*Scan a pair of terms; while they are similar, 
   1.575 +  accumulate corresponding bound vars in "al"*)
   1.576 +fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)
   1.577 +  | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   1.578 +  | match_bvs(_,_,al) = al;
   1.579 +
   1.580 +(* strip abstractions created by parameters *)
   1.581 +fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   1.582 +
   1.583 +
   1.584 +(* strip_apply f A(,B) strips off all assumptions/parameters from A 
   1.585 +   introduced by lifting over B, and applies f to remaining part of A*)
   1.586 +fun strip_apply f =
   1.587 +  let fun strip(Const("==>",_)$ A1 $ B1,
   1.588 +		Const("==>",_)$ _  $ B2) = implies $ A1 $ strip(B1,B2)
   1.589 +	| strip((c as Const("all",_)) $ Abs(a,T,t1),
   1.590 +		      Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
   1.591 +	| strip(A,_) = f A
   1.592 +  in strip end;
   1.593 +
   1.594 +(*Use the alist to rename all bound variables and some unknowns in a term
   1.595 +  dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
   1.596 +  Preserves unknowns in tpairs and on lhs of dpairs. *)
   1.597 +fun rename_bvs([],_,_,_) = I
   1.598 +  | rename_bvs(al,dpairs,tpairs,B) =
   1.599 +    let val vars = foldr add_term_vars 
   1.600 +			(map fst dpairs @ map fst tpairs @ map snd tpairs, [])
   1.601 +	(*unknowns appearing elsewhere be preserved!*)
   1.602 +	val vids = map (#1 o #1 o dest_Var) vars;
   1.603 +	fun rename(t as Var((x,i),T)) =
   1.604 +		(case assoc(al,x) of
   1.605 +		   Some(y) => if x mem vids orelse y mem vids then t
   1.606 +			      else Var((y,i),T)
   1.607 +		 | None=> t)
   1.608 +          | rename(Abs(x,T,t)) =
   1.609 +	      Abs(case assoc(al,x) of Some(y) => y | None => x,
   1.610 +		  T, rename t)
   1.611 +          | rename(f$t) = rename f $ rename t
   1.612 +          | rename(t) = t;
   1.613 +	fun strip_ren Ai = strip_apply rename (Ai,B)
   1.614 +    in strip_ren end;
   1.615 +
   1.616 +(*Function to rename bounds/unknowns in the argument, lifted over B*)
   1.617 +fun rename_bvars(dpairs, tpairs, B) =
   1.618 +	rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B);
   1.619 +
   1.620 +
   1.621 +(*** RESOLUTION ***)
   1.622 +
   1.623 +(*strip off pairs of assumptions/parameters in parallel -- they are
   1.624 +  identical because of lifting*)
   1.625 +fun strip_assums2 (Const("==>", _) $ _ $ B1, 
   1.626 +		   Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2)
   1.627 +  | strip_assums2 (Const("all",_)$Abs(a,T,t1),
   1.628 +		   Const("all",_)$Abs(_,_,t2)) = 
   1.629 +      let val (B1,B2) = strip_assums2 (t1,t2)
   1.630 +      in  (Abs(a,T,B1), Abs(a,T,B2))  end
   1.631 +  | strip_assums2 BB = BB;
   1.632 +
   1.633 +
   1.634 +(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)
   1.635 +  Unifies B with Bi, replacing subgoal i    (1 <= i <= n)  
   1.636 +  If match then forbid instantiations in proof state
   1.637 +  If lifted then shorten the dpair using strip_assums2.
   1.638 +  If eres_flg then simultaneously proves A1 by assumption.
   1.639 +  nsubgoal is the number of new subgoals (written m above). 
   1.640 +  Curried so that resolution calls dest_state only once.
   1.641 +*)
   1.642 +local open Sequence; exception Bicompose
   1.643 +in
   1.644 +fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
   1.645 +                        (eres_flg, orule, nsubgoal) =
   1.646 + let val Thm{maxidx=smax, hyps=shyps, ...} = state
   1.647 +     and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule;
   1.648 +     val sign = merge_theories(state,orule);
   1.649 +     (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
   1.650 +     fun addth As ((env as Envir.Envir{maxidx,asol,iTs}, tpairs), thq) =
   1.651 +       let val minenv = case Envir.alist_of_olist asol of
   1.652 +			  [] => ~1  |  ((_,i),_) :: _ => i;
   1.653 +	   val minx = min (minenv :: map (fn ((_,i),_) => i) iTs);
   1.654 +	   val normt = Envir.norm_term env;
   1.655 +	   (*Perform minimal copying here by examining env*)
   1.656 +	   val normp = if minx = ~1 then (tpairs, Bs@As, C) 
   1.657 +		       else 
   1.658 +		       let val ntps = map (pairself normt) tpairs
   1.659 +		       in if minx>smax then (*no assignments in state*)
   1.660 +			    (ntps, Bs @ map normt As, C)
   1.661 +			  else if match then raise Bicompose
   1.662 +			  else (*normalize the new rule fully*)
   1.663 +			    (ntps, map normt (Bs @ As), normt C)
   1.664 +		       end
   1.665 +	   val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx,
   1.666 +			prop= Logic.rule_of normp}
   1.667 +        in  cons(th, thq)  end  handle Bicompose => thq
   1.668 +     val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop);
   1.669 +     val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn)
   1.670 +       handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]);
   1.671 +     (*Modify assumptions, deleting n-th if n>0 for e-resolution*)
   1.672 +     fun newAs(As0, n, dpairs, tpairs) =
   1.673 +       let val As1 = if !Logic.auto_rename orelse not lifted then As0
   1.674 +		     else map (rename_bvars(dpairs,tpairs,B)) As0
   1.675 +       in (map (Logic.flatten_params n) As1)
   1.676 +	  handle TERM _ =>
   1.677 +	  raise THM("bicompose: 1st premise", 0, [orule])
   1.678 +       end;
   1.679 +     val env = Envir.empty(max[rmax,smax]);
   1.680 +     val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
   1.681 +     val dpairs = BBi :: (rtpairs@stpairs);
   1.682 +     (*elim-resolution: try each assumption in turn.  Initially n=1*)
   1.683 +     fun tryasms (_, _, []) = null
   1.684 +       | tryasms (As, n, (t,u)::apairs) =
   1.685 +	  (case pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
   1.686 +	       None                   => tryasms (As, n+1, apairs)
   1.687 +	     | cell as Some((_,tpairs),_) => 
   1.688 +		   its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs)))
   1.689 +		       (seqof (fn()=> cell),
   1.690 +		        seqof (fn()=> pull (tryasms (As, n+1, apairs)))));
   1.691 +     fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
   1.692 +       | eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1);
   1.693 +     (*ordinary resolution*)
   1.694 +     fun res(None) = null
   1.695 +       | res(cell as Some((_,tpairs),_)) = 
   1.696 +	     its_right (addth(newAs(rev rAs, 0, [BBi], tpairs)))
   1.697 +	 	       (seqof (fn()=> cell), null)
   1.698 + in  if eres_flg then eres(rev rAs)
   1.699 +     else res(pull(Unify.unifiers(sign, env, dpairs)))
   1.700 + end;
   1.701 +end;  (*open Sequence*)
   1.702 +
   1.703 +
   1.704 +fun bicompose match arg i state =
   1.705 +    bicompose_aux match (state, dest_state(state,i), false) arg;
   1.706 +
   1.707 +(*Quick test whether rule is resolvable with the subgoal with hyps Hs
   1.708 +  and conclusion B.  If eres_flg then checks 1st premise of rule also*)
   1.709 +fun could_bires (Hs, B, eres_flg, rule) =
   1.710 +    let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs
   1.711 +	  | could_reshyp [] = false;  (*no premise -- illegal*)
   1.712 +    in  could_unify(concl_of rule, B) andalso 
   1.713 +	(not eres_flg  orelse  could_reshyp (prems_of rule))
   1.714 +    end;
   1.715 +
   1.716 +(*Bi-resolution of a state with a list of (flag,rule) pairs.
   1.717 +  Puts the rule above:  rule/state.  Renames vars in the rules. *)
   1.718 +fun biresolution match brules i state = 
   1.719 +    let val lift = lift_rule(state, i);
   1.720 +	val (stpairs, Bs, Bi, C) = dest_state(state,i)
   1.721 +	val B = Logic.strip_assums_concl Bi;
   1.722 +	val Hs = Logic.strip_assums_hyp Bi;
   1.723 +	val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
   1.724 +	fun res [] = Sequence.null
   1.725 +	  | res ((eres_flg, rule)::brules) = 
   1.726 +	      if could_bires (Hs, B, eres_flg, rule)
   1.727 +	      then Sequence.seqof (*delay processing remainder til needed*)
   1.728 +	          (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
   1.729 +			       res brules))
   1.730 +	      else res brules
   1.731 +    in  Sequence.flats (res brules)  end;
   1.732 +
   1.733 +
   1.734 +(**** THEORIES ****)
   1.735 +
   1.736 +val pure_thy = Pure{sign = Sign.pure};
   1.737 +
   1.738 +(*Look up the named axiom in the theory*)
   1.739 +fun get_axiom thy axname =
   1.740 +    let fun get (Pure _) = raise Match
   1.741 +	  | get (Extend{axioms,thy,...}) =
   1.742 +	     (case Symtab.lookup(axioms,axname) of
   1.743 +		  Some th => th
   1.744 +		| None => get thy)
   1.745 + 	 | get (Merge{thy1,thy2,...}) = 
   1.746 +		get thy1  handle Match => get thy2
   1.747 +    in  get thy
   1.748 +	handle Match => raise THEORY("get_axiom: No axiom "^axname, [thy])
   1.749 +    end;
   1.750 +
   1.751 +(*Converts Frees to Vars: axioms can be written without question marks*)
   1.752 +fun prepare_axiom sign sP =
   1.753 +    Logic.varify (Sign.term_of (Sign.read_cterm sign (sP,propT)));
   1.754 +
   1.755 +(*Read an axiom for a new theory*)
   1.756 +fun read_ax sign (a, sP) : string*thm =
   1.757 +  let val prop = prepare_axiom sign sP
   1.758 +  in  (a, Thm{sign=sign, hyps=[], maxidx= maxidx_of_term prop, prop= prop}) 
   1.759 +  end
   1.760 +  handle ERROR =>
   1.761 +	error("extend_theory: The error above occurred in axiom " ^ a);
   1.762 +
   1.763 +fun mk_axioms sign axpairs =
   1.764 +	Symtab.st_of_alist(map (read_ax sign) axpairs, Symtab.null)
   1.765 +	handle Symtab.DUPLICATE(a) => error("Two axioms named " ^ a);
   1.766 +
   1.767 +(*Extension of a theory with given classes, types, constants and syntax.
   1.768 +  Reads the axioms from strings: axpairs have the form (axname, axiom). *)
   1.769 +fun extend_theory thy thyname ext axpairs =
   1.770 +  let val sign = Sign.extend (sign_of thy) thyname ext;
   1.771 +      val axioms= mk_axioms sign axpairs
   1.772 +  in  Extend{sign=sign, axioms= axioms, thy = thy}  end;
   1.773 +
   1.774 +(*The union of two theories*)
   1.775 +fun merge_theories (thy1,thy2) =
   1.776 +    Merge{sign = Sign.merge(sign_of thy1, sign_of thy2),
   1.777 +	  thy1 = thy1, thy2 = thy2};
   1.778 +
   1.779 +
   1.780 +(*** Meta simp sets ***)
   1.781 +
   1.782 +type rrule = {thm:thm, lhs:term};
   1.783 +datatype meta_simpset =
   1.784 +  Mss of {net:rrule Net.net, congs:(string * rrule)list, primes:string,
   1.785 +          prems: thm list, mk_rews: thm -> thm list};
   1.786 +
   1.787 +(*A "mss" contains data needed during conversion:
   1.788 +  net: discrimination net of rewrite rules
   1.789 +  congs: association list of congruence rules
   1.790 +  primes: offset for generating unique new names
   1.791 +          for rewriting under lambda abstractions
   1.792 +  mk_rews: used when local assumptions are added
   1.793 +*)
   1.794 +
   1.795 +val empty_mss = Mss{net= Net.empty, congs= [], primes="", prems= [],
   1.796 +                    mk_rews = K[]};
   1.797 +
   1.798 +exception SIMPLIFIER of string * thm;
   1.799 +
   1.800 +fun prtm a sg t = (writeln a; writeln(Sign.string_of_term sg t));
   1.801 +
   1.802 +(*simple test for looping rewrite*)
   1.803 +fun loops sign prems (lhs,rhs) =
   1.804 +  null(prems) andalso
   1.805 +  Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs);
   1.806 +
   1.807 +fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) =
   1.808 +  let val prems = Logic.strip_imp_prems prop
   1.809 +      val concl = Pattern.eta_contract (Logic.strip_imp_concl prop)
   1.810 +      val (lhs,rhs) = Logic.dest_equals concl handle TERM _ =>
   1.811 +                      raise SIMPLIFIER("Rewrite rule not a meta-equality",thm)
   1.812 +  in if loops sign prems (lhs,rhs)
   1.813 +     then (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
   1.814 +     else Some{thm=thm,lhs=lhs}
   1.815 +  end;
   1.816 +
   1.817 +fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews},
   1.818 +             thm as Thm{sign,prop,...}) =
   1.819 +  let fun eq({thm=Thm{prop=p1,...},...}:rrule,
   1.820 +             {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2
   1.821 +  in case mk_rrule thm of
   1.822 +       None => mss
   1.823 +     | Some(rrule as {lhs,...}) =>
   1.824 +         Mss{net= (Net.insert_term((lhs,rrule),net,eq)
   1.825 +                   handle Net.INSERT =>
   1.826 +                   (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
   1.827 +                    net)),
   1.828 +             congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}
   1.829 +  end;
   1.830 +
   1.831 +val add_simps = foldl add_simp;
   1.832 +
   1.833 +fun mss_of thms = add_simps(empty_mss,thms);
   1.834 +
   1.835 +fun add_cong(Mss{net,congs,primes,prems,mk_rews},thm) =
   1.836 +  let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ =>
   1.837 +                    raise SIMPLIFIER("Congruence not a meta-equality",thm)
   1.838 +      val lhs = Pattern.eta_contract lhs
   1.839 +      val (a,_) = dest_Const (head_of lhs) handle TERM _ =>
   1.840 +                  raise SIMPLIFIER("Congruence must start with a constant",thm)
   1.841 +  in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, primes=primes,
   1.842 +         prems=prems, mk_rews=mk_rews}
   1.843 +  end;
   1.844 +
   1.845 +val (op add_congs) = foldl add_cong;
   1.846 +
   1.847 +fun add_prems(Mss{net,congs,primes,prems,mk_rews},thms) =
   1.848 +  Mss{net=net, congs=congs, primes=primes, prems=thms@prems, mk_rews=mk_rews};
   1.849 +
   1.850 +fun prems_of_mss(Mss{prems,...}) = prems;
   1.851 +
   1.852 +fun set_mk_rews(Mss{net,congs,primes,prems,...},mk_rews) =
   1.853 +  Mss{net=net, congs=congs, primes=primes, prems=prems, mk_rews=mk_rews};
   1.854 +fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews;
   1.855 +
   1.856 +
   1.857 +(*** Meta-level rewriting 
   1.858 +     uses conversions, omitting proofs for efficiency.  See
   1.859 +	L C Paulson, A higher-order implementation of rewriting,
   1.860 +	Science of Computer Programming 3 (1983), pages 119-149. ***)
   1.861 +
   1.862 +type prover = meta_simpset -> thm -> thm option;
   1.863 +type termrec = (Sign.sg * term list) * term;
   1.864 +type conv = meta_simpset -> termrec -> termrec;
   1.865 +
   1.866 +val trace_simp = ref false;
   1.867 +
   1.868 +fun trace_term a sg t = if !trace_simp then prtm a sg t else ();
   1.869 +
   1.870 +fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
   1.871 +
   1.872 +fun check_conv(thm as Thm{sign,hyps,prop,...}, prop0) =
   1.873 +  let fun err() = (trace_term "Proved wrong thm" sign prop;
   1.874 +                   error "Check your prover")
   1.875 +      val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
   1.876 +  in case prop of
   1.877 +       Const("==",_) $ lhs $ rhs =>
   1.878 +         if (lhs = lhs0) orelse
   1.879 +            (lhs aconv (Envir.norm_term (Envir.empty 0) lhs0))
   1.880 +         then (trace_thm "SUCCEEDED" thm; ((sign,hyps),rhs))
   1.881 +         else err()
   1.882 +     | _ => err()
   1.883 +  end;
   1.884 +
   1.885 +(*Conversion to apply the meta simpset to a term*)
   1.886 +fun rewritec prover (mss as Mss{net,...}) (sghyt as (sgt,hypst),t) =
   1.887 +  let val t = Pattern.eta_contract t
   1.888 +      fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs} =
   1.889 +	let val sign' = Sign.merge(sgt,sign)
   1.890 +            val tsig = #tsig(Sign.rep_sg sign')
   1.891 +            val insts = Pattern.match tsig (lhs,t)
   1.892 +            val prop' = subst_vars insts prop;
   1.893 +            val hyps' = hyps union hypst;
   1.894 +            val thm' = Thm{sign=sign', hyps=hyps', prop=prop', maxidx=maxidx}
   1.895 +        in if nprems_of thm' = 0
   1.896 +           then let val (_,rhs) = Logic.dest_equals prop'
   1.897 +                in trace_thm "Rewriting:" thm'; Some((sign',hyps'),rhs) end
   1.898 +           else (trace_thm "Trying to rewrite:" thm';
   1.899 +                 case prover mss thm' of
   1.900 +                   None       => (trace_thm "FAILED" thm'; None)
   1.901 +                 | Some(thm2) => Some(check_conv(thm2,prop')))
   1.902 +        end
   1.903 +
   1.904 +      fun rewl [] = None
   1.905 +	| rewl (rrule::rrules) =
   1.906 +            let val opt = rew rrule handle Pattern.MATCH => None
   1.907 +            in case opt of None => rewl rrules | some => some end;
   1.908 +
   1.909 +  in case t of
   1.910 +       Abs(_,_,body) $ u => Some(sghyt,subst_bounds([u], body))
   1.911 +     | _                 => rewl (Net.match_term net t)
   1.912 +  end;
   1.913 +
   1.914 +(*Conversion to apply a congruence rule to a term*)
   1.915 +fun congc prover {thm=cong,lhs=lhs} (sghyt as (sgt,hypst),t) =
   1.916 +  let val Thm{sign,hyps,maxidx,prop,...} = cong
   1.917 +      val sign' = Sign.merge(sgt,sign)
   1.918 +      val tsig = #tsig(Sign.rep_sg sign')
   1.919 +      val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH =>
   1.920 +                  error("Congruence rule did not match")
   1.921 +      val prop' = subst_vars insts prop;
   1.922 +      val thm' = Thm{sign=sign', hyps=hyps union hypst,
   1.923 +                     prop=prop', maxidx=maxidx}
   1.924 +      val unit = trace_thm "Applying congruence rule" thm';
   1.925 +
   1.926 +  in case prover thm' of
   1.927 +       None => error("Failed congruence proof!")
   1.928 +     | Some(thm2) => check_conv(thm2,prop')
   1.929 +  end;
   1.930 +
   1.931 +
   1.932 +fun bottomc prover =
   1.933 +  let fun botc mss trec = let val trec1 = subc mss trec
   1.934 +                          in case rewritec prover mss trec1 of
   1.935 +                               None => trec1
   1.936 +                             | Some(trec2) => botc mss trec2
   1.937 +                          end
   1.938 +
   1.939 +      and subc (mss as Mss{net,congs,primes,prems,mk_rews})
   1.940 +               (trec as (sghy,t)) =
   1.941 +        (case t of
   1.942 +            Abs(a,T,t) =>
   1.943 +              let val v = Free(".subc." ^ primes,T)
   1.944 +                  val mss' = Mss{net=net, congs=congs, primes=primes^"'",
   1.945 +                                 prems=prems,mk_rews=mk_rews}
   1.946 +                  val (sghy',t') = botc mss' (sghy,subst_bounds([v],t))
   1.947 +              in  (sghy', Abs(a, T, abstract_over(v,t')))  end
   1.948 +          | t$u => (case t of
   1.949 +              Const("==>",_)$s  => impc(sghy,s,u,mss)
   1.950 +            | Abs(_,_,body)     => subc mss (sghy,subst_bounds([u], body))
   1.951 +            | _                 =>
   1.952 +                let fun appc() = let val (sghy1,t1) = botc mss (sghy,t)
   1.953 +                                     val (sghy2,u1) = botc mss (sghy1,u)
   1.954 +                                 in (sghy2,t1$u1) end
   1.955 +                    val (h,ts) = strip_comb t
   1.956 +                in case h of
   1.957 +                     Const(a,_) =>
   1.958 +                       (case assoc(congs,a) of
   1.959 +                          None => appc()
   1.960 +                        | Some(cong) => congc (prover mss) cong trec)
   1.961 +                   | _ => appc()
   1.962 +                end)
   1.963 +          | _ => trec)
   1.964 +
   1.965 +      and impc(sghy,s,u,mss as Mss{mk_rews,...}) =
   1.966 +        let val (sghy1 as (sg1,hyps1),s') = botc mss (sghy,s)
   1.967 +            val (rthms,mss) =
   1.968 +              if maxidx_of_term s' <> ~1 then ([],mss)
   1.969 +              else let val thm = Thm{sign=sg1,hyps=[s'],prop=s',maxidx= ~1}
   1.970 +                   in (mk_rews thm, add_prems(mss,[thm])) end
   1.971 +            val unit = seq (trace_thm "Adding rewrite rule:") rthms
   1.972 +            val mss' = add_simps(mss,rthms)
   1.973 +            val ((sg2,hyps2),u') = botc mss' (sghy1,u)
   1.974 +        in ((sg2,hyps2\s'), Logic.mk_implies(s',u')) end
   1.975 +
   1.976 +  in botc end;
   1.977 +
   1.978 +
   1.979 +(*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
   1.980 +(* Parameters:
   1.981 +   mss: contains equality theorems of the form [|p1,...|] ==> t==u
   1.982 +   prover: how to solve premises in conditional rewrites and congruences
   1.983 +*)
   1.984 +
   1.985 +(*** FIXME: check that #primes(mss) does not "occur" in ct alread ***)
   1.986 +fun rewrite_cterm mss prover ct =
   1.987 +  let val {sign, t, T, maxidx} = Sign.rep_cterm ct;
   1.988 +      val ((sign',hyps),u) = bottomc prover mss ((sign,[]),t);
   1.989 +      val prop = Logic.mk_equals(t,u)
   1.990 +  in  Thm{sign= sign', hyps= hyps, maxidx= maxidx_of_term prop, prop= prop}
   1.991 +  end
   1.992 +
   1.993 +end;