theory Prefix_Refinement

lemma par_tr_fragment_in_parallel:
  "par_tr_fin_principle f
    \<Longrightarrow> par_tr_fin_principle g
    \<Longrightarrow> is_matching_fragment sr osr rvr ctr1 cres s0 R s f
    \<Longrightarrow> is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g
    \<Longrightarrow> length ctr1 = length ctr2
    \<Longrightarrow> \<exists>f_steps res'. length f_steps = length tr
        \<and> (map (\<lambda>(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps tr), res) \<in> f s
        \<and> (map (\<lambda>(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps tr), res') \<in> g s
    \<Longrightarrow> (tr, res) \<in> parallel f g s" apply (clarsimp simp: parallel_def) apply (rule_tac x=f_steps in exI, clarsimp) apply (drule(2) par_tr_fin_fragment)+ apply (simp only: list_all2_lengthD) apply (clarsimp split: nat.split_asm tmres.split_asm) apply (simp add: last_st_tr_def o_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; par_tr_fin_principle g; is_matching_fragment sr osr rvr ctr1 cres s0 R s f; is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; length ctr1 = length ctr2; \<exists>f_steps res'. length f_steps = length tr \<and> (map2 (\<lambda>f_step (id, s). (if f_step then id else Env, s)) f_steps tr, res) \<in> f s \<and> (map2 (\<lambda>f_step (id, s). (if f_step then Env else id, s)) f_steps tr, res') \<in> g s\<rbrakk> \<Longrightarrow> (tr, res) \<in> parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps res'. \<lbrakk>par_tr_fin_principle f; par_tr_fin_principle g; is_matching_fragment sr osr rvr ctr1 cres s0 R s f; is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; length ctr1 = length ctr2; length f_steps = length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, res) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res') \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_steps. length f_steps = length tr \<and> (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, res) \<in> f s \<and> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps res'. \<lbrakk>par_tr_fin_principle f; par_tr_fin_principle g; is_matching_fragment sr osr rvr ctr1 cres s0 R s f; is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; length ctr1 = length ctr2; length f_steps = length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, res) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res') \<in> g s\<rbrakk> \<Longrightarrow> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps res'. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres s0 R s f; is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; length ctr1 = length ctr2; length f_steps = length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, res) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res') \<in> g s; res = (case (length ctr1 - length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete); res' = (case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete)\<rbrakk> \<Longrightarrow> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps res'. \<lbrakk>is_matching_fragment sr osr rvr ctr1 cres s0 R s f; is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; length ctr1 = length ctr2; length f_steps = length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete) \<in> g s; res = (case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete); res' = (case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete)\<rbrakk> \<Longrightarrow> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, case (length ctr2 - length (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr), cres) of (0, Failed) \<Rightarrow> Failed | (0, Incomplete) \<Rightarrow> Incomplete | (0, Result x) \<Rightarrow> Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s) | (Suc nat, b) \<Rightarrow> Incomplete) \<in> g s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps a b. \<lbrakk>res = Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s); is_matching_fragment sr osr rvr ctr1 (Result (a, b)) s0 R s f; is_matching_fragment sr osr' rvr ctr2 (Result (a, b)) s0 R' s g; length ctr1 = length ctr2; length f_steps = length tr; length ctr2 \<le> length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s)) \<in> f s; cres = Result (a, b); (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr) s)) \<in> g s\<rbrakk> \<Longrightarrow> (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, Result ((), last_st_tr (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr) s)) \<in> g s proof (prove)
goal:
No subgoals!