Browse Source

Initial import from AFP.

main
Achim D. Brucker 4 months ago
commit
f36cbcc496
22 changed files with 16506 additions and 0 deletions
  1. +14
    -0
      Shadow_DOM/ROOT
  2. +10508
    -0
      Shadow_DOM/Shadow_DOM.thy
  3. +42
    -0
      Shadow_DOM/Shadow_DOM_Tests.thy
  4. +460
    -0
      Shadow_DOM/classes/ShadowRootClass.thy
  5. +518
    -0
      Shadow_DOM/document/root.bib
  6. +216
    -0
      Shadow_DOM/document/root.tex
  7. +711
    -0
      Shadow_DOM/monads/ShadowRootMonad.thy
  8. +36
    -0
      Shadow_DOM/tests/Document-adoptNode.html
  9. +251
    -0
      Shadow_DOM/tests/Document-getElementById.html
  10. +288
    -0
      Shadow_DOM/tests/Node-insertBefore.html
  11. +66
    -0
      Shadow_DOM/tests/Node-removeChild.html
  12. +373
    -0
      Shadow_DOM/tests/Shadow_DOM_BaseTest.thy
  13. +114
    -0
      Shadow_DOM/tests/Shadow_DOM_Document_adoptNode.thy
  14. +278
    -0
      Shadow_DOM/tests/Shadow_DOM_Document_getElementById.thy
  15. +129
    -0
      Shadow_DOM/tests/Shadow_DOM_Node_insertBefore.thy
  16. +160
    -0
      Shadow_DOM/tests/Shadow_DOM_Node_removeChild.thy
  17. +28
    -0
      Shadow_DOM/tests/my_get_owner_document.html
  18. +81
    -0
      Shadow_DOM/tests/my_get_owner_document.thy
  19. +253
    -0
      Shadow_DOM/tests/slots-fallback.html
  20. +526
    -0
      Shadow_DOM/tests/slots.html
  21. +947
    -0
      Shadow_DOM/tests/slots.thy
  22. +507
    -0
      Shadow_DOM/tests/slots_fallback.thy

+ 14
- 0
Shadow_DOM/ROOT View File

@@ -0,0 +1,14 @@
chapter AFP

session "Shadow_DOM" (AFP) = "Core_DOM" +
options [timeout = 3600]
directories
classes
monads
tests
theories
Shadow_DOM
Shadow_DOM_Tests
document_files
"root.tex"
"root.bib"

+ 10508
- 0
Shadow_DOM/Shadow_DOM.thy
File diff suppressed because it is too large
View File


+ 42
- 0
Shadow_DOM/Shadow_DOM_Tests.thy View File

@@ -0,0 +1,42 @@
(***********************************************************************************
* 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\<open>Shadow DOM Tests\<close>

theory Shadow_DOM_Tests
imports
"tests/slots"
"tests/slots_fallback"
"tests/Shadow_DOM_Document_adoptNode"
"tests/Shadow_DOM_Document_getElementById"
"tests/Shadow_DOM_Node_insertBefore"
"tests/Shadow_DOM_Node_removeChild"
begin
end

+ 460
- 0
Shadow_DOM/classes/ShadowRootClass.thy View File

@@ -0,0 +1,460 @@
(***********************************************************************************
* 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 \<open>The Shadow DOM Data Model\<close>

theory ShadowRootClass
imports
Core_DOM.ShadowRootPointer
Core_DOM.DocumentClass
begin

subsection \<open>ShadowRoot\<close>

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

type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
'shadow_root_ptr, 'Object, 'Node,
'Element, 'CharacterData, 'Document, 'ShadowRoot) heap
= "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
('node_ptr, 'element_ptr,
'character_data_ptr, 'ShadowRoot option) RShadowRoot_ext + 'Object, 'Node, 'Element,
'CharacterData, 'Document) heap"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr,
'shadow_root_ptr, 'Object,
'Node, 'Element, 'CharacterData, 'Document, 'ShadowRoot) heap"
type_synonym "heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l" = "(unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"



definition shadow_root_ptr_kinds :: "(_) heap \<Rightarrow> (_) shadow_root_ptr fset"
where
"shadow_root_ptr_kinds heap =
the |`| (cast |`| (ffilter is_shadow_root_ptr_kind (object_ptr_kinds heap)))"

lemma shadow_root_ptr_kinds_simp [simp]:
"shadow_root_ptr_kinds (Heap (fmupd (cast shadow_root_ptr) shadow_root (the_heap h))) =
{|shadow_root_ptr|} |\<union>| shadow_root_ptr_kinds h"
apply(auto simp add: shadow_root_ptr_kinds_def)[1]
by force

definition shadow_root_ptrs :: "(_) heap \<Rightarrow> (_) shadow_root_ptr fset"
where
"shadow_root_ptrs heap = ffilter is_shadow_root_ptr (shadow_root_ptr_kinds heap)"

definition cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t :: "(_) Object \<Rightarrow> (_) ShadowRoot option"
where
"cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t obj = (case RObject.more obj of
Inr (Inr (Inl shadow_root)) \<Rightarrow> Some (RObject.extend (RObject.truncate obj) shadow_root)
| _ \<Rightarrow> None)"
adhoc_overloading cast cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t

definition cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t:: "(_) ShadowRoot \<Rightarrow> (_) Object"
where
"cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t shadow_root =
(RObject.extend (RObject.truncate shadow_root) (Inr (Inr (Inl (RObject.more shadow_root)))))"
adhoc_overloading cast cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t

definition is_shadow_root_kind :: "(_) Object \<Rightarrow> bool"
where
"is_shadow_root_kind ptr \<longleftrightarrow> cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr \<noteq> None"

lemma shadow_root_ptr_kinds_heap_upd [simp]:
"shadow_root_ptr_kinds (Heap (fmupd (cast shadow_root_ptr) shadow_root (the_heap h))) =
{|shadow_root_ptr|} |\<union>| shadow_root_ptr_kinds h"
apply(auto simp add: shadow_root_ptr_kinds_def)[1]
by force

lemma shadow_root_ptr_kinds_commutes [simp]:
"cast shadow_root_ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
apply(auto simp add: object_ptr_kinds_def shadow_root_ptr_kinds_def)[1]
by (metis (no_types, lifting) shadow_root_ptr_casts_commute2 shadow_root_ptr_shadow_root_ptr_cast
ffmember_filter fimage_eqI
fset.map_comp option.sel)

definition get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t :: "(_) shadow_root_ptr \<Rightarrow> (_) heap \<Rightarrow> (_) ShadowRoot option"
where
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Option.bind (get (cast shadow_root_ptr) h) cast"
adhoc_overloading get get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t

locale l_type_wf_def\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
begin
definition a_type_wf :: "(_) heap \<Rightarrow> bool"
where
"a_type_wf h = (DocumentClass.type_wf h \<and> (\<forall>shadow_root_ptr \<in> fset (shadow_root_ptr_kinds h).
get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h \<noteq> None))"
end
global_interpretation l_type_wf_def\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t = l_type_wf type_wf for type_wf :: "((_) heap \<Rightarrow> bool)" +
assumes type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t: "type_wf h \<Longrightarrow> ShadowRootClass.type_wf h"

sublocale l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t \<subseteq> l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t
apply(unfold_locales)
by (metis (full_types) ShadowRootClass.type_wf_def a_type_wf_def l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_axioms
l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)

lemma type_wf_implies_previous: "type_wf h \<Longrightarrow> DocumentClass.type_wf h"
by(simp add: type_wf_defs)

locale l_get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas = l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
begin
sublocale l_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_lemmas by unfold_locales
lemma get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_type_wf:
assumes "type_wf h"
shows "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h \<longleftrightarrow> get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h \<noteq> None"
using l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_axioms assms
apply(simp add: type_wf_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
by (metis is_none_bind is_none_simps(1) is_none_simps(2) local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf notin_fset
shadow_root_ptr_kinds_commutes)
end

global_interpretation l_get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas type_wf by unfold_locales

definition put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t :: "(_) shadow_root_ptr \<Rightarrow> (_) ShadowRoot \<Rightarrow> (_) heap \<Rightarrow> (_) heap"
where
"put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr shadow_root = put (cast shadow_root_ptr) (cast shadow_root)"
adhoc_overloading put put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t

lemma put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_in_heap:
assumes "put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr shadow_root h = h'"
shows "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h'"
using assms
unfolding put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def
by (metis shadow_root_ptr_kinds_commutes put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap)

lemma put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_put_ptrs:
assumes "put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr shadow_root h = h'"
shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast shadow_root_ptr|}"
using assms
by (simp add: put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_put_ptrs)


lemma cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_inject [simp]: "cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x = cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t y \<longleftrightarrow> x = y"
apply(simp add: cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def)
by (metis (full_types) RObject.surjective old.unit.exhaust)

lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_none [simp]:
"cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t obj = None \<longleftrightarrow> \<not> (\<exists>shadow_root. cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t shadow_root = obj)"
apply(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def
split: sum.splits)[1]
by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)

lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_some [simp]:
"cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t obj = Some shadow_root \<longleftrightarrow> cast shadow_root = obj"
by(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def split: sum.splits)

lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_inv [simp]: "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t (cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t shadow_root) = Some shadow_root"
by simp

lemma cast_shadow_root_not_node [simp]:
"cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t shadow_root \<noteq> cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node"
"cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node \<noteq> cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t shadow_root"
by(auto simp add: cast\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def)


lemma get_shadow_root_ptr_simp1 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr shadow_root h) = Some shadow_root"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma get_shadow_root_ptr_simp2 [simp]:
"shadow_root_ptr \<noteq> shadow_root_ptr'
\<Longrightarrow> get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' shadow_root h) =
get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)

lemma get_shadow_root_ptr_simp3 [simp]:
"get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f 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 get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma get_shadow_root_ptr_simp4 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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 get_shadow_root_ptr_simp5 [simp]:
"get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f h) = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h"
by(auto simp add: get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma get_shadow_root_ptr_simp6 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
lemma get_shadow_root_ptr_simp7 [simp]:
"get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f h) = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma get_shadow_root_ptr_simp8 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t [simp]:
assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
shows "get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^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)

lemma new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t [simp]:
assumes "new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a h = (new_character_data_ptr, h')"
shows "get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h'"
using assms
by(auto simp add: new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def Let_def)

lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t [simp]:
assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
shows "get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h'"
using assms
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


abbreviation "create_shadow_root_obj mode_arg child_nodes_arg
\<equiv> \<lparr> RObject.nothing = (), RShadowRoot.nothing = (), mode = mode_arg,
RShadowRoot.child_nodes = child_nodes_arg, \<dots> = None \<rparr>"

definition new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t :: "(_)heap \<Rightarrow> ((_) shadow_root_ptr \<times> (_) heap)"
where
"new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_in_heap:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "new_shadow_root_ptr |\<in>| shadow_root_ptr_kinds h'"
using assms
unfolding new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def
using put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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)))) |\<notin>|
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 new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_not_in_heap:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "new_shadow_root_ptr |\<notin>| shadow_root_ptr_kinds h"
using assms
unfolding new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def
by (metis Pair_inject shadow_root_ptrs_def fMax_finsert fempty_iff ffmember_filter
fimage_is_fempty is_shadow_root_ptr_ref max_0L new_shadow_root_ptr_new)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_new_ptr:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_shadow_root_ptr|}"
using assms
by (metis Pair_inject new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_put_ptrs)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_is_shadow_root_ptr:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "is_shadow_root_ptr new_shadow_root_ptr"
using assms
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def)


lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
assumes "ptr \<noteq> cast new_shadow_root_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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
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
apply(simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr h = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr h'"
using assms
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
shows "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
using assms
apply(simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t [simp]:
assumes "new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h = (new_shadow_root_ptr, h')"
assumes "ptr \<noteq> new_shadow_root_ptr"
shows "get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h'"
using assms
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def)


locale l_known_ptr\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
begin
definition a_known_ptr :: "(_) object_ptr \<Rightarrow> bool"
where
"a_known_ptr ptr = (known_ptr ptr \<or> is_shadow_root_ptr ptr)"

lemma known_ptr_not_shadow_root_ptr: "a_known_ptr ptr \<Longrightarrow> \<not>is_shadow_root_ptr ptr \<Longrightarrow> known_ptr ptr"
by(simp add: a_known_ptr_def)
lemma known_ptr_new_shadow_root_ptr: "a_known_ptr ptr \<Longrightarrow> \<not>known_ptr ptr \<Longrightarrow> is_shadow_root_ptr ptr"
using l_known_ptr\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t.known_ptr_not_shadow_root_ptr by blast

end
global_interpretation l_known_ptr\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def

locale l_known_ptrs\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^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 \<in> fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> 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' \<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 (simp add: less_eq_fset.rep_eq local.a_known_ptrs_def subsetD)
lemma known_ptrs_new_ptr:
"object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow>
a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrs\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^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 [instances]: "l_known_ptrs known_ptr known_ptrs"
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
known_ptrs_new_ptr
by blast


lemma shadow_root_get_put_1 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr shadow_root h) = Some shadow_root"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma shadow_root_different_get_put [simp]:
"shadow_root_ptr \<noteq> shadow_root_ptr' \<Longrightarrow>
get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' shadow_root h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)


lemma shadow_root_get_put_2 [simp]:
"get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f 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 get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma shadow_root_get_put_3 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t element_ptr (put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t shadow_root_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t element_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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 shadow_root_get_put_4 [simp]:
"get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f h) = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h"
by(auto simp add: get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma shadow_root_get_put_5 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t character_data_ptr (put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a shadow_root_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t character_data_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
lemma shadow_root_get_put_6 [simp]:
"get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr f h) = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)
lemma shadow_root_get_put_7 [simp]:
"get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t document_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t shadow_root_ptr f h) = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t document_ptr h"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)

lemma known_ptrs_implies: "DocumentClass.known_ptrs h \<Longrightarrow> 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 delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t :: "(_) shadow_root_ptr \<Rightarrow> (_) heap \<Rightarrow> (_) heap option" where
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr = delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t (cast shadow_root_ptr)"

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_pointer_removed:
assumes "delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = Some h'"
shows "ptr |\<notin>| shadow_root_ptr_kinds h'"
using assms
by(auto simp add: delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_pointer_removed delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def shadow_root_ptr_kinds_def
split: if_splits)

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_pointer_ptr_in_heap:
assumes "delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h = Some h'"
shows "ptr |\<in>| shadow_root_ptr_kinds h"
using assms
apply(auto simp add: delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_pointer_ptr_in_heap delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def split: if_splits)[1]
using delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_pointer_ptr_in_heap
by fastforce

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ok:
assumes "ptr |\<in>| shadow_root_ptr_kinds h"
shows "delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr h \<noteq> None"
using assms
by (simp add: delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ok delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)

lemma shadow_root_delete_get_1 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h' = None"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)
lemma shadow_root_different_delete_get [simp]:
"shadow_root_ptr \<noteq> shadow_root_ptr' \<Longrightarrow> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' h = Some h' \<Longrightarrow>
get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h' = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)


lemma shadow_root_delete_get_2 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> object_ptr \<noteq> cast shadow_root_ptr \<Longrightarrow>
get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr h' = get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr h"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)
lemma shadow_root_delete_get_3 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h' = get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr h"
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)
lemma shadow_root_delete_get_4 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h' = get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h"
by(simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
lemma shadow_root_delete_get_5 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow>
get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h' = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h"
by(simp add: get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def)
lemma shadow_root_delete_get_6 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h' = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
by(simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
lemma shadow_root_delete_get_7 [simp]:
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h = Some h' \<Longrightarrow> shadow_root_ptr' \<noteq> shadow_root_ptr \<Longrightarrow>
get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' h' = get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' h"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)
end

+ 518
- 0
Shadow_DOM/document/root.bib View File

@@ -0,0 +1,518 @@
@STRING{j-fac = "Formal Aspects of Computing" }
@STRING{pub-springer={Springer-Verlag} }
@STRING{pub-springer:adr={Heidelberg} }
@STRING{s-lncs = "Lecture Notes in Computer Science" }

@Book{ nipkow.ea:isabelle:2002,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {Isabelle/HOL---A Proof Assistant for Higher-Order Logic},
publisher = pub-springer,
address = pub-springer:adr,
series = s-lncs,
volume = 2283,
doi = {10.1007/3-540-45949-9},
abstract = {This book is a self-contained introduction to interactive proof in higher-order logic (HOL), using
the proof assistant Isabelle2002. It is a tutorial for potential users rather than a monograph for
researchers. The book has three parts.
1. Elementary Techniques shows how to model functional programs in higher-order logic. Early examples
involve lists and the natural numbers. Most proofs are two steps long, consisting of induction on a
chosen variable followed by the auto tactic. But even this elementary part covers such advanced topics
as nested and mutual recursion. 2. Logic and Sets presents a collection of lower-level tactics that
you can use to apply rules selectively. It also describes Isabelle/HOL's treatment of sets, functions
and relations and explains how to define sets inductively. One of the examples concerns the theory of
model checking, and another is drawn from a classic textbook on formal languages. 3. Advanced Material
describes a variety of other topics. Among these are the real numbers, records and overloading.
Advanced techniques are described involving induction and recursion. A whole chapter is devoted to an
extended example: the verification of a security protocol. },
year = 2002,
acknowledgement={brucker, 2007-02-19},
bibkey = {nipkow.ea:isabelle:2002}
}

@Misc{ dom-specification,
year = 2016,
month = {DOM Living Standard -- Last Updated 20 October 2016},
day = 20,
url = {https://dom.spec.whatwg.org/},
organization = {Web Hypertext Application Technology Working Group (WHATWG)},
note = {An archived copy of the version from 20 October 2016 is available at
\url{https://git.logicalhacking.com/BrowserSecurity/fDOM-idl/}.}
}

@InProceedings{ brucker.ea:core-dom:2018,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
booktitle = {Proceedings of the Web Programming, Design, Analysis, And Implementation (WPDAI) track at WWW 2018},
location = {Lyon, France},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-fdom-2018},
year = 2018,
abstract = {At its core, the Document Object Model (DOM) defines a tree-like data structure for representing
documents in general and HTML documents in particular. It forms the heart of any rendering engine of
modern web browsers. Formalizing the key concepts of the DOM is a pre-requisite for the formal
reasoning over client-side JavaScript programs as well as for the analysis of security concepts in
modern web browsers. In this paper, we present a formalization of the core DOM, with focus on the
node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to
verify the functional correctness of the most important functions defined in the DOM standard.
Moreover, our formalization is (1) extensible, i.e., can be extended without the need of re-proving
already proven properties and (2) executable, i.e., we can generate executable code from our
specification. },
keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
classification= {conference},
areas = {formal methods, software},
public = {yes}
}

@Article{ klein:operating:2009,
author = {Gerwin Klein},
title = {Operating System Verification --- An Overview},
journal = {S\={a}dhan\={a}},
publisher = pub-springer,
year = 2009,
volume = 34,
number = 1,
month = feb,
pages = {27--69},
abstract = {This paper gives a high-level introduction to the topic of formal, interactive, machine-checked
software verification in general, and the verification of operating systems code in particular. We
survey the state of the art, the advantages and limitations of machine-checked code proofs, and
describe two specific ongoing larger-scale verification projects in more detail.}
}

@InProceedings{ gardner.ea:securing:2009,
author = {Ryan W. Gardner and Sujata Garera and Matthew W. Pagano and Matthew Green and Aviel D. Rubin},
title = {Securing medical records on smart phones},
booktitle = {ACM workshop on Security and privacy in medical and home-care systems (SPIMACS)},
year = 2009,
isbn = {978-1-60558-790-5},
pages = {31--40},
location = {Chicago, Illinois, USA},
doi = {10.1145/1655084.1655090},
address = pub-acm:adr,
publisher = pub-acm,
abstract = {There is an inherent conflict between the desire to maintain privacy of one's medical records and the
need to make those records available during an emergency. To satisfy both objectives, we introduce a
flexible architecture for the secure storage of medical records on smart phones. In our system, a
person can view her records at any time, and emergency medical personnel can view the records as long
as the person is present (even if she is unconscious). Our solution allows for efficient revocation of
access rights and is robust against adversaries who can access the phone's storage offline.}
}

@InProceedings{ raad.ea:dom:2016,
author = {Azalea Raad and Jos{\'{e}} Fragoso Santos and Philippa Gardner},
title = {{DOM:} Specification and Client Reasoning},
booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November
21-23, 2016, Proceedings},
pages = {401--422},
year = 2016,
crossref = {igarashi:programming:2016},
doi = {10.1007/978-3-319-47958-3_21},
abstract = {We present an axiomatic specification of a key fragment of DOM using structural separation logic.
This specification allows us to develop modular reasoning about client programs that call the DOM.}
}

@InProceedings{ bohannon.ea:featherweight:2010,
author = {Aaron Bohannon and Benjamin C. Pierce},
title = {Featherweight {F}irefox: {F}ormalizing the Core of a Web Browser},
booktitle = {Usenix Conference on Web Application Development (WebApps)},
year = 2010,
month = jun,
url = {http://www.cis.upenn.edu/~bohannon/browser-model/},
abstract = {We offer a formal specification of the core functionality of a web browser in the form of a
small-step operational semantics. The specification accurately models the asyn- chronous nature of web
browsers and covers the basic as- pects of windows, DOM trees, cookies, HTTP requests and responses,
user input, and a minimal scripting lan- guage with first-class functions, dynamic evaluation, and
AJAX requests. No security enforcement mechanisms are included{\^a}instead, the model is intended to
serve as a basis for formalizing and experimenting with different security policies and mechanisms. We
survey the most interesting design choices and discuss how our model re- lates to real web browsers.}
}

@Proceedings{ joyce.ea:higher:1994,
editor = {Jeffrey J. Joyce and Carl-Johan H. Seger},
title = {Higher Order Logic Theorem Proving and Its Applications (HUG)},
booktitle = {Higher Order Logic Theorem Proving and Its Applications (HUG)},
publisher = pub-springer,
address = pub-springer:adr,
series = s-lncs,
abstract = {Theorem proving based techniques for formal hardware verification have been evolving constantly and
researchers are getting able to reason about more complex issues than it was possible or practically
feasible in the past. It is often the case that a model of a system is built in a formal logic and
then reasoning about this model is carried out in the logic. Concern is growing on how to consistently
interface a model built in a formal logic with an informal CAD environment. Researchers have been
investigating how to define the formal semantics of hardware description languages so that one can
formally reason about models informally dealt with in a CAD environment. At the University of
Cambridge, the embedding of hardware description languages in a logic is classified in two categories:
deep embedding and shallow embedding. In this paper we argue that there are degrees of formality in
shallow embedding a language in a logic. The choice of the degree of formality is a trade-off between
the security of the embedding and the amount and complexity of the proof effort in the logic. We also
argue that the design of a language could consider this verifiability issue. There are choices in the
design of a language that can make it easier to improve the degree of formality, without implying
serious drawbacks for the CAD environment.},
volume = 780,
year = 1994,
doi = {10.1007/3-540-57826-9},
isbn = {3-540-57826-9},
acknowledgement={brucker, 2007-02-19}
}

@Misc{ whatwg:dom:2017,
key = {whatwg},
author = {{WHATWG}},
url = {https://dom.spec.whatwg.org/commit-snapshots/6253e53af2fbfaa6d25ad09fd54280d8083b2a97/},
month = mar,
year = 2017,
day = 24,
title = {{DOM} -- Living Standard},
note = {Last Updated 24 {March} 2017},
institution = {WHATWG}
}

@Misc{ whatwg:html:2017,
key = {whatwg},
author = {{WHATWG}},
url = {https://html.spec.whatwg.org/},
month = apr,
year = 2017,
day = 13,
title = {{HTML} -- Living Standard},
note = {Last Updated 13 {April} 2017},
institution = {WHATWG}
}

@Misc{ w3c:dom:2015,
key = {w3c},
author = {{W3C}},
url = {https://www.w3.org/TR/dom/},
month = nov,
year = 2015,
day = 19,
title = {{W3C} {DOM4}},
institution = {W3C}
}

@Proceedings{ igarashi:programming:2016,
editor = {Atsushi Igarashi},
title = {Programming Languages and Systems - 14th Asian Symposium, {APLAS} 2016, Hanoi, Vietnam, November
21-23, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = 10017,
year = 2016,
doi = {10.1007/978-3-319-47958-3},
isbn = {978-3-319-47957-6}
}

@InProceedings{ gardner.ea:dom:2008,
author = {Philippa Gardner and Gareth Smith and Mark J. Wheelhouse and Uri Zarfaty},
title = {{DOM:} Towards a Formal Specification},
booktitle = {{PLAN-X} 2008, Programming Language Technologies for XML, An {ACM} {SIGPLAN} Workshop colocated with
{POPL} 2008, San Francisco, California, USA, January 9, 2008},
year = 2008,
crossref = {plan-x:2008},
url = {http://gemo.futurs.inria.fr/events/PLANX2008/papers/p18.pdf},
abstract = {The W3C Document Object Model (DOM) specifies an XML up- date library. DOM is written in English, and
is therefore not compo- sitional and not complete. We provide a first step towards a compo- sitional
specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a
complete reason- ing for straight-line code. Our work transfers O{\^a}Hearn, Reynolds and Yang{\^a}s
local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM.
In par- ticular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about
a simple tree-update language to DOM, showing that our reasoning scales to DOM. Our reasoning not only
formally specifies a significant subset of DOM Core Level 1, but can also be used to verify e.g.
invariant properties of simple Javascript programs.}
}

@InProceedings{ jang.ea:establishing:2012,
author = {Dongseok Jang and Zachary Tatlock and Sorin Lerner},
title = {Establishing Browser Security Guarantees through Formal Shim Verification},
booktitle = {Proceedings of the 21th {USENIX} Security Symposium, Bellevue, WA, USA, August 8-10, 2012},
pages = {113--128},
year = 2012,
crossref = {kohno:proceedings:2012},
url = {https://www.usenix.org/conference/usenixsecurity12/technical-sessions/presentation/jang},
abstract = { Web browsers mediate access to valuable private data in domains ranging from health care to banking.
Despite this critical role, attackers routinely exploit browser vulnerabilities to exfiltrate private
data and take over the un- derlying system. We present Q UARK , a browser whose kernel has been
implemented and verified in Coq. We give a specification of our kernel, show that the implementation
satisfies the specification, and finally show that the specification implies several security
properties, including tab non-interference, cookie integrity and confidentiality, and address bar
integrity. }
}

@Proceedings{ kohno:proceedings:2012,
editor = {Tadayoshi Kohno},
title = {Proceedings of the 21th {USENIX} Security Symposium, Bellevue, WA, USA, August 8-10, 2012},
publisher = {{USENIX} Association},
year = 2012,
timestamp = {Thu, 15 May 2014 09:12:27 +0200}
}

@Proceedings{ plan-x:2008,
title = {{PLAN-X} 2008, Programming Language Technologies for XML, An {ACM} {SIGPLAN} Workshop colocated with
{POPL} 2008, San Francisco, California, USA, January 9, 2008},
year = 2008,
timestamp = {Fri, 18 Jan 2008 13:01:04 +0100}
}

@Article{ brucker.ea:extensible:2008-b,
abstract = {We present an extensible encoding of object-oriented data models into HOL. Our encoding is supported
by a datatype package that leverages the use of the shallow embedding technique to object-oriented
specification and programming languages. The package incrementally compiles an object-oriented data
model, i.e., a class model, to a theory containing object-universes, constructors, accessor functions,
coercions (casts) between dynamic and static types, characteristic sets, and co-inductive class
invariants. The package is conservative, i.e., all properties are derived entirely from constant
definitions, including the constraints over object structures. As an application, we use the package
for an object-oriented core-language called IMP++, for which we formally prove the correctness of a
Hoare-Logic with respect to a denotational semantics.},
address = {Heidelberg},
author = {Achim D. Brucker and Burkhart Wolff},
doi = {10.1007/s10817-008-9108-3},
issn = {0168-7433},
issue = 3,
journal = {Journal of Automated Reasoning},
keywords = {object-oriented data models, HOL, theorem proving, verification},
language = {USenglish},
pages = {219--249},
pdf = {https://www.brucker.ch/bibliography/download/2008/brucker.ea-extensible-2008-b.pdf},
publisher = {Springer-Verlag},
title = {An Extensible Encoding of Object-oriented Data Models in HOL},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b},
volume = 41,
year = 2008
}

@PhDThesis{ brucker:interactive:2007,
abstract = {We present a semantic framework for object-oriented specification languages. We develop this
framework as a conservative shallow embedding in Isabelle/HOL. Using only conservative extensions
guarantees by construction the consistency of our formalization. Moreover, we show how our framework
can be used to build an interactive proof environment, called HOL-OCL, for object-oriented
specifications in general and for UML/OCL in particular.\\\\Our main contributions are an extensible
encoding of object-oriented data structures in HOL, a datatype package for object-oriented
specifications, and the development of several equational and tableaux calculi for object-oriented
specifications. Further, we show that our formal framework can be the basis of a formal
machine-checked semantics for OCL that is compliant to the OCL 2.0 standard.},
abstract_de = {In dieser Arbeit wird ein semantisches Rahmenwerk f{\"u}r objektorientierte Spezifikationen
vorgestellt. Das Rahmenwerk ist als konservative, flache Einbettung in Isabelle/HOL realisiert. Durch
die Beschr{\"a}nkung auf konservative Erweiterungen kann die logische Konsistenz der Einbettung
garantiert werden. Das semantische Rahmenwerk wird verwendet, um das interaktives Beweissystem HOL-OCL
f{\"u}r objektorientierte Spezifikationen im Allgemeinen und insbesondere f{\"u}r UML/OCL zu
entwickeln.\\\\Die Hauptbeitr{\"a}ge dieser Arbeit sind die Entwicklung einer erweiterbaren Kodierung
objektorientierter Datenstrukturen in HOL, ein Datentyp-Paket f{\"u}r objektorientierte
Spezifikationen und die Entwicklung verschiedener Kalk{\"u}le f{\"u}r objektorientierte
Spezifikationen. Zudem zeigen wir, wie das formale Rahmenwerk verwendet werden kann, um eine formale,
maschinell gepr{\"u}fte Semantik f{\"u}r OCL anzugeben, die konform zum Standard f{\"u}r OCL 2.0 ist.},
author = {Achim D. Brucker},
keywords = {OCL, UML, formal semantics, theorem proving, Isabelle, HOL-OCL},
month = {mar},
note = {ETH Dissertation No. 17097.},
pdf = {https://www.brucker.ch/bibliography/download/2007/brucker-interactive-2007.pdf},
school = {ETH Zurich},
title = {An Interactive Proof Environment for Object-oriented Specifications},
url = {https://www.brucker.ch/bibliography/abstract/brucker-interactive-2007},
year = 2007
}

@InCollection{ brucker.ea:standard-compliance-testing:2018,
talk = {talk:brucker.ea:standard-compliance-testing:2018},
abstract = {Most popular technologies are based on informal or semiformal standards that lack a rigid formal
semantics. Typical examples include web technologies such as the DOM or HTML, which are defined by the
Web Hypertext Application Technology Working Group (WHATWG) and the World Wide Web Consortium (W3C).
While there might be API specifications and test cases meant to assert the compliance of a certain
implementation, the actual standard is rarely accompanied by a formal model that would lend itself
for, e.g., verifying the security or safety properties of real systems.
Even when such a formalization of a standard exists, two important questions arise: first, to what
extend does the formal model comply to the standard and, second, to what extend does the
implementation comply to the formal model and the assumptions made during the verification? In this
paper, we present an approach that brings all three involved artifacts - the (semi-)formal standard,
the formalization of the standard, and the implementations - closer together by combining
verification, symbolic execution, and specification based testing.},
keywords = {standard compliance, compliance tests, DOM},
location = {Toulouse, France},
author = {Achim D. Brucker and Michael Herzberg},
booktitle = {{TAP} 2018: Tests And Proofs},
language = {USenglish},
publisher = pub-springer,
address = pub-springer:adr,
series = s-lncs,
number = 10889,
editor = {Cathrine Dubois and Burkhart Wolff},
title = {Formalizing (Web) Standards: An Application of Test and Proof},
categories = {holtestgen, websecurity},
classification= {conference},
areas = {formal methods, software engineering},
public = {yes},
year = 2018,
doi = {10.1007/978-3-319-92994-1_9},
pages = {159--166},
isbn = {978-3-642-38915-3},
pdf = {http://www.brucker.ch/bibliography/download/2018/brucker.ea-standard-compliance-testing-2018.pdf},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-standard-compliance-testing-2018}
}

@InCollection{ brucker.ea:interactive:2005,
keywords = {symbolic test case generations, black box testing, white box testing, theorem proving, interactive
testing},
abstract = {HOL-TestGen is a test environment for specification-based unit testing build upon the proof assistant
Isabelle/HOL\@. While there is considerable skepticism with regard to interactive theorem provers in
testing communities, we argue that they are a natural choice for (automated) symbolic computations
underlying systematic tests. This holds in particular for the development on non-trivial formal test
plans of complex software, where some parts of the overall activity require inherently guidance by a
test engineer. In this paper, we present the underlying methods for both black box and white box
testing in interactive unit test scenarios. HOL-TestGen can also be understood as a unifying technical
and conceptual framework for presenting and investigating the variety of unit test techniques in a
logically consistent way. },
location = {Edinburgh},
author = {Achim D. Brucker and Burkhart Wolff},
booktitle = {Formal Approaches to Testing of Software},
language = {USenglish},
publisher = pub-springer,
address = pub-springer:adr,
series = s-lncs,
number = 3997,
doi = {10.1007/11759744_7},
isbn = {3-540-25109-X},
editor = {Wolfgang Grieskamp and Carsten Weise},
pdf = {http://www.brucker.ch/bibliography/download/2005/brucker.ea-interactive-2005.pdf},
project = {CSFMDOS},
title = {Interactive Testing using {HOL}-{TestGen}},
classification= {workshop},
areas = {formal methods, software},
categories = {holtestgen},
year = 2005,
public = {yes},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-interactive-2005}
}

@Article{ brucker.ea:theorem-prover:2012,
author = {Achim D. Brucker and Burkhart Wolff},
journal = j-fac,
publisher = pub-springer,
address = pub-springer:adr,
language = {USenglish},
categories = {holtestgen},
title = {On Theorem Prover-based Testing},
year = 2013,
issn = {0934-5043},
pages = {683--721},
volume = 25,
number = 5,
classification= {journal},
areas = {formal methods, software},
public = {yes},
doi = {10.1007/s00165-012-0222-y},
keywords = {test case generation, domain partitioning, test sequence, theorem proving, HOL-TestGen},
abstract = {HOL-TestGen is a specification and test case generation environment extending the interactive theorem
prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive
theorem proving, test case generation, and test data generation.
The HOL-TestGen method is two-staged: first, the original formula is partitioned into test cases by
transformation into a normal form called test theorem. Second, the test cases are analyzed for ground
instances (the test data) satisfying the constraints of the test cases. Particular emphasis is put on
the control of explicit test-hypotheses which can be proven over concrete programs.
Due to the generality of the underlying framework, our system can be used for black-box unit,
sequence, reactive sequence and white-box test scenarios. Although based on particularly clean
theoretical foundations, the system can be applied for substantial case-studies. },
pdf = {http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf},
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-theorem-prover-2012}
}

@Article{ brucker.ea:afp-core-dom:2018,
abstract = {In this AFP entry, we formalize the core of the Document Object Model (DOM). At its core, the DOM
defines a tree-like data structure for representing documents in general and HTML documents in
particular. It is the heart of any modern web browser. Formalizing the key concepts of the DOM is a
prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of
security concepts in modern web browsers. We present a formalization of the core DOM, with focus on
the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to
verify the functional correctness of the most important functions defined in the DOM standard.
Moreover, our formalization is 1) extensible, i.e., can be extended without the need of re-proving
already proven properties and 2) executable, i.e., we can generate executable code from our
specification.},
author = {Achim D. Brucker and Michael Herzberg},
date = {2018-12-26},
file = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},
filelabel = {Outline},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {dec},
note = {\url{http://www.isa-afp.org/entries/Core_DOM.html}, Formal proof development},
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-afp-core-dom-2018.pdf},
title = {The Core {DOM}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018-a},
year = 2018
}

@InCollection{ brucker.ea:web-components:2019,
abstract = {The trend towards ever more complex client-side web applications is unstoppable. Compared to
traditional software development, client-side web development lacks a well-established component
model, i.e., a method for easily and safely reusing already developed functionality. To address this
issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM):
shadow trees allow developers to "partition" a DOM instance into parts that should be safely
separated, e.g., code modifying one part should not, unintentionally, affect other parts of the
DOM.\\\\While shadow trees provide the technical basis for defining web components, the DOM standard
neither defines the concept of web components nor specifies the safety properties that web components
should guarantee. Consequently, the standard also does not discuss how or even if the methods for
modifying the DOM respect component boundaries. In this paper, we present a formally verified model of
web components and define safety properties which ensure that different web components can only
interact with each other using well-defined interfaces. Moreover, our verification of the application
programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM
API need to preserve to ensure the integrity of components.},
address = {Heidelberg},
author = {Achim D. Brucker and Michael Herzberg},
booktitle = {Formal Aspects of Component Software (FACS)},
doi = {10.1007/978-3-030-40914-2_3},
editor = {Sung-Shik Jongmans and Farhad Arbab},
isbn = {3-540-25109-X},
keywords = {Web Component, Shadow Tree, DOM, Isabelle/HOL},
language = {USenglish},
location = {Amsterdam, The Netherlands},
number = 12018,
pdf = {https://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {A Formally Verified Model of Web Components},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019},
year = 2020
}

@Article{ brucker.ea:afp-dom-components:2020,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formalization of Web Components},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
date = {2020-09-28},
note = {\url{http://www.isa-afp.org/entries/DOM_Components.html}, Formal proof development},
issn = {2150-914x},
public = {yes},
classification= {formal},
categories = {websecurity},
pdf = {download/2020/brucker.ea-afp-dom-components-2020.pdf},
filelabel = {Outline},
file = {download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
areas = {formal methods, security, software engineering}
}

@Article{ brucker.ea:afp-dom-components:2020-a,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formalization of Web Components},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
date = {2020-09-28},
note = {\url{http://www.isa-afp.org/entries/DOM_Components.html}, Formal proof development},
issn = {2150-914x},
public = {yes},
classification= {formal},
categories = {websecurity},
pdf = {download/2020/brucker.ea-afp-dom-components-2020.pdf},
filelabel = {Outline},
file = {download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
areas = {formal methods, security, software engineering}
}
@PhdThesis{herzberg:web-components:2020,
author = {Michael Herzberg},
title = {Formal Foundations for Provably Safe Web Components},
school = {The University of Sheffield},
year = {2020}
}


+ 216
- 0
Shadow_DOM/document/root.tex View File

@@ -0,0 +1,216 @@
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
{scrreprt}
\usepackage[USenglish]{babel}
\usepackage[numbers, sort&compress]{natbib}
\usepackage{isabelle,isabellesym}
\usepackage{booktabs}
\usepackage{paralist}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{listings}
\lstloadlanguages{HTML}
\usepackage[]{mathtools}
\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
\lstdefinestyle{html}{language=XML,
basicstyle=\ttfamily,
commentstyle=\itshape,
keywordstyle=\color{blue},
ndkeywordstyle=\color{blue},
}
\lstdefinestyle{displayhtml}{style=html,
floatplacement={tbp},
captionpos=b,
framexleftmargin=0pt,
basicstyle=\ttfamily\scriptsize,
backgroundcolor=\color{black!2},
frame=lines,
}
\lstnewenvironment{html}[1][]{\lstset{style=displayhtml, #1}}{}
\def\inlinehtml{\lstinline[style=html, columns=fullflexible]}

\pagestyle{headings}
\isabellestyle{default}
\setcounter{tocdepth}{1}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\thy}{\isabellecontext}
\renewcommand{\isamarkupsection}[1]{%
\begingroup%
\def\isacharunderscore{\textunderscore}%
\section{#1 (\thy)}%
\endgroup%
}

\title{Shadow DOM\\\medskip \Large
A Formal Model of the Document Object Model \emph{with Shadow Roots}}%



\author{%
\href{https://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[1]
\and
\href{https://www.michael-herzberg.de/}{Michael Herzberg}\footnotemark[2]
}

\publishers{
\footnotemark[1]~Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }
\texttt{a.brucker@exeter.ac.uk}\\[2em]
%
\footnotemark[2]~ Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }
\texttt{msherzberg1@sheffield.ac.uk}
}
\begin{document}
\maketitle
\begin{abstract}
\begin{quote}
In this AFP entry, we extend our formalization of the core DOM
(AFP entry \href{https://www.isa-afp.org/entries/Core_DOM.html}
{Core\_DOM}) with \emph{Shadow Roots}. Shadow roots are a recent
proposal of the web community to support a component-based
development approach for client-side web applications.

Shadow roots are a significant extension to the DOM standard
and, as web standards are condemned to be backward compatible,
such extensions often result in complex specification that may
contain unwanted subtleties that can be detected by a
formalization.

Our Isabelle/HOL formalization is, in the sense of
object-orientation, an extension of our formalization of the
core DOM and enjoys the same basic properties, i.e., it is
\begin{inparaenum}
\item \emph{extensible}, i.e., can be extended without the need of
re-proving already proven properties and
\item \emph{executable}, i.e., we can generate executable code
from our specification.
\end{inparaenum}
We exploit the executability to show that our formalization
complies to the official standard of the W3C, respectively,
the WHATWG.

\bigskip
\noindent{\textbf{Keywords:}}
Document Object Model, DOM, Shadow Root, Web Component, Formal
Semantics, Isabelle/HOL
\end{quote}
\end{abstract}


\tableofcontents
\cleardoublepage

\chapter{Introduction}

In a world in which more and more applications are offered as services
on the internet, web browsers start to take on a similarly central
role in our daily IT infrastructure as operating systems. Thus, web
browsers should be developed as rigidly and formally as operating
systems. While formal methods are a well-established technique in the
development of operating systems (see,
\eg,~\citet{klein:operating:2009} for an overview of formal
verification of operating systems), there are few proposals for
improving the development of web browsers using formal
approaches~\cite{gardner.ea:dom:2008,raad.ea:dom:2016,jang.ea:establishing:2012,bohannon.ea:featherweight:2010}.

In~\cite{brucker.ea:afp-core-dom:2018}, we formalized the core of the
Document Object Model (DOM) in Isabelle/HOL\@. The
DOM~\cite{whatwg:dom:2017,w3c:dom:2015} is \emph{the} central data
structure of all modern web browsers. In this work, we extend the
formalization presented in~\cite{brucker.ea:afp-core-dom:2018} with
support for \emph{shadow trees}. Shadow trees are a recent addition to
the DOM standard~\cite{whatwg:dom:2017} that promise support for web
components. As we will see, this promise is not fully achieved and,
for example, the DOM standard itself does not formally define what a
component should be. In this work, we focus on a standard compliant
representation of the DOM with shadow
trees. As~\cite{brucker.ea:afp-core-dom:2018}, our formalization has
the following properties:
\begin{itemize}
\item It provides a \emph{consistency guarantee.} Since all
definitions in our formal semantics are conservative and all rules
are derived, the logical consistency of the DOM node-tree is reduced
to the consistency of HOL.
\item It serves as a \emph{technical basis for a proof system.} Based
on the derived rules and specific setup of proof tactics over
node-trees, our formalization provides a generic proof environment
for the verification of programs manipulating node-trees.
\item It is \emph{executable}, which allows to validate its compliance
to the standard by evaluating the compliance test suite on the
formal model and
\item It is \emph{extensible} in the sense
of~\cite{brucker.ea:extensible:2008-b,brucker:interactive:2007},
\ie, properties proven over the core DOM do not need to be re-proven
for object-oriented extensions such as the HTML document model.
\end{itemize}

In this AFP entry, we limit ourselves to the faithful formalization of
the DOM. As the DOM standard does not formally define web components,
we address the question of formally defining web components and
discussing their safety properties
elsewhere~\cite{brucker.ea:afp-dom-components:2020,brucker.ea:web-components:2019}.

The rest of this document is automatically generated from the
formalization in Isabelle/HOL, i.e., all content is checked by
Isabelle (we refer readers interested in a more high-level presentation
and additional explanations to~\cite{herzberg:web-components:2020,brucker.ea:web-components:2019}.
The structure follows the theory dependencies
(see \autoref{fig:session-graph}): first, we
formalize the DOM with Shadow Roots (\autoref{cha:dom}) and then
formalize we the relevant compliance test cases in
\autoref{cha:tests}.

\begin{figure}
\centering
\includegraphics[height=.9\textheight]{session_graph}
\caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}}
\end{figure}

\clearpage

\chapter{The Shadow DOM}
\label{cha:dom}
In this chapter, we introduce the formalization of the core DOM
\emph{with Shadow Roots}, i.e., the most important algorithms for
querying or modifying the Shadow DOM, as defined in the standard.

\input{ShadowRootClass.tex}
\input{ShadowRootMonad.tex}
\input{Shadow_DOM.tex}


\chapter{Test Suite}
\label{cha:tests}
In this chapter, we present the formalized compliance test cases for
the core DOM. As our formalization is executable, we can
(symbolically) execute the test cases on top of our model. Executing
these test cases successfully shows that our model is compliant to the
official DOM standard. As future work, we plan to generate test cases
from our formal model (e.g.,
using~\cite{brucker.ea:interactive:2005,brucker.ea:theorem-prover:2012})
to improve the quality of the official compliance test suite. For more
details on the relation of test and proof in the context of web
standards, we refer the reader to
\cite{brucker.ea:standard-compliance-testing:2018}.

\input{Shadow_DOM_BaseTest.tex}
\input{slots.tex}
\input{slots_fallback.tex}
\input{Shadow_DOM_Document_adoptNode.tex}
\input{Shadow_DOM_Document_getElementById.tex}
\input{Shadow_DOM_Node_insertBefore.tex}
\input{Shadow_DOM_Node_removeChild.tex}
\input{Shadow_DOM_Tests.tex}


{\small
\bibliographystyle{abbrvnat}
\bibliography{root}
}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

+ 711
- 0
Shadow_DOM/monads/ShadowRootMonad.thy View File

@@ -0,0 +1,711 @@
(***********************************************************************************
* 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\<open>Shadow Root Monad\<close>
theory ShadowRootMonad
imports
"Core_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 \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
shows "|h \<turnstile> shadow_root_ptr_kinds_M|\<^sub>r = |h' \<turnstile> shadow_root_ptr_kinds_M|\<^sub>r"
using assms
by(auto simp add: shadow_root_ptr_kinds_M_defs object_ptr_kinds_M_defs shadow_root_ptr_kinds_def)



global_interpretation l_dummy defines get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t = "l_get_M.a_get_M get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t" .
lemma get_M_is_l_get_M: "l_get_M get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t type_wf shadow_root_ptr_kinds"
apply(simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_type_wf l_get_M_def)
by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf ObjectClass.type_wf_defs bind_eq_None_conv
shadow_root_ptr_kinds_commutes get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def option.simps(3))
lemmas get_M_defs = get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t

locale l_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas = l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
begin
sublocale l_get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_lemmas by unfold_locales

interpretation l_get_M get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t type_wf shadow_root_ptr_kinds
apply(unfold_locales)
apply (simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_type_wf local.type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t)
by (meson ShadowRootMonad.get_M_is_l_get_M l_get_M_def)
lemmas get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ok = get_M_ok[folded get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def]
lemmas get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_in_heap = get_M_ptr_in_heap[folded get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def]
end

global_interpretation l_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas type_wf by unfold_locales


global_interpretation l_put_M type_wf shadow_root_ptr_kinds get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t rewrites
"a_get_M = get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t" defines put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t = a_put_M
apply (simp add: get_M_is_l_get_M l_put_M_def)
by (simp add: get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def)

lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t


locale l_put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas = l_type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
begin
sublocale l_put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_lemmas by unfold_locales

interpretation l_put_M type_wf shadow_root_ptr_kinds get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t
apply(unfold_locales)
apply (simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_type_wf local.type_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t)
by (meson ShadowRootMonad.get_M_is_l_get_M l_get_M_def)
lemmas put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ok = put_M_ok[folded put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def]
end

global_interpretation l_put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_lemmas type_wf by unfold_locales


lemma shadow_root_put_get [simp]: "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
\<Longrightarrow> (\<And>x. getter (setter (\<lambda>_. v) x) = v)
\<Longrightarrow> h' \<turnstile> get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr getter \<rightarrow>\<^sub>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 \<noteq> shadow_root_ptr'
\<Longrightarrow> h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
\<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
\<Longrightarrow> (\<And>x. getter (setter (\<lambda>_. v) x) = getter x)
\<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 NodeMonad.get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def
put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved3 [simp]:
"cast shadow_root_ptr \<noteq> object_ptr
\<Longrightarrow> h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def ObjectMonad.get_M_defs
preserved_def split: option.splits dest: get_heap_E)
lemma get_M_Mshadow_root_preserved4 [simp]:
"h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 shadow_root_ptr \<noteq> object_ptr")[1]
by(auto simp add: put_M_defs get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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 \<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>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr getter) h h'"
by(auto simp add: ObjectMonad.put_M_defs get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def ObjectMonad.get_M_defs
preserved_def split: option.splits dest: get_heap_E)

lemma get_M_Mshadow_root_preserved6 [simp]:
"h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 ElementMonad.get_M_defs preserved_def
split: option.splits dest: get_heap_E)
lemma get_M_Mshadow_root_preserved7 [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> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h'
\<Longrightarrow> preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a 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 \<turnstile> put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr setter v \<rightarrow>\<^sub>h h'
\<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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_Mshadow_root_preserved10 [simp]:
"(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x))
\<Longrightarrow> h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 shadow_root_ptr = object_ptr")
by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def
get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def bind_eq_Some_conv
split: option.splits)

lemma new_element_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t:
"h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^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)

lemma new_character_data_get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t:
"h \<turnstile> new_character_data \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t:
"h \<turnstile> new_document \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M :: "(_) shadow_root_ptr \<Rightarrow> (_, unit) dom_prog" where
"delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr = do {
h \<leftarrow> get_heap;
(case delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr h of
Some h \<Rightarrow> return_heap h |
None \<Rightarrow> error HierarchyRequestError)
}"
adhoc_overloading delete_M delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ok [simp]:
assumes "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
shows "h \<turnstile> ok (delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr)"
using assms
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: prod.splits)

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_in_heap:
assumes "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h'"
shows "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
using assms
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)

lemma delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_not_in_heap:
assumes "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h'"
shows "shadow_root_ptr |\<notin>| shadow_root_ptr_kinds h'"
using assms
apply(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def split: if_splits)[1]
by (metis comp_apply fmdom_notI fmdrop_lookup heap.sel object_ptr_kinds_def shadow_root_ptr_kinds_commutes)

lemma delete_shadow_root_pointers:
assumes "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h'"
shows "object_ptr_kinds h = object_ptr_kinds h' |\<union>| {|cast shadow_root_ptr|}"
using assms
apply(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def split: option.splits)[1]
apply (metis (no_types, lifting) ObjectClass.a_type_wf_def ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_pointer_ptr_in_heap fmlookup_drop get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel option.sel
shadow_root_ptr_kinds_commutes)
using delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_pointer_ptr_in_heap apply blast
by (metis (no_types, lifting) ObjectClass.a_type_wf_def ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def
delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_pointer_ptr_in_heap fmlookup_drop get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def heap.sel option.sel
shadow_root_ptr_kinds_commutes)

lemma delete_shadow_root_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<Longrightarrow>
ptr \<noteq> cast shadow_root_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: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def ObjectMonad.get_M_defs preserved_def
split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)
lemma delete_shadow_root_get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr getter) h h'"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_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_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<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: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_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_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr getter) h h'"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_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_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr getter) h h'"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_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_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t: "h \<turnstile> delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M shadow_root_ptr \<rightarrow>\<^sub>h h' \<Longrightarrow>
shadow_root_ptr \<noteq> shadow_root_ptr' \<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' getter) h h'"
by(auto simp add: delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def delete\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def get_M_defs ObjectMonad.get_M_defs
preserved_def split: prod.splits option.splits if_splits elim!: bind_returns_heap_E)


lemma shadow_root_put_get_1 [simp]: "shadow_root_ptr \<noteq> shadow_root_ptr' \<Longrightarrow>
h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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_2 [simp]: "(\<And>x. getter (setter (\<lambda>_. v) x) = getter x) \<Longrightarrow>
h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr' getter) h h'"
by (cases "shadow_root_ptr = shadow_root_ptr'") (auto simp add: put_M_defs get_M_defs preserved_def
split: option.splits dest: get_heap_E)
lemma shadow_root_put_get_3 [simp]: "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 ElementMonad.get_M_defs preserved_def split: option.splits
dest: get_heap_E)
lemma shadow_root_put_get_4 [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>
preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 shadow_root_put_get_5 [simp]: "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a 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 shadow_root_put_get_6 [simp]: "h \<turnstile> put_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 shadow_root_put_get_7 [simp]: "h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr getter) h h'"
by(auto simp add: put_M_defs DocumentMonad.get_M_defs preserved_def split: option.splits
dest: get_heap_E)
lemma shadow_root_put_get_8 [simp]: "h \<turnstile> put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow>
preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr getter) h h'"
by(auto simp add: DocumentMonad.put_M_defs get_M_defs preserved_def split: option.splits
dest: get_heap_E)
lemma shadow_root_put_get_9 [simp]: "(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) \<Longrightarrow>
h \<turnstile> put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_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 (cases "cast shadow_root_ptr = object_ptr") (auto simp add: put_M_defs get_M_defs
ObjectMonad.get_M_defs NodeMonad.get_M_defs get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def
put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def bind_eq_Some_conv split: option.splits)

subsection \<open>new\_M\<close>

definition new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M :: "(_, (_) shadow_root_ptr) dom_prog"
where
"new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M = do {
h \<leftarrow> get_heap;
(new_ptr, h') \<leftarrow> return (new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t h);
return_heap h';
return new_ptr
}"

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ok [simp]:
"h \<turnstile> ok new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M"
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def split: prod.splits)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_in_heap:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'"
and "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "new_shadow_root_ptr |\<in>| shadow_root_ptr_kinds h'"
using assms
unfolding new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_in_heap is_OK_returns_result_I
elim!: bind_returns_result_E bind_returns_heap_E)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_not_in_heap:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'"
and "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "new_shadow_root_ptr |\<notin>| shadow_root_ptr_kinds h"
using assms new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_ptr_not_in_heap
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_new_ptr:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'"
and "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_shadow_root_ptr|}"
using assms new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_new_ptr
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_is_shadow_root_ptr:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "is_shadow_root_ptr new_shadow_root_ptr"
using assms new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_is_shadow_root_ptr
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def elim!: bind_returns_result_E split: prod.splits)

lemma new_shadow_root_mode:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'"
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "h' \<turnstile> get_M new_shadow_root_ptr mode \<rightarrow>\<^sub>r Open"
using assms
by(auto simp add: get_M_defs new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def
split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_shadow_root_children:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'"
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "h' \<turnstile> get_M new_shadow_root_ptr child_nodes \<rightarrow>\<^sub>r []"
using assms
by(auto simp add: get_M_defs new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def
split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_shadow_root_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr
\<Longrightarrow> ptr \<noteq> cast new_shadow_root_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\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr
\<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr getter) h h'"
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_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\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr
\<Longrightarrow> preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr getter) h h'"
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'
\<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr
\<Longrightarrow> preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr getter) h h'"
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t:
"h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'
\<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr \<Longrightarrow> ptr \<noteq> new_shadow_root_ptr
\<Longrightarrow> preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t ptr getter) h h'"
by(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_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 shadow_root_get_put_1 [simp]: "get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t shadow_root_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = (if ptr = cast shadow_root_ptr
then cast obj else get shadow_root_ptr h)"
by(auto simp add: get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def split: option.splits Option.bind_splits)

lemma shadow_root_ptr_kinds_new[simp]: "shadow_root_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = shadow_root_ptr_kinds h |\<union>|
(if is_shadow_root_ptr_kind ptr then {|the (cast ptr)|} else {||})"
by(auto simp add: shadow_root_ptr_kinds_def split: option.splits)

lemma type_wf_put_I:
assumes "type_wf h"
assumes "DocumentClass.type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
assumes "is_shadow_root_ptr_kind ptr \<Longrightarrow> is_shadow_root_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 is_shadow_root_kind_def 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!: DocumentMonad.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 "DocumentClass.type_wf h"
assumes "is_shadow_root_ptr_kind ptr \<Longrightarrow> 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, hide_lams) ObjectClass.a_type_wf_def ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf
bind.bind_lunit finite_set_in get\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def is_shadow_root_kind_def option.exhaust_sel)


subsection \<open>type\_wf\<close>

lemma new_element_type_wf_preserved [simp]:
assumes "h \<turnstile> new_element \<rightarrow>\<^sub>h h'"
shows "type_wf h = type_wf h'"
proof -
obtain new_element_ptr where "h \<turnstile> new_element \<rightarrow>\<^sub>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 |\<union>| {|cast new_element_ptr|}"
using new_element_new_ptr by auto
then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
unfolding shadow_root_ptr_kinds_def by auto
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_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_tag_name_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M element_ptr tag_name_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_child_nodes_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M element_ptr RElement.child_nodes_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_attrs_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M element_ptr attrs_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: ElementMonad.put_M_defs type_wf_defs)
qed
lemma put_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_shadow_root_opt_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M element_ptr shadow_root_opt_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
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 \<turnstile> new_character_data \<rightarrow>\<^sub>h h'"
shows "type_wf h = type_wf h'"
proof -
obtain new_character_data_ptr where "h \<turnstile> new_character_data \<rightarrow>\<^sub>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 |\<union>| {|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'"
unfolding shadow_root_ptr_kinds_def by auto
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_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_val_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M character_data_ptr val_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: CharacterDataMonad.put_M_defs type_wf_defs)
qed

lemma new_document_type_wf_preserved [simp]:
assumes "h \<turnstile> new_document \<rightarrow>\<^sub>h h'"
shows "type_wf h = type_wf h'"
proof -
obtain new_document_ptr where "h \<turnstile> new_document \<rightarrow>\<^sub>r new_document_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 |\<union>| {|cast new_document_ptr|}"
using new_document_new_ptr by auto
then have "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
unfolding shadow_root_ptr_kinds_def by auto
with assms show ?thesis
by(auto simp add: DocumentMonad.new_document_def type_wf_defs Let_def elim!: bind_returns_heap_E
split: prod.splits)
qed

lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_doctype_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M document_ptr doctype_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: DocumentMonad.put_M_defs type_wf_defs)
qed
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_document_element_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M document_ptr document_element_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: DocumentMonad.put_M_defs type_wf_defs)
qed
lemma put_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_disconnected_nodes_type_wf_preserved [simp]:
assumes "h \<turnstile> put_M document_ptr disconnected_nodes_update v \<rightarrow>\<^sub>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'"
unfolding shadow_root_ptr_kinds_def by simp
with assms show ?thesis
by(auto simp add: DocumentMonad.put_M_defs type_wf_defs)
qed

lemma put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_mode_type_wf_preserved [simp]:
"h \<turnstile> put_M shadow_root_ptr mode_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
by(auto simp add: get_M_defs is_shadow_root_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 put_M_defs
put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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
split: option.splits)


lemma put_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_child_nodes_type_wf_preserved [simp]:
"h \<turnstile> put_M shadow_root_ptr RShadowRoot.child_nodes_update v \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
by(auto simp add: get_M_defs is_shadow_root_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 put_M_defs
put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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
split: option.splits)


lemma shadow_root_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 "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h'"
by(simp add: shadow_root_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 \<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 "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)
by (metis assms object_ptr_kinds_preserved)

lemma new_shadow_root_known_ptr:
assumes "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr"
shows "known_ptr (cast new_shadow_root_ptr)"
using assms
apply(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def a_known_ptr_def
elim!: bind_returns_result_E2 split: prod.splits)[1]
using assms new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_is_shadow_root_ptr by blast

lemma new_shadow_root_type_wf_preserved [simp]: "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
apply(auto simp add: new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_def new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def Let_def put\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
ShadowRootClass.type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ShadowRootClass.type_wf\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ShadowRootClass.type_wf\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
ShadowRootClass.type_wf\<^sub>N\<^sub>o\<^sub>d\<^sub>e ShadowRootClass.type_wf\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t
is_node_ptr_kind_none new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_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 \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h' \<Longrightarrow> 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 "\<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'"
assumes "\<And>character_data_ptr. preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr RCharacterData.nothing) h h'"
assumes "\<And>document_ptr. preserved (get_M\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr RDocument.nothing) h h'"
assumes "\<And>shadow_root_ptr. preserved (get_M\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t 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 preserved_def get_M_defs shadow_root_ptr_kinds_small[OF assms(1)]
split: option.splits)[1]
apply(force)
apply(force)
done

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.i