theory Untyped_R

lemma caps_no_overlap'[simp]: "caps_no_overlap'' ptr sz s" using cte_wp_at' misc cover desc_range idx_cases apply - apply (erule disjE) apply (erule cte_wp_at_caps_no_overlapI'
     [OF  _ _ _ range_cover.sz(1)[where 'a=32, folded word_bits_def]]) apply simp+ apply (erule descendants_range_caps_no_overlapI') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_no_overlap'' ptr sz s proof (prove)
using this:
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
ct_active' s
invs' s
range_cover ptr sz (APIType_capBits tp us) (length slots)
reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s)
\<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz

goal (1 subgoal):
 1. caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; invs' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; invs' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; invs' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap ?d9 (ptr && ~~ mask sz) sz ?idx9) ?cref9 s
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> ?idx9 \<le> unat (ptr && mask sz)
 3. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> range_cover ?ptr10 sz ?sbit10 ?n10
 4. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; ct_active' s; invs' s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev ptr sz idx) cref s; ct_active' s; invs' s; range_cover ptr sz (APIType_capBits tp us) (length slots); descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev ptr sz idx) cref s; ct_active' s; range_cover ptr sz (APIType_capBits tp us) (length slots); descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap ?d17 (ptr && ~~ mask sz) sz ?idx17) ?cref17 s
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev ptr sz idx) cref s; ct_active' s; range_cover ptr sz (APIType_capBits tp us) (length slots); descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} ?cref17 (ctes_of s) proof (prove)
goal:
No subgoals!