theory ExtraCorres

lemma corres_underlying_split_ex_abs:
  assumes ac: "corres_underlying srel nf nf' r' G G' a c"
  assumes bd: "\<forall>rv rv'. r' rv rv' \<longrightarrow>
                        corres_underlying srel nf nf' r (P rv) (P' rv') (b rv) (d rv')"
  assumes valid: "\<lbrace>G\<rbrace> a \<lbrace>P\<rbrace>" "\<lbrace>G' and ex_abs_underlying srel G\<rbrace> c \<lbrace>P'\<rbrace>"
  shows "corres_underlying srel nf nf' r G G' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" using assms apply (clarsimp simp: corres_underlying_def bind_def) apply (clarsimp simp: Bex_def Ball_def valid_def ex_abs_underlying_def) by meson

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' r G G' (a >>= b) (c >>= d) proof (prove)
using this:
corres_underlying srel nf nf' r' G G' a c
\<forall>rv rv'. r' rv rv' \<longrightarrow> corres_underlying srel nf nf' r (P rv) (P' rv') (b rv) (d rv')
\<lbrace>G\<rbrace> a \<lbrace>P\<rbrace>
\<lbrace>G' and ex_abs_underlying srel G\<rbrace> c \<lbrace>P'\<rbrace>

goal (1 subgoal):
 1. corres_underlying srel nf nf' r G G' (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>srel. case x of (s, s') \<Rightarrow> G s \<and> G' 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> srel \<and> r' r r'a) \<and> (nf' \<longrightarrow> \<not> snd (c s')); \<forall>rv rv'. r' rv rv' \<longrightarrow> (\<forall>x\<in>srel. case x of (s, s') \<Rightarrow> P rv s \<and> P' 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> srel \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (d rv' s'))); \<lbrace>G\<rbrace> a \<lbrace>P\<rbrace>; \<lbrace>G' and ex_abs_underlying srel G\<rbrace> c \<lbrace>P'\<rbrace>; (aa, ba) \<in> srel; G aa; G' 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> srel \<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> srel \<longrightarrow> G aa \<and> G' 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> srel \<and> r' ac ab)) \<and> (nf' \<longrightarrow> \<not> snd (c b)); \<forall>rv rv'. r' rv rv' \<longrightarrow> (\<forall>a ba. (a, ba) \<in> srel \<longrightarrow> P rv a \<and> P' 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> srel \<and> r ab aa)) \<and> (nf' \<longrightarrow> \<not> snd (d rv' ba))); \<forall>s. G s \<longrightarrow> (\<forall>aa b. (aa, b) \<in> fst (a s) \<longrightarrow> P aa b); \<forall>s. G' s \<and> (\<exists>sa. (sa, s) \<in> srel \<and> G sa) \<longrightarrow> (\<forall>a b. (a, b) \<in> fst (c s) \<longrightarrow> P' a b); (aa, ba) \<in> srel; G aa; G' 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> srel \<and> r a ac)))) \<and> (nf' \<longrightarrow> (\<forall>a b. (a, b) \<in> fst (c ba) \<longrightarrow> \<not> snd (d a b)))