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