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