theory EquivValid

lemma equiv_valid_2_liftE:
  "equiv_valid_2 D A B R P P' f f' \<Longrightarrow>
   equiv_valid_2 D A B (E \<oplus> R) P P' (liftE f) (liftE f')" apply(unfold liftE_def) apply(rule equiv_valid_2_guard_imp) apply(rule_tac Q="\<top>\<top>" and Q'="\<top>\<top>" and R'=R in equiv_valid_2_bind_general) apply(fastforce intro: return_ev2) apply assumption apply(rule wp_post_taut)+ by(simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> equiv_valid_2 D A B (E \<oplus> R) P P' (liftE f) (liftE f') proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> equiv_valid_2 D A B (E \<oplus> R) P P' (do r <- f;
return (Inr r)
od) (do r <- f';
return (Inr r)
od) proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> equiv_valid_2 D A B (E \<oplus> R) ?Q ?Q' (do r <- f;
return (Inr r)
od) (do r <- f';
return (Inr r)
od)
 2. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P' s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. \<lbrakk>equiv_valid_2 D A B R P P' f f'; R rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 D ?B4 B (E \<oplus> R) (\<lambda>_. True) (\<lambda>_. True) (return (Inr rv)) (return (Inr rv'))
 2. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> equiv_valid_2 D A ?B4 R ?P4 ?P'4 f f'
 3. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S4\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>
 4. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S'4\<rbrace> f' \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P s\<rbrakk> \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P' s\<rbrakk> \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> equiv_valid_2 D A B R ?P4 ?P'4 f f'
 2. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S4\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>
 3. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S'4\<rbrace> f' \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P s\<rbrakk> \<Longrightarrow> ?P4 s \<and> ?S4 s
 5. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P' s\<rbrakk> \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (4 subgoals):
 1. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S4\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>
 2. equiv_valid_2 D A B R P P' f f' \<Longrightarrow> \<lbrace>?S'4\<rbrace> f' \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P s\<rbrakk> \<Longrightarrow> P s \<and> ?S4 s
 4. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P' s\<rbrakk> \<Longrightarrow> P' s \<and> ?S'4 s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P s\<rbrakk> \<Longrightarrow> P s \<and> True
 2. \<And>s. \<lbrakk>equiv_valid_2 D A B R P P' f f'; P' s\<rbrakk> \<Longrightarrow> P' s \<and> True