theory Refine

lemma set_thread_state_sched_act:
  "\<lbrace>(\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))\<rbrace>
  set_thread_state thread state
  \<lbrace>\<lambda>rs s. P (scheduler_action (s::det_state))\<rbrace>" apply (simp add: set_thread_state_def) apply wp apply (simp add: set_thread_state_ext_def) apply wp apply (rule hoare_pre_cont) apply (rule_tac Q="\<lambda>rv. (\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))"
              in hoare_strengthen_post) apply wp apply force apply (wp gts_st_tcb_at)+ apply (rule_tac Q="\<lambda>rv. st_tcb_at ((=) state) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))" in hoare_strengthen_post) apply (simp add: st_tcb_at_def) apply (wp obj_set_prop_at)+ apply (force simp: st_tcb_at_def obj_at_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))\<rbrace> set_thread_state thread state \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>));
set_thread_state_ext thread
od \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tcb y. \<lbrace>?B2 tcb y\<rbrace> set_thread_state_ext thread \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> do ts <- get_thread_state thread;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = thread \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace>
 2. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>tcb ts x xa. \<not> runnable ts \<and> x = thread \<and> xa = resume_cur_thread \<Longrightarrow> \<lbrace>?Q7 tcb ts x xa\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace>
 2. \<And>tcb ts x. \<lbrace>?B5 tcb ts x\<rbrace> gets scheduler_action \<lbrace>\<lambda>xa. if \<not> runnable ts \<and> x = thread \<and> xa = resume_cur_thread then ?Q7 tcb ts x xa else (\<lambda>s. P (scheduler_action s))\<rbrace>
 3. \<And>tcb ts. \<lbrace>?B4 tcb ts\<rbrace> gets cur_thread \<lbrace>?B5 tcb ts\<rbrace>
 4. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> get_thread_state thread \<lbrace>?B4 tcb\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 7. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>tcb ts x. \<lbrace>?B5 tcb ts x\<rbrace> gets scheduler_action \<lbrace>\<lambda>xa. if \<not> runnable ts \<and> x = thread \<and> xa = resume_cur_thread then \<lambda>_. False else (\<lambda>s. P (scheduler_action s))\<rbrace>
 2. \<And>tcb ts. \<lbrace>?B4 tcb ts\<rbrace> gets cur_thread \<lbrace>?B5 tcb ts\<rbrace>
 3. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> get_thread_state thread \<lbrace>?B4 tcb\<rbrace>
 4. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>tcb ts x. \<lbrace>?B5 tcb ts x\<rbrace> gets scheduler_action \<lbrace>\<lambda>rv. (\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))\<rbrace>
 2. \<And>tcb ts x rv s. ((\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> (if \<not> runnable ts \<and> x = thread \<and> rv = resume_cur_thread then \<lambda>_. False else (\<lambda>s. P (scheduler_action s))) s
 3. \<And>tcb ts. \<lbrace>?B4 tcb ts\<rbrace> gets cur_thread \<lbrace>?B5 tcb ts\<rbrace>
 4. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> get_thread_state thread \<lbrace>?B4 tcb\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 7. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>tcb ts x rv s. ((\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> (if \<not> runnable ts \<and> x = thread \<and> rv = resume_cur_thread then \<lambda>_. False else (\<lambda>s. P (scheduler_action s))) s
 2. \<And>tcb ts. \<lbrace>?B4 tcb ts\<rbrace> gets cur_thread \<lbrace>\<lambda>x. (\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))\<rbrace>
 3. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> get_thread_state thread \<lbrace>?B4 tcb\<rbrace>
 4. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 6. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>tcb ts. \<lbrace>?B4 tcb ts\<rbrace> gets cur_thread \<lbrace>\<lambda>x. (\<lambda>s. runnable ts) and (\<lambda>s. P (scheduler_action s))\<rbrace>
 2. \<And>tcb. \<lbrace>?B2 tcb ()\<rbrace> get_thread_state thread \<lbrace>?B4 tcb\<rbrace>
 3. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>?B2 tcb\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 5. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>\<lambda>a b. st_tcb_at runnable thread b \<and> P (scheduler_action b)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 3. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>\<lambda>rv. st_tcb_at ((=) state) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))\<rbrace>
 2. \<And>tcb rv s. (st_tcb_at ((=) state) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> st_tcb_at runnable thread s \<and> P (scheduler_action s)
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_state := state\<rparr>)) \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> state = tcb_state tcb) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))\<rbrace>
 2. \<And>tcb rv s. (st_tcb_at ((=) state) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> st_tcb_at runnable thread s \<and> P (scheduler_action s)
 3. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>?B1\<rbrace>
 4. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb rv s. (st_tcb_at ((=) state) thread and (\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> st_tcb_at runnable thread s \<and> P (scheduler_action s)
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>tcb s. (\<exists>tcba. TCB (tcb\<lparr>tcb_state := state\<rparr>) = TCB tcba \<and> state = tcb_state tcba) \<and> runnable state \<and> P (scheduler_action s)\<rbrace>
 3. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>tcb s. (\<exists>tcba. TCB (tcb\<lparr>tcb_state := state\<rparr>) = TCB tcba \<and> state = tcb_state tcba) \<and> runnable state \<and> P (scheduler_action s)\<rbrace>
 2. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. runnable state) and (\<lambda>s. P (scheduler_action s))) s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (\<exists>tcb. TCB (the (get_tcb thread s)\<lparr>tcb_state := state\<rparr>) = TCB tcb \<and> state = tcb_state tcb) \<and> runnable state \<and> P (scheduler_action s) proof (prove)
goal:
No subgoals!