Theory Shadow_DOM_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›
theory Shadow_DOM_DOM_Components
  imports
    Shadow_SC_DOM.Shadow_DOM
    Core_DOM_DOM_Components
begin

declare [[smt_timeout = 1200]]

section ‹Shadow root components›


subsection ‹get\_component›

global_interpretation l_get_dom_componentCore_DOM_defs get_root_node get_root_node_locs to_tree_order
  defines get_dom_component = a_get_dom_component
    and is_strongly_dom_component_safe = a_is_strongly_dom_component_safe
    and is_weakly_dom_component_safe = a_is_weakly_dom_component_safe
  .

interpretation i_get_dom_component?: l_get_dom_componentCore_DOM
  heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs to_tree_order 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_disconnected_nodes get_disconnected_nodes_locs get_element_by_id get_elements_by_class_name
  get_elements_by_tag_name
  by(auto simp add: l_get_dom_componentCore_DOM_def l_get_dom_componentCore_DOM_axioms_def
      get_dom_component_def is_strongly_dom_component_safe_def is_weakly_dom_component_safe_def instances)
declare l_get_dom_componentCore_DOM_axioms [instances]




subsection ‹attach\_shadow\_root›

locale l_get_dom_component_attach_shadow_rootCore_DOM =
  l_get_dom_componentCore_DOM heap_is_wellformed parent_child_rel type_wf known_ptr known_ptrs
  to_tree_order 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_disconnected_nodes get_disconnected_nodes_locs get_element_by_id
  get_elements_by_class_name get_elements_by_tag_name +
  l_attach_shadow_rootShadow_DOM known_ptr set_shadow_root set_shadow_root_locs set_mode set_mode_locs
  attach_shadow_root type_wf get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs +
  l_set_modeShadow_DOM type_wf set_mode set_mode_locs +
  l_set_shadow_rootShadow_DOM type_wf set_shadow_root set_shadow_root_locs
  for known_ptr :: "(_::linorder) object_ptr  bool"
    and heap_is_wellformed :: "(_) heap  bool"
    and parent_child_rel :: "(_) heap  ((_) object_ptr × (_) object_ptr) set"
    and type_wf :: "(_) heap  bool"
    and known_ptrs :: "(_) heap  bool"
    and to_tree_order :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
    and get_parent :: "(_) node_ptr  ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap  (_) heap  bool) set"
    and get_child_nodes :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
    and get_dom_component :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
    and get_root_node :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap  (_) heap  bool) set"
    and get_ancestors :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
    and get_ancestors_locs :: "((_) heap  (_) heap  bool) set"
    and get_element_by_id :: "(_) object_ptr  char list  ((_) heap, exception, (_) element_ptr option) prog"
    and get_elements_by_class_name :: "(_) object_ptr  char list  ((_) heap, exception, (_) element_ptr list) prog"
    and get_elements_by_tag_name :: "(_) object_ptr  char list  ((_) heap, exception, (_) element_ptr list) prog"
    and set_shadow_root :: "(_) element_ptr  (_) shadow_root_ptr option  ((_) heap, exception, unit) prog"
    and set_shadow_root_locs :: "(_) element_ptr  ((_) heap, exception, unit) prog set"
    and set_mode :: "(_) shadow_root_ptr  shadow_root_mode  ((_) heap, exception, unit) prog"
    and set_mode_locs :: "(_) shadow_root_ptr  ((_) heap, exception, unit) prog set"
    and attach_shadow_root :: "(_) element_ptr  shadow_root_mode  ((_) heap, exception, (_) shadow_root_ptr) prog"
    and get_disconnected_nodes :: "(_) document_ptr  ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"
    and is_strongly_dom_component_safe :: "(_) object_ptr set  (_) object_ptr set  (_) heap  (_) heap  bool"
    and is_weakly_dom_component_safe :: "(_) object_ptr set  (_) object_ptr set  (_) heap  (_) heap  bool"
    and get_tag_name :: "(_) element_ptr  ((_) heap, exception, char list) prog"
    and get_tag_name_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
    and get_shadow_root :: "(_) element_ptr  ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin

lemma attach_shadow_root_is_weakly_dom_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 h h'"
  assumes "ptr  cast |h  attach_shadow_root element_ptr shadow_root_mode|r"
  assumes "ptr  set |h  get_dom_component (cast element_ptr)|r"
  shows "preserved (get_MObject ptr getter) h h'"
proof -
  obtain h2 h3 new_shadow_root_ptr where
    h2: "h  newShadowRoot_M h h2" and
    new_shadow_root_ptr: "h  newShadowRoot_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(4)
    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(4)
    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)
  have "preserved (get_MObject ptr getter) h h2"
    using h2 new_shadow_root_ptr
    by (metis (no_types, lifting) h  attach_shadow_root element_ptr shadow_root_mode r new_shadow_root_ptr
        assms(5) new_shadow_root_get_MObject select_result_I2)

  have "ptr  cast new_shadow_root_ptr"
    using h  attach_shadow_root element_ptr shadow_root_mode r new_shadow_root_ptr assms(5)
    by auto

  have "preserved (get_MObject ptr getter) h2 h3"
    using set_mode_writes h3
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_mode_locs_def all_args_def)[1]
    using ptr  castshadow_root_ptr2object_ptr new_shadow_root_ptr
    by (metis get_M_Mshadow_root_preserved3a)

  have "element_ptr |∈| element_ptr_kinds h"
    using h  attach_shadow_root element_ptr shadow_root_mode r new_shadow_root_ptr attach_shadow_root_element_ptr_in_heap
    by blast
  have "ptr  cast element_ptr"
    by (metis (no_types, lifting) element_ptr |∈| element_ptr_kinds h assms(1) assms(2) assms(3)
        assms(6) element_ptr_kinds_commutes is_OK_returns_result_E l_get_dom_componentCore_DOM.get_dom_component_ok
        local.get_dom_component_ptr local.l_get_dom_componentCore_DOM_axioms node_ptr_kinds_commutes select_result_I2)

  have "preserved (get_MObject ptr getter) h3 h'"
    using set_shadow_root_writes h'
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_shadow_root_locs_def all_args_def)[1]
    by (metis ptr  castelement_ptr2object_ptr element_ptr get_M_Element_preserved8)

  show ?thesis
    using preserved (get_M ptr getter) h h2 preserved (get_M ptr getter) h2 h3 preserved (get_M ptr getter) h3 h'
    by(auto simp add: preserved_def)
qed
end

interpretation i_get_dom_component_attach_shadow_root?: l_get_dom_component_attach_shadow_rootCore_DOM
  known_ptr heap_is_wellformed parent_child_rel type_wf known_ptrs to_tree_order get_parent
  get_parent_locs get_child_nodes get_child_nodes_locs get_dom_component 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 is_strongly_dom_component_safe is_weakly_dom_component_safe get_tag_name
  get_tag_name_locs get_shadow_root get_shadow_root_locs
  by(auto simp add: l_get_dom_component_attach_shadow_rootCore_DOM_def instances)
declare l_get_dom_component_attach_shadow_rootCore_DOM_axioms [instances]


subsection ‹get\_shadow\_root›

locale l_get_shadow_root_componentShadow_DOM =
  l_get_shadow_root +
  l_heap_is_wellformedShadow_DOM +
  l_get_dom_componentCore_DOM +
  l_get_root_nodeCore_DOM +
  l_get_root_node_wfCore_DOM +
  l_remove_shadow_root_get_child_nodes
begin
lemma get_shadow_root_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h  get_shadow_root host r Some shadow_root_ptr"
  shows "set |h  get_dom_component (cast host)|r  set |h  get_dom_component (cast shadow_root_ptr)|r = {}"
proof -
  have "cast host |∈| object_ptr_kinds h"
    using assms(4) get_shadow_root_ptr_in_heap by auto
  then obtain host_c where host_c: "h  get_dom_component (cast host) r host_c"
    by (meson  assms(1) assms(2) assms(3) get_dom_component_ok is_OK_returns_result_E)
  obtain host_root where host_root: "h  get_root_node (cast host) r host_root"
    by (metis (no_types, lifting) bind_returns_heap_E get_dom_component_def host_c
        is_OK_returns_result_I pure_def pure_eq_iff)

  have "cast shadow_root_ptr |∈| object_ptr_kinds h"
    using get_shadow_root_shadow_root_ptr_in_heap assms shadow_root_ptr_kinds_commutes
    using document_ptr_kinds_commutes by blast
  then obtain shadow_root_ptr_c where shadow_root_ptr_c: "h  get_dom_component (cast shadow_root_ptr) r shadow_root_ptr_c"
    by (meson  assms(1) assms(2) assms(3) get_dom_component_ok is_OK_returns_result_E)
  have "h  get_root_node (cast shadow_root_ptr) r cast shadow_root_ptr"
    using cast shadow_root_ptr |∈| object_ptr_kinds h
    by(auto simp add: get_root_node_def get_ancestors_def intro!: bind_pure_returns_result_I
        split: option.splits)

  have "host_root  cast shadow_root_ptr"
  proof (rule ccontr, simp)
    assume "host_root = castshadow_root_ptr2object_ptr shadow_root_ptr"

    have "(cast shadow_root_ptr, host_root)  (parent_child_rel h)*"
      using host_root = castshadow_root_ptr2object_ptr shadow_root_ptr by auto
    moreover have "(host_root, cast host)  (parent_child_rel h)*"
      using get_root_node_parent_child_rel host_root assms
      by blast
    moreover have "(cast host, cast shadow_root_ptr)  (a_host_shadow_root_rel h)"
      using assms(4) apply(auto simp add: a_host_shadow_root_rel_def)[1]
      by (metis (mono_tags, lifting) get_shadow_root_ptr_in_heap image_eqI is_OK_returns_result_I
          mem_Collect_eq prod.simps(2) select_result_I2)
    moreover have " acyclic (parent_child_rel h  local.a_host_shadow_root_rel h  a_ptr_disconnected_node_rel h)"
      using assms(1)[unfolded heap_is_wellformed_def]
      by auto
    ultimately show False
      using local.parent_child_rel_node_ptr
      by (metis (no_types, lifting) Un_iff host_root = castshadow_root_ptr2object_ptr shadow_root_ptr
          acyclic_def in_rtrancl_UnI rtrancl_into_trancl1)
  qed
  then have "host_c  shadow_root_ptr_c"
    by (metis h  get_root_node (castshadow_root_ptr2object_ptr shadow_root_ptr) r castshadow_root_ptr2object_ptr shadow_root_ptr
        assms(1) assms(2) assms(3) get_dom_component_ptr get_dom_component_root_node_same host_c host_root
        local.get_root_node_parent_child_rel local.get_root_node_same_no_parent_parent_child_rel rtranclE shadow_root_ptr_c)
  then have "set host_c  set shadow_root_ptr_c = {}"
    using assms get_dom_component_no_overlap Shadow_DOM.a_heap_is_wellformed_def host_c shadow_root_ptr_c
    by blast
  then show ?thesis
    using host_c shadow_root_ptr_c
    by auto
qed
end

interpretation i_get_shadow_root_component?: l_get_shadow_root_componentShadow_DOM
  type_wf 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 known_ptr
  heap_is_wellformed parent_child_rel heap_is_wellformedCore_DOM get_host get_host_locs
  get_disconnected_document get_disconnected_document_locs known_ptrs to_tree_order get_parent
  get_parent_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 remove_shadow_root remove_shadow_root_locs
  by(auto simp add: l_get_shadow_root_componentShadow_DOM_def instances)
declare l_get_shadow_root_componentShadow_DOM_axioms [instances]


subsection ‹get\_host›

locale l_get_host_componentShadow_DOM =
  l_heap_is_wellformedShadow_DOM +
  l_get_host +
  l_get_dom_componentCore_DOM  +
  l_get_shadow_root_componentShadow_DOM
begin
lemma get_host_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h  get_host shadow_root_ptr r host"
  shows "set |h  get_dom_component (cast host)|r  set |h  get_dom_component (cast shadow_root_ptr)|r = {}"
proof -
  have "h  get_shadow_root host r Some shadow_root_ptr"
    using assms(1) assms(2) assms(4) local.shadow_root_host_dual by blast
  then show ?thesis
    using assms(1) assms(2) assms(3) local.get_shadow_root_is_component_unsafe by blast
qed
end

interpretation i_get_host_component?: l_get_host_componentShadow_DOM
  get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
  get_shadow_root get_shadow_root_locs get_tag_name get_tag_name_locs known_ptr type_wf heap_is_wellformed
  parent_child_rel heap_is_wellformedCore_DOM get_host get_host_locs get_disconnected_document
  get_disconnected_document_locs known_ptrs to_tree_order get_parent get_parent_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 remove_shadow_root
  remove_shadow_root_locs
  by(auto simp add: l_get_host_componentShadow_DOM_def instances)
declare l_get_host_componentShadow_DOM_axioms [instances]



subsection ‹get\_root\_node\_si›

locale l_get_dom_component_get_root_node_siShadow_DOM =
  l_get_root_node_si_wfShadow_DOM +
  l_get_dom_componentCore_DOM
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_dom_component ptr'|r = set |h  get_dom_component root|r 
set |h  get_dom_component ptr'|r  set |h  get_dom_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 c where "h  get_dom_component ptr' r c"
    by (meson assms(1) assms(2) assms(3) local.get_dom_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 c' where "h  get_dom_component root r c'"
    by (meson assms(1) assms(2) assms(3) local.get_dom_component_ok select_result_I)
  ultimately show ?thesis
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) local.get_dom_component_no_overlap select_result_I2)
qed
end

interpretation i_get_dom_component_get_root_node_si?: l_get_dom_component_get_root_node_siShadow_DOM
  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_wellformedCore_DOM 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
  by(auto simp add: l_get_dom_component_get_root_node_siShadow_DOM_def instances)
declare l_get_dom_component_get_root_node_siShadow_DOM_axioms [instances]



subsection ‹get\_assigned\_nodes›

lemma get_shadow_root_not_weakly_dom_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 element_ptr r shadow_root_ptr_opt h h'" and
    "¬ is_weakly_dom_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

lemma assigned_nodes_not_weakly_dom_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_dom_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 get_composed_root_node_not_weakly_dom_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_dom_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="castelement_ptr2object_ptr ?e3"])
    by code_simp+
qed

lemma assigned_slot_not_weakly_dom_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_dom_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="castelement_ptr2node_ptr ?e2"])
    by code_simp+
qed

locale l_assigned_nodes_componentShadow_DOM =
  l_get_tag_name +
  l_get_child_nodes +
  l_heap_is_wellformedShadow_DOM +
  l_find_slotShadow_DOM +
  l_assigned_nodesShadow_DOM +
  l_assigned_nodes_wfShadow_DOM +
  l_get_dom_componentCore_DOM +
  l_adopt_nodeShadow_DOM +
  l_remove_childCore_DOM +
  l_remove_child_wf2 +
  l_insert_before_wf +
  l_insert_before_wf2 +
  l_append_childCore_DOM +
  l_append_child_wfShadow_DOM +
  l_set_disconnected_nodes_get_tag_name +
  l_set_shadow_root_get_child_nodes +
  l_set_child_nodes_get_tag_name +
  l_get_shadow_root_componentShadow_DOM +
  l_remove_shadow_rootShadow_DOM +
  l_remove_shadow_root_get_tag_name +
  l_set_disconnected_nodes_get_shadow_root +
  l_set_child_nodes_get_shadow_root +
  l_remove_shadow_root_wfShadow_DOM
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_dom_component (cast node_ptr)|r  set |h  get_dom_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_dom_component (cast node_ptr) r node_ptr_c"
    using assms(1) assms(2) assms(3) get_dom_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) get_dom_component_parent_inside assms(1)
      assms(2) assms(3) get_dom_component_ptr
    by blast

  then have "h  get_dom_component (cast host) r node_ptr_c"
    using h  get_parent node_ptr r Some (cast host) get_dom_component_subset a_heap_is_wellformed_def
      assms(1) assms(2) assms(3) node_ptr_c
    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_dom_component (cast slot) r slot_c"
    using a_heap_is_wellformed_def assms(1) assms(2) assms(3) get_dom_component_ok is_OK_returns_result_E
      node_ptr_kinds_commutes[symmetric] element_ptr_kinds_commutes[symmetric]
    by metis
  then have "cast shadow_root_ptr  set slot_c"
    using h  to_tree_order (cast shadow_root_ptr) r to cast slot  set to get_dom_component_to_tree_order
      assms(1) assms(2) assms(3) get_dom_component_ptr
    by blast
  then have "h  get_dom_component (cast shadow_root_ptr) r slot_c"
    using  h  get_shadow_root host r Some shadow_root_ptr get_dom_component_subset assms(1) assms(2)
      assms(3) slot_c
    by blast

  ultimately show ?thesis
    using get_shadow_root_is_component_unsafe assms h  get_shadow_root host r Some shadow_root_ptr
      node_ptr_c slot_c
    by fastforce
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_dom_component (cast element_ptr)|r  set |h  get_dom_component (cast node_ptr)|r = {}"
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 flatten_dom_assigned_nodes_become_children:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h  flatten_dom h h'"
  assumes "h  assigned_nodes slot r nodes"
  assumes "nodes  []"
  shows "h'  get_child_nodes (cast slot) r nodes"
proof -
  obtain tups h2 element_ptrs shadow_root_ptrs where
    "h  element_ptr_kinds_M r element_ptrs" and
    tups: "h  map_filter_M2 (λelement_ptr. do {
      tag  get_tag_name element_ptr;
      assigned_nodes  assigned_nodes element_ptr;
      (if tag = ''slot''  assigned_nodes  [] then return (Some (element_ptr, assigned_nodes))
else return None)}) element_ptrs r tups" (is "h  map_filter_M2 ?f element_ptrs r tups") and
    h2: "h  forall_M (λ(slot, assigned_nodes). do {
      get_child_nodes (cast slot)  forall_M remove;
      forall_M (append_child (cast slot)) assigned_nodes
    }) tups h h2" and
    "h2  shadow_root_ptr_kinds_M r shadow_root_ptrs" and
    h': "h2  forall_M (λshadow_root_ptr. do {
      host  get_host shadow_root_ptr;
      get_child_nodes (cast host)  forall_M remove;
      get_child_nodes (cast shadow_root_ptr)  forall_M (append_child (cast host));
      remove_shadow_root host
    }) shadow_root_ptrs h h'"
    using h  flatten_dom h h'
    apply(auto simp add: flatten_dom_def elim!: bind_returns_heap_E
        bind_returns_heap_E2[rotated, OF ElementMonad.ptr_kinds_M_pure, rotated]
        bind_returns_heap_E2[rotated, OF ShadowRootMonad.ptr_kinds_M_pure, rotated])[1]
    apply(drule pure_returns_heap_eq)
    by(auto intro!: map_filter_M2_pure bind_pure_I)

  have all_tups_slot: "slot assigned_nodes. (slot, assigned_nodes)  set tups 
h  get_tag_name slot r ''slot''"
    using tups
    apply(induct element_ptrs arbitrary: tups)
    by(auto elim!: bind_returns_result_E2 split: if_splits intro!: map_filter_M2_pure bind_pure_I)

  have "distinct element_ptrs"
    using h  element_ptr_kinds_M r element_ptrs
    by auto
  then
  have "distinct tups"
    using tups
    apply(induct element_ptrs arbitrary: tups)
    by(auto elim!: bind_returns_result_E2 intro!: map_filter_M2_pure bind_pure_I
        split: option.splits if_splits intro: map_filter_pure_foo[rotated] )


  have "slot  set element_ptrs"
    using assms(5) assigned_nodes_ptr_in_heap h  element_ptr_kinds_M r element_ptrs
    by auto
  then
  have "(slot, nodes)  set tups"
    apply(rule map_filter_M2_in_result[OF tups])
    apply(auto intro!: bind_pure_I)[1]
    apply(intro bind_pure_returns_result_I)
    using assms assigned_nodes_slot_is_slot
    by(auto intro!: bind_pure_returns_result_I)

  have "slot nodes. (slot, nodes)  set tups  h  assigned_nodes slot r nodes"
    using tups
    apply(induct element_ptrs arbitrary: tups)
    by(auto elim!: bind_returns_result_E2 intro!: map_filter_M2_pure bind_pure_I split: if_splits)
  then
  have elementwise_eq: "slot slot' nodes nodes'. (slot, nodes)  set tups 
(slot', nodes')  set tups  slot = slot'  nodes = nodes'"
    by (meson returns_result_eq)

  have "slot nodes. (slot, nodes)  set tups  distinct nodes"
    using slot nodes. (slot, nodes)  set tups  h  assigned_nodes slot r nodes assigned_nodes_distinct
    using assms(1) by blast

  have "slot slot' nodes nodes'. (slot, nodes)  set tups  (slot', nodes')  set tups  slot  slot'  set nodes  set nodes' = {}"
    using slot nodes. (slot, nodes)  set tups  h  assigned_nodes slot r nodes
      assigned_nodes_different_ptr assms(1) assms(2) assms(3) by blast

  have "h  get_tag_name slot r ''slot''"
    using (slot, nodes)  set tups all_tups_slot by blast
  then have "h2  get_tag_name slot r ''slot''"
    using h2
  proof(induct tups arbitrary: h, simp)
    case (Cons x xs)
    obtain xc ha hb slot' nodes' where
      "x = (slot', nodes')" and
      "h  get_child_nodes (castelement_ptr2object_ptr slot') r xc" and
      ha: "h  forall_M remove xc h ha" and
      hb: "ha  forall_M (append_child (castelement_ptr2object_ptr slot')) nodes' h hb" and
      remainder: "hb  forall_M (λ(slot, assigned_nodes). Heap_Error_Monad.bind
(get_child_nodes (castelement_ptr2object_ptr slot))
(λx. Heap_Error_Monad.bind (forall_M remove x)
(λ_. forall_M (append_child (castelement_ptr2object_ptr slot)) assigned_nodes))) xs h h2"
      using Cons(3)
      by (auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
          bind_returns_result_E bind_returns_result_E2[rotated, OF get_child_nodes_pure, rotated] split: prod.splits)

    have "ha  get_tag_name slot r ''slot''"
      using h  get_tag_name slot r ''slot'' ha
    proof(induct xc arbitrary: h, simp)
      case (Cons a yc)
      obtain hb1 where
        hb1: "h  remove a h hb1" and
        hba: "hb1  forall_M remove yc h ha"
        using Cons
        by (auto elim!: bind_returns_heap_E)
      have "hb1  get_tag_name slot r ''slot''"
        using h  get_tag_name slot r ''slot'' hb1
        by(auto simp add: CD.remove_child_locs_def set_child_nodes_get_tag_name
            set_disconnected_nodes_get_tag_name dest!: reads_writes_separate_forwards[OF get_tag_name_reads
              CD.remove_writes])
      then show ?case
        using hba Cons(1) by simp
    qed
    then
    have "hb  get_tag_name slot r ''slot''"
      using hb
    proof (induct nodes' arbitrary: ha, simp)
      case (Cons a nodes')
      obtain ha1 where
        ha1: "ha  append_child (cast slot') a h ha1" and
        hb: "ha1  forall_M (append_child (cast slot')) nodes' h hb"
        using Cons
        by (auto elim!: bind_returns_heap_E)
      have "ha1  get_tag_name slot r ''slot''"
        using ha  get_tag_name slot r ''slot'' ha1
        by(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def
            CD.adopt_node_locs_def CD.remove_child_locs_def set_child_nodes_get_tag_name
            set_disconnected_nodes_get_tag_name dest!: reads_writes_separate_forwards[OF get_tag_name_reads
              insert_before_writes] split: if_splits)
      then show ?case
        using ha1 hb Cons(1)
        by simp
    qed
    then
    show ?case
      using Cons(1) remainder by simp
  qed

  have "h2  get_child_nodes (cast slot) r nodes  heap_is_wellformed h2  type_wf h2  known_ptrs h2"
    using (slot, nodes)  set tups
    using h2 assms(1) assms(2) assms(3) distinct tups all_tups_slot elementwise_eq
    using slot slot' assigned_nodes nodes'. (slot, assigned_nodes)  set tups 
(slot', nodes')  set tups  slot  slot'  set assigned_nodes  set nodes' = {}
    using slot assigned_nodes. (slot, assigned_nodes)  set tups  distinct assigned_nodes
  proof(induct tups arbitrary: h, simp)
    case (Cons x xs)
    obtain xc ha hb slot' nodes' where
      "x = (slot', nodes')" and
      "h  get_child_nodes (castelement_ptr2object_ptr slot') r xc" and
      ha: "h  forall_M remove xc h ha" and
      hb: "ha  forall_M (append_child (castelement_ptr2object_ptr slot')) nodes' h hb" and
      remainder: "hb  forall_M (λ(slot, assigned_nodes). Heap_Error_Monad.bind
(get_child_nodes (castelement_ptr2object_ptr slot)) (λx. Heap_Error_Monad.bind (forall_M remove x)
(λ_. forall_M (append_child (castelement_ptr2object_ptr slot)) assigned_nodes))) xs h h2"
      using Cons(3)
      by (auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
          bind_returns_result_E bind_returns_result_E2[rotated, OF get_child_nodes_pure, rotated]
          split: prod.splits)

    have "slot assigned_nodes. (slot, assigned_nodes)  set xs  h  get_tag_name slot r ''slot''"
      using Cons by auto

    have "heap_is_wellformed ha" and "type_wf ha" and "known_ptrs ha"
      using Cons(4) Cons(5) Cons(6) h  forall_M remove xc h ha
      apply(induct xc arbitrary: h)
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf remove_child_preserves_known_ptrs
      apply metis
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf remove_child_preserves_known_ptrs
      apply metis
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: CD.remove_def split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf remove_child_preserves_known_ptrs
      apply metis
      done
    then
    have "heap_is_wellformed hb" and "type_wf hb" and "known_ptrs hb"
      using ha  forall_M (append_child (castelement_ptr2object_ptr slot')) nodes' h hb
      apply(induct nodes' arbitrary: ha)
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply metis
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply metis
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply metis
      done

    {
      fix slot assigned_nodes
      assume "(slot, assigned_nodes)  set xs"
      then have "h  get_tag_name slot r ''slot''"
        using slot assigned_nodes. (slot, assigned_nodes)  set xs  h  get_tag_name slot r ''slot''
        by auto
      then have "ha  get_tag_name slot r ''slot''"
        using h  forall_M remove xc h ha
        apply(induct xc arbitrary: h)
        by(auto simp add: CD.remove_child_locs_def set_child_nodes_get_tag_name set_disconnected_nodes_get_tag_name
            dest!: reads_writes_separate_forwards[OF get_tag_name_reads CD.remove_writes]
            elim!: bind_returns_heap_E)
      then have "hb  get_tag_name slot r ''slot''"
        using ha  forall_M (append_child (castelement_ptr2object_ptr slot')) nodes' h hb
        apply(induct nodes' arbitrary: ha)
        by(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def CD.adopt_node_locs_def
            CD.remove_child_locs_def set_child_nodes_get_tag_name set_disconnected_nodes_get_tag_name
            dest!: reads_writes_separate_forwards[OF get_tag_name_reads insert_before_writes]
            elim!: bind_returns_heap_E
            split: if_splits)
    } note tag_names_same = this

    show ?case
    proof(cases "slot' = slot")
      case True
      then
      have "nodes' = nodes"
        using Cons.prems(1) Cons.prems(8) x = (slot', nodes')
        by (metis list.set_intros(1))
      then
      have "(slot, nodes)  set xs"
        using Cons.prems(6) True x = (slot', nodes') by auto

      have "ha  get_child_nodes (castelement_ptr2object_ptr slot) r []"
        using remove_for_all_empty_children Cons.prems(3) Cons.prems(4) Cons.prems(5)
          True h  forall_M remove xc h ha
        using h  get_child_nodes (castelement_ptr2object_ptr slot') r xc
        by blast
      then
      have "hb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes"
        using  append_child_for_all_on_no_children[OF heap_is_wellformed hb type_wf hb known_ptrs hb]
          True nodes' = nodes
        using ha  forall_M (append_child (castelement_ptr2object_ptr slot')) nodes' h hb
        using (slot, nodes)  set tups slot assigned_nodes. (slot, assigned_nodes)  set tups 
distinct assigned_nodes heap_is_wellformed ha known_ptrs ha type_wf ha local.append_child_for_all_on_no_children
        by blast
      with heap_is_wellformed hb and type_wf hb and known_ptrs hb
      show ?thesis
        using (slot, nodes)  set xs remainder
        using slot slot' assigned_nodes nodes'. (slot, assigned_nodes)  set (x#xs) 
(slot', nodes')  set (x#xs)  slot = slot'  assigned_nodes = nodes'
        using (slot, nodes)  set (x # xs)
        using slot slot' assigned_nodes nodes'. (slot, assigned_nodes)  set (x#xs) 
(slot', nodes')  set (x#xs)  slot  slot'  set assigned_nodes  set nodes' = {}
      proof(induct xs arbitrary: hb, simp)
        case (Cons y ys)
        obtain yc hba hbb slot'' nodes'' where
          "y = (slot'', nodes'')" and
          "hb  get_child_nodes (castelement_ptr2object_ptr slot'') r yc" and
          "hb  forall_M remove yc h hba" and
          "hba  forall_M (append_child (castelement_ptr2object_ptr slot'')) nodes'' h hbb" and
          remainder: "hbb  forall_M (λ(slot, assigned_nodes).
Heap_Error_Monad.bind (get_child_nodes (castelement_ptr2object_ptr slot))
(λx. Heap_Error_Monad.bind (forall_M remove x)
(λ_. forall_M (append_child (castelement_ptr2object_ptr slot)) assigned_nodes))) ys h h2"
          using Cons(7)
          by (auto elim!: bind_returns_heap_E
              bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated] split: prod.splits)

        have "slot  slot''"
          by (metis Cons.prems(5) Cons.prems(7) Cons.prems(8) y = (slot'', nodes'')
              list.set_intros(1) list.set_intros(2))
        then have "set nodes  set nodes'' = {}"
          by (metis Cons.prems(8) Cons.prems(9) y = (slot'', nodes'') list.set_intros(1)
              list.set_intros(2))

        have "hba  get_child_nodes (cast slot) r nodes  heap_is_wellformed hba  type_wf hba  known_ptrs hba"
          using hb  get_child_nodes (cast slot) r nodes
          using hb  forall_M remove yc h hba
          using hb  get_child_nodes (castelement_ptr2object_ptr slot'') r yc
          using heap_is_wellformed hb type_wf hb known_ptrs hb
        proof(induct yc arbitrary: hb, simp)
          case (Cons a yc)
          obtain hb1 where
            hb1: "hb  remove a h hb1" and
            hba: "hb1  forall_M remove yc h hba"
            using Cons
            by (auto elim!: bind_returns_heap_E)
          have "hb  get_parent a r Some (cast slot'')"
            using Cons.prems(3) Cons.prems(4) Cons.prems(5) Cons.prems(6) local.child_parent_dual
            by auto

          moreover
          have "heap_is_wellformed hb1" and "type_wf hb1" and "known_ptrs hb1"
            using  hb  remove a h hb1 Cons.prems(4) Cons.prems(5) Cons.prems(6)
              local.remove_child_heap_is_wellformed_preserved
            apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
                bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
            using Cons.prems(4) Cons.prems(5) Cons.prems(6) hb1 local.remove_preserves_type_wf
            apply blast
            using Cons.prems(4) Cons.prems(5) Cons.prems(6) hb1 local.remove_preserves_known_ptrs
            by blast
          moreover have "hb1  get_child_nodes (castelement_ptr2object_ptr slot'') r yc"
            using hb  get_child_nodes (castelement_ptr2object_ptr slot'') r a # yc hb1
            using remove_removes_child heap_is_wellformed hb type_wf hb known_ptrs hb
            by simp
          moreover have "hb1  get_child_nodes (cast slot) r nodes"
            using Cons(2) hb1 CD.set_child_nodes_get_child_nodes_different_pointers
              hb  get_parent a r Some (cast slot'') slot  slot''
            apply(auto simp add: CD.remove_child_locs_def elim!: bind_returns_heap_E
                dest!: reads_writes_separate_forwards[OF get_child_nodes_reads CD.remove_writes])[1]
            by (metis castelement_ptr2node_ptr_inject castnode_ptr2object_ptr_inject)
          ultimately show ?thesis
            using hb1  forall_M remove (yc) h hba Cons
            by auto
        qed


        then have "hbb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes 
heap_is_wellformed hbb  type_wf hbb  known_ptrs hbb"
          using hba  forall_M (append_child (castelement_ptr2object_ptr slot'')) nodes'' h hbb
          using set nodes  set nodes'' = {}
        proof(induct nodes'' arbitrary: hba, simp)
          case (Cons a nodes'')
          then have "hba  get_child_nodes (castelement_ptr2object_ptr slot) r nodes" and
            "heap_is_wellformed hba" and
            "type_wf hba" and
            "known_ptrs hba"
            by auto
          obtain hba1 where
            hba1: "hba  append_child (cast slot'') a h hba1" and
            "hba1  forall_M (append_child (cast slot'')) nodes'' h hbb"
            using Cons(3)
            by (auto elim!: bind_returns_heap_E)

          have "heap_is_wellformed hba1" and "type_wf hba1" and "known_ptrs hba1"
            using Cons.prems(1) hba1 local.append_child_heap_is_wellformed_preserved(1)
            apply blast
            using heap_is_wellformed hba known_ptrs hba type_wf hba hba1 local.append_child_preserves_type_wf
            apply blast
            using Cons.prems(1) hba1 local.append_child_preserves_known_ptrs
            by blast

          moreover
          have "a  set nodes"
            using set nodes  set (a # nodes'') = {}
            by auto


          moreover
          obtain parent_opt where "hba  get_parent a r parent_opt"
            using insert_before_child_in_heap hba1 get_parent_ok unfolding append_child_def
            by (meson Cons.prems(1) is_OK_returns_heap_I is_OK_returns_result_E)
          then
          have "hba1  get_child_nodes (cast slot) r nodes"
          proof (induct parent_opt)
            case None
            then show ?case
              using hba  append_child (cast slot'') a h hba1
              using hba  get_child_nodes (cast slot) r nodes
              using slot  slot''
              apply(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def
                  CD.adopt_node_locs_def remove_child_locs_def elim!: reads_writes_separate_forwards[OF get_child_nodes_reads
                    insert_before_writes])[1]
              by (metis castelement_ptr2node_ptr_inject castnode_ptr2object_ptr_inject
                  CD.set_child_nodes_get_child_nodes_different_pointers)
          next
            case (Some parent)
            have "parent  cast slot"
              apply(rule ccontr, simp)
              using Cons(2)
              apply -
              apply(rule get_parent_child_dual[OF hba  get_parent a r Some parent])
              apply(auto)[1]
              using a  set nodes returns_result_eq
              by fastforce
            show ?case
              apply(rule reads_writes_separate_forwards)
              apply(fact get_child_nodes_reads)
              apply(fact insert_before_writes)
              apply(fact hba  append_child (cast slot'') a h hba1[unfolded append_child_def])
              apply(fact hba  get_child_nodes (cast slot) r nodes)
              using hba  get_parent a r Some parent parent  cast slot slot  slot''
              apply(auto simp add: insert_before_locs_def adopt_node_locs_def CD.adopt_node_locs_def
                  CD.remove_child_locs_def)[1]
              apply (simp_all add: CD.set_child_nodes_get_child_nodes_different_pointers
                  CD.set_disconnected_nodes_get_child_nodes)
              by (metis castelement_ptr2node_ptr_inject castnode_ptr2object_ptr_inject
                  CD.set_child_nodes_get_child_nodes_different_pointers)
          qed
          moreover
          have "set nodes  set nodes'' = {}"
            using Cons.prems(3) by auto
          ultimately show ?case
            using Cons.hyps  hba1  forall_M (append_child (castelement_ptr2object_ptr slot'')) nodes'' h hbb
            by blast
        qed
        show ?case
          apply(rule Cons(1))
          using hbb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes 
heap_is_wellformed hbb  type_wf hbb  known_ptrs hbb
          apply(auto)[1]
          using hbb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes 
heap_is_wellformed hbb  type_wf hbb  known_ptrs hbb
          apply(auto)[1]
          using hbb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes 
heap_is_wellformed hbb  type_wf hbb  known_ptrs hbb
          apply(auto)[1]
          using hbb  get_child_nodes (castelement_ptr2object_ptr slot) r nodes 
heap_is_wellformed hbb  type_wf hbb  known_ptrs hbb
          apply(auto)[1]
          using Cons.prems(5) apply auto[1]
          apply (simp add: remainder)
          using Cons.prems(7) apply auto[1]
          apply (simp add: True nodes' = nodes x = (slot', nodes'))
          by (metis Cons.prems(9) insert_iff list.simps(15))
      qed
    next
      case False
      then have "nodes'  nodes"
        using Cons.prems(1) Cons.prems(9) x = (slot', nodes')
        by (metis assms(6) inf.idem list.set_intros(1) set_empty2)
      then
      have "(slot, nodes)  set xs"
        using Cons.prems(1) x = (slot', nodes')
        by auto
      then show ?thesis
        using Cons(1)[simplified, OF (slot, nodes)  set xs remainder
            heap_is_wellformed hb type_wf hb known_ptrs hb]
        using Cons.prems(6) tag_names_same  Cons.prems(8) Cons.prems(9)
        by (smt (verit) Cons.prems(10) distinct.simps(2) list.set_intros(2))
    qed
  qed
  then
  show ?thesis
    using h' h2  get_tag_name slot r ''slot''
  proof(induct shadow_root_ptrs arbitrary: h2, simp)
    case (Cons shadow_root_ptr shadow_root_ptrs)
    then have "h2  get_child_nodes (castelement_ptr2object_ptr slot) r nodes" and
      "heap_is_wellformed h2" and
      "type_wf h2" and
      "known_ptrs h2"
      by auto
    obtain host h2a h2b h2c host_children shadow_root_children where
      "h2  get_host shadow_root_ptr r host" and
      "h2  get_child_nodes (cast host) r host_children" and
      h2a: "h2  forall_M remove host_children h h2a" and
      "h2a  get_child_nodes (cast shadow_root_ptr) r shadow_root_children" and
      h2b: "h2a  forall_M (append_child (cast host)) shadow_root_children h h2b" and
      "h2b  remove_shadow_root host h h2c" and
      remainder: "h2c  forall_M(λshadow_root_ptr. Heap_Error_Monad.bind (get_host shadow_root_ptr)
        (λhost. Heap_Error_Monad.bind (get_child_nodes (castelement_ptr2object_ptr host))
                     (λx. Heap_Error_Monad.bind (forall_M remove x)
                            (λ_. Heap_Error_Monad.bind (get_child_nodes (castshadow_root_ptr2object_ptr shadow_root_ptr))
                                   (λx. Heap_Error_Monad.bind (forall_M (append_child (castelement_ptr2object_ptr host)) x)
                                          (λ_. remove_shadow_root host))))))
           shadow_root_ptrs
       h h'"
      using Cons(3)
      by(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_host_pure, rotated]
          bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated])


    have "h2  get_shadow_root host r Some shadow_root_ptr"
      using h2  get_host shadow_root_ptr r host shadow_root_host_dual
      using heap_is_wellformed h2 type_wf h2 by blast
    then have "h2a  get_shadow_root host r Some shadow_root_ptr"
      using h2  forall_M remove host_children h h2a
      apply(induct host_children arbitrary: h2)
      by(auto simp add: set_disconnected_nodes_get_shadow_root set_child_nodes_get_shadow_root
          CD.remove_child_locs_def elim!: bind_returns_heap_E
          dest!: reads_writes_separate_forwards[OF get_shadow_root_reads CD.remove_writes])
    then have "h2b  get_shadow_root host r Some shadow_root_ptr"
      using h2a  forall_M (append_child (cast host)) shadow_root_children h h2b
      apply(induct shadow_root_children arbitrary: h2a)
      by(auto simp add: set_disconnected_nodes_get_shadow_root set_child_nodes_get_shadow_root
          append_child_def insert_before_locs_def adopt_node_locs_def CD.adopt_node_locs_def
          CD.remove_child_locs_def elim!: bind_returns_heap_E
          dest!: reads_writes_separate_forwards[OF get_shadow_root_reads insert_before_writes]
          split: if_splits)

    have "host  slot"
    proof (rule ccontr, simp)
      assume "host = slot"
      show False
        using get_host_valid_tag_name[OF heap_is_wellformed h2 type_wf h2
            h2  get_host shadow_root_ptr r host[unfolded host = slot] h2  get_tag_name slot r ''slot'']
        by(simp)
    qed

    have "heap_is_wellformed h2a" and "type_wf h2a" and "known_ptrs h2a"
      using heap_is_wellformed h2 and type_wf h2 and known_ptrs h2 h2  forall_M remove host_children h h2a
      apply(induct host_children arbitrary: h2)
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
        remove_child_preserves_known_ptrs apply metis
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
        remove_child_preserves_known_ptrs apply metis
      apply(auto simp add: CD.remove_def elim!: bind_returns_heap_E
          bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
      using remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
        remove_child_preserves_known_ptrs apply metis
      done
    then
    have "heap_is_wellformed h2b" and "type_wf h2b" and "known_ptrs h2b"
      using h2a  forall_M (append_child (cast host)) shadow_root_children h h2b
      apply(induct shadow_root_children arbitrary: h2a)
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply(metis)
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply(metis)
      apply(auto simp add: append_child_def elim!: bind_returns_heap_E)[1]
      using insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf insert_before_preserves_known_ptrs
      apply(metis)
      done
    then
    have "heap_is_wellformed h2c" and "type_wf h2c" and "known_ptrs h2c"
      using remove_shadow_root_preserves h2b  remove_shadow_root host h h2c
      by blast+

    moreover
    have "h2a  get_child_nodes (castelement_ptr2object_ptr slot) r nodes"
      using h2  get_child_nodes (castelement_ptr2object_ptr slot) r nodes
      using h2  forall_M remove host_children h h2a
      using h2  get_child_nodes (cast host) r host_children
      using heap_is_wellformed h2 type_wf h2 known_ptrs h2
    proof (induct host_children arbitrary: h2, simp)
      case (Cons a host_children)
      obtain h21 where "h2  remove a h h21" and
        "h21  forall_M remove host_children h h2a"
        using Cons(3)
        by(auto elim!: bind_returns_heap_E)

      have "heap_is_wellformed h21" and "type_wf h21" and "known_ptrs h21"
        using Cons.prems(4) Cons.prems(5) Cons.prems(6) h2  remove a h h21 local.remove_heap_is_wellformed_preserved
        apply blast
        using Cons.prems(4) Cons.prems(5) Cons.prems(6) h2  remove a h h21 local.remove_preserves_type_wf
        apply blast
        using Cons.prems(4) Cons.prems(5) Cons.prems(6) h2  remove a h h21 local.remove_preserves_known_ptrs
        by blast
      have "h2  get_parent a r Some (cast host)"
        using h2  get_child_nodes (castelement_ptr2object_ptr host) r a # host_children
        using heap_is_wellformed h2 type_wf h2 known_ptrs h2 child_parent_dual
        using heap_is_wellformed_def by auto
      then have "h21  get_child_nodes (castelement_ptr2object_ptr slot) r nodes"
        using h2  get_child_nodes (castelement_ptr2object_ptr slot) r nodes host  slot
        using h2  remove a h h21
        apply(auto simp add: CD.remove_child_locs_def CD.set_disconnected_nodes_get_child_nodes
            dest!: reads_writes_preserved[OF get_child_nodes_reads CD.remove_writes])[1]
        by (meson castelement_ptr2node_ptr_inject castnode_ptr2object_ptr_inject
            CD.set_child_nodes_get_child_nodes_different_pointers)
      moreover have "h21  get_child_nodes (castelement_ptr2object_ptr host) r host_children"
        using h2  remove a h h21  remove_removes_child[OF heap_is_wellformed h2 type_wf h2
            known_ptrs h2 h2  get_child_nodes (castelement_ptr2object_ptr host) r a # host_children]
        by blast
      ultimately show ?case
        using heap_is_wellformed h21 and type_wf h21 and known_ptrs h21
          h21  forall_M remove host_children h h2a Cons(1)
        using Cons.prems(3) Cons.prems(4) Cons.prems(5) Cons.prems(6) heap_is_wellformed_def
          h2  remove a h h21 remove_removes_child
        by blast
    qed

    then
    have "h2b  get_child_nodes (castelement_ptr2object_ptr slot) r nodes"
      using h2a  forall_M (append_child (cast host)) shadow_root_children h h2b
      using h2a  get_child_nodes (cast shadow_root_ptr) r shadow_root_children
      using heap_is_wellformed h2a type_wf h2a known_ptrs h2a
    proof(induct shadow_root_children arbitrary: h2a, simp)
      case (Cons a shadow_root_children)
      obtain h2a1 where "h2a  append_child (castelement_ptr2object_ptr host) a h h2a1" and
        "h2a1  forall_M (append_child (castelement_ptr2object_ptr host)) (shadow_root_children) h h2b"
        using Cons(3)
        by(auto elim!: bind_returns_heap_E)

      have "heap_is_wellformed h2a1" and "type_wf h2a1" and "known_ptrs h2a1"
        using Cons.prems(4) Cons.prems(5) Cons.prems(6) h2a  append_child (castelement_ptr2object_ptr host) a h h2a1
          local.append_child_heap_is_wellformed_preserved by blast+
      moreover have "h2a1  get_child_nodes (cast shadow_root_ptr) r shadow_root_children"
        using h2a  get_child_nodes (cast shadow_root_ptr) r a # shadow_root_children
        using insert_before_removes_child h2a  append_child (castelement_ptr2object_ptr host) a h h2a1[unfolded append_child_def]
        using heap_is_wellformed h2a type_wf h2a known_ptrs h2a
        using cast_document_ptr_not_node_ptr(2) by blast
      moreover have "h2a  get_parent a r Some (cast shadow_root_ptr)"
        using h2a  get_child_nodes (castshadow_root_ptr2object_ptr shadow_root_ptr) r a # shadow_root_children
        using heap_is_wellformed h2a type_wf h2a known_ptrs h2a child_parent_dual
        using heap_is_wellformed_def by auto
      then have "h2a1  get_child_nodes (cast slot) r nodes"
        using h2a  get_child_nodes (castelement_ptr2object_ptr slot) r nodes
        using h2a  append_child (castelement_ptr2object_ptr host) a h h2a1 host  slot
        apply(auto simp add:  set_disconnected_nodes_get_child_nodes append_child_def
            insert_before_locs_def adopt_node_locs_def CD.adopt_node_locs_def CD.remove_child_locs_def
            elim!: bind_returns_heap_E dest!: reads_writes_preserved[OF get_child_nodes_reads insert_before_writes])[1]
        using CD.set_child_nodes_get_child_nodes_different_pointers castelement_ptr2node_ptr_inject
          castnode_ptr2object_ptr_inject cast_document_ptr_not_node_ptr(2)
        by metis+
      ultimately
      show ?case
        using Cons(1) h2a1  forall_M (append_child (castelement_ptr2object_ptr host)) shadow_root_children h h2b
        by blast
    qed
    then
    have "h2c  get_child_nodes (castelement_ptr2object_ptr slot) r nodes"
      using h2b  remove_shadow_root host h h2c
      by(auto simp add: remove_shadow_root_get_child_nodes_different_pointers[OF
            cast_document_ptr_not_node_ptr(2)] dest!: reads_writes_separate_forwards[OF get_child_nodes_reads
            remove_shadow_root_writes])

    moreover
    have "h2a  get_tag_name slot r ''slot''"
      using h2a h2  get_tag_name slot r ''slot''
      apply(induct host_children arbitrary: h2)
      by(auto simp add: CD.remove_child_locs_def set_disconnected_nodes_get_tag_name
          set_child_nodes_get_tag_name dest!: reads_writes_separate_forwards[OF get_tag_name_reads CD.remove_writes]
          elim!: bind_returns_heap_E)
    then
    have "h2b  get_tag_name slot r ''slot''"
      using h2b
      apply(induct shadow_root_children arbitrary: h2a)
      by(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def
          CD.adopt_node_locs_def CD.remove_child_locs_def set_disconnected_nodes_get_tag_name
          set_child_nodes_get_tag_name dest!: reads_writes_separate_forwards[OF get_tag_name_reads insert_before_writes]
          elim!: bind_returns_heap_E split: if_splits)
    then
    have "h2c  get_tag_name slot r ''slot''"
      using h2b  remove_shadow_root host h h2c
      by(auto simp add: remove_shadow_root_get_tag_name dest!:
          reads_writes_separate_forwards[OF get_tag_name_reads remove_shadow_root_writes])

    ultimately show ?case
      using Cons(1) remainder
      by auto
  qed
qed
end

interpretation i_assigned_nodes_component?: l_assigned_nodes_componentShadow_DOM
  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_wellformedCore_DOM 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_nodeCore_DOM adopt_node_locsCore_DOM set_child_nodes set_child_nodes_locs
  by(auto simp add: l_assigned_nodes_componentShadow_DOM_def instances)
declare l_assigned_nodes_componentShadow_DOM_axioms [instances]


subsubsection ‹get\_owner\_document›

locale l_get_owner_document_componentShadow_DOM =
  l_get_owner_document_wfShadow_DOM +
  l_get_dom_componentCore_DOM
begin
lemma get_owner_document_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h  get_owner_document ptr r owner_document"
  assumes "¬is_document_ptr_kind |h  get_root_node ptr|r"
  shows "set |h  get_dom_component ptr|r  set |h  get_dom_component (cast owner_document)|r = {}"
proof -
  have "owner_document |∈| document_ptr_kinds h"
    using assms(1) assms(2) assms(3) assms(4) get_owner_document_owner_document_in_heap by blast
  have "ptr |∈| object_ptr_kinds h"
    by (meson assms(4) is_OK_returns_result_I local.get_owner_document_ptr_in_heap)
  obtain root where root: "h  get_root_node ptr r root"
    by (meson assms(1) assms(2) assms(3) assms(4) is_OK_returns_result_I
        local.get_owner_document_ptr_in_heap local.get_root_node_ok returns_result_select_result)
  then obtain to where to: "h  to_tree_order root r to"
    by (meson assms(1) assms(2) assms(3) is_OK_returns_result_E local.get_root_node_root_in_heap
        local.to_tree_order_ok)
  then have "p  set to. ¬is_document_ptr_kind p"
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(5) document_ptr_casts_commute3
        local.to_tree_order_node_ptrs node_ptr_no_document_ptr_cast root select_result_I2)
  then have "cast owner_document  set |h  get_dom_component ptr|r"
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) assms(5) document_ptr_document_ptr_cast
        is_OK_returns_result_I l_get_dom_componentCore_DOM.get_dom_component_ok local.get_dom_component_root_node_same
        local.get_root_node_not_node_same local.get_root_node_ptr_in_heap local.l_get_dom_componentCore_DOM_axioms
        node_ptr_no_document_ptr_cast returns_result_select_result root select_result_I2)
  then have "|h  get_dom_component ptr|r  |h  get_dom_component (cast owner_document)|r"
    by (metis (no_types, lifting) owner_document |∈| document_ptr_kinds h assms(1) assms(2) assms(3)
        document_ptr_kinds_commutes l_get_dom_componentCore_DOM.get_dom_component_ok local.get_dom_component_ptr
        local.l_get_dom_componentCore_DOM_axioms returns_result_select_result)
  then show ?thesis
    by (meson owner_document |∈| document_ptr_kinds h ptr |∈| object_ptr_kinds h assms(1) assms(2)
        assms(3) document_ptr_kinds_commutes l_get_dom_componentCore_DOM.get_dom_component_no_overlap
        l_get_dom_componentCore_DOM.get_dom_component_ok local.l_get_dom_componentCore_DOM_axioms returns_result_select_result)
qed

end

interpretation i_get_owner_document_component?: l_get_owner_document_componentShadow_DOM
  type_wf get_disconnected_nodes get_disconnected_nodes_locs known_ptr get_child_nodes get_child_nodes_locs
  DocumentClass.known_ptr get_parent get_parent_locs DocumentClass.type_wf get_root_node get_root_node_locs
  CD.a_get_owner_document get_host get_host_locs get_owner_document get_shadow_root get_shadow_root_locs
  get_tag_name get_tag_name_locs heap_is_wellformed parent_child_rel heap_is_wellformedCore_DOM
  get_disconnected_document get_disconnected_document_locs known_ptrs get_ancestors get_ancestors_locs to_tree_order
  get_dom_component is_strongly_dom_component_safe is_weakly_dom_component_safe get_element_by_id
  get_elements_by_class_name get_elements_by_tag_name
  by(auto simp add: l_get_owner_document_componentShadow_DOM_def instances)
declare l_get_owner_document_componentShadow_DOM_axioms [instances]

definition is_shadow_root_component :: "(_) object_ptr list  bool"
  where
    "is_shadow_root_component c = is_shadow_root_ptr_kind (hd c)"

end