src/Pure/logic.ML
author wenzelm
Sat Oct 07 01:31:11 2006 +0200 (2006-10-07)
changeset 20883 b432f20a47ca
parent 20630 2010cbb1a941
child 21016 430b35c9cd27
permissions -rw-r--r--
removed is_equals, is_implies;
tuned;
     1 (*  Title:      Pure/logic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Abstract syntax operations of the Pure meta-logic.
     7 *)
     8 
     9 signature LOGIC =
    10 sig
    11   val is_all: term -> bool
    12   val dest_all: term -> typ * term
    13   val mk_equals: term * term -> term
    14   val dest_equals: term -> term * term
    15   val mk_implies: term * term -> term
    16   val dest_implies: term -> term * term
    17   val list_implies: term list * term -> term
    18   val strip_imp_prems: term -> term list
    19   val strip_imp_concl: term -> term
    20   val strip_prems: int * term list * term -> term list * term
    21   val count_prems: term * int -> int
    22   val nth_prem: int * term -> term
    23   val conjunction: term
    24   val mk_conjunction: term * term -> term
    25   val mk_conjunction_list: term list -> term
    26   val mk_conjunction_list2: term list list -> term
    27   val dest_conjunction: term -> term * term
    28   val dest_conjunction_list: term -> term list
    29   val dest_conjunctions: term -> term list
    30   val strip_horn: term -> term list * term
    31   val dest_type: term -> typ
    32   val const_of_class: class -> string
    33   val class_of_const: string -> class
    34   val mk_inclass: typ * class -> term
    35   val dest_inclass: term -> typ * class
    36   val name_classrel: string * string -> string
    37   val mk_classrel: class * class -> term
    38   val dest_classrel: term -> class * class
    39   val name_arities: arity -> string list
    40   val name_arity: string * sort list * class -> string
    41   val mk_arities: arity -> term list
    42   val dest_arity: term -> string * sort list * class
    43   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    44     term -> (term * term) * term
    45   val abs_def: term -> term * term
    46   val mk_cond_defpair: term list -> term * term -> string * term
    47   val mk_defpair: term * term -> string * term
    48   val mk_type: typ -> term
    49   val protectC: term
    50   val protect: term -> term
    51   val unprotect: term -> term
    52   val mk_term: term -> term
    53   val dest_term: term -> term
    54   val occs: term * term -> bool
    55   val close_form: term -> term
    56   val combound: term * int * int -> term
    57   val rlist_abs: (string * typ) list * term -> term
    58   val incr_indexes: typ list * int -> term -> term
    59   val incr_tvar: int -> typ -> typ
    60   val lift_abs: int -> term -> term -> term
    61   val lift_all: int -> term -> term -> term
    62   val strip_assums_hyp: term -> term list
    63   val strip_assums_concl: term -> term
    64   val strip_params: term -> (string * typ) list
    65   val has_meta_prems: term -> int -> bool
    66   val flatten_params: int -> term -> term
    67   val auto_rename: bool ref
    68   val set_rename_prefix: string -> unit
    69   val list_rename_params: string list * term -> term
    70   val assum_pairs: int * term -> (term*term)list
    71   val varifyT: typ -> typ
    72   val unvarifyT: typ -> typ
    73   val varify: term -> term
    74   val unvarify: term -> term
    75   val legacy_varifyT: typ -> typ
    76   val legacy_unvarifyT: typ -> typ
    77   val legacy_varify: term -> term
    78   val legacy_unvarify: term -> term
    79   val get_goal: term -> int -> term
    80   val goal_params: term -> int -> term * term list
    81   val prems_of_goal: term -> int -> term list
    82   val concl_of_goal: term -> int -> term
    83 end;
    84 
    85 structure Logic : LOGIC =
    86 struct
    87 
    88 
    89 (*** Abstract syntax operations on the meta-connectives ***)
    90 
    91 (** all **)
    92 
    93 fun is_all (Const ("all", _) $ _) = true
    94   | is_all _ = false;
    95 
    96 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    97   | dest_all t = raise TERM ("dest_all", [t]);
    98 
    99 
   100 (** equality **)
   101 
   102 fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
   103 
   104 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   105   | dest_equals t = raise TERM ("dest_equals", [t]);
   106 
   107 
   108 (** implies **)
   109 
   110 fun mk_implies (A, B) = implies $ A $ B;
   111 
   112 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   113   | dest_implies A = raise TERM ("dest_implies", [A]);
   114 
   115 
   116 (** nested implications **)
   117 
   118 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   119 fun list_implies ([], B) = B
   120   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   121 
   122 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   123 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   124   | strip_imp_prems _ = [];
   125 
   126 (* A1==>...An==>B  goes to B, where B is not an implication *)
   127 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   128   | strip_imp_concl A = A : term;
   129 
   130 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   131     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   132   if  i<0 or else i too big then raises  TERM*)
   133 fun strip_prems (0, As, B) = (As, B)
   134   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   135         strip_prems (i-1, A::As, B)
   136   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   137 
   138 (*Count premises -- quicker than (length o strip_prems) *)
   139 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   140   | count_prems (_,n) = n;
   141 
   142 (*Select Ai from A1 ==>...Ai==>B*)
   143 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   144   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   145   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   146 
   147 (*strip a proof state (Horn clause):
   148   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   149 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   150 
   151 
   152 (** conjunction **)
   153 
   154 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
   155 
   156 (*A && B*)
   157 fun mk_conjunction (A, B) = conjunction $ A $ B;
   158 
   159 (*A && B && C -- improper*)
   160 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   161   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   162 
   163 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   164 fun mk_conjunction_list2 tss =
   165   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
   166 
   167 (*A && B*)
   168 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   169   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   170 
   171 (*A && B && C -- improper*)
   172 fun dest_conjunction_list t =
   173   (case try dest_conjunction t of
   174     NONE => [t]
   175   | SOME (A, B) => A :: dest_conjunction_list B);
   176 
   177 (*((A && B) && C) && D && E -- flat*)
   178 fun dest_conjunctions t =
   179   (case try dest_conjunction t of
   180     NONE => [t]
   181   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   182 
   183 
   184 
   185 (** types as terms **)
   186 
   187 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   188 
   189 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   190   | dest_type t = raise TERM ("dest_type", [t]);
   191 
   192 
   193 
   194 (** type classes **)
   195 
   196 (* const names *)
   197 
   198 val classN = "_class";
   199 
   200 val const_of_class = suffix classN;
   201 
   202 fun class_of_const c = unsuffix classN c
   203   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   204 
   205 
   206 (* class constraints *)
   207 
   208 fun mk_inclass (ty, c) =
   209   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   210 
   211 fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   212   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   213 
   214 
   215 (* class relations *)
   216 
   217 fun name_classrel (c1, c2) =
   218   NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
   219 
   220 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
   221 
   222 fun dest_classrel tm =
   223   (case dest_inclass tm of
   224     (TVar (_, [c1]), c2) => (c1, c2)
   225   | _ => raise TERM ("dest_classrel", [tm]));
   226 
   227 
   228 (* type arities *)
   229 
   230 fun name_arities (t, _, S) =
   231   let val b = NameSpace.base t
   232   in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
   233 
   234 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   235 
   236 fun mk_arities (t, Ss, S) =
   237   let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
   238   in map (fn c => mk_inclass (T, c)) S end;
   239 
   240 fun dest_arity tm =
   241   let
   242     fun err () = raise TERM ("dest_arity", [tm]);
   243 
   244     val (ty, c) = dest_inclass tm;
   245     val (t, tvars) =
   246       (case ty of
   247         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   248       | _ => err ());
   249     val Ss =
   250       if has_duplicates (eq_fst (op =)) tvars then err ()
   251       else map snd tvars;
   252   in (t, Ss, c) end;
   253 
   254 
   255 
   256 (** definitions **)
   257 
   258 fun term_kind (Const _) = "existing constant "
   259   | term_kind (Free _) = "free variable "
   260   | term_kind (Bound _) = "bound variable "
   261   | term_kind _ = "";
   262 
   263 (*c x == t[x] to !!x. c x == t[x]*)
   264 fun dest_def pp check_head is_fixed is_fixedT eq =
   265   let
   266     fun err msg = raise TERM (msg, [eq]);
   267     val eq_vars = Term.strip_all_vars eq;
   268     val eq_body = Term.strip_all_body eq;
   269 
   270     val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
   271     val display_types = commas_quote o map (Pretty.string_of_typ pp);
   272 
   273     val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
   274     val lhs = Envir.beta_eta_contract raw_lhs;
   275     val (head, args) = Term.strip_comb lhs;
   276     val head_tfrees = Term.add_tfrees head [];
   277 
   278     fun check_arg (Bound _) = true
   279       | check_arg (Free (x, _)) = not (is_fixed x)
   280       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   281       | check_arg _ = false;
   282     fun close_arg (Bound _) t = t
   283       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
   284 
   285     val lhs_bads = filter_out check_arg args;
   286     val lhs_dups = duplicates (op aconv) args;
   287     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   288       if is_fixed x orelse member (op aconv) args v then I
   289       else insert (op aconv) v | _ => I) rhs [];
   290     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
   291       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   292       else insert (op =) v | _ => I)) rhs [];
   293   in
   294     if not (check_head head) then
   295       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
   296     else if not (null lhs_bads) then
   297       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   298     else if not (null lhs_dups) then
   299       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   300     else if not (null rhs_extras) then
   301       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   302     else if not (null rhs_extrasT) then
   303       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   304     else if exists_subterm (fn t => t aconv head) rhs then
   305       err "Entity to be defined occurs on rhs"
   306     else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
   307   end;
   308 
   309 (*!!x. c x == t[x] to c == %x. t[x]*)
   310 fun abs_def eq =
   311   let
   312     val body = Term.strip_all_body eq;
   313     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   314     val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   315     val (lhs', args) = Term.strip_comb lhs;
   316     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   317   in (lhs', rhs') end;
   318 
   319 fun mk_cond_defpair As (lhs, rhs) =
   320   (case Term.head_of lhs of
   321     Const (name, _) =>
   322       (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   323   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   324 
   325 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   326 
   327 
   328 
   329 (** protected propositions and embedded terms **)
   330 
   331 val protectC = Const ("prop", propT --> propT);
   332 fun protect t = protectC $ t;
   333 
   334 fun unprotect (Const ("prop", _) $ t) = t
   335   | unprotect t = raise TERM ("unprotect", [t]);
   336 
   337 
   338 fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
   339 
   340 fun dest_term (Const ("ProtoPure.term", _) $ t) = t
   341   | dest_term t = raise TERM ("dest_term", [t]);
   342 
   343 
   344 
   345 (*** Low-level term operations ***)
   346 
   347 (*Does t occur in u?  Or is alpha-convertible to u?
   348   The term t must contain no loose bound variables*)
   349 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   350 
   351 (*Close up a formula over all free variables by quantification*)
   352 fun close_form A =
   353   Term.list_all_free (rev (Term.add_frees A []), A);
   354 
   355 
   356 
   357 (*** Specialized operations for resolution... ***)
   358 
   359 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   360 fun combound (t, n, k) =
   361     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   362 
   363 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   364 fun rlist_abs ([], body) = body
   365   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   366 
   367 
   368 local exception SAME in
   369 
   370 fun incrT k =
   371   let
   372     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   373       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   374       | incr _ = raise SAME
   375     and incrs (T :: Ts) =
   376         (incr T :: (incrs Ts handle SAME => Ts)
   377           handle SAME => T :: incrs Ts)
   378       | incrs [] = raise SAME;
   379   in incr end;
   380 
   381 (*For all variables in the term, increment indexnames and lift over the Us
   382     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   383 fun incr_indexes ([], 0) t = t
   384   | incr_indexes (Ts, k) t =
   385   let
   386     val n = length Ts;
   387     val incrT = if k = 0 then I else incrT k;
   388 
   389     fun incr lev (Var ((x, i), T)) =
   390           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   391       | incr lev (Abs (x, T, body)) =
   392           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   393             handle SAME => Abs (x, T, incr (lev + 1) body))
   394       | incr lev (t $ u) =
   395           (incr lev t $ (incr lev u handle SAME => u)
   396             handle SAME => t $ incr lev u)
   397       | incr _ (Const (c, T)) = Const (c, incrT T)
   398       | incr _ (Free (x, T)) = Free (x, incrT T)
   399       | incr _ (t as Bound _) = t;
   400   in incr 0 t handle SAME => t end;
   401 
   402 fun incr_tvar 0 T = T
   403   | incr_tvar k T = incrT k T handle SAME => T;
   404 
   405 end;
   406 
   407 
   408 (* Lifting functions from subgoal and increment:
   409     lift_abs operates on terms
   410     lift_all operates on propositions *)
   411 
   412 fun lift_abs inc =
   413   let
   414     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   415       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   416       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   417   in lift [] end;
   418 
   419 fun lift_all inc =
   420   let
   421     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   422       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   423       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   424   in lift [] end;
   425 
   426 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   427 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   428   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   429   | strip_assums_hyp B = [];
   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;