6 header "Correctness of Hoare by Fixpoint Reasoning" |
6 header "Correctness of Hoare by Fixpoint Reasoning" |
7 |
7 |
8 theory HoareEx imports Denotational begin |
8 theory HoareEx imports Denotational begin |
9 |
9 |
10 text {* |
10 text {* |
11 An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch |
11 An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch |
12 \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
12 \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
13 the correctness of the Hoare rule for while-loops. |
13 the correctness of the Hoare rule for while-loops. |
14 *} |
14 *} |
15 |
15 |
16 type_synonym assn = "state => bool" |
16 type_synonym assn = "state => bool" |
17 |
17 |
18 definition |
18 definition |
19 hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where |
19 hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where |
20 "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)" |
20 "|= {P} c {Q} = (\<forall>s t. P s \<and> D c $(Discr s) = Def t --> Q t)" |
21 |
21 |
22 lemma WHILE_rule_sound: |
22 lemma WHILE_rule_sound: |
23 "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}" |
23 "|= {A} c {A} ==> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}" |
24 apply (unfold hoare_valid_def) |
24 apply (unfold hoare_valid_def) |
25 apply (simp (no_asm)) |
25 apply (simp (no_asm)) |
26 apply (rule fix_ind) |
26 apply (rule fix_ind) |
27 apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic" |
27 apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic" |
28 apply (simp (no_asm)) |
28 apply (simp (no_asm)) |