res_quanScript.sml

1(* res_quanScript.sml - Development of restricted quantifiers
2
3BY: Wai Wong
4DATE: 1 Aug 92
5CHANGED BY: Joe Hurd, June 2001 (to use predicate sets)
6CHANGED BY: Joe Hurd, June 2001 (to remove the ARB from RES_ABSTRACT)
7CHANGED BY: Joe Hurd, October 2001 (moved definitions to boolTheory)
8
9============================================================================*)
10Theory res_quan
11Ancestors
12  combin pred_set
13Libs
14  simpLib pred_setSimps boolSimps BasicProvers
15
16
17(* --------------------------------------------------------------------- *)
18(* Support theorems and code (not exported)                              *)
19(* --------------------------------------------------------------------- *)
20
21fun simp thml = ASM_SIMP_TAC (bool_ss ++ pred_setSimps.PRED_SET_ss) thml;
22val CONJ_AC = AC CONJ_COMM CONJ_ASSOC;
23val ELIM_EXISTS_IMP = GSYM boolTheory.LEFT_FORALL_IMP_THM;
24
25Theorem EMPTY[local]:
26    !s. (s = {}) <=> !x. x NOTIN s
27Proof
28  prove_tac [MEMBER_NOT_EMPTY]
29QED
30
31(* --------------------------------------------------------------------- *)
32(* Definitions to support restricted abstractions and quantifications    *)
33(* --------------------------------------------------------------------- *)
34
35(* JEH: Defns moved to boolTheory: the following versions remove lambdas *)
36
37Theorem RES_FORALL = RES_FORALL_THM;
38Theorem RES_EXISTS = RES_EXISTS_THM;
39Theorem RES_EXISTS_UNIQUE = RES_EXISTS_UNIQUE_THM;
40Theorem RES_SELECT = RES_SELECT_THM;
41Theorem RES_ABSTRACT = cj 1 RES_ABSTRACT_DEF
42
43(* ===================================================================== *)
44(* Properties of restricted quantification.                              *)
45(* --------------------------------------------------------------------- *)
46
47(* --------------------------------------------------------------------- *)
48(* RES_FORALL                                                            *)
49(* --------------------------------------------------------------------- *)
50
51Theorem RES_FORALL_CONJ_DIST:
52  !P Q R.
53     (!(i:'a)::P. (Q i /\ R i)) <=> (!i::P. Q i) /\ (!i::P. R i)
54Proof
55    REPEAT STRIP_TAC >> REWRITE_TAC [RES_FORALL]
56    >> BETA_TAC >> EQ_TAC >> REPEAT STRIP_TAC >> RES_TAC
57QED
58
59Theorem RES_FORALL_DISJ_DIST:
60  !P Q R.
61     (!(i:'a)::(\j. P j \/ Q j). R i) <=> (!i::P. R i) /\ (!i::Q. R i)
62Proof
63    REPEAT STRIP_TAC >> REWRITE_TAC [RES_FORALL, SPECIFICATION] >>
64    BETA_TAC >> EQ_TAC >> REPEAT STRIP_TAC >> RES_TAC
65QED
66
67Theorem RES_FORALL_UNIQUE:
68      !P j. (!(i:'a)::($= j). P i) = P j
69Proof
70    REWRITE_TAC [RES_FORALL, SPECIFICATION] >> BETA_TAC >>
71    PROVE_TAC []
72QED
73
74Theorem RES_FORALL_FORALL:
75      !(P:'a->bool) (R:'a->'b->bool) (x:'b).
76        (!x. !i::P. R i x) = (!i::P. !x. R i x)
77Proof
78    REPEAT STRIP_TAC >> REWRITE_TAC [RES_FORALL, SPECIFICATION]
79    >> BETA_TAC >> EQ_TAC >> REPEAT STRIP_TAC >> RES_TAC
80    >> FIRST_ASSUM MATCH_ACCEPT_TAC
81QED
82
83Theorem RES_FORALL_REORDER:
84      !(P:'a->bool) (Q:'b->bool) (R:'a->'b->bool).
85        (!i::P. !j::Q. R i j) = (!j::Q. !i::P. R i j)
86Proof
87    REPEAT STRIP_TAC >> REWRITE_TAC [RES_FORALL, SPECIFICATION] >>
88    BETA_TAC >> EQ_TAC >> REPEAT STRIP_TAC >> RES_TAC
89QED
90
91Theorem RES_FORALL_T:
92    !P s x. !x::s. T
93Proof
94  simp [RES_FORALL_TRUE]
95QED
96
97Theorem RES_FORALL_F:
98    !P s x. (!x::s. F) <=> (s = {})
99Proof
100  simp [RES_FORALL, EMPTY]
101QED
102
103Theorem RES_FORALL_EMPTY:
104     !(p : 'a -> bool). RES_FORALL {} p
105Proof
106   RW_TAC bool_ss [RES_FORALL, NOT_IN_EMPTY]
107QED
108
109Theorem RES_FORALL_UNIV:
110     !(p : 'a -> bool). RES_FORALL UNIV p = $! p
111Proof
112   RW_TAC bool_ss [RES_FORALL, IN_UNIV, ETA_AX]
113QED
114
115Theorem RES_FORALL_NULL:
116     !(p : 'a -> bool) m. RES_FORALL p (\x. m) = ((p = {}) \/ m)
117Proof
118   RW_TAC bool_ss [RES_FORALL, EXTENSION, NOT_IN_EMPTY]
119   >> Cases_on `m`
120   >> PROVE_TAC []
121QED
122
123Theorem NOT_RES_FORALL:
124    !P s. ~(!x::s. P x) <=> ?x::s. ~P x
125Proof
126  simp [RES_FORALL, RES_EXISTS]
127QED
128
129Theorem RES_FORALL_NOT_EMPTY:
130    !P s. ~RES_FORALL s P ==> (s <> {})
131Proof
132  rpt strip_tac >>
133  `RES_FORALL s P` suffices_by (simp []) >>
134  pop_assum SUBST1_TAC >>
135  MATCH_ACCEPT_TAC RES_FORALL_EMPTY
136QED
137
138Theorem RES_FORALL_SUBSET:
139    !P s t. s SUBSET t ==> RES_FORALL t P ==> RES_FORALL s P
140Proof
141  simp [RES_FORALL, SUBSET_DEF]
142QED
143
144Theorem RES_FORALL_UNION:
145    !P s t. RES_FORALL (s UNION t) P <=> RES_FORALL s P /\ RES_FORALL t P
146Proof
147  asm_simp_tac (bool_ss ++ DNF_ss ++ PRED_SET_ss) [RES_FORALL]
148QED
149
150Theorem RES_FORALL_DIFF:
151    !P s t x. (!x::s DIFF t. P x) <=> !x::s. x NOTIN t ==> P x
152Proof
153  simp [RES_FORALL, AND_IMP_INTRO]
154QED
155
156Theorem IN_BIGINTER_RES_FORALL:
157    !x sos. x IN BIGINTER sos <=> !s::sos. x IN s
158Proof
159  simp [RES_FORALL]
160QED
161
162Theorem RES_FORALL_BIGUNION:
163    !P sos. (!x::BIGUNION sos. P x) <=> !(s::sos) (x::s). P x
164Proof
165  simp [RES_FORALL, IN_BIGUNION] >>
166  prove_tac []
167QED
168
169Theorem RES_FORALL_BIGINTER:
170    !P sos. (!x::BIGINTER sos. P x) <=> !x. (!s::sos. x IN s) ==> P x
171Proof
172  simp [RES_FORALL]
173QED
174
175(* --------------------------------------------------------------------- *)
176(* RES_EXISTS                                                            *)
177(* --------------------------------------------------------------------- *)
178
179Theorem RES_EXISTS_DISJ_DIST:
180  !P Q R.
181     (?(i:'a)::P. (Q i \/ R i)) <=> (?i::P. Q i) \/ (?i::P. R i)
182Proof
183    REPEAT STRIP_TAC >> REWRITE_TAC [RES_EXISTS, SPECIFICATION]
184    >> BETA_TAC >> PURE_ONCE_REWRITE_TAC[CONJ_SYM]
185    >> PURE_ONCE_REWRITE_TAC[RIGHT_AND_OVER_OR]
186    >> CONV_TAC (ONCE_DEPTH_CONV EXISTS_OR_CONV) >> REFL_TAC
187QED
188
189Theorem RES_DISJ_EXISTS_DIST:
190  !P Q R.
191     (?(i:'a)::(\i. P i \/ Q i). R i) <=> (?i::P. R i) \/ (?i::Q. R i)
192Proof
193    REPEAT STRIP_TAC >> REWRITE_TAC [RES_EXISTS, SPECIFICATION]
194    >> BETA_TAC >> PURE_ONCE_REWRITE_TAC[RIGHT_AND_OVER_OR]
195    >> CONV_TAC (ONCE_DEPTH_CONV EXISTS_OR_CONV) >> REFL_TAC
196QED
197
198Theorem RES_EXISTS_EQUAL:
199      !P j. (?(i:'a)::($= j). P i) = P j
200Proof
201    REWRITE_TAC [RES_EXISTS, SPECIFICATION] >> BETA_TAC >> REPEAT GEN_TAC
202    >> EQ_TAC >|[
203      DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) >> ASM_REWRITE_TAC[],
204      DISCH_TAC >> EXISTS_TAC (``j:'a``) >>  ASM_REWRITE_TAC[]]
205QED
206
207Theorem RES_EXISTS_REORDER:
208      !(P:'a->bool) (Q:'b->bool) (R:'a->'b->bool).
209        (?i::P. ?j::Q. R i j) = (?j::Q. ?i::P. R i j)
210Proof
211    REPEAT STRIP_TAC >> REWRITE_TAC [RES_EXISTS, SPECIFICATION] >> BETA_TAC
212    >> EQ_TAC >> DISCH_THEN (CHOOSE_THEN STRIP_ASSUME_TAC) >|[
213      EXISTS_TAC (``x':'b``) >> CONJ_TAC >|[
214        ALL_TAC, EXISTS_TAC ``x:'a`` >> CONJ_TAC],
215      EXISTS_TAC ``x':'a`` >> CONJ_TAC >|[
216        ALL_TAC, EXISTS_TAC ``x:'b`` >> CONJ_TAC]]
217    >> FIRST_ASSUM ACCEPT_TAC
218QED
219
220Theorem RES_EXISTS_F:
221    !P s x. ~?s::x. F
222Proof
223  simp [RES_EXISTS_FALSE]
224QED
225
226Theorem RES_EXISTS_T:
227    !P s x. (?x::s. T) <=> (s <> {})
228Proof
229  simp [RES_EXISTS, EMPTY]
230QED
231
232Theorem RES_EXISTS_EMPTY:
233     !(p : 'a -> bool). ~RES_EXISTS {} p
234Proof
235   RW_TAC bool_ss [RES_EXISTS, NOT_IN_EMPTY]
236QED
237
238Theorem RES_EXISTS_UNIV:
239     !(p : 'a -> bool). RES_EXISTS UNIV p = $? p
240Proof
241   RW_TAC bool_ss [RES_EXISTS, IN_UNIV, ETA_AX]
242QED
243
244Theorem RES_EXISTS_NULL:
245     !(p : 'a -> bool) m. RES_EXISTS p (\x. m) = (~(p = {}) /\ m)
246Proof
247   RW_TAC bool_ss [RES_EXISTS, EXTENSION, NOT_IN_EMPTY]
248   >> Cases_on `m`
249   >> PROVE_TAC []
250QED
251
252Theorem RES_EXISTS_ALT:
253  !(p : 'a -> bool) m.
254      RES_EXISTS p m <=> (RES_SELECT p m) IN p /\ m (RES_SELECT p m)
255Proof
256   RW_TAC bool_ss [RES_EXISTS, EXISTS_DEF, RES_SELECT, SPECIFICATION]
257QED
258
259Theorem NOT_RES_EXISTS:
260    !P s. ~(?x::s. P x) <=> !x::s. ~P x
261Proof
262  simp [RES_FORALL, RES_EXISTS, GSYM IMP_DISJ_THM]
263QED
264
265Theorem RES_EXISTS_NOT_EMPTY:
266    !P s. RES_EXISTS s P ==> (s <> {})
267Proof
268  rpt strip_tac >>
269  `~RES_EXISTS s P` suffices_by simp [] >>
270  pop_assum SUBST1_TAC >>
271  MATCH_ACCEPT_TAC RES_EXISTS_EMPTY
272QED
273
274Theorem RES_EXISTS_SUBSET:
275    !P s t. s SUBSET t ==> RES_EXISTS s P ==> RES_EXISTS t P
276Proof
277  simp [RES_EXISTS, SUBSET_DEF] >>
278  prove_tac []
279QED
280
281Theorem RES_EXISTS_UNION:
282    !P s t. RES_EXISTS (s UNION t) P <=> RES_EXISTS s P \/ RES_EXISTS t P
283Proof
284  simp [RES_EXISTS] >>
285  prove_tac []
286QED
287
288Theorem RES_EXISTS_DIFF:
289    !P s t x. (?x::s DIFF t. P x) <=> ?x::s. x NOTIN t /\ P x
290Proof
291  simp [RES_EXISTS, CONJ_AC]
292QED
293
294Theorem IN_BIGUNION_RES_EXISTS:
295    !x sos. x IN BIGUNION sos <=> ?s::sos. x IN s
296Proof
297  simp [RES_FORALL, RES_EXISTS, CONJ_AC]
298QED
299
300Theorem RES_EXISTS_BIGUNION:
301    !P sos. (?x::BIGUNION sos. P x) <=> ?(s::sos) (x::s). P x
302Proof
303  simp [RES_EXISTS] >>
304  prove_tac []
305QED
306
307Theorem RES_EXISTS_BIGINTER:
308    !P sos. (?x::BIGINTER sos. P x) <=> ?x. (!s::sos. x IN s) /\ P x
309Proof
310  simp [RES_EXISTS, RES_FORALL] >>
311  prove_tac []
312QED
313
314(* --------------------------------------------------------------------- *)
315(* RES_EXISTS_UNIQUE                                                     *)
316(* --------------------------------------------------------------------- *)
317
318(* This one should be called ``RES_EXISTS_UNIQUE``, but the identifier is
319already used. *)
320Theorem RES_EXISTS_UNIQUE_ELIM:
321    !P s. (?!x::s. P x) <=> ?!x. x IN s /\ P x
322Proof
323  rpt gen_tac >>
324  simp [RES_EXISTS_UNIQUE, RES_FORALL, RES_EXISTS, EXISTS_UNIQUE_DEF] >>
325  prove_tac[]
326QED
327
328Theorem RES_EXISTS_UNIQUE_EXISTS:
329    !P s. RES_EXISTS_UNIQUE P s ==> RES_EXISTS P s
330Proof
331  simp [RES_EXISTS_UNIQUE, RES_EXISTS]
332QED
333
334Theorem RES_EXISTS_UNIQUE_F:
335    !P s x. ~?!x::s. F
336Proof
337  simp [RES_EXISTS_UNIQUE_ELIM, EXISTS_UNIQUE_THM]
338QED
339
340Theorem RES_EXISTS_UNIQUE_T:
341    !P s x. (?!x::s. T) <=> ?!x. x IN s
342Proof
343  simp [RES_EXISTS_UNIQUE_ELIM]
344QED
345
346Theorem RES_EXISTS_UNIQUE_EMPTY:
347     !(p : 'a -> bool). ~RES_EXISTS_UNIQUE {} p
348Proof
349   RW_TAC bool_ss [RES_EXISTS_UNIQUE, RES_EXISTS_EMPTY, NOT_IN_EMPTY]
350QED
351
352Theorem RES_EXISTS_UNIQUE_NOT_EMPTY:
353    !P s. RES_EXISTS_UNIQUE s P ==> (s <> {})
354Proof
355  rpt gen_tac >> disch_tac >>
356  imp_res_tac RES_EXISTS_UNIQUE_EXISTS >>
357  imp_res_tac RES_EXISTS_NOT_EMPTY
358QED
359
360Theorem RES_EXISTS_UNIQUE_UNIV:
361     !(p : 'a -> bool). RES_EXISTS_UNIQUE UNIV p = $?! p
362Proof
363   RW_TAC bool_ss [RES_EXISTS_UNIQUE, RES_EXISTS_UNIV, IN_UNIV,
364                   RES_FORALL_UNIV, EXISTS_UNIQUE_DEF]
365   >> KNOW_TAC ``$? (p:'a->bool) = ?x. p x`` >- RW_TAC bool_ss [ETA_AX]
366   >> DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
367   >> PROVE_TAC []
368QED
369
370Theorem RES_EXISTS_UNIQUE_NULL:
371     !(p : 'a -> bool) m. RES_EXISTS_UNIQUE p (\x. m) = ((?x. p = {x}) /\ m)
372Proof
373   RW_TAC bool_ss [RES_EXISTS_UNIQUE, RES_EXISTS_NULL, NOT_IN_EMPTY,
374                   RES_FORALL_NULL, EXISTS_UNIQUE_DEF, EXTENSION, IN_SING]
375   >> RW_TAC bool_ss [RES_EXISTS, RES_FORALL]
376   >> Cases_on `m`
377   >> PROVE_TAC []
378QED
379
380Theorem RES_EXISTS_UNIQUE_SING:
381    !P s x. (?!x::s. T) <=> ?y. s = {y}
382Proof
383  simp [RES_EXISTS_UNIQUE_NULL]
384QED
385
386Theorem RES_EXISTS_UNIQUE_ALT:
387     !(p : 'a -> bool) m.
388      RES_EXISTS_UNIQUE p m = (?x::p. m x /\ !y::p. m y ==> (y = x))
389Proof
390   RW_TAC bool_ss [SPECIFICATION, RES_EXISTS_UNIQUE, RES_EXISTS, RES_FORALL]
391   >> PROVE_TAC []
392QED
393
394(* --------------------------------------------------------------------- *)
395(* RES_SELECT                                                            *)
396(* --------------------------------------------------------------------- *)
397
398Theorem RES_SELECT_EMPTY:
399     !(p : 'a -> bool). RES_SELECT {} p = @x. F
400Proof
401   RW_TAC bool_ss [RES_SELECT, NOT_IN_EMPTY, ETA_AX]
402QED
403
404Theorem RES_SELECT_UNIV:
405     !(p : 'a -> bool). RES_SELECT UNIV p = $@ p
406Proof
407   RW_TAC bool_ss [RES_SELECT, IN_UNIV, ETA_AX]
408QED
409
410(* --------------------------------------------------------------------- *)
411(* RES_ABSTRACT                                                          *)
412(* --------------------------------------------------------------------- *)
413
414Theorem RES_ABSTRACT_EQUAL = CONJUNCT2 RES_ABSTRACT_DEF;
415
416Theorem RES_ABSTRACT_IDEMPOT:
417     !p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m
418Proof
419   REPEAT STRIP_TAC
420   >> MATCH_MP_TAC RES_ABSTRACT_EQUAL
421   >> RW_TAC bool_ss [RES_ABSTRACT]
422QED
423
424(* Sanity check for RES_ABSTRACT definition suggested by Lockwood Morris *)
425Theorem RES_ABSTRACT_EQUAL_EQ:
426     !p m1 m2.
427      (RES_ABSTRACT p m1 = RES_ABSTRACT p m2) =
428      (!x. x IN p ==> (m1 x = m2 x))
429Proof
430   REPEAT STRIP_TAC
431   >> EQ_TAC >|
432   [PROVE_TAC [RES_ABSTRACT],
433    PROVE_TAC [RES_ABSTRACT_EQUAL]]
434QED
435
436Theorem RES_ABSTRACT_UNIV:
437    !m. RES_ABSTRACT UNIV m = m
438Proof
439  gen_tac >>
440  `!x. RES_ABSTRACT UNIV m x = m x` suffices_by simp [Once FUN_EQ_THM] >>
441  simp [RES_ABSTRACT]
442QED
443
444val _ = let
445  val ^^ = Path.concat
446  infix ^^
447in
448  export_theory_as_docfiles (Path.parentArc ^^ "help" ^^ "thms")
449end
450
451(* Local Variables: *)
452(* fill-column: 78 *)
453(* indent-tabs-mode: nil *)
454(* End: *)