src/Pure/term.ML
author haftmann
Fri Oct 13 16:52:48 2006 +0200 (2006-10-13)
changeset 21013 b9321724c2cc
parent 20854 f9cf9e62d11c
child 21353 cfee13454195
permissions -rw-r--r--
fixed bug
     1 (*  Title:      Pure/term.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Simply typed lambda-calculus: types, terms, and basic operations.
     7 *)
     8 
     9 infix 9  $;
    10 infixr 5 -->;
    11 infixr --->;
    12 infix aconv;
    13 
    14 signature BASIC_TERM =
    15 sig
    16   type indexname
    17   type class
    18   type sort
    19   type arity
    20   datatype typ =
    21     Type  of string * typ list |
    22     TFree of string * sort |
    23     TVar  of indexname * sort
    24   datatype term =
    25     Const of string * typ |
    26     Free of string * typ |
    27     Var of indexname * typ |
    28     Bound of int |
    29     Abs of string * typ * term |
    30     $ of term * term
    31   exception TYPE of string * typ list * term list
    32   exception TERM of string * term list
    33   val dummyT: typ
    34   val no_dummyT: typ -> typ
    35   val --> : typ * typ -> typ
    36   val ---> : typ list * typ -> typ
    37   val dest_Type: typ -> string * typ list
    38   val dest_TVar: typ -> indexname * sort
    39   val dest_TFree: typ -> string * sort
    40   val is_Bound: term -> bool
    41   val is_Const: term -> bool
    42   val is_Free: term -> bool
    43   val is_Var: term -> bool
    44   val is_TVar: typ -> bool
    45   val dest_Const: term -> string * typ
    46   val dest_Free: term -> string * typ
    47   val dest_Var: term -> indexname * typ
    48   val domain_type: typ -> typ
    49   val range_type: typ -> typ
    50   val binder_types: typ -> typ list
    51   val body_type: typ -> typ
    52   val strip_type: typ -> typ list * typ
    53   val type_of1: typ list * term -> typ
    54   val type_of: term -> typ
    55   val fastype_of1: typ list * term -> typ
    56   val fastype_of: term -> typ
    57   val list_abs: (string * typ) list * term -> term
    58   val strip_abs: term -> (string * typ) list * term
    59   val strip_abs_body: term -> term
    60   val strip_abs_vars: term -> (string * typ) list
    61   val strip_qnt_body: string -> term -> term
    62   val strip_qnt_vars: string -> term -> (string * typ) list
    63   val list_comb: term * term list -> term
    64   val strip_comb: term -> term * term list
    65   val head_of: term -> term
    66   val size_of_term: term -> int
    67   val map_atyps: (typ -> typ) -> typ -> typ
    68   val map_aterms: (term -> term) -> term -> term
    69   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    70   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    71   val map_types: (typ -> typ) -> term -> term
    72   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    73   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    74   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    75   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    76   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
    77   val add_term_names: term * string list -> string list
    78   val aconv: term * term -> bool
    79   structure Vartab: TABLE
    80   structure Typtab: TABLE
    81   structure Termtab: TABLE
    82   val propT: typ
    83   val implies: term
    84   val all: typ -> term
    85   val equals: typ -> term
    86   val strip_all_body: term -> term
    87   val strip_all_vars: term -> (string * typ) list
    88   val incr_bv: int * int * term -> term
    89   val incr_boundvars: int -> term -> term
    90   val add_loose_bnos: term * int * int list -> int list
    91   val loose_bnos: term -> int list
    92   val loose_bvar: term * int -> bool
    93   val loose_bvar1: term * int -> bool
    94   val subst_bounds: term list * term -> term
    95   val subst_bound: term * term -> term
    96   val betapply: term * term -> term
    97   val betapplys: term * term list -> term
    98   val eq_ix: indexname * indexname -> bool
    99   val could_unify: term * term -> bool
   100   val subst_free: (term * term) list -> term -> term
   101   val abstract_over: term * term -> term
   102   val lambda: term -> term -> term
   103   val absfree: string * typ * term -> term
   104   val absdummy: typ * term -> term
   105   val list_abs_free: (string * typ) list * term -> term
   106   val list_all_free: (string * typ) list * term -> term
   107   val list_all: (string * typ) list * term -> term
   108   val subst_atomic: (term * term) list -> term -> term
   109   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   110   val subst_atomic_types: (typ * typ) list -> term -> term
   111   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   112   val subst_TVars: (indexname * typ) list -> term -> term
   113   val subst_Vars: (indexname * term) list -> term -> term
   114   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   115   val is_first_order: string list -> term -> bool
   116   val maxidx_of_typ: typ -> int
   117   val maxidx_of_typs: typ list -> int
   118   val maxidx_of_term: term -> int
   119   val add_term_consts: term * string list -> string list
   120   val term_consts: term -> string list
   121   val exists_subtype: (typ -> bool) -> typ -> bool
   122   val exists_type: (typ -> bool) -> term -> bool
   123   val exists_subterm: (term -> bool) -> term -> bool
   124   val exists_Const: (string * typ -> bool) -> term -> bool
   125   val add_term_free_names: term * string list -> string list
   126   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   127   val add_typ_tfree_names: typ * string list -> string list
   128   val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
   129   val add_typ_varnames: typ * string list -> string list
   130   val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
   131   val add_term_tfrees: term * (string * sort) list -> (string * sort) list
   132   val add_term_tfree_names: term * string list -> string list
   133   val typ_tfrees: typ -> (string * sort) list
   134   val typ_tvars: typ -> (indexname * sort) list
   135   val term_tfrees: term -> (string * sort) list
   136   val term_tvars: term -> (indexname * sort) list
   137   val add_typ_ixns: indexname list * typ -> indexname list
   138   val add_term_tvar_ixns: term * indexname list -> indexname list
   139   val add_term_vars: term * term list -> term list
   140   val term_vars: term -> term list
   141   val add_term_frees: term * term list -> term list
   142   val term_frees: term -> term list
   143   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   144   val show_question_marks: bool ref
   145 end;
   146 
   147 signature TERM =
   148 sig
   149   include BASIC_TERM
   150   val aT: sort -> typ
   151   val itselfT: typ -> typ
   152   val a_itselfT: typ
   153   val argument_type_of: term -> typ
   154   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   155   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   156   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   157   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   158   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   159   val add_frees: term -> (string * typ) list -> (string * typ) list
   160   val add_varnames: term -> indexname list -> indexname list
   161   val strip_abs_eta: int -> term -> (string * typ) list * term
   162   val fast_indexname_ord: indexname * indexname -> order
   163   val indexname_ord: indexname * indexname -> order
   164   val sort_ord: sort * sort -> order
   165   val typ_ord: typ * typ -> order
   166   val fast_term_ord: term * term -> order
   167   val term_ord: term * term -> order
   168   val hd_ord: term * term -> order
   169   val termless: term * term -> bool
   170   val term_lpo: (term -> int) -> term * term -> order
   171   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   172   val rename_abs: term -> term -> term -> term option
   173   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   174   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   175   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   176   val var_ord: (indexname * typ) * (indexname * typ) -> order
   177   val maxidx_typ: typ -> int -> int
   178   val maxidx_typs: typ list -> int -> int
   179   val maxidx_term: term -> int -> int
   180   val dest_abs: string * typ * term -> string * term
   181   val declare_term_names: term -> Name.context -> Name.context
   182   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   183   val dummy_patternN: string
   184   val dummy_pattern: typ -> term
   185   val no_dummy_patterns: term -> term
   186   val replace_dummy_patterns: int * term -> int * term
   187   val is_replaced_dummy_pattern: indexname -> bool
   188   val show_dummy_patterns: term -> term
   189   val string_of_vname: indexname -> string
   190   val string_of_vname': indexname -> string
   191 end;
   192 
   193 structure Term: TERM =
   194 struct
   195 
   196 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   197   for resolution.*)
   198 type indexname = string * int;
   199 
   200 (* Types are classified by sorts. *)
   201 type class = string;
   202 type sort  = class list;
   203 type arity = string * sort list * sort;
   204 
   205 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   206 datatype typ = Type  of string * typ list
   207              | TFree of string * sort
   208              | TVar  of indexname * sort;
   209 
   210 (*Terms.  Bound variables are indicated by depth number.
   211   Free variables, (scheme) variables and constants have names.
   212   An term is "closed" if every bound variable of level "lev"
   213   is enclosed by at least "lev" abstractions.
   214 
   215   It is possible to create meaningless terms containing loose bound vars
   216   or type mismatches.  But such terms are not allowed in rules. *)
   217 
   218 datatype term =
   219     Const of string * typ
   220   | Free  of string * typ
   221   | Var   of indexname * typ
   222   | Bound of int
   223   | Abs   of string*typ*term
   224   | op $  of term*term;
   225 
   226 (*Errors involving type mismatches*)
   227 exception TYPE of string * typ list * term list;
   228 
   229 (*Errors errors involving terms*)
   230 exception TERM of string * term list;
   231 
   232 (*Note variable naming conventions!
   233     a,b,c: string
   234     f,g,h: functions (including terms of function type)
   235     i,j,m,n: int
   236     t,u: term
   237     v,w: indexnames
   238     x,y: any
   239     A,B,C: term (denoting formulae)
   240     T,U: typ
   241 *)
   242 
   243 
   244 (** Types **)
   245 
   246 (*dummy type for parsing and printing etc.*)
   247 val dummyT = Type ("dummy", []);
   248 
   249 fun no_dummyT typ =
   250   let
   251     fun check (T as Type ("dummy", _)) =
   252           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   253       | check (Type (_, Ts)) = List.app check Ts
   254       | check _ = ();
   255   in check typ; typ end;
   256 
   257 fun S --> T = Type("fun",[S,T]);
   258 
   259 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   260 val op ---> = Library.foldr (op -->);
   261 
   262 fun dest_Type (Type x) = x
   263   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   264 fun dest_TVar (TVar x) = x
   265   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   266 fun dest_TFree (TFree x) = x
   267   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   268 
   269 
   270 (** Discriminators **)
   271 
   272 fun is_Bound (Bound _) = true
   273   | is_Bound _         = false;
   274 
   275 fun is_Const (Const _) = true
   276   | is_Const _ = false;
   277 
   278 fun is_Free (Free _) = true
   279   | is_Free _ = false;
   280 
   281 fun is_Var (Var _) = true
   282   | is_Var _ = false;
   283 
   284 fun is_TVar (TVar _) = true
   285   | is_TVar _ = false;
   286 
   287 
   288 (** Destructors **)
   289 
   290 fun dest_Const (Const x) =  x
   291   | dest_Const t = raise TERM("dest_Const", [t]);
   292 
   293 fun dest_Free (Free x) =  x
   294   | dest_Free t = raise TERM("dest_Free", [t]);
   295 
   296 fun dest_Var (Var x) =  x
   297   | dest_Var t = raise TERM("dest_Var", [t]);
   298 
   299 
   300 fun domain_type (Type("fun", [T,_])) = T
   301 and range_type  (Type("fun", [_,T])) = T;
   302 
   303 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   304 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   305   | binder_types _   =  [];
   306 
   307 (* maps  [T1,...,Tn]--->T  to T*)
   308 fun body_type (Type("fun",[S,T])) = body_type T
   309   | body_type T   =  T;
   310 
   311 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   312 fun strip_type T : typ list * typ =
   313   (binder_types T, body_type T);
   314 
   315 
   316 (*Compute the type of the term, checking that combinations are well-typed
   317   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   318 fun type_of1 (Ts, Const (_,T)) = T
   319   | type_of1 (Ts, Free  (_,T)) = T
   320   | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
   321         handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   322   | type_of1 (Ts, Var (_,T)) = T
   323   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   324   | type_of1 (Ts, f$u) =
   325       let val U = type_of1(Ts,u)
   326           and T = type_of1(Ts,f)
   327       in case T of
   328             Type("fun",[T1,T2]) =>
   329               if T1=U then T2  else raise TYPE
   330                     ("type_of: type mismatch in application", [T1,U], [f$u])
   331           | _ => raise TYPE
   332                     ("type_of: function type is expected in application",
   333                      [T,U], [f$u])
   334       end;
   335 
   336 fun type_of t : typ = type_of1 ([],t);
   337 
   338 (*Determines the type of a term, with minimal checking*)
   339 fun fastype_of1 (Ts, f$u) =
   340     (case fastype_of1 (Ts,f) of
   341         Type("fun",[_,T]) => T
   342         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   343   | fastype_of1 (_, Const (_,T)) = T
   344   | fastype_of1 (_, Free (_,T)) = T
   345   | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
   346          handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   347   | fastype_of1 (_, Var (_,T)) = T
   348   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   349 
   350 fun fastype_of t : typ = fastype_of1 ([],t);
   351 
   352 (*Determine the argument type of a function*)
   353 fun argument_type_of tm =
   354   let
   355     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   356       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   357 
   358     fun arg 0 _ (Abs (_, T, _)) = T
   359       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   360       | arg i Ts (t $ _) = arg (i + 1) Ts t
   361       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   362   in arg 0 [] tm end;
   363 
   364 
   365 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
   366 
   367 fun strip_abs (Abs (a, T, t)) =
   368       let val (a', t') = strip_abs t
   369       in ((a, T) :: a', t') end
   370   | strip_abs t = ([], t);
   371 
   372 (* maps  (x1,...,xn)t   to   t  *)
   373 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   374   | strip_abs_body u  =  u;
   375 
   376 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   377 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   378   | strip_abs_vars u  =  [] : (string*typ) list;
   379 
   380 
   381 fun strip_qnt_body qnt =
   382 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   383       | strip t = t
   384 in strip end;
   385 
   386 fun strip_qnt_vars qnt =
   387 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   388       | strip t  =  [] : (string*typ) list
   389 in strip end;
   390 
   391 
   392 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   393 val list_comb : term * term list -> term = Library.foldl (op $);
   394 
   395 
   396 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   397 fun strip_comb u : term * term list =
   398     let fun stripc (f$t, ts) = stripc (f, t::ts)
   399         |   stripc  x =  x
   400     in  stripc(u,[])  end;
   401 
   402 
   403 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   404 fun head_of (f$t) = head_of f
   405   | head_of u = u;
   406 
   407 
   408 (*number of atoms and abstractions in a term*)
   409 fun size_of_term tm =
   410   let
   411     fun add_size (t $ u, n) = add_size (t, add_size (u, n))
   412       | add_size (Abs (_ ,_, t), n) = add_size (t, n + 1)
   413       | add_size (_, n) = n + 1;
   414   in add_size (tm, 0) end;
   415 
   416 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   417   | map_atyps f T = f T;
   418 
   419 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   420   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   421   | map_aterms f t = f t;
   422 
   423 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   424 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   425 
   426 fun map_types f =
   427   let
   428     fun map_aux (Const (a, T)) = Const (a, f T)
   429       | map_aux (Free (a, T)) = Free (a, f T)
   430       | map_aux (Var (v, T)) = Var (v, f T)
   431       | map_aux (t as Bound _)  = t
   432       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   433       | map_aux (t $ u) = map_aux t $ map_aux u;
   434   in map_aux end;
   435 
   436 (* iterate a function over all types in a term *)
   437 fun it_term_types f =
   438 let fun iter(Const(_,T), a) = f(T,a)
   439       | iter(Free(_,T), a) = f(T,a)
   440       | iter(Var(_,T), a) = f(T,a)
   441       | iter(Abs(_,T,t), a) = iter(t,f(T,a))
   442       | iter(f$u, a) = iter(f, iter(u, a))
   443       | iter(Bound _, a) = a
   444 in iter end
   445 
   446 
   447 (* fold types and terms *)
   448 
   449 (*fold atoms of type*)
   450 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   451   | fold_atyps f T = f T;
   452 
   453 (*fold atoms of term*)
   454 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   455   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   456   | fold_aterms f a = f a;
   457 
   458 (*fold types of term*)
   459 fun fold_term_types f (t as Const (_, T)) = f t T
   460   | fold_term_types f (t as Free (_, T)) = f t T
   461   | fold_term_types f (t as Var (_, T)) = f t T
   462   | fold_term_types f (Bound _) = I
   463   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   464   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   465 
   466 fun fold_types f = fold_term_types (K f);
   467 
   468 (*collect variables*)
   469 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   470 val add_tvars = fold_types add_tvarsT;
   471 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   472 val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   473 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   474 val add_tfrees = fold_types add_tfreesT;
   475 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   476 
   477 
   478 (** Comparing terms, types, sorts etc. **)
   479 
   480 (* alpha equivalence -- tuned for equalities *)
   481 
   482 fun tm1 aconv tm2 =
   483   pointer_eq (tm1, tm2) orelse
   484     (case (tm1, tm2) of
   485       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
   486     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
   487     | (a1, a2) => a1 = a2);
   488 
   489 
   490 (* fast syntactic ordering -- tuned for inequalities *)
   491 
   492 fun fast_indexname_ord ((x, i), (y, j)) =
   493   (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   494 
   495 fun sort_ord SS =
   496   if pointer_eq SS then EQUAL
   497   else dict_ord fast_string_ord SS;
   498 
   499 local
   500 
   501 fun cons_nr (TVar _) = 0
   502   | cons_nr (TFree _) = 1
   503   | cons_nr (Type _) = 2;
   504 
   505 in
   506 
   507 fun typ_ord TU =
   508   if pointer_eq TU then EQUAL
   509   else
   510     (case TU of
   511       (Type (a, Ts), Type (b, Us)) =>
   512         (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   513     | (TFree (a, S), TFree (b, S')) =>
   514         (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   515     | (TVar (xi, S), TVar (yj, S')) =>
   516         (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
   517     | (T, U) => int_ord (cons_nr T, cons_nr U));
   518 
   519 end;
   520 
   521 local
   522 
   523 fun cons_nr (Const _) = 0
   524   | cons_nr (Free _) = 1
   525   | cons_nr (Var _) = 2
   526   | cons_nr (Bound _) = 3
   527   | cons_nr (Abs _) = 4
   528   | cons_nr (_ $ _) = 5;
   529 
   530 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   531   | struct_ord (t1 $ t2, u1 $ u2) =
   532       (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   533   | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
   534 
   535 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   536   | atoms_ord (t1 $ t2, u1 $ u2) =
   537       (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   538   | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   539   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   540   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   541   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   542   | atoms_ord _ = sys_error "atoms_ord";
   543 
   544 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
   545       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   546   | types_ord (t1 $ t2, u1 $ u2) =
   547       (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   548   | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   549   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   550   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   551   | types_ord (Bound _, Bound _) = EQUAL
   552   | types_ord _ = sys_error "types_ord";
   553 
   554 in
   555 
   556 fun fast_term_ord tu =
   557   if pointer_eq tu then EQUAL
   558   else
   559     (case struct_ord tu of
   560       EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
   561     | ord => ord);
   562 
   563 structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
   564 structure Typtab = TableFun(type key = typ val ord = typ_ord);
   565 structure Termtab = TableFun(type key = term val ord = fast_term_ord);
   566 
   567 end;
   568 
   569 
   570 (* term_ord *)
   571 
   572 (*a linear well-founded AC-compatible ordering for terms:
   573   s < t <=> 1. size(s) < size(t) or
   574             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   575             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   576                (s1..sn) < (t1..tn) (lexicographically)*)
   577 
   578 fun indexname_ord ((x, i), (y, j)) =
   579   (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   580 
   581 local
   582 
   583 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
   584   | hd_depth p = p;
   585 
   586 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   587   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   588   | dest_hd (Var v) = (v, 2)
   589   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   590   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   591 
   592 in
   593 
   594 fun term_ord tu =
   595   if pointer_eq tu then EQUAL
   596   else
   597     (case tu of
   598       (Abs (_, T, t), Abs(_, U, u)) =>
   599         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   600     | (t, u) =>
   601         (case int_ord (size_of_term t, size_of_term u) of
   602           EQUAL =>
   603             (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
   604               EQUAL => args_ord (t, u) | ord => ord)
   605         | ord => ord))
   606 and hd_ord (f, g) =
   607   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   608 and args_ord (f $ t, g $ u) =
   609       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   610   | args_ord _ = EQUAL;
   611 
   612 fun termless tu = (term_ord tu = LESS);
   613 
   614 end;
   615 
   616 
   617 (** Lexicographic path order on terms **)
   618 
   619 (*
   620   See Baader & Nipkow, Term rewriting, CUP 1998.
   621   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   622   constants.
   623 
   624   f_ord maps terms to integers and serves two purposes:
   625   - Predicate on constant symbols.  Those that are not recognised by f_ord
   626     must be mapped to ~1.
   627   - Order on the recognised symbols.  These must be mapped to distinct
   628     integers >= 0.
   629   The argument of f_ord is never an application.
   630 *)
   631 
   632 local
   633 
   634 fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
   635   | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
   636   | unrecognized (Var v) = ((1, v), 1)
   637   | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
   638   | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
   639 
   640 fun dest_hd f_ord t =
   641       let val ord = f_ord t in
   642         if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
   643       end
   644 
   645 fun term_lpo f_ord (s, t) =
   646   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
   647     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
   648     then case hd_ord f_ord (f, g) of
   649         GREATER =>
   650           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   651           then GREATER else LESS
   652       | EQUAL =>
   653           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   654           then list_ord (term_lpo f_ord) (ss, ts)
   655           else LESS
   656       | LESS => LESS
   657     else GREATER
   658   end
   659 and hd_ord f_ord (f, g) = case (f, g) of
   660     (Abs (_, T, t), Abs (_, U, u)) =>
   661       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   662   | (_, _) => prod_ord (prod_ord int_ord
   663                   (prod_ord indexname_ord typ_ord)) int_ord
   664                 (dest_hd f_ord f, dest_hd f_ord g)
   665 in
   666 val term_lpo = term_lpo
   667 end;
   668 
   669 
   670 (** Connectives of higher order logic **)
   671 
   672 fun aT S = TFree ("'a", S);
   673 
   674 fun itselfT ty = Type ("itself", [ty]);
   675 val a_itselfT = itselfT (TFree ("'a", []));
   676 
   677 val propT : typ = Type("prop",[]);
   678 
   679 val implies = Const("==>", propT-->propT-->propT);
   680 
   681 fun all T = Const("all", (T-->propT)-->propT);
   682 
   683 fun equals T = Const("==", T-->T-->propT);
   684 
   685 (* maps  !!x1...xn. t   to   t  *)
   686 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   687   | strip_all_body t  =  t;
   688 
   689 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   690 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   691                 (a,T) :: strip_all_vars t
   692   | strip_all_vars t  =  [] : (string*typ) list;
   693 
   694 (*increments a term's non-local bound variables
   695   required when moving a term within abstractions
   696      inc is  increment for bound variables
   697      lev is  level at which a bound variable is considered 'loose'*)
   698 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   699   | incr_bv (inc, lev, Abs(a,T,body)) =
   700         Abs(a, T, incr_bv(inc,lev+1,body))
   701   | incr_bv (inc, lev, f$t) =
   702       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   703   | incr_bv (inc, lev, u) = u;
   704 
   705 fun incr_boundvars  0  t = t
   706   | incr_boundvars inc t = incr_bv(inc,0,t);
   707 
   708 (*Scan a pair of terms; while they are similar,
   709   accumulate corresponding bound vars in "al"*)
   710 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   711       match_bvs(s, t, if x="" orelse y="" then al
   712                                           else (x,y)::al)
   713   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   714   | match_bvs(_,_,al) = al;
   715 
   716 (* strip abstractions created by parameters *)
   717 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   718 
   719 fun rename_abs pat obj t =
   720   let
   721     val ren = match_bvs (pat, obj, []);
   722     fun ren_abs (Abs (x, T, b)) =
   723           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   724       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   725       | ren_abs t = t
   726   in if null ren then NONE else SOME (ren_abs t) end;
   727 
   728 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   729    (Bound 0) is loose at level 0 *)
   730 fun add_loose_bnos (Bound i, lev, js) =
   731         if i<lev then js else insert (op =) (i - lev) js
   732   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   733   | add_loose_bnos (f$t, lev, js) =
   734         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   735   | add_loose_bnos (_, _, js) = js;
   736 
   737 fun loose_bnos t = add_loose_bnos (t, 0, []);
   738 
   739 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   740    level k or beyond. *)
   741 fun loose_bvar(Bound i,k) = i >= k
   742   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   743   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   744   | loose_bvar _ = false;
   745 
   746 fun loose_bvar1(Bound i,k) = i = k
   747   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   748   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   749   | loose_bvar1 _ = false;
   750 
   751 (*Substitute arguments for loose bound variables.
   752   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   753   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   754         and the appropriate call is  subst_bounds([b,a], c) .
   755   Loose bound variables >=n are reduced by "n" to
   756      compensate for the disappearance of lambdas.
   757 *)
   758 fun subst_bounds (args: term list, t) : term =
   759   let
   760     exception SAME;
   761     val n = length args;
   762     fun subst (t as Bound i, lev) =
   763          (if i < lev then raise SAME   (*var is locally bound*)
   764           else incr_boundvars lev (List.nth (args, i - lev))
   765             handle Subscript => Bound (i - n))  (*loose: change it*)
   766       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   767       | subst (f $ t, lev) =
   768           (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
   769       | subst _ = raise SAME;
   770   in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
   771 
   772 (*Special case: one argument*)
   773 fun subst_bound (arg, t) : term =
   774   let
   775     exception SAME;
   776     fun subst (Bound i, lev) =
   777           if i < lev then raise SAME   (*var is locally bound*)
   778           else if i = lev then incr_boundvars lev arg
   779           else Bound (i - 1)   (*loose: change it*)
   780       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   781       | subst (f $ t, lev) =
   782           (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
   783       | subst _ = raise SAME;
   784   in subst (t, 0) handle SAME => t end;
   785 
   786 (*beta-reduce if possible, else form application*)
   787 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   788   | betapply (f,u) = f$u;
   789 
   790 val betapplys = Library.foldl betapply;
   791 
   792 
   793 (*unfolding abstractions with substitution
   794   of bound variables and implicit eta-expansion*)
   795 fun strip_abs_eta k t =
   796   let
   797     val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context;
   798     fun strip_abs t (0, used) = (([], t), (0, used))
   799       | strip_abs (Abs (v, T, t)) (k, used) =
   800           let
   801             val ([v'], used') = Name.variants [v] used;
   802             val t' = subst_bound (Free (v', T), t);
   803             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   804           in (((v', T) :: vs, t''), (k', used'')) end
   805       | strip_abs t (k, used) = (([], t), (k, used));
   806     fun expand_eta [] t _ = ([], t)
   807       | expand_eta (T::Ts) t used =
   808           let
   809             val ([v], used') = Name.variants [""] used;
   810             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   811           in ((v, T) :: vs, t') end;
   812     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   813     val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
   814     val (vs2, t'') = expand_eta Ts t' used';
   815   in (vs1 @ vs2, t'') end;
   816 
   817 
   818 (* comparing variables *)
   819 
   820 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   821 
   822 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   823 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   824 
   825 val tvar_ord = prod_ord indexname_ord sort_ord;
   826 val var_ord = prod_ord indexname_ord typ_ord;
   827 
   828 
   829 (*A fast unification filter: true unless the two terms cannot be unified.
   830   Terms must be NORMAL.  Treats all Vars as distinct. *)
   831 fun could_unify (t,u) =
   832   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   833         | matchrands _ = true
   834   in case (head_of t , head_of u) of
   835         (_, Var _) => true
   836       | (Var _, _) => true
   837       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   838       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   839       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   840       | (Abs _, _) =>  true   (*because of possible eta equality*)
   841       | (_, Abs _) =>  true
   842       | _ => false
   843   end;
   844 
   845 (*Substitute new for free occurrences of old in a term*)
   846 fun subst_free [] = (fn t=>t)
   847   | subst_free pairs =
   848       let fun substf u =
   849             case AList.lookup (op aconv) pairs u of
   850                 SOME u' => u'
   851               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   852                                  | t$u' => substf t $ substf u'
   853                                  | _ => u)
   854       in  substf  end;
   855 
   856 (*Abstraction of the term "body" over its occurrences of v,
   857     which must contain no loose bound variables.
   858   The resulting term is ready to become the body of an Abs.*)
   859 fun abstract_over (v, body) =
   860   let
   861     exception SAME;
   862     fun abs lev tm =
   863       if v aconv tm then Bound lev
   864       else
   865         (case tm of
   866           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   867         | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
   868         | _ => raise SAME);
   869   in abs 0 body handle SAME => body end;
   870 
   871 fun lambda (v as Const (x, T)) t = Abs (NameSpace.base x, T, abstract_over (v, t))
   872   | lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   873   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
   874   | lambda v t = raise TERM ("lambda", [v, t]);
   875 
   876 (*Form an abstraction over a free variable.*)
   877 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
   878 fun absdummy (T, body) = Abs ("uu", T, body);
   879 
   880 (*Abstraction over a list of free variables*)
   881 fun list_abs_free ([ ] ,     t) = t
   882   | list_abs_free ((a,T)::vars, t) =
   883       absfree(a, T, list_abs_free(vars,t));
   884 
   885 (*Quantification over a list of free variables*)
   886 fun list_all_free ([], t: term) = t
   887   | list_all_free ((a,T)::vars, t) =
   888         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   889 
   890 (*Quantification over a list of variables (already bound in body) *)
   891 fun list_all ([], t) = t
   892   | list_all ((a,T)::vars, t) =
   893         (all T) $ (Abs(a, T, list_all(vars,t)));
   894 
   895 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   896   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   897 fun subst_atomic [] tm = tm
   898   | subst_atomic inst tm =
   899       let
   900         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   901           | subst (t $ u) = subst t $ subst u
   902           | subst t = the_default t (AList.lookup (op aconv) inst t);
   903       in subst tm end;
   904 
   905 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   906 fun typ_subst_atomic [] ty = ty
   907   | typ_subst_atomic inst ty =
   908       let
   909         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   910           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   911       in subst ty end;
   912 
   913 fun subst_atomic_types [] tm = tm
   914   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   915 
   916 fun typ_subst_TVars [] ty = ty
   917   | typ_subst_TVars inst ty =
   918       let
   919         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   920           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   921           | subst T = T;
   922       in subst ty end;
   923 
   924 fun subst_TVars [] tm = tm
   925   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   926 
   927 fun subst_Vars [] tm = tm
   928   | subst_Vars inst tm =
   929       let
   930         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   931           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   932           | subst (t $ u) = subst t $ subst u
   933           | subst t = t;
   934       in subst tm end;
   935 
   936 fun subst_vars ([], []) tm = tm
   937   | subst_vars ([], inst) tm = subst_Vars inst tm
   938   | subst_vars (instT, inst) tm =
   939       let
   940         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   941           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   942           | subst (t as Var (xi, T)) =
   943               (case AList.lookup (op =) inst xi of
   944                 NONE => Var (xi, typ_subst_TVars instT T)
   945               | SOME t => t)
   946           | subst (t as Bound _) = t
   947           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   948           | subst (t $ u) = subst t $ subst u;
   949       in subst tm end;
   950 
   951 
   952 (** Identifying first-order terms **)
   953 
   954 (*Differs from proofterm/is_fun in its treatment of TVar*)
   955 fun is_funtype (Type("fun",[_,_])) = true
   956   | is_funtype _ = false;
   957 
   958 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   959 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
   960 
   961 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   962   function type. The supplied quantifiers are excluded: their argument always
   963   has a function type through a recursive call into its body.*)
   964 fun is_first_order quants =
   965   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   966         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   967             member (op =) quants q  andalso   (*it is a known quantifier*)
   968             not (is_funtype T)   andalso first_order1 (T::Ts) body
   969         | first_order1 Ts t =
   970             case strip_comb t of
   971                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   972                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   973                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   974                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   975                | (Abs _, ts) => false (*not in beta-normal form*)
   976                | _ => error "first_order: unexpected case"
   977     in  first_order1 []  end;
   978 
   979 
   980 (* maximum index of typs and terms *)
   981 
   982 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   983   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   984   | maxidx_typ (TFree _) i = i
   985 and maxidx_typs [] i = i
   986   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
   987 
   988 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   989   | maxidx_term (Const (_, T)) i = maxidx_typ T i
   990   | maxidx_term (Free (_, T)) i = maxidx_typ T i
   991   | maxidx_term (Bound _) i = i
   992   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   993   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
   994 
   995 fun maxidx_of_typ T = maxidx_typ T ~1;
   996 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
   997 fun maxidx_of_term t = maxidx_term t ~1;
   998 
   999 
  1000 
  1001 (**** Syntax-related declarations ****)
  1002 
  1003 (* substructure *)
  1004 
  1005 fun exists_subtype P =
  1006   let
  1007     fun ex ty = P ty orelse
  1008       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
  1009   in ex end;
  1010 
  1011 fun exists_type P =
  1012   let
  1013     fun ex (Const (_, T)) = P T
  1014       | ex (Free (_, T)) = P T
  1015       | ex (Var (_, T)) = P T
  1016       | ex (Bound _) = false
  1017       | ex (Abs (_, T, t)) = P T orelse ex t
  1018       | ex (t $ u) = ex t orelse ex u;
  1019   in ex end;
  1020 
  1021 fun exists_subterm P =
  1022   let
  1023     fun ex tm = P tm orelse
  1024       (case tm of
  1025         t $ u => ex t orelse ex u
  1026       | Abs (_, _, t) => ex t
  1027       | _ => false);
  1028   in ex end;
  1029 
  1030 
  1031 (** Consts etc. **)
  1032 
  1033 fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
  1034   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
  1035   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
  1036   | add_term_consts (_, cs) = cs;
  1037 
  1038 fun term_consts t = add_term_consts(t,[]);
  1039 
  1040 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
  1041 
  1042 
  1043 (** TFrees and TVars **)
  1044 
  1045 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
  1046 fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
  1047   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  1048   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  1049   | add_term_free_names (_, bs) = bs;
  1050 
  1051 (*Accumulates the names in the term, suppressing duplicates.
  1052   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  1053 fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
  1054   | add_term_names (Free(a,_), bs) = insert (op =) a bs
  1055   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  1056   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  1057   | add_term_names (_, bs) = bs;
  1058 
  1059 (*Accumulates the TVars in a type, suppressing duplicates. *)
  1060 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
  1061   | add_typ_tvars(TFree(_),vs) = vs
  1062   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  1063 
  1064 (*Accumulates the TFrees in a type, suppressing duplicates. *)
  1065 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
  1066   | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
  1067   | add_typ_tfree_names(TVar(_),fs) = fs;
  1068 
  1069 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
  1070   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  1071   | add_typ_tfrees(TVar(_),fs) = fs;
  1072 
  1073 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
  1074   | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
  1075   | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
  1076 
  1077 (*Accumulates the TVars in a term, suppressing duplicates. *)
  1078 val add_term_tvars = it_term_types add_typ_tvars;
  1079 
  1080 (*Accumulates the TFrees in a term, suppressing duplicates. *)
  1081 val add_term_tfrees = it_term_types add_typ_tfrees;
  1082 val add_term_tfree_names = it_term_types add_typ_tfree_names;
  1083 
  1084 (*Non-list versions*)
  1085 fun typ_tfrees T = add_typ_tfrees(T,[]);
  1086 fun typ_tvars T = add_typ_tvars(T,[]);
  1087 fun term_tfrees t = add_term_tfrees(t,[]);
  1088 fun term_tvars t = add_term_tvars(t,[]);
  1089 
  1090 (*special code to enforce left-to-right collection of TVar-indexnames*)
  1091 
  1092 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
  1093   | add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
  1094                                      else ixns@[ixn]
  1095   | add_typ_ixns(ixns,TFree(_)) = ixns;
  1096 
  1097 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1098   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1099   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1100   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1101   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1102       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1103   | add_term_tvar_ixns(f$t,ixns) =
  1104       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1105 
  1106 
  1107 (** Frees and Vars **)
  1108 
  1109 (*Accumulates the Vars in the term, suppressing duplicates*)
  1110 fun add_term_vars (t, vars: term list) = case t of
  1111     Var   _ => OrdList.insert term_ord t vars
  1112   | Abs (_,_,body) => add_term_vars(body,vars)
  1113   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1114   | _ => vars;
  1115 
  1116 fun term_vars t = add_term_vars(t,[]);
  1117 
  1118 (*Accumulates the Frees in the term, suppressing duplicates*)
  1119 fun add_term_frees (t, frees: term list) = case t of
  1120     Free   _ => OrdList.insert term_ord t frees
  1121   | Abs (_,_,body) => add_term_frees(body,frees)
  1122   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1123   | _ => frees;
  1124 
  1125 fun term_frees t = add_term_frees(t,[]);
  1126 
  1127 
  1128 (* dest abstraction *)
  1129 
  1130 fun dest_abs (x, T, body) =
  1131   let
  1132     fun name_clash (Free (y, _)) = (x = y)
  1133       | name_clash (t $ u) = name_clash t orelse name_clash u
  1134       | name_clash (Abs (_, _, t)) = name_clash t
  1135       | name_clash _ = false;
  1136   in
  1137     if name_clash body then
  1138       dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
  1139     else (x, subst_bound (Free (x, T), body))
  1140   end;
  1141 
  1142 
  1143 (* renaming variables *)
  1144 
  1145 fun declare_term_names tm =
  1146   fold_aterms
  1147     (fn Const (a, _) => Name.declare (NameSpace.base a)
  1148       | Free (a, _) => Name.declare a
  1149       | _ => I) tm #>
  1150   fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
  1151 
  1152 fun variant_frees t frees =
  1153   fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
  1154 
  1155 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
  1156 
  1157 
  1158 (* dummy patterns *)
  1159 
  1160 val dummy_patternN = "dummy_pattern";
  1161 
  1162 fun dummy_pattern T = Const (dummy_patternN, T);
  1163 
  1164 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1165   | is_dummy_pattern _ = false;
  1166 
  1167 fun no_dummy_patterns tm =
  1168   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  1169   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1170 
  1171 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
  1172       (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
  1173   | replace_dummy Ts (i, Abs (x, T, t)) =
  1174       let val (i', t') = replace_dummy (T :: Ts) (i, t)
  1175       in (i', Abs (x, T, t')) end
  1176   | replace_dummy Ts (i, t $ u) =
  1177       let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
  1178       in (i'', t' $ u') end
  1179   | replace_dummy _ (i, a) = (i, a);
  1180 
  1181 val replace_dummy_patterns = replace_dummy [];
  1182 
  1183 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1184   | is_replaced_dummy_pattern _ = false;
  1185 
  1186 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1187   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1188   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1189   | show_dummy_patterns a = a;
  1190 
  1191 
  1192 (* display variables *)
  1193 
  1194 val show_question_marks = ref true;
  1195 
  1196 fun string_of_vname (x, i) =
  1197   let
  1198     val question_mark = if ! show_question_marks then "?" else "";
  1199     val idx = string_of_int i;
  1200     val dot =
  1201       (case rev (Symbol.explode x) of
  1202         _ :: "\\<^isub>" :: _ => false
  1203       | _ :: "\\<^isup>" :: _ => false
  1204       | c :: _ => Symbol.is_digit c
  1205       | _ => true);
  1206   in
  1207     if dot then question_mark ^ x ^ "." ^ idx
  1208     else if i <> 0 then question_mark ^ x ^ idx
  1209     else question_mark ^ x
  1210   end;
  1211 
  1212 fun string_of_vname' (x, ~1) = x
  1213   | string_of_vname' xi = string_of_vname xi;
  1214 
  1215 end;
  1216 
  1217 structure BasicTerm: BASIC_TERM = Term;
  1218 open BasicTerm;