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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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 (subst dcorres_symb_exec_r) prefer 2 apply (clarsimp simp:lift_def validE_def bind_def) apply (simp) apply (case_tac rv) apply (simp add:throwError_def)+ apply (simp add:catch_def) apply simp+ 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>rv. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' rv) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 3. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 2. \<And>rv. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' rv) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= case_sum h return)
 3. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace>
 2. \<And>rv. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (?Q' rv) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= case_sum h return)
 3. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case rv of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= case_sum h return)
 2. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>rv 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>; rv = Inl a\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case rv of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= case_sum h return)
 2. \<And>rv 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>; rv = Inr b\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. case rv of Inl e \<Rightarrow> Q1 e s | Inr r \<Rightarrow> Q2 r s) f ((case rv of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> i x) >>= case_sum h return)
 3. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>rv 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>; rv = Inr b\<rbrakk> \<Longrightarrow> dcorres r P (Q2 b) f (i b >>= case_sum h return)
 2. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>cs. \<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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 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>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!