theory DetSchedSchedule_AI

lemma ct_in_q_valid_blocked_ct_upd:
  "\<lbrakk>ct_in_q s; valid_blocked s\<rbrakk> \<Longrightarrow> valid_blocked (s\<lparr>cur_thread := thread\<rparr>)" apply (clarsimp simp: valid_blocked_def ct_in_q_def) apply (erule_tac x=t in allE) apply clarsimp apply (case_tac "t=cur_thread s") apply (simp add: not_queued_def) apply (case_tac st, (force simp: st_tcb_at_def obj_at_def)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_in_q s; valid_blocked s\<rbrakk> \<Longrightarrow> valid_blocked (s\<lparr>cur_thread := thread\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); \<forall>t. not_queued t s \<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); not_queued t s; 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 (1 subgoal):
 1. \<And>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); not_queued t s; st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; not_queued t s \<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 (1 subgoal):
 1. \<And>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); not_queued t s; st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); not_queued t s; st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart; t = cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart
 2. \<And>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); not_queued t s; st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (2 subgoals):
 1. \<And>t st. \<lbrakk>\<not> st_tcb_at runnable (cur_thread s) s; \<forall>d p. 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>t st. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); not_queued t s; st_tcb_at ((=) st) t s; t \<noteq> thread; scheduler_action s \<noteq> switch_thread t; \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart; t \<noteq> cur_thread s\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!