kings-crown/FVELER_Isabelle huggingface dataset:
theory Atomicity_Lib

lemma is_matching_fragment_list_all2:
  "is_matching_fragment sr osr rvr tr' res s0 R s f
    \<Longrightarrow> list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'
    \<Longrightarrow> is_matching_fragment sr osr rvr tr res s0 R s f" apply (clarsimp simp: is_matching_fragment_def) apply (subst(asm) list_all2_is_me[symmetric], assumption, simp) apply (simp add: list_all2_matching_tr_pfx list_all2_lengthD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr tr' res s0 R s f; list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr tr res s0 R s f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'; prefix_closed f; self_closed (\<lambda>xs. length xs < length tr' \<and> fst (rev tr' ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) tr' \<and> rely_cond R s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, resa) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr tr' \<and> (length tr < length tr' \<longrightarrow> resa = Incomplete) \<and> (length tr = length tr' \<longrightarrow> rel_tmres osr rvr resa res)\<rbrakk> \<Longrightarrow> self_closed (\<lambda>xs. length xs < length tr \<and> fst (rev tr ! length xs) = Me) s f \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) tr \<and> rely_cond R s0 ((Env, s) # xs)) s f \<and> (\<forall>x\<in>f s. case x of (tra, resa) \<Rightarrow> rely_cond R s0 tra \<and> matching_tr_pfx sr tra tr \<and> (length tra < length tr \<longrightarrow> resa = Incomplete) \<and> (length tra = length tr \<longrightarrow> rel_tmres osr rvr resa res)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (rel_prod (=) (\<lambda>cs cs'. \<forall>as. sr as cs = sr as cs')) tr tr'; prefix_closed f; self_closed (\<lambda>xs. length xs < length tr \<and> fst (rev tr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) tr' \<and> rely_cond R s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, resa) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr tr' \<and> (length tr < length tr' \<longrightarrow> resa = Incomplete) \<and> (length tr = length tr' \<longrightarrow> rel_tmres osr rvr resa res)\<rbrakk> \<Longrightarrow> self_closed (\<lambda>xs. length xs < length tr \<and> fst (rev tr ! length xs) = Me) s f \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) tr \<and> rely_cond R s0 ((Env, s) # xs)) s f \<and> (\<forall>x\<in>f s. case x of (tra, resa) \<Rightarrow> rely_cond R s0 tra \<and> matching_tr_pfx sr tra tr \<and> (length tra < length tr \<longrightarrow> resa = Incomplete) \<and> (length tra = length tr \<longrightarrow> rel_tmres osr rvr resa res)) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma pfx_refinement_use_rel_tr_refinement_equivp:
  "rel_tr_refinement sr Q R False g g'
    \<Longrightarrow> equivp sr
    \<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 (erule pfx_refinement_use_rel_tr_refinement, simp_all) apply (metis equivpE sympD transpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_tr_refinement sr Q R False g g'; equivp sr; 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. \<lbrakk>equivp sr; prefix_refinement sr isr osr rvr P Q' AR R f g'\<rbrakk> \<Longrightarrow> \<forall>s t t'. sr t t' \<longrightarrow> sr s t = sr s t' proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma not_env_steps_first_bind:
  "not_env_steps_first f
    \<Longrightarrow> \<forall>x. not_env_steps_first (g x)
    \<Longrightarrow> not_env_steps_first (do x \<leftarrow> f; g x od)" apply (subst not_env_steps_first_def, clarsimp) apply (erule elem_bindE) apply (simp add: not_env_steps_firstD) apply (clarsimp simp: last_append) apply (auto elim: not_env_steps_firstD[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x)\<rbrakk> \<Longrightarrow> not_env_steps_first (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>tr res s. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x); (tr, res) \<in> (f >>= g) s; tr \<noteq> []\<rbrakk> \<Longrightarrow> fst (last tr) = Me proof (prove)
goal (2 subgoals):
 1. \<And>tr res s. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x); tr \<noteq> []; res = Incomplete \<or> res = Failed; (tr, map_tmres undefined undefined res) \<in> f s\<rbrakk> \<Longrightarrow> fst (last tr) = Me
 2. \<And>tr res s tr' tr'' x s'. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x); tr \<noteq> []; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> fst (last tr) = Me proof (prove)
goal (1 subgoal):
 1. \<And>tr res s tr' tr'' x s'. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x); tr \<noteq> []; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'; tr = tr'' @ tr'\<rbrakk> \<Longrightarrow> fst (last tr) = Me proof (prove)
goal (1 subgoal):
 1. \<And>res s tr' tr'' x s'. \<lbrakk>not_env_steps_first f; \<forall>x. not_env_steps_first (g x); tr'' = [] \<longrightarrow> tr' \<noteq> []; (tr', Result (x, s')) \<in> f s; (tr'', res) \<in> g x s'\<rbrakk> \<Longrightarrow> (tr' = [] \<longrightarrow> fst (last tr'') = Me) \<and> (tr' \<noteq> [] \<longrightarrow> fst (last tr') = Me) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma not_env_steps_first_no_trace:
  "no_trace f \<Longrightarrow> not_env_steps_first f" by (fastforce simp add: not_env_steps_first_def dest: no_trace_emp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_trace f \<Longrightarrow> not_env_steps_first f
theory Atomicity_Lib

lemma not_env_steps_first_interference:
  "not_env_steps_first interference" apply (simp add: interference_def commit_step_def bind_def get_def
                   return_def put_trace_elem_def) apply (clarsimp simp: not_env_steps_first_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_env_steps_first interference proof (prove)
goal (1 subgoal):
 1. not_env_steps_first (\<lambda>s. insert ([], Incomplete) ((\<lambda>(a, y). (a @ [(Me, s)], y)) ` env_steps s)) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma not_env_steps_first_repeat_n:
  "not_env_steps_first f \<Longrightarrow> not_env_steps_first (repeat_n n f)" by (induct n; simp add: not_env_steps_first_bind not_env_steps_first_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_env_steps_first f \<Longrightarrow> not_env_steps_first (repeat_n n f)
theory Atomicity_Lib

lemma not_env_steps_first_repeat:
  "not_env_steps_first f \<Longrightarrow> not_env_steps_first (repeat f)" by (simp add: repeat_def not_env_steps_first_bind
                   not_env_steps_first_repeat_n not_env_steps_first_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_env_steps_first f \<Longrightarrow> not_env_steps_first (repeat f)
theory Atomicity_Lib

lemma alternative_distrib_lhs_bind:
  "(f \<sqinter> g) >>= h = ((f >>= h) \<sqinter> (g >>= h))" by (simp add: bind_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> g) >>= h = (f >>= h \<sqinter> g >>= h)
theory Atomicity_Lib

lemma shuttle_modify_commit_step[simplified K_bind_def]:
  "\<forall>s. sr s (f s) \<Longrightarrow> rel_tr_refinement sr P R C
    (do x \<leftarrow> commit_step; modify f od) (do x \<leftarrow> modify f; commit_step od)" apply (simp add: rel_tr_refinement_def commit_step_def
                   put_trace_elem_def bind_def get_def return_def modify_def put_def) apply (simp add: rely_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. sr s (f s) \<Longrightarrow> rel_tr_refinement sr P R C (do x <- commit_step;
modify f
od) (do x <- modify f;
commit_step
od) proof (prove)
goal (1 subgoal):
 1. \<forall>s. sr s (f s) \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>s0. rely_cond R s0 [(Me, s)] \<longrightarrow> (C \<longrightarrow> s0 = s) \<longrightarrow> rely_cond R s0 [(Me, f s)]) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma shuttle_gets_commit_step[simplified K_bind_def]:
  "reflp sr \<Longrightarrow> rel_tr_refinement sr P R C
    (do x \<leftarrow> commit_step; gets f od) (do x \<leftarrow> gets f; commit_step; return x od)" apply (simp add: rel_tr_refinement_def commit_step_def
                   put_trace_elem_def bind_def get_def return_def gets_def) apply (simp add: rely_cond_def reflpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp sr \<Longrightarrow> rel_tr_refinement sr P R C (do x <- commit_step;
gets f
od) (do x <- gets f;
commit_step;
return x
od) proof (prove)
goal (1 subgoal):
 1. reflp sr \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>s0. rely_cond R s0 [(Me, s)] \<longrightarrow> (C \<longrightarrow> s0 = s) \<longrightarrow> sr s s) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma last_st_tr_in_set:
  "last_st_tr (map (Pair x) ss') s \<in> set (ss' @ [s])" by (clarsimp simp: last_st_tr_def o_def hd_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. last_st_tr (map (Pair x) ss') s \<in> set (ss' @ [s])
theory Atomicity_Lib

lemma shuttle_gets_env_step[simplified K_bind_def]:
  "reflp sr \<Longrightarrow> \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> f s = f t
    \<Longrightarrow> rel_tr_refinement sr P R True
        (do x \<leftarrow> env_step; gets f od) (do x \<leftarrow> gets f; env_step; return x od)" apply (simp add: rel_tr_refinement_def env_step_def select_def
                   put_trace_elem_def bind_def get_def return_def gets_def put_def) apply (clarsimp simp: rely_cond_def reflpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp sr; \<forall>s t. P s \<longrightarrow> R s t \<longrightarrow> f s = f t\<rbrakk> \<Longrightarrow> rel_tr_refinement sr P R True (do x <- env_step;
gets f
od) (do x <- gets f;
env_step;
return x
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp sr; \<forall>s. P s \<longrightarrow> (\<forall>t. R s t \<longrightarrow> f s = f t)\<rbrakk> \<Longrightarrow> \<forall>tr res s. P s \<longrightarrow> (\<exists>x. tr = [(Env, x)] \<and> res = Result (f x, x)) \<longrightarrow> rely_cond R s tr \<longrightarrow> (\<exists>tr'. ((\<exists>x. tr' = [(Env, x)] \<and> res = Result (f s, x)) \<or> tr' = [] \<and> res = Incomplete) \<and> rely_cond R s tr' \<and> list_all2 (rel_prod (=) sr) tr tr') proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma env_step_twp[wp]:
  "\<lbrace>\<lambda>s0 s. (\<forall>s'. R s0 s' \<longrightarrow> Q () s' s')\<rbrace>,\<lbrace>R\<rbrace> env_step \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: env_step_def) apply (wp put_trace_elem_twp) apply (clarsimp simp: rely_cond_def drop_Cons' guar_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<forall>s'. R s0 s' \<longrightarrow> Q () s' s'\<rbrace>, \<lbrace>R\<rbrace> env_step \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<forall>s'. R s0 s' \<longrightarrow> Q () s' s'\<rbrace>, \<lbrace>R\<rbrace> do s' <- select UNIV;
y <- put_trace_elem (Env, s');
put s'
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<forall>s'. R s0 s' \<longrightarrow> Q () s' s' \<Longrightarrow> \<forall>x\<in>UNIV. (\<forall>n. rely_cond R s0 (drop n [(Env, x)]) \<longrightarrow> guar_cond G s0 (drop n [(Env, x)])) \<and> (rely_cond R s0 [(Env, x)] \<longrightarrow> Q () (snd (Env, x)) x) proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma adjust_tr_relation_equivp:
  "equivp sr
    \<Longrightarrow> adjust_tr_relation sr sr" apply (simp add: adjust_tr_relation_def) apply (metis equivpE sympD transpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equivp sr \<Longrightarrow> adjust_tr_relation sr sr proof (prove)
goal (1 subgoal):
 1. equivp sr \<Longrightarrow> \<forall>s t t'. sr t t' \<longrightarrow> sr s t = sr s t' proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma other_ident_split:
  "P (other_ident x) = ((x = A \<longrightarrow> P B) \<and> (x = B \<longrightarrow> P A))" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (other_ident x) = ((x = A \<longrightarrow> P B) \<and> (x = B \<longrightarrow> P A))
theory Peterson_Atomicity

lemma neq_A_B[simp]:
  "(x \<noteq> A) = (x = B)"
  "(A \<noteq> x) = (x = B)"
  "(x \<noteq> B) = (x = A)"
  "(B \<noteq> x) = (x = A)" by (simp | cases x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x \<noteq> A) = (x = B) &&& (A \<noteq> x) = (x = B)) &&& (x \<noteq> B) = (x = A) &&& (B \<noteq> x) = (x = A)
theory Peterson_Atomicity

lemma forall_ident_eq:
  "(\<forall>ident. P ident) = (P A \<and> P B)" using ident.nchotomy by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>ident. P ident) = (P A \<and> P B) proof (prove)
using this:
\<forall>ident. ident = A \<or> ident = B

goal (1 subgoal):
 1. (\<forall>ident. P ident) = (P A \<and> P B)
theory Peterson_Atomicity

lemma other_other_ident_simps[simp]:
  "other_ident (other_ident x) = x"
  "(other_ident x = y) = (x \<noteq> y)"
  "(x = other_ident y) = (x \<noteq> y)" by (simp_all split: other_ident_split add: eq_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. other_ident (other_ident x) = x &&& (other_ident x = y) = (x \<noteq> y) &&& (x = other_ident y) = (x \<noteq> y)
theory Peterson_Atomicity

lemma peterson_rel_rtranclp[simp]:
  "rtranclp (peterson_rel ident) = (peterson_rel ident)" apply (rule rtranclp_id2) apply (clarsimp simp: peterson_rel_def) apply (clarsimp simp: peterson_rel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (peterson_rel ident)\<^sup>*\<^sup>* = peterson_rel ident proof (prove)
goal (2 subgoals):
 1. \<forall>x. peterson_rel ident x x
 2. \<forall>x xa. (peterson_rel ident OO peterson_rel ident) x xa \<le> peterson_rel ident x xa proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. (peterson_rel ident OO peterson_rel ident) x xa \<le> peterson_rel ident x xa proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma reflp_peterson_rel[simp]:
 "reflp (peterson_rel x)" apply (rule reflpI) apply (clarsimp simp add: peterson_rel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp (peterson_rel x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. peterson_rel x xa xa proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma peterson_rel_imp_assume_invs:
  "invs x \<Longrightarrow> (peterson_rel ident x y \<and> invs x \<and> invs y \<longrightarrow> P x y)
    \<Longrightarrow> (peterson_rel ident x y \<longrightarrow> P x y)" by (simp add: peterson_rel_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs x; peterson_rel ident x y \<and> invs x \<and> invs y \<longrightarrow> P x y\<rbrakk> \<Longrightarrow> peterson_rel ident x y \<longrightarrow> P x y
theory Peterson_Atomicity

theorem abs_peterson_proc_mutual_excl:
  "\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
            \<and> ab_label s ident = Exited \<rbrace>,
   \<lbrace> peterson_rel (other_ident ident) \<rbrace>
     abs_peterson_proc ident
   \<lbrace> peterson_rel ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
               \<and> ab_label s ident = Exited \<rbrace>" apply (simp add: abs_peterson_proc_def bind_assoc) apply (wpsimp wp: release_lock_mutual_excl acquire_lock_mutual_excl
                    abs_critical_section_mutual_excl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_peterson_proc ident \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> do y <- acquire_lock ident;
y <- abs_critical_section;
release_lock ident
od \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma peterson_sr_set_ab[simp]:
 "peterson_sr s t \<Longrightarrow> peterson_sr (set_ab ident v s) (set_ab ident v t)" by (simp add: peterson_sr_def set_ab_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. peterson_sr s t \<Longrightarrow> peterson_sr (set_ab ident v s) (set_ab ident v t)
theory Peterson_Atomicity

lemma env_stable_peterson_sr:
  "env_stable AR R peterson_sr peterson_sr \<top>" by (fastforce simp: env_stable_def rely_stable_def env_rely_stable_iosr_def peterson_sr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable AR R peterson_sr peterson_sr (\<lambda>_. True)
theory Peterson_Atomicity

lemma peterson_sr_reflp[simp]:
  "reflp peterson_sr" by (simp add: peterson_sr_def reflpI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp peterson_sr
theory Peterson_Atomicity

lemma peterson_sr_cs1_invs: "peterson_sr_cs1 s t \<Longrightarrow> invs s = invs t" apply (auto simp: peterson_sr_def peterson_sr_cs1_def invs_def
                     req_peterson_inv_def key_peterson_inv_def
                     local_peterson_inv_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. peterson_sr_cs1 s t \<Longrightarrow> invs s = invs t proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma peterson_rel_imp_label:
  "peterson_rel (other_ident ident) x y \<Longrightarrow> invs x
   \<Longrightarrow> ab_label x ident = ab_label y ident" by (simp add: peterson_rel_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_rel (other_ident ident) x y; invs x\<rbrakk> \<Longrightarrow> ab_label x ident = ab_label y ident
theory Peterson_Atomicity

lemma peterson_rel_set_label:
  "peterson_rel (other_ident ident) (set_label ident label s) s'
   \<Longrightarrow> invs (set_label ident label s)
   \<Longrightarrow> ab_label s' ident = label" by (simp add: peterson_rel_def set_label_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_rel (other_ident ident) (set_label ident label s) s'; invs (set_label ident label s)\<rbrakk> \<Longrightarrow> ab_label s' ident = label
theory Peterson_Atomicity

lemma peterson_sr_invs[simp]:
  "peterson_sr as cs \<Longrightarrow> invs as \<Longrightarrow> invs cs" by (simp add: peterson_sr_def invs_def invs_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_sr as cs; invs as\<rbrakk> \<Longrightarrow> invs cs
theory Peterson_Atomicity

lemma peterson_sr_invs_sym:
  "peterson_sr as cs \<Longrightarrow> invs cs \<Longrightarrow> invs as" by (simp add: peterson_sr_def invs_def invs_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_sr as cs; invs cs\<rbrakk> \<Longrightarrow> invs as
theory Peterson_Atomicity

lemma peterson_sr_ab_label:
  "peterson_sr as cs \<Longrightarrow> ab_label as = ab_label cs" by (simp add: peterson_sr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. peterson_sr as cs \<Longrightarrow> ab_label as = ab_label cs
theory Peterson_Atomicity

lemma critical_section_prefix_closed[simp]:
  "prefix_closed critical_section" by (auto intro!: prefix_closed_bind
           simp: cs_closed critical_section_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed critical_section
theory Peterson_Atomicity

lemma abs_critical_section_prefix_closed[simp]:
  "prefix_closed abs_critical_section" by (auto intro!: prefix_closed_bind
           simp: cs_closed abs_critical_section_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed abs_critical_section
theory Peterson_Atomicity

lemma peterson_rel_trans:
 "peterson_rel ident x y \<Longrightarrow> peterson_rel ident y z \<Longrightarrow>
  peterson_rel ident x z" by (clarsimp simp: peterson_rel_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_rel ident x y; peterson_rel ident y z\<rbrakk> \<Longrightarrow> peterson_rel ident x z
theory Peterson_Atomicity

lemma invs_set_label_Critical:
  "invs s \<Longrightarrow> locked ident s \<Longrightarrow> ab_label s ident = Awaiting
   \<Longrightarrow> invs (set_label ident Critical s)" by (auto simp: invs_def invs_defs set_label_def locked_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; locked ident s; ab_label s ident = Awaiting\<rbrakk> \<Longrightarrow> invs (set_label ident Critical s)
theory Peterson_Atomicity

lemma acquire_lock_prefix_closed[simp]:
  "prefix_closed (acquire_lock ident)" by (auto intro!: prefix_closed_bind
           simp: cs_closed acquire_lock_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (acquire_lock ident)
theory Peterson_Atomicity

lemma peterson_rel_helpers:
  "peterson_rel2 ident s0 s \<and> peterson_rel3 ident s0 s
   \<longrightarrow> peterson_rel ident s0 s" by (clarsimp simp: peterson_rel_def peterson_rel2_def peterson_rel3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. peterson_rel2 ident s0 s \<and> peterson_rel3 ident s0 s \<longrightarrow> peterson_rel ident s0 s
theory Peterson_Atomicity

lemma peterson_rel_peterson_rel2:
  "peterson_rel ident s0 s \<Longrightarrow> peterson_rel2 ident s0 s" by (clarsimp simp: peterson_rel_def peterson_rel2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. peterson_rel ident s0 s \<Longrightarrow> peterson_rel2 ident s0 s