theory Ipc_IF

lemma tcb_sched_action_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and pas_refined aag\<rbrace>
   tcb_sched_action action thread
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" apply (simp add: tcb_sched_action_def, wp) apply (clarsimp simp: etcb_at_def equiv_but_for_labels_def split: option.splits) apply (rule states_equiv_forI) apply (fastforce intro!: equiv_forI elim!: states_equiv_forE dest: equiv_forD[where f=kheap]) apply (simp add: states_equiv_for_def) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ekheap]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=cdt_list]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=is_original_cap]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_states]) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=interrupt_irq_node]) apply (fastforce simp: equiv_asids_def elim: states_equiv_forE) apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def split: option.splits) apply (rule equiv_forI) apply (erule_tac x="(thread, tcb_domain (the (ekheap s thread)))" in ballE) apply (fastforce elim: states_equiv_forE intro: equiv_forI dest: equiv_forD[where f=ready_queues]) apply (force intro: domtcbs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L) and pas_refined aag\<rbrace> tcb_sched_action action thread \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (equiv_but_for_labels aag L st and (\<lambda>y. pasObjectAbs aag thread \<in> L) and pas_refined aag) s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. equiv_but_for_labels aag L st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then action thread (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) thread s) thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (10 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) kheap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<notin> L) (machine_state st) (machine_state (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s))
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 6. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 7. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 8. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 9. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 10. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (9 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<notin> L) (machine_state st) (machine_state (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s))
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 6. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 7. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 8. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 9. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (8 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 6. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 7. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 8. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (7 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) ekheap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 6. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 7. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (6 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) cdt_list st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 6. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (5 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for ((\<lambda>x. pasObjectAbs aag x \<notin> L) \<circ> fst) is_original_cap st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 5. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (4 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_states st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 4. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. pasIRQAbs aag x \<notin> L) interrupt_irq_node st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 3. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s)
 2. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; pas_refined aag s; ekheap s thread = Some x2\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; ekheap s thread = Some x2; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> equiv_for (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) ready_queues st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; ekheap s thread = Some x2; pas_wellformed aag; irq_map_wellformed aag s; \<forall>x\<in>domains_of_state s. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>l\<in>pasDomainAbs aag x. l \<notin> L\<rbrakk> \<Longrightarrow> ready_queues st x = ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) x proof (prove)
goal (2 subgoals):
 1. \<And>s x2 x. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; ekheap s thread = Some x2; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>l\<in>pasDomainAbs aag x. l \<notin> L; case (thread, tcb_domain (the (ekheap s thread))) of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d\<rbrakk> \<Longrightarrow> ready_queues st x = ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) x
 2. \<And>s x2 x. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; ekheap s thread = Some x2; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>l\<in>pasDomainAbs aag x. l \<notin> L; (thread, tcb_domain (the (ekheap s thread))) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> ready_queues st x = ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) x proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x. \<lbrakk>states_equiv_for (\<lambda>x. pasObjectAbs aag x \<notin> L) (\<lambda>x. pasIRQAbs aag x \<notin> L) (\<lambda>x. pasASIDAbs aag x \<notin> L) (\<lambda>x. \<forall>l\<in>pasDomainAbs aag x. l \<notin> L) st s; cur_thread st = cur_thread s; cur_domain st = cur_domain s; scheduler_action st = scheduler_action s; work_units_completed st = work_units_completed s; equiv_irq_state (machine_state st) (machine_state s); pasObjectAbs aag thread \<in> L; ekheap s thread = Some x2; pas_wellformed aag; irq_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<forall>l\<in>pasDomainAbs aag x. l \<notin> L; (thread, tcb_domain (the (ekheap s thread))) \<notin> domains_of_state s\<rbrakk> \<Longrightarrow> ready_queues st x = ready_queues (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then action thread (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) x proof (prove)
goal:
No subgoals!