theory Retype_C

lemma cmap_array_typ_region_bytes_triv[OF refl]:
  "ptrf = (Ptr :: _ \<Rightarrow> 'b ptr)
    \<Longrightarrow> carray_map_relation bits' (map_comp f (ksPSpace s)) (h_t_valid htd c_guard) ptrf
    \<Longrightarrow> is_aligned ptr bits
    \<Longrightarrow> pspace_no_overlap' ptr bits s
    \<Longrightarrow> pspace_aligned' s
    \<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' (map_comp (f :: _ \<Rightarrow> 'a option) (ksPSpace s))
        (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf" apply (frule(7) cmap_array_typ_region_bytes[where ptrf=ptrf]) apply (subst(asm) restrict_map_subdom, simp_all) apply (drule(1) pspace_no_overlap_disjoint') apply (simp add: upto_intvl_eq) apply (rule order_trans[OF map_comp_subset_dom]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) ptrf; is_aligned ptr bits; pspace_no_overlap' ptr bits s; pspace_aligned' s; 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' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) ptrf; is_aligned ptr bits; pspace_no_overlap' ptr bits s; pspace_aligned' s; 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; carray_map_relation bits' ((f \<circ>\<^sub>m ksPSpace s)|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf\<rbrakk> \<Longrightarrow> carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) PTR('b); is_aligned ptr bits; pspace_no_overlap' ptr bits s; pspace_aligned' s; 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> dom (f \<circ>\<^sub>m ksPSpace s) \<subseteq> - {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) PTR('b); is_aligned ptr bits; pspace_no_overlap' ptr bits s; 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; {ptr..(ptr && ~~ mask bits) + 2 ^ bits - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> dom (f \<circ>\<^sub>m ksPSpace s) \<subseteq> - {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) PTR('b); is_aligned ptr bits; pspace_no_overlap' ptr bits s; 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; {ptr..ptr + 2 ^ bits - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> dom (f \<circ>\<^sub>m ksPSpace s) \<subseteq> - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrf = PTR('b); carray_map_relation bits' (f \<circ>\<^sub>m ksPSpace s) (h_t_valid htd c_guard) PTR('b); is_aligned ptr bits; pspace_no_overlap' ptr bits s; 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; {ptr..ptr + 2 ^ bits - 1} \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> dom (ksPSpace s) \<subseteq> - {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal:
No subgoals!