theory Retype_R

lemma obj_relation_cuts_trivial:
  "ptr \<in> fst ` obj_relation_cuts x ptr" apply (case_tac x) apply (rename_tac sz cs) apply (clarsimp simp:image_def cte_map_def well_formed_cnode_n_def) apply (rule_tac x = "replicate sz False" in exI) apply clarsimp+ apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj) apply clarsimp apply (simp_all add:image_def pageBits_def) apply (rule_tac x = 0 in exI, simp)+ apply (rule p2_gt_0[THEN iffD2]) apply (rename_tac vmpage_size) apply (case_tac vmpage_size) apply (clarsimp simp:pageBitsForSize_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<in> fst ` obj_relation_cuts x ptr proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. x = CNode x11 x12 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 2. \<And>x2. x = TCB x2 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 3. \<And>x3. x = Endpoint x3 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 4. \<And>x4. x = Notification x4 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 5. \<And>x5. x = ArchObj x5 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr proof (prove)
goal (5 subgoals):
 1. \<And>sz cs. x = CNode sz cs \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 2. \<And>x2. x = TCB x2 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 3. \<And>x3. x = Endpoint x3 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 4. \<And>x4. x = Notification x4 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 5. \<And>x5. x = ArchObj x5 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr proof (prove)
goal (5 subgoals):
 1. \<And>sz cs. \<lbrakk>x = CNode sz cs; dom cs = {x. length x = sz}\<rbrakk> \<Longrightarrow> \<exists>y. of_bl y * 2 ^ cte_level_bits = 0 \<and> length y = sz
 2. \<And>x2. x = TCB x2 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 3. \<And>x3. x = Endpoint x3 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 4. \<And>x4. x = Notification x4 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 5. \<And>x5. x = ArchObj x5 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr proof (prove)
goal (5 subgoals):
 1. \<And>sz cs. \<lbrakk>x = CNode sz cs; dom cs = {x. length x = sz}\<rbrakk> \<Longrightarrow> of_bl (replicate sz False) * 2 ^ cte_level_bits = 0 \<and> length (replicate sz False) = sz
 2. \<And>x2. x = TCB x2 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 3. \<And>x3. x = Endpoint x3 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 4. \<And>x4. x = Notification x4 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr
 5. \<And>x5. x = ArchObj x5 \<Longrightarrow> ptr \<in> fst ` obj_relation_cuts x ptr proof (prove)
goal (1 subgoal):
 1. \<And>x5. x = ArchObj x5 \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts x5 ptr proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj. x = ArchObj arch_kernel_obj \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x1. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = arch_kernel_obj.ASIDPool x1\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr
 2. \<And>arch_kernel_obj x2. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr
 3. \<And>arch_kernel_obj x3. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr
 4. \<And>arch_kernel_obj x41 x42. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr
 2. \<And>arch_kernel_obj x3. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>x = ArchObj arch_kernel_obj; arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> ptr \<in> fst ` aobj_relation_cuts arch_kernel_obj ptr proof (prove)
goal (3 subgoals):
 1. \<And>arch_kernel_obj x2. \<lbrakk>x = ArchObj (PageTable x2); arch_kernel_obj = PageTable x2\<rbrakk> \<Longrightarrow> \<exists>x. UCAST(8 \<rightarrow> 32) x << 2 = 0
 2. \<And>arch_kernel_obj x3. \<lbrakk>x = ArchObj (PageDirectory x3); arch_kernel_obj = PageDirectory x3\<rbrakk> \<Longrightarrow> \<exists>x. UCAST(12 \<rightarrow> 32) x << 2 = 0
 3. \<And>arch_kernel_obj x41 x42. \<lbrakk>x = ArchObj (DataPage x41 x42); arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>n. n * 0x1000 = 0 \<and> n < 2 ^ (pageBitsForSize x42 - 12) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 x42. \<lbrakk>x = ArchObj (DataPage x41 x42); arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> 0 < 2 ^ (pageBitsForSize x42 - 12) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 x42. \<lbrakk>x = ArchObj (DataPage x41 x42); arch_kernel_obj = DataPage x41 x42\<rbrakk> \<Longrightarrow> pageBitsForSize x42 - 12 < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>x = ArchObj (DataPage x41 vmpage_size); arch_kernel_obj = DataPage x41 vmpage_size\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size - 12 < LENGTH(32) proof (prove)
goal (4 subgoals):
 1. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>x = ArchObj (DataPage x41 vmpage_size); arch_kernel_obj = DataPage x41 vmpage_size; vmpage_size = ARMSmallPage\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size - 12 < LENGTH(32)
 2. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>x = ArchObj (DataPage x41 vmpage_size); arch_kernel_obj = DataPage x41 vmpage_size; vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size - 12 < LENGTH(32)
 3. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>x = ArchObj (DataPage x41 vmpage_size); arch_kernel_obj = DataPage x41 vmpage_size; vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size - 12 < LENGTH(32)
 4. \<And>arch_kernel_obj x41 vmpage_size. \<lbrakk>x = ArchObj (DataPage x41 vmpage_size); arch_kernel_obj = DataPage x41 vmpage_size; vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size - 12 < LENGTH(32) proof (prove)
goal:
No subgoals!