theory Scheduler_IF

lemma sts_scheduler_affects_equiv[wp]:
  "\<lbrace>K (pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace>
   set_thread_state x Running
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def) apply (wp gts_wp set_object_wp) apply (intro impI conjI allI) apply (clarsimp simp: st_tcb_at_def obj_at_def) apply (fastforce intro!: scheduler_affects_equiv_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> set_thread_state x Running \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> do tcb <- gets_the (get_tcb x);
y <- set_object x (TCB (tcb\<lparr>tcb_state := Running\<rparr>));
set_thread_state_ext x
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> do tcb <- gets_the (get_tcb x);
y <- set_object x (TCB (tcb\<lparr>tcb_state := Running\<rparr>));
ts <- get_thread_state x;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = x \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st) s \<Longrightarrow> get_tcb x s \<noteq> None \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) \<longrightarrow> (if \<not> runnable sta \<and> cur_thread (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) = x \<and> scheduler_action (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) = resume_cur_thread then \<lambda>s. scheduler_affects_equiv aag l st (scheduler_action_update (\<lambda>_. choose_new_thread) s) else scheduler_affects_equiv aag l st) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>((\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st) s; get_tcb x s \<noteq> None; st_tcb_at ((=) sta) x (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> (if \<not> runnable sta \<and> cur_thread (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) = x \<and> scheduler_action (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) = resume_cur_thread then \<lambda>s. scheduler_affects_equiv aag l st (scheduler_action_update (\<lambda>_. choose_new_thread) s) else scheduler_affects_equiv aag l st) (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>get_tcb x s = Some y; pasObjectAbs aag x \<notin> reads_scheduler aag l; scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (y\<lparr>tcb_state := Running\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!