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