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