1(*  Title:      HOL/HOLCF/IMP/HoareEx.thy
2    Author:     Tobias Nipkow, TUM
3    Copyright   1997 TUM
4*)
5
6section "Correctness of Hoare by Fixpoint Reasoning"
7
8theory HoareEx imports Denotational begin
9
10text \<open>
11  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch
12  @{cite MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
13  the correctness of the Hoare rule for while-loops.
14\<close>
15
16type_synonym assn = "state \<Rightarrow> bool"
17
18definition
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)"
21
22lemma WHILE_rule_sound:
23    "|= {A} c {A} \<Longrightarrow> |= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
24  apply (unfold hoare_valid_def)
25  apply (simp (no_asm))
26  apply (rule fix_ind)
27    apply (simp (no_asm)) \<comment> \<open>simplifier with enhanced \<open>adm\<close>-tactic\<close>
28   apply (simp (no_asm))
29  apply (simp (no_asm))
30  apply blast
31  done
32
33end
34