theory Monad_Commute

lemma monad_commute_get:
  assumes hf: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>"
    and hg: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>"
    and eptyf: "empty_fail f" "empty_fail g"
  shows "monad_commute \<top> f g" proof - have fsame: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s" by (drule use_valid[OF _ hf],auto) have gsame: "\<And>a b s. (a,b) \<in> fst (g s) \<Longrightarrow> b = s" by (drule use_valid[OF _ hg],auto) note ef = empty_fail_not_snd[OF _ eptyf(1)] note eg = empty_fail_not_snd[OF _ eptyf(2)] show ?thesis apply (simp add: monad_commute_def) apply (clarsimp simp: bind_def split_def return_def) apply (intro conjI) apply (rule set_eqI) apply (rule iffI) apply (clarsimp simp:Union_eq) apply (frule fsame) apply clarsimp apply (frule gsame) apply (metis fst_conv snd_conv) apply (clarsimp simp:Union_eq) apply (frule gsame) apply clarsimp apply (frule fsame) apply clarsimp apply (metis fst_conv snd_conv) apply (rule iffI) apply (erule disjE) apply (clarsimp simp: image_def) apply (metis fsame) apply (clarsimp simp: image_def) apply (drule eg) apply clarsimp apply (rule bexI [rotated], assumption) apply (frule gsame) apply clarsimp apply (erule disjE) apply (clarsimp simp: image_def dest!: gsame) apply (clarsimp simp: image_def) apply (drule ef) apply clarsimp apply (frule fsame) apply (erule bexI[rotated]) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (state)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (prove)
goal (1 subgoal):
 1. \<And>a b s. (a, b) \<in> fst (f s) \<Longrightarrow> b = s proof (state)
this:
(?a, ?b) \<in> fst (f ?s) \<Longrightarrow> ?b = ?s

goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (prove)
goal (1 subgoal):
 1. \<And>a b s. (a, b) \<in> fst (g s) \<Longrightarrow> b = s proof (state)
this:
(?a, ?b) \<in> fst (g ?s) \<Longrightarrow> ?b = ?s

goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (state)
this:
\<not> snd (f ?s) \<Longrightarrow> \<exists>v. v \<in> fst (f ?s)

goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (state)
this:
\<not> snd (g ?s) \<Longrightarrow> \<exists>v. v \<in> fst (g ?s)

goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) f g proof (prove)
goal (1 subgoal):
 1. \<forall>s. (do x <- f;
y <- g;
return (x, y)
od) s = (do y <- g;
x <- f;
return (x, y)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)}) = (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<and> ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)}) = (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)})
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. (x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})) = (x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}))
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>s x. x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)})
 2. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa bb ab bc. \<lbrakk>(aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (g bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). \<exists>xa\<in>fst (f (snd x)). aa = fst xa \<and> ab = fst x \<and> bc = snd xa
 2. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa bb ab bc. \<lbrakk>(aa, bb) \<in> fst (f s); (ab, bc) \<in> fst (g bb); bb = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). \<exists>xa\<in>fst (f (snd x)). aa = fst xa \<and> ab = fst x \<and> bc = snd xa
 2. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa ab bc. \<lbrakk>(aa, s) \<in> fst (f s); (ab, bc) \<in> fst (g s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). \<exists>xa\<in>fst (f (snd x)). aa = fst xa \<and> ab = fst x \<and> bc = snd xa
 2. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (3 subgoals):
 1. \<And>s aa ab bc. \<lbrakk>(aa, s) \<in> fst (f s); (ab, bc) \<in> fst (g s); bc = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). \<exists>xa\<in>fst (f (snd x)). aa = fst xa \<and> ab = fst x \<and> bc = snd xa
 2. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 3. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s x. x \<in> (\<Union>x\<in>fst (g s). \<Union>xa\<in>fst (f (snd x)). {((fst xa, fst x), snd xa)}) \<Longrightarrow> x \<in> (\<Union>x\<in>fst (f s). \<Union>xa\<in>fst (g (snd x)). {((fst x, fst xa), snd xa)})
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa bb ab bc. \<lbrakk>(aa, bb) \<in> fst (g s); (ab, bc) \<in> fst (f bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ab = fst x \<and> (\<exists>x\<in>fst (g (snd x)). aa = fst x \<and> bc = snd x)
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa bb ab bc. \<lbrakk>(aa, bb) \<in> fst (g s); (ab, bc) \<in> fst (f bb); bb = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ab = fst x \<and> (\<exists>x\<in>fst (g (snd x)). aa = fst x \<and> bc = snd x)
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ab bc. \<lbrakk>(aa, s) \<in> fst (g s); (ab, bc) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ab = fst x \<and> (\<exists>x\<in>fst (g (snd x)). aa = fst x \<and> bc = snd x)
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ab bc. \<lbrakk>(aa, s) \<in> fst (g s); (ab, bc) \<in> fst (f s); bc = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ab = fst x \<and> (\<exists>x\<in>fst (g (snd x)). aa = fst x \<and> bc = snd x)
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s aa ab. \<lbrakk>(aa, s) \<in> fst (g s); (ab, s) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). ab = fst x \<and> (\<exists>x\<in>fst (g (snd x)). aa = fst x \<and> s = snd x)
 2. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)) = ((\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)) proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<exists>x\<in>fst (f s). snd (g (snd x)) \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)
 2. \<And>s. snd (f s) \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)
 3. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); snd (g b); \<not> snd (g s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). snd (f (snd x))
 2. \<And>s. snd (f s) \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)
 3. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s. snd (f s) \<Longrightarrow> (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s)
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>snd (f s); \<not> snd (g s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). snd (f (snd x))
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>snd (f s); \<exists>v. v \<in> fst (g s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). snd (f (snd x))
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>snd (f s); (a, b) \<in> fst (g s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). snd (f (snd x))
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>snd (f s); (a, b) \<in> fst (g s)\<rbrakk> \<Longrightarrow> snd (f (snd (a, b)))
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>snd (f s); (a, b) \<in> fst (g s); b = s\<rbrakk> \<Longrightarrow> snd (f (snd (a, b)))
 2. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>x\<in>fst (g s). snd (f (snd x))) \<or> snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<exists>x\<in>fst (g s). snd (f (snd x)) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s)
 2. \<And>s. snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<And>s. snd (g s) \<Longrightarrow> (\<exists>x\<in>fst (f s). snd (g (snd x))) \<or> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>snd (g s); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (g (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>snd (g s); \<exists>v. v \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (g (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>snd (g s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (g (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>snd (g s); (a, b) \<in> fst (f s); b = s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). snd (g (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>snd (g s); b = s\<rbrakk> \<Longrightarrow> snd (g (snd (a, b))) proof (prove)
goal:
No subgoals! proof (state)
this:
monad_commute (\<lambda>_. True) f g

goal:
No subgoals!