theory Finalise_R

lemma cancelAllIPC_mapM_x_valid_queues:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)\<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (rule_tac R="\<lambda>_ s. (\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s"
               in hoare_post_add) apply (rule hoare_pre) apply (rule mapM_x_wp') apply (rule hoare_name_pre_state) apply (wp hoare_vcg_const_Ball_lift
            tcbSchedEnqueue_valid_queues tcbSchedEnqueue_not_st
            sts_valid_queues sts_st_tcb_at'_cases setThreadState_not_st
       | simp
       | ((elim conjE)?, drule (1) bspec, clarsimp elim!: obj_at'_weakenE simp: valid_tcb_state'_def))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>r s. ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>r s. ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set q \<Longrightarrow> \<lbrace>\<lambda>s. ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r s. ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)) s \<Longrightarrow> ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set q; ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>r s. ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)) s \<Longrightarrow> ((\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s) \<and> Invariants_H.valid_queues s proof (prove)
goal:
No subgoals!