theory Peterson_Atomicity

theorem peterson_proc_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    (\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
    (\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
    (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
    (abs_peterson_proc ident)
    (peterson_proc ident)" apply (simp add: abs_peterson_proc_def peterson_proc_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind_sr) apply (rule acquire_lock_refinement) apply (rule prefix_refinement_bind_sr) apply (rule critical_section_refinement) apply (rule release_lock_refinement) apply (wpsimp wp: validI_triv acquire_lock_wp
                     simp: pred_conj_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ s. invs s \<and> ab_label s ident = Exited) (\<lambda>_ s. invs s \<and> ab_label s ident = Exited) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident) proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ s. invs s \<and> ab_label s ident = Exited) (\<lambda>_ s. invs s \<and> ab_label s ident = Exited) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- acquire_lock ident;
y <- abs_critical_section;
release_lock ident
od) (do y <- acquire_lock ident;
y <- critical_section;
release_lock ident
od) proof (prove)
goal (3 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P' ?Q' (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- acquire_lock ident;
y <- abs_critical_section;
release_lock ident
od) (do y <- acquire_lock ident;
y <- critical_section;
release_lock ident
od)
 2. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> ?P' s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> ?Q' t0 t proof (prove)
goal (6 subgoals):
 1. pfx_refn peterson_sr ?rvr4 ?P4 ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (acquire_lock ident) (acquire_lock ident)
 2. \<And>x y. ?rvr4 x y \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- abs_critical_section;
release_lock ident
od) (do y <- critical_section;
release_lock ident
od)
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> (?P4 and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do y <- abs_critical_section;
release_lock ident
od) (do y <- critical_section;
release_lock ident
od)
 2. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>?P''4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (?rvr10 x y) (?P11 x) (?Q13 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) abs_critical_section critical_section
 2. \<And>x y xa ya. \<lbrakk>True; ?rvr10 x y xa ya\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''10 x y xa) (?Q''10 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (release_lock ident) (release_lock ident)
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?P'12 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_critical_section -, \<lbrace>?P''10 x y\<rbrace>
 4. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'14 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> critical_section -, \<lbrace>?Q''10 x y\<rbrace>
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>x. ?P11 x and ?P'12 x\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>y. ?Q13 y and ?Q'14 y\<rbrace>
 7. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (7 subgoals):
 1. \<And>x y xa ya. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''10 x y xa) (?Q''10 x y ya) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (release_lock ident) (release_lock ident)
 2. \<And>x y. True \<Longrightarrow> \<lbrace>?P'12 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_critical_section -, \<lbrace>?P''10 x y\<rbrace>
 3. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'14 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> critical_section -, \<lbrace>?Q''10 x y\<rbrace>
 4. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>x. (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) and ?P'12 x\<rbrace>
 5. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>y. (\<lambda>_ _. True) and ?Q'14 y\<rbrace>
 6. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (6 subgoals):
 1. \<And>x y. True \<Longrightarrow> \<lbrace>?P'12 x\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_critical_section -, \<lbrace>\<lambda>xa _ _. True\<rbrace>
 2. \<And>x y. True \<Longrightarrow> \<lbrace>?Q'14 y\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> critical_section -, \<lbrace>\<lambda>ya _ _. True\<rbrace>
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>x. (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) and ?P'12 x\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>y. (\<lambda>_ _. True) and ?Q'14 y\<rbrace>
 5. \<forall>s s0. invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal:
No subgoals!