Unity/mk_comp_unity.ml

   1 (*---------------------------------------------------------------------------*)
   2 (*
   3    File:         mk_comp_unity.ml
   4
   5    Description:  This file proves the unity compositionality theorems and
   6                  corrollaries valid.
   7
   8    Author:       (c) Copyright 1989-2008 by Flemming Andersen
   9    Date:         December 1, 1989
  10    Last Update:  December 30, 2007
  11 *)
  12 (*---------------------------------------------------------------------------*)
  13
  14 (*---------------------------------------------------------------------------*)
  15 (*
  16   Theorems
  17 *)
  18 (*---------------------------------------------------------------------------*)
  19
  20 (*
  21    Prove:
  22    !p q FPr GPr.
  23       (p UNLESS q) (APPEND FPr GPr) ==> (p UNLESS q) FPr /\ (p UNLESS q) GPr
  24 *)
  25 let COMP_UNLESS_thm1_lemma_1 = TAC_PROOF
  26   (([],
  27    (`!(p:'a->bool) q FPr GPr.
  28       (p UNLESS q) (APPEND FPr GPr) ==> (p UNLESS q) FPr /\ (p UNLESS q) GPr`)),
  29    REPEAT GEN_TAC THEN
  30    SPEC_TAC ((`GPr:('a->'a)list`),(`GPr:('a->'a)list`)) THEN
  31    SPEC_TAC ((`FPr:('a->'a)list`),(`FPr:('a->'a)list`)) THEN
  32    LIST_INDUCT_TAC THENL
  33      [
  34       REWRITE_TAC [UNLESS;APPEND]
  35      ;
  36       REWRITE_TAC [APPEND] THEN
  37       REWRITE_TAC [UNLESS] THEN
  38       REPEAT STRIP_TAC THENL
  39         [
  40          ASM_REWRITE_TAC []
  41         ;
  42          RES_TAC
  43         ;
  44          RES_TAC]]);;
  45
  46 (*
  47    Prove:
  48      !p q FPr GPr.
  49      (p UNLESS q) FPr /\ (p UNLESS q) GPr ==> (p UNLESS q) (APPEND FPr GPr)
  50 *)
  51 let COMP_UNLESS_thm1_lemma_2 = TAC_PROOF
  52   (([],
  53    (`!(p:'a->bool) q FPr GPr.
  54      (p UNLESS q) FPr /\ (p UNLESS q) GPr ==> (p UNLESS q) (APPEND FPr GPr)`)),
  55    REPEAT GEN_TAC THEN
  56    SPEC_TAC ((`GPr:('a->'a)list`),(`GPr:('a->'a)list`)) THEN
  57    SPEC_TAC ((`FPr:('a->'a)list`),(`FPr:('a->'a)list`)) THEN
  58    LIST_INDUCT_TAC THENL
  59      [
  60       REWRITE_TAC [UNLESS;APPEND]
  61      ;
  62       REWRITE_TAC [APPEND] THEN
  63       REWRITE_TAC [UNLESS] THEN
  64       REPEAT STRIP_TAC THENL
  65         [
  66          ASM_REWRITE_TAC []
  67         ;
  68          RES_TAC
  69         ]]);;
  70
  71
  72 (*
  73    Prove:
  74      !p q FPr GPr.
  75       (p UNLESS q) (APPEND FPr GPr) = (p UNLESS q) FPr /\ (p UNLESS q) GPr
  76 *)
  77 let COMP_UNLESS_thm1 = prove_thm
  78   ("COMP_UNLESS_thm1",
  79    (`!(p:'a->bool) q FPr GPr.
  80       (p UNLESS q) (APPEND FPr GPr) <=> (p UNLESS q) FPr /\ (p UNLESS q) GPr`),
  81    REPEAT GEN_TAC THEN
  82    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
  83                        (SPEC_ALL COMP_UNLESS_thm1_lemma_1)
  84                        (SPEC_ALL COMP_UNLESS_thm1_lemma_2)));;
  85
  86
  87 (*
  88    Prove:
  89    !p q FPr GPr.
  90     (p ENSURES q) (APPEND FPr GPr) ==> (p ENSURES q) FPr /\ (p UNLESS q) GPr \/
  91                                        (p ENSURES q) GPr /\ (p UNLESS q) FPr
  92 *)
  93 let COMP_ENSURES_thm1_lemma_1 = TAC_PROOF
  94   (([],
  95    (`!(p:'a->bool) q FPr GPr.
  96     (p ENSURES q) (APPEND FPr GPr) ==> (p ENSURES q) FPr /\ (p UNLESS q) GPr \/
  97                                        (p ENSURES q) GPr /\ (p UNLESS q) FPr`)),
  98    REPEAT GEN_TAC THEN
  99    SPEC_TAC ((`GPr:('a->'a)list`),(`GPr:('a->'a)list`)) THEN
 100    SPEC_TAC ((`FPr:('a->'a)list`),(`FPr:('a->'a)list`)) THEN
 101    LIST_INDUCT_TAC THENL
 102      [
 103       REWRITE_TAC [ENSURES;EXIST_TRANSITION;UNLESS;APPEND]
 104      ;
 105       GEN_TAC THEN
 106       REWRITE_TAC [ENSURES;EXIST_TRANSITION;UNLESS;APPEND] THEN
 107       REPEAT STRIP_TAC THEN
 108       ASM_REWRITE_TAC [] THENL
 109         [
 110          DISJ1_TAC THEN
 111          ASM_REWRITE_TAC [] THEN
 112          ASM_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL COMP_UNLESS_thm1))]
 113         ;
 114          ASSUME_TAC (UNDISCH_ALL (SPECL
 115            [(`((p:'a->bool) UNLESS q)(APPEND t GPr)`);
 116             (`((p:'a->bool) EXIST_TRANSITION q)(APPEND t GPr)`)]
 117             AND_INTRO_THM)) THEN
 118          UNDISCH_TAC (`((p:'a->bool) UNLESS  q)(APPEND t GPr) /\
 119                        (p EXIST_TRANSITION q)(APPEND t GPr)`) THEN
 120          REWRITE_TAC [SPECL [(`q:'a->bool`); (`p:'a->bool`);
 121                              (`APPEND (t:('a->'a)list) GPr`)]
 122                              (GEN_ALL (SYM (SPEC_ALL ENSURES)))] THEN
 123          DISCH_TAC THEN
 124          RES_TAC THENL
 125            [
 126             UNDISCH_TAC (`((p:'a->bool) ENSURES q) t`) THEN
 127             REWRITE_TAC [ENSURES] THEN
 128             STRIP_TAC THEN
 129             ASM_REWRITE_TAC []
 130            ;
 131             UNDISCH_TAC (`((p:'a->bool) ENSURES q) GPr`) THEN
 132             REWRITE_TAC [ENSURES] THEN
 133             STRIP_TAC THEN
 134             ASM_REWRITE_TAC []
 135            ]]]);;
 136
 137 (*
 138    Prove:
 139     !p q FPr GPr.
 140     (p ENSURES q) FPr /\ (p UNLESS q) GPr \/
 141     (p ENSURES q) GPr /\ (p UNLESS q) FPr ==> (p ENSURES q) (APPEND FPr GPr)
 142 *)
 143 let COMP_ENSURES_thm1_lemma_2 = TAC_PROOF
 144   (([],
 145     `!(p:'a->bool) q FPr GPr.
 146     ((p ENSURES q) FPr /\ (p UNLESS q) GPr \/
 147      (p ENSURES q) GPr /\ (p UNLESS q) FPr)
 148            ==> (p ENSURES q) (APPEND FPr GPr)`),
 149    GEN_TAC THEN GEN_TAC THEN
 150    LIST_INDUCT_TAC THEN
 151    REWRITE_TAC [ENSURES;EXIST_TRANSITION;UNLESS;APPEND] THEN
 152    REPEAT STRIP_TAC THEN
 153    RES_TAC THEN
 154    ASM_REWRITE_TAC [COMP_UNLESS_thm1;ENSURES;EXIST_TRANSITION;
 155                     UNLESS;APPEND] THEN
 156    REWRITE_TAC [UNDISCH_ALL (ONCE_REWRITE_RULE [EXIST_TRANSITION_thm12]
 157         (SPEC_ALL EXIST_TRANSITION_thm8))] THENL
 158    [
 159      REWRITE_TAC
 160        [ONCE_REWRITE_RULE [EXIST_TRANSITION_thm12] (UNDISCH_ALL (SPECL
 161           [`p:'a->bool`;`q:'a->bool`;`t:('a->'a)list`;`GPr:('a->'a)list`]
 162              EXIST_TRANSITION_thm8))]
 163    ;
 164      REWRITE_TAC
 165        [UNDISCH_ALL
 166           (SPECL [`p:'a->bool`;`q:'a->bool`;`GPr:('a->'a)list`;`t:('a->'a)list`]
 167              EXIST_TRANSITION_thm8)]
 168    ]);;
 169
 170 (*
 171    Prove:
 172     !p q FPr GPr.
 173       (p ENSURES q) (APPEND FPr GPr) = (p ENSURES q) FPr /\ (p UNLESS q) GPr \/
 174                                        (p ENSURES q) GPr /\ (p UNLESS q) FPr
 175 *)
 176 let COMP_ENSURES_thm1 = prove_thm
 177   ("COMP_ENSURES_thm1",
 178    (`!(p:'a->bool) q FPr GPr.
 179       (p ENSURES q) (APPEND FPr GPr) <=>
 180          ((p ENSURES q) FPr /\ (p UNLESS q) GPr \/
 181           (p ENSURES q) GPr /\ (p UNLESS q) FPr)`),
 182    REPEAT GEN_TAC THEN
 183    STRIP_ASSUME_TAC (IMP_ANTISYM_RULE
 184                        (SPEC_ALL COMP_ENSURES_thm1_lemma_1)
 185                        (SPEC_ALL COMP_ENSURES_thm1_lemma_2)));;
 186
 187 (*
 188    Prove:
 189     |- !p q FPr GPr.
 190          (p ENSURES q)FPr /\ (p UNLESS q)GPr ==> (p ENSURES q)(APPEND FPr GPr)
 191 *)
 192 let COMP_ENSURES_cor0 = prove_thm
 193   ("COMP_ENSURES_cor0",
 194    (`!(p:'a->bool) q FPr GPr.
 195       (p ENSURES q) FPr /\ (p UNLESS q) GPr
 196          ==> (p ENSURES q) (APPEND FPr GPr)`),
 197    REPEAT STRIP_TAC THEN
 198    ACCEPT_TAC (REWRITE_RULE
 199     [ASSUME (`((p:'a->bool) ENSURES q)FPr`);ASSUME (`((p:'a->bool) UNLESS q)GPr`)]
 200     (SPEC_ALL COMP_ENSURES_thm1)));;
 201
 202
 203 (*
 204    Prove:
 205     |- !p q FPr GPr.
 206          (p ENSURES q)GPr /\ (p UNLESS q)FPr ==> (p ENSURES q)(APPEND FPr GPr)
 207 *)
 208 let COMP_ENSURES_cor1 = prove_thm
 209   ("COMP_ENSURES_cor1",
 210    (`!(p:'a->bool) q FPr GPr.
 211       (p ENSURES q) GPr /\ (p UNLESS q) FPr
 212          ==> (p ENSURES q) (APPEND FPr GPr)`),
 213    REPEAT STRIP_TAC THEN
 214    ACCEPT_TAC (REWRITE_RULE
 215     [ASSUME (`((p:'a->bool) ENSURES q)GPr`);ASSUME (`((p:'a->bool) UNLESS q)FPr`)]
 216     (SPEC_ALL COMP_ENSURES_thm1)));;
 217
 218
 219 (*
 220    Prove:
 221      !p q FPr GPr.
 222       (p INVARIANT q) (APPEND FPr GPr) =
 223           (p INVARIANT q) FPr /\ (p INVARIANT q) GPr
 224 *)
 225 let COMP_UNITY_cor0 = prove_thm
 226   ("COMP_UNITY_cor0",
 227    (`!(p0:'a->bool) p FPr GPr.
 228        (p INVARIANT (p0, APPEND FPr GPr)) =
 229           (p INVARIANT (p0,FPr) /\ p INVARIANT (p0,GPr))`),
 230    REWRITE_TAC [INVARIANT;STABLE;COMP_UNLESS_thm1] THEN
 231    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN
 232    RES_TAC THEN ASM_REWRITE_TAC []);;
 233
 234
 235 (*
 236    Prove:
 237         !p FPr GPr.
 238            p STABLE (APPEND FPr GPr) = p STABLE FPr /\ p STABLE GPr
 239 *)
 240 let COMP_UNITY_cor1 = prove_thm
 241   ("COMP_UNITY_cor1",
 242    (`!(p:'a->bool) FPr GPr.
 243            (p STABLE (APPEND FPr GPr)) = (p STABLE FPr /\ p STABLE GPr)`),
 244    REWRITE_TAC [STABLE;COMP_UNLESS_thm1]);;
 245
 246
 247 (*
 248    Prove:
 249         !p q FPr GPr.
 250          (p UNLESS q) FPr /\ p STABLE GPr ==>(p UNLESS q) (APPEND FPr GPr)
 251 *)
 252 let COMP_UNITY_cor2 = prove_thm
 253   ("COMP_UNITY_cor2",
 254    (`!(p:'a->bool) q FPr GPr.
 255          (p UNLESS q) FPr /\ p STABLE GPr ==>(p UNLESS q) (APPEND FPr GPr)`),
 256    REWRITE_TAC [STABLE;COMP_UNLESS_thm1] THEN
 257    REPEAT STRIP_TAC THENL
 258      [
 259       ASM_REWRITE_TAC []
 260      ;
 261       UNDISCH_TAC (`((p:'a->bool) UNLESS False)GPr`) THEN
 262       SPEC_TAC ((`GPr:('a->'a)list`),(`GPr:('a->'a)list`)) THEN
 263       LIST_INDUCT_TAC THENL
 264         [
 265          REWRITE_TAC [UNLESS]
 266         ;
 267          REWRITE_TAC [UNLESS;UNLESS_STMT] THEN
 268          CONV_TAC (DEPTH_CONV BETA_CONV) THEN
 269          REPEAT STRIP_TAC THENL
 270            [
 271             RES_TAC THEN
 272             UNDISCH_TAC
 273                (`~(False:'a->bool) s ==> (p:'a->bool)(h s) \/ False(h s)`) THEN
 274             REWRITE_TAC [FALSE_def;NOT_CLAUSES;OR_INTRO_THM1]
 275            ;
 276             RES_TAC]]]);;
 277
 278
 279 (*
 280    Prove:
 281      !p0 p FPr GPr.
 282        p INVARIANT (p0; FPr) /\ p STABLE GPr
 283             ==> p INVARIANT (p0; (APPEND FPr GPr))
 284 *)
 285 let COMP_UNITY_cor3 = prove_thm
 286   ("COMP_UNITY_cor3",
 287    (`!(p0:'a->bool) p FPr GPr.
 288        p INVARIANT (p0, FPr) /\ p STABLE GPr ==>
 289                     p INVARIANT (p0, (APPEND FPr GPr))`),
 290    REWRITE_TAC [INVARIANT;STABLE;COMP_UNLESS_thm1] THEN
 291    REPEAT STRIP_TAC THENL
 292      [
 293       RES_TAC
 294      ;
 295       ASM_REWRITE_TAC []
 296      ;
 297       ASM_REWRITE_TAC []]);;
 298
 299
 300 (*
 301    Prove:
 302        !p q FPr GPr.
 303         (p ENSURES q) FPr /\ p STABLE GPr ==> (p ENSURES q) (APPEND FPr GPr)
 304 *)
 305 let COMP_UNITY_cor4 = prove_thm
 306   ("COMP_UNITY_cor4",
 307    (`!(p:'a->bool) q FPr GPr.
 308         (p ENSURES q) FPr /\ p STABLE GPr ==> (p ENSURES q) (APPEND FPr GPr)`),
 309    REPEAT STRIP_TAC THEN
 310    ASSUME_TAC (UNDISCH_ALL (SPECL
 311         [(`p:'a->bool`);(`q:'a->bool`);(`FPr:('a->'a)list`)] ENSURES_cor2)) THEN
 312    ASSUME_TAC (UNDISCH_ALL (SPECL
 313         [(`((p:'a->bool) UNLESS q)FPr`);(`(p:'a->bool) STABLE GPr`)]
 314          AND_INTRO_THM)) THEN
 315    ASSUME_TAC (UNDISCH_ALL (SPECL
 316         [(`p:'a->bool`);(`q:'a->bool`);(`FPr:('a->'a)list`);(`GPr:('a->'a)list`)]
 317          COMP_UNITY_cor2)) THEN
 318    REWRITE_TAC [ENSURES] THEN
 319    ASM_REWRITE_TAC [] THEN
 320    UNDISCH_TAC (`((p:'a->bool) ENSURES q)FPr`) THEN
 321    REWRITE_TAC [ENSURES] THEN
 322    STRIP_TAC THEN
 323    UNDISCH_TAC (`((p:'a->bool) EXIST_TRANSITION q)FPr`) THEN
 324    SPEC_TAC ((`FPr:('a->'a)list`),(`FPr:('a->'a)list`)) THEN
 325    LIST_INDUCT_TAC THENL
 326      [
 327       REWRITE_TAC [EXIST_TRANSITION]
 328      ;
 329       REWRITE_TAC [APPEND;EXIST_TRANSITION] THEN
 330       REPEAT STRIP_TAC THENL
 331         [
 332          ASM_REWRITE_TAC []
 333         ;
 334          RES_TAC THEN
 335          ASM_REWRITE_TAC []]]);;
 336
 337 (*
 338    Prove:
 339    !p q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q) GPr
 340 *)
 341 let COMP_UNITY_cor5 = prove_thm
 342   ("COMP_UNITY_cor5",
 343    (`!(p:'a->bool) q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q) GPr`),
 344    REWRITE_TAC [COMP_UNLESS_thm1] THEN
 345    REPEAT STRIP_TAC);;
 346
 347 (*
 348    Prove:
 349     !p q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q) FPr
 350 *)
 351 let COMP_UNITY_cor6 = prove_thm
 352   ("COMP_UNITY_cor6",
 353    (`!(p:'a->bool) q FPr GPr. (p UNLESS q)(APPEND FPr GPr) ==> (p UNLESS q) FPr`),
 354    REWRITE_TAC [COMP_UNLESS_thm1] THEN
 355    REPEAT STRIP_TAC);;
 356
 357 (*
 358    Prove:
 359     !p q st FPr. (p UNLESS q)(CONS st FPr) ==> (p UNLESS q) FPr
 360 *)
 361 let COMP_UNITY_cor7 = prove_thm
 362   ("COMP_UNITY_cor7",
 363    (`!(p:'a->bool) q st FPr. (p UNLESS q)(CONS st FPr) ==> (p UNLESS q) FPr`),
 364    REWRITE_TAC [UNLESS] THEN
 365    REPEAT STRIP_TAC);;
 366
 367 (*
 368    Prove:
 369         !p FPr GPr.
 370            (p ENSURES (NotX  p)) FPr ==> (p ENSURES (NotX  p)) (APPEND FPr GPr)
 371 *)
 372 let COMP_UNITY_cor8 = prove_thm
 373   ("COMP_UNITY_cor8",
 374    (`!(p:'a->bool) FPr GPr.
 375         (p ENSURES (Not p)) FPr ==> (p ENSURES (Not p)) (APPEND FPr GPr)`),
 376    GEN_TAC THEN
 377    LIST_INDUCT_TAC THEN
 378    REWRITE_TAC [APPEND;ENSURES;UNLESS;EXIST_TRANSITION] THEN
 379    REPEAT STRIP_TAC THEN
 380    RES_TAC THEN
 381    ASM_REWRITE_TAC [UNLESS_thm2] THEN
 382    REWRITE_TAC [UNDISCH_ALL (ONCE_REWRITE_RULE [EXIST_TRANSITION_thm12] (SPECL
 383      [`p:'a->bool`;`Not (p:'a->bool)`;`t:('a->'a)list`;`GPr:('a->'a)list`]
 384        EXIST_TRANSITION_thm8))]);;
 385
 386 (*
 387    Prove:
 388         !p q FPr GPr.
 389            p STABLE FPr /\ (p UNLESS q) GPr ==> (p UNLESS q) (APPEND FPr GPr)
 390 *)
 391 let COMP_UNITY_cor9 = prove_thm
 392   ("COMP_UNITY_cor9",
 393    (`!(p:'a->bool) q FPr GPr.
 394          p STABLE FPr /\ (p UNLESS q) GPr ==> (p UNLESS q) (APPEND FPr GPr)`),
 395    REWRITE_TAC [STABLE;COMP_UNLESS_thm1] THEN
 396    REPEAT STRIP_TAC THENL
 397      [
 398       UNDISCH_TAC (`((p:'a->bool) UNLESS False)FPr`) THEN
 399       SPEC_TAC ((`FPr:('a->'a)list`),(`FPr:('a->'a)list`)) THEN
 400       LIST_INDUCT_TAC THENL
 401         [
 402          REWRITE_TAC [UNLESS]
 403         ;
 404          REWRITE_TAC [UNLESS;UNLESS_STMT] THEN
 405          BETA_TAC THEN
 406          REPEAT STRIP_TAC THENL
 407            [
 408             RES_TAC THEN
 409             UNDISCH_TAC
 410                (`~(False:'a->bool) s ==> (p:'a->bool)(h s) \/ False(h s)`) THEN
 411             REWRITE_TAC [FALSE_def;NOT_CLAUSES;OR_INTRO_THM1]
 412            ;
 413             RES_TAC
 414            ]
 415         ]
 416      ;
 417       ASM_REWRITE_TAC []
 418      ]);;
 419
 420
 421 (*
 422    Prove:
 423     !p q FPr GPr.
 424          (p UNLESS q) (APPEND FPr GPr) = (p UNLESS q) (APPEND GPr FPr)
 425 *)
 426 let COMP_UNITY_cor10 = prove_thm
 427   ("COMP_UNITY_cor10",
 428    (`!(p:'a->bool) q FPr GPr.
 429          (p UNLESS q) (APPEND FPr GPr) = (p UNLESS q) (APPEND GPr FPr)`),
 430    REPEAT GEN_TAC THEN
 431    REWRITE_TAC [COMP_UNLESS_thm1] THEN
 432    EQ_TAC THEN
 433    REPEAT STRIP_TAC THEN
 434    ASM_REWRITE_TAC []);;
 435
 436 (*
 437    Prove:
 438     !p q FPr GPr.
 439          (p ENSURES q) (APPEND FPr GPr) = (p ENSURES q) (APPEND GPr FPr)
 440 *)
 441 let COMP_UNITY_cor11 = prove_thm
 442   ("COMP_UNITY_cor11",
 443    (`!(p:'a->bool) q FPr GPr.
 444          (p ENSURES q) (APPEND FPr GPr) = (p ENSURES q) (APPEND GPr FPr)`),
 445    REPEAT GEN_TAC THEN
 446    REWRITE_TAC [COMP_ENSURES_thm1] THEN
 447    EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
 448
 449 (*
 450    Prove:
 451     !p q FPr GPr.
 452       (p LEADSTO q) (APPEND FPr GPr) = (p LEADSTO q) (APPEND GPr FPr)
 453 *)
 454
 455 (*
 456   |- (!p' q'.
 457      ((p' ENSURES q')(APPEND Pr1 Pr2) ==> (p' LEADSTO q')(APPEND Pr2 Pr1)) /\
 458      (!r.
 459        (p' LEADSTO r)(APPEND Pr1 Pr2) /\ (p' LEADSTO r)(APPEND Pr2 Pr1) /\
 460        (r LEADSTO q')(APPEND Pr1 Pr2) /\ (r LEADSTO q')(APPEND Pr2 Pr1) ==>
 461        (p' LEADSTO q')(APPEND Pr1 Pr2) ==> (p' LEADSTO q')(APPEND Pr2 Pr1)) /\
 462      (!P.
 463        (!i. ((P i) LEADSTO q')(APPEND Pr1 Pr2)) /\
 464        (!i. ((P i) LEADSTO q')(APPEND Pr2 Pr1)) ==>
 465           (($ExistsX  P) LEADSTO q')(APPEND Pr1 Pr2) ==>
 466           (($ExistsX  P) LEADSTO q')(APPEND Pr2 Pr1)))
 467      ==>
 468        (p LEADSTO q)(APPEND Pr1 Pr2) ==> (p LEADSTO q)(APPEND Pr2 Pr1)
 469 *)
 470 let COMP_UNITY_cor12_lemma00 = (BETA_RULE (SPECL
 471   [(`\(p:'a->bool) q. (p LEADSTO q)(APPEND Pr2 Pr1)`);
 472    (`p:'a->bool`);(`q:'a->bool`);(`APPEND (Pr1:('a->'a)list) Pr2`)] LEADSTO_thm37));;
 473
 474 let COMP_UNITY_cor12_lemma01 = TAC_PROOF
 475   (([],
 476    (`!(p':'a->bool) q' Pr1 Pr2.
 477       (p' ENSURES q')(APPEND Pr1 Pr2) ==> (p' LEADSTO q')(APPEND Pr2 Pr1)`)),
 478    REPEAT STRIP_TAC THEN
 479    ASSUME_TAC (ONCE_REWRITE_RULE [COMP_UNITY_cor11] (ASSUME
 480     (`((p':'a->bool) ENSURES q')(APPEND Pr1 Pr2)`))) THEN
 481    IMP_RES_TAC LEADSTO_thm0);;
 482
 483 let COMP_UNITY_cor12_lemma02 = TAC_PROOF
 484   (([],
 485    (`!(p':'a->bool) q' Pr1 Pr2.
 486      (!r.
 487        (p' LEADSTO r)(APPEND Pr1 Pr2) /\ (p' LEADSTO r)(APPEND Pr2 Pr1) /\
 488        (r LEADSTO q')(APPEND Pr1 Pr2) /\ (r LEADSTO q')(APPEND Pr2 Pr1)
 489           ==> (p' LEADSTO q')(APPEND Pr2 Pr1))`)),
 490    REPEAT STRIP_TAC THEN
 491    IMP_RES_TAC LEADSTO_thm1);;
 492
 493 let COMP_UNITY_cor12_lemma03 = TAC_PROOF
 494   (([],
 495    (`!(p':'a->bool) q' Pr1 Pr2.
 496      (!P:('a->bool)->bool.
 497        (!p''. p'' In P ==> (p'' LEADSTO q')(APPEND Pr1 Pr2)) /\
 498        (!p''. p'' In P ==> (p'' LEADSTO q')(APPEND Pr2 Pr1))
 499             ==> ((LUB P) LEADSTO q')(APPEND Pr2 Pr1))`)),
 500    REPEAT STRIP_TAC THEN
 501    IMP_RES_TAC LEADSTO_thm3a);;
 502
 503 (*
 504   |- !p q Pr1 Pr2.
 505        (p LEADSTO q)(APPEND Pr1 Pr2) ==> (p LEADSTO q)(APPEND Pr2 Pr1)
 506 *)
 507 let COMP_UNITY_cor12_lemma04 = (GEN_ALL (REWRITE_RULE
 508    [COMP_UNITY_cor12_lemma01;COMP_UNITY_cor12_lemma02;COMP_UNITY_cor12_lemma03]
 509     (SPEC_ALL COMP_UNITY_cor12_lemma00)));;
 510
 511 (*
 512  |- !p q Pr1 Pr2. (p LEADSTO q)(APPEND Pr1 Pr2) = (p LEADSTO q)(APPEND Pr2 Pr1)
 513 *)
 514 let COMP_UNITY_cor12 = prove_thm
 515   ("COMP_UNITY_cor12",
 516    (`!(p:'a->bool) q Pr1 Pr2.
 517        (p LEADSTO q)(APPEND Pr1 Pr2) = (p LEADSTO q)(APPEND Pr2 Pr1)`),
 518    REPEAT GEN_TAC THEN
 519    EQ_TAC THEN REWRITE_TAC [COMP_UNITY_cor12_lemma04]);;
 520
 521 (*
 522   |- !p FPr GPr. p STABLE (APPEND FPr GPr) = p STABLE (APPEND GPr FPr)
 523 *)
 524 let COMP_UNITY_cor13 = prove_thm
 525   ("COMP_UNITY_cor13",
 526    (`!(p:'a->bool) FPr GPr.
 527       (p STABLE (APPEND FPr GPr)) = (p STABLE (APPEND GPr FPr))`),
 528    REPEAT GEN_TAC THEN
 529    REWRITE_TAC [STABLE] THEN
 530    EQ_TAC THEN
 531    STRIP_TAC THEN
 532    ONCE_REWRITE_TAC [COMP_UNITY_cor10] THEN
 533    ASM_REWRITE_TAC []);;
 534
 535
 536 (*
 537   |- !p0 p FPr GPr.
 538       p INVARIANT (p0, APPEND FPr GPr) = p INVARIANT (p0, APPEND GPr FPr)
 539 *)
 540 let COMP_UNITY_cor14 = prove_thm
 541   ("COMP_UNITY_cor14",
 542    (`!(p0:'a->bool) p FPr GPr.
 543       (p INVARIANT (p0, (APPEND FPr GPr)))
 544     =
 545       (p INVARIANT (p0, (APPEND GPr FPr)))`),
 546    REPEAT GEN_TAC THEN
 547    REWRITE_TAC [INVARIANT] THEN
 548    EQ_TAC THEN
 549    STRIP_TAC THEN
 550    ONCE_REWRITE_TAC [COMP_UNITY_cor13] THEN
 551    ASM_REWRITE_TAC []);;