theory Retype_C

lemma createObject_no_inter:
notes blah[simp del] =  atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
      Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
shows
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits newType userSize) (n + 2) \<and> ptr \<noteq> 0\<rbrace>
  createObject newType (ptr + (of_nat n << APIType_capBits newType userSize)) userSize dev
  \<lbrace>\<lambda>rv s. untypedRange rv \<inter>
  {ptr + (1 + of_nat n << APIType_capBits newType userSize) ..
   ptrend } =
  {}\<rbrace>" apply (rule createObject_untypedRange) apply (clarsimp | wp)+ apply (clarsimp simp: blah toAPIType_def APIType_capBits_def
    ARM_H.toAPIType_def split: object_type.splits) apply (clarsimp simp:shiftl_t2n field_simps) apply (drule word_eq_zeroI) apply (drule(1) range_cover_no_0[where p = "Suc n"]) apply simp apply (simp add:field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits newType userSize) (n + 2) \<and> ptr \<noteq> 0\<rbrace> global.createObject newType (ptr + (word_of_nat n << APIType_capBits newType userSize)) userSize dev \<lbrace>\<lambda>rv s. untypedRange rv \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..ptrend} = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits newType userSize) (n + 2) \<and> ptr \<noteq> 0\<rbrace> global.createObject newType (ptr + (word_of_nat n << APIType_capBits newType userSize)) userSize dev \<lbrace>\<lambda>rv s. (toAPIType newType = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> {ptr + (word_of_nat n << APIType_capBits newType userSize)..ptr + (word_of_nat n << APIType_capBits newType userSize) + 2 ^ userSize - 1} \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..ptrend} = {}) \<and> (toAPIType newType \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> {} \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..ptrend} = {})\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (Suc (Suc n)); ptr \<noteq> 0; toAPIType newType = Some ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> {ptr + (word_of_nat n << APIType_capBits newType userSize)..ptr + (word_of_nat n << APIType_capBits newType userSize) + 2 ^ userSize - 1} \<inter> {ptr + (1 + word_of_nat n << APIType_capBits newType userSize)..ptrend} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> 0; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + (word_of_nat n << userSize) \<le> ptrend; ptr + (1 + word_of_nat n << userSize) \<le> ptr + (word_of_nat n << userSize) + 2 ^ userSize - 1; ptr + (word_of_nat n << userSize) \<le> ptr + (word_of_nat n << userSize) + 2 ^ userSize - 1; ptr + (1 + word_of_nat n << userSize) \<le> ptrend\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> 0; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + word_of_nat n * 2 ^ userSize \<le> ptrend; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + word_of_nat n * 2 ^ userSize \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptrend\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> 0; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + word_of_nat n * 2 ^ userSize \<le> ptrend; ptr + word_of_nat n * 2 ^ userSize \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptrend; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + word_of_nat n * 2 ^ userSize \<le> ptrend; ptr + word_of_nat n * 2 ^ userSize \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptrend; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) = 0\<rbrakk> \<Longrightarrow> Suc n < Suc (Suc n)
 2. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + word_of_nat n * 2 ^ userSize \<le> ptrend; ptr + word_of_nat n * 2 ^ userSize \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptrend; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) = 0; ptr + word_of_nat (Suc n) * 2 ^ userSize \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.Untyped; range_cover ptr sz userSize (Suc (Suc n)); ptr + word_of_nat n * 2 ^ userSize \<le> ptrend; ptr + word_of_nat n * 2 ^ userSize \<le> ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) - 1; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) \<le> ptrend; ptr + (2 ^ userSize + word_of_nat n * 2 ^ userSize) = 0; ptr + word_of_nat (Suc n) * 2 ^ userSize \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!