outer_constraints with original variable names, to ensure that argsP is consistent with args
1 (* Title: Pure/logic.ML
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5 Abstract syntax operations of the Pure meta-logic.
10 val all: term -> term -> term
11 val is_all: term -> bool
12 val dest_all: term -> (string * typ) * term
13 val mk_equals: term * term -> term
14 val dest_equals: term -> term * term
16 val mk_implies: term * term -> term
17 val dest_implies: term -> term * term
18 val list_implies: term list * term -> term
19 val strip_imp_prems: term -> term list
20 val strip_imp_concl: term -> term
21 val strip_prems: int * term list * term -> term list * term
22 val count_prems: term -> int
23 val nth_prem: int * term -> term
26 val mk_conjunction: term * term -> term
27 val mk_conjunction_list: term list -> term
28 val mk_conjunction_balanced: term list -> term
29 val dest_conjunction: term -> term * term
30 val dest_conjunction_list: term -> term list
31 val dest_conjunction_balanced: int -> term -> term list
32 val dest_conjunctions: term -> term list
33 val strip_horn: term -> term list * term
34 val mk_type: typ -> term
35 val dest_type: term -> typ
36 val type_map: (term -> term) -> typ -> typ
37 val const_of_class: class -> string
38 val class_of_const: string -> class
39 val mk_of_class: typ * class -> term
40 val dest_of_class: term -> typ * class
41 val mk_of_sort: typ * sort -> term list
42 val name_classrel: string * string -> string
43 val mk_classrel: class * class -> term
44 val dest_classrel: term -> class * class
45 val name_arities: arity -> string list
46 val name_arity: string * sort list * class -> string
47 val mk_arities: arity -> term list
48 val dest_arity: term -> string * sort list * class
49 val unconstrainT: sort list -> term ->
50 ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
52 val protect: term -> term
53 val unprotect: term -> term
54 val mk_term: term -> term
55 val dest_term: term -> term
56 val occs: term * term -> bool
57 val close_form: term -> term
58 val combound: term * int * int -> term
59 val rlist_abs: (string * typ) list * term -> term
60 val incr_tvar_same: int -> typ Same.operation
61 val incr_tvar: int -> typ -> typ
62 val incr_indexes_same: typ list * int -> term Same.operation
63 val incr_indexes: typ list * int -> term -> term
64 val lift_abs: int -> term -> term -> term
65 val lift_all: int -> term -> term -> term
66 val strip_assums_hyp: term -> term list
67 val strip_assums_concl: term -> term
68 val strip_params: term -> (string * typ) list
69 val has_meta_prems: term -> bool
70 val flatten_params: int -> term -> term
71 val list_rename_params: string list * term -> term
72 val assum_pairs: int * term -> (term*term)list
73 val assum_problems: int * term -> (term -> term) * term list * term
74 val varifyT_global: typ -> typ
75 val unvarifyT_global: typ -> typ
76 val varify_global: term -> term
77 val unvarify_global: term -> term
78 val get_goal: term -> int -> term
79 val goal_params: term -> int -> term * term list
80 val prems_of_goal: term -> int -> term list
81 val concl_of_goal: term -> int -> term
84 structure Logic : LOGIC =
88 (*** Abstract syntax operations on the meta-connectives ***)
92 fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
94 fun is_all (Const ("all", _) $ Abs _) = true
97 fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
98 let val (x, b) = Term.dest_abs abs (*potentially slow*)
100 | dest_all t = raise TERM ("dest_all", [t]);
105 fun mk_equals (t, u) =
106 let val T = Term.fastype_of t
107 in Const ("==", T --> T --> propT) $ t $ u end;
109 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
110 | dest_equals t = raise TERM ("dest_equals", [t]);
115 val implies = Const ("==>", propT --> propT --> propT);
117 fun mk_implies (A, B) = implies $ A $ B;
119 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
120 | dest_implies A = raise TERM ("dest_implies", [A]);
123 (** nested implications **)
125 (* [A1,...,An], B goes to A1==>...An==>B *)
126 fun list_implies ([], B) = B
127 | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
129 (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *)
130 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
131 | strip_imp_prems _ = [];
133 (* A1==>...An==>B goes to B, where B is not an implication *)
134 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
135 | strip_imp_concl A = A : term;
137 (*Strip and return premises: (i, [], A1==>...Ai==>B)
138 goes to ([Ai, A(i-1),...,A1] , B) (REVERSED)
139 if i<0 or else i too big then raises TERM*)
140 fun strip_prems (0, As, B) = (As, B)
141 | strip_prems (i, As, Const("==>", _) $ A $ B) =
142 strip_prems (i-1, A::As, B)
143 | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
145 (*Count premises -- quicker than (length o strip_prems) *)
146 fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
149 (*Select Ai from A1 ==>...Ai==>B*)
150 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
151 | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
152 | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
154 (*strip a proof state (Horn clause):
155 B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *)
156 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
162 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
163 val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
167 fun mk_conjunction (A, B) = conjunction $ A $ B;
169 (*A &&& B &&& C -- improper*)
170 fun mk_conjunction_list [] = true_prop
171 | mk_conjunction_list ts = foldr1 mk_conjunction ts;
173 (*(A &&& B) &&& (C &&& D) -- balanced*)
174 fun mk_conjunction_balanced [] = true_prop
175 | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
179 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
180 | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
182 (*A &&& B &&& C -- improper*)
183 fun dest_conjunction_list t =
184 (case try dest_conjunction t of
186 | SOME (A, B) => A :: dest_conjunction_list B);
188 (*(A &&& B) &&& (C &&& D) -- balanced*)
189 fun dest_conjunction_balanced 0 _ = []
190 | dest_conjunction_balanced n t = Balanced_Tree.dest dest_conjunction n t;
192 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
193 fun dest_conjunctions t =
194 (case try dest_conjunction t of
196 | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
200 (** types as terms **)
202 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
204 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
205 | dest_type t = raise TERM ("dest_type", [t]);
207 fun type_map f = dest_type o f o mk_type;
215 val classN = "_class";
217 val const_of_class = suffix classN;
219 fun class_of_const c = unsuffix classN c
220 handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
223 (* class/sort membership *)
225 fun mk_of_class (ty, c) =
226 Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
228 fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
229 | dest_of_class t = raise TERM ("dest_of_class", [t]);
231 fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
234 (* class relations *)
236 fun name_classrel (c1, c2) =
237 Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
239 fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
241 fun dest_classrel tm =
242 (case dest_of_class tm of
243 (TVar (_, [c1]), c2) => (c1, c2)
244 | _ => raise TERM ("dest_classrel", [tm]));
249 fun name_arities (t, _, S) =
250 let val b = Long_Name.base_name t
251 in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
253 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
255 fun mk_arities (t, Ss, S) =
256 let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
257 in map (fn c => mk_of_class (T, c)) S end;
261 fun err () = raise TERM ("dest_arity", [tm]);
263 val (ty, c) = dest_of_class tm;
266 Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
269 if has_duplicates (eq_fst (op =)) tvars then err ()
274 (* internalized sort constraints *)
276 fun unconstrainT shyps prop =
278 val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
279 val extra = fold (Sorts.remove_sort o #2) present shyps;
281 val n = length present;
282 val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n;
285 map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
286 val constraints_map =
287 map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
288 map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
291 (case AList.lookup (op =) present_map T of
294 (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
296 | NONE => raise TYPE ("Dangling type variable", [T], [])));
299 maps (fn (_, T as TVar (ai, S)) =>
300 map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
303 val outer_constraints =
304 maps (fn (T, S) => map (pair T) S)
305 (present @ map (fn S => (TFree ("'dummy", S), S)) extra);
309 |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
310 |> curry list_implies (map snd constraints);
311 in ((atyp_map, constraints, outer_constraints), prop') end;
315 (** protected propositions and embedded terms **)
317 val protectC = Const ("prop", propT --> propT);
318 fun protect t = protectC $ t;
320 fun unprotect (Const ("prop", _) $ t) = t
321 | unprotect t = raise TERM ("unprotect", [t]);
324 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
326 fun dest_term (Const ("Pure.term", _) $ t) = t
327 | dest_term t = raise TERM ("dest_term", [t]);
331 (*** Low-level term operations ***)
333 (*Does t occur in u? Or is alpha-convertible to u?
334 The term t must contain no loose bound variables*)
335 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
337 (*Close up a formula over all free variables by quantification*)
339 Term.list_all_free (rev (Term.add_frees A []), A);
343 (*** Specialized operations for resolution... ***)
345 (*computes t(Bound(n+k-1),...,Bound(n)) *)
346 fun combound (t, n, k) =
347 if k>0 then combound (t,n+1,k-1) $ (Bound n) else t;
349 (* ([xn,...,x1], t) ======> (x1,...,xn)t *)
350 fun rlist_abs ([], body) = body
351 | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
353 fun incr_tvar_same 0 = Same.same
354 | incr_tvar_same k = Term_Subst.map_atypsT_same
355 (fn TVar ((a, i), S) => TVar ((a, i + k), S)
356 | _ => raise Same.SAME);
358 fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
360 (*For all variables in the term, increment indexnames and lift over the Us
361 result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
362 fun incr_indexes_same ([], 0) = Same.same
363 | incr_indexes_same (Ts, k) =
366 val incrT = incr_tvar_same k;
368 fun incr lev (Var ((x, i), T)) =
369 combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
370 | incr lev (Abs (x, T, body)) =
371 (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
372 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
374 (incr lev t $ (incr lev u handle Same.SAME => u)
375 handle Same.SAME => t $ incr lev u)
376 | incr _ (Const (c, T)) = Const (c, incrT T)
377 | incr _ (Free (x, T)) = Free (x, incrT T)
378 | incr _ (Bound _) = raise Same.SAME;
381 fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
384 (* Lifting functions from subgoal and increment:
385 lift_abs operates on terms
386 lift_all operates on propositions *)
390 fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
391 | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
392 | lift Ts _ t = incr_indexes (rev Ts, inc) t;
397 fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
398 | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
399 | lift Ts _ t = incr_indexes (rev Ts, inc) t;
402 (*Strips assumptions in goal, yielding list of hypotheses. *)
403 fun strip_assums_hyp B =
405 fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
406 | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
407 strip (map (incr_boundvars 1) Hs) t
408 | strip Hs B = rev Hs
411 (*Strips assumptions in goal, yielding conclusion. *)
412 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
413 | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
414 | strip_assums_concl B = B;
416 (*Make a list of all the parameters in a subgoal, even if nested*)
417 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
418 | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
419 | strip_params B = [];
421 (*test for nested meta connectives in prems*)
424 fun is_meta (Const ("==", _) $ _ $ _) = true
425 | is_meta (Const ("==>", _) $ _ $ _) = true
426 | is_meta (Const ("all", _) $ _) = true
428 fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
429 | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
433 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
434 where j is the total number of parameters (precomputed)
435 If n>0 then deletes assumption n. *)
436 fun remove_params j n A =
437 if j=0 andalso n<=0 then A (*nothing left to do...*)
439 Const("==>", _) $ H $ B =>
440 if n=1 then (remove_params j (n-1) B)
441 else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
442 | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
443 | _ => if n>0 then raise TERM("remove_params", [A])
446 (*Move all parameters to the front of the subgoal, renaming them apart;
447 if n>0 then deletes assumption n. *)
448 fun flatten_params n A =
449 let val params = strip_params A;
450 val vars = ListPair.zip (Name.variant_list [] (map #1 params),
452 in list_all (vars, remove_params (length vars) n A)
455 (*Makes parameters in a goal have the names supplied by the list cs.*)
456 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
457 implies $ A $ list_rename_params (cs, B)
458 | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
459 a $ Abs(c, T, list_rename_params (cs, t))
460 | list_rename_params (cs, B) = B;
464 (*** Treatment of "assume", "erule", etc. ***)
466 (*Strips assumptions in goal yielding
467 HS = [Hn,...,H1], params = [xm,...,x1], and B,
468 where x1...xm are the parameters. This version (21.1.2005) REQUIRES
469 the the parameters to be flattened, but it allows erule to work on
470 assumptions of the form !!x. phi. Any !! after the outermost string
471 will be regarded as belonging to the conclusion, and left untouched.
472 Used ONLY by assum_pairs.
473 Unless nasms<0, it can terminate the recursion early; that allows
474 erule to work on assumptions of the form P==>Q.*)
475 fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*)
476 | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
477 strip_assums_imp (nasms-1, H::Hs, B)
478 | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
480 (*Strips OUTER parameters only.*)
481 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
482 strip_assums_all ((a,T)::params, t)
483 | strip_assums_all (params, B) = (params, B);
485 (*Produces disagreement pairs, one for each assumption proof, in order.
486 A is the first premise of the lifted rule, and thus has the form
487 H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B).
488 nasms is the number of assumptions in the original subgoal, needed when B
489 has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
490 fun assum_pairs(nasms,A) =
491 let val (params, A') = strip_assums_all ([],A)
492 val (Hs,B) = strip_assums_imp (nasms,[],A')
493 fun abspar t = rlist_abs(params, t)
495 fun pairrev ([], pairs) = pairs
496 | pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs)
500 fun assum_problems (nasms, A) =
502 val (params, A') = strip_assums_all ([], A)
503 val (Hs, B) = strip_assums_imp (nasms, [], A')
504 fun abspar t = rlist_abs (params, t)
505 in (abspar, rev Hs, B) end;
508 (* global schematic variables *)
510 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
511 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
513 fun varifyT_global_same ty = ty
514 |> Term_Subst.map_atypsT_same
515 (fn TFree (a, S) => TVar ((a, 0), S)
516 | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
518 fun unvarifyT_global_same ty = ty
519 |> Term_Subst.map_atypsT_same
520 (fn TVar ((a, 0), S) => TFree (a, S)
521 | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
522 | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
524 val varifyT_global = Same.commit varifyT_global_same;
525 val unvarifyT_global = Same.commit unvarifyT_global_same;
527 fun varify_global tm = tm
528 |> Same.commit (Term_Subst.map_aterms_same
529 (fn Free (x, T) => Var ((x, 0), T)
530 | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
531 | _ => raise Same.SAME))
532 |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
533 handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
535 fun unvarify_global tm = tm
536 |> Same.commit (Term_Subst.map_aterms_same
537 (fn Var ((x, 0), T) => Free (x, T)
538 | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
539 | Free (x, _) => raise TERM (bad_fixed x, [tm])
540 | _ => raise Same.SAME))
541 |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
542 handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
547 fun get_goal st i = nth_prem (i, st)
548 handle TERM _ => error "Goal number out of range";
550 (*reverses parameters for substitution*)
551 fun goal_params st i =
552 let val gi = get_goal st i
553 val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
556 fun concl_of_goal st i =
557 let val (gi, rfrees) = goal_params st i
558 val B = strip_assums_concl gi
559 in subst_bounds (rfrees, B) end;
561 fun prems_of_goal st i =
562 let val (gi, rfrees) = goal_params st i
563 val As = strip_assums_hyp gi
564 in map (fn A => subst_bounds (rfrees, A)) As end;