quotientScript.sml
1Theory quotient[bare]
2Ancestors
3 combin
4Libs
5 HolKernel Parse boolLib dep_rewrite simpLib boolSimps
6 Q[qualified] BasicProvers[qualified]
7
8(* --------------------------------------------------------------------- *)
9(* Fundamental definitions and theorems for the quotients package. *)
10(* Version 2.2. *)
11(* Date: April 11, 2005 *)
12(* --------------------------------------------------------------------- *)
13
14
15val REWRITE_THM = fn th => REWRITE_TAC[th];
16val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th];
17val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th])
18 THEN REWRITE_TAC[th];
19
20val POP_TAC = POP_ASSUM (fn th => ALL_TAC);
21val PROVE_TAC = metisLib.METIS_TAC
22
23
24(* =================================================================== *)
25(* To form a ABS / REP function or a equivalence relation REL from *)
26(* the corresponding functions/relations of the constituent subtypes *)
27(* of the main type, use the following table of operators: *)
28(* *)
29(* Type Operator Constructor Abstraction Equivalence *)
30(* *)
31(* Identity I x I $= *)
32(* Product (ty1 # ty2) (a,b) (abs1 ## abs2) (R1 ### R2) *)
33(* Sum (ty1 + ty2) (INL x) (abs1 ++ abs2) (R1 +++ R2) *)
34(* List (ty list) (CONS h t) (MAP abs) (LIST_REL R) *)
35(* Option (ty option) (SOME x) (OPTION_MAP abs) (OPTION_REL R) *)
36(* Function (ty1 -> ty2) (\x. f x) (rep1 --> abs2) (rep1 =-> abs2) *)
37(* (Strong respect) (R1 ===> R2) *)
38(* *)
39(* =================================================================== *)
40
41
42
43(* Equivalence relations: *)
44
45val EQUIV_def = new_definition("EQUIV_def",
46 “EQUIV E = !x y:'a. E x y = (E x = E y)”);
47
48(* Partial Equivalence relations: *)
49
50val PARTIAL_EQUIV_def = new_definition("PARTIAL_EQUIV_def",
51 “PARTIAL_EQUIV R <=> (?x:'a. R x x) /\
52 (!x y. R x y <=> R x x /\ R y y /\ (R x = R y))”);
53
54Theorem EQUIV_IMP_PARTIAL_EQUIV:
55 !R :'a -> 'a -> bool. EQUIV R ==> PARTIAL_EQUIV R
56Proof
57 REWRITE_TAC[EQUIV_def,PARTIAL_EQUIV_def]
58 THEN REPEAT STRIP_TAC
59 THEN PROVE_TAC[]
60QED
61
62(* Quotients, with partial equivalence relation, abstraction function, and
63 representation function: *)
64
65val QUOTIENT_def = new_definition("QUOTIENT_def",
66 “QUOTIENT R abs rep <=>
67 (!a:'b. abs (rep a) = a) /\
68 (!a. R (rep a) (rep a)) /\
69 (!(r:'a) (s:'a). R r s <=> R r r /\ R s s /\ (abs r = abs s))”);
70
71Theorem QUOTIENT_ABS_REP:
72 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==> (!a. abs (rep a) = a)
73Proof
74 REWRITE_TAC[QUOTIENT_def]
75 THEN REPEAT STRIP_TAC
76QED
77
78Theorem QUOTIENT_REP_REFL:
79 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
80 (!a. R (rep a) (rep a))
81Proof
82 REWRITE_TAC[QUOTIENT_def]
83 THEN REPEAT STRIP_TAC
84QED
85
86Theorem QUOTIENT_REL:
87 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
88 (!r s. R r s <=> R r r /\ R s s /\ (abs r = abs s))
89Proof
90 REWRITE_TAC[QUOTIENT_def]
91 THEN REPEAT STRIP_TAC
92QED
93
94Theorem QUOTIENT_REL_ABS:
95 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
96 (!r s. R r s ==> (abs r = abs s))
97Proof
98 REWRITE_TAC[QUOTIENT_def]
99 THEN REPEAT STRIP_TAC
100 THEN RES_TAC
101QED
102
103Theorem QUOTIENT_REL_ABS_EQ:
104 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
105 (!r s. R r r ==> R s s ==>
106 (R r s = (abs r = abs s)))
107Proof
108 REWRITE_TAC[QUOTIENT_def]
109 THEN REPEAT GEN_TAC
110 THEN STRIP_TAC
111 THEN POP_ASSUM (fn th => REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[th])
112 THEN ASM_REWRITE_TAC[]
113QED
114
115Theorem QUOTIENT_REL_REP:
116 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
117 (!a b. R (rep a) (rep b) = (a = b))
118Proof
119 REWRITE_TAC[QUOTIENT_def]
120 THEN REPEAT STRIP_TAC
121 THEN POP_ASSUM ONCE_REWRITE_THM
122 THEN ASM_REWRITE_TAC[]
123QED
124
125
126Theorem QUOTIENT_REP_ABS:
127 !R (abs:'a->'b) rep. QUOTIENT R abs rep ==>
128 (!r. R r r ==> R (rep (abs r)) r)
129Proof
130 REPEAT STRIP_TAC
131 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
132 THEN IMP_RES_TAC QUOTIENT_REP_REFL
133 THEN IMP_RES_TAC QUOTIENT_ABS_REP
134 THEN ASM_REWRITE_TAC[]
135QED
136
137
138
139
140Theorem IDENTITY_EQUIV:
141 EQUIV ($= : 'a -> 'a -> bool)
142Proof
143 REWRITE_TAC[EQUIV_def]
144 THEN REPEAT GEN_TAC
145 THEN EQ_TAC
146 THEN DISCH_THEN REWRITE_THM
147QED
148
149Theorem IDENTITY_QUOTIENT:
150 QUOTIENT $= (I:'a->'a) I
151Proof
152 REWRITE_TAC[QUOTIENT_def]
153 THEN REWRITE_TAC[I_THM]
154QED
155
156
157
158Theorem EQUIV_REFL_SYM_TRANS:
159 !R.
160 (!x y:'a. R x y = (R x = R y))
161 <=>
162 (!x. R x x) /\
163 (!x y. R x y ==> R y x) /\
164 (!x y z. R x y /\ R y z ==> R x z)
165Proof
166 GEN_TAC
167 THEN EQ_TAC
168 THEN STRIP_TAC
169 THEN REPEAT CONJ_TAC
170 THEN REPEAT GEN_TAC
171 THENL (* 4 subgoals *)
172 [
173 PURE_ASM_REWRITE_TAC[]
174 THEN REFL_TAC,
175
176 PURE_ASM_REWRITE_TAC[]
177 THEN MATCH_ACCEPT_TAC EQ_SYM,
178
179 PURE_ASM_REWRITE_TAC[]
180 THEN MATCH_ACCEPT_TAC EQ_TRANS,
181
182 CONV_TAC (RAND_CONV FUN_EQ_CONV)
183 THEN EQ_TAC
184 THEN DISCH_TAC
185 THENL
186 [ GEN_TAC
187 THEN EQ_TAC
188 THEN DISCH_TAC
189 THEN RES_TAC
190 THEN RES_TAC,
191
192 PURE_ASM_REWRITE_TAC[]
193 ]
194 ]
195QED
196
197
198Theorem QUOTIENT_SYM:
199 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
200 !x y. R x y ==> R y x
201Proof
202 REPEAT GEN_TAC
203 THEN STRIP_TAC
204 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
205 THEN PROVE_TAC[]
206QED
207
208Theorem QUOTIENT_TRANS:
209 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
210 !x y z. R x y /\ R y z ==> R x z
211Proof
212 REPEAT GEN_TAC
213 THEN STRIP_TAC
214 THEN REPEAT GEN_TAC
215 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
216 THEN PROVE_TAC[]
217QED
218
219
220(* FUNCTIONS: *)
221
222(* for ABS / REP of functions,
223 use (rep --> abs) for ABS, and (abs --> rep) for REP. *)
224
225val _ = set_fixity "-->" (Infixr 750);
226
227val FUN_MAP =
228 new_definition
229 ("FUN_MAP",
230 (“$--> (f:'a->'c) (g:'b->'d) = \h x. g (h (f x))”));
231
232Theorem FUN_MAP_THM:
233 !(f:'a -> 'c) (g:'b -> 'd) h x.
234 (f --> g) h x = g (h (f x))
235Proof
236 REPEAT GEN_TAC
237 THEN PURE_ONCE_REWRITE_TAC[FUN_MAP]
238 THEN BETA_TAC
239 THEN REFL_TAC
240QED
241
242Theorem FUN_MAP_I:
243 ((I:'a->'a) --> (I:'b->'b)) = I
244Proof
245 PURE_ONCE_REWRITE_TAC[FUN_MAP]
246 THEN CONV_TAC FUN_EQ_CONV
247 THEN GEN_TAC
248 THEN BETA_TAC
249 THEN REWRITE_TAC[I_THM,ETA_AX]
250QED
251
252Theorem IN_FUN:
253 !(f:'a -> 'b) (g:bool -> bool) s x.
254 x IN ((f --> g) s) <=> g ((f x) IN s)
255Proof
256 REPEAT GEN_TAC
257 THEN PURE_ONCE_REWRITE_TAC[IN_DEF]
258 THEN BETA_TAC
259 THEN REWRITE_TAC[FUN_MAP_THM]
260QED
261
262(*
263val SET_MAP_def =
264 Define
265 `SET_MAP (f:'a->'b) = (f --> (I:bool->bool))`;
266*)
267
268
269
270(* The strong version of FUN_REL: *)
271val FUN_REL = new_definition("FUN_REL",
272 “$===> (R1:'a->'b->bool) (R2:'c->'d->bool) f g =
273 !x y. R1 x y ==> R2 (f x) (g y)”);
274
275val _ = set_fixity "===>" (Infixr 490)
276val _ = TeX_notation {hol = "===>", TeX = ("\\HOLTokenLongimp", 2)};
277
278
279Theorem FUN_REL_EQ[simp]:
280 (($= :'a -> 'a -> bool) ===> ($= :'b -> 'b -> bool)) = $=
281Proof
282 CONV_TAC FUN_EQ_CONV
283 THEN GEN_TAC
284 THEN CONV_TAC FUN_EQ_CONV
285 THEN GEN_TAC
286 THEN PURE_ONCE_REWRITE_TAC[FUN_REL]
287 THEN CONV_TAC (RAND_CONV FUN_EQ_CONV)
288 THEN PROVE_TAC[]
289QED
290
291Theorem FUN_QUOTIENT:
292 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
293 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
294 QUOTIENT (R1 ===> R2) (rep1 --> abs2) (abs1 --> rep2)
295Proof
296 REPEAT STRIP_TAC
297 THEN REWRITE_TAC[QUOTIENT_def]
298 THEN REPEAT CONJ_TAC
299 THENL (* 3 subgoals *)
300 [ IMP_RES_TAC QUOTIENT_ABS_REP
301 THEN GEN_TAC
302 THEN CONV_TAC FUN_EQ_CONV
303 THEN GEN_TAC
304 THEN ASM_REWRITE_TAC[FUN_MAP_THM],
305
306 REWRITE_TAC[FUN_REL]
307 THEN REWRITE_TAC[FUN_MAP_THM]
308 THEN REPEAT GEN_TAC
309 THEN IMP_RES_THEN (fn th =>
310 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th]))) QUOTIENT_REL
311 THEN STRIP_TAC
312 THEN IMP_RES_TAC QUOTIENT_REP_REFL
313 THEN ASM_REWRITE_TAC[],
314
315 REPEAT GEN_TAC
316 THEN REWRITE_TAC[FUN_REL]
317 THEN CONV_TAC (RAND_CONV (RAND_CONV (RAND_CONV FUN_EQ_CONV)))
318 THEN REWRITE_TAC[FUN_REL,FUN_MAP_THM]
319 THEN EQ_TAC
320 THENL
321 [ REPEAT STRIP_TAC
322 THENL (* 3 subgoals *)
323 [ PROVE_TAC[QUOTIENT_REL],
324
325 PROVE_TAC[QUOTIENT_REL],
326
327 IMP_RES_TAC QUOTIENT_REL_ABS
328 THEN FIRST_ASSUM MATCH_MP_TAC
329 THEN FIRST_ASSUM MATCH_MP_TAC
330 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
331 ],
332
333 STRIP_TAC
334 THEN REPEAT GEN_TAC
335 THEN DISCH_TAC
336 THEN FIRST_ASSUM MP_TAC
337 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
338 THEN STRIP_TAC
339 THEN REPEAT CONJ_TAC
340 THENL (* 3 subgoals *)
341 [ FIRST_ASSUM MATCH_MP_TAC
342 THEN FIRST_ASSUM ACCEPT_TAC,
343
344 FIRST_ASSUM MATCH_MP_TAC
345 THEN FIRST_ASSUM ACCEPT_TAC,
346
347 IMP_RES_TAC QUOTIENT_REP_ABS
348 THEN RES_TAC
349 THEN IMP_RES_THEN (IMP_RES_THEN (ONCE_REWRITE_THM o GSYM))
350 QUOTIENT_REL_ABS
351 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
352 THEN ASM_REWRITE_TAC[]
353 ]
354 ]
355 ]
356QED
357
358(* NOTE: R1 ===> R2 is NOT an equivalence relation, but
359 does satisfy a quotient theorem. *)
360
361
362(* Definition of respectfulness for restricted quantification. *)
363
364val respects_def = new_definition ("respects_def",
365 “respects = W : ('a -> 'a -> 'b) -> 'a -> 'b”);
366
367(* Tests:
368
369``!f::respects(R1 ===> R2). f 1 = 2``;
370``!P::respects($= ===> $=). !n:num. P n``;
371
372*)
373
374
375Theorem RESPECTS:
376 !(R:'a->'a->bool) x.
377 respects R x = R x x
378Proof
379 REPEAT GEN_TAC
380 THEN REWRITE_TAC[respects_def,W_THM]
381QED
382
383Theorem IN_RESPECTS:
384 !(R:'a->'a->bool) x. x IN respects R <=> R x x
385Proof SIMP_TAC bool_ss [IN_DEF,RESPECTS]
386QED
387
388Theorem RESPECTS_THM:
389 !R1 R2 (f:'a->'b).
390 respects(R1 ===> R2) (f:'a->'b) = !x y. R1 x y ==> R2 (f x) (f y)
391Proof
392 REPEAT GEN_TAC
393 THEN REWRITE_TAC[respects_def,W_THM,FUN_REL]
394QED
395
396Theorem RESPECTS_MP:
397 !R1 R2 (f:'a->'b) x y.
398 respects(R1 ===> R2) f /\ R1 x y
399 ==> R2 (f x) (f y)
400Proof
401 REPEAT GEN_TAC
402 THEN REWRITE_TAC[RESPECTS_THM]
403 THEN STRIP_TAC
404 THEN RES_TAC
405QED
406
407
408Theorem RESPECTS_REP_ABS:
409 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
410 !(R2:'b->'b->bool).
411 !f x.
412 respects(R1 ===> R2) f /\ R1 x x
413 ==> R2 (f (rep1 (abs1 x))) (f x)
414Proof
415 REPEAT STRIP_TAC
416 THEN DEP_REWRITE_TAC [RESPECTS_MP]
417 THEN EXISTS_TAC ``R1:'a -> 'a -> bool``
418 THEN IMP_RES_TAC QUOTIENT_REP_ABS
419 THEN ASM_REWRITE_TAC[]
420QED
421
422Theorem RESPECTS_o:
423 !(R1:'a->'a->bool) (R2:'b->'b->bool) (R3:'c->'c->bool).
424 !f g.
425 respects(R2 ===> R3) f /\ respects(R1 ===> R2) g
426 ==> respects(R1 ===> R3) (f o g)
427Proof
428 REWRITE_TAC[RESPECTS_THM]
429 THEN REPEAT STRIP_TAC
430 THEN REWRITE_TAC[o_THM]
431 THEN FIRST_ASSUM MATCH_MP_TAC
432 THEN FIRST_ASSUM MATCH_MP_TAC
433 THEN FIRST_ASSUM ACCEPT_TAC
434QED
435
436
437(*
438val EXISTS_EQUIV_DEF =
439 Definition.new_definition
440 ("EXISTS_EQUIV_DEF", Term `?!! R = \P:'a->bool.
441 $? P /\ !x y. P x /\ P y ==> R x y`);
442
443val _ = add_const "?!!";
444
445val EXISTS_EQUIV = store_thm
446 ("EXISTS_EQUIV",
447 (“!R P.
448 ?!! R P = ($? P /\ !x y:'a. P x /\ P y ==> (R x y))”),
449 REPEAT GEN_TAC
450 THEN REWRITE_TAC[EXISTS_EQUIV_DEF]
451 THEN BETA_TAC
452 THEN REWRITE_TAC[]
453 );
454
455val EXISTS_UNIQUE_EQUIV = store_thm
456 ("EXISTS_UNIQUE_EQUIV",
457 (“$?! = ?!! ($= : 'a->'a->bool)”),
458 REWRITE_TAC[EXISTS_UNIQUE_DEF,EXISTS_EQUIV_DEF]
459 );
460
461*)
462
463(*
464val _ = (add_binder ("?!!", std_binder_precedence); add_const "?!")
465*)
466
467val EXISTS_EQUIV_DEF =
468 new_binder_definition("?!!", “?!!(P:'a->bool) = $?! P”);
469
470val RES_EXISTS_EQUIV_DEF =
471 Definition.new_definition
472 ("RES_EXISTS_EQUIV_DEF",
473 Term `RES_EXISTS_EQUIV =
474 \R P. (?(x : 'a) :: respects R. P x) /\
475 (!x y :: respects R. P x /\ P y ==> R x y)`);
476
477val _ = add_const "RES_EXISTS_EQUIV";
478
479val _ = associate_restriction ("?!!", "RES_EXISTS_EQUIV");
480
481(* Tests:
482``RES_EXISTS_EQUIV R (\x. x = 5)``;
483``?!!x :: R. x = 5``;
484*)
485
486Theorem RES_EXISTS_EQUIV:
487 !R m.
488 RES_EXISTS_EQUIV R m <=>
489 (?(x : 'a) :: respects R. m x) /\
490 (!x y :: respects R. m x /\ m y ==> (R x y))
491Proof
492 REPEAT GEN_TAC
493 THEN REWRITE_TAC[RES_EXISTS_EQUIV_DEF]
494 THEN BETA_TAC
495 THEN REFL_TAC
496QED
497
498(*
499val RES_EXISTS_UNIQUE_EQUIV_REL = store_thm
500 ("RES_EXISTS_UNIQUE_EQUIV_REL",
501 (“!R (m:'a -> bool).
502 (!x. x IN respects R ==> R x x) /\
503 RES_EXISTS_UNIQUE (respects R) m ==>
504 RES_EXISTS_EQUIV R m”),
505 REPEAT GEN_TAC
506 THEN REWRITE_TAC[res_quanTheory.RES_EXISTS_UNIQUE,RES_EXISTS_EQUIV]
507 THEN STRIP_TAC
508 THEN ASM_REWRITE_TAC[]
509 THEN REPEAT res_quanLib.RESQ_GEN_TAC
510 THEN STRIP_TAC
511 THEN res_quanLib.RESQ_RES_TAC
512 THEN RES_TAC
513 THEN POP_ASSUM MP_TAC
514 THEN POP_ASSUM MP_TAC
515 THEN POP_ASSUM MP_TAC
516 THEN POP_ASSUM MP_TAC
517 THEN POP_ASSUM MP_TAC
518 THEN ASM_REWRITE_TAC[]
519 );
520*)
521
522(*
523val RES_EXISTS_UNIQUE_EQUIV_REL = store_thm
524 ("RES_EXISTS_UNIQUE_EQUIV_REL",
525 (“!R m.
526 RES_EXISTS_UNIQUE (respects R) m ==>
527 RES_EXISTS_EQUIV (respects R) R m”),
528 REPEAT GEN_TAC
529 THEN REWRITE_TAC[res_quanTheory.RES_EXISTS_UNIQUE,RES_EXISTS_EQUIV]
530 THEN STRIP_TAC
531 THEN ASM_REWRITE_TAC[]
532 THEN REPEAT res_quanLib.RESQ_GEN_TAC
533 THEN STRIP_TAC
534 THEN res_quanLib.RESQ_RES_TAC
535 THEN RES_TAC
536 THEN POP_ASSUM MP_TAC
537 THEN POP_ASSUM MP_TAC
538 THEN POP_ASSUM MP_TAC
539 THEN ASM_REWRITE_TAC[]
540 THEN REWRITE_ALL_TAC[SPECIFICATION,RESPECTS]
541 THEN FIRST_ASSUM ACCEPT_TAC
542 );
543*)
544
545(* Not needed.
546
547val RES_EXISTS_UNIQUE_EQUIV = store_thm
548 ("RES_EXISTS_UNIQUE_EQUIV",
549 (“!p.
550 RES_EXISTS_UNIQUE p =
551 RES_EXISTS_EQUIV p ($= :'a->'a->bool)”),
552 GEN_TAC
553 THEN CONV_TAC FUN_EQ_CONV
554 THEN GEN_TAC
555 THEN REWRITE_TAC[res_quanTheory.RES_EXISTS_UNIQUE,RES_EXISTS_EQUIV]
556 );
557*)
558
559(* These don't work becuase of the extra parameter.
560``RES_EXISTS_EQUIV
561 (ALPHA) (* (\t. ?y u. t = Lam1 y u) *)
562 (\t. ?y. t = Lam1 y (Var1 y))
563 (ALPHA)``;
564``(?!!t :: (\t. ?y u. t = Lam1 y u). ?y. t = Lam1 y (Var1 y))`` handle e => Raise e;
565``(?!!t :: (\t. ?y u. t = Lam1 y u). ?y. t = Lam1 y (Var1 y)) (ALPHA)``;
566
567``(?!! (t :: (\t. ?y u. t = Lam1 y u) ALPHA). ?y. t = Lam1 y (Var1 y)))``;
568
569``RES_EXISTS_EQUIV (ALPHA ===> ($= :bool->bool->bool))
570 (\x. ?y. x = Lam1 y (Var1 y))``;
571*)
572
573
574
575Theorem FUN_REL_EQ_REL:
576 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
577 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
578 !f g.
579 (R1 ===> R2) f g =
580 (respects(R1 ===> R2) f /\ respects(R1 ===> R2) g /\
581 ((rep1 --> abs2) f = (rep1 --> abs2) g))
582Proof
583 REPEAT STRIP_TAC
584 THEN REWRITE_TAC[respects_def,W_THM]
585 THEN MATCH_MP_TAC QUOTIENT_REL
586 THEN EXISTS_TAC ``(abs1:'a -> 'c) --> (rep2:'d -> 'b)``
587 THEN DEP_REWRITE_TAC [FUN_QUOTIENT]
588 THEN ASM_REWRITE_TAC[]
589QED
590
591
592Theorem FUN_REL_MP:
593 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
594 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
595 !f g x y.
596 (R1 ===> R2) f g /\ (R1 x y)
597 ==> (R2 (f x) (g y))
598Proof
599 REWRITE_TAC[FUN_REL]
600 THEN REPEAT STRIP_TAC
601 THEN RES_TAC
602QED
603
604Theorem FUN_REL_IMP:
605 !(R1:'a->'a->bool) (R2:'b->'b->bool) f g x y.
606 (R1 ===> R2) f g /\ (R1 x y) ==> (R2 (f x) (g y))
607Proof
608 REPEAT GEN_TAC
609 THEN REWRITE_TAC[FUN_REL]
610 THEN STRIP_TAC
611 THEN RES_TAC
612QED
613
614
615Theorem FUN_REL_EQUALS:
616 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
617 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
618 !f g. respects(R1 ===> R2) f /\ respects(R1 ===> R2) g
619 ==> (((rep1 --> abs2) f = (rep1 --> abs2) g) =
620 (!x y. R1 x y ==> R2 (f x) (g y)))
621Proof
622 REPEAT GEN_TAC THEN STRIP_TAC
623 THEN REPEAT GEN_TAC
624 THEN POP_ASSUM ((fn th => DISCH_THEN (ASSUME_TAC o (MATCH_MP th)))
625 o MATCH_MP FUN_QUOTIENT)
626 THEN REWRITE_TAC[respects_def,W_THM]
627 THEN REWRITE_TAC[GSYM FUN_REL]
628 THEN REPEAT STRIP_TAC
629 THEN IMP_RES_TAC QUOTIENT_REL_ABS_EQ
630 THEN FIRST_ASSUM (ACCEPT_TAC o SYM)
631QED
632
633
634Theorem QT_FUN_REL_IMP:
635 !R1 (abs1:'a -> 'c) rep1.
636 QUOTIENT R1 abs1 rep1 ==>
637 !R2 (abs2:'b -> 'd) rep2.
638 QUOTIENT R2 abs2 rep2 ==>
639 !f g. respects(R1 ===> R2) f /\ respects(R1 ===> R2) g /\
640 ((rep1 --> abs2) f = (rep1 --> abs2) g) ==>
641 !x y. R1 x y ==> R2 (f x) (g y)
642Proof
643 REPEAT STRIP_TAC THEN IMP_RES_TAC FUN_REL_EQUALS
644QED
645
646
647
648(* Here are some definitional and well-formedness theorems
649 for some standard polymorphic operators.
650*)
651
652
653(* The most standard and common polymorphic operator of all
654 is clearly simple equality (=). Unfortunately, it does
655 not lift unchanged.
656*)
657
658Theorem EQUALS_PRS:
659 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
660 !x y. (x = y) = R (rep x) (rep y)
661Proof
662 REPEAT STRIP_TAC
663 THEN IMP_RES_TAC QUOTIENT_REL_REP
664 THEN ASM_REWRITE_TAC[]
665QED
666
667Theorem EQUALS_RSP:
668 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
669 !x1 x2 y1 y2.
670 R x1 x2 /\ R y1 y2 ==>
671 (R x1 y1 = R x2 y2)
672Proof
673 REPEAT STRIP_TAC
674 THEN EQ_TAC
675 THEN DISCH_TAC
676 THEN IMP_RES_TAC QUOTIENT_SYM
677 THEN IMP_RES_TAC QUOTIENT_TRANS
678QED
679
680
681
682(* Abstractions: LAMBDA, RES_ABSTRACT *)
683
684 (* (\x. f x) = ^(\x. v(f ^x)) *)
685Theorem LAMBDA_PRS:
686 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
687 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
688 !f. (\x. f x) = (rep1 --> abs2) (\x. rep2 (f (abs1 x)))
689Proof
690 REPEAT STRIP_TAC
691 THEN CONV_TAC FUN_EQ_CONV
692 THEN GEN_TAC
693 THEN REWRITE_TAC[FUN_MAP_THM]
694 THEN BETA_TAC
695 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
696QED
697
698Theorem LAMBDA_PRS1:
699 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
700 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
701 !f. (\x. f x) = (rep1 --> abs2) (\x. (abs1 --> rep2) f x)
702Proof
703 REPEAT STRIP_TAC
704 THEN CONV_TAC FUN_EQ_CONV
705 THEN GEN_TAC
706 THEN REWRITE_TAC[FUN_MAP_THM]
707 THEN BETA_TAC
708 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
709QED
710
711Theorem LAMBDA_RSP:
712 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
713 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
714 !f1 f2.
715 (R1 ===> R2) f1 f2 ==>
716 (R1 ===> R2) (\x. f1 x) (\y. f2 y)
717Proof
718 REWRITE_TAC[ETA_AX]
719QED
720
721Theorem ABSTRACT_PRS:
722 !R1 (abs1:'a -> 'c) rep1.
723 QUOTIENT R1 abs1 rep1 ==>
724 !R2 (abs2:'b -> 'd) rep2.
725 QUOTIENT R2 abs2 rep2 ==>
726 !f. f = (rep1 --> abs2) (RES_ABSTRACT (respects R1) ((abs1 --> rep2) f))
727Proof
728 REPEAT STRIP_TAC
729 THEN IMP_RES_THEN ASSUME_TAC QUOTIENT_REP_REFL
730 THEN IMP_RES_THEN ASSUME_TAC QUOTIENT_ABS_REP
731 THEN ASM_SIMP_TAC bool_ss [FUN_EQ_THM, cj 1 RES_ABSTRACT_DEF, respects_def,
732 W_THM, IN_DEF, FUN_MAP_THM]
733QED
734
735Theorem RES_ABSTRACT_RSP:
736 !R1 (abs1:'a -> 'c) rep1.
737 QUOTIENT R1 abs1 rep1 ==>
738 !R2 (abs2:'b -> 'd) rep2.
739 QUOTIENT R2 abs2 rep2 ==>
740 !f1 f2.
741 (R1 ===> R2) f1 f2 ==>
742 (R1 ===> R2) (RES_ABSTRACT (respects R1) f1)
743 (RES_ABSTRACT (respects R1) f2)
744Proof
745 REWRITE_TAC[FUN_REL]
746 THEN REPEAT STRIP_TAC
747 THEN first_x_assum $ drule_then assume_tac
748 THEN Q.RENAME_TAC [‘R2 (RES_ABSTRACT _ f1 x) (_ _ f2 y)’]
749 THEN Q.SUBGOAL_THEN ‘R1 x x /\ R1 y y’ strip_assume_tac
750 >- PROVE_TAC[QUOTIENT_REL] >>
751 asm_simp_tac bool_ss [IN_DEF, RES_ABSTRACT_DEF, respects_def, W_THM]
752QED
753
754Theorem LET_RES_ABSTRACT:
755 !r (lam:'a->'b) v.
756 v IN r ==> (LET (RES_ABSTRACT r lam) v = LET lam v)
757Proof
758 REPEAT GEN_TAC
759 THEN ONCE_REWRITE_TAC[LET_DEF]
760 THEN BETA_TAC
761 THEN REWRITE_TAC[RES_ABSTRACT_DEF]
762QED
763
764Theorem LAMBDA_REP_ABS_RSP:
765 !REL1 (abs1:'a -> 'c) rep1 REL2 (abs2:'b -> 'd) rep2 f1 f2.
766 ((!r r'. REL1 r r' ==> REL1 r (rep1 (abs1 r'))) /\
767 (!r r'. REL2 r r' ==> REL2 r (rep2 (abs2 r')))) /\
768 (REL1 ===> REL2) f1 f2 ==>
769 (REL1 ===> REL2) f1 ((abs1 --> rep2) ((rep1 --> abs2) f2))
770Proof
771 REPEAT GEN_TAC
772 THEN REWRITE_TAC[FUN_REL]
773 THEN REPEAT STRIP_TAC
774 THEN REWRITE_TAC[FUN_MAP]
775 THEN BETA_TAC
776 THEN BETA_TAC
777 THEN FIRST_ASSUM MATCH_MP_TAC
778 THEN FIRST_ASSUM MATCH_MP_TAC
779 THEN FIRST_ASSUM MATCH_MP_TAC
780 THEN FIRST_ASSUM ACCEPT_TAC
781QED
782
783
784Theorem REP_ABS_RSP:
785 !REL (abs:'a -> 'b) rep. QUOTIENT REL abs rep ==>
786 (!x1 x2.
787 REL x1 x2 ==>
788 REL x1 (rep (abs x2)))
789Proof
790 REPEAT GEN_TAC
791 THEN STRIP_TAC
792 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
793 THEN REPEAT GEN_TAC
794 THEN STRIP_TAC
795 THEN IMP_RES_TAC QUOTIENT_ABS_REP
796 THEN IMP_RES_TAC QUOTIENT_REP_REFL
797 THEN ASM_REWRITE_TAC[]
798QED
799
800
801(* ----------------------------------------------------- *)
802(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)
803(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
804(* ----------------------------------------------------- *)
805
806val IN_THM = REFL “(x:'a) IN P”
807 |> CONV_RULE (RAND_CONV (REWRITE_CONV [IN_DEF]))
808 |> RIGHT_LIST_BETA
809
810Theorem FORALL_PRS:
811 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
812 !f. $! f = RES_FORALL (respects R) ((abs --> I) f)
813Proof
814 REPEAT GEN_TAC
815 THEN STRIP_TAC
816 THEN GEN_TAC
817 THEN REWRITE_TAC[FORALL_DEF,RES_FORALL_THM]
818 THEN BETA_TAC
819 THEN CONV_TAC (LAND_CONV FUN_EQ_CONV
820 THENC RAND_CONV FUN_EQ_CONV)
821 THEN BETA_TAC
822 THEN REWRITE_TAC[FUN_MAP_THM,I_THM]
823 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
824 THEN EQ_TAC
825 THENL
826 [ DISCH_THEN REWRITE_THM,
827
828 DISCH_TAC
829 THEN GEN_TAC
830 THEN POP_ASSUM (MP_TAC o SPEC (“(rep:'b->'a) x”))
831 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
832 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
833 ]
834QED
835
836val RES_FORALL = RES_FORALL_THM
837Theorem RES_FORALL_RSP:
838 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
839 !f g.
840 (R ===> $=) f g ==>
841 (RES_FORALL (respects R) f = RES_FORALL (respects R) g)
842Proof
843 REPEAT GEN_TAC
844 THEN STRIP_TAC
845 THEN REPEAT GEN_TAC
846 THEN REWRITE_TAC[FUN_REL]
847 THEN DISCH_TAC
848 THEN REWRITE_TAC[RES_FORALL]
849 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
850 THEN EQ_TAC
851 THEN REPEAT STRIP_TAC
852 THEN RES_TAC
853QED
854
855
856Theorem RES_FORALL_PRS:
857 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
858 !P f. RES_FORALL P f = RES_FORALL ((abs --> I) P) ((abs --> I) f)
859Proof
860 REPEAT GEN_TAC
861 THEN STRIP_TAC
862 THEN REPEAT GEN_TAC
863 THEN REWRITE_TAC[RES_FORALL]
864 THEN REWRITE_TAC[IN_THM,FUN_MAP_THM,I_THM]
865 THEN EQ_TAC
866 THENL
867 [ DISCH_THEN REWRITE_THM,
868
869 DISCH_TAC
870 THEN GEN_TAC
871 THEN POP_ASSUM (MP_TAC o SPEC (“(rep:'b->'a) x”))
872 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
873 ]
874QED
875
876val RES_EXISTS = RES_EXISTS_THM
877Theorem EXISTS_PRS:
878 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
879 !f. $? f = RES_EXISTS (respects R) ((abs --> I) f)
880Proof
881 REPEAT GEN_TAC
882 THEN STRIP_TAC
883 THEN GEN_TAC
884 THEN REWRITE_TAC[boolTheory.EXISTS_DEF,RES_EXISTS]
885 THEN BETA_TAC
886 THEN REWRITE_TAC[FUN_MAP_THM,I_THM]
887 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
888 THEN EQ_TAC
889 THENL
890 [ DISCH_TAC
891 THEN MATCH_MP_TAC (BETA_RULE
892 (SPEC ``\x:'a. R x x /\ f ((abs x):'b)`` SELECT_AX))
893 THEN EXISTS_TAC (“(rep:'b->'a) ($@ f)”)
894 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
895 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
896 THEN FIRST_ASSUM ACCEPT_TAC,
897
898 STRIP_TAC
899 THEN MATCH_MP_TAC SELECT_AX
900 THEN EXISTS_TAC (“(abs:'a->'b) (@x. R x x /\ f (abs x))”)
901 THEN FIRST_ASSUM ACCEPT_TAC
902 ]
903QED
904
905Theorem RES_EXISTS_RSP:
906 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
907 !f g.
908 (R ===> $=) f g ==>
909 (RES_EXISTS (respects R) f = RES_EXISTS (respects R) g)
910Proof
911 REPEAT GEN_TAC
912 THEN STRIP_TAC
913 THEN REPEAT GEN_TAC
914 THEN REWRITE_TAC[FUN_REL]
915 THEN DISCH_TAC
916 THEN REWRITE_TAC[RES_EXISTS]
917 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
918 THEN EQ_TAC
919 THEN REPEAT STRIP_TAC
920 THEN RES_TAC
921 THEN EXISTS_TAC ``x:'a``
922 THEN ASM_REWRITE_TAC[]
923QED
924
925
926Theorem RES_EXISTS_PRS:
927 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
928 !P f. RES_EXISTS P f = RES_EXISTS ((abs --> I) P) ((abs --> I) f)
929Proof
930 REPEAT GEN_TAC
931 THEN STRIP_TAC
932 THEN REPEAT GEN_TAC
933 THEN REWRITE_TAC[RES_EXISTS]
934 THEN REWRITE_TAC[IN_THM,FUN_MAP_THM,I_THM]
935 THEN EQ_TAC
936 THENL
937 [ STRIP_TAC
938 THEN EXISTS_TAC (“(rep:'b->'a) x”)
939 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
940 THEN ASM_REWRITE_TAC[],
941
942 STRIP_TAC
943 THEN EXISTS_TAC (“(abs:'a->'b) x”)
944 THEN ASM_REWRITE_TAC[]
945 ]
946QED
947
948
949Theorem EXISTS_UNIQUE_PRS:
950 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
951 !f. $?! f = RES_EXISTS_EQUIV R ((abs --> I) f)
952Proof
953 REPEAT GEN_TAC
954 THEN STRIP_TAC
955 THEN GEN_TAC
956 THEN REWRITE_TAC[boolTheory.EXISTS_UNIQUE_DEF,RES_EXISTS_EQUIV]
957 THEN BETA_TAC
958 THEN MK_COMB_TAC
959 THENL
960 [ AP_TERM_TAC
961 THEN IMP_RES_TAC EXISTS_PRS
962 THEN ASM_REWRITE_TAC[]
963 THEN CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
964 THEN REFL_TAC,
965
966 REWRITE_TAC[FUN_MAP_THM,I_THM]
967 THEN REWRITE_TAC[RES_FORALL]
968 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
969 THEN BETA_TAC
970 THEN EQ_TAC
971 THENL
972 [ REPEAT STRIP_TAC
973 THEN IMP_RES_TAC QUOTIENT_REL_ABS_EQ
974 THEN FIRST_ASSUM MATCH_MP_TAC
975 THEN RES_TAC,
976
977 REPEAT STRIP_TAC
978 THEN FIRST_ASSUM (MP_TAC o SPEC (“(rep:'b->'a) x”))
979 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
980 THEN DISCH_THEN (MP_TAC o SPEC (“(rep:'b->'a) y”))
981 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
982 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
983 THEN DISCH_TAC
984 THEN RES_TAC
985 THEN POP_ASSUM MP_TAC
986 THEN IMP_RES_THEN ONCE_REWRITE_THM QUOTIENT_REL
987 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL
988 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
989 ]
990 ]
991QED
992
993Theorem RES_EXISTS_EQUIV_RSP:
994 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
995 !f g.
996 (R ===> $=) f g ==>
997 (RES_EXISTS_EQUIV R f =
998 RES_EXISTS_EQUIV R g)
999Proof
1000 REPEAT GEN_TAC
1001 THEN STRIP_TAC
1002 THEN REPEAT GEN_TAC
1003 THEN REWRITE_TAC[FUN_REL]
1004 THEN DISCH_TAC
1005 THEN REWRITE_TAC[RES_EXISTS_EQUIV]
1006 THEN MK_COMB_TAC
1007 THENL
1008 [ AP_TERM_TAC
1009 THEN REWRITE_TAC[ETA_AX]
1010 THEN IMP_RES_THEN (fn th => DEP_REWRITE_TAC[th]) RES_EXISTS_RSP
1011 THEN ASM_REWRITE_TAC[FUN_REL],
1012
1013 REWRITE_TAC[RES_FORALL]
1014 THEN REWRITE_TAC[IN_THM,respects_def,W_THM]
1015 THEN BETA_TAC
1016 THEN EQ_TAC
1017 THENL
1018 [ REPEAT STRIP_TAC
1019 THEN RES_TAC
1020 THEN RES_TAC,
1021
1022 REPEAT STRIP_TAC
1023 THEN RES_TAC
1024 THEN RES_TAC
1025 ]
1026 ]
1027QED
1028
1029
1030(*
1031val RES_EXISTS_UNIQUE_PRS = store_thm
1032 ("RES_EXISTS_UNIQUE_PRS",
1033 (“!REL (abs:'a -> 'b) rep.
1034 (!a. abs (rep a) = a) /\ (!r r'. REL r r' = (abs r = abs r'))
1035 ==>
1036 !P f. RES_EXISTS_UNIQUE P f =
1037 RES_EXISTS_EQUIV ((abs --> I) P) REL ((abs --> I) f)”),
1038 REPEAT GEN_TAC
1039 THEN STRIP_TAC
1040 THEN REPEAT GEN_TAC
1041 THEN REWRITE_TAC[RES_EXISTS_UNIQUE_DEF,RES_EXISTS_EQUIV]
1042 THEN BETA_TAC
1043 THEN MK_COMB_TAC
1044 THENL
1045 [ AP_TERM_TAC
1046 THEN IMP_RES_TAC RES_EXISTS_PRS
1047 THEN ASM_REWRITE_TAC[FUN_MAP,I_THM,ETA_AX],
1048
1049 CONV_TAC (DEPTH_CONV RES_FORALL_CONV)
1050 THEN REWRITE_TAC[IN_THM,FUN_MAP_THM,I_THM]
1051 THEN EQ_TAC
1052 THENL
1053 [ REPEAT STRIP_TAC
1054 THEN RES_TAC
1055 THEN RES_TAC,
1056
1057 CONV_TAC (LAND_CONV (DEPTH_CONV RIGHT_IMP_FORALL_CONV))
1058 THEN REWRITE_TAC[AND_IMP_INTRO]
1059 THEN REPEAT STRIP_TAC
1060 THEN FIRST_ASSUM (SUBST1_TAC o SYM o SPEC (“x:'b”))
1061 THEN FIRST_ASSUM (SUBST1_TAC o SYM o SPEC (“y:'b”))
1062 THEN FIRST_ASSUM (REWRITE_THM o SYM o SPEC_ALL)
1063 THEN FIRST_ASSUM MATCH_MP_TAC
1064 THEN ASM_REWRITE_TAC[]
1065 ]
1066 ]
1067 );
1068
1069*)
1070
1071(* I don't think the select operator is respectful of equivalence.
1072RES_SELECT is not defined in all cases,
1073and even in those its value may not be well-behaved.
1074
1075val RES_SELECT_FUN_PRS = store_thm
1076 ("RES_SELECT_FUN_PRS",
1077 (“!REL1 (abs1:'a -> 'c) rep1 REL2 (abs2:'b -> 'd) rep2.
1078 (!a. abs1 (rep1 a) = a) /\ (!r r'. REL1 r r' = (abs1 r = abs1 r'))
1079 ==>
1080 (!a. abs2 (rep2 a) = a) /\ (!r r'. REL2 r r' = (abs2 r = abs2 r'))
1081 ==>
1082 !f. $@ f = (rep1 --> abs2)
1083 (RES_SELECT (respects(REL1,REL2))
1084 (((rep1 --> abs2) --> I) f))”),
1085 REPEAT GEN_TAC
1086 THEN STRIP_TAC
1087 THEN STRIP_TAC
1088 THEN REPEAT GEN_TAC
1089 THEN CONV_TAC FUN_EQ_CONV
1090 THEN GEN_TAC
1091 THEN REWRITE_TAC[FUN_MAP_THM]
1092 THEN REWRITE_TAC[res_quanTheory.RES_SELECT]
1093 THEN REWRITE_TAC[IN_THM,respects_def]
1094 THEN BETA_TAC
1095 THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM]
1096 THEN CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV (GSYM ETA_AX))))
1097 THEN DEP_REWRITE_TAC[FUN_REL_ABS_REP]
1098 THEN ASM_REWRITE_TAC[]
1099 THEN PROVE_TAC[]
1100 );
1101
1102val RES_SELECT_FUN_RSP = store_thm
1103 ("RES_SELECT_FUN_RSP",
1104 (“!REL1 (abs1:'a -> 'd) rep1 REL2 (abs2:'b -> 'e) rep2
1105 REL3 (abs3:'c -> 'f) rep3.
1106 (!a. abs1 (rep1 a) = a) /\ (!r r'. REL1 r r' = (abs1 r = abs1 r'))
1107 ==>
1108 (!a. abs2 (rep2 a) = a) /\ (!r r'. REL2 r r' = (abs2 r = abs2 r'))
1109 ==>
1110 (!a. abs3 (rep3 a) = a) /\ (!r r'. REL3 r r' = (abs3 r = abs3 r'))
1111 ==>
1112 !f1 f2.
1113 ((REL1 ===> REL2) ===> REL3) f1 f2 ==>
1114 ((REL1 ===> REL2) ===> REL3) (RES_SELECT (respects(REL1,REL2)) f1)
1115 (RES_SELECT (respects(REL1,REL2)) f2)
1116 ”),
1117 REPEAT GEN_TAC
1118 THEN ONCE_REWRITE_TAC[FUN_REL]
1119 THEN REPEAT STRIP_TAC
1120 THEN RES_TAC
1121 THEN DEP_REWRITE_TAC[res_quanTheory.RES_SELECT]
1122 THEN REWRITE_TAC[IN_THM,respects_def]
1123 THEN BETA_TAC
1124 THEN POP_ASSUM REWRITE_THM
1125 THEN POP_ASSUM MP_TAC
1126 THEN REWRITE_TAC[FUN_REL]
1127 THEN PROVE_TAC[]
1128 );
1129
1130*)
1131
1132
1133(* bool theory: COND, LET *)
1134
1135Theorem COND_PRS:
1136 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
1137 !a b c. COND a b c = abs (COND a (rep b) (rep c))
1138Proof
1139 REPEAT STRIP_TAC
1140 THEN REWRITE_TAC[GSYM COND_RAND]
1141 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
1142QED
1143
1144Theorem COND_RSP:
1145 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
1146 !a1 a2 b1 b2 c1 c2.
1147 (a1 = a2) /\ R b1 b2 /\ R c1 c2
1148 ==> R (COND a1 b1 c1) (COND a2 b2 c2)
1149Proof
1150 REPEAT GEN_TAC
1151 THEN STRIP_TAC
1152 THEN REPEAT GEN_TAC
1153 THEN STRIP_TAC
1154 THEN ASM_REWRITE_TAC[]
1155 THEN COND_CASES_TAC
1156 THEN ASM_REWRITE_TAC[]
1157QED
1158
1159
1160Theorem LET_PRS:
1161 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1162 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1163 !f x. LET f x = abs2 (LET ((abs1-->rep2) f) (rep1 x))
1164Proof
1165 REPEAT STRIP_TAC
1166 THEN PURE_ONCE_REWRITE_TAC[LET_DEF]
1167 THEN BETA_TAC
1168 THEN REWRITE_TAC[FUN_MAP]
1169 THEN BETA_TAC
1170 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
1171QED
1172
1173Theorem LET_RSP:
1174 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1175 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1176 !f g x y.
1177 (R1 ===> R2) f g /\ R1 x y ==>
1178 R2 (LET f x) (LET g y)
1179Proof
1180 REPEAT STRIP_TAC
1181 THEN PURE_ONCE_REWRITE_TAC[LET_DEF]
1182 THEN BETA_TAC
1183 THEN IMP_RES_TAC FUN_REL_MP
1184QED
1185
1186Theorem literal_case_PRS:
1187 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1188 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1189 !f x. literal_case f x = abs2 (literal_case ((abs1-->rep2) f) (rep1 x))
1190Proof
1191 REPEAT STRIP_TAC
1192 THEN PURE_ONCE_REWRITE_TAC[literal_case_DEF]
1193 THEN BETA_TAC
1194 THEN REWRITE_TAC[FUN_MAP]
1195 THEN BETA_TAC
1196 THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
1197QED
1198
1199Theorem literal_case_RSP:
1200 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1201 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1202 !f g x y.
1203 (R1 ===> R2) f g /\ R1 x y ==>
1204 R2 (literal_case f x) (literal_case g y)
1205Proof
1206 REPEAT STRIP_TAC
1207 THEN PURE_ONCE_REWRITE_TAC[literal_case_DEF]
1208 THEN BETA_TAC
1209 THEN IMP_RES_TAC FUN_REL_MP
1210QED
1211
1212
1213
1214(* FUNCTION APPLICATION *)
1215
1216Theorem APPLY_PRS:
1217 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1218 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1219 !f x. f x = abs2 (((abs1-->rep2) f) (rep1 x))
1220Proof
1221 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
1222 THEN REWRITE_TAC[FUN_MAP_THM]
1223 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1224 THEN ASM_REWRITE_TAC[]
1225QED
1226
1227Theorem APPLY_RSP:
1228 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1229 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1230 !f g x y.
1231 (R1 ===> R2) f g /\ R1 x y ==>
1232 R2 (f x) (g y)
1233Proof
1234 REPEAT STRIP_TAC
1235 THEN IMP_RES_TAC FUN_REL_MP
1236QED
1237
1238
1239(* combin theory: I, K, o, C, W *)
1240
1241
1242Theorem I_PRS:
1243 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
1244 !e. I e = abs (I (rep e))
1245Proof
1246 REPEAT STRIP_TAC
1247 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1248 THEN ASM_REWRITE_TAC[I_THM]
1249QED
1250
1251Theorem I_RSP:
1252 !R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
1253 !e1 e2.
1254 R e1 e2 ==>
1255 R (I e1) (I e2)
1256Proof
1257 REPEAT GEN_TAC
1258 THEN DISCH_TAC
1259 THEN REWRITE_TAC[I_THM]
1260QED
1261
1262Theorem K_PRS:
1263 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1264 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1265 !x y. K x y = abs1 (K (rep1 x) (rep2 y))
1266Proof
1267 REPEAT STRIP_TAC
1268 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1269 THEN ASM_REWRITE_TAC[K_THM]
1270QED
1271
1272Theorem K_RSP:
1273 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1274 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1275 !x1 x2 y1 y2.
1276 R1 x1 x2 /\ R2 y1 y2 ==>
1277 R1 (K x1 y1) (K x2 y2)
1278Proof
1279 REPEAT STRIP_TAC
1280 THEN ASM_REWRITE_TAC[K_THM]
1281QED
1282
1283Theorem o_PRS:
1284 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1285 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1286 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1287 !f g. f o g =
1288 (rep1-->abs3) ( ((abs2-->rep3) f) o ((abs1-->rep2) g) )
1289Proof
1290 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
1291 THEN REPEAT GEN_TAC
1292 THEN CONV_TAC FUN_EQ_CONV
1293 THEN GEN_TAC
1294 THEN PURE_ONCE_REWRITE_TAC[o_THM]
1295 THEN REWRITE_TAC[FUN_MAP_THM,o_THM]
1296 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1297 THEN ASM_REWRITE_TAC[]
1298QED
1299
1300Theorem o_RSP:
1301 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1302 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1303 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1304 !f1 f2 g1 g2.
1305 (R2 ===> R3) f1 f2 /\ (R1 ===> R2) g1 g2 ==>
1306 (R1 ===> R3) (f1 o g1) (f2 o g2)
1307Proof
1308 REPEAT GEN_TAC THEN DISCH_TAC
1309 THEN REPEAT GEN_TAC THEN DISCH_TAC
1310 THEN REPEAT GEN_TAC THEN DISCH_TAC
1311 THEN REPEAT GEN_TAC
1312 THEN REWRITE_TAC[FUN_REL]
1313 THEN REPEAT STRIP_TAC
1314 THEN REWRITE_TAC[o_THM]
1315 THEN FIRST_ASSUM MATCH_MP_TAC
1316 THEN FIRST_ASSUM MATCH_MP_TAC
1317 THEN FIRST_ASSUM ACCEPT_TAC
1318QED
1319
1320Theorem C_PRS:
1321 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1322 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1323 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1324 !f x y. combin$C f x y =
1325 abs3 (combin$C ((abs1-->abs2-->rep3) f) (rep2 x) (rep1 y))
1326Proof
1327 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
1328 THEN REPEAT GEN_TAC
1329 THEN PURE_ONCE_REWRITE_TAC[C_THM]
1330 THEN REWRITE_TAC[FUN_MAP_THM]
1331 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1332 THEN ASM_REWRITE_TAC[]
1333QED
1334
1335Theorem C_RSP:
1336 !R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
1337 !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
1338 !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
1339 !f1 f2 x1 x2 y1 y2.
1340 (R1 ===> R2 ===> R3) f1 f2 /\ R2 x1 x2 /\ R1 y1 y2 ==>
1341 R3 (combin$C f1 x1 y1) (combin$C f2 x2 y2)
1342Proof
1343 REWRITE_TAC[FUN_REL]
1344 THEN REPEAT STRIP_TAC
1345 THEN REWRITE_TAC[C_THM]
1346 THEN RES_TAC
1347QED
1348
1349Theorem W_PRS:
1350 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1351 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1352 !f x. W f x = abs2 (W ((abs1-->abs1-->rep2) f) (rep1 x))
1353Proof
1354 REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
1355 THEN REPEAT GEN_TAC
1356 THEN PURE_ONCE_REWRITE_TAC[W_THM]
1357 THEN REWRITE_TAC[FUN_MAP_THM]
1358 THEN IMP_RES_TAC QUOTIENT_ABS_REP
1359 THEN ASM_REWRITE_TAC[]
1360QED
1361
1362Theorem W_RSP:
1363 !R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1364 !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
1365 !f1 f2 x1 x2.
1366 (R1 ===> R1 ===> R2) f1 f2 /\ R1 x1 x2 ==>
1367 R2 (W f1 x1) (W f2 x2)
1368Proof
1369 REWRITE_TAC[FUN_REL]
1370 THEN REPEAT STRIP_TAC
1371 THEN REWRITE_TAC[W_THM]
1372 THEN RES_TAC
1373QED
1374
1375
1376
1377(* ----------------------------------------- *)
1378(* theorems for regularized version of goals *)
1379(* ----------------------------------------- *)
1380
1381
1382Theorem EQ_IMPLIES = boolTheory.EQ_IMPLIES
1383
1384Theorem EQUALS_IMPLIES:
1385 !P P' Q Q':'a.
1386 (P = Q) /\ (P' = Q') ==>
1387 ((P = P') ==> (Q = Q'))
1388Proof
1389 REPEAT GEN_TAC
1390 THEN STRIP_TAC
1391 THEN ASM_REWRITE_TAC[]
1392QED
1393
1394Theorem CONJ_IMPLIES:
1395 !P P' Q Q'.
1396 (P ==> Q) /\ (P' ==> Q') ==>
1397 (P /\ P' ==> Q /\ Q')
1398Proof
1399 REPEAT STRIP_TAC
1400 THEN RES_TAC
1401QED
1402
1403Theorem DISJ_IMPLIES:
1404 !P P' Q Q'.
1405 (P ==> Q) /\ (P' ==> Q') ==>
1406 (P \/ P' ==> Q \/ Q')
1407Proof
1408 REPEAT STRIP_TAC
1409 THENL [ DISJ1_TAC, DISJ2_TAC ]
1410 THEN RES_TAC
1411QED
1412
1413Theorem IMP_IMPLIES:
1414 !P P' Q Q'.
1415 (Q ==> P) /\ (P' ==> Q') ==>
1416 ((P ==> P') ==> (Q ==> Q'))
1417Proof
1418 REPEAT STRIP_TAC
1419 THEN RES_TAC
1420 THEN RES_TAC
1421 THEN RES_TAC
1422QED
1423
1424Theorem NOT_IMPLIES:
1425 !P Q.
1426 (Q ==> P) ==>
1427 (~P ==> ~Q)
1428Proof
1429 REPEAT STRIP_TAC
1430 THEN RES_TAC
1431 THEN RES_TAC
1432QED
1433
1434Theorem EQUALS_EQUIV_IMPLIES:
1435 !R:'a -> 'a -> bool.
1436 EQUIV R ==>
1437 R a1 a2 /\ R b1 b2 ==>
1438 ((a1 = b1) ==> R a2 b2)
1439Proof
1440 REWRITE_TAC[EQUIV_def]
1441 THEN REPEAT STRIP_TAC
1442 THEN POP_ASSUM REWRITE_ALL_THM
1443 THEN IMP_RES_TAC EQUIV_REFL_SYM_TRANS
1444QED
1445
1446(*
1447val EQUALS_EQUIV_IMPLIES1 = store_thm
1448 ("EQUALS_EQUIV_IMPLIES1",
1449 (“!R:'a -> 'a -> bool.
1450 EQUIV R ==>
1451 (R a1 b1 ==> R a2 b2) ==>
1452 ((a1 = b1) ==> R a2 b2)”),
1453 REWRITE_TAC[EQUIV_def]
1454 THEN REPEAT STRIP_TAC
1455 THEN POP_ASSUM REWRITE_ALL_THM
1456 THEN FIRST_ASSUM MATCH_MP_TAC
1457 THEN ASM_REWRITE_TAC[]
1458 );
1459*)
1460
1461Theorem ABSTRACT_RES_ABSTRACT:
1462 !(R1:'a -> 'a -> bool) (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1463 !(R2:'b -> 'b -> bool) f g.
1464 (R1 ===> R2) f g ==>
1465 (R1 ===> R2) f (RES_ABSTRACT (respects R1) g)
1466Proof
1467 REWRITE_TAC[FUN_REL]
1468 THEN REPEAT STRIP_TAC
1469 THEN DEP_REWRITE_TAC[cj 1 RES_ABSTRACT_DEF]
1470 THEN RES_THEN REWRITE_THM
1471 THEN REWRITE_TAC[IN_THM,RESPECTS]
1472 THEN POP_ASSUM MP_TAC
1473 THEN IMP_RES_THEN (CONV_TAC o LAND_CONV o REWR_CONV) QUOTIENT_REL
1474 THEN STRIP_TAC
1475QED
1476
1477Theorem RES_ABSTRACT_ABSTRACT:
1478 !(R1:'a -> 'a -> bool) (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
1479 !(R2:'b -> 'b -> bool) f g.
1480 (R1 ===> R2) f g ==>
1481 (R1 ===> R2) (RES_ABSTRACT (respects R1) f) g
1482Proof
1483 REWRITE_TAC[FUN_REL]
1484 THEN REPEAT STRIP_TAC
1485 THEN DEP_REWRITE_TAC[cj 1 RES_ABSTRACT_DEF]
1486 THEN RES_THEN REWRITE_THM
1487 THEN REWRITE_TAC[IN_THM,RESPECTS]
1488 THEN POP_ASSUM MP_TAC
1489 THEN IMP_RES_THEN (CONV_TAC o LAND_CONV o REWR_CONV) QUOTIENT_REL
1490 THEN STRIP_TAC
1491QED
1492
1493Theorem EQUIV_RES_ABSTRACT_LEFT:
1494 !R1 R2 (f1:'a -> 'b) (f2:'a -> 'b) x1 x2.
1495 R2 (f1 x1) (f2 x2) /\ R1 x1 x1 ==>
1496 R2 (RES_ABSTRACT (respects R1) f1 x1) (f2 x2)
1497Proof
1498 REPEAT STRIP_TAC
1499 THEN DEP_REWRITE_TAC[cj 1 RES_ABSTRACT_DEF]
1500 THEN REWRITE_TAC[IN_THM,RESPECTS]
1501 THEN ASM_REWRITE_TAC[]
1502QED
1503
1504Theorem EQUIV_RES_ABSTRACT_RIGHT:
1505 !R1 R2 (f1:'a -> 'b) (f2:'a -> 'b) x1 x2.
1506 R2 (f1 x1) (f2 x2) /\ R1 x2 x2 ==>
1507 R2 (f1 x1) (RES_ABSTRACT (respects R1) f2 x2)
1508Proof
1509 REPEAT STRIP_TAC
1510 THEN DEP_REWRITE_TAC[cj 1 RES_ABSTRACT_DEF]
1511 THEN REWRITE_TAC[IN_THM,RESPECTS]
1512 THEN ASM_REWRITE_TAC[]
1513QED
1514
1515Theorem EQUIV_RES_FORALL:
1516 !E (P:'a -> bool).
1517 EQUIV E ==>
1518 (RES_FORALL (respects E) P = ($! P))
1519Proof
1520 REWRITE_TAC[EQUIV_def]
1521 THEN REPEAT STRIP_TAC
1522 THEN CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1523 THEN CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1524 THEN asm_simp_tac bool_ss [RES_FORALL_THM, respects_def, W_THM, IN_THM]
1525QED
1526
1527Theorem EQUIV_RES_EXISTS:
1528 !E (P:'a -> bool).
1529 EQUIV E ==>
1530 (RES_EXISTS (respects E) P = ($? P))
1531Proof
1532 REWRITE_TAC[EQUIV_def]
1533 THEN REPEAT STRIP_TAC
1534 THEN CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1535 THEN CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1536 THEN asm_simp_tac bool_ss [RES_EXISTS_THM, respects_def, W_THM, IN_THM]
1537QED
1538
1539Theorem EQUIV_RES_EXISTS_UNIQUE:
1540 !E (P:'a -> bool).
1541 EQUIV E ==>
1542 (RES_EXISTS_UNIQUE (respects E) P = ($?! P))
1543Proof
1544 REWRITE_TAC[EQUIV_def]
1545 THEN REPEAT STRIP_TAC
1546 THEN CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1547 THEN CONV_TAC (RAND_CONV (RAND_CONV (REWR_CONV (GSYM ETA_AX))))
1548 THEN asm_simp_tac bool_ss [RES_EXISTS_UNIQUE_THM, RES_EXISTS_THM,
1549 RES_FORALL_THM, respects_def, W_THM, IN_THM,
1550 EXISTS_UNIQUE_THM]
1551QED
1552
1553Theorem FORALL_REGULAR:
1554 !P Q.
1555 (!x:'a. P x ==> Q x) ==>
1556 ($! P ==> $! Q)
1557Proof
1558 REPEAT GEN_TAC
1559 THEN STRIP_TAC
1560 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1561 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1562 THEN REPEAT STRIP_TAC
1563 THEN POP_ASSUM (ASSUME_TAC o SPEC_ALL)
1564 THEN RES_TAC
1565QED
1566
1567Theorem EXISTS_REGULAR:
1568 !P Q.
1569 (!x:'a. P x ==> Q x) ==>
1570 ($? P ==> $? Q)
1571Proof
1572 REPEAT GEN_TAC
1573 THEN STRIP_TAC
1574 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1575 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1576 THEN STRIP_TAC
1577 THEN RES_TAC
1578 THEN EXISTS_TAC (“x:'a”)
1579 THEN POP_ASSUM ACCEPT_TAC
1580QED
1581
1582Theorem RES_FORALL_REGULAR:
1583 !P Q R.
1584 (!x:'a. R x ==> P x ==> Q x) ==>
1585 (RES_FORALL R P ==> RES_FORALL R Q)
1586Proof
1587 REPEAT GEN_TAC
1588 THEN STRIP_TAC
1589 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1590 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1591 THEN asm_simp_tac bool_ss [RES_FORALL_THM, IN_THM]
1592QED
1593
1594Theorem RES_EXISTS_REGULAR:
1595 !P Q R.
1596 (!x:'a. R x ==> P x ==> Q x) ==>
1597 (RES_EXISTS R P ==> RES_EXISTS R Q)
1598Proof
1599 REPEAT GEN_TAC
1600 THEN STRIP_TAC
1601 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1602 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1603 THEN asm_simp_tac bool_ss [RES_EXISTS_THM, IN_THM]
1604 THEN PROVE_TAC[]
1605QED
1606
1607Theorem LEFT_RES_FORALL_REGULAR:
1608 !P R Q.
1609 (!x:'a. R x /\ (Q x ==> P x)) ==>
1610 (RES_FORALL R Q ==> $! P)
1611Proof
1612 simp_tac bool_ss [RES_FORALL_THM, IN_THM] >>
1613 rpt strip_tac >>
1614 CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])) >>
1615 asm_simp_tac bool_ss []
1616QED
1617
1618Theorem RIGHT_RES_FORALL_REGULAR:
1619 !P R Q. (!x:'a. R x ==> P x ==> Q x) ==>
1620 ($! P ==> RES_FORALL R Q)
1621Proof
1622 REPEAT GEN_TAC
1623 THEN STRIP_TAC
1624 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1625 THEN asm_simp_tac bool_ss [RES_FORALL_THM, IN_THM]
1626QED
1627
1628Theorem LEFT_RES_EXISTS_REGULAR:
1629 !P R Q.
1630 (!x:'a. R x ==> Q x ==> P x) ==>
1631 (RES_EXISTS R Q ==> $? P)
1632Proof
1633 REPEAT GEN_TAC
1634 THEN STRIP_TAC
1635 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1636 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1637 THEN asm_simp_tac bool_ss [RES_EXISTS_THM, IN_THM]
1638 THEN rpt strip_tac
1639 THEN rpt (first_x_assum $ irule_at Any)
1640QED
1641
1642Theorem RIGHT_RES_EXISTS_REGULAR:
1643 !P R Q.
1644 (!x:'a. R x /\ (P x ==> Q x)) ==>
1645 ($? P ==> RES_EXISTS R Q)
1646Proof
1647 REPEAT GEN_TAC
1648 THEN DISCH_THEN (STRIP_ASSUME_TAC o CONV_RULE FORALL_AND_CONV)
1649 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1650 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1651 THEN STRIP_TAC
1652 THEN asm_simp_tac bool_ss [RES_EXISTS_THM, IN_THM]
1653 THEN rpt (first_x_assum $ irule_at Any)
1654QED
1655
1656Theorem EXISTS_UNIQUE_REGULAR:
1657 !P E Q.
1658 (!x:'a. P x ==> respects E x /\ Q x) /\
1659 (!x y. respects E x /\ Q x /\ respects E y /\ Q y ==> E x y) ==>
1660 ($?! P ==> RES_EXISTS_EQUIV E Q)
1661Proof
1662 REPEAT GEN_TAC
1663 THEN STRIP_TAC
1664 THEN CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1665 THEN CONV_TAC (RAND_CONV (RAND_CONV (ONCE_REWRITE_CONV[GSYM ETA_AX])))
1666 THEN CONV_TAC (LAND_CONV EXISTS_UNIQUE_CONV)
1667 THEN REWRITE_TAC[RES_EXISTS_EQUIV]
1668 THEN asm_simp_tac bool_ss [RES_EXISTS_THM, RES_FORALL_THM, IN_THM]
1669 THEN PROVE_TAC[]
1670QED
1671
1672(*
1673val RES_EXISTS_UNIQUE_RESPECTS_REGULAR = store_thm
1674 ("RES_EXISTS_UNIQUE_RESPECTS_REGULAR",
1675 (“!R (P:'a -> bool).
1676 (RES_EXISTS_UNIQUE (respects R) P ==>
1677 RES_EXISTS_EQUIV (respects R) R P)”),
1678 REPEAT STRIP_TAC
1679 THEN IMP_RES_TAC RES_EXISTS_UNIQUE_EQUIV_REL
1680 THEN POP_ASSUM MATCH_MP_TAC
1681 THEN REWRITE_TAC[IN_THM,RESPECTS]
1682 );
1683*)
1684
1685Theorem RES_EXISTS_UNIQUE_RESPECTS_REGULAR:
1686 !R (P:'a -> bool).
1687 RES_EXISTS_UNIQUE (respects R) P ==>
1688 RES_EXISTS_EQUIV R P
1689Proof
1690 simp_tac bool_ss [RES_EXISTS_UNIQUE_THM, RES_EXISTS_EQUIV,
1691 RES_FORALL_THM, RES_EXISTS_THM, IN_RESPECTS] THEN
1692 PROVE_TAC[]
1693QED
1694
1695Theorem RES_EXISTS_UNIQUE_REGULAR:
1696 !P R Q.
1697 (!x:'a. P x ==> Q x) /\
1698 (!x y. respects R x /\ Q x /\ respects R y /\ Q y ==> R x y) ==>
1699 (RES_EXISTS_UNIQUE (respects R) P ==> RES_EXISTS_EQUIV R Q)
1700Proof
1701 simp_tac bool_ss [RES_EXISTS_UNIQUE_THM, RES_EXISTS_EQUIV, respects_def,
1702 W_THM, IN_THM,
1703 RES_FORALL_THM, RES_EXISTS_THM, IN_RESPECTS] THEN
1704 PROVE_TAC[]
1705QED
1706
1707Theorem RES_EXISTS_UNIQUE_REGULAR_SAME:
1708 !R (P:'a -> bool) Q.
1709 (R ===> $=) P Q ==>
1710 (RES_EXISTS_UNIQUE (respects R) P ==>
1711 RES_EXISTS_EQUIV R Q)
1712Proof
1713 simp_tac bool_ss [RES_EXISTS_UNIQUE_THM, RES_EXISTS_EQUIV, respects_def,
1714 W_THM, IN_THM, FUN_REL,
1715 RES_FORALL_THM, RES_EXISTS_THM, IN_RESPECTS] THEN
1716 PROVE_TAC[]
1717QED
1718
1719
1720
1721val _ = print_theory_to_file "-" "quotient.lst";
1722
1723val _ = html_theory "quotient";