Theory Shadow_DOM_SC_DOM_Components

(***********************************************************************************
 * Copyright (c) 2016-2020 The University of Sheffield, UK
 *               2019-2020 University of Exeter, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

section ‹Shadow SC DOM Components II›
theory Shadow_DOM_SC_DOM_Components
  imports
    Core_DOM_SC_DOM_Components
    Shadow_DOM_DOM_Components
begin

section ‹Shadow root scope components›


subsection ‹get\_scope\_component›

global_interpretation l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def get_scdom_component_def
      is_strongly_scdom_component_safe_def is_weakly_scdom_component_safe_def instances)
declare l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_component›

locale l_get_dom_component_get_scdom_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M =
  l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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 ⟹ is_node_ptr_kind ptr ∨ 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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  shows "set c ⊆ set sc"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document: "h ⊢ get_owner_document ptr →⇩r document"
    and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
    and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
    and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩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 ⊢ get_root_node ptr →⇩r root_ptr"
    and c: "h ⊢ to_tree_order root_ptr →⇩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 |∈| 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⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_node_ptr"
      by (metis node_ptr_casts_commute3)
    then have "h ⊢ get_owner_document root_ptr →⇩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 ∈ 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 ∈ 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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "ptr' ∈ set sc"
  assumes "h ⊢ get_owner_document ptr →⇩r owner_document"
  shows "h ⊢ get_owner_document ptr' →⇩r owner_document"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document: "h ⊢ get_owner_document ptr →⇩r document"
    and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
    and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
    and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩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' ∈ 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⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩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' ∈ set disconnected_tree_order" and "disconnected_tree_order ∈ set disconnected_tree_orders"
      using sc ‹ptr' ∈ set sc›
      by auto
    obtain root_ptr' where
      root_ptr': "root_ptr' ∈ set disc_nodes" and
      "h ⊢ to_tree_order (cast root_ptr') →⇩r disconnected_tree_order"
      using map_M_pure_E2[OF disconnected_tree_orders ‹disconnected_tree_order ∈ set disconnected_tree_orders›]
      by (metis comp_apply local.to_tree_order_pure)
    have "¬(∃parent ∈ fset (object_ptr_kinds h). root_ptr' ∈ set |h ⊢ get_child_nodes parent|⇩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
          returns_result_select_result root_ptr')
    then
    have "h ⊢ get_parent root_ptr' →⇩r None"
      using disc_nodes
      by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) 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 ⊢ get_root_node ptr' →⇩r cast root_ptr'"
      using ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr') →⇩r disconnected_tree_order› 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 ⊢ get_owner_document (cast root_ptr') →⇩r document"
      using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
      by blast

    then have "h ⊢ get_owner_document ptr' →⇩r document"
      using ‹h ⊢ get_root_node ptr' →⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr'› 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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "ptr' ∈ set sc"
  shows "h ⊢ get_scdom_component ptr' →⇩r sc"
proof -
  obtain document disc_nodes tree_order disconnected_tree_orders where document:
    "h ⊢ get_owner_document ptr →⇩r document"
    and disc_nodes: "h ⊢ get_disconnected_nodes document →⇩r disc_nodes"
    and tree_order: "h ⊢ to_tree_order (cast document) →⇩r tree_order"
    and disconnected_tree_orders: "h ⊢ map_M (to_tree_order ∘ cast) disc_nodes →⇩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' ∈ set tree_order")
    case True
    then have "h ⊢ get_owner_document ptr' →⇩r document"
      by (metis assms(1) assms(2) assms(3) cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩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' ∈ set disconnected_tree_order" and "disconnected_tree_order ∈ set disconnected_tree_orders"
      using sc ‹ptr' ∈ set sc›
      by auto
    obtain root_ptr' where
      root_ptr': "root_ptr' ∈ set disc_nodes" and
      "h ⊢ to_tree_order (cast root_ptr') →⇩r disconnected_tree_order"
      using map_M_pure_E2[OF disconnected_tree_orders ‹disconnected_tree_order ∈ set disconnected_tree_orders›]
      by (metis comp_apply local.to_tree_order_pure)
    have "¬(∃parent ∈ fset (object_ptr_kinds h). root_ptr' ∈ set |h ⊢ get_child_nodes parent|⇩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
          returns_result_select_result root_ptr')
    then
    have "h ⊢ get_parent root_ptr' →⇩r None"
      using disc_nodes
      by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) 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 ⊢ get_root_node ptr' →⇩r cast root_ptr'"
      using ‹h ⊢ to_tree_order (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr') →⇩r disconnected_tree_order› 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 ⊢ get_owner_document (cast root_ptr') →⇩r document"
      using assms(1) assms(2) assms(3) disc_nodes local.get_owner_document_disconnected_nodes root_ptr'
      by blast

    then have "h ⊢ get_owner_document ptr' →⇩r document"
      using ‹h ⊢ get_root_node ptr' →⇩r cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r root_ptr'› 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 |∈| object_ptr_kinds h"
  shows "h ⊢ 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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "ptr' ∈ set sc"
  shows "ptr' |∈| 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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "ptr' ∈ set sc"
  obtains c where "h ⊢ get_dom_component ptr' →⇩r c" and "set c ⊆ set sc"
proof -
  have "h ⊢ get_scdom_component ptr' →⇩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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "ptr' ∈ set sc"
  obtains owner_document where "h ⊢ get_owner_document ptr' →⇩r owner_document" and "cast owner_document ∈ 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 (verit) 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 ⊢ get_owner_document ptr →⇩r owner_document"
  assumes "h ⊢ get_owner_document ptr' →⇩r owner_document'"
  assumes "owner_document ≠ owner_document'"
  shows "set |h ⊢ get_scdom_component ptr|⇩r ∩ set |h ⊢ get_scdom_component ptr'|⇩r = {}"
  using assms get_scdom_component_ptrs_same_owner_document
  by (smt (verit) 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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_def l_get_dom_component_get_scdom_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms_def instances)
declare l_get_dom_component_get_scdom_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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 ‹attach\_shadow\_root›

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 ⊢ attach_shadow_root host m →⇩r new_shadow_root_ptr →⇩h h'" and
    "¬ 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 ← create_document;
    create_element doc ''div''
}"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e1 = "|?h0 ⊢ ?P|⇩r"

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

locale l_get_scdom_component_attach_shadow_root⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component_get_scdom_component +
  l_get_dom_component_attach_shadow_root⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_dom_component_get_scdom_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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 ⊢ attach_shadow_root element_ptr shadow_root_mode →⇩h h'"
  assumes "ptr ≠ cast |h ⊢ attach_shadow_root element_ptr shadow_root_mode|⇩r"
  assumes "ptr ∉ set |h ⊢ get_scdom_component (cast element_ptr)|⇩r"
  shows "preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t ptr getter) h h'"
proof -
  have "element_ptr |∈| 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 ⊢ get_scdom_component (cast element_ptr) →⇩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 ∉ set |h ⊢ get_dom_component (cast element_ptr)|⇩r"
    by (metis (no_types, lifting) ‹element_ptr |∈| element_ptr_kinds h› 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 ⊢ attach_shadow_root element_ptr shadow_root_mode →⇩r result"
  assumes "h ⊢ attach_shadow_root element_ptr shadow_root_mode →⇩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 ⊢ new⇩S⇩h⇩a⇩d⇩o⇩w⇩R⇩o⇩o⇩t_M →⇩h h2" and
    new_shadow_root_ptr: "h ⊢ new⇩S⇩h⇩a⇩d⇩o⇩w⇩R⇩o⇩o⇩t_M →⇩r new_shadow_root_ptr" and
    h3: "h2 ⊢ set_mode new_shadow_root_ptr shadow_root_mode →⇩h h3" and
    h': "h3 ⊢ set_shadow_root element_ptr (Some new_shadow_root_ptr) →⇩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 ⊢ attach_shadow_root element_ptr shadow_root_mode →⇩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|} |∪| object_ptr_kinds h"
    using h2 new⇩S⇩h⇩a⇩d⇩o⇩w⇩R⇩o⇩o⇩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="λ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="λ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|} |∪| object_ptr_kinds h"
    by simp
  moreover
  have "result |∉| shadow_root_ptr_kinds h"
    using h2 new⇩S⇩h⇩a⇩d⇩o⇩w⇩R⇩o⇩o⇩t_M_ptr_not_in_heap new_shadow_root_ptr
    using ‹h ⊢ attach_shadow_root element_ptr shadow_root_mode →⇩r new_shadow_root_ptr› 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 (verit) 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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_attach_shadow_root⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsection ‹get\_shadow\_root›

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 ⊢ get_shadow_root_safe element_ptr →⇩r shadow_root_ptr_opt →⇩h h'" and
    "¬ 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 ← create_document;
        html ← create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head ← create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body ← create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 ← create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 ← create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 ← attach_shadow_root e1 Open;
        e3 ← create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e1
      }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e1 = "|?h0 ⊢ ?P|⇩r"

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

locale l_get_shadow_root_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M =
  l_get_dom_component_get_scdom_component +
  l_get_shadow_root_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_create_document +
  l_get_owner_document_wf⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_heap_is_wellformed⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_get_mode +
  l_get_scdom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_shadow_root_safe⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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 ⊢ get_scdom_component ptr →⇩r sc"
  assumes "h ⊢ get_shadow_root host →⇩r Some shadow_root_ptr"
  shows "set |h ⊢ get_scdom_component (cast host)|⇩r ∩ set |  h ⊢ get_scdom_component (cast shadow_root_ptr)|⇩r = {}"
proof -
  obtain owner_document where owner_document: "h ⊢ get_owner_document (cast host) →⇩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 ≠ cast shadow_root_ptr"
  proof
    assume "owner_document = cast shadow_root_ptr"
    then have "(cast owner_document, cast host) ∈
(parent_child_rel h ∪ local.a_host_shadow_root_rel h ∪ a_ptr_disconnected_node_rel h)⇧*"
      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) ∈
(parent_child_rel h ∪ local.a_host_shadow_root_rel h ∪ a_ptr_disconnected_node_rel h)⇧*"
      by (simp add: ‹owner_document = cast shadow_root_ptr›)
    moreover have "(cast host, cast shadow_root_ptr) ∈ 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) ∈
(parent_child_rel h ∪ local.a_host_shadow_root_rel h ∪ a_ptr_disconnected_node_rel h)"
      by (simp)
    ultimately show False
      using assms(1)
      unfolding heap_is_wellformed_def ‹owner_document = cast shadow_root_ptr› acyclic_def
      by (meson rtrancl_into_trancl1)
  qed
  moreover
  have "shadow_root_ptr |∈| 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 ∈ 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
        ‹cast shadow_root_ptr ∈ fset (object_ptr_kinds h)›]
    by(auto simp add: is_document_ptr⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def cast⇩s⇩h⇩a⇩d⇩o⇩w⇩_⇩r⇩o⇩o⇩t⇩_⇩p⇩t⇩r⇩2⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r_def
        split: option.splits document_ptr.splits)
  then
  have "h ⊢ get_owner_document (cast shadow_root_ptr) →⇩r cast shadow_root_ptr"
    using ‹shadow_root_ptr |∈| shadow_root_ptr_kinds h›
    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⇩s⇩h⇩a⇩d⇩o⇩w⇩_⇩r⇩o⇩o⇩t⇩_⇩p⇩t⇩r_def
        CD.a_get_owner_document⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩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 ⊢ get_shadow_root_safe element_ptr →⇩r shadow_root_ptr_opt →⇩h h'"
  assumes "∀shadow_root_ptr ∈ fset (shadow_root_ptr_kinds h). h ⊢ get_mode shadow_root_ptr →⇩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 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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_def l_get_shadow_root_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms_def instances)
declare l_get_shadow_root_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms [instances]


subsection ‹get\_host›

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 ⊢ get_host shadow_root_ptr →⇩r element_ptr →⇩h h'" and
    "¬ 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 ← create_document;
        html ← create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head ← create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body ← create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 ← create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 ← create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 ← attach_shadow_root e1 Open;
        e3 ← create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return s1
      }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?s1 = "|?h0 ⊢ ?P|⇩r"

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

locale l_get_host_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M =
  l_get_shadow_root_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_get_host_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M
begin
lemma get_host_components_disjunct:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_scdom_component ptr →⇩r sc"
  assumes "h ⊢ get_host shadow_root_ptr →⇩r host"
  shows "set |h ⊢ get_scdom_component (cast host)|⇩r ∩ set |  h ⊢ get_scdom_component (cast shadow_root_ptr)|⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_def instances)
declare l_get_host_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms [instances]


subsection ‹get\_root\_node\_si›

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 ⊢ get_root_node_si ptr →⇩r root →⇩h h'" and
    "¬ 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 ← create_document;
        html ← create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head ← create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body ← create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 ← create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 ← create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 ← attach_shadow_root e1 Closed;
        e3 ← create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e3
      }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e3 = "|?h0 ⊢ ?P|⇩r"

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

locale l_get_scdom_component_get_root_node_si⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M =
  l_get_dom_component_get_root_node_si⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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 ⊢ get_root_node_si ptr' →⇩r root"
  shows "set |h ⊢ get_scdom_component ptr'|⇩r = set |h ⊢ get_scdom_component root|⇩r ∨
set |h ⊢ get_scdom_component ptr'|⇩r ∩ set |h ⊢ get_scdom_component root|⇩r = {}"
proof -
  have "ptr' |∈| 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 ⊢ get_scdom_component ptr' →⇩r sc"
    by (meson assms(1) assms(2) assms(3) local.get_scdom_component_ok select_result_I)
  moreover
  have "root |∈| 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 ⊢ get_scdom_component root →⇩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, opaque_lifting) IntE ‹⋀thesis. (⋀sc'. h ⊢ get_scdom_component root →⇩r sc' ⟹ thesis) ⟹ thesis›
        ‹⋀thesis. (⋀sc. h ⊢ get_scdom_component ptr' →⇩r sc ⟹ thesis) ⟹ thesis› 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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_def instances)
declare l_get_scdom_component_get_root_node_si⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms [instances]


subsection ‹get\_assigned\_nodes›

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 ⊢ assigned_nodes node_ptr →⇩r nodes →⇩h h'" and
    "¬ 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 ← create_document;
        html ← create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head ← create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body ← create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 ← create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 ← create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 ← attach_shadow_root e1 Closed;
        e3 ← create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e3
      }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e3 = "|?h0 ⊢ ?P|⇩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 ⊢ assigned_slot node_ptr →⇩r slot_opt →⇩h h'" and
    "¬ 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 ← create_document;
        html ← create_element document_ptr ''html'';
        append_child (cast document_ptr) (cast html);
        head ← create_element document_ptr ''head'';
        append_child (cast html) (cast head);
        body ← create_element document_ptr ''body'';
        append_child (cast html) (cast body);
        e1 ← create_element document_ptr ''div'';
        append_child (cast body) (cast e1);
        e2 ← create_element document_ptr ''div'';
        append_child (cast e1) (cast e2);
        s1 ← attach_shadow_root e1 Open;
        e3 ← create_element document_ptr ''slot'';
        append_child (cast s1) (cast e3);
        return e2
      }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e2 = "|?h0 ⊢ ?P|⇩r"

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

locale l_assigned_nodes_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M =
  l_assigned_nodes_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_get_shadow_root_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M +
  l_find_slot⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M
begin

lemma find_slot_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ find_slot open_flag node_ptr →⇩r Some slot"
  shows "set |h ⊢ get_scdom_component (cast node_ptr)|⇩r ∩ set |h ⊢ get_scdom_component (cast slot)|⇩r = {}"
proof -
  obtain host shadow_root_ptr to where
    "h ⊢ get_parent node_ptr →⇩r Some (cast host)" and
    "h ⊢ get_shadow_root host →⇩r Some shadow_root_ptr" and
    "h ⊢ to_tree_order (cast shadow_root_ptr) →⇩r to" and
    "cast slot ∈ 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 |∈| node_ptr_kinds h"
    using assms(4) find_slot_ptr_in_heap by blast
  then obtain node_ptr_c where node_ptr_c: "h ⊢ get_scdom_component (cast node_ptr) →⇩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 ∈ set node_ptr_c"
    using ‹h ⊢ get_parent node_ptr →⇩r Some (cast host)› 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 ⊢ get_scdom_component (cast host) →⇩r node_ptr_c"
    using ‹h ⊢ get_parent node_ptr →⇩r Some (cast host)› 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 |∈| element_ptr_kinds h"
    using assms(4) find_slot_slot_in_heap by blast
  then obtain slot_c where slot_c: "h ⊢ get_scdom_component (cast slot) →⇩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 (verit, best))
  then have "cast shadow_root_ptr ∈ set slot_c"
    using ‹h ⊢ to_tree_order (cast shadow_root_ptr) →⇩r to› ‹cast slot ∈ set to› 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 ⊢ get_scdom_component (cast shadow_root_ptr) →⇩r slot_c"
    using  ‹h ⊢ get_shadow_root host →⇩r Some shadow_root_ptr› 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 ‹h ⊢ get_shadow_root host →⇩r Some shadow_root_ptr›
      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 ⊢ assigned_nodes element_ptr →⇩r nodes"
  assumes "node_ptr ∈ set nodes"
  shows "set |h ⊢ get_scdom_component (cast element_ptr)|⇩r ∩ set |h ⊢ get_scdom_component (cast node_ptr)|⇩r = {}"
  using assms
proof -
  have "h ⊢ find_slot False node_ptr →⇩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 ⊢ assigned_slot element_ptr →⇩r slot_opt →⇩h h'"
  assumes "∀shadow_root_ptr ∈ fset (shadow_root_ptr_kinds h). h ⊢ get_mode shadow_root_ptr →⇩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 returns_result_eq shadow_root_mode.distinct(1))
    apply (meson 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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M adopt_node_locs⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_def instances)
declare l_assigned_nodes_scope_component⇩S⇩h⇩a⇩d⇩o⇩w⇩_⇩D⇩O⇩M_axioms [instances]
end