theory Atomicity_Lib

lemma detrace_bind:
  "detrace (f >>= (\<lambda>x. g x)) = (detrace f >>= (\<lambda>x. detrace (g x)))" apply (simp add: bind_def) apply (simp add: detrace_UN) apply (simp add: bind_def detrace_def image_UN) apply (rule ext, safe) apply (rule UN_I, erule IntI) apply (clarsimp split: tmres.split_asm) apply (clarsimp split: tmres.split_asm) apply fastforce apply (erule UN_I) apply (clarsimp split: tmres.split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (f >>= g) = do x <- detrace f;
detrace (g x)
od proof (prove)
goal (1 subgoal):
 1. detrace (\<lambda>s. \<Union>x\<in>f s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, b). (a @ xs, b)) ` g rv s) = (\<lambda>s. \<Union>x\<in>detrace f s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, b). (a @ xs, b)) ` detrace (g rv) s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<Union>x\<in>f s. detrace (\<lambda>s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s) s) = (\<lambda>s. \<Union>x\<in>detrace f s. case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, b). (a @ xs, b)) ` detrace (g rv) s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<Union>x\<in>f s. (\<lambda>x. case x of (tr, x) \<Rightarrow> ([], x)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) = (\<lambda>s. \<Union>x\<in>f s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}. case case x of (tr, x) \<Rightarrow> ([], x) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` (\<lambda>x. case x of (tr, x) \<Rightarrow> ([], x)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(aa, ba) \<in> f s; (ab, bb) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` g rv s); Env \<notin> fst ` set ab; bb \<noteq> Incomplete\<rbrakk> \<Longrightarrow> ([], bb) \<in> (\<Union>x\<in>f s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}. case case x of (tr, x) \<Rightarrow> ([], x) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}))
 2. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); (aa, ba) \<in> f s; Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>x\<in>f s. (\<lambda>(tr, y). ([], y)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(ab, bb) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` g rv s); Env \<notin> fst ` set ab; bb \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (aa, ba) \<in> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}
 2. \<And>s a b aa ba ab bb. \<lbrakk>(aa, ba) \<in> f s; (ab, bb) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` g rv s); Env \<notin> fst ` set ab; bb \<noteq> Incomplete\<rbrakk> \<Longrightarrow> ([], bb) \<in> (case case (aa, ba) of (tr, x) \<Rightarrow> ([], x) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}))
 3. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); (aa, ba) \<in> f s; Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>x\<in>f s. (\<lambda>(tr, y). ([], y)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba ab bb. \<lbrakk>(aa, ba) \<in> f s; (ab, bb) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` g rv s); Env \<notin> fst ` set ab; bb \<noteq> Incomplete\<rbrakk> \<Longrightarrow> ([], bb) \<in> (case case (aa, ba) of (tr, x) \<Rightarrow> ([], x) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}))
 2. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); (aa, ba) \<in> f s; Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>x\<in>f s. (\<lambda>(tr, y). ([], y)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (2 subgoals):
 1. \<And>s aa a b ac bc. \<lbrakk>Env \<notin> fst ` (set ac \<union> set aa); bc \<noteq> Incomplete; (aa, Result (a, b)) \<in> f s; (ac, bc) \<in> g a b\<rbrakk> \<Longrightarrow> ([], bc) \<in> (\<lambda>x. case x of (tr, x) \<Rightarrow> ([], x)) ` (g a b \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})
 2. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); (aa, ba) \<in> f s; Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>x\<in>f s. (\<lambda>(tr, y). ([], y)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); (aa, ba) \<in> f s; Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>x\<in>f s. (\<lambda>(tr, y). ([], y)) ` ((case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> (case ba of Failed \<Rightarrow> {([], Failed)} | Incomplete \<Rightarrow> {([], Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ [], y)) ` (\<lambda>(tr, y). ([], y)) ` (g rv s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})); Env \<notin> fst ` set aa; ba \<noteq> Incomplete\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<lambda>(tr, y). ([], y)) ` ((case (aa, ba) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>(a, y). (a @ xs, y)) ` g rv s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}) proof (prove)
goal (1 subgoal):
 1. \<And>aa ab bb ac bc. \<lbrakk>Env \<notin> fst ` set aa; (ac, bc) \<in> g ab bb; Env \<notin> fst ` set ac; bc \<noteq> Incomplete\<rbrakk> \<Longrightarrow> ([], bc) \<in> (\<lambda>x. case x of (tr, x) \<Rightarrow> ([], x)) ` ((\<lambda>x. case x of (a, x) \<Rightarrow> (a @ aa, x)) ` g ab bb \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}) proof (prove)
goal:
No subgoals!