theory IpcCancel_R

lemma ep_cancel_corres_helper:
  "corres dc ((\<lambda>s. \<forall>t \<in> set list. tcb_at t s) and valid_etcbs)
             ((\<lambda>s. \<forall>t \<in> set list. tcb_at' t s)
                    and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
                    and Invariants_H.valid_queues and valid_queues' and valid_objs')
          (mapM_x (\<lambda>t. do
                        y \<leftarrow> set_thread_state t Structures_A.Restart;
                        tcb_sched_action tcb_sched_enqueue t
                     od) list)
          (mapM_x (\<lambda>t. do
                        y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                        tcbSchedEnqueue t
                     od) list)" apply (rule_tac S="{t. (fst t = snd t) \<and> fst t \<in> set list}"
                     in corres_mapM_x) apply clarsimp apply (rule corres_guard_imp) apply (subst bind_return_unit, rule corres_split[OF _ tcbSchedEnqueue_corres]) apply simp apply (rule corres_guard_imp [OF setThreadState_corres]) apply simp apply (simp add: valid_tcb_state_def) apply simp apply (wp sts_valid_queues)+ apply (force simp: tcb_at_is_etcb_at) apply (fastforce elim: obj_at'_weakenE) apply ((wp hoare_vcg_const_Ball_lift | simp)+)[1] apply (rule hoare_pre) apply (wp hoare_vcg_const_Ball_lift
               weak_sch_act_wf_lift_linear sts_st_tcb' setThreadState_not_st
               sts_valid_queues tcbSchedEnqueue_not_st
          | simp)+ apply (auto elim: obj_at'_weakenE simp: valid_tcb_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') (mapM_x (\<lambda>t. do y <- set_thread_state t Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue t
od) list) (mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) list) proof (prove)
goal (5 subgoals):
 1. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> corres dc ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') (do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od) (do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od)
 2. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 3. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 4. length list = length list
 5. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> corres dc ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') (do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od) (do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od)
 2. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 3. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 4. length list = length list
 5. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (7 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> corres dc (?Q4 x) (?Q'4 x) (do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od) (do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od)
 2. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q4 x s
 3. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> ?Q'4 x s
 4. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 5. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 6. length list = length list
 7. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (9 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> corres (?r'11 x) (?P25 x x) (?P'23 x x) (do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od) (setThreadState Structures_H.thread_state.Restart x)
 2. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 3. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 4. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P25 x x and ?Q24 x x) s
 5. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (?P'23 x x and ?Q'22 x x) s
 6. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 7. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 8. length list = length list
 9. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (9 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> corres (?r'11 x) (?P25 x x) (?P'23 x x) (set_thread_state x Structures_A.thread_state.Restart) (setThreadState Structures_H.thread_state.Restart x)
 2. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 3. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 4. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P25 x x and ?Q24 x x) s
 5. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (?P'23 x x and ?Q'22 x x) s
 6. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 7. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 8. length list = length list
 9. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (11 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> thread_state_relation Structures_A.thread_state.Restart Structures_H.thread_state.Restart
 2. \<And>x s. \<lbrakk>x \<in> set list; ?P25 x x s\<rbrakk> \<Longrightarrow> tcb_at x s
 3. \<And>x s. \<lbrakk>x \<in> set list; ?P'23 x x s\<rbrakk> \<Longrightarrow> tcb_at' x s
 4. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 5. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 6. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P25 x x and ?Q24 x x) s
 7. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (?P'23 x x and ?Q'22 x x) s
 8. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 9. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 10. length list = length list
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set list; ?P25 x x s\<rbrakk> \<Longrightarrow> tcb_at x s
 2. \<And>x s. \<lbrakk>x \<in> set list; ?P'23 x x s\<rbrakk> \<Longrightarrow> tcb_at' x s
 3. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 4. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 5. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P25 x x and ?Q24 x x) s
 6. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (?P'23 x x and ?Q'22 x x) s
 7. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 8. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 9. length list = length list
 10. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (9 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set list; ?P'23 x x s\<rbrakk> \<Longrightarrow> tcb_at' x s
 2. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 3. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 4. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at x and ?Q24 x x) s
 5. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (?P'23 x x and ?Q'22 x x) s
 6. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 7. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 8. length list = length list
 9. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (8 subgoals):
 1. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q24 x x\<rbrace> do x <- set_thread_state x Structures_A.thread_state.Restart;
return ()
od \<lbrace>\<lambda>y. is_etcb_at x\<rbrace>
 2. \<And>x. x \<in> set list \<Longrightarrow> \<lbrace>?Q'22 x x\<rbrace> setThreadState Structures_H.thread_state.Restart x \<lbrace>\<lambda>y. tcb_at' x and Invariants_H.valid_queues and valid_queues'\<rbrace>
 3. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at x and ?Q24 x x) s
 4. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (tcb_at' x and ?Q'22 x x) s
 5. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 6. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 7. length list = length list
 8. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (6 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at x and is_etcb_at x) s
 2. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (tcb_at' x and (\<lambda>a. tcb_at' x a \<and> (Invariants_H.valid_queues a \<and> ((\<exists>p. x \<in> set (ksReadyQueues a p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> valid_queues' a)) s
 3. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 4. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 5. length list = length list
 6. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (5 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set list; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> (tcb_at' x and (\<lambda>a. tcb_at' x a \<and> (Invariants_H.valid_queues a \<and> ((\<exists>p. x \<in> set (ksReadyQueues a p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> valid_queues' a)) s
 2. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 3. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 4. length list = length list
 5. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (4 subgoals):
 1. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace> do y <- set_thread_state x Structures_A.thread_state.Restart;
tcb_sched_action tcb_sched_enqueue x
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at t s) and valid_etcbs\<rbrace>
 2. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 3. length list = length list
 4. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (3 subgoals):
 1. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>(\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 2. length list = length list
 3. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (4 subgoals):
 1. \<And>x y. (x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list} \<Longrightarrow> \<lbrace>?Q83 x y\<rbrace> do ya <- setThreadState Structures_H.thread_state.Restart y;
tcbSchedEnqueue y
od \<lbrace>\<lambda>rv. (\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs'\<rbrace>
 2. \<And>x y s. \<lbrakk>(x, y) \<in> {t. fst t = snd t \<and> fst t \<in> set list}; ((\<lambda>s. \<forall>t\<in>set list. tcb_at' t s) and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_queues' and valid_objs') s\<rbrakk> \<Longrightarrow> ?Q83 x y s
 3. length list = length list
 4. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>x \<in> set list; (\<forall>t\<in>set list. tcb_at' t s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> valid_tcb_state' Structures_H.thread_state.Restart s
 2. length list = length list
 3. set (zip list list) \<subseteq> {t. fst t = snd t \<and> fst t \<in> set list} proof (prove)
goal:
No subgoals!