Unity/mk_leadsto.ml

   1 (*---------------------------------------------------------------------------*)
   2 (*
   3    File:         mk_leadsto.ml
   4
   5    Description:  This file defines LEADSTO and the theorems and corrollaries
   6                  described in [CM88].
   7
   8    Author:       (c) Copyright 1990-2008 by Flemming Andersen
   9    Date:         July 24. 1990
  10    Updated:      November 11, 1991 (including LUB)
  11    Updated:      October 3, 1992 (including state space restriction)
  12    Last Update:  December 30, 2007
  13 *)
  14 (*---------------------------------------------------------------------------*)
  15
  16 (*
  17  We want to define a function LeadstoRel, which satisfies the three
  18  properties of the given axiomatic definition of LEADSTO:
  19
  20                   p ensures q in Pr
  21                  ------------------- (1)
  22                   p leadsto q in Pr
  23
  24          p leadsto q in Pr,  q leadsto r in Pr
  25         -------------------------------------- (2)
  26                   p leadsto r in Pr
  27
  28                  !i. (p i) leadsto q in Pr
  29                ------------------------- (3)
  30                 (?i. p i) leadsto q in Pr
  31 *)
  32 let LUB = new_definition
  33   `LUB (P:('a->bool)->bool) = \s:'a. ?p. (P p) /\ p s`;;
  34
  35 let IN = new_infix_definition
  36   ("In", "<=>",
  37    `In (p:'a->bool) (P:('a->bool)->bool) = P p`, TL_FIX);;
  38
  39 let LeadstoRel = new_definition
  40    (`LeadstoRel R Pr =
  41       !(p:'a->bool) q.
  42         ((p ENSURES q)Pr                                 ==> R p q Pr) /\
  43         (!r. (R p r Pr /\ R r q Pr)                      ==> R p q Pr) /\
  44         (!P.  (p = LUB P) /\ (!p. (p In P) ==> R p q Pr) ==> R p q Pr)`);;
  45
  46 (*
  47    Now we may define LEADSTO:
  48 *)
  49 let LEADSTO = new_infix_definition
  50   ("LEADSTO", "<=>",
  51    (`LEADSTO (p:'a->bool) q Pr = (!R. (LeadstoRel R Pr) ==> (R p q Pr))`),
  52      TL_FIX);;
  53
  54 (*
  55         Prove that the given axioms 1, 2, 3 are really theorems for the family
  56 *)
  57
  58 (* Prove:
  59    !P Q Pr. (P ENSURES Q)Pr ==> (P LEADSTO Q)Pr
  60 *)
  61 let LEADSTO_thm0 = prove_thm
  62   ("LEADSTO_thm0",
  63    (`!(p:'a->bool) q Pr. (p ENSURES q) Pr ==> (p LEADSTO q)Pr`),
  64    REWRITE_TAC [LEADSTO; LeadstoRel] THEN
  65    REPEAT STRIP_TAC THEN
  66    RES_TAC);;
  67
  68 (* Prove:
  69    !P Q R Pr.
  70     (P LEADSTO Q)Pr /\ (Q LEADSTO R)Pr ==> (P LEADSTO R)Pr
  71 *)
  72 let LEADSTO_thm1 = prove_thm
  73   ("LEADSTO_thm1",
  74    (`!(p:'a->bool) r q Pr.
  75         (p LEADSTO r)Pr /\ (r LEADSTO q)Pr ==> (p LEADSTO q) Pr`),
  76    REWRITE_TAC [LEADSTO; LeadstoRel] THEN
  77    REPEAT STRIP_TAC THEN
  78    RES_TAC THEN
  79    RES_TAC);;
  80
  81 (* Prove:
  82    !P Q R Pr.
  83     (P ENSURES Q)Pr /\ (Q LEADSTO R)Pr ==> (P LEADSTO R)Pr
  84 *)
  85 let LEADSTO_thm2 = prove_thm
  86   ("LEADSTO_thm2",
  87    (`!(p:'a->bool) r q Pr.
  88         (p ENSURES r)Pr /\ (r LEADSTO q)Pr ==> (p LEADSTO q) Pr`),
  89    REWRITE_TAC [LEADSTO; LeadstoRel] THEN
  90    REPEAT STRIP_TAC THEN
  91    RES_TAC THEN
  92    RES_TAC);;
  93
  94 (* Prove:
  95    !P Q R Pr.
  96     (P ENSURES Q)Pr /\ (Q ENSURES R)Pr ==> (P LEADSTO R)Pr
  97 *)
  98 let LEADSTO_thm2a = prove_thm
  99   ("LEADSTO_thm2a",
 100    (`!(p:'a->bool) r q Pr.
 101         (p ENSURES r)Pr /\ (r ENSURES q)Pr ==> (p LEADSTO q) Pr`),
 102    REWRITE_TAC [LEADSTO; LeadstoRel] THEN
 103    REPEAT STRIP_TAC THEN
 104    RES_TAC THEN
 105    RES_TAC);;
 106
 107 (* Prove:
 108    !P q Pr. (!i. (P i) LEADSTO q)Pr ==> ((( ?* )  P) LEADSTO q)Pr
 109 *)
 110 let LEADSTO_thm3_lemma01 = TAC_PROOF
 111   (([],
 112    (`(!p:'a->bool.
 113         p In P ==>
 114         (!R.
 115           (!p q.
 116             ((p ENSURES q)Pr ==> R p q Pr) /\
 117             (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
 118             (!P.
 119               (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==> R p q Pr)) ==>
 120           R p q Pr))
 121         ==>
 122        (!p:'a->bool.
 123         p In P ==>
 124         ((!p q.
 125             ((p ENSURES q)Pr ==> R p q Pr) /\
 126             (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
 127             (!P.
 128               (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==> R p q Pr)) ==>
 129           R p q Pr))`)),
 130    REPEAT STRIP_TAC THEN
 131    RES_TAC);;
 132
 133 let LEADSTO_thm3 = prove_thm
 134   ("LEADSTO_thm3",
 135    (`!p (P:('a->bool)->bool) q Pr.
 136       ((p = LUB P) /\ (!p. (p In P) ==> (p LEADSTO q)Pr)) ==> (p LEADSTO q)Pr`),
 137    REPEAT GEN_TAC THEN
 138    REWRITE_TAC [LEADSTO;LeadstoRel] THEN
 139    REPEAT STRIP_TAC THEN
 140    ASSUME_TAC (GEN_ALL (REWRITE_RULE[ASSUME
 141      (`!(p:'a->bool) q.
 142         ((p ENSURES q)Pr ==> R p q Pr) /\
 143         (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
 144         (!P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==> R p q Pr)`)]
 145            (SPEC_ALL (UNDISCH (SPEC_ALL LEADSTO_thm3_lemma01))))) THEN
 146    RES_TAC);;
 147
 148 let LEADSTO_thm3a = prove_thm
 149   ("LEADSTO_thm3a",
 150    (`!(P:('a->bool)->bool) q Pr.
 151        (!p. (p In P) ==> (p LEADSTO q)Pr) ==> ((LUB P) LEADSTO q)Pr`),
 152    REPEAT GEN_TAC THEN
 153    ACCEPT_TAC (SPEC_ALL
 154     (REWRITE_RULE [] (SPECL
 155       [(`LUB (P:('a->bool)->bool)`); (`P:('a->bool)->bool`)] LEADSTO_thm3))));;
 156
 157 let LEADSTO_thm3c_lemma01 = TAC_PROOF
 158   (([],
 159    (`!p:'a->bool. p In (\p. ?i. p = P (i:num)) = (?i. p = P i)`)),
 160    REWRITE_TAC [IN] THEN
 161    BETA_TAC THEN
 162    REWRITE_TAC []);;
 163
 164 let LEADSTO_thm3c_lemma02 = TAC_PROOF
 165   (([],
 166    (`!(P:num->'a->bool) q i.
 167        ((?i'. P i = P i') ==> q) = (!i'. (P i = P i') ==> q)`)),
 168    REPEAT GEN_TAC THEN
 169    EQ_TAC THEN
 170    REPEAT STRIP_TAC THENL
 171     [
 172      ASM_CASES_TAC (`?i'. (P:num->'a->bool) i = P i'`) THEN
 173      RES_TAC
 174     ;
 175      ACCEPT_TAC (REWRITE_RULE [SYM (ASSUME (`(P:num->'a->bool) i = P i'`))]
 176       (SPEC_ALL (ASSUME (`!i'. ((P:num->'a->bool) i = P i') ==> q`))))
 177     ]);;
 178
 179 let LEADSTO_thm3c_lemma03 = TAC_PROOF
 180   (([],
 181    (`(!p:'a->bool. (?i. p = P i) ==> (p LEADSTO q)Pr) =
 182     (!i:num. ((P i) LEADSTO q)Pr)`)),
 183    EQ_TAC THEN
 184    REPEAT STRIP_TAC THENL
 185     [
 186      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`i:num`) (REWRITE_RULE
 187       [LEADSTO_thm3c_lemma02] (SPEC (`(P:num->'a->bool)i`) (ASSUME
 188        (`!p:'a->bool. (?i:num. p = P i) ==> (p LEADSTO q)Pr`))))))
 189     ;
 190      ASM_REWRITE_TAC []
 191     ]);;
 192
 193 let LEADSTO_thm3c_lemma04 = TAC_PROOF
 194   (([],
 195    (`!s. ((?*) (P:num->'a->bool))s <=> (LUB(\p. ?i. p = P i))s`)),
 196    REPEAT GEN_TAC THEN
 197    REWRITE_TAC [EXISTS_def; LUB] THEN
 198    BETA_TAC THEN
 199    EQ_TAC THEN
 200    REPEAT STRIP_TAC THENL
 201     [
 202      EXISTS_TAC (`(P:num->'a->bool)x`) THEN
 203      ASM_REWRITE_TAC [] THEN
 204      EXISTS_TAC (`x:num`) THEN
 205      REFL_TAC
 206     ;
 207      EXISTS_TAC (`i:num`) THEN
 208      ACCEPT_TAC (ONCE_REWRITE_RULE [ASSUME (`p = (P:num->'a->bool)i`)]
 209       (ASSUME (`(p:'a->bool) s`)))
 210     ]);;
 211
 212 let LEADSTO_thm3c = prove_thm
 213   ("LEADSTO_thm3c",
 214    (`!(P:num->'a->bool) q Pr.
 215         (!i. ((P i) LEADSTO q)Pr) ==> (((?*)  P) LEADSTO q)Pr`),
 216    REPEAT STRIP_TAC THEN
 217    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm3c_lemma03]
 218     (REWRITE_RULE [LEADSTO_thm3c_lemma01] (ISPEC
 219        (`\p. ?i. (p = (P:num->'a->bool)i)`) LEADSTO_thm3a))) THEN
 220    RES_TAC THEN
 221    ASM_REWRITE_TAC [REWRITE_RULE [ETA_AX] (MK_ABS LEADSTO_thm3c_lemma04)]);;
 222
 223 (* Prove:
 224    !p1 p2 q Pr.
 225      (p1 LEADSTO q)Pr /\ (p2 LEADSTO q)Pr ==> ((p1 \/* p2) LEADSTO q)Pr
 226 *)
 227
 228 (*
 229   To prove this we need some general lemmas about expressing two known
 230   relations as one relation:
 231 *)
 232
 233 (*
 234   |- !p1 p2 s. (p1 \/* p2)s = LUB(\p. (p = p1) \/ (p = p2))s
 235 *)
 236 let LEADSTO_thm4_lemma1a = TAC_PROOF
 237   (([],
 238    (`!(p1:'a->bool) p2 s.
 239         (p1 \/* p2) s = (LUB (\p. (p = p1) \/ (p = p2))) s`)),
 240    REPEAT GEN_TAC THEN
 241    REWRITE_TAC [LUB; OR_def ] THEN
 242    BETA_TAC THEN
 243    EQ_TAC THENL
 244      [
 245       STRIP_TAC THENL
 246        [
 247         EXISTS_TAC (`p1:'a->bool`) THEN
 248         ASM_REWRITE_TAC []
 249        ;
 250         EXISTS_TAC (`p2:'a->bool`) THEN
 251         ASM_REWRITE_TAC []
 252        ]
 253      ;
 254       STRIP_TAC THENL
 255        [
 256         REWRITE_TAC [REWRITE_RULE [ASSUME (`(p:'a->bool) = p1`)] (ASSUME
 257          (`(p:'a->bool) s`))]
 258        ;
 259         REWRITE_TAC [REWRITE_RULE [ASSUME (`(p:'a->bool) = p2`)] (ASSUME
 260          (`(p:'a->bool) s`))]
 261        ]
 262      ]);;
 263
 264 (*
 265   |- !p1 p2. p1 \/* p2 = LUB(\p. (p = p1) \/ (p = p2))
 266 *)
 267 let LEADSTO_thm4_lemma1 =
 268     (GEN_ALL (REWRITE_RULE [ETA_AX]
 269                     (MK_ABS (GEN (`s:'a`)
 270                              (SPEC_ALL LEADSTO_thm4_lemma1a)))));;
 271
 272 (*
 273   |- !R p1 p2 q Pr.
 274     R p1 q Pr ==> R p2 q Pr ==> (!p. (\p. (p = p1) \/ (p = p2))p ==> R p q Pr)
 275 *)
 276 let LEADSTO_thm4_lemma2 = TAC_PROOF
 277   (([],
 278    (`!R (p1:'a->bool) p2 (q:'a->bool) (Pr:('a->'a)list).
 279       R p1 q Pr ==> R p2 q Pr ==>
 280        (!p. (\p. (p = p1) \/ (p = p2))p ==> R p q Pr)`)),
 281    BETA_TAC THEN
 282    REPEAT STRIP_TAC THEN
 283    ASM_REWRITE_TAC []);;
 284
 285 (*
 286   |- !R p1 p2 q Pr. R p1 q Pr ==> R p2 q Pr ==>
 287       (!p q P. (p = LUB P) /\ (!p. P p ==> R p q Pr) ==> R p q Pr)
 288            ==> R(p1 \/* p2) q Pr
 289 *)
 290 let LEADSTO_thm4_lemma3 = TAC_PROOF
 291   (([],
 292    (`!R (p1:'a->bool) p2 (q:'a->bool) (Pr:('a->'a)list).
 293      R p1 q Pr ==> R p2 q Pr ==>
 294        (!p q P. (p = LUB P) /\ (!p. P p ==> R p q Pr) ==> R p q Pr) ==>
 295           R (p1 \/* p2) q Pr`)),
 296    REPEAT STRIP_TAC THEN
 297    ACCEPT_TAC (REWRITE_RULE
 298     [SYM (SPEC_ALL LEADSTO_thm4_lemma1);
 299      UNDISCH_ALL (SPEC_ALL LEADSTO_thm4_lemma2)]
 300       (SPECL
 301         [(`(p1:'a->bool) \/* p2`); (`q:'a->bool`);
 302          (`\p:'a->bool. (p = p1) \/ (p = p2)`)]
 303            (ASSUME (`!p (q:'a->bool) (P:('a->bool)->bool). (p = LUB P) /\
 304                     (!p. P p ==> R p q Pr) ==> R p q (Pr:('a->'a)list)`)))));;
 305 (*
 306   Now Prove that the finite disjunction is satisfied
 307 *)
 308
 309 (*
 310 |- !p1 p2 q Pr.
 311       (p1 LEADSTO q)Pr /\ (p2 LEADSTO q)Pr ==> ((p1 \/* p2) LEADSTO q)Pr
 312 *)
 313 let LEADSTO_thm4 = prove_thm
 314   ("LEADSTO_thm4",
 315    (`!(p1:'a->bool) p2 q Pr.
 316         (p1 LEADSTO q)Pr /\ (p2 LEADSTO q)Pr ==>
 317             ((p1 \/* p2) LEADSTO q)Pr`),
 318    REWRITE_TAC [LEADSTO;LeadstoRel] THEN
 319    (* BETA_TAC THEN *)
 320    REPEAT STRIP_TAC THEN
 321    RES_TAC THEN
 322    ASSUME_TAC (GEN(`p:'a->bool`)(GEN(`q:'a->bool`)(REWRITE_RULE [IN]
 323    (CONJUNCT2 (CONJUNCT2 (SPEC_ALL
 324     (ASSUME
 325       (`!(p:'a->bool) q.
 326         ((p ENSURES q)Pr ==> R p q Pr) /\
 327         (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
 328         (!P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==>
 329             R p q Pr)`)))))))) THEN
 330    ACCEPT_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO_thm4_lemma3)));;
 331
 332 (*
 333    Prove:
 334       ((p ENSURES q)Pr \/
 335        (?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) \/
 336        (?P. (p = (( ?* )  P)) /\ (!i. ((P i) LEADSTO q)Pr))) =
 337           (p LEADSTO q)Pr
 338 *)
 339 let LEADSTO_thm5_lemma1 = TAC_PROOF
 340   (([],
 341    `!(p:'a->bool) s. (p s = (\s. ?p'. (if (p = p') then T else F) /\ p' s)s)`),
 342    REPEAT GEN_TAC THEN
 343    BETA_TAC THEN
 344    EQ_TAC THEN REPEAT STRIP_TAC THENL
 345     [
 346      EXISTS_TAC (`p:'a->bool`) THEN
 347      ASM_REWRITE_TAC []
 348     ;
 349      UNDISCH_TAC (`(if ((p:'a->bool) = p') then T else F)`) THEN
 350      REPEAT COND_CASES_TAC THEN
 351      ASM_REWRITE_TAC []
 352     ]);;
 353
 354 (*
 355    |- !p. p = (\s. ?p'. ((p = p') => T | F) /\ p' s)
 356 *)
 357 let LEADSTO_thm5_lemma2 = (GEN_ALL
 358      (REWRITE_RULE [ETA_AX]
 359       (MK_ABS (SPEC (`p:'a->bool`) LEADSTO_thm5_lemma1))));;
 360
 361 let LEADSTO_thm5_lemma3 = TAC_PROOF
 362   (([],
 363    (`!(p:'a->bool) p'. (if (p = p') then T else F) = (p = p')`)),
 364    REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN REWRITE_TAC []);;
 365
 366
 367 (*
 368   |- !p q Pr.
 369        (p ENSURES q)Pr \/
 370        (?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) \/
 371        (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))
 372       =
 373        (p LEADSTO q)Pr
 374 *)
 375 let LEADSTO_thm5 = prove_thm
 376   ("LEADSTO_thm5",
 377    (`!(p:'a->bool) q Pr.
 378       ((p ENSURES q) Pr \/
 379       (?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) \/
 380       (?P:('a->bool)->bool. (p = LUB P) /\ (!p. (p In P) ==> (p LEADSTO q)Pr)))
 381      =
 382       (p LEADSTO q)Pr`),
 383    REPEAT STRIP_TAC THEN
 384    EQ_TAC THENL
 385      [
 386       REPEAT STRIP_TAC THENL
 387         [
 388          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO_thm0))
 389         ;
 390          IMP_RES_TAC LEADSTO_thm1
 391         ;
 392          IMP_RES_TAC LEADSTO_thm3
 393         ]
 394      ;
 395       REPEAT STRIP_TAC THEN
 396       DISJ2_TAC THEN
 397       DISJ2_TAC THEN
 398       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 399       REWRITE_TAC [LUB; IN] THEN
 400       BETA_TAC THEN
 401       CONJ_TAC THENL
 402        [
 403         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 404        ;
 405         GEN_TAC THEN
 406         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 407         DISCH_TAC THEN
 408         ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 409          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 410        ]
 411      ]);;
 412
 413 (*
 414    Prove:
 415       ((p ENSURES q)Pr \/
 416        (?r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 417        (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))
 418       =
 419        (p LEADSTO q)Pr
 420 *)
 421 let LEADSTO_thm6 = prove_thm
 422   ("LEADSTO_thm6",
 423    (`!(p:'a->bool) q Pr.
 424        ((p ENSURES q) Pr \/
 425         (?r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 426         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)))
 427       =
 428         (p LEADSTO q)Pr`),
 429    REPEAT STRIP_TAC THEN
 430    EQ_TAC THENL
 431      [
 432       REPEAT STRIP_TAC THENL
 433         [
 434          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO_thm0))
 435         ;
 436          IMP_RES_TAC LEADSTO_thm2
 437         ;
 438          IMP_RES_TAC LEADSTO_thm3
 439         ]
 440      ;
 441       REPEAT STRIP_TAC THEN
 442       DISJ2_TAC THEN
 443       DISJ2_TAC THEN
 444       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 445       REWRITE_TAC [LUB; IN] THEN
 446       BETA_TAC THEN
 447       CONJ_TAC THENL
 448        [
 449         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 450        ;
 451         GEN_TAC THEN
 452         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 453         DISCH_TAC THEN
 454         ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 455          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 456        ]
 457      ]);;
 458
 459 (*
 460    Prove:
 461       ((p ENSURES q)Pr \/
 462        (?r. (p ENSURES r)Pr /\ (r ENSURES q)Pr) \/
 463        (?P. (p = (( ?* )  P)) /\ (!i. ((P i) LEADSTO q)Pr))) =
 464           (p LEADSTO q)Pr
 465 *)
 466 let LEADSTO_thm7 = prove_thm
 467   ("LEADSTO_thm7",
 468    (`!(p:'a->bool) q Pr.
 469        ((p ENSURES q) Pr \/
 470         (?r. (p ENSURES r)Pr /\ (r ENSURES q)Pr) \/
 471         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))) =
 472            (p LEADSTO q)Pr`),
 473    REPEAT STRIP_TAC THEN
 474    EQ_TAC THENL
 475      [
 476       REPEAT STRIP_TAC THENL
 477         [
 478          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO_thm0))
 479         ;
 480          IMP_RES_TAC LEADSTO_thm2a
 481         ;
 482          IMP_RES_TAC LEADSTO_thm3
 483         ]
 484      ;
 485       REPEAT STRIP_TAC THEN
 486       DISJ2_TAC THEN
 487       DISJ2_TAC THEN
 488       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 489       REWRITE_TAC [LUB; IN] THEN
 490       BETA_TAC THEN
 491       CONJ_TAC THENL
 492        [
 493         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 494        ;
 495         GEN_TAC THEN
 496         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 497         DISCH_TAC THEN
 498         ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 499          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 500        ]
 501      ]);;
 502
 503 (*
 504    Prove:
 505       ((p ENSURES q)Pr \/
 506       (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) =
 507           (p LEADSTO q)Pr
 508 *)
 509 let LEADSTO_thm8 = prove_thm
 510   ("LEADSTO_thm8",
 511    (`!(p:'a->bool) q Pr.
 512        ((p ENSURES q) Pr \/
 513         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)))
 514       =
 515         (p LEADSTO q)Pr`),
 516    REPEAT STRIP_TAC THEN
 517    EQ_TAC THENL
 518      [
 519       REPEAT STRIP_TAC THENL
 520         [
 521          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO_thm0))
 522         ;
 523          IMP_RES_TAC LEADSTO_thm3 THEN
 524          ASM_REWRITE_TAC []
 525         ]
 526      ;
 527       REPEAT STRIP_TAC THEN
 528       DISJ2_TAC THEN
 529       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 530       REWRITE_TAC [LUB; IN] THEN
 531       BETA_TAC THEN
 532       CONJ_TAC THENL
 533        [
 534         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 535        ;
 536         GEN_TAC THEN
 537         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 538         DISCH_TAC THEN
 539         ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 540          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 541        ]
 542      ]);;
 543
 544 (*
 545    Prove:
 546      (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr)) = (p LEADSTO q)Pr
 547 *)
 548 let LEADSTO_thm9 = prove_thm
 549   ("LEADSTO_thm9",
 550    (`!(p:'a->bool) q Pr.
 551       (?P. (p = LUB P) /\
 552        (!p. p In P ==> (p LEADSTO q)Pr)) = (p LEADSTO q)Pr`),
 553    REPEAT STRIP_TAC THEN
 554    EQ_TAC THENL
 555      [
 556       REPEAT STRIP_TAC THEN
 557       IMP_RES_TAC LEADSTO_thm3 THEN
 558       ASM_REWRITE_TAC []
 559      ;
 560       REPEAT STRIP_TAC THEN
 561       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 562       REWRITE_TAC [LUB; IN] THEN
 563       BETA_TAC THEN
 564       CONJ_TAC THENL
 565        [
 566         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 567        ;
 568         GEN_TAC THEN
 569         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 570         DISCH_TAC THEN
 571         ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 572          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 573        ]
 574      ]);;
 575
 576 (* Prove:
 577
 578   !P Q Pr. (P LEADSTO Q) [] = false
 579
 580 *)
 581
 582 (*
 583    Theorem LEADSTO_thm10 does Not hold for the generalised disjunctive
 584    rule, since:
 585
 586      (!P. (p = LUB P) /\ (!p'. p' In P ==> F) ==> F))
 587
 588    is only satisfied when P is non-empty
 589
 590 let LEADSTO_thm10 = prove_thm
 591   ("LEADSTO_thm10",
 592    (`!(p:'a->bool) q. (p LEADSTO q) [] = F`),
 593    REPEAT GEN_TAC THEN
 594    REWRITE_TAC [LEADSTO;LeadstoRel] THEN
 595    CONV_TAC NOT_FORALL_CONV THEN
 596    EXISTS_TAC (`\(p:'a->bool) (q:'a->bool) (Pr:('a->'a)list). F`) THEN
 597    BETA_TAC THEN
 598    REWRITE_TAC [ENSURES_thm0] THEN
 599    REPEAT GEN_TAC THEN
 600    REWRITE_TAC [DE_MORGAN_THM] THEN
 601    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL IMP_DISJ_THM))] THEN
 602    REWRITE_TAC [In,LUB] THEN
 603    STRIP_TAC THEN
 604    CONV_TAC NOT_FORALL_CONV THEN
 605    REWRITE_TAC [] THEN
 606
 607    ...
 608
 609 *)
 610
 611 (*
 612    Prove:
 613        (?r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) = (p LEADSTO q)Pr
 614 *)
 615 let LEADSTO_thm11 = prove_thm
 616   ("LEADSTO_thm11",
 617    (`!(p:'a->bool) q st Pr.
 618         (?r. (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr)) =
 619             (p LEADSTO q)(CONS st Pr)`),
 620    REPEAT GEN_TAC THEN
 621    EQ_TAC THEN
 622    REPEAT STRIP_TAC THENL
 623     [
 624      IMP_RES_TAC LEADSTO_thm2
 625     ;
 626      EXISTS_TAC (`p:'a->bool`) THEN
 627      ASM_REWRITE_TAC [ENSURES_thm1]
 628     ]);;
 629
 630
 631 (* Prove:
 632   !P Pr. (P LEADSTO P) (CONS st Pr)
 633 *)
 634 let LEADSTO_thm12 = prove_thm
 635   ("LEADSTO_thm12",
 636    (`!(p:'a->bool) st Pr. (p LEADSTO p) (CONS st Pr)`),
 637    REPEAT GEN_TAC THEN
 638    ONCE_REWRITE_TAC [SYM (SPEC_ALL LEADSTO_thm5)] THEN
 639    DISJ1_TAC THEN
 640    REWRITE_TAC [ENSURES_thm1]);;
 641
 642 (*
 643    Prove:
 644        (?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) = (p LEADSTO q)Pr
 645 *)
 646 let LEADSTO_thm13 = prove_thm
 647   ("LEADSTO_thm13",
 648    (`!(p:'a->bool) q st Pr.
 649         (?r. (p LEADSTO r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr))
 650       = (p LEADSTO q)(CONS st Pr)`),
 651    REPEAT GEN_TAC THEN
 652    EQ_TAC THEN
 653    REPEAT STRIP_TAC THENL
 654     [
 655      IMP_RES_TAC LEADSTO_thm1
 656     ;
 657      EXISTS_TAC (`p:'a->bool`) THEN
 658      ASM_REWRITE_TAC [LEADSTO_thm12]
 659     ]);;
 660
 661 (*
 662    Prove:
 663        (?r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr) =
 664        (?r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr)
 665 *)
 666 let LEADSTO_thm14 = prove_thm
 667   ("LEADSTO_thm14",
 668    (`!(p:'a->bool) q st Pr.
 669         (?r. (p LEADSTO r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr))
 670       =
 671         (?r. (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr))`),
 672    REPEAT GEN_TAC THEN
 673    REWRITE_TAC [LEADSTO_thm11; LEADSTO_thm13]);;
 674
 675 (*
 676    Prove:
 677     |- !p q Pr.
 678         (p ENSURES q)Pr \/
 679         (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 680         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))
 681       =
 682         (p LEADSTO q)Pr
 683 *)
 684 let LEADSTO_thm15 = prove_thm
 685   ("LEADSTO_thm15",
 686    (`!(p:'a->bool) q Pr.
 687        ((p ENSURES q) Pr \/
 688         (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 689         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))) =
 690            (p LEADSTO q)Pr`),
 691    REPEAT STRIP_TAC THEN
 692    EQ_TAC THEN
 693    REPEAT STRIP_TAC THENL
 694     [
 695      IMP_RES_TAC LEADSTO_thm0
 696     ;
 697      ACCEPT_TAC (MP (SPEC_ALL LEADSTO_thm2) (SPEC_ALL
 698       (ASSUME (`!r:'a->bool. (p ENSURES r)Pr /\ (r LEADSTO q)Pr`))))
 699     ;
 700      IMP_RES_TAC LEADSTO_thm3
 701     ;
 702      DISJ2_TAC THEN
 703      DISJ2_TAC THEN
 704      EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 705      REWRITE_TAC [LUB; IN] THEN
 706      BETA_TAC THEN
 707      CONJ_TAC THENL
 708       [
 709        ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 710       ;
 711        GEN_TAC THEN
 712        REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 713        DISCH_TAC THEN
 714        ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 715          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 716       ]
 717     ]);;
 718
 719 (*
 720    Prove:
 721     |- !p q Pr.
 722         (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 723         (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))
 724        =
 725         (p LEADSTO q)Pr
 726 *)
 727 let LEADSTO_thm16 = prove_thm
 728   ("LEADSTO_thm16",
 729    (`!(p:'a->bool) q Pr.
 730        ((!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr) \/
 731        (?P. (p = LUB P) /\ (!p. p In P ==> (p LEADSTO q)Pr))) =
 732            (p LEADSTO q)Pr`),
 733    REPEAT STRIP_TAC THEN
 734    EQ_TAC THEN
 735    REPEAT STRIP_TAC THENL
 736     [
 737      ACCEPT_TAC (MP (SPEC_ALL LEADSTO_thm2) (SPEC_ALL
 738       (ASSUME (`!r:'a->bool. (p ENSURES r)Pr /\ (r LEADSTO q)Pr`))))
 739     ;
 740      IMP_RES_TAC LEADSTO_thm3
 741     ;
 742      DISJ2_TAC THEN
 743      EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
 744      REWRITE_TAC [LUB; IN] THEN
 745      BETA_TAC THEN
 746      CONJ_TAC THENL
 747       [
 748        ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
 749       ;
 750        GEN_TAC THEN
 751        REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
 752        DISCH_TAC THEN
 753        ACCEPT_TAC (REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)]
 754          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))
 755       ]
 756     ]);;
 757
 758
 759 (*
 760   Finally prove one of the used LEADSTO induction principles in CM88:
 761
 762 |- !X p q Pr.
 763
 764     (!p q.
 765
 766       ((p ENSURES q)Pr ==> X p q Pr)
 767
 768      /\
 769
 770       (!r.
 771         (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 772         (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 773
 774            ==> (p LEADSTO q)Pr ==> X p q Pr)
 775
 776      /\
 777
 778       (!P.
 779         (!p. p In P ==> (p LEADSTO q)Pr) /\
 780         (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
 781
 782            ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
 783
 784     ==> (p LEADSTO q)Pr ==> X p q Pr
 785
 786 *)
 787
 788 let STRUCT_lemma0 = TAC_PROOF
 789   (([],
 790    (` (!p:'a->bool. p In P ==>
 791           (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr))
 792        =
 793         ((!p. p In P ==> (p LEADSTO q)Pr) /\
 794          (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr))`)),
 795    EQ_TAC THEN
 796    REPEAT STRIP_TAC THEN
 797    RES_TAC);;
 798
 799
 800 let STRUCT_lemma00 = TAC_PROOF
 801   (([],
 802    (`!X Pr.
 803       (!(p:'a->bool) q.
 804         ((p ENSURES q)Pr ==> X p q Pr) /\
 805         (!r.
 806           (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 807           (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 808              ==> (p LEADSTO q)Pr ==> X p q Pr) /\
 809         (!P.
 810           (!p. p In P ==> (p LEADSTO q)Pr) /\
 811           (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
 812              ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
 813      =
 814       (!p q.
 815          ((p ENSURES q)Pr ==>
 816           (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)) /\
 817          (!r.
 818            ((p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr)) /\
 819            (r LEADSTO q)Pr /\
 820            ((r LEADSTO q)Pr ==> X r q Pr) ==>
 821            (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)) /\
 822          (!P.
 823            (p = LUB P) /\
 824            (!p'.
 825              p' In P ==> (p' LEADSTO q)Pr /\ ((p' LEADSTO q)Pr ==> X p' q Pr))
 826                 ==> (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)))`)),
 827    REPEAT GEN_TAC THEN
 828    EQ_TAC THEN
 829    REPEAT STRIP_TAC THENL
 830     [
 831      IMP_RES_TAC LEADSTO_thm0
 832     ;
 833      RES_TAC
 834     ;
 835      IMP_RES_TAC LEADSTO_thm1
 836     ;
 837      RES_TAC
 838     ;
 839      IMP_RES_TAC STRUCT_lemma0 THEN
 840      IMP_RES_TAC LEADSTO_thm3a THEN
 841      RES_TAC THEN
 842      ASM_REWRITE_TAC []
 843     ;
 844      IMP_RES_TAC STRUCT_lemma0 THEN
 845      IMP_RES_TAC LEADSTO_thm3a THEN
 846      RES_TAC THEN
 847      ASM_REWRITE_TAC []
 848     ;
 849      RES_TAC
 850     ;
 851      RES_TAC
 852     ;
 853      ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL STRUCT_lemma0)] (CONJ
 854       (ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr`))
 855       (ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr ==> X p q Pr`)))) THEN
 856      ACCEPT_TAC (REWRITE_RULE [ASSUME (`((LUB P) LEADSTO (q:'a->bool))Pr`)]
 857       (SPEC (`LUB (P:('a->bool)->bool)`) (GEN_ALL (REWRITE_RULE
 858         [ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr /\
 859                                      ((p LEADSTO q)Pr ==> X p q Pr)`)]
 860           (SPEC_ALL (CONJUNCT2 (CONJUNCT2 (SPEC_ALL (ASSUME
 861             (`!(p:'a->bool) q.
 862                ((p ENSURES q)Pr ==>
 863                (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)) /\
 864                (!r.
 865                  ((p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr)) /\
 866                   (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr) ==>
 867                      (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)) /\
 868                (!P. (p = LUB P) /\
 869                   (!p'. p' In P ==>
 870                      (p' LEADSTO q)Pr /\ ((p' LEADSTO q)Pr ==> X p' q Pr)) ==>
 871               (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr))`))))))))))
 872     ]);;
 873
 874 (*
 875   The induction theorem:
 876 *)
 877 let LEADSTO_thm17 = prove_thm
 878   ("LEADSTO_thm17",
 879    (`!X (p:'a->bool) q Pr.
 880       (!(p:'a->bool) q.
 881         ((p ENSURES q)Pr ==> X p q Pr) /\
 882         (!r. (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 883              (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 884             ==> ((p LEADSTO q)Pr ==> X p q Pr)) /\
 885         (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\
 886              (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
 887             ==> (((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr)))
 888      ==> ((p LEADSTO q)Pr ==> X p q Pr)`),
 889    REPEAT GEN_TAC THEN
 890    REPEAT DISCH_TAC THEN
 891    ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL STRUCT_lemma00)] (BETA_RULE (SPEC
 892      (`\(p:'a->bool) q Pr.
 893            (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)`)
 894        (REWRITE_RULE [LEADSTO;LeadstoRel]
 895           (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))))) THEN
 896    RES_TAC);;
 897
 898 (*
 899   A derived theorem for an induction tactic
 900 *)
 901 let LEADSTO_thm18 = prove_thm
 902   ("LEADSTO_thm18",
 903    (`!X.
 904       ((!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
 905        (!p r q Pr. (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 906                  (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 907             ==> ((p LEADSTO q)Pr ==> X p q Pr)) /\
 908        (!(p:'a->bool) P q Pr. (!p. p In P ==> (p LEADSTO q)Pr) /\
 909                   (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
 910             ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
 911      ==> (!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)`),
 912    REPEAT STRIP_TAC THEN
 913    ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL STRUCT_lemma00)]
 914     (BETA_RULE (SPEC
 915      (`\ (p:'a->bool) q Pr. (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)`)
 916        (REWRITE_RULE [LEADSTO;LeadstoRel]
 917           (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))))) THEN
 918    ACCEPT_TAC (REWRITE_RULE
 919     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
 920      ASSUME (`!(p:'a->bool) r q Pr.
 921         (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 922         (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 923             ==> (p LEADSTO q)Pr ==> X p q Pr`);
 924      ASSUME (`!(p:'a->bool) P (q:'a->bool) Pr.
 925         (!p. p In P ==> (p LEADSTO q)Pr) /\
 926         (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
 927             ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr`);
 928      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)] (ASSUME
 929       (`(!(p:'a->bool) q.
 930          ((p ENSURES q)Pr ==> X p q Pr) /\
 931          (!r.
 932            (p LEADSTO r)Pr /\ ((p LEADSTO r)Pr ==> X p r Pr) /\
 933            (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
 934              ==> (p LEADSTO q)Pr ==> X p q Pr) /\
 935          (!P.
 936            (!p'. p' In P ==> (p' LEADSTO q)Pr) /\
 937            (!p'. p' In P ==> (p' LEADSTO q)Pr ==> X p' q Pr)
 938              ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
 939          ==> (p LEADSTO q)Pr /\ ((p LEADSTO q)Pr ==> X p q Pr)`))));;
 940
 941
 942 (*
 943   Now prove another LEADSTO induction principle:
 944 *)
 945 let STRUCT_lemma1 = TAC_PROOF
 946   (([],
 947    (`(!p:'a->bool. p In P ==> (p LEADSTO q)Pr /\ X p q Pr)
 948     =
 949     ((!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr))`)),
 950    EQ_TAC THEN
 951    REPEAT STRIP_TAC THEN
 952    RES_TAC);;
 953
 954
 955 let STRUCT_lemma01 = TAC_PROOF
 956   (([],
 957    (`!X Pr.
 958       (!(p:'a->bool) q.
 959          ((p ENSURES q)Pr ==> (p LEADSTO q)Pr /\ X p q Pr) /\
 960          (!r. ((p LEADSTO r)Pr /\ X p r Pr) /\ (r LEADSTO q)Pr /\ X r q Pr
 961               ==> (p LEADSTO q)Pr /\ X p q Pr) /\
 962          (!P. (p = LUB P) /\ (!p'. p' In P ==> (p' LEADSTO q)Pr /\ X p' q Pr)
 963               ==> (p LEADSTO q)Pr /\ X p q Pr))
 964      =
 965       (!p q.
 966         ((p ENSURES q)Pr ==> X p q Pr) /\
 967         (!r. (p LEADSTO r)Pr /\ X p r Pr /\ (r LEADSTO q)Pr /\ X r q Pr
 968               ==> (p LEADSTO q)Pr ==> X p q Pr) /\
 969         (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
 970                ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))`)),
 971    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
 972     [
 973      RES_TAC
 974     ;
 975      RES_TAC
 976     ;
 977      ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL STRUCT_lemma1)] (CONJ
 978       (ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr`))
 979       (ASSUME (`!p. p In P
 980          ==> (X:('a->bool)->('a->bool)->('a->'a)list->bool) p q Pr`)))) THEN
 981      RES_TAC THEN
 982      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
 983       (`!p. (p = LUB P) ==> (X:('a->bool)->('a->bool)->('a->'a)list->bool)p q Pr`))))
 984     ;
 985      IMP_RES_TAC LEADSTO_thm0
 986     ;
 987      RES_TAC
 988     ;
 989      IMP_RES_TAC LEADSTO_thm1
 990     ;
 991      IMP_RES_TAC LEADSTO_thm1 THEN
 992      RES_TAC
 993     ;
 994      IMP_RES_TAC STRUCT_lemma1 THEN
 995      IMP_RES_TAC LEADSTO_thm3
 996     ;
 997      IMP_RES_TAC STRUCT_lemma1 THEN
 998      IMP_RES_TAC LEADSTO_thm3a THEN
 999      RES_TAC THEN
1000      ASM_REWRITE_TAC []
1001     ]);;
1002
1003 (*
1004   The induction theorem:
1005 *)
1006 let LEADSTO_thm19 = prove_thm
1007   ("LEADSTO_thm19",
1008    (`!X (p:'a->bool) q Pr.
1009       (!(p:'a->bool) q.
1010         ((p ENSURES q)Pr ==> X p q Pr) /\
1011         (!r. (p LEADSTO r)Pr /\ (X p r Pr) /\ (r LEADSTO q)Pr /\ (X r q Pr)
1012             ==> ((p LEADSTO q)Pr ==> X p q Pr)) /\
1013         (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1014             ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
1015      ==> ((p LEADSTO q)Pr ==> X p q Pr)`),
1016    REPEAT STRIP_TAC THEN
1017    ASSUME_TAC (REWRITE_RULE [STRUCT_lemma01] (BETA_RULE
1018     (SPEC (`\(p:'a->bool) q Pr. (p LEADSTO q)Pr /\ (X p q Pr)`)
1019       (REWRITE_RULE [LEADSTO;LeadstoRel]
1020         (ASSUME (`((p:'a->bool) LEADSTO q)Pr`)))))) THEN
1021    RES_TAC);;
1022
1023 (*
1024   The derived theorem for the induction tactic
1025 *)
1026 let LEADSTO_thm20 = prove_thm
1027   ("LEADSTO_thm20",
1028    (`!X.
1029      ((!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
1030       (!p r q Pr. (p LEADSTO r)Pr /\ X p r Pr /\ (r LEADSTO q)Pr /\ X r q Pr
1031             ==> ((p LEADSTO q)Pr ==> X p q Pr)) /\
1032       (!(p:'a->bool) P q Pr.
1033          (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1034             ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
1035      ==> (!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)`),
1036    REPEAT STRIP_TAC THEN
1037    ACCEPT_TAC (REWRITE_RULE
1038     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
1039      ASSUME (`!(p:'a->bool) r q Pr.
1040                 (p LEADSTO r)Pr /\ X p r Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==>
1041                    (p LEADSTO q)Pr ==> X p q Pr`);
1042      ASSUME (`!(p:'a->bool) P q Pr.
1043         (!p:'a->bool.
1044            p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
1045                    ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr`);
1046      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)]
1047       (REWRITE_RULE [STRUCT_lemma01](BETA_RULE (SPEC
1048         (`\(p:'a->bool) q Pr. (p LEADSTO q)Pr /\ (X p q Pr)`)
1049           (REWRITE_RULE [LEADSTO;LeadstoRel]
1050              (ASSUME (`((p:'a->bool) LEADSTO q)Pr`))))))));;
1051
1052 (*
1053   Now prove a third LEADSTO induction principle:
1054 |- !X p q Pr.
1055     (!p q.
1056        ((p ENSURES q)Pr ==> X p q Pr)
1057      /\
1058        (!r. (X p r Pr) /\ (X r q Pr) ==> X p q Pr)
1059      /\
1060        (!P. (!i. X(P i)q Pr) ==> X(( ?* )  P)q Pr))
1061      ==> (p LEADSTO q)Pr ==> X p q Pr
1062 *)
1063 let LEADSTO_thm21 = prove_thm
1064   ("LEADSTO_thm21",
1065    (`!X (p:'a->bool) q Pr.
1066       (!(p:'a->bool) q.
1067         ((p ENSURES q)Pr ==> X p q Pr) /\
1068         (!r. (X p r Pr) /\ (X r q Pr) ==> X p q Pr) /\
1069         (!P. (p = LUB P) /\ (!p. p In P ==> X p q Pr) ==> X p q Pr))
1070      ==> ((p LEADSTO q)Pr ==> X p q Pr)`),
1071    REPEAT STRIP_TAC THEN
1072    ASSUME_TAC (BETA_RULE (SPEC
1073      (`\(p:'a->bool) (q:'a->bool) (Pr:('a->'a)list). X p q Pr:bool`)
1074       (REWRITE_RULE [LEADSTO;LeadstoRel]
1075         (ASSUME (`((p:'a->bool) LEADSTO q)Pr`))))) THEN
1076    RES_TAC);;
1077
1078 (*
1079   The theorem derived for an induction tactic
1080 *)
1081 let LEADSTO_thm22 = prove_thm
1082   ("LEADSTO_thm22",
1083    (`!X.
1084       ((!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
1085        (!p r q Pr. (X p r Pr) /\ (X r q Pr) ==> (X p q Pr)) /\
1086        (!p P q Pr. (p = LUB P) /\ (!p. p In P ==> X p q Pr) ==> X p q Pr))
1087      ==> (!p q Pr. (p LEADSTO q)Pr ==> X p q Pr)`),
1088    REPEAT STRIP_TAC THEN
1089    ACCEPT_TAC (REWRITE_RULE
1090     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
1091      ASSUME (`!(p:'a->bool) (r:'a->bool) q (Pr:('a->'a)list).
1092                 X p r Pr /\ X r q Pr ==> X p q Pr`);
1093      ASSUME (`!(p:'a->bool) P (q:'a->bool) (Pr:('a->'a)list).
1094                (p = LUB P) /\ (!p. p In P ==> X p q Pr) ==> X p q Pr`);
1095      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)]
1096      (REWRITE_RULE [SYM (SPEC_ALL CONJ_ASSOC)] (BETA_RULE (SPEC
1097        (`\(p:'a->bool) (q:'a->bool) (Pr:('a->'a)list). X p q Pr:bool`)
1098          (REWRITE_RULE [LEADSTO;LeadstoRel]
1099            (ASSUME (`((p:'a->bool) LEADSTO q)Pr`))))))));;
1100
1101 (*
1102   yet another LEADSTO induction principle:
1103 *)
1104 let LEADSTO_thm23_lemma00 = TAC_PROOF
1105   (([],
1106    (`!X Pr.
1107       ((!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)) =
1108        (!p:'a->bool. p In P ==> (p LEADSTO q)Pr /\ X p q Pr)`)),
1109    REPEAT GEN_TAC THEN
1110    EQ_TAC THEN
1111    REPEAT STRIP_TAC THEN
1112    RES_TAC);;
1113
1114 let LEADSTO_thm23_lemma01 = TAC_PROOF
1115   (([],
1116    (`!X Pr.
1117       (!(p:'a->bool) q.
1118          ((p ENSURES q)Pr ==> (p LEADSTO q)Pr /\ X p q Pr) /\
1119          (!r.
1120            ((p LEADSTO r)Pr /\ X p r Pr) /\ (r LEADSTO q)Pr /\ X r q Pr
1121                           ==> (p LEADSTO q)Pr /\ X p q Pr) /\
1122          (!P. (p = LUB P) /\
1123               (!p'. p' In P ==> (p' LEADSTO q)Pr /\ X p' q Pr)
1124                           ==> (p LEADSTO q)Pr /\ X p q Pr))
1125       =
1126        (!(p:'a->bool) q.
1127         ((p ENSURES q)Pr ==> X p q Pr) /\
1128         (!r.
1129           (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
1130                          ==> X p q Pr) /\
1131         (!P. (p = LUB P) /\
1132              (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1133                          ==> X p q Pr))`)),
1134    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL
1135     [
1136      RES_TAC
1137     ;
1138      RES_TAC
1139     ;
1140      ASSUME_TAC (REWRITE_RULE [LEADSTO_thm23_lemma00] (CONJ
1141       (ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr`))
1142       (ASSUME (`!p. p In P
1143                  ==> (X:('a->bool)->('a->bool)->('a->'a)list->bool) p q Pr`)))) THEN
1144      RES_TAC
1145     ;
1146      IMP_RES_TAC LEADSTO_thm0
1147     ;
1148      RES_TAC
1149     ;
1150      IMP_RES_TAC LEADSTO_thm1
1151     ;
1152      RES_TAC
1153     ;
1154      STRIP_ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm23_lemma00)]
1155       (ASSUME (`!p':'a->bool. p' In P ==> (p' LEADSTO q)Pr /\ X p' q Pr`))) THEN
1156      IMP_RES_TAC LEADSTO_thm3a THEN
1157      ASM_REWRITE_TAC []
1158     ;
1159      STRIP_ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm23_lemma00)]
1160       (ASSUME (`!p':'a->bool. p' In P ==> (p' LEADSTO q)Pr /\ X p' q Pr`))) THEN
1161      RES_TAC
1162     ]);;
1163
1164 let LEADSTO_thm23 = prove_thm
1165   ("LEADSTO_thm23",
1166    (`!X Pr.
1167       (!(p:'a->bool) q.
1168        ((p ENSURES q)Pr ==> X p q Pr) /\
1169        (!r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
1170                         ==> X p q Pr) /\
1171        (!P. (p = LUB P) /\
1172             (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1173                         ==> X p q Pr))
1174      ==> (!p q. (p LEADSTO q) Pr ==> X p q Pr)`),
1175    REPEAT STRIP_TAC THEN
1176    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm23_lemma01] (BETA_RULE (SPEC
1177      (`\(p:'a->bool) q Pr. (p LEADSTO q)Pr /\ (X p q Pr)`)
1178        (REWRITE_RULE [LEADSTO;LeadstoRel]
1179          (ASSUME (`((p:'a->bool) LEADSTO q) Pr`)))))) THEN
1180    RES_TAC);;
1181
1182 let LEADSTO_thm24_lemma01 = TAC_PROOF
1183   (([],
1184    (`!X Pr.
1185      (!(p:'a->bool) q.
1186        ((p ENSURES q)Pr ==> X p q Pr) /\
1187        (!r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
1188                         ==> X p q Pr) /\
1189        (!P. (p = LUB P) /\
1190             (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1191                         ==> X p q Pr))
1192      =
1193      (!(p:'a->bool) q.
1194         ((p ENSURES q)Pr ==> X p q Pr) /\
1195         (!r.
1196           (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==>
1197           X p q Pr) /\
1198         (!P.
1199           (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
1200           X(LUB P)q Pr))`)),
1201    REPEAT GEN_TAC THEN
1202    EQ_TAC THEN
1203    REPEAT STRIP_TAC THEN
1204    RES_TAC THENL
1205     [
1206      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
1207      (`!p. (p = LUB P) ==> (X:('a->bool)->('a->bool)->('a->'a)list->bool) p q Pr`))))
1208     ;
1209      ASM_REWRITE_TAC []
1210     ]);;
1211
1212 let LEADSTO_thm24 = prove_thm
1213   ("LEADSTO_thm24",
1214    (`!X Pr.
1215       (!(p:'a->bool) q.
1216        ((p ENSURES q)Pr ==> X p q Pr) /\
1217        (!r. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
1218                         ==> X p q Pr) /\
1219        (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
1220                         ==> X (LUB P) q Pr))
1221      ==> (!p q. (p LEADSTO q) Pr ==> X p q Pr)`),
1222    REPEAT STRIP_TAC THEN
1223    ACCEPT_TAC (UNDISCH (SPEC_ALL (UNDISCH (REWRITE_RULE [LEADSTO_thm24_lemma01]
1224     (SPEC_ALL LEADSTO_thm23))))));;
1225
1226 (* Prove:
1227   !P Q st Pr. (!s. P s ==> Q s) ==> (P LEADSTO Q) (CONS st Pr)
1228 *)
1229 let LEADSTO_thm25 = prove_thm
1230   ("LEADSTO_thm25",
1231    (`!(p:'a->bool) q st Pr. (!s. p s ==> q s) ==> (p LEADSTO q) (CONS st Pr)`),
1232    REPEAT STRIP_TAC THEN
1233    STRIP_ASSUME_TAC
1234      (MP (SPECL [(`p:'a->bool`); (`q:'a->bool`); (`CONS (st:'a->'a) Pr`)] LEADSTO_thm0)
1235          (MP (SPECL [(`p:'a->bool`); (`q:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
1236                      ENSURES_cor1) (ASSUME (`!s:'a. p s ==> q s`)))));;
1237
1238
1239 (* Prove:
1240   |- !p q q' st Pr.
1241          (p LEADSTO q)(CONS st Pr) ==> (p LEADSTO (q \/* q'))(CONS st Pr)
1242 *)
1243 let LEADSTO_thm26 = prove_thm
1244   ("LEADSTO_thm26",
1245    (`!(p:'a->bool) q q' st Pr.
1246        (p LEADSTO q)(CONS st Pr) ==> (p LEADSTO (q \/* q'))(CONS st Pr)`),
1247    REPEAT GEN_TAC THEN
1248    DISCH_TAC THEN
1249    ASSUME_TAC (SPECL [(`q:'a->bool`); (`q':'a->bool`)] IMPLY_WEAK_lemma_b) THEN
1250    ASSUME_TAC (UNDISCH_ALL (SPECL
1251      [(`q:'a->bool`); (`(q:'a->bool) \/* q'`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
1252       LEADSTO_thm25)) THEN
1253    IMP_RES_TAC (SPECL
1254      [(`p:'a->bool`); (`q:'a->bool`); (`(q:'a->bool) \/* q'`); (`CONS (st:'a->'a) Pr`)]
1255      LEADSTO_thm1));;
1256
1257
1258 (* Prove:
1259    |- !p q p' q' st Pr.
1260         (p LEADSTO q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) ==>
1261            ((p \/* p') LEADSTO (q \/* q'))(CONS st Pr)
1262 *)
1263 let LEADSTO_thm27 = prove_thm
1264   ("LEADSTO_thm27",
1265    (`!(p:'a->bool) q p' q' st Pr.
1266       (p LEADSTO q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr)
1267           ==> ((p \/* p') LEADSTO (q \/* q'))(CONS st Pr)`),
1268    REPEAT STRIP_TAC THEN
1269    ASSUME_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO_thm26)) THEN
1270    ASSUME_TAC (UNDISCH_ALL (SPECL
1271     [(`p':'a->bool`); (`q':'a->bool`); (`q:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
1272      LEADSTO_thm26)) THEN
1273    ASSUME_TAC (ONCE_REWRITE_RULE [OR_COMM_lemma]
1274     (ASSUME (`((p':'a->bool) LEADSTO (q' \/* q))(CONS st Pr)`))) THEN
1275    IMP_RES_TAC (SPECL
1276     [(`p:'a->bool`); (`p':'a->bool`); (`(q:'a->bool) \/* q'`); (`CONS (st:'a->'a) Pr`)]
1277      LEADSTO_thm4));;
1278
1279
1280 (* Prove:
1281    |- !p q b r st Pr.
1282       (p LEADSTO (q \/* b))(CONS st Pr) /\ (b LEADSTO r)(CONS st Pr) ==>
1283          (p LEADSTO (q \/* r))(CONS st Pr)
1284 *)
1285 let LEADSTO_thm28 = prove_thm
1286   ("LEADSTO_thm28",
1287    (`!(p:'a->bool) q b r st Pr.
1288        (p LEADSTO (q \/* b))(CONS st Pr) /\ (b LEADSTO r)(CONS st Pr)
1289            ==> (p LEADSTO (q \/* r))(CONS st Pr)`),
1290    REPEAT GEN_TAC THEN
1291    STRIP_TAC THEN
1292    ASSUME_TAC (SPEC_ALL (SPEC (`q:'a->bool`) LEADSTO_thm12)) THEN
1293    ASSUME_TAC (MP (SPECL
1294     [(`b:'a->bool`); (`r:'a->bool`); (`q:'a->bool`); (`q:'a->bool`);
1295      (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm27) (CONJ
1296        (ASSUME (`((b:'a->bool) LEADSTO r)(CONS st Pr)`))
1297          (ASSUME (`((q:'a->bool) LEADSTO q)(CONS st Pr)`)))) THEN
1298    ACCEPT_TAC (MP (SPECL [(`p:'a->bool`); (`(q:'a->bool) \/* b`);
1299     (`(q:'a->bool) \/* r`); (`CONS (st:'a->'a) Pr`)] LEADSTO_thm1)
1300        (CONJ (ASSUME (`((p:'a->bool) LEADSTO (q \/* b))(CONS st Pr)`))
1301          (ONCE_REWRITE_RULE [OR_COMM_lemma]
1302            (ASSUME (`(((b:'a->bool) \/* q) LEADSTO (r \/* q))(CONS st Pr)`))))));;
1303
1304 (* Prove:
1305    !p q r b Pr.
1306       (p LEADSTO q)Pr /\ (r UNLESS b)Pr
1307           ==> ((p  /\*  r) LEADSTO ((q  /\*  r) \/* b))Pr
1308 *)
1309 let LEADSTO_thm29_lemma00 =
1310   (SPEC (`CONS (st:'a->'a) Pr`) (GEN (`Pr:('a->'a)list`) (BETA_RULE (SPEC_ALL (SPEC
1311    (`\(p:'a->bool) q Pr.
1312         (r UNLESS b) Pr ==> ((p  /\*  r) LEADSTO ((q  /\*  r) \/* b)) Pr`)
1313    LEADSTO_thm17)))));;
1314
1315 let LEADSTO_thm29_lemma05_1 = TAC_PROOF
1316   (([],
1317    (`(!p'':'a->bool. p'' In P ==> (p'' LEADSTO q')(CONS st Pr)) ==>
1318        (!p''. p'' In P ==>
1319         (p'' LEADSTO q')(CONS st Pr) ==> (r UNLESS b)(CONS st Pr) ==>
1320         ((p''  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) ==>
1321        (!p''. p'' In P ==> (r UNLESS b)(CONS st Pr) ==>
1322         ((p''  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))`)),
1323    REPEAT STRIP_TAC THEN
1324    RES_TAC THEN
1325    RES_TAC);;
1326
1327 let LEADSTO_thm29_lemma05_2 = TAC_PROOF
1328   (([],
1329    (`!(P:('a->bool)->bool) r q st Pr.
1330     (!p. p In P ==> ((p  /\*  r) LEADSTO q)(CONS st Pr)) ==>
1331     (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) ==>
1332     (((LUB P)  /\*  r) LEADSTO q)(CONS st Pr)`)),
1333    REPEAT STRIP_TAC THEN
1334    IMP_RES_TAC LEADSTO_thm3a THEN
1335    ASSUME_TAC (SPECL
1336     [(`LUB (P:('a->bool)->bool)`); (`r:'a->bool`)] SYM_AND_IMPLY_WEAK_lemma) THEN
1337    ASSUME_TAC (UNDISCH (SPEC_ALL (SPECL
1338     [(`(LUB P)  /\*  (r:'a->bool)`); (`(LUB P):'a->bool`)] ENSURES_cor1))) THEN
1339    IMP_RES_TAC LEADSTO_thm0 THEN
1340    IMP_RES_TAC LEADSTO_thm1);;
1341
1342 let LEADSTO_thm29_lemma05_3 = TAC_PROOF
1343   (([],
1344    (`!(p:'a->bool) P r.
1345       p In (\p''. ?p'. p' In P /\ (p'' = p'  /\*  r))
1346      =
1347       (?p'. p' In P /\ (p = p'  /\*  r))`)),
1348    REWRITE_TAC [IN] THEN
1349    BETA_TAC THEN
1350    REWRITE_TAC []);;
1351
1352 let LEADSTO_thm29_lemma05_4 = TAC_PROOF
1353   (([],
1354    (`!s:'a.
1355       ((LUB P)  /\*  r)s =
1356       (LUB(\p. ?p'. p' In P /\ (p = p'  /\*  r)))s`)),
1357    REPEAT GEN_TAC THEN
1358    REWRITE_TAC [LUB; AND_def ] THEN
1359    BETA_TAC THEN
1360    EQ_TAC THEN
1361    REPEAT STRIP_TAC THENL
1362     [
1363      EXISTS_TAC (`\s:'a. p s /\ r s`) THEN
1364      BETA_TAC THEN
1365      ASM_REWRITE_TAC [] THEN
1366      EXISTS_TAC (`p:'a->bool`) THEN
1367      ASM_REWRITE_TAC [IN]
1368     ;
1369      EXISTS_TAC (`p':'a->bool`) THEN
1370      REWRITE_TAC [REWRITE_RULE [IN] (ASSUME (`(p':'a->bool) In P`))] THEN
1371      STRIP_ASSUME_TAC (BETA_RULE (SUBS [ASSUME (`p = (\s:'a. p' s /\ r s)`)]
1372                                        (ASSUME (`(p:'a->bool) s`))))
1373     ;
1374      STRIP_ASSUME_TAC (BETA_RULE (SUBS [ASSUME (`p = (\s:'a. p' s /\ r s)`)]
1375                                        (ASSUME (`(p:'a->bool) s`))))
1376     ]);;
1377
1378 let LEADSTO_thm29_lemma05_5 = TAC_PROOF
1379   (([],
1380    (`!(P:('a->bool)->bool) r q' b st Pr.
1381     (!p''. p'' In P ==> ((p''  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))
1382       ==>
1383         (!p. (?p'. p' In P /\ (p = p'  /\*  r)) ==>
1384                  (p LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))`)),
1385    REPEAT STRIP_TAC THEN
1386    RES_TAC THEN
1387    ASM_REWRITE_TAC []);;
1388
1389 let LEADSTO_thm29_lemma05_6 = TAC_PROOF
1390   (([],
1391    (`!(P:('a->bool)->bool) r q' b st Pr.
1392        (!p''.
1393         p'' In P ==>
1394         ((p''  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))
1395            ==> ((((LUB P)  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))`)),
1396    REPEAT STRIP_TAC THEN
1397    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm29_lemma05_3] (SPECL
1398      [(`\p:'a->bool. ?p'. p' In P /\ (p = (p'  /\*  r))`);
1399       (`(q'  /\*  r) \/* (b:'a->bool)`); (`CONS (st:'a->'a) Pr`)]
1400      LEADSTO_thm3a)) THEN
1401    ASSUME_TAC (REWRITE_RULE [UNDISCH (SPEC_ALL LEADSTO_thm29_lemma05_5)]
1402     (ASSUME (`(!p:'a->bool. (?p'. p' In P /\ (p = p'  /\*  r)) ==>
1403        (p LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) ==>
1404        ((LUB(\p. ?p'. p' In P /\ (p = p'  /\*  r))) LEADSTO ((q'  /\*  r) \/* b))
1405         (CONS st Pr)`))) THEN
1406    ASM_REWRITE_TAC [REWRITE_RULE [ETA_AX] (MK_ABS LEADSTO_thm29_lemma05_4)]);;
1407
1408
1409 let LEADSTO_thm29_lemma05 = TAC_PROOF
1410   (([],
1411    (`!(p':'a->bool) q' r b st Pr.
1412      ((p' ENSURES q')(CONS st Pr) ==>
1413       (r UNLESS b)(CONS st Pr) ==>
1414       ((p'  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) /\
1415      (!r'.
1416        (p' LEADSTO r')(CONS st Pr) /\
1417        ((p' LEADSTO r')(CONS st Pr) ==>
1418         (r UNLESS b)(CONS st Pr) ==>
1419         ((p'  /\*  r) LEADSTO ((r'  /\*  r) \/* b))(CONS st Pr)) /\
1420        (r' LEADSTO q')(CONS st Pr) /\
1421        ((r' LEADSTO q')(CONS st Pr) ==>
1422         (r UNLESS b)(CONS st Pr) ==>
1423         ((r'  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) ==>
1424        (p' LEADSTO q')(CONS st Pr) ==>
1425        (r UNLESS b)(CONS st Pr) ==>
1426        ((p'  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) /\
1427      (!P.
1428        (!p''. p'' In P ==> (p'' LEADSTO q')(CONS st Pr)) /\
1429        (!p''.
1430          p'' In P ==>
1431          (p'' LEADSTO q')(CONS st Pr) ==>
1432          (r UNLESS b)(CONS st Pr) ==>
1433          ((p''  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)) ==>
1434        ((LUB P) LEADSTO q')(CONS st Pr) ==>
1435        (r UNLESS b)(CONS st Pr) ==>
1436        (((LUB P)  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr))`)),
1437    REPEAT GEN_TAC THEN
1438    REPEAT CONJ_TAC THENL
1439      [
1440       REPEAT STRIP_TAC THEN
1441       IMP_RES_TAC ENSURES_thm4 THEN
1442       ASSUME_TAC (SPECL
1443         [(`p':'a->bool`); (`q':'a->bool`); (`b:'a->bool`); (`r:'a->bool`)]
1444          IMPLY_WEAK_lemma6) THEN
1445       ASSUME_TAC (MP (SPECL
1446         [(`(r:'a->bool)  /\*  p'`);
1447          (`((r:'a->bool)  /\*  q') \/* ((p'  /\*  b) \/* (b  /\*  q'))`);
1448          (`((q':'a->bool)  /\*  r) \/* b`); (`(CONS st Pr):('a->'a)list`)] ENSURES_thm2)
1449           (CONJ (REWRITE_RULE [OR_ASSOC_lemma]
1450             (ASSUME (`(((r:'a->bool)  /\*  p') ENSURES
1451                   (((r  /\*  q') \/* (p'  /\*  b)) \/* (b  /\*  q')))(CONS st Pr)`)))
1452             (ASSUME (`!s:'a. ((r  /\*  q') \/* ((p'  /\*  b) \/* (b  /\*  q')))s ==>
1453                           ((q'  /\*  r) \/* b)s`)))) THEN
1454       ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
1455       ONCE_REWRITE_TAC [AND_COMM_OR_lemma] THEN
1456       IMP_RES_TAC (SPECL [(`(r:'a->bool)  /\*  p'`); (`((q':'a->bool)  /\*  r) \/* b`);
1457                           (`(CONS st Pr):('a->'a)list`)] LEADSTO_thm0)
1458      ;
1459       REPEAT STRIP_TAC THEN
1460       ASSUME_TAC (MP (MP (ASSUME (`((p':'a->bool) LEADSTO r')(CONS st Pr) ==>
1461          (r UNLESS b)(CONS st Pr)
1462              ==> ((p'  /\*  r) LEADSTO ((r'  /\*  r) \/* b))(CONS st Pr)`))
1463        (ASSUME (`((p':'a->bool) LEADSTO r')(CONS st Pr)`)))
1464        (ASSUME (`((r:'a->bool) UNLESS b)(CONS st Pr)`))) THEN
1465       ASSUME_TAC (MP (MP (ASSUME (`((r':'a->bool) LEADSTO q')(CONS st Pr) ==>
1466          (r UNLESS b)(CONS st Pr)
1467              ==> ((r'  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)`))
1468        (ASSUME (`((r':'a->bool) LEADSTO q')(CONS st Pr)`)))
1469        (ASSUME (`((r:'a->bool) UNLESS b)(CONS st Pr)`))) THEN
1470       ACCEPT_TAC (REWRITE_RULE [OR_ASSOC_lemma; OR_OR_lemma]
1471        (ONCE_REWRITE_RULE [OR_COMM_lemma] (MP (SPECL
1472         [(`(p':'a->bool)  /\*  r`); (`b:'a->bool`); (`(r':'a->bool)  /\*  r`);
1473          (`((q':'a->bool)  /\*  r) \/* b`); (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm28)
1474          (CONJ (ONCE_REWRITE_RULE [OR_COMM_lemma]
1475           (ASSUME
1476              (`(((p':'a->bool)  /\*  r) LEADSTO ((r'  /\*  r) \/* b))(CONS st Pr)`)))
1477           (ASSUME
1478            (`(((r':'a->bool)  /\*  r) LEADSTO ((q'  /\*  r) \/* b))(CONS st Pr)`))))))
1479      ;
1480       REPEAT STRIP_TAC THEN
1481       ASSUME_TAC (REWRITE_RULE [ASSUME (`((r:'a->bool) UNLESS b)(CONS st Pr)`)]
1482        (UNDISCH_ALL LEADSTO_thm29_lemma05_1)) THEN
1483       IMP_RES_TAC LEADSTO_thm29_lemma05_6
1484      ]);;
1485
1486 let LEADSTO_thm29_lemma06 =
1487    GEN_ALL (MP (SPEC_ALL LEADSTO_thm29_lemma00)
1488       (GEN (`p':'a->bool`) (GEN (`q':'a->bool`) (SPEC_ALL LEADSTO_thm29_lemma05))));;
1489
1490 let LEADSTO_thm29 = prove_thm
1491   ("LEADSTO_thm29",
1492    (`!(p:'a->bool) q r b st Pr.
1493     (p LEADSTO q)(CONS st Pr) /\ (r UNLESS b)(CONS st Pr)
1494       ==> ((p  /\*  r) LEADSTO ((q  /\*  r) \/* b))(CONS st Pr)`),
1495    REPEAT STRIP_TAC THEN
1496    REWRITE_TAC [UNDISCH_ALL (SPEC_ALL LEADSTO_thm29_lemma06)]);;
1497
1498 (* Prove:
1499       !p st Pr. (p LEADSTO False)(CONS st Pr) ==> (!s. Not p s)
1500 *)
1501 let LEADSTO_thm30_lemma00 = BETA_RULE
1502   (SPEC (`CONS (st:'a->'a) Pr`) (GEN (`Pr:('a->'a)list`) (BETA_RULE (SPEC_ALL (SPEC
1503    (`\(p:'a->bool) (q:'a->bool) (Pr:('a->'a)list). (q = False) ==> (!s. Not p s)`)
1504    LEADSTO_thm21)))));;
1505
1506 let LEADSTO_thm30_lemma01 = TAC_PROOF
1507   (([],
1508    (`!(r:'a->bool). (!s. Not r s) ==> (!s. r s = False s)`)),
1509    REWRITE_TAC [NOT_def1; FALSE_def] THEN
1510    BETA_TAC THEN
1511    REWRITE_TAC []);;
1512
1513 (*
1514   |- (!s. Not r s) ==> (r = False)
1515 *)
1516 let LEADSTO_thm30_lemma02 = (DISCH_ALL (REWRITE_RULE [ETA_AX] (MK_ABS (UNDISCH
1517      (SPEC_ALL LEADSTO_thm30_lemma01)))));;
1518
1519 let LEADSTO_thm30_lemma03 = TAC_PROOF
1520   (([],
1521   (`!p:'a->bool.
1522     (p' = (\s:'a->'a. ?p. P p /\ p s)) ==> (!s. p' s = ?p. P p /\ p s)`)),
1523   GEN_TAC THEN
1524   DISCH_TAC THEN
1525   GEN_TAC THEN
1526   ONCE_ASM_REWRITE_TAC [] THEN
1527   BETA_TAC THEN
1528   REFL_TAC);;
1529
1530 let LEADSTO_thm30_lemma04 = TAC_PROOF
1531   (([],
1532    (`!(p':'a->bool) (q':'a->bool).
1533      ((p' ENSURES q')(CONS st Pr) ==> (q' = False) ==> (!s. Not p' s)) /\
1534      (!r:'a->bool.
1535        ((r = False) ==> (!s. Not p' s)) /\
1536        ((q' = False) ==> (!s. Not r s)) ==>
1537        (q' = False) ==> (!s. Not p' s)) /\
1538      (!P:('a->bool)->bool.
1539        (p' = LUB P) /\
1540        (!p''. p'' In P ==> (q' = False) ==> (!s. Not p'' s)) ==>
1541        (q' = False) ==> (!s. Not p' s))`)),
1542    REPEAT GEN_TAC THEN
1543    REPEAT CONJ_TAC THENL
1544      [
1545       REPEAT STRIP_TAC THEN
1546       ASSUME_TAC (REWRITE_RULE [ASSUME (`(q':'a->bool) = False`)]
1547        (ASSUME (`((p':'a->bool) ENSURES q')(CONS st Pr)`))) THEN
1548       IMP_RES_TAC ENSURES_thm3 THEN
1549       ASM_REWRITE_TAC []
1550      ;
1551       REPEAT STRIP_TAC THEN
1552       RES_TAC THEN
1553       IMP_RES_TAC LEADSTO_thm30_lemma02 THEN
1554       RES_TAC THEN
1555       ASM_REWRITE_TAC []
1556      ;
1557       REPEAT GEN_TAC THEN
1558       REWRITE_TAC [LUB; IN; NOT_def1; FALSE_def] THEN
1559       BETA_TAC THEN
1560       REPEAT STRIP_TAC THEN
1561       ASSUME_TAC (REWRITE_RULE [ASSUME (`(q':'a->bool) = \s. F`)] (ASSUME
1562        (`!p'':'a->bool. P p''
1563             ==> ((q':'a->bool) = \s. F) ==> (!s. ~p'' s)`))) THEN
1564       IMP_RES_TAC LEADSTO_thm30_lemma03 THEN
1565       UNDISCH_TAC(`(p':'a->bool)s`) THEN
1566       ASM_REWRITE_TAC [] THEN
1567       BETA_TAC THEN
1568       REPEAT STRIP_TAC THEN
1569       RES_TAC
1570      ]);;
1571
1572 (*
1573   |- !p q st Pr. (p LEADSTO q)(CONS st Pr) ==> (q = False) ==> (!s. Not p s)
1574 *)
1575 let LEADSTO_thm30_lemma05 =
1576    GEN_ALL (MP (SPEC_ALL LEADSTO_thm30_lemma00) LEADSTO_thm30_lemma04);;
1577
1578 let LEADSTO_thm30_lemma06 = TAC_PROOF
1579   (([],
1580    (`!(p:'a->bool) st Pr.
1581        (p LEADSTO False)(CONS st Pr)
1582           ==> (?q. (q = False) /\ (p LEADSTO q)(CONS st Pr))`)),
1583    REPEAT STRIP_TAC THEN
1584    EXISTS_TAC (`False:'a->bool`) THEN
1585    ASM_REWRITE_TAC []);;
1586
1587 (* Now Prove:
1588    |- !p st Pr. (p LEADSTO False)(CONS st Pr) ==> (!s. Not p s)
1589 *)
1590 let LEADSTO_thm30 = prove_thm
1591   ("LEADSTO_thm30",
1592    (`!(p:'a->bool) st Pr. (p LEADSTO False)(CONS st Pr) ==> (!s. Not p s)`),
1593    REPEAT STRIP_TAC THEN
1594    IMP_RES_TAC LEADSTO_thm30_lemma06 THEN
1595    REWRITE_TAC [UNDISCH_ALL (SPEC_ALL LEADSTO_thm30_lemma05)]);;
1596
1597
1598 (* Prove:
1599   |- !p b q Pr.
1600     ((p  /\*  b) LEADSTO q)Pr /\ ((p  /\*  (Not b)) LEADSTO q)Pr ==> (p LEADSTO q)Pr
1601 *)
1602 let LEADSTO_cor1 = prove_thm
1603   ("LEADSTO_cor1",
1604    (`!(p:'a->bool) b q Pr.
1605        ((p  /\*  b) LEADSTO q) Pr /\ ((p  /\*  (Not b)) LEADSTO q) Pr
1606            ==> (p LEADSTO q) Pr`),
1607    REPEAT STRIP_TAC THEN
1608    IMP_RES_TAC (SPECL [(`(p:'a->bool)  /\*  b`); (`(p:'a->bool)  /\*  (Not b)`);
1609                        (`q:'a->bool`); (`Pr:('a->'a)list`)] LEADSTO_thm4) THEN
1610    ACCEPT_TAC (REWRITE_RULE [SYM (SPEC_ALL AND_OR_DISTR_lemma);
1611                                P_OR_NOT_P_lemma; AND_True_lemma]
1612     (ASSUME (`((((p:'a->bool)  /\*  b) \/* (p  /\*  (Not b))) LEADSTO q)Pr`))));;
1613
1614
1615 (* Prove:
1616   |- !p q r st Pr.
1617        (p LEADSTO q)(CONS st Pr) /\ r STABLE (CONS st Pr) ==>
1618            ((p  /\*  r) LEADSTO (q  /\*  r))(CONS st Pr)
1619 *)
1620 let LEADSTO_cor2 = prove_thm
1621   ("LEADSTO_cor2",
1622    (`!(p:'a->bool) q r st Pr.
1623        (p LEADSTO q)(CONS st Pr) /\ r STABLE (CONS st Pr)
1624             ==> ((p  /\*  r) LEADSTO (q  /\*  r))(CONS st Pr)`),
1625    REPEAT GEN_TAC THEN
1626    REWRITE_TAC [STABLE] THEN
1627    REPEAT STRIP_TAC THEN
1628    IMP_RES_TAC LEADSTO_thm29 THEN
1629    ACCEPT_TAC (REWRITE_RULE [OR_False_lemma] (ASSUME
1630      (`(((p:'a->bool)  /\*  r) LEADSTO ((q  /\*  r) \/* False))(CONS st Pr)`))));;
1631
1632
1633 (* Prove:
1634    |- !p q st Pr.
1635            (p LEADSTO q)(CONS st Pr) = ((p  /\*  (Not q)) LEADSTO q)(CONS st Pr)
1636 *)
1637 let LEADSTO_cor3 = prove_thm
1638   ("LEADSTO_cor3",
1639    (`!(p:'a->bool) q st Pr.
1640         (p LEADSTO q)(CONS st  Pr) = ((p  /\*  (Not q)) LEADSTO q)(CONS st  Pr)`),
1641    REPEAT GEN_TAC THEN
1642    EQ_TAC THEN
1643    REPEAT STRIP_TAC THENL
1644     [
1645      ASSUME_TAC (REWRITE_RULE [NOT_NOT_lemma]
1646       (SPECL [(`Not (q:'a->bool)`); (`CONS (st:'a->'a) Pr`)] UNLESS_thm2)) THEN
1647      IMP_RES_TAC LEADSTO_thm29 THEN
1648      ASSUME_TAC (REWRITE_RULE [P_AND_NOT_P_lemma]
1649       (ASSUME (`(((p:'a->bool) /\* (Not q)) LEADSTO
1650                  ((q /\* (Not q)) \/* q))(CONS st Pr)`))) THEN
1651      ACCEPT_TAC (REWRITE_RULE [OR_False_lemma]
1652       (ONCE_REWRITE_RULE [OR_COMM_lemma] (ASSUME
1653         (`(((p:'a->bool) /\* (Not q)) LEADSTO (False \/* q))(CONS st Pr)`))))
1654     ;
1655      ASSUME_TAC (MP
1656       (SPECL [(`(p:'a->bool) /\* q`); (`q:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
1657               LEADSTO_thm25)
1658       (SPECL [(`p:'a->bool`); (`q:'a->bool`)] AND_IMPLY_WEAK_lemma)) THEN
1659      IMP_RES_TAC LEADSTO_cor1
1660     ]);;
1661
1662
1663 (* Prove:
1664    |- !p b q st Pr.
1665        ((p /\* b) LEADSTO q)(CONS st Pr) /\
1666        ((p /\* (Not b)) LEADSTO ((p /\* b) \/* q))(CONS st Pr) ==>
1667            (p LEADSTO q)(CONS st Pr)
1668 *)
1669 let LEADSTO_cor4 = prove_thm
1670   ("LEADSTO_cor4",
1671    (`!(p:'a->bool) b q st Pr.
1672      ((p /\* b) LEADSTO q)(CONS st Pr) /\
1673      ((p /\* (Not b)) LEADSTO ((p /\* b) \/* q))(CONS st Pr)
1674           ==> (p LEADSTO q)(CONS st Pr)`),
1675    ONCE_REWRITE_TAC [OR_COMM_lemma] THEN
1676    REPEAT STRIP_TAC THEN
1677    IMP_RES_TAC LEADSTO_thm28 THEN
1678    ASSUME_TAC (REWRITE_RULE [OR_OR_lemma] (ASSUME
1679     (`(((p:'a->bool) /\* (Not b)) LEADSTO (q \/* q))(CONS st Pr)`))) THEN
1680    IMP_RES_TAC LEADSTO_cor1);;
1681
1682
1683 (* Prove:
1684   |- !p q r st Pr.
1685    ((p /\* q) LEADSTO r)(CONS st Pr) ==> (p LEADSTO ((Not q) \/* r))(CONS st Pr)
1686 *)
1687 let LEADSTO_cor5 = prove_thm
1688   ("LEADSTO_cor5",
1689    (`!(p:'a->bool) q r st Pr.
1690           ((p /\* q) LEADSTO r)(CONS st Pr)
1691                ==> (p LEADSTO ((Not q) \/* r))(CONS st Pr)`),
1692    REPEAT STRIP_TAC THEN
1693    ONCE_REWRITE_TAC [LEADSTO_cor3] THEN
1694    REWRITE_TAC [NOT_OR_AND_NOT_lemma; NOT_NOT_lemma] THEN
1695    ASSUME_TAC (REWRITE_RULE [NOT_NOT_lemma]
1696     (SPECL [(`Not (r:'a->bool)`); (`CONS (st:'a->'a) Pr`)] UNLESS_thm2)) THEN
1697    IMP_RES_TAC LEADSTO_thm29 THEN
1698    ASSUME_TAC (REWRITE_RULE [AND_ASSOC_lemma; P_AND_NOT_P_lemma] (ASSUME
1699     (`((((p:'a->bool) /\* q) /\* (Not r)) LEADSTO ((r /\* (Not r)) \/* r))
1700                                                (CONS st Pr)`))) THEN
1701    ASSUME_TAC (REWRITE_RULE [OR_False_lemma] (ONCE_REWRITE_RULE
1702     [OR_COMM_lemma] (ASSUME (`(((p:'a->bool) /\* (q /\* (Not r))) LEADSTO
1703                              (False \/* r))(CONS st Pr)`)))) THEN
1704    ASSUME_TAC (MP
1705     (SPEC_ALL (SPECL [(`r:'a->bool`); (`(Not (q:'a->bool)) \/* r`)] LEADSTO_thm25))
1706     (SPECL [(`r:'a->bool`); (`Not (q:'a->bool)`)] SYM_OR_IMPLY_WEAK_lemma)) THEN
1707    IMP_RES_TAC LEADSTO_thm1);;
1708
1709
1710 (* Prove:
1711    |- !p q r st Pr.
1712        (p LEADSTO q)(CONS st Pr) /\ (r UNLESS (q /\* r))(CONS st Pr) ==>
1713            ((p /\* r) LEADSTO (q /\* r))(CONS st Pr)
1714 *)
1715 let LEADSTO_cor6 = prove_thm
1716   ("LEADSTO_cor6",
1717    (`!(p:'a->bool) q r st Pr.
1718        (p LEADSTO q)(CONS st Pr) /\ (r UNLESS (q /\* r))(CONS st Pr)
1719             ==> ((p /\* r) LEADSTO (q /\* r))(CONS st Pr)`),
1720    REPEAT STRIP_TAC THEN
1721    IMP_RES_TAC LEADSTO_thm29 THEN
1722    ACCEPT_TAC (REWRITE_RULE [OR_OR_lemma] (ASSUME
1723     (`(((p:'a->bool) /\* r) LEADSTO ((q /\* r) \/* (q /\* r)))(CONS st Pr)`))));;
1724
1725
1726 (* Prove:
1727    |- !p q r st Pr.
1728        (p LEADSTO q)(CONS st Pr) /\ (r /\* (Not q)) STABLE (CONS st Pr) ==>
1729            (!s. (p /\* r)s ==> q s)
1730 *)
1731 let LEADSTO_cor7 = prove_thm
1732   ("LEADSTO_cor7",
1733    (`!(p:'a->bool) q r st Pr.
1734      (p LEADSTO q)(CONS st Pr) /\ (r /\* (Not q)) STABLE (CONS st Pr)
1735           ==> (!s. (p /\* r)s ==> q s)`),
1736    REPEAT GEN_TAC THEN
1737    STRIP_TAC THEN
1738    IMP_RES_TAC LEADSTO_cor2 THEN
1739    ASSUME_TAC (REWRITE_RULE
1740      [(SYM (SPEC_ALL AND_ASSOC_lemma)); P_AND_NOT_P_lemma]
1741       (ONCE_REWRITE_RULE [AND_AND_COMM_lemma] (ASSUME
1742         (`(((p:'a->bool) /\* (r /\* (Not q))) LEADSTO
1743            (q /\* (r /\* (Not q))))(CONS st Pr)`)))) THEN
1744    ASSUME_TAC (REWRITE_RULE [AND_False_lemma]
1745     (ONCE_REWRITE_RULE [AND_COMM_lemma] (ASSUME
1746       (`((((p:'a->bool) /\* (Not q)) /\* r) LEADSTO (False /\* r))
1747                                             (CONS st Pr)`)))) THEN
1748    IMP_RES_TAC LEADSTO_thm30 THEN
1749    GEN_TAC THEN
1750    MP_TAC (SPEC_ALL (ASSUME (`!s:'a. Not (r /\* (p /\* (Not q)))s`))) THEN
1751    REWRITE_TAC [NOT_def1; AND_def] THEN
1752    BETA_TAC THEN
1753    REWRITE_TAC [DE_MORGAN_THM] THEN
1754    REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
1755
1756 (*
1757   Prove:
1758    |- !p r q st Pr.
1759             (p LEADSTO r)(CONS st Pr) ==> ((p /\* q) LEADSTO r)(CONS st Pr)
1760 *)
1761 let LEADSTO_cor8 = prove_thm
1762   ("LEADSTO_cor8",
1763    (`!(p:'a->bool) r q st Pr. (p LEADSTO r)(CONS st Pr)
1764                    ==> ((p /\* q) LEADSTO r)(CONS st Pr)`),
1765    REPEAT STRIP_TAC THEN
1766    ASSUME_TAC (SPECL
1767      [`p:'a->bool`; `q:'a->bool`] SYM_AND_IMPLY_WEAK_lemma) THEN
1768    ASSUME_TAC (UNDISCH_ALL (SPECL
1769      [`(p:'a->bool) /\* q`; `p:'a->bool`; `st:'a->'a`; `Pr:('a->'a)list`]
1770      LEADSTO_thm25)) THEN
1771    IMP_RES_TAC LEADSTO_thm1);;
1772
1773 (*
1774   Prove:
1775    |- !p q r st Pr.
1776        (p LEADSTO q)(CONS st Pr) /\ (!s. q s ==> r s) ==>
1777            (p LEADSTO r)(CONS st Pr)
1778 *)
1779 let LEADSTO_cor9 = prove_thm
1780   ("LEADSTO_cor9",
1781    (`!(p:'a->bool) q r st Pr.
1782         (p LEADSTO q)(CONS st Pr) /\ (!s. q s ==> r s)
1783               ==> (p LEADSTO r)(CONS st Pr)`),
1784    REPEAT STRIP_TAC THEN
1785    IMP_RES_TAC LEADSTO_thm25 THEN
1786    ASSUME_TAC (SPEC_ALL (ASSUME
1787     (`!st Pr. ((q:'a->bool) LEADSTO r)(CONS st Pr)`))) THEN
1788    IMP_RES_TAC LEADSTO_thm1);;
1789
1790
1791 (* Prove:
1792    |- !P q Pr. (!i. ((P i) LEADSTO q)Pr) ==> (!i. (( \<=/*  P i) LEADSTO q)Pr)
1793 *)
1794 let LEADSTO_cor10 = prove_thm
1795   ("LEADSTO_cor10",
1796    (`!(P:num->'a->bool) q Pr.
1797       (!i. ((P i) LEADSTO q)Pr) ==> (!i. (( \<=/*  P i) LEADSTO q)Pr)`),
1798    REPEAT GEN_TAC THEN
1799    STRIP_TAC THEN
1800    INDUCT_TAC THENL
1801      [
1802       ASM_REWRITE_TAC [OR_LE_N_def]
1803      ;
1804       REWRITE_TAC [OR_LE_N_def] THEN
1805       ACCEPT_TAC (MP
1806        (SPECL [(` \<=/*  (P:num->'a->bool) i`); (`(P:num->'a->bool) (SUC i)`);
1807                (`q:'a->bool`); (`Pr:('a->'a)list`)] LEADSTO_thm4) (CONJ
1808          (ASSUME (`(( \<=/*  (P:num->'a->bool) i) LEADSTO q)Pr`))
1809          (SPEC (`SUC i`) (ASSUME (`!i. (((P:num->'a->bool) i) LEADSTO q)Pr`)))))
1810      ]);;
1811
1812
1813 (* Prove:
1814    !p st Pr. (False LEADSTO p) (CONS st Pr)
1815 *)
1816 let LEADSTO_cor11 = prove_thm
1817   ("LEADSTO_cor11",
1818    (`!(p:'a->bool) st Pr. (False LEADSTO p) (CONS st Pr)`),
1819    REPEAT GEN_TAC THEN
1820    REWRITE_TAC [LEADSTO;LeadstoRel] THEN
1821    REPEAT STRIP_TAC THEN
1822    ACCEPT_TAC (REWRITE_RULE [ENSURES_cor6] (CONJUNCT1
1823     (SPECL [(`False:'a->bool`); (`p:'a->bool`)]
1824       (ASSUME (`!(p:'a->bool) q.
1825         ((p ENSURES q)(CONS st Pr) ==> R p q(CONS st Pr)) /\
1826         (!r. R p r(CONS st Pr) /\ R r q(CONS st Pr) ==> R p q(CONS st Pr)) /\
1827         (!P. (p = LUB P) /\ (!p'. p' In P ==> R p' q(CONS st Pr)) ==>
1828                            R p q(CONS st Pr))`))))));;
1829
1830
1831 (* Prove:
1832    |- !P q st Pr. (!i. ((P i) LEADSTO q)(CONS st Pr)) ==>
1833                   (!i. (( \</*  P i) LEADSTO q)(CONS st Pr))
1834 *)
1835 let LEADSTO_cor12 = prove_thm
1836   ("LEADSTO_cor12",
1837    (`!(P:num->'a->bool) q st Pr.
1838       (!i. ((P i) LEADSTO q)(CONS st Pr))
1839              ==> (!i. (( \</*  P i) LEADSTO q)(CONS st Pr))`),
1840    REPEAT GEN_TAC THEN
1841    STRIP_TAC THEN
1842    INDUCT_TAC THEN
1843    ASM_REWRITE_TAC [OR_LT_N_def; LEADSTO_cor11] THEN
1844    ACCEPT_TAC (MP
1845       (SPECL [(` \</*  (P:num->'a->bool) i`); (`(P:num->'a->bool) i`);
1846               (`q:'a->bool`); (`CONS (st:'a->'a) Pr`)] LEADSTO_thm4) (CONJ
1847          (ASSUME (`(( \</*  (P:num->'a->bool) i) LEADSTO q)(CONS st Pr)`))
1848          (SPEC (`i:num`)
1849            (ASSUME (`!i. (((P:num->'a->bool) i) LEADSTO q)(CONS st Pr)`))))));;
1850
1851 (*
1852   We now want to introduce some tactics for allowing structural induction
1853   of leadsto relations, but we have problems with the induction principle
1854   for the completion theorem:
1855
1856    !P Q R P' Q' Pr.
1857      (P LEADSTO Q)Pr /\ (P' LEADSTO Q')Pr /\ (Q UNLESS R)Pr /\ (Q' UNLESS R)Pr
1858        ==> ((P /\* P') LEADSTO ((Q /\* Q') \/* R))Pr
1859
1860   since this theorems demands another induction principle not directly
1861   derivable from the given definition of leadsto.
1862
1863   We circumvent the problem by proving that leadsto may be defined by another
1864   functional.
1865
1866   This time we use the results of Tarski directly.
1867 *)
1868 (* *)
1869 (*
1870   Suppose we wanted to change the transitive inductitive axiom into
1871
1872                    p ensures r, r leadsto q
1873                  --------------------------- (2)
1874                         p leadsto q
1875
1876   instead of the previous given.
1877
1878   Let us investigate the following definition a litte:
1879
1880   Now the functional becomes
1881 *)
1882
1883 (*
1884   |- !R Pr.
1885     LEADSTO2Fn R Pr =
1886     (\p q.
1887       (p ENSURES q) Pr \/
1888       (?r. (p ENSURES r) Pr /\ R r q Pr) \/
1889       (?P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr)))
1890 *)
1891 let LEADSTO2Fn = new_definition
1892   (`LEADSTO2Fn R = \(p:'a->bool) q Pr.
1893      (p ENSURES q) Pr \/
1894      (?r. (p ENSURES r) Pr /\ R r q Pr) \/
1895      (?P. (p = LUB P) /\ (!p. p In P ==> R p q Pr))`);;
1896
1897 (*
1898   |- !p q Pr.
1899       LEADSTO2 p q Pr =
1900         (!R Pr. (!p' q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr) ==> R p q Pr)
1901 *)
1902 let LEADSTO2 = new_definition
1903    (`LEADSTO2 (p:'a->bool) q Pr =
1904       !R. (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr) ==> R p q Pr`);;
1905
1906 (*
1907   |- !R p q Pr.
1908     (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr) ==>
1909     (!p q.
1910       (\p q Pr. !R.
1911            (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr) ==> R p q Pr) p q Pr
1912     ==>
1913       R p q Pr)
1914 *)
1915 let LEADSTO2Imply_1 = TAC_PROOF
1916   (([],
1917    (`!R (p:'a->bool) (q:'a->bool) (Pr:('a->'a)list).
1918        (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr) ==>
1919           (!p q. (\p q Pr. !R. (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr)
1920                            ==> R p q Pr) p q Pr
1921                    ==> R p q Pr)`)),
1922    BETA_TAC THEN
1923    REPEAT STRIP_TAC THEN
1924    RES_TAC);;
1925
1926 (*
1927   |- !R1 R2 Pr.
1928     (!p q. R1 p q Pr ==> R2 p q Pr) ==>
1929     (!p q. LEADSTO2Fn R1 p q Pr ==> LEADSTO2Fn R2 p q Pr)
1930 *)
1931 let IsMonoLEADSTO2 = TAC_PROOF
1932   (([],
1933    (`!R1 R2 (Pr:('a->'a)list).
1934       (!p q. R1 p q Pr ==> R2 p q Pr)
1935             ==> (!p q. LEADSTO2Fn R1 p q Pr ==> LEADSTO2Fn R2 p q Pr)`)),
1936    REWRITE_TAC [LEADSTO2Fn] THEN
1937    BETA_TAC THEN
1938    REPEAT STRIP_TAC THENL
1939     [
1940      ASM_REWRITE_TAC []
1941     ;
1942      RES_TAC THEN
1943      DISJ2_TAC THEN
1944      DISJ1_TAC THEN
1945      EXISTS_TAC (`r:'a->bool`) THEN
1946      ASM_REWRITE_TAC []
1947     ;
1948      DISJ2_TAC THEN
1949      DISJ2_TAC THEN
1950      EXISTS_TAC (`P:('a->bool)->bool`) THEN
1951      ASM_REWRITE_TAC [] THEN
1952      REPEAT STRIP_TAC THEN
1953      RES_TAC THEN
1954      RES_TAC
1955     ]);;
1956
1957 (*
1958 LEADSTO2th =
1959   |- LEADSTO2 =
1960    (\p q Pr.
1961      !R. (!p' q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr) ==> R p q Pr)
1962 *)
1963 let LEADSTO2th = (REWRITE_RULE [ETA_AX] (MK_ABS (GEN (`p:'a->bool`)  (MK_ABS
1964   (GEN (`q:'a->bool`) (MK_ABS (GEN (`Pr:('a->'a)list`) (SPEC_ALL LEADSTO2))))))));;
1965
1966 (*
1967   |- !p q Pr. LEADSTO2Fn LEADSTO2 p q Pr ==> LEADSTO2 p q Pr
1968 *)
1969 let LEADSTO2Imply1 = TAC_PROOF
1970   (([],
1971    (`!(p:'a->bool) q Pr.
1972        LEADSTO2Fn LEADSTO2 p q Pr ==> LEADSTO2 p q Pr`)),
1973    REPEAT GEN_TAC THEN
1974    ASSUME_TAC (GENL
1975     [(`R1:('a->bool)->('a->bool)->(('a->'a)list)->bool`);
1976      (`R2:('a->bool)->('a->bool)->(('a->'a)list)->bool`)]
1977      (SPEC_ALL IsMonoLEADSTO2)) THEN
1978    REWRITE_TAC [LEADSTO2th] THEN
1979    BETA_TAC THEN
1980    REPEAT STRIP_TAC THEN
1981    ASSUME_TAC (MP (SPEC_ALL (MP (BETA_RULE (SPEC_ALL (SPECL
1982       [(`\(p:'a->bool) q Pr. !R. (!p' q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr)
1983             ==> R p q Pr`);
1984        (`R:('a->bool)->('a->bool)->(('a->'a)list)->bool`)] IsMonoLEADSTO2)))
1985      (BETA_RULE (MP (SPEC_ALL LEADSTO2Imply_1)
1986           (ASSUME (`!(p':'a->bool) q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr`))))))
1987       (ASSUME (`LEADSTO2Fn (\(p:'a->bool) q Pr.
1988         !R. (!p' q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr)
1989                 ==> R p q Pr) p q Pr`))) THEN
1990    RES_TAC);;
1991
1992 (*
1993   |- !p q Pr. LEADSTO2 p q Pr ==> LEADSTO2Fn LEADSTO2 p q Pr
1994 *)
1995 let LEADSTO2Imply2 = TAC_PROOF
1996   (([],
1997    (`!(p:'a->bool) q Pr. LEADSTO2 p q Pr ==> LEADSTO2Fn LEADSTO2 p q Pr`)),
1998    REPEAT STRIP_TAC THEN
1999    ASSUME_TAC (REWRITE_RULE [ETA_AX] (MP (BETA_RULE (SPECL
2000     [(`\p q Pr. LEADSTO2Fn LEADSTO2 (p:'a->bool) q Pr`);
2001      (`LEADSTO2:('a->bool)->('a->bool)->(('a->'a)list)->bool`);
2002      (`Pr:('a->'a)list`)] IsMonoLEADSTO2))
2003        (GENL [(`p:'a->bool`); (`q:'a->bool`)] (SPEC_ALL LEADSTO2Imply1)))) THEN
2004    ACCEPT_TAC (UNDISCH (GEN_ALL (SPEC
2005     (`LEADSTO2Fn (LEADSTO2:('a->bool)->('a->bool)->(('a->'a)list)->bool)`) (BETA_RULE
2006       (REWRITE_RULE [LEADSTO2] (ASSUME (`LEADSTO2 (p:'a->bool) q Pr`))))))));;
2007
2008 (*
2009   |- !p q Pr. LEADSTO2 p q Pr = LEADSTO2Fn LEADSTO2 p q Pr
2010 *)
2011 let LEADSTO2EQs = TAC_PROOF
2012   (([],
2013    (`!(p:'a->bool) q Pr. LEADSTO2 p q Pr = LEADSTO2Fn LEADSTO2 p q Pr`)),
2014    REPEAT STRIP_TAC THEN
2015    EQ_TAC THENL
2016     [
2017      ACCEPT_TAC (SPEC_ALL LEADSTO2Imply2)
2018     ;
2019      ACCEPT_TAC (SPEC_ALL LEADSTO2Imply1)
2020     ]);;
2021
2022 (*
2023   |- LEADSTO2 = LEADSTO2Fn LEADSTO2
2024 *)
2025 let LEADSTO2EQ =
2026   (REWRITE_RULE [ETA_AX]
2027     (MK_ABS (GEN (`p:'a->bool`)
2028       (MK_ABS (GEN (`q:'a->bool`) (MK_ABS (GEN (`Pr:('a->'a)list`)
2029          (SPEC_ALL LEADSTO2EQs))))))));;
2030
2031 (*
2032   |- !R. (R = LEADSTO2Fn R) ==> (!p q Pr. LEADSTO2Fn R p q Pr ==> R p q Pr)
2033 *)
2034 let LEADSTO2Thm1_1 = TAC_PROOF
2035   (([],
2036    (`!R. (R = LEADSTO2Fn R)
2037            ==> (!(p:'a->bool) q Pr. LEADSTO2Fn R p q Pr ==> R p q Pr)`)),
2038    REPEAT STRIP_TAC THEN
2039    ONCE_REWRITE_TAC
2040     [ASSUME
2041       (`R = LEADSTO2Fn (R:('a->bool)->('a->bool)->(('a->'a)list)->bool)`)] THEN
2042    REWRITE_TAC [ASSUME (`LEADSTO2Fn R (p:'a->bool) q Pr`)]);;
2043
2044 (*
2045   |- !R. (R = LEADSTO2Fn R) ==> (!p q Pr. LEADSTO2 p q Pr ==> R p q Pr)
2046 *)
2047 let LEADSTO2MinFixThm = TAC_PROOF
2048   (([],
2049    (`!R. (R = LEADSTO2Fn R)
2050            ==> (!(p:'a->bool) q Pr. LEADSTO2 p q Pr ==> R p q Pr)`)),
2051    REWRITE_TAC [LEADSTO2] THEN
2052    REPEAT STRIP_TAC THEN
2053    ASSUME_TAC (SPEC_ALL (ASSUME
2054      (`!R. (!(p':'a->bool) q'. LEADSTO2Fn R p' q' Pr ==> R p' q' Pr)
2055               ==> R p q Pr`))) THEN
2056    ASSUME_TAC (GENL [(`p:'a->bool`); (`q:'a->bool`)] (SPEC_ALL
2057      (UNDISCH (SPEC_ALL LEADSTO2Thm1_1)))) THEN
2058    RES_TAC);;
2059
2060 (*
2061   |- !R.
2062     (!p q Pr. LEADSTO2Fn R p q Pr ==> R p q Pr) ==>
2063     (!p q Pr. LEADSTO2 p q Pr ==> R p q Pr)
2064 *)
2065 let LEADSTO2InductThm = TAC_PROOF
2066   (([],
2067    (`!R. (!(p:'a->bool) q Pr. LEADSTO2Fn R p q Pr ==> R p q Pr)
2068              ==> (!p q Pr. LEADSTO2 p q Pr ==> R p q Pr)`)),
2069    REPEAT GEN_TAC THEN
2070    REWRITE_TAC [LEADSTO2] THEN
2071    REPEAT STRIP_TAC THEN
2072    ASSUME_TAC (GENL [(`p:'a->bool`); (`q:'a->bool`)] (SPEC_ALL (ASSUME
2073     (`!(p:'a->bool) q Pr. LEADSTO2Fn R p q Pr ==> R p q Pr`)))) THEN
2074    RES_TAC);;
2075
2076 (*
2077   |- !R Pr.
2078     LEADSTO2Fam R Pr =
2079     (!p q.
2080       ((p ENSURES q)Pr ==> R p q Pr) /\
2081       (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2082       (!P. (!p. p In P ==> R p q Pr)    ==> R (LUB P) q Pr)
2083 *)
2084 let LEADSTO2Fam = new_definition
2085    (`LEADSTO2Fam R Pr =
2086      !(p:'a->bool) (q:'a->bool).
2087          ((p ENSURES q) Pr                 ==> R p q Pr) /\
2088          (!r. (p ENSURES r) Pr /\ R r q Pr ==> R p q Pr) /\
2089          (!P. (!p. p In P ==> R p q Pr)    ==> R (LUB P) q Pr)`);;
2090
2091 (*
2092   |- !R Pr. (!p q. LEADSTO2Fn R p q Pr ==> R p q Pr) = LEADSTO2Fam R Pr
2093 *)
2094 let LEADSTO2Fn_EQ_LEADSTO2Fam = TAC_PROOF
2095   (([],
2096    (`!R Pr.
2097       (!(p:'a->bool) q. LEADSTO2Fn R p q Pr ==> R p q Pr) = LEADSTO2Fam R Pr`)),
2098    REWRITE_TAC [LEADSTO2Fam; LEADSTO2Fn] THEN
2099    BETA_TAC THEN
2100    REPEAT GEN_TAC THEN
2101    EQ_TAC THEN
2102    REPEAT STRIP_TAC THEN
2103    RES_TAC THENL
2104     [
2105      REWRITE_TAC [REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
2106         (`!p. (p = LUB (P:('a->bool)->bool)) ==>
2107              (R:('a->bool)->('a->bool)->(('a->'a)list)->bool) p q Pr`)))]
2108     ;
2109      ASM_REWRITE_TAC []
2110     ]);;
2111
2112
2113 (*
2114         Prove that the wanted axioms 1;  2, 3 are really theorems for the found
2115         fixed point
2116 *)
2117
2118 (*
2119   |- !p q Pr. (p ENSURES q)Pr ==> LEADSTO2 p q Pr
2120 *)
2121 let LEADSTO2_thm0 = prove_thm
2122   ("LEADSTO2_thm0",
2123    (`!(p:'a->bool) q Pr. (p ENSURES q) Pr ==> LEADSTO2 p q Pr`),
2124    REWRITE_TAC [LEADSTO2; LEADSTO2Fn] THEN
2125    BETA_TAC THEN
2126    REPEAT STRIP_TAC THEN
2127    RES_TAC);;
2128
2129 (*
2130   |- !p r q Pr. (p ENSURES r)Pr /\ LEADSTO2 r q Pr ==> LEADSTO2 p q Pr
2131 *)
2132 let LEADSTO2_thm1 = prove_thm
2133   ("LEADSTO2_thm1",
2134    (`!(p:'a->bool) r q Pr.
2135         (p ENSURES r) Pr /\ (LEADSTO2 r q Pr) ==> (LEADSTO2 p q Pr)`),
2136    REWRITE_TAC [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam] THEN
2137    REPEAT STRIP_TAC THEN
2138    RES_TAC THEN
2139    RES_TAC);;
2140
2141
2142 (* Prove:
2143    |- !P q Pr. (!p. p In P ==> LEADSTO2 p q Pr) ==> LEADSTO2(LUB P)q Pr
2144 *)
2145 let LEADSTO2_thm3_lemma1 = TAC_PROOF
2146   (([],
2147    (`(!p:'a->bool. p In P ==>
2148      (!R.
2149        (!p q.
2150          ((p ENSURES q)Pr ==> R p q Pr) /\
2151          (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2152          (!P. (!p'. p' In P ==> R p' q Pr) ==> R (LUB P) q Pr)) ==>
2153        R p q Pr)) ==>
2154    (!p. p In P ==>
2155      (!p q.
2156        ((p ENSURES q)Pr ==> R p q Pr) /\
2157        (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2158        (!P. (!p'. p' In P ==> R p' q Pr) ==> R (LUB P) q Pr)) ==>
2159      R p q Pr)`)),
2160    REPEAT STRIP_TAC THEN
2161    RES_TAC);;
2162
2163 let LEADSTO2_thm3 = prove_thm
2164   ("LEADSTO2_thm3",
2165    (`!(P:('a->bool)->bool) q Pr.
2166        (!p. p In P ==> LEADSTO2 p q Pr) ==> LEADSTO2 (LUB P) q Pr`),
2167    REPEAT GEN_TAC THEN
2168    REWRITE_TAC [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam] THEN
2169    REPEAT STRIP_TAC THEN
2170    ASSUME_TAC (GEN_ALL (REWRITE_RULE[ASSUME
2171      (`!(p:'a->bool) q.
2172         ((p ENSURES q)Pr ==> R p q Pr) /\
2173         (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2174         (!P. (!p'. p' In P ==> R p' q Pr) ==> R (LUB P) q Pr)`)]
2175            (SPEC_ALL (UNDISCH (SPEC_ALL LEADSTO2_thm3_lemma1))))) THEN
2176    RES_TAC);;
2177
2178 let LEADSTO2_thm3a = prove_thm
2179   ("LEADSTO2_thm3a",
2180    (`!(P:('a->bool)->bool) q Pr.
2181        (p = LUB P) /\ (!p. p In P ==> LEADSTO2 p q Pr)
2182              ==> LEADSTO2 p q Pr`),
2183    REPEAT STRIP_TAC THEN
2184    IMP_RES_TAC LEADSTO2_thm3 THEN
2185    ASM_REWRITE_TAC []);;
2186
2187 (*
2188    !p1 p2 q Pr. (LEADSTO2 p1 q Pr) /\ (LEADSTO2 p2 q Pr)
2189                      ==> (LEADSTO2 (p1 \/* p2) q Pr)
2190 *)
2191
2192 (*
2193   To prove this we need some general lemmas about expressing two known
2194   relations as one relation:
2195 *)
2196
2197 (*
2198   |- !p1 p2 s. (p1 \/* p2)s = LUB(\p. (p = p1) \/ (p = p2))s
2199 *)
2200 let LEADSTO2_thm4_lemma1a = TAC_PROOF
2201   (([],
2202    (`!(p1:'a->bool) p2 s. (p1 \/* p2) s = (LUB (\p. (p = p1) \/ (p = p2))) s`)),
2203    REPEAT GEN_TAC THEN
2204    REWRITE_TAC [LUB; OR_def] THEN
2205    BETA_TAC THEN
2206    EQ_TAC THENL
2207      [
2208       STRIP_TAC THENL
2209        [
2210         EXISTS_TAC (`p1:'a->bool`) THEN
2211         ASM_REWRITE_TAC []
2212        ;
2213         EXISTS_TAC (`p2:'a->bool`) THEN
2214         ASM_REWRITE_TAC []
2215        ]
2216      ;
2217       STRIP_TAC THENL
2218        [
2219         REWRITE_TAC [REWRITE_RULE [ASSUME (`(p:'a->bool) = p1`)] (ASSUME
2220          (`(p:'a->bool) s`))]
2221        ;
2222         REWRITE_TAC [REWRITE_RULE [ASSUME (`(p:'a->bool) = p2`)] (ASSUME
2223          (`(p:'a->bool) s`))]
2224        ]
2225      ]);;
2226
2227 (*
2228   |- !p1 p2. p1 \/* p2 = LUB(\p. (p = p1) \/ (p = p2))
2229 *)
2230 let LEADSTO2_thm4_lemma1 =  (GEN_ALL (REWRITE_RULE [ETA_AX] (MK_ABS (GEN (`s:'a`)
2231   (SPEC_ALL LEADSTO2_thm4_lemma1a)))));;
2232
2233 (*
2234   |- !R Pr.
2235     (!p' q'.
2236       (p' ENSURES q')Pr \/
2237       (?r. (p' ENSURES r)Pr /\ R r q' Pr) \/
2238       (?P. (p' = LUB P) /\ (!p. p In P ==> R p q' Pr)) ==>
2239       R p' q' Pr) ==>
2240     (!p q P. (p = LUB P) /\ (!p. p In P ==> R p q Pr) ==> R p q Pr)
2241 *)
2242 let LEADSTO2_thm4_lemma2 = TAC_PROOF
2243   (([],
2244    (`!(R:('a->bool)->('a->bool)->(('a->'a)list)->bool) Pr.
2245      (!p' q'.
2246         (p' ENSURES q') Pr \/ (?r. (p' ENSURES r) Pr /\ R r q' Pr) \/
2247         (?P. (p' = LUB P) /\ (!p. p In P ==> R p q' Pr)) ==> R p' q' Pr)
2248       ==> (!p q P. ((p = LUB P) /\ (!p. p In P ==> R p q Pr)) ==> R p q Pr)`)),
2249    REPEAT STRIP_TAC THEN
2250    RES_TAC);;
2251
2252 (*
2253   |- !R p1 p2 q Pr Pr. R p1 q Pr ==> R p2 q Pr ==>
2254                           (!p. (\p. (p = p1) \/ (p = p2))p ==> R p q Pr)
2255 *)
2256 let LEADSTO2_thm4_lemma3 = TAC_PROOF
2257   (([],
2258    (`!R (p1:'a->bool) p2 (q:'a->bool) (Pr:('a->'a)list) (Pr:('a->'a)list).
2259       R p1 q Pr ==> R p2 q Pr ==>
2260        (!p. (\p. (p = p1) \/ (p = p2))p ==> R p q Pr)`)),
2261    BETA_TAC THEN
2262    REPEAT STRIP_TAC THENL
2263     [
2264      ASM_REWRITE_TAC []
2265     ;
2266      ASM_REWRITE_TAC []
2267     ]);;
2268
2269 (*
2270   |- !R p1 p2 q Pr. R p1 q Pr ==> R p2 q Pr ==>
2271        (!p q P. (p = LUB P) /\ (!p. p In P ==> R p q Pr) ==> R p q Pr) ==>
2272                  R(p1 \/* p2)q Pr
2273 *)
2274 let LEADSTO2_thm4_lemma4 = TAC_PROOF
2275   (([],
2276    (`!R (p1:'a->bool) (p2:'a->bool) (q:'a->bool)  (Pr:('a->'a)list).
2277       R p1 q Pr ==> R p2 q Pr ==>
2278        (!p q P. (p = LUB P) /\ (!p. p In P ==> R p q Pr) ==> R p q Pr) ==>
2279           R (p1 \/* p2) q Pr`)),
2280    REWRITE_TAC [IN] THEN
2281    REPEAT STRIP_TAC THEN
2282    ACCEPT_TAC (REWRITE_RULE
2283     [SYM (SPEC_ALL LEADSTO2_thm4_lemma1);
2284      UNDISCH_ALL (SPEC_ALL LEADSTO2_thm4_lemma3)]
2285       (SPECL
2286         [(`(p1:'a->bool) \/* p2`); (`q:'a->bool`); (`\p:'a->bool. (p = p1) \/ (p = p2)`)]
2287            (ASSUME (`!p (q:'a->bool) (P:('a->bool)->bool). (p = LUB P) /\
2288                      (!p. P p ==> R p q Pr) ==> R p q (Pr:('a->'a)list)`)))));;
2289
2290 (*
2291   Now Prove that the finite disjunction is satisfied
2292 *)
2293
2294 (*
2295   |- !p1 p2 q Pr.
2296        LEADSTO2 p1 q Pr /\ LEADSTO2 p2 q Pr ==> LEADSTO2(p1 \/* p2)q Pr
2297 *)
2298 let LEADSTO2_thm4 = prove_thm
2299   ("LEADSTO2_thm4",
2300    (`!(p1:'a->bool) p2 q Pr.
2301        (LEADSTO2 p1 q Pr) /\ (LEADSTO2 p2 q Pr) ==> LEADSTO2 (p1 \/* p2) q Pr`),
2302    REWRITE_TAC [LEADSTO2; LEADSTO2Fn] THEN
2303    BETA_TAC THEN
2304    REPEAT STRIP_TAC THEN
2305    RES_TAC THEN
2306    ASSUME_TAC (UNDISCH (SPEC_ALL LEADSTO2_thm4_lemma2)) THEN
2307    ACCEPT_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO2_thm4_lemma4)));;
2308
2309
2310 (* Prove:
2311
2312    This is more difficult and we need to use structural induction
2313
2314 *)
2315
2316 (*
2317   Prove the induction theorem:
2318   |- !X p q Pr.
2319       (!p q.
2320         ((p ENSURES q)Pr ==> X p q Pr) /\
2321         (!r. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
2322         (!P. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr))
2323      ==>
2324       LEADSTO2 p q Pr ==> X p q Pr
2325 *)
2326 let LEADSTO2_thm8 = prove_thm
2327   ("LEADSTO2_thm8",
2328    (`!X (p:'a->bool) q Pr.
2329       (!(p:'a->bool) q.
2330         ((p ENSURES q)Pr ==> X p q Pr) /\
2331         (!r. (p ENSURES r)Pr /\ X r q Pr ==> (X p q Pr)) /\
2332         (!P. (!p. p In P ==> X p q Pr) ==> (X (LUB P) q Pr)))
2333      ==> ((LEADSTO2 p q Pr) ==> X p q Pr)`),
2334    REPEAT GEN_TAC THEN
2335    REPEAT DISCH_TAC THEN
2336    ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL CONJ_ASSOC)] (BETA_RULE
2337     (SPEC (`\(p:'a->bool) (q:'a->bool) (Pr:('a->'a)list). X p q Pr:bool`)
2338      (REWRITE_RULE [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam]
2339         (ASSUME (`LEADSTO2 (p:'a->bool) q Pr`)))))) THEN
2340    RES_TAC);;
2341
2342 (*
2343   We now use LEADSTO2_thm8 to prove a slightly modified writing of the wanted
2344   theorem:
2345
2346      !p q Pr. (LEADSTO2 p q Pr) ==> (!r. LEADSTO2 q r Pr ==> LEADSTO2 p r Pr)
2347
2348 *)
2349
2350 (*
2351   We get by specialization:
2352
2353   |- (!p' q'.
2354
2355        ((p' ENSURES q')Pr ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr)) /\
2356
2357        (!r.
2358          (p' ENSURES r)Pr /\ (!r'. LEADSTO2 q' r' Pr ==> LEADSTO2 r r' Pr)
2359             ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr)) /\
2360
2361        (!P.
2362          (!p''. p'' In P ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p'' r Pr))
2363             ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2(LUB P)r Pr)))
2364
2365     ==>
2366
2367       LEADSTO2 p q Pr ==> (!r. LEADSTO2 q r Pr ==> LEADSTO2 p r Pr)
2368
2369 *)
2370
2371 let LEADSTO2_thm2a = (BETA_RULE (SPECL
2372   [(`\p q Pr. !r:'a->bool. LEADSTO2 q r Pr ==> LEADSTO2 p r Pr`);
2373    (`p:'a->bool`); (`q:'a->bool`); (`Pr:('a->'a)list`)] LEADSTO2_thm8));;
2374
2375 (*
2376   We prove the implications of Rel_thm2a:
2377 *)
2378
2379 (*
2380   |- !p' q'. (p' ENSURES q')Pr ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr)
2381 *)
2382 let LEADSTO2_thm2b = TAC_PROOF
2383   (([],
2384    (`!(p':'a->bool) q'.
2385      ((p' ENSURES q')Pr ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr))`)),
2386    REPEAT STRIP_TAC THEN
2387    IMP_RES_TAC LEADSTO2_thm1);;
2388
2389 (*
2390   |- !p' q' r.
2391     (p' ENSURES r)Pr /\ (!r'. LEADSTO2 q' r' Pr ==> LEADSTO2 r r' Pr) ==>
2392     (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr)
2393 *)
2394 let LEADSTO2_thm2c = TAC_PROOF
2395   (([],
2396    (`!(p':'a->bool) q'.
2397      (!r.
2398        (p' ENSURES r)Pr /\ (!r'. LEADSTO2 q' r' Pr ==> LEADSTO2 r r' Pr) ==>
2399        (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p' r Pr))`)),
2400    REPEAT STRIP_TAC THEN
2401    RES_TAC THEN
2402    IMP_RES_TAC LEADSTO2_thm1);;
2403
2404 (*
2405   |- !p' q' P.
2406       (!p''. p'' In P ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p'' r Pr)) ==>
2407          (!r. LEADSTO2 q' r Pr ==> LEADSTO2(LUB P)r Pr)
2408 *)
2409 let LEADSTO2_thm2d_lemma1 = TAC_PROOF
2410   (([],
2411    (`!(q':'a->bool) r Pr.
2412      LEADSTO2 q' r Pr ==>
2413       (!p'':'a->bool. p'' In P ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p'' r Pr))
2414           ==> (!p'':'a->bool. p'' In P ==> LEADSTO2 p'' r Pr)`)),
2415    REPEAT STRIP_TAC THEN
2416    RES_TAC);;
2417
2418 let LEADSTO2_thm2d = TAC_PROOF
2419   (([],
2420    (`!(p':'a->bool) q'.
2421       (!P:('a->bool)->bool.
2422        (!p''. p'' In P ==> (!r. LEADSTO2 q' r Pr ==> LEADSTO2 p'' r Pr)) ==>
2423        (!r. LEADSTO2 q' r Pr ==> LEADSTO2(LUB P)r Pr))`)),
2424    REPEAT STRIP_TAC THEN
2425    IMP_RES_TAC LEADSTO2_thm2d_lemma1 THEN
2426    IMP_RES_TAC LEADSTO2_thm3);;
2427
2428 (*
2429   Hence by rewriting we get:
2430
2431   |- LEADSTO2 p q Pr ==> (!r. LEADSTO2 q r Pr ==> LEADSTO2 p r Pr)
2432
2433 *)
2434 let LEADSTO2_thm2e =
2435 (REWRITE_RULE [LEADSTO2_thm2b; LEADSTO2_thm2c; LEADSTO2_thm2d] LEADSTO2_thm2a);;
2436
2437 (* Now we may Prove:
2438
2439   |- !p r q Pr. LEADSTO2 p r Pr /\ LEADSTO2 r q Pr ==> LEADSTO2 p q Pr
2440
2441 *)
2442 let LEADSTO2_thm2 = prove_thm
2443   ("LEADSTO2_thm2",
2444    (`!(p:'a->bool) r q Pr.
2445        (LEADSTO2 p r Pr) /\ (LEADSTO2 r q Pr) ==> (LEADSTO2 p q Pr)`),
2446    REPEAT STRIP_TAC THEN
2447    IMP_RES_TAC LEADSTO2_thm2e);;
2448
2449 (*
2450   |- !p q Pr.
2451     (p ENSURES q)Pr \/
2452     (?r. LEADSTO2 p r Pr /\ LEADSTO2 r q Pr) \/
2453     (?P. (p = LUB P) /\ (!p. p In P ==> LEADSTO2 p q Pr))
2454    =
2455     LEADSTO2 p q Pr
2456 *)
2457 let LEADSTO2_thm5 = prove_thm
2458   ("LEADSTO2_thm5",
2459    (`!(p:'a->bool) q Pr.
2460        ((p ENSURES q)Pr \/
2461         (?r. (LEADSTO2 p r Pr) /\ (LEADSTO2 r q Pr)) \/
2462         (?P. (p = (LUB P)) /\ (!p. p In P ==> LEADSTO2 p q Pr)))
2463       =
2464        (LEADSTO2 p q Pr)`),
2465    REPEAT STRIP_TAC THEN
2466    EQ_TAC THENL
2467      [
2468       REPEAT STRIP_TAC THENL
2469         [
2470          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO2_thm0))
2471         ;
2472          IMP_RES_TAC LEADSTO2_thm2
2473         ;
2474          IMP_RES_TAC LEADSTO2_thm3 THEN
2475          ASM_REWRITE_TAC []
2476         ]
2477      ;
2478       REPEAT STRIP_TAC THEN
2479       DISJ2_TAC THEN
2480       DISJ2_TAC THEN
2481       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
2482       REWRITE_TAC [LUB; IN] THEN
2483       BETA_TAC THEN
2484       CONJ_TAC THENL
2485        [
2486         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
2487        ;
2488         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
2489         REPEAT STRIP_TAC THEN
2490         ACCEPT_TAC (ONCE_REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)] (ASSUME
2491          (`LEADSTO2 (p:'a->bool) q Pr`)))
2492        ]
2493      ]);;
2494
2495 (*
2496   |- !p q Pr.
2497     (p ENSURES q)Pr \/
2498     (?r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr) \/
2499     (?P. (p = ?*  P) /\ (!i. LEADSTO2(P i)q Pr))
2500    =
2501     LEADSTO2 p q Pr
2502 *)
2503 let LEADSTO2_thm6 = prove_thm
2504   ("LEADSTO2_thm6",
2505    (`!(p:'a->bool) q Pr.
2506        ((p ENSURES q)Pr \/
2507         (?r. (p ENSURES r)Pr /\ (LEADSTO2 r q Pr)) \/
2508         (?P. (p = (LUB P)) /\ (!p. p In P ==> LEADSTO2 p q Pr)))
2509       =
2510        (LEADSTO2 p q Pr)`),
2511    REPEAT STRIP_TAC THEN
2512    EQ_TAC THENL
2513      [
2514       REPEAT STRIP_TAC THENL
2515         [
2516          ACCEPT_TAC (UNDISCH (SPEC_ALL LEADSTO2_thm0))
2517         ;
2518          IMP_RES_TAC LEADSTO2_thm1
2519         ;
2520          IMP_RES_TAC LEADSTO2_thm3 THEN
2521          ASM_REWRITE_TAC []
2522         ]
2523      ;
2524       REPEAT STRIP_TAC THEN
2525       DISJ2_TAC THEN
2526       DISJ2_TAC THEN
2527       EXISTS_TAC (`\(p':'a->bool). if (p = p') then T else F`) THEN
2528       REWRITE_TAC [LUB; IN] THEN
2529       BETA_TAC THEN
2530       CONJ_TAC THENL
2531        [
2532         ACCEPT_TAC (SPEC_ALL LEADSTO_thm5_lemma2)
2533        ;
2534         REWRITE_TAC [LEADSTO_thm5_lemma3] THEN
2535         REPEAT STRIP_TAC THEN
2536         ACCEPT_TAC (ONCE_REWRITE_RULE [ASSUME (`(p:'a->bool) = p'`)] (ASSUME
2537          (`LEADSTO2 (p:'a->bool) q Pr`)))
2538        ]
2539      ]);;
2540
2541 (*
2542   Now we are able to prove another induction principle
2543 *)
2544
2545 (*
2546   We need a lemma
2547
2548 *)
2549 let LEADSTO2_thm7_lemma01 = TAC_PROOF
2550   (([],
2551   (`(!p':'a->bool.
2552       p' In P ==> LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q Pr))
2553     =
2554      ((!p'. p' In P ==> LEADSTO2 p' q Pr) /\
2555       (!p'. p' In P ==> LEADSTO2 p' q Pr ==> X p' q Pr))`)),
2556   EQ_TAC THEN
2557   REPEAT STRIP_TAC THEN
2558   RES_TAC);;
2559
2560 let LEADSTO2_thm7_lemma = TAC_PROOF
2561   (([],
2562    (`!X Pr.
2563      (!(p:'a->bool) q.
2564         ((p ENSURES q)Pr ==> X p q Pr) /\
2565         (!r.
2566           (p ENSURES r)Pr /\
2567           LEADSTO2 r q Pr /\
2568           (LEADSTO2 r q Pr ==> X r q Pr) ==>
2569           LEADSTO2 p q Pr ==>
2570           X p q Pr) /\
2571         (!P.
2572           (!p. p In P ==> LEADSTO2 p q Pr) /\
2573           (!p. p In P ==> LEADSTO2 p q Pr ==> X p q Pr) ==>
2574           LEADSTO2(LUB P)q Pr ==>
2575           X(LUB P)q Pr))
2576     =
2577      (!(p:'a->bool) q.
2578          ((p ENSURES q)Pr ==>
2579           LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q Pr)) /\
2580          (!r.
2581            (p ENSURES r)Pr /\
2582            LEADSTO2 r q Pr /\
2583            (LEADSTO2 r q Pr ==> X r q Pr) ==>
2584            LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q Pr)) /\
2585          (!P.
2586            (!p'.
2587              p' In P ==>
2588              LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q Pr)) ==>
2589            LEADSTO2(LUB P)q Pr /\ (LEADSTO2(LUB P)q Pr ==> X(LUB P)q Pr)))`)),
2590    REPEAT GEN_TAC THEN
2591    EQ_TAC THEN
2592    REPEAT STRIP_TAC THENL
2593     [
2594      IMP_RES_TAC LEADSTO2_thm0
2595     ;
2596      RES_TAC
2597     ;
2598      IMP_RES_TAC LEADSTO2_thm1
2599     ;
2600      RES_TAC
2601     ;
2602      STRIP_ASSUME_TAC (REWRITE_RULE [LEADSTO2_thm7_lemma01] (ASSUME
2603       (`!p':'a->bool. p' In P
2604          ==> LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q Pr)`))) THEN
2605      IMP_RES_TAC LEADSTO2_thm3
2606     ;
2607      STRIP_ASSUME_TAC (REWRITE_RULE [LEADSTO2_thm7_lemma01] (ASSUME
2608       (`!p':'a->bool. p' In P
2609          ==> LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q Pr)`))) THEN
2610      RES_TAC
2611     ;
2612      RES_TAC
2613     ;
2614      RES_TAC
2615     ;
2616      ASSUME_TAC (REWRITE_RULE [SYM LEADSTO2_thm7_lemma01] (CONJ
2617       (ASSUME (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr`))
2618       (ASSUME (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr ==> X p q Pr`)))) THEN
2619      RES_TAC
2620     ]);;
2621
2622 (*
2623   The induction theorem:
2624
2625   |- !X p q Pr.
2626
2627     (!p q.
2628
2629       ((p ENSURES q)Pr ==> X p q Pr) /\
2630
2631       (!r.
2632         (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\ (LEADSTO2 r q Pr ==> X r q Pr)
2633             ==> LEADSTO2 p q Pr ==> X p q Pr) /\
2634
2635       (!P.
2636         (!p. p In P ==> LEADSTO2 p q Pr) /\
2637         (!p. p In P ==> LEADSTO2 p q Pr ==> X p q Pr)
2638             ==> LEADSTO2(LUB P)q Pr ==> X(LUB P)q Pr))
2639    ==>
2640
2641     LEADSTO2 p q Pr ==> X p q Pr
2642
2643 *)
2644 let LEADSTO2_thm7 = prove_thm
2645   ("LEADSTO2_thm7",
2646    (`!X (p:'a->bool) q Pr.
2647       (!(p:'a->bool) q.
2648         ((p ENSURES q)Pr ==> X p q Pr) /\
2649         (!r. (p ENSURES r)Pr /\ (LEADSTO2 r q Pr) /\
2650              ((LEADSTO2 r q Pr) ==> X r q Pr)
2651             ==> ((LEADSTO2 p q Pr) ==> X p q Pr)) /\
2652         (!P. (!p. p In P ==> LEADSTO2 p q Pr) /\
2653              (!p.  p In P ==> LEADSTO2 p q Pr ==> X p q Pr)
2654             ==> ((LEADSTO2 (LUB P) q Pr) ==> X (LUB P) q Pr)))
2655      ==> ((LEADSTO2 p q Pr) ==> X p q Pr)`),
2656    REPEAT GEN_TAC THEN
2657    REPEAT DISCH_TAC THEN
2658    ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO2_thm7_lemma)]
2659     (BETA_RULE (SPEC
2660       (`\(p:'a->bool) q Pr. (LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q Pr))`)
2661          (REWRITE_RULE [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam]
2662            (ASSUME (`LEADSTO2 (p:'a->bool) q Pr`)))))) THEN
2663    RES_TAC);;
2664
2665 (*
2666   Finally we want to prove that LEADSTO is equal to LEADSTO2:
2667 *)
2668
2669 (*
2670   We do the proving as two implication proofs:
2671 *)
2672
2673 (*
2674   |- !R Pr.
2675     (!p q.
2676       ((p ENSURES q)Pr ==> R p q Pr) /\
2677       (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
2678       (!P. (!p. p In P ==> R p q Pr) ==> R(LUB P)q Pr))
2679    ==>
2680     (!p q.
2681       ((p ENSURES q)Pr ==> R p q Pr) /\
2682       (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2683       (!P. (!p. p In P ==> R p q Pr) ==> R(LUB P)q Pr))
2684
2685 *)
2686 let LEADSTO_EQ_LEADSTO2a = TAC_PROOF
2687   (([],
2688    (`!R (Pr:('a->'a)list).
2689        (!p q. ((p ENSURES q)Pr ==> R p q Pr) /\
2690               (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
2691               (!P. (!p. p In P ==> R p q Pr) ==> R (LUB P) q Pr))
2692             ==>
2693        (!p q. ((p ENSURES q)Pr ==> R p q Pr) /\
2694               (!r. (p ENSURES r)Pr /\ R r q Pr ==> R p q Pr) /\
2695               (!P. (!p. p In P ==> R p q Pr) ==> R (LUB P) q Pr))`)),
2696    REPEAT STRIP_TAC THEN
2697    RES_TAC);;
2698
2699 (*
2700   |- !p q Pr. LEADSTO2 p q Pr ==> (p LEADSTO q)Pr
2701 *)
2702 let LEADSTO_EQ_LEADSTO2b_lemma = TAC_PROOF
2703   (([],
2704    (`(!(p:'a->bool) q.
2705         ((p ENSURES q)Pr ==> R p q Pr) /\
2706         (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
2707         (!P. (p = LUB P) /\ (!p'. p' In P ==> R p' q Pr) ==> R p q Pr))
2708    ==>
2709     (!p q.
2710         ((p ENSURES q)Pr ==> R p q Pr) /\
2711         (!r. R p r Pr /\ R r q Pr ==> R p q Pr) /\
2712         (!P. (!p'. p' In P ==> R p' q Pr) ==> R (LUB P) q Pr))`)),
2713    REPEAT STRIP_TAC THEN
2714    RES_TAC THEN
2715    ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
2716     (`!p:'a->bool. (p = LUB P) ==> R p (q:'a->bool) (Pr:('a->'a)list)`)))));;
2717
2718 let LEADSTO_EQ_LEADSTO2b = TAC_PROOF
2719   (([],
2720    (`!(p:'a->bool) q Pr. LEADSTO2 p q Pr ==> (p LEADSTO q) Pr`)),
2721    REWRITE_TAC [LEADSTO;  LeadstoRel;
2722                 LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam] THEN
2723    REPEAT STRIP_TAC THEN
2724    ASSUME_TAC (UNDISCH (SPEC_ALL LEADSTO_EQ_LEADSTO2b_lemma)) THEN
2725    ASSUME_TAC (UNDISCH (SPEC_ALL LEADSTO_EQ_LEADSTO2a)) THEN
2726    RES_TAC);;
2727
2728 (*
2729  |- (!p' q'.
2730       ((p' ENSURES q')Pr ==> LEADSTO2 p' q' Pr) /\
2731       (!r. LEADSTO2 p' r Pr /\ LEADSTO2 r q' Pr ==> LEADSTO2 p' q' Pr) /\
2732       (!P. (p' = LUB P) /\
2733            (!p''. p'' In P ==> LEADSTO2 p'' q' Pr) ==> LEADSTO2 p' q' Pr))
2734      ==>
2735       (p LEADSTO q)Pr ==> LEADSTO2 p q Pr
2736 *)
2737 let LEADSTO_EQ_LEADSTO2c = (SPECL
2738   [(`LEADSTO2:('a->bool)->('a->bool)->(('a->'a)list)->bool`);
2739    (`p:'a->bool`); (`q:'a->bool`); (`Pr:('a->'a)list`)] LEADSTO_thm21);;
2740
2741 (*
2742   |- !p q Pr. (p LEADSTO q)Pr ==> LEADSTO2 p q Pr
2743 *)
2744 let LEADSTO_EQ_LEADSTO2d =
2745    (GEN_ALL (REWRITE_RULE [LEADSTO2_thm0; LEADSTO2_thm2; LEADSTO2_thm3a]
2746                            LEADSTO_EQ_LEADSTO2c));;
2747
2748 (*
2749   The equivalence proof:
2750
2751   |- !p q Pr. (p LEADSTO q)Pr = LEADSTO2 p q Pr
2752
2753 *)
2754 let LEADSTO_EQ_LEADSTO2 = prove_thm
2755   ("LEADSTO_EQ_LEADSTO2",
2756    (`!(p:'a->bool) q Pr. (p LEADSTO q)Pr = LEADSTO2 p q Pr`),
2757    REPEAT GEN_TAC THEN
2758    EQ_TAC THENL
2759     [
2760      REWRITE_TAC [LEADSTO_EQ_LEADSTO2d]
2761     ;
2762      REWRITE_TAC [LEADSTO_EQ_LEADSTO2b]
2763     ]);;
2764
2765 (*
2766   Hence now we may conclude all theorems proven valid for both relations
2767 *)
2768
2769 (*
2770   We get the last two induction principles for LEADSTO:
2771 *)
2772
2773 (*
2774   |- !X p q Pr.
2775
2776     (!p q.
2777
2778       ((p ENSURES q)Pr ==> X p q Pr) /\
2779
2780       (!r. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
2781
2782       (!P. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr)) ==>
2783
2784    ==>
2785
2786     (p LEADSTO q)Pr ==> X p q Pr
2787 *)
2788 let LEADSTO_thm31 = prove_thm
2789    ("LEADSTO_thm31",
2790     (`!X (p:'a->bool) q Pr.
2791       (!p q.
2792         ((p ENSURES q)Pr ==> X p q Pr) /\
2793         (!r. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
2794         (!P. (!p. p In P ==> X p q Pr) ==> X (LUB P) q Pr))
2795      ==>
2796       (p LEADSTO q)Pr ==> X p q Pr`),
2797     ACCEPT_TAC (REWRITE_RULE
2798      [SYM (SPEC_ALL LEADSTO_EQ_LEADSTO2)] LEADSTO2_thm8));;
2799
2800 (*
2801   The theorem may also be written:
2802 *)
2803 let LEADSTO_thm32 = prove_thm
2804  ("LEADSTO_thm32",
2805   (`!X.
2806     (!p q Pr.   (p ENSURES q)Pr ==> X p q Pr) /\
2807     (!p r q Pr. (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr) /\
2808     (!P q Pr. (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr)
2809    ==>
2810      !(p:'a->bool) q Pr. (p LEADSTO q)Pr ==> X p q Pr`),
2811   REPEAT STRIP_TAC THEN
2812   ASSUME_TAC (REWRITE_RULE
2813    [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
2814     ASSUME (`!(p:'a->bool) (r:'a->bool) (q:'a->bool) Pr.
2815               (p ENSURES r)Pr /\ X r q Pr ==> X p q Pr`);
2816     ASSUME (`!(P:('a->bool)->bool) (q:'a->bool) (Pr:('a->'a)list).
2817               (!p. p In P ==> X p q Pr) ==> X(LUB P)q Pr`)]
2818      (SPEC_ALL LEADSTO_thm31)) THEN
2819   RES_TAC);;
2820
2821
2822 (*
2823   |- !X p q Pr.
2824
2825     (!p q.
2826
2827       ((p ENSURES q)Pr ==> X p q Pr) /\
2828
2829       (!r.
2830         (p ENSURES r)Pr /\
2831         (r LEADSTO q)Pr /\
2832         ((r LEADSTO q)Pr ==> X r q Pr)
2833            ==> (p LEADSTO q)Pr ==> X p q Pr) /\
2834
2835       (!P.
2836         (!p. p In P ==> (p LEADSTO q)Pr) /\
2837         (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
2838            ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))
2839
2840     ==>
2841
2842     (p LEADSTO q)Pr ==> X p q Pr
2843 *)
2844 let LEADSTO_thm33 = prove_thm
2845   ("LEADSTO_thm33",
2846    (`!X (p:'a->bool) q Pr.
2847     (!p q.
2848       ((p ENSURES q)Pr ==> X p q Pr) /\
2849       (!r.
2850         (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\
2851         ((r LEADSTO q)Pr ==> X r q Pr) ==>
2852         (p LEADSTO q)Pr ==> X p q Pr) /\
2853       (!P.
2854         (!p. p In P ==> (p LEADSTO q)Pr) /\
2855         (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
2856         ((LUB P) LEADSTO q)Pr ==> X (LUB P) q Pr))
2857       ==>
2858         (p LEADSTO q)Pr ==> X p q Pr`),
2859    ACCEPT_TAC (REWRITE_RULE
2860      [SYM (SPEC_ALL LEADSTO_EQ_LEADSTO2)] LEADSTO2_thm7));;
2861
2862 (*
2863   We may now derive the theorem:
2864 *)
2865 let LEADSTO_thm34 = prove_thm
2866   ("LEADSTO_thm34",
2867    (`!X.
2868     (!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
2869     (!p r q Pr.
2870         (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\
2871         ((r LEADSTO q)Pr ==> X r q Pr) ==>
2872         (p LEADSTO q)Pr ==> X p q Pr) /\
2873     (!P q Pr.
2874       (!p. p In P ==> (p LEADSTO q)Pr) /\
2875       (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
2876       ((LUB P) LEADSTO q)Pr ==> X (LUB P) q Pr)
2877       ==>
2878         !(p:'a->bool) q Pr. (p LEADSTO q)Pr ==> X p q Pr`),
2879   REPEAT STRIP_TAC THEN
2880   ASSUME_TAC (REWRITE_RULE
2881    [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
2882     ASSUME (`!(p:'a->bool) r q Pr. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\
2883         ((r LEADSTO q)Pr ==> X r q Pr) ==> (p LEADSTO q)Pr ==> X p q Pr`);
2884     ASSUME (`!(P:('a->bool)->bool) q Pr.
2885         (!p. p In P ==> (p LEADSTO q)Pr) /\
2886         (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
2887         ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr`)]
2888      (SPEC_ALL LEADSTO_thm33)) THEN
2889   RES_TAC);;
2890
2891
2892 (*
2893   And the theorem:
2894
2895   |- !X Pr.
2896
2897     (!p q. (p ENSURES q)Pr ==> X p q Pr) /\
2898
2899     (!p r q.
2900       (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr
2901                            ==> X p q Pr) /\
2902
2903     (!P q.
2904       (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
2905                            ==> X(LUB P)q Pr)
2906
2907    ==>
2908
2909     (!p q. (p LEADSTO q)Pr ==> X p q Pr)
2910
2911   which may be used for deriving a tactic supporting given programs.
2912 *)
2913 let LEADSTO_thm34a_lemma1 = TAC_PROOF
2914   (([],
2915    (`!P q Pr. (!p:'a->bool. p In P ==> (p LEADSTO q)Pr) ==>
2916        (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
2917           ==> (!p. p In P ==> X p q Pr)`)),
2918    REPEAT STRIP_TAC THEN
2919    RES_TAC THEN
2920    RES_TAC);;
2921
2922 let LEADSTO_thm34a_lemma2 = TAC_PROOF
2923   (([],
2924    (`!P q Pr. (!p:'a->bool. p In P ==> (p LEADSTO q)Pr) ==>
2925                    (!p. p In P ==> X p q Pr) ==>
2926                        (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)`)),
2927    REPEAT STRIP_TAC THEN
2928    RES_TAC);;
2929
2930 let LEADSTO_thm34a_lemma3 = TAC_PROOF
2931   (([],
2932    (`((!(p:'a->bool) q. (p ENSURES q)Pr ==> X p q Pr) /\
2933        (!p r q.
2934          (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==> X p q Pr) /\
2935        (!P q.
2936          (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
2937          X(LUB P)q Pr))
2938      =
2939     (!p q.
2940      ((p ENSURES q)Pr ==> X p q Pr) /\
2941      (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
2942                       ==> (p LEADSTO q)Pr ==> X p q Pr) /\
2943      (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\
2944           (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr)
2945                       ==> ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr))`)),
2946    EQ_TAC THEN
2947    REPEAT STRIP_TAC THENL
2948     [
2949      RES_TAC
2950     ;
2951      RES_TAC
2952     ;
2953      ASSUME_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO_thm34a_lemma1)) THEN
2954      RES_TAC
2955     ;
2956      RES_TAC
2957     ;
2958      IMP_RES_TAC LEADSTO_thm2 THEN
2959      ACCEPT_TAC (REWRITE_RULE
2960       [ASSUME (`((p:'a->bool) ENSURES r)Pr`);
2961        ASSUME (`((r:'a->bool) LEADSTO q)Pr`);
2962        ASSUME (`(X:('a->bool)->('a->bool)->('a->'a)list->bool) r q Pr`);
2963        ASSUME (`((p:'a->bool) LEADSTO q)Pr`)]
2964       (SPEC_ALL (CONJUNCT1 (CONJUNCT2 (SPEC_ALL (ASSUME
2965         (`!(p:'a->bool) q.
2966         ((p ENSURES q)Pr ==> X p q Pr) /\
2967         (!r.
2968           (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
2969              ==> (p LEADSTO q)Pr ==> X p q Pr) /\
2970         (!P.
2971           (!p. p In P ==> (p LEADSTO q)Pr) /\
2972           (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
2973           ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr)`)))))))
2974     ;
2975      IMP_RES_TAC LEADSTO_thm3a THEN
2976      ASSUME_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO_thm34a_lemma2)) THEN
2977      ACCEPT_TAC (REWRITE_RULE
2978       [ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr`);
2979        ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr ==> X p q Pr`);
2980        ASSUME (`((LUB (P:('a->bool)->bool)) LEADSTO q)Pr`)]
2981       (SPEC_ALL (CONJUNCT2 (CONJUNCT2 (SPEC_ALL (ASSUME
2982         (`!(p:'a->bool) q.
2983         ((p ENSURES q)Pr ==> X p q Pr) /\
2984         (!r.
2985           (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ ((r LEADSTO q)Pr ==> X r q Pr)
2986              ==> (p LEADSTO q)Pr ==> X p q Pr) /\
2987         (!P.
2988           (!p. p In P ==> (p LEADSTO q)Pr) /\
2989           (!p. p In P ==> (p LEADSTO q)Pr ==> X p q Pr) ==>
2990           ((LUB P) LEADSTO q)Pr ==> X(LUB P)q Pr)`)))))))
2991     ]);;
2992
2993 (*
2994   The theorem for the tactic
2995 *)
2996 let LEADSTO_thm34a = prove_thm
2997   ("LEADSTO_thm34a",
2998    (`!X Pr.
2999     (!p q. (p ENSURES q)Pr ==> X p q Pr) /\
3000     (!p r q.
3001         (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr
3002           ==> X p q Pr) /\
3003     (!P q.
3004       (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
3005           ==> X (LUB P) q Pr)
3006       ==>
3007         !(p:'a->bool) q. (p LEADSTO q)Pr ==> X p q Pr`),
3008   REPEAT GEN_TAC THEN
3009   STRIP_TAC THEN
3010   REPEAT GEN_TAC THEN
3011   ACCEPT_TAC (REWRITE_RULE
3012    [ASSUME (`!(p:'a->bool) q. (p ENSURES q)Pr ==> X p q Pr`);
3013     ASSUME (`!(p:'a->bool) r q.
3014         (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==> X p q Pr`);
3015     ASSUME (`!P (q:'a->bool).
3016         (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr) ==>
3017         X(LUB P)q Pr`)]
3018      (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm34a_lemma3)]
3019        (SPEC_ALL LEADSTO_thm33))));;
3020
3021 let LEADSTO_thm34b = prove_thm
3022   ("LEADSTO_thm34b",
3023    (`!X:('a->bool)->('a->bool)->('a->'a)list->bool.
3024     (!p q st Pr. (p ENSURES q)(CONS st Pr) ==> X p q (CONS st Pr)) /\
3025     (!p r q st Pr.
3026         (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr) /\
3027          X r q (CONS st Pr)
3028           ==> X p q (CONS st Pr)) /\
3029     (!P q st Pr.
3030       (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) /\
3031       (!p. p In P ==> X p q (CONS st Pr))
3032           ==> X (LUB P) q (CONS st Pr))
3033       ==>
3034         !p q st Pr. (p LEADSTO q)(CONS st Pr) ==> X p q (CONS st Pr)`),
3035    REPEAT STRIP_TAC THEN
3036    ACCEPT_TAC (REWRITE_RULE [ASSUME (`((p:'a->bool) LEADSTO q)(CONS st Pr)`)]
3037    (SPEC_ALL (REWRITE_RULE
3038     [ASSUME
3039       (`!(p:'a->bool) q st Pr. (p ENSURES q)(CONS st Pr) ==> X p q(CONS st Pr)`);
3040      ASSUME (`!(p:'a->bool) r q st Pr.
3041         (p ENSURES r)(CONS st Pr) /\ (r LEADSTO q)(CONS st Pr) /\
3042         X r q(CONS st Pr) ==> X p q(CONS st Pr)`);
3043      ASSUME (`!P (q:'a->bool) st Pr.
3044         (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) /\
3045         (!p. p In P ==> X p q(CONS st Pr)) ==> X(LUB P)q(CONS st Pr)`)]
3046       (SPECL [(`X:('a->bool)->('a->bool)->('a->'a)list->bool`); (`CONS (st:'a->'a) Pr`)]
3047               LEADSTO_thm34a)))));;
3048
3049 (*
3050   Now we may introduce some tactics for supporting structural induction
3051   of leadsto relations:
3052 *)
3053 (* use"leadsto_induct0.sml";; *)
3054 (*
3055 |- !X st Pr.
3056     (!p q.   (p ENSURES q)(CONS st Pr) ==> X p q(CONS st Pr)) /\
3057     (!p r q. (p ENSURES r)(CONS st Pr) /\
3058              (r LEADSTO q)(CONS st Pr) /\ X r q(CONS st Pr)
3059                                        ==> X p q(CONS st Pr)) /\
3060     (!P q.   (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) /\
3061              (!p. p In P ==> X p q(CONS st Pr))
3062                                        ==> X (LUB P) q (CONS st Pr))
3063
3064     ==> (!p q. (p LEADSTO q)(CONS st Pr) ==> X p q(CONS st Pr))
3065 *)
3066
3067 let LEADSTO_thm34a_lemma00 = TAC_PROOF
3068   (([],
3069     `!(p:'a->bool) q Pr X.
3070        (!p q. (p ENSURES q) Pr ==> X p q Pr) /\
3071        (!p r q.
3072             (p ENSURES r) Pr /\ (r LEADSTO q) Pr /\ X r q Pr ==> X p q Pr) /\
3073        (!P q.
3074             (!p. p In P ==> (p LEADSTO q) Pr) /\ (!p. p In P ==> X p q Pr)
3075             ==> X (LUB P) q Pr)
3076        ==> ((p LEADSTO q) Pr ==> X p q Pr)`),
3077    REPEAT STRIP_TAC THEN
3078    IMP_RES_TAC (SPEC_ALL LEADSTO_thm34a));;
3079
3080 let LEADSTO_thm34a_lemma01 = GENL
3081   [`p:'a->bool`;`q:'a->bool`;`st:'a->'a`;`Pr:('a->'a)list`;
3082    `X:('a->bool)->('a->bool)->('a->'a)list->bool`]
3083   (SPECL [`p:'a->bool`;`q:'a->bool`;`(CONS st Pr):('a->'a)list`;
3084      `X:('a->bool)->('a->bool)->('a->'a)list->bool`] LEADSTO_thm34a_lemma00);;
3085
3086 (*
3087  Prove:
3088   |- !p q st Pr.
3089        (p ENSURES q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) /\
3090        (q UNLESS r)(CONS st Pr) /\ (q' UNLESS r)(CONS st Pr)
3091           ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)
3092 *)
3093 let LEADSTO_thm35_lemma00 = TAC_PROOF
3094   (([],
3095    (`!(p:'a->bool) q r st Pr.
3096      (p ENSURES q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) /\
3097      (q UNLESS r)(CONS st Pr) /\ (q' UNLESS r)(CONS st Pr)
3098          ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)`)),
3099    REPEAT STRIP_TAC THEN
3100    ASSUME_TAC (MP (SPECL
3101     [(`p:'a->bool`); (`q:'a->bool`);
3102      (`(CONS st Pr):('a->'a)list`)] ENSURES_cor2)
3103        (ASSUME (`((p:'a->bool) ENSURES q)(CONS st Pr)`))) THEN
3104    ASSUME_TAC (MP (SPECL
3105     [(`p:'a->bool`); (`q:'a->bool`); (`r:'a->bool`);
3106      (`(CONS st Pr):('a->'a)list`)]
3107      UNLESS_thm8)
3108       (CONJ (MP (SPECL [(`p:'a->bool`); (`q:'a->bool`);
3109                         (`(CONS st Pr):('a->'a)list`)]
3110                         ENSURES_cor2)
3111         (ASSUME (`((p:'a->bool) ENSURES q)(CONS st Pr)`)))
3112         (ASSUME (`((q:'a->bool) UNLESS r)(CONS st Pr)`)))) THEN
3113    ASSUME_TAC (MP (SPECL
3114      [(`p':'a->bool`); (`q':'a->bool`);
3115       (`(p:'a->bool) \/* q`); (`r:'a->bool`);
3116       (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm29) (CONJ
3117         (ASSUME (`((p':'a->bool) LEADSTO q')(CONS st Pr)`))
3118         (ASSUME (`(((p:'a->bool) \/* q) UNLESS r)(CONS st Pr)`)))) THEN
3119    ASSUME_TAC (MP (SPECL [(`p:'a->bool`); (`(p:'a->bool) \/* q`);
3120                           (`p':'a->bool`)] IMPLY_WEAK_AND_lemma)
3121               (SPECL [(`p:'a->bool`);
3122                       (`q:'a->bool`)] OR_IMPLY_WEAK_lemma)) THEN
3123    ASSUME_TAC (MP (SPECL
3124      [(`(p:'a->bool) /\* p'`); (`(p':'a->bool) /\* (p \/* q)`);
3125         (`st:'a->'a`);
3126         (`Pr:('a->'a)list`)] LEADSTO_thm25) (ONCE_REWRITE_RULE
3127       [(SPECL [(`(p:'a->bool) \/* q`);
3128                (`p':'a->bool`)] AND_COMM_lemma)]
3129        (ASSUME (`!s:'a. (p /\* p')s ==>
3130                           ((p \/* q) /\* p')s`)))) THEN
3131    ASSUME_TAC (MP (SPECL
3132     [(`(p:'a->bool) /\* p'`); (`(p':'a->bool) /\* (p \/* q)`);
3133      (`((q':'a->bool) /\* (p \/* q)) \/* r`);
3134      (`CONS (st:'a->'a) Pr`)] LEADSTO_thm1)
3135                (CONJ
3136        (ASSUME (`(((p:'a->bool) /\* p') LEADSTO
3137                     (p' /\* (p \/* q)))(CONS st Pr)`))
3138        (ASSUME (`((p' /\* (p \/* q)) LEADSTO
3139                     ((q' /\* (p \/* q)) \/* r))
3140                 (CONS (st:'a->'a) Pr)`)))) THEN
3141    ASSUME_TAC (MP (SPECL
3142     [(`p:'a->bool`); (`q:'a->bool`);
3143      (`q':'a->bool`); (`r:'a->bool`);
3144      (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm29)
3145       (CONJ (MP (SPECL [(`p:'a->bool`); (`q:'a->bool`);
3146                         (`CONS (st:'a->'a) Pr`)]
3147                         LEADSTO_thm0)
3148         (ASSUME (`((p:'a->bool) ENSURES q)(CONS st Pr)`)))
3149         (ASSUME (`((q':'a->bool) UNLESS r)(CONS st Pr)`)))) THEN
3150    ASSUME_TAC (ONCE_REWRITE_RULE [SPECL
3151     [(`((q':'a->bool) /\* q) \/* r`);
3152      (`p:'a->bool`); (`q':'a->bool`)]
3153      OR_AND_COMM_lemma] (ONCE_REWRITE_RULE [SPECL
3154       [(`(q':'a->bool) /\* p`); (`((q':'a->bool) /\* q) \/* r`)]
3155        OR_COMM_lemma] (REWRITE_RULE [OR_ASSOC_lemma]
3156       (REWRITE_RULE [AND_OR_DISTR_lemma] (ASSUME
3157          (`(((p:'a->bool) /\* p') LEADSTO
3158            ((q' /\* (p \/* q)) \/* r))(CONS st Pr)`)))))) THEN
3159    ACCEPT_TAC (ONCE_REWRITE_RULE [OR_COMM_lemma] (REWRITE_RULE [OR_OR_lemma]
3160     (REWRITE_RULE [OR_ASSOC_lemma] (ONCE_REWRITE_RULE[OR_AND_COMM_lemma]
3161     (REWRITE_RULE [OR_OR_lemma] (REWRITE_RULE [SYM (SPEC_ALL OR_ASSOC_lemma)]
3162     (ONCE_REWRITE_RULE [OR_COMM_lemma] (REWRITE_RULE [OR_ASSOC_lemma]
3163     (ONCE_REWRITE_RULE [OR_OR_COMM_lemma] (MP (SPECL
3164       [(`(p:'a->bool) /\* p'`); (`((q':'a->bool) /\* q) \/* r`);
3165        (`(p:'a->bool) /\* q'`); (`((q:'a->bool) /\* q') \/* r`);
3166        (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm28) (CONJ
3167        (ASSUME (`((p /\* p') LEADSTO
3168                     (((q' /\* q) \/* r) \/* (p /\* q')))
3169                    (CONS (st:'a->'a) Pr)`))
3170        (ASSUME (`((p /\* q') LEADSTO ((q /\* q') \/* r))
3171                    (CONS (st:'a->'a) Pr)`))))))))))))));;
3172
3173
3174 let LEADSTO_thm35_lemma01_1 = TAC_PROOF
3175   (([],
3176    (`!(q:'a->bool) (q':'a->bool) r'' p r s.
3177         ((((q /\* q') \/* r'') \/* (p /\* r)) \/* ((q' /\* q) \/* r''))s =
3178         (((q /\* q') \/* r'') \/* (p /\* r))s`)),
3179    REWRITE_TAC [OR_def; AND_def] THEN
3180    BETA_TAC THEN
3181    REPEAT GEN_TAC THEN
3182    EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []);;
3183
3184 let LEADSTO_thm35_lemma01_2 =
3185     GEN_ALL (REWRITE_RULE [ETA_AX] (MK_ABS (GEN (`s:'a`) (SPEC_ALL
3186       LEADSTO_thm35_lemma01_1))));;
3187
3188 let LEADSTO_thm35_lemma01_3 = TAC_PROOF
3189   (([],
3190    (`(!p:'a->bool. p In P ==>
3191         (!p'' q r r'.
3192           (r LEADSTO q)(CONS st Pr) ==>
3193           (p'' ENSURES r)(CONS st Pr) ==>
3194           (q' UNLESS r')(CONS st Pr) ==>
3195           (q UNLESS r')(CONS st Pr) ==>
3196           (!p' q' r''.
3197             (p' LEADSTO q')(CONS st Pr) ==>
3198             (q UNLESS r'')(CONS st Pr) ==>
3199             (q' UNLESS r'')(CONS st Pr) ==>
3200             ((r /\* p') LEADSTO ((q /\* q') \/* r''))(CONS st Pr)) ==>
3201           ((p'' /\* p) LEADSTO ((q /\* q') \/* r'))(CONS st Pr)))
3202       ==>
3203       (!p'' q r r'.
3204           (r LEADSTO q)(CONS st Pr) ==>
3205           (p'' ENSURES r)(CONS st Pr) ==>
3206           (q' UNLESS r')(CONS st Pr) ==>
3207           (q UNLESS r')(CONS st Pr) ==>
3208           (!p' q' r''.
3209             (p' LEADSTO q')(CONS st Pr) ==>
3210             (q UNLESS r'')(CONS st Pr) ==>
3211             (q' UNLESS r'')(CONS st Pr) ==>
3212             ((r /\* p') LEADSTO ((q /\* q') \/* r''))(CONS st Pr)) ==>
3213           (!p. p In P ==>
3214                  ((p'' /\* p) LEADSTO ((q /\* q') \/* r'))(CONS st Pr)))`)),
3215    REPEAT STRIP_TAC THEN
3216    RES_TAC);;
3217
3218 let LEADSTO_thm35_lemma01_4 = TAC_PROOF
3219   (([],
3220    (`!(P:('a->bool)->bool) r q st Pr.
3221     (!p. p In P ==> ((p /\* r) LEADSTO q)(CONS st Pr)) ==>
3222     (!p. p In P ==> (p LEADSTO q)(CONS st Pr)) ==>
3223     (((LUB P) /\* r) LEADSTO q)(CONS st Pr)`)),
3224    REPEAT STRIP_TAC THEN
3225    IMP_RES_TAC LEADSTO_thm3a THEN
3226    ASSUME_TAC (SPECL
3227     [(`LUB (P:('a->bool)->bool)`); (`r:'a->bool`)] SYM_AND_IMPLY_WEAK_lemma) THEN
3228    ASSUME_TAC (UNDISCH (SPEC_ALL (SPECL
3229     [(`(LUB P) /\* (r:'a->bool)`); (`(LUB P):'a->bool`)] ENSURES_cor1))) THEN
3230    IMP_RES_TAC LEADSTO_thm0 THEN
3231    IMP_RES_TAC LEADSTO_thm1);;
3232
3233 let LEADSTO_thm35_lemma01_5 = TAC_PROOF
3234   (([],
3235    (`!(p':'a->bool) P p (p'':'a->bool).
3236       p' In (\p''. ?p'''. p''' In P /\ (p'' = p /\* p'''))
3237      =
3238       (?p'''. p''' In P /\ (p' = p /\* p'''))`)),
3239    REWRITE_TAC [IN] THEN
3240    BETA_TAC THEN
3241    REWRITE_TAC []);;
3242
3243 let LEADSTO_thm35_lemma01_6 = TAC_PROOF
3244   (([],
3245    (`!s:'a.
3246       (p /\* (LUB P))s =
3247       (LUB(\p''. ?p'. p' In P /\ (p'' = p /\* p')))s`)),
3248    REPEAT GEN_TAC THEN
3249    REWRITE_TAC [LUB; AND_def] THEN
3250    BETA_TAC THEN
3251    EQ_TAC THEN
3252    REPEAT STRIP_TAC THENL
3253     [
3254      EXISTS_TAC (`\s:'a. p s /\ p' s`) THEN
3255      BETA_TAC THEN
3256      ASM_REWRITE_TAC [] THEN
3257      EXISTS_TAC (`p':'a->bool`) THEN
3258      ASM_REWRITE_TAC [IN]
3259     ;
3260      STRIP_ASSUME_TAC (BETA_RULE (SUBS
3261         [ASSUME (`p' = (\s:'a. p s /\ p'' s)`)]
3262            (ASSUME (`(p':'a->bool) s`))))
3263     ;
3264      EXISTS_TAC (`p'':'a->bool`) THEN
3265      REWRITE_TAC [REWRITE_RULE [IN] (ASSUME (`(p'':'a->bool) In P`))] THEN
3266      STRIP_ASSUME_TAC (BETA_RULE (SUBS
3267         [ASSUME (`p' = (\s:'a. p s /\ p'' s)`)]
3268                                   (ASSUME (`(p':'a->bool) s`))))
3269     ]);;
3270
3271 let LEADSTO_thm35_lemma01_7 = TAC_PROOF
3272   (([],
3273    (`!(P:('a->bool)->bool) r' q q' st Pr.
3274     (!p'. p' In P ==> ((p /\* p') LEADSTO ((q /\* q') \/* r'))(CONS st Pr))
3275       ==>
3276         (!p'. (?p'''. p''' In P /\ (p' = p /\* p''')) ==>
3277                              (p' LEADSTO ((q /\* q') \/* r'))(CONS st Pr))`)),
3278    REPEAT STRIP_TAC THEN
3279    RES_TAC THEN
3280    ASM_REWRITE_TAC []);;
3281
3282 let LEADSTO_thm35_lemma01_8 = TAC_PROOF
3283   (([],
3284    (`!(P:('a->bool)->bool) r' q q' st Pr.
3285        (!p'.
3286         p' In P ==> ((p /\* p') LEADSTO ((q /\* q') \/* r'))(CONS st Pr))
3287           ==> (((p /\* (LUB P)) LEADSTO ((q /\* q') \/* r'))(CONS st Pr))`)),
3288    REPEAT STRIP_TAC THEN
3289    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm35_lemma01_5] (SPECL
3290      [(`\p'':'a->bool. ?p'. p' In P /\ (p'' = (p /\* p'))`);
3291       (`(q /\* q') \/* (r':'a->bool)`); (`CONS (st:'a->'a) Pr`)]
3292      LEADSTO_thm3a)) THEN
3293    ASSUME_TAC (REWRITE_RULE [(UNDISCH (SPEC_ALL LEADSTO_thm35_lemma01_7))]
3294       (ASSUME (`(!p':'a->bool.
3295          (?p'''. p''' In P /\ (p' = p /\* p''')) ==>
3296          (p' LEADSTO ((q /\* q') \/* r'))(CONS st Pr)) ==>
3297        ((LUB(\p''. ?p'. p' In P /\ (p'' = p /\* p'))) LEADSTO
3298         ((q /\* q') \/* r'))
3299        (CONS st Pr)`))) THEN
3300    ASM_REWRITE_TAC [REWRITE_RULE [ETA_AX] (MK_ABS LEADSTO_thm35_lemma01_6)]);;
3301
3302 let LEADSTO_thm35_lemma01_9 = TAC_PROOF
3303   (([],
3304    (`(!p:'a->bool.
3305         p In P ==>
3306         (!p' q' r.
3307           (p' LEADSTO q')(CONS st Pr) ==>
3308           (q UNLESS r)(CONS st Pr) ==>
3309           (q' UNLESS r)(CONS st Pr) ==>
3310           ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)))
3311      ==>
3312      ((!p' q' r.
3313           (p' LEADSTO q')(CONS st Pr) ==>
3314           (q UNLESS r)(CONS st Pr) ==>
3315           (q' UNLESS r)(CONS st Pr) ==>
3316        (!p. p In P ==>
3317           ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr))))`)),
3318    REPEAT STRIP_TAC THEN
3319    RES_TAC);;
3320
3321 let LEADSTO_thm35_lemma01_10 = TAC_PROOF
3322   (([],
3323   (`(!p:'a->bool. p In P ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr))
3324       ==>
3325     (!p. p In P ==> ((p' /\* p) LEADSTO ((q /\* q') \/* r))(CONS st Pr))`)),
3326    REPEAT STRIP_TAC THEN
3327    RES_TAC THEN
3328    ONCE_REWRITE_TAC [SPECL [(`p':'a->bool`); (`p:'a->bool`)] AND_COMM_lemma] THEN
3329    ONCE_REWRITE_TAC [AND_COMM_OR_lemma] THEN
3330    ASM_REWRITE_TAC []);;
3331
3332 let LEADSTO_thm35_lemma01a = TAC_PROOF
3333   (([],
3334    (`(!(p:'a->bool) q r'' r'.
3335         (r'' LEADSTO q)(CONS st Pr) ==>
3336         (p ENSURES r'')(CONS st Pr) ==>
3337         (q' UNLESS r')(CONS st Pr) ==>
3338         (q UNLESS r')(CONS st Pr) ==>
3339         (!p' q' r'.
3340           (p' LEADSTO q')(CONS st Pr) ==>
3341           (q UNLESS r')(CONS st Pr) ==>
3342           (q' UNLESS r')(CONS st Pr) ==>
3343           ((r'' /\* p') LEADSTO ((q /\* q') \/* r'))(CONS st Pr)) ==>
3344         ((p /\* r) LEADSTO ((q /\* q') \/* r'))(CONS st Pr))
3345        ==>
3346         (!(p:'a->bool) q r' r''.
3347         (r' LEADSTO q)(CONS st Pr) ==>
3348         (p ENSURES r')(CONS st Pr) ==>
3349         (q' UNLESS r'')(CONS st Pr) ==>
3350         (q UNLESS r'')(CONS st Pr) ==>
3351         (!p' q' r''.
3352           (p' LEADSTO q')(CONS st Pr) ==>
3353           (q UNLESS r'')(CONS st Pr) ==>
3354           (q' UNLESS r'')(CONS st Pr) ==>
3355           ((r' /\* p') LEADSTO ((q /\* q') \/* r''))(CONS st Pr)) ==>
3356         ((p /\* r) LEADSTO ((q /\* q') \/* r''))(CONS st Pr))`)),
3357
3358   REPEAT STRIP_TAC THEN
3359   RES_TAC THEN
3360   ASM_REWRITE_TAC[]
3361 );;
3362
3363 (*
3364    Now we define a tactic that given one of the LEADSTO induction
3365    theorems can be used as a tactic to prove properties that require
3366    structural induction to prove the required propertie
3367 *)
3368 let LEADSTO_INDUCT0_TAC : tactic =
3369 (
3370   try
3371     MATCH_MP_TAC LEADSTO_thm34b THEN REPEAT CONJ_TAC
3372   with Failure _ -> failwith "LEADSTO_INDUCT0_TAC Failed"
3373 );;
3374
3375 let LEADSTO_thm35_lemma01 = TAC_PROOF
3376   (([],
3377    (`!(p:'a->bool) q st Pr.
3378      (p LEADSTO q)(CONS st Pr) ==>
3379        !p' q' r. (p' LEADSTO q')(CONS st Pr)
3380            ==> (q UNLESS r)(CONS st Pr) ==> (q' UNLESS r)(CONS st Pr)
3381                   ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)`)),
3382    LEADSTO_INDUCT0_TAC THENL
3383    [
3384      REPEAT STRIP_TAC THEN
3385      IMP_RES_TAC LEADSTO_thm35_lemma00
3386     ;
3387      REPEAT STRIP_TAC THEN
3388      UNDISCH_TAC (`!(p':'a->bool) q' r'.
3389         (p' LEADSTO q')(CONS st Pr) ==>
3390         (q UNLESS r')(CONS st Pr) ==>
3391         (q' UNLESS r')(CONS st Pr) ==>
3392         ((r /\* p') LEADSTO ((q /\* q') \/* r'))(CONS st Pr)`) THEN
3393      UNDISCH_TAC (`((q:'a->bool) UNLESS r')(CONS st Pr)`) THEN
3394      UNDISCH_TAC (`((q':'a->bool) UNLESS r')(CONS st Pr)`) THEN
3395      UNDISCH_TAC (`((p:'a->bool) ENSURES r)(CONS st Pr)`) THEN
3396      UNDISCH_TAC (`((r:'a->bool) LEADSTO q)(CONS st Pr)`) THEN
3397      SPEC_TAC ((`r':'a->bool`), (`r':'a->bool`)) THEN
3398      SPEC_TAC ((`r:'a->bool`), (`r:'a->bool`)) THEN
3399      SPEC_TAC ((`q:'a->bool`), (`q:'a->bool`)) THEN
3400      SPEC_TAC ((`p:'a->bool`), (`p:'a->bool`)) THEN
3401      UNDISCH_TAC (`((p':'a->bool) LEADSTO q')(CONS st Pr)`) THEN
3402      SPEC_TAC ((`Pr:('a->'a)list`), (`Pr:('a->'a)list`)) THEN
3403      SPEC_TAC ((`st:'a->'a`), (`st:'a->'a`)) THEN
3404      SPEC_TAC ((`q':'a->bool`), (`q':'a->bool`)) THEN
3405      SPEC_TAC ((`p':'a->bool`), (`p':'a->bool`)) THEN
3406      LEADSTO_INDUCT0_TAC THENL
3407      [
3408        REPEAT STRIP_TAC THEN
3409        IMP_RES_TAC LEADSTO_thm2 THEN
3410        IMP_RES_TAC LEADSTO_thm35_lemma00 THEN
3411        ONCE_REWRITE_TAC [AND_COMM_lemma] THEN
3412        ACCEPT_TAC (ASSUME
3413         (`(((p':'a->bool) /\* p) LEADSTO
3414              ((q' /\* q) \/* r'))(CONS st Pr)`))
3415       ;
3416        REPEAT STRIP_TAC THEN
3417        IMP_RES_TAC LEADSTO_thm2 THEN
3418        IMP_RES_TAC LEADSTO_thm0 THEN
3419        ASSUME_TAC (UNDISCH (SPECL
3420          [(`p:'a->bool`); (`r':'a->bool`);
3421           (`CONS (st:'a->'a) Pr`)] ENSURES_cor2)) THEN
3422        ASSUME_TAC (UNDISCH (SPECL
3423          [(`p':'a->bool`); (`r:'a->bool`);
3424           (`CONS (st:'a->'a) Pr`)] ENSURES_cor2)) THEN
3425        ASSUME_TAC (REWRITE_RULE
3426         [ASSUME (`((p:'a->bool)UNLESS r')(CONS st Pr)`);
3427          ASSUME (`((p':'a->bool)ENSURES r)(CONS st Pr)`)]
3428           (SPECL
3429             [(`p:'a->bool`); (`r':'a->bool`);
3430              (`p':'a->bool`); (`r:'a->bool`);
3431              (`CONS (st:'a->'a) Pr`)] ENSURES_thm4)) THEN
3432        IMP_RES_TAC LEADSTO_thm0 THEN
3433        RES_TAC THEN
3434        ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL OR_ASSOC_lemma)]
3435         (ONCE_REWRITE_RULE [OR_COMM_lemma] (REWRITE_RULE [
3436           (ASSUME
3437             (`(((r':'a->bool) /\* r) LEADSTO ((q /\* q') \/* r''))
3438                   (CONS st Pr)`));
3439           (ASSUME (`(((p:'a->bool) /\* p') LEADSTO
3440             (((p /\* r) \/* (p' /\* r')) \/* (r' /\* r)))
3441                 (CONS st Pr)`))] (SPECL
3442            [(`(p:'a->bool) /\* p'`);
3443             (`((p:'a->bool) /\* r) \/* (p' /\* r')`);
3444             (`(r':'a->bool) /\* r`);
3445             (`((q:'a->bool) /\* q') \/* r''`); (`st:'a->'a`);
3446             (`Pr:('a->'a)list`)] LEADSTO_thm28)))) THEN
3447        ASSUME_TAC (REWRITE_RULE [LEADSTO_thm35_lemma01_2] (REWRITE_RULE
3448         [(ONCE_REWRITE_RULE [SPECL [(`r':'a->bool`);
3449                                     (`p':'a->bool`)] AND_COMM_lemma]
3450         (ASSUME
3451           (`(((r':'a->bool) /\* p') LEADSTO ((q /\* q') \/* r''))
3452                  (CONS st Pr)`)));
3453          (ASSUME (`(((p:'a->bool) /\* p') LEADSTO
3454          ((((q /\* q') \/* r'') \/* (p /\* r)) \/* (p' /\* r')))
3455                   (CONS st Pr)`))] (SPECL
3456           [(`(p:'a->bool) /\* p'`);
3457            (`(((q:'a->bool) /\* q') \/* r'') \/* (p /\* r)`);
3458            (`(p':'a->bool) /\* r'`);
3459            (`((q':'a->bool) /\* q) \/* r''`); (`st:'a->'a`);
3460            (`Pr:('a->'a)list`)] LEADSTO_thm28))) THEN
3461        ASM_REWRITE_TAC [REWRITE_RULE [OR_OR_lemma] (REWRITE_RULE
3462         [(ASSUME
3463            (`(((p:'a->bool) /\* r) LEADSTO ((q /\* q') \/* r''))(CONS st Pr)`));
3464          (ASSUME (`(((p:'a->bool) /\* p') LEADSTO
3465                   (((q /\* q') \/* r'') \/* (p /\* r)))(CONS st Pr)`))] (SPECL
3466            [(`(p:'a->bool) /\* p'`); (`((q:'a->bool) /\* q') \/* r''`);
3467             (`(p:'a->bool) /\* r`); (`((q:'a->bool) /\* q') \/* r''`);
3468             (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm28))]
3469       ;
3470        REPEAT STRIP_TAC THEN
3471        IMP_RES_TAC LEADSTO_thm0 THEN
3472        IMP_RES_TAC LEADSTO_thm2 THEN
3473        IMP_RES_TAC LEADSTO_thm35_lemma01_3 THEN
3474        IMP_RES_TAC LEADSTO_thm35_lemma01_8
3475      ]
3476     ;
3477      REPEAT STRIP_TAC THEN
3478      IMP_RES_TAC LEADSTO_thm35_lemma01_9 THEN
3479      IMP_RES_TAC LEADSTO_thm35_lemma01_10 THEN
3480      IMP_RES_TAC LEADSTO_thm35_lemma01_8 THEN
3481      ONCE_REWRITE_TAC [SPECL
3482       [(`LUB (P:('a->bool)->bool)`); (`p':'a->bool`)] AND_COMM_lemma] THEN
3483      ASM_REWRITE_TAC []
3484    ]);;
3485
3486 (*
3487   Now prove the completion theorem:
3488
3489   |- !p q p' q' r st Pr.
3490       (p LEADSTO q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) /\
3491       (q UNLESS r)(CONS st Pr) /\ (q' UNLESS r)(CONS st Pr)
3492          ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)
3493 *)
3494 let LEADSTO_thm35 = prove_thm
3495   ("LEADSTO_thm35",
3496    (`!(p:'a->bool) q p' q' r st Pr.
3497      (p LEADSTO q)(CONS st Pr) /\ (p' LEADSTO q')(CONS st Pr) /\
3498      (q UNLESS r)(CONS st Pr) /\ (q' UNLESS r)(CONS st Pr)
3499         ==> ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)`),
3500    REPEAT STRIP_TAC THEN
3501    IMP_RES_TAC LEADSTO_thm35_lemma01);;
3502
3503 (*
3504        We now prove the theorem valid for proving bounds of progress.
3505  *)
3506
3507 (*
3508   We need to define the metric predicates EQmetric and LESSmetric
3509 *)
3510
3511 (*
3512         EQmetric is the state abstracted predicate expressing that the metric
3513         function M must have the value m in the state s.
3514 *)
3515 let EQmetric = new_infix_definition
3516   ("EQmetric", "<=>",
3517   (`EQmetric (M:'a->num) m = \s. M s = m`), TL_FIX);;
3518
3519 (*
3520         LESSmetric is the state abstracted predicate expressing that the metric
3521         function M must have a value less than m in the state s.
3522 *)
3523 let LESSmetric = new_infix_definition
3524   ("LESSmetric", "<=>",
3525   (`LESSmetric (M:'a->num) m = \s. M s < m`), TL_FIX);;
3526
3527 (*---------------------------------------------------------------------------*)
3528 (*
3529   Lemmas
3530 *)
3531 (*---------------------------------------------------------------------------*)
3532
3533 let LEADSTO_thm36_lemma00 = BETA_RULE
3534    (SPEC (`\n. (((p:'a->bool) /\* (M EQmetric n)) LEADSTO q)(CONS st Pr)`)
3535          GEN_INDUCT_thm);;
3536
3537 let LEADSTO_thm36_lemma01 = TAC_PROOF
3538   (([],
3539    (`!(M:'a->num) m. (p /\* (M EQmetric m)) = ((\i. p /\* (M EQmetric i))m)`)),
3540    BETA_TAC THEN
3541    REWRITE_TAC []);;
3542
3543 let LEADSTO_thm36_lemma02 = TAC_PROOF
3544   (([],
3545    (`!(p:'a->bool) q st Pr M m.
3546        (!n. n < (SUC m) ==> ((p /\* (M EQmetric n)) LEADSTO q)(CONS st Pr)) ==>
3547              (!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q)(CONS st Pr))`)),
3548    REPEAT STRIP_TAC THEN
3549    STRIP_ASSUME_TAC
3550      (MP (SPEC (`n:num`) (ASSUME (`!n. n < (SUC m) ==>
3551            (((p:'a->bool) /\* (M EQmetric n)) LEADSTO q)(CONS st Pr)`)))
3552          (MP (SPECL [(`n:num`); (`m:num`)] LESS_SUC) (ASSUME (`n < m`)))));;
3553
3554 let LEADSTO_thm36_lemma03 = TAC_PROOF
3555   (([],
3556    (`!(p:'a->bool) q st Pr M m.
3557       (!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q) (CONS st Pr)) ==>
3558          (( \</*  (\i. p /\* (M EQmetric i))m) LEADSTO q) (CONS st Pr)`)),
3559    GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
3560    INDUCT_TAC THENL
3561      [
3562       REWRITE_TAC [OR_LT_N_def; LEADSTO_cor12; LEADSTO_cor11; NOT_LESS_0]
3563      ;
3564       DISCH_TAC THEN
3565       REWRITE_TAC [OR_LT_N_def] THEN
3566       BETA_TAC THEN
3567       ASSUME_TAC (UNDISCH_ALL (SPEC_ALL LEADSTO_thm36_lemma02)) THEN
3568       ASSUME_TAC (MP
3569        (ASSUME (`(!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q)(CONS st Pr))
3570                     ==> (( \</* (\i. p /\* (M EQmetric i))m) LEADSTO q)
3571                          (CONS (st:'a->'a) Pr)`))
3572        (ASSUME (`!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q)
3573                          (CONS (st:'a->'a) Pr)`))) THEN
3574       ASSUME_TAC (REWRITE_RULE [LESS_SUC_REFL] (SPEC (`m:num`)
3575        (ASSUME (`!n. n < (SUC m) ==> ((p /\* (M EQmetric n)) LEADSTO q)
3576                          (CONS (st:'a->'a) Pr)`)))) THEN
3577       STRIP_ASSUME_TAC (MP (SPECL
3578        [(` \</* (\i. (p:'a->bool) /\* (M EQmetric i))m`);
3579         (`(p:'a->bool) /\* (M EQmetric m)`); (`q:'a->bool`); (`CONS (st:'a->'a) Pr`)]
3580         LEADSTO_thm4) (CONJ
3581          (ASSUME (`(( \</* (\i. p /\* (M EQmetric i))m) LEADSTO q)
3582                     (CONS (st:'a->'a) Pr)`))
3583          (ASSUME (`((p /\* (M EQmetric m)) LEADSTO q)(CONS (st:'a->'a) Pr)`))))
3584      ]);;
3585
3586 let LEADSTO_thm36_lemma04 = TAC_PROOF
3587   (([],
3588    (`!M:'a->num. (!m s. (M LESSmetric m)s = ( \</*  (\i. M EQmetric i) m) s)`)),
3589    GEN_TAC THEN
3590    INDUCT_TAC THENL
3591      [
3592       REWRITE_TAC [LESSmetric; EQmetric; OR_LT_N_def; FALSE_def; NOT_LESS_0]
3593      ;
3594       GEN_TAC THEN
3595       REWRITE_TAC [OR_LT_N_def; OR_def; LESSmetric; LESS_THM] THEN
3596       BETA_TAC THEN
3597       EQ_TAC THENL
3598         [
3599          STRIP_TAC THENL
3600            [
3601             DISJ2_TAC THEN
3602             REWRITE_TAC [EQmetric] THEN
3603             BETA_TAC THEN
3604             ASM_REWRITE_TAC []
3605            ;
3606             DISJ1_TAC THEN
3607             ASM_REWRITE_TAC [SYM (SPEC_ALL(BETA_RULE (REWRITE_RULE [LESSmetric]
3608              (ASSUME (`!s:'a. (M LESSmetric m)s =  \</* (\i. M EQmetric i)m s`)))))]
3609            ]
3610         ;
3611          STRIP_TAC THENL
3612            [
3613             DISJ2_TAC THEN
3614             ASM_REWRITE_TAC [SPEC_ALL (BETA_RULE (REWRITE_RULE [LESSmetric]
3615              (ASSUME (`!s:'a. (M LESSmetric m)s =  \</* (\i. M EQmetric i)m s`))))]
3616            ;
3617             DISJ1_TAC THEN
3618             STRIP_ASSUME_TAC (BETA_RULE (REWRITE_RULE [EQmetric]
3619              (ASSUME (`(M EQmetric m)(s:'a)`))))
3620            ]
3621         ]
3622      ]);;
3623
3624 let LEADSTO_thm36_lemma05 = TAC_PROOF
3625   (([],
3626    (`!(M:'a->num) m. (M LESSmetric m) = ( \</*  (\i. M EQmetric i) m)`)),
3627    REWRITE_TAC [LESSmetric; EQmetric;
3628                 BETA_RULE ((REWRITE_RULE [LESSmetric; EQmetric]) (MK_ABS
3629                   (SPECL [(`M:'a->num`); (`m:num`)] LEADSTO_thm36_lemma04)))] THEN
3630    REWRITE_TAC [ETA_AX]);;
3631
3632 let LEADSTO_thm36_lemma06 = TAC_PROOF
3633   (([],
3634   (`!(p:'a->bool) M q Pr.
3635    (!m. ((p /\* (M EQmetric m)) LEADSTO ((p /\* (M LESSmetric m)) \/* q))Pr)
3636       ==> (!m. ((p /\* (M EQmetric m)) LEADSTO
3637                ((p /\* ( \</* (\i. M EQmetric i)m)) \/* q))Pr)`)),
3638    REWRITE_TAC [LEADSTO_thm36_lemma05]);;
3639
3640 let LEADSTO_thm36_lemma07 = TAC_PROOF
3641   (([],
3642    (`!(p:'a->bool) M m.
3643       ( \</* (\i. p /\* (M EQmetric i))m) = (p /\* ( \</* (\i. M EQmetric i)m))`)),
3644    GEN_TAC THEN GEN_TAC THEN
3645    INDUCT_TAC THENL
3646      [
3647       REWRITE_TAC [OR_LT_N_def; AND_False_lemma]
3648      ;
3649       REWRITE_TAC [OR_LT_N_def] THEN
3650       BETA_TAC THEN
3651       ASM_REWRITE_TAC [SYM (SPEC_ALL AND_OR_DISTR_lemma)]]);;
3652
3653 let LEADSTO_thm36_lemma08 = TAC_PROOF
3654   (([],
3655    (`!(p:'a->bool) q st Pr M.
3656        (!m. ((p /\* (M EQmetric m)) LEADSTO
3657            ((p /\* (M LESSmetric m)) \/* q)) (CONS st Pr)) ==>
3658        (!m. (!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q)(CONS st Pr)) ==>
3659                    ((p /\* (M EQmetric m)) LEADSTO q) (CONS st Pr))`)),
3660    REPEAT STRIP_TAC THEN
3661    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm36_lemma07]
3662     (MP (SPEC_ALL LEADSTO_thm36_lemma03)
3663         (ASSUME (`!n. n < m ==> ((p /\* (M EQmetric n)) LEADSTO q)
3664                    (CONS (st:'a->'a) Pr)`)))) THEN
3665    ASSUME_TAC (ONCE_REWRITE_RULE [OR_COMM_lemma] (SPEC_ALL (UNDISCH (SPECL
3666     [(`p:'a->bool`); (`M:'a->num`); (`q:'a->bool`); (`CONS (st:'a->'a) Pr`)]
3667      LEADSTO_thm36_lemma06)))) THEN
3668    STRIP_ASSUME_TAC (REWRITE_RULE [OR_OR_lemma]
3669     (MP (SPECL [(`(p:'a->bool) /\* (M EQmetric m)`); (`q:'a->bool`);
3670                 (`(p:'a->bool) /\* ( \</* (\i. M EQmetric i)m)`);
3671                 (`q:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
3672                 LEADSTO_thm28)
3673       (CONJ (ASSUME (`(((p:'a->bool) /\* (M EQmetric m)) LEADSTO
3674                       (q \/* (p /\* ( \</* (\i. M EQmetric i)m)))) (CONS st Pr)`))
3675             (ASSUME (`((p /\* ( \</* (\i. M EQmetric i)m)) LEADSTO q)
3676                         (CONS (st:'a->'a) Pr)`))))));;
3677
3678 let LEADSTO_thm36_lemma09 = TAC_PROOF
3679   (([],
3680    (`!(p:'a->bool) q st Pr M.
3681        (!m. ((p /\* (M EQmetric m)) LEADSTO
3682             ((p /\* (M LESSmetric m)) \/* q)) (CONS st Pr)) ==>
3683                 (!m. ((p /\* (M EQmetric m)) LEADSTO q) (CONS st Pr))`)),
3684    REPEAT STRIP_TAC THEN
3685    ASSUME_TAC (UNDISCH (SPEC_ALL LEADSTO_thm36_lemma08)) THEN
3686    STRIP_ASSUME_TAC (SPEC (`m:num`) (UNDISCH_ALL LEADSTO_thm36_lemma00)));;
3687
3688 let LEADSTO_thm36_lemma10s = TAC_PROOF
3689   (([],
3690    (`!(p:'a->bool) M s.
3691      (p /\* ((?*) (\n. M EQmetric n)))s = ((?*) (\i. p /\* (M EQmetric i)))s`)),
3692    REPEAT STRIP_TAC THEN
3693    REWRITE_TAC [AND_def; EXISTS_def; EQmetric] THEN
3694    BETA_TAC THEN
3695    EQ_TAC THENL
3696      [
3697       STRIP_TAC THEN
3698       EXISTS_TAC (`x:num`) THEN
3699       ASM_REWRITE_TAC []
3700      ;
3701       STRIP_TAC THEN
3702       ASM_REWRITE_TAC [] THEN
3703       EXISTS_TAC (`x:num`) THEN
3704       ASM_REWRITE_TAC []
3705      ]);;
3706
3707 (*
3708    |- !p M. p /\* ( ?* ) ((EQmetric) M) = (?*i. p /\* (M EQmetric i))
3709 *)
3710 let LEADSTO_thm36_lemma10 =
3711   (GENL [`p:'a->bool`;`M:'a->num`] (ONCE_REWRITE_RULE [ETA_AX]
3712     (MK_ABS (SPECL [`p:'a->bool`;`M:'a->num`] LEADSTO_thm36_lemma10s))));;
3713
3714 let LEADSTO_thm36_lemma11s = TAC_PROOF
3715   (([],
3716    (`!(M:'a->num) s. ((?*)  (\n. M EQmetric n))s = True s`)),
3717    REWRITE_TAC [EXISTS_def; EQmetric; TRUE_def] THEN
3718    BETA_TAC THEN
3719    REPEAT GEN_TAC THEN
3720    EXISTS_TAC (`(M:'a->num) s`) THEN
3721    REFL_TAC);;
3722
3723 (*
3724    |- !M. ( ?* ) ((EQmetric) M) = True
3725 *)
3726 let LEADSTO_thm36_lemma11 =
3727   (GENL [`M:'a->num`] (ONCE_REWRITE_RULE [ETA_AX]
3728     (MK_ABS (SPECL [`M:'a->num`] LEADSTO_thm36_lemma11s))));;
3729
3730 let LEADSTO_thm36_lemma12 = TAC_PROOF
3731   (([],
3732    (`!(p:'a->bool) q st Pr M.
3733       (!m. ((p /\* (M EQmetric m)) LEADSTO
3734            ((p /\* (M LESSmetric m)) \/* q))(CONS st Pr))
3735              ==> ((p /\* ((?*)  (\n. M EQmetric n))) LEADSTO q)(CONS st Pr)`)),
3736    REPEAT STRIP_TAC THEN
3737    ASSUME_TAC (ONCE_REWRITE_RULE [LEADSTO_thm36_lemma01] (MP
3738     (SPEC_ALL LEADSTO_thm36_lemma09)
3739     (ASSUME (`!m. ((p /\* (M EQmetric m)) LEADSTO
3740              ((p /\* (M LESSmetric m)) \/* q)) (CONS (st:'a->'a) Pr)`)))) THEN
3741    IMP_RES_TAC (SPECL [`\i:num. (p:'a->bool) /\* (M EQmetric i)`]
3742                 LEADSTO_thm3c) THEN
3743    ASM_REWRITE_TAC [LEADSTO_thm36_lemma10]);;
3744
3745 let LEADSTO_thm36 = prove_thm
3746   ("LEADSTO_thm36",
3747    (`!(p:'a->bool) q st Pr M.
3748       (!m. ((p /\* (M EQmetric m)) LEADSTO ((p /\* (M LESSmetric m)) \/* q))
3749                                            (CONS st Pr))
3750              ==> (p LEADSTO q)(CONS st Pr)`),
3751    REPEAT STRIP_TAC THEN
3752    IMP_RES_TAC LEADSTO_thm36_lemma12 THEN
3753    ACCEPT_TAC (REWRITE_RULE [LEADSTO_thm36_lemma11; AND_True_lemma]
3754     (ASSUME
3755       (`(((p:'a->bool) /\* ((?*) (\n. M EQmetric n))) LEADSTO q)(CONS st Pr)`))));;
3756
3757 (*
3758   We prove a new induction theorem:
3759 *)
3760 let LEADSTO_thm37_lemma00 = TAC_PROOF
3761   (([],
3762    (`((!p:'a->bool. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)) =
3763     (!p'. p' In P ==> (p' LEADSTO q)Pr /\ X p' q)`)),
3764    EQ_TAC THEN
3765    REPEAT STRIP_TAC THEN
3766    RES_TAC);;
3767
3768 let LEADSTO_thm37_lemma01 = TAC_PROOF
3769   (([],
3770    (`(!p':'a->bool. p' In P ==> (p' LEADSTO q)Pr /\ X p' q) =
3771     ((!p'. p' In P ==> (p' LEADSTO q)Pr) /\ (!p'. p' In P ==> X p' q))`)),
3772    EQ_TAC THEN
3773    REPEAT STRIP_TAC THEN
3774    RES_TAC);;
3775
3776 let LEADSTO_thm37_lemma02 = TAC_PROOF
3777   (([],
3778    (`!(X:('a->bool)->('a->bool)->bool) Pr.
3779        (!p q.
3780          ((p ENSURES q)Pr ==> (p LEADSTO q)Pr /\ X p q) /\
3781          (!r.
3782            (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q ==>
3783            (p LEADSTO q)Pr /\ X p q) /\
3784          (!P.
3785            (p = LUB P) /\ (!p'. p' In P ==> (p' LEADSTO q)Pr /\ X p' q) ==>
3786            (p LEADSTO q)Pr /\ X p q))
3787       =
3788         (!p q.
3789         ((p ENSURES q)Pr ==> X p q) /\
3790         (!r.
3791           (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q ==> X p q) /\
3792         (!P.
3793           (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q) ==>
3794           X(LUB P)q))`)),
3795    REPEAT GEN_TAC THEN
3796    EQ_TAC THEN REPEAT STRIP_TAC THENL
3797     [
3798      RES_TAC
3799     ;
3800      RES_TAC
3801     ;
3802      ASSUME_TAC (REWRITE_RULE [LEADSTO_thm37_lemma00] (CONJ
3803        (ASSUME (`!p:'a->bool. p In P ==> (p LEADSTO q)Pr`))
3804        (ASSUME (`!p. p In P ==> (X:('a->bool)->('a->bool)->bool) p q`)))) THEN
3805      RES_TAC THEN
3806      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
3807       (`!p. (p = LUB P) ==> (X:('a->bool)->('a->bool)->bool) p q`))))
3808     ;
3809      IMP_RES_TAC LEADSTO_thm0
3810     ;
3811      RES_TAC
3812     ;
3813      IMP_RES_TAC LEADSTO_thm1 THEN
3814      RES_TAC
3815     ;
3816      IMP_RES_TAC LEADSTO_thm1 THEN
3817      RES_TAC
3818     ;
3819      IMP_RES_TAC LEADSTO_thm37_lemma01 THEN
3820      IMP_RES_TAC LEADSTO_thm3
3821     ;
3822      IMP_RES_TAC LEADSTO_thm37_lemma01 THEN
3823      RES_TAC THEN
3824      ASM_REWRITE_TAC []
3825     ]);;
3826
3827 let LEADSTO_thm37 = prove_thm
3828   ("LEADSTO_thm37",
3829    (`!X p q Pr.
3830       (!(p:'a->bool) q.
3831         ((p ENSURES q)Pr ==> X p q) /\
3832         (!r. (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q
3833                          ==> X p q) /\
3834         (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)
3835                          ==> X (LUB P) q))
3836      ==> ((p LEADSTO q)Pr ==> X p q)`),
3837    REPEAT STRIP_TAC THEN
3838    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm37_lemma02]
3839     (REWRITE_RULE [SYM (SPEC_ALL CONJ_ASSOC)] (BETA_RULE (SPEC
3840      (`\ (p:'a->bool) q Pr. (p LEADSTO q)Pr /\ (X p q)`)
3841        (REWRITE_RULE [LEADSTO; LeadstoRel]
3842          (ASSUME (`((p:'a->bool) LEADSTO q)Pr`))))))) THEN
3843    RES_TAC);;
3844
3845 (*
3846   The theorem useful for an induction tactic
3847 *)
3848 let LEADSTO_thm38 = prove_thm
3849   ("LEADSTO_thm38",
3850    (`!X.
3851       (!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q) /\
3852       (!p r q Pr. (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q
3853                                           ==> X p q) /\
3854       (!P q Pr. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)
3855                                           ==> X (LUB P) q)
3856      ==> (!p q Pr. (p LEADSTO q)Pr ==> X p q)`),
3857    REPEAT STRIP_TAC THEN
3858    ACCEPT_TAC (REWRITE_RULE
3859     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q`);
3860      ASSUME (`!(p:'a->bool) r q Pr.
3861                (p LEADSTO r)Pr /\ X p r /\ (r LEADSTO q)Pr /\ X r q
3862                                                 ==> X p q`);
3863      ASSUME (`!(P:('a->bool)->bool) q Pr.
3864         (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)
3865                                                 ==> X (LUB P) q`);
3866      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)] (SPEC_ALL LEADSTO_thm37)));;
3867
3868
3869 let LEADSTO_thm39_lemma00 = TAC_PROOF
3870   (([],
3871    (`!(X:('a->bool)->('a->bool)->bool) Pr.
3872        ((!p. p In P ==> LEADSTO2 p q Pr) /\ (!p. p In P ==> X p q)) =
3873         (!p. p In P ==> LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q))`)),
3874    REPEAT GEN_TAC THEN
3875    EQ_TAC THEN
3876    REPEAT STRIP_TAC THEN
3877    RES_TAC);;
3878
3879 let LEADSTO_thm39_lemma01 = TAC_PROOF
3880   (([],
3881    (`!(X:('a->bool)->('a->bool)->bool) Pr.
3882        (!p q.
3883          ((p ENSURES q)Pr ==>
3884           LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q)) /\
3885          (!r.
3886            (p ENSURES r)Pr /\
3887            LEADSTO2 r q Pr /\
3888            (LEADSTO2 r q Pr ==> X r q) ==>
3889            LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q)) /\
3890          (!P.
3891            (!p'.
3892              p' In P ==>
3893              LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q)) ==>
3894            LEADSTO2(LUB P)q Pr /\ (LEADSTO2(LUB P)q Pr ==> X(LUB P)q)))
3895       =
3896       (!p q.
3897         ((p ENSURES q)Pr ==> X p q) /\
3898         (!r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\ X r q ==> X p q) /\
3899         (!P.
3900           (!p. p In P ==> LEADSTO2 p q Pr) /\ (!p. p In P ==> X p q) ==>
3901           X(LUB P)q))`)),
3902    REPEAT GEN_TAC THEN
3903    EQ_TAC THEN REPEAT STRIP_TAC THENL
3904     [
3905      RES_TAC
3906     ;
3907      IMP_RES_TAC LEADSTO2_thm1 THEN
3908      ACCEPT_TAC (REWRITE_RULE
3909       [ASSUME (`((p:'a->bool) ENSURES r)Pr`);
3910        ASSUME (`LEADSTO2 (r:'a->bool) q Pr`);
3911        ASSUME (`LEADSTO2 (p:'a->bool) q Pr`);
3912        ASSUME (`(X:('a->bool)->('a->bool)->bool) r q`)]
3913       (SPEC_ALL (CONJUNCT1 (CONJUNCT2 (SPEC_ALL
3914        (ASSUME (`!(p:'a->bool) q.
3915         ((p ENSURES q)Pr ==> LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q)) /\
3916         (!r.
3917           (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\
3918           (LEADSTO2 r q Pr ==> X r q) ==>
3919           LEADSTO2 p q Pr /\ (LEADSTO2 p q Pr ==> X p q)) /\
3920         (!P.
3921           (!p'. p' In P ==> LEADSTO2 p' q Pr /\ (LEADSTO2 p' q Pr ==> X p' q))
3922         ==> LEADSTO2(LUB P)q Pr /\ (LEADSTO2(LUB P)q Pr ==> X(LUB P)q))`)))))))
3923     ;
3924      ASSUME_TAC (REWRITE_RULE [LEADSTO_thm39_lemma00] (CONJ
3925       (ASSUME (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr`))
3926       (ASSUME (`!p. p In P ==> (X:('a->bool)->('a->bool)->bool) p q`)))) THEN
3927      IMP_RES_TAC LEADSTO2_thm3a THEN
3928      ASSUME_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
3929       (`!p:'a->bool. (p = LUB P) ==> LEADSTO2 p q Pr`)))) THEN
3930      RES_TAC
3931     ;
3932      IMP_RES_TAC LEADSTO2_thm0
3933     ;
3934      RES_TAC
3935     ;
3936      IMP_RES_TAC LEADSTO2_thm1
3937     ;
3938      RES_TAC
3939     ;
3940      STRIP_ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm39_lemma00)]
3941       (ASSUME (`!p':'a->bool. p' In P ==> (LEADSTO2 p' q)Pr /\
3942                                         (LEADSTO2 p' q Pr ==> X p' q)`))) THEN
3943      IMP_RES_TAC LEADSTO2_thm3a THEN
3944      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
3945       (`!p:'a->bool. (p = LUB P) ==> LEADSTO2 p q Pr`))))
3946     ;
3947      STRIP_ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm39_lemma00)]
3948       (ASSUME (`!p':'a->bool. p' In P ==> (LEADSTO2 p' q)Pr /\
3949                                         (LEADSTO2 p' q Pr ==> X p' q)`))) THEN
3950      RES_TAC
3951     ]);;
3952
3953 let LEADSTO_thm39 = prove_thm
3954   ("LEADSTO_thm39",
3955    (`!(X:('a->bool)->('a->bool)->bool) p q Pr.
3956     (!p q. ((p ENSURES q)Pr ==> X p q) /\
3957             (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ (X r q) ==> X p q) /\
3958             (!P. (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)
3959                ==> X (LUB P) q))
3960       ==> ((p LEADSTO q)Pr ==> X p q)`),
3961    REWRITE_TAC [LEADSTO_EQ_LEADSTO2] THEN
3962    REPEAT GEN_TAC THEN
3963    REPEAT DISCH_TAC THEN
3964    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm39_lemma01] (BETA_RULE
3965     (SPEC (`\(p:'a->bool) q Pr. (LEADSTO2 p q Pr /\
3966                               (LEADSTO2 p q Pr ==> X p q))`)
3967      (REWRITE_RULE [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam]
3968         (ASSUME (`LEADSTO2 (p:'a->bool) q Pr`)))))) THEN
3969    RES_TAC);;
3970
3971
3972 (*
3973   The theorem useful for an induction tactic
3974 *)
3975 let LEADSTO_thm40 = prove_thm
3976   ("LEADSTO_thm40",
3977    (`!X.
3978     (!p q Pr. (p ENSURES q)Pr ==> X p q) /\
3979     (!p r q Pr.
3980         (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q ==> X p q) /\
3981     (!P q Pr.
3982         (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q)
3983             ==> X (LUB P) q)
3984       ==>
3985         (!(p:'a->bool) q Pr. (p LEADSTO q)Pr ==> X p q)`),
3986   REPEAT STRIP_TAC THEN
3987   ASSUME_TAC (REWRITE_RULE
3988    [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q`);
3989     ASSUME (`!(p:'a->bool) r q Pr. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\
3990         X r q ==> X p q`);
3991     ASSUME (`!P (q:'a->bool) Pr. (!p. p In P ==> (p LEADSTO q)Pr) /\
3992         (!p. p In P ==> X p q) ==> X (LUB P) q`)]
3993      (SPEC_ALL LEADSTO_thm39)) THEN
3994   RES_TAC);;
3995
3996 (*
3997   Finally let us present the most compact form of the two induction principles
3998   used in [CM88]
3999 *)
4000
4001 (*
4002   The first induction principle (actually a weakening of LEADSTO_thm23):
4003 *)
4004 let LEADSTO_thm41 = prove_thm
4005  ("LEADSTO_thm41",
4006   (`!X.
4007         (!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
4008         (!p r q Pr. (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
4009                         ==> X p q Pr) /\
4010         (!p P q Pr. (p = LUB P) /\
4011                   (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4012                         ==> X p q Pr)
4013      ==> (!(p:'a->bool) q Pr. (p LEADSTO q) Pr ==> X p q Pr)`),
4014    REPEAT STRIP_TAC THEN
4015    ACCEPT_TAC (UNDISCH (SPEC_ALL (REWRITE_RULE
4016     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
4017      ASSUME (`!(p:'a->bool) r q Pr.
4018       (p LEADSTO r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr ==> X p q Pr`);
4019      ASSUME (`!(p:'a->bool) P q Pr. (p = LUB P) /\
4020                 (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4021                          ==> X p q Pr`);
4022      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)] (SPEC_ALL LEADSTO_thm23)))));;
4023
4024 (*
4025   Now prove the second induction principle:
4026 *)
4027 let LEADSTO_thm42_lemma00 = TAC_PROOF
4028   (([],
4029    (`!X Pr.
4030        (!p:'a->bool. p In P ==> LEADSTO2 p q Pr /\ X p q Pr) =
4031       ((!p. p In P ==> LEADSTO2 p q Pr) /\ (!p. p In P ==> X p q Pr))`)),
4032    REPEAT GEN_TAC THEN
4033    EQ_TAC THEN
4034    REPEAT STRIP_TAC THEN
4035    RES_TAC);;
4036
4037 let LEADSTO_thm42_lemma01 = TAC_PROOF
4038   (([],
4039    (`!X Pr.
4040       (!(p:'a->bool) q.
4041        ((p ENSURES q)Pr ==> X p q Pr) /\
4042        (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
4043             ==> X p q Pr) /\
4044        (!P. (p = (LUB P)) /\
4045             (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4046             ==> X p q Pr))
4047       =
4048       (!p q.
4049        ((p ENSURES q)Pr ==> X p q Pr) /\
4050        (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X r q Pr ==> X p q Pr) /\
4051        (!P. (p = (LUB P)) /\
4052             (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4053             ==> X p q Pr))`)),
4054    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC);;
4055
4056 let LEADSTO_thm42_lemma02 = TAC_PROOF
4057   (([],
4058    (`!X Pr.
4059      (!(p:'a->bool) q.
4060       ((p ENSURES q)Pr ==> X p q Pr) /\
4061       (!r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\ X r q Pr ==> X p q Pr) /\
4062       (!P. (p = LUB P) /\
4063            (!p. p In P ==> LEADSTO2 p q Pr) /\
4064            (!p. p In P ==> X p q Pr) ==> X p q Pr))
4065     =
4066      (!p q.
4067       ((p ENSURES q)Pr ==> LEADSTO2 p q Pr /\ X p q Pr) /\
4068       (!r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\ X r q Pr
4069                ==> LEADSTO2 p q Pr /\ X p q Pr) /\
4070       (!P. (!p. p In P ==> LEADSTO2 p q Pr /\ X p q Pr)
4071                ==> LEADSTO2 (LUB P) q Pr /\ X (LUB P) q Pr))`)),
4072    REPEAT GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC THENL
4073     [
4074      IMP_RES_TAC LEADSTO2_thm0
4075     ;
4076      IMP_RES_TAC LEADSTO2_thm1
4077     ;
4078      STRIP_ASSUME_TAC (REWRITE_RULE [LEADSTO_thm42_lemma00] (ASSUME
4079       (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr /\ X p q Pr`))) THEN
4080      IMP_RES_TAC LEADSTO2_thm3
4081     ;
4082      STRIP_ASSUME_TAC (REWRITE_RULE [LEADSTO_thm42_lemma00] (ASSUME
4083       (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr /\ X p q Pr`))) THEN
4084      RES_TAC THEN
4085      ACCEPT_TAC (REWRITE_RULE [] (SPEC (`LUB (P:('a->bool)->bool)`) (ASSUME
4086      (`!p. (p = LUB P)
4087         ==> (X:('a->bool)->('a->bool)->(('a->'a)list)->bool)p q Pr`))))
4088     ;
4089      ASSUME_TAC (REWRITE_RULE [SYM (SPEC_ALL LEADSTO_thm42_lemma00)] (CONJ
4090       (ASSUME (`!p:'a->bool. p In P ==> LEADSTO2 p q Pr`))
4091       (ASSUME (`!p. p In P
4092             ==> (X:('a->bool)->('a->bool)->(('a->'a)list)->bool) p q Pr`)))) THEN
4093      RES_TAC THEN
4094      ASM_REWRITE_TAC []
4095     ]);;
4096
4097 (*
4098   The strongest version of the second induction theorem:
4099 *)
4100 let LEADSTO_thm42 = prove_thm
4101  ("LEADSTO_thm42",
4102    (`!X Pr.
4103      (!(p:'a->bool) q.
4104        ((p ENSURES q)Pr ==> X p q Pr) /\
4105        (!r. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
4106            ==> X p q Pr) /\
4107        (!P. (p = (LUB P)) /\
4108             (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4109             ==> X p q Pr))
4110      ==> (!(p:'a->bool) q. (p LEADSTO q) Pr ==> X p q Pr)`),
4111    REWRITE_TAC [LEADSTO_thm42_lemma01] THEN
4112    REWRITE_TAC [LEADSTO_EQ_LEADSTO2] THEN
4113    REPEAT STRIP_TAC THEN
4114    ASSUME_TAC (BETA_RULE (SPEC
4115      (`\(p:'a->bool) q Pr. (LEADSTO2 p q Pr) /\ (X p q Pr)`)
4116        (REWRITE_RULE [LEADSTO2; LEADSTO2Fn_EQ_LEADSTO2Fam; LEADSTO2Fam]
4117          (ASSUME (`LEADSTO2 (p:'a->bool) q Pr`))))) THEN
4118    ASSUME_TAC (REWRITE_RULE [LEADSTO_thm42_lemma02] (ASSUME
4119     (`!(p:'a->bool) q.
4120       ((p ENSURES q)Pr ==> X p q Pr) /\
4121       (!r. (p ENSURES r)Pr /\ LEADSTO2 r q Pr /\ X r q Pr ==> X p q Pr) /\
4122       (!P. (p = LUB P) /\
4123            (!p. p In P ==> LEADSTO2 p q Pr) /\ (!p. p In P ==> X p q Pr) ==>
4124               X p q Pr)`))) THEN
4125    RES_TAC);;
4126
4127 (*
4128   The second induction principle (actually a weakening of LEADSTO_thm42a):
4129 *)
4130 let LEADSTO_thm43 = prove_thm
4131  ("LEADSTO_thm43",
4132   (`!X.
4133       (!p q Pr. (p ENSURES q)Pr ==> X p q Pr) /\
4134       (!p r q Pr. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\ X p r Pr /\ X r q Pr
4135                         ==> X p q Pr) /\
4136       (!p P q Pr. (p = (LUB P)) /\
4137                   (!p. p In P ==> (p LEADSTO q)Pr) /\ (!p. p In P ==> X p q Pr)
4138                         ==> X p q Pr)
4139      ==> (!(p:'a->bool) q Pr. (p LEADSTO q) Pr ==> X p q Pr)`),
4140    REPEAT STRIP_TAC THEN
4141    ACCEPT_TAC (UNDISCH (SPEC_ALL (REWRITE_RULE
4142     [ASSUME (`!(p:'a->bool) q Pr. (p ENSURES q)Pr ==> X p q Pr`);
4143      ASSUME (`!(p:'a->bool) r q Pr. (p ENSURES r)Pr /\ (r LEADSTO q)Pr /\
4144                                    X p r Pr /\ X r q Pr ==> X p q Pr`);
4145      ASSUME (`!(p:'a->bool) P q Pr. (p = LUB P) /\
4146                                   (!p. p In P ==> (p LEADSTO q)Pr) /\
4147                                   (!p. p In P ==> X p q Pr) ==> X p q Pr`);
4148      ASSUME (`((p:'a->bool) LEADSTO q)Pr`)] (SPEC_ALL LEADSTO_thm42)))));;
4149
4150
4151 (*
4152      The last corollaries using the completion theorem:
4153  *)
4154
4155 let LEADSTO_cor13_lemma01 = TAC_PROOF
4156   (([],
4157    (`!(Q:num->('a->bool)) r s.
4158        ((((/<=\* Q i) \/* r) /\* ((Q(SUC i)) \/* r)) \/* r)s
4159       =
4160        ((/<=\* Q (SUC i)) \/* r)s`)),
4161    REPEAT GEN_TAC THEN
4162    REWRITE_TAC [AND_LE_N_def; OR_def; AND_def] THEN
4163    BETA_TAC THEN
4164    EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
4165
4166 let LEADSTO_cor13 = prove_thm
4167   ("LEADSTO_cor13",
4168    (`!(P:num->('a->bool)) Q r st Pr.
4169        (!i. ((P i) LEADSTO ((Q i) \/* r)) (CONS st Pr)) /\
4170        (!i. ((Q i) UNLESS r) (CONS st Pr)) ==>
4171          (!i. ((/<=\* P i) LEADSTO ((/<=\* Q i) \/* r)) (CONS st Pr))`),
4172    REPEAT GEN_TAC THEN
4173    STRIP_TAC THEN
4174    INDUCT_TAC THENL
4175     [
4176      ASM_REWRITE_TAC [AND_LE_N_def]
4177     ;
4178      IMP_RES_TAC UNLESS_cor17 THEN
4179      ASSUME_TAC (SPEC_ALL
4180       (ASSUME (`!i. ((/<=\* (Q:num->'a->bool) i) UNLESS r)(CONS st Pr)`))) THEN
4181      ASSUME_TAC (SPEC (`SUC i`) (ASSUME
4182       (`!i. (((P:num->('a->bool)) i) LEADSTO ((Q i) \/* r))(CONS st Pr)`))) THEN
4183      ASSUME_TAC (SPEC (`SUC i`) (ASSUME
4184        (`!i. (((Q:num->('a->bool)) i) UNLESS r)(CONS st Pr)`))) THEN
4185      ASSUME_TAC (REWRITE_RULE
4186       [ASSUME (`((/<=\* (Q:num->'a->bool) i) UNLESS r)(CONS st Pr)`);
4187        UNLESS_thm1] (SPECL
4188         [(`/<=\* (Q:num->('a->bool))i`); (`r:'a->bool`); (`r:'a->bool`); (`CONS(st:'a->'a)Pr`)]
4189           UNLESS_thm8)) THEN
4190      ASSUME_TAC (REWRITE_RULE
4191       [ASSUME (`(((Q:num->'a->bool)(SUC i)) UNLESS r)(CONS st Pr)`);
4192        UNLESS_thm1] (SPECL
4193         [(`(Q:num->('a->bool))(SUC i)`); (`r:'a->bool`); (`r:'a->bool`); (`CONS(st:'a->'a)Pr`)]
4194           UNLESS_thm8)) THEN
4195      ACCEPT_TAC (REWRITE_RULE
4196       [REWRITE_RULE [ETA_AX]
4197          (MK_ABS (GEN (`s:'a`) (SPEC_ALL LEADSTO_cor13_lemma01)));
4198        SYM (SPEC_ALL (CONJUNCT2 AND_LE_N_def))] (REWRITE_RULE
4199         [ASSUME (`((/<=\* (P:num->'a->bool)i) LEADSTO ((/<=\* Q i) \/* r))
4200                    (CONS st Pr)`);
4201          ASSUME (`(((P:num->'a->bool)(SUC i)) LEADSTO ((Q(SUC i)) \/* r))
4202                    (CONS st Pr)`);
4203          ASSUME (`(((/<=\* (Q:num->'a->bool) i) \/* r) UNLESS r)(CONS st Pr)`);
4204          ASSUME (`((((Q:num->'a->bool)(SUC i)) \/* r) UNLESS r)(CONS st Pr)`)]
4205           (SPECL [(`/<=\* (P:num->'a->bool)i`); (`(/<=\* (Q:num->'a->bool)i) \/* r`);
4206                   (`(P:num->'a->bool)(SUC i)`); (`((Q:num->'a->bool)(SUC i)) \/* r`);
4207                   (`r:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm35)))
4208      ]);;
4209
4210 (* Prove:
4211
4212    !p q r b p' q' r' b' Pr.
4213         (p  LEADSTO (q  \/* r))  Pr /\ (q  UNLESS b) Pr /\
4214         (p' LEADSTO (q' \/* r')) Pr /\ (q' UNLESS b') Pr ==>
4215             ((p /\* p') LEADSTO ((q /\* q') \/* ((r \/* b) \/* (r' \/* b'))) Pr
4216
4217  Hint:
4218    Show that:
4219        b  ==> (r \/* b) \/* (r' \/* b')
4220        b' ==> (r \/* b) \/* (r' \/* b')
4221    use these as assumptions for the unless properties in using the
4222    weakening theorem we then have
4223        q  unless (r \/* b) \/* (r' \/* b') in st^Pr,
4224        q' unless (R \/* B) \/* (R' \/* B') in st^Pr,
4225    now show that:
4226        r  ==> (r \/* b) \/* (r' \/* b')
4227        r' ==> (r \/* b) \/* (r' \/* b')
4228    use these to derive the leadto properties:
4229        r  leadsto ((r \/* b) \/* (r' \/* b')) in st^Pr
4230        r' leadsto ((r \/* b) \/* (r' \/* b')) in st^Pr
4231    by using the cancellation theorem of leadsto we get
4232        p  leadsto q  \/* ((r \/* b) \/* (r' \/* b')) in st^Pr
4233        p' leadsto q' \/* ((r \/* b) \/* (r' \/* b')) in st^Pr
4234    now we are ready to use the theorem of completion:
4235        p  leadsto q  \/* ((r \/* b) \/* (r' \/* b')) in st^Pr,
4236        q  unless (r \/* b) \/* (r' \/* b') in st^Pr,
4237        p' leadsto q  \/* ((r \/* b) \/* (r' \/* b')) in st^Pr,
4238        q' unless (r \/* b) \/* (r' \/* b') in st^Pr
4239     ----------------------------------------------------------------------
4240       (p /\* p') leadsto (q /\* q')  \/* ((r \/* b) \/* (r' \/* b')) in st^Pr
4241
4242 *)
4243
4244 (* Prove:
4245    !p q r p' q' Pr.
4246      (p  LEADSTO (q  \/* r)) Pr /\ (q  UNLESS r) Pr /\
4247      (p' LEADSTO (q' \/* r)) Pr /\ (q' UNLESS r) Pr ==>
4248             ((p /\* p') LEADSTO ((q /\* q') \/* r)) Pr
4249 *)
4250 let LEADSTO_cor14 = prove_thm
4251   ("LEADSTO_cor14",
4252    (`!(p:'a->bool) q r p' q' st Pr.
4253          (p  LEADSTO (q  \/* r))(CONS st Pr) /\ (q  UNLESS r)(CONS st Pr) /\
4254          (p' LEADSTO (q' \/* r))(CONS st Pr) /\ (q' UNLESS r)(CONS st Pr)
4255              ==>
4256                  ((p /\* p') LEADSTO ((q /\* q') \/* r))(CONS st Pr)`),
4257    REPEAT STRIP_TAC THEN
4258    ASSUME_TAC (SPECL [(`r:'a->bool`); (`CONS (st:'a->'a) Pr`)] UNLESS_thm1) THEN
4259    ASSUME_TAC (UNDISCH_ALL (SPECL
4260     [(`((q:'a->bool) UNLESS r)(CONS st Pr)`); (`((r:'a->bool) UNLESS r)(CONS st Pr)`)]
4261      AND_INTRO_THM)) THEN
4262    ASSUME_TAC (REWRITE_RULE [OR_OR_lemma] (UNDISCH_ALL (SPECL
4263     [(`q:'a->bool`); (`r:'a->bool`); (`r:'a->bool`); (`r:'a->bool`); (`CONS (st:'a->'a) Pr`)]
4264      UNLESS_thm7))) THEN
4265    ASSUME_TAC (UNDISCH_ALL (SPECL
4266     [(`((q':'a->bool)UNLESS r)(CONS st Pr)`); (`((r:'a->bool) UNLESS r)(CONS st Pr)`)]
4267      AND_INTRO_THM)) THEN
4268    ASSUME_TAC (REWRITE_RULE [OR_OR_lemma] (UNDISCH_ALL (SPECL
4269     [(`q':'a->bool`); (`r:'a->bool`); (`r:'a->bool`); (`r:'a->bool`); (`CONS (st:'a->'a) Pr`)]
4270      UNLESS_thm7))) THEN
4271    ASSUME_TAC (SPECL
4272     [(`p:'a->bool`); (`(q:'a->bool) \/* r`);
4273      (`p':'a->bool`); (`(q':'a->bool) \/* r`); (`r:'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
4274      LEADSTO_thm35) THEN
4275    RES_TAC THEN
4276    UNDISCH_TAC (`(((p:'a->bool) /\* p') LEADSTO
4277                 (((q \/* r) /\* (q' \/* r)) \/* r))(CONS st Pr)`) THEN
4278    ONCE_REWRITE_TAC [SPECL
4279     [(`(q:'a->bool) \/* r`); (`r:'a->bool`); (`q':'a->bool`)] AND_OR_COMM_lemma] THEN
4280    ONCE_REWRITE_TAC [SPECL
4281     [(`(r:'a->bool) \/* q'`); (`r:'a->bool`); (`q:'a->bool`)] OR_COMM_AND_lemma] THEN
4282    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL OR_AND_DISTR_lemma))] THEN
4283    ONCE_REWRITE_TAC [SPECL
4284     [(`r:'a->bool`); (`(q:'a->bool) /\* q'`)] OR_COMM_lemma] THEN
4285    REWRITE_TAC [OR_ASSOC_lemma; OR_OR_lemma]);;
4286
4287
4288 (*
4289    !p q r b p' q' r' b' Pr.
4290      (p  LEADSTO (q  \/* r))  Pr /\ (q  UNLESS b)  Pr /\
4291      (p' LEADSTO (q' \/* r')) Pr /\ (q' UNLESS b') Pr ==>
4292         ((p /\* p') LEADSTO ((q /\* q') \/* ((r \/* b) \/* (r' \/* b')))) Pr
4293 *)
4294 let LEADSTO_cor15 = prove_thm
4295   ("LEADSTO_cor15",
4296    (`!(p:'a->bool) q r b p' q' r' b' st Pr.
4297        (p  LEADSTO (q  \/* r))(CONS st Pr)  /\ (q  UNLESS b)(CONS st Pr) /\
4298        (p' LEADSTO (q' \/* r'))(CONS st Pr) /\ (q' UNLESS b')(CONS st Pr)
4299          ==>
4300          ((p /\* p') LEADSTO
4301           ((q /\* q') \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr)`),
4302    REPEAT STRIP_TAC THEN
4303    MP_TAC (SPECL
4304     [(`b:'a->bool`); (`(r:'a->bool) \/* (r' \/* b')`)] OR_IMPLY_WEAK_lemma) THEN
4305    REWRITE_TAC [SYM (SPECL [(`b:'a->bool`); (`r:'a->bool`); (`(r':'a->bool) \/* b'`)]
4306                 OR_ASSOC_lemma)] THEN
4307    ONCE_REWRITE_TAC [SPECL [(`(r':'a->bool) \/* b'`); (`r:'a->bool`); (`b:'a->bool`)]
4308                             OR_COMM_OR_lemma] THEN
4309    DISCH_TAC THEN
4310    MP_TAC (SPECL
4311     [(`b':'a->bool`); (`(r':'a->bool) \/* (r \/* b)`)] OR_IMPLY_WEAK_lemma) THEN
4312    REWRITE_TAC [SYM (SPECL [(`b':'a->bool`); (`r':'a->bool`); (`(r:'a->bool) \/* b`)]
4313                              OR_ASSOC_lemma)] THEN
4314    ONCE_REWRITE_TAC [SPECL [(`(r:'a->bool) \/* b`); (`r':'a->bool`); (`b':'a->bool`)]
4315                              OR_COMM_OR_lemma] THEN
4316    ONCE_REWRITE_TAC [SPECL [(`(r':'a->bool) \/* b'`); (`(r:'a->bool) \/* b`)]
4317                             OR_COMM_lemma] THEN
4318    DISCH_TAC THEN
4319    MP_TAC (SPECL
4320     [(`r:'a->bool`); (`(b:'a->bool) \/* (r' \/* b')`)] OR_IMPLY_WEAK_lemma) THEN
4321    REWRITE_TAC [SYM (SPECL [(`r:'a->bool`); (`b:'a->bool`); (`(r':'a->bool) \/* b'`)]
4322                             OR_ASSOC_lemma)] THEN
4323    DISCH_TAC THEN
4324    MP_TAC (SPECL
4325     [(`r':'a->bool`); (`(b':'a->bool) \/* (r \/* b)`)] OR_IMPLY_WEAK_lemma) THEN
4326    REWRITE_TAC [SYM (SPECL [(`r':'a->bool`); (`b':'a->bool`); (`(r:'a->bool) \/* b`)]
4327                             OR_ASSOC_lemma)] THEN
4328    ONCE_REWRITE_TAC [SPECL [(`(r':'a->bool) \/* b'`); (`(r:'a->bool) \/* b`)]
4329                             OR_COMM_lemma] THEN
4330    DISCH_TAC THEN
4331    REWRITE_TAC [SYM (SPECL [(`(r:'a->bool) \/* b`); (`(r':'a->bool) \/* b'`);
4332                             (`(q:'a->bool) /\* q'`)]
4333                             OR_ASSOC_lemma)] THEN
4334    ONCE_REWRITE_TAC [SPECL
4335     [(`(((r:'a->bool) \/* b) \/* (r' \/* b'))`); (`(q:'a->bool) /\* q'`)]
4336      OR_COMM_lemma] THEN
4337    ASSUME_TAC (UNDISCH_ALL (SPECL
4338     [(`((q:'a->bool) UNLESS b)(CONS st Pr)`);
4339      (`!s:'a. b s ==> ((r \/* b) \/* (r' \/* b'))s`)]
4340      AND_INTRO_THM)) THEN
4341    ASSUME_TAC (UNDISCH_ALL (SPECL
4342     [(`q:'a->bool`); (`b:'a->bool`); (`((r:'a->bool) \/* b) \/* (r' \/* b')`);
4343      (`CONS (st:'a->'a) Pr`)]
4344      UNLESS_thm3)) THEN
4345    ASSUME_TAC (UNDISCH_ALL (SPECL
4346     [(`((q':'a->bool) UNLESS b')(CONS st Pr)`);
4347      (`!s:'a. b' s ==> ((r \/* b) \/* (r' \/* b'))s`)]
4348      AND_INTRO_THM)) THEN
4349    ASSUME_TAC (UNDISCH_ALL (SPECL
4350     [(`q':'a->bool`); (`b':'a->bool`); (`((r:'a->bool) \/* b) \/* (r' \/* b')`);
4351      (`CONS (st:'a->'a) Pr`)]
4352      UNLESS_thm3)) THEN
4353    ASSUME_TAC (UNDISCH_ALL (SPECL
4354     [(`r:'a->bool`); (`((r:'a->bool) \/* b) \/* (r' \/* b')`);
4355      (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm25)) THEN
4356    ASSUME_TAC (UNDISCH_ALL (SPECL
4357     [(`r':'a->bool`); (`((r:'a->bool) \/* b) \/* (r' \/* b')`);
4358      (`st:'a->'a`); (`Pr:('a->'a)list`)] LEADSTO_thm25)) THEN
4359    ASSUME_TAC (UNDISCH_ALL (SPECL
4360     [(`((p:'a->bool) LEADSTO (q \/* r))(CONS st Pr)`);
4361      (`((r:'a->bool) LEADSTO ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`)]
4362      AND_INTRO_THM)) THEN
4363    ASSUME_TAC (UNDISCH_ALL (SPECL
4364     [(`p:'a->bool`); (`q:'a->bool`); (`r:'a->bool`);
4365      (`((r:'a->bool) \/* b) \/* (r' \/* b')`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
4366      LEADSTO_thm28)) THEN
4367    ASSUME_TAC (UNDISCH_ALL (SPECL
4368     [(`((p':'a->bool) LEADSTO (q' \/* r'))(CONS st Pr)`);
4369      (`((r':'a->bool) LEADSTO ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`)]
4370      AND_INTRO_THM)) THEN
4371    ASSUME_TAC (UNDISCH_ALL (SPECL
4372     [(`p':'a->bool`); (`q':'a->bool`); (`r':'a->bool`);
4373      (`((r:'a->bool) \/* b) \/* (r' \/* b')`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
4374      LEADSTO_thm28)) THEN
4375    ASSUME_TAC (UNDISCH_ALL (SPECL
4376     [(`((p:'a->bool) LEADSTO (q \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr)`);
4377      (`((q:'a->bool) UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`)]
4378      AND_INTRO_THM)) THEN
4379    ASSUME_TAC (UNDISCH_ALL (SPECL
4380     [(`((p':'a->bool) LEADSTO(q' \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr)`);
4381      (`((q':'a->bool) UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`)]
4382      AND_INTRO_THM)) THEN
4383    ASSUME_TAC (UNDISCH_ALL (SPECL
4384     [(`((p:'a->bool) LEADSTO(q \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr) /\
4385       ((q:'a->bool) UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`);
4386      (`((p':'a->bool)LEADSTO(q' \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr) /\
4387       ((q':'a->bool) UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`)]
4388      AND_INTRO_THM)) THEN
4389    UNDISCH_TAC
4390     (`(((p:'a->bool) LEADSTO(q \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr) /\
4391       (q UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)) /\
4392       (p' LEADSTO (q' \/* ((r \/* b) \/* (r' \/* b'))))(CONS st Pr) /\
4393       (q' UNLESS ((r \/* b) \/* (r' \/* b')))(CONS st Pr)`) THEN
4394    REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL CONJ_ASSOC))] THEN
4395    DISCH_TAC THEN
4396    STRIP_ASSUME_TAC (UNDISCH_ALL (SPECL
4397     [(`p:'a->bool`); (`q:'a->bool`); (`((r:'a->bool) \/* b) \/* (r' \/* b'):'a->bool`);
4398      (`p':'a->bool`); (`q':'a->bool`); (`st:'a->'a`); (`Pr:('a->'a)list`)]
4399      LEADSTO_cor14)));;
4400
4401
4402 (* Prove:
4403  |- !P Q R B Pr.
4404   (!i. ((P i) LEADSTO ((Q i) \/* (R i)))Pr) /\ (!i. ((Q i) UNLESS (B i))Pr) ==>
4405   (!i. ((/<=\* P i) LEADSTO ((/<=\* Q i) \/* (( \<=/*  R i) \/* ( \<=/*  B i))))Pr)
4406 *)
4407 let LEADSTO_cor16_lemma1 = TAC_PROOF
4408   (([],
4409    (`!(Q:num->('a->bool)) R B i s.
4410       ((/<=\* Q(SUC i))  \/*
4411          (((( \<=/*  R i) \/* ( \<=/*  B i)) \/* ( \<=/*  B i))  \/*
4412           ((R(SUC i)) \/* (B(SUC i)))))s =
4413       ((/<=\* Q(SUC i)) \/* (( \<=/*  R(SUC i)) \/* ( \<=/*  B(SUC i))))s`)),
4414    REPEAT GEN_TAC THEN
4415    REWRITE_TAC [OR_def; AND_LE_N_def; OR_LE_N_def; AND_def] THEN
4416    BETA_TAC THEN
4417    EQ_TAC THEN REPEAT STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC []);;
4418
4419 let LEADSTO_cor16 = prove_thm
4420   ("LEADSTO_cor16",
4421    (`!(P:num->('a->bool)) Q R B st Pr.
4422       (!i. ((P i) LEADSTO ((Q i) \/* (R i)))(CONS st Pr)) /\
4423         (!i. ((Q i) UNLESS (B i))(CONS st Pr)) ==>
4424           (!i. ((/<=\* P i) LEADSTO
4425               ((/<=\* Q i) \/* (( \<=/*  R i) \/* ( \<=/*  B i)))) (CONS st Pr))`),
4426    REPEAT GEN_TAC THEN
4427    STRIP_TAC THEN
4428    INDUCT_TAC THENL
4429    [
4430      ASM_REWRITE_TAC [AND_LE_N_def; OR_LE_N_def] THEN
4431      ASSUME_TAC (ONCE_REWRITE_RULE [OR_ASSOC_lemma] (SPECL
4432       [(`((Q:num->('a->bool))0) \/* (R 0)`); (`((B:num->('a->bool))0)`)]
4433        OR_IMPLY_WEAK_lemma)) THEN
4434      ASSUME_TAC (SPEC (`0`) (ASSUME
4435       (`!i.(((P:num->('a->bool))i) LEADSTO ((Q i) \/* (R i)))(CONS st Pr)`))) THEN
4436      IMP_RES_TAC (SPECL [`(P:num->('a->bool)) 0`;
4437                          `(Q:num->('a->bool)) 0 \/* R 0`;
4438                          `(Q:num->('a->bool)) 0 \/* R 0 \/* B 0` ] LEADSTO_cor9)
4439     ;
4440      ASSUME_TAC (SPEC (`SUC i`) (ASSUME
4441       (`!i.(((P:num->('a->bool))i) LEADSTO ((Q i) \/* (R i)))(CONS st Pr)`))) THEN
4442      ASSUME_TAC (SPEC (`SUC i`) (ASSUME
4443        (`!i. (((Q:num->('a->bool)) i) UNLESS (B i))(CONS st Pr)`))) THEN
4444      ASSUME_TAC (SPEC (`i:num`) (UNDISCH_ALL (SPECL
4445       [(`Q:num->('a->bool)`); (`B:num->('a->bool)`); (`CONS st Pr:('a->'a)list`)]
4446        UNLESS_cor16))) THEN
4447      ACCEPT_TAC (REWRITE_RULE [ONCE_REWRITE_RULE [ETA_AX]
4448                          (MK_ABS (GEN (`s:'a`) (SPEC_ALL LEADSTO_cor16_lemma1)))]
4449      (REWRITE_RULE [SYM (SPEC_ALL (CONJUNCT2 AND_LE_N_def))] (REWRITE_RULE
4450       [ASSUME (`((/<=\* (P:num->'a->bool) i) LEADSTO
4451                  ((/<=\* Q i) \/* (( \<=/*  R i) \/* ( \<=/*  B i))))(CONS st Pr)`);
4452        ASSUME (`(((P:num->'a->bool)(SUC i)) LEADSTO ((Q(SUC i)) \/* (R(SUC i))))
4453                  (CONS st Pr)`);
4454        ASSUME (`(((Q:num->'a->bool)(SUC i)) UNLESS (B(SUC i)))(CONS st Pr)`);
4455        ASSUME (`((/<=\* (Q:num->'a->bool) i) UNLESS ( \<=/*  B i))(CONS st Pr)`)]
4456          (SPECL
4457            [(`/<=\* (P:num->('a->bool))i`); (`/<=\* (Q:num->('a->bool))i`);
4458             (`( \<=/*  (R:num->('a->bool))i) \/* ( \<=/*  (B:num->('a->bool))i)`);
4459             (` \<=/*  (B:num->('a->bool))i`);
4460             (`(P:num->('a->bool))(SUC i)`); (`(Q:num->('a->bool))(SUC i)`);
4461             (`(R:num->('a->bool))(SUC i)`); (`(B:num->('a->bool))(SUC i)`);
4462             (`st:'a->'a`); (`Pr:('a->'a)list`)]
4463             LEADSTO_cor15))))
4464     ]);;