lib/monads: remove FIXMEs and hoare_gets

These FIXMEs were recently added and apart from removing hoare_gets I no longer think that they are worth doing, as the lemmas they refer to are used in more proofs than I first thought. Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jul 9, 2024 · f4107b6 · f4107b6
1 parent 05d0df3
commit f4107b6
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 22 deletions.
diff --git a/lib/Monads/nondet/Nondet_More_VCG.thy b/lib/Monads/nondet/Nondet_More_VCG.thy
@@ -154,7 +154,6 @@ lemma throwErrorE_E [wp]:
   "\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>"
   by (simp add: validE_E_def) wp
 
-\<comment> \<open>FIXME: remove these inv rules?\<close>
 lemma gets_inv [simp]:
   "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>"
   by (simp add: gets_def, wp)
@@ -163,8 +162,6 @@ lemma select_inv:
   "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>"
   by wpsimp
 
-lemmas return_inv = hoare_return_drop_var
-
 lemma assert_inv:
   "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>r. P\<rbrace>"
   unfolding assert_def

diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
@@ -221,32 +221,22 @@ lemma hoare_FalseE[simp]:
   "\<lbrace>\<bottom>\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   by (simp add: valid_def validE_def)
 
-\<comment> \<open>FIXME: remove?\<close>
-lemma hoare_return_drop_var[iff]:
+lemma return_inv[iff]:
   "\<lbrace>Q\<rbrace> return x \<lbrace>\<lambda>r. Q\<rbrace>"
   by (simp add: valid_def return_def)
 
-\<comment> \<open>FIXME: remove?\<close>
-lemma hoare_gets[intro]:
-  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets f \<lbrace>Q\<rbrace>"
-  by (simp add:valid_def gets_def get_def bind_def return_def)
-
-\<comment> \<open>FIXME: remove?\<close>
 lemma hoare_modifyE_var:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
   by(simp add: valid_def modify_def put_def get_def bind_def)
 
-\<comment> \<open>FIXME: remove?\<close>
 lemma hoare_if:
   "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> if P' then f else g \<lbrace>Q\<rbrace>"
   by (simp add: valid_def)
 
-\<comment> \<open>FIXME: remove?\<close>
 lemma hoare_pre_subst:
   "\<lbrakk> P = P'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
   by (erule subst)
 
-\<comment> \<open>FIXME: remove?\<close>
 lemma hoare_post_subst:
   "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
   by (erule subst)

diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy
@@ -154,7 +154,6 @@ lemma throwErrorE_E [wp]:
   "\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>"
   by (simp add: validE_E_def) wp
 
-\<comment> \<open>FIXME: remove these inv rules?\<close>
 lemma gets_inv [simp]:
   "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>"
   by (simp add: gets_def, wp)
@@ -163,8 +162,6 @@ lemma select_inv:
   "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>"
   by wpsimp
 
-lemmas return_inv = hoare_return_drop_var
-
 lemma assert_inv:
   "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>r. P\<rbrace>"
   unfolding assert_def

diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
@@ -217,14 +217,10 @@ lemma hoare_FalseE[simp]:
   "\<lbrace>\<bottom>\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
   by (simp add: valid_def validE_def)
 
-lemma hoare_return_drop_var[iff]:
+lemma return_inv[iff]:
   "\<lbrace>Q\<rbrace> return x \<lbrace>\<lambda>r. Q\<rbrace>"
   by (simp add: valid_def return_def mres_def)
 
-lemma hoare_gets[intro]:
-  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> gets f \<lbrace>Q\<rbrace>"
-  by (simp add:valid_def gets_def get_def bind_def return_def mres_def)
-
 lemma hoare_modifyE_var:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>"
   by(simp add: valid_def modify_def put_def get_def bind_def mres_def)