clib+crefine: improve and consolidate variants of ccorres_to_vcg

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

lib/clib/Corres_UL_C.thy

@@ -288,26 +288,37 @@ lemma ccorres_from_vcg_nofail:
   apply (rule hoare_complete, simp add: HoarePartialDef.valid_def)
   done
 
-
-lemma ccorres_to_vcg:
-  "ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c \<Longrightarrow>
-  (\<forall>\<sigma>. \<not> snd (a \<sigma>) \<longrightarrow> \<Gamma> \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel}
-  c
-  {s. (\<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s))})"
-  apply -
-  apply rule
-  apply (rule impI)
+lemma ccorres_to_vcg_with_prop:
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel}
+           c {t'. \<exists>(rv, t) \<in> fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t}"
   apply (rule hoare_complete)
-  apply (simp add: HoarePartialDef.valid_def cvalid_def)
-  apply (intro impI allI)
+  apply (clarsimp simp: HoarePartialDef.valid_def cvalid_def no_fail_def)
+  apply (drule_tac x=s in spec)
   apply clarsimp
   apply (frule (5) ccorres_empty_handler_abrupt)
-  apply (erule (4) ccorresE)
-   apply (erule (1) EHOther)
-  apply clarsimp
-  apply rule
-   apply simp
-  apply (fastforce simp: unif_rrel_simps)
+  apply (fastforce elim!: ccorresE EHOther simp: unif_rrel_simps valid_def)
+  done
+
+lemma ccorres_to_vcg:
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel}
+           c {t'. \<exists>(rv, t) \<in> fst (a s). (t, t') \<in> srel \<and> rrel rv (xf t')}"
+  apply (frule (1) ccorres_to_vcg_with_prop[where R="\<top>\<top>"])
+   apply wpsimp
+  apply fastforce
+  done
+
+lemma ccorres_to_vcg_gets_the:
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> (P' \<inter> {s'. (s, s') \<in> srel \<and> P s})
+           c {t'. (s, t') \<in> srel \<and> P s \<and> (r s \<noteq> None) \<and> rrel (the (r s)) (xf t')}"
+  apply (frule ccorres_to_vcg_with_prop[where R="\<lambda>_. P" and s=s])
+    apply (erule no_ofail_gets_the)
+   apply wpsimp
+  apply (clarsimp simp: gets_the_def simpler_gets_def bind_def return_def get_def assert_opt_def
+                        fail_def conseq_under_new_pre
+                 split: option.splits)
   done
 
 lemma exec_handlers_Seq_cases0':
@@ -1402,14 +1413,6 @@ lemma ccorres_move_Guard:
 
 section "novcg"
 
-lemma ccorres_to_vcg':
-  "\<lbrakk> ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; \<not> snd (a \<sigma>) \<rbrakk> \<Longrightarrow>
-    \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c
-       {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> rrel rv (xf s)}"
-  apply (drule  ccorres_to_vcg)
-  apply clarsimp
-  done
-
 lemma exec_handlers_Hoare_UNIV:
   "guard_is_UNIV r xf Q \<Longrightarrow>
    exec_handlers_Hoare \<Gamma> UNIV cs (ccHoarePost r xf Q) UNIV"

proof/crefine/ARM_HYP/Retype_C.thy

@@ -2422,21 +2422,6 @@ next
     done
 qed
 
-(* FIXME: move *)
-lemma ccorres_to_vcg_nf:
-  "\<lbrakk>ccorres rrel xf P P' [] a c; no_fail Q a; \<And>s. P s \<Longrightarrow> Q s\<rbrakk>
-   \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c
-          {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rrel rv (xf s)}"
-  apply (rule HoarePartial.conseq_exploit_pre)
-  apply clarsimp
-  apply (rule conseqPre)
-  apply (drule ccorres_to_vcg')
-    prefer 2
-    apply simp
-   apply (simp add: no_fail_def)
-  apply clarsimp
-  done
-
 lemma mdb_node_get_mdbNext_heap_ccorres:
   "ccorres (=) ret__unsigned_' \<top> UNIV hs
   (liftM (mdbNext \<circ> cteMDBNode) (getCTE parent))

proof/crefine/RISCV64/Retype_C.thy

@@ -2225,21 +2225,6 @@ next
     done
 qed
 
-(* FIXME: move *)
-lemma ccorres_to_vcg_nf:
-  "\<lbrakk>ccorres rrel xf P P' [] a c; no_fail Q a; \<And>s. P s \<Longrightarrow> Q s\<rbrakk>
-   \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c
-          {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rrel rv (xf s)}"
-  apply (rule HoarePartial.conseq_exploit_pre)
-  apply clarsimp
-  apply (rule conseqPre)
-  apply (drule ccorres_to_vcg')
-    prefer 2
-    apply simp
-   apply (simp add: no_fail_def)
-  apply clarsimp
-  done
-
 lemma mdb_node_get_mdbNext_heap_ccorres:
   "ccorres (=) ret__unsigned_longlong_' \<top> UNIV hs
   (liftM (mdbNext \<circ> cteMDBNode) (getCTE parent))

proof/crefine/X64/Retype_C.thy

@@ -2771,21 +2771,6 @@ next
     done
 qed
 
-(* FIXME: move *)
-lemma ccorres_to_vcg_nf:
-  "\<lbrakk>ccorres rrel xf P P' [] a c; no_fail Q a; \<And>s. P s \<Longrightarrow> Q s\<rbrakk>
-   \<Longrightarrow> \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c
-          {s. \<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rrel rv (xf s)}"
-  apply (rule HoarePartial.conseq_exploit_pre)
-  apply clarsimp
-  apply (rule conseqPre)
-  apply (drule ccorres_to_vcg')
-    prefer 2
-    apply simp
-   apply (simp add: no_fail_def)
-  apply clarsimp
-  done
-
 lemma mdb_node_get_mdbNext_heap_ccorres:
   "ccorres (=) ret__unsigned_longlong_' \<top> UNIV hs
   (liftM (mdbNext \<circ> cteMDBNode) (getCTE parent))