Theory DocumentMonad

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 * 
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section‹Document›
text‹In this theory, we introduce the monadic method setup for the Document class.›

theory DocumentMonad
  imports
    CharacterDataMonad
    "../classes/DocumentClass"
begin

type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 
    'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document, 'result) dom_prog
  = "((_) heap, exception, 'result) prog"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 
           'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document, 'result) dom_prog" 


global_interpretation l_ptr_kinds_M document_ptr_kinds defines document_ptr_kinds_M = a_ptr_kinds_M .
lemmas document_ptr_kinds_M_defs = a_ptr_kinds_M_def

lemma document_ptr_kinds_M_eq:
  assumes "|h ⊢ object_ptr_kinds_M|⇩r = |h' ⊢ object_ptr_kinds_M|⇩r"
  shows "|h ⊢ document_ptr_kinds_M|⇩r = |h' ⊢ document_ptr_kinds_M|⇩r"
  using assms 
  by(auto simp add: document_ptr_kinds_M_defs object_ptr_kinds_M_defs document_ptr_kinds_def)

lemma document_ptr_kinds_M_reads: 
  "reads (⋃object_ptr. {preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing)}) document_ptr_kinds_M h h'"
  using object_ptr_kinds_M_reads
  apply (simp add: reads_def object_ptr_kinds_M_defs document_ptr_kinds_M_defs 
    document_ptr_kinds_def preserved_def cong del: image_cong_simp)
  apply (metis (mono_tags, opaque_lifting) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)
  done

global_interpretation l_dummy defines get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t = "l_get_M.a_get_M get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t" .
lemma get_M_is_l_get_M: "l_get_M get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t type_wf document_ptr_kinds"
  apply(simp add: get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_type_wf l_get_M_def)
  by (metis ObjectClass.get⇩O⇩b⇩j⇩e⇩c⇩t_type_wf ObjectClass.type_wf_defs bind_eq_None_conv 
      document_ptr_kinds_commutes get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def option.simps(3))
lemmas get_M_defs = get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t

locale l_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_lemmas = l_type_wf⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t
begin
sublocale l_get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_lemmas by unfold_locales

interpretation l_get_M get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t type_wf document_ptr_kinds
  apply(unfold_locales)
   apply (simp add: get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_type_wf local.type_wf⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t)
  by (meson DocumentMonad.get_M_is_l_get_M l_get_M_def)
lemmas get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok = get_M_ok[folded get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def]
end

global_interpretation l_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_lemmas type_wf by unfold_locales


global_interpretation l_put_M type_wf document_ptr_kinds get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t 
  rewrites "a_get_M = get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t" defines put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def)

lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t


locale l_put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_lemmas = l_type_wf⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t
begin
sublocale l_put_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_lemmas by unfold_locales

interpretation l_put_M type_wf document_ptr_kinds get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t
  apply(unfold_locales)
   apply (simp add: get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_type_wf local.type_wf⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t)
  by (meson DocumentMonad.get_M_is_l_get_M l_get_M_def)
lemmas put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ok = put_M_ok[folded put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def]
end

global_interpretation l_put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_lemmas type_wf by unfold_locales


lemma document_put_get [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
     ⟹ (⋀x. getter (setter (λ_. v) x) = v) 
     ⟹ h' ⊢ get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr getter →⇩r v"
  by(auto simp add: put_M_defs get_M_defs split: option.splits)
lemma get_M_Mdocument_preserved1 [simp]: 
  "document_ptr ≠ document_ptr' 
    ⟹ h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
    ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr' getter) h h'"
  by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)
lemma document_put_get_preserved [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
   ⟹ (⋀x. getter (setter (λ_. v) x) = getter x) 
   ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr' getter) h h'"
  apply(cases "document_ptr = document_ptr'") 
  by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mdocument_preserved2 [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' ⟹ preserved (get_M⇩N⇩o⇩d⇩e node_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs NodeMonad.get_M_defs get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def 
      put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def get⇩N⇩o⇩d⇩e_def preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mdocument_preserved3 [simp]: 
  "cast document_ptr ≠ object_ptr 
   ⟹ h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
   ⟹ preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def ObjectMonad.get_M_defs 
      preserved_def split: option.splits dest: get_heap_E)
lemma get_M_Mdocument_preserved4  [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
   ⟹ (⋀x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
   ⟹ preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr getter) h h'"
  apply(cases "cast document_ptr ≠ object_ptr")[1]
  by(auto simp add: put_M_defs get_M_defs get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def 
      ObjectMonad.get_M_defs preserved_def 
      split: option.splits bind_splits dest: get_heap_E)

lemma get_M_Mdocument_preserved5 [simp]: 
  "cast document_ptr ≠ object_ptr 
  ⟹ h ⊢ put_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr setter v →⇩h h' 
  ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr getter) h h'"
  by(auto simp add: ObjectMonad.put_M_defs get_M_defs get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def ObjectMonad.get_M_defs 
      preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mdocument_preserved6 [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' ⟹ preserved (get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t element_ptr getter) h h'"
  by(auto simp add: put_M_defs ElementMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma get_M_Mdocument_preserved7 [simp]: 
  "h ⊢ put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t element_ptr setter v →⇩h h' ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr getter) h h'"
  by(auto simp add: ElementMonad.put_M_defs get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma get_M_Mdocument_preserved8 [simp]: 
  "h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' 
    ⟹ preserved (get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a character_data_ptr getter) h h'"
  by(auto simp add: put_M_defs CharacterDataMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma get_M_Mdocument_preserved9 [simp]: 
  "h ⊢ put_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a character_data_ptr setter v →⇩h h' 
    ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr getter) h h'"
  by(auto simp add: CharacterDataMonad.put_M_defs get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma get_M_Mdocument_preserved10 [simp]: 
  "(⋀x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
    ⟹ h ⊢ put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr setter v →⇩h h' ⟹ preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr getter) h h'"
  apply(cases "cast document_ptr = object_ptr") 
  by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def 
      get⇩N⇩o⇩d⇩e_def preserved_def put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def bind_eq_Some_conv 
      split: option.splits)

lemma new_element_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t: 
  "h ⊢ new_element →⇩h h' ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t ptr getter) h h'"
  by(auto simp add: new_element_def get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_character_data_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t: 
  "h ⊢ new_character_data →⇩h h' ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t ptr getter) h h'"
  by(auto simp add: new_character_data_def get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)


subsection ‹Creating Documents›

definition new_document :: "(_, (_) document_ptr) dom_prog"
  where
    "new_document = do {
      h ← get_heap;
      (new_ptr, h') ← return (new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t h);
      return_heap h';
      return new_ptr
    }"

lemma new_document_ok [simp]:
  "h ⊢ ok new_document"
  by(auto simp add: new_document_def split: prod.splits)

lemma new_document_ptr_in_heap:
  assumes "h ⊢ new_document →⇩h h'"
    and "h ⊢ new_document →⇩r new_document_ptr"
  shows "new_document_ptr |∈| document_ptr_kinds h'"
  using assms
  unfolding new_document_def
  by(auto simp add: new_document_def new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def Let_def put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ptr_in_heap is_OK_returns_result_I
      elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_document_ptr_not_in_heap:
  assumes "h ⊢ new_document →⇩h h'"
    and "h ⊢ new_document →⇩r new_document_ptr"
  shows "new_document_ptr |∉| document_ptr_kinds h"
  using assms new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_ptr_not_in_heap
  by(auto simp add: new_document_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_document_new_ptr:
  assumes "h ⊢ new_document →⇩h h'"
    and "h ⊢ new_document →⇩r new_document_ptr"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_document_ptr|}"
  using assms new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_new_ptr
  by(auto simp add: new_document_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_document_is_document_ptr:
  assumes "h ⊢ new_document →⇩r new_document_ptr"
  shows "is_document_ptr new_document_ptr"
  using assms new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_is_document_ptr
  by(auto simp add: new_document_def elim!: bind_returns_result_E split: prod.splits)

lemma new_document_doctype:
  assumes "h ⊢ new_document →⇩h h'"
  assumes "h ⊢ new_document →⇩r new_document_ptr"
  shows "h' ⊢ get_M new_document_ptr doctype →⇩r ''''"
  using assms
  by(auto simp add: get_M_defs new_document_def new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_document_document_element:
  assumes "h ⊢ new_document →⇩h h'"
  assumes "h ⊢ new_document →⇩r new_document_ptr"
  shows "h' ⊢ get_M new_document_ptr document_element →⇩r None"
  using assms
  by(auto simp add: get_M_defs new_document_def new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_document_disconnected_nodes:
  assumes "h ⊢ new_document →⇩h h'"
  assumes "h ⊢ new_document →⇩r new_document_ptr"
  shows "h' ⊢ get_M new_document_ptr disconnected_nodes →⇩r []"
  using assms
  by(auto simp add: get_M_defs new_document_def new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)


lemma new_document_get_M⇩O⇩b⇩j⇩e⇩c⇩t: 
  "h ⊢ new_document →⇩h h' ⟹ h ⊢ new_document →⇩r new_document_ptr 
    ⟹ ptr ≠ cast new_document_ptr ⟹ preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t ptr getter) h h'"
  by(auto simp add: new_document_def ObjectMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_document_get_M⇩N⇩o⇩d⇩e: 
  "h ⊢ new_document →⇩h h' ⟹ h ⊢ new_document →⇩r new_document_ptr 
    ⟹ preserved (get_M⇩N⇩o⇩d⇩e ptr getter) h h'"
  by(auto simp add: new_document_def NodeMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_document_get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t: 
  "h ⊢ new_document →⇩h h' ⟹ h ⊢ new_document →⇩r new_document_ptr 
     ⟹ preserved (get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t ptr getter) h h'"
  by(auto simp add: new_document_def ElementMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_document_get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a: 
  "h ⊢ new_document →⇩h h' ⟹ h ⊢ new_document →⇩r new_document_ptr 
    ⟹ preserved (get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a ptr getter) h h'"
  by(auto simp add: new_document_def CharacterDataMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_document_get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t: 
  "h ⊢ new_document →⇩h h' 
     ⟹ h ⊢ new_document →⇩r new_document_ptr ⟹ ptr ≠ new_document_ptr 
     ⟹ preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t ptr getter) h h'"
  by(auto simp add: new_document_def get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)



subsection ‹Modified Heaps›

lemma get_document_ptr_simp [simp]: 
  "get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h) 
     = (if ptr = cast document_ptr then cast obj else get document_ptr h)"
  by(auto simp add: get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def split: option.splits Option.bind_splits)

lemma document_ptr_kidns_simp [simp]: 
  "document_ptr_kinds (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h) 
    = document_ptr_kinds h |∪| (if is_document_ptr_kind ptr then {|the (cast ptr)|} else {||})"
  by(auto simp add: document_ptr_kinds_def split: option.splits)

lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "CharacterDataClass.type_wf (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h)"
  assumes "is_document_ptr_kind ptr ⟹ is_document_kind obj"
  shows "type_wf (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h)"
  using assms
  by(auto simp add: type_wf_defs is_document_kind_def split: option.splits)

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by(auto simp add: type_wf_defs elim!: CharacterDataMonad.type_wf_put_ptr_not_in_heap_E 
      split: option.splits if_splits)

lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (put⇩O⇩b⇩j⇩e⇩c⇩t ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "CharacterDataClass.type_wf h"
  assumes "is_document_ptr_kind ptr ⟹ is_document_kind (the (get ptr h))"
  shows "type_wf h"
  using assms
  apply(auto simp add: type_wf_defs elim!: CharacterDataMonad.type_wf_put_ptr_in_heap_E 
      split: option.splits if_splits)[1]
  by (metis (no_types, opaque_lifting) CharacterDataClass.get⇩O⇩b⇩j⇩e⇩c⇩t_type_wf bind.bind_lunit get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def
      is_document_kind_def option.exhaust_sel)



subsection ‹Preserving Types›

lemma new_element_type_wf_preserved [simp]: 
  "h ⊢ new_element →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: new_element_def new⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def Let_def put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def element_ptrs_def
      elim!: bind_returns_heap_E type_wf_put_ptr_not_in_heap_E 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I 
      split: if_splits)[1]
   apply force
  by (metis Suc_n_not_le_n element_ptr.sel(1) element_ptrs_def fMax_ge ffmember_filter 
      fimage_eqI is_element_ptr_ref)

lemma new_element_is_l_new_element [instances]: 
  "l_new_element type_wf"
  using l_new_element.intro new_element_type_wf_preserved
  by blast

lemma put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_tag_name_type_wf_preserved [simp]:
  "h ⊢ put_M element_ptr tag_name_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: ElementMonad.put_M_defs put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def
      dest!: get_heap_E  
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs NodeClass.type_wf_defs
      ElementMonad.get_M_defs ObjectClass.type_wf_defs
      CharacterDataClass.type_wf_defs split: option.splits)[1]
   apply (metis bind.bind_lzero get⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def option.collapse option.simps(3))
  by metis

lemma put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_child_nodes_type_wf_preserved [simp]: 
  "h ⊢ put_M element_ptr child_nodes_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: ElementMonad.put_M_defs put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def
      dest!: get_heap_E
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
   apply (metis bind.bind_lzero get⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def option.collapse option.simps(3))
  by metis

lemma put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_attrs_type_wf_preserved [simp]: 
  "h ⊢ put_M element_ptr attrs_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: ElementMonad.put_M_defs put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def
      dest!: get_heap_E
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
   apply (metis bind.bind_lzero get⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def option.collapse option.simps(3))
  by metis

lemma put_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t_shadow_root_opt_type_wf_preserved [simp]:
  "h ⊢ put_M element_ptr shadow_root_opt_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: ElementMonad.put_M_defs put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def
      dest!: get_heap_E
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
   apply (metis bind.bind_lzero get⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def option.collapse option.simps(3))
  by metis

lemma new_character_data_type_wf_preserved [simp]: 
  "h ⊢ new_character_data →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: ElementMonad.put_M_defs put⇩E⇩l⇩e⇩m⇩e⇩n⇩t_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_kind_def
      new_character_data_def new⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_def Let_def put⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_def put⇩N⇩o⇩d⇩e_def
      dest!: get_heap_E
      elim!: bind_returns_heap_E2 bind_returns_heap_E type_wf_put_ptr_not_in_heap_E
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  by (meson new⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_def new⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_ptr_not_in_heap)

lemma new_character_data_is_l_new_character_data [instances]: 
  "l_new_character_data type_wf"
  using l_new_character_data.intro new_character_data_type_wf_preserved
  by blast

lemma put_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_val_type_wf_preserved [simp]: 
  "h ⊢ put_M character_data_ptr val_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: CharacterDataMonad.put_M_defs put⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_def put⇩N⇩o⇩d⇩e_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t is_node_kind_def
      dest!: get_heap_E  elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: is_node_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs CharacterDataMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
  apply (metis bind.bind_lzero get⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a_def option.distinct(1) option.exhaust_sel)
  by metis


lemma new_document_type_wf_preserved [simp]: "h ⊢ new_document →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: new_document_def new⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def Let_def put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a  DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_ptr_kind_none
      elim!: bind_returns_heap_E type_wf_put_ptr_not_in_heap_E 
      intro!: type_wf_put_I ElementMonad.type_wf_put_I CharacterDataMonad.type_wf_put_I 
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I 
      split: if_splits)[1] 
   apply(auto simp add: type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs 
      NodeClass.type_wf_defs ObjectClass.type_wf_defs is_document_kind_def 
      split: option.splits)[1]
  using document_ptrs_def apply force
   apply (simp add: is_document_kind_def)
  apply (metis Suc_n_not_le_n document_ptr.sel(1) document_ptrs_def fMax_ge ffmember_filter
      fimage_eqI is_document_ptr_ref)
  done

locale l_new_document = l_type_wf +
  assumes new_document_types_preserved: "h ⊢ new_document →⇩h h' ⟹ type_wf h = type_wf h'"

lemma new_document_is_l_new_document  [instances]: "l_new_document type_wf"
  using l_new_document.intro new_document_type_wf_preserved
  by blast

lemma put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_doctype_type_wf_preserved [simp]: 
  "h ⊢ put_M document_ptr doctype_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: put_M_defs put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def dest!: get_heap_E  
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I 
      ElementMonad.type_wf_put_I NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I)[1]
         apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
        apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
       apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
      apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
     apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
    apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
   apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
  apply(auto simp add: is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
  apply(auto simp add: get_M_defs)[1]
  by (metis (mono_tags) error_returns_result option.exhaust_sel option.simps(4))

lemma put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_document_element_type_wf_preserved [simp]: 
  "h ⊢ put_M document_ptr document_element_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: put_M_defs put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def 
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a
      DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e
      DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t is_node_ptr_kind_none
      cast⇩O⇩b⇩j⇩e⇩c⇩t⇩2⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_none is_document_kind_def
      dest!: get_heap_E  
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I 
      ElementMonad.type_wf_put_I NodeMonad.type_wf_put_I 
      ObjectMonad.type_wf_put_I)[1]
  apply(auto simp add: get_M_defs is_document_kind_def type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs 
      split: option.splits)[1]
  by metis

lemma put_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_disconnected_nodes_type_wf_preserved [simp]: 
  "h ⊢ put_M document_ptr disconnected_nodes_update v →⇩h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: put_M_defs put⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def
      DocumentClass.type_wf⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a
      DocumentClass.type_wf⇩E⇩l⇩e⇩m⇩e⇩n⇩t
      DocumentClass.type_wf⇩N⇩o⇩d⇩e
      DocumentClass.type_wf⇩O⇩b⇩j⇩e⇩c⇩t
      is_node_ptr_kind_none
      cast⇩O⇩b⇩j⇩e⇩c⇩t⇩2⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_none is_document_kind_def
      dest!: get_heap_E  
      elim!: bind_returns_heap_E2 
      intro!: type_wf_put_I CharacterDataMonad.type_wf_put_I 
      ElementMonad.type_wf_put_I NodeMonad.type_wf_put_I
      ObjectMonad.type_wf_put_I)[1] 
  apply(auto simp add: is_document_kind_def get_M_defs type_wf_defs ElementClass.type_wf_defs 
      NodeClass.type_wf_defs ElementMonad.get_M_defs ObjectClass.type_wf_defs 
      CharacterDataClass.type_wf_defs split: option.splits)[1]
  by metis

lemma document_ptr_kinds_small:
  assumes "⋀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h'"
  shows "document_ptr_kinds h = document_ptr_kinds h'"
  by(simp add: document_ptr_kinds_def preserved_def object_ptr_kinds_preserved_small[OF assms])

lemma document_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h ⊢ setter →⇩h h'"
  assumes "⋀h h'. ∀w ∈ SW. h ⊢ w →⇩h h' 
           ⟶ (∀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h')"
  shows "document_ptr_kinds h = document_ptr_kinds h'"
  using writes_small_big[OF assms]
  apply(simp add: reflp_def transp_def preserved_def document_ptr_kinds_def)
  by (metis assms object_ptr_kinds_preserved)

lemma type_wf_preserved_small:
  assumes "⋀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h'"
  assumes "⋀node_ptr. preserved (get_M⇩N⇩o⇩d⇩e node_ptr RNode.nothing) h h'"
  assumes "⋀element_ptr. preserved (get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t element_ptr RElement.nothing) h h'"
  assumes "⋀character_data_ptr. preserved 
                          (get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a character_data_ptr RCharacterData.nothing) h h'"
  assumes "⋀document_ptr. preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr RDocument.nothing) h h'"
  shows "DocumentClass.type_wf h = DocumentClass.type_wf h'"
  using type_wf_preserved_small[OF assms(1) assms(2) assms(3) assms(4)]  
    allI[OF assms(5), of id, simplified] document_ptr_kinds_small[OF assms(1)]
  apply(auto simp add: type_wf_defs )[1]
   apply(auto simp add: type_wf_defs preserved_def get_M_defs document_ptr_kinds_small[OF assms(1)] 
      split: option.splits)[1]
   apply force
  apply(auto simp add: type_wf_defs preserved_def get_M_defs document_ptr_kinds_small[OF assms(1)] 
      split: option.splits)[1]
  by force

lemma type_wf_preserved:
  assumes "writes SW setter h h'"
  assumes "h ⊢ setter →⇩h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' 
          ⟹ ∀object_ptr. preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t object_ptr RObject.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' 
          ⟹ ∀node_ptr. preserved (get_M⇩N⇩o⇩d⇩e node_ptr RNode.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' 
          ⟹ ∀element_ptr. preserved (get_M⇩E⇩l⇩e⇩m⇩e⇩n⇩t element_ptr RElement.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' 
          ⟹ ∀character_data_ptr. preserved 
                    (get_M⇩C⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩D⇩a⇩t⇩a character_data_ptr RCharacterData.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' 
          ⟹ ∀document_ptr. preserved (get_M⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t document_ptr RDocument.nothing) h h'"
  shows "DocumentClass.type_wf h = DocumentClass.type_wf h'"
proof -
  have "⋀h h' w. w ∈ SW ⟹ h ⊢ w →⇩h h' ⟹ DocumentClass.type_wf h = DocumentClass.type_wf h'"
    using assms type_wf_preserved_small by fast
  with assms(1) assms(2) show ?thesis
    apply(rule writes_small_big)
    by(auto simp add: reflp_def transp_def)
qed

lemma type_wf_drop: "type_wf h ⟹ type_wf (Heap (fmdrop ptr (the_heap h)))"
  apply(auto simp add: type_wf_defs)[1]
  using type_wf_drop
   apply blast
  by (metis (no_types, opaque_lifting) CharacterDataClass.get⇩O⇩b⇩j⇩e⇩c⇩t_type_wf CharacterDataMonad.type_wf_drop
      document_ptr_kinds_commutes fmlookup_drop get⇩D⇩o⇩c⇩u⇩m⇩e⇩n⇩t_def get⇩O⇩b⇩j⇩e⇩c⇩t_def heap.sel)
end