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