theory Corres_UL

lemma corres_split4:
  assumes corr: "corres_underlying sr nf nf' (\<lambda>(a, b, c, d).\<lambda>(a', b', c', d'). r a a' b b' c c' d d') P P'
                        (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; return (a, b, c, d) od)
                        (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; return (a', b', c', d') od)"
  and     corr': "\<And>a a' b b' c c' d d'. \<lbrakk> r a a' b b' c c' d d'\<rbrakk>
                     \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b c d) (P1' a' b' c' d')
                                  (H a b c d) (H' a' b' c' d')"
  and       h1: "\<lbrace>P\<rbrace>
                    do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; return (a, b, c, d) od
                 \<lbrace>\<lambda>(a, b, c, d). P1 a b c d\<rbrace>"
  and       h2: "\<lbrace>P'\<rbrace>
                    do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; return (a', b', c', d') od
                 \<lbrace>\<lambda>(a', b', c', d'). P1' a' b' c' d'\<rbrace>"
  shows "corres_underlying sr nf nf' r1 P P'
                (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; H a b c d od)
                (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; H' a' b' c' d' od)" proof - have "corres_underlying sr nf nf' r1 P P'
               (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; rv \<leftarrow> return (a, b, c, d);
                   H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv))) od)
               (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; rv \<leftarrow> return (a', b', c', d');
                   H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv))) od)" using h1 h2 by - (rule corres_underlying_split [OF corr corr', simplified bind_assoc],
    simp_all add: split_beta split_def) thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
D >>= H a b c
od) (do a' <- A';
b' <- B';
c' <- C';
D' >>= H' a' b' c'
od) proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
D >>= H a b c
od) (do a' <- A';
b' <- B';
c' <- C';
D' >>= H' a' b' c'
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
d <- D;
rv <- return (a, b, c, d);
H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) (do a' <- A';
b' <- B';
c' <- C';
d' <- D';
rv <- return (a', b', c', d');
H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) proof (prove)
using this:
\<lbrace>P\<rbrace> do a <- A;
b <- B;
c <- C;
d <- D;
return (a, b, c, d)
od \<lbrace>\<lambda>(a, b, c, d). P1 a b c d\<rbrace>
\<lbrace>P'\<rbrace> do a' <- A';
b' <- B';
c' <- C';
d' <- D';
return (a', b', c', d')
od \<lbrace>\<lambda>(a', b', c', d'). P1' a' b' c' d'\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
d <- D;
rv <- return (a, b, c, d);
H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) (do a' <- A';
b' <- B';
c' <- C';
d' <- D';
rv <- return (a', b', c', d');
H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) proof (state)
this:
corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
d <- D;
rv <- return (a, b, c, d);
H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) (do a' <- A';
b' <- B';
c' <- C';
d' <- D';
rv <- return (a', b', c', d');
H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od)

goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
D >>= H a b c
od) (do a' <- A';
b' <- B';
c' <- C';
D' >>= H' a' b' c'
od) proof (prove)
using this:
corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
d <- D;
rv <- return (a, b, c, d);
H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od) (do a' <- A';
b' <- B';
c' <- C';
d' <- D';
rv <- return (a', b', c', d');
H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv)))
od)

goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
D >>= H a b c
od) (do a' <- A';
b' <- B';
c' <- C';
D' >>= H' a' b' c'
od) proof (state)
this:
corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B;
c <- C;
D >>= H a b c
od) (do a' <- A';
b' <- B';
c' <- C';
D' >>= H' a' b' c'
od)

goal:
No subgoals!