kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma as_user_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: valid_blocked_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def) apply (drule_tac x=ptr in spec) by (drule get_tcb_SomeD, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. valid_blocked sa \<Longrightarrow> (\<exists>y. get_tcb ptr sa = Some y) \<longrightarrow> (\<forall>x\<in>fst (s (arch_tcb_context_get (tcb_arch (the (get_tcb ptr sa))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> a_type (the (kheap sa ptr)) = ATCB \<longrightarrow> valid_blocked_2 (ready_queues sa) (\<lambda>a. if a = ptr then Some (TCB (the (get_tcb ptr sa)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb ptr sa)))\<rparr>)) else kheap sa a) (scheduler_action sa) (cur_thread sa)) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb. \<lbrakk>\<forall>t. not_queued t sa \<longrightarrow> (\<forall>st. (\<exists>ko. kheap sa t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> st = tcb_state tcb)) \<longrightarrow> t \<noteq> cur_thread sa \<longrightarrow> scheduler_action sa \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); not_queued ptr sa; ptr \<noteq> cur_thread sa; scheduler_action sa \<noteq> switch_thread ptr\<rbrakk> \<Longrightarrow> tcb_state y \<noteq> Running \<and> tcb_state y \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb. \<lbrakk>get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); not_queued ptr sa; ptr \<noteq> cur_thread sa; scheduler_action sa \<noteq> switch_thread ptr; not_queued ptr sa \<longrightarrow> (\<forall>st. (\<exists>ko. kheap sa ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> st = tcb_state tcb)) \<longrightarrow> ptr \<noteq> cur_thread sa \<longrightarrow> scheduler_action sa \<noteq> switch_thread ptr \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> tcb_state y \<noteq> Running \<and> tcb_state y \<noteq> Restart
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_ct_not_in_q_2_ct_upd:
  "\<lbrace>valid_queues\<rbrace>
     tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>r s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) thread\<rbrace>" apply (simp add: tcb_sched_action_def unless_def set_tcb_queue_def) apply wp apply (fastforce simp: etcb_at_def ct_not_in_q_def valid_queues_def
                         tcb_sched_dequeue_def not_queued_def
                   split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>r s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then tcb_sched_dequeue thread queue else ready_queues es d' p) es)
od \<lbrace>\<lambda>r s. ct_not_in_q_2 (ready_queues s) (scheduler_action s) thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_not_in_q_2 (ready_queues (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) (scheduler_action (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) thread) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_valid_sched_action_2_ct_upd:
  "\<lbrace>valid_sched_action and
       (\<lambda>s. is_activatable_2 thread (scheduler_action s) (kheap s))\<rbrace>
     tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>r s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) thread (cur_domain s)\<rbrace>" apply (simp add: tcb_sched_action_def unless_def set_tcb_queue_def) apply wp apply (clarsimp simp: etcb_at_def valid_sched_action_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and is_activatable thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>r s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) thread (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and is_activatable thread\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = d \<and> p = prio then tcb_sched_dequeue thread queue else ready_queues es d' p) es)
od \<lbrace>\<lambda>r s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) thread (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched_action and is_activatable thread) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_sched_action_2 (scheduler_action (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) (ekheap (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) (kheap (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s)) thread (cur_domain (ready_queues_update (\<lambda>_ d' p. if d' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s d' p) s))) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma as_user_valid_sched[wp]:
  "\<lbrace>valid_sched\<rbrace> as_user tptr f \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def) apply (wp | wpc)+ apply clarsimp apply (fastforce simp: valid_sched_def valid_etcbs_def valid_queues_def
                         valid_sched_action_def is_activatable_def
                         weak_valid_sched_action_def st_tcb_at_kh_if_split
                         st_tcb_def2 valid_blocked_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> as_user tptr f \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do tcb <- gets_the (get_tcb tptr);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tptr = Some y);
return (the (kh tptr))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return a
od \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched s \<Longrightarrow> get_tcb tptr s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb tptr s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap s tptr = Some y) \<longrightarrow> a_type (the (kheap s tptr)) = ATCB \<longrightarrow> valid_sched (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb tptr s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>valid_sched s; (x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb tptr s = Some y; kheap s tptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_sched_2 (ready_queues s) (ekheap s) (scheduler_action s) (cur_domain s) (\<lambda>a. if a = tptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap s a) (cur_thread s) (idle_thread s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ct_not_in_q_def2:
  "ct_not_in_q_2 queues sa ct = (sa = resume_cur_thread \<longrightarrow> (\<forall>d p. ct \<notin> set (queues d p)))" by (fastforce simp add: ct_not_in_q_def not_queued_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_not_in_q_2 queues sa ct = (sa = resume_cur_thread \<longrightarrow> (\<forall>d p. ct \<notin> set (queues d p)))
theory DetSchedSchedule_AI

lemma switch_to_thread_ct_not_in_q[wp]:
  "\<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: ct_not_in_q_def2 not_queued_def[symmetric]) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> switch_to_thread t \<lbrace>\<lambda>_ s. scheduler_action s = resume_cur_thread \<longrightarrow> ct_not_queued s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma switch_to_thread_valid_sched_action[wp]:
  "\<lbrace>valid_sched_action and is_activatable t\<rbrace>
     switch_to_thread t
   \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" by (wpsimp wp: tcb_sched_action_dequeue_valid_sched_action_2_ct_upd simp: switch_to_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and is_activatable t\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. valid_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_ct_in_cur_domain':
  "\<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>
    tcb_sched_action tcb_sched_dequeue thread
  \<lbrace>\<lambda>_ s. ct_in_cur_domain (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (simp add: etcb_at_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_ s. ct_in_cur_domain (s\<lparr>cur_thread := thread\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_dequeue thread queue)
od \<lbrace>\<lambda>_ s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s) \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_in_cur_domain_2 thread (idle_thread (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (scheduler_action (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (cur_domain (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) (ekheap (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_dequeue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s))) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma switch_to_thread_ct_in_cur_domain[wp]:
  "\<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace>
  switch_to_thread thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: switch_to_thread_def) apply (wpsimp wp: tcb_sched_action_dequeue_ct_in_cur_domain') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<rbrace> switch_to_thread thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_in_cur_domain_2 thread (idle_thread s) (scheduler_action s) (cur_domain s) (ekheap s)\<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>_. ct_in_cur_domain\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma ct_in_q_arch_state_upd[simp]:
  "ct_in_q (s\<lparr>arch_state := f\<rparr>) = ct_in_q s" by (simp add: ct_in_q_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_q (s\<lparr>arch_state := f\<rparr>) = ct_in_q s
theory DetSchedSchedule_AI

lemma ct_in_q_machine_state_upd[simp]:
  "ct_in_q (s\<lparr>machine_state := f\<rparr>) = ct_in_q s" by (simp add: ct_in_q_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_q (s\<lparr>machine_state := f\<rparr>) = ct_in_q s
theory DetSchedSchedule_AI

lemma do_machine_op_valid_blocked[wp]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>" by (wpsimp | auto)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>
theory DetSchedSchedule_AI

lemma switch_to_thread_valid_sched:
  "\<lbrace>is_activatable t and in_cur_domain t and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb\<rbrace>
    switch_to_thread t
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def | wp | simp add: ct_in_cur_domain_2_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_activatable t and in_cur_domain t and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma valid_queues_trivial[simp]: "valid_queues_2 (\<lambda>_ _. []) kh ekh" by (simp add: valid_queues_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues_2 (\<lambda>_ _. []) kh ekh
theory DetSchedSchedule_AI

lemma ct_not_in_q_trivial[simp]: "ct_not_in_q_2 (\<lambda>_ _. []) sa ct" by (simp add: ct_not_in_q_def not_queued_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_not_in_q_2 (\<lambda>_ _. []) sa ct
theory DetSchedSchedule_AI

lemma st_tcb_at_get_lift: "get_tcb thread s = Some y \<Longrightarrow> test (tcb_state y) \<Longrightarrow>
         st_tcb_at test thread s" by (simp add: ct_in_state_def st_tcb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb thread s = Some y; test (tcb_state y)\<rbrakk> \<Longrightarrow> st_tcb_at test thread s
theory DetSchedSchedule_AI

lemma guarded_switch_to_lift:
  "\<lbrace>P\<rbrace> switch_to_thread thread \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> guarded_switch_to thread \<lbrace>Q\<rbrace>" by (wpsimp simp: guarded_switch_to_def get_thread_state_def thread_get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> switch_to_thread thread \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> guarded_switch_to thread \<lbrace>Q\<rbrace>
theory DetSchedSchedule_AI

lemma tcb_sched_action_lift:
  "(\<And>f s. P s \<Longrightarrow> P (ready_queues_update f s))
  \<Longrightarrow> \<lbrace>P\<rbrace> tcb_sched_action a b \<lbrace>\<lambda>_. P\<rbrace>" by (wp | simp add: tcb_sched_action_def etcb_at_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>f s. P s \<Longrightarrow> P (ready_queues_update f s)) \<Longrightarrow> \<lbrace>P\<rbrace> tcb_sched_action a b \<lbrace>\<lambda>_. P\<rbrace>
theory DetSchedSchedule_AI

lemma enqueue_thread_queued:
  "\<lbrace>\<top>\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread
   \<lbrace>\<lambda>_ s. (\<exists>d prio. thread \<in> set (ready_queues s d prio))\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (fastforce simp: etcb_at_def tcb_sched_enqueue_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_ s. \<exists>d prio. thread \<in> set (ready_queues s d prio)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do d <- ethread_get tcb_domain thread;
prio <- ethread_get tcb_priority thread;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue thread queue)
od \<lbrace>\<lambda>_ s. \<exists>d prio. thread \<in> set (ready_queues s d prio)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. \<exists>d prio. thread \<in> set (ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s) d prio)) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma enqueue_nonempty:
  "\<lbrace>\<top>\<rbrace>
   tcb_sched_action tcb_sched_enqueue thread
   \<lbrace>\<lambda>_ s. (\<exists>d prio. ready_queues s d prio \<noteq> [])\<rbrace>" by (rule hoare_post_imp[OF _ enqueue_thread_queued], metis empty_iff empty_set)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_ s. \<exists>d prio. ready_queues s d prio \<noteq> []\<rbrace>
theory DetSchedSchedule_AI

lemma next_thread_queued: "queues p \<noteq> [] \<Longrightarrow> \<exists>p. next_thread queues \<in> set (queues p)" apply (clarsimp simp: next_thread_def max_non_empty_queue_def) apply (rule_tac x="Max {prio. queues prio \<noteq> []}" in exI) apply (rule Max_prop) apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. queues p \<noteq> [] \<Longrightarrow> \<exists>p. next_thread queues \<in> set (queues p) proof (prove)
goal (1 subgoal):
 1. queues p \<noteq> [] \<Longrightarrow> \<exists>p. hd (queues (Max {prio. queues prio \<noteq> []})) \<in> set (queues p) proof (prove)
goal (1 subgoal):
 1. queues p \<noteq> [] \<Longrightarrow> hd (queues (Max {prio. queues prio \<noteq> []})) \<in> set (queues (Max {prio. queues prio \<noteq> []})) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queues p \<noteq> []; Max {prio. queues prio \<noteq> []} \<in> {prio. queues prio \<noteq> []}\<rbrakk> \<Longrightarrow> hd (queues (Max {prio. queues prio \<noteq> []})) \<in> set (queues (Max {prio. queues prio \<noteq> []}))
 2. queues p \<noteq> [] \<Longrightarrow> {prio. queues prio \<noteq> []} \<noteq> {} proof (prove)
goal (1 subgoal):
 1. queues p \<noteq> [] \<Longrightarrow> {prio. queues prio \<noteq> []} \<noteq> {} proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma choose_thread_valid_sched[wp]:
  "\<lbrace>valid_sched_action and valid_idle and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb\<rbrace>
     choose_thread
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: choose_thread_def) apply (wp guarded_switch_to_lift switch_to_idle_thread_valid_sched switch_to_thread_valid_sched) apply (clarsimp simp: valid_queues_def next_thread_def is_activatable_2_def
                 dest!: next_thread_queued) apply (fastforce simp: st_tcb_def2 in_cur_domain_def etcb_at_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and valid_idle and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb\<rbrace> choose_thread \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action and valid_idle and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb\<rbrace> do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_sched_action and valid_idle and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (valid_sched_action and valid_idle and valid_queues and valid_etcbs and valid_blocked and ct_in_q and valid_idle_etcb) s) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (is_activatable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) and in_cur_domain (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) and valid_sched_action and valid_etcbs and valid_queues and valid_blocked and ct_in_q and valid_idle_etcb) s) proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>valid_sched_action s; valid_idle s; valid_etcbs s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); valid_blocked s; ct_in_q s; valid_idle_etcb s; hd (max_non_empty_queue (ready_queues s (cur_domain s))) \<in> set (ready_queues s (cur_domain s) p)\<rbrakk> \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> st_tcb_at activatable (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s) \<and> in_cur_domain (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_enqueue_in_cur_domain:
  "\<lbrace>in_cur_domain w\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>_. in_cur_domain w\<rbrace>" apply (simp add: tcb_sched_action_def in_cur_domain_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_cur_domain w\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>_. in_cur_domain w\<rbrace> proof (prove)
goal:
No subgoals!