rt monads: rename whileLoop_wp' + minor changes

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jul 6, 2023 · cdf85ba · cdf85ba
1 parent 3bc3259
commit cdf85ba
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/lib/Monads/NonDetMonadVCG.thy b/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>"

diff --git a/lib/Monads/WhileLoopRules.thy b/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