equal
deleted
inserted
replaced
415 done |
415 done |
416 |
416 |
417 (* ------ the main proof q o p = q ------ *) |
417 (* ------ the main proof q o p = q ------ *) |
418 |
418 |
419 theorem hoare_main: "q oo p = q" |
419 theorem hoare_main: "q oo p = q" |
420 apply (rule ext_cfun) |
420 apply (rule cfun_eqI) |
421 apply (subst cfcomp2) |
421 apply (subst cfcomp2) |
422 apply (rule hoare_lemma3 [THEN disjE]) |
422 apply (rule hoare_lemma3 [THEN disjE]) |
423 apply (erule hoare_lemma23) |
423 apply (erule hoare_lemma23) |
424 apply (erule hoare_lemma29) |
424 apply (erule hoare_lemma29) |
425 done |
425 done |