theory EquivValid

lemma equiv_valid_rv_liftE_bindE:
  assumes ev1:
  "equiv_valid_rv_inv I A W P f"
  assumes ev2:
  "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')"
  assumes hoare:
  "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid_rv_inv I A R P ((liftE f) >>=E g)" apply(unfold bindE_def) 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)" in equiv_valid_rv_bind) apply(rule_tac E="dc" in equiv_valid_2_liftE) apply(rule ev1) apply(clarsimp simp: lift_def split: sum.split) apply(insert ev2, fastforce simp: equiv_valid_2_def)[1] apply(insert hoare, clarsimp simp: valid_def liftE_def bind_def return_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R P (liftE f >>=E g) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R P (liftE f >>= lift g) proof (prove)
goal (3 subgoals):
 1. equiv_valid_rv_inv I A ?W P (liftE f)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 I A A 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>P\<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> proof (prove)
goal (3 subgoals):
 1. equiv_valid_rv_inv I A ?R2 P f
 2. \<And>rv rv'. (dc \<oplus> ?R2) rv rv' \<Longrightarrow> equiv_valid_2 I A A 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>P\<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> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. (dc \<oplus> W) rv rv' \<Longrightarrow> equiv_valid_2 I A A 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>P\<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> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. (dc \<oplus> W) rv rv' \<Longrightarrow> (\<forall>x1. rv = Inl x1 \<longrightarrow> (\<forall>x1a. rv' = Inl x1a \<longrightarrow> equiv_valid_2 I A A R (\<lambda>y. False) (\<lambda>y. False) (throwError x1) (throwError x1a)) \<and> (\<forall>x2. rv' = Inr x2 \<longrightarrow> equiv_valid_2 I A A 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 I A A R (Q x2) (\<lambda>y. False) (g x2) (throwError x1)) \<and> (\<forall>x2a. rv' = Inr x2a \<longrightarrow> equiv_valid_2 I A A R (Q x2) (Q x2a) (g x2) (g x2a)))
 2. \<lbrace>P\<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> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<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> proof (prove)
goal:
No subgoals!