Theory AutoCorres2.SepCode

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

(* License: BSD, terms see file ./LICENSE *)

theory SepCode
imports
  Separation_UMM
  "Simpl.Vcg"
begin

definition
  singleton_t :: "'a::c_type ptr ⇒ 'a ⇒ heap_state"
where
  "singleton_t p v ≡ lift_state (heap_update p v (λx. 0), (ptr_retyp p empty_htd))"

definition
  tagd :: "'a ptr_guard ⇒ 'a::c_type ptr ⇒ heap_assert" (infix ‹⊢s› 100)
where
  "g ⊢s p ≡ λs. s,g ⊨s p ∧ dom s = s_footprint p"

definition
  field_footprint :: "'a::c_type ptr ⇒ qualified_field_name ⇒ (addr × s_heap_index) set"
where
  "field_footprint p f ≡
     s_footprint_untyped (ptr_val p + of_nat (field_offset TYPE('a) f))
                         (export_uinfo (field_typ TYPE('a) f))"

definition
  fs_footprint :: "'a::c_type ptr ⇒ qualified_field_name set ⇒ (addr × s_heap_index) set"
where
  "fs_footprint p F ≡ ⋃{field_footprint p f | f. f ∈ F}"

definition fields :: "'a::c_type itself ⇒ qualified_field_name set" where
  "fields t ≡ {f. field_lookup (typ_info_t TYPE('a)) f 0 ≠ None}"

definition
  mfs_sep_map :: "'a::c_type ptr ⇒ 'a ptr_guard ⇒ qualified_field_name set ⇒ 'a ⇒ heap_assert"
    (‹(‹open_block notation=‹mixfix mfs_sep_map››_ ↦⇘_⇙⇗_⇖ _)› [56,0,0,51] 56)
where
  "p ↦⇘g⇙⇗F⇖ v ≡ λs. lift_typ_heap g (singleton_t p v ++ s) p = Some v ∧
      F ⊆ fields TYPE('a) ∧
      dom s = s_footprint p - fs_footprint p F ∧ wf_heap_val s"

notation (input)
  mfs_sep_map (‹(‹open_block notation=‹mixfix mfs_sep_map››_ ↦⇩_⇧_ _)› [56,0,1000,51] 56)

definition
  disjoint_fn :: "qualified_field_name ⇒ qualified_field_name set ⇒ bool"
where
  "disjoint_fn f F ≡ ∀f'∈F. ¬ f ≤ f' ∧ ¬ f' ≤ f"

definition
  sep_cut' :: "addr ⇒ nat ⇒ (s_addr,'b) map_assert"
where
  "sep_cut' p n ≡ λs. dom s = {(x,y). x ∈ {p..+n}}"

definition
  sep_cut :: "addr ⇒ addr_bitsize word ⇒ (s_addr,'b) map_assert"
where
  "sep_cut x y ≡ sep_cut' x (unat y)"

text ‹----›

(* fixme MOVE *)
lemma heap_list_h_eq:
  "⟦ x ∈ {p..+q}; q < addr_card; heap_list h q p = heap_list h' q p ⟧ ⟹ h x = h' x"
proof (induct q arbitrary: p)
  case 0 thus ?case by simp
next
  case (Suc n) thus ?case by (force dest: intvl_neq_start)
qed

lemma s_footprint_intvl:
  "(a, SIndexVal) ∈ s_footprint p = (a ∈ {ptr_val (p::'a::c_type ptr)..+size_of TYPE('a)})"
  apply(clarsimp simp: s_footprint_def s_footprint_untyped_def)
  apply(rule iffI, clarsimp)
   apply(rule intvlI)
   apply(simp add: size_of_def)
  apply(drule intvlD, clarsimp)
  apply(simp add: size_of_def)
  apply fast
  done

lemma singleton_t_dom [simp]:
  "dom (singleton_t p (v::'a::mem_type)) = s_footprint p"
  supply unsigned_of_nat [simp del]
  apply(rule equalityI; clarsimp simp: singleton_t_def lift_state_def s_footprint_intvl
                                 split: s_heap_index.splits if_split_asm option.splits)
    apply(rule ccontr)
    apply(simp add: ptr_retyp_None)
  subgoal for a b y x2 x2a
   apply(cases "a ∈ {ptr_val p..+size_of TYPE('a)}")
    apply(simp add: ptr_retyp_footprint list_map_eq split: if_split_asm)
    apply(drule intvlD, clarsimp)
    apply(rule s_footprintI)
     apply(subst (asm) word_unat.eq_norm)
     apply(subst (asm) mod_less)
      apply(subst len_of_addr_card)
      apply(erule less_trans)
      apply(rule max_size)
     apply(simp add: map_le_def)
    apply assumption
    apply(simp add: ptr_retyp_None)
    done
  apply(rule conjI; clarsimp)
   apply (simp add: ptr_retyp_d_empty s_footprintD)
  apply(frule s_footprintD2)
  apply(frule s_footprintD)
  apply(simp add: ptr_retyp_footprint)
  done

lemma heap_update_merge:
  assumes val: "d,g ⊨t p"
  shows "lift_state ((heap_update p (v::'a::mem_type) h),d)
            = lift_state (h,d) ++ singleton p v h d" (is "?x = ?y")
proof (rule ext, cases)
  fix x
  assume c: "x ∈ dom (singleton p v h d)"
  with val
  have "lift_state (heap_update_list (ptr_val p)
                                     (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p))) h,
                    d) x =
        singleton p v h d x"
    by (auto simp: heap_list_update_to_bytes singleton_def lift_state_def heap_update_def
                   singleton_dom
             split: option.splits s_heap_index.splits)
  with c show "?x x = ?y x" by (force simp: heap_update_def dest: domD)
next
  fix x
  assume nc: "x ∉ dom (singleton p v h d)"
  with val show "?x x = ?y x"
    apply(cases x)
    apply(clarsimp simp: lift_state_def heap_update_def map_add_def
                   split: option.splits s_heap_index.splits)
    apply(safe; clarsimp)
    by (metis heap_list_length heap_update_nmem_same len nc s_footprint_intvl singleton_dom)
qed

lemma tagd_dom_exc:
  "(g ⊢s p) s ⟹ dom s = s_footprint p"
  by (clarsimp simp: tagd_def)

lemma tagd_dom_p_exc:
  "(g ⊢s p) s ⟹ (ptr_val (p::'a::mem_type ptr),SIndexVal) ∈ dom s"
  by (drule tagd_dom_exc) clarsimp

lemma tagd_g_exc:
  "(g ⊢s p ∧* P) s ⟹ g p"
  by (drule sep_conjD, force simp: tagd_def elim: s_valid_g)

lemma sep_map_tagd_exc:
  "(p ↦⇩g (v::'a::mem_type)) s ⟹ (g ⊢s p) s"
  by (clarsimp simp: sep_map_def tagd_def lift_typ_heap_s_valid)

lemma sep_map_any_tagd_exc:
  "(p ↦⇩g -) s ⟹ (g ⊢s (p::'a::mem_type ptr)) s"
  by (clarsimp dest!: sep_map_anyD_exc, erule sep_map_tagd_exc)

lemma ptr_retyp_tagd_exc:
  "g (p::'a::mem_type ptr) ⟹
      (g ⊢s p) (lift_state (h, ptr_retyp p empty_htd))"
  supply unsigned_of_nat [simp del]
  apply(simp add: tagd_def ptr_retyp_s_valid lift_state_dom)
  apply(rule equalityI;
      clarsimp simp: lift_state_def split: s_heap_index.splits if_split_asm option.splits)
  subgoal for a
    apply(cases "a ∈ {ptr_val p..+size_of TYPE('a)}")
     apply(drule intvlD, clarsimp)
     apply(rule s_footprintI2, simp)
    apply(subst (asm) ptr_retyp_None; simp)
    done
  subgoal for a b y x2 x2a
    apply(cases "a ∈ {ptr_val p..+size_of TYPE('a)}")
     apply(subst (asm) ptr_retyp_footprint)
      apply simp
     apply(drule intvlD, clarsimp)
     apply(subst (asm )word_unat.eq_norm)
     apply(subst (asm) mod_less)
      apply(subst len_of_addr_card)
      apply(erule less_trans)
      apply simp
     apply(subst (asm) list_map_eq)
     apply(clarsimp split: if_split_asm)
     apply(erule (1) s_footprintI)
    apply(simp add: ptr_retyp_None)
    done
  subgoal for a b
    apply(rule conjI; clarsimp)
     apply(cases "a ∈ {ptr_val p..+size_of TYPE('a)}")
      apply(simp add: ptr_retyp_footprint)
     apply(drule s_footprintD)
     apply simp
    apply(cases "a ∈ {ptr_val p..+size_of TYPE('a)}")
     apply(subst (asm) ptr_retyp_footprint)
      apply simp
     apply(drule intvlD, clarsimp)
     apply(subst (asm )word_unat.eq_norm)
     apply(subst (asm) mod_less)
      apply(subst len_of_addr_card)
      apply(erule less_trans)
      apply simp
     apply(subst (asm) list_map_eq)
     apply(clarsimp split: if_split_asm)
     apply(drule s_footprintD2)
     apply simp
     apply(subst (asm) unat_of_nat)
     apply(subst (asm) mod_less)
      apply(subst len_of_addr_card)
      apply(erule less_trans, simp)
     apply simp
    apply(fastforce dest: s_footprintD)
    done
  done

lemma singleton_dom_proj_d [simp]:
  "(g ⊢s p) s ⟹ dom (singleton p (v::'a::mem_type) h (proj_d s)) = dom s"
  by (clarsimp simp: tagd_def singleton_dom s_valid_def)

lemma singleton_d_restrict_eq:
  "restrict_s d (s_footprint p) = restrict_s d' (s_footprint p)
      ⟹ singleton p v h d = singleton p (v::'a::mem_type) h d'"
  apply(clarsimp simp: singleton_def)
  apply(rule ext)
  subgoal for x
    apply(cases "x ∈ s_footprint p"; simp)
    apply(cases x, clarsimp)
    subgoal for a b
      apply(drule fun_cong [where x=a])
      apply(clarsimp simp: s_footprint_restrict lift_state_def
          split: s_heap_index.splits if_split_asm option.splits)
      apply(rule conjI, clarsimp simp: restrict_s_def)
      apply(clarsimp simp: restrict_s_def)
      subgoal for x'
        apply(drule fun_cong [where x="x'"])
        apply auto
        done
      done
    done
  done

lemma sep_heap_update'_exc:
  assumes sep: "(g ⊢s p ∧* (p ↦⇩g v ⟶* P)) (lift_state (h,d))"
  shows "P (lift_state (heap_update p (v::'a::mem_type) h,d))"
proof -
  from sep obtain s0 s1 where disj: "s0 ⊥ s1" and
    merge: "lift_state (h,d) = s1 ++ s0" and
    l: "(g ⊢s p) s0" and r: "(p ↦⇩g v ⟶* P) s1" by (force dest: sep_conjD)
  moreover from this have "s1 ⊥ singleton p v h (proj_d s0)"
    by (fastforce simp: map_disj_def)
  moreover from l have "g p" by (force simp: tagd_def elim: s_valid_g)
  moreover from merge l have "lift_state (h,d),g ⊨s p"
    by (force simp: tagd_def intro: s_valid_heap_merge_right)
  hence "d,g ⊨t p" by (simp add: h_t_s_valid)
  moreover from l have "s0 ++ singleton p v h (proj_d s0) = singleton p v h (proj_d s0)"
    by (force simp: map_add_dom_eq singleton_dom dest: tagd_dom_exc)
  moreover from l merge have "s1 ++ singleton p v h (proj_d s0) = s1 ++ s0 ++ singleton p v h d"
    apply(clarsimp simp: tagd_def)
    apply(rule ext)
    subgoal for  x
      apply(cases x, clarsimp simp: restrict_map_def)
      subgoal for a b
        apply(simp add: s_valid_def)
        apply(drule singleton_dom [where v=v and h=h])
        apply(drule fun_cong [where x="(a,b)"])
        apply(cases "(a,b) ∈ s_footprint p")
        subgoal premises prems
        proof -
          have "(s1 ++ singleton p v h (proj_d s0)) (a, b) = singleton p v h d (a, b)"
            using prems 
            by(force simp: lift_state_def map_add_def singleton_def proj_d_def
                split: option.splits s_heap_index.splits if_split_asm)
          then show ?thesis using prems
            apply(clarsimp simp: map_add_def s_valid_def split: option.splits)
             apply force
            apply (fastforce intro: sym)
            done
        qed
        apply(auto simp: map_add_def singleton_def split: option.splits)
        done
      done
    done
  ultimately show ?thesis
    by (fastforce dest: sep_implD simp: sep_map_singleton tagd_def s_valid_def heap_update_merge)
qed

lemma sep_heap_update_exc:
  "⟦ (p ↦⇩g - ∧* (p ↦⇩g v ⟶* P)) (lift_state (h,d)) ⟧ ⟹
      P (lift_state (heap_update p (v::'a::mem_type) h,d))"
  by (force intro: sep_heap_update'_exc dest: sep_map_anyD_exc sep_map_tagd_exc
            elim: sep_conj_impl)

lemma sep_heap_update_global'_exc:
  "(g ⊢s p ∧* R) (lift_state (h,d)) ⟹
      ((p ↦⇩g v) ∧* R) (lift_state (heap_update p (v::'a::mem_type) h,d))"
  by (rule sep_heap_update'_exc, erule sep_conj_sep_conj_sep_impl_sep_conj)

lemma sep_heap_update_global_exc:
  "(p ↦⇩g - ∧* R) (lift_state (h,d)) ⟹
      ((p ↦⇩g v) ∧* R) (lift_state (heap_update p (v::'a::mem_type) h,d))"
  by (fast intro: sep_heap_update_global'_exc sep_conj_impl sep_map_any_tagd_exc)

lemma sep_heap_update_global_exc2:
  "(p ↦⇩g u ∧* R) (lift_state (h,d)) ⟹
      ((p ↦⇩g v) ∧* R) (lift_state (heap_update p (v::'a::mem_type) h,d))"
  by (fastforce intro: sep_heap_update_global_exc simp: sep_map_any_def sep_conj_exists)

lemma heap_update_mem_same_point:
  "⟦ q ∈ {p..+length v}; length v < addr_card ⟧ ⟹
      heap_update_list p v h q = v ! unat (q - p)"
  apply(induct v arbitrary: p h; clarsimp)
  subgoal for x1 v p h
  apply(cases "p=q")
   apply (simp add: heap_update_list_same [where k=1, simplified])
  apply(drule meta_spec [where x="p+1"])
  apply(drule meta_spec, drule meta_mp)
     apply(fastforce dest: intvl_neq_start)
    by (smt (verit, ccfv_SIG) Suc_lessD add_diff_cancel_left' diff_add_cancel diff_diff_eq 
        diff_zero heap_update_mem_same intvl_neq_start nth_Cons' plus_1_eq_Suc unat_eq_zero 
        unat_minus_one)
  done

lemma heap_update_list_value:
  "length v < addr_card ⟹
   heap_update_list p v h q = (if q ∈ {p..+length v} then v!unat (q-p) else h q)"
  by (auto simp: heap_update_nmem_same heap_update_mem_same_point
           split: if_split)

lemma heap_update_list_value':
  "length xs < addr_card ⟹
   heap_update_list ptr xs hp x = (if unat (x - ptr) < length xs then xs ! unat (x - ptr) else hp x)"
  supply unsigned_of_nat [simp del]
  apply (simp only: heap_update_list_value addr_card_def card_word)
  apply (rule if_cong; simp)
  apply (rule iffI)
   apply (drule intvlD, clarsimp simp add: unat_of_nat)
  apply (simp add: intvl_def unat_arith_simps(4) unat_of_nat split: if_split_asm)
   apply (rule exI [where x="unat x - unat ptr"], simp)
  apply (rule exI [where x="unat x + 2^addr_bitsize - unat ptr"])
  using unat_lt2p [of ptr]
  apply (simp add: unat_arith_simps unat_of_nat)
  done

lemma heap_list_h_eq2:
  "(⋀x. x ∈ {p..+n} ⟹ h x = h' x) ⟹ heap_list h n p = heap_list h' n p"
  apply(induct n arbitrary: p; clarsimp)
  apply(rule conjI)
   apply(fastforce intro: intvl_self)
  apply(fastforce intro: intvl_plus_sub_Suc)
  done

lemma map_td_f_eq':
  "(f=g) ⟶ (map_td f h  t = map_td g h t)"
  "(f=g) ⟶ (map_td_struct f h st = map_td_struct g h st)"
  "(f=g) ⟶ (map_td_list f h ts = map_td_list g h ts)"
  "(f=g) ⟶ (map_td_tuple f h x = map_td_tuple g h x)"
  by (induct t and st and ts and x) auto

lemma map_td_f_eq:
  "f=g ⟹ map_td f t = map_td g t"
  by (erule arg_cong)

lemma sep_map'_lift_exc:
  "(p ↪⇩g (v::'a::mem_type)) (lift_state (h,d)) ⟹ lift h p = v"
  by (frule sep_map'_lift_typ_heapD, simp add: lift_t lift_t_lift)

lemma sep_map_lift_wp_exc:
  "∃v. (p ↦⇩g v ∧* (p ↦⇩g v ⟶* P v)) (lift_state (h,d))
      ⟹ P (lift h (p::'a::mem_type ptr)) (lift_state (h,d))"
  apply clarsimp
  apply(subst sep_map'_lift_exc)
   apply(fastforce simp: sep_map'_def elim: sep_conj_impl)
  subgoal for v
    apply(rule sep_conj_impl_same [where P="p ↦⇩g v" and Q="P v"])
    apply(erule (2) sep_conj_impl)
    done
  done

lemma sep_map_lift_exc:
  "((p::'a::mem_type ptr) ↦⇩g -) (lift_state (h,d)) ⟹
      (p ↦⇩g lift h p) (lift_state (h,d))"
 by (clarsimp simp: sep_map_any_def)
    (frule sep_map_sep_map'_exc, drule sep_map'_lift_exc, simp)

lemma sep_map'_lift_rev_exc:
  "⟦ lift h p = (v::'a::mem_type); (p ↪⇩g -) (lift_state (h,d)) ⟧ ⟹
      (p ↪⇩g v) (lift_state (h,d))"
  by (clarsimp simp: sep_map'_any_def)
     (frule sep_map'_lift_exc, simp)

(* fixme: can be made more flexible when generalised separation conjunction
   is added *)
lemma sep_lift_exists_exc:
  fixes p :: "'a::mem_type ptr"
  assumes ex: "((λs. ∃v. (p ↪⇩g  v) s ∧ P v s) ∧* Q) (lift_state (h,d))"
  shows "(P (lift h p) ∧* Q) (lift_state (h,d))"
proof -
  from ex obtain v where "((λs. (p ↪⇩g  v) s ∧ P v s) ∧* Q)
      (lift_state (h,d))"
    by (subst (asm) sep_conj_exists, clarsimp)
  thus ?thesis
    by (force simp: sep_map'_lift_exc sep_conj_ac
        dest: sep_map'_conjE2_exc dest!: sep_conj_conj)
qed

lemma merge_dom:
  "x ∈ dom s ⟹ (t ++ s) x = s x"
  by (force simp: map_add_def)

lemma merge_dom2:
  "x ∉ dom s ⟹ (t ++ s) x = t x"
  by (force simp: map_add_def split: option.splits)

lemma fs_footprint_empty [simp]:
  "fs_footprint p {} = {}"
  by (auto simp: fs_footprint_def)

lemma fs_footprint_un:
  "fs_footprint p (insert f F) = fs_footprint p {f} ∪ fs_footprint p F"
  by (auto simp: fs_footprint_def)

lemma proj_d_restrict_map_le:
  "snd (proj_d (s |` X) x) ⊆m snd (proj_d s x)"
  by(clarsimp simp: map_le_def proj_d_def restrict_map_def
              split: option.splits if_split_asm)

lemma SIndexVal_conj_setcomp_simp [simp]:
  "{x. snd x = SIndexVal ∧ x ∉ s_footprint_untyped p t}
      = {(x,SIndexVal) | x. x ∉ {p..+size_td t}}"
  by (force dest: intvlD intro: intvlI simp: s_footprint_untyped_def)

lemma heap_list_s_restrict_same:
  "{(x,SIndexVal) | x. x ∈ {p..+n}} ⊆ X ⟹ heap_list_s (s |` X) n p = heap_list_s s n p"
  apply(induct n arbitrary: p; clarsimp simp: heap_list_s_def)
  apply(rule conjI)
   apply(fastforce intro: intvl_self simp: proj_h_def restrict_map_def)
  apply(fastforce intro: intvl_plus_sub_Suc)
  done

lemma heap_list_s_restrict_fs_footprint:
  "field_lookup (typ_info_t TYPE('a::c_type)) f 0 = Some (t,n) ⟹
      heap_list_s (s |` fs_footprint p {f}) (size_td t) &(p→f)
          = heap_list_s s (size_td t) &((p::'a ptr)→f)"
  apply(simp add: fs_footprint_def field_footprint_def field_offset_def)
  apply(subst heap_list_s_restrict_same)
   apply(fastforce simp: s_footprint_untyped_def field_size_def field_lvalue_def field_offset_def
                         field_ti_def field_typ_def field_typ_untyped_def dest: intvlD)
  apply simp
  done

lemma heap_list_proj_h_disj:
  "{(x,SIndexVal) | x. x ∈ {p..+n}} ∩ dom s1 = {} ⟹
      heap_list (proj_h (s0 ++ s1)) n p = heap_list (proj_h s0) n p"
  apply(induct n arbitrary: p; clarsimp)
  apply(rule conjI)
   apply(fastforce simp: proj_h_def intro: intvl_self split: option.splits)
  apply(fastforce intro: intvl_plus_sub_Suc)
  done

lemma heap_list_proj_h_sub:
  "{(x,SIndexVal) | x. x ∈ {p..+n}} ⊆ dom s1 ⟹
      heap_list (proj_h (s0 ++ s1)) n p = heap_list (proj_h s1) n p"
  apply(induct n arbitrary: p; clarsimp)
  apply(rule conjI, fastforce simp: proj_h_def intro: intvl_self split: option.splits)
  subgoal premises prems for n p
  proof -
    have  "{p + 1..+n} ⊆ {p..+Suc n}" using prems by (fastforce intro: intvl_plus_sub_Suc)
    then show ?thesis using prems by fast
  qed
  done



lemma heap_list_s_map_add_super_update_bs:
  "⟦ {x. (x,SIndexVal) ∈ dom s1} = {p+of_nat k..+z}; k + z ≤ n; n < addr_card ⟧
      ⟹ heap_list_s (s0 ++ s1) n p =
          super_update_bs (heap_list_s s1 z (p+of_nat k)) (heap_list_s s0 n p) k"
  apply(clarsimp simp: super_update_bs_def heap_list_s_def)
  subgoal premises prems
  proof -
    have  "heap_list (proj_h (s0 ++ s1)) (k + z + (n - (k+z))) p =
                       take k (heap_list (proj_h s0) n p) @
                       heap_list (proj_h s1) z (p + of_nat k) @
                       drop (k + z) (heap_list (proj_h s0) n p)"
      using prems
      apply(subst heap_list_split2)
      apply(subst heap_list_split2)
      apply simp
      apply(rule conjI)
       apply(subst take_heap_list_le, simp)
       apply(subst heap_list_proj_h_disj)
      using init_intvl_disj [of k z p]
        apply fastforce
       apply simp
      apply(rule conjI)
       apply(subst heap_list_proj_h_sub; fast)
      apply(simp add: drop_heap_list_le)
      apply(subst heap_list_proj_h_disj)
      using final_intvl_disj [of k z n p]
       apply fast
      apply simp
      done
    then show ?thesis using prems by simp
  qed
  done

lemma s_footprint_untyped_dom_SIndexVal:
  "dom s = s_footprint_untyped p t ⟹
      {x. (x,SIndexVal) ∈ dom s} = {p..+size_td t}"
  by (auto simp: s_footprint_untyped_def intro: intvlI dest: intvlD)

lemma field_ti_s_sub:
  "field_lookup (export_uinfo (typ_info_t TYPE('b::mem_type))) f 0 = Some (a,b) ⟹
      s_footprint_untyped &(p→f) a ⊆ s_footprint (p::'b ptr)"
  apply(clarsimp simp: field_ti_def s_footprint_def s_footprint_untyped_def split: option.splits)
  apply(simp add: field_lvalue_def field_offset_def typ_uinfo_t_def)
  subgoal for x k
  apply(rule exI [where x="b+x"])
  apply simp
  apply(simp add: field_offset_untyped_def)
  apply(drule td_set_field_lookupD)
  apply(frule td_set_offset_size)
  apply(drule typ_slice_td_set [where k=x])
   apply simp
  apply(auto simp: prefix_def less_eq_list_def)
    done
  done

lemma wf_heap_val_map_add [simp]:
  "⟦ wf_heap_val s0; wf_heap_val s1 ⟧ ⟹ wf_heap_val (s0 ++ s1)"
  unfolding wf_heap_val_def by auto

lemma of_nat_lt_size_of:
  "⟦ (of_nat x::addr) = of_nat y + of_nat z; x < size_of TYPE('a::mem_type);
      y + z < size_of TYPE('a) ⟧ ⟹ x = y+z"
  by (metis (mono_tags) len_of_addr_card less_trans max_size mod_less of_nat_add unat_of_nat)

lemma proj_d_map_add:
  "snd (proj_d s1 p) n = Some k ⟹ snd (proj_d (s0 ++ s1) p) n = Some k"
  by (auto simp: proj_d_def split: option.splits)

lemma proj_d_map_add2:
  "fst (proj_d s1 p) ⟹ fst (proj_d (s0 ++ s1) p)"
  by (auto simp: proj_d_def split: option.splits)

lemma heap_list_s_restrict_disj_same:
  "dom s ∩ (UNIV - X) = {} ⟹ heap_list_s (s |` X) n p = heap_list_s s n p"
  apply(induct n arbitrary: p; clarsimp simp: heap_list_s_def)
  apply(fastforce simp: proj_h_def restrict_map_def split: option.splits)
  done

lemma UNIV_minus_inter:
  "(X - Y) ∩ (X ∩ (X - Y) - Z) = X - (Y ∪ Z)"
  by fast

lemma sep_map_mfs_sep_map_empty:
  "(p ↦⇩g (v::'a::mem_type)) = (p ↦⇩g⇧({}) v)"
  by (auto simp: sep_map_def mfs_sep_map_def map_add_dom_eq)

lemma fd_cons_double_update:
  "⟦ fd_cons t; length bs = length  bs' ⟧ ⟹
      update_ti_t t bs (update_ti_t t bs' v) = update_ti_t t bs v"
  by (simp add: fd_cons_def Let_def fd_cons_double_update_def fd_cons_desc_def)

lemma fd_cons_update_access:
  "⟦ fd_cons t; length bs = size_td t ⟧ ⟹
      update_ti_t t (access_ti t v bs) v = v"
  by (simp add: fd_cons_def Let_def fd_cons_update_access_def fd_cons_desc_def)

lemma fd_cons_length:
  "⟦ fd_cons t; length bs = size_td t ⟧ ⟹
      length (access_ti t v bs) = size_td t"
  by (simp add: fd_cons_def Let_def  fd_cons_desc_def fd_cons_length_def access_ti0_def)

lemma fd_cons_length_p:
  "fd_cons t ⟹ length (access_ti0 t v) = size_td t"
  by (simp add: fd_cons_length access_ti0_def)

lemma fd_cons_update_normalise:
  "⟦ fd_cons t; length bs = size_td t ⟧ ⟹
      update_ti_t t ((norm_desc (field_desc t) (size_td t)) bs) v = update_ti_t t bs v"
  by (fastforce simp: fd_cons_def Let_def fd_cons_desc_def fd_cons_update_normalise_def
                dest: fd_cons_update_normalise)

lemma field_footprint_SIndexVal:
  "field_lookup (typ_info_t TYPE('a::c_type)) f 0 = Some (t, n) ⟹
      {x. (x, SIndexVal) ∈ field_footprint (p::'a ptr) f} =
          {ptr_val p + of_nat n..+size_td t}"
  by (auto simp: field_footprint_def s_footprint_untyped_def field_typ_def field_typ_untyped_def
           intro: intvlI dest: intvlD)

lemma fs_footprint_subset:
  "F ⊆ fields TYPE('a::mem_type) ⟹ fs_footprint (p::'a ptr) F ⊆ s_footprint p"
  unfolding fs_footprint_def field_footprint_def
  apply(clarsimp simp: fields_def)
  apply(drule (1) subsetD, clarsimp)
  apply(frule field_lookup_export_uinfo_Some)
  apply(drule field_ti_s_sub)
  apply(unfold field_lvalue_def)[1]
  apply(subst (asm) field_lookup_offset_eq, assumption)
  apply(fastforce simp: field_typ_def field_typ_untyped_def)
  done

lemma length_heap_list_s [simp]:
  "length (heap_list_s s n p) = n"
  by (clarsimp simp: heap_list_s_def)

lemma heap_list_proj_h_restrict:
  "{p..+n} ⊆ {x. (x,SIndexVal) ∈ X} ⟹ heap_list (proj_h (s |` X)) n p = heap_list (proj_h s) n p"
  apply(induct n arbitrary: p; clarsimp)
  apply(rule conjI)
   apply(fastforce simp: proj_h_restrict intro: intvl_self)
  apply(fastforce intro: intvl_plus_sub_Suc)
  done

lemma heap_list_proj_h_lift_state:
  "{p..+n} ⊆ {x. fst (d x)} ⟹ heap_list (proj_h (lift_state (h,d))) n p = heap_list h n p"
  by (fastforce intro: heap_list_h_eq2 simp: proj_h_lift_state)

lemma heap_list_rpbs:
  "heap_list (λx. 0) n p = replicate n 0"
  by (induct n arbitrary: p) auto

lemma field_access_take_drop:
  fixes
   t::"('a,'b) typ_info" and
   st::"('a,'b) typ_info_struct" and
   ts::"('a,'b) typ_info_tuple list" and
   x::"('a,'b) typ_info_tuple"
  shows
  "∀s m n f. field_lookup t f m = Some (s,n) ⟶ wf_fd t ⟶
      take (size_td s) (drop (n - m) (access_ti0 t v)) =
        access_ti0 s v"
  "∀s m n f. field_lookup_struct st f m = Some (s,n) ⟶ wf_fd_struct st ⟶
      take (size_td s) (drop (n - m) (access_ti_struct st v (replicate (size_td_struct st) 0))) =
        access_ti0 s v"
  "∀s m n f. field_lookup_list ts f m = Some (s,n) ⟶ wf_fd_list ts ⟶
      take (size_td s) (drop (n - m) (access_ti_list ts v (replicate (size_td_list ts) 0))) =
        access_ti0 s v"
  "∀s m n f. field_lookup_tuple x f m = Some (s,n) ⟶ wf_fd_tuple x ⟶
      take (size_td s) (drop (n - m) (access_ti_tuple x v (replicate (size_td_tuple x) 0))) =
        access_ti0 s v"
     apply(induct t and st and ts and x, all ‹clarsimp simp: access_ti0_def›)
    apply(fastforce dest: wf_fd_cons_structD
      simp: fd_cons_struct_def fd_cons_desc_def fd_cons_length_def)
   apply(drule wf_fd_cons_tupleD)
   apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def fd_cons_length_def)
   apply(clarsimp split: option.splits)
    apply(subst drop_all)
     apply(fastforce dest: field_lookup_offset_le simp: fd_cons_length_def split_DTuple_all)
    apply simp
    apply (metis (no_types, opaque_lifting) add.commute add_le_imp_le_diff diff_is_0_eq' 
      diff_zero field_lookup_offset_le(2) fl2 size_td_tuple_dt_fst)
   apply (metis (no_types, lifting) Nat.diff_diff_right add_leD2 append.right_neutral 
      diff_is_0_eq length_0_conv length_take nat_min_simps(1) 
      td_set_offset_size' td_set_tuple_field_lookup_tupleD zero_le)
  apply fastforce
  done

lemma field_access_take_dropD:
  "⟦ field_lookup t f 0 = Some (s,n); wf_lf (lf_set t []); wf_desc t ⟧ ⟹
      take (size_td s) (drop n (access_ti0 t v)) = access_ti0 s v"
  using field_access_take_drop(1) [of t v] by (fastforce dest: wf_fdp_fdD wf_lf_fdp)

lemma singleton_t_field:
  "field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (t, n) ⟹
     heap_list_s (singleton_t p v |` fs_footprint p {f}) (size_td t) (ptr_val p + of_nat n) =
     access_ti0 t v"
  apply(clarsimp simp: heap_list_s_def singleton_def singleton_t_def)
  apply(subst heap_list_proj_h_restrict)
   apply(fastforce simp: fields_def fs_footprint_def
                   intro!: fs_footprint_subset
                   dest: field_footprint_SIndexVal)
  apply(subst heap_list_proj_h_lift_state)
   apply(frule field_tag_sub[where p=p] )
   apply(fastforce simp: field_lvalue_def dest: ptr_retyp_footprint[where d=empty_htd])
  apply(clarsimp simp: access_ti0_def heap_update_def)
  apply(subst heap_list_update_list; simp?)
   apply(simp add: size_of_def)
   apply(erule field_lookup_offset_size)
  apply(fastforce simp: access_ti0_def to_bytes_def heap_list_rpbs size_of_def
                  dest: field_access_take_dropD
                  elim: field_lookup_offset_size)
  done

lemma field_lookup_fd_consD:
  "field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (t,n) ⟹ fd_cons t"
  by (erule fd_consistentD) simp

lemma s_valid_map_add:
  "⟦ s,g ⊨s p; t,g' ⊨s p ⟧ ⟹ (s ++ t |` X),g ⊨s p"
  by (clarsimp simp: map_le_def s_valid_def h_t_valid_def valid_footprint_def Let_def
                     proj_d_map_add_snd proj_d_restrict_map_snd proj_d_map_add_fst
                     proj_d_restrict_map_fst)

lemma singleton_t_s_valid:
  "g p ⟹ singleton_t p (v::'a::mem_type),g ⊨s p"
  by (fastforce simp: singleton_t_def h_t_s_valid elim: ptr_retyp_h_t_valid)

lemma sep_map_mfs_sep_map:
  "⟦ (p ↦⇩g⇧F v) s; field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n) ⟧ ⟹
      (p ↦⇩g⇧({f}∪F) (v::'a::mem_type)) (s |` (dom s - fs_footprint p {f}))"
  apply(clarsimp simp: mfs_sep_map_def)
  apply(rule conjI)
   prefer 2
   apply(fastforce simp: fs_footprint_un[where F=F] fields_def)
  apply(clarsimp simp: lift_typ_heap_if split: if_split_asm)
  apply(rule conjI, clarsimp)
  subgoal premises prems
  proof -
    have "(singleton_t p v ++
                        s |` (s_footprint p - fs_footprint p F - fs_footprint p {f})) =
                      (singleton_t p v ++ s) ++ (singleton_t p v |` fs_footprint p {f})"
      using prems
      apply(simp add: map_add_restrict_sub)
      done
    then show ?thesis
      using prems
      apply clarsimp
      apply(subst heap_list_s_map_add_super_update_bs)
         apply clarsimp
         apply(subgoal_tac "fs_footprint p {f} ⊆ s_footprint p")
          apply(subgoal_tac "{x. (x, SIndexVal) ∈ fs_footprint p {f}} =
                           {ptr_val p + of_nat n..+size_td t}")
           apply fast
          apply(clarsimp simp: fs_footprint_def)
          apply(erule field_footprint_SIndexVal)
         apply(rule fs_footprint_subset)
         apply(clarsimp simp: fields_def)
        apply(clarsimp simp: size_of_def)
        apply(subst ac_simps)
        apply(rule td_set_offset_size)
        apply(erule td_set_field_lookupD)
       apply simp
      apply(clarsimp simp: from_bytes_def)
      apply(frule_tac v="heap_list_s (singleton_t p v |` fs_footprint p {f}) (size_td t)
                                   (ptr_val p + of_nat n)" and
          bs="heap_list_s (singleton_t p v ++ s) (size_of TYPE('a)) (ptr_val p)" and
          w=undefined in fi_fu_consistentD; simp)
       apply(simp add: size_of_def)
      apply(simp add: singleton_t_field)
      apply(fastforce simp: access_ti0_def fd_cons_update_access dest!: field_lookup_fd_consD)
      done
  qed
  subgoal premises prems
  proof -
    have  "(singleton_t p v ++
                       s |` (s_footprint p - fs_footprint p F - fs_footprint p {f})) =
                     (singleton_t p v ++ s) ++ (singleton_t p v |` fs_footprint p {f})"
      using prems by (simp add: map_add_restrict_sub)
    then show ?thesis using prems
      by(fastforce intro: s_valid_map_add singleton_t_s_valid ptr_retyp_h_t_valid)
  qed
  done

lemma disjoint_fn_disjoint:
  "⟦ disjoint_fn f F; F ⊆ fields TYPE('a::mem_type);
      field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n) ⟧ ⟹
      fs_footprint (p::'a ptr) F ∩ field_footprint p f = {}"
  apply(clarsimp simp: fs_footprint_def field_footprint_def s_footprint_untyped_def field_typ_def
                       field_typ_untyped_def fields_def)
  apply safe
  apply (drule (1) subsetD, clarsimp,
         drule (1) fa_fu_lookup_disj_interD;
         force intro: intvlI simp: max_size[unfolded size_of_def] disj_fn_def disjoint_fn_def)
  apply (drule (1) subsetD, clarsimp,
         drule (1) fa_fu_lookup_disj_interD;
         force intro: intvlI simp: max_size[unfolded size_of_def] disj_fn_def disjoint_fn_def)
  done

lemma sep_map_mfs_sep_map2:
  "⟦field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s, n);
       disjoint_fn f F; guard_mono g g';
       export_uinfo s = typ_uinfo_t TYPE('b); ((p::'a ptr) ↦⇩g⇧F v) x⟧
        ⟹ (Ptr &(p→f) ↦⇩g' ((from_bytes (access_ti0 s v))::'b::mem_type))
            (x |` field_footprint p f)"
  apply(clarsimp simp: mfs_sep_map_def sep_map_def)
  apply(rule conjI)
  subgoal premises prems
  proof -
    have "field_footprint p f = s_footprint ((Ptr &(p→f))::'b ptr)"
      using prems
      by(clarsimp simp: field_footprint_def s_footprint_def field_lvalue_def typ_uinfo_t_def
          field_typ_def field_typ_untyped_def)
    then show ?thesis
      using prems
      apply simp
      apply(frule lift_typ_heap_mono, assumption+)
      apply(clarsimp simp: lift_typ_heap_if split: if_split_asm)
      apply(rule conjI, fastforce simp: heap_list_s_heap_merge_right[where p="&(p→f)"])
      apply(erule s_valid_heap_merge_right2)
      apply simp
      apply(frule (2) disjoint_fn_disjoint[where p=p])
      apply(subgoal_tac "fs_footprint p {f} ⊆ s_footprint p")
       apply(fastforce simp: fs_footprint_def)
      apply(rule fs_footprint_subset)
      apply(fastforce simp: fields_def)
      done
  qed
  apply(clarsimp simp: field_footprint_def field_lvalue_def s_footprint_def field_typ_def
      field_typ_untyped_def)
  subgoal premises prems
  proof -
    have "{f} ⊆ fields TYPE('a)"
      using prems by(clarsimp simp: fields_def)
    then show ?thesis
      using prems
      apply -
      apply(drule fs_footprint_subset[where F="{f}" and p=p])
      apply(subst (asm) (2) fs_footprint_def)
      apply(clarsimp simp: field_footprint_def s_footprint_def field_typ_def field_typ_untyped_def)
      apply(subgoal_tac "fs_footprint p F ∩
                      s_footprint_untyped (ptr_val p + of_nat n) (typ_uinfo_t TYPE('b)) = {}")
       apply blast
      apply(drule disjoint_fn_disjoint[where p=p], assumption+)
      apply(simp add: field_footprint_def field_typ_def field_typ_untyped_def)
      done

  qed
  done

lemma export_size_of:
  "export_uinfo t = typ_uinfo_t TYPE('a) ⟹ size_of TYPE('a::c_type) = size_td t"
  by (fastforce simp: size_of_def simp flip: typ_uinfo_size dest: sym)

lemma sep_map_field_unfold:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n);
      disjoint_fn f F; guard_mono g g';
      export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
      (p ↦⇩g⇧F v) = (p ↦⇩g⇧({f}∪F) (v::'a::mem_type) ∧*
          Ptr (&(p→f)) ↦⇩g' ((from_bytes (access_ti0 t v))::'b::mem_type))"
  supply unsigned_of_nat [simp del]
  apply(rule ext)
  apply(rule iffI)
  subgoal for x
    apply(rule sep_conjI [where  s0="x |` (dom x - fs_footprint p {f})" and
          s1="x |` fs_footprint p {f}"] )
       apply(erule (1) sep_map_mfs_sep_map)
      apply(clarsimp simp: fs_footprint_def)
      apply(erule (4) sep_map_mfs_sep_map2)
     apply(clarsimp simp: map_disj_def)
     apply fast
    apply clarsimp
    done

  apply(drule sep_conjD, clarsimp)
  apply(clarsimp simp: mfs_sep_map_def sep_map_def)
  apply(rule conjI)
   apply(subst map_ac_simps)
   apply(subst map_add_com, solves ‹simp add: map_ac_simps›)
   apply(subst map_add_assoc)
   apply(clarsimp simp: lift_typ_heap_if split: if_split_asm)
   apply(rule conjI, clarsimp)
    apply(subst heap_list_s_map_add_super_update_bs)
       apply(subst s_footprint_untyped_dom_SIndexVal)
        apply(fastforce simp: s_footprint_def)
       apply(fastforce simp: field_lvalue_def)
      apply(drule field_lookup_offset_size)
      apply(drule export_size_of)
      apply(simp add: size_of_def)
     apply simp
    apply(clarsimp simp: from_bytes_def)
  subgoal for s0 s1
    apply(frule fi_fu_consistentD [where v="heap_list_s s1 (size_td (typ_info_t TYPE('b))) (ptr_val p + of_nat n)" and
          bs="heap_list_s (singleton_t p v ++ s0) (size_of TYPE('a)) (ptr_val p)" and
          w=undefined]; simp)
      apply(simp add: size_of_def)
     apply(drule export_size_of, simp add: size_of_def)
    apply(subst fd_cons_update_normalise [symmetric])
      apply(erule field_lookup_fd_consD)
     apply simp
     apply(drule export_size_of, simp add: size_of_def)
    apply(simp add: norm_desc_def)
    apply(drule arg_cong [where f="access_ti0 (typ_info_t TYPE('b))"])
    apply(drule arg_cong [where f="λbs. update_ti_t t bs v"])
    apply(subst (asm) wf_fd_norm_tuD [symmetric]; simp?)
     apply(simp add: size_of_def)
    apply(subst (asm) wf_fd_norm_tuD [symmetric])
      apply simp
     apply(subst fd_cons_length_p)
      apply(erule field_lookup_fd_consD)
     apply(drule export_size_of, simp add: size_of_def)
    apply(subgoal_tac "export_uinfo (typ_info_t TYPE('b)) = typ_uinfo_t TYPE('b)")
     prefer 2
     apply(simp add: typ_uinfo_t_def)
    apply simp
    apply(drule sym, simp)
    apply(subst (asm) wf_fd_norm_tuD)
      apply(erule wf_fd_field_lookupD, simp)
     apply simp
     apply(drule sym, drule export_size_of)
     apply(simp add: size_of_def)
    apply(simp add: access_ti0_def)
    apply(clarsimp simp: field_lvalue_def)
    apply(simp add: size_of_def)
    apply(subst wf_fd_norm_tuD)
      apply(erule wf_fd_field_lookupD, simp)
     apply(subst fd_cons_length; simp?)
     apply(erule field_lookup_fd_consD)
    apply(subgoal_tac "update_ti_t t (norm_desc (field_desc t) (size_td t)
                                     (access_ti t v (replicate (size_td t) 0))) v = v")
     apply(simp add: norm_desc_def access_ti0_def)
    apply(subst fd_cons_update_normalise)
      apply(erule field_lookup_fd_consD)
     apply(subst fd_cons_length; simp?)
     apply(erule field_lookup_fd_consD)
    apply(subst fd_cons_update_access; simp?)
    apply(erule field_lookup_fd_consD)
    done

   prefer 2
   apply(subst fs_footprint_un)
   apply(subst fs_footprint_def)
   apply(clarsimp simp: field_footprint_def s_footprint_def field_lvalue_def field_typ_def)
   apply(drule disjoint_fn_disjoint [where p=p]; assumption?)
   apply(clarsimp simp: field_footprint_def s_footprint_def field_lvalue_def field_typ_def)
   apply(subgoal_tac "{f} ⊆ fields TYPE('a)")
    apply(drule fs_footprint_subset[where F="{f}" and p = p])
    apply(clarsimp simp: s_footprint_def)
    apply(fastforce simp: fs_footprint_def field_footprint_def s_footprint_def
      field_typ_def field_typ_untyped_def field_lvalue_def)
   apply(clarsimp simp: fields_def)
  apply(clarsimp simp: s_valid_def h_t_valid_def valid_footprint_def Let_def)

  subgoal for s0 s1 y
    apply(standard, clarsimp simp: map_le_def) 
    subgoal for a
      apply(subst proj_d_map_add_snd[where s="a ++ b" for a b])
      apply(clarsimp split: if_split_asm)
      apply(frule s_footprintD2)
      apply(drule s_footprintD)
      apply(drule spec [where x=y])
      apply clarsimp
      apply(drule bspec [where x=a])
       apply clarsimp
      apply(drule intvlD, clarsimp simp: field_lvalue_def)
      subgoal for k
        apply(drule spec [where x=k])
        apply(clarsimp simp add: size_of_def)
        apply(drule bspec [where x=a])
         apply clarsimp
         apply(subst (asm) unat_of_nat)
         apply(subst (asm) mod_less)
          apply(subst len_of_addr_card)
          apply(erule less_trans)
          apply(simp add: max_size[unfolded size_of_def])
         apply simp
        apply(simp add: ac_simps)
        apply(rotate_tac -1)
        apply(drule sym)
        apply simp
        apply(drule sym[where s="Some s" for s])
        apply simp
        apply(drule field_lookup_export_uinfo_Some)
        apply(drule td_set_field_lookupD)
        apply(frule typ_slice_td_set [where k=k])
         apply simp
        apply simp
        apply(simp add: typ_uinfo_t_def)
        apply(subgoal_tac "y=n+k")
         apply(simp add: strict_prefix_def)
         apply(subst (asm) unat_of_nat)
         apply(subst (asm) mod_less)
          apply(subst len_of_addr_card)
          apply(erule less_trans)
          apply(simp add: max_size[unfolded size_of_def])
         apply (clarsimp simp: prefix_eq_nth)
        apply(drule arg_cong [where f=unat])
        apply(rotate_tac -1)
        apply(subst (asm) unat_of_nat)
        apply(subst (asm) mod_less)
         apply(subst len_of_addr_card)
         apply(erule less_trans)
         apply(simp add: max_size[unfolded size_of_def])
        apply(subst (asm) Abs_fnat_hom_add)
        apply(subst (asm) unat_of_nat)
        apply(subst (asm) mod_less)
         apply(subst len_of_addr_card)
         apply(drule td_set_offset_size)
         apply(rule le_less_trans [where y="size_td (typ_info_t TYPE('a))"] , simp)
         apply(simp add: max_size[unfolded size_of_def])
        apply simp
        done
      done

    apply(subst proj_d_map_add_fst)
    apply(fastforce simp: size_of_def field_lvalue_def ac_simps
        dest: intvlD s_footprintD)
    done
  done

lemma disjoint_fn_empty [simp]:
  "disjoint_fn f {}"
  by (simp add: disjoint_fn_def)

lemma sep_map_field_map':
  "⟦ ((p::'a::mem_type ptr) ↦⇩g v) s;
     field_lookup (typ_info_t TYPE('a)) f 0 = Some (d,n); export_uinfo d = typ_uinfo_t TYPE('b);
     guard_mono g g' ⟧ ⟹
   ((Ptr (&(p→f))::'b::mem_type ptr) ↪⇩g' from_bytes (access_ti0 d v)) s"
  by (fastforce dest: sep_map_g elim: sep_conj_impl
                simp: sep_map_mfs_sep_map_empty sep_map_field_unfold sep_map'_def sep_conj_ac)

lemma fd_cons_access_update_p:
  "⟦ fd_cons t; length bs = size_td t ⟧ ⟹
      access_ti0 t (update_ti_t t bs v) = access_ti0 t (update_ti_t t bs w)"
  by (simp add: fd_cons_def Let_def fd_cons_access_update_def fd_cons_desc_def access_ti0_def)

lemma length_to_bytes_p [simp]:
  "length (to_bytes_p (v::'a)) = size_of TYPE('a::mem_type)"
  by (simp add: to_bytes_p_def)

lemma inv_p [simp]:
  "from_bytes (to_bytes_p v) = (v::'a::mem_type)"
  by (simp add: to_bytes_p_def)

lemma singleton_SIndexVal:
  "x ∈ {ptr_val p..+size_of TYPE('a)} ⟹
      singleton_t p (v::'a::mem_type) (x,SIndexVal) = Some (SValue (to_bytes_p v ! unat (x - ptr_val p)))"
  by (clarsimp simp: singleton_def singleton_t_def lift_state_def heap_update_def
                     heap_update_mem_same_point to_bytes_p_def heap_list_rpbs ptr_retyp_d_eq_fst)

lemma access_ti0:
  "access_ti s v (replicate (size_td s) 0) = access_ti0 s v"
  by (simp add: access_ti0_def)

lemma fd_cons_mem_type [simp]:
  "fd_cons (typ_info_t TYPE('a::mem_type))"
  by (rule wf_fd_consD) simp

lemma norm_tu_rpbs:
  "wf_fd t ⟹ norm_tu (export_uinfo t) (access_ti0 t v) = access_ti0 t v"
  apply(frule wf_fd_consD)
  apply(simp add: wf_fd_norm_tuD fd_cons_length_p)
  apply(subst fd_cons_access_update_p [where w=v]; (simp add: fd_cons_length_p)?)
  apply(fastforce simp: access_ti0_def fd_cons_update_access)
  done

lemma heap_list_s_singleton_t_field_update:
  "⟦ field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s, n);
     export_uinfo s = typ_uinfo_t TYPE('b) ⟧ ⟹
       heap_list_s (singleton_t p (update_ti_t s (to_bytes_p w) v)) (size_td s)
                   (ptr_val (p::'a::mem_type ptr) + of_nat n) =
       to_bytes_p (w::'b::mem_type)"
  apply(clarsimp simp: singleton_t_def singleton_def)
  apply(subst heap_list_s_heap_list_dom)
   apply clarsimp
   apply(frule field_tag_sub [where p=p])
   apply(clarsimp simp: field_lvalue_def)
   apply(drule (1) subsetD)
   apply(drule intvlD [where n="size_of TYPE('a)"], clarsimp)
   apply(erule s_footprintI2)
  apply(simp add: heap_update_def)
  apply(subst heap_list_update_list; simp?)
   apply(drule field_lookup_offset_size)
   apply(simp add: size_of_def)
  apply(frule field_access_take_dropD [where v="(update_ti_t s (to_bytes_p w) v)"]; simp?)
  apply(simp add: access_ti0_def to_bytes_def heap_list_rpbs size_of_def to_bytes_p_def)
  apply(simp add: access_ti0)
  apply(subst fd_cons_access_update_p [where w=undefined])
    apply(erule field_lookup_fd_consD)
   apply(subst fd_cons_length_p)
    apply simp
   apply(drule export_size_of, simp add: size_of_def)
  apply(subst wf_fd_norm_tuD [symmetric])
    apply(erule wf_fd_field_lookupD)
    apply simp
   apply(fastforce simp: fd_cons_length_p size_of_def dest: export_size_of)
  apply(simp add: typ_uinfo_t_def norm_tu_rpbs)
  done

lemma field_access_update_nth_disj:
  fixes
   t::"('a,'b) typ_info" and
   st::"('a,'b) typ_info_struct" and
   ts::"('a,'b) typ_info_tuple list" and
   y::"('a,'b) typ_info_tuple"
  shows
  "∀m f s n x bs bs'. field_lookup t f m = Some (s,n) ⟶ x < size_td t ⟶
      (x < n - m ∨ x ≥ (n - m) + size_td s) ⟶ wf_fd t ⟶ length bs = size_td s ⟶ length bs' = size_td t ⟶
      access_ti t (update_ti_t s bs v) bs' ! x
          = access_ti t v bs' ! x"
  "∀m f s n x bs bs'. field_lookup_struct  st f m = Some (s,n) ⟶ x < size_td_struct st ⟶
      (x < n -  m ∨ x ≥ (n - m) + size_td s) ⟶ wf_fd_struct st ⟶length bs = size_td s ⟶ length bs' = size_td_struct st ⟶
      access_ti_struct st (update_ti_t s bs v) bs' ! x
          = access_ti_struct st v bs' ! x"
  "∀m f s n x bs bs'. field_lookup_list ts f m = Some (s,n) ⟶ x < size_td_list ts ⟶
      (x < n -  m ∨ x ≥ (n - m) + size_td s) ⟶ wf_fd_list ts ⟶length bs = size_td s ⟶ length bs' = size_td_list ts ⟶
      access_ti_list ts (update_ti_t s bs v) bs' ! x
          = access_ti_list ts v bs' ! x"
  "∀m f s n x bs bs'. field_lookup_tuple y f m = Some (s,n) ⟶ x < size_td_tuple y ⟶
      (x < n -  m ∨ x ≥ (n - m) + size_td s) ⟶ wf_fd_tuple y ⟶length bs = size_td s ⟶ length bs' = size_td_tuple y ⟶
      access_ti_tuple y (update_ti_t s bs v) bs' ! x
          = access_ti_tuple y v bs' ! x"
proof(induct t and st and ts and y)
  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 clarify
    subgoal for m f s n x bs bs'
      apply(clarsimp split: if_split_asm)
      apply(clarsimp split: option.splits)

       apply(rotate_tac -3)
       apply(drule spec [where x="m + size_td (dt_fst dt_tuple)"])
       apply(drule spec [where x=f])
       apply(drule spec [where x=s])
       apply(rotate_tac -1)
       apply(drule spec [where x=n])

       apply clarsimp
       apply(rotate_tac -1)
       apply(drule_tac spec [where x="x - size_td_tuple dt_tuple"])
       apply(frule field_lookup_fa_fu_rhs_listD)
         apply simp
        apply assumption
       apply(clarsimp simp: fa_fu_ind_def)
       apply(subgoal_tac "access_ti_tuple dt_tuple (update_ti_t s bs v) (take (size_td_tuple dt_tuple) bs') =
                      access_ti_tuple dt_tuple v (take (size_td_tuple dt_tuple) bs')")
        prefer 2
        apply (fastforce simp: min_def)
       apply(clarsimp simp: nth_append)
       apply(subgoal_tac "length
                 (access_ti_tuple dt_tuple v
                   (take (size_td_tuple dt_tuple) bs')) = size_td_tuple dt_tuple")
        apply simp
        prefer 2
        apply(drule wf_fd_cons_tupleD)
        apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def fd_cons_length_def)
       apply(erule impE)
        apply simp
       apply(cases dt_tuple, simp+)
      subgoal for a b c

        apply(drule spec [where x=bs])
        apply(drule spec [where x="drop (size_td a) bs'"])
        apply clarsimp
        apply(frule field_lookup_offset_le)
        apply clarsimp
        apply(drule td_set_list_field_lookup_listD)
        apply(drule td_set_list_offset_size_m)
        apply clarsimp
        apply(erule disjE)
         apply arith
        apply arith
        done
      apply(frule field_lookup_fa_fu_rhs_tupleD, simp)
       apply assumption
      apply(clarsimp simp: fa_fu_ind_def)
      apply(subgoal_tac "length (access_ti_tuple dt_tuple (update_ti_t s bs v)
                            (take (size_td_tuple dt_tuple) bs')) = size_td_tuple dt_tuple")
       apply(subgoal_tac "length (access_ti_tuple dt_tuple v
                             (take (size_td_tuple dt_tuple) bs')) = size_td_tuple dt_tuple")
        apply(clarsimp simp: nth_append)
        apply(drule spec [where x=m])
        apply(drule spec [where x=f])
        apply(drule spec [where x=s])
        apply(drule spec [where x=n])
        apply clarsimp
        apply(drule spec [where x=x])
        apply clarsimp
        apply(drule spec [where x=bs])
        apply(drule spec [where x="take (size_td_tuple dt_tuple) bs'"])
        apply(clarsimp simp: min_def split: if_split_asm)
       apply(drule wf_fd_cons_tupleD)
       apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def fd_cons_length_def)
      apply(drule wf_fd_cons_tupleD)
      apply(clarsimp simp: fd_cons_tuple_def fd_cons_desc_def fd_cons_length_def)
      done
    done
next
  case (DTuple_typ_desc typ_desc list b)
  then show ?case by auto
qed
   

lemma field_access_update_nth_disjD:
  "⟦ field_lookup t f m = Some (s,n); x < size_td t;
      (x < n - m ∨ x ≥ (n - m) + size_td s);  wf_fd t;
      length bs = size_td s; length bs' = size_td t ⟧ ⟹
      access_ti t (update_ti_t s bs v) bs' ! x
          = access_ti t v bs' ! x"
  by (simp add: field_access_update_nth_disj)

lemma intvl_cut:
  "⟦ (x::addr) ∈ {p..+m}; x ∉ {p+of_nat k..+n}; m < addr_card ⟧ ⟹
      unat (x - p) < k ∨ k + n ≤ unat (x - p)"
  supply unsigned_of_nat [simp del]
  apply(drule intvlD, clarsimp)
  apply(subst unat_of_nat, subst mod_less, subst len_of_addr_card)
   apply(erule (1) less_trans)
  apply(subst (asm) unat_of_nat, subst (asm) mod_less, subst len_of_addr_card)
   apply(erule (1) less_trans)
  apply(rule ccontr)
  apply(subgoal_tac "∃z. ka = k + z")
   apply(force simp flip: add.assoc intro: intvlI)
  apply arith
  done

lemma singleton_t_mask_out:
  "⟦ field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s,n);
      export_uinfo s = typ_uinfo_t TYPE('b);
      K = (UNIV - s_footprint_untyped &(p→f) (export_uinfo s)) ⟧ ⟹
    singleton_t p (update_ti_t s (to_bytes_p (w::'b::mem_type)) (v::'a)) |` K =
    singleton_t p v |` K"
  supply unsigned_of_nat [simp del]
  supply max_size[unfolded size_of_def, simp]
  apply(rule ext)
  apply(clarsimp simp: restrict_map_def singleton_t_def singleton_def lift_state_def
                       heap_update_def to_bytes_def access_ti0 heap_list_rpbs size_of_def
                 split: s_heap_index.splits)
  apply(subst heap_update_mem_same_point)
    apply(fastforce simp: fd_cons_length_p ptr_retyp_None size_of_def intro: ccontr)
   apply(simp add: fd_cons_length_p)
  apply(subst heap_update_mem_same_point)
    apply(fastforce simp: fd_cons_length_p ptr_retyp_None size_of_def intro: ccontr)
   apply(simp add: fd_cons_length_p)
  apply(simp add: access_ti0_def)
  apply(rule field_access_update_nth_disjD; simp?)
    apply(subst (asm) ptr_retyp_d_eq_fst)
    apply(clarsimp simp: empty_htd_def split: if_split_asm)
    apply(drule intvlD, clarsimp)
    apply(subst unat_of_nat)
    apply(subst mod_less)
     apply(subst len_of_addr_card)
     apply(erule less_trans)
     apply simp
    apply(simp add: size_of_def)
   apply(clarsimp simp: empty_htd_def ptr_retyp_d_eq_fst split: if_split_asm)
   apply(drule_tac k="of_nat n" and n="size_td s" in intvl_cut; simp?)
   apply(fastforce dest: intvlD export_size_of
                   simp: size_of_def s_footprint_untyped_def field_lvalue_def)
  apply(drule export_size_of, simp add: size_of_def)
  done

lemma singleton_t_SIndexTyp:
  "singleton_t p v (x,SIndexTyp n) = singleton_t p undefined (x,SIndexTyp n)"
  by (auto simp: singleton_t_def singleton_def restrict_map_def lift_state_def)


lemma proj_d_singleton_t:
  "proj_d (singleton_t p (v::'a::mem_type) ++ x) = proj_d (singleton_t p undefined ++ x)"
  apply(rule ext)
  apply(clarsimp simp: proj_d_def)
  apply(safe)
    apply(subgoal_tac "dom (singleton_t p undefined) = dom (singleton_t p v)", blast, simp)+
  apply(rule ext)
  apply(clarsimp split: option.splits)
  apply(safe; clarsimp?)
    apply(subgoal_tac "dom (singleton_t p undefined) = dom (singleton_t p v)", blast, simp)+
  apply(subst (asm) singleton_t_SIndexTyp)
  apply simp
  done

lemma from_bytes_heap_list_s_update:
  "⟦ field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s, n);
     export_uinfo s = typ_uinfo_t TYPE('b::mem_type);
     dom x = s_footprint p - fs_footprint p F; f ∈ F ⟧ ⟹
   from_bytes (heap_list_s (singleton_t p (update_ti_t s (to_bytes_p (w::'b)) (v::'a)) ++ x)
                           (size_of TYPE('a)) (ptr_val p))  =
   update_ti_t s (to_bytes_p w)
                 (from_bytes (heap_list_s (singleton_t p v ++ x) (size_of TYPE('a)) (ptr_val p)))"
  apply(subst map_add_restrict_UNIV [where X="s_footprint_untyped (&(p→f)) (export_uinfo s)" and
                                           h="singleton_t p v"])
    apply(force simp: fs_footprint_def field_footprint_def field_lvalue_def
                      field_typ_def field_typ_untyped_def )
   apply simp
  apply(subst heap_list_s_map_add_super_update_bs [where k=n and z="size_td s"]; simp?)
    apply(rule equalityI)
     apply(fastforce dest: s_footprintD export_size_of intro: intvlI
                     simp: s_footprint_untyped_def field_lvalue_def size_of_def)
    apply clarsimp
    apply(rule conjI)
     apply(frule field_tag_sub)
     apply(clarsimp simp: field_lvalue_def)
     apply(drule (1) subsetD)
     apply(fastforce elim: s_footprintI2 dest: intvlD)
    apply(fastforce dest: intvlD export_size_of
                    simp: size_of_def s_footprint_untyped_def field_lvalue_def)
   apply(fastforce dest: field_lookup_offset_size simp: size_of_def)
  apply(clarsimp simp: from_bytes_def)
  apply(frule_tac v="heap_list_s (singleton_t p (update_ti_t s (to_bytes_p w) v) |`
                                   s_footprint_untyped &(p→f) (export_uinfo s))
                                 (size_td s) (ptr_val p + of_nat n)" and
                  bs="heap_list_s (singleton_t p (update_ti_t s (to_bytes_p w) v) |`
                                    (UNIV - s_footprint_untyped &(p→f) (export_uinfo s)) ++
                                    singleton_t p v |`
                                      s_footprint_untyped &(p→f) (typ_uinfo_t TYPE('b)) ++ x)
                                  (size_of TYPE('a)) (ptr_val p)" and
                  w=undefined in fi_fu_consistentD; simp add: size_of_def)
  apply(subst heap_list_s_restrict)
   apply(fastforce dest: intvlD export_size_of
                   simp: size_of_def field_lvalue_def s_footprint_untyped_def)
  apply(simp add: heap_list_s_singleton_t_field_update)
  apply(subst singleton_t_mask_out; assumption?)
   apply simp
  apply(subst map_add_restrict_comp_left)
  apply simp
  done

lemma mfs_sep_map_field_update:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n); f ∈ F;
      export_uinfo s = typ_uinfo_t TYPE('b) ⟧ ⟹
   (p ↦⇩g⇧F update_ti_t s (to_bytes_p (w::'b::mem_type)) v) =
   (p ↦⇩g⇧F update_ti_t s (to_bytes_p (u::'b::mem_type)) (v::'a::mem_type))"
  apply(rule ext)
  apply(clarsimp simp: mfs_sep_map_def lift_typ_heap_if s_valid_def)
  apply safe
     apply(simp add: from_bytes_heap_list_s_update)
     apply(drule_tac f="update_ti_t s (to_bytes_p u)" in arg_cong)
     apply(simp add: fd_cons_double_update field_lookup_fd_consD)
    apply(simp add: from_bytes_heap_list_s_update)
    apply(drule_tac f="update_ti_t s (to_bytes_p w)" in arg_cong)
    apply(simp add: fd_cons_double_update field_lookup_fd_consD)
   apply(subst (asm) proj_d_singleton_t)
   apply(subst (asm) proj_d_singleton_t[where v="update_ti_t s (to_bytes_p u) v"])
   apply simp
  apply(subst (asm) proj_d_singleton_t)
  apply(subst (asm) proj_d_singleton_t[where v="update_ti_t s (to_bytes_p u) v"])
  apply simp
  done

lemma mfs_sep_map_field_update_v:
  "⟦field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n); f ∈ F;
     disjoint_fn f (F - {f}); guard_mono g g';
     export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
   p ↦⇩g⇧F update_ti_t t (to_bytes_p (w::'b::mem_type)) (v::'a::mem_type) = p ↦⇩g⇧F v"
  apply(subst mfs_sep_map_field_update [where u="from_bytes (access_ti0 t v)"]; simp?)
  apply(simp add: to_bytes_p_def to_bytes_def from_bytes_def access_ti0 size_of_def)
  apply(subst wf_fd_norm_tuD [symmetric], simp)
   apply(fastforce dest: fd_cons_length_p export_size_of field_lookup_fd_consD simp: size_of_def)
  apply(rotate_tac -1)
  apply(drule sym)
  apply(simp add: typ_uinfo_t_def)
  apply(subgoal_tac "norm_tu (typ_uinfo_t TYPE('b)) = norm_bytes TYPE('b)")
   prefer 2
   apply(simp add: norm_bytes_def typ_uinfo_t_def)
  apply(clarsimp simp: norm_bytes_def
                       wf_fd_norm_tuD wf_fd_field_lookupD fd_cons_length_p field_lookup_fd_consD)
  apply(subst fd_cons_access_update_p [where w=v])
    apply(erule field_lookup_fd_consD)
   apply(simp add: fd_cons_length_p field_lookup_fd_consD)
  apply(simp add: access_ti0_def fd_cons_update_access field_lookup_fd_consD)
  done

lemma sep_map_field_fold:
  "⟦ field_lookup (typ_info_t TYPE('a)) f 0 = Some (t,n);
      f ∈ F; disjoint_fn f (F - {f}); guard_mono g g';
      export_uinfo t = typ_uinfo_t TYPE('b) ⟧ ⟹
      (p ↦⇩g⇧F (v::'a::mem_type) ∧*
          Ptr &(p→f) ↦⇘g'⇙ (w::'b::mem_type))
      = p ↦⇩g⇧(F - {f}) (update_ti_t t (to_bytes_p w) v)"
  apply(simp add: sep_map_field_unfold)
  apply(subst fd_cons_access_update_p [where w=undefined])
    apply(erule field_lookup_fd_consD)
   apply(fastforce dest: export_size_of simp: size_of_def)
  apply(subst wf_fd_norm_tuD [symmetric])
    apply(simp add: wf_fd_field_lookupD)
   apply(fastforce dest: export_size_of simp: size_of_def)
  apply(subgoal_tac "norm_tu (typ_uinfo_t TYPE('b)) = norm_bytes TYPE('b)")
   apply(simp add: sep_conj_ac norm mfs_sep_map_field_update_v insert_absorb)
  apply(simp add: norm_bytes_def typ_uinfo_t_def)
  done

lemma norm_bytes:
  "length bs = size_of TYPE('a) ⟹
      to_bytes_p ((from_bytes bs)::'a) = norm_bytes TYPE('a::mem_type) bs"
  by (simp add: norm_bytes_def wf_fd_norm_tuD size_of_def to_bytes_p_def from_bytes_def
                to_bytes_def access_ti0_def)

lemma sep_heap_update_global_super_fl:
  "⟦ (p ↦⇩g u ∧* R) (lift_state (h,d));
      field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (t,n);
      export_uinfo t = (typ_uinfo_t TYPE('a)) ⟧ ⟹
   ((p ↦⇩g update_ti_t t (to_bytes_p v) u) ∧* R)
     (lift_state (heap_update (Ptr &(p→f)) (v::'a::mem_type) h,d))"
  apply(subst sep_map_mfs_sep_map_empty)
  apply(simp add: sep_map_field_unfold [where g'="λx. True"] guard_mono_def)
  apply(subst fd_cons_access_update_p [where w=undefined])
    apply(erule field_lookup_fd_consD)
   apply simp
   apply(simp add: export_size_of)
  apply(subst wf_fd_norm_tuD [symmetric])
    apply(erule wf_fd_field_lookupD, simp)
   apply(simp add: export_size_of)
  apply(subgoal_tac "norm_tu (typ_uinfo_t TYPE('a)) = norm_bytes TYPE('a)")
   prefer 2
   apply(simp add: norm_bytes_def typ_uinfo_t_def)
  apply(simp add: norm sep_conj_ac)
  apply(subst sep_conj_com)
  apply(simp add: sep_conj_assoc)
  apply(rule sep_heap_update_global_exc2 [where u="from_bytes (access_ti0 t u)"])
  apply(simp add: sep_conj_ac)
  apply(subst sep_conj_com)
  apply(simp add: sep_map_field_fold guard_mono_def)
  apply(subst sep_map_mfs_sep_map_empty [symmetric])
  apply(simp add: fd_cons_double_update field_lookup_fd_consD)
  apply(simp add: norm_bytes fd_cons_length_p field_lookup_fd_consD export_size_of)
  apply(simp add: norm_bytes_def typ_uinfo_t_def)
  apply(rotate_tac -1)
  apply(drule sym)
  apply(simp add: wf_fd_norm_tuD wf_fd_field_lookupD fd_cons_length_p field_lookup_fd_consD)
  apply(subst fd_cons_access_update_p [where w=u])
    apply(erule field_lookup_fd_consD)
   apply(simp add: fd_cons_length_p field_lookup_fd_consD)
  apply(simp add: access_ti0_def fd_cons_update_access field_lookup_fd_consD sep_conj_com)
  done

lemma sep_cut'_dom:
  "sep_cut' x y s ⟹ dom s = {(a,b). a ∈ {x..+y}}"
  by (simp add: sep_cut'_def)

lemma dom_exact_sep_cut':
  "dom_exact (sep_cut' x y)"
  by (force intro!: dom_exactI dest!: sep_cut'_dom)

lemma dom_lift_state_dom_s [simp]:
  "dom (lift_state (h,d)) = dom_s d"
  by (force simp: lift_state_def dom_s_def split: s_heap_index.splits if_split_asm option.splits)

lemma dom_ptr_retyp_empty_htd [simp]:
  "dom (lift_state (h,ptr_retyp (p::'a::mem_type ptr) empty_htd)) = s_footprint p"
  by simp

lemma ptr_retyp_sep_cut'_exc:
  fixes p::"'a::mem_type ptr"
  assumes sc: "(sep_cut' (ptr_val p) (size_of TYPE('a)) ∧* P) (lift_state (h,d))" and "g p"
  shows "(g ⊢s p ∧* sep_true ∧* P) (lift_state (h,(ptr_retyp p d)))"
proof -
  from sc
  obtain s0 and s1 where "s0 ⊥ s1" and "lift_state (h,d) = s1 ++ s0" and
         "P s1" and d: "dom s0 = {(a,b). a ∈ {ptr_val p..+size_of TYPE('a)}}"
    by (fast dest: sep_conjD sep_cut'_dom)
  moreover from this
  have "lift_state (h, ptr_retyp p d) = s1 ++ lift_state (h, ptr_retyp p d) |` dom s0"
    apply -
    apply(rule ext)
    subgoal for x
      apply (cases "x ∈ dom s0")
       apply(cases "x ∈ dom s1")
        apply(fastforce simp: map_disj_def)
       apply(subst map_add_com)
        apply(fastforce simp: map_disj_def)
       apply(clarsimp simp: map_add_def split: option.splits)
      apply(cases x, clarsimp)
      apply(clarsimp simp: lift_state_ptr_retyp_d merge_dom2)
      done
    done
  moreover have "g p" by fact
  with d have "(g ⊢s p ∧* sep_true) (lift_state (h, ptr_retyp p d) |` dom s0)"
    apply(clarsimp simp: lift_state_ptr_retyp_restrict sep_conj_ac intro: ptr_retyp_tagd_exc)
    apply(rule sep_conjI [where s0="lift_state (h,d) |` ({(a, b). a ∈ {ptr_val p..+size_of TYPE('a)}} - s_footprint p)"])
       apply (simp add: sep_conj_ac)
      apply(erule ptr_retyp_tagd_exc [where h=h])
     apply(fastforce simp: map_disj_def)
    apply(subst map_add_com[where h0="lift_state (h, ptr_retyp p empty_htd)"])
     apply (simp add: map_disj_def)
     apply fast
    apply(rule ext)
    apply(clarsimp simp: map_add_def split: option.splits)
    by (metis (mono_tags) Diff_iff dom_ptr_retyp_empty_htd non_dom_eval_eq restrict_in_dom restrict_out)
  ultimately
  show ?thesis
    by (subst sep_conj_assoc [symmetric])
       (rule sep_conjI [where s0="(lift_state (h,ptr_retyp p d))|`dom s0" and s1=s1],
        auto simp: map_disj_def)
qed

lemma sep_cut_dom:
  "sep_cut x y s ⟹ dom s = {(a,b). a ∈ {x..+unat y}}"
  by (force simp: sep_cut_def dest: sep_cut'_dom)

lemma sep_cut_0 [simp]:
  "sep_cut p 0 = □"
  by (auto simp: sep_cut'_def sep_cut_def sep_emp_def None_com split_def)

lemma heap_merge_restrict_dom_un:
  "dom s = P ∪ Q ⟹ (s|`P) ++ (s|`Q) = s"
  by (force simp: map_add_def restrict_map_def split: option.splits)

lemma sep_cut_split:
  assumes sc: "sep_cut p y s" and le: "x ≤ y"
  shows "(sep_cut p x ∧* sep_cut (p + x) (y - x)) s"
proof (rule sep_conjI [where s0="s|`{(a,b). a ∈ {p..+unat x}}" and
                s1="s|`({(a,b). a ∈ {p..+unat y}} - {(a,b). a ∈ {p..+unat x}})"])
  from sc le show "sep_cut p x (s |` {(a,b). a ∈ {p..+unat x}})"
    by (force simp: sep_cut_def sep_cut'_def word_le_nat_alt
              dest: intvl_start_le)
next
  from sc le
  show "sep_cut (p + x) (y - x) (s |` ({(a,b). a ∈ {p..+unat y}} - {(a,b). a ∈ {p..+unat x}}))"
    by (force simp: sep_cut_def sep_cut'_def intvl_sub_eq)
next
  show "s |` {(a,b). a ∈ {p..+unat x}} ⊥ s |` ({(a,b). a ∈ {p..+unat y}} - {(a,b). a ∈ {p..+unat x}})"
    by (force simp: map_disj_def)
next
  from sc le
  show "s = s |` ({(a,b). a ∈ {p..+unat y}} - {(a,b). a ∈ {p..+unat x}}) ++ s |` {(a,b). a ∈ {p..+unat x}}"
    by (simp add: sep_cut_def sep_cut'_def, subst heap_merge_restrict_dom_un)
       (auto simp: word_le_nat_alt dest: intvl_start_le)
qed

lemma tagd_ptr_safe_exc:
  "(g ⊢s p ∧* sep_true) (lift_state (h,d)) ⟹ ptr_safe p d"
  apply(clarsimp simp: ptr_safe_def sep_conj_ac sep_conj_def, drule tagd_dom_exc)
  apply(drule_tac x="(a,b)" in fun_cong)
  apply(force simp: map_ac_simps lift_state_def sep_conj_ac dom_s_def merge_dom
                 split: option.splits s_heap_index.splits if_split_asm)

  done

lemma sep_map'_ptr_safe_exc:
  "(p ↪⇩g (v::'a::mem_type)) (lift_state (h,d)) ⟹ ptr_safe p d"
  by (force simp: sep_map'_def intro: sep_conj_impl tagd_ptr_safe_exc
            dest: sep_map_tagd_exc)

end