theory IpcCancel_R

lemma cancelAll_unlive_helper:
  "\<lbrace>\<lambda>s. (\<forall>x\<in>set xs. tcb_at' x s) \<and>
     ko_wp_at' (\<lambda>x. \<not> live' x \<and> (projectKO_opt x = (None :: tcb option))) p s\<rbrace>
     mapM_x (\<lambda>t. do
                   y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                   tcbSchedEnqueue t
                 od) xs
   \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace>" apply (rule hoare_strengthen_post) apply (rule mapM_x_wp') apply (rule hoare_pre) apply (wp tcbSchedEnqueue_unlive hoare_vcg_const_Ball_lift) apply clarsimp apply (clarsimp elim!: ko_wp_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) xs \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) xs \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> ko_wp_at' (Not \<circ> live') p s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrace>
 2. \<And>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s \<Longrightarrow> ko_wp_at' (Not \<circ> live') p s proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>?Q5 x\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrace>
 2. \<And>x s. \<lbrakk>x \<in> set xs; (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrakk> \<Longrightarrow> ?Q5 x s
 3. \<And>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s \<Longrightarrow> ko_wp_at' (Not \<circ> live') p s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set xs; (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s \<and> tcb_at' x s
 2. \<And>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s \<Longrightarrow> ko_wp_at' (Not \<circ> live') p s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (\<forall>x\<in>set xs. tcb_at' x s) \<and> ko_wp_at' (\<lambda>x. \<not> live' x \<and> projectKO_opt x = None) p s \<Longrightarrow> ko_wp_at' (Not \<circ> live') p s proof (prove)
goal:
No subgoals!