Theory AutoCorres2.TypHeapLib

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

chapter "Misc. Lemmas"

theory TypHeapLib
imports "CTranslation"
begin

(* This file contains everything you need to know and use for the
   day-to-day solving of TypHeap related goals.  See KernelState.thy for
   abbreviations for cslift etc. *)

section "Abbreviations and helpers"

(* The idea here is to make sure that all abbreviations have defs that let you know they are an abbrev. *)
definition "is_an_abbreviation ≡ True"

(* specialised to c_guard *)
abbreviation
  "clift ≡ lift_t c_guard"

lemma clift_def: "is_an_abbreviation" by (simp add: is_an_abbreviation_def)

section "Basic operations"

subsection "clift"

lemma c_guard_clift:
  "clift hp p = Some x ⟹ c_guard p"
  by (rule lift_t_g)

lemma clift_heap_update:
  fixes p :: "'a :: mem_type ptr"
  shows "hrs_htd hp ⊨⇩t p ⟹ clift (hrs_mem_update (heap_update p v) hp) = (clift hp)(p ↦ v)"
  unfolding hrs_mem_update_def
  apply (cases hp)
  apply (simp add: split_def hrs_htd_def)
  apply (erule lift_t_heap_update)
  done

lemma clift_heap_update_same:
  fixes p :: "'a :: mem_type ptr"
  shows "⟦ hrs_htd hp ⊨⇩t p; typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b) ⟧
  ⟹ clift (hrs_mem_update (heap_update p v) hp) = (clift hp :: 'b :: mem_type typ_heap)"
  unfolding hrs_mem_update_def
  apply (cases hp)
  apply (simp add: split_def hrs_htd_def)
  apply (erule lift_t_heap_update_same)
  apply simp
  done

lemmas clift_heap_update_same_td_name = clift_heap_update_same [OF _  tag_disj_via_td_name, unfolded pad_typ_name_def]

subsection "\<^const>‹h_val›"

lemmas h_val_clift = lift_t_lift [where g = c_guard, unfolded CTypesDefs.lift_def, simplified]
lemma h_val_clift':
  "clift hp p = Some v ⟹ h_val (hrs_mem hp) p = v"
  unfolding hrs_mem_def by (cases hp, simp add: h_val_clift)

subsection "\<^const>‹h_t_valid›"

lemma clift_Some_eq_valid:
  "(∃v. clift hp p = Some v) = (hrs_htd hp ⊨⇩t p)"
  apply (cases hp)
  apply (simp add: lift_t_if hrs_htd_def)
  done

lemma h_t_valid_clift_Some_iff:
  "(hrs_htd hp ⊨⇩t p) = (∃v. clift hp p = Some v)"
  apply (cases hp)
  apply (simp add: lift_t_if hrs_htd_def)
  done

lemma h_t_valid_clift:
  "clift hp p = Some v ⟹ hrs_htd hp ⊨⇩t p"
  apply (cases hp, simp add: hrs_htd_def)
  apply (erule lift_t_h_t_valid)
  done

lemma c_guard_h_t_valid:
  "hrs_htd hp ⊨⇩t p ⟹ c_guard p"
  by (simp add: h_t_valid_def)

section "\<^const>‹field_lvalue›"
(* field_lvalue is the name of &(p→f) *)

subsection "\<^const>‹heap_update›"

lemma heap_update_field:
  "⟦field_ti TYPE('a :: packed_type) f = Some t; c_guard p;
  export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))⟧
  ⟹ heap_update (Ptr &(p→f) :: 'b ptr) v hp =
  heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp"
  apply (erule field_ti_field_lookupE)
  apply (erule (2) packed_heap_super_field_update [unfolded typ_uinfo_t_def])
  done

lemma heap_update_field':
  "⟦field_ti TYPE('a :: packed_type) f = Some t; c_guard p;
  export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))⟧
  ⟹ heap_update (Ptr &(p→f) :: 'b ptr) v hp =
  heap_update p (update_ti_t t (to_bytes_p v) (h_val hp p)) hp"
  apply (erule field_ti_field_lookupE)
  apply (subst packed_heap_super_field_update [unfolded typ_uinfo_t_def])
     apply assumption+
  apply (drule export_size_of [simplified typ_uinfo_t_def])
  apply (simp add: update_ti_t_def)
  done

lemma heap_update_field_hrs:
  fixes p :: "'a :: packed_type ptr" and v :: "'b :: packed_type"
  shows "⟦field_ti TYPE('a) f = Some t; c_guard p;
    export_uinfo t = export_uinfo (typ_info_t TYPE('b))⟧
  ⟹ hrs_mem_update (heap_update (Ptr &(p→f)) v) hp =
    hrs_mem_update (heap_update p (update_ti_t t (to_bytes_p v) (h_val (hrs_mem hp) p))) hp"
  unfolding hrs_mem_update_def
  apply (simp add: split_def)
  apply (subst heap_update_field)
     apply assumption
    apply assumption
   apply assumption
  apply (frule export_size_of [unfolded typ_uinfo_t_def])
  apply (simp add: update_ti_t_def hrs_mem_def)
  done

lemma heap_update_field_ext:
  "⟦field_ti TYPE('a :: packed_type) f = Some t; c_guard p;
  export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))⟧
  ⟹ heap_update (Ptr &(p→f) :: 'b ptr) =
  (λv hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp)"
  apply (rule ext, rule ext)
  apply (erule (2) heap_update_field)
  done

subsection "\<^const>‹c_guard›"

lemma c_guard_field:
  "⟦c_guard (p :: 'a :: mem_type ptr); field_ti TYPE('a :: mem_type) f = Some t;
  export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type))⟧
  ⟹ c_guard (Ptr &(p→f) :: 'b :: mem_type ptr)"
  apply (erule field_ti_field_lookupE)
  apply (erule (1) c_guard_field_lvalue)
   apply (simp add: typ_uinfo_t_def)
   done

subsection "clift"

lemma clift_field:
  fixes v :: "'a :: mem_type" and p :: "'a :: mem_type ptr"
  assumes lf: "clift hp p = Some v"
  and     fl: "field_ti TYPE('a) f = Some t"
  and     eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b  :: mem_type))"
  shows   "clift hp (Ptr &(p→f) :: 'b :: mem_type ptr) = Some (from_bytes (access_ti⇩0 t v))"
  using lf fl eu
  apply (clarsimp elim!: field_ti_field_lookupE)
  apply (erule (2) lift_t_mono [unfolded typ_uinfo_t_def])
  apply (rule c_guard_mono)
  done

subsubsection "Updates"

lemma clift_field_update:
  fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
  assumes   fl: "field_ti TYPE('a) f = Some t"
  and       eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b))"
  and       cl: "clift hp ptr = Some z"
  shows "(clift (hrs_mem_update (heap_update (Ptr &(ptr→f)) val) hp)) =
  (clift hp)(ptr ↦ field_update (field_desc t) (to_bytes_p val) z)"
  (is "?LHS = ?RHS")
proof -
  have cl': "clift (fst hp, snd hp) ptr = Some z" using cl by simp

  have "?LHS = super_field_update_t (Ptr &(ptr→f)) val (clift (fst hp, snd hp))"
    unfolding hrs_mem_update_def split_def
  proof (rule lift_t_super_field_update [OF h_t_valid_sub, unfolded typ_uinfo_t_def])
    from cl' show "snd hp ⊨⇩t ptr" by (rule lift_t_h_t_valid)
    show "TYPE('b) ≤⇩τ TYPE('a)" using fl eu by (rule field_ti_sub_typ [unfolded typ_uinfo_t_def])
  qed fact+

  also have "… = ?RHS" using fl eu cl
    apply -
    apply (erule field_ti_field_lookupE)
    apply (subst super_field_update_lookup [unfolded typ_uinfo_t_def])
    apply assumption
    apply simp
    apply simp
    apply simp
    done

  finally show ?thesis .
qed

lemma clift_field_update_padding:
  fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
  assumes   fl: "field_ti TYPE('a) f = Some t"
  and       eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b))"
  and       cl: "clift hp ptr = Some z"
  and      lbs: "length bs = size_of TYPE('b)"
  shows "(clift (hrs_mem_update (heap_update_padding (Ptr &(ptr→f)) val bs) hp)) =
  (clift hp)(ptr ↦ field_update (field_desc t) (to_bytes_p val) z)"
  (is "?LHS = ?RHS")
proof -
  have cl': "clift (fst hp, snd hp) ptr = Some z" using cl by simp

  have "?LHS = super_field_update_t (Ptr &(ptr→f)) val (clift (fst hp, snd hp))"
    unfolding hrs_mem_update_def split_def
  proof (rule lift_t_super_field_update_padding [OF h_t_valid_sub _ lbs, unfolded typ_uinfo_t_def])
    from cl' show "snd hp ⊨⇩t ptr" by (rule lift_t_h_t_valid)
    show "TYPE('b) ≤⇩τ TYPE('a)" using fl eu by (rule field_ti_sub_typ [unfolded typ_uinfo_t_def])
  qed fact+

  also have "… = ?RHS" using fl eu cl
    apply -
    apply (erule field_ti_field_lookupE)
    apply (subst super_field_update_lookup [unfolded typ_uinfo_t_def])
    apply assumption
    apply simp
    apply simp
    apply simp
    done

  finally show ?thesis .
qed

subsection "cparent"
(* cparent gives the address of the outerlying structure.  It is equivalent to the c expression
   ptr - offset_of field
*)

definition
  cparent :: "('a :: c_type) ptr ⇒ string list ⇒ ('b :: c_type) ptr"
  where
  "cparent p fs ≡ THE p'. p = Ptr &(p'→fs)"

lemma cparent_field [simp]:
  "cparent (Ptr &(p→fs)) fs = p"
  unfolding cparent_def
  by (simp add: field_lvalue_def)

lemma cparent_def2:
  fixes p :: "'b :: c_type ptr"
  shows "cparent p f ≡ (Ptr (ptr_val p - of_nat (field_offset TYPE('a :: c_type) f)) :: 'a :: c_type ptr)"
  (is "cparent p f ≡ ?p'")
proof -
  have pv: "p = Ptr &(?p'→f)"
    by (simp add: field_lvalue_def field_simps)
  show "cparent p f ≡ ?p'"
    by (subst pv) simp
qed

lemma field_cparent [simp]:
  fixes p :: "'a :: c_type ptr"
  shows "(Ptr &(cparent p f :: 'b :: c_type ptr →f)) = p"
  by (simp add: cparent_def2 field_lvalue_def)

(* If we know the value at the parent, we can derive the value at the field *)
lemma clift_cparentE:
  fixes v :: "'a :: mem_type" and p :: "'b :: mem_type ptr"
  assumes lf: "clift hp (cparent p fs :: 'a ptr) = Some v"
  and     fl: "field_ti TYPE('a) fs = Some t"
  and     eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b))"
  shows   "clift hp p = Some (from_bytes (access_ti⇩0 t v))"
  unfolding cparent_def
proof -
  have pv: "p = Ptr &((Ptr (ptr_val p - of_nat (field_offset TYPE('a) fs)) :: 'a ptr)→fs)"
    (is "p = Ptr &(?p'→fs)") by (simp add: field_lvalue_def field_simps)
  have cp: "cparent p fs = ?p'"
    by (subst pv) simp

  from lf have lf': "clift hp ?p' = Some v"
    by (simp add: cparent_def2)

  have "clift hp (Ptr &(?p'→fs) :: 'b ptr) = Some (from_bytes (access_ti⇩0 t v))" using lf' fl eu
    by (rule clift_field)

  thus ?thesis
    by (simp add: pv [symmetric])
qed

lemma heap_update_to_cparent:
  fixes p :: "'b :: packed_type ptr" and fs :: "char list list"
  defines "cp ≡ cparent p fs :: 'a :: packed_type ptr"
  assumes fl: "field_ti TYPE('a :: packed_type) fs = Some t"
  and     cg: "c_guard cp"
  and     eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b))"
  shows   "heap_update p v hp = heap_update cp (update_ti t (to_bytes_p v) (h_val hp cp)) hp"
  (is "?LHS = ?RHS")
proof -
  have "?LHS = heap_update (Ptr &(cp→fs)) v hp"
    unfolding cp_def by simp

  moreover have "… = ?RHS" using fl cg eu
    by (fastforce intro: heap_update_field)

  finally show ?thesis .
qed

lemma c_guard_cparent:
 "⟦ c_guard ((cparent p f)::'a::mem_type ptr);
    field_ti TYPE('a) f = Some t;
    export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
  c_guard (p::'b::mem_type ptr)"
 apply(subst field_cparent[symmetric, where f=f])
 apply(rule c_guard_field, (simp add:typ_uinfo_t_def)+)
done

lemma parent_update_child:
 fixes p::"'b::packed_type ptr"
 shows
 "⟦ c_guard ((cparent p f)::'a::packed_type ptr); field_ti TYPE('a) f = Some t;
   export_uinfo t = export_uinfo (typ_info_t TYPE('b))⟧
⟹ hrs_mem_update (heap_update p v) hp =
   hrs_mem_update
    (heap_update ((cparent p f)::'a ptr)
      (update_ti_t t (to_bytes_p v) (h_val (hrs_mem hp) (cparent p f))))
    hp"
 apply(subst field_cparent[symmetric, where f=f and 'b='a])
 apply(rule heap_update_field_hrs, simp+)
done

subsection "\<^const>‹h_val›"
(* h_val looks up the heap to construct a value of the desired type (Used to be CTypeDefs.lift) *)

lemma h_val_field_clift:
  fixes pa :: "'a :: mem_type ptr"
  assumes cl: "clift (h, d) pa = Some v"
  and     fl: "field_ti TYPE('a) f = Some t"
  and     eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type))"
  shows   "h_val h (Ptr &(pa→f) :: 'b :: mem_type ptr) = from_bytes (access_ti⇩0 t v)"
  using cl fl eu
  apply -
  apply (rule h_val_clift)
  apply (clarsimp simp: field_ti_def split: option.splits)
  apply (erule (2) lift_t_mono [unfolded typ_uinfo_t_def])
  apply (rule c_guard_mono)
  done

lemma h_val_field_clift':
  fixes pa :: "'a :: mem_type ptr"
  assumes cl: "clift hp pa = Some v"
  and     fl: "field_ti TYPE('a) f = Some t"
  and     eu: "export_uinfo t = typ_uinfo_t TYPE('b :: mem_type)"
  shows   "h_val (hrs_mem hp) (Ptr &(pa→f) :: 'b :: mem_type ptr) = from_bytes (access_ti⇩0 t v)"
  using cl fl eu
  apply (cases hp)
  apply (simp add: h_val_field_clift hrs_mem_def typ_uinfo_t_def)
  done

lemma clift_subtype:
  "⟦ clift hp ((cparent p f)::'a::mem_type ptr) = Some v;
     field_ti TYPE('a) f = Some t;
     export_uinfo t = export_uinfo (typ_info_t TYPE('b::mem_type)) ⟧ ⟹
   clift hp (p::'b ptr) = Some (from_bytes (access_ti⇩0 t v))"
 apply(subst field_cparent[symmetric, where f=f])
 apply(rule clift_field)
   apply(simp)+
done

subsection "\<^const>‹h_t_valid›"

lemma h_t_valid_field:
  fixes p :: "'a :: mem_type ptr"
  assumes htv: "d ⊨⇩t p"
  and     fti: "field_ti TYPE('a :: mem_type) f = Some t"
  and      eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type))"
  shows    "d ⊨⇩t (Ptr &(p→f) :: 'b :: mem_type ptr)"
  using htv fti eu
  apply -
  apply (clarsimp simp: field_ti_def split: option.splits)
  apply (erule (1) h_t_valid_mono [rule_format, unfolded typ_uinfo_t_def])
   apply (rule c_guard_mono)
  apply assumption
  done

lemma h_t_valid_field':
  fixes p::"'a::mem_type ptr"
  shows
  "⟦ field_ti TYPE('a) f = Some t;
     export_uinfo t = typ_uinfo_t TYPE('b);
     d,g ⊨⇩t p; g' ((Ptr &(p→f))::'b::mem_type ptr) ⟧ ⟹ d,g' ⊨⇩t Ptr &(p→f)"
 apply(simp add:h_t_valid_guard_subst[OF h_t_valid_sub])
done

lemma h_t_valid_c_guard_field:
  fixes p::"'a::mem_type ptr"
  shows
  "⟦ d ⊨⇩t p;
     field_ti TYPE('a) f = Some t;
     export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
   d ⊨⇩t ((Ptr &(p→f))::'b::mem_type ptr)"
 apply(simp add:h_t_valid_field c_guard_field h_t_valid_c_guard typ_uinfo_t_def)
done

lemma h_t_valid_cparent:
 "⟦ field_ti TYPE('a) f = Some t;
    export_uinfo t = typ_uinfo_t TYPE('b);
    d,g ⊨⇩t ((cparent p f)::'a::mem_type ptr); g' (p::'b::mem_type ptr) ⟧ ⟹
  d,g' ⊨⇩t p"
 apply(subst field_cparent[symmetric, where f=f])
 apply(rule h_t_valid_field')
    apply(assumption)
   apply(simp add:typ_uinfo_t_def)
  apply(assumption)
 apply(simp)
done

lemma h_t_valid_c_guard_cparent:
 fixes p::"'b::mem_type ptr"
 shows
 "⟦ d ⊨⇩t ((cparent p f)::'a::mem_type ptr);
    field_ti TYPE('a) f = Some t;
    export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
  d ⊨⇩t p"
 apply(rule h_t_valid_cparent)
    apply(assumption)
   apply(simp add:typ_uinfo_t_def)
  apply(assumption)
 apply(rule c_guard_cparent)
   apply(rule h_t_valid_c_guard, assumption)
  apply(assumption)
 apply(simp add:typ_uinfo_t_def)
done

lemma c_guard_array_c_guard:
  "c_guard (ptr_coerce p :: ('b :: c_type, 'a :: finite) array ptr) ⟹ c_guard (p :: 'b ptr)"
  apply (clarsimp simp: c_guard_def)
  apply (rule conjI)
   apply (clarsimp simp: ptr_aligned_def align_of_def align_td_array)
  apply (simp add: c_null_guard_def)
  apply (erule contra_subsetD [rotated])
  apply (rule intvl_start_le)
  apply simp
  done

lemma c_guard_array_field:
  assumes parent_cguard: "c_guard (p :: 'a :: mem_type ptr)"
  and subfield: "field_ti TYPE('a :: mem_type) f = Some t"
  and type_match: "export_uinfo t = export_uinfo (typ_info_t TYPE(('b :: array_outer_max_size, 'c :: array_max_count) array))"
  shows "c_guard (Ptr &(p→f) :: 'b ptr)"
  by (metis c_guard_array_c_guard c_guard_field parent_cguard ptr_coerce.simps subfield type_match)

instantiation ptr :: (type) enum
begin

  definition "enum_ptr ≡ map Ptr enum_class.enum"
  definition "enum_all_ptr P ≡ enum_class.enum_all (λv. P (Ptr v))"
  definition "enum_ex_ptr P ≡ enum_class.enum_ex (λv. P (Ptr v))"

  instance
    apply (intro_classes)
       apply (clarsimp simp: enum_ptr_def)
       apply (metis ptr.exhaust surj_def)
      apply (clarsimp simp: enum_ptr_def distinct_map)
      apply (metis injI ptr.inject)
     apply (clarsimp simp: enum_all_ptr_def)
     apply (rule iffI)
      apply (rule allI)
      apply (rename_tac x)
      apply (erule_tac x="ptr_val x" in allE)
      apply force
     apply force
    apply (clarsimp simp: enum_ex_ptr_def)
    apply (rule iffI)
     apply force
    apply clarsimp
    subgoal for P x
      apply (rule exI[where x="ptr_val x"])
      apply clarsimp
      done
    done
end

subsection ‹Type Combinators and Padding›



lemma ti_typ_pad_combine_empty_ti:
  fixes tp :: "'b :: c_type itself"
  shows "ti_typ_pad_combine tp lu upd algn fld (empty_typ_info algn' n) =
  TypDesc (max algn' (max algn (align_td (typ_info_t TYPE('b))))) 
     (TypAggregate [DTuple (adjust_ti (typ_info_t TYPE('b)) lu upd) fld 
            ⦇field_access = xto_bytes ∘ lu,
            field_update = upd ∘ xfrom_bytes,
            field_sz = size_of TYPE('b)⦈]) n"
  by (simp add: ti_typ_pad_combine_def ti_typ_combine_def empty_typ_info_def Let_def)

lemma ti_typ_combine_empty_ti:
  fixes tp :: "'b :: c_type itself"
  shows "ti_typ_combine tp lu upd algn fld (empty_typ_info algn' n) =
  TypDesc (max algn' (max algn (align_td (typ_info_t TYPE('b))))) 
     (TypAggregate [DTuple (adjust_ti (typ_info_t TYPE('b)) lu upd) fld  
            ⦇field_access = xto_bytes ∘ lu,
            field_update = upd ∘ xfrom_bytes,
            field_sz = size_of TYPE('b)⦈]) n"
  by (simp add: ti_typ_combine_def empty_typ_info_def Let_def)

lemma ti_typ_pad_combine_td:
  fixes tp :: "'b :: c_type itself"
  shows "padup  (max (2 ^ algn) (align_of TYPE('b))) (size_td_struct st) = 0 ⟹
  ti_typ_pad_combine tp lu upd algn fld (TypDesc algn' st n) =
  TypDesc (max algn' (max algn (align_td (typ_info_t TYPE('b))))) 
     (extend_ti_struct st (adjust_ti (typ_info_t TYPE('b)) lu upd) fld  
            ⦇field_access = xto_bytes ∘ lu,
            field_update = upd ∘ xfrom_bytes,
            field_sz = size_of TYPE('b)⦈) n"
  by (simp add: ti_typ_pad_combine_def ti_typ_combine_def Let_def)

lemma ti_typ_combine_td:
  fixes tp :: "'b :: c_type itself"
  shows "padup (align_of TYPE('b)) (size_td_struct st) = 0 ⟹
  ti_typ_combine tp lu upd algn fld (TypDesc algn' st n) =
  TypDesc (max algn' (max algn (align_td (typ_info_t TYPE('b))))) 
     (extend_ti_struct st (adjust_ti (typ_info_t TYPE('b)) lu upd) fld  
            ⦇field_access = xto_bytes ∘ lu,
            field_update = upd ∘ xfrom_bytes,
            field_sz = size_of TYPE('b)⦈) n"
  by (simp add: ti_typ_combine_def Let_def)

lemma update_ti_t_pad_combine:
  assumes std: "size_td td' mod 2 ^ (max algn (align_td (typ_info_t TYPE('a :: c_type)))) = 0"
  shows "update_ti_t (ti_typ_pad_combine TYPE('a :: c_type) lu upd algn fld td') bs v =
  update_ti_t (ti_typ_combine TYPE('a :: c_type) lu upd algn fld td') bs v"
  using std
  by (simp add: ti_typ_pad_combine_def size_td_simps Let_def max_2_exp)

subsection ‹
  The orphanage: miscellaneous lemmas pulled up to (roughly) where they belong.
›

lemma uinfo_array_tag_n_m_not_le_typ_name:
  "typ_name (typ_info_t TYPE('b)) @ ''_array_'' @ nat_to_bin_string m
      ∉ td_names (typ_info_t TYPE('a))
    ⟹ ¬ uinfo_array_tag_n_m TYPE('b :: c_type) n m ≤ typ_uinfo_t TYPE('a :: c_type)"
  apply (clarsimp simp: typ_tag_le_def typ_uinfo_t_def)
  apply (drule td_set_td_names)
   apply (clarsimp simp: uinfo_array_tag_n_m_def typ_uinfo_t_def)
   apply (drule arg_cong[where f="λxs. set ''r'' ⊆ set xs"], simp)
  apply (simp add: uinfo_array_tag_n_m_def typ_uinfo_t_def)
  done

lemma tag_not_le_via_td_name:
  "typ_name (typ_info_t TYPE('a)) ∉ td_names (typ_info_t TYPE('b))
    ⟹ typ_name (typ_info_t TYPE('a)) ≠ pad_typ_name
    ⟹ ¬ typ_uinfo_t TYPE('a :: c_type) ≤ typ_uinfo_t TYPE ('b :: c_type)"
  apply (clarsimp simp: typ_tag_le_def typ_uinfo_t_def)
  apply (drule td_set_td_names, simp+)
  done

(* Simplifier setup *)

(* Basic idea:
    - Try to stay at highest level, i.e., c_guard, then ptr_valid, then clift
    - remove all field references.
    - try the less costly clift_update

*)

lemmas typ_heap_simps =
  ― ‹\<^const>‹c_guard››
  c_guard_field
  c_guard_h_t_valid
  ― ‹\<^const>‹h_t_valid››
  h_t_valid_field
  h_t_valid_clift
  ― ‹\<^const>‹h_val››
  h_val_field_clift'
  h_val_clift'
  ― ‹\<^const>‹clift››
  clift_field
  clift_field_update
  heap_update_field_hrs
  heap_update_field'
  clift_heap_update
  clift_heap_update_same_td_name ― ‹Try this last (is expensive)›

end