From 8e81962b476cf7f313194c24f7bf736020364bef Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@proofcraft.systems>
Date: Mon, 30 Jan 2023 09:48:04 +1100
Subject: [PATCH] lib/monads: refactor + cleanup in No_Fail

- factor out valid_NF definition and lemmas into NonDetMonad_Total
- apply modern style and (very) occasional proof contraction in both

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
---
 lib/Monads/Monad_Equations.thy   |  12 +
 lib/Monads/No_Fail.thy           | 560 ++++---------------------------
 lib/Monads/NonDetMonad_Total.thy | 349 +++++++++++++++++++
 3 files changed, 424 insertions(+), 497 deletions(-)
 create mode 100644 lib/Monads/NonDetMonad_Total.thy

diff --git a/lib/Monads/Monad_Equations.thy b/lib/Monads/Monad_Equations.thy
index bbd3479da..f85ee9859 100644
--- a/lib/Monads/Monad_Equations.thy
+++ b/lib/Monads/Monad_Equations.thy
@@ -552,4 +552,16 @@ lemma bind_known_operation_eq:
   apply (fastforce simp: valid_def empty_fail_def)
   done
 
+lemma assert_opt_If:
+  "assert_opt v = If (v = None) fail (return (the v))"
+  by (simp add: assert_opt_def split: option.split)
+
+lemma if_to_top_of_bind:
+  "(bind (If P x y) z) = If P (bind x z) (bind y z)"
+  by (simp split: if_split)
+
+lemma if_to_top_of_bindE:
+  "(bindE (If P x y) z) = If P (bindE x z) (bindE y z)"
+  by (simp split: if_split)
+
 end
\ No newline at end of file
diff --git a/lib/Monads/No_Fail.thy b/lib/Monads/No_Fail.thy
index f4126ae94..9736a0874 100644
--- a/lib/Monads/No_Fail.thy
+++ b/lib/Monads/No_Fail.thy
@@ -17,58 +17,15 @@ begin
 subsection "Non-Failure"
 
 text \<open>
-  With the failure flag, we can formulate non-failure separately
-  from validity. A monad @{text m} does not fail under precondition
-  @{text P}, if for no start state in that precondition it sets
-  the failure flag.
+  With the failure flag, we can formulate non-failure separately from validity.
+  A monad @{text m} does not fail under precondition @{text P}, if for no start
+  state that satisfies the precondition it sets the failure flag.
 \<close>
-definition
-  no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> bool"
-where
-  "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> \<not> (snd (m s))"
+definition no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> bool" where
+  "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> \<not>snd (m s)"
 
 
-text \<open>
-  It is often desired to prove non-failure and a Hoare triple
-  simultaneously, as the reasoning is often similar. The following
-  definitions allow such reasoning to take place.
-\<close>
-
-definition
-  validNF ::"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
-      ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!")
-where
-  "validNF P f Q \<equiv> valid P f Q \<and> no_fail P f"
-
-definition
-  validE_NF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) nondet_monad \<Rightarrow>
-             ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow>
-             ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
-  ("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>!)")
-where
-  "validE_NF P f Q E \<equiv> validE P f Q E \<and> no_fail P f"
-
-lemma validE_NF_alt_def:
-  "\<lbrace> P \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! = \<lbrace> P \<rbrace> B \<lbrace> \<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s \<rbrace>!"
-  by (clarsimp simp: validE_NF_def validE_def validNF_def)
-
-lemma validNF_make_schematic_post:
-  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>!) \<Longrightarrow>
-   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>!"
-  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)
-
-lemma validE_NF_make_schematic_post:
-  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>!) \<Longrightarrow>
-   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
-        \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>!"
-  by (auto simp add: validE_NF_def validE_def valid_def no_fail_def split: prod.splits sum.splits)
-
-lemma validNF_conjD1: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
-  by (fastforce simp: validNF_def valid_def no_fail_def)
-
-lemma validNF_conjD2: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q' \<rbrace>!"
-  by (fastforce simp: validNF_def valid_def no_fail_def)
-
+subsection \<open>@{method wpc} setup\<close>
 
 lemma no_fail_pre[wp_pre]:
   "\<lbrakk> no_fail P f; \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> no_fail Q f"
@@ -78,29 +35,26 @@ lemma wpc_helper_no_fail_final:
   "no_fail Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (no_fail P f)"
   by (clarsimp simp: wpc_helper_def elim!: no_fail_pre)
 
-lemma wpc_helper_validNF:
-  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
-  apply (clarsimp simp: wpc_helper_def)
-  by (metis hoare_vcg_precond_imp no_fail_pre validNF_def)
-
 wpc_setup "\<lambda>m. no_fail P m" wpc_helper_no_fail_final
-wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_validNF
 
 
+subsection \<open>Bundles\<close>
+
 bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del]
 
-bundle classic_wp_pre = hoare_pre [wp_pre del]
-    all_classic_wp_combs[wp_comb del] all_classic_wp_combs[wp_comb]
+bundle classic_wp_pre =
+  hoare_pre [wp_pre del]
+  all_classic_wp_combs[wp_comb del]
+  all_classic_wp_combs[wp_comb]
 
 
-
-subsection "Non-Failure"
+subsection \<open>Lemmas\<close>
 
 lemma no_failD:
   "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> \<not>(snd (m s))"
   by (simp add: no_fail_def)
 
-lemma no_fail_modify [wp,simp]:
+lemma no_fail_modify[wp,simp]:
   "no_fail \<top> (modify f)"
   by (simp add: no_fail_def modify_def get_def put_def bind_def)
 
@@ -109,106 +63,92 @@ lemma no_fail_gets_simp[simp]:
   unfolding no_fail_def gets_def get_def return_def bind_def
   by simp
 
-lemma no_fail_gets:
+lemma no_fail_gets[wp]:
   "no_fail \<top> (gets f)"
   by simp
 
-lemma no_fail_select [simp]:
+lemma no_fail_select[simp]:
   "no_fail \<top> (select S)"
   by (simp add: no_fail_def select_def)
 
-lemma no_fail_alt [wp]:
+lemma no_fail_alt[wp]:
   "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)"
   by (simp add: no_fail_def alternative_def)
 
-lemma no_fail_return [simp, wp]:
+lemma no_fail_return[simp, wp]:
   "no_fail \<top> (return x)"
   by (simp add: return_def no_fail_def)
 
-lemma no_fail_get [simp, wp]:
+lemma no_fail_get[simp, wp]:
   "no_fail \<top> get"
   by (simp add: get_def no_fail_def)
 
-lemma no_fail_put [simp, wp]:
+lemma no_fail_put[simp, wp]:
   "no_fail \<top> (put s)"
   by (simp add: put_def no_fail_def)
 
-lemma no_fail_when [wp]:
+lemma no_fail_when[wp]:
   "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)"
   by (simp add: when_def)
 
-lemma no_fail_unless [wp]:
+lemma no_fail_unless[wp]:
   "(\<not>P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<top> else Q) (unless P f)"
   by (simp add: unless_def when_def)
 
-lemma no_fail_fail [simp, wp]:
+lemma no_fail_fail[simp, wp]:
   "no_fail \<bottom> fail"
   by (simp add: fail_def no_fail_def)
 
-lemmas [wp] = no_fail_gets
-
-lemma no_fail_assert [simp, wp]:
+lemma no_fail_assert[simp, wp]:
   "no_fail (\<lambda>_. P) (assert P)"
   by (simp add: assert_def)
 
-lemma no_fail_assert_opt [simp, wp]:
+lemma no_fail_assert_opt[simp, wp]:
   "no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)"
   by (simp add: assert_opt_def split: option.splits)
 
-lemma no_fail_case_option [wp]:
+lemma no_fail_case_option[wp]:
   assumes f: "no_fail P f"
   assumes g: "\<And>x. no_fail (Q x) (g x)"
   shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)"
   by (clarsimp simp add: f g)
 
-lemma no_fail_if [wp]:
-  "\<lbrakk> P \<Longrightarrow> no_fail Q f; \<not>P \<Longrightarrow> no_fail R g \<rbrakk> \<Longrightarrow>
-  no_fail (if P then Q else R) (if P then f else g)"
+lemma no_fail_if[wp]:
+  "\<lbrakk> P \<Longrightarrow> no_fail Q f; \<not>P \<Longrightarrow> no_fail R g \<rbrakk> \<Longrightarrow> no_fail (if P then Q else R) (if P then f else g)"
   by simp
 
-lemma no_fail_apply [wp]:
+lemma no_fail_apply[wp]:
   "no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)"
   by simp
 
-lemma no_fail_undefined [simp, wp]:
+lemma no_fail_undefined[simp, wp]:
   "no_fail \<bottom> undefined"
   by (simp add: no_fail_def)
 
-lemma no_fail_returnOK [simp, wp]:
+lemma no_fail_returnOK[simp, wp]:
   "no_fail \<top> (returnOk x)"
   by (simp add: returnOk_def)
 
-lemma no_fail_bind [wp]:
-  assumes f: "no_fail P f"
-  assumes g: "\<And>rv. no_fail (R rv) (g rv)"
-  assumes v: "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>"
-  shows "no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
-  apply (clarsimp simp: no_fail_def bind_def)
-  apply (rule conjI)
-   prefer 2
-   apply (erule no_failD [OF f])
-  apply clarsimp
-  apply (drule (1) use_valid [OF _ v])
-  apply (drule no_failD [OF g])
-  apply simp
-  done
-
+lemma no_fail_bind[wp]:
+  "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
+  unfolding no_fail_def bind_def
+  using post_by_hoare by fastforce
 
 lemma no_fail_assume_pre:
   "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
 
-lemma no_fail_liftM_eq [simp]:
+lemma no_fail_liftM_eq[simp]:
   "no_fail P (liftM f m) = no_fail P m"
   by (auto simp: liftM_def no_fail_def bind_def return_def)
 
-lemma no_fail_select_f [wp]:
+lemma no_fail_select_f[wp]:
   "no_fail (\<lambda>s. \<not>snd S) (select_f S)"
   by (simp add: select_f_def no_fail_def)
 
-lemma no_fail_liftM [wp]:
+lemma no_fail_liftM[wp]:
   "no_fail P m \<Longrightarrow> no_fail P (liftM f m)"
-  by (simp)
+  by simp
 
 lemma no_fail_pre_and:
   "no_fail P f \<Longrightarrow> no_fail (P and Q) f"
@@ -218,7 +158,7 @@ lemma no_fail_spec:
   "\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
 
-lemma no_fail_assertE [wp]:
+lemma no_fail_assertE[wp]:
   "no_fail (\<lambda>_. P) (assertE P)"
   by (simp add: assertE_def split: if_split)
 
@@ -226,77 +166,44 @@ lemma no_fail_spec_pre:
   "\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f"
   by (erule no_fail_pre, simp)
 
-lemma no_fail_whenE [wp]:
+lemma no_fail_whenE[wp]:
   "\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)"
   by (simp add: whenE_def split: if_split)
 
-lemma no_fail_unlessE [wp]:
+lemma no_fail_unlessE[wp]:
   "\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)"
   by (simp add: unlessE_def split: if_split)
 
-lemma no_fail_throwError [wp]:
+lemma no_fail_throwError[wp]:
   "no_fail \<top> (throwError e)"
   by (simp add: throwError_def)
 
-lemma no_fail_liftE [wp]:
+lemma no_fail_liftE[wp]:
   "no_fail P f \<Longrightarrow> no_fail P (liftE f)"
   unfolding liftE_def by wpsimp
 
-lemma no_fail_gets_the [wp]:
+lemma no_fail_gets_the[wp]:
   "no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)"
-  apply (simp add: gets_the_def)
-  apply (rule no_fail_pre, wp)
-  apply simp
-  done
+  unfolding gets_the_def
+  by wpsimp
 
-lemma assert_opt_If:
-  "assert_opt v = If (v = None) fail (return (the v))"
-  by (simp_all add: assert_opt_def split: option.split)
+lemma no_fail_lift:
+  "(\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not>isl x \<longrightarrow> P s) (lift f x)"
+  unfolding lift_def
+  by (wpsimp wp: no_fail_throwError split: sum.splits | assumption)+
 
-lemma if_to_top_of_bind:
-  "(bind (If P x y) z) = If P (bind x z) (bind y z)"
-  by (simp split: if_split)
+lemma validE_R_valid_eq:
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace>"
+  unfolding validE_R_def validE_def valid_def
+  by (fastforce split: sum.splits prod.split)
 
-lemma if_to_top_of_bindE:
-  "(bindE (If P x y) z) = If P (bindE x z) (bindE y z)"
-  by (simp split: if_split)
-
-lemma alternative_bind:
-  "((a \<sqinter> b) >>= c) = ((a >>= c) \<sqinter> (b >>= c))"
-  apply (rule ext, simp add: alternative_def bind_def split_def)
-  apply blast
-  done
-
-lemma alternative_refl:
-  "(a \<sqinter> a) = a"
-  by (rule ext, simp add: alternative_def)
-
-lemma alternative_com:
-  "(f \<sqinter> g) = (g \<sqinter> f)"
-  apply (rule ext)
-  apply (auto simp: alternative_def)
-  done
-
-lemma liftE_alternative:
-  "liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)"
-  by (simp add: liftE_def alternative_bind)
-
-lemma no_fail_bindE [wp]:
+lemma no_fail_bindE[wp]:
   "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk>
      \<Longrightarrow> no_fail (P and Q) (f >>=E g)"
-  apply (simp add: bindE_def)
-  apply (erule no_fail_bind)
-   apply (simp add: lift_def)
-   apply wpc
-    apply (simp add: throwError_def)
-    apply wp
-   apply assumption
-  apply (simp add: validE_R_def validE_def)
-  apply (erule hoare_strengthen_post)
-  apply clarsimp
-  done
+  unfolding bindE_def
+  by (wpsimp wp: no_fail_lift simp: validE_R_valid_eq | assumption)+
 
-lemma no_fail_False [simp]:
+lemma no_fail_False[simp]:
   "no_fail (\<lambda>_. False) X"
   by (clarsimp simp: no_fail_def)
 
@@ -313,350 +220,9 @@ lemma no_fail_state_assert[wp]:
   unfolding state_assert_def
   by wpsimp
 
-section "validNF Rules"
-
-subsection "Basic validNF theorems"
-
-lemma validNF [intro?]:
-  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
-  by (clarsimp simp: validNF_def)
-
-lemma validNF_valid: "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
-  by (clarsimp simp: validNF_def)
-
-lemma validNF_no_fail: "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
-  by (clarsimp simp: validNF_def)
-
-lemma snd_validNF:
-  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> \<not> snd (f s)"
-  by (clarsimp simp: validNF_def no_fail_def)
-
-lemma use_validNF:
-  "\<lbrakk> (r', s') \<in> fst (f s); \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Q r' s'"
-  by (fastforce simp: validNF_def valid_def)
-
-subsection "validNF weakest pre-condition rules"
-
-lemma validNF_return [wp]:
-  "\<lbrace> P x \<rbrace> return x \<lbrace> P \<rbrace>!"
-  by (wp validNF)+
-
-lemma validNF_get [wp]:
-  "\<lbrace> \<lambda>s. P s s  \<rbrace> get \<lbrace> P \<rbrace>!"
-  by (wp validNF)+
-
-lemma validNF_put [wp]:
-  "\<lbrace> \<lambda>s. P () x  \<rbrace> put x \<lbrace> P \<rbrace>!"
-  by (wp validNF)+
-
-lemma validNF_K_bind [wp]:
-  "\<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> K_bind x f \<lbrace> Q \<rbrace>!"
-  by simp
-
-lemma validNF_fail [wp]:
-  "\<lbrace> \<lambda>s. False \<rbrace> fail \<lbrace> Q \<rbrace>!"
-  by (clarsimp simp: validNF_def fail_def no_fail_def)
-
-lemma validNF_prop [wp_unsafe]:
-  "\<lbrakk> no_fail (\<lambda>s. P) f \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s. P \<rbrace> f \<lbrace> \<lambda>rv s. P \<rbrace>!"
-  by (wp validNF)+
-
-lemma validNF_post_conj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>!"
-  by (auto simp: validNF_def)
-
-lemma validNF_pre_disj [intro!]:
-  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>!; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>!"
-  by (rule validNF) (auto dest: validNF_valid validNF_no_fail intro: no_fail_or)
-
-(*
- * Set up combination rules for WP, which also requires
- * a "wp_trip" rule for validNF.
- *)
-
-definition "validNF_property Q s b \<equiv> \<not> snd (b s) \<and> (\<forall>(r', s') \<in> fst (b s). Q r' s')"
-
-lemma validNF_is_triple [wp_trip]:
-  "validNF P f Q = triple_judgement P f (validNF_property Q)"
-  apply (clarsimp simp: validNF_def triple_judgement_def validNF_property_def)
-  apply (auto simp: no_fail_def valid_def)
-  done
-
-lemma validNF_weaken_pre[wp_pre]:
-  "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
-  by (metis hoare_pre_imp no_fail_pre validNF_def)
-
-lemma validNF_post_comb_imp_conj:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  by (fastforce simp: validNF_def valid_def)
-
-lemma validNF_post_comb_conj_L:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (clarsimp simp: validNF_def valid_def no_fail_def)
-  apply force
-  done
-
-lemma validNF_post_comb_conj_R:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (clarsimp simp: validNF_def valid_def no_fail_def)
-  apply force
-  done
-
-lemma validNF_post_comb_conj:
-  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (clarsimp simp: validNF_def valid_def no_fail_def)
-  apply force
-  done
-
-lemma validNF_if_split [wp_split]:
-  "\<lbrakk>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>!; \<not> P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>!"
-  by simp
-
-lemma validNF_vcg_conj_lift:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow>
-      \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
-  apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule validNF_post_conj)
-   apply (erule validNF_weaken_pre, fastforce)
-  apply (erule validNF_weaken_pre, fastforce)
-  done
-
-lemma validNF_vcg_disj_lift:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow>
-       \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>!"
-  apply (clarsimp simp: validNF_def)
-  apply safe
-   apply (auto intro!: hoare_vcg_disj_lift)[1]
-  apply (clarsimp simp: no_fail_def)
-  done
-
-lemma validNF_vcg_all_lift [wp]:
-  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>!"
-  apply atomize
-  apply (rule validNF)
-   apply (clarsimp simp: validNF_def)
-   apply (rule hoare_vcg_all_lift)
-   apply force
-  apply (clarsimp simp: no_fail_def validNF_def)
-  done
-
-lemma validNF_bind [wp_split]:
-  "\<lbrakk> \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>! \<rbrakk> \<Longrightarrow>
-       \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>!"
-  apply (rule validNF)
-   apply (metis validNF_valid hoare_seq_ext)
-  apply (clarsimp simp: no_fail_def validNF_def bind_def' valid_def)
-  apply blast
-  done
-
-lemmas validNF_seq_ext = validNF_bind
-
-subsection "validNF compound rules"
-
-lemma validNF_state_assert [wp]:
-  "\<lbrace> \<lambda>s. P () s \<and> G s  \<rbrace> state_assert G \<lbrace> P \<rbrace>!"
-  apply (rule validNF)
-   apply wpsimp
-  apply (clarsimp simp: no_fail_def state_assert_def
-              bind_def' assert_def return_def get_def)
-  done
-
-lemma validNF_modify [wp]:
-  "\<lbrace> \<lambda>s. P () (f s) \<rbrace> modify f \<lbrace> P \<rbrace>!"
-  apply (clarsimp simp: modify_def)
-  apply wp
-  done
-
-lemma validNF_gets [wp]:
-  "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>!"
-  apply (clarsimp simp: gets_def)
-  apply wp
-  done
-
-lemma validNF_condition [wp]:
-  "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>!"
-  apply rule
-   apply (drule validNF_valid)+
-   apply (erule (1) condition_wp)
-  apply (drule validNF_no_fail)+
-  apply (clarsimp simp: no_fail_def condition_def)
-  done
-
-lemma validNF_alt_def:
-  "validNF P m Q = (\<forall>s. P s \<longrightarrow> ((\<forall>(r', s') \<in> fst (m s). Q r' s') \<and> \<not> snd (m s)))"
-  by (fastforce simp: validNF_def valid_def no_fail_def)
-
-lemma validNF_assert [wp]:
-    "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
-  apply (rule validNF)
-   apply (clarsimp simp: valid_def in_return)
-  apply (clarsimp simp: no_fail_def return_def)
-  done
-
-lemma validNF_false_pre:
-  "\<lbrace> \<lambda>_. False \<rbrace> P \<lbrace> Q \<rbrace>!"
-  by (clarsimp simp: validNF_def no_fail_def)
-
-lemma validNF_chain:
-   "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. R' r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
-  by (fastforce simp: validNF_def valid_def no_fail_def Ball_def)
-
-lemma validNF_case_prod [wp]:
-  "\<lbrakk> \<And>x y. validNF (P x y) (B x y) Q \<rbrakk> \<Longrightarrow> validNF (case_prod P v) (case_prod (\<lambda>x y. B x y) v) Q"
-  by (metis prod.exhaust split_conv)
-
-lemma validE_NF_case_prod [wp]:
-    "\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
-          \<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def)
-  apply (erule validNF_case_prod)
-  done
-
-lemma no_fail_is_validNF_True: "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
-  by (clarsimp simp: no_fail_def validNF_def valid_def)
-
-subsection "validNF reasoning in the exception monad"
-
-lemma validE_NF [intro?]:
-  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!"
-  apply (clarsimp simp: validE_NF_def)
-  done
-
-lemma validE_NF_valid:
-  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
-  apply (clarsimp simp: validE_NF_def)
-  done
-
-lemma validE_NF_no_fail:
-  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
-  apply (clarsimp simp: validE_NF_def)
-  done
-
-lemma validE_NF_weaken_pre[wp_pre]:
-   "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def)
-  apply (erule validNF_weaken_pre)
-  apply simp
-  done
-
-lemma validE_NF_post_comb_conj_L:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> E \<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def
-          valid_def no_fail_def split: sum.splits)
-  apply force
-  done
-
-lemma validE_NF_post_comb_conj_R:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def
-          valid_def no_fail_def split: sum.splits)
-  apply force
-  done
-
-lemma validE_NF_post_comb_conj:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> E \<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def
-          valid_def no_fail_def split: sum.splits)
-  apply force
-  done
-
-lemma validE_NF_chain:
-   "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>,\<lbrace>E'\<rbrace>!;
-    \<And>s. P s \<Longrightarrow> P' s;
-    \<And>r' s'. R' r' s' \<Longrightarrow> R r' s';
-    \<And>r'' s''. E' r'' s'' \<Longrightarrow> E r'' s''\<rbrakk> \<Longrightarrow>
-  \<lbrace>\<lambda>s. P s \<rbrace> a \<lbrace>\<lambda>r' s'. R r' s'\<rbrace>,\<lbrace>\<lambda>r'' s''. E r'' s''\<rbrace>!"
-  by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits)
-
-lemma validE_NF_bind_wp [wp]:
-  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!"
-  apply (unfold validE_NF_alt_def bindE_def)
-  apply (rule validNF_bind [rotated])
-   apply assumption
-  apply (clarsimp simp: lift_def throwError_def split: sum.splits)
-  apply wpsimp
-  done
-
-lemma validNF_catch [wp]:
-  "\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!"
-  apply (unfold validE_NF_alt_def catch_def)
-  apply (rule validNF_bind [rotated])
-   apply assumption
-  apply (clarsimp simp: lift_def throwError_def split: sum.splits)
-  apply wp
-  done
-
-lemma validNF_throwError [wp]:
-  "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
-  by (unfold validE_NF_alt_def throwError_def o_def) wpsimp
-
-lemma validNF_returnOk [wp]:
-  "\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
-  by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
-
-lemma validNF_whenE [wp]:
-  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!"
-  unfolding whenE_def by clarsimp wp
-
-lemma validNF_nobindE [wp]:
-  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!;
-     \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
-   \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!"
-  by clarsimp wp
-
-text \<open>
-Setup triple rules for @{term validE_NF} so that we can use
-wp combinator rules.
-\<close>
-
-definition "validE_NF_property Q E s b \<equiv> \<not> snd (b s)
-       \<and> (\<forall>(r', s') \<in> fst (b s). case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> Q x s')"
-
-lemma validE_NF_is_triple [wp_trip]:
-  "validE_NF P f Q E = triple_judgement P f (validE_NF_property Q E)"
-  apply (clarsimp simp: validE_NF_def validE_def2 no_fail_def triple_judgement_def
-           validE_NF_property_def split: sum.splits)
-  apply blast
-  done
-
-lemma validNF_cong:
-   "\<lbrakk> \<And>s. P s = P' s; \<And>s. P s \<Longrightarrow> m s = m' s;
-           \<And>r' s' s. \<lbrakk> P s; (r', s') \<in> fst (m s) \<rbrakk> \<Longrightarrow> Q r' s' = Q' r' s' \<rbrakk> \<Longrightarrow>
-     (\<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>!) = (\<lbrace> P' \<rbrace> m' \<lbrace> Q' \<rbrace>!)"
-  by (fastforce simp: validNF_alt_def)
-
-lemma validE_NF_liftE [wp]:
-  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
-  by (wpsimp simp: validE_NF_alt_def liftE_def)
-
-lemma validE_NF_handleE' [wp]:
-  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
-   \<lbrace>P\<rbrace> f <handle2> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
-  apply (unfold validE_NF_alt_def handleE'_def)
-  apply (rule validNF_bind [rotated])
-   apply assumption
-  apply (clarsimp split: sum.splits)
-  apply wpsimp
-  done
-
-lemma validE_NF_handleE [wp]:
-  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
-   \<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
-  apply (unfold handleE_def)
-  apply (metis validE_NF_handleE')
-  done
-
-lemma validE_NF_condition [wp]:
-  "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!\<rbrakk>
-      \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!"
-  apply rule
-   apply (drule validE_NF_valid)+
-   apply wp
-  apply (drule validE_NF_no_fail)+
-  apply (clarsimp simp: no_fail_def condition_def)
-  done
-
-lemma hoare_assume_preNF:
-  "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"
-  by (metis validNF_alt_def)
+lemma no_fail_condition:
+  "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)"
+  unfolding condition_def no_fail_def
+  by clarsimp
 
 end
diff --git a/lib/Monads/NonDetMonad_Total.thy b/lib/Monads/NonDetMonad_Total.thy
new file mode 100644
index 000000000..7ad256f5a
--- /dev/null
+++ b/lib/Monads/NonDetMonad_Total.thy
@@ -0,0 +1,349 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Total correctness Hoare logic for the NonDetMonad (= valid + no_fail) *)
+
+theory NonDetMonad_Total
+  imports No_Fail
+begin
+
+section \<open>Total correctness for NonDetMonad and NonDetMonad with exceptions\<close>
+
+subsection Definitions
+
+text \<open>
+  It is often desired to prove non-failure and a Hoare triple simultaneously, as the reasoning
+  is often similar. The following definitions allow such reasoning to take place.\<close>
+
+definition validNF ::
+  "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") where
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<equiv> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> no_fail P f"
+
+lemma validNF_alt_def:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! = (\<forall>s. P s \<longrightarrow> ((\<forall>(r', s') \<in> fst (f s). Q r' s') \<and> \<not> snd (f s)))"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+definition validE_NF ::
+  "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
+  ("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>!)") where
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<equiv> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<and> no_fail P f"
+
+lemma validE_NF_alt_def:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!"
+  by (clarsimp simp: validE_NF_def validE_def validNF_def)
+
+
+subsection \<open>@{method wpc} setup\<close>
+
+lemma wpc_helper_validNF:
+  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!"
+  unfolding wpc_helper_def
+  by clarsimp (metis hoare_vcg_precond_imp no_fail_pre validNF_def)
+
+wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_validNF
+
+
+subsection \<open>Basic @{const validNF} theorems\<close>
+
+lemma validNF_make_schematic_post:
+  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>!) \<Longrightarrow>
+   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>!"
+  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)
+
+lemma validE_NF_make_schematic_post:
+  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>!) \<Longrightarrow>
+   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
+        \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>!"
+  by (auto simp add: validE_NF_def validE_def valid_def no_fail_def split: prod.splits sum.splits)
+
+lemma validNF_conjD1:
+  "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF_conjD2:
+  "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q' \<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF[intro?]: (* FIXME lib: should be validNFI *)
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
+  by (clarsimp simp: validNF_def)
+
+lemma validNFE:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+  by (clarsimp simp: validNF_def)
+
+lemma validNF_valid:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
+  by (erule validNFE)
+
+lemma validNF_no_fail:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
+  by (erule validNFE)
+
+lemma snd_validNF:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> \<not> snd (f s)"
+  by (clarsimp simp: validNF_def no_fail_def)
+
+lemma use_validNF:
+  "\<lbrakk> (r', s') \<in> fst (f s); \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Q r' s'"
+  by (fastforce simp: validNF_def valid_def)
+
+
+subsection \<open>@{const validNF} weakest precondition rules\<close>
+
+lemma validNF_return[wp]:
+  "\<lbrace> P x \<rbrace> return x \<lbrace> P \<rbrace>!"
+  by (wp validNF)+
+
+lemma validNF_get[wp]:
+  "\<lbrace> \<lambda>s. P s s  \<rbrace> get \<lbrace> P \<rbrace>!"
+  by (wp validNF)+
+
+lemma validNF_put[wp]:
+  "\<lbrace> \<lambda>s. P () x  \<rbrace> put x \<lbrace> P \<rbrace>!"
+  by (wp validNF)+
+
+lemma validNF_K_bind[wp]:
+  "\<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> K_bind x f \<lbrace> Q \<rbrace>!"
+  by simp
+
+lemma validNF_fail[wp]:
+  "\<lbrace> \<lambda>s. False \<rbrace> fail \<lbrace> Q \<rbrace>!"
+  by (clarsimp simp: validNF_def fail_def no_fail_def)
+
+lemma validNF_prop[wp_unsafe]:
+  "\<lbrakk> no_fail (\<lambda>s. P) f \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s. P \<rbrace> f \<lbrace> \<lambda>rv s. P \<rbrace>!"
+  by (wp validNF)+
+
+lemma validNF_post_conj[intro!]:
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>!"
+  by (auto simp: validNF_def)
+
+lemma validNF_pre_disj[intro!]:
+  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>!; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>!"
+  by (rule validNF) (auto dest: validNF_valid validNF_no_fail intro: no_fail_or)
+
+text \<open>
+  Set up combination rules for @{method wp}, which also requires a @{text wp_trip} rule for
+  @{const validNF}.\<close>
+definition validNF_property :: "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> bool" where
+  "validNF_property Q s b \<equiv> \<not> snd (b s) \<and> (\<forall>(r', s') \<in> fst (b s). Q r' s')"
+
+lemma validNF_is_triple[wp_trip]:
+  "validNF P f Q = triple_judgement P f (validNF_property Q)"
+  by (auto simp: validNF_def triple_judgement_def validNF_property_def no_fail_def valid_def)
+
+lemma validNF_weaken_pre[wp_pre]:
+  "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
+  by (metis hoare_pre_imp no_fail_pre validNF_def)
+
+lemma validNF_post_comb_imp_conj:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
+  by (fastforce simp: validNF_def valid_def)
+
+lemma validNF_post_comb_conj_L:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF_post_comb_conj_R:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF_post_comb_conj:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF_if_split[wp_split]:
+  "\<lbrakk>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>!; \<not> P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>!\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>!"
+  by simp
+
+lemma validNF_vcg_conj_lift:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!"
+  by (fastforce intro!: validNF_post_conj[unfolded pred_conj_def] intro: validNF_weaken_pre)
+
+lemma validNF_vcg_disj_lift:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>!"
+  by (auto  simp: validNF_def no_fail_def intro!: hoare_vcg_disj_lift)
+
+lemma validNF_vcg_all_lift[wp]:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>!"
+  by (auto simp: validNF_def no_fail_def intro!: hoare_vcg_all_lift)
+
+lemma validNF_bind[wp_split]:
+  "\<lbrakk> \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>!"
+  unfolding validNF_def
+  by (auto intro: hoare_seq_ext no_fail_bind[where P=Q and Q=Q for Q, simplified])
+
+lemmas validNF_seq_ext = validNF_bind
+
+
+subsection "validNF compound rules"
+
+lemma validNF_state_assert[wp]:
+  "\<lbrace> \<lambda>s. P () s \<and> G s  \<rbrace> state_assert G \<lbrace> P \<rbrace>!"
+  by (rule validNF; wpsimp)
+
+lemma validNF_modify[wp]:
+  "\<lbrace> \<lambda>s. P () (f s) \<rbrace> modify f \<lbrace> P \<rbrace>!"
+  by (rule validNF; wpsimp)
+
+lemma validNF_gets[wp]:
+  "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>!"
+  by (rule validNF; wpsimp)
+
+lemma validNF_condition[wp]:
+  "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>!"
+  by (erule validNFE)+
+     (rule validNF; wpsimp wp: no_fail_condition)
+
+lemma validNF_assert[wp]:
+  "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
+  by (rule validNF; wpsimp)
+
+lemma validNF_false_pre:
+  "\<lbrace> \<lambda>_. False \<rbrace> P \<lbrace> Q \<rbrace>!"
+  by (rule validNF; wpsimp)
+
+lemma validNF_chain:
+   "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. R' r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def Ball_def)
+
+lemma validNF_case_prod[wp]:
+  "(\<And>x y. \<lbrace>P x y\<rbrace> B x y \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>case v of (x, y) \<Rightarrow> P x y\<rbrace> case v of (x, y) \<Rightarrow> B x y \<lbrace>Q\<rbrace>!"
+  by (metis prod.exhaust split_conv)
+
+lemma validE_NF_case_prod[wp]:
+  "\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def
+  by (erule validNF_case_prod)
+
+lemma no_fail_is_validNF_True:
+  "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
+  by (clarsimp simp: no_fail_def validNF_def valid_def)
+
+
+subsection \<open>@{const validNF} reasoning in the exception monad\<close>
+
+lemma validE_NF[intro?]: (* FIXME lib: should be validE_NFI *)
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!"
+  by (clarsimp simp: validE_NF_def)
+
+lemma validE_NFE:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+  by (clarsimp simp: validE_NF_def)
+
+lemma validE_NF_valid:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
+  by (rule validE_NFE)
+
+lemma validE_NF_no_fail:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
+  by (rule validE_NFE)
+
+lemma validE_NF_weaken_pre[wp_pre]:
+  "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!"
+  by (simp add: validE_NF_alt_def validNF_weaken_pre)
+
+lemma validE_NF_post_comb_conj_L:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def
+  by (fastforce simp: validE_def validNF_def valid_def no_fail_def split: sum.splits)
+
+lemma validE_NF_post_comb_conj_R:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def validE_def validNF_def valid_def no_fail_def
+  by (fastforce split: sum.splits)
+
+lemma validE_NF_post_comb_conj:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def validE_def validNF_def valid_def no_fail_def
+  by (fastforce split: sum.splits)
+
+lemma validE_NF_chain:
+  "\<lbrakk> \<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>,\<lbrace>E'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r' s'. R' r' s' \<Longrightarrow> R r' s';
+     \<And>r'' s''. E' r'' s'' \<Longrightarrow> E r'' s''\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P s \<rbrace> a \<lbrace>\<lambda>r' s'. R r' s'\<rbrace>,\<lbrace>\<lambda>r'' s''. E r'' s''\<rbrace>!"
+  by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits)
+
+lemma validE_NF_bind_wp[wp]:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!"
+  by (blast intro: validE_NF hoare_vcg_seqE no_fail_pre no_fail_bindE validE_validE_R validE_weaken
+            elim!: validE_NFE)
+
+lemma validNF_catch[wp]:
+  "\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!"
+  unfolding validE_NF_alt_def catch_def lift_def throwError_def
+  by (clarsimp simp: validNF_return split: sum.splits elim!: validNF_bind[rotated])
+
+lemma validNF_throwError[wp]:
+  "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
+  by (unfold validE_NF_alt_def throwError_def o_def) wpsimp
+
+lemma validNF_returnOk[wp]:
+  "\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
+  by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
+
+lemma validNF_whenE[wp]:
+  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding whenE_def by wpsimp
+
+lemma validNF_nobindE[wp]:
+  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!"
+  by wpsimp
+
+text \<open>
+  Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\<close>
+definition validE_NF_property ::
+  "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> ('s, 'c+'a) nondet_monad \<Rightarrow> bool" where
+  "validE_NF_property Q E s b \<equiv>
+   \<not> snd (b s) \<and> (\<forall>(r', s') \<in> fst (b s). case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> Q x s')"
+
+lemma validE_NF_is_triple[wp_trip]:
+  "validE_NF P f Q E = triple_judgement P f (validE_NF_property Q E)"
+  by (fastforce simp: validE_NF_def validE_def2 no_fail_def triple_judgement_def
+                      validE_NF_property_def
+                split: sum.splits)
+
+lemma validNF_cong:
+  "\<lbrakk> \<And>s. P s = P' s; \<And>s. P s \<Longrightarrow> m s = m' s;
+     \<And>r' s' s. \<lbrakk> P s; (r', s') \<in> fst (m s) \<rbrakk> \<Longrightarrow> Q r' s' = Q' r' s' \<rbrakk> \<Longrightarrow>
+   (\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!) = (\<lbrace>P'\<rbrace> m' \<lbrace>Q'\<rbrace>!)"
+  by (fastforce simp: validNF_alt_def)
+
+lemma validE_NF_liftE[wp]:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
+  by (wpsimp simp: validE_NF_alt_def liftE_def)
+
+lemma validE_NF_handleE'[wp]:
+  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>P\<rbrace> f <handle2> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def handleE'_def
+  apply (erule validNF_bind[rotated])
+  apply (clarsimp split: sum.splits)
+  apply wpsimp
+  done
+
+lemma validE_NF_handleE[wp]:
+  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
+  unfolding handleE_def
+  by (metis validE_NF_handleE')
+
+lemma validE_NF_condition[wp]:
+  "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!"
+  by (erule validE_NFE)+ (wpsimp wp: no_fail_condition validE_NF)
+
+lemma hoare_assume_preNF:
+  "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"
+  by (metis validNF_alt_def)
+
+end
\ No newline at end of file