theory Trace_Monad

lemma bind_assoc:
  fixes m :: "('a,'b) tmonad"
  fixes f :: "'b \<Rightarrow> ('a,'c) tmonad"
  fixes g :: "'c \<Rightarrow> ('a,'d) tmonad"
  shows "(m >>= f) >>= g  =  m >>= (\<lambda>x. f x >>= g)" apply (unfold bind_def Let_def split_def) apply (rule ext) apply clarsimp apply (rule SUP_cong[OF refl], clarsimp) apply (split tmres.split; intro conjI impI; clarsimp) apply (simp add: image_Union) apply (rule SUP_cong[OF refl], clarsimp) apply (split tmres.split; intro conjI impI; clarsimp) apply (simp add: image_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = m >>= (\<lambda>x. f x >>= g) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<Union>p\<in>\<Union>p\<in>m s. case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a)) = (\<lambda>s. \<Union>p\<in>m s. case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` (\<Union>p\<in>f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>p\<in>\<Union>p\<in>m s. case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a)) = (\<Union>p\<in>m s. case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` (\<Union>p\<in>f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union>x\<in>m s. \<Union>p\<in>case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result a \<Rightarrow> (\<lambda>p. (fst p @ fst x, snd p)) ` f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a)) = (\<Union>p\<in>m s. case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` (\<Union>p\<in>f (fst a) (snd a). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> m s \<Longrightarrow> (\<Union>x\<in>case b of Failed \<Rightarrow> {(fst (a, b), Failed)} | Incomplete \<Rightarrow> {(fst (a, b), Incomplete)} | Result aa \<Rightarrow> (\<lambda>p. (fst p @ fst (a, b), snd p)) ` f (fst aa) (snd aa). case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result a \<Rightarrow> (\<lambda>p. (fst p @ fst x, snd p)) ` g (fst a) (snd a)) = (case b of Failed \<Rightarrow> {(fst (a, b), Failed)} | Incomplete \<Rightarrow> {(fst (a, b), Incomplete)} | Result aa \<Rightarrow> (\<lambda>p. (fst p @ fst (a, b), snd p)) ` (\<Union>p\<in>f (fst aa) (snd aa). case snd p of Failed \<Rightarrow> {(fst p, Failed)} | Incomplete \<Rightarrow> {(fst p, Incomplete)} | Result a \<Rightarrow> (\<lambda>pa. (fst pa @ fst p, snd pa)) ` g (fst a) (snd a))) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ba. (a, Result (aa, ba)) \<in> m s \<Longrightarrow> (\<Union>x\<in>f aa ba. case snd x of Failed \<Rightarrow> {(fst (fst x @ a, snd x), Failed)} | Incomplete \<Rightarrow> {(fst (fst x @ a, snd x), Incomplete)} | Result aa \<Rightarrow> (\<lambda>p. (fst p @ fst (fst x @ a, snd x), snd p)) ` g (fst aa) (snd aa)) = (\<lambda>x. (fst x @ a, snd x)) ` (\<Union>x\<in>f aa ba. case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result a \<Rightarrow> (\<lambda>p. (fst p @ fst x, snd p)) ` g (fst a) (snd a)) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ba. (a, Result (aa, ba)) \<in> m s \<Longrightarrow> (\<Union>x\<in>f aa ba. case snd x of Failed \<Rightarrow> {(fst (fst x @ a, snd x), Failed)} | Incomplete \<Rightarrow> {(fst (fst x @ a, snd x), Incomplete)} | Result aa \<Rightarrow> (\<lambda>p. (fst p @ fst (fst x @ a, snd x), snd p)) ` g (fst aa) (snd aa)) = (\<Union>x\<in>f aa ba. (\<lambda>x. (fst x @ a, snd x)) ` (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result a \<Rightarrow> (\<lambda>p. (fst p @ fst x, snd p)) ` g (fst a) (snd a))) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ba ab b. \<lbrakk>(a, Result (aa, ba)) \<in> m s; (ab, b) \<in> f aa ba\<rbrakk> \<Longrightarrow> (case b of Failed \<Rightarrow> {(fst (fst (ab, b) @ a, snd (ab, b)), Failed)} | Incomplete \<Rightarrow> {(fst (fst (ab, b) @ a, snd (ab, b)), Incomplete)} | Result aa \<Rightarrow> (\<lambda>p. (fst p @ fst (fst (ab, b) @ a, snd (ab, b)), snd p)) ` g (fst aa) (snd aa)) = (\<lambda>x. (fst x @ a, snd x)) ` (case b of Failed \<Rightarrow> {(fst (ab, b), Failed)} | Incomplete \<Rightarrow> {(fst (ab, b), Incomplete)} | Result a \<Rightarrow> (\<lambda>p. (fst p @ fst (ab, b), snd p)) ` g (fst a) (snd a)) proof (prove)
goal (1 subgoal):
 1. \<And>s a aa ba ab ac bb. \<lbrakk>(a, Result (aa, ba)) \<in> m s; (ab, Result (ac, bb)) \<in> f aa ba\<rbrakk> \<Longrightarrow> (\<lambda>x. (fst x @ ab @ a, snd x)) ` g ac bb = (\<lambda>x. (fst x @ a, snd x)) ` (\<lambda>x. (fst x @ ab, snd x)) ` g ac bb proof (prove)
goal:
No subgoals!