theory Peterson_Atomicity

lemma peterson_repeat_refinement:
  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
    (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
    (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
    (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
    (do repeat (abs_peterson_proc ident);
        interference
     od)
    (do repeat (peterson_proc ident);
        interference
     od)" apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_repeat[rotated]) apply (rule abs_peterson_proc_mutual_excl[THEN rg_strengthen_guar]) apply simp apply (rule peterson_proc_mutual_excl[THEN rg_strengthen_guar, THEN rg_weaken_pre]) apply simp+ apply (rule peterson_proc_refinement[THEN prefix_refinement_weaken_pre]) apply simp+ apply (rule prefix_refinement_interference_peterson) apply (wpsimp wp: validI_triv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do repeat (abs_peterson_proc ident);
interference
od) (do repeat (peterson_proc ident);
interference
od) proof (prove)
goal (3 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) ?P' ?Q' (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (do repeat (abs_peterson_proc ident);
interference
od) (do repeat (peterson_proc ident);
interference
od)
 2. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ?P' s0 s
 3. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ?Q' t0 t proof (prove)
goal (6 subgoals):
 1. pfx_refn peterson_sr ?rvr4 ?P4 ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (repeat (abs_peterson_proc ident)) (repeat (peterson_proc ident))
 2. \<And>x y. ?rvr4 x y \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> (?P4 and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. \<lbrace>?P4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> abs_peterson_proc ident -, \<lbrace>\<lambda>_. ?P4\<rbrace>
 2. \<lbrace>\<lambda>t0 t. ?Q4 t0 t \<and> (\<exists>s0 s. peterson_sr s0 t0 \<and> peterson_sr s t)\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident -, \<lbrace>\<lambda>_. ?Q4\<rbrace>
 3. pfx_refn peterson_sr (\<lambda>_ _. True) ?P4 ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident)
 4. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 7. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> (?P4 and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>s0 s. peterson_rel ident s0 s \<Longrightarrow> True
 2. \<lbrace>\<lambda>t0 t. ?Q4 t0 t \<and> (\<exists>s0 s. peterson_sr s0 t0 \<and> peterson_sr s t)\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident -, \<lbrace>\<lambda>_. ?Q4\<rbrace>
 3. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident)
 4. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 7. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (7 subgoals):
 1. \<lbrace>\<lambda>t0 t. ?Q4 t0 t \<and> (\<exists>s0 s. peterson_sr s0 t0 \<and> peterson_sr s t)\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident -, \<lbrace>\<lambda>_. ?Q4\<rbrace>
 2. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) ?Q4 (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident)
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 4. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 6. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> (?Q4 and ?Q'4) t0 t proof (prove)
goal (8 subgoals):
 1. \<And>s0 s. peterson_rel ident s0 s \<Longrightarrow> True
 2. \<And>s0 s. (peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> (\<exists>s0a sa. peterson_sr s0a s0 \<and> peterson_sr sa s) \<Longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited
 3. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident)
 4. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 5. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 7. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 8. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?Q'4) t0 t proof (prove)
goal (6 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (abs_peterson_proc ident) (peterson_proc ident)
 2. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 3. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 5. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 6. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?Q'4) t0 t proof (prove)
goal (7 subgoals):
 1. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> invs s \<and> ab_label s ident = Exited
 2. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> invs t \<and> ab_label t ident = Exited
 3. \<And>x y. True \<Longrightarrow> pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 x) (?Q''4 y) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) (K_bind interference x) (K_bind interference y)
 4. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 5. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 6. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 7. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?Q'4) t0 t proof (prove)
goal (5 subgoals):
 1. pfx_refn peterson_sr (\<lambda>_ _. True) (?P''4 ()) (?Q''4 ()) (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) interference interference
 2. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>?P''4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>?Q''4\<rbrace>
 4. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 5. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?Q'4) t0 t proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (abs_peterson_proc ident) -, \<lbrace>\<lambda>a b c. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> repeat (peterson_proc ident) -, \<lbrace>\<lambda>a b c. True\<rbrace>
 3. \<forall>s s0. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?P'4) s0 s
 4. \<forall>s t s0 t0. peterson_sr s t \<longrightarrow> peterson_sr s0 t0 \<longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<longrightarrow> peterson_rel ident t0 t \<and> invs t \<and> ab_label t ident = Exited \<longrightarrow> ((\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited) and ?Q'4) t0 t proof (prove)
goal:
No subgoals!