Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/IMP/HoareEx.thy
author huffman
Sat, 27 Nov 2010 16:08:10 -0800
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IMP/HoareEx.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF; added HOLCF theories to src/HOL/IsaMakefile;

(*  Title:      HOLCF/IMP/HoareEx.thy
    Author:     Tobias Nipkow, TUM
    Copyright   1997 TUM
*)

header "Correctness of Hoare by Fixpoint Reasoning"

theory HoareEx imports Denotational begin

text {*
  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
  \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
  the correctness of the Hoare rule for while-loops.
*}

types assn = "state => bool"

definition
  hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
  "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"

lemma WHILE_rule_sound:
    "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
  apply (unfold hoare_valid_def)
  apply (simp (no_asm))
  apply (rule fix_ind)
    apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic"
   apply (simp (no_asm))
  apply (simp (no_asm))
  apply blast
  done

end
isabelle