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