theory Scheduler_IF

lemma schedule_reads_respects_scheduler:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_scheduler aag l (invs and pas_refined aag and valid_sched
                                          and guarded_pas_domain aag and tick_done) schedule" apply (rule_tac P="\<lambda>s. reads_scheduler_cur_domain aag l s"
               in equiv_valid_cases) apply (rule equiv_valid_guard_imp) apply (rule schedule_reads_respects_scheduler_cur_domain[OF domains_distinct]) apply simp apply (rule_tac P="\<lambda>s. domain_time s = 0" in equiv_valid_cases) apply (rule equiv_valid_guard_imp) apply (rule reads_respects_scheduler_invisible_domain_switch[OF domains_distinct]) apply (clarsimp simp: tick_done_def valid_sched_def) apply (rule equiv_valid_guard_imp) apply (rule reads_respects_scheduler_invisible_no_domain_switch[OF domains_distinct]) apply simp apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done) schedule proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done and reads_scheduler_cur_domain aag l) schedule
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done)) schedule
 3. \<And>s t. \<lbrakk>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) ?Q1 schedule
 2. \<And>s. (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?Q1 s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done)) schedule
 4. \<And>s t. \<lbrakk>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_sched and guarded_pas_domain aag and tick_done and reads_scheduler_cur_domain aag l) s \<Longrightarrow> (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and reads_scheduler_cur_domain aag l) s
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done)) schedule
 3. \<And>s t. \<lbrakk>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. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done)) schedule
 2. \<And>s t. \<lbrakk>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) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done) and (\<lambda>s. domain_time s = 0)) schedule
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) schedule
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 4. \<And>s t. \<lbrakk>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 (5 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q7 schedule
 2. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done) and (\<lambda>s. domain_time s = 0)) s \<Longrightarrow> ?Q7 s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) schedule
 4. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 5. \<And>s t. \<lbrakk>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. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done) and (\<lambda>s. domain_time s = 0)) s \<Longrightarrow> pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> \<not> reads_scheduler_cur_domain aag l s
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) schedule
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 4. \<And>s t. \<lbrakk>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) ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) schedule
 2. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 3. \<And>s t. \<lbrakk>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) ?Q14 schedule
 2. \<And>s. ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) s \<Longrightarrow> ?Q14 s
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 4. \<And>s t. \<lbrakk>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. ((\<lambda>s. domain_time s \<noteq> 0) and ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (invs and pas_refined aag and valid_sched and guarded_pas_domain aag and tick_done))) s \<Longrightarrow> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s
 2. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 3. \<And>s t. \<lbrakk>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 t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> (domain_time s = 0) = (domain_time t = 0)
 2. \<And>s t. \<lbrakk>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!