src/Pure/term.ML
author wenzelm
Thu Oct 11 19:10:24 2007 +0200 (2007-10-11)
changeset 24982 f2f0722675b1
parent 24850 0cfd722ab579
child 25050 0dc445970b4b
permissions -rw-r--r--
replaced Term.equiv_types by Type.similar_types;
     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 strip_abs_eta: int -> term -> (string * typ) list * term
   166   val fast_indexname_ord: indexname * indexname -> order
   167   val indexname_ord: indexname * indexname -> order
   168   val sort_ord: sort * sort -> order
   169   val typ_ord: typ * typ -> order
   170   val fast_term_ord: term * term -> order
   171   val term_ord: term * term -> order
   172   val hd_ord: term * term -> order
   173   val termless: term * term -> bool
   174   val term_lpo: (term -> int) -> term * term -> order
   175   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   176   val map_abs_vars: (string -> string) -> term -> term
   177   val rename_abs: term -> term -> term -> term option
   178   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   179   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   180   val tvar_ord: (indexname * sort) * (indexname * sort) -> order
   181   val var_ord: (indexname * typ) * (indexname * typ) -> order
   182   val maxidx_typ: typ -> int -> int
   183   val maxidx_typs: typ list -> int -> int
   184   val maxidx_term: term -> int -> int
   185   val has_abs: term -> bool
   186   val dest_abs: string * typ * term -> string * term
   187   val declare_typ_names: typ -> Name.context -> Name.context
   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: term -> int -> term * int
   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 (* fast syntactic ordering -- tuned for inequalities *)
   538 
   539 fun fast_indexname_ord ((x, i), (y, j)) =
   540   (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
   541 
   542 fun sort_ord SS =
   543   if pointer_eq SS then EQUAL
   544   else dict_ord fast_string_ord SS;
   545 
   546 local
   547 
   548 fun cons_nr (TVar _) = 0
   549   | cons_nr (TFree _) = 1
   550   | cons_nr (Type _) = 2;
   551 
   552 in
   553 
   554 fun typ_ord TU =
   555   if pointer_eq TU then EQUAL
   556   else
   557     (case TU of
   558       (Type (a, Ts), Type (b, Us)) =>
   559         (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
   560     | (TFree (a, S), TFree (b, S')) =>
   561         (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
   562     | (TVar (xi, S), TVar (yj, S')) =>
   563         (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
   564     | (T, U) => int_ord (cons_nr T, cons_nr U));
   565 
   566 end;
   567 
   568 local
   569 
   570 fun cons_nr (Const _) = 0
   571   | cons_nr (Free _) = 1
   572   | cons_nr (Var _) = 2
   573   | cons_nr (Bound _) = 3
   574   | cons_nr (Abs _) = 4
   575   | cons_nr (_ $ _) = 5;
   576 
   577 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   578   | struct_ord (t1 $ t2, u1 $ u2) =
   579       (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   580   | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
   581 
   582 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   583   | atoms_ord (t1 $ t2, u1 $ u2) =
   584       (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   585   | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   586   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   587   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   588   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   589   | atoms_ord _ = sys_error "atoms_ord";
   590 
   591 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
   592       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   593   | types_ord (t1 $ t2, u1 $ u2) =
   594       (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   595   | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   596   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   597   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   598   | types_ord (Bound _, Bound _) = EQUAL
   599   | types_ord _ = sys_error "types_ord";
   600 
   601 in
   602 
   603 fun fast_term_ord tu =
   604   if pointer_eq tu then EQUAL
   605   else
   606     (case struct_ord tu of
   607       EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
   608     | ord => ord);
   609 
   610 structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
   611 structure Typtab = TableFun(type key = typ val ord = typ_ord);
   612 structure Termtab = TableFun(type key = term val ord = fast_term_ord);
   613 
   614 end;
   615 
   616 
   617 (* term_ord *)
   618 
   619 (*a linear well-founded AC-compatible ordering for terms:
   620   s < t <=> 1. size(s) < size(t) or
   621             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
   622             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   623                (s1..sn) < (t1..tn) (lexicographically)*)
   624 
   625 fun indexname_ord ((x, i), (y, j)) =
   626   (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
   627 
   628 local
   629 
   630 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
   631   | hd_depth p = p;
   632 
   633 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   634   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   635   | dest_hd (Var v) = (v, 2)
   636   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   637   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
   638 
   639 in
   640 
   641 fun term_ord tu =
   642   if pointer_eq tu then EQUAL
   643   else
   644     (case tu of
   645       (Abs (_, T, t), Abs(_, U, u)) =>
   646         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   647     | (t, u) =>
   648         (case int_ord (size_of_term t, size_of_term u) of
   649           EQUAL =>
   650             (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
   651               EQUAL => args_ord (t, u) | ord => ord)
   652         | ord => ord))
   653 and hd_ord (f, g) =
   654   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
   655 and args_ord (f $ t, g $ u) =
   656       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   657   | args_ord _ = EQUAL;
   658 
   659 fun termless tu = (term_ord tu = LESS);
   660 
   661 end;
   662 
   663 
   664 (** Lexicographic path order on terms **)
   665 
   666 (*
   667   See Baader & Nipkow, Term rewriting, CUP 1998.
   668   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   669   constants.
   670 
   671   f_ord maps terms to integers and serves two purposes:
   672   - Predicate on constant symbols.  Those that are not recognised by f_ord
   673     must be mapped to ~1.
   674   - Order on the recognised symbols.  These must be mapped to distinct
   675     integers >= 0.
   676   The argument of f_ord is never an application.
   677 *)
   678 
   679 local
   680 
   681 fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
   682   | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
   683   | unrecognized (Var v) = ((1, v), 1)
   684   | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
   685   | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
   686 
   687 fun dest_hd f_ord t =
   688       let val ord = f_ord t in
   689         if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
   690       end
   691 
   692 fun term_lpo f_ord (s, t) =
   693   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
   694     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
   695     then case hd_ord f_ord (f, g) of
   696         GREATER =>
   697           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   698           then GREATER else LESS
   699       | EQUAL =>
   700           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
   701           then list_ord (term_lpo f_ord) (ss, ts)
   702           else LESS
   703       | LESS => LESS
   704     else GREATER
   705   end
   706 and hd_ord f_ord (f, g) = case (f, g) of
   707     (Abs (_, T, t), Abs (_, U, u)) =>
   708       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   709   | (_, _) => prod_ord (prod_ord int_ord
   710                   (prod_ord indexname_ord typ_ord)) int_ord
   711                 (dest_hd f_ord f, dest_hd f_ord g)
   712 in
   713 val term_lpo = term_lpo
   714 end;
   715 
   716 
   717 (** Connectives of higher order logic **)
   718 
   719 fun aT S = TFree (Name.aT, S);
   720 
   721 fun itselfT ty = Type ("itself", [ty]);
   722 val a_itselfT = itselfT (TFree (Name.aT, []));
   723 
   724 val propT : typ = Type("prop",[]);
   725 
   726 val implies = Const("==>", propT-->propT-->propT);
   727 
   728 fun all T = Const("all", (T-->propT)-->propT);
   729 
   730 fun equals T = Const("==", T-->T-->propT);
   731 
   732 (* maps  !!x1...xn. t   to   t  *)
   733 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   734   | strip_all_body t  =  t;
   735 
   736 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   737 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   738                 (a,T) :: strip_all_vars t
   739   | strip_all_vars t  =  [] : (string*typ) list;
   740 
   741 (*increments a term's non-local bound variables
   742   required when moving a term within abstractions
   743      inc is  increment for bound variables
   744      lev is  level at which a bound variable is considered 'loose'*)
   745 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   746   | incr_bv (inc, lev, Abs(a,T,body)) =
   747         Abs(a, T, incr_bv(inc,lev+1,body))
   748   | incr_bv (inc, lev, f$t) =
   749       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   750   | incr_bv (inc, lev, u) = u;
   751 
   752 fun incr_boundvars  0  t = t
   753   | incr_boundvars inc t = incr_bv(inc,0,t);
   754 
   755 (*Scan a pair of terms; while they are similar,
   756   accumulate corresponding bound vars in "al"*)
   757 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   758       match_bvs(s, t, if x="" orelse y="" then al
   759                                           else (x,y)::al)
   760   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   761   | match_bvs(_,_,al) = al;
   762 
   763 (* strip abstractions created by parameters *)
   764 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   765 
   766 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   767   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   768   | map_abs_vars f t = t;
   769 
   770 fun rename_abs pat obj t =
   771   let
   772     val ren = match_bvs (pat, obj, []);
   773     fun ren_abs (Abs (x, T, b)) =
   774           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   775       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   776       | ren_abs t = t
   777   in if null ren then NONE else SOME (ren_abs t) end;
   778 
   779 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   780    (Bound 0) is loose at level 0 *)
   781 fun add_loose_bnos (Bound i, lev, js) =
   782         if i<lev then js else insert (op =) (i - lev) js
   783   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   784   | add_loose_bnos (f$t, lev, js) =
   785         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   786   | add_loose_bnos (_, _, js) = js;
   787 
   788 fun loose_bnos t = add_loose_bnos (t, 0, []);
   789 
   790 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   791    level k or beyond. *)
   792 fun loose_bvar(Bound i,k) = i >= k
   793   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   794   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   795   | loose_bvar _ = false;
   796 
   797 fun loose_bvar1(Bound i,k) = i = k
   798   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   799   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   800   | loose_bvar1 _ = false;
   801 
   802 (*Substitute arguments for loose bound variables.
   803   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   804   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   805         and the appropriate call is  subst_bounds([b,a], c) .
   806   Loose bound variables >=n are reduced by "n" to
   807      compensate for the disappearance of lambdas.
   808 *)
   809 fun subst_bounds (args: term list, t) : term =
   810   let
   811     exception SAME;
   812     val n = length args;
   813     fun subst (t as Bound i, lev) =
   814          (if i < lev then raise SAME   (*var is locally bound*)
   815           else incr_boundvars lev (List.nth (args, i - lev))
   816             handle Subscript => Bound (i - n))  (*loose: change it*)
   817       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   818       | subst (f $ t, lev) =
   819           (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
   820       | subst _ = raise SAME;
   821   in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
   822 
   823 (*Special case: one argument*)
   824 fun subst_bound (arg, t) : term =
   825   let
   826     exception SAME;
   827     fun subst (Bound i, lev) =
   828           if i < lev then raise SAME   (*var is locally bound*)
   829           else if i = lev then incr_boundvars lev arg
   830           else Bound (i - 1)   (*loose: change it*)
   831       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   832       | subst (f $ t, lev) =
   833           (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
   834       | subst _ = raise SAME;
   835   in subst (t, 0) handle SAME => t end;
   836 
   837 (*beta-reduce if possible, else form application*)
   838 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   839   | betapply (f,u) = f$u;
   840 
   841 val betapplys = Library.foldl betapply;
   842 
   843 
   844 (*unfolding abstractions with substitution
   845   of bound variables and implicit eta-expansion*)
   846 fun strip_abs_eta k t =
   847   let
   848     val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context;
   849     fun strip_abs t (0, used) = (([], t), (0, used))
   850       | strip_abs (Abs (v, T, t)) (k, used) =
   851           let
   852             val ([v'], used') = Name.variants [v] used;
   853             val t' = subst_bound (Free (v', T), t);
   854             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   855           in (((v', T) :: vs, t''), (k', used'')) end
   856       | strip_abs t (k, used) = (([], t), (k, used));
   857     fun expand_eta [] t _ = ([], t)
   858       | expand_eta (T::Ts) t used =
   859           let
   860             val ([v], used') = Name.variants [""] used;
   861             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   862           in ((v, T) :: vs, t') end;
   863     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   864     val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
   865     val (vs2, t'') = expand_eta Ts t' used';
   866   in (vs1 @ vs2, t'') end;
   867 
   868 
   869 (* comparing variables *)
   870 
   871 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   872 
   873 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   874 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   875 
   876 val tvar_ord = prod_ord indexname_ord sort_ord;
   877 val var_ord = prod_ord indexname_ord typ_ord;
   878 
   879 
   880 (*A fast unification filter: true unless the two terms cannot be unified.
   881   Terms must be NORMAL.  Treats all Vars as distinct. *)
   882 fun could_unify (t,u) =
   883   let fun matchrands (f$t, g$u) = could_unify(t,u) andalso  matchrands(f,g)
   884         | matchrands _ = true
   885   in case (head_of t , head_of u) of
   886         (_, Var _) => true
   887       | (Var _, _) => true
   888       | (Const(a,_), Const(b,_)) =>  a=b andalso matchrands(t,u)
   889       | (Free(a,_), Free(b,_)) =>  a=b andalso matchrands(t,u)
   890       | (Bound i, Bound j) =>  i=j andalso matchrands(t,u)
   891       | (Abs _, _) =>  true   (*because of possible eta equality*)
   892       | (_, Abs _) =>  true
   893       | _ => false
   894   end;
   895 
   896 (*Substitute new for free occurrences of old in a term*)
   897 fun subst_free [] = (fn t=>t)
   898   | subst_free pairs =
   899       let fun substf u =
   900             case AList.lookup (op aconv) pairs u of
   901                 SOME u' => u'
   902               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   903                                  | t$u' => substf t $ substf u'
   904                                  | _ => u)
   905       in  substf  end;
   906 
   907 (*Abstraction of the term "body" over its occurrences of v,
   908     which must contain no loose bound variables.
   909   The resulting term is ready to become the body of an Abs.*)
   910 fun abstract_over (v, body) =
   911   let
   912     exception SAME;
   913     fun abs lev tm =
   914       if v aconv tm then Bound lev
   915       else
   916         (case tm of
   917           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   918         | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
   919         | _ => raise SAME);
   920   in abs 0 body handle SAME => body end;
   921 
   922 fun lambda v t =
   923   let val x =
   924     (case v of
   925       Const (x, _) => NameSpace.base x
   926     | Free (x, _) => x
   927     | Var ((x, _), _) => x
   928     | _ => Name.uu)
   929   in Abs (x, fastype_of v, abstract_over (v, t)) end;
   930 
   931 (*Form an abstraction over a free variable.*)
   932 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
   933 fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body);
   934 
   935 (*Abstraction over a list of free variables*)
   936 fun list_abs_free ([ ] ,     t) = t
   937   | list_abs_free ((a,T)::vars, t) =
   938       absfree(a, T, list_abs_free(vars,t));
   939 
   940 (*Quantification over a list of free variables*)
   941 fun list_all_free ([], t: term) = t
   942   | list_all_free ((a,T)::vars, t) =
   943         (all T) $ (absfree(a, T, list_all_free(vars,t)));
   944 
   945 (*Quantification over a list of variables (already bound in body) *)
   946 fun list_all ([], t) = t
   947   | list_all ((a,T)::vars, t) =
   948         (all T) $ (Abs(a, T, list_all(vars,t)));
   949 
   950 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   951   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   952 fun subst_atomic [] tm = tm
   953   | subst_atomic inst tm =
   954       let
   955         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   956           | subst (t $ u) = subst t $ subst u
   957           | subst t = the_default t (AList.lookup (op aconv) inst t);
   958       in subst tm end;
   959 
   960 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   961 fun typ_subst_atomic [] ty = ty
   962   | typ_subst_atomic inst ty =
   963       let
   964         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   965           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   966       in subst ty end;
   967 
   968 fun subst_atomic_types [] tm = tm
   969   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   970 
   971 fun typ_subst_TVars [] ty = ty
   972   | typ_subst_TVars inst ty =
   973       let
   974         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   975           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   976           | subst T = T;
   977       in subst ty end;
   978 
   979 fun subst_TVars [] tm = tm
   980   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   981 
   982 fun subst_Vars [] tm = tm
   983   | subst_Vars inst tm =
   984       let
   985         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   986           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   987           | subst (t $ u) = subst t $ subst u
   988           | subst t = t;
   989       in subst tm end;
   990 
   991 fun subst_vars ([], []) tm = tm
   992   | subst_vars ([], inst) tm = subst_Vars inst tm
   993   | subst_vars (instT, inst) tm =
   994       let
   995         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   996           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   997           | subst (t as Var (xi, T)) =
   998               (case AList.lookup (op =) inst xi of
   999                 NONE => Var (xi, typ_subst_TVars instT T)
  1000               | SOME t => t)
  1001           | subst (t as Bound _) = t
  1002           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
  1003           | subst (t $ u) = subst t $ subst u;
  1004       in subst tm end;
  1005 
  1006 
  1007 (** Identifying first-order terms **)
  1008 
  1009 (*Differs from proofterm/is_fun in its treatment of TVar*)
  1010 fun is_funtype (Type("fun",[_,_])) = true
  1011   | is_funtype _ = false;
  1012 
  1013 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
  1014 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
  1015 
  1016 (*First order means in all terms of the form f(t1,...,tn) no argument has a
  1017   function type. The supplied quantifiers are excluded: their argument always
  1018   has a function type through a recursive call into its body.*)
  1019 fun is_first_order quants =
  1020   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
  1021         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
  1022             member (op =) quants q  andalso   (*it is a known quantifier*)
  1023             not (is_funtype T)   andalso first_order1 (T::Ts) body
  1024         | first_order1 Ts t =
  1025             case strip_comb t of
  1026                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1027                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1028                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1029                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
  1030                | (Abs _, ts) => false (*not in beta-normal form*)
  1031                | _ => error "first_order: unexpected case"
  1032     in  first_order1 []  end;
  1033 
  1034 
  1035 (* maximum index of typs and terms *)
  1036 
  1037 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
  1038   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
  1039   | maxidx_typ (TFree _) i = i
  1040 and maxidx_typs [] i = i
  1041   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
  1042 
  1043 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
  1044   | maxidx_term (Const (_, T)) i = maxidx_typ T i
  1045   | maxidx_term (Free (_, T)) i = maxidx_typ T i
  1046   | maxidx_term (Bound _) i = i
  1047   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
  1048   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
  1049 
  1050 fun maxidx_of_typ T = maxidx_typ T ~1;
  1051 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
  1052 fun maxidx_of_term t = maxidx_term t ~1;
  1053 
  1054 
  1055 
  1056 (**** Syntax-related declarations ****)
  1057 
  1058 (* substructure *)
  1059 
  1060 fun exists_subtype P =
  1061   let
  1062     fun ex ty = P ty orelse
  1063       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
  1064   in ex end;
  1065 
  1066 fun exists_type P =
  1067   let
  1068     fun ex (Const (_, T)) = P T
  1069       | ex (Free (_, T)) = P T
  1070       | ex (Var (_, T)) = P T
  1071       | ex (Bound _) = false
  1072       | ex (Abs (_, T, t)) = P T orelse ex t
  1073       | ex (t $ u) = ex t orelse ex u;
  1074   in ex end;
  1075 
  1076 fun exists_subterm P =
  1077   let
  1078     fun ex tm = P tm orelse
  1079       (case tm of
  1080         t $ u => ex t orelse ex u
  1081       | Abs (_, _, t) => ex t
  1082       | _ => false);
  1083   in ex end;
  1084 
  1085 fun has_abs (Abs _) = true
  1086   | has_abs (t $ u) = has_abs t orelse has_abs u
  1087   | has_abs _ = false;
  1088 
  1089 
  1090 
  1091 (** Consts etc. **)
  1092 
  1093 fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
  1094   | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
  1095   | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
  1096   | add_term_consts (_, cs) = cs;
  1097 
  1098 fun term_consts t = add_term_consts(t,[]);
  1099 
  1100 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
  1101 
  1102 
  1103 (** TFrees and TVars **)
  1104 
  1105 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
  1106 fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
  1107   | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
  1108   | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
  1109   | add_term_free_names (_, bs) = bs;
  1110 
  1111 (*Accumulates the names in the term, suppressing duplicates.
  1112   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
  1113 fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
  1114   | add_term_names (Free(a,_), bs) = insert (op =) a bs
  1115   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
  1116   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
  1117   | add_term_names (_, bs) = bs;
  1118 
  1119 (*Accumulates the TVars in a type, suppressing duplicates. *)
  1120 fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
  1121   | add_typ_tvars(TFree(_),vs) = vs
  1122   | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
  1123 
  1124 (*Accumulates the TFrees in a type, suppressing duplicates. *)
  1125 fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
  1126   | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
  1127   | add_typ_tfree_names(TVar(_),fs) = fs;
  1128 
  1129 fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
  1130   | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
  1131   | add_typ_tfrees(TVar(_),fs) = fs;
  1132 
  1133 fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
  1134   | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
  1135   | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
  1136 
  1137 (*Accumulates the TVars in a term, suppressing duplicates. *)
  1138 val add_term_tvars = it_term_types add_typ_tvars;
  1139 
  1140 (*Accumulates the TFrees in a term, suppressing duplicates. *)
  1141 val add_term_tfrees = it_term_types add_typ_tfrees;
  1142 val add_term_tfree_names = it_term_types add_typ_tfree_names;
  1143 
  1144 (*Non-list versions*)
  1145 fun typ_tfrees T = add_typ_tfrees(T,[]);
  1146 fun typ_tvars T = add_typ_tvars(T,[]);
  1147 fun term_tfrees t = add_term_tfrees(t,[]);
  1148 fun term_tvars t = add_term_tvars(t,[]);
  1149 
  1150 (*special code to enforce left-to-right collection of TVar-indexnames*)
  1151 
  1152 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
  1153   | add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
  1154                                      else ixns@[ixn]
  1155   | add_typ_ixns(ixns,TFree(_)) = ixns;
  1156 
  1157 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
  1158   | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
  1159   | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
  1160   | add_term_tvar_ixns(Bound _,ixns) = ixns
  1161   | add_term_tvar_ixns(Abs(_,T,t),ixns) =
  1162       add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
  1163   | add_term_tvar_ixns(f$t,ixns) =
  1164       add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
  1165 
  1166 
  1167 (** Frees and Vars **)
  1168 
  1169 (*Accumulates the Vars in the term, suppressing duplicates*)
  1170 fun add_term_vars (t, vars: term list) = case t of
  1171     Var   _ => OrdList.insert term_ord t vars
  1172   | Abs (_,_,body) => add_term_vars(body,vars)
  1173   | f$t =>  add_term_vars (f, add_term_vars(t, vars))
  1174   | _ => vars;
  1175 
  1176 fun term_vars t = add_term_vars(t,[]);
  1177 
  1178 (*Accumulates the Frees in the term, suppressing duplicates*)
  1179 fun add_term_frees (t, frees: term list) = case t of
  1180     Free   _ => OrdList.insert term_ord t frees
  1181   | Abs (_,_,body) => add_term_frees(body,frees)
  1182   | f$t =>  add_term_frees (f, add_term_frees(t, frees))
  1183   | _ => frees;
  1184 
  1185 fun term_frees t = add_term_frees(t,[]);
  1186 
  1187 
  1188 (* dest abstraction *)
  1189 
  1190 fun dest_abs (x, T, body) =
  1191   let
  1192     fun name_clash (Free (y, _)) = (x = y)
  1193       | name_clash (t $ u) = name_clash t orelse name_clash u
  1194       | name_clash (Abs (_, _, t)) = name_clash t
  1195       | name_clash _ = false;
  1196   in
  1197     if name_clash body then
  1198       dest_abs (Name.variant [x] x, T, body)    (*potentially slow, but rarely happens*)
  1199     else (x, subst_bound (Free (x, T), body))
  1200   end;
  1201 
  1202 
  1203 (* renaming variables *)
  1204 
  1205 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
  1206 
  1207 fun declare_term_names tm =
  1208   fold_aterms
  1209     (fn Const (a, _) => Name.declare (NameSpace.base a)
  1210       | Free (a, _) => Name.declare a
  1211       | _ => I) tm #>
  1212   fold_types declare_typ_names tm;
  1213 
  1214 fun variant_frees t frees =
  1215   fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
  1216 
  1217 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
  1218 
  1219 
  1220 (* dummy patterns *)
  1221 
  1222 val dummy_patternN = "dummy_pattern";
  1223 
  1224 fun dummy_pattern T = Const (dummy_patternN, T);
  1225 
  1226 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
  1227   | is_dummy_pattern _ = false;
  1228 
  1229 fun no_dummy_patterns tm =
  1230   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
  1231   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
  1232 
  1233 fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
  1234       let val [x] = Name.invents used Name.uu 1
  1235       in (Free (Name.internal x, T), Name.declare x used) end
  1236   | free_dummy_patterns (Abs (x, T, b)) used =
  1237       let val (b', used') = free_dummy_patterns b used
  1238       in (Abs (x, T, b'), used') end
  1239   | free_dummy_patterns (t $ u) used =
  1240       let
  1241         val (t', used') = free_dummy_patterns t used;
  1242         val (u', used'') = free_dummy_patterns u used';
  1243       in (t' $ u', used'') end
  1244   | free_dummy_patterns a used = (a, used);
  1245 
  1246 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
  1247       (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1)
  1248   | replace_dummy Ts (Abs (x, T, t)) i =
  1249       let val (t', i') = replace_dummy (T :: Ts) t i
  1250       in (Abs (x, T, t'), i') end
  1251   | replace_dummy Ts (t $ u) i =
  1252       let
  1253         val (t', i') = replace_dummy Ts t i;
  1254         val (u', i'') = replace_dummy Ts u i';
  1255       in (t' $ u', i'') end
  1256   | replace_dummy _ a i = (a, i);
  1257 
  1258 val replace_dummy_patterns = replace_dummy [];
  1259 
  1260 fun is_replaced_dummy_pattern ("_dummy_", _) = true
  1261   | is_replaced_dummy_pattern _ = false;
  1262 
  1263 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
  1264   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
  1265   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
  1266   | show_dummy_patterns a = a;
  1267 
  1268 
  1269 (* display variables *)
  1270 
  1271 val show_question_marks = ref true;
  1272 
  1273 fun string_of_vname (x, i) =
  1274   let
  1275     val question_mark = if ! show_question_marks then "?" else "";
  1276     val idx = string_of_int i;
  1277     val dot =
  1278       (case rev (Symbol.explode x) of
  1279         _ :: "\\<^isub>" :: _ => false
  1280       | _ :: "\\<^isup>" :: _ => false
  1281       | c :: _ => Symbol.is_digit c
  1282       | _ => true);
  1283   in
  1284     if dot then question_mark ^ x ^ "." ^ idx
  1285     else if i <> 0 then question_mark ^ x ^ idx
  1286     else question_mark ^ x
  1287   end;
  1288 
  1289 fun string_of_vname' (x, ~1) = x
  1290   | string_of_vname' xi = string_of_vname xi;
  1291 
  1292 end;
  1293 
  1294 structure BasicTerm: BASIC_TERM = Term;
  1295 open BasicTerm;