Unity/mk_ensures.ml

   1 (*---------------------------------------------------------------------------*)
   2 (*
   3    File:         mk_ensures.sml
   4
   5    Description:  This file defines ENSURES and the theorems and corrollaries
   6                  described in [CM88].
   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 (* The definition of ENSURES is based on the definition:
  16
  17       p ensures q in Pr = <p unless q in Pr /\ (?s in Pr: {p /\ ~q} s {q})>
  18
  19   where p and q are state dependent first order logic predicates and s
  20   in the program Pr are conditionally enabled statements transforming
  21   a state into a new state. ENSURES then requires safety and the
  22   existance of at least one state transition statement s which makes q
  23   valid.
  24 *)
  25
  26 let EXIST_TRANSITION_term =
  27    `(!p q. EXIST_TRANSITION (p:'a->bool) q []         <=> F) /\
  28     (!p q. EXIST_TRANSITION p q (CONS (st:'a->'a) Pr) <=>
  29           ((!s. (p s /\ ~q s) ==> q (st s)) \/ (EXIST_TRANSITION p q Pr)))`;;
  30 let EXIST_TRANSITION = new_recursive_definition
  31     list_RECURSION EXIST_TRANSITION_term;;
  32 parse_as_infix ( "EXIST_TRANSITION", (TL_FIX, "right") );;
  33
  34 let ENSURES = new_infix_definition
  35   ("ENSURES", "<=>",
  36    `!(p:'a->bool) q (Pr:('a->'a)list).
  37        ENSURES p q Pr = (((p UNLESS q) Pr) /\ ((p EXIST_TRANSITION q) Pr))`,
  38    TL_FIX);;
  39
  40 let ENSURES_STMT = new_infix_definition
  41   ("ENSURES_STMT", "<=>",
  42    `!(p:'a->bool) q (st:'a->'a).
  43         ENSURES_STMT p q st = (\s. p s /\ ~(q s) ==> q (st s))`,
  44    TL_FIX);;
  45
  46
  47 (*-------------------------------------------------------------------------*)
  48 (*
  49   Lemmas
  50 *)
  51 (*-------------------------------------------------------------------------*)
  52
  53 let ENSURES_lemma0 = TAC_PROOF
  54   (([],
  55    (`!(p:'a->bool) q r st.
  56           ((!s. p s /\ ~q s ==> q (st s)) /\ (!s. q s ==> r s)) ==>
  57            (!s. p s /\ ~r s ==> r (st s))`)),
  58     REPEAT STRIP_TAC THEN
  59     ASSUME_TAC (CONTRAPOS (SPEC_ALL (ASSUME (`!s:'a. q s ==> r s`)))) THEN
  60     ASSUME_TAC (SPEC (`(st:'a->'a) s`) (ASSUME (`!s:'a. q s ==> r s`))) THEN
  61     RES_TAC THEN
  62     RES_TAC);;
  63
  64 set_goal([],
  65    (`!(p:'a->bool) p' q q' h.
  66      (!s. (p  UNLESS_STMT q)  h s)     ==>
  67      (!s. (p' UNLESS_STMT q') h s)     ==>
  68      (!s. p' s /\ ~q' s ==> q' (h s))  ==>
  69      (!s. (p /\* p') s /\ ~((p /\* q' \/* p' /\* q) \/* q /\* q') s) ==>
  70      (((p /\* q' \/* p' /\* q) \/* q /\* q') (h s))`)
  71 );;
  72
  73 let ENSURES_lemma1 = TAC_PROOF
  74   (([],
  75     `!(p:'a->bool) p' q q' h.
  76       (!s. (p  UNLESS_STMT q)  h s)     ==>
  77       (!s. (p' UNLESS_STMT q') h s)     ==>
  78       (!s. p' s /\ ~q' s ==> q' (h s))  ==>
  79       (!s. (p /\* p') s /\ ~((p /\* q' \/* p' /\* q) \/* q /\* q') s
  80                ==> ((p /\* q' \/* p' /\* q) \/* q /\* q') (h s))`),
  81     REWRITE_TAC [UNLESS_STMT; AND_def; OR_def] THEN
  82     CONV_TAC (DEPTH_CONV BETA_CONV) THEN
  83     MESON_TAC []);;
  84
  85 let ENSURES_lemma2 = TAC_PROOF
  86   (([],
  87    (`!(p:'a->bool) q r st.
  88        (!s. p s /\ ~q s ==> q (st s)) ==>
  89          (!s. (p s \/ r s) /\ ~(q s \/ r s) ==> q (st s) \/ r (st s))`)),
  90      REWRITE_TAC [(GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC)));
  91                   (SYM (SPEC_ALL DISJ_ASSOC));NOT_CLAUSES;DE_MORGAN_THM] THEN
  92      REPEAT STRIP_TAC THEN RES_TAC THEN
  93      ASM_REWRITE_TAC []);;
  94
  95 let ENSURES_lemma3 = TAC_PROOF
  96   (([],
  97    (`!(p:'a->bool) q r Pr. (p ENSURES (q \/* r)) Pr ==>
  98               (((p /\* (Not q)) \/* (p /\* q)) ENSURES (q \/* r)) Pr`)),
  99    REWRITE_TAC [AND_COMPL_OR_lemma]);;
 100
 101 let ENSURES_lemma4 = TAC_PROOF
 102   (([],
 103     `!(p:'a->bool) q r (st:'a->'a).
 104          (!s. p s /\ ~q s ==> q (st s)) ==>
 105             (!s. (p \/* r) s /\ ~(q \/* r) s ==> (q \/* r) (st s))`),
 106     REPEAT GEN_TAC THEN
 107     REWRITE_TAC [OR_def] THEN
 108     MESON_TAC []);;
 109
 110 (*---------------------------------------------------------------------------*)
 111 (*
 112   Theorems about EXIST_TRANSITION
 113 *)
 114 (*---------------------------------------------------------------------------*)
 115
 116 (*
 117   EXIST_TRANSITION Consequence Weakening Theorem:
 118
 119                p EXIST_TRANSITION q in Pr; q ==> r
 120               -------------------------------------
 121                    p EXIST_TRANSITION r in Pr
 122 *)
 123
 124 let EXIST_TRANSITION_thm1 = prove_thm
 125  ("EXIST_TRANSITION_thm1",
 126   (`!(p:'a->bool) q r Pr.
 127      ((p EXIST_TRANSITION q) Pr /\ (!s. (q s) ==> (r s))) ==>
 128        ((p EXIST_TRANSITION r) Pr)`),
 129    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 130    LIST_INDUCT_TAC THEN
 131    REWRITE_TAC [EXIST_TRANSITION] THEN
 132    STRIP_TAC THEN
 133    RES_TAC THEN
 134    ASM_REWRITE_TAC [] THEN
 135    REWRITE_TAC [REWRITE_RULE
 136     [ASSUME `!s:'a. p s /\ ~q s ==> q (h s)`; ASSUME `!s:'a. q s ==> r s`]
 137      (SPECL [`p:'a->bool`;`q:'a->bool`;`r:'a->bool`;`h:'a->'a`] ENSURES_lemma0)]);;
 138
 139 (*
 140   Impossibility EXIST_TRANSITION Theorem:
 141
 142                p EXIST_TRANSITION false in Pr
 143               --------------------------------
 144                           ~p
 145 *)
 146 let EXIST_TRANSITION_thm2 = prove_thm
 147   ("EXIST_TRANSITION_thm2",
 148    (`!(p:'a->bool) Pr.
 149      ((p EXIST_TRANSITION False) Pr) ==> !s. (Not p) s`),
 150    GEN_TAC THEN
 151    LIST_INDUCT_TAC THEN
 152    REWRITE_TAC [EXIST_TRANSITION; NOT_def1] THEN
 153    STRIP_TAC THEN
 154    RES_TAC THEN
 155    ASM_REWRITE_TAC [] THENL
 156    [
 157      UNDISCH_TAC (`!s:'a. ((p:'a->bool) s) /\ ~(False s)
 158                           ==> (False ((h:'a->'a) s))`) THEN
 159      REWRITE_TAC [FALSE_def] THEN
 160      CONV_TAC (DEPTH_CONV BETA_CONV)
 161     ;
 162      UNDISCH_TAC (`!s:'a. (Not (p:'a->bool)) s`) THEN
 163      REWRITE_TAC [NOT_def1] THEN
 164      CONV_TAC (DEPTH_CONV BETA_CONV)
 165    ]);;
 166
 167 (*
 168   Always EXIST_TRANSITION Theorem:
 169
 170                false EXIST_TRANSITION p in Pr
 171 *)
 172 let EXIST_TRANSITION_thm3 = prove_thm
 173   ("EXIST_TRANSITION_thm3",
 174    (`!(p:'a->bool) st Pr. (False EXIST_TRANSITION p) (CONS st Pr)`),
 175    REPEAT GEN_TAC THEN
 176    REWRITE_TAC [EXIST_TRANSITION; FALSE_def]);;
 177
 178 let EXIST_TRANSITION_thm4 = prove_thm
 179   ("EXIST_TRANSITION_thm4",
 180    (`!(p:'a->bool) q r Pr.
 181          (p EXIST_TRANSITION q) Pr ==>
 182             ((p \/* r) EXIST_TRANSITION (q \/* r)) Pr`),
 183    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 184    LIST_INDUCT_TAC THEN
 185    REWRITE_TAC [EXIST_TRANSITION] THEN
 186    STRIP_TAC THEN
 187    RES_TAC THEN
 188    ASM_REWRITE_TAC [] THEN
 189    REWRITE_TAC [REWRITE_RULE
 190       [ASSUME `!s:'a. (p:'a->bool) s /\ ~q s ==> q (h s)`]
 191         (SPECL [`p:'a->bool`;`q:'a->bool`;`r:'a->bool`;`h:'a->'a`]
 192             ENSURES_lemma4)]);;
 193
 194 let APPEND_lemma01 = TAC_PROOF
 195   (([],
 196    `!(l:('a)list). (APPEND l []) = l`),
 197    LIST_INDUCT_TAC THEN
 198    ASM_REWRITE_TAC [APPEND]);;
 199
 200 let EXIST_TRANSITION_thm5 = prove_thm
 201   ("EXIST_TRANSITION_thm5",
 202    (`!(p:'a->bool) q st Pr.
 203        (!s. p s /\ ~q s ==> q (st s))
 204             ==> (p EXIST_TRANSITION q) (CONS st Pr)`),
 205    REPEAT GEN_TAC THEN
 206    REWRITE_TAC [EXIST_TRANSITION] THEN
 207    STRIP_TAC THEN
 208    ASM_REWRITE_TAC []);;
 209
 210 let APPEND_lemma02 = TAC_PROOF
 211   (([],
 212    `!st (l:('a)list).  (APPEND [st] l) = (CONS st l)`),
 213    GEN_TAC THEN
 214    LIST_INDUCT_TAC THEN
 215    REWRITE_TAC [APPEND]);;
 216
 217 let APPEND_lemma03 = TAC_PROOF
 218   (([],
 219    `!st (l1:('a)list) l2.
 220        (APPEND (APPEND l1 [st]) l2) = (APPEND l1 (CONS st l2))`),
 221    GEN_TAC THEN
 222    LIST_INDUCT_TAC THEN
 223    LIST_INDUCT_TAC THEN
 224    REWRITE_TAC [APPEND] THEN
 225    REPEAT STRIP_TAC THEN
 226    RES_TAC THEN
 227    ASM_REWRITE_TAC [APPEND]);;
 228
 229 let APPEND_lemma04 = TAC_PROOF
 230   (([],
 231    `!st (l1:('a)list) l2.
 232        (APPEND (CONS st l1) l2) = (CONS st (APPEND l1 l2))`),
 233    GEN_TAC THEN
 234    LIST_INDUCT_TAC THEN
 235    LIST_INDUCT_TAC THEN
 236    REWRITE_TAC [APPEND] THEN
 237    REPEAT STRIP_TAC THEN
 238    RES_TAC THEN
 239    ASM_REWRITE_TAC [APPEND]);;
 240
 241 let EXIST_TRANSITION_thm6 = prove_thm
 242   ("EXIST_TRANSITION_thm6",
 243    (`!(p:'a->bool) q st Pr1 Pr2.
 244        (!s. p s /\ ~q s ==> q (st s))
 245             ==> (p EXIST_TRANSITION q) (APPEND Pr1 (CONS st Pr2))`),
 246    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 247    LIST_INDUCT_TAC THEN
 248    LIST_INDUCT_TAC THEN
 249    REWRITE_TAC [EXIST_TRANSITION;APPEND] THEN
 250    REPEAT STRIP_TAC THEN
 251    RES_TAC THEN
 252    ASM_REWRITE_TAC []);;
 253
 254 let EXIST_TRANSITION_thm7 = prove_thm
 255   ("EXIST_TRANSITION_thm7",
 256    (`!(p:'a->bool) q FPr GPr.
 257      (p EXIST_TRANSITION q) FPr
 258               ==> (p EXIST_TRANSITION q) (APPEND FPr GPr)`),
 259    GEN_TAC THEN GEN_TAC THEN
 260    LIST_INDUCT_TAC THEN
 261    LIST_INDUCT_TAC THEN
 262    REWRITE_TAC [EXIST_TRANSITION;APPEND] THEN
 263    REPEAT STRIP_TAC THEN
 264    RES_TAC THEN
 265    ASM_REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND]);;
 266
 267 let EXIST_TRANSITION_thm8 = prove_thm
 268   ("EXIST_TRANSITION_thm8",
 269    (`!(p:'a->bool) q FPr GPr.
 270      (p EXIST_TRANSITION q) FPr
 271               ==> (p EXIST_TRANSITION q) (APPEND GPr FPr)`),
 272    GEN_TAC THEN GEN_TAC THEN
 273    LIST_INDUCT_TAC THEN
 274    LIST_INDUCT_TAC THEN
 275    REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND] THEN
 276    REPEAT STRIP_TAC THEN
 277    RES_TAC THEN
 278    ASM_REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND] THENL
 279    [
 280      REWRITE_TAC [UNDISCH_ALL (SPECL
 281       [`p:'a->bool`;`q:'a->bool`;`h:'a->'a`;`t':('a->'a)list`;`t:('a->'a)list`]
 282         EXIST_TRANSITION_thm6)]
 283     ;
 284      REWRITE_TAC [REWRITE_RULE [APPEND_lemma03] (SPECL
 285        [`(APPEND (t':('a->'a)list) [h])`]
 286         (ASSUME `!GPr:('a->'a)list. (p EXIST_TRANSITION q) (APPEND GPr t)`))]
 287    ]);;
 288
 289 let EXIST_TRANSITION_thm9 = prove_thm
 290   ("EXIST_TRANSITION_thm9",
 291    (`!(p:'a->bool) q st FPr GPr.
 292      (p EXIST_TRANSITION q) (APPEND FPr GPr)
 293               ==> (p EXIST_TRANSITION q) (APPEND FPr (CONS st GPr))`),
 294    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 295    LIST_INDUCT_TAC THEN
 296    REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND] THEN
 297    REPEAT STRIP_TAC THEN
 298    RES_TAC THEN
 299    ASM_REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND]);;
 300
 301 let EXIST_TRANSITION_thm10 = prove_thm
 302   ("EXIST_TRANSITION_thm10",
 303    (`!(p:'a->bool) q st Pr.
 304        (p EXIST_TRANSITION q) Pr ==> (p EXIST_TRANSITION q) (CONS st Pr)`),
 305    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 306    LIST_INDUCT_TAC THEN
 307    ASM_REWRITE_TAC [APPEND_lemma01;APPEND;EXIST_TRANSITION] THEN
 308    STRIP_TAC THEN
 309    ASM_REWRITE_TAC []);;
 310
 311 let EXIST_TRANSITION_thm11 = prove_thm
 312   ("EXIST_TRANSITION_thm11",
 313    (`!(p:'a->bool) q st Pr.
 314       (p EXIST_TRANSITION q) (APPEND [st] Pr) =
 315       (p EXIST_TRANSITION q) (APPEND  Pr [st])`),
 316    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 317    LIST_INDUCT_TAC THEN
 318    ASM_REWRITE_TAC [APPEND_lemma01;APPEND;EXIST_TRANSITION] THEN
 319    EQ_TAC THEN
 320    STRIP_TAC THEN
 321    RES_TAC THEN
 322    ASM_REWRITE_TAC [APPEND_lemma01;APPEND;EXIST_TRANSITION] THENL
 323    [
 324      REWRITE_TAC [REWRITE_RULE [APPEND_lemma02] (SYM (ASSUME
 325           `(((p:'a->bool) EXIST_TRANSITION q) (APPEND [st] t)) <=>
 326            ((p EXIST_TRANSITION q) (APPEND t [st]))`))] THEN
 327      ASM_REWRITE_TAC [EXIST_TRANSITION]
 328     ;
 329      REWRITE_TAC [REWRITE_RULE [APPEND_lemma02] (SYM (ASSUME
 330           `(((p:'a->bool) EXIST_TRANSITION q) (APPEND [st] t)) <=>
 331            ((p EXIST_TRANSITION q) (APPEND t [st]))`))] THEN
 332      ASM_REWRITE_TAC [UNDISCH_ALL (SPECL
 333        [`p:'a->bool`;`q:'a->bool`;`st:'a->'a`;`t:('a->'a)list`]
 334         EXIST_TRANSITION_thm10)]
 335     ;
 336      STRIP_ASSUME_TAC (REWRITE_RULE [APPEND_lemma02;EXIST_TRANSITION]
 337        (ASSUME `((p:'a->bool) EXIST_TRANSITION q) (APPEND [st] t)`)) THEN
 338      ASM_REWRITE_TAC []
 339    ]);;
 340
 341 let EXIST_TRANSITION_thm12a = prove_thm
 342   ("EXIST_TRANSITION_thm12a",
 343    (`!(p:'a->bool) q FPr GPr.
 344       (p EXIST_TRANSITION q) (APPEND FPr GPr) ==>
 345       (p EXIST_TRANSITION q) (APPEND GPr FPr)`),
 346    GEN_TAC THEN GEN_TAC THEN
 347    LIST_INDUCT_TAC THEN
 348    ASM_REWRITE_TAC [APPEND_lemma01;APPEND;EXIST_TRANSITION] THEN
 349    REPEAT STRIP_TAC THEN
 350    RES_TAC THEN
 351    ASM_REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND] THENL
 352     [
 353       REWRITE_TAC [UNDISCH_ALL (SPECL [`p:'a->bool`;`q:'a->bool`;`h:'a->'a`;
 354               `GPr:('a->'a)list`;`t:('a->'a)list`] EXIST_TRANSITION_thm6)]
 355      ;
 356       REWRITE_TAC [UNDISCH_ALL (SPECL [`p:'a->bool`;`q:'a->bool`;`h:'a->'a`;
 357               `GPr:('a->'a)list`;`t:('a->'a)list`] EXIST_TRANSITION_thm9)]
 358     ]);;
 359
 360 let EXIST_TRANSITION_thm12b = prove_thm
 361   ("EXIST_TRANSITION_thm12b",
 362    (`!(p:'a->bool) q FPr GPr.
 363       (p EXIST_TRANSITION q) (APPEND GPr FPr) ==>
 364       (p EXIST_TRANSITION q) (APPEND FPr GPr)`),
 365    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 366    LIST_INDUCT_TAC THEN
 367    ASM_REWRITE_TAC [APPEND_lemma01;APPEND;EXIST_TRANSITION] THEN
 368    REPEAT STRIP_TAC THEN
 369    RES_TAC THEN
 370    ASM_REWRITE_TAC [APPEND_lemma01;EXIST_TRANSITION;APPEND] THENL
 371     [
 372       REWRITE_TAC [UNDISCH_ALL (SPECL [`p:'a->bool`;`q:'a->bool`;`h:'a->'a`;
 373               `FPr:('a->'a)list`;`t:('a->'a)list`] EXIST_TRANSITION_thm6)]
 374      ;
 375       REWRITE_TAC [UNDISCH_ALL (SPECL [`p:'a->bool`;`q:'a->bool`;`h:'a->'a`;
 376               `FPr:('a->'a)list`;`t:('a->'a)list`] EXIST_TRANSITION_thm9)]
 377     ]);;
 378
 379 let EXIST_TRANSITION_thm12 = prove_thm
 380   ("EXIST_TRANSITION_thm12",
 381    (`!(p:'a->bool) q FPr GPr.
 382       (p EXIST_TRANSITION q) (APPEND GPr FPr) =
 383       (p EXIST_TRANSITION q) (APPEND FPr GPr)`),
 384    REPEAT GEN_TAC THEN
 385    EQ_TAC THEN
 386    REPEAT STRIP_TAC THEN
 387    RES_TAC THEN
 388    REWRITE_TAC [UNDISCH_ALL (SPEC_ALL EXIST_TRANSITION_thm12a);
 389                 UNDISCH_ALL (SPEC_ALL EXIST_TRANSITION_thm12b)]);;
 390
 391 (*---------------------------------------------------------------------------*)
 392 (*
 393   Theorems about ENSURES
 394 *)
 395 (*---------------------------------------------------------------------------*)
 396
 397 (*
 398   Reflexivity Theorem:
 399
 400                p ensures p in Pr
 401
 402   The theorem is only valid for non-empty programs
 403 *)
 404 let ENSURES_thm0 = prove_thm
 405   ("ENSURES_thm0",
 406    (`!(p:'a->bool) q. (p ENSURES q) [] = F`),
 407      REWRITE_TAC [ENSURES] THEN
 408      STRIP_TAC THEN
 409      REWRITE_TAC [UNLESS;EXIST_TRANSITION]);;
 410
 411 let ENSURES_thm1 = prove_thm
 412   ("ENSURES_thm1",
 413    (`!(p:'a->bool) st Pr. (p ENSURES p) (CONS st Pr)`),
 414      REWRITE_TAC [ENSURES] THEN
 415      STRIP_TAC THEN
 416      REWRITE_TAC [UNLESS;EXIST_TRANSITION] THEN
 417      REWRITE_TAC [UNLESS_thm1;UNLESS_STMT] THEN
 418      REWRITE_TAC [BETA_CONV (`(\s:'a. (p s /\ ~p s) ==> p (st s))s`)] THEN
 419      REWRITE_TAC[NOT_AND;IMP_CLAUSES]);;
 420
 421 (*
 422   Consequence Weakening Theorem:
 423
 424                p ensures q in Pr; q ==> r
 425               ----------------------------
 426                    p ensures r in Pr
 427 *)
 428
 429 let ENSURES_thm2 = prove_thm
 430   ("ENSURES_thm2",
 431    (`!(p:'a->bool) q r Pr.
 432          ((p ENSURES q) Pr /\ (!s:'a. (q s) ==> (r s)))
 433         ==>
 434          ((p ENSURES r) Pr)`),
 435    REWRITE_TAC [ENSURES] THEN
 436    REPEAT STRIP_TAC THENL
 437      [
 438       ASSUME_TAC (UNDISCH_ALL (SPEC (`!s:'a. q s ==> r s`)
 439         (SPEC (`((p:'a->bool) UNLESS q) Pr`) AND_INTRO_THM))) THEN
 440       STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL UNLESS_thm3))
 441      ;
 442       ASSUME_TAC (UNDISCH_ALL (SPEC (`!s:'a. q s ==> r s`)
 443         (SPEC (`((p:'a->bool) EXIST_TRANSITION q) Pr`) AND_INTRO_THM))) THEN
 444       STRIP_ASSUME_TAC (UNDISCH_ALL (SPEC_ALL EXIST_TRANSITION_thm1))
 445      ]);;
 446
 447 (*
 448   Impossibility Theorem:
 449
 450                p ensures false in Pr
 451               ----------------------
 452                        ~p
 453 *)
 454
 455 let ENSURES_thm3 = prove_thm
 456   ("ENSURES_thm3",
 457    (`!(p:'a->bool) Pr. ((p ENSURES False) Pr) ==> !s. (Not p)s`),
 458    GEN_TAC THEN
 459    LIST_INDUCT_TAC THEN
 460    ASM_REWRITE_TAC [ENSURES; UNLESS; EXIST_TRANSITION] THEN
 461    STRIP_TAC THEN
 462    ASM_REWRITE_TAC [] THENL
 463    [
 464      UNDISCH_TAC `!s:'a. (p:'a->bool) s /\ ~(False s) ==> False ((h:'a->'a) s)` THEN
 465      REWRITE_TAC [FALSE_def; NOT_def1] THEN
 466      CONV_TAC (DEPTH_CONV BETA_CONV)
 467     ;
 468      IMP_RES_TAC EXIST_TRANSITION_thm2
 469    ]);;
 470
 471 (*
 472   Conjunction Theorem:
 473
 474                    p unless q in Pr; p' ensures q' in Pr
 475               -----------------------------------------------
 476                p/\p' ensures (p/\q')\/(p'/\q)\/(q/\q') in Pr
 477 *)
 478 let ENSURES_thm4 = prove_thm
 479   ("ENSURES_thm4",
 480    (`!(p:'a->bool) q p' q' Pr.
 481     (p UNLESS q) Pr /\ (p' ENSURES q') Pr ==>
 482       ((p /\* p') ENSURES (((p /\* q') \/*  (p' /\* q)) \/*  (q /\* q')))
 483         Pr`),
 484    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 485    LIST_INDUCT_TAC THEN
 486    REWRITE_TAC [ENSURES;UNLESS;EXIST_TRANSITION] THEN
 487    REPEAT STRIP_TAC THEN
 488    ASM_REWRITE_TAC [] THENL
 489    [
 490     REWRITE_TAC
 491       [REWRITE_RULE [ASSUME `!s:'a. ((p:'a->bool) UNLESS_STMT q)   (h:'a->'a) s`;
 492                      ASSUME `!s:'a. ((p':'a->bool) UNLESS_STMT q') (h:'a->'a) s`]
 493         (SPECL [`p:'a->bool`;`q:'a->bool`;`p':'a->bool`;`q':'a->bool`;`h:'a->'a`]
 494                 UNLESS_STMT_thm3)]
 495    ;
 496     REWRITE_TAC
 497       [REWRITE_RULE [ASSUME `((p:'a->bool)  UNLESS q)  (t:('a->'a)list)`;
 498                      ASSUME `((p':'a->bool) UNLESS q') (t:('a->'a)list)`]
 499       (SPECL [`p:'a->bool`;`q:'a->bool`;`p':'a->bool`;`q':'a->bool`;`t:('a->'a)list`]
 500                 UNLESS_thm4)]
 501    ;
 502     REWRITE_TAC [REWRITE_RULE
 503          [ASSUME `!s:'a. ((p:'a->bool) UNLESS_STMT q) (h:'a->'a) s`;
 504           ASSUME `!s:'a. ((p':'a->bool) UNLESS_STMT q') (h:'a->'a) s`;
 505           ASSUME `!s:'a. (p':'a->bool) s /\ ~(q' s) ==> q' ((h:'a->'a) s)`]
 506        (SPEC_ALL ENSURES_lemma1)]
 507    ;
 508     REWRITE_TAC
 509       [REWRITE_RULE [ASSUME `!s:'a. ((p:'a->bool) UNLESS_STMT q)   (h:'a->'a) s`;
 510                      ASSUME `!s:'a. ((p':'a->bool) UNLESS_STMT q') (h:'a->'a) s`]
 511         (SPECL [`p:'a->bool`;`q:'a->bool`;`p':'a->bool`;`q':'a->bool`;`h:'a->'a`]
 512                 UNLESS_STMT_thm3)]
 513    ;
 514     UNDISCH_TAC `((p:'a->bool) UNLESS q) t /\ (p' ENSURES q') (t:('a->'a)list)
 515        ==> (p /\* p' ENSURES (p /\* q' \/* p' /\* q) \/* q /\* q') t` THEN
 516     ASM_REWRITE_TAC [ENSURES] THEN
 517     STRIP_TAC THEN
 518     ASM_REWRITE_TAC []
 519    ;
 520     UNDISCH_TAC `((p:'a->bool) UNLESS q) t /\ (p' ENSURES q') (t:('a->'a)list)
 521        ==> (p /\* p' ENSURES (p /\* q' \/* p' /\* q) \/* q /\* q') t` THEN
 522     ASM_REWRITE_TAC [ENSURES] THEN
 523     STRIP_TAC THEN
 524     ASM_REWRITE_TAC []
 525   ]);;
 526
 527 (*
 528   Conjunction Theorem:
 529
 530                    p ensures q in Pr
 531               -------------------------
 532                p\/r ensures q\/r in Pr
 533 *)
 534
 535 let ENSURES_thm5 = prove_thm
 536   ("ENSURES_thm5",
 537    (`!(p:'a->bool) q r Pr.
 538       ((p ENSURES q) Pr) ==> (((p \/* r) ENSURES (q \/* r)) Pr)`),
 539    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
 540    LIST_INDUCT_TAC THEN
 541    REWRITE_TAC [ENSURES;UNLESS;EXIST_TRANSITION] THEN
 542    REPEAT STRIP_TAC THEN
 543    ASM_REWRITE_TAC [] THENL
 544    [
 545      IMP_RES_TAC UNLESS_STMT_thm6 THEN
 546      ASM_REWRITE_TAC []
 547     ;
 548      IMP_RES_TAC UNLESS_cor23 THEN
 549      ASM_REWRITE_TAC []
 550     ;
 551      REWRITE_TAC [REWRITE_RULE
 552       [ASSUME `!s:'a. (p:'a->bool) s /\ ~q s ==> q (h s)`]
 553         (SPECL [`p:'a->bool`;`q:'a->bool`;`r:'a->bool`;`h:'a->'a`]
 554             ENSURES_lemma4)]
 555     ;
 556      IMP_RES_TAC UNLESS_STMT_thm6 THEN
 557      ASM_REWRITE_TAC []
 558     ;
 559      IMP_RES_TAC UNLESS_cor23 THEN
 560      ASM_REWRITE_TAC []
 561     ;
 562      IMP_RES_TAC EXIST_TRANSITION_thm4 THEN
 563      ASM_REWRITE_TAC []
 564    ]);;
 565
 566 (*
 567  -----------------------------------------------------------------------------
 568   Corollaries about ENSURES
 569  -----------------------------------------------------------------------------
 570 *)
 571
 572 (*
 573   Implies Corollary:
 574
 575                    p => q
 576               -------------------
 577                p ensures q in Pr
 578
 579   This corollary is only valid for non-empty programs.
 580 *)
 581
 582 let ENSURES_cor1 = prove_thm
 583   ("ENSURES_cor1",
 584    (`!(p:'a->bool) q st Pr.
 585     (!s. p s ==> q s) ==> (p ENSURES q) (CONS st Pr)`),
 586    REPEAT GEN_TAC THEN
 587    DISCH_TAC THEN
 588    ASSUME_TAC (SPEC_ALL ENSURES_thm1) THEN
 589    ASSUME_TAC (UNDISCH_ALL (SPECL
 590      [(`((p:'a->bool) ENSURES p)(CONS st Pr)`);(`!s:'a. p s ==> q s`)]
 591       AND_INTRO_THM)) THEN
 592    STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
 593      [(`p:'a->bool`);(`p:'a->bool`);(`q:'a->bool`);
 594       (`CONS (st:'a->'a) Pr`)]
 595       ENSURES_thm2)));;
 596
 597 let ENSURES_cor2 = prove_thm
 598   ("ENSURES_cor2",
 599    (`!(p:'a->bool) q Pr. (p ENSURES q) Pr ==> (p UNLESS q) Pr`),
 600    REWRITE_TAC [ENSURES] THEN
 601    REPEAT STRIP_TAC);;
 602
 603 let ENSURES_cor3 = prove_thm
 604   ("ENSURES_cor3",
 605    (`!(p:'a->bool) q r Pr.
 606         ((p \/*  q) ENSURES r)Pr ==> (p ENSURES (q \/*  r))Pr`),
 607    REPEAT GEN_TAC THEN
 608    DISCH_TAC THEN
 609    ASSUME_TAC (UNDISCH_ALL (SPECL
 610      [(`((p:'a->bool) \/*  q)`);(`r:'a->bool`);
 611       (`Pr:('a->'a)list`)] ENSURES_cor2)) THEN
 612    ASSUME_TAC (UNDISCH_ALL (SPECL
 613      [(`p:'a->bool`);(`q:'a->bool`);(`r:'a->bool`);
 614       (`Pr:('a->'a)list`)] UNLESS_cor4)) THEN
 615    ASSUME_TAC (UNDISCH_ALL (SPECL
 616      [(`((p:'a->bool) UNLESS (q \/*  r))Pr`);
 617       (`(((p:'a->bool) \/*  q) ENSURES r)Pr`)]
 618       AND_INTRO_THM)) THEN
 619    ASSUME_TAC (UNDISCH_ALL (SPECL
 620      [(`p:'a->bool`);(`((q:'a->bool) \/*  r)`);
 621       (`((p:'a->bool) \/*  q)`);(`r:'a->bool`);
 622       (`Pr:('a->'a)list`)] ENSURES_thm4)) THEN
 623    UNDISCH_TAC (`(((p:'a->bool) /\* (p \/*  q)) ENSURES
 624                 (((p /\* r) \/*  ((p \/*  q) /\* (q \/*  r))) \/*
 625                  ((q \/*  r) /\* r))) Pr`) THEN
 626    REWRITE_TAC [AND_OR_EQ_lemma] THEN
 627    REWRITE_TAC [OR_ASSOC_lemma;AND_ASSOC_lemma] THEN
 628    PURE_ONCE_REWRITE_TAC [SPECL
 629          [(`((q:'a->bool) \/*  r)`);
 630           (`r:'a->bool`)] AND_COMM_lemma] THEN
 631    ONCE_REWRITE_TAC [AND_OR_EQ_AND_COMM_OR_lemma] THEN
 632    REWRITE_TAC [AND_OR_EQ_lemma] THEN
 633    DISCH_TAC THEN
 634    ASSUME_TAC (SPECL [(`p:'a->bool`);(`q:'a->bool`);(`r:'a->bool`)]
 635                            IMPLY_WEAK_lemma5) THEN
 636    ASSUME_TAC (UNDISCH_ALL (SPECL
 637     [(`((p:'a->bool) ENSURES
 638       ((p /\* r) \/*  (((p \/*  q) /\* (q \/*  r)) \/*  r)))Pr`);
 639      (`!s:'a. ((p /\* r) \/*  (((p \/*  q) /\* (q \/*  r)) \/* r))s ==>
 640          (q \/*  r)s`)]
 641      AND_INTRO_THM)) THEN
 642    STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
 643     [(`p:'a->bool`);
 644      (`(((p:'a->bool) /\* r) \/* (((p \/*  q) /\* (q \/*  r)) \/* r))`);
 645      (`((q:'a->bool) \/*  r)`);(`Pr:('a->'a)list`)]
 646      ENSURES_thm2)));;
 647
 648 let ENSURES_cor4 = prove_thm
 649   ("ENSURES_cor4",
 650    (`!(p:'a->bool) q r Pr. (p ENSURES (q \/*  r)) Pr ==>
 651               ((p /\* (Not  q)) ENSURES (q \/*  r)) Pr`),
 652    REPEAT STRIP_TAC THEN
 653    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL ENSURES_lemma3)) THEN
 654    ASSUME_TAC (UNDISCH_ALL (SPECL
 655      [(`((p:'a->bool) /\* (Not  q))`);(`((p:'a->bool) /\* q)`);
 656       (`((q:'a->bool) \/* r)`);(`Pr:('a->'a)list`)] ENSURES_cor3)) THEN
 657    UNDISCH_TAC
 658      (`(((p:'a->bool) /\* (Not  q)) ENSURES
 659           ((p /\* q) \/* (q \/* r)))Pr`) THEN
 660    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL OR_ASSOC_lemma))] THEN
 661    REWRITE_TAC [P_AND_Q_OR_Q_lemma]);;
 662
 663 (*
 664   Consequence Weakening Corollary:
 665
 666                   p ensures q in Pr
 667               -------------------------
 668                p ensures (q \/ r) in Pr
 669 *)
 670
 671 let ENSURES_cor5 = prove_thm
 672  ("ENSURES_cor5",
 673    (`!(p:'a->bool) q r Pr.
 674          (p ENSURES q) Pr ==> (p ENSURES (q \/*  r)) Pr`),
 675    REPEAT STRIP_TAC THEN
 676    ASSUME_TAC (SPECL [(`q:'a->bool`);(`r:'a->bool`)]
 677                IMPLY_WEAK_lemma_b) THEN
 678    ASSUME_TAC (SPECL
 679      [(`p:'a->bool`);(`q:'a->bool`);(`(q:'a->bool) \/* r`)]
 680                ENSURES_thm2) THEN
 681    RES_TAC);;
 682
 683 (*
 684   Always Corollary:
 685
 686                   false ensures p in Pr
 687 *)
 688
 689 let ENSURES_cor6 = prove_thm
 690   ("ENSURES_cor6",
 691    (`!(p:'a->bool) st Pr. (False ENSURES p) (CONS st Pr)`),
 692    REWRITE_TAC [ENSURES;UNLESS_cor7;EXIST_TRANSITION_thm3]);;
 693
 694 let ENSURES_cor7 = prove_thm
 695   ("ENSURES_cor7",
 696    (`!(p:'a->bool) q r Pr.
 697         (p ENSURES q) Pr /\ (r STABLE Pr)
 698        ==>
 699         ((p /\* r) ENSURES (q /\*
 700  r))Pr`),
 701    REPEAT GEN_TAC THEN
 702    REWRITE_TAC [STABLE] THEN
 703    REPEAT STRIP_TAC THEN
 704    IMP_RES_TAC (ONCE_REWRITE_RULE [AND_COMM_lemma]
 705       (REWRITE_RULE [AND_False_lemma;OR_False_lemma]
 706         (ONCE_REWRITE_RULE [OR_AND_COMM_lemma]
 707           (REWRITE_RULE [AND_False_lemma;OR_False_lemma] (SPECL
 708             [(`r:'a->bool`);(`False:'a->bool`);
 709              (`p:'a->bool`);(`q:'a->bool`);
 710              (`Pr:('a->'a)list`)] ENSURES_thm4))))));;