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