theory Prefix_Refinement

lemma par_tr_fragment_parallel_def:
  "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> parallel f g s = {(tr, res). \<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}" apply (rule equalityI; clarsimp) apply (auto simp: parallel_def)[1] apply (erule(4) par_tr_fragment_in_parallel) apply blast 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\<rbrakk> \<Longrightarrow> parallel f g s = {(tr, res). \<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} proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<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; (a, b) \<in> parallel f g s\<rbrakk> \<Longrightarrow> \<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 s \<and> (\<exists>res'. (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, res') \<in> g s)
 2. \<And>a b 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 a; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, res') \<in> g s\<rbrakk> \<Longrightarrow> (a, b) \<in> parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>a b 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 a; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, res') \<in> g s\<rbrakk> \<Longrightarrow> (a, b) \<in> parallel f g s proof (prove)
goal (1 subgoal):
 1. \<And>a b f_steps res'. \<lbrakk>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 a; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps a, b) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps a, res') \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_steps res'. length f_steps = length a \<and> (map2 (\<lambda>f_step (id, s). (if f_step then id else Env, s)) f_steps a, b) \<in> f s \<and> (map2 (\<lambda>f_step (id, s). (if f_step then Env else id, s)) f_steps a, res') \<in> g s proof (prove)
goal:
No subgoals!