src/Pure/logic.ML
author wenzelm
Wed Jun 13 00:02:00 2007 +0200 (2007-06-13)
changeset 23357 16e0ec4bcd81
parent 23238 3de6e253efc4
child 23418 c195f6f13769
permissions -rw-r--r--
removed unused is_atomic;
     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 dest_all: term -> typ * term
    12   val mk_equals: term * term -> term
    13   val dest_equals: term -> term * term
    14   val mk_implies: term * term -> term
    15   val dest_implies: term -> term * term
    16   val list_implies: term list * term -> term
    17   val strip_imp_prems: term -> term list
    18   val strip_imp_concl: term -> term
    19   val strip_prems: int * term list * term -> term list * term
    20   val count_prems: term -> int
    21   val nth_prem: int * term -> term
    22   val conjunction: term
    23   val mk_conjunction: term * term -> term
    24   val mk_conjunction_list: term list -> term
    25   val mk_conjunction_list2: term list list -> term
    26   val dest_conjunction: term -> term * term
    27   val dest_conjunction_list: term -> term list
    28   val dest_conjunctions: term -> term list
    29   val strip_horn: term -> term list * term
    30   val mk_type: typ -> term
    31   val dest_type: term -> typ
    32   val type_map: (term -> term) -> typ -> 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 name_classrel: string * string -> string
    38   val mk_classrel: class * class -> term
    39   val dest_classrel: term -> class * class
    40   val name_arities: arity -> string list
    41   val name_arity: string * sort list * class -> string
    42   val mk_arities: arity -> term list
    43   val dest_arity: term -> string * sort list * class
    44   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    45     term -> (term * term) * term
    46   val abs_def: term -> term * term
    47   val mk_defpair: term * term -> string * 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 dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    93   | dest_all t = raise TERM ("dest_all", [t]);
    94 
    95 
    96 (** equality **)
    97 
    98 fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
    99 
   100 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   101   | dest_equals t = raise TERM ("dest_equals", [t]);
   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 
   112 (** nested implications **)
   113 
   114 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   115 fun list_implies ([], B) = B
   116   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   117 
   118 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   119 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   120   | strip_imp_prems _ = [];
   121 
   122 (* A1==>...An==>B  goes to B, where B is not an implication *)
   123 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   124   | strip_imp_concl A = A : term;
   125 
   126 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   127     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   128   if  i<0 or else i too big then raises  TERM*)
   129 fun strip_prems (0, As, B) = (As, B)
   130   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   131         strip_prems (i-1, A::As, B)
   132   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   133 
   134 (*Count premises -- quicker than (length o strip_prems) *)
   135 fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
   136   | count_prems _ = 0;
   137 
   138 (*Select Ai from A1 ==>...Ai==>B*)
   139 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   140   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   141   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   142 
   143 (*strip a proof state (Horn clause):
   144   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   145 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   146 
   147 
   148 (** conjunction **)
   149 
   150 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
   151 
   152 (*A && B*)
   153 fun mk_conjunction (A, B) = conjunction $ A $ B;
   154 
   155 (*A && B && C -- improper*)
   156 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   157   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   158 
   159 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   160 fun mk_conjunction_list2 tss =
   161   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
   162 
   163 (*A && B*)
   164 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   165   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   166 
   167 (*A && B && C -- improper*)
   168 fun dest_conjunction_list t =
   169   (case try dest_conjunction t of
   170     NONE => [t]
   171   | SOME (A, B) => A :: dest_conjunction_list B);
   172 
   173 (*((A && B) && C) && D && E -- flat*)
   174 fun dest_conjunctions t =
   175   (case try dest_conjunction t of
   176     NONE => [t]
   177   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   178 
   179 
   180 
   181 (** types as terms **)
   182 
   183 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   184 
   185 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   186   | dest_type t = raise TERM ("dest_type", [t]);
   187 
   188 fun type_map f = dest_type o f o mk_type;
   189 
   190 
   191 
   192 (** type classes **)
   193 
   194 (* const names *)
   195 
   196 val classN = "_class";
   197 
   198 val const_of_class = suffix classN;
   199 
   200 fun class_of_const c = unsuffix classN c
   201   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   202 
   203 
   204 (* class constraints *)
   205 
   206 fun mk_inclass (ty, c) =
   207   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   208 
   209 fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   210   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   211 
   212 
   213 (* class relations *)
   214 
   215 fun name_classrel (c1, c2) =
   216   NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
   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 name_arities (t, _, S) =
   229   let val b = NameSpace.base t
   230   in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
   231 
   232 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   233 
   234 fun mk_arities (t, Ss, S) =
   235   let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'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_defpair (lhs, rhs) =
   318   (case Term.head_of lhs of
   319     Const (name, _) =>
   320       (NameSpace.base name ^ "_def", mk_equals (lhs, rhs))
   321   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   322 
   323 
   324 
   325 (** protected propositions and embedded terms **)
   326 
   327 val protectC = Const ("prop", propT --> propT);
   328 fun protect t = protectC $ t;
   329 
   330 fun unprotect (Const ("prop", _) $ t) = t
   331   | unprotect t = raise TERM ("unprotect", [t]);
   332 
   333 
   334 fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
   335 
   336 fun dest_term (Const ("ProtoPure.term", _) $ t) = t
   337   | dest_term t = raise TERM ("dest_term", [t]);
   338 
   339 
   340 
   341 (*** Low-level term operations ***)
   342 
   343 (*Does t occur in u?  Or is alpha-convertible to u?
   344   The term t must contain no loose bound variables*)
   345 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   346 
   347 (*Close up a formula over all free variables by quantification*)
   348 fun close_form A =
   349   Term.list_all_free (rev (Term.add_frees A []), A);
   350 
   351 
   352 
   353 (*** Specialized operations for resolution... ***)
   354 
   355 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   356 fun combound (t, n, k) =
   357     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   358 
   359 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   360 fun rlist_abs ([], body) = body
   361   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   362 
   363 
   364 local exception SAME in
   365 
   366 fun incrT k =
   367   let
   368     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   369       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   370       | incr _ = raise SAME
   371     and incrs (T :: Ts) =
   372         (incr T :: (incrs Ts handle SAME => Ts)
   373           handle SAME => T :: incrs Ts)
   374       | incrs [] = raise SAME;
   375   in incr end;
   376 
   377 (*For all variables in the term, increment indexnames and lift over the Us
   378     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   379 fun incr_indexes ([], 0) t = t
   380   | incr_indexes (Ts, k) t =
   381   let
   382     val n = length Ts;
   383     val incrT = if k = 0 then I else incrT k;
   384 
   385     fun incr lev (Var ((x, i), T)) =
   386           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   387       | incr lev (Abs (x, T, body)) =
   388           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   389             handle SAME => Abs (x, T, incr (lev + 1) body))
   390       | incr lev (t $ u) =
   391           (incr lev t $ (incr lev u handle SAME => u)
   392             handle SAME => t $ incr lev u)
   393       | incr _ (Const (c, T)) = Const (c, incrT T)
   394       | incr _ (Free (x, T)) = Free (x, incrT T)
   395       | incr _ (t as Bound _) = t;
   396   in incr 0 t handle SAME => t end;
   397 
   398 fun incr_tvar 0 T = T
   399   | incr_tvar k T = incrT k T handle SAME => T;
   400 
   401 end;
   402 
   403 
   404 (* Lifting functions from subgoal and increment:
   405     lift_abs operates on terms
   406     lift_all operates on propositions *)
   407 
   408 fun lift_abs inc =
   409   let
   410     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   411       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   412       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   413   in lift [] end;
   414 
   415 fun lift_all inc =
   416   let
   417     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   418       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   419       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   420   in lift [] end;
   421 
   422 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   423 fun strip_assums_hyp B =
   424   let
   425     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   426       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   427           strip (map (incr_boundvars 1) Hs) t
   428       | strip Hs B = rev Hs
   429   in strip [] B end;
   430 
   431 (*Strips assumptions in goal, yielding conclusion.   *)
   432 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   433   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   434   | strip_assums_concl B = B;
   435 
   436 (*Make a list of all the parameters in a subgoal, even if nested*)
   437 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   438   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   439   | strip_params B = [];
   440 
   441 (*test for meta connectives in prems of a 'subgoal'*)
   442 fun has_meta_prems prop i =
   443   let
   444     fun is_meta (Const ("==>", _) $ _ $ _) = true
   445       | is_meta (Const ("==", _) $ _ $ _) = true
   446       | is_meta (Const ("all", _) $ _) = true
   447       | is_meta _ = false;
   448   in
   449     (case strip_prems (i, [], prop) of
   450       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   451     | _ => false) handle TERM _ => false
   452   end;
   453 
   454 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   455     where j is the total number of parameters (precomputed)
   456   If n>0 then deletes assumption n. *)
   457 fun remove_params j n A =
   458     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   459     else case A of
   460         Const("==>", _) $ H $ B =>
   461           if n=1 then                           (remove_params j (n-1) B)
   462           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   463       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   464       | _ => if n>0 then raise TERM("remove_params", [A])
   465              else A;
   466 
   467 (** Auto-renaming of parameters in subgoals **)
   468 
   469 val auto_rename = ref false
   470 and rename_prefix = ref "ka";
   471 
   472 (*rename_prefix is not exported; it is set by this function.*)
   473 fun set_rename_prefix a =
   474     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   475     then  (rename_prefix := a;  auto_rename := true)
   476     else  error"rename prefix must be nonempty and consist of letters";
   477 
   478 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   479   A name clash could cause the printer to rename bound vars;
   480     then res_inst_tac would not work properly.*)
   481 fun rename_vars (a, []) = []
   482   | rename_vars (a, (_,T)::vars) =
   483         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   484 
   485 (*Move all parameters to the front of the subgoal, renaming them apart;
   486   if n>0 then deletes assumption n. *)
   487 fun flatten_params n A =
   488     let val params = strip_params A;
   489         val vars = if !auto_rename
   490                    then rename_vars (!rename_prefix, params)
   491                    else ListPair.zip (Name.variant_list [] (map #1 params),
   492                                       map #2 params)
   493     in  list_all (vars, remove_params (length vars) n A)
   494     end;
   495 
   496 (*Makes parameters in a goal have the names supplied by the list cs.*)
   497 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   498       implies $ A $ list_rename_params (cs, B)
   499   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   500       all T $ Abs(c, T, list_rename_params (cs, t))
   501   | list_rename_params (cs, B) = B;
   502 
   503 (*** Treatment of "assume", "erule", etc. ***)
   504 
   505 (*Strips assumptions in goal yielding
   506    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   507   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   508   the the parameters to be flattened, but it allows erule to work on
   509   assumptions of the form !!x. phi. Any !! after the outermost string
   510   will be regarded as belonging to the conclusion, and left untouched.
   511   Used ONLY by assum_pairs.
   512       Unless nasms<0, it can terminate the recursion early; that allows
   513   erule to work on assumptions of the form P==>Q.*)
   514 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   515   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   516       strip_assums_imp (nasms-1, H::Hs, B)
   517   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   518 
   519 
   520 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   521 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   522       strip_assums_all ((a,T)::params, t)
   523   | strip_assums_all (params, B) = (params, B);
   524 
   525 (*Produces disagreement pairs, one for each assumption proof, in order.
   526   A is the first premise of the lifted rule, and thus has the form
   527     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   528   nasms is the number of assumptions in the original subgoal, needed when B
   529     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   530 fun assum_pairs(nasms,A) =
   531   let val (params, A') = strip_assums_all ([],A)
   532       val (Hs,B) = strip_assums_imp (nasms,[],A')
   533       fun abspar t = rlist_abs(params, t)
   534       val D = abspar B
   535       fun pairrev ([], pairs) = pairs
   536         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   537   in  pairrev (Hs,[])
   538   end;
   539 
   540 
   541 (* global schematic variables *)
   542 
   543 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   544 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   545 
   546 fun varifyT ty = ty |> Term.map_atyps
   547   (fn TFree (a, S) => TVar ((a, 0), S)
   548     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   549 
   550 fun unvarifyT ty = ty |> Term.map_atyps
   551   (fn TVar ((a, 0), S) => TFree (a, S)
   552     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   553     | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   554 
   555 fun varify tm =
   556   tm |> Term.map_aterms
   557     (fn Free (x, T) => Var ((x, 0), T)
   558       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   559       | t => t)
   560   |> Term.map_types varifyT
   561   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   562 
   563 fun unvarify tm =
   564   tm |> Term.map_aterms
   565     (fn Var ((x, 0), T) => Free (x, T)
   566       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   567       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   568       | t => t)
   569   |> Term.map_types unvarifyT
   570   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   571 
   572 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   573 val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
   574 
   575 val legacy_varify =
   576   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   577   Term.map_types legacy_varifyT;
   578 
   579 val legacy_unvarify =
   580   Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
   581   Term.map_types legacy_unvarifyT;
   582 
   583 
   584 (* goal states *)
   585 
   586 fun get_goal st i = nth_prem (i, st)
   587   handle TERM _ => error "Goal number out of range";
   588 
   589 (*reverses parameters for substitution*)
   590 fun goal_params st i =
   591   let val gi = get_goal st i
   592       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   593   in (gi, rfrees) end;
   594 
   595 fun concl_of_goal st i =
   596   let val (gi, rfrees) = goal_params st i
   597       val B = strip_assums_concl gi
   598   in subst_bounds (rfrees, B) end;
   599 
   600 fun prems_of_goal st i =
   601   let val (gi, rfrees) = goal_params st i
   602       val As = strip_assums_hyp gi
   603   in map (fn A => subst_bounds (rfrees, A)) As end;
   604 
   605 end;