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_All: Proof.context -> cterm -> thm option
71  val rearrange_ex: Proof.context -> cterm -> thm option
72  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
73  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
74  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
75end;
76
77functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
78struct
79
80(* FIXME: only test! *)
81fun def xs eq =
82  (case Data.dest_eq eq of
83    SOME (s, t) =>
84      let val n = length xs in
85        s = Bound n andalso not (loose_bvar1 (t, n)) orelse
86        t = Bound n andalso not (loose_bvar1 (s, n))
87      end
88  | NONE => false);
89
90fun extract_conj fst xs t =
91  (case Data.dest_conj t of
92    NONE => NONE
93  | SOME (P, Q) =>
94      if def xs P then (if fst then NONE else SOME (xs, P, Q))
95      else if def xs Q then SOME (xs, Q, P)
96      else
97        (case extract_conj false xs P of
98          SOME (xs, eq, P') => SOME (xs, eq, Data.conj $ P' $ Q)
99        | NONE =>
100            (case extract_conj false xs Q of
101              SOME (xs, eq, Q') => SOME (xs, eq, Data.conj $ P $ Q')
102            | NONE => NONE)));
103
104fun extract_imp fst xs t =
105  (case Data.dest_imp t of
106    NONE => NONE
107  | SOME (P, Q) =>
108      if def xs P then (if fst then NONE else SOME (xs, P, Q))
109      else
110        (case extract_conj false xs P of
111          SOME (xs, eq, P') => SOME (xs, eq, Data.imp $ P' $ Q)
112        | NONE =>
113            (case extract_imp false xs Q of
114              NONE => NONE
115            | SOME (xs, eq, Q') => SOME (xs, eq, Data.imp $ P $ Q'))));
116
117fun extract_conj_from_judgment ctxt fst xs t =
118  if Object_Logic.is_judgment ctxt t
119  then
120    (case extract_conj fst xs (Object_Logic.drop_judgment ctxt t) of
121      NONE => NONE
122    | SOME (xs, eq, P) => SOME (xs, Object_Logic.ensure_propT ctxt eq, Object_Logic.ensure_propT ctxt P))
123  else NONE;
124
125fun extract_implies ctxt fst xs t =
126  (case try Logic.dest_implies t of
127    NONE => NONE
128  | SOME (P, Q) =>
129      if def xs P then (if fst then NONE else SOME (xs, P, Q))
130      else
131        (case extract_conj_from_judgment ctxt false xs P of
132          SOME (xs, eq, P') => SOME (xs, eq, Logic.implies $ P' $ Q)
133        | NONE =>
134            (case extract_implies ctxt false xs Q of
135              NONE => NONE
136            | SOME (xs, eq, Q') => (SOME (xs, eq, Logic.implies $ P $ Q')))));
137
138fun extract_quant ctxt extract q =
139  let
140    fun exqu xs ((qC as Const (qa, _)) $ Abs (x, T, Q)) =
141          if qa = q then exqu ((qC, x, T) :: xs) Q else NONE
142      | exqu xs P = extract ctxt (null xs) xs P
143  in exqu [] end;
144
145fun iff_reflection_tac ctxt =
146  resolve_tac ctxt [Data.iff_reflection] 1;
147
148fun qcomm_tac ctxt qcomm qI i =
149  REPEAT_DETERM (resolve_tac ctxt [qcomm] i THEN resolve_tac ctxt [qI] i);
150
151(* Proves (? x0..xn. ... & x0 = t & ...) = (? x1..xn x0. x0 = t & ... & ...)
152   Better: instantiate exI
153*)
154local
155  val excomm = Data.ex_comm RS Data.iff_trans;
156in
157  fun prove_one_point_ex_tac ctxt =
158    qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
159    ALLGOALS
160      (EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
161        resolve_tac ctxt [Data.exI],
162        DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
163end;
164
165(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
166          (! x1..xn x0. x0 = t --> (... & ...) --> P x0)
167*)
168local
169  fun tac ctxt =
170    SELECT_GOAL
171      (EVERY1 [REPEAT o dresolve_tac ctxt [Data.uncurry],
172        REPEAT o resolve_tac ctxt [Data.impI],
173        eresolve_tac ctxt [Data.mp],
174        REPEAT o eresolve_tac ctxt [Data.conjE],
175        REPEAT o ares_tac ctxt [Data.conjI]]);
176  val all_comm = Data.all_comm RS Data.iff_trans;
177  val All_comm = @{thm swap_params [THEN transitive]};
178in
179  fun prove_one_point_all_tac ctxt =
180    EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI,
181      resolve_tac ctxt [Data.iff_allI],
182      resolve_tac ctxt [Data.iffI],
183      tac ctxt,
184      tac ctxt];
185  fun prove_one_point_All_tac ctxt =
186    EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
187      resolve_tac ctxt [@{thm equal_allI}],
188      resolve_tac ctxt [@{thm equal_intr_rule}],
189      Object_Logic.atomize_prems_tac ctxt,
190      tac ctxt,
191      Object_Logic.atomize_prems_tac ctxt,
192      tac ctxt];
193end
194
195fun prove_conv ctxt tu tac =
196  let
197    val (goal, ctxt') =
198      yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
199    val thm =
200      Goal.prove ctxt' [] [] goal
201        (fn {context = ctxt'', ...} => tac ctxt'');
202  in singleton (Variable.export ctxt' ctxt) thm end;
203
204fun renumber l u (Bound i) =
205      Bound (if i < l orelse i > u then i else if i = u then l else i + 1)
206  | renumber l u (s $ t) = renumber l u s $ renumber l u t
207  | renumber l u (Abs (x, T, t)) = Abs (x, T, renumber (l + 1) (u + 1) t)
208  | renumber _ _ atom = atom;
209
210fun quantify qC x T xs P =
211  let
212    fun quant [] P = P
213      | quant ((qC, x, T) :: xs) P = quant xs (qC $ Abs (x, T, P));
214    val n = length xs;
215    val Q = if n = 0 then P else renumber 0 n P;
216  in quant xs (qC $ Abs (x, T, Q)) end;
217
218fun rearrange_all ctxt ct =
219  (case Thm.term_of ct of
220    F as (all as Const (q, _)) $ Abs (x, T, P) =>
221      (case extract_quant ctxt (K extract_imp) q P of
222        NONE => NONE
223      | SOME (xs, eq, Q) =>
224          let val R = quantify all x T xs (Data.imp $ eq $ Q)
225          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_all_tac)) end)
226  | _ => NONE);
227
228fun rearrange_All ctxt ct =
229  (case Thm.term_of ct of
230    F as (all as Const (q, _)) $ Abs (x, T, P) =>
231      (case extract_quant ctxt extract_implies q P of
232        NONE => NONE
233      | SOME (xs, eq, Q) =>
234          let val R = quantify all x T xs (Logic.implies $ eq $ Q)
235            in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end)
236  | _ => NONE);
237
238fun rearrange_ball tac ctxt ct =
239  (case Thm.term_of ct of
240    F as Ball $ A $ Abs (x, T, P) =>
241      (case extract_imp true [] P of
242        NONE => NONE
243      | SOME (xs, eq, Q) =>
244          if not (null xs) then NONE
245          else
246            let val R = Data.imp $ eq $ Q
247            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) (iff_reflection_tac THEN' tac)) end)
248  | _ => NONE);
249
250fun rearrange_ex ctxt ct =
251  (case Thm.term_of ct of
252    F as (ex as Const (q, _)) $ Abs (x, T, P) =>
253      (case extract_quant ctxt (K extract_conj) q P of
254        NONE => NONE
255      | SOME (xs, eq, Q) =>
256          let val R = quantify ex x T xs (Data.conj $ eq $ Q)
257          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end)
258  | _ => NONE);
259
260fun rearrange_bex tac ctxt ct =
261  (case Thm.term_of ct of
262    F as Bex $ A $ Abs (x, T, P) =>
263      (case extract_conj true [] P of
264        NONE => NONE
265      | SOME (xs, eq, Q) =>
266          if not (null xs) then NONE
267          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) (iff_reflection_tac THEN' tac)))
268  | _ => NONE);
269
270fun rearrange_Collect tac ctxt ct =
271  (case Thm.term_of ct of
272    F as Collect $ Abs (x, T, P) =>
273      (case extract_conj true [] P of
274        NONE => NONE
275      | SOME (_, eq, Q) =>
276          let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
277          in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' tac)) end)
278  | _ => NONE);
279
280end;
281
282