formal_ineqs/lib/ssrbool-compiled.hl

   1 needs "lib/ssrfun-compiled.hl";;
   2
   3 (* Section ApplyIff *)
   4 begin_section "ApplyIff";;
   5 (add_section_var (mk_var ("P", (`:bool`))); add_section_var (mk_var ("Q", (`:bool`))));;
   6 (add_section_hyp "eqPQ" (`P <=> Q`));;
   7
   8 (* Lemma iffLR *)
   9 let iffLR = section_proof []
  10 `P ==> Q`
  11 [
  12    (done_tac);
  13 ];;
  14
  15 (* Lemma iffRL *)
  16 let iffRL = section_proof []
  17 `Q ==> P`
  18 [
  19    (done_tac);
  20 ];;
  21
  22 (* Lemma iffLRn *)
  23 let iffLRn = section_proof []
  24 `~P ==> ~Q`
  25 [
  26    (done_tac);
  27 ];;
  28
  29 (* Lemma iffRLn *)
  30 let iffRLn = section_proof []
  31 `~Q ==> ~P`
  32 [
  33    (done_tac);
  34 ];;
  35
  36 (* Finalization of the section ApplyIff *)
  37 let iffLR = finalize_theorem iffLR;;
  38 let iffRL = finalize_theorem iffRL;;
  39 let iffLRn = finalize_theorem iffLRn;;
  40 let iffRLn = finalize_theorem iffRLn;;
  41 end_section "ApplyIff";;
  42
  43 (* Lemma is_true_true *)
  44 let is_true_true = section_proof []
  45 `T`
  46 [
  47    (done_tac);
  48 ];;
  49
  50 (* Lemma not_false_is_true *)
  51 let not_false_is_true = section_proof []
  52 `~F`
  53 [
  54    (done_tac);
  55 ];;
  56 let isT = is_true_true;;
  57 let notF = not_false_is_true;;
  58
  59 (* Lemma negbT *)
  60 let negbT = section_proof ["b"]
  61 `(b = F) ==> ~b`
  62 [
  63    (done_tac);
  64 ];;
  65
  66 (* Lemma negbTE *)
  67 let negbTE = section_proof ["b"]
  68 `~b ==> b = F`
  69 [
  70    (done_tac);
  71 ];;
  72
  73 (* Lemma negbF *)
  74 let negbF = section_proof ["b"]
  75 `b ==> ~b = F`
  76 [
  77    (done_tac);
  78 ];;
  79
  80 (* Lemma negbFE *)
  81 let negbFE = section_proof ["b"]
  82 `~b = F ==> b`
  83 [
  84    (done_tac);
  85 ];;
  86
  87 (* Lemma negbK *)
  88 let negbK = section_proof ["b"]
  89 `~ ~b = b`
  90 [
  91    (done_tac);
  92 ];;
  93
  94 (* Lemma negbNE *)
  95 let negbNE = section_proof ["b"]
  96 `~ ~ b ==> b`
  97 [
  98    (done_tac);
  99 ];;
 100
 101 (* Lemma negb_inj *)
 102 let negb_inj = section_proof ["b1";"b2"]
 103 `~b1 = ~b2 ==> b1 = b2`
 104 [
 105    ((((use_arg_then "b1") (disch_tac [])) THEN (clear_assumption "b1") THEN case) THEN (((use_arg_then "b2") (disch_tac [])) THEN (clear_assumption "b2") THEN case THEN (simp_tac)) THEN (done_tac));
 106 ];;
 107
 108 (* Lemma negbLR *)
 109 let negbLR = section_proof ["b";"c"]
 110 `b = ~c ==> ~b = c`
 111 [
 112    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "negbK")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 113 ];;
 114
 115 (* Lemma negbRL *)
 116 let negbRL = section_proof ["b";"c"]
 117 `~b = c ==> b = ~c`
 118 [
 119    ((BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "negbK")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 120 ];;
 121
 122 (* Lemma contra *)
 123 let contra = section_proof ["c";"b"]
 124 `(c ==> b) ==> ~b ==> ~c`
 125 [
 126    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 127 ];;
 128 let contraNN = contra;;
 129
 130 (* Lemma contraL *)
 131 let contraL = section_proof ["c";"b"]
 132 `(c ==> ~b) ==> b ==> ~c`
 133 [
 134    (BETA_TAC THEN (move ["h"]));
 135    ((((fun arg_tac -> (use_arg_then "contra") (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then "negbK")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 136 ];;
 137
 138 (* Lemma contraR *)
 139 let contraR = section_proof ["c";"b"]
 140 `(~c ==> b) ==> ~b ==> c`
 141 [
 142    (BETA_TAC THEN (move ["h"]));
 143    ((((fun arg_tac -> (use_arg_then "contra") (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((use_arg_then "negbK")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 144 ];;
 145
 146 (* Lemma contraLR *)
 147 let contraLR = section_proof ["c";"b"]
 148 `(~c ==> ~b) ==> b ==> c`
 149 [
 150    (BETA_TAC THEN (move ["h"]));
 151    ((((fun arg_tac -> (use_arg_then "contra") (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (repeat_tactic 1 9 (((use_arg_then "negbK")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 152 ];;
 153
 154 (* Lemma contraT *)
 155 let contraT = section_proof ["b"]
 156 `(~b ==> F) ==> b`
 157 [
 158    (done_tac);
 159 ];;
 160
 161 (* Lemma wlog_neg *)
 162 let wlog_neg = section_proof ["b"]
 163 `(~b ==> b) ==> b`
 164 [
 165    (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac));
 166 ];;
 167
 168 (* Lemma contraFT *)
 169 let contraFT = section_proof ["c";"b"]
 170 `(~c ==> b) ==> b = F ==> c`
 171 [
 172    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 173 ];;
 174
 175 (* Lemma contraFN *)
 176 let contraFN = section_proof ["c";"b"]
 177 `(c ==> b) ==> b = F ==> ~c`
 178 [
 179    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 180 ];;
 181
 182 (* Lemma contraTF *)
 183 let contraTF = section_proof ["c";"b"]
 184 `(c ==> ~b) ==> b ==> c = F`
 185 [
 186    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 187 ];;
 188
 189 (* Lemma contraNF *)
 190 let contraNF = section_proof ["c";"b"]
 191 `(c ==> b) ==> ~b ==> c = F`
 192 [
 193    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 194 ];;
 195
 196 (* Lemma contraFF *)
 197 let contraFF = section_proof ["c";"b"]
 198 `(c ==> b) ==> b = F ==> c = F`
 199 [
 200    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)));
 201 ];;
 202 let isSome = define `isSome NONE = F /\ (!x. isSome (SOME x) = T)`;;
 203
 204 (* Section BoolIf *)
 205 begin_section "BoolIf";;
 206 (add_section_var (mk_var ("vT", (`:A`))); add_section_var (mk_var ("vF", (`:A`))));;
 207 (add_section_var (mk_var ("f", (`:A -> B`))));;
 208 (add_section_var (mk_var ("b", (`:bool`))));;
 209
 210 (* Lemma if_same *)
 211 let if_same = section_proof []
 212 `(if b then vT else vT) = vT`
 213 [
 214    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 215 ];;
 216
 217 (* Lemma if_neg *)
 218 let if_neg = section_proof []
 219 `(if ~b then vT else vF) = if b then vF else vT`
 220 [
 221    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 222 ];;
 223
 224 (* Lemma fun_if *)
 225 let fun_if = section_proof []
 226 `f (if b then vT else vF) = if b then f vT else f vF`
 227 [
 228    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 229 ];;
 230
 231 (* Lemma if_arg *)
 232 let if_arg = section_proof ["fT";"fF";"x"]
 233 `(if b then (fT:A->B) else fF) x = if b then fT x else fF x`
 234 [
 235    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 236 ];;
 237
 238 (* Finalization of the section BoolIf *)
 239 let if_same = finalize_theorem if_same;;
 240 let if_neg = finalize_theorem if_neg;;
 241 let fun_if = finalize_theorem fun_if;;
 242 let if_arg = finalize_theorem if_arg;;
 243 end_section "BoolIf";;
 244
 245 (* Lemma andTb *)
 246 let andTb = section_proof ["b"]
 247 `(T /\ b) = b`
 248 [
 249    (done_tac);
 250 ];;
 251
 252 (* Lemma andFb *)
 253 let andFb = section_proof ["b"]
 254 `(F /\ b) = F`
 255 [
 256    (done_tac);
 257 ];;
 258
 259 (* Lemma andbT *)
 260 let andbT = section_proof ["b"]
 261 `(b /\ T) = b`
 262 [
 263    (done_tac);
 264 ];;
 265
 266 (* Lemma andbF *)
 267 let andbF = section_proof ["b"]
 268 `(b /\ F) = F`
 269 [
 270    (done_tac);
 271 ];;
 272
 273 (* Lemma andbb *)
 274 let andbb = section_proof ["b"]
 275 `(b /\ b) = b`
 276 [
 277    (done_tac);
 278 ];;
 279
 280 (* Lemma andbC *)
 281 let andbC = section_proof ["b";"c"]
 282 `(b /\ c) = (c /\ b)`
 283 [
 284    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 285 ];;
 286
 287 (* Lemma andbA *)
 288 let andbA = section_proof ["b";"c";"p"]
 289 `b /\ (c /\ p) <=> (b /\ c) /\ p`
 290 [
 291    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 292 ];;
 293
 294 (* Lemma andbCA *)
 295 let andbCA = section_proof ["b";"c";"p"]
 296 `b /\ (c /\ p) <=> c /\ (b /\ p)`
 297 [
 298    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 299 ];;
 300
 301 (* Lemma andbAC *)
 302 let andbAC = section_proof ["b";"c";"p"]
 303 `(b /\ c) /\ p <=> (b /\ p) /\ c`
 304 [
 305    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 306 ];;
 307
 308 (* Lemma orTb *)
 309 let orTb = section_proof ["b"]
 310 `T \/ b <=> T`
 311 [
 312    (done_tac);
 313 ];;
 314
 315 (* Lemma orFb *)
 316 let orFb = section_proof ["b"]
 317 `F \/ b <=> b`
 318 [
 319    (done_tac);
 320 ];;
 321
 322 (* Lemma orbT *)
 323 let orbT = section_proof ["b"]
 324 `b \/ T <=> T`
 325 [
 326    (done_tac);
 327 ];;
 328
 329 (* Lemma orbF *)
 330 let orbF = section_proof ["b"]
 331 `b \/ F <=> b`
 332 [
 333    (done_tac);
 334 ];;
 335
 336 (* Lemma orbb *)
 337 let orbb = section_proof ["b"]
 338 `b \/ b <=> b`
 339 [
 340    (done_tac);
 341 ];;
 342
 343 (* Lemma orbC *)
 344 let orbC = section_proof ["b";"c"]
 345 `b \/ c <=> c \/ b`
 346 [
 347    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 348 ];;
 349
 350 (* Lemma orbA *)
 351 let orbA = section_proof ["b";"c";"p"]
 352 `b \/ (c \/ p) <=> (b \/ c) \/ p`
 353 [
 354    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 355 ];;
 356
 357 (* Lemma orbCA *)
 358 let orbCA = section_proof ["b";"c";"p"]
 359 `b \/ (c \/ p) <=> c \/ (b \/ p)`
 360 [
 361    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 362 ];;
 363
 364 (* Lemma orbAC *)
 365 let orbAC = section_proof ["b";"c";"p"]
 366 `(b \/ c) \/ p <=> (b \/ p) \/ c`
 367 [
 368    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 369 ];;
 370
 371 (* Lemma andbN *)
 372 let andbN = section_proof ["b"]
 373 `b /\ ~b <=> F`
 374 [
 375    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 376 ];;
 377
 378 (* Lemma andNb *)
 379 let andNb = section_proof ["b"]
 380 `~b /\ b <=> F`
 381 [
 382    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 383 ];;
 384
 385 (* Lemma orbN *)
 386 let orbN = section_proof ["b"]
 387 `b \/ ~b`
 388 [
 389    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 390 ];;
 391
 392 (* Lemma orNb *)
 393 let orNb = section_proof ["b"]
 394 `~b \/ b`
 395 [
 396    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 397 ];;
 398
 399 (* Lemma andb_orl *)
 400 let andb_orl = section_proof ["b";"c";"p"]
 401 `(b \/ c) /\ p <=> (b /\ p) \/ (c /\ p)`
 402 [
 403    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 404 ];;
 405
 406 (* Lemma andb_orr *)
 407 let andb_orr = section_proof ["b";"c";"p"]
 408 `b /\ (c \/ p) <=> (b /\ c) \/ (b /\ p)`
 409 [
 410    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 411 ];;
 412
 413 (* Lemma orb_andl *)
 414 let orb_andl = section_proof ["b";"c";"p"]
 415 `(b /\ c) \/ p <=> (b \/ p) /\ (c \/ p)`
 416 [
 417    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 418 ];;
 419
 420 (* Lemma orb_andr *)
 421 let orb_andr = section_proof ["b";"c";"p"]
 422 `b \/ (c /\ p) <=> (b \/ c) /\ (b \/ p)`
 423 [
 424    ((((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 425 ];;
 426
 427 (* Lemma andb_idl *)
 428 let andb_idl = section_proof ["a";"b"]
 429 `(b ==> a) ==> (a /\ b <=> b)`
 430 [
 431    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 432 ];;
 433
 434 (* Lemma andb_idr *)
 435 let andb_idr = section_proof ["a";"b"]
 436 `(a ==> b) ==> (a /\ b <=> a)`
 437 [
 438    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 439 ];;
 440
 441 (* Lemma andb_id2l *)
 442 let andb_id2l = section_proof ["a";"b";"c"]
 443 `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`
 444 [
 445    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 446 ];;
 447
 448 (* Lemma andb_id2r *)
 449 let andb_id2r = section_proof ["a";"b";"c"]
 450 `(b ==> (a <=> c)) ==> (a /\ b <=> c /\ b)`
 451 [
 452    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 453 ];;
 454
 455 (* Lemma orb_idl *)
 456 let orb_idl = section_proof ["a";"b"]
 457 `(a ==> b) ==> (a \/ b <=> b)`
 458 [
 459    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 460 ];;
 461
 462 (* Lemma orbb_idr *)
 463 let orbb_idr = section_proof ["a";"b"]
 464 `(b ==> a) ==> (a \/ b <=> a)`
 465 [
 466    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 467 ];;
 468
 469 (* Lemma orb_id2l *)
 470 let orb_id2l = section_proof ["a";"b";"c"]
 471 `(~ a ==> (b <=> c)) ==> (a \/ b <=> a \/ c)`
 472 [
 473    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 474 ];;
 475
 476 (* Lemma orb_id2r *)
 477 let orb_id2r = section_proof ["a";"b";"c"]
 478 `(~ b ==> (a <=> c)) ==> (a \/ b <=> c \/ b)`
 479 [
 480    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 481 ];;
 482
 483 (* Lemma negb_and *)
 484 let negb_and = section_proof ["a";"b"]
 485 `~ (a /\ b) <=> ~ a \/ ~ b`
 486 [
 487    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 488 ];;
 489
 490 (* Lemma negb_or *)
 491 let negb_or = section_proof ["a";"b"]
 492 `~ (a \/ b) <=> ~ a /\ ~ b`
 493 [
 494    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 495 ];;
 496
 497 (* Lemma andbK *)
 498 let andbK = section_proof ["a";"b"]
 499 `((a /\ b) \/ a) = a`
 500 [
 501    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 502 ];;
 503
 504 (* Lemma andKb *)
 505 let andKb = section_proof ["a";"b"]
 506 `a \/ b /\ a <=> a`
 507 [
 508    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 509 ];;
 510
 511 (* Lemma orbK *)
 512 let orbK = section_proof ["a";"b"]
 513 `(a \/ b) /\ a <=> a`
 514 [
 515    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 516 ];;
 517
 518 (* Lemma orKb *)
 519 let orKb = section_proof ["a";"b"]
 520 `a /\ (b \/ a) <=> a`
 521 [
 522    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 523 ];;
 524
 525 (* Lemma implybT *)
 526 let implybT = section_proof ["b"]
 527 `b ==> T`
 528 [
 529    (done_tac);
 530 ];;
 531
 532 (* Lemma implybF *)
 533 let implybF = section_proof ["b"]
 534 `(b ==> F) <=> ~ b`
 535 [
 536    (done_tac);
 537 ];;
 538
 539 (* Lemma implyFb *)
 540 let implyFb = section_proof ["b"]
 541 `F ==> b`
 542 [
 543    (done_tac);
 544 ];;
 545
 546 (* Lemma implyTb *)
 547 let implyTb = section_proof ["b"]
 548 `(T ==> b) <=> b`
 549 [
 550    (done_tac);
 551 ];;
 552
 553 (* Lemma implybb *)
 554 let implybb = section_proof ["b"]
 555 `b ==> b`
 556 [
 557    (done_tac);
 558 ];;
 559
 560 (* Lemma negb_imply *)
 561 let negb_imply = section_proof ["a";"b"]
 562 `~ (a ==> b) <=> a /\ ~ b`
 563 [
 564    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 565 ];;
 566
 567 (* Lemma implybE *)
 568 let implybE = section_proof ["a";"b"]
 569 `(a ==> b) <=> ~ a \/ b`
 570 [
 571    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 572 ];;
 573
 574 (* Lemma implyNb *)
 575 let implyNb = section_proof ["a";"b"]
 576 `(~ a ==> b) <=> a \/ b`
 577 [
 578    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 579 ];;
 580
 581 (* Lemma implybN *)
 582 let implybN = section_proof ["a";"b"]
 583 `(a ==> ~ b) <=> (b ==> ~ a)`
 584 [
 585    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 586 ];;
 587
 588 (* Lemma implybNN *)
 589 let implybNN = section_proof ["a";"b"]
 590 `(~ a ==> ~ b) <=> b ==> a`
 591 [
 592    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 593 ];;
 594
 595 (* Lemma implyb_idl *)
 596 let implyb_idl = section_proof ["a";"b"]
 597 `(~ a ==> b) ==> ((a ==> b) <=> b)`
 598 [
 599    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 600 ];;
 601
 602 (* Lemma implyb_idr *)
 603 let implyb_idr = section_proof ["a";"b"]
 604 `(b ==> ~ a) ==> ((a ==> b) <=> ~ a)`
 605 [
 606    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 607 ];;
 608
 609 (* Lemma implyb_id2l *)
 610 let implyb_id2l = section_proof ["a";"b";"c"]
 611 `(a ==> (b <=> c)) ==> ((a ==> b) <=> (a ==> c))`
 612 [
 613    ((((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)) THEN (done_tac));
 614 ];;
 615 let XOR_DEF = new_definition `XOR p q = if p then ~q else q`;;
 616 overload_interface("+", `XOR`);;
 617
 618 (* Lemma addFb *)
 619 let addFb = section_proof ["b"]
 620 `F + b <=> b`
 621 [
 622    ((((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] [])))) THEN (done_tac));
 623 ];;
 624
 625 (* Lemma addbF *)
 626 let addbF = section_proof ["b"]
 627 `b + F <=> b`
 628 [
 629    ((((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 630 ];;
 631
 632 (* Lemma addbb *)
 633 let addbb = section_proof ["b"]
 634 `b + b <=> F`
 635 [
 636    ((((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 637 ];;
 638
 639 (* Lemma addbC *)
 640 let addbC = section_proof ["b";"c"]
 641 `b + c <=> c + b`
 642 [
 643    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case THEN (simp_tac)) THEN (done_tac));
 644 ];;
 645
 646 (* Lemma addbA *)
 647 let addbA = section_proof ["a";"b";"c"]
 648 `a + (b + c) <=> (a + b) + c`
 649 [
 650    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
 651 ];;
 652
 653 (* Lemma addbCA *)
 654 let addbCA = section_proof ["a";"b";"c"]
 655 `(a + b) + c <=> (a + c) + b`
 656 [
 657    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
 658 ];;
 659
 660 (* Lemma addbAC *)
 661 let addbAC = section_proof ["a";"b";"c"]
 662 `a + (b + c) <=> b + (a + c)`
 663 [
 664    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
 665 ];;
 666
 667 (* Lemma andb_addl *)
 668 let andb_addl = section_proof ["a";"b";"c"]
 669 `(a + b) /\ c <=> (a /\ c) + (b /\ c)`
 670 [
 671    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
 672 ];;
 673
 674 (* Lemma andb_addr *)
 675 let andb_addr = section_proof ["a";"b";"c"]
 676 `a /\ (b + c) <=> (a /\ b) + (a /\ c)`
 677 [
 678    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case) THEN (((use_arg_then "c") (disch_tac [])) THEN (clear_assumption "c") THEN case) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case THEN (simp_tac)));
 679 ];;
 680
 681 (* Lemma addKb *)
 682 let addKb = section_proof ["x";"y"]
 683 `x + (x + y) <=> y`
 684 [
 685    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then "y") (disch_tac [])) THEN (clear_assumption "y") THEN case THEN (simp_tac)));
 686 ];;
 687
 688 (* Lemma addbK *)
 689 let addbK = section_proof ["x";"y"]
 690 `(y + x) + x <=> y`
 691 [
 692    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then "y") (disch_tac [])) THEN (clear_assumption "y") THEN case THEN (simp_tac)));
 693 ];;
 694
 695 (* Lemma addIb *)
 696 let addIb = section_proof ["x";"y1";"y2"]
 697 `(y1 + x <=> y2 + x) ==> (y1 = y2)`
 698 [
 699    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "y1") (disch_tac [])) THEN (clear_assumption "y1") THEN case) THEN (((use_arg_then "y2") (disch_tac [])) THEN (clear_assumption "y2") THEN case) THEN (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN case THEN (simp_tac)));
 700 ];;
 701
 702 (* Lemma addbI *)
 703 let addbI = section_proof ["x";"y1";"y2"]
 704 `(x + y1 <=> x + y2) ==> (y1 = y2)`
 705 [
 706    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "x") (disch_tac [])) THEN (clear_assumption "x") THEN case) THEN (((use_arg_then "y1") (disch_tac [])) THEN (clear_assumption "y1") THEN case) THEN (((use_arg_then "y2") (disch_tac [])) THEN (clear_assumption "y2") THEN case THEN (simp_tac)));
 707 ];;
 708
 709 (* Lemma addTb *)
 710 let addTb = section_proof ["b"]
 711 `T + b <=> ~b`
 712 [
 713    (((((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac))) THEN (done_tac));
 714 ];;
 715
 716 (* Lemma addbT *)
 717 let addbT = section_proof ["b"]
 718 `b + T <=> ~ b`
 719 [
 720    ((((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)) THEN (done_tac));
 721 ];;
 722
 723 (* Lemma addbN *)
 724 let addbN = section_proof ["a";"b"]
 725 `a + ~ b <=> ~ (a + b)`
 726 [
 727    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)));
 728 ];;
 729
 730 (* Lemma addNb *)
 731 let addNb = section_proof ["a";"b"]
 732 `~ a + b <=> ~ (a + b)`
 733 [
 734    ((repeat_tactic 1 9 (((use_arg_then "XOR_DEF")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "a") (disch_tac [])) THEN (clear_assumption "a") THEN case) THEN (((use_arg_then "b") (disch_tac [])) THEN (clear_assumption "b") THEN case THEN (simp_tac)));
 735 ];;
 736 let subpred = new_definition `subpred p1 p2 <=> (!x. p1 x ==> p2 x)`;;
 737 let subrel = new_definition `subrel r1 r2 <=> (!x y. r1 x y ==> r2 x y)`;;
 738 let pred0 = new_definition `pred0 = (\x. F)`;;
 739 let predT = new_definition `predT = (\x. T)`;;
 740 let predI = new_definition `predI p1 p2 = (\x. p1 x /\ p2 x)`;;
 741 let predU = new_definition `predU p1 p2 = (\x. p1 x \/ p2 x)`;;
 742 let predC = new_definition `predC p = (\x. ~p x)`;;
 743 let predD = new_definition `predD p1 p2 = (\x. ~p2 x /\ p1 x)`;;
 744 let preim = new_definition `preim f (d:A->bool) = (\x. d (f x))`;;
 745 let relU = new_definition `relU r1 r2 = (\x y. r1 x y \/ r2 x y)`;;
 746
 747 (* Lemma subrelUl *)
 748 let subrelUl = section_proof ["r1";"r2"]
 749 `subrel r1 (relU r1 r2)`
 750 [
 751    (((((use_arg_then "relU")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subrel")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
 752 ];;
 753
 754 (* Lemma subrelUr *)
 755 let subrelUr = section_proof ["r1";"r2"]
 756 `subrel r2 (relU r1 r2)`
 757 [
 758    (((((use_arg_then "relU")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "subrel")(thm_tac (new_rewrite [] [])))) THEN (simp_tac)) THEN (done_tac));
 759 ];;