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