Unity/mk_state_logic.ml

   1 (*
   2   File:        mk_state_logic.ml
   3
   4   Description: This file defines the state abstracted logical
   5                operators used in unity and some theorems valid for
   6                the combination of these operators.
   7
   8   Author:       (c) Copyright 1989-2008 by Flemming Andersen
   9   Date:         October 23, 1989
  10   Last Update:  December 30, 2007
  11
  12 *)
  13
  14 (* loadt"aux_definitions.ml";; *)
  15
  16 let FALSE_def   = new_definition (`(False:'a->bool)  = \s:'a. F`);;
  17 let TRUE_def    = new_definition (`(True:'a->bool)   = \s:'a. T`);;
  18 let NOT_def1    = new_definition (`Not (p:'a->bool) = \s. ~p s`);;
  19 let NOT_def2    = new_definition (`~* (p:'a->bool)  = \s. ~p s`);;
  20
  21 let AND_def     = new_infix_definition
  22 ("/\*", "/\\", `/\* (p:'a->bool) (q:'a->bool) = \s. (p s) /\ (q s)`, OP_FIX);;
  23 let OR_def      = new_infix_definition
  24 ("\/*", "\/", `\/* (p:'a->bool) (q:'a->bool) = \s. (p s) \/ (q s)`, OP_FIX);;
  25
  26 let FORALL_def  = new_binder_definition
  27    (`!* (P:'b->('a->bool)) = (\s. (!x. ((P x)s)))`) "!*";;
  28 let EXISTS_def  = new_binder_definition
  29    (`?* (P:'b->('a->bool)) = (\s. (?x. ((P x)s)))`) "?*";;
  30 let CHOICE_def  = new_binder_definition
  31    (`@* P = (\s:'a. (@x:'b. ((P x)s)))`) "@*";;
  32
  33 let IMPLIES_def = new_infix_definition
  34 ("==>*", "==>", `==>* (p:'a->bool) (q:'a->bool) = \s. (p s) ==> (q s)`, OP_FIX);;
  35
  36 let LESS_def = new_infix_definition
  37   ("<*", "<", `<* (p:'a->num) (q:'a->num) = \s. (p s) < (q s)`, OP_FIX);;
  38 let GREATER_def = new_infix_definition
  39   (">*", ">", `>* (p:'a->num) (q:'a->num) = \s. (p s) > (q s)`, OP_FIX);;
  40 let LESS_EQ_def = new_infix_definition
  41   ("<=*", "<=", `<=* (p:'a->num) (q:'a->num) = \s. (p s) <= (q s)`, OP_FIX);;
  42 let GREATER_EQ_def = new_infix_definition
  43   (">=*", ">=", `>=* (p:'a->num) (q:'a->num) = \s. (p s) >= (q s)`, OP_FIX);;
  44 let EQ_def = new_infix_definition
  45   ("=*", "=", `=* (p:'a->'b) (q:'a->'b) = \s. (p s) = (q s)`, OP_FIX);;
  46 let NEQ_def = new_infix_definition
  47   ("<>*", "=", `<>* (p:'a->'b) (q:'a->'b) = \s. ~((p s) = (q s))`, OP_FIX);;
  48 let GE_def = new_infix_definition
  49   ("=>*", "<=>", `=>* (p:'a->bool) (r1:'a->'b) (r2:'a->'b) =
  50                         \s. if (p s) then r1 s else r2 s`, OP_FIX);;
  51 let PLUS_def = new_infix_definition
  52   ("+*", "+", `+* (p:'a->num) (q:'a->num) = \s. (p s) + (q s)`, OP_FIX);;
  53 let SUB_def = new_infix_definition
  54   ("-*", "-", `-* (p:'a->num) (q:'a->num) = \s. (p s) - (q s)`, OP_FIX);;
  55 let MUL_def = new_infix_definition
  56   ("**", "*", `(**) (p:'a->num) (q:'a->num) = \s. ((p s) * (q s))`, OP_FIX);;
  57 let SUC_def = new_definition
  58   (`Suc (p:'a->num) = \s. SUC (p s)`);;
  59 let PRE_def = new_definition
  60   (`Pre (p:'a->num) = \s. PRE (p s)`);;
  61 let MOD_def = new_infix_definition
  62   ("%*", "MOD", `%* (p:'a->num) (q:'a->num) = \s. (p s) MOD (q s)`, OP_FIX);;
  63 let DIV_def = new_infix_definition
  64   ("/*", "/", `/* (p:'a->num) (q:'a->num) = \s. (p s) DIV (q s)`, OP_FIX);;
  65 let EXP_def = new_infix_definition
  66   ("***", "EXP", `*** (p:'a->num) (q:'a->num) = \s. (p s) EXP (q s)`, OP_FIX);;
  67
  68 (* State dependent index *)
  69 (* Weakness in defining priority: does o have same prio as Ind? *)
  70 let IND_def = new_infix_definition
  71   ("Ind", "o", `Ind (a:'a->('b->'c)) (i:'a->'b) = \s. (a s) (i s)`, OP_FIX);;
  72
  73 (* More State dependent operators to be defined ??? *)
  74
  75 (*  Be aware that (!i :: i <= m. P i) = (!i. i <= m ==> P i) *)
  76 let FORALL_LE_def = new_definition
  77    (`!<=* (P:num->('a->bool)) m = (\s:'a. (!i. i <= m ==> ((P i)s)))`);;
  78
  79 (*  Be aware that ?i :: i <= m. P i == ?i. i <= m /\ P i *)
  80 let EXISTS_LE_def = new_definition
  81    (`?<=* (P:num->('a->bool)) m = (\s:'a. (?i. i <= m /\ ((P i)s)))`);;
  82
  83 let EXISTS_LT_def = new_definition
  84    (`?<* (P:num->('a->bool)) m = (\s:'a. (?i. i < m /\ ((P i)s)))`);;
  85
  86 let AND_LE_N_def = new_recursive_definition
  87    num_RECURSION
  88    (`(!P. /<=\* P 0       = (P:num->('a->bool)) 0) /\
  89      (!P. /<=\* P (SUC i) = ((/<=\* P i) /\* (P (SUC i))))`);;
  90
  91 let OR_LE_N_def = new_recursive_definition
  92    num_RECURSION
  93    (`(!P. \<=/* P 0       = (P:num->('a->bool)) 0) /\
  94      (!P. (\<=/* P (SUC i)) = ((\<=/* P i) \/* (P (SUC i))))`);;
  95
  96 let AND_LT_N_def = new_recursive_definition
  97    num_RECURSION
  98    (`(!P. /<\* P 0       = (False:'a->bool)) /\
  99      (!P. /<\* P (SUC i) = ((/<\* P i) /\* (P i)))`);;
 100
 101 let OR_LT_N_def = new_recursive_definition
 102    num_RECURSION
 103    (`(!P. \</* P 0       = (False:'a->bool)) /\
 104      (!P. \</* P (SUC i) = ((\</* P i) \/* (P i)))`);;
 105
 106 (*-------------------------------------------------------------------------*)
 107 (* Theorems valid in this theory                                           *)
 108 (*-------------------------------------------------------------------------*)
 109
 110 let s  = `s:'a`;;
 111 let p  = `p:'a->bool`;;
 112 let q  = `q:'a->bool`;;
 113 let r  = `r:'a->bool`;;
 114 let i  = `i:num`;;
 115 let P  = `P:num->('a->bool)`;;
 116
 117 let IMPLY_WEAK_lemma1 = prove_thm
 118    ("IMPLY_WEAK_lemma1",
 119     (`!p q p' q' (s:'a).
 120          ( (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')) s ) ==> ((q \/* q') s)`),
 121     REPEAT(GEN_TAC) THEN
 122     REWRITE_TAC [AND_def; OR_def] THEN
 123     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 124     REWRITE_TAC [(SYM (SPEC_ALL DISJ_ASSOC))] THEN
 125     REPEAT STRIP_TAC THENL
 126       [ASM_REWRITE_TAC [];
 127        ASM_REWRITE_TAC [];
 128        ASM_REWRITE_TAC []]);;
 129
 130 let IMPLY_WEAK_lemma2 = prove_thm
 131    ("IMPLY_WEAK_lemma2",
 132     `!p q p' q' (s:'a).
 133          ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q'))s
 134        ==>
 135          (q \/* q')s`,
 136     REPEAT GEN_TAC THEN
 137     REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 138     BETA_TAC THEN
 139     REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
 140                  SYM (SPEC_ALL DISJ_ASSOC);
 141                  NOT_CLAUSES;
 142                  DE_MORGAN_THM] THEN
 143     REPEAT STRIP_TAC THENL
 144       [ASM_REWRITE_TAC [];
 145        ASM_REWRITE_TAC [];
 146        ASM_REWRITE_TAC []]);;
 147
 148 let IMPLY_WEAK_lemma3 = prove_thm
 149    ("IMPLY_WEAK_lemma3",
 150     `!p q r (s:'a).
 151          ((((Not p) /\* r) \/* ((Not q) /\* q)) \/* (q /\* r))s
 152        ==>
 153          r s`,
 154     REPEAT GEN_TAC THEN
 155     REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 156     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 157     REWRITE_TAC [(SYM (SPEC_ALL DISJ_ASSOC))] THEN
 158     REPEAT STRIP_TAC THEN
 159     RES_TAC);;
 160
 161 let IMPLY_WEAK_lemma4 = prove_thm
 162   ("IMPLY_WEAK_lemma4",
 163    `!p q p' q' r r' (s:'a).
 164         ((((Not(p \/* p')) /\* (p \/* r')) \/*
 165           ((Not(q \/* q')) /\* (q \/* r))) \/*
 166          ((q \/* r) /\* (p \/* r')))s
 167       ==>
 168         ((p /\* q) \/* r \/* r')s`,
 169    REPEAT GEN_TAC THEN
 170    REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 171    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 172    REWRITE_TAC [SYM (SPEC_ALL DISJ_ASSOC);
 173                 GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
 174                 NOT_CLAUSES;
 175                 DE_MORGAN_THM] THEN
 176    REPEAT STRIP_TAC THEN
 177    RES_TAC THEN ASM_REWRITE_TAC []);;
 178
 179 let IMPLY_WEAK_lemma5 = prove_thm
 180   ("IMPLY_WEAK_lemma5",
 181    `!p q r (s:'a).
 182         ((p /\* r) \/* (((p \/* q) /\* (q \/* r)) \/* r)) s
 183       ==>
 184         (q \/* r) s`,
 185    REPEAT GEN_TAC THEN
 186    REWRITE_TAC [AND_def; OR_def] THEN
 187    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 188    REPEAT STRIP_TAC THEN
 189    RES_TAC THEN ASM_REWRITE_TAC []);;
 190
 191 let IMPLY_WEAK_lemma6 = prove_thm
 192   ("IMPLY_WEAK_lemma6",
 193    `!p q b r (s:'a).
 194         ((r /\* q) \/* (p /\* b) \/* (b /\* q)) s
 195       ==>
 196         ((q /\* r) \/* b) s`,
 197    REPEAT GEN_TAC THEN
 198    REWRITE_TAC [AND_def; OR_def] THEN
 199    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 200    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 201
 202 let IMPLY_WEAK_lemma7 = prove_thm
 203   ("IMPLY_WEAK_lemma7",
 204    `!p q b r (s:'a).
 205         (((r /\* q) \/* ((r /\* p) /\* b)) \/* (b /\* q)) s
 206       ==>
 207         ((q /\* r) \/* b) s`,
 208    REPEAT GEN_TAC THEN
 209    REWRITE_TAC [AND_def; OR_def] THEN
 210    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 211    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 212
 213 let CONJ_COMM_DISJ_lemma_a = TAC_PROOF
 214     (([],
 215       `!p q r (s:'a).
 216            (r s /\ q s) \/ p s
 217          ==>
 218            (q s /\ r s) \/ p s`),
 219    REPEAT STRIP_TAC THENL
 220      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 221
 222 let CONJ_COMM_DISJ_lemma_b = TAC_PROOF
 223   (([],
 224     `!p q r (s:'a).
 225          (q s /\ r s) \/ p s
 226        ==>
 227          (r s /\ q s) \/ p s`),
 228    REPEAT STRIP_TAC THENL
 229      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 230
 231 let CONJ_COMM_DISJ_lemma = TAC_PROOF
 232   (([],
 233     `!p q r (s:'a).
 234          (r s /\ q s) \/ p s
 235        <=> (q s /\ r s) \/ p s`),
 236    REPEAT GEN_TAC THEN
 237    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 238                     (SPEC_ALL CONJ_COMM_DISJ_lemma_a)
 239                     (SPEC_ALL CONJ_COMM_DISJ_lemma_b)));;
 240
 241 let AND_COMM_OR_lemma = prove_thm
 242   ("AND_COMM_OR_lemma",
 243    `!(p:'a->bool) q r. ((r /\* q) \/* p) = ((q /\* r) \/* p)`,
 244    REPEAT GEN_TAC THEN
 245    REWRITE_TAC [AND_def; OR_def] THEN
 246    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 247    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] CONJ_COMM_DISJ_lemma)));;
 248
 249 let CONJ_DISJ_COMM_lemma_a = TAC_PROOF
 250   (([],
 251     `!p q r (s:'a).
 252          (p s /\ (r s \/ q s))
 253        ==>
 254          (p s /\ (q s \/ r s))`),
 255    REPEAT STRIP_TAC THENL
 256      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 257       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 258
 259 let CONJ_DISJ_COMM_lemma_b = TAC_PROOF
 260   (([],
 261     `!p q r (s:'a).
 262          (p s /\ (q s \/ r s))
 263         ==>
 264          (p s /\ (r s \/ q s))`),
 265    REPEAT STRIP_TAC THENL
 266      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 267       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 268
 269 let CONJ_DISJ_COMM_lemma = TAC_PROOF
 270   (([],
 271     `!p q r (s:'a).
 272          (p s /\ (r s \/ q s))
 273        = (p s /\ (q s \/ r s))`),
 274    REPEAT GEN_TAC THEN
 275    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 276                     (SPEC_ALL CONJ_DISJ_COMM_lemma_a)
 277                     (SPEC_ALL CONJ_DISJ_COMM_lemma_b)));;
 278
 279 let AND_OR_COMM_lemma = prove_thm
 280   ("AND_OR_COMM_lemma",
 281    `!(p:'a->bool) q r.
 282         p /\* (r \/* q)
 283       = p /\* (q \/* r)`,
 284    REPEAT GEN_TAC THEN
 285    REWRITE_TAC [AND_def; OR_def] THEN
 286    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 287    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] CONJ_DISJ_COMM_lemma)));;
 288
 289 let DISJ_COMM_CONJ_lemma_a = TAC_PROOF
 290   (([],
 291     `!p q r (s:'a).
 292          (r s \/ q s) /\ p s
 293        ==>
 294          (q s \/ r s) /\ p s`),
 295    REPEAT STRIP_TAC THENL
 296      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 297       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 298
 299 let DISJ_COMM_CONJ_lemma_b = TAC_PROOF
 300   (([],
 301     `!p q r (s:'a).
 302          (q s \/ r s) /\ p s
 303        ==>
 304          (r s \/ q s) /\ p s`),
 305    REPEAT STRIP_TAC THENL
 306      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 307       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 308
 309 let DISJ_COMM_CONJ_lemma = TAC_PROOF
 310   (([],
 311     `!p q r (s:'a).
 312          (r s \/ q s) /\ p s
 313        <=> (q s \/ r s) /\ p s`),
 314    REPEAT GEN_TAC THEN
 315    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 316                     (SPEC_ALL DISJ_COMM_CONJ_lemma_a)
 317                     (SPEC_ALL DISJ_COMM_CONJ_lemma_b)));;
 318
 319 let OR_COMM_AND_lemma = prove_thm
 320   ("OR_COMM_AND_lemma",
 321    `!(p:'a->bool) q r.
 322         (r \/* q) /\* p
 323       = (q \/* r) /\* p`,
 324    REPEAT GEN_TAC THEN
 325    REWRITE_TAC [AND_def; OR_def] THEN
 326    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 327    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] DISJ_COMM_CONJ_lemma)));;
 328
 329 let DISJ_COMM_DISJ_lemma_a = TAC_PROOF
 330   (([],
 331     `!p q r (s:'a).
 332          (r s \/ q s) \/ p s
 333        ==>
 334          (q s \/ r s) \/ p s`),
 335    REPEAT STRIP_TAC THENL
 336      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 337
 338 let DISJ_COMM_DISJ_lemma_b = TAC_PROOF
 339   (([],
 340     `!p q r (s:'a).
 341          (q s \/ r s) \/ p s
 342        ==>
 343          (r s \/ q s) \/ p s`),
 344    REPEAT STRIP_TAC THENL
 345      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 346
 347 let DISJ_COMM_DISJ_lemma = TAC_PROOF
 348   (([],
 349     `!(p:'a->bool) q r s. (r s \/ q s) \/ p s <=> (q s \/ r s) \/ p s`),
 350    REPEAT GEN_TAC THEN
 351    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 352                     (SPEC_ALL DISJ_COMM_DISJ_lemma_a)
 353                     (SPEC_ALL DISJ_COMM_DISJ_lemma_b)));;
 354
 355 let OR_COMM_OR_lemma = prove_thm
 356   ("OR_COMM_OR_lemma",
 357    `!(p:'a->bool) q r. (r \/* q) \/* p = (q \/* r) \/* p`,
 358    REPEAT GEN_TAC THEN
 359    REWRITE_TAC [OR_def] THEN
 360    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 361    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] DISJ_COMM_DISJ_lemma)));;
 362
 363 let DISJ_DISJ_COMM_lemma_a = TAC_PROOF
 364   (([], `!p q r (s:'a). p s \/ (r s \/ q s) ==> p s \/ (q s \/ r s)`),
 365    REPEAT STRIP_TAC THENL
 366      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 367
 368 let DISJ_DISJ_COMM_lemma_b = TAC_PROOF
 369   (([], `!p q r (s:'a). p s \/ (q s \/ r s) ==> p s \/ (r s \/ q s)`),
 370    REPEAT STRIP_TAC THENL
 371      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 372
 373 let DISJ_DISJ_COMM_lemma = TAC_PROOF
 374   (([], `!p q r (s:'a). p s \/ (r s \/ q s) <=> p s \/ (q s \/ r s) `),
 375    REPEAT GEN_TAC THEN
 376    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 377                     (SPEC_ALL DISJ_DISJ_COMM_lemma_a)
 378                     (SPEC_ALL DISJ_DISJ_COMM_lemma_b)));;
 379
 380 let OR_OR_COMM_lemma = prove_thm
 381   ("OR_OR_COMM_lemma",
 382    (`!(p:'a->bool) q r. p \/* (r \/* q) = p \/* (q \/* r)`),
 383    REPEAT GEN_TAC THEN
 384    REWRITE_TAC [OR_def] THEN
 385    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 386    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] DISJ_DISJ_COMM_lemma)));;
 387
 388 let CONJ_COMM_CONJ_lemma_a = TAC_PROOF
 389   (([], `!p q r (s:'a). (r s /\ q s) /\ p s ==> (q s /\ r s) /\ p s`),
 390    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 391
 392 let CONJ_COMM_CONJ_lemma_b = TAC_PROOF
 393   (([], `!p q r (s:'a). (q s /\ r s) /\ p s ==> (r s /\ q s) /\ p s`),
 394    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 395
 396 let CONJ_COMM_CONJ_lemma = TAC_PROOF
 397   (([], `!p q r (s:'a). (r s /\ q s) /\ p s <=> (q s /\ r s) /\ p s`),
 398    REPEAT GEN_TAC THEN
 399    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 400                     (SPEC_ALL CONJ_COMM_CONJ_lemma_a)
 401                     (SPEC_ALL CONJ_COMM_CONJ_lemma_b)));;
 402
 403 let AND_COMM_AND_lemma = prove_thm
 404   ("AND_COMM_AND_lemma",
 405    `!(p:'a->bool) q r. (r /\* q) /\* p = (q /\* r) /\* p`,
 406    REPEAT GEN_TAC THEN
 407    REWRITE_TAC [AND_def] THEN
 408    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 409    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] CONJ_COMM_CONJ_lemma)));;
 410
 411 let CONJ_CONJ_COMM_lemma_a = TAC_PROOF
 412   (([], `!p q r (s:'a). p s /\ (r s /\ q s) ==> p s /\ (q s /\ r s)`),
 413    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 414
 415 let CONJ_CONJ_COMM_lemma_b = TAC_PROOF
 416   (([], `!p q r (s:'a). p s /\ (q s /\ r s) ==> p s /\ (r s /\ q s)`),
 417    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 418
 419 let CONJ_CONJ_COMM_lemma = TAC_PROOF
 420   (([], `!p q r (s:'a). p s /\ (r s /\ q s) <=> p s /\ (q s /\ r s) `),
 421    REPEAT GEN_TAC THEN
 422    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 423                     (SPEC_ALL CONJ_CONJ_COMM_lemma_a)
 424                     (SPEC_ALL CONJ_CONJ_COMM_lemma_b)));;
 425
 426 let AND_AND_COMM_lemma = prove_thm
 427   ("AND_AND_COMM_lemma",
 428    `!(p:'a->bool) q r. p /\* (r /\* q) = p /\* (q /\* r)`,
 429    REPEAT GEN_TAC THEN
 430    REWRITE_TAC [AND_def] THEN
 431    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 432    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] CONJ_CONJ_COMM_lemma)));;
 433
 434 let DISJ_CONJ_COMM_lemma_a = TAC_PROOF
 435   (([], `!p q r (s:'a). p s \/ (r s /\ q s) ==> p s \/ (q s /\ r s)`),
 436    REPEAT STRIP_TAC THENL
 437      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 438
 439 let DISJ_CONJ_COMM_lemma_b = TAC_PROOF
 440   (([], `!p q r (s:'a). p s \/ (q s /\ r s) ==> p s \/ (r s /\ q s)`),
 441    REPEAT STRIP_TAC THENL
 442      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 443
 444 let DISJ_CONJ_COMM_lemma = TAC_PROOF
 445   (([], `!p q r (s:'a). p s \/ (r s /\ q s) <=> p s \/ (q s /\ r s)`),
 446    REPEAT GEN_TAC THEN
 447    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 448                     (SPEC_ALL DISJ_CONJ_COMM_lemma_a)
 449                     (SPEC_ALL DISJ_CONJ_COMM_lemma_b)));;
 450
 451 let OR_AND_COMM_lemma = prove_thm
 452   ("OR_AND_COMM_lemma",
 453    `!(p:'a->bool) q r. p \/* (r /\* q) = p \/* (q /\* r)`,
 454    REPEAT GEN_TAC THEN
 455    REWRITE_TAC [AND_def; OR_def] THEN
 456    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 457    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] DISJ_CONJ_COMM_lemma)));;
 458
 459 let NOT_NOT_lemma = prove_thm
 460    ("NOT_NOT_lemma",
 461     `!(p:'a->bool). (Not (Not p)) = p`,
 462     REWRITE_TAC [NOT_def1] THEN
 463     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 464     REWRITE_TAC [NOT_CLAUSES; ETA_AX]);;
 465
 466 let DISJ_COMM_lemma = TAC_PROOF
 467    (([], `!p q (s:'a). p s \/ q s <=> q s \/ p s`),
 468     REPEAT STRIP_TAC THEN
 469     STRIP_ASSUME_TAC
 470       (SPECL [`(p (s:'a)):bool`; `(q (s:'a)):bool`] DISJ_SYM));;
 471
 472 let OR_COMM_lemma = prove_thm
 473    ("OR_COMM_lemma",
 474     `!(p:'a->bool) q. (p \/* q) = (q \/* p)`,
 475     REPEAT STRIP_TAC THEN
 476     REWRITE_TAC [OR_def] THEN
 477     ASSUME_TAC DISJ_COMM_lemma THEN
 478     STRIP_ASSUME_TAC
 479         (MK_ABS (SPECL [p;q]
 480                 (ASSUME (`!(p:'a->bool) q s. p s \/ q s <=> q s \/ p s`)))));;
 481
 482 let OR_OR_lemma = prove_thm
 483    ("OR_OR_lemma",
 484     `!p:'a->bool. p \/* p = p`,
 485     GEN_TAC THEN REWRITE_TAC [OR_def; ETA_AX]);;
 486
 487 let DISJ_ASSOC_lemma = TAC_PROOF
 488    (([], `!p q  r (s:'a). ((p s \/ q s) \/ r s) <=> (p s \/ (q s \/ r s))`),
 489     REWRITE_TAC [(SYM (SPEC_ALL DISJ_ASSOC))]);;
 490
 491 let OR_ASSOC_lemma = prove_thm
 492    ("OR_ASSOC_lemma",
 493     (`!(p:'a->bool) q r. (p \/* q) \/* r = p \/* (q \/* r)`),
 494     REPEAT STRIP_TAC THEN REWRITE_TAC [OR_def]  THEN
 495     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 496     ASSUME_TAC DISJ_ASSOC_lemma THEN
 497     STRIP_ASSUME_TAC
 498    (MK_ABS (SPECL [p;q;r]
 499       (ASSUME (`!p q r (s:'a).
 500                     ((p s \/ q s) \/ r s) <=> (p s \/ (q s \/ r s))`)))));;
 501
 502 let CONJ_WEAK_lemma = TAC_PROOF
 503   (([], `!p q (s:'a). p s /\ q s ==> q s`),
 504     REPEAT STRIP_TAC THEN RES_TAC);;
 505
 506 let AND_IMPLY_WEAK_lemma = prove_thm
 507   ("AND_IMPLY_WEAK_lemma",
 508     `!p q (s:'a). (p /\* q) s ==> q s`,
 509     REWRITE_TAC [AND_def] THEN
 510     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 511     REWRITE_TAC [CONJ_WEAK_lemma]);;
 512
 513 let SYM_CONJ_WEAK_lemma = TAC_PROOF
 514   (([], `!p q (s:'a). p s /\ q s ==> p s`),
 515     REPEAT STRIP_TAC THEN RES_TAC);;
 516
 517 let SYM_AND_IMPLY_WEAK_lemma = prove_thm
 518   ("SYM_AND_IMPLY_WEAK_lemma",
 519     `!p q (s:'a). (p /\* q) s ==> p s`,
 520     REWRITE_TAC [AND_def] THEN
 521     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 522     REWRITE_TAC [SYM_CONJ_WEAK_lemma]);;
 523
 524 let OR_IMPLY_WEAK_lemma = prove_thm
 525   ("OR_IMPLY_WEAK_lemma",
 526    `!p q (s:'a). p s ==> (p \/* q) s`,
 527    REWRITE_TAC [OR_def] THEN
 528    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 529    REPEAT STRIP_TAC THEN
 530    ASM_REWRITE_TAC []);;
 531
 532 let SYM_OR_IMPLY_WEAK_lemma = prove_thm
 533   ("SYM_OR_IMPLY_WEAK_lemma",
 534    `!p q (s:'a). p s ==> (q \/* p) s`,
 535    REWRITE_TAC [OR_def] THEN
 536    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 537    REPEAT STRIP_TAC THEN
 538    ASM_REWRITE_TAC []);;
 539
 540 let IMPLY_WEAK_AND_lemma = prove_thm
 541   ("IMPLY_WEAK_AND_lemma",
 542    `!(p:'a->bool) q r.
 543         (!s. p s ==> q s)
 544       ==>
 545         (!s. (p /\* r) s ==> (q /\* r) s)`,
 546    REWRITE_TAC [AND_def] THEN
 547    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 548    REPEAT STRIP_TAC THENL
 549      [RES_TAC;
 550       RES_TAC THEN
 551       ASM_REWRITE_TAC []]);;
 552
 553 let IMPLY_WEAK_OR_lemma = prove_thm
 554   ("IMPLY_WEAK_OR_lemma",
 555    `!(p:'a->bool) q r.
 556         (!s. p s ==> q s)
 557       ==>
 558         (!s. (p \/* r) s ==> (q \/* r) s)`,
 559    REWRITE_TAC [OR_def] THEN
 560    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 561    REPEAT STRIP_TAC THENL
 562      [RES_TAC THEN
 563       ASM_REWRITE_TAC [];
 564       ASM_REWRITE_TAC []]);;
 565
 566 let AND_AND_lemma = prove_thm
 567   ("AND_AND_lemma",
 568    `!p:'a->bool. p /\* p = p`,
 569    REWRITE_TAC [AND_def; ETA_AX]);;
 570
 571 let CONJ_COMM_lemma = TAC_PROOF
 572   (([],
 573     `!p q (s:'a). (p s /\ q s) <=> (q s /\ p s)`),
 574    REPEAT GEN_TAC THEN
 575    STRIP_ASSUME_TAC (SPECL [`(p:'a->bool) s`; `(q:'a->bool) s`] CONJ_SYM));;
 576
 577 let AND_COMM_lemma = prove_thm
 578    ("AND_COMM_lemma",
 579    (`!(p:'a->bool) q. (p /\* q) = (q /\* p)`),
 580    REWRITE_TAC [AND_def] THEN
 581    REPEAT GEN_TAC THEN
 582    ASSUME_TAC CONJ_COMM_lemma THEN
 583    STRIP_ASSUME_TAC
 584         (MK_ABS (SPECL [p;q]
 585                 (ASSUME (`!p q (s:'a). p s /\ q s <=> q s /\ p s`)))));;
 586
 587 let CONJ_ASSOC_lemma = TAC_PROOF
 588   (([],
 589     `!p q r (s:'a). ((p s /\ q s) /\ r s) <=> (p s /\ (q s /\ r s))`),
 590     REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC))]);;
 591
 592 let AND_ASSOC_lemma = prove_thm
 593    ("AND_ASSOC_lemma",
 594     `!(p:'a->bool) q r. (p /\* q) /\* r = p /\* (q /\* r)`,
 595    REPEAT GEN_TAC THEN REWRITE_TAC [AND_def]  THEN
 596    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 597    ASSUME_TAC CONJ_ASSOC_lemma THEN
 598    STRIP_ASSUME_TAC
 599    (MK_ABS (SPECL [p;q;r]
 600       (ASSUME (`!p q  r (s:'a).
 601                  ((p s /\ q s) /\ r s) <=> (p s /\ (q s /\ r s))`)))));;
 602
 603 let NOT_True_lemma = prove_thm
 604    ("NOT_True_lemma",
 605     `Not (True:'a->bool) = False`,
 606    REWRITE_TAC [NOT_def1; TRUE_def; FALSE_def; ETA_AX]);;
 607
 608 let NOT_False_lemma = prove_thm
 609    ("NOT_False_lemma",
 610     `Not (False:'a->bool) = True`,
 611    REWRITE_TAC [NOT_def1; TRUE_def; FALSE_def; ETA_AX]);;
 612
 613 let AND_True_lemma = prove_thm
 614    ("AND_True_lemma",
 615     `!p:'a->bool. p /\* True = p`,
 616    REWRITE_TAC [AND_def; TRUE_def; ETA_AX]);;
 617
 618 let OR_True_lemma = prove_thm
 619    ("OR_True_lemma",
 620     `!p:'a->bool. p \/* True = True`,
 621    REWRITE_TAC [OR_def; TRUE_def; ETA_AX]);;
 622
 623 let AND_False_lemma = prove_thm
 624    ("AND_False_lemma",
 625     `!p:'a->bool. p /\* False = False`,
 626    REWRITE_TAC [AND_def; FALSE_def; ETA_AX]);;
 627
 628 let OR_False_lemma = prove_thm
 629    ("OR_False_lemma",
 630     `!p:'a->bool. p \/* False = p`,
 631    REWRITE_TAC [OR_def; FALSE_def; ETA_AX]);;
 632
 633 let P_OR_NOT_P_lemma = prove_thm
 634    ("P_OR_NOT_P_lemma",
 635     `!p:'a->bool. p \/* (Not p) = True`,
 636    REWRITE_TAC [OR_def; NOT_def1; TRUE_def] THEN
 637    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 638    REWRITE_TAC [EXCLUDED_MIDDLE; OR_CLAUSES; NOT_CLAUSES; ETA_AX]);;
 639
 640 let P_AND_NOT_P_lemma = prove_thm
 641    ("P_AND_NOT_P_lemma",
 642     `!p:'a->bool. p /\* (Not p) = False`,
 643    REWRITE_TAC [AND_def; NOT_def1; FALSE_def] THEN
 644    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 645    REWRITE_TAC [NOT_AND; AND_CLAUSES; NOT_CLAUSES; ETA_AX]);;
 646
 647 let CONJ_COMPL_DISJ_lemma1 = TAC_PROOF
 648   (([],
 649     `!p q. p /\ ~q \/ p /\ q ==> p`),
 650    REPEAT STRIP_TAC);;
 651
 652 let CONJ_COMPL_DISJ_lemma2 = TAC_PROOF
 653   (([],
 654     `!p q. p ==> p /\ ~q \/ p /\ q`),
 655    REPEAT STRIP_TAC THEN
 656    ASM_REWRITE_TAC [] THEN
 657    PURE_ONCE_REWRITE_TAC [DISJ_SYM] THEN
 658    REWRITE_TAC [EXCLUDED_MIDDLE]);;
 659
 660 let CONJ_COMPL_DISJ_lemma = TAC_PROOF
 661   (([],
 662     `!p q. p /\ ~q \/ p /\ q <=> p`),
 663    REWRITE_TAC [IMP_ANTISYM_RULE
 664                   (SPEC_ALL CONJ_COMPL_DISJ_lemma1)
 665                   (SPEC_ALL CONJ_COMPL_DISJ_lemma2)]);;
 666
 667 let AND_COMPL_OR_lemma = prove_thm
 668    ("AND_COMPL_OR_lemma",
 669     `!(p:'a->bool) q. ((p /\* (Not q)) \/* (p /\* q)) = p`,
 670    REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 671    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 672    REWRITE_TAC [CONJ_COMPL_DISJ_lemma; ETA_AX]);;
 673
 674 let DISJ_NOT_CONJ_lemma1 = TAC_PROOF
 675   (([],
 676     `!p q. (p \/ q) /\ ~q ==> p /\ ~q`),
 677     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN RES_TAC);;
 678
 679 let DISJ_NOT_CONJ_lemma2 = TAC_PROOF
 680   (([],
 681     `!p q. p /\ ~q ==> (p \/ q) /\ ~q`),
 682     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN RES_TAC);;
 683
 684 let DISJ_NOT_CONJ_lemma = TAC_PROOF
 685   (([], `!p q. (p \/ q) /\ ~q <=> p /\ ~q`),
 686    REWRITE_TAC [IMP_ANTISYM_RULE
 687                   (SPEC_ALL DISJ_NOT_CONJ_lemma1)
 688                   (SPEC_ALL DISJ_NOT_CONJ_lemma2)]);;
 689
 690 let OR_NOT_AND_lemma = prove_thm
 691   ("OR_NOT_AND_lemma",
 692    `!(p:'a->bool) q. ((p \/* q) /\* (Not q)) = p /\* (Not q)`,
 693    REPEAT GEN_TAC THEN
 694    REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 695    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 696    REWRITE_TAC [DISJ_NOT_CONJ_lemma]);;
 697
 698 let P_CONJ_Q_DISJ_Q_lemma1 = TAC_PROOF
 699   (([], `!(p:'a->bool) q s. (p s /\ q s) \/ q s ==> q s`),
 700    REPEAT STRIP_TAC);;
 701
 702 let P_CONJ_Q_DISJ_Q_lemma2 = TAC_PROOF
 703   (([], `!(p:'a->bool) q s. q s ==> (p s /\ q s) \/ q s`),
 704    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 705
 706 let P_CONJ_Q_DISJ_Q_lemma = TAC_PROOF
 707   (([], `!(p:'a->bool) q s. (p s /\ q s) \/ q s <=> q s`),
 708    ASM_REWRITE_TAC [IMP_ANTISYM_RULE
 709                          (SPEC_ALL P_CONJ_Q_DISJ_Q_lemma1)
 710                          (SPEC_ALL P_CONJ_Q_DISJ_Q_lemma2)]);;
 711
 712 let P_AND_Q_OR_Q_lemma = prove_thm
 713   ("P_AND_Q_OR_Q_lemma",
 714    `!(p:'a->bool) q. (p /\* q) \/* q = q`,
 715    REPEAT GEN_TAC THEN
 716    REWRITE_TAC [AND_def; OR_def] THEN
 717    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 718    REWRITE_TAC [GEN_ALL (MK_ABS (SPECL [p;q] P_CONJ_Q_DISJ_Q_lemma)); ETA_AX]);;
 719
 720 let P_DISJ_Q_CONJ_Q_lemma1 = TAC_PROOF
 721   (([], `!(p:'a->bool) q s. (p s \/ q s) /\ q s ==> q s`),
 722    REPEAT STRIP_TAC);;
 723
 724 let P_DISJ_Q_CONJ_Q_lemma2 = TAC_PROOF
 725   (([], `!(p:'a->bool) q s. q s ==> (p s \/ q s) /\ q s`),
 726    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 727
 728 let P_DISJ_Q_CONJ_Q_lemma = TAC_PROOF
 729   (([], `!(p:'a->bool) q s. (p s \/ q s) /\ q s <=> q s`),
 730    ASM_REWRITE_TAC [IMP_ANTISYM_RULE
 731                          (SPEC_ALL P_DISJ_Q_CONJ_Q_lemma1)
 732                          (SPEC_ALL P_DISJ_Q_CONJ_Q_lemma2)]);;
 733
 734 let P_OR_Q_AND_Q_lemma = prove_thm
 735   ("P_OR_Q_AND_Q_lemma",
 736    `!(p:'a->bool) q. (p \/* q) /\* q = q`,
 737    REPEAT GEN_TAC THEN
 738    REWRITE_TAC [AND_def; OR_def] THEN
 739    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 740    REWRITE_TAC [GEN_ALL (MK_ABS (SPECL [p;q] P_DISJ_Q_CONJ_Q_lemma)); ETA_AX]);;
 741
 742 let NOT_OR_AND_NOT_lemma = prove_thm
 743   ("NOT_OR_AND_NOT_lemma",
 744    `!(p:'a->bool) q. Not (p \/* q) = (Not p) /\* (Not q)`,
 745    REPEAT GEN_TAC THEN
 746    REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 747    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 748    REWRITE_TAC [NOT_CLAUSES;
 749                 DE_MORGAN_THM]);;
 750
 751 let NOT_AND_OR_NOT_lemma = prove_thm
 752   ("NOT_AND_OR_NOT_lemma",
 753    `!(p:'a->bool) q. Not (p /\* q) = (Not p) \/* (Not q)`,
 754       REPEAT GEN_TAC THEN
 755    REWRITE_TAC [NOT_def1; AND_def; OR_def] THEN
 756    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 757    REWRITE_TAC [NOT_CLAUSES;
 758                 DE_MORGAN_THM]);;
 759
 760 let NOT_IMPLY_OR_lemma = prove_thm
 761   ("NOT_IMPLY_OR_lemma",
 762    `!(p:'a->bool) q.
 763         (!s. (Not p)s ==> q s)
 764       = (!s. (p \/* q)s)`,
 765    REPEAT GEN_TAC THEN
 766    REWRITE_TAC [NOT_def1; OR_def] THEN
 767    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 768    REWRITE_TAC [IMP_DISJ_THM]);;
 769
 770 let IMPLY_OR_lemma = prove_thm
 771   ("IMPLY_OR_lemma",
 772    `!(p:'a->bool) q. (!s. p s ==> q s) = (!s. ((Not p) \/* q)s)`,
 773    REPEAT GEN_TAC THEN
 774    REWRITE_TAC [NOT_def1; OR_def] THEN
 775    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 776    REWRITE_TAC [IMP_DISJ_THM]);;
 777
 778 let OR_IMPLY_lemma = prove_thm
 779   ("OR_IMPLY_lemma",
 780    `!(p:'a->bool) q. (!s. (p \/* q)s) = (!s. (Not p)s ==> q s)`,
 781    REPEAT GEN_TAC THEN
 782    REWRITE_TAC [NOT_def1; OR_def] THEN
 783    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 784    REWRITE_TAC [IMP_DISJ_THM; NOT_CLAUSES]);;
 785
 786 let NOT_OR_IMPLY_lemma = prove_thm
 787   ("NOT_OR_IMPLY_lemma",
 788    `!(p:'a->bool) q. (!s. ((Not p) \/* q)s) = (!s. p s ==> q s)`,
 789    REPEAT GEN_TAC THEN
 790    REWRITE_TAC [NOT_def1; OR_def] THEN
 791    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 792    REWRITE_TAC [IMP_DISJ_THM; NOT_CLAUSES]);;
 793
 794 let DISJ_CONJ_lemma1 = TAC_PROOF
 795   (([],
 796     `!p q r (s:'a).
 797          (p s \/ q s /\ r s)
 798        ==>
 799          ((p s \/ q s) /\ (p s \/ r s))`),
 800    REPEAT STRIP_TAC THENL
 801      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 802       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 803
 804 let DISJ_CONJ_lemma2 = TAC_PROOF
 805   (([], `!(p:'a->bool) q r s.
 806              ((p s \/ q s) /\ (p s \/ r s)) ==> (p s \/ q s /\ r s)`),
 807    REPEAT STRIP_TAC THENL
 808      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 809       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 810
 811 let DISJ_CONJ_lemma = TAC_PROOF
 812   (([], `!(p:'a->bool) q r s.
 813             (p s \/ q s /\ r s) <=> ((p s \/ q s) /\ (p s \/ r s))`),
 814    REWRITE_TAC [IMP_ANTISYM_RULE
 815                       (SPEC_ALL DISJ_CONJ_lemma1)
 816                       (SPEC_ALL DISJ_CONJ_lemma2)]);;
 817
 818 let OR_AND_DISTR_lemma = prove_thm
 819   ("OR_AND_DISTR_lemma",
 820    `!(p:'a->bool) q r. p \/* (q /\* r) = (p \/* q) /\* (p \/* r)`,
 821    REPEAT GEN_TAC THEN
 822    REWRITE_TAC [AND_def; OR_def] THEN
 823    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 824    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] DISJ_CONJ_lemma)));;
 825
 826 let CONJ_DISJ_lemma1 = TAC_PROOF
 827   (([], `!(p:'a->bool) q r s.
 828             (p s /\ (q s \/ r s)) ==> (p s /\ q s \/ p s /\ r s)`),
 829    REPEAT STRIP_TAC THENL
 830      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 831
 832 let CONJ_DISJ_lemma2 = TAC_PROOF
 833   (([], `!(p:'a->bool) q r s.
 834             (p s /\ q s \/ p s /\ r s) ==> (p s /\ (q s \/ r s))`),
 835    REPEAT STRIP_TAC THENL
 836      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC [];
 837       ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 838
 839 let CONJ_DISJ_lemma = TAC_PROOF
 840   (([], `!(p:'a->bool) q r s.
 841             (p s /\ (q s \/ r s)) <=> (p s /\ q s \/ p s /\ r s)`),
 842    REWRITE_TAC [IMP_ANTISYM_RULE
 843                       (SPEC_ALL CONJ_DISJ_lemma1)
 844                       (SPEC_ALL CONJ_DISJ_lemma2)]);;
 845
 846 let AND_OR_DISTR_lemma = prove_thm
 847   ("AND_OR_DISTR_lemma",
 848    `!(p:'a->bool) q r. p /\* (q \/* r) = (p /\* q) \/* (p /\* r)`,
 849    REPEAT GEN_TAC THEN
 850    REWRITE_TAC [AND_def; OR_def] THEN
 851    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 852    STRIP_ASSUME_TAC (MK_ABS (SPECL [p;q;r] CONJ_DISJ_lemma)));;
 853
 854 let NOT_IMPLIES_False_lemma = prove_thm
 855   ("NOT_IMPLIES_False_lemma",
 856    `!(p:'a->bool). (!s. (Not p)s) ==> (!s. p s = False s)`,
 857    REWRITE_TAC [FALSE_def; NOT_def1] THEN
 858    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 859    REWRITE_TAC []);;
 860
 861 let NOT_P_IMPLIES_P_EQ_False_lemma = prove_thm
 862   ("NOT_P_IMPLIES_P_EQ_False_lemma",
 863    `!(p:'a->bool). (!s. (Not p)s) ==> (p = False)`,
 864    REPEAT STRIP_TAC THEN
 865    ASSUME_TAC (MK_ABS (UNDISCH_ALL (SPEC_ALL NOT_IMPLIES_False_lemma))) THEN
 866    UNDISCH_TAC (`(\s:'a. p s) = (\s. False s)`) THEN
 867    REWRITE_TAC [ETA_AX]);;
 868
 869 let NOT_AND_IMPLIES_lemma = prove_thm
 870   ("NOT_AND_IMPLIES_lemma",
 871    `!(p:'a->bool) q. (!s. (Not (p /\* q))s) <=> (!s. p s ==> Not q s)`,
 872    REWRITE_TAC [NOT_def1; AND_def] THEN
 873    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 874    REWRITE_TAC [DE_MORGAN_THM; NOT_CLAUSES; IMP_DISJ_THM]);;
 875
 876 let NOT_AND_IMPLIES_lemma1 = prove_thm
 877   ("NOT_AND_IMPLIES_lemma1",
 878    `!(p:'a->bool) q. (!s. (Not (p /\* q))s) ==> (!s. p s ==> Not q s)`,
 879    REWRITE_TAC [NOT_AND_IMPLIES_lemma]);;
 880
 881 let NOT_AND_IMPLIES_lemma2 = prove_thm
 882   ("NOT_AND_IMPLIES_lemma2",
 883    `!(p:'a->bool) q. (!s. (Not (p /\* q))s) ==> (!s. q s ==> Not p s)`,
 884    REWRITE_TAC [NOT_AND_IMPLIES_lemma; NOT_def1] THEN
 885    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 886    REPEAT STRIP_TAC THEN
 887    RES_TAC);;
 888
 889 let CONJ_DISJ_IMPLY_lemma1 = TAC_PROOF
 890    (([], `!(p:'a->bool) q s. p s /\ (p s \/ q s) ==> p s`),
 891    REPEAT STRIP_TAC);;
 892
 893 let CONJ_DISJ_IMPLY_lemma2 = TAC_PROOF
 894    (([], `!(p:'a->bool) q s. p s ==> p s /\ (p s \/ q s)`),
 895    REPEAT STRIP_TAC THENL
 896      [ASM_REWRITE_TAC []; ASM_REWRITE_TAC []]);;
 897
 898 let CONJ_DISJ_IMPLY_lemma = TAC_PROOF
 899   (([], `!(p:'a->bool) q s. p s /\ (p s \/ q s) <=> p s`),
 900    REWRITE_TAC [IMP_ANTISYM_RULE
 901                   (SPEC_ALL CONJ_DISJ_IMPLY_lemma1)
 902                   (SPEC_ALL CONJ_DISJ_IMPLY_lemma2)]);;
 903
 904 let CONJ_DISJ_ABS_IMPLY_lemma = TAC_PROOF
 905   (([], `!(p:'a->bool) q.  (\s. p s /\ (p s \/ q s)) = p`),
 906    REPEAT GEN_TAC THEN
 907    REWRITE_TAC [CONJ_DISJ_IMPLY_lemma; ETA_AX]);;
 908
 909 let AND_OR_EQ_lemma = prove_thm
 910   ("AND_OR_EQ_lemma",
 911    `!(p:'a->bool) q. p /\* (p \/* q) = p`,
 912    REPEAT GEN_TAC THEN
 913    REWRITE_TAC [AND_def; OR_def] THEN
 914    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 915    REWRITE_TAC [CONJ_DISJ_ABS_IMPLY_lemma]);;
 916
 917 let AND_OR_EQ_AND_COMM_OR_lemma = prove_thm
 918   ("AND_OR_EQ_AND_COMM_OR_lemma",
 919    `!(p:'a->bool) q. p /\* (q \/* p) = p /\* (p \/* q)`,
 920    REPEAT GEN_TAC THEN
 921    REWRITE_TAC [AND_OR_EQ_lemma] THEN
 922    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 923    REWRITE_TAC [AND_OR_EQ_lemma]);;
 924
 925 let IMPLY_WEAK_lemma = prove_thm
 926   ("IMPLY_WEAK_lemma",
 927    `!(p:'a->bool) q. (!s. p s) ==> (!s. (p \/* q) s)`,
 928    REPEAT STRIP_TAC THEN
 929    REWRITE_TAC [OR_def] THEN
 930    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 931    ASM_REWRITE_TAC []);;
 932
 933 let IMPLY_WEAK_lemma_b = prove_thm
 934   ("IMPLY_WEAK_lemma_b",
 935    `!(p:'a->bool) q s. p s ==> (p \/* q) s`,
 936    REPEAT STRIP_TAC THEN
 937    REWRITE_TAC [OR_def] THEN
 938    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 939    ASM_REWRITE_TAC []);;
 940
 941 let ALL_AND_lemma1 = TAC_PROOF
 942   (([],
 943    `!(P:num->('a->bool)) i s. (!i. P i s) <=> (P i s /\ (!i. P i s))`),
 944    REPEAT STRIP_TAC THEN
 945    EQ_TAC THENL
 946      [
 947       REPEAT STRIP_TAC THENL
 948         [
 949          ASM_REWRITE_TAC []
 950         ;
 951          ASM_REWRITE_TAC []
 952         ];
 953       REPEAT STRIP_TAC THEN
 954       ASM_REWRITE_TAC []]);;
 955
 956 let ALL_OR_lemma1 = TAC_PROOF
 957   (([],
 958    `!(P:num->('a->bool)) i s. (?i. P i s) <=> (P i s \/ (?i. P i s))`),
 959    REPEAT GEN_TAC THEN
 960    EQ_TAC THENL
 961    [
 962      REPEAT STRIP_TAC THEN
 963      DISJ2_TAC THEN
 964      EXISTS_TAC (`i':num`) THEN
 965      ASM_REWRITE_TAC []
 966     ;
 967      REPEAT STRIP_TAC THENL
 968      [
 969        EXISTS_TAC (`i:num`) THEN
 970        ASM_REWRITE_TAC []
 971       ;
 972        EXISTS_TAC (`i:num`) THEN
 973        ASM_REWRITE_TAC []
 974      ]
 975    ]);;
 976
 977 let ALL_OR_lemma = prove_thm
 978   ("ALL_OR_lemma",
 979    `!(P:num->('a->bool)) i. (((?*) P) = ((P i) \/* ((?*) P)))`,
 980    GEN_TAC THEN GEN_TAC THEN
 981    REWRITE_TAC [EXISTS_def; OR_def] THEN
 982    BETA_TAC THEN
 983    STRIP_ASSUME_TAC (MK_ABS (SPECL [P;i] ALL_OR_lemma1)));;
 984
 985 let ALL_i_OR_lemma1 = TAC_PROOF
 986   (([],
 987     `!P (s:'a). (?i. \<=/* P i s) = (?i. P i s)`),
 988    REPEAT STRIP_TAC THEN
 989    EQ_TAC THENL
 990      [
 991       STRIP_TAC THEN
 992       UNDISCH_TAC (`\<=/* (P:num->('a->bool)) i s`) THEN
 993       SPEC_TAC (i,i) THEN
 994       INDUCT_TAC THENL
 995         [
 996          REWRITE_TAC [OR_LE_N_def] THEN
 997          DISCH_TAC THEN
 998          EXISTS_TAC (`0`) THEN
 999          ASM_REWRITE_TAC []
1000         ;
1001          REWRITE_TAC [OR_LE_N_def; OR_def] THEN
1002          BETA_TAC THEN
1003          REPEAT STRIP_TAC THENL
1004            [
1005             RES_TAC THEN
1006             EXISTS_TAC (`i':num`) THEN
1007             ASM_REWRITE_TAC []
1008            ;
1009             EXISTS_TAC (`SUC i`) THEN
1010             ASM_REWRITE_TAC []
1011            ]
1012         ]
1013      ;
1014       STRIP_TAC THEN
1015       UNDISCH_TAC (`(P (i:num) (s:'a)):bool`) THEN
1016       SPEC_TAC (i,i) THEN
1017       INDUCT_TAC THENL
1018         [
1019          DISCH_TAC THEN
1020          EXISTS_TAC (`0`) THEN
1021          ASM_REWRITE_TAC [OR_LE_N_def]
1022         ;
1023          DISCH_TAC THEN
1024          EXISTS_TAC (`SUC i`) THEN
1025          REWRITE_TAC [OR_LE_N_def; OR_def] THEN
1026          BETA_TAC THEN
1027          ASM_REWRITE_TAC []
1028         ]
1029      ]);;
1030
1031 let ALL_i_OR_lemma = prove_thm
1032   ("ALL_i_OR_lemma",
1033    (`!P. ((\s:'a. ?i. \<=/* P i s) = ((?*) P))`),
1034    REWRITE_TAC [EXISTS_def] THEN
1035    GEN_TAC THEN
1036    STRIP_ASSUME_TAC (MK_ABS (SPEC P ALL_i_OR_lemma1)));;