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