theory KHeap_R

lemma obj_relation_cut_same_type:
  "\<lbrakk> (y, P) \<in> obj_relation_cuts ko x; P ko z;
    (y', P') \<in> obj_relation_cuts ko' x'; P' ko' z \<rbrakk>
     \<Longrightarrow> (a_type ko = a_type ko') \<or> (\<exists>n n'. a_type ko = ACapTable n \<and> a_type ko' = ACapTable n')
         \<or> (\<exists>sz sz'. a_type ko = AArch (AUserData sz) \<and> a_type ko' = AArch (AUserData sz'))
         \<or> (\<exists>sz sz'. a_type ko = AArch (ADeviceData sz) \<and> a_type ko' = AArch (ADeviceData sz'))" apply (rule ccontr) apply (simp add: obj_relation_cuts_def2 a_type_def) apply (auto simp: other_obj_relation_def cte_relation_def
                    pte_relation_def pde_relation_def
             split: Structures_A.kernel_object.split_asm if_split_asm
                    Structures_H.kernel_object.split_asm
                    ARM_A.arch_kernel_obj.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; P ko z; (y', P') \<in> obj_relation_cuts ko' x'; P' ko' z\<rbrakk> \<Longrightarrow> a_type ko = a_type ko' \<or> (\<exists>n n'. a_type ko = ACapTable n \<and> a_type ko' = ACapTable n') \<or> (\<exists>sz sz'. a_type ko = AArch (AUserData sz) \<and> a_type ko' = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type ko = AArch (ADeviceData sz) \<and> a_type ko' = AArch (ADeviceData sz')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> obj_relation_cuts ko x; P ko z; (y', P') \<in> obj_relation_cuts ko' x'; P' ko' z; \<not> (a_type ko = a_type ko' \<or> (\<exists>n n'. a_type ko = ACapTable n \<and> a_type ko' = ACapTable n') \<or> (\<exists>sz sz'. a_type ko = AArch (AUserData sz) \<and> a_type ko' = AArch (AUserData sz')) \<or> (\<exists>sz sz'. a_type ko = AArch (ADeviceData sz) \<and> a_type ko' = AArch (ADeviceData sz')))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, P) \<in> (case ko of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs then {(cte_map (x, y), cte_relation y) |y. y \<in> dom cs} else {(x, \<lambda>_ _. False)} | ArchObj (arch_kernel_obj.ASIDPool fun) \<Rightarrow> {(x, other_obj_relation)} | ArchObj (PageTable pt) \<Rightarrow> range (\<lambda>y. (x + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)) | ArchObj (PageDirectory pd) \<Rightarrow> range (\<lambda>y. (x + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)) | ArchObj (DataPage dev sz) \<Rightarrow> {(x + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData)) |n. n < 2 ^ (pageBitsForSize sz - pageBits)} | _ \<Rightarrow> {(x, other_obj_relation)}); P ko z; (y', P') \<in> (case ko' of CNode sz cs \<Rightarrow> if well_formed_cnode_n sz cs then {(cte_map (x', y), cte_relation y) |y. y \<in> dom cs} else {(x', \<lambda>_ _. False)} | ArchObj (arch_kernel_obj.ASIDPool fun) \<Rightarrow> {(x', other_obj_relation)} | ArchObj (PageTable pt) \<Rightarrow> range (\<lambda>y. (x' + (UCAST(8 \<rightarrow> 32) y << 2), pte_relation y)) | ArchObj (PageDirectory pd) \<Rightarrow> range (\<lambda>y. (x' + (UCAST(12 \<rightarrow> 32) y << 2), pde_relation y)) | ArchObj (DataPage dev sz) \<Rightarrow> {(x' + n * 2 ^ pageBits, \<lambda>_ obj. obj = (if dev then KOUserDataDevice else KOUserData)) |n. n < 2 ^ (pageBitsForSize sz - pageBits)} | _ \<Rightarrow> {(x', other_obj_relation)}); P' ko' z; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> (case ko' of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<and> ((\<forall>n. (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> ACapTable n) \<or> (\<forall>n'. (case ko' of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> ACapTable n')) \<and> ((\<forall>sz. (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> AArch (AUserData sz)) \<or> (\<forall>sz'. (case ko' of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> AArch (AUserData sz'))) \<and> ((\<forall>sz. (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> AArch (ADeviceData sz)) \<or> (\<forall>sz'. (case ko' of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> AArch (ADeviceData sz')))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!