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