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