theory Arch_IF

lemma equiv_but_for_reads_equiv:
  "\<lbrakk> pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s' \<rbrakk>
     \<Longrightarrow> reads_equiv aag s s'" apply (simp add: reads_equiv_def2) apply (rule conjI) apply (clarsimp simp: labels_are_invisible_def equiv_but_for_labels_def) apply (rule states_equiv_forI) apply (fastforce intro: equiv_forI elim: states_equiv_forE equiv_forD)+ apply (auto intro!: equiv_forI elim!: states_equiv_forE elim!: equiv_forD simp: o_def)[1] apply (fastforce intro: equiv_forI elim: states_equiv_forE equiv_forD)+ apply (fastforce simp: equiv_asids_def elim: states_equiv_forE elim: equiv_forD) apply (clarsimp simp: equiv_for_def states_equiv_for_def disjoint_iff_not_equal) apply (metis pas_domains_distinct_inj) apply (fastforce simp: equiv_but_for_labels_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> reads_equiv aag s s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s'
 2. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s'
 2. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (11 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag) kheap s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s')
 3. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) cdt s s'
 4. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag) ekheap s s'
 5. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'
 6. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'
 7. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_states s s'
 8. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'
 9. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (aag_can_read_asid aag) s s'
 10. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) ready_queues s s'
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_states s s'
 3. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'
 4. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (aag_can_read_asid aag) s s'
 5. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) ready_queues s s'
 6. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_states s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'
 3. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (aag_can_read_asid aag) s s'
 4. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) ready_queues s s'
 5. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_asids (aag_can_read_asid aag) s s'
 2. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) ready_queues s s'
 3. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); 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) s s'; cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s')\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read_domain aag) ready_queues s s'
 2. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>pas_domains_distinct aag; \<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) (pasSubject aag); aag_can_affect_label aag l \<longrightarrow> (\<forall>d\<in>L. d \<notin> subjectReads (pasPolicy aag) l); cur_thread s = cur_thread s'; cur_domain s = cur_domain s'; scheduler_action s = scheduler_action s'; work_units_completed s = work_units_completed s'; equiv_irq_state (machine_state s) (machine_state s'); \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> kheap s x = kheap s' x; \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> underlying_memory (machine_state s) x = underlying_memory (machine_state s') x; \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> device_state (machine_state s) x = device_state (machine_state s') x; \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. cdt s (a, b) = cdt s' (a, b)); \<forall>x. pasObjectAbs aag x \<notin> L \<longrightarrow> ekheap s x = ekheap s' x; \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. cdt_list s (a, b) = cdt_list s' (a, b)); \<forall>a. pasObjectAbs aag a \<notin> L \<longrightarrow> (\<forall>b. is_original_cap s (a, b) = is_original_cap s' (a, b)); \<forall>x. pasIRQAbs aag x \<notin> L \<longrightarrow> interrupt_states s x = interrupt_states s' x; \<forall>x. pasIRQAbs aag x \<notin> L \<longrightarrow> interrupt_irq_node s x = interrupt_irq_node s' x; \<forall>x. (\<forall>l\<in>pasDomainAbs aag x. l \<notin> L) \<longrightarrow> ready_queues s x = ready_queues s' x; equiv_asids (\<lambda>x. pasASIDAbs aag x \<notin> L) s s'; xa \<in> pasDomainAbs aag x; xa \<in> subjectReads (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> ready_queues s x = ready_queues s' x
 2. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_domains_distinct aag; labels_are_invisible aag l L; equiv_but_for_labels aag L s s'\<rbrakk> \<Longrightarrow> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') proof (prove)
goal:
No subgoals!