theory Scheduler_IF

lemma reschedule_required_reads_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l (pas_refined aag and valid_queues and valid_etcbs
                                                         and valid_sched_action)
                                  reschedule_required" apply (rule reads_respects_scheduler_cases') apply (simp add: reschedule_required_def) apply (wp | wpc)+ apply clarsimp apply (rule reads_respects_scheduler_unobservable'') apply (wp | simp | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) reschedule_required proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' reschedule_required
 2. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P' s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' reschedule_required
 4. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (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)
 2. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P' s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' reschedule_required
 4. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s \<and> ((scheduler_action s = resume_cur_thread \<longrightarrow> True) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> pas_refined aag s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> True)) \<and> True
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' reschedule_required
 3. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' reschedule_required
 2. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrace>?P40 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> reschedule_required \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>?P'40 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> reschedule_required \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. ?P'' s \<Longrightarrow> ?P40 s \<and> ?P'40 s
 4. \<And>s. \<lbrakk>(pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal:
No subgoals!