Theory ShadowRootMonad

(***********************************************************************************
 * Copyright (c) 2016-2020 The University of Sheffield, UK
 *               2019-2020 University of Exeter, 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‹Shadow Root Monad›
theory ShadowRootMonad
  imports
    "Core_SC_DOM.DocumentMonad"
    "../classes/ShadowRootClass"
begin


type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
    'shadow_root_ptr, 'Object, 'Node, 'Element, 'CharacterData, 'Document, 'ShadowRoot, '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, 'ShadowRoot, 'result) dom_prog"



global_interpretation l_ptr_kinds_M shadow_root_ptr_kinds defines shadow_root_ptr_kinds_M = a_ptr_kinds_M .
lemmas shadow_root_ptr_kinds_M_defs = a_ptr_kinds_M_def

lemma shadow_root_ptr_kinds_M_eq:
  assumes "|h ⊢ object_ptr_kinds_M|r = |h' ⊢ object_ptr_kinds_M|r"
  shows "|h ⊢ shadow_root_ptr_kinds_M|r = |h' ⊢ shadow_root_ptr_kinds_M|r"
  using assms
  by(auto simp add: shadow_root_ptr_kinds_M_defs document_ptr_kinds_def object_ptr_kinds_M_defs
      shadow_root_ptr_kinds_def)



global_interpretation l_dummy defines get_MShadowRoot = "l_get_M.a_get_M getShadowRoot" .
lemma get_M_is_l_get_M: "l_get_M getShadowRoot type_wf shadow_root_ptr_kinds"
proof -
  have "∀ptr h. (∃y. get ptr h = Some y) ⟶ ptr |∈| shadow_root_ptr_kinds h"
  apply(auto simp add: getShadowRoot_def shadow_root_ptr_kinds_def bind_eq_Some_conv image_iff Bex_def)
  by (metis (no_types, opaque_lifting) DocumentMonad.l_get_M_axioms is_shadow_root_ptr_kind_cast l_get_M_def
      option.sel option.simps(3) shadow_root_ptr_casts_commute2)
  thus ?thesis
    by (simp add: getShadowRoot_type_wf l_get_M_def)
qed

lemmas get_M_defs = get_MShadowRoot_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_MShadowRoot

locale l_get_MShadowRoot_lemmas = l_type_wfShadowRoot
begin
sublocale l_get_MCharacterData_lemmas by unfold_locales

interpretation l_get_M getShadowRoot type_wf shadow_root_ptr_kinds
  apply(unfold_locales)
   apply (simp add: getShadowRoot_type_wf local.type_wfShadowRoot)
  by (meson ShadowRootMonad.get_M_is_l_get_M l_get_M_def)
lemmas get_MShadowRoot_ok = get_M_ok[folded get_MShadowRoot_def]
lemmas get_MShadowRoot_ptr_in_heap = get_M_ptr_in_heap[folded get_MShadowRoot_def]
end

global_interpretation l_get_MShadowRoot_lemmas type_wf by unfold_locales


global_interpretation l_put_M type_wf shadow_root_ptr_kinds getShadowRoot putShadowRoot rewrites
  "a_get_M = get_MShadowRoot" defines put_MShadowRoot = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_MShadowRoot_def)

lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_MShadowRoot


locale l_put_MShadowRoot_lemmas = l_type_wfShadowRoot
begin
sublocale l_put_MCharacterData_lemmas by unfold_locales

interpretation l_put_M type_wf shadow_root_ptr_kinds getShadowRoot putShadowRoot
  apply(unfold_locales)
   apply (simp add: getShadowRoot_type_wf local.type_wfShadowRoot)
  by (meson ShadowRootMonad.get_M_is_l_get_M l_get_M_def)
lemmas put_MShadowRoot_ok = put_M_ok[folded put_MShadowRoot_def]
end

global_interpretation l_put_MShadowRoot_lemmas type_wf by unfold_locales


lemma shadow_root_put_get [simp]: "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
  ⟹ (⋀x. getter (setter (λ_. v) x) = v)
  ⟹ h' ⊢ get_MShadowRoot shadow_root_ptr getter →r v"
  by(auto simp add: put_M_defs get_M_defs split: option.splits)
lemma get_M_Mshadow_root_preserved1 [simp]:
  "shadow_root_ptr ≠ shadow_root_ptr'
    ⟹ h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
    ⟹ preserved (get_MShadowRoot shadow_root_ptr' getter) h h'"
  by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)
lemma shadow_root_put_get_preserved [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ (⋀x. getter (setter (λ_. v) x) = getter x)
   ⟹ preserved (get_MShadowRoot shadow_root_ptr' getter) h h'"
  apply(cases "shadow_root_ptr = shadow_root_ptr'")
  by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved2 [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h' ⟹ preserved (get_MNode node_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs NodeMonad.get_M_defs
      putShadowRoot_def putDocument_def getNode_def preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved3 [simp]:
  "cast shadow_root_ptr ≠ document_ptr
   ⟹ h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ preserved (get_MDocument document_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs putShadowRoot_def putDocument_def DocumentMonad.get_M_defs
      preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved4  [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ (⋀x. getter (cast (setter (λ_. v) x)) = getter (cast x))
   ⟹ preserved (get_MDocument document_ptr getter) h h'"
  apply(cases "cast shadow_root_ptr ≠ document_ptr")[1]
  by(auto simp add: put_M_defs get_M_defs getShadowRoot_def putShadowRoot_def getDocument_def putDocument_def
      DocumentMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved3a [simp]:
  "cast shadow_root_ptr ≠ object_ptr
   ⟹ h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ preserved (get_MObject object_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs putShadowRoot_def putDocument_def ObjectMonad.get_M_defs
      preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved4a  [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ (⋀x. getter (cast (setter (λ_. v) x)) = getter (cast x))
   ⟹ preserved (get_MObject object_ptr getter) h h'"
  apply(cases "cast shadow_root_ptr ≠ object_ptr")[1]
  by(auto simp add: put_M_defs get_M_defs getShadowRoot_def putShadowRoot_def getDocument_def putDocument_def
      ObjectMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved5 [simp]:
  "cast shadow_root_ptr ≠ object_ptr
  ⟹ h ⊢ put_MObject object_ptr setter v →h h'
  ⟹ preserved (get_MShadowRoot shadow_root_ptr getter) h h'"
  by(auto simp add: ObjectMonad.put_M_defs get_M_defs getShadowRoot_def ObjectMonad.get_M_defs
      preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved6 [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h' ⟹ preserved (get_MElement 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_Mshadow_root_preserved7 [simp]:
  "h ⊢ put_MElement element_ptr setter v →h h' ⟹ preserved (get_MShadowRoot shadow_root_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_Mshadow_root_preserved8 [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
    ⟹ preserved (get_MCharacterData 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_Mshadow_root_preserved9 [simp]:
  "h ⊢ put_MCharacterData character_data_ptr setter v →h h'
    ⟹ preserved (get_MShadowRoot shadow_root_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_shadow_root_put_M_document_different_pointers [simp]:
  "cast shadow_root_ptr ≠ document_ptr
    ⟹ h ⊢ put_MDocument document_ptr setter v →h h'
    ⟹ preserved (get_MShadowRoot shadow_root_ptr getter) h h'"
  by(auto simp add: DocumentMonad.put_M_defs get_M_defs DocumentMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)
lemma get_M_shadow_root_put_M_document [simp]:
  "h ⊢ put_MDocument document_ptr setter v →h h'
   ⟹ (⋀x. is_shadow_root_kind x ⟷ is_shadow_root_kind (setter (λ_. v) x))
   ⟹ (⋀x. getter (the (cast (((setter (λ_. v) (cast x)))))) = getter ((x)))
   ⟹ preserved (get_MShadowRoot shadow_root_ptr getter) h h'"
  apply(cases "cast shadow_root_ptr ≠ document_ptr ")
   apply(auto simp add: preserved_def is_shadow_root_kind_def DocumentMonad.put_M_defs
      getShadowRoot_def get_M_defs DocumentMonad.get_M_defs split: option.splits)[1]
  apply(auto simp add: preserved_def is_shadow_root_kind_def DocumentMonad.put_M_defs
      getShadowRoot_def get_M_defs DocumentMonad.get_M_defs split: option.splits)[1]
   apply(metis castDocument2ShadowRoot_inv option.sel)
  apply(metis castDocument2ShadowRoot_inv option.sel)
  done

lemma get_M_document_put_M_shadow_root_different_pointers [simp]:
  "document_ptr ≠ cast shadow_root_ptr
    ⟹ h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
    ⟹ preserved (get_MDocument document_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs DocumentMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)
lemma get_M_document_put_M_shadow_root [simp]:
  "h ⊢ put_MShadowRoot shadow_root_ptr setter v →h h'
   ⟹ (⋀x. is_shadow_root_kind x ⟹  getter ((cast (((setter (λ_. v) (the (cast x))))))) = getter ((x)))
   ⟹ preserved (get_MDocument document_ptr getter) h h'"
  apply(cases "document_ptr ≠ cast shadow_root_ptr ")
   apply(auto simp add: preserved_def is_document_kind_def putDocument_def putShadowRoot_def put_M_defs
      getDocument_def getShadowRoot_def DocumentMonad.get_M_defs ShadowRootMonad.get_M_defs
      split: option.splits Option.bind_splits)[1]
  apply(auto simp add: preserved_def is_document_kind_def putDocument_def putShadowRoot_def put_M_defs
      getDocument_def getShadowRoot_def DocumentMonad.get_M_defs ShadowRootMonad.get_M_defs
      split: option.splits Option.bind_splits)[1]
  using is_shadow_root_kindDocument_def apply force
  by (metis castDocument2ShadowRoot_inv is_shadow_root_kindDocument_def option.distinct(1) option.sel)

lemma cast_shadow_root_child_nodes_document_disconnected_nodes [simp]:
  "RShadowRoot.child_nodes (the (cast (cast x⦇disconnected_nodes := y⦈))) = RShadowRoot.child_nodes x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject
      RShadowRoot.surjective)
lemma cast_shadow_root_child_nodes_document_doctype [simp]:
  "RShadowRoot.child_nodes (the (cast (cast x⦇doctype := y⦈))) = RShadowRoot.child_nodes x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject RShadowRoot.surjective)
lemma cast_shadow_root_child_nodes_document_document_element [simp]:
  "RShadowRoot.child_nodes (the (cast (cast x⦇document_element := y⦈))) = RShadowRoot.child_nodes x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject
      RShadowRoot.surjective)

lemma cast_shadow_root_mode_document_disconnected_nodes [simp]:
  "RShadowRoot.mode (the (cast (cast x⦇disconnected_nodes := y⦈))) = RShadowRoot.mode x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def
      RDocument.truncate_def split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject
      RShadowRoot.surjective)
lemma cast_shadow_root_mode_document_doctype [simp]:
  "RShadowRoot.mode (the (cast (cast x⦇doctype := y⦈))) = RShadowRoot.mode x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject RShadowRoot.surjective)
lemma cast_shadow_root_mode_document_document_element [simp]:
  "RShadowRoot.mode (the (cast (cast x⦇document_element := y⦈))) = RShadowRoot.mode x"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits)[1]
  by (metis RDocument.ext_inject RDocument.surjective RObject.ext_inject RShadowRoot.ext_inject RShadowRoot.surjective)

lemma cast_document_disconnected_nodes_shadow_root_child_nodes [simp]:
  "is_shadow_root_kind x ⟹
disconnected_nodes (cast (the (cast x)⦇RShadowRoot.child_nodes := arg⦈)) = disconnected_nodes x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)
lemma cast_document_doctype_shadow_root_child_nodes [simp]:
  "is_shadow_root_kind x ⟹ doctype (cast (the (cast x)⦇RShadowRoot.child_nodes := arg⦈)) = doctype x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)
lemma cast_document_document_element_shadow_root_child_nodes [simp]:
  "is_shadow_root_kind x ⟹
document_element (cast (the (cast x)⦇RShadowRoot.child_nodes := arg⦈)) = document_element x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)
lemma cast_document_disconnected_nodes_shadow_root_mode [simp]:
  "is_shadow_root_kind x ⟹
disconnected_nodes (cast (the (cast x)⦇RShadowRoot.mode := arg⦈)) = disconnected_nodes x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)
lemma cast_document_doctype_shadow_root_mode [simp]:
  "is_shadow_root_kind x ⟹
doctype (cast (the (cast x)⦇RShadowRoot.mode := arg⦈)) = doctype x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)
lemma cast_document_document_element_shadow_root_mode [simp]:
  "is_shadow_root_kind x ⟹
document_element (cast (the (cast x)⦇RShadowRoot.mode := arg⦈)) = document_element x"
  by(auto simp add: is_shadow_root_kind_def castDocument2ShadowRoot_def castShadowRoot2Document_def
      RDocument.extend_def RDocument.truncate_def split: option.splits sum.splits)


lemma new_element_get_MShadowRoot:
  "h ⊢ new_element →h h' ⟹ preserved (get_MShadowRoot 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_MShadowRoot:
  "h ⊢ new_character_data →h h' ⟹ preserved (get_MShadowRoot 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)

lemma new_document_get_MShadowRoot:
  "h ⊢ new_document →r new_document_ptr ⟹ h ⊢ new_document →h h'
    ⟹ cast ptr ≠ new_document_ptr ⟹ preserved (get_MShadowRoot 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)


definition deleteShadowRoot_M :: "(_) shadow_root_ptr ⇒ (_, unit) dom_prog" where
  "deleteShadowRoot_M shadow_root_ptr = do {
    h ← get_heap;
    (case deleteShadowRoot shadow_root_ptr h of
      Some h ⇒ return_heap h |
      None ⇒ error HierarchyRequestError)
  }"
adhoc_overloading delete_M deleteShadowRoot_M

lemma deleteShadowRoot_M_ok [simp]:
  assumes "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  shows "h ⊢ ok (deleteShadowRoot_M shadow_root_ptr)"
  using assms
  by(auto simp add: deleteShadowRoot_M_def deleteShadowRoot_def deleteObject_def split: prod.splits)

lemma deleteShadowRoot_M_ptr_in_heap:
  assumes "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h'"
  shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  using assms
  by(auto simp add: deleteShadowRoot_M_def deleteShadowRoot_def deleteObject_def split: if_splits)

lemma deleteShadowRoot_M_ptr_not_in_heap:
  assumes "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h'"
  shows "shadow_root_ptr |∉| shadow_root_ptr_kinds h'"
  using assms
  by(auto simp add: deleteShadowRoot_M_def deleteShadowRoot_def deleteObject_def shadow_root_ptr_kinds_def
      document_ptr_kinds_def object_ptr_kinds_def split: if_splits)

lemma delete_shadow_root_pointers:
  assumes "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h' |∪| {|cast shadow_root_ptr|}"
  using assms
  by(auto simp add: deleteShadowRoot_M_def deleteShadowRoot_def deleteObject_def shadow_root_ptr_kinds_def
      document_ptr_kinds_def object_ptr_kinds_def split: if_splits)

lemma delete_shadow_root_get_MObject:
  "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ ptr ≠ cast shadow_root_ptr ⟹
preserved (get_MObject ptr getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def ObjectMonad.get_M_defs preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_MNode:
  "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ preserved (get_MNode ptr getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def NodeMonad.get_M_defs ObjectMonad.get_M_defs
      preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_MElement:
  "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ preserved (get_MElement ptr getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def ElementMonad.get_M_defs NodeMonad.get_M_defs
      ObjectMonad.get_M_defs preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_MCharacterData:
  "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ preserved (get_MCharacterData ptr getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def CharacterDataMonad.get_M_defs NodeMonad.get_M_defs
      ObjectMonad.get_M_defs preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_MDocument:
  "cast shadow_root_ptr ≠ ptr ⟹ h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ preserved (get_MDocument ptr getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def DocumentMonad.get_M_defs ObjectMonad.get_M_defs
      preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_MShadowRoot:
  "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h' ⟹ shadow_root_ptr ≠ shadow_root_ptr' ⟹ preserved (get_MShadowRoot shadow_root_ptr' getter) h h'"
  by(auto simp add: deleteShadowRoot_M_def deleteObject_def get_M_defs ObjectMonad.get_M_defs preserved_def
      split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)



subsection ‹new\_M›

definition newShadowRoot_M :: "(_, (_) shadow_root_ptr) dom_prog"
  where
    "newShadowRoot_M = do {
      h ← get_heap;
      (new_ptr, h') ← return (newShadowRoot h);
      return_heap h';
      return new_ptr
    }"

lemma newShadowRoot_M_ok [simp]:
  "h ⊢ ok newShadowRoot_M"
  by(auto simp add: newShadowRoot_M_def split: prod.splits)

lemma newShadowRoot_M_ptr_in_heap:
  assumes "h ⊢ newShadowRoot_M →h h'"
    and "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "new_shadow_root_ptr |∈| shadow_root_ptr_kinds h'"
  using assms
  unfolding newShadowRoot_M_def
  by(auto simp add: newShadowRoot_M_def newShadowRoot_def Let_def putShadowRoot_ptr_in_heap is_OK_returns_result_I
      elim!: bind_returns_result_E bind_returns_heap_E)

lemma newShadowRoot_M_ptr_not_in_heap:
  assumes "h ⊢ newShadowRoot_M →h h'"
    and "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "new_shadow_root_ptr |∉| shadow_root_ptr_kinds h"
  using assms newShadowRoot_ptr_not_in_heap
  by(auto simp add: newShadowRoot_M_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma newShadowRoot_M_new_ptr:
  assumes "h ⊢ newShadowRoot_M →h h'"
    and "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_shadow_root_ptr|}"
  using assms newShadowRoot_new_ptr
  by(auto simp add: newShadowRoot_M_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma newShadowRoot_M_is_shadow_root_ptr:
  assumes "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "is_shadow_root_ptr new_shadow_root_ptr"
  using assms newShadowRoot_is_shadow_root_ptr
  by(auto simp add: newShadowRoot_M_def elim!: bind_returns_result_E split: prod.splits)

lemma new_shadow_root_mode:
  assumes "h ⊢ newShadowRoot_M →h h'"
  assumes "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "h' ⊢ get_M new_shadow_root_ptr mode →r Open"
  using assms
  by(auto simp add: get_M_defs newShadowRoot_M_def newShadowRoot_def Let_def
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_shadow_root_children:
  assumes "h ⊢ newShadowRoot_M →h h'"
  assumes "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "h' ⊢ get_M new_shadow_root_ptr child_nodes →r []"
  using assms
  by(auto simp add: get_M_defs newShadowRoot_M_def newShadowRoot_def Let_def
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_shadow_root_disconnected_nodes:
  assumes "h ⊢ newShadowRoot_M →h h'"
  assumes "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "h' ⊢ get_M (castshadow_root_ptr2document_ptr new_shadow_root_ptr) disconnected_nodes →r []"
  using assms
  by(auto simp add: DocumentMonad.get_M_defs put_M_defs putShadowRoot_def newShadowRoot_M_def newShadowRoot_def Let_def
      castshadow_root_ptr2document_ptr_def castShadowRoot2Document_def RDocument.extend_def RDocument.truncate_def
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_shadow_root_get_MObject:
  "h ⊢ newShadowRoot_M →h h' ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr
    ⟹ ptr ≠ cast new_shadow_root_ptr ⟹ preserved (get_MObject ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def ObjectMonad.get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_shadow_root_get_MNode:
  "h ⊢ newShadowRoot_M →h h' ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr
    ⟹ preserved (get_MNode ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def NodeMonad.get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_shadow_root_get_MElement:
  "h ⊢ newShadowRoot_M →h h' ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr
     ⟹ preserved (get_MElement ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def ElementMonad.get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_shadow_root_get_MCharacterData:
  "h ⊢ newShadowRoot_M →h h' ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr
    ⟹ preserved (get_MCharacterData ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def CharacterDataMonad.get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_shadow_root_get_MDocument:
  "h ⊢ newShadowRoot_M →h h'
     ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr ⟹ ptr ≠ cast new_shadow_root_ptr
     ⟹ preserved (get_MDocument ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def DocumentMonad.get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_shadow_root_get_MShadowRoot:
  "h ⊢ newShadowRoot_M →h h'
     ⟹ h ⊢ newShadowRoot_M →r new_shadow_root_ptr ⟹ ptr ≠ new_shadow_root_ptr
     ⟹ preserved (get_MShadowRoot ptr getter) h h'"
  by(auto simp add: newShadowRoot_M_def get_M_defs preserved_def
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)


subsection ‹modified heaps›

lemma shadow_root_get_put_1 [simp]: "getShadowRoot shadow_root_ptr (putObject ptr obj h) =
(if ptr = cast shadow_root_ptr then cast obj else get shadow_root_ptr h)"
  by(auto simp add: getShadowRoot_def split: option.splits Option.bind_splits)

lemma shadow_root_ptr_kinds_new [simp]: "shadow_root_ptr_kinds (putObject ptr obj h) =
shadow_root_ptr_kinds h |∪| (if is_shadow_root_ptr_kind ptr then {|the (cast ptr)|} else {||})"
  by(auto simp add: shadow_root_ptr_kinds_def is_document_ptr_kind_def split: option.splits)

lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "DocumentClass.type_wf (putObject ptr obj h)"
  assumes "is_shadow_root_ptr_kind ptr ⟹ is_shadow_root_kind obj"
  shows "type_wf (putObject ptr obj h)"
  using assms
  by(auto simp add: type_wf_defs is_shadow_root_kind_def split: option.splits)

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  by (metis (no_types, opaque_lifting) DocumentMonad.type_wf_put_ptr_not_in_heap_E ObjectClass.getObject_type_wf
      ObjectMonad.type_wf_put_ptr_not_in_heap_E ShadowRootClass.type_wfObject ShadowRootClass.type_wf_defs
      document_ptr_kinds_commutes getShadowRoot_def get_document_ptr_simp get_object_ptr_simp2
      shadow_root_ptr_kinds_commutes)


lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "DocumentClass.type_wf h"
  assumes "is_shadow_root_ptr_kind ptr ⟹ is_shadow_root_kind (the (get ptr h))"
  shows "type_wf h"
  using assms
  apply(auto simp add: type_wf_defs elim!: DocumentMonad.type_wf_put_ptr_in_heap_E
      split: option.splits if_splits)[1]
  by (metis (no_types, opaque_lifting) DocumentClass.l_getObject_lemmas_axioms assms(2) bind.bind_lunit
      castDocument2ShadowRoot_inv castObject2Document_inv getDocument_def getShadowRoot_def l_getObject_lemmas.getObject_type_wf option.collapse)


subsection ‹type\_wf›

lemma new_element_type_wf_preserved [simp]:
  assumes "h ⊢ new_element →h h'"
  shows "type_wf h = type_wf h'"
proof -
  obtain new_element_ptr where "h ⊢ new_element →r new_element_ptr"
    using assms
    by (meson is_OK_returns_heap_I is_OK_returns_result_E)
  with assms have "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
    using new_element_new_ptr by auto
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)

  with assms show ?thesis
    by(auto simp add: ElementMonad.new_element_def type_wf_defs Let_def elim!: bind_returns_heap_E
        split: prod.splits)
qed

lemma put_MElement_tag_name_type_wf_preserved [simp]:
  assumes "h ⊢ put_M element_ptr tag_name_update v →h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "object_ptr_kinds h = object_ptr_kinds h'"
    using writes_singleton assms object_ptr_kinds_preserved unfolding all_args_def by fastforce
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_MElement_child_nodes_type_wf_preserved [simp]:
  assumes "h ⊢ put_M element_ptr RElement.child_nodes_update v →h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "object_ptr_kinds h = object_ptr_kinds h'"
    using writes_singleton assms object_ptr_kinds_preserved unfolding all_args_def by fastforce
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_MElement_attrs_type_wf_preserved [simp]:
  assumes "h ⊢ put_M element_ptr attrs_update v →h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "object_ptr_kinds h = object_ptr_kinds h'"
    using writes_singleton assms object_ptr_kinds_preserved unfolding all_args_def by fastforce
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_MElement_shadow_root_opt_type_wf_preserved [simp]:
  assumes "h ⊢ put_M element_ptr shadow_root_opt_update v →h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "object_ptr_kinds h = object_ptr_kinds h'"
    using writes_singleton assms object_ptr_kinds_preserved unfolding all_args_def by fastforce
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed

lemma new_character_data_type_wf_preserved [simp]:
  assumes "h ⊢ new_character_data →h h'"
  shows "type_wf h = type_wf h'"
proof -
  obtain new_character_data_ptr where "h ⊢ new_character_data →r new_character_data_ptr"
    using assms
    by (meson is_OK_returns_heap_I is_OK_returns_result_E)
  with assms have "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
    using new_character_data_new_ptr by auto
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: CharacterDataMonad.new_character_data_def type_wf_defs Let_def
        elim!: bind_returns_heap_E split: prod.splits)
qed
lemma put_MCharacterData_val_type_wf_preserved [simp]:
  assumes "h ⊢ put_M character_data_ptr val_update v →h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "object_ptr_kinds h = object_ptr_kinds h'"
    using writes_singleton assms object_ptr_kinds_preserved unfolding all_args_def by fastforce
  then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
    by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)
  with assms show ?thesis
    by(auto simp add: CharacterDataMonad.put_M_defs type_wf_defs)
qed

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 newDocument_def Let_def putDocument_def
      type_wfDocument
      type_wfCharacterData  type_wfElement
      type_wfNode type_wfObject
      is_node_ptr_kind_none
      elim!: bind_returns_heap_E type_wf_put_ptr_not_in_heap_E
      intro!: type_wf_put_I DocumentMonad.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]
    apply (metis fMax_finsert fimage_is_fempty newDocument_def newDocument_ptr_not_in_heap)
   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]
  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

lemma put_MDocument_doctype_type_wf_preserved [simp]:
  "h ⊢ put_MDocument document_ptr doctype_update v →h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: DocumentMonad.put_M_defs putDocument_def dest!: get_heap_E
      elim!: bind_returns_heap_E2
      intro!: type_wf_put_I DocumentMonad.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 DocumentClass.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 DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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]
proof -
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇doctype := v⦈)) h"
    and 2: "ShadowRootClass.type_wf h"
    and 3: "is_shadow_root_ptr_kind document_ptr"
  obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr" and
    "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
    by (metis "0" "3" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I
        is_shadow_root_ptr_kind_obtains shadow_root_ptr_kinds_commutes)

  then have "is_shadow_root_kind x"
    using 0 2
    apply(auto simp add: is_document_kind_def type_wf_defs is_shadow_root_kind_def getShadowRoot_def
        split: option.splits Option.bind_splits)[1]
    by (metis (no_types, lifting) DocumentMonad.get_M_defs get_heap_returns_result
        id_apply option.simps(5) return_returns_result)


  then show "∃y. cast y = x⦇doctype := v⦈"
    using castDocument2ShadowRoot_none is_shadow_root_kind_doctype is_shadow_root_kindDocument_def by blast
next
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇doctype := v⦈)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (x⦇doctype := v⦈)) h)"
  have 3: "⋀document_ptr'. document_ptr' ≠ document_ptr ⟹ getObject (cast document_ptr') h = getObject (cast document_ptr') h'"
    by (simp add: "1")
  have "document_ptr |∈| document_ptr_kinds h"
    by (meson "0" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I)
  show "ShadowRootClass.type_wf h"
  proof (cases "is_shadow_root_ptr_kind document_ptr")
    case True
    then obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr"
      using is_shadow_root_ptr_kind_obtains by blast
    then
    have "is_shadow_root_kind (x⦇doctype := v⦈)"
      using 2 True
      by(simp add: type_wf_defs is_shadow_root_kindDocument_def split: if_splits option.splits)
    then
    have "is_shadow_root_kind x"
      using is_shadow_root_kind_doctype by blast
    then
    have "is_shadow_root_kind (the (getObject (cast document_ptr) h))"
      using 0
      by(auto simp add: DocumentMonad.a_get_M_def getDocument_def getObject_def is_shadow_root_kind_def
          split: option.splits Option.bind_splits)
    show ?thesis
      using 0 2 ‹is_shadow_root_kind x› shadow_root_ptr
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  next
    case False
    then show ?thesis
      using 0 1 2
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  qed
qed

lemma put_MDocument_document_element_type_wf_preserved [simp]:
  assumes "h ⊢ put_MDocument document_ptr document_element_update v →h h'"
  shows "type_wf h = type_wf h'"
  using assms
  apply(auto simp add: DocumentMonad.put_M_defs putDocument_def dest!: get_heap_E
      elim!: bind_returns_heap_E2
      intro!: type_wf_put_I DocumentMonad.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 DocumentClass.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 DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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]
proof -
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇document_element := v⦈)) h"
    and 2: "ShadowRootClass.type_wf h"
    and 3: "is_shadow_root_ptr_kind document_ptr"
  obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr" and
    "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
    by (metis "0" "3" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I
        is_shadow_root_ptr_kind_obtains shadow_root_ptr_kinds_commutes)

  then have "is_shadow_root_kind x"
    using 0 2
    apply(auto simp add: is_document_kind_def type_wf_defs is_shadow_root_kind_def getShadowRoot_def
        split: option.splits Option.bind_splits)[1]
    by (metis (no_types, lifting) DocumentMonad.get_M_defs get_heap_returns_result id_def
        option.simps(5) return_returns_result)

  then show "∃y. cast y = x⦇document_element := v⦈"
    using castDocument2ShadowRoot_none is_shadow_root_kind_document_element is_shadow_root_kindDocument_def
    by blast
next
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇document_element := v⦈)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (x⦇document_element := v⦈)) h)"
  have 3: "⋀document_ptr'. document_ptr' ≠ document_ptr ⟹ getObject (cast document_ptr') h = getObject (cast document_ptr') h'"
    by (simp add: "1")
  have "document_ptr |∈| document_ptr_kinds h"
    by (meson "0" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I)
  show "ShadowRootClass.type_wf h"
  proof (cases "is_shadow_root_ptr_kind document_ptr")
    case True
    then obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr"
      using is_shadow_root_ptr_kind_obtains by blast
    then
    have "is_shadow_root_kind (x⦇document_element := v⦈)"
      using 2 True
      by(simp add: type_wf_defs is_shadow_root_kindDocument_def split: if_splits option.splits)
    then
    have "is_shadow_root_kind x"
      using is_shadow_root_kind_document_element by blast
    then
    have "is_shadow_root_kind (the (getObject (cast document_ptr) h))"
      using 0
      by(auto simp add: DocumentMonad.a_get_M_def getDocument_def getObject_def is_shadow_root_kind_def
          split: option.splits Option.bind_splits)
    show ?thesis
      using 0 2 ‹is_shadow_root_kind x› shadow_root_ptr
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  next
    case False
    then show ?thesis
      using 0 1 2
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  qed
qed

lemma put_MDocument_disconnected_nodes_type_wf_preserved [simp]:
  assumes "h ⊢ put_MDocument document_ptr disconnected_nodes_update v →h h'"
  shows "type_wf h = type_wf h'"

  using assms
  apply(auto simp add: DocumentMonad.put_M_defs putDocument_def dest!: get_heap_E
      elim!: bind_returns_heap_E2
      intro!: type_wf_put_I DocumentMonad.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 DocumentClass.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 DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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  DocumentClass.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]
proof -
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇disconnected_nodes := v⦈)) h"
    and 2: "ShadowRootClass.type_wf h"
    and 3: "is_shadow_root_ptr_kind document_ptr"
  obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr" and
    "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
    by (metis "0" "3" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I is_shadow_root_ptr_kind_obtains
        shadow_root_ptr_kinds_commutes)

  then have "is_shadow_root_kind x"
    using 0 2
    apply(auto simp add: is_document_kind_def type_wf_defs is_shadow_root_kind_def getShadowRoot_def
        split: option.splits Option.bind_splits)[1]
    by (metis (no_types, lifting) DocumentMonad.get_M_defs get_heap_returns_result
        id_def option.simps(5) return_returns_result)

  then show "∃y. cast y = x⦇disconnected_nodes := v⦈"
    using castDocument2ShadowRoot_none is_shadow_root_kind_disconnected_nodes is_shadow_root_kindDocument_def
    by blast
next
  fix x
  assume 0: "h ⊢ get_MDocument document_ptr id →r x"
    and 1: "h' = put (cast document_ptr) (castDocument2Object (x⦇disconnected_nodes := v⦈)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (x⦇disconnected_nodes := v⦈)) h)"
  have 3: "⋀document_ptr'. document_ptr' ≠ document_ptr ⟹ getObject (cast document_ptr') h = getObject (cast document_ptr') h'"
    by (simp add: "1")
  have "document_ptr |∈| document_ptr_kinds h"
    by (meson "0" DocumentMonad.get_M_ptr_in_heap is_OK_returns_result_I)
  show "ShadowRootClass.type_wf h"
  proof (cases "is_shadow_root_ptr_kind document_ptr")
    case True
    then obtain shadow_root_ptr where shadow_root_ptr: "document_ptr = cast shadow_root_ptr"
      using is_shadow_root_ptr_kind_obtains by blast
    then
    have "is_shadow_root_kind (x⦇disconnected_nodes := v⦈)"
      using 2 True
      by(simp add: type_wf_defs is_shadow_root_kindDocument_def split: if_splits option.splits)
    then
    have "is_shadow_root_kind x"
      using is_shadow_root_kind_disconnected_nodes by blast
    then
    have "is_shadow_root_kind (the (getObject (cast document_ptr) h))"
      using 0
      by(auto simp add: DocumentMonad.a_get_M_def getDocument_def getObject_def is_shadow_root_kind_def
          split: option.splits Option.bind_splits)
    show ?thesis
      using 0 2 ‹is_shadow_root_kind x› shadow_root_ptr
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  next
    case False
    then show ?thesis
      using 0 1 2
      by(auto simp add: DocumentMonad.a_get_M_def getShadowRoot_def is_shadow_root_kind_def
          is_document_kind_def type_wf_defs  DocumentClass.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 if_splits)
  qed
qed

lemma put_MShadowRoot_mode_type_wf_preserved [simp]:
  "h ⊢ put_M shadow_root_ptr mode_update v →h h' ⟹ type_wf h = type_wf h'"
  by(auto simp add: get_M_defs getShadowRoot_def DocumentMonad.get_M_defs put_M_defs putShadowRoot_def
      putDocument_def dest!: get_heap_E  elim!: bind_returns_heap_E2 intro!: type_wf_put_I DocumentMonad.type_wf_put_I
      CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I
      simp add: is_shadow_root_kind_def 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 DocumentClass.type_wf_defs split: option.splits)[1]

lemma put_MShadowRoot_child_nodes_type_wf_preserved [simp]:
  "h ⊢ put_M shadow_root_ptr RShadowRoot.child_nodes_update v →h h' ⟹ type_wf h = type_wf h'"
  by(auto simp add: get_M_defs getShadowRoot_def DocumentMonad.get_M_defs put_M_defs putShadowRoot_def
      putDocument_def dest!: get_heap_E  elim!: bind_returns_heap_E2 intro!: type_wf_put_I
      DocumentMonad.type_wf_put_I CharacterDataMonad.type_wf_put_I ElementMonad.type_wf_put_I
      NodeMonad.type_wf_put_I ObjectMonad.type_wf_put_I
      simp add: is_shadow_root_kind_def 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
      DocumentClass.type_wf_defs split: option.splits)[1]

lemma shadow_root_ptr_kinds_small:
  assumes "⋀object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
  by(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def preserved_def
      object_ptr_kinds_preserved_small[OF assms])

lemma shadow_root_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_MObject object_ptr RObject.nothing) h h')"
  shows "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
  using writes_small_big[OF assms]
  apply(simp add: reflp_def transp_def preserved_def shadow_root_ptr_kinds_def document_ptr_kinds_def)
  by (metis assms object_ptr_kinds_preserved)


lemma new_shadow_root_known_ptr:
  assumes "h ⊢ newShadowRoot_M →r new_shadow_root_ptr"
  shows "known_ptr (cast new_shadow_root_ptr)"
  using assms
  apply(auto simp add: newShadowRoot_M_def newShadowRoot_def Let_def a_known_ptr_def
      elim!: bind_returns_result_E2 split: prod.splits)[1]
  using assms newShadowRoot_M_is_shadow_root_ptr by blast


lemma new_shadow_root_type_wf_preserved [simp]: "h ⊢ newShadowRoot_M →h h' ⟹ type_wf h = type_wf h'"
  apply(auto simp add: newShadowRoot_M_def newShadowRoot_def Let_def putShadowRoot_def putDocument_def
      ShadowRootClass.type_wfDocument ShadowRootClass.type_wfCharacterData  ShadowRootClass.type_wfElement
      ShadowRootClass.type_wfNode ShadowRootClass.type_wfObject
      is_node_ptr_kind_none newShadowRoot_ptr_not_in_heap
      elim!: bind_returns_heap_E type_wf_put_ptr_not_in_heap_E
      intro!: type_wf_put_I DocumentMonad.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]
  by(auto simp add: type_wf_defs DocumentClass.type_wf_defs ElementClass.type_wf_defs CharacterDataClass.type_wf_defs
      NodeClass.type_wf_defs ObjectClass.type_wf_defs is_shadow_root_kind_def is_document_kind_def
      split: option.splits)[1]


locale l_new_shadow_root = l_type_wf +
  assumes new_shadow_root_types_preserved: "h ⊢ newShadowRoot_M →h h' ⟹ type_wf h = type_wf h'"

lemma new_shadow_root_is_l_new_shadow_root  [instances]: "l_new_shadow_root type_wf"
  using l_new_shadow_root.intro new_shadow_root_type_wf_preserved
  by blast

lemma type_wf_preserved_small:
  assumes "⋀object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  assumes "⋀node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  assumes "⋀element_ptr. preserved (get_MElement element_ptr RElement.nothing) h h'"
  assumes "⋀character_data_ptr. preserved (get_MCharacterData character_data_ptr RCharacterData.nothing) h h'"
  assumes "⋀document_ptr. preserved (get_MDocument document_ptr RDocument.nothing) h h'"
  assumes "⋀shadow_root_ptr. preserved (get_MShadowRoot shadow_root_ptr RShadowRoot.nothing) h h'"
  shows "type_wf h = type_wf h'"
  using type_wf_preserved_small[OF assms(1) assms(2) assms(3) assms(4) assms(5)]
    allI[OF assms(6), of id, simplified] shadow_root_ptr_kinds_small[OF assms(1)]
  apply(auto simp add: type_wf_defs )[1]
   apply(auto simp add: preserved_def get_M_defs shadow_root_ptr_kinds_small[OF assms(1)]
      split: option.splits)[1]
   apply(force)
  apply(auto simp add: preserved_def get_M_defs shadow_root_ptr_kinds_small[OF assms(1)]
      split: option.splits)[1]
  apply(force)
  done

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_MObject object_ptr RObject.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ ∀node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ ∀element_ptr. preserved (get_MElement element_ptr RElement.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ ∀character_data_ptr. preserved (get_MCharacterData character_data_ptr RCharacterData.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ ∀document_ptr. preserved (get_MDocument document_ptr RDocument.nothing) h h'"
  assumes "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ ∀shadow_root_ptr. preserved (get_MShadowRoot shadow_root_ptr RShadowRoot.nothing) h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h' ⟹ type_wf h = 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) DocumentClass.type_wfObject DocumentMonad.type_wf_drop
      ObjectClass.getObject_type_wf document_ptr_kinds_commutes fmlookup_drop getDocument_def
      getObject_def getShadowRoot_def heap.sel shadow_root_ptr_kinds_commutes)

lemma delete_shadow_root_type_wf_preserved [simp]:
  assumes "h ⊢ deleteShadowRoot_M shadow_root_ptr →h h'"
  assumes "type_wf h"
  shows "type_wf h'"
  using assms
  using type_wf_drop
  by(auto simp add: deleteShadowRoot_M_def deleteShadowRoot_def deleteObject_def split: if_splits)



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 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 new_document_is_l_new_document [instances]:
  "l_new_document type_wf"
  using l_new_document.intro new_document_type_wf_preserved
  by blast
end