kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma list_map_override_comono:
  "list_map xs  \<subseteq>\<^sub>m m ++ list_map ys
    \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs" apply (simp add: map_le_def list_map_eq map_add_def) apply (cases "length xs \<le> length ys") apply (simp add: prefix_eq_nth) apply (simp split: if_split_asm add: prefix_eq_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_map xs \<subseteq>\<^sub>m m ++ list_map ys \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>{0..<length xs}. Some (xs ! a) = (case if a < length ys then Some (ys ! a) else None of None \<Rightarrow> m a | Some x \<Rightarrow> Some x) \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a\<in>{0..<length xs}. Some (xs ! a) = (case if a < length ys then Some (ys ! a) else None of None \<Rightarrow> m a | Some x \<Rightarrow> Some x); length xs \<le> length ys\<rbrakk> \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs
 2. \<lbrakk>\<forall>a\<in>{0..<length xs}. Some (xs ! a) = (case if a < length ys then Some (ys ! a) else None of None \<Rightarrow> m a | Some x \<Rightarrow> Some x); \<not> length xs \<le> length ys\<rbrakk> \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>{0..<length xs}. Some (xs ! a) = (case if a < length ys then Some (ys ! a) else None of None \<Rightarrow> m a | Some x \<Rightarrow> Some x); \<not> length xs \<le> length ys\<rbrakk> \<Longrightarrow> xs \<le> ys \<or> ys \<le> xs proof (prove)
goal:
No subgoals!
theory Retype_C

lemma list_map_plus_le_not_tag_disj:
  "list_map (typ_slice_t td y) \<subseteq>\<^sub>m m ++ list_map (typ_slice_t td' y')
    \<Longrightarrow> \<not> td \<bottom>\<^sub>t td'" apply (drule list_map_override_comono) apply (auto dest: typ_slice_sub) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_map (typ_slice_t td y) \<subseteq>\<^sub>m m ++ list_map (typ_slice_t td' y') \<Longrightarrow> \<not> td \<bottom>\<^sub>t td' proof (prove)
goal (1 subgoal):
 1. typ_slice_t td y \<le> typ_slice_t td' y' \<or> typ_slice_t td' y' \<le> typ_slice_t td y \<Longrightarrow> \<not> td \<bottom>\<^sub>t td' proof (prove)
goal:
No subgoals!
theory Retype_C

lemma td_set_offset_ind:
  "\<forall>j. td_set t (Suc j) = (apsnd Suc :: ('a typ_desc \<times> nat) \<Rightarrow> _) ` td_set t j"
  "\<forall>j. td_set_struct ts (Suc j) = (apsnd Suc :: ('a typ_desc \<times> nat) \<Rightarrow> _) ` td_set_struct ts j"
  "\<forall>j. td_set_list xs (Suc j) = (apsnd Suc :: ('a typ_desc \<times> nat) \<Rightarrow> _) ` td_set_list xs j"
  "\<forall>j. td_set_pair x (Suc j) = (apsnd Suc :: ('a typ_desc \<times> nat) \<Rightarrow> _) ` td_set_pair x j" apply (induct t and ts and xs and x) apply (simp_all add: image_Un) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>j. td_set t (Suc j) = apsnd Suc ` td_set t j &&& \<forall>j. td_set_struct ts (Suc j) = apsnd Suc ` td_set_struct ts j) &&& \<forall>j. td_set_list xs (Suc j) = apsnd Suc ` td_set_list xs j &&& \<forall>j. td_set_pair x (Suc j) = apsnd Suc ` td_set_pair x j proof (prove)
goal (6 subgoals):
 1. \<And>typ_struct list. \<forall>j. td_set_struct typ_struct (Suc j) = apsnd Suc ` td_set_struct typ_struct j \<Longrightarrow> \<forall>j. td_set (TypDesc typ_struct list) (Suc j) = apsnd Suc ` td_set (TypDesc typ_struct list) j
 2. \<And>nat1 nat2 a. \<forall>j. td_set_struct (TypScalar nat1 nat2 a) (Suc j) = apsnd Suc ` td_set_struct (TypScalar nat1 nat2 a) j
 3. \<And>list. \<forall>j. td_set_list list (Suc j) = apsnd Suc ` td_set_list list j \<Longrightarrow> \<forall>j. td_set_struct (TypAggregate list) (Suc j) = apsnd Suc ` td_set_struct (TypAggregate list) j
 4. \<forall>j. td_set_list [] (Suc j) = apsnd Suc ` td_set_list [] j
 5. \<And>dt_pair list. \<lbrakk>\<forall>j. td_set_pair dt_pair (Suc j) = apsnd Suc ` td_set_pair dt_pair j; \<forall>j. td_set_list list (Suc j) = apsnd Suc ` td_set_list list j\<rbrakk> \<Longrightarrow> \<forall>j. td_set_list (dt_pair # list) (Suc j) = apsnd Suc ` td_set_list (dt_pair # list) j
 6. \<And>typ_desc list. \<forall>j. td_set typ_desc (Suc j) = apsnd Suc ` td_set typ_desc j \<Longrightarrow> \<forall>j. td_set_pair (DTPair typ_desc list) (Suc j) = apsnd Suc ` td_set_pair (DTPair typ_desc list) j proof (prove)
goal:
No subgoals!
theory Retype_C

lemma td_set_offset:
  "(td, i) \<in> td_set td' j \<Longrightarrow> (td, i - j) \<in> td_set td' 0" by (induct j arbitrary: i, auto simp: td_set_offset_ind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (td, i) \<in> td_set td' j \<Longrightarrow> (td, i - j) \<in> td_set td' 0
theory Retype_C

lemma h_t_array_valid_retyp:
  "0 < n \<Longrightarrow> n * size_of TYPE('a) < addr_card
    \<Longrightarrow> h_t_array_valid (ptr_arr_retyps n p htd) (p :: ('a :: wf_type) ptr) n" apply (clarsimp simp: ptr_arr_retyps_def h_t_array_valid_def
                        valid_footprint_def) apply (simp add: htd_update_list_index intvlI mult.commute) apply (simp add: addr_card_wb unat_of_nat32) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n * size_of TYPE('a) < addr_card\<rbrakk> \<Longrightarrow> h_t_array_valid (ptr_arr_retyps n p htd) p n proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; n * size_of TYPE('a) < addr_card; y < size_of TYPE('a) * n\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) y) \<subseteq>\<^sub>m snd (htd_update_list (ptr_val p) (map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i)) [0..<n * size_of TYPE('a)]) htd (ptr_val p + word_of_nat y)) \<and> fst (htd_update_list (ptr_val p) (map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i)) [0..<n * size_of TYPE('a)]) htd (ptr_val p + word_of_nat y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>0 < n; n * size_of TYPE('a) < addr_card; y < n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) y) \<subseteq>\<^sub>m snd (htd (ptr_val p + word_of_nat y)) ++ (map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i)) [0..<n * size_of TYPE('a)] ! unat (word_of_nat y)) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma clift_ptr_retyps_gen_prev_memset_same:
  assumes guard: "\<forall>n' < n. c_guard (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) (of_nat n'))"
  assumes cleared: "region_is_bytes' p (n * size_of TYPE('a :: mem_type)) (hrs_htd hrs)"
    and not_byte: "typ_uinfo_t TYPE('a :: mem_type) \<noteq> typ_uinfo_t TYPE(word8)"
  and nb: "nb = n * size_of TYPE ('a)"
  and sz: "n * size_of TYPE('a) < 2 ^ word_bits"
  and rep0:  "heap_list (hrs_mem hrs) nb p = replicate nb 0"
  shows "(clift (hrs_htd_update (ptr_retyps_gen n (Ptr p :: 'a :: mem_type ptr) arr) hrs) :: 'a :: mem_type typ_heap)
         = (\<lambda>y. if y \<in> (CTypesDefs.ptr_add (Ptr p :: 'a :: mem_type ptr) o of_nat) ` {k. k < n}
                then Some (from_bytes (replicate (size_of TYPE('a  :: mem_type)) 0)) else clift hrs y)" using rep0 apply (subst clift_ptr_retyps_gen_memset_same[symmetric, OF guard cleared not_byte nb sz]) apply (rule arg_cong[where f=clift]) apply (rule_tac f="hrs_htd_update f" for f in arg_cong) apply (cases hrs, simp add: hrs_mem_update_def) apply (simp add: heap_update_list_id hrs_mem_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hrs) = (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else clift hrs y) proof (prove)
using this:
heap_list (hrs_mem hrs) nb p = replicate nb 0

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hrs) = (\<lambda>y. if y \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else clift hrs y) proof (prove)
goal (1 subgoal):
 1. heap_list (hrs_mem hrs) nb p = replicate nb 0 \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hrs) = clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) ?arr1) (hrs_mem_update (heap_update_list p (replicate nb 0)) hrs)) proof (prove)
goal (1 subgoal):
 1. heap_list (hrs_mem hrs) nb p = replicate nb 0 \<Longrightarrow> hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hrs = hrs_htd_update (ptr_retyps_gen n (PTR('a) p) ?arr1) (hrs_mem_update (heap_update_list p (replicate nb 0)) hrs) proof (prove)
goal (1 subgoal):
 1. heap_list (hrs_mem hrs) nb p = replicate nb 0 \<Longrightarrow> hrs = hrs_mem_update (heap_update_list p (replicate nb 0)) hrs proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>heap_list (hrs_mem (a, b)) nb p = replicate nb 0; hrs = (a, b)\<rbrakk> \<Longrightarrow> a = heap_update_list p (replicate nb 0) a proof (prove)
goal:
No subgoals!
theory Retype_C

lemma clift_ptr_retyps_gen_other:
  assumes cleared: "region_is_bytes' (ptr_val p) (nptrs * size_of TYPE('a :: mem_type)) (hrs_htd hrs)"
  and sz: "nptrs * size_of TYPE('a) < 2 ^ word_bits"
  and other: "typ_uinfo_t TYPE('b)  \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
  and not_byte: "typ_uinfo_t TYPE('b :: mem_type) \<noteq> typ_uinfo_t TYPE(word8)"
  shows "(clift (hrs_htd_update (ptr_retyps_gen nptrs (p :: 'a ptr) arr) hrs) :: 'b :: mem_type typ_heap)
         = clift hrs" using sz cleared apply (cases p) apply (simp add: liftt_if[folded hrs_mem_def hrs_htd_def]
                   h_t_valid_def hrs_htd_update
                   ptr_retyps_gen_valid_footprint[simplified addr_card_wb, OF _ other not_byte sz]
              cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen nptrs p arr) hrs) = clift hrs proof (prove)
using this:
nptrs * size_of TYPE('a) < 2 ^ word_bits
region_is_bytes' (ptr_val p) (nptrs * size_of TYPE('a)) (hrs_htd hrs)

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen nptrs p arr) hrs) = clift hrs proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>nptrs * size_of TYPE('a) < 2 ^ word_bits; region_is_bytes' (ptr_val p) (nptrs * size_of TYPE('a)) (hrs_htd hrs); p = PTR('a) x\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (ptr_retyps_gen nptrs p arr) hrs) = clift hrs proof (prove)
goal:
No subgoals!
theory Retype_C

lemma add_is_injective_ring:
  "inj ((+) (x :: 'a :: ring))" by (rule inj_onI, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj ((+) x)
theory Retype_C

lemma ptr_retyp_to_array:
  "ptr_retyps_gen 1 (p :: (('a :: wf_type)['b :: finite]) ptr) False
    = ptr_retyps_gen CARD('b) (ptr_coerce p :: 'a ptr) True" by (intro ext, simp add: ptr_retyps_gen_def ptr_arr_retyps_to_retyp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_retyps_gen 1 p False = ptr_retyps_gen CARD('b) (PTR_COERCE('a['b] \<rightarrow> 'a) p) True
theory Retype_C

lemma ptr_add_to_new_cap_addrs:
  assumes size_of_m: "size_of TYPE('a :: mem_type) = 2 ^ objBitsKO ko"
  shows "(CTypesDefs.ptr_add (Ptr ptr :: 'a :: mem_type ptr) \<circ> of_nat) ` {k. k < n}
   = Ptr ` set (new_cap_addrs n ptr ko)" unfolding new_cap_addrs_def apply (simp add: image_image shiftl_t2n size_of_m field_simps) apply (clarsimp simp: atLeastLessThan_def lessThan_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((+\<^sub>p) (PTR('a) ptr) \<circ> int) ` {k. k < n} = PTR('a) ` set (new_cap_addrs n ptr ko) proof (prove)
goal (1 subgoal):
 1. ((+\<^sub>p) (PTR('a) ptr) \<circ> int) ` {k. k < n} = PTR('a) ` set (map (\<lambda>p. ptr + (word_of_nat p << objBitsKO ko)) [0..<n]) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. PTR('a) (ptr + word_of_nat x * 2 ^ objBitsKO ko)) ` {k. k < n} = (\<lambda>x. PTR('a) (ptr + word_of_nat x * 2 ^ objBitsKO ko)) ` {0..<n} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma update_ti_t_word32_0s:
  "update_ti_t (typ_info_t TYPE(word32)) [0,0,0,0] X = 0"
  "word_rcat [0, 0, 0, (0 :: word8)] = (0 :: word32)" by (simp_all add: typ_info_word word_rcat_def bin_rcat_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_ti_t (typ_info_t TYPE(32 word)) [0, 0, 0, 0] X = 0 &&& word_rcat [0, 0, 0, 0] = 0
theory Retype_C

lemma ptr_retyps_htd_safe:
  "\<lbrakk> htd_safe D htd;
    {ptr_val ptr ..+ n * size_of TYPE('a :: mem_type)}
        \<subseteq> D \<rbrakk>
   \<Longrightarrow> htd_safe D (ptr_retyps_gen n (ptr :: 'a ptr) arr htd)" apply (clarsimp simp: htd_safe_def) apply (case_tac "a \<in> {ptr_val ptr..+n * size_of TYPE('a)}") apply blast apply (case_tac "(a, b) \<in> dom_s htd") apply blast apply (clarsimp simp: dom_s_def ptr_retyps_gen_out) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>htd_safe D htd; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D\<rbrakk> \<Longrightarrow> htd_safe D (ptr_retyps_gen n ptr arr htd) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd)\<rbrakk> \<Longrightarrow> a \<in> D proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<in> {ptr_val ptr..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> a \<in> D
 2. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<notin> {ptr_val ptr..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> a \<in> D proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<notin> {ptr_val ptr..+n * size_of TYPE('a)}\<rbrakk> \<Longrightarrow> a \<in> D proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<notin> {ptr_val ptr..+n * size_of TYPE('a)}; (a, b) \<in> dom_s htd\<rbrakk> \<Longrightarrow> a \<in> D
 2. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<notin> {ptr_val ptr..+n * size_of TYPE('a)}; (a, b) \<notin> dom_s htd\<rbrakk> \<Longrightarrow> a \<in> D proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<subseteq> D; (a, b) \<in> dom_s (ptr_retyps_gen n ptr arr htd); a \<notin> {ptr_val ptr..+n * size_of TYPE('a)}; (a, b) \<notin> dom_s htd\<rbrakk> \<Longrightarrow> a \<in> D proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ptr_retyps_htd_safe_neg:
  "\<lbrakk> htd_safe D htd; {ptr_val ptr ..+ n * size_of TYPE('a :: mem_type)} \<inter> D' = {}; -D \<subseteq> D' \<rbrakk>
   \<Longrightarrow> htd_safe D (ptr_retyps_gen n (ptr :: 'a ptr) arr htd)" using ptr_retyps_htd_safe by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>htd_safe D htd; {ptr_val ptr..+n * size_of TYPE('a)} \<inter> D' = {}; - D \<subseteq> D'\<rbrakk> \<Longrightarrow> htd_safe D (ptr_retyps_gen n ptr arr htd) proof (prove)
using this:
\<lbrakk>htd_safe ?D ?htd; {ptr_val ?ptr..+?n * size_of TYPE(?'a)} \<subseteq> ?D\<rbrakk> \<Longrightarrow> htd_safe ?D (ptr_retyps_gen ?n ?ptr ?arr ?htd)

goal (1 subgoal):
 1. \<lbrakk>htd_safe D htd; {ptr_val ptr..+n * size_of TYPE('a)} \<inter> D' = {}; - D \<subseteq> D'\<rbrakk> \<Longrightarrow> htd_safe D (ptr_retyps_gen n ptr arr htd)
theory Retype_C

lemma region_is_bytes_subset:
  "region_is_bytes' ptr sz htd
    \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
    \<Longrightarrow> region_is_bytes' ptr' sz' htd" by (auto simp: region_is_bytes'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_is_bytes' ptr sz htd; {ptr'..+sz'} \<subseteq> {ptr..+sz}\<rbrakk> \<Longrightarrow> region_is_bytes' ptr' sz' htd
theory Retype_C

lemma (in range_cover) strong_times_32:
  "len_of TYPE('a) = len_of TYPE(32) \<Longrightarrow> n * 2 ^ sbit < 2 ^ word_bits" apply (simp add: nat_mult_power_less_eq) apply (rule order_less_le_trans, rule string) apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) = LENGTH(32) \<Longrightarrow> n * 2 ^ sbit < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. LENGTH('a) = 32 \<Longrightarrow> n < 2 ^ (word_bits - sbit) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) = 32 \<Longrightarrow> 2 ^ (LENGTH('a) - sbit) \<le> 2 ^ (word_bits - sbit) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma cslift_ptr_retyp_other_inst:
  assumes   bytes: "region_is_bytes' p (n * (2 ^ bits)) (hrs_htd hp)"
  and       cover: "range_cover p sz bits n"
  and          sz: "region_sz = n * size_of TYPE('a :: mem_type)"
  and         sz2: "size_of TYPE('a :: mem_type) = 2 ^ bits"
  and       tdisj: "typ_uinfo_t TYPE('b) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
  and    not_byte: "typ_uinfo_t TYPE('b :: mem_type) \<noteq> typ_uinfo_t TYPE(word8)"
  shows "(clift (hrs_htd_update (ptr_retyps_gen n (Ptr p :: 'a :: mem_type ptr) arr)
               hp) :: 'b :: mem_type typ_heap)
         = clift hp" using bytes apply (subst clift_ptr_retyps_gen_other[OF _ _ tdisj not_byte], simp_all) apply (simp add: sz2) apply (simp add: sz2 range_cover.strong_times_32[OF cover]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hp) = clift hp proof (prove)
using this:
region_is_bytes' p (n * 2 ^ bits) (hrs_htd hp)

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) hp) = clift hp proof (prove)
goal (2 subgoals):
 1. region_is_bytes' p (n * 2 ^ bits) (hrs_htd hp) \<Longrightarrow> region_is_bytes' p (n * size_of TYPE('a)) (hrs_htd hp)
 2. region_is_bytes' p (n * 2 ^ bits) (hrs_htd hp) \<Longrightarrow> n * size_of TYPE('a) < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. region_is_bytes' p (n * 2 ^ bits) (hrs_htd hp) \<Longrightarrow> n * size_of TYPE('a) < 2 ^ word_bits proof (prove)
goal:
No subgoals!
theory Retype_C

lemma cslift_ptr_retyp_memset_other_inst:
  assumes   bytes: "region_is_bytes p (n * (2 ^ bits)) x"
  and       cover: "range_cover p sz bits n"
  and          sz: "region_sz = n * size_of TYPE('a :: mem_type)"
  and         sz2: "size_of TYPE('a :: mem_type) = 2 ^ bits"
  and       tdisj: "typ_uinfo_t TYPE('b) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
  and    not_byte: "typ_uinfo_t TYPE('b :: mem_type) \<noteq> typ_uinfo_t TYPE(word8)"
  shows "(clift (hrs_htd_update (ptr_retyps_gen n (Ptr p :: 'a :: mem_type ptr) arr)
              (hrs_mem_update (heap_update_list p (replicate (region_sz) 0))
               (t_hrs_' (globals x)))) :: 'b :: mem_type typ_heap)
         = cslift x" using bytes apply (subst cslift_ptr_retyp_other_inst[OF _ cover sz sz2 tdisj not_byte]) apply simp apply (rule clift_heap_list_update_no_heap_other[OF _ not_byte]) apply (simp add: hrs_htd_def sz sz2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) (hrs_mem_update (heap_update_list p (replicate region_sz 0)) (t_hrs_' (globals x)))) = cslift x proof (prove)
using this:
region_is_bytes p (n * 2 ^ bits) x

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) (hrs_mem_update (heap_update_list p (replicate region_sz 0)) (t_hrs_' (globals x)))) = cslift x proof (prove)
goal (2 subgoals):
 1. region_is_bytes p (n * 2 ^ bits) x \<Longrightarrow> region_is_bytes' p (n * 2 ^ bits) (hrs_htd (hrs_mem_update (heap_update_list p (replicate region_sz 0)) (t_hrs_' (globals x))))
 2. region_is_bytes p (n * 2 ^ bits) x \<Longrightarrow> clift (hrs_mem_update (heap_update_list p (replicate region_sz 0)) (t_hrs_' (globals x))) = cslift x proof (prove)
goal (1 subgoal):
 1. region_is_bytes p (n * 2 ^ bits) x \<Longrightarrow> clift (hrs_mem_update (heap_update_list p (replicate region_sz 0)) (t_hrs_' (globals x))) = cslift x proof (prove)
goal (1 subgoal):
 1. region_is_bytes p (n * 2 ^ bits) x \<Longrightarrow> region_is_bytes p (length (replicate region_sz 0)) x proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ptr_retyps_one:
  "ptr_retyps (Suc 0) = ptr_retyp" apply (rule ext)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_retyps (Suc 0) = ptr_retyp proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. ptr_retyps (Suc 0) x xa xb = ptr_retyp x xa xb proof (prove)
goal:
No subgoals!
theory Retype_C

lemma in_set_list_map:
  "x \<in> set xs \<Longrightarrow> \<exists>n. [n \<mapsto> x] \<subseteq>\<^sub>m list_map xs" apply (clarsimp simp: in_set_conv_nth) apply (rule_tac x=i in exI) apply (simp add: map_le_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> \<exists>n. [n \<mapsto> x] \<subseteq>\<^sub>m list_map xs proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length xs; x = xs ! i\<rbrakk> \<Longrightarrow> \<exists>n. [n \<mapsto> xs ! i] \<subseteq>\<^sub>m list_map xs proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length xs; x = xs ! i\<rbrakk> \<Longrightarrow> [i \<mapsto> xs ! i] \<subseteq>\<^sub>m list_map xs proof (prove)
goal:
No subgoals!
theory Retype_C

lemma h_t_valid_eq_array_valid:
  "h_t_valid htd gd (p :: (('a :: wf_type)['b :: finite]) ptr)
    = (gd p \<and> h_t_array_valid htd (ptr_coerce p :: 'a ptr) CARD('b))" by (auto simp: h_t_array_valid_def h_t_valid_def
                 typ_uinfo_array_tag_n_m_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. htd,gd \<Turnstile>\<^sub>t p = (gd p \<and> h_t_array_valid htd (PTR_COERCE('a['b] \<rightarrow> 'a) p) CARD('b))
theory Retype_C

lemma cvariable_array_ptr_retyps:
  assumes sz2: "size_of TYPE('a :: mem_type) = sz"
  assumes bytes: "region_is_bytes' (ptr_val p) (n * sz) htd"
  shows "cvariable_array_map_relation m ns ptrfun htd
    \<Longrightarrow> cvariable_array_map_relation m ns (ptrfun :: _ \<Rightarrow> ('b :: mem_type) ptr)
            (ptr_retyps_gen n (p :: 'a :: mem_type ptr) arr htd)" by (clarsimp simp: cvariable_array_map_relation_def
                     h_t_array_valid_ptr_retyps_gen[OF sz2 bytes])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cvariable_array_map_relation m ns ptrfun htd \<Longrightarrow> cvariable_array_map_relation m ns ptrfun (ptr_retyps_gen n p arr htd)
theory Retype_C

lemma cvariable_array_ptr_upd:
  assumes at: "h_t_array_valid htd (ptrfun x) (ns y)"
  shows "cvariable_array_map_relation m ns ptrfun htd
    \<Longrightarrow> cvariable_array_map_relation (m(x \<mapsto> y))
        ns (ptrfun :: _ \<Rightarrow> ('b :: mem_type) ptr) htd" by (clarsimp simp: cvariable_array_map_relation_def at
              split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cvariable_array_map_relation m ns ptrfun htd \<Longrightarrow> cvariable_array_map_relation (m(x \<mapsto> y)) ns ptrfun htd
theory Retype_C

lemma clift_eq_h_t_valid_eq:
  "clift hp = (clift hp' :: ('a :: c_type) ptr \<Rightarrow> _)
    \<Longrightarrow> (h_t_valid (hrs_htd hp) c_guard :: 'a ptr \<Rightarrow> _)
        = h_t_valid (hrs_htd hp') c_guard" by (rule ext, simp add: h_t_valid_clift_Some_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift hp = clift hp' \<Longrightarrow> h_t_valid (hrs_htd hp) c_guard = h_t_valid (hrs_htd hp') c_guard