theory Corres_UL_C

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

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