src/Pure/term.ML
author wenzelm
Wed May 18 15:20:54 1994 +0200 (1994-05-18)
changeset 375 d7ae7ac22d48
parent 61 f8c1922b78e3
child 728 9a973c3ba350
permissions -rw-r--r--
added logicC: class, logicS: sort;
added itselfT: typ -> typ, a_itselfT: typ (for axclasses);
     1 (*  Title: 	Pure/term.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 *)
     6 
     7 
     8 (*Simply typed lambda-calculus: types, terms, and basic operations*)
     9 
    10 
    11 (*Indexnames can be quickly renamed by adding an offset to the integer part,
    12   for resolution.*)
    13 type indexname = string*int;
    14 
    15 (* Types are classified by classes. *)
    16 type class = string;
    17 type sort  = class list;
    18 
    19 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
    20 datatype typ = Type  of string * typ list
    21              | TFree of string * sort
    22 	     | TVar  of indexname * sort;
    23 
    24 infixr 5 -->;
    25 fun S --> T = Type("fun",[S,T]);
    26 
    27 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
    28 infixr --->;
    29 val op ---> = foldr (op -->);
    30 
    31 
    32 (*terms.  Bound variables are indicated by depth number.
    33   Free variables, (scheme) variables and constants have names.
    34   An term is "closed" if there every bound variable of level "lev"
    35   is enclosed by at least "lev" abstractions. 
    36 
    37   It is possible to create meaningless terms containing loose bound vars
    38   or type mismatches.  But such terms are not allowed in rules. *)
    39 
    40 
    41 
    42 infix 9 $;  (*application binds tightly!*)
    43 datatype term = 
    44     Const of string * typ
    45   | Free  of string * typ 
    46   | Var   of indexname * typ
    47   | Bound of int
    48   | Abs   of string*typ*term
    49   | op $  of term*term;
    50 
    51 
    52 (*For errors involving type mismatches*)
    53 exception TYPE of string * typ list * term list;
    54 
    55 fun raise_type msg tys ts = raise TYPE (msg, tys, ts);
    56 
    57 (*For system errors involving terms*)
    58 exception TERM of string * term list;
    59 
    60 fun raise_term msg ts = raise TERM (msg, ts);
    61 
    62 
    63 (*Note variable naming conventions!
    64     a,b,c: string
    65     f,g,h: functions (including terms of function type)
    66     i,j,m,n: int
    67     t,u: term
    68     v,w: indexnames
    69     x,y: any
    70     A,B,C: term (denoting formulae)
    71     T,U: typ
    72 *)
    73 
    74 
    75 (** Discriminators **)
    76 
    77 fun is_Const (Const _) = true
    78   | is_Const _ = false;
    79 
    80 fun is_Free (Free _) = true
    81   | is_Free _ = false;
    82 
    83 fun is_Var (Var _) = true
    84   | is_Var _ = false;
    85 
    86 fun is_TVar (TVar _) = true
    87   | is_TVar _ = false;
    88 
    89 (** Destructors **)
    90 
    91 fun dest_Const (Const x) =  x
    92   | dest_Const t = raise TERM("dest_Const", [t]);
    93 
    94 fun dest_Free (Free x) =  x
    95   | dest_Free t = raise TERM("dest_Free", [t]);
    96 
    97 fun dest_Var (Var x) =  x
    98   | dest_Var t = raise TERM("dest_Var", [t]);
    99 
   100 
   101 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   102 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   103   | binder_types _   =  [];
   104 
   105 (* maps  [T1,...,Tn]--->T  to T*)
   106 fun body_type (Type("fun",[S,T])) = body_type T
   107   | body_type T   =  T;
   108 
   109 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   110 fun strip_type T : typ list * typ =
   111   (binder_types T, body_type T);
   112 
   113 
   114 (*Compute the type of the term, checking that combinations are well-typed
   115   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   116 fun type_of1 (Ts, Const (_,T)) = T
   117   | type_of1 (Ts, Free  (_,T)) = T
   118   | type_of1 (Ts, Bound i) = (nth_elem (i,Ts)  
   119   	handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))
   120   | type_of1 (Ts, Var (_,T)) = T
   121   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   122   | type_of1 (Ts, f$u) = 
   123       let val U = type_of1(Ts,u)
   124           and T = type_of1(Ts,f)
   125       in case T of
   126 	    Type("fun",[T1,T2]) =>
   127 	      if T1=U then T2  else raise TYPE
   128 	         ("type_of: type mismatch in application", [T1,U], [f$u])
   129 	  | _ => raise TYPE ("type_of: Rator must have function type",
   130 	                        [T,U], [f$u])
   131       end;
   132 
   133 fun type_of t : typ = type_of1 ([],t);
   134 
   135 (*Determines the type of a term, with minimal checking*)
   136 fun fastype_of1 (Ts, f$u) = 
   137     (case fastype_of1 (Ts,f) of
   138 	Type("fun",[_,T]) => T
   139 	| _ => raise TERM("fastype_of: expected function type", [f$u]))
   140   | fastype_of1 (_, Const (_,T)) = T
   141   | fastype_of1 (_, Free (_,T)) = T
   142   | fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts)
   143   	 handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))
   144   | fastype_of1 (_, Var (_,T)) = T 
   145   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   146 
   147 fun fastype_of t : typ = fastype_of1 ([],t);
   148 
   149 
   150 (* maps  (x1,...,xn)t   to   t  *)
   151 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t  
   152   | strip_abs_body u  =  u;
   153 
   154 
   155 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   156 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t 
   157   | strip_abs_vars u  =  [] : (string*typ) list;
   158 
   159 
   160 fun strip_qnt_body qnt =
   161 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   162       | strip t = t
   163 in strip end;
   164 
   165 fun strip_qnt_vars qnt =
   166 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   167       | strip t  =  [] : (string*typ) list
   168 in strip end;
   169 
   170 
   171 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   172 val list_comb : term * term list -> term = foldl (op $);
   173 
   174 
   175 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   176 fun strip_comb u : term * term list = 
   177     let fun stripc (f$t, ts) = stripc (f, t::ts)
   178         |   stripc  x =  x 
   179     in  stripc(u,[])  end;
   180 
   181 
   182 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   183 fun head_of (f$t) = head_of f
   184   | head_of u = u;
   185 
   186 
   187 (*Number of atoms and abstractions in a term*)
   188 fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
   189   | size_of_term (f$t) = size_of_term f  +  size_of_term t
   190   | size_of_term _ = 1;
   191 
   192  
   193 (* apply a function to all types in a term *)
   194 fun map_term_types f =
   195 let fun map(Const(a,T)) = Const(a, f T)
   196       | map(Free(a,T)) = Free(a, f T)
   197       | map(Var(v,T)) = Var(v, f T)
   198       | map(t as Bound _)  = t
   199       | map(Abs(a,T,t)) = Abs(a, f T, map t)
   200       | map(f$t) = map f $ map t;
   201 in map end;
   202 
   203 (* iterate a function over all types in a term *)
   204 fun it_term_types f =
   205 let fun iter(Const(_,T), a) = f(T,a)
   206       | iter(Free(_,T), a) = f(T,a)
   207       | iter(Var(_,T), a) = f(T,a)
   208       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   209       | iter(f$u, a) = iter(f, iter(u, a))
   210       | iter(Bound _, a) = a
   211 in iter end
   212 
   213 
   214 (** Connectives of higher order logic **)
   215 
   216 val logicC: class = "logic";
   217 val logicS: sort = [logicC];
   218 
   219 fun itselfT ty = Type ("itself", [ty]);
   220 val a_itselfT = itselfT (TFree ("'a", logicS));
   221 
   222 val propT : typ = Type("prop",[]);
   223 
   224 val implies = Const("==>", propT-->propT-->propT);
   225 
   226 fun all T = Const("all", (T-->propT)-->propT);
   227 
   228 fun equals T = Const("==", T-->T-->propT);
   229 
   230 fun flexpair T = Const("=?=", T-->T-->propT);
   231 
   232 (* maps  !!x1...xn. t   to   t  *)
   233 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t  
   234   | strip_all_body t  =  t;
   235 
   236 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   237 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   238 		(a,T) :: strip_all_vars t 
   239   | strip_all_vars t  =  [] : (string*typ) list;
   240 
   241 (*increments a term's non-local bound variables
   242   required when moving a term within abstractions
   243      inc is  increment for bound variables
   244      lev is  level at which a bound variable is considered 'loose'*)
   245 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   246   | incr_bv (inc, lev, Abs(a,T,body)) =
   247 	Abs(a, T, incr_bv(inc,lev+1,body))
   248   | incr_bv (inc, lev, f$t) = 
   249       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   250   | incr_bv (inc, lev, u) = u;
   251 
   252 fun incr_boundvars  0  t = t
   253   | incr_boundvars inc t = incr_bv(inc,0,t);
   254 
   255 
   256 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   257    (Bound 0) is loose at level 0 *)
   258 fun add_loose_bnos (Bound i, lev, js) = 
   259 	if i<lev then js  else  (i-lev) :: js
   260   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   261   | add_loose_bnos (f$t, lev, js) =
   262 	add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   263   | add_loose_bnos (_, _, js) = js;
   264 
   265 fun loose_bnos t = add_loose_bnos (t, 0, []);
   266 
   267 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   268    level k or beyond. *)
   269 fun loose_bvar(Bound i,k) = i >= k
   270   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   271   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   272   | loose_bvar _ = false;
   273 
   274 
   275 (*Substitute arguments for loose bound variables.
   276   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   277   Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0
   278 	and the appropriate call is  subst_bounds([b,a], c) .
   279   Loose bound variables >=n are reduced by "n" to
   280      compensate for the disappearance of lambdas.
   281 *)
   282 fun subst_bounds (args: term list, t) : term = 
   283   let val n = length args;
   284       fun subst (t as Bound i, lev) =
   285  	    if i<lev then  t    (*var is locally bound*)
   286 	    else  (case (drop (i-lev,args)) of
   287 		  []     => Bound(i-n)  (*loose: change it*)
   288 	        | arg::_ => incr_boundvars lev arg)
   289 	| subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
   290 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   291 	| subst (t,lev) = t
   292   in   case args of [] => t  | _ => subst (t,0)  end;
   293 
   294 (*beta-reduce if possible, else form application*)
   295 fun betapply (Abs(_,_,t), u) = subst_bounds([u],t)
   296   | betapply (f,u) = f$u;
   297 
   298 (*Tests whether 2 terms are alpha-convertible and have same type.
   299   Note that constants and Vars may have more than one type.*)
   300 infix aconv;
   301 fun (Const(a,T)) aconv (Const(b,U)) = a=b  andalso  T=U
   302   | (Free(a,T)) aconv (Free(b,U)) = a=b  andalso  T=U
   303   | (Var(v,T)) aconv (Var(w,U)) =   v=w  andalso  T=U
   304   | (Bound i) aconv (Bound j)  =   i=j
   305   | (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u  andalso  T=U
   306   | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)
   307   | _ aconv _  =  false;
   308 
   309 (*are two term lists alpha-convertible in corresponding elements?*)
   310 fun aconvs ([],[]) = true
   311   | aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)
   312   | aconvs _ = false;
   313 
   314 (*A fast unification filter: true unless the two terms cannot be unified. 
   315   Terms must be NORMAL.  Treats all Vars as distinct. *)
   316 fun could_unify (t,u) =
   317   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   318 	| matchrands _ = true
   319   in case (head_of t , head_of u) of
   320 	(_, Var _) => true
   321       | (Var _, _) => true
   322       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   323       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   324       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   325       | (Abs _, _) =>  true   (*because of possible eta equality*)
   326       | (_, Abs _) =>  true
   327       | _ => false
   328   end;
   329 
   330 (*Substitute new for free occurrences of old in a term*)
   331 fun subst_free [] = (fn t=>t)
   332   | subst_free pairs =
   333       let fun substf u = 
   334 	    case gen_assoc (op aconv) (pairs, u) of
   335 		Some u' => u'
   336 	      | None => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   337 				 | t$u' => substf t $ substf u'
   338 				 | _ => u)
   339       in  substf  end;
   340 
   341 (*a total, irreflexive ordering on index names*)
   342 fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
   343 
   344 
   345 (*Abstraction of the term "body" over its occurrences of v, 
   346     which must contain no loose bound variables.
   347   The resulting term is ready to become the body of an Abs.*)
   348 fun abstract_over (v,body) =
   349   let fun abst (lev,u) = if (v aconv u) then (Bound lev) else
   350       (case u of
   351           Abs(a,T,t) => Abs(a, T, abst(lev+1, t))
   352 	| f$rand => abst(lev,f) $ abst(lev,rand)
   353 	| _ => u)
   354   in  abst(0,body)  end;
   355 
   356 
   357 (*Form an abstraction over a free variable.*)
   358 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   359 
   360 (*Abstraction over a list of free variables*)
   361 fun list_abs_free ([ ] ,     t) = t
   362   | list_abs_free ((a,T)::vars, t) = 
   363       absfree(a, T, list_abs_free(vars,t));
   364 
   365 (*Quantification over a list of free variables*)
   366 fun list_all_free ([], t: term) = t
   367   | list_all_free ((a,T)::vars, t) = 
   368         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   369 
   370 (*Quantification over a list of variables (already bound in body) *)
   371 fun list_all ([], t) = t
   372   | list_all ((a,T)::vars, t) = 
   373         (all T) $ (Abs(a, T, list_all(vars,t)));
   374 
   375 (*Replace the ATOMIC term ti by ui;    instl = [(t1,u1), ..., (tn,un)]. 
   376   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   377 fun subst_atomic [] t = t : term
   378   | subst_atomic (instl: (term*term) list) t =
   379       let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)
   380 	    | subst (f$t') = subst f $ subst t'
   381 	    | subst t = (case assoc(instl,t) of
   382 		           Some u => u  |  None => t)
   383       in  subst t  end;
   384 
   385 fun typ_subst_TVars iTs T = if null iTs then T else
   386   let fun subst(Type(a,Ts)) = Type(a, map subst Ts)
   387 	| subst(T as TFree _) = T
   388 	| subst(T as TVar(ixn,_)) =
   389             (case assoc(iTs,ixn) of None => T | Some(U) => U)
   390   in subst T end;
   391 
   392 val subst_TVars = map_term_types o typ_subst_TVars;
   393 
   394 fun subst_Vars itms t = if null itms then t else
   395   let fun subst(v as Var(ixn,_)) =
   396             (case assoc(itms,ixn) of None => v | Some t => t)
   397         | subst(Abs(a,T,t)) = Abs(a,T,subst t)
   398         | subst(f$t) = subst f $ subst t
   399         | subst(t) = t
   400   in subst t end;
   401 
   402 fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else
   403   let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)
   404         | subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)
   405         | subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of
   406             None   => Var(ixn,typ_subst_TVars iTs T)
   407           | Some t => t)
   408         | subst(b as Bound _) = b
   409         | subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)
   410         | subst(f$t) = subst f $ subst t
   411   in subst end;
   412 
   413 
   414 (*Computing the maximum index of a typ*)
   415 fun maxidx_of_typ(Type(_,Ts)) =
   416 	if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
   417   | maxidx_of_typ(TFree _) = ~1
   418   | maxidx_of_typ(TVar((_,i),_)) = i;
   419 
   420 
   421 (*Computing the maximum index of a term*)
   422 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   423   | maxidx_of_term (Bound _) = ~1
   424   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
   425   | maxidx_of_term (Var ((_,i), T)) = max[i, maxidx_of_typ T]
   426   | maxidx_of_term (Abs (_,T,body)) = max[maxidx_of_term body, maxidx_of_typ T]
   427   | maxidx_of_term (f$t) = max [maxidx_of_term f,  maxidx_of_term t];
   428 
   429 
   430 (* Increment the index of all Poly's in T by k *)
   431 fun incr_tvar k (Type(a,Ts)) = Type(a, map (incr_tvar k) Ts)
   432   | incr_tvar k (T as TFree _) = T
   433   | incr_tvar k (TVar((a,i),rs)) = TVar((a,i+k),rs);
   434 
   435 
   436 (**** Syntax-related declarations ****)
   437 
   438 
   439 (*Dummy type for parsing.  Will be replaced during type inference. *)
   440 val dummyT = Type("dummy",[]);
   441 
   442 (*scan a numeral of the given radix, normally 10*)
   443 fun scan_radixint (radix: int, cs) : int * string list =
   444   let val zero = ord"0"
   445       val limit = zero+radix
   446       fun scan (num,[]) = (num,[])
   447 	| scan (num, c::cs) =
   448 	      if  zero <= ord c  andalso  ord c < limit
   449 	      then scan(radix*num + ord c - zero, cs)
   450 	      else (num, c::cs)
   451   in  scan(0,cs)  end;
   452 
   453 fun scan_int cs = scan_radixint(10,cs);
   454 
   455 
   456 (*** Printing ***)
   457 
   458 
   459 (*Makes a variant of the name c distinct from the names in bs.
   460   First attaches the suffix "a" and then increments this. *)
   461 fun variant bs c : string =
   462   let fun vary2 c = if (c mem bs) then  vary2 (bump_string c)  else  c
   463       fun vary1 c = if (c mem bs) then  vary2 (c ^ "a")  else  c
   464   in  vary1 (if c="" then "u" else c)  end;
   465 
   466 (*Create variants of the list of names, with priority to the first ones*)
   467 fun variantlist ([], used) = []
   468   | variantlist(b::bs, used) = 
   469       let val b' = variant used b
   470       in  b' :: variantlist (bs, b'::used)  end;
   471 
   472 (** TFrees and TVars **)
   473 
   474 (*maps  (bs,v)  to   v'::bs    this reverses the identifiers bs*)
   475 fun add_new_id (bs, c) : string list =  variant bs c  ::  bs;
   476 
   477 (*Accumulates the names in the term, suppressing duplicates.
   478   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   479 fun add_term_names (Const(a,_), bs) = a ins bs
   480   | add_term_names (Free(a,_), bs) = a ins bs
   481   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   482   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   483   | add_term_names (_, bs) = bs;
   484 
   485 (*Accumulates the TVars in a type, suppressing duplicates. *)
   486 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)
   487   | add_typ_tvars(TFree(_),vs) = vs
   488   | add_typ_tvars(TVar(v),vs) = v ins vs;
   489 
   490 (*Accumulates the TFrees in a type, suppressing duplicates. *)
   491 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)
   492   | add_typ_tfree_names(TFree(f,_),fs) = f ins fs
   493   | add_typ_tfree_names(TVar(_),fs) = fs;
   494 
   495 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)
   496   | add_typ_tfrees(TFree(f),fs) = f ins fs
   497   | add_typ_tfrees(TVar(_),fs) = fs;
   498 
   499 (*Accumulates the TVars in a term, suppressing duplicates. *)
   500 val add_term_tvars = it_term_types add_typ_tvars;
   501 val add_term_tvar_ixns = (map #1) o (it_term_types add_typ_tvars);
   502 
   503 (*Accumulates the TFrees in a term, suppressing duplicates. *)
   504 val add_term_tfrees = it_term_types add_typ_tfrees;
   505 val add_term_tfree_names = it_term_types add_typ_tfree_names;
   506 
   507 (*Non-list versions*)
   508 fun typ_tfrees T = add_typ_tfrees(T,[]);
   509 fun typ_tvars T = add_typ_tvars(T,[]);
   510 fun term_tfrees t = add_term_tfrees(t,[]);
   511 fun term_tvars t = add_term_tvars(t,[]);
   512 
   513 (** Frees and Vars **)
   514 
   515 (*a partial ordering (not reflexive) for atomic terms*)
   516 fun atless (Const (a,_), Const (b,_))  =  a<b
   517   | atless (Free (a,_), Free (b,_)) =  a<b
   518   | atless (Var(v,_), Var(w,_))  =  xless(v,w)
   519   | atless (Bound i, Bound j)  =   i<j
   520   | atless _  =  false;
   521 
   522 (*insert atomic term into partially sorted list, suppressing duplicates (?)*)
   523 fun insert_aterm (t,us) =
   524   let fun inserta [] = [t]
   525         | inserta (us as u::us') = 
   526 	      if atless(t,u) then t::us
   527 	      else if t=u then us (*duplicate*)
   528 	      else u :: inserta(us')
   529   in  inserta us  end;
   530 
   531 (*Accumulates the Vars in the term, suppressing duplicates*)
   532 fun add_term_vars (t, vars: term list) = case t of
   533     Var   _ => insert_aterm(t,vars)
   534   | Abs (_,_,body) => add_term_vars(body,vars)
   535   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
   536   | _ => vars;
   537 
   538 fun term_vars t = add_term_vars(t,[]);
   539 
   540 (*Accumulates the Frees in the term, suppressing duplicates*)
   541 fun add_term_frees (t, frees: term list) = case t of
   542     Free   _ => insert_aterm(t,frees)
   543   | Abs (_,_,body) => add_term_frees(body,frees)
   544   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
   545   | _ => frees;
   546 
   547 fun term_frees t = add_term_frees(t,[]);
   548 
   549 (*Given an abstraction over P, replaces the bound variable by a Free variable
   550   having a unique name. *)
   551 fun variant_abs (a,T,P) =
   552   let val b = variant (add_term_names(P,[])) a
   553   in  (b,  subst_bounds ([Free(b,T)], P))  end;
   554 
   555 (* renames and reverses the strings in vars away from names *)
   556 fun rename_aTs names vars : (string*typ)list =
   557   let fun rename_aT (vars,(a,T)) =
   558 		(variant (map #1 vars @ names) a, T) :: vars
   559   in foldl rename_aT ([],vars) end;
   560 
   561 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));