theory Detype_C

lemma lift_t_typ_region_bytes:
  assumes doms: "\<And>x :: 'a :: mem_type ptr. \<lbrakk> hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<in> - (Ptr ` {ptr ..+2 ^ bits}) \<rbrakk>
  \<Longrightarrow> {ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}"
  assumes neq_byte: "typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE (word8)"
  shows "(lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) :: 'a :: mem_type typ_heap) =
          lift_t g hp |` (- Ptr ` {ptr ..+2 ^ bits})" apply (rule ext) apply (case_tac "({ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x)") apply (clarsimp simp add: lift_t_def lift_typ_heap_if s_valid_def
                             h_t_valid_typ_region_bytes neq_byte) apply (subgoal_tac "x \<in> - Ptr ` {ptr..+2 ^ bits}") apply clarsimp apply (subst heap_list_s_heap_list') apply (clarsimp simp add: hrs_htd_update h_t_valid_typ_region_bytes neq_byte) apply (erule h_t_valid_taut) apply (subst heap_list_s_heap_list') apply (clarsimp elim!:  h_t_valid_taut) apply simp apply (simp add: image_Ptr) apply (cut_tac p=x in mem_type_self) apply blast apply (simp add: lift_t_def lift_typ_heap_if s_valid_def neq_byte
                   h_t_valid_typ_region_bytes  del: disj_not1 split del: if_split) apply (clarsimp simp add: restrict_map_def) apply (blast dest: doms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) = lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub> proof (prove)
goal (1 subgoal):
 1. \<And>x. lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (2 subgoals):
 1. \<And>x. ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x
 2. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> Some (from_bytes (heap_list_s (lift_state (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x))) = ((\<lambda>p. if hrs_htd hp,g \<Turnstile>\<^sub>t p then Some (from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p))) else None)|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x
 2. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<in> - PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> Some (from_bytes (heap_list_s (lift_state (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x))) = ((\<lambda>p. if hrs_htd hp,g \<Turnstile>\<^sub>t p then Some (from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p))) else None)|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 3. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list_s (lift_state (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val x))
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 3. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) hp),\<lambda>_. True \<Turnstile>\<^sub>t x
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val x))
 3. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 4. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> hrs_htd hp,\<lambda>_. True \<Turnstile>\<^sub>t x
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val x))
 3. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 4. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val x))
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 3. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> hrs_htd hp,\<lambda>_. True \<Turnstile>\<^sub>t x
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val x))
 3. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 4. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> from_bytes (heap_list (hrs_mem (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x)) = from_bytes (heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val x))
 2. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 3. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> x \<in> - PTR('a) ` {ptr..+2 ^ bits}
 2. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x\<rbrakk> \<Longrightarrow> ptr_val x \<notin> {ptr..+2 ^ bits}
 2. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ptr_span x \<inter> {ptr..+2 ^ bits} = {}; hrs_htd hp,g \<Turnstile>\<^sub>t x; ptr_val x \<in> ptr_span x\<rbrakk> \<Longrightarrow> ptr_val x \<notin> {ptr..+2 ^ bits}
 2. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<not> (ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x) \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) x = (lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (1 subgoal):
 1. \<And>x. ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {} \<or> \<not> hrs_htd hp,g \<Turnstile>\<^sub>t x \<Longrightarrow> (if ptr_span x \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x then Some (from_bytes (heap_list_s (lift_state (hrs_htd_update (typ_region_bytes ptr bits) hp)) (size_of TYPE('a)) (ptr_val x))) else None) = ((\<lambda>p. if hrs_htd hp,g \<Turnstile>\<^sub>t p then Some (from_bytes (heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p))) else None)|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub>) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>hrs_htd hp,g \<Turnstile>\<^sub>t x; ptr_span x \<inter> {ptr..+2 ^ bits} \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> PTR('a) ` {ptr..+2 ^ bits} proof (prove)
goal:
No subgoals!