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