theory Retype_C

lemma ptr_retyps_gen_not_tag_disj:
  "x \<in> {p ..+ n * size_of TYPE('a :: mem_type)}
    \<Longrightarrow> list_map (typ_slice_t td y)
        \<subseteq>\<^sub>m snd (ptr_retyps_gen n (Ptr p :: 'a ptr) arr htd x)
    \<Longrightarrow> y < size_td td
    \<Longrightarrow> n * size_of TYPE('a) < addr_card
    \<Longrightarrow> 0 < n
    \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)" apply (simp add: ptr_retyps_gen_def ptr_arr_retyps_def
            split: if_split_asm) apply (drule_tac td'="uinfo_array_tag_n_m TYPE('a) n n"
     in htd_update_list_not_tag_disj, simp+) apply (clarsimp simp: mult.commute) apply (clarsimp simp: tag_disj_def) apply (erule disjE) apply (metis order_refl typ_le_uinfo_array_tag_n_m) apply (erule notE, erule order_trans[rotated]) apply (simp add: typ_le_uinfo_array_tag_n_m) apply clarsimp apply (induct n arbitrary: p htd, simp_all) apply (case_tac "x \<in> {p ..+ size_of TYPE('a)}") apply (simp add: intvl_sum ptr_retyp_def) apply (drule_tac td'="typ_uinfo_t TYPE('a)"
     in htd_update_list_not_tag_disj, simp+) apply (clarsimp simp add: typ_slices_def size_of_def) apply simp apply (simp add: intvl_sum) apply (case_tac "n = 0") apply simp apply (simp add: ptr_retyps_out[where n=1, simplified]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<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 x); y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p (map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i)) [0..<n * size_of TYPE('a)]) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr\<rbrakk> \<Longrightarrow> (\<lambda>x. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) x)) ` {0..<n * size_of TYPE('a)} \<subseteq> list_map ` typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) ` {..<size_of TYPE('a) * n}
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; \<not> td \<bottom>\<^sub>t uinfo_array_tag_n_m TYPE('a) n n\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)
 3. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; \<not> td \<bottom>\<^sub>t uinfo_array_tag_n_m TYPE('a) n n\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; td \<le> uinfo_array_tag_n_m TYPE('a) n n \<or> uinfo_array_tag_n_m TYPE('a) n n \<le> td; \<not> typ_uinfo_t TYPE('a) \<le> td\<rbrakk> \<Longrightarrow> td \<le> typ_uinfo_t TYPE('a)
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; \<not> typ_uinfo_t TYPE('a) \<le> td; td \<le> uinfo_array_tag_n_m TYPE('a) n n\<rbrakk> \<Longrightarrow> td \<le> typ_uinfo_t TYPE('a)
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; \<not> typ_uinfo_t TYPE('a) \<le> td; uinfo_array_tag_n_m TYPE('a) n n \<le> td\<rbrakk> \<Longrightarrow> td \<le> typ_uinfo_t TYPE('a)
 3. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr; \<not> typ_uinfo_t TYPE('a) \<le> td; uinfo_array_tag_n_m TYPE('a) n n \<le> td\<rbrakk> \<Longrightarrow> td \<le> typ_uinfo_t TYPE('a)
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; arr\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('a) \<le> uinfo_array_tag_n_m TYPE('a) n n
 2. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < size_td td; n * size_of TYPE('a) < addr_card; 0 < n; x \<in> {p..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<in> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False
 2. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (htd_update_list p (typ_slices TYPE('a)) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<in> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False
 2. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>n p. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; \<not> arr; td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<in> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> set (typ_slices TYPE('a)) \<subseteq> list_map ` typ_slice_t (typ_uinfo_t TYPE('a)) ` {..<size_td (typ_info_t TYPE('a))}
 2. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; \<not> arr; td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<in> {p..+size_of TYPE('a)}; \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> False
 3. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; \<not> arr; td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<in> {p..+size_of TYPE('a)}; \<not> td \<bottom>\<^sub>t typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p..+size_of TYPE('a) + n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p + word_of_nat (size_of TYPE('a))..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p + word_of_nat (size_of TYPE('a))..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}; n = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p + word_of_nat (size_of TYPE('a))..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}; n \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>0 < n; x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p + word_of_nat (size_of TYPE('a))..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyp (PTR('a) p) (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd) x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}; n \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n p htd. \<lbrakk>\<And>p htd. \<lbrakk>x \<in> {p..+n * size_of TYPE('a)}; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) p) htd x)\<rbrakk> \<Longrightarrow> False; y < size_td td; size_of TYPE('a) + n * size_of TYPE('a) < addr_card; x \<in> {p + word_of_nat (size_of TYPE('a))..+n * size_of TYPE('a)}; \<not> arr; list_map (typ_slice_t td y) \<subseteq>\<^sub>m snd (ptr_retyps n (PTR('a) (p + word_of_nat (size_of TYPE('a)))) htd x); td \<bottom>\<^sub>t typ_uinfo_t TYPE('a); x \<notin> {p..+size_of TYPE('a)}; 0 < n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!