201 lemma pred_exI: 

   201 lemma pred_exI: 

   202   assumes "(P(x) \<and>* r) s"

   202   assumes "(P(x) \<and>* r) s"

   203   shows "((EXS x. P(x)) \<and>* r) s"

   203   shows "((EXS x. P(x)) \<and>* r) s"

   204   by (metis assms pred_ex_def sep_globalise)

   204   by (metis assms pred_ex_def sep_globalise)

   205 

   205 

   206 definition

   208 definition

   207   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 

   209   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 

   208              ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

   210              ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)

   209 where

   211 where

   210   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 

   212   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c