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