1(* ===================================================================== *) 2(* FILE : combinScript.sml *) 3(* DESCRIPTION : Basic combinator definitions and some theorems about *) 4(* them. Translated from hol88. *) 5(* *) 6(* AUTHOR : (c) Tom Melham, University of Cambridge *) 7(* DATE : 87.02.26 *) 8(* TRANSLATOR : Konrad Slind, University of Calgary *) 9(* DATE : September 15, 1991 *) 10(* AUGMENTED : (kxs) added C and W combinators *) 11(* ===================================================================== *) 12 13open HolKernel Parse boolLib; 14 15val _ = new_theory "combin"; 16 17(*---------------------------------------------------------------------------*) 18(* Some basic combinators: function composition, S, K, I, W, and C. *) 19(*---------------------------------------------------------------------------*) 20 21val K_DEF = Q.new_definition("K_DEF", `K = \x y. x`); 22val S_DEF = Q.new_definition("S_DEF", `S = \f g x. f x (g x)`); 23val I_DEF = Q.new_definition("I_DEF", `I = S K (K:'a->'a->'a)`); 24val C_DEF = Q.new_definition("C_DEF", `C = \f x y. f y x`); 25val W_DEF = Q.new_definition("W_DEF", `W = \f x. f x x`); 26val o_DEF = Q.new_infixr_definition("o_DEF", `$o f g = \x. f(g x)`, 800); 27val APP_DEF = Q.new_definition ("APP_DEF", `$:> x f = f x`); 28 29val UPDATE_def = Q.new_definition("UPDATE_def", 30 `UPDATE a b = \f c. if a = c then b else f c`); 31 32val _ = set_fixity ":>" (Infixl 310); 33val _ = set_mapped_fixity {tok = "=+", fixity = Infix(NONASSOC, 320), 34 term_name = "UPDATE"} 35val _ = Parse.Unicode.unicode_version {tmnm = "o", u = UTF8.chr 0x2218} 36val _ = TeX_notation {hol = "o", TeX = ("\\HOLTokenCompose", 1)} 37val _ = TeX_notation {hol = UTF8.chr 0x2218, TeX = ("\\HOLTokenCompose", 1)} 38 39val _ = let 40 open combinpp 41 fun addlform l r = 42 add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 43 fixity = Suffix 2100, 44 paren_style = OnlyIfNecessary, 45 pp_elements = [ 46 TOK l, 47 ListForm { 48 separator = [TOK ";", BreakSpace(1,0)], 49 block_info = (PP.CONSISTENT, 1), 50 cons = internal_consupd, 51 nilstr = internal_idupd 52 }, 53 TOK r], 54 term_name = toplevel_updname}; 55in 56 set_mapped_fixity {fixity = Infix(NONASSOC,100), 57 term_name = mapsto_special, 58 tok = "|->"}; 59 set_mapped_fixity {fixity = Infix(NONASSOC,100), 60 term_name = mapsto_special, 61 tok = "���"}; (* UOK *) 62 addlform "(|" "|)"; 63 addlform UnicodeChars.lensel UnicodeChars.lenser; 64 add_ML_dependency "combinpp"; 65 add_absyn_postprocessor "combin.UPDATE"; 66 inferior_overload_on (update_constname, ``UPDATE``); 67 add_user_printer ("combin.updpp", ���UPDATE k v f���) 68end; 69 70 71local open OpenTheoryMap in 72 val _ = OpenTheory_const_name {const={Thy="combin",Name="K"},name=(["Function"],"const")} 73 val _ = OpenTheory_const_name {const={Thy="combin",Name="C"},name=(["Function"],"flip")} 74 val _ = OpenTheory_const_name {const={Thy="combin",Name="I"},name=(["Function"],"id")} 75 val _ = OpenTheory_const_name {const={Thy="combin",Name="o"},name=(["Function"],"o")} 76 val _ = OpenTheory_const_name {const={Thy="combin",Name="S"},name=(["Function","Combinator"],"s")} 77 val _ = OpenTheory_const_name {const={Thy="combin",Name="W"},name=(["Function","Combinator"],"w")} 78end 79(*---------------------------------------------------------------------------* 80 * In I_DEF, the type constraint is necessary in order to meet one of * 81 * the criteria for a definition : the tyvars of the lhs must be a * 82 * superset of those on the rhs. * 83 *---------------------------------------------------------------------------*) 84 85 86val o_THM = store_thm("o_THM", 87 ���!f g x. (f o g) x = f(g x)���, 88 REPEAT GEN_TAC 89 THEN PURE_REWRITE_TAC [ o_DEF ] 90 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 91 THEN REFL_TAC); 92 93val o_ASSOC = store_thm("o_ASSOC", 94 ���!f g h. f o (g o h) = (f o g) o h���, 95 REPEAT GEN_TAC 96 THEN REWRITE_TAC [ o_DEF ] 97 THEN CONV_TAC (REDEPTH_CONV BETA_CONV) 98 THEN REFL_TAC); 99 100Theorem o_ASSOC' = GSYM o_ASSOC 101 102val o_ABS_L = store_thm( 103 "o_ABS_L", 104 ``(\x:'a. f x:'c) o (g:'b -> 'a) = (\x. f (g x))``, 105 REWRITE_TAC [FUN_EQ_THM, o_THM] THEN BETA_TAC THEN REWRITE_TAC []); 106 107val o_ABS_R = store_thm( 108 "o_ABS_R", 109 ``f o (\x. g x) = (\x. f (g x))``, 110 REWRITE_TAC [FUN_EQ_THM, o_THM] THEN BETA_TAC THEN REWRITE_TAC []); 111 112val K_THM = store_thm("K_THM", 113 ���!x y. K x y = x���, 114 REPEAT GEN_TAC 115 THEN PURE_REWRITE_TAC [ K_DEF ] 116 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 117 THEN REFL_TAC); 118 119val S_THM = store_thm("S_THM", 120 ���!f g x. S f g x = f x (g x)���, 121 REPEAT GEN_TAC 122 THEN PURE_REWRITE_TAC [ S_DEF ] 123 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 124 THEN REFL_TAC); 125 126val S_ABS_L = store_thm( 127 "S_ABS_L", 128 ``S (\x. f x) g = \x. (f x) (g x)``, 129 REWRITE_TAC [FUN_EQ_THM, S_THM] THEN BETA_TAC THEN REWRITE_TAC []); 130 131val S_ABS_R = store_thm( 132 "S_ABS_R", 133 ``S f (\x. g x) = \x. (f x) (g x)``, 134 REWRITE_TAC [FUN_EQ_THM, S_THM] THEN BETA_TAC THEN REWRITE_TAC[]); 135 136val C_THM = store_thm("C_THM", 137 ���!f x y. C f x y = f y x���, 138 REPEAT GEN_TAC 139 THEN PURE_REWRITE_TAC [ C_DEF ] 140 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 141 THEN REFL_TAC); 142 143val C_ABS_L = store_thm( 144 "C_ABS_L", 145 ``C (\x. f x) y = (\x. f x y)``, 146 REWRITE_TAC [FUN_EQ_THM, C_THM] THEN BETA_TAC THEN REWRITE_TAC []); 147 148val W_THM = store_thm("W_THM", 149 ���!f x. W f x = f x x���, 150 REPEAT GEN_TAC 151 THEN PURE_REWRITE_TAC [ W_DEF ] 152 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 153 THEN REFL_TAC); 154 155val I_THM = store_thm("I_THM", 156 ���!x. I x = x���, 157 REPEAT GEN_TAC 158 THEN PURE_REWRITE_TAC [ I_DEF, S_THM, K_THM ] 159 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 160 THEN REFL_TAC); 161 162val I_o_ID = store_thm("I_o_ID", 163 ���!f. (I o f = f) /\ (f o I = f)���, 164 REWRITE_TAC [I_THM, o_THM, FUN_EQ_THM]); 165 166val K_o_THM = store_thm("K_o_THM", 167 ���(!f v. K v o f = K v) /\ (!f v. f o K v = K (f v))���, 168 REWRITE_TAC [o_THM, K_THM, FUN_EQ_THM]); 169 170val UPDATE_APPLY = Q.store_thm("UPDATE_APPLY", 171 `(!a x f. (a =+ x) f a = x) /\ 172 (!a b x f. a <> b ==> ((a =+ x) f b = f b))`, 173 REWRITE_TAC [UPDATE_def] 174 THEN BETA_TAC 175 THEN REWRITE_TAC [] 176 THEN REPEAT STRIP_TAC 177 THEN ASM_REWRITE_TAC []) 178 179val APPLY_UPDATE_THM = Q.store_thm("APPLY_UPDATE_THM", 180 `!f a b c. (a =+ b) f c = (if a = c then b else f c)`, 181 PURE_REWRITE_TAC [UPDATE_def] 182 THEN BETA_TAC THEN REWRITE_TAC []); 183 184val UPDATE_COMMUTES = Q.store_thm("UPDATE_COMMUTES", 185 `!f a b c d. ~(a = b) ==> ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f))`, 186 REPEAT STRIP_TAC 187 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 188 THEN BETA_TAC THEN GEN_TAC 189 THEN NTAC 2 COND_CASES_TAC 190 THEN BETA_TAC 191 THEN PURE_ASM_REWRITE_TAC [] 192 THEN NTAC 2 (POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th]))) 193 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC []); 194 195val UPDATE_EQ = Q.store_thm("UPDATE_EQ", 196 `!f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f`, 197 REPEAT STRIP_TAC 198 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 199 THEN TRY GEN_TAC THEN BETA_TAC 200 THEN NTAC 2 (TRY COND_CASES_TAC) 201 THEN BETA_TAC THEN ASM_REWRITE_TAC []); 202 203val UPDATE_APPLY_ID = Q.store_thm("UPDATE_APPLY_ID", 204 `!f a b. (f a = b) = ((a =+ b) f = f)`, 205 REPEAT GEN_TAC 206 THEN EQ_TAC 207 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 208 THENL [ 209 REPEAT STRIP_TAC 210 THEN BETA_TAC 211 THEN COND_CASES_TAC 212 THEN1 POP_ASSUM (fn th => ASM_REWRITE_TAC [SYM th]) 213 THEN REWRITE_TAC [], 214 BETA_TAC THEN STRIP_TAC 215 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC) 216 THEN RULE_ASSUM_TAC (REWRITE_RULE []) 217 THEN ASM_REWRITE_TAC []]); 218 219val UPDATE_APPLY_ID' = GSYM UPDATE_APPLY_ID 220Theorem UPDATE_APPLY_ID_RWT = 221 CONJ UPDATE_APPLY_ID' 222 (CONV_RULE (STRIP_QUANT_CONV (LAND_CONV (REWR_CONV EQ_SYM_EQ))) 223 UPDATE_APPLY_ID') 224 225 226val UPDATE_APPLY_IMP_ID = save_thm("UPDATE_APPLY_IMP_ID", 227 GEN_ALL (fst (EQ_IMP_RULE (SPEC_ALL UPDATE_APPLY_ID)))); 228 229val APPLY_UPDATE_ID = Q.store_thm("APPLY_UPDATE_ID", 230 `!f a. (a =+ f a) f = f`, 231 REWRITE_TAC [GSYM UPDATE_APPLY_ID]); 232 233Theorem UPD11_SAME_BASE: 234 !f a b c d. 235 ((a =+ c) f = (b =+ d) f) <=> 236 a = b /\ c = d \/ 237 a <> b /\ (a =+ c) f = f /\ (b =+ d) f = f 238Proof 239 REPEAT GEN_TAC 240 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 241 THEN BETA_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] 242 THEN ASM_CASES_TAC ``a = b`` THEN ASM_REWRITE_TAC [] 243 THENL [ 244 POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th])) 245 THEN POP_ASSUM (Q.SPEC_THEN `b` ASSUME_TAC) 246 THEN RULE_ASSUM_TAC (REWRITE_RULE []) 247 THEN ASM_REWRITE_TAC [], 248 GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC [] 249 THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (PURE_REWRITE_RULE [th])) 250 THEN FIRST_ASSUM (Q.SPEC_THEN `x` ASSUME_TAC) 251 THEN Q.PAT_ASSUM `~(a = x)` (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) 252 THEN ASM_REWRITE_TAC [] 253 ] 254QED 255 256val SAME_KEY_UPDATE_DIFFER = Q.store_thm("SAME_KEY_UPDATE_DIFFER", 257 `!f1 f2 a b c. ~(b = c) ==> ~((a =+ b) f = (a =+ c) f)`, 258 REPEAT GEN_TAC THEN STRIP_TAC 259 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 260 THEN BETA_TAC 261 THEN STRIP_TAC 262 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC) 263 THEN RULE_ASSUM_TAC (REWRITE_RULE []) 264 THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) 265 THEN POP_ASSUM CONTR_TAC); 266 267val UPD11_SAME_KEY_AND_BASE = Q.store_thm("UPD11_SAME_KEY_AND_BASE", 268 `!f a b c. ((a =+ b) f = (a =+ c) f) = (b = c)`, 269 REPEAT GEN_TAC THEN EQ_TAC 270 THEN PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 271 THEN BETA_TAC THEN STRIP_TAC 272 THEN ASM_REWRITE_TAC [] 273 THEN POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC) 274 THEN RULE_ASSUM_TAC (REWRITE_RULE []) 275 THEN ASM_REWRITE_TAC []); 276 277val UPD_SAME_KEY_UNWIND = Q.store_thm("UPD_SAME_KEY_UNWIND", 278 `!f1 f2 a b c. 279 ((a =+ b) f1 = (a =+ c) f2) ==> 280 (b = c) /\ !v. (a =+ v) f1 = (a =+ v) f2`, 281 PURE_REWRITE_TAC [UPDATE_def,FUN_EQ_THM] 282 THEN BETA_TAC THEN REPEAT STRIP_TAC 283 THENL [ 284 POP_ASSUM (Q.SPEC_THEN `a` ASSUME_TAC) 285 THEN RULE_ASSUM_TAC (REWRITE_RULE []) 286 THEN ASM_REWRITE_TAC [], 287 COND_CASES_TAC THEN REWRITE_TAC [] 288 THEN FIRST_ASSUM (Q.SPEC_THEN `x` ASSUME_TAC) 289 THEN Q.PAT_ASSUM `~(a = x)` (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) 290 THEN ASM_REWRITE_TAC []]); 291 292(*---------------------------------------------------------------------------*) 293(* Theorems using combinators to specify let-movements *) 294(*---------------------------------------------------------------------------*) 295 296val GEN_LET_RAND = store_thm( 297 "GEN_LET_RAND", 298 ``P (LET f v) = LET (P o f) v``, 299 REWRITE_TAC [LET_THM, o_THM]); 300 301val GEN_LET_RATOR = store_thm( 302 "GEN_LET_RATOR", 303 ``(LET f v) x = LET (C f x) v``, 304 REWRITE_TAC [LET_THM, C_THM]); 305 306val LET_FORALL_ELIM = store_thm( 307 "LET_FORALL_ELIM", 308 ``LET f v = (!) (S ((==>) o Abbrev o (C (=) v)) f)``, 309 REWRITE_TAC [S_DEF, LET_THM, C_DEF] THEN BETA_TAC THEN 310 REWRITE_TAC [o_THM, markerTheory.Abbrev_def] THEN BETA_TAC THEN 311 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 312 ASM_REWRITE_TAC [], 313 FIRST_X_ASSUM MATCH_MP_TAC THEN REFL_TAC 314 ]); 315 316val GEN_literal_case_RAND = store_thm( 317 "GEN_literal_case_RAND", 318 ``P (literal_case f v) = literal_case (P o f) v``, 319 REWRITE_TAC [literal_case_THM, o_THM]); 320 321val GEN_literal_case_RATOR = store_thm( 322 "GEN_literal_case_RATOR", 323 ``(literal_case f v) x = literal_case (C f x) v``, 324 REWRITE_TAC [literal_case_THM, C_THM]); 325 326val literal_case_FORALL_ELIM = store_thm( 327 "literal_case_FORALL_ELIM", 328 ``literal_case f v = (!) (S ((==>) o Abbrev o (C (=) v)) f)``, 329 REWRITE_TAC [S_DEF, literal_case_THM, C_DEF] THEN BETA_TAC THEN 330 REWRITE_TAC [o_THM, markerTheory.Abbrev_def] THEN BETA_TAC THEN 331 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 332 ASM_REWRITE_TAC [], 333 FIRST_X_ASSUM MATCH_MP_TAC THEN REFL_TAC 334 ]); 335 336(* ---------------------------------------------------------------------- 337 Predicates on functions 338 ---------------------------------------------------------------------- *) 339 340val ASSOC_DEF = new_definition("ASSOC_DEF", 341 `` 342 ASSOC (f:'a->'a->'a) <=> (!x y z. f x (f y z) = f (f x y) z) 343 ``); 344 345val COMM_DEF = new_definition("COMM_DEF", 346 `` 347 COMM (f:'a->'a->'b) <=> (!x y. f x y = f y x) 348 ``); 349 350val FCOMM_DEF = new_definition("FCOMM_DEF", 351 `` 352 FCOMM (f:'a->'b->'a) (g:'c->'a->'a) <=> (!x y z. g x (f y z) = f (g x y) z) 353 ``); 354 355val RIGHT_ID_DEF = new_definition("RIGHT_ID_DEF", 356 `` 357 RIGHT_ID (f:'a->'b->'a) e <=> (!x. f x e = x) 358 ``); 359 360val LEFT_ID_DEF = new_definition("LEFT_ID_DEF", 361 `` 362 LEFT_ID (f:'a->'b->'b) e <=> (!x. f e x = x) 363 ``); 364 365val MONOID_DEF = new_definition("MONOID_DEF", 366 `` 367 MONOID (f:'a->'a->'a) e <=> 368 ASSOC f /\ RIGHT_ID f e /\ LEFT_ID f e 369 ``); 370 371(* ======================================================================== *) 372(* Theorems about operators *) 373(* ======================================================================== *) 374 375val ASSOC_CONJ = store_thm ("ASSOC_CONJ", ``ASSOC $/\``, 376 REWRITE_TAC[ASSOC_DEF,CONJ_ASSOC]); 377 378val ASSOC_SYM = save_thm ("ASSOC_SYM", 379 CONV_RULE 380 (STRIP_QUANT_CONV (RHS_CONV (STRIP_QUANT_CONV SYM_CONV))) 381 ASSOC_DEF); 382 383 384val ASSOC_DISJ = store_thm ("ASSOC_DISJ", 385 ``ASSOC $\/``, 386 REWRITE_TAC[ASSOC_DEF,DISJ_ASSOC]); 387 388val FCOMM_ASSOC = store_thm ("FCOMM_ASSOC", 389 ``!f: 'a->'a->'a. FCOMM f f = ASSOC f``, 390 REWRITE_TAC[ASSOC_DEF,FCOMM_DEF]); 391 392val MONOID_CONJ_T = store_thm ("MONOID_CONJ_T", 393 ``MONOID $/\ T``, 394 REWRITE_TAC[MONOID_DEF,CONJ_ASSOC, LEFT_ID_DEF,ASSOC_DEF,RIGHT_ID_DEF]); 395 396val MONOID_DISJ_F = store_thm ("MONOID_DISJ_F", 397 ``MONOID $\/ F``, 398 REWRITE_TAC[MONOID_DEF,DISJ_ASSOC, 399 LEFT_ID_DEF,ASSOC_DEF,RIGHT_ID_DEF]); 400 401(*---------------------------------------------------------------------------*) 402(* Tag combinator equal to K. Used in generating ML from HOL *) 403(*---------------------------------------------------------------------------*) 404 405val FAIL_DEF = Q.new_definition("FAIL_DEF", `FAIL = \x y. x`); 406val FAIL_THM = Q.store_thm("FAIL_THM", `FAIL x y = x`, 407 REPEAT GEN_TAC 408 THEN PURE_REWRITE_TAC [ FAIL_DEF ] 409 THEN CONV_TAC (DEPTH_CONV BETA_CONV) 410 THEN REFL_TAC); 411 412Overload flip = ���C��� 413val _ = remove_ovl_mapping "C" {Name="C", Thy = "combin"} 414 415val _ = adjoin_to_theory 416{sig_ps = NONE, 417 struct_ps = SOME (fn _ => 418 let val S = PP.add_string fun SPC n = PP.add_break(1,n) 419 fun B n = PP.block PP.CONSISTENT n 420 fun I n = PP.block PP.INCONSISTENT n 421 val L = PP.pr_list 422 in 423 B 0 [ 424 S "val _ =", SPC 2, 425 B 4 [ 426 S "let open computeLib", SPC 0, 427 B 2 [ 428 S "val K_tm =", SPC 0, 429 S "Term.prim_mk_const{Name=\"K\",Thy=\"combin\"}" 430 ], SPC ~4, 431 S "in", SPC 0, 432 B 2 [ 433 S "add_funs", SPC 0, 434 I 1 (S "[" :: 435 L S [S ",", PP.add_break(0,0)] [ 436 "K_THM", "S_DEF", "I_THM", "C_DEF", "W_DEF", "o_THM", 437 "K_o_THM", "APP_DEF", "APPLY_UPDATE_THM];" 438 ]) 439 ], SPC 0, 440 B 2 (L S [SPC 1] ["set_skip", "the_compset", "K_tm", "(SOME 1)"]), 441 SPC ~4, S "end;" 442 ] 443 ] 444 end)} 445 446val _ = export_theory(); 447