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