theory MoreCorres

lemma corres_alternate_split:
  "\<lbrakk> corres_underlying sr nf nf' r P Q a x;
     corres_underlying sr nf nf' r P' Q' a y \<rbrakk> \<Longrightarrow>
   corres_underlying sr nf nf' r (P and P') (Q and Q') a (x \<sqinter> y)" apply (simp add: corres_underlying_def alternative_def) apply (clarsimp) apply (drule (1) bspec, clarsimp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P Q a x; corres_underlying sr nf nf' r P' Q' a y\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (Q and Q') a (x \<sqinter> y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (x s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (x s')); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P' s \<and> Q' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (y s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s'))\<rbrakk> \<Longrightarrow> \<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> P s \<and> P' s \<and> Q s' \<and> Q' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (x s') \<union> fst (y s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (x s') \<and> \<not> snd (y s')) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>\<forall>xa\<in>sr. case xa of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (x s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (x s')); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P' s \<and> Q' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (y s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (y s')); (aa, b) \<in> sr; P aa; P' aa; Q b; Q' b; nf \<longrightarrow> \<not> snd (a aa)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (x b) \<union> fst (y b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (x b) \<and> \<not> snd (y b)) proof (prove)
goal (1 subgoal):
 1. \<And>aa b aaa ba. \<lbrakk>(aa, b) \<in> sr; P aa; P' aa; Q b; Q' b; nf \<longrightarrow> \<not> snd (a aa); \<forall>x\<in>fst (x b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'; nf' \<longrightarrow> \<not> snd (x b); (aaa, ba) \<in> fst (x b) \<or> (aaa, ba) \<in> fst (y b); \<forall>x\<in>fst (y b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'; nf' \<longrightarrow> \<not> snd (y b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa). case x of (ra, t) \<Rightarrow> (t, ba) \<in> sr \<and> r ra aaa proof (prove)
goal:
No subgoals!