theory Schedule_DR

lemma idle_thread_not_in_queue:
  "\<lbrakk> valid_idle s; DetSchedInvs_AI.valid_queues s; ready_queues s d p \<noteq> [] \<rbrakk> \<Longrightarrow> idle_thread s \<noteq> hd (ready_queues s d p)" apply (clarsimp simp: valid_idle_def DetSchedInvs_AI.valid_queues_def pred_tcb_at_def obj_at_def) apply (erule_tac x="d" in allE) apply (erule_tac x="p" in allE) apply clarsimp apply (erule_tac x="idle_thread s" in ballE) apply clarsimp apply (frule hd_in_set) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_queues s; ready_queues s d p \<noteq> []\<rbrakk> \<Longrightarrow> idle_thread s \<noteq> hd (ready_queues s d p) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s d p); ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); \<forall>p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); \<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb))); distinct (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); distinct (ready_queues s d p); is_etcb_at (idle_thread s) s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) (idle_thread s) s \<and> (\<exists>ko. kheap s (idle_thread s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))\<rbrakk> \<Longrightarrow> False
 2. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); distinct (ready_queues s d p); idle_thread s \<notin> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); distinct (ready_queues s d p); idle_thread s \<notin> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ready_queues s d p \<noteq> []; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); idle_thread_ptr = hd (ready_queues s d p); distinct (ready_queues s d p); idle_thread s \<notin> set (ready_queues s d p); hd (ready_queues s d p) \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!