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