theory Corres_UL_C

lemma ccorres_split_nothrow_record_novcg:
  fixes R' :: "'a set"
  assumes ac: "ccorres_underlying sr \<Gamma> r' (xfr \<circ> xf') r' (xfr \<circ> xf') P P' [] a c"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' (xfru (\<lambda>_. rv') oldv))"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  and  novcg: "guard_is_UNIV r' (xfr \<circ> xf') Q'"
  \<comment> \<open>This might cause problems \<dots> has to be preserved across c in vcg case, but we can't do that\<close>
  and xfoldv: "\<And>s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= (\<lambda>rv. b rv)) (c ;; d)" apply (rule ccorres_master_split_nohs_UNIV) apply (rule ac) apply (rule ccorres_abstract[OF ceqv]) apply (rule_tac P="d' rv' = d' (xfru (\<lambda>_. (xfr rv')) oldv)" in ccorres_gen_asm2) apply (rule_tac P="r' rv (xfr rv')" in ccorres_gen_asm2) apply simp apply (erule bd) apply (rule valid) apply (simp add: xfoldv[symmetric, unfolded o_def]) apply (cut_tac novcg, clarsimp simp: guard_is_UNIV_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P P' [] a c
 2. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 3. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 4. guard_is_UNIV ?r' ?xf' (\<lambda>a b. ?R' a) proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. ?R' a) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'5 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> ?G'5 a (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. d' rv' = d' (xfru (\<lambda>_. xfr rv') oldv) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'8 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> ?G'8 a (xf' s) \<inter> \<lbrace>d' (xf' s) = d' (xfru (\<lambda>_. xfr (xf' s)) oldv)\<rbrace>}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>d' rv' = d' (xfru (\<lambda>_. xfr rv') oldv); r' rv (xfr rv')\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'9 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> ?G'9 a (xf' s) \<inter> \<lbrace>r' a (xfr (xf' s))\<rbrace> \<inter> \<lbrace>d' (xf' s) = d' (xfru (\<lambda>_. xfr (xf' s)) oldv)\<rbrace>}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>d' rv' = d' (xfru (\<lambda>_. xfr rv') oldv); r' rv (xfr rv')\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'9 rv rv') hs (b rv) (d' (xfru (\<lambda>_. xfr rv') oldv))
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> ?G'9 a (xf' s) \<inter> \<lbrace>r' a (xfr (xf' s))\<rbrace> \<inter> \<lbrace>d' (xf' s) = d' (xfru (\<lambda>_. xfr (xf' s)) oldv)\<rbrace>}) proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>
 2. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> Q' a (xfr (xf' s)) \<inter> \<lbrace>r' a (xfr (xf' s))\<rbrace> \<inter> \<lbrace>d' (xf' s) = d' (xfru (\<lambda>_. xfr (xf' s)) oldv)\<rbrace>}) proof (prove)
goal (1 subgoal):
 1. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. s \<in> Q' a (xfr (xf' s)) \<inter> \<lbrace>r' a (xfr (xf' s))\<rbrace> \<inter> \<lbrace>d' (xf' s) = d' (xfru (\<lambda>_. xfr (xf' s)) oldv)\<rbrace>}) proof (prove)
goal (1 subgoal):
 1. guard_is_UNIV r' (xfr \<circ> xf') (\<lambda>a b. {s. (r' a (xfr (xf' s)) \<longrightarrow> s \<in> Q' a (xfr (xf' s))) \<and> r' a (xfr (xf' s))}) proof (prove)
goal:
No subgoals!