theory Retype_C

lemma cslift_bytes_mem_update:
  fixes x :: cstate and sz and ptr
  defines "x' \<equiv> x\<lparr>globals := globals x
                       \<lparr>t_hrs_' := hrs_mem_update (heap_update_list ptr (replicate sz 0)) (t_hrs_' (globals x))\<rparr>\<rparr>"
  assumes bytes: "region_is_bytes ptr sz x"
  assumes not_byte: "typ_uinfo_t TYPE ('a) \<noteq> typ_uinfo_t TYPE (word8)"
  shows "(cslift x' :: ('a :: mem_type) ptr \<Rightarrow> _)
     = clift (fst (t_hrs_' (globals x)), snd (t_hrs_' (globals x)))" using bytes apply (unfold region_is_bytes'_def) apply (rule ext) apply (simp only: lift_t_if hrs_mem_update_def split_def x'_def) apply (simp add: lift_t_if hrs_mem_update_def split_def) apply (clarsimp simp: h_val_def split: if_split) apply (subst heap_list_update_disjoint_same) apply simp apply (rule disjointI) apply clarsimp apply (drule (1) bspec) apply (frule (1) h_t_valid_intvl_htd_contains_uinfo_t) apply (clarsimp simp: hrs_htd_def not_byte) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cslift x' = clift (fst (t_hrs_' (globals x)), snd (t_hrs_' (globals x))) proof (prove)
using this:
region_is_bytes ptr sz x

goal (1 subgoal):
 1. cslift x' = clift (fst (t_hrs_' (globals x)), snd (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)) \<Longrightarrow> cslift x' = clift (fst (t_hrs_' (globals x)), snd (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)) \<Longrightarrow> cslift x' xa = clift (fst (t_hrs_' (globals x)), snd (t_hrs_' (globals x))) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)) \<Longrightarrow> cslift (x\<lparr>globals := globals x\<lparr>t_hrs_' := (heap_update_list ptr (replicate sz 0) (fst (t_hrs_' (globals x))), snd (t_hrs_' (globals x)))\<rparr>\<rparr>) xa = (if snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa then Some (h_val (fst (t_hrs_' (globals x))) xa) else None) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)) \<Longrightarrow> (if snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa then Some (h_val (heap_update_list ptr (replicate sz 0) (fst (t_hrs_' (globals x)))) xa) else None) = (if snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa then Some (h_val (fst (t_hrs_' (globals x))) xa) else None) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list ptr (replicate sz 0) (fst (t_hrs_' (globals x)))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> {ptr..+length (replicate sz 0)} \<inter> ptr_span xa = {}
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> {ptr..+sz} \<inter> ptr_span xa = {}
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa xaa y. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa; xaa \<in> {ptr..+sz}; y \<in> ptr_span xa\<rbrakk> \<Longrightarrow> xaa \<noteq> y
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa; y \<in> {ptr..+sz}; y \<in> ptr_span xa\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa; y \<in> {ptr..+sz}; y \<in> ptr_span xa; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) y) n \<noteq> Some (td, b))\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (2 subgoals):
 1. \<And>xa y. \<lbrakk>snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa; y \<in> {ptr..+sz}; y \<in> ptr_span xa; \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) y) n \<noteq> Some (td, b)); \<exists>n. snd (snd (t_hrs_' (globals x)) y) n \<noteq> None \<and> fst (the (snd (snd (t_hrs_' (globals x)) y) n)) = typ_uinfo_t TYPE('a)\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>z\<in>{ptr..+sz}. \<forall>td. td \<noteq> typ_uinfo_t TYPE(8 word) \<longrightarrow> (\<forall>n b. snd (hrs_htd (t_hrs_' (globals x)) z) n \<noteq> Some (td, b)); snd (t_hrs_' (globals x)) \<Turnstile>\<^sub>t xa\<rbrakk> \<Longrightarrow> from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) = from_bytes (heap_list (fst (t_hrs_' (globals x))) (size_of TYPE('a)) (ptr_val xa)) proof (prove)
goal:
No subgoals!