Theory TypHeap

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)


theory TypHeap
imports
  Vanilla32
  ArchArraysMemInstance
  HeapRawState
  MapExtraTrans
begin

declare map_add_assoc [simp del]

definition wf_heap_val :: "heap_state ⇒ bool" where
  "wf_heap_val s ≡
     ∀x t n v. s (x,SIndexVal) ≠ Some (STyp t) ∧ s (x,SIndexTyp n) ≠ Some (SValue v)"

type_synonym typ_slice_list = "(typ_uinfo × typ_base) list"

primrec
  typ_slice_t :: "typ_uinfo ⇒ nat ⇒ typ_slice_list" and
  typ_slice_struct :: "typ_uinfo_struct ⇒ nat ⇒ typ_slice_list" and
  typ_slice_list :: "(typ_uinfo,field_name, unit) dt_tuple list ⇒ nat ⇒ typ_slice_list" and
  typ_slice_tuple :: "(typ_uinfo,field_name, unit) dt_tuple ⇒ nat ⇒ typ_slice_list"
where
  tl0: "typ_slice_t (TypDesc algn st nm) m = typ_slice_struct st m @
        [(if m = 0 then ((TypDesc algn st nm),True) else
        ((TypDesc algn st nm),False))]"

| tl1: "typ_slice_struct (TypScalar n algn d) m = []"
| tl2: "typ_slice_struct (TypAggregate xs) m = typ_slice_list xs m"

| tl3: "typ_slice_list [] m = []"
| tl4: "typ_slice_list (x#xs) m = (if m < size_td (dt_fst x) ∨ xs = [] then
        typ_slice_tuple x m else typ_slice_list xs (m - size_td (dt_fst x)))"

| tl5: "typ_slice_tuple (DTuple t n d) m = typ_slice_t t m"

definition list_map :: "'a list ⇒ (nat ⇀ 'a)" where
  "list_map xs ≡ map_of (zip [0..<length xs] xs)"

definition s_footprint_untyped :: "addr ⇒ typ_uinfo ⇒ (addr × s_heap_index) set" where
  "s_footprint_untyped p t ≡
     {(p + of_nat x,k) | x k. x < size_td t ∧
                              (k=SIndexVal ∨ (∃n. k=SIndexTyp n ∧ n < length (typ_slice_t t x)))}"

definition (in c_type) s_footprint :: "'a ptr ⇒ (addr × s_heap_index) set" where
  "s_footprint p ≡ s_footprint_untyped (ptr_val p) (typ_uinfo_t TYPE('a))"

definition empty_htd :: "heap_typ_desc" where
  "empty_htd ≡ λx. (False,Map.empty)"

definition dom_s :: "heap_typ_desc ⇒ s_addr set" where
  "dom_s d ≡ {(x,SIndexVal) | x. fst (d x)} ∪
      {(x,SIndexTyp n) | x n. snd (d x) n ≠ None}"

definition restrict_s :: "heap_typ_desc ⇒ s_addr set ⇒ heap_typ_desc" where
  "restrict_s d X ≡
     λx. ((x,SIndexVal) ∈ X ∧ fst (d x), (λy. if (x,SIndexTyp y) ∈ X then snd (d x) y else None))"

definition valid_footprint :: "heap_typ_desc ⇒ addr ⇒ typ_uinfo ⇒ bool" where
  "valid_footprint d x t  ≡
     let n = size_td t in
       0 < n ∧ (∀y. y < n ⟶          
                    list_map (typ_slice_t t y) ⊆⇩m snd (d (x + of_nat y)) ∧ fst (d (x + of_nat y)))"



definition (in c_type) h_t_valid ::
  "heap_typ_desc ⇒ 'a ptr_guard ⇒ 'a ptr ⇒ bool" ("_,_ ⊨⇩t _" [99,0,99] 100) where
  "d,g ⊨⇩t p ≡ valid_footprint d (ptr_val (p::'a ptr)) (typ_uinfo_t TYPE('a)) ∧ g p"


type_synonym 'a typ_heap = "'a ptr ⇀ 'a"

definition proj_h :: "heap_state ⇒ heap_mem" where
  "proj_h s ≡ λx. case_option undefined (case_s_heap_value id undefined) (s (x,SIndexVal))"

definition lift_state :: "heap_raw_state ⇒ heap_state" where
  "lift_state ≡ λ(h,d) (x,y).
     case y of
       SIndexVal ⇒ if fst (d x)then Some (SValue (h x)) else None
     | SIndexTyp n ⇒ case_option None (Some ∘ STyp) (snd (d x) n)"


definition fun2list :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a list" where
  "fun2list f n ≡ if n=0 then [] else map f [0..<n]"

definition null_d :: "heap_state ⇒ addr ⇒ nat ⇒ bool" where
  "null_d s x y ≡ s (x,SIndexTyp y) = None"

definition max_d :: "heap_state ⇒ addr ⇒ nat" where
  "max_d s x ≡ 1 + (GREATEST y. ¬ null_d s x y)"

definition proj_d :: "heap_state ⇒ heap_typ_desc" where
  "proj_d s ≡ λx. (s (x,SIndexVal) ≠ None,
      λn. case_option None (Some ∘ s_heap_tag) (s (x,SIndexTyp n)))"

definition (in c_type) s_valid ::
  "heap_state ⇒ 'a ptr_guard ⇒ 'a ptr ⇒ bool" ("_,_ ⊨⇩s _" [100,0,100] 100) where
  "s,g ⊨⇩s p ≡ proj_d s,g ⊨⇩t p"

definition heap_list_s :: "heap_state ⇒ nat ⇒ addr ⇒  byte list" where
  "heap_list_s s n p ≡ heap_list (proj_h s) n p"

definition (in c_type) lift_typ_heap :: "'a ptr_guard ⇒ heap_state ⇒ 'a typ_heap" where
  "lift_typ_heap g s ≡
     (Some ∘ from_bytes ∘ heap_list_s s (size_of TYPE('a)) ∘ ptr_val) |` {p. s,g ⊨⇩s p}"

definition (in c_type) heap_update_s :: "'a ptr ⇒ 'a ⇒ heap_state ⇒ heap_state" where
  "heap_update_s n p s ≡ lift_state (heap_update n p (proj_h s), proj_d s)"

definition (in c_type) lift_t :: "'a ptr_guard ⇒ heap_raw_state ⇒ 'a typ_heap" where
  "lift_t g ≡ lift_typ_heap g ∘ lift_state"

definition tag_disj :: "('a, 'b) typ_desc ⇒ ('a,'b) typ_desc ⇒ bool" ("_ ⊥⇩t _" [90,90] 90) where
  "f ⊥⇩t g ≡ ¬ (f ≤ g ∨ g ≤ f)"

definition ladder_set :: "typ_uinfo ⇒ nat ⇒ nat ⇒ (typ_uinfo × nat) set" where
  "ladder_set s n p ≡ {(t,n+p) | t. ∃k. (t,k) ∈ set (typ_slice_t s n)}"


(* case where 'b is a field type of 'a *)

primrec
  field_names :: "('a,'b) typ_info ⇒ typ_uinfo ⇒
      (qualified_field_name) list" and
  field_names_struct :: "('a field_desc,'b) typ_struct ⇒ typ_uinfo ⇒
      (qualified_field_name) list" and
  field_names_list :: "(('a,'b) typ_info,field_name, 'b) dt_tuple list ⇒ typ_uinfo ⇒
      (qualified_field_name) list" and
  field_names_tuple :: "(('a,'b) typ_info,field_name, 'b) dt_tuple ⇒ typ_uinfo ⇒
      (qualified_field_name) list"
where
  tfs0: "field_names (TypDesc algn st nm) t = (if t=export_uinfo (TypDesc algn st nm) then
         [[]] else field_names_struct st t)"

| tfs1: "field_names_struct (TypScalar m algn d) t = []"
| tfs2: "field_names_struct (TypAggregate xs) t = field_names_list xs t"

| tfs3: "field_names_list [] t = []"
| tfs4: "field_names_list (x#xs) t = field_names_tuple x t@field_names_list xs t"

| tfs5: "field_names_tuple (DTuple s f d) t = map (λfs. f#fs) (field_names s t)"

definition field_typ_untyped :: "('a,'b) typ_desc ⇒ qualified_field_name ⇒ ('a,'b) typ_desc" where
  "field_typ_untyped t n ≡ (fst (the (field_lookup t n 0)))"

definition (in c_type) field_typ :: "'a itself ⇒ qualified_field_name ⇒ 'a xtyp_info" where
  "field_typ t n ≡ field_typ_untyped (typ_info_t TYPE('a)) n"

definition (in c_type) fs_consistent ::
  "qualified_field_name list ⇒ 'a itself ⇒ 'b::c_type itself ⇒ bool" where
  "fs_consistent fs a b ≡ set fs ⊆ set (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b)))"

definition (in c_type) field_offset_footprint :: "'a ptr ⇒ (qualified_field_name) list ⇒ 'b ptr set"
  where
  "field_offset_footprint p fs ≡ {Ptr &(p→k) | k. k ∈ set fs}"


definition sub_typ :: "'a::c_type itself ⇒ 'b::c_type itself ⇒ bool" ("_ ≤⇩τ _" [51, 51] 50) where
  "s ≤⇩τ t ≡ typ_uinfo_t s ≤ typ_uinfo_t t"

definition sub_typ_proper :: "'a::c_type itself ⇒ 'b::c_type itself ⇒ bool" ("_ <⇩τ _" [51, 51] 50)
  where
  "s <⇩τ t ≡ typ_uinfo_t s < typ_uinfo_t t"

definition peer_typ :: "'a::c_type itself ⇒ 'b :: c_type itself ⇒ bool"
  where
  "peer_typ a b ≡ typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b) ∨
                   typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b)"

definition (in c_type) guard_mono :: "'a ptr_guard ⇒ 'b::c_type ptr_guard ⇒ bool" where
  "guard_mono g g' ≡
     ∀n f p. g p ∧
        field_lookup  (typ_uinfo_t TYPE('a)) f 0 = Some (typ_uinfo_t TYPE('b),n)  ⟶
        g' (Ptr (ptr_val p + of_nat n))"

primrec (in c_type) sub_field_update_t ::
  "qualified_field_name list ⇒ 'a ptr ⇒ 'a ⇒ 'b::c_type typ_heap ⇒ 'b typ_heap"
where
  sft0: "sub_field_update_t [] p v s = s"
| sft1: "sub_field_update_t (f#fs) p (v::'a) s =
           (let s' = sub_field_update_t fs p v s in
              s'(Ptr &(p→f) ↦ from_bytes (access_ti⇩0 (field_typ TYPE('a) f) v))) |`
                dom (s::'b::c_type typ_heap)"

(* case where 'b contains a field of type of 'a *)

primrec (in c_type) update_value_t :: "(qualified_field_name) list ⇒ 'a ⇒ 'b ⇒ nat ⇒ 'b::c_type"
where
  uvt0:  "update_value_t [] v w x = w"
| uvt1:  "update_value_t (f#fs) v (w::'b) x = (if x=field_offset TYPE('b) f then
      field_update (field_desc (field_typ TYPE('b) f)) (to_bytes_p (v::'a)) (w::'b::c_type) else update_value_t fs v w x)"

definition (in c_type) super_field_update_t :: "'a ptr ⇒ 'a ⇒ 'b::c_type typ_heap ⇒ 'b typ_heap" where
  "super_field_update_t p v s ≡ λq.
     if field_of_t p q
     then
       case_option None
                   (λw. Some (update_value_t (field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a)))
                                             v w (unat (ptr_val p - ptr_val q))))
                   (s q)
     else s q"

definition heap_footprint :: "heap_typ_desc ⇒ typ_uinfo ⇒ addr set" where
  "heap_footprint d t ≡ {x. ∃y. valid_footprint d y t ∧ x ∈ {y} ∪ {y..+size_td t}}"

definition (in c_type) ptr_safe :: "'a ptr ⇒ heap_typ_desc ⇒ bool" where
  "ptr_safe p d ≡ s_footprint p ⊆ dom_s d"

(* Retyping *)

primrec
  htd_update_list :: "addr ⇒ typ_slice list ⇒ heap_typ_desc ⇒ heap_typ_desc"
where
  hul0:  "htd_update_list p [] d = d"
| hul1:  "htd_update_list p (x#xs) d = htd_update_list (p+1) xs (d(p := (True,snd (d p) ++ x)))"

definition dom_tll :: "addr ⇒ typ_slice list ⇒ s_addr set" where
  "dom_tll p xs ≡ {(p + of_nat x,SIndexVal) | x. x < length xs} ∪
                   {(p + of_nat x,SIndexTyp n) | x n. x < length xs ∧ (xs ! x) n ≠ None}"

definition (in c_type) typ_slices :: "'a itself ⇒ typ_slice list" where
  "typ_slices t ≡ map (λn. list_map (typ_slice_t (typ_uinfo_t TYPE('a)) n)) [0..<size_of TYPE('a)]"

definition (in c_type) ptr_retyp :: "'a ptr ⇒ heap_typ_desc ⇒ heap_typ_desc" where
  "ptr_retyp p ≡ htd_update_list (ptr_val p) (typ_slices TYPE('a))"

definition (in c_type) field_fd :: "'a itself ⇒ qualified_field_name ⇒ 'a field_desc" where
  "field_fd t n ≡ field_desc (field_typ t n)"

definition tag_disj_typ :: "'a::c_type itself ⇒ 'b::c_type itself ⇒ bool" ("_ ⊥⇩τ _") where
  "s ⊥⇩τ t ≡ typ_uinfo_t s ⊥⇩t typ_uinfo_t t"

text ‹----›

lemma wf_heap_val_SIndexVal_STyp_simp [simp]:
  "wf_heap_val s ⟹ s (x,SIndexVal) ≠ Some (STyp t)"
  apply(clarsimp simp: wf_heap_val_def)
  apply(drule spec [where x=x])
  apply clarsimp
  apply(cases t, simp)
  apply fast
  done

lemma wf_heap_val_SIndexTyp_SValue_simp [simp]:
  "wf_heap_val s ⟹ s (x,SIndexTyp n) ≠ Some (SValue v)"
  apply(unfold wf_heap_val_def)
  apply clarify
  apply(drule_tac x=x in spec)
  apply clarsimp
  done

lemma (in mem_type) field_tag_sub:
  "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n) ⟹
      {&(p→f)..+size_td t} ⊆ {ptr_val (p::'a ptr)..+size_of TYPE('a)}"
  apply(clarsimp simp: field_ti_def split: option.splits)
  apply(drule intvlD, clarsimp simp: field_lvalue_def field_offset_def)
  apply(drule field_lookup_export_uinfo_Some)
  apply(subst add.assoc)
  apply(subst Abs_fnat_homs)
  apply(rule intvlI)
  apply(simp add: size_of_def typ_uinfo_t_def)
  apply(drule td_set_field_lookupD)
  apply(drule td_set_offset_size)
  apply(simp)
  done

lemma typ_slice_t_not_empty [simp]:
  "typ_slice_t t n ≠ []"
  by (cases t, simp)

lemma list_map_typ_slice_t_not_empty [simp]:
  "list_map (typ_slice_t t n) ≠ Map.empty"
  by(simp add: list_map_def)

lemma (in c_type) s_footprint:
  "s_footprint (p::'a ptr) =
     {(ptr_val p + of_nat x,k) | x k.
        x < size_of TYPE('a) ∧
        (k=SIndexVal ∨ (∃n. k=SIndexTyp n ∧ n < length (typ_slice_t (typ_uinfo_t TYPE('a)) x)))}"
  by (auto simp: s_footprint_def s_footprint_untyped_def size_of_def )

lemma (in mem_type) ptr_val_SIndexVal_in_s_footprint [simp]:
  "(ptr_val p, SIndexVal) ∈ s_footprint (p::'a ptr)"
  apply(simp add: s_footprint)
  apply(rule exI [where x=0])
  by auto

lemma (in c_type) s_footprintI:
  "⟦ n < length (typ_slice_t (typ_uinfo_t TYPE('a)) x); x < size_of TYPE('a) ⟧ ⟹
      (ptr_val p + of_nat x, SIndexTyp n) ∈ s_footprint (p::'a ptr)"
  apply(simp add: s_footprint)
  apply(rule exI [where x=x])
  apply auto
  done

lemma (in c_type) s_footprintI2:
  "x < size_of TYPE('a) ⟹ (ptr_val p + of_nat x, SIndexVal) ∈ s_footprint (p::'a ptr)"
  apply(simp add: s_footprint)
  apply(rule exI [where x=x])
  apply auto
  done

lemma (in c_type) s_footprintD:
  "(x,k) ∈ s_footprint p ⟹ x ∈ {ptr_val (p::'a ptr)..+size_of TYPE('a)}"
  by (auto simp: s_footprint elim: intvlI)

lemma (in mem_type) s_footprintD2:
  "(x,SIndexTyp n) ∈ s_footprint (p::'a ptr) ⟹
      n < length (typ_slice_t (typ_uinfo_t TYPE('a)) (unat (x - ptr_val p)))"
  by (clarsimp simp add: s_footprint)
     (metis len_of_addr_card max_size nat_less_le of_nat_inverse order_less_le_trans)
 
lemma (in c_type) s_footprint_restrict:
  "x ∈ s_footprint p ⟹ (s |` s_footprint p) x = s x"
  by (rule restrict_in)

lemma restrict_s_fst:
  "fst (restrict_s d X x) ⟹ fst (d x)"
  by (clarsimp simp: restrict_s_def)

lemma restrict_s_map_le [simp]:
  "snd (restrict_s d X x) ⊆⇩m snd (d x)"
  by (auto simp: restrict_s_def map_le_def)

lemma dom_list_map [simp]:
  "dom (list_map xs) = {0..<length xs}"
  by (auto simp: list_map_def)

lemma list_map [simp]:
  "n < length xs ⟹ list_map xs n = Some (xs ! n)"
  by (force simp: list_map_def set_zip)

lemma list_map_eq:
  "list_map xs n = (if n < length xs then Some (xs ! n) else None)"
  by (force simp: list_map_def set_zip)

lemma valid_footprintI:
  "⟦ 0 < size_td t; ⋀y. y < size_td t ⟹ list_map (typ_slice_t t y) ⊆⇩m snd (d (x + of_nat y)) ∧
      fst (d (x + of_nat y)) ⟧ ⟹
      valid_footprint d x t"
  by (simp add: valid_footprint_def)

lemma valid_footprintD:
  "⟦ valid_footprint d x t; y < size_td t ⟧ ⟹
      list_map (typ_slice_t t y) ⊆⇩m snd (d (x + of_nat y)) ∧
          fst (d (x + of_nat y))"
 by (simp add: valid_footprint_def Let_def)

lemma (in c_type) h_t_valid_taut:
  "d,g ⊨⇩t p ⟹ d,(λx. True) ⊨⇩t p"
  by (simp add: h_t_valid_def)

lemma (in c_type) h_t_valid_restrict:
  "restrict_s d (s_footprint p),g ⊨⇩t p = d,g ⊨⇩t p"
  apply (simp add: h_t_valid_def valid_footprint_def Let_def)
  apply (fastforce simp: restrict_s_def map_le_def size_of_def intro: s_footprintI s_footprintI2)
  done

lemma (in c_type) h_t_valid_restrict2:
  "⟦ d,g ⊨⇩t p; restrict_s d (s_footprint p) = restrict_s d' (s_footprint p)
       ⟧ ⟹ d',g ⊨⇩t (p::'a ptr)"
  apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
  apply(rule conjI; clarsimp?)
   apply(clarsimp simp: map_le_def)
   apply(drule_tac x="(ptr_val p + of_nat y)" in fun_cong)
   apply(clarsimp simp: restrict_s_def)
   apply(drule_tac x=a in fun_cong)
   apply(fastforce simp: size_of_def intro: s_footprintI split: if_split_asm)
  apply(drule_tac x="(ptr_val p + of_nat y)" in fun_cong)
  apply(fastforce simp: size_of_def restrict_s_def intro: s_footprintI2)
  done

lemma lift_state_wf_heap_val [simp]:
  "wf_heap_val (lift_state (h,d))"
  unfolding wf_heap_val_def
  by (auto simp: lift_state_def split: option.splits)

lemma wf_hs_proj_d:
  "fst (proj_d s x) ⟹ s (x,SIndexVal) ≠ None"
  by (auto simp: proj_d_def)


lemma (in c_type) s_valid_g:
  "s,g ⊨⇩s p ⟹ g p"
  by (simp add: s_valid_def h_t_valid_def)

lemma (in c_type) lift_typ_heap_if:
  "lift_typ_heap g s = (λ(p::'a ptr). if s,g ⊨⇩s p then Some (from_bytes
      (heap_list_s s (size_of TYPE('a)) (ptr_val p))) else None)"
  by (force simp: lift_typ_heap_def)

lemma (in c_type) lift_typ_heap_s_valid:
  "lift_typ_heap g s p = Some x ⟹ s,g ⊨⇩s p"
  by (simp add: lift_typ_heap_if split: if_split_asm)

lemma (in c_type) lift_typ_heap_g:
  "lift_typ_heap g s p = Some x ⟹ g p"
  by (fast dest: lift_typ_heap_s_valid s_valid_g)

lemma lift_state_empty [simp]:
  "lift_state (h,empty_htd) = Map.empty"
 by (auto simp: lift_state_def empty_htd_def split: s_heap_index.splits)

lemma lift_state_eqI:
  "⟦ h x = h' x; d x = d' x ⟧ ⟹ lift_state (h,d) (x,k) = lift_state (h',d') (x,k)"
  by (clarsimp simp: lift_state_def split: s_heap_index.splits)

lemma proj_h_lift_state:
  "fst (d x) ⟹  proj_h (lift_state (h,d)) x = h x"
  by (clarsimp simp: proj_h_def lift_state_def)

lemma lift_state_proj_simp [simp]:
  "lift_state (proj_h (lift_state (h, d)), d) = lift_state (h, d)"
  by (auto simp: lift_state_def proj_h_def split: s_heap_index.splits option.splits)

lemma f2l_length [simp]:
  "length (fun2list f n) = n"
  by (simp add: fun2list_def)

lemma GREATEST_lt [simp]:
  "0 < n ⟹ (GREATEST x. x < n) = n - (1::nat)"
  by (rule Greatest_equality; simp)

lemma fun2list_nth [simp]:
  "x < n ⟹ fun2list f n ! x = f x"
  by (clarsimp simp: fun2list_def)

lemma proj_d_lift_state:
  "proj_d (lift_state (h,d)) = d"
  apply(rule ext)
  subgoal for x
    apply(cases "d x")
    apply(auto simp: proj_d_def lift_state_def Let_def split: option.splits)
    done
  done

lemma lift_state_proj [simp]:
  "wf_heap_val s ⟹ lift_state (proj_h s,proj_d s) = s"
  apply (clarsimp simp: proj_h_def proj_d_def lift_state_def fun_eq_iff
                 split: if_split_asm s_heap_index.splits option.splits)
  apply safe
    apply (metis s_heap_tag.simps s_heap_value.exhaust wf_heap_val_SIndexTyp_SValue_simp)
   apply (metis id_apply s_heap_value.exhaust s_heap_value.simps(5) wf_heap_val_SIndexVal_STyp_simp)
  apply (metis s_heap_tag.simps s_heap_value.exhaust wf_heap_val_SIndexTyp_SValue_simp)
  done

lemma lift_state_Some:
  "lift_state (h,d) (p,SIndexTyp n) = Some t ⟹ snd (d p) n = Some (s_heap_tag t)"
  apply (simp add: lift_state_def split: option.splits split: if_split_asm)
  apply (cases t; simp)
  done

lemma lift_state_Some2:
  "snd (d p) n = Some t ⟹
      ∃v. lift_state (h,d) (p,SIndexTyp n) = Some (STyp t)"
  by (simp add: lift_state_def split: option.split)

lemma (in c_type) h_t_s_valid:
  "lift_state (h,d),g ⊨⇩s p = d,g ⊨⇩t p"
  by (simp add: s_valid_def proj_d_lift_state)

lemma (in c_type) lift_t:
  "lift_typ_heap g (lift_state s) = lift_t g s"
  by (simp add: lift_t_def)

lemma (in c_type) lift_t_h_t_valid:
  "lift_t g (h,d) p = Some x ⟹ d,g ⊨⇩t p"
  by (force simp: lift_t_def h_t_s_valid dest: lift_typ_heap_s_valid)

lemma (in c_type) lift_t_g:
  "lift_t g s p = Some x ⟹ g p"
  by (force simp: lift_t_def dest: lift_typ_heap_g)

lemma (in c_type) lift_t_proj [simp]:
  "wf_heap_val s ⟹ lift_t g (proj_h s, proj_d s) = lift_typ_heap g s"
  by (simp add: lift_t_def)

lemma valid_footprint_Some:
  assumes valid: "valid_footprint d p t" and size: "x < size_td t"
  shows "fst (d (p + of_nat x))"
proof (cases "of_nat x=(0::addr)")
  case True
  with valid show ?thesis by (force simp add: valid_footprint_def Let_def)
next
  case False
  with size valid show ?thesis by (force simp: valid_footprint_def Let_def)
qed

lemma (in c_type) h_t_valid_Some:
  "⟦ d,g ⊨⇩t (p::'a ptr); x < size_of TYPE('a) ⟧ ⟹
    fst (d (ptr_val p + of_nat x))"
  by (force simp: h_t_valid_def size_of_def   dest: valid_footprint_Some)

lemma (in c_type) h_t_valid_ptr_safe:
  "d,g ⊨⇩t (p::'a ptr) ⟹ ptr_safe p d"
  apply(clarsimp simp: ptr_safe_def h_t_valid_def valid_footprint_def s_footprint_def
                       s_footprint_untyped_def dom_s_def size_of_def Let_def)
  by (metis (mono_tags, opaque_lifting) domIff list_map map_le_def option.simps(3) surj_pair)

lemma (in c_type) lift_t_ptr_safe:
  "lift_t g (h,d) (p::'a ptr) = Some x ⟹ ptr_safe p d"
  by (fast dest: lift_t_h_t_valid h_t_valid_ptr_safe)

lemma (in c_type) s_valid_Some:
  "⟦ d,g ⊨⇩s (p::'a ptr); x < size_of TYPE('a) ⟧ ⟹
       d (ptr_val p + of_nat x,SIndexVal) ≠ None"
  by (auto simp: s_valid_def dest!: h_t_valid_Some wf_hs_proj_d split: option.splits)

lemma heap_list_s_heap_list_dom:
  "⋀n. (λx. (x,SIndexVal)) ` {n..+k} ⊆ dom_s d ⟹
        heap_list_s (lift_state (h,d)) k n = heap_list h k n"
proof (induct k)
  case 0 show ?case by (simp add: heap_list_s_def)
next
  case (Suc k)
  hence "(λx. (x,SIndexVal)) ` {n + 1..+k} ⊆ dom_s d"
    by (force intro: intvl_plus_sub_Suc subset_trans simp: image_def)
  with Suc have "heap_list_s (lift_state (h, d)) k (n + 1) =
      heap_list h k (n + 1)" by simp
  moreover from this Suc have "(n,SIndexVal) ∈ dom_s d"
    by (force simp: dom_s_def image_def intro: intvl_self)
  ultimately show ?case
    by (auto simp add: heap_list_s_def proj_h_lift_state dom_s_def)
qed

lemma (in c_type) heap_list_s_heap_list:
  "d,(λx. True) ⊨⇩t (p::'a ptr) ⟹
          heap_list_s (lift_state (h,d)) (size_of TYPE('a)) (ptr_val p)
              = heap_list h (size_of TYPE('a)) (ptr_val p)"
  apply(drule h_t_valid_ptr_safe)
  apply(clarsimp simp: ptr_safe_def)
  apply(subst heap_list_s_heap_list_dom)
   apply(clarsimp simp: dom_s_def)
   apply(drule_tac c="(x,SIndexVal)" in subsetD)
    apply(clarsimp simp: intvl_def)
    apply(erule s_footprintI2)
   apply clarsimp+
  done

lemma (in c_type) lift_t_if:
  "lift_t g (h,d) = (λp. if d,g ⊨⇩t p then Some (h_val h (p::'a ptr)) else None)"
  by (force simp: lift_t_def lift_typ_heap_if h_t_s_valid h_val_def
                  heap_list_s_heap_list h_t_valid_taut)

lemma (in c_type) lift_lift_t:
  "d,g ⊨⇩t (p::'a ptr) ⟹ lift h p = the (lift_t g (h,d) p)"
  by (simp add: lift_t_if lift_def)

lemma (in c_type) lift_t_lift:
  "lift_t g (h,d) (p::'a ptr) = Some v ⟹ lift h p = v"
  by (simp add: lift_t_if lift_def split: if_split_asm)

lemma heap_update_list_same:
  "⋀h p k. ⟦ 0 < k; k ≤ addr_card - length v ⟧ ⟹ heap_update_list (p + of_nat k) v h p = h p"
proof (induct v)
  case Nil show ?case by simp
next
  case (Cons x xs)
  have "heap_update_list (p + of_nat k) (x # xs) h p =
        heap_update_list (p + of_nat (k + 1)) xs (h(p + of_nat k := x)) p"
    by (simp add: ac_simps)
  also have "… = (h(p + of_nat k := x)) p"
  proof -
    from Cons have "k + 1 ≤ addr_card - length xs" by simp
    with Cons show ?thesis by (simp only:)
  qed
  also have "… = h p"
  proof -
    from Cons have "of_nat k ≠ (0::addr)"
      by - (erule of_nat_neq_0, simp add: addr_card)
    thus ?thesis by clarsimp
  qed
  finally show ?case .
qed

lemma heap_list_update:
  "⋀h p. length v ≤ addr_card ⟹
          heap_list (heap_update_list p v h) (length v) p = v"
proof (induct v)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  hence "heap_update_list (p + of_nat 1) xs (h(p := x)) p = (h(p := x)) p"
    by - (rule heap_update_list_same, auto)
  with Cons show ?case by simp
qed

lemma (in mem_type) heap_list_update_to_bytes:
  "heap_list (heap_update_list p (to_bytes (v::'a) (heap_list h (size_of TYPE('a)) p)) h)
             (size_of TYPE('a)) p = to_bytes v (heap_list h (size_of TYPE('a)) p)"
  by (metis (mono_tags) heap_list_length heap_list_update len less_imp_le max_size)

lemma (in mem_type) heap_list_update_to_bytes_padding:
  "length bs = size_of TYPE('a) ⟹ heap_list (heap_update_list p (to_bytes (v::'a) bs) h)
             (size_of TYPE('a)) p = to_bytes v bs"
  by (metis heap_list_update local.len local.max_size nless_le)

lemma (in mem_type) h_val_heap_update[simp]:
  "h_val (heap_update p v h) p = (v::'a)"
  by (simp add: h_val_def heap_update_def heap_list_update_to_bytes inv)

lemma (in mem_type) h_val_heap_update_padding:
  fixes p:: "'a ptr"
  shows "length bs = size_of TYPE('a) ⟹ h_val (heap_update_padding p v bs h) p = v"
  apply (simp add: heap_update_padding_def h_val_def)
  by (metis heap_list_update inv le_eq_less_or_eq len max_size)

lemma heap_list_update_disjoint_same:
  shows "⋀q. {p..+length v} ∩ {q..+k} = {} ⟹
             heap_list (heap_update_list p v h) k q = heap_list h k q"
proof (induct k)
  case 0 show ?case by simp
next
  case (Suc n)
  hence "{p..+length v} ∩ {q + 1..+n} = {}"
    by (force intro: intvl_plus_sub_Suc)
  with Suc have "heap_list (heap_update_list p v h) n (q + 1) =
      heap_list h n (q + 1)" by simp
  moreover have "heap_update_list (q + of_nat (unat (p - q))) v h q = h q"
  proof (cases v)
    case Nil thus ?thesis by simp
  next
    case (Cons y ys)
    with Suc have "0 < unat (p - q)"
      by (cases "p=q")
         (simp add: intvl_start_inter unat_gt_0)+
    moreover have "unat (p - q) ≤ addr_card - length v" (is ?G)
    proof (rule ccontr)
      assume "¬ ?G"
      moreover from Suc have "q ∉ {p..+length v}"
        by (fast intro: intvl_self)
      ultimately show False
        by (simp only: linorder_not_le len_of_addr_card [symmetric])
           (frule_tac p=q in intvl_self_offset, force+)
    qed
    ultimately show ?thesis by (rule heap_update_list_same)
  qed
  ultimately show ?case by simp
qed

lemma heap_update_nmem_same:
  assumes nmem: "q ∉ {p..+length v}"
  shows "heap_update_list p v h q = h q"
proof -
  from nmem have "heap_list (heap_update_list p v h) 1 q = heap_list h 1 q"
    by - (rule heap_list_update_disjoint_same, force dest: intvl_Suc)
  thus ?thesis by simp
qed

lemma heap_update_mem_same:
  "⟦ q ∈ {p..+length v}; length v < addr_card ⟧ ⟹
      heap_update_list p v h q = heap_update_list p v h' q"
  by (induct v arbitrary: p h h'; simp)
     (fastforce dest: intvl_neq_start simp: heap_update_list_same [where k=1, simplified])

lemma sub_tag_proper_TypScalar [simp]:
  "¬ t < TypDesc algn' (TypScalar n algn d) nm"
  by (simp add: typ_tag_lt_def typ_tag_le_def)

lemma tag_disj_com [simp]:
  "f ⊥⇩t g = g ⊥⇩t f"
  by (force simp: tag_disj_def)

lemma typ_slice_set':
  "∀m n. fst ` set (typ_slice_t s n)  ⊆ fst ` td_set s m"
  "∀m n. fst ` set (typ_slice_struct st n) ⊆ fst ` td_set_struct st m"
  "∀m n. fst ` set (typ_slice_list xs n) ⊆ fst ` td_set_list xs m"
  "∀m n. fst ` set (typ_slice_tuple x n) ⊆ fst ` td_set_tuple x m"
  apply(induct s and st and xs and x, all ‹clarsimp simp: ladder_set_def›)
   apply auto[1]
  apply (rule conjI; clarsimp)
   apply force
  apply(thin_tac "All P" for P)
  apply force
  done

lemma typ_slice_set:
  "fst ` set (typ_slice_t s n) ⊆ fst ` td_set s m"
  using typ_slice_set'(1) [of s] by clarsimp

lemma typ_slice_struct_set:
  "(s,t) ∈ set (typ_slice_struct st n) ⟹ ∃k. (s,k) ∈ td_set_struct st m"
  using typ_slice_set'(2) [of st] by force

lemma typ_slice_set_sub:
  "typ_slice_t s m ≤ typ_slice_t t n ⟹
      fst ` set (typ_slice_t s m) ⊆ fst ` set (typ_slice_t t n)"
  by (force simp: image_def prefix_def less_eq_list_def)

lemma ladder_set_self:
  "s ∈ fst ` set (typ_slice_t s n)"
  by (cases s) (auto simp: ladder_set_def)

lemma typ_slice_sub:
  "typ_slice_t s m ≤ typ_slice_t t n ⟹ s ≤ t"
  apply(drule typ_slice_set_sub)
  using ladder_set_self [of s m] typ_slice_set [of t n 0]
  apply(force simp: typ_tag_le_def)
  done

lemma typ_slice_self:
  "(s,True) ∈ set (typ_slice_t s 0)"
  by (cases s) simp

lemma typ_slice_struct_nmem:
  "(TypDesc algn st nm,n) ∉ set (typ_slice_struct st k)"
  by (fastforce dest: typ_slice_struct_set td_set_struct_size_lte)

lemma typ_slice_0_prefix:
  "0 < n ⟹ ¬ typ_slice_t t 0 ≤ typ_slice_t t n ∧ ¬ typ_slice_t t n ≤ typ_slice_t t 0"
  by (cases t) (fastforce simp: less_eq_list_def typ_slice_struct_nmem dest: set_mono_prefix)

lemma prefix_eq_nth:
  "xs ≤ ys = ((∀i. i < length xs ⟶ xs ! i = ys ! i) ∧ length xs ≤ length ys)"
  apply(rule iffI; clarsimp simp: less_eq_list_def prefix_def nth_append)
  by (metis append_take_drop_id nth_take_lemma order_refl take_all)

lemma map_prefix_same_cases:
  "⟦ list_map xs ⊆⇩m f; list_map ys ⊆⇩m f ⟧ ⟹ xs ≤ ys ∨ ys ≤ xs"
  using linorder_linear[where x="length xs" and y="length ys"]
  apply(clarsimp simp: prefix_eq_nth map_le_def prefix_def)
  apply (erule disjE)
   apply clarsimp
  subgoal for i
    by ((drule_tac x=i in bspec, simp)+, force dest: sym)
  apply clarsimp
  subgoal for i
    by ((drule_tac x=i in bspec, simp)+, force dest: sym)
  done

lemma list_map_mono:
  "xs ≤ ys ⟹ list_map xs ⊆⇩m list_map ys"
  by (auto simp: map_le_def prefix_def nth_append less_eq_list_def)

lemma map_list_map_trans:
  "⟦ xs ≤ ys; list_map ys ⊆⇩m f ⟧ ⟹ list_map xs ⊆⇩m f"
  apply(drule list_map_mono)
  apply(erule (1) map_le_trans)
  done

lemma valid_footprint_le:
  "valid_footprint d x t ⟹ size_td t ≤ addr_card"
  apply(clarsimp simp: valid_footprint_def Let_def)
  apply(rule ccontr)
  apply(frule_tac x=addr_card in spec)
  apply(drule_tac x=0 in spec)
  apply clarsimp
  apply(drule (1) map_prefix_same_cases)
  apply(simp add: typ_slice_0_prefix addr_card)
  done

lemma typ_slice_True_set':
  "∀s k m. (s,True) ∈ set (typ_slice_t t k) ⟶ (s,k+m) ∈ td_set t m"
  "∀s k m. (s,True) ∈ set (typ_slice_struct st k) ⟶ (s,k+m) ∈ td_set_struct st m"
  "∀s k m. (s,True) ∈ set (typ_slice_list xs k) ⟶ (s,k+m) ∈ td_set_list xs m"
  "∀s k m. (s,True) ∈ set (typ_slice_tuple x k) ⟶ (s,k+m) ∈ td_set_tuple x m"
proof (induct t and st and xs and x)
  case (TypDesc nat typ_struct list)
  then show ?case by auto
next
  case (TypScalar nat1 nat2 a)
  then show ?case by auto
next
  case (TypAggregate list)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
   apply clarsimp
   apply(cases dt_tuple, clarsimp)
    subgoal for s k m a b
   apply(thin_tac "All P" for P)
   apply(drule spec [where x=s])
   apply(drule spec [where x="k - size_td a"])
   apply clarsimp
   apply(drule spec [where x="m + size_td a"])
      apply simp
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by auto
qed

lemma typ_slice_True_set:
  "(s,True) ∈ set (typ_slice_t t k) ⟹ (s,k+m) ∈ td_set t m"
  by (simp add: typ_slice_True_set')

lemma typ_slice_True_prefix:
  "typ_slice_t s 0 ≤ typ_slice_t t k ⟹ (s,k) ∈ td_set t 0"
  using typ_slice_self [of s] typ_slice_True_set [of s t k 0]
  by (force simp: less_eq_list_def dest: set_mono_prefix)

lemma tag_sub_prefix [simp]:
  "t < s ⟹ ¬ typ_slice_t s m ≤ typ_slice_t t n"
  by (fastforce dest: typ_slice_sub)

lemma tag_disj_prefix [simp]:
  "s ⊥⇩t t ⟹ ¬ typ_slice_t s m ≤ typ_slice_t t n"
  by (auto dest: typ_slice_sub simp: tag_disj_def typ_slice_sub)

lemma typ_slice_0_True':
  "∀x. x ∈ set (typ_slice_t t 0) ⟶ snd x = True"
  "∀x. x ∈ set (typ_slice_struct st 0) ⟶ snd x = True"
  "∀x. x ∈ set (typ_slice_list xs 0) ⟶ snd x = True"
  "∀x. x ∈ set (typ_slice_tuple y 0) ⟶ snd x = True"
  by (induct t and st and xs and y)  auto

lemma typ_slice_0_True:
  "x ∈ set (typ_slice_t t 0) ⟹ snd x = True"
  by (simp add: typ_slice_0_True')

lemma typ_slice_False_self:
  "k ≠ 0 ⟹ (t,False) ∈ set (typ_slice_t t k)"
  by (cases t) simp

lemma tag_prefix_True:
  "typ_slice_t s k ≤ typ_slice_t t 0 ⟹ k = 0"
  using typ_slice_0_True [of "(s,False)" t]
  apply(clarsimp simp: less_eq_list_def dest!: set_mono_prefix)
  apply(rule ccontr)
  apply(fastforce dest!: typ_slice_False_self[where t=s and k=k])
  done

lemma valid_footprint_neq_nmem:
  assumes valid_p: "valid_footprint d p f" and
          valid_q: "valid_footprint d q g" and
              neq: "p ≠ q" and
             disj: "f ⊥⇩t g ∨ f=g"
  shows "p ∉ {q..+size_td g}" (is ?G)
proof -
  from assms show ?thesis
    apply(clarsimp simp: valid_footprint_def intvl_def Let_def)
    apply(erule disjE)
     apply(drule_tac x=0 in spec)
     apply (fastforce dest: map_prefix_same_cases)
    apply(drule_tac x=0 in spec)
    apply(drule_tac x=k in spec)
    apply clarsimp
    by (metis add.comm_neutral map_prefix_same_cases neq semiring_1_class.of_nat_0 
      typ_slice_0_prefix zero_less_iff_neq_zero)
qed

lemma valid_footprint_sub:
  assumes valid_p: "valid_footprint d p s"
  assumes valid_q: "valid_footprint d q t"
  assumes sub: "¬ t < s"
  shows "p ∉ {q..+size_td t} ∨ field_of (p - q) (s) (t)" (is ?G)
proof -
  from assms show ?thesis
    apply clarsimp
    apply(insert valid_footprint_le[OF valid_q])
    apply(clarsimp simp: valid_footprint_def Let_def)
    apply(drule_tac x=0 in spec)
    apply clarsimp
    apply(drule intvlD)
    apply clarsimp
    apply(drule_tac x=k in spec)
    apply clarsimp
    apply(drule (1) map_prefix_same_cases)
    apply(erule disjE)
     prefer 2
     apply(frule typ_slice_sub)
     apply(subgoal_tac "k = 0")
      prefer 2
      apply(rule ccontr, simp)
      apply(simp add: typ_slice_0_prefix)
     apply simp
    (* given by the fd_tag_consistent condition *)
    apply(drule typ_slice_True_prefix)
    apply(clarsimp simp: field_of_def)
    apply(simp only: unat_simps)
    done
qed

lemma valid_footprint_sub2:
  "⟦ valid_footprint d p s; valid_footprint d q t; ¬ t < s ⟧ ⟹
      q ∉ {p..+size_td s} ∨ p=q"
  apply(clarsimp simp: valid_footprint_def Let_def)
  apply(drule intvlD)
  apply clarsimp
  subgoal for k
    apply(drule spec [where x=k])
    apply clarsimp
    apply(drule spec [where x=0])
    apply clarsimp
    apply(drule (1) map_prefix_same_cases)
    apply(cases "k=0")
     apply simp
    apply(erule disjE)
     prefer 2
     apply(frule typ_slice_sub)
     apply(drule order_le_imp_less_or_eq[where x=t])
     apply clarsimp
     apply(simp add: typ_slice_0_prefix)
    apply(drule tag_prefix_True)
    apply simp
    done
  done

lemma valid_footprint_neq_disjoint:
  "⟦ valid_footprint d p s; valid_footprint d q t; ¬  t < s;
      ¬ field_of (p - q) (s) (t) ⟧ ⟹ {p..+size_td s} ∩ {q..+size_td t} = {}"
  apply(rule ccontr)
  apply(drule intvl_inter)
  apply(erule disjE)
   apply(drule (2) valid_footprint_sub)
   apply clarsimp
  apply(frule (1) valid_footprint_sub2, assumption)
  apply(frule (1) valid_footprint_sub2)
   apply simp
  apply simp
  apply(clarsimp simp: field_of_def)
  apply(clarsimp simp: valid_footprint_def Let_def)
  apply(drule_tac x=0 in spec)+
  apply clarsimp
  apply(drule (1) map_prefix_same_cases [where xs="typ_slice_t s 0"])
  apply(erule disjE)
   apply(drule typ_slice_True_prefix)
   apply simp
  apply(drule typ_slice_sub)
  apply(drule order_le_imp_less_or_eq)
  apply simp
  done

lemma sub_typ_proper_not_same [simp]:
  "¬ t <⇩τ t"
  by (simp add: sub_typ_proper_def)

lemma sub_typ_proper_not_simple [simp]:
  "¬ TYPE('a::c_type) <⇩τ TYPE('b::simple_mem_type)"
  apply(cases "typ_uinfo_t TYPE('b)")
  subgoal for x1 typ_struct
    by(cases typ_struct, auto simp: sub_typ_proper_def)
  done

lemma field_of_sub:
  "field_of p s t ⟹ s ≤ t"
  by (auto simp: field_of_def typ_tag_lt_def typ_tag_le_def)

lemma h_t_valid_neq_disjoint:
  "⟦ d,g ⊨⇩t (p::'a::c_type ptr); d,g' ⊨⇩t (q::'b::c_type ptr);
      ¬ TYPE('b) <⇩τ TYPE('a); ¬ field_of_t p q ⟧ ⟹ {ptr_val p..+size_of TYPE('a)} ∩
          {ptr_val q..+size_of TYPE('b)} = {}"
  by (fastforce dest: valid_footprint_neq_disjoint
                simp: size_of_def h_t_valid_def sub_typ_proper_def field_of_t_def)

lemma field_ti_sub_typ:
  "⟦ field_ti (TYPE('b::mem_type)) f = Some t; export_uinfo t = (typ_uinfo_t TYPE('a::c_type)) ⟧ ⟹
      TYPE('a) ≤⇩τ TYPE('b)"
  by (auto simp: field_ti_def sub_typ_def typ_tag_le_def typ_uinfo_t_def
           dest!: td_set_export_uinfoD td_set_field_lookupD
           split: option.splits)

lemma h_t_valid_neq_disjoint_simple:
  "⟦ d,g ⊨⇩t (p::'a::simple_mem_type ptr); d,g' ⊨⇩t (q::'b::simple_mem_type ptr) ⟧
      ⟹ ptr_val p ≠ ptr_val q ∨ typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b)"
  apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
  apply(drule_tac x=0 in spec)+
  apply clarsimp
  apply(drule (1) map_prefix_same_cases[where xs="typ_slice_t (typ_uinfo_t TYPE('a)) 0"])
  apply(erule disjE; drule typ_slice_sub)
   apply(cases "typ_info_t TYPE('b)", rename_tac typ_struct xs)
  subgoal for x1 typ_struct xs
    apply(cases "typ_struct"; fastforce simp: typ_tag_le_def typ_uinfo_t_def)
    done
  apply(cases "typ_info_t TYPE('a)", rename_tac typ_struct xs)
  subgoal for x1 typ_struct xs
    apply(cases "typ_struct"; simp add: typ_tag_le_def typ_uinfo_t_def)
    done
  done


lemma h_val_heap_same:
  fixes p::"'a::mem_type ptr" and q::"'b::c_type ptr"
  assumes val_p: "d,g ⊨⇩t p" and val_q: "d,g' ⊨⇩t q" and
          subt: "¬ TYPE('a) <⇩τ TYPE('b)" and nf: "¬ field_of_t q p"
  shows "h_val (heap_update p v h) q = h_val h q"
proof -
  from val_p val_q subt nf
  have "{ptr_val p..+length (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p)))} ∩
        {ptr_val q..+size_of TYPE('b)} = {}"
    by (force dest: h_t_valid_neq_disjoint)
  hence "heap_list (heap_update_list (ptr_val p) (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))) h)
                   (size_of TYPE('b)) (ptr_val q) = heap_list h (size_of TYPE('b)) (ptr_val q)"
     by - (erule heap_list_update_disjoint_same)
  thus ?thesis by (simp add: h_val_def heap_update_def)
qed

lemma h_val_heap_same_padding:
  fixes p::"'a::mem_type ptr" and q::"'b::c_type ptr"
  assumes val_p: "d,g ⊨⇩t p" and val_q: "d,g' ⊨⇩t q" and
          subt: "¬ TYPE('a) <⇩τ TYPE('b)" and nf: "¬ field_of_t q p"
  assumes lbs: "length bs = size_of TYPE('a)"
  shows "h_val (heap_update_padding p v bs h) q = h_val h q"
proof -
  from val_p val_q subt nf
  have "{ptr_val p..+length (to_bytes v bs)} ∩
        {ptr_val q..+size_of TYPE('b)} = {}"
    using lbs
    by (force dest: h_t_valid_neq_disjoint)
  hence "heap_list (heap_update_list (ptr_val p) (to_bytes v bs) h)
                   (size_of TYPE('b)) (ptr_val q) = heap_list h (size_of TYPE('b)) (ptr_val q)"
     by - (erule heap_list_update_disjoint_same)
  thus ?thesis by (simp add: h_val_def heap_update_padding_def)
qed

lemma peer_typI:
  "typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b) ⟹ peer_typ (a::'a::c_type itself) (b::'b::c_type itself)"
  by (simp add: peer_typ_def)

lemma peer_typD:
  "peer_typ TYPE('a::c_type) TYPE('b::c_type) ⟹ ¬ TYPE('a) <⇩τ TYPE('b)"
  by (clarsimp simp: peer_typ_def tag_disj_def sub_typ_proper_def order_less_imp_le)

lemma peer_typ_refl [simp]:
  "peer_typ t t"
  by (simp add: peer_typ_def)

lemma peer_typ_simple [simp]:
  "peer_typ TYPE('a::simple_mem_type) TYPE('b::simple_mem_type)"
  apply(clarsimp simp: peer_typ_def tag_disj_def typ_tag_le_def typ_uinfo_t_def)
  apply(erule disjE)
   apply(cases "typ_info_t TYPE('b)")
  subgoal for x1 typ_struct xs
    by(cases typ_struct; simp)
  apply(cases "typ_info_t TYPE('a)")
  subgoal for x1  typ_struct xs
    by(cases typ_struct; simp)
  done

(* fixme: remove *)
lemmas peer_typ_nlt = peer_typD

lemma peer_typ_not_field_of:
  "⟦ peer_typ TYPE('a::c_type) TYPE('b::c_type); ptr_val p ≠ ptr_val q ⟧ ⟹
      ¬ field_of_t (q::'b ptr) (p::'a ptr)"
  by (fastforce simp: peer_typ_def field_of_t_def field_of_def tag_disj_def typ_tag_le_def
                      unat_eq_zero
                dest: td_set_size_lte)

lemma h_val_heap_same_peer:
  "⟦ d,g ⊨⇩t (p::'a::mem_type ptr); d,g' ⊨⇩t (q::'b::c_type ptr);
      ptr_val p ≠ ptr_val q; peer_typ TYPE('a) TYPE('b) ⟧ ⟹
      h_val (heap_update p v h) q = h_val h q"
  apply(erule (1) h_val_heap_same)
   apply(erule peer_typ_nlt)
  apply(erule (1) peer_typ_not_field_of)
  done

lemma h_val_heap_same_peer_padding:
  "⟦ d,g ⊨⇩t (p::'a::mem_type ptr); d,g' ⊨⇩t (q::'b::c_type ptr);
      ptr_val p ≠ ptr_val q; peer_typ TYPE('a) TYPE('b); length bs = size_of TYPE('a) ⟧ ⟹
      h_val (heap_update_padding p v bs h) q = h_val h q"
  apply(erule (1) h_val_heap_same_padding)
   apply(erule peer_typ_nlt)
   apply(erule (1) peer_typ_not_field_of)
  apply assumption
  done

lemma field_offset_footprint_cons_simp [simp]:
  "field_offset_footprint p (x#xs) = {Ptr &(p→x)} ∪ field_offset_footprint p xs"
  unfolding field_offset_footprint_def by (cases x) auto

lemma heap_list_update_list:
  "⟦ n + x ≤ length v; length v < addr_card ⟧ ⟹
      heap_list (heap_update_list p v h) n (p + of_nat x) = take n (drop x v)"
  apply(induct v arbitrary: n x p h; clarsimp)
  subgoal for a list n x p h
    apply(cases x; clarsimp)
     apply(cases n; clarsimp)
     apply (rule conjI)
      apply(subgoal_tac "heap_update_list (p + of_nat 1) list (h(p := a)) p = a", simp)
      apply(subst heap_update_list_same; simp)
     apply(metis add.right_neutral drop0 semiring_1_class.of_nat_0)
    subgoal for nat
      apply(drule meta_spec [where x=n])
      apply(drule meta_spec [where x=nat])
      apply(drule meta_spec  [where x="p+1"])
      apply (simp add: add.assoc)
      done
    done
  done

lemma typ_slice_td_set':
  "∀s m n k. (s,m + n) ∈ td_set t m ∧ k < size_td s ⟶
      typ_slice_t s k ≤ typ_slice_t t (n + k)"
  "∀s m n k. (s,m + n) ∈ td_set_struct st m ∧ k < size_td s ⟶
      typ_slice_t s k ≤ typ_slice_struct st (n + k)"
  "∀s m n k. (s,m + n) ∈ td_set_list ts m ∧ k < size_td s ⟶
      typ_slice_t s k ≤ typ_slice_list ts (n + k)"
  "∀s m n k. (s,m + n) ∈ td_set_tuple x m ∧ k < size_td s ⟶
      typ_slice_t s k ≤ typ_slice_tuple x (n + k)"
  apply(induct t and st and ts and x, all ‹clarsimp simp: split_DTuple_all›)
   apply(safe; clarsimp)
   apply(drule_tac x=s in spec)
   apply(drule_tac x=m in spec)
   apply(drule_tac x=0 in spec)
   apply fastforce
  apply (safe; clarsimp?)
    apply(fastforce dest: td_set_list_offset_le)
   apply(fastforce dest: td_set_offset_size_m)
  apply(rotate_tac)
  apply(drule_tac x=s in spec)
  apply(rename_tac a list s m n k)
  apply(drule_tac x="m + size_td a" in spec)
  apply(drule_tac x="n - size_td a" in spec)
  apply(drule_tac x="k" in spec)
  apply(erule impE)
   apply(subgoal_tac "m + size_td a + (n - size_td a) = m + n", simp)
   apply(fastforce dest: td_set_list_offset_le)
  apply(fastforce dest: td_set_list_offset_le)
  done

lemma typ_slice_td_set:
  "⟦ (s,n) ∈ td_set t 0; k < size_td s ⟧ ⟹
      typ_slice_t s k ≤ typ_slice_t t (n + k)"
  using typ_slice_td_set'(1) [of t]
  apply(drule_tac x=s in spec)
  apply(drule_tac x=0 in spec)
  apply clarsimp
  done

lemma typ_slice_td_set_list:
  "⟦ (s,n) ∈ td_set_list ts 0; k < size_td s ⟧ ⟹
      typ_slice_t s k ≤ typ_slice_list ts (n + k)"
  using typ_slice_td_set'(3) [of ts]
  apply(drule_tac x=s in spec)
  apply(drule_tac x=0 in spec)
  apply clarsimp
  done

lemma h_t_valid_sub:
  "⟦ d,g ⊨⇩t (p::'b::mem_type ptr);
      field_ti TYPE('b) f = Some t; export_uinfo t = (typ_uinfo_t TYPE('a)) ⟧ ⟹
      d,(λx. True) ⊨⇩t ((Ptr &(p→f))::'a::mem_type ptr)"
  apply(clarsimp simp: h_t_valid_def field_ti_def valid_footprint_def Let_def split: option.splits)
  apply(rule conjI)
   apply(simp add: typ_uinfo_t_def export_uinfo_def size_of_def [symmetric, where t="TYPE('a)"])
  apply clarsimp
  apply(drule_tac x="field_offset TYPE('b) f + y" in spec)
  apply(erule impE)
   apply(fastforce simp: field_offset_def field_offset_untyped_def typ_uinfo_t_def size_of_def
                   dest: td_set_offset_size td_set_field_lookupD field_lookup_export_uinfo_Some)
  apply clarsimp
  apply(frule td_set_field_lookupD)
  apply(clarsimp simp: field_lvalue_def ac_simps)
  apply(drule td_set_export_uinfoD)
  apply(drule typ_slice_td_set)
   apply(simp add: size_of_def typ_uinfo_t_def)
  apply(drule field_lookup_export_uinfo_Some)
  apply(simp add: field_offset_def ac_simps field_offset_untyped_def typ_uinfo_t_def export_uinfo_def)
  apply(erule (1) map_list_map_trans)
  done

lemma size_of_tag:
  "size_td (typ_uinfo_t t) = size_of t"
  by (simp add: size_of_def typ_uinfo_t_def)

lemma size_of_neq_implies_typ_uinfo_t_neq [simp]:
  "size_of TYPE('a::c_type) ≠ size_of TYPE('b::c_type) ⟹ typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
  by (metis size_of_tag)

lemma guard_mono_self[simp]:
  "guard_mono g g"
  by (fastforce dest: td_set_field_lookupD td_set_size_lte simp: guard_mono_def)

lemma (in c_type) field_lookup_offset_size:
  "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n) ⟹
      size_td t + n ≤ size_td (typ_info_t TYPE('a))"
  by (fastforce dest: td_set_field_lookupD td_set_offset_size)

lemma (in mem_type) sub_h_t_valid':
  "⟦ d,g ⊨⇩t (p::'a ptr);
     field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (typ_uinfo_t TYPE('b),n);
     guard_mono g (g'::'b::mem_type ptr_guard)  ⟧ ⟹
   d,g' ⊨⇩t ((Ptr (ptr_val p + of_nat n))::'b::mem_type ptr)"
  apply(clarsimp simp: h_t_valid_def c_type_class.h_t_valid_def guard_mono_def valid_footprint_def Let_def size_of_tag)
  apply(drule_tac x="n+y" in spec, erule impE;
        fastforce simp: ac_simps size_of_def c_type_class.size_of_def typ_uinfo_t_def c_type_class.typ_uinfo_t_def
                  dest: td_set_field_lookupD typ_slice_td_set map_list_map_trans td_set_offset_size)
  done

lemma (in mem_type) sub_h_t_valid:
  "⟦ d,g ⊨⇩t (p::'a ptr); (typ_uinfo_t TYPE('b),n) ∈ td_set (typ_uinfo_t TYPE('a)) 0 ⟧ ⟹
      d,(λx. True) ⊨⇩t ((Ptr (ptr_val p + of_nat n))::'b::mem_type ptr)"
  apply(subst (asm) td_set_field_lookup)
   apply(simp add: typ_uinfo_t_def export_uinfo_def wf_desc_map)
  apply(fastforce intro: sub_h_t_valid' simp: guard_mono_def)
  done

lemma (in mem_type) h_t_valid_mono:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n);
      export_uinfo s = typ_uinfo_t TYPE('b); guard_mono g g' ⟧ ⟹
      d,g ⊨⇩t (p::'a ptr) ⟶ d,g' ⊨⇩t (Ptr (&(p→f))::'b::mem_type ptr)"
  apply(clarsimp simp: field_lvalue_def)
  apply(drule field_lookup_export_uinfo_Some)
  apply(clarsimp simp: field_offset_def c_type_class.field_offset_def typ_uinfo_t_def c_type_class.typ_uinfo_t_def field_offset_untyped_def)
  apply(rule sub_h_t_valid'; fast?)
  apply(fastforce simp: c_type_class.typ_uinfo_t_def typ_uinfo_t_def)
  done

lemma (in mem_type) s_valid_mono:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n);
      export_uinfo s = typ_uinfo_t TYPE('b); guard_mono g g' ⟧ ⟹
      d,g ⊨⇩s (p::'a ptr) ⟶ d,g' ⊨⇩s (Ptr (&(p→f))::'b::mem_type ptr)"
  unfolding s_valid_def c_type_class.s_valid_def by (rule h_t_valid_mono)

lemma take_heap_list_le:
  "k ≤ n ⟹ take k (heap_list h n x) = heap_list h k x"
  apply (induct n arbitrary: k x; clarsimp) 
  subgoal for n k x by (cases k; simp)
  done

lemma drop_heap_list_le:
  "k ≤ n ⟹ drop k (heap_list h n x) = heap_list h (n - k) (x + of_nat k)"
  apply (induct n arbitrary: k x; clarsimp) 
  subgoal for n k x by (cases k; simp add: ac_simps)
  done

lemma (in mem_type) h_val_field_from_bytes':
  "⟦ field_ti TYPE('a) f = Some t;
     export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type})) ⟧ ⟹
    h_val h (Ptr &(pa→f) :: 'b ptr) = from_bytes (access_ti⇩0 t (h_val h pa))"
  apply (clarsimp simp: field_ti_def h_val_def c_type_class.h_val_def split: option.splits)
  apply (frule field_lookup_export_uinfo_Some)
  apply (frule_tac bs="heap_list h (size_of TYPE('a)) (ptr_val pa)" in fi_fa_consistentD)
   apply simp
  apply (clarsimp simp: field_lvalue_def field_offset_def field_offset_untyped_def typ_uinfo_t_def
                        field_names_def access_ti⇩0_def)
  apply (subst drop_heap_list_le)
   apply(simp add: size_of_def)
   apply(drule td_set_field_lookupD)
   apply(drule td_set_offset_size)
   apply simp
  apply(subst take_heap_list_le)
   apply(simp add: size_of_def)
   apply(drule td_set_field_lookupD)
   apply(drule td_set_offset_size)
   apply simp
  apply (fold c_type_class.norm_bytes_def)
  apply (subgoal_tac "size_td t = size_of TYPE('b)")
   apply (clarsimp simp: wf_type_class.norm)
  apply(clarsimp simp: c_type_class.size_of_def)
  apply(subst c_type_class.typ_uinfo_size [symmetric])
  apply(unfold c_type_class.typ_uinfo_t_def)
  apply(drule sym)
  apply simp
  done

lemma (in mem_type) h_val_field_from_bytes:
  "⟦ field_ti TYPE('a) f = Some t;
     export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type})) ⟧ ⟹
    h_val (hrs_mem h) (Ptr &(pa→f) :: 'b ptr) = from_bytes (access_ti⇩0 t (h_val (hrs_mem h) pa))"
  by (simp add: h_val_field_from_bytes')

lemma (in mem_type) lift_typ_heap_mono:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n);
      lift_typ_heap g s (p::'a ptr) = Some v;
      export_uinfo t = typ_uinfo_t TYPE('b); guard_mono g g' ⟧ ⟹
          lift_typ_heap g' s (Ptr (&(p→f))::'b::mem_type ptr) = Some (from_bytes (access_ti⇩0 t v))"
  apply(clarsimp simp: c_type_class.lift_typ_heap_if lift_typ_heap_if split: if_split_asm)
  apply(rule conjI; clarsimp?)
   apply(clarsimp simp: heap_list_s_def)
   apply(frule field_lookup_export_uinfo_Some)
   apply(frule_tac bs="heap_list (proj_h s) (size_of TYPE('a)) (ptr_val p)" in fi_fa_consistentD; simp)
   apply(simp add: c_type_class.field_lvalue_def 
      field_lvalue_def c_type_class.field_offset_def field_offset_def  field_offset_untyped_def 
      typ_uinfo_t_def c_type_class.typ_uinfo_t_def
                   field_names_def access_ti⇩0_def)
   apply(subst drop_heap_list_le)
    apply(simp add: size_of_def)
    apply(drule td_set_field_lookupD)
    apply(drule td_set_offset_size)
    apply simp
   apply(subst take_heap_list_le)
    apply(simp add: size_of_def)
    apply(drule td_set_field_lookupD)
    apply(drule td_set_offset_size)
    apply simp
   apply(fold c_type_class.norm_bytes_def)
   apply(subgoal_tac "size_td t = size_of TYPE('b)")
    apply(simp add: wf_type_class.norm)
   apply(clarsimp simp: c_type_class.size_of_def size_of_def)
   apply(subst c_type_class.typ_uinfo_size [symmetric])
   apply(unfold c_type_class.typ_uinfo_t_def)[1]
   apply(drule sym)
    apply simp
  apply (fastforce dest: s_valid_mono)
  done

lemma (in mem_type) lift_t_mono:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n);
      lift_t g s (p::'a ptr) = Some v;
      export_uinfo t = typ_uinfo_t TYPE('b); guard_mono g g' ⟧ ⟹
          lift_t g' s (Ptr (&(p→f))::'b::mem_type ptr) = Some (from_bytes (access_ti⇩0 t v))"
  by (clarsimp simp: lift_t_def c_type_class.lift_t_def lift_typ_heap_mono)

lemma align_td_wo_align_field_lookupD:
  "field_lookup (t::('a,'b) typ_desc) f m = Some (s, n) ⟹ align_td_wo_align s ≤ align_td_wo_align t"
  by(simp add: align_td_wo_align_field_lookup)

lemma (in c_type) align_td_wo_align_uinfo:
  "align_td_wo_align (typ_uinfo_t TYPE('a)) = align_td_wo_align (typ_info_t TYPE('a))"
  by (clarsimp simp: typ_uinfo_t_def)

lemma (in c_type) align_td_uinfo:
  "align_td (typ_uinfo_t TYPE('a)) = align_td (typ_info_t TYPE('a))"
  by (clarsimp simp: typ_uinfo_t_def export_uinfo_def)

lemma align_td_export_uinfo: "align_td (export_uinfo t) = align_td t"
  by (clarsimp simp add: export_uinfo_def)

lemma (in mem_type) align_field_uinfo:
  "align_field (typ_uinfo_t TYPE('a)) = align_field (typ_info_t TYPE('a))"
  apply (standard)
  apply (simp add: align_field)
  apply (clarsimp simp add: typ_uinfo_t_def align_field_def align_field)
  apply (drule field_lookup_export_uinfo_Some_rev)
  apply (clarsimp simp add: align_td_export_uinfo)
  done
 
lemma (in mem_type) ptr_aligned_mono':
  "field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (typ_uinfo_t TYPE('b),n) ⟹
      ptr_aligned (p::'a ptr) ⟶ ptr_aligned (Ptr (&(p→f))::'b::mem_type ptr)"
  apply(clarsimp simp: ptr_aligned_def c_type_class.ptr_aligned_def 
      align_of_def c_type_class.align_of_def 
      field_lvalue_def c_type_class.field_lvalue_def)
  apply(subgoal_tac "align_field (typ_uinfo_t (TYPE('a)))")
   apply(subst (asm) align_field_def)
   apply(drule_tac x=f in spec)
   apply(drule_tac x="typ_uinfo_t TYPE('b)" in spec)
   apply(drule_tac x=n in spec)
   apply clarsimp
   apply(simp add: c_type_class.align_td_uinfo)
   apply(clarsimp simp: field_offset_def field_offset_untyped_def)
   apply(subst unat_word_ariths)
   apply(rule dvd_mod)
    apply(rule dvd_add)
  subgoal
    apply (drule field_lookup_uinfo_Some_rev)
    apply clarsimp
    by (metis ArraysMemInstance.align_td_export_uinfo c_type_class.typ_uinfo_t_def align_td_field_lookup_mem_type power_le_dvd)
  subgoal
    apply(subst unat_of_nat)
    apply(subst mod_less)
     apply(frule td_set_field_lookupD)
     apply(drule td_set_offset_size)
     apply(subst len_of_addr_card)
    using local.max_size local.size_of_def apply force
    apply assumption
    done
  subgoal
   apply(subst len_of_addr_card)
   apply(subgoal_tac "align_of TYPE('b) dvd addr_card")
    apply(subst (asm) c_type_class.align_of_def)
    apply simp
      apply simp
    done
  apply(subst align_field_uinfo)
  apply(rule align_field)
  done

lemma (in mem_type) ptr_aligned_mono:
  "guard_mono (ptr_aligned::'a ptr_guard) (ptr_aligned::'b::mem_type ptr_guard)"
  apply(clarsimp simp: guard_mono_def)
  apply(frule ptr_aligned_mono')
  apply(fastforce simp: field_lvalue_def field_offset_def field_offset_untyped_def)
  done

lemma (in wf_type)  wf_desc_typ_tag [simp]:
  "wf_desc (typ_uinfo_t TYPE('a))"
  by (simp add: typ_uinfo_t_def export_uinfo_def wf_desc_map)

lemma (in c_type) sft1':
  "sub_field_update_t (f#fs) p (v::'a) s =
     (let s' = sub_field_update_t fs p (v::'a) s in
        s'(Ptr &(p→f) ↦ from_bytes (access_ti⇩0 (field_typ TYPE('a) f) v))) |`
        dom (s::'b::c_type typ_heap)"
  by (rule sft1)

lemma size_map_td:
  "size (map_td f g t) = size t"
  "size (map_td_struct f g st) = size st"
  "size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) (map_td_list f g ts) = size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) ts"
  "size_dt_tuple size (λ_. 0) (λ_. 0) (map_td_tuple f g x) = size_dt_tuple size (λ_. 0) (λ_. 0) x"
  by (induct t and st and ts and x) auto

(* case where 'b is a field type of 'a *)

lemma field_names_size':
  "field_names t s ≠ [] ⟶ size s ≤ size (t::('a,'b) typ_info)"
  "field_names_struct st s ≠ [] ⟶ size s ≤ size (st::('a field_desc,'b) typ_struct)"
  "field_names_list ts s ≠ [] ⟶ size s ≤ size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) (ts::(('a,'b) typ_info,field_name,'b) dt_tuple list)"
  "field_names_tuple x s ≠ [] ⟶ size s ≤ size_dt_tuple size (λ_. 0) (λ_. 0) (x::(('a,'b) typ_info,field_name,'b) dt_tuple)"
  by (induct t and st and ts and x) (auto simp: size_map_td size_char_def)

lemma field_names_size:
  "f ∈ set (field_names t s) ⟹ size s ≤ size t"
  by (cases "field_names t s"; simp add: field_names_size')

lemma field_names_size_struct:
  "f ∈ set (field_names_struct st s) ⟹ size s ≤ size st"
  by (cases "field_names_struct st s"; simp add: field_names_size')

lemma field_names_Some3:
  "∀f m s n. field_lookup (t::('a,'b) typ_info) f m = Some (s,n) ⟶
     f ∈ set (field_names t (export_uinfo s))"
  "∀f m s n. field_lookup_struct (st::('a field_desc,'b) typ_struct) f m = Some (s,n) ⟶
     f ∈ set (field_names_struct  st (export_uinfo s))"
  "∀f m s n. field_lookup_list (ts::(('a,'b) typ_info,field_name,'b) dt_tuple list) f m = Some (s,n) ⟶
     f ∈ set (field_names_list ts (export_uinfo s))"
  "∀f m s n. field_lookup_tuple (x::(('a,'b) typ_info,field_name,'b) dt_tuple) f m = Some (s,n) ⟶
     f ∈ set (field_names_tuple x (export_uinfo s))"
  apply(induct t and st and ts and x)
       apply clarsimp
       apply((erule allE)+, erule impE, fast)
       apply simp
       apply(drule field_names_size_struct)
       apply(simp add: size_map_td)
      apply (auto split: option.splits)[4]
  apply clarsimp
  by (metis image_eqI list.collapse)


lemma field_names_SomeD3:
  "field_lookup (t::('a,'b) typ_info) f m = Some (s,n) ⟹ f ∈ set (field_names t (export_uinfo s))"
  by (simp add: field_names_Some3)

lemma empty_not_in_field_names [simp]:
  "[] ∉ set (field_names_tuple x s)"
  by (cases x, auto)

lemma empty_not_in_field_names_list [simp]:
  "[] ∉ set (field_names_list ts s)"
  by (induct ts, auto)

lemma  empty_not_in_field_names_struct [simp]:
  "[] ∉ set (field_names_struct st s)"
  by (cases st, auto)

lemma field_names_Some:
  "∀m f. f ∈ set (field_names (t::('a,'b) typ_info) s) ⟶ (field_lookup t f m ≠ None)"
  "∀m f. f ∈ set (field_names_struct (st::('a field_desc,'b) typ_struct) s) ⟶ (field_lookup_struct st f m ≠ None)"
  "∀m f. f ∈ set (field_names_list (ts::(('a,'b) typ_info,field_name,'b) dt_tuple list) s) ⟶ (field_lookup_list ts f m ≠ None)"
  "∀m f. f ∈ set (field_names_tuple (x::(('a,'b) typ_info,field_name,'b) dt_tuple) s) ⟶ (field_lookup_tuple x f m ≠ None)"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by auto
next
  case (TypScalar nat1 nat2 a)
  then show ?case by auto
next
  case (TypAggregate list)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case
    apply clarsimp
    apply (safe; clarsimp?)
    subgoal for m f
      apply(drule spec [where x=m])
      apply(drule spec [where x=f])
      apply clarsimp
      done
    apply(clarsimp split: option.splits)
    done
  
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by force
qed

lemma dt_snd_field_names_list_simp [simp]:
  "f ∉ dt_snd ` set xs ⟹ ¬ f#fs ∈ set (field_names_list xs s)"
  by (induct xs; clarsimp) (auto simp: split_DTuple_all)

lemma field_names_Some2:
  "∀m f. wf_desc t ⟶ f ∈ set (field_names (t::('a,'b) typ_info) s) ⟶
     (∃n k. field_lookup t f m = Some (k,n) ∧ export_uinfo k = s)"
  "∀m f. wf_desc_struct st ⟶ f ∈ set (field_names_struct (st::('a field_desc,'b) typ_struct) s) ⟶
     (∃n k. field_lookup_struct st f m = Some (k,n) ∧ export_uinfo k = s)"
  "∀m f. wf_desc_list ts ⟶ f ∈ set (field_names_list (ts::(('a,'b) typ_info,field_name,'b) dt_tuple list) s) ⟶
      (∃n k. field_lookup_list ts f m = Some (k,n) ∧ export_uinfo k = s)"
  "∀m f. wf_desc_tuple x ⟶ f ∈ set (field_names_tuple (x::(('a,'b) typ_info,field_name,'b) dt_tuple) s) ⟶
      (∃n k. field_lookup_tuple x f m = Some (k,n) ∧ export_uinfo k = s )"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by auto
next
  case (TypScalar nat1 nat2 a)
  then show ?case by auto
next
  case (TypAggregate list)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: export_uinfo_def)
    subgoal for m f
      apply(safe; clarsimp?)
       apply(drule spec [where x=m])
       apply(fastforce simp: split: option.split)
      apply (cases dt_tuple)
      apply(clarsimp )
      apply(cases f; fastforce)
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply  (clarsimp simp: export_uinfo_def)
    subgoal for m f
      apply(cases f; fastforce)
      done
    done
qed

lemma field_names_SomeD2:
  "⟦ f ∈ set (field_names (t::('a,'b) typ_info) s); wf_desc t ⟧ ⟹
      (∃n k. field_lookup t f m = Some (k,n) ∧ export_uinfo k = s)"
  by (simp add: field_names_Some2)

lemma field_names_SomeD:
  "f ∈ set (field_names (t::('a,'b) typ_info) s) ⟹ (field_lookup t f m ≠ None)"
  by (simp add: field_names_Some)

lemma lift_t_sub_field_update' [rule_format]:
  "⟦ d,g' ⊨⇩t p; ¬ (TYPE('a) <⇩τ TYPE('b)) ⟧ ⟹ fs_consistent fs TYPE('a) TYPE('b) ⟶
      (∀K. K = UNIV - (((field_offset_footprint p (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b))))) - (field_offset_footprint p fs)) ⟶
      lift_t g (heap_update p (v::'a::mem_type) h,d) |` K =
           sub_field_update_t fs p v ((lift_t g (h,d))::'b::mem_type typ_heap) |` K)"
  apply(induct fs)
   apply clarsimp
   apply(rule ext)
  subgoal for x
    apply(clarsimp simp: lift_t_if restrict_map_def)
    apply(erule (2) h_val_heap_same)
    apply(clarsimp simp: field_of_t_def field_offset_footprint_def field_of_def)
    apply(cases x)
    apply(clarsimp simp: field_lvalue_def td_set_field_lookup field_offset_def field_offset_untyped_def)
    subgoal for xa f
      apply(drule_tac x=f in spec)
      apply(fastforce simp: typ_uinfo_t_def dest: field_lookup_export_uinfo_Some_rev field_names_SomeD3)
      done
    done
  subgoal for  a list
    apply clarify
    apply(clarsimp simp: fs_consistent_def)
    apply (rule conjI; clarsimp)
    subgoal for y
      apply(rule ext) 
      subgoal for  x
        apply(cases "x ≠ Ptr &(p→a)")
         apply(clarsimp simp: restrict_map_def)
         apply(drule fun_cong [where x=x])
         apply clarsimp
         apply(fastforce simp: lift_t_if split: if_split_asm)
        apply(clarsimp simp: lift_t_if)
        apply (rule conjI)
         apply clarsimp
         apply(clarsimp simp: h_val_def heap_update_def field_lvalue_def)
         apply(subst heap_list_update_list; simp?)
          apply(simp add: size_of_def)

          apply(subst typ_uinfo_size [symmetric])
          apply(subst typ_uinfo_size [symmetric])
          apply(drule field_names_SomeD2 [where m=0]; clarsimp)
          apply(frule td_set_field_lookupD [where m=0])
          apply(clarsimp simp: field_offset_def field_offset_untyped_def typ_uinfo_t_def)
          apply(drule field_lookup_export_uinfo_Some)
          apply simp
          apply(drule td_set_export_uinfoD)
          apply(simp add: export_uinfo_def)
          apply(drule td_set_offset_size)
          apply fastforce

         apply(drule field_names_SomeD2 [where m=0], clarsimp+)
        subgoal for n k
          apply(frule fi_fa_consistentD [where bs="to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))"] )
           apply simp
          apply(simp add: size_of_def)
          apply(frule field_lookup_export_uinfo_Some)
          apply(simp add: typ_uinfo_t_def)
          apply(subgoal_tac "size_td k = size_td (typ_info_t TYPE('b))")
           prefer 2
           apply(simp flip: export_uinfo_size)
          apply simp
          apply(rule sym)
          apply(fold norm_bytes_def)
          apply(subst typ_uinfo_size [symmetric])
          apply(drule sym [where t="Some (k,n)"])
          apply(simp only: typ_uinfo_t_def)
          apply(simp)
          apply(clarsimp simp: access_ti⇩0_def field_typ_def field_typ_untyped_def)
          apply(drule sym [where s="Some (k,n)"])
          apply simp
          apply(rule norm)
          apply(simp add: size_of_def)
          apply(subst typ_uinfo_size [symmetric])+
          apply(drule td_set_field_lookupD, drule td_set_offset_size)
          apply(fastforce simp: min_def split: if_split_asm)
          done
        apply(clarsimp split: if_split_asm)
        done
      done
    apply(rule ccontr, clarsimp)
    apply(erule notE, rule ext)
    subgoal for x
      apply(cases "x ≠ Ptr &(p→a)")
       apply(clarsimp simp: restrict_map_def)
       apply(drule fun_cong [where x=x])
       apply clarsimp
       apply(rule ccontr, clarsimp)
       apply(erule impE [where P="x ∈ dom (lift_t g (h, d))"])
        apply(clarsimp simp: lift_t_if h_t_valid_def split: if_split_asm)
       apply clarsimp
      apply(clarsimp simp: restrict_map_def)
      apply(rule conjI, clarsimp)
      apply(clarsimp simp: lift_t_if)
      done
    done
  done

lemma lift_t_sub_field_update:
  "⟦ d,g' ⊨⇩t p; ¬ (TYPE('a) <⇩τ TYPE('b))⟧ ⟹
      lift_t g (heap_update p (v::'a::mem_type) h,d) =
          sub_field_update_t (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b))) p v
              ((lift_t g (h,d))::'b::mem_type typ_heap)"
  apply(drule lift_t_sub_field_update' [where fs="(field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b)))"] , assumption+)
    apply(clarsimp simp: fs_consistent_def)
   apply fast
  apply(simp add: restrict_map_def)
  done


(* Bornat-style *)

lemma lift_t_field_ind:
  "⟦ d,g' ⊨⇩t (p::'b::mem_type ptr); d,ga ⊨⇩t (q::'b ptr);
      field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (a,ba);
      field_lookup (typ_info_t TYPE('b::mem_type)) z 0 = Some (c,da) ;
      size_td a = size_of TYPE('a); size_td c = size_of TYPE('c);
      ¬ f ≤ z; ¬ z ≤ f ⟧ ⟹
      lift_t g (heap_update (Ptr (&(p→f))) (v::'a::mem_type) h,d) (Ptr (&(q→z))) =
          ((lift_t g (h,d) (Ptr (&(q→z))))::'c::c_type option)"
  apply(clarsimp simp: lift_t_if h_val_def heap_update_def)
  apply(subgoal_tac "(heap_list (heap_update_list &(p→f) (to_bytes v (heap_list h (size_of TYPE('a)) &(p→f))) h)
                               (size_of TYPE('c)) &(q→z)) =
                     (heap_list h (size_of TYPE('c)) &(q→z))")
   apply(drule arg_cong [where f=from_bytes])
   apply simp
  apply(rule heap_list_update_disjoint_same)
  apply simp
  apply(simp add: field_lvalue_def field_offset_def field_offset_untyped_def)
  apply(simp add: typ_uinfo_t_def field_lookup_export_uinfo_Some)
  apply(frule field_lookup_export_uinfo_Some[where s=c])
  apply(cases "ptr_val p = ptr_val q")
   apply clarsimp
   apply(subst intvl_disj_offset)
   apply(drule fa_fu_lookup_disj_interD)
       apply fast
      apply(simp add: disj_fn_def)
     apply simp
    apply(subst size_of_def [symmetric, where t="TYPE('b)"])
    apply simp
   apply simp
  apply clarsimp
  apply(drule (1) h_t_valid_neq_disjoint, simp)
   apply(rule peer_typ_not_field_of; clarsimp)
  apply(subgoal_tac "{ptr_val p + of_nat ba..+size_td a} ⊆ {ptr_val p..+size_of TYPE('b)}")
   apply(subgoal_tac "{ptr_val q + of_nat da..+size_td c} ⊆ {ptr_val q..+size_of TYPE('b)}")
    apply fastforce
   apply(rule intvl_sub_offset)
   apply(simp add: size_of_def)
   apply(drule td_set_field_lookupD[where k="(c,da)"])
   apply(drule td_set_offset_size)
  apply (smt (verit, ccfv_threshold) add.commute add_le_cancel_right le_trans le_unat_uoi nat_le_linear)
  apply(rule intvl_sub_offset)
  apply(simp add: size_of_def)
  apply(drule td_set_field_lookupD)
  apply(drule td_set_offset_size)
  by (smt (verit, ccfv_threshold) add.commute add_le_imp_le_right le_trans le_unat_uoi nat_le_linear)



(* case where 'b contains a field of type of 'a *)

lemma (in c_type) uvt1':
  "update_value_t (f#fs) v (w::'b) x = (if x=field_offset TYPE('b) f then
      update_ti_t (field_typ TYPE('b) f) (to_bytes_p (v::'a)) (w::'b::c_type) else update_value_t fs v w x)"
  by simp

lemma (in c_type) field_typ_self [simp]:
  "field_typ TYPE('a) [] = typ_info_t TYPE('a)"
  by (simp add: field_typ_def field_typ_untyped_def)

lemma (in mem_type) field_of_t_less_size:
  "field_of_t (p::'a ptr) (x::'b::c_type ptr) ⟹
    unat (ptr_val p - ptr_val x) < size_of TYPE('b)"
  apply(simp add: field_of_t_def field_of_def)
  apply(drule td_set_offset_size)
  apply(subgoal_tac "0 < size_td (typ_info_t TYPE('a)) ")
   apply(simp add: c_type_class.size_of_def)
  apply(simp add: size_of_def [symmetric, where t="TYPE('a)"])
  done

lemma unat_minus:
  "x ≠ 0 ⟹ unat (- (x::addr)) = addr_card - unat x"
  by (metis word_bits_def word_bits_size len_of_addr_card unat_minus)

lemma (in mem_type) field_of_t_nmem:
  "⟦ field_of_t p q; ptr_val p ≠ ptr_val (q::'b::mem_type ptr) ⟧ ⟹
    ptr_val q ∉ {ptr_val (p::'a ptr)..+size_of TYPE('a)}"
  supply unsigned_of_nat [simp del] unsigned_of_int [simp del]
  apply(clarsimp simp: field_of_t_def field_of_def intvl_def)
  apply(drule td_set_offset_size)
  apply(simp add: unat_minus size_of_def)
  apply(subgoal_tac "size_td (typ_info_t TYPE('b)) < addr_card")
   apply(simp only: unat_simps)
   apply (smt add.commute add.left_neutral diff_less_mono2 gr_implies_not0 le_eq_less_or_eq 
    less_diff_conv2 less_trans max_size nat_mod_eq' size_of_def c_type_class.size_of_def)
  by (metis c_type_class.size_of_def mem_type_class.max_size)

lemma (in mem_type) field_of_t_init_neq_disjoint:
  "field_of_t p (x::'b::mem_type ptr) ⟹
    {ptr_val (p::'a ptr)..+size_of TYPE('a)} ∩
    {ptr_val x..+unat (ptr_val p - ptr_val x)} = {}"
  apply(cases "ptr_val p = ptr_val x", simp)
  apply(rule ccontr)
  apply(drule intvl_inter)
  apply(auto simp: field_of_t_nmem le_unat_uoi nat_less_le dest!: intvlD)
  done

lemma (in mem_type) field_of_t_final_neq_disjoint:
  "field_of_t (p::'a ptr) (x::'b ptr) ⟹ {ptr_val p..+size_of TYPE('a)} ∩
      {ptr_val p + of_nat (size_of TYPE('a))..+size_of TYPE('b::mem_type) -
          (unat (ptr_val p - ptr_val x) + size_of TYPE('a))} = {}"
  supply unsigned_of_nat [simp del] unsigned_of_int [simp del]
  apply(rule ccontr)
  apply(drule intvl_inter)
  apply(erule disjE)
   apply(subgoal_tac "ptr_val p ∉ {ptr_val p + of_nat (size_of TYPE('a)) ..+
                                     size_of TYPE('b) - (unat (ptr_val p - ptr_val x) +
                                     size_of TYPE('a))}")
    apply simp
   apply(rule intvl_offset_nmem)
    apply(rule intvl_self)
    apply(subst unat_of_nat)
    apply(subst mod_less)
     apply(subst len_of_addr_card)
     apply(rule max_size)
    apply(rule sz_nzero)
   apply(subst len_of_addr_card)
   apply(thin_tac "x ∈ S" for x S)
   apply(simp add: field_of_t_def field_of_def)
   apply(drule td_set_offset_size)
   apply(simp add: size_of_def)
  subgoal 

  proof -
    have "size_td (typ_info_t (TYPE('b)::'b itself)) ≤ addr_card"
      by (metis c_type_class.size_of_def less_imp_le_nat mem_type_class.max_size)
    then show ?thesis
      by (smt (verit, ccfv_threshold) c_type_class.size_of_def diff_diff_left diff_le_mono2 diff_le_self 
          le_diff_conv le_trans le_unat_uoi nat_le_linear)
  qed
 
  apply(drule intvlD, clarsimp)
  apply(subst (asm) word_unat.norm_eq_iff [symmetric])
  apply(subst (asm) mod_less)
   apply(subst len_of_addr_card)
   apply(rule max_size)
  apply(subst (asm) mod_less)
   apply(subst len_of_addr_card)
   apply(erule less_trans)
   apply(rule max_size)
  apply simp
  done

lemma (in mem_type)  h_val_super_update_bs:
  "field_of_t p x ⟹ h_val (heap_update p (v::'a) h) (x::'b::mem_type ptr) =
      from_bytes (super_update_bs (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p)) ) (heap_list h (size_of TYPE('b)) (ptr_val x)) (unat (ptr_val p - ptr_val x)))"
  apply(simp add: h_val_def c_type_class.h_val_def)
  apply (rule arg_cong [where f = "c_type_class.from_bytes::byte list ⇒ 'b"])
  apply(simp add: heap_update_def c_type_class.heap_update_def super_update_bs_def)
  apply(subst heap_list_split [of "unat (ptr_val p - ptr_val x)" "size_of TYPE('b)"])
   apply(drule field_of_t_less_size)
   apply simp
  apply simp
  apply(subst heap_list_update_disjoint_same)
   apply(drule field_of_t_init_neq_disjoint)
   apply (simp add: len)
  apply(subst take_heap_list_le)
   apply(drule field_of_t_less_size)
   apply simp
  apply simp
  apply(subst heap_list_split [of "size_of TYPE('a)"
                                  "size_of TYPE('b) - unat (ptr_val p - ptr_val x)"])
   apply(frule field_of_t_less_size)
   apply(simp add: field_of_t_def field_of_def)
   apply(drule td_set_offset_size)
   apply(simp add: size_of_def c_type_class.size_of_def)
  apply clarsimp
  apply (rule conjI)
   apply(simp add: heap_list_update_to_bytes)
  apply(subst heap_list_update_disjoint_same)
   apply(drule field_of_t_final_neq_disjoint)
   apply(simp)
  apply(subst drop_heap_list_le)
   apply(simp add: field_of_t_def field_of_def)
   apply(drule td_set_offset_size)
   apply(simp add: size_of_def c_type_class.size_of_def)
  apply simp
  done

lemma (in mem_type)  h_val_super_update_bs_padding:
  "field_of_t p x ⟹ length bs = size_of TYPE('a) ⟹  h_val (heap_update_padding p (v::'a) bs h) (x::'b::mem_type ptr) =
      from_bytes (super_update_bs (to_bytes v bs) (heap_list h (size_of TYPE('b)) (ptr_val x)) (unat (ptr_val p - ptr_val x)))"
  apply(simp add: h_val_def c_type_class.h_val_def)
  apply (rule arg_cong [where f = "c_type_class.from_bytes::byte list ⇒ 'b"])
  apply(simp add: heap_update_padding_def c_type_class.heap_update_padding_def super_update_bs_def)
  apply(subst heap_list_split [of "unat (ptr_val p - ptr_val x)" "size_of TYPE('b)"])
   apply(drule field_of_t_less_size)
   apply simp
  apply simp

  apply(subst heap_list_update_disjoint_same)
   apply(drule field_of_t_init_neq_disjoint)
   apply (simp add: len)
  apply(subst take_heap_list_le)
   apply(drule field_of_t_less_size)
   apply simp
  apply simp
  apply(subst heap_list_split [of "size_of TYPE('a)"
                                  "size_of TYPE('b) - unat (ptr_val p - ptr_val x)"])
   apply(frule field_of_t_less_size)
   apply(simp add: field_of_t_def field_of_def)
   apply(drule td_set_offset_size)
   apply(simp add: size_of_def c_type_class.size_of_def)
  apply clarsimp
  apply (rule conjI)
   apply(simp add: heap_list_update_to_bytes_padding)
  apply(subst heap_list_update_disjoint_same)
   apply(drule field_of_t_final_neq_disjoint)
   apply(simp)
  apply(subst drop_heap_list_le)
   apply(simp add: field_of_t_def field_of_def)
   apply(drule td_set_offset_size)
   apply(simp add: size_of_def c_type_class.size_of_def)
  apply simp
  done

lemma (in c_type) update_field_update':
  "n ∈ (λf. field_offset TYPE('b) f) ` set fs ⟹
      (∃f. update_value_t fs (v::'a) (v'::'b::c_type) n =
          field_update (field_desc (field_typ TYPE('b) f)) (to_bytes_p v) v' ∧ f ∈ set fs ∧ n = field_offset TYPE('b) f)"
  by (induct fs) auto

lemma (in c_type) update_field_update:
  "field_of_t (p::'a ptr) (x::'b ptr) ⟹
      ∃f. update_value_t (field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a))) (v::'a)
          (v'::'b::mem_type) (unat (ptr_val p - ptr_val x)) =
              field_update (field_desc (field_typ TYPE('b) f)) (to_bytes_p v) v' ∧
      f ∈ set (field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a))) ∧
      unat (ptr_val p - ptr_val x) = field_offset TYPE('b) f"
  apply(rule update_field_update')
  apply(clarsimp simp: image_def field_offset_def c_type_class.field_offset_def field_of_t_def field_of_def field_offset_untyped_def)
  apply(simp add: td_set_field_lookup)
  apply clarsimp
  subgoal for f
    apply(simp add: typ_uinfo_t_def c_type_class.typ_uinfo_t_def)
    apply(rule bexI [where x="f"], simp)
    apply(drule field_lookup_export_uinfo_Some_rev)
    apply clarsimp
    apply(drule field_names_SomeD3)
    apply clarsimp
    done
  done

lemma length_fa_ti:
  "⟦ wf_fd s; length bs = size_td s ⟧ ⟹ length (access_ti s w bs) = size_td s"
  apply(drule wf_fd_consD)
  apply(clarsimp simp: fd_cons_def fd_cons_length_def fd_cons_desc_def)
  done

lemma fa_fu_v:
  "⟦ wf_fd s; length bs = size_td s; length bs' = size_td s ⟧ ⟹
      access_ti s (update_ti_t s bs v) bs' = access_ti s (update_ti_t s bs w) bs'"
  apply(drule wf_fd_consD)
  apply(clarsimp simp: fd_cons_def fd_cons_access_update_def fd_cons_desc_def)
  done

lemma fu_fa:
  "⟦ wf_fd s; length bs = size_td s ⟧ ⟹
      update_ti_t s (access_ti s v bs) v = v"
  apply(drule wf_fd_consD)
  apply(clarsimp simp: fd_cons_def fd_cons_update_access_def fd_cons_desc_def)
  done

lemma fu_fu:
  "⟦ wf_fd s; length bs = length bs' ⟧ ⟹
        update_ti_t s bs (update_ti_t s bs' v) = update_ti_t s bs v"
  apply(drule wf_fd_consD)
  apply(clarsimp simp: fd_cons_def fd_cons_double_update_def fd_cons_desc_def)
  done


lemma fu_fa'_rpbs:
  "⟦ export_uinfo s = export_uinfo t; length bs = size_td s; wf_fd s; wf_fd t ⟧ ⟹
       update_ti_t s (access_ti t v bs) w = update_ti_t s (access_ti⇩0 t v) w"
  apply(clarsimp simp: access_ti⇩0_def)
  apply(subgoal_tac "size_td s = size_td t")
   apply(frule_tac bs="access_ti t v bs" in wf_fd_norm_tuD[where t=t])
    apply(subst length_fa_ti; simp)
   apply(frule_tac bs="access_ti t v bs" in wf_fd_norm_tuD)
    apply(subst length_fa_ti; simp)
   apply(clarsimp simp: access_ti⇩0_def)
   apply(thin_tac "norm_tu X Y = Z" for X Y Z)+
   apply(subst (asm) fa_fu_v [where w=v]; simp?)
    apply(simp add: length_fa_ti)
   apply(subst (asm) fa_fu_v [where w=w]; simp?)
    apply(simp add: length_fa_ti; simp)
   apply(subst (asm) fu_fa; (solves ‹simp›)?)
   apply(drule_tac f="update_ti_t s" in arg_cong)
   apply(drule_tac x="update_ti_t s (access_ti t v bs) w" in fun_cong)
   apply(subst (asm) fu_fa; (solves ‹simp›)?)
   apply(fastforce simp: fu_fu length_fa_ti)
  apply(drule_tac f=size_td in arg_cong)
  apply(simp add: export_uinfo_def)
  done

lemma lift_t_super_field_update:
  "⟦ d,g' ⊨⇩t p; TYPE('a) ≤⇩τ TYPE('b) ⟧ ⟹
      lift_t g (heap_update p (v::'a::mem_type) h,d) =
      super_field_update_t p v ((lift_t g (h,d))::'b::mem_type typ_heap)"
  apply(rule ext)
  apply(clarsimp simp: super_field_update_t_def split: option.splits)
  apply(rule conjI; clarsimp)
   apply(simp add: lift_t_if split: if_split_asm)
  apply(rule conjI; clarsimp)
   apply(simp add: lift_t_if  h_val_super_update_bs split: if_split_asm)
   apply(drule sym)
   apply(rename_tac x1 x2)
   apply(drule_tac v=v and v'=x2 in update_field_update)
   apply(clarsimp simp: h_val_def)
   apply(frule_tac m=0 in field_names_SomeD)
   apply clarsimp
   apply(subgoal_tac "export_uinfo a = typ_uinfo_t TYPE('a)")
    prefer  2
    apply(drule_tac m=0 in field_names_SomeD2; clarsimp)
   apply(simp add: from_bytes_def)
   apply(frule_tac bs="heap_list h (size_of TYPE('b)) (ptr_val x1)" and
                   v="to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))" and
                   w=undefined in fi_fu_consistentD)
      apply simp
     apply(simp add: size_of_def)
    apply(clarsimp simp: size_of_def sub_typ_def typ_tag_le_def simp flip: export_uinfo_size)
   apply(simp add: field_offset_def field_offset_untyped_def typ_uinfo_t_def)
   apply(frule field_lookup_export_uinfo_Some)
   apply(simp add: to_bytes_def to_bytes_p_def)
   apply(subst fu_fa'_rpbs; simp?)
     apply(simp add: size_of_def flip: export_uinfo_size)
    apply(fastforce intro: wf_fd_field_lookupD)
   apply(unfold access_ti⇩0_def)[1]
   apply(simp flip: export_uinfo_size)
   apply(simp add: size_of_def access_ti⇩0_def field_typ_def field_typ_untyped_def)
  apply(frule lift_t_h_t_valid)
  apply(simp add: lift_t_if)
  apply(cases "typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b)")
   apply(subst h_val_heap_same_peer; assumption?)
    apply(clarsimp simp: field_of_t_def)
   apply(simp add: peer_typ_def)
  apply(drule (1) h_t_valid_neq_disjoint)
    apply(simp add: sub_typ_proper_def)
    apply(rule order_less_not_sym)
    apply(simp add: sub_typ_def)
   apply assumption
  apply(simp add: h_val_def heap_update_def heap_list_update_disjoint_same)
  done

lemma lift_t_super_field_update_padding:
  "⟦ d,g' ⊨⇩t p; TYPE('a) ≤⇩τ TYPE('b); length bs = size_of TYPE('a) ⟧ ⟹
      lift_t g (heap_update_padding p (v::'a::mem_type) bs h,d) =
      super_field_update_t p v ((lift_t g (h,d))::'b::mem_type typ_heap)"
  apply(rule ext)
  apply(clarsimp simp: super_field_update_t_def split: option.splits)
  apply(rule conjI; clarsimp)
   apply(simp add: lift_t_if split: if_split_asm)
  apply(rule conjI; clarsimp)
   apply(simp add: lift_t_if  h_val_super_update_bs_padding split: if_split_asm)
   apply(drule sym)
   apply(rename_tac x1 x2)
   apply(drule_tac v=v and v'=x2 in update_field_update)
   apply(clarsimp simp: h_val_def)
   apply(frule_tac m=0 in field_names_SomeD)
   apply clarsimp
   apply(subgoal_tac "export_uinfo a = typ_uinfo_t TYPE('a)")
    prefer  2
    apply(drule_tac m=0 in field_names_SomeD2; clarsimp)
   apply(simp add: from_bytes_def)
   apply(frule_tac bs="heap_list h (size_of TYPE('b)) (ptr_val x1)" and
                   v="to_bytes v bs" and
                   w=undefined in fi_fu_consistentD)
      apply simp
     apply(simp add: size_of_def)
    apply(clarsimp simp: size_of_def sub_typ_def typ_tag_le_def simp flip: export_uinfo_size)
   apply(simp add: field_offset_def field_offset_untyped_def typ_uinfo_t_def)
   apply(frule field_lookup_export_uinfo_Some)
   apply(simp add: to_bytes_def to_bytes_p_def)
   apply(subst fu_fa'_rpbs; simp?)
     apply(simp add: size_of_def flip: export_uinfo_size)
    apply(fastforce intro: wf_fd_field_lookupD)
   apply(unfold access_ti⇩0_def)[1]
   apply(simp flip: export_uinfo_size)
   apply(simp add: size_of_def access_ti⇩0_def field_typ_def field_typ_untyped_def)
  apply(frule lift_t_h_t_valid)
  apply(simp add: lift_t_if)
  apply(cases "typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b)")
   apply(subst h_val_heap_same_peer_padding; assumption?)
    apply(clarsimp simp: field_of_t_def)
   apply(simp add: peer_typ_def)
  apply(drule (1) h_t_valid_neq_disjoint)
    apply(simp add: sub_typ_proper_def)
    apply(rule order_less_not_sym)
    apply(simp add: sub_typ_def)
   apply assumption
  apply(simp add: h_val_def heap_update_padding_def heap_list_update_disjoint_same)
  done

lemma field_names_same:
  "k = export_uinfo ti ⟹ field_names ti k = [[]]"
  by (cases ti, clarsimp)

lemma lift_t_heap_update:
  "d,g ⊨⇩t p ⟹ lift_t g (heap_update p v h,d) =
      ((lift_t g (h,d)) (p ↦ (v::'a::mem_type)))"
  apply(subst lift_t_sub_field_update)
    apply fast
   apply(simp add: sub_typ_proper_def)
  apply(simp add: typ_uinfo_t_def Let_def)
  apply(subgoal_tac "access_ti⇩0 (typ_info_t TYPE('a)) = to_bytes_p")
   apply(simp add: field_names_same)
   apply(clarsimp simp: Let_def to_bytes_p_def)
   apply(rule conjI, clarsimp)
    apply(rule ext, clarsimp simp: restrict_self_UNIV)
   apply clarsimp
   apply(clarsimp simp: h_t_valid_def lift_t_if)
  apply(rule ext)
  apply(simp add: to_bytes_p_def to_bytes_def size_of_def access_ti⇩0_def)
  done

lemma field_names_disj:
  "typ_uinfo_t TYPE('a::c_type) ⊥⇩t typ_uinfo_t TYPE('b::mem_type) ⟹
   field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a)) = []"
  apply(rule ccontr)
  apply(subgoal_tac "(∃k. k ∈ set (field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a))))")
   apply clarsimp
   apply(frule field_names_SomeD2 [where m=0], clarsimp+)
   apply(drule field_lookup_export_uinfo_Some)
   apply(drule td_set_field_lookupD)
   apply(fastforce simp: tag_disj_def typ_tag_le_def typ_uinfo_t_def)
  apply(cases "field_names (typ_info_t TYPE('b)) (typ_uinfo_t TYPE('a))"; simp)
  apply fast
  done

lemma lift_t_heap_update_same:
  "⟦ d,g' ⊨⇩t (p::'b::mem_type ptr); typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b) ⟧ ⟹
      lift_t g (heap_update p v h,d) = (lift_t g (h,d)::'a::mem_type typ_heap)"
  apply(subst lift_t_sub_field_update, simp)
   apply(fastforce dest: order_less_imp_le simp: sub_typ_proper_def tag_disj_def)
  apply(simp add: field_names_disj)
  done

lemma lift_heap_update:
  "⟦ d,g ⊨⇩t (p::'a ptr); d,g' ⊨⇩t q ⟧ ⟹ lift (heap_update p v h) q =
      ((lift h)(p := (v::'a::mem_type))) q"
  by (simp add: lift_def h_val_heap_update h_val_heap_same_peer)

lemma (in mem_type) lift_heap_update_p [simp]:
  "lift (heap_update p v h) p = (v::'a)"
  by (simp add: lift_def heap_update_def h_val_def heap_list_update_to_bytes)

lemma lift_heap_update_same:
  "⟦ ptr_val p ≠ ptr_val q; d,g ⊨⇩t (p::'a::mem_type ptr);
      d,g' ⊨⇩t (q::'b::mem_type ptr); peer_typ TYPE('a) TYPE('b) ⟧  ⟹
      lift (heap_update p v h) q = lift h q"
  by (simp add: lift_def h_val_heap_same_peer)

lemma lift_heap_update_same_type:
  fixes p::"'a::mem_type ptr" and q::"'b::mem_type ptr"
  assumes valid: "d,g ⊨⇩t p" "d,g' ⊨⇩t q"
  assumes type: "typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b)"
  shows "lift (heap_update p v h) q = lift h q"
proof -
  from valid type have "ptr_val p ≠ ptr_val q"
    apply(clarsimp simp: h_t_valid_def)
    apply(drule (1) valid_footprint_sub)
     apply(clarsimp simp: tag_disj_def order_less_imp_le)
    apply(fastforce intro: intvl_self
                    simp: field_of_def tag_disj_def typ_tag_le_def
                    simp flip: size_of_def [where t="TYPE('b)"])
    done
  thus ?thesis using valid type
    by (fastforce elim: lift_heap_update_same peer_typI)
qed

lemma lift_heap_update_same_ptr_coerce:
  "⟦ ptr_val q ≠ ptr_val p;
      d,g ⊨⇩t (ptr_coerce (q::'b::mem_type ptr)::'c::mem_type ptr);
      d,g' ⊨⇩t (p::'a::mem_type ptr);
      size_of TYPE('b) = size_of TYPE('c); peer_typ TYPE('a) TYPE('c) ⟧  ⟹
     lift (heap_update q v h) p = lift h p"
  apply(clarsimp simp: lift_def h_val_def heap_update_def size_of_def)
  apply(subst heap_list_update_disjoint_same)
   apply(drule (1) h_t_valid_neq_disjoint)
     apply(erule peer_typD)
    apply(erule peer_typ_not_field_of, simp)
   apply(simp add: size_of_def)
  apply simp
  done

lemma heap_footprintI:
  "⟦ valid_footprint d y t; x ∈ {y..+size_td t} ⟧ ⟹ x ∈ heap_footprint d t"
  by (force simp: heap_footprint_def)

lemma valid_heap_footprint:
  "valid_footprint d x t ⟹ x ∈ heap_footprint d t"
  by (force simp: heap_footprint_def)

lemma heap_valid_footprint:
  "x ∈ heap_footprint d t ⟹ ∃y. valid_footprint d y t ∧ x ∈ {y} ∪ {y..+size_td t}"
  by (simp add: heap_footprint_def)

lemma heap_footprint_Some:
  "x ∈ heap_footprint d t ⟹ d x ≠ (False,Map.empty)"
  by (auto simp: heap_footprint_def intvl_def valid_footprint_def Let_def)


(* Retyping *)

lemma dom_tll_empty [simp]:
  "dom_tll p [] = {}"
  by (clarsimp simp: dom_tll_def)

lemma dom_s_upd [simp]:
  "dom_s (λb. if b = p then (True,a) else d b) =
      (dom_s d - {(p,y) | y. True}) ∪ {(p,SIndexVal)} ∪ {(p,SIndexTyp n) | n. a n ≠ None}"
  unfolding dom_s_def by (cases "d p") auto

lemma dom_tll_cons [simp]:
  "dom_tll p (x#xs) = dom_tll (p + 1) xs ∪ {(p,SIndexVal)} ∪ {(p,SIndexTyp n) | n. x n ≠ None}"
  unfolding dom_tll_def
  apply (rule equalityI; clarsimp)
   apply (rule conjI; clarsimp)

  subgoal using less_Suc_eq_0_disj by auto[1]

  subgoal using less_Suc_eq_0_disj by force
  subgoal using less_Suc_eq_0_disj Suc_mono of_nat_Suc 
    by (smt (verit) Groups.add_ac(2) Groups.add_ac(3) UnCI add.right_neutral 
        mem_Collect_eq nth_Cons' nth_Cons_Suc semiring_1_class.of_nat_simps(1) subsetI)
  done
 


lemma one_plus_x_zero:
  "(1::addr) + of_nat x = 0 ⟹ x ≥ addr_card - 1"
  apply(simp add: addr_card)
  apply(subst (asm) of_nat_1 [symmetric])
  apply(subst (asm) Abs_fnat_homs)
  apply(subst (asm) Word.of_nat_0)
  apply(erule exE) 
  subgoal for q
    apply(cases q; simp)
    done
  done

lemma htd_update_list_dom [rule_format, simp]:
  "length xs < addr_card ⟶ (∀p d. dom_s (htd_update_list p xs d) = dom_s d ∪ dom_tll p xs)"
  by (induct xs; clarsimp) (auto simp: dom_s_def)

(* fixme: this is clag from heap_update_list_same - should be able to prove
   this once for these kinds of update functions *)
lemma htd_update_list_same:
  shows "⋀h p k. ⟦ 0 < k; k ≤ addr_card - length v ⟧ ⟹
      (htd_update_list (p + of_nat k) v) h p = h p"
proof (induct v)
  case Nil show ?case by simp
next
  case (Cons x xs)
  have "htd_update_list (p + of_nat k) (x # xs) h p =
      htd_update_list (p + of_nat (k + 1)) xs (h(p + of_nat k := (True,snd (h (p + of_nat k)) ++ x))) p"
    by (simp add: ac_simps)
  also have "… = (h(p + of_nat k := (True,snd (h (p + of_nat k)) ++ x))) p"
  proof -
    from Cons have "k + 1 ≤ addr_card - length xs" by simp
    with Cons show ?thesis by (simp only:)
  qed
  also have "… = h p"
  proof -
    from Cons have "of_nat k ≠ (0::addr)"
      by - (erule of_nat_neq_0, simp add: addr_card)
    thus ?thesis by clarsimp
  qed
  finally show ?case .
qed

lemma htd_update_list_index [rule_format]:
  "∀p d. length xs < addr_card ⟶ x ∈ {p..+length xs} ⟶
         htd_update_list p xs d x = (True, snd (d x) ++ (xs ! (unat (x - p))))"
  apply(induct xs; clarsimp)
  subgoal for x1 xs p d
    apply(cases "p=x")
     apply simp
     apply(subst of_nat_1 [symmetric])
     apply(subst htd_update_list_same; simp)
    apply(drule spec [where x="p+1"])
    apply(erule impE)
     apply(drule intvl_neq_start; simp)
    apply(subgoal_tac "unat (x - p) = unat (x - (p + 1)) + 1")
     apply simp
    apply (clarsimp simp: unatSuc[symmetric] field_simps)
    done
  done

lemma (in c_type) typ_slices_length [simp]:
  "length (typ_slices TYPE('a)) = size_of TYPE('a)"
  by (simp add: typ_slices_def)

lemma (in c_type) typ_slices_index [simp]:
  "n < size_of TYPE('a) ⟹ typ_slices TYPE('a) ! n =
     list_map (typ_slice_t (typ_uinfo_t TYPE('a)) n)"
  by (simp add: typ_slices_def)

lemma (in c_type) empty_not_in_typ_slices [simp]:
  "Map.empty ∉ set (typ_slices TYPE('a))"
  by (auto simp: typ_slices_def dest: sym)

lemma (in c_type) dom_tll_s_footprint [simp]:
  "dom_tll (ptr_val p) (typ_slices TYPE('a)) = s_footprint (p::'a ptr)"
  by (fastforce simp: list_map_eq typ_slices_def s_footprint_def s_footprint_untyped_def
                      dom_tll_def size_of_def
                split: if_split_asm)

lemma (in mem_type) ptr_retyp_dom [simp]:
  "dom_s (ptr_retyp (p::'a ptr) d) = dom_s d ∪ s_footprint p"
  by (simp add: ptr_retyp_def)

lemma dom_s_empty_htd [simp]:
  "dom_s empty_htd = {}"
  by (clarsimp simp: empty_htd_def dom_s_def)

lemma dom_s_nempty:
  "d x ≠ (False, Map.empty) ⟹ ∃k. (x,k) ∈ dom_s d"
  apply(clarsimp simp: dom_s_def)
  apply(cases "d x", clarsimp)
  using None_not_eq by fastforce

lemma (in mem_type) ptr_retyp_None:
  "x ∉ {ptr_val p..+size_of TYPE('a)} ⟹
    ptr_retyp (p::'a ptr) empty_htd x = (False,Map.empty)"
  using ptr_retyp_dom [of p empty_htd]
  by (fastforce dest: dom_s_nempty s_footprintD)

lemma (in mem_type) ptr_retyp_footprint:
  "x ∈ {ptr_val p..+size_of TYPE('a)} ⟹
      ptr_retyp (p::'a ptr) d x =
        (True,snd (d x) ++ list_map (typ_slice_t (typ_uinfo_t TYPE('a)) (unat (x - ptr_val p))))"
  apply(clarsimp simp: ptr_retyp_def)
  apply(subst htd_update_list_index; simp)
  apply(subst typ_slices_index; simp?)
  apply(drule intvlD, clarsimp)
  by (metis le_unat_uoi linorder_not_less nat_less_le)

lemma (in mem_type) ptr_retyp_Some:
  "ptr_retyp (p::'a ptr) d (ptr_val p) =
     (True,snd (d (ptr_val p)) ++ list_map (typ_slice_t (typ_uinfo_t TYPE('a)) 0))"
  by (simp add: ptr_retyp_footprint)

lemma (in mem_type) ptr_retyp_Some2:
  "x ∈ {ptr_val (p::'a ptr)..+size_of TYPE('a)} ⟹ ptr_retyp p d x ≠ (False,Map.empty)"
  by (auto simp: ptr_retyp_Some ptr_retyp_footprint dest: intvl_neq_start)

lemma snd_empty_htd [simp]:
  "snd (empty_htd x) = Map.empty"
  by (auto simp: empty_htd_def)

lemma (in mem_type) ptr_retyp_d_empty:
  "x ∈ {ptr_val (p::'a ptr)..+size_of TYPE('a)} ⟹
      (∀d. fst (ptr_retyp p d x)) ∧
      snd (ptr_retyp p d x) = snd (d x) ++ snd (ptr_retyp p empty_htd x)"
 by (auto simp: ptr_retyp_Some ptr_retyp_footprint dest: intvl_neq_start)

lemma unat_minus_abs:
  "x ≠ y ⟹ unat ((x::addr) - y) = addr_card - unat (y - x)"
  by (clarsimp simp: unat_sub_if_size)
     (metis (no_types) Nat.diff_cancel Nat.diff_diff_right add.commute len_of_addr_card
                       nat_le_linear not_le trans_le_add1 unat_lt2p wsst_TYs(3))

lemma (in mem_type) ptr_retyp_d:
  "x ∉ {ptr_val (p::'a ptr)..+size_of TYPE('a)} ⟹
      ptr_retyp p d x = d x"
  apply(simp add: ptr_retyp_def)
  apply(subgoal_tac "∃k. ptr_val p = x + of_nat k ∧ 0 < k ∧ k ≤ addr_card - size_of TYPE('a)")
   apply clarsimp
   apply(subst htd_update_list_same; simp)
  apply(rule exI [where x="unat (ptr_val p - x)"])
  apply clarsimp
  apply(cases "ptr_val p = x")
   apply simp
   apply(erule notE)
   apply(rule intvl_self)
   apply simp
  apply(rule conjI)
   apply(subst unat_gt_0)
   apply clarsimp
  apply(rule ccontr)
  apply(erule notE)
  apply(clarsimp simp: intvl_def)
  apply(rule exI [where x="unat (x - ptr_val p)"])
  apply simp
  apply(subst (asm) unat_minus_abs; simp)
  done

lemma (in mem_type) ptr_retyp_valid_footprint_disjoint:
  "⟦ valid_footprint d p s; {p..+size_td s} ∩ {ptr_val q..+size_of TYPE('a)} = {} ⟧
     ⟹ valid_footprint (ptr_retyp (q::'a ptr) d) p s"
  apply(clarsimp simp: valid_footprint_def Let_def)
  apply((subst ptr_retyp_d; clarsimp), fastforce intro: intvlI)+
  done

lemma ptr_retyp_disjoint:
  "⟦ d,g ⊨⇩t (q::'b::mem_type ptr); {ptr_val p..+size_of TYPE('a)} ∩
      {ptr_val q..+size_of TYPE('b)} = {} ⟧ ⟹
      ptr_retyp (p::'a::mem_type ptr) d,g ⊨⇩t q"
  apply(clarsimp simp: h_t_valid_def)
  apply(erule ptr_retyp_valid_footprint_disjoint)
  apply(fastforce simp: size_of_def)
  done

lemma ptr_retyp_d_fst:
  "(x,SIndexVal) ∉ s_footprint (p::'a::mem_type ptr) ⟹ fst (ptr_retyp p d x) = fst (d x)"
  apply(simp add: ptr_retyp_def)
  apply(subgoal_tac "∃k. ptr_val p = x + of_nat k ∧ 0 < k ∧ k ≤ addr_card - size_of TYPE('a)")
   apply(fastforce simp: htd_update_list_same)
  apply(rule exI [where x="unat (ptr_val p - x)"])
  apply clarsimp
  apply(cases "ptr_val p = x")
   apply(fastforce dest: sym)
  apply(rule conjI)
   apply(subst unat_gt_0, clarsimp)
  apply(rule ccontr)
  apply(erule notE)
  apply(subst (asm) unat_minus_abs, simp)
  apply(clarsimp simp: s_footprint_def s_footprint_untyped_def)
  apply(rule exI [where x="unat (x - ptr_val p)"])
  apply(simp add: size_of_def)
  done

lemma (in mem_type) ptr_retyp_d_eq_fst:
  "fst (ptr_retyp p d x) =
     (if x ∈ {ptr_val (p::'a ptr)..+size_of TYPE('a)} then True else fst (d x))"
  by (auto dest!: ptr_retyp_d_empty[where d=d] ptr_retyp_d[where d=d])

lemma (in mem_type) ptr_retyp_d_eq_snd:
  "snd (ptr_retyp p d x) =
     (if x ∈ {ptr_val (p::'a ptr)..+size_of TYPE('a)}
      then snd (d x) ++ snd (ptr_retyp p empty_htd x)
      else snd (d x))"
  by (auto dest!: ptr_retyp_d_empty[where d=d] ptr_retyp_d[where d=d])

lemma lift_state_ptr_retyp_d_empty:
  "x ∈ {ptr_val (p::'a::mem_type ptr)..+size_of TYPE('a)} ⟹
      lift_state (h,ptr_retyp p d) (x,k) =
      (lift_state (h,d) ++ lift_state (h,ptr_retyp p empty_htd)) (x,k)"
  apply(clarsimp simp: lift_state_def map_add_def split: s_heap_index.splits)
  apply safe
     apply(subst ptr_retyp_d_empty; simp)
    apply(subst ptr_retyp_d_empty; simp)
   apply(subst (asm) ptr_retyp_d_empty; simp)
  apply(subst ptr_retyp_d_empty, simp)
  apply(auto split: option.splits)
  done

lemma lift_state_ptr_retyp_d:
  "x ∉ {ptr_val (p::'a::mem_type ptr)..+size_of TYPE('a)} ⟹
      lift_state (h,ptr_retyp p d) (x,k) = lift_state (h,d) (x,k)"
  by (clarsimp simp: lift_state_def ptr_retyp_d split: s_heap_index.splits)

lemma (in mem_type) ptr_retyp_valid_footprint:
  "valid_footprint (ptr_retyp p d) (ptr_val (p::'a ptr)) (typ_uinfo_t TYPE('a))"
  apply(clarsimp simp: valid_footprint_def Let_def)
  apply(subst size_of_def [symmetric, where t="TYPE('a)"])
  apply clarsimp
  apply(subst ptr_retyp_footprint)
   apply(rule intvlI)
   apply(simp add: size_of_def)
  apply(subst ptr_retyp_footprint)
   apply(rule intvlI)
   apply(simp add: size_of_def)
  apply clarsimp
  by (metis (mono_tags) id_apply len_of_addr_card less_trans map_le_map_add max_size of_nat_eq_id 
   size_of_def take_bit_nat_eq_self unsigned_of_nat)

lemma (in mem_type) ptr_retyp_h_t_valid:
  "g p ⟹ ptr_retyp p d,g ⊨⇩t (p::'a ptr)"
  by (simp add: h_t_valid_def ptr_retyp_valid_footprint)

lemma (in mem_type) ptr_retyp_s_valid:
  "g p ⟹ lift_state (h,ptr_retyp p d),g ⊨⇩s (p::'a ptr)"
  by (simp add: s_valid_def proj_d_lift_state ptr_retyp_h_t_valid)

lemma (in mem_type) lt_size_of_unat_simps:
  "k < size_of TYPE('a) ⟹ unat ((of_nat k)::addr) < size_of TYPE('a)"
  by (metis le_def le_unat_uoi less_trans)

lemma (in mem_type) ptr_retyp_h_t_valid_same:
  "⟦ d,g ⊨⇩t (p::'a ptr); x ∈ {ptr_val p..+size_of TYPE('a)} ⟧ ⟹
       snd (ptr_retyp p d x) ⊆⇩m snd (d x)"
  apply(clarsimp simp: h_t_valid_def valid_footprint_def Let_def)
  apply(subst ptr_retyp_footprint)
   apply simp
  apply clarsimp
  apply(drule_tac x="unat (x - ptr_val p)" in spec)
  apply clarsimp
  apply(erule impE)
   apply(simp only: size_of_def [symmetric, where t="TYPE('a)"])
   apply(drule intvlD, clarsimp)
  using lt_size_of_unat_simps apply blast
  apply(fastforce intro: map_add_le_mapI)
  done

lemma (in mem_type) ptr_retyp_ptr_safe [simp]:
  "ptr_safe p (ptr_retyp (p::'a ptr) d)"
  by (force intro: h_t_valid_ptr_safe ptr_retyp_h_t_valid)


lemma (in mem_type) lift_state_ptr_retyp_restrict:
  "(lift_state (h, ptr_retyp p d) |` {(x,k). x ∈ {ptr_val p..+size_of TYPE('a)}}) =
      (lift_state (h,d) |` {(x,k). x ∈ {ptr_val p..+size_of TYPE('a)}}) ++
      lift_state (h, ptr_retyp (p::'a ptr) empty_htd)" (is "?x = ?y")
proof (rule ext, cases)
  fix x::"addr × s_heap_index"
  assume "fst x ∈ {ptr_val p..+size_of TYPE('a)}"
  thus "?x x = ?y x"
    apply(cases x)
    apply(clarsimp simp: lift_state_def map_add_def split: s_heap_index.splits)
    apply(safe; clarsimp)
        apply(drule ptr_retyp_d_empty, fast)
       apply(frule_tac d=d in ptr_retyp_d_empty, clarsimp simp: map_add_def)
       apply(clarsimp simp: restrict_map_def split: option.splits)
      apply(drule ptr_retyp_d_empty, fast)
     apply(drule ptr_retyp_d_empty, fast)
    apply(frule_tac d=d in ptr_retyp_d_empty, clarsimp simp: map_add_def)
    apply(clarsimp simp: restrict_map_def split: option.splits)
    done
next
  fix x::"addr × s_heap_index"
  assume "fst x ∉ {ptr_val p..+size_of TYPE('a)}"
  thus "?x x = ?y x"
    by (cases x) (auto simp: lift_state_def ptr_retyp_None map_add_def split: s_heap_index.splits)
qed

(* Old set of simps, not all that useful in general, below specialised
   simp sets are given *)
lemmas typ_simps = lift_t_heap_update lift_t_heap_update_same lift_heap_update
                   lift_t_h_t_valid h_t_valid_ptr_safe lift_t_ptr_safe lift_lift_t lift_t_lift
                   tag_disj_def typ_tag_le_def  typ_uinfo_t_def

declare field_desc_def [simp del]

lemma field_fd:
  "field_fd (t::'a::c_type itself) n =
     (case field_lookup (typ_info_t TYPE('a)) n 0 of
        None ⇒ field_desc (fst (the (None::('a xtyp_info × nat) option)))
      | Some x ⇒ field_desc (fst x))"
  by (auto simp: field_fd_def field_typ_def field_typ_untyped_def split: option.splits)

declare field_desc_def [simp add]

lemma (in mem_type) super_field_update_lookup:
  assumes "field_lookup (typ_info_t TYPE('b)) f 0 = Some (s,n)"
    and "typ_uinfo_t TYPE('a) = export_uinfo s"
    and "lift_t g h p = Some v'"
  shows "super_field_update_t (Ptr (&(p→f))) (v::'a) (lift_t g h::'b::mem_type typ_heap) =
           (lift_t g h)(p ↦ field_update (field_desc s) (to_bytes_p v) v')"
proof -
  note unsigned_of_nat [simp del]
  from assms have "size_of TYPE('b) < addr_card" by simp
  with assms have [simp]: "unat (of_nat n :: addr_bitsize word) = n"
    apply(subst unat_of_nat)
    apply(subst mod_less)
     apply(drule td_set_field_lookupD)+
     apply(drule td_set_offset_size)+
     apply(subst len_of_addr_card)
     apply(subst (asm) c_type_class.size_of_def [symmetric, where t="TYPE('b)"])+
     apply arith
    apply simp
    done
  from assms show ?thesis
    apply(clarsimp simp: super_field_update_t_def c_type_class.super_field_update_t_def)
    apply(rule ext)
    apply(clarsimp simp: field_lvalue_def c_type_class.field_lvalue_def split: option.splits)
    apply(safe; clarsimp?)
       apply(frule_tac v=v and v'=v' in update_field_update)
       apply clarsimp
        apply(thin_tac "P = update_ti_t x y z" for P x y z)
       apply(clarsimp simp: field_of_t_def c_type_class.field_of_t_def field_of_def c_type_class.typ_uinfo_t_def typ_uinfo_t_def)
       apply(frule_tac m=0 in field_names_SomeD2; clarsimp)
       apply(simp add: field_typ_def c_type_class.field_typ_def field_typ_untyped_def)
       apply(frule field_lookup_export_uinfo_Some)
       apply(frule_tac s=k in field_lookup_export_uinfo_Some)
       apply simp


         
       apply(drule (1) field_lookup_inject)
        apply(subst c_type_class.typ_uinfo_t_def [symmetric, where t="TYPE('b)"])
        apply simp
       apply simp
      apply(drule field_of_t_mem)+
      apply(cases h)
      apply(clarsimp simp: lift_t_if c_type_class.lift_t_if split: if_split_asm)
      apply(drule (1) h_t_valid_neq_disjoint)
        apply simp
       apply(fastforce simp: unat_eq_zero field_of_t_def c_type_class.field_of_t_def field_of_def dest!: td_set_size_lte)
      apply fast
     apply(clarsimp simp: field_of_t_def c_type_class.field_of_t_def field_of_def td_set_field_lookup)
     apply(fastforce simp: typ_uinfo_t_def c_type_class.typ_uinfo_t_def dest: field_lookup_export_uinfo_Some)
    apply(clarsimp simp: field_of_t_def c_type_class.field_of_t_def field_of_def td_set_field_lookup)
    apply(fastforce simp: typ_uinfo_t_def c_type_class.typ_uinfo_t_def dest: field_lookup_export_uinfo_Some)
    done
qed


(* Should use these in lift/heap_update reductions *)
lemmas typ_rewrs =
  lift_lift_t
  lift_t_heap_update
  lift_t_heap_update_same
  lift_t_heap_update [OF lift_t_h_t_valid]
  lift_t_heap_update_same [OF lift_t_h_t_valid]
  lift_lift_t [OF lift_t_h_t_valid]

end