theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_valid_blocked':
  "\<lbrace>valid_blocked and ct_in_q\<rbrace>
    tcb_sched_action tcb_sched_dequeue thread
  \<lbrace>\<lambda>_ s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: etcb_at_def tcb_sched_dequeue_def not_queued_def valid_blocked_def split: option.splits) apply (case_tac "t = cur_thread s") apply (simp add: ct_in_q_def) apply clarsimp apply (rule ccontr) apply clarsimp apply (erule impE) apply (case_tac st, (force simp: st_tcb_at_def obj_at_def)+)[1] apply force apply (erule_tac x=t in allE) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_ s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_blocked_2 (ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (kheap (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (scheduler_action (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread) thread s) thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t = cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); t = cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); \<not> (st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); active st\<rbrakk> \<Longrightarrow> False
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (3 subgoals):
 1. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); active st\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) s
 2. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); active st; \<exists>d p. cur_thread s \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False
 3. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>s x2 st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> cur_thread s \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> cur_thread s \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) (cur_thread s) s; cur_thread s \<noteq> thread; scheduler_action s \<noteq> switch_thread (cur_thread s); active st; \<exists>d p. cur_thread s \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>\<forall>t. (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>ct_in_q s; ekheap s thread = Some x2; \<forall>d p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> t \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> t \<notin> set (ready_queues s d p)); st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; t \<noteq> cur_thread s; (\<forall>d p. t \<notin> set (ready_queues s d p)) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!