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_sum";
11
12open prim_recTheory;
13open combinTheory;
14open sumTheory;
15open bossLib;
16open res_quanTheory;
17open res_quanLib;
18open dep_rewrite;
19open quotientTheory;
20
21
22val REWRITE_THM = fn th => REWRITE_TAC[th];
23val ONCE_REWRITE_THM = fn th => ONCE_REWRITE_TAC[th];
24val REWRITE_ALL_THM = fn th => RULE_ASSUM_TAC (REWRITE_RULE[th])
25                               THEN REWRITE_TAC[th];
26
27val POP_TAC = POP_ASSUM (fn th => ALL_TAC);
28val _ = temp_set_mapped_fixity { term_name = "SUM_MAP", tok = "++",
29                                 fixity = Infixl 480}
30
31
32(* =================================================================== *)
33(* To form a ABS / REP function or a equivalence relation REL from     *)
34(* the corresponding functions/relations of the constituent subtypes   *)
35(* of the main type, use the following table of operators:             *)
36(*                                                                     *)
37(*      Type Operator     Constructor   Abstraction      Equivalence   *)
38(*                                                                     *)
39(*  Identity                  I x           I                $=        *)
40(*  Product  (ty1 # ty2)     (a,b)    (abs1 ## abs2)     (R1 ### R2)   *)
41(*  Sum      (ty1 + ty2)    (INL x)   (abs1 ++ abs2)     (R1 +++ R2)   *)
42(*  List      (ty list)    (CONS h t)    (MAP abs)       (LIST_REL R)  *)
43(*  Option    (ty option)  (SOME x)  (OPTION_MAP abs)   (OPTION_REL R) *)
44(*  Function (ty1 -> ty2)  (\x. f x)  (rep1 --> abs2)  (rep1 =-> abs2) *)
45(*  (Strong respect)                                     (R1 ===> R2)  *)
46(*                                                                     *)
47(* =================================================================== *)
48
49
50
51(* for SUM of ABS / REP functions, use infix ++, defined in
52   src/sum/sumScript.sml. *)
53
54(* for SUM of equivalence relations, use infix +++, defined here: *)
55
56val _ = Lib.try add_infix("+++", 480, HOLgrammars.LEFT)
57
58val SUM_REL_def = xDefine "SUM_REL"
59       `(($+++ R1 R2) (INL (a1:'a)) (INL (a2:'a)) = R1 a1 a2) /\
60        (($+++ R1 R2) (INR (b1:'b)) (INR (b2:'b)) = R2 b1 b2) /\
61        (($+++ R1 R2) (INL a1) (INR b2) = F) /\
62        (($+++ R1 R2) (INR b1) (INL a2) = F)`;
63
64val SUM_REL_EQ = store_thm
65   ("SUM_REL_EQ",
66    (���($= +++ $=) = ($= : 'a + 'b -> 'a + 'b -> bool)���),
67    CONV_TAC FUN_EQ_CONV
68    THEN Cases
69    THEN CONV_TAC FUN_EQ_CONV
70    THEN Cases
71    THEN REWRITE_TAC[SUM_REL_def,INR_INL_11,sum_distinct,sum_distinct1]
72   );
73
74val SUM_EQUIV = store_thm
75   ("SUM_EQUIV",
76    (���!(R1:'a -> 'a -> bool) (R2:'b -> 'b -> bool).
77            EQUIV R1 ==> EQUIV R2 ==> EQUIV (R1 +++ R2)���),
78    REPEAT GEN_TAC
79    THEN REWRITE_TAC[EQUIV_def]
80    THEN REPEAT DISCH_TAC
81    THEN Cases
82    THEN Cases (* 4 subgoals *)
83    THEN ASM_REWRITE_TAC[SUM_REL_def]
84    THEN CONV_TAC (RAND_CONV FUN_EQ_CONV)
85    THENL
86      [ EQ_TAC
87        THENL
88          [ STRIP_TAC
89            THEN Cases
90            THEN ASM_REWRITE_TAC[SUM_REL_def],
91
92            DISCH_THEN (MP_TAC o SPEC ``INL x :'a + 'b``)
93            THEN ASM_REWRITE_TAC[SUM_REL_def]
94          ],
95
96        DISCH_THEN (MP_TAC o SPEC ``INL x' :'a + 'b``)
97        THEN ASM_REWRITE_TAC[SUM_REL_def],
98
99        DISCH_THEN (MP_TAC o SPEC ``INR y :'a + 'b``)
100        THEN ASM_REWRITE_TAC[SUM_REL_def],
101
102        EQ_TAC
103        THENL
104          [ STRIP_TAC
105            THEN Cases
106            THEN ASM_REWRITE_TAC[SUM_REL_def],
107
108            DISCH_THEN (MP_TAC o SPEC ``INR y'' :'a + 'b``)
109            THEN ASM_REWRITE_TAC[SUM_REL_def]
110          ]
111      ]
112   );
113
114val SUM_QUOTIENT = store_thm
115   ("SUM_QUOTIENT",
116    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
117        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
118         QUOTIENT (R1 +++ R2) (abs1 ++ abs2) (rep1 ++ rep2)���),
119    REPEAT STRIP_TAC
120    THEN REWRITE_TAC[QUOTIENT_def]
121    THEN REPEAT CONJ_TAC
122    THENL
123      [ IMP_RES_TAC QUOTIENT_ABS_REP
124        THEN Cases
125        THEN ASM_REWRITE_TAC[SUM_MAP_def],
126
127        IMP_RES_TAC QUOTIENT_REP_REFL
128        THEN Cases
129        THEN ASM_REWRITE_TAC[SUM_MAP_def,SUM_REL_def],
130
131        REPEAT Cases
132        THEN REWRITE_TAC[SUM_REL_def,SUM_MAP_def]
133        THEN REWRITE_TAC[INR_INL_11,sum_distinct,GSYM sum_distinct]
134        THEN IMP_RES_THEN
135                 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th])))
136                 QUOTIENT_REL
137        THEN REFL_TAC
138      ]
139   );
140
141
142
143(* sum theory: INL, INR, ISL, ISR, ++ *)
144
145val INL_PRS = store_thm
146   ("INL_PRS",
147    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
148        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
149         !a. INL a = (abs1 ++ abs2) (INL (rep1 a))���),
150    REPEAT STRIP_TAC
151    THEN PURE_REWRITE_TAC[SUM_MAP_def]
152    THEN PURE_REWRITE_TAC[INR_INL_11]
153    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
154   );
155
156val INL_RSP = store_thm
157   ("INL_RSP",
158    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
159        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
160         !a1 a2.
161          R1 a1 a2 ==>
162          (R1 +++ R2) (INL a1) (INL a2)���),
163    REPEAT GEN_TAC
164    THEN DISCH_TAC
165    THEN REPEAT GEN_TAC
166    THEN DISCH_TAC
167    THEN REPEAT GEN_TAC
168    THEN REWRITE_TAC[SUM_REL_def]
169   );
170
171val INR_PRS = store_thm
172   ("INR_PRS",
173    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
174        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
175         !b. INR b = (abs1 ++ abs2) (INR (rep2 b))���),
176    REPEAT STRIP_TAC
177    THEN PURE_REWRITE_TAC[SUM_MAP_def]
178    THEN PURE_REWRITE_TAC[INR_INL_11]
179    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
180   );
181
182val INR_RSP = store_thm
183   ("INR_RSP",
184    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
185        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
186         !b1 b2.
187          R2 b1 b2 ==>
188          (R1 +++ R2) (INR b1) (INR b2)���),
189    REPEAT GEN_TAC
190    THEN DISCH_TAC
191    THEN REPEAT GEN_TAC
192    THEN DISCH_TAC
193    THEN REPEAT GEN_TAC
194    THEN REWRITE_TAC[SUM_REL_def]
195   );
196
197val ISL_PRS = store_thm
198   ("ISL_PRS",
199    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
200        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
201         !a. ISL a = ISL ((rep1 ++ rep2) a)���),
202    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
203    THEN Cases
204    THEN PURE_REWRITE_TAC[SUM_MAP_def]
205    THEN REWRITE_TAC[ISL]
206   );
207
208val ISL_RSP = store_thm
209   ("ISL_RSP",
210    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
211        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
212         !a1 a2.
213          (R1 +++ R2) a1 a2 ==>
214          (ISL a1 = ISL a2)���),
215    REPEAT GEN_TAC THEN DISCH_TAC
216    THEN REPEAT GEN_TAC THEN DISCH_TAC
217    THEN Cases
218    THEN Cases
219    THEN REWRITE_TAC[SUM_REL_def,ISL]
220   );
221
222val ISR_PRS = store_thm
223   ("ISR_PRS",
224    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
225        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
226         !a. ISR a = ISR ((rep1 ++ rep2) a)���),
227    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
228    THEN Cases
229    THEN PURE_REWRITE_TAC[SUM_MAP_def]
230    THEN REWRITE_TAC[ISR]
231   );
232
233val ISR_RSP = store_thm
234   ("ISR_RSP",
235    (���!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
236        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
237         !a1 a2.
238          (R1 +++ R2) a1 a2 ==>
239          (ISR a1 = ISR a2)���),
240    REPEAT GEN_TAC THEN DISCH_TAC
241    THEN REPEAT GEN_TAC THEN DISCH_TAC
242    THEN Cases
243    THEN Cases
244    THEN REWRITE_TAC[SUM_REL_def,ISR]
245   );
246
247(* OUTL and OUTR are not completely defined, so do not lift. *)
248
249val SUM_MAP_PRS = store_thm
250   ("SUM_MAP_PRS",
251    (���!R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
252        !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
253        !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
254        !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
255         !f g. (f ++ g) =
256               ((rep1 ++ rep3) --> (abs2 ++ abs4))
257                   (((abs1 --> rep2) f) ++ ((abs3 --> rep4) g))���),
258    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
259    THEN REPEAT GEN_TAC
260    THEN CONV_TAC FUN_EQ_CONV
261    THEN Cases
262    THEN PURE_REWRITE_TAC[FUN_MAP_THM,SUM_MAP_def]
263    THEN IMP_RES_THEN REWRITE_THM QUOTIENT_ABS_REP
264   );
265
266val SUM_MAP_RSP = store_thm
267   ("SUM_MAP_RSP",
268    (���!R1 (abs1:'a -> 'e) rep1. QUOTIENT R1 abs1 rep1 ==>
269        !R2 (abs2:'b -> 'f) rep2. QUOTIENT R2 abs2 rep2 ==>
270        !R3 (abs3:'c -> 'g) rep3. QUOTIENT R3 abs3 rep3 ==>
271        !R4 (abs4:'d -> 'h) rep4. QUOTIENT R4 abs4 rep4 ==>
272         !f1 f2 g1 g2.
273          (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
274          ((R1 +++ R3) ===> (R2 +++ R4)) (f1 ++ g1) (f2 ++ g2)���),
275    REPEAT (REPEAT GEN_TAC THEN DISCH_TAC)
276    THEN POP_ASSUM MP_TAC
277    THEN REWRITE_TAC[FUN_REL]
278    THEN STRIP_TAC
279    THEN Cases
280    THEN Cases
281    THEN ASM_REWRITE_TAC[SUM_REL_def,SUM_MAP_def]
282   );
283
284
285val _ = temp_remove_termtok {term_name = "SUM_MAP", tok = "++"}
286
287
288val _ = export_theory();
289
290val _ = print_theory_to_file "-" "quotient_sum.lst";
291
292val _ = html_theory "quotient_sum";
293