theory Retype_C

lemma cmap_relation_array_add_array[OF refl]:
  "ptrf = Ptr \<Longrightarrow> carray_map_relation n ahp chp ptrf
    \<Longrightarrow> is_aligned p n
    \<Longrightarrow> ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs sz p ko) then Some v else ahp x)
    \<Longrightarrow> (\<forall>x. chp x \<longrightarrow> is_aligned (ptr_val x) n \<Longrightarrow> \<forall>y. chp' y = (y = ptrf p | chp y))
    \<Longrightarrow> sz = 2 ^ (n - objBits v)
    \<Longrightarrow> objBitsKO ko = objBitsKO (injectKOS v)
    \<Longrightarrow> objBits v \<le> n \<Longrightarrow> n < word_bits
    \<Longrightarrow> carray_map_relation n ahp' chp' ptrf" apply (clarsimp simp: carray_map_relation_def objBits_koTypeOf
                        objBitsT_koTypeOf[symmetric]
                        koTypeOf_injectKO
              simp del: objBitsT_koTypeOf) apply (drule meta_mp) apply auto[1] apply (case_tac "pa = p"; clarsimp) apply (subst if_P; simp add: new_cap_addrs_def) apply (rule_tac x="unat ((p' && mask n) >> objBitsKO ko)" in image_eqI) apply (simp add: shiftr_shiftl1 is_aligned_andI1 add.commute
                     word_plus_and_or_coroll2) apply (simp, rule unat_less_helper, simp, rule shiftr_less_t2n) apply (simp add: and_mask_less_size word_size word_bits_def) apply (case_tac "chp (ptrf pa)", simp_all) apply (drule spec, drule(1) iffD2) apply (auto split: if_split)[1] apply (drule_tac x=pa in spec, clarsimp) apply (drule_tac x=p' in spec, clarsimp split: if_split_asm) apply (clarsimp simp: new_cap_addrs_def) apply (subst(asm) is_aligned_add_helper, simp_all) apply (rule shiftl_less_t2n, rule word_of_nat_less, simp_all add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('a); carray_map_relation n ahp chp ptrf; is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs sz p ko) then Some v else ahp x); \<forall>x. chp x \<longrightarrow> is_aligned (ptr_val x) n \<Longrightarrow> \<forall>y. chp' y = (y = ptrf p \<or> chp y); sz = 2 ^ (n - objBits v); objBitsKO ko = objBitsKO (injectKOS v); objBits v \<le> n; n < word_bits\<rbrakk> \<Longrightarrow> carray_map_relation n ahp' chp' ptrf proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); \<forall>x. chp x \<longrightarrow> is_aligned (ptr_val x) n \<Longrightarrow> \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsT (koTypeOf ko) = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp' (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsT (koTypeOf ko) = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits\<rbrakk> \<Longrightarrow> \<forall>x. chp x \<longrightarrow> is_aligned (ptr_val x) n
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsT (koTypeOf ko) = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y)\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp' (PTR('a) pa) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsT (koTypeOf ko) = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y)\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp' (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) (p' && ~~ mask n) ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> \<exists>y. (if p' \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) (p' && ~~ mask n) ko) then Some v else ahp p') = Some y
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))}
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (3 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> p' = (p' && ~~ mask n) + (word_of_nat (unat (p' && mask n >> objBitsKO ko)) << objBitsT (koType TYPE('b)))
 2. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> unat (p' && mask n >> objBitsKO ko) \<in> {0..<2 ^ (n - objBitsT (koType TYPE('b)))}
 3. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> unat (p' && mask n >> objBitsKO ko) \<in> {0..<2 ^ (n - objBitsT (koType TYPE('b)))}
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. (p' && ~~ mask n) + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) (p' && ~~ mask n) \<or> chp y); is_aligned p' (objBitsT (koType TYPE('b))); p = p' && ~~ mask n\<rbrakk> \<Longrightarrow> p' && mask n < 2 ^ (objBitsT (koType TYPE('b)) + (n - objBitsT (koType TYPE('b))))
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p\<rbrakk> \<Longrightarrow> (is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))) = chp (PTR('a) pa) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p; chp (PTR('a) pa)\<rbrakk> \<Longrightarrow> is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p; \<not> chp (PTR('a) pa)\<rbrakk> \<Longrightarrow> is_aligned pa n \<longrightarrow> (\<exists>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<and> p' \<notin> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x)) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p; chp (PTR('a) pa); is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)\<rbrakk> \<Longrightarrow> is_aligned pa n \<and> (\<forall>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x))
 2. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p; \<not> chp (PTR('a) pa)\<rbrakk> \<Longrightarrow> is_aligned pa n \<longrightarrow> (\<exists>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<and> p' \<notin> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x)) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>ptrf = PTR('a); \<forall>p. (is_aligned p n \<and> (\<forall>p'. p' && ~~ mask n = p \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<longrightarrow> p' \<in> dom ahp)) = chp (PTR('a) p); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); pa \<noteq> p; \<not> chp (PTR('a) pa)\<rbrakk> \<Longrightarrow> is_aligned pa n \<longrightarrow> (\<exists>p'. p' && ~~ mask n = pa \<and> is_aligned p' (objBitsT (koType TYPE('b))) \<and> p' \<notin> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x)) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>ptrf = PTR('a); is_aligned p n; ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); p' && ~~ mask n \<noteq> p; \<not> chp (PTR('a) (p' && ~~ mask n)); is_aligned p' (objBitsT (koType TYPE('b))); \<forall>p'a. is_aligned p'a (objBitsT (koType TYPE('b))) \<longrightarrow> p'a && ~~ mask n = p' && ~~ mask n \<longrightarrow> p'a \<in> dom (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x)\<rbrakk> \<Longrightarrow> \<exists>y. ahp p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>ahp' = (\<lambda>x. if x \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko) then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); p' && ~~ mask n \<noteq> p; \<not> chp (PTR('a) (p' && ~~ mask n)); is_aligned p' (objBitsT (koType TYPE('b))); ptrf = PTR('a); is_aligned p n; p' \<in> set (new_cap_addrs (2 ^ (n - objBitsT (koType TYPE('b)))) p ko)\<rbrakk> \<Longrightarrow> \<exists>y. ahp p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>ahp' = (\<lambda>x. if x \<in> (\<lambda>x. p + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y); p + (word_of_nat x << objBitsT (koType TYPE('b))) && ~~ mask n \<noteq> p; \<not> chp (PTR('a) (p + (word_of_nat x << objBitsT (koType TYPE('b))) && ~~ mask n)); is_aligned (p + (word_of_nat x << objBitsT (koType TYPE('b)))) (objBitsT (koType TYPE('b))); ptrf = PTR('a); is_aligned p n; x < 2 ^ (n - objBitsT (koType TYPE('b)))\<rbrakk> \<Longrightarrow> \<exists>y. ahp (p + (word_of_nat x << objBitsT (koType TYPE('b)))) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> chp (PTR('a) (p + (word_of_nat x << objBitsT (koType TYPE('b))) && ~~ mask n)); is_aligned (p + (word_of_nat x << objBitsT (koType TYPE('b)))) (objBitsT (koType TYPE('b))); ptrf = PTR('a); is_aligned p n; x < 2 ^ (n - objBitsT (koType TYPE('b))); ahp' = (\<lambda>x. if x \<in> (\<lambda>x. p + (word_of_nat x << objBitsT (koType TYPE('b)))) ` {0..<2 ^ (n - objBitsT (koType TYPE('b)))} then Some v else ahp x); sz = 2 ^ (n - objBitsT (koType TYPE('b))); objBitsKO ko = objBitsT (koType TYPE('b)); objBitsT (koType TYPE('b)) \<le> n; n < word_bits; \<forall>y. chp' y = (y = PTR('a) p \<or> chp y)\<rbrakk> \<Longrightarrow> word_of_nat x << objBitsT (koType TYPE('b)) < 2 ^ n proof (prove)
goal:
No subgoals!