kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedSchedule_AI

lemma tcb_sched_action_append_valid_queues[wp]:
  "\<lbrace>valid_queues and st_tcb_at runnable thread\<rbrace>
     tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_append_def is_etcb_at_def
         split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and st_tcb_at runnable thread\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_queues and st_tcb_at runnable thread) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append 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 tcb_sched_action_dequeue_valid_queues[wp]:
  "\<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_dequeue_def
         split: option.splits) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_queues (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 (1 subgoal):
 1. \<And>s x2 t. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<and> (\<forall>x2. ekheap s t = Some x2 \<longrightarrow> tcb_domain x2 = d \<and> tcb_priority x2 = p \<and> is_etcb_at t s \<and> st_tcb_at runnable t s)) \<and> distinct (ready_queues s d p); ekheap s thread = Some x2; t \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)); t \<noteq> thread\<rbrakk> \<Longrightarrow> is_etcb_at t s \<and> st_tcb_at runnable t s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_action_enqueue_ct_not_in_q[wp]:
  "\<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread
     \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: ct_not_in_q_def not_cur_thread_def etcb_at_def
                        tcb_sched_enqueue_def not_queued_def
         split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_not_in_q and not_cur_thread thread) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_not_in_q (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)) thread s) thread s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma tcb_sched_action_append_ct_not_in_q[wp]:
  "\<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace>
     tcb_sched_action tcb_sched_append thread
     \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: ct_not_in_q_def not_cur_thread_def etcb_at_def
                        tcb_sched_append_def not_queued_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q and not_cur_thread thread\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_not_in_q and not_cur_thread thread) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. ct_not_in_q (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_append 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 tcb_sched_action_enqueue_valid_sched[wp]:
  "\<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def | wp tcb_sched_action_enqueue_valid_blocked)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace> tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma tcb_sched_action_append_valid_sched[wp]:
  "\<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace>
      tcb_sched_action tcb_sched_append thread
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def | wp tcb_sched_action_append_valid_blocked)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and st_tcb_at runnable thread and not_cur_thread thread and valid_blocked_except thread\<rbrace> tcb_sched_action tcb_sched_append thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_valid_sched_not_runnable:
  "\<lbrace>valid_sched and st_tcb_at (\<lambda>st. \<not> active st) thread\<rbrace>
     tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def | wp tcb_sched_action_dequeue_valid_blocked)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and st_tcb_at (\<lambda>st. \<not> active st) thread\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma tcb_sched_action_dequeue_valid_sched_except_blocked:
  "\<lbrace>valid_sched\<rbrace>
     tcb_sched_action tcb_sched_dequeue thread
   \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace>" by (simp add: valid_sched_def | wp tcb_sched_action_dequeue_valid_blocked_except)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> tcb_sched_action tcb_sched_dequeue thread \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace>
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_ct_not_in_q[wp]:
  "\<lbrace>ct_not_queued\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (fastforce simp: ct_not_in_q_def not_queued_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_queued\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ct_not_queued s \<Longrightarrow> ct_not_in_q (scheduler_action_update (\<lambda>_. resume_cur_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_is_activatable[wp]:
  "\<lbrace>st_tcb_at activatable t\<rbrace>
     set_scheduler_action resume_cur_thread
   \<lbrace>\<lambda>_. is_activatable t\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (simp add: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at activatable t\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. is_activatable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at activatable t s \<Longrightarrow> is_activatable t (scheduler_action_update (\<lambda>_. resume_cur_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_wp:
  "\<lbrace>\<lambda>s. Q (scheduler_action_update (\<lambda>_. a) s)\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_.Q\<rbrace>" apply (simp add: set_scheduler_action_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (scheduler_action_update (\<lambda>_. a) s)\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (scheduler_action_update (\<lambda>_. a) s)\<rbrace> modify (scheduler_action_update (\<lambda>_. a)) \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_valid_sched_action[wp]:
  "\<lbrace>\<lambda>s. st_tcb_at activatable (cur_thread s) s\<rbrace>
     set_scheduler_action resume_cur_thread
   \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def  | wp set_scheduler_action_wp)+ apply (simp add: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at activatable (cur_thread s) s\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at activatable (cur_thread s) s \<Longrightarrow> is_activatable_2 (cur_thread s) resume_cur_thread (kheap s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_ct_in_cur_domain[wp]:
  "\<lbrace>\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace>
     set_scheduler_action resume_cur_thread  \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: valid_sched_action_def  | wp set_scheduler_action_wp)+ apply (clarsimp simp: in_cur_domain_def ct_in_cur_domain_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. in_cur_domain (cur_thread s) s \<or> cur_thread s = idle_thread s \<Longrightarrow> ct_in_cur_domain_2 (cur_thread s) (idle_thread s) resume_cur_thread (cur_domain s) (ekheap s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_rct_valid_blocked:
  "\<lbrace>valid_blocked and simple_sched_action\<rbrace>
     set_scheduler_action resume_cur_thread  \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: valid_blocked_def simple_sched_action_def split: scheduler_action.splits | wp set_scheduler_action_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and simple_sched_action\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_ct_not_in_q[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (simp add: ct_not_in_q_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ct_not_in_q (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_is_activatable[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. is_activatable t\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (simp add: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. is_activatable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> is_activatable t (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_ct_in_cur_domain[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (simp add: ct_in_cur_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ct_in_cur_domain (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_weak_valid_sched_action[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" apply (simp add: set_scheduler_action_def, wp) apply (simp add: weak_valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> weak_valid_sched_action (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_valid_sched_action[wp]:
  "\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def, wp set_scheduler_action_wp) apply (simp add: is_activatable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> is_activatable (cur_thread (scheduler_action_update (\<lambda>_. choose_new_thread) s)) (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<and> weak_valid_sched_action (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<and> switch_in_cur_domain (scheduler_action_update (\<lambda>_. choose_new_thread) s) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_valid_blocked_weak:
  "\<lbrace>valid_blocked and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread  \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: valid_blocked_def, wp set_scheduler_action_wp) apply (simp add: simple_sched_action_def split: scheduler_action.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)) and simple_sched_action) s \<Longrightarrow> \<forall>t. not_queued t (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> t \<noteq> cur_thread (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<longrightarrow> scheduler_action (scheduler_action_update (\<lambda>_. choose_new_thread) s) \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma set_scheduler_action_cnt_weak_valid_sched:
  "\<lbrace>valid_sched and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def simple_sched_action_def split: scheduler_action.splits | wp set_scheduler_action_cnt_valid_blocked)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and simple_sched_action\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_valid_queues[wp]:
  "\<lbrace>valid_queues and weak_valid_sched_action\<rbrace>
      reschedule_required
   \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: reschedule_required_def | wp | wpc)+ apply (simp add: weak_valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues and weak_valid_sched_action\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<and> weak_valid_sched_action s \<Longrightarrow> \<forall>x. scheduler_action s = switch_thread x \<longrightarrow> st_tcb_at runnable x s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma reschedule_required_ct_not_in_q[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>" by (simp add: reschedule_required_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_not_in_q\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_is_activatable[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. is_activatable t\<rbrace>" by (simp add: reschedule_required_def, wp)

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

lemma reschedule_required_weak_valid_sched_action[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>" by (simp add: reschedule_required_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>_. weak_valid_sched_action\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_valid_sched_action[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: valid_sched_action_def reschedule_required_def) apply (wp set_scheduler_action_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od \<lbrace>\<lambda>_ s. is_activatable (cur_thread s) s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma reschedule_required_ct_in_cur_domain[wp]:
  "\<lbrace>\<top>\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>" by (simp add: reschedule_required_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>_. ct_in_cur_domain\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_valid_sched:
  "\<lbrace>valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked and valid_idle_etcb\<rbrace>
    reschedule_required
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" by (simp add: valid_sched_def | wp reschedule_required_valid_blocked)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked and valid_idle_etcb\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched\<rbrace>
theory DetSchedSchedule_AI

lemma reschedule_required_valid_sched_cur_thread:
  "\<lbrace>(\<lambda>s. target = cur_thread s) and valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked_except target and valid_idle_etcb\<rbrace>
    reschedule_required
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (simp add: valid_sched_def | wp reschedule_required_valid_blocked)+ apply (clarsimp simp: valid_blocked_except_def valid_blocked_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. target = cur_thread s) and valid_etcbs and valid_queues and weak_valid_sched_action and valid_blocked_except target and valid_idle_etcb\<rbrace> reschedule_required \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. target = cur_thread s \<and> valid_etcbs s \<and> valid_queues s \<and> weak_valid_sched_action s \<and> valid_blocked_except target s \<and> valid_idle_etcb s \<Longrightarrow> valid_blocked s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma get_tcb_st_tcb_at:
  "get_tcb t s = Some y \<Longrightarrow> st_tcb_at \<top> t s" apply (simp add: get_tcb_def pred_tcb_at_def obj_at_def
              split: option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb t s = Some y \<Longrightarrow> st_tcb_at (\<lambda>_. True) t s proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma st_tcb_at_kh_if_split:
  "st_tcb_at_kh P ptr (\<lambda>t. if t = ref then x else kh t)
     = (if ptr = ref then (\<exists>tcb. x = Some (TCB tcb) \<and> P (tcb_state tcb))
        else st_tcb_at_kh P ptr kh)" by (fastforce simp: st_tcb_at_kh_def obj_at_kh_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at_kh P ptr (\<lambda>t. if t = ref then x else kh t) = (if ptr = ref then \<exists>tcb. x = Some (TCB tcb) \<and> P (tcb_state tcb) else st_tcb_at_kh P ptr kh)
theory DetSchedSchedule_AI

lemma set_thread_state_valid_etcbs[wp]:
  "\<lbrace>valid_etcbs\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: set_thread_state_def) apply (wp | wpc | simp add: set_thread_state_ext_def set_object_def get_object_def)+ apply (fastforce simp: valid_etcbs_def st_tcb_at_kh_if_split
                   dest: get_tcb_st_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> set_thread_state ref ts \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do tcb <- gets_the (get_tcb ref);
y <- set_object ref (TCB (tcb\<lparr>tcb_state := ts\<rparr>));
set_thread_state_ext ref
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<Longrightarrow> (\<exists>y. get_tcb ref s = Some y) \<longrightarrow> (\<exists>y. kheap s ref = Some y) \<longrightarrow> a_type (the (kheap s ref)) = ATCB \<longrightarrow> valid_etcbs_2 (ekheap s) (\<lambda>a. if a = ref then Some (TCB (the (get_tcb ref s)\<lparr>tcb_state := ts\<rparr>)) else kheap s a) proof (prove)
goal:
No subgoals!