theory Trace_Monad

lemma parallel_def2:
  "parallel f g = (\<lambda>s. {(xs, rv). \<exists>ys zs. (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s
    \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs
    \<and> xs = map parallel_mrg (zip ys zs)})" apply (simp add: parallel_def fun_eq_iff set_eq_iff) apply safe apply (rule exI, rule conjI, assumption)+ apply (simp add: list_all2_conv_all_nth list_eq_iff_nth_eq split_def prod_eq_iff) apply clarsimp apply (rename_tac ys zs) apply (rule_tac x="map (((\<noteq>) Env) o fst) ys" in exI) apply (simp add: zip_map1 o_def split_def) apply (strengthen subst[where P="\<lambda>xs. (xs, v) \<in> S" for v S, mk_strg I _ E]) apply (clarsimp simp: list_all2_conv_all_nth list_eq_iff_nth_eq
                        split_def prod_eq_iff
             split del: if_split cong: if_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. parallel f g = (\<lambda>s. {(xs, rv). \<exists>ys zs. (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs \<and> xs = map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs}) proof (prove)
goal (1 subgoal):
 1. \<forall>x a b. (\<exists>f_steps. length f_steps = length a \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, b) \<in> g x) = (\<exists>ys. (ys, b) \<in> f x \<and> (\<exists>zs. (zs, b) \<in> g x \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs \<and> a = map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs)) proof (prove)
goal (2 subgoals):
 1. \<And>x a b f_steps. \<lbrakk>length f_steps = length a; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f x; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, b) \<in> g x\<rbrakk> \<Longrightarrow> \<exists>ys. (ys, b) \<in> f x \<and> (\<exists>zs. (zs, b) \<in> g x \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs \<and> a = map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs)
 2. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (2 subgoals):
 1. \<And>x a b f_steps. \<lbrakk>length f_steps = length a; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f x; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, b) \<in> g x\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a) (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a) \<and> a = map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a) (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a)
 2. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (2 subgoals):
 1. \<And>x a b f_steps. \<lbrakk>length f_steps = length a; (map (\<lambda>p. (if fst p then fst (snd p) else Env, snd (snd p))) (zip f_steps a), b) \<in> f x; (map (\<lambda>p. (if fst p then Env else fst (snd p), snd (snd p))) (zip f_steps a), b) \<in> g x\<rbrakk> \<Longrightarrow> \<forall>i. f_steps ! i \<longrightarrow> fst (snd (zip f_steps a ! i)) = Env \<longrightarrow> i < length a \<longrightarrow> fst (a ! i) = Env
 2. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (1 subgoal):
 1. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (1 subgoal):
 1. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (1 subgoal):
 1. \<And>x a b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> length (map ((\<noteq>) Env \<circ> fst) ys) = length (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs) \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) (map ((\<noteq>) Env \<circ> fst) ys) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> f x \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) (map ((\<noteq>) Env \<circ> fst) ys) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs), b) \<in> g x proof (prove)
goal (1 subgoal):
 1. \<And>x b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> length ys = min (length ys) (length zs) \<and> (map (\<lambda>x. (if Env \<noteq> fst (fst x) then fst (snd (Env \<noteq> fst (fst x), snd x)) else Env, snd (snd x))) (zip ys (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip ys zs))), b) \<in> f x \<and> (map (\<lambda>x. (if Env \<noteq> fst (fst x) then Env else fst (snd (Env \<noteq> fst (fst x), snd x)), snd (snd x))) (zip ys (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip ys zs))), b) \<in> g x proof (prove)
goal (1 subgoal):
 1. \<And>x b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> length ys = min (length ys) (length zs) \<and> ys = map (\<lambda>x. (if Env \<noteq> fst (fst x) then fst (snd (Env \<noteq> fst (fst x), snd x)) else Env, snd (snd x))) (zip ys (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip ys zs))) \<and> zs = map (\<lambda>x. (if Env \<noteq> fst (fst x) then Env else fst (snd (Env \<noteq> fst (fst x), snd x)), snd (snd x))) (zip ys (map (\<lambda>p. (if fst (fst p) = Env then fst (snd p) else fst (fst p), snd (fst p))) (zip ys zs))) proof (prove)
goal (1 subgoal):
 1. \<And>x b ys zs. \<lbrakk>(ys, b) \<in> f x; (zs, b) \<in> g x; length ys = length zs; \<forall>i<length zs. (fst (ys ! i) = Env \<or> fst (zs ! i) = Env) \<and> snd (ys ! i) = snd (zs ! i)\<rbrakk> \<Longrightarrow> (\<forall>i<length zs. fst (ys ! i) = (if Env \<noteq> fst (ys ! i) then fst (ys ! i) else Env)) \<and> (\<forall>i<length zs. fst (zs ! i) = (if Env \<noteq> fst (ys ! i) then Env else if fst (ys ! i) = Env then fst (zs ! i) else fst (ys ! i))) proof (prove)
goal:
No subgoals!