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