theory Finalise_IF

lemma owns_cnode_owns_obj_ref_of_child_cnodes_threads_and_zombies:
  "\<lbrakk> pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s;
     is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap \<rbrakk>
     \<Longrightarrow> is_subject aag (obj_ref_of cap)" apply (frule (1) cap_cur_auth_caps_of_state[rotated]) apply (simp add: cte_wp_at_caps_of_state) apply (clarsimp simp: aag_cap_auth_def) apply (case_tac cap, simp_all add: is_zombie_def) apply (drule_tac x=Control in bspec) apply (clarsimp simp: cap_auth_conferred_def) apply (erule (1) aag_Control_into_owns) apply (drule_tac x=Control in bspec) apply (clarsimp simp: cap_auth_conferred_def) apply (erule (1) aag_Control_into_owns) apply (drule_tac x=Control in bspec) apply (clarsimp simp: cap_auth_conferred_def) apply (erule (1) aag_Control_into_owns) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap\<rbrakk> \<Longrightarrow> caps_of_state s slot = Some ?cap
 2. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap; pas_cap_cur_auth aag ?cap\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap; pas_cap_cur_auth aag cap\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) cap) slot s; is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap; \<forall>x\<in>obj_refs_ac cap. \<forall>auth\<in>cap_auth_conferred cap. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag; \<forall>x\<in>untyped_range cap. (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) cap; cap_links_irq aag (pasSubject aag) cap\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of cap) proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot s; \<forall>auth\<in>cap_auth_conferred (CNodeCap x61 x62 x63). (pasSubject aag, auth, pasObjectAbs aag x61) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (CNodeCap x61 x62 x63); cap_links_irq aag (pasSubject aag) (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> is_subject aag x61
 2. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> is_subject aag x7
 3. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (4 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot s; cap_links_asid_slot aag (pasSubject aag) (CNodeCap x61 x62 x63); cap_links_irq aag (pasSubject aag) (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (CNodeCap x61 x62 x63)
 2. \<And>x61 x62 x63. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot s; cap_links_asid_slot aag (pasSubject aag) (CNodeCap x61 x62 x63); cap_links_irq aag (pasSubject aag) (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63; (pasSubject aag, Control, pasObjectAbs aag x61) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x61
 3. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> is_subject aag x7
 4. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot s; cap_links_asid_slot aag (pasSubject aag) (CNodeCap x61 x62 x63); cap_links_irq aag (pasSubject aag) (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63; (pasSubject aag, Control, pasObjectAbs aag x61) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x61
 2. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> is_subject aag x7
 3. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; \<forall>auth\<in>cap_auth_conferred (ThreadCap x7). (pasSubject aag, auth, pasObjectAbs aag x7) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> is_subject aag x7
 2. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (3 subgoals):
 1. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (ThreadCap x7)
 2. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7; (pasSubject aag, Control, pasObjectAbs aag x7) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x7
 3. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (2 subgoals):
 1. \<And>x7. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (ThreadCap x7)) slot s; cap_links_asid_slot aag (pasSubject aag) (ThreadCap x7); cap_links_irq aag (pasSubject aag) (ThreadCap x7); cap = ThreadCap x7; (pasSubject aag, Control, pasObjectAbs aag x7) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x7
 2. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; \<forall>auth\<in>cap_auth_conferred (Zombie x111 x112 x113). (pasSubject aag, auth, pasObjectAbs aag x111) \<in> pasPolicy aag; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (Zombie x111 x112 x113)
 2. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113; (pasSubject aag, Control, pasObjectAbs aag x111) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; cap_links_asid_slot aag (pasSubject aag) (Zombie x111 x112 x113); cap_links_irq aag (pasSubject aag) (Zombie x111 x112 x113); cap = Zombie x111 x112 x113; (pasSubject aag, Control, pasObjectAbs aag x111) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x111 proof (prove)
goal:
No subgoals!