theory DetSchedSchedule_AI

lemma set_thread_state_sched_act_not_valid_sched_action:
  "\<lbrace>valid_sched_action and scheduler_act_not thread\<rbrace>
     set_thread_state thread ts
   \<lbrace>\<lambda>rv. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def set_thread_state_def) apply (rule hoare_conjI) apply (wp gts_wp | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split
                         scheduler_act_not_def is_activatable_def pred_tcb_at_def
                         obj_at_def) apply (wp gts_wp | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_kh_if_split
                        scheduler_act_not_def is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and scheduler_act_not thread\<rbrace> set_thread_state thread ts \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s) and scheduler_act_not thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>rv s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>(\<lambda>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s) and scheduler_act_not thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>r s. is_activatable (cur_thread s) s\<rbrace>
 2. \<lbrace>(\<lambda>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s) and scheduler_act_not thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>r s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s \<and> scheduler_act_not thread s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> (\<exists>y. kheap s thread = Some y) \<longrightarrow> a_type (the (kheap s thread)) = ATCB \<longrightarrow> (\<forall>st. (cur_thread s = thread \<longrightarrow> runnable st \<or> scheduler_action s \<noteq> resume_cur_thread) \<longrightarrow> st_tcb_at ((=) st) thread (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> is_activatable_2 (cur_thread s) (scheduler_action s) (\<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a))
 2. \<lbrace>(\<lambda>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s) and scheduler_act_not thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>r s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s) and scheduler_act_not thread\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>r s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s \<and> scheduler_act_not thread s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> (\<exists>y. kheap s thread = Some y) \<longrightarrow> a_type (the (kheap s thread)) = ATCB \<longrightarrow> (\<forall>st. (cur_thread s = thread \<longrightarrow> runnable st \<or> scheduler_action s \<noteq> resume_cur_thread) \<longrightarrow> st_tcb_at ((=) st) thread (s\<lparr>kheap := \<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>a. if a = thread then Some (TCB (the (get_tcb thread s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a)) proof (prove)
goal:
No subgoals!