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