monads: synchronise with rt branch

Signed-off-by: Corey Lewis <corey.lewis@unsw.edu.au>

lib/Monads/NonDetMonadVCG.thy

@@ -306,6 +306,8 @@ lemma hoare_gen_asm:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp add: valid_def)
 
+lemmas hoare_gen_asm_single = hoare_gen_asm[where P'="\<top>", simplified pred_conj_def simp_thms]
+
 lemma hoare_gen_asm_lk:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>K P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp add: valid_def)

lib/Monads/OptionMonadWP.thy

@@ -21,8 +21,10 @@ begin
    TODO: design a sensible syntax for them. *)
 
 (* Partial correctness. *)
-definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
-  "ovalid P f Q \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
+definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
+  ("\<lblot>_\<rblot>/ _ /\<lblot>_\<rblot>") where
+  "\<lblot>P\<rblot> f \<lblot>Q\<rblot> \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
+
 (* Total correctness. *)
 definition ovalidNF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
   "ovalidNF P f Q \<equiv> \<forall>s. P s \<longrightarrow> (f s \<noteq> None \<and> (\<forall>r. f s = Some r \<longrightarrow> Q r s))"
@@ -57,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric]
 
 
 (* WP rules for ovalid. *)
+lemma ovalid_inv[wp]:
+  "ovalid P f (\<lambda>_. P)"
+  by (simp add: ovalid_def)
+
 lemma obind_wp[wp]:
   "\<lbrakk> \<And>r. ovalid (R r) (g r) Q; ovalid P f R \<rbrakk> \<Longrightarrow> ovalid P (obind f g) Q"
   by (simp add: ovalid_def obind_def split: option.splits, fast)

lib/Monads/WhileLoopRules.thy

@@ -383,6 +383,22 @@ lemma whileLoop_wp:
   \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
   by (rule valid_whileLoop)
 
+lemma whileLoop_valid_inv:
+  "(\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>) \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> I \<rbrace>"
+  apply (fastforce intro: whileLoop_wp)
+  done
+
+lemma valid_whileLoop_cond_fail:
+  assumes pre_implies_post: "\<And>s. P r s \<Longrightarrow> Q r s"
+      and pre_implies_fail: "\<And>s. P r s \<Longrightarrow> \<not> C r s"
+    shows "\<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
+  using assms
+  apply (clarsimp simp: valid_def)
+  apply (subst (asm) whileLoop_cond_fail)
+   apply blast
+  apply (clarsimp simp: return_def)
+  done
+
 lemma whileLoop_wp_inv [wp]:
   "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
    \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop_inv C B r I M \<lbrace> Q \<rbrace>"