src/Pure/logic.ML
author wenzelm
Sat Feb 18 18:08:23 2006 +0100 (2006-02-18)
changeset 19103 0eb600479944
parent 19071 fdffd7c40864
child 19125 59b26248547b
permissions -rw-r--r--
dest_def: tuned error msg;
     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 fun term_kind (Const _) = "existing constant "
   206   | term_kind (Free _) = "free variable "
   207   | term_kind (Bound _) = "bound variable "
   208   | term_kind _ = "";
   209 
   210 (*c x == t[x] to !!x. c x == t[x]*)
   211 fun dest_def pp check_head is_fixed is_fixedT eq =
   212   let
   213     fun err msg = raise TERM (msg, [eq]);
   214     val eq_vars = Term.strip_all_vars eq;
   215     val eq_body = Term.strip_all_body eq;
   216 
   217     val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
   218     val display_types = commas_quote o map (Pretty.string_of_typ pp);
   219 
   220     val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
   221     val lhs = Envir.beta_eta_contract raw_lhs;
   222     val (head, args) = Term.strip_comb lhs;
   223     val head_tfrees = Term.add_tfrees head [];
   224 
   225     fun check_arg (Bound _) = true
   226       | check_arg (Free (x, _)) = not (is_fixed x)
   227       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   228       | check_arg _ = false;
   229     fun close_arg (Bound _) t = t
   230       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
   231 
   232     val lhs_bads = filter_out check_arg args;
   233     val lhs_dups = duplicates (op aconv) args;
   234     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   235       if is_fixed x orelse member (op aconv) args v then I
   236       else insert (op aconv) v | _ => I) rhs [];
   237     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
   238       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   239       else insert (op =) v | _ => I)) rhs [];
   240   in
   241     if not (check_head head) then
   242       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
   243     else if not (null lhs_bads) then
   244       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   245     else if not (null lhs_dups) then
   246       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   247     else if not (null rhs_extras) then
   248       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   249     else if not (null rhs_extrasT) then
   250       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   251     else if exists_subterm (fn t => t aconv head) rhs then
   252       err "Entity to be defined occurs on rhs"
   253     else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
   254   end;
   255 
   256 (*!!x. c x == t[x] to c == %x. t[x]*)
   257 fun abs_def eq =
   258   let
   259     val body = Term.strip_all_body eq;
   260     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   261     val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   262     val (lhs', args) = Term.strip_comb lhs;
   263     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   264   in (lhs', rhs') end;
   265 
   266 fun mk_cond_defpair As (lhs, rhs) =
   267   (case Term.head_of lhs of
   268     Const (name, _) =>
   269       (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   270   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   271 
   272 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   273 
   274 
   275 (** protected propositions **)
   276 
   277 val protectC = Const ("prop", propT --> propT);
   278 fun protect t = protectC $ t;
   279 
   280 fun unprotect (Const ("prop", _) $ t) = t
   281   | unprotect t = raise TERM ("unprotect", [t]);
   282 
   283 
   284 
   285 (*** Low-level term operations ***)
   286 
   287 (*Does t occur in u?  Or is alpha-convertible to u?
   288   The term t must contain no loose bound variables*)
   289 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   290 
   291 (*Close up a formula over all free variables by quantification*)
   292 fun close_form A =
   293   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   294 
   295 
   296 
   297 (*** Specialized operations for resolution... ***)
   298 
   299 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   300 fun combound (t, n, k) =
   301     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   302 
   303 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   304 fun rlist_abs ([], body) = body
   305   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   306 
   307 
   308 local exception SAME in
   309 
   310 fun incrT k =
   311   let
   312     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   313       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   314       | incr _ = raise SAME
   315     and incrs (T :: Ts) =
   316         (incr T :: (incrs Ts handle SAME => Ts)
   317           handle SAME => T :: incrs Ts)
   318       | incrs [] = raise SAME;
   319   in incr end;
   320 
   321 (*For all variables in the term, increment indexnames and lift over the Us
   322     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   323 fun incr_indexes ([], 0) t = t
   324   | incr_indexes (Ts, k) t =
   325   let
   326     val n = length Ts;
   327     val incrT = if k = 0 then I else incrT k;
   328 
   329     fun incr lev (Var ((x, i), T)) =
   330           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   331       | incr lev (Abs (x, T, body)) =
   332           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   333             handle SAME => Abs (x, T, incr (lev + 1) body))
   334       | incr lev (t $ u) =
   335           (incr lev t $ (incr lev u handle SAME => u)
   336             handle SAME => t $ incr lev u)
   337       | incr _ (Const (c, T)) = Const (c, incrT T)
   338       | incr _ (Free (x, T)) = Free (x, incrT T)
   339       | incr _ (t as Bound _) = t;
   340   in incr 0 t handle SAME => t end;
   341 
   342 fun incr_tvar 0 T = T
   343   | incr_tvar k T = incrT k T handle SAME => T;
   344 
   345 end;
   346 
   347 
   348 (* Lifting functions from subgoal and increment:
   349     lift_abs operates on terms
   350     lift_all operates on propositions *)
   351 
   352 fun lift_abs inc =
   353   let
   354     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   355       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   356       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   357   in lift [] end;
   358 
   359 fun lift_all inc =
   360   let
   361     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   362       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   363       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   364   in lift [] end;
   365 
   366 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   367 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   368   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   369   | strip_assums_hyp B = [];
   370 
   371 (*Strips assumptions in goal, yielding conclusion.   *)
   372 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   373   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   374   | strip_assums_concl B = B;
   375 
   376 (*Make a list of all the parameters in a subgoal, even if nested*)
   377 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   378   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   379   | strip_params B = [];
   380 
   381 (*test for meta connectives in prems of a 'subgoal'*)
   382 fun has_meta_prems prop i =
   383   let
   384     fun is_meta (Const ("==>", _) $ _ $ _) = true
   385       | is_meta (Const ("==", _) $ _ $ _) = true
   386       | is_meta (Const ("all", _) $ _) = true
   387       | is_meta _ = false;
   388   in
   389     (case strip_prems (i, [], prop) of
   390       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   391     | _ => false) handle TERM _ => false
   392   end;
   393 
   394 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   395     where j is the total number of parameters (precomputed)
   396   If n>0 then deletes assumption n. *)
   397 fun remove_params j n A =
   398     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   399     else case A of
   400         Const("==>", _) $ H $ B =>
   401           if n=1 then                           (remove_params j (n-1) B)
   402           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   403       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   404       | _ => if n>0 then raise TERM("remove_params", [A])
   405              else A;
   406 
   407 (** Auto-renaming of parameters in subgoals **)
   408 
   409 val auto_rename = ref false
   410 and rename_prefix = ref "ka";
   411 
   412 (*rename_prefix is not exported; it is set by this function.*)
   413 fun set_rename_prefix a =
   414     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   415     then  (rename_prefix := a;  auto_rename := true)
   416     else  error"rename prefix must be nonempty and consist of letters";
   417 
   418 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   419   A name clash could cause the printer to rename bound vars;
   420     then res_inst_tac would not work properly.*)
   421 fun rename_vars (a, []) = []
   422   | rename_vars (a, (_,T)::vars) =
   423         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   424 
   425 (*Move all parameters to the front of the subgoal, renaming them apart;
   426   if n>0 then deletes assumption n. *)
   427 fun flatten_params n A =
   428     let val params = strip_params A;
   429         val vars = if !auto_rename
   430                    then rename_vars (!rename_prefix, params)
   431                    else ListPair.zip (variantlist(map #1 params,[]),
   432                                       map #2 params)
   433     in  list_all (vars, remove_params (length vars) n A)
   434     end;
   435 
   436 (*Makes parameters in a goal have the names supplied by the list cs.*)
   437 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   438       implies $ A $ list_rename_params (cs, B)
   439   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   440       all T $ Abs(c, T, list_rename_params (cs, t))
   441   | list_rename_params (cs, B) = B;
   442 
   443 (*** Treatmsent of "assume", "erule", etc. ***)
   444 
   445 (*Strips assumptions in goal yielding
   446    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   447   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   448   the the parameters to be flattened, but it allows erule to work on
   449   assumptions of the form !!x. phi. Any !! after the outermost string
   450   will be regarded as belonging to the conclusion, and left untouched.
   451   Used ONLY by assum_pairs.
   452       Unless nasms<0, it can terminate the recursion early; that allows
   453   erule to work on assumptions of the form P==>Q.*)
   454 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   455   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   456       strip_assums_imp (nasms-1, H::Hs, B)
   457   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   458 
   459 
   460 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   461 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   462       strip_assums_all ((a,T)::params, t)
   463   | strip_assums_all (params, B) = (params, B);
   464 
   465 (*Produces disagreement pairs, one for each assumption proof, in order.
   466   A is the first premise of the lifted rule, and thus has the form
   467     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   468   nasms is the number of assumptions in the original subgoal, needed when B
   469     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   470 fun assum_pairs(nasms,A) =
   471   let val (params, A') = strip_assums_all ([],A)
   472       val (Hs,B) = strip_assums_imp (nasms,[],A')
   473       fun abspar t = rlist_abs(params, t)
   474       val D = abspar B
   475       fun pairrev ([], pairs) = pairs
   476         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   477   in  pairrev (Hs,[])
   478   end;
   479 
   480 (*Converts Frees to Vars and TFrees to TVars*)
   481 fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   482   | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   483   | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   484   | varify (t as Bound _) = t
   485   | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   486   | varify (f $ t) = varify f $ varify t;
   487 
   488 (*Inverse of varify.*)
   489 fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   490   | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   491   | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
   492   | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
   493   | unvarify (t as Bound _) = t
   494   | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
   495   | unvarify (f $ t) = unvarify f $ unvarify t;
   496 
   497 
   498 (* goal states *)
   499 
   500 fun get_goal st i = nth_prem (i, st)
   501   handle TERM _ => error "Goal number out of range";
   502 
   503 (*reverses parameters for substitution*)
   504 fun goal_params st i =
   505   let val gi = get_goal st i
   506       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   507   in (gi, rfrees) end;
   508 
   509 fun concl_of_goal st i =
   510   let val (gi, rfrees) = goal_params st i
   511       val B = strip_assums_concl gi
   512   in subst_bounds (rfrees, B) end;
   513 
   514 fun prems_of_goal st i =
   515   let val (gi, rfrees) = goal_params st i
   516       val As = strip_assums_hyp gi
   517   in map (fn A => subst_bounds (rfrees, A)) As end;
   518 
   519 end;