Theory AutoCorres2.CTypes

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

theory CTypes
imports
  CTypesDefs "HOL-Eisbach.Eisbach_Tools"
begin

section ‹‹super_update_bs››

lemma length_super_update_bs [simp]:
  "n + length v ≤ length bs ⟹ length (super_update_bs v bs n) = length bs"
  by (clarsimp simp: super_update_bs_def)

lemma drop_super_update_bs:
  "⟦ k ≤ n; n ≤ length bs ⟧ ⟹ drop k (super_update_bs v bs n) = super_update_bs v (drop k bs) (n - k)"
  by (simp add: super_update_bs_def take_drop)

lemma drop_super_update_bs2:
  "⟦ n ≤ length bs; n + length v ≤ k ⟧ ⟹
      drop k (super_update_bs v bs n) = drop k bs"
  by (clarsimp simp: super_update_bs_def min_def split: if_split_asm)

lemma take_super_update_bs:
  "⟦ k ≤ n; n ≤ length bs ⟧ ⟹ take k (super_update_bs v bs n) = take k bs"
  by (clarsimp simp: super_update_bs_def min_def split: if_split_asm)

lemma take_super_update_bs2:
  "⟦ n ≤ length bs; n + length v ≤ k ⟧ ⟹
      take k (super_update_bs v bs n) = super_update_bs v (take k bs) n"
  apply (clarsimp simp: super_update_bs_def min_def split: if_split_asm)
  apply (cases "n=k"; simp add: drop_take)
  done

lemma take_drop_super_update_bs:
  "length v = n ⟹ m ≤ length bs ⟹ take n (drop m (super_update_bs v bs m)) = v"
  by (simp add: super_update_bs_def)

lemma super_update_bs_take_drop:
  "n + m ≤ length bs ⟹ super_update_bs (take m (drop n bs)) bs n = bs"
  by (simp add: super_update_bs_def) (metis append.assoc append_take_drop_id take_add)

lemma super_update_bs_same_length: "length bs = length xbs ⟹ super_update_bs bs xbs 0 = bs"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append_drop_first:
  "length xbs = m ⟹ n + length bs ≤ m ⟹ drop m (super_update_bs bs (xbs @ ybs) n) = ybs"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append_take_first:
  "length xbs = m ⟹ n + length bs ≤ m ⟹ take m (super_update_bs bs (xbs @ ybs) n) = (super_update_bs bs xbs n)"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append_drop_second:
  "length xbs = m ⟹ m ≤ n  ⟹
  drop m (super_update_bs bs (xbs @ ybs) n) = (super_update_bs bs ybs (n - m))"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append_take_second:
  "length xbs = m ⟹ m ≤ n  ⟹
  take m (super_update_bs bs (xbs @ ybs) n) = xbs"
  by (simp add: super_update_bs_def)

lemma super_update_bs_length: "length bs + n ≤ length xbs ==> length (super_update_bs bs xbs n) = length xbs"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append2: "length xbs ≤ n   ⟹
  super_update_bs bs (xbs @ ybs) n =  xbs @ super_update_bs bs ybs (n - length xbs)"
  by (simp add: super_update_bs_def)

lemma super_update_bs_append1: "n + length bs ≤ length xbs ⟹
  super_update_bs bs (xbs @ ybs) n = super_update_bs bs xbs n @ ybs"
  by (simp add: super_update_bs_def)

section ‹Rest›


lemma fu_commutes:
  "fu_commutes f g ⟹ f bs (g bs' v) = g bs' (f bs v)"
  by (simp add: fu_commutes_def)


lemma size_td_list_append [simp]:
  "size_td_list (xs@ys) = size_td_list xs + size_td_list ys"
  by (induct xs) (auto)


lemma access_ti_append:
  "⋀bs. length bs = size_td_list (xs@ys) ⟹
      access_ti_list (xs@ys) t bs =
          access_ti_list xs t (take (size_td_list xs) bs) @
          access_ti_list ys t (drop (size_td_list xs) bs)"
proof (induct xs)
  case Nil show ?case by simp
next
  case (Cons x xs) thus ?case by (simp add: min_def ac_simps drop_take)
qed

lemma update_ti_append [simp]:
  "⋀bs. update_ti_list (xs@ys) bs v =
      update_ti_list xs (take (size_td_list xs) bs)
          (update_ti_list ys (drop (size_td_list xs) bs) v)"
proof (induct xs)
  case Nil show ?case by simp
next
  case (Cons x xs) thus ?case by (simp add: drop_take ac_simps min_def)
qed

lemma update_ti_struct_t_typscalar [simp]:
  "update_ti_struct_t (TypScalar n algn d) =
      (λbs. if length bs = n then field_update d bs else id)"
  by (rule ext, simp add: update_ti_struct_t_def)

lemma update_ti_list_t_empty [simp]:
  "update_ti_list_t [] = (λx. id)"
  by (rule ext, simp add: update_ti_list_t_def)

lemma update_ti_list_t_cons [simp]:
  "update_ti_list_t (x#xs) = (λbs v.
      if length bs = size_td_tuple x + size_td_list xs then
          update_ti_tuple_t x (take (size_td_tuple x) bs)
              (update_ti_list_t xs (drop (size_td_tuple x) bs) v) else
          v)"
  by (force simp: update_ti_list_t_def update_ti_tuple_t_def min_def)

lemma update_ti_append_s [simp]:
  "⋀bs. update_ti_list_t (xs@ys) bs v = (
      if length bs = size_td_list xs + size_td_list ys then
          update_ti_list_t xs (take (size_td_list xs) bs)
              (update_ti_list_t ys (drop (size_td_list xs) bs) v) else
          v)"
proof (induct xs)
  case Nil show ?case by (simp add: update_ti_list_t_def)
next
  case (Cons x xs) thus ?case by (simp add: min_def drop_take ac_simps)
qed

lemma update_ti_tuple_t_dtuple [simp]:
  "update_ti_tuple_t (DTuple t f d) = update_ti_t t"
  by (rule ext, simp add: update_ti_tuple_t_def update_ti_t_def)

text ‹---------------------------------------------------------------›

lemma field_desc_empty [simp]:
  "field_desc (TypDesc algn (TypAggregate []) nm) =
    ⦇ field_access = λx bs. [],
      field_update = λx. id, field_sz = 0 ⦈"
  by (force simp: update_ti_t_def)


lemma export_uinfo_typdesc_simp [simp]:
  "export_uinfo (TypDesc algn st nm) = map_td field_norm (λ_. ()) (TypDesc algn st nm)"
  by (simp add: export_uinfo_def)

lemma map_td_list_append [simp]:
  "map_td_list f g (xs@ys) = map_td_list f g xs @ map_td_list f g ys"
  by (induct xs) auto

lemma map_td_id:
  "map_td (λn algn. id) id t = (t::('a, 'b) typ_desc)"
  "map_td_struct (λn algn. id) id st = (st::('a, 'b) typ_struct)"
  "map_td_list (λn algn. id) id ts = (ts::('a, 'b) typ_tuple list)"
  "map_td_tuple (λn algn. id) id x = (x::('a, 'b) typ_tuple)"
  by (induction t and st and ts and x) simp_all


lemma dt_snd_map_td_list:
  "dt_snd ` set (map_td_list f g ts) = dt_snd ` set ts"
proof (induct ts)
  case (Cons x xs) thus ?case by (cases x) auto
qed simp

lemma wf_desc_map:
  shows "wf_desc (map_td f g t) = wf_desc t" and
        "wf_desc_struct (map_td_struct f g st) = wf_desc_struct st" and
        "wf_desc_list (map_td_list f g ts) = wf_desc_list ts" and
        "wf_desc_tuple (map_td_tuple f g x) = wf_desc_tuple x"
proof (induct t and st and ts and x)
  case (Cons_typ_desc x xs) thus ?case
    by (cases x, auto simp: dt_snd_map_td_list)
qed auto

lemma wf_desc_list_append [simp]:
  "wf_desc_list (xs@ys) =
   (wf_desc_list xs ∧ wf_desc_list ys ∧ dt_snd ` set xs ∩ dt_snd ` set ys = {})"
  by (induct xs) auto

lemma wf_size_desc_list_append [simp]:
  "wf_size_desc_list (xs@ys) = (wf_size_desc_list xs ∧ wf_size_desc_list ys)"
  by (induct xs) auto

lemma norm_tu_list_append [simp]:
  "norm_tu_list (xs@ys) bs =
   norm_tu_list xs (take (size_td_list xs) bs) @ norm_tu_list ys (drop (size_td_list xs) bs)"
  by (induct xs arbitrary: bs, auto simp: min_def ac_simps drop_take)

lemma wf_size_desc_gt:
  shows "wf_size_desc (t::('a, 'b) typ_desc) ⟹ 0 < size_td t" and
        "wf_size_desc_struct st ⟹ 0 < size_td_struct (st::('a,'b) typ_struct)" and
        "⟦ ts ≠ []; wf_size_desc_list ts ⟧ ⟹ 0 < size_td_list (ts::('a,'b) typ_tuple list)" and
        "wf_size_desc_tuple x ⟹ 0 < size_td_tuple (x::('a,'b) typ_tuple)"
  by (induct t and st and ts and x rule: typ_desc_typ_struct_inducts, auto)

lemma field_lookup_empty [simp]:
  "field_lookup t [] n = Some (t,n)"
  by (cases t) clarsimp

lemma field_lookup_tuple_empty [simp]:
  "field_lookup_tuple x [] n = None"
  by (cases x) clarsimp

lemma field_lookup_list_empty [simp]:
  "field_lookup_list ts [] n = None"
  by (induct ts arbitrary: n) auto

lemma field_lookup_struct_empty [simp]:
  "field_lookup_struct st [] n = None"
  by (cases st) auto

lemma field_lookup_list_append:
  "field_lookup_list (xs@ys) f n = (case field_lookup_list xs f n of
                                      None ⇒ field_lookup_list ys f (n + size_td_list xs)
                                    | Some y ⇒ Some y)"
proof (induct xs arbitrary: n)
  case Nil show ?case by simp
next
  case (Cons x xs) thus ?case
    by (cases x) (auto simp: ac_simps split: option.splits)
qed

lemma field_lookup_list_None:
  "f ∉ dt_snd ` set ts ⟹ field_lookup_list ts (f#fs) m = None"
proof (induct ts arbitrary: f fs m)
  case (Cons x _) thus ?case by (cases x) auto
qed simp

lemma field_lookup_list_Some:
  "f ∈ dt_snd ` set ts ⟹ field_lookup_list ts [f] m ≠ None"
proof (induct ts arbitrary: f m)
  case (Cons x _) thus ?case by (cases x) auto
qed simp

lemma field_lookup_offset_le:
  shows "⋀s m n f. field_lookup t f m = Some ((s::('a,'b) typ_desc),n) ⟹ m ≤ n" and
        "⋀s m n f. field_lookup_struct st f m = Some ((s::('a,'b) typ_desc),n) ⟹ m ≤ n" and
        "⋀s m n f. field_lookup_list ts f m = Some ((s::('a, 'b) typ_desc),n) ⟹ m ≤ n" and
        "⋀s m n f. field_lookup_tuple x f m = Some ((s::('a, 'b) typ_desc),n) ⟹ m ≤ n"
proof (induct t and st and ts and x)
  case (Cons_typ_desc x xs) thus ?case by (fastforce split: option.splits)
qed (auto split: if_split_asm)

lemma field_lookup_offset':
  shows "⋀f m m' n t'. (field_lookup t f m = Some ((t'::('a,'b) typ_desc),m + n)) =
          (field_lookup t f m' = Some (t',m' + n))" and
        "⋀f m m' n t'. (field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),m + n)) =
          (field_lookup_struct st f m' = Some (t',m' + n))" and
        "⋀f m m' n t'. (field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),m + n)) =
          (field_lookup_list ts f m' = Some (t',m' + n))" and
        "⋀f m m' n t'. (field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),m + n)) =
          (field_lookup_tuple x f m' = Some (t',m' + n))"
proof (induct t and st and ts and x)
  case (Cons_typ_desc x xs)
  show ?case
  proof
    assume ls: "field_lookup_list (x # xs) f m = Some (t', m + n)"
    show "field_lookup_list (x # xs) f m' = Some (t', m' + n)" (is "?X")
    proof cases
      assume ps: "field_lookup_tuple x f m = None"
      moreover from this ls have "∃k. n = size_td (dt_fst x) + k"
        by (clarsimp dest!: field_lookup_offset_le, arith)
      moreover have "field_lookup_tuple x f m' = None"
        apply (rule ccontr)
        using ps
        apply clarsimp
        subgoal premises prems for a b
        proof -
          obtain k where "b = m' + k"
            using prems field_lookup_offset_le
            by (metis less_eqE)
        then show ?thesis
          using prems
          by (clarsimp simp: Cons_typ_desc [where m'=m])
      qed
      done
      ultimately show "?X" using ls
        by (clarsimp simp: add.assoc [symmetric])
           (subst (asm) Cons_typ_desc [where m'="m' + size_td (dt_fst x)"], fast)
    next
      assume nps: "field_lookup_tuple x f m ≠ None"
      moreover from this have "field_lookup_tuple x f m' ≠ None"
        apply (clarsimp)
        subgoal premises prems for a b
        proof -
          obtain k where "b = m + k"
            using prems field_lookup_offset_le
            by (metis less_eqE)
          then show ?thesis 
            using prems
            apply clarsimp
            apply (subst (asm) Cons_typ_desc [where m'=m']) 
            apply fast
            done
        qed
        done
      ultimately show "?X" using ls
        by (clarsimp, subst (asm) Cons_typ_desc [where m'=m'], simp)
    qed
  next
    assume ls: "field_lookup_list (x # xs) f m' = Some (t', m' + n)"
    show "field_lookup_list (x # xs) f m = Some (t', m + n)" (is "?X")
    proof cases
      assume ps: "field_lookup_tuple x f m' = None"
      moreover from this ls have "∃k. n = size_td (dt_fst x) + k"
        by (clarsimp dest!: field_lookup_offset_le, arith)
      moreover have "field_lookup_tuple x f m = None"
        apply (rule ccontr)
        using ps
        apply clarsimp
        subgoal premises prems for a b
        proof -
          obtain k where "b = m + k"
            using prems field_lookup_offset_le
            by (metis less_eqE)
          then show ?thesis using prems
            by (clarsimp simp: Cons_typ_desc [where m'=m'])
        qed
        done
      ultimately show "?X" using ls
        by (clarsimp simp: add.assoc [symmetric])
           (subst (asm) Cons_typ_desc [where m'="m + size_td (dt_fst x)"], fast)
    next
      assume nps: "field_lookup_tuple x f m' ≠ None"
      moreover from this have "field_lookup_tuple x f m ≠ None"
        apply clarsimp
        subgoal premises prems for a b
        proof -
          obtain k where "b = m' + k"
            using prems field_lookup_offset_le
            by (metis less_eqE)
          then show ?thesis using prems
            apply clarsimp
            apply (subst (asm) Cons_typ_desc [where m'=m]) 
            apply fast
            done
        qed
        done
      ultimately show "?X" using ls
        by (clarsimp, subst (asm) Cons_typ_desc [where m'=m], simp)
    qed
  qed
qed auto

lemma field_lookup_offset:
  "(field_lookup t f m = Some (t',m + n)) = (field_lookup t f 0 = Some (t',n))"
  by (simp add: field_lookup_offset' [where m'=0])

lemma field_lookup_offset2:
  "field_lookup t f m = Some (t',n) ⟹ field_lookup t f 0 = Some (t',n - m)"
  by (simp add: field_lookup_offset_le
           flip: field_lookup_offset [where m=m])

lemma field_lookup_list_offset:
  "(field_lookup_list ts f m = Some (t',m + n)) = (field_lookup_list ts f 0 = Some (t',n))"
  by (simp add: field_lookup_offset' [where m'=0])

lemma field_lookup_list_offset2:
  "field_lookup_list ts f m = Some (t',n) ⟹ field_lookup_list ts f 0 = Some (t',n - m)"
  by (simp add: field_lookup_offset_le
           flip: field_lookup_list_offset [where m=m])

lemma field_lookup_list_offset3:
  "field_lookup_list ts f 0 = Some (t',n) ⟹ field_lookup_list ts f m = Some (t',m + n)"
  by (simp add: field_lookup_list_offset)

lemma field_lookup_list_offsetD:
  "⟦ field_lookup_list ts f 0 = Some (s,k);
      field_lookup_list ts f m = Some (t,n) ⟧ ⟹ s=t ∧ n=m+k"
  subgoal premises prems
  proof - 
    have "∃k. n = m + k" using prems field_lookup_offset_le by (metis less_eqE)
    then show ?thesis using prems
      by (clarsimp simp: field_lookup_list_offset)
  qed
  done

lemma field_lookup_offset_None:
  "(field_lookup t f m = None) = (field_lookup t f 0 = None)"
  by (auto simp: field_lookup_offset2 field_lookup_offset [where m=m,symmetric]
           intro: ccontr)

lemma field_lookup_list_offset_None:
  "(field_lookup_list ts f m = None) = (field_lookup_list ts f 0 = None)"
  by (auto simp: field_lookup_list_offset2 field_lookup_list_offset [where m=m,symmetric]
           intro: ccontr)

lemma map_td_size [simp]:
  shows "size_td (map_td f g t) = size_td t" and
        "size_td_struct (map_td_struct f g st) = size_td_struct st" and
        "size_td_list (map_td_list f g ts) = size_td_list ts" and
        "size_td_tuple (map_td_tuple f g x) = size_td_tuple x"
  by (induct t and st and ts and x, auto)

lemma td_set_map_td1:
"(s, n) ∈ td_set t k ⟹ (map_td f g s, n) ∈ td_set (map_td f g t) k" and
"(s, n) ∈ td_set_struct st k ⟹ (map_td f g s, n) ∈ td_set_struct (map_td_struct f g st) k" and
"(s, n) ∈ td_set_list ts k ⟹ (map_td f g s, n) ∈ td_set_list (map_td_list f g ts) k" and
"(s, n) ∈ td_set_tuple td k ⟹ (map_td f g s, n) ∈ td_set_tuple (map_td_tuple f g td) k"
     apply (induct t and st and ts and td arbitrary: n k and n k and n k and n k)
  by (auto, metis dt_tuple.collapse map_td_size(4) tz5)


lemma size_td_tuple_dt_fst:
  "size_td_tuple p = size_td (dt_fst p)"
  by (cases p, simp)

lemma td_set_map_td2:
"(s', n) ∈ td_set (map_td f g t) k ⟹ ∃s. (s, n) ∈ td_set t k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_struct (map_td_struct f g st) k ⟹ ∃s. (s, n) ∈ td_set_struct st k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_list (map_td_list f g ts) k ⟹ ∃s. (s, n) ∈ td_set_list ts k ∧ s' = map_td f g s" and
"(s', n) ∈ td_set_tuple (map_td_tuple f g td) k ⟹ ∃s. (s, n) ∈ td_set_tuple td k ∧ s' = map_td f g s"
proof (induct t and st and ts and td arbitrary: n k  and n k  and n k  and n k )
  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, safe)
     apply blast
    by (metis map_td_size(4) size_td_tuple_dt_fst)
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by auto
qed

lemma td_set_offset1:
"(s, n) ∈ td_set t k ⟹ (s, n + l) ∈ td_set t (k + l)" and
"(s, n) ∈ td_set_struct st k ⟹ (s, n + l) ∈ td_set_struct st (k + l)" and
"(s, n) ∈ td_set_list xs k ⟹ (s, n + l) ∈ td_set_list xs (k + l)" and
"(s, n) ∈ td_set_tuple td k ⟹ (s, n + l) ∈ td_set_tuple td (k + l)"
 apply (induct t and st and xs and td arbitrary: s n k l and  s n k l  and s n k l  and s n k l)
 by (auto, smt (verit, best) add.commute add.left_commute)

lemma td_set_offset2:
"(s, n + l) ∈ td_set t (k + l) ⟹ (s, n) ∈ td_set t k" and
"(s, n + l) ∈ td_set_struct st (k + l) ⟹ (s, n) ∈ td_set_struct st k" and
"(s, n + l) ∈ td_set_list xs (k + l) ⟹ (s, n) ∈ td_set_list xs k" and
"(s, n + l) ∈ td_set_tuple td (k + l) ⟹ (s, n) ∈ td_set_tuple td k"
 apply (induct t and st and xs and td arbitrary: s n k l and  s n k l  and s n k l  and s n k l)
 by (auto, smt (verit, best) add.commute add.left_commute)

lemma td_set_offset_conv: "(s, n) ∈ td_set t k  ⟷ (s, n + l) ∈ td_set t (k + l)"
  using td_set_offset1 td_set_offset2 by blast

lemma td_set_offset_0_conv: "(s, n + k) ∈ td_set t k ⟷ (s, n) ∈ td_set t 0 "
  using td_set_offset_conv [where k=0 and n=n and l=k and s=s and t =t]
  by simp

lemma td_set_offset_le':
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ m ≤ n"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ m ≤ n"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ m ≤ n"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ m ≤ n"
  by (induct t and st and ts and x) fastforce+

lemma td_set_offset_0_conv': "(s, n) ∈ td_set t k ⟷ (∃n'. (s, n') ∈ td_set t 0 ∧ n = n' + k) "
  by (metis add.commute le_Suc_ex td_set_offset_0_conv td_set_offset_le'(1))


lemma td_set_list_set_td_set1: "(s, n) ∈ td_set_list ts k ⟹
  (∃t n'. t ∈ set ts ∧ (s, n') ∈ td_set (dt_fst t) 0)"
  apply (induct ts arbitrary: n k)
   apply simp
  apply simp
  by (metis dt_tuple.collapse td_set_offset_0_conv' ts5)

lemma export_uinfo_size [simp]:
  "size_td (export_uinfo t) = size_td (t::('a,'b) typ_info)"
  by (simp add: export_uinfo_def)

lemma (in c_type) typ_uinfo_size [simp]:
  "size_td (typ_uinfo_t TYPE('a)) = size_td (typ_info_t TYPE('a))"
  by (simp add: typ_uinfo_t_def export_uinfo_def)

lemma wf_size_desc_map:
  shows "wf_size_desc (map_td f g t) = wf_size_desc t" and
        "wf_size_desc_struct (map_td_struct f g st) = wf_size_desc_struct st" and
        "wf_size_desc_list (map_td_list f g ts) = wf_size_desc_list ts" and
        "wf_size_desc_tuple (map_td_tuple f g x) = wf_size_desc_tuple x"
proof (induction t and st and ts and x)
  case (TypAggregate list)
  then show ?case by (cases list) auto
qed auto

lemma map_td_flr_Some [simp]:
  "map_td_flr f g (Some (t,n)) = Some (map_td f g t,n)"
  by (clarsimp simp: map_td_flr_def)

lemma map_td_flr_None [simp]:
  "map_td_flr f g None = None"
  by (clarsimp simp: map_td_flr_def)

lemma field_lookup_map:
  shows "⋀f m s. field_lookup t f m = s ⟹
            field_lookup (map_td fupd g t) f m = map_td_flr fupd g s" and
        "⋀f m s. field_lookup_struct st f m = s ⟹
            field_lookup_struct (map_td_struct fupd g st) f m = map_td_flr fupd g s" and
        "⋀f m s. field_lookup_list ts f m = s ⟹
            field_lookup_list (map_td_list fupd g ts) f m = map_td_flr fupd g s" and
        "⋀f m s. field_lookup_tuple x f m = s ⟹
            field_lookup_tuple (map_td_tuple fupd g x) f m = map_td_flr fupd g s"
proof (induct t and st and ts and x)
  case (Cons_typ_desc x xs) thus ?case
    by (clarsimp, cases x, auto simp: map_td_flr_def split: option.splits)
qed auto

lemma field_lookup_export_uinfo_Some:
  "field_lookup (t::('a,'b) typ_info) f m = Some (s,n) ⟹
      field_lookup (export_uinfo t) f m = Some (export_uinfo s,n)"
  by (simp add: export_uinfo_def field_lookup_map)

lemma field_lookup_struct_export_Some:
  "field_lookup_struct (st::('a,'b) typ_struct) f m = Some (s,n) ⟹
      field_lookup_struct (map_td_struct fupd g st) f m = Some (map_td fupd g s,n)"
  by (simp add: field_lookup_map)

lemma field_lookup_struct_export_None:
  "field_lookup_struct (st::('a, 'b) typ_struct) f m = None ⟹
      field_lookup_struct (map_td_struct fupd g st) f m = None"
  by (simp add: field_lookup_map)

lemma field_lookup_list_export_Some:
  "field_lookup_list (ts::('a, 'b) typ_tuple list) f m = Some (s,n) ⟹
      field_lookup_list (map_td_list fupd g ts) f m = Some (map_td fupd g s,n)"
  by (simp add: field_lookup_map)

lemma field_lookup_list_export_None:
  "field_lookup_list (ts::('a, 'b) typ_tuple list) f m = None ⟹
      field_lookup_list (map_td_list fupd g ts) f m = None"
  by (simp add: field_lookup_map)

lemma field_lookup_tuple_export_Some:
  "field_lookup_tuple (x::('a, 'b) typ_tuple) f m = Some (s,n) ⟹
      field_lookup_tuple (map_td_tuple fupd g x) f m = Some (map_td fupd g s,n)"
  by (simp add: field_lookup_map)

lemma field_lookup_tuple_export_None:
  "field_lookup_tuple (x::('a, 'b) typ_tuple) f m = None ⟹
      field_lookup_tuple (map_td_tuple fupd g x) f m = None"
  by (simp add: field_lookup_map)

lemma import_flr_Some [simp]:
  "import_flr f g (Some (map_td f g t,n)) (Some (t,n))"
  by (clarsimp simp: import_flr_def)

lemma import_flr_None [simp]:
  "import_flr f g None None"
  by (clarsimp simp: import_flr_def)

lemma field_lookup_export_uinfo_rev'':
  "⋀f m s. field_lookup (map_td fupd g t) f m = s ⟹
      import_flr fupd g s ((field_lookup t f m)::('a,'b) flr)"
  "⋀f m s. field_lookup_struct (map_td_struct fupd g st) f m = s ⟹
      import_flr fupd g s ((field_lookup_struct st f m)::('a,'b) flr)"
  "⋀f m s. field_lookup_list (map_td_list fupd g ts) f m = s ⟹
      import_flr fupd g s ((field_lookup_list ts f m)::('a,'b) flr)"
  "⋀f m s. field_lookup_tuple (map_td_tuple fupd g x) f m = s ⟹
      import_flr fupd g s ((field_lookup_tuple x f m)::('a,'b)  flr)"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: import_flr_def export_uinfo_def)
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(clarsimp split: option.splits)
     apply(cases f, clarsimp+)
     apply(rule conjI, clarsimp)
      apply(cases dt_tuple, simp)
     apply clarsimp
     apply(drule field_lookup_tuple_export_Some [where fupd=fupd and g=g])
     apply simp
    apply(rule conjI; clarsimp)
     apply(drule field_lookup_tuple_export_None [where fupd=fupd and g=g])
     apply simp
    apply metis
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by (auto)
qed



lemma field_lookup_export_uinfo_rev':
  "(∀f m s. field_lookup (map_td fupd g t) f m = s ⟶
      import_flr fupd g s ((field_lookup t f m)::('a,'b) flr)) ∧
   (∀f m s. field_lookup_struct (map_td_struct fupd g st) f m = s ⟶
      import_flr fupd g s ((field_lookup_struct st f m)::('a,'b) flr)) ∧
   (∀f m s. field_lookup_list (map_td_list fupd g ts) f m = s ⟶
      import_flr fupd g s ((field_lookup_list ts f m)::('a,'b) flr)) ∧
   (∀f m s. field_lookup_tuple (map_td_tuple fupd g x) f m = s ⟶
      import_flr fupd g s ((field_lookup_tuple x f m)::('a,'b)  flr))"
  by (auto simp: field_lookup_export_uinfo_rev'')


lemma field_lookup_export_uinfo_Some_rev:
  "field_lookup (export_uinfo (t::('a,'b) typ_info)) f m = Some (s,n) ⟹
      ∃k. field_lookup t f m = Some (k,n) ∧ export_uinfo k = s"
  apply(insert field_lookup_export_uinfo_rev' [of field_norm "(λ_. ())" t undefined undefined undefined])
  apply clarsimp
  apply(drule spec [where x=f])
  apply(drule spec [where x=m])
  apply(clarsimp simp: import_flr_def export_uinfo_def split: option.splits)
  done

lemma (in c_type) field_lookup_uinfo_Some_rev:
  "field_lookup (typ_uinfo_t (TYPE('a))) f m = Some (s,n) ⟹
      ∃k. field_lookup (typ_info_t (TYPE('a))) f m = Some (k,n) ∧ export_uinfo k = s"
  apply (simp add: typ_uinfo_t_def)
  apply (rule field_lookup_export_uinfo_Some_rev)
  apply assumption
  done

lemma (in c_type) field_lookup_offset_untyped_eq [simp]:
  "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n) ⟹
      field_offset_untyped (typ_uinfo_t TYPE('a)) f = n"
  apply(simp add: field_offset_untyped_def typ_uinfo_t_def)
  apply(drule field_lookup_export_uinfo_Some)
  apply(simp add: typ_uinfo_t_def export_uinfo_def)
  done

lemma (in c_type) field_lookup_offset_eq [simp]:
  "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s,n) ⟹
      field_offset TYPE('a) f = n"
  by(simp add: field_offset_def)

lemma field_offset_self [simp]:
  "field_offset t [] = 0"
  by (simp add: field_offset_def field_offset_untyped_def)

lemma (in c_type) field_ti_self [simp]:
  "field_ti TYPE('a) [] = Some (typ_info_t TYPE('a))"
  by (simp add: field_ti_def)

lemma (in c_type) field_size_self [simp]:
  "field_size TYPE('a) [] = size_td (typ_info_t TYPE('a))"
  by (simp add: field_size_def)


lemma field_lookup_prefix_None'':
  "(∀f g m. field_lookup (t::('a,'b) typ_desc) f m = None ⟶ field_lookup t (f@g) m = None)"
  "(∀f g m. field_lookup_struct (st::('a,'b) typ_struct) f m = None ⟶ f ≠ [] ⟶
      field_lookup_struct st (f@g) m = None)"
  "(∀f g m. field_lookup_list (ts::('a,'b) typ_tuple list) f m = None ⟶ f ≠ [] ⟶
      field_lookup_list ts (f@g) m = None)"
  "(∀f g m. field_lookup_tuple (x::('a,'b) typ_tuple) f m = None ⟶ f ≠ [] ⟶
      field_lookup_tuple x (f@g) m = None)"
  by (induct t and st and ts and x)
     (clarsimp split: option.splits)+

lemma field_lookup_prefix_None':
  "(∀f g m. field_lookup (t::('a,'b) typ_desc) f m = None ⟶ field_lookup t (f@g) m = None) ∧
   (∀f g m. field_lookup_struct (st::('a,'b) typ_struct) f m = None ⟶ f ≠ [] ⟶
      field_lookup_struct st (f@g) m = None) ∧
   (∀f g m. field_lookup_list (ts::('a,'b) typ_tuple list) f m = None ⟶ f ≠ [] ⟶
      field_lookup_list ts (f@g) m = None) ∧
   (∀f g m. field_lookup_tuple (x::('a,'b) typ_tuple) f m = None ⟶ f ≠ [] ⟶
      field_lookup_tuple x (f@g) m = None)"
  by (auto simp: field_lookup_prefix_None'')

lemma field_lookup_prefix_Some'':
  "(∀f g t' m n. field_lookup t f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc t ⟶
      field_lookup t (f@g) m = field_lookup t' g n)"
  "(∀f g t' m n. field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_struct st ⟶
      field_lookup_struct st (f@g) m = field_lookup t' g n)"
  "(∀f g t' m n. field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_list ts ⟶
      field_lookup_list ts (f@g) m = field_lookup t' g n)"
  "(∀f g t' m n. field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_tuple x ⟶
      field_lookup_tuple x (f@g) m = field_lookup t' g n)"
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 split: option.splits)
    apply(cases dt_tuple)
    subgoal for f
    apply(cases f, clarsimp)
      by (clarsimp simp: field_lookup_list_None split: if_split_asm)
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case  by auto
qed


lemma field_lookup_prefix_Some':
  "(∀f g t' m n. field_lookup t f m = Some ((t'::('a, 'b) typ_desc),n) ⟶ wf_desc t ⟶
      field_lookup t (f@g) m = field_lookup t' g n) ∧
   (∀f g t' m n. field_lookup_struct st f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_struct st ⟶
      field_lookup_struct st (f@g) m = field_lookup t' g n) ∧
   (∀f g t' m n. field_lookup_list ts f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_list ts ⟶
      field_lookup_list ts (f@g) m = field_lookup t' g n) ∧
   (∀f g t' m n. field_lookup_tuple x f m = Some ((t'::('a,'b) typ_desc),n) ⟶ wf_desc_tuple x ⟶
      field_lookup_tuple x (f@g) m = field_lookup t' g n)"
  by (auto simp: field_lookup_prefix_Some'')

lemma field_lookup_append_eq:
  "wf_desc t ⟹
    field_lookup t (f @ g) n =
    Option.bind (field_lookup t f n) (λ(t', m). field_lookup t' g m)"
  by (cases "field_lookup t f n")
     (auto simp add: field_lookup_prefix_None''(1)[rule_format]
                     field_lookup_prefix_Some''(1)[rule_format])

lemma field_lookup_offset_shift:
  "NO_MATCH 0 m ⟹ field_lookup t f 0 = Some (t', n) ⟹ field_lookup t f m = Some (t', m + n)"
  by (simp add: field_lookup_offset)

lemma field_lookup_offset_shift':
  "field_lookup t f m = Some (s, k) ⟹ field_lookup t f n = Some (s, k + n - m)"
  by (metis CTypes.field_lookup_offset2 Nat.add_diff_assoc2 add.commute field_lookup_offset
            field_lookup_offset_le(1))

lemma field_lookup_append:
  assumes t: "wf_desc t"
    and f: "field_lookup t f n = Some (u, m)" and g: "field_lookup u g l = Some (v, k)"
  shows "field_lookup t (f @ g) n = Some (v, k + m - l)"
  using field_lookup_prefix_Some''(1)[rule_format, OF f t, of g]
    g[THEN field_lookup_offset_shift', of m]
  by simp

lemma field_lvalue_empty_simp [simp]:
  "Ptr &(p→[]) = p"
  by (simp add: field_lvalue_def field_offset_def field_offset_untyped_def)

lemma map_td_align [simp]:
  "align_td_wo_align (map_td f g t) = align_td_wo_align (t::('a,'b) typ_desc)"
  "align_td_wo_align_struct (map_td_struct f g st) = align_td_wo_align_struct (st::('a,'b) typ_struct)"
  "align_td_wo_align_list (map_td_list f g ts) = align_td_wo_align_list (ts::('a,'b) typ_tuple list)"
  "align_td_wo_align_tuple (map_td_tuple f g x) = align_td_wo_align_tuple (x::('a,'b) typ_tuple)"
  by (induct t and st and ts and x) auto

lemma map_td_align' [simp]:
  "align_td (map_td f g t) = align_td (t::('a,'b) typ_desc)"
  "align_td_struct (map_td_struct f g st) = align_td_struct (st::('a,'b) typ_struct)"
  "align_td_list (map_td_list f g ts) = align_td_list (ts::('a,'b) typ_tuple list)"
  "align_td_tuple (map_td_tuple f g x) = align_td_tuple (x::('a,'b) typ_tuple)"
  by (induct t and st and ts and x) auto

lemma typ_uinfo_align [simp]:
  "align_td_wo_align (export_uinfo t) = align_td_wo_align (t::('a,'b) typ_info)"
  by (simp add: export_uinfo_def)

lemma ptr_aligned_Ptr_0 [simp]:
  "ptr_aligned NULL"
  by (simp add: ptr_aligned_def)

lemma td_set_self [simp]:
  "(t,m) ∈ td_set t m"
  by (cases t) simp

lemma td_set_wf_size_desc [rule_format]:
  "(∀s m n. wf_size_desc t ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set t n ⟶ wf_size_desc s)"
  "(∀s m n. wf_size_desc_struct st ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_struct st n ⟶ wf_size_desc s)"
  "(∀s m n. wf_size_desc_list ts ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_list ts n ⟶ wf_size_desc s)"
  "(∀s m n. wf_size_desc_tuple x ⟶ ((s::('a,'b) typ_desc),m) ∈ td_set_tuple x n ⟶ wf_size_desc s)"
  by (induct t and st and ts and x) force+

lemma td_set_size_lte':
  "(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set t m ⟶ size s = size t ∧ s=t ∧ k=m ∨ size s < size t)"
  "(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_struct st m ⟶ size s < size st)"
  "(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_list xs m ⟶ size s < size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) xs)"
  "(∀s k m. ((s::('a,'b) typ_desc),k) ∈ td_set_tuple x m ⟶ size s < size_dt_tuple size (λ_. 0) (λ_. 0) x)"
  by (induct t and st and xs and x) force+

lemma td_set_size_lte:
  "(s,k) ∈ td_set t m ⟹ size s = size t ∧ s=t ∧ k=m ∨
      size s < size t"
  by (simp add: td_set_size_lte')

lemma td_set_struct_size_lte:
  "(s,k) ∈ td_set_struct st m ⟹ size s < size st"
  by (simp add: td_set_size_lte')

lemma td_set_list_size_lte:
  "(s,k) ∈ td_set_list ts m ⟹ size s < size_list (size_dt_tuple size (λ_. 0) (λ_. 0)) ts"
  by (simp add: td_set_size_lte')

lemma td_aggregate_not_in_td_set_list [simp]:
  "¬ (TypDesc algn (TypAggregate xs) tn,k) ∈ td_set_list xs m"
  by (fastforce dest: td_set_list_size_lte simp: size_char_def)

lemma sub_size_td:
  "(s::('a,'b) typ_desc) ≤ t ⟹ size s ≤ size t"
  by (fastforce dest: td_set_size_lte simp: typ_tag_le_def)

lemma sub_tag_antisym:
  "⟦ (s::('a,'b) typ_desc) ≤ t; t ≤ s ⟧ ⟹ s=t"
  apply(frule sub_size_td)
  apply(frule sub_size_td [where t=s])
  apply(clarsimp simp: typ_tag_le_def)
  apply(drule td_set_size_lte)
  apply clarsimp
  done

lemma sub_tag_refl:
  "(s::('a,'b) typ_desc) ≤ s"
  unfolding typ_tag_le_def by (cases s, fastforce)

lemma sub_tag_sub':
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m ⟶ td_set s n ⊆ td_set t m"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct ts m ⟶ td_set s n ⊆ td_set_struct ts m"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list xs m ⟶ td_set s n ⊆ td_set_list xs m"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ td_set s n ⊆ td_set_tuple x m"
  by (induct t and ts and xs and x) fastforce+

lemma sub_tag_sub:
  "(s,n) ∈ td_set t m ⟹ td_set s n ⊆ td_set t m"
  by (simp add: sub_tag_sub')

lemma td_set_fst:
  "∀m n. fst ` td_set (s::('a, 'b) typ_desc) m = fst ` td_set s n"
  "∀m n. fst ` td_set_struct (st::('a,'b) typ_struct) m = fst ` td_set_struct st n"
  "∀m n. fst ` td_set_list (xs::('a, 'b) typ_tuple list) m = fst ` td_set_list xs n"
  "∀m n. fst ` td_set_tuple (x::('a, 'b) typ_tuple) m = fst ` td_set_tuple x n"
  by (induct s and st and xs and x) (all ‹clarsimp›, fast, fast)

lemma sub_tag_trans:
  "⟦ (s::('a,'b) typ_desc) ≤ t; t ≤ u ⟧ ⟹ s ≤ u"
  apply(clarsimp simp: typ_tag_le_def)
  by (meson sub_tag_sub'(1) subset_iff td_set_offset_0_conv)

(*fixme: move*)
instantiation typ_desc :: (type, type) order
begin
instance
  apply intro_classes
     apply(fastforce simp: typ_tag_lt_def typ_tag_le_def dest: td_set_size_lte)
    apply(rule sub_tag_refl)
   apply(erule (1) sub_tag_trans)
  apply(erule (1) sub_tag_antisym)
  done
end

lemma td_set_offset_size'':
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m  ⟶ size_td s + (n - m) ≤ size_td t"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ size_td s + (n - m) ≤ size_td_struct st"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ size_td s + (n - m) ≤ size_td_list ts"
  "∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ size_td s + (n - m) ≤ size_td_tuple x"
proof (induct t and st and ts and x)
  case (Cons_typ_desc dt_tuple list)
  then show ?case  
    apply (cases dt_tuple) 
    apply fastforce
    done
qed auto

lemma td_set_offset_size':
  "(∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set t m  ⟶ size_td s + (n - m) ≤ size_td t) ∧
    (∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_struct st m ⟶ size_td s + (n - m) ≤ size_td_struct st) ∧
    (∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_list ts m ⟶ size_td s + (n - m) ≤ size_td_list ts) ∧
    (∀s m n. ((s::('a,'b) typ_desc),n) ∈ td_set_tuple x m ⟶ size_td s + (n - m) ≤ size_td_tuple x)"
  by (auto simp: td_set_offset_size'')

lemma td_set_offset_size:
  "(s,n) ∈ td_set t 0 ⟹ size_td s + n ≤ size_td t"
  using td_set_offset_size' [of t undefined undefined undefined] by fastforce

lemma td_set_struct_offset_size:
  "(s,n) ∈ td_set_struct st m ⟹ size_td s + (n - m) ≤ size_td_struct st"
  using td_set_offset_size' [of undefined st undefined undefined] by clarsimp

lemma td_set_list_offset_size:
  "(s,n) ∈ td_set_list ts 0 ⟹ size_td s + n ≤ size_td_list ts"
  using td_set_offset_size' [of undefined undefined ts undefined]
  by fastforce

lemma td_set_offset_size_m:
  "(s,n) ∈ td_set t m ⟹ size_td s + (n - m) ≤ size_td t"
  using insert td_set_offset_size' [of t undefined undefined undefined]
  by clarsimp

lemma td_set_list_offset_size_m:
  "(s,n) ∈ td_set_list t m ⟹ size_td s + (n - m) ≤ size_td_list t"
  using insert td_set_offset_size' [of undefined undefined t undefined]
  by clarsimp

lemma td_set_tuple_offset_size_m:
  "(s,n) ∈ td_set_tuple t m ⟹ size_td s + (n - m) ≤ size_td_tuple t"
  using td_set_offset_size' [of undefined undefined undefined t]
  by clarsimp



lemma td_set_list_offset_le:
  "(s,n) ∈ td_set_list ts m ⟹ m ≤ n"
  by (simp add: td_set_offset_le')

lemma td_set_tuple_offset_le:
  "(s,n) ∈ td_set_tuple ts m ⟹ m ≤ n"
  by (simp add: td_set_offset_le')

lemma field_of_self [simp]:
  "field_of 0 t t"
  by (simp add: field_of_def)

lemma td_set_export_uinfo':
  "∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set t m ⟶
     (export_uinfo s,n) ∈ td_set (export_uinfo t) m"
  "∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_struct st m ⟶
     (export_uinfo s,n) ∈ td_set_struct (map_td_struct field_norm (λ_. ()) st) m"
  "∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_list ts m ⟶
     (export_uinfo s,n) ∈ td_set_list (map_td_list field_norm (λ_. ()) ts) m"
  "∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_tuple x m ⟶
     (export_uinfo s,n) ∈ td_set_tuple (map_td_tuple field_norm (λ_. ()) x) m"
proof (induct t and st and ts and x)
  case (Cons_typ_desc dt_tuple list)
  then show ?case by(cases dt_tuple) (simp add: export_uinfo_def)
qed (auto simp add: export_uinfo_def)

lemma td_set_export_uinfo:
  "(∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set t m ⟶
      (export_uinfo s,n) ∈ td_set (export_uinfo t) m) ∧
   (∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_struct st m ⟶
      (export_uinfo s,n) ∈ td_set_struct (map_td_struct field_norm (λ_. ()) st) m) ∧
   (∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_list ts m ⟶
      (export_uinfo s,n) ∈ td_set_list (map_td_list field_norm (λ_. ()) ts) m) ∧
   (∀f m n s. ((s::('a,'b) typ_info),n) ∈ td_set_tuple x m ⟶
      (export_uinfo s,n) ∈ td_set_tuple (map_td_tuple field_norm (λ_. ()) x) m)"
  by (auto simp: td_set_export_uinfo')


lemma td_set_export_uinfoD:
  "(s,n) ∈ td_set t m ⟹ (export_uinfo s,n) ∈ td_set (export_uinfo t) m"
  using td_set_export_uinfo [of t undefined undefined undefined] by clarsimp

lemma td_set_field_lookup'':
  "∀s m n. wf_desc t ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set t m ⟶
     (∃f. field_lookup t f m = Some (s,m+n)))"
  "∀s m n. wf_desc_struct st ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m ⟶
     (∃f. field_lookup_struct st f m = Some (s,m+n)))"
  "∀s m n. wf_desc_list ts ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m ⟶
     (∃f. field_lookup_list ts f m = Some (s,m+n)))"
  "∀s m n. wf_desc_tuple x ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m ⟶
     (∃f. field_lookup_tuple x f m = Some (s,m+n)))"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case    
    apply clarsimp
    subgoal for s m n
      apply(cases s, clarsimp)
      apply (rule conjI)
       apply clarsimp
       apply(rule exI [where x="[]"])
       apply clarsimp+
      apply((erule allE)+, erule (1) impE)
      apply clarsimp
      subgoal for _ _ _ f
        apply(cases f, clarsimp+)
        subgoal for x xs
          apply(rule exI [where x="x#xs"])
          apply clarsimp
          done
        done
      done
    done
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(rule conjI, clarsimp)
     apply((erule allE)+, erule (1) impE)
     apply(clarsimp) 

    subgoal for s m n f
      apply (cases f, clarsimp+)
      subgoal for x xs
        apply(rule exI [where x="x#xs"])
        apply(clarsimp)
        done
      done
    apply clarsimp
    subgoal premises prems for s m n
      using prems(1-3,6 ) 
        prems(5)[rule_format, of s "m + size_td (dt_fst dt_tuple)" "n - size_td (dt_fst dt_tuple)"]
      apply -
      apply(frule td_set_list_offset_le)
      apply clarsimp
      subgoal for f
        apply(rule exI [where x=f])
        apply(clarsimp split: option.splits)
        apply(cases dt_tuple, clarsimp split: if_split_asm)
        apply(cases f, clarsimp+)
        apply(simp add: field_lookup_list_None)
        done
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case   
    apply clarsimp
    apply((erule allE)+, erule (1) impE)
    apply clarsimp
    subgoal for s m n f
      apply(rule exI [where x="list#f"])
      apply clarsimp
      done
    done
qed

lemma td_set_field_lookup':
  "(∀s m n. wf_desc t ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set t m ⟶
      (∃f. field_lookup t f m = Some (s,m+n)))) ∧
    (∀s m n. wf_desc_struct st ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m ⟶
      (∃f. field_lookup_struct st f m = Some (s,m+n)))) ∧
    (∀s m n. wf_desc_list ts ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m ⟶
      (∃f. field_lookup_list ts f m = Some (s,m+n)))) ∧
    (∀s m n. wf_desc_tuple x ⟶ (((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m ⟶
      (∃f. field_lookup_tuple x f m = Some (s,m+n))))"
  by (auto simp: td_set_field_lookup'')


lemma td_set_field_lookup_rev'':
  "∀s m n. (∃f. field_lookup t f m = Some (s,m+n)) ⟶
     ((s::('a,'b) typ_desc),m + n) ∈ td_set t m"
  "∀s m n. (∃f. field_lookup_struct st f m = Some (s,m+n)) ⟶
     ((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m"
  "∀s m n. (∃f. field_lookup_list ts f m = Some (s,m+n)) ⟶
     ((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m"
  "∀s m n. (∃f. field_lookup_tuple x f m = Some (s,m+n)) ⟶
     ((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case        
    apply clarsimp
    subgoal for s m n f
      apply(cases f, clarsimp)
      apply clarsimp
      apply((erule allE)+, erule impE, fast)
      apply fast
      done
    done
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(clarsimp split: option.splits)
    subgoal premises prems for s m n f
      using prems (1, 4-5)
        prems(3)[rule_format, where s = s and m = "m + size_td (dt_fst dt_tuple)" and n= "n - size_td (dt_fst dt_tuple)"]
      apply -

      apply(frule field_lookup_offset_le)
      apply clarsimp
      apply fast
      done
    subgoal by auto 
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case   
    apply clarsimp
    subgoal for s m n f
      apply(cases f, clarsimp+)
      apply((erule allE)+, erule impE, fast)
      apply assumption
      done
    done
qed

lemma td_set_field_lookup_rev':
  "(∀s m n. (∃f. field_lookup t f m = Some (s,m+n)) ⟶
      ((s::('a,'b) typ_desc),m + n) ∈ td_set t m) ∧
    (∀s m n. (∃f. field_lookup_struct st f m = Some (s,m+n)) ⟶
      ((s::('a,'b) typ_desc),m + n) ∈ td_set_struct st m) ∧
    (∀s m n. (∃f. field_lookup_list ts f m = Some (s,m+n)) ⟶
      ((s::('a,'b) typ_desc),m + n) ∈ td_set_list ts m) ∧
    (∀s m n. (∃f. field_lookup_tuple x f m = Some (s,m+n)) ⟶
      ((s::('a,'b) typ_desc),m + n) ∈ td_set_tuple x m)"
  by (auto simp: td_set_field_lookup_rev'')

lemma td_set_field_lookup:
  "wf_desc t ⟹ k ∈ td_set t 0 = (∃f. field_lookup t f 0 = Some k)"
  using td_set_field_lookup' [of t undefined undefined undefined]
        td_set_field_lookup_rev' [of t undefined undefined undefined]
  apply clarsimp
  apply(cases k, clarsimp)
  by (metis add_0)

lemma td_set_field_lookupD:
  "field_lookup t f m = Some k ⟹ k ∈ td_set t m"
  using td_set_field_lookup_rev' [of t undefined undefined undefined]
  apply(cases k, clarsimp)
  by (metis field_lookup_offset_le(1) le_iff_add)

lemma td_set_struct_field_lookup_structD:
  "field_lookup_struct st f m = Some k ⟹ k ∈ td_set_struct st m"
  using td_set_field_lookup_rev' [of undefined st undefined undefined]
  apply(cases k, clarsimp)
  by (metis field_lookup_offset_le(2) le_iff_add)

lemma field_lookup_struct_td_simp [simp]:
  "field_lookup_struct ts f m ≠ Some (TypDesc algn ts nm, m)"
  by (fastforce dest: td_set_struct_field_lookup_structD td_set_struct_size_lte)


lemma td_set_list_field_lookup_listD:
  "field_lookup_list xs f m = Some k ⟹ k ∈ td_set_list xs m"
  using td_set_field_lookup_rev' [of undefined undefined xs undefined]
  apply(cases k, clarsimp)
  by (metis field_lookup_offset_le(3) le_Suc_ex)

lemma td_set_tuple_field_lookup_tupleD:
  "field_lookup_tuple x f m = Some k ⟹ k ∈ td_set_tuple x m"
  using td_set_field_lookup_rev' [of undefined undefined undefined x]
  apply(cases k, clarsimp)
  by (metis field_lookup_offset_le(4) nat_le_iff_add)

lemma field_lookup_offset_size'':
  "field_lookup t f n = Some (u, m) ⟹ size_td u + m ≤ size_td t + n"
  by (metis Nat.add_diff_assoc field_lookup_offset_le(1)
            le_diff_conv td_set_field_lookupD td_set_offset_size')

lemma field_lookup_offset_size':
  assumes n: "field_lookup t f 0 = Some (t',n)" shows "size_td t' + n ≤ size_td t"
  using field_lookup_offset_size''[OF n] by simp

lemma intvl_subset_of_field_lookup:
  "field_lookup t f 0 = Some (u, n) ⟹
    {a + of_nat n ..+ size_td u} ⊆ {a ..+ size_td t}"
  by (simp add: field_lookup_offset_size' intvl_le)

lemma field_lookup_wf_size_desc_gt:
  "⟦ field_lookup t f n = Some (a,b); wf_size_desc t ⟧ ⟹ 0 < size_td a"
  by (fastforce simp: td_set_wf_size_desc wf_size_desc_gt dest!: td_set_field_lookupD)

lemma field_lookup_inject'':
  "∀f g m s. wf_size_desc t ⟶ field_lookup (t::('a,'b) typ_desc) f m = Some s ∧ field_lookup t g m = Some s ⟶ f=g"
  "∀f g m s. wf_size_desc_struct st ⟶ field_lookup_struct (st::('a,'b) typ_struct) f m = Some s ∧ field_lookup_struct  st g m = Some s ⟶ f=g"
  "∀f g m s. wf_size_desc_list ts ⟶ field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some s ∧ field_lookup_list ts g m = Some s ⟶ f=g"
  "∀f g m s. wf_size_desc_tuple x ⟶ field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some s ∧ field_lookup_tuple x g m = Some s ⟶ f=g"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by clarsimp fast
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
    subgoal for f g m a b
      apply(clarsimp split: option.splits)
         apply fast
      subgoal
        apply(frule td_set_tuple_field_lookup_tupleD)
        apply(drule field_lookup_offset_le)
        apply(drule td_set_tuple_offset_size_m)
        subgoal premises prems
          using prems(3-8)
          apply(cases dt_tuple, simp)
          subgoal premises prems
          proof -
            have "0 < size_td a"
              using prems
              apply -
              apply(clarsimp split: if_split_asm; drule (2) field_lookup_wf_size_desc_gt)
              done
            then show ?thesis
              using prems
              by simp
          qed
          done
        done
      subgoal
        apply(frule td_set_tuple_field_lookup_tupleD)
        apply(drule field_lookup_offset_le)
        apply(drule td_set_tuple_offset_size_m)
        subgoal premises prems
          using prems(3-8)
          apply(cases dt_tuple, simp)
          subgoal premises prems
          proof -
            have "0 < size_td a"
              using prems
              apply -
              apply(clarsimp split: if_split_asm; drule (2) field_lookup_wf_size_desc_gt)
              done
            then show ?thesis
              using prems
              by simp
          qed
          done
        done   
      subgoal by best
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply clarsimp
    subgoal for f g m a b
      apply(drule spec [where x="tl f"])
      apply(drule spec [where x="tl g"])
      apply(cases f; simp)
      apply(cases g; simp)
      apply fastforce
      done
    done
qed

lemma field_lookup_inject':
  "(∀f g m s. wf_size_desc t ⟶ field_lookup (t::('a,'b) typ_desc) f m = Some s ∧ field_lookup t g m = Some s ⟶ f=g) ∧
      (∀f g m s. wf_size_desc_struct st ⟶ field_lookup_struct (st::('a,'b) typ_struct) f m = Some s ∧ field_lookup_struct  st g m = Some s ⟶ f=g) ∧
      (∀f g m s. wf_size_desc_list ts ⟶ field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some s ∧ field_lookup_list ts g m = Some s ⟶ f=g) ∧
      (∀f g m s. wf_size_desc_tuple x ⟶ field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some s ∧ field_lookup_tuple x g m = Some s ⟶ f=g)"
  by (auto simp: field_lookup_inject'')


lemma field_lookup_inject:
  "⟦ field_lookup (t::('a,'b) typ_desc) f m = Some s;
      field_lookup t g m = Some s; wf_size_desc t ⟧ ⟹ f=g"
  using field_lookup_inject' [of t undefined undefined undefined]
  apply(cases s)
  apply clarsimp
  apply(drule spec [where x=f])
  apply(drule spec [where x=g])
  apply fast
  done

lemma fd_cons_update_normalise:
  "⟦ fd_cons_update_access d n; fd_cons_access_update d n;
        fd_cons_double_update d; fd_cons_length d n ⟧ ⟹
        fd_cons_update_normalise d n"
  apply(clarsimp simp: fd_cons_update_access_def fd_cons_update_normalise_def norm_desc_def)
  subgoal for v bs
    apply(drule spec [where x="field_update d bs v"])
    apply(drule spec [where x="replicate (length bs) 0"])
    apply clarsimp
    apply(clarsimp simp: fd_cons_access_update_def)
    apply(drule spec [where x=bs])
    apply clarsimp
    apply(drule spec [where x="replicate (length bs) 0"])
    apply clarsimp
    apply(drule spec [where x=v])
    apply(drule spec [where x=undefined])
    apply clarsimp
    apply(clarsimp simp: fd_cons_double_update_def)
    apply(drule spec [where x="v"])
    apply(drule spec [where x="field_access d (field_update d bs undefined)
                                    (replicate (length bs) 0)"])
    apply(drule spec [where x=bs])
    apply clarsimp
    apply(erule impE)
     apply(clarsimp simp: fd_cons_length_def)
    apply clarsimp
    done
  done

lemma update_ti_t_update_ti_struct_t [simp]:
  "update_ti_t (TypDesc algn st tn) = update_ti_struct_t st"
  by (auto simp: update_ti_t_def update_ti_struct_t_def)

lemma fd_cons_fd_cons_struct [simp]:
  "fd_cons (TypDesc algn st tn) = fd_cons_struct st"
  by (clarsimp simp: fd_cons_def fd_cons_struct_def)

lemma update_ti_struct_t_update_ti_list_t [simp]:
  "update_ti_struct_t (TypAggregate ts) = update_ti_list_t ts"
  by (auto simp: update_ti_struct_t_def update_ti_list_t_def)

lemma fd_cons_struct_fd_cons_list [simp]:
  "fd_cons_struct (TypAggregate ts) = fd_cons_list ts"
  by (clarsimp simp: fd_cons_struct_def fd_cons_list_def)

lemma fd_cons_list_empty [simp]:
  "fd_cons_list []"
  by (clarsimp simp: fd_cons_list_def fd_cons_double_update_def
    fd_cons_update_access_def fd_cons_access_update_def fd_cons_length_def
    fd_cons_update_normalise_def update_ti_list_t_def fd_cons_desc_def)

lemma fd_cons_double_update_list_append:
  "⟦ fd_cons_double_update (field_desc_list xs);
      fd_cons_double_update (field_desc_list ys);
      fu_commutes (field_update (field_desc_list xs)) (field_update (field_desc_list ys)) ⟧ ⟹
      fd_cons_double_update (field_desc_list (xs@ys))"
  by (auto simp: fd_cons_double_update_def fu_commutes_def)

lemma fd_cons_update_access_list_append:
  "⟦ fd_cons_update_access (field_desc_list xs) (size_td_list xs);
      fd_cons_update_access (field_desc_list ys) (size_td_list ys);
      fd_cons_length (field_desc_list xs) (size_td_list xs);
      fd_cons_length (field_desc_list ys) (size_td_list ys) ⟧ ⟹
      fd_cons_update_access (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
 by (auto simp: fd_cons_update_access_def fd_cons_length_def access_ti_append)

(* fixme MOVE *)
lemma min_ll:
  "min (x + y) x = (x::nat)"
  by simp

lemma fd_cons_access_update_list_append:
  "⟦ fd_cons_access_update (field_desc_list xs) (size_td_list xs);
      fd_cons_access_update (field_desc_list ys) (size_td_list ys);
      fu_commutes (field_update (field_desc_list xs)) (field_update (field_desc_list ys)) ⟧ ⟹
      fd_cons_access_update (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
  apply(clarsimp simp: fd_cons_access_update_def)
  subgoal for bs bs' v v'
    apply(drule spec [where x="take (size_td_list xs) bs"])
    apply clarsimp
    apply(simp add: access_ti_append)
    apply(drule spec [where x="drop (size_td_list xs) bs"])
    apply clarsimp
    apply(drule spec [where x="take (size_td_list xs) bs'"])
    apply(simp add: min_ll)
    apply(drule spec [where x="update_ti_list_t ys (drop (size_td_list xs) bs) v"])
    apply(drule spec [where x="update_ti_list_t ys (drop (size_td_list xs) bs) v'"])
    apply simp
    apply(frule fu_commutes[where bs="take (size_td_list xs) bs" and
        bs'="drop (size_td_list xs) bs" and v=v ])
    apply clarsimp
    apply(frule fu_commutes[where bs="take (size_td_list xs) bs" and
        bs'="drop (size_td_list xs) bs" and v=v'])
    apply clarsimp
    done
  done

lemma fd_cons_length_list_append:
  "⟦ fd_cons_length (field_desc_list xs) (size_td_list xs);
     fd_cons_length (field_desc_list ys) (size_td_list ys) ⟧ ⟹
   fd_cons_length (field_desc_list (xs@ys)) (size_td_list (xs@ys))"
  by (auto simp: fd_cons_length_def access_ti_append)

lemma wf_fdp_insert:
  "wf_fdp (insert x xs) ⟹ wf_fdp {x} ∧ wf_fdp xs"
  by (auto simp: wf_fdp_def)

lemma wf_fdp_fd_cons:
  "⟦ wf_fdp X; (t,m) ∈ X ⟧ ⟹ fd_cons t"
  by (auto simp: wf_fdp_def)

lemma wf_fdp_fu_commutes:
  "⟦ wf_fdp X; (s,m) ∈ X; (t,n) ∈ X; ¬ m ≤ n; ¬ n ≤ m ⟧ ⟹
      fu_commutes (field_update (field_desc s)) (field_update (field_desc t))"
  by (auto simp: wf_fdp_def)

lemma wf_fdp_fa_fu_ind:
  "⟦ wf_fdp X; (s,m) ∈ X; (t,n) ∈ X; ¬ m ≤ n; ¬ n ≤ m ⟧ ⟹
      fa_fu_ind (field_desc s) (field_desc t) (size_td t) (size_td s)"
  by (auto simp: wf_fdp_def)

lemma wf_fdp_mono:
  "⟦ wf_fdp Y; X ⊆ Y ⟧ ⟹ wf_fdp X"
  by (fastforce simp: wf_fdp_def)

lemma tf0 [simp]:
  "tf_set (TypDesc algn st nm) = {(TypDesc algn st nm,[])} ∪ tf_set_struct st"
  by (auto simp: tf_set_def tf_set_struct_def)

lemma tf1 [simp]:  "tf_set_struct (TypScalar m algn d) = {}"
  by (clarsimp simp: tf_set_struct_def)

lemma tf2 [simp]:  "tf_set_struct (TypAggregate xs) = tf_set_list xs"
  by (auto simp: tf_set_struct_def tf_set_list_def)

lemma tf3 [simp]:  "tf_set_list [] = {}"
  by (simp add: tf_set_list_def)

lemma tf4:  "tf_set_list (x#xs) = tf_set_tuple x ∪ {t. t ∈ tf_set_list xs ∧ snd t ∉  snd ` tf_set_tuple x}"
  apply(clarsimp simp: tf_set_list_def tf_set_tuple_def)
  apply(cases x)
  apply clarsimp
  subgoal for x1 a b
    apply(rule equalityI; clarsimp)
    subgoal for a' b'
      apply(cases b'; clarsimp)
      apply(erule disjE; clarsimp?)
      apply(fastforce dest: field_lookup_list_offset2 split: option.splits)[1]
      done
    apply (rule conjI; clarsimp)
    subgoal for   _ ys n
      apply(cases ys; clarsimp split: option.splits)
      apply(rule conjI; clarsimp simp: image_def)
       apply(drule field_lookup_list_offset3[where  m="size_td x1"])
       apply fast
      apply(drule field_lookup_list_offset3[where  m="size_td x1"])
      apply fast
      done
    done
  done

lemma tf4D:
  "t ∈ tf_set_list (x#xs) ⟹ t ∈ (tf_set_tuple x ∪ tf_set_list xs)"
  by (clarsimp simp: tf4)

lemma tf4' [simp]:  "wf_desc_list (x#xs) ⟹
  tf_set_list (x#xs) = tf_set_tuple x ∪ tf_set_list xs"
  apply(simp add: tf4)
  apply(rule equalityI; clarsimp)
  subgoal for _ _ ys
  apply(clarsimp simp: tf_set_tuple_def tf_set_list_def)
  apply(cases x, simp)
  apply(clarsimp split: if_split_asm)
    apply(cases ys; simp)
    subgoal for _ _ _ _ _ list
      apply(drule field_lookup_list_None [where fs=list and m=0])
      apply fastforce
      done
    done
  done

lemma tf5 [simp]:  "tf_set_tuple (DTuple t m d) = {(a,m#b) | a b. (a,b) ∈ tf_set t}"
  apply(clarsimp simp: tf_set_tuple_def tf_set_def)
  apply(rule equalityI; clarsimp)
  subgoal for _ xs n
  apply(cases xs; clarsimp)
    done
  done

lemma tf_set_self [simp]:
  "(t,[]) ∈ tf_set t"
  by (clarsimp simp: tf_set_def)


lemma tf_set_list_mem:
  "wf_desc_list ts ⟹  DTuple t n d ∈ set ts ⟹ (t,[n]) ∈ tf_set_list ts"
  by (induct ts) auto

lemma tf_set_list_append:
  "wf_desc_list (xs@ys) ⟹ tf_set_list (xs@ys) = tf_set_list xs ∪ tf_set_list ys"
  apply(induct xs; clarsimp)
  apply(subst tf4'; fastforce)
  done

lemma lf_set_list_append [simp]:
  "lf_set_list (xs@ys) fn = lf_set_list xs fn ∪ lf_set_list ys fn"
  by (induct xs) auto

lemma ti_ind_sym:
  "ti_ind X Y ⟹ ti_ind Y X"
  by (auto simp: ti_ind_def fu_commutes_def)

lemma ti_ind_sym2:
  "ti_ind X Y = ti_ind Y X"
  by (blast dest: ti_ind_sym)

lemma ti_ind_list [simp]:
  "ti_ind (X ∪ Y) Z = (ti_ind X Z ∧ ti_ind Y Z)"
  unfolding ti_ind_def by auto

lemma ti_empty [simp]:
  "ti_ind {} X"
  by (simp add: ti_ind_def)

lemma wf_lf_list:
  "lf_fn ` X ∩ lf_fn ` Y = {} ⟹
      wf_lf (X ∪ Y) = (wf_lf X ∧ wf_lf Y ∧ ti_ind X Y)"
  unfolding wf_lf_def ti_ind_def field_desc_def fu_commutes_def
  apply (rule iffI; clarsimp)
  subgoal for x y
   apply(frule spec [where x=x])
   apply(drule spec [where x=y])
   apply clarsimp
   apply(drule spec [where x=y])
   apply(drule spec [where x=x])
   apply clarsimp
    apply fastforce
    done
  subgoal by fast
  done

lemma wf_lf_listD:
  "wf_lf (X ∪ Y) ⟹ wf_lf X ∧ wf_lf Y"
  unfolding wf_lf_def ti_ind_def field_desc_def fu_commutes_def by clarsimp

lemma ti_ind_fn:
  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
  "∀fn. ti_ind (lf_set t fn) Y = ti_ind (lf_set t []) Y"
  "∀fn. ti_ind (lf_set_struct st fn) Y = ti_ind (lf_set_struct st []) Y"
  "∀fn. ti_ind (lf_set_list ts fn) Y = ti_ind (lf_set_list ts []) Y"
  "∀fn. ti_ind (lf_set_tuple x fn) Y = ti_ind (lf_set_tuple x []) Y"
  apply(induct t and st and ts and x, all ‹clarsimp›)
    apply (fastforce simp: ti_ind_def)
   apply auto
  done

lemma ti_ind_ld_td':
  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
  "ti_ind (lf_set t []) Y ⟶ ti_ind {t2d (t,[])} Y"
  "ti_ind (lf_set_struct st []) Y ⟶ ti_ind {⦇ lf_fd = field_desc_struct st, lf_sz = size_td_struct st, lf_fn = [] ⦈} Y"
  "ti_ind (lf_set_list ts []) Y ⟶ ti_ind {⦇ lf_fd = field_desc_list ts, lf_sz = size_td_list ts, lf_fn = [] ⦈} Y"
  "ti_ind (lf_set_tuple x []) Y ⟶ ti_ind {⦇ lf_fd = field_desc_tuple x, lf_sz = size_td_tuple x, lf_fn = [] ⦈} Y"
  apply(induct t and st and ts and x, all ‹clarsimp simp: t2d_def›)
     apply((clarsimp simp: ti_ind_def fu_commutes_def fa_fu_ind_def)+)[3]
  apply(subst (asm) ti_ind_fn)
  apply simp
  done

lemma ti_ind_ld_td_struct:
  "ti_ind (lf_set_struct st fn) Y ⟹
   ti_ind {⦇ lf_fd = field_desc_struct st, lf_sz = size_td_struct st, lf_fn = [] ⦈} Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld_td')

lemma ti_ind_ld_td_list:
  "ti_ind (lf_set_list ts fn) Y ⟹
   ti_ind {⦇ lf_fd = field_desc_list ts, lf_sz = size_td_list ts, lf_fn = [] ⦈} Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld_td')

lemma ti_ind_ld_td_tuple:
  "ti_ind (lf_set_tuple x fn) Y ⟹
   ti_ind {⦇ lf_fd = field_desc_tuple x, lf_sz = size_td_tuple x, lf_fn = [] ⦈} Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld_td')

lemma ti_ind_ld':
  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
  "ti_ind (lf_set t []) Y ⟶ ti_ind (t2d ` (tf_set t)) Y"
  "ti_ind (lf_set_struct st []) Y ⟶ ti_ind (t2d ` (tf_set_struct st)) Y"
  "ti_ind (lf_set_list ts []) Y ⟶ ti_ind (t2d ` (tf_set_list ts)) Y"
  "ti_ind (lf_set_tuple x []) Y ⟶ ti_ind (t2d ` (tf_set_tuple x)) Y"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case 
    apply clarsimp
    apply(frule ti_ind_ld_td_struct)
    apply(subst insert_def)
    apply(subst ti_ind_list)
    apply(clarsimp simp: ti_ind_def t2d_def)
    done
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(clarsimp simp: ti_ind_def t2d_def)
   apply(drule tf4D)
    apply clarsimp
    by (smt (verit, best) field_desc.select_convs(2) fst_eqD image_eqI 
        leaf_desc.select_convs(1) leaf_desc.select_convs(2))
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply clarsimp
    apply(subst (asm) (2) ti_ind_fn)
    apply(simp add: t2d_def)
    apply(clarsimp simp: ti_ind_def)
    by (metis (mono_tags, lifting) field_desc.select_convs(2) fst_conv image_eqI 
        leaf_desc.select_convs(1) leaf_desc.select_convs(2))
qed

lemma ti_ind_ld:
  "ti_ind (lf_set t fn) Y ⟹ ti_ind (t2d ` (tf_set t)) Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld')

lemma ti_ind_ld_struct:
  "ti_ind (lf_set_struct t fn) Y ⟹ ti_ind (t2d ` (tf_set_struct t)) Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld')

lemma ti_ind_ld_list:
  "ti_ind (lf_set_list t fn) Y ⟹ ti_ind (t2d ` (tf_set_list t)) Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld')

lemma ti_ind_ld_tuple:
  "ti_ind (lf_set_tuple t fn) Y ⟹ ti_ind (t2d ` (tf_set_tuple t)) Y"
  by (subst (asm) ti_ind_fn) (simp only: ti_ind_ld')

lemma lf_set_fn':
  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
  "∀s fn. s ∈ lf_set t fn ⟶ fn ≤ lf_fn s"
  "∀s fn. s ∈ lf_set_struct st fn ⟶ fn ≤ lf_fn s"
  "∀s fn. s ∈ lf_set_list ts fn ⟶ fn ≤ lf_fn s"
  "∀s fn. s ∈ lf_set_tuple x fn ⟶ fn ≤ lf_fn s"
proof (induct t and st and ts and x)
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply clarsimp
    subgoal for s fn
      apply(drule spec [where x=s])
      apply(drule spec [where x="fn @ [list]"])
      apply(clarsimp simp: prefix_def less_eq_list_def)
      done
    done
qed auto

lemma lf_set_fn:
  "s ∈ lf_set (t::('a,'b) typ_info) fn ⟹ fn ≤ lf_fn s"
  by (clarsimp simp: lf_set_fn')

lemma ln_fn_disj:
  "dt_snd x ∉ dt_snd ` set xs ⟹ lf_fn ` lf_set_tuple x fn ∩ lf_fn ` lf_set_list xs fn = {}"
  apply (induct xs arbitrary: x; clarsimp)
  apply (rule set_eqI, clarsimp)
  apply (erule disjE)
   apply (clarsimp dest!: lf_set_fn simp: split_DTuple_all prefix_def less_eq_list_def)
  apply fastforce
  done

lemma wf_lf_fn:
  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
  "∀fn. wf_desc t ⟶ wf_lf (lf_set t fn) = wf_lf (lf_set t [])"
  "∀fn. wf_desc_struct st ⟶ wf_lf (lf_set_struct st fn) = wf_lf (lf_set_struct  st [])"
  "∀fn. wf_desc_list ts ⟶ wf_lf (lf_set_list ts fn) = wf_lf (lf_set_list ts [])"
  "∀fn. wf_desc_tuple x ⟶ wf_lf (lf_set_tuple x fn) = wf_lf (lf_set_tuple x [])"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case        
    apply clarify
    subgoal for fn
      apply(drule spec [where x=fn])
      apply clarsimp
      done
    done
next
  case (TypScalar nat1 nat2 a)
  then show ?case       
    apply clarsimp
    apply(clarsimp simp: wf_lf_def)
    done
next
  case (TypAggregate list)
  then show ?case 
    apply clarify
    subgoal for fn
     apply(drule spec [where x=fn])
    apply clarsimp
      done
    done
next
  case Nil_typ_desc
  then show ?case by clarsimp   
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case  
    apply clarify
    subgoal for fn
      apply(drule spec [where x=fn])+
      apply clarsimp
      apply(subst wf_lf_list)
       apply(erule ln_fn_disj)
      apply(subst wf_lf_list)
       apply(erule ln_fn_disj)
      apply clarsimp
      apply(subst ti_ind_fn)
      apply(subst ti_ind_sym2)
      apply(subst ti_ind_fn)
      apply(subst ti_ind_sym2)
      apply(clarsimp)
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply clarify
    subgoal for fn
      apply(frule spec [where x="[list]"])
      apply(drule spec [where x="fn@[list]"])
      apply clarsimp
      done
    done
qed

lemma wf_lf_fd_cons':
  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
  "∀m. wf_lf (lf_set t []) ⟶ wf_desc t ⟶ fd_cons t"
  "∀m. wf_lf (lf_set_struct st []) ⟶ wf_desc_struct st ⟶ fd_cons_struct st"
  "∀m. wf_lf (lf_set_list ts []) ⟶ wf_desc_list ts ⟶ fd_cons_list ts"
  "∀m. wf_lf (lf_set_tuple x []) ⟶ wf_desc_tuple x ⟶ fd_cons_tuple x"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by clarsimp
next
  case (TypScalar nat1 nat2 a)
  then show ?case       
    apply(clarsimp simp: wf_lf_def fd_cons_struct_def fd_cons_def)
      apply(clarsimp simp: fd_cons_desc_def fd_cons_double_update_def fd_cons_update_access_def
                           fd_cons_access_update_def fd_cons_length_def)
    done
next
  case (TypAggregate list)
  then show ?case by clarsimp
next
  case Nil_typ_desc
  then show ?case by clarsimp
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case
   apply clarsimp
   apply(subst (asm) wf_lf_list)
    apply(erule ln_fn_disj)
   apply clarsimp
   apply(drule ti_ind_ld_td_tuple)
   apply(drule ti_ind_sym)
   apply(drule ti_ind_ld_td_list)
   apply(drule ti_ind_sym)
   apply(clarsimp simp: ti_ind_def)
   apply(clarsimp simp: fd_cons_list_def fd_cons_desc_def)
   apply(rule conjI)
    apply(clarsimp simp: fd_cons_tuple_def fd_cons_double_update_def fd_cons_desc_def)
    apply(simp add: fu_commutes_def)
   apply(rule conjI)
    apply(clarsimp simp: fd_cons_tuple_def fd_cons_update_access_def fd_cons_desc_def)
    apply(clarsimp simp: fd_cons_length_def)
   apply(rule conjI)
    apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def)
     apply(clarsimp simp: fd_cons_access_update_def)
    subgoal for bs bs' v v'
    apply(simp add: fu_commutes_def)
      apply(clarsimp simp: fa_fu_ind_def)
      subgoal premises prems
        using prems (1-14, 16-18)
          prems (15)[rule_format, where bs'= "take (size_td_tuple dt_tuple) bs'" and 
            bs= "take (size_td_tuple dt_tuple) bs" and v="v" and v'="v'" ]
        apply -
        apply(simp add: min_ll)
        done
      done
    apply(clarsimp simp: fd_cons_length_def fd_cons_tuple_def fd_cons_desc_def)
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case   
    apply clarsimp
  apply(subst (asm) (2) wf_lf_fn, assumption)
  apply(clarsimp simp: fd_cons_def fd_cons_tuple_def export_uinfo_def)
  done
qed

lemma wf_lf_fd_cons:
  "⟦ wf_lf (lf_set t fn); wf_desc t ⟧ ⟹ fd_cons t"
  by (subst (asm) wf_lf_fn; simp only: wf_lf_fd_cons')

lemma wf_lf_fd_cons_struct:
  "⟦ wf_lf (lf_set_struct t fn); wf_desc_struct t ⟧ ⟹ fd_cons_struct t"
  by (subst (asm) wf_lf_fn; simp only: wf_lf_fd_cons')

lemma wf_lf_fd_cons_list:
  "⟦ wf_lf (lf_set_list t fn); wf_desc_list t ⟧ ⟹ fd_cons_list t"
  by (subst (asm) wf_lf_fn; simp only: wf_lf_fd_cons')

lemma wf_lf_fd_cons_tuple:
  "⟦ wf_lf (lf_set_tuple t fn); wf_desc_tuple t ⟧ ⟹ fd_cons_tuple t"
  by (subst (asm) wf_lf_fn; simp only: wf_lf_fd_cons')


lemma wf_lf_fdp':
  "∀m. wf_lf (lf_set (t::('a,'b) typ_info) []) ⟶ wf_desc t ⟶ wf_fdp (tf_set t)"
  "∀m. wf_lf (lf_set_struct (st::('a,'b) typ_info_struct) []) ⟶ wf_desc_struct st ⟶ wf_fdp (tf_set_struct st)"
  "∀m. wf_lf (lf_set_list (ts::('a,'b) typ_info_tuple list) []) ⟶ wf_desc_list ts ⟶ wf_fdp (tf_set_list ts)"
  "∀m. wf_lf (lf_set_tuple (x::('a,'b) typ_info_tuple) []) ⟶ wf_desc_tuple x ⟶ wf_fdp (tf_set_tuple x)"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case 
    apply (clarsimp simp: wf_fdp_def)
    apply (fastforce elim: wf_lf_fd_cons_struct)
    done
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: wf_fdp_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: wf_fdp_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: wf_fdp_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: wf_fdp_def)
    apply(subst (asm) wf_lf_list)
     apply(erule ln_fn_disj)
    apply clarsimp
    apply(drule ti_ind_ld_tuple)
    apply(drule ti_ind_sym)
    apply(drule ti_ind_ld_list)
    apply(drule ti_ind_sym)
    apply(rule conjI, clarsimp)
     apply(erule disjE, fast)
     apply(clarsimp simp: ti_ind_def t2d_def)
    subgoal for x m y n
      apply(drule spec [where x="t2d (x,m)"])
      apply(drule spec [where x="t2d (y,n)"])
      apply(clarsimp simp: t2d_def image_def)
      apply(erule impE)
       apply(rule conjI)
        apply(rule bexI [where x="(x,m)"])
         apply clarsimp
        apply assumption
       apply(rule bexI [where x="(y,n)"])
        apply clarsimp
       apply assumption
      apply clarsimp
      done

    apply clarsimp
    subgoal for x m y n
      apply(erule disjE)
       apply(clarsimp simp: ti_ind_def t2d_def)
       apply(drule spec [where x="t2d (y,n)"])
       apply(drule spec [where x="t2d (x,m)"])
       apply(clarsimp simp: t2d_def image_def)
       apply(erule impE)
        apply(standard)
         apply(rule bexI [where x="(y,n)"])
          apply clarsimp
         apply assumption
        apply(rule bexI [where x="(x,m)"])
         apply clarsimp
        apply assumption
       apply clarsimp
       apply(clarsimp simp: fu_commutes_def)
      apply fast
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply (clarsimp simp: wf_fdp_def)
  apply(subst (asm) (2) wf_lf_fn, assumption)
  apply(clarsimp simp: wf_fdp_def)
    apply fast
    done
qed

lemma wf_lf_fdp:
  "⟦ wf_lf (lf_set t []); wf_desc t ⟧ ⟹ wf_fdp (tf_set t)"
  by (simp only: wf_lf_fdp')

lemma wf_fd_field_lookup [rule_format]:
  "∀f m n s. wf_fd (t::('a,'b) typ_info) ⟶ field_lookup t f m = Some (s,n) ⟶ wf_fd s"
  "∀f m n s. wf_fd_struct (st::('a,'b) typ_info_struct) ⟶ field_lookup_struct st f m = Some (s,n) ⟶ wf_fd s"
  "∀f m n s. wf_fd_list (ts::('a,'b) typ_info_tuple list) ⟶ field_lookup_list ts f m = Some (s,n) ⟶ wf_fd s"
  "∀f m n s. wf_fd_tuple (x::('a,'b) typ_info_tuple) ⟶ field_lookup_tuple x f m = Some (s,n) ⟶ wf_fd s"
  by (induct t and st and ts and x) (clarsimp split: option.splits)+

lemma wf_fd_field_lookupD:
  "⟦ field_lookup t f m = Some (s,n); wf_fd t ⟧ ⟹ wf_fd s"
  by (rule wf_fd_field_lookup)

lemma wf_fd_tf_set:
  "⟦ wf_fd t; ((s::('a,'b) typ_info),m) ∈ tf_set t ⟧ ⟹ wf_fd s"
  by (fastforce simp: tf_set_def wf_fd_field_lookupD)

lemma tf_set_field_lookupD:
  "field_lookup t f m = Some (s,n) ⟹ (s,f) ∈ tf_set t"
  unfolding tf_set_def
  by (clarsimp simp flip: field_lookup_offset[where m=m] dest!: field_lookup_offset_le) arith

lemma fu_commutes_ts:
  "(⋀ t. t ∈ dt_fst ` set ts ⟹ fu_commutes d (update_ti_t t)) ⟹
      fu_commutes d (update_ti_list_t ts)"
  by (induct ts; clarsimp simp: fu_commutes_def) (clarsimp simp: split_DTuple_all)

lemma fa_fu_ind_ts:
  "(⋀t. t ∈ dt_fst ` set ts ⟹ fa_fu_ind d (field_desc t) (size_td t) n) ⟹
      fa_fu_ind d ⦇ field_access = access_ti_list ts,
              field_update = update_ti_list_t ts, field_sz = size_td_list ts⦈
           (size_td_list ts) n"
  by (induct ts; clarsimp simp: fa_fu_ind_def) (clarsimp simp: split_DTuple_all)

lemma fa_fu_ind_ts2:
  "(⋀t. t ∈ dt_fst ` set ts ⟹ fa_fu_ind (field_desc t) d n (size_td t)) ⟹
      fa_fu_ind ⦇ field_access = access_ti_list ts,
              field_update = update_ti_list_t ts, field_sz = size_td_list ts⦈ d
           n (size_td_list ts)"
  by (induct ts; clarsimp simp: fa_fu_ind_def) (clarsimp simp: split_DTuple_all)

lemma wf_fdp_fd [rule_format]:
  "∀m. wf_fdp (tf_set t) ⟶ wf_desc t ⟶ wf_fd (t::('a,'b) typ_info)"
  "∀m. (case st of TypScalar sz algn d ⇒ fd_cons_struct ((TypScalar sz algn d)::('a,'b) typ_info_struct)
           | _ ⇒ wf_fdp (tf_set_struct st)) ⟶ wf_desc_struct st ⟶ wf_fd_struct (st::('a,'b) typ_info_struct)"
  "∀m. wf_fdp (tf_set_list ts) ⟶ wf_desc_list ts ⟶ wf_fd_list (ts::('a,'b) typ_info_tuple list)"
  "∀m. wf_fdp (tf_set_tuple x) ⟶ wf_desc_tuple x ⟶ wf_fd_tuple (x::('a,'b) typ_info_tuple)"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case  
    apply(clarsimp split: typ_struct.split_asm)
     apply(clarsimp simp: wf_fdp_def fd_cons_def fd_cons_struct_def)
    apply (fastforce dest: wf_fdp_mono)
    done
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 xs)
  then show ?case 
    apply clarsimp
    apply (rule conjI, fastforce dest: wf_fdp_mono)
    apply (rule conjI)
    subgoal
      using wf_fdp_mono
      by blast
    subgoal
      apply(clarsimp simp: wf_fdp_def)
      apply(cases dt_tuple, clarsimp)
      subgoal for a b x3

        apply(frule spec [where x=a])
        apply(drule spec [where x="[b]"])
        apply clarsimp
        apply (rule conjI)
         apply(rule fu_commutes_ts)
         apply clarsimp
        subgoal for x
          apply(drule spec [where x="dt_fst x"], erule impE, rule exI [where  x="[dt_snd x]"])
           apply (metis Prefix_Order.Cons_prefix_Cons dt_tuple.exhaust_sel rev_image_eqI tf_set_list_mem)
          apply simp
          done
        apply(rule conjI)
         apply(rule fa_fu_ind_ts)
         apply clarsimp
        subgoal for x

          apply(drule spec [where x="dt_fst x"], erule impE, rule exI [where x="[dt_snd x]"])
           apply (metis Prefix_Order.Cons_prefix_Cons dt_tuple.exhaust_sel rev_image_eqI tf_set_list_mem)
          apply simp
          done

        apply(rule fa_fu_ind_ts2)
        subgoal for t
          apply(drule spec [where x=t])
          apply clarsimp
          subgoal for x
            apply(cases x, clarsimp)
            subgoal for ba aa
              apply(drule spec [where x="[ba]"])
              apply clarsimp
              apply(simp add: tf_set_list_mem)
              apply clarsimp
              by (metis Prefix_Order.Cons_prefix_Cons dt_tuple.sel(2) imageI tf_set_self)

            done
          done
        done
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply(clarsimp simp: wf_fdp_def)
    subgoal for x m
      apply(drule spec [where x=x])
      apply(drule spec [where x="list#m"])
      apply clarsimp
      subgoal for y n
        apply(drule spec [where x=y])
        apply auto
        done
      done
    done
qed

lemma wf_fdp_fdD:
  "⟦ wf_fdp (tf_set t); wf_desc t ⟧ ⟹ wf_fd (t::('a,'b) typ_info)"
  by (rule wf_fdp_fd)

lemma wf_fdp_fd_listD:
  "⟦ wf_fdp (tf_set_list t); wf_desc_list t ⟧ ⟹ wf_fd_list t"
  by (rule wf_fdp_fd)

lemma fd_consistentD:
  "⟦ field_lookup t f 0 = Some (s,n); fd_consistent t ⟧
      ⟹ fd_cons s"
  by (fastforce simp: fd_consistent_def)

lemma wf_fd_cons_access_update' [rule_format]:
  "wf_fd (t::('a,'b) typ_info) ⟶ fd_cons_access_update (field_desc t) (size_td t)"
  "wf_fd_struct (st::('a,'b) typ_info_struct) ⟶ fd_cons_access_update (field_desc_struct st) (size_td_struct st)"
  "wf_fd_list (ts::('a,'b) typ_info_tuple list) ⟶ fd_cons_access_update (field_desc_list ts) (size_td_list ts)"
  "wf_fd_tuple (x::('a,'b) typ_info_tuple) ⟶ fd_cons_access_update (field_desc_tuple x) (size_td_tuple x)"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp split: typ_struct.splits)
next
  case (TypScalar nat1 nat2 a)
  then show ?case 
    apply (clarsimp split: typ_struct.splits)
    apply(clarsimp simp: fd_cons_access_update_def fd_cons_struct_def fd_cons_desc_def)
    done
next
  case (TypAggregate list)
  then show ?case by (clarsimp split: typ_struct.splits)
next
  case Nil_typ_desc
  then show ?case apply (clarsimp split: typ_struct.splits)
    apply(clarsimp simp: fd_cons_access_update_def)
    done
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp split: typ_struct.splits)
    apply(clarsimp simp: fd_cons_access_update_def)
    apply(simp add: fu_commutes_def)
    apply(clarsimp simp: fa_fu_ind_def)
    by (metis (no_types, lifting) add_diff_cancel_left' length_drop length_take min_ll)
 next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case  by (clarsimp split: typ_struct.splits)
qed

lemma wf_fd_cons_access_updateD:
  "wf_fd t ⟹ fd_cons_access_update (field_desc t) (size_td t)"
  by (rule wf_fd_cons_access_update')

lemma wf_fd_cons_access_update_structD:
  "wf_fd_struct t ⟹ fd_cons_access_update (field_desc_struct t) (size_td_struct t)"
  by (rule wf_fd_cons_access_update')

lemma wf_fd_cons_access_update_listD:
  "wf_fd_list t ⟹ fd_cons_access_update (field_desc_list t) (size_td_list t)"
  by (rule wf_fd_cons_access_update')

lemma wf_fd_cons_access_update_tupleD:
  "wf_fd_tuple t ⟹ fd_cons_access_update (field_desc_tuple t) (size_td_tuple t)"
  by (rule wf_fd_cons_access_update')

lemma wf_fd_norm_tu:
  "∀bs. wf_fd t ⟶ length bs = size_td t ⟶ norm_tu (export_uinfo (t::('a,'b) typ_info)) bs = (access_ti t (update_ti_t t bs undefined) (replicate (size_td t) 0))"
  "∀bs. wf_fd_struct st ⟶ length bs = size_td_struct st ⟶ norm_tu_struct (map_td_struct field_norm (λ_. ()) (st::('a,'b) typ_info_struct)) bs = (access_ti_struct st (update_ti_struct_t st bs undefined) (replicate (size_td_struct st) 0))"
  "∀bs. wf_fd_list ts ⟶ length bs = size_td_list ts ⟶ norm_tu_list (map_td_list field_norm (λ_. ()) (ts::('a,'b) typ_info_tuple list)) bs = (access_ti_list ts (update_ti_list_t ts bs undefined) (replicate (size_td_list ts) 0))"
  "∀bs. wf_fd_tuple x ⟶ length bs = size_td_tuple x ⟶ norm_tu_tuple (map_td_tuple field_norm (λ_. ()) (x::('a,'b) typ_info_tuple)) bs = (access_ti_tuple x (update_ti_tuple_t x bs undefined) (replicate (size_td_tuple x) 0))"
  apply(induct t and st and ts and x, all ‹clarsimp simp: export_uinfo_def›)
   apply(simp add: field_norm_def)
  apply(simp add: fu_commutes_def)
  apply(simp add: fa_fu_ind_def)
  apply(drule wf_fd_cons_access_update_listD)
  apply(clarsimp simp: fd_cons_access_update_def export_uinfo_def min_def)
  done

lemma wf_fd_norm_tuD:
  "⟦ wf_fd t; length bs = size_td t ⟧  ⟹ norm_tu (export_uinfo t) bs =
      (access_ti⇩0 t (update_ti_t t bs undefined))"
  using wf_fd_norm_tu(1) [of t] by (clarsimp simp: access_ti⇩0_def)

lemma wf_fd_norm_tu_structD:
  "⟦ wf_fd_struct t; length bs = size_td_struct t ⟧ ⟹ norm_tu_struct (map_td_struct field_norm (λ_. ()) t) bs =
      (access_ti_struct t (update_ti_struct_t t bs undefined) (replicate (size_td_struct t) 0))"
  using wf_fd_norm_tu(2) [of t] by clarsimp

lemma wf_fd_norm_tu_listD:
  "⟦ wf_fd_list t; length bs = size_td_list t ⟧ ⟹ norm_tu_list (map_td_list field_norm (λ_. ()) t) bs =
      (access_ti_list t (update_ti_list_t t bs undefined) (replicate (size_td_list t) 0))"
  using wf_fd_norm_tu(3) [of t] by clarsimp

lemma wf_fd_norm_tu_tupleD:
  "⟦ wf_fd_tuple t; length bs = size_td_tuple t ⟧ ⟹ norm_tu_tuple (map_td_tuple field_norm (λ_. ()) t) bs =
      (access_ti_tuple t (update_ti_tuple_t t bs undefined) (replicate (size_td_tuple t) 0))"
  using wf_fd_norm_tu(4) [of t] by clarsimp

lemma wf_fd_cons [rule_format]:
  "wf_fd t ⟶ fd_cons (t::('a,'b) typ_info)"
  "wf_fd_struct st ⟶ fd_cons_struct (st::('a,'b) typ_info_struct)"
  "wf_fd_list ts ⟶ fd_cons_list (ts::('a,'b) typ_info_tuple list)"
  "wf_fd_tuple x ⟶ fd_cons_tuple (x::('a,'b) typ_info_tuple)"
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(clarsimp simp: fd_cons_list_def fd_cons_desc_def)
    apply (rule conjI)
     apply(clarsimp simp: fd_cons_tuple_def fd_cons_double_update_def fd_cons_desc_def)
     apply(simp add: fu_commutes_def)
    apply (rule conjI)
     apply(clarsimp simp: fd_cons_tuple_def fd_cons_update_access_def fd_cons_desc_def)
     apply(clarsimp simp: fd_cons_length_def)
    apply (rule conjI)
     apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def)
     apply(clarsimp simp: fd_cons_access_update_def fu_commutes_def fa_fu_ind_def )
     apply (smt (verit) diff_add_inverse length_drop length_take min_ll)
    apply(clarsimp simp: fd_cons_length_def fd_cons_tuple_def  fd_cons_desc_def)
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by(clarsimp simp: fd_cons_def fd_cons_tuple_def export_uinfo_def)
qed

lemma wf_fd_consD:
  "wf_fd t ⟹ fd_cons t"
  by (rule wf_fd_cons)

lemma wf_fd_cons_structD:
  "wf_fd_struct t ⟹ fd_cons_struct t"
  by (rule wf_fd_cons)

lemma wf_fd_cons_listD:
  "wf_fd_list t ⟹ fd_cons_list t"
  by (rule wf_fd_cons)

lemma wf_fd_cons_tupleD:
  "wf_fd_tuple t ⟹ fd_cons_tuple t"
  by (rule wf_fd_cons)

lemma fd_cons_list_append:
  "⟦ wf_fd_list xs; wf_fd_list ys; fu_commutes
      (field_update (field_desc_list xs)) (field_update (field_desc_list ys)) ⟧ ⟹
      fd_cons_list (xs@ys)"
  apply(frule wf_fd_cons_listD)
  apply(frule wf_fd_cons_listD [where t=ys])
  apply(unfold fd_cons_list_def fd_cons_desc_def)
  apply(fastforce intro: fd_cons_double_update_list_append fd_cons_update_access_list_append
                         fd_cons_access_update_list_append fd_cons_length_list_append)
  done


lemma (in wf_type) wf_fd  [simp]:
  "wf_fd (typ_info_t TYPE('a))"
  by (fastforce intro: wf_fdp_fdD wf_lf_fdp wf_lf)

lemma (in wf_type) fd_cons [simp]:
  "fd_consistent (typ_info_t TYPE('a))"
  unfolding fd_consistent_def by (fastforce intro: wf_fd_consD wf_fd_field_lookupD)


lemma (in wf_type) field_lvalue_append [simp]:
  "⟦ field_ti TYPE('a) f = Some t;
      export_uinfo t = typ_uinfo_t TYPE('b::c_type);
      field_ti TYPE('b) g = Some k ⟧ ⟹
          &(((Ptr &((p::'a ptr)→f))::'b ptr)→g) = &(p→f@g)"
  apply(clarsimp simp: field_lvalue_def c_type_class.field_ti_def field_ti_def field_offset_def
                       field_offset_untyped_def typ_uinfo_t_def
                 split: option.splits)
  apply(subst field_lookup_prefix_Some')
    apply(fastforce dest: field_lookup_export_uinfo_Some)
   apply(simp add: export_uinfo_def wf_desc_map)
  apply(drule field_lookup_export_uinfo_Some)
  apply(simp add: export_uinfo_def)
  apply(drule field_lookup_export_uinfo_Some)
  apply(simp add: export_uinfo_def)
  apply (simp add: c_type_class.field_lvalue_def c_type_class.field_offset_def 
        c_type_class.typ_uinfo_t_def export_uinfo_def field_lookup_offset_shift' field_offset_untyped_def)
  done



lemma (in wf_type) field_lvalue_cons_unfold':
― ‹rhs contains additional type variable @{typ 'b}, hence simplifier won't apply this rule›
  "⟦ field_ti TYPE('a) [f] = Some t;
      export_uinfo t = typ_uinfo_t TYPE('b::c_type);
      field_ti TYPE('b) g = Some k ⟧ ⟹
          &(p→f#g) = &(((Ptr &((p::'a ptr)→[f]))::'b ptr)→g)"
  using field_lvalue_append [where f="[f]" and g=g]
  by simp

lemma (in mem_type) field_lvalue_cons_unfold:
  "⟦field_ti TYPE('b) g = Some k;
    export_uinfo t = export_uinfo (typ_info_t TYPE('b::c_type));
    field_ti TYPE('a) [f] = Some t⟧ ⟹
      &(p→f#g) ≡ &(((Ptr &((p::'a ptr)→[f]))::'b ptr)→g)"
  using field_lvalue_cons_unfold' [simplified c_type_class.typ_uinfo_t_def]
  apply -
  apply (rule eq_reflection)
  apply blast
  done

lemma field_access_update_take_drop [rule_format]:
  "∀f s m n bs bs' v. field_lookup t f m = Some (s,m+n) ⟶
      length bs = size_td t ⟶ length bs' = size_td s ⟶ wf_fd t ⟶
      field_access (field_desc s) (field_update (field_desc t) bs v) bs'
          = field_access (field_desc s) (field_update (field_desc s)
              (take (size_td (s::('a,'b) typ_info)) (drop n bs)) undefined) bs'"
  "∀f s m n bs bs' v. field_lookup_struct st f m = Some (s,m+n) ⟶
      length bs = size_td_struct st ⟶ length bs' = size_td s ⟶ wf_fd_struct st ⟶
      field_access (field_desc s) (field_update (field_desc_struct st) bs v) bs'
          = field_access (field_desc s) (field_update (field_desc s)
              (take (size_td (s::('a,'b) typ_info)) (drop n bs)) undefined) bs'"
  "∀f s m n bs bs' v. field_lookup_list ts f m = Some (s,m+n) ⟶
      length bs = size_td_list ts ⟶ length bs' = size_td s ⟶ wf_fd_list ts ⟶
      field_access (field_desc s) (field_update (field_desc_list ts) bs v) bs'
          = field_access (field_desc s) (field_update (field_desc s)
              (take (size_td (s::('a,'b) typ_info)) (drop n bs)) undefined) bs'"
  "∀f s m n bs bs' v. field_lookup_tuple x f m = Some (s,m+n) ⟶
      length bs = size_td_tuple x ⟶ length bs' = size_td s ⟶ wf_fd_tuple x ⟶
      field_access (field_desc s) (field_update (field_desc_tuple x) bs v) bs'
          = field_access (field_desc s) (field_update (field_desc s)
              (take (size_td (s::('a,'b) typ_info)) (drop n bs)) undefined) bs'"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case 
    apply clarsimp   
    apply(fastforce dest!: wf_fd_cons_structD
        simp: fd_cons_struct_def fd_cons_desc_def fd_cons_access_update_def)
    done
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
    subgoal for f s m n bs bs' v
      apply(clarsimp simp: fd_cons_desc_def split: option.splits)
       apply(cases f; clarsimp)
      subgoal premises prems for a lista
        using prems (1-7, 10-12)
          prems(9) [rule_format, where f= "a#lista" and s=s and m= "m + size_td (dt_fst dt_tuple)" and n="n - size_td (dt_fst dt_tuple)"] 
        apply clarsimp
        apply(frule field_lookup_offset_le)
        apply simp
        apply(cases dt_tuple, clarsimp simp: fu_commutes_def)
        done
      apply(cases f; clarsimp)
      subgoal for a lista
        apply(drule spec [where x="a#lista"])
        apply(drule spec [where x="s"])
        apply(drule spec [where x="m"])
        apply(drule spec [where x="n"])
        apply clarsimp
        apply(frule field_lookup_offset_le)
        apply simp
        apply(cases dt_tuple, clarsimp)
        apply(clarsimp split: if_split_asm)
        by(fastforce dest: td_set_field_lookupD td_set_offset_size_m simp: ac_simps drop_take min_def)
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by auto
qed


lemma field_access_update_take_dropD:
  "⟦ field_lookup t f m = Some (s,m+n); length bs = size_td t;
      length bs' = size_td s; wf_fd t ⟧ ⟹
      field_access (field_desc s) (field_update (field_desc t) bs v) bs'
          = field_access (field_desc s) (field_update (field_desc s)
              (take (size_td (s::('a,'b) typ_info)) (drop n bs)) undefined) bs'"
  by (rule field_access_update_take_drop)

lemma (in wf_type) fi_fa_consistentD:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (d,n);
      length bs = size_of TYPE('a) ⟧ ⟹
      field_access (field_desc d) (from_bytes bs) (replicate (size_td d) 0) =
      norm_tu (export_uinfo d) (take (size_td d) (drop n bs))"
  apply(clarsimp simp: field_offset_def from_bytes_def size_of_def)
  apply(frule field_lookup_export_uinfo_Some)
  apply(subst wf_fd_norm_tuD)
    apply(fastforce intro: wf_fd_field_lookupD)
   apply(clarsimp simp: min_def split: if_split_asm)
   apply(drule td_set_field_lookupD)
   apply(drule td_set_offset_size)
   apply simp
  apply(frule field_access_update_take_dropD[where v=undefined and m=0 and
                                                   bs'="replicate (size_td d) 0",simplified]; simp?)
  apply(simp add: min_def access_ti⇩0_def)
  done

lemma fi_fu_consistent [rule_format]:
  "∀f m n s bs v w. field_lookup t f m = Some (s,n + m) ⟶ wf_fd t ⟶
      length bs = size_td t ⟶ length v = size_td (s::('a,'b) typ_info) ⟶
      field_update (field_desc t) (super_update_bs v bs n) w =
          field_update (field_desc s) v (field_update (field_desc t) bs w)"
  "∀f m n s bs v w. field_lookup_struct st f m = Some (s,n + m) ⟶ wf_fd_struct st ⟶
      length bs = size_td_struct  st ⟶ length v = size_td (s::('a,'b) typ_info) ⟶
      field_update (field_desc_struct st) (super_update_bs v bs n) w =
          field_update (field_desc s) v (field_update (field_desc_struct  st) bs w)"
  "∀f m n s bs v w. field_lookup_list ts f m = Some (s,n + m) ⟶ wf_fd_list ts ⟶
      length bs = size_td_list ts ⟶ length v = size_td (s::('a,'b) typ_info) ⟶
      field_update (field_desc_list ts) (super_update_bs v bs n) w =
          field_update (field_desc s) v (field_update (field_desc_list ts) bs w)"
  "∀f m n s bs v w. field_lookup_tuple x f m = Some (s,n + m) ⟶ wf_fd_tuple x ⟶
      length bs = size_td_tuple x ⟶ length v = size_td (s::('a,'b) typ_info) ⟶
      field_update (field_desc_tuple x) (super_update_bs v bs n) w =
          field_update (field_desc s) v (field_update (field_desc_tuple x) bs w)"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case 
    apply clarsimp
    apply(drule wf_fd_cons_structD)
    apply(clarsimp simp: fd_cons_struct_def fd_cons_double_update_def super_update_bs_def
        fd_cons_desc_def)
    done
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
    subgoal for f m n s bs v w
      apply(cases f; clarsimp)
      apply(clarsimp simp: fd_cons_desc_def split: option.splits)
       apply(clarsimp simp: fu_commutes_def)
      subgoal premises prems for a lista
        using prems (1-8,11-12)
          prems(10)[rule_format, where f="a#lista" and s= s and m="m + size_td (dt_fst dt_tuple)" 
            and n= "n - size_td (dt_fst dt_tuple)"] 
        apply -
        apply(frule field_lookup_offset_le)
        apply simp
        apply(drule td_set_list_field_lookup_listD)
        apply(drule td_set_list_offset_size_m)
        apply (cases dt_tuple)
        apply(clarsimp simp: drop_super_update_bs take_super_update_bs)
        done
      subgoal for a lista
        apply(simp add: fu_commutes_def)
        by (smt (verit, best) add.commute append_take_drop_id diff_add_inverse2 
            length_append length_super_update_bs length_take min_ll 
            super_update_bs_append_drop_first super_update_bs_append_take_first 
            td_set_offset_size' td_set_tuple_field_lookup_tupleD)
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by auto
qed


lemma fi_fu_consistentD:
  "⟦ field_lookup t f 0 = Some (s,n); wf_fd t; length bs = size_td t;
      length v = size_td s ⟧ ⟹
      field_update (field_desc t) (super_update_bs v bs n) w =
          field_update (field_desc s) v (field_update (field_desc t) bs w)"
  using fi_fu_consistent(1) [of t f 0] by clarsimp

lemma (in wf_type) norm:
  assumes lbs: "length bs = size_of TYPE('a)" 
  shows "from_bytes (norm_bytes TYPE('a) bs) = ((from_bytes bs)::'a)"
proof -
  have "wf_fd (typ_info_t TYPE('a))"
    by simp
  with lbs  show ?thesis 
    apply -
    apply(drule wf_fd_consD)
    apply(simp add: from_bytes_def norm_bytes_def)
    apply(clarsimp simp: fd_cons_def fd_cons_desc_def)
    apply(drule (3) fd_cons_update_normalise)
    apply(fastforce simp: fd_cons_update_normalise_def size_of_def wf_fd_norm_tuD norm_desc_def
        access_ti⇩0_def)
    done
qed

lemma (in wf_type) len:
  "length bs = size_of TYPE('a) ⟹
      length (to_bytes (x::'a) bs) = size_of TYPE('a)"
  apply(simp add: size_of_def to_bytes_def)
  by (metis fd_cons_def fd_cons_desc_def fd_cons_length_def 
      field_desc.simps(1) field_desc_def local.wf_fd wf_fd_consD)


lemma (in wf_type) sz_nzero:
  "0 < size_of (TYPE('a))"
  unfolding size_of_def
  by (simp add: wf_size_desc_gt)

lemma not_disj_fn_empty1 [simp]:
  "¬ disj_fn [] s"
  by (simp add: disj_fn_def)

lemma disj_fn_comm: "disj_fn a b ⟷ disj_fn b a"
  by (auto simp add: disj_fn_def)

lemma disj_fn_append_right: "disj_fn x y ⟹ disj_fn x (y @ z)"
  by (auto simp: disj_fn_def less_eq_list_def prefix_def append_eq_append_conv2)

lemma disj_fn_cons_consI[simp]: "(x = y ⟶ disj_fn a b) ⟹ disj_fn (x # a) (y # b)"
  by (auto simp: disj_fn_def)

lemma fd_path_cons [simp]:
  "f ∉ fs_path (x#xs) = (disj_fn f x ∧ f ∉ fs_path xs)"
  by (auto simp: fs_path_def disj_fn_def)

lemma fu_commutes_lookup_disjD:
  "⟦ field_lookup t f m = Some (d,n); field_lookup t f' m' = Some (d',n');
      disj_fn f f'; wf_fdp (tf_set t) ⟧ ⟹
      fu_commutes (field_update (field_desc (d::('a,'b) typ_info)))
          (field_update (field_desc d'))"
  by (auto simp: disj_fn_def wf_fdp_def dest!: tf_set_field_lookupD)

lemma field_lookup_fa_fu_lhs:
  "∀f m n s d k. field_lookup t f m = Some (s,n) ⟶ fa_fu_ind (field_desc t) d k (size_td t)
      ⟶ wf_fd t ⟶ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s)"
  "∀f m n s d k. field_lookup_struct st f m = Some (s,n) ⟶ fa_fu_ind (field_desc_struct st) d k (size_td_struct st)
      ⟶ wf_fd_struct st ⟶ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s)"
  "∀f m n s d k. field_lookup_list ts f m = Some (s,n) ⟶ fa_fu_ind (field_desc_list ts) d k (size_td_list ts)
      ⟶ wf_fd_list ts ⟶ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s)"
  "∀f m n s d k. field_lookup_tuple x f m = Some (s,n) ⟶ fa_fu_ind (field_desc_tuple x) d k (size_td_tuple x)
      ⟶ wf_fd_tuple x ⟶ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s)"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: fa_fu_ind_def)
    subgoal for  f m n s d v bs bs'
      apply(clarsimp split: option.splits)
      subgoal premises prems 
        using prems (1-8, 10) 
        apply -
        apply (rule 
            prems (9)[rule_format, where f=f and s = s and m = "m + size_td (dt_fst dt_tuple)"
              and n=n and d=d and k="length bs", OF prems(11), simplified])
        subgoal for v ys ys'
          apply(drule spec [where x=v])
          apply(drule spec [where x=ys])
          apply clarsimp
          apply(drule spec [where x="replicate (size_td_tuple dt_tuple) 0 @ ys'"])
          apply clarsimp
          apply(drule wf_fd_cons_tupleD)
          apply(clarsimp simp: fd_cons_tuple_def fd_cons_length_def fd_cons_desc_def)
          done
        subgoal by clarsimp
        subgoal by fast
        done
      subgoal
        apply(drule spec [where x=f])
        apply(drule spec [where x=m])
        apply(drule spec [where x=n])
        apply(drule spec [where x=s])
        apply clarsimp
        apply(drule spec [where x=d])
        apply(drule spec [where x="length bs"])
        apply(erule impE)
         apply clarsimp
        subgoal for  v ys ys'
          apply(drule spec [where x=v])
          apply(drule spec [where x=ys])
          apply clarsimp
          apply(drule spec [where x="ys'@replicate (size_td_list list) 0"])
          apply clarsimp
          apply(drule wf_fd_cons_tupleD)
          apply(clarsimp simp: fd_cons_tuple_def fd_cons_length_def fd_cons_desc_def)
          done
        apply clarsimp
        done
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
qed

lemma field_lookup_fa_fu_lhs_listD:
  "⟦ field_lookup_list ts f m = Some (s,n); fa_fu_ind (field_desc_list ts) d k (size_td_list ts);
      wf_fd_list ts ⟧ ⟹ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s) "
  using field_lookup_fa_fu_lhs(3) [of ts] by blast

lemma field_lookup_fa_fu_lhs_tupleD:
  "⟦ field_lookup_tuple x f m = Some (s,n); fa_fu_ind (field_desc_tuple x) d k (size_td_tuple x);
      wf_fd_tuple x ⟧ ⟹ fa_fu_ind (field_desc (s::('a,'b) typ_info)) d k (size_td s)"
  using field_lookup_fa_fu_lhs(4) [of x] by blast

lemma field_lookup_fa_fu_rhs:
  "∀f m n s d k . field_lookup t f m = Some (s,n) ⟶ fa_fu_ind d (field_desc t) (size_td t) k
      ⟶ wf_fd t ⟶ fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
  "∀f m n s d k. field_lookup_struct st f m = Some (s,n) ⟶ fa_fu_ind d (field_desc_struct st) (size_td_struct st) k
      ⟶ wf_fd_struct st ⟶ fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
  "∀f m n s d k. field_lookup_list ts f m = Some (s,n) ⟶ fa_fu_ind d (field_desc_list ts) (size_td_list ts) k
      ⟶ wf_fd_list ts ⟶ fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
  "∀f m n s d k. field_lookup_tuple x f m = Some (s,n) ⟶ fa_fu_ind d (field_desc_tuple x) (size_td_tuple x) k
      ⟶ wf_fd_tuple x ⟶ fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: fa_fu_ind_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: fa_fu_ind_def)
    subgoal for f m n s d v bs bs'
      apply(clarsimp split: option.splits)
      subgoal premises prems 
        thm prems
        using prems (1-8, 10) 
        apply -
        apply (rule 
            prems (9)[rule_format, where f=f and s = s and m = "m + size_td (dt_fst dt_tuple)"
              and n=n and d=d and k="length bs'", OF prems(11), simplified])
        subgoal for v ys ys'
          apply(drule spec [where x=v])
          apply(drule spec [where x="access_ti_tuple dt_tuple v (replicate (size_td_tuple dt_tuple) 0)@ys"])
          apply clarsimp

          apply(drule wf_fd_cons_tupleD)
          apply(clarsimp simp: fd_cons_tuple_def fd_cons_length_def fd_cons_desc_def)
          apply(drule spec [where x="ys'"])
          apply(clarsimp simp: fd_cons_tuple_def fd_cons_length_def fd_cons_update_access_def fd_cons_desc_def)
          apply(clarsimp simp: fu_commutes_def)
          done
        subgoal by clarsimp
        subgoal
          apply(drule spec [where x=f])
          apply(drule spec [where x=m])
          apply(drule spec [where x=n])
          apply(drule spec [where x=s])
          apply clarsimp
          done
        done
      subgoal
        apply(drule spec [where x=f])
        apply(drule spec [where x=m])
        apply(drule spec [where x=n])
        apply(drule spec [where x=s])
        apply clarsimp
        apply(drule spec [where x=d])
        apply(drule spec [where x="length bs'"])
        apply(erule impE)
         apply clarsimp
        subgoal for v ys ys'
          apply(drule spec [where x=v])
          apply(drule spec [where x="ys@access_ti_list list v (replicate (size_td_list list) 0)"])
          apply(drule wf_fd_cons_tupleD)
          apply(drule wf_fd_cons_listD)
          apply(clarsimp simp: fd_cons_tuple_def fd_cons_list_def fd_cons_length_def
              fd_cons_update_access_def fd_cons_desc_def)
          done
        apply fastforce
        done
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by (clarsimp simp: fa_fu_ind_def)
qed

lemma field_lookup_fa_fu_rhs_listD:
  "⟦ field_lookup_list ts f m = Some (s,n);
      fa_fu_ind d (field_desc_list ts) (size_td_list ts) k; wf_fd_list ts ⟧ ⟹
      fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
  using field_lookup_fa_fu_rhs(3) [of ts] by blast

lemma field_lookup_fa_fu_rhs_tupleD:
  "⟦ field_lookup_tuple x f m = Some (s,n);
      fa_fu_ind d (field_desc_tuple x) (size_td_tuple x) k; wf_fd_tuple x ⟧ ⟹
      fa_fu_ind d (field_desc (s::('a,'b) typ_info)) (size_td s) k"
  using field_lookup_fa_fu_rhs(4) [of x] by blast


lemma fa_fu_lookup_ind_list_tuple:
  shows
  "⟦ field_lookup_tuple x f m = Some (d',n); wf_fd_tuple x;
      field_lookup_list ts f' m' = Some (d,n'); wf_fd_list ts;
      fa_fu_ind (field_desc_list ts) (field_desc_tuple x) (size_td_tuple x) (size_td_list ts) ⟧
      ⟹ fa_fu_ind (field_desc d) (field_desc d') (size_td d') (size_td d)"
  apply(drule (2) field_lookup_fa_fu_lhs_listD)
  apply(drule (3) field_lookup_fa_fu_rhs_tupleD)
  done

lemma fa_fu_lookup_ind_tuple_list:
  "⟦ field_lookup_tuple x f m = Some (d,n); wf_fd_tuple x;
      field_lookup_list ts f' m' = Some (d',n'); wf_fd_list ts;
      fa_fu_ind (field_desc_tuple x) (field_desc_list ts) (size_td_list ts) (size_td_tuple x) ⟧
      ⟹ fa_fu_ind (field_desc d) (field_desc d') (size_td d') (size_td d)"
  apply(drule (2) field_lookup_fa_fu_lhs_tupleD)
  apply(drule (3) field_lookup_fa_fu_rhs_listD)
  done

lemma fa_fu_lookup_disj:
  "∀f m d n f' m' d' n'. field_lookup t f m = Some (d,n) ⟶
      field_lookup t f' m' = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd t ⟶ fa_fu_ind (field_desc (d::('a,'b) typ_info)) (field_desc d') (size_td d') (size_td d)"
  "∀f m d n f' m' d' n'. field_lookup_struct st f m = Some (d,n) ⟶
      field_lookup_struct st f' m' = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_struct st ⟶ fa_fu_ind (field_desc (d::('a,'b) typ_info)) (field_desc d') (size_td d') (size_td d)"
  "∀f m d n f' m' d' n'. field_lookup_list ts f m = Some (d,n) ⟶
      field_lookup_list ts f' m' = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_list ts ⟶ fa_fu_ind (field_desc (d::('a,'b) typ_info)) (field_desc d') (size_td d') (size_td d)"
  "∀f m d n f' m' d' n'. field_lookup_tuple x f m = Some (d,n) ⟶
      field_lookup_tuple x f' m' = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_tuple x ⟶ fa_fu_ind (field_desc (d::('a,'b) typ_info)) (field_desc d') (size_td d') (size_td d)"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: disj_fn_def)
    apply(clarsimp simp: split: option.splits)
    subgoal by blast
    subgoal 
      by(drule (3) fa_fu_lookup_ind_list_tuple; simp)
    subgoal by (drule (3) fa_fu_lookup_ind_tuple_list; simp)
    subgoal for f m d n f' m' d' n'
      apply(drule spec [where x=f ])
      apply(drule spec [where x=m])
      apply(drule spec [where x=d])
      apply clarsimp
      by blast
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply(clarsimp simp: disj_fn_def)
    subgoal for f m d n f' m' d' n'
      apply(drule spec [where x="tl f"])
      apply(drule spec [where x=m])
      apply(drule spec [where x=d])
      apply clarsimp
      apply(drule spec [where x="tl f'"])
      apply(drule spec [where x=m'])
      apply(drule spec [where x=d'])
      apply clarsimp
      apply(cases f; clarsimp)
      apply(cases f'; clarsimp)
      done
    done
qed

lemma fa_fu_lookup_disjD:
  "⟦ field_lookup t f m = Some (d,n); field_lookup t f' m' = Some (d',n');
      disj_fn f f'; wf_fd t ⟧ ⟹
      fa_fu_ind (field_desc (d::('a,'b) typ_info)) (field_desc d') (size_td d') (size_td d)"
 using fa_fu_lookup_disj(1) [of t] by fastforce

lemma field_access_update_disj:
  "⟦ field_lookup t f m = Some (d,n); field_lookup t f' m' = Some (d',n');
      disj_fn f f'; length bs = size_td d'; length bs' = size_td d; wf_fd t ⟧ ⟹
      access_ti d (update_ti_t d' bs v) bs' = access_ti d v bs'"
  by (fastforce dest: fa_fu_lookup_disjD simp: fa_fu_ind_def)

lemma td_set_list_intvl_sub:
  "(d,n) ∈ td_set_list t m ⟹ {of_nat n..+size_td d} ⊆ {of_nat m..+size_td_list t}"
  apply(frule td_set_list_offset_le)
  apply(drule td_set_list_offset_size_m)
  apply clarsimp
  apply(drule intvlD, clarsimp)
  apply(clarsimp simp: intvl_def)
  subgoal for k
    apply(rule exI [where x="k + n - m"])
    apply simp
    done
  done

lemma td_set_tuple_intvl_sub:
  "(d,n) ∈ td_set_tuple t m ⟹ {of_nat n..+size_td d} ⊆ {of_nat m..+size_td_tuple t}"
  apply(frule td_set_tuple_offset_le)
  apply(drule td_set_tuple_offset_size_m)
  apply clarsimp
  apply(drule intvlD, clarsimp)
  apply(clarsimp simp: intvl_def)
  subgoal for k
    apply(rule exI [where x="k + n - m"])
    apply simp
    done
  done

lemma intvl_inter_le:
  assumes inter: "a + of_nat k = c + of_nat ka" and lt_d: "ka < d" and lt_ka: "k ≤ ka"
  shows "a ∈ {c..+d}"
proof -
  from lt_ka inter have "a = c + of_nat (ka - k)" by (simp add: field_simps)
  moreover from lt_d have "ka - k < d" by simp
  ultimately show ?thesis by (force simp: intvl_def)
qed

lemma intvl_inter:
  assumes nondisj: "{a..+b} ∩ {c..+d} ≠ {}"
  shows "a ∈ {c..+d} ∨ c ∈ {a..+b}"
proof -
  from nondisj obtain k ka where "a + of_nat k = c + of_nat ka"
    and "k < b" and "ka < d" by (force simp: intvl_def)
  thus ?thesis by (force intro: intvl_inter_le)
qed

lemma init_intvl_disj:
  "k + z < addr_card ⟹ {(p::addr)+of_nat k..+z} ∩ {p..+k} = {}"
  apply(cases "k ≠ 0"; simp)
  apply(rule ccontr)
  apply(drule intvl_inter)
  apply(erule disjE)
   apply(drule intvlD, clarsimp)
   apply(metis add_lessD1 len_of_addr_card less_trans mod_less order_less_irrefl unat_of_nat)
  apply(drule intvlD, clarsimp)
  apply(subst (asm) Abs_fnat_homs)
  apply(subst (asm) Word.of_nat_0)
  apply(subst (asm) len_of_addr_card)
  apply clarsimp
  subgoal for k' q
    apply(cases q; simp)
    done
  done

lemma final_intvl_disj:
  "⟦ k + z ≤ n; n < addr_card ⟧ ⟹
      {(p::addr)+of_nat k..+z} ∩ {p+(of_nat k + of_nat z)..+n - (k+z)} = {}"
  apply(cases "z ≠ 0"; simp)
  apply(rule ccontr)
  apply(drule intvl_inter)
  apply(erule disjE)
   apply(drule intvlD, clarsimp)
   apply(subst (asm) Abs_fnat_homs)
   apply(subst (asm) Word.of_nat_0)
   apply(subst (asm) len_of_addr_card)
   apply clarsimp
  subgoal for k' q
    apply(cases q; simp)
    done
  apply(drule intvlD, clarsimp)
  apply(subst (asm) word_unat.norm_eq_iff [symmetric])
  apply(subst (asm) len_of_addr_card)
  apply simp
  done

lemma fa_fu_lookup_disj_inter:
  "∀f m d n f' d' n'. field_lookup t f m = Some (d,n) ⟶
      field_lookup t f' m = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd t ⟶ size_td t < addr_card ⟶
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
  "∀f m d n f' m d' n'. field_lookup_struct st f m = Some (d,n) ⟶
      field_lookup_struct st f' m = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_struct st ⟶ size_td_struct st < addr_card ⟶
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
  "∀f m d n f' m d' n'. field_lookup_list ts f m = Some (d,n) ⟶
      field_lookup_list ts f' m = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_list ts ⟶ size_td_list ts < addr_card ⟶
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
  "∀f m d n f' m d' n'. field_lookup_tuple x f m = Some (d,n) ⟶
      field_lookup_tuple x f' m = Some (d',n') ⟶ disj_fn f f' ⟶
      wf_fd_tuple x ⟶ size_td_tuple x < addr_card ⟶
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: disj_fn_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: disj_fn_def)
    apply(rule set_eqI)
    apply(clarsimp split: option.splits)
       apply fastforce
      apply(drule td_set_list_field_lookup_listD)
      apply(drule td_set_list_intvl_sub)
      apply(drule td_set_tuple_field_lookup_tupleD)
      apply(drule td_set_tuple_intvl_sub)
      apply (cases dt_tuple)
      apply(fastforce dest: init_intvl_disj)
     apply(drule td_set_list_field_lookup_listD)
     apply(drule td_set_list_intvl_sub)
     apply(drule td_set_tuple_field_lookup_tupleD)
     apply(drule td_set_tuple_intvl_sub)
     apply (cases dt_tuple)
     apply(fastforce dest: init_intvl_disj)
    apply fastforce
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case 
    apply (clarsimp simp: disj_fn_def)
    apply(rule set_eqI, clarsimp)
    subgoal for f d n f' m d' n' x
      apply(cases f; clarsimp)
      apply(cases f'; clarsimp)
      apply(fastforce simp: disj_fn_def)
      done
    done
qed

lemma fa_fu_lookup_disj_interD:
  "⟦ field_lookup t f m = Some (d,n); field_lookup t f' m = Some (d',n');
      disj_fn f f'; wf_fd t; size_td t < addr_card ⟧ ⟹
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
  using fa_fu_lookup_disj_inter(1) [of t] by clarsimp

lemma fa_fu_lookup_disj_inter_listD:
  "⟦ field_lookup_list ts f m = Some (d,n);
      field_lookup_list ts f' m = Some (d',n'); disj_fn f f';
      wf_fd_list ts; size_td_list ts < addr_card ⟧ ⟹
      {(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩
          {of_nat n'..+size_td d'} = {}"
  using fa_fu_lookup_disj_inter(3) [of ts] by clarsimp

lemma (in mem_type_sans_size) upd_rf:
  "length bs = size_of TYPE('a) ⟹
      update_ti_t (typ_info_t TYPE('a)) bs v
          = update_ti_t (typ_info_t TYPE('a)) bs w"
  by (simp add: upd)

lemma (in mem_type_sans_size) inv:
  "length bs = size_of TYPE('a) ⟹
      from_bytes (to_bytes (x::'a) bs) = x"
  unfolding from_bytes_def to_bytes_def
  by (metis fd_cons_def fd_cons_desc_def fd_cons_update_access_def field_desc.simps(1) 
      field_desc.simps(2) field_desc_def local.len local.size_of_fold 
      local.to_bytes_def local.upd local.wf_fd wf_fd_consD)

lemma (in mem_type) align:
  "align_of (TYPE('a)) dvd addr_card"
proof -
  have *: "align_of TYPE('a) < addr_card"
    by (smt (verit, best) int_dvd_int_iff less_imp_of_nat_less local.align_size_of
        local.max_size local.sz_nzero of_nat_0_less_iff of_nat_less_imp_less zdvd_not_zless)
  from * show ?thesis
    apply -
    apply(subst (asm) align_of_def)
    apply(clarsimp simp: dvd_def align_of_def)
    apply(rule exI [where x="2^(len_of TYPE(addr_bitsize) - align_td (typ_info_t TYPE('a)))"])
    apply clarsimp
    subgoal premises prems
    proof -

      from prems 
      have "align_td (typ_info_t TYPE('a)) < addr_bitsize"
        apply -
        apply(rule power_less_imp_less_exp [where a="2"]; simp add: addr_card)
        done
      then show ?thesis
        apply(simp add: addr_card flip: power_add)
        done
    qed
    done
qed

lemma (in mem_type) to_bytes_inj:
  "to_bytes (v::'a) = to_bytes (v'::'a) ⟹ v=v'"
  apply (drule fun_cong [where x="replicate (size_of TYPE('a)) 0"])
  apply (drule arg_cong [where f="from_bytes::byte list ⇒ 'a"])
  apply (simp add: inv)
  done

lemmas unat_simps = unat_simps' max_size

lemmas (in mem_type) mem_type_simps [simp] = inv len sz_nzero max_size align
lemmas mem_type_simps [simp] = inv len sz_nzero max_size align

lemma (in mem_type) ptr_aligned_plus:
  assumes aligned: "ptr_aligned (p::'a ptr) "
  shows "ptr_aligned (p +⇩p i)"
proof -
  have "int (align_of TYPE('a)) dvd (i * int (size_of TYPE('a)))"
    by (simp add: align_size_of)
  with aligned show ?thesis
    apply (cases p, simp add: ptr_aligned_def ptr_add_def scast_id)
    apply (simp only: unat_simps len_signed)
    apply (metis align align_size_of dvd_add dvd_mod dvd_mult2 mult.commute)
    done
qed


lemma (in mem_type) mem_type_self [simp]:
  "ptr_val (p::'a ptr) ∈ {ptr_val p..+size_of TYPE('a)}"
  by (rule intvl_self, rule sz_nzero)

lemma (in mem_type) intvl_Suc_nmem [simp]:
  "(p::addr) ∉ {p + 1..+size_of TYPE('a) - Suc 0}"
  by (rule intvl_Suc_nmem', subst len_of_addr_card, rule max_size)

lemma (in mem_type) wf_size_desc_typ_uinfo_t_simp [simp]:
  "wf_size_desc (typ_uinfo_t TYPE('a))"
  by (simp add: typ_uinfo_t_def export_uinfo_def wf_size_desc_map)


lemma aggregate_map [simp]:
  "aggregate (map_td f g t) = aggregate t"
  apply(cases t)
  subgoal for x1 st n
    apply(cases st; simp)
    done
  done


lemma (in simple_mem_type) simple_tag_not_aggregate2 [simp]:
  "typ_uinfo_t TYPE('a) ≠ TypDesc algn (TypAggregate ts) tn"
  by (metis aggregate.simps aggregate_map aggregate_struct.simps(2) export_uinfo_def
      local.simple_tag local.typ_uinfo_t_def)

lemma (in simple_mem_type) simple_tag_not_aggregate3 [simp]:
  "typ_info_t TYPE('a) ≠ TypDesc algn (TypAggregate ts) tn"
  by (metis aggregate.simps aggregate_struct.simps(2) simple_tag)

lemma (in mem_type) field_of_t_mem:
  "field_of_t (p::'a ptr) (q::'b::mem_type ptr) ⟹
   ptr_val p ∈ {ptr_val q..+size_of TYPE('b)}"
  apply(clarsimp simp: field_of_t_def field_of_def intvl_def)
  apply(rule exI [where x="unat (ptr_val p - ptr_val q)"])
  apply simp
  apply(drule td_set_offset_size)
  apply(clarsimp simp: size_of_def)
  by (metis (mono_tags, lifting) add_leD2 add_le_same_cancel2 c_type_class.size_of_def
      leD local.size_of_def local.sz_nzero nat_less_le)

lemma map_td_map:
  "map_td f p (map_td g q t) = map_td (λn algn. f n algn o g n algn) (p o q) t"
  "map_td_struct f p (map_td_struct g q st) = map_td_struct (λn algn. f n algn o g n algn) (p o q) st"
  "map_td_list f p (map_td_list g q ts) = map_td_list (λn algn. f n algn o g n algn) (p o q) ts"
  "map_td_tuple f p (map_td_tuple g q x) = map_td_tuple (λn algn. f n algn o g n algn) (p o q) x"
  by (induct t and st and ts and x) auto

lemma field_of_t_simple:
  "field_of_t p (x::'a::simple_mem_type ptr) ⟹ ptr_val p = ptr_val x"
  apply(clarsimp simp: field_of_t_def)
  apply(cases "typ_uinfo_t TYPE('a)")
  subgoal for x1 st n

    apply(cases st; clarsimp)
    apply(clarsimp simp: field_of_def unat_eq_zero)
    done
  done

lemma fold_td'_unfold:
 "fold_td' t =
    (let (f,s) = t in
     case s of TypDesc algn' st nm ⇒
       (case st of
          TypScalar n algn d ⇒ d
        | TypAggregate ts ⇒ f nm (map (λx. case x of DTuple t n d ⇒ (fold_td' (f,t),n)) ts)))"
  apply (cases t, simp)
  subgoal for a b
    apply (cases b, simp)
    done
  done

lemma fold_td_alt_def':
  "fold_td f t = (case t of
                    TypDesc algn' st nm ⇒
                      (case st of
                         TypScalar n algn d ⇒ d
                       | TypAggregate ts ⇒ f nm (map (λx. (fold_td f (dt_fst x),dt_snd x)) ts)))"
  apply(cases t)
  apply(clarsimp split: typ_desc.split typ_struct.splits dt_tuple.splits)
  by (metis (no_types, lifting) dt_tuple.case dt_tuple.collapse)

lemma fold_td_alt_def:
  "fold_td f t ≡ (case t of
                    TypDesc algn' st nm ⇒
                      (case st of
                         TypScalar n algn d ⇒ d
                       | TypAggregate ts ⇒ f nm (map (λx. (fold_td f (dt_fst x),dt_snd x)) ts)))"
  by (fastforce simp: fold_td_alt_def' simp del: fold_td_def)


lemma map_td'_map':
  "map_td f g t = (map_td' ((f,g),t))"
  "TypDesc algn (map_td_struct f g st) (typ_name t) = (map_td' ((f,g),TypDesc algn st (typ_name t)))"
  "TypDesc algn (TypAggregate (map_td_list f g ts)) (typ_name t) = map_td' ((f,g),TypDesc algn (TypAggregate ts) (typ_name t))"
  "map_td_tuple f g x = DTuple (map_td' ((f,g),dt_fst x)) (dt_snd x) (g (dt_trd x))"
  by (induct t and st and ts and x) (auto simp: split_DTuple_all)

lemma map_td'_map:
  "map_td f g t = (case t of TypDesc algn st nm ⇒ TypDesc algn (case st of
           TypScalar n algn d ⇒ TypScalar n algn (f n algn d) |
           TypAggregate ts ⇒ TypAggregate (map (λx. DTuple (map_td f g (dt_fst x)) (dt_snd x) (g (dt_trd x))) ts)) nm)"
  apply(subst map_td'_map')
  apply(subst map_td'_map')
  apply(cases t, simp add: typ_struct.splits)
  apply(auto simp: split_DTuple_all)
  done

lemma map_td_alt_def:
  "map_td f g t ≡ (case t of TypDesc algn st nm ⇒ TypDesc algn (case st of
           TypScalar n algn d ⇒ TypScalar n algn (f n algn d) |
           TypAggregate ts ⇒ TypAggregate (map (λx. DTuple (map_td f g (dt_fst x)) (dt_snd x) (g (dt_trd x))) ts)) nm)"
  by (simp add: map_td'_map)

lemma size_td_fm':
  "size_td (t::('a,'b) typ_desc) = fold_td tnSum (map_td (λn x d. n) g t)"
  "size_td_struct (st::('a,'b) typ_struct) = fold_td_struct (typ_name t) tnSum (map_td_struct (λn x d. n) g st)"
  "size_td_list (ts::('a,'b) typ_tuple list) = fold_td_list (typ_name t) tnSum (map_td_list (λn x d. n) g ts)"
  "size_td_tuple (x::('a,'b) typ_tuple) = fold_td_tuple tnSum (map_td_tuple (λn x d. n) g x)"
  by  (induct t and st and ts and x) (auto simp: tnSum_def split: dt_tuple.splits)

lemma size_td_fm:
  "size_td (t::('a,'b) typ_desc) ≡ fold_td tnSum (map_td (λn algn d. n) id t)"
  using size_td_fm'(1) [of t id] by clarsimp

lemma align_td_wo_align_fm':
  "align_td_wo_align (t::('a,'b) typ_desc) = fold_td tnMax (map_td (λn x d. x) g t)"
  "align_td_wo_align_struct (st::('a,'b) typ_struct) = fold_td_struct (typ_name t) tnMax (map_td_struct (λn x d. x) g st)"
  "align_td_wo_align_list (ts::('a,'b) typ_tuple list) = fold_td_list (typ_name t) tnMax (map_td_list (λn x d. x) g ts)"
  "align_td_wo_align_tuple (x::('a,'b) typ_tuple) = fold_td_tuple tnMax (map_td_tuple (λn x d. x) g x)"
  by (induct t and st and ts and x) (auto simp: tnMax_def split: dt_tuple.splits)

lemma align_td_wo_align_fm:
  "align_td_wo_align (t::('a,'b) typ_desc) ≡ fold_td tnMax (map_td (λn algn d. algn) id t)"
  using align_td_wo_align_fm'(1) [of t id] by clarsimp

thm case_dt_tuple_def

lemma case_dt_tuple:
  "snd ` case_dt_tuple (λt n d. Pair (f t) n) ` X = dt_snd ` X"
  by (force simp: image_iff split_DTuple_all split: dt_tuple.splits)

lemma map_DTuple_dt_snd:
  "map_td_tuple f g x = DTuple a b c ⟹ b = dt_snd x"
  by (metis dt_tuple.inject map_td'_map'(4))

lemma wf_desc_fm':
  "wf_desc (t::('a,'b) typ_desc) = fold_td wfd (map_td (λn x d. True) g t)"
  "wf_desc_struct (st::('a,'b) typ_struct) = fold_td_struct (typ_name t) wfd (map_td_struct (λn x d. True) g st)"
  "wf_desc_list (ts::('a,'b) typ_tuple list) = fold_td_list (typ_name t) wfd (map_td_list (λn x d. True) g ts)"
  "wf_desc_tuple (x::('a,'b) typ_tuple) = fold_td_tuple wfd (map_td_tuple (λn x d. True) g x)"
  supply split_DTuple_all[simp] dt_tuple.splits[split]
  apply (induct t and st and ts and x, all ‹clarsimp simp: wfd_def image_comp[symmetric]›)
  apply (rule iffI; clarsimp)
   apply (metis (no_types) dt_prj_simps(2) dt_snd_map_td_list imageI)
  by (metis (mono_tags) case_dt_tuple dt_prj_simps(2) dt_snd_map_td_list image_eqI)

lemma wf_desc_fm:
  "wf_desc (t::('a,'b) typ_desc) ≡ fold_td wfd (map_td (λn algn d. True) id t)"
  using wf_desc_fm'(1) [of t id] by auto

lemma update_tag_list_empty [simp]:
  "(map_td_list f g xs = []) = (xs = [])"
  by (cases xs, auto)

lemma wf_size_desc_fm':
  "wf_size_desc (t::('a,'b) typ_desc) = fold_td wfsd (map_td (λn x d. 0 < n) g t)"
  "wf_size_desc_struct (st::('a,'b) typ_struct) = fold_td_struct (typ_name t) wfsd (map_td_struct (λn x d. 0 < n) g st)"
  "ts ≠ [] ⟶ wf_size_desc_list (ts::('a,'b) typ_tuple list) = fold_td_list (typ_name t) wfsd (map_td_list (λn x d. 0 < n) g ts)"
  "wf_size_desc_tuple (x::('a,'b) typ_tuple) = fold_td_tuple wfsd (map_td_tuple (λn x d. 0 < n) g x)"
  by (induct t and st and ts and x) (auto simp: wfsd_def split: dt_tuple.splits)

lemma wf_size_desc_fm:
  "wf_size_desc (t::('a,'b) typ_desc) ≡ fold_td wfsd (map_td (λn algn d. 0 < n) id t)"
  using wf_size_desc_fm'(1) [of t id] by auto

typedef stack_byte = "UNIV::byte set"
  by (simp)

definition "stack_byte_name = ''stack_byte''"

instantiation stack_byte :: c_type
begin

definition "typ_name_itself (x::stack_byte itself) = stack_byte_name"

definition
  typ_info_stack_byte: "typ_info_t (x::stack_byte itself) ≡
     TypDesc 0 (TypScalar 1 0
              ⦇field_access = λv bs. [Rep_stack_byte v],
               field_update = λbs v. if length bs ≥ 1 then Abs_stack_byte (hd bs) else Abs_stack_byte (0::byte),
               field_sz = 1⦈)
            stack_byte_name"

instance
  by (intro_classes) (simp add: typ_name_itself_stack_byte_def typ_info_stack_byte)
end

lemma size_of_stack_byte [simp]:
  "size_of TYPE(stack_byte) = 1"
  "size_td (typ_info_t TYPE(stack_byte)) = 1"
  "size_td (typ_uinfo_t TYPE(stack_byte)) = 1"
  by (simp_all add: size_of_def typ_info_stack_byte typ_uinfo_t_def)

lemma align_of_stack_byte [simp]:
  "align_of TYPE(stack_byte) = 1"
  "align_td (typ_info_t TYPE(stack_byte)) = 0"
  "align_td (typ_uinfo_t TYPE(stack_byte)) = 0"
  by (simp_all add: align_of_def typ_info_stack_byte typ_uinfo_t_def)

lemma length_1_conv: "length bs = Suc 0 ⟷ (∃b. bs = [b])"
  by (cases bs) auto
lemma padding_lense_stack_byte: "padding_lense (λv bs. [Rep_stack_byte v])
     (λbs v.
         if Suc 0 ≤ length bs then Abs_stack_byte (hd bs) else Abs_stack_byte 0)
     (Suc 0)"
  apply (unfold_locales)
        apply (simp add: padding_base.is_padding_byte_def padding_base.is_value_byte_def Abs_stack_byte_inverse )
    subgoal

      proof -
        have "length [1::8 word] = Suc 0"
          by simp
        then show ?thesis
          by (metis (mono_tags, opaque_lifting) Abs_stack_byte_inject One_nat_def
              Rep_stack_byte_inject UNIV_I hd_conv_nth length_append n_not_Suc_n
              plus_1_eq_Suc self_append_conv2 zero_neq_one)
      qed
           apply (clarsimp)
          apply clarsimp
         apply (clarsimp simp add: Rep_stack_byte_inverse)
        apply simp
       apply simp
      apply simp
      done

instantiation stack_byte:: xmem_contained_type
begin
instance
  apply (intro_classes)
              apply (simp add: typ_info_stack_byte)
             apply (simp add: typ_info_stack_byte)
            apply (simp add: typ_info_stack_byte wf_lf_def fd_cons_desc_def fd_cons_double_update_def
                    fd_cons_update_access_def fd_cons_access_update_def
                    Rep_stack_byte_inverse fd_cons_length_def)
           apply (simp add: typ_info_stack_byte)
          apply simp
         apply (simp add: typ_info_stack_byte align_field_def)
        apply (simp add: typ_info_stack_byte)
       apply (simp add: addr_card)
      apply (simp add: typ_info_stack_byte)
     apply (simp add: typ_info_stack_byte)
    apply (simp add: typ_info_stack_byte wf_field_desc_def padding_lense_stack_byte)
   apply  (simp add: typ_info_stack_byte)
  apply  (simp add: typ_info_stack_byte)
  done

end

end