theory CCorresLemmas

lemma lift_t_super_update:
  fixes p :: "'a :: mem_type ptr" and v :: "'b :: mem_type"
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  and    eu: "export_uinfo s = typ_uinfo_t TYPE('b)"
  and    lp: "lift_t g (h, d) p = Some v'"
  shows "lift_t g (heap_update (Ptr &(p\<rightarrow>f)) v h, d)
         = (lift_t g (h, d)) (p \<mapsto> field_update (field_desc s) (to_bytes_p v) v')" using fl eu lp apply - apply (rule trans [OF lift_t_super_field_update super_field_update_lookup]) apply (erule (1) h_t_valid_mono [OF _ _ guard_mono_True, rule_format]) apply (erule lift_t_h_t_valid) apply (erule (1) fl_sub_typ) apply assumption apply simp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift_t g (heap_update (PTR('b) &(p\<rightarrow>f)) v h, d) = (lift_t g (h, d))(p \<mapsto> field_update (field_desc s) (to_bytes_p v) v') proof (prove)
using this:
field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)
export_uinfo s = typ_uinfo_t TYPE('b)
lift_t g (h, d) p = Some v'

goal (1 subgoal):
 1. lift_t g (heap_update (PTR('b) &(p\<rightarrow>f)) v h, d) = (lift_t g (h, d))(p \<mapsto> field_update (field_desc s) (to_bytes_p v) v') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (heap_update (PTR('b) &(p\<rightarrow>f)) v h, d) = (lift_t g (h, d))(p \<mapsto> field_update (field_desc s) (to_bytes_p v) v') proof (prove)
goal (5 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> d,?g'5 \<Turnstile>\<^sub>t PTR('b) &(p\<rightarrow>f)
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> TYPE('b) \<le>\<^sub>\<tau> TYPE('a)
 3. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, ?n4)
 4. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) = export_uinfo s
 5. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal (5 subgoals):
 1. \<lbrakk>export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> d,?g11 \<Turnstile>\<^sub>t p
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> TYPE('b) \<le>\<^sub>\<tau> TYPE('a)
 3. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, ?n4)
 4. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) = export_uinfo s
 5. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> TYPE('b) \<le>\<^sub>\<tau> TYPE('a)
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, ?n4)
 3. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) = export_uinfo s
 4. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, ?n4)
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) = export_uinfo s
 3. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> typ_uinfo_t TYPE('b) = export_uinfo s
 2. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); export_uinfo s = typ_uinfo_t TYPE('b); lift_t g (h, d) p = Some v'\<rbrakk> \<Longrightarrow> lift_t g (h, d) p = Some v' proof (prove)
goal:
No subgoals!