theory DetSchedSchedule_AI

lemma restart_valid_sched[wp]:
  "\<lbrace>valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> restart thread \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: restart_def | wp set_thread_state_runnable_valid_queues
                                    set_thread_state_runnable_valid_sched_action
                                    set_thread_state_valid_blocked_except
                                    sts_st_tcb_at' cancel_ipc_simple2
                                    possible_switch_to_valid_sched)+ apply (rule_tac Q="\<lambda>_. valid_sched and not_cur_thread thread and (\<lambda>s. thread \<noteq> idle_thread s)" in hoare_strengthen_post) apply wp apply (simp add: valid_sched_def) apply (simp add: if_fun_split) apply (rule hoare_vcg_conj_lift) apply (simp add: get_thread_state_def thread_get_def) apply wp apply (simp add: get_thread_state_def | wp hoare_drop_imps)+ apply (clarsimp simp: not_cur_thread_def valid_sched_def valid_sched_action_def
                        is_activatable_def) apply (drule_tac test="\<lambda>ts. \<not> activatable ts" in st_tcb_at_get_lift) apply simp apply (simp only: st_tcb_at_not) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace> restart thread \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?P'80 state\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> not_cur_thread thread s \<and> valid_blocked s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>?Q\<rbrace> get_thread_state thread \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. valid_etcbs s \<and> ?P'80 state s else valid_sched\<rbrace>
 3. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?P'80 state\<rbrace> cancel_ipc thread \<lbrace>\<lambda>_. valid_sched and not_cur_thread thread and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
 2. \<And>state rv s. \<lbrakk>\<not> runnable state \<and> state \<noteq> IdleThreadState; (valid_sched and not_cur_thread thread and (\<lambda>s. thread \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> not_cur_thread thread s \<and> valid_blocked s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s
 3. \<lbrace>?Q\<rbrace> get_thread_state thread \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. valid_etcbs s \<and> ?P'80 state s else valid_sched\<rbrace>
 4. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>state rv s. \<lbrakk>\<not> runnable state \<and> state \<noteq> IdleThreadState; (valid_sched and not_cur_thread thread and (\<lambda>s. thread \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_idle_etcb s \<and> not_cur_thread thread s \<and> valid_blocked s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s
 2. \<lbrace>?Q\<rbrace> get_thread_state thread \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. valid_etcbs s \<and> valid_sched s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s else valid_sched\<rbrace>
 3. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state thread \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. valid_etcbs s \<and> valid_sched s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s else valid_sched\<rbrace>
 2. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state thread \<lbrace>\<lambda>state x. (\<not> runnable state \<and> state \<noteq> IdleThreadState \<longrightarrow> valid_etcbs x \<and> valid_sched x \<and> not_cur_thread thread x \<and> thread \<noteq> idle_thread x) \<and> (runnable state \<longrightarrow> valid_sched x) \<and> (idle state \<longrightarrow> valid_sched x)\<rbrace>
 2. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P93\<rbrace> get_thread_state thread \<lbrace>\<lambda>rv s. \<not> runnable rv \<and> rv \<noteq> IdleThreadState \<longrightarrow> valid_etcbs s \<and> valid_sched s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>?P'93\<rbrace> get_thread_state thread \<lbrace>\<lambda>rv s. (runnable rv \<longrightarrow> valid_sched s) \<and> (idle rv \<longrightarrow> valid_sched s)\<rbrace>
 3. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?P93 s \<and> ?P'93 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P93\<rbrace> do tcb <- gets_the (get_tcb thread);
return (tcb_state tcb)
od \<lbrace>\<lambda>rv s. \<not> runnable rv \<and> rv \<noteq> IdleThreadState \<longrightarrow> valid_etcbs s \<and> valid_sched s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>?P'93\<rbrace> get_thread_state thread \<lbrace>\<lambda>rv s. (runnable rv \<longrightarrow> valid_sched s) \<and> (idle rv \<longrightarrow> valid_sched s)\<rbrace>
 3. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> ?P93 s \<and> ?P'93 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'93\<rbrace> get_thread_state thread \<lbrace>\<lambda>rv s. (runnable rv \<longrightarrow> valid_sched s) \<and> (idle rv \<longrightarrow> valid_sched s)\<rbrace>
 2. \<And>s. (valid_sched and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> (get_tcb thread s \<noteq> None \<longrightarrow> \<not> runnable (tcb_state (the (get_tcb thread s))) \<and> tcb_state (the (get_tcb thread s)) \<noteq> IdleThreadState \<longrightarrow> valid_etcbs s \<and> valid_sched s \<and> not_cur_thread thread s \<and> thread \<noteq> idle_thread s) \<and> ?P'93 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<and> thread \<noteq> idle_thread s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> \<not> runnable (tcb_state (the (get_tcb thread s))) \<and> tcb_state (the (get_tcb thread s)) \<noteq> IdleThreadState \<longrightarrow> valid_etcbs s \<and> not_cur_thread thread s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; cur_thread s \<noteq> idle_thread s; get_tcb (cur_thread s) s = Some y; \<not> runnable (tcb_state y); tcb_state y \<noteq> IdleThreadState; scheduler_action s = resume_cur_thread; thread = cur_thread s; st_tcb_at activatable (cur_thread s) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; cur_thread s \<noteq> idle_thread s; \<not> runnable (tcb_state y); tcb_state y \<noteq> IdleThreadState; scheduler_action s = resume_cur_thread; thread = cur_thread s; st_tcb_at activatable (cur_thread s) s\<rbrakk> \<Longrightarrow> \<not> activatable (tcb_state y)
 2. \<And>s y. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; cur_thread s \<noteq> idle_thread s; \<not> runnable (tcb_state y); tcb_state y \<noteq> IdleThreadState; scheduler_action s = resume_cur_thread; thread = cur_thread s; st_tcb_at activatable (cur_thread s) s; st_tcb_at (\<lambda>ts. \<not> activatable ts) (cur_thread s) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; cur_thread s \<noteq> idle_thread s; \<not> runnable (tcb_state y); tcb_state y \<noteq> IdleThreadState; scheduler_action s = resume_cur_thread; thread = cur_thread s; st_tcb_at activatable (cur_thread s) s; st_tcb_at (\<lambda>ts. \<not> activatable ts) (cur_thread s) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>valid_etcbs s; valid_queues s; ct_not_in_q_2 (ready_queues s) resume_cur_thread (cur_thread s); ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s); valid_blocked_2 (ready_queues s) (kheap s) resume_cur_thread (cur_thread s); valid_idle_etcb s; cur_thread s \<noteq> idle_thread s; \<not> runnable (tcb_state y); tcb_state y \<noteq> IdleThreadState; scheduler_action s = resume_cur_thread; thread = cur_thread s; st_tcb_at activatable (cur_thread s) s; \<not> True \<and> tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!