kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_DR

lemma option_set_priority_dcorres_strong:
  "dcorres (dc \<oplus> dc) P Q
        (returnOk ())
        (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> do_extended_op (set_priority obj_id' prio)))" supply option.case_cong[cong] if_cong[cong] apply (clarsimp) apply (case_tac prio') apply (clarsimp simp: liftE_def set_priority_def returnOk_def bind_assoc)+ apply (rule corres_noop) apply (wpsimp wp: reschedule_required_transform possible_switch_to_transform
                     thread_set_priority_transform tcb_sched_action_transform)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P Q (returnOk ()) (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> do_extended_op (set_priority obj_id' prio))) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P Q (returnOk ()) (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> do_extended_op (set_priority obj_id' prio))) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) P Q (returnOk ()) (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> set_priority obj_id' prio)) proof (prove)
goal (2 subgoals):
 1. prio' = None \<Longrightarrow> dcorres (dc \<oplus> dc) P Q (returnOk ()) (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> set_priority obj_id' prio))
 2. \<And>a. prio' = Some a \<Longrightarrow> dcorres (dc \<oplus> dc) P Q (returnOk ()) (liftE (case prio' of None \<Rightarrow> return () | Some (prio, auth) \<Rightarrow> set_priority obj_id' prio)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. prio' = Some (a, b) \<Longrightarrow> dcorres (dc \<oplus> dc) P Q (return (Inr ())) (do x <- tcb_sched_action tcb_sched_dequeue obj_id';
x <- thread_set_priority obj_id' a;
x <- get_thread_state obj_id';
r <- when (runnable x) (do cur <- gets cur_thread;
if obj_id' = cur then reschedule_required else possible_switch_to obj_id'
od);
return (Inr ())
od) proof (prove)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>prio' = Some (a, b); P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> Q s'\<rbrace> do x <- tcb_sched_action tcb_sched_dequeue obj_id';
x <- thread_set_priority obj_id' a;
x <- get_thread_state obj_id';
r <- when (runnable x) (do cur <- gets cur_thread;
if obj_id' = cur then reschedule_required else possible_switch_to obj_id'
od);
return (Inr ())
od \<lbrace>\<lambda>rv s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> (dc \<oplus> dc) (Inr ()) rv\<rbrace>
 2. \<And>a b s. \<lbrakk>prio' = Some (a, b); P s; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> Q s') (do x <- tcb_sched_action tcb_sched_dequeue obj_id';
x <- thread_set_priority obj_id' a;
x <- get_thread_state obj_id';
r <- when (runnable x) (do cur <- gets cur_thread;
if obj_id' = cur then reschedule_required else possible_switch_to obj_id'
od);
return (Inr ())
od) proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma transform_full_intent_set_mcpriority:
  "transform_full_intent ms t (tcb_mcpriority_update f tcb) = transform_full_intent ms t tcb" by (simp add: transform_full_intent_def Let_def get_ipc_buffer_words_def
                get_tcb_message_info_def get_tcb_mrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_full_intent ms t (tcb_mcpriority_update f tcb) = transform_full_intent ms t tcb
theory Tcb_DR

lemma option_set_mcpriority_corres:
  "dcorres (dc \<oplus> dc) \<top> valid_etcbs
    (returnOk ())
    (liftE (case mcp' of None \<Rightarrow> return () | Some (mcp, auth) \<Rightarrow> set_mcpriority t mcp))" apply (cases mcp'; simp add: liftE_def returnOk_def) apply (rule corres_noop; clarsimp) apply (wp set_mcpriority_transform) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) valid_etcbs (returnOk ()) (liftE (case mcp' of None \<Rightarrow> return () | Some (mcp, auth) \<Rightarrow> set_mcpriority t mcp)) proof (prove)
goal (1 subgoal):
 1. \<And>a. mcp' = Some a \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) valid_etcbs (return (Inr ())) (do r <- case a of (mcp, auth) \<Rightarrow> set_mcpriority t mcp;
return (Inr ())
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. mcp' = Some (a, b) \<Longrightarrow> \<lbrace>\<lambda>s'. transform s' = s \<and> valid_etcbs s'\<rbrace> do r <- set_mcpriority t a;
return (Inr ())
od \<lbrace>\<lambda>rv s'. transform s' = s \<and> rv = Inr ()\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s sa. \<lbrakk>mcp' = Some (a, b); transform sa = s \<and> valid_etcbs sa\<rbrakk> \<Longrightarrow> (transform sa = s \<and> valid_etcbs sa) \<and> Inr () = Inr ()
theory Tcb_DR

lemma not_idle_thread_ekheap_update[iff]:
  "not_idle_thread ptr (ekheap_update f s) = not_idle_thread ptr s" by (simp add: not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_idle_thread ptr (ekheap_update f s) = not_idle_thread ptr s
theory Tcb_DR

lemma not_idle_thread_scheduler_action_update[iff]:
  "not_idle_thread ptr (scheduler_action_update f s) = not_idle_thread ptr s" by (simp add: not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_idle_thread ptr (scheduler_action_update f s) = not_idle_thread ptr s
theory Tcb_DR

lemma set_priority_transform: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_priority tptr prio \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (clarsimp simp: set_priority_def ethread_set_def set_eobject_def cong: if_cong |
      wp reschedule_required_transform tcb_sched_action_transform
         possible_switch_to_transform thread_set_priority_transform)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_priority tptr prio \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Tcb_DR

lemma set_mcpriority_valid_cap_fst:
  "\<lbrace>(valid_cap \<circ> fst) caps\<rbrace> set_mcpriority obj_id' new_mcp \<lbrace>\<lambda>rv. (valid_cap \<circ> fst) caps\<rbrace>" by clarsimp wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(valid_cap \<circ> fst) caps\<rbrace> set_mcpriority obj_id' new_mcp \<lbrace>\<lambda>rv. (valid_cap \<circ> fst) caps\<rbrace>
theory Tcb_DR

lemma dcorres_dummy_returnOk_pl':
  "dcorres c P P' (f >>=E (\<lambda>_. returnOk ())) g \<Longrightarrow> dcorres c P P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' (doE _ <- f;
returnOk ()
odE) g \<Longrightarrow> dcorres c P P' f g
theory Tcb_DR

lemma invoke_tcb_corres_suspend:
  "\<lbrakk> t' = tcb_invocation.Suspend obj_id';
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs)
    (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def) apply (rule corres_alternate1) apply (rule corres_bind_ignore_ret_rhs) apply (rule corres_return_dc_rhs) apply (rule corres_guard_imp) apply (rule suspend_corres, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.suspend obj_id' \<sqinter> return ()) (do y <- IpcCancel_A.suspend obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.suspend obj_id') (do y <- IpcCancel_A.suspend obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.suspend obj_id') (do IpcCancel_A.suspend obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.suspend obj_id') (IpcCancel_A.suspend obj_id') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'\<rbrakk> \<Longrightarrow> dcorres dc ?Q7 ?Q'7 (Tcb_D.suspend obj_id') (IpcCancel_A.suspend obj_id')
 2. \<And>s. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'; True\<rbrakk> \<Longrightarrow> ?Q7 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.Suspend obj_id'; t = cdl_tcb_invocation.Suspend obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'7 s proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma invoke_tcb_corres_resume:
  "\<lbrakk> t' = tcb_invocation.Resume obj_id';
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs)
  (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def) apply (rule corres_bind_ignore_ret_rhs) apply (rule corres_return_dc_rhs) apply (rule corres_guard_imp[OF restart_corres],clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Resume obj_id'; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Resume obj_id'; t = cdl_tcb_invocation.Resume obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.restart obj_id') (do y <- Tcb_A.restart obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Resume obj_id'; t = cdl_tcb_invocation.Resume obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.restart obj_id') (do Tcb_A.restart obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.Resume obj_id'; t = cdl_tcb_invocation.Resume obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.restart obj_id') (Tcb_A.restart obj_id') proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma ex_nonz_cap_to_idle_from_invs:
  "invs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s" apply (rule Invariants_AI.idle_no_ex_cap) apply (clarsimp simp: invs_def valid_state_def) apply (clarsimp simp: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s proof (prove)
goal (2 subgoals):
 1. invs s \<Longrightarrow> valid_global_refs s
 2. invs s \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma ex_nonz_cap_implies_normal_tcb:
  "\<lbrakk> invs s; tcb_at t' s; ex_nonz_cap_to t' s \<rbrakk> \<Longrightarrow> not_idle_thread t' s" by (auto simp: ex_nonz_cap_to_idle_from_invs not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t' s; ex_nonz_cap_to t' s\<rbrakk> \<Longrightarrow> not_idle_thread t' s
theory Schedule_DR

lemma allActiveTCBs_corres:
  "dcorres allActiveTCBs_relation \<top> (invs and valid_etcbs) (gets all_active_tcbs) allActiveTCBs" apply (clarsimp simp: allActiveTCBs_def gets_def) apply (clarsimp simp: corres_underlying_def) apply (clarsimp simp: exec_get split_def return_def) apply (clarsimp simp: allActiveTCBs_relation_def) apply (auto simp: getActiveTCBs_subset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres allActiveTCBs_relation (\<lambda>_. True) (invs and valid_etcbs) (gets all_active_tcbs) allActiveTCBs proof (prove)
goal (1 subgoal):
 1. dcorres allActiveTCBs_relation (\<lambda>_. True) (invs and valid_etcbs) (do s <- get;
return (all_active_tcbs s)
od) (do state <- get;
return {x. \<exists>y. getActiveTCB x state = Some y}
od) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>(a, ba) \<in> fst ((do state <- get;
return {x. \<exists>y. getActiveTCB x state = Some y}
od) b); invs b; valid_etcbs b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do s <- get;
return (all_active_tcbs s)
od) (transform b)). case x of (r, t) \<Rightarrow> transform ba = t \<and> allActiveTCBs_relation r a proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>invs b; valid_etcbs b\<rbrakk> \<Longrightarrow> allActiveTCBs_relation (all_active_tcbs (transform b)) {x. \<exists>y. getActiveTCB x b = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>b x y. \<lbrakk>invs b; valid_etcbs b; getActiveTCB x b = Some y\<rbrakk> \<Longrightarrow> x \<in> all_active_tcbs (transform b) proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma dcorres_arch_switch_to_idle_thread_return: "dcorres dc \<top> \<top> (return ()) arch_switch_to_idle_thread" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (rule corres_guard_imp) apply (rule dcorres_gets_all_param) apply (rule dcorres_set_vm_root) by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) arch_switch_to_idle_thread proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (gets idle_thread >>= set_vm_root) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (return ()) (gets idle_thread >>= set_vm_root)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<And>thread. dcorres dc ?Q ?Q' (return ()) (set_vm_root thread)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. True \<Longrightarrow> True
theory Schedule_DR

lemma change_current_domain_same: "\<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" apply (clarsimp simp: change_current_domain_def exs_valid_def bind_def return_def gets_def modify_def put_def fst_def snd_def get_def select_def) apply (rule_tac x="cdl_current_domain s" in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> change_current_domain \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<exists>x. s = s\<lparr>cdl_current_domain := x\<rparr> proof (prove)
goal (1 subgoal):
 1. s = s\<lparr>cdl_current_domain := cdl_current_domain s\<rparr> proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma corrupt_intents_current_thread:
  "cdl_current_thread (corrupt_intents x p s) = cdl_current_thread s" by (simp add: corrupt_intents_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_current_thread (corrupt_intents x p s) = cdl_current_thread s
theory Schedule_DR

lemma set_scheduler_action_dcorres:
   "dcorres dc \<top> \<top> (return ()) (set_scheduler_action sa)" by (clarsimp simp: corres_underlying_def set_scheduler_action_def modify_def get_def put_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (set_scheduler_action sa)
theory Schedule_DR

lemma switch_to_thread_None_dcorres_L:
   "dcorres dc (\<lambda>s. cdl_current_thread s = None) \<top>
               (do _ \<leftarrow> change_current_domain;
                   Schedule_D.switch_to_thread None
                od)
               (return ())" apply (auto simp: Schedule_D.switch_to_thread_def modify_def corres_underlying_def get_def put_def bind_def return_def
                    change_current_domain_def gets_def select_def transform_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. cdl_current_thread s = None) (\<lambda>_. True) (do _ <- change_current_domain;
Schedule_D.switch_to_thread None
od) (return ()) proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma switch_to_thread_None_dcorres:
  "dcorres dc \<top> (\<lambda>s. cur_thread s = idle_thread s)
                (do _ \<leftarrow> change_current_domain;
                    Schedule_D.switch_to_thread None
                 od)
               (return ())" apply (rule_tac Q="\<lambda>s. cdl_current_thread s = None" and Q'="\<top>" in stronger_corres_guard_imp) apply (rule switch_to_thread_None_dcorres_L) apply (clarsimp simp: transform_def transform_current_thread_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>s. cur_thread s = idle_thread s) (do _ <- change_current_domain;
Schedule_D.switch_to_thread None
od) (return ()) proof (prove)
goal (3 subgoals):
 1. dcorres dc (\<lambda>s. cdl_current_thread s = None) (\<lambda>_. True) (do _ <- change_current_domain;
Schedule_D.switch_to_thread None
od) (return ())
 2. \<And>s s'. \<lbrakk>True; cur_thread s' = idle_thread s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> cdl_current_thread s = None
 3. \<And>s s'. \<lbrakk>True; cur_thread s' = idle_thread s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>True; cur_thread s' = idle_thread s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> cdl_current_thread s = None
 2. \<And>s s'. \<lbrakk>True; cur_thread s' = idle_thread s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma change_current_domain_dcorres: "dcorres dc \<top> \<top> change_current_domain next_domain" by (auto simp: corres_underlying_def change_current_domain_def next_domain_def bind_def return_def modify_def Let_def put_def select_def
                    get_def transform_def trans_state_def transform_objects_def transform_cdt_def transform_current_thread_def
                    transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) change_current_domain next_domain
theory Schedule_DR

lemma max_set_not_empty:
  "\<And>x::'a::{linorder,finite}. f x \<noteq> [] \<Longrightarrow> f (Max {x. f x \<noteq> []}) \<noteq> []" apply (rule_tac S="{x. f x \<noteq> []}" in Max_prop) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x. f x \<noteq> [] \<Longrightarrow> f (Max {x. f x \<noteq> []}) \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f x \<noteq> []; Max {x. f x \<noteq> []} \<in> {x. f x \<noteq> []}\<rbrakk> \<Longrightarrow> f (Max {x. f x \<noteq> []}) \<noteq> []
 2. \<And>x. f x \<noteq> [] \<Longrightarrow> {x. f x \<noteq> []} \<noteq> {} proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma next_domain_valid_sched_except_blocked[wp]:
  "\<lbrace> valid_sched_except_blocked and (\<lambda>s. scheduler_action s  = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched_except_blocked \<rbrace>" apply (simp add: next_domain_def Let_def) apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> next_domain \<lbrace>\<lambda>_. valid_sched_except_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_except_blocked and (\<lambda>s. scheduler_action s = choose_new_thread)\<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>_. valid_sched_except_blocked\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma schedule_def_2:
  "Schedule_D.schedule \<equiv> do
     change_current_domain;
     (do
       next_domain \<leftarrow> gets cdl_current_domain;
       threads     \<leftarrow> gets (active_tcbs_in_domain next_domain);
       next_thread \<leftarrow> select threads;
       Schedule_D.switch_to_thread (Some next_thread)
     od \<sqinter> Schedule_D.switch_to_thread None)
   od" unfolding Schedule_D.schedule_def apply (subst alternative_bind_distrib_2, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Schedule_D.schedule \<equiv> do change_current_domain;
do next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od \<sqinter> Schedule_D.switch_to_thread None
od proof (prove)
goal (1 subgoal):
 1. do change_current_domain;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od \<sqinter> do change_current_domain;
Schedule_D.switch_to_thread None
od \<equiv> do change_current_domain;
do next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
Schedule_D.switch_to_thread (Some next_thread)
od \<sqinter> Schedule_D.switch_to_thread None
od proof (prove)
goal:
No subgoals!
theory Schedule_DR

lemma dcorres_If_both:
  "\<lbrakk> dcorres r P P' h m ;
     dcorres r P Q' h n \<rbrakk>
  \<Longrightarrow> dcorres r P (\<lambda>s. if b then P' s else Q' s) h (if b then m else n)" by (case_tac b; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres r P P' h m; dcorres r P Q' h n\<rbrakk> \<Longrightarrow> dcorres r P (\<lambda>s. if b then P' s else Q' s) h (if b then m else n)
theory Schedule_DR

lemma set_scheduler_action_transform:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (clarsimp simp: set_scheduler_action_def etcb_at_def| wp )+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_scheduler_action a \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Schedule_DR

lemma get_tcb_message_info_nextPC [simp]:
  "get_tcb_message_info (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) =
   get_tcb_message_info tcb" by (simp add: get_tcb_message_info_def
                arch_tcb_context_get_def
                msg_info_register_def
                ARM.msgInfoRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb_message_info (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) = get_tcb_message_info tcb
theory Schedule_DR

lemma map_msg_registers_nextPC [simp]:
  "map ((tcb_context tcb)(NextIP := pc)) msg_registers =
   map (tcb_context tcb) msg_registers" by (simp add: msg_registers_def ARM.msgRegisters_def
                upto_enum_red fromEnum_def toEnum_def enum_register)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map ((tcb_context tcb)(NextIP := pc)) msg_registers = map (tcb_context tcb) msg_registers