1open HolKernel Parse boolLib;
2
3(* --------------------------------------------------------------------- *)
4(* Lifting the lambda calculus syntax to the abstract level.             *)
5(* Version 2.1.                                                          *)
6(* Date: February 28, 2005                                               *)
7(* --------------------------------------------------------------------- *)
8
9
10val _ = new_theory "quotient_pair";
11
12open prim_recTheory;
13open combinTheory;
14open pairTheory;
15open pairLib;
16open bossLib;
17open res_quanTheory;
18open res_quanLib;
19open dep_rewrite;
20open quotientTheory;
21
22
23val REWRITE_THM = fn th => REWRITE_TAC[th];
24val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th];
25val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th])
26                               THEN REWRITE_TAC[th];
27
28val POP_TAC = POP_ASSUM (fn th => ALL_TAC);
29
30
31(* =================================================================== *)
32(* To form a ABS / REP function or a equivalence relation REL from     *)
33(* the corresponding functions/relations of the constituent subtypes   *)
34(* of the main type, use the following table of operators:             *)
35(*                                                                     *)
36(*      Type Operator     Constructor   Abstraction      Equivalence   *)
37(*                                                                     *)
38(*  Identity                  I x           I                $=        *)
39(*  Product  (ty1 # ty2)     (a,b)    (abs1 ## abs2)     (R1 ### R2)   *)
40(*  Sum      (ty1 + ty2)    (INL x)   (abs1 ++ abs2)     (R1 +++ R2)   *)
41(*  List      (ty list)    (CONS h t)    (MAP abs)       (LIST_REL R)  *)
42(*  Option    (ty option)  (SOME x)  (OPTION_MAP abs)   (OPTION_REL R) *)
43(*  Function (ty1 -> ty2)  (\x. f x)  (rep1 --> abs2)  (rep1 =-> abs2) *)
44(*  (Strong respect)                                     (R1 ===> R2)  *)
45(*                                                                     *)
46(* =================================================================== *)
47
48
49
50
51(* to create PROD (i.e., PAIR) ABS and REP functions, use infix ## *)
52(*  See PAIR_MAP_THM, PAIR_MAP. *)
53
54val PAIR_MAP_I = store_thm
55   ("PAIR_MAP_I",
56    (���(I ## I) = (I : 'a # 'b -> 'a # 'b)���),
57    CONV_TAC FUN_EQ_CONV
58    THEN Cases
59    THEN REWRITE_TAC[PAIR_MAP_THM,I_THM]
60   );
61
62(* just like RPROD_DEF, except infix: *)
63
64val PAIR_REL =
65    new_infixr_definition
66    ("PAIR_REL",
67     (���$### R1 R2 = \(a:'a,b:'b) (c:'c,d:'d). R1 a c /\ R2 b d���),
68     490);
69
70Theorem PAIR_REL_THM:
71   !R1 R2 (a:'a) (b:'b) (c:'c) (d:'d).
72         (R1 ### R2) (a,b) (c,d) <=> R1 a c /\ R2 b d
73Proof
74    REPEAT GEN_TAC
75    THEN PURE_ONCE_REWRITE_TAC[PAIR_REL]
76    THEN GEN_BETA_TAC
77    THEN REFL_TAC
78QED
79
80val PAIR_REL_EQ = store_thm
81   ("PAIR_REL_EQ",
82    (���($= ### $=) = ($= : 'a # 'b -> 'a # 'b -> bool)���),
83    CONV_TAC FUN_EQ_CONV
84    THEN Cases
85    THEN CONV_TAC FUN_EQ_CONV
86    THEN Cases
87    THEN REWRITE_TAC[PAIR_REL_THM,PAIR_EQ]
88   );
89
90val PAIR_REL_REFL = store_thm
91   ("PAIR_REL_REFL",
92    (���!R1 R2. (!x y:'a. R1 x y = (R1 x = R1 y)) /\
93                (!x y:'b. R2 x y = (R2 x = R2 y)) ==>
94                !x. (R1 ### R2) x x���),
95    REPEAT GEN_TAC
96    THEN STRIP_TAC
97    THEN Cases
98    THEN REWRITE_TAC[PAIR_REL_THM]
99    THEN ASM_REWRITE_TAC[]
100   );
101
102val PAIR_EQUIV = store_thm
103   ("PAIR_EQUIV",
104    (���!(R1:'a -> 'a -> bool) (R2:'b -> 'b -> bool).
105            EQUIV R1 ==> EQUIV R2 ==> EQUIV (R1 ### R2)���),
106    REPEAT GEN_TAC
107    THEN REWRITE_TAC[EQUIV_def]
108    THEN REPEAT DISCH_TAC
109    THEN Cases
110    THEN Cases
111    THEN REWRITE_TAC[PAIR_REL_THM]
112    THEN CONV_TAC (RAND_CONV FUN_EQ_CONV)
113    THEN EQ_TAC
114    THENL
115      [ STRIP_TAC
116        THEN Cases
117        THEN REWRITE_TAC[PAIR_REL_THM]
118        THEN PROVE_TAC[],
119
120        DISCH_THEN (MP_TAC o GEN ``a:'a`` o GEN ``b:'b``
121                               o SPEC ``(a:'a, b:'b)``)
122        THEN REWRITE_TAC[PAIR_REL_THM]
123        THEN IMP_RES_TAC PAIR_REL_REFL
124        THEN PROVE_TAC[]
125      ]
126   );
127
128val PAIR_QUOTIENT = store_thm
129   ("PAIR_QUOTIENT",
130    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
131        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
132         QUOTIENT (R1 ### R2) (abs1 ## abs2) (rep1 ## rep2)���),
133    REPEAT STRIP_TAC
134    THEN REWRITE_TAC[QUOTIENT_def]
135    THEN REPEAT CONJ_TAC
136    THENL
137      [ Cases
138        THEN REWRITE_TAC[PAIR_MAP_THM]
139        THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP,
140
141        Cases
142        THEN REWRITE_TAC[PAIR_MAP_THM,PAIR_REL_THM,PAIR_EQ]
143        THEN IMP_RES_THEN REWRITE_THM QUOTIENT_REP_REFL,
144
145        REPEAT Cases
146        THEN REWRITE_TAC[PAIR_REL_THM,PAIR_MAP_THM,PAIR_EQ]
147        THEN IMP_RES_THEN
148                 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th])))
149                 QUOTIENT_REL
150        THEN PROVE_TAC[]
151      ]
152   );
153
154
155
156(* Here are some definitional and well-formedness theorems
157   for some standard polymorphic operators.
158*)
159
160
161
162(* pair theory: FST, SND, COMMA, CURRY, UNCURRY, ## *)
163
164val FST_PRS = store_thm
165   ("FST_PRS",
166    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
167        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
168         !p. FST p = abs1 (FST ((rep1 ## rep2) p))���),
169    REPEAT GEN_TAC
170    THEN DISCH_TAC
171    THEN REPEAT GEN_TAC
172    THEN DISCH_TAC
173    THEN Cases
174    THEN PURE_REWRITE_TAC[PAIR_MAP_THM,FST]
175    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
176   );
177
178val FST_RSP = store_thm
179   ("FST_RSP",
180    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
181        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
182         !p1 p2.
183          (R1 ### R2) p1 p2 ==> R1 (FST p1) (FST p2)���),
184    REPEAT GEN_TAC
185    THEN DISCH_TAC
186    THEN REPEAT GEN_TAC
187    THEN DISCH_TAC
188    THEN Cases
189    THEN Cases
190    THEN REWRITE_TAC[PAIR_REL_THM,FST]
191    THEN STRIP_TAC
192   );
193
194
195val SND_PRS = store_thm
196   ("SND_PRS",
197    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
198        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
199         !p. SND p = abs2 (SND ((rep1 ## rep2) p))���),
200    REPEAT GEN_TAC
201    THEN DISCH_TAC
202    THEN REPEAT GEN_TAC
203    THEN DISCH_TAC
204    THEN Cases
205    THEN PURE_REWRITE_TAC[PAIR_MAP_THM,SND]
206    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
207   );
208
209val SND_RSP = store_thm
210   ("SND_RSP",
211    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
212        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
213         !p1 p2.
214          (R1 ### R2) p1 p2 ==> R2 (SND p1) (SND p2)���),
215    REPEAT GEN_TAC
216    THEN DISCH_TAC
217    THEN REPEAT GEN_TAC
218    THEN DISCH_TAC
219    THEN Cases
220    THEN Cases
221    THEN REWRITE_TAC[PAIR_REL_THM,SND]
222    THEN STRIP_TAC
223   );
224
225
226val COMMA_PRS = store_thm
227   ("COMMA_PRS",
228    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
229        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
230         !a b. (a,b) = (abs1 ## abs2) (rep1 a, rep2 b)���),
231    REPEAT STRIP_TAC
232    THEN PURE_REWRITE_TAC[PAIR_MAP_THM]
233    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
234   );
235
236val COMMA_RSP = store_thm
237   ("COMMA_RSP",
238    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
239        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
240         !a1 a2 b1 b2.
241          R1 a1 b1 /\ R2 a2 b2 ==>
242          (R1 ### R2) (a1,a2) (b1,b2)���),
243    REPEAT GEN_TAC
244    THEN DISCH_TAC
245    THEN REPEAT GEN_TAC
246    THEN DISCH_TAC
247    THEN REPEAT GEN_TAC
248    THEN REWRITE_TAC[PAIR_REL_THM]
249   );
250
251
252val CURRY_PRS = store_thm
253   ("CURRY_PRS",
254    (���!R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
255        !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
256        !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
257         !f a b. CURRY f a b =
258                 abs3 (CURRY (((abs1 ## abs2) --> rep3) f)
259                             (rep1 a) (rep2 b))���),
260    REPEAT GEN_TAC
261    THEN DISCH_TAC
262    THEN REPEAT GEN_TAC
263    THEN DISCH_TAC
264    THEN REPEAT GEN_TAC
265    THEN DISCH_TAC
266    THEN REPEAT GEN_TAC
267    THEN PURE_ONCE_REWRITE_TAC[CURRY_DEF]
268    THEN PURE_REWRITE_TAC[FUN_MAP_THM]
269    THEN PURE_ONCE_REWRITE_TAC[PAIR_MAP_THM]
270    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
271   );
272
273val CURRY_RSP = store_thm
274   ("CURRY_RSP",
275    (���!R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
276        !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
277        !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
278         !f1 f2.
279          ((R1 ### R2) ===> R3) f1 f2 ==>
280          (R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)���),
281    REPEAT GEN_TAC
282    THEN DISCH_TAC
283    THEN REPEAT GEN_TAC
284    THEN DISCH_TAC
285    THEN REPEAT GEN_TAC
286    THEN DISCH_TAC
287    THEN REPEAT GEN_TAC
288    THEN REWRITE_TAC[FUN_REL]
289    THEN REPEAT STRIP_TAC
290    THEN PURE_REWRITE_TAC[CURRY_DEF]
291    THEN FIRST_ASSUM MATCH_MP_TAC
292    THEN PURE_REWRITE_TAC[PAIR_REL_THM]
293    THEN CONJ_TAC
294    THEN FIRST_ASSUM ACCEPT_TAC
295   );
296
297
298val UNCURRY_PRS = store_thm
299   ("UNCURRY_PRS",
300    (���!R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
301        !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
302        !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
303         !f p. UNCURRY f p =
304               abs3 (UNCURRY ((abs1 --> abs2 --> rep3) f)
305                             ((rep1 ## rep2) p))���),
306    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
307    THEN GEN_TAC
308    THEN Cases
309    THEN PURE_ONCE_REWRITE_TAC[PAIR_MAP_THM]
310    THEN PURE_ONCE_REWRITE_TAC[UNCURRY_DEF]
311    THEN PURE_REWRITE_TAC[FUN_MAP_THM]
312    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
313   );
314
315val UNCURRY_RSP = store_thm
316   ("UNCURRY_RSP",
317    (���!R1 (abs1:'a -> 'd) rep1. QUOTIENT R1 abs1 rep1 ==>
318        !R2 (abs2:'b -> 'e) rep2. QUOTIENT R2 abs2 rep2 ==>
319        !R3 (abs3:'c -> 'f) rep3. QUOTIENT R3 abs3 rep3 ==>
320         !f1 f2.
321          (R1 ===> R2 ===> R3) f1 f2 ==>
322          ((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)���),
323    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
324    THEN POP_ASSUM MP_TAC
325    THEN REWRITE_TAC[FUN_REL]
326    THEN DISCH_TAC
327    THEN Cases
328    THEN Cases
329    THEN REWRITE_TAC[PAIR_REL_THM,UNCURRY_DEF]
330    THEN STRIP_TAC
331    THEN RES_TAC
332   );
333
334
335val PAIR_MAP_PRS = store_thm
336   ("PAIR_MAP_PRS",
337    (���!R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
338        !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
339        !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
340        !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
341         !f g. (f ## g) =
342               ((rep1 ## rep3) --> (abs2 ## abs4))
343                   (((abs1 --> rep2) f) ## ((abs3 --> rep4) g))���),
344    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
345    THEN REPEAT GEN_TAC
346    THEN CONV_TAC FUN_EQ_CONV
347    THEN Cases
348    THEN PURE_REWRITE_TAC[FUN_MAP_THM,PAIR_MAP_THM]
349    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
350   );
351
352val PAIR_MAP_RSP = store_thm
353   ("PAIR_MAP_RSP",
354    (���!R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
355        !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
356        !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
357        !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
358         !f1 f2 g1 g2.
359          (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
360          ((R1 ### R3) ===> (R2 ### R4)) (f1 ## g1) (f2 ## g2)���),
361    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
362    THEN POP_ASSUM MP_TAC
363    THEN REWRITE_TAC[FUN_REL]
364    THEN STRIP_TAC
365    THEN Cases
366    THEN Cases
367    THEN PURE_REWRITE_TAC[PAIR_REL_THM,PAIR_MAP_THM]
368    THEN STRIP_TAC
369    THEN CONJ_TAC
370    THEN FIRST_ASSUM MATCH_MP_TAC
371    THEN FIRST_ASSUM ACCEPT_TAC
372   );
373
374
375
376
377val _ = export_theory();
378
379val _ = print_theory_to_file "-" "quotient_pair.lst";
380
381val _ = html_theory "quotient_pair";
382