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