theory ArchUserOp_IF

lemma requiv_get_pd_of_thread_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; is_subject aag (cur_thread s);
     pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s');
     get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref;
     get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref' \<rbrakk>
     \<Longrightarrow> pd_ref = pd_ref'" apply (erule reads_equivE) apply (erule equiv_forE) apply (subgoal_tac "aag_can_read aag (cur_thread s)") apply (clarsimp simp: get_pd_of_thread_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'\<rbrakk> \<Longrightarrow> pd_ref = pd_ref' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'; equiv_for (aag_can_read aag) kheap s s'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues 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> pd_ref = pd_ref' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> pd_ref = pd_ref' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x; aag_can_read aag (cur_thread s)\<rbrakk> \<Longrightarrow> pd_ref = pd_ref'
 2. \<lbrakk>pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> aag_can_read aag (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (cur_thread s); pd_ref \<noteq> arm_global_pd (arch_state s); pd_ref' \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = pd_ref; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = pd_ref'; equiv_machine_state (aag_can_read aag) (machine_state s) (machine_state s'); equiv_for (aag_can_read aag \<circ> fst) cdt s s'; equiv_for (aag_can_read aag \<circ> fst) cdt_list s s'; equiv_for (aag_can_read aag) ekheap s s'; equiv_for (aag_can_read aag \<circ> fst) is_original_cap s s'; equiv_for (aag_can_read_irq aag) interrupt_states s s'; equiv_for (aag_can_read_irq aag) interrupt_irq_node s s'; equiv_asids (aag_can_read_asid aag) s s'; equiv_for (aag_can_read_domain aag) ready_queues 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'); \<And>x. aag_can_read aag x \<Longrightarrow> kheap s x = kheap s' x\<rbrakk> \<Longrightarrow> aag_can_read aag (cur_thread s) proof (prove)
goal:
No subgoals!