theory DetSchedSchedule_AI

lemma set_thread_state_runnable_valid_blocked:
  "\<lbrace>valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: set_thread_state_def) apply (rule hoare_seq_ext[OF _ gets_the_get_tcb_sp]) apply (rule_tac B="\<lambda>rv. valid_blocked and st_tcb_at runnable ref" in hoare_seq_ext[rotated]) apply (wp set_object_wp) apply (clarsimp simp: valid_blocked_def not_queued_def runnable_eq_active
                         pred_tcb_at_def st_tcb_at_kh_def obj_at_kh_def obj_at_def) apply (simp add: set_thread_state_ext_def) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule_tac S="runnable ts" in hoare_gen_asm_spec) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply clarsimp by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts)\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts)\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrace>valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts) and ko_at (TCB tcb) ref\<rbrace> do y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts) and ko_at (TCB tcb) ref\<rbrace> set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>)) \<lbrace>\<lambda>rv. valid_blocked and st_tcb_at runnable ref\<rbrace>
 2. \<And>tcb x. \<lbrace>valid_blocked and st_tcb_at runnable ref\<rbrace> set_thread_state_ext ref \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. (valid_blocked and st_tcb_at runnable ref and (\<lambda>s. runnable ts) and ko_at (TCB tcb) ref) s \<Longrightarrow> (valid_blocked and st_tcb_at runnable ref) (s\<lparr>kheap := (kheap s)(ref \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
 2. \<And>tcb x. \<lbrace>valid_blocked and st_tcb_at runnable ref\<rbrace> set_thread_state_ext ref \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb x. \<lbrace>valid_blocked and st_tcb_at runnable ref\<rbrace> set_thread_state_ext ref \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and st_tcb_at runnable ref\<rbrace> do ts <- get_thread_state ref;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ts. \<lbrace>st_tcb_at ((=) ts) ref and (valid_blocked and st_tcb_at runnable ref)\<rbrace> do cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ts s. (st_tcb_at ((=) ts) ref and (valid_blocked and st_tcb_at runnable ref)) s \<Longrightarrow> runnable ts
 2. \<And>ts. runnable ts \<Longrightarrow> \<lbrace>st_tcb_at ((=) ts) ref and (valid_blocked and st_tcb_at runnable ref)\<rbrace> do cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ts. runnable ts \<Longrightarrow> \<lbrace>st_tcb_at ((=) ts) ref and (valid_blocked and st_tcb_at runnable ref)\<rbrace> do cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = ref \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ts. runnable ts \<Longrightarrow> \<lbrace>st_tcb_at ((=) ts) ref and (valid_blocked and st_tcb_at runnable ref)\<rbrace> do cur <- gets cur_thread;
action <- gets scheduler_action;
return ()
od \<lbrace>\<lambda>_. valid_blocked\<rbrace>