theory Peterson_Atomicity

lemma abs_critical_section_mutual_excl:
  "\<lbrace> \<lambda>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>,
   \<lbrace> peterson_rel (other_ident ident) \<rbrace>
     abs_critical_section
   \<lbrace> peterson_rel ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
               \<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>" apply (simp add: abs_critical_section_def) apply wpsimp apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) apply (safe, simp_all) by ((clarsimp simp: peterson_rel_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> invs s0 \<and> ab_label s ident = Critical \<and> csI (cs2_v s)\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_critical_section \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<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> invs s0 \<and> ab_label s ident = Critical \<and> csI (cs2_v s)\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> do y <- interferences;
y <- modify (\<lambda>s. s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>);
y <- cs2;
interference
od \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Critical \<and> csI (cs2_v s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; invs s0; ab_label s ident = Critical; csI (cs2_v s)\<rbrakk> \<Longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) s s' \<longrightarrow> csI (cs2_v s') \<and> invs s' \<and> invs (s'\<lparr>cs1_v := cs1 (cs2_v s')\<rparr>) \<and> ab_label s' ident = Critical \<and> (\<forall>s0' c. csI c \<longrightarrow> (s0' = s' \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (s'\<lparr>cs1_v := cs1 (cs2_v s'), cs2_v := c\<rparr>) s'a \<longrightarrow> invs s'a \<and> ab_label s'a ident = Critical \<and> csI (cs2_v s'a)) \<and> peterson_rel ident s' (s'\<lparr>cs1_v := cs1 (cs2_v s'), cs2_v := c\<rparr>)) \<and> ((\<exists>c'. s0' = s'\<lparr>cs1_v := cs1 (cs2_v s'), cs2_v := c'\<rparr>) \<longrightarrow> (\<forall>s'a. peterson_rel (other_ident ident) (s'\<lparr>cs1_v := cs1 (cs2_v s'), cs2_v := c\<rparr>) s'a \<longrightarrow> invs s'a \<and> ab_label s'a ident = Critical \<and> csI (cs2_v s'a)) \<and> peterson_rel ident s0' (s'\<lparr>cs1_v := cs1 (cs2_v s'), cs2_v := c\<rparr>)))) \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) \<and> (\<forall>s0' c. csI c \<longrightarrow> (s0' = s0 \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c\<rparr>) s' \<longrightarrow> invs s' \<and> ab_label s' ident = Critical \<and> csI (cs2_v s')) \<and> peterson_rel ident s0 (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c\<rparr>)) \<and> ((\<exists>c'. s0' = s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c'\<rparr>) \<longrightarrow> (\<forall>s'. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c\<rparr>) s' \<longrightarrow> invs s' \<and> ab_label s' ident = Critical \<and> csI (cs2_v s')) \<and> peterson_rel ident s0' (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; invs s0; ab_label s ident = Critical; csI (cs2_v s)\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x)\<rparr>) \<and> ab_label x ident = Critical \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident x (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident xa (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)))) \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) \<and> (\<forall>x xa. csI xa \<longrightarrow> (x = s0 \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident s0 (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>)) \<and> ((\<exists>c'. x = s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c'\<rparr>) \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident x (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; invs s0; ab_label s ident = Critical; csI (cs2_v s); ident = A\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x)\<rparr>) \<and> ab_label x ident = Critical \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident x (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident xa (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)))) \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) \<and> (\<forall>x xa. csI xa \<longrightarrow> (x = s0 \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident s0 (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>)) \<and> ((\<exists>c'. x = s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c'\<rparr>) \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident x (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>)))
 2. \<And>s0 s. \<lbrakk>peterson_rel ident s0 s; invs s; invs s0; ab_label s ident = Critical; csI (cs2_v s); ident = B\<rbrakk> \<Longrightarrow> (\<forall>x. peterson_rel (other_ident ident) s x \<and> invs x \<longrightarrow> csI (cs2_v x) \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x)\<rparr>) \<and> ab_label x ident = Critical \<and> (\<forall>xa xb. csI xb \<longrightarrow> (xa = x \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident x (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)) \<and> ((\<exists>c'. xa = x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := c'\<rparr>) \<longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> (\<forall>xa. peterson_rel (other_ident ident) (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xa \<and> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) \<and> invs xa \<longrightarrow> ab_label xa ident = Critical \<and> csI (cs2_v xa)) \<and> peterson_rel ident xa (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)))) \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s)\<rparr>) \<and> (\<forall>x xa. csI xa \<longrightarrow> (x = s0 \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident s0 (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>)) \<and> ((\<exists>c'. x = s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := c'\<rparr>) \<longrightarrow> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> (\<forall>x. peterson_rel (other_ident ident) (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) x \<and> invs (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>) \<and> invs x \<longrightarrow> ab_label x ident = Critical \<and> csI (cs2_v x)) \<and> peterson_rel ident x (s\<lparr>cs1_v := cs1 (cs2_v s), cs2_v := xa\<rparr>))) proof (prove)
goal (40 subgoals):
 1. \<And>s0 s x. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x\<rbrakk> \<Longrightarrow> csI (cs2_v x)
 2. \<And>s0 s x. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x\<rbrakk> \<Longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x)\<rparr>)
 3. \<And>s0 s x. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x\<rbrakk> \<Longrightarrow> ab_label x A = Critical
 4. \<And>s0 s x xb. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb\<rbrakk> \<Longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)
 5. \<And>s0 s x xb xc. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb; peterson_rel B (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xc; invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>); invs xc\<rbrakk> \<Longrightarrow> ab_label xc A = Critical
 6. \<And>s0 s x xb xc. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb; peterson_rel B (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xc; invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>); invs xc\<rbrakk> \<Longrightarrow> csI (cs2_v xc)
 7. \<And>s0 s x xb. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb\<rbrakk> \<Longrightarrow> peterson_rel A x (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)
 8. \<And>s0 s x xb. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb\<rbrakk> \<Longrightarrow> invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>)
 9. \<And>s0 s x xb xc. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb; peterson_rel B (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xc; invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>); invs xc\<rbrakk> \<Longrightarrow> ab_label xc A = Critical
 10. \<And>s0 s x xb xc. \<lbrakk>peterson_rel A s0 s; invs s; invs s0; ab_label s A = Critical; csI (cs2_v s); ident = A; peterson_rel B s x; invs x; csI xb; peterson_rel B (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>) xc; invs (x\<lparr>cs1_v := cs1 (cs2_v x), cs2_v := xb\<rparr>); invs xc\<rbrakk> \<Longrightarrow> csI (cs2_v xc)
A total of 40 subgoals...