theory Retype_C

lemma h_t_array_first_element_at:
  "h_t_array_valid htd p n
    \<Longrightarrow> 0 < n
    \<Longrightarrow> gd p
    \<Longrightarrow> h_t_valid htd gd (p :: ('a :: wf_type) ptr)" apply (clarsimp simp: h_t_array_valid_def h_t_valid_def valid_footprint_def
                        Let_def CTypes.sz_nzero[unfolded size_of_def]) apply(drule_tac x="y" in spec, erule impE) apply (erule order_less_le_trans, simp add: size_of_def) apply (clarsimp simp: uinfo_array_tag_n_m_def upt_conv_Cons) apply (erule map_le_trans[rotated]) apply (simp add: list_map_mono split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h_t_array_valid htd p n; 0 < n; gd p\<rbrakk> \<Longrightarrow> htd,gd \<Turnstile>\<^sub>t p proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<forall>y<size_of TYPE('a) * n. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y)); 0 < n; gd p; y < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < n; gd p; y < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> y < size_of TYPE('a) * n
 2. \<And>y. \<lbrakk>0 < n; gd p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; gd p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) \<and> fst (htd (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; gd p; y < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y @ [if y = 0 then (TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string n), True) else (TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string n), False)]) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)); fst (htd (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; gd p; y < size_td (typ_info_t TYPE('a)); fst (htd (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y @ [if y = 0 then (TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string n), True) else (TypDesc (TypAggregate (DTPair (typ_uinfo_t TYPE('a)) [] # map (\<lambda>i. DTPair (typ_uinfo_t TYPE('a)) (replicate i CHR ''1'')) [Suc 0..<n])) (typ_name (typ_uinfo_t TYPE('a)) @ CHR ''_'' # CHR ''a'' # CHR ''r'' # CHR ''r'' # CHR ''a'' # CHR ''y'' # CHR ''_'' # nat_to_bin_string n), False)]) proof (prove)
goal:
No subgoals!