theory DetSchedSchedule_AI

lemma set_thread_state_active_valid_sched:
  "active st \<Longrightarrow>
   \<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace>
     set_thread_state ct st \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def valid_queues_def) apply (wp hoare_vcg_all_lift) apply (rule hoare_lift_Pf [where f="\<lambda>s. ready_queues s", OF _ set_thread_state_ready_queues]) apply (wpsimp wp: hoare_vcg_ball_lift sts_st_tcb_at_cases simp: runnable_eq_active) apply (wp set_thread_state_runnable_valid_sched_action set_thread_state_runnable_valid_blocked) apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def runnable_eq_active) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. active st \<Longrightarrow> \<lbrace>valid_sched and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace> set_thread_state ct st \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. active st \<Longrightarrow> \<lbrace>(\<lambda>s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and ct_active and (\<lambda>s. cur_thread s = ct)\<rbrace> set_thread_state ct st \<lbrace>\<lambda>_ s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d p. active st \<Longrightarrow> \<lbrace>?P11 d p\<rbrace> set_thread_state ct st \<lbrace>\<lambda>rv s. (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)\<rbrace>
 2. active st \<Longrightarrow> \<lbrace>?P'9\<rbrace> set_thread_state ct st \<lbrace>\<lambda>rv s. ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace>
 3. \<And>s. \<lbrakk>active st; ((\<lambda>s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and ct_active and (\<lambda>s. cur_thread s = ct)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (\<forall>x xa. ?P11 x xa s) \<and> ?P'9 s proof (prove)
goal (3 subgoals):
 1. \<And>d p x. active st \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set (x d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (x d p)\<rbrace> set_thread_state ct st \<lbrace>\<lambda>_ a. (\<forall>t\<in>set (x d p). is_etcb_at t a \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t a \<and> st_tcb_at runnable t a) \<and> distinct (x d p)\<rbrace>
 2. active st \<Longrightarrow> \<lbrace>?P'9\<rbrace> set_thread_state ct st \<lbrace>\<lambda>rv s. ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace>
 3. \<And>s. \<lbrakk>active st; ((\<lambda>s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and ct_active and (\<lambda>s. cur_thread s = ct)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (\<forall>x xa. (\<forall>t\<in>set (ready_queues s x xa). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = xa \<and> tcb_domain t = x) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s x xa)) \<and> ?P'9 s proof (prove)
goal (2 subgoals):
 1. active st \<Longrightarrow> \<lbrace>?P'9\<rbrace> set_thread_state ct st \<lbrace>\<lambda>rv s. ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace>
 2. \<And>s. \<lbrakk>active st; ((\<lambda>s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and ct_active and (\<lambda>s. cur_thread s = ct)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (\<forall>x xa. (\<forall>t\<in>set (ready_queues s x xa). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = xa \<and> tcb_domain t = x) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s x xa)) \<and> ?P'9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>active st; ((\<lambda>s. valid_etcbs s \<and> (\<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> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p)) \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s) and ct_active and (\<lambda>s. cur_thread s = ct)) s\<rbrakk> \<Longrightarrow> valid_etcbs s \<and> (\<forall>x xa. (\<forall>t\<in>set (ready_queues s x xa). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = xa \<and> tcb_domain t = x) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s x xa)) \<and> ct_not_in_q s \<and> (valid_sched_action and (\<lambda>s. runnable st)) s \<and> ct_in_cur_domain s \<and> (valid_blocked and st_tcb_at runnable ct and (\<lambda>s. runnable st)) s \<and> valid_idle_etcb s proof (prove)
goal:
No subgoals!