(***********************************************************************************
 * 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 SC DOM Components II\<close>
theory Shadow_DOM_SC_DOM_Components
  imports
    Core_DOM_SC_DOM_Components
    Shadow_DOM_DOM_Components
begin

section \<open>Shadow root scope components\<close>


subsection \<open>get\_scope\_component\<close>

global_interpretation l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_owner_document get_disconnected_nodes
  get_disconnected_nodes_locs to_tree_order
  defines get_scdom_component = a_get_scdom_component
    and is_strongly_scdom_component_safe = a_is_strongly_scdom_component_safe
    and is_weakly_scdom_component_safe = a_is_weakly_scdom_component_safe
  .
interpretation i_get_scdom_component?: l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
  get_owner_document get_disconnected_nodes get_disconnected_nodes_locs to_tree_order
  by(auto simp add: l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def get_scdom_component_def
      is_strongly_scdom_component_safe_def is_weakly_scdom_component_safe_def instances)
declare l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsubsection \<open>get\_component\<close>

locale l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_dom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_heap_is_wellformed +
  l_get_owner_document +
  l_get_owner_document_wf +
  l_get_disconnected_nodes +
  l_to_tree_order +
  l_known_ptr +
  l_known_ptrs +
  l_get_owner_document_wf_get_root_node_wf +
  assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
begin

lemma known_ptr_node_or_document: "known_ptr ptr \<Longrightarrow> is_node_ptr_kind ptr \<or> is_document_ptr_kind ptr"
  by(auto simp add: known_ptr_impl known_ptr_defs DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs
      ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)

lemma get_scdom_component_subset_get_dom_component:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "h \<turnstile> get_dom_component ptr \<rightarrow>\<^sub>r c"
  shows "set c \<subseteq> set sc"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document: "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r document"
    and disc_nodes: "h \<turnstile> get_disconnected_nodes document \<rightarrow>\<^sub>r disc_nodes"
    and tree_order: "h \<turnstile> to_tree_order (cast document) \<rightarrow>\<^sub>r tree_order"
    and disconnected_tree_orders: "h \<turnstile> map_M (to_tree_order \<circ> cast) disc_nodes \<rightarrow>\<^sub>r disconnected_tree_orders"
    and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
    using assms(4)
    by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
        elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
        )

  obtain root_ptr where root_ptr: "h \<turnstile> get_root_node ptr \<rightarrow>\<^sub>r root_ptr"
    and c: "h \<turnstile> to_tree_order root_ptr \<rightarrow>\<^sub>r c"
    using assms(5)
    by(auto simp add: get_dom_component_def elim!: bind_returns_result_E2[rotated, OF get_root_node_pure, rotated])

  show ?thesis
  proof (cases "is_document_ptr_kind root_ptr")
    case True
    then have "cast document = root_ptr"
      using get_root_node_document assms(1) assms(2) assms(3) root_ptr document
      by (metis document_ptr_casts_commute3 returns_result_eq)
    then have "c = tree_order"
      using tree_order c
      by auto
    then show ?thesis
      by(simp add: sc)
  next
    case False
    moreover have "root_ptr |\<in>| object_ptr_kinds h"
      using assms(1) assms(2) assms(3) local.get_root_node_root_in_heap root_ptr by blast
    ultimately have "is_node_ptr_kind root_ptr"
      using assms(3) known_ptrs_known_ptr known_ptr_node_or_document
      by auto
    then obtain root_node_ptr where root_node_ptr: "root_ptr = cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_node_ptr"
      by (metis node_ptr_casts_commute3)
    then have "h \<turnstile> get_owner_document root_ptr \<rightarrow>\<^sub>r document"
      using get_root_node_same_owner_document
      using assms(1) assms(2) assms(3) document root_ptr by blast
    then have "root_node_ptr \<in> set disc_nodes"
      using assms(1) assms(2) assms(3) disc_nodes in_disconnected_nodes_no_parent root_node_ptr
      using local.get_root_node_same_no_parent root_ptr by blast
    then have "c \<in> set disconnected_tree_orders"
      using c root_node_ptr
      using map_M_pure_E[OF disconnected_tree_orders]
      by (metis (mono_tags, lifting) comp_apply local.to_tree_order_pure select_result_I2)
    then show ?thesis
      by(auto simp add: sc)
  qed
qed

lemma get_scdom_component_ptrs_same_owner_document:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "ptr' \<in> set sc"
  assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
  shows "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r owner_document"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document: "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r document"
    and disc_nodes: "h \<turnstile> get_disconnected_nodes document \<rightarrow>\<^sub>r disc_nodes"
    and tree_order: "h \<turnstile> to_tree_order (cast document) \<rightarrow>\<^sub>r tree_order"
    and disconnected_tree_orders: "h \<turnstile> map_M (to_tree_order \<circ> cast) disc_nodes \<rightarrow>\<^sub>r disconnected_tree_orders"
    and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
    using assms(4)
    by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
        elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
        )
  show ?thesis
  proof (cases "ptr' \<in> set tree_order")
    case True
    have "owner_document = document"
      using assms(6) document by fastforce
    then show ?thesis
      by (metis (no_types) True assms(1) assms(2) assms(3) cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject document
          document_ptr_casts_commute3 document_ptr_document_ptr_cast document_ptr_kinds_commutes
          local.get_owner_document_owner_document_in_heap local.get_root_node_document
          local.get_root_node_not_node_same local.to_tree_order_same_root node_ptr_no_document_ptr_cast
          tree_order)
  next
    case False
    then obtain disconnected_tree_order where disconnected_tree_order:
      "ptr' \<in> set disconnected_tree_order" and "disconnected_tree_order \<in> set disconnected_tree_orders"
      using sc \<open>ptr' \<in> set sc\<close>
      by auto
    obtain root_ptr' where
      root_ptr': "root_ptr' \<in> set disc_nodes" and
      "h \<turnstile> to_tree_order (cast root_ptr') \<rightarrow>\<^sub>r disconnected_tree_order"
      using map_M_pure_E2[OF disconnected_tree_orders \<open>disconnected_tree_order \<in> set disconnected_tree_orders\<close>]
      by (metis comp_apply local.to_tree_order_pure)
    have "\<not>(\<exists>parent \<in> fset (object_ptr_kinds h). root_ptr' \<in> set |h \<turnstile> get_child_nodes parent|\<^sub>r)"
      using disc_nodes
      by (meson assms(1) assms(2) assms(3) disjoint_iff_not_equal local.get_child_nodes_ok
          local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr notin_fset
          returns_result_select_result root_ptr')
    then
    have "h \<turnstile> get_parent root_ptr' \<rightarrow>\<^sub>r None"
      using disc_nodes
      by (metis (no_types, lifting) assms(1) assms(2) assms(3) fmember.rep_eq local.get_parent_child_dual
          local.get_parent_ok local.get_parent_parent_in_heap local.heap_is_wellformed_disc_nodes_in_heap
          returns_result_select_result root_ptr' select_result_I2 split_option_ex)
    then have "h \<turnstile> get_root_node ptr' \<rightarrow>\<^sub>r cast root_ptr'"
      using \<open>h \<turnstile> to_tree_order (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_ptr') \<rightarrow>\<^sub>r disconnected_tree_order\<close> assms(1)
        assms(2) assms(3) disconnected_tree_order local.get_root_node_no_parent local.to_tree_order_get_root_node
        local.to_tree_order_ptr_in_result
      by blast
    then have "h \<turnstile> get_owner_document (cast root_ptr') \<rightarrow>\<^sub>r document"
      using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
      by blast

    then have "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r document"
      using \<open>h \<turnstile> get_root_node ptr' \<rightarrow>\<^sub>r cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_ptr'\<close> assms(1) assms(2) assms(3)
        local.get_root_node_same_owner_document
      by blast
    then show ?thesis
      using assms(6) document returns_result_eq by force
  qed
qed

lemma get_scdom_component_ptrs_same_scope_component:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "ptr' \<in> set sc"
  shows "h \<turnstile> get_scdom_component ptr' \<rightarrow>\<^sub>r sc"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document:
    "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r document"
    and disc_nodes: "h \<turnstile> get_disconnected_nodes document \<rightarrow>\<^sub>r disc_nodes"
    and tree_order: "h \<turnstile> to_tree_order (cast document) \<rightarrow>\<^sub>r tree_order"
    and disconnected_tree_orders: "h \<turnstile> map_M (to_tree_order \<circ> cast) disc_nodes \<rightarrow>\<^sub>r disconnected_tree_orders"
    and sc: "sc = tree_order @ (concat disconnected_tree_orders)"
    using assms(4)
    by(auto simp add: get_scdom_component_def elim!: bind_returns_result_E
        elim!: bind_returns_result_E2[rotated, OF get_owner_document_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF get_disconnected_nodes_pure, rotated]
        elim!: bind_returns_result_E2[rotated, OF to_tree_order_pure, rotated]
        )
  show ?thesis
  proof (cases "ptr' \<in> set tree_order")
    case True
    then have "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r document"
      by (metis assms(1) assms(2) assms(3) cast\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject document document_ptr_casts_commute3
          document_ptr_kinds_commutes known_ptr_node_or_document local.get_owner_document_owner_document_in_heap
          local.get_root_node_document local.get_root_node_not_node_same local.known_ptrs_known_ptr
          local.to_tree_order_get_root_node local.to_tree_order_ptr_in_result node_ptr_no_document_ptr_cast tree_order)
    then show ?thesis
      using disc_nodes tree_order disconnected_tree_orders sc
      by(auto simp add: get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
  next
    case False
    then obtain disconnected_tree_order where disconnected_tree_order:
      "ptr' \<in> set disconnected_tree_order" and "disconnected_tree_order \<in> set disconnected_tree_orders"
      using sc \<open>ptr' \<in> set sc\<close>
      by auto
    obtain root_ptr' where
      root_ptr': "root_ptr' \<in> set disc_nodes" and
      "h \<turnstile> to_tree_order (cast root_ptr') \<rightarrow>\<^sub>r disconnected_tree_order"
      using map_M_pure_E2[OF disconnected_tree_orders \<open>disconnected_tree_order \<in> set disconnected_tree_orders\<close>]
      by (metis comp_apply local.to_tree_order_pure)
    have "\<not>(\<exists>parent \<in> fset (object_ptr_kinds h). root_ptr' \<in> set |h \<turnstile> get_child_nodes parent|\<^sub>r)"
      using disc_nodes
      by (meson assms(1) assms(2) assms(3) disjoint_iff_not_equal local.get_child_nodes_ok
          local.heap_is_wellformed_children_disc_nodes_different local.known_ptrs_known_ptr notin_fset
          returns_result_select_result root_ptr')
    then
    have "h \<turnstile> get_parent root_ptr' \<rightarrow>\<^sub>r None"
      using disc_nodes
      by (metis (no_types, lifting) assms(1) assms(2) assms(3) fmember.rep_eq local.get_parent_child_dual
          local.get_parent_ok local.get_parent_parent_in_heap local.heap_is_wellformed_disc_nodes_in_heap
          returns_result_select_result root_ptr' select_result_I2 split_option_ex)
    then have "h \<turnstile> get_root_node ptr' \<rightarrow>\<^sub>r cast root_ptr'"
      using \<open>h \<turnstile> to_tree_order (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_ptr') \<rightarrow>\<^sub>r disconnected_tree_order\<close> assms(1)
        assms(2) assms(3) disconnected_tree_order local.get_root_node_no_parent local.to_tree_order_get_root_node
        local.to_tree_order_ptr_in_result
      by blast
    then have "h \<turnstile> get_owner_document (cast root_ptr') \<rightarrow>\<^sub>r document"
      using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
      by blast

    then have "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r document"
      using \<open>h \<turnstile> get_root_node ptr' \<rightarrow>\<^sub>r cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r root_ptr'\<close> assms(1) assms(2) assms(3)
        local.get_root_node_same_owner_document
      by blast
    then show ?thesis
      using disc_nodes tree_order disconnected_tree_orders sc
      by(auto simp add: get_scdom_component_def intro!: bind_pure_returns_result_I map_M_pure_I)
  qed
qed

lemma get_scdom_component_ok:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "ptr |\<in>| object_ptr_kinds h"
  shows "h \<turnstile> ok (get_scdom_component ptr)"
  using assms
  apply(auto simp add: get_scdom_component_def intro!: bind_is_OK_pure_I map_M_pure_I map_M_ok_I)[1]
  using get_owner_document_ok
     apply blast
    apply (simp add: local.get_disconnected_nodes_ok local.get_owner_document_owner_document_in_heap)
   apply (simp add: local.get_owner_document_owner_document_in_heap local.to_tree_order_ok)
  using local.heap_is_wellformed_disc_nodes_in_heap local.to_tree_order_ok node_ptr_kinds_commutes
  by blast


lemma get_scdom_component_ptr_in_heap:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "ptr' \<in> set sc"
  shows "ptr' |\<in>| object_ptr_kinds h"
  using assms
  apply(auto simp add: get_scdom_component_def elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
  using local.to_tree_order_ptrs_in_heap apply blast
  by (metis (no_types, lifting) assms(4) assms(5) bind_returns_result_E get_scdom_component_impl
      get_scdom_component_ptrs_same_scope_component is_OK_returns_result_I
      l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs.a_get_scdom_component_def local.get_owner_document_ptr_in_heap)

lemma get_scdom_component_contains_get_dom_component:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "ptr' \<in> set sc"
  obtains c where "h \<turnstile> get_dom_component ptr' \<rightarrow>\<^sub>r c" and "set c \<subseteq> set sc"
proof -
  have "h \<turnstile> get_scdom_component ptr' \<rightarrow>\<^sub>r sc"
    using assms(1) assms(2) assms(3) assms(4) assms(5) get_scdom_component_ptrs_same_scope_component
    by blast
  then show ?thesis
    by (meson assms(1) assms(2) assms(3) assms(5) get_scdom_component_ptr_in_heap
        get_scdom_component_subset_get_dom_component is_OK_returns_result_E local.get_dom_component_ok that)
qed

lemma get_scdom_component_owner_document_same:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "ptr' \<in> set sc"
  obtains owner_document where "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r owner_document" and "cast owner_document \<in> set sc"
  using assms
  apply(auto simp add: get_scdom_component_def elim!: bind_returns_result_E2 intro!: map_M_pure_I)[1]
   apply (metis (no_types, lifting) assms(4) assms(5) document_ptr_casts_commute3
      document_ptr_document_ptr_cast get_scdom_component_contains_get_dom_component local.get_dom_component_ptr
      local.get_dom_component_root_node_same local.get_dom_component_to_tree_order local.get_root_node_document
      local.get_root_node_not_node_same local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap
      node_ptr_no_document_ptr_cast)
  apply(rule map_M_pure_E2)
     apply(simp)
    apply(simp)
   apply(simp)
  by (smt assms(4) assms(5) comp_apply get_scdom_component_ptr_in_heap is_OK_returns_result_E
      local.get_owner_document_disconnected_nodes local.get_root_node_ok local.get_root_node_same_owner_document
      local.to_tree_order_get_root_node local.to_tree_order_ptr_in_result)

lemma get_scdom_component_different_owner_documents:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
  assumes "h \<turnstile> get_owner_document ptr' \<rightarrow>\<^sub>r owner_document'"
  assumes "owner_document \<noteq> owner_document'"
  shows "set |h \<turnstile> get_scdom_component ptr|\<^sub>r \<inter> set |h \<turnstile> get_scdom_component ptr'|\<^sub>r = {}"
  using assms get_scdom_component_ptrs_same_owner_document
  by (smt disjoint_iff_not_equal get_scdom_component_ok is_OK_returns_result_I
      local.get_owner_document_ptr_in_heap returns_result_eq returns_result_select_result)
end

interpretation i_get_dom_component_get_scdom_component?: l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_owner_document
  get_disconnected_nodes get_disconnected_nodes_locs to_tree_order heap_is_wellformed parent_child_rel
  type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs
  get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_root_node
  get_root_node_locs get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name
  get_elements_by_tag_name
  by(auto simp add: l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def instances)
declare l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]

lemma get_dom_component_get_scdom_component_is_l_get_dom_component_get_scdom_component [instances]:
  "l_get_dom_component_get_scdom_component get_owner_document heap_is_wellformed type_wf known_ptr known_ptrs get_scdom_component get_dom_component"
  apply(auto simp add: l_get_dom_component_get_scdom_component_def
      l_get_dom_component_get_scdom_component_axioms_def instances)[1]
  using get_scdom_component_subset_get_dom_component apply fast
  using get_scdom_component_ptrs_same_scope_component apply fast
  using get_scdom_component_ptrs_same_owner_document apply fast
  using get_scdom_component_ok apply fast
  using get_scdom_component_ptr_in_heap apply fast
  using get_scdom_component_contains_get_dom_component apply blast
  using get_scdom_component_owner_document_same apply blast
  using get_scdom_component_different_owner_documents apply fast
  done


subsection \<open>attach\_shadow\_root\<close>

lemma attach_shadow_root_not_strongly_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'ShadowRoot::{equal,linorder}) heap" and
    h' and host and new_shadow_root_ptr where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> attach_shadow_root host m \<rightarrow>\<^sub>r new_shadow_root_ptr \<rightarrow>\<^sub>h h'" and
    "\<not> is_strongly_scdom_component_safe {cast host} {cast new_shadow_root_ptr} h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder},
'ShadowRoot::{equal,linorder}) heap"
  let ?P = "do {
    doc \<leftarrow> create_document;
    create_element doc ''div''
}"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?e1 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and host="?e1"])
    by code_simp+
qed

locale l_get_scdom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_dom_component_get_scdom_component +
  l_get_dom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_dom_component_get_scdom_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma attach_shadow_root_is_weakly_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>h h'"
  assumes "ptr \<noteq> cast |h \<turnstile> attach_shadow_root element_ptr shadow_root_mode|\<^sub>r"
  assumes "ptr \<notin> set |h \<turnstile> get_scdom_component (cast element_ptr)|\<^sub>r"
  shows "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
proof -
  have "element_ptr |\<in>| element_ptr_kinds h"
    by (meson assms(4) is_OK_returns_heap_I local.attach_shadow_root_element_ptr_in_heap)
  obtain sc where sc: "h \<turnstile> get_scdom_component (cast element_ptr) \<rightarrow>\<^sub>r sc"
    using get_scdom_component_ok
    by (meson assms(1) assms(2) assms(3) assms(4) element_ptr_kinds_commutes is_OK_returns_heap_I
        local.attach_shadow_root_element_ptr_in_heap node_ptr_kinds_commutes select_result_I)
  then have "ptr \<notin> set |h \<turnstile> get_dom_component (cast element_ptr)|\<^sub>r"
    by (metis (no_types, lifting) \<open>element_ptr |\<in>| element_ptr_kinds h\<close> assms(1) assms(2) assms(3)
        assms(6) element_ptr_kinds_commutes local.get_dom_component_ok
        local.get_scdom_component_subset_get_dom_component node_ptr_kinds_commutes
        returns_result_select_result select_result_I2 set_rev_mp)
  then show ?thesis
    using assms(1) assms(2) assms(3) assms(4) assms(5) local.attach_shadow_root_is_weakly_dom_component_safe
    by blast
qed

lemma attach_shadow_root_is_weakly_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r result"
  assumes "h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>h h'"
  shows "is_weakly_scdom_component_safe {cast element_ptr} {cast result} h h'"
proof -

  obtain h2 h3 new_shadow_root_ptr where
    h2: "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 h2" and
    new_shadow_root_ptr: "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" and
    h3: "h2 \<turnstile> set_mode new_shadow_root_ptr shadow_root_mode \<rightarrow>\<^sub>h h3" and
    h': "h3 \<turnstile> set_shadow_root element_ptr (Some new_shadow_root_ptr) \<rightarrow>\<^sub>h h'"
    using assms(5)
    by(auto simp add: attach_shadow_root_def elim!:  bind_returns_heap_E
        bind_returns_heap_E2[rotated, OF get_tag_name_pure, rotated]
        bind_returns_heap_E2[rotated, OF get_shadow_root_pure, rotated] split: if_splits)
  have "h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr"
    using new_shadow_root_ptr h2 h3 h'
    using assms(5)
    by(auto simp add: attach_shadow_root_def intro!: bind_returns_result_I
        bind_pure_returns_result_I[OF get_tag_name_pure] bind_pure_returns_result_I[OF get_shadow_root_pure]
        elim!:  bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_tag_name_pure, rotated]
        bind_returns_heap_E2[rotated, OF get_shadow_root_pure, rotated] split: if_splits)
  then
  have "object_ptr_kinds h2 = {|cast result|} |\<union>| object_ptr_kinds h"
    using h2 new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_new_ptr
    using new_shadow_root_ptr
    using assms(4) by auto
  moreover
  have object_ptr_kinds_eq_h2: "object_ptr_kinds h2 = object_ptr_kinds h3"
    apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
          OF set_mode_writes h3])
    using set_mode_pointers_preserved
      apply blast
    by (auto simp add: reflp_def transp_def)
  moreover
  have object_ptr_kinds_eq_h3: "object_ptr_kinds h3 = object_ptr_kinds h'"
    apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
          OF set_shadow_root_writes h'])
    using set_shadow_root_pointers_preserved
      apply blast
    by (auto simp add: reflp_def transp_def)
  ultimately have "object_ptr_kinds h' = {|cast result|} |\<union>| object_ptr_kinds h"
    by simp
  moreover
  have "result |\<notin>| shadow_root_ptr_kinds h"
    using h2 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 new_shadow_root_ptr
    using \<open>h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr\<close> assms(4)
      returns_result_eq by metis
  ultimately
  show ?thesis
    using assms
    apply(auto simp add: is_weakly_scdom_component_safe_def Let_def)[1]
    using attach_shadow_root_is_weakly_component_safe_step
    by (smt document_ptr_kinds_commutes local.get_scdom_component_impl select_result_I2
        shadow_root_ptr_kinds_commutes)
qed
end

interpretation i_get_scdom_component_attach_shadow_root?: l_get_scdom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
  get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
  get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe to_tree_order
  get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
  set_shadow_root set_shadow_root_locs set_mode set_mode_locs attach_shadow_root get_disconnected_nodes
  get_disconnected_nodes_locs get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs
  by(auto simp add: l_get_scdom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_scdom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsection \<open>get\_shadow\_root\<close>

lemma get_shadow_root_not_weakly_scdom_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder}, 'CharacterData::{equal,linorder},
'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap" and
    element_ptr and shadow_root_ptr_opt and h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> get_shadow_root_safe element_ptr \<rightarrow>\<^sub>r shadow_root_ptr_opt \<rightarrow>\<^sub>h h'" and
    "\<not> is_weakly_scdom_component_safe {cast element_ptr} (cast ` set_option shadow_root_ptr_opt) h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder}, 'CharacterData::{equal,linorder},
'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap"
  let ?P = "do {
        document_ptr \<leftarrow> create_document;
        html \<leftarrow> create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head \<leftarrow> create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body \<leftarrow> create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 \<leftarrow> attach_shadow_root e1 Open;
        e3 \<leftarrow> create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e1
      }"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?e1 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and element_ptr="?e1"])
    by code_simp+
qed

locale l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_dom_component_get_scdom_component +
  l_get_shadow_root_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_create_document +
  l_get_owner_document_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_mode +
  l_get_scdom_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_shadow_root_safe\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  assumes known_ptrs_impl: "known_ptrs = a_known_ptrs"
begin
lemma get_shadow_root_components_disjunct:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
  shows "set |h \<turnstile> get_scdom_component (cast host)|\<^sub>r \<inter> set |  h \<turnstile> get_scdom_component (cast shadow_root_ptr)|\<^sub>r = {}"
proof -
  obtain owner_document where owner_document: "h \<turnstile> get_owner_document (cast host) \<rightarrow>\<^sub>r owner_document"
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(5) element_ptr_kinds_commutes
        is_OK_returns_result_E is_OK_returns_result_I local.get_dom_component_ok local.get_dom_component_ptr
        local.get_scdom_component_ok local.get_scdom_component_owner_document_same
        local.get_scdom_component_subset_get_dom_component local.get_shadow_root_ptr_in_heap node_ptr_kinds_commutes
        subset_code(1))
  have "owner_document \<noteq> cast shadow_root_ptr"
  proof
    assume "owner_document = cast shadow_root_ptr"
    then have "(cast owner_document, cast host) \<in>
(parent_child_rel h \<union> local.a_host_shadow_root_rel h \<union> a_ptr_disconnected_node_rel h)\<^sup>*"
      using get_owner_document_rel owner_document
      by (metis (no_types, lifting) assms(1) assms(2) assms(3) cast_document_ptr_not_node_ptr(2)
          in_rtrancl_UnI inf_sup_aci(6) inf_sup_aci(7))
    then have "(cast shadow_root_ptr, cast host) \<in>
(parent_child_rel h \<union> local.a_host_shadow_root_rel h \<union> a_ptr_disconnected_node_rel h)\<^sup>*"
      by (simp add: \<open>owner_document = cast shadow_root_ptr\<close>)
    moreover have "(cast host, cast shadow_root_ptr) \<in> a_host_shadow_root_rel h"
      by (metis (mono_tags, lifting) assms(5) is_OK_returns_result_I local.get_shadow_root_ptr_in_heap
          local.a_host_shadow_root_rel_def mem_Collect_eq pair_imageI prod.simps(2) select_result_I2)
    then have "(cast host, cast shadow_root_ptr) \<in>
(parent_child_rel h \<union> local.a_host_shadow_root_rel h \<union> a_ptr_disconnected_node_rel h)"
      by (simp)
    ultimately show False
      using assms(1)
      unfolding heap_is_wellformed_def \<open>owner_document = cast shadow_root_ptr\<close> acyclic_def
      by (meson rtrancl_into_trancl1)
  qed
  moreover
  have "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
    using assms(1) assms(5) local.get_shadow_root_shadow_root_ptr_in_heap by blast
  then
  have "cast shadow_root_ptr \<in> fset (object_ptr_kinds h)"
    by auto
  have "is_shadow_root_ptr shadow_root_ptr"
    using assms(3)[unfolded known_ptrs_impl ShadowRootClass.known_ptrs_defs
        ShadowRootClass.known_ptr_defs DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs NodeClass.known_ptr_defs, simplified, rule_format, OF
        \<open>cast shadow_root_ptr \<in> fset (object_ptr_kinds h)\<close>]
    by(auto simp add: is_document_ptr\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
        split: option.splits document_ptr.splits)
  then
  have "h \<turnstile> get_owner_document (cast shadow_root_ptr) \<rightarrow>\<^sub>r cast shadow_root_ptr"
    using \<open>shadow_root_ptr |\<in>| shadow_root_ptr_kinds h\<close>
    apply(auto simp add: get_owner_document_def a_get_owner_document_tups_def
        CD.a_get_owner_document_tups_def)[1]
    apply(split invoke_splits, (rule conjI | rule impI)+)+
    by(auto simp add: is_node_ptr_kind_none a_get_owner_document\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
        CD.a_get_owner_document\<^sub>d\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)
  ultimately show ?thesis
    using assms(1) assms(2) assms(3) get_scdom_component_different_owner_documents owner_document
    by blast
qed

lemma get_shadow_root_is_strongly_scdom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_shadow_root_safe element_ptr \<rightarrow>\<^sub>r shadow_root_ptr_opt \<rightarrow>\<^sub>h h'"
  assumes "\<forall>shadow_root_ptr \<in> fset (shadow_root_ptr_kinds h). h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Closed"
  shows "is_strongly_scdom_component_safe {cast element_ptr} (cast ` set_option shadow_root_ptr_opt) h h'"
proof -
  have "h = h'"
    using assms(4)
    by(auto simp add: returns_result_heap_def pure_returns_heap_eq)
  moreover have "shadow_root_ptr_opt = None"
    using assms(4)
    apply(auto simp add: returns_result_heap_def get_shadow_root_safe_def elim!: bind_returns_result_E2
        split: option.splits if_splits)[1]
    using get_shadow_root_shadow_root_ptr_in_heap
    by (meson assms(5) is_OK_returns_result_I local.get_mode_ptr_in_heap notin_fset returns_result_eq
        shadow_root_mode.distinct(1))
  ultimately show ?thesis
    by(simp add: is_strongly_scdom_component_safe_def preserved_def)
qed
end

interpretation i_get_shadow_root_scope_component?: l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
  get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe get_dom_component
  is_strongly_dom_component_safe is_weakly_dom_component_safe get_shadow_root get_shadow_root_locs
  get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_tag_name
  get_tag_name_locs heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs get_disconnected_document
  get_disconnected_document_locs to_tree_order get_parent get_parent_locs get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
  remove_shadow_root remove_shadow_root_locs create_document DocumentClass.known_ptr DocumentClass.type_wf
  CD.a_get_owner_document  get_mode get_mode_locs get_shadow_root_safe get_shadow_root_safe_locs
  by(auto simp add: l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def instances)
declare l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsection \<open>get\_host\<close>

lemma get_host_not_weakly_scdom_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap" and
    shadow_root_ptr and element_ptr and h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r element_ptr \<rightarrow>\<^sub>h h'" and
    "\<not> is_weakly_scdom_component_safe {cast shadow_root_ptr} {cast element_ptr} h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder},
'Shadowroot::{equal,linorder}) heap"
  let ?P = "do {
        document_ptr \<leftarrow> create_document;
        html \<leftarrow> create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head \<leftarrow> create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body \<leftarrow> create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 \<leftarrow> attach_shadow_root e1 Open;
        e3 \<leftarrow> create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return s1
      }"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?s1 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and shadow_root_ptr="?s1"])
    by code_simp+
qed

locale l_get_host_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_host_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma get_host_components_disjunct:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_scdom_component ptr \<rightarrow>\<^sub>r sc"
  assumes "h \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r host"
  shows "set |h \<turnstile> get_scdom_component (cast host)|\<^sub>r \<inter> set |  h \<turnstile> get_scdom_component (cast shadow_root_ptr)|\<^sub>r = {}"
  using assms get_shadow_root_components_disjunct local.shadow_root_host_dual
  by blast
end

interpretation i_get_host_scope_component?: l_get_host_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  get_owner_document heap_is_wellformed parent_child_rel type_wf known_ptr
  known_ptrs get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe
  get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_shadow_root
  get_shadow_root_locs get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
  get_tag_name get_tag_name_locs heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs get_disconnected_document
  get_disconnected_document_locs to_tree_order get_parent get_parent_locs get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
  remove_shadow_root remove_shadow_root_locs create_document DocumentClass.known_ptr DocumentClass.type_wf
  CD.a_get_owner_document get_mode get_mode_locs get_shadow_root_safe get_shadow_root_safe_locs
  by(auto simp add: l_get_host_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_host_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsection \<open>get\_root\_node\_si\<close>

lemma get_composed_root_node_not_weakly_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap" and
    ptr and root and h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> get_root_node_si ptr \<rightarrow>\<^sub>r root \<rightarrow>\<^sub>h h'" and
    "\<not> is_weakly_scdom_component_safe {ptr} {root} h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder},
'Shadowroot::{equal,linorder}) heap"
  let ?P = "do {
        document_ptr \<leftarrow> create_document;
        html \<leftarrow> create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head \<leftarrow> create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body \<leftarrow> create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 \<leftarrow> attach_shadow_root e1 Closed;
        e3 \<leftarrow> create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e3
      }"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?e3 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and ptr="cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r ?e3"])
    by code_simp+
qed

locale l_get_scdom_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_dom_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_dom_component_get_scdom_component
begin

lemma get_root_node_si_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_root_node_si ptr' \<rightarrow>\<^sub>r root"
  shows "set |h \<turnstile> get_scdom_component ptr'|\<^sub>r = set |h \<turnstile> get_scdom_component root|\<^sub>r \<or>
set |h \<turnstile> get_scdom_component ptr'|\<^sub>r \<inter> set |h \<turnstile> get_scdom_component root|\<^sub>r = {}"
proof -
  have "ptr' |\<in>| object_ptr_kinds h"
    using get_ancestors_si_ptr_in_heap assms(4)
    by(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)
  then
  obtain sc where "h \<turnstile> get_scdom_component ptr' \<rightarrow>\<^sub>r sc"
    by (meson assms(1) assms(2) assms(3) local.get_scdom_component_ok select_result_I)
  moreover
  have "root |\<in>| object_ptr_kinds h"
    using get_ancestors_si_ptr assms(4)
    apply(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)[1]
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) empty_iff empty_set
        get_ancestors_si_ptrs_in_heap last_in_set)
  then
  obtain sc' where "h \<turnstile> get_scdom_component root \<rightarrow>\<^sub>r sc'"
    by (meson assms(1) assms(2) assms(3) local.get_scdom_component_ok select_result_I)
  ultimately show ?thesis
    by (metis (no_types, hide_lams) IntE \<open>\<And>thesis. (\<And>sc'. h \<turnstile> get_scdom_component root \<rightarrow>\<^sub>r sc' \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
        \<open>\<And>thesis. (\<And>sc. h \<turnstile> get_scdom_component ptr' \<rightarrow>\<^sub>r sc \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> assms(1) assms(2) assms(3) empty_subsetI
        local.get_scdom_component_ptrs_same_scope_component returns_result_eq select_result_I2 subsetI subset_antisym)
qed
end

interpretation i_get_scdom_component_get_root_node_si?: l_get_scdom_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_host
  get_host_locs get_ancestors_si get_ancestors_si_locs get_root_node_si get_root_node_si_locs get_disconnected_nodes
  get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs get_tag_name get_tag_name_locs heap_is_wellformed
  parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_document get_disconnected_document_locs to_tree_order
  get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
  get_owner_document get_scdom_component is_strongly_scdom_component_safe
  by(auto simp add: l_get_scdom_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_scdom_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsection \<open>get\_assigned\_nodes\<close>

lemma assigned_nodes_not_weakly_scdom_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap" and
    node_ptr and nodes and h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> assigned_nodes node_ptr \<rightarrow>\<^sub>r nodes \<rightarrow>\<^sub>h h'" and
    "\<not> is_weakly_scdom_component_safe {cast node_ptr} (cast ` set nodes) h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap"
  let ?P = "do {
        document_ptr \<leftarrow> create_document;
        html \<leftarrow> create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head \<leftarrow> create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body \<leftarrow> create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 \<leftarrow> attach_shadow_root e1 Closed;
        e3 \<leftarrow> create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e3
      }"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?e3 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and node_ptr="?e3"])
    by code_simp+
qed

lemma assigned_slot_not_weakly_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}, 'Shadowroot::{equal,linorder}) heap" and
    node_ptr and slot_opt and h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h \<turnstile> assigned_slot node_ptr \<rightarrow>\<^sub>r slot_opt \<rightarrow>\<^sub>h h'" and
    "\<not> is_weakly_scdom_component_safe {cast node_ptr} (cast ` set_option slot_opt) h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder},
'Shadowroot::{equal,linorder}) heap"
  let ?P = "do {
        document_ptr \<leftarrow> create_document;
        html \<leftarrow> create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head \<leftarrow> create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body \<leftarrow> create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 \<leftarrow> create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 \<leftarrow> attach_shadow_root e1 Open;
        e3 \<leftarrow> create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e2
      }"
  let ?h1 = "|?h0 \<turnstile> ?P|\<^sub>h"
  let ?e2 = "|?h0 \<turnstile> ?P|\<^sub>r"

  show thesis
    apply(rule that[where h="?h1" and node_ptr="cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r ?e2"])
    by code_simp+
qed

locale l_assigned_nodes_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_assigned_nodes_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_shadow_root_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin

lemma find_slot_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> find_slot open_flag node_ptr \<rightarrow>\<^sub>r Some slot"
  shows "set |h \<turnstile> get_scdom_component (cast node_ptr)|\<^sub>r \<inter> set |h \<turnstile> get_scdom_component (cast slot)|\<^sub>r = {}"
proof -
  obtain host shadow_root_ptr to where
    "h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some (cast host)" and
    "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr" and
    "h \<turnstile> to_tree_order (cast shadow_root_ptr) \<rightarrow>\<^sub>r to" and
    "cast slot \<in> set to"
    using assms(4)
    apply(auto simp add: find_slot_def first_in_tree_order_def elim!: bind_returns_result_E2
        map_filter_M_pure_E[where y=slot] split: option.splits if_splits list.splits
        intro!: map_filter_M_pure bind_pure_I)[1]
    by (metis element_ptr_casts_commute3)+

  have "node_ptr |\<in>| node_ptr_kinds h"
    using assms(4) find_slot_ptr_in_heap by blast
  then obtain node_ptr_c where node_ptr_c: "h \<turnstile> get_scdom_component (cast node_ptr) \<rightarrow>\<^sub>r node_ptr_c"
    using assms(1) assms(2) assms(3) get_scdom_component_ok is_OK_returns_result_E
      node_ptr_kinds_commutes[symmetric]
    by metis

  then have "cast host \<in> set node_ptr_c"
    using \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some (cast host)\<close> assms(1) assms(2) assms(3)
    by (meson assms(4) is_OK_returns_result_E local.find_slot_ptr_in_heap local.get_dom_component_ok
        local.get_dom_component_parent_inside local.get_dom_component_ptr
        local.get_scdom_component_subset_get_dom_component node_ptr_kinds_commutes subsetCE)

  then have "h \<turnstile> get_scdom_component (cast host) \<rightarrow>\<^sub>r node_ptr_c"
    using \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some (cast host)\<close> a_heap_is_wellformed_def assms(1) assms(2)
      assms(3) node_ptr_c
    using local.get_scdom_component_ptrs_same_scope_component by blast

  moreover have "slot |\<in>| element_ptr_kinds h"
    using assms(4) find_slot_slot_in_heap by blast
  then obtain slot_c where slot_c: "h \<turnstile> get_scdom_component (cast slot) \<rightarrow>\<^sub>r slot_c"
    using a_heap_is_wellformed_def assms(1) assms(2) assms(3) get_scdom_component_ok
      is_OK_returns_result_E node_ptr_kinds_commutes[symmetric] element_ptr_kinds_commutes[symmetric]
    by smt
  then have "cast shadow_root_ptr \<in> set slot_c"
    using \<open>h \<turnstile> to_tree_order (cast shadow_root_ptr) \<rightarrow>\<^sub>r to\<close> \<open>cast slot \<in> set to\<close> assms(1) assms(2) assms(3)
    by (meson is_OK_returns_result_E local.get_dom_component_ok local.get_dom_component_ptr
        local.get_dom_component_to_tree_order local.get_scdom_component_subset_get_dom_component local.to_tree_order_ptrs_in_heap subsetCE)
  then have "h \<turnstile> get_scdom_component (cast shadow_root_ptr) \<rightarrow>\<^sub>r slot_c"
    using  \<open>h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr\<close> assms(1) assms(2) assms(3) slot_c
    using local.get_scdom_component_ptrs_same_scope_component by blast

  ultimately show ?thesis
    using get_shadow_root_components_disjunct assms \<open>h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr\<close>
      node_ptr_c slot_c
    by (metis (no_types, lifting) select_result_I2)
qed


lemma assigned_nodes_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> assigned_nodes element_ptr \<rightarrow>\<^sub>r nodes"
  assumes "node_ptr \<in> set nodes"
  shows "set |h \<turnstile> get_scdom_component (cast element_ptr)|\<^sub>r \<inter> set |h \<turnstile> get_scdom_component (cast node_ptr)|\<^sub>r = {}"
  using assms
proof -
  have "h \<turnstile> find_slot False node_ptr \<rightarrow>\<^sub>r Some element_ptr"
    using assms(4) assms(5)
    by(auto simp add: assigned_nodes_def elim!: bind_returns_result_E2
        dest!: filter_M_holds_for_result[where x=node_ptr] intro!: bind_pure_I split: if_splits)
  then show ?thesis
    using assms find_slot_is_component_unsafe
    by blast
qed

lemma assigned_slot_is_strongly_scdom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> assigned_slot element_ptr \<rightarrow>\<^sub>r slot_opt \<rightarrow>\<^sub>h h'"
  assumes "\<forall>shadow_root_ptr \<in> fset (shadow_root_ptr_kinds h). h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Closed"
  shows "is_strongly_scdom_component_safe {cast element_ptr} (cast ` set_option slot_opt) h h'"
proof -
  have "h = h'"
    using assms(4) find_slot_pure
    by(auto simp add: assigned_slot_def returns_result_heap_def pure_returns_heap_eq find_slot_impl)
  moreover have "slot_opt = None"
    using assms(4) assms(5)
    apply(auto simp add: returns_result_heap_def assigned_slot_def a_find_slot_def
        elim!: bind_returns_result_E2 split: option.splits if_splits
        dest!: get_shadow_root_shadow_root_ptr_in_heap[OF assms(1)])[1]
     apply (meson finite_set_in returns_result_eq shadow_root_mode.distinct(1))
    apply (meson finite_set_in returns_result_eq shadow_root_mode.distinct(1))
    done
  ultimately show ?thesis
    by(auto simp add: is_strongly_scdom_component_safe_def preserved_def)
qed
end

interpretation i_assigned_nodes_scope_component?: l_assigned_nodes_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  type_wf get_tag_name get_tag_name_locs known_ptr get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs
  heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs
  get_disconnected_document get_disconnected_document_locs get_parent get_parent_locs
  get_mode get_mode_locs get_attribute get_attribute_locs first_in_tree_order find_slot
  assigned_slot known_ptrs to_tree_order assigned_nodes assigned_nodes_flatten flatten_dom
  get_root_node get_root_node_locs remove insert_before insert_before_locs append_child
  remove_shadow_root remove_shadow_root_locs set_shadow_root set_shadow_root_locs remove_child
  remove_child_locs get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe
  get_ancestors get_ancestors_locs get_element_by_id get_elements_by_class_name get_elements_by_tag_name
  get_owner_document set_disconnected_nodes set_disconnected_nodes_locs get_ancestors_di get_ancestors_di_locs
  adopt_node adopt_node_locs adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M adopt_node_locs\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M set_child_nodes set_child_nodes_locs
  get_scdom_component is_strongly_scdom_component_safe is_weakly_scdom_component_safe create_document
  DocumentClass.known_ptr DocumentClass.type_wf CD.a_get_owner_document get_shadow_root_safe
  get_shadow_root_safe_locs
  by(auto simp add: l_assigned_nodes_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_assigned_nodes_scope_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
end