kings-crown/FVELER_Isabelle huggingface dataset:
theory Atomicity_Lib

lemma interferences_twp[wp]:
  "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> interferences \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  (is "\<lbrace>?P\<rbrace>,\<lbrace>R\<rbrace> ?f \<lbrace>G\<rbrace>,\<lbrace>?Q\<rbrace>") apply (rule rg_strengthen_post, rule repeat_validI) apply wp apply (clarsimp simp: reflpD[where R=G]) apply (metis rtranclp_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s\<rbrace>, \<lbrace>R\<rbrace> interferences \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s\<rbrace>, \<lbrace>R\<rbrace> interference \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s\<rbrace>
 2. \<And>v s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s \<Longrightarrow> Q v s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s \<Longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> (\<forall>s'a. R\<^sup>*\<^sup>* s' s'a \<longrightarrow> Q () s'a s'a) \<and> G s' s' \<and> reflp G \<and> Q () s' s') \<and> G s0 s
 2. \<And>v s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s \<Longrightarrow> Q v s0 s proof (prove)
goal (2 subgoals):
 1. \<And>s0 s s' s'a. \<lbrakk>\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s'; G s0 s; reflp G; Q () s0 s; R\<^sup>*\<^sup>* s s'; R\<^sup>*\<^sup>* s' s'a\<rbrakk> \<Longrightarrow> Q () s'a s'a
 2. \<And>v s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s \<Longrightarrow> Q v s0 s proof (prove)
goal (1 subgoal):
 1. \<And>v s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s \<Longrightarrow> Q v s0 s proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma repeat_pre_triv_refinement[simplified]:
  "triv_refinement (repeat f) (do f; repeat f od)" apply (simp add: repeat_def select_early) apply (rule triv_refinement_select_concrete_All; clarsimp) apply (rule_tac x="Suc x" in triv_refinement_select_abstract_x; simp) apply (rule triv_refinement_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement (repeat f) (do f;
repeat f
od) proof (prove)
goal (1 subgoal):
 1. triv_refinement (do n <- select UNIV;
repeat_n n f
od) (do n <- select UNIV;
y <- f;
repeat_n n f
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. triv_refinement (do n <- select UNIV;
repeat_n n f
od) (do y <- f;
repeat_n x f
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. triv_refinement (do y <- f;
repeat_n x f
od) (do y <- f;
repeat_n x f
od) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma repeat_none_triv_refinement:
  "triv_refinement (repeat f) (return ())" apply (simp add: repeat_def) apply (rule_tac x="0" in triv_refinement_select_abstract_x; simp) apply (rule triv_refinement_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement (repeat f) (return ()) proof (prove)
goal (1 subgoal):
 1. triv_refinement (do n <- select UNIV;
repeat_n n f
od) (return ()) proof (prove)
goal (1 subgoal):
 1. triv_refinement (return ()) (return ()) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma detrace_UN:
  "detrace (\<lambda>s. \<Union>x \<in> S s. f x s)
    = (\<lambda>s. \<Union>x \<in> S s. detrace (f x) s)" apply (simp add: detrace_def) apply (rule ext; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (\<lambda>s. \<Union>x\<in>S s. f x s) = (\<lambda>s. \<Union>x\<in>S s. detrace (f x) s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<lambda>x. case x of (tr, res) \<Rightarrow> ([], res)) ` ((\<Union>x\<in>S s. f x s) \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) = (\<lambda>s. \<Union>x\<in>S s. (\<lambda>x. case x of (tr, x) \<Rightarrow> ([], x)) ` (f x s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma det_detrace_eq:
  "det f \<Longrightarrow> detrace f = f" apply (clarsimp simp: det_def detrace_def) apply (rule ext, drule_tac x=s in spec) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> detrace f = f proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>a b. f s = {([], Result (a, b))} \<Longrightarrow> (\<lambda>s. (\<lambda>x. case x of (tr, res) \<Rightarrow> ([], res)) ` (f s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete})) = f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>a b. f s = {([], Result (a, b))} \<Longrightarrow> (\<lambda>x. case x of (tr, res) \<Rightarrow> ([], res)) ` (f s \<inter> {tr. Env \<notin> fst ` set tr} \<times> {res. res \<noteq> Incomplete}) = f s proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma detrace_select[simp]:
  "detrace (select S) = select S" by (rule ext, auto simp add: select_def detrace_def image_image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (select S) = select S
theory Atomicity_Lib

lemma detrace_put_trace:
  "detrace (put_trace xs) = (if Env \<in> fst ` set xs
    then (\<lambda>_. {}) else return ())" apply (induct xs; simp) apply (clarsimp simp: detrace_bind detrace_put_trace_elem) apply (simp add: bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (put_trace xs) = (if Env \<in> fst ` set xs then \<lambda>_. {} else return ()) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. detrace (put_trace xs) = (if Env \<in> fst ` set xs then \<lambda>_. {} else return ()) \<Longrightarrow> (Env = fst a \<longrightarrow> detrace (do _ <- put_trace xs;
put_trace_elem a
od) = (\<lambda>_. {})) \<and> (Env \<in> fst ` set xs \<longrightarrow> detrace (do _ <- put_trace xs;
put_trace_elem a
od) = (\<lambda>_. {})) \<and> (Env \<noteq> fst a \<and> Env \<notin> fst ` set xs \<longrightarrow> detrace (do _ <- put_trace xs;
put_trace_elem a
od) = return ()) proof (prove)
goal (1 subgoal):
 1. \<And>xs b. \<lbrakk>detrace (put_trace xs) = (\<lambda>_. {}); (Env, b) \<in> set xs\<rbrakk> \<Longrightarrow> do _ <- \<lambda>_. {};
\<lambda>_. {}
od = (\<lambda>_. {}) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma detrace_repeat_n:
  "detrace (repeat_n n f) = repeat_n n (detrace f)" by (induct n; simp add: detrace_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (repeat_n n f) = repeat_n n (detrace f)
theory Atomicity_Lib

lemma detrace_repeat:
  "detrace (repeat f) = repeat (detrace f)" by (simp add: repeat_def detrace_repeat_n detrace_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace (repeat f) = repeat (detrace f)
theory Atomicity_Lib

lemma detrace_env_step:
  "detrace env_step = (\<lambda>_. {})" apply (simp add: env_step_def detrace_bind detrace_put_trace_elem) apply (simp add: bind_def select_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace env_step = (\<lambda>_. {}) proof (prove)
goal (1 subgoal):
 1. do s' <- select UNIV;
y <- \<lambda>_. {};
put s'
od = (\<lambda>_. {}) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma repeat_n_nothing:
  "repeat_n n (\<lambda>_. {}) = (if n = 0 then return () else (\<lambda>_. {}))" by (induct n; simp add: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. repeat_n n (\<lambda>_. {}) = (if n = 0 then return () else (\<lambda>_. {}))
theory Atomicity_Lib

lemma repeat_nothing:
  "repeat (\<lambda>_. {}) = return ()" by (simp add: repeat_def bind_def select_def repeat_n_nothing
                Sigma_def if_distribR UN_If_distrib return_def
           cong del: image_cong_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. repeat (\<lambda>_. {}) = return ()
theory Atomicity_Lib

lemma detrace_env_steps:
  "detrace env_steps = return ()" by (simp add: env_steps_repeat detrace_repeat detrace_env_step repeat_nothing)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace env_steps = return ()
theory Atomicity_Lib

lemma detrace_interference:
  "detrace interference = return ()" apply (simp add: interference_def detrace_bind commit_step_def
                   detrace_env_steps detrace_put_trace_elem) apply (simp add: bind_def get_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detrace interference = return () proof (prove)
goal (1 subgoal):
 1. do s <- get;
return ()
od = return () proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma equivp_compare_f:
  "equivp (\<lambda>x y. f x = f y)" by (simp add: equivp_def fun_eq_iff, metis)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equivp (\<lambda>x y. f x = f y)
theory Atomicity_Lib

lemma equivp_split_eqs:
  "equivp (fst_split_eq f)"
  "equivp (snd_split_eq f)" by (simp_all add: fst_split_eq_def snd_split_eq_def equivp_compare_f)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equivp (fst_split_eq f) &&& equivp (snd_split_eq f)
theory Atomicity_Lib

lemma dom_s_match_refl:
  "dom_s_match ds D s s" by (simp add: dom_s_match_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom_s_match ds D s s
theory Atomicity_Lib

lemma dom_s_match_equivp:
  "equivp (dom_s_match ds D)" apply (intro equivpI reflpI dom_s_match_refl) apply (rule sympI, simp add: dom_s_match_def) apply (rule transpI, simp add: dom_s_match_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equivp (dom_s_match ds D) proof (prove)
goal (2 subgoals):
 1. symp (dom_s_match ds D)
 2. transp (dom_s_match ds D) proof (prove)
goal (1 subgoal):
 1. transp (dom_s_match ds D) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma dom_s_match_mono:
  "dom_s_match ds D s s' \<Longrightarrow> D' \<subseteq> D
    \<Longrightarrow> dom_s_match ds D' s s'" by (auto simp add: dom_s_match_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom_s_match ds D s s'; D' \<subseteq> D\<rbrakk> \<Longrightarrow> dom_s_match ds D' s s'
theory Atomicity_Lib

lemma diamond_flips:
  "diamond ds s sa sb sab \<Longrightarrow> diamond ds sb sab s sa"
  "diamond ds s sa sb sab \<Longrightarrow> diamond ds sa s sab sb" by (auto simp add: diamond_def, metis+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (diamond ds s sa sb sab \<Longrightarrow> diamond ds sb sab s sa) &&& (diamond ds s sa sb sab \<Longrightarrow> diamond ds sa s sab sb)
theory Atomicity_Lib

lemma diamond_diag_flip:
  "diamond ds s sa sb sab \<Longrightarrow> diamond ds s sb sa sab" by (simp add: diamond_def, metis)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diamond ds s sa sb sab \<Longrightarrow> diamond ds s sb sa sab
theory Atomicity_Lib

lemma diamond_unique:
  "domains_complete ds \<Longrightarrow> diamond ds s sa sb sab
    \<Longrightarrow> diamond ds s sa sb sab' \<Longrightarrow> sab = sab'" apply (erule domains_completeD) apply (simp add: diamond_def) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domains_complete ds; diamond ds s sa sb sab; diamond ds s sa sb sab'\<rbrakk> \<Longrightarrow> sab = sab' proof (prove)
goal (1 subgoal):
 1. \<And>d. \<lbrakk>diamond ds s sa sb sab; diamond ds s sa sb sab'\<rbrakk> \<Longrightarrow> ds sab d = ds sab' d proof (prove)
goal (1 subgoal):
 1. \<And>d. \<lbrakk>\<forall>d. ds sab d = ds sa d \<and> ds sb d = ds s d \<or> ds sab d = ds sb d \<and> ds sa d = ds s d; \<forall>d. ds sab' d = ds sa d \<and> ds sb d = ds s d \<or> ds sab' d = ds sb d \<and> ds sa d = ds s d\<rbrakk> \<Longrightarrow> ds sab d = ds sab' d proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma diamond_uniques_other:
  "domains_complete ds \<Longrightarrow> diamond ds s sa sb sab
    \<Longrightarrow> diamond ds s sa sb' sab \<Longrightarrow> sb = sb'"
  "domains_complete ds \<Longrightarrow> diamond ds s sa sb sab
    \<Longrightarrow> diamond ds s sa' sb sab \<Longrightarrow> sa = sa'"
  "domains_complete ds \<Longrightarrow> diamond ds s sa sb sab
    \<Longrightarrow> diamond ds s' sa sb sab \<Longrightarrow> s = s'" by (metis diamond_unique diamond_flips)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>domains_complete ds; diamond ds s sa sb sab; diamond ds s sa sb' sab\<rbrakk> \<Longrightarrow> sb = sb') &&& (\<lbrakk>domains_complete ds; diamond ds s sa sb sab; diamond ds s sa' sb sab\<rbrakk> \<Longrightarrow> sa = sa') &&& (\<lbrakk>domains_complete ds; diamond ds s sa sb sab; diamond ds s' sa sb sab\<rbrakk> \<Longrightarrow> s = s')
theory Atomicity_Lib

lemma dom_s_match_diamond:
  "dom_s_match ds D s sa \<Longrightarrow> diamond ds s sa sb sab
    \<Longrightarrow> dom_s_match ds D sb sab" apply (simp add: dom_s_match_def diamond_def) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom_s_match ds D s sa; diamond ds s sa sb sab\<rbrakk> \<Longrightarrow> dom_s_match ds D sb sab proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>d\<in>D. ds sa d = ds s d; \<forall>d. ds sab d = ds sa d \<and> ds sb d = ds s d \<or> ds sab d = ds sb d \<and> ds sa d = ds s d\<rbrakk> \<Longrightarrow> \<forall>d\<in>D. ds sab d = ds sb d proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma diamond_trans:
  "diamond ds s sa sb sab \<Longrightarrow> diamond ds sb sab sc sac \<Longrightarrow> diamond ds s sa sc sac" by (simp add: diamond_def, metis)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>diamond ds s sa sb sab; diamond ds sb sab sc sac\<rbrakk> \<Longrightarrow> diamond ds s sa sc sac
theory Atomicity_Lib

lemma diamond_trans_eq:
  "diamond ds s sa sb sab \<Longrightarrow> (diamond ds sb sab = diamond ds s sa)" by (simp add: fun_eq_iff, metis diamond_trans diamond_flips)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diamond ds s sa sb sab \<Longrightarrow> diamond ds sb sab = diamond ds s sa
theory Atomicity_Lib

lemma rely_cond_equiv_s:
  "rely_cond R s0 tr
    \<Longrightarrow> (\<And>s. tr \<noteq> [] \<Longrightarrow> last tr = (Env, s) \<Longrightarrow> R s0 s \<Longrightarrow> R s0' s)
    \<Longrightarrow> rely_cond R s0' tr" apply (cases tr rule: rev_cases) apply simp apply (clarsimp simp: rely_cond_append rely_cond_def[where tr="Cons x xs" for x xs]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 tr; \<And>s. \<lbrakk>tr \<noteq> []; last tr = (Env, s); R s0 s\<rbrakk> \<Longrightarrow> R s0' s\<rbrakk> \<Longrightarrow> rely_cond R s0' tr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rely_cond R s0 tr; \<And>s. \<lbrakk>tr \<noteq> []; last tr = (Env, s); R s0 s\<rbrakk> \<Longrightarrow> R s0' s; tr = []\<rbrakk> \<Longrightarrow> rely_cond R s0' tr
 2. \<And>ys y. \<lbrakk>rely_cond R s0 tr; \<And>s. \<lbrakk>tr \<noteq> []; last tr = (Env, s); R s0 s\<rbrakk> \<Longrightarrow> R s0' s; tr = ys @ [y]\<rbrakk> \<Longrightarrow> rely_cond R s0' tr proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>rely_cond R s0 tr; \<And>s. \<lbrakk>tr \<noteq> []; last tr = (Env, s); R s0 s\<rbrakk> \<Longrightarrow> R s0' s; tr = ys @ [y]\<rbrakk> \<Longrightarrow> rely_cond R s0' tr proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma rel_tr_refinement_refl:
  "reflp sr
    \<Longrightarrow> rel_tr_refinement sr P R C f f" apply (clarsimp simp: rel_tr_refinement_def) apply (intro exI, rule conjI, assumption) apply (simp add: list_all2_same rel_prod_sel reflpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp sr \<Longrightarrow> rel_tr_refinement sr P R C f f proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> f s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>reflp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> rely_cond R s0 tr \<and> list_all2 (rel_prod (=) sr) tr tr proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma rel_tr_refinement_drop_C:
  "rel_tr_refinement sr P R False f g
    \<Longrightarrow> rel_tr_refinement sr P R C f g" by (clarsimp simp: rel_tr_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_tr_refinement sr P R False f g \<Longrightarrow> rel_tr_refinement sr P R C f g
theory Atomicity_Lib

lemma rel_tr_refinement_trans:
  "transp sr
    \<Longrightarrow> rel_tr_refinement sr P R C f g
    \<Longrightarrow> rel_tr_refinement sr P R C g h
    \<Longrightarrow> rel_tr_refinement sr P R C f h" apply (subst rel_tr_refinement_def, clarsimp) apply (drule(3) rel_tr_refinementD, clarsimp+) apply (drule(3) rel_tr_refinementD, clarsimp+) apply (intro exI, rule conjI, assumption, clarsimp) apply (erule(1) list_all2_trans[rotated]) apply clarsimp apply (metis transpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transp sr; rel_tr_refinement sr P R C f g; rel_tr_refinement sr P R C g h\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R C f h proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0. \<lbrakk>transp sr; rel_tr_refinement sr P R C f g; rel_tr_refinement sr P R C g h; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> h s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr'. \<lbrakk>transp sr; rel_tr_refinement sr P R C g h; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', res) \<in> g s; rely_cond R s0 tr'; list_all2 (rel_prod (=) sr) tr tr'\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> h s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr' tr'a. \<lbrakk>transp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', res) \<in> g s; rely_cond R s0 tr'; list_all2 (rel_prod (=) sr) tr tr'; (tr'a, res) \<in> h s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> \<exists>tr'. (tr', res) \<in> h s \<and> rely_cond R s0 tr' \<and> list_all2 (rel_prod (=) sr) tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr' tr'a. \<lbrakk>transp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', res) \<in> g s; rely_cond R s0 tr'; list_all2 (rel_prod (=) sr) tr tr'; (tr'a, res) \<in> h s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) sr) tr tr'a proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr' tr'a a b c. \<lbrakk>transp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', res) \<in> g s; rely_cond R s0 tr'; (tr'a, res) \<in> h s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; rel_prod (=) sr a b; rel_prod (=) sr b c\<rbrakk> \<Longrightarrow> rel_prod (=) sr a c proof (prove)
goal (1 subgoal):
 1. \<And>tr res s s0 tr' tr'a b ba bb. \<lbrakk>transp sr; P s; (tr, res) \<in> f s; rely_cond R s0 tr; C \<longrightarrow> s0 = s; (tr', res) \<in> g s; rely_cond R s0 tr'; (tr'a, res) \<in> h s; rely_cond R s0 tr'a; list_all2 (rel_prod (=) sr) tr' tr'a; sr b ba; sr ba bb\<rbrakk> \<Longrightarrow> sr b bb proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma list_all2_matching_tr_pfx:
  "list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'
    \<Longrightarrow> matching_tr_pfx sr atr tr = matching_tr_pfx sr atr tr'" apply (simp add: matching_tr_pfx_def list_all2_lengthD matching_tr_def) apply (intro conj_cong; simp?) apply (clarsimp simp: list_all2_conv_all_nth rel_prod_sel split_def) apply (simp add: rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr' \<Longrightarrow> matching_tr_pfx sr atr tr = matching_tr_pfx sr atr tr' proof (prove)
goal (1 subgoal):
 1. list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr' \<Longrightarrow> (length atr \<le> length tr' \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev atr) (take (length atr) (rev tr))) = (length atr \<le> length tr' \<and> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev atr) (take (length atr) (rev tr'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'; length atr \<le> length tr'\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev atr) (take (length atr) (rev tr)) = list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev atr) (take (length atr) (rev tr')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length atr \<le> length tr'; length tr = length tr'; \<forall>i<length tr'. fst (tr ! i) = fst (tr' ! i) \<and> (\<forall>as. sr as (snd (tr ! i)) = sr as (snd (tr' ! i)))\<rbrakk> \<Longrightarrow> (\<forall>i<length atr. fst (rev atr ! i) = fst (rev tr ! i) \<and> sr (snd (rev atr ! i)) (snd (rev tr ! i))) = (\<forall>i<length atr. fst (rev atr ! i) = fst (rev tr' ! i) \<and> sr (snd (rev atr ! i)) (snd (rev tr' ! i))) proof (prove)
goal:
No subgoals!