theory Corres_UL_C

lemma ccorres_symb_exec_r_abstract_UNIV:
  "\<lbrakk>  \<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)});
        \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv');
        \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv');
        guard_is_UNIV (\<lambda>rv rv'. F rv') xf' (\<lambda>rv. Q) \<rbrakk>
       \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) R' hs a (m;;y)" apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return,
          rule_tac r'="\<lambda>rv rv'. F rv'" and xf'=xf'
                in ccorres_split_nothrow_novcg) apply (rule_tac P'=R' in ccorres_from_vcg[where P=R]) apply (clarsimp simp add: return_def Int_def conj_comms) apply assumption apply fastforce apply wp apply (simp add: guard_is_UNIV_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) R' hs a (m;;
y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (m;;
y)
 2. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> (\<lambda>rv. F) xf' ?P5 ?Q' [] (return ()) m
 2. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' ?Q'5
 6. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (?P5 and ?R5) s \<and> s' \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. R \<sigma> \<and> s \<in> R' \<and> (\<sigma>, s) \<in> sr} m {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s) \<in> sr \<and> F (xf' s)}
 2. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' ?Q'5
 6. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 2. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 3. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' ?Q'5
 5. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (y' rv')
 2. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 3. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' ?Q'5
 4. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>\<lambda>a. P\<rbrace>
 2. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>a. Q)
 3. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q)\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>a. Q)
 2. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and P) s \<and> s' \<in> R' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); guard_is_UNIV (\<lambda>rv. F) xf' (\<lambda>rv. Q); (s, s') \<in> sr; (P and R) s; s' \<in> R'\<rbrakk> \<Longrightarrow> (R and P) s \<and> s' \<in> R' proof (prove)
goal:
No subgoals!