theory Corres_UL

lemma corres_underlying_split:
  assumes ac: "corres_underlying sr nf nf' r' P P' a c"
  assumes bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow>
                        corres_underlying sr nf nf' r (Q rv) (Q' rv') (b rv) (d rv')"
  assumes valid: "\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>" "\<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>"
  shows "corres_underlying sr nf nf' r P P' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" using ac bd valid apply (clarsimp simp: corres_underlying_def bind_def) apply (clarsimp simp: Bex_def Ball_def valid_def) apply meson done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (a >>= b) (c >>= d) proof (prove)
using this:
corres_underlying sr nf nf' r' P P' a c
r' ?rv ?rv' \<Longrightarrow> corres_underlying sr nf nf' r (Q ?rv) (Q' ?rv') (b ?rv) (d ?rv')
\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>
\<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (c s'). case x of (r'a, t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> r' r r'a) \<and> (nf' \<longrightarrow> \<not> snd (c s')); \<And>rv rv'. r' rv rv' \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> Q rv s \<and> Q' rv' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (b rv s)) \<longrightarrow> (\<forall>x\<in>fst (d rv' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (d rv' s')); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>; (aa, ba) \<in> sr; P aa; P' ba; nf \<longrightarrow> (\<forall>x\<in>fst (a aa). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa)) \<and> \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>y\<in>fst (c ba). \<forall>x\<in>fst (case y of (x, xa) \<Rightarrow> d x xa). case x of (r', t') \<Rightarrow> \<exists>y\<in>fst (a aa). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> b x xa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> (\<forall>x\<in>fst (c ba). \<not> snd (case x of (x, xa) \<Rightarrow> d x xa)) \<and> \<not> snd (c ba)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>aa b. (aa, b) \<in> sr \<longrightarrow> P aa \<and> P' b \<longrightarrow> (nf \<longrightarrow> \<not> snd (a aa)) \<longrightarrow> (\<forall>ab ba. (ab, ba) \<in> fst (c b) \<longrightarrow> (\<exists>ac b. (ac, b) \<in> fst (a aa) \<and> (b, ba) \<in> sr \<and> r' ac ab)) \<and> (nf' \<longrightarrow> \<not> snd (c b)); \<And>rv rv'. r' rv rv' \<Longrightarrow> \<forall>a ba. (a, ba) \<in> sr \<longrightarrow> Q rv a \<and> Q' rv' ba \<longrightarrow> (nf \<longrightarrow> \<not> snd (b rv a)) \<longrightarrow> (\<forall>aa bb. (aa, bb) \<in> fst (d rv' ba) \<longrightarrow> (\<exists>ab ba. (ab, ba) \<in> fst (b rv a) \<and> (ba, bb) \<in> sr \<and> r ab aa)) \<and> (nf' \<longrightarrow> \<not> snd (d rv' ba)); \<forall>s. P s \<longrightarrow> (\<forall>aa b. (aa, b) \<in> fst (a s) \<longrightarrow> Q aa b); \<forall>s. P' s \<longrightarrow> (\<forall>a b. (a, b) \<in> fst (c s) \<longrightarrow> Q' a b); (aa, ba) \<in> sr; P aa; P' ba; nf \<longrightarrow> (\<forall>ab ba. (ab, ba) \<in> fst (a aa) \<longrightarrow> \<not> snd (b ab ba)) \<and> \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>ab bb. (ab, bb) \<in> fst (c ba) \<longrightarrow> (\<forall>ac ba. (ac, ba) \<in> fst (d ab bb) \<longrightarrow> (\<exists>ab bb. (ab, bb) \<in> fst (a aa) \<and> (\<exists>a bc. (a, bc) \<in> fst (b ab bb) \<and> (bc, ba) \<in> sr \<and> r a ac)))) \<and> (nf' \<longrightarrow> (\<forall>a b. (a, b) \<in> fst (c ba) \<longrightarrow> \<not> snd (d a b))) proof (prove)
goal:
No subgoals!