src/Pure/logic.ML
author wenzelm
Tue Nov 28 00:35:21 2006 +0100 (2006-11-28)
changeset 21566 af2932baf068
parent 21520 63c73f461eec
child 21576 8c11b1ce2f05
permissions -rw-r--r--
dest_term: strip_imp_concl;
     1 (*  Title:      Pure/logic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Abstract syntax operations of the Pure meta-logic.
     7 *)
     8 
     9 signature LOGIC =
    10 sig
    11   val is_all: term -> bool
    12   val dest_all: term -> typ * term
    13   val mk_equals: term * term -> term
    14   val dest_equals: term -> term * term
    15   val mk_implies: term * term -> term
    16   val dest_implies: term -> term * term
    17   val list_implies: term list * term -> term
    18   val strip_imp_prems: term -> term list
    19   val strip_imp_concl: term -> term
    20   val strip_prems: int * term list * term -> term list * term
    21   val count_prems: term * int -> int
    22   val nth_prem: int * term -> term
    23   val conjunction: term
    24   val mk_conjunction: term * term -> term
    25   val mk_conjunction_list: term list -> term
    26   val mk_conjunction_list2: term list list -> term
    27   val dest_conjunction: term -> term * term
    28   val dest_conjunction_list: term -> term list
    29   val dest_conjunctions: term -> term list
    30   val strip_horn: term -> term list * term
    31   val mk_type: typ -> term
    32   val dest_type: term -> typ
    33   val type_map: (term -> term) -> typ -> typ
    34   val const_of_class: class -> string
    35   val class_of_const: string -> class
    36   val mk_inclass: typ * class -> term
    37   val dest_inclass: term -> typ * class
    38   val name_classrel: string * string -> string
    39   val mk_classrel: class * class -> term
    40   val dest_classrel: term -> class * class
    41   val name_arities: arity -> string list
    42   val name_arity: string * sort list * class -> string
    43   val mk_arities: arity -> term list
    44   val dest_arity: term -> string * sort list * class
    45   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    46     term -> (term * term) * term
    47   val abs_def: term -> term * term
    48   val mk_cond_defpair: term list -> term * term -> string * term
    49   val mk_defpair: term * term -> string * 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_indexes: typ list * int -> term -> term
    60   val incr_tvar: int -> typ -> typ
    61   val lift_abs: int -> term -> term -> term
    62   val lift_all: int -> term -> term -> term
    63   val strip_assums_hyp: term -> term list
    64   val strip_assums_concl: term -> term
    65   val strip_params: term -> (string * typ) list
    66   val has_meta_prems: term -> int -> bool
    67   val flatten_params: int -> term -> term
    68   val auto_rename: bool ref
    69   val set_rename_prefix: string -> unit
    70   val list_rename_params: string list * term -> term
    71   val assum_pairs: int * term -> (term*term)list
    72   val varifyT: typ -> typ
    73   val unvarifyT: typ -> typ
    74   val varify: term -> term
    75   val unvarify: term -> term
    76   val legacy_varifyT: typ -> typ
    77   val legacy_unvarifyT: typ -> typ
    78   val legacy_varify: term -> term
    79   val legacy_unvarify: term -> term
    80   val get_goal: term -> int -> term
    81   val goal_params: term -> int -> term * term list
    82   val prems_of_goal: term -> int -> term list
    83   val concl_of_goal: term -> int -> term
    84 end;
    85 
    86 structure Logic : LOGIC =
    87 struct
    88 
    89 
    90 (*** Abstract syntax operations on the meta-connectives ***)
    91 
    92 (** all **)
    93 
    94 fun is_all (Const ("all", _) $ _) = true
    95   | is_all _ = false;
    96 
    97 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    98   | dest_all t = raise TERM ("dest_all", [t]);
    99 
   100 
   101 (** equality **)
   102 
   103 fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
   104 
   105 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   106   | dest_equals t = raise TERM ("dest_equals", [t]);
   107 
   108 
   109 (** implies **)
   110 
   111 fun mk_implies (A, B) = implies $ A $ B;
   112 
   113 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   114   | dest_implies A = raise TERM ("dest_implies", [A]);
   115 
   116 
   117 (** nested implications **)
   118 
   119 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   120 fun list_implies ([], B) = B
   121   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   122 
   123 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   124 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   125   | strip_imp_prems _ = [];
   126 
   127 (* A1==>...An==>B  goes to B, where B is not an implication *)
   128 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   129   | strip_imp_concl A = A : term;
   130 
   131 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   132     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   133   if  i<0 or else i too big then raises  TERM*)
   134 fun strip_prems (0, As, B) = (As, B)
   135   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   136         strip_prems (i-1, A::As, B)
   137   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   138 
   139 (*Count premises -- quicker than (length o strip_prems) *)
   140 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   141   | count_prems (_,n) = n;
   142 
   143 (*Select Ai from A1 ==>...Ai==>B*)
   144 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   145   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   146   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   147 
   148 (*strip a proof state (Horn clause):
   149   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   150 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   151 
   152 
   153 (** conjunction **)
   154 
   155 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
   156 
   157 (*A && B*)
   158 fun mk_conjunction (A, B) = conjunction $ A $ B;
   159 
   160 (*A && B && C -- improper*)
   161 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   162   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   163 
   164 (*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
   165 fun mk_conjunction_list2 tss =
   166   mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
   167 
   168 (*A && B*)
   169 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   170   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   171 
   172 (*A && B && C -- improper*)
   173 fun dest_conjunction_list t =
   174   (case try dest_conjunction t of
   175     NONE => [t]
   176   | SOME (A, B) => A :: dest_conjunction_list B);
   177 
   178 (*((A && B) && C) && D && E -- flat*)
   179 fun dest_conjunctions t =
   180   (case try dest_conjunction t of
   181     NONE => [t]
   182   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   183 
   184 
   185 
   186 (** types as terms **)
   187 
   188 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   189 
   190 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   191   | dest_type t = raise TERM ("dest_type", [t]);
   192 
   193 fun type_map f = dest_type o f o mk_type;
   194 
   195 
   196 
   197 (** type classes **)
   198 
   199 (* const names *)
   200 
   201 val classN = "_class";
   202 
   203 val const_of_class = suffix classN;
   204 
   205 fun class_of_const c = unsuffix classN c
   206   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   207 
   208 
   209 (* class constraints *)
   210 
   211 fun mk_inclass (ty, c) =
   212   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   213 
   214 fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   215   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   216 
   217 
   218 (* class relations *)
   219 
   220 fun name_classrel (c1, c2) =
   221   NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
   222 
   223 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
   224 
   225 fun dest_classrel tm =
   226   (case dest_inclass tm of
   227     (TVar (_, [c1]), c2) => (c1, c2)
   228   | _ => raise TERM ("dest_classrel", [tm]));
   229 
   230 
   231 (* type arities *)
   232 
   233 fun name_arities (t, _, S) =
   234   let val b = NameSpace.base t
   235   in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
   236 
   237 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   238 
   239 fun mk_arities (t, Ss, S) =
   240   let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
   241   in map (fn c => mk_inclass (T, c)) S end;
   242 
   243 fun dest_arity tm =
   244   let
   245     fun err () = raise TERM ("dest_arity", [tm]);
   246 
   247     val (ty, c) = dest_inclass tm;
   248     val (t, tvars) =
   249       (case ty of
   250         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   251       | _ => err ());
   252     val Ss =
   253       if has_duplicates (eq_fst (op =)) tvars then err ()
   254       else map snd tvars;
   255   in (t, Ss, c) end;
   256 
   257 
   258 
   259 (** definitions **)
   260 
   261 fun term_kind (Const _) = "existing constant "
   262   | term_kind (Free _) = "free variable "
   263   | term_kind (Bound _) = "bound variable "
   264   | term_kind _ = "";
   265 
   266 (*c x == t[x] to !!x. c x == t[x]*)
   267 fun dest_def pp check_head is_fixed is_fixedT eq =
   268   let
   269     fun err msg = raise TERM (msg, [eq]);
   270     val eq_vars = Term.strip_all_vars eq;
   271     val eq_body = Term.strip_all_body eq;
   272 
   273     val display_terms = commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
   274     val display_types = commas_quote o map (Pretty.string_of_typ pp);
   275 
   276     val (raw_lhs, rhs) = dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
   277     val lhs = Envir.beta_eta_contract raw_lhs;
   278     val (head, args) = Term.strip_comb lhs;
   279     val head_tfrees = Term.add_tfrees head [];
   280 
   281     fun check_arg (Bound _) = true
   282       | check_arg (Free (x, _)) = not (is_fixed x)
   283       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
   284       | check_arg _ = false;
   285     fun close_arg (Bound _) t = t
   286       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
   287 
   288     val lhs_bads = filter_out check_arg args;
   289     val lhs_dups = duplicates (op aconv) args;
   290     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   291       if is_fixed x orelse member (op aconv) args v then I
   292       else insert (op aconv) v | _ => I) rhs [];
   293     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
   294       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
   295       else insert (op =) v | _ => I)) rhs [];
   296   in
   297     if not (check_head head) then
   298       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
   299     else if not (null lhs_bads) then
   300       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
   301     else if not (null lhs_dups) then
   302       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
   303     else if not (null rhs_extras) then
   304       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
   305     else if not (null rhs_extrasT) then
   306       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
   307     else if exists_subterm (fn t => t aconv head) rhs then
   308       err "Entity to be defined occurs on rhs"
   309     else ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (mk_equals (lhs, rhs)))))
   310   end;
   311 
   312 (*!!x. c x == t[x] to c == %x. t[x]*)
   313 fun abs_def eq =
   314   let
   315     val body = Term.strip_all_body eq;
   316     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
   317     val (lhs, rhs) = dest_equals (Term.subst_bounds (vars, body));
   318     val (lhs', args) = Term.strip_comb lhs;
   319     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
   320   in (lhs', rhs') end;
   321 
   322 fun mk_cond_defpair As (lhs, rhs) =
   323   (case Term.head_of lhs of
   324     Const (name, _) =>
   325       (NameSpace.base name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   326   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   327 
   328 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   329 
   330 
   331 
   332 (** protected propositions and embedded terms **)
   333 
   334 val protectC = Const ("prop", propT --> propT);
   335 fun protect t = protectC $ t;
   336 
   337 fun unprotect (Const ("prop", _) $ t) = t
   338   | unprotect t = raise TERM ("unprotect", [t]);
   339 
   340 
   341 fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
   342 
   343 fun dest_term (Const ("ProtoPure.term", _) $ t) = t
   344   | dest_term t = raise TERM ("dest_term", [t]);
   345 
   346 
   347 
   348 (*** Low-level term operations ***)
   349 
   350 (*Does t occur in u?  Or is alpha-convertible to u?
   351   The term t must contain no loose bound variables*)
   352 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   353 
   354 (*Close up a formula over all free variables by quantification*)
   355 fun close_form A =
   356   Term.list_all_free (rev (Term.add_frees A []), A);
   357 
   358 
   359 
   360 (*** Specialized operations for resolution... ***)
   361 
   362 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   363 fun combound (t, n, k) =
   364     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   365 
   366 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   367 fun rlist_abs ([], body) = body
   368   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   369 
   370 
   371 local exception SAME in
   372 
   373 fun incrT k =
   374   let
   375     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   376       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   377       | incr _ = raise SAME
   378     and incrs (T :: Ts) =
   379         (incr T :: (incrs Ts handle SAME => Ts)
   380           handle SAME => T :: incrs Ts)
   381       | incrs [] = raise SAME;
   382   in incr end;
   383 
   384 (*For all variables in the term, increment indexnames and lift over the Us
   385     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   386 fun incr_indexes ([], 0) t = t
   387   | incr_indexes (Ts, k) t =
   388   let
   389     val n = length Ts;
   390     val incrT = if k = 0 then I else incrT k;
   391 
   392     fun incr lev (Var ((x, i), T)) =
   393           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   394       | incr lev (Abs (x, T, body)) =
   395           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   396             handle SAME => Abs (x, T, incr (lev + 1) body))
   397       | incr lev (t $ u) =
   398           (incr lev t $ (incr lev u handle SAME => u)
   399             handle SAME => t $ incr lev u)
   400       | incr _ (Const (c, T)) = Const (c, incrT T)
   401       | incr _ (Free (x, T)) = Free (x, incrT T)
   402       | incr _ (t as Bound _) = t;
   403   in incr 0 t handle SAME => t end;
   404 
   405 fun incr_tvar 0 T = T
   406   | incr_tvar k T = incrT k T handle SAME => T;
   407 
   408 end;
   409 
   410 
   411 (* Lifting functions from subgoal and increment:
   412     lift_abs operates on terms
   413     lift_all operates on propositions *)
   414 
   415 fun lift_abs inc =
   416   let
   417     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   418       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   419       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   420   in lift [] end;
   421 
   422 fun lift_all inc =
   423   let
   424     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   425       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   426       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   427   in lift [] end;
   428 
   429 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   430 fun strip_assums_hyp B =
   431   let
   432     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   433       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   434           strip (map (incr_boundvars 1) Hs) t
   435       | strip Hs B = rev Hs
   436   in strip [] B end;
   437 
   438 (*Strips assumptions in goal, yielding conclusion.   *)
   439 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   440   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   441   | strip_assums_concl B = B;
   442 
   443 (*Make a list of all the parameters in a subgoal, even if nested*)
   444 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   445   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   446   | strip_params B = [];
   447 
   448 (*test for meta connectives in prems of a 'subgoal'*)
   449 fun has_meta_prems prop i =
   450   let
   451     fun is_meta (Const ("==>", _) $ _ $ _) = true
   452       | is_meta (Const ("==", _) $ _ $ _) = true
   453       | is_meta (Const ("all", _) $ _) = true
   454       | is_meta _ = false;
   455   in
   456     (case strip_prems (i, [], prop) of
   457       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   458     | _ => false) handle TERM _ => false
   459   end;
   460 
   461 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   462     where j is the total number of parameters (precomputed)
   463   If n>0 then deletes assumption n. *)
   464 fun remove_params j n A =
   465     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   466     else case A of
   467         Const("==>", _) $ H $ B =>
   468           if n=1 then                           (remove_params j (n-1) B)
   469           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   470       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   471       | _ => if n>0 then raise TERM("remove_params", [A])
   472              else A;
   473 
   474 (** Auto-renaming of parameters in subgoals **)
   475 
   476 val auto_rename = ref false
   477 and rename_prefix = ref "ka";
   478 
   479 (*rename_prefix is not exported; it is set by this function.*)
   480 fun set_rename_prefix a =
   481     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   482     then  (rename_prefix := a;  auto_rename := true)
   483     else  error"rename prefix must be nonempty and consist of letters";
   484 
   485 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   486   A name clash could cause the printer to rename bound vars;
   487     then res_inst_tac would not work properly.*)
   488 fun rename_vars (a, []) = []
   489   | rename_vars (a, (_,T)::vars) =
   490         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   491 
   492 (*Move all parameters to the front of the subgoal, renaming them apart;
   493   if n>0 then deletes assumption n. *)
   494 fun flatten_params n A =
   495     let val params = strip_params A;
   496         val vars = if !auto_rename
   497                    then rename_vars (!rename_prefix, params)
   498                    else ListPair.zip (Name.variant_list [] (map #1 params),
   499                                       map #2 params)
   500     in  list_all (vars, remove_params (length vars) n A)
   501     end;
   502 
   503 (*Makes parameters in a goal have the names supplied by the list cs.*)
   504 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   505       implies $ A $ list_rename_params (cs, B)
   506   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   507       all T $ Abs(c, T, list_rename_params (cs, t))
   508   | list_rename_params (cs, B) = B;
   509 
   510 (*** Treatment of "assume", "erule", etc. ***)
   511 
   512 (*Strips assumptions in goal yielding
   513    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   514   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   515   the the parameters to be flattened, but it allows erule to work on
   516   assumptions of the form !!x. phi. Any !! after the outermost string
   517   will be regarded as belonging to the conclusion, and left untouched.
   518   Used ONLY by assum_pairs.
   519       Unless nasms<0, it can terminate the recursion early; that allows
   520   erule to work on assumptions of the form P==>Q.*)
   521 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   522   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   523       strip_assums_imp (nasms-1, H::Hs, B)
   524   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   525 
   526 
   527 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   528 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   529       strip_assums_all ((a,T)::params, t)
   530   | strip_assums_all (params, B) = (params, B);
   531 
   532 (*Produces disagreement pairs, one for each assumption proof, in order.
   533   A is the first premise of the lifted rule, and thus has the form
   534     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   535   nasms is the number of assumptions in the original subgoal, needed when B
   536     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   537 fun assum_pairs(nasms,A) =
   538   let val (params, A') = strip_assums_all ([],A)
   539       val (Hs,B) = strip_assums_imp (nasms,[],A')
   540       fun abspar t = rlist_abs(params, t)
   541       val D = abspar B
   542       fun pairrev ([], pairs) = pairs
   543         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   544   in  pairrev (Hs,[])
   545   end;
   546 
   547 
   548 (* global schematic variables *)
   549 
   550 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   551 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   552 
   553 fun varifyT ty = ty |> Term.map_atyps
   554   (fn TFree (a, S) => TVar ((a, 0), S)
   555     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   556 
   557 fun unvarifyT ty = ty |> Term.map_atyps
   558   (fn TVar ((a, 0), S) => TFree (a, S)
   559     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   560     | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   561 
   562 fun varify tm =
   563   tm |> Term.map_aterms
   564     (fn Free (x, T) => Var ((x, 0), T)
   565       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   566       | t => t)
   567   |> Term.map_types varifyT
   568   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   569 
   570 fun unvarify tm =
   571   tm |> Term.map_aterms
   572     (fn Var ((x, 0), T) => Free (x, T)
   573       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   574       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   575       | t => t)
   576   |> Term.map_types unvarifyT
   577   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   578 
   579 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   580 val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
   581 
   582 val legacy_varify =
   583   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   584   Term.map_types legacy_varifyT;
   585 
   586 val legacy_unvarify =
   587   Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
   588   Term.map_types legacy_unvarifyT;
   589 
   590 
   591 (* goal states *)
   592 
   593 fun get_goal st i = nth_prem (i, st)
   594   handle TERM _ => error "Goal number out of range";
   595 
   596 (*reverses parameters for substitution*)
   597 fun goal_params st i =
   598   let val gi = get_goal st i
   599       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   600   in (gi, rfrees) end;
   601 
   602 fun concl_of_goal st i =
   603   let val (gi, rfrees) = goal_params st i
   604       val B = strip_assums_concl gi
   605   in subst_bounds (rfrees, B) end;
   606 
   607 fun prems_of_goal st i =
   608   let val (gi, rfrees) = goal_params st i
   609       val As = strip_assums_hyp gi
   610   in map (fn A => subst_bounds (rfrees, A)) As end;
   611 
   612 end;