theory Scheduler_IF

lemma choose_thread_reads_respects_scheduler:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues)
           (choose_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))" apply (rule equiv_valid_cases
                [where P="\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l \<noteq> {}"]) apply (rule equiv_valid_guard_imp) apply (rule choose_thread_reads_respects_scheduler_cur_domain[OF domains_distinct]) apply simp apply (rule equiv_valid_guard_imp) apply (rule midstrength_cur_domain_unobservable) apply (rule equiv_valid_guard_imp) apply (wp choose_thread_reads_respects_scheduler_other_domain | simp)+ apply force apply clarsimp apply (simp add: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (3 subgoals):
 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)
 2. midstrength_reads_respects_scheduler aag l ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 3. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (4 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q4 (do _ <- choose_thread;
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> ?Q4 s
 3. midstrength_reads_respects_scheduler aag l ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 4. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. \<And>s. (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s \<Longrightarrow> (invs and pas_refined aag and valid_queues and reads_scheduler_cur_domain aag l) s
 2. midstrength_reads_respects_scheduler aag l ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 3. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q8 (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) s \<Longrightarrow> ?Q8 s
 3. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P11 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) s \<Longrightarrow> (?P11 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s
 3. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q13 (do _ <- choose_thread;
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. (?P11 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?Q13 s
 3. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) s \<Longrightarrow> (?P11 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s
 4. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. \<And>s. ?P11 s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<Longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}
 2. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) s \<Longrightarrow> (?P11 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s
 3. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_queues)) s \<Longrightarrow> ((\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s) and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s
 2. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>midstrength_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal:
No subgoals!