src/Pure/logic.ML
author wenzelm
Tue Feb 07 19:56:45 2006 +0100 (2006-02-07)
changeset 18964 67f572e03236
parent 18938 b401ee1cda14
child 19071 fdffd7c40864
permissions -rw-r--r--
renamed gen_duplicates to duplicates;
     1 (*  Title:      Pure/logic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Abstract syntax operations of the Pure meta-logic.
     7 *)
     8 
     9 signature LOGIC =
    10 sig
    11   val is_all: term -> bool
    12   val dest_all: term -> typ * term
    13   val mk_equals: term * term -> term
    14   val dest_equals: term -> term * term
    15   val is_equals: term -> bool
    16   val mk_implies: term * term -> term
    17   val dest_implies: term -> term * term
    18   val is_implies: term -> bool
    19   val list_implies: term list * term -> term
    20   val strip_imp_prems: term -> term list
    21   val strip_imp_concl: term -> term
    22   val strip_prems: int * term list * term -> term list * term
    23   val count_prems: term * int -> int
    24   val nth_prem: int * term -> term
    25   val mk_conjunction: term * term -> term
    26   val mk_conjunction_list: term list -> term
    27   val mk_conjunction_list2: term list list -> term
    28   val dest_conjunction: term -> term * term
    29   val dest_conjunctions: term -> term list
    30   val strip_horn: term -> term list * term
    31   val dest_type: term -> typ
    32   val const_of_class: class -> string
    33   val class_of_const: string -> class
    34   val mk_inclass: typ * class -> term
    35   val dest_inclass: term -> typ * class
    36   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    37     term -> (term * term) * term
    38   val abs_def: term -> term * term
    39   val mk_cond_defpair: term list -> term * term -> string * term
    40   val mk_defpair: term * term -> string * term
    41   val mk_type: typ -> term
    42   val protectC: term
    43   val protect: term -> term
    44   val unprotect: term -> term
    45   val occs: term * term -> bool
    46   val close_form: term -> term
    47   val combound: term * int * int -> term
    48   val rlist_abs: (string * typ) list * term -> term
    49   val incr_indexes: typ list * int -> term -> term
    50   val incr_tvar: int -> typ -> typ
    51   val lift_abs: int -> term -> term -> term
    52   val lift_all: int -> term -> term -> term
    53   val strip_assums_hyp: term -> term list
    54   val strip_assums_concl: term -> term
    55   val strip_params: term -> (string * typ) list
    56   val has_meta_prems: term -> int -> bool
    57   val flatten_params: int -> term -> term
    58   val auto_rename: bool ref
    59   val set_rename_prefix: string -> unit
    60   val list_rename_params: string list * term -> term
    61   val assum_pairs: int * term -> (term*term)list
    62   val varify: term -> term
    63   val unvarify: term -> term
    64   val get_goal: term -> int -> term
    65   val goal_params: term -> int -> term * term list
    66   val prems_of_goal: term -> int -> term list
    67   val concl_of_goal: term -> int -> term
    68 end;
    69 
    70 structure Logic : LOGIC =
    71 struct
    72 
    73 
    74 (*** Abstract syntax operations on the meta-connectives ***)
    75 
    76 (** all **)
    77 
    78 fun is_all (Const ("all", _) $ _) = true
    79   | is_all _ = false;
    80 
    81 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    82   | dest_all t = raise TERM ("dest_all", [t]);
    83 
    84 
    85 
    86 (** equality **)
    87 
    88 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
    89 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    90 
    91 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    92   | dest_equals t = raise TERM("dest_equals", [t]);
    93 
    94 fun is_equals (Const ("==", _) $ _ $ _) = true
    95   | is_equals _ = false;
    96 
    97 
    98 (** implies **)
    99 
   100 fun mk_implies(A,B) = implies $ A $ B;
   101 
   102 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
   103   | dest_implies A = raise TERM("dest_implies", [A]);
   104 
   105 fun is_implies (Const ("==>", _) $ _ $ _) = true
   106   | is_implies _ = false;
   107 
   108 
   109 (** nested implications **)
   110 
   111 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   112 fun list_implies ([], B) = B
   113   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   114 
   115 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   116 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   117   | strip_imp_prems _ = [];
   118 
   119 (* A1==>...An==>B  goes to B, where B is not an implication *)
   120 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   121   | strip_imp_concl A = A : term;
   122 
   123 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   124     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   125   if  i<0 or else i too big then raises  TERM*)
   126 fun strip_prems (0, As, B) = (As, B)
   127   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   128         strip_prems (i-1, A::As, B)
   129   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   130 
   131 (*Count premises -- quicker than (length o strip_prems) *)
   132 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   133   | count_prems (_,n) = n;
   134 
   135 (*Select Ai from A1 ==>...Ai==>B*)
   136 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   137   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   138   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   139 
   140 (*strip a proof state (Horn clause):
   141   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   142 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   143 
   144 
   145 (** conjunction **)
   146 
   147 (*A && B*)
   148 fun mk_conjunction (t, u) =
   149   Term.list_all ([("X", propT)],
   150     mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
   151 
   152 (*A && B && C -- improper*)
   153 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   154   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   155 
   156 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   157 fun mk_conjunction_list2 tss =
   158   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
   159 
   160 (*A && B*)
   161 fun dest_conjunction
   162       (t as Const ("all", _) $ Abs (_, _,
   163         Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
   164       if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0)
   165       then raise TERM ("dest_conjunction", [t])
   166       else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
   167   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   168 
   169 (*((A && B) && C) && D && E -- flat*)
   170 fun dest_conjunctions t =
   171   (case try dest_conjunction t of
   172     NONE => [t]
   173   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   174 
   175 
   176 
   177 (** types as terms **)
   178 
   179 fun mk_type ty = Const ("TYPE", itselfT ty);
   180 
   181 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   182   | dest_type t = raise TERM ("dest_type", [t]);
   183 
   184 
   185 (** class constraints **)
   186 
   187 val classN = "_class";
   188 
   189 val const_of_class = suffix classN;
   190 fun class_of_const c = unsuffix classN c
   191   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   192 
   193 fun mk_inclass (ty, c) =
   194   Const (const_of_class c, itselfT ty --> propT) $ mk_type ty;
   195 
   196 fun dest_inclass (t as Const (c_class, _) $ ty) =
   197       ((dest_type ty, class_of_const c_class)
   198         handle TERM _ => raise TERM ("dest_inclass", [t]))
   199   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   200 
   201 
   202 
   203 (** definitions **)
   204 
   205 (*c x == t[x] to !!x. c x == t[x]*)
   206 fun dest_def pp check_head is_fixed is_fixedT eq =
   207   let
   208     fun err msg = raise TERM (msg, [eq]);
   209     val bound_vars = Syntax.bound_vars (Term.strip_all_vars eq);
   210     val display_terms = commas_quote o map (Pretty.string_of_term pp o bound_vars);
   211     val display_types = commas_quote o map (Pretty.string_of_typ pp);
   212 
   213     val (lhs, rhs) = dest_equals (Term.strip_all_body eq)
   214       handle TERM _ => err "Not a meta-equality (==)";
   215     val (head, args) = Term.strip_comb (Envir.beta_eta_contract lhs);
   216     val head_tfrees = Term.add_tfrees head [];
   217 
   218     fun check_arg (Bound _) = true
   219       | check_arg (Free (x, _)) = not (is_fixed x)
   220       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   221       | check_arg _ = false;
   222     fun close_arg (Bound _) t = t
   223       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
   224 
   225     val lhs_bads = filter_out check_arg args;
   226     val lhs_dups = duplicates (op aconv) args;
   227     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   228       if is_fixed x orelse member (op aconv) args v then I
   229       else insert (op aconv) v | _ => I) rhs [];
   230     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
   231       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   232       else insert (op =) v | _ => I)) rhs [];
   233   in
   234     if not (check_head head) then
   235       err ("Bad head of lhs: " ^ display_terms [head])
   236     else if not (null lhs_bads) then
   237       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   238     else if not (null lhs_dups) then
   239       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   240     else if not (null rhs_extras) then
   241       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   242     else if not (null rhs_extrasT) then
   243       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   244     else if exists_subterm (fn t => t aconv head) rhs then
   245       err "Entity to be defined occurs on rhs"
   246     else ((lhs, rhs), fold_rev close_arg args eq)
   247   end;
   248 
   249 (*!!x. c x == t[x] to c == %x. t[x]*)
   250 fun abs_def eq =
   251   let
   252     val body = Term.strip_all_body eq;
   253     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   254     val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   255     val (lhs', args) = Term.strip_comb lhs;
   256     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   257   in (lhs', rhs') end;
   258 
   259 fun mk_cond_defpair As (lhs, rhs) =
   260   (case Term.head_of lhs of
   261     Const (name, _) =>
   262       (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   263   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   264 
   265 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   266 
   267 
   268 (** protected propositions **)
   269 
   270 val protectC = Const ("prop", propT --> propT);
   271 fun protect t = protectC $ t;
   272 
   273 fun unprotect (Const ("prop", _) $ t) = t
   274   | unprotect t = raise TERM ("unprotect", [t]);
   275 
   276 
   277 
   278 (*** Low-level term operations ***)
   279 
   280 (*Does t occur in u?  Or is alpha-convertible to u?
   281   The term t must contain no loose bound variables*)
   282 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   283 
   284 (*Close up a formula over all free variables by quantification*)
   285 fun close_form A =
   286   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   287 
   288 
   289 
   290 (*** Specialized operations for resolution... ***)
   291 
   292 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   293 fun combound (t, n, k) =
   294     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   295 
   296 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   297 fun rlist_abs ([], body) = body
   298   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   299 
   300 
   301 local exception SAME in
   302 
   303 fun incrT k =
   304   let
   305     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   306       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   307       | incr _ = raise SAME
   308     and incrs (T :: Ts) =
   309         (incr T :: (incrs Ts handle SAME => Ts)
   310           handle SAME => T :: incrs Ts)
   311       | incrs [] = raise SAME;
   312   in incr end;
   313 
   314 (*For all variables in the term, increment indexnames and lift over the Us
   315     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   316 fun incr_indexes ([], 0) t = t
   317   | incr_indexes (Ts, k) t =
   318   let
   319     val n = length Ts;
   320     val incrT = if k = 0 then I else incrT k;
   321 
   322     fun incr lev (Var ((x, i), T)) =
   323           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   324       | incr lev (Abs (x, T, body)) =
   325           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   326             handle SAME => Abs (x, T, incr (lev + 1) body))
   327       | incr lev (t $ u) =
   328           (incr lev t $ (incr lev u handle SAME => u)
   329             handle SAME => t $ incr lev u)
   330       | incr _ (Const (c, T)) = Const (c, incrT T)
   331       | incr _ (Free (x, T)) = Free (x, incrT T)
   332       | incr _ (t as Bound _) = t;
   333   in incr 0 t handle SAME => t end;
   334 
   335 fun incr_tvar 0 T = T
   336   | incr_tvar k T = incrT k T handle SAME => T;
   337 
   338 end;
   339 
   340 
   341 (* Lifting functions from subgoal and increment:
   342     lift_abs operates on terms
   343     lift_all operates on propositions *)
   344 
   345 fun lift_abs inc =
   346   let
   347     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   348       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   349       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   350   in lift [] end;
   351 
   352 fun lift_all inc =
   353   let
   354     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   355       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   356       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   357   in lift [] end;
   358 
   359 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   360 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   361   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   362   | strip_assums_hyp B = [];
   363 
   364 (*Strips assumptions in goal, yielding conclusion.   *)
   365 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   366   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   367   | strip_assums_concl B = B;
   368 
   369 (*Make a list of all the parameters in a subgoal, even if nested*)
   370 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   371   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   372   | strip_params B = [];
   373 
   374 (*test for meta connectives in prems of a 'subgoal'*)
   375 fun has_meta_prems prop i =
   376   let
   377     fun is_meta (Const ("==>", _) $ _ $ _) = true
   378       | is_meta (Const ("==", _) $ _ $ _) = true
   379       | is_meta (Const ("all", _) $ _) = true
   380       | is_meta _ = false;
   381   in
   382     (case strip_prems (i, [], prop) of
   383       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   384     | _ => false) handle TERM _ => false
   385   end;
   386 
   387 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   388     where j is the total number of parameters (precomputed)
   389   If n>0 then deletes assumption n. *)
   390 fun remove_params j n A =
   391     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   392     else case A of
   393         Const("==>", _) $ H $ B =>
   394           if n=1 then                           (remove_params j (n-1) B)
   395           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   396       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   397       | _ => if n>0 then raise TERM("remove_params", [A])
   398              else A;
   399 
   400 (** Auto-renaming of parameters in subgoals **)
   401 
   402 val auto_rename = ref false
   403 and rename_prefix = ref "ka";
   404 
   405 (*rename_prefix is not exported; it is set by this function.*)
   406 fun set_rename_prefix a =
   407     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   408     then  (rename_prefix := a;  auto_rename := true)
   409     else  error"rename prefix must be nonempty and consist of letters";
   410 
   411 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   412   A name clash could cause the printer to rename bound vars;
   413     then res_inst_tac would not work properly.*)
   414 fun rename_vars (a, []) = []
   415   | rename_vars (a, (_,T)::vars) =
   416         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   417 
   418 (*Move all parameters to the front of the subgoal, renaming them apart;
   419   if n>0 then deletes assumption n. *)
   420 fun flatten_params n A =
   421     let val params = strip_params A;
   422         val vars = if !auto_rename
   423                    then rename_vars (!rename_prefix, params)
   424                    else ListPair.zip (variantlist(map #1 params,[]),
   425                                       map #2 params)
   426     in  list_all (vars, remove_params (length vars) n A)
   427     end;
   428 
   429 (*Makes parameters in a goal have the names supplied by the list cs.*)
   430 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   431       implies $ A $ list_rename_params (cs, B)
   432   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   433       all T $ Abs(c, T, list_rename_params (cs, t))
   434   | list_rename_params (cs, B) = B;
   435 
   436 (*** Treatmsent of "assume", "erule", etc. ***)
   437 
   438 (*Strips assumptions in goal yielding
   439    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   440   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   441   the the parameters to be flattened, but it allows erule to work on
   442   assumptions of the form !!x. phi. Any !! after the outermost string
   443   will be regarded as belonging to the conclusion, and left untouched.
   444   Used ONLY by assum_pairs.
   445       Unless nasms<0, it can terminate the recursion early; that allows
   446   erule to work on assumptions of the form P==>Q.*)
   447 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   448   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   449       strip_assums_imp (nasms-1, H::Hs, B)
   450   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   451 
   452 
   453 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   454 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   455       strip_assums_all ((a,T)::params, t)
   456   | strip_assums_all (params, B) = (params, B);
   457 
   458 (*Produces disagreement pairs, one for each assumption proof, in order.
   459   A is the first premise of the lifted rule, and thus has the form
   460     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   461   nasms is the number of assumptions in the original subgoal, needed when B
   462     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   463 fun assum_pairs(nasms,A) =
   464   let val (params, A') = strip_assums_all ([],A)
   465       val (Hs,B) = strip_assums_imp (nasms,[],A')
   466       fun abspar t = rlist_abs(params, t)
   467       val D = abspar B
   468       fun pairrev ([], pairs) = pairs
   469         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   470   in  pairrev (Hs,[])
   471   end;
   472 
   473 (*Converts Frees to Vars and TFrees to TVars*)
   474 fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   475   | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   476   | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   477   | varify (t as Bound _) = t
   478   | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   479   | varify (f $ t) = varify f $ varify t;
   480 
   481 (*Inverse of varify.*)
   482 fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   483   | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   484   | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
   485   | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
   486   | unvarify (t as Bound _) = t
   487   | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
   488   | unvarify (f $ t) = unvarify f $ unvarify t;
   489 
   490 
   491 (* goal states *)
   492 
   493 fun get_goal st i = nth_prem (i, st)
   494   handle TERM _ => error "Goal number out of range";
   495 
   496 (*reverses parameters for substitution*)
   497 fun goal_params st i =
   498   let val gi = get_goal st i
   499       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   500   in (gi, rfrees) end;
   501 
   502 fun concl_of_goal st i =
   503   let val (gi, rfrees) = goal_params st i
   504       val B = strip_assums_concl gi
   505   in subst_bounds (rfrees, B) end;
   506 
   507 fun prems_of_goal st i =
   508   let val (gi, rfrees) = goal_params st i
   509       val As = strip_assums_hyp gi
   510   in map (fn A => subst_bounds (rfrees, A)) As end;
   511 
   512 end;