src/Provers/quantifier1.ML
 author wenzelm Fri Oct 21 18:14:34 2005 +0200 (2005-10-21) changeset 17956 369e2af8ee45 parent 17002 fb9261990ffe child 20049 f48c4a3a34bc permissions -rw-r--r--
Goal.prove;
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)".
26      And similarly for the bounded quantifiers.
28 Gries etc call this the "1 point rules"
29 *)
31 signature QUANTIFIER1_DATA =
32 sig
33   (*abstract syntax*)
34   val dest_eq: term -> (term*term*term)option
35   val dest_conj: term -> (term*term*term)option
36   val dest_imp:  term -> (term*term*term)option
37   val conj: term
38   val imp:  term
39   (*rules*)
40   val iff_reflection: thm (* P <-> Q ==> P == Q *)
41   val iffI:  thm
42   val iff_trans: thm
43   val conjI: thm
44   val conjE: thm
45   val impI:  thm
46   val mp:    thm
47   val exI:   thm
48   val exE:   thm
49   val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
50   val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
51   val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
52   val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
53   val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
54 end;
56 signature QUANTIFIER1 =
57 sig
58   val prove_one_point_all_tac: tactic
59   val prove_one_point_ex_tac: tactic
60   val rearrange_all: theory -> simpset -> term -> thm option
61   val rearrange_ex:  theory -> simpset -> term -> thm option
62   val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
63   val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
64 end;
66 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
67 struct
69 open Data;
71 (* FIXME: only test! *)
72 fun def xs eq =
73   let val n = length xs
74   in case dest_eq eq of
75       SOME(c,s,t) =>
76         s = Bound n andalso not(loose_bvar1(t,n)) orelse
77         t = Bound n andalso not(loose_bvar1(s,n))
78     | NONE => false
79   end;
81 fun extract_conj xs t = case dest_conj t of NONE => NONE
82     | SOME(conj,P,Q) =>
83         (if def xs P then SOME(xs,P,Q) else
84          if def xs Q then SOME(xs,Q,P) else
85          (case extract_conj xs P of
86             SOME(xs,eq,P') => SOME(xs,eq, conj \$ P' \$ Q)
87           | NONE => (case extract_conj xs Q of
88                        SOME(xs,eq,Q') => SOME(xs,eq,conj \$ P \$ Q')
89                      | NONE => NONE)));
91 fun extract_imp xs t = case dest_imp t of NONE => NONE
92     | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
93                        else (case extract_conj xs P of
94                                SOME(xs,eq,P') => SOME(xs, eq, imp \$ P' \$ Q)
95                              | NONE => (case extract_imp xs Q of
96                                           NONE => NONE
97                                         | SOME(xs,eq,Q') =>
98                                             SOME(xs,eq,imp\$P\$Q')));
100 fun extract_quant extract q =
101   let fun exqu xs ((qC as Const(qa,_)) \$ Abs(x,T,Q)) =
102             if qa = q then exqu ((qC,x,T)::xs) Q else NONE
103         | exqu xs P = extract xs P
104   in exqu end;
106 fun prove_conv tac thy tu =
107   Goal.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
109 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
111 (* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
112    Better: instantiate exI
113 *)
114 local
115 val excomm = ex_comm RS iff_trans
116 in
117 val prove_one_point_ex_tac = qcomm_tac excomm iff_exI 1 THEN rtac iffI 1 THEN
118     ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
119                     DEPTH_SOLVE_1 o (ares_tac [conjI])])
120 end;
122 (* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
123           (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
124 *)
125 local
126 val tac = SELECT_GOAL
127           (EVERY1[REPEAT o (dtac uncurry), REPEAT o (rtac impI), etac mp,
128                   REPEAT o (etac conjE), REPEAT o (ares_tac [conjI])])
129 val allcomm = all_comm RS iff_trans
130 in
131 val prove_one_point_all_tac =
132       EVERY1[qcomm_tac allcomm iff_allI,rtac iff_allI, rtac iffI, tac, tac]
133 end
135 fun renumber l u (Bound i) = Bound(if i < l orelse i > u then i else
136                                    if i=u then l else i+1)
137   | renumber l u (s\$t) = renumber l u s \$ renumber l u t
138   | renumber l u (Abs(x,T,t)) = Abs(x,T,renumber (l+1) (u+1) t)
139   | renumber _ _ atom = atom;
141 fun quantify qC x T xs P =
142   let fun quant [] P = P
143         | quant ((qC,x,T)::xs) P = quant xs (qC \$ Abs(x,T,P))
144       val n = length xs
145       val Q = if n=0 then P else renumber 0 n P
146   in quant xs (qC \$ Abs(x,T,Q)) end;
148 fun rearrange_all thy _ (F as (all as Const(q,_)) \$ Abs(x,T, P)) =
149      (case extract_quant extract_imp q [] P of
150         NONE => NONE
151       | SOME(xs,eq,Q) =>
152           let val R = quantify all x T xs (imp \$ eq \$ Q)
153           in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
154   | rearrange_all _ _ _ = NONE;
156 fun rearrange_ball tac thy ss (F as Ball \$ A \$ Abs(x,T,P)) =
157      (case extract_imp [] P of
158         NONE => NONE
159       | SOME(xs,eq,Q) => if not(null xs) then NONE else
160           let val R = imp \$ eq \$ Q
161           in SOME(prove_conv (tac ss) thy (F,Ball \$ A \$ Abs(x,T,R))) end)
162   | rearrange_ball _ _ _ _ = NONE;
164 fun rearrange_ex thy _ (F as (ex as Const(q,_)) \$ Abs(x,T,P)) =
165      (case extract_quant extract_conj q [] P of
166         NONE => NONE
167       | SOME(xs,eq,Q) =>
168           let val R = quantify ex x T xs (conj \$ eq \$ Q)
169           in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
170   | rearrange_ex _ _ _ = NONE;
172 fun rearrange_bex tac thy ss (F as Bex \$ A \$ Abs(x,T,P)) =
173      (case extract_conj [] P of
174         NONE => NONE
175       | SOME(xs,eq,Q) => if not(null xs) then NONE else
176           SOME(prove_conv (tac ss) thy (F,Bex \$ A \$ Abs(x,T,conj\$eq\$Q))))
177   | rearrange_bex _ _ _ _ = NONE;
179 end;