theory Fastpath_C

lemma ccorres_catch_bindE_symb_exec_l:
  "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f;
      \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (catch (g rv) h >>= j) c;
      \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c;
      \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<rbrakk>
    \<Longrightarrow>
  ccorres_underlying sr G r xf ar axf P {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)} hs
          (catch (f >>=E g) h >>= j) c" apply (simp add: catch_def bindE_def bind_assoc lift_def) apply (rule ccorres_guard_imp2) apply (rule ccorres_symb_exec_l[where G=P]) apply wpc apply (simp add: throwError_bind) apply assumption+ apply (clarsimp simp: valid_def validE_def split_def split: sum.split_asm) apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs ((g rv <catch> h) >>= j) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf P {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)} hs ((f >>=E g <catch> h) >>= j) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf P {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)} hs (do x <- f;
x <- case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf ?Q6 ?Q'6 hs (do x <- f;
x <- case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c
 2. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (?Q9 x) (?Q'9 x) hs (do x <- case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?Q9\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> empty_fail f
 5. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> ?Q9 rv s \<longrightarrow> s' \<in> ?Q'9 rv} proof (prove)
goal (6 subgoals):
 1. \<And>x x1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; x = Inl x1\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (?R23 x x1) (?R''25 x x1) hs (do x <- throwError x1;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c
 2. \<And>x x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; x = Inr x2\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (?R24 x x2) (?R''26 x x2) hs (do x <- g x2;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x s. (\<forall>xa. x = Inl xa \<longrightarrow> ?R23 x xa s) \<and> (\<forall>xa. x = Inr xa \<longrightarrow> ?R24 x xa s)\<rbrace>
 5. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> empty_fail f
 6. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> (\<forall>x. rv = Inl x \<longrightarrow> ?R23 rv x s) \<and> (\<forall>x. rv = Inr x \<longrightarrow> ?R24 rv x s) \<longrightarrow> s' \<in> {s. \<forall>x. s \<in> {s. rv = Inl x \<longrightarrow> s \<in> ?R''25 rv x}} \<inter> {s. \<forall>x. s \<in> {s. rv = Inr x \<longrightarrow> s \<in> ?R''26 rv x}}} proof (prove)
goal (6 subgoals):
 1. \<And>x x1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; x = Inl x1\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (?R23 (Inl x1) x1) (?R''25 (Inl x1) x1) hs (h x1 >>= j) c
 2. \<And>x x2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; x = Inr x2\<rbrakk> \<Longrightarrow> ccorres_underlying sr G r xf ar axf (?R24 x x2) (?R''26 x x2) hs (do x <- g x2;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x s. (\<forall>xa. x = Inl xa \<longrightarrow> ?R23 x xa s) \<and> (\<forall>xa. x = Inr xa \<longrightarrow> ?R24 x xa s)\<rbrace>
 5. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> empty_fail f
 6. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> (\<forall>x. rv = Inl x \<longrightarrow> ?R23 rv x s) \<and> (\<forall>x. rv = Inr x \<longrightarrow> ?R24 rv x s) \<longrightarrow> s' \<in> {s. \<forall>x. s \<in> {s. rv = Inl x \<longrightarrow> s \<in> ?R''25 rv x}} \<inter> {s. \<forall>x. s \<in> {s. rv = Inr x \<longrightarrow> s \<in> ?R''26 rv x}}} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x s. (\<forall>xa. x = Inl xa \<longrightarrow> R xa s) \<and> (\<forall>xa. x = Inr xa \<longrightarrow> Q xa s)\<rbrace>
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> empty_fail f
 3. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> (\<forall>x. rv = Inl x \<longrightarrow> R x s) \<and> (\<forall>x. rv = Inr x \<longrightarrow> Q x s) \<longrightarrow> s' \<in> {s. \<forall>x. s \<in> {s. rv = Inl x \<longrightarrow> s \<in> R' x}} \<inter> {s. \<forall>x. s \<in> {s. rv = Inr x \<longrightarrow> s \<in> Q' x}}} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> empty_fail f
 2. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> (\<forall>x. rv = Inl x \<longrightarrow> R x s) \<and> (\<forall>x. rv = Inr x \<longrightarrow> Q x s) \<longrightarrow> s' \<in> {s. \<forall>x. s \<in> {s. rv = Inl x \<longrightarrow> s \<in> R' x}} \<inter> {s. \<forall>x. s \<in> {s. rv = Inr x \<longrightarrow> s \<in> Q' x}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace>; empty_fail f; \<And>rv. ccorres_underlying sr G r xf ar axf (Q rv) (Q' rv) hs (do x <- g rv;
(case x of Inl x \<Rightarrow> h x | Inr x \<Rightarrow> return x) >>= j
od) c; \<And>ex. ccorres_underlying sr G r xf ar axf (R ex) (R' ex) hs (h ex >>= j) c; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>; (s, s') \<in> sr; P s; s' \<in> {s. (\<forall>rv. s \<in> Q' rv) \<and> (\<forall>ex. s \<in> R' ex)}\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> (\<forall>x. rv = Inl x \<longrightarrow> R x s) \<and> (\<forall>x. rv = Inr x \<longrightarrow> Q x s) \<longrightarrow> s' \<in> {s. \<forall>x. s \<in> {s. rv = Inl x \<longrightarrow> s \<in> R' x}} \<inter> {s. \<forall>x. s \<in> {s. rv = Inr x \<longrightarrow> s \<in> Q' x}}} proof (prove)
goal:
No subgoals!