theory Peterson_Atomicity

lemma validI_repeat_interference:
  "\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
   \<Longrightarrow> \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s
   \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> do repeat f; interference od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>" apply (rule bind_twp) apply simp apply (rule interference_twp) apply (rule rg_strengthen_post) apply (rule repeat_validI, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> do repeat f;
interference
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>?Q' r\<rbrace>, \<lbrace>R\<rbrace> K_bind interference r \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>, \<lbrace>?Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>?Q' ()\<rbrace>, \<lbrace>R\<rbrace> interference \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>, \<lbrace>?Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>a b c. (\<forall>s'. R\<^sup>*\<^sup>* c s' \<longrightarrow> Q a s' s') \<and> G b c\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>, \<lbrace>?Q'4\<rbrace>
 2. \<And>v s0 s. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s; ?Q'4 v s0 s\<rbrakk> \<Longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q v s' s') \<and> G s0 s proof (prove)
goal (1 subgoal):
 1. \<And>v s0 s. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s; P s0 s\<rbrakk> \<Longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q v s' s') \<and> G s0 s proof (prove)
goal:
No subgoals!