theory CNodeInv_R

lemma spec_corres_splitE:
  assumes x: "spec_corres s (e \<oplus> r') P P' f f'"
  assumes y: "\<And>rv rv' s'. \<lbrakk> (Inr rv, s') \<in> fst (f s); r' rv rv' \<rbrakk> \<Longrightarrow>
                spec_corres s' (e \<oplus> r) (R rv) (R' rv') (g rv) (g' rv')"
  assumes z: "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,-" "\<lbrace>Q'\<rbrace> f' \<lbrace>R'\<rbrace>,-"
  shows "spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g')" proof - note w = z[unfolded validE_R_def validE_def] show ?thesis unfolding bindE_def apply (rule spec_corres_split [OF x _ w(1) w(2)]) apply (case_tac rv) apply (clarsimp simp: lift_def spec_corres_def) apply (clarsimp simp: lift_def) apply (erule(1) y) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g') proof (state)
goal (1 subgoal):
 1. spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g') proof (state)
this:
\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s\<rbrace>
\<lbrace>Q'\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' r s\<rbrace>

goal (1 subgoal):
 1. spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g') proof (prove)
goal (1 subgoal):
 1. spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g') proof (prove)
goal (1 subgoal):
 1. spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>= lift g) (f' >>= lift g') proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' s'. \<lbrakk>(rv, s') \<in> fst (f s); (e \<oplus> r') rv rv'\<rbrakk> \<Longrightarrow> spec_corres s' (e \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' r s) (lift g rv) (lift g' rv') proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' s' a. \<lbrakk>(rv, s') \<in> fst (f s); (e \<oplus> r') rv rv'; rv = Inl a\<rbrakk> \<Longrightarrow> spec_corres s' (e \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' r s) (lift g rv) (lift g' rv')
 2. \<And>rv rv' s' b. \<lbrakk>(rv, s') \<in> fst (f s); (e \<oplus> r') rv rv'; rv = Inr b\<rbrakk> \<Longrightarrow> spec_corres s' (e \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' r s) (lift g rv) (lift g' rv') proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' s' b. \<lbrakk>(rv, s') \<in> fst (f s); (e \<oplus> r') rv rv'; rv = Inr b\<rbrakk> \<Longrightarrow> spec_corres s' (e \<oplus> r) (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R' r s) (lift g rv) (lift g' rv') proof (prove)
goal (1 subgoal):
 1. \<And>s' b y'. \<lbrakk>(Inr b, s') \<in> fst (f s); r' b y'\<rbrakk> \<Longrightarrow> spec_corres s' (e \<oplus> r) (R b) (R' y') (g b) (g' y') proof (prove)
goal:
No subgoals! proof (state)
this:
spec_corres s (e \<oplus> r) (P and Q) (P' and Q') (f >>=E g) (f' >>=E g')

goal:
No subgoals!