theory EquivValid

lemma equiv_valid_2_bindE:
  assumes g: "\<And>rv rv'. R' rv rv' \<Longrightarrow>
      equiv_valid_2 D A A (E \<oplus> R) (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes h1: "\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes h2: "\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>,-"
  assumes f: "equiv_valid_2 D A A (E \<oplus> R') P P' f f'"
  shows "equiv_valid_2 D A A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g')" apply(unfold bindE_def) apply(rule equiv_valid_2_guard_imp) apply(rule_tac R'="E \<oplus> R'" and Q="case_sum \<top>\<top> Q" and Q'="case_sum \<top>\<top> Q'" and S=S and S'=S' in equiv_valid_2_bind) apply(clarsimp simp: lift_def split: sum.splits) apply(intro impI conjI allI) apply(simp add: throwError_def) apply(rule return_ev2) apply simp apply(simp) apply(simp) apply(fastforce intro: g) apply(rule f) apply(insert h1, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] apply(insert h2, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g') proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A A (E \<oplus> R) (P and S) (P' and S') (f >>= lift g) (f' >>= lift g') proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 D A A (E \<oplus> R) ?Q ?Q' (f >>= lift g) (f' >>= lift g')
 2. \<And>s. (P and S) s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and S') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. (E \<oplus> R') rv rv' \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (case rv of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> Q x) (case rv' of Inl uu_ \<Rightarrow> \<lambda>_. True | Inr x \<Rightarrow> Q' x) (lift g rv) (lift g' rv')
 2. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 3. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 4. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. (E \<oplus> R') rv rv' \<Longrightarrow> (\<forall>x1. rv = Inl x1 \<longrightarrow> (\<forall>x1a. rv' = Inl x1a \<longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (throwError x1) (throwError x1a)) \<and> (\<forall>x2. rv' = Inr x2 \<longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2))) \<and> (\<forall>x2. rv = Inr x2 \<longrightarrow> (\<forall>x1. rv' = Inl x1 \<longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)) \<and> (\<forall>x2a. rv' = Inr x2a \<longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)))
 2. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 3. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 4. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' x1 x1a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inl x1a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (throwError x1) (throwError x1a)
 2. \<And>rv rv' x1 x2. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv rv' x2 x1. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 6. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 7. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 8. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 9. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' x1 x1a. \<lbrakk>E x1 x1a; rv = Inl x1; rv' = Inl x1a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (return (Inl x1)) (return (Inl x1a))
 2. \<And>rv rv' x1 x2. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv rv' x2 x1. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 6. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 7. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 8. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 9. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' x1 x1a s t. \<lbrakk>E x1 x1a; rv = Inl x1; rv' = Inl x1a; True; True; D s t; A s t\<rbrakk> \<Longrightarrow> (E \<oplus> R) (Inl x1) (Inl x1a)
 2. \<And>rv rv' x1 x2. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv rv' x2 x1. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 6. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 7. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 8. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 9. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' x1 x2. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 2. \<And>rv rv' x2 x1. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 3. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 4. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 5. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 6. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 7. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 8. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' x2 x1. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 2. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 3. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 4. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 5. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 6. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 7. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' x2 x2a. \<lbrakk>(E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 2. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 3. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 4. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 D A A (E \<oplus> R') ?P4 ?P'4 f f'
 2. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 3. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 4. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> S s
 5. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> S' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>S\<rbrace> f \<lbrace>case_sum (\<lambda>_ _. True) Q\<rbrace>
 2. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 3. \<And>s. (P and S) s \<Longrightarrow> P s \<and> S s
 4. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> S' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>S'\<rbrace> f' \<lbrace>case_sum (\<lambda>_ _. True) Q'\<rbrace>
 2. \<And>s. (P and S) s \<Longrightarrow> P s \<and> S s
 3. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> S' s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and S) s \<Longrightarrow> P s \<and> S s
 2. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> S' s