theory Retype_C

lemma typ_region_bytes_dom:
 "typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE (word8)
    \<Longrightarrow> dom (clift (hrs_htd_update (typ_region_bytes ptr bits) hp) :: 'b :: mem_type typ_heap)
  \<subseteq>  dom ((clift hp) :: 'b :: mem_type typ_heap)" apply (clarsimp simp: liftt_if split: if_splits) apply (case_tac "{ptr_val x ..+ size_of TYPE('b)} \<inter> {ptr ..+ 2 ^ bits} = {}") apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def
                         hrs_htd_update_def split_def typ_region_bytes_def) apply (drule spec, drule(1) mp) apply (simp add: size_of_def split: if_split_asm) apply (drule subsetD[OF equalityD1], rule IntI, erule intvlI, simp) apply simp apply (clarsimp simp: set_eq_iff) apply (drule(1) h_t_valid_intvl_htd_contains_uinfo_t) apply (clarsimp simp: hrs_htd_update_def typ_region_bytes_def split_def
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word) \<Longrightarrow> dom (clift (hrs_htd_update (typ_region_bytes ptr bits) hp)) \<subseteq> dom (clift hp) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x
 2. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); ptr_span x \<inter> {ptr..+2 ^ bits} = {}; \<forall>y<size_td (typ_info_t TYPE('b)). list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (if ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else snd hp (ptr_val x + word_of_nat y)) \<and> fst (if ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else snd hp (ptr_val x + word_of_nat y)); c_guard x; 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 (snd hp (ptr_val x + word_of_nat y)) \<and> fst (snd hp (ptr_val x + word_of_nat y))
 2. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); ptr_span x \<inter> {ptr..+2 ^ bits} = {}; c_guard x; y < size_td (typ_info_t TYPE('b)); list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (if ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else snd hp (ptr_val x + word_of_nat y)) \<and> fst (if ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else snd hp (ptr_val x + word_of_nat y))\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (snd hp (ptr_val x + word_of_nat y)) \<and> fst (snd hp (ptr_val x + word_of_nat y))
 2. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); {ptr_val x..+size_td (typ_info_t TYPE('b))} \<inter> {ptr..+2 ^ bits} = {}; c_guard x; y < size_td (typ_info_t TYPE('b)); ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits}; list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (snd hp (ptr_val x + word_of_nat y)) \<and> fst (snd hp (ptr_val x + word_of_nat y))
 2. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); c_guard x; y < size_td (typ_info_t TYPE('b)); ptr_val x + word_of_nat y \<in> {ptr..+2 ^ bits}; list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]; ptr_val x + word_of_nat y \<in> {}\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (typ_uinfo_t TYPE('b)) y) \<subseteq>\<^sub>m snd (snd hp (ptr_val x + word_of_nat y)) \<and> fst (snd hp (ptr_val x + word_of_nat y))
 2. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); snd (hrs_htd_update (typ_region_bytes ptr bits) hp) \<Turnstile>\<^sub>t x; xa \<in> ptr_span x; xa \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>typ_uinfo_t TYPE('b) \<noteq> typ_uinfo_t TYPE(8 word); xa \<in> ptr_span x; xa \<in> {ptr..+2 ^ bits}; \<exists>n. snd (snd (hrs_htd_update (typ_region_bytes ptr bits) hp) xa) n \<noteq> None \<and> fst (the (snd (snd (hrs_htd_update (typ_region_bytes ptr bits) hp) xa) n)) = typ_uinfo_t TYPE('b)\<rbrakk> \<Longrightarrow> snd hp \<Turnstile>\<^sub>t x proof (prove)
goal:
No subgoals!