squash monads: resync

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/NonDetMonadVCG.thy

@@ -711,11 +711,6 @@ lemma hoare_vcg_if_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 hoare_vcg_if_split_strong:
- "\<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. if P then Q s else R s\<rbrace> if P then f else g \<lbrace>S\<rbrace>"
-  by simp
-
 lemma hoare_vcg_if_splitE:
   "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>,\<lbrace>E\<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>,\<lbrace>E\<rbrace>"

lib/Monads/OptionMonadWP.thy

@@ -22,13 +22,8 @@ begin
 
 (* Partial correctness. *)
 definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool"
-  ("o\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") where
-  "o\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
-
-abbreviation (input)
-  oinvariant :: "('s,'a) lookup \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ o\<lbrace>_\<rbrace>" [59,0] 60)
-where
-  "oinvariant f P \<equiv> o\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
+  ("\<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
@@ -64,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,7 +383,7 @@ lemma whileLoop_wp:
   \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
   by (rule valid_whileLoop)
 
-lemma whileLoop_wp':
+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
@@ -392,7 +392,7 @@ 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>"
-  apply (insert assms)
+  using assms
   apply (clarsimp simp: valid_def)
   apply (subst (asm) whileLoop_cond_fail)
    apply blast