theory CNodeInv_R

lemma whenE_throwError_corres':
  assumes P: "frel f f'"
  assumes Q: "\<And>s s'. \<lbrakk>(s, s') \<in> state_relation; R s; R' s'\<rbrakk> \<Longrightarrow> P = P'"
  assumes R: "\<not> P \<Longrightarrow> corres (frel \<oplus> rvr) Q Q' m m'"
  shows      "corres (frel \<oplus> rvr) (R and Q) (R' and Q')
                     (whenE P  (throwError f ) >>=E (\<lambda>_. m ))
                     (whenE P' (throwError f') >>=E (\<lambda>_. m'))" unfolding whenE_def apply (rule corres_req) apply (erule Q) apply simp apply simp apply (cases P) apply (simp add: P) apply simp apply (erule corres_guard_imp [OF R]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- whenE P (throwError f);
m
odE) (doE _ <- whenE P' (throwError f');
m'
odE) proof (prove)
goal (1 subgoal):
 1. corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (R and Q) s; (R' and Q') s'\<rbrakk> \<Longrightarrow> ?F
 2. ?F \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>(R and Q) s; (R' and Q') s'\<rbrakk> \<Longrightarrow> R s
 2. \<And>s s'. \<lbrakk>(R and Q) s; (R' and Q') s'\<rbrakk> \<Longrightarrow> R' s'
 3. P = P' \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(R and Q) s; (R' and Q') s'\<rbrakk> \<Longrightarrow> R' s'
 2. P = P' \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. P = P' \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P = P'; P\<rbrakk> \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE)
 2. \<lbrakk>P = P'; \<not> P\<rbrakk> \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; \<not> P\<rbrakk> \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> P'; \<not> P\<rbrakk> \<Longrightarrow> corres (frel \<oplus> rvr) (R and Q) (R' and Q') m m' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> P'; (R and Q) s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>\<not> P'; (R' and Q') s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> P'; (R' and Q') s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!