theory ArchScheduler_IF

lemma arch_switch_to_thread_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l
     ((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs)
     (arch_switch_to_thread t)" apply (rule reads_respects_scheduler_cases) apply (simp add: arch_switch_to_thread_def) apply wp apply (clarsimp simp: scheduler_equiv_def globals_equiv_scheduler_def) apply (simp add: arch_switch_to_thread_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) (arch_switch_to_thread t) proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (arch_switch_to_thread t)
 2. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P' s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (arch_switch_to_thread t)
 4. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (do y <- set_vm_root t;
do_machine_op clearExMonitor
od)
 2. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P' s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (arch_switch_to_thread t)
 4. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True \<and> True
 2. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (arch_switch_to_thread t)
 3. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (arch_switch_to_thread t)
 2. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (do y <- set_vm_root t;
do_machine_op clearExMonitor
od)
 2. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>((\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)) and invs) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True \<and> True proof (prove)
goal:
No subgoals!