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