theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_valid_blocked_except:
  "\<lbrace>valid_blocked\<rbrace>
     tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>_. valid_blocked_except thread\<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 valid_blocked_except_def split: option.splits) apply (case_tac "t=thread") apply simp apply (erule_tac x=t in allE) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_blocked_except thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_blocked_except thread (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 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); ekheap s thread = Some x2; t \<noteq> thread; \<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> cur_thread s; 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); ekheap s thread = Some x2; t \<noteq> thread; \<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> cur_thread s; scheduler_action s \<noteq> switch_thread t; t = thread\<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); ekheap s thread = Some x2; t \<noteq> thread; \<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> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<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); ekheap s thread = Some x2; t \<noteq> thread; \<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> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s x2 t st. \<lbrakk>ekheap s thread = Some x2; t \<noteq> thread; \<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> cur_thread s; scheduler_action s \<noteq> switch_thread t; t \<noteq> thread; (\<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!