Theory Padding_Equivalence

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Padding_Equivalence
  imports
    TypHeap
    SepCode
    CProof
    More_Lib
begin

lemma field_lookup_padding_field_name:
  fixes
  t:: "('a, 'b) typ_info " and
  st :: "('a, 'b) typ_info_struct" and
  ts :: "('a, 'b) typ_info_tuple list" and
  x :: "('a, 'b) typ_info_tuple"
shows
"field_lookup t [f] n = Some (s, m) ⟹ padding_field_name f ⟹ wf_padding t ⟹
   is_padding_tag s"
"field_lookup_struct st [f] n = Some (s, m) ⟹ padding_field_name f ⟹ wf_padding_struct st ⟹
   is_padding_tag s"
"field_lookup_list ts [f] n = Some (s, m) ⟹ padding_field_name f ⟹ wf_padding_list ts ⟹
   is_padding_tag s"
"field_lookup_tuple x [f] n = Some (s, m) ⟹ padding_field_name f ⟹ wf_padding_tuple x ⟹
   is_padding_tag s"
  by (induct t and st and ts and x arbitrary: n m and n m and n m and n m)
    (auto split: if_split_asm option.splits)

lemma field_lookup_access_ti_take_drop':
  fixes t::"('a, 'b) typ_info"
  and st::"('a, 'b) typ_info_struct"
  and ts::"('a, 'b) typ_info_tuple list"
  and x::"('a, 'b) typ_info_tuple"
shows
  "field_lookup t f m = Some (s, m + n) ⟹ wf_fd t ⟹ wf_desc t ⟹ wf_size_desc t ⟹ length bs = size_td t ⟹
     access_ti s v (take (size_td s) (drop n bs)) =
       (take (size_td s) (drop n (access_ti t v bs)))"

  "field_lookup_struct st f m = Some (s, m + n) ⟹ wf_fd_struct st ⟹ wf_desc_struct st ⟹ wf_size_desc_struct st ⟹ length bs = size_td_struct st  ⟹
     access_ti s v (take (size_td s) (drop n bs)) =
       (take (size_td s) (drop n (access_ti_struct st v bs)))"

  "field_lookup_list ts f m = Some (s, m + n) ⟹ wf_fd_list ts ⟹ wf_desc_list ts ⟹ wf_size_desc_list ts ⟹ length bs = size_td_list ts ⟹
     access_ti s v (take (size_td s) (drop n bs)) =
       (take (size_td s) (drop n (access_ti_list ts v bs)))"

  "field_lookup_tuple x f m = Some (s, m + n) ⟹ wf_fd_tuple x ⟹ wf_desc_tuple x ⟹ wf_size_desc_tuple x ⟹ length bs = size_td_tuple x ⟹
     access_ti s v (take (size_td s) (drop n bs)) =
       (take (size_td s) (drop n (access_ti_tuple x v bs)))"
proof (induct t and st and ts and x arbitrary: f m n s bs v and f m n s bs v and f m n s bs v and f m n s bs v)
  case (TypDesc algn st nm)
  then show ?case 
    by (auto split: if_split_asm)
       (metis TypDesc.prems(2) TypDesc.prems(5) access_ti.simps le_refl length_fa_ti take_all)
next
  term TypDesc
  case (TypScalar algn st d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  obtain d nm y where x: "x = DTuple d nm y" by (cases x) auto
  from Cons_typ_desc.prems obtain
    lbs: "length bs = size_td_tuple x + size_td_list fs" and
    wf_fd_x: "wf_fd_tuple (DTuple d nm y)" and
    wf_desc_x: "wf_desc_tuple (DTuple d nm y)" and
    wf_fd_fs: "wf_fd_list fs" and
    wf_size_desc_x: "wf_size_desc_tuple (DTuple d nm y)" and
    wf_size_desc_fs: "wf_size_desc_list fs" and
    nm_notin:  "nm ∉ dt_snd ` set fs" and
    wf_desc_fs: "wf_desc_list fs" and
    commutes: "fu_commutes (update_ti_t d) (update_ti_list_t fs)"
    by (auto simp add: x)

  from lbs
  have lbs_drop: "length (drop (size_td_tuple x) bs) = size_td_list fs"
    by simp

  from lbs
  have lbs_take: "length (take (size_td_tuple x) bs) = size_td_tuple (DTuple d nm y)"
    by (simp add: x)

  from lbs wf_fd_x
  have eq1: "length (access_ti d v (take (size_td d) bs)) = size_td d"
    by (metis lbs_take length_fa_ti size_td_tuple.simps wf_fd_tuple.simps x)

  from Cons_typ_desc.prems obtain f1 fxs
    where f: "f = f1#fxs"
    by (cases f) auto

  show ?case
  proof (cases "f1 = nm")
    case True
    show ?thesis
    proof (cases "field_lookup d fxs m")
      case None
      from Cons_typ_desc.prems field_lookup_list_None [OF nm_notin]
      have False
        by (simp add: True None f x)
      thus ?thesis by simp
    next
      case (Some r)
      from Cons_typ_desc.prems have r: "r = (s, m + n)"
        by (simp add: x True Some f)
      hence fl: "field_lookup_tuple (DTuple d nm y) f m = Some (s, m + n)"
        by  (simp add: f True Some r)

      from td_set_wf_size_desc(4)[OF wf_size_desc_x td_set_tuple_field_lookup_tupleD, OF fl]
      have "wf_size_desc s" .
      from wf_size_desc_gt(1)[OF this]
      have "0 < size_td s" .


      with td_set_tuple_offset_size_m [OF td_set_tuple_field_lookup_tupleD, OF fl]
      have n_le: "n < size_td d"
        by auto

      have bound: "size_td s + (m + n - m) ≤ size_td_tuple (DTuple d nm y)" by fact
      from bound
      have take_eq: "(take (size_td s) (drop n (take (size_td d) bs))) =
         (take (size_td s) (drop n bs))"
        by (simp add: take_drop)

      from Cons_typ_desc.hyps(1)[simplified x, OF fl wf_fd_x wf_desc_x wf_size_desc_x lbs_take, of v] lbs bound
      show ?thesis by (simp add: x True Some r take_eq eq1)
    qed
  next
    case False
    with Cons_typ_desc.prems
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, m + n)"
      by (clarsimp simp add: x f False)
    hence n_bound: "size_td d ≤ n"
      by (meson field_lookup_offset_le(3) nat_add_left_cancel_le)

    from fl
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, (m + size_td d) + (n - size_td d))"
      by (metis Nat.diff_cancel field_lookup_list_offset2 field_lookup_list_offsetD)
    from n_bound
    have take_eq: "(take (size_td s) (drop (n - size_td d + size_td d) bs)) =
            (take (size_td s) (drop n bs))"
      by simp


    from Cons_typ_desc.hyps(2) [OF fl wf_fd_fs wf_desc_fs wf_size_desc_fs lbs_drop, of v]
      False n_bound
    show ?thesis
      by (simp add: x f eq1)
  qed
next
  case (DTuple_typ_desc d nm y)
  then show ?case apply (cases f) by (auto split: if_split_asm)
qed

lemma field_lookup_access_ti_take_drop:
  "field_lookup t f 0 = Some (s, n) ⟹ wf_fd t ⟹ wf_desc t ⟹ wf_size_desc t ⟹ length bs = size_td t ⟹
     access_ti s v (take (size_td s) (drop n bs)) =
       (take (size_td s) (drop n (access_ti t v bs)))"
  using field_lookup_access_ti_take_drop' [where m=0] by auto

lemma field_lookup_nth_focus':
  fixes t::"('a, 'b) typ_info"
  and st::"('a, 'b) typ_info_struct"
  and ts::"('a, 'b) typ_info_tuple list"
  and x::"('a, 'b) typ_info_tuple"
shows
"⟦field_lookup t f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td t;
  wf_fd t; wf_desc t; wf_size_desc t⟧ ⟹
   access_ti t v bs ! i = access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"

"⟦field_lookup_struct st f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_struct st;
  wf_fd_struct st; wf_desc_struct st; wf_size_desc_struct st⟧ ⟹
   access_ti_struct st v bs ! i = access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"

"⟦field_lookup_list ts f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_list ts;
  wf_fd_list ts; wf_desc_list ts; wf_size_desc_list ts⟧ ⟹
   access_ti_list ts v bs ! i = access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"

"⟦field_lookup_tuple x f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_tuple x;
  wf_fd_tuple x; wf_desc_tuple x; wf_size_desc_tuple x⟧ ⟹
   access_ti_tuple x v bs ! i = access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"
proof (induct t and st and ts and x arbitrary: f m n i s bs v and f m n i s bs v and f m n i s bs v and f m n i s bs v)
case (TypDesc algn st nm)
  then show ?case by (auto split: if_split_asm)
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  obtain d nm y where x: "x = DTuple d nm y" by (cases x) auto
  from Cons_typ_desc.prems obtain
    lbs: "length bs = size_td_tuple x + size_td_list fs" and
    wf_fd_x: "wf_fd_tuple (DTuple d nm y)" and
    wf_desc_x: "wf_desc_tuple (DTuple d nm y)" and
    wf_fd_fs: "wf_fd_list fs" and
    wf_size_desc_x: "wf_size_desc_tuple (DTuple d nm y)" and
    wf_size_desc_fs: "wf_size_desc_list fs" and
    nm_notin:  "nm ∉ dt_snd ` set fs" and
    wf_desc_fs: "wf_desc_list fs" and
    i_lower: "n ≤ i" and
    i_upper: "i < n + size_td s"
    by (auto simp add: x)

  from lbs
  have lbs_drop: "length (drop (size_td_tuple x) bs) = size_td_list fs"
    by simp

  from lbs
  have lbs_take: "length (take (size_td_tuple x) bs) = size_td_tuple (DTuple d nm y)"
    by (simp add: x)

  from lbs wf_fd_x
  have eq1: "length (access_ti d v (take (size_td d) bs)) = size_td d"
    by (metis lbs_take length_fa_ti size_td_tuple.simps wf_fd_tuple.simps x)

  from Cons_typ_desc.prems obtain f1 fxs
    where f: "f = f1#fxs"
    by (cases f) auto

  thm Cons_typ_desc.hyps [simplified x]

  show ?case
  proof (cases "f1 = nm")
    case True
    show ?thesis
    proof (cases "field_lookup d fxs m")
      case None
      from Cons_typ_desc.prems field_lookup_list_None [OF nm_notin]
      have False
        by (simp add: True None f x)
      thus ?thesis by simp
    next
      case (Some r)
      from Cons_typ_desc.prems have r: "r = (s, m + n)"
        by (simp add: x True Some f)
      hence fl: "field_lookup_tuple (DTuple d nm y) f m = Some (s, m + n)"
        by  (simp add: f True Some r)
      from td_set_wf_size_desc(4)[OF wf_size_desc_x td_set_tuple_field_lookup_tupleD, OF fl]
      have "wf_size_desc s" .
      from wf_size_desc_gt(1)[OF this]
      have "0 < size_td s" .


      with td_set_tuple_offset_size_m [OF td_set_tuple_field_lookup_tupleD, OF fl]
      have n_le: "n < size_td d"
        by auto

      have i_in_d: "i < size_td d"
        using ‹size_td s + (m + n - m) ≤ size_td_tuple (DTuple d nm y)› i_upper by auto
      have bound: "size_td s + (m + n - m) ≤ size_td_tuple (DTuple d nm y)" by fact
      from bound
      have take_eq: "(take (size_td s) (drop n (take (size_td d) bs))) =
         (take (size_td s) (drop n bs))"
        by (simp add: take_drop)
      from  Cons_typ_desc.hyps(1)[simplified x, OF fl i_lower i_upper lbs_take wf_fd_x wf_desc_x wf_size_desc_x, of v] lbs bound
      show ?thesis
        by (simp add: x True Some r take_eq eq1 nth_append i_in_d)
    qed
  next
    case False
    with Cons_typ_desc.prems
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, m + n)"
      by (clarsimp simp add: x f False)
    hence n_bound: "size_td d ≤ n"
      by (meson field_lookup_offset_le(3) nat_add_left_cancel_le)

    from fl
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, (m + size_td d) + (n - size_td d))"
      by (metis Nat.diff_cancel field_lookup_list_offset2 field_lookup_list_offsetD)
    from n_bound
    have take_eq: "(take (size_td s) (drop (n - size_td d + size_td d) bs)) =
            (take (size_td s) (drop n bs))"
      by simp

    have i_lower': "n - size_td d ≤ i - size_td d"
      using diff_le_mono i_lower by blast

    have i_upper': "i - size_td d < n - size_td d + size_td s"
      using i_lower i_upper by linarith

    have i_notin_d: "¬ i < size_td d"
      by (meson i_lower leD less_le_trans n_bound)

    from Cons_typ_desc.hyps(2) [OF fl i_lower' i_upper' lbs_drop wf_fd_fs wf_desc_fs wf_size_desc_fs, where v=v]
      False n_bound
    show ?thesis
      by (simp add: x f eq1 nth_append i_notin_d)
  qed
next
  case (DTuple_typ_desc d nm y)
then show ?case apply (cases f) by (auto split: if_split_asm)
qed

lemma field_lookup_nth_focus:
 "⟦field_lookup t f 0 = Some (s, n); n ≤ i; i < n + size_td s; length bs = size_td t;
  wf_fd t; wf_desc t; wf_size_desc t⟧ ⟹
   access_ti t v bs ! i = access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"
  using field_lookup_nth_focus' [where m=0] by auto


lemma field_lookup_nth_update_focus':
  fixes t::"('a, 'b) typ_info"
  and st::"('a, 'b) typ_info_struct"
  and ts::"('a, 'b) typ_info_tuple list"
  and x::"('a, 'b) typ_info_tuple"
shows
"⟦field_lookup t f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td t;
  wf_fd t; wf_desc t; wf_size_desc t⟧ ⟹
   access_ti t v (bs[i := b]) =
    super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
     (access_ti t v bs) n"

"⟦field_lookup_struct st f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_struct st;
  wf_fd_struct st; wf_desc_struct st; wf_size_desc_struct st⟧ ⟹
   access_ti_struct st v (bs[i := b]) =
     super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
      (access_ti_struct st v bs) n"

"⟦field_lookup_list ts f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_list ts;
  wf_fd_list ts; wf_desc_list ts; wf_size_desc_list ts⟧ ⟹
   access_ti_list ts v (bs[i := b]) =
     super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
       (access_ti_list ts v bs) n"

"⟦field_lookup_tuple x f m = Some (s, m + n); n ≤ i; i < n + size_td s; length bs = size_td_tuple x;
  wf_fd_tuple x; wf_desc_tuple x; wf_size_desc_tuple x⟧ ⟹
   access_ti_tuple x v (bs[i := b]) =
     super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
       (access_ti_tuple x v bs) n"
proof (induct t and st and ts and x arbitrary: f m n i s bs v and f m n i s bs v and f m n i s bs v and f m n i s bs v)
case (TypDesc algn st nm)
  then show ?case
    by (auto split: if_split_asm simp add: super_update_bs_def)
       (metis TypDesc.prems(4) TypDesc.prems(5) access_ti.simps le_refl length_fa_ti length_list_update)
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  obtain d nm y where x: "x = DTuple d nm y" by (cases x) auto
  from Cons_typ_desc.prems obtain
    lbs: "length bs = size_td_tuple x + size_td_list fs" and
    wf_fd_x: "wf_fd_tuple (DTuple d nm y)" and
    wf_desc_x: "wf_desc_tuple (DTuple d nm y)" and
    wf_fd_fs: "wf_fd_list fs" and
    wf_size_desc_x: "wf_size_desc_tuple (DTuple d nm y)" and
    wf_size_desc_fs: "wf_size_desc_list fs" and
    nm_notin:  "nm ∉ dt_snd ` set fs" and
    wf_desc_fs: "wf_desc_list fs" and
    i_lower: "n ≤ i" and
    i_upper: "i < n + size_td s"
    by (auto simp add: x)

  from lbs
  have lbs_drop: "length (drop (size_td_tuple x) bs) = size_td_list fs"
    by simp

  from lbs
  have lbs_take: "length (take (size_td_tuple x) bs) = size_td_tuple (DTuple d nm y)"
    by (simp add: x)

  from lbs wf_fd_x
  have eq1: "length (access_ti d v (take (size_td d) bs)) = size_td d"
    by (metis lbs_take length_fa_ti size_td_tuple.simps wf_fd_tuple.simps x)

  from Cons_typ_desc.prems obtain f1 fxs
    where f: "f = f1#fxs"
    by (cases f) auto

  thm Cons_typ_desc.hyps [simplified x]

  show ?case
  proof (cases "f1 = nm")
    case True
    show ?thesis
    proof (cases "field_lookup d fxs m")
      case None
      from Cons_typ_desc.prems field_lookup_list_None [OF nm_notin]
      have False
        by (simp add: True None f x)
      thus ?thesis by simp
    next
      case (Some r)
      from Cons_typ_desc.prems have r: "r = (s, m + n)"
        by (simp add: x True Some f)
      hence fl: "field_lookup_tuple (DTuple d nm y) f m = Some (s, m + n)"
        by  (simp add: f True Some r)
      from td_set_wf_size_desc(4)[OF wf_size_desc_x td_set_tuple_field_lookup_tupleD, OF fl]
      have "wf_size_desc s" .
      from wf_size_desc_gt(1)[OF this]
      have "0 < size_td s" .


      with td_set_tuple_offset_size_m [OF td_set_tuple_field_lookup_tupleD, OF fl]
      have n_le: "n < size_td d"
        by auto

      have i_in_d: "i < size_td d"
        using ‹size_td s + (m + n - m) ≤ size_td_tuple (DTuple d nm y)› i_upper by auto
      have bound: "size_td s + (m + n - m) ≤ size_td_tuple (DTuple d nm y)" by fact
      from bound
      have take_eq: "(take (size_td s) (drop n (take (size_td d) bs))) =
         (take (size_td s) (drop n bs))"
        by (simp add: take_drop)
      from bound
      have take_upd_eq: " ((take (size_td d) bs)[i := b]) = (take (size_td d) (bs[i := b]))"
        by (simp add: take_update_swap)

      have take_eq1: "take (size_td s) (drop n (take (size_td d) bs)) = take (size_td s) (drop n bs)"
        using take_eq by blast

      have l_take_s: "length (take (size_td s) (drop n bs)) = size_td s"
        using bound lbs_take by auto

      have sz_s: "size_td s ≤ length bs - n"
        using l_take_s by auto

      from fl
      have fd_cons_s: "fd_cons s"
        using wf_fd_consD wf_fd_field_lookup(4) wf_fd_x by blast
      have l_acc_s: "length (access_ti s v ((take (size_td s) (drop n bs))[i - n := b])) = size_td s"
        by (simp add: fd_cons_length [OF fd_cons_s] sz_s eq1)

      have take_eq2: "(take (size_td s) (drop n (take (size_td d) bs)))[i - n := b] = (take (size_td s) (drop n bs))[i - n := b]"
        using take_eq1 by presburger

      note hyp =  Cons_typ_desc.hyps(1)[simplified x, OF fl i_lower i_upper lbs_take wf_fd_x wf_desc_x wf_size_desc_x, of v,
          simplified, simplified x, simplified, simplified take_upd_eq]
      from lbs bound
      show ?thesis
        apply (simp add: x True Some r take_eq take_upd_eq eq1 list_update_append i_in_d)
        apply (simp add: hyp)
        apply (subst super_update_bs_append1)
         apply (simp add: l_acc_s eq1)
        apply (simp add: take_eq2)
        done
    qed
  next
    case False
    with Cons_typ_desc.prems
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, m + n)"
      by (clarsimp simp add: x f False)
    hence n_bound: "size_td d ≤ n"
      by (meson field_lookup_offset_le(3) nat_add_left_cancel_le)

    from fl
    have fl: "field_lookup_list fs (f1 # fxs) (m + size_td d) = Some (s, (m + size_td d) + (n - size_td d))"
      by (metis Nat.diff_cancel field_lookup_list_offset2 field_lookup_list_offsetD)
    from n_bound
    have take_eq: "(take (size_td s) (drop (n - size_td d + size_td d) bs)) =
            (take (size_td s) (drop n bs))"
      by simp

    have i_lower': "n - size_td d ≤ i - size_td d"
      using diff_le_mono i_lower by blast

    have i_upper': "i - size_td d < n - size_td d + size_td s"
      using i_lower i_upper by linarith

    have i_notin_d: "¬ i < size_td d"
      by (meson i_lower leD less_le_trans n_bound)

    from i_notin_d have take_d_eq: "take (size_td d) (bs[i := b]) = take (size_td d) bs"
      by simp
    have drop_shift: "(drop (size_td d) bs)[i - size_td d := b] = drop (size_td d) (bs[i := b])"
      by (metis drop_update_swap i_notin_d le_def)

    note hyp = Cons_typ_desc.hyps(2) [OF fl i_lower' i_upper' lbs_drop wf_fd_fs wf_desc_fs wf_size_desc_fs, where v=v,
        simplified x, simplified, simplified drop_shift]
    from  False n_bound
    show ?thesis
      apply (simp add: x f eq1 nth_append i_notin_d)
      apply (subst super_update_bs_append2)
       apply (simp add: eq1)
      apply (simp add: take_d_eq add: eq1)
      apply (simp add: hyp)
      done
  qed
next
  case (DTuple_typ_desc d nm y)
then show ?case apply (cases f) by (auto split: if_split_asm)
qed

lemma field_lookup_nth_update_focus:
shows
"⟦field_lookup t f 0 = Some (s, n); n ≤ i; i < n + size_td s; length bs = size_td t;
  wf_fd t; wf_desc t; wf_size_desc t⟧ ⟹
   access_ti t v (bs[i := b]) =
    super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
     (access_ti t v bs) n"
  using field_lookup_nth_update_focus' [where m=0] by auto


context mem_type
begin
lemma mem_type_field_lookup_access_ti_take_drop:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lbs : "length bs = size_of TYPE('a)"
  shows "access_ti s v (take (size_td s) (drop n bs)) =
           take (size_td s) (drop n (access_ti (typ_info_t TYPE('a)) v bs))"
proof -
  have wf_fd: "wf_fd (typ_info_t TYPE('a))"
    by (simp add: wf_fdp_fdD wf_lf_fdp)
  have wf_desc: "wf_desc (typ_info_t TYPE('a))" by simp
  have wf_size: "wf_size_desc (typ_info_t TYPE('a))" by simp
  from field_lookup_access_ti_take_drop [OF fl wf_fd wf_desc wf_size lbs [simplified size_of_def]]
  show ?thesis .
qed

lemma mem_type_update_ti_super_update_bs:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lbs: "length bs = size_of TYPE('a)"
  assumes lv: "length v = size_td s"
  shows "update_ti s v (update_ti (typ_info_t TYPE('a)) bs w) =
           update_ti (typ_info_t TYPE('a)) (super_update_bs v bs n) w"
proof -
  have wf_fd: "wf_fd (typ_info_t TYPE('a))"
    by (simp add: wf_fdp_fdD wf_lf_fdp)
  have lsuper: "length (super_update_bs v bs n) = size_td (typ_info_t TYPE('a))"
    by (metis add.commute field_lookup_offset_size' fl lbs length_super_update_bs local.size_of_def lv)

  from fi_fu_consistentD [OF fl wf_fd lbs [simplified size_of_def] lv, of w] lbs
  show ?thesis
    by (simp add: update_ti_t_def lsuper lv size_of_def)
qed


lemma mem_type_update_ti_from_bytes_super_update_bs:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lbs: "length bs = size_of TYPE('a)"
  assumes lv: "length v = size_td s"
  shows "update_ti s v (from_bytes bs) = update_ti (typ_info_t TYPE('a)) (super_update_bs v bs n) undefined"
proof -
  from mem_type_update_ti_super_update_bs [OF fl lbs lv, of undefined]
  show ?thesis
    by (simp add: from_bytes_def update_ti_t_def lbs size_of_def)
qed

lemma mem_type_field_lookup_nth_focus:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes i_lower: "n ≤ i"
  assumes i_upper: "i < n + size_td s"
  assumes lbs : "length bs = size_of TYPE('a)"
  shows "access_ti (typ_info_t TYPE('a)) v bs ! i =
           access_ti s v (take (size_td s) (drop n bs)) ! (i - n)"
proof -
  have wf_fd: "wf_fd (typ_info_t TYPE('a))"
    by (simp add: wf_fdp_fdD wf_lf_fdp)
  have wf_desc: "wf_desc (typ_info_t TYPE('a))" by simp
  have wf_size: "wf_size_desc (typ_info_t TYPE('a))" by simp
  from field_lookup_nth_focus [OF fl i_lower i_upper lbs [simplified size_of_def] wf_fd wf_desc wf_size]
  show ?thesis .
qed

lemma mem_type_field_lookup_nth_update_focus:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes i_lower: "n ≤ i"
  assumes i_upper: "i < n + size_td s"
  assumes lbs : "length bs = size_of TYPE('a)"
  shows
"access_ti (typ_info_t TYPE('a)) v (bs[i := b]) =
    super_update_bs (access_ti s v ((take (size_td s) (drop n bs))[i - n := b]))
     (access_ti (typ_info_t TYPE('a)) v bs) n"
proof -
  have wf_fd: "wf_fd (typ_info_t TYPE('a))"
    by (simp add: wf_fdp_fdD wf_lf_fdp)
  have wf_desc: "wf_desc (typ_info_t TYPE('a))" by simp
  have wf_size: "wf_size_desc (typ_info_t TYPE('a))" by simp
  from field_lookup_nth_update_focus [OF fl i_lower i_upper lbs [simplified size_of_def] wf_fd wf_desc wf_size]
  show ?thesis .
qed
end



ML ‹@{term  "xs[i := v]"}›


lemma nth_take_drop_index_shift:
"n ≤ i ⟹ i < m + n ⟹ m + n ≤ length xs ⟹ take m (drop n xs) ! (i - n) = xs ! i"
proof (induct xs arbitrary: n i m)
  case Nil
  then show ?case by simp
next
  case (Cons x1 xs)
  then show ?case by auto
qed

lemma super_update_bs_update_index_shift: "n ≤ i ⟹ i - n < length bs ⟹ n + length bs ≤ length xbs ⟹
(super_update_bs bs xbs n)[i := b] = super_update_bs (bs[i - n := b]) xbs n"
  apply (simp add: super_update_bs_def)
  apply (simp add: list_update_append)
  done

lemma super_update_bs_nth_shift:
 "n ≤ i ⟹ i - n < length bs ⟹ n + length bs ≤ length xbs ⟹ super_update_bs bs xbs n ! i = bs ! (i - n)"
  apply (simp add: super_update_bs_def)
  apply (simp add: nth_append)
  done

lemma (in mem_type) field_lookup_is_padding_byte_outer_to_inner:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  assumes is_padding: "padding_base.is_padding_byte (access_ti (typ_info_t (TYPE('a)))) (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
  shows "padding_base.is_padding_byte (access_ti s) (update_ti s) (size_td s) (x - n)"
proof (rule padding_base.is_padding_byteI)
  from lower_bound_x upper_bound_x show "x - n < size_td s" by simp
next
  fix v::'a and bs::"byte list"
  assume "x - n < size_td s"
  assume lbs: "length bs = size_td s"
  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (simp add: field_lookup_offset_size' size_of_def)

  obtain pfx sfx xbs where
    xbs: "xbs = pfx @ bs @ sfx" and
    lpfx: "length pfx = n" and
    lsfx: "length sfx = size_of TYPE('a) - n - size_td s"
    by (metis Ex_list_of_length)
  with sz have lxbs: "length xbs = size_of TYPE('a)"
    by (metis add_leD2 add_le_imp_le_diff lbs le_add_diff_inverse length_append)
  from xbs lpfx lsfx xbs lbs have bs: "(take (size_td s) (drop n xbs)) = bs"
    by simp

  have bound: "x - n < size_td s" by fact

  have lacc: "length (access_ti (typ_info_t TYPE('a)) v xbs) = size_of TYPE('a)"
    by (simp add: length_fa_ti lxbs size_of_def)

  from mem_type_field_lookup_access_ti_take_drop [OF fl lxbs, simplified bs, of v]
  have acc_conv: "access_ti s v bs =
         take (size_td s) (drop n (access_ti (typ_info_t TYPE('a)) v xbs))" .
  from padding_base.is_padding_byte_acc_eq [OF is_padding, of xbs v] lxbs
  have "access_ti (typ_info_t TYPE('a)) v xbs ! x = xbs ! x"
    by (simp add: size_of_def)
  moreover have "xbs ! x = bs ! (x - n)"
    using xbs lpfx lsfx lxbs bound
    apply (simp add: xbs)
    by (metis bs drop_append_miracle le_def lower_bound_x nth_append nth_take xbs)
  moreover have "take (size_td s) (drop n (access_ti (typ_info_t TYPE('a)) v xbs)) ! (x - n) =
    access_ti (typ_info_t TYPE('a)) v xbs ! x"
    using lacc lxbs bound lower_bound_x upper_bound_x
    by (metis less_diff_conv2 nth_take_drop_index_shift sz)

  ultimately show "access_ti s v bs ! (x - n) = bs ! (x - n)"
    by (simp add: acc_conv)
next
  fix v::'a and bs::"byte list" and b::byte
  assume "x - n < size_td s"
  assume lbs: "length bs = size_td s"

  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (simp add: local.field_lookup_offset_size local.size_of_def)

  obtain pfx sfx xbs where
    xbs: "xbs = pfx @ bs @ sfx" and
    lpfx: "length pfx = n" and
    lsfx: "length sfx = size_of TYPE('a) - n - size_td s"
    by (metis Ex_list_of_length)

  with sz have lxbs: "length xbs = size_of TYPE('a)"
    by (metis add_leD2 add_le_imp_le_diff lbs le_add_diff_inverse length_append)
  from xbs lpfx lsfx xbs lbs have bs: "(take (size_td s) (drop n xbs)) = bs"
    by simp

  have v_upd_conv: "(update_ti (typ_info_t TYPE('a)) (to_bytes v xbs) v) = v"
    by (simp add: fu_fa length_fa_ti local.size_of_def local.to_bytes_def lxbs update_ti_update_ti_t)

   have lxto: "length (to_bytes v xbs) = size_of TYPE('a)"
     by (simp add: length_fa_ti lxbs size_of_def to_bytes_def)

  from lxto lbs
  have lsuper: "length (super_update_bs bs (to_bytes v xbs) n) = size_of TYPE('a)"
    using sz by auto

  have bound: "x - n < size_td s" by fact

  have xbs_super: "xbs = super_update_bs bs xbs n"
    by (simp add: lpfx super_update_bs_def xbs)
  from mem_type_update_ti_super_update_bs [OF fl lxto lbs, of v, simplified v_upd_conv]
  have upd_eq1:
    "update_ti s bs v =
       update_ti (typ_info_t TYPE('a)) (super_update_bs bs (to_bytes v xbs) n) v" .

  have lbs': "length (bs[x - n := b]) = size_td s"
    using lbs by auto

  from mem_type_update_ti_super_update_bs [OF fl lxto lbs', of v, simplified v_upd_conv]
  have upd_eq2:
    "update_ti s (bs[x - n := b]) v =
       update_ti (typ_info_t TYPE('a)) (super_update_bs (bs[x - n := b]) (to_bytes v xbs) n) v" .

  from lxto lxbs lbs lower_bound_x upper_bound_x bound sz
  have super_eq: "(super_update_bs bs (to_bytes v xbs) n)[x := b] = super_update_bs (bs[x - n := b]) (to_bytes v xbs) n"
    by (simp add: super_update_bs_update_index_shift)

  from padding_base.is_padding_byte_upd_eq [OF is_padding, of "(super_update_bs bs (to_bytes v xbs) n)" v b] lsuper
  have upd_pad: "update_ti (typ_info_t TYPE('a)) (super_update_bs bs (to_bytes v xbs) n) v =
         update_ti (typ_info_t TYPE('a)) ((super_update_bs bs (to_bytes v xbs) n)[x := b]) v"
    by (simp add: size_of_def)
  show "update_ti s bs v = update_ti s (bs[x - n := b]) v"
    apply (simp add: upd_eq1)
    apply (simp add: upd_pad)
    apply (simp add: upd_eq2)
    apply (simp add: super_eq)
    done
qed

lemma (in mem_type) field_lookup_is_padding_byte_inner_to_outer:
  assumes fl: "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  assumes is_padding: "padding_base.is_padding_byte (access_ti s) (update_ti s) (size_td s) (x - n)"
  shows "padding_base.is_padding_byte (access_ti (typ_info_t (TYPE('a)))) (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
proof (rule padding_base.is_padding_byteI)
  from lower_bound_x upper_bound_x fl
  show "x < size_td (typ_info_t TYPE('a))"
    using field_lookup_offset_size' by fastforce
next
  fix v::'a and bs::"byte list"
  assume sz: "x < size_td (typ_info_t TYPE('a))"
  assume lbs: "length bs = size_td (typ_info_t TYPE('a))"
  from mem_type_field_lookup_nth_focus [OF fl lower_bound_x upper_bound_x, simplified size_of_def, OF lbs]
  have eq1:
    "access_ti (typ_info_t TYPE('a)) v bs ! x =
       access_ti s v (take (size_td s) (drop n bs)) ! (x - n)" .
  from lbs fl
  have l_take_drop: "length (take (size_td s) (drop n bs)) = size_td s"
    using field_lookup_offset_size' by fastforce

  from padding_base.is_padding_byte_acc_eq [OF is_padding l_take_drop, of v]
  have eq2:
    "access_ti s v (take (size_td s) (drop n bs)) ! (x - n) =
      take (size_td s) (drop n bs) ! (x - n)" .
  have eq3:
    "take (size_td s) (drop n bs) ! (x - n) = bs ! x"
    by (metis add.commute field_lookup_offset_size' fl lbs lower_bound_x nth_take_drop_index_shift upper_bound_x)

  show "access_ti (typ_info_t TYPE('a)) v bs ! x = bs ! x"
    apply (simp add: eq1)
    apply (simp add: eq2)
    apply (simp add: eq3)
    done
next
  fix v::'a and bs::"byte list" and b::byte
  assume sz: "x < size_td (typ_info_t TYPE('a))"
  assume lbs: "length bs = size_td (typ_info_t TYPE('a))"

  have v_upd_conv: "(update_ti (typ_info_t TYPE('a)) (to_bytes v bs) v) = v"
    by (simp add: fu_fa lbs length_fa_ti to_bytes_def update_ti_update_ti_t)

  have lto: "length (to_bytes v bs) = size_td (typ_info_t TYPE('a))"
    by (simp add: lbs length_fa_ti to_bytes_def)

  note upd_focus = mem_type_update_ti_super_update_bs [OF fl, simplified size_of_def, OF lto, where w=v, simplified v_upd_conv]

  from lbs lower_bound_x upper_bound_x sz
  have lbs1: "length (take (size_td s) (drop n bs)) = size_td s"
    by (metis add_le_imp_le_diff field_lookup_offset_size' fl length_drop length_take min.absorb2)

  from lbs lower_bound_x upper_bound_x
  have bs_upd_eq: "(take (size_td s) (drop n bs))[x - n := b] = take (size_td s) (drop n (bs[x := b]))"
    by (metis drop_update_swap take_update_swap)

  from lbs lbs1 lower_bound_x upper_bound_x
  have lbs2: "length (take (size_td s) (drop n (bs[x := b]))) = size_td s"
    by (metis bs_upd_eq length_list_update)


  from lbs lbs1
  have bs_super_conv: "(super_update_bs (take (size_td s) (drop n bs)) bs n) = bs"
    by (metis append_take_drop_id super_update_bs_def take_drop_append)

  from lbs lbs1 lower_bound_x upper_bound_x
  have bs_upd_super_conv: "(super_update_bs (take (size_td s) (drop n (bs[x := b]))) bs n) = bs[x := b]"
    by (metis add.commute bs_super_conv bs_upd_eq field_lookup_offset_size' fl
        nat_diff_less super_update_bs_update_index_shift)

  from mem_type_update_ti_super_update_bs [OF fl, simplified size_of_def, OF lbs lbs1, simplified bs_super_conv, where w=v]
  have eq1:
    "update_ti (typ_info_t TYPE('a)) bs v =
       update_ti s (take (size_td s) (drop n bs)) (update_ti (typ_info_t TYPE('a)) bs v)" by simp

  from mem_type_update_ti_super_update_bs [OF fl, simplified size_of_def, OF lbs lbs2, simplified bs_upd_super_conv, where w=v]
  have eq2:
    "update_ti s (take (size_td s) (drop n (bs[x := b])))
       (update_ti (typ_info_t TYPE('a)) bs v) =
     update_ti (typ_info_t TYPE('a)) (bs[x := b]) v" .

  thm upd_focus [OF lbs1]
  note pad_eq= padding_base.is_padding_byte_upd_eq [OF is_padding, OF lbs1, where b=b]
  show "update_ti (typ_info_t TYPE('a)) bs v =
          update_ti (typ_info_t TYPE('a)) (bs[x := b]) v"
    apply (subst eq1)
    apply (simp add: pad_eq)
    apply (simp add: bs_upd_eq)
    apply (simp add: eq2)
    done
qed


lemma (in mem_type) field_lookup_is_padding_byte:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  shows
   "padding_base.is_padding_byte (access_ti s) (update_ti s) (size_td s) (x - n) ⟷
    padding_base.is_padding_byte
     (access_ti (typ_info_t (TYPE('a)))) (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
  using field_lookup_is_padding_byte_outer_to_inner [OF fl lower_bound_x upper_bound_x]
    field_lookup_is_padding_byte_inner_to_outer [OF fl lower_bound_x upper_bound_x]
  by blast

lemma (in mem_type) field_lookup_is_value_byte_outer_to_inner:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  assumes is_value: "padding_base.is_value_byte (access_ti (typ_info_t (TYPE('a)))) (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
  shows "padding_base.is_value_byte (access_ti s) (update_ti s) (size_td s) (x - n)"
proof (rule padding_base.is_value_byteI)
  from lower_bound_x upper_bound_x show "x - n < size_td s" by simp
next
  fix v::'a and bs::"byte list" and bs'::"byte list"
  assume "x - n < size_td s"
  assume lbs: "length bs = size_td s"
  assume lbs': "length bs' = size_td s"
  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (metis (no_types, lifting) diff_add_zero diff_is_0_eq dual_order.trans field_lookup_offset_size' size_of_def)

  obtain pfx sfx xbs where
    xbs: "xbs = pfx @ bs @ sfx" and
    lpfx: "length pfx = n" and
    lsfx: "length sfx = size_of TYPE('a) - n - size_td s"
    by (metis Ex_list_of_length)

  with sz have lxbs: "length xbs = size_of TYPE('a)"
    by (metis add_leD2 add_le_imp_le_diff lbs le_add_diff_inverse length_append)
  from xbs lpfx lsfx xbs lbs have bs: "(take (size_td s) (drop n xbs)) = bs"
    by simp

  obtain pfx' sfx' xbs' where
    xbs': "xbs' = pfx' @ bs' @ sfx'" and
    lpfx': "length pfx' = n" and
    lsfx': "length sfx' = size_of TYPE('a) - n - size_td s"
    by (metis Ex_list_of_length)

  with sz have lxbs': "length xbs' = size_of TYPE('a)"
    by (metis add_leD2 add_le_imp_le_diff lbs' le_add_diff_inverse length_append)

  from xbs' lpfx' lsfx' xbs' lbs' have bs': "(take (size_td s) (drop n xbs')) = bs'"
    by simp

  have bound: "x - n < size_td s" by fact

  have lacc: "length (access_ti (typ_info_t TYPE('a)) v xbs) = size_of TYPE('a)"
    by (simp add: fd_cons_length lxbs size_of_def wf_fd_consD)

  have v_upd_conv: "(update_ti (typ_info_t TYPE('a)) (to_bytes v xbs) v) = v"
    by (simp add: fu_fa lacc lxbs size_of_def to_bytes_def update_ti_update_ti_t)

  have lxto: "length (to_bytes v xbs) = size_of TYPE('a)"
    by (simp add: lacc to_bytes_def)

  from lxto lbs
  have lsuper: "length (super_update_bs bs (to_bytes v xbs) n) = size_of TYPE('a)"
    using sz by auto

  have bound: "x - n < size_td s" by fact

  have xbs_super: "xbs = super_update_bs bs xbs n"
    by (simp add: lpfx super_update_bs_def xbs)

  from mem_type_update_ti_super_update_bs [OF fl lxto lbs, of v, simplified v_upd_conv]
  have upd_eq1:
    "update_ti s bs v =
       update_ti (typ_info_t TYPE('a)) (super_update_bs bs (to_bytes v xbs) n) v" .

  have idx_shift1:
    "take (size_td s) (drop n
         (access_ti (typ_info_t TYPE('a))
           (update_ti (typ_info_t TYPE('a)) (super_update_bs bs (to_bytes v xbs) n) v) xbs'))
        ! (x - n)
       = access_ti (typ_info_t TYPE('a))
           (update_ti (typ_info_t TYPE('a)) (super_update_bs bs (to_bytes v xbs) n) v) xbs'
        ! x "
    by (metis bound fd_cons_length less_diff_conv2 local.wf_fd lower_bound_x lxbs'
        nth_take_drop_index_shift size_of_def sz wf_fd_consD)

  from lxto lbs lower_bound_x upper_bound_x sz
  have super_nth: "super_update_bs bs (to_bytes v xbs) n ! x = bs ! (x - n)"
    by (simp add: super_update_bs_nth_shift)
  note val_eq = padding_base.is_value_byte_acc_upd_cancel [OF is_value lsuper [simplified size_of_def] lxbs' [simplified size_of_def]]
  note acc_eq = mem_type_field_lookup_access_ti_take_drop [OF fl lxbs', simplified bs' ]
  show "access_ti s (update_ti s bs v) bs' ! (x - n) = bs ! (x - n)"
    apply (simp add: upd_eq1)
    apply (simp add: acc_eq)
    apply (simp add: idx_shift1 )
    apply (simp add: val_eq)
    apply (simp add: super_nth)
    done
next
  fix v::'a and bs::"byte list" and b::"byte"
  assume "x - n < size_td s"
  assume lbs: "length bs = size_td s"


  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (metis (no_types, lifting) diff_add_zero diff_is_0_eq dual_order.trans field_lookup_offset_size' size_of_def)

  obtain pfx sfx xbs where
    xbs: "xbs = pfx @ bs @ sfx" and
    lpfx: "length pfx = n" and
    lsfx: "length sfx = size_of TYPE('a) - n - size_td s"
    by (metis Ex_list_of_length)

  with sz have lxbs: "length xbs = size_of TYPE('a)"
    by (metis add_leD2 add_le_imp_le_diff lbs le_add_diff_inverse length_append)
  from xbs lpfx lsfx xbs lbs have bs: "(take (size_td s) (drop n xbs)) = bs"
    by simp

  obtain xbs' where
    xbs': "xbs' = pfx @ bs [x - n := b] @ sfx" by blast
  from lxbs lbs xbs have lxbs': "length xbs' = size_of TYPE('a)"
    using xbs' by auto
  from xbs' lpfx lxbs' lbs have bs': "(take (size_td s) (drop n xbs')) = bs[x - n :=b]"
    by simp

  from lbs lower_bound_x upper_bound_x sz lpfx lsfx
  have xbs'_conv: "xbs' = xbs[x := b]"
    by (simp add: xbs xbs' list_update_append)

  note eq1 = mem_type_field_lookup_access_ti_take_drop [OF fl lxbs, simplified bs, of v]
  note eq2 = mem_type_field_lookup_access_ti_take_drop [OF fl lxbs', simplified bs', of v]
  note val_eq = padding_base.is_value_byte_acc_eq [OF is_value lxbs [simplified size_of_def], where b=b]
  show "access_ti s v bs = access_ti s v (bs[x - n := b])"
    apply (simp add: eq1)
    apply (simp add: val_eq)
    apply (simp add: eq2)
    apply (simp add: xbs'_conv)
    done
qed

lemma (in mem_type) field_lookup_is_value_byte_inner_to_outer:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  assumes is_value: "padding_base.is_value_byte (access_ti s) (update_ti s) (size_td s) (x - n)"
  shows "padding_base.is_value_byte (access_ti (typ_info_t (TYPE('a)))) (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
proof (rule padding_base.is_value_byteI)
  from lower_bound_x upper_bound_x fl
  show "x < size_td (typ_info_t TYPE('a))"
    using field_lookup_offset_size' by fastforce
next
  fix v::'a and bs::"byte list" and bs'::"byte list"
  assume sz: "x < size_td (typ_info_t TYPE('a))"
  assume lbs: "length bs = size_td (typ_info_t TYPE('a))"
  assume lbs': "length bs' = size_td (typ_info_t TYPE('a))"

  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (metis (no_types, lifting) diff_add_zero diff_is_0_eq dual_order.trans field_lookup_offset_size' size_of_def)

  from sz lbs
  have super_bs: "(super_update_bs (take (size_td s) (drop n bs)) bs n) = bs"
    by (metis (no_types, lifting) append.assoc append_len2 append_take_drop_id diff_diff_cancel
        length_drop nat_move_sub_le size_of_def super_update_bs_def take_add)
  from lower_bound_x upper_bound_x lbs sz
  have l_take_drop: "length (take (size_td s) (drop n bs)) = size_td s"
    by (simp add: size_of_def)

  from lower_bound_x upper_bound_x lbs' sz
  have l_take_drop': "length (take (size_td s) (drop n bs')) = size_td s"
    by (simp add: size_of_def)

  from lbs lower_bound_x upper_bound_x sz
  have take_drop_eq: "take (size_td s) (drop n bs) ! (x - n) = bs ! x"
    by (simp add: size_of_def)


  note upd_focus = mem_type_update_ti_super_update_bs [OF fl, simplified size_of_def, OF lbs l_take_drop, simplified super_bs, symmetric ]
  note acc_focus = mem_type_field_lookup_nth_focus [OF fl lower_bound_x upper_bound_x, simplified size_of_def, OF lbs']
  note cancel = padding_base.is_value_byte_acc_upd_cancel [OF is_value l_take_drop l_take_drop']
  show "access_ti (typ_info_t TYPE('a)) (update_ti (typ_info_t TYPE('a)) bs v) bs' ! x =
         bs ! x"
    apply (subst upd_focus)
    apply (simp add: acc_focus)
    apply (simp add: cancel)
    apply (simp add: take_drop_eq)
    done
next
  fix v::'a and bs::"byte list" and b::"byte"
  assume sz: "x < size_td (typ_info_t TYPE('a))"
  assume lbs: "length bs = size_td (typ_info_t TYPE('a))"

  from fl have sz: "size_td s + n ≤ size_of TYPE('a)"
    by (metis (no_types, lifting) diff_add_zero diff_is_0_eq dual_order.trans field_lookup_offset_size' size_of_def)

  note eq1 = mem_type_field_lookup_access_ti_take_drop [OF fl, simplified size_of_def, OF lbs ]


  from sz lower_bound_x upper_bound_x lbs
  have l_take_s: "length (take (size_td s) (drop n bs)) = size_td s"
    by (simp add: size_of_def)

  from lbs sz lower_bound_x upper_bound_x
  have super_eq:
    "super_update_bs (access_ti s v (take (size_td s) (drop n bs)))
          (access_ti (typ_info_t TYPE('a)) v bs) n = (access_ti (typ_info_t TYPE('a)) v bs)"
    by (metis append_take_drop_id eq1 l_take_s length_drop length_fa_ti
        length_take local.wf_fd super_update_bs_def take_drop_append)

  note focus1 = mem_type_field_lookup_nth_update_focus [OF fl lower_bound_x upper_bound_x, simplified size_of_def, OF lbs]
  note pad_eq = padding_base.is_value_byte_acc_eq [OF is_value l_take_s, symmetric]
  show "access_ti (typ_info_t TYPE('a)) v bs =
         access_ti (typ_info_t TYPE('a)) v (bs[x := b])"

    apply (simp add: focus1)
    apply (subst pad_eq)
    apply (simp add: super_eq)
    done
qed


lemma (in mem_type) field_lookup_is_value_byte:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_td s"
  shows "padding_base.is_value_byte (access_ti s) (update_ti s) (size_td s) (x - n) ⟷
   padding_base.is_value_byte (access_ti (typ_info_t (TYPE('a))))
     (update_ti (typ_info_t (TYPE('a)))) (size_td (typ_info_t (TYPE('a)))) x"
  using field_lookup_is_value_byte_inner_to_outer [OF fl lower_bound_x upper_bound_x]
    field_lookup_is_value_byte_outer_to_inner [OF fl lower_bound_x upper_bound_x]
  by blast

thm padding_base.eq_padding_def
thm padding_base.eq_upto_padding_def
(* Such a thing is not present! *)



lemma td_set_component_descs_independent:
 fixes t::"'a xtyp_info"
  and st::"'a xtyp_info_struct"
  and ts::"'a xtyp_info_tuple list"
  and x::"'a xtyp_info_tuple"
shows
  "(s, n) ∈ td_set t m ⟹ component_descs_independent t ⟹ component_descs_independent s"
  "(s, n) ∈ td_set_struct st m ⟹ component_descs_independent_struct st ⟹ component_descs_independent s"
  "(s, n) ∈ td_set_list ts m ⟹ component_descs_independent_list ts ⟹ component_descs_independent s"
  "(s, n) ∈ td_set_tuple x m ⟹ component_descs_independent_tuple x ⟹ component_descs_independent s"
proof (induct t and st and ts and x arbitrary: m and m and m and m)
case (TypDesc algn st nm)
then show ?case by auto
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  then show ?case by auto
next
  case (DTuple_typ_desc d nm y)
  then show ?case by auto
qed

lemma td_set_wf_component_descs:
 fixes t::"'a xtyp_info"
  and st::"'a xtyp_info_struct"
  and ts::"'a xtyp_info_tuple list"
  and x::"'a xtyp_info_tuple"
shows
  "(s, n) ∈ td_set t m ⟹ wf_component_descs t ⟹ wf_component_descs s"
  "(s, n) ∈ td_set_struct st m ⟹ wf_component_descs_struct st ⟹ wf_component_descs s"
  "(s, n) ∈ td_set_list ts m ⟹ wf_component_descs_list ts ⟹ wf_component_descs s"
  "(s, n) ∈ td_set_tuple x m ⟹ wf_component_descs_tuple x ⟹ wf_component_descs s"
proof (induct t and st and ts and x arbitrary: m and m and m and m)
case (TypDesc algn st nm)
then show ?case by auto
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  then show ?case by auto
next
  case (DTuple_typ_desc d nm y)
  then show ?case by auto
qed


lemma td_set_field_descs:
 fixes t::"'a xtyp_info"
  and st::"'a xtyp_info_struct"
  and ts::"'a xtyp_info_tuple list"
  and x::"'a xtyp_info_tuple"
shows
  "(s, n) ∈ td_set t m ⟹ wf_component_descs t ⟹ component_desc s ∈ insert (component_desc t) (set (field_descs t))"
  "(s, n) ∈ td_set_struct st m ⟹ wf_component_descs_struct st ⟹ component_desc s ∈ (set (field_descs_struct st))"
  "(s, n) ∈ td_set_list ts m ⟹ wf_component_descs_list ts ⟹ component_desc s ∈ (set (field_descs_list ts))"
  "(s, n) ∈ td_set_tuple x m ⟹ wf_component_descs_tuple x ⟹ component_desc s ∈ (set (field_descs_tuple x))"
proof (induct t and st and ts and x arbitrary: m and m and m and m)
case (TypDesc algn st nm)
then show ?case by auto
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  then show ?case by auto
next
  case (DTuple_typ_desc d nm y)
  then show ?case by auto
qed

lemma td_set_wf_field_descs:
 fixes t::"'a xtyp_info"
  and st::"'a xtyp_info_struct"
  and ts::"'a xtyp_info_tuple list"
  and x::"'a xtyp_info_tuple"
shows
  "(s, n) ∈ td_set t m ⟹ wf_field_descs (set (field_descs t)) ⟹ wf_field_descs (set (field_descs s))"
  "(s, n) ∈ td_set_struct st m ⟹wf_field_descs (set (field_descs_struct st)) ⟹ wf_field_descs (set (field_descs s))"
  "(s, n) ∈ td_set_list ts m ⟹ wf_field_descs (set (field_descs_list ts)) ⟹ wf_field_descs (set (field_descs s))"
  "(s, n) ∈ td_set_tuple x m ⟹ wf_field_descs (set (field_descs_tuple x)) ⟹ wf_field_descs (set (field_descs s))"
proof (induct t and st and ts and x arbitrary: m and m and m and m)
case (TypDesc algn st nm)
then show ?case by auto
next
  case (TypScalar sz algn d)
  then show ?case by auto
next
  case (TypAggregate ts)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc x fs)
  then show ?case by auto
next
  case (DTuple_typ_desc d nm y)
  then show ?case by auto
qed

context xmem_type
begin
lemma xmem_type_td_set_field_descs:
  "(s,n) ∈ td_set (typ_info_t TYPE('a)) m ⟹
  component_desc s ∈ insert (component_desc (typ_info_t TYPE('a))) (set (field_descs (typ_info_t TYPE('a))))"
  using td_set_field_descs local.wf_component_descs by blast

lemma field_lookup_component_desc:
"field_lookup (typ_info_t TYPE('a)) f m = Some (s, n) ⟹
  component_desc s ∈ insert (component_desc (typ_info_t TYPE('a))) (set (field_descs (typ_info_t TYPE('a))))"
  using xmem_type_td_set_field_descs td_set_field_lookupD
  by blast

lemma field_lookup_wf_field_desc:
"field_lookup (typ_info_t TYPE('a)) f m = Some (s, n) ⟹
  wf_field_desc (component_desc s)"
  using field_lookup_component_desc
  by (meson local.wf_field_descs' wf_field_descs_def)

lemma field_lookup_component_descs_independent:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "component_descs_independent s"
  using field_lookup_component_desc [OF fl]
  by (meson fl local.component_descs_independent td_set_component_descs_independent(1) td_set_field_lookupD)

lemma field_lookup_wf_component_descs:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "wf_component_descs s"
  using field_lookup_component_desc [OF fl] td_set_wf_component_descs fl
    local.wf_component_descs td_set_field_lookupD by blast

lemma field_lookup_wf_field_descs:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "wf_field_descs (set (field_descs s))"
  using td_set_wf_field_descs fl local.wf_field_descs td_set_field_lookupD by blast


lemma field_lookup_field_access_access_ti:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "field_access (component_desc s) = access_ti s"
  using access_ti_component_desc_compatible(1) [OF field_lookup_wf_component_descs [OF fl]
      field_lookup_component_descs_independent [OF fl]  field_lookup_wf_field_descs [OF fl]]
  by (simp add: fun_eq_iff)

lemma field_lookup_field_update_update_ti:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "field_update (component_desc s) = update_ti s"
  using update_ti_component_desc_compatible(1) [OF field_lookup_wf_component_descs [OF fl]
      field_lookup_component_descs_independent [OF fl]  field_lookup_wf_field_descs [OF fl]]
  by (simp add: fun_eq_iff)

lemma field_lookup_field_sz_size_td:
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "field_sz (component_desc s) = size_td s"
  using size_td_field_sz(1)  [OF field_lookup_wf_component_descs [OF fl] ]
  by simp

lemma field_lookup_component_desc_complement_padding:
"field_lookup (typ_info_t TYPE('a)) f m = Some (s, n) ⟹
  complement_padding (field_access (component_desc s)) (field_update (component_desc s)) (field_sz (component_desc s))"
  using field_lookup_component_desc
  by (meson field_lookup_wf_field_desc padding_lense.axioms(1) wf_field_desc.axioms)


lemma field_lookup_component_desc_complement_padding':
  assumes fl: "field_lookup (typ_info_t TYPE('a)) f m = Some (s, n)"
  shows "complement_padding (access_ti s) (update_ti s) (size_td s)"
  using field_lookup_component_desc_complement_padding
    field_lookup_field_access_access_ti [OF fl]
    field_lookup_field_update_update_ti [OF fl]
    field_lookup_field_sz_size_td [OF fl]
  by (metis fl)

lemma field_lookup_padding_lense:
"field_lookup (typ_info_t TYPE('a)) f m = Some (s, n) ⟹
  padding_lense (access_ti s) (update_ti s) (size_td s)"
  by (metis field_lookup_field_access_access_ti field_lookup_field_update_update_ti
      field_lookup_wf_component_descs field_lookup_wf_field_desc size_td_field_sz(1) wf_field_desc_def)

sublocale lense: padding_lense
  "access_ti (typ_info_t TYPE('a))"
  "update_ti (typ_info_t TYPE('a))"
  "size_of TYPE('a)"
  using local.field_access_access_ti local.field_sz_size_of
    local.field_update_update_ti local.xmem_type_wf_field_desc.padding_lense_axioms by simp

end


lemma eq_padding_access_update_field_cancel:
  assumes fl: "field_lookup (typ_info_t (TYPE('a::xmem_type))) f 0 = Some (s, n)"
  assumes lower_bound_x: "n ≤ x"
  assumes upper_bound_x: "x < n + size_of TYPE('b)"
  assumes match: "export_uinfo s = typ_uinfo_t TYPE('b::xmem_type)"
  assumes lbs: "length bs = size_of TYPE('b)"
  assumes lbs': "length bs' = size_of TYPE('a)"
  assumes eq_padding: "padding_base.eq_padding (access_ti s) (size_td s) bs (take (size_of TYPE('b)) (drop n bs'))"
  shows "access_ti (typ_info_t TYPE('a::xmem_type)) (update_ti s bs v) bs' ! x = bs ! (x - n)"
proof -
  obtain i where i: "i = x - n" by blast
  from match fl have sz_b: "size_of TYPE('b) = size_td s"
    using export_size_of by blast

  interpret cps: complement_padding "access_ti s" "update_ti s" "size_td s"
    by (rule field_lookup_component_desc_complement_padding' [OF fl])

  from lower_bound_x upper_bound_x sz_b
  have x_n_bound: "x - n < size_td s"
    by simp
  from eq_padding
  have l_take_drop_bs': "length (take (size_td s) (drop n bs')) = size_td s"
    by (metis lbs padding_base.eq_padding_length_eq sz_b)

  from lower_bound_x upper_bound_x fl lbs'
  have acc_bs': "take (size_td s) (drop n bs') ! (x - n) = bs' ! x"
    by (metis add.commute field_lookup_offset_size nth_take_drop_index_shift size_of_def sz_b)

  from mem_type_field_lookup_nth_focus [OF fl lower_bound_x [simplified size_of_def] upper_bound_x [simplified sz_b] lbs']
  have "access_ti (typ_info_t TYPE('a)) (update_ti s bs v) bs' ! x =
     access_ti s (update_ti s bs v) (take (size_td s) (drop n bs')) ! (x - n) " .
  also have "… = bs ! (x - n)" (is "?lhs = ?rhs")
  proof (cases "padding_base.is_padding_byte (access_ti s) (update_ti s) (size_td s) (x - n)")
    case True

    from padding_base.is_padding_byte_acc_eq [OF True l_take_drop_bs' ] acc_bs'
    have "?lhs = bs' ! x" by simp
    also have "bs' ! x = bs ! (x - n)"
      using cps.eq_padding_padding_byte_id [OF eq_padding True] acc_bs' sz_b
      by simp
    finally show ?thesis .
  next
    case False
    then have is_value: "cps.is_value_byte (x - n)" using cps.complement x_n_bound by simp
    from cps.is_value_byte_acc_upd_cancel [OF is_value lbs [simplified sz_b] l_take_drop_bs']
    show ?thesis .
  qed
  finally show ?thesis .
qed

context xmem_type
begin

sublocale xmem_type_padding: complement_padding
  "access_ti (typ_info_t TYPE('a))"
  "update_ti (typ_info_t TYPE('a))"
  "size_of TYPE('a)"
  using xmem_type_wf_field_desc.complement_padding_axioms
  by (simp add: field_access_access_ti field_update_update_ti field_sz_size_td size_of_def)
end

lemma drop_heap_list_le2:
  "heap_list h n (x + of_nat k)
      = drop k (heap_list h (n + k) x)"
  by (simp add: drop_heap_list_le)

lemma heap_list_take_drop:
  assumes N_bound: "unat a + N ≤ 2 ^ len_of TYPE(addr_bitsize)"
  shows "n + m ≤ N ⟹ take m (drop n (heap_list hp N a)) =
       heap_list hp m (a + word_of_nat n)"
  apply (induct m arbitrary: n)
   apply simp
  apply simp
  using N_bound
  by auto
    (metis (no_types, opaque_lifting) add.left_commute add.right_neutral add_Suc_right drop_heap_list_le2 heap_list_rec take_drop take_heap_list_le)

lemma heap_list_take_drop':
  assumes N_bound: "unat a + N ≤ addr_card"
  assumes bound: "n + m ≤ N"
  shows "take m (drop n (heap_list hp N a)) =
       heap_list hp m (a + word_of_nat n)"
proof -
  have "addr_card = 2 ^ len_of TYPE(addr_bitsize)"
    by (simp add: addr_card)
  from heap_list_take_drop [OF N_bound [simplified this ] bound] show ?thesis by blast
qed

experiment
  fixes proj:: "'a::xmem_type ⇒ 'b::xmem_type"
  fixes t::"'a xtyp_info"

  assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
  and     eu: "export_uinfo t = typ_uinfo_t TYPE('b)"
  assumes access_comp: "access_ti t v = access_ti (typ_info_t TYPE('b)) (proj v)"
  assumes surj: "surj proj"
begin

lemma sz: "size_td t = size_of TYPE('b)"
  using eu
  by (metis export_uinfo_size size_of_def typ_uinfo_size)

lemma "padding_base.eq_padding (access_ti t) (size_td t) =
       padding_base.eq_padding (access_ti (typ_info_t TYPE('b))) (size_of TYPE('b))"
  unfolding padding_base.eq_padding_def
  apply (rule ext)
  apply (rule ext)
  apply (simp add: sz)
  apply (simp add: access_comp)
  using surj
  by (metis surj_def)
end



definition is_padding_byte::"typ_uinfo ⇒ nat ⇒ bool" where
  "is_padding_byte t i ≡ i < size_td t ∧
     (∀bs b. length bs = size_td t ⟶ norm_tu t (bs[i := b]) = norm_tu t bs)"

definition is_value_byte::"typ_uinfo ⇒ nat ⇒ bool" where
  "is_value_byte t i ≡ i < size_td t ∧
     (∃bs b. length bs = size_td t ∧ norm_tu t (bs[i := b]) ≠ norm_tu t bs)"

lemma is_padding_byteI:
  assumes "i < size_td t"
  assumes "⋀i bs b. length bs = size_td t ⟹ norm_tu t (bs[i := b]) = norm_tu t bs"
  shows "is_padding_byte t i"
  using assms by (simp add: is_padding_byte_def)

lemma complement_tu_padding:
"i < size_td t ⟹ is_padding_byte t i ≠ is_value_byte t i"
  by (auto simp add: is_padding_byte_def is_value_byte_def)

definition eq_padding::"typ_uinfo ⇒ byte list ⇒ byte list ⇒ bool" where
 "eq_padding t bs bs' ≡ length bs = size_td t ∧ length bs' = size_td t ∧
    (∀i. is_padding_byte t i ⟶ bs ! i = bs' ! i)"

definition eq_upto_padding::"typ_uinfo ⇒ byte list ⇒ byte list ⇒ bool" where
 "eq_upto_padding t bs bs' ≡ length bs = size_td t ∧ length bs' = size_td t ∧
    (∀i. is_value_byte t i ⟶ bs ! i = bs' ! i)"

lemma eq_padding_refl[simp]: "length bs = size_td t ⟹ eq_padding t bs bs"
  by (auto simp add: eq_padding_def)

lemma eq_upto_padding_refl[simp]: "length bs = size_td t ⟹ eq_upto_padding t bs bs"
  by (auto simp add: eq_upto_padding_def)

lemma eq_padding_sym: "eq_padding t bs bs' ⟷ eq_padding t bs' bs"
  by (auto simp add: eq_padding_def)

lemma eq_padding_symp: "symp (eq_padding t)"
  by (simp add: symp_def eq_padding_sym)

lemma eq_upto_padding_sym: "eq_upto_padding t bs bs' ⟷ eq_upto_padding t bs' bs"
  by (auto simp add: eq_upto_padding_def)

lemma eq_upto_padding_symp: "symp (eq_upto_padding t)"
  by (simp add: symp_def eq_upto_padding_sym)

lemma eq_padding_trans: "eq_padding t bs1 bs2 ⟹ eq_padding t bs2 bs3 ⟹ eq_padding t bs1 bs3"
  by (auto simp add: eq_padding_def)

lemma eq_padding_transp: "transp (eq_padding t)"
  unfolding transp_def
  by (auto intro: eq_padding_trans)

lemma eq_upto_padding_trans: "eq_upto_padding t bs1 bs2 ⟹ eq_upto_padding t bs2 bs3 ⟹ eq_upto_padding t bs1 bs3"
  by (auto simp add: eq_upto_padding_def)

lemma eq_upto_padding_transp: "transp (eq_upto_padding t)"
  unfolding transp_def
  by (auto intro: eq_upto_padding_trans)

lemma eq_padding_eq_upto_padding_eq: "eq_padding t bs bs' ⟹ eq_upto_padding t bs bs' ⟹ bs = bs'"
proof -
assume a1: "eq_padding t bs bs'"
assume a2: "eq_upto_padding t bs bs'"
  have f3: "length bs' = size_td t"
    using a1 by (simp add: eq_padding_def)
  have "length bs = size_td t"
    using a1 eq_padding_def by blast
    then show ?thesis
      using f3 a2 a1 by (metis (full_types) complement_tu_padding eq_padding_def eq_upto_padding_def nth_equalityI)
qed

thm padding_base.is_padding_byte_def




lemma is_padding_byte_access_ti':
  fixes t::"'a xtyp_info"
  and st::"'a xtyp_info_struct"
  and ts::"'a xtyp_info_tuple list"
  and x::"'a xtyp_info_tuple"
shows
"⟦ wf_desc t; wf_size_desc t; wf_field_descs (set (field_descs t)); wf_component_descs t; wf_fd t;
  i < size_td t; length bs = size_td t;
   ∀bs b. length bs = size_td t ⟶ norm_tu (map_td field_norm (λ_. ()) t) (bs[i := b]) = norm_tu (export_uinfo t) bs⟧
  ⟹ access_ti t v bs ! i = bs ! i"

"⟦ wf_desc_struct st