theory Peterson_Atomicity

lemma env_stable_peterson_sr_cs1:
  "env_stable (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
               peterson_sr peterson_sr_cs1 (\<lambda>s. invs s \<and> critical (ab_label s ident))" apply (simp add: env_stable_def rely_stable_def env_rely_stable_iosr_def
                 peterson_rel_def) apply (rule conjI) apply (auto simp: peterson_sr_def peterson_sr_cs1_def)[1] apply (rule conjI) apply clarsimp apply (clarsimp simp: peterson_sr_cs1_invs) apply (auto simp: peterson_sr_cs1_def peterson_sr_def)[1] apply (auto simp: peterson_sr_cs1_def peterson_sr_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) peterson_sr peterson_sr_cs1 (\<lambda>s. invs s \<and> ab_label s ident = Critical) proof (prove)
goal (1 subgoal):
 1. (\<forall>s t t'. invs t \<and> ab_label t ident = Critical \<and> peterson_sr s t \<and> (invs t \<longrightarrow> invs t' \<and> ab_v t' ident = ab_v t ident \<and> ab_label t' ident = ab_label t ident \<and> (t_v t = ident \<longrightarrow> t_v t' = ident) \<and> (ab_label t ident = Critical \<longrightarrow> cs2_v t' = cs2_v t \<and> cs1_v t' = cs1_v t)) \<longrightarrow> (\<exists>s'. peterson_sr s' t')) \<and> (\<forall>s0 t0. invs t0 \<and> ab_label t0 ident = Critical \<longrightarrow> peterson_sr_cs1 s0 t0 \<longrightarrow> (\<forall>s t. invs t \<and> ab_v t ident = ab_v t0 ident \<and> ab_label t ident = Critical \<and> (t_v t0 = ident \<longrightarrow> t_v t = ident) \<and> cs2_v t = cs2_v t0 \<and> cs1_v t = cs1_v t0 \<longrightarrow> (invs s0 \<longrightarrow> invs s \<and> ab_v s ident = ab_v s0 ident \<and> ab_label s ident = ab_label s0 ident \<and> (t_v s0 = ident \<longrightarrow> t_v s = ident) \<and> (ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0)) \<longrightarrow> peterson_sr s t \<longrightarrow> peterson_sr_cs1 s t)) \<and> peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (2 subgoals):
 1. \<forall>s t t'. invs t \<and> ab_label t ident = Critical \<and> peterson_sr s t \<and> (invs t \<longrightarrow> invs t' \<and> ab_v t' ident = ab_v t ident \<and> ab_label t' ident = ab_label t ident \<and> (t_v t = ident \<longrightarrow> t_v t' = ident) \<and> (ab_label t ident = Critical \<longrightarrow> cs2_v t' = cs2_v t \<and> cs1_v t' = cs1_v t)) \<longrightarrow> (\<exists>s'. peterson_sr s' t')
 2. (\<forall>s0 t0. invs t0 \<and> ab_label t0 ident = Critical \<longrightarrow> peterson_sr_cs1 s0 t0 \<longrightarrow> (\<forall>s t. invs t \<and> ab_v t ident = ab_v t0 ident \<and> ab_label t ident = Critical \<and> (t_v t0 = ident \<longrightarrow> t_v t = ident) \<and> cs2_v t = cs2_v t0 \<and> cs1_v t = cs1_v t0 \<longrightarrow> (invs s0 \<longrightarrow> invs s \<and> ab_v s ident = ab_v s0 ident \<and> ab_label s ident = ab_label s0 ident \<and> (t_v s0 = ident \<longrightarrow> t_v s = ident) \<and> (ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0)) \<longrightarrow> peterson_sr s t \<longrightarrow> peterson_sr_cs1 s t)) \<and> peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (1 subgoal):
 1. (\<forall>s0 t0. invs t0 \<and> ab_label t0 ident = Critical \<longrightarrow> peterson_sr_cs1 s0 t0 \<longrightarrow> (\<forall>s t. invs t \<and> ab_v t ident = ab_v t0 ident \<and> ab_label t ident = Critical \<and> (t_v t0 = ident \<longrightarrow> t_v t = ident) \<and> cs2_v t = cs2_v t0 \<and> cs1_v t = cs1_v t0 \<longrightarrow> (invs s0 \<longrightarrow> invs s \<and> ab_v s ident = ab_v s0 ident \<and> ab_label s ident = ab_label s0 ident \<and> (t_v s0 = ident \<longrightarrow> t_v s = ident) \<and> (ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0)) \<longrightarrow> peterson_sr s t \<longrightarrow> peterson_sr_cs1 s t)) \<and> peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (2 subgoals):
 1. \<forall>s0 t0. invs t0 \<and> ab_label t0 ident = Critical \<longrightarrow> peterson_sr_cs1 s0 t0 \<longrightarrow> (\<forall>s t. invs t \<and> ab_v t ident = ab_v t0 ident \<and> ab_label t ident = Critical \<and> (t_v t0 = ident \<longrightarrow> t_v t = ident) \<and> cs2_v t = cs2_v t0 \<and> cs1_v t = cs1_v t0 \<longrightarrow> (invs s0 \<longrightarrow> invs s \<and> ab_v s ident = ab_v s0 ident \<and> ab_label s ident = ab_label s0 ident \<and> (t_v s0 = ident \<longrightarrow> t_v s = ident) \<and> (ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0)) \<longrightarrow> peterson_sr s t \<longrightarrow> peterson_sr_cs1 s t)
 2. peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (2 subgoals):
 1. \<And>s0 t0 s t. \<lbrakk>invs t0; ab_label t0 ident = Critical; peterson_sr_cs1 s0 t0; invs t; ab_v t ident = ab_v t0 ident; ab_label t ident = Critical; t_v t0 = ident \<longrightarrow> t_v t = ident; cs2_v t = cs2_v t0; cs1_v t = cs1_v t0; invs s0 \<longrightarrow> invs s \<and> ab_v s ident = ab_v s0 ident \<and> ab_label s ident = ab_label s0 ident \<and> (t_v s0 = ident \<longrightarrow> t_v s = ident) \<and> (ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0); peterson_sr s t\<rbrakk> \<Longrightarrow> peterson_sr_cs1 s t
 2. peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (2 subgoals):
 1. \<And>s0 t0 s t. \<lbrakk>invs t0; ab_label t0 ident = Critical; peterson_sr_cs1 s0 t0; invs t; ab_v t ident = ab_v t0 ident; ab_label t ident = Critical; t_v t0 = ident \<longrightarrow> t_v t = ident; cs2_v t = cs2_v t0; cs1_v t = cs1_v t0; peterson_sr s t; invs s; ab_v s ident = ab_v s0 ident; ab_label s ident = ab_label s0 ident; t_v s0 = ident \<longrightarrow> t_v s = ident; ab_label s0 ident = Critical \<longrightarrow> cs2_v s = cs2_v s0 \<and> cs1_v s = cs1_v s0\<rbrakk> \<Longrightarrow> peterson_sr_cs1 s t
 2. peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal (1 subgoal):
 1. peterson_sr_cs1 \<le> peterson_sr proof (prove)
goal:
No subgoals!