theory Peterson_Atomicity

lemma cs2_wp_apply_peterson[wp]:
 "\<lbrace> (\<lambda>s0 s. csI (cs2_v s)
      \<and> invs s0 \<and> invs s \<and> critical (ab_label s ident)
      \<and> cs1_v s = cs1 (cs2_v s)
      \<and> (\<forall>s0' c' c. csI c \<longrightarrow> (\<exists>c'. s0' = s0 \<or> s0' = s \<lparr> cs2_v := c' \<rparr>)
              \<longrightarrow>  Q () s0' (s \<lparr> cs2_v := c\<rparr>))) \<rbrace>,
  \<lbrace> peterson_rel (other_ident ident) \<rbrace>
    cs2
  \<lbrace> peterson_rel ident \<rbrace>,
  \<lbrace> Q \<rbrace>" apply (rule validI_name_pre[OF cs_closed], clarsimp simp del: imp_disjL) apply (rule rg_weaken_pre) apply (rule validI_well_behaved[OF cs_closed]) apply (rule rg_strengthen_post) apply (rule_tac s=s and ?s0.0=s0
         and lockf="\<lambda>s. critical (ab_label s ident)"
         and I="invs" in cs_wp) apply (clarsimp simp: invs_defs invs_def) apply (clarsimp simp del: imp_disjL) apply (simp only: imp_conjL[symmetric]) apply (thin_tac "\<forall>x. P x" for P) apply (clarsimp simp: peterson_rel_def) apply (thin_tac "\<forall>x. P x" for P) apply (clarsimp simp: peterson_rel_def) apply (cases ident; fastforce simp: invs_def key_peterson_inv_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. csI (cs2_v s) \<and> invs s0 \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v s = cs1 (cs2_v s) \<and> (\<forall>s0' c' c. csI c \<longrightarrow> (\<exists>c'. s0' = s0 \<or> s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>))\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0' s'. s0' = s0 \<and> s' = s\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<lbrace>?P'10 s0 s\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> cs2 \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> ?P'10 s0 s s0a sa proof (prove)
goal (4 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<lbrace>?P'10 s0 s\<rbrace>, \<lbrace>?R'13 s0 s\<rbrace> cs2 \<lbrace>?G'13 s0 s\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<longrightarrow> ?R'13 s0 s x xa
 3. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. ?G'13 s0 s x xa \<longrightarrow> peterson_rel ident x xa
 4. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> ?P'10 s0 s s0a sa proof (prove)
goal (5 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<lbrace>?P'10 s0 s\<rbrace>, \<lbrace>?R'13 s0 s\<rbrace> cs2 \<lbrace>?G'13 s0 s\<rbrace>, \<lbrace>?Q'17 s0 s\<rbrace>
 2. \<And>s0 s v s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); ?Q'17 s0 s v s0a sa\<rbrakk> \<Longrightarrow> Q v s0a sa
 3. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<longrightarrow> ?R'13 s0 s x xa
 4. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. ?G'13 s0 s x xa \<longrightarrow> peterson_rel ident x xa
 5. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> ?P'10 s0 s s0a sa proof (prove)
goal (5 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>s c. invs s \<and> ab_label s ident = Critical \<longrightarrow> invs s \<and> ab_label (s\<lparr>cs2_v := c\<rparr>) ident = Critical
 2. \<And>s0 s v s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); \<exists>c. csI c \<and> sa = s\<lparr>cs2_v := c\<rparr> \<and> (\<exists>c'. s0a = s0 \<or> s0a = s\<lparr>cs2_v := c'\<rparr>) \<and> invs sa \<and> ab_label sa ident = Critical\<rbrakk> \<Longrightarrow> Q v s0a sa
 3. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<longrightarrow> invs x \<and> ab_label x ident = Critical \<longrightarrow> cs2_v xa = cs2_v x \<and> invs xa \<and> ab_label xa ident = Critical \<and> cs1_v xa = cs1_v x
 4. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 5. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (4 subgoals):
 1. \<And>s0 s v s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); \<exists>c. csI c \<and> sa = s\<lparr>cs2_v := c\<rparr> \<and> (\<exists>c'. s0a = s0 \<or> s0a = s\<lparr>cs2_v := c'\<rparr>) \<and> invs sa \<and> ab_label sa ident = Critical\<rbrakk> \<Longrightarrow> Q v s0a sa
 2. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<longrightarrow> invs x \<and> ab_label x ident = Critical \<longrightarrow> cs2_v xa = cs2_v x \<and> invs xa \<and> ab_label xa ident = Critical \<and> cs1_v xa = cs1_v x
 3. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 4. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (3 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<longrightarrow> invs x \<and> ab_label x ident = Critical \<longrightarrow> cs2_v xa = cs2_v x \<and> invs xa \<and> ab_label xa ident = Critical \<and> cs1_v xa = cs1_v x
 2. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 3. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (3 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<and> (s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>)) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<and> invs x \<and> ab_label x ident = Critical \<longrightarrow> cs2_v xa = cs2_v x \<and> invs xa \<and> ab_label xa ident = Critical \<and> cs1_v xa = cs1_v x
 2. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 3. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (3 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s)\<rbrakk> \<Longrightarrow> \<forall>x xa. peterson_rel (other_ident ident) x xa \<and> invs x \<and> ab_label x ident = Critical \<longrightarrow> cs2_v xa = cs2_v x \<and> invs xa \<and> ab_label xa ident = Critical \<and> cs1_v xa = cs1_v x
 2. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 3. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 2. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (2 subgoals):
 1. \<And>s0 s. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s)\<rbrakk> \<Longrightarrow> \<forall>x xa. (invs x \<longrightarrow> (\<exists>c. xa = x\<lparr>cs2_v := c\<rparr>) \<and> invs xa \<and> ab_label xa ident = Critical) \<longrightarrow> peterson_rel ident x xa
 2. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (2 subgoals):
 1. \<And>s0 s x c. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); invs x; invs (x\<lparr>cs2_v := c\<rparr>); ab_label x ident = Critical; ab_label x (other_ident ident) = Critical\<rbrakk> \<Longrightarrow> c = cs2_v x
 2. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s s0a sa. \<lbrakk>csI (cs2_v s); invs s0; invs s; ab_label s ident = Critical; cs1_v s = cs1 (cs2_v s); \<forall>s0' c. csI c \<longrightarrow> s0' = s0 \<or> (\<exists>c'. s0' = s\<lparr>cs2_v := c'\<rparr>) \<longrightarrow> Q () s0' (s\<lparr>cs2_v := c\<rparr>); s0a = s0 \<and> sa = s\<rbrakk> \<Longrightarrow> csI (cs2_v sa) \<and> s0a = s0 \<and> sa = s \<and> invs s \<and> ab_label s ident = Critical \<and> cs1_v sa = cs1 (cs2_v sa) proof (prove)
goal:
No subgoals!