theory Invoke_C

lemma byte_regions_unmodified_actually_heap_list:
  "byte_regions_unmodified hrs hrs'
    \<Longrightarrow> region_actually_is_bytes' p' n' htd
    \<Longrightarrow> htd = (hrs_htd hrs)
    \<Longrightarrow> heap_list (hrs_mem hrs) n p = v
    \<Longrightarrow> {p ..+ n} \<subseteq> {p' ..+ n'}
    \<Longrightarrow> heap_list (hrs_mem hrs') n p = v" apply (erule trans[rotated], rule heap_list_h_eq2) apply (simp add: byte_regions_unmodified_def region_actually_is_bytes_def) apply (drule_tac x=x in spec) apply (drule_tac x=x in bspec) apply blast apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>byte_regions_unmodified hrs hrs'; region_actually_is_bytes' p' n' htd; htd = hrs_htd hrs; heap_list (hrs_mem hrs) n p = v; {p..+n} \<subseteq> {p'..+n'}\<rbrakk> \<Longrightarrow> heap_list (hrs_mem hrs') n p = v proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>byte_regions_unmodified hrs hrs'; region_actually_is_bytes' p' n' htd; htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<longrightarrow> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x; \<forall>x\<in>{p'..+n'}. hrs_htd hrs x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>{p'..+n'}. hrs_htd hrs x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]); htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}; (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<longrightarrow> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}; (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<longrightarrow> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x\<rbrakk> \<Longrightarrow> x \<in> {p'..+n'}
 2. \<And>x. \<lbrakk>htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}; (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<longrightarrow> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x; hrs_htd hrs x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>htd = hrs_htd hrs; {p..+n} \<subseteq> {p'..+n'}; x \<in> {p..+n}; (\<forall>n td. (\<exists>b. snd (hrs_htd hrs x) n = Some (td, b)) \<longrightarrow> td = typ_uinfo_t TYPE(8 word)) \<longrightarrow> (\<exists>a b. snd (hrs_htd hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem hrs' x = hrs_mem hrs x; hrs_htd hrs x = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)])\<rbrakk> \<Longrightarrow> hrs_mem hrs' x = hrs_mem hrs x proof (prove)
goal:
No subgoals!