theory Schedule_DR

lemma schedule_switch_thread_helper:
            "\<lbrakk> valid_etcbs s;
               valid_sched s;
               invs s;
               scheduler_action s = switch_thread t
             \<rbrakk>
             \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s)" apply (clarsimp simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_def is_activatable_def invs_def
                        valid_state_def pred_tcb_at_def obj_at_def switch_in_cur_domain_def in_cur_domain_def only_idle_def) apply (frule(1) valid_etcbs_tcb_etcb) apply (clarsimp simp: valid_idle_def pred_tcb_at_def) apply (drule_tac s="idle_thread s" in sym) apply (auto simp: transform_def transform_current_thread_def all_active_tcbs_def transform_objects_def active_tcbs_in_domain_def etcb_at_def
                        map_add_def restrict_map_def option_map_def transform_object_def transform_tcb_def valid_idle_def pred_tcb_at_def get_tcb_def tcb_pending_op_slot_def tcb_boundntfn_slot_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) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s; valid_sched s; invs s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_etcbs s; scheduler_action s = switch_thread t; valid_queues s; valid_pspace s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); valid_mdb s; valid_ioc s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; kheap s t = Some (TCB tcb); valid_idle s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread 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\<rbrakk> \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_etcbs s; scheduler_action s = switch_thread t; valid_queues s; valid_pspace s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); valid_mdb s; valid_ioc s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; kheap s t = Some (TCB tcb); valid_idle s; valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread 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; \<exists>etcb. ekheap s t = Some etcb\<rbrakk> \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb etcb. \<lbrakk>valid_etcbs s; scheduler_action s = switch_thread t; valid_queues s; valid_pspace s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); valid_mdb s; valid_ioc s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; kheap s t = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread_ptr; 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; ekheap s t = Some etcb; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb) \<and> tcb_bound_notification tcb = None \<and> valid_arch_idle (tcb_iarch tcb)) idle_thread_ptr s; idle_thread s = idle_thread_ptr\<rbrakk> \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb etcb. \<lbrakk>valid_etcbs s; scheduler_action s = switch_thread t; valid_queues s; valid_pspace s; ct_not_in_q_2 (ready_queues s) (switch_thread t) (cur_thread s); valid_mdb s; valid_ioc s; etcb_at (\<lambda>t. tcb_domain t = cur_domain s) t s; kheap s t = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread t) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread_ptr; 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; ekheap s t = Some etcb; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb) \<and> tcb_bound_notification tcb = None \<and> valid_arch_idle (tcb_iarch tcb)) idle_thread_ptr s; idle_thread_ptr = idle_thread s\<rbrakk> \<Longrightarrow> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal:
No subgoals!