src/Pure/term.ML
author wenzelm
Sat Jan 14 19:06:05 2012 +0100 (2012-01-14)
changeset 46217 7b19666f0e3d
parent 46215 0da9433f959e
child 46218 ecf6375e2abb
permissions -rw-r--r--
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
     1 (*  Title:      Pure/term.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Simply typed lambda-calculus: types, terms, and basic operations.
     6 *)
     7 
     8 infix 9 $;
     9 infixr 5 -->;
    10 infixr --->;
    11 infix aconv;
    12 
    13 signature BASIC_TERM =
    14 sig
    15   type indexname = string * int
    16   type class = string
    17   type sort = class list
    18   type arity = string * sort list * sort
    19   datatype typ =
    20     Type  of string * typ list |
    21     TFree of string * sort |
    22     TVar  of indexname * sort
    23   datatype term =
    24     Const of string * typ |
    25     Free of string * typ |
    26     Var of indexname * typ |
    27     Bound of int |
    28     Abs of string * typ * term |
    29     $ of term * term
    30   exception TYPE of string * typ list * term list
    31   exception TERM of string * term list
    32   val dummyS: sort
    33   val dummyT: typ
    34   val no_dummyT: typ -> typ
    35   val --> : typ * typ -> typ
    36   val ---> : typ list * typ -> typ
    37   val dest_Type: typ -> string * typ list
    38   val dest_TVar: typ -> indexname * sort
    39   val dest_TFree: typ -> string * sort
    40   val is_Bound: term -> bool
    41   val is_Const: term -> bool
    42   val is_Free: term -> bool
    43   val is_Var: term -> bool
    44   val is_TVar: typ -> bool
    45   val dest_Const: term -> string * typ
    46   val dest_Free: term -> string * typ
    47   val dest_Var: term -> indexname * typ
    48   val dest_comb: term -> term * term
    49   val domain_type: typ -> typ
    50   val range_type: typ -> typ
    51   val dest_funT: typ -> typ * typ
    52   val binder_types: typ -> typ list
    53   val body_type: typ -> typ
    54   val strip_type: typ -> typ list * typ
    55   val type_of1: typ list * term -> typ
    56   val type_of: term -> typ
    57   val fastype_of1: typ list * term -> typ
    58   val fastype_of: term -> typ
    59   val list_abs: (string * typ) list * term -> term
    60   val strip_abs: term -> (string * typ) list * term
    61   val strip_abs_body: term -> term
    62   val strip_abs_vars: term -> (string * typ) list
    63   val strip_qnt_body: string -> term -> term
    64   val strip_qnt_vars: string -> term -> (string * typ) list
    65   val list_comb: term * term list -> term
    66   val strip_comb: term -> term * term list
    67   val head_of: term -> term
    68   val size_of_term: term -> int
    69   val size_of_typ: typ -> int
    70   val map_atyps: (typ -> typ) -> typ -> typ
    71   val map_aterms: (term -> term) -> term -> term
    72   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    73   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    74   val map_types: (typ -> typ) -> term -> term
    75   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    76   val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
    77   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    78   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    79   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    80   val burrow_types: (typ list -> typ list) -> term list -> term list
    81   val aconv: term * term -> bool
    82   val propT: typ
    83   val strip_all_body: term -> term
    84   val strip_all_vars: term -> (string * typ) list
    85   val incr_bv: int * int * term -> term
    86   val incr_boundvars: int -> term -> term
    87   val add_loose_bnos: term * int * int list -> int list
    88   val loose_bnos: term -> int list
    89   val loose_bvar: term * int -> bool
    90   val loose_bvar1: term * int -> bool
    91   val subst_bounds: term list * term -> term
    92   val subst_bound: term * term -> term
    93   val betapply: term * term -> term
    94   val betapplys: term * term list -> term
    95   val subst_free: (term * term) list -> term -> term
    96   val abstract_over: term * term -> term
    97   val lambda: term -> term -> term
    98   val absfree: string * typ -> term -> term
    99   val absdummy: typ -> term -> term
   100   val list_all: (string * typ) list * term -> term
   101   val subst_atomic: (term * term) list -> term -> term
   102   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   103   val subst_atomic_types: (typ * typ) list -> term -> term
   104   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   105   val subst_TVars: (indexname * typ) list -> term -> term
   106   val subst_Vars: (indexname * term) list -> term -> term
   107   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   108   val is_first_order: string list -> term -> bool
   109   val maxidx_of_typ: typ -> int
   110   val maxidx_of_typs: typ list -> int
   111   val maxidx_of_term: term -> int
   112   val exists_subtype: (typ -> bool) -> typ -> bool
   113   val exists_type: (typ -> bool) -> term -> bool
   114   val exists_subterm: (term -> bool) -> term -> bool
   115   val exists_Const: (string * typ -> bool) -> term -> bool
   116 end;
   117 
   118 signature TERM =
   119 sig
   120   include BASIC_TERM
   121   val aT: sort -> typ
   122   val itselfT: typ -> typ
   123   val a_itselfT: typ
   124   val argument_type_of: term -> int -> typ
   125   val add_tvar_namesT: typ -> indexname list -> indexname list
   126   val add_tvar_names: term -> indexname list -> indexname list
   127   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   128   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   129   val add_var_names: term -> indexname list -> indexname list
   130   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   131   val add_tfree_namesT: typ -> string list -> string list
   132   val add_tfree_names: term -> string list -> string list
   133   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   134   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   135   val add_free_names: term -> string list -> string list
   136   val add_frees: term -> (string * typ) list -> (string * typ) list
   137   val add_const_names: term -> string list -> string list
   138   val add_consts: term -> (string * typ) list -> (string * typ) list
   139   val hidden_polymorphism: term -> (indexname * sort) list
   140   val declare_typ_names: typ -> Name.context -> Name.context
   141   val declare_term_names: term -> Name.context -> Name.context
   142   val declare_term_frees: term -> Name.context -> Name.context
   143   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   144   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   145   val eq_ix: indexname * indexname -> bool
   146   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   147   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   148   val aconv_untyped: term * term -> bool
   149   val could_unify: term * term -> bool
   150   val strip_abs_eta: int -> term -> (string * typ) list * term
   151   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   152   val map_abs_vars: (string -> string) -> term -> term
   153   val rename_abs: term -> term -> term -> term option
   154   val is_open: term -> bool
   155   val is_dependent: term -> bool
   156   val lambda_name: string * term -> term -> term
   157   val close_schematic_term: term -> term
   158   val maxidx_typ: typ -> int -> int
   159   val maxidx_typs: typ list -> int -> int
   160   val maxidx_term: term -> int -> int
   161   val has_abs: term -> bool
   162   val dest_abs: string * typ * term -> string * term
   163   val dummy_patternN: string
   164   val dummy_pattern: typ -> term
   165   val dummy: term
   166   val dummy_prop: term
   167   val is_dummy_pattern: term -> bool
   168   val free_dummy_patterns: term -> Name.context -> term * Name.context
   169   val no_dummy_patterns: term -> term
   170   val replace_dummy_patterns: term -> int -> term * int
   171   val is_replaced_dummy_pattern: indexname -> bool
   172   val show_dummy_patterns: term -> term
   173   val string_of_vname: indexname -> string
   174   val string_of_vname': indexname -> string
   175 end;
   176 
   177 structure Term: TERM =
   178 struct
   179 
   180 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   181   for resolution.*)
   182 type indexname = string * int;
   183 
   184 (* Types are classified by sorts. *)
   185 type class = string;
   186 type sort  = class list;
   187 type arity = string * sort list * sort;
   188 
   189 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
   190 datatype typ = Type  of string * typ list
   191              | TFree of string * sort
   192              | TVar  of indexname * sort;
   193 
   194 (*Terms.  Bound variables are indicated by depth number.
   195   Free variables, (scheme) variables and constants have names.
   196   An term is "closed" if every bound variable of level "lev"
   197   is enclosed by at least "lev" abstractions.
   198 
   199   It is possible to create meaningless terms containing loose bound vars
   200   or type mismatches.  But such terms are not allowed in rules. *)
   201 
   202 datatype term =
   203     Const of string * typ
   204   | Free  of string * typ
   205   | Var   of indexname * typ
   206   | Bound of int
   207   | Abs   of string*typ*term
   208   | op $  of term*term;
   209 
   210 (*Errors involving type mismatches*)
   211 exception TYPE of string * typ list * term list;
   212 
   213 (*Errors errors involving terms*)
   214 exception TERM of string * term list;
   215 
   216 (*Note variable naming conventions!
   217     a,b,c: string
   218     f,g,h: functions (including terms of function type)
   219     i,j,m,n: int
   220     t,u: term
   221     v,w: indexnames
   222     x,y: any
   223     A,B,C: term (denoting formulae)
   224     T,U: typ
   225 *)
   226 
   227 
   228 (** Types **)
   229 
   230 (*dummies for type-inference etc.*)
   231 val dummyS = [""];
   232 val dummyT = Type ("dummy", []);
   233 
   234 fun no_dummyT typ =
   235   let
   236     fun check (T as Type ("dummy", _)) =
   237           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   238       | check (Type (_, Ts)) = List.app check Ts
   239       | check _ = ();
   240   in check typ; typ end;
   241 
   242 fun S --> T = Type("fun",[S,T]);
   243 
   244 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   245 val op ---> = Library.foldr (op -->);
   246 
   247 fun dest_Type (Type x) = x
   248   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   249 fun dest_TVar (TVar x) = x
   250   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   251 fun dest_TFree (TFree x) = x
   252   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   253 
   254 
   255 (** Discriminators **)
   256 
   257 fun is_Bound (Bound _) = true
   258   | is_Bound _         = false;
   259 
   260 fun is_Const (Const _) = true
   261   | is_Const _ = false;
   262 
   263 fun is_Free (Free _) = true
   264   | is_Free _ = false;
   265 
   266 fun is_Var (Var _) = true
   267   | is_Var _ = false;
   268 
   269 fun is_TVar (TVar _) = true
   270   | is_TVar _ = false;
   271 
   272 
   273 (** Destructors **)
   274 
   275 fun dest_Const (Const x) =  x
   276   | dest_Const t = raise TERM("dest_Const", [t]);
   277 
   278 fun dest_Free (Free x) =  x
   279   | dest_Free t = raise TERM("dest_Free", [t]);
   280 
   281 fun dest_Var (Var x) =  x
   282   | dest_Var t = raise TERM("dest_Var", [t]);
   283 
   284 fun dest_comb (t1 $ t2) = (t1, t2)
   285   | dest_comb t = raise TERM("dest_comb", [t]);
   286 
   287 
   288 fun domain_type (Type ("fun", [T, _])) = T;
   289 
   290 fun range_type (Type ("fun", [_, U])) = U;
   291 
   292 fun dest_funT (Type ("fun", [T, U])) = (T, U)
   293   | dest_funT T = raise TYPE ("dest_funT", [T], []);
   294 
   295 
   296 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   297 fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
   298   | binder_types _ = [];
   299 
   300 (* maps  [T1,...,Tn]--->T  to T*)
   301 fun body_type (Type ("fun", [_, U])) = body_type U
   302   | body_type T = T;
   303 
   304 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
   305 fun strip_type T = (binder_types T, body_type T);
   306 
   307 
   308 (*Compute the type of the term, checking that combinations are well-typed
   309   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   310 fun type_of1 (Ts, Const (_,T)) = T
   311   | type_of1 (Ts, Free  (_,T)) = T
   312   | type_of1 (Ts, Bound i) = (nth Ts i
   313         handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   314   | type_of1 (Ts, Var (_,T)) = T
   315   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   316   | type_of1 (Ts, f$u) =
   317       let val U = type_of1(Ts,u)
   318           and T = type_of1(Ts,f)
   319       in case T of
   320             Type("fun",[T1,T2]) =>
   321               if T1=U then T2  else raise TYPE
   322                     ("type_of: type mismatch in application", [T1,U], [f$u])
   323           | _ => raise TYPE
   324                     ("type_of: function type is expected in application",
   325                      [T,U], [f$u])
   326       end;
   327 
   328 fun type_of t : typ = type_of1 ([],t);
   329 
   330 (*Determines the type of a term, with minimal checking*)
   331 fun fastype_of1 (Ts, f$u) =
   332     (case fastype_of1 (Ts,f) of
   333         Type("fun",[_,T]) => T
   334         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   335   | fastype_of1 (_, Const (_,T)) = T
   336   | fastype_of1 (_, Free (_,T)) = T
   337   | fastype_of1 (Ts, Bound i) = (nth Ts i
   338          handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   339   | fastype_of1 (_, Var (_,T)) = T
   340   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   341 
   342 fun fastype_of t : typ = fastype_of1 ([],t);
   343 
   344 (*Determine the argument type of a function*)
   345 fun argument_type_of tm k =
   346   let
   347     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   348       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   349 
   350     fun arg 0 _ (Abs (_, T, _)) = T
   351       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   352       | arg i Ts (t $ _) = arg (i + 1) Ts t
   353       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   354   in arg k [] tm end;
   355 
   356 
   357 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
   358 
   359 fun strip_abs (Abs (a, T, t)) =
   360       let val (a', t') = strip_abs t
   361       in ((a, T) :: a', t') end
   362   | strip_abs t = ([], t);
   363 
   364 (* maps  (x1,...,xn)t   to   t  *)
   365 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   366   | strip_abs_body u  =  u;
   367 
   368 (* maps  (x1,...,xn)t   to   [x1, ..., xn]  *)
   369 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   370   | strip_abs_vars u  =  [] : (string*typ) list;
   371 
   372 
   373 fun strip_qnt_body qnt =
   374 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   375       | strip t = t
   376 in strip end;
   377 
   378 fun strip_qnt_vars qnt =
   379 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   380       | strip t  =  [] : (string*typ) list
   381 in strip end;
   382 
   383 
   384 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   385 val list_comb : term * term list -> term = Library.foldl (op $);
   386 
   387 
   388 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   389 fun strip_comb u : term * term list =
   390     let fun stripc (f$t, ts) = stripc (f, t::ts)
   391         |   stripc  x =  x
   392     in  stripc(u,[])  end;
   393 
   394 
   395 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   396 fun head_of (f$t) = head_of f
   397   | head_of u = u;
   398 
   399 (*number of atoms and abstractions in a term*)
   400 fun size_of_term tm =
   401   let
   402     fun add_size (t $ u) n = add_size t (add_size u n)
   403       | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
   404       | add_size _ n = n + 1;
   405   in add_size tm 0 end;
   406 
   407 (*number of atoms and constructors in a type*)
   408 fun size_of_typ ty =
   409   let
   410     fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
   411       | add_size _ n = n + 1;
   412   in add_size ty 0 end;
   413 
   414 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   415   | map_atyps f T = f T;
   416 
   417 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   418   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   419   | map_aterms f t = f t;
   420 
   421 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   422 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   423 
   424 fun map_types f =
   425   let
   426     fun map_aux (Const (a, T)) = Const (a, f T)
   427       | map_aux (Free (a, T)) = Free (a, f T)
   428       | map_aux (Var (v, T)) = Var (v, f T)
   429       | map_aux (Bound i) = Bound i
   430       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   431       | map_aux (t $ u) = map_aux t $ map_aux u;
   432   in map_aux end;
   433 
   434 
   435 (* fold types and terms *)
   436 
   437 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   438   | fold_atyps f T = f T;
   439 
   440 fun fold_atyps_sorts f =
   441   fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
   442 
   443 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   444   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   445   | fold_aterms f a = f a;
   446 
   447 fun fold_term_types f (t as Const (_, T)) = f t T
   448   | fold_term_types f (t as Free (_, T)) = f t T
   449   | fold_term_types f (t as Var (_, T)) = f t T
   450   | fold_term_types f (Bound _) = I
   451   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   452   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   453 
   454 fun fold_types f = fold_term_types (K f);
   455 
   456 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
   457   | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
   458   | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
   459   | replace_types (Bound i) Ts = (Bound i, Ts)
   460   | replace_types (Abs (x, _, b)) (T :: Ts) =
   461       let val (b', Ts') = replace_types b Ts
   462       in (Abs (x, T, b'), Ts') end
   463   | replace_types (t $ u) Ts =
   464       let
   465         val (t', Ts') = replace_types t Ts;
   466         val (u', Ts'') = replace_types u Ts';
   467       in (t' $ u', Ts'') end;
   468 
   469 fun burrow_types f ts =
   470   let
   471     val Ts = rev (fold (fold_types cons) ts []);
   472     val Ts' = f Ts;
   473     val (ts', []) = fold_map replace_types ts Ts';
   474   in ts' end;
   475 
   476 (*collect variables*)
   477 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
   478 val add_tvar_names = fold_types add_tvar_namesT;
   479 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   480 val add_tvars = fold_types add_tvarsT;
   481 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   482 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   483 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
   484 val add_tfree_names = fold_types add_tfree_namesT;
   485 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   486 val add_tfrees = fold_types add_tfreesT;
   487 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
   488 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   489 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
   490 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
   491 
   492 (*extra type variables in a term, not covered by its type*)
   493 fun hidden_polymorphism t =
   494   let
   495     val T = fastype_of t;
   496     val tvarsT = add_tvarsT T [];
   497     val extra_tvars = fold_types (fold_atyps
   498       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   499   in extra_tvars end;
   500 
   501 
   502 (* renaming variables *)
   503 
   504 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   505 
   506 fun declare_term_names tm =
   507   fold_aterms
   508     (fn Const (a, _) => Name.declare (Long_Name.base_name a)
   509       | Free (a, _) => Name.declare a
   510       | _ => I) tm #>
   511   fold_types declare_typ_names tm;
   512 
   513 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
   514 
   515 fun variant_frees t frees =
   516   fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
   517     map snd frees;
   518 
   519 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   520 
   521 
   522 
   523 (** Comparing terms **)
   524 
   525 (* variables *)
   526 
   527 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   528 
   529 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   530 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   531 
   532 
   533 (* alpha equivalence *)
   534 
   535 fun tm1 aconv tm2 =
   536   pointer_eq (tm1, tm2) orelse
   537     (case (tm1, tm2) of
   538       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
   539     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
   540     | (a1, a2) => a1 = a2);
   541 
   542 fun aconv_untyped (tm1, tm2) =
   543   pointer_eq (tm1, tm2) orelse
   544     (case (tm1, tm2) of
   545       (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
   546     | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
   547     | (Const (a, _), Const (b, _)) => a = b
   548     | (Free (x, _), Free (y, _)) => x = y
   549     | (Var (xi, _), Var (yj, _)) => xi = yj
   550     | (Bound i, Bound j) => i = j
   551     | _ => false);
   552 
   553 
   554 (*A fast unification filter: true unless the two terms cannot be unified.
   555   Terms must be NORMAL.  Treats all Vars as distinct. *)
   556 fun could_unify (t, u) =
   557   let
   558     fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
   559       | matchrands _ _ = true;
   560   in
   561     case (head_of t, head_of u) of
   562       (_, Var _) => true
   563     | (Var _, _) => true
   564     | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
   565     | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
   566     | (Bound i, Bound j) => i = j andalso matchrands t u
   567     | (Abs _, _) => true   (*because of possible eta equality*)
   568     | (_, Abs _) => true
   569     | _ => false
   570   end;
   571 
   572 
   573 
   574 (** Connectives of higher order logic **)
   575 
   576 fun aT S = TFree (Name.aT, S);
   577 
   578 fun itselfT ty = Type ("itself", [ty]);
   579 val a_itselfT = itselfT (TFree (Name.aT, []));
   580 
   581 val propT : typ = Type ("prop",[]);
   582 
   583 (* maps  !!x1...xn. t   to   t  *)
   584 fun strip_all_body (Const("all",_)$Abs(_,_,t))  =  strip_all_body t
   585   | strip_all_body t  =  t;
   586 
   587 (* maps  !!x1...xn. t   to   [x1, ..., xn]  *)
   588 fun strip_all_vars (Const("all",_)$Abs(a,T,t))  =
   589                 (a,T) :: strip_all_vars t
   590   | strip_all_vars t  =  [] : (string*typ) list;
   591 
   592 (*increments a term's non-local bound variables
   593   required when moving a term within abstractions
   594      inc is  increment for bound variables
   595      lev is  level at which a bound variable is considered 'loose'*)
   596 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   597   | incr_bv (inc, lev, Abs(a,T,body)) =
   598         Abs(a, T, incr_bv(inc,lev+1,body))
   599   | incr_bv (inc, lev, f$t) =
   600       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   601   | incr_bv (inc, lev, u) = u;
   602 
   603 fun incr_boundvars  0  t = t
   604   | incr_boundvars inc t = incr_bv(inc,0,t);
   605 
   606 (*Scan a pair of terms; while they are similar,
   607   accumulate corresponding bound vars in "al"*)
   608 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   609       match_bvs(s, t, if x="" orelse y="" then al
   610                                           else (x,y)::al)
   611   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   612   | match_bvs(_,_,al) = al;
   613 
   614 (* strip abstractions created by parameters *)
   615 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
   616 
   617 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   618   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   619   | map_abs_vars f t = t;
   620 
   621 fun rename_abs pat obj t =
   622   let
   623     val ren = match_bvs (pat, obj, []);
   624     fun ren_abs (Abs (x, T, b)) =
   625           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   626       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   627       | ren_abs t = t
   628   in if null ren then NONE else SOME (ren_abs t) end;
   629 
   630 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   631    (Bound 0) is loose at level 0 *)
   632 fun add_loose_bnos (Bound i, lev, js) =
   633         if i<lev then js else insert (op =) (i - lev) js
   634   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   635   | add_loose_bnos (f$t, lev, js) =
   636         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   637   | add_loose_bnos (_, _, js) = js;
   638 
   639 fun loose_bnos t = add_loose_bnos (t, 0, []);
   640 
   641 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   642    level k or beyond. *)
   643 fun loose_bvar(Bound i,k) = i >= k
   644   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   645   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   646   | loose_bvar _ = false;
   647 
   648 fun loose_bvar1(Bound i,k) = i = k
   649   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   650   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   651   | loose_bvar1 _ = false;
   652 
   653 fun is_open t = loose_bvar (t, 0);
   654 fun is_dependent t = loose_bvar1 (t, 0);
   655 
   656 (*Substitute arguments for loose bound variables.
   657   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   658   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   659         and the appropriate call is  subst_bounds([b,a], c) .
   660   Loose bound variables >=n are reduced by "n" to
   661      compensate for the disappearance of lambdas.
   662 *)
   663 fun subst_bounds (args: term list, t) : term =
   664   let
   665     val n = length args;
   666     fun subst (t as Bound i, lev) =
   667          (if i < lev then raise Same.SAME   (*var is locally bound*)
   668           else incr_boundvars lev (nth args (i - lev))
   669             handle General.Subscript => Bound (i - n))  (*loose: change it*)
   670       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   671       | subst (f $ t, lev) =
   672           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   673             handle Same.SAME => f $ subst (t, lev))
   674       | subst _ = raise Same.SAME;
   675   in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
   676 
   677 (*Special case: one argument*)
   678 fun subst_bound (arg, t) : term =
   679   let
   680     fun subst (Bound i, lev) =
   681           if i < lev then raise Same.SAME   (*var is locally bound*)
   682           else if i = lev then incr_boundvars lev arg
   683           else Bound (i - 1)   (*loose: change it*)
   684       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   685       | subst (f $ t, lev) =
   686           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   687             handle Same.SAME => f $ subst (t, lev))
   688       | subst _ = raise Same.SAME;
   689   in subst (t, 0) handle Same.SAME => t end;
   690 
   691 (*beta-reduce if possible, else form application*)
   692 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   693   | betapply (f,u) = f$u;
   694 
   695 val betapplys = Library.foldl betapply;
   696 
   697 
   698 (*unfolding abstractions with substitution
   699   of bound variables and implicit eta-expansion*)
   700 fun strip_abs_eta k t =
   701   let
   702     val used = fold_aterms declare_term_frees t Name.context;
   703     fun strip_abs t (0, used) = (([], t), (0, used))
   704       | strip_abs (Abs (v, T, t)) (k, used) =
   705           let
   706             val (v', used') = Name.variant v used;
   707             val t' = subst_bound (Free (v', T), t);
   708             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   709           in (((v', T) :: vs, t''), (k', used'')) end
   710       | strip_abs t (k, used) = (([], t), (k, used));
   711     fun expand_eta [] t _ = ([], t)
   712       | expand_eta (T::Ts) t used =
   713           let
   714             val (v, used') = Name.variant "" used;
   715             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   716           in ((v, T) :: vs, t') end;
   717     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   718     val Ts = fst (chop k' (binder_types (fastype_of t')));
   719     val (vs2, t'') = expand_eta Ts t' used';
   720   in (vs1 @ vs2, t'') end;
   721 
   722 
   723 (*Substitute new for free occurrences of old in a term*)
   724 fun subst_free [] = I
   725   | subst_free pairs =
   726       let fun substf u =
   727             case AList.lookup (op aconv) pairs u of
   728                 SOME u' => u'
   729               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   730                                  | t$u' => substf t $ substf u'
   731                                  | _ => u)
   732       in  substf  end;
   733 
   734 (*Abstraction of the term "body" over its occurrences of v,
   735     which must contain no loose bound variables.
   736   The resulting term is ready to become the body of an Abs.*)
   737 fun abstract_over (v, body) =
   738   let
   739     fun abs lev tm =
   740       if v aconv tm then Bound lev
   741       else
   742         (case tm of
   743           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   744         | t $ u =>
   745             (abs lev t $ (abs lev u handle Same.SAME => u)
   746               handle Same.SAME => t $ abs lev u)
   747         | _ => raise Same.SAME);
   748   in abs 0 body handle Same.SAME => body end;
   749 
   750 fun term_name (Const (x, _)) = Long_Name.base_name x
   751   | term_name (Free (x, _)) = x
   752   | term_name (Var ((x, _), _)) = x
   753   | term_name _ = Name.uu;
   754 
   755 fun lambda_name (x, v) t =
   756   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
   757 
   758 fun lambda v t = lambda_name ("", v) t;
   759 
   760 fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
   761 fun absdummy T body = Abs (Name.uu_, T, body);
   762 
   763 (*Quantification over a list of variables (already bound in body) *)
   764 fun list_all ([], t) = t
   765   | list_all ((a,T)::vars, t) =
   766       Const ("all", (T --> propT) --> propT) $ Abs (a, T, list_all (vars, t));
   767 
   768 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   769   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
   770 fun subst_atomic [] tm = tm
   771   | subst_atomic inst tm =
   772       let
   773         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
   774           | subst (t $ u) = subst t $ subst u
   775           | subst t = the_default t (AList.lookup (op aconv) inst t);
   776       in subst tm end;
   777 
   778 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
   779 fun typ_subst_atomic [] ty = ty
   780   | typ_subst_atomic inst ty =
   781       let
   782         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   783           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
   784       in subst ty end;
   785 
   786 fun subst_atomic_types [] tm = tm
   787   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
   788 
   789 fun typ_subst_TVars [] ty = ty
   790   | typ_subst_TVars inst ty =
   791       let
   792         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
   793           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
   794           | subst T = T;
   795       in subst ty end;
   796 
   797 fun subst_TVars [] tm = tm
   798   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
   799 
   800 fun subst_Vars [] tm = tm
   801   | subst_Vars inst tm =
   802       let
   803         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
   804           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
   805           | subst (t $ u) = subst t $ subst u
   806           | subst t = t;
   807       in subst tm end;
   808 
   809 fun subst_vars ([], []) tm = tm
   810   | subst_vars ([], inst) tm = subst_Vars inst tm
   811   | subst_vars (instT, inst) tm =
   812       let
   813         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
   814           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
   815           | subst (Var (xi, T)) =
   816               (case AList.lookup (op =) inst xi of
   817                 NONE => Var (xi, typ_subst_TVars instT T)
   818               | SOME t => t)
   819           | subst (t as Bound _) = t
   820           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
   821           | subst (t $ u) = subst t $ subst u;
   822       in subst tm end;
   823 
   824 fun close_schematic_term t =
   825   let
   826     val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
   827     val extra_terms = map Var (add_vars t []);
   828   in fold lambda (extra_terms @ extra_types) t end;
   829 
   830 
   831 
   832 (** Identifying first-order terms **)
   833 
   834 (*Differs from proofterm/is_fun in its treatment of TVar*)
   835 fun is_funtype (Type ("fun", [_, _])) = true
   836   | is_funtype _ = false;
   837 
   838 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
   839 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
   840 
   841 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   842   function type. The supplied quantifiers are excluded: their argument always
   843   has a function type through a recursive call into its body.*)
   844 fun is_first_order quants =
   845   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
   846         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
   847             member (op =) quants q  andalso   (*it is a known quantifier*)
   848             not (is_funtype T)   andalso first_order1 (T::Ts) body
   849         | first_order1 Ts t =
   850             case strip_comb t of
   851                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   852                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   853                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   854                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
   855                | (Abs _, ts) => false (*not in beta-normal form*)
   856                | _ => error "first_order: unexpected case"
   857     in  first_order1 []  end;
   858 
   859 
   860 (* maximum index of typs and terms *)
   861 
   862 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   863   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   864   | maxidx_typ (TFree _) i = i
   865 and maxidx_typs [] i = i
   866   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
   867 
   868 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   869   | maxidx_term (Const (_, T)) i = maxidx_typ T i
   870   | maxidx_term (Free (_, T)) i = maxidx_typ T i
   871   | maxidx_term (Bound _) i = i
   872   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   873   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
   874 
   875 fun maxidx_of_typ T = maxidx_typ T ~1;
   876 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
   877 fun maxidx_of_term t = maxidx_term t ~1;
   878 
   879 
   880 
   881 (** misc syntax operations **)
   882 
   883 (* substructure *)
   884 
   885 fun exists_subtype P =
   886   let
   887     fun ex ty = P ty orelse
   888       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   889   in ex end;
   890 
   891 fun exists_type P =
   892   let
   893     fun ex (Const (_, T)) = P T
   894       | ex (Free (_, T)) = P T
   895       | ex (Var (_, T)) = P T
   896       | ex (Bound _) = false
   897       | ex (Abs (_, T, t)) = P T orelse ex t
   898       | ex (t $ u) = ex t orelse ex u;
   899   in ex end;
   900 
   901 fun exists_subterm P =
   902   let
   903     fun ex tm = P tm orelse
   904       (case tm of
   905         t $ u => ex t orelse ex u
   906       | Abs (_, _, t) => ex t
   907       | _ => false);
   908   in ex end;
   909 
   910 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   911 
   912 fun has_abs (Abs _) = true
   913   | has_abs (t $ u) = has_abs t orelse has_abs u
   914   | has_abs _ = false;
   915 
   916 
   917 (* dest abstraction *)
   918 
   919 fun dest_abs (x, T, body) =
   920   let
   921     fun name_clash (Free (y, _)) = (x = y)
   922       | name_clash (t $ u) = name_clash t orelse name_clash u
   923       | name_clash (Abs (_, _, t)) = name_clash t
   924       | name_clash _ = false;
   925   in
   926     if name_clash body then
   927       dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
   928     else (x, subst_bound (Free (x, T), body))
   929   end;
   930 
   931 
   932 (* dummy patterns *)
   933 
   934 val dummy_patternN = "dummy_pattern";
   935 
   936 fun dummy_pattern T = Const (dummy_patternN, T);
   937 val dummy = dummy_pattern dummyT;
   938 val dummy_prop = dummy_pattern propT;
   939 
   940 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
   941   | is_dummy_pattern _ = false;
   942 
   943 fun no_dummy_patterns tm =
   944   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   945   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   946 
   947 fun free_dummy_patterns (Const ("dummy_pattern", T)) used =
   948       let val [x] = Name.invent used Name.uu 1
   949       in (Free (Name.internal x, T), Name.declare x used) end
   950   | free_dummy_patterns (Abs (x, T, b)) used =
   951       let val (b', used') = free_dummy_patterns b used
   952       in (Abs (x, T, b'), used') end
   953   | free_dummy_patterns (t $ u) used =
   954       let
   955         val (t', used') = free_dummy_patterns t used;
   956         val (u', used'') = free_dummy_patterns u used';
   957       in (t' $ u', used'') end
   958   | free_dummy_patterns a used = (a, used);
   959 
   960 fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
   961       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   962   | replace_dummy Ts (Abs (x, T, t)) i =
   963       let val (t', i') = replace_dummy (T :: Ts) t i
   964       in (Abs (x, T, t'), i') end
   965   | replace_dummy Ts (t $ u) i =
   966       let
   967         val (t', i') = replace_dummy Ts t i;
   968         val (u', i'') = replace_dummy Ts u i';
   969       in (t' $ u', i'') end
   970   | replace_dummy _ a i = (a, i);
   971 
   972 val replace_dummy_patterns = replace_dummy [];
   973 
   974 fun is_replaced_dummy_pattern ("_dummy_", _) = true
   975   | is_replaced_dummy_pattern _ = false;
   976 
   977 fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
   978   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   979   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   980   | show_dummy_patterns a = a;
   981 
   982 
   983 (* display variables *)
   984 
   985 fun string_of_vname (x, i) =
   986   let
   987     val idx = string_of_int i;
   988     val dot =
   989       (case rev (Symbol.explode x) of
   990         _ :: "\\<^isub>" :: _ => false
   991       | _ :: "\\<^isup>" :: _ => false
   992       | c :: _ => Symbol.is_digit c
   993       | _ => true);
   994   in
   995     if dot then "?" ^ x ^ "." ^ idx
   996     else if i <> 0 then "?" ^ x ^ idx
   997     else "?" ^ x
   998   end;
   999 
  1000 fun string_of_vname' (x, ~1) = x
  1001   | string_of_vname' xi = string_of_vname xi;
  1002 
  1003 end;
  1004 
  1005 structure Basic_Term: BASIC_TERM = Term;
  1006 open Basic_Term;