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