theory CNode_DR

lemma corres_symb_exec_r_dcE:
  "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>;
     \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x);
     \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>,- \<rbrakk> \<Longrightarrow>
   corres_underlying rel False False (dc \<oplus> anyrel) P Q
      (throwError e) (g >>=E (\<lambda>x. h x))" unfolding bindE_def apply (rule corres_symb_exec_r[where Q'="\<lambda>rv. case rv of Inl _ \<Rightarrow> \<top> | Inr x \<Rightarrow> R x"]) apply (simp add: lift_def split: sum.split) apply (simp add: validE_R_def validE_def) apply (erule hoare_chain, simp_all split: sum.split)[1] apply assumption apply (rule no_fail_pre, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> corres_underlying rel False False (dc \<oplus> anyrel) P Q (throwError e) (g >>=E h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> corres_underlying rel False False (dc \<oplus> anyrel) P Q (throwError e) (g >>= lift h) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> corres_underlying rel False False (dc \<oplus> anyrel) P (case rv of Inl x \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> R x) (throwError e) (lift h rv)
 2. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g \<lbrace>\<lambda>rv. case rv of Inl x \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> R x\<rbrace>
 3. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; False\<rbrakk> \<Longrightarrow> no_fail Q g proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g \<lbrace>\<lambda>rv. case rv of Inl x \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> R x\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; False\<rbrakk> \<Longrightarrow> no_fail Q g proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>\<lambda>v s. \<forall>r. v = Inr r \<longrightarrow> R r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> g \<lbrace>\<lambda>rv. case rv of Inl x \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> R x\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; False\<rbrakk> \<Longrightarrow> no_fail Q g proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; Q s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; False\<rbrakk> \<Longrightarrow> no_fail Q g proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>; \<And>x. corres_underlying rel False False (dc \<oplus> anyrel) P (R x) (throwError e) (h x); \<lbrace>Q\<rbrace> g \<lbrace>R\<rbrace>, -; False\<rbrakk> \<Longrightarrow> no_fail Q g proof (prove)
goal:
No subgoals!