theory Scheduler_IF

lemma read_respects_scheduler_switch_thread_case:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_scheduler aag l
       (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t)
             and valid_sched_action and pas_refined aag)
       (do tcb_sched_action tcb_sched_enqueue t;
           set_scheduler_action choose_new_thread;
           schedule_choose_new_thread
        od)" unfolding schedule_choose_new_thread_def apply (rule equiv_valid_guard_imp) apply simp apply (rule bind_ev) apply (rule bind_ev) apply (rule next_domain_snippit[OF domains_distinct]) apply wp[1] apply (simp add: pred_conj_def) apply (rule hoare_vcg_conj_lift) apply (rule set_scheduler_action_extended.invs) apply (wp tcb_action_reads_respects_scheduler)+ apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) (do tcb_sched_action tcb_sched_enqueue t;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) (do tcb_sched_action tcb_sched_enqueue t;
set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q (do tcb_sched_action tcb_sched_enqueue t;
set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
when (dom_time = 0) next_domain;
choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q (do y <- tcb_sched_action tcb_sched_enqueue t;
y <- set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q3 rv) (do y <- set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 3. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>?Q3\<rbrace>
 4. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (6 subgoals):
 1. \<And>rv rva. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?Q7 rv rva) (do dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (set_scheduler_action choose_new_thread)
 3. \<And>rv. \<lbrace>?P''7 rv\<rbrace> set_scheduler_action choose_new_thread \<lbrace>?Q7 rv\<rbrace>
 4. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 5. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 6. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. \<And>rv. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P'7 rv) (set_scheduler_action choose_new_thread)
 2. \<And>rv. \<lbrace>?P''7 rv\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rva. invs and pas_refined aag and valid_queues\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 4. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. ?P'7 rv s \<and> ?P''7 rv s\<rbrace>
 5. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrace>?P''7 rv\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rva. invs and pas_refined aag and valid_queues\<rbrace>
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 3. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. True \<and> ?P''7 rv s\<rbrace>
 4. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P''7 ()\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rva x. invs x \<and> pas_refined aag x \<and> valid_queues x\<rbrace>
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 3. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. True \<and> ?P''7 rv s\<rbrace>
 4. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P17 ()\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<lbrace>?P'16 ()\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. pas_refined aag s \<and> valid_queues s\<rbrace>
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 4. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. True \<and> ?P17 rv s \<and> ?P'16 rv s\<rbrace>
 5. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'16 ()\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv s. pas_refined aag s \<and> valid_queues s\<rbrace>
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'3 (tcb_sched_action tcb_sched_enqueue t)
 3. \<lbrace>?P''3\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>rv s. True \<and> invs s \<and> ?P'16 rv s\<rbrace>
 4. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_queues and (\<lambda>s. scheduler_action s = switch_thread t) and valid_sched_action and pas_refined aag) s \<Longrightarrow> pas_refined aag s \<and> True \<and> invs s \<and> pas_refined aag s \<and> (valid_queues and st_tcb_at runnable t) s proof (prove)
goal:
No subgoals!