theory Peterson_Atomicity

lemma peterson_proc_mutual_excl_helper:
  "\<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>
     peterson_proc ident
   \<lbrace> peterson_rel3 ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel3 ident s0 s \<and> invs s
               \<and> ab_label s ident = Exited \<rbrace>" apply (rule prefix_refinement_validI') apply (rule peterson_proc_refinement) apply (rule abs_peterson_proc_mutual_excl) apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label) apply (clarsimp simp: peterson_sr_peterson_rel3) apply clarsimp apply (rule_tac x=t0 in exI) apply (rule_tac x="t \<lparr>cs1_v := cs1_v t0\<rparr>" in exI) apply (clarsimp simp: peterson_rel_def peterson_sr_def) apply clarsimp apply (rule_tac x="t \<lparr>cs1_v := cs1_v s0\<rparr>" in exI) apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs) apply clarsimp done

(* 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> peterson_proc ident \<lbrace>peterson_rel3 ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel3 ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal (7 subgoals):
 1. prefix_refinement ?sr ?isr ?osr ?rvr ?prP' ?prP ?R' (peterson_rel (other_ident ident)) ?f (peterson_proc ident)
 2. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> ?f \<lbrace>?G'\<rbrace>, \<lbrace>?Q'\<rbrace>
 3. \<And>v s0 s. ?Q' v s0 s \<Longrightarrow> \<forall>rv' cs0 cs. ?sr s0 cs0 \<and> ?osr s cs \<and> ?rvr v rv' \<longrightarrow> peterson_rel3 ident cs0 cs \<and> invs cs \<and> ab_label cs ident = Exited
 4. \<And>s0 s. ?G' s0 s \<Longrightarrow> \<forall>cs0 cs. ?sr s0 cs0 \<and> ?sr s cs \<longrightarrow> peterson_rel3 ident cs0 cs
 5. \<forall>t0 t. peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> ?prP' s0 s \<and> ?prP t0 t \<and> ?isr s t \<and> ?sr s0 t0)
 6. \<forall>s0 t0 t. ?sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> ?sr s t)
 7. prefix_closed (peterson_proc ident) proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_peterson_proc ident \<lbrace>?G'\<rbrace>, \<lbrace>?Q'\<rbrace>
 2. \<And>v s0 s. ?Q' v s0 s \<Longrightarrow> \<forall>rv' cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<and> True \<longrightarrow> peterson_rel3 ident cs0 cs \<and> invs cs \<and> ab_label cs ident = Exited
 3. \<And>s0 s. ?G' s0 s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> peterson_rel3 ident cs0 cs
 4. \<forall>t0 t. peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> (invs s \<and> ab_label s ident = Exited) \<and> (invs t \<and> ab_label t ident = Exited) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 5. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 6. prefix_closed (peterson_proc ident) proof (prove)
goal (5 subgoals):
 1. \<And>v s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<Longrightarrow> \<forall>rv' cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<and> True \<longrightarrow> peterson_rel3 ident cs0 cs \<and> invs cs \<and> ab_label cs ident = Exited
 2. \<And>s0 s. peterson_rel ident s0 s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> peterson_rel3 ident cs0 cs
 3. \<forall>t0 t. peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (\<exists>s0 s. (peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> (invs s \<and> ab_label s ident = Exited) \<and> (invs t \<and> ab_label t ident = Exited) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 4. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 5. prefix_closed (peterson_proc ident) proof (prove)
goal (4 subgoals):
 1. \<And>s0 s. peterson_rel ident s0 s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> peterson_rel3 ident cs0 cs
 2. \<forall>t0 t. peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (\<exists>s0 s. (peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> (invs s \<and> ab_label s ident = Exited) \<and> (invs t \<and> ab_label t ident = Exited) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 3. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 4. prefix_closed (peterson_proc ident) proof (prove)
goal (3 subgoals):
 1. \<forall>t0 t. peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (\<exists>s0 s. (peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> (invs s \<and> ab_label s ident = Exited) \<and> (invs t \<and> ab_label t ident = Exited) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 2. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 3. prefix_closed (peterson_proc ident) proof (prove)
goal (3 subgoals):
 1. \<And>t0 t. \<lbrakk>peterson_rel ident t0 t; invs t; ab_label t ident = Exited\<rbrakk> \<Longrightarrow> \<exists>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<and> invs s \<and> ab_label s ident = Exited \<and> peterson_sr s t \<and> peterson_sr s0 t0
 2. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 3. prefix_closed (peterson_proc ident) proof (prove)
goal (3 subgoals):
 1. \<And>t0 t. \<lbrakk>peterson_rel ident t0 t; invs t; ab_label t ident = Exited\<rbrakk> \<Longrightarrow> \<exists>s. peterson_rel ident t0 s \<and> invs s \<and> ab_label s ident = Exited \<and> invs s \<and> ab_label s ident = Exited \<and> peterson_sr s t \<and> peterson_sr t0 t0
 2. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 3. prefix_closed (peterson_proc ident) proof (prove)
goal (3 subgoals):
 1. \<And>t0 t. \<lbrakk>peterson_rel ident t0 t; invs t; ab_label t ident = Exited\<rbrakk> \<Longrightarrow> peterson_rel ident t0 (t\<lparr>cs1_v := cs1_v t0\<rparr>) \<and> invs (t\<lparr>cs1_v := cs1_v t0\<rparr>) \<and> ab_label (t\<lparr>cs1_v := cs1_v t0\<rparr>) ident = Exited \<and> invs (t\<lparr>cs1_v := cs1_v t0\<rparr>) \<and> ab_label (t\<lparr>cs1_v := cs1_v t0\<rparr>) ident = Exited \<and> peterson_sr (t\<lparr>cs1_v := cs1_v t0\<rparr>) t \<and> peterson_sr t0 t0
 2. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 3. prefix_closed (peterson_proc ident) proof (prove)
goal (2 subgoals):
 1. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> peterson_rel (other_ident ident) t0 t \<longrightarrow> (\<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t)
 2. prefix_closed (peterson_proc ident) proof (prove)
goal (2 subgoals):
 1. \<And>s0 t0 t. \<lbrakk>peterson_sr s0 t0; peterson_rel (other_ident ident) t0 t\<rbrakk> \<Longrightarrow> \<exists>s. peterson_rel (other_ident ident) s0 s \<and> peterson_sr s t
 2. prefix_closed (peterson_proc ident) proof (prove)
goal (2 subgoals):
 1. \<And>s0 t0 t. \<lbrakk>peterson_sr s0 t0; peterson_rel (other_ident ident) t0 t\<rbrakk> \<Longrightarrow> peterson_rel (other_ident ident) s0 (t\<lparr>cs1_v := cs1_v s0\<rparr>) \<and> peterson_sr (t\<lparr>cs1_v := cs1_v s0\<rparr>) t
 2. prefix_closed (peterson_proc ident) proof (prove)
goal (1 subgoal):
 1. prefix_closed (peterson_proc ident) proof (prove)
goal:
No subgoals!