author | wenzelm |
Tue, 07 Oct 2014 23:12:08 +0200 | |
changeset 58622 | aa99568f56de |
parent 43143 | 1aeafba76f21 |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IMP/HoareEx.thy |
3664 | 2 |
Author: Tobias Nipkow, TUM |
3 |
Copyright 1997 TUM |
|
4 |
*) |
|
5 |
||
12431 | 6 |
header "Correctness of Hoare by Fixpoint Reasoning" |
7 |
||
16417 | 8 |
theory HoareEx imports Denotational begin |
3664 | 9 |
|
12431 | 10 |
text {* |
43143 | 11 |
An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch |
58622 | 12 |
@{cite MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
12546 | 13 |
the correctness of the Hoare rule for while-loops. |
12431 | 14 |
*} |
3664 | 15 |
|
41476 | 16 |
type_synonym assn = "state => bool" |
12431 | 17 |
|
19737 | 18 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19737
diff
changeset
|
19 |
hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where |
43143 | 20 |
"|= {P} c {Q} = (\<forall>s t. P s \<and> D c $(Discr s) = Def t --> Q t)" |
3664 | 21 |
|
12431 | 22 |
lemma WHILE_rule_sound: |
43143 | 23 |
"|= {A} c {A} ==> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}" |
12431 | 24 |
apply (unfold hoare_valid_def) |
25 |
apply (simp (no_asm)) |
|
26 |
apply (rule fix_ind) |
|
12600 | 27 |
apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic" |
12431 | 28 |
apply (simp (no_asm)) |
29 |
apply (simp (no_asm)) |
|
30 |
apply blast |
|
31 |
done |
|
32 |
||
3664 | 33 |
end |