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