theory Schedule_DR

lemma schedule_resume_cur_thread_dcorres:
         "\<And>cur cur_ts. dcorres dc \<top> (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = resume_cur_thread)
        Schedule_D.schedule
       (do idle_t \<leftarrow> gets idle_thread;
           assert (runnable cur_ts \<or> cur = idle_t)
         od)" apply (rule stronger_corres_guard_imp) apply (rule schedule_resume_cur_thread_dcorres_L) apply (case_tac "cur \<noteq> idle_thread s'") apply (clarsimp simp: valid_sched_def valid_sched_action_def is_activatable_def invs_def valid_state_def
                          pred_tcb_at_def obj_at_def ct_in_cur_domain_def in_cur_domain_def) apply (frule(1) valid_etcbs_tcb_etcb) apply (auto simp: transform_def transform_current_thread_def all_active_tcbs_def transform_objects_def active_tcbs_in_domain_def etcb_at_def tcb_boundntfn_slot_def tcb_pending_op_slot_def
                          map_add_def restrict_map_def option_map_def transform_object_def transform_tcb_def valid_idle_def st_tcb_def2 get_tcb_def
                          transform_cnode_contents_def infer_tcb_pending_op_def transform_cap_def domIff st_tcb_at_kh_def obj_at_def only_idle_def
                    split: option.splits if_split Structures_A.kernel_object.splits Structures_A.thread_state.splits)[1] 
     (* cur = idle_thread s' *)
    apply (subgoal_tac "cdl_current_thread s = None") apply (clarsimp simp: transform_def transform_current_thread_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cur cur_ts. dcorres dc (\<lambda>_. True) (\<lambda>s. cur = cur_thread s \<and> st_tcb_at ((=) cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = resume_cur_thread) Schedule_D.schedule (do idle_t <- gets idle_thread;
assert (runnable cur_ts \<or> cur = idle_t)
od) proof (prove)
goal (3 subgoals):
 1. \<And>cur cur_ts. dcorres dc (?Q cur cur_ts) (?Q' cur cur_ts) Schedule_D.schedule (do idle_t <- gets idle_thread;
assert (runnable cur_ts \<or> cur = idle_t)
od)
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q cur cur_ts s
 3. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ?Q' cur cur_ts s' proof (prove)
goal (2 subgoals):
 1. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 3. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb y. \<lbrakk>cur_thread s' \<noteq> idle_thread s'; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') resume_cur_thread (cur_thread s'); valid_blocked_2 (ready_queues s') (kheap s') resume_cur_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = resume_cur_thread; cdl_current_thread (transform s') = Some y; kheap s' (cur_thread s') = Some (TCB tcb); activatable (tcb_state tcb); etcb_at (\<lambda>t. tcb_domain t = cur_domain s') (cur_thread s') s'\<rbrakk> \<Longrightarrow> (\<exists>d. transform s' = transform s'\<lparr>cdl_current_domain := d\<rparr>) \<and> y \<in> active_tcbs_in_domain (cdl_current_domain (transform s')) (transform s')
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 3. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>s' tcb y. \<lbrakk>cur_thread s' \<noteq> idle_thread s'; valid_etcbs s'; valid_queues s'; ct_not_in_q_2 (ready_queues s') resume_cur_thread (cur_thread s'); valid_blocked_2 (ready_queues s') (kheap s') resume_cur_thread (cur_thread s'); valid_idle_etcb s'; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; scheduler_action s' = resume_cur_thread; cdl_current_thread (transform s') = Some y; kheap s' (cur_thread s') = Some (TCB tcb); activatable (tcb_state tcb); etcb_at (\<lambda>t. tcb_domain t = cur_domain s') (cur_thread s') s'; \<exists>etcb. ekheap s' (cur_thread s') = Some etcb\<rbrakk> \<Longrightarrow> (\<exists>d. transform s' = transform s'\<lparr>cdl_current_domain := d\<rparr>) \<and> y \<in> active_tcbs_in_domain (cdl_current_domain (transform s')) (transform s')
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 3. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'; cdl_current_thread s = None\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<exists>t tcb. cdl_current_thread s = Some t \<and> (\<exists>d. s = s\<lparr>cdl_current_domain := d\<rparr>) \<and> t \<in> active_tcbs_in_domain (cdl_current_domain s) s) or (\<lambda>s. cdl_current_thread s = None)) s
 2. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; \<not> cur \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> cdl_current_thread s = None
 3. \<And>cur cur_ts s s'. \<lbrakk>True; cur = cur_thread s' \<and> st_tcb_at ((=) cur_ts) cur s' \<and> valid_etcbs s' \<and> valid_sched s' \<and> invs s' \<and> scheduler_action s' = resume_cur_thread; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!