clib: move ccorres_cond_both' to CCorresLemmas

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

lib/clib/CCorresLemmas.thy

@@ -990,6 +990,29 @@ lemma ccorres_cond2':
   apply clarsimp
   done
 
+text \<open>
+  A stronger version of @{thm ccorres_cond_both}, which allows specifying a C state predicate
+  when showing equality of the conditionals' guards, and which supplies the relevant @{term If}
+  guard truth to the @{term ccorres_underlying} assumptions.\<close>
+lemma ccorres_cond_both':
+  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
+  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
+  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
+  shows  "ccorres_underlying sr G r xf arrel axf
+          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
+          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
+          hs
+          (if P then a else b) (Cond P' c d)"
+  apply (rule ccorres_guard_imp2)
+   apply (rule ccorres_if_lhs)
+    apply (rule ccorres_cond_true)
+    apply (erule ac)
+   apply (rule ccorres_cond_false)
+   apply (erule bd)
+  apply clarsimp
+  apply (frule abs[rule_format, OF conjI], simp+)
+  done
+
 lemmas ccorres_handlers_weaken2 = ccorres_nohs
 
 lemma ccorres_abstract_cleanup:

proof/crefine/AARCH64/SyscallArgs_C.thy

@@ -707,25 +707,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_64 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)

proof/crefine/ARM/SyscallArgs_C.thy

@@ -688,25 +688,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 32"
   by (cases sz, auto)

proof/crefine/ARM_HYP/SyscallArgs_C.thy

@@ -711,25 +711,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 32"
   by (cases sz, auto)

proof/crefine/RISCV64/SyscallArgs_C.thy

@@ -707,25 +707,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)

proof/crefine/X64/SyscallArgs_C.thy

@@ -713,25 +713,6 @@ lemma ccorres_case_bools:
    apply (auto simp: P Q)
   done
 
-lemma ccorres_cond_both':
-  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
-  and     ac: "P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf R R' hs a c"
-  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr G r xf arrel axf U U' hs b d"
-  shows  "ccorres_underlying sr G r xf arrel axf
-          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
-          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
-          hs
-          (if P then a else b) (Cond P' c d)"
-  apply (rule ccorres_guard_imp2)
-   apply (rule ccorres_if_lhs)
-    apply (rule ccorres_cond_true)
-    apply (erule ac)
-   apply (rule ccorres_cond_false)
-   apply (erule bd)
-  apply clarsimp
-  apply (frule abs[rule_format, OF conjI], simp+)
-  done
-
 lemma pageBitsForSize_32 [simp]:
   "pageBitsForSize sz < 64"
   by (cases sz, auto simp: bit_simps)