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 <[email protected]>

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)

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"

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