theory Retype_C

lemma lift_t_typ_region_bytes_none:
  "\<lbrakk> \<And>x (v :: 'a). lift_t g hp x = Some v
    \<Longrightarrow> {ptr_val x ..+ size_of TYPE('a)} \<inter> {ptr ..+ 2 ^ bits} = {};
     typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word) \<rbrakk> \<Longrightarrow>
  lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp)
    = (lift_t g hp :: (('a :: mem_type) ptr) \<Rightarrow> _)" apply atomize apply (subst lift_t_typ_region_bytes, simp_all) apply (clarsimp simp: liftt_if hrs_htd_def split: if_splits) apply (rule ext, simp add: restrict_map_def) apply (rule ccontr, clarsimp split: if_splits) apply (clarsimp simp: liftt_if hrs_htd_def split: if_splits) apply (clarsimp simp: set_eq_iff intvl_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x v. lift_t g hp x = Some v \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) = lift_t g hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x v. lift_t g hp x = Some v \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) = lift_t g hp proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. (\<exists>v. lift_t g hp x = Some v) \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<notin> PTR('a) ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}
 2. \<lbrakk>\<forall>x. (\<exists>v. lift_t g hp x = Some v) \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub> = lift_t g hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (\<exists>v. lift_t g hp x = Some v) \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> lift_t g hp|\<^bsub>(- PTR('a) ` {ptr..+2 ^ bits})\<^esub> = lift_t g hp proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. (\<exists>v. lift_t g hp x = Some v) \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> (if x \<notin> PTR('a) ` {ptr..+2 ^ bits} then lift_t g hp x else None) = lift_t g hp x proof (prove)
goal (1 subgoal):
 1. \<And>xa y. \<lbrakk>\<forall>x. (\<exists>v. lift_t g hp x = Some v) \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); xa \<in> {ptr..+2 ^ bits}; lift_t g hp (PTR('a) xa) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>x. snd hp,g \<Turnstile>\<^sub>t x \<longrightarrow> ptr_span x \<inter> {ptr..+2 ^ bits} = {}; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); xa \<in> {ptr..+2 ^ bits}; snd hp,g \<Turnstile>\<^sub>t PTR('a) xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!