theory Monad_Commute

lemma monad_commute_split:
  "\<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>\<lambda>r. Q r\<rbrace>\<rbrakk>
   \<Longrightarrow> monad_commute (P and P') f (h>>=g)" apply (simp (no_asm) add: monad_commute_def) apply (clarsimp simp: bind_assoc) apply (subst monad_commute_simple) apply simp+ apply (rule_tac Q = "(\<lambda>x. Q x)" in monad_eq_split) apply (subst monad_commute_simple[where a = f]) apply assumption apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> monad_commute (P and P') f (h >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s. P s \<and> P' s \<longrightarrow> (do x <- f;
y <- h >>= g;
return (x, y)
od) s = (do y <- h >>= g;
x <- f;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> (do x <- f;
xa <- h;
y <- g xa;
return (x, y)
od) s = (do x <- h;
y <- g x;
x <- f;
return (x, y)
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> monad_commute (?P6 s) f h
 2. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> ?P6 s s
 3. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> (do y <- h;
x <- f;
y <- g y;
return (x, y)
od) s = (do x <- h;
y <- g x;
x <- f;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> (do y <- h;
x <- f;
y <- g y;
return (x, y)
od) s = (do x <- h;
y <- g x;
x <- f;
return (x, y)
od) s proof (prove)
goal (3 subgoals):
 1. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> (do x <- f;
y <- g r;
return (x, y)
od) sa = (do y <- g r;
x <- f;
return (x, y)
od) sa
 2. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> \<lbrace>?P7 s\<rbrace> h \<lbrace>Q\<rbrace>
 3. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> ?P7 s s proof (prove)
goal (5 subgoals):
 1. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> monad_commute (?P9 s r sa) f (g r)
 2. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> ?P9 s r sa sa
 3. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> (do y <- g r;
x <- f;
return (x, y)
od) sa = (do y <- g r;
x <- f;
return (x, y)
od) sa
 4. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> \<lbrace>?P7 s\<rbrace> h \<lbrace>Q\<rbrace>
 5. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> ?P7 s s proof (prove)
goal (4 subgoals):
 1. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> Q r sa
 2. \<And>s r sa. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s; Q r sa\<rbrakk> \<Longrightarrow> (do y <- g r;
x <- f;
return (x, y)
od) sa = (do y <- g r;
x <- f;
return (x, y)
od) sa
 3. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> \<lbrace>?P7 s\<rbrace> h \<lbrace>Q\<rbrace>
 4. \<And>s. \<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h; \<lbrace>P'\<rbrace> h \<lbrace>Q\<rbrace>; P s; P' s\<rbrakk> \<Longrightarrow> ?P7 s s proof (prove)
goal:
No subgoals!