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