jHOLLight/Examples/ssrbool-compiled.hl

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