theory Retype_R

lemma captable_relation_retype:
  "n < word_bits \<Longrightarrow>
   obj_relation_retype (default_object Structures_A.CapTableObject dev n) (KOCTE makeObject)" apply (clarsimp simp: obj_relation_retype_def default_object_def
                        wf_empty_bits objBits_simps'
                        dom_empty_cnode ex_with_length cte_level_bits_def) apply (rule conjI) defer apply (clarsimp simp: cte_relation_def empty_cnode_def makeObject_cte) apply (rule set_eqI, rule iffI) apply (clarsimp simp: cte_map_def') apply (rule_tac x="of_bl y" in exI) apply (simp add: of_bl_length[where 'a=32, folded word_bits_def]) apply (clarsimp simp: image_def cte_map_def') apply (rule_tac x="drop (word_bits - n) (to_bl xa)" in exI) apply (simp add: of_drop_to_bl word_bits_def word_size) apply (simp add: less_mask_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < word_bits \<Longrightarrow> obj_relation_retype (default_object Structures_A.apiobject_type.CapTableObject dev n) (KOCTE makeObject) proof (prove)
goal (1 subgoal):
 1. \<And>p. n < word_bits \<Longrightarrow> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} = {p + x * 0x10 |x. x < 2 ^ n} \<and> (\<forall>a b. (\<exists>y. a = cte_map (p, y) \<and> b = cte_relation y \<and> length y = n) \<longrightarrow> b (CNode n (empty_cnode n)) (KOCTE makeObject)) proof (prove)
goal (2 subgoals):
 1. \<And>p. n < word_bits \<Longrightarrow> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} = {p + x * 0x10 |x. x < 2 ^ n}
 2. \<And>p. n < word_bits \<Longrightarrow> \<forall>a b. (\<exists>y. a = cte_map (p, y) \<and> b = cte_relation y \<and> length y = n) \<longrightarrow> b (CNode n (empty_cnode n)) (KOCTE makeObject) proof (prove)
goal (2 subgoals):
 1. \<And>p. n < word_bits \<Longrightarrow> \<forall>a b. (\<exists>y. a = cte_map (p, y) \<and> b = cte_relation y \<and> length y = n) \<longrightarrow> b (CNode n (empty_cnode n)) (KOCTE makeObject)
 2. \<And>p. n < word_bits \<Longrightarrow> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} = {p + x * 0x10 |x. x < 2 ^ n} proof (prove)
goal (1 subgoal):
 1. \<And>p. n < word_bits \<Longrightarrow> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} = {p + x * 0x10 |x. x < 2 ^ n} proof (prove)
goal (2 subgoals):
 1. \<And>p x. \<lbrakk>n < word_bits; x \<in> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n}\<rbrakk> \<Longrightarrow> x \<in> {p + x * 0x10 |x. x < 2 ^ n}
 2. \<And>p x. \<lbrakk>n < word_bits; x \<in> {p + x * 0x10 |x. x < 2 ^ n}\<rbrakk> \<Longrightarrow> x \<in> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>length y < word_bits; n = length y\<rbrakk> \<Longrightarrow> \<exists>x. of_bl y * 0x10 = x * 0x10 \<and> x < 2 ^ length y
 2. \<And>p x. \<lbrakk>n < word_bits; x \<in> {p + x * 0x10 |x. x < 2 ^ n}\<rbrakk> \<Longrightarrow> x \<in> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>length y < word_bits; n = length y\<rbrakk> \<Longrightarrow> of_bl y * 0x10 = of_bl y * 0x10 \<and> of_bl y < 2 ^ length y
 2. \<And>p x. \<lbrakk>n < word_bits; x \<in> {p + x * 0x10 |x. x < 2 ^ n}\<rbrakk> \<Longrightarrow> x \<in> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} proof (prove)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>n < word_bits; x \<in> {p + x * 0x10 |x. x < 2 ^ n}\<rbrakk> \<Longrightarrow> x \<in> fst ` {(cte_map (p, y), cte_relation y) |y. length y = n} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>n < word_bits; xa < 2 ^ n\<rbrakk> \<Longrightarrow> \<exists>y. xa * 0x10 = of_bl y * 0x10 \<and> length y = n proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>n < word_bits; xa < 2 ^ n\<rbrakk> \<Longrightarrow> xa * 0x10 = of_bl (drop (word_bits - n) (to_bl xa)) * 0x10 \<and> length (drop (word_bits - n) (to_bl xa)) = n proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>n < 32; xa < 2 ^ n\<rbrakk> \<Longrightarrow> xa * 0x10 = (xa && mask n) * 0x10 proof (prove)
goal:
No subgoals!