src/HOL/HOLCF/IMP/HoareEx.thy
changeset 40774 0437dbc127b3
parent 35174 e15040ae75d7
child 40945 b8703f63bfb2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,33 @@
     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