Theory CompoundCTypes

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

theory CompoundCTypes
  imports
    Vanilla32
    Padding
    Lens
begin

lemma simple_type_dest: "¬aggregate t ⟹ ∃n sz align align' d. t = TypDesc align' (TypScalar sz align d) n"
  apply (cases t)
  subgoal for x1 st n
    apply (cases st)
     apply auto
    done
  done

definition empty_typ_info :: "nat ⇒ typ_name ⇒ ('a,'b) typ_desc" where
  "empty_typ_info algn tn ≡ TypDesc algn (TypAggregate []) tn"

(*
  More general type, may cause problems in some proofs as type inference
  extend_ti :: "('a,'b) typ_info ⇒ ('a,'b) typ_info ⇒ field_name ⇒ 'b ⇒ ('a,'b) typ_info" and
  extend_ti_struct :: "('a,'b) typ_info_struct ⇒ ('a,'b) typ_info ⇒ field_name ⇒ 'b ⇒ ('a,'b) typ_info_struct"

*)
primrec
  extend_ti :: "'a xtyp_info ⇒ 'a xtyp_info ⇒ nat ⇒ field_name ⇒ 'a field_desc ⇒ 'a xtyp_info" and
  extend_ti_struct :: "'a xtyp_info_struct ⇒ 'a xtyp_info ⇒ field_name ⇒ 'a field_desc ⇒ 'a xtyp_info_struct"
where
  et0: "extend_ti (TypDesc algn' st nm) t algn fn d  = TypDesc (max algn' (max algn (align_td t))) (extend_ti_struct st t fn d) nm"

| et1: "extend_ti_struct (TypScalar n sz algn) t fn d = TypAggregate [DTuple t fn d]"
| et2: "extend_ti_struct (TypAggregate ts) t fn d = TypAggregate (ts@[DTuple t fn d])"

lemma aggregate_empty_typ_info [simp]:
  "aggregate (empty_typ_info algn tn)"
  by (simp add: empty_typ_info_def)

lemma aggregate_extend_ti [simp]:
  "aggregate (extend_ti tag t algn f d)"
  apply(cases tag)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct, auto)
    done
  done

lemma typ_name_extend_ti [simp]: "typ_name (extend_ti T t algn fn d) = typ_name T"
  by (cases T) auto

definition update_desc :: "('a ⇒ 'b) ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ 'b field_desc ⇒ 'a field_desc" where
  "update_desc acc upd d ≡ ⦇field_access = (field_access d) ∘  acc,
                             field_update = λbs v. upd (field_update d bs (acc v)) v, field_sz = field_sz d ⦈"

lemma update_desc_id[simp]: "update_desc id (λx _. x) = id"
  by (simp add: update_desc_def fun_eq_iff)

term "map_td (λn algn. update_desc acc upd) (update_desc acc upd) t"


definition adjust_ti :: "'b xtyp_info ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ 'a xtyp_info" where
  "adjust_ti t acc upd ≡ map_td (λn algn. update_desc acc upd) (update_desc acc upd) t"

lemma adjust_ti_adjust_ti:
  "adjust_ti (adjust_ti t g s) g' s' =
    adjust_ti t (g ∘ g') (λv x. s' (s v (g' x)) x)"
  by (simp add: adjust_ti_def map_td_map update_desc_def[abs_def] comp_def)

lemma typ_desc_size_update_ti [simp]:
  "(size_td (adjust_ti t acc upd) = size_td t)"
  by (simp add: adjust_ti_def)

lemma export_tag_adjust_ti[rule_format]:
  "∀bs. fg_cons acc upd  ⟶ wf_fd t ⟶
    export_uinfo (adjust_ti t acc upd) = export_uinfo t"
  "∀bs. fg_cons acc upd ⟶ wf_fd_struct st ⟶
    map_td_struct field_norm (λ_. ()) (map_td_struct (λn algn. update_desc acc upd) (update_desc acc upd) st) =
    map_td_struct field_norm (λ_. ()) st"
  "∀bs. fg_cons acc upd ⟶ wf_fd_list ts ⟶
    map_td_list field_norm (λ_. ()) (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) =
    map_td_list field_norm (λ_. ()) ts"
  "∀bs. fg_cons acc upd ⟶ wf_fd_tuple x ⟶
    map_td_tuple field_norm (λ_. ()) (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) =
    map_td_tuple field_norm (λ_. ()) x"
  unfolding adjust_ti_def
  by (induct t and st and ts and x, all ‹clarsimp simp: export_uinfo_def›)
     (fastforce simp: update_desc_def field_norm_def fg_cons_def fd_cons_struct_def
                      fd_cons_access_update_def fd_cons_desc_def)


definition (in c_type) ti_typ_combine ::
  "'a itself ⇒ ('b ⇒ 'a) ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ nat ⇒ field_name ⇒ 'b xtyp_info ⇒ 'b xtyp_info"
  where
  "ti_typ_combine t_b acc upd algn fn tag ≡
     let ft = adjust_ti (typ_info_t TYPE('a)) acc upd
     in extend_ti tag ft algn fn ⦇field_access = xto_bytes o acc, field_update = upd o xfrom_bytes, field_sz = size_of TYPE('a)⦈"

primrec
  padding_fields :: "('a,'b) typ_desc ⇒ field_name list" and
  padding_fields_struct :: "('a,'b) typ_struct ⇒ field_name list"
where
  pf0: "padding_fields (TypDesc algn st tn) = padding_fields_struct st"

| pf1: "padding_fields_struct (TypScalar n algn d) = []"
| pf2: "padding_fields_struct (TypAggregate xs) = filter (λx. hd x = CHR ''!'') (map dt_snd xs)"

primrec
  non_padding_fields :: "('a,'b) typ_desc ⇒ field_name list" and
  non_padding_fields_struct :: "('a,'b) typ_struct ⇒ field_name list"
where
  npf0: "non_padding_fields (TypDesc algn st tn) = non_padding_fields_struct st"

| npf1: "non_padding_fields_struct (TypScalar n algn d) = []"
| npf2: "non_padding_fields_struct (TypAggregate xs) = filter (λx. hd x ≠ CHR ''!'') (map dt_snd xs)"

definition field_names_list :: "('a,'b) typ_desc ⇒ field_name list" where
  "field_names_list tag ≡ non_padding_fields tag @ padding_fields tag"




definition ti_pad_combine :: "nat ⇒ 'a xtyp_info ⇒ 'a xtyp_info" where
  "ti_pad_combine n tag ≡
     let
       fn = foldl (@) ''!pad_'' (field_names_list tag);
       td = padding_desc n;
       nf = TypDesc 0 (TypScalar n 0 td) ''!pad_typ''
     in extend_ti tag nf 0 fn td"

lemma aggregate_ti_pad_combine [simp]:
  "aggregate (ti_pad_combine n tag)"
  by (simp add: ti_pad_combine_def Let_def)

definition (in c_type) ti_typ_pad_combine ::
  "'a itself ⇒ ('b ⇒ 'a) ⇒ ('a ⇒ 'b ⇒ 'b) ⇒ nat ⇒ field_name ⇒ 'b xtyp_info ⇒ 'b xtyp_info"
  where
  "ti_typ_pad_combine t acc upd algn fn tag ≡
     let
       pad = padup (max (2 ^ algn) (align_of TYPE('a))) (size_td tag);
       ntag = if 0 < pad then ti_pad_combine pad tag else tag
     in
       ti_typ_combine t acc upd algn fn ntag"

definition "map_align f t = (case t of TypDesc algn st n ⇒ TypDesc (f algn) st n)"
lemma map_align_simp [simp]: "map_align f (TypDesc algn st n) = TypDesc (f algn) st n"
  by (simp add: map_align_def)


definition final_pad :: "nat ⇒ 'a xtyp_info ⇒ 'a xtyp_info" where
  "final_pad algn tag ≡
     let n = padup (2^(max algn (align_td tag))) (size_td tag)
     in map_align (max algn) (if 0 < n then ti_pad_combine n tag else tag)"

lemma field_names_list_empty_typ_info [simp]:
  "set (field_names_list (empty_typ_info algn tn)) = {}"
  by (simp add: empty_typ_info_def field_names_list_def)

lemma field_names_list_extend_ti [simp]:
  "set (field_names_list (extend_ti tag t algn fn d)) = set (field_names_list tag) ∪ {fn}"
  unfolding field_names_list_def
  apply(cases tag)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct; simp)
    done
  done

lemma (in c_type) field_names_list_ti_typ_combine [simp]:
  "set (field_names_list (ti_typ_combine (t::'a itself) f f_upd algn fn tag))
     = set (field_names_list tag) ∪ {fn}"
  by (clarsimp simp: ti_typ_combine_def Let_def)

lemma field_names_list_ti_pad_combine [simp]:
  "set (field_names_list (ti_pad_combine n tag))
     = set (field_names_list tag) ∪ {foldl (@) ''!pad_'' (field_names_list tag)}"
  by (clarsimp simp: ti_pad_combine_def Let_def)

― ‹matches on padding›
lemma hd_string_hd_fold_eq [simp]:
  "⟦ s ≠ []; hd s = CHR ''!'' ⟧ ⟹ hd (foldl (@) s xs) = CHR ''!''"
  by (induct xs arbitrary: s; clarsimp)

lemma field_names_list_ti_typ_pad_combine [simp]:
  "hd x ≠ CHR ''!'' ⟹
      x ∈ set (field_names_list (ti_typ_pad_combine align t_b f_ab f_upd_ab fn tag))
          = (x ∈ set (field_names_list tag) ∪ {fn})"
  by (auto simp: ti_typ_pad_combine_def Let_def)

lemma wf_desc_empty_typ_info [simp]:
  "wf_desc (empty_typ_info algn tn)"
  by (simp add: empty_typ_info_def)

lemma wf_desc_extend_ti:
  "⟦ wf_desc tag; wf_desc t; f ∉ set (field_names_list tag) ⟧ ⟹
      wf_desc (extend_ti tag t algn f d)"
  unfolding field_names_list_def
  apply(cases tag)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct; clarsimp)
    done
  done

lemma foldl_append_length:
  "length (foldl (@) s xs) ≥ length s"
  apply(induct xs arbitrary: s, clarsimp)
  subgoal for  a list s
    apply(drule meta_spec [where x="s@a"])
    apply clarsimp
    done
  done

lemma foldl_append_nmem:
  "s ≠ [] ⟹ foldl (@) s xs ∉ set xs"
  apply(induct xs arbitrary: s, clarsimp)
  subgoal for a list s
  apply(drule meta_spec [where x="s@a"])
    apply clarsimp
    by (metis add_le_same_cancel2 foldl_append_length le_zero_eq length_0_conv length_append)
  done

lemma wf_desc_ti_pad_combine:
  "wf_desc tag ⟹ wf_desc (ti_pad_combine n tag)"
  apply(clarsimp simp: ti_pad_combine_def Let_def)
  apply(erule wf_desc_extend_ti)
   apply simp
  apply(rule foldl_append_nmem, simp)
  done

lemma wf_desc_adjust_ti [simp]:
  "wf_desc (adjust_ti t f g) = wf_desc (t::'a xtyp_info)"
  by (simp add: adjust_ti_def wf_desc_map)

lemma (in wf_type) wf_desc_ti_typ_combine:
  "⟦ wf_desc tag; fn ∉ set (field_names_list tag) ⟧ ⟹
    wf_desc (ti_typ_combine (t_b::'a itself) acc upd_ab algn fn tag)"
  by (fastforce simp: ti_typ_combine_def Let_def elim: wf_desc_extend_ti)

lemma (in wf_type) wf_desc_ti_typ_pad_combine:
  "⟦ wf_desc tag;  fn ∉ set (field_names_list tag); hd fn ≠ CHR ''!'' ⟧ ⟹
   wf_desc (ti_typ_pad_combine (t_b::'a itself) acc upd algn fn tag)"
  unfolding ti_typ_pad_combine_def Let_def
  by (auto intro!: wf_desc_ti_typ_combine wf_desc_ti_pad_combine)

lemma wf_desc_map_align: "wf_desc tag ⟹ wf_desc (map_align f tag)"
  by (cases tag) (simp)

lemma wf_desc_final_pad:
  "wf_desc tag ⟹ wf_desc (final_pad algn tag)"
  by (auto simp: final_pad_def Let_def wf_desc_map_align wf_desc_ti_pad_combine)

lemma wf_size_desc_extend_ti:
  "⟦ wf_size_desc tag; wf_size_desc t ⟧ ⟹ wf_size_desc (extend_ti tag t algn fn d)"
  apply(cases tag)
  subgoal for x1 typ_struct list
    apply(cases typ_struct, auto)
    done
  done

lemma wf_size_desc_ti_pad_combine:
  "⟦ wf_size_desc tag; 0 < n ⟧ ⟹ wf_size_desc (ti_pad_combine n tag)"
  by (fastforce simp: ti_pad_combine_def Let_def elim: wf_size_desc_extend_ti)

lemma wf_size_desc_adjust_ti:
  "wf_size_desc (adjust_ti t f g) = wf_size_desc (t::'a xtyp_info)"
  by (simp add: adjust_ti_def wf_size_desc_map)

lemma (in wf_type) wf_size_desc_ti_typ_combine:
  "wf_size_desc tag ⟹ wf_size_desc (ti_typ_combine (t_b::'a itself) acc upd_ab algn fn tag)"
  by (fastforce simp: wf_size_desc_adjust_ti ti_typ_combine_def Let_def elim: wf_size_desc_extend_ti)

lemma (in wf_type) wf_size_desc_ti_typ_pad_combine:
  "wf_size_desc tag ⟹
    wf_size_desc (ti_typ_pad_combine (t_b::'a itself) acc upd algn fn tag)"
  by (auto simp: ti_typ_pad_combine_def Let_def
           intro: wf_size_desc_ti_typ_combine
           elim: wf_size_desc_ti_pad_combine)

lemma (in wf_type) wf_size_desc_ti_typ_combine_empty [simp]:
  "wf_size_desc (ti_typ_combine (t_b::'a itself) acc upd algn fn (empty_typ_info algn' tn))"
  by (clarsimp simp: ti_typ_combine_def Let_def empty_typ_info_def wf_size_desc_adjust_ti)

lemma (in wf_type) wf_size_desc_ti_typ_pad_combine_empty [simp]:
  "wf_size_desc (ti_typ_pad_combine (t_b::'a itself) acc upd algn fn
      (empty_typ_info algn' tn))"
  by (clarsimp simp: ti_typ_pad_combine_def Let_def ti_typ_combine_def empty_typ_info_def
                     ti_pad_combine_def wf_size_desc_adjust_ti)

lemma wf_size_desc_msp_align:
  "wf_size_desc tag ⟹ wf_size_desc (map_align f tag)"
  by (cases tag) (simp add: wf_size_desc_def)

lemma wf_size_desc_final_pad:
  "wf_size_desc tag ⟹ wf_size_desc (final_pad algn tag)"
  by (fastforce simp: final_pad_def Let_def wf_size_desc_msp_align wf_size_desc_ti_pad_combine)

lemma wf_fdp_set_comp_simp [simp]:
  "wf_fdp {(a, n # b) |a b. (a, b) ∈ tf_set t} = wf_fdp (tf_set t)"
  unfolding wf_fdp_def by fastforce

lemma lf_set_adjust_ti':
  "∀d fn. d ∈ lf_set (map_td (λn algn. update_desc acc upd) (update_desc acc upd) t) fn ⟶
      (∃y. lf_fd d=update_desc acc upd (lf_fd y) ∧ lf_sz d=lf_sz y ∧ lf_fn d=lf_fn y ∧ y ∈ lf_set t fn)"
  "∀d fn. d ∈ lf_set_struct (map_td_struct (λn algn. update_desc acc upd) (update_desc acc upd) st) fn ⟶
      (∃y. lf_fd d=update_desc acc upd (lf_fd y) ∧ lf_sz d=lf_sz y ∧ lf_fn d=lf_fn y ∧ y ∈ lf_set_struct st fn)"
  "∀d fn. d ∈ lf_set_list (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) fn ⟶
      (∃y. lf_fd d=update_desc acc upd (lf_fd y) ∧ lf_sz d=lf_sz y ∧ lf_fn d=lf_fn y ∧ y ∈ lf_set_list ts fn)"
  "∀d fn. d ∈ lf_set_tuple (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) fn ⟶
      (∃y. lf_fd d=update_desc acc upd (lf_fd y) ∧ lf_sz d=lf_sz y ∧ lf_fn d=lf_fn y ∧ y ∈ lf_set_tuple x fn)"
  unfolding update_desc_def
  by (induct t and st and ts and x) fastforce+

lemma lf_set_adjust_ti:
  "⟦ d ∈ lf_set (adjust_ti t acc upd) fn; ⋀y. upd (acc y) y = y ⟧ ⟹
      (∃y. lf_fd d=update_desc acc upd (lf_fd y) ∧ lf_sz d=lf_sz y ∧ lf_fn d=lf_fn y ∧ y ∈ lf_set t fn)"
  by (simp add: lf_set_adjust_ti' adjust_ti_def)

lemma fd_cons_struct_id_simp [simp]:
  "fd_cons_struct (TypScalar n algn ⦇field_access = λv. id, field_update = λbs. id, field_sz = m⦈)"
  by (auto simp: fd_cons_struct_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 fd_cons_desc_def)


lemma field_desc_adjust_ti:
  "fg_cons acc upd ⟶
     field_desc (adjust_ti (t::'a xtyp_info) acc upd) =
     update_desc acc upd (field_desc t)"
  "fg_cons acc upd ⟶
     field_desc_struct (map_td_struct (λn algn. update_desc  acc upd) (update_desc acc upd) st) =
     update_desc  acc upd (field_desc_struct st)"
  "fg_cons acc upd ⟶
     field_desc_list (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) =
     update_desc acc upd (field_desc_list ts)"
  "fg_cons acc upd ⟶
     field_desc_tuple (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) =
     update_desc acc upd (field_desc_tuple x)"
  unfolding adjust_ti_def
     by (induct t and st and ts and x) (fastforce simp: fg_cons_def update_desc_def update_ti_t_struct_t)+

lemma update_ti_t_adjust_ti:
  "fg_cons acc upd ⟹ update_ti_t (adjust_ti t acc upd) bs v = upd (update_ti_t t bs (acc v)) v"
  using field_desc_adjust_ti(1) [of acc upd t]
  by (clarsimp simp: update_desc_def)

declare field_desc_def [simp del]

lemma (in c_type) aggregate_ti_typ_combine [simp]:
  "aggregate (ti_typ_combine (t_b::'a itself) acc upd algn fn tag)"
  by (simp add: ti_typ_combine_def Let_def)

lemma (in c_type) aggregate_ti_typ_pad_combine [simp]:
  "aggregate (ti_typ_pad_combine (t_b::'a itself) acc upd algn fn tag)"
  by (simp add: ti_typ_pad_combine_def Let_def)

lemma align_of_empty_typ_info [simp]:
  "align_td_wo_align (empty_typ_info algn tn) = 0"
  by (simp add: empty_typ_info_def)

lemma align_of_empty_typ_info' [simp]:
  "align_td (empty_typ_info algn tn) = algn"
  by (simp add: empty_typ_info_def)

lemma align_of_tag_list [simp]:
  "align_td_wo_align_list (xs @ [DTuple t fn d]) = max (align_td_wo_align_list xs) (align_td_wo_align t)"
  by (induct xs) auto

lemma align_of_tag_list' [simp]:
  "align_td_list (xs @ [DTuple t fn d]) = max (align_td_list xs) (align_td t)"
  by (induct xs) auto

lemma align_of_extend_ti [simp]:
  "aggregate ti ⟹ align_td_wo_align (extend_ti ti t algn fn d) = max (align_td_wo_align ti) (align_td_wo_align t)"
  apply (cases ti)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct; clarsimp)
    done
  done

lemma align_of_extend_ti' [simp]:
  "aggregate ti ⟹ align_td (extend_ti ti t algn fn d) = max (align_td ti) (max algn (align_td t))"
  apply (cases ti)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct; clarsimp)
    done
  done

lemma align_of_adjust_ti [simp]:
  "align_td_wo_align (adjust_ti t acc upd) = align_td_wo_align (t::'a xtyp_info)"
  by (simp add: adjust_ti_def)

lemma align_of_adjust_ti' [simp]:
  "align_td (adjust_ti t acc upd) = align_td (t::'a xtyp_info)"
  by (simp add: adjust_ti_def)

lemma (in c_type) align_of_ti_typ_combine [simp]:
  "aggregate ti ⟹
     align_td_wo_align (ti_typ_combine (t::'a itself) acc upd algn fn ti) =
     max (align_td_wo_align ti) (align_td_wo_align (typ_info_t (TYPE('a))))"
  by (clarsimp simp: ti_typ_combine_def Let_def align_of_def)

lemma (in c_type) align_of_ti_typ_combine' [simp]:
  "aggregate ti ⟹
     align_td (ti_typ_combine (t::'a itself) acc upd algn fn ti) =
     max (align_td ti) (max algn (align_td (typ_info_t TYPE('a))))"
  by (clarsimp simp: ti_typ_combine_def Let_def align_of_def)

lemma align_of_ti_pad_combine [simp]:
  "aggregate ti ⟹ align_td_wo_align (ti_pad_combine n ti) = (align_td_wo_align ti)"
  by (clarsimp simp: ti_pad_combine_def Let_def max_def)

lemma align_of_ti_pad_combine' [simp]:
  "aggregate ti ⟹ align_td (ti_pad_combine n ti) = (align_td ti)"
  by (clarsimp simp: ti_pad_combine_def Let_def max_def)

lemma max_2_exp: "max ((2::nat) ^ a) (2 ^ b) = 2 ^ (max a b)"
  by (simp add: max_def)

lemma align_td_wo_align_map_align: "align_td_wo_align (map_align f t) = align_td_wo_align t"
  by (cases t) simp

lemma align_td_wo_align_final_pad:
  "aggregate ti ⟹
  align_td_wo_align (final_pad algn ti) = (align_td_wo_align ti)"
  by (simp add: final_pad_def Let_def  padup_def align_td_wo_align_map_align)

lemma align_td_map_align [simp]: "align_td (map_align f t) = f (align_td t)"
  by (cases t) simp

lemma align_of_final_pad:
  "aggregate ti ⟹
  align_td (final_pad algn ti) = max algn (align_td ti)"
  by (simp add: final_pad_def Let_def  padup_def align_td_map_align )


lemma (in c_type) align_td_wo_align_ti_typ_pad_combine [simp]:
  "aggregate ti ⟹
     align_td_wo_align (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) =
     max (align_td_wo_align ti) (align_td_wo_align (typ_info_t TYPE('a)))"
  by (clarsimp simp: ti_typ_pad_combine_def Let_def)

lemma (in c_type) align_td_ti_typ_pad_combine [simp]:
  "aggregate ti ⟹
     align_td (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) =
     max (align_td ti) (max algn (align_td (typ_info_t TYPE('a))))"
  by (clarsimp simp: ti_typ_pad_combine_def Let_def)

definition fu_s_comm_set :: "(byte list ⇒ 'a ⇒ 'a) set ⇒ (byte list ⇒ 'a ⇒ 'a) set ⇒ bool"
  where
  "fu_s_comm_set X Y ≡ ∀x y. x ∈ X ∧ y ∈ Y ⟶ (∀v bs bs'. x bs (y bs' v) = y bs' (x bs v))"

lemma fc_empty_ti [simp]:
  "fu_commutes (update_ti_t (empty_typ_info algn tn)) f"
  by (auto simp: fu_commutes_def empty_typ_info_def)

lemma fc_extend_ti:
  "⟦ fu_commutes (update_ti_t s) h; fu_commutes (update_ti_t t) h ⟧
      ⟹ fu_commutes (update_ti_t (extend_ti s t algn fn d)) h"
  apply(cases s)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct, auto simp: fu_commutes_def)
    done
  done

lemma fc_update_ti:
  "⟦ fu_commutes (update_ti_t ti) h; fg_cons acc upd;
     ∀v bs bs'. upd bs (h bs' v) = h bs' (upd bs v); ∀bs v. acc (h bs v) = acc v  ⟧
   ⟹ fu_commutes (update_ti_t (adjust_ti t acc upd)) h"
  by (auto simp: fu_commutes_def update_ti_t_adjust_ti)

lemma (in c_type) fc_ti_typ_combine:
  "⟦ fu_commutes (update_ti_t ti) h; fg_cons acc upd;
     ∀v bs bs'. upd bs (h bs' v) = h bs' (upd bs v); ∀bs v. acc (h bs v) = acc v ⟧
   ⟹ fu_commutes (update_ti_t (ti_typ_combine (t::'a itself) acc upd algn fn ti)) h"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(rule fc_extend_ti, assumption)
  apply(rule fc_update_ti; simp)
  done

lemma fc_ti_pad_combine:
  "fu_commutes (update_ti_t ti) f ⟹ fu_commutes (update_ti_t (ti_pad_combine n ti)) f"
  apply(clarsimp simp: ti_pad_combine_def Let_def)
  apply(rule fc_extend_ti, assumption)
  apply(auto simp: fu_commutes_def padding_desc_def)
  done

lemma (in c_type) fc_ti_typ_pad_combine:
  "⟦ fu_commutes (update_ti_t ti) h; fg_cons acc upd;
     ∀v bs bs'. upd bs (h bs' v) = h bs' (upd bs v); ∀bs v. acc (h bs v) = acc v ⟧
   ⟹ fu_commutes (update_ti_t (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti)) h"
  apply(clarsimp simp: ti_typ_pad_combine_def Let_def)
  apply(rule conjI; clarsimp)
   apply(rule fc_ti_typ_combine; assumption?)
   apply(erule fc_ti_pad_combine)
  apply(erule (3) fc_ti_typ_combine)
  done

definition fu_eq_mask :: "'a xtyp_info ⇒ ('a ⇒ 'a) ⇒ bool" where
  "fu_eq_mask ti f ≡
     ∀bs v v'. length bs = size_td ti ⟶ update_ti_t ti bs (f v) = update_ti_t ti bs (f v')"

lemma fu_eq_mask:
  "⟦ length bs = size_td ti; fu_eq_mask ti id  ⟧ ⟹
      update_ti_t ti bs v = update_ti_t ti bs w"
 by (clarsimp simp: fu_eq_mask_def update_ti_t_def)

lemma fu_eq_mask_ti_pad_combine:
  "⟦ fu_eq_mask ti f; aggregate ti ⟧ ⟹ fu_eq_mask (ti_pad_combine n ti) f"
  unfolding ti_pad_combine_def Let_def
  apply(cases ti)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct, auto simp: fu_eq_mask_def update_ti_list_t_def padding_desc_def)
    done
  done

lemma fu_eq_mask_map_align: "fu_eq_mask t f ⟹ fu_eq_mask (map_align g t) f"
  by (cases t) (auto simp add: fu_eq_mask_def)

lemma fu_eq_mask_final_pad:
  "⟦ fu_eq_mask ti f; aggregate ti ⟧ ⟹ fu_eq_mask (final_pad algn ti) f"
  by(auto simp: final_pad_def Let_def fu_eq_mask_map_align fu_eq_mask_ti_pad_combine)

definition upd_local :: "('b ⇒ 'a ⇒ 'a) ⇒ bool" where
  "upd_local g ≡ ∀j k v v'. g k v = g k v' ⟶ g j v = g j v'"

lemma fg_cons_upd_local:
  "fg_cons f g ⟹ upd_local g"
  apply(clarsimp simp: fg_cons_def upd_local_def)
  subgoal for j k v v'
    apply(drule arg_cong [where f="g j"])
    apply simp
    done
  done

lemma (in mem_type) fu_eq_mask_ti_typ_combine:
  "⟦ fu_eq_mask ti (λv. (upd (acc undefined) (h v))); fg_cons acc upd;
      fu_commutes (update_ti_t ti) upd; aggregate ti ⟧ ⟹
      fu_eq_mask (ti_typ_combine (t::'a itself) acc upd algn fn ti) h"
  apply(frule fg_cons_upd_local)
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(cases ti)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct; clarsimp)
    subgoal for xs'
      apply(clarsimp simp: fu_eq_mask_def update_ti_t_adjust_ti)
      apply(clarsimp simp: update_ti_list_t_def size_of_def)
      apply(subst upd [where w="acc undefined"])
       apply(simp add: size_of_def)
      apply(subst upd [where w="acc undefined" and v="acc (h v')" for v'])
       apply(simp add: size_of_def)
      apply (smt (verit, ccfv_threshold) fu_commutes_def length_take min_ll upd_local_def)
      done
    done
  done

lemma (in mem_type) fu_eq_mask_ti_typ_pad_combine:
  "⟦ fu_eq_mask ti (λv. (upd (acc undefined) (h v))); fg_cons acc upd;
      fu_commutes (update_ti_t ti) upd; aggregate ti ⟧ ⟹
      fu_eq_mask (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) h"
  by (fastforce simp: ti_typ_pad_combine_def Let_def
                intro: fu_eq_mask_ti_typ_combine fu_eq_mask_ti_pad_combine fc_ti_pad_combine)

lemma fu_eq_mask_empty_typ_info_g:
  "∃k. ∀v. f v = k ⟹ fu_eq_mask t f"
  by (auto simp: fu_eq_mask_def)

lemma fu_eq_mask_empty_typ_info:
  "∀v. f v = undefined ⟹ fu_eq_mask t f"
 by (auto simp: fu_eq_mask_def)

lemma size_td_extend_ti:
  "aggregate s ⟹ size_td (extend_ti s t algn fn d) = size_td s + size_td t"
  apply (cases s) 
  subgoal for x1 typ_struct xs 
    apply (cases typ_struct; simp)
    done
  done

lemma size_td_ti_pad_combine:
  "aggregate ti ⟹ size_td (ti_pad_combine n ti) = n + size_td ti"
  unfolding ti_pad_combine_def Let_def by (simp add: size_td_extend_ti)

lemma size_td_map_align [simp]: "size_td (map_align f ti) = size_td ti"
  by (cases ti) auto

lemma align_of_dvd_size_of_final_pad [simp]:
  "aggregate ti ⟹ 2^align_td (final_pad algn ti) dvd size_td (final_pad algn ti)"
  unfolding final_pad_def Let_def
  apply (cases ti)
  apply (auto simp: size_td_ti_pad_combine ac_simps padup_dvd power_le_dvd  intro: dvd_padup_add)
  done

lemma size_td_lt_ti_pad_combine:
  "aggregate t ⟹ size_td (ti_pad_combine n t) = size_td t + n"
  by (metis add.commute size_td_ti_pad_combine)

lemma (in c_type) size_td_lt_ti_typ_combine:
  "aggregate ti ⟹
    size_td (ti_typ_combine (t::'a itself) f g algn fn ti) =
    size_td ti + size_td (typ_info_t TYPE('a))"
  by (clarsimp simp: ti_typ_combine_def Let_def size_td_extend_ti)

lemma (in c_type) size_td_lt_ti_typ_pad_combine:
  "aggregate ti  ⟹
      size_td (ti_typ_pad_combine (t::'a itself) f g algn fn ti) =
        (let k = size_td ti in
           k + size_td (typ_info_t TYPE('a)) + padup (2^(max algn (align_td (typ_info_t TYPE('a))))) k)"
  unfolding ti_typ_pad_combine_def Let_def
  by (auto simp: size_td_lt_ti_typ_combine size_td_ti_pad_combine align_of_def max_2_exp)

lemma size_td_lt_final_pad:
  "aggregate tag ⟹
   size_td (final_pad align tag) = (let k=size_td tag in k + padup (2^(max align (align_td tag))) k)"
  by (auto simp: final_pad_def Let_def size_td_ti_pad_combine)

lemma size_td_empty_typ_info [simp]:
  "size_td (empty_typ_info algn tn) = 0"
  by (clarsimp simp: empty_typ_info_def)

lemma wf_lf_empty_typ_info [simp]:
  "wf_lf {}"
  by (auto simp: wf_lf_def empty_typ_info_def)

lemma lf_fn_disj_fn:
  "fn ∉ set (field_names_list (TypDesc algn (TypAggregate xs) tn)) ⟹
   lf_fn ` lf_set_list xs [] ∩ lf_fn ` lf_set t [fn] = {}"
  apply(induct xs arbitrary: fn t tn, clarsimp)
  subgoal for  a list fn t tn
  apply(cases a, clarsimp)
  apply(drule meta_spec [where x=fn])
  apply(drule meta_spec [where  x=t])
  apply(drule meta_spec [where  x=tn])
  apply(drule meta_mp, fastforce simp: field_names_list_def split: if_split_asm)
  apply(safe)
   apply(fastforce dest!: lf_set_fn simp: field_names_list_def prefix_def less_eq_list_def
                  split: if_split_asm)
    by force
  done


lemma wf_lf_extend_ti:
  "⟦ wf_lf (lf_set t []); wf_lf (lf_set ti []); wf_desc t; fn ∉ set (field_names_list ti);
     ti_ind (lf_set ti []) (lf_set t []) ⟧ ⟹
   wf_lf (lf_set (extend_ti ti t algn fn d) [])"
  apply(cases ti)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct; clarsimp)
     apply(subst wf_lf_fn; simp)
    apply(subst wf_lf_list, erule lf_fn_disj_fn)
    apply(subst ti_ind_sym2)
    apply(subst ti_ind_fn)
    apply(subst ti_ind_sym2)
    apply clarsimp
    apply(subst wf_lf_fn; simp)
    done
  done

lemma wf_lf_ti_pad_combine:
  "wf_lf (lf_set ti []) ⟹ wf_lf (lf_set (ti_pad_combine n ti) [])"
  apply(clarsimp simp: ti_pad_combine_def Let_def padding_desc_def)
  apply(rule wf_lf_extend_ti)
      apply(clarsimp simp: wf_lf_def fd_cons_desc_def fd_cons_double_update_def
                           fd_cons_update_access_def fd_cons_access_update_def fd_cons_length_def)
     apply assumption
    apply(clarsimp)
   apply(rule foldl_append_nmem)
   apply clarsimp
  apply(clarsimp simp: ti_ind_def fu_commutes_def fa_fu_ind_def)
  done

lemma lf_set_map_align [simp]: "lf_set (map_align f ti) = lf_set ti"
  by (cases ti) auto

lemma wf_lf_final_pad:
  "wf_lf (lf_set ti []) ⟹ wf_lf (lf_set (final_pad algn ti) [])"
  by (auto simp: final_pad_def Let_def elim: wf_lf_ti_pad_combine)

lemma wf_lf_adjust_ti:
  "⟦ wf_lf (lf_set t []); ⋀v. g (f v) v = v;
      ⋀bs bs' v. g bs (g bs' v) = g bs v; ⋀bs v. f (g bs v) = bs ⟧
      ⟹ wf_lf (lf_set (adjust_ti t f g) [])"
  apply(clarsimp simp: wf_lf_def)
  apply(drule lf_set_adjust_ti; clarsimp)
  apply(rule conjI)
   apply(fastforce simp: fd_cons_desc_def fd_cons_double_update_def update_desc_def
                         fd_cons_update_access_def fd_cons_access_update_def fd_cons_length_def)
  apply(fastforce simp: fu_commutes_def update_desc_def fa_fu_ind_def dest!: lf_set_adjust_ti)
  done

lemma ti_ind_empty_typ_info [simp]:
  "ti_ind (lf_set (empty_typ_info algn tn) []) (lf_set (adjust_ti k f g) [])"
  by (clarsimp simp: ti_ind_def empty_typ_info_def)

lemma ti_ind_extend_ti:
  "⟦ ti_ind (lf_set t []) (lf_set (adjust_ti k acc upd) []);
      ti_ind (lf_set ti []) (lf_set (adjust_ti k acc upd) []) ⟧
      ⟹ ti_ind (lf_set (extend_ti ti t algn n d) []) (lf_set (adjust_ti k acc upd) [])"
  apply(cases ti)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct; clarsimp, subst ti_ind_fn, simp)
    done
  done

lemma ti_ind_ti_pad_combine:
  "ti_ind (lf_set ti []) (lf_set (adjust_ti k acc upd) []) ⟹
      ti_ind (lf_set (ti_pad_combine n ti) []) (lf_set (adjust_ti k acc upd) [])"
  apply(clarsimp simp: ti_pad_combine_def Let_def padding_desc_def)
  apply(rule ti_ind_extend_ti)
   apply(clarsimp simp: ti_ind_def fu_commutes_def fa_fu_ind_def)
  apply assumption
  done

definition acc_ind :: "('a ⇒ 'b) ⇒ 'a field_desc set ⇒ bool" where
  "acc_ind acc X ≡ ∀x bs v. x ∈ X ⟶ acc (field_update x bs v) = acc v"

definition fu_s_comm_k :: "'a leaf_desc set ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ bool" where
  "fu_s_comm_k X upd ≡ ∀x. x ∈ field_update ` lf_fd ` X ⟶ fu_commutes x upd"

definition upd_ind :: "'a leaf_desc set ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ bool" where
  "upd_ind X upd ≡ fu_s_comm_k X upd"

definition fa_ind :: "'a field_desc set ⇒ ('b ⇒ 'a ⇒ 'a) ⇒ bool" where
  "fa_ind X upd ≡ ∀x bs v. x ∈ X ⟶ field_access x (upd bs v) = field_access x v"

lemma lf_fd_fn:
  "∀fn. lf_fd ` (lf_set (t::'a xtyp_info) fn) = lf_fd ` (lf_set t [])"
  "∀fn. lf_fd ` (lf_set_struct (st::'a xtyp_info_struct) fn) = lf_fd ` (lf_set_struct st [])"
  "∀fn. lf_fd ` (lf_set_list (ts::'a xtyp_info_tuple list) fn) = lf_fd ` (lf_set_list ts [])"
  "∀fn. lf_fd ` (lf_set_tuple (x::'a xtyp_info_tuple) fn) = lf_fd ` (lf_set_tuple x [])"
  by (induct t and st and ts and x, all ‹clarsimp simp: image_Un›) metis+

lemma lf_set_empty_typ_info [simp]:
  "lf_set (empty_typ_info algn tn) fn = {}"
  by (clarsimp simp: empty_typ_info_def)

lemma upd_ind_empty [simp]:
  "upd_ind {} upd"
  by (clarsimp simp: upd_ind_def fu_s_comm_k_def)

lemma upd_ind_extend_ti:
  "⟦ upd_ind (lf_set s []) upd; upd_ind (lf_set t []) upd ⟧ ⟹
      upd_ind (lf_set (extend_ti s t algn fn d) []) upd"
  apply (cases s)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct)
    subgoal 
      apply (simp add:  upd_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    subgoal 
      apply (simp add:  upd_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    done
  done


lemma (in c_type) upd_ind_ti_typ_combine:
  "⟦ upd_ind (lf_set ti []) h; ⋀w u v. upd w (h u v) = h u (upd w v);
      ⋀w v. acc (h w v) = acc v; ⋀v. upd (acc v) v = v ⟧
      ⟹ upd_ind (lf_set (ti_typ_combine (t::'a itself) acc upd algn fn ti) []) h"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(erule upd_ind_extend_ti)
  apply(clarsimp simp: upd_ind_def fu_s_comm_k_def)
  apply(drule lf_set_adjust_ti)
   apply clarsimp
  apply(clarsimp simp: update_desc_def fu_commutes_def )
  done

lemma upd_ind_ti_pad_combine:
  "upd_ind ((lf_set ti [])) upd ⟹ upd_ind ((lf_set (ti_pad_combine n ti) [])) upd"
  apply(clarsimp simp: ti_pad_combine_def Let_def padding_desc_def)
  apply(erule upd_ind_extend_ti)
  apply(auto simp: upd_ind_def fu_s_comm_k_def fu_commutes_def)
  done

lemma (in c_type) upd_ind_ti_typ_pad_combine:
  "⟦ upd_ind (lf_set ti []) h; ⋀w u v. upd w (h u v) = h u (upd w v);
      ⋀w v. acc (h w v) = acc v; ⋀v. upd (acc v) v = v ⟧
      ⟹ upd_ind (lf_set (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) []) h"
  unfolding ti_typ_pad_combine_def Let_def
  by (fastforce intro!: upd_ind_ti_typ_combine upd_ind_ti_pad_combine)

lemma acc_ind_empty [simp]:
  "acc_ind acc {}"
  by (clarsimp simp: acc_ind_def)

lemma acc_ind_extend_ti:
  "⟦ acc_ind acc (lf_fd ` lf_set s []); acc_ind acc (lf_fd ` lf_set t []) ⟧ ⟹
      acc_ind acc (lf_fd ` lf_set (extend_ti s t algn fn d) [])"
  apply (cases s)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct)
    subgoal 
      apply (simp add: acc_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    subgoal 
      apply (simp add:  acc_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    done
  done

lemma (in c_type) acc_ind_ti_typ_combine:
  "⟦ acc_ind h (lf_fd ` lf_set ti []); ⋀v w. h (upd w v) = h v;
      ⋀v. upd (acc v) v = v  ⟧
      ⟹ acc_ind h (lf_fd ` lf_set (ti_typ_combine (t::'a itself) acc upd algn fn ti) [])"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(erule acc_ind_extend_ti)
  apply(clarsimp simp: acc_ind_def)
  apply(drule lf_set_adjust_ti)
   apply clarsimp
  apply(clarsimp simp: update_desc_def)
  done

lemma acc_ind_ti_pad_combine:
  "acc_ind acc (lf_fd ` (lf_set t [])) ⟹ acc_ind acc (lf_fd ` (lf_set (ti_pad_combine n t) []))"
  apply(clarsimp simp: ti_pad_combine_def Let_def padding_desc_def)
  apply(erule acc_ind_extend_ti)
  apply(auto simp: acc_ind_def)
  done

lemma (in c_type) acc_ind_ti_typ_pad_combine:
  "⟦ acc_ind h (lf_fd ` lf_set ti []); ⋀v w. h (upd w v) = h v; ⋀v. upd (acc v) v = v  ⟧
      ⟹ acc_ind h (lf_fd ` lf_set (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) [])"
  by (auto simp: ti_typ_pad_combine_def Let_def intro: acc_ind_ti_typ_combine acc_ind_ti_pad_combine)

lemma fa_ind_empty [simp]:
  "fa_ind {} upd"
  by (clarsimp simp: fa_ind_def)

lemma fa_ind_extend_ti:
  "⟦ fa_ind (lf_fd ` lf_set s []) upd; fa_ind (lf_fd ` lf_set t []) upd ⟧ ⟹
      fa_ind (lf_fd ` lf_set (extend_ti s t algn fn d) []) upd"
  apply (cases s)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct)
    subgoal 
      apply (simp add: fa_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    subgoal 
      apply (simp add:  fa_ind_def image_Un fu_s_comm_k_def )
      by (metis lf_fd_fn(1))
    done
  done
 
lemma (in c_type) fa_ind_ti_typ_combine:
  "⟦ fa_ind (lf_fd ` lf_set ti []) h; ⋀v w. acc (h w v) = acc v;
      ⋀v. upd (acc v) v = v   ⟧
      ⟹ fa_ind (lf_fd ` lf_set (ti_typ_combine (t::'a itself) acc upd algn fn ti) []) h"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(erule fa_ind_extend_ti)
  apply(clarsimp simp: fa_ind_def fu_s_comm_k_def)
  apply(drule lf_set_adjust_ti)
   apply clarsimp
  apply(clarsimp simp: update_desc_def fu_commutes_def)
  done

lemma fa_ind_ti_pad_combine:
  "fa_ind (lf_fd ` (lf_set ti [])) upd ⟹ fa_ind (lf_fd ` (lf_set (ti_pad_combine n ti) [])) upd"
  apply(clarsimp simp: ti_pad_combine_def Let_def padding_desc_def)
  apply(erule fa_ind_extend_ti)
  apply(auto simp: fa_ind_def)
  done

lemma (in c_type) fa_ind_ti_typ_pad_combine:
  "⟦ fa_ind (lf_fd ` lf_set ti []) h; ⋀v w. f (h w v) = f v;
      ⋀v. g (f v) v = v   ⟧
      ⟹ fa_ind (lf_fd ` lf_set (ti_typ_pad_combine (t::'a itself) f g algn fn ti) []) h"
  by (auto simp: ti_typ_pad_combine_def Let_def intro: fa_ind_ti_typ_combine fa_ind_ti_pad_combine)

lemma (in wf_type) wf_lf_ti_typ_combine:
  "⟦ wf_lf (lf_set ti []); fn ∉ set (field_names_list ti);
      ⋀v. upd (acc v) v = v; ⋀w u v. upd w (upd u v) = upd w v;
      ⋀w v. acc (upd w v) = w;
      upd_ind (lf_set ti []) upd; acc_ind acc (lf_fd ` lf_set ti []);
      fa_ind (lf_fd ` lf_set ti []) upd ⟧ ⟹
      wf_lf (lf_set (ti_typ_combine (t::'a itself) acc upd algn fn ti) [])"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(rule wf_lf_extend_ti; simp?)
   apply(rule wf_lf_adjust_ti; simp)
  apply(clarsimp simp: ti_ind_def)
  apply(drule lf_set_adjust_ti, simp)
  apply(clarsimp simp: fu_commutes_def update_desc_def upd_ind_def acc_ind_def fu_s_comm_k_def
                       fa_fu_ind_def fa_ind_def)
  done

lemma (in wf_type) wf_lf_ti_typ_pad_combine:
  "⟦ wf_lf (lf_set ti []); fn ∉ set (field_names_list ti); hd fn ≠ CHR ''!'';
      ⋀v. upd (acc v) v = v; ⋀w u v. upd w (upd u v) = upd w v;
      ⋀w v. acc (upd w v) = w;
      upd_ind (lf_set ti []) upd; acc_ind acc (lf_fd ` lf_set ti []);
      fa_ind (lf_fd ` lf_set ti []) upd ⟧ ⟹
      wf_lf (lf_set (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) [])"
  apply(clarsimp simp: ti_typ_pad_combine_def Let_def)
  apply (fastforce intro!: wf_lf_ti_typ_combine wf_lf_ti_pad_combine upd_ind_ti_pad_combine
                           acc_ind_ti_pad_combine fa_ind_ti_pad_combine)
  done

definition "upd_fa_ind X upd  ≡  upd_ind X upd ∧ fa_ind (lf_fd ` X) upd"

lemma (in wf_type) wf_lf_ti_typ_pad_combine':
  "⟦ wf_lf (lf_set ti []); fn ∉ set (field_names_list ti); hd fn ≠ CHR ''!'';
      ⋀v. upd (acc v) v = v; ⋀w u v. upd w (upd u v) = upd w v;
      ⋀w v. acc (upd w v) = w;
      upd_fa_ind (lf_set ti []) upd; acc_ind acc (lf_fd ` lf_set ti [])⟧
  ⟹
      wf_lf (lf_set (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) [])"
  unfolding upd_fa_ind_def
  by (erule conjE) (rule wf_lf_ti_typ_pad_combine)


lemma (in c_type) upd_fa_ind_ti_typ_pad_combine:
"⟦ upd_fa_ind (lf_set ti []) h; ⋀w u v. upd w (h u v) = h u (upd w v);
      ⋀w v. acc (h w v) = acc v; ⋀v. upd (acc v) v = v ⟧
      ⟹ upd_fa_ind (lf_set (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti) []) h"
  unfolding upd_fa_ind_def
  by (auto intro: upd_ind_ti_typ_pad_combine fa_ind_ti_typ_pad_combine)

lemma upd_fa_ind_empty [simp]:
  "upd_fa_ind {} h"
  by (simp add: upd_fa_ind_def)

lemma wf_align_empty_typ_info: "wf_align (empty_typ_info algn tn)"
  by (simp add: wf_align_def empty_typ_info_def)

lemma wf_align_list: "wf_align t ⟹ wf_align_list fs ⟹  wf_align_list (fs @ [DTuple t f d])"
  by (induct fs) auto
lemma wf_align_struct: "wf_align t ⟹ wf_align_struct st ⟹ wf_align_struct (extend_ti_struct st t f d)"
  apply (cases st)
   apply simp
  apply (simp add: wf_align_list)
  done

lemma align_td_extend_ti: "align_td (extend_ti tag t algn f d) = max (align_td tag) (max algn (align_td t))"
  apply (cases tag)
  apply (simp)
  done

lemma align_td_struct_extend_ti: "aggregate_struct st ⟹
  align_td_struct (extend_ti_struct st t f d) = max (align_td_struct st) (align_td t)"
  by (cases st) auto
lemma wf_align_extend_ti':
  assumes wf_t: "wf_align t"
  assumes agg: "aggregate tag"
  assumes wf_tag: "wf_align tag"
  shows "wf_align (extend_ti tag t algn f d)"
proof (cases tag)
  case (TypDesc algn' st n)
  with wf_tag agg obtain le: "align_td_wo_align_struct st ≤ algn'"
   and le': "align_td_struct st ≤ algn'"
   and wf_st: "wf_align_struct st"
   and agg_st: "aggregate_struct st" by auto
  from wf_align_struct [OF wf_t wf_st]
  have wf_st: "wf_align_struct (extend_ti_struct st t f d)" .
  from align_td_wo_align_le_align_td (2) [OF this]
  have "align_td_wo_align_struct (extend_ti_struct st t f d) ≤ align_td_struct (extend_ti_struct st t f d)" .
  also from align_td_struct_extend_ti [OF agg_st]
  have "… = max (align_td_struct st) (align_td t)" .
  finally
  have "align_td_wo_align_struct (extend_ti_struct st t f d) ≤ max algn' (max algn (align_td t))"
    using le'
    by (metis (full_types) le_max_iff_disj max.orderE)
  moreover from align_td_struct_extend_ti [OF agg_st] le'
  have "align_td_struct (extend_ti_struct st t f d) ≤ max algn' (max algn (align_td t))"
    by (metis max.cobounded2 max.mono )
  ultimately show ?thesis
    by (simp add: TypDesc wf_st)
qed

lemma (in mem_type) wf_align_extend_ti:
  assumes agg: "aggregate tag"
  assumes wf_tag: "wf_align tag"
  shows "wf_align (extend_ti tag (typ_info_t (TYPE('a))) algn f d)"
proof -
  have "wf_align (typ_info_t (TYPE('a)))" by (rule wf_align)
  from wf_align_extend_ti' [OF this agg wf_tag] show ?thesis .
qed

lemma wf_align_map_td [simp]:
"wf_align (map_td f g d) = wf_align d"
"wf_align_struct (map_td_struct f g ts) = wf_align_struct (ts)"
"wf_align_list (map_td_list f g fs) = wf_align_list fs"
"wf_align_tuple (map_td_tuple f g fd) = wf_align_tuple fd"
  by (induct d and ts and fs and fd) auto

lemma wf_align_adjust_ti[simp]: "wf_align (adjust_ti t acc upd) = wf_align t"
  by (simp add: adjust_ti_def)

lemma (in mem_type) wf_align_ti_typ_combine:
 "aggregate tag ⟹ wf_align tag ⟹ wf_align (ti_typ_combine (TYPE('a)) acc upd algn fn tag)"
  apply (simp add: ti_typ_combine_def Let_def)
  apply (rule wf_align_extend_ti')
    apply (simp add: wf_align)
   apply assumption
  apply assumption
  done

lemma wf_align_ti_pad_combine:
 "aggregate tag ⟹ wf_align tag ⟹ wf_align (ti_pad_combine n tag)"
  apply (simp add: ti_pad_combine_def Let_def)
  apply (rule wf_align_extend_ti')
    apply simp
   apply assumption
  apply assumption
  done

lemma (in mem_type) wf_align_ti_typ_pad_combine:
 "aggregate tag ⟹ wf_align tag ⟹ wf_align (ti_typ_pad_combine (TYPE('a)) acc upd algn fn tag)"
  by (simp add: ti_typ_pad_combine_def Let_def wf_align_ti_pad_combine wf_align_ti_typ_combine)

lemma wf_align_map_align:
  assumes wf_tag: "wf_align tag"
  assumes mono: "⋀a. a ≤ f a"
  shows "wf_align (map_align f tag)"
  using wf_tag mono
  apply (cases tag)
  using order_trans apply auto
  done

lemma wf_align_final_pad: "aggregate tag ⟹ wf_align tag ⟹ wf_align (final_pad algn tag)"
  by (auto simp add: final_pad_def Let_def max_2_exp wf_align_map_align wf_align_ti_pad_combine)

lemmas wf_align_simps =
  wf_align_empty_typ_info
  wf_align_ti_typ_pad_combine
  wf_align_ti_typ_combine
  wf_align_ti_pad_combine
  wf_align_final_pad

lemma align_field_empty_typ_info [simp]:
  "align_field (empty_typ_info algn tn)"
  by (clarsimp simp: empty_typ_info_def align_field_def)

lemma align_td_wo_align_field_lookup:
  "∀f m s n. field_lookup (t::('a,'b) typ_desc) f m = Some (s,n) ⟶ align_td_wo_align s ≤ align_td_wo_align t"
  "∀f m s n. field_lookup_struct (st::('a,'b) typ_struct) f m = Some (s,n) ⟶ align_td_wo_align s ≤ align_td_wo_align_struct st"
  "∀f m s n. field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some (s,n) ⟶ align_td_wo_align s ≤ align_td_wo_align_list ts"
  "∀f m s n. field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some (s,n) ⟶ align_td_wo_align s ≤ align_td_wo_align_tuple x"
  by (induct t and st and ts and x, all ‹clarsimp›)
     (fastforce simp: max_def split: option.splits)

lemma align_td_field_lookup[rule_format]:
  "∀f m s n. wf_align t ⟶ field_lookup (t::('a,'b) typ_desc) f m = Some (s,n) ⟶ align_td s ≤ align_td t"
  "∀f m s n. wf_align_struct st ⟶ field_lookup_struct (st::('a,'b) typ_struct) f m = Some (s,n) ⟶ align_td s ≤ align_td_struct st"
  "∀f m s n. wf_align_list ts ⟶ field_lookup_list (ts::('a,'b) typ_tuple list) f m = Some (s,n) ⟶ align_td s ≤ align_td_list ts"
  "∀f m s n. wf_align_tuple x ⟶ field_lookup_tuple (x::('a,'b) typ_tuple) f m = Some (s,n) ⟶ align_td s ≤ align_td_tuple x"
  apply (induct t and st and ts and x, all ‹clarsimp›)
    apply  (fastforce simp: max_def split: option.splits)+
  done

lemma (in mem_type) align_td_field_lookup_mem_type: "field_lookup (typ_info_t (TYPE('a))) f m = Some (s, n) ⟹
  align_td s ≤ align_td (typ_info_t (TYPE('a)))"
  apply (rule align_td_field_lookup(1))
   apply (rule wf_align)
  apply simp
  done

lemma align_field_extend_ti:
  "⟦ align_field s; align_field t; wf_align t;  2^(align_td t) dvd size_td s ⟧ ⟹
      align_field (extend_ti s t algn fn d)"
  apply(cases s, clarsimp)
  subgoal for x1 typ_struct xs
    apply(cases typ_struct, clarsimp)
     apply(clarsimp simp: align_field_def split: option.splits)
    apply(clarsimp simp: align_field_def)
    apply(subst (asm) field_lookup_list_append)
    apply(clarsimp split: if_split_asm option.splits)
    subgoal for x2 f s n
      apply(cases f, clarsimp)
      apply clarsimp
      apply(frule field_lookup_offset2)
      apply (meson align_td_field_lookup(1) dvd_diffD field_lookup_offset_le(1) power_le_dvd)
      done
    subgoal for x2 f s n
      by(cases f) auto       
    done
  done

lemma align_field_ti_pad_combine:
  "align_field ti ⟹ align_field (ti_pad_combine n ti)"
  apply(clarsimp simp: ti_pad_combine_def Let_def)
  apply(erule align_field_extend_ti)
   apply(clarsimp simp: align_field_def)
   apply clarsimp
  apply clarsimp
  done

lemma align_field_map_align [simp]: "align_field (map_align f t)  = align_field t"
  by (cases t) (auto simp add: align_field_def)

lemma align_field_final_pad:
  "align_field ti ⟹ align_field (final_pad algn ti)"
  apply(clarsimp simp: final_pad_def Let_def split: if_split_asm)
  apply(erule align_field_ti_pad_combine)
  done

lemma field_lookup_adjust_ti_None:
  "∀fn m s n. field_lookup (adjust_ti t acc upd) fn m = None ⟶
      (field_lookup t fn m = None)"
  "∀fn m s n. field_lookup_struct (map_td_struct (λn algn. update_desc acc upd) (update_desc acc upd) st)
        fn m = None ⟶
        (field_lookup_struct st fn m = None)"
  "∀fn m s n. field_lookup_list (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) fn m = None ⟶
        (field_lookup_list ts fn m = None)"
  "∀fn m s n. field_lookup_tuple (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) fn m = None ⟶
        (field_lookup_tuple x fn m = None)"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: adjust_ti_def split: option.splits)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by auto
next
  case (TypAggregate list)
  then show ?case by auto
next
  case Nil_typ_desc
  then show ?case by auto
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case
    apply (clarsimp simp: adjust_ti_def split: option.splits)
    apply (cases dt_tuple)
    apply clarsimp
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by (clarsimp simp: adjust_ti_def split: option.splits)
qed

lemma field_lookup_adjust_ti' [rule_format]:
  "∀fn m s n. field_lookup (adjust_ti t acc upd) fn m = Some (s,n) ⟶
      (∃s'. field_lookup t fn m = Some (s',n) ∧ align_td_wo_align s = align_td_wo_align s')"
  "∀fn m s n. field_lookup_struct (map_td_struct (λn algn. update_desc acc upd) (update_desc acc upd) st)
        fn m = Some (s,n) ⟶
        (∃s'. field_lookup_struct st fn m = Some (s',n) ∧ align_td_wo_align s = align_td_wo_align s')"
  "∀fn m s n. field_lookup_list (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) fn m = Some (s,n) ⟶
        (∃s'. field_lookup_list ts fn m = Some (s',n) ∧ align_td_wo_align s = align_td_wo_align s')"
  "∀fn m s n. field_lookup_tuple (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) fn m = Some (s,n) ⟶
        (∃s'. field_lookup_tuple x fn m = Some (s',n) ∧ align_td_wo_align s = align_td_wo_align s')"
proof (induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: adjust_ti_def)
next
  case (TypScalar nat1 nat2 a)
  then show ?case by (clarsimp simp: adjust_ti_def)
next
  case (TypAggregate list)
  then show ?case by (clarsimp simp: adjust_ti_def)
next
  case Nil_typ_desc
  then show ?case by (clarsimp simp: adjust_ti_def)
next
  case (Cons_typ_desc dt_tuple list)
  then show ?case 
    apply (clarsimp simp: adjust_ti_def)
    apply(clarsimp split: option.splits)
     apply(rule conjI; clarsimp)
      apply(cases dt_tuple, clarsimp)
     apply(cases dt_tuple, clarsimp split: if_split_asm)
    subgoal for fn
      apply(drule spec [where x=fn])
      apply clarsimp
      apply(fold adjust_ti_def)
      apply(subst (asm) field_lookup_adjust_ti_None; simp)
      done
    apply fastforce
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by (clarsimp simp: adjust_ti_def)
qed

lemma field_lookup_adjust_ti''' [rule_format]:
  "∀fn m s n. field_lookup (adjust_ti t acc upd) fn m = Some (s,n) ⟶
      (∃s'. field_lookup t fn m = Some (s',n) ∧ align_td s = align_td s')"
  "∀fn m s n. field_lookup_struct (map_td_struct (λn algn. update_desc acc upd) (update_desc acc upd) st)
        fn m = Some (s,n) ⟶
        (∃s'. field_lookup_struct st fn m = Some (s',n) ∧ align_td s = align_td s')"
  "∀fn m s n. field_lookup_list (map_td_list (λn algn. update_desc acc upd) (update_desc acc upd) ts) fn m = Some (s,n) ⟶
        (∃s'. field_lookup_list ts fn m = Some (s',n) ∧ align_td s = align_td s')"
  "∀fn m s n. field_lookup_tuple (map_td_tuple (λn algn. update_desc acc upd) (update_desc acc upd) x) fn m = Some (s,n) ⟶
        (∃s'. field_lookup_tuple x fn m = Some (s',n) ∧ align_td s = align_td s')"
proof(induct t and st and ts and x)
  case (TypDesc nat typ_struct list)
  then show ?case by (clarsimp simp: adjust_ti_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 simp: adjust_ti_def)
    apply(clarsimp split: option.splits)
     apply(rule conjI; clarsimp)
      apply(cases dt_tuple, clarsimp)
     apply(cases dt_tuple, clarsimp split: if_split_asm)
    subgoal for fn
      apply(drule spec [where x=fn])
      apply clarsimp
      apply(fold adjust_ti_def)
      apply(subst (asm) field_lookup_adjust_ti_None; simp)
      done
    apply fastforce
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case  by(clarsimp simp: adjust_ti_def)
qed

lemma field_lookup_adjust_ti:
  "⟦ field_lookup (adjust_ti t acc upd) fn m = Some (s,n) ⟧ ⟹
      (∃s'. field_lookup t fn m = Some (s',n) ∧ align_td_wo_align s = align_td_wo_align s')"
  by (rule field_lookup_adjust_ti')

lemma field_lookup_adjust_ti1:
  "⟦ field_lookup (adjust_ti t acc upd) fn m = Some (s,n) ⟧ ⟹
      (∃s'. field_lookup t fn m = Some (s',n) ∧ align_td s = align_td s')"
  by (rule field_lookup_adjust_ti''')

lemma align_adjust_ti:
  "align_field ti ⟹ align_field (adjust_ti ti acc upd)"
  apply(clarsimp simp: align_field_def)
  apply(drule field_lookup_adjust_ti1)
  apply clarsimp
  done

lemma (in mem_type) align_field_ti_typ_combine:
  "⟦ align_field ti; 2 ^ align_td (typ_info_t TYPE('a)) dvd size_td ti ⟧ ⟹
   align_field (ti_typ_combine (t::'a itself) acc upd algn fn ti)"
  apply(clarsimp simp: ti_typ_combine_def Let_def)
  apply(rule align_field_extend_ti, assumption)
   apply(rule align_adjust_ti)
   apply(rule align_field)
   apply (simp add: wf_align)
  apply simp
  done

lemma (in mem_type) align_td_wo_align_type_info_t_le_align_td:
  "align_td_wo_align (typ_info_t TYPE('a)) ≤ align_td (typ_info_t TYPE('a))"
proof -
  have "wf_align (typ_info_t TYPE('a))" by (rule wf_align)
  then show ?thesis thm wf_align.wfal0 by (rule align_td_wo_align_le_align_td(1))
qed

lemma (in mem_type) align_field_ti_typ_pad_combine:
  "⟦wf_align ti; align_field ti; aggregate ti⟧ ⟹
   align_field (ti_typ_pad_combine (t::'a itself) acc upd algn fn ti)"

  unfolding ti_typ_pad_combine_def Let_def
  apply (rule align_field_ti_typ_combine)
  subgoal
    apply clarsimp
    apply (rule align_field_ti_pad_combine)
    apply assumption
    done
  apply clarsimp
  apply (rule conjI)
  subgoal
    apply (clarsimp simp add: align_of_def)
    apply (metis (no_types, lifting) align_td_wo_align_type_info_t_le_align_td dvd_padup_add max.cobounded2 max_2_exp
     power_le_dvd size_td_lt_ti_pad_combine zero_less_numeral zero_less_power)
    done
  apply (clarsimp simp add: align_of_def)
  by (simp add: max_2_exp padup_dvd power_le_dvd)

lemma npf_extend_ti [simp]:
  "non_padding_fields (extend_ti s t algn fn d) = non_padding_fields s @
      (if hd fn = CHR ''!'' then [] else [fn])"
  apply (cases s)
  subgoal for x1 typ_struct xs
    apply (cases typ_struct; simp)
    done
  done

lemma npf_ti_pad_combine [simp]:
  "non_padding_fields (ti_pad_combine n tag) = non_padding_fields tag"
  by (clarsimp simp: ti_pad_combine_def Let_def)

lemma (in c_type) npf_ti_typ_combine [simp]:
  "hd fn ≠ CHR ''!'' ⟹
   non_padding_fields (ti_typ_combine (t::'a itself) acc upd algn fn tag) = non_padding_fields tag @ [fn]"
  by (clarsimp simp: ti_typ_combine_def Let_def)

lemma (in c_type) npf_ti_typ_pad_combine [simp]:
  "hd fn ≠ CHR ''!'' ⟹
   non_padding_fields (ti_typ_pad_combine (t::'a itself) acc upd algn fn tag) = non_padding_fields tag @ [fn]"
  by (clarsimp simp: ti_typ_pad_combine_def Let_def)

lemma non_padding_fields_map_align [simp]:
 "non_padding_fields (map_align f t) = non_padding_fields t"
  by (cases t) simp

lemma npf_final_pad [simp]:
  "non_padding_fields (final_pad algn tag) = non_padding_fields tag"
  by (clarsimp simp: final_pad_def Let_def)

lemma npf_empty_typ_info [simp]:
  "non_padding_fields (empty_typ_info algn tn) = []"
  by (clarsimp simp: empty_typ_info_def)

definition field_fd' :: "'a xtyp_info ⇒ qualified_field_name ⇀ 'a field_desc" where
  "field_fd' t f ≡ case field_lookup t f 0 of None ⇒ None | Some x ⇒ Some (field_desc (fst x))"

lemma padup_zero [simp]:
  "padup n 0 = 0"
  by (clarsimp simp: padup_def)

lemma padup_same [simp]:
  "padup n n = 0"
  by (clarsimp simp: padup_def)

lemmas size_td_simps_0 = size_td_lt_final_pad size_td_lt_ti_typ_pad_combine

lemmas size_td_simps_1 = size_td_simps_0
                         aggregate_ti_typ_pad_combine aggregate_empty_typ_info

lemmas size_td_simps_2 = padup_def align_of_final_pad align_of_def

lemmas size_td_simps = size_td_simps_1 size_td_simps_2

lemmas size_td_simps_3 = size_td_simps_0 size_td_simps_2


lemma fu_commutes_sym: "fu_commutes x y = fu_commutes y x"
  by (auto simp add: fu_commutes_def)

(*fixme: remove unused? *)
lemma wf_lf_insert_recursion:
  assumes wf_D:  "wf_lf D"
  assumes cons_x: "fd_cons_desc (lf_fd x) (lf_sz x)"
  assumes comm_D: "⋀y. y ∈ D ⟹ fu_commutes (field_update (lf_fd x)) (field_update (lf_fd y)) ∧
            fa_fu_ind (lf_fd x) (lf_fd y) (lf_sz y) (lf_sz x) ∧
            fa_fu_ind (lf_fd y) (lf_fd x) (lf_sz x) (lf_sz y)"
  shows "wf_lf (insert x D)"
proof -
  have comm_x_D:
   "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd y))" and
   "fa_fu_ind (lf_fd x') (lf_fd y) (lf_sz y) (lf_sz x')"
    if x'_in: "x' ∈ insert x D" and y_in: "y ∈ insert x D" and neq: "lf_fn y ≠ lf_fn x'"
    for x' and y
  proof - (*(induct "x' = x")*)
    show "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd y))"
      proof (cases "x' = x")
        case True
        from True y_in neq comm_D x'_in show ?thesis
          by auto
      next
        case False
        note neq_x'_x = this
        with x'_in have x'_D: "x' ∈ D"
          by auto
        from comm_D [OF this] have "fu_commutes (field_update (lf_fd x)) (field_update (lf_fd x'))"
          by auto
        with fu_commutes_sym have comm_x'_x: "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd x))"
          by auto
        from neq have neq': "y ≠ x'"
          by auto
        show ?thesis
        proof (cases "y = x")
          case True
          with comm_x'_x show ?thesis by simp
        next
          case False
          from False y_in have y_D: "y ∈ D" by simp
          with x'_D neq wf_D
          show ?thesis
            by (auto simp add: wf_lf_def)
        qed
      qed
    next
      show "fa_fu_ind (lf_fd x') (lf_fd y) (lf_sz y) (lf_sz x')"
      proof (cases "x' = x")
        case True
        from True y_in neq comm_D x'_in show ?thesis
          by auto
      next
        case False
        note neq_x'_x = this
        with x'_in have x'_D: "x' ∈ D"
          by auto
        from comm_D [OF this] have "fa_fu_ind (lf_fd x) (lf_fd x') (lf_sz x') (lf_sz x)" and
            fa_fu_x'_x: "fa_fu_ind (lf_fd x') (lf_fd x) (lf_sz x) (lf_sz x')" by auto
        from neq have neq': "y ≠ x'"
          by auto
        show ?thesis
        proof (cases "y = x")
          case True
          with fa_fu_x'_x show ?thesis by simp
        next
          case False
          from False y_in have y_D: "y ∈ D" by simp
          with x'_D neq wf_D
          show ?thesis
            by (auto simp add: wf_lf_def)
        qed
      qed
    qed
    with cons_x wf_D
    show ?thesis
      by (auto simp add: wf_lf_def)
qed


(*fixme: remove unused? *)
lemma wf_lf_insert_recursion':
  assumes cons_x: "fd_cons_desc (lf_fd x) (lf_sz x)"
  assumes comm_D: "⋀y. y ∈ D ⟹ fu_commutes (field_update (lf_fd x)) (field_update (lf_fd y)) ∧
            fa_fu_ind (lf_fd x) (lf_fd y) (lf_sz y) (lf_sz x) ∧
            fa_fu_ind (lf_fd y) (lf_fd x) (lf_sz x) (lf_sz y)"
  assumes wf_D:  "wf_lf D"
  shows "wf_lf (insert x D)"
  using wf_D cons_x comm_D
  by (rule wf_lf_insert_recursion)

(*fixme: remove unused? *)
lemma wf_lf_insert_recursion'':
  assumes wf_D:  "wf_lf D"
  assumes cons_x: "fd_cons_desc (lf_fd x) (lf_sz x)"
  assumes comm_D: "⋀y. y ∈ D ⟹ lf_fn y ≠ lf_fn x ⟹ fu_commutes (field_update (lf_fd x)) (field_update (lf_fd y)) ∧
            fa_fu_ind (lf_fd x) (lf_fd y) (lf_sz y) (lf_sz x) ∧
            fa_fu_ind (lf_fd y) (lf_fd x) (lf_sz x) (lf_sz y)"
  shows "wf_lf (insert x D)"
proof -
  have comm_x_D:
   "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd y))" and
   "fa_fu_ind (lf_fd x') (lf_fd y) (lf_sz y) (lf_sz x')"
    if x'_in: "x' ∈ insert x D" and y_in: "y ∈ insert x D" and neq: "lf_fn y ≠ lf_fn x'"
    for x' and y
  proof - (*(induct "x' = x")*)
    show "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd y))"
      proof (cases "x' = x")
        case True
        from True y_in neq comm_D x'_in show ?thesis
          by auto
      next
        case False
        note neq_x'_x = this
        with x'_in have x'_D: "x' ∈ D"
          by auto
        from neq have neq': "y ≠ x'"
          by auto
        show ?thesis
        proof (cases "y = x")
          case True
          with neq neq_x'_x neq'
          have "lf_fn x' ≠ lf_fn x" by simp
          from comm_D [OF x'_D this]  have "fu_commutes (field_update (lf_fd x)) (field_update (lf_fd x'))"
            by auto
          with fu_commutes_sym have comm_x'_x: "fu_commutes (field_update (lf_fd x')) (field_update (lf_fd x))"
            by auto
          from True comm_x'_x show ?thesis by simp
        next
          case False
          from False y_in have y_D: "y ∈ D" by simp
          with x'_D neq wf_D
          show ?thesis
            by (auto simp add: wf_lf_def)
        qed
      qed
    next
      show "fa_fu_ind (lf_fd x') (lf_fd y) (lf_sz y) (lf_sz x')"
      proof (cases "x' = x")
        case True
        from True y_in neq comm_D x'_in show ?thesis
          by auto
      next
        case False
        note neq_x'_x = this
        with x'_in have x'_D: "x' ∈ D"
          by auto
        from neq have neq': "y ≠ x'"
          by auto
        show ?thesis
        proof (cases "y = x")
          case True
          with neq neq_x'_x neq'
          have "lf_fn x' ≠ lf_fn x" by simp
          from comm_D [OF x'_D this] have "fa_fu_ind (lf_fd x) (lf_fd x') (lf_sz x') (lf_sz x)" and
            fa_fu_x'_x: "fa_fu_ind (lf_fd x') (lf_fd x) (lf_sz x) (lf_sz x')" by auto
          from True fa_fu_x'_x show ?thesis by simp
        next
          case False
          from False y_in have y_D: "y ∈ D" by simp
          with x'_D neq wf_D
          show ?thesis
            by (auto simp add: wf_lf_def)
        qed
      qed
    qed
    with cons_x wf_D
    show ?thesis
      by (auto simp add: wf_lf_def)
  qed


lemma wf_field_desc_empty [simp]:
"wf_field_desc ⦇field_access = λv bs. [], field_update = λbs. id, field_sz = 0⦈"
  by (unfold_locales) (auto simp add: padding_base.eq_padding_def padding_base.eq_upto_padding_def)


lemma field_desc_independent_subset:
  "D ⊆ E ⟹ field_desc_independent acc upd E ⟹ field_desc_independent acc upd D"
  by (auto simp add: field_desc_independent_def)

lemma field_desc_independent_union_iff:
 "field_desc_independent acc upd (D ∪ E) =
   (field_desc_independent acc upd D ∧ field_desc_independent acc upd E)"
  by (auto simp add: field_desc_independent_def)

lemma field_desc_independent_unionI:
 "field_desc_independent acc upd D ⟹ field_desc_independent acc upd E ⟹
  field_desc_independent acc upd (D ∪ E)"
  by (simp add: field_desc_independent_union_iff)

lemma field_desc_independent_unionD1:
 "field_desc_independent acc upd (D ∪ E) ⟹
   field_desc_independent acc upd D"
  by (simp add: field_desc_independent_union_iff)

lemma field_desc_independent_unionD2:
 "field_desc_independent acc upd (D ∪ E) ⟹
   field_desc_independent acc upd E"
  by (simp add: field_desc_independent_union_iff)

lemma field_desc_independent_insert_iff:
  "field_desc_independent acc upd (insert d D) =
    (field_desc_independent acc upd {d} ∧ field_desc_independent acc upd D)"
  apply (subst insert_is_Un)
  apply (simp only: field_desc_independent_union_iff)
  done

lemma field_desc_independent_insertI:
  "field_desc_independent acc upd {d} ⟹ field_desc_independent acc upd D ⟹
   field_desc_independent acc upd (insert d D)"
  apply (subst insert_is_Un)
  apply (simp only: field_desc_independent_union_iff)
  done

lemma field_desc_independent_insertD1:
  assumes ins: "field_desc_independent acc upd (insert d D)"
  shows "field_desc_independent acc upd {d}"
proof -
  from ins have "field_desc_independent acc upd ({d} ∪ D)"
    by (simp)
  from field_desc_independent_unionD1 [OF this]
  show ?thesis .
qed

lemma field_desc_independent_insertD2:
  assumes ins: "field_desc_independent acc upd (insert d D)"
  shows "field_desc_independent acc upd D"
proof -
  from ins have "field_desc_independent acc upd ({d} ∪ D)"
    by (simp)
  from field_desc_independent_unionD2 [OF this]
  show ?thesis .
qed



lemma field_descs_independent_append_first: "field_descs_independent (xs @ ys) ⟹ field_descs_independent xs"
  by (induct xs arbitrary: ys) (auto intro: field_desc_independent_subset)

lemma field_descs_independent_append_second: "field_descs_independent (xs @ ys) ⟹ field_descs_independent ys"
  by (induct xs arbitrary: ys) (auto intro: field_desc_independent_subset)

lemma field_descs_independent_append_first_ind:
 "field_descs_independent (xs @ ys) ⟹ x ∈ set xs ⟹
       field_desc_independent (field_access x) (field_update x) (set ys)"
by (induct xs arbitrary: ys) (auto simp add: field_desc_independent_union_iff)

lemma field_descs_independent_appendI1:
 "field_descs_independent xs ⟹ field_descs_independent ys ⟹
 (∀x ∈ set xs. field_desc_independent (field_access x) (field_update x) (set ys)) ⟹
 field_descs_independent (xs @ ys)"