1open HolKernel Parse boolLib;
2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->;
3infixr -->;
4
5
6(* --------------------------------------------------------------------- *)
7(* Lifting the lambda calculus syntax to the abstract level.             *)
8(* Version 2.1.                                                          *)
9(* Date: February 28, 2005                                               *)
10(* --------------------------------------------------------------------- *)
11
12
13val _ = new_theory "quotient_list";
14
15open prim_recTheory;
16open combinTheory;
17open listTheory;
18open rich_listTheory;
19open listLib;
20open bossLib;
21open res_quanTheory;
22open res_quanLib;
23open dep_rewrite;
24open quotientTheory;
25
26
27val REWRITE_THM = fn th => REWRITE_TAC[th];
28val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th];
29val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th])
30                               THEN REWRITE_TAC[th];
31
32val POP_TAC = POP_ASSUM (fn th => ALL_TAC);
33
34
35(* =================================================================== *)
36(* To form a ABS / REP function or a equivalence relation REL from     *)
37(* the corresponding functions/relations of the constituent subtypes   *)
38(* of the main type, use the following table of operators:             *)
39(*                                                                     *)
40(*      Type Operator     Constructor   Abstraction      Equivalence   *)
41(*                                                                     *)
42(*  Identity                  I x           I                $=        *)
43(*  Product  (ty1 # ty2)     (a,b)    (abs1 ## abs2)     (R1 ### R2)   *)
44(*  Sum      (ty1 + ty2)    (INL x)   (abs1 ++ abs2)     (R1 +++ R2)   *)
45(*  List      (ty list)    (CONS h t)    (MAP abs)       (LIST_REL R)  *)
46(*  Option    (ty option)  (SOME x)  (OPTION_MAP abs)   (OPTION_REL R) *)
47(*  Function (ty1 -> ty2)  (\x. f x)  (rep1 --> abs2)  (rep1 =-> abs2) *)
48(*  (Strong respect)                                     (R1 ===> R2)  *)
49(*                                                                     *)
50(* =================================================================== *)
51
52
53
54
55(* for LIST_REP or LIST_ABS, just use MAP! See Theorem MAP. *)
56
57val LIST_MAP_I =
58 store_thm
59  ("LIST_MAP_I",
60   (���MAP (I:'a -> 'a) = I���),
61   REWRITE_TAC[FUN_EQ_THM]
62   THEN Induct
63   THEN ASM_REWRITE_TAC[MAP,I_THM]
64  );
65
66(* for list equivalence relation, use prefix LIST_REL *)
67
68val LIST_REL_def = listTheory.LIST_REL_def
69
70val LIST_REL_EQ = store_thm
71   ("LIST_REL_EQ",
72    (���(LIST_REL ($= : 'a->'a->bool)) = $=���),
73    CONV_TAC FUN_EQ_CONV
74    THEN CONV_TAC (RAND_CONV (ABS_CONV FUN_EQ_CONV))
75    THEN Induct
76    THENL [ ALL_TAC, GEN_TAC ]
77    THEN Induct
78    THEN REWRITE_TAC[LIST_REL_def,NOT_CONS_NIL,NOT_NIL_CONS]
79    THEN GEN_TAC
80    THEN ASM_REWRITE_TAC[CONS_11]
81   );
82
83val LIST_REL_REFL = store_thm
84   ("LIST_REL_REFL",
85    (���!R. (!x y:'a. R x y = (R x = R y)) ==>
86            !x. LIST_REL R x x���),
87    GEN_TAC
88    THEN DISCH_TAC
89    THEN Induct
90    THEN REWRITE_TAC[LIST_REL_def]
91    THEN GEN_TAC
92    THEN ASM_REWRITE_TAC[]
93   );
94
95val LIST_EQUIV = store_thm
96   ("LIST_EQUIV",
97    (���!R:'a -> 'a -> bool. EQUIV R ==> EQUIV (LIST_REL R)���),
98    GEN_TAC
99    THEN REWRITE_TAC[EQUIV_def]
100    THEN DISCH_TAC
101    THEN Induct THENL [ALL_TAC, GEN_TAC]
102    THEN Induct
103    THEN REWRITE_TAC[LIST_REL_def]
104    THENL
105      [ PROVE_TAC[LIST_REL_def],
106
107        PROVE_TAC[LIST_REL_def],
108
109        GEN_TAC
110        THEN CONV_TAC (RAND_CONV FUN_EQ_CONV)
111        THEN EQ_TAC
112        THENL
113          [ STRIP_TAC
114            THEN Cases
115            THEN REWRITE_TAC[LIST_REL_def]
116            THEN PROVE_TAC[],
117
118            DISCH_THEN (MP_TAC o GEN ``c:'a`` o GEN ``cs:'a list``
119                               o SPEC ``(c:'a)::cs``)
120            THEN REWRITE_TAC[LIST_REL_def]
121            THEN IMP_RES_TAC LIST_REL_REFL
122            THEN PROVE_TAC[]
123          ]
124      ]
125   );
126
127Theorem LIST_REL_REL:
128  !R (abs:'a -> 'b) rep.
129         QUOTIENT R abs rep ==>
130         !r s. LIST_REL R r s <=> LIST_REL R r r /\ LIST_REL R s s /\
131                                  (MAP abs r = MAP abs s)
132Proof
133    REPEAT GEN_TAC
134    THEN STRIP_TAC
135    THEN Induct
136    THENL [ ALL_TAC, GEN_TAC ]
137    THEN Cases
138    THEN ONCE_REWRITE_TAC[LIST_REL_def]
139    THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS]
140    THEN REWRITE_TAC[CONS_11]
141    THEN IMP_RES_THEN
142               (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th))))
143               QUOTIENT_REL
144    THEN POP_ASSUM
145               (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th))))
146    THEN PROVE_TAC[]
147QED
148
149val LIST_QUOTIENT = store_thm
150   ("LIST_QUOTIENT",
151    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
152         QUOTIENT (LIST_REL R) (MAP abs) (MAP rep)���),
153    REPEAT STRIP_TAC
154    THEN REWRITE_TAC[QUOTIENT_def]
155    THEN REPEAT CONJ_TAC
156    THENL (* 3 subgoals *)
157      [ IMP_RES_TAC QUOTIENT_ABS_REP
158        THEN Induct
159        THEN ASM_REWRITE_TAC[MAP],
160
161        IMP_RES_TAC QUOTIENT_REP_REFL
162        THEN Induct
163        THEN ASM_REWRITE_TAC[MAP,LIST_REL_def],
164
165        Induct
166        THENL [ ALL_TAC, GEN_TAC ]
167        THEN Cases
168        THEN ONCE_REWRITE_TAC[LIST_REL_def]
169        THEN REWRITE_TAC[MAP,NOT_CONS_NIL,NOT_NIL_CONS]
170        THEN REWRITE_TAC[CONS_11]
171        THEN IMP_RES_THEN
172               (fn th => CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV th))))
173               QUOTIENT_REL
174        THEN IMP_RES_THEN
175               (fn th => CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV th))))
176               LIST_REL_REL
177        THEN PROVE_TAC[]
178      ]
179   );
180
181
182
183
184(* Here are some definitional and well-formedness theorems
185   for some standard polymorphic operators.
186*)
187
188
189
190(* list theory: CONS, NIL, MAP, LENGTH, APPEND, FLAT, REVERSE, FILTER,
191                NULL, EVERY (ALL_EL), EXISTS (SOME_EL), FOLDL, FOLDR *)
192
193val CONS_PRS = store_thm
194   ("CONS_PRS",
195    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
196         !t h. CONS h t = (MAP abs) (CONS (rep h) (MAP rep t))���),
197    REPEAT GEN_TAC
198    THEN DISCH_TAC
199    THEN Induct
200    THEN ASM_REWRITE_TAC[MAP]
201    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
202   );
203
204val CONS_RSP = store_thm
205   ("CONS_RSP",
206    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
207         !t1 t2 h1 h2.
208          R h1 h2 /\ (LIST_REL R) t1 t2 ==>
209          (LIST_REL R) (CONS h1 t1) (CONS h2 t2)���),
210    REPEAT GEN_TAC
211    THEN DISCH_TAC
212    THEN Cases
213    THEN Cases
214    THEN REPEAT GEN_TAC
215    THEN REWRITE_TAC[LIST_REL_def]
216   );
217
218
219val NIL_PRS = store_thm
220   ("NIL_PRS",
221    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
222         ([] = (MAP abs) [])���),
223    REPEAT STRIP_TAC
224    THEN REWRITE_TAC[MAP]
225   );
226
227val NIL_RSP = store_thm
228   ("NIL_RSP",
229    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
230         (LIST_REL R) [] []���),
231    REPEAT STRIP_TAC
232    THEN REWRITE_TAC[LIST_REL_def]
233   );
234
235
236val MAP_PRS = store_thm
237   ("MAP_PRS",
238    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
239        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
240         !l f. MAP f l = (MAP abs2) (MAP ((abs1 --> rep2) f) (MAP rep1 l))���),
241    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
242    THEN Induct
243    THEN ASM_REWRITE_TAC[MAP]
244    THEN REPEAT GEN_TAC
245    THEN REWRITE_TAC[CONS_11]
246    THEN ASM_REWRITE_TAC[FUN_MAP_THM]
247    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
248   );
249
250val MAP_RSP = store_thm
251   ("MAP_RSP",
252    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
253        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
254         !l1 l2 f1 f2.
255          (R1 ===> R2) f1 f2 /\ (LIST_REL R1) l1 l2 ==>
256          (LIST_REL R2) (MAP f1 l1) (MAP f2 l2)���),
257    REPEAT GEN_TAC
258    THEN DISCH_TAC
259    THEN REPEAT GEN_TAC
260    THEN DISCH_TAC
261    THEN Induct
262    THENL [ ALL_TAC, GEN_TAC ]
263    THEN Induct
264    THEN REPEAT GEN_TAC
265    THEN REWRITE_TAC[MAP,LIST_REL_def]
266    THEN STRIP_TAC
267    THEN CONJ_TAC
268    THENL
269      [ IMP_RES_TAC FUN_REL_MP,
270
271        FIRST_ASSUM MATCH_MP_TAC
272        THEN ASM_REWRITE_TAC[]
273      ]
274   );
275
276val LENGTH_PRS = store_thm
277   ("LENGTH_PRS",
278    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
279         !l. LENGTH l = LENGTH (MAP rep l)���),
280    REPEAT GEN_TAC
281    THEN DISCH_TAC
282    THEN Induct
283    THEN ASM_REWRITE_TAC[LENGTH,MAP]
284   );
285
286val LENGTH_RSP = store_thm
287   ("LENGTH_RSP",
288    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
289         !l1 l2.
290          (LIST_REL R) l1 l2 ==>
291          (LENGTH l1 = LENGTH l2)���),
292    REPEAT GEN_TAC
293    THEN DISCH_TAC
294    THEN Induct
295    THENL [ ALL_TAC, GEN_TAC ]
296    THEN Induct
297    THEN REPEAT GEN_TAC
298    THEN REWRITE_TAC[LENGTH,LIST_REL_def]
299    THEN STRIP_TAC
300    THEN REWRITE_TAC[INV_SUC_EQ]
301    THEN FIRST_ASSUM MATCH_MP_TAC
302    THEN FIRST_ASSUM ACCEPT_TAC
303   );
304
305val APPEND_PRS = store_thm
306   ("APPEND_PRS",
307    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
308         !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))���),
309    REPEAT GEN_TAC
310    THEN DISCH_TAC
311    THEN Induct
312    THENL [ ALL_TAC, GEN_TAC ]
313    THEN Induct
314    THEN ASM_REWRITE_TAC[APPEND,MAP]
315    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
316    THEN GEN_TAC
317    THEN POP_ASSUM MP_TAC
318    THEN REWRITE_TAC[APPEND,MAP]
319    THEN DISCH_THEN (REWRITE_THM o SYM)
320   );
321
322val APPEND_RSP = store_thm
323   ("APPEND_RSP",
324    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
325         !l1 l2 m1 m2.
326          (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==>
327          (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)���),
328    REPEAT GEN_TAC
329    THEN DISCH_TAC
330    THEN Induct
331    THENL [ ALL_TAC, GEN_TAC ]
332    THEN Induct
333    THEN REPEAT GEN_TAC
334    THEN REWRITE_TAC[APPEND,LIST_REL_def]
335    THEN STRIP_TAC
336    THEN ASM_REWRITE_TAC[]
337    THEN FIRST_ASSUM MATCH_MP_TAC
338    THEN CONJ_TAC
339    THEN FIRST_ASSUM ACCEPT_TAC
340   );
341
342val FLAT_PRS = store_thm
343   ("FLAT_PRS",
344    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
345         !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))���),
346    REPEAT GEN_TAC
347    THEN DISCH_TAC
348    THEN Induct
349    THEN ASM_REWRITE_TAC[FLAT,MAP]
350    THEN Induct
351    THEN REWRITE_TAC[MAP,APPEND]
352    THEN ASM_REWRITE_TAC[MAP_APPEND]
353    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
354   );
355
356val FLAT_RSP = store_thm
357   ("FLAT_RSP",
358    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
359         !l1 l2.
360          LIST_REL (LIST_REL R) l1 l2 ==>
361          (LIST_REL R) (FLAT l1) (FLAT l2)���),
362    REPEAT GEN_TAC
363    THEN DISCH_TAC
364    THEN Induct
365    THENL [ ALL_TAC, GEN_TAC ]
366    THEN Induct
367    THEN REPEAT GEN_TAC
368    THEN REWRITE_TAC[FLAT,LIST_REL_def]
369    THEN STRIP_TAC
370    THEN DEP_REWRITE_TAC[APPEND_RSP]
371    THEN EXISTS_TAC (���abs:'a -> 'b���)
372    THEN EXISTS_TAC (���rep:'b -> 'a���)
373    THEN ASM_REWRITE_TAC[]
374    THEN FIRST_ASSUM MATCH_MP_TAC
375    THEN FIRST_ASSUM ACCEPT_TAC
376   );
377
378val REVERSE_PRS = store_thm
379   ("REVERSE_PRS",
380    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
381         !l. REVERSE l = MAP abs (REVERSE (MAP rep l))���),
382    REPEAT GEN_TAC
383    THEN DISCH_TAC
384    THEN Induct
385    THEN ASM_REWRITE_TAC[REVERSE_DEF,MAP]
386    THEN GEN_TAC
387    THEN ASM_REWRITE_TAC[MAP_APPEND,MAP]
388    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
389   );
390
391val REVERSE_RSP = store_thm
392   ("REVERSE_RSP",
393    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
394         !l1 l2.
395          LIST_REL R l1 l2 ==>
396          (LIST_REL R) (REVERSE l1) (REVERSE l2)���),
397    REPEAT GEN_TAC
398    THEN DISCH_TAC
399    THEN Induct
400    THENL [ ALL_TAC, GEN_TAC ]
401    THEN Induct
402    THEN REPEAT GEN_TAC
403    THEN REWRITE_TAC[REVERSE_DEF,LIST_REL_def]
404    THEN STRIP_TAC
405    THEN DEP_REWRITE_TAC[APPEND_RSP]
406    THEN EXISTS_TAC (���abs:'a -> 'b���)
407    THEN EXISTS_TAC (���rep:'b -> 'a���)
408    THEN ASM_REWRITE_TAC[LIST_REL_def]
409    THEN FIRST_ASSUM MATCH_MP_TAC
410    THEN FIRST_ASSUM ACCEPT_TAC
411   );
412
413val FILTER_PRS = store_thm
414   ("FILTER_PRS",
415    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
416         !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l))
417       ���),
418    REPEAT GEN_TAC
419    THEN DISCH_TAC
420    THEN GEN_TAC
421    THEN Induct
422    THEN ASM_REWRITE_TAC[FILTER,MAP]
423    THEN GEN_TAC
424    THEN IMP_RES_TAC QUOTIENT_ABS_REP
425    THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM]
426    THEN COND_CASES_TAC
427    THEN ASM_REWRITE_TAC[MAP]
428   );
429
430val FILTER_RSP = store_thm
431   ("FILTER_RSP",
432    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
433         !P1 P2 l1 l2.
434          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
435          (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)���),
436    REPEAT GEN_TAC
437    THEN DISCH_TAC
438    THEN GEN_TAC THEN GEN_TAC
439    THEN Induct
440    THENL [ ALL_TAC, GEN_TAC ]
441    THEN Induct
442    THEN REPEAT GEN_TAC
443    THEN REWRITE_TAC[FILTER,LIST_REL_def]
444    THEN REWRITE_TAC[FUN_REL]
445    THEN STRIP_TAC
446    THEN REPEAT COND_CASES_TAC
447    THEN REWRITE_TAC[LIST_REL_def]
448    THEN REPEAT CONJ_TAC
449    THENL (* 5 subgoals *)
450      [ FIRST_ASSUM ACCEPT_TAC,
451
452        FIRST_ASSUM MATCH_MP_TAC
453        THEN ASM_REWRITE_TAC[FUN_REL],
454
455        RES_TAC
456        THEN RES_TAC,
457
458        RES_TAC
459        THEN RES_TAC,
460
461        FIRST_ASSUM MATCH_MP_TAC
462        THEN ASM_REWRITE_TAC[FUN_REL]
463      ]
464   );
465
466val NULL_PRS = store_thm
467   ("NULL_PRS",
468    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
469         !l. NULL l = NULL (MAP rep l)���),
470    REPEAT GEN_TAC
471    THEN DISCH_TAC
472    THEN Cases
473    THEN REWRITE_TAC[NULL,MAP]
474   );
475
476val NULL_RSP = store_thm
477   ("NULL_RSP",
478    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
479         !l1 l2.
480          LIST_REL R l1 l2 ==>
481          (NULL l1 = NULL l2)���),
482    REPEAT GEN_TAC
483    THEN DISCH_TAC
484    THEN Induct
485    THENL [ ALL_TAC, GEN_TAC ]
486    THEN Induct
487    THEN REPEAT GEN_TAC
488    THEN REWRITE_TAC[NULL,LIST_REL_def]
489   );
490
491val ALL_EL_PRS = store_thm
492   ("ALL_EL_PRS",
493    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
494         !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)���),
495    REPEAT GEN_TAC
496    THEN DISCH_TAC
497    THEN Induct
498    THEN ASM_REWRITE_TAC[ALL_EL,MAP]
499    THEN REPEAT GEN_TAC
500    THEN IMP_RES_TAC QUOTIENT_ABS_REP
501    THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM]
502   );
503
504val ALL_EL_RSP = store_thm
505   ("ALL_EL_RSP",
506    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
507         !l1 l2 P1 P2.
508          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
509          (ALL_EL P1 l1 = ALL_EL P2 l2)���),
510    REPEAT GEN_TAC
511    THEN DISCH_TAC
512    THEN Induct
513    THENL [ ALL_TAC, GEN_TAC ]
514    THEN Induct
515    THEN REPEAT GEN_TAC
516    THEN REWRITE_TAC[ALL_EL,LIST_REL_def]
517    THEN REWRITE_TAC[FUN_REL]
518    THEN STRIP_TAC
519    THEN MK_COMB_TAC
520    THENL
521      [ AP_TERM_TAC
522        THEN FIRST_ASSUM MATCH_MP_TAC
523        THEN FIRST_ASSUM ACCEPT_TAC,
524
525        FIRST_ASSUM MATCH_MP_TAC
526        THEN ASM_REWRITE_TAC[FUN_REL]
527      ]
528   );
529
530val SOME_EL_PRS = store_thm
531   ("SOME_EL_PRS",
532    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
533         !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)���),
534    REPEAT GEN_TAC
535    THEN DISCH_TAC
536    THEN Induct
537    THEN ASM_REWRITE_TAC[SOME_EL,MAP]
538    THEN REPEAT GEN_TAC
539    THEN IMP_RES_TAC QUOTIENT_ABS_REP
540    THEN ASM_REWRITE_TAC[FUN_MAP_THM,I_THM]
541   );
542
543val SOME_EL_RSP = store_thm
544   ("SOME_EL_RSP",
545    (���!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
546         !l1 l2 P1 P2.
547          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
548          (SOME_EL P1 l1 = SOME_EL P2 l2)���),
549    REPEAT GEN_TAC
550    THEN DISCH_TAC
551    THEN Induct
552    THENL [ ALL_TAC, GEN_TAC ]
553    THEN Induct
554    THEN REPEAT GEN_TAC
555    THEN REWRITE_TAC[SOME_EL,LIST_REL_def]
556    THEN REWRITE_TAC[FUN_REL]
557    THEN STRIP_TAC
558    THEN MK_COMB_TAC
559    THENL
560      [ AP_TERM_TAC
561        THEN FIRST_ASSUM MATCH_MP_TAC
562        THEN FIRST_ASSUM ACCEPT_TAC,
563
564        FIRST_ASSUM MATCH_MP_TAC
565        THEN ASM_REWRITE_TAC[FUN_REL]
566      ]
567   );
568
569
570val FOLDL_PRS = store_thm
571   ("FOLDL_PRS",
572    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
573        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
574         !l f e. FOLDL f e l =
575                 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f)
576                      (rep1 e)
577                      (MAP rep2 l))���),
578    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
579    THEN IMP_RES_TAC QUOTIENT_ABS_REP
580    THEN Induct
581    THEN ASM_REWRITE_TAC[FOLDL,MAP,FUN_MAP_THM]
582   );
583
584val FOLDL_RSP = store_thm
585   ("FOLDL_RSP",
586    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
587        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
588         !l1 l2 f1 f2 e1 e2.
589          (R1 ===> R2 ===> R1) f1 f2 /\
590             R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==>
591          R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)���),
592    REPEAT GEN_TAC THEN DISCH_TAC
593    THEN REPEAT GEN_TAC THEN DISCH_TAC
594    THEN Induct
595    THENL [ ALL_TAC, GEN_TAC ]
596    THEN Induct
597    THEN REPEAT GEN_TAC
598    THEN REWRITE_TAC[FOLDL,LIST_REL_def]
599    THEN REWRITE_TAC[FUN_REL]
600    THEN STRIP_TAC
601    THEN FIRST_ASSUM MATCH_MP_TAC
602    THEN REWRITE_TAC[FUN_REL]
603    THEN REPEAT CONJ_TAC (* 3 subgoals *)
604    THEN TRY (FIRST_ASSUM ACCEPT_TAC)
605    THEN DEP_ONCE_ASM_REWRITE_TAC[]
606    THEN CONJ_TAC
607    THEN FIRST_ASSUM ACCEPT_TAC
608   );
609
610
611val FOLDR_PRS = store_thm
612   ("FOLDR_PRS",
613    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
614        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
615         !l f e. FOLDR f e l =
616                 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f)
617                      (rep2 e)
618                      (MAP rep1 l))���),
619    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
620    THEN IMP_RES_TAC QUOTIENT_ABS_REP
621    THEN Induct
622    THEN ASM_REWRITE_TAC[FOLDR,MAP,FUN_MAP_THM]
623   );
624
625val FOLDR_RSP = store_thm
626   ("FOLDR_RSP",
627    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
628        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
629         !l1 l2 f1 f2 e1 e2.
630          (R1 ===> R2 ===> R2) f1 f2 /\
631             R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==>
632          R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)���),
633    REPEAT GEN_TAC THEN DISCH_TAC
634    THEN REPEAT GEN_TAC THEN DISCH_TAC
635    THEN Induct
636    THENL [ ALL_TAC, GEN_TAC ]
637    THEN Induct
638    THEN REPEAT GEN_TAC
639    THEN REWRITE_TAC[FOLDR,LIST_REL_def]
640    THEN REWRITE_TAC[FUN_REL]
641    THEN STRIP_TAC
642    THEN DEP_ONCE_ASM_REWRITE_TAC[]
643    THEN CONJ_TAC
644    THEN TRY (FIRST_ASSUM ACCEPT_TAC)
645    THEN FIRST_ASSUM MATCH_MP_TAC
646    THEN REWRITE_TAC[FUN_REL]
647    THEN REPEAT CONJ_TAC
648    THEN FIRST_ASSUM ACCEPT_TAC
649   );
650
651
652
653
654val _ = export_theory();
655
656val _ = print_theory_to_file "-" "quotient_list.lst";
657
658val _ = html_theory "quotient_list";
659