theory Retype_C

lemma byte_regions_unmodified_hrs_mem_update2:
  "byte_regions_unmodified hrs hrs'
    \<Longrightarrow> hrs_htd hrs \<Turnstile>\<^sub>t (p :: ('a :: wf_type) ptr)
    \<Longrightarrow> typ_uinfo_t TYPE ('a) \<noteq> typ_uinfo_t TYPE (word8)
    \<Longrightarrow> byte_regions_unmodified (hrs_mem_update (heap_update p v) hrs) hrs'" apply (erule byte_regions_unmodified_trans[rotated], simp_all) apply (clarsimp simp: byte_regions_unmodified_def hrs_mem_update
                        heap_update_def h_t_valid_def
                        valid_footprint_def Let_def) apply (rule sym, rule heap_update_nmem_same) apply (clarsimp simp: size_of_def intvl_def) apply (drule spec, drule(1) mp, clarsimp) apply (cut_tac s="(typ_uinfo_t TYPE('a))" and n=k in ladder_set_self) apply (clarsimp dest!: in_set_list_map) apply (drule(1) map_le_trans) apply (simp add: map_le_def) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>byte_regions_unmodified hrs hrs'; hrs_htd hrs \<Turnstile>\<^sub>t p; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> byte_regions_unmodified (hrs_mem_update (heap_update p v) hrs) hrs' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hrs_htd hrs \<Turnstile>\<^sub>t p; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> byte_regions_unmodified (hrs_mem_update (heap_update p v) hrs) hrs proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); 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 p + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val p + word_of_nat y)); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs x) 0 = Some (a, b)\<rbrakk> \<Longrightarrow> hrs_mem hrs x = heap_update_list (ptr_val p) (to_bytes v (heap_list (hrs_mem hrs) (size_of TYPE('a)) (ptr_val p))) (hrs_mem hrs) x proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); 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 p + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val p + word_of_nat y)); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs x) 0 = Some (a, b)\<rbrakk> \<Longrightarrow> x \<notin> {ptr_val p..+length (to_bytes v (heap_list (hrs_mem hrs) (size_of TYPE('a)) (ptr_val p)))} proof (prove)
goal (1 subgoal):
 1. \<And>a b k. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); \<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 p + word_of_nat y)) \<and> fst (hrs_htd hrs (ptr_val p + word_of_nat y)); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); k < size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b k. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); 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 p + word_of_nat k)); fst (hrs_htd hrs (ptr_val p + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b k. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); 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 p + word_of_nat k)); fst (hrs_htd hrs (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>a b k ba n. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); 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 p + word_of_nat k)); fst (hrs_htd hrs (ptr_val p + word_of_nat k)); [n \<mapsto> (typ_uinfo_t TYPE('a), ba)] \<subseteq>\<^sub>m list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b k ba n. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); 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 p + word_of_nat k)); fst (hrs_htd hrs (ptr_val p + word_of_nat k)); [n \<mapsto> (typ_uinfo_t TYPE('a), ba)] \<subseteq>\<^sub>m snd (hrs_htd hrs (ptr_val p + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b k ba n. \<lbrakk>typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); c_guard p; \<forall>n td. (\<exists>b. snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word); snd (hrs_htd hrs (ptr_val p + word_of_nat k)) 0 = Some (a, b); k < size_td (typ_info_t TYPE('a)); \<forall>a\<in>{0..<length (typ_slice_t (typ_uinfo_t TYPE('a)) k)}. Some (typ_slice_t (typ_uinfo_t TYPE('a)) k ! a) = snd (hrs_htd hrs (ptr_val p + word_of_nat k)) a; fst (hrs_htd hrs (ptr_val p + word_of_nat k)); Some (typ_uinfo_t TYPE('a), ba) = snd (hrs_htd hrs (ptr_val p + word_of_nat k)) n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!