From d2535f2f2ebc6e80f0cf03f531f8cdb51e72572d Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Tue, 9 Jul 2024 19:37:15 +0930
Subject: [PATCH] lib+proof: move corres_add_noop_rhs and corres_add_noop_rhs2
 to Lib

Moved from DRefine and CRefine, respectively

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Corres_UL.thy                                | 10 ++++++++++
 proof/crefine/autocorres-test/AutoCorresTest.thy |  5 -----
 proof/drefine/Arch_DR.thy                        |  5 -----
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
index 395a327b04..c919ae8874 100644
--- a/lib/Corres_UL.thy
+++ b/lib/Corres_UL.thy
@@ -1298,6 +1298,16 @@ lemmas corres_split_noop_rhs2
 
 lemmas corres_split_dc = corres_split[where r'=dc, simplified]
 
+lemma corres_add_noop_rhs:
+  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> return (); g od)
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by simp
+
+lemma corres_add_noop_rhs2:
+  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> g; return () od)
+   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
+  by simp
+
 lemma isLeft_case_sum:
   "isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)"
   by (clarsimp split: sum.splits)
diff --git a/proof/crefine/autocorres-test/AutoCorresTest.thy b/proof/crefine/autocorres-test/AutoCorresTest.thy
index 01ee243362..bb83ea0a7d 100644
--- a/proof/crefine/autocorres-test/AutoCorresTest.thy
+++ b/proof/crefine/autocorres-test/AutoCorresTest.thy
@@ -132,11 +132,6 @@ local_setup \<open>AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_
 
 text \<open>Extra corres_underlying rules.\<close>
 
-lemma corres_add_noop_rhs2:
-  "corres_underlying sr nf nf' r P P' f (do _ \<leftarrow> g; return () od)
-      \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
-  by simp
-
 (* Use termination (nf=True) to avoid exs_valid *)
 lemma corres_noop2_no_exs:
   assumes x: "\<And>s. P s  \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s\<rbrace> \<and> empty_fail f"
diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy
index b0450bbbd3..ab45a0f247 100644
--- a/proof/drefine/Arch_DR.thy
+++ b/proof/drefine/Arch_DR.thy
@@ -1082,11 +1082,6 @@ lemma pde_opt_cap_eq:
   apply (clarsimp simp: valid_idle_def st_tcb_at_def obj_at_def pred_tcb_at_def)
   done
 
-lemma corres_add_noop_rhs:
-  "corres_underlying sr fl fl' r P P' f (do _ \<leftarrow> return (); g od)
-    \<Longrightarrow> corres_underlying sr fl fl' r P P' f g"
-  by simp
-
 lemma gets_the_noop_dcorres:
   "dcorres dc (\<lambda>s. f s \<noteq> None) \<top> (gets_the f) (return x)"
   by (clarsimp simp: gets_the_def corres_underlying_def exec_gets