theory Detype_R

lemma new_cap_addrs_disjoint:
  "\<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n))\<rbrakk>
   \<Longrightarrow> set (new_cap_addrs (2^us)
             (((1::word32) + of_nat n << objBitsKO val + us) + ptr) val) \<inter>
       set (new_cap_addrs (unat ((1::word32) + of_nat n << us)) ptr val) = {}" apply (frule range_cover.unat_of_nat_n_shift[where gbits = us,symmetric]) apply simp apply (frule range_cover_rel[where sbit' = "objBitsKO val"]) apply (simp add:field_simps)+ apply (frule new_cap_addrs_distinct) apply (subst (asm) add.commute[where b = 2])+ apply (subst (asm) new_caps_addrs_append[where n = "Suc n",simplified]) apply (simp add:field_simps) apply (clarsimp simp:field_simps Int_ac range_cover_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<Longrightarrow> set (new_cap_addrs (2 ^ us) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)) \<Longrightarrow> us \<le> objBitsKO val + us
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); Suc (Suc n) * 2 ^ us = unat (word_of_nat (Suc (Suc n)) << us)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); Suc (Suc n) * 2 ^ us = unat (word_of_nat (Suc (Suc n)) << us)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); Suc (Suc n) * 2 ^ us = unat (word_of_nat (Suc (Suc n)) << us)\<rbrakk> \<Longrightarrow> objBitsKO val \<le> objBitsKO val + us
 2. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); Suc (Suc n) * 2 ^ us = unat (word_of_nat (Suc (Suc n)) << us)\<rbrakk> \<Longrightarrow> ?m3 = 2 ^ (objBitsKO val + us - objBitsKO val) * Suc (Suc n)
 3. \<lbrakk>range_cover ptr sz (objBitsKO val + us) (Suc (Suc n)); Suc (Suc n) * 2 ^ us = unat (word_of_nat (Suc (Suc n)) << us); range_cover ptr sz (objBitsKO val) ?m3\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (word_of_nat n + 2 << us); range_cover ptr sz (objBitsKO val) (unat (word_of_nat n + 2 << us))\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) (ptr + (1 + word_of_nat n << us + objBitsKO val)) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (word_of_nat n + 2 << us); range_cover ptr sz (objBitsKO val) (unat (word_of_nat n + 2 << us)); distinct (new_cap_addrs (unat (word_of_nat n + 2 << us)) ptr val)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) (ptr + (1 + word_of_nat n << us + objBitsKO val)) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (2 + word_of_nat n << us); range_cover ptr sz (objBitsKO val) (unat (2 + word_of_nat n << us)); distinct (new_cap_addrs (unat (2 + word_of_nat n << us)) ptr val)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) (ptr + (1 + word_of_nat n << us + objBitsKO val)) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (2 + word_of_nat n << us); range_cover ptr sz (objBitsKO val) (unat (2 + word_of_nat n << us))\<rbrakk> \<Longrightarrow> range_cover ptr ?sz13 (objBitsKO ?va13 + us) (Suc (Suc n))
 2. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (2 + word_of_nat n << us); range_cover ptr sz (objBitsKO val) (unat (2 + word_of_nat n << us)); distinct (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val @ new_cap_addrs (unat (2 ^ us)) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) (ptr + (1 + word_of_nat n << us + objBitsKO val)) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (us + objBitsKO val) (Suc (Suc n)); 2 ^ us + (2 ^ us + n * 2 ^ us) = unat (2 + word_of_nat n << us); range_cover ptr sz (objBitsKO val) (unat (2 + word_of_nat n << us)); distinct (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val @ new_cap_addrs (unat (2 ^ us)) ((1 + word_of_nat n << objBitsKO val + us) + ptr) val)\<rbrakk> \<Longrightarrow> set (new_cap_addrs (2 ^ us) (ptr + (1 + word_of_nat n << us + objBitsKO val)) val) \<inter> set (new_cap_addrs (unat (1 + word_of_nat n << us)) ptr val) = {} proof (prove)
goal:
No subgoals!