theory Scheduler_IF

lemma choose_thread_reads_respects_scheduler_cur_domain:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "midstrength_reads_respects_scheduler aag l
           (invs and pas_refined aag and valid_queues
                 and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l \<noteq> {}))
           (choose_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))" apply (simp add: choose_thread_def bind_assoc) apply (rule equiv_valid_guard_imp) apply (rule bind_ev_general) apply (rule bind_ev_general) apply (rule if_ev_bind) apply (rule switch_to_idle_thread_midstrength_reads_respects_scheduler) apply (rule guarded_switch_to_thread_midstrength_reads_respects_scheduler) apply wp+ apply clarsimp apply (erule any_valid_thread) apply (frule(1) tcb_with_domain_at) apply clarsimp apply (frule(1) tcb_domain_wellformed) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
_ <- if \<forall>prio. x prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue x));
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q (do x <- gets cur_domain;
x <- gets (\<lambda>s. ready_queues s x);
_ <- if \<forall>prio. x prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue x));
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (scheduler_affects_equiv aag l) (?Q3 rv) (do x <- gets (\<lambda>s. ready_queues s rv);
_ <- if \<forall>prio. x prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue x));
set_scheduler_action resume_cur_thread
od)
 2. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets cur_domain)
 3. \<lbrace>?P''3\<rbrace> gets cur_domain \<lbrace>?Q3\<rbrace>
 4. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. equiv_valid (scheduler_equiv aag) (?B7 rv) (scheduler_affects_equiv aag l) (?Q7 rv rva) (do _ <- if \<forall>prio. rva prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue rva));
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (?B7 rv) (?P'7 rv) (gets (\<lambda>s. ready_queues s rv))
 3. \<And>rv. \<lbrace>?P''7 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>?Q7 rv\<rbrace>
 4. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets cur_domain)
 5. \<lbrace>?P''3\<rbrace> gets cur_domain \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (7 subgoals):
 1. \<And>rv rva. \<forall>prio. rva prio = [] \<Longrightarrow> equiv_valid (scheduler_equiv aag) (?B7 rv) (scheduler_affects_equiv aag l) (?P11 rv rva) (do _ <- switch_to_idle_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv rva. \<not> (\<forall>prio. rva prio = []) \<Longrightarrow> equiv_valid (scheduler_equiv aag) (?B7 rv) (scheduler_affects_equiv aag l) (?Q11 rv rva) (do _ <- guarded_switch_to (hd (max_non_empty_queue rva));
set_scheduler_action resume_cur_thread
od)
 3. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (?B7 rv) (?P'7 rv) (gets (\<lambda>s. ready_queues s rv))
 4. \<And>rv. \<lbrace>?P''7 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>rva s. ((\<forall>prio. rva prio = []) \<longrightarrow> ?P11 rv rva s) \<and> (\<not> (\<forall>prio. rva prio = []) \<longrightarrow> ?Q11 rv rva s)\<rbrace>
 5. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets cur_domain)
 6. \<lbrace>?P''3\<rbrace> gets cur_domain \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 7. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<not> (\<forall>prio. rva prio = []) \<Longrightarrow> midstrength_reads_respects_scheduler aag l (?Q11 rv rva) (do _ <- guarded_switch_to (hd (max_non_empty_queue rva));
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (midstrength_scheduler_affects_equiv aag l) (?P'7 rv) (gets (\<lambda>s. ready_queues s rv))
 3. \<And>rv. \<lbrace>?P''7 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>rva s. ((\<forall>prio. rva prio = []) \<longrightarrow> (invs and pas_refined aag) s) \<and> (\<not> (\<forall>prio. rva prio = []) \<longrightarrow> ?Q11 rv rva s)\<rbrace>
 4. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets cur_domain)
 5. \<lbrace>?P''3\<rbrace> gets cur_domain \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. \<not> (\<forall>prio. rva prio = []) \<Longrightarrow> pas_domains_distinct aag
 2. \<And>rv. equiv_valid (scheduler_equiv aag) ?B3 (midstrength_scheduler_affects_equiv aag l) (?P'7 rv) (gets (\<lambda>s. ready_queues s rv))
 3. \<And>rv. \<lbrace>?P''7 rv\<rbrace> gets (\<lambda>s. ready_queues s rv) \<lbrace>\<lambda>rva s. ((\<forall>prio. rva prio = []) \<longrightarrow> (invs and pas_refined aag) s) \<and> (\<not> (\<forall>prio. rva prio = []) \<longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag (hd (max_non_empty_queue rva)) \<in> pasDomainAbs aag (cur_domain s))) s)\<rbrace>
 4. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B3 ?P'3 (gets cur_domain)
 5. \<lbrace>?P''3\<rbrace> gets cur_domain \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 6. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> True \<and> reads_scheduler_cur_domain aag l s \<and> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (invs and pas_refined aag) s) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> (invs and pas_refined aag and (\<lambda>sa. pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain sa))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>invs s; pas_refined aag s; valid_queues s; reads_scheduler_cur_domain aag l s; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio x prioa. \<lbrakk>invs s; pas_refined aag s; valid_queues s; reads_scheduler_cur_domain aag l s; x \<in> set (ready_queues s (cur_domain s) prioa)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s prio x prioa. \<lbrakk>invs s; pas_refined aag s; valid_queues s; reads_scheduler_cur_domain aag l s; x \<in> set (ready_queues s (cur_domain s) prioa); \<exists>t. ekheap s x = Some t \<and> tcb_domain t = cur_domain s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s x prioa t. \<lbrakk>invs s; pas_refined aag s; valid_queues s; reads_scheduler_cur_domain aag l s; x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal (1 subgoal):
 1. \<And>s x prioa t. \<lbrakk>invs s; pas_refined aag s; valid_queues s; reads_scheduler_cur_domain aag l s; x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain t)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s) proof (prove)
goal:
No subgoals!