theory SR_lemmas_C

lemma region_is_bytes_disjoint:
  assumes cleared: "region_is_bytes' p n (hrs_htd hrs)"
    and not_byte: "typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)"
  shows "hrs_htd hrs \<Turnstile>\<^sub>t (p' :: 'a ptr)
    \<Longrightarrow> {p ..+ n} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}" apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def) apply (clarsimp simp: set_eq_iff dest!: intvlD[where p="ptr_val p'"]) apply (drule_tac x="of_nat k" in spec, clarsimp simp: size_of_def) apply (cut_tac m=k in typ_slice_t_self[where td="typ_uinfo_t TYPE('a)"]) apply (clarsimp simp: in_set_conv_nth) apply (drule_tac x=i in map_leD, simp) apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_htd hrs \<Turnstile>\<^sub>t p' \<Longrightarrow> {p..+n} \<inter> {ptr_val p'..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p' + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val p' + word_of_nat y)); c_guard p'\<rbrakk> \<Longrightarrow> {p..+n} \<inter> {ptr_val p'..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p' + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val p' + word_of_nat y)); c_guard p'; ptr_val p' + word_of_nat k \<in> {p..+n}; k < size_of TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>c_guard p'; ptr_val p' + word_of_nat k \<in> {p..+n}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p' + word_of_nat k)); fst (hrs_htd hrs (ptr_val p' + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>c_guard p'; ptr_val p' + word_of_nat k \<in> {p..+n}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p' + word_of_nat k)); fst (hrs_htd hrs (ptr_val p' + word_of_nat k)); typ_uinfo_t TYPE('a) \<in> fst ` set (typ_slice_t (typ_uinfo_t TYPE('a)) k)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k b i. \<lbrakk>c_guard p'; ptr_val p' + word_of_nat k \<in> {p..+n}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p' + word_of_nat k)); fst (hrs_htd hrs (ptr_val p' + word_of_nat k)); i < length (typ_slice_t (typ_uinfo_t TYPE('a)) k); typ_slice_t (typ_uinfo_t TYPE('a)) k ! i = (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k b i. \<lbrakk>c_guard p'; ptr_val p' + word_of_nat k \<in> {p..+n}; k < size_td (typ_info_t TYPE('a)); fst (hrs_htd hrs (ptr_val p' + word_of_nat k)); i < length (typ_slice_t (typ_uinfo_t TYPE('a)) k); typ_slice_t (typ_uinfo_t TYPE('a)) k ! i = (typ_uinfo_t TYPE('a), b); snd (hrs_htd hrs (ptr_val p' + word_of_nat k)) i = Some (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!