theory EquivValid

lemma spec_equiv_valid_2_inv_bindE:
  assumes g: "\<And>rv s' rv'. \<lbrakk>(Inr rv, s') \<in> fst (f s); R' rv rv'\<rbrakk> \<Longrightarrow>
      spec_equiv_valid_2_inv s' I 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: "spec_equiv_valid_2_inv s I A (E \<oplus> R') P P' f f'"
  shows "spec_equiv_valid_2_inv s I A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g')" apply(unfold bindE_def) apply(rule spec_equiv_valid_2_inv_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 bind_spec_ev2) apply(clarsimp simp: lift_def split: sum.splits) apply(intro impI conjI allI) apply(simp add: throwError_def) apply(rule drop_spec_ev2_inv[OF 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. spec_equiv_valid_2_inv s I A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g') proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_2_inv s I A (E \<oplus> R) (P and S) (P' and S') (f >>= lift g) (f' >>= lift g') proof (prove)
goal (3 subgoals):
 1. spec_equiv_valid_2_inv s I 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 s' rv'. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I 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. spec_equiv_valid_2_inv s I 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 and S) s
 6. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (6 subgoals):
 1. \<And>rv s' rv'. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'\<rbrakk> \<Longrightarrow> (\<forall>x1. rv = Inl x1 \<longrightarrow> (\<forall>x1a. rv' = Inl x1a \<longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (throwError x1) (throwError x1a)) \<and> (\<forall>x2. rv' = Inr x2 \<longrightarrow> spec_equiv_valid_2_inv s' I 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> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)) \<and> (\<forall>x2a. rv' = Inr x2a \<longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)))
 2. spec_equiv_valid_2_inv s I 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 and S) s
 6. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (9 subgoals):
 1. \<And>rv s' rv' x1 x1a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inl x1a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (throwError x1) (throwError x1a)
 2. \<And>rv s' rv' x1 x2. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv s' rv' x2 x1. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. spec_equiv_valid_2_inv s I 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 and S) s
 9. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (9 subgoals):
 1. \<And>rv s' rv' x1 x1a. \<lbrakk>(Inl x1, s') \<in> fst (f s); E x1 x1a; rv = Inl x1; rv' = Inl x1a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (return (Inl x1)) (return (Inl x1a))
 2. \<And>rv s' rv' x1 x2. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv s' rv' x2 x1. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. spec_equiv_valid_2_inv s I 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 and S) s
 9. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (9 subgoals):
 1. \<And>rv s' rv' x1 x1a sa t. \<lbrakk>(Inl x1, s') \<in> fst (f s); E x1 x1a; rv = Inl x1; rv' = Inl x1a; True; True; I sa t; A sa t\<rbrakk> \<Longrightarrow> (E \<oplus> R) (Inl x1) (Inl x1a)
 2. \<And>rv s' rv' x1 x2. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 3. \<And>rv s' rv' x2 x1. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 4. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 5. spec_equiv_valid_2_inv s I 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 and S) s
 9. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (8 subgoals):
 1. \<And>rv s' rv' x1 x2. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inl x1; rv' = Inr x2\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (\<lambda>_. True) (Q' x2) (throwError x1) (g' x2)
 2. \<And>rv s' rv' x2 x1. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 3. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 4. spec_equiv_valid_2_inv s I 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 and S) s
 8. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (7 subgoals):
 1. \<And>rv s' rv' x2 x1. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inl x1\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (\<lambda>_. True) (g x2) (throwError x1)
 2. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 3. spec_equiv_valid_2_inv s I 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 and S) s
 7. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (6 subgoals):
 1. \<And>rv s' rv' x2 x2a. \<lbrakk>(rv, s') \<in> fst (f s); (E \<oplus> R') rv rv'; rv = Inr x2; rv' = Inr x2a\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q x2) (Q' x2a) (g x2) (g' x2a)
 2. spec_equiv_valid_2_inv s I 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 and S) s
 6. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 and S') s proof (prove)
goal (5 subgoals):
 1. spec_equiv_valid_2_inv s I 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 and S) s
 5. \<And>s. (P' and S') s \<Longrightarrow> (?P'4 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 and S) s
 4. \<And>s. (P' and S') s \<Longrightarrow> (P' 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 and S) s
 3. \<And>s. (P' and S') s \<Longrightarrow> (P' and S') s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and S) s \<Longrightarrow> (P and S) s
 2. \<And>s. (P' and S') s \<Longrightarrow> (P' and S') s