theory DetSchedSchedule_AI

lemma switch_to_thread_valid_blocked[wp]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_thread thread \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: switch_to_thread_def) apply (wp|wpc)+ prefer 4 apply (rule get_wp) prefer 3 apply (rule assert_inv) prefer 2 apply (rule arch_switch_to_thread_valid_blocked) by (wp tcb_sched_action_dequeue_ct_in_cur_domain' tcb_sched_action_dequeue_valid_blocked')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> switch_to_thread thread \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb thread state = Some y);
y <- arch_switch_to_thread thread;
y <- tcb_sched_action tcb_sched_dequeue thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 3. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb thread state = Some y) \<lbrace>?B2 state\<rbrace>
 4. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 5. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 2. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 3. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 4. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb thread state = Some y) \<lbrace>?B2 state\<rbrace>
 5. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 3. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb thread state = Some y) \<lbrace>?B2 state\<rbrace>
 4. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?B1 s s proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb thread state = Some y) \<lbrace>?B2 state\<rbrace>
 2. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 3. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 4. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?B1 s s proof (prove)
goal (3 subgoals):
 1. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>?B1 state\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 3. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?B1 s s proof (prove)
goal (3 subgoals):
 1. \<And>state y. \<lbrace>?B1 state\<rbrace> arch_switch_to_thread thread \<lbrace>?B3 state y\<rbrace>
 2. \<And>state y ya. \<lbrace>?B3 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 3. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> ?B1 s s proof (prove)
goal (2 subgoals):
 1. \<And>state y ya. \<lbrace>valid_blocked and ct_in_q\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>yb s. valid_blocked (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
 2. \<And>s. (valid_blocked and ct_in_q) s \<Longrightarrow> (valid_blocked and ct_in_q) s