From f4107b64d81dc000fe04b4145ac005a7c1311641 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Wed, 12 Jun 2024 09:49:48 +1000
Subject: [PATCH] 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 <corey.lewis@proofcraft.systems>
---
 lib/Monads/nondet/Nondet_More_VCG.thy |  3 ---
 lib/Monads/nondet/Nondet_VCG.thy      | 12 +-----------
 lib/Monads/trace/Trace_More_VCG.thy   |  3 ---
 lib/Monads/trace/Trace_VCG.thy        |  6 +-----
 4 files changed, 2 insertions(+), 22 deletions(-)

diff --git a/lib/Monads/nondet/Nondet_More_VCG.thy b/lib/Monads/nondet/Nondet_More_VCG.thy
index 602816f4d0..6740e78210 100644
--- 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
index ad97f941be..9e0a7199d7 100644
--- 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
index 38992c13ed..b3f0fa9992 100644
--- 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
index f5849c555a..4b8170b5d3 100644
--- 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)