diff --git a/thys/Core_DOM/ROOT b/thys/Core_DOM/ROOT
--- a/thys/Core_DOM/ROOT
+++ b/thys/Core_DOM/ROOT
@@ -1,16 +1,20 @@
 chapter AFP
 
 session "Core_DOM" (AFP) = "HOL-Library" + 
   options [timeout = 1200]
   directories
-    "classes"
-    "monads"
-    "pointers"
-    "preliminaries"
-    "tests"
+    "common"
+    "common/classes"
+    "common/monads"
+    "common/pointers"
+    "common/preliminaries"
+    "common/tests"
+    "standard" 
+    "standard/classes" 
+    "standard/pointers" 
   theories
     Core_DOM
     Core_DOM_Tests
-  document_files
+  document_files (in "document")
     "root.tex"
     "root.bib"
diff --git a/thys/Core_DOM/Core_DOM.thy b/thys/Core_DOM/common/Core_DOM.thy
rename from thys/Core_DOM/Core_DOM.thy
rename to thys/Core_DOM/common/Core_DOM.thy
diff --git a/thys/Core_DOM/Core_DOM_Basic_Datatypes.thy b/thys/Core_DOM/common/Core_DOM_Basic_Datatypes.thy
rename from thys/Core_DOM/Core_DOM_Basic_Datatypes.thy
rename to thys/Core_DOM/common/Core_DOM_Basic_Datatypes.thy
diff --git a/thys/Core_DOM/Core_DOM_Functions.thy b/thys/Core_DOM/common/Core_DOM_Functions.thy
rename from thys/Core_DOM/Core_DOM_Functions.thy
rename to thys/Core_DOM/common/Core_DOM_Functions.thy
diff --git a/thys/Core_DOM/Core_DOM_Tests.thy b/thys/Core_DOM/common/Core_DOM_Tests.thy
rename from thys/Core_DOM/Core_DOM_Tests.thy
rename to thys/Core_DOM/common/Core_DOM_Tests.thy
diff --git a/thys/Core_DOM/classes/BaseClass.thy b/thys/Core_DOM/common/classes/BaseClass.thy
rename from thys/Core_DOM/classes/BaseClass.thy
rename to thys/Core_DOM/common/classes/BaseClass.thy
diff --git a/thys/Core_DOM/classes/CharacterDataClass.thy b/thys/Core_DOM/common/classes/CharacterDataClass.thy
rename from thys/Core_DOM/classes/CharacterDataClass.thy
rename to thys/Core_DOM/common/classes/CharacterDataClass.thy
diff --git a/thys/Core_DOM/classes/DocumentClass.thy b/thys/Core_DOM/common/classes/DocumentClass.thy
rename from thys/Core_DOM/classes/DocumentClass.thy
rename to thys/Core_DOM/common/classes/DocumentClass.thy
diff --git a/thys/Core_DOM/classes/NodeClass.thy b/thys/Core_DOM/common/classes/NodeClass.thy
rename from thys/Core_DOM/classes/NodeClass.thy
rename to thys/Core_DOM/common/classes/NodeClass.thy
diff --git a/thys/Core_DOM/classes/ObjectClass.thy b/thys/Core_DOM/common/classes/ObjectClass.thy
rename from thys/Core_DOM/classes/ObjectClass.thy
rename to thys/Core_DOM/common/classes/ObjectClass.thy
diff --git a/thys/Core_DOM/monads/BaseMonad.thy b/thys/Core_DOM/common/monads/BaseMonad.thy
rename from thys/Core_DOM/monads/BaseMonad.thy
rename to thys/Core_DOM/common/monads/BaseMonad.thy
diff --git a/thys/Core_DOM/monads/CharacterDataMonad.thy b/thys/Core_DOM/common/monads/CharacterDataMonad.thy
rename from thys/Core_DOM/monads/CharacterDataMonad.thy
rename to thys/Core_DOM/common/monads/CharacterDataMonad.thy
diff --git a/thys/Core_DOM/monads/DocumentMonad.thy b/thys/Core_DOM/common/monads/DocumentMonad.thy
rename from thys/Core_DOM/monads/DocumentMonad.thy
rename to thys/Core_DOM/common/monads/DocumentMonad.thy
diff --git a/thys/Core_DOM/monads/ElementMonad.thy b/thys/Core_DOM/common/monads/ElementMonad.thy
rename from thys/Core_DOM/monads/ElementMonad.thy
rename to thys/Core_DOM/common/monads/ElementMonad.thy
--- a/thys/Core_DOM/monads/ElementMonad.thy
+++ b/thys/Core_DOM/common/monads/ElementMonad.thy
@@ -1,457 +1,457 @@
 (***********************************************************************************
  * Copyright (c) 2016-2018 The University of Sheffield, UK
  *
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
  *
  * * Redistributions of source code must retain the above copyright notice, this
  *   list of conditions and the following disclaimer.
  *
  * * Redistributions in binary form must reproduce the above copyright notice,
  *   this list of conditions and the following disclaimer in the documentation
  *   and/or other materials provided with the distribution.
  *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  * 
  * SPDX-License-Identifier: BSD-2-Clause
  ***********************************************************************************)
 
 section\<open>Element\<close>
 text\<open>In this theory, we introduce the monadic method setup for the Element class.\<close>
 theory ElementMonad
   imports
     NodeMonad
-    "../classes/ElementClass"
+    "ElementClass"
 begin
 
 type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 
     'shadow_root_ptr, 'Object, 'Node, 'Element,'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,'result) dom_prog" 
 
 
 global_interpretation l_ptr_kinds_M element_ptr_kinds defines element_ptr_kinds_M = a_ptr_kinds_M .
 lemmas element_ptr_kinds_M_defs = a_ptr_kinds_M_def
 
 
 lemma element_ptr_kinds_M_eq:
   assumes "|h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
   shows "|h \<turnstile> element_ptr_kinds_M|\<^sub>r = |h' \<turnstile> element_ptr_kinds_M|\<^sub>r"
   using assms 
   by(auto simp add: element_ptr_kinds_M_defs node_ptr_kinds_M_defs element_ptr_kinds_def)
 
 lemma element_ptr_kinds_M_reads: 
   "reads (\<Union>element_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
   apply (simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
     node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
   apply (metis (mono_tags, hide_lams) node_ptr_kinds_small old.unit.exhaust preserved_def)
   done
 
 global_interpretation l_dummy defines get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = "l_get_M.a_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" .
 lemma get_M_is_l_get_M: "l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds"
   apply(simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf l_get_M_def)
   by (metis (no_types, lifting) ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf ObjectClass.type_wf_defs 
       bind_eq_Some_conv bind_eq_Some_conv element_ptr_kinds_commutes get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def node_ptr_kinds_commutes option.simps(3))
 lemmas get_M_defs = get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]
 
 adhoc_overloading get_M get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 
 locale l_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas = l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 begin
 sublocale l_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas by unfold_locales
 
 interpretation l_get_M get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf element_ptr_kinds
   apply(unfold_locales)
    apply (simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf local.type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t)
   by (meson ElementMonad.get_M_is_l_get_M l_get_M_def)
 lemmas get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok = get_M_ok[folded get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def]
 lemmas get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap = get_M_ptr_in_heap[folded get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def]
 end
 
 global_interpretation l_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf by unfold_locales
 
 
 global_interpretation l_put_M type_wf element_ptr_kinds get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t 
   rewrites "a_get_M = get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t" 
   defines put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = a_put_M
    apply (simp add: get_M_is_l_get_M l_put_M_def)
   by (simp add: get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
 
 lemmas put_M_defs = a_put_M_def
 adhoc_overloading put_M put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 
 
 locale l_put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas = l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 begin
 sublocale l_put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas by unfold_locales
 
 interpretation l_put_M type_wf element_ptr_kinds get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
   apply(unfold_locales)
    apply (simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf local.type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t)
   by (meson ElementMonad.get_M_is_l_get_M l_get_M_def)
 
 lemmas put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ok = put_M_ok[folded put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def]
 end
 
 global_interpretation l_put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf by unfold_locales
 
 
 lemma element_put_get [simp]: 
   "h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow> (\<And>x. getter (setter (\<lambda>_. v) x) = v) 
   \<Longrightarrow> h' \<turnstile> get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr getter \<rightarrow>\<^sub>r v"
   by(auto simp add: put_M_defs get_M_defs split: option.splits)
 lemma get_M_Element_preserved1 [simp]: 
   "element_ptr \<noteq> element_ptr' \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
      \<Longrightarrow> preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr' getter) h h'"
   by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)
 lemma element_put_get_preserved [simp]: 
   "(\<And>x. getter (setter (\<lambda>_. v) x) = getter x) \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr' getter) h h'"
   apply(cases "element_ptr = element_ptr'") 
   by(auto simp add: put_M_defs get_M_defs preserved_def 
       split: option.splits dest: get_heap_E)
 lemma  get_M_Element_preserved3 [simp]: 
   "(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) 
     \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
   apply(cases "cast element_ptr = object_ptr") 
   by (auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def bind_eq_Some_conv 
       split: option.splits)
 lemma  get_M_Element_preserved4 [simp]: 
   "(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) 
      \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr getter) h h'"
   apply(cases "cast element_ptr = node_ptr") 
   by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def bind_eq_Some_conv 
       split: option.splits)
 
 lemma  get_M_Element_preserved5 [simp]: 
   "cast element_ptr \<noteq> node_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
   \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr getter) h h'"
   by(auto simp add: put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def NodeMonad.get_M_defs preserved_def 
       split: option.splits dest: get_heap_E)
 lemma  get_M_Element_preserved6 [simp]: 
   "h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) 
     \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr getter) h h'"
   apply(cases "cast element_ptr \<noteq> node_ptr")
   by(auto simp add: put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def NodeMonad.get_M_defs preserved_def 
       split: option.splits bind_splits dest: get_heap_E)
 
 lemma  get_M_Element_preserved7 [simp]: 
   "cast element_ptr \<noteq> node_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr getter) h h'"
   by(auto simp add: NodeMonad.put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def NodeMonad.get_M_defs preserved_def 
       split: option.splits dest: get_heap_E)
 
 lemma  get_M_Element_preserved8 [simp]: 
   "cast element_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
   by(auto simp add: put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       ObjectMonad.get_M_defs preserved_def 
       split: option.splits dest: get_heap_E)
 lemma  get_M_Element_preserved9 [simp]: 
   "h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) 
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
   apply(cases "cast element_ptr \<noteq> object_ptr")
   by(auto simp add: put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def 
       ObjectMonad.get_M_defs preserved_def 
       split: option.splits bind_splits dest: get_heap_E)
 
 lemma  get_M_Element_preserved10 [simp]: 
   "cast element_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr setter v \<rightarrow>\<^sub>h h' 
     \<Longrightarrow> preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr getter) h h'"
   by(auto simp add: ObjectMonad.put_M_defs get_M_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def 
       ObjectMonad.get_M_defs preserved_def 
       split: option.splits dest: get_heap_E)
 
 subsection\<open>Creating Elements\<close>
 
 definition new_element :: "(_, (_) element_ptr) dom_prog"
   where
     "new_element = do {
       h \<leftarrow> get_heap;
       (new_ptr, h') \<leftarrow> return (new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h);
       return_heap h';
       return new_ptr
     }"
 
 lemma new_element_ok [simp]:
   "h \<turnstile> ok new_element"
   by(auto simp add: new_element_def split: prod.splits)
 
 lemma new_element_ptr_in_heap:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
     and "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "new_element_ptr |\<in>| element_ptr_kinds h'"
   using assms
   unfolding new_element_def
   by(auto simp add: new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap is_OK_returns_result_I
       elim!: bind_returns_result_E bind_returns_heap_E)
 
 lemma new_element_ptr_not_in_heap:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
     and "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "new_element_ptr |\<notin>| element_ptr_kinds h"
   using assms new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap
   by(auto simp add: new_element_def split: prod.splits elim!: bind_returns_result_E 
       bind_returns_heap_E)
 
 lemma new_element_new_ptr:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
     and "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_element_ptr|}"
   using assms new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_new_ptr
   by(auto simp add: new_element_def split: prod.splits elim!: bind_returns_result_E 
       bind_returns_heap_E)
 
 lemma new_element_is_element_ptr:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "is_element_ptr new_element_ptr"
   using assms new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_is_element_ptr
   by(auto simp add: new_element_def elim!: bind_returns_result_E split: prod.splits)
 
 lemma new_element_child_nodes:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "h' \<turnstile> get_M new_element_ptr child_nodes \<rightarrow>\<^sub>r []"
   using assms
   by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def 
       split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
 
 lemma new_element_tag_type:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "h' \<turnstile> get_M new_element_ptr tag_type \<rightarrow>\<^sub>r ''''"
   using assms
   by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def 
       split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
 
 lemma new_element_attrs:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "h' \<turnstile> get_M new_element_ptr attrs \<rightarrow>\<^sub>r fmempty"
   using assms
   by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def 
       split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
 
 lemma new_element_shadow_root_opt:
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
   assumes "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr"
   shows "h' \<turnstile> get_M new_element_ptr shadow_root_opt \<rightarrow>\<^sub>r None"
   using assms
   by(auto simp add: get_M_defs new_element_def new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def 
       split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)
 
 lemma new_element_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t: 
   "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> ptr \<noteq> cast new_element_ptr 
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
   by(auto simp add: new_element_def ObjectMonad.get_M_defs preserved_def 
       split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
 lemma new_element_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e: 
   "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> ptr \<noteq> cast new_element_ptr 
     \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr getter) h h'"
   by(auto simp add: new_element_def NodeMonad.get_M_defs preserved_def 
       split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
 lemma new_element_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t: 
   "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> ptr \<noteq> new_element_ptr 
     \<Longrightarrow> preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr getter) h h'"
   by(auto simp add: new_element_def get_M_defs preserved_def 
       split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
 
 subsection\<open>Modified Heaps\<close>
 
 lemma get_Element_ptr_simp [simp]: 
   "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) 
       = (if ptr = cast element_ptr then cast obj else get element_ptr h)"
   by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def split: option.splits Option.bind_splits)
 
 
 lemma element_ptr_kinds_simp [simp]: 
   "element_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) 
       = element_ptr_kinds h |\<union>| (if is_element_ptr_kind ptr then {|the (cast ptr)|} else {||})"
   by(auto simp add: element_ptr_kinds_def is_node_ptr_kind_def split: option.splits)
 
 lemma type_wf_put_I:
   assumes "type_wf h"
   assumes "NodeClass.type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
   assumes "is_element_ptr_kind ptr \<Longrightarrow> is_element_kind obj"
   shows "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
   using assms
   by(auto simp add: type_wf_defs split: option.splits)
 
 lemma type_wf_put_ptr_not_in_heap_E:
   assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
   assumes "ptr |\<notin>| object_ptr_kinds h"
   shows "type_wf h"
   using assms
   by(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E 
       split: option.splits if_splits)
 
 lemma type_wf_put_ptr_in_heap_E:
   assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
   assumes "ptr |\<in>| object_ptr_kinds h"
   assumes "NodeClass.type_wf h"
   assumes "is_element_ptr_kind ptr \<Longrightarrow> is_element_kind (the (get ptr h))"
   shows "type_wf h"
   using assms
   apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
   apply(case_tac "x2 = cast element_ptr")
    apply(drule_tac x=element_ptr in allE)
     apply(auto)[1]
    apply(metis (no_types, lifting) NodeClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf assms(2) bind.bind_lunit 
       cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def option.exhaust_sel)
   by(auto)
 
 subsection\<open>Preserving Types\<close>
 
 lemma new_element_type_wf_preserved [simp]: "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       new_element_def Let_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
       split: prod.splits if_splits elim!: bind_returns_heap_E)[1]
      apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter 
       is_element_ptr_ref)
   using element_ptrs_def apply fastforce
    apply (metis (mono_tags, hide_lams) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes 
       element_ptrs_def fMax_ge ffmember_filter fimageI is_element_ptr_ref)
   by (metis (no_types, lifting) fMax_finsert fempty_iff fimage_is_fempty max_0L new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap)
 
 locale l_new_element = l_type_wf +
   assumes new_element_types_preserved: "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
 
 lemma new_element_is_l_new_element: "l_new_element type_wf"
   using l_new_element.intro new_element_type_wf_preserved
   by blast
 
 lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_type_type_wf_preserved [simp]: 
   "h \<turnstile> put_M element_ptr tag_type_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
       Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
       apply (metis option.distinct(1))
      apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
     apply (metis option.distinct(1))
    apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
   by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
 
 
 lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]: 
   "h \<turnstile> put_M element_ptr child_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
       Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
       apply (metis option.distinct(1))
      apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
     apply (metis option.distinct(1))
    apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
   by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
 
 lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]: 
   "h \<turnstile> put_M element_ptr attrs_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  Let_def 
       put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def 
       get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
       apply (metis option.distinct(1))
      apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
     apply (metis option.distinct(1))
    apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
   by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
 
 lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]: 
   "h \<turnstile> put_M element_ptr shadow_root_opt_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
       Let_def put_M_defs get_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
       apply (metis option.distinct(1))
      apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
     apply (metis option.distinct(1))
    apply (metis bind.bind_lunit  cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none)
   by (metis bind.bind_lunit cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inv)
 
 lemma put_M_pointers_preserved:
   assumes "h \<turnstile> put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr setter v \<rightarrow>\<^sub>h h'"
   shows "object_ptr_kinds h = object_ptr_kinds h'"
   using assms 
   apply(auto simp add: put_M_defs put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def 
       elim!: bind_returns_heap_E2 dest!: get_heap_E)[1]
   by (meson get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap is_OK_returns_result_I)
 
 lemma element_ptr_kinds_preserved:
   assumes "writes SW setter h h'"
   assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
   assumes "\<And>h h'. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h' 
                     \<longrightarrow> (\<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h')"
   shows "element_ptr_kinds h = element_ptr_kinds h'"
   using writes_small_big[OF assms]
   apply(simp add: reflp_def transp_def preserved_def element_ptr_kinds_def)
   by (metis assms node_ptr_kinds_preserved)
 
 
 lemma element_ptr_kinds_small:
   assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
   shows "element_ptr_kinds h = element_ptr_kinds h'"
   by(simp add: element_ptr_kinds_def node_ptr_kinds_def preserved_def 
       object_ptr_kinds_preserved_small[OF assms])
 
 lemma type_wf_preserved_small:
   assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
   assumes "\<And>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
   assumes "\<And>element_ptr. preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr RElement.nothing) h h'"
   shows "type_wf h = type_wf h'"
   using type_wf_preserved_small[OF assms(1) assms(2)] allI[OF assms(3), of id, simplified]
   apply(auto simp add: type_wf_defs )[1]
    apply(auto simp add: preserved_def get_M_defs element_ptr_kinds_small[OF assms(1)] 
       split: option.splits,force)[1]
   by(auto simp add: preserved_def get_M_defs element_ptr_kinds_small[OF assms(1)] 
       split: option.splits,force)
 
 lemma type_wf_preserved:
   assumes "writes SW setter h h'"
   assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
   assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' 
            \<Longrightarrow> \<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
   assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' 
            \<Longrightarrow> \<forall>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
   assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' 
            \<Longrightarrow> \<forall>element_ptr. preserved (get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr RElement.nothing) h h'"
   shows "type_wf h = type_wf h'"
 proof -
   have "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> 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 \<Longrightarrow> type_wf (Heap (fmdrop ptr (the_heap h)))"
   apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs 
       node_ptr_kinds_def object_ptr_kinds_def is_node_ptr_kind_def 
       get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def)[1]
     apply (metis (mono_tags, lifting) comp_apply ffmember_filter fimage_eqI 
       is_node_ptr_kind_cast node_ptr_casts_commute2 option.sel)
    apply (metis (no_types, lifting) comp_apply element_ptr_kinds_commutes ffmember_filter 
       fmdom_filter fmfilter_alt_defs(1) heap.sel node_ptr_kinds_commutes object_ptr_kinds_def)
   by (metis comp_eq_dest_lhs element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel 
       node_ptr_kinds_commutes object_ptr_kinds_def)
 
 end
diff --git a/thys/Core_DOM/monads/NodeMonad.thy b/thys/Core_DOM/common/monads/NodeMonad.thy
rename from thys/Core_DOM/monads/NodeMonad.thy
rename to thys/Core_DOM/common/monads/NodeMonad.thy
diff --git a/thys/Core_DOM/monads/ObjectMonad.thy b/thys/Core_DOM/common/monads/ObjectMonad.thy
rename from thys/Core_DOM/monads/ObjectMonad.thy
rename to thys/Core_DOM/common/monads/ObjectMonad.thy
diff --git a/thys/Core_DOM/pointers/CharacterDataPointer.thy b/thys/Core_DOM/common/pointers/CharacterDataPointer.thy
rename from thys/Core_DOM/pointers/CharacterDataPointer.thy
rename to thys/Core_DOM/common/pointers/CharacterDataPointer.thy
diff --git a/thys/Core_DOM/pointers/DocumentPointer.thy b/thys/Core_DOM/common/pointers/DocumentPointer.thy
rename from thys/Core_DOM/pointers/DocumentPointer.thy
rename to thys/Core_DOM/common/pointers/DocumentPointer.thy
diff --git a/thys/Core_DOM/pointers/ElementPointer.thy b/thys/Core_DOM/common/pointers/ElementPointer.thy
rename from thys/Core_DOM/pointers/ElementPointer.thy
rename to thys/Core_DOM/common/pointers/ElementPointer.thy
diff --git a/thys/Core_DOM/pointers/NodePointer.thy b/thys/Core_DOM/common/pointers/NodePointer.thy
rename from thys/Core_DOM/pointers/NodePointer.thy
rename to thys/Core_DOM/common/pointers/NodePointer.thy
diff --git a/thys/Core_DOM/pointers/ObjectPointer.thy b/thys/Core_DOM/common/pointers/ObjectPointer.thy
rename from thys/Core_DOM/pointers/ObjectPointer.thy
rename to thys/Core_DOM/common/pointers/ObjectPointer.thy
diff --git a/thys/Core_DOM/pointers/Ref.thy b/thys/Core_DOM/common/pointers/Ref.thy
rename from thys/Core_DOM/pointers/Ref.thy
rename to thys/Core_DOM/common/pointers/Ref.thy
diff --git a/thys/Core_DOM/preliminaries/Heap_Error_Monad.thy b/thys/Core_DOM/common/preliminaries/Heap_Error_Monad.thy
rename from thys/Core_DOM/preliminaries/Heap_Error_Monad.thy
rename to thys/Core_DOM/common/preliminaries/Heap_Error_Monad.thy
diff --git a/thys/Core_DOM/preliminaries/Hiding_Type_Variables.thy b/thys/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy
rename from thys/Core_DOM/preliminaries/Hiding_Type_Variables.thy
rename to thys/Core_DOM/common/preliminaries/Hiding_Type_Variables.thy
diff --git a/thys/Core_DOM/preliminaries/Testing_Utils.thy b/thys/Core_DOM/common/preliminaries/Testing_Utils.thy
rename from thys/Core_DOM/preliminaries/Testing_Utils.thy
rename to thys/Core_DOM/common/preliminaries/Testing_Utils.thy
diff --git a/thys/Core_DOM/tests/Core_DOM_BaseTest.thy b/thys/Core_DOM/common/tests/Core_DOM_BaseTest.thy
rename from thys/Core_DOM/tests/Core_DOM_BaseTest.thy
rename to thys/Core_DOM/common/tests/Core_DOM_BaseTest.thy
diff --git a/thys/Core_DOM/tests/Document-adoptNode.html b/thys/Core_DOM/common/tests/Document-adoptNode.html
rename from thys/Core_DOM/tests/Document-adoptNode.html
rename to thys/Core_DOM/common/tests/Document-adoptNode.html
diff --git a/thys/Core_DOM/tests/Document-getElementById.html b/thys/Core_DOM/common/tests/Document-getElementById.html
rename from thys/Core_DOM/tests/Document-getElementById.html
rename to thys/Core_DOM/common/tests/Document-getElementById.html
diff --git a/thys/Core_DOM/tests/Document_adoptNode.thy b/thys/Core_DOM/common/tests/Document_adoptNode.thy
rename from thys/Core_DOM/tests/Document_adoptNode.thy
rename to thys/Core_DOM/common/tests/Document_adoptNode.thy
diff --git a/thys/Core_DOM/tests/Document_getElementById.thy b/thys/Core_DOM/common/tests/Document_getElementById.thy
rename from thys/Core_DOM/tests/Document_getElementById.thy
rename to thys/Core_DOM/common/tests/Document_getElementById.thy
diff --git a/thys/Core_DOM/tests/Node-insertBefore.html b/thys/Core_DOM/common/tests/Node-insertBefore.html
rename from thys/Core_DOM/tests/Node-insertBefore.html
rename to thys/Core_DOM/common/tests/Node-insertBefore.html
diff --git a/thys/Core_DOM/tests/Node-removeChild.html b/thys/Core_DOM/common/tests/Node-removeChild.html
rename from thys/Core_DOM/tests/Node-removeChild.html
rename to thys/Core_DOM/common/tests/Node-removeChild.html
diff --git a/thys/Core_DOM/tests/Node_insertBefore.thy b/thys/Core_DOM/common/tests/Node_insertBefore.thy
rename from thys/Core_DOM/tests/Node_insertBefore.thy
rename to thys/Core_DOM/common/tests/Node_insertBefore.thy
diff --git a/thys/Core_DOM/tests/Node_removeChild.thy b/thys/Core_DOM/common/tests/Node_removeChild.thy
rename from thys/Core_DOM/tests/Node_removeChild.thy
rename to thys/Core_DOM/common/tests/Node_removeChild.thy
diff --git a/thys/Core_DOM/Core_DOM_Heap_WF.thy b/thys/Core_DOM/standard/Core_DOM_Heap_WF.thy
rename from thys/Core_DOM/Core_DOM_Heap_WF.thy
rename to thys/Core_DOM/standard/Core_DOM_Heap_WF.thy
diff --git a/thys/Core_DOM/classes/ElementClass.thy b/thys/Core_DOM/standard/classes/ElementClass.thy
rename from thys/Core_DOM/classes/ElementClass.thy
rename to thys/Core_DOM/standard/classes/ElementClass.thy
--- a/thys/Core_DOM/classes/ElementClass.thy
+++ b/thys/Core_DOM/standard/classes/ElementClass.thy
@@ -1,311 +1,311 @@
 (***********************************************************************************
  * Copyright (c) 2016-2018 The University of Sheffield, UK
  *
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
  *
  * * Redistributions of source code must retain the above copyright notice, this
  *   list of conditions and the following disclaimer.
  *
  * * Redistributions in binary form must reproduce the above copyright notice,
  *   this list of conditions and the following disclaimer in the documentation
  *   and/or other materials provided with the distribution.
  *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  * 
  * SPDX-License-Identifier: BSD-2-Clause
  ***********************************************************************************)
 
 section\<open>Element\<close>
 text\<open>In this theory, we introduce the types for the Element  class.\<close>
 theory ElementClass
   imports
-    NodeClass
-    "../pointers/ShadowRootPointer"
+    "NodeClass"
+    "ShadowRootPointer"
 begin
 text\<open>The type @{type "DOMString"} is a type synonym for @{type "string"}, define 
      in \autoref{sec:Core_DOM_Basic_Datatypes}.\<close>
 type_synonym attr_key = DOMString 
 type_synonym attr_value = DOMString
 type_synonym attrs = "(attr_key, attr_value) fmap"
 type_synonym tag_type = DOMString
 record ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr) RElement = RNode +
   nothing :: unit
   tag_type :: tag_type
   child_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
   attrs :: attrs
   shadow_root_opt :: "'shadow_root_ptr shadow_root_ptr option"
 type_synonym 
   ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element) Element
   = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_scheme"
 register_default_tvars 
   "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element) Element"
 type_synonym 
   ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 'Element) Node
   = "(('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) Node"
 register_default_tvars 
   "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 'Element) Node"
 type_synonym 
   ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) Object
   = "('Object, ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) Object"
 register_default_tvars 
   "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) Object"
 
 type_synonym
   ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) heap
   = "('document_ptr document_ptr + 'shadow_root_ptr shadow_root_ptr + 'object_ptr, 'element_ptr element_ptr + 'character_data_ptr character_data_ptr + 'node_ptr, 'Object,
       ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) heap" 
 register_default_tvars
   "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) heap" 
 
 definition element_ptr_kinds :: "(_) heap \<Rightarrow> (_) element_ptr fset"
   where
     "element_ptr_kinds heap = the |`| (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r |`| (ffilter is_element_ptr_kind (node_ptr_kinds heap)))"
 
 lemma element_ptr_kinds_simp [simp]: 
   "element_ptr_kinds (Heap (fmupd (cast element_ptr) element (the_heap h))) = {|element_ptr|} |\<union>| element_ptr_kinds h"
   apply(auto simp add: element_ptr_kinds_def)[1]
   by force
 
 definition element_ptrs :: "(_) heap \<Rightarrow> (_) element_ptr fset"
   where
     "element_ptrs heap = ffilter is_element_ptr (element_ptr_kinds heap)"
 
 definition cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) Node \<Rightarrow> (_) Element option"
   where
     "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t node = (case RNode.more node of Inl element \<Rightarrow> Some (RNode.extend (RNode.truncate node) element) | _ \<Rightarrow> None)"
 adhoc_overloading cast cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 
 abbreviation cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) Object \<Rightarrow> (_) Element option"
   where
     "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t obj \<equiv> (case cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e obj of Some node \<Rightarrow> cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t node | None \<Rightarrow> None)"
 adhoc_overloading cast cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 
 definition cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e :: "(_) Element \<Rightarrow> (_) Node"
   where
     "cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e element = RNode.extend (RNode.truncate element) (Inl (RNode.more element))"
 adhoc_overloading cast cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e
 
 abbreviation cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t :: "(_) Element \<Rightarrow> (_) Object"
   where
     "cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr \<equiv> cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t (cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr)"
 adhoc_overloading cast cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
 
 consts is_element_kind :: 'a
 definition is_element_kind\<^sub>N\<^sub>o\<^sub>d\<^sub>e :: "(_) Node \<Rightarrow> bool"
   where
     "is_element_kind\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr \<longleftrightarrow> cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr \<noteq> None"
 
 adhoc_overloading is_element_kind is_element_kind\<^sub>N\<^sub>o\<^sub>d\<^sub>e
 lemmas is_element_kind_def = is_element_kind\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def
 
 abbreviation is_element_kind\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t :: "(_) Object \<Rightarrow> bool"
   where
     "is_element_kind\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr \<equiv> cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr \<noteq> None"
 adhoc_overloading is_element_kind is_element_kind\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
 
 lemma element_ptr_kinds_commutes [simp]: 
   "cast element_ptr |\<in>| node_ptr_kinds h \<longleftrightarrow> element_ptr |\<in>| element_ptr_kinds h"
   apply(auto simp add: node_ptr_kinds_def element_ptr_kinds_def)[1]
   by (metis (no_types, lifting) element_ptr_casts_commute2 ffmember_filter fimage_eqI 
       fset.map_comp is_element_ptr_kind_none node_ptr_casts_commute3 
       node_ptr_kinds_commutes node_ptr_kinds_def option.sel option.simps(3))
 
 definition get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) element_ptr \<Rightarrow> (_) heap \<Rightarrow> (_) Element option"
   where                             
     "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h = Option.bind (get\<^sub>N\<^sub>o\<^sub>d\<^sub>e (cast element_ptr) h) cast"
 adhoc_overloading get get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 
 locale l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 begin
 definition a_type_wf :: "(_) heap \<Rightarrow> bool"
   where
     "a_type_wf h = (NodeClass.type_wf h \<and> (\<forall>element_ptr. element_ptr |\<in>| element_ptr_kinds h 
                                              \<longrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \<noteq> None))"
 end
 global_interpretation l_type_wf_def\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines type_wf = a_type_wf .
 lemmas type_wf_defs = a_type_wf_def
 
 locale l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = l_type_wf type_wf for type_wf :: "((_) heap \<Rightarrow> bool)" +
   assumes type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t: "type_wf h \<Longrightarrow> ElementClass.type_wf h"
 
 sublocale l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t \<subseteq> l_type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e
   apply(unfold_locales)
   using NodeClass.a_type_wf_def
   by (meson ElementClass.a_type_wf_def l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
 
 locale l_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas = l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 begin
 sublocale l_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_lemmas by unfold_locales
 
 lemma get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf:
   assumes "type_wf h"
   shows "element_ptr |\<in>| element_ptr_kinds h \<longleftrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h \<noteq> None"
   using l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms
   apply(simp add: type_wf_defs get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
   by (metis NodeClass.get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_type_wf bind_eq_None_conv element_ptr_kinds_commutes 
       option.distinct(1))
 end
 
 global_interpretation l_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas type_wf
   by unfold_locales
 
 definition put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) element_ptr \<Rightarrow> (_) Element \<Rightarrow> (_) heap \<Rightarrow> (_) heap"
   where                                     
     "put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr element = put\<^sub>N\<^sub>o\<^sub>d\<^sub>e (cast element_ptr) (cast element)"
 adhoc_overloading put put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t      
 
 lemma put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap:
   assumes "put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr element h = h'"
   shows "element_ptr |\<in>| element_ptr_kinds h'"
   using assms
   unfolding put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def element_ptr_kinds_def
   by (metis element_ptr_kinds_commutes element_ptr_kinds_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_ptr_in_heap)
 
 lemma put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_put_ptrs:
   assumes "put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr element h = h'"
   shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast element_ptr|}"
   using assms
   by (simp add: put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_put_ptrs)
 
 
 
 lemma cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_inject [simp]: 
   "cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e x = cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e y \<longleftrightarrow> x = y"
   apply(simp add: cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def RObject.extend_def RNode.extend_def)
   by (metis (full_types) RNode.surjective old.unit.exhaust)
 
 lemma cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none [simp]: 
   "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t node = None \<longleftrightarrow> \<not> (\<exists>element. cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e element = node)"
   apply(auto simp add: cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def RObject.extend_def RNode.extend_def 
       split: sum.splits)[1]
   by (metis (full_types) RNode.select_convs(2) RNode.surjective old.unit.exhaust)
 
 lemma cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_some [simp]: 
   "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t node = Some element \<longleftrightarrow> cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e element = node"
   by(auto simp add: cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def RObject.extend_def RNode.extend_def 
       split: sum.splits)
 
 lemma cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv [simp]: "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t (cast\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e element) = Some element"
   by simp
 
 lemma get_elment_ptr_simp1 [simp]: 
   "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr element h) = Some element"
   by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
 lemma get_elment_ptr_simp2 [simp]: 
   "element_ptr \<noteq> element_ptr' 
   \<Longrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr' element h) = get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h"
   by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
 
 
 abbreviation "create_element_obj tag_type_arg child_nodes_arg attrs_arg shadow_root_opt_arg
   \<equiv> \<lparr> RObject.nothing = (), RNode.nothing = (), RElement.nothing = (),
       tag_type = tag_type_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
       shadow_root_opt = shadow_root_opt_arg, \<dots> = None \<rparr>"
 
 definition new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t :: "(_) heap \<Rightarrow> ((_) element_ptr \<times> (_) heap)"
   where
     "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = 
       (let new_element_ptr = element_ptr.Ref (Suc (fMax (finsert 0 (element_ptr.the_ref 
                                  |`| (element_ptrs h))))) 
        in
       (new_element_ptr, put new_element_ptr (create_element_obj '''' [] fmempty None) h))"
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   shows "new_element_ptr |\<in>| element_ptr_kinds h'"
   using assms
   unfolding new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def
   using put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap by blast
 
 lemma new_element_ptr_new: 
   "element_ptr.Ref (Suc (fMax (finsert 0 (element_ptr.the_ref |`| element_ptrs h)))) |\<notin>| element_ptrs h"
   by (metis Suc_n_not_le_n element_ptr.sel(1) fMax_ge fimage_finsert finsertI1 finsertI2 set_finsert)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   shows "new_element_ptr |\<notin>| element_ptr_kinds h"
   using assms
   unfolding new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
   by (metis Pair_inject element_ptrs_def ffmember_filter new_element_ptr_new is_element_ptr_ref)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_new_ptr:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_element_ptr|}"
   using assms
   by (metis Pair_inject new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_put_ptrs)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_is_element_ptr:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   shows "is_element_ptr new_element_ptr"
   using assms
   by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t [simp]:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   assumes "ptr \<noteq> cast new_element_ptr"
   shows "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr h = get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr h'"
   using assms
   by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e [simp]:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   assumes "ptr \<noteq> cast new_element_ptr"
   shows "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr h = get\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr h'"
   using assms
   by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
 
 lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
   assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
   assumes "ptr \<noteq> new_element_ptr"
   shows "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
   using assms
   by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)
 
 
 locale l_known_ptr\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
 begin
 definition a_known_ptr :: "(_) object_ptr \<Rightarrow> bool"
   where
     "a_known_ptr ptr = (known_ptr ptr \<or> is_element_ptr ptr)"
 
 lemma known_ptr_not_element_ptr: "\<not>is_element_ptr ptr \<Longrightarrow> a_known_ptr ptr \<Longrightarrow> known_ptr ptr"
   by(simp add: a_known_ptr_def)
 end
 global_interpretation l_known_ptr\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t defines known_ptr = a_known_ptr .
 lemmas known_ptr_defs = a_known_ptr_def
 
 
 locale l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr \<Rightarrow> bool"
 begin
 definition a_known_ptrs :: "(_) heap \<Rightarrow> bool"
   where
     "a_known_ptrs h = (\<forall>ptr. ptr |\<in>| object_ptr_kinds h \<longrightarrow> known_ptr ptr)"
 
 lemma known_ptrs_known_ptr: 
   "ptr |\<in>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> known_ptr ptr"
   by(simp add: a_known_ptrs_def)
 
 lemma known_ptrs_preserved: "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
   by(auto simp add: a_known_ptrs_def)
 lemma known_ptrs_subset: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
   by(auto simp add: a_known_ptrs_def)
 end
 global_interpretation l_known_ptrs\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t known_ptr defines known_ptrs = a_known_ptrs .
 lemmas known_ptrs_defs = a_known_ptrs_def
 
 lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
   using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset by blast
 
 end
diff --git a/thys/Core_DOM/pointers/ShadowRootPointer.thy b/thys/Core_DOM/standard/pointers/ShadowRootPointer.thy
rename from thys/Core_DOM/pointers/ShadowRootPointer.thy
rename to thys/Core_DOM/standard/pointers/ShadowRootPointer.thy
--- a/thys/Core_DOM/pointers/ShadowRootPointer.thy
+++ b/thys/Core_DOM/standard/pointers/ShadowRootPointer.thy
@@ -1,182 +1,182 @@
 (***********************************************************************************
  * Copyright (c) 2016-2018 The University of Sheffield, UK
  *
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
  *
  * * Redistributions of source code must retain the above copyright notice, this
  *   list of conditions and the following disclaimer.
  *
  * * Redistributions in binary form must reproduce the above copyright notice,
  *   this list of conditions and the following disclaimer in the documentation
  *   and/or other materials provided with the distribution.
  *
  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
  * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
  * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
  * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
  * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  * 
  * SPDX-License-Identifier: BSD-2-Clause
  ***********************************************************************************)
 
 section\<open>ShadowRoot\<close>
 text\<open>In this theory, we introduce the typed pointers for the class ShadowRoot. Note that, in 
 this document, we will not make use of ShadowRoots nor will we discuss their particular properties. 
 We only include them here, as they are required for future work and they cannot be added alter
 following the object-oriented extensibility of our data model.\<close>   
 theory ShadowRootPointer
   imports
-    DocumentPointer
+    "DocumentPointer"
 begin
 
 datatype 'shadow_root_ptr shadow_root_ptr = Ref (the_ref: ref) | Ext 'shadow_root_ptr
 register_default_tvars "'shadow_root_ptr shadow_root_ptr" 
 type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 
     'document_ptr, 'shadow_root_ptr) object_ptr
   = "('shadow_root_ptr shadow_root_ptr + 'object_ptr, 'node_ptr, 'element_ptr, 
       'character_data_ptr, 'document_ptr) object_ptr"
 register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 
                          'document_ptr, 'shadow_root_ptr) object_ptr" 
 
 definition cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r :: "(_)shadow_root_ptr \<Rightarrow> (_) object_ptr"
   where
     "cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = object_ptr.Ext (Inr (Inr (Inl ptr)))"
 
 definition cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r :: "(_) object_ptr \<Rightarrow> (_) shadow_root_ptr option"
   where
     "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = (case ptr of
               object_ptr.Ext (Inr (Inr (Inl shadow_root_ptr))) \<Rightarrow> Some shadow_root_ptr 
               | _ \<Rightarrow> None)"
 
 adhoc_overloading cast cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
 
 
 definition is_shadow_root_ptr_kind :: "(_) object_ptr \<Rightarrow> bool"
   where
     "is_shadow_root_ptr_kind ptr = (case cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr of Some _ \<Rightarrow> True 
                                                                       | None \<Rightarrow> False)"
 
 consts is_shadow_root_ptr :: 'a
 definition is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r :: "(_) shadow_root_ptr \<Rightarrow> bool"
   where
     "is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = (case ptr of shadow_root_ptr.Ref _ \<Rightarrow> True 
                                                     | _ \<Rightarrow> False)"
 
 abbreviation is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r :: "(_) object_ptr \<Rightarrow> bool"
   where
     "is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr \<equiv> (case cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr of
       Some shadow_root_ptr \<Rightarrow> is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr
     | None \<Rightarrow> False)"
 adhoc_overloading is_shadow_root_ptr is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
 lemmas is_shadow_root_ptr_def = is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
 
 consts is_shadow_root_ptr_ext :: 'a
 abbreviation "is_shadow_root_ptr_ext\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr \<equiv> \<not> is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr"
 
 abbreviation "is_shadow_root_ptr_ext\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr \<equiv> (case cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr of
   Some shadow_root_ptr \<Rightarrow> is_shadow_root_ptr_ext\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr
 | None \<Rightarrow> False)"
 adhoc_overloading is_shadow_root_ptr_ext is_shadow_root_ptr_ext\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r is_shadow_root_ptr_ext\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
 
 instantiation shadow_root_ptr :: (linorder) linorder
 begin
 definition 
   less_eq_shadow_root_ptr :: "(_::linorder) shadow_root_ptr \<Rightarrow> (_) shadow_root_ptr \<Rightarrow> bool"
   where 
     "less_eq_shadow_root_ptr x y \<equiv> (case x of Ext i \<Rightarrow> (case y of Ext j \<Rightarrow> i \<le> j | Ref _ \<Rightarrow> False)
                                           | Ref i \<Rightarrow> (case y of Ext _ \<Rightarrow> True | Ref j \<Rightarrow> i \<le> j))"
 definition less_shadow_root_ptr :: "(_::linorder) shadow_root_ptr \<Rightarrow> (_) shadow_root_ptr \<Rightarrow> bool"
   where "less_shadow_root_ptr x y \<equiv> x \<le> y \<and> \<not> y \<le> x"
 instance 
   apply(standard)
   by(auto simp add: less_eq_shadow_root_ptr_def less_shadow_root_ptr_def 
       split: shadow_root_ptr.splits)
 end
 
 
 lemma is_shadow_root_ptr_ref [simp]: "is_shadow_root_ptr (shadow_root_ptr.Ref n)"
   by(simp add: is_shadow_root_ptr\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
 
 lemma is_shadow_root_ptr_not_node_ptr[simp]: "\<not>is_shadow_root_ptr (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr)"
   by(simp add: is_shadow_root_ptr_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
 
 lemma cast_shadow_root_ptr_not_node_ptr [simp]:
   "cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr \<noteq> cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr"
   "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr \<noteq> cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr"
   unfolding cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def by auto
 
 lemma cast_shadow_root_ptr_not_document_ptr [simp]:
   "cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr \<noteq> cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr"
   "cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr \<noteq> cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr"
   unfolding cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def by auto
 
 lemma shadow_root_ptr_no_node_ptr_cast [simp]: 
   "\<not> is_shadow_root_ptr_kind (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr)"
   by(simp add: cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_shadow_root_ptr_kind_def)
 lemma node_ptr_no_shadow_root_ptr_cast [simp]: 
   "\<not> is_node_ptr_kind (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr)"
   using is_node_ptr_kind_obtains by fastforce
 
 lemma shadow_root_ptr_no_document_ptr_cast [simp]: 
   "\<not> is_shadow_root_ptr_kind (cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r document_ptr)"
   by(simp add: cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_shadow_root_ptr_kind_def)
 lemma document_ptr_no_shadow_root_ptr_cast [simp]: 
   "\<not> is_document_ptr_kind (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr)"
   using is_document_ptr_kind_obtains by fastforce
 
 lemma shadow_root_ptr_shadow_root_ptr_cast [simp]: 
   "is_shadow_root_ptr_kind (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr)"
   by (simp add: cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def is_shadow_root_ptr_kind_def)
 
 lemma shadow_root_ptr_casts_commute [simp]:
   "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = Some shadow_root_ptr \<longleftrightarrow> cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr = ptr"
   unfolding cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
   by(auto split: object_ptr.splits sum.splits)
 
 lemma shadow_root_ptr_casts_commute2 [simp]: 
   "(cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr) = Some shadow_root_ptr)"
   by simp
 
 lemma shadow_root_ptr_casts_commute3 [simp]:
   assumes "is_shadow_root_ptr_kind ptr"
   shows "cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (the (cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr)) = ptr"
   using assms
   by(auto simp add: is_shadow_root_ptr_kind_def cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
       split: object_ptr.splits sum.splits)
 
 lemma is_shadow_root_ptr_kind_obtains:
   assumes "is_shadow_root_ptr_kind ptr"
   obtains shadow_root_ptr where "ptr = cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr"
   using assms is_shadow_root_ptr_kind_def
   by (metis case_optionE shadow_root_ptr_casts_commute)
 
 lemma is_shadow_root_ptr_kind_none:
   assumes "\<not>is_shadow_root_ptr_kind ptr"
   shows "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = None"
   using assms
   unfolding is_shadow_root_ptr_kind_def cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
   by (auto split: object_ptr.splits sum.splits)
 
 lemma cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject [simp]: 
   "cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r x = cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r y \<longleftrightarrow> x = y"
   by(simp add: cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
 
 lemma cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_ext_none [simp]: 
   "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
   by(simp add: cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
 
 lemma is_shadow_root_ptr_kind_simp1 [dest]: "is_document_ptr_kind ptr \<Longrightarrow> \<not>is_shadow_root_ptr_kind ptr"
   by (metis document_ptr_no_shadow_root_ptr_cast shadow_root_ptr_casts_commute3)
 
 lemma is_shadow_root_ptr_kind_simp2 [dest]: "is_node_ptr_kind ptr \<Longrightarrow> \<not>is_shadow_root_ptr_kind ptr"
   by (metis node_ptr_no_shadow_root_ptr_cast shadow_root_ptr_casts_commute3)
 
 end