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