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