(* Title: HOL/HOLCF/IMP/HoareEx.thy Author: Tobias Nipkow, TUM Copyright 1997 TUM
*)
section "Correctness of Hoare by Fixpoint Reasoning"
theory HoareEx imports Denotational begin
text\<open>
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch \<^cite>\<open>MuellerNvOS99\<close>. It demonstrates fixpoint reasoning by showing
the correctness of the Hoare rule for while-loops. \<close>
type_synonym assn = "state \ bool"
definition
hoare_valid :: "[assn, com, assn] \ bool" (\|= {(1_)}/ (_)/ {(1_)}\ 50) where "|= {P} c {Q} = (\s t. P s \ D c\(Discr s) = Def t \ Q t)"
lemma WHILE_rule_sound: "|= {A} c {A} \ |= {A} WHILE b DO c {\s. A s \ \ bval b s}" apply (unfold hoare_valid_def) apply (simp (no_asm)) apply (rule fix_ind) apply (simp (no_asm)) \<comment> \<open>simplifier with enhanced \<open>adm\<close>-tactic\<close> apply (simp (no_asm)) apply (simp (no_asm)) apply blast done
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
