theory CNode_IF

lemma descendants_of_eq:
  "\<lbrakk> reads_equiv aag s t; affects_equiv aag l s t;
     pas_refined aag s; pas_refined aag t; is_subject aag (fst slot) \<rbrakk>
   \<Longrightarrow> descendants_of slot (cdt s) = descendants_of slot (cdt t)" apply (rule all_children_descendants_equal[OF _ all_children_subjectReads all_children_subjectReads]) apply (elim reads_equivE) apply (solves\<open>simp add: equiv_for_apply\<close>) by force+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = descendants_of slot (cdt t) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read ?aag1 \<circ> fst) id (cdt s) (cdt t)
 2. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined ?aag1 s
 3. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined ?aag1 t
 4. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> (aag_can_read ?aag1 \<circ> fst) slot proof (prove)
goal (4 subgoals):
 1. \<lbrakk>affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot); equiv_for (aag_can_read aag) kheap s t; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state t); equiv_for (aag_can_read aag \<circ> fst) cdt s t; equiv_for (aag_can_read aag \<circ> fst) cdt_list s t; equiv_for (aag_can_read aag) ekheap s t; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s t; equiv_for (aag_can_read_irq aag) interrupt_states s t; equiv_for (aag_can_read_irq aag) interrupt_irq_node s t; equiv_asids (aag_can_read_asid aag) s t; equiv_for (aag_can_read_domain aag) ready_queues s t; cur_thread s = cur_thread t; cur_domain s = cur_domain t; scheduler_action s = scheduler_action t; work_units_completed s = work_units_completed t; equiv_irq_state (machine_state s) (machine_state t)\<rbrakk> \<Longrightarrow> equiv_for (aag_can_read ?aag1 \<circ> fst) id (cdt s) (cdt t)
 2. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined ?aag1 s
 3. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined ?aag1 t
 4. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> (aag_can_read ?aag1 \<circ> fst) slot proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined aag s
 2. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> pas_refined aag t
 3. \<lbrakk>reads_equiv aag s t; affects_equiv aag l s t; pas_refined aag s; pas_refined aag t; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> (aag_can_read aag \<circ> fst) slot