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