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