theory Trace_No_Trace

lemma no_trace_liftM_eq[simp]:
  "no_trace (liftM f m) = no_trace m" apply (clarsimp simp: no_trace_def bind_def liftM_def return_def) apply safe apply (drule_tac x=tr in spec) apply (drule_tac x="map_tmres id f res" in spec) apply (drule mp) apply (rule exI) apply (erule rev_bexI) apply (clarsimp split: tmres.splits) apply clarsimp apply (drule spec, drule spec, drule mp, rule exI, erule rev_bexI) apply (auto split: tmres.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace (liftM f m) = no_trace m proof (prove)
goal (1 subgoal):
 1. (\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete) = (\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete) proof (prove)
goal (4 subgoals):
 1. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, res) \<in> m s\<rbrakk> \<Longrightarrow> tr = []
 2. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; \<forall>res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 2. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; (\<exists>s. \<exists>x\<in>m s. (tr, map_tmres_rv f res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> map_tmres_rv f res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 2. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>tr res s. (tr, res) \<in> m s \<Longrightarrow> \<exists>s. \<exists>x\<in>m s. (tr, map_tmres_rv f res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})
 2. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; tr = [] \<and> map_tmres_rv f res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 3. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 5. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>tr res s. (tr, res) \<in> m s \<Longrightarrow> \<exists>x\<in>m (?s42 tr res s). (tr, map_tmres_rv f res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})
 2. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; tr = [] \<and> map_tmres_rv f res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 3. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 5. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>tr res s. (tr, map_tmres_rv f res) \<in> (case (tr, res) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})
 2. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; tr = [] \<and> map_tmres_rv f res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 3. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 5. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>tr res s. \<lbrakk>(tr, res) \<in> m s; tr = [] \<and> map_tmres_rv f res \<noteq> Incomplete\<rbrakk> \<Longrightarrow> tr = []
 2. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>tr res s. \<lbrakk>\<forall>tr res. (\<exists>s. \<exists>x\<in>m s. (tr, res) \<in> (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (tr, Incomplete) \<in> m s\<rbrakk> \<Longrightarrow> False
 2. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>tr res s. (?tr50 tr res s, ?res52 tr res s) \<in> (case (tr, Incomplete) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> {(xs, Result (f rv, s))})
 2. \<And>tr res s. \<lbrakk>(tr, Incomplete) \<in> m s; ?tr50 tr res s = [] \<and> ?res52 tr res s \<noteq> Incomplete\<rbrakk> \<Longrightarrow> False
 3. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, res) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> tr = []
 4. \<And>tr res s a b. \<lbrakk>\<forall>tr res. (\<exists>s. (tr, res) \<in> m s) \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete; (a, b) \<in> m s; (tr, Incomplete) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> {(a, Result (f rv, s))})\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!