theory Atomicity_Lib

lemma pfx_refinement_use_rel_tr_refinement:
  "rel_tr_refinement tr_r Q R False g g'
    \<Longrightarrow> \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q' AR R f g'
    \<Longrightarrow> prefix_refinement sr isr osr rvr P (\<lambda>s0. Q and Q' s0) AR R f g" apply (subst prefix_refinement_def, clarsimp) apply (drule(3) rel_tr_refinementD, simp) apply clarsimp apply (drule(5) prefix_refinementD) apply clarsimp apply (rule exI, rule conjI[rotated], assumption) apply (erule is_matching_fragment_list_all2) apply (erule list_all2_mono) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_tr_refinement tr_r Q R False g g'; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; prefix_refinement sr isr osr rvr P Q' AR R f g'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr P (\<lambda>s0. Q and Q' s0) AR R f g proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>rel_tr_refinement tr_r Q R False g g'; \<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; prefix_refinement sr isr osr rvr P Q' AR R f g'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr rvr a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; prefix_refinement sr isr osr rvr P Q' AR R f g'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; \<exists>tr'. (tr', b) \<in> g' t \<and> rely_cond R t0 tr' \<and> list_all2 (rel_prod (=) tr_r) a tr'\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr rvr a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr'. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; prefix_refinement sr isr osr rvr P Q' AR R f g'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; list_all2 (rel_prod (=) tr_r) a tr'\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr rvr a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr'. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; list_all2 (rel_prod (=) tr_r) a tr'; case (tr', b) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>fa. is_matching_fragment sr osr rvr ctr cres s0 AR s fa \<and> triv_refinement f fa)\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr rvr a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr' fa. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; list_all2 (rel_prod (=) tr_r) a tr'; is_matching_fragment sr osr rvr tr' b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr rvr a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr' fa. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; list_all2 (rel_prod (=) tr_r) a tr'; is_matching_fragment sr osr rvr tr' b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr a b s0 AR s fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr' fa. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; list_all2 (rel_prod (=) tr_r) a tr'; triv_refinement f fa\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) a tr' proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b tr' fa xs ys. \<lbrakk>\<forall>s t t'. tr_r t t' \<longrightarrow> sr s t = sr s t'; isr s t; P s0 s; sr s0 t0; (a, b) \<in> g t; Q t; Q' t0 t; rely_cond R t0 a; (tr', b) \<in> g' t; rely_cond R t0 tr'; triv_refinement f fa; rel_prod (=) tr_r xs ys\<rbrakk> \<Longrightarrow> rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs') xs ys proof (prove)
goal:
No subgoals!