src/Pure/term.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (21 months ago)
changeset 66695 91500c024c7f
parent 63619 9c870388e87a
child 67703 8c4806fe827f
permissions -rw-r--r--
tuned;
     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 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 size_of_typ: typ -> int
    69   val map_atyps: (typ -> typ) -> typ -> typ
    70   val map_aterms: (term -> term) -> term -> term
    71   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    72   val map_type_tfree: (string * sort -> typ) -> typ -> typ
    73   val map_types: (typ -> typ) -> term -> term
    74   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    75   val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
    76   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    77   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    78   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
    79   val burrow_types: (typ list -> typ list) -> term list -> term list
    80   val aconv: term * term -> bool
    81   val propT: typ
    82   val strip_all_body: term -> term
    83   val strip_all_vars: term -> (string * typ) list
    84   val incr_bv: int * int * term -> term
    85   val incr_boundvars: int -> term -> term
    86   val add_loose_bnos: term * int * int list -> int list
    87   val loose_bnos: term -> int list
    88   val loose_bvar: term * int -> bool
    89   val loose_bvar1: term * int -> bool
    90   val subst_bounds: term list * term -> term
    91   val subst_bound: term * term -> term
    92   val betapply: term * term -> term
    93   val betapplys: term * term list -> term
    94   val subst_free: (term * term) list -> term -> term
    95   val abstract_over: term * term -> term
    96   val lambda: term -> term -> term
    97   val absfree: string * typ -> term -> term
    98   val absdummy: typ -> term -> term
    99   val subst_atomic: (term * term) list -> term -> term
   100   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   101   val subst_atomic_types: (typ * typ) list -> term -> term
   102   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   103   val subst_TVars: (indexname * typ) list -> term -> term
   104   val subst_Vars: (indexname * term) list -> term -> term
   105   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   106   val is_first_order: string list -> term -> bool
   107   val maxidx_of_typ: typ -> int
   108   val maxidx_of_typs: typ list -> int
   109   val maxidx_of_term: term -> int
   110   val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   111   val exists_subtype: (typ -> bool) -> typ -> bool
   112   val exists_type: (typ -> bool) -> term -> bool
   113   val exists_subterm: (term -> bool) -> term -> bool
   114   val exists_Const: (string * typ -> bool) -> term -> bool
   115 end;
   116 
   117 signature TERM =
   118 sig
   119   include BASIC_TERM
   120   val aT: sort -> typ
   121   val itselfT: typ -> typ
   122   val a_itselfT: typ
   123   val argument_type_of: term -> int -> typ
   124   val abs: string * typ -> term -> term
   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 term_name: term -> string
   157   val dependent_lambda_name: string * term -> term -> term
   158   val lambda_name: string * term -> term -> term
   159   val close_schematic_term: term -> term
   160   val maxidx_typ: typ -> int -> int
   161   val maxidx_typs: typ list -> int -> int
   162   val maxidx_term: term -> int -> int
   163   val could_beta_contract: term -> bool
   164   val could_eta_contract: term -> bool
   165   val could_beta_eta_contract: term -> bool
   166   val dest_abs: string * typ * term -> string * term
   167   val dummy_pattern: typ -> term
   168   val dummy: term
   169   val dummy_prop: term
   170   val is_dummy_pattern: term -> bool
   171   val free_dummy_patterns: term -> Name.context -> term * Name.context
   172   val no_dummy_patterns: term -> term
   173   val replace_dummy_patterns: term -> int -> term * int
   174   val show_dummy_patterns: term -> term
   175   val string_of_vname: indexname -> string
   176   val string_of_vname': indexname -> string
   177 end;
   178 
   179 structure Term: TERM =
   180 struct
   181 
   182 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   183   for resolution.*)
   184 type indexname = string * int;
   185 
   186 (*Types are classified by sorts.*)
   187 type class = string;
   188 type sort  = class list;
   189 type arity = string * sort list * sort;
   190 
   191 (*The sorts attached to TFrees and TVars specify the sort of that variable.*)
   192 datatype typ = Type  of string * typ list
   193              | TFree of string * sort
   194              | TVar  of indexname * sort;
   195 
   196 (*Terms.  Bound variables are indicated by depth number.
   197   Free variables, (scheme) variables and constants have names.
   198   An term is "closed" if every bound variable of level "lev"
   199   is enclosed by at least "lev" abstractions.
   200 
   201   It is possible to create meaningless terms containing loose bound vars
   202   or type mismatches.  But such terms are not allowed in rules. *)
   203 
   204 datatype term =
   205     Const of string * typ
   206   | Free  of string * typ
   207   | Var   of indexname * typ
   208   | Bound of int
   209   | Abs   of string*typ*term
   210   | op $  of term*term;
   211 
   212 (*Errors involving type mismatches*)
   213 exception TYPE of string * typ list * term list;
   214 
   215 (*Errors errors involving terms*)
   216 exception TERM of string * term list;
   217 
   218 (*Note variable naming conventions!
   219     a,b,c: string
   220     f,g,h: functions (including terms of function type)
   221     i,j,m,n: int
   222     t,u: term
   223     v,w: indexnames
   224     x,y: any
   225     A,B,C: term (denoting formulae)
   226     T,U: typ
   227 *)
   228 
   229 
   230 (** Types **)
   231 
   232 (*dummies for type-inference etc.*)
   233 val dummyS = [""];
   234 val dummyT = Type ("dummy", []);
   235 
   236 fun no_dummyT typ =
   237   let
   238     fun check (T as Type ("dummy", _)) =
   239           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
   240       | check (Type (_, Ts)) = List.app check Ts
   241       | check _ = ();
   242   in check typ; typ end;
   243 
   244 fun S --> T = Type("fun",[S,T]);
   245 
   246 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
   247 val op ---> = Library.foldr (op -->);
   248 
   249 fun dest_Type (Type x) = x
   250   | dest_Type T = raise TYPE ("dest_Type", [T], []);
   251 fun dest_TVar (TVar x) = x
   252   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
   253 fun dest_TFree (TFree x) = x
   254   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
   255 
   256 
   257 (** Discriminators **)
   258 
   259 fun is_Bound (Bound _) = true
   260   | is_Bound _         = false;
   261 
   262 fun is_Const (Const _) = true
   263   | is_Const _ = false;
   264 
   265 fun is_Free (Free _) = true
   266   | is_Free _ = false;
   267 
   268 fun is_Var (Var _) = true
   269   | is_Var _ = false;
   270 
   271 fun is_TVar (TVar _) = true
   272   | is_TVar _ = false;
   273 
   274 
   275 (** Destructors **)
   276 
   277 fun dest_Const (Const x) =  x
   278   | dest_Const t = raise TERM("dest_Const", [t]);
   279 
   280 fun dest_Free (Free x) =  x
   281   | dest_Free t = raise TERM("dest_Free", [t]);
   282 
   283 fun dest_Var (Var x) =  x
   284   | dest_Var t = raise TERM("dest_Var", [t]);
   285 
   286 fun dest_comb (t1 $ t2) = (t1, t2)
   287   | dest_comb t = raise TERM("dest_comb", [t]);
   288 
   289 
   290 fun domain_type (Type ("fun", [T, _])) = T;
   291 
   292 fun range_type (Type ("fun", [_, U])) = U;
   293 
   294 fun dest_funT (Type ("fun", [T, U])) = (T, U)
   295   | dest_funT T = raise TYPE ("dest_funT", [T], []);
   296 
   297 
   298 (*maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
   299 fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
   300   | binder_types _ = [];
   301 
   302 (*maps  [T1,...,Tn]--->T  to T*)
   303 fun body_type (Type ("fun", [_, U])) = body_type U
   304   | body_type T = T;
   305 
   306 (*maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)*)
   307 fun strip_type T = (binder_types T, body_type T);
   308 
   309 
   310 (*Compute the type of the term, checking that combinations are well-typed
   311   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
   312 fun type_of1 (Ts, Const (_,T)) = T
   313   | type_of1 (Ts, Free  (_,T)) = T
   314   | type_of1 (Ts, Bound i) = (nth Ts i
   315         handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   316   | type_of1 (Ts, Var (_,T)) = T
   317   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   318   | type_of1 (Ts, f$u) =
   319       let val U = type_of1(Ts,u)
   320           and T = type_of1(Ts,f)
   321       in case T of
   322             Type("fun",[T1,T2]) =>
   323               if T1=U then T2  else raise TYPE
   324                     ("type_of: type mismatch in application", [T1,U], [f$u])
   325           | _ => raise TYPE
   326                     ("type_of: function type is expected in application",
   327                      [T,U], [f$u])
   328       end;
   329 
   330 fun type_of t : typ = type_of1 ([],t);
   331 
   332 (*Determines the type of a term, with minimal checking*)
   333 fun fastype_of1 (Ts, f$u) =
   334     (case fastype_of1 (Ts,f) of
   335         Type("fun",[_,T]) => T
   336         | _ => raise TERM("fastype_of: expected function type", [f$u]))
   337   | fastype_of1 (_, Const (_,T)) = T
   338   | fastype_of1 (_, Free (_,T)) = T
   339   | fastype_of1 (Ts, Bound i) = (nth Ts i
   340          handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
   341   | fastype_of1 (_, Var (_,T)) = T
   342   | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
   343 
   344 fun fastype_of t : typ = fastype_of1 ([],t);
   345 
   346 (*Determine the argument type of a function*)
   347 fun argument_type_of tm k =
   348   let
   349     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
   350       | argT _ T = raise TYPE ("argument_type_of", [T], []);
   351 
   352     fun arg 0 _ (Abs (_, T, _)) = T
   353       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
   354       | arg i Ts (t $ _) = arg (i + 1) Ts t
   355       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   356   in arg k [] tm end;
   357 
   358 
   359 fun abs (x, T) t = Abs (x, T, t);
   360 
   361 fun strip_abs (Abs (a, T, t)) =
   362       let val (a', t') = strip_abs t
   363       in ((a, T) :: a', t') end
   364   | strip_abs t = ([], t);
   365 
   366 (*maps  (x1,...,xn)t   to   t*)
   367 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   368   | strip_abs_body u  =  u;
   369 
   370 (*maps  (x1,...,xn)t   to   [x1, ..., xn]*)
   371 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   372   | strip_abs_vars u  =  [] : (string*typ) list;
   373 
   374 
   375 fun strip_qnt_body qnt =
   376 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
   377       | strip t = t
   378 in strip end;
   379 
   380 fun strip_qnt_vars qnt =
   381 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
   382       | strip t  =  [] : (string*typ) list
   383 in strip end;
   384 
   385 
   386 (*maps   (f, [t1,...,tn])  to  f(t1,...,tn)*)
   387 val list_comb : term * term list -> term = Library.foldl (op $);
   388 
   389 
   390 (*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   391 fun strip_comb u : term * term list =
   392     let fun stripc (f$t, ts) = stripc (f, t::ts)
   393         |   stripc  x =  x
   394     in  stripc(u,[])  end;
   395 
   396 
   397 (*maps   f(t1,...,tn)  to  f , which is never a combination*)
   398 fun head_of (f$t) = head_of f
   399   | head_of u = u;
   400 
   401 (*number of atoms and abstractions in a term*)
   402 fun size_of_term tm =
   403   let
   404     fun add_size (t $ u) n = add_size t (add_size u n)
   405       | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
   406       | add_size _ n = n + 1;
   407   in add_size tm 0 end;
   408 
   409 (*number of atoms and constructors in a type*)
   410 fun size_of_typ ty =
   411   let
   412     fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
   413       | add_size _ n = n + 1;
   414   in add_size ty 0 end;
   415 
   416 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   417   | map_atyps f T = f T;
   418 
   419 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   420   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   421   | map_aterms f t = f t;
   422 
   423 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
   424 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
   425 
   426 fun map_types f =
   427   let
   428     fun map_aux (Const (a, T)) = Const (a, f T)
   429       | map_aux (Free (a, T)) = Free (a, f T)
   430       | map_aux (Var (v, T)) = Var (v, f T)
   431       | map_aux (Bound i) = Bound i
   432       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
   433       | map_aux (t $ u) = map_aux t $ map_aux u;
   434   in map_aux end;
   435 
   436 
   437 (* fold types and terms *)
   438 
   439 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   440   | fold_atyps f T = f T;
   441 
   442 fun fold_atyps_sorts f =
   443   fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
   444 
   445 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   446   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   447   | fold_aterms f a = f a;
   448 
   449 fun fold_term_types f (t as Const (_, T)) = f t T
   450   | fold_term_types f (t as Free (_, T)) = f t T
   451   | fold_term_types f (t as Var (_, T)) = f t T
   452   | fold_term_types f (Bound _) = I
   453   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   454   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
   455 
   456 fun fold_types f = fold_term_types (K f);
   457 
   458 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
   459   | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
   460   | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
   461   | replace_types (Bound i) Ts = (Bound i, Ts)
   462   | replace_types (Abs (x, _, b)) (T :: Ts) =
   463       let val (b', Ts') = replace_types b Ts
   464       in (Abs (x, T, b'), Ts') end
   465   | replace_types (t $ u) Ts =
   466       let
   467         val (t', Ts') = replace_types t Ts;
   468         val (u', Ts'') = replace_types u Ts';
   469       in (t' $ u', Ts'') end;
   470 
   471 fun burrow_types f ts =
   472   let
   473     val Ts = rev ((fold o fold_types) cons ts []);
   474     val Ts' = f Ts;
   475     val (ts', []) = fold_map replace_types ts Ts';
   476   in ts' end;
   477 
   478 (*collect variables*)
   479 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
   480 val add_tvar_names = fold_types add_tvar_namesT;
   481 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
   482 val add_tvars = fold_types add_tvarsT;
   483 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
   484 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
   485 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
   486 val add_tfree_names = fold_types add_tfree_namesT;
   487 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
   488 val add_tfrees = fold_types add_tfreesT;
   489 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
   490 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
   491 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
   492 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
   493 
   494 (*extra type variables in a term, not covered by its type*)
   495 fun hidden_polymorphism t =
   496   let
   497     val T = fastype_of t;
   498     val tvarsT = add_tvarsT T [];
   499     val extra_tvars = fold_types (fold_atyps
   500       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   501   in extra_tvars end;
   502 
   503 
   504 (* renaming variables *)
   505 
   506 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
   507 
   508 fun declare_term_names tm =
   509   fold_aterms
   510     (fn Const (a, _) => Name.declare (Long_Name.base_name a)
   511       | Free (a, _) => Name.declare a
   512       | _ => I) tm #>
   513   fold_types declare_typ_names tm;
   514 
   515 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
   516 
   517 fun variant_frees t frees =
   518   fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
   519     map snd frees;
   520 
   521 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
   522 
   523 
   524 
   525 (** Comparing terms **)
   526 
   527 (* variables *)
   528 
   529 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
   530 
   531 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
   532 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
   533 
   534 
   535 (* alpha equivalence *)
   536 
   537 fun tm1 aconv tm2 =
   538   pointer_eq (tm1, tm2) orelse
   539     (case (tm1, tm2) of
   540       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
   541     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
   542     | (a1, a2) => a1 = a2);
   543 
   544 fun aconv_untyped (tm1, tm2) =
   545   pointer_eq (tm1, tm2) orelse
   546     (case (tm1, tm2) of
   547       (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
   548     | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
   549     | (Const (a, _), Const (b, _)) => a = b
   550     | (Free (x, _), Free (y, _)) => x = y
   551     | (Var (xi, _), Var (yj, _)) => xi = yj
   552     | (Bound i, Bound j) => i = j
   553     | _ => false);
   554 
   555 
   556 (*A fast unification filter: true unless the two terms cannot be unified.
   557   Terms must be NORMAL.  Treats all Vars as distinct. *)
   558 fun could_unify (t, u) =
   559   let
   560     fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
   561       | matchrands _ _ = true;
   562   in
   563     case (head_of t, head_of u) of
   564       (_, Var _) => true
   565     | (Var _, _) => true
   566     | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
   567     | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
   568     | (Bound i, Bound j) => i = j andalso matchrands t u
   569     | (Abs _, _) => true   (*because of possible eta equality*)
   570     | (_, Abs _) => true
   571     | _ => false
   572   end;
   573 
   574 
   575 
   576 (** Connectives of higher order logic **)
   577 
   578 fun aT S = TFree (Name.aT, S);
   579 
   580 fun itselfT ty = Type ("itself", [ty]);
   581 val a_itselfT = itselfT (TFree (Name.aT, []));
   582 
   583 val propT : typ = Type ("prop",[]);
   584 
   585 (*maps  !!x1...xn. t   to   t*)
   586 fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
   587   | strip_all_body t = t;
   588 
   589 (*maps  !!x1...xn. t   to   [x1, ..., xn]*)
   590 fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
   591   | strip_all_vars t = [];
   592 
   593 (*increments a term's non-local bound variables
   594   required when moving a term within abstractions
   595      inc is  increment for bound variables
   596      lev is  level at which a bound variable is considered 'loose'*)
   597 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   598   | incr_bv (inc, lev, Abs(a,T,body)) =
   599         Abs(a, T, incr_bv(inc,lev+1,body))
   600   | incr_bv (inc, lev, f$t) =
   601       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   602   | incr_bv (inc, lev, u) = u;
   603 
   604 fun incr_boundvars  0  t = t
   605   | incr_boundvars inc t = incr_bv(inc,0,t);
   606 
   607 (*Scan a pair of terms; while they are similar,
   608   accumulate corresponding bound vars in "al"*)
   609 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
   610       match_bvs(s, t, if x="" orelse y="" then al
   611                                           else (x,y)::al)
   612   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   613   | match_bvs(_,_,al) = al;
   614 
   615 (* strip abstractions created by parameters *)
   616 fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
   617 
   618 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   619   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   620   | map_abs_vars f t = t;
   621 
   622 fun rename_abs pat obj t =
   623   let
   624     val ren = match_bvs (pat, obj, []);
   625     fun ren_abs (Abs (x, T, b)) =
   626           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
   627       | ren_abs (f $ t) = ren_abs f $ ren_abs t
   628       | ren_abs t = t
   629   in if null ren then NONE else SOME (ren_abs t) end;
   630 
   631 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   632    (Bound 0) is loose at level 0 *)
   633 fun add_loose_bnos (Bound i, lev, js) =
   634         if i<lev then js else insert (op =) (i - lev) js
   635   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   636   | add_loose_bnos (f$t, lev, js) =
   637         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   638   | add_loose_bnos (_, _, js) = js;
   639 
   640 fun loose_bnos t = add_loose_bnos (t, 0, []);
   641 
   642 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
   643    level k or beyond. *)
   644 fun loose_bvar(Bound i,k) = i >= k
   645   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   646   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   647   | loose_bvar _ = false;
   648 
   649 fun loose_bvar1(Bound i,k) = i = k
   650   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   651   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   652   | loose_bvar1 _ = false;
   653 
   654 fun is_open t = loose_bvar (t, 0);
   655 fun is_dependent t = loose_bvar1 (t, 0);
   656 
   657 (*Substitute arguments for loose bound variables.
   658   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   659   Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
   660         and the appropriate call is  subst_bounds([b,a], c) .
   661   Loose bound variables >=n are reduced by "n" to
   662      compensate for the disappearance of lambdas.
   663 *)
   664 fun subst_bounds (args: term list, t) : term =
   665   let
   666     val n = length args;
   667     fun subst (t as Bound i, lev) =
   668          (if i < lev then raise Same.SAME   (*var is locally bound*)
   669           else incr_boundvars lev (nth args (i - lev))
   670             handle General.Subscript => Bound (i - n))  (*loose: change it*)
   671       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   672       | subst (f $ t, lev) =
   673           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   674             handle Same.SAME => f $ subst (t, lev))
   675       | subst _ = raise Same.SAME;
   676   in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
   677 
   678 (*Special case: one argument*)
   679 fun subst_bound (arg, t) : term =
   680   let
   681     fun subst (Bound i, lev) =
   682           if i < lev then raise Same.SAME   (*var is locally bound*)
   683           else if i = lev then incr_boundvars lev arg
   684           else Bound (i - 1)   (*loose: change it*)
   685       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
   686       | subst (f $ t, lev) =
   687           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
   688             handle Same.SAME => f $ subst (t, lev))
   689       | subst _ = raise Same.SAME;
   690   in subst (t, 0) handle Same.SAME => t end;
   691 
   692 (*beta-reduce if possible, else form application*)
   693 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   694   | betapply (f,u) = f$u;
   695 
   696 val betapplys = Library.foldl betapply;
   697 
   698 
   699 (*unfolding abstractions with substitution
   700   of bound variables and implicit eta-expansion*)
   701 fun strip_abs_eta k t =
   702   let
   703     val used = fold_aterms declare_term_frees t Name.context;
   704     fun strip_abs t (0, used) = (([], t), (0, used))
   705       | strip_abs (Abs (v, T, t)) (k, used) =
   706           let
   707             val (v', used') = Name.variant v used;
   708             val t' = subst_bound (Free (v', T), t);
   709             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
   710           in (((v', T) :: vs, t''), (k', used'')) end
   711       | strip_abs t (k, used) = (([], t), (k, used));
   712     fun expand_eta [] t _ = ([], t)
   713       | expand_eta (T::Ts) t used =
   714           let
   715             val (v, used') = Name.variant "" used;
   716             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
   717           in ((v, T) :: vs, t') end;
   718     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
   719     val Ts = fst (chop k' (binder_types (fastype_of t')));
   720     val (vs2, t'') = expand_eta Ts t' used';
   721   in (vs1 @ vs2, t'') end;
   722 
   723 
   724 (*Substitute new for free occurrences of old in a term*)
   725 fun subst_free [] = I
   726   | subst_free pairs =
   727       let fun substf u =
   728             case AList.lookup (op aconv) pairs u of
   729                 SOME u' => u'
   730               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
   731                                  | t$u' => substf t $ substf u'
   732                                  | _ => u)
   733       in  substf  end;
   734 
   735 (*Abstraction of the term "body" over its occurrences of v,
   736     which must contain no loose bound variables.
   737   The resulting term is ready to become the body of an Abs.*)
   738 fun abstract_over (v, body) =
   739   let
   740     fun abs lev tm =
   741       if v aconv tm then Bound lev
   742       else
   743         (case tm of
   744           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
   745         | t $ u =>
   746             (abs lev t $ (abs lev u handle Same.SAME => u)
   747               handle Same.SAME => t $ abs lev u)
   748         | _ => raise Same.SAME);
   749   in abs 0 body handle Same.SAME => body end;
   750 
   751 fun term_name (Const (x, _)) = Long_Name.base_name x
   752   | term_name (Free (x, _)) = x
   753   | term_name (Var ((x, _), _)) = x
   754   | term_name _ = Name.uu;
   755 
   756 fun dependent_lambda_name (x, v) t =
   757   let val t' = abstract_over (v, t)
   758   in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
   759 
   760 fun lambda_name (x, v) t =
   761   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
   762 
   763 fun lambda v t = lambda_name ("", v) t;
   764 
   765 fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
   766 fun absdummy T body = Abs (Name.uu_, T, body);
   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 ("Pure.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 fold_subtypes f =
   886   let
   887     fun iter ty =
   888       (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty);
   889   in iter end;
   890 
   891 fun exists_subtype P =
   892   let
   893     fun ex ty = P ty orelse
   894       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   895   in ex end;
   896 
   897 fun exists_type P =
   898   let
   899     fun ex (Const (_, T)) = P T
   900       | ex (Free (_, T)) = P T
   901       | ex (Var (_, T)) = P T
   902       | ex (Bound _) = false
   903       | ex (Abs (_, T, t)) = P T orelse ex t
   904       | ex (t $ u) = ex t orelse ex u;
   905   in ex end;
   906 
   907 fun exists_subterm P =
   908   let
   909     fun ex tm = P tm orelse
   910       (case tm of
   911         t $ u => ex t orelse ex u
   912       | Abs (_, _, t) => ex t
   913       | _ => false);
   914   in ex end;
   915 
   916 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   917 
   918 
   919 (* contraction *)
   920 
   921 fun could_beta_contract (Abs _ $ _) = true
   922   | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u
   923   | could_beta_contract (Abs (_, _, b)) = could_beta_contract b
   924   | could_beta_contract _ = false;
   925 
   926 fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true
   927   | could_eta_contract (Abs (_, _, b)) = could_eta_contract b
   928   | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u
   929   | could_eta_contract _ = false;
   930 
   931 fun could_beta_eta_contract (Abs _ $ _) = true
   932   | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true
   933   | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b
   934   | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u
   935   | could_beta_eta_contract _ = false;
   936 
   937 
   938 (* dest abstraction *)
   939 
   940 fun dest_abs (x, T, body) =
   941   let
   942     fun name_clash (Free (y, _)) = (x = y)
   943       | name_clash (t $ u) = name_clash t orelse name_clash u
   944       | name_clash (Abs (_, _, t)) = name_clash t
   945       | name_clash _ = false;
   946   in
   947     if name_clash body then
   948       dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
   949     else (x, subst_bound (Free (x, T), body))
   950   end;
   951 
   952 
   953 (* dummy patterns *)
   954 
   955 fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
   956 val dummy = dummy_pattern dummyT;
   957 val dummy_prop = dummy_pattern propT;
   958 
   959 fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
   960   | is_dummy_pattern _ = false;
   961 
   962 fun no_dummy_patterns tm =
   963   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   964   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   965 
   966 fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
   967       let val [x] = Name.invent used Name.uu 1
   968       in (Free (Name.internal x, T), Name.declare x used) end
   969   | free_dummy_patterns (Abs (x, T, b)) used =
   970       let val (b', used') = free_dummy_patterns b used
   971       in (Abs (x, T, b'), used') end
   972   | free_dummy_patterns (t $ u) used =
   973       let
   974         val (t', used') = free_dummy_patterns t used;
   975         val (u', used'') = free_dummy_patterns u used';
   976       in (t' $ u', used'') end
   977   | free_dummy_patterns a used = (a, used);
   978 
   979 fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
   980       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   981   | replace_dummy Ts (Abs (x, T, t)) i =
   982       let val (t', i') = replace_dummy (T :: Ts) t i
   983       in (Abs (x, T, t'), i') end
   984   | replace_dummy Ts (t $ u) i =
   985       let
   986         val (t', i') = replace_dummy Ts t i;
   987         val (u', i'') = replace_dummy Ts u i';
   988       in (t' $ u', i'') end
   989   | replace_dummy _ a i = (a, i);
   990 
   991 val replace_dummy_patterns = replace_dummy [];
   992 
   993 fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
   994   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   995   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   996   | show_dummy_patterns a = a;
   997 
   998 
   999 (* display variables *)
  1000 
  1001 fun string_of_vname (x, i) =
  1002   let
  1003     val idx = string_of_int i;
  1004     val dot =
  1005       (case rev (Symbol.explode x) of
  1006         _ :: "\<^sub>" :: _ => false
  1007       | c :: _ => Symbol.is_digit c
  1008       | _ => true);
  1009   in
  1010     if dot then "?" ^ x ^ "." ^ idx
  1011     else if i <> 0 then "?" ^ x ^ idx
  1012     else "?" ^ x
  1013   end;
  1014 
  1015 fun string_of_vname' (x, ~1) = x
  1016   | string_of_vname' xi = string_of_vname xi;
  1017 
  1018 end;
  1019 
  1020 structure Basic_Term: BASIC_TERM = Term;
  1021 open Basic_Term;