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