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