theory Peterson_Atomicity

lemma release_lock_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    \<top>\<top> \<top>\<top>
    (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
    (release_lock ident) (release_lock ident)" apply (unfold release_lock_def) apply (rule prefix_refinement_weaken_pre) apply (simp add: modify_modify_bind) apply (rule prefix_refinement_bind_sr) apply (rule pfx_refn_modifyT) apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def set_label_def set_ab_def) apply (rule prefix_refinement_interference_peterson) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (release_lock ident) (release_lock ident) proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do modify (set_ab ident False);
modify (set_label ident Exited);
interference;
return ()
od) (do modify (set_ab ident False);
modify (set_label ident Exited);
interference;
return ()
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 modify (set_ab ident False);
modify (set_label ident Exited);
interference;
return ()
od) (do modify (set_ab ident False);
modify (set_label ident Exited);
interference;
return ()
od)
 2. \<forall>s s0. True \<longrightarrow> ?P' s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ?Q' t0 t 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 <- modify (set_label ident Exited \<circ> set_ab ident False);
interference
od) (do y <- modify (set_label ident Exited \<circ> set_ab ident False);
interference
od)
 2. \<forall>s s0. True \<longrightarrow> ?P' s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<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)) (modify (set_label ident Exited \<circ> set_ab ident False)) (modify (set_label ident Exited \<circ> set_ab ident False))
 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)) interference interference
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. True \<longrightarrow> (?P4 and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (6 subgoals):
 1. \<forall>s t. peterson_sr s t \<longrightarrow> True \<longrightarrow> True \<longrightarrow> peterson_sr ((set_label ident Exited \<circ> set_ab ident False) s) ((set_label ident Exited \<circ> set_ab ident False) t)
 2. \<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)) interference interference
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>_ _. True) 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)) interference interference
 2. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?P''4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>\<lambda>x _ _. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> modify (set_label ident Exited \<circ> set_ab ident False) -, \<lbrace>\<lambda>y t0 t. True\<rbrace>
 3. \<forall>s s0. True \<longrightarrow> ((\<lambda>_ _. True) and ?P'4) s0 s
 4. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> True \<longrightarrow> True \<longrightarrow> ((\<lambda>_ _. True) and ?Q'4) t0 t proof (prove)
goal:
No subgoals!