theory Corres_UL_C

lemma ccorres_split_throws:
  assumes ac: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c"
  and valid': "\<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> R' c {}, UNIV" (* Always throws *)
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P (P' \<inter> R') hs a (c ;; d)" apply (rule ccorres_add_return2) apply (rule ccorres_guard_imp,
         rule ccorres_master_split_hs[OF ac]) apply (rule ccorres_empty[where P=\<top>]) apply (rule ccorres_return_Skip') apply wp apply clarsimp apply (rule exec_handlers_Hoare_from_vcg_fails [OF valid']) apply (simp add: ccHoarePost_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P (P' \<inter> R') hs a (c;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P (P' \<inter> R') hs (a >>= return) (c;;
d) proof (prove)
goal (6 subgoals):
 1. \<And>x. ccorres_underlying sr \<Gamma> r xf arrel axf (?R6 x) (?R'6 x) hs (return x) d
 2. \<And>x. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E6 x) (?E'6 x) [] (return x) SKIP
 3. \<lbrace>?Q6\<rbrace> a \<lbrace>\<lambda>x. ?R6 x and ?E6 x\<rbrace>
 4. exec_handlers_Hoare \<Gamma> ?Q'6 (c # hs) (ccHoarePost r xf (\<lambda>a b. ?R'6 a)) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. ?E'6 a)}
 5. \<And>s. P s \<Longrightarrow> (P and ?Q6) s
 6. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> ?Q'6 proof (prove)
goal (5 subgoals):
 1. \<And>x. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E6 x) (?E'6 x) [] (return x) SKIP
 2. \<lbrace>?Q6\<rbrace> a \<lbrace>\<lambda>x. (\<lambda>_. True) and ?E6 x\<rbrace>
 3. exec_handlers_Hoare \<Gamma> ?Q'6 (c # hs) (ccHoarePost r xf (\<lambda>a b. {})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. ?E'6 a)}
 4. \<And>s. P s \<Longrightarrow> (P and ?Q6) s
 5. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> ?Q'6 proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> a \<lbrace>\<lambda>x. (\<lambda>_. True) and (\<lambda>_. True)\<rbrace>
 2. exec_handlers_Hoare \<Gamma> ?Q'6 (c # hs) (ccHoarePost r xf (\<lambda>a b. {})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. UNIV \<inter> {s. arrel a (axf s)})}
 3. \<And>s. P s \<Longrightarrow> (P and ?Q6) s
 4. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> ?Q'6 proof (prove)
goal (3 subgoals):
 1. exec_handlers_Hoare \<Gamma> ?Q'6 (c # hs) (ccHoarePost r xf (\<lambda>a b. {})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. UNIV \<inter> {s. arrel a (axf s)})}
 2. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 3. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> ?Q'6 proof (prove)
goal (3 subgoals):
 1. exec_handlers_Hoare \<Gamma> ?Q'6 (c # hs) (ccHoarePost r xf (\<lambda>a b. {})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. {s. arrel a (axf s)})}
 2. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 3. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> ?Q'6 proof (prove)
goal (3 subgoals):
 1. UNIV \<subseteq> {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost arrel axf (\<lambda>a b. {s. arrel a (axf s)})}
 2. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 3. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> R' proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 2. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> R' proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P' \<inter> R' \<Longrightarrow> s \<in> P' \<inter> R' proof (prove)
goal:
No subgoals!