theory Trace_Monad

lemma liftE_def2:
  "liftE f = (\<lambda>s. snd_upd (map_tmres_rv Inr) ` (f s))" apply (clarsimp simp: fun_eq_iff liftE_def return_def split_def bind_def image_def) apply (rule set_eqI) apply (rule iffI) apply clarsimp apply (erule rev_bexI[where A="f s" for s]) apply (clarsimp split: tmres.splits) apply clarsimp apply (rule exI) apply (rule conjI) apply (erule rev_bexI[where A="f s" for s]) apply (rule refl) apply (clarsimp split: tmres.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE f = (\<lambda>s. (\<lambda>(a, b). (a, map_tmres_rv Inr b)) ` f s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} = {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})}) = (xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))}) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} \<Longrightarrow> xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))}
 2. \<And>x xa. xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))} \<Longrightarrow> xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} proof (prove)
goal (2 subgoals):
 1. \<And>x a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {(fst (aa, ba), Failed)} | Incomplete \<Rightarrow> {(fst (aa, ba), Incomplete)} | Result p \<Rightarrow> {(fst (aa, ba), Result (Inr (fst p), snd p))}); (aa, ba) \<in> f x\<rbrakk> \<Longrightarrow> \<exists>x\<in>f x. a = fst x \<and> b = map_tmres_rv Inr (snd x)
 2. \<And>x xa. xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))} \<Longrightarrow> xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} proof (prove)
goal (2 subgoals):
 1. \<And>x a b aa ba. (a, b) \<in> (case ba of Failed \<Rightarrow> {(fst (aa, ba), Failed)} | Incomplete \<Rightarrow> {(fst (aa, ba), Incomplete)} | Result p \<Rightarrow> {(fst (aa, ba), Result (Inr (fst p), snd p))}) \<Longrightarrow> a = fst (aa, ba) \<and> b = map_tmres_rv Inr (snd (aa, ba))
 2. \<And>x xa. xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))} \<Longrightarrow> xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> {y. \<exists>x\<in>f x. y = (fst x, map_tmres_rv Inr (snd x))} \<Longrightarrow> xa \<in> \<Union> {y. \<exists>x\<in>f x. y = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})} proof (prove)
goal (1 subgoal):
 1. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> \<exists>xa. (\<exists>x\<in>f x. xa = (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> {(fst x, Result (Inr (fst p), snd p))})) \<and> (aa, map_tmres_rv Inr ba) \<in> xa proof (prove)
goal (1 subgoal):
 1. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> (\<exists>xa\<in>f x. ?x58 x aa ba = (case snd xa of Failed \<Rightarrow> {(fst xa, Failed)} | Incomplete \<Rightarrow> {(fst xa, Incomplete)} | Result p \<Rightarrow> {(fst xa, Result (Inr (fst p), snd p))})) \<and> (aa, map_tmres_rv Inr ba) \<in> ?x58 x aa ba proof (prove)
goal (2 subgoals):
 1. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> \<exists>xa\<in>f x. ?x58 x aa ba = (case snd xa of Failed \<Rightarrow> {(fst xa, Failed)} | Incomplete \<Rightarrow> {(fst xa, Incomplete)} | Result p \<Rightarrow> {(fst xa, Result (Inr (fst p), snd p))})
 2. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> (aa, map_tmres_rv Inr ba) \<in> ?x58 x aa ba proof (prove)
goal (2 subgoals):
 1. \<And>x aa ba. ?x58 x aa ba = (case snd (aa, ba) of Failed \<Rightarrow> {(fst (aa, ba), Failed)} | Incomplete \<Rightarrow> {(fst (aa, ba), Incomplete)} | Result p \<Rightarrow> {(fst (aa, ba), Result (Inr (fst p), snd p))})
 2. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> (aa, map_tmres_rv Inr ba) \<in> ?x58 x aa ba proof (prove)
goal (1 subgoal):
 1. \<And>x aa ba. (aa, ba) \<in> f x \<Longrightarrow> (aa, map_tmres_rv Inr ba) \<in> (case snd (aa, ba) of Failed \<Rightarrow> {(fst (aa, ba), Failed)} | Incomplete \<Rightarrow> {(fst (aa, ba), Incomplete)} | Result p \<Rightarrow> {(fst (aa, ba), Result (Inr (fst p), snd p))}) proof (prove)
goal:
No subgoals!