src/HOLCF/IMP/HoareEx.thy
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
     1.1 --- a/src/HOLCF/IMP/HoareEx.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,33 +0,0 @@
     1.4 -(*  Title:      HOLCF/IMP/HoareEx.thy
     1.5 -    Author:     Tobias Nipkow, TUM
     1.6 -    Copyright   1997 TUM
     1.7 -*)
     1.8 -
     1.9 -header "Correctness of Hoare by Fixpoint Reasoning"
    1.10 -
    1.11 -theory HoareEx imports Denotational begin
    1.12 -
    1.13 -text {*
    1.14 -  An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
    1.15 -  \cite{MuellerNvOS99}.  It demonstrates fixpoint reasoning by showing
    1.16 -  the correctness of the Hoare rule for while-loops.
    1.17 -*}
    1.18 -
    1.19 -types assn = "state => bool"
    1.20 -
    1.21 -definition
    1.22 -  hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
    1.23 -  "|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"
    1.24 -
    1.25 -lemma WHILE_rule_sound:
    1.26 -    "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
    1.27 -  apply (unfold hoare_valid_def)
    1.28 -  apply (simp (no_asm))
    1.29 -  apply (rule fix_ind)
    1.30 -    apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic"
    1.31 -   apply (simp (no_asm))
    1.32 -  apply (simp (no_asm))
    1.33 -  apply blast
    1.34 -  done
    1.35 -
    1.36 -end