theory Peterson_Atomicity

lemma acquire_lock_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>
     acquire_lock ident
   \<lbrace> peterson_rel ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0
               \<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>" apply (simp add: acquire_lock_def) apply (wpsimp wp: Await_sync_twp) apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) apply (safe, simp_all) by ((clarsimp simp: peterson_rel_def set_label_def set_ab_def
                      locked_def invs_defs
    | rule invs_def[THEN iffD2] conjI
    | rev_drule invs_def[THEN iffD1])+)

(* 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> acquire_lock ident \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0 \<and> ab_label s ident = Critical \<and> csI (cs2_v s)\<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 <- 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>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0 \<and> ab_label s ident = Critical \<and> csI (cs2_v s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s s'. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; peterson_rel (other_ident ident) s s'\<rbrakk> \<Longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) s'a \<longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s'a x \<and> locked ident x \<longrightarrow> peterson_rel ident x (set_label ident Critical x) \<and> invs (set_label ident Critical x) \<and> invs x \<and> ab_label (set_label ident Critical x) ident = Critical \<and> csI (cs2_v (set_label ident Critical x)))) \<and> peterson_rel ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s s'. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; peterson_rel (other_ident ident) s s'\<rbrakk> \<Longrightarrow> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x \<and> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs x \<longrightarrow> (\<forall>xa. peterson_rel (other_ident ident) x xa \<and> locked ident xa \<longrightarrow> peterson_rel ident xa (set_label ident Critical xa) \<and> invs (set_label ident Critical xa) \<and> invs xa \<and> ab_label (set_label ident Critical xa) ident = Critical \<and> csI (cs2_v (set_label ident Critical xa)))) \<and> peterson_rel ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s0 s s'. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; peterson_rel (other_ident ident) s s'; ident = A\<rbrakk> \<Longrightarrow> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x \<and> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs x \<longrightarrow> (\<forall>xa. peterson_rel (other_ident ident) x xa \<and> locked ident xa \<longrightarrow> peterson_rel ident xa (set_label ident Critical xa) \<and> invs (set_label ident Critical xa) \<and> invs xa \<and> ab_label (set_label ident Critical xa) ident = Critical \<and> csI (cs2_v (set_label ident Critical xa)))) \<and> peterson_rel ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>))
 2. \<And>s0 s s'. \<lbrakk>peterson_rel ident s0 s; invs s; ab_label s ident = Exited; peterson_rel (other_ident ident) s s'; ident = B\<rbrakk> \<Longrightarrow> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> (\<forall>x. peterson_rel (other_ident ident) (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) x \<and> invs (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) \<and> invs x \<longrightarrow> (\<forall>xa. peterson_rel (other_ident ident) x xa \<and> locked ident xa \<longrightarrow> peterson_rel ident xa (set_label ident Critical xa) \<and> invs (set_label ident Critical xa) \<and> invs xa \<and> ab_label (set_label ident Critical xa) ident = Critical \<and> csI (cs2_v (set_label ident Critical xa)))) \<and> peterson_rel ident s' (set_label ident Awaiting (set_ab ident True s'\<lparr>t_v := other_ident ident\<rparr>)) proof (prove)
goal (14 subgoals):
 1. \<And>s0 s s'. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A\<rbrakk> \<Longrightarrow> invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>))
 2. \<And>s0 s s' x xa. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A; peterson_rel B (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)) x; invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)); invs x; peterson_rel B x xa; locked A xa\<rbrakk> \<Longrightarrow> peterson_rel A xa (set_label A Critical xa)
 3. \<And>s0 s s' x xa. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A; peterson_rel B (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)) x; invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)); invs x; peterson_rel B x xa; locked A xa\<rbrakk> \<Longrightarrow> invs (set_label A Critical xa)
 4. \<And>s0 s s' x xa. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A; peterson_rel B (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)) x; invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)); invs x; peterson_rel B x xa; locked A xa\<rbrakk> \<Longrightarrow> invs xa
 5. \<And>s0 s s' x xa. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A; peterson_rel B (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)) x; invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)); invs x; peterson_rel B x xa; locked A xa\<rbrakk> \<Longrightarrow> ab_label (set_label A Critical xa) A = Critical
 6. \<And>s0 s s' x xa. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A; peterson_rel B (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)) x; invs (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>)); invs x; peterson_rel B x xa; locked A xa\<rbrakk> \<Longrightarrow> csI (cs2_v (set_label A Critical xa))
 7. \<And>s0 s s'. \<lbrakk>peterson_rel A s0 s; invs s; ab_label s A = Exited; peterson_rel B s s'; ident = A\<rbrakk> \<Longrightarrow> peterson_rel A s' (set_label A Awaiting (set_ab A True s'\<lparr>t_v := B\<rparr>))
 8. \<And>s0 s s'. \<lbrakk>peterson_rel B s0 s; invs s; ab_label s B = Exited; peterson_rel A s s'; ident = B\<rbrakk> \<Longrightarrow> invs (set_label B Awaiting (set_ab B True s'\<lparr>t_v := A\<rparr>))
 9. \<And>s0 s s' x xa. \<lbrakk>peterson_rel B s0 s; invs s; ab_label s B = Exited; peterson_rel A s s'; ident = B; peterson_rel A (set_label B Awaiting (set_ab B True s'\<lparr>t_v := A\<rparr>)) x; invs (set_label B Awaiting (set_ab B True s'\<lparr>t_v := A\<rparr>)); invs x; peterson_rel A x xa; locked B xa\<rbrakk> \<Longrightarrow> peterson_rel B xa (set_label B Critical xa)
 10. \<And>s0 s s' x xa. \<lbrakk>peterson_rel B s0 s; invs s; ab_label s B = Exited; peterson_rel A s s'; ident = B; peterson_rel A (set_label B Awaiting (set_ab B True s'\<lparr>t_v := A\<rparr>)) x; invs (set_label B Awaiting (set_ab B True s'\<lparr>t_v := A\<rparr>)); invs x; peterson_rel A x xa; locked B xa\<rbrakk> \<Longrightarrow> invs (set_label B Critical xa)
A total of 14 subgoals...