theory Trace_Prefix_Closed

lemma prefix_closed_parallel[wp_split]:
  "\<lbrakk>prefix_closed f; prefix_closed g\<rbrakk>
   \<Longrightarrow> prefix_closed (parallel f g)" apply (subst prefix_closed_def, clarsimp simp: parallel_def) apply (subst (asm) zip.zip_Cons) apply (clarsimp split: list.splits) apply (drule(1) prefix_closedD)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; prefix_closed g\<rbrakk> \<Longrightarrow> prefix_closed (parallel f g) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba f_steps. \<lbrakk>prefix_closed f; prefix_closed g; length f_steps = Suc (length xs); (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps ((a, b) # xs), ba) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps ((a, b) # xs), ba) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length xs \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba f_steps. \<lbrakk>prefix_closed f; prefix_closed g; length f_steps = Suc (length xs); (map (\<lambda>(f_step, id, y). (if f_step then id else Env, y)) (case f_steps of [] \<Rightarrow> [] | z # zs \<Rightarrow> (z, a, b) # zip zs xs), ba) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps ((a, b) # xs), ba) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length xs \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba x21 x22. \<lbrakk>((if x21 then Env else a, b) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) x22 xs, ba) \<in> g s; prefix_closed f; prefix_closed g; length x22 = length xs; ((if x21 then a else Env, b) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) x22 xs, ba) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length xs \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba x21 x22. \<lbrakk>((if x21 then Env else a, b) # map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) x22 xs, ba) \<in> g s; length x22 = length xs; ((if x21 then a else Env, b) # map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) x22 xs, ba) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) x22 xs, Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) x22 xs, Incomplete) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length xs \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps xs, Incomplete) \<in> f s \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps xs, Incomplete) \<in> g s proof (prove)
goal:
No subgoals!