theory FieldAccessors

lemma heap_update_field2:
  "\<lbrakk> field_ti TYPE('a :: packed_type) f = Some t;
     align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0;
     export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))\<rbrakk>
   \<Longrightarrow> heap_update (Ptr &(p\<rightarrow>f)) (v :: 'b) hp =
       heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp" apply (rule trans,
         rule_tac q="Ptr &(Ptr (of_nat (align_of TYPE('a))) \<rightarrow> f)"
            in heap_update_rotate) apply (rule trans[rotated], rule sym,
         rule_tac q="Ptr (of_nat (align_of TYPE('a)))" in heap_update_rotate) apply (erule field_ti_field_lookupE) apply (subst packed_heap_super_field_update, assumption,
         simp_all add: typ_uinfo_t_def) apply (simp add: c_guard_align_of) apply (simp add: h_val_def heap_list_rotate) apply (simp add: field_lvalue_def field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_ti TYPE('a) f = Some t; align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0; export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> heap_update (PTR('b) &(p\<rightarrow>f)) v hp = heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_ti TYPE('a) f = Some t; align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0; export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) v (\<lambda>x. hp (x + (ptr_val (PTR('b) &(p\<rightarrow>f)) - ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f))))) (x + (ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) - ptr_val (PTR('b) &(p\<rightarrow>f))))) = heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_ti TYPE('a) f = Some t; align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0; export_uinfo t = export_uinfo (typ_info_t TYPE('b))\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) v (\<lambda>x. hp (x + (ptr_val (PTR('b) &(p\<rightarrow>f)) - ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f))))) (x + (ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) - ptr_val (PTR('b) &(p\<rightarrow>f))))) = (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val hp p)) (\<lambda>x. hp (x + (ptr_val p - ptr_val (PTR('a) (word_of_nat (align_of TYPE('a))))))) (x + (ptr_val (PTR('a) (word_of_nat (align_of TYPE('a)))) - ptr_val p))) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; align_of TYPE('a) \<noteq> 0; export_uinfo t = export_uinfo (typ_info_t TYPE('b)); field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) v (\<lambda>x. hp (x + (ptr_val (PTR('b) &(p\<rightarrow>f)) - ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f))))) (x + (ptr_val (PTR('b) &(PTR(?'d4) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)) - ptr_val (PTR('b) &(p\<rightarrow>f))))) = (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val hp p)) (\<lambda>x. hp (x + (ptr_val p - ptr_val (PTR('a) (word_of_nat (align_of TYPE('a))))))) (x + (ptr_val (PTR('a) (word_of_nat (align_of TYPE('a)))) - ptr_val p))) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; 0 < align_of TYPE('a); export_uinfo t = export_uinfo (typ_info_t TYPE('b)); field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)\<rbrakk> \<Longrightarrow> c_guard (PTR('a) (word_of_nat (align_of TYPE('a))))
 2. \<And>n. \<lbrakk>align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; 0 < align_of TYPE('a); export_uinfo t = export_uinfo (typ_info_t TYPE('b)); field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val (\<lambda>x. hp (x + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))) (PTR('a) (word_of_nat (align_of TYPE('a)))))) (\<lambda>x. hp (x + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))) (x + (&(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f) - &(p\<rightarrow>f)))) = (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val hp p)) (\<lambda>x. hp (x + (ptr_val p - word_of_nat (align_of TYPE('a))))) (x + (word_of_nat (align_of TYPE('a)) - ptr_val p))) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; 0 < align_of TYPE('a); export_uinfo t = export_uinfo (typ_info_t TYPE('b)); field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val (\<lambda>x. hp (x + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))) (PTR('a) (word_of_nat (align_of TYPE('a)))))) (\<lambda>x. hp (x + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))) (x + (&(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f) - &(p\<rightarrow>f)))) = (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (h_val hp p)) (\<lambda>x. hp (x + (ptr_val p - word_of_nat (align_of TYPE('a))))) (x + (word_of_nat (align_of TYPE('a)) - ptr_val p))) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>align_of TYPE('a) + size_of TYPE('a) < 2 ^ word_bits; 0 < align_of TYPE('a); export_uinfo t = export_uinfo (typ_info_t TYPE('b)); field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)\<rbrakk> \<Longrightarrow> (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (from_bytes (heap_list hp (size_of TYPE('a)) (word_of_nat (align_of TYPE('a)) + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))))) (\<lambda>x. hp (x + (&(p\<rightarrow>f) - &(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f)))) (x + (&(PTR('a) (word_of_nat (align_of TYPE('a)))\<rightarrow>f) - &(p\<rightarrow>f)))) = (\<lambda>x. heap_update (PTR('a) (word_of_nat (align_of TYPE('a)))) (update_ti t (to_bytes_p v) (from_bytes (heap_list hp (size_of TYPE('a)) (ptr_val p)))) (\<lambda>x. hp (x + (ptr_val p - word_of_nat (align_of TYPE('a))))) (x + (word_of_nat (align_of TYPE('a)) - ptr_val p))) proof (prove)
goal:
No subgoals!