Unity/mk_unless.ml

   1 (*-------------------------------------------------------------------------*)
   2 (*
   3    File:         mk_unless.ml
   4    Description:
   5
   6    This file defines the theorems for the UNLESS definition.
   7
   8    Author:       (c) Copyright 1989-2008 by Flemming Andersen
   9    Date:         June 29, 1989
  10    Last Update:  December 30, 2007
  11 *)
  12 (*-------------------------------------------------------------------------*)
  13
  14
  15 (*-------------------------------------------------------------------------*)
  16 (* The definition of UNLESS is based on the definition:
  17
  18       p UNLESS q in Pr = <!s in Pr: {p /\ ~q} s {p \/ q}>
  19
  20   where p and q are state dependent first order logic predicates or all
  21   s in the program Pr are conditionally enabled statements transforming
  22   a state into a new state.
  23
  24   To define UNLESS as a relation UNLESS_STMT to be satisfied for a finite
  25   number of program statements, we define the UNLESS_STMT to be fulfilled as
  26   a separate HOARE tripple relation between pre- or post predicates to be
  27   satisfied for state transitions. The pre- or post predicates of the
  28   UNLESS_STMT relation must be satisfiable for all states possible in the
  29   finite state space of the program.
  30 *)
  31
  32 let TL_FIX = 100;;
  33
  34 let UNLESS_STMT = new_infix_definition
  35   ("UNLESS_STMT", "<=>",
  36    `UNLESS_STMT (p:'a->bool) q st =
  37       \s:'a. (p s /\ ~q s) ==> (p (st s) \/ q (st s))`, TL_FIX);;
  38
  39 (*
  40   Since a program is defined as a set (list) of statements, we
  41   recursively define the UNLESS relation itself using the UNLESS_STMT
  42   relation to be satisfied for every statement in the program.
  43
  44   As the bottom of the recursion we choose the empty program always to be
  45   satisfied. For every statement in the program the UNLESS_STMT relation
  46   must be satisfied in all possible states.
  47 *)
  48
  49 let UNLESS_term =
  50   (`(!p q. UNLESS p q  []                   <=> T) /\
  51     (!p q. UNLESS p q (CONS (st:'a->'a) Pr) <=>
  52      ((!s:'a. (p UNLESS_STMT q) st s) /\ (UNLESS p q Pr)))`);;
  53 let UNLESS = new_recursive_definition list_RECURSION UNLESS_term;;
  54 parse_as_infix ( "UNLESS", (TL_FIX, "right") );;
  55
  56 let STABLE_STMT = new_infix_definition
  57   ("STABLE_STMT", "<=>",
  58    `STABLE_STMT (p:'a->bool) st = \s:'a. p s ==> p (st s)`, TL_FIX);;
  59
  60 (*
  61 * The state predicate STABLE is a special case of UNLESS.
  62 *
  63 *       stable p in Pr = p unless false in Pr
  64 *)
  65 let STABLE = new_infix_definition
  66   ("STABLE", "<=>", `STABLE (p:'a->bool) Pr = (p UNLESS False) Pr`, TL_FIX);;
  67
  68 (*
  69 *  The state predicate INVARIANT is a special case of UNLESS too.
  70 *  However invariant is dependent of a program /\* its initial state.
  71 *
  72 *       invariant P in (initial condition, Pr) =
  73 *           (initial condition ==> p) /\ (p stable in Pr)
  74 *)
  75 let INVARIANT = new_infix_definition
  76   ("INVARIANT", "<=>",
  77    `INVARIANT p (p0, Pr) = ((!s:'a. p0 s ==> p s) /\ (p STABLE Pr))`, TL_FIX);;
  78
  79 (************************************************************************
  80 *                                                                       *
  81 * Lemmas used in the UNLESS Theory                                      *
  82 *                                                                       *
  83 ************************************************************************)
  84
  85 let s = `s:'a`;;
  86 let p = `p:'a->bool`;;
  87 let q = `q:'a->bool`;;
  88 let r = `r:'a->bool`;;
  89 let P = `P:num->'a->bool`;;
  90
  91 let IMP_IMP_CONJIMP_lemma = TAC_PROOF
  92   (([],
  93    (`!p q ps qs p' q' p's q's.
  94         (p /\ ~q ==> ps \/ qs) ==> (p' /\ ~q' ==> p's \/ q's) ==>
  95           (p /\ p' /\ (~p \/ ~q') /\ (~p' \/ ~q) /\ (~q \/ ~q') ==>
  96                 ps /\ p's \/ ps /\ q's \/ p's /\ qs \/ qs /\ q's)`)),
  97    REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
  98
  99 let NOT_NOT_OR_lemma = TAC_PROOF
 100   (([],
 101    (`!t1 t2 t3. t1 \/ t2 \/ t3 <=> ~(~t1 /\ ~t2) \/ t3`)),
 102    REWRITE_TAC [NOT_CLAUSES; DE_MORGAN_THM; (SYM (SPEC_ALL DISJ_ASSOC))]);;
 103
 104 let CONJ_IMPLY_THM = TAC_PROOF
 105   (([],
 106    (`!p p' q q'.
 107      ((p \/ p') /\ (p \/ ~q') /\ (p' \/ ~q) /\ (~q \/ ~q')) =
 108      ((p /\ ~q) \/ (p' /\ ~q'))`)),
 109     REPEAT GEN_TAC THEN
 110     EQ_TAC THEN
 111     REPEAT STRIP_TAC THEN REPEAT (ASM_REWRITE_TAC []));;
 112
 113 (************************************************************************
 114 *                                                                       *
 115 * Theorems about UNLESS_STMT                                            *
 116 *                                                                       *
 117 ************************************************************************)
 118
 119 (*
 120  *  The reflexivity theorem:
 121  *
 122  *               p unless_stmt P in Prog
 123  *)
 124 let UNLESS_STMT_thm0 = prove_thm
 125   ("UNLESS_STMT_thm0",
 126     `!p st (s:'a). (p UNLESS_STMT p)st s`,
 127     REPEAT STRIP_TAC THEN
 128     REWRITE_TAC [UNLESS_STMT] THEN
 129     REWRITE_TAC [BETA_CONV (`(\s:'a. p s /\ ~(p s) ==> p (st s))s`)] THEN
 130     REPEAT STRIP_TAC THEN
 131     RES_TAC);;
 132
 133 (*
 134  *  Theorem:
 135  *               p unless_stmt Q in stmt, q ==> r
 136  *              ------------------------------
 137  *                   p unless_stmt r in stmt
 138  *)
 139
 140 let UNLESS_STMT_thm1 = prove_thm
 141   ("UNLESS_STMT_thm1",
 142    `!(p:'a->bool) q r st.
 143       ((!s. (p UNLESS_STMT q) st s) /\ (!s. (q s) ==> (r s))) ==>
 144        (!s. (p UNLESS_STMT r) st s)`,
 145    REPEAT GEN_TAC THEN
 146    REWRITE_TAC [UNLESS_STMT] THEN
 147    REPEAT STRIP_TAC THEN
 148    ASSUME_TAC (REWRITE_RULE [ASSUME `~r (s:'a)`]
 149      ( CONTRAPOS (SPEC `s:'a` (ASSUME `!s:'a. q s ==> r s`)))) THEN
 150    STRIP_ASSUME_TAC (REWRITE_RULE [ASSUME `(p:'a->bool) s`; ASSUME `~q (s:'a)`]
 151      (SPEC `s:'a` (ASSUME `!s:'a. p s /\ ~q s ==> p (st s) \/ q (st s)`))) THEN
 152    ASM_REWRITE_TAC [] THEN
 153    STRIP_ASSUME_TAC (REWRITE_RULE [ASSUME `(q:'a->bool) ((st:'a->'a) s)`]
 154      (SPEC `(st:'a->'a) s` (ASSUME `!s:'a. q s ==> r s`))) THEN
 155    ASM_REWRITE_TAC []);;
 156
 157 (*
 158    Theorem:
 159                 p unless_stmt Q in st, p' unless_stmt q' in st
 160                ------------------------------------------------
 161                         p\/p' unless_stmt q\/q' in st
 162 *)
 163 let UNLESS_STMT_thm2 = prove_thm
 164   ("UNLESS_STMT_thm2",
 165    `!p q p' q' (st:'a->'a).
 166     ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
 167      (!s. ((p \/* p') UNLESS_STMT (q \/* q')) st s)`,
 168     REWRITE_TAC [UNLESS_STMT;OR_def] THEN
 169     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 170     REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
 171                  (SYM (SPEC_ALL DISJ_ASSOC)); NOT_CLAUSES; DE_MORGAN_THM] THEN
 172     (REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []));;
 173
 174 (*
 175   Conjunction Theorem:
 176                p unless_stmt Q in stmt, p' unless_stmt q' in stmt
 177      ------------------------------------------------------------------
 178      (p /\ p') unless_stmt (p /\ q') \/ (p' /\ q) \/ (q /\ q') in stmt
 179 *)
 180 let UNLESS_STMT_thm3 = prove_thm
 181   ("UNLESS_STMT_thm3",
 182    `!p q p' q' (st:'a->'a).
 183      ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
 184       (!s. ((p /\* p') UNLESS_STMT
 185            (((p /\* q') \/* (p' /\* q)) \/* (q /\* q'))) st s)`,
 186     PURE_REWRITE_TAC [UNLESS_STMT;AND_def;OR_def] THEN
 187     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 188     REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC));
 189                  (SYM (SPEC_ALL DISJ_ASSOC)); NOT_CLAUSES; DE_MORGAN_THM] THEN
 190     STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
 191     DISCH_TAC THEN STRIP_TAC THEN DISCH_TAC THEN
 192     ASSUME_TAC (CONJUNCT1 (ASSUME
 193        (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s)) /\
 194            (!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
 195     ASSUME_TAC (CONJUNCT2 (ASSUME
 196        (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s)) /\
 197            (!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
 198     STRIP_ASSUME_TAC (SPEC_ALL (ASSUME
 199        (`(!s. p s /\ ~q s ==> p ((st:'a->'a) s) \/ q (st s))`))) THEN
 200     STRIP_ASSUME_TAC (SPEC_ALL (ASSUME
 201        (`(!s. p' s /\ ~q' s ==> p'((st:'a->'a) s) \/ q'(st s))`))) THEN
 202     ASSUME_TAC (UNDISCH_ALL
 203      (SPEC (`(q':'a->bool) ((st:'a->'a) s)`)
 204       (SPEC (`(p':'a->bool) ((st:'a->'a) s)`)
 205        (SPEC (`(q':'a->bool) s`)
 206         (SPEC (`(p':'a->bool) s`)
 207          (SPEC (`(q:'a->bool) ((st:'a->'a) s)`)
 208           (SPEC (`(p:'a->bool) ((st:'a->'a) s)`)
 209            (SPEC (`(q:'a->bool) s`)
 210             (SPEC (`(p:'a->bool) s`)
 211              IMP_IMP_CONJIMP_lemma))))))))) THEN
 212     ASM_REWRITE_TAC []);;
 213
 214 (*
 215   Disjunction Theorem:
 216                p unless_stmt Q in stmt, p' unless_stmt q' in stmt
 217      ------------------------------------------------------------------
 218      (p \/ p') unless_stmt (~p /\ q') \/ (~p' /\ q) \/ (q /\ q') in stmt
 219 *)
 220 let UNLESS_STMT_thm4 = prove_thm
 221   ("UNLESS_STMT_thm4",
 222    `!p q p' q' (st:'a->'a).
 223      ((!s. (p UNLESS_STMT q) st s) /\ (!s. (p' UNLESS_STMT q') st s)) ==>
 224       (!s. ((p \/* p') UNLESS_STMT
 225             ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')))
 226            st s)`,
 227     REPEAT GEN_TAC THEN
 228     PURE_REWRITE_TAC [UNLESS_STMT;AND_def;OR_def;NOT_def1] THEN
 229     MESON_TAC []);;
 230
 231 let UNLESS_STMT_thm5_lemma1 = TAC_PROOF
 232   (([],
 233    `!p q r. (p ==> q) ==> (p \/ r ==> q \/ r)`),
 234    REPEAT STRIP_TAC THENL
 235      [RES_TAC THEN ASM_REWRITE_TAC []
 236      ;ASM_REWRITE_TAC []]);;
 237
 238 let UNLESS_STMT_thm5_lemma2 = TAC_PROOF
 239   (([],
 240    `!(P:num->('a->bool)) q s. ((?n. P n s) \/ q s) = (?n. P n s \/ q s)`),
 241    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
 242     [ EXISTS_TAC (`n:num`) THEN
 243       ASM_REWRITE_TAC []
 244     ; EXISTS_TAC (`n:num`) THEN
 245       ASM_REWRITE_TAC []
 246     ; DISJ1_TAC THEN
 247       EXISTS_TAC (`n:num`) THEN
 248       ASM_REWRITE_TAC []
 249     ; DISJ2_TAC THEN
 250       ASM_REWRITE_TAC []
 251     ]);;
 252
 253 let UNLESS_STMT_thm5 = prove_thm
 254   ("UNLESS_STMT_thm5",
 255    `!(P:num->('a->bool)) q st.
 256           (!m. (!s. ((P m) UNLESS_STMT q)st s)) ==>
 257                (!s. ((\s. ?n. P n s) UNLESS_STMT q)st s)`,
 258    REPEAT GEN_TAC THEN
 259    REWRITE_TAC [UNLESS_STMT] THEN
 260    BETA_TAC THEN
 261    REPEAT STRIP_TAC THEN
 262    REWRITE_TAC [UNLESS_STMT_thm5_lemma2] THEN
 263    EXISTS_TAC (`n:num`) THEN
 264    RES_TAC THEN
 265    ASM_REWRITE_TAC []);;
 266
 267 let UNLESS_STMT_thm6 = prove_thm
 268   ("UNLESS_STMT_thm6",
 269    `!(p:'a->bool) q r (st:'a->'a).
 270       (!s. (p UNLESS_STMT q) st s) ==>
 271          (!s. ((p \/* r) UNLESS_STMT (q \/* r)) st s)`,
 272    REPEAT GEN_TAC THEN
 273    REWRITE_TAC [UNLESS_STMT; OR_def] THEN
 274    MESON_TAC []);;
 275
 276 (*
 277  Theorems about UNLESS
 278 *)
 279
 280 (*
 281   The reflexivity theorem:
 282                p unless p in Prog
 283 *)
 284
 285 let UNLESS_thm1 = prove_thm
 286   ("UNLESS_thm1",
 287    `!(p:'a->bool) Pr. (p UNLESS p) Pr`,
 288    GEN_TAC THEN
 289    LIST_INDUCT_TAC THEN
 290    PURE_REWRITE_TAC [UNLESS] THEN
 291    ASM_REWRITE_TAC [] THEN
 292    PURE_REWRITE_TAC [UNLESS_STMT] THEN
 293    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 294    REPEAT STRIP_TAC THEN
 295    RES_TAC);;
 296
 297 (*
 298 *  The anti reflexivity theorem:
 299 *
 300 *               p unless ~p in Prog
 301 *)
 302 let UNLESS_thm2 = prove_thm
 303   ("UNLESS_thm2",
 304    (`!(p:'a->bool) Pr. (p UNLESS (Not p)) Pr`),
 305    GEN_TAC THEN
 306    LIST_INDUCT_TAC THEN
 307    PURE_REWRITE_TAC [UNLESS] THEN
 308    ASM_REWRITE_TAC [] THEN
 309    PURE_REWRITE_TAC [UNLESS_STMT;NOT_def1] THEN
 310    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 311    REPEAT STRIP_TAC THEN
 312    REWRITE_TAC [EXCLUDED_MIDDLE]);;
 313
 314 (*
 315   The unless implies theorem:
 316                p unless q in Pr, q ==> r
 317               ---------------------------
 318                    p unless r in Pr
 319 *)
 320 let UNLESS_thm3 = prove_thm
 321   ("UNLESS_thm3",
 322    `!(p:'a->bool) q r Pr.
 323       (((p UNLESS q) Pr) /\ (!s. (q s) ==> (r s))) ==> ((p UNLESS r) Pr)`,
 324     GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 325     LIST_INDUCT_TAC THEN
 326     REWRITE_TAC [UNLESS] THEN
 327     STRIP_TAC THEN
 328     ASM_REWRITE_TAC [] THEN
 329     RES_TAC THEN
 330     ASM_REWRITE_TAC [] THEN
 331     IMP_RES_TAC UNLESS_STMT_thm1);;
 332
 333 (*
 334   Conjunction Theorem:
 335                p unless q in Pr, p' unless q' in Pr
 336      -----------------------------------------------------------
 337      (p /\ p') unless (p /\ q') \/ (p' /\ q) \/ (q /\ q') in Pr
 338 *)
 339 let UNLESS_thm4 = prove_thm
 340   ("UNLESS_thm4",
 341    `!(p:'a->bool) q p' q' Pr.
 342       (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
 343         (((p /\* p') UNLESS
 344          (((p /\* q') \/* (p' /\* q)) \/* (q /\* q'))) Pr)`,
 345     GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 346     LIST_INDUCT_TAC THEN
 347     REWRITE_TAC [UNLESS] THEN
 348     STRIP_TAC THEN
 349     ASM_REWRITE_TAC [] THEN
 350     RES_TAC THEN
 351     ASM_REWRITE_TAC [] THEN
 352     IMP_RES_TAC UNLESS_STMT_thm3);;
 353
 354 (*
 355   Disjunction Theorem:
 356                p unless q in Pr, p' unless q' in Pr
 357      -------------------------------------------------------------
 358      (p \/ p') unless (~p /\ q') \/ (~p' /\ q) \/ (q /\ q') in Pr
 359 *)
 360 let UNLESS_thm5 = prove_thm
 361   ("UNLESS_thm5",
 362    `!(p:'a->bool) q p' q' Pr.
 363         (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr))
 364       ==>
 365         (((p \/* p') UNLESS
 366           ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q'))) Pr)`,
 367     GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 368     LIST_INDUCT_TAC THEN
 369     REWRITE_TAC [UNLESS] THEN
 370     STRIP_TAC THEN
 371     ASM_REWRITE_TAC [] THEN
 372     RES_TAC THEN
 373     ASM_REWRITE_TAC [] THEN
 374     IMP_RES_TAC UNLESS_STMT_thm4);;
 375
 376 (*
 377   Simple Conjunction Theorem:
 378                p unless q in Pr, p' unless q' in Pr
 379               -------------------------------------------
 380                     (p /\ p') unless (q \/ q') in Pr
 381 *)
 382 let UNLESS_thm6 = prove_thm
 383   ("UNLESS_thm6",
 384    `!(p:'a->bool) q p' q' Pr.
 385       (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
 386          (((p /\* p') UNLESS (q \/* q')) Pr)`,
 387     REPEAT STRIP_TAC THEN
 388     ASSUME_TAC (UNDISCH_ALL (SPECL
 389          [(`((p:'a->bool) UNLESS q)Pr`);
 390           (`((p':'a->bool) UNLESS q')Pr`)]
 391            AND_INTRO_THM)) THEN
 392     ASSUME_TAC (UNDISCH_ALL (SPEC_ALL UNLESS_thm4)) THEN
 393     ASSUME_TAC (SPECL [(`p:'a->bool`); (`q:'a->bool`);
 394                        (`p':'a->bool`); (`q':'a->bool`)]
 395                        IMPLY_WEAK_lemma1) THEN
 396     ASSUME_TAC (UNDISCH_ALL (SPECL
 397        [(`(((p:'a->bool) /\* p') UNLESS
 398              (((p /\* q') \/* (p' /\* q)) \/* (q /\* q')))Pr`);
 399         (`!s. ((((p:'a->bool) /\* q') \/* (p' /\* q)) \/* (q /\* q'))s ==>
 400                 (q \/* q')s`)]
 401         AND_INTRO_THM)) THEN
 402     ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
 403          [(`(p:'a->bool) /\* p'`);
 404           (`((((p:'a->bool) /\* q') \/* (p' /\* q)) \/* (q /\* q'))`);
 405           (`(q:'a->bool) \/* q'`); (`Pr:('a->'a)list`)]
 406           UNLESS_thm3)]);;
 407
 408 (*
 409   Simple Disjunction Theorem:
 410                p unless Q in Pr, p' unless q' in Pr
 411              ---------------------------------------
 412                  (p \/ p') unless (q \/ q') in Pr
 413 *)
 414 let UNLESS_thm7 = prove_thm
 415   ("UNLESS_thm7",
 416    `!(p:'a->bool) q p' q' Pr.
 417          (((p UNLESS q) Pr) /\ ((p' UNLESS q') Pr)) ==>
 418              (((p \/* p') UNLESS (q \/* q')) Pr)`,
 419     REPEAT STRIP_TAC THEN
 420     ASSUME_TAC (UNDISCH_ALL (SPECL
 421         [(`((p:'a->bool) UNLESS q)Pr`); (`((p':'a->bool) UNLESS q')Pr`)]
 422          AND_INTRO_THM)) THEN
 423     ASSUME_TAC (UNDISCH_ALL (SPEC_ALL UNLESS_thm5)) THEN
 424     ASSUME_TAC (SPECL [(`p:'a->bool`);  (`q:'a->bool`);
 425                        (`p':'a->bool`); (`q':'a->bool`)]
 426                        IMPLY_WEAK_lemma2) THEN
 427     ASSUME_TAC (UNDISCH_ALL (SPECL
 428          [(`(((p:'a->bool) \/* p') UNLESS
 429                ((((Not p) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')))
 430                Pr`);
 431           (`!s. ((((Not (p:'a->bool)) /\* q') \/* ((Not p') /\* q)) \/*
 432                     (q /\* q'))s ==> (q \/* q')s`)]
 433           AND_INTRO_THM)) THEN
 434     STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
 435          [`(p:'a->bool) \/* p'`;
 436           `(((Not (p:'a->bool)) /\* q') \/* ((Not p') /\* q)) \/* (q /\* q')`;
 437           `(q:'a->bool) \/* q'`;
 438           `Pr:('a->'a)list`]
 439            UNLESS_thm3)));;
 440
 441 (*
 442   Cancellation Theorem:
 443                p unless Q in Pr, q unless r in Pr
 444               ------------------------------------
 445                     (p \/ q) unless r in Pr
 446 *)
 447 let UNLESS_thm8 = prove_thm
 448   ("UNLESS_thm8",
 449    `!(p:'a->bool) q r Pr.
 450      (((p UNLESS q) Pr) /\ ((q UNLESS r) Pr)) ==>
 451      (((p \/* q) UNLESS r) Pr)`,
 452     REPEAT STRIP_TAC THEN
 453     ASSUME_TAC (UNDISCH_ALL (SPECL
 454          [`((p:'a->bool) UNLESS q)Pr`; `((q:'a->bool) UNLESS r)Pr`]
 455           AND_INTRO_THM)) THEN
 456     ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 457          [(`p:'a->bool`); (`q:'a->bool`);
 458           (`q:'a->bool`); (`r:'a->bool`)]
 459           UNLESS_thm5))) THEN
 460     ASSUME_TAC (SPECL
 461          [(`p:'a->bool`); (`q:'a->bool`); (`r:'a->bool`)]
 462           IMPLY_WEAK_lemma3) THEN
 463     ASSUME_TAC (UNDISCH_ALL (SPECL
 464          [(`(((p:'a->bool) \/* q) UNLESS
 465            ((((Not p) /\* r) \/* ((Not q) /\* q)) \/* (q /\* r))) Pr`);
 466           (`!s:'a. ((((Not p) /\* r) \/* ((Not q) /\* q)) \/*
 467                       (q /\* r))s ==> r s`)]
 468           AND_INTRO_THM)) THEN
 469     STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 470          [(`((p:'a->bool) \/* q)`);
 471           (`((((Not (p:'a->bool)) /\* r) \/* ((Not q) /\* q)) \/*
 472                (q /\* r))`);
 473           (`r:'a->bool`)]
 474           UNLESS_thm3))));;
 475
 476 (*
 477   Corollaries
 478 *)
 479 let UNLESS_cor1 = prove_thm
 480   ("UNLESS_cor1",
 481    `!(p:'a->bool) q Pr. (!s. p s ==> q s) ==> ((p UNLESS q) Pr)`,
 482     REPEAT STRIP_TAC THEN
 483     ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
 484     ASSUME_TAC (UNDISCH_ALL (SPECL
 485       [`((p:'a->bool) UNLESS p)Pr`; `!s:'a. p s ==> q s`]
 486        AND_INTRO_THM)) THEN
 487     ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
 488       [(`p:'a->bool`); (`p:'a->bool`); (`q:'a->bool`);
 489        (`Pr:('a->'a)list`)] UNLESS_thm3)]);;
 490
 491 let UNLESS_cor2 = prove_thm
 492   ("UNLESS_cor2",
 493    (`!(p:'a->bool) q Pr. (!s. (Not p)s ==> q s) ==> ((p UNLESS q) Pr)`),
 494     REPEAT STRIP_TAC THEN
 495     ASSUME_TAC (SPEC_ALL UNLESS_thm2) THEN
 496     ASSUME_TAC (UNDISCH_ALL (SPECL
 497       [(`((p:'a->bool) UNLESS (Not p))Pr`);
 498        (`!s:'a. (Not p) s ==> q s`)]
 499        AND_INTRO_THM)) THEN
 500     ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
 501        [(`p:'a->bool`); (`Not (p:'a->bool)`);
 502         (`q:'a->bool`); (`Pr:('a->'a)list`)]
 503         UNLESS_thm3)]);;
 504
 505 let UNLESS_cor3a = TAC_PROOF
 506   (([],
 507    (`!(p:'a->bool) q r Pr.
 508           (p UNLESS (q \/* r)) Pr ==>
 509           ((p /\* (Not q)) UNLESS (q \/* r)) Pr`)),
 510    REPEAT GEN_TAC THEN
 511    ASSUME_TAC (SPECL [(`Not (q:'a->bool)`);
 512                       (`Pr:('a->'a)list`)] UNLESS_thm2) THEN
 513    UNDISCH_TAC (`((Not (q:'a->bool)) UNLESS (Not(Not q)))Pr`) THEN
 514    REWRITE_TAC [NOT_NOT_lemma] THEN
 515    REPEAT STRIP_TAC THEN
 516    ASSUME_TAC (UNDISCH_ALL (SPECL
 517      [(`((p:'a->bool) UNLESS (q \/* r))Pr`);
 518       (`((Not (q:'a->bool)) UNLESS q)Pr`)]
 519       AND_INTRO_THM)) THEN
 520    ASSUME_TAC (UNDISCH_ALL (SPECL
 521      [(`p:'a->bool`); (`((q:'a->bool) \/* r)`);
 522       (`(Not (q:'a->bool))`); (`q:'a->bool`); (`Pr:('a->'a)list`)]
 523       UNLESS_thm6)) THEN
 524    UNDISCH_TAC (`(((p:'a->bool) /\* (Not q)) UNLESS
 525                     ((q \/* r) \/* q))Pr`) THEN
 526    PURE_ONCE_REWRITE_TAC
 527       [SPECL [(`(q:'a->bool) \/* r`);
 528               (`q:'a->bool`)] OR_COMM_lemma] THEN
 529    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL OR_ASSOC_lemma))] THEN
 530    REWRITE_TAC [OR_OR_lemma]);;
 531
 532 let UNLESS_cor3b = TAC_PROOF
 533   (([],
 534    (`!(p:'a->bool) q r Pr.
 535       ((p /\* (Not q)) UNLESS (q \/* r)) Pr ==> (p UNLESS (q \/* r)) Pr`)),
 536    REPEAT STRIP_TAC THEN
 537    ASSUME_TAC (SPECL [(`(p:'a->bool) /\* q`);
 538                       (`Pr:('a->'a)list`)] UNLESS_thm1) THEN
 539    ASSUME_TAC (SPECL [(`p:'a->bool`); (`q:'a->bool`)]
 540                  AND_IMPLY_WEAK_lemma) THEN
 541    ASSUME_TAC (UNDISCH_ALL (SPECL
 542      [(`(((p:'a->bool) /\* q) UNLESS (p /\* q))Pr`);
 543       (`!s:'a. (p /\* q)s ==> q s`)]
 544       AND_INTRO_THM)) THEN
 545    ASSUME_TAC (UNDISCH_ALL (SPECL
 546      [(`(p:'a->bool) /\* q`); (`(p:'a->bool) /\* q`);
 547       (`q:'a->bool`); (`Pr:('a->'a)list`)]
 548       UNLESS_thm3)) THEN
 549    ASSUME_TAC (UNDISCH_ALL (SPECL
 550      [(`(((p:'a->bool) /\* (Not q)) UNLESS (q \/* r))Pr`);
 551       (`(((p:'a->bool) /\* q) UNLESS q)Pr`)]
 552       AND_INTRO_THM)) THEN
 553    ASSUME_TAC (UNDISCH_ALL (SPECL
 554      [(`((p:'a->bool) /\* (Not q))`); (`((q:'a->bool) \/* r)`);
 555       (`((p:'a->bool) /\* q)`); (`q:'a->bool`); (`Pr:('a->'a)list`)]
 556       UNLESS_thm7)) THEN
 557    UNDISCH_TAC
 558    (`((((p:'a->bool) /\* (Not q)) \/* (p /\* q)) UNLESS
 559         ((q \/* r) \/* q))Pr`) THEN
 560    REWRITE_TAC [AND_COMPL_OR_lemma] THEN
 561    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 562    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL (OR_ASSOC_lemma)))] THEN
 563    REWRITE_TAC [OR_OR_lemma] THEN
 564    STRIP_TAC THEN
 565    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 566    ASM_REWRITE_TAC []);;
 567
 568 let UNLESS_cor3 = prove_thm
 569   ("UNLESS_cor3",
 570    (`!(p:'a->bool) q r Pr.
 571          ((p /\* (Not q)) UNLESS (q \/* r)) Pr = (p UNLESS (q \/* r)) Pr`),
 572    REWRITE_TAC [IMP_ANTISYM_RULE
 573                  (SPEC_ALL UNLESS_cor3b) (SPEC_ALL UNLESS_cor3a)]);;
 574
 575 let UNLESS_cor4 = prove_thm
 576   ("UNLESS_cor4",
 577    (`!(p:'a->bool) q r Pr.
 578                ((p \/* q) UNLESS r) Pr ==> (p UNLESS (q \/* r)) Pr`),
 579    REPEAT STRIP_TAC THEN
 580    ASSUME_TAC (SPEC_ALL ((SPEC (`Not (q:'a->bool)`) UNLESS_thm2))) THEN
 581    UNDISCH_TAC (`((Not (q:'a->bool)) UNLESS (Not(Not q)))Pr`) THEN
 582    REWRITE_TAC [NOT_NOT_lemma] THEN
 583    STRIP_TAC THEN
 584    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 585          [(`(((p:'a->bool) \/* q) UNLESS r)Pr`);
 586           (`((Not (q:'a->bool)) UNLESS q)Pr`)]
 587           AND_INTRO_THM))) THEN
 588    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 589          [(`((p:'a->bool) \/* q)`); (`r:'a->bool`);
 590           (`(Not (q:'a->bool))`); (`q:'a->bool`)]
 591           UNLESS_thm6))) THEN
 592    UNDISCH_TAC (`((((p:'a->bool) \/* q) /\* (Not q)) UNLESS
 593                     (r \/* q))Pr`) THEN
 594    REWRITE_TAC [OR_NOT_AND_lemma] THEN
 595    PURE_ONCE_REWRITE_TAC [SPECL [(`r:'a->bool`); (`q:'a->bool`)]
 596        OR_COMM_lemma] THEN
 597    REWRITE_TAC [UNLESS_cor3] THEN
 598    STRIP_TAC THEN
 599    PURE_ONCE_REWRITE_TAC [SPECL [(`r:'a->bool`); (`q:'a->bool`)]
 600        OR_COMM_lemma] THEN
 601    ASM_REWRITE_TAC []);;
 602
 603 let UNLESS_cor5 = prove_thm
 604   ("UNLESS_cor5",
 605    (`!(p:'a->bool) Pr. (p UNLESS True) Pr`),
 606    REPEAT GEN_TAC THEN
 607    ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
 608    ASSUME_TAC (SPEC_ALL UNLESS_thm2) THEN
 609    ASSUME_TAC (UNDISCH_ALL (SPECL
 610          [(`((p:'a->bool) UNLESS p)Pr`);
 611           (`((p:'a->bool) UNLESS (Not p))Pr`)]
 612           AND_INTRO_THM)) THEN
 613    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 614          [(`p:'a->bool`); (`p:'a->bool`);
 615           (`p:'a->bool`); (`(Not (p:'a->bool))`)]
 616           UNLESS_thm6))) THEN
 617    UNDISCH_TAC (`(((p:'a->bool) /\* p) UNLESS (p \/* (Not p)))Pr`) THEN
 618    REWRITE_TAC [AND_AND_lemma;P_OR_NOT_P_lemma]);;
 619
 620 let UNLESS_cor6 = prove_thm
 621   ("UNLESS_cor6",
 622    (`!(p:'a->bool) Pr. (True UNLESS p) Pr`),
 623    REPEAT GEN_TAC THEN
 624    ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
 625    ASSUME_TAC (SPEC_ALL (SPEC (`(Not (p:'a->bool))`) UNLESS_thm2)) THEN
 626    UNDISCH_TAC (`((Not (p:'a->bool)) UNLESS (Not(Not p)))Pr`) THEN
 627    REWRITE_TAC [NOT_NOT_lemma] THEN
 628    DISCH_TAC THEN
 629    ASSUME_TAC (UNDISCH_ALL (SPECL
 630          [(`((Not (p:'a->bool)) UNLESS p)Pr`);
 631           (`((p:'a->bool) UNLESS p)Pr`)]
 632           AND_INTRO_THM)) THEN
 633    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 634          [(`(Not (p:'a->bool))`); (`p:'a->bool`);
 635           (`p:'a->bool`); (`p:'a->bool`)]
 636           UNLESS_thm7))) THEN
 637    UNDISCH_TAC (`(((Not (p:'a->bool)) \/* p) UNLESS (p \/* p))Pr`) THEN
 638    PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 639    REWRITE_TAC [OR_OR_lemma;P_OR_NOT_P_lemma]);;
 640
 641 let UNLESS_cor7 = prove_thm
 642   ("UNLESS_cor7",
 643    (`!(p:'a->bool) Pr. (False UNLESS p) Pr`),
 644    REPEAT GEN_TAC THEN
 645    ASSUME_TAC (SPEC_ALL UNLESS_thm1) THEN
 646    ASSUME_TAC (SPEC_ALL (SPEC (`(Not (p:'a->bool))`) UNLESS_thm2)) THEN
 647    UNDISCH_TAC (`((Not (p:'a->bool)) UNLESS (Not(Not p)))Pr`) THEN
 648    REWRITE_TAC [NOT_NOT_lemma] THEN
 649    DISCH_TAC THEN
 650    ASSUME_TAC (UNDISCH_ALL (SPECL
 651          [(`((Not (p:'a->bool)) UNLESS p)Pr`);
 652           (`((p:'a->bool) UNLESS p)Pr`)]
 653           AND_INTRO_THM)) THEN
 654    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 655          [(`(Not (p:'a->bool))`); (`p:'a->bool`);
 656           (`p:'a->bool`); (`p:'a->bool`)]
 657           UNLESS_thm6))) THEN
 658    UNDISCH_TAC (`(((Not (p:'a->bool)) /\* p) UNLESS (p \/* p))Pr`) THEN
 659    PURE_ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
 660    REWRITE_TAC [OR_OR_lemma;P_AND_NOT_P_lemma]);;
 661
 662 let HeJiFeng_lemma1 = TAC_PROOF
 663   (([],
 664    (`!(p:'a->bool) q p'.
 665      (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
 666          (!s. p s /\ ~q s ==> p' s /\ ~q s)`)),
 667    REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
 668
 669 let HeJiFeng_lemma2 = TAC_PROOF
 670   (([],
 671    (`!(p:'a->bool) q p'.
 672      (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
 673          (!s. p' s /\ ~q s ==> p s /\ ~q s)`)),
 674    REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
 675
 676 let HeJiFeng_lemma = TAC_PROOF
 677   (([],
 678    (`!(p:'a->bool) q p'.
 679      (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s) ==>
 680          (!s. p s /\ ~q s <=> p' s /\ ~q s)`)),
 681    REPEAT STRIP_TAC THEN
 682    REWRITE_TAC [IMP_ANTISYM_RULE
 683      (SPEC_ALL (UNDISCH (UNDISCH (UNDISCH (SPEC_ALL HeJiFeng_lemma1)))))
 684      (SPEC_ALL (UNDISCH (UNDISCH (UNDISCH (SPEC_ALL HeJiFeng_lemma2)))))]);;
 685
 686 let HeJiFeng_lemma_f = MK_ABS (UNDISCH_ALL (SPEC_ALL HeJiFeng_lemma));;
 687
 688 let UNLESS_cor8 = prove_thm
 689   ("UNLESS_cor8",
 690    (`!(p:'a->bool) q p' Pr.
 691        (!s. p s /\ ~q s) ==> (!s. p' s) ==> (!s. p s \/ q s)
 692             ==> (((p  /\* (Not q)) UNLESS q) Pr =
 693                  ((p' /\* (Not q)) UNLESS q) Pr)`),
 694    REPEAT STRIP_TAC THEN
 695    REWRITE_TAC [AND_def;OR_def;NOT_def1] THEN
 696    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 697    REWRITE_TAC [HeJiFeng_lemma_f]);;
 698
 699 (*
 700   Corollary of generalized cancellation
 701 *)
 702 let UNLESS_cor9 = prove_thm
 703   ("UNLESS_cor9",
 704    (`!(p:'a->bool) q p' q' r r' Pr.
 705      ((p \/* p') UNLESS (q \/* r)) Pr /\ ((q \/* q') UNLESS (p \/* r')) Pr ==>
 706             ((p \/* p' \/* q \/* q') UNLESS ((p /\* q) \/* r \/* r')) Pr`),
 707    REPEAT GEN_TAC THEN DISCH_TAC THEN
 708    ASSUME_TAC (UNDISCH_ALL (SPECL
 709          [(`((p:'a->bool) \/* p')`); (`((q:'a->bool) \/* r)`);
 710           (`((q:'a->bool) \/* q')`); (`((p:'a->bool) \/* r')`);
 711           (`Pr:('a->'a)list`)]
 712           UNLESS_thm5)) THEN
 713    ASSUME_TAC (SPECL
 714         [(`p:'a->bool`); (`q:'a->bool`);
 715          (`p':'a->bool`); (`q':'a->bool`);
 716          (`r:'a->bool`); (`r':'a->bool`)] IMPLY_WEAK_lemma4) THEN
 717    ASSUME_TAC (UNDISCH_ALL (SPECL
 718       [(`((((p:'a->bool) \/* p') \/* (q \/* q')) UNLESS
 719         ((((Not(p \/* p')) /\* (p \/* r')) \/*
 720           ((Not(q \/* q')) /\* (q \/* r))) \/*
 721          ((q \/* r) /\* (p \/* r')))) Pr`);
 722        (`!s:'a. ((((Not(p \/* p')) /\* (p \/* r')) \/*
 723               ((Not(q \/* q')) /\* (q \/* r))) \/*
 724               ((q \/* r) /\* (p \/* r'))) s ==>
 725                   ((p /\* q) \/* (r \/* r'))s`)]
 726        AND_INTRO_THM)) THEN
 727    STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL (SPECL
 728         [(`(((p:'a->bool) \/* p') \/* (q \/* q'))`);
 729          (`((((Not((p:'a->bool) \/* p')) /\* (p \/* r')) \/*
 730           ((Not(q \/* q')) /\* (q \/* r))) \/*
 731           ((q \/* r) /\* (p \/* r')))`);
 732          (`(((p:'a->bool) /\* q) \/* (r \/* r'))`)]
 733          UNLESS_thm3))) THEN
 734    UNDISCH_TAC (`((((p:'a->bool) \/* p') \/* (q \/* q')) UNLESS
 735                 ((p /\* q) \/* (r \/* r')))Pr`) THEN
 736    REWRITE_TAC [OR_ASSOC_lemma]);;
 737
 738 let UNLESS_cor10 = prove_thm
 739   ("UNLESS_cor10",
 740    (`!(p:'a->bool) q Pr. (p \/* q) STABLE Pr ==> (p UNLESS q) Pr`),
 741    REPEAT GEN_TAC THEN
 742    REWRITE_TAC [STABLE] THEN
 743    DISCH_TAC THEN
 744    STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
 745      [(`p:'a->bool`); (`q:'a->bool`);
 746       (`False:'a->bool`); (`Pr:('a->'a)list`)]
 747       UNLESS_cor4)) THEN
 748    UNDISCH_TAC (`((p:'a->bool) UNLESS (q \/* False))Pr`) THEN
 749    REWRITE_TAC [OR_False_lemma]);;
 750
 751
 752 let UNLESS_cor11 = prove_thm
 753   ("UNLESS_cor11",
 754    (`!(p:'a->bool) Pr. (!s. (Not p)s) ==> p STABLE Pr`),
 755    GEN_TAC THEN
 756    REWRITE_TAC [STABLE] THEN
 757    LIST_INDUCT_TAC THEN
 758    REWRITE_TAC [UNLESS] THEN
 759    STRIP_TAC THEN
 760    RES_TAC THEN
 761    ASM_REWRITE_TAC [] THEN
 762    GEN_TAC THEN
 763    REWRITE_TAC [UNLESS_STMT; FALSE_def] THEN
 764    STRIP_ASSUME_TAC (REWRITE_RULE [NOT_def1]
 765        (SPEC `s:'a` (ASSUME `!s:'a. Not (p:'a->bool) s`))) THEN
 766    STRIP_TAC THEN
 767    RES_TAC);;
 768
 769 let UNLESS_cor12 = prove_thm
 770   ("UNLESS_cor12",
 771    (`!(p:'a->bool) Pr. (!s. (Not p)s) ==> (Not p) STABLE Pr`),
 772    GEN_TAC THEN
 773    REWRITE_TAC [STABLE] THEN
 774    LIST_INDUCT_TAC THEN
 775    REWRITE_TAC [UNLESS] THEN
 776    STRIP_TAC THEN
 777    RES_TAC THEN
 778    ASM_REWRITE_TAC [UNLESS_STMT]);;
 779
 780 let UNLESS_cor13 = prove_thm
 781   ("UNLESS_cor13",
 782    (`!(p:'a->bool) q Pr.
 783         (p UNLESS q) Pr /\ (q UNLESS p) Pr /\ (!s. Not (p /\* q) s) ==>
 784                 (p \/* q) STABLE Pr`),
 785    REPEAT STRIP_TAC THEN
 786    ASSUME_TAC (UNDISCH_ALL (SPECL
 787          [(`((p:'a->bool) /\* q)`);
 788           (`Pr:('a->'a)list`)] UNLESS_cor11)) THEN
 789    UNDISCH_TAC (`((p:'a->bool) /\* q) STABLE Pr`) THEN
 790    REWRITE_TAC [STABLE] THEN
 791    DISCH_TAC THEN
 792    ASSUME_TAC (UNDISCH_ALL (SPECL
 793       [(`((p:'a->bool) UNLESS q)Pr`); (`((q:'a->bool) UNLESS p)Pr`)]
 794        AND_INTRO_THM)) THEN
 795    ASSUME_TAC (UNDISCH_ALL (SPECL
 796       [(`(p:'a->bool)`); (`(q:'a->bool)`);
 797        (`(q:'a->bool)`); (`(p:'a->bool)`); (`Pr:('a->'a)list`)]
 798        UNLESS_thm5)) THEN
 799    UNDISCH_TAC (`(((p:'a->bool) \/* q) UNLESS
 800                     ((((Not p) /\* p) \/* ((Not q) /\* q)) \/* (q /\* p))
 801                    ) Pr`) THEN
 802    PURE_ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
 803    REWRITE_TAC [P_AND_NOT_P_lemma;OR_False_lemma] THEN
 804    PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 805    REWRITE_TAC [OR_False_lemma] THEN
 806    DISCH_TAC THEN
 807    ASSUME_TAC (UNDISCH_ALL (SPECL
 808         [(`(((q:'a->bool) \/* p) UNLESS (p /\* q))Pr`);
 809          (`(((p:'a->bool) /\* q) UNLESS False)Pr`)]
 810          AND_INTRO_THM)) THEN
 811    ASSUME_TAC (UNDISCH_ALL (SPECL
 812      [(`((q:'a->bool) \/* p)`); (`((p:'a->bool) /\* q)`);
 813       (`False:'a->bool`); (`Pr:('a->'a)list`)]
 814        UNLESS_thm8)) THEN
 815    UNDISCH_TAC
 816      (`((((q:'a->bool) \/* p) \/* (p /\* q)) UNLESS False)Pr`) THEN
 817    REWRITE_TAC [OR_AND_DISTR_lemma] THEN
 818    REWRITE_TAC [OR_ASSOC_lemma;OR_OR_lemma] THEN
 819    PURE_ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 820    REWRITE_TAC [OR_ASSOC_lemma;OR_OR_lemma;AND_AND_lemma]);;
 821
 822 let UNLESS_cor14 = prove_thm
 823   ("UNLESS_cor14",
 824    (`!(p:'a->bool) q Pr. (p UNLESS (Not q)) Pr /\ q STABLE Pr ==>
 825                                (p UNLESS (p /\* (Not q))) Pr`),
 826    REWRITE_TAC [STABLE] THEN
 827    REPEAT GEN_TAC THEN DISCH_TAC THEN
 828    ASSUME_TAC (UNDISCH_ALL (SPECL
 829     [(`p:'a->bool`); (`Not (q:'a->bool)`);
 830      (`q:'a->bool`); (`False:'a->bool`); (`Pr:('a->'a)list`)]
 831       UNLESS_thm4)) THEN
 832    UNDISCH_TAC (`(((p:'a->bool) /\* q) UNLESS
 833                      (((p /\* False) \/* (q /\* (Not q))) \/*
 834                       ((Not q) /\* False)))Pr`) THEN
 835    REWRITE_TAC [AND_False_lemma;P_AND_NOT_P_lemma;OR_False_lemma] THEN
 836    DISCH_TAC THEN
 837    ASSUME_TAC (SPECL
 838      [(`(p:'a->bool) /\* (Not q)`);
 839       (`Pr:('a->'a)list`)] UNLESS_thm1) THEN
 840    ASSUME_TAC (UNDISCH_ALL (SPECL
 841      [(`(((p:'a->bool) /\* q) UNLESS False)Pr`);
 842       (`(((p:'a->bool) /\* (Not q)) UNLESS (p /\* (Not q)))Pr`)]
 843       AND_INTRO_THM)) THEN
 844    ASSUME_TAC (UNDISCH_ALL (SPECL
 845      [(`(p:'a->bool) /\* q`); (`False:'a->bool`);
 846       (`(p:'a->bool) /\* (Not q)`); (`(p:'a->bool) /\* (Not q)`);
 847       (`Pr:('a->'a)list`)]
 848       UNLESS_thm5)) THEN
 849    UNDISCH_TAC (`((((p:'a->bool) /\* q) \/* (p /\* (Not q))) UNLESS
 850                  ((((Not(p /\* q)) /\* (p /\* (Not q))) \/*
 851                    ((Not(p /\* (Not q))) /\* False)) \/*
 852                     (False /\* (p /\* (Not q)))))Pr`) THEN
 853    REWRITE_TAC [AND_False_lemma;OR_False_lemma] THEN
 854    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 855    REWRITE_TAC [AND_COMPL_OR_lemma] THEN
 856    ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
 857    REWRITE_TAC [AND_False_lemma] THEN
 858    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 859    REWRITE_TAC [OR_False_lemma] THEN
 860    REWRITE_TAC [NOT_AND_OR_NOT_lemma] THEN
 861    REWRITE_TAC [AND_OR_DISTR_lemma] THEN
 862    REWRITE_TAC [AND_ASSOC_lemma] THEN
 863    REWRITE_TAC [AND_AND_lemma] THEN
 864    ONCE_REWRITE_TAC [AND_AND_COMM_lemma] THEN
 865    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL AND_ASSOC_lemma))] THEN
 866    REWRITE_TAC [P_AND_NOT_P_lemma] THEN
 867    ONCE_REWRITE_TAC [AND_COMM_OR_lemma] THEN
 868    REWRITE_TAC [AND_False_lemma] THEN
 869    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
 870    REWRITE_TAC [OR_False_lemma] THEN
 871    DISCH_TAC THEN
 872    ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
 873    ASM_REWRITE_TAC []);;
 874
 875 let UNLESS_cor15_lem1 = TAC_PROOF
 876   (([],
 877    (`!p q. p /\ (~p \/ ~q) <=> p /\ ~q`)),
 878    REPEAT GEN_TAC THEN
 879    EQ_TAC THEN
 880    REPEAT STRIP_TAC THEN
 881      (RES_TAC THEN ASM_REWRITE_TAC []));;
 882
 883 let UNLESS_cor15_lem2 = TAC_PROOF
 884   (([],
 885    (`!p q. p \/ (p /\ q) <=> p`)),
 886    REPEAT GEN_TAC THEN
 887    EQ_TAC THEN
 888    REPEAT STRIP_TAC THEN
 889    ASM_REWRITE_TAC []);;
 890
 891 let UNLESS_cor15_lem3 = TAC_PROOF
 892   (([],
 893    (`!P Q. (!(i:num). (P i) /\ (Q i)) <=> ((!i. P i) /\ (!i. Q i))`)),
 894    REPEAT GEN_TAC THEN
 895    EQ_TAC THEN
 896    REPEAT STRIP_TAC THEN
 897    ASM_REWRITE_TAC []);;
 898
 899 (*
 900    MESON_TAC is powerful, but I should change this proof to not use
 901    MESON_TAC as a detailed proof will better show why the UNLESS_STMT
 902    property holds
 903 *)
 904 let UNLESS_STMT_cor15 = prove_thm
 905   ("UNLESS_STMT_cor15",
 906    `!(P:num->('a->bool)) Q st.
 907             (!i s. (P i UNLESS_STMT P i /\* Q i) st s) ==>
 908                (!s. ((!*) P UNLESS_STMT (!*) P /\* (?*) Q) st s)`,
 909    REPEAT GEN_TAC THEN
 910    REWRITE_TAC [FORALL_def; EXISTS_def; UNLESS_STMT; AND_def] THEN
 911    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 912    MESON_TAC []);;
 913
 914 let UNLESS_cor15 = prove_thm
 915   ("UNLESS_cor15",
 916    `!(P:num->('a->bool)) Q Pr.
 917        (!i. ((P i) UNLESS ((P i) /\* (Q i))) Pr) ==>
 918            (((!*) P) UNLESS (((!*) P) /\* ((?*) Q))) Pr`,
 919    GEN_TAC THEN GEN_TAC THEN
 920    LIST_INDUCT_TAC THEN
 921    REWRITE_TAC [UNLESS] THEN
 922    STRIP_TAC THEN
 923    RES_TAC THEN
 924    ASM_REWRITE_TAC [] THEN
 925    STRIP_ASSUME_TAC (REWRITE_RULE [UNLESS_cor15_lem3] (ASSUME
 926     `!i:num. (!s:'a. (P i UNLESS_STMT P i /\* Q i) h s) /\
 927                   (P i UNLESS P i /\* Q i) t`)) THEN
 928    RES_TAC THEN
 929    ASM_REWRITE_TAC [] THEN
 930    IMP_RES_TAC UNLESS_STMT_cor15);;
 931
 932 let UNLESS_cor16 = prove_thm
 933   ("UNLESS_cor16",
 934    `!(P:num->('a->bool)) Q Pr.
 935     (!i. ((P i) UNLESS (Q i))Pr) ==>
 936       (!i. ((/<=\* P i) UNLESS (\<=/* Q i))Pr)`,
 937    REPEAT GEN_TAC THEN
 938    DISCH_TAC THEN
 939    INDUCT_TAC THENL
 940      [
 941       ASM_REWRITE_TAC [AND_LE_N_def;OR_LE_N_def]
 942      ;
 943       REWRITE_TAC [AND_LE_N_def;OR_LE_N_def] THEN
 944       ASSUME_TAC (SPEC (`SUC i`) (ASSUME
 945         (`!i. (((P:num->('a->bool)) i) UNLESS (Q i))Pr`))) THEN
 946       STRIP_ASSUME_TAC (UNDISCH_ALL (hd (IMP_CANON (SPECL
 947         [(`/<=\* (P:num->('a->bool)) i`);
 948          (`\<=/* (Q:num->('a->bool)) i`);
 949          (`(P:num->('a->bool))(SUC i)`); (`(Q:num->('a->bool))(SUC i)`);
 950          (`Pr:('a->'a)list`)]
 951          UNLESS_thm6))))
 952      ]);;
 953
 954 let UNLESS_cor17 = prove_thm
 955   ("UNLESS_cor17",
 956    (`!(P:num->('a->bool)) q Pr.
 957        (!i. ((P i) UNLESS q)Pr) ==> (!i. ((/<=\* P i) UNLESS q)Pr)`),
 958    REPEAT GEN_TAC THEN
 959    DISCH_TAC THEN
 960    INDUCT_TAC THENL
 961      [
 962       ASM_REWRITE_TAC [AND_LE_N_def;OR_LE_N_def]
 963      ;
 964       REWRITE_TAC [AND_LE_N_def;OR_LE_N_def] THEN
 965       ASSUME_TAC (SPEC (`SUC i`) (ASSUME
 966         (`!i. (((P:num->('a->bool)) i) UNLESS q)Pr`))) THEN
 967       ASSUME_TAC (UNDISCH_ALL (hd (IMP_CANON (SPECL
 968         [(`/<=\* (P:num->('a->bool)) i`); (`q:'a->bool`);
 969          (`(P:num->('a->bool))(SUC i)`);
 970          (`q:'a->bool`); (`Pr:('a->'a)list`)]
 971          UNLESS_thm6)))) THEN
 972       UNDISCH_ONE_TAC THEN
 973       REWRITE_TAC [OR_OR_lemma]
 974      ]);;
 975
 976 (*
 977    MESON_TAC is powerful, but I should change this proof to not use
 978    MESON_TAC as a detailed proof will better show why the UNLESS_STMT
 979    property holds
 980 *)
 981 let UNLESS_STMT_cor18 = prove_thm
 982   ("UNLESS_STMT_cor18",
 983    `!(P:num->('a->bool)) Q st.
 984          (!i s. ((P i) UNLESS_STMT q) st s) ==>
 985             (!s. (((?*) P) UNLESS_STMT q) st s)`,
 986    REPEAT GEN_TAC THEN
 987    REWRITE_TAC [FORALL_def; EXISTS_def; UNLESS_STMT; AND_def] THEN
 988    CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 989    MESON_TAC []);;
 990
 991 let UNLESS_cor18 = prove_thm
 992   ("UNLESS_cor18",
 993    (`!(P:num->('a->bool)) q Pr.
 994         (!m. ((P m) UNLESS q) Pr) ==> (((?*) P) UNLESS q) Pr`),
 995    GEN_TAC THEN GEN_TAC THEN
 996    LIST_INDUCT_TAC THEN
 997    REWRITE_TAC [UNLESS] THEN
 998    STRIP_TAC THEN
 999    ASM_REWRITE_TAC [] THEN
1000    STRIP_ASSUME_TAC (REWRITE_RULE [UNLESS_cor15_lem3] (ASSUME
1001     `!m:num. (!s:'a. (P m UNLESS_STMT q) h s) /\ (P m UNLESS q) t`)) THEN
1002    RES_TAC THEN
1003    ASM_REWRITE_TAC [] THEN
1004    IMP_RES_TAC UNLESS_STMT_cor18);;
1005
1006 let UNLESS_cor19 = prove_thm
1007   ("UNLESS_cor19",
1008    (`!Pr. (False:'a->bool) STABLE Pr`),
1009    GEN_TAC THEN
1010    REWRITE_TAC [STABLE] THEN
1011    REWRITE_TAC [UNLESS_thm1]);;
1012
1013 let UNLESS_cor20 = prove_thm
1014   ("UNLESS_cor20",
1015    (`!(p:'a->bool) q Pr.
1016         (p STABLE Pr) /\ (q STABLE Pr) ==> ((p /\* q) STABLE Pr)`),
1017    REPEAT GEN_TAC THEN
1018    REWRITE_TAC [STABLE] THEN
1019    ACCEPT_TAC (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1020      [(`p:'a->bool`); (`False:'a->bool`);
1021       (`q:'a->bool`); (`False:'a->bool`);
1022       (`Pr:('a->'a)list`)] UNLESS_thm4)));;
1023
1024 let UNLESS_cor21 = prove_thm
1025   ("UNLESS_cor21",
1026    (`!(p:'a->bool) q Pr.
1027         (p STABLE Pr) /\ (q STABLE Pr) ==> ((p \/* q) STABLE Pr)`),
1028    REPEAT GEN_TAC THEN
1029    REWRITE_TAC [STABLE] THEN
1030    ACCEPT_TAC (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1031      [(`p:'a->bool`); (`False:'a->bool`);
1032       (`q:'a->bool`); (`False:'a->bool`);
1033       (`Pr:('a->'a)list`)] UNLESS_thm7)));;
1034
1035 let UNLESS_cor22 = prove_thm
1036   ("UNLESS_cor22",
1037    (`!(p:'a->bool) q r Pr.
1038           (p UNLESS q) Pr /\ (r STABLE Pr) ==>
1039           ((p /\* r) UNLESS (q /\* r))Pr`),
1040    REPEAT GEN_TAC THEN
1041    REWRITE_TAC [STABLE] THEN
1042    ACCEPT_TAC (REWRITE_RULE [OR_False_lemma] (ONCE_REWRITE_RULE [OR_COMM_lemma]
1043     (ONCE_REWRITE_RULE [OR_AND_COMM_lemma]
1044       (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
1045         [(`p:'a->bool`); (`q:'a->bool`);
1046          (`r:'a->bool`); (`False:'a->bool`);
1047          (`Pr:('a->'a)list`)] UNLESS_thm4))))));;
1048
1049 let UNLESS_cor23 = prove_thm
1050   ("UNLESS_cor23",
1051    (`!(p:'a->bool) q r Pr.
1052          ((p UNLESS q) Pr) ==> ((p \/* r) UNLESS (q \/* r)) Pr`),
1053    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1054    LIST_INDUCT_TAC THEN
1055    REWRITE_TAC [UNLESS] THEN
1056    STRIP_TAC THEN
1057    RES_TAC THEN
1058    ASM_REWRITE_TAC [] THEN
1059    IMP_RES_TAC UNLESS_STMT_thm6 THEN
1060    ASM_REWRITE_TAC []);;