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