theory Retype_C

lemma clift_ptr_retyps_gen_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"
  shows "(clift (hrs_htd_update (ptr_retyps_gen n (Ptr p :: 'a :: mem_type ptr) arr)
              (hrs_mem_update (heap_update_list p (replicate nb 0))
               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 sz supply if_cong[cong] apply (simp add: nb liftt_if[folded hrs_mem_def hrs_htd_def]
                   hrs_htd_update hrs_mem_update
                   h_t_valid_ptr_retyps_gen_same[OF guard cleared not_byte]
                   addr_card_wb) apply (rule ext, rename_tac p') apply (case_tac "p' \<in> ((+\<^sub>p) (Ptr p) \<circ> int) ` {k. k < n}") apply (clarsimp simp: h_val_def) apply (simp only: Word.Abs_fnat_hom_mult hrs_mem_update) apply (frule_tac k="size_of TYPE('a)" in mult_le_mono1[where j=n, OF Suc_leI]) apply (subst heap_list_update_list; simp?) apply (simp add: addr_card_def card_word word_bits_def) apply (clarsimp split: if_split) apply (simp add: h_val_def) apply (subst heap_list_update_disjoint_same, simp_all) apply (simp add: region_is_bytes_disjoint[OF cleared not_byte]) 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 nb 0)) 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:
n * size_of TYPE('a) < 2 ^ word_bits

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) (hrs_mem_update (heap_update_list p (replicate nb 0)) 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:
n * size_of TYPE('a) < 2 ^ word_bits

goal (1 subgoal):
 1. clift (hrs_htd_update (ptr_retyps_gen n (PTR('a) p) arr) (hrs_mem_update (heap_update_list p (replicate nb 0)) 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. n * size_of TYPE('a) < 2 ^ word_bits \<Longrightarrow> (\<lambda>pa. if pa \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t pa then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) pa) else None) = (\<lambda>y. if y \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t y then Some (h_val (hrs_mem hrs) y) else None) proof (prove)
goal (1 subgoal):
 1. \<And>p'. n * size_of TYPE('a) < 2 ^ word_bits \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<in> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None)
 2. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; x < n\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) (size_of TYPE('a)) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) = from_bytes (replicate (size_of TYPE('a)) 0)
 2. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; x < n\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) (size_of TYPE('a)) (p + word_of_nat (x * size_of TYPE('a)))) = from_bytes (replicate (size_of TYPE('a)) 0)
 2. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; x < n; Suc x * size_of TYPE('a) \<le> n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) (size_of TYPE('a)) (p + word_of_nat (x * size_of TYPE('a)))) = from_bytes (replicate (size_of TYPE('a)) 0)
 2. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; x < n; size_of TYPE('a) + x * size_of TYPE('a) \<le> n * size_of TYPE('a)\<rbrakk> \<Longrightarrow> n * size_of TYPE('a) < addr_card
 2. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> ((+\<^sub>p) (PTR('a) p) \<circ> int) ` {k. k < n}\<rbrakk> \<Longrightarrow> (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} \<or> hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p') else None) = (if p' \<in> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n} then Some (from_bytes (replicate (size_of TYPE('a)) 0)) else if hrs_htd hrs \<Turnstile>\<^sub>t p' then Some (h_val (hrs_mem hrs) p') else None) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n}; hrs_htd hrs \<Turnstile>\<^sub>t p'\<rbrakk> \<Longrightarrow> h_val (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) p' = h_val (hrs_mem hrs) p' proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n}; hrs_htd hrs \<Turnstile>\<^sub>t p'\<rbrakk> \<Longrightarrow> from_bytes (heap_list (heap_update_list p (replicate (n * size_of TYPE('a)) 0) (hrs_mem hrs)) (size_of TYPE('a)) (ptr_val p')) = from_bytes (heap_list (hrs_mem hrs) (size_of TYPE('a)) (ptr_val p')) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>n * size_of TYPE('a) < 2 ^ word_bits; p' \<notin> (\<lambda>x. PTR('a) (p + word_of_nat x * word_of_nat (size_of TYPE('a)))) ` {k. k < n}; hrs_htd hrs \<Turnstile>\<^sub>t p'\<rbrakk> \<Longrightarrow> {p..+n * size_of TYPE('a)} \<inter> ptr_span p' = {} proof (prove)
goal:
No subgoals!