theory Corres_UL_C

lemma ccorres_split_nothrow:
  fixes R' :: "'a set"
  assumes ac: "ccorres_underlying sr \<Gamma> r' xf' r' xf' P P' hs 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' rv')"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  and valid': "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' c {s. \<forall>rv. r' rv (xf' s) \<longrightarrow> s \<in> Q' rv (xf' s)}"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= (\<lambda>rv. b rv)) (c ;; d)" apply (rule ccorres_master_split_hs[OF ac]) apply (rule ccorres_abstract[OF ceqv]) apply (rule_tac P="r' rv rv'" in ccorres_gen_asm2) apply (erule bd) apply (rule ccorres_empty[where P=\<top>]) apply (simp add: valid) apply (rule exec_handlers_Hoare_from_vcg_nofail) apply (rule conseqPost, rule valid') apply (clarsimp simp: ccHoarePost_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. ?R rv and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. ?R' a)) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. ?E' a)} proof (prove)
goal (4 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. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. ?R rv and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> ?G'5 a (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'8 rv rv') hs (b rv) (d' rv')
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. ?R rv and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> ?G'8 a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. ?E' a)} proof (prove)
goal (3 subgoals):
 1. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (b rv) SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. Q rv and ?E rv\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. ?E' a)} proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. Q rv and (\<lambda>_. True)\<rbrace>
 2. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost r' xf' (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/?F11\<^esub> R' c (ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})) proof (prove)
goal (2 subgoals):
 1. {s. \<forall>rv. r' rv (xf' s) \<longrightarrow> s \<in> Q' rv (xf' s)} \<subseteq> ccHoarePost r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>})
 2. {} \<subseteq> {} proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> {} proof (prove)
goal:
No subgoals!