src/Pure/logic.ML
author wenzelm
Sat Nov 05 15:00:49 2011 +0100 (2011-11-05)
changeset 45344 e209da839ff4
parent 45328 e5b33eecbf6e
child 46215 0da9433f959e
permissions -rw-r--r--
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
tuned;
     1 (*  Title:      Pure/logic.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Abstract syntax operations of the Pure meta-logic.
     6 *)
     7 
     8 signature LOGIC =
     9 sig
    10   val all: term -> term -> term
    11   val is_all: term -> bool
    12   val dest_all: term -> (string * typ) * term
    13   val mk_equals: term * term -> term
    14   val dest_equals: term -> term * term
    15   val implies: term
    16   val mk_implies: term * term -> term
    17   val dest_implies: term -> term * term
    18   val list_implies: term list * term -> term
    19   val strip_imp_prems: term -> term list
    20   val strip_imp_concl: term -> term
    21   val strip_prems: int * term list * term -> term list * term
    22   val count_prems: term -> int
    23   val nth_prem: int * term -> term
    24   val true_prop: term
    25   val conjunction: term
    26   val mk_conjunction: term * term -> term
    27   val mk_conjunction_list: term list -> term
    28   val mk_conjunction_balanced: term list -> term
    29   val dest_conjunction: term -> term * term
    30   val dest_conjunction_list: term -> term list
    31   val dest_conjunction_balanced: int -> term -> term list
    32   val dest_conjunctions: term -> term list
    33   val strip_horn: term -> term list * term
    34   val mk_type: typ -> term
    35   val dest_type: term -> typ
    36   val type_map: (term -> term) -> typ -> typ
    37   val const_of_class: class -> string
    38   val class_of_const: string -> class
    39   val mk_of_class: typ * class -> term
    40   val dest_of_class: term -> typ * class
    41   val mk_of_sort: typ * sort -> term list
    42   val name_classrel: string * string -> string
    43   val mk_classrel: class * class -> term
    44   val dest_classrel: term -> class * class
    45   val name_arities: arity -> string list
    46   val name_arity: string * sort list * class -> string
    47   val mk_arities: arity -> term list
    48   val dest_arity: term -> string * sort list * class
    49   val unconstrainT: sort list -> term ->
    50     ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
    51   val protectC: term
    52   val protect: term -> term
    53   val unprotect: term -> term
    54   val mk_term: term -> term
    55   val dest_term: term -> term
    56   val occs: term * term -> bool
    57   val close_form: term -> term
    58   val combound: term * int * int -> term
    59   val rlist_abs: (string * typ) list * term -> term
    60   val incr_tvar_same: int -> typ Same.operation
    61   val incr_tvar: int -> typ -> typ
    62   val incr_indexes_same: typ list * int -> term Same.operation
    63   val incr_indexes: typ list * int -> term -> term
    64   val lift_abs: int -> term -> term -> term
    65   val lift_all: int -> term -> term -> term
    66   val strip_assums_hyp: term -> term list
    67   val strip_assums_concl: term -> term
    68   val strip_params: term -> (string * typ) list
    69   val has_meta_prems: term -> bool
    70   val flatten_params: int -> term -> term
    71   val list_rename_params: string list -> term -> term
    72   val assum_pairs: int * term -> (term * term) list
    73   val assum_problems: int * term -> (term -> term) * term list * term
    74   val varifyT_global: typ -> typ
    75   val unvarifyT_global: typ -> typ
    76   val varify_types_global: term -> term
    77   val unvarify_types_global: term -> term
    78   val varify_global: term -> term
    79   val unvarify_global: term -> term
    80   val get_goal: term -> int -> term
    81   val goal_params: term -> int -> term * term list
    82   val prems_of_goal: term -> int -> term list
    83   val concl_of_goal: term -> int -> term
    84 end;
    85 
    86 structure Logic : LOGIC =
    87 struct
    88 
    89 
    90 (*** Abstract syntax operations on the meta-connectives ***)
    91 
    92 (** all **)
    93 
    94 fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
    95 
    96 fun is_all (Const ("all", _) $ Abs _) = true
    97   | is_all _ = false;
    98 
    99 fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
   100       let val (x, b) = Term.dest_abs abs  (*potentially slow*)
   101       in ((x, T), b) end
   102   | dest_all t = raise TERM ("dest_all", [t]);
   103 
   104 
   105 (** equality **)
   106 
   107 fun mk_equals (t, u) =
   108   let val T = Term.fastype_of t
   109   in Const ("==", T --> T --> propT) $ t $ u end;
   110 
   111 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   112   | dest_equals t = raise TERM ("dest_equals", [t]);
   113 
   114 
   115 (** implies **)
   116 
   117 val implies = Const ("==>", propT --> propT --> propT);
   118 
   119 fun mk_implies (A, B) = implies $ A $ B;
   120 
   121 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   122   | dest_implies A = raise TERM ("dest_implies", [A]);
   123 
   124 
   125 (** nested implications **)
   126 
   127 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   128 fun list_implies ([], B) = B
   129   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   130 
   131 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   132 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   133   | strip_imp_prems _ = [];
   134 
   135 (* A1==>...An==>B  goes to B, where B is not an implication *)
   136 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   137   | strip_imp_concl A = A : term;
   138 
   139 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   140     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   141   if  i<0 or else i too big then raises  TERM*)
   142 fun strip_prems (0, As, B) = (As, B)
   143   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   144         strip_prems (i-1, A::As, B)
   145   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   146 
   147 (*Count premises -- quicker than (length o strip_prems) *)
   148 fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
   149   | count_prems _ = 0;
   150 
   151 (*Select Ai from A1 ==>...Ai==>B*)
   152 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   153   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   154   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   155 
   156 (*strip a proof state (Horn clause):
   157   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   158 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   159 
   160 
   161 
   162 (** conjunction **)
   163 
   164 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
   165 val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
   166 
   167 
   168 (*A &&& B*)
   169 fun mk_conjunction (A, B) = conjunction $ A $ B;
   170 
   171 (*A &&& B &&& C -- improper*)
   172 fun mk_conjunction_list [] = true_prop
   173   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   174 
   175 (*(A &&& B) &&& (C &&& D) -- balanced*)
   176 fun mk_conjunction_balanced [] = true_prop
   177   | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
   178 
   179 
   180 (*A &&& B*)
   181 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   182   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   183 
   184 (*A &&& B &&& C -- improper*)
   185 fun dest_conjunction_list t =
   186   (case try dest_conjunction t of
   187     NONE => [t]
   188   | SOME (A, B) => A :: dest_conjunction_list B);
   189 
   190 (*(A &&& B) &&& (C &&& D) -- balanced*)
   191 fun dest_conjunction_balanced 0 _ = []
   192   | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
   193 
   194 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
   195 fun dest_conjunctions t =
   196   (case try dest_conjunction t of
   197     NONE => [t]
   198   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   199 
   200 
   201 
   202 (** types as terms **)
   203 
   204 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   205 
   206 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   207   | dest_type t = raise TERM ("dest_type", [t]);
   208 
   209 fun type_map f = dest_type o f o mk_type;
   210 
   211 
   212 
   213 (** type classes **)
   214 
   215 (* const names *)
   216 
   217 val classN = "_class";
   218 
   219 val const_of_class = suffix classN;
   220 
   221 fun class_of_const c = unsuffix classN c
   222   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   223 
   224 
   225 (* class/sort membership *)
   226 
   227 fun mk_of_class (ty, c) =
   228   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   229 
   230 fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   231   | dest_of_class t = raise TERM ("dest_of_class", [t]);
   232 
   233 fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
   234 
   235 
   236 (* class relations *)
   237 
   238 fun name_classrel (c1, c2) =
   239   Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
   240 
   241 fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
   242 
   243 fun dest_classrel tm =
   244   (case dest_of_class tm of
   245     (TVar (_, [c1]), c2) => (c1, c2)
   246   | _ => raise TERM ("dest_classrel", [tm]));
   247 
   248 
   249 (* type arities *)
   250 
   251 fun name_arities (t, _, S) =
   252   let val b = Long_Name.base_name t
   253   in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
   254 
   255 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   256 
   257 fun mk_arities (t, Ss, S) =
   258   let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
   259   in map (fn c => mk_of_class (T, c)) S end;
   260 
   261 fun dest_arity tm =
   262   let
   263     fun err () = raise TERM ("dest_arity", [tm]);
   264 
   265     val (ty, c) = dest_of_class tm;
   266     val (t, tvars) =
   267       (case ty of
   268         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   269       | _ => err ());
   270     val Ss =
   271       if has_duplicates (eq_fst (op =)) tvars then err ()
   272       else map snd tvars;
   273   in (t, Ss, c) end;
   274 
   275 
   276 (* internalized sort constraints *)
   277 
   278 fun unconstrainT shyps prop =
   279   let
   280     val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
   281     val extra = fold (Sorts.remove_sort o #2) present shyps;
   282 
   283     val n = length present;
   284     val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n;
   285 
   286     val present_map =
   287       map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
   288     val constraints_map =
   289       map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
   290       map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
   291 
   292     fun atyp_map T =
   293       (case AList.lookup (op =) present_map T of
   294         SOME U => U
   295       | NONE =>
   296           (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
   297             SOME U => U
   298           | NONE => raise TYPE ("Dangling type variable", [T], [])));
   299 
   300     val constraints =
   301       maps (fn (_, T as TVar (ai, S)) =>
   302         map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
   303         constraints_map;
   304 
   305     val outer_constraints =
   306       maps (fn (T, S) => map (pair T) S)
   307         (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
   308 
   309     val prop' =
   310       prop
   311       |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
   312       |> curry list_implies (map snd constraints);
   313   in ((atyp_map, constraints, outer_constraints), prop') end;
   314 
   315 
   316 
   317 (** protected propositions and embedded terms **)
   318 
   319 val protectC = Const ("prop", propT --> propT);
   320 fun protect t = protectC $ t;
   321 
   322 fun unprotect (Const ("prop", _) $ t) = t
   323   | unprotect t = raise TERM ("unprotect", [t]);
   324 
   325 
   326 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
   327 
   328 fun dest_term (Const ("Pure.term", _) $ t) = t
   329   | dest_term t = raise TERM ("dest_term", [t]);
   330 
   331 
   332 
   333 (*** Low-level term operations ***)
   334 
   335 (*Does t occur in u?  Or is alpha-convertible to u?
   336   The term t must contain no loose bound variables*)
   337 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   338 
   339 (*Close up a formula over all free variables by quantification*)
   340 fun close_form A =
   341   Term.list_all_free (rev (Term.add_frees A []), A);
   342 
   343 
   344 
   345 (*** Specialized operations for resolution... ***)
   346 
   347 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   348 fun combound (t, n, k) =
   349     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   350 
   351 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   352 fun rlist_abs ([], body) = body
   353   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   354 
   355 fun incr_tvar_same 0 = Same.same
   356   | incr_tvar_same k = Term_Subst.map_atypsT_same
   357       (fn TVar ((a, i), S) => TVar ((a, i + k), S)
   358         | _ => raise Same.SAME);
   359 
   360 fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
   361 
   362 (*For all variables in the term, increment indexnames and lift over the Us
   363     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   364 fun incr_indexes_same ([], 0) = Same.same
   365   | incr_indexes_same (Ts, k) =
   366       let
   367         val n = length Ts;
   368         val incrT = incr_tvar_same k;
   369 
   370         fun incr lev (Var ((x, i), T)) =
   371               combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
   372           | incr lev (Abs (x, T, body)) =
   373               (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
   374                 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
   375           | incr lev (t $ u) =
   376               (incr lev t $ (incr lev u handle Same.SAME => u)
   377                 handle Same.SAME => t $ incr lev u)
   378           | incr _ (Const (c, T)) = Const (c, incrT T)
   379           | incr _ (Free (x, T)) = Free (x, incrT T)
   380           | incr _ (Bound _) = raise Same.SAME;
   381       in incr 0 end;
   382 
   383 fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
   384 
   385 
   386 (* Lifting functions from subgoal and increment:
   387     lift_abs operates on terms
   388     lift_all operates on propositions *)
   389 
   390 fun lift_abs inc =
   391   let
   392     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   393       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   394       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   395   in lift [] end;
   396 
   397 fun lift_all inc =
   398   let
   399     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   400       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   401       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   402   in lift [] end;
   403 
   404 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   405 fun strip_assums_hyp B =
   406   let
   407     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   408       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   409           strip (map (incr_boundvars 1) Hs) t
   410       | strip Hs B = rev Hs
   411   in strip [] B end;
   412 
   413 (*Strips assumptions in goal, yielding conclusion.   *)
   414 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   415   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   416   | strip_assums_concl B = B;
   417 
   418 (*Make a list of all the parameters in a subgoal, even if nested*)
   419 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   420   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   421   | strip_params B = [];
   422 
   423 (*test for nested meta connectives in prems*)
   424 val has_meta_prems =
   425   let
   426     fun is_meta (Const ("==", _) $ _ $ _) = true
   427       | is_meta (Const ("==>", _) $ _ $ _) = true
   428       | is_meta (Const ("all", _) $ _) = true
   429       | is_meta _ = false;
   430     fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
   431       | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
   432       | ex_meta _ = false;
   433   in ex_meta end;
   434 
   435 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   436     where j is the total number of parameters (precomputed)
   437   If n>0 then deletes assumption n. *)
   438 fun remove_params j n A =
   439     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   440     else case A of
   441         Const("==>", _) $ H $ B =>
   442           if n=1 then                           (remove_params j (n-1) B)
   443           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   444       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   445       | _ => if n>0 then raise TERM("remove_params", [A])
   446              else A;
   447 
   448 (*Move all parameters to the front of the subgoal, renaming them apart;
   449   if n>0 then deletes assumption n. *)
   450 fun flatten_params n A =
   451     let val params = strip_params A;
   452         val vars = ListPair.zip (Name.variant_list [] (map #1 params),
   453                                  map #2 params)
   454     in  list_all (vars, remove_params (length vars) n A)
   455     end;
   456 
   457 (*Makes parameters in a goal have the names supplied by the list cs.*)
   458 fun list_rename_params cs (Const ("==>", _) $ A $ B) =
   459       implies $ A $ list_rename_params cs B
   460   | list_rename_params (c :: cs) ((a as Const ("all", _)) $ Abs (_, T, t)) =
   461       a $ Abs (c, T, list_rename_params cs t)
   462   | list_rename_params cs B = B;
   463 
   464 
   465 
   466 (*** Treatment of "assume", "erule", etc. ***)
   467 
   468 (*Strips assumptions in goal yielding
   469    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   470   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   471   the the parameters to be flattened, but it allows erule to work on
   472   assumptions of the form !!x. phi. Any !! after the outermost string
   473   will be regarded as belonging to the conclusion, and left untouched.
   474   Used ONLY by assum_pairs.
   475       Unless nasms<0, it can terminate the recursion early; that allows
   476   erule to work on assumptions of the form P==>Q.*)
   477 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   478   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   479       strip_assums_imp (nasms-1, H::Hs, B)
   480   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   481 
   482 (*Strips OUTER parameters only.*)
   483 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   484       strip_assums_all ((a,T)::params, t)
   485   | strip_assums_all (params, B) = (params, B);
   486 
   487 (*Produces disagreement pairs, one for each assumption proof, in order.
   488   A is the first premise of the lifted rule, and thus has the form
   489     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   490   nasms is the number of assumptions in the original subgoal, needed when B
   491     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   492 fun assum_pairs(nasms,A) =
   493   let val (params, A') = strip_assums_all ([],A)
   494       val (Hs,B) = strip_assums_imp (nasms,[],A')
   495       fun abspar t = rlist_abs(params, t)
   496       val D = abspar B
   497       fun pairrev ([], pairs) = pairs
   498         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   499   in  pairrev (Hs,[])
   500   end;
   501 
   502 fun assum_problems (nasms, A) =
   503   let
   504     val (params, A') = strip_assums_all ([], A)
   505     val (Hs, B) = strip_assums_imp (nasms, [], A')
   506     fun abspar t = rlist_abs (params, t)
   507   in (abspar, rev Hs, B) end;
   508 
   509 
   510 (* global schematic variables *)
   511 
   512 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   513 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   514 
   515 fun varifyT_global_same ty = ty
   516   |> Term_Subst.map_atypsT_same
   517     (fn TFree (a, S) => TVar ((a, 0), S)
   518       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   519 
   520 fun unvarifyT_global_same ty = ty
   521   |> Term_Subst.map_atypsT_same
   522     (fn TVar ((a, 0), S) => TFree (a, S)
   523       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   524       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   525 
   526 val varifyT_global = Same.commit varifyT_global_same;
   527 val unvarifyT_global = Same.commit unvarifyT_global_same;
   528 
   529 fun varify_types_global tm = tm
   530   |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
   531   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   532 
   533 fun unvarify_types_global tm = tm
   534   |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
   535   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   536 
   537 fun varify_global tm = tm
   538   |> Same.commit (Term_Subst.map_aterms_same
   539     (fn Free (x, T) => Var ((x, 0), T)
   540       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   541       | _ => raise Same.SAME))
   542   |> varify_types_global;
   543 
   544 fun unvarify_global tm = tm
   545   |> Same.commit (Term_Subst.map_aterms_same
   546     (fn Var ((x, 0), T) => Free (x, T)
   547       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   548       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   549       | _ => raise Same.SAME))
   550   |> unvarify_types_global;
   551 
   552 
   553 (* goal states *)
   554 
   555 fun get_goal st i = nth_prem (i, st)
   556   handle TERM _ => error "Goal number out of range";
   557 
   558 (*reverses parameters for substitution*)
   559 fun goal_params st i =
   560   let val gi = get_goal st i
   561       val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
   562   in (gi, rfrees) end;
   563 
   564 fun concl_of_goal st i =
   565   let val (gi, rfrees) = goal_params st i
   566       val B = strip_assums_concl gi
   567   in subst_bounds (rfrees, B) end;
   568 
   569 fun prems_of_goal st i =
   570   let val (gi, rfrees) = goal_params st i
   571       val As = strip_assums_hyp gi
   572   in map (fn A => subst_bounds (rfrees, A)) As end;
   573 
   574 end;