src/Provers/quantifier1.ML
 author nipkow Sat May 16 11:28:02 2009 +0200 (2009-05-16) changeset 31166 a90fe83f58ea parent 20049 f48c4a3a34bc child 31197 c1c163ec6c44 permissions -rw-r--r--
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".
1 (*  Title:      Provers/quantifier1
2     ID:         \$Id\$
3     Author:     Tobias Nipkow
4     Copyright   1997  TU Munich
6 Simplification procedures for turning
8             ? x. ... & x = t & ...
9      into   ? x. x = t & ... & ...
10      where the `? x. x = t &' in the latter formula must be eliminated
11            by ordinary simplification.
13      and   ! x. (... & x = t & ...) --> P x
14      into  ! x. x = t --> (... & ...) --> P x
15      where the `!x. x=t -->' in the latter formula is eliminated
16            by ordinary simplification.
18      And analogously for t=x, but the eqn is not turned around!
20      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
21         "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
22         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
23         As must be "? x. t=x & P(x)".
25      And similarly for the bounded quantifiers.
27 Gries etc call this the "1 point rules"
29 The above also works for !x1..xn. and ?x1..xn by moving the defined
30 qunatifier inside first, but not for nested bounded quantifiers.
32 For set comprehensions the basic permutations
33       ... & x = t & ...  ->  x = t & (... & ...)
34       ... & t = x & ...  ->  t = x & (... & ...)
35 are also exported.
37 To avoid looping, NONE is returned if the term cannot be rearranged,
38 esp if x=t/t=x sits at the front already.
39 *)
41 signature QUANTIFIER1_DATA =
42 sig
43   (*abstract syntax*)
44   val dest_eq: term -> (term*term*term)option
45   val dest_conj: term -> (term*term*term)option
46   val dest_imp:  term -> (term*term*term)option
47   val conj: term
48   val imp:  term
49   (*rules*)
50   val iff_reflection: thm (* P <-> Q ==> P == Q *)
51   val iffI:  thm
52   val iff_trans: thm
53   val conjI: thm
54   val conjE: thm
55   val impI:  thm
56   val mp:    thm
57   val exI:   thm
58   val exE:   thm
59   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
60   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
61   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
62   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
63   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
64 end;
66 signature QUANTIFIER1 =
67 sig
68   val prove_one_point_all_tac: tactic
69   val prove_one_point_ex_tac: tactic
70   val rearrange_all: theory -> simpset -> term -> thm option
71   val rearrange_ex:  theory -> simpset -> term -> thm option
72   val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
73   val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
74   val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
75 end;
77 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
78 struct
80 open Data;
82 (* FIXME: only test! *)
83 fun def xs eq =
84   (case dest_eq eq of
85      SOME(c,s,t) =>
86        let val n = length xs
87        in s = Bound n andalso not(loose_bvar1(t,n)) orelse
88           t = Bound n andalso not(loose_bvar1(s,n)) end
89    | NONE => false);
91 fun extract_conj fst xs t = case dest_conj t of NONE => NONE
92     | SOME(conj,P,Q) =>
93         (if not fst andalso def xs P then SOME(xs,P,Q) else
94          if def xs Q then SOME(xs,Q,P) else
95          (case extract_conj false xs P of
96             SOME(xs,eq,P') => SOME(xs,eq, conj \$ P' \$ Q)
97           | NONE => (case extract_conj false xs Q of
98                        SOME(xs,eq,Q') => SOME(xs,eq,conj \$ P \$ Q')
99                      | NONE => NONE)));
101 fun extract_imp fst xs t = case dest_imp t of NONE => NONE
102     | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
103                        else (case extract_conj false xs P of
104                                SOME(xs,eq,P') => SOME(xs, eq, imp \$ P' \$ Q)
105                              | NONE => (case extract_imp false xs Q of
106                                           NONE => NONE
107                                         | SOME(xs,eq,Q') =>
108                                             SOME(xs,eq,imp\$P\$Q')));
110 fun extract_quant extract q =
111   let fun exqu xs ((qC as Const(qa,_)) \$ Abs(x,T,Q)) =
112             if qa = q then exqu ((qC,x,T)::xs) Q else NONE
113         | exqu xs P = extract (null xs) xs P
114   in exqu [] end;
116 fun prove_conv tac thy tu =
117   Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
118     (K (rtac iff_reflection 1 THEN tac));
120 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
122 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
123    Better: instantiate exI
124 *)
125 local
126 val excomm = ex_comm RS iff_trans
127 in
128 val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
129     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
130                     DEPTH_SOLVE_1 o (ares_tac [conjI])])
131 end;
133 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
134           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
135 *)
136 local
137 val tac = SELECT_GOAL
138           (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
139                   REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
140 val allcomm = all_comm RS iff_trans
141 in
142 val prove_one_point_all_tac =
143       EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
144 end
146 fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
147                                    if i=u then l else i+1)
148   | renumber l u (s\$t) = renumber l u s \$ renumber l u t
149   | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
150   | renumber _ _ atom = atom;
152 fun quantify qC x T xs P =
153   let fun quant [] P = P
154         | quant ((qC,x,T)::xs) P = quant xs (qC \$ Abs(x,T,P))
155       val n = length xs
156       val Q = if n=0 then P else renumber 0 n P
157   in quant xs (qC \$ Abs(x,T,Q)) end;
159 fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
160      (case extract_quant extract_imp q P of
161         NONE => NONE
162       | SOME(xs,eq,Q) =>
163           let val R = quantify all x T xs (imp \$ eq \$ Q)
164           in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
165   | rearrange_all _ _ _ = NONE;
167 fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) =
168      (case extract_imp true [] P of
169         NONE => NONE
170       | SOME(xs,eq,Q) => if not(null xs) then NONE else
171           let val R = imp \$ eq \$ Q
172           in SOME(prove_conv (tac ss) thy (F,Ball \$ A \$ Abs(x,T,R))) end)
173   | rearrange_ball _ _ _ _ = NONE;
175 fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
176      (case extract_quant extract_conj q P of
177         NONE => NONE
178       | SOME(xs,eq,Q) =>
179           let val R = quantify ex x T xs (conj \$ eq \$ Q)
180           in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
181   | rearrange_ex _ _ _ = NONE;
183 fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) =
184      (case extract_conj true [] P of
185         NONE => NONE
186       | SOME(xs,eq,Q) => if not(null xs) then NONE else
187           SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
188   | rearrange_bex _ _ _ _ = NONE;
190 fun rearrange_Coll tac thy _ (F as Coll \$ Abs(x,T,P)) =
191      (case extract_conj true [] P of
192         NONE => NONE
193       | SOME(_,eq,Q) =>
194           let val R = Coll \$ Abs(x,T, conj \$ eq \$ Q)
195           in SOME(prove_conv tac thy (F,R)) end);
197 end;