theory Trace_Prefix_Closed

lemma prefix_closed_liftM_eq[simp]:
  "prefix_closed (liftM f m) = prefix_closed m" apply (clarsimp simp: prefix_closed_def bind_def' liftM_def return_def image_def) apply (rule iff_allI)+ apply safe apply clarsimp apply (drule_tac x="((a, b) # xs, map_tmres id f ba)" in bspec) apply clarsimp apply (case_tac ba; clarsimp) apply (auto split: tmres.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (liftM f m) = prefix_closed m proof (prove)
goal (1 subgoal):
 1. (\<forall>s a b xs. (\<exists>x\<in>{y. \<exists>x. (x, Failed) \<in> m s \<and> y = (x, Failed)} \<union> {y. \<exists>x. (x, Incomplete) \<in> m s \<and> y = (x, Incomplete)} \<union> \<Union> {y. \<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> y = {(a, Result (f aa, b))}}. (a, b) # xs = fst x) \<longrightarrow> (xs, Incomplete) \<in> m s \<or> (\<exists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x)) = (\<forall>s a b xs. (\<exists>x\<in>m s. (a, b) # xs = fst x) \<longrightarrow> (xs, Incomplete) \<in> m s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs. ((\<exists>x\<in>{y. \<exists>x. (x, Failed) \<in> m s \<and> y = (x, Failed)} \<union> {y. \<exists>x. (x, Incomplete) \<in> m s \<and> y = (x, Incomplete)} \<union> \<Union> {y. \<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> y = {(a, Result (f aa, b))}}. (a, b) # xs = fst x) \<longrightarrow> (xs, Incomplete) \<in> m s \<or> (\<exists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x)) = ((\<exists>x\<in>m s. (a, b) # xs = fst x) \<longrightarrow> (xs, Incomplete) \<in> m s) proof (prove)
goal (4 subgoals):
 1. \<And>s a b xs aa ba. \<lbrakk>(aa, ba) \<in> m s; (a, b) # xs = fst (aa, ba); \<not> (\<exists>x\<in>{y. \<exists>x. (x, Failed) \<in> m s \<and> y = (x, Failed)} \<union> {y. \<exists>x. (x, Incomplete) \<in> m s \<and> y = (x, Incomplete)} \<union> \<Union> {y. \<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> y = {(a, Result (f aa, b))}}. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 2. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Failed); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Failed) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 3. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Incomplete); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Incomplete) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 4. \<And>s a b xs aa ba X ab ac bb. \<lbrakk>(a, b) # xs = fst (ab, Result (f ac, bb)); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (ab, Result (ac, bb)) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s proof (prove)
goal (4 subgoals):
 1. \<And>s a b xs ba. \<lbrakk>((a, b) # xs, ba) \<in> m s; \<forall>x\<in>{y. \<exists>x. (x, Failed) \<in> m s \<and> y = (x, Failed)} \<union> {y. \<exists>x. (x, Incomplete) \<in> m s \<and> y = (x, Incomplete)} \<union> \<Union> {y. \<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> y = {(a, Result (f aa, b))}}. (a, b) # xs \<noteq> fst x\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 2. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Failed); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Failed) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 3. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Incomplete); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Incomplete) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 4. \<And>s a b xs aa ba X ab ac bb. \<lbrakk>(a, b) # xs = fst (ab, Result (f ac, bb)); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (ab, Result (ac, bb)) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s proof (prove)
goal (5 subgoals):
 1. \<And>s a b xs ba. ((a, b) # xs, ba) \<in> m s \<Longrightarrow> ((a, b) # xs, map_tmres_rv f ba) \<in> {y. \<exists>x. (x, Failed) \<in> m s \<and> y = (x, Failed)} \<union> {y. \<exists>x. (x, Incomplete) \<in> m s \<and> y = (x, Incomplete)} \<union> \<Union> {y. \<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> y = {(a, Result (f aa, b))}}
 2. \<And>s a b xs ba. \<lbrakk>((a, b) # xs, ba) \<in> m s; (a, b) # xs \<noteq> fst ((a, b) # xs, map_tmres_rv f ba)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 3. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Failed); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Failed) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 4. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Incomplete); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Incomplete) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 5. \<And>s a b xs aa ba X ab ac bb. \<lbrakk>(a, b) # xs = fst (ab, Result (f ac, bb)); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (ab, Result (ac, bb)) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s proof (prove)
goal (5 subgoals):
 1. \<And>s a b xs ba. \<lbrakk>((a, b) # xs, ba) \<in> m s; ((a, b) # xs, Failed) \<in> m s \<longrightarrow> map_tmres_rv f ba \<noteq> Failed; \<forall>x. (\<forall>a aa b. (a, Result (aa, b)) \<in> m s \<longrightarrow> x \<noteq> {(a, Result (f aa, b))}) \<or> ((a, b) # xs, map_tmres_rv f ba) \<notin> x\<rbrakk> \<Longrightarrow> ((a, b) # xs, Incomplete) \<in> m s \<and> map_tmres_rv f ba = Incomplete
 2. \<And>s a b xs ba. \<lbrakk>((a, b) # xs, ba) \<in> m s; (a, b) # xs \<noteq> fst ((a, b) # xs, map_tmres_rv f ba)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 3. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Failed); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Failed) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 4. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Incomplete); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Incomplete) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 5. \<And>s a b xs aa ba X ab ac bb. \<lbrakk>(a, b) # xs = fst (ab, Result (f ac, bb)); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (ab, Result (ac, bb)) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s proof (prove)
goal (5 subgoals):
 1. \<And>s a b xs aa bb. \<lbrakk>((a, b) # xs, Result (aa, bb)) \<in> m s; \<forall>x. (\<forall>a aa b. (a, Result (aa, b)) \<in> m s \<longrightarrow> x \<noteq> {(a, Result (f aa, b))}) \<or> ((a, b) # xs, Result (f aa, bb)) \<notin> x\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b xs ba. \<lbrakk>((a, b) # xs, ba) \<in> m s; (a, b) # xs \<noteq> fst ((a, b) # xs, map_tmres_rv f ba)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 3. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Failed); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Failed) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 4. \<And>s a b xs aa ba x. \<lbrakk>(a, b) # xs = fst (x, Incomplete); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (x, Incomplete) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s
 5. \<And>s a b xs aa ba X ab ac bb. \<lbrakk>(a, b) # xs = fst (ab, Result (f ac, bb)); \<nexists>x. (\<exists>a aa b. (a, Result (aa, b)) \<in> m s \<and> x = {(a, Result (f aa, b))}) \<and> (xs, Incomplete) \<in> x; (ab, Result (ac, bb)) \<in> m s; \<not> (\<exists>x\<in>m s. (a, b) # xs = fst x)\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> m s proof (prove)
goal:
No subgoals!