author | wenzelm |
Tue, 16 Jan 2018 09:30:00 +0100 | |
changeset 67443 | 3abf6a722518 |
parent 63549 | b0d31c7def86 |
child 72835 | 66ca5016b008 |
permissions | -rw-r--r-- |
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) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63549
diff
changeset
|
27 |
apply (simp (no_asm)) \<comment> \<open>simplifier with enhanced \<open>adm\<close>-tactic\<close> |
12431 | 28 |
apply (simp (no_asm)) |
29 |
apply (simp (no_asm)) |
|
30 |
apply blast |
|
31 |
done |
|
32 |
||
3664 | 33 |
end |