theory Corres_D

lemma dcorres_symb_exec_r_catch:
  "\<lbrakk>
    \<And>rv. dcorres r P (Q1 rv) f (h rv);
    \<And>rv'. dcorres r P (Q2 rv') f (i rv'<catch> h);
   \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
   \<rbrakk>
  \<Longrightarrow> dcorres r P P' f (g >>=E i <catch> h)" apply (subst catch_def) apply (clarsimp simp:lift_def bindE_def bind_assoc) apply (rule corres_symb_exec_r) prefer 2 apply (clarsimp simp:lift_def validE_def bind_def) apply (simp) apply (case_tac x) apply (simp add:throwError_def)+ apply (simp add:catch_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P P' f (g >>=E i <catch> h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P P' f (g >>=E i >>= case_sum h return) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P P' f (do x <- g;
(case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return
od) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' x) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 2. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 3. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 2. \<And>x. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' x) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 3. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 2. \<And>x. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' x) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 3. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case x of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 2. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (4 subgoals):
 1. \<And>x a. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; x = Inl a\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case x of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 2. \<And>x b. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; x = Inr b\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case x of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> i v') >>= case_sum h return)
 3. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal (3 subgoals):
 1. \<And>x b. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; x = Inr b\<rbrakk> \<Longrightarrow> dcorres r P (Q2 b) f (i b >>= case_sum h return)
 2. \<And>s. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; P' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>rv. dcorres r P (Q1 rv) f (h rv); \<And>rv'. dcorres r P (Q2 rv') f (i rv' <catch> h); \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail P' g proof (prove)
goal:
No subgoals!