42151
|
1 |
(* Title: HOL/HOLCF/IMP/HoareEx.thy
|
3664
|
2 |
Author: Tobias Nipkow, TUM
|
|
3 |
Copyright 1997 TUM
|
|
4 |
*)
|
|
5 |
|
58880
|
6 |
section "Correctness of Hoare by Fixpoint Reasoning"
|
12431
|
7 |
|
16417
|
8 |
theory HoareEx imports Denotational begin
|
3664
|
9 |
|
62175
|
10 |
text \<open>
|
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.
|
62175
|
14 |
\<close>
|
3664
|
15 |
|
63549
|
16 |
type_synonym assn = "state \<Rightarrow> bool"
|
12431
|
17 |
|
19737
|
18 |
definition
|
63549
|
19 |
hoare_valid :: "[assn, com, assn] \<Rightarrow> bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
|
|
20 |
"|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"
|
3664
|
21 |
|
12431
|
22 |
lemma WHILE_rule_sound:
|
63549
|
23 |
"|= {A} c {A} \<Longrightarrow> |= {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)
|
62175
|
27 |
apply (simp (no_asm)) \<comment> "simplifier with enhanced \<open>adm\<close>-tactic"
|
12431
|
28 |
apply (simp (no_asm))
|
|
29 |
apply (simp (no_asm))
|
|
30 |
apply blast
|
|
31 |
done
|
|
32 |
|
3664
|
33 |
end
|