1open HolKernel Parse boolLib Drule BasicProvers 2 pairTheory listTheory optionTheory metisLib simpLib 3 boolSimps pureSimps TotalDefn numLib ConseqConv 4 5val _ = new_theory "quantHeuristics"; 6 7(* 8quietdec := false; 9*) 10 11val list_ss = arith_ss ++ listSimps.LIST_ss 12 13val GUESS_EXISTS_def = Define ` 14 GUESS_EXISTS i P = ((?v. P v) = (?fv. P (i fv)))` 15 16val GUESS_FORALL_def = Define ` 17 GUESS_FORALL i P = ((!v. P v) = (!fv. P (i fv)))` 18 19val GUESS_EXISTS_FORALL_REWRITES = store_thm ("GUESS_EXISTS_FORALL_REWRITES", 20``(GUESS_EXISTS i P = (!v. P v ==> (?fv. P (i fv)))) /\ 21 (GUESS_FORALL i P = (!v. ~(P v) ==> (?fv. ~(P (i fv)))))``, 22SIMP_TAC std_ss [GUESS_EXISTS_def, GUESS_FORALL_def] THEN 23METIS_TAC[]); 24 25 26val GUESS_EXISTS_POINT_def = Define ` 27 GUESS_EXISTS_POINT i P = (!fv. P (i fv))` 28 29val GUESS_FORALL_POINT_def = Define ` 30 GUESS_FORALL_POINT i P = (!fv. ~(P (i fv)))` 31 32val GUESS_POINT_THM = store_thm ("GUESS_POINT_THM", 33``(GUESS_EXISTS_POINT i P ==> ((?v. P v) = T)) /\ 34 (GUESS_FORALL_POINT i P ==> ((!v. P v) = F))``, 35SIMP_TAC std_ss [GUESS_EXISTS_POINT_def, GUESS_FORALL_POINT_def] THEN 36METIS_TAC[]); 37 38 39val GUESS_EXISTS_GAP_def = Define ` 40 GUESS_EXISTS_GAP i P = 41 (!v. P v ==> (?fv. v = (i fv)))`; 42 43val GUESS_FORALL_GAP_def = Define ` 44 GUESS_FORALL_GAP i P = 45 (!v. ~(P v) ==> (?fv. v = (i fv)))`; 46 47 48val GUESS_REWRITES = save_thm ("GUESS_REWRITES", 49 LIST_CONJ [GUESS_EXISTS_FORALL_REWRITES, GUESS_EXISTS_POINT_def, GUESS_FORALL_POINT_def, 50 GUESS_EXISTS_GAP_def, GUESS_FORALL_GAP_def]); 51 52 53 54 55(******************************************************************************) 56(* Now the intended semantic *) 57(******************************************************************************) 58 59val GUESS_EXISTS_POINT_THM = store_thm ("GUESS_EXISTS_POINT_THM", 60``!i P. GUESS_EXISTS_POINT i P ==> ($? P = T)``, 61SIMP_TAC std_ss [GUESS_EXISTS_POINT_def, EXISTS_THM] THEN 62METIS_TAC[]); 63 64val GUESS_FORALL_POINT_THM = store_thm ("GUESS_FORALL_POINT_THM", 65``!i P. GUESS_FORALL_POINT i P ==> (($! P) = F)``, 66SIMP_TAC std_ss [GUESS_REWRITES, FORALL_THM] THEN 67METIS_TAC[]); 68 69val GUESS_EXISTS_THM = store_thm ("GUESS_EXISTS_THM", 70``!i P. GUESS_EXISTS i P ==> ($? P = ?fv. P (i fv))``, 71SIMP_TAC std_ss [GUESS_REWRITES, EXISTS_THM] THEN 72METIS_TAC[]); 73 74val GUESS_FORALL_THM = store_thm ("GUESS_FORALL_THM", 75``!i P. GUESS_FORALL i P ==> (($! P) = !fv. P (i fv))``, 76SIMP_TAC std_ss [GUESS_REWRITES, FORALL_THM] THEN 77METIS_TAC[]); 78 79 80val GUESSES_UEXISTS_THM1 = store_thm("GUESSES_UEXISTS_THM1", 81``!i P. GUESS_EXISTS (\x. i) P ==> 82 ($?! P = ((P i) /\ (!v. P v ==> (v = i))))``, 83SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 84METIS_TAC[]); 85 86val GUESSES_UEXISTS_THM2 = store_thm("GUESSES_UEXISTS_THM2", 87``!i P. GUESS_EXISTS_GAP (\x. i) P ==> ($?! P = P i)``, 88SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 89METIS_TAC[]); 90 91val GUESSES_UEXISTS_THM3 = store_thm("GUESSES_UEXISTS_THM3", 92``!i P. GUESS_EXISTS_POINT (\x. i) P ==> 93 ($?! P = (!v. P v ==> (v = i)))``, 94SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 95METIS_TAC[]); 96 97val GUESSES_UEXISTS_THM4 = store_thm("GUESSES_UEXISTS_THM4", 98``!i P. GUESS_EXISTS_POINT (\x. i) P ==> GUESS_EXISTS_GAP (\x. i) P ==> 99 ($?! P = T)``, 100SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 101METIS_TAC[]); 102 103 104val GUESSES_NEG_DUALITY = store_thm ("GUESSES_NEG_DUALITY", 105``(GUESS_EXISTS i ($~ o P) = 106 GUESS_FORALL i P) /\ 107 108 (GUESS_FORALL i ($~ o P) = 109 GUESS_EXISTS i P) /\ 110 111 (GUESS_EXISTS_GAP i ($~ o P) = 112 GUESS_FORALL_GAP i P) /\ 113 114 (GUESS_FORALL_GAP i ($~ o P) = 115 GUESS_EXISTS_GAP i P) /\ 116 117 (GUESS_EXISTS_POINT i ($~ o P) = 118 GUESS_FORALL_POINT i P) /\ 119 120 (GUESS_FORALL_POINT i ($~ o P) = 121 GUESS_EXISTS_POINT i P)``, 122 123SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.o_DEF]); 124 125 126val GUESSES_NEG_REWRITE = save_thm ("GUESSES_NEG_REWRITE", 127SIMP_RULE std_ss [combinTheory.o_DEF] 128 (INST [``P:'b -> bool`` |-> ``\x:'b. (P x):bool``] GUESSES_NEG_DUALITY)); 129 130 131val GUESSES_WEAKEN_THM = store_thm ("GUESSES_WEAKEN_THM", 132``(GUESS_FORALL_GAP i P ==> GUESS_FORALL i P) /\ 133 (GUESS_FORALL_POINT i P ==> GUESS_FORALL i P) /\ 134 (GUESS_EXISTS_POINT i P ==> GUESS_EXISTS i P) /\ 135 (GUESS_EXISTS_GAP i P ==> GUESS_EXISTS i P)``, 136 137SIMP_TAC std_ss [GUESS_REWRITES] THEN 138METIS_TAC[]); 139 140 141 142(******************************************************************************) 143(* Equations *) 144(******************************************************************************) 145 146val GUESS_RULES_EQUATION_EXISTS_POINT = store_thm ("GUESS_RULES_EQUATION_EXISTS_POINT", 147``!i P Q. 148 (P i = Q i) ==> 149 GUESS_EXISTS_POINT (\xxx:unit. i) (\x. P x = Q x)``, 150SIMP_TAC std_ss [GUESS_REWRITES]); 151 152val GUESS_RULES_EQUATION_FORALL_POINT = store_thm ("GUESS_RULES_EQUATION_FORALL_POINT", 153``!i P Q. 154 (!fv. ~(P (i fv) = Q (i fv))) ==> 155 GUESS_FORALL_POINT i (\x. P x = Q x)``, 156SIMP_TAC std_ss [GUESS_REWRITES]); 157 158val GUESS_RULES_EQUATION_EXISTS_GAP = store_thm ("GUESS_RULES_EQUATION_EXISTS_GAP", 159``!i. 160 GUESS_EXISTS_GAP (\xxx:unit. i) (\x. x = i)``, 161SIMP_TAC std_ss [GUESS_REWRITES] THEN 162METIS_TAC[]); 163 164(******************************************************************************) 165(* Trivial point guesses *) 166(******************************************************************************) 167 168val GUESS_RULES_TRIVIAL_EXISTS_POINT = store_thm ("GUESS_RULES_TRIVIAL_EXISTS_POINT", 169``!i P. P i ==> 170 GUESS_EXISTS_POINT (\xxx:unit. i) P``, 171SIMP_TAC std_ss [GUESS_REWRITES]); 172 173val GUESS_RULES_TRIVIAL_FORALL_POINT = store_thm ("GUESS_RULES_TRIVIAL_FORALL_POINT", 174``!i P. ~(P i) ==> 175 GUESS_FORALL_POINT (\xxx:unit. i) P``, 176SIMP_TAC std_ss [GUESS_REWRITES]); 177 178(******************************************************************************) 179(* Trivial booleans *) 180(******************************************************************************) 181 182val GUESS_RULES_BOOL = store_thm ("GUESS_RULES_BOOL", 183``GUESS_EXISTS_POINT (\ARB:unit. T) (\x. x) /\ 184 GUESS_FORALL_POINT (\ARB:unit. F) (\x. x) /\ 185 GUESS_EXISTS_GAP (\ARB:unit. T) (\x. x) /\ 186 GUESS_FORALL_GAP (\ARB:unit. F) (\x. x)``, 187SIMP_TAC std_ss [GUESS_REWRITES]); 188 189 190 191(******************************************************************************) 192(* Cases *) 193(******************************************************************************) 194 195val GUESS_RULES_TWO_CASES = store_thm ("GUESS_RULES_TWO_CASES", 196``!y Q. ((!x. ((x = y) \/ (?fv. x = Q fv)))) ==> 197 GUESS_FORALL_GAP Q (\x. x = y)``, 198SIMP_TAC std_ss [GUESS_REWRITES] THEN 199METIS_TAC[]); 200 201val GUESS_RULES_ONE_CASE___FORALL_GAP = store_thm ("GUESS_RULES_ONE_CASE___FORALL_GAP", 202``!P Q. ((!x:'a. (?fv. x = Q fv))) ==> 203 GUESS_FORALL_GAP Q (P:'a -> bool)``, 204SIMP_TAC std_ss [GUESS_REWRITES]); 205 206val GUESS_RULES_ONE_CASE___EXISTS_GAP = store_thm ("GUESS_RULES_ONE_CASE___EXISTS_GAP", 207``!P Q. ((!x:'a. (?fv. x = Q fv))) ==> 208 GUESS_EXISTS_GAP Q (P:'a -> bool)``, 209SIMP_TAC std_ss [GUESS_REWRITES]); 210 211 212(******************************************************************************) 213(* Boolean operators *) 214(******************************************************************************) 215 216val GUESS_RULES_NEG = store_thm ("GUESS_RULES_NEG", 217``(GUESS_EXISTS i (\x. P x) ==> 218 GUESS_FORALL i (\x. ~(P x))) /\ 219 220 (GUESS_EXISTS_GAP i (\x. P x) ==> 221 GUESS_FORALL_GAP i (\x. ~(P x))) /\ 222 223 (GUESS_EXISTS_POINT i (\x. P x) ==> 224 GUESS_FORALL_POINT i (\x. ~(P x))) /\ 225 226 (GUESS_FORALL i (\x. P x) ==> 227 GUESS_EXISTS i (\x. ~(P x))) /\ 228 229 (GUESS_FORALL_GAP i (\x. P x) ==> 230 GUESS_EXISTS_GAP i (\x. ~(P x))) /\ 231 232 (GUESS_FORALL_POINT i (\x. P x) ==> 233 GUESS_EXISTS_POINT i (\x. ~(P x)))``, 234 235SIMP_TAC std_ss [GUESSES_NEG_REWRITE]); 236 237 238val GUESS_RULES_CONSTANT_EXISTS = store_thm ("GUESS_RULES_CONSTANT_EXISTS", 239``(GUESS_EXISTS i (\x. p)) = T``, 240SIMP_TAC std_ss [GUESS_REWRITES]); 241 242val GUESS_RULES_CONSTANT_FORALL = store_thm ("GUESS_RULES_CONSTANT_FORALL", 243``(GUESS_FORALL i (\x. p)) = T``, 244SIMP_TAC std_ss [GUESS_REWRITES]); 245 246val GUESS_RULES_DISJ = store_thm ("GUESS_RULES_DISJ", 247``(GUESS_EXISTS_POINT i (\x. P x) ==> 248 GUESS_EXISTS_POINT i (\x. P x \/ Q x)) /\ 249 250 (GUESS_EXISTS_POINT i (\x. Q x) ==> 251 GUESS_EXISTS_POINT i (\x. P x \/ Q x)) /\ 252 253 (GUESS_EXISTS i (\x. P x) /\ 254 GUESS_EXISTS i (\x. Q x) ==> 255 GUESS_EXISTS i (\x. P x \/ Q x)) /\ 256 257 (* Not needed because of GUESS_RULES_CONSTANT_EXISTS, GUESS_RULES_CONSTANT_FORALL 258 (GUESS_EXISTS i (\x. P x) ==> 259 GUESS_EXISTS i (\x. P x \/ q)) /\ 260 261 (GUESS_EXISTS i (\x. Q x) ==> 262 GUESS_EXISTS i (\x. p \/ Q x)) /\ *) 263 264 (GUESS_EXISTS_GAP i (\x. P x) /\ 265 GUESS_EXISTS_GAP i (\x. Q x) ==> 266 GUESS_EXISTS_GAP i (\x. P x \/ Q x)) /\ 267 268 (GUESS_FORALL (\xxx:unit. iK) (\x. P x) /\ 269 GUESS_FORALL (\xxx:unit. iK) (\x. Q x) ==> 270 GUESS_FORALL (\xxx:unit. iK) (\x. P x \/ Q x)) /\ 271 272 (GUESS_FORALL i (\x. P x) ==> 273 GUESS_FORALL i (\x. P x \/ q)) /\ 274 275 (GUESS_FORALL i (\x. Q x) ==> 276 GUESS_FORALL i (\x. p \/ Q x)) /\ 277 278 (GUESS_FORALL_POINT i (\x. P x) /\ 279 GUESS_FORALL_POINT i (\x. Q x) ==> 280 GUESS_FORALL_POINT i (\x. P x \/ Q x)) /\ 281 282 (GUESS_FORALL_GAP i (\x. P x) ==> 283 GUESS_FORALL_GAP i (\x. P x \/ Q x)) /\ 284 285 (GUESS_FORALL_GAP i (\x. Q x) ==> 286 GUESS_FORALL_GAP i (\x. P x \/ Q x))``, 287 288SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 289METIS_TAC[]); 290 291 292 293val GUESS_RULES_CONJ = save_thm ("GUESS_RULES_CONJ", 294let 295 val thm0 = INST [ 296 ``P:'b->bool`` |-> ``$~ o (P:'b->bool)``, 297 ``Q:'b->bool`` |-> ``$~ o (Q:'b->bool)``, 298 ``p:bool`` |-> ``~p``, 299 ``q:bool`` |-> ``~q``] GUESS_RULES_DISJ 300 val thm1 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm0 301 val thm2 = REWRITE_RULE [GSYM DE_MORGAN_THM] thm1 302 val thm3 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm2 303in 304 thm3 305end); 306 307 308 309val GUESS_RULES_IMP = save_thm ("GUESS_RULES_IMP", 310let 311 val thm0 = INST [ 312 ``P:'b->bool`` |-> ``$~ o (P:'b->bool)``, 313 ``p:bool`` |-> ``~p``] GUESS_RULES_DISJ 314 val thm1 = SIMP_RULE std_ss [GUESSES_NEG_REWRITE] thm0 315 val thm2 = REWRITE_RULE [GSYM IMP_DISJ_THM] thm1 316in 317 thm2 318end); 319 320 321(* 322 323Code for generating theorems with rewriting using the basic ones. 324This is used for comming up with ideas for the lemma for 325COND and EXISTS_UNIQUE 326 327 328local 329 330(* 331val thmL = [GUESS_RULES_NEG, GUESS_RULES_DISJ, GUESS_RULES_CONJ, 332 GUESS_RULES_IMP, GUESSES_RULES_CONSTANT_EXISTS, 333 GUESSES_RULES_CONSTANT_FORALL, ELIM_UNLICKLY_THM] 334 335val tmL = [``\x:'a. P x <=> Q x``, ``\x. p <=> Q x``, ``\x. P x <=> q``] 336val rewr = [EQ_EXPAND] 337val tm = hd tmL 338 339val currentL = prepare_org_thms rewr tmL 340val ruleL = prepare_rules thmL 341*) 342 343val ELIM_UNLICKLY_THM = prove( 344``(F ==> GUESS_EXISTS_POINT i (\x. p)) /\ 345 (F ==> GUESS_FORALL_POINT i (\x. p)) /\ 346 (F ==> GUESS_EXISTS_GAP i (\x. p)) /\ 347 (F ==> GUESS_FORALL_GAP i (\x. p))``, 348SIMP_TAC std_ss []) 349 350 351fun prepare_org_thms rewr tmL = 352let 353 val thmL0 = map (fn t => REWRITE_CONV rewr t handle UNCHANGED => REFL t) tmL 354 fun mk_guess_terms tm = 355 ([``GUESS_EXISTS_POINT (i:'b -> 'a) ^tm``, 356 ``GUESS_FORALL_POINT (i:'b -> 'a) ^tm``, 357 ``GUESS_EXISTS (i:'b -> 'a) ^tm``, 358 ``GUESS_FORALL (i:'b -> 'a) ^tm``, 359 ``GUESS_EXISTS_GAP (i:'b -> 'a) ^tm``, 360 ``GUESS_FORALL_GAP (i:'b -> 'a) ^tm``], 361 [``GUESS_EXISTS_POINT (K (iK:'a)) ^tm``, 362 ``GUESS_FORALL_POINT (K (iK:'a)) ^tm``, 363 ``GUESS_EXISTS (K (iK:'a)) ^tm``, 364 ``GUESS_FORALL (K (iK:'a)) ^tm``, 365 ``GUESS_EXISTS_GAP (K (iK:'a)) ^tm``, 366 ``GUESS_FORALL_GAP (K (iK:'a)) ^tm``]) 367 368 fun basic_thms Pthm = 369 let 370 val (xtmL1, xtmL2) = mk_guess_terms (rhs (concl Pthm)); 371 val xthmL1 = map ConseqConv.REFL_CONSEQ_CONV xtmL1; 372 val xthmL2 = map ConseqConv.REFL_CONSEQ_CONV xtmL2; 373 val Pthm' = GSYM Pthm; 374 val xthmL1' = map (CONV_RULE (RAND_CONV (RAND_CONV (K Pthm')))) xthmL1 375 val xthmL2' = map (CONV_RULE (RAND_CONV (RAND_CONV (K Pthm')))) xthmL2 376 in 377 (xthmL1', xthmL2') 378 end; 379 380 val (thmL1, thmL2) = unzip (map basic_thms thmL0); 381in 382 (flatten thmL1, flatten thmL2) 383end; 384 385 386fun prepare_rules thmL = 387 let 388 val thmL' = flatten (map BODY_CONJUNCTS thmL); 389 in 390 map (fn thm => fn thm2 => SOME (ConseqConv.STRENGTHEN_CONSEQ_CONV_RULE 391 (ConseqConv.CONSEQ_HO_REWRITE_CONV ([],[thm],[])) thm2) handle UNCHANGED => NONE) thmL' 392 end 393 394 395fun mapPartial f = ((map valOf) o (filter isSome) o (map f)); 396 397fun apply_rules ruleL doneL [] = doneL 398 | apply_rules ruleL doneL (thm::currentL) = 399 let 400 val xthmL = mapPartial (fn r => r thm) ruleL; 401 in 402 if null xthmL then apply_rules ruleL (thm::doneL) currentL 403 else apply_rules ruleL doneL (xthmL @ currentL) 404 end; 405 406in 407 fun test_rules thmL rewr tmL = 408 let 409 val (currentL1, currentL2) = prepare_org_thms rewr tmL 410 val ruleL = prepare_rules thmL; 411 412 fun doit cL = 413 filter (fn x => not (same_const ((fst o dest_imp o concl) x) F)) 414 (apply_rules ruleL [] cL); 415 416 val thmL1 = doit currentL1; 417 val thmL2 = doit currentL2; 418 419 val thm1' = SIMP_RULE (std_ss++boolSimps.CONJ_ss) [] (LIST_CONJ thmL1) 420 val thm2' = SIMP_RULE (std_ss++boolSimps.CONJ_ss) [thm1'] (LIST_CONJ thmL2) 421 in 422 CONJ thm2' thm1' 423 end 424end 425 426 427*) 428 429val GUESS_RULES_EQUIV = store_thm ("GUESS_RULES_EQUIV", 430``(GUESS_EXISTS_POINT i (\x. P x) /\ 431 GUESS_EXISTS_POINT i (\x. Q x) ==> 432 GUESS_EXISTS_POINT i (\x. P x <=> Q x)) /\ 433 434 (GUESS_FORALL_POINT i (\x. P x) /\ 435 GUESS_FORALL_POINT i (\x. Q x) ==> 436 GUESS_EXISTS_POINT i (\x. P x <=> Q x)) /\ 437 438 (GUESS_EXISTS_POINT i (\x. P x) /\ 439 GUESS_FORALL_POINT i (\x. Q x) ==> 440 GUESS_FORALL_POINT i (\x. P x <=> Q x)) /\ 441 442 (GUESS_FORALL_POINT i (\x. P x) /\ 443 GUESS_EXISTS_POINT i (\x. Q x) ==> 444 GUESS_FORALL_POINT i (\x. P x <=> Q x)) /\ 445 446 (GUESS_FORALL_GAP i (\x. P1 x) /\ 447 GUESS_FORALL_GAP i (\x. P2 x) ==> 448 GUESS_FORALL_GAP i (\x. P1 x <=> P2 x)) /\ 449 450 (GUESS_EXISTS_GAP i (\x. P1 x) /\ 451 GUESS_EXISTS_GAP i (\x. P2 x) ==> 452 GUESS_FORALL_GAP i (\x. P1 x <=> P2 x)) /\ 453 454 (GUESS_EXISTS_GAP i (\x. P1 x) /\ 455 GUESS_FORALL_GAP i (\x. P2 x) ==> 456 GUESS_EXISTS_GAP i (\x. P1 x <=> P2 x)) /\ 457 458 (GUESS_FORALL_GAP i (\x. P1 x) /\ 459 GUESS_EXISTS_GAP i (\x. P2 x) ==> 460 GUESS_EXISTS_GAP i (\x. P1 x <=> P2 x)) 461``, 462 463SIMP_TAC std_ss [GUESS_REWRITES, combinTheory.K_DEF] THEN 464METIS_TAC[]); 465 466 467val GUESS_RULES_COND = store_thm ("GUESS_RULES_COND", 468`` (GUESS_FORALL_POINT i (\x. P x) /\ 469 GUESS_FORALL_POINT i (\x. Q x) ==> 470 GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\ 471 472 (GUESS_EXISTS_POINT i (\x. P x) /\ 473 GUESS_EXISTS_POINT i (\x. Q x) ==> 474 GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\ 475 476 (GUESS_EXISTS i (\x. P x) /\ 477 GUESS_EXISTS i (\x. Q x) ==> 478 GUESS_EXISTS i (\x. if bc then P x else Q x)) /\ 479 480 (GUESS_FORALL i (\x. P x) /\ 481 GUESS_FORALL i (\x. Q x) ==> 482 GUESS_FORALL i (\x. if bc then P x else Q x)) /\ 483 484 (GUESS_EXISTS_GAP i (\x. P x) /\ 485 GUESS_EXISTS_GAP i (\x. Q x) ==> 486 GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\ 487 488 (GUESS_FORALL_GAP i (\x. P x) /\ 489 GUESS_FORALL_GAP i (\x. Q x) ==> 490 GUESS_FORALL_GAP i (\x. if b x then P x else Q x)) /\ 491 492 493 (GUESS_FORALL_POINT i (\x. b x) /\ 494 GUESS_FORALL_POINT i (\x. Q x) ==> 495 GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\ 496 497 (GUESS_FORALL_POINT i (\x. b x) /\ 498 GUESS_EXISTS_POINT i (\x. Q x) ==> 499 GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\ 500 501 (GUESS_EXISTS_POINT i (\x. b x) /\ 502 GUESS_FORALL_POINT i (\x. P x) ==> 503 GUESS_FORALL_POINT i (\x. if b x then P x else Q x)) /\ 504 505 (GUESS_EXISTS_POINT i (\x. b x) /\ 506 GUESS_EXISTS_POINT i (\x. P x) ==> 507 GUESS_EXISTS_POINT i (\x. if b x then P x else Q x)) /\ 508 509 (GUESS_FORALL_GAP i (\x. b x) /\ 510 GUESS_EXISTS_GAP i (\x. P x) ==> 511 GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\ 512 513 (GUESS_EXISTS_GAP i (\x. b x) /\ 514 GUESS_EXISTS_GAP i (\x. Q x) ==> 515 GUESS_EXISTS_GAP i (\x. if b x then P x else Q x)) /\ 516 517 (GUESS_EXISTS_GAP i (\x. b x) /\ 518 GUESS_FORALL_GAP i (\x. Q x) ==> 519 GUESS_FORALL_GAP i (\x. if b x then P x else Q x)) /\ 520 521 (GUESS_FORALL_GAP i (\x. b x) /\ 522 GUESS_FORALL_GAP i (\x. P x) ==> 523 GUESS_FORALL_GAP i (\x. if b x then P x else Q x))``, 524 525SIMP_TAC std_ss [GUESS_REWRITES] THEN 526METIS_TAC[]); 527 528 529val GUESS_RULES_FORALL___NEW_FV = store_thm ("GUESS_RULES_FORALL___NEW_FV", 530``((!y. GUESS_FORALL_POINT (iy y) (\x. P x y)) ==> 531 GUESS_FORALL_POINT (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\ 532 533 ((!y. GUESS_FORALL (iy y) (\x. P x y)) ==> 534 GUESS_FORALL (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\ 535 536 ((!y. GUESS_FORALL_GAP (iy y) (\x. P x y)) ==> 537 GUESS_FORALL_GAP (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y)) /\ 538 539 ((!y. GUESS_EXISTS_GAP (iy y) (\x. P x y)) ==> 540 GUESS_EXISTS_GAP (\fv. iy (FST fv) (SND fv)) (\x. !y. P x y))``, 541 542SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN 543METIS_TAC[]); 544 545 546(* A variant of GUESS_RULES_FORALL___NEW_FV that eliminates unit directly. *) 547val GUESS_RULES_FORALL___NEW_FV_1 = store_thm ("GUESS_RULES_FORALL___NEW_FV_1", 548``((!y. GUESS_FORALL_POINT (\xxx:unit. (i y)) (\x. P (x:'c) (y:'a))) ==> 549 GUESS_FORALL_POINT i (\x. !y. P x y)) /\ 550 551 ((!y. GUESS_FORALL (\xxx:unit. (i y)) (\x. P x y)) ==> 552 GUESS_FORALL i (\x. !y. P x y)) /\ 553 554 ((!y. GUESS_FORALL_GAP (\xxx:unit. (i y)) (\x. P x y)) ==> 555 GUESS_FORALL_GAP i (\x. !y. P x y)) /\ 556 557 ((!y. GUESS_EXISTS_GAP (\xxx:unit. (i y)) (\x. P x y)) ==> 558 GUESS_EXISTS_GAP i (\x. !y. P x y))``, 559 560SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN 561METIS_TAC[]); 562 563 564val GUESS_RULES_FORALL = store_thm ("GUESS_RULES_FORALL", 565``((!y. GUESS_FORALL_POINT i (\x. P x y)) ==> 566 GUESS_FORALL_POINT i (\x. !y. P x y)) /\ 567 568 ((!y. GUESS_FORALL i (\x. P x y)) ==> 569 GUESS_FORALL i (\x. !y. P x y)) /\ 570 571 ((!y. GUESS_FORALL_GAP i (\x. P x y)) ==> 572 GUESS_FORALL_GAP i (\x. !y. P x y)) /\ 573 574 ((!y. GUESS_EXISTS_POINT i (\x. P x y)) ==> 575 GUESS_EXISTS_POINT i (\x. !y. P x y)) /\ 576 577 ((!y. GUESS_EXISTS (\xxx:unit. iK) (\x. P x y)) ==> 578 GUESS_EXISTS (\xxx:unit. iK) (\x. !y. P x y)) /\ 579 580 ((!y. GUESS_EXISTS_GAP i (\x. P x y)) ==> 581 GUESS_EXISTS_GAP i (\x. !y. P x y))``, 582 583SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, EXISTS_PROD] THEN 584METIS_TAC[]); 585 586 587 588local 589 590fun mk_exists_thm thm = 591let 592 val thm0 = INST [ 593 ``P:'c -> 'a -> bool`` |-> ``\x y. ~((P:'c -> 'a ->bool) x y)``] thm 594 val thm1 = BETA_RULE thm0 595 val thm2 = SIMP_RULE pure_ss [GSYM NOT_FORALL_THM, GSYM NOT_EXISTS_THM, 596 GUESSES_NEG_REWRITE] thm1 597in 598 thm2 599end; 600 601in 602 603val GUESS_RULES_EXISTS___NEW_FV = save_thm ("GUESS_RULES_EXISTS___NEW_FV", 604 mk_exists_thm GUESS_RULES_FORALL___NEW_FV); 605 606val GUESS_RULES_EXISTS___NEW_FV_1= save_thm ("GUESS_RULES_EXISTS___NEW_FV_1", 607 mk_exists_thm GUESS_RULES_FORALL___NEW_FV_1); 608 609val GUESS_RULES_EXISTS = save_thm ("GUESS_RULES_EXISTS", 610 mk_exists_thm GUESS_RULES_FORALL); 611 612end 613 614 615val GUESS_RULES_EXISTS_UNIQUE = store_thm ("GUESS_RULES_EXISTS_UNIQUE", 616``((!y. GUESS_FORALL_POINT i (\x. P x y)) ==> 617 GUESS_FORALL_POINT i (\x. ?!y. P x y)) /\ 618 619 ((!y. GUESS_EXISTS_GAP i (\x. P x y)) ==> 620 GUESS_EXISTS_GAP i (\x. ?!y. P x y))``, 621 622SIMP_TAC std_ss [GUESS_REWRITES, EXISTS_UNIQUE_THM]); 623 624 625val QUANT_UNIT_ELIM = prove (`` 626 ((!x:unit. P x) = (P ())) /\ 627 ((?x:unit. P x) = (P ()))``, 628REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 629 ASM_REWRITE_TAC[], 630 Cases_on `x` THEN ASM_REWRITE_TAC[], 631 Cases_on `x` THEN ASM_REWRITE_TAC[], 632 EXISTS_TAC ``()`` THEN ASM_REWRITE_TAC[] 633]); 634 635 636 637val GUESS_RULES_ELIM_UNIT = store_thm ("GUESS_RULES_ELIM_UNIT", 638``(GUESS_FORALL_POINT (i:('a # unit) -> 'b) vt = 639 GUESS_FORALL_POINT (\x:'a. i (x,())) vt) /\ 640 641 (GUESS_EXISTS_POINT (i:('a # unit) -> 'b) vt = 642 GUESS_EXISTS_POINT (\x:'a. i (x,())) vt) /\ 643 644 (GUESS_EXISTS (i:('a # unit) -> 'b) vt = 645 GUESS_EXISTS (\x:'a. i (x,())) vt) /\ 646 647 (GUESS_FORALL (i:('a # unit) -> 'b) vt = 648 GUESS_FORALL (\x:'a. i (x,())) vt) /\ 649 650 (GUESS_EXISTS_GAP (i:('a # unit) -> 'b) vt = 651 GUESS_EXISTS_GAP (\x:'a. i (x,())) vt) /\ 652 653 (GUESS_FORALL_GAP (i:('a # unit) -> 'b) vt = 654 GUESS_FORALL_GAP (\x:'a. i (x,())) vt)``, 655 656SIMP_TAC std_ss [GUESS_REWRITES, FORALL_PROD, 657 EXISTS_PROD, QUANT_UNIT_ELIM]); 658 659 660val GUESS_RULES_STRENGTHEN_EXISTS_POINT = store_thm ("GUESS_RULES_STRENGTHEN_EXISTS_POINT", 661``!P Q. ((!x. P x ==> Q x) ==> 662 ((GUESS_EXISTS_POINT i P ==> 663 GUESS_EXISTS_POINT i Q)))``, 664SIMP_TAC std_ss [GUESS_REWRITES] THEN 665METIS_TAC[]); 666 667val GUESS_RULES_STRENGTHEN_FORALL_GAP = store_thm ("GUESS_RULES_STRENGTHEN_FORALL_GAP", 668``!P Q. ((!x. P x ==> Q x) ==> 669 ((GUESS_FORALL_GAP i P ==> 670 GUESS_FORALL_GAP i Q)))``, 671SIMP_TAC std_ss [GUESS_REWRITES] THEN 672METIS_TAC[]); 673 674val GUESS_RULES_WEAKEN_FORALL_POINT = store_thm ("GUESS_RULES_WEAKEN_FORALL_POINT", 675``!P Q. ((!x. Q x ==> P x) ==> 676 ((GUESS_FORALL_POINT i P ==> 677 GUESS_FORALL_POINT i Q)))``, 678SIMP_TAC std_ss [GUESS_REWRITES] THEN 679METIS_TAC[]); 680 681val GUESS_RULES_WEAKEN_EXISTS_GAP = store_thm ("GUESS_RULES_WEAKEN_EXISTS_GAP", 682``!P Q. ((!x. Q x ==> P x) ==> 683 ((GUESS_EXISTS_GAP i P ==> 684 GUESS_EXISTS_GAP i Q)))``, 685SIMP_TAC std_ss [GUESS_REWRITES] THEN 686METIS_TAC[]); 687 688 689 690(*Basic theorems*) 691 692val CONJ_NOT_OR_THM = store_thm ("CONJ_NOT_OR_THM", 693``!A B. A /\ B = ~(~A \/ ~B)``, 694REWRITE_TAC[DE_MORGAN_THM]) 695 696 697val EXISTS_NOT_FORALL_THM = store_thm ("EXISTS_NOT_FORALL_THM", 698``!P. ((?x. P x) = (~(!x. ~(P x))))``, 699PROVE_TAC[]) 700 701 702val MOVE_EXISTS_IMP_THM = store_thm ("MOVE_EXISTS_IMP_THM", 703``(?x. ((!y. (~(P x y)) ==> R y) ==> Q x)) = 704 (((!y. (~(!x. P x y)) ==> R y)) ==> ?x. Q x)``, 705 PROVE_TAC[]); 706 707 708val UNWIND_EXISTS_THM = store_thm ("UNWIND_EXISTS_THM", 709 ``!a P. (?x. P x) = ((!x. ~(x = a) ==> ~(P x)) ==> P a)``, 710 PROVE_TAC[]); 711 712 713val LEFT_IMP_AND_INTRO = store_thm ("LEFT_IMP_AND_INTRO", 714 ``!x t1 t2. (t1 ==> t2) ==> ((x /\ t1) ==> (x /\ t2))``, 715 PROVE_TAC[]); 716 717val RIGHT_IMP_AND_INTRO = store_thm ("RIGHT_IMP_AND_INTRO", 718 ``!x t1 t2. (t1 ==> t2) ==> ((t1 /\ x) ==> (t2 /\ x))``, 719 PROVE_TAC[]); 720 721 722val LEFT_IMP_OR_INTRO = store_thm ("LEFT_IMP_OR_INTRO", 723 ``!x t1 t2. (t1 ==> t2) ==> ((x \/ t1) ==> (x \/ t2))``, 724 PROVE_TAC[]); 725 726val RIGHT_IMP_OR_INTRO = store_thm ("RIGHT_IMP_OR_INTRO", 727 ``!x t1 t2. (t1 ==> t2) ==> ((t1 \/ x) ==> (t2 \/ x))``, 728 PROVE_TAC[]); 729 730val IMP_NEG_CONTRA = store_thm("IMP_NEG_CONTRA", 731 ``!P i x. ~(P i) ==> (P x) ==> ~(x = i)``, PROVE_TAC[]) 732 733 734val DISJ_IMP_INTRO = store_thm ("DISJ_IMP_INTRO", 735 ``(!x. P x \/ Q x) ==> ((~(P y) ==> Q y) /\ (~(Q y) ==> P y))``, PROVE_TAC[]) 736 737 738(******************************************************************************) 739(* Simple GUESSES *) 740(******************************************************************************) 741 742val SIMPLE_GUESS_EXISTS_def = Define ` 743 SIMPLE_GUESS_EXISTS (v : 'a) (i : 'a) (P : bool) = 744 (P ==> (v = i))` 745 746val SIMPLE_GUESS_EXISTS_ALT_DEF = store_thm ("SIMPLE_GUESS_EXISTS_ALT_DEF", 747 ``(!v. SIMPLE_GUESS_EXISTS (v:'a) i (P v)) <=> ( 748 GUESS_EXISTS_GAP ((K i):(unit -> 'a)) (\v. P v))``, 749SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, GUESS_EXISTS_GAP_def]); 750 751 752val SIMPLE_GUESS_FORALL_def = Define ` 753 SIMPLE_GUESS_FORALL (v : 'a) (i : 'a) (P : bool) = 754 (~P ==> (v = i))` 755 756val SIMPLE_GUESS_FORALL_ALT_DEF = store_thm ("SIMPLE_GUESS_FORALL_ALT_DEF", 757 ``(!v. SIMPLE_GUESS_FORALL (v:'a) i (P v)) <=> ( 758 GUESS_FORALL_GAP ((K i):(unit -> 'a)) (\v. P v))``, 759SIMP_TAC std_ss [SIMPLE_GUESS_FORALL_def, GUESS_FORALL_GAP_def]); 760 761val SIMPLE_GUESS_FORALL_THM = store_thm ("SIMPLE_GUESS_FORALL_THM", 762 ``!i P. (!v. SIMPLE_GUESS_FORALL v i (P v)) ==> 763 ((!v. P v) <=> (P i))``, 764REWRITE_TAC [SIMPLE_GUESS_FORALL_def] THEN 765METIS_TAC[]) 766 767val SIMPLE_GUESS_EXISTS_THM = store_thm ("SIMPLE_GUESS_EXISTS_THM", 768 ``!i P. (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==> 769 ((?v. P v) <=> (P i))``, 770REWRITE_TAC [SIMPLE_GUESS_EXISTS_def] THEN 771METIS_TAC[]) 772 773val SIMPLE_GUESS_UEXISTS_THM = store_thm ("SIMPLE_GUESS_UEXISTS_THM", 774 ``!i P. 775 (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==> 776 ((?!v. P v) <=> (P i))``, 777SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, EXISTS_UNIQUE_THM] THEN 778METIS_TAC[]) 779 780val SIMPLE_GUESS_SELECT_THM = store_thm ("SIMPLE_GUESS_SELECT_THM", 781 ``!i P. 782 (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==> 783 ((@v. P v) = if P i then i else (@v. F))``, 784SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def] THEN 785REPEAT STRIP_TAC THEN 786Cases_on `P i` THEN ASM_REWRITE_TAC [] THENL [ 787 SELECT_ELIM_TAC THEN 788 METIS_TAC[], 789 790 `!v. P v = F` by METIS_TAC[] THEN 791 ASM_REWRITE_TAC[] 792]) 793 794 795val SIMPLE_GUESS_SOME_THM = store_thm ("SIMPLE_GUESS_SOME_THM", 796 ``!i P. 797 (!v. SIMPLE_GUESS_EXISTS v i (P v)) ==> 798 ((some v. P v) = (if P i then SOME i else NONE))``, 799 800SIMP_TAC std_ss [SIMPLE_GUESS_EXISTS_def, some_def] THEN 801REPEAT STRIP_TAC THEN 802Cases_on `?v. P v` THEN ( 803 ASM_REWRITE_TAC [] THEN 804 METIS_TAC[] 805)) 806 807val SIMPLE_GUESS_TAC = 808 SIMP_TAC std_ss [SIMPLE_GUESS_FORALL_def, SIMPLE_GUESS_EXISTS_def] THEN METIS_TAC[]; 809 810val SIMPLE_GUESS_EXISTS_EQ_1 = store_thm ("SIMPLE_GUESS_EXISTS_EQ_1", 811 ``!v:'a i. SIMPLE_GUESS_EXISTS v i (v = i)``, 812 SIMPLE_GUESS_TAC) 813 814val SIMPLE_GUESS_EXISTS_EQ_2 = store_thm ("SIMPLE_GUESS_EXISTS_EQ_2", 815 ``!v:'a i. SIMPLE_GUESS_EXISTS v i (i = v)``, 816 SIMPLE_GUESS_TAC) 817 818val SIMPLE_GUESS_EXISTS_EQ_T = store_thm ("SIMPLE_GUESS_EXISTS_EQ_T", 819 ``!v. SIMPLE_GUESS_EXISTS v T v``, 820 SIMPLE_GUESS_TAC) 821 822val SIMPLE_GUESS_FORALL_NEG = store_thm ("SIMPLE_GUESS_FORALL_NEG", 823 ``!v:'a i P. SIMPLE_GUESS_EXISTS v i P ==> SIMPLE_GUESS_FORALL v i (~P)``, 824 SIMPLE_GUESS_TAC 825) 826 827val SIMPLE_GUESS_EXISTS_NEG = store_thm ("SIMPLE_GUESS_EXISTS_NEG", 828 ``!v:'a i P. SIMPLE_GUESS_FORALL v i P ==> SIMPLE_GUESS_EXISTS v i (~P)``, 829 SIMPLE_GUESS_TAC 830) 831 832val SIMPLE_GUESS_FORALL_OR_1 = store_thm ("SIMPLE_GUESS_FORALL_OR_1", 833 ``!v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P1 ==> SIMPLE_GUESS_FORALL v i (P1 \/ P2)``, 834 SIMPLE_GUESS_TAC); 835 836val SIMPLE_GUESS_FORALL_OR_2 = store_thm ("SIMPLE_GUESS_FORALL_OR_2", 837 ``!v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P2 ==> SIMPLE_GUESS_FORALL v i (P1 \/ P2)``, 838 SIMPLE_GUESS_TAC); 839 840val SIMPLE_GUESS_EXISTS_AND_1 = store_thm ("SIMPLE_GUESS_EXISTS_AND_1", 841 ``!v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P1 ==> SIMPLE_GUESS_EXISTS v i (P1 /\ P2)``, 842 SIMPLE_GUESS_TAC); 843 844val SIMPLE_GUESS_EXISTS_AND_2 = store_thm ("SIMPLE_GUESS_EXISTS_AND_2", 845 ``!v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P2 ==> SIMPLE_GUESS_EXISTS v i (P1 /\ P2)``, 846 SIMPLE_GUESS_TAC); 847 848val SIMPLE_GUESS_EXISTS_EXISTS = store_thm ("SIMPLE_GUESS_EXISTS_EXISTS", 849 ``!v:'a i P. (!v2. SIMPLE_GUESS_EXISTS v i (P v2)) ==> 850 SIMPLE_GUESS_EXISTS v i (?v2. P v2)``, 851 SIMPLE_GUESS_TAC) 852 853val SIMPLE_GUESS_EXISTS_FORALL = store_thm ("SIMPLE_GUESS_EXISTS_FORALL", 854 ``!v:'a i P. (!v2. SIMPLE_GUESS_EXISTS v i (P v2)) ==> 855 SIMPLE_GUESS_EXISTS v i (!v2. P v2)``, 856 SIMPLE_GUESS_TAC) 857 858val SIMPLE_GUESS_FORALL_EXISTS = store_thm ("SIMPLE_GUESS_FORALL_EXISTS", 859 ``!v:'a i P. (!v2. SIMPLE_GUESS_FORALL v i (P v2)) ==> 860 SIMPLE_GUESS_FORALL v i (?v2. P v2)``, 861 SIMPLE_GUESS_TAC) 862 863val SIMPLE_GUESS_FORALL_FORALL = store_thm ("SIMPLE_GUESS_FORALL_FORALL", 864 ``!v i P. (!v2. SIMPLE_GUESS_FORALL v i (P v2)) ==> 865 SIMPLE_GUESS_FORALL v i (!v2. P v2)``, 866 SIMPLE_GUESS_TAC) 867 868val SIMPLE_GUESS_FORALL_IMP_1 = store_thm ("SIMPLE_GUESS_FORALL_IMP_1", 869 ``!v:'a i P1 P2. SIMPLE_GUESS_EXISTS v i P1 ==> SIMPLE_GUESS_FORALL v i (P1 ==> P2)``, 870 SIMPLE_GUESS_TAC); 871 872val SIMPLE_GUESS_FORALL_IMP_2 = store_thm ("SIMPLE_GUESS_FORALL_IMP_2", 873 ``!v:'a i P1 P2. SIMPLE_GUESS_FORALL v i P2 ==> SIMPLE_GUESS_FORALL v i (P1 ==> P2)``, 874 SIMPLE_GUESS_TAC); 875 876val SIMPLE_GUESS_EXISTS_EQ_FUN = store_thm ("SIMPLE_GUESS_EXISTS_EQ_FUN", 877 ``!v:'a i t1 t2 f. 878 SIMPLE_GUESS_EXISTS v i (f t1 = f t2) ==> 879 SIMPLE_GUESS_EXISTS v i (t1 = t2)``, 880 SIMPLE_GUESS_TAC) 881 882 883(******************************************************************************) 884(* Removing functions under quantifiers *) 885(******************************************************************************) 886 887 888val IS_REMOVABLE_QUANT_FUN_def = Define ` 889 IS_REMOVABLE_QUANT_FUN f = (!v. ?x. f x = v)` 890 891val IS_REMOVABLE_QUANT_FUN___EXISTS_THM = store_thm ("IS_REMOVABLE_QUANT_FUN___EXISTS_THM", 892 ``!f P. IS_REMOVABLE_QUANT_FUN f ==> ((?x. P (f x)) = (?x'. P x'))``, 893REWRITE_TAC[IS_REMOVABLE_QUANT_FUN_def] THEN METIS_TAC[]); 894 895val IS_REMOVABLE_QUANT_FUN___FORALL_THM = store_thm ("IS_REMOVABLE_QUANT_FUN___FORALL_THM", 896 ``!f P. IS_REMOVABLE_QUANT_FUN f ==> ((!x. P (f x)) = (!x'. P x'))``, 897REWRITE_TAC[IS_REMOVABLE_QUANT_FUN_def] THEN METIS_TAC[]); 898 899 900 901(* Theorems for the specialised logics *) 902 903val PAIR_EQ_EXPAND = store_thm ("PAIR_EQ_EXPAND", 904``(((x:'a,y:'b) = X) = ((x = FST X) /\ (y = SND X))) /\ 905 ((X = (x,y)) = ((FST X = x) /\ (SND X = y)))``, 906Cases_on `X` THEN 907REWRITE_TAC[pairTheory.PAIR_EQ]); 908 909 910val PAIR_EQ_SIMPLE_EXPAND = store_thm ("PAIR_EQ_SIMPLE_EXPAND", 911``(((x:'a,y:'b) = (x, y')) = (y = y')) /\ 912 (((y:'b,x:'a) = (y', x)) = (y = y')) /\ 913 (((FST X, y) = X) = (y = SND X)) /\ 914 (((x, SND X) = X) = (x = FST X)) /\ 915 ((X = (FST X, y)) = (SND X = y)) /\ 916 ((X = (x, SND X)) = (FST X = x))``, 917Cases_on `X` THEN 918ASM_REWRITE_TAC[pairTheory.PAIR_EQ]); 919 920 921val IS_SOME_EQ_NOT_NONE = store_thm ("IS_SOME_EQ_NOT_NONE", 922``!x. IS_SOME x = ~(x = NONE)``, 923REWRITE_TAC[GSYM optionTheory.NOT_IS_SOME_EQ_NONE]); 924 925 926val ISL_exists = store_thm ("ISL_exists", 927 ``ISL x = (?l. x = INL l)``, 928Cases_on `x` THEN SIMP_TAC std_ss []) 929 930val ISR_exists = store_thm ("ISR_exists", 931 ``ISR x = (?r. x = INR r)``, 932Cases_on `x` THEN SIMP_TAC std_ss []) 933 934val INL_NEQ_ELIM = store_thm ("INL_NEQ_ELIM", 935 ``((!l. x <> INL l) <=> (ISR x)) /\ 936 ((!l. INL l <> x) <=> (ISR x))``, 937Cases_on `x` THEN SIMP_TAC std_ss []); 938 939val INR_NEQ_ELIM = store_thm ("INR_NEQ_ELIM", 940 ``((!r. x <> INR r) <=> (ISL x)) /\ 941 ((!r. INR r <> x) <=> (ISL x))``, 942Cases_on `x` THEN SIMP_TAC std_ss []); 943 944val LENGTH_LE_PLUS = store_thm ("LENGTH_LE_PLUS", 945 ``(n + m) <= LENGTH l <=> (?l1 l2. (LENGTH l1 = n) /\ m <= LENGTH l2 /\ (l = l1 ++ l2))``, 946SIMP_TAC list_ss [arithmeticTheory.LESS_EQ_EXISTS, LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM, 947 GSYM RIGHT_EXISTS_AND_THM] THEN 948METIS_TAC[]); 949 950val LENGTH_LE_NUM = store_thm ("LENGTH_LE_NUM", 951 ``n <= LENGTH l <=> (?l1 l2. (LENGTH l1 = n) /\ (l = l1 ++ l2))``, 952SIMP_TAC list_ss [arithmeticTheory.LESS_EQ_EXISTS, LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM, 953 GSYM RIGHT_EXISTS_AND_THM]); 954 955 956val LENGTH_NIL_SYM = save_thm ("LENGTH_NIL_SYM", 957 CONV_RULE (LHS_CONV SYM_CONV) (SPEC_ALL listTheory.LENGTH_NIL)) 958 959val LIST_LENGTH_COMPARE_1_0 = store_thm ("LIST_LENGTH_COMPARE_1", 960 ``((LENGTH l < 1) <=> (l = [])) /\ 961 ((1 > LENGTH l) <=> (l = [])) /\ 962 ((0 >= LENGTH l) <=> (l = [])) /\ 963 ((LENGTH l <= 0) <=> (l = []))``, 964`LENGTH l < 1 <=> (LENGTH l = 0)` by DECIDE_TAC THEN 965`1 > LENGTH l <=> (LENGTH l = 0)` by DECIDE_TAC THEN 966`0 >= LENGTH l <=> (LENGTH l = 0)` by DECIDE_TAC THEN 967ASM_SIMP_TAC arith_ss [LENGTH_NIL]); 968 969 970val LIST_LENGTH_THMS_0 = ((SPEC_ALL listTheory.LENGTH_NIL):: 971 (SPEC_ALL LENGTH_NIL_SYM):: 972 (BODY_CONJUNCTS LIST_LENGTH_COMPARE_1_0)) 973 974(* prove length theormes generally *) 975 976local 977 val len_t = ``LENGTH (l:'a list)`` 978 979 fun mk_e l 0 = l 980 | mk_e l n = 981 mk_e (("e"^Int.toString n)::l) (n-1) 982 983 fun mk_base_length_thms n = 984 let 985 val n_t = mk_numeral (Arbnum.fromInt n) 986 val pre_n_t = mk_numeral (Arbnum.fromInt (n-1)) 987 val es = mk_e [] n 988 989 (* equality *) 990 val thm_eq = let 991 val l = mk_eq (len_t, n_t); 992 val thm_aux = SIMP_CONV arith_ss [LENGTH_EQ_NUM_compute, GSYM LEFT_EXISTS_AND_THM] l; 993 in 994 CONV_RULE (RHS_CONV (RENAME_VARS_CONV es)) thm_aux 995 end 996 997 (* equality plus *) 998 val thm_eqp = let 999 val l = mk_eq (len_t, mk_plus(n_t, mk_var("x", ``:num``))); 1000 val thm_aux = SIMP_CONV list_ss [LENGTH_EQ_NUM, GSYM LEFT_EXISTS_AND_THM, thm_eq] l; 1001 in 1002 CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux 1003 end 1004 1005 (* less equal *) 1006 val thm_le = let 1007 val l = mk_leq (n_t, len_t); 1008 val thm_aux = SIMP_CONV list_ss [LENGTH_LE_NUM, thm_eq, GSYM LEFT_EXISTS_AND_THM] l; 1009 in 1010 CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux 1011 end 1012 1013 (* less equal plus *) 1014 val thm_lep = let 1015 val l = mk_leq (mk_plus(n_t, mk_var("x", ``:num``)), len_t); 1016 val thm_aux = SIMP_CONV list_ss [LENGTH_LE_PLUS, thm_eq, GSYM LEFT_EXISTS_AND_THM] l; 1017 in 1018 CONV_RULE (RHS_CONV (RENAME_VARS_CONV ["l'"])) thm_aux 1019 end 1020 1021 (* less *) 1022 val thm_less = let 1023 val l = mk_less (pre_n_t, len_t); 1024 val thm_aux = SIMP_CONV list_ss [arithmeticTheory.LESS_EQ, thm_le] l; 1025 in 1026 thm_aux 1027 end 1028 in 1029 (thm_eq, thm_eqp, thm_le, thm_lep, thm_less) 1030 end 1031 1032in 1033 1034fun mk_length_n_thms 0 = LIST_LENGTH_THMS_0 1035 | mk_length_n_thms n = 1036let 1037 fun lhs_rule c = CONV_RULE (LHS_CONV c) 1038 val (eq_thm, eqp_thm, le_thm, lep_thm, less_thm) = mk_base_length_thms n 1039 1040 val eq_thm_sym = lhs_rule SYM_CONV eq_thm 1041 val ge_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) le_thm 1042 val greater_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_DEF)) less_thm 1043 val gep_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) lep_thm 1044 val leps_thm = lhs_rule (RATOR_CONV (RAND_CONV (REWR_CONV (GSYM arithmeticTheory.ADD_SYM)))) lep_thm 1045 val geps_thm = lhs_rule (REWR_CONV (GSYM arithmeticTheory.GREATER_EQ)) leps_thm 1046 1047 val eqp_thm_sym = lhs_rule SYM_CONV eqp_thm 1048 val eqps_thm = lhs_rule (RHS_CONV (REWR_CONV (GSYM arithmeticTheory.ADD_SYM))) eqp_thm 1049 val eqps_thm_sym = lhs_rule SYM_CONV eqps_thm 1050 1051in 1052 [eq_thm, eq_thm_sym, less_thm, greater_thm, le_thm, ge_thm, lep_thm, gep_thm, leps_thm, geps_thm, eqp_thm, eqp_thm_sym, eqps_thm, eqps_thm_sym] 1053end 1054 1055fun mk_length_upto_n_thms 0 = LIST_LENGTH_THMS_0 1056 | mk_length_upto_n_thms n = 1057 (mk_length_n_thms n) @ (mk_length_upto_n_thms (n-1)) 1058 1059end 1060 1061val LIST_LENGTH_0 = save_thm ("LIST_LENGTH_0", LIST_CONJ (mk_length_upto_n_thms 0)); 1062val LIST_LENGTH_1 = save_thm ("LIST_LENGTH_1", LIST_CONJ (mk_length_upto_n_thms 1)); 1063val LIST_LENGTH_2 = save_thm ("LIST_LENGTH_2", LIST_CONJ (mk_length_upto_n_thms 2)); 1064val LIST_LENGTH_3 = save_thm ("LIST_LENGTH_3", LIST_CONJ (mk_length_upto_n_thms 3)); 1065val LIST_LENGTH_4 = save_thm ("LIST_LENGTH_4", LIST_CONJ (mk_length_upto_n_thms 4)); 1066val LIST_LENGTH_5 = save_thm ("LIST_LENGTH_5", LIST_CONJ (mk_length_upto_n_thms 5)); 1067val LIST_LENGTH_7 = save_thm ("LIST_LENGTH_7", LIST_CONJ (mk_length_upto_n_thms 7)); 1068val LIST_LENGTH_10 = save_thm ("LIST_LENGTH_10", LIST_CONJ (mk_length_upto_n_thms 10)); 1069val LIST_LENGTH_15 = save_thm ("LIST_LENGTH_15", LIST_CONJ (mk_length_upto_n_thms 15)); 1070val LIST_LENGTH_20 = save_thm ("LIST_LENGTH_20", LIST_CONJ (mk_length_upto_n_thms 20)); 1071val LIST_LENGTH_25 = save_thm ("LIST_LENGTH_25", LIST_CONJ (mk_length_upto_n_thms 25)); 1072 1073val LIST_LENGTH_COMPARE_SUC = store_thm ("LIST_LENGTH_COMPARE_SUC", 1074``(SUC x <= LENGTH l <=> ?l' e1. x <= LENGTH l' /\ (l = e1::l')) /\ 1075 (LENGTH l >= SUC x <=> ?l' e1. x <= LENGTH l' /\ (l = e1::l')) /\ 1076 ((LENGTH l = SUC x) <=> ?l' e1. (LENGTH l' = x) /\ (l = e1::l')) /\ 1077 ((SUC x = LENGTH l) <=> ?l' e1. (LENGTH l' = x) /\ (l = e1::l'))``, 1078SIMP_TAC std_ss [arithmeticTheory.ADD1, LIST_LENGTH_1]); 1079 1080 1081(* Useful rewrites *) 1082val HD_TL_EQ_TAC = REPEAT (Cases THEN SIMP_TAC list_ss [] THEN SPEC_ALL_TAC) 1083 1084val HD_TL_EQ_1 = prove ( 1085 ``!l. (HD l :: TL l = l) <=> l <> []``, 1086HD_TL_EQ_TAC) 1087 1088val HD_TL_EQ_2 = prove ( 1089 ``!l. (HD l :: (HD (TL l)) :: (TL (TL l)) = l) <=> (LENGTH l > 1)``, 1090HD_TL_EQ_TAC) 1091 1092val HD_TL_EQ_3 = prove ( 1093 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (TL (TL (TL l))) = l) <=> (LENGTH l > 2)``, 1094HD_TL_EQ_TAC) 1095 1096val HD_TL_EQ_4 = prove ( 1097 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: TL (TL (TL (TL l))) = l) <=> (LENGTH l > 3)``, 1098HD_TL_EQ_TAC) 1099 1100val HD_TL_EQ_5 = prove ( 1101 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1102 (HD (TL (TL (TL (TL l))))) :: TL (TL (TL (TL (TL l)))) = l) <=> (LENGTH l > 4)``, 1103HD_TL_EQ_TAC) 1104 1105val HD_TL_EQ_6 = prove ( 1106 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1107 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: TL (TL (TL (TL (TL (TL l))))) = l) <=> (LENGTH l > 5)``, 1108HD_TL_EQ_TAC) 1109 1110val HD_TL_EQ_7 = prove ( 1111 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1112 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1113 HD (TL (TL (TL (TL (TL (TL l)))))) :: TL (TL (TL (TL (TL (TL (TL l)))))) = l) <=> (LENGTH l > 6)``, 1114HD_TL_EQ_TAC) 1115 1116val HD_TL_EQ_8 = prove ( 1117 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1118 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1119 HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) :: 1120 TL (TL (TL (TL (TL (TL (TL (TL l))))))) = l) <=> (LENGTH l > 7)``, 1121HD_TL_EQ_TAC) 1122 1123val HD_TL_EQ_9 = prove ( 1124 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1125 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1126 HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) :: 1127 HD (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) :: TL (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) = l) <=> (LENGTH l > 8)``, 1128HD_TL_EQ_TAC) 1129 1130 1131val HD_TL_EQ_NIL_1 = prove ( 1132 ``!l. (HD l :: [] = l) <=> (LENGTH l = 1)``, 1133HD_TL_EQ_TAC) 1134 1135val HD_TL_EQ_NIL_2 = prove ( 1136 ``!l. (HD l :: (HD (TL l)) :: [] = l) <=> (LENGTH l = 2)``, 1137HD_TL_EQ_TAC) 1138 1139val HD_TL_EQ_NIL_3 = prove ( 1140 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: [] = l) <=> (LENGTH l = 3)``, 1141HD_TL_EQ_TAC) 1142 1143val HD_TL_EQ_NIL_4 = prove ( 1144 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: [] = l) <=> (LENGTH l = 4)``, 1145HD_TL_EQ_TAC) 1146 1147val HD_TL_EQ_NIL_5 = prove ( 1148 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1149 (HD (TL (TL (TL (TL l))))) :: [] = l) <=> (LENGTH l = 5)``, 1150HD_TL_EQ_TAC) 1151 1152val HD_TL_EQ_NIL_6 = prove ( 1153 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1154 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: [] = l) <=> (LENGTH l = 6)``, 1155HD_TL_EQ_TAC) 1156 1157val HD_TL_EQ_NIL_7 = prove ( 1158 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1159 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1160 HD (TL (TL (TL (TL (TL (TL l)))))) :: [] = l) <=> (LENGTH l = 7)``, 1161HD_TL_EQ_TAC) 1162 1163val HD_TL_EQ_NIL_8 = prove ( 1164 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1165 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1166 HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) :: 1167 [] = l) <=> (LENGTH l = 8)``, 1168HD_TL_EQ_TAC) 1169 1170val HD_TL_EQ_NIL_9 = prove ( 1171 ``!l. (HD l :: (HD (TL l)) :: (HD (TL (TL l))) :: (HD (TL (TL (TL l)))) :: 1172 (HD (TL (TL (TL (TL l))))) :: HD (TL (TL (TL (TL (TL l))))) :: 1173 HD (TL (TL (TL (TL (TL (TL l)))))) :: HD (TL (TL (TL (TL (TL (TL (TL l))))))) :: 1174 HD (TL (TL (TL (TL (TL (TL (TL (TL l)))))))) :: [] = l) <=> (LENGTH l = 9)``, 1175HD_TL_EQ_TAC) 1176 1177val HD_TL_EQ_THMS_1 = [ 1178 HD_TL_EQ_1, 1179 HD_TL_EQ_2, 1180 HD_TL_EQ_3, 1181 HD_TL_EQ_4, 1182 HD_TL_EQ_5, 1183 HD_TL_EQ_6, 1184 HD_TL_EQ_7, 1185 HD_TL_EQ_8, 1186 HD_TL_EQ_9, 1187 HD_TL_EQ_NIL_1, 1188 HD_TL_EQ_NIL_2, 1189 HD_TL_EQ_NIL_3, 1190 HD_TL_EQ_NIL_4, 1191 HD_TL_EQ_NIL_5, 1192 HD_TL_EQ_NIL_6, 1193 HD_TL_EQ_NIL_7, 1194 HD_TL_EQ_NIL_8, 1195 HD_TL_EQ_NIL_9] 1196 1197val HD_TL_EQ_THMS_2 = map ( 1198 CONV_RULE (QUANT_CONV (LHS_CONV (REWR_CONV EQ_SYM_EQ)))) HD_TL_EQ_THMS_1 1199 1200val HD_TL_EQ_THMS = save_thm ("HD_TL_EQ_THMS", LIST_CONJ 1201 (HD_TL_EQ_THMS_1 @ HD_TL_EQ_THMS_2)) 1202 1203val SOME_THE_EQ = store_thm ("SOME_THE_EQ", 1204 ``!opt. (SOME (THE opt) = opt) <=> IS_SOME opt``, 1205Cases THEN SIMP_TAC std_ss []) 1206 1207val SOME_THE_EQ_SYM = store_thm ("SOME_THE_EQ_SYM", 1208 ``!opt. (opt = SOME (THE opt)) <=> IS_SOME opt``, 1209Cases THEN SIMP_TAC std_ss []) 1210 1211val FST_PAIR_EQ = store_thm ("FST_PAIR_EQ", 1212``!p p2. ((FST p, p2) = p) <=> (p2 = SND p)``, 1213Cases THEN SIMP_TAC std_ss []) 1214 1215val SND_PAIR_EQ = store_thm ("SND_PAIR_EQ", 1216``!p p1. ((p1, SND p) = p) <=> (p1 = FST p)``, 1217Cases THEN SIMP_TAC std_ss []) 1218 1219val FST_PAIR_EQ_SYM = store_thm ("FST_PAIR_EQ_SYM", 1220``!p p2. (p = (FST p, p2)) <=> (SND p = p2)``, 1221Cases THEN SIMP_TAC std_ss []) 1222 1223val SND_PAIR_EQ_SYM = store_thm ("SND_PAIR_EQ_SYM", 1224``!p p1. (p = (p1, SND p)) <=> (FST p = p1)``, 1225Cases THEN SIMP_TAC std_ss []) 1226 1227 1228val _ = export_theory(); 1229