theory BCorres2_AI

lemma choose_thread_bcorres: "BCorres2_AI TYPE(det_ext)
    \<Longrightarrow> s_bcorres choose_thread schedule s" apply (frule BCorres2_AI.switch_thread_bcorreses(1)) apply (simp add: choose_thread_def gets_def s_bcorres_get_left
                   BCorres2_AI.guarded_switch_bcorres) apply (clarsimp simp: schedule_def s_bcorres_underlying_def) apply (drule_tac s=s in drop_sbcorres_underlying) apply (clarsimp simp: s_bcorres_underlying_def) apply (auto intro!: alternative_second simp: exec_gets) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. BCorres2_AI TYPE(det_ext) \<Longrightarrow> s_bcorres choose_thread schedule s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BCorres2_AI TYPE(det_ext); bcorres switch_to_idle_thread switch_to_idle_thread\<rbrakk> \<Longrightarrow> s_bcorres choose_thread schedule s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>BCorres2_AI TYPE(det_ext); bcorres switch_to_idle_thread switch_to_idle_thread\<rbrakk> \<Longrightarrow> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> s_bcorres switch_to_idle_thread schedule s proof (prove)
goal (1 subgoal):
 1. \<And>ba. \<lbrakk>BCorres2_AI TYPE(det_ext); bcorres switch_to_idle_thread switch_to_idle_thread; \<forall>prio. ready_queues s (cur_domain s) prio = []; ((), ba) \<in> fst (switch_to_idle_thread s)\<rbrakk> \<Longrightarrow> ((), truncate_state ba) \<in> fst ((do cur <- gets cur_thread;
threads <- allActiveTCBs;
thread <- select threads;
if thread = cur then return () \<sqinter> switch_to_thread cur else switch_to_thread thread
od \<sqinter> do cur <- gets cur_thread;
idl <- gets idle_thread;
if idl = cur then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread
od) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba. \<lbrakk>BCorres2_AI TYPE(det_ext); \<forall>prio. ready_queues s (cur_domain s) prio = []; ((), ba) \<in> fst (switch_to_idle_thread s); s_bcorres switch_to_idle_thread switch_to_idle_thread s\<rbrakk> \<Longrightarrow> ((), truncate_state ba) \<in> fst ((do cur <- gets cur_thread;
threads <- allActiveTCBs;
thread <- select threads;
if thread = cur then return () \<sqinter> switch_to_thread cur else switch_to_thread thread
od \<sqinter> do cur <- gets cur_thread;
idl <- gets idle_thread;
if idl = cur then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread
od) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba. \<lbrakk>BCorres2_AI TYPE(det_ext); \<forall>prio. ready_queues s (cur_domain s) prio = []; ((), ba) \<in> fst (switch_to_idle_thread s); (\<lambda>x. case x of (x, y) \<Rightarrow> ((), truncate_state y)) ` fst (switch_to_idle_thread s) \<subseteq> fst (switch_to_idle_thread (truncate_state s))\<rbrakk> \<Longrightarrow> ((), truncate_state ba) \<in> fst ((do cur <- gets cur_thread;
threads <- allActiveTCBs;
thread <- select threads;
if thread = cur then return () \<sqinter> switch_to_thread cur else switch_to_thread thread
od \<sqinter> do cur <- gets cur_thread;
idl <- gets idle_thread;
if idl = cur then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread
od) (truncate_state s)) proof (prove)
goal:
No subgoals!