theory Retype_C

lemma h_t_array_valid_ptr_retyps_gen:
  assumes sz2: "size_of TYPE('a :: mem_type) = sz"
  assumes bytes: "region_is_bytes' (ptr_val p) (n * sz) htd"
  shows "h_t_array_valid htd p' n'
    \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n (p :: 'a :: mem_type ptr) arr htd) p' n'" apply (clarsimp simp: h_t_array_valid_def valid_footprint_def) apply (drule spec, drule(1) mp, clarsimp) apply (case_tac "ptr_val p' + of_nat y \<in> {ptr_val p ..+ n * size_of TYPE('a)}") apply (cut_tac s="uinfo_array_tag_n_m TYPE('b) n' n'" and n=y in ladder_set_self) apply (clarsimp dest!: in_set_list_map) apply (drule(1) map_le_trans) apply (simp add: map_le_def) apply (subst(asm) bytes[unfolded region_is_bytes'_def, rule_format, symmetric]) apply (simp add: sz2) apply (simp add: uinfo_array_tag_n_m_def typ_uinfo_t_def typ_info_word) apply simp apply (simp add: ptr_retyps_gen_out) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h_t_array_valid htd p' n' \<Longrightarrow> h_t_array_valid (ptr_retyps_gen n p arr htd) p' n' proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; \<forall>y<size_of TYPE('b) * n'. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) 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)); y < size_of TYPE('b) * n'\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<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 (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; uinfo_array_tag_n_m TYPE('b) n' n' \<in> fst ` set (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; [na \<mapsto> (uinfo_array_tag_n_m TYPE('b) n' n', b)] \<subseteq>\<^sub>m list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; [na \<mapsto> (uinfo_array_tag_n_m TYPE('b) n' n', b)] \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; Some (uinfo_array_tag_n_m TYPE('b) n' n', b) = snd (htd (ptr_val p' + word_of_nat y)) na\<rbrakk> \<Longrightarrow> (\<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. snd (htd (ptr_val p' + word_of_nat y)) a = snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) a) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (4 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * sz}
 2. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> uinfo_array_tag_n_m TYPE('b) n' n' \<noteq> typ_uinfo_t TYPE(8 word)
 3. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; False\<rbrakk> \<Longrightarrow> (\<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. snd (htd (ptr_val p' + word_of_nat y)) a = snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) a) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 4. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (3 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> uinfo_array_tag_n_m TYPE('b) n' n' \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; False\<rbrakk> \<Longrightarrow> (\<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. snd (htd (ptr_val p' + word_of_nat y)) a = snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) a) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 3. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y b na. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; \<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. Some (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y ! a) = snd (htd (ptr_val p' + word_of_nat y)) a; fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<in> {ptr_val p..+n * size_of TYPE('a)}; False\<rbrakk> \<Longrightarrow> (\<forall>a\<in>{0..<length (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y)}. snd (htd (ptr_val p' + word_of_nat y)) a = snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) a) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y))
 2. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < size_of TYPE('b); 0 < n'; y < size_of TYPE('b) * n'; list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat y)); fst (htd (ptr_val p' + word_of_nat y)); ptr_val p' + word_of_nat y \<notin> {ptr_val p..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('b) n' n') y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) \<and> fst (ptr_retyps_gen n p arr htd (ptr_val p' + word_of_nat y)) proof (prove)
goal:
No subgoals!