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