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