kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedAux_AI

lemma delete_objects_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> delete_objects a b \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: delete_objects_def) apply (wpsimp simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def do_machine_op_def) apply (simp add: valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> delete_objects a b \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do y <- do_machine_op (freeMemory a b);
modify (detype {a..a + 2 ^ b - 1})
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_etcbs s; ((), x) \<in> fst (freeMemory a b (machine_state s))\<rbrakk> \<Longrightarrow> valid_etcbs_2 (\<lambda>x. if a \<le> x \<and> x \<le> a + 2 ^ b - 1 then None else ekheap s x) (\<lambda>x. if a \<le> x \<and> x \<le> a + 2 ^ b - 1 then None else kheap s x) proof (prove)
goal:
No subgoals!
theory DetSchedAux_AI

lemma delete_objects_valid_blocked[wp]: "\<lbrace>valid_blocked\<rbrace> delete_objects a b \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: delete_objects_def) apply (wpsimp simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def do_machine_op_def) apply (simp add: valid_blocked_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> delete_objects a b \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> do y <- do_machine_op (freeMemory a b);
modify (detype {a..a + 2 ^ b - 1})
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>valid_blocked s; ((), x) \<in> fst (freeMemory a b (machine_state s))\<rbrakk> \<Longrightarrow> valid_blocked_2 (ready_queues s) (\<lambda>x. if a \<le> x \<and> x \<le> a + 2 ^ b - 1 then None else kheap s x) (scheduler_action s) (cur_thread s) proof (prove)
goal:
No subgoals!
theory DetSchedAux_AI

lemma valid_idle_etcb_lift:
  assumes "\<And>P t. \<lbrace>\<lambda>s. etcb_at P t s\<rbrace> f \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>"
  shows "\<lbrace>valid_idle_etcb\<rbrace> f \<lbrace>\<lambda>r. valid_idle_etcb\<rbrace>" apply(simp add: valid_idle_etcb_def) apply(wp assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb\<rbrace> f \<lbrace>\<lambda>r. valid_idle_etcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr\<rbrace> f \<lbrace>\<lambda>r. etcb_at (\<lambda>etcb. tcb_domain etcb = default_domain) idle_thread_ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedAux_AI

lemma ethread_get_when_wp:
  "\<lbrace>\<lambda>s. (b \<longrightarrow> etcb_at (\<lambda>t. P (f t) s) ptr s) \<and> (\<not>b \<longrightarrow> P undefined s)\<rbrace> ethread_get_when b f ptr \<lbrace>P\<rbrace>" unfolding ethread_get_when_def ethread_get_def by (wpsimp simp: etcb_at_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (b \<longrightarrow> etcb_at (\<lambda>t. P (f t) s) ptr s) \<and> (\<not> b \<longrightarrow> P undefined s)\<rbrace> ethread_get_when b f ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (b \<longrightarrow> etcb_at (\<lambda>t. P (f t) s) ptr s) \<and> (\<not> b \<longrightarrow> P undefined s)\<rbrace> if b then do tcb <- gets_the $ get_etcb ptr;
return $ f tcb
od else return undefined \<lbrace>P\<rbrace>
theory ArchDetSchedAux_AI

lemma tcb_sched_action_valid_idle_etcb:
  "\<lbrace>valid_idle_etcb\<rbrace>
     tcb_sched_action foo thread
   \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace>" apply (rule valid_idle_etcb_lift) apply (simp add: tcb_sched_action_def set_tcb_queue_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle_etcb\<rbrace> tcb_sched_action foo thread \<lbrace>\<lambda>_. valid_idle_etcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t. \<lbrace>etcb_at P t\<rbrace> tcb_sched_action foo thread \<lbrace>\<lambda>_. etcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t. \<lbrace>etcb_at P t\<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 foo thread queue else ready_queues es d' p) es)
od \<lbrace>\<lambda>_. etcb_at P t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDetSchedAux_AI

lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]:
  "\<lbrace>\<lambda>s::det_ext state. etcb_at P t s\<rbrace> delete_objects a b \<lbrace>\<lambda>r s. etcb_at P t s\<rbrace>" apply (simp add: delete_objects_def) apply (wp) apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t\<rbrace> delete_objects a b \<lbrace>\<lambda>r. etcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t\<rbrace> do y <- do_machine_op (freeMemory a b);
modify (detype {a..a + 2 ^ b - 1})
od \<lbrace>\<lambda>r. etcb_at P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (freeMemory a b) \<lbrace>\<lambda>y s. etcb_at P t (detype {a..a + 2 ^ b - 1} s)\<rbrace>
 2. \<And>s. etcb_at P t s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchDetSchedAux_AI

lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]:
  "\<lbrace>(\<lambda>s :: det_ext state. etcb_at P t s) and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not o inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>" apply (cases ui) apply (simp add: mapM_x_def[symmetric] invoke_untyped_def whenE_def
           split del: if_split) apply (wp retype_region_etcb_at mapM_x_wp'
            create_cap_no_pred_tcb_at typ_at_pred_tcb_at_lift
            hoare_convert_imp[OF create_cap_no_pred_tcb_at]
            hoare_convert_imp[OF _ init_arch_objects_exst]
      | simp
      | (wp (once) hoare_drop_impE_E))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>etcb_at P t and valid_etcbs\<rbrace> invoke_untyped ui \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x5 x6 x7 x8. ui = Retype x1 x2 x3 x4 x5 x6 x7 x8 \<Longrightarrow> \<lbrace>etcb_at P t and valid_etcbs\<rbrace> doE y <- if x2 then reset_untyped_cap x1 else returnOk ();
liftE (do cap <- get_cap x1;
y <- set_cap (UntypedCap x8 x3 (bits_of cap) (unat (x4 + (word_of_nat (length x7) << obj_bits_api x5 x6) - x3))) x1;
orefs <- retype_region x4 (length x7) x6 x5 x8;
y <- init_arch_objects x5 x4 (length x7) x6 orefs;
mapM_x (create_cap x5 x6 x1 x8) (zip x7 orefs)
od)
odE \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma ethread_get_wp[wp]:
  "\<lbrace>\<lambda>s. etcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> ethread_get f ptr \<lbrace>P\<rbrace>" unfolding ethread_get_def by (wp | clarsimp simp add: get_etcb_def etcb_at'_def is_etcb_at'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. etcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> ethread_get f ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. etcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> do tcb <- gets_the $ get_etcb ptr;
return $ f tcb
od \<lbrace>P\<rbrace>
theory DetSchedDomainTime_AI

lemma rec_del_domain_list[wp]:
  "\<lbrace>\<lambda>s. P (domain_list s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>" by (wp rec_del_preservation preemption_point_inv' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>
theory DetSchedDomainTime_AI

lemma cap_revoke_domain_list_inv[wp]:
  "\<lbrace>(\<lambda>s :: det_ext state. P (domain_list s))\<rbrace> cap_revoke a \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>" by (rule cap_revoke_preservation2)
     (wp preemption_point_inv'|simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> cap_revoke a \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>
theory DetSchedDomainTime_AI

lemma invoke_cnode_domain_list_inv[wp]:
  "\<lbrace>\<lambda>s :: det_ext state. P (domain_list s)\<rbrace>
     invoke_cnode i
   \<lbrace>\<lambda>rv s. P (domain_list s) \<rbrace>" apply (rule hoare_pre) apply (wp crunch_wps cap_move_src_slot_Null hoare_drop_imps hoare_vcg_all_lift
          | wpc | simp add: invoke_cnode_def crunch_simps split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv s. P (domain_list s)\<rbrace>
 2. \<And>s. P (domain_list s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma call_kernel_domain_list_inv_det_ext:
  "\<lbrace> \<lambda>s. P (domain_list s) \<rbrace>
     (call_kernel e) :: (unit,det_ext) s_monad
   \<lbrace>\<lambda>_ s. P (domain_list s) \<rbrace>" unfolding call_kernel_def apply (wp) apply (simp add: schedule_def) apply (wpsimp wp: without_preemption_wp simp: if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> call_kernel e \<lbrace>\<lambda>_ s. P (domain_list s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_list s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. P (domain_list s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?P9 x\<rbrace> without_preemption (do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od) -, \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>
 2. \<And>x. \<lbrace>?P'9 x\<rbrace> without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>, -
 3. \<lbrace>?Q\<rbrace> handle_event e \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>, \<lbrace>\<lambda>x s. ?P9 x s \<and> ?P'9 x s\<rbrace>
 4. \<And>s. P (domain_list s) \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P9 ()\<rbrace> liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od) -, \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>
 2. \<And>x. \<lbrace>?P'9 x\<rbrace> without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>, -
 3. \<lbrace>?Q\<rbrace> handle_event e \<lbrace>\<lambda>x s. P (domain_list s)\<rbrace>, \<lbrace>\<lambda>x s. ?P9 x s \<and> ?P'9 x s\<rbrace>
 4. \<And>s. P (domain_list s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma rec_del_domain_time[wp]:
  "\<lbrace>\<lambda>s. P (domain_time s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>" by (wp rec_del_preservation preemption_point_inv' | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> rec_del call \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>
theory DetSchedDomainTime_AI

lemma cap_revoke_domain_time_inv[wp]:
  "\<lbrace>(\<lambda>s :: det_ext state. P (domain_time s))\<rbrace> cap_revoke a \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>" apply (rule cap_revoke_preservation2) apply (wp preemption_point_inv'|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> cap_revoke a \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> cap_delete p \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>
 2. \<And>s. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> preemption_point \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma invoke_cnode_domain_time_inv[wp]:
  "\<lbrace>\<lambda>s :: det_ext state. P (domain_time s)\<rbrace>
     invoke_cnode i
   \<lbrace>\<lambda>rv s. P (domain_time s) \<rbrace>" apply (rule hoare_pre) apply (wp crunch_wps cap_move_src_slot_Null hoare_drop_imps hoare_vcg_all_lift
          | wpc | simp add: invoke_cnode_def crunch_simps split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (domain_time s)\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv s. P (domain_time s)\<rbrace>
 2. \<And>s. P (domain_time s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma next_domain_domain_time_left[wp]:
  "\<lbrace> valid_domain_list \<rbrace> next_domain \<lbrace>\<lambda>_ s. 0 < domain_time s \<rbrace>" apply (rule hoare_pre) apply (simp add: next_domain_def Let_def) apply wp apply (clarsimp simp: valid_domain_list_def) apply (simp add: all_set_conv_all_nth) apply (erule_tac x="Suc (domain_index s) mod length (domain_list s)" in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list\<rbrace> next_domain \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> next_domain \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>s. valid_domain_list s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> modify (\<lambda>s. trans_state (\<lambda>e. e\<lparr>domain_index_internal := Suc (domain_index s) mod length (domain_list s), cur_domain_internal := fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), domain_time_internal := snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), work_units_completed_internal := 0\<rparr>) s) \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>s. valid_domain_list s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_domain_list s \<Longrightarrow> 0 < domain_time (trans_state (\<lambda>e. e\<lparr>domain_index_internal := Suc (domain_index s) mod length (domain_list s), cur_domain_internal := fst (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), domain_time_internal := snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))), work_units_completed_internal := 0\<rparr>) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_list s \<noteq> []; \<forall>x\<in>set (domain_list s). case x of (d, time) \<Rightarrow> 0 < time\<rbrakk> \<Longrightarrow> 0 < snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_list s \<noteq> []; \<forall>i<length (domain_list s). case domain_list s ! i of (d, x) \<Rightarrow> 0 < x\<rbrakk> \<Longrightarrow> 0 < snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>domain_list s \<noteq> []; Suc (domain_index s) mod length (domain_list s) < length (domain_list s) \<longrightarrow> (case domain_list s ! (Suc (domain_index s) mod length (domain_list s)) of (d, x) \<Rightarrow> 0 < x)\<rbrakk> \<Longrightarrow> 0 < snd (domain_list s ! (Suc (domain_index s) mod length (domain_list s))) proof (prove)
goal:
No subgoals!
theory DetSchedDomainTime_AI

lemma schedule_choose_new_thread_domain_time_left[wp]:
  "\<lbrace> valid_domain_list \<rbrace>
   schedule_choose_new_thread
   \<lbrace>\<lambda>_ s. 0 < domain_time s \<rbrace>" unfolding schedule_choose_new_thread_def by (wpsimp simp: word_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_domain_list\<rbrace> do dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
theory DetSchedDomainTime_AI

lemma reschedule_required_choose_new_thread[wp]:
  "\<lbrace> \<top> \<rbrace> reschedule_required
   \<lbrace>\<lambda>x s. scheduler_action s = choose_new_thread\<rbrace>" unfolding reschedule_required_def set_scheduler_action_def by (wp hoare_vcg_imp_lift | simp | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>x s. scheduler_action s = choose_new_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do action <- gets scheduler_action;
case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
modify (scheduler_action_update (\<lambda>_. choose_new_thread))
od \<lbrace>\<lambda>x s. scheduler_action s = choose_new_thread\<rbrace>
theory DetSchedDomainTime_AI

lemma reschedule_required_valid_domain_time:
  "\<lbrace> \<top> \<rbrace> reschedule_required
   \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>" by (wpsimp wp: hoare_drop_imp reschedule_required_choose_new_thread)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> reschedule_required \<lbrace>\<lambda>x s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>
theory DetSchedSchedule_AI

lemma set_tcb_queue_wp[wp]: "\<lbrace>\<lambda>s. P (ready_queues_update (\<lambda>_ t' p. if t' = t \<and> p = prio then queue else ready_queues s t' p) s)\<rbrace> set_tcb_queue t prio queue \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: set_tcb_queue_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues_update (\<lambda>_ t' p. if t' = t \<and> p = prio then queue else ready_queues s t' p) s)\<rbrace> set_tcb_queue t prio queue \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues_update (\<lambda>_ t' p. if t' = t \<and> p = prio then queue else ready_queues s t' p) s)\<rbrace> modify (\<lambda>es. ready_queues_update (\<lambda>_ d' p. if d' = t \<and> p = prio then queue else ready_queues es d' p) es) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma get_tcb_queue_wp[wp]: "\<lbrace>\<lambda>s. P (ready_queues s t p) s\<rbrace> get_tcb_queue t p \<lbrace>P\<rbrace>" apply (simp add: get_tcb_queue_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues s t p) s\<rbrace> get_tcb_queue t p \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ready_queues s t p) s\<rbrace> do queues <- gets ready_queues;
return (queues t p)
od \<lbrace>P\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma enqueue_distinct[intro!]: "distinct queue \<Longrightarrow> distinct (tcb_sched_enqueue thread queue)" apply (simp add: tcb_sched_enqueue_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct queue \<Longrightarrow> distinct (tcb_sched_enqueue thread queue) proof (prove)
goal:
No subgoals!
theory DetSchedSchedule_AI

lemma is_activatable_trivs[iff]:
  "is_activatable_2 ct (switch_thread t) kh"
  "is_activatable_2 ct choose_new_thread kh" by (simp_all add: is_activatable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_activatable_2 ct (switch_thread t) kh &&& is_activatable_2 ct choose_new_thread kh
theory DetSchedSchedule_AI

lemma weak_valid_sched_action_trivs[iff]:
  "weak_valid_sched_action_2 resume_cur_thread ekh kh"
  "weak_valid_sched_action_2 choose_new_thread ekh kh" by (simp_all add: weak_valid_sched_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_valid_sched_action_2 resume_cur_thread ekh kh &&& weak_valid_sched_action_2 choose_new_thread ekh kh
theory DetSchedSchedule_AI

lemma switch_in_cur_domain_trivs[iff]:
  "switch_in_cur_domain_2 resume_cur_thread ekh cdom"
  "switch_in_cur_domain_2 choose_new_thread ekh cdom" by (simp_all add: switch_in_cur_domain_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. switch_in_cur_domain_2 resume_cur_thread ekh cdom &&& switch_in_cur_domain_2 choose_new_thread ekh cdom
theory DetSchedSchedule_AI

lemma ct_in_cur_domain_2_trivs[iff]:
  "ct_in_cur_domain_2 thread thread' (switch_thread t) cdom ekh"
  "ct_in_cur_domain_2 thread thread' choose_new_thread cdom ekh" by (simp_all add: ct_in_cur_domain_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_cur_domain_2 thread thread' (switch_thread t) cdom ekh &&& ct_in_cur_domain_2 thread thread' choose_new_thread cdom ekh
theory DetSchedSchedule_AI

lemma valid_sched_action_triv[iff]:
  "valid_sched_action_2 choose_new_thread ekh kh ct cdom" by (simp add: valid_sched_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched_action_2 choose_new_thread ekh kh ct cdom
theory DetSchedSchedule_AI

lemma simple_sched_action_trivs[iff]:
  "simple_sched_action_2 resume_cur_thread"
  "simple_sched_action_2 choose_new_thread" by (simp_all add: simple_sched_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_sched_action_2 resume_cur_thread &&& simple_sched_action_2 choose_new_thread
theory DetSchedSchedule_AI

lemma scheduler_act_not_trivs[iff]:
  "scheduler_act_not_2 resume_cur_thread t"
  "scheduler_act_not_2 choose_new_thread t" by (simp_all add: scheduler_act_not_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_act_not_2 resume_cur_thread t &&& scheduler_act_not_2 choose_new_thread t
theory DetSchedSchedule_AI

lemma tcb_sched_action_enqueue_valid_queues[wp]:
  "\<lbrace>valid_queues and st_tcb_at runnable thread\<rbrace>
     tcb_sched_action tcb_sched_enqueue thread \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply simp apply (clarsimp simp: valid_queues_def2 etcb_at_def tcb_sched_enqueue_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_enqueue 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_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 (1 subgoal):
 1. \<And>s. valid_queues s \<and> st_tcb_at runnable thread s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. valid_queues_2 (\<lambda>a b. if a = tcb_domain t \<and> b = tcb_priority ta then tcb_sched_enqueue thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s a b) (ekheap s) (kheap s)) thread s) thread s proof (prove)
goal:
No subgoals!