1(* ===================================================================== *) 2(* FILE : pairScript.sml *) 3(* DESCRIPTION : The theory of pairs. This is a mix of the original *) 4(* non-definitional theory of pairs from hol88 *) 5(* and John Harrison's definitional theory of pairs from *) 6(* GTT, plus some subsequent simplifications from *) 7(* Konrad Slind. *) 8(* *) 9(* AUTHORS : (c) Mike Gordon, John Harrison, Konrad Slind *) 10(* Jim Grundy *) 11(* University of Cambridge *) 12(* DATE : August 7, 1997 *) 13(* ===================================================================== *) 14 15(* interactive use: 16 app load ["Q", "relationTheory", "mesonLib", "OpenTheoryMap", "BasicProvers"]; 17 open Parse relationTheory mesonLib; 18*) 19 20open HolKernel Parse boolLib relationTheory mesonLib metisLib 21 22val _ = new_theory "pair"; 23 24(*---------------------------------------------------------------------------*) 25(* Define the type of pairs and tell the grammar about it. *) 26(*---------------------------------------------------------------------------*) 27 28val pairfn = Term `\a b. (a=x) /\ (b=y)`; 29 30val PAIR_EXISTS = Q.prove 31(`?p:'a -> 'b -> bool. (\p. ?x y. p = ^pairfn) p`, 32 BETA_TAC 33 THEN Ho_Rewrite.ONCE_REWRITE_TAC [SWAP_EXISTS_THM] THEN Q.EXISTS_TAC `x` 34 THEN Ho_Rewrite.ONCE_REWRITE_TAC [SWAP_EXISTS_THM] THEN Q.EXISTS_TAC `y` 35 THEN EXISTS_TAC pairfn 36 THEN REFL_TAC); 37 38val ABS_REP_prod = 39 let val tydef = new_type_definition("prod", PAIR_EXISTS) 40 in 41 define_new_type_bijections 42 {ABS="ABS_prod", REP="REP_prod", 43 name="ABS_REP_prod", tyax=tydef} 44 end; 45 46val _ = add_infix_type 47 {Prec = 70, 48 ParseName = SOME "#", Name = "prod", 49 Assoc = HOLgrammars.RIGHT}; 50val _ = TeX_notation { hol = "#", TeX = ("\\HOLTokenProd{}", 1)} 51local 52 open OpenTheoryMap 53 val ns = ["Data","Pair"] 54in 55 val _ = OpenTheory_tyop_name{tyop={Thy="pair",Tyop="prod"},name=(ns,"*")} 56 fun ot0 x y = OpenTheory_const_name{const={Thy="pair",Name=x},name=(ns,y)} 57 fun ot x = ot0 x x 58end 59 60val REP_ABS_PAIR = Q.prove 61(`!x y. REP_prod (ABS_prod ^pairfn) = ^pairfn`, 62 REPEAT GEN_TAC 63 THEN REWRITE_TAC [SYM (SPEC pairfn (CONJUNCT2 ABS_REP_prod))] 64 THEN BETA_TAC 65 THEN MAP_EVERY Q.EXISTS_TAC [`x`, `y`] 66 THEN REFL_TAC); 67 68 69(*---------------------------------------------------------------------------*) 70(* Define the constructor for pairs, and install grammar rule for it. *) 71(*---------------------------------------------------------------------------*) 72 73val COMMA_DEF = 74 Q.new_definition 75 ("COMMA_DEF", 76 `$, x y = ABS_prod ^pairfn`); 77val _ = ot"," 78 79val _ = add_rule {term_name = ",", fixity = Infixr 50, 80 pp_elements = [TOK ",", BreakSpace(0,0)], 81 paren_style = ParoundName, 82 block_style = (AroundSameName, (PP.INCONSISTENT, 0))}; 83 84 85(*--------------------------------------------------------------------------- 86 The constructor for pairs is one-to-one. 87 ---------------------------------------------------------------------------*) 88 89val PAIR_EQ = Q.store_thm 90("PAIR_EQ", 91 `((x,y) = (a,b)) = (x=a) /\ (y=b)`, 92 EQ_TAC THENL 93 [REWRITE_TAC[COMMA_DEF] 94 THEN DISCH_THEN(MP_TAC o Q.AP_TERM `REP_prod`) 95 THEN REWRITE_TAC [REP_ABS_PAIR] 96 THEN Ho_Rewrite.REWRITE_TAC [FUN_EQ_THM] 97 THEN DISCH_THEN (MP_TAC o Q.SPECL [`x`, `y`]) 98 THEN REWRITE_TAC[], 99 STRIP_TAC THEN ASM_REWRITE_TAC[]]); 100 101val CLOSED_PAIR_EQ = 102 save_thm("CLOSED_PAIR_EQ", itlist Q.GEN [`x`, `y`, `a`, `b`] PAIR_EQ); 103 104 105(*--------------------------------------------------------------------------- 106 Case analysis for pairs. 107 ---------------------------------------------------------------------------*) 108 109val ABS_PAIR_THM = Q.store_thm 110("ABS_PAIR_THM", 111 `!x. ?q r. x = (q,r)`, 112 GEN_TAC THEN REWRITE_TAC[COMMA_DEF] 113 THEN MP_TAC(Q.SPEC `REP_prod x` (CONJUNCT2 ABS_REP_prod)) 114 THEN REWRITE_TAC[CONJUNCT1 ABS_REP_prod] THEN BETA_TAC 115 THEN DISCH_THEN(Q.X_CHOOSE_THEN `a` (Q.X_CHOOSE_THEN `b` MP_TAC)) 116 THEN DISCH_THEN(MP_TAC o Q.AP_TERM `ABS_prod`) 117 THEN REWRITE_TAC[CONJUNCT1 ABS_REP_prod] 118 THEN DISCH_THEN SUBST1_TAC 119 THEN MAP_EVERY Q.EXISTS_TAC [`a`, `b`] 120 THEN REFL_TAC); 121 122val pair_CASES = save_thm("pair_CASES", ABS_PAIR_THM) 123 124 125(*---------------------------------------------------------------------------* 126 * Surjective pairing and definition of projection functions. * 127 * * 128 * PAIR = |- !x. (FST x,SND x) = x * 129 * FST = |- !x y. FST (x,y) = x * 130 * SND = |- !x y. SND (x,y) = y * 131 *---------------------------------------------------------------------------*) 132 133val PAIR = 134 Definition.new_specification 135 ("PAIR", ["FST","SND"], 136 Ho_Rewrite.REWRITE_RULE[SKOLEM_THM] (GSYM ABS_PAIR_THM)); 137 138local val th1 = REWRITE_RULE [PAIR_EQ] (SPEC (Term`(x,y):'a#'b`) PAIR) 139 val (th2,th3) = (CONJUNCT1 th1, CONJUNCT2 th1) 140in 141val FST = save_thm("FST", itlist Q.GEN [`x`,`y`] th2); 142val SND = save_thm("SND", itlist Q.GEN [`x`,`y`] th3); 143end; 144val _ = ot0 "FST" "fst" 145val _ = ot0 "SND" "snd" 146 147val PAIR_FST_SND_EQ = store_thm( 148 "PAIR_FST_SND_EQ", 149 ``!(p:'a # 'b) q. (p = q) = (FST p = FST q) /\ (SND p = SND q)``, 150 REPEAT GEN_TAC THEN 151 X_CHOOSE_THEN ``p1:'a`` (X_CHOOSE_THEN ``p2:'b`` SUBST_ALL_TAC) 152 (SPEC ``p:'a # 'b`` ABS_PAIR_THM) THEN 153 X_CHOOSE_THEN ``q1:'a`` (X_CHOOSE_THEN ``q2:'b`` SUBST_ALL_TAC) 154 (SPEC ``q:'a # 'b`` ABS_PAIR_THM) THEN 155 REWRITE_TAC [PAIR_EQ, FST, SND]); 156 157val SWAP_def = new_definition ("SWAP_def", ``SWAP a = (SND a, FST a)``) 158 159(*---------------------------------------------------------------------------*) 160(* CURRY and UNCURRY. UNCURRY is needed for terms of the form `\(x,y).t` *) 161(*---------------------------------------------------------------------------*) 162 163val CURRY_DEF = Q.new_definition 164 ("CURRY_DEF", 165 `CURRY f x y :'c = f (x,y)`); 166 167val UNCURRY = Q.new_definition 168 ("UNCURRY", 169 `UNCURRY f (v:'a#'b) = f (FST v) (SND v)`); 170val _ = ot0 "UNCURRY" "uncurry" 171 172val UNCURRY_VAR = save_thm("UNCURRY_VAR", UNCURRY); (* compatibility *) 173 174val ELIM_UNCURRY = Q.store_thm( 175 "ELIM_UNCURRY", 176 `!f:'a -> 'b -> 'c. UNCURRY f = \x. f (FST x) (SND x)`, 177 GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 178 REWRITE_TAC [UNCURRY] THEN CONV_TAC (RAND_CONV BETA_CONV) THEN 179 REFL_TAC); 180 181 182val UNCURRY_DEF = Q.store_thm 183 ("UNCURRY_DEF", 184 `!f x y. UNCURRY f (x,y) :'c = f x y`, 185 REWRITE_TAC [UNCURRY,FST,SND]) 186 187 188(* ------------------------------------------------------------------------- *) 189(* CURRY_UNCURRY_THM = |- !f. CURRY(UNCURRY f) = f *) 190(* ------------------------------------------------------------------------- *) 191 192val CURRY_UNCURRY_THM = 193 let val th1 = prove 194 (���CURRY (UNCURRY (f:'a->'b->'c)) x y = f x y���, 195 REWRITE_TAC [UNCURRY_DEF, CURRY_DEF]) 196 val th2 = GEN ���y:'b��� th1 197 val th3 = EXT th2 198 val th4 = GEN ���x:'a��� th3 199 val th4 = EXT th4 200 in 201 GEN ���f:'a->'b->'c��� th4 202 end; 203 204val _ = save_thm("CURRY_UNCURRY_THM",CURRY_UNCURRY_THM); 205 206 207(* ------------------------------------------------------------------------- *) 208(* UNCURRY_CURRY_THM = |- !f. UNCURRY(CURRY f) = f *) 209(* ------------------------------------------------------------------------- *) 210 211val UNCURRY_CURRY_THM = 212 let val th1 = prove 213 (���UNCURRY (CURRY (f:('a#'b)->'c)) (x,y) = f(x,y)���, 214 REWRITE_TAC [CURRY_DEF, UNCURRY_DEF]) 215 val th2 = Q.INST [`x:'a` |-> `FST (z:'a#'b)`, 216 `y:'b` |-> `SND (z:'a#'b)`] th1 217 val th3 = CONV_RULE (RAND_CONV 218 (RAND_CONV (K (ISPEC ���z:'a#'b��� PAIR)))) th2 219 val th4 = CONV_RULE(RATOR_CONV (RAND_CONV 220 (RAND_CONV (K (ISPEC ���z:'a#'b��� PAIR)))))th3 221 val th5 = GEN ���z:'a#'b��� th4 222 val th6 = EXT th5 223 in 224 GEN ���f:('a#'b)->'c��� th6 225 end; 226 227 val _ = save_thm("UNCURRY_CURRY_THM",UNCURRY_CURRY_THM); 228 229(* ------------------------------------------------------------------------- *) 230(* CURRY_ONE_ONE_THM = |- (CURRY f = CURRY g) = (f = g) *) 231(* ------------------------------------------------------------------------- *) 232 233val CURRY_ONE_ONE_THM = 234 let val th1 = ASSUME ���(f:('a#'b)->'c) = g��� 235 val th2 = AP_TERM ���CURRY:(('a#'b)->'c)->('a->'b->'c)��� th1 236 val th3 = DISCH_ALL th2 237 val thA = ASSUME ���(CURRY (f:('a#'b)->'c)) = (CURRY g)��� 238 val thB = AP_TERM ���UNCURRY:('a->'b->'c)->(('a#'b)->'c)��� thA 239 val thC = PURE_REWRITE_RULE [UNCURRY_CURRY_THM] thB 240 val thD = DISCH_ALL thC 241 in 242 IMP_ANTISYM_RULE thD th3 243 end; 244 245val _ = save_thm("CURRY_ONE_ONE_THM",CURRY_ONE_ONE_THM); 246 247(* ------------------------------------------------------------------------- *) 248(* UNCURRY_ONE_ONE_THM = |- (UNCURRY f = UNCURRY g) = (f = g) *) 249(* ------------------------------------------------------------------------- *) 250 251val UNCURRY_ONE_ONE_THM = 252 let val th1 = ASSUME ���(f:'a->'b->'c) = g��� 253 val th2 = AP_TERM ���UNCURRY:('a->'b->'c)->(('a#'b)->'c)��� th1 254 val th3 = DISCH_ALL th2 255 val thA = ASSUME ���(UNCURRY (f:'a->'b->'c)) = (UNCURRY g)��� 256 val thB = AP_TERM ���CURRY:(('a#'b)->'c)->('a->'b->'c)��� thA 257 val thC = PURE_REWRITE_RULE [CURRY_UNCURRY_THM] thB 258 val thD = DISCH_ALL thC 259 in 260 IMP_ANTISYM_RULE thD th3 261 end; 262 263val _ = save_thm("UNCURRY_ONE_ONE_THM",UNCURRY_ONE_ONE_THM); 264 265 266(* ------------------------------------------------------------------------- *) 267(* pair_Axiom = |- !f. ?fn. !x y. fn (x,y) = f x y *) 268(* ------------------------------------------------------------------------- *) 269 270val pair_Axiom = Q.store_thm("pair_Axiom", 271 `!f:'a->'b->'c. ?fn. !x y. fn (x,y) = f x y`, 272 GEN_TAC THEN Q.EXISTS_TAC`UNCURRY f` THEN REWRITE_TAC[UNCURRY_DEF]); 273 274(* -------------------------------------------------------------------------*) 275(* UNCURRY_CONG = *) 276(* |- !f' f M' M. *) 277(* (M = M') /\ *) 278(* (!x y. (M' = (x,y)) ==> (f x y = f' x y)) *) 279(* ==> *) 280(* (UNCURRY f M = UNCURRY f' M') *) 281(* -------------------------------------------------------------------------*) 282 283open simpLib boolSimps 284val UNCURRY_CONG = store_thm( 285 "UNCURRY_CONG", 286 ``!f' f M' M. 287 (M = M') /\ (!x y. (M' = (x,y)) ==> (f x y = f' x y)) ==> 288 (UNCURRY f M = UNCURRY f' M')``, 289 REPEAT STRIP_TAC THEN 290 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC pair_CASES THEN 291 Q.SPEC_THEN `M'` FULL_STRUCT_CASES_TAC pair_CASES THEN 292 FULL_SIMP_TAC bool_ss [PAIR_EQ, UNCURRY_DEF]) 293 294(*--------------------------------------------------------------------------- 295 LAMBDA_PROD = |- !P. (\p. P p) = (\(p1,p2). P (p1,p2)) 296 ---------------------------------------------------------------------------*) 297 298val LAMBDA_PROD = Q.store_thm("LAMBDA_PROD", 299`!P:'a#'b->'c. (\p. P p) = \(p1,p2). P(p1,p2)`, 300 GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC 301 THEN STRUCT_CASES_TAC (Q.SPEC `p` ABS_PAIR_THM) 302 THEN REWRITE_TAC [UNCURRY,FST,SND] 303 THEN BETA_TAC THEN REFL_TAC) 304 305(*--------------------------------------------------------------------------- 306 EXISTS_PROD = |- (?p. P p) = ?p_1 p_2. P (p_1,p_2) 307 ---------------------------------------------------------------------------*) 308 309val EXISTS_PROD = Q.store_thm("EXISTS_PROD", 310 `(?p. P p) = ?p_1 p_2. P (p_1,p_2)`, 311 EQ_TAC THEN STRIP_TAC 312 THENL [MAP_EVERY Q.EXISTS_TAC [`FST p`, `SND p`], Q.EXISTS_TAC `p_1, p_2`] 313 THEN ASM_REWRITE_TAC[PAIR]); 314 315(*--------------------------------------------------------------------------- 316 FORALL_PROD = |- (!p. P p) = !p_1 p_2. P (p_1,p_2) 317 ---------------------------------------------------------------------------*) 318 319val FORALL_PROD = Q.store_thm("FORALL_PROD", 320 `(!p. P p) = !p_1 p_2. P (p_1,p_2)`, 321 EQ_TAC THENL 322 [DISCH_THEN(fn th => REPEAT GEN_TAC THEN ASSUME_TAC (Q.SPEC `p_1, p_2` th)), 323 REPEAT STRIP_TAC 324 THEN REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC (Q.SPEC `p` ABS_PAIR_THM) 325 ] 326 THEN ASM_REWRITE_TAC[]); 327 328 329val pair_induction = save_thm("pair_induction", #2(EQ_IMP_RULE FORALL_PROD)); 330 331(* ---------------------------------------------------------------------- 332 PROD_ALL 333 ---------------------------------------------------------------------- *) 334 335val PROD_ALL_def = new_definition( 336 "PROD_ALL_def", 337 ``PROD_ALL (P:'a -> bool) (Q : 'b -> bool) p <=> P (FST p) /\ Q (SND p)``); 338 339val PROD_ALL_THM = store_thm( 340 "PROD_ALL_THM", 341 ``PROD_ALL P Q (x:'a,y:'b) <=> P x /\ Q y``, 342 REWRITE_TAC [PROD_ALL_def, FST, SND]); 343val _ = BasicProvers.export_rewrites ["PROD_ALL_THM"] 344val _ = computeLib.add_persistent_funs ["PROD_ALL_THM"] 345 346val PROD_ALL_MONO = store_thm( 347 "PROD_ALL_MONO", 348 ``(!x:'a. P x ==> P' x) /\ (!y:'b. Q y ==> Q' y) ==> 349 PROD_ALL P Q p ==> PROD_ALL P' Q' p``, 350 Q.SPEC_THEN `p` STRUCT_CASES_TAC ABS_PAIR_THM THEN 351 REWRITE_TAC [PROD_ALL_THM] THEN REPEAT STRIP_TAC THEN RES_TAC); 352val _ = IndDefLib.export_mono "PROD_ALL_MONO" 353 354val PROD_ALL_CONG = store_thm( 355 "PROD_ALL_CONG[defncong]", 356 ``!p p' P P' Q Q'. 357 (p = p') /\ (!x:'a y:'b. (p' = (x,y)) ==> (P x <=> P' x)) /\ 358 (!x:'a y:'b. (p' = (x,y)) ==> (Q y <=> Q' y)) ==> 359 (PROD_ALL P Q p <=> PROD_ALL P' Q' p')``, 360 SIMP_TAC (BasicProvers.srw_ss()) [FORALL_PROD, PAIR_EQ]); 361 362(* ------------------------------------------------------------------------- *) 363(* ELIM_PEXISTS = |- !P. (?p. P (FST p) (SND p)) = ?p1 p2. P p1 p2 *) 364(* ------------------------------------------------------------------------- *) 365 366val ELIM_PEXISTS = Q.store_thm 367("ELIM_PEXISTS", 368 `(?p. P (FST p) (SND p)) = ?p1 p2. P p1 p2`, 369 EQ_TAC THEN STRIP_TAC THENL 370 [MAP_EVERY Q.EXISTS_TAC [`FST p`, `SND p`] THEN ASM_REWRITE_TAC [], 371 Q.EXISTS_TAC `(p1,p2)` THEN ASM_REWRITE_TAC [FST,SND]]); 372 373(* ------------------------------------------------------------------------- *) 374(* ELIM_PFORALL = |- !P. (!p. P (FST p) (SND p)) = !p1 p2. P p1 p2 *) 375(* ------------------------------------------------------------------------- *) 376 377val ELIM_PFORALL = Q.store_thm 378("ELIM_PFORALL", 379 `(!p. P (FST p) (SND p)) = !p1 p2. P p1 p2`, 380 EQ_TAC THEN REPEAT STRIP_TAC THENL 381 [POP_ASSUM (MP_TAC o Q.SPEC `(p1,p2)`) THEN REWRITE_TAC [FST,SND], 382 ASM_REWRITE_TAC []]); 383 384(* ------------------------------------------------------------------------- *) 385(* PFORALL_THM = |- !P. (!x y. P x y) = (!(x,y). P x y) *) 386(* ------------------------------------------------------------------------- *) 387 388val PFORALL_THM = Q.store_thm 389("PFORALL_THM", 390 `!P:'a -> 'b -> bool. (!x y. P x y) = !(x,y). P x y`, 391 REWRITE_TAC [ELIM_UNCURRY] THEN BETA_TAC THEN 392 MATCH_ACCEPT_TAC (GSYM ELIM_PFORALL)); 393 394(* ------------------------------------------------------------------------- *) 395(* PEXISTS_THM = |- !P. (?x y. P x y) = (?(x,y). P x y) *) 396(* ------------------------------------------------------------------------- *) 397 398val PEXISTS_THM = Q.store_thm 399("PEXISTS_THM", 400 `!P:'a -> 'b -> bool. (?x y. P x y) = ?(x,y). P x y`, 401 REWRITE_TAC [ELIM_UNCURRY] THEN BETA_TAC THEN 402 MATCH_ACCEPT_TAC (GSYM ELIM_PEXISTS)); 403 404 405(* ------------------------------------------------------------------------- *) 406(* Rewrite versions of ELIM_PEXISTS and ELIM_PFORALL *) 407(* ------------------------------------------------------------------------- *) 408 409val ELIM_PEXISTS_EVAL = Q.store_thm 410("ELIM_PEXISTS_EVAL", 411 `$? (UNCURRY (\x. P x)) = ?x. $? (P x)`, 412 Q.SUBGOAL_THEN `!x. P x = \y. P x y` (fn th => ONCE_REWRITE_TAC [th]) THEN 413 REWRITE_TAC [ETA_THM, PEXISTS_THM]); 414 415val ELIM_PFORALL_EVAL = Q.store_thm 416("ELIM_PFORALL_EVAL", 417 `$! (UNCURRY (\x. P x)) = !x. $! (P x)`, 418 Q.SUBGOAL_THEN `!x. P x = \y. P x y` (fn th => ONCE_REWRITE_TAC [th]) THEN 419 REWRITE_TAC [ETA_THM, PFORALL_THM]); 420 421(*--------------------------------------------------------------------------- 422 Map for pairs 423 ---------------------------------------------------------------------------*) 424 425val PAIR_MAP = Q.new_infixr_definition 426 ("PAIR_MAP", 427 `$## (f:'a->'c) (g:'b->'d) p = (f (FST p), g (SND p))`, 490); 428 429val PAIR_MAP_THM = Q.store_thm 430("PAIR_MAP_THM", 431 `!f g x y. (f##g) (x,y) = (f x, g y)`, 432 REWRITE_TAC [PAIR_MAP,FST,SND]); 433 434val FST_PAIR_MAP = store_thm( 435 "FST_PAIR_MAP", 436 ``!p f g. FST ((f ## g) p) = f (FST p)``, 437 REWRITE_TAC [PAIR_MAP, FST]); 438 439val SND_PAIR_MAP = store_thm( 440 "SND_PAIR_MAP", 441 ``!p f g. SND ((f ## g) p) = g (SND p)``, 442 REWRITE_TAC [PAIR_MAP, SND]); 443 444(*--------------------------------------------------------------------------- 445 Distribution laws for paired lets. Only will work for the 446 exact form given. See also boolTheory. 447 ---------------------------------------------------------------------------*) 448 449val LET2_RAND = Q.store_thm("LET2_RAND", 450`!(P:'c->'d) (M:'a#'b) N. 451 P (let (x,y) = M in N x y) = (let (x,y) = M in P (N x y))`, 452REWRITE_TAC[boolTheory.LET_DEF] THEN REPEAT GEN_TAC THEN BETA_TAC 453 THEN REPEAT_TCL CHOOSE_THEN SUBST_ALL_TAC 454 (SPEC (Term `M:'a#'b`) ABS_PAIR_THM) 455 THEN REWRITE_TAC[UNCURRY_DEF] THEN BETA_TAC THEN REFL_TAC); 456 457val LET2_RATOR = Q.store_thm("LET2_RATOR", 458`!(M:'a1#'a2) (N:'a1->'a2->'b->'c) (b:'b). 459 (let (x,y) = M in N x y) b = let (x,y) = M in N x y b`, 460REWRITE_TAC [boolTheory.LET_DEF] THEN BETA_TAC 461 THEN REWRITE_TAC [UNCURRY_VAR] THEN BETA_TAC 462 THEN REWRITE_TAC[]); 463 464open BasicProvers 465 466val o_UNCURRY_R = store_thm( 467 "o_UNCURRY_R", 468 ``f o UNCURRY g = UNCURRY ((o) f o g)``, 469 SRW_TAC [][FUN_EQ_THM, UNCURRY]); 470 471val C_UNCURRY_L = store_thm( 472 "C_UNCURRY_L", 473 ``combin$C (UNCURRY f) x = UNCURRY (combin$C (combin$C o f) x)``, 474 SRW_TAC [][FUN_EQ_THM, UNCURRY]); 475 476val S_UNCURRY_R = store_thm( 477 "S_UNCURRY_R", 478 ``S f (UNCURRY g) = UNCURRY (S (S o ((o) f) o (,)) g)``, 479 SRW_TAC [][FUN_EQ_THM, UNCURRY, PAIR]); 480 481val UNCURRY' = prove( 482 ``UNCURRY f = \p. f (FST p) (SND p)``, 483 SRW_TAC [][FUN_EQ_THM, UNCURRY]); 484 485val FORALL_UNCURRY = store_thm( 486 "FORALL_UNCURRY", 487 ``(!) (UNCURRY f) = (!) ((!) o f)``, 488 SRW_TAC [][UNCURRY', combinTheory.o_DEF] THEN 489 Q.SUBGOAL_THEN `!x. f x = \y. f x y` (fn th => ONCE_REWRITE_TAC [th]) THENL [ 490 REWRITE_TAC [FUN_EQ_THM] THEN BETA_TAC THEN REWRITE_TAC [], 491 ALL_TAC 492 ] THEN 493 SRW_TAC [][FORALL_PROD, FST, SND]); 494 495(* --------------------------------------------------------------------- *) 496(* A nice theorem from Tom Melham, lifted from examples/lambda/ncScript *) 497(* States ability to express a function: *) 498(* *) 499(* h : A -> B x C *) 500(* *) 501(* as the combination h = <f,g> of two component functions *) 502(* *) 503(* f : A -> B and g : A -> C *) 504(* *) 505(* --------------------------------------------------------------------- *) 506 507val PAIR_FUN_THM = Q.store_thm 508("PAIR_FUN_THM", 509 `!P. (?!f:'a->('b#'c). P f) = 510 (?!p:('a->'b)#('a->'c). P(\a.(FST p a, SND p a)))`, 511RW_TAC bool_ss [EXISTS_UNIQUE_THM] 512 THEN EQ_TAC THEN RW_TAC bool_ss [] 513 THENL 514 [Q.EXISTS_TAC `FST o f, SND o f` 515 THEN RW_TAC bool_ss [FST,SND,combinTheory.o_THM,PAIR,ETA_THM], 516 STRIP_ASSUME_TAC (Q.ISPEC `p:('a -> 'b) # ('a -> 'c)` ABS_PAIR_THM) THEN 517 STRIP_ASSUME_TAC (Q.ISPEC `p':('a -> 'b) # ('a -> 'c)` ABS_PAIR_THM) 518 THEN RW_TAC bool_ss [] 519 THEN RULE_ASSUM_TAC (REWRITE_RULE [FST,SND]) 520 THEN ``(\a:'a. (q a:'b,r a:'c)) = (\a:'a. (q' a:'b,r' a:'c))`` via RES_TAC 521 THEN simpLib.FULL_SIMP_TAC bool_ss [FUN_EQ_THM,PAIR_EQ], 522 PROVE_TAC[], 523 Q.PAT_ASSUM `$! M` 524 (MP_TAC o Q.SPECL [`(FST o f, SND o f)`, `(FST o y, SND o y)`]) 525 THEN RW_TAC bool_ss [FST,SND,combinTheory.o_THM, 526 PAIR,PAIR_EQ,FUN_EQ_THM,ETA_THM] 527 THEN PROVE_TAC [PAIR_EQ,PAIR]]); 528 529 530(*--------------------------------------------------------------------------- 531 TFL support. 532 ---------------------------------------------------------------------------*) 533 534val pair_CASE_def = 535 new_definition("pair_CASE_def", Term`pair_CASE p f = f (FST p) (SND p)`) 536val _ = ot0 "pair_case" "case" 537 538val pair_case_thm = save_thm("pair_case_thm", 539 pair_CASE_def |> Q.SPEC `(x,y)` |> REWRITE_RULE [FST, SND] |> SPEC_ALL) 540 541(* and, to be consistent with what would be generated if we could use 542 Hol_datatype to generate the pair type: *) 543val pair_case_def = save_thm("pair_case_def", pair_case_thm) 544val _ = overload_on("case", ``pair_CASE``) 545 546 547val pair_case_cong = save_thm("pair_case_cong", 548 Prim_rec.case_cong_thm pair_CASES pair_case_thm); 549val pair_rws = [PAIR, FST, SND]; 550 551val pair_case_eq = Q.store_thm( 552 "pair_case_eq", 553 ���(pair_CASE p f = v) <=> ?x y. (p = (x,y)) /\ (f x y = v)���, 554 Q.ISPEC_THEN ���p��� STRUCT_CASES_TAC pair_CASES THEN 555 SRW_TAC[][pair_CASE_def, FST, SND, PAIR_EQ]); 556 557val _ = TypeBase.export [ 558 TypeBasePure.mk_datatype_info_no_simpls { 559 ax=TypeBasePure.ORIG pair_Axiom, 560 case_def=pair_case_thm, 561 case_cong=pair_case_cong, 562 case_eq = pair_case_eq, 563 induction=TypeBasePure.ORIG pair_induction, 564 nchotomy=ABS_PAIR_THM, 565 size=NONE, 566 encode=NONE, 567 fields=[], 568 accessors=[], 569 updates=[], 570 destructors=[FST,SND], 571 recognizers=[], 572 lift=SOME(mk_var("pairSyntax.lift_prod", 573 ���:'type -> ('a -> 'term) -> ('b -> 'term) -> 'a # 'b -> 574 'term���)), 575 one_one=SOME CLOSED_PAIR_EQ, 576 distinct=NONE 577 } 578 ]; 579 580(*--------------------------------------------------------------------------- 581 Generate some ML that gets evaluated at theory load time. 582 583 The TFL definition package uses "pair_case" as a case construct, 584 rather than UNCURRY. This (apparently) solves a deeply buried 585 problem in termination condition extraction involving paired 586 beta-reduction. 587 588 ---------------------------------------------------------------------------*) 589 590 591 592val S = PP.add_string and NL = PP.NL and B = PP.block PP.CONSISTENT 0 593 594val _ = adjoin_to_theory 595{sig_ps = SOME(fn _ => S "val pair_rws : thm list"), 596 struct_ps = SOME(fn _ => S "val pair_rws = [PAIR, FST, SND];")}; 597 598val datatype_pair = store_thm( 599 "datatype_pair", 600 ``DATATYPE (pair ((,) : 'a -> 'b -> 'a # 'b))``, 601 REWRITE_TAC [DATATYPE_TAG_THM]); 602 603 604(*--------------------------------------------------------------------------- 605 Wellfoundedness and pairs. 606 ---------------------------------------------------------------------------*) 607 608 609(*--------------------------------------------------------------------------- 610 * The lexicographic combination of two wellfounded orderings is wellfounded. 611 * The minimal element of this relation is found by 612 * 613 * 1. Finding the set of first elements of the pairs in B 614 * 2. That set is non-empty, so it has an R-minimal element, call it min 615 * 3. Find the set of second elements of those pairs in B whose first 616 * element is min. 617 * 4. This set is non-empty, so it has a Q-minimal element, call it min'. 618 * 5. A minimal element is (min,min'). 619 *---------------------------------------------------------------------------*) 620 621val LEX_DEF = 622Q.new_infixr_definition 623("LEX_DEF", 624 `$LEX (R1:'a->'a->bool) (R2:'b->'b->bool) 625 = 626 \(s,t) (u,v). R1 s u \/ (s=u) /\ R2 t v`, 490); 627 628val LEX_DEF_THM = Q.store_thm 629("LEX_DEF_THM", 630 `(R1 LEX R2) (a,b) (c,d) = R1 a c \/ (a = c) /\ R2 b d`, 631 REWRITE_TAC [LEX_DEF,UNCURRY_DEF] THEN BETA_TAC THEN 632 REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC THEN REFL_TAC); 633 634val LEX_MONO = store_thm("LEX_MONO", 635 ``(!x y. R1 x y ==> R2 x y) /\ 636 (!x y. R3 x y ==> R4 x y) 637 ==> 638 (R1 LEX R3) x y ==> (R2 LEX R4) x y``, 639 STRIP_TAC THEN 640 Q.SPEC_THEN`x`FULL_STRUCT_CASES_TAC pair_CASES THEN 641 Q.SPEC_THEN`y`FULL_STRUCT_CASES_TAC pair_CASES THEN 642 SRW_TAC[][LEX_DEF_THM] THEN 643 PROVE_TAC[]) 644val () = IndDefLib.export_mono"LEX_MONO"; 645 646val WF_LEX = Q.store_thm("WF_LEX", 647 `!(R:'a->'a->bool) (Q:'b->'b->bool). WF R /\ WF Q ==> WF (R LEX Q)`, 648REWRITE_TAC [LEX_DEF, relationTheory.WF_DEF] 649 THEN CONV_TAC (DEPTH_CONV LEFT_IMP_EXISTS_CONV) 650 THEN REPEAT STRIP_TAC 651 THEN Q.SUBGOAL_THEN `?w1. (\v. ?y. B (v,y)) w1` STRIP_ASSUME_TAC THENL 652 [BETA_TAC THEN MAP_EVERY Q.EXISTS_TAC [`FST w`, `SND w`] 653 THEN ASM_REWRITE_TAC pair_rws, 654 Q.SUBGOAL_THEN 655 `?min. (\v. ?y. B (v,y)) min 656 /\ !b. R b min ==> 657 ~(\v. ?y. B (v,y)) b` STRIP_ASSUME_TAC THENL 658 [RES_TAC THEN ASM_MESON_TAC[], 659 Q.SUBGOAL_THEN 660 `?w2:'b. (\z. B (min:'a,z)) w2` STRIP_ASSUME_TAC THENL 661 [BETA_TAC THEN RULE_ASSUM_TAC BETA_RULE THEN ASM_REWRITE_TAC[], 662 Q.SUBGOAL_THEN 663 `?min':'b. (\z. B (min,z)) min' 664 /\ !b. Q b min' ==> 665 ~((\z. B (min,z)) b)` STRIP_ASSUME_TAC THENL 666 [RES_TAC THEN ASM_MESON_TAC[], 667 RULE_ASSUM_TAC BETA_RULE 668 THEN EXISTS_TAC (Term`(min:'a, (min':'b))`) 669 THEN ASM_REWRITE_TAC[] 670 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`b:'a#'b` PAIR)] 671 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC 672 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC 673 THEN ASM_MESON_TAC pair_rws]]]]); 674 675(*--------------------------------------------------------------------------- 676 * The relational product of two wellfounded relations is wellfounded. This 677 * is a consequence of WF_LEX. 678 *---------------------------------------------------------------------------*) 679 680val RPROD_DEF = 681Q.new_definition 682("RPROD_DEF", 683 `RPROD (R1:'a->'a->bool) 684 (R2:'b->'b->bool) = \(s,t) (u,v). R1 s u /\ R2 t v`); 685 686 687val WF_RPROD = 688Q.store_thm("WF_RPROD", 689 `!(R:'a->'a->bool) (Q:'b->'b->bool). WF R /\ WF Q ==> WF(RPROD R Q)`, 690REPEAT STRIP_TAC THEN MATCH_MP_TAC relationTheory.WF_SUBSET 691 THEN Q.EXISTS_TAC`R LEX Q` 692 THEN CONJ_TAC 693 THENL [MATCH_MP_TAC WF_LEX THEN ASM_REWRITE_TAC[], 694 REWRITE_TAC[LEX_DEF,RPROD_DEF] 695 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`x:'a#'b` PAIR)] 696 THEN GEN_TAC THEN SUBST_TAC [GSYM(Q.SPEC`y:'a#'b` PAIR)] 697 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC 698 THEN REWRITE_TAC [UNCURRY_DEF] THEN BETA_TAC 699 THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]]); 700 701(* more relational properties of LEX *) 702val total_LEX = store_thm( 703 "total_LEX", 704 ``total R1 /\ total R2 ==> total (R1 LEX R2)``, 705 ASM_SIMP_TAC (srw_ss()) [total_def, FORALL_PROD, LEX_DEF, UNCURRY_DEF] THEN 706 METIS_TAC[]); 707val _ = export_rewrites ["total_LEX"] 708 709val transitive_LEX = store_thm( 710 "transitive_LEX", 711 ``transitive R1 /\ transitive R2 ==> transitive (R1 LEX R2)``, 712 SIMP_TAC (srw_ss()) [transitive_def, FORALL_PROD, LEX_DEF, UNCURRY_DEF] THEN 713 METIS_TAC[]); 714val _ = export_rewrites ["transitive_LEX"] 715 716val reflexive_LEX = store_thm( 717 "reflexive_LEX", 718 ``reflexive (R1 LEX R2) <=> reflexive R1 \/ reflexive R2``, 719 SIMP_TAC (srw_ss()) [reflexive_def, LEX_DEF, FORALL_PROD, UNCURRY_DEF] THEN 720 METIS_TAC[]) 721val _ = export_rewrites ["reflexive_LEX"] 722 723val symmetric_LEX = store_thm( 724 "symmetric_LEX", 725 ``symmetric R1 /\ symmetric R2 ==> symmetric (R1 LEX R2)``, 726 SIMP_TAC (srw_ss()) [symmetric_def, LEX_DEF, FORALL_PROD, UNCURRY_DEF] THEN 727 METIS_TAC[]); 728val _ = export_rewrites ["symmetric_LEX"] 729 730val LEX_CONG = Q.store_thm 731("LEX_CONG", 732 `!R1 R2 v1 v2 R1' R2' v1' v2'. 733 (v1 = v1') /\ (v2 = v2') /\ 734 (!a b c d. (v1' = (a,b)) /\ (v2' = (c,d)) ==> (R1 a c = R1' a c)) /\ 735 (!a b c d. (v1' = (a,b)) /\ (v2' = (c,d)) /\ (a=c) ==> (R2 b d = R2' b d)) 736 ==> 737 ($LEX R1 R2 v1 v2 = $LEX R1' R2' v1' v2')`, 738 Ho_Rewrite.REWRITE_TAC [LEX_DEF,FORALL_PROD,PAIR_EQ] 739 THEN NTAC 2 (REWRITE_TAC [UNCURRY_VAR,FST,SND] THEN BETA_TAC) 740 THEN METIS_TAC[]); 741 742val _ = DefnBase.export_cong "LEX_CONG"; 743 744(*--------------------------------------------------------------------------- 745 Generate some ML that gets evaluated at theory load time. 746 It adds relevant rewrites into the global compset. 747 ---------------------------------------------------------------------------*) 748 749val _ = adjoin_to_theory 750{sig_ps = NONE, 751 struct_ps = SOME(fn _ => B[ 752 S "val _ = let open computeLib", NL, 753 S " in add_funs (map lazyfy_thm", NL, 754 S " [CLOSED_PAIR_EQ,FST,SND,pair_case_thm,SWAP_def,", NL, 755 S " CURRY_DEF,UNCURRY_DEF,PAIR_MAP_THM])", NL, 756 S " end;", NL])} 757 758(*--------------------------------------------------------------------------- 759 Some messiness in order to teach the definition principle about 760 varstructs. 761 ---------------------------------------------------------------------------*) 762 763val _ = adjoin_to_theory 764{sig_ps = SOME(fn _ => B[ 765 S "type hol_type = Abbrev.hol_type", NL, 766 S "type term = Abbrev.term", NL, 767 S "type conv = Abbrev.conv", NL,NL, 768 S "val uncurry_tm : term", NL, 769 S "val comma_tm : term", NL, 770 S "val dest_pair : term -> term * term", NL, 771 S "val strip_pair : term -> term list", NL, 772 S "val spine_pair : term -> term list", NL, 773 S "val is_vstruct : term -> bool", NL, 774 S "val mk_pabs : term * term -> term", NL, 775 S "val PAIRED_BETA_CONV : conv", NL]), 776 struct_ps = SOME(fn _ => B[ 777S"(*---------------------------------------------------------------", NL, 778S" Support for definitions using varstructs", NL, 779S"----------------------------------------------------------------*)", NL, 780NL, 781S "open HolKernel boolLib;", NL, 782S "infix |-> ORELSEC THENC;", NL, 783NL, 784S "val ERR1 = mk_HOL_ERR \"pairSyntax\"", NL, 785S "val ERR2 = mk_HOL_ERR \"PairedLambda\"", NL, 786S "val ERR3 = mk_HOL_ERR \"pairTheory.dest\"", NL, 787NL, 788S "val comma_tm = prim_mk_const {Name=\",\", Thy=\"pair\"};", NL, 789S "val uncurry_tm = prim_mk_const {Name=\"UNCURRY\", Thy=\"pair\"};", NL, 790NL, 791S "val dest_pair = dest_binop comma_tm (ERR1 \"dest_pair\" \"not a pair\")", NL, 792S "val strip_pair = strip_binop (total dest_pair);", NL, 793S "val spine_pair = spine_binop (total dest_pair);", NL, 794NL, 795S "local fun check [] = true", NL, 796S " | check (h::t) = is_var h andalso not(mem h t) andalso check t", NL, 797S "in", NL, 798S "fun is_vstruct M = check (strip_pair M)", 799S "end;", NL, 800NL, 801S "fun mk_uncurry_tm(xt,yt,zt) = ", NL, 802S " inst [alpha |-> xt, beta |-> yt, gamma |-> zt] uncurry_tm;", NL, 803NL, 804NL, 805S "fun mk_pabs(vstruct,body) =", NL, 806S " if is_var vstruct then Term.mk_abs(vstruct, body)", NL, 807S " else let val (fst,snd) = dest_pair vstruct", NL, 808S " in mk_comb(mk_uncurry_tm(type_of fst, type_of snd, type_of body),", NL, 809S " mk_pabs(fst,mk_pabs(snd,body)))", NL, 810S " end handle HOL_ERR _ => raise ERR1 \"mk_pabs\" \"\";", NL, 811NL, 812NL, 813S "local val vs = map genvar [alpha --> beta --> gamma, alpha, beta]", NL, 814S " val DEF = SPECL vs UNCURRY_DEF", NL, 815S " val RBCONV = RATOR_CONV BETA_CONV THENC BETA_CONV", NL, 816S " fun conv tm = ", NL, 817S " let val (Rator,Rand) = dest_comb tm", NL, 818S " val (fst,snd) = dest_pair Rand", NL, 819S " val (Rator,f) = dest_comb Rator", NL, 820S " val _ = assert (same_const uncurry_tm) Rator", NL, 821S " val (t1,ty') = dom_rng (type_of f)", NL, 822S " val (t2,t3) = dom_rng ty'", NL, 823S " val iDEF = INST_TYPE [alpha |-> t1, beta |-> t2, gamma |-> t3] DEF", NL, 824S " val (fv,xyv) = strip_comb(rand(concl iDEF))", NL, 825S " val xv = hd xyv and yv = hd (tl xyv)", NL, 826S " val def = INST [yv |-> snd, xv |-> fst, fv |-> f] iDEF", NL, 827S " in", NL, 828S " TRANS def ", NL, 829S " (if Term.is_abs f ", NL, 830S " then if Term.is_abs (body f) ", NL, 831S " then RBCONV (rhs(concl def))", NL, 832S " else CONV_RULE (RAND_CONV conv)", NL, 833S " (AP_THM(BETA_CONV(mk_comb(f, fst))) snd)", NL, 834S " else let val recc = conv (rator(rand(concl def)))", NL, 835S " in if Term.is_abs (rhs(concl recc))", NL, 836S " then RIGHT_BETA (AP_THM recc snd)", NL, 837S " else TRANS (AP_THM recc snd) ", NL, 838S " (conv(mk_comb(rhs(concl recc), snd)))", NL, 839S " end)", NL, 840S " end", NL, 841S "in", NL, 842S "fun PAIRED_BETA_CONV tm ", NL, 843S " = conv tm handle HOL_ERR _ => raise ERR2 \"PAIRED_BETA_CONV\" \"\"", NL, 844S "end;", NL, 845NL, 846NL, 847S "(*---------------------------------------------------------------------------", NL, 848S " Lifting primitive definition principle to understand varstruct", NL, 849S " arguments in definitions.", NL, 850S " ---------------------------------------------------------------------------*)", NL, 851NL, 852S "fun inter s1 [] = []", NL, 853S " | inter s1 (h::t) = case intersect s1 h of [] => inter s1 t | X => X", NL, 854NL, 855S "fun joint_vars [] = []", NL, 856S " | joint_vars [_] = []", NL, 857S " | joint_vars (h::t) = case inter h t of [] => joint_vars t | X => X;", NL, 858NL, 859S "fun dest t = ", NL, 860S " let val (lhs,rhs) = dest_eq (snd(strip_forall t))", NL, 861S " val (f,args) = strip_comb lhs", NL, 862S " val f = mk_var(dest_const f) handle HOL_ERR _ => f", NL, 863S " in ", NL, 864S " case filter (not o is_vstruct) args ", NL, 865S " of [] => (case joint_vars (map free_vars args)", NL, 866S " of [] => (args, mk_eq(f,itlist (curry mk_pabs) args rhs))", NL, 867S " | V => raise ERR3 \"new_definition\" (String.concat", NL, 868S " (\"shared variables between arguments: \" ::", NL, 869S " commafy (map Parse.term_to_string V))))", NL, 870S " | tml => raise ERR3 \"new_definition\" (String.concat", NL, 871S " (\"The following arguments are not varstructs: \"::", NL, 872S " commafy (map Parse.term_to_string tml)))", NL, 873S " end;", NL, 874NL, 875S "fun RHS_CONV conv th = TRANS th (conv(rhs(concl th)));", NL, 876NL, 877S "fun add_varstruct v th = ", NL, 878S " RHS_CONV(BETA_CONV ORELSEC PAIRED_BETA_CONV) (AP_THM th v)", NL, 879NL, 880S "fun post (V,th) =", NL, 881S " let val vars = List.concat (map free_vars_lr V)", NL, 882S " in", NL, 883S " itlist GEN vars (rev_itlist add_varstruct V th)", NL, 884S " end;", NL, 885S " ", NL, 886S "val _ = Definition.new_definition_hook := (dest, post)", NL])}; 887 888val _ = BasicProvers.export_rewrites 889 ["PAIR", "FST", "SND", "CLOSED_PAIR_EQ", "CURRY_UNCURRY_THM", 890 "UNCURRY_CURRY_THM", "CURRY_ONE_ONE_THM", "UNCURRY_ONE_ONE_THM", 891 "UNCURRY_DEF", "CURRY_DEF", "PAIR_MAP_THM", "FST_PAIR_MAP", 892 "SND_PAIR_MAP"] 893 894val FST_EQ_EQUIV = Q.store_thm("FST_EQ_EQUIV", 895 `(FST p = x) <=> ?y. p = (x,y)`, 896 Q.ISPEC_THEN `p` STRUCT_CASES_TAC pair_CASES >> simp_tac(srw_ss())[]); 897val SND_EQ_EQUIV = Q.store_thm("SND_EQ_EQUIV", 898 ���(SND p = y) <=> ?x. p = (x,y)���, 899 Q.ISPEC_THEN `p` STRUCT_CASES_TAC pair_CASES >> simp_tac(srw_ss())[]); 900 901 902 903val comma_tm = Term.prim_mk_const{Name=",", Thy="pair"}; 904fun is_pair tm = Term.same_const comma_tm (fst(strip_comb tm)); 905fun dest_pair tm = 906 case snd (strip_comb tm) of [a,b] => (a,b) | _ => raise Match; 907 908val _ = adjoin_to_theory 909{sig_ps = NONE, 910 struct_ps = SOME(fn _ => 911 S "val _ = BasicProvers.new_let_thms\ 912 \[o_UNCURRY_R, C_UNCURRY_L, S_UNCURRY_R, \ 913 \FORALL_UNCURRY]")} 914 915val _ = export_theory(); 916 917val _ = export_theory_as_docfiles "pair-help/thms" 918