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