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