theory Peterson_Atomicity

theorem peterson_proc_system_mutual_excl:
  "\<lbrace> \<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<rbrace>,
   \<lbrace> \<lambda>s0 s. s0 = s \<rbrace>
     peterson_proc_system
   \<lbrace> \<lambda>s0 s. invs s0 \<longrightarrow> invs s \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. invs s \<rbrace>" apply (rule prefix_refinement_validI') apply (rule peterson_proc_system_refinement) apply (rule abs_peterson_proc_system_mutual_excl) apply clarsimp apply (clarsimp simp: peterson_sr_invs_sym ) apply (fastforce simp: peterson_rel_def peterson_sr_def) apply clarsimp apply (fastforce simp: peterson_sr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)\<rbrace>, \<lbrace>(=)\<rbrace> peterson_proc_system \<lbrace>\<lambda>s0 s. invs s0 \<longrightarrow> invs s\<rbrace>, \<lbrace>\<lambda>rv s0. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. prefix_refinement ?sr ?isr ?osr ?rvr ?prP' ?prP ?R' (=) ?f peterson_proc_system
 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> invs cs
 4. \<And>s0 s. ?G' s0 s \<Longrightarrow> \<forall>cs0 cs. ?sr s0 cs0 \<and> ?sr s cs \<longrightarrow> invs cs0 \<longrightarrow> invs cs
 5. \<forall>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. 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> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> ?sr s t)
 7. prefix_closed peterson_proc_system proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>(=)\<rbrace> abs_peterson_proc_system \<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> invs cs
 3. \<And>s0 s. ?G' s0 s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> invs cs0 \<longrightarrow> invs cs
 4. \<forall>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 5. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> peterson_sr s t)
 6. prefix_closed peterson_proc_system proof (prove)
goal (5 subgoals):
 1. \<And>v s0 s. invs s \<Longrightarrow> \<forall>rv' cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<and> True \<longrightarrow> invs cs
 2. \<And>s0 s. invs s0 \<longrightarrow> invs s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> invs cs0 \<longrightarrow> invs cs
 3. \<forall>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> (\<exists>s0 s. (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 4. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> peterson_sr s t)
 5. prefix_closed peterson_proc_system proof (prove)
goal (4 subgoals):
 1. \<And>s0 s. invs s0 \<longrightarrow> invs s \<Longrightarrow> \<forall>cs0 cs. peterson_sr s0 cs0 \<and> peterson_sr s cs \<longrightarrow> invs cs0 \<longrightarrow> invs cs
 2. \<forall>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> (\<exists>s0 s. (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 3. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> peterson_sr s t)
 4. prefix_closed peterson_proc_system proof (prove)
goal (3 subgoals):
 1. \<forall>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited) \<longrightarrow> (\<exists>s0 s. (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited)) \<and> (t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited)) \<and> peterson_sr s t \<and> peterson_sr s0 t0)
 2. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> peterson_sr s t)
 3. prefix_closed peterson_proc_system proof (prove)
goal (2 subgoals):
 1. \<forall>s0 t0 t. peterson_sr s0 t0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> peterson_sr s t)
 2. prefix_closed peterson_proc_system proof (prove)
goal (1 subgoal):
 1. prefix_closed peterson_proc_system proof (prove)
goal:
No subgoals!