author | huffman |
Sat, 08 Jan 2011 09:30:52 -0800 | |
changeset 41476 | 0fa9629aa399 |
parent 40945 | b8703f63bfb2 |
child 42151 | 4da4fc77664b |
permissions | -rw-r--r-- |
3664 | 1 |
(* Title: HOLCF/IMP/HoareEx.thy |
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 {* |
40945 | 11 |
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch |
12546 | 12 |
\cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
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 |
19737 | 20 |
"|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)" |
3664 | 21 |
|
12431 | 22 |
lemma WHILE_rule_sound: |
12600 | 23 |
"|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> 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 |