theory CNodeInv_R

lemma spec_corres_split:
  assumes x: "spec_corres s r' P P' f f'"
  assumes y: "\<And>rv rv' s'. \<lbrakk> (rv, s') \<in> fst (f s); r' rv rv' \<rbrakk> \<Longrightarrow>
                spec_corres s' 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 r (P and Q) (P' and Q') (f >>= g) (f' >>= g')" proof - have w: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres r (R rv and (\<lambda>s'. (rv, s') \<in> fst (f s))) (R' rv') (g rv) (g' rv')" apply (rule use_spec_corres') apply (erule(1) y) done show ?thesis unfolding spec_corres_def apply (rule corres_guard_imp) apply (rule corres_split) apply (rule x[unfolded spec_corres_def]) apply (erule w) apply (wp z) apply (rule univ_wp) apply (rule z) apply simp apply assumption done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r (P and Q) (P' and Q') (f >>= g) (f' >>= g') proof (state)
goal (1 subgoal):
 1. spec_corres s r (P and Q) (P' and Q') (f >>= g) (f' >>= g') proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> corres r (R rv and (\<lambda>s'. (rv, s') \<in> fst (f s))) (R' rv') (g rv) (g' rv') proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' sa. \<lbrakk>r' rv rv'; (rv, sa) \<in> fst (f s)\<rbrakk> \<Longrightarrow> spec_corres sa r (R rv) (R' rv') (g rv) (g' rv') proof (prove)
goal:
No subgoals! proof (state)
this:
r' ?rv ?rv' \<Longrightarrow> corres r (R ?rv and (\<lambda>s'. (?rv, s') \<in> fst (f s))) (R' ?rv') (g ?rv) (g' ?rv')

goal (1 subgoal):
 1. spec_corres s r (P and Q) (P' and Q') (f >>= g) (f' >>= g') proof (prove)
goal (1 subgoal):
 1. spec_corres s r (P and Q) (P' and Q') (f >>= g) (f' >>= g') proof (prove)
goal (1 subgoal):
 1. corres r (P and Q and (=) s) (P' and Q') (f >>= g) (f' >>= g') proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' (f >>= g) (f' >>= g')
 2. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> ?Q sa
 3. \<And>s. (P' and Q') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ?r'4 ?P4 ?P'4 f f'
 2. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres r (?R4 rv) (?R'4 rv') (g rv) (g' rv')
 3. \<lbrace>?Q4\<rbrace> f \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> f' \<lbrace>?R'4\<rbrace>
 5. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (?P4 and ?Q4) sa
 6. \<And>s. (P' and Q') s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. r' rv rv' \<Longrightarrow> corres r (?R4 rv) (?R'4 rv') (g rv) (g' rv')
 2. \<lbrace>?Q4\<rbrace> f \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> f' \<lbrace>?R'4\<rbrace>
 4. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (P and (=) s and ?Q4) sa
 5. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> f \<lbrace>\<lambda>rv. R rv and (\<lambda>s'. (rv, s') \<in> fst (f s))\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> f' \<lbrace>R'\<rbrace>
 3. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (P and (=) s and ?Q4) sa
 4. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'12\<rbrace> f \<lbrace>\<lambda>rv sa. (rv, sa) \<in> fst (f s)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> f' \<lbrace>R'\<rbrace>
 3. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (P and (=) s and (\<lambda>s. Q s \<and> ?P'12 s)) sa
 4. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'4\<rbrace> f' \<lbrace>R'\<rbrace>
 2. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (P and (=) s and (\<lambda>sa. Q sa \<and> (\<forall>(rv, s')\<in>fst (f sa). (rv, s') \<in> fst (f s)))) sa
 3. \<And>s. (P' and Q') s \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>sa. (P and Q and (=) s) sa \<Longrightarrow> (P and (=) s and (\<lambda>sa. Q sa \<and> (\<forall>(rv, s')\<in>fst (f sa). (rv, s') \<in> fst (f s)))) sa
 2. \<And>s. (P' and Q') s \<Longrightarrow> (P' and Q') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P' and Q') s \<Longrightarrow> (P' and Q') s proof (prove)
goal:
No subgoals! proof (state)
this:
spec_corres s r (P and Q) (P' and Q') (f >>= g) (f' >>= g')

goal:
No subgoals!