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