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_SC_DOM.ShadowRootPointer
    Core_SC_DOM.DocumentClass
begin

subsection ‹ShadowRoot›

datatype shadow_root_mode = Open | Closed
record ('node_ptr, 'element_ptr, 'character_data_ptr) RShadowRoot =
  "('node_ptr, 'element_ptr, 'character_data_ptr) RDocument" +
  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, 'Document, 'ShadowRoot) Document
  = "('node_ptr, 'element_ptr, 'character_data_ptr, ('node_ptr, 'element_ptr, 'character_data_ptr,
'ShadowRoot option) RShadowRoot_ext + 'Document) Document"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'Document, 'ShadowRoot) Document"
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, 'Object, 'Node, 'Element,
'CharacterData, ('node_ptr, 'element_ptr, 'character_data_ptr, 'ShadowRoot option)
      RShadowRoot_ext + '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,
'Object, 'Node, 'Element, 'CharacterData, ('node_ptr, 'element_ptr,
      'character_data_ptr, 'ShadowRoot option) RShadowRoot_ext + '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 |`| (castdocument_ptr2shadow_root_ptr |`| (ffilter is_shadow_root_ptr_kind (document_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 castDocument2ShadowRoot :: "(_) Document ⇒ (_) ShadowRoot option"
  where
    "castDocument2ShadowRoot document = (case RDocument.more document of Some (Inl shadow_root) ⇒
Some (RDocument.extend (RDocument.truncate document) shadow_root) | _ ⇒ None)"
adhoc_overloading cast castDocument2ShadowRoot

abbreviation castObject2ShadowRoot :: "(_) Object ⇒ (_) ShadowRoot option"
  where
    "castObject2ShadowRoot obj ≡ (case castObject2Document obj of
Some document ⇒ castDocument2ShadowRoot document | None ⇒ None)"
adhoc_overloading cast castObject2ShadowRoot

definition castShadowRoot2Document :: "(_) ShadowRoot ⇒ (_) Document"
  where
    "castShadowRoot2Document shadow_root = RDocument.extend (RDocument.truncate shadow_root)
(Some (Inl (RDocument.more shadow_root)))"
adhoc_overloading cast castShadowRoot2Document

abbreviation castShadowRoot2Object :: "(_) ShadowRoot ⇒ (_) Object"
  where
    "castShadowRoot2Object ptr ≡ castDocument2Object (castShadowRoot2Document ptr)"
adhoc_overloading cast castShadowRoot2Object

consts is_shadow_root_kind :: 'a
definition is_shadow_root_kindDocument :: "(_) Document ⇒ bool"
  where
    "is_shadow_root_kindDocument ptr ⟷ castDocument2ShadowRoot ptr ≠ None"

adhoc_overloading is_shadow_root_kind is_shadow_root_kindDocument
lemmas is_shadow_root_kind_def = is_shadow_root_kindDocument_def

abbreviation is_shadow_root_kindObject :: "(_) Object ⇒ bool"
  where
    "is_shadow_root_kindObject ptr ≡ castObject2ShadowRoot ptr ≠ None"
adhoc_overloading is_shadow_root_kind is_shadow_root_kindObject

definition getShadowRoot :: "(_) shadow_root_ptr ⇒ (_) heap ⇒ (_) ShadowRoot option"
  where
    "getShadowRoot shadow_root_ptr h = Option.bind (getDocument (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)
  using DocumentClass.a_type_wf_def
  by (meson ShadowRootClass.a_type_wf_def l_type_wfShadowRoot_axioms l_type_wfShadowRoot_def)

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"
proof
  assume "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  then
  show "get shadow_root_ptr h ≠ None"
    using l_type_wfShadowRoot_axioms[unfolded l_type_wfShadowRoot_def type_wf_defs] assms
    by meson
next
  assume "get shadow_root_ptr h ≠ None"
  then
  show "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
    apply(auto simp add: getShadowRoot_def getDocument_def getObject_def shadow_root_ptr_kinds_def
        document_ptr_kinds_def object_ptr_kinds_def
        split: Option.bind_splits)[1]
    by (metis (no_types, lifting) IntI document_ptr_casts_commute2 document_ptr_document_ptr_cast
        fmdomI image_iff is_shadow_root_ptr_kind_cast mem_Collect_eq option.sel
        shadow_root_ptr_casts_commute2)
qed
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 = putDocument (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 shadow_root_ptr_kinds_def
  by (metis ffmember_filter fimage_eqI is_shadow_root_ptr_kind_cast option.sel
      putDocument_ptr_in_heap shadow_root_ptr_casts_commute2)

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 putDocument_put_ptrs)



lemma castShadowRoot2Document_inject [simp]:
  "castShadowRoot2Document x = castShadowRoot2Document y ⟷ x = y"
  apply(auto simp add: castShadowRoot2Document_def RObject.extend_def RDocument.extend_def
      RDocument.truncate_def)[1]
  by (metis RDocument.select_convs(5) RShadowRoot.surjective old.unit.exhaust)

lemma castDocument2ShadowRoot_none [simp]:
  "castDocument2ShadowRoot document = None ⟷ ¬ (∃shadow_root. castShadowRoot2Document shadow_root = document)"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RObject.extend_def
      RDocument.extend_def RDocument.truncate_def
      split: sum.splits option.splits)[1]
  by (metis (mono_tags, lifting) RDocument.select_convs(2) RDocument.select_convs(3)
      RDocument.select_convs(4) RDocument.select_convs(5) RDocument.surjective old.unit.exhaust)


lemma castDocument2ShadowRoot_some [simp]:
  "castDocument2ShadowRoot document = Some shadow_root ⟷ castShadowRoot2Document shadow_root = document"
  apply(auto simp add: castDocument2ShadowRoot_def castShadowRoot2Document_def RObject.extend_def
      RDocument.extend_def RDocument.truncate_def
      split: sum.splits option.splits)[1]
  by (metis RDocument.select_convs(5) RShadowRoot.surjective old.unit.exhaust)


lemma castDocument2ShadowRoot_inv [simp]:
  "castDocument2ShadowRoot (castShadowRoot2Document shadow_root) = Some shadow_root"
  by simp

lemma is_shadow_root_kind_doctype [simp]:
  "is_shadow_root_kind x ⟷ is_shadow_root_kind (doctype_update (λ_. v) x)"
  apply(auto simp add: is_shadow_root_kind_def castShadowRoot2Document_def RDocument.extend_def
      RDocument.truncate_def split: option.splits)[1]
   apply (metis RDocument.ext_inject RDocument.select_convs(3) RDocument.surjective RObject.ext_inject)
  by (smt RDocument.select_convs(2) RDocument.select_convs(3) RDocument.select_convs(4)
      RDocument.select_convs(5) RDocument.surjective RDocument.update_convs(2) old.unit.exhaust)

lemma is_shadow_root_kind_document_element [simp]:
  "is_shadow_root_kind x ⟷ is_shadow_root_kind (document_element_update (λ_. v) x)"
  apply(auto simp add: is_shadow_root_kind_def castShadowRoot2Document_def RDocument.extend_def
      RDocument.truncate_def  split: option.splits)[1]
   apply (metis RDocument.ext_inject RDocument.select_convs(3) RDocument.surjective RObject.ext_inject)
  by (metis (no_types, lifting) RDocument.ext_inject RDocument.surjective RDocument.update_convs(3)
      RObject.select_convs(1) RObject.select_convs(2))

lemma is_shadow_root_kind_disconnected_nodes [simp]:
  "is_shadow_root_kind x ⟷ is_shadow_root_kind (disconnected_nodes_update (λ_. v) x)"
  apply(auto simp add: is_shadow_root_kind_def castShadowRoot2Document_def RDocument.extend_def
      RDocument.truncate_def split: option.splits)[1]
   apply (metis RDocument.ext_inject RDocument.select_convs(3) RDocument.surjective RObject.ext_inject)
  by (metis (no_types, lifting) RDocument.ext_inject RDocument.surjective RDocument.update_convs(4)
      RObject.select_convs(1) RObject.select_convs(2))

lemma shadow_root_ptr_kinds_commutes [simp]:
  "cast shadow_root_ptr |∈| document_ptr_kinds h ⟷ shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  apply(auto simp add: document_ptr_kinds_def shadow_root_ptr_kinds_def)[1]
  by (metis Int_iff imageI is_shadow_root_ptr_kind_cast mem_Collect_eq option.sel
      shadow_root_ptr_casts_commute2)

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 putDocument_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 getDocument_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 putDocument_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 getDocument_def putCharacterData_def putNode_def)

lemma get_shadow_root_put_document [simp]:
  "cast shadow_root_ptr ≠ document_ptr
   ⟹ getShadowRoot shadow_root_ptr (putDocument document_ptr document h) = getShadowRoot shadow_root_ptr h"
  by(auto simp add: getShadowRoot_def putShadowRoot_def)
lemma get_document_put_shadow_root [simp]:
  "document_ptr ≠ cast shadow_root_ptr
   ⟹ getDocument document_ptr (putShadowRoot shadow_root_ptr shadow_root h) = getDocument document_ptr h"
  by(auto simp add: putShadowRoot_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')"
  assumes "cast ptr ≠ new_document_ptr"
  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 = (), RDocument.nothing = (), RDocument.doctype = ''html'',
RDocument.document_element = None, RDocument.disconnected_nodes = [], 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
  apply(auto simp add: Let_def newShadowRoot_def shadow_root_ptr_kinds_def)[1]
  by (metis Suc_n_not_le_n fMax_ge ffmember_filter fimageI is_shadow_root_ptr_ref
      shadow_root_ptr.disc(1) shadow_root_ptr.exhaust shadow_root_ptr.is_Ref_def shadow_root_ptr.sel(1)
      shadow_root_ptr.simps(4) shadow_root_ptr_casts_commute3 shadow_root_ptr_kinds_commutes
      shadow_root_ptrs_def)

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 putDocument_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 putDocument_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')"
  assumes "ptr ≠ cast new_shadow_root_ptr"
  shows "getDocument ptr h = getDocument ptr h'"
  using assms
  apply(simp add: newShadowRoot_def Let_def putShadowRoot_def putDocument_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: a_known_ptrs_def less_eq_fset.rep_eq 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 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
      document_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 getDocument_def getObject_def
      split: if_splits)
lemma shadow_root_delete_get_2 [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 getDocument_def getObject_def
      split: if_splits)


lemma shadow_root_delete_get_3 [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_4 [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_5 [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_6 [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_7 [simp]:
  "deleteShadowRoot shadow_root_ptr h = Some h' ⟹ document_ptr  ≠ cast shadow_root_ptr ⟹
getDocument document_ptr h' = getDocument document_ptr h"
  by(simp add: getDocument_def)
lemma shadow_root_delete_get_8 [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