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