theory Retype_C

lemma ptr_retyps_gen_valid_footprint:
  assumes cleared: "region_is_bytes' p (n * size_of TYPE('a)) htd"
    and distinct: "td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
    and not_byte: "td \<noteq> typ_uinfo_t TYPE(word8)"
    and sz: "n * size_of TYPE('a) < addr_card"
  shows
  "valid_footprint (ptr_retyps_gen n (Ptr p :: 'a :: mem_type ptr) arr htd) p' td
    = (valid_footprint htd p' td)" apply (cases "n = 0") apply (simp add: ptr_retyps_gen_def ptr_arr_retyps_def split: if_split) apply (simp add: valid_footprint_def Let_def) apply (intro conj_cong refl, rule all_cong) apply (case_tac "p' + of_nat y \<in> {p ..+ n * size_of TYPE('a)}") apply (simp_all add: ptr_retyps_gen_out) apply (rule iffI; clarsimp) apply (frule(1) ptr_retyps_gen_not_tag_disj, (simp add: sz)+) apply (simp add: distinct) apply (cut_tac m=y in typ_slice_t_self[where td=td]) apply (clarsimp simp: in_set_conv_nth) apply (drule_tac x=i in map_leD) apply simp apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_footprint (ptr_retyps_gen n (PTR('a) p) arr htd) p' td = valid_footprint htd p' td proof (prove)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> valid_footprint (ptr_retyps_gen n (PTR('a) p) arr htd) p' td = valid_footprint htd p' td
 2. n \<noteq> 0 \<Longrightarrow> valid_footprint (ptr_retyps_gen n (PTR('a) p) arr htd) p' td = valid_footprint htd p' td proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> valid_footprint (ptr_retyps_gen n (PTR('a) p) arr htd) p' td = valid_footprint htd p' td proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)))) = (0 < size_td td \<and> (\<forall>y<size_td td. list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y)))) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; 0 < size_td td; y < size_td td\<rbrakk> \<Longrightarrow> (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y))) = (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < n; 0 < size_td td; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y))) = (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y)))
 2. \<And>y. \<lbrakk>0 < n; 0 < size_td td; y < size_td td; p' + word_of_nat y \<notin> {p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y))) = (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y))) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y))) = (list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y))) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)); fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)); fst (htd (p' + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)); fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)); \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)) \<and> fst (htd (p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)); fst (htd (p' + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)); fst (htd (p' + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)); fst (htd (p' + word_of_nat y)); td \<in> fst ` set (typ_slice_t td y)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y b i. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd (p' + word_of_nat y)); fst (htd (p' + word_of_nat y)); i < length (typ_slice_t td y); typ_slice_t td y ! i = (td, b)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y b i. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; fst (htd (p' + word_of_nat y)); i < length (typ_slice_t td y); typ_slice_t td y ! i = (td, b)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) i = Some (?y37 y b i)
 2. \<And>y b i. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; fst (htd (p' + word_of_nat y)); i < length (typ_slice_t td y); typ_slice_t td y ! i = (td, b); snd (htd (p' + word_of_nat y)) i = Some (?y37 y b i)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y b i. \<lbrakk>0 < n; y < size_td td; p' + word_of_nat y \<in> {p..+n * size_of TYPE('a)}; fst (htd (p' + word_of_nat y)); i < length (typ_slice_t td y); typ_slice_t td y ! i = (td, b); snd (htd (p' + word_of_nat y)) i = Some (td, b)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n (PTR('a) p) arr htd (p' + word_of_nat y)) proof (prove)
goal:
No subgoals!