theory Syscall_IF

lemma sts_schact_is_rct_runnable:
  "\<lbrace>schact_is_rct and K (runnable b)\<rbrace>
   set_thread_state a b
   \<lbrace>\<lambda>_. schact_is_rct\<rbrace>" apply (simp add: set_thread_state_def set_scheduler_action_def) apply (wpsimp wp: set_object_wp) apply (simp add: set_thread_state_ext_def) apply (wp modify_wp set_scheduler_action_wp gts_wp) apply (wpsimp wp: set_object_wp) apply wp apply (clarsimp simp: schact_is_rct_def st_tcb_at_def obj_at_def gets_the_def gets_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>schact_is_rct and K (runnable b)\<rbrace> set_thread_state a b \<lbrace>\<lambda>_. schact_is_rct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>schact_is_rct and (\<lambda>y. runnable b)\<rbrace> do tcb <- gets_the (get_tcb a);
y <- set_object a (TCB (tcb\<lparr>tcb_state := b\<rparr>));
set_thread_state_ext a
od \<lbrace>\<lambda>_. schact_is_rct\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B3 tcb ()\<rbrace> set_thread_state_ext a \<lbrace>\<lambda>_. schact_is_rct\<rbrace>
 2. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> set_object a (TCB (tcb\<lparr>tcb_state := b\<rparr>)) \<lbrace>?B3 tcb\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets_the (get_tcb a) \<lbrace>?B2\<rbrace>
 4. \<And>s. (schact_is_rct and (\<lambda>y. runnable b)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrace>?B3 tcb ()\<rbrace> do ts <- get_thread_state a;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = a \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. schact_is_rct\<rbrace>
 2. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> set_object a (TCB (tcb\<lparr>tcb_state := b\<rparr>)) \<lbrace>?B3 tcb\<rbrace>
 3. \<lbrace>?Q1\<rbrace> gets_the (get_tcb a) \<lbrace>?B2\<rbrace>
 4. \<And>s. (schact_is_rct and (\<lambda>y. runnable b)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> set_object a (TCB (tcb\<lparr>tcb_state := b\<rparr>)) \<lbrace>\<lambda>b c. \<forall>st. st_tcb_at ((=) st) a c \<longrightarrow> (if \<not> runnable st \<and> cur_thread c = a \<and> scheduler_action c = resume_cur_thread then \<lambda>s. schact_is_rct (scheduler_action_update (\<lambda>_. choose_new_thread) s) else schact_is_rct) c\<rbrace>
 2. \<lbrace>?Q1\<rbrace> gets_the (get_tcb a) \<lbrace>?B2\<rbrace>
 3. \<And>s. (schact_is_rct and (\<lambda>y. runnable b)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> gets_the (get_tcb a) \<lbrace>\<lambda>tcb s. \<forall>st. st_tcb_at ((=) st) a (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_state := b\<rparr>))\<rparr>) \<longrightarrow> (if \<not> runnable st \<and> cur_thread (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_state := b\<rparr>))\<rparr>) = a \<and> scheduler_action (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_state := b\<rparr>))\<rparr>) = resume_cur_thread then \<lambda>s. schact_is_rct (scheduler_action_update (\<lambda>_. choose_new_thread) s) else schact_is_rct) (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_state := b\<rparr>))\<rparr>)\<rbrace>
 2. \<And>s. (schact_is_rct and (\<lambda>y. runnable b)) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (schact_is_rct and (\<lambda>y. runnable b)) s \<Longrightarrow> get_tcb a s \<noteq> None \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) a (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_state := b\<rparr>))\<rparr>) \<longrightarrow> (if \<not> runnable st \<and> cur_thread (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_state := b\<rparr>))\<rparr>) = a \<and> scheduler_action (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_state := b\<rparr>))\<rparr>) = resume_cur_thread then \<lambda>s. schact_is_rct (scheduler_action_update (\<lambda>_. choose_new_thread) s) else schact_is_rct) (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_state := b\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!