theory CCorresLemmas

lemma lift_t_update_fld_other2:
  fixes val :: "'b :: packed_type" and ptr :: "'a :: packed_type ptr"
  assumes   fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, m')"
  and     disj: "typ_uinfo_t TYPE('c :: mem_type) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)"
  and       eu: "export_uinfo t = typ_uinfo_t TYPE('b)"
  and       cl: "clift (hp,d) ptr = Some z"
  shows "(clift (heap_update (Ptr &(ptr\<rightarrow>f)) val hp, d)) = (clift (hp, d) :: 'c :: mem_type typ_heap)"
  (is "?LHS = ?RHS") proof - from cl have "c_guard ptr" by (rule lift_t_g) hence "?LHS = clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d)" using eu by (simp add: packed_heap_super_field_update [OF fl]) also have "... = ?RHS" using cl disj by (rule typ_rewrs(5)) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (state)
goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (chain)
picking this:
clift (hp, d) ptr = Some z proof (prove)
using this:
clift (hp, d) ptr = Some z

goal (1 subgoal):
 1. c_guard ptr proof (state)
this:
c_guard ptr

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (prove)
using this:
c_guard ptr

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d) proof (prove)
using this:
c_guard ptr
export_uinfo t = typ_uinfo_t TYPE('b)

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d) proof (state)
this:
clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d)

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (state)
this:
clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d)

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (prove)
goal (1 subgoal):
 1. clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d) = clift (hp, d) proof (prove)
using this:
clift (hp, d) ptr = Some z
typ_uinfo_t TYPE('c) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)

goal (1 subgoal):
 1. clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d) = clift (hp, d) proof (state)
this:
clift (heap_update ptr (update_ti t (to_bytes_p val) (h_val hp ptr)) hp, d) = clift (hp, d)

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (chain)
picking this:
clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (prove)
using this:
clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d)

goal (1 subgoal):
 1. clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d) proof (state)
this:
clift (heap_update (PTR('b) &(ptr\<rightarrow>f)) val hp, d) = clift (hp, d)

goal:
No subgoals!