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