theory Scheduler_IF

lemma context_update_cur_thread_snippit:
  "equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l)
     (scheduler_affects_equiv aag l) (=)
     (invs and silc_inv aag st and guarded_pas_domain aag
           and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')
           and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s))
     (invs and silc_inv aag st and guarded_pas_domain aag
           and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc')
           and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s))
     (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)))
     (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))" apply (insert context_update_cur_thread_snippit_cur_domain[where l=l and uc=uc and st=st]) apply (insert context_update_cur_thread_snippit_unobservable[where l=l and uc=uc and uc'=uc' and st=st]) apply (clarsimp simp: equiv_valid_2_def equiv_valid_def2) apply (drule_tac x=s in spec) apply (drule_tac x=s in spec) apply (drule_tac x=t in spec) apply (drule_tac x=t in spec) apply clarsimp apply (subgoal_tac "reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s") apply clarsimp apply (case_tac "reads_scheduler_cur_domain aag l s") apply (fastforce+)[2] apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))); equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc')))\<rbrakk> \<Longrightarrow> equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) (=) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s)) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>\<forall>s t. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<and> reads_scheduler_cur_domain aag l t \<and> invs t \<and> silc_inv aag st t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<and> guarded_pas_domain aag t \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); \<forall>s t. invs s \<and> silc_inv aag st s \<and> guarded_pas_domain aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> invs t \<and> silc_inv aag st t \<and> guarded_pas_domain aag t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> (ct_idle t \<longrightarrow> uc' = idle_context t) \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); ((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>\<forall>s t. invs s \<and> silc_inv aag st s \<and> guarded_pas_domain aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> invs t \<and> silc_inv aag st t \<and> guarded_pas_domain aag t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> (ct_idle t \<longrightarrow> uc' = idle_context t) \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); ((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; \<forall>t. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<and> reads_scheduler_cur_domain aag l t \<and> invs t \<and> silc_inv aag st t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<and> guarded_pas_domain aag t \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; \<forall>t. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<and> reads_scheduler_cur_domain aag l t \<and> invs t \<and> silc_inv aag st t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<and> guarded_pas_domain aag t \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); \<forall>t. invs s \<and> silc_inv aag st s \<and> guarded_pas_domain aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> invs t \<and> silc_inv aag st t \<and> guarded_pas_domain aag t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> (ct_idle t \<longrightarrow> uc' = idle_context t) \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; \<forall>t. invs s \<and> silc_inv aag st s \<and> guarded_pas_domain aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> invs t \<and> silc_inv aag st t \<and> guarded_pas_domain aag t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> (ct_idle t \<longrightarrow> uc' = idle_context t) \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<and> reads_scheduler_cur_domain aag l t \<and> invs t \<and> silc_inv aag st t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<and> guarded_pas_domain aag t \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<and> reads_scheduler_cur_domain aag l t \<and> invs t \<and> silc_inv aag st t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<and> guarded_pas_domain aag t \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); invs s \<and> silc_inv aag st s \<and> guarded_pas_domain aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> invs t \<and> silc_inv aag st t \<and> guarded_pas_domain aag t \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<and> (ct_idle t \<longrightarrow> uc' = idle_context t) \<and> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba
 2. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); (pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}) = (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba
 2. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s proof (prove)
goal (3 subgoals):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); (pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}) = (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}); reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba
 2. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); (pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {}) = (pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}); \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> scheduler_equiv aag b ba \<and> scheduler_affects_equiv aag l b ba
 3. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s proof (prove)
goal (1 subgoal):
 1. \<And>s t b ba. \<lbrakk>((), b) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s); ((), ba) \<in> fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t); invs s; silc_inv aag st s; guarded_pas_domain aag s; reads_scheduler_cur_domain aag l s \<longrightarrow> uc = uc'; ct_idle s \<longrightarrow> uc = idle_context s; invs t; silc_inv aag st t; guarded_pas_domain aag t; reads_scheduler_cur_domain aag l t \<longrightarrow> uc = uc'; ct_idle t \<longrightarrow> uc' = idle_context t; scheduler_equiv aag s t; scheduler_affects_equiv aag l s t; reads_scheduler_cur_domain aag l s \<and> reads_scheduler_cur_domain aag l t \<and> (ct_idle t \<longrightarrow> uc = idle_context t) \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t'); pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasDomainAbs aag (cur_domain t) \<inter> reads_scheduler aag l = {} \<longrightarrow> (\<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst ((gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc'))) t). case x of (rvb, t') \<Rightarrow> scheduler_equiv aag s' t' \<and> scheduler_affects_equiv aag l s' t')\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l t = reads_scheduler_cur_domain aag l s proof (prove)
goal:
No subgoals!