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