theory Peterson_Atomicity

lemma acquire_lock_wp:
  "\<lbrace> \<lambda>s0 s. invs s \<and> ab_label s ident = Exited \<rbrace>,
   \<lbrace> peterson_rel (other_ident ident) \<rbrace>
     acquire_lock ident
   \<lbrace> \<top>\<top> \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. invs s \<and> ab_label s ident = Critical \<rbrace>" apply (simp add: acquire_lock_def) apply (wpsimp wp: Await_sync_twp) apply (subst (asm) peterson_rel_imp_label, assumption+) apply (drule(1) peterson_rel_imp_invs) apply (drule(1) peterson_rel_trans) apply (thin_tac "peterson_rel (other_ident ident) s'a x") apply (frule peterson_rel_set_label) apply (fastforce simp: set_label_def set_ab_def
                          locked_def invs_def invs_defs) apply (drule peterson_rel_imp_invs) apply (fastforce simp: set_label_def set_ab_def
                          locked_def invs_def invs_defs) apply (clarsimp simp: invs_set_label_Critical) apply (clarsimp simp: set_label_def set_ab_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> acquire_lock ident -, \<lbrace>\<lambda>rv s0 s. invs s \<and> ab_label s ident = Critical\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> do y <- interference;
y <- modify (set_ab ident True);
y <- modify (t_v_update (\<lambda>_. other_ident ident));
y <- modify (set_label ident Awaiting);
y <- interference;
y <- Await (locked ident);
modify (set_label ident Critical)
od -, \<lbrace>\<lambda>rv s0 s. invs s \<and> ab_label s ident = Critical\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s ident = Exited; peterson_rel (other_ident ident) s s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a; peterson_rel (other_ident ident) s'a x; locked ident x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; peterson_rel (other_ident ident) s s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a; peterson_rel (other_ident ident) s'a x; locked ident x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a; peterson_rel (other_ident ident) s'a x; locked ident x; invs s'\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; peterson_rel (other_ident ident) s'a x; locked ident x; invs s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (2 subgoals):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x\<rbrakk> \<Longrightarrow> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>))
 2. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x; ab_label x ident = Awaiting\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x; ab_label x ident = Awaiting\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (2 subgoals):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; ab_label x ident = Awaiting\<rbrakk> \<Longrightarrow> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>))
 2. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; ab_label x ident = Awaiting; invs x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' s'a x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; ab_label x ident = Awaiting; invs x\<rbrakk> \<Longrightarrow> invs (set_label ident Critical x) \<and> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>invs s; ab_label s' ident = Exited; locked ident x; invs s'; ab_label x ident = Awaiting; invs x\<rbrakk> \<Longrightarrow> ab_label (set_label ident Critical x) ident = Critical proof (prove)
goal:
No subgoals!