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