Quelle  HoareEx.thy

(*  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 ‹
  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
  🍋‹MuellerNvOS99›. It demonstrates fixpoint reasoning by showing
  the correctness of the Hoare rule for while-loops.
 ›

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)) 🍋 ‹simplifier with enhanced ‹adm›-tactic›
   apply (simp (no_asm))
  apply (simp (no_asm))
  apply blast
  done

end