theory ArchFinalise_IF

lemma aag_cap_auth_ASIDPoolCap_asid:
  "\<lbrakk> pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0;
     asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s \<rbrakk>
     \<Longrightarrow> is_subject_asid aag asid'" apply (frule (1) aag_cap_auth_ASIDPoolCap) apply (unfold aag_cap_auth_def) apply (rule is_subject_into_is_subject_asid) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s\<rbrakk> \<Longrightarrow> is_subject_asid aag asid' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> is_subject_asid aag asid' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> is_subject_asid aag asid' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag ?p3) ?cap3
 2. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> is_subject aag ?p3
 3. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> pas_refined aag ?s3
 4. \<lbrakk>(\<forall>x\<in>obj_refs_ac (ArchObjectCap (ASIDPoolCap r asid)). \<forall>auth\<in>cap_auth_conferred (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> (\<forall>x\<in>untyped_range (ArchObjectCap (ASIDPoolCap r asid)). (pasSubject aag, Control, pasObjectAbs aag x) \<in> pasPolicy aag) \<and> cap_links_asid_slot aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)) \<and> cap_links_irq aag (pasSubject aag) (ArchObjectCap (ASIDPoolCap r asid)); asid' \<noteq> 0; asid_high_bits_of asid' = asid_high_bits_of asid; pas_refined aag s; is_subject aag r\<rbrakk> \<Longrightarrow> asid' \<in> cap_asid' ?cap3 proof (prove)
goal:
No subgoals!