Session Shadow_SC_DOM

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"
  apply(auto simp add: shadow_root_ptr_kinds_def)[1]
  by force

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 notin_fset)
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 comp_eq_dest_lhs document_ptr_casts_commute2 document_ptr_document_ptr_cast
        ffmember_filter fimageI fmdomI is_shadow_root_ptr_kind_cast 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 (no_types, lifting) shadow_root_ptr_casts_commute2 ffmember_filter fimage_eqI
      fset.map_comp is_shadow_root_ptr_kind_none document_ptr_casts_commute3
      document_ptr_kinds_commutes document_ptr_kinds_def option.sel option.simps(3))

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"
  apply(simp add: a_known_ptrs_def)
  using notin_fset by fastforce

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

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"
  apply(simp add: getShadowRoot_type_wf l_get_M_def)
  apply(auto simp add: getShadowRoot_def shadow_root_ptr_kinds_def)[1]
  by (metis (no_types, lifting) DocumentMonad.l_get_M_axioms bind_eq_None_conv fset.map_comp
      l_get_M_def option.discI shadow_root_ptr_kinds_commutes shadow_root_ptr_kinds_def)
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 xdisconnected_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 xdoctype := 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 xdocument_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 xdisconnected_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 xdoctype := 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 xdocument_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, 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 notin_fset
      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, lifting) DocumentClass.l_getObject_lemmas_axioms assms(2) bind.bind_lunit
      castDocument2ShadowRoot_inv castObject2Document_inv finite_set_in 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 (xdoctype := 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 finite_set_in get_heap_returns_result
        id_apply option.simps(5) return_returns_result)


  then show "y. cast y = xdoctype := 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 (xdoctype := v)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (xdoctype := 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 (xdoctype := 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 (xdocument_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 finite_set_in get_heap_returns_result id_def
        option.simps(5) return_returns_result)

  then show "y. cast y = xdocument_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 (xdocument_element := v)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (xdocument_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 (xdocument_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 (xdisconnected_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 finite_set_in get_heap_returns_result
        id_def option.simps(5) return_returns_result)

  then show "y. cast y = xdisconnected_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 (xdisconnected_nodes := v)) h"
    and 2: "ShadowRootClass.type_wf (put (cast document_ptr) (castDocument2Object (xdisconnected_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 (xdisconnected_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, lifting) DocumentClass.type_wfObject DocumentMonad.type_wf_drop
      ObjectClass.getObject_type_wf document_ptr_kinds_commutes finite_set_in 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

Theory Shadow_DOM

(***********************************************************************************
 * 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‹The Shadow DOM›
theory Shadow_DOM
  imports
    "monads/ShadowRootMonad"
    Core_SC_DOM.Core_DOM
begin



abbreviation "safe_shadow_root_element_types  {''article'', ''aside'', ''blockquote'', ''body'',
  ''div'', ''footer'', ''h1'', ''h2'', ''h3'', ''h4'', ''h5'', ''h6'', ''header'', ''main'',
  ''nav'', ''p'', ''section'', ''span''}"


subsection ‹Function Definitions›



subsubsection ‹get\_child\_nodes›

locale l_get_child_nodesShadow_DOM_defs =
  CD: l_get_child_nodesCore_DOM_defs
begin
definition get_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr  unit
     (_, (_) node_ptr list) dom_prog" where
  "get_child_nodesshadow_root_ptr shadow_root_ptr _ = get_M shadow_root_ptr RShadowRoot.child_nodes"

definition a_get_child_nodes_tups :: "(((_) object_ptr  bool) × ((_) object_ptr  unit
     (_, (_) node_ptr list) dom_prog)) list" where
  "a_get_child_nodes_tups  [(is_shadow_root_ptrobject_ptr, get_child_nodesshadow_root_ptr  the  cast)]"

definition a_get_child_nodes :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog" where
  "a_get_child_nodes ptr = invoke (CD.a_get_child_nodes_tups @ a_get_child_nodes_tups) ptr ()"

definition a_get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set" where
  "a_get_child_nodes_locs ptr 
    (if is_shadow_root_ptr_kind ptr
    then {preserved (get_M (the (cast ptr)) RShadowRoot.child_nodes)} else {}) 
    CD.a_get_child_nodes_locs ptr"

definition first_child :: "(_) object_ptr  (_, (_) node_ptr option) dom_prog"
  where
    "first_child ptr = do {
      children  a_get_child_nodes ptr;
      return (case children of []  None | child#_  Some child)}"
end

global_interpretation l_get_child_nodesShadow_DOM_defs defines
  get_child_nodes = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes and
  get_child_nodes_locs = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes_locs
  .

locale l_get_child_nodesShadow_DOM =
  l_type_wf type_wf +
  l_known_ptr known_ptr +
  l_get_child_nodesShadow_DOM_defs +
  l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
  CD: l_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
  get_child_nodes_locsCore_DOM
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and get_child_nodes :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog"
    and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and get_child_nodesCore_DOM :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog"
    and get_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap  (_) heap  bool) set" +
  assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
  assumes get_child_nodes_impl: "get_child_nodes = a_get_child_nodes"
  assumes get_child_nodes_locs_impl: "get_child_nodes_locs = a_get_child_nodes_locs"
begin
lemmas get_child_nodes_def = get_child_nodes_impl[unfolded a_get_child_nodes_def get_child_nodes_def]
lemmas get_child_nodes_locs_def = get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def
    get_child_nodes_locs_def, folded CD.get_child_nodes_locs_impl]

lemma get_child_nodes_ok:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "ptr |∈| object_ptr_kinds h"
  shows "h  ok (get_child_nodes ptr)"
  using assms[unfolded known_ptr_impl type_wf_impl]
  apply(auto simp add: get_child_nodes_def)[1]
  apply(split CD.get_child_nodes_splits, rule conjI)+
  using ShadowRootClass.type_wfDocument CD.get_child_nodes_ok CD.known_ptr_impl CD.type_wf_impl
   apply blast
  apply(auto simp add: CD.known_ptr_impl a_get_child_nodes_tups_def get_child_nodesshadow_root_ptr_def
      get_MShadowRoot_ok
      dest!: known_ptr_new_shadow_root_ptr intro!: bind_is_OK_I2)[1]
  by(auto dest: get_MShadowRoot_ok split: option.splits)

lemma get_child_nodes_ptr_in_heap:
  assumes "h  get_child_nodes ptr r children"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  by(auto simp add: get_child_nodes_def invoke_ptr_in_heap dest: is_OK_returns_result_I)

lemma get_child_nodes_pure [simp]:
  "pure (get_child_nodes ptr) h"
  apply (auto simp add: get_child_nodes_def a_get_child_nodes_tups_def)[1]
  apply(split CD.get_child_nodes_splits, rule conjI)+
   apply(simp)
  apply(split invoke_splits, rule conjI)+
   apply(simp)
  by(auto simp add: get_child_nodesshadow_root_ptr_def intro!: bind_pure_I)

lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
  apply (simp add: get_child_nodes_def a_get_child_nodes_tups_def get_child_nodes_locs_def
      CD.get_child_nodes_locs_def)
  apply(split CD.get_child_nodes_splits, rule conjI)+
   apply(auto intro!: reads_subset[OF CD.get_child_nodes_reads[unfolded  CD.get_child_nodes_locs_def]]
      split: if_splits)[1]
  apply(split invoke_splits, rule conjI)+
   apply(auto)[1]
  apply(auto simp add: get_child_nodesshadow_root_ptr_def
      intro: reads_subset[OF reads_singleton] reads_subset[OF check_in_heap_reads]
      intro!: reads_bind_pure reads_subset[OF return_reads] split: option.splits)[1]
  done
end

interpretation i_get_child_nodes?: l_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by(simp add: l_get_child_nodesShadow_DOM_def l_get_child_nodesShadow_DOM_axioms_def instances)
declare l_get_child_nodesShadow_DOM_axioms [instances]

lemma get_child_nodes_is_l_get_child_nodes [instances]: "l_get_child_nodes type_wf known_ptr
    get_child_nodes get_child_nodes_locs"
  apply(auto simp add: l_get_child_nodes_def instances)[1]
  using get_child_nodes_reads get_child_nodes_ok get_child_nodes_ptr_in_heap get_child_nodes_pure
  by blast+


paragraph ‹new\_document›

locale l_new_document_get_child_nodesShadow_DOM =
  CD: l_new_document_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
  get_child_nodes_locsCore_DOM
  + l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
  get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and get_child_nodes :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and get_child_nodesCore_DOM :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_child_nodes_new_document:
  "ptr'  cast new_document_ptr  h  new_document r new_document_ptr
      h  new_document h h'  r  get_child_nodes_locs ptr'  r h h'"
  apply(auto simp add: get_child_nodes_locs_def)[1]
  using CD.get_child_nodes_new_document
   apply (metis document_ptr_casts_commute3 empty_iff is_document_ptr_kind_none
      new_document_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3 singletonD)
  by (simp add: CD.get_child_nodes_new_document)

lemma new_document_no_child_nodes:
  "h  new_document r new_document_ptr  h  new_document h h'
      h'  get_child_nodes (cast new_document_ptr) r []"
  apply(auto simp add: get_child_nodes_def)[1]
  apply(split CD.get_child_nodes_splits, rule conjI)+
  using CD.new_document_no_child_nodes apply auto[1]
  by(auto simp add: DocumentClass.a_known_ptr_def CD.known_ptr_impl known_ptr_def
      dest!: new_document_is_document_ptr)
end
interpretation i_new_document_get_child_nodes?:
  l_new_document_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by(unfold_locales)
declare l_new_document_get_child_nodesCore_DOM_axioms[instances]

lemma new_document_get_child_nodes_is_l_new_document_get_child_nodes [instances]:
  "l_new_document_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  using new_document_is_l_new_document get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_new_document_get_child_nodes_def l_new_document_get_child_nodes_axioms_def)
  using get_child_nodes_new_document new_document_no_child_nodes
  by fast

paragraph ‹new\_shadow\_root›

locale l_new_shadow_root_get_child_nodesShadow_DOM =
  l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
  get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and get_child_nodes :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and get_child_nodesCore_DOM :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_child_nodes_new_shadow_root:
  "ptr'  cast new_shadow_root_ptr  h  newShadowRoot_M r new_shadow_root_ptr
      h  newShadowRoot_M h h'  r  get_child_nodes_locs ptr'  r h h'"
  apply(auto simp add: get_child_nodes_locs_def)[1]
   apply (metis document_ptr_casts_commute3 insert_absorb insert_not_empty is_document_ptr_kind_none
      new_shadow_root_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3 singletonD)
  apply(auto simp add: CD.get_child_nodes_locs_def)[1]
  using new_shadow_root_get_MObject apply blast
   apply (smt insertCI new_shadow_root_get_MElement singleton_iff)
  apply (metis document_ptr_casts_commute3 empty_iff new_shadow_root_get_MDocument singletonD)
  done

lemma new_shadow_root_no_child_nodes:
  "h  newShadowRoot_M r new_shadow_root_ptr  h  newShadowRoot_M h h'
      h'  get_child_nodes (cast new_shadow_root_ptr) r []"
  apply(auto simp add: get_child_nodes_def )[1]
  apply(split CD.get_child_nodes_splits, rule conjI)+
   apply(auto simp add: CD.get_child_nodes_def CD.a_get_child_nodes_tups_def)[1]
   apply(split invoke_splits, rule conjI)+
  using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr
    known_ptr_not_element_ptr local.CD.known_ptr_impl apply blast
     apply(auto simp add: is_document_ptr_def castshadow_root_ptr2document_ptr_def
      split: option.splits document_ptr.splits)[1]
    apply(auto simp add: is_character_data_ptr_def castshadow_root_ptr2document_ptr_def
      split: option.splits document_ptr.splits)[1]
   apply(auto simp add: is_element_ptr_def castshadow_root_ptr2document_ptr_def
      split: option.splits document_ptr.splits)[1]
  apply(auto simp add: a_get_child_nodes_tups_def)[1]
  apply(split invoke_splits, rule conjI)+
   apply(auto simp add: is_shadow_root_ptr_def split: shadow_root_ptr.splits
      dest!: newShadowRoot_M_is_shadow_root_ptr)[1]
  apply(auto intro!: bind_pure_returns_result_I)[1]
   apply(drule(1) newShadowRoot_M_ptr_in_heap)
   apply(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)[1]
   apply (metis check_in_heap_ptr_in_heap is_OK_returns_result_E old.unit.exhaust)
  using  new_shadow_root_children
  by (simp add: new_shadow_root_children get_child_nodesshadow_root_ptr_def)
end
interpretation i_new_shadow_root_get_child_nodes?:
  l_new_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by(unfold_locales)
declare l_new_shadow_root_get_child_nodesShadow_DOM_def[instances]

locale l_new_shadow_root_get_child_nodes = l_get_child_nodes +
  assumes get_child_nodes_new_shadow_root:
    "ptr'  cast new_shadow_root_ptr  h  newShadowRoot_M r new_shadow_root_ptr
      h  newShadowRoot_M h h'  r  get_child_nodes_locs ptr'  r h h'"
  assumes new_shadow_root_no_child_nodes:
    "h  newShadowRoot_M r new_shadow_root_ptr  h  newShadowRoot_M h h'
      h'  get_child_nodes (cast new_shadow_root_ptr) r []"

lemma new_shadow_root_get_child_nodes_is_l_new_shadow_root_get_child_nodes [instances]:
  "l_new_shadow_root_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  apply(simp add: l_new_shadow_root_get_child_nodes_def l_new_shadow_root_get_child_nodes_axioms_def instances)
  using get_child_nodes_new_shadow_root new_shadow_root_no_child_nodes
  by fast

paragraph ‹new\_element›

locale l_new_element_get_child_nodesShadow_DOM =
  l_get_child_nodesShadow_DOM +
  l_new_element_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
begin
lemma get_child_nodes_new_element:
  "ptr'  cast new_element_ptr  h  new_element r new_element_ptr  h  new_element h h'
      r  get_child_nodes_locs ptr'  r h h'"
  by (auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def new_element_get_MObject new_element_get_MElement
      new_element_get_MDocument new_element_get_MShadowRoot split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)

lemma new_element_no_child_nodes:
  "h  new_element r new_element_ptr  h  new_element h h'
    h'  get_child_nodes (cast new_element_ptr) r []"
  apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def
      split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
  apply(split CD.get_child_nodes_splits, rule conjI)+
  using local.new_element_no_child_nodes apply auto[1]
  apply(auto simp add: invoke_def)[1]
  using case_optionE apply fastforce
  apply(auto simp add: new_element_ptr_in_heap get_child_nodeselement_ptr_def check_in_heap_def
      new_element_child_nodes intro!: bind_pure_returns_result_I
      intro: new_element_is_element_ptr elim!: new_element_ptr_in_heap)[1]
proof -
  assume " h  new_element r new_element_ptr"
  assume "h  new_element h h'"
  assume "¬ is_shadow_root_ptrobject_ptr (castelement_ptr2object_ptr new_element_ptr)"
  assume "¬ known_ptrCore_DOM (castelement_ptr2object_ptr new_element_ptr)"
  moreover
  have "known_ptr (cast new_element_ptr)"
    using new_element_is_element_ptr h  new_element r new_element_ptr
    by(auto simp add: known_ptr_impl ShadowRootClass.a_known_ptr_def DocumentClass.a_known_ptr_def
        CharacterDataClass.a_known_ptr_def ElementClass.a_known_ptr_def)
  ultimately show "False"
    by(simp add: known_ptr_impl CD.known_ptr_impl ShadowRootClass.a_known_ptr_def is_document_ptr_kind_none)
qed
end

interpretation i_new_element_get_child_nodes?:
  l_new_element_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by(unfold_locales)
declare l_new_element_get_child_nodesShadow_DOM_axioms[instances]

lemma new_element_get_child_nodes_is_l_new_element_get_child_nodes [instances]:
  "l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  using new_element_is_l_new_element get_child_nodes_is_l_get_child_nodes
  apply(auto simp add: l_new_element_get_child_nodes_def l_new_element_get_child_nodes_axioms_def)[1]
  using get_child_nodes_new_element new_element_no_child_nodes
  by fast+


subsubsection ‹delete\_shadow\_root›

locale l_delete_shadow_root_get_child_nodesShadow_DOM =
  l_get_child_nodesShadow_DOM
begin
lemma get_child_nodes_delete_shadow_root:
  "ptr'  cast shadow_root_ptr  h  deleteShadowRoot_M shadow_root_ptr h h' 
r  get_child_nodes_locs ptr'  r h h'"
  by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def delete_shadow_root_get_MObject
      delete_shadow_root_get_MShadowRoot delete_shadow_root_get_MDocument delete_shadow_root_get_MElement
      split: if_splits  intro: is_shadow_root_ptr_kind_obtains
      intro: is_shadow_root_ptr_kind_obtains delete_shadow_root_get_MShadowRoot delete_shadow_root_get_MDocument
      simp add: shadow_root_ptr_casts_commute3 delete_shadow_root_get_MDocument
      intro!: delete_shadow_root_get_MDocument dest: document_ptr_casts_commute3
      split: option.splits)
end

locale l_delete_shadow_root_get_child_nodes = l_get_child_nodes_defs +
  assumes get_child_nodes_delete_shadow_root:
    "ptr'  cast shadow_root_ptr  h  deleteShadowRoot_M shadow_root_ptr h h' 
r  get_child_nodes_locs ptr'  r h h'"

interpretation l_delete_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by(auto simp add: l_delete_shadow_root_get_child_nodesShadow_DOM_def instances)

lemma l_delete_shadow_root_get_child_nodes_get_child_nodes_locs [instances]: "l_delete_shadow_root_get_child_nodes get_child_nodes_locs"
  apply(auto simp add: l_delete_shadow_root_get_child_nodes_def)[1]
  using get_child_nodes_delete_shadow_root apply fast
  done


subsubsection ‹set\_child\_nodes›

locale l_set_child_nodesShadow_DOM_defs =
  CD: l_set_child_nodesCore_DOM_defs
begin
definition set_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr  (_) node_ptr list
     (_, unit) dom_prog" where
  "set_child_nodesshadow_root_ptr shadow_root_ptr = put_M shadow_root_ptr RShadowRoot.child_nodes_update"

definition a_set_child_nodes_tups :: "(((_) object_ptr  bool) × ((_) object_ptr  (_) node_ptr list
     (_, unit) dom_prog)) list" where
  "a_set_child_nodes_tups  [(is_shadow_root_ptrobject_ptr, set_child_nodesshadow_root_ptr  the  cast)]"

definition a_set_child_nodes :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
    "a_set_child_nodes ptr children = invoke (CD.a_set_child_nodes_tups @ a_set_child_nodes_tups) ptr children"

definition a_set_child_nodes_locs :: "(_) object_ptr  (_, unit) dom_prog set"
  where
    "a_set_child_nodes_locs ptr 
      (if is_shadow_root_ptr_kind ptr then all_args (put_M (the (cast ptr)) RShadowRoot.child_nodes_update) else {}) 
      CD.a_set_child_nodes_locs ptr"
end

global_interpretation l_set_child_nodesShadow_DOM_defs defines
  set_child_nodes = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes and
  set_child_nodes_locs = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes_locs
  .

locale l_set_child_nodesShadow_DOM =
  l_type_wf type_wf +
  l_known_ptr known_ptr +
  l_set_child_nodesShadow_DOM_defs +
  l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
  CD: l_set_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and set_child_nodes :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
    and set_child_nodes_locs :: "(_) object_ptr  (_, unit) dom_prog set"
    and set_child_nodesCore_DOM :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
    and set_child_nodes_locsCore_DOM :: "(_) object_ptr  (_, unit) dom_prog set" +
  assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
  assumes set_child_nodes_impl: "set_child_nodes = a_set_child_nodes"
  assumes set_child_nodes_locs_impl: "set_child_nodes_locs = a_set_child_nodes_locs"
begin
lemmas set_child_nodes_def = set_child_nodes_impl[unfolded a_set_child_nodes_def set_child_nodes_def]
lemmas set_child_nodes_locs_def =set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def
    set_child_nodes_locs_def, folded CD.set_child_nodes_locs_impl]

lemma set_child_nodes_writes: "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
  apply (simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes_locs_def)
  apply(split CD.set_child_nodes_splits, rule conjI)+
   apply (simp add: CD.set_child_nodes_writes writes_union_right_I)
  apply(split invoke_splits, rule conjI)+
   apply(auto simp add: a_set_child_nodes_def)[1]
  apply(auto simp add: set_child_nodesshadow_root_ptr_def intro!: writes_bind_pure
      intro: writes_union_right_I writes_union_left_I split: list.splits)[1]
  by (metis is_shadow_root_ptr_implies_kind option.case_eq_if)

lemma set_child_nodes_pointers_preserved:
  assumes "w  set_child_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def split: if_splits)

lemma set_child_nodes_types_preserved:
  assumes "w  set_child_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)] type_wf_impl
  by(auto simp add: all_args_def a_set_child_nodes_tups_def set_child_nodes_locs_def CD.set_child_nodes_locs_def
      split: if_splits option.splits)
end

interpretation
  i_set_child_nodes?: l_set_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr set_child_nodes set_child_nodes_locs Core_DOM_Functions.set_child_nodes
  Core_DOM_Functions.set_child_nodes_locs
  apply(unfold_locales)
  by (auto simp add: set_child_nodes_def set_child_nodes_locs_def)
declare l_set_child_nodesShadow_DOM_axioms[instances]

lemma set_child_nodes_is_l_set_child_nodes [instances]: "l_set_child_nodes type_wf
set_child_nodes set_child_nodes_locs"
  apply(auto simp add: l_set_child_nodes_def instances)[1]
  using  set_child_nodes_writes apply fast
  using set_child_nodes_pointers_preserved apply(fast, fast)
  using set_child_nodes_types_preserved apply(fast, fast)
  done



paragraph ‹get\_child\_nodes›

locale l_set_child_nodes_get_child_nodesShadow_DOM =
  l_get_child_nodesShadow_DOM
  type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes get_child_nodes_locs
  get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
  + l_set_child_nodesShadow_DOM
  type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes set_child_nodes_locs
  set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
  + CD: l_set_child_nodes_get_child_nodesCore_DOM
  type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
  set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and get_child_nodes :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and get_child_nodesCore_DOM :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
    and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
    and set_child_nodesCore_DOM :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
    and set_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
begin

lemma set_child_nodes_get_child_nodes:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "h  set_child_nodes ptr children h h'"
  shows "h'  get_child_nodes ptr r children"
proof -
  have "h  check_in_heap ptr r ()"
    using assms set_child_nodes_def invoke_ptr_in_heap
    by (metis (full_types) check_in_heap_ptr_in_heap is_OK_returns_heap_I is_OK_returns_result_E
        old.unit.exhaust)
  then have ptr_in_h: "ptr |∈| object_ptr_kinds h"
    by (simp add: check_in_heap_ptr_in_heap is_OK_returns_result_I)

  have "type_wf h'"
    apply(unfold type_wf_impl)
    apply(rule subst[where P=id, OF type_wf_preserved[OF set_child_nodes_writes assms(3),
            unfolded all_args_def], simplified])
    by(auto simp add: all_args_def assms(2)[unfolded type_wf_impl] set_child_nodes_locs_def
        CD.set_child_nodes_locs_def split: if_splits)
  have "h'  check_in_heap ptr r ()"
    using check_in_heap_reads set_child_nodes_writes assms(3) h  check_in_heap ptr r ()
    apply(rule reads_writes_separate_forwards)
    apply(auto simp add: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def)[1]
    done
  then have "ptr |∈| object_ptr_kinds h'"
    using check_in_heap_ptr_in_heap by blast
  with assms ptr_in_h type_wf h' show ?thesis
    apply(auto simp add: type_wf_impl known_ptr_impl  get_child_nodes_def a_get_child_nodes_tups_def
        set_child_nodes_def a_set_child_nodes_tups_def del: bind_pure_returns_result_I2 intro!: bind_pure_returns_result_I2)[1]
    apply(split CD.get_child_nodes_splits, (rule conjI impI)+)+
     apply(split CD.set_child_nodes_splits)+
      apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
        dest: ShadowRootClass.type_wfDocument)[1]
     apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
        dest: ShadowRootClass.type_wfDocument)[1]
    apply(split CD.set_child_nodes_splits)+
    by(auto simp add: known_ptr_impl CD.known_ptr_impl set_child_nodesshadow_root_ptr_def
        get_child_nodesshadow_root_ptr_def CD.type_wf_impl ShadowRootClass.type_wfDocument dest: known_ptr_new_shadow_root_ptr)[2]
qed

lemma set_child_nodes_get_child_nodes_different_pointers:
  assumes "ptr  ptr'"
  assumes "w  set_child_nodes_locs ptr"
  assumes "h  w h h'"
  assumes "r  get_child_nodes_locs ptr'"
  shows "r h h'"
  using assms
  apply(auto simp add: set_child_nodes_locs_def CD.set_child_nodes_locs_def
      get_child_nodes_locs_def CD.get_child_nodes_locs_def)[1]
  by(auto simp add: all_args_def elim!: is_document_ptr_kind_obtains is_shadow_root_ptr_kind_obtains
      is_element_ptr_kind_obtains split: if_splits option.splits)

end

interpretation
  i_set_child_nodes_get_child_nodes?: l_set_child_nodes_get_child_nodesShadow_DOM type_wf known_ptr
  DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes get_child_nodes_locs
  Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs set_child_nodes
  set_child_nodes_locs Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs
  using instances
  by(auto simp add: l_set_child_nodes_get_child_nodesShadow_DOM_def )
declare l_set_child_nodes_get_child_nodesShadow_DOM_axioms[instances]

lemma set_child_nodes_get_child_nodes_is_l_set_child_nodes_get_child_nodes [instances]:
  "l_set_child_nodes_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs"
  apply(auto simp add: instances l_set_child_nodes_get_child_nodes_def l_set_child_nodes_get_child_nodes_axioms_def)[1]
  using set_child_nodes_get_child_nodes apply fast
  using set_child_nodes_get_child_nodes_different_pointers apply fast
  done


subsubsection ‹set\_tag\_type›

locale l_set_tag_nameShadow_DOM =
  CD: l_set_tag_nameCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs +
  l_type_wf type_wf
  for type_wf :: "(_) heap  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and set_tag_name :: "(_) element_ptr  tag_name  (_, unit) dom_prog"
    and set_tag_name_locs :: "(_) element_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemmas set_tag_name_def = CD.set_tag_name_impl[unfolded CD.a_set_tag_name_def set_tag_name_def]
lemmas set_tag_name_locs_def = CD.set_tag_name_locs_impl[unfolded CD.a_set_tag_name_locs_def
    set_tag_name_locs_def]

lemma set_tag_name_ok:
  "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_tag_name element_ptr tag)"
  apply(unfold type_wf_impl)
  unfolding set_tag_name_impl[unfolded a_set_tag_name_def] using get_MElement_ok put_MElement_ok
  using CD.set_tag_name_ok CD.type_wf_impl ShadowRootClass.type_wfDocument by blast

lemma set_tag_name_writes:
  "writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
  using CD.set_tag_name_writes .

lemma set_tag_name_pointers_preserved:
  assumes "w  set_tag_name_locs element_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms
  by(simp add: CD.set_tag_name_pointers_preserved)

lemma set_tag_name_typess_preserved:
  assumes "w  set_tag_name_locs element_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  apply(unfold type_wf_impl)
  apply(rule type_wf_preserved[OF writes_singleton2 assms(2)])
  using assms(1) set_tag_name_locs_def
  by(auto simp add: all_args_def set_tag_name_locs_def
      split: if_splits)
end

interpretation i_set_tag_name?: l_set_tag_nameShadow_DOM type_wf DocumentClass.type_wf set_tag_name
  set_tag_name_locs
  by(auto simp add: l_set_tag_nameShadow_DOM_def l_set_tag_nameShadow_DOM_axioms_def instances)
declare l_set_tag_nameShadow_DOM_axioms [instances]

lemma set_tag_name_is_l_set_tag_name [instances]: "l_set_tag_name type_wf set_tag_name set_tag_name_locs"
  apply(auto simp add: l_set_tag_name_def)[1]

  using set_tag_name_writes apply fast
  using set_tag_name_ok apply fast
  using set_tag_name_pointers_preserved apply (fast, fast)
  using set_tag_name_typess_preserved apply (fast, fast)
  done

paragraph ‹get\_child\_nodes›

locale l_set_tag_name_get_child_nodesShadow_DOM =
  l_set_tag_nameShadow_DOM +
  l_get_child_nodesShadow_DOM +
  CD: l_set_tag_name_get_child_nodesCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs
  known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
begin
lemma set_tag_name_get_child_nodes:
  "w  set_tag_name_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  apply(auto simp add: get_child_nodes_locs_def)[1]
    apply(auto simp add: set_tag_name_locs_def all_args_def)[1]
  using CD.set_tag_name_get_child_nodes apply(blast)
  using CD.set_tag_name_get_child_nodes apply(blast)
  done
end

interpretation
  i_set_tag_name_get_child_nodes?: l_set_tag_name_get_child_nodesShadow_DOM type_wf DocumentClass.type_wf
  set_tag_name set_tag_name_locs known_ptr DocumentClass.known_ptr get_child_nodes
  get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by unfold_locales
declare l_set_tag_name_get_child_nodesShadow_DOM_axioms[instances]

lemma set_tag_name_get_child_nodes_is_l_set_tag_name_get_child_nodes [instances]:
  "l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr get_child_nodes
                                         get_child_nodes_locs"
  using set_tag_name_is_l_set_tag_name get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_tag_name_get_child_nodes_def
      l_set_tag_name_get_child_nodes_axioms_def)
  using set_tag_name_get_child_nodes
  by fast


subsubsection ‹get\_shadow\_root›

locale l_get_shadow_rootShadow_DOM_defs
begin
definition a_get_shadow_root :: "(_) element_ptr  (_, (_) shadow_root_ptr option) dom_prog"
  where
    "a_get_shadow_root element_ptr = get_M element_ptr shadow_root_opt"

definition a_get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
  where
    "a_get_shadow_root_locs element_ptr  {preserved (get_M element_ptr shadow_root_opt)}"
end

global_interpretation l_get_shadow_rootShadow_DOM_defs
  defines get_shadow_root = a_get_shadow_root
    and get_shadow_root_locs = a_get_shadow_root_locs
  .

locale l_get_shadow_root_defs =
  fixes get_shadow_root :: "(_) element_ptr  (_, (_) shadow_root_ptr option) dom_prog"
  fixes get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"

locale l_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM_defs +
  l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
  l_type_wf type_wf
  for type_wf :: "(_) heap  bool"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set" +
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
  assumes get_shadow_root_impl: "get_shadow_root = a_get_shadow_root"
  assumes get_shadow_root_locs_impl: "get_shadow_root_locs = a_get_shadow_root_locs"
begin
lemmas get_shadow_root_def = get_shadow_root_impl[unfolded get_shadow_root_def a_get_shadow_root_def]
lemmas get_shadow_root_locs_def = get_shadow_root_locs_impl[unfolded get_shadow_root_locs_def a_get_shadow_root_locs_def]

lemma get_shadow_root_ok: "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_shadow_root element_ptr)"
  unfolding get_shadow_root_def type_wf_impl
  using ShadowRootMonad.get_MElement_ok by blast

lemma get_shadow_root_pure [simp]: "pure (get_shadow_root element_ptr) h"
  unfolding get_shadow_root_def by simp

lemma get_shadow_root_ptr_in_heap:
  assumes "h  get_shadow_root element_ptr r children"
  shows "element_ptr |∈| element_ptr_kinds h"
  using assms
  by(auto simp add: get_shadow_root_def get_MElement_ptr_in_heap dest: is_OK_returns_result_I)

lemma get_shadow_root_reads: "reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
  by(simp add: get_shadow_root_def get_shadow_root_locs_def reads_bind_pure reads_insert_writes_set_right)
end

interpretation i_get_shadow_root?: l_get_shadow_rootShadow_DOM type_wf  get_shadow_root get_shadow_root_locs
  using instances
  by (auto simp add: l_get_shadow_rootShadow_DOM_def)
declare l_get_shadow_rootShadow_DOM_axioms [instances]

locale l_get_shadow_root = l_type_wf + l_get_shadow_root_defs +
  assumes get_shadow_root_reads: "reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
  assumes get_shadow_root_ok: "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_shadow_root element_ptr)"
  assumes get_shadow_root_ptr_in_heap: "h  ok (get_shadow_root element_ptr)  element_ptr |∈| element_ptr_kinds h"
  assumes get_shadow_root_pure [simp]: "pure (get_shadow_root element_ptr) h"

lemma get_shadow_root_is_l_get_shadow_root [instances]: "l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
  using instances
  apply(auto simp add: l_get_shadow_root_def)[1]
  using get_shadow_root_reads apply blast
  using get_shadow_root_ok apply blast
  using get_shadow_root_ptr_in_heap apply blast
  done


paragraph ‹set\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_shadow_rootShadow_DOM =
  l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and set_disconnected_nodes :: "(_) document_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
    and set_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap, exception, unit) prog set"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma set_disconnected_nodes_get_shadow_root:
  "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"
  by(auto simp add: set_disconnected_nodes_locs_def get_shadow_root_locs_def all_args_def)
end

locale l_set_disconnected_nodes_get_shadow_root = l_set_disconnected_nodes_defs + l_get_shadow_root_defs +
  assumes set_disconnected_nodes_get_shadow_root: "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"

interpretation
  i_set_disconnected_nodes_get_shadow_root?: l_set_disconnected_nodes_get_shadow_rootShadow_DOM type_wf
  DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_shadow_root get_shadow_root_locs
  by(auto simp add: l_set_disconnected_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_shadow_rootShadow_DOM_axioms[instances]

lemma set_disconnected_nodes_get_shadow_root_is_l_set_disconnected_nodes_get_shadow_root [instances]:
  "l_set_disconnected_nodes_get_shadow_root set_disconnected_nodes_locs get_shadow_root_locs"
  apply(auto simp add: l_set_disconnected_nodes_get_shadow_root_def)[1]
  using set_disconnected_nodes_get_shadow_root apply fast
  done



paragraph ‹set\_tag\_type›

locale l_set_tag_name_get_shadow_rootCore_DOM =
  l_set_tag_nameShadow_DOM +
  l_get_shadow_rootShadow_DOM
begin
lemma set_tag_name_get_shadow_root:
  "w  set_tag_name_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"
  by(auto simp add: set_tag_name_locs_def
      get_shadow_root_locs_def all_args_def
      intro: element_put_get_preserved[where setter=tag_name_update and getter=shadow_root_opt])
end

locale l_set_tag_name_get_shadow_root = l_set_tag_name + l_get_shadow_root +
  assumes set_tag_name_get_shadow_root:
    "w  set_tag_name_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"

interpretation
  i_set_tag_name_get_shadow_root?: l_set_tag_name_get_shadow_rootCore_DOM type_wf DocumentClass.type_wf
  set_tag_name set_tag_name_locs
  get_shadow_root get_shadow_root_locs
  apply(auto simp add: l_set_tag_name_get_shadow_rootCore_DOM_def instances)[1]
  using l_set_tag_nameShadow_DOM_axioms
  by unfold_locales
declare l_set_tag_name_get_shadow_rootCore_DOM_axioms[instances]

lemma set_tag_name_get_shadow_root_is_l_set_tag_name_get_shadow_root [instances]:
  "l_set_tag_name_get_shadow_root type_wf set_tag_name set_tag_name_locs get_shadow_root
                                  get_shadow_root_locs"
  using set_tag_name_is_l_set_tag_name get_shadow_root_is_l_get_shadow_root
  apply(simp add: l_set_tag_name_get_shadow_root_def l_set_tag_name_get_shadow_root_axioms_def)
  using set_tag_name_get_shadow_root
  by fast


paragraph ‹set\_child\_nodes›

locale l_set_child_nodes_get_shadow_rootShadow_DOM =
  l_set_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes
  set_child_nodes_locs set_child_nodesCore_DOM set_child_nodes_locsCore_DOM +
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and known_ptr :: "(_) object_ptr  bool"
    and type_wfCore_DOM :: "(_) heap  bool"
    and known_ptrCore_DOM :: "(_) object_ptr  bool"
    and set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
    and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
    and set_child_nodesCore_DOM :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
    and set_child_nodes_locsCore_DOM :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma set_child_nodes_get_shadow_root: "w  set_child_nodes_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"
  apply(auto simp add: set_child_nodes_locs_def get_shadow_root_locs_def CD.set_child_nodes_locs_def all_args_def)[1]
  by(auto intro!: element_put_get_preserved[where getter=shadow_root_opt and setter=RElement.child_nodes_update])
end

locale l_set_child_nodes_get_shadow_root = l_set_child_nodes_defs + l_get_shadow_root_defs +
  assumes set_child_nodes_get_shadow_root: "w  set_child_nodes_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"

interpretation
  i_set_child_nodes_get_shadow_root?: l_set_child_nodes_get_shadow_rootShadow_DOM type_wf known_ptr
  DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
  Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_shadow_root
  get_shadow_root_locs
  by(auto simp add: l_set_child_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_child_nodes_get_shadow_rootShadow_DOM_axioms[instances]

lemma set_child_nodes_get_shadow_root_is_l_set_child_nodes_get_shadow_root [instances]:
  "l_set_child_nodes_get_shadow_root set_child_nodes_locs get_shadow_root_locs"
  apply(auto simp add: l_set_child_nodes_get_shadow_root_def)[1]
  using set_child_nodes_get_shadow_root apply fast
  done


paragraph ‹delete\_shadow\_root›

locale l_delete_shadow_root_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM
begin
lemma get_shadow_root_delete_shadow_root:  "h  deleteShadowRoot_M shadow_root_ptr h h'
     r  get_shadow_root_locs ptr'  r h h'"
  by(auto simp add: get_shadow_root_locs_def delete_shadow_root_get_MElement)
end

locale l_delete_shadow_root_get_shadow_root = l_get_shadow_root_defs +
  assumes get_shadow_root_delete_shadow_root:  "h  deleteShadowRoot_M shadow_root_ptr h h'
     r  get_shadow_root_locs ptr'  r h h'"
interpretation l_delete_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  by(auto simp add: l_delete_shadow_root_get_shadow_rootShadow_DOM_def instances)

lemma l_delete_shadow_root_get_shadow_root_get_shadow_root_locs [instances]: "l_delete_shadow_root_get_shadow_root get_shadow_root_locs"
  apply(auto simp add: l_delete_shadow_root_get_shadow_root_def)[1]
  using get_shadow_root_delete_shadow_root apply fast
  done



paragraph ‹new\_character\_data›

locale l_new_character_data_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_shadow_root_new_character_data:
  "h  new_character_data r new_character_data_ptr  h  new_character_data h h'
      r  get_shadow_root_locs ptr'  r h h'"
  by (auto simp add: get_shadow_root_locs_def new_character_data_get_MObject new_character_data_get_MElement
      split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end

locale l_new_character_data_get_shadow_root = l_new_character_data + l_get_shadow_root +
  assumes get_shadow_root_new_character_data:
    "h  new_character_data r new_character_data_ptr
             h  new_character_data h h'  r  get_shadow_root_locs ptr'  r h h'"


interpretation i_new_character_data_get_shadow_root?:
  l_new_character_data_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  by(unfold_locales)
declare l_new_character_data_get_shadow_rootShadow_DOM_axioms [instances]

lemma new_character_data_get_shadow_root_is_l_new_character_data_get_shadow_root [instances]:
  "l_new_character_data_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
  using new_character_data_is_l_new_character_data get_shadow_root_is_l_get_shadow_root
  apply(auto simp add: l_new_character_data_get_shadow_root_def
      l_new_character_data_get_shadow_root_axioms_def instances)[1]
  using get_shadow_root_new_character_data
  by fast






paragraph ‹new\_document›

locale l_new_document_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_shadow_root_new_document:
  "h  new_document r new_document_ptr  h  new_document h h'
      r  get_shadow_root_locs ptr'  r h h'"
  by (auto simp add: get_shadow_root_locs_def new_document_get_MObject new_document_get_MElement
      split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end

locale l_new_document_get_shadow_root = l_new_document + l_get_shadow_root +
  assumes get_shadow_root_new_document:
    "h  new_document r new_document_ptr
             h  new_document h h'  r  get_shadow_root_locs ptr'  r h h'"


interpretation i_new_document_get_shadow_root?:
  l_new_document_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  by(unfold_locales)
declare l_new_document_get_shadow_rootShadow_DOM_axioms [instances]

lemma new_document_get_shadow_root_is_l_new_document_get_shadow_root [instances]:
  "l_new_document_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
  using new_document_is_l_new_document get_shadow_root_is_l_get_shadow_root
  apply(auto simp add: l_new_document_get_shadow_root_def l_new_document_get_shadow_root_axioms_def instances)[1]
  using get_shadow_root_new_document
  by fast




paragraph ‹new\_element›

locale l_new_element_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_shadow_root_new_element:
  "ptr'  new_element_ptr  h  new_element r new_element_ptr  h  new_element h h'
      r  get_shadow_root_locs ptr'  r h h'"
  by (auto simp add: get_shadow_root_locs_def new_element_get_MObject new_element_get_MElement
      new_element_get_MDocument split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)

lemma new_element_no_shadow_root:
  "h  new_element r new_element_ptr  h  new_element h h'
    h'  get_shadow_root new_element_ptr r None"
  by(simp add: get_shadow_root_def new_element_shadow_root_opt)
end

locale l_new_element_get_shadow_root = l_new_element + l_get_shadow_root +
  assumes get_shadow_root_new_element:
    "ptr'  new_element_ptr  h  new_element r new_element_ptr
             h  new_element h h'  r  get_shadow_root_locs ptr'  r h h'"
  assumes new_element_no_shadow_root:
    "h  new_element r new_element_ptr  h  new_element h h'
             h'  get_shadow_root new_element_ptr r None"


interpretation i_new_element_get_shadow_root?:
  l_new_element_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  by(unfold_locales)
declare l_new_element_get_shadow_rootShadow_DOM_axioms [instances]

lemma new_element_get_shadow_root_is_l_new_element_get_shadow_root [instances]:
  "l_new_element_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
  using new_element_is_l_new_element get_shadow_root_is_l_get_shadow_root
  apply(auto simp add: l_new_element_get_shadow_root_def l_new_element_get_shadow_root_axioms_def instances)[1]
  using get_shadow_root_new_element new_element_no_shadow_root
  by fast+

paragraph ‹new\_shadow\_root›

locale l_new_shadow_root_get_shadow_rootShadow_DOM =
  l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  for type_wf :: "(_) heap  bool"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
lemma get_shadow_root_new_shadow_root:
  "h  newShadowRoot_M r new_shadow_root_ptr  h  newShadowRoot_M h h'
      r  get_shadow_root_locs ptr'  r h h'"
  by (auto simp add: get_shadow_root_locs_def new_shadow_root_get_MObject new_shadow_root_get_MElement
      split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end

locale l_new_shadow_root_get_shadow_root = l_get_shadow_root +
  assumes get_shadow_root_new_shadow_root:
    "h  newShadowRoot_M r new_shadow_root_ptr
             h  newShadowRoot_M h h'  r  get_shadow_root_locs ptr'  r h h'"

interpretation i_new_shadow_root_get_shadow_root?:
  l_new_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
  by(unfold_locales)
declare l_new_shadow_root_get_shadow_rootShadow_DOM_axioms [instances]

lemma new_shadow_root_get_shadow_root_is_l_new_shadow_root_get_shadow_root [instances]:
  "l_new_shadow_root_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
  using get_shadow_root_is_l_get_shadow_root
  apply(auto simp add: l_new_shadow_root_get_shadow_root_def l_new_shadow_root_get_shadow_root_axioms_def instances)[1]
  using get_shadow_root_new_shadow_root
  by fast


subsubsection ‹set\_shadow\_root›

locale l_set_shadow_rootShadow_DOM_defs
begin
definition a_set_shadow_root :: "(_) element_ptr  (_) shadow_root_ptr option  (_, unit) dom_prog"
  where
    "a_set_shadow_root element_ptr = put_M element_ptr shadow_root_opt_update"

definition a_set_shadow_root_locs :: "(_) element_ptr  ((_, unit) dom_prog) set"
  where
    "a_set_shadow_root_locs element_ptr  all_args (put_M element_ptr shadow_root_opt_update)"
end

global_interpretation l_set_shadow_rootShadow_DOM_defs
  defines set_shadow_root = a_set_shadow_root
    and set_shadow_root_locs = a_set_shadow_root_locs
  .

locale l_set_shadow_root_defs =
  fixes set_shadow_root :: "(_) element_ptr  (_) shadow_root_ptr option  (_, unit) dom_prog"
  fixes set_shadow_root_locs :: "(_) element_ptr  (_, unit) dom_prog set"


locale l_set_shadow_rootShadow_DOM =
  l_type_wf type_wf +
  l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
  l_set_shadow_rootShadow_DOM_defs
  for type_wf :: "(_) heap  bool"
    and set_shadow_root :: "(_) element_ptr  (_) shadow_root_ptr option  (_, unit) dom_prog"
    and set_shadow_root_locs :: "(_) element_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
  assumes set_shadow_root_impl: "set_shadow_root = a_set_shadow_root"
  assumes set_shadow_root_locs_impl: "set_shadow_root_locs = a_set_shadow_root_locs"
begin
lemmas set_shadow_root_def = set_shadow_root_impl[unfolded set_shadow_root_def a_set_shadow_root_def]
lemmas set_shadow_root_locs_def = set_shadow_root_locs_impl[unfolded set_shadow_root_locs_def a_set_shadow_root_locs_def]

lemma set_shadow_root_ok: "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_shadow_root element_ptr tag)"
  apply(unfold type_wf_impl)
  unfolding set_shadow_root_def using get_MElement_ok put_MElement_ok
  by (simp add: ShadowRootMonad.put_MElement_ok)

lemma set_shadow_root_ptr_in_heap:
  "h  ok (set_shadow_root element_ptr shadow_root)  element_ptr |∈| element_ptr_kinds h"
  by(simp add: set_shadow_root_def ElementMonad.put_M_ptr_in_heap)

lemma set_shadow_root_writes: "writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr tag) h h'"
  by(auto simp add: set_shadow_root_def set_shadow_root_locs_def intro: writes_bind_pure)

lemma set_shadow_root_pointers_preserved:
  assumes "w  set_shadow_root_locs element_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_shadow_root_locs_def split: if_splits)

lemma set_shadow_root_types_preserved:
  assumes "w  set_shadow_root_locs element_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  apply(unfold type_wf_impl)
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_shadow_root_locs_def split: if_splits)
end

interpretation i_set_shadow_root?: l_set_shadow_rootShadow_DOM type_wf set_shadow_root set_shadow_root_locs
  by (auto simp add: l_set_shadow_rootShadow_DOM_def instances)
declare l_set_shadow_rootShadow_DOM_axioms [instances]

locale l_set_shadow_root = l_type_wf +l_set_shadow_root_defs +
  assumes set_shadow_root_writes:
    "writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr disc_nodes) h h'"
  assumes set_shadow_root_ok:
    "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_shadow_root element_ptr shadow_root)"
  assumes set_shadow_root_ptr_in_heap:
    "h  ok (set_shadow_root element_ptr shadow_root)  element_ptr |∈| element_ptr_kinds h"
  assumes set_shadow_root_pointers_preserved:
    "w  set_shadow_root_locs element_ptr  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes set_shadow_root_types_preserved:
    "w  set_shadow_root_locs element_ptr  h  w h h'  type_wf h = type_wf h'"

lemma set_shadow_root_is_l_set_shadow_root [instances]: "l_set_shadow_root type_wf set_shadow_root set_shadow_root_locs"
  apply(auto simp add: l_set_shadow_root_def instances)[1]
  using set_shadow_root_writes apply blast
  using set_shadow_root_ok apply (blast)
  using set_shadow_root_ptr_in_heap apply blast
  using set_shadow_root_pointers_preserved apply(blast, blast)
  using set_shadow_root_types_preserved apply(blast, blast)
  done

paragraph ‹get\_shadow\_root›

locale l_set_shadow_root_get_shadow_rootShadow_DOM =
  l_set_shadow_rootShadow_DOM +
  l_get_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_shadow_root:
  "type_wf h  h  set_shadow_root ptr shadow_root_ptr_opt h h' 
h'  get_shadow_root ptr r shadow_root_ptr_opt"
  by(auto simp add: set_shadow_root_def get_shadow_root_def)

lemma set_shadow_root_get_shadow_root_different_pointers:
  "ptr  ptr'  w  set_shadow_root_locs ptr.
(h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"
  by(auto simp add: set_shadow_root_locs_def get_shadow_root_locs_def all_args_def)
end

interpretation
  i_set_shadow_root_get_shadow_root?: l_set_shadow_root_get_shadow_rootShadow_DOM type_wf
  set_shadow_root set_shadow_root_locs get_shadow_root get_shadow_root_locs
  apply(auto simp add: l_set_shadow_root_get_shadow_rootShadow_DOM_def instances)[1]
  by(unfold_locales)
declare l_set_shadow_root_get_shadow_rootShadow_DOM_axioms[instances]

locale l_set_shadow_root_get_shadow_root = l_type_wf + l_set_shadow_root_defs + l_get_shadow_root_defs +
  assumes set_shadow_root_get_shadow_root:
    "type_wf h  h  set_shadow_root ptr shadow_root_ptr_opt h h' 
h'  get_shadow_root ptr r shadow_root_ptr_opt"
  assumes set_shadow_root_get_shadow_root_different_pointers:
    "ptr  ptr'  w  set_shadow_root_locs ptr  h  w h h'  r  get_shadow_root_locs ptr' 
r h h'"

lemma set_shadow_root_get_shadow_root_is_l_set_shadow_root_get_shadow_root [instances]:
  "l_set_shadow_root_get_shadow_root type_wf set_shadow_root set_shadow_root_locs get_shadow_root
get_shadow_root_locs"
  apply(auto simp add: l_set_shadow_root_get_shadow_root_def instances)[1]
  using set_shadow_root_get_shadow_root apply fast
  using set_shadow_root_get_shadow_root_different_pointers apply fast
  done


subsubsection ‹set\_mode›

locale l_set_modeShadow_DOM_defs
begin
definition a_set_mode :: "(_) shadow_root_ptr  shadow_root_mode  (_, unit) dom_prog"
  where
    "a_set_mode shadow_root_ptr = put_M shadow_root_ptr mode_update"

definition a_set_mode_locs :: "(_) shadow_root_ptr  ((_, unit) dom_prog) set"
  where
    "a_set_mode_locs shadow_root_ptr  all_args (put_M shadow_root_ptr mode_update)"
end

global_interpretation l_set_modeShadow_DOM_defs
  defines set_mode = a_set_mode
    and set_mode_locs = a_set_mode_locs
  .

locale l_set_mode_defs =
  fixes set_mode :: "(_) shadow_root_ptr  shadow_root_mode  (_, unit) dom_prog"
  fixes set_mode_locs :: "(_) shadow_root_ptr  (_, unit) dom_prog set"


locale l_set_modeShadow_DOM =
  l_type_wf type_wf +
  l_set_mode_defs set_mode set_mode_locs +
  l_set_modeShadow_DOM_defs
  for type_wf :: "(_) heap  bool"
    and set_mode :: "(_) shadow_root_ptr  shadow_root_mode  (_, unit) dom_prog"
    and set_mode_locs :: "(_) shadow_root_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
  assumes set_mode_impl: "set_mode = a_set_mode"
  assumes set_mode_locs_impl: "set_mode_locs = a_set_mode_locs"
begin
lemmas set_mode_def = set_mode_impl[unfolded set_mode_def a_set_mode_def]
lemmas set_mode_locs_def = set_mode_locs_impl[unfolded set_mode_locs_def a_set_mode_locs_def]

lemma set_mode_ok: "type_wf h  shadow_root_ptr |∈| shadow_root_ptr_kinds h 
h  ok (set_mode shadow_root_ptr shadow_root_mode)"
  apply(unfold type_wf_impl)
  unfolding set_mode_def using get_MShadowRoot_ok put_MShadowRoot_ok
  by (simp add: ShadowRootMonad.put_MShadowRoot_ok)

lemma set_mode_ptr_in_heap:
  "h  ok (set_mode shadow_root_ptr shadow_root_mode)  shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  by(simp add: set_mode_def put_M_ptr_in_heap)

lemma set_mode_writes: "writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
  by(auto simp add: set_mode_def set_mode_locs_def intro: writes_bind_pure)

lemma set_mode_pointers_preserved:
  assumes "w  set_mode_locs element_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_mode_locs_def split: if_splits)

lemma set_mode_types_preserved:
  assumes "w  set_mode_locs element_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  apply(unfold type_wf_impl)
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_mode_locs_def split: if_splits)
end

interpretation i_set_mode?: l_set_modeShadow_DOM type_wf set_mode set_mode_locs
  by (auto simp add: l_set_modeShadow_DOM_def instances)
declare l_set_modeShadow_DOM_axioms [instances]

locale l_set_mode = l_type_wf +l_set_mode_defs +
  assumes set_mode_writes:
    "writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
  assumes set_mode_ok:
    "type_wf h  shadow_root_ptr |∈| shadow_root_ptr_kinds h  h  ok (set_mode shadow_root_ptr shadow_root_mode)"
  assumes set_mode_ptr_in_heap:
    "h  ok (set_mode shadow_root_ptr shadow_root_mode)  shadow_root_ptr |∈| shadow_root_ptr_kinds h"
  assumes set_mode_pointers_preserved:
    "w  set_mode_locs shadow_root_ptr  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes set_mode_types_preserved:
    "w  set_mode_locs shadow_root_ptr  h  w h h'  type_wf h = type_wf h'"

lemma set_mode_is_l_set_mode [instances]: "l_set_mode type_wf set_mode set_mode_locs"
  apply(auto simp add: l_set_mode_def instances)[1]
  using set_mode_writes apply blast
  using set_mode_ok apply (blast)
  using set_mode_ptr_in_heap apply blast
  using set_mode_pointers_preserved apply(blast, blast)
  using set_mode_types_preserved apply(blast, blast)
  done


paragraph ‹get\_child\_nodes›

locale l_set_shadow_root_get_child_nodesShadow_DOM =
  l_get_child_nodesShadow_DOM +
  l_set_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_child_nodes:
  "w  set_shadow_root_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: get_child_nodes_locs_def set_shadow_root_locs_def CD.get_child_nodes_locs_def
      all_args_def intro: element_put_get_preserved[where setter=shadow_root_opt_update])
end

interpretation i_set_shadow_root_get_child_nodes?:
  l_set_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs set_shadow_root set_shadow_root_locs
  by(unfold_locales)
declare l_set_shadow_root_get_child_nodesShadow_DOM_axioms[instances]

locale l_set_shadow_root_get_child_nodes = l_set_shadow_root + l_get_child_nodes +
  assumes set_shadow_root_get_child_nodes:
    "w  set_shadow_root_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

lemma set_shadow_root_get_child_nodes_is_l_set_shadow_root_get_child_nodes [instances]:
  "l_set_shadow_root_get_child_nodes type_wf set_shadow_root set_shadow_root_locs known_ptr
get_child_nodes get_child_nodes_locs"
  apply(auto simp add: l_set_shadow_root_get_child_nodes_def l_set_shadow_root_get_child_nodes_axioms_def
      instances)[1]
  using set_shadow_root_get_child_nodes apply blast
  done

paragraph ‹get\_shadow\_root›

locale l_set_mode_get_shadow_rootShadow_DOM =
  l_set_modeShadow_DOM +
  l_get_shadow_rootShadow_DOM
begin
lemma set_mode_get_shadow_root:
  "w  set_mode_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"
  by(auto simp add: set_mode_locs_def get_shadow_root_locs_def all_args_def)
end

interpretation
  i_set_mode_get_shadow_root?: l_set_mode_get_shadow_rootShadow_DOM type_wf
  set_mode set_mode_locs get_shadow_root
  get_shadow_root_locs
  by unfold_locales
declare l_set_mode_get_shadow_rootShadow_DOM_axioms[instances]

locale l_set_mode_get_shadow_root = l_set_mode + l_get_shadow_root +
  assumes set_mode_get_shadow_root:
    "w  set_mode_locs ptr. (h  w h h'  (r  get_shadow_root_locs ptr'. r h h'))"

lemma set_mode_get_shadow_root_is_l_set_mode_get_shadow_root [instances]:
  "l_set_mode_get_shadow_root type_wf set_mode set_mode_locs get_shadow_root
                                         get_shadow_root_locs"
  using set_mode_is_l_set_mode get_shadow_root_is_l_get_shadow_root
  apply(simp add: l_set_mode_get_shadow_root_def
      l_set_mode_get_shadow_root_axioms_def)
  using set_mode_get_shadow_root
  by fast

paragraph ‹get\_child\_nodes›

locale l_set_mode_get_child_nodesShadow_DOM =
  l_set_modeShadow_DOM +
  l_get_child_nodesShadow_DOM
begin
lemma set_mode_get_child_nodes:
  "w  set_mode_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def set_mode_locs_def all_args_def)[1]
end

interpretation
  i_set_mode_get_child_nodes?: l_set_mode_get_child_nodesShadow_DOM type_wf set_mode set_mode_locs known_ptr DocumentClass.type_wf
  DocumentClass.known_ptr get_child_nodes
  get_child_nodes_locs Core_DOM_Functions.get_child_nodes
  Core_DOM_Functions.get_child_nodes_locs
  by unfold_locales
declare l_set_mode_get_child_nodesShadow_DOM_axioms[instances]

locale l_set_mode_get_child_nodes = l_set_mode + l_get_child_nodes +
  assumes set_mode_get_child_nodes:
    "w  set_mode_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

lemma set_mode_get_child_nodes_is_l_set_mode_get_child_nodes [instances]:
  "l_set_mode_get_child_nodes type_wf set_mode set_mode_locs known_ptr get_child_nodes
                                         get_child_nodes_locs"
  using set_mode_is_l_set_mode get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_mode_get_child_nodes_def
      l_set_mode_get_child_nodes_axioms_def)
  using set_mode_get_child_nodes
  by fast


subsubsection ‹get\_host›

locale l_get_hostShadow_DOM_defs =
  l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
  for get_shadow_root :: "(_::linorder) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
definition a_get_host :: "(_) shadow_root_ptr  (_, (_) elemen