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