theory Retype_C

lemma h_t_valid_intvl_htd_contains_uinfo_t:
  "h_t_valid d g (p :: ('a :: c_type) ptr) \<Longrightarrow> x \<in> {ptr_val p ..+ size_of TYPE('a)} \<Longrightarrow>
    (\<exists>n. snd (d x) n \<noteq> None \<and> fst (the (snd (d x) n)) = typ_uinfo_t TYPE ('a))" apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def intvl_def size_of_def) apply (drule spec, drule(1) mp) 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) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> \<exists>n. snd (d x) n \<noteq> None \<and> fst (the (snd (d x) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat y)) \<and> fst (d (ptr_val p + word_of_nat y)); g p\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat k)) \<and> fst (d (ptr_val p + word_of_nat k))\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat k)) \<and> fst (d (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> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<And>k b i. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat k)); fst (d (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> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (2 subgoals):
 1. \<And>k b i. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; fst (d (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> list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) i = Some (?y23 k b i)
 2. \<And>k b i. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; fst (d (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 (d (ptr_val p + word_of_nat k)) i = Some (?y23 k b i)\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal (1 subgoal):
 1. \<And>k b i. \<lbrakk>k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; g p; fst (d (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 (d (ptr_val p + word_of_nat k)) i = Some (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>a b. snd (d (ptr_val p + word_of_nat k)) n = Some (a, b)) \<and> fst (the (snd (d (ptr_val p + word_of_nat k)) n)) = typ_uinfo_t TYPE('a) proof (prove)
goal:
No subgoals!