lib/monads: style cleanup in No_Throw

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

lib/Monads/No_Throw.thy

@@ -17,26 +17,27 @@ begin
 section "Basic exception reasoning"
 
 text \<open>
-  The following predicates @{text no_throw} and @{text no_return} allow
-  reasoning about functions in the exception monad that either never
-  throw an exception or never return normally.
-\<close>
+  The predicates @{text no_throw} and @{text no_return} allow us to reason about functions in
+  the exception monad that never throw an exception or never return normally.\<close>
 
-definition "no_throw P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_ _. False \<rbrace>"
+definition no_throw :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) nondet_monad \<Rightarrow> bool" where
+  "no_throw P A \<equiv> \<lbrace>P\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>"
 
-definition "no_return P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>,\<lbrace>\<lambda>_ _. True \<rbrace>"
+definition no_return :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b + 'c) nondet_monad \<Rightarrow> bool" where
+  "no_return P A \<equiv> \<lbrace>P\<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>"
 
 (* Alternative definition of no_throw; easier to work with than unfolding validE. *)
 lemma no_throw_def':
   "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> fst (A s). (\<exists>x. r = Inr x)))"
   by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
 
-lemma no_throw_returnOk [simp]:
+
+lemma no_throw_returnOk[simp]:
   "no_throw P (returnOk a)"
   unfolding no_throw_def
   by wp
 
-lemma no_throw_liftE [simp]:
+lemma no_throw_liftE[simp]:
   "no_throw P (liftE x)"
   by (wpsimp simp: liftE_def no_throw_def validE_def)
 
@@ -44,43 +45,21 @@ lemma no_throw_bindE:
   "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
    \<Longrightarrow> no_throw A (X >>=E Y)"
   unfolding no_throw_def
-  apply (rule seqE[rotated])
-   apply force
-  apply (rule hoare_validE_cases; simp)
-  done
+  using hoare_validE_cases seqE by blast
 
 lemma no_throw_bindE_simple:
   "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)"
-  apply (erule no_throw_bindE)
-   apply assumption
-  apply wp
-  done
+  using hoareE_TrueI no_throw_bindE by blast
 
 lemma no_throw_handleE_simple:
-  notes hoare_vcg_prop[wp del]
-  shows "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
-  unfolding no_throw_def
-  apply atomize
-  apply clarsimp
-  apply (erule disjE)
-   apply (wpsimp wp: hoare_vcg_prop[where f="R x" for x])
-    apply assumption
-   apply simp
-  apply (rule handleE_wp)
-   apply (erule_tac x=x in allE)
-   apply assumption
-  apply wp
-  done
+  "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
+  by (fastforce simp: no_throw_def' handleE_def handleE'_def validE_def valid_def bind_def return_def
+                split: sum.splits)
 
 lemma no_throw_handle2:
   "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)"
-  apply (clarsimp simp: no_throw_def' handleE'_def bind_def)
-  apply (clarsimp simp: validE_def valid_def)
-  apply (erule allE, erule (1) impE)
-  apply (drule (1) bspec)
-  apply (clarsimp simp: return_def split: sum.splits)
-  apply force
-  done
+  by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def
+                split: sum.splits)
 
 lemma no_throw_handle:
   "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)"
@@ -100,27 +79,17 @@ lemma bindE_fail_propagates:
 lemma whileLoopE_nothrow:
   "\<lbrakk> \<And>x. no_throw \<top> (B x) \<rbrakk> \<Longrightarrow> no_throw \<top> (whileLoopE C B x)"
   unfolding no_throw_def
-  apply (rule validE_whileLoopE [where I="\<lambda>_ _. True"])
-    apply simp
-   apply (rule validE_weaken; force)
-  apply simp
-  done
+  by (fastforce intro!: validE_whileLoopE intro: validE_weaken)
 
 lemma handleE'_nothrow_lhs:
-  "\<lbrakk> no_throw \<top> L \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)"
+  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)"
   unfolding no_throw_def
-  apply (rule handleE'_wp[rotated])
-   apply assumption
-  apply simp
-  done
+  using handleE'_wp[rotated] by fastforce
 
 lemma handleE'_nothrow_rhs:
   "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)"
   unfolding no_throw_def
-  apply (rule handleE'_wp)
-   apply assumption
-  apply (rule hoareE_TrueI)
-  done
+  by (metis hoareE_TrueI no_throw_def no_throw_handle2)
 
 lemma handleE_nothrow_lhs:
   "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle> R)"
@@ -140,12 +109,9 @@ lemma no_throw_Inr:
 
 lemma no_throw_handleE':
   "no_throw \<top> A \<Longrightarrow> (A <handle2> B) = A"
-  apply (rule monad_eqI)
-    apply monad_eq
+  apply (rule monad_eqI; monad_eq)
     apply (fastforce dest: no_throw_Inr)
-   apply monad_eq
    apply (metis (lifting) fst_conv no_throw_Inr)
-  apply monad_eq
   apply (fastforce dest: no_throw_Inr)
   done
 
@@ -156,8 +122,6 @@ lemma no_throw_handleE:
 
 lemma bindE_handleE_join:
   "no_throw \<top> A \<Longrightarrow> (A >>=E (\<lambda>x. (B x) <handle> C)) = ((A >>=E B <handle> C))"
-  apply (monad_eq simp: Bex_def Ball_def no_throw_def')
-  apply blast
-  done
+  by (monad_eq simp: Bex_def Ball_def no_throw_def') blast
 
 end