theory EquivValid

lemma equiv_valid_2_liftE_bindE_general:
  assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes hoare':  "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
  assumes r1: "equiv_valid_2 D A B R' P P' f f'"
  shows "equiv_valid_2 D A C R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')" apply(unfold bindE_def) apply(rule equiv_valid_2_guard_imp) apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" and Q'="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q' v s)" in equiv_valid_2_bind_general) prefer 2 apply(rule_tac E="dc" in equiv_valid_2_liftE) apply(rule r1) apply(clarsimp simp: lift_def split: sum.split) apply(insert r2, fastforce simp: equiv_valid_2_def)[1] apply(simp add: liftE_def, wp, fastforce intro!: hoare_strengthen_post[OF hoare]) apply(simp add: liftE_def, wp, fastforce intro!: hoare_strengthen_post[OF hoare']) by(auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A C R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g') proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A C R (P and S) (P' and S') (liftE f >>= lift g) (liftE f' >>= lift g') proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 D A C R ?Q ?Q' (liftE f >>= lift g) (liftE 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'. ?R'4 rv rv' \<Longrightarrow> equiv_valid_2 D ?B4 C R (K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)) (K (\<forall>v. rv' \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv' = Inr v \<longrightarrow> Q' v s)) (lift g rv) (lift g' rv')
 2. equiv_valid_2 D A ?B4 ?R'4 ?P4 ?P'4 (liftE f) (liftE f')
 3. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 4. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (6 subgoals):
 1. equiv_valid_2 D A ?B4 ?R'4 ?P4 ?P'4 (liftE f) (liftE f')
 2. \<And>rv rv'. ?R'4 rv rv' \<Longrightarrow> equiv_valid_2 D ?B4 C R (K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)) (K (\<forall>v. rv' \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv' = Inr v \<longrightarrow> Q' v s)) (lift g rv) (lift g' rv')
 3. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 4. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (6 subgoals):
 1. equiv_valid_2 D A ?B4 ?R6 ?P4 ?P'4 f f'
 2. \<And>rv rv'. (dc \<oplus> ?R6) rv rv' \<Longrightarrow> equiv_valid_2 D ?B4 C R (K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)) (K (\<forall>v. rv' \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv' = Inr v \<longrightarrow> Q' v s)) (lift g rv) (lift g' rv')
 3. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 4. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 5. \<And>s. (P and S) s \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. (P' and S') s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. (dc \<oplus> R') rv rv' \<Longrightarrow> equiv_valid_2 D B C R (K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)) (K (\<forall>v. rv' \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv' = Inr v \<longrightarrow> Q' v s)) (lift g rv) (lift g' rv')
 2. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 3. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 4. \<And>s. (P and S) s \<Longrightarrow> P s \<and> ?S4 s
 5. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. (dc \<oplus> R') rv rv' \<Longrightarrow> (\<forall>x1. rv = Inl x1 \<longrightarrow> (\<forall>x1a. rv' = Inl x1a \<longrightarrow> equiv_valid_2 D B C R (\<lambda>y. False) (\<lambda>y. False) (throwError x1) (throwError x1a)) \<and> (\<forall>x2. rv' = Inr x2 \<longrightarrow> equiv_valid_2 D B C R (\<lambda>y. False) (Q' x2) (throwError x1) (g' x2))) \<and> (\<forall>x2. rv = Inr x2 \<longrightarrow> (\<forall>x1. rv' = Inl x1 \<longrightarrow> equiv_valid_2 D B C R (Q x2) (\<lambda>y. False) (g x2) (throwError x1)) \<and> (\<forall>x2a. rv' = Inr x2a \<longrightarrow> equiv_valid_2 D B C R (Q x2) (Q' x2a) (g x2) (g' x2a)))
 2. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 3. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 4. \<And>s. (P and S) s \<Longrightarrow> P s \<and> ?S4 s
 5. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> ?S'4 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S4\<rbrace> liftE f \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q v s)\<rbrace>
 2. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<rbrace>
 3. \<And>s. (P and S) s \<Longrightarrow> P s \<and> ?S4 s
 4. \<And>s. (P' and S') s \<Longrightarrow> P' s \<and> ?S'4 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S'4\<rbrace> liftE f' \<lbrace>\<lambda>rv. K (\<forall>v. rv \<noteq> Inl v) and (\<lambda>s. \<forall>v. rv = Inr v \<longrightarrow> Q' v s)\<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'4 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