theory Retype_C

lemma h_t_valid_ptr_retyps_gen_same:
  assumes guard: "\<forall>n' < nptrs. gd (CTypesDefs.ptr_add (Ptr p :: 'a ptr) (of_nat n'))"
  assumes cleared: "region_is_bytes' p (nptrs * size_of TYPE('a :: mem_type)) htd"
  and not_byte: "typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(word8)"
  assumes sz: "nptrs * size_of TYPE('a) < addr_card"
  shows
  "h_t_valid (ptr_retyps_gen nptrs (Ptr p :: 'a ptr) arr htd) gd p'
    = ((p' \<in> ((+\<^sub>p) (Ptr p :: 'a ptr) \<circ> int) ` {k. k < nptrs}) \<or> h_t_valid htd gd p')"
  (is "h_t_valid ?htd' gd p' = (p' \<in> ?S \<or> h_t_valid htd gd p')") proof (cases "{ptr_val p' ..+ size_of TYPE('a)} \<inter> {p ..+ nptrs * size_of TYPE('a)} = {}") case True from True have notin:
    "p' \<notin> ?S" apply clarsimp apply (drule_tac x="p + of_nat (x * size_of TYPE('a))" in eqset_imp_iff) apply (simp only: Int_iff empty_iff simp_thms) apply (subst(asm) intvlI, simp) apply (simp add: intvl_self) done from True have same: "\<forall>y < size_of TYPE('a). ?htd' (ptr_val p' + of_nat y)
        = htd (ptr_val p' + of_nat y)" apply clarsimp apply (rule ptr_retyps_gen_out) apply simp apply (blast intro: intvlI) done show ?thesis by (clarsimp simp: h_t_valid_def valid_footprint_def Let_def
                       notin same size_of_def[symmetric, where t="TYPE('a)"]
             cong del: image_cong_simp) next case False from False have nvalid: "\<not> h_t_valid htd gd p'" apply (clarsimp simp: h_t_valid_def valid_footprint_def set_eq_iff
                          Let_def size_of_def[symmetric, where t="TYPE('a)"]
                          intvl_def[where x="(ptr_val p', a)" for a]) apply (drule cleared[unfolded region_is_bytes'_def, THEN bspec]) apply (drule spec, drule(1) mp, clarsimp) 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_all) apply (simp add: not_byte) done have mod_split: "\<And>k. k < nptrs * size_of TYPE('a)
    \<Longrightarrow> \<exists>quot rem. k = quot * size_of TYPE('a) + rem \<and> rem < size_of TYPE('a) \<and> quot < nptrs" apply (intro exI conjI, rule div_mult_mod_eq[symmetric]) apply simp apply (simp add: More_Divides.td_gal_lt) done have gd: "\<And>p'. p' \<in> ?S \<Longrightarrow> gd p'" using guard by auto note htv = h_t_valid_ptr_retyps_gen[where gd=gd, OF sz gd] show ?thesis using False apply (simp add: nvalid) apply (rule iffI, simp_all add: htv) apply (clarsimp simp: set_eq_iff intvl_def[where x="(p, a)" for a]) apply (drule mod_split, clarsimp) apply (frule_tac htv[OF imageI, simplified]) apply fastforce apply (rule ccontr) apply (drule(1) h_t_valid_neq_disjoint) apply simp apply (clarsimp simp: field_of_t_refl) apply (simp add: set_eq_iff) apply (drule spec, drule(1) mp) apply (subst(asm) add.assoc[symmetric], subst(asm) intvlI, assumption) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
goal (2 subgoals):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')
 2. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}

goal (2 subgoals):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')
 2. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (chain)
picking this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} proof (prove)
using this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}

goal (1 subgoal):
 1. p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>{p + word_of_nat x * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} \<inter> {p..+nptrs * size_of TYPE('a)} = {}; p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < nptrs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < nptrs; (p + word_of_nat (x * size_of TYPE('a)) \<in> {p + word_of_nat x * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} \<inter> {p..+nptrs * size_of TYPE('a)}) = (p + word_of_nat (x * size_of TYPE('a)) \<in> {})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < nptrs; \<not> (p + word_of_nat (x * size_of TYPE('a)) \<in> {p + word_of_nat x * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} \<and> p + word_of_nat (x * size_of TYPE('a)) \<in> {p..+nptrs * size_of TYPE('a)})\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p' = PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a))); x < nptrs; \<not> (p + word_of_nat (x * size_of TYPE('a)) \<in> {p + word_of_nat x * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)} \<and> True)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs}

goal (2 subgoals):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')
 2. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (chain)
picking this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} proof (prove)
using this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}

goal (1 subgoal):
 1. \<forall>y<size_of TYPE('a). ptr_retyps_gen nptrs (PTR('a) p) arr htd (ptr_val p' + word_of_nat y) = htd (ptr_val p' + word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}; y < size_of TYPE('a)\<rbrakk> \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd (ptr_val p' + word_of_nat y) = htd (ptr_val p' + word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}; y < size_of TYPE('a)\<rbrakk> \<Longrightarrow> ptr_val p' + word_of_nat y \<notin> {ptr_val (PTR('a) p)..+nptrs * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {}; y < size_of TYPE('a)\<rbrakk> \<Longrightarrow> ptr_val p' + word_of_nat y \<notin> {p..+nptrs * size_of TYPE('a)} proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>y<size_of TYPE('a). ptr_retyps_gen nptrs (PTR('a) p) arr htd (ptr_val p' + word_of_nat y) = htd (ptr_val p' + word_of_nat y)

goal (2 subgoals):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} = {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')
 2. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
goal (1 subgoal):
 1. ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
this:
ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {}

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (chain)
picking this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} proof (prove)
using this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {}

goal (1 subgoal):
 1. \<not> htd,gd \<Turnstile>\<^sub>t p' proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_val p' + word_of_nat k \<in> {p..+nptrs * size_of TYPE('a)}; k < size_of TYPE('a); \<forall>y<size_of TYPE('a). 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)); gd p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_of TYPE('a); \<forall>y<size_of TYPE('a). 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)); gd p'; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (htd (ptr_val p' + word_of_nat k)) n \<noteq> Some (td, b))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_of TYPE('a); gd p'; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (htd (ptr_val p' + word_of_nat k)) n \<noteq> Some (td, b)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat k)); fst (htd (ptr_val p' + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_of TYPE('a); gd p'; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (htd (ptr_val p' + word_of_nat k)) n \<noteq> Some (td, b)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat k)); fst (htd (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>k < size_of TYPE('a); gd p'; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (htd (ptr_val p' + word_of_nat k)) n \<noteq> Some (td, b)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (htd (ptr_val p' + word_of_nat k)); fst (htd (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>k < size_of TYPE('a); gd p'; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (htd (ptr_val p' + word_of_nat k)) n \<noteq> Some (td, b)); fst (htd (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 (htd (ptr_val p' + word_of_nat k)) i = Some (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<not> htd,gd \<Turnstile>\<^sub>t p'

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
goal (1 subgoal):
 1. \<And>k. k < nptrs * size_of TYPE('a) \<Longrightarrow> \<exists>quot rem. k = quot * size_of TYPE('a) + rem \<and> rem < size_of TYPE('a) \<and> quot < nptrs proof (prove)
goal (2 subgoals):
 1. \<And>k. k < nptrs * size_of TYPE('a) \<Longrightarrow> k mod size_of TYPE('a) < size_of TYPE('a)
 2. \<And>k. k < nptrs * size_of TYPE('a) \<Longrightarrow> k div size_of TYPE('a) < nptrs proof (prove)
goal (1 subgoal):
 1. \<And>k. k < nptrs * size_of TYPE('a) \<Longrightarrow> k div size_of TYPE('a) < nptrs proof (prove)
goal:
No subgoals! proof (state)
this:
?k2 < nptrs * size_of TYPE('a) \<Longrightarrow> \<exists>quot rem. ?k2 = quot * size_of TYPE('a) + rem \<and> rem < size_of TYPE('a) \<and> quot < nptrs

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
goal (1 subgoal):
 1. \<And>p'. p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<Longrightarrow> gd p' proof (prove)
using this:
\<forall>n'<nptrs. gd (PTR('a) p +\<^sub>p int n')

goal (1 subgoal):
 1. \<And>p'. p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<Longrightarrow> gd p' proof (state)
this:
?p'2 \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<Longrightarrow> gd ?p'2

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (state)
this:
\<lbrakk>?p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs}; ?p' \<in> ((+\<^sub>p) (PTR('a) ?p) \<circ> int) ` {k. k < nptrs}\<rbrakk> \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) ?p) ?arr ?htd,gd \<Turnstile>\<^sub>t ?p'

goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
goal (1 subgoal):
 1. ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
using this:
ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {}

goal (1 subgoal):
 1. ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p') proof (prove)
goal (1 subgoal):
 1. ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {} \<Longrightarrow> ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_span p' \<inter> {p..+nptrs * size_of TYPE('a)} \<noteq> {}; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + word_of_nat k \<in> ptr_span p'; k < nptrs * size_of TYPE('a)\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} proof (prove)
goal (2 subgoals):
 1. \<And>quot rem. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs\<rbrakk> \<Longrightarrow> PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))) \<in> (\<lambda>x. PTR('a) (?p21 quot rem + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}
 2. \<And>quot rem. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) (?p21 quot rem)) (?arr21 quot rem) (?htd21 quot rem),gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a)))\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) (?arr21 quot rem) (?htd21 quot rem),gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a)))\<rbrakk> \<Longrightarrow> p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs} proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p'; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) (?arr21 quot rem) (?htd21 quot rem),gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}\<rbrakk> \<Longrightarrow> \<not> TYPE('a) <\<^sub>\<tau> TYPE('a)
 2. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}\<rbrakk> \<Longrightarrow> \<not> field_of_t p' (PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))))
 3. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; ptr_span p' \<inter> ptr_span (PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a)))) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}\<rbrakk> \<Longrightarrow> \<not> field_of_t p' (PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))))
 2. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; ptr_span p' \<inter> ptr_span (PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a)))) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; ptr_span p' \<inter> ptr_span (PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a)))) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<forall>x. x \<in> ptr_span p' \<longrightarrow> x \<notin> {p + word_of_nat quot * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<notin> {p + word_of_nat quot * word_of_nat (size_of TYPE('a))..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>quot rem. \<lbrakk>p + (word_of_nat quot * word_of_nat (size_of TYPE('a)) + word_of_nat rem) \<in> ptr_span p'; rem < size_of TYPE('a); quot < nptrs; ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t PTR('a) (p + word_of_nat quot * word_of_nat (size_of TYPE('a))); p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < nptrs}; \<not> True\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_retyps_gen nptrs (PTR('a) p) arr htd,gd \<Turnstile>\<^sub>t p' = (p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < nptrs} \<or> htd,gd \<Turnstile>\<^sub>t p')

goal:
No subgoals!