theory Scheduler_IF

lemma sts_reads_respects_scheduler:
  "reads_respects_scheduler aag l
     (K (pasObjectAbs aag rv \<in> reads_scheduler aag l) and reads_scheduler_cur_domain aag l
                                                      and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s))
     (set_thread_state rv st)" apply (simp add: set_thread_state_def) apply (simp add: set_thread_state_ext_def) apply (wp when_ev get_thread_state_reads_respects_scheduler gts_wp set_object_wp) apply (clarsimp simp: get_tcb_scheduler_equiv valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (pasObjectAbs aag rv \<in> reads_scheduler aag l) and reads_scheduler_cur_domain aag l and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s)) (set_thread_state rv st) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>y. pasObjectAbs aag rv \<in> reads_scheduler aag l) and reads_scheduler_cur_domain aag l and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s)) (do tcb <- gets_the (get_tcb rv);
y <- set_object rv (TCB (tcb\<lparr>tcb_state := st\<rparr>));
set_thread_state_ext rv
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>y. pasObjectAbs aag rv \<in> reads_scheduler aag l) and reads_scheduler_cur_domain aag l and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s)) (do tcb <- gets_the (get_tcb rv);
y <- set_object rv (TCB (tcb\<lparr>tcb_state := st\<rparr>));
ts <- get_thread_state rv;
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable ts \<and> cur = rv \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. pasObjectAbs aag rv \<in> reads_scheduler aag l) and reads_scheduler_cur_domain aag l and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s)) s \<Longrightarrow> K (\<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> get_tcb rv s = get_tcb rv t) s \<and> (get_tcb rv s \<noteq> None \<longrightarrow> True \<and> ((\<lambda>s. st_tcb_at (\<lambda>_. True) rv s \<longrightarrow> pasObjectAbs aag rv \<in> reads_scheduler aag l \<or> rv = idle_thread s) and valid_idle) (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) \<and> (\<forall>sta. st_tcb_at ((=) sta) rv (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) \<longrightarrow> reads_scheduler_cur_domain aag l (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) \<and> reads_scheduler_cur_domain aag l (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) \<and> (\<not> runnable sta \<and> cur_thread (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) = rv \<and> scheduler_action (s\<lparr>kheap := (kheap s)(rv \<mapsto> TCB (the (get_tcb rv s)\<lparr>tcb_state := st\<rparr>))\<rparr>) = resume_cur_thread \<longrightarrow> True))) proof (prove)
goal:
No subgoals!