theory Retype_C

lemma clift_heap_list_update_no_heap_other:
  assumes cleared: "region_is_bytes' p (length xs) (hrs_htd hrs)"
  and not_byte: "typ_uinfo_t TYPE('a :: c_type) \<noteq> typ_uinfo_t TYPE(word8)"
  shows "clift (hrs_mem_update (heap_update_list p xs) hrs) = (clift hrs :: 'a typ_heap)" apply (clarsimp simp: liftt_if[folded hrs_mem_def hrs_htd_def] hrs_mem_update
                        fun_eq_iff h_val_def split: if_split) apply (subst heap_list_update_disjoint_same, simp_all) apply (clarsimp simp: set_eq_iff h_t_valid_def valid_footprint_def Let_def
                 dest!: intvlD[where n="size_of TYPE('a)"]) apply (drule_tac x="of_nat k" in spec, clarsimp simp: size_of_def) 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) apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_mem_update (heap_update_list p xs) hrs) = clift hrs proof (prove)
goal (1 subgoal):
 1. \<And>x. hrs_htd hrs \<Turnstile>\<^sub>t x \<Longrightarrow> from_bytes (heap_list (heap_update_list p xs (hrs_mem hrs)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list (hrs_mem hrs) (size_of TYPE('a)) (ptr_val x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. hrs_htd hrs \<Turnstile>\<^sub>t x \<Longrightarrow> {p..+length xs} \<inter> {ptr_val x..+size_of TYPE('a)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x k. \<lbrakk>0 < size_td (typ_info_t TYPE('a)); \<forall>y<size_td (typ_info_t TYPE('a)). list_map (typ_slice_t (typ_uinfo_t TYPE('a)) y) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val x + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val x + word_of_nat y)); c_guard x; ptr_val x + word_of_nat k \<in> {p..+length xs}; k < size_of TYPE('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x k. \<lbrakk>c_guard x; ptr_val x + word_of_nat k \<in> {p..+length xs}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val x + word_of_nat k)); fst (hrs_htd hrs (ptr_val x + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x k. \<lbrakk>c_guard x; ptr_val x + word_of_nat k \<in> {p..+length xs}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val x + word_of_nat k)); fst (hrs_htd hrs (ptr_val x + 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>x k b i. \<lbrakk>c_guard x; ptr_val x + word_of_nat k \<in> {p..+length xs}; k < size_td (typ_info_t TYPE('a)); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val x + word_of_nat k)); fst (hrs_htd hrs (ptr_val x + 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>x k b i. \<lbrakk>c_guard x; ptr_val x + word_of_nat k \<in> {p..+length xs}; k < size_td (typ_info_t TYPE('a)); fst (hrs_htd hrs (ptr_val x + 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 (hrs_htd hrs (ptr_val x + word_of_nat k)) i = Some (typ_uinfo_t TYPE('a), b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!