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