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