kings-crown/FVELER_Isabelle huggingface dataset:
theory Scheduler_IF

lemma schedule_choose_new_thread_read_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues)
                                  schedule_choose_new_thread" unfolding schedule_choose_new_thread_def by (simp add: next_domain_snippit[OF domains_distinct])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_queues) schedule_choose_new_thread proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_queues) (do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od)
theory Scheduler_IF

lemma switch_to_cur_domain:
  "\<lbrakk> valid_sched s; scheduler_action s = switch_thread x; pas_refined aag s \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)" apply (clarsimp simp: valid_sched_def valid_sched_action_def switch_in_cur_domain_def
                        in_cur_domain_def etcb_at_def weak_valid_sched_action_def
                        is_etcb_at_def st_tcb_at_def obj_at_def valid_etcbs_def) apply (drule_tac x=x in spec) apply clarsimp apply (drule(1) tcb_domain_wellformed) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_sched s; scheduler_action s = switch_thread x; pas_refined aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread x; pas_refined aag s; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s x = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread x; pas_refined aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s x = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>scheduler_action s = switch_thread x; pas_refined aag s; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); tcb_domain y = cur_domain s; kheap s x = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); ekheap s x = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>scheduler_action s = switch_thread x; valid_queues s; ct_not_in_q_2 (ready_queues s) (switch_thread x) (cur_thread s); tcb_domain y = cur_domain s; kheap s x = Some (TCB tcb); valid_blocked_2 (ready_queues s) (kheap s) (switch_thread x) (cur_thread s); valid_idle_etcb s; runnable (tcb_state tcb); ekheap s x = Some y; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain y)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma equiv_valid_dc:
  assumes a: "\<And>P. f \<lbrace>P\<rbrace>"
  assumes b: "\<And>P. f' \<lbrace>P\<rbrace>"
  shows "equiv_valid_2 I A A dc P P' f f'" apply (clarsimp simp add: equiv_valid_2_def) apply (erule use_valid[OF _ a]) apply (erule use_valid[OF _ b]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A dc P P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); (aa, ba) \<in> fst (f' t); P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(aa, ba) \<in> fst (f' t); P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s ba \<and> A s ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma equiv_valid_2:
  "equiv_valid I A B P f \<Longrightarrow> equiv_valid_rv I A B (=) P f" by (simp add: equiv_valid_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid_rv I A B (=) P f
theory Scheduler_IF

lemma ev_gets_const:
  "equiv_valid_inv I A (\<lambda>s. f s = x) (gets f)" by (clarsimp simp: equiv_valid_def2 equiv_valid_2_def gets_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. f s = x) (gets f)
theory Scheduler_IF

lemma when_next_domain_domain_fields:
  "\<lbrace>\<lambda>s. \<not> B \<and> domain_fields Q s\<rbrace>
   when B next_domain
   \<lbrace>\<lambda>_. domain_fields Q\<rbrace>" by (wpsimp | rule hoare_pre_cont[where f=next_domain])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> B \<and> Q (domain_time s) (domain_index s) (domain_list s)\<rbrace> when B next_domain \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
theory Scheduler_IF

lemma cur_thread_cur_domain:
  "\<lbrakk> st_tcb_at ((=) st) (cur_thread s) s; \<not> idle st; invs s; guarded_pas_domain aag s \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)" by (clarsimp simp: pred_tcb_at_def invs_def valid_idle_def
                     valid_state_def obj_at_def guarded_pas_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at ((=) st) (cur_thread s) s; st \<noteq> IdleThreadState; invs s; guarded_pas_domain aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)
theory Scheduler_IF

lemma valid_sched_valid_queues[intro]:
  "valid_sched s \<Longrightarrow> valid_queues s" by (simp add: valid_sched_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s \<Longrightarrow> valid_queues s
theory Scheduler_IF

lemma ethread_get_wp2:
  "\<lbrace>\<lambda>s. \<forall>etcb. etcb_at ((=) etcb) t s \<longrightarrow> Q (f etcb) s\<rbrace>
   ethread_get f t
   \<lbrace>Q\<rbrace>" apply wp apply (clarsimp simp: etcb_at_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>etcb. etcb_at ((=) etcb) t s \<longrightarrow> Q (f etcb) s\<rbrace> ethread_get f t \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>etcb. etcb_at ((=) etcb) t s \<longrightarrow> Q (f etcb) s \<Longrightarrow> etcb_at (\<lambda>t. Q (f t) s) t s proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma switch_thread_runnable:
  "\<lbrakk> valid_sched s; scheduler_action s = switch_thread t \<rbrakk>
     \<Longrightarrow> st_tcb_at runnable t s" unfolding valid_sched_def valid_sched_action_def weak_valid_sched_action_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_sched s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at runnable t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> (is_activatable (cur_thread s) s \<and> (\<forall>t. scheduler_action s = switch_thread t \<longrightarrow> st_tcb_at_kh runnable t (kheap s)) \<and> switch_in_cur_domain s) \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s; scheduler_action s = switch_thread t\<rbrakk> \<Longrightarrow> st_tcb_at runnable t s
theory Scheduler_IF

lemma gets_highest_prio_ev_from_weak_sae:
  "(\<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t)
   \<Longrightarrow> equiv_valid_inv R B (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {})
                       (gets (\<lambda>s. is_highest_prio d p s))" apply (simp add: is_highest_prio_def) apply (erule gets_read_queue_ev_from_weak_sae) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t \<Longrightarrow> equiv_valid_inv R B (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (is_highest_prio d p)) proof (prove)
goal (1 subgoal):
 1. \<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t \<Longrightarrow> equiv_valid_inv R B (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. (\<forall>prio. ready_queues s d prio = []) \<or> Max {prio. ready_queues s d prio \<noteq> []} \<le> p)) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma etcb_in_domains_of_state:
  "\<lbrakk> is_etcb_at tcb_ptr s; etcb_at (\<lambda>t. tcb_domain t = tcb_dom) tcb_ptr s \<rbrakk>
     \<Longrightarrow> (tcb_ptr, tcb_dom) \<in> domains_of_state s" by (auto simp: domains_of_state_aux.simps is_etcb_at_def etcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_etcb_at tcb_ptr s; etcb_at (\<lambda>t. tcb_domain t = tcb_dom) tcb_ptr s\<rbrakk> \<Longrightarrow> (tcb_ptr, tcb_dom) \<in> domains_of_state s
theory Scheduler_IF

lemma guarded_active_ct_cur_domain:
  "\<lbrakk> guarded_pas_domain aag s; ct_active s; invs s \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)" by (fastforce simp: guarded_pas_domain_def invs_def valid_state_def
                      valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guarded_pas_domain aag s; ct_active s; invs s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)
theory Scheduler_IF

lemma set_scheduler_action_unobservable:
  "\<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st
                                               and (\<lambda>s. cur_domain st = cur_domain s)\<rbrace>
   set_scheduler_action a
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: set_scheduler_action_def) apply wp apply (clarsimp simp: scheduler_affects_equiv_def scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s)\<rbrace> set_scheduler_action a \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s)\<rbrace> modify (scheduler_action_update (\<lambda>_. a)) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s)) s \<Longrightarrow> scheduler_affects_equiv aag l st (scheduler_action_update (\<lambda>_. a) s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma sched_equiv_cur_domain[intro]:
  "scheduler_equiv aag st s \<Longrightarrow> cur_domain st = cur_domain s" by (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_equiv aag st s \<Longrightarrow> cur_domain st = cur_domain s
theory Scheduler_IF

lemma reschedule_required_scheduler_equiv[wp]:
  "reschedule_required \<lbrace>scheduler_equiv aag st\<rbrace>" apply (simp add: reschedule_required_def) apply (wp scheduler_equiv_lift | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_equiv aag st\<rbrace> reschedule_required \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_equiv aag st\<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>_. scheduler_equiv aag st\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma dec_domain_time_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l \<top> dec_domain_time" apply (simp add: dec_domain_time_def) apply (wp ev_modify) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
                        scheduler_globals_frame_equiv_def silc_dom_equiv_def states_equiv_for_def
                        scheduler_affects_equiv_def equiv_for_def equiv_asids_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) dec_domain_time proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (modify (\<lambda>s. domain_time_update (\<lambda>_. domain_time s - 1) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; True; scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag (domain_time_update (\<lambda>_. domain_time s - 1) s) (domain_time_update (\<lambda>_. domain_time t - 1) t) \<and> scheduler_affects_equiv aag l (domain_time_update (\<lambda>_. domain_time s - 1) s) (domain_time_update (\<lambda>_. domain_time t - 1) t) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma schedule_choose_new_thread_schedule_affects_no_switch:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "\<lbrace>\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s \<and> domain_time s \<noteq> 0
                 \<and> \<not> reads_scheduler_cur_domain aag l s \<and> scheduler_equiv aag st s
                 \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s\<rbrace>
     schedule_choose_new_thread
     \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" unfolding schedule_choose_new_thread_def by (wpsimp wp: set_scheduler_action_unobservable choose_thread_unobservable
                 hoare_pre_cont[where f=next_domain])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
theory Scheduler_IF

lemma switch_to_cur_domain':
  "\<lbrakk> valid_etcbs s; valid_sched_action s; scheduler_action s = switch_thread x; pas_refined aag s \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)" apply (clarsimp simp: valid_sched_def valid_sched_action_def switch_in_cur_domain_def
                        in_cur_domain_def etcb_at_def weak_valid_sched_action_def
                        is_etcb_at_def st_tcb_at_def obj_at_def valid_etcbs_def) apply (drule_tac x=x in spec) apply clarsimp apply (drule (1) tcb_domain_wellformed) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s; valid_sched_action s; scheduler_action s = switch_thread x; pas_refined aag s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); scheduler_action s = switch_thread x; pas_refined aag s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s x = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>scheduler_action s = switch_thread x; pas_refined aag s; case ekheap s x of None \<Rightarrow> True | Some x \<Rightarrow> tcb_domain x = cur_domain s; kheap s x = Some (TCB tcb); runnable (tcb_state tcb); (\<exists>ko. kheap s x = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s x = Some y)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>scheduler_action s = switch_thread x; pas_refined aag s; tcb_domain y = cur_domain s; kheap s x = Some (TCB tcb); runnable (tcb_state tcb); ekheap s x = Some y\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>tcb y. \<lbrakk>scheduler_action s = switch_thread x; tcb_domain y = cur_domain s; kheap s x = Some (TCB tcb); runnable (tcb_state tcb); ekheap s x = Some y; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain y)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma ethread_set_time_slice_valid_queues[wp]:
  "ethread_set (tcb_time_slice_update f) t \<lbrace>valid_queues\<rbrace>" apply (simp add: ethread_set_def set_eobject_def) apply wp apply (clarsimp simp: get_etcb_def valid_sched_def valid_etcbs_def is_etcb_at_def valid_queues_def
                        etcb_at'_def valid_sched_action_def weak_valid_sched_action_def
                        switch_in_cur_domain_def ct_in_cur_domain_def in_cur_domain_def) apply (intro impI conjI allI ballI) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> ethread_set (tcb_time_slice_update f) t \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> do tcb <- gets_the (get_etcb t);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(t \<mapsto> tcb_time_slice_update f tcb)) es)
od \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues s \<Longrightarrow> get_etcb t s \<noteq> None \<longrightarrow> valid_queues (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> tcb_time_slice_update f (the (get_etcb t s)))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s y d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); ekheap s t = Some y; t \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> tcb_priority y = p \<and> tcb_domain y = d proof (prove)
goal (2 subgoals):
 1. \<And>s y d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); ekheap s t = Some y; t \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> tcb_priority y = p
 2. \<And>s y d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues s d p). (\<exists>y. ekheap s t = Some y) \<and> (case ekheap s t of None \<Rightarrow> True | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); ekheap s t = Some y; t \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> tcb_domain y = d proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma ethread_set_time_slice_valid_sched_action[wp]:
  "ethread_set (tcb_time_slice_update f) t \<lbrace>valid_sched_action\<rbrace>" apply (simp add: ethread_set_def set_eobject_def) apply wp apply (clarsimp simp: get_etcb_def valid_sched_def valid_etcbs_def is_etcb_at_def valid_queues_def
                        etcb_at'_def valid_sched_action_def weak_valid_sched_action_def
                        switch_in_cur_domain_def ct_in_cur_domain_def in_cur_domain_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> ethread_set (tcb_time_slice_update f) t \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> do tcb <- gets_the (get_etcb t);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(t \<mapsto> tcb_time_slice_update f tcb)) es)
od \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_sched_action s \<Longrightarrow> get_etcb t s \<noteq> None \<longrightarrow> valid_sched_action (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> tcb_time_slice_update f (the (get_etcb t s)))) s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma dec_domain_time_valid_queues[wp]:
  "dec_domain_time \<lbrace>valid_queues\<rbrace>" apply (simp add: dec_domain_time_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> modify (\<lambda>s. domain_time_update (\<lambda>_. domain_time s - 1) s) \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma dec_domain_time_valid_etcbs[wp]:
  "dec_domain_time \<lbrace>valid_etcbs\<rbrace>" apply (simp add: dec_domain_time_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> modify (\<lambda>s. domain_time_update (\<lambda>_. domain_time s - 1) s) \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma dec_domain_time_valid_sched_action[wp]:
  "dec_domain_time \<lbrace>valid_sched_action\<rbrace>" apply (simp add: dec_domain_time_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> modify (\<lambda>s. domain_time_update (\<lambda>_. domain_time s - 1) s) \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal:
No subgoals!