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