clib: some variants of ccorres_to_vcg

Signed-off-by: Michael McInerney <[email protected]>

lib/clib/Corres_UL_C.thy

@@ -288,6 +288,43 @@ lemma ccorres_from_vcg_nofail:
   apply (rule hoare_complete, simp add: HoarePartialDef.valid_def)
   done
 
+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 (clarsimp simp: no_fail_def)
+  apply (drule_tac x=s in spec)
+  apply (rule hoare_complete)
+  apply (simp add: HoarePartialDef.valid_def cvalid_def)
+  apply (intro impI allI)
+  apply clarsimp
+  apply (frule (5) ccorres_empty_handler_abrupt)
+  apply (erule (4) ccorresE)
+   apply (erule (1) EHOther)
+  apply (rule image_eqI)
+   apply simp
+  apply (fastforce simp: unif_rrel_simps valid_def)
+  done
+
+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. (t, t') \<in> srel \<and> rrel rv (xf t') \<and> R rv t}"
+  apply (frule (2) ccorres_to_vcg_with_prop[where s=s])
+  apply (fastforce elim: conseq_under_new_pre)
+  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 gets_def bind_def return_def get_def assert_opt_def
+                        fail_def conseq_under_new_pre
+                 split: option.splits)
+  done
 
 lemma ccorres_to_vcg:
   "ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c \<Longrightarrow>