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