Theory ShadowRootClass

(***********************************************************************************
 * 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.
 ********************************************************************************\***)

section ‹The Shadow DOM Data Model›

theory ShadowRootClass
  imports
    Core_DOM.ShadowRootPointer
    Core_DOM.DocumentClass
begin

subsection ‹ShadowRoot›

datatype shadow_root_mode = Open | Closed
record ('node_ptr, 'element_ptr, 'character_data_ptr) RShadowRoot = RObject +
  nothing :: unit
  mode :: shadow_root_mode
  child_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr, 'ShadowRoot) ShadowRoot
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'ShadowRoot option) RShadowRoot_scheme"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'ShadowRoot) ShadowRoot"
type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node,
    'Element, 'CharacterData, 'Document,
    'ShadowRoot) Object
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, ('node_ptr, 'element_ptr,
'character_data_ptr, 'ShadowRoot option)
      RShadowRoot_ext + 'Object, 'Node, 'Element, 'CharacterData, 'Document) Object"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object,
'Node, 'Element, 'CharacterData,
    'Document, 'ShadowRoot) Object"

type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
    'shadow_root_ptr, 'Object, 'Node,
    'Element, 'CharacterData, 'Document, 'ShadowRoot) heap
  = "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
('node_ptr, 'element_ptr,
      'character_data_ptr, 'ShadowRoot option) RShadowRoot_ext + 'Object, 'Node, 'Element,
'CharacterData, 'Document) heap"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
'shadow_root_ptr, 'Object,
    'Node, 'Element, 'CharacterData, 'Document, 'ShadowRoot) heap"
type_synonym "heapfinal" = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"



definition shadow_root_ptr_kinds :: "(_) heap ⇒ (_) shadow_root_ptr fset"
  where
    "shadow_root_ptr_kinds heap =
the |`| (cast |`| (ffilter is_shadow_root_ptr_kind (object_ptr_kinds heap)))"

lemma shadow_root_ptr_kinds_simp [simp]:
  "shadow_root_ptr_kinds (Heap (fmupd (cast shadow_root_ptr) shadow_root (the_heap h))) =
{|shadow_root_ptr|} |∪| shadow_root_ptr_kinds h"
  by (auto simp add: shadow_root_ptr_kinds_def)

definition shadow_root_ptrs :: "(_) heap ⇒ (_) shadow_root_ptr fset"
  where
    "shadow_root_ptrs heap = ffilter is_shadow_root_ptr (shadow_root_ptr_kinds heap)"

definition castObject2ShadowRoot :: "(_) Object ⇒ (_) ShadowRoot option"
  where
    "castObject2ShadowRoot obj = (case RObject.more obj of
      Inr (Inr (Inl shadow_root)) ⇒ Some (RObject.extend (RObject.truncate obj) shadow_root)
    | _ ⇒ None)"
adhoc_overloading cast castObject2ShadowRoot

definition castShadowRoot2Object:: "(_) ShadowRoot ⇒ (_) Object"
  where
    "castShadowRoot2Object shadow_root =
(RObject.extend (RObject.truncate shadow_root) (Inr (Inr (Inl (RObject.more shadow_root)))))"
adhoc_overloading cast castShadowRoot2Object

definition is_shadow_root_kind :: "(_) Object ⇒ bool"
  where
    "is_shadow_root_kind ptr ⟷ castObject2ShadowRoot ptr ≠ None"

lemma shadow_root_ptr_kinds_heap_upd [simp]:
  "shadow_root_ptr_kinds (Heap (fmupd (cast shadow_root_ptr) shadow_root (the_heap h))) =
{|shadow_root_ptr|} |∪| shadow_root_ptr_kinds h"
  by (auto simp add: shadow_root_ptr_kinds_def)

lemma shadow_root_ptr_kinds_commutes [simp]:
  "cast shadow_root_ptr |∈| object_ptr_kinds h ⟷ shadow_root_ptr |∈| shadow_root_ptr_kinds h"
proof (rule iffI)
  show "cast shadow_root_ptr |∈| object_ptr_kinds h ⟹ shadow_root_ptr |∈| shadow_root_ptr_kinds h"
    by (metis (no_types, opaque_lifting) finsertI1 finsert_absorb funion_finsert_left
        funion_finsert_right putObject_def putObject_put_ptrs shadow_root_ptr_kinds_def
        shadow_root_ptr_kinds_heap_upd sup_bot.right_neutral)
next
  show "shadow_root_ptr |∈| shadow_root_ptr_kinds h ⟹ cast shadow_root_ptr |∈| object_ptr_kinds h"
    by (auto simp add: object_ptr_kinds_def shadow_root_ptr_kinds_def)
qed

definition getShadowRoot :: "(_) shadow_root_ptr ⇒ (_) heap ⇒ (_) ShadowRoot option"
  where
    "getShadowRoot shadow_root_ptr h = Option.bind (get (cast shadow_root_ptr) h) cast"
adhoc_overloading get getShadowRoot

locale l_type_wf_defShadowRoot
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = (DocumentClass.type_wf h ∧ (∀shadow_root_ptr ∈ fset (shadow_root_ptr_kinds h).
getShadowRoot shadow_root_ptr h ≠ None))"
end
global_interpretation l_type_wf_defShadowRoot defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfShadowRoot = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfShadowRoot: "type_wf h ⟹ ShadowRootClass.type_wf h"

sublocale l_type_wfShadowRoot ⊆ l_type_wfDocument
  apply(unfold_locales)
  by (metis (full_types) ShadowRootClass.type_wf_def a_type_wf_def l_type_wfShadowRoot_axioms
      l_type_wfShadowRoot_def)

lemma type_wf_implies_previous: "type_wf h ⟹ DocumentClass.type_wf h"
  by(simp add: type_wf_defs)

locale l_getShadowRoot_lemmas = l_type_wfShadowRoot
begin
sublocale l_getDocument_lemmas by unfold_locales
lemma getShadowRoot_type_wf:
  assumes "type_wf h"
  shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h ⟷ getShadowRoot shadow_root_ptr h ≠ None"
  using l_type_wfShadowRoot_axioms assms
  apply(simp add: type_wf_defs getShadowRoot_def l_type_wfShadowRoot_def)
  by (metis is_none_bind is_none_simps(1) is_none_simps(2) local.getObject_type_wf
      shadow_root_ptr_kinds_commutes)
end

global_interpretation l_getShadowRoot_lemmas type_wf by unfold_locales

definition putShadowRoot :: "(_) shadow_root_ptr ⇒ (_) ShadowRoot ⇒ (_) heap ⇒ (_) heap"
  where
    "putShadowRoot shadow_root_ptr shadow_root = put (cast shadow_root_ptr) (cast shadow_root)"
adhoc_overloading put putShadowRoot

lemma putShadowRoot_ptr_in_heap:
  assumes "putShadowRoot shadow_root_ptr shadow_root h = h'"
  shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h'"
  using assms
  unfolding putShadowRoot_def
  by (metis shadow_root_ptr_kinds_commutes putObject_ptr_in_heap)

lemma putShadowRoot_put_ptrs:
  assumes "putShadowRoot shadow_root_ptr shadow_root h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast shadow_root_ptr|}"
  using assms
  by (simp add: putShadowRoot_def putObject_put_ptrs)


lemma castShadowRoot2Object_inject [simp]: "castShadowRoot2Object x = castShadowRoot2Object y ⟷ x = y"
  apply(simp add: castShadowRoot2Object_def RObject.extend_def)
  by (metis (full_types) RObject.surjective old.unit.exhaust)

lemma castObject2ShadowRoot_none [simp]:
  "castObject2ShadowRoot obj = None ⟷ ¬ (∃shadow_root. castShadowRoot2Object shadow_root = obj)"
  apply(auto simp add: castObject2ShadowRoot_def castShadowRoot2Object_def RObject.extend_def
      split: sum.splits)[1]
  by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)

lemma castObject2ShadowRoot_some [simp]:
  "castObject2ShadowRoot obj = Some shadow_root ⟷ cast shadow_root = obj"
  by(auto simp add: castObject2ShadowRoot_def castShadowRoot2Object_def RObject.extend_def split: sum.splits)

lemma castObject2ShadowRoot_inv [simp]: "castObject2ShadowRoot (castShadowRoot2Object shadow_root) = Some shadow_root"
  by simp

lemma cast_shadow_root_not_node [simp]:
  "castShadowRoot2Object shadow_root ≠ castNode2Object node"
  "castNode2Object node ≠ castShadowRoot2Object shadow_root"
  by(auto simp add: castShadowRoot2Object_def castNode2Object_def RObject.extend_def)


lemma get_shadow_root_ptr_simp1 [simp]:
  "getShadowRoot shadow_root_ptr (putShadowRoot shadow_root_ptr shadow_root h) = Some shadow_root"
  by(auto simp add: getShadowRoot_def putShadowRoot_def)
lemma get_shadow_root_ptr_simp2 [simp]:
  "shadow_root_ptr ≠ shadow_root_ptr'
   ⟹ getShadowRoot shadow_root_ptr (putShadowRoot shadow_root_ptr' shadow_root h) =
getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putShadowRoot_def)

lemma get_shadow_root_ptr_simp3 [simp]:
  "getElement element_ptr (putShadowRoot shadow_root_ptr f h) = getElement element_ptr h"
  by(auto simp add: getElement_def getNode_def putShadowRoot_def)
lemma get_shadow_root_ptr_simp4 [simp]:
  "getShadowRoot shadow_root_ptr (putElement element_ptr f h) = getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putElement_def putNode_def)
lemma get_shadow_root_ptr_simp5 [simp]:
  "getCharacterData character_data_ptr (putShadowRoot shadow_root_ptr f h) = getCharacterData character_data_ptr h"
  by(auto simp add: getCharacterData_def getNode_def putShadowRoot_def)
lemma get_shadow_root_ptr_simp6 [simp]:
  "getShadowRoot shadow_root_ptr (putCharacterData character_data_ptr f h) = getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putCharacterData_def putNode_def)
lemma get_shadow_root_ptr_simp7 [simp]:
  "getDocument document_ptr (putShadowRoot shadow_root_ptr f h) = getDocument document_ptr h"
  by(auto simp add: getDocument_def getNode_def putShadowRoot_def)
lemma get_shadow_root_ptr_simp8 [simp]:
  "getShadowRoot shadow_root_ptr (putDocument document_ptr f h) = getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putDocument_def putNode_def)

lemma newElement_getShadowRoot [simp]:
  assumes "newElement h = (new_element_ptr, h')"
  shows "getShadowRoot ptr h = getShadowRoot ptr h'"
  using assms
  by(auto simp add: newElement_def Let_def)

lemma newCharacterData_getShadowRoot [simp]:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "getShadowRoot ptr h = getShadowRoot ptr h'"
  using assms
  by(auto simp add: newCharacterData_def Let_def)

lemma newDocument_getShadowRoot [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "getShadowRoot ptr h = getShadowRoot ptr h'"
  using assms
  by(auto simp add: newDocument_def Let_def)


abbreviation "create_shadow_root_obj mode_arg child_nodes_arg
  ≡ ⦇ RObject.nothing = (), RShadowRoot.nothing = (), mode = mode_arg,
RShadowRoot.child_nodes = child_nodes_arg, … = None ⦈"

definition newShadowRoot :: "(_)heap ⇒ ((_) shadow_root_ptr × (_) heap)"
  where
    "newShadowRoot h = (let new_shadow_root_ptr =
shadow_root_ptr.Ref (Suc (fMax (shadow_root_ptr.the_ref |`| (shadow_root_ptrs h)))) in
      (new_shadow_root_ptr, put new_shadow_root_ptr (create_shadow_root_obj Open []) h))"

lemma newShadowRoot_ptr_in_heap:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "new_shadow_root_ptr |∈| shadow_root_ptr_kinds h'"
  using assms
  unfolding newShadowRoot_def Let_def
  using putShadowRoot_ptr_in_heap by blast

lemma new_shadow_root_ptr_new:
  "shadow_root_ptr.Ref (Suc (fMax (finsert 0 (shadow_root_ptr.the_ref |`| shadow_root_ptrs h)))) |∉|
shadow_root_ptrs h"
  by (metis Suc_n_not_le_n shadow_root_ptr.sel(1) fMax_ge fimage_finsert finsertI1 finsertI2 set_finsert)

lemma newShadowRoot_ptr_not_in_heap:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "new_shadow_root_ptr |∉| shadow_root_ptr_kinds h"
  using assms
  unfolding newShadowRoot_def
  by (metis Pair_inject shadow_root_ptrs_def fMax_finsert fempty_iff ffmember_filter
      fimage_is_fempty is_shadow_root_ptr_ref max_0L new_shadow_root_ptr_new)

lemma newShadowRoot_new_ptr:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_shadow_root_ptr|}"
  using assms
  by (metis Pair_inject newShadowRoot_def putShadowRoot_put_ptrs)

lemma newShadowRoot_is_shadow_root_ptr:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "is_shadow_root_ptr new_shadow_root_ptr"
  using assms
  by(auto simp add: newShadowRoot_def Let_def)


lemma newShadowRoot_getObject [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  assumes "ptr ≠ cast new_shadow_root_ptr"
  shows "getObject ptr h = getObject ptr h'"
  using assms
  by(auto simp add: newShadowRoot_def Let_def putShadowRoot_def)

lemma newShadowRoot_getNode [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "getNode ptr h = getNode ptr h'"
  using assms
  apply(simp add: newShadowRoot_def Let_def putShadowRoot_def)
  by(auto simp add: getNode_def)

lemma newShadowRoot_getElement [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "getElement ptr h = getElement ptr h'"
  using assms
  by(auto simp add: newShadowRoot_def Let_def)

lemma newShadowRoot_getCharacterData [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "getCharacterData ptr h = getCharacterData ptr h'"
  using assms
  by(auto simp add: newShadowRoot_def Let_def)

lemma newShadowRoot_getDocument [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  shows "getDocument ptr h = getDocument ptr h'"
  using assms
  apply(simp add: newShadowRoot_def Let_def putShadowRoot_def)
  by(auto simp add: getDocument_def)

lemma newShadowRoot_getShadowRoot [simp]:
  assumes "newShadowRoot h = (new_shadow_root_ptr, h')"
  assumes "ptr ≠ new_shadow_root_ptr"
  shows "getShadowRoot ptr h = getShadowRoot ptr h'"
  using assms
  by(auto simp add: newShadowRoot_def Let_def)


locale l_known_ptrShadowRoot
begin
definition a_known_ptr :: "(_) object_ptr ⇒ bool"
  where
    "a_known_ptr ptr = (known_ptr ptr ∨ is_shadow_root_ptr ptr)"

lemma known_ptr_not_shadow_root_ptr: "a_known_ptr ptr ⟹ ¬is_shadow_root_ptr ptr ⟹ known_ptr ptr"
  by(simp add: a_known_ptr_def)
lemma known_ptr_new_shadow_root_ptr: "a_known_ptr ptr ⟹ ¬known_ptr ptr ⟹ is_shadow_root_ptr ptr"
  using l_known_ptrShadowRoot.known_ptr_not_shadow_root_ptr by blast

end
global_interpretation l_known_ptrShadowRoot defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def

locale l_known_ptrsShadowRoot = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr ⇒ bool"
begin
definition a_known_ptrs :: "(_) heap ⇒ bool"
  where
    "a_known_ptrs h = (∀ptr ∈ fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr: "a_known_ptrs h ⟹ ptr |∈| object_ptr_kinds h ⟹ known_ptr ptr"
  by (simp add: a_known_ptrs_def)

lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h' ⟹ a_known_ptrs h = a_known_ptrs h'"
  by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
  "object_ptr_kinds h' |⊆| object_ptr_kinds h ⟹ a_known_ptrs h ⟹ a_known_ptrs h'"
  by (simp add: less_eq_fset.rep_eq local.a_known_ptrs_def subsetD)
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|} ⟹ known_ptr new_ptr ⟹
a_known_ptrs h ⟹ a_known_ptrs h'"
  by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrsShadowRoot known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

lemma known_ptrs_is_l_known_ptrs  [instances]: "l_known_ptrs known_ptr known_ptrs"
  using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
    known_ptrs_new_ptr
  by blast


lemma shadow_root_get_put_1 [simp]:
  "getShadowRoot shadow_root_ptr (putShadowRoot shadow_root_ptr shadow_root h) = Some shadow_root"
  by(auto simp add: getShadowRoot_def putShadowRoot_def)
lemma shadow_root_different_get_put [simp]:
  "shadow_root_ptr ≠ shadow_root_ptr' ⟹
getShadowRoot shadow_root_ptr (putShadowRoot shadow_root_ptr' shadow_root h) = getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putShadowRoot_def)


lemma shadow_root_get_put_2 [simp]:
  "getElement element_ptr (putShadowRoot shadow_root_ptr f h) = getElement element_ptr h"
  by(auto simp add: getElement_def getNode_def putShadowRoot_def)
lemma shadow_root_get_put_3 [simp]:
  "getShadowRoot element_ptr (putElement shadow_root_ptr f h) = getShadowRoot element_ptr h"
  by(auto simp add: getShadowRoot_def putElement_def putNode_def)
lemma shadow_root_get_put_4 [simp]:
  "getCharacterData character_data_ptr (putShadowRoot shadow_root_ptr f h) = getCharacterData character_data_ptr h"
  by(auto simp add: getCharacterData_def getNode_def putShadowRoot_def)
lemma shadow_root_get_put_5 [simp]:
  "getShadowRoot character_data_ptr (putCharacterData shadow_root_ptr f h) = getShadowRoot character_data_ptr h"
  by(auto simp add: getShadowRoot_def putCharacterData_def putNode_def)
lemma shadow_root_get_put_6 [simp]:
  "getDocument document_ptr (putShadowRoot shadow_root_ptr f h) = getDocument document_ptr h"
  by(auto simp add: getDocument_def getNode_def putShadowRoot_def)
lemma shadow_root_get_put_7 [simp]:
  "getShadowRoot document_ptr (putDocument shadow_root_ptr f h) = getShadowRoot document_ptr h"
  by(auto simp add: getShadowRoot_def putDocument_def putNode_def)

lemma known_ptrs_implies: "DocumentClass.known_ptrs h ⟹ ShadowRootClass.known_ptrs h"
  by(auto simp add: DocumentClass.known_ptrs_defs DocumentClass.known_ptr_defs
      ShadowRootClass.known_ptrs_defs ShadowRootClass.known_ptr_defs)

definition deleteShadowRoot :: "(_) shadow_root_ptr ⇒ (_) heap ⇒ (_) heap option" where
  "deleteShadowRoot shadow_root_ptr = deleteObject (cast shadow_root_ptr)"

lemma deleteShadowRoot_pointer_removed:
  assumes "deleteShadowRoot ptr h = Some h'"
  shows "ptr |∉| shadow_root_ptr_kinds h'"
  using assms
  by(auto simp add: deleteObject_pointer_removed deleteShadowRoot_def shadow_root_ptr_kinds_def
      split: if_splits)

lemma deleteShadowRoot_pointer_ptr_in_heap:
  assumes "deleteShadowRoot ptr h = Some h'"
  shows "ptr |∈| shadow_root_ptr_kinds h"
  using assms
  apply(auto simp add: deleteObject_pointer_ptr_in_heap deleteShadowRoot_def split: if_splits)[1]
  using deleteObject_pointer_ptr_in_heap
  by fastforce

lemma deleteShadowRoot_ok:
  assumes "ptr |∈| shadow_root_ptr_kinds h"
  shows "deleteShadowRoot ptr h ≠ None"
  using assms
  by (simp add: deleteObject_ok deleteShadowRoot_def)

lemma shadow_root_delete_get_1 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ getShadowRoot shadow_root_ptr h' = None"
  by(auto simp add: deleteShadowRoot_def deleteObject_def getShadowRoot_def getObject_def split: if_splits)
lemma shadow_root_different_delete_get [simp]:
  "shadow_root_ptr ≠ shadow_root_ptr' ⟹ deleteShadowRoot shadow_root_ptr' h = Some h' ⟹
getShadowRoot shadow_root_ptr h' = getShadowRoot shadow_root_ptr h"
  by(auto simp add: deleteShadowRoot_def deleteObject_def getShadowRoot_def getObject_def split: if_splits)


lemma shadow_root_delete_get_2 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ object_ptr ≠ cast shadow_root_ptr ⟹
getObject object_ptr h' = getObject object_ptr h"
  by(auto simp add: deleteShadowRoot_def deleteObject_def getShadowRoot_def getObject_def split: if_splits)
lemma shadow_root_delete_get_3 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ getNode node_ptr h' = getNode node_ptr h"
  by(auto simp add: getNode_def)
lemma shadow_root_delete_get_4 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ getElement element_ptr h' = getElement element_ptr h"
  by(simp add: getElement_def)
lemma shadow_root_delete_get_5 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹
getCharacterData character_data_ptr h' = getCharacterData character_data_ptr h"
  by(simp add: getCharacterData_def)
lemma shadow_root_delete_get_6 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ getDocument document_ptr h' = getDocument document_ptr h"
  by(simp add: getDocument_def)
lemma shadow_root_delete_get_7 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ shadow_root_ptr' ≠ shadow_root_ptr ⟹
getShadowRoot shadow_root_ptr' h' = getShadowRoot shadow_root_ptr' h"
  by(auto simp add: deleteShadowRoot_def deleteObject_def getShadowRoot_def getObject_def split: if_splits)
end