theory FieldAccessors

lemma field_lookup_to_bytes_split:
  "\<lbrakk> field_lookup (typ_info_t TYPE('a :: mem_type)) f 0
        \<equiv> Some (adjust_ti (typ_info_t TYPE('b :: mem_type)) accsr
           (updtr \<circ> (\<lambda>x _. x)), n);
        m = n + size_of TYPE('b) \<rbrakk>
    \<Longrightarrow> drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))
        = to_bytes (accsr v) (heap_list hp (size_of TYPE ('b)) (addr + of_nat n))
            @ drop m (to_bytes v (heap_list hp (size_of TYPE('a)) addr))" apply clarsimp apply (rule trans, rule_tac n="size_of TYPE('b)" in append_take_drop_id[symmetric]) apply (rule arg_cong2[where f=append]) apply (rule trans, rule field_lookup_to_bytes, simp+) apply (drule field_lookup_offset_size[OF meta_eq_to_obj_eq]) apply (simp add: drop_heap_list_le take_heap_list_le size_of_def) apply (simp add: add.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n)) @ drop m (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n)) @ drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) @ drop (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n)) @ drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> take (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n))
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> to_bytes (accsr v) (take (size_of TYPE('b)) (drop n (heap_list hp (size_of TYPE('a)) addr))) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n))
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m = n + size_of TYPE('b); size_td (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x))) + n \<le> size_td (typ_info_t TYPE('a))\<rbrakk> \<Longrightarrow> to_bytes (accsr v) (take (size_of TYPE('b)) (drop n (heap_list hp (size_of TYPE('a)) addr))) = to_bytes (accsr v) (heap_list hp (size_of TYPE('b)) (addr + word_of_nat n))
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 \<equiv> Some (adjust_ti (typ_info_t TYPE('b)) accsr (updtr \<circ> (\<lambda>x _. x)), n); m = n + size_of TYPE('b)\<rbrakk> \<Longrightarrow> drop (size_of TYPE('b)) (drop n (to_bytes v (heap_list hp (size_of TYPE('a)) addr))) = drop (n + size_of TYPE('b)) (to_bytes v (heap_list hp (size_of TYPE('a)) addr)) proof (prove)
goal:
No subgoals!