kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_C

lemma h_t_array_valid_typ_region_bytes:
  "h_t_array_valid htd (p :: ('a :: c_type) ptr) n
    \<Longrightarrow> {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}
    \<Longrightarrow> h_t_array_valid (typ_region_bytes ptr bits htd) p n" apply (clarsimp simp: h_t_array_valid_def) apply (subst valid_footprint_typ_region_bytes) apply (simp add: uinfo_array_tag_n_m_def typ_uinfo_t_def typ_info_word) apply (simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h_t_array_valid htd p n; {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> h_t_array_valid (typ_region_bytes ptr bits htd) p n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n); {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> valid_footprint (typ_region_bytes ptr bits htd) (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n); {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> uinfo_array_tag_n_m TYPE('a) n n \<noteq> typ_uinfo_t TYPE(8 word)
 2. \<lbrakk>valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n); {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_td (uinfo_array_tag_n_m TYPE('a) n n)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n); {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> {ptr_val p..+size_td (uinfo_array_tag_n_m TYPE('a) n n)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint htd (ptr_val p) (uinfo_array_tag_n_m TYPE('a) n n) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma cvariable_array_map_relation_detype:
  "cvariable_array_map_relation mp szs ptrfun htd
    \<Longrightarrow> ptrfun = (Ptr :: _ \<Rightarrow> ('a :: c_type ptr))
    \<Longrightarrow> \<forall>p v. mp p = Some v \<longrightarrow> p \<notin> {ptr ..+ 2 ^ bits}
        \<longrightarrow> {p ..+ szs v * size_of TYPE('a)} \<inter> {ptr ..+ 2 ^ bits} = {}
    \<Longrightarrow> cvariable_array_map_relation (mp |` (- {ptr..+2 ^ bits}))
        szs ptrfun (typ_region_bytes ptr bits htd)" apply (clarsimp simp: cvariable_array_map_relation_def restrict_map_def) apply (elim allE, (drule(1) mp)+) apply (simp add: h_t_array_valid_typ_region_bytes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cvariable_array_map_relation mp szs ptrfun htd; ptrfun = PTR('a); \<forall>p v. mp p = Some v \<longrightarrow> p \<notin> {ptr..+2 ^ bits} \<longrightarrow> {p..+szs v * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> cvariable_array_map_relation (mp|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) szs ptrfun (typ_region_bytes ptr bits htd) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>\<forall>p v. mp p = Some v \<longrightarrow> h_t_array_valid htd (PTR('a) p) (szs v); ptrfun = PTR('a); \<forall>p v. mp p = Some v \<longrightarrow> p \<notin> {ptr..+2 ^ bits} \<longrightarrow> {p..+szs v * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}; p \<notin> {ptr..+2 ^ bits}; mp p = Some v\<rbrakk> \<Longrightarrow> h_t_array_valid (typ_region_bytes ptr bits htd) (PTR('a) p) (szs v) proof (prove)
goal (1 subgoal):
 1. \<And>p v. \<lbrakk>ptrfun = PTR('a); p \<notin> {ptr..+2 ^ bits}; mp p = Some v; h_t_array_valid htd (PTR('a) p) (szs v); {p..+szs v * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> h_t_array_valid (typ_region_bytes ptr bits htd) (PTR('a) p) (szs v) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma zero_ranges_are_zero_typ_region_bytes:
  "zero_ranges_are_zero rs hrs
    \<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs)" apply (clarsimp simp: zero_ranges_are_zero_def) apply (drule(1) bspec) apply (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def hrs_htd_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zero_ranges_are_zero rs hrs \<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>rs. case x of (start, end) \<Rightarrow> region_actually_is_bytes' start (unat (end + 1 - start)) (hrs_htd hrs) \<and> heap_list (hrs_mem hrs) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> rs\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) hrs)) \<and> heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rs; case (a, b) of (start, end) \<Rightarrow> region_actually_is_bytes' start (unat (end + 1 - start)) (hrs_htd hrs) \<and> heap_list (hrs_mem hrs) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) hrs)) \<and> heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal:
No subgoals!
theory Detype_C

lemma kernel_data_refs_domain_eq_rotate:
  "(kernel_data_refs = - domain) = (domain = - kernel_data_refs)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (kernel_data_refs = - domain) = (domain = - kernel_data_refs)
theory Retype_C

lemma c_guard_word8:
  "c_guard (p :: word8 ptr) = (ptr_val p \<noteq> 0)" unfolding c_guard_def ptr_aligned_def c_null_guard_def apply simp apply (rule iffI) apply (drule intvlD) apply clarsimp apply simp apply (rule intvl_self) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p = (ptr_val p \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. (align_of TYPE(8 word) dvd unat (ptr_val p) \<and> 0 \<notin> ptr_span p) = (ptr_val p \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. (0 \<in> {ptr_val p..+Suc 0}) = (ptr_val p = 0) proof (prove)
goal (2 subgoals):
 1. 0 \<in> {ptr_val p..+Suc 0} \<Longrightarrow> ptr_val p = 0
 2. ptr_val p = 0 \<Longrightarrow> 0 \<in> {ptr_val p..+Suc 0} proof (prove)
goal (2 subgoals):
 1. \<exists>k. 0 = ptr_val p + word_of_nat k \<and> k < Suc 0 \<Longrightarrow> ptr_val p = 0
 2. ptr_val p = 0 \<Longrightarrow> 0 \<in> {ptr_val p..+Suc 0} proof (prove)
goal (1 subgoal):
 1. ptr_val p = 0 \<Longrightarrow> 0 \<in> {ptr_val p..+Suc 0} proof (prove)
goal (1 subgoal):
 1. ptr_val p = 0 \<Longrightarrow> 0 \<in> {0..+Suc 0} proof (prove)
goal (1 subgoal):
 1. ptr_val p = 0 \<Longrightarrow> 0 < Suc 0 proof (prove)
goal:
No subgoals!
theory Retype_C

lemma heap_update_list_append3:
    "\<lbrakk> s' = s + of_nat (length xs) \<rbrakk> \<Longrightarrow> heap_update_list s (xs @ ys) H = heap_update_list s' ys (heap_update_list s xs H)" apply simp apply (subst heap_update_list_append [symmetric]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' = s + word_of_nat (length xs) \<Longrightarrow> heap_update_list s (xs @ ys) H = heap_update_list s' ys (heap_update_list s xs H) proof (prove)
goal (1 subgoal):
 1. s' = s + word_of_nat (length xs) \<Longrightarrow> heap_update_list s (xs @ ys) H = heap_update_list (s + word_of_nat (length xs)) ys (heap_update_list s xs H) proof (prove)
goal (1 subgoal):
 1. s' = s + word_of_nat (length xs) \<Longrightarrow> heap_update_list s (xs @ ys) H = heap_update_list s (xs @ ys) H proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ptr_aligned_word32:
  "\<lbrakk> is_aligned p 2  \<rbrakk> \<Longrightarrow> ptr_aligned ((Ptr p) :: word32 ptr)" apply (clarsimp simp: is_aligned_def ptr_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p 2 \<Longrightarrow> ptr_aligned (PTR(32 word) p) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma c_guard_word32:
  "\<lbrakk> is_aligned (ptr_val p) 2; p \<noteq> NULL  \<rbrakk> \<Longrightarrow> c_guard (p :: (word32 ptr))" apply (clarsimp simp: c_guard_def) apply (rule conjI) apply (case_tac p, clarsimp simp: ptr_aligned_word32) apply (case_tac p, simp add: c_null_guard_def) apply (subst intvl_aligned_bottom_eq [where n=2 and bits=2], auto simp: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (ptr_val p) 2; p \<noteq> NULL\<rbrakk> \<Longrightarrow> c_guard p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (ptr_val p) 2; p \<noteq> NULL\<rbrakk> \<Longrightarrow> ptr_aligned p \<and> c_null_guard p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (ptr_val p) 2; p \<noteq> NULL\<rbrakk> \<Longrightarrow> ptr_aligned p
 2. \<lbrakk>is_aligned (ptr_val p) 2; p \<noteq> NULL\<rbrakk> \<Longrightarrow> c_null_guard p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (ptr_val p) 2; p \<noteq> NULL\<rbrakk> \<Longrightarrow> c_null_guard p proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned x 2; x \<noteq> 0; p = PTR(32 word) x\<rbrakk> \<Longrightarrow> 0 \<notin> {x..+4} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma is_aligned_and_not_zero: "\<lbrakk> is_aligned n k; n \<noteq> 0 \<rbrakk> \<Longrightarrow> 2^k \<le> n" apply (metis aligned_small_is_0 word_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned n k; n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ k \<le> n proof (prove)
goal:
No subgoals!
theory Retype_C

lemma heap_update_list_replicate:
  "\<lbrakk> set L = {0}; n' = n + length L \<rbrakk> \<Longrightarrow>  heap_update_list s ((replicate n 0) @ L) H = heap_update_list s (replicate n' 0) H" apply (subst replicate_append_list) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set L = {0}; n' = n + length L\<rbrakk> \<Longrightarrow> heap_update_list s (replicate n 0 @ L) H = heap_update_list s (replicate n' 0) H proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set L = {0}; n' = n + length L\<rbrakk> \<Longrightarrow> set L \<subseteq> {0}
 2. \<lbrakk>set L = {0}; n' = n + length L\<rbrakk> \<Longrightarrow> heap_update_list s (replicate (n + length L) 0) H = heap_update_list s (replicate n' 0) H proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set L = {0}; n' = n + length L\<rbrakk> \<Longrightarrow> heap_update_list s (replicate (n + length L) 0) H = heap_update_list s (replicate n' 0) H proof (prove)
goal:
No subgoals!
theory Retype_C

lemma heap_update_word32_is_heap_update_list:
  "heap_update p (x :: word32) = heap_update_list (ptr_val p) (to_bytes x a)" apply (rule ext)+ apply (clarsimp simp: heap_update_def) apply (clarsimp simp: to_bytes_def typ_info_word) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update p x = heap_update_list (ptr_val p) (to_bytes x a) proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. heap_update p x xa xaa = heap_update_list (ptr_val p) (to_bytes x a) xa xaa proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. heap_update_list (ptr_val p) (to_bytes x (heap_list xa 4 (ptr_val p))) xa xaa = heap_update_list (ptr_val p) (to_bytes x a) xa xaa proof (prove)
goal:
No subgoals!
theory Retype_C

lemma to_bytes_word32_0:
  "to_bytes (0 :: word32) xs = [0, 0, 0, 0 :: word8]" by (simp add: to_bytes_def typ_info_word word_rsplit_same word_rsplit_0 word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bytes 0 xs = [0, 0, 0, 0]
theory Retype_C

lemma globals_list_distinct_subset:
  "\<lbrakk> globals_list_distinct D symtab xs; D' \<subseteq> D \<rbrakk>
    \<Longrightarrow> globals_list_distinct D' symtab xs" by (simp add: globals_list_distinct_def disjoint_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>globals_list_distinct D symtab xs; D' \<subseteq> D\<rbrakk> \<Longrightarrow> globals_list_distinct D' symtab xs
theory Retype_C

lemma is_aligned_and_2_to_k:
  assumes  mask_2_k: "(n && 2 ^ k - 1) = 0"
  shows "is_aligned (n :: word32) k" proof (subst is_aligned_mask) have "mask k = (2 :: word32) ^ k - 1" by (clarsimp simp: mask_def) thus "n && mask k = 0" using mask_2_k by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned n k proof (state)
goal (1 subgoal):
 1. n && mask k = 0 proof (prove)
goal (1 subgoal):
 1. mask k = 2 ^ k - 1 proof (state)
this:
mask k = 2 ^ k - 1

goal (1 subgoal):
 1. n && mask k = 0 proof (prove)
using this:
mask k = 2 ^ k - 1

goal (1 subgoal):
 1. n && mask k = 0 proof (prove)
using this:
mask k = 2 ^ k - 1
n && 2 ^ k - 1 = 0

goal (1 subgoal):
 1. n && mask k = 0 proof (state)
this:
n && mask k = 0

goal:
No subgoals!
theory Retype_C

lemma dvd_4_iff_and_mask_eq_0:
  \<open>4 dvd a \<longleftrightarrow> a && mask 2 = 0\<close> for a :: \<open>'a::len word\<close> using take_bit_eq_0_iff [of 2 a] by (simp add: take_bit_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (4 dvd a) = (a && mask 2 = 0) proof (prove)
using this:
(take_bit 2 a = 0) = (2\<^sup>2 dvd a)

goal (1 subgoal):
 1. (4 dvd a) = (a && mask 2 = 0)
theory Retype_C

lemma snd_when_aligneError[simp]:
  shows "(snd ((when P (alignError sz)) s)) = P" by (simp add: when_def alignError_def fail_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. snd (when P (alignError sz) s) = P
theory Retype_C

lemma lift_t_retyp_heap_same:
  fixes p :: "'a :: mem_type ptr"
  assumes gp: "g p"
  shows "lift_t g (hp, ptr_retyp p td) p = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)))" apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def) apply (subst ptr_retyp_h_t_valid) apply (rule gp) apply simp apply (subst heap_list_s_heap_list_dom) apply (clarsimp simp: s_footprint_intvl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g (hp, ptr_retyp p td) p = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p))) proof (prove)
goal (1 subgoal):
 1. (if ptr_retyp p td,g \<Turnstile>\<^sub>t p then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('a)) (ptr_val p))) else None) = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p))) proof (prove)
goal (2 subgoals):
 1. g p
 2. (if True then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('a)) (ptr_val p))) else None) = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p))) proof (prove)
goal (1 subgoal):
 1. (if True then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('a)) (ptr_val p))) else None) = Some (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p))) proof (prove)
goal (1 subgoal):
 1. from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('a)) (ptr_val p)) = from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)) proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. (x, SIndexVal)) ` ptr_span p \<subseteq> dom_s (ptr_retyp p td)
 2. from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)) = from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)) proof (prove)
goal (1 subgoal):
 1. from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)) = from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma lift_t_retyp_heap_same_rep0:
  fixes p :: "'a :: mem_type ptr"
  assumes gp: "g p"
  shows "lift_t g (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp, ptr_retyp p td) p =
  Some (from_bytes (replicate (size_of TYPE('a)) 0))" apply (subst lift_t_retyp_heap_same) apply (rule gp) apply (subst heap_list_update [where v = "replicate (size_of TYPE('a)) 0", simplified]) apply (rule order_less_imp_le) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp, ptr_retyp p td) p = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal (2 subgoals):
 1. g p
 2. Some (from_bytes (heap_list (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp) (size_of TYPE('a)) (ptr_val p))) = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal (1 subgoal):
 1. Some (from_bytes (heap_list (heap_update_list (ptr_val p) (replicate (size_of TYPE('a)) 0) hp) (size_of TYPE('a)) (ptr_val p))) = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal (2 subgoals):
 1. size_of TYPE('a) \<le> addr_card
 2. Some (from_bytes (replicate (size_of TYPE('a)) 0)) = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal (2 subgoals):
 1. size_of TYPE('a) < addr_card
 2. Some (from_bytes (replicate (size_of TYPE('a)) 0)) = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal (1 subgoal):
 1. Some (from_bytes (replicate (size_of TYPE('a)) 0)) = Some (from_bytes (replicate (size_of TYPE('a)) 0)) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma lift_t_retyp_heap_other2:
  fixes p :: "'a :: mem_type ptr" and p' :: "'b :: mem_type ptr"
  assumes orth: "{ptr_val p..+size_of TYPE('a)} \<inter> {ptr_val p'..+size_of TYPE('b)} = {}"
  shows "lift_t g (hp, ptr_retyp p td) p' = lift_t g (hp, td) p'" apply (simp add: lift_t_def lift_typ_heap_if s_valid_def hrs_htd_def ptr_retyp_disjoint_iff [OF orth]) apply (cases "td, g \<Turnstile>\<^sub>t p'") apply simp apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
     ptr_retyp_disjoint_iff orth) apply (simp add: h_t_valid_taut heap_list_s_heap_list heap_list_update_disjoint_same
    ptr_retyp_disjoint_iff orth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g (hp, ptr_retyp p td) p' = lift_t g (hp, td) p' proof (prove)
goal (1 subgoal):
 1. (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p'))) else None) = (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))) else None) proof (prove)
goal (2 subgoals):
 1. td,g \<Turnstile>\<^sub>t p' \<Longrightarrow> (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p'))) else None) = (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))) else None)
 2. \<not> td,g \<Turnstile>\<^sub>t p' \<Longrightarrow> (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p'))) else None) = (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))) else None) proof (prove)
goal (2 subgoals):
 1. td,g \<Turnstile>\<^sub>t p' \<Longrightarrow> from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p')) = from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))
 2. \<not> td,g \<Turnstile>\<^sub>t p' \<Longrightarrow> (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p'))) else None) = (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))) else None) proof (prove)
goal (1 subgoal):
 1. \<not> td,g \<Turnstile>\<^sub>t p' \<Longrightarrow> (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, ptr_retyp p td)) (size_of TYPE('b)) (ptr_val p'))) else None) = (if td,g \<Turnstile>\<^sub>t p' then Some (from_bytes (heap_list_s (lift_state (hp, td)) (size_of TYPE('b)) (ptr_val p'))) else None) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma h_t_valid_not_empty:
  fixes p :: "'a :: c_type ptr"
  shows "\<lbrakk> d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)} \<rbrakk> \<Longrightarrow> snd (d x) \<noteq> Map.empty" apply (drule intvlD) apply (clarsimp simp: h_t_valid_def size_of_def) apply (drule valid_footprintD) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)}\<rbrakk> \<Longrightarrow> snd (d x) \<noteq> (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d,g \<Turnstile>\<^sub>t p; \<exists>k. x = ptr_val p + word_of_nat k \<and> k < size_of TYPE('a)\<rbrakk> \<Longrightarrow> snd (d x) \<noteq> (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>valid_footprint d (ptr_val p) (typ_uinfo_t TYPE('a)); g p; k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; snd (d (ptr_val p + word_of_nat k)) = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>g p; k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; snd (d (ptr_val p + word_of_nat k)) = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> ?y8 k < size_td (typ_uinfo_t TYPE('a))
 2. \<And>k. \<lbrakk>g p; k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; snd (d (ptr_val p + word_of_nat k)) = (\<lambda>x. None); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) (?y8 k)) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat (?y8 k))) \<and> fst (d (ptr_val p + word_of_nat (?y8 k)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>g p; k < size_td (typ_info_t TYPE('a)); x = ptr_val p + word_of_nat k; snd (d (ptr_val p + word_of_nat k)) = (\<lambda>x. None); list_map (typ_slice_t (typ_uinfo_t TYPE('a)) k) \<subseteq>\<^sub>m snd (d (ptr_val p + word_of_nat k)) \<and> fst (d (ptr_val p + word_of_nat k))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_C

lemma image_add_intvl:
  "((+) x) ` {p ..+ n} = {p + x ..+ n}" by (auto simp add: intvl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (+) x ` {p..+n} = {p + x..+n}
theory Retype_C

lemma intvl_Suc_right:
  "{p ..+ Suc n} = {p} \<union> {(p :: ('a :: len) word) + 1 ..+ n}" apply (simp add: intvl_sum[where p=p and i=1 and j=n, simplified]) apply (auto dest: intvl_Suc simp: intvl_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {p..+Suc n} = {p} \<union> {p + 1..+n} proof (prove)
goal (1 subgoal):
 1. {p..+Suc 0} \<union> {p + 1..+n} = insert p {p + 1..+n} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma htd_update_list_same2:
  "x \<notin> {p ..+ length xs} \<Longrightarrow>
    htd_update_list p xs htd x = htd x" by (induct xs arbitrary: p htd, simp_all add: intvl_Suc_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {p..+length xs} \<Longrightarrow> htd_update_list p xs htd x = htd x
theory Retype_C

lemma ptr_retyps_gen_out:
  fixes p :: "'a :: mem_type ptr"
  shows "x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps_gen n p arr td x = td x" apply (simp add: ptr_retyps_gen_def ptr_retyps_out split: if_split) apply (clarsimp simp: ptr_arr_retyps_def htd_update_list_same2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_retyps_gen n p arr td x = td x proof (prove)
goal (1 subgoal):
 1. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> arr \<longrightarrow> ptr_arr_retyps n p td x = td x proof (prove)
goal:
No subgoals!