theory Corres_UL

lemma corres_either_alternate2:
  "\<lbrakk> corres_underlying sr nf nf' r P R a c; corres_underlying sr nf nf' r Q R b c \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P or Q) R (a \<sqinter> b) c" apply (simp add: corres_underlying_def alternative_def) apply clarsimp apply (drule (1) bspec, clarsimp)+ apply (erule disjE) apply clarsimp apply (drule(1) bspec, clarsimp) apply (rule rev_bexI) apply (erule UnI1) apply simp apply clarsimp apply (drule(1) bspec, clarsimp) apply (rule rev_bexI) apply (erule UnI2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P R a c; corres_underlying sr nf nf' r Q R b c\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P or Q) R (a \<sqinter> b) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> R s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (c 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 (c s')); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> Q s \<and> R s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (b s)) \<longrightarrow> (\<forall>x\<in>fst (c s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s'))\<rbrakk> \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> (P s \<or> Q s) \<and> R s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s) \<and> \<not> snd (b s)) \<longrightarrow> (\<forall>x\<in>fst (c s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a s) \<union> fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s')) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> R s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>x\<in>fst (c 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 (c s')); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> Q s \<and> R s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (b s)) \<longrightarrow> (\<forall>x\<in>fst (c s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s')); (aa, ba) \<in> sr; P aa \<or> Q aa; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; P aa \<or> Q aa; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); P aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba))
 2. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba aaa baa. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'); P aa; (aaa, baa) \<in> fst (c ba); \<forall>x\<in>fst (c ba). 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 (c ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa
 2. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'); P aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (a aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa
 2. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (3 subgoals):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'); P aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (a aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> ?x48 aa ba aaa baa ab bb \<in> fst (a aa) \<union> fst (b aa)
 2. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'); P aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (a aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> case ?x48 aa ba aaa baa ab bb of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa
 3. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (2 subgoals):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'); P aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (a aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> case (ab, bb) of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa
 2. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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 (c ba)); Q aa \<longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)); Q aa\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c ba)) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba aaa baa. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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'); Q aa; (aaa, baa) \<in> fst (c ba); \<forall>x\<in>fst (c ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (b aa). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r'; nf' \<longrightarrow> \<not> snd (c ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa proof (prove)
goal (1 subgoal):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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'); Q aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (b aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa) \<union> fst (b aa). case x of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa proof (prove)
goal (2 subgoals):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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'); Q aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (b aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> ?x59 aa ba aaa baa ab bb \<in> fst (a aa) \<union> fst (b aa)
 2. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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'); Q aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (b aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> case ?x59 aa ba aaa baa ab bb of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa proof (prove)
goal (1 subgoal):
 1. \<And>aa ba aaa baa ab bb. \<lbrakk>(aa, ba) \<in> sr; R ba; nf \<longrightarrow> \<not> snd (a aa) \<and> \<not> snd (b aa); P aa \<longrightarrow> (\<forall>x\<in>fst (c ba). 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'); Q aa; (aaa, baa) \<in> fst (c ba); nf' \<longrightarrow> \<not> snd (c ba); (ab, bb) \<in> fst (b aa); (bb, baa) \<in> sr; r ab aaa\<rbrakk> \<Longrightarrow> case (ab, bb) of (ra, t) \<Rightarrow> (t, baa) \<in> sr \<and> r ra aaa proof (prove)
goal:
No subgoals!