diff --git a/lib/Monads/NonDetMonad_Sat.thy b/lib/Monads/NonDetMonad_Sat.thy
index d34b8df2d..ced68f50f 100644
--- a/lib/Monads/NonDetMonad_Sat.thy
+++ b/lib/Monads/NonDetMonad_Sat.thy
@@ -20,13 +20,36 @@ definition exs_valid ::
   "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s') \<in> fst (f s). Q rv s')"
 
-
 text \<open>The above for the exception monad\<close>
 definition ex_exs_validE ::
   "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'e + 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('e \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace> f  \<exists>\<lbrace>\<lambda>rv. case rv of Inl e \<Rightarrow> E e | Inr v \<Rightarrow> Q v\<rbrace>"
 
+text \<open>
+  Seen as predicate transformer, @{const exs_valid} is the so-called conjugate wp in the literature,
+  i.e. with
+  @{term "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"} and
+  @{term "cwp f Q \<equiv> not (wp f (not Q))"}, we get
+  @{prop "valid P f Q = (\<forall>s. P s \<longrightarrow> wp f Q s)"} and
+  @{prop "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"}.
+
+  See also "Predicate Calculus and Program Semantics" by E. W. Dijkstra and C. S. Scholten.\<close>
+experiment
+begin
+
+definition
+  "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"
+
+definition
+  "cwp f Q \<equiv> not (wp f (not Q))"
+
+lemma
+  "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"
+  unfolding exs_valid_def cwp_def wp_def by auto
+
+end
+
 
 subsection \<open>Set up for @{method wp}\<close>
 
@@ -73,6 +96,10 @@ lemma exs_valid_select[wp]:
   "\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>"
   by (clarsimp simp: exs_valid_def select_def)
 
+lemma exs_valid_alt[wp]:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>"
+  by (fastforce simp: exs_valid_def alternative_def)
+
 lemma exs_valid_get[wp]:
   "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>"
   by (clarsimp simp: exs_valid_def get_def)