theory Retype_C

lemma h_t_valid_ptr_retyps_gen_disjoint:
  "\<lbrakk> d \<Turnstile>\<^sub>t p; {ptr_val p..+ size_of TYPE('b)} \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {} \<rbrakk> \<Longrightarrow>
  ptr_retyps_gen n (ptr::'a::mem_type ptr) arr d \<Turnstile>\<^sub>t (p::'b::mem_type ptr)" apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def) apply (drule spec, drule (1) mp) apply (subgoal_tac "ptr_val p + of_nat y \<notin> {ptr_val ptr..+n * size_of TYPE('a)}") apply (simp add: ptr_retyps_gen_out) apply clarsimp apply (drule intvlD) apply (clarsimp simp: disjoint_iff_not_equal ) apply (drule_tac x = "ptr_val p + of_nat y" in bspec) apply (rule intvlI) apply (simp add: size_of_def) apply (drule_tac x = "ptr_val ptr + of_nat k" in bspec) apply (erule intvlI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d \<Turnstile>\<^sub>t p; ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> ptr_retyps_gen n ptr arr d \<Turnstile>\<^sub>t p proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; \<forall>y<size_td (typ_info_t TYPE('b)). list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y)); c_guard p; y < size_td (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y)) \<and> fst (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y)) \<and> fst (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y)) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y)); ptr_val p + word_of_nat y \<notin> {ptr_val ptr..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y)) \<and> fst (ptr_retyps_gen n ptr arr d (ptr_val p + word_of_nat y))
 2. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<notin> {ptr_val ptr..+n * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y))\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<notin> {ptr_val ptr..+n * size_of TYPE('a)} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)); fst (d (ptr_val p + word_of_nat y)); ptr_val p + word_of_nat y \<in> {ptr_val ptr..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>ptr_span p \<inter> {ptr_val ptr..+n * size_of TYPE('a)} = {}; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)); fst (d (ptr_val p + word_of_nat y)); \<exists>k. ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k \<and> k < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>\<forall>x\<in>ptr_span p. \<forall>y\<in>{ptr_val ptr..+n * size_of TYPE('a)}. x \<noteq> y; c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> ptr_val p + word_of_nat y \<in> ptr_span p
 2. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a); \<forall>ya\<in>{ptr_val ptr..+n * size_of TYPE('a)}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> y < size_of TYPE('b)
 2. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a); \<forall>ya\<in>{ptr_val ptr..+n * size_of TYPE('a)}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a); \<forall>ya\<in>{ptr_val ptr..+n * size_of TYPE('a)}. ptr_val p + word_of_nat y \<noteq> ya\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> ptr_val ptr + word_of_nat k \<in> {ptr_val ptr..+n * size_of TYPE('a)}
 2. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a); ptr_val p + word_of_nat y \<noteq> ptr_val ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y k. \<lbrakk>c_guard p; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (d (ptr_val ptr + word_of_nat k)); fst (d (ptr_val ptr + word_of_nat k)); ptr_val p + word_of_nat y = ptr_val ptr + word_of_nat k; k < n * size_of TYPE('a); ptr_val p + word_of_nat y \<noteq> ptr_val ptr + word_of_nat k\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!