theory Corres_UL

lemma corres_split3:
  assumes corr: "corres_underlying sr nf nf' (\<lambda>(a, b, c).\<lambda>(a', b', c'). r a a' b b' c c') P P'
                        (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; return (a, b, c) od)
                        (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; return (a', b', c') od)"
  and     corr': "\<And>a a' b b' c c'. \<lbrakk> r a a' b b' c c'\<rbrakk>
                     \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b c) (P1' a' b' c') (H a b c) (H' a' b' c')"
  and       h1: "\<lbrace>P\<rbrace>
                    do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; return (a, b, c) od
                 \<lbrace>\<lambda>(a, b, c). P1 a b c\<rbrace>"
  and       h2: "\<lbrace>P'\<rbrace>
                    do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; return (a', b', c') od
                 \<lbrace>\<lambda>(a', b', c'). P1' a' b' c'\<rbrace>"
  shows "corres_underlying sr nf nf' r1 P P'
                (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; H a b c od)
                (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; H' a' b' c' od)" proof - have "corres_underlying sr nf nf' r1 P P'
               (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; rv \<leftarrow> return (a, b, c);
                          H (fst rv) (fst (snd rv)) (snd (snd rv)) od)
               (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; rv \<leftarrow> return (a', b', c');
                          H' (fst rv) (fst (snd rv)) (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 a;
C a b >>= H a b
od) (do a' <- A';
b' <- B' a';
C' a' b' >>= H' a' b'
od) proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B a;
C a b >>= H a b
od) (do a' <- A';
b' <- B' a';
C' a' b' >>= H' a' b'
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- A;
b <- B a;
c <- C a b;
rv <- return (a, b, c);
H (fst rv) (fst (snd rv)) (snd (snd rv))
od) (do a' <- A';
b' <- B' a';
c' <- C' a' b';
rv <- return (a', b', c');
H' (fst rv) (fst (snd rv)) (snd (snd rv))
od) proof (prove)
using this:
\<lbrace>P\<rbrace> do a <- A;
b <- B a;
c <- C a b;
return (a, b, c)
od \<lbrace>\<lambda>(a, b, c). P1 a b c\<rbrace>
\<lbrace>P'\<rbrace> do a' <- A';
b' <- B' a';
c' <- C' a' b';
return (a', b', c')
od \<lbrace>\<lambda>(a', b', c'). P1' a' b' c'\<rbrace>

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

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

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

goal:
No subgoals!