1(*  Title:      Provers/quantifier1.ML
2    Author:     Tobias Nipkow
3    Copyright   1997  TU Munich
4
5Simplification procedures for turning
6
7            ? x. ... & x = t & ...
8     into   ? x. x = t & ... & ...
9     where the `? x. x = t &' in the latter formula must be eliminated
10           by ordinary simplification.
11
12     and   ! x. (... & x = t & ...) --> P x
13     into  ! x. x = t --> (... & ...) --> P x
14     where the `!x. x=t -->' in the latter formula is eliminated
15           by ordinary simplification.
16
17     And analogously for t=x, but the eqn is not turned around!
18
19     NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
20        "!x. x=t --> P(x)" is covered by the congruence rule for -->;
21        "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
22        As must be "? x. t=x & P(x)".
23
24     And similarly for the bounded quantifiers.
25
26Gries etc call this the "1 point rules"
27
28The above also works for !x1..xn. and ?x1..xn by moving the defined
29quantifier inside first, but not for nested bounded quantifiers.
30
31For set comprehensions the basic permutations
32      ... & x = t & ...  ->  x = t & (... & ...)
33      ... & t = x & ...  ->  t = x & (... & ...)
34are also exported.
35
36To avoid looping, NONE is returned if the term cannot be rearranged,
37esp if x=t/t=x sits at the front already.
38*)
39
40signature QUANTIFIER1_DATA =
41sig
42  (*abstract syntax*)
43  val dest_eq: term -> (term * term) option
44  val dest_conj: term -> (term * term) option
45  val dest_imp: term -> (term * term) option
46  val conj: term
47  val imp: term
48  (*rules*)
49  val iff_reflection: thm (* P <-> Q ==> P == Q *)
50  val iffI: thm
51  val iff_trans: thm
52  val conjI: thm
53  val conjE: thm
54  val impI: thm
55  val mp: thm
56  val exI: thm
57  val exE: thm
58  val uncurry: thm (* P --> Q --> R ==> P & Q --> R *)
59  val iff_allI: thm (* !!x. P x <-> Q x ==> (!x. P x) = (!x. Q x) *)
60  val iff_exI: thm (* !!x. P x <-> Q x ==> (? x. P x) = (? x. Q x) *)
61  val all_comm: thm (* (!x y. P x y) = (!y x. P x y) *)
62  val ex_comm: thm (* (? x y. P x y) = (? y x. P x y) *)
63end;
64
65signature QUANTIFIER1 =
66sig
67  val prove_one_point_all_tac: Proof.context -> tactic
68  val prove_one_point_ex_tac: Proof.context -> tactic
69  val rearrange_all: Proof.context -> cterm -> thm option
70  val rearrange_ex: Proof.context -> cterm -> thm option
71  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
72  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
73  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
74end;
75
76functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
77struct
78
79(* FIXME: only test! *)
80fun def xs eq =
81  (case Data.dest_eq eq of
82    SOME (s, t) =>
83      let val n = length xs in
84        s = Bound n andalso not (loose_bvar1 (t, n)) orelse
85        t = Bound n andalso not (loose_bvar1 (s, n))
86      end
87  | NONE => false);
88
89fun extract_conj fst xs t =
90  (case Data.dest_conj t of
91    NONE => NONE
92  | SOME (P, Q) =>
93      if def xs P then (if fst then NONE else SOME (xs, P, Q))
94      else if def xs Q then SOME (xs, Q, P)
95      else
96        (case extract_conj false xs P of
97          SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
98        | NONE =>
99            (case extract_conj false xs Q of
100              SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
101            | NONE => NONE)));
102
103fun extract_imp fst xs t =
104  (case Data.dest_imp t of
105    NONE => NONE
106  | SOME (P, Q) =>
107      if def xs P then (if fst then NONE else SOME (xs, P, Q))
108      else
109        (case extract_conj false xs P of
110          SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q)
111        | NONE =>
112            (case extract_imp false xs Q of
113              NONE => NONE
114            | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q'))));
115
116fun extract_quant extract q =
117  let
118    fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
119          if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
120      | exqu xs P = extract (null xs) xs P
121  in exqu [] end;
122
123fun prove_conv ctxt tu tac =
124  let
125    val (goal, ctxt') =
126      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
127    val thm =
128      Goal.prove ctxt' [] [] goal
129        (fn {context = ctxt'', ...} =>
130          resolve_tac ctxt'' [Data.iff_reflection] 1 THEN tac ctxt'');
131  in singleton (Variable.export ctxt' ctxt) thm end;
132
133fun qcomm_tac ctxt qcomm qI i =
134  REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i);
135
136(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
137   Better: instantiate exI
138*)
139local
140  val excomm = Data.ex_comm RS Data.iff_trans;
141in
142  fun prove_one_point_ex_tac ctxt =
143    qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
144    ALLGOALS
145      (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
146        resolve_tac ctxt [Data.exI],
147        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
148end;
149
150(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
151          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
152*)
153local
154  fun tac ctxt =
155    SELECT_GOAL
156      (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry],
157        REPEAT o resolve_tac ctxt [Data.impI],
158        eresolve_tac ctxt [Data.mp],
159        REPEAT o eresolve_tac ctxt [Data.conjE],
160        REPEAT o ares_tac ctxt [Data.conjI]]);
161  val allcomm = Data.all_comm RS Data.iff_trans;
162in
163  fun prove_one_point_all_tac ctxt =
164    EVERY1 [qcomm_tac ctxt allcomm Data.iff_allI,
165      resolve_tac ctxt [Data.iff_allI],
166      resolve_tac ctxt [Data.iffI], tac ctxt, tac ctxt];
167end
168
169fun renumber l u (Bound i) =
170      Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
171  | renumber l u (s $ t) = renumber l u s $ renumber l u t
172  | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
173  | renumber _ _ atom = atom;
174
175fun quantify qC x T xs P =
176  let
177    fun quant [] P = P
178      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
179    val n = length xs;
180    val Q = if n = 0 then P else renumber 0 n P;
181  in quant xs (qC $ Abs (x, T, Q)) end;
182
183fun rearrange_all ctxt ct =
184  (case Thm.term_of ct of
185    F as (all as Const (q, _)) $ Abs (x, T, P) =>
186      (case extract_quant extract_imp q P of
187        NONE => NONE
188      | SOME (xs, eq, Q) =>
189          let val R = quantify all x T xs (Data.imp $ eq $ Q)
190          in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
191  | _ => NONE);
192
193fun rearrange_ball tac ctxt ct =
194  (case Thm.term_of ct of
195    F as Ball $ A $ Abs (x, T, P) =>
196      (case extract_imp true [] P of
197        NONE => NONE
198      | SOME (xs, eq, Q) =>
199          if not (null xs) then NONE
200          else
201            let val R = Data.imp $ eq $ Q
202            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
203  | _ => NONE);
204
205fun rearrange_ex ctxt ct =
206  (case Thm.term_of ct of
207    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
208      (case extract_quant extract_conj q P of
209        NONE => NONE
210      | SOME (xs, eq, Q) =>
211          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
212          in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end)
213  | _ => NONE);
214
215fun rearrange_bex tac ctxt ct =
216  (case Thm.term_of ct of
217    F as Bex $ A $ Abs (x, T, P) =>
218      (case extract_conj true [] P of
219        NONE => NONE
220      | SOME (xs, eq, Q) =>
221          if not (null xs) then NONE
222          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
223  | _ => NONE);
224
225fun rearrange_Collect tac ctxt ct =
226  (case Thm.term_of ct of
227    F as Collect $ Abs (x, T, P) =>
228      (case extract_conj true [] P of
229        NONE => NONE
230      | SOME (_, eq, Q) =>
231          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
232          in SOME (prove_conv ctxt (F, R) tac) end)
233  | _ => NONE);
234
235end;
236
237