theory DetSchedSchedule_AI

lemma switch_to_thread_ct_not_queued[wp]:
  "\<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv s. not_queued (cur_thread s) s\<rbrace>" apply (simp add: switch_to_thread_def) including no_pre apply wp prefer 4 apply (rule get_wp) prefer 3 apply (rule assert_inv) prefer 2 apply (rule arch_switch_to_thread_valid_queues') apply (simp add: tcb_sched_action_def
                   tcb_sched_dequeue_def | wp)+ apply (clarsimp simp add: valid_queues_def etcb_at_def not_queued_def
                       split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv. ct_not_queued\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>rv. ct_not_queued\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>rv. ct_not_queued\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>?B1 state y\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace>
 3. \<And>state. \<lbrace>?B state\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>?B1 state\<rbrace>
 4. \<lbrace>valid_queues\<rbrace> get \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>valid_queues\<rbrace> get \<lbrace>?B\<rbrace>
 2. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace>
 3. \<And>state y. \<lbrace>?B1 state y\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace>
 4. \<And>state. \<lbrace>?B state\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>?B1 state\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>?B1 state y\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace>
 3. \<And>state. \<lbrace>valid_queues\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>?B1 state\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>state. \<lbrace>valid_queues\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>?B1 state\<rbrace>
 2. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace>
 3. \<And>state y. \<lbrace>?B1 state y\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace>
 2. \<And>state y. \<lbrace>valid_queues\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state y. \<lbrace>valid_queues\<rbrace> arch_switch_to_thread t \<lbrace>?B2 state y\<rbrace>
 2. \<And>state y ya. \<lbrace>?B2 state y ya\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state y ya. \<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>yb s. ct_not_queued (s\<lparr>cur_thread := t\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> etcb_at (\<lambda>ta. etcb_at (\<lambda>tb. not_queued_2 (\<lambda>a b. if a = tcb_domain ta \<and> b = tcb_priority tb then filter (\<lambda>x. x \<noteq> t) (ready_queues s (tcb_domain ta) (tcb_priority tb)) else ready_queues s a b) t) t s) t s proof (prove)
goal:
No subgoals!