theory Corres_UL

lemma corres_split_bind_case_sum:
  assumes x: "corres_underlying sr nf nf' (lr \<oplus> rr) P P' a d"
  assumes y: "\<And>rv rv'. lr rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (e rv')"
  assumes z: "\<And>rv rv'. rr rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (S rv) (S' rv') (c rv) (f rv')"
  assumes w: "\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>,\<lbrace>R'\<rbrace>"
  shows "corres_underlying sr nf nf' r (P and Q) (P' and Q')
            (a >>= (\<lambda>rv. case_sum b c rv)) (d >>= (\<lambda>rv'. case_sum e f rv'))" apply (rule corres_split [OF x]) defer apply (insert w)[2] apply (simp add: validE_def)+ apply (case_tac rv) apply (clarsimp simp: y) apply (clarsimp simp: z) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (do rv <- a;
case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x
od) (do rv' <- d;
case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. (lr \<oplus> rr) rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R rv) (?R' rv') (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 2. \<lbrace>Q\<rbrace> a \<lbrace>?R\<rbrace>
 3. \<lbrace>Q'\<rbrace> d \<lbrace>?R'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>Q\<rbrace> a \<lbrace>?R\<rbrace>
 2. \<lbrace>Q'\<rbrace> d \<lbrace>?R'\<rbrace>
 3. \<And>rv rv'. (lr \<oplus> rr) rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R rv) (?R' rv') (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>?R\<rbrace>
 2. \<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> d \<lbrace>?R'\<rbrace>
 3. \<And>rv rv'. (lr \<oplus> rr) rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R rv) (?R' rv') (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. (lr \<oplus> rr) rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. case rv of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> S r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> S' r s) (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' a. \<lbrakk>(lr \<oplus> rr) rv rv'; rv = Inl a\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. case rv of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> S r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> S' r s) (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x)
 2. \<And>rv rv' ba. \<lbrakk>(lr \<oplus> rr) rv rv'; rv = Inr ba\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. case rv of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> S r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> S' r s) (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' ba. \<lbrakk>(lr \<oplus> rr) rv rv'; rv = Inr ba\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. case rv of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> S r s) (\<lambda>s. case rv' of Inl e \<Rightarrow> R' e s | Inr r \<Rightarrow> S' r s) (case rv of Inl x \<Rightarrow> b x | Inr x \<Rightarrow> c x) (case rv' of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> f x) proof (prove)
goal:
No subgoals!