theory Detype_C

lemma cmap_array_typ_region_bytes:
  "ptrf = (Ptr :: _ \<Rightarrow> 'b ptr)
    \<Longrightarrow> carray_map_relation bits' amap (h_t_valid htd c_guard) ptrf
    \<Longrightarrow> is_aligned ptr bits
    \<Longrightarrow> typ_uinfo_t TYPE('b :: c_type) \<noteq> typ_uinfo_t TYPE(8 word)
    \<Longrightarrow> size_of TYPE('b) = 2 ^ bits'
    \<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits
    \<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits'
    \<Longrightarrow> bits' < word_bits
    \<Longrightarrow> carray_map_relation bits' (restrict_map (amap :: _ \<Rightarrow> 'a option) (- {ptr ..+ 2 ^ bits}))
        (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf" apply (clarsimp simp: carray_map_relation_def h_t_valid_typ_region_bytes) apply (case_tac "h_t_valid htd c_guard (ptrf p)", simp_all) apply (clarsimp simp: objBits_koTypeOf) apply (drule spec, drule(1) iffD2, clarsimp) apply (rule iffI[rotated]) apply clarsimp apply (drule equals0D, erule notE, erule IntI[rotated]) apply (simp only: upto_intvl_eq is_aligned_neg_mask2 mask_in_range[symmetric]) apply (simp only: upto_intvl_eq, rule distinct_aligned_addresses_accumulate,
     simp_all add: upto_intvl_eq[symmetric] word_size word_bits_def) apply clarsimp apply (drule_tac x="p + (y << objBitsT (koType TYPE('a)))" in spec)+ apply (simp add: is_aligned_add[OF is_aligned_weaken is_aligned_shiftl]) apply (simp add: is_aligned_add_helper shiftl_less_t2n word_bits_def) apply clarsimp apply (drule_tac x=p in spec) apply (clarsimp simp: objBits_koTypeOf) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' amap (h_t_valid htd c_guard) ptrf; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits\<rbrakk> \<Longrightarrow> carray_map_relation bits' (amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits\<rbrakk> \<Longrightarrow> (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<longrightarrow> p' \<in> dom amap \<and> p' \<notin> {ptr..+2 ^ bits})) = ({p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {} \<and> htd \<Turnstile>\<^sub>t PTR('b) p) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<longrightarrow> p' \<in> dom amap \<and> p' \<notin> {ptr..+2 ^ bits})) = ({p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {})
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap \<and> p' \<notin> {ptr..+2 ^ bits})) = ({p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {})
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap\<rbrakk> \<Longrightarrow> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}) = ({p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {})
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; {p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}
 2. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}
 3. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (3 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) (p' && ~~ mask bits'); \<forall>p'a. p'a && ~~ mask bits' = p' && ~~ mask bits' \<and> is_aligned p'a (objBitsT (koType TYPE('a))) \<longrightarrow> p'a \<in> dom amap; {p' && ~~ mask bits'..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}; is_aligned p' (objBitsT (koType TYPE('a))); p' \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}
 3. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (3 subgoals):
 1. \<And>p'. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) (p' && ~~ mask bits'); \<forall>p'a. p'a && ~~ mask bits' = p' && ~~ mask bits' \<and> is_aligned p'a (objBitsT (koType TYPE('a))) \<longrightarrow> p'a \<in> dom amap; is_aligned p' (objBitsT (koType TYPE('a)))\<rbrakk> \<Longrightarrow> p' \<in> {p' && ~~ mask bits'..+2 ^ bits'}
 2. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}
 3. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> {p..+2 ^ bits'} \<inter> {ptr..+2 ^ bits} = {}
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < word_bits; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> \<forall>y<2 ^ (bits' - objBitsT (koType TYPE('a))). p + (y << objBitsT (koType TYPE('a))) \<notin> {ptr..+2 ^ bits}
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p y. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<in> dom amap; \<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBitsT (koType TYPE('a))) \<longrightarrow> p' \<notin> {ptr..+2 ^ bits}; y < 2 ^ (bits' - objBitsT (koType TYPE('a))); p + (y << objBitsT (koType TYPE('a))) \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p y. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; y < 2 ^ (bits' - objBitsT (koType TYPE('a))); p + (y << objBitsT (koType TYPE('a))) \<in> {ptr..+2 ^ bits}; p + (y << objBitsT (koType TYPE('a))) && ~~ mask bits' = p \<and> is_aligned (p + (y << objBitsT (koType TYPE('a)))) (objBitsT (koType TYPE('a))) \<longrightarrow> p + (y << objBitsT (koType TYPE('a))) \<in> dom amap; p + (y << objBitsT (koType TYPE('a))) && ~~ mask bits' = p \<and> is_aligned (p + (y << objBitsT (koType TYPE('a)))) (objBitsT (koType TYPE('a))) \<longrightarrow> p + (y << objBitsT (koType TYPE('a))) \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (2 subgoals):
 1. \<And>p y. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; y < 2 ^ (bits' - objBitsT (koType TYPE('a))); p + (y << objBitsT (koType TYPE('a))) \<in> {ptr..+2 ^ bits}; p + (y << objBitsT (koType TYPE('a))) && ~~ mask bits' \<noteq> p\<rbrakk> \<Longrightarrow> False
 2. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> is_aligned p bits' \<longrightarrow> (\<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits})) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); \<forall>p. (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'\<rbrakk> \<Longrightarrow> \<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits}) proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) p; is_aligned p bits'; (is_aligned p bits' \<and> (\<forall>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the (amap p'))) \<longrightarrow> p' \<in> dom amap)) = htd \<Turnstile>\<^sub>t PTR('b) p\<rbrakk> \<Longrightarrow> \<exists>p'. p' && ~~ mask bits' = p \<and> is_aligned p' (objBits (the ((amap|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) p'))) \<and> (p' \<in> dom amap \<longrightarrow> p' \<in> {ptr..+2 ^ bits}) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>ptrf = PTR('b); is_aligned ptr bits; typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); size_of TYPE('b) = 2 ^ bits'; objBitsT (koType TYPE('a)) \<le> bits; objBitsT (koType TYPE('a)) \<le> bits'; bits' < 32; \<not> htd \<Turnstile>\<^sub>t PTR('b) (p' && ~~ mask bits'); is_aligned p' (objBitsT (koType TYPE('a))); \<forall>p'a. is_aligned p'a (objBitsT (koType TYPE('a))) \<longrightarrow> p'a && ~~ mask bits' = p' && ~~ mask bits' \<longrightarrow> p'a \<in> dom amap \<and> p'a \<notin> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> \<exists>y. amap p' = Some y proof (prove)
goal:
No subgoals!