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