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

section \<open>Shadow Root Components\<close>

theory Shadow_DOM_Components
  imports
    Shadow_DOM.Shadow_DOM
    Core_DOM_Components
begin

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

global_interpretation l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_defs get_root_node get_root_node_locs to_tree_order
  defines get_component = a_get_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_component?: l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  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_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_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms_def get_component_def
      is_strongly_dom_component_safe_def is_weakly_dom_component_safe_def instances)
declare l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]



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

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

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

locale l_get_dom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M 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_component_safe is_weakly_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_root\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M 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_mode\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf set_mode set_mode_locs +
  l_set_shadow_root\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M type_wf set_shadow_root set_shadow_root_locs
  for known_ptr :: "(_::linorder) object_ptr \<Rightarrow> bool"
    and heap_is_wellformed :: "(_) heap \<Rightarrow> bool"
    and parent_child_rel :: "(_) heap \<Rightarrow> ((_) object_ptr \<times> (_) object_ptr) set"
    and type_wf :: "(_) heap \<Rightarrow> bool"
    and known_ptrs :: "(_) heap \<Rightarrow> bool"
    and to_tree_order :: "(_) object_ptr \<Rightarrow> ((_) heap, exception, (_) object_ptr list) prog"
    and get_parent :: "(_) node_ptr \<Rightarrow> ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and get_child_nodes :: "(_) object_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and get_dom_component :: "(_) object_ptr \<Rightarrow> ((_) heap, exception, (_) object_ptr list) prog"
    and get_root_node :: "(_) object_ptr \<Rightarrow> ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and get_ancestors :: "(_) object_ptr \<Rightarrow> ((_) heap, exception, (_) object_ptr list) prog"
    and get_ancestors_locs :: "((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and get_element_by_id ::
    "(_) object_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr option) prog"
    and get_elements_by_class_name ::
    "(_) object_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr list) prog"
    and get_elements_by_tag_name ::
    "(_) object_ptr \<Rightarrow> char list \<Rightarrow> ((_) heap, exception, (_) element_ptr list) prog"
    and set_shadow_root ::
    "(_) element_ptr \<Rightarrow> (_) shadow_root_ptr option \<Rightarrow> ((_) heap, exception, unit) prog"
    and set_shadow_root_locs :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
    and set_mode :: "(_) shadow_root_ptr \<Rightarrow> shadow_root_mode \<Rightarrow> ((_) heap, exception, unit) prog"
    and set_mode_locs :: "(_) shadow_root_ptr \<Rightarrow> ((_) heap, exception, unit) prog set"
    and attach_shadow_root ::
    "(_) element_ptr \<Rightarrow> shadow_root_mode \<Rightarrow> ((_) heap, exception, (_) shadow_root_ptr) prog"
    and get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and is_strongly_component_safe ::
    "(_) object_ptr set \<Rightarrow> (_) object_ptr set \<Rightarrow> (_) heap \<Rightarrow> (_) heap \<Rightarrow> bool"
    and is_weakly_component_safe ::
    "(_) object_ptr set \<Rightarrow> (_) object_ptr set \<Rightarrow> (_) heap \<Rightarrow> (_) heap \<Rightarrow> bool"
    and get_tag_name :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, char list) prog"
    and get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
    and get_shadow_root :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, (_) shadow_root_ptr option) prog"
    and get_shadow_root_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> 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 \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>h h'"
  assumes "ptr \<noteq> cast |h \<turnstile> attach_shadow_root element_ptr shadow_root_mode|\<^sub>r"
  assumes "ptr \<notin> set |h \<turnstile> get_dom_component (cast element_ptr)|\<^sub>r"
  shows "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h'"
proof -
  obtain h2 h3 new_shadow_root_ptr where
    h2: "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h2" and
    new_shadow_root_ptr: "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr" and
    h3: "h2 \<turnstile> set_mode new_shadow_root_ptr shadow_root_mode \<rightarrow>\<^sub>h h3" and
    h': "h3 \<turnstile> set_shadow_root element_ptr (Some new_shadow_root_ptr) \<rightarrow>\<^sub>h h'"
    using assms(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 \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr"
    using new_shadow_root_ptr h2 h3 h'
    using assms(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_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr getter) h h2"
    using h2 new_shadow_root_ptr
    by (metis (no_types, lifting)
        \<open>h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr\<close> assms(5)
        new_shadow_root_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t select_result_I2)

  have "ptr \<noteq> cast new_shadow_root_ptr"
    using \<open>h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr\<close> assms(5)
    by auto

  have "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t 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 \<open>ptr \<noteq> cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r new_shadow_root_ptr\<close>
    by (metis get_M_Mshadow_root_preserved3)

  have "element_ptr |\<in>| element_ptr_kinds h"
    using \<open>h \<turnstile> attach_shadow_root element_ptr shadow_root_mode \<rightarrow>\<^sub>r new_shadow_root_ptr\<close>
      attach_shadow_root_element_ptr_in_heap
    by blast
  have "ptr \<noteq> cast element_ptr"
    by (metis (no_types, lifting) \<open>element_ptr |\<in>| element_ptr_kinds h\<close> assms(1) assms(2) assms(3)
        assms(6) element_ptr_kinds_commutes is_OK_returns_result_E get_component_ok local.get_dom_component_ptr
        node_ptr_kinds_commutes select_result_I2)

  have "preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t 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 \<open>ptr \<noteq> cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r element_ptr\<close> get_M_Element_preserved8)

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

interpretation i_get_dom_component_attach_shadow_root?: l_get_dom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  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_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_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_dom_component_attach_shadow_root\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


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

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

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

locale l_get_shadow_root_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_shadow_root +
  l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_root_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  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 \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
  shows "set |h \<turnstile> get_component (cast host)|\<^sub>r \<inter> set |h \<turnstile> get_component (cast shadow_root_ptr)|\<^sub>r = {}"
proof -
  have "cast host |\<in>| object_ptr_kinds h"
    using assms(4) get_shadow_root_ptr_in_heap by auto
  then obtain host_c where host_c: "h \<turnstile> get_component (cast host) \<rightarrow>\<^sub>r host_c"
    by (meson  assms(1) assms(2) assms(3) get_component_ok is_OK_returns_result_E)
  obtain host_root where host_root: "h \<turnstile> get_root_node (cast host) \<rightarrow>\<^sub>r host_root"
    by (metis (no_types, lifting) bind_returns_heap_E get_component_def host_c is_OK_returns_result_I
        pure_def pure_eq_iff)

  have "cast shadow_root_ptr |\<in>| 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 \<turnstile> get_component (cast shadow_root_ptr) \<rightarrow>\<^sub>r shadow_root_ptr_c"
    by (meson  assms(1) assms(2) assms(3) get_component_ok is_OK_returns_result_E)
  have "h \<turnstile> get_root_node (cast shadow_root_ptr) \<rightarrow>\<^sub>r cast shadow_root_ptr"
    using \<open>cast shadow_root_ptr |\<in>| object_ptr_kinds h\<close>
    by(auto simp add: get_root_node_def get_ancestors_def intro!: bind_pure_returns_result_I
        split: option.splits)

  have "host_root \<noteq> cast shadow_root_ptr"
  proof (rule ccontr, simp)
    assume "host_root = cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr"

    have "(cast shadow_root_ptr, host_root) \<in> (parent_child_rel h)\<^sup>*"
      using \<open>host_root = cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr\<close> by auto
    moreover have "(host_root, cast host) \<in> (parent_child_rel h)\<^sup>*"
      using get_root_node_parent_child_rel host_root assms
      by blast
    moreover have "(cast host, cast shadow_root_ptr) \<in> (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 \<union> local.a_host_shadow_root_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 \<open>host_root = cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr\<close>
          acyclic_def in_rtrancl_UnI rtrancl_into_trancl1)
  qed
  then have "host_c \<noteq> shadow_root_ptr_c"
    by (metis \<open>h \<turnstile> get_root_node (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr) \<rightarrow>\<^sub>r cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r
shadow_root_ptr\<close> assms(1) assms(2) assms(3) get_dom_component_ptr get_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 \<inter> 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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  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_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs
  get_disconnected_document get_disconnected_document_locs known_ptrs to_tree_order get_parent
  get_parent_locs get_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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_shadow_root_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


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

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

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

locale l_get_host_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_host +
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M  +
  l_get_shadow_root_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma get_host_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r host"
  shows "set |h \<turnstile> get_component (cast host)|\<^sub>r \<inter> set |h \<turnstile> get_component (cast shadow_root_ptr)|\<^sub>r = {}"
proof -
  have "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  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_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs get_disconnected_document
  get_disconnected_document_locs known_ptrs to_tree_order get_parent get_parent_locs get_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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_host_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]



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

locale l_get_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_root_node_si_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin

lemma get_root_node_si_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_root_node_si ptr' \<rightarrow>\<^sub>r root"
  shows "set |h \<turnstile> get_component ptr'|\<^sub>r = set |h \<turnstile> get_component root|\<^sub>r \<or>
set |h \<turnstile> get_component ptr'|\<^sub>r \<inter> set |h \<turnstile> get_component root|\<^sub>r = {}"
proof -
  have "ptr' |\<in>| object_ptr_kinds h"
    using get_ancestors_si_ptr_in_heap assms(4)
    by(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)
  then
  obtain c where "h \<turnstile> get_component ptr' \<rightarrow>\<^sub>r c"
    by (meson assms(1) assms(2) assms(3) local.get_component_ok select_result_I)
  moreover
  have "root |\<in>| object_ptr_kinds h"
    using get_ancestors_si_ptr assms(4)
    apply(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)[1]
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) empty_iff empty_set
        get_ancestors_si_ptrs_in_heap last_in_set)
  then
  obtain c' where "h \<turnstile> get_component root \<rightarrow>\<^sub>r c'"
    by (meson assms(1) assms(2) assms(3) local.get_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_component_get_root_node_si?: l_get_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs
  get_host get_host_locs get_ancestors_si get_ancestors_si_locs get_root_node_si get_root_node_si_locs
  get_disconnected_nodes get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs get_tag_name
  get_tag_name_locs heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_document
  get_disconnected_document_locs to_tree_order get_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_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_component_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]



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

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

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

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

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

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

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

locale l_assigned_nodes_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_tag_name +
  l_get_child_nodes +
  l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_find_slot\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_assigned_nodes\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_assigned_nodes_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_adopt_node\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_remove_child\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_remove_child_wf2 +
  l_insert_before_wf +
  l_insert_before_wf2 +
  l_insert_before\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M _ _ _ _ _ _ get_ancestors_si get_ancestors_si_locs +
  l_append_child\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_append_child_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M  _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ get_ancestors_si get_ancestors_si_locs +
  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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_remove_shadow_root\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  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_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma find_slot_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> find_slot open_flag node_ptr \<rightarrow>\<^sub>r Some slot"
  shows "set |h \<turnstile> get_component (cast node_ptr)|\<^sub>r \<inter> set |h \<turnstile> get_component (cast slot)|\<^sub>r = {}"
proof -
  obtain host shadow_root_ptr to where
    "h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some (cast host)" and
    "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr" and
    "h \<turnstile> to_tree_order (cast shadow_root_ptr) \<rightarrow>\<^sub>r to" and
    "cast slot \<in> set to"
    using assms(4)
    apply(auto simp add: find_slot_def first_in_tree_order_def elim!: bind_returns_result_E2
        map_filter_M_pure_E[where y=slot]
        split: option.splits if_splits list.splits intro!: map_filter_M_pure bind_pure_I)[1]
    by (metis element_ptr_casts_commute3)+

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

  then have "cast host \<in> set node_ptr_c"
    using \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some (cast host)\<close> get_component_parent_inside assms(1)
      assms(2) assms(3) get_dom_component_ptr
    by blast

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

  moreover have "slot |\<in>| element_ptr_kinds h"
    using assms(4) find_slot_slot_in_heap by blast
  then obtain slot_c where slot_c: "h \<turnstile> get_component (cast slot) \<rightarrow>\<^sub>r slot_c"
    using a_heap_is_wellformed_def assms(1) assms(2) assms(3) get_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 \<in> set slot_c"
    using \<open>h \<turnstile> to_tree_order (cast shadow_root_ptr) \<rightarrow>\<^sub>r to\<close> \<open>cast slot \<in> set to\<close>
      get_component_to_tree_order assms(1) assms(2) assms(3) get_dom_component_ptr
    by blast
  then have "h \<turnstile> get_component (cast shadow_root_ptr) \<rightarrow>\<^sub>r slot_c"
    using  \<open>h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr\<close> get_component_subset assms(1) assms(2)
      assms(3) slot_c
    by blast

  ultimately show ?thesis
    using get_shadow_root_is_component_unsafe assms \<open>h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr\<close>
      node_ptr_c slot_c
    by fastforce
qed

lemma assigned_slot_pure:
  "pure (assigned_slot node_ptr) h"
  apply(auto simp add: assigned_slot_def a_find_slot_def intro!: bind_pure_I  split: option.splits)[1]
  by(auto simp add: first_in_tree_order_def intro!: bind_pure_I map_filter_M_pure split: list.splits)

lemma assigned_slot_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> assigned_slot node_ptr \<rightarrow>\<^sub>r slot_opt \<rightarrow>\<^sub>h h'"
  assumes "\<forall>shadow_root_ptr \<in> fset (shadow_root_ptr_kinds h). h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Closed"
  shows "is_strongly_dom_component_safe {cast node_ptr} (cast ` set_option slot_opt) h h'"
proof -
  have "h = h'"
    using assms(5) assigned_slot_pure
    by (meson assms(4) pure_returns_heap_eq returns_result_heap_def)
  obtain parent_opt where parent_opt: "h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r parent_opt"
    using assms(4)
    by (auto simp add: assigned_slot_def a_find_slot_def returns_result_heap_def
        elim!: bind_returns_result_E2 split: option.splits split: if_splits)
  then
  have "slot_opt = None"
  proof (induct parent_opt)
    case None
    then show ?case
      using assms(4)
      apply(auto simp add: assigned_slot_def a_find_slot_def returns_result_heap_def
          elim!: bind_returns_result_E2 split: option.splits split: if_splits)[1]
      by (meson option.distinct(1) returns_result_eq)+
  next
    case (Some parent)
    then show ?case
    proof (cases "is_element_ptr_kind parent")
      case True
      then obtain host where host: "parent = cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host"
        by (metis (no_types, lifting) case_optionE element_ptr_casts_commute3 node_ptr_casts_commute)
      moreover have "host |\<in>| element_ptr_kinds h"
        using Some.prems element_ptr_kinds_commutes host local.get_parent_parent_in_heap
          node_ptr_kinds_commutes
        by blast
      ultimately obtain shadow_root_opt where shadow_root_opt:
        "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r shadow_root_opt"
        using get_shadow_root_ok
        by (meson assms(2) is_OK_returns_result_E)
      then show ?thesis
      proof (induct shadow_root_opt)
        case None
        then show ?case
          using assms(4)
          apply(auto dest!: returns_result_eq[OF \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some parent\<close>]
              simp add: assigned_slot_def a_find_slot_def returns_result_heap_def elim!: bind_returns_result_E2
              split: option.splits split: if_splits)[1]
          using host select_result_I2 by fastforce+
      next
        case (Some shadow_root_ptr)
        have "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
          using Some.prems assms(1) local.get_shadow_root_shadow_root_ptr_in_heap by blast
        then
        have "h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Closed"
          using assms by simp
        have "\<not>h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Open"
        proof (rule ccontr, simp)
          assume "h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Open"
          then have "Open = Closed"
            using returns_result_eq  \<open>h \<turnstile> get_mode shadow_root_ptr \<rightarrow>\<^sub>r Closed\<close>
            by fastforce
          then show False
            by simp
        qed
        then show ?case
          using assms(4) Some parent_opt host
          by(auto dest!: returns_result_eq[OF \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some parent\<close>]
              returns_result_eq[OF \<open>h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr\<close>]
              simp add: assigned_slot_def a_find_slot_def returns_result_heap_def
              elim!: bind_returns_result_E2 split: option.splits split: if_splits)
      qed
    next
      case False
      then show ?thesis
        using assms(4)
        by(auto dest!: returns_result_eq[OF \<open>h \<turnstile> get_parent node_ptr \<rightarrow>\<^sub>r Some parent\<close>]
            simp add: assigned_slot_def a_find_slot_def returns_result_heap_def
            elim!: bind_returns_result_E2 split: option.splits split: if_splits)
    qed
  qed
  then show ?thesis
    using \<open>h = h'\<close>
    by(auto simp add: is_strongly_dom_component_safe_def preserved_def)
qed

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

lemma flatten_dom_assigned_nodes_become_children:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> flatten_dom \<rightarrow>\<^sub>h h'"
  assumes "h \<turnstile> assigned_nodes slot \<rightarrow>\<^sub>r nodes"
  assumes "nodes \<noteq> []"
  shows "h' \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes"
proof -
  obtain tups h2 element_ptrs shadow_root_ptrs where
    "h \<turnstile> element_ptr_kinds_M \<rightarrow>\<^sub>r element_ptrs" and
    tups: "h \<turnstile> map_filter_M2 (\<lambda>element_ptr. do {
      tag \<leftarrow> get_tag_name element_ptr;
      assigned_nodes \<leftarrow> assigned_nodes element_ptr;
      (if tag = ''slot'' \<and> assigned_nodes \<noteq> [] then return (Some (element_ptr, assigned_nodes))
else return None)}) element_ptrs \<rightarrow>\<^sub>r tups" (is "h \<turnstile> map_filter_M2 ?f element_ptrs \<rightarrow>\<^sub>r tups") and
    h2: "h \<turnstile> forall_M (\<lambda>(slot, assigned_nodes). do {
      get_child_nodes (cast slot) \<bind> forall_M remove;
      forall_M (append_child (cast slot)) assigned_nodes
    }) tups \<rightarrow>\<^sub>h h2" and
    "h2 \<turnstile> shadow_root_ptr_kinds_M \<rightarrow>\<^sub>r shadow_root_ptrs" and
    h': "h2 \<turnstile> forall_M (\<lambda>shadow_root_ptr. do {
      host \<leftarrow> get_host shadow_root_ptr;
      get_child_nodes (cast host) \<bind> forall_M remove;
      get_child_nodes (cast shadow_root_ptr) \<bind> forall_M (append_child (cast host));
      remove_shadow_root host
    }) shadow_root_ptrs \<rightarrow>\<^sub>h h'"
    using \<open>h \<turnstile> flatten_dom \<rightarrow>\<^sub>h h'\<close>
    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: "\<And>slot assigned_nodes. (slot, assigned_nodes) \<in> set tups \<Longrightarrow>
h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>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 \<open>h \<turnstile> element_ptr_kinds_M \<rightarrow>\<^sub>r element_ptrs\<close>
    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 \<in> set element_ptrs"
    using assms(5) assigned_nodes_ptr_in_heap \<open>h \<turnstile> element_ptr_kinds_M \<rightarrow>\<^sub>r element_ptrs\<close>
    by auto
  then
  have "(slot, nodes) \<in> 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 "\<And>slot nodes. (slot, nodes) \<in> set tups \<Longrightarrow> h \<turnstile> assigned_nodes slot \<rightarrow>\<^sub>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: "\<And>slot slot' nodes nodes'. (slot, nodes) \<in> set tups \<Longrightarrow>
(slot', nodes') \<in> set tups \<Longrightarrow> slot = slot' \<Longrightarrow> nodes = nodes'"
    by (meson returns_result_eq)

  have "\<And>slot nodes. (slot, nodes) \<in> set tups \<Longrightarrow> distinct nodes"
    using \<open>\<And>slot nodes. (slot, nodes) \<in> set tups \<Longrightarrow> h \<turnstile> assigned_nodes slot \<rightarrow>\<^sub>r nodes\<close>
      assigned_nodes_distinct
    using assms(1) by blast

  have "\<And>slot slot' nodes nodes'. (slot, nodes) \<in> set tups \<Longrightarrow> (slot', nodes') \<in> set tups \<Longrightarrow>
slot \<noteq> slot' \<Longrightarrow> set nodes \<inter> set nodes' = {}"
    using \<open>\<And>slot nodes. (slot, nodes) \<in> set tups \<Longrightarrow> h \<turnstile> assigned_nodes slot \<rightarrow>\<^sub>r nodes\<close>
      assigned_nodes_different_ptr assms(1) assms(2) assms(3) by blast

  have "h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
    using \<open>(slot, nodes) \<in> set tups\<close> all_tups_slot by blast
  then have "h2 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>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 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot') \<rightarrow>\<^sub>r xc" and
      ha: "h \<turnstile> forall_M remove xc \<rightarrow>\<^sub>h ha" and
      hb: "ha \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot')) nodes' \<rightarrow>\<^sub>h hb" and
      remainder: "hb \<turnstile> forall_M (\<lambda>(slot, assigned_nodes). Heap_Error_Monad.bind
(get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) (\<lambda>x. Heap_Error_Monad.bind (forall_M remove x)
(\<lambda>_. forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) assigned_nodes))) xs \<rightarrow>\<^sub>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 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
      using \<open>h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close> ha
    proof(induct xc arbitrary: h, simp)
      case (Cons a yc)
      obtain hb1 where
        hb1: "h \<turnstile> remove a \<rightarrow>\<^sub>h hb1" and
        hba: "hb1 \<turnstile> forall_M remove yc \<rightarrow>\<^sub>h ha"
        using Cons
        by (auto elim!: bind_returns_heap_E)
      have "hb1 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
        using \<open>h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close> hb1
        by(auto simp add: 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 remove_writes])
      then show ?case
        using hba Cons(1) by simp
    qed
    then
    have "hb \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
      using hb
    proof (induct nodes' arbitrary: ha, simp)
      case (Cons a nodes')
      obtain ha1 where
        ha1: "ha \<turnstile> append_child (cast slot') a \<rightarrow>\<^sub>h ha1" and
        hb: "ha1 \<turnstile> forall_M (append_child (cast slot')) nodes' \<rightarrow>\<^sub>h hb"
        using Cons
        by (auto elim!: bind_returns_heap_E)
      have "ha1 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
        using \<open>ha \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close> ha1
        by(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def
            adopt_node_locs_def 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 \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes \<and> heap_is_wellformed h2 \<and> type_wf h2 \<and> known_ptrs h2"
    using \<open>(slot, nodes) \<in> set tups\<close>
    using h2 assms(1) assms(2) assms(3) \<open>distinct tups\<close> all_tups_slot elementwise_eq
    using \<open>\<And>slot slot' assigned_nodes nodes'. (slot, assigned_nodes) \<in> set tups \<Longrightarrow>
(slot', nodes') \<in> set tups \<Longrightarrow> slot \<noteq> slot' \<Longrightarrow> set assigned_nodes \<inter> set nodes' = {}\<close>
    using \<open>\<And>slot assigned_nodes. (slot, assigned_nodes) \<in> set tups \<Longrightarrow> distinct assigned_nodes\<close>
  proof(induct tups arbitrary: h, simp)
    case (Cons x xs)
    obtain xc ha hb slot' nodes' where
      "x = (slot', nodes')" and
      "h \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot') \<rightarrow>\<^sub>r xc" and
      ha: "h \<turnstile> forall_M remove xc \<rightarrow>\<^sub>h ha" and
      hb: "ha \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot')) nodes' \<rightarrow>\<^sub>h hb" and
      remainder: "hb \<turnstile> forall_M (\<lambda>(slot, assigned_nodes). Heap_Error_Monad.bind
(get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) (\<lambda>x. Heap_Error_Monad.bind (forall_M remove x)
(\<lambda>_. forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) assigned_nodes))) xs \<rightarrow>\<^sub>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 "\<And>slot assigned_nodes. (slot, assigned_nodes) \<in> set xs \<Longrightarrow> h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>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) \<open>h \<turnstile> forall_M remove xc \<rightarrow>\<^sub>h ha\<close>
      apply(induct xc arbitrary: h)
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: 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: 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: 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: remove_def split: option.splits)[1]
      apply (meson local.remove_child_heap_is_wellformed_preserved local.remove_child_preserves_known_ptrs
          local.remove_child_preserves_type_wf)
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: remove_def split: option.splits)[1]
      apply (meson local.remove_child_heap_is_wellformed_preserved local.remove_child_preserves_known_ptrs
          local.remove_child_preserves_type_wf)
      apply(auto elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_parent_pure, rotated]
          simp add: 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 \<open>ha \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot')) nodes' \<rightarrow>\<^sub>h hb\<close>
      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]
      apply (metis insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
          insert_before_preserves_known_ptrs)
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      apply (metis insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
          insert_before_preserves_known_ptrs)
      apply(auto elim!: bind_returns_heap_E simp add: append_child_def)[1]
      apply (metis insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
          insert_before_preserves_known_ptrs)
      done

    {
      fix slot assigned_nodes
      assume "(slot, assigned_nodes) \<in> set xs"
      then have "h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
        using \<open>\<And>slot assigned_nodes. (slot, assigned_nodes) \<in> set xs \<Longrightarrow>
h \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close>
        by auto
      then have "ha \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
        using \<open>h \<turnstile> forall_M remove xc \<rightarrow>\<^sub>h ha\<close>
        apply(induct xc arbitrary: h)
        by(auto simp add: 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 remove_writes]
            elim!: bind_returns_heap_E)
      then have "hb \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
        using \<open>ha \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot')) nodes' \<rightarrow>\<^sub>h hb\<close>
        apply(induct nodes' arbitrary: ha)
        by(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def adopt_node_locs_def
            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) \<open>x = (slot', nodes')\<close>
        by (metis list.set_intros(1))
      then
      have "(slot, nodes) \<notin> set xs"
        using Cons.prems(6) True \<open>x = (slot', nodes')\<close> by auto

      have "ha \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r []"
        using remove_for_all_empty_children Cons.prems(3) Cons.prems(4) Cons.prems(5) True
          \<open>h \<turnstile> forall_M remove xc \<rightarrow>\<^sub>h ha\<close>
        using \<open>h \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot') \<rightarrow>\<^sub>r xc\<close>
        by blast
      then
      have "hb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes"
        using  append_child_for_all_on_no_children[OF \<open>heap_is_wellformed hb\<close> \<open>type_wf hb\<close> \<open>known_ptrs hb\<close>]
          True \<open>nodes' = nodes\<close>
        using \<open>ha \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot')) nodes' \<rightarrow>\<^sub>h hb\<close>
        using \<open>(slot, nodes) \<in> set tups\<close> \<open>\<And>slot assigned_nodes. (slot, assigned_nodes) \<in> set tups \<Longrightarrow>
distinct assigned_nodes\<close> \<open>heap_is_wellformed ha\<close> \<open>known_ptrs ha\<close> \<open>type_wf ha\<close>
          local.append_child_for_all_on_no_children
        by blast
      with \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
      show ?thesis
        using \<open>(slot, nodes) \<notin> set xs\<close> remainder
        using \<open>\<And>slot slot' assigned_nodes nodes'. (slot, assigned_nodes) \<in> set (x#xs) \<Longrightarrow>
(slot', nodes') \<in> set (x#xs) \<Longrightarrow> slot = slot' \<Longrightarrow> assigned_nodes = nodes'\<close>
        using \<open>(slot, nodes) \<in> set (x # xs)\<close>
        using \<open>\<And>slot slot' assigned_nodes nodes'. (slot, assigned_nodes) \<in> set (x#xs) \<Longrightarrow>
(slot', nodes') \<in> set (x#xs) \<Longrightarrow> slot \<noteq> slot' \<Longrightarrow> set assigned_nodes \<inter> set nodes' = {}\<close>
      proof(induct xs arbitrary: hb, simp)
        case (Cons y ys)
        obtain yc hba hbb slot'' nodes'' where
          "y = (slot'', nodes'')" and
          "hb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'') \<rightarrow>\<^sub>r yc" and
          "hb \<turnstile> forall_M remove yc \<rightarrow>\<^sub>h hba" and
          "hba \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'')) nodes'' \<rightarrow>\<^sub>h hbb" and
          remainder: "hbb \<turnstile> forall_M (\<lambda>(slot, assigned_nodes). Heap_Error_Monad.bind
(get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) (\<lambda>x. Heap_Error_Monad.bind (forall_M remove x)
(\<lambda>_. forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot)) assigned_nodes))) ys \<rightarrow>\<^sub>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 \<noteq> slot''"
          by (metis Cons.prems(5) Cons.prems(7) Cons.prems(8) \<open>y = (slot'', nodes'')\<close>
              list.set_intros(1) list.set_intros(2))
        then have "set nodes \<inter> set nodes'' = {}"
          by (metis Cons.prems(8) Cons.prems(9) \<open>y = (slot'', nodes'')\<close> list.set_intros(1)
              list.set_intros(2))

        have "hba \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hba \<and> type_wf hba \<and> known_ptrs hba"
          using \<open>hb \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes\<close>
          using \<open>hb \<turnstile> forall_M remove yc \<rightarrow>\<^sub>h hba\<close>
          using \<open>hb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'') \<rightarrow>\<^sub>r yc\<close>
          using \<open>heap_is_wellformed hb\<close> \<open>type_wf hb\<close> \<open>known_ptrs hb\<close>
        proof(induct yc arbitrary: hb, simp)
          case (Cons a yc)
          obtain hb1 where
            hb1: "hb \<turnstile> remove a \<rightarrow>\<^sub>h hb1" and
            hba: "hb1 \<turnstile> forall_M remove yc \<rightarrow>\<^sub>h hba"
            using Cons
            by (auto elim!: bind_returns_heap_E)
          have "hb \<turnstile> get_parent a \<rightarrow>\<^sub>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 \<open>hb \<turnstile> remove a \<rightarrow>\<^sub>h hb1\<close>
            apply(auto simp add: remove_def elim!: bind_returns_heap_E
                bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            using \<open>hb \<turnstile> remove a \<rightarrow>\<^sub>h hb1\<close>
            apply(auto simp add: remove_def elim!: bind_returns_heap_E
                bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            using \<open>hb \<turnstile> remove a \<rightarrow>\<^sub>h hb1\<close>
            apply(auto simp add: remove_def elim!: bind_returns_heap_E
                bind_returns_heap_E2[rotated, OF get_parent_pure, rotated] split: option.splits)[1]
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            using \<open>heap_is_wellformed hb\<close> and \<open>type_wf hb\<close> and \<open>known_ptrs hb\<close>
              remove_child_heap_is_wellformed_preserved remove_child_preserves_type_wf
              remove_child_preserves_known_ptrs
            apply blast
            done
          moreover have "hb1 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'') \<rightarrow>\<^sub>r yc"
            using \<open>hb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'') \<rightarrow>\<^sub>r a # yc\<close> hb1
            using remove_removes_child \<open>heap_is_wellformed hb\<close> \<open>type_wf hb\<close> \<open>known_ptrs hb\<close>
            by simp
          moreover have "hb1 \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes"
            using Cons(2) hb1 set_child_nodes_get_child_nodes_different_pointers
              \<open>hb \<turnstile> get_parent a \<rightarrow>\<^sub>r Some (cast slot'')\<close> \<open>slot \<noteq> slot''\<close>
            apply(auto simp add: remove_child_locs_def elim!: bind_returns_heap_E
                dest!: reads_writes_separate_forwards[OF get_child_nodes_reads remove_writes])[1]
            by (metis cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject)
          ultimately show ?thesis
            using \<open>hb1 \<turnstile> forall_M remove (yc) \<rightarrow>\<^sub>h hba\<close> Cons
            by auto
        qed


        then have "hbb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hbb \<and> type_wf hbb \<and> known_ptrs hbb"
          using \<open>hba \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'')) nodes'' \<rightarrow>\<^sub>h hbb\<close>
          using \<open>set nodes \<inter> set nodes'' = {}\<close>
        proof(induct nodes'' arbitrary: hba, simp)
          case (Cons a nodes'')
          then have "hba \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes" and
            "heap_is_wellformed hba" and
            "type_wf hba" and
            "known_ptrs hba"
            by auto
          obtain hba1 where
            hba1: "hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1" and
            "hba1 \<turnstile> forall_M (append_child (cast slot'')) nodes'' \<rightarrow>\<^sub>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 \<open>hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1\<close>
            apply(auto simp add: append_child_def)[1]
            using \<open>heap_is_wellformed hba\<close> and \<open>type_wf hba\<close> and \<open>known_ptrs hba\<close>
              insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
              insert_before_preserves_known_ptrs
            apply blast
            using \<open>hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1\<close>
            apply(auto simp add: append_child_def)[1]
            using \<open>heap_is_wellformed hba\<close> and \<open>type_wf hba\<close> and \<open>known_ptrs hba\<close>
              insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
              insert_before_preserves_known_ptrs
            apply blast
            using \<open>hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1\<close>
            apply(auto simp add: append_child_def)[1]
            using \<open>heap_is_wellformed hba\<close> and \<open>type_wf hba\<close> and \<open>known_ptrs hba\<close>
              insert_before_heap_is_wellformed_preserved insert_before_preserves_type_wf
              insert_before_preserves_known_ptrs
            apply blast
            done

          moreover
          have "a \<notin> set nodes"
            using \<open>set nodes \<inter> set (a # nodes'') = {}\<close>
            by auto


          moreover
          obtain parent_opt where "hba \<turnstile> get_parent a \<rightarrow>\<^sub>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 \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes"
          proof (induct parent_opt)
            case None
            then show ?case
              using \<open>hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1\<close>
              using \<open>hba \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes\<close>
              using \<open>slot \<noteq> slot''\<close>
              apply(auto simp add: append_child_def insert_before_locs_def adopt_node_locs_def
                  adopt_node_locs_def remove_child_locs_def
                  elim!: reads_writes_separate_forwards[OF get_child_nodes_reads insert_before_writes])[1]
              by (metis cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject
                  set_child_nodes_get_child_nodes_different_pointers)
          next
            case (Some parent)
            have "parent \<noteq> cast slot"
              apply(rule ccontr, simp)
              using Cons(2)
              apply -
              apply(rule get_parent_child_dual[OF \<open>hba \<turnstile> get_parent a \<rightarrow>\<^sub>r Some parent\<close>])
              apply(auto)[1]
              using \<open>a \<notin> set nodes\<close> 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 \<open>hba \<turnstile> append_child (cast slot'') a \<rightarrow>\<^sub>h hba1\<close>[unfolded append_child_def])
              apply(fact \<open>hba \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes\<close>)
              using \<open>hba \<turnstile> get_parent a \<rightarrow>\<^sub>r Some parent\<close> \<open>parent \<noteq> cast slot\<close> \<open>slot \<noteq> slot''\<close>
              apply(auto simp add: insert_before_locs_def adopt_node_locs_def adopt_node_locs_def
                  remove_child_locs_def)[1]
              apply (simp_all add: set_child_nodes_get_child_nodes_different_pointers
                  set_disconnected_nodes_get_child_nodes)
              by (metis cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject
                  set_child_nodes_get_child_nodes_different_pointers)
          qed
          moreover
          have "set nodes \<inter> set nodes'' = {}"
            using Cons.prems(3) by auto
          ultimately show ?case
            using Cons.hyps  \<open>hba1 \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot'')) nodes'' \<rightarrow>\<^sub>h hbb\<close>
            by blast
        qed
        show ?case
          apply(rule Cons(1))
          using \<open>hbb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hbb \<and> type_wf hbb \<and> known_ptrs hbb\<close>
          apply(auto)[1]
          using \<open>hbb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hbb \<and> type_wf hbb \<and> known_ptrs hbb\<close>
          apply(auto)[1]
          using \<open>hbb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hbb \<and> type_wf hbb \<and> known_ptrs hbb\<close>
          apply(auto)[1]
          using \<open>hbb \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes \<and>
heap_is_wellformed hbb \<and> type_wf hbb \<and> known_ptrs hbb\<close>
          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 \<open>nodes' = nodes\<close> \<open>x = (slot', nodes')\<close>)
          by (metis Cons.prems(9) insert_iff list.simps(15))
      qed
    next
      case False
      then have "nodes' \<noteq> nodes"
        using Cons.prems(1) Cons.prems(9) \<open>x = (slot', nodes')\<close>
        by (metis assms(6) inf.idem list.set_intros(1) set_empty2)
      then
      have "(slot, nodes) \<in> set xs"
        using Cons.prems(1) \<open>x = (slot', nodes')\<close>
        by auto
      then show ?thesis
        using Cons(1)[simplified, OF \<open>(slot, nodes) \<in> set xs\<close> remainder
            \<open>heap_is_wellformed hb\<close> \<open>type_wf hb\<close> \<open>known_ptrs hb\<close>]
        using Cons.prems(6) tag_names_same  Cons.prems(8) Cons.prems(9)
        by (smt Cons.prems(10) distinct.simps(2) list.set_intros(2))
    qed
  qed
  then
  show ?thesis
    using h' \<open>h2 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close>
  proof(induct shadow_root_ptrs arbitrary: h2, simp)
    case (Cons shadow_root_ptr shadow_root_ptrs)
    then have "h2 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>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 \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r host" and
      "h2 \<turnstile> get_child_nodes (cast host) \<rightarrow>\<^sub>r host_children" and
      h2a: "h2 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>h h2a" and
      "h2a \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r shadow_root_children" and
      h2b: "h2a \<turnstile> forall_M (append_child (cast host)) shadow_root_children \<rightarrow>\<^sub>h h2b" and
      "h2b \<turnstile> remove_shadow_root host \<rightarrow>\<^sub>h h2c" and
      remainder: "h2c \<turnstile> forall_M(\<lambda>shadow_root_ptr. Heap_Error_Monad.bind (get_host shadow_root_ptr)
        (\<lambda>host. Heap_Error_Monad.bind (get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host))
             (\<lambda>x. Heap_Error_Monad.bind (forall_M remove x)
               (\<lambda>_. Heap_Error_Monad.bind (get_child_nodes (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr))
                    (\<lambda>x. Heap_Error_Monad.bind (forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host)) x)
                           (\<lambda>_. remove_shadow_root host))))))
           shadow_root_ptrs
       \<rightarrow>\<^sub>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 \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
      using \<open>h2 \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r host\<close> shadow_root_host_dual
      using \<open>heap_is_wellformed h2\<close> \<open>type_wf h2\<close> by blast
    then have "h2a \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
      using \<open>h2 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>h h2a\<close>
      apply(induct host_children arbitrary: h2)
      by(auto simp add: set_disconnected_nodes_get_shadow_root set_child_nodes_get_shadow_root
          remove_child_locs_def elim!: bind_returns_heap_E
          dest!: reads_writes_separate_forwards[OF get_shadow_root_reads remove_writes])
    then have "h2b \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
      using \<open>h2a \<turnstile> forall_M (append_child (cast host)) shadow_root_children \<rightarrow>\<^sub>h h2b\<close>
      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 adopt_node_locs_def 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 \<noteq> slot"
    proof (rule ccontr, simp)
      assume "host = slot"
      show False
        using get_host_valid_tag_name[OF \<open>heap_is_wellformed h2\<close> \<open>type_wf h2\<close>
            \<open>h2 \<turnstile> get_host shadow_root_ptr \<rightarrow>\<^sub>r host\<close>[unfolded \<open>host = slot\<close>] \<open>h2 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close>]
        by(simp)
    qed

    have "heap_is_wellformed h2a" and "type_wf h2a" and "known_ptrs h2a"
      using \<open>heap_is_wellformed h2\<close> and \<open>type_wf h2\<close> and \<open>known_ptrs h2\<close>
        \<open>h2 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>h h2a\<close>
      apply(induct host_children arbitrary: h2)
      apply(auto simp add: 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: 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: 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: 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: 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: 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 \<open>h2a \<turnstile> forall_M (append_child (cast host)) shadow_root_children \<rightarrow>\<^sub>h h2b\<close>
      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 \<open>h2b \<turnstile> remove_shadow_root host \<rightarrow>\<^sub>h h2c\<close>
      by blast+

    moreover
    have "h2a \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes"
      using \<open>h2 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes\<close>
      using \<open>h2 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>h h2a\<close>
      using \<open>h2 \<turnstile> get_child_nodes (cast host) \<rightarrow>\<^sub>r host_children\<close>
      using \<open>heap_is_wellformed h2\<close> \<open>type_wf h2\<close> \<open>known_ptrs h2\<close>
    proof (induct host_children arbitrary: h2, simp)
      case (Cons a host_children)
      obtain h21 where "h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21" and
        "h21 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>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 \<open>heap_is_wellformed h2\<close> and \<open>type_wf h2\<close> and \<open>known_ptrs h2\<close> \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close>
        apply(auto simp add: 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)
        using \<open>heap_is_wellformed h2\<close> and \<open>type_wf h2\<close> and \<open>known_ptrs h2\<close> \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close>
        apply(auto simp add: 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)
        using \<open>heap_is_wellformed h2\<close> and \<open>type_wf h2\<close> and \<open>known_ptrs h2\<close> \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close>
        apply(auto simp add: 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
      have "h2 \<turnstile> get_parent a \<rightarrow>\<^sub>r Some (cast host)"
        using \<open>h2 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) \<rightarrow>\<^sub>r a # host_children\<close>
        using \<open>heap_is_wellformed h2\<close> \<open>type_wf h2\<close> \<open>known_ptrs h2\<close> child_parent_dual
        using heap_is_wellformed_def by auto
      then have "h21 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes"
        using \<open>h2 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes\<close> \<open>host \<noteq> slot\<close>
        using \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close>
        apply(auto simp add: remove_child_locs_def set_disconnected_nodes_get_child_nodes
            dest!: reads_writes_preserved[OF get_child_nodes_reads remove_writes])[1]
        by (meson cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject
            set_child_nodes_get_child_nodes_different_pointers)
      moreover have "h21 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) \<rightarrow>\<^sub>r host_children"
        using \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close>  remove_removes_child[OF \<open>heap_is_wellformed h2\<close> \<open>type_wf h2\<close>
            \<open>known_ptrs h2\<close> \<open>h2 \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) \<rightarrow>\<^sub>r a # host_children\<close>]
        by blast
      ultimately show ?case
        using \<open>heap_is_wellformed h21\<close> and \<open>type_wf h21\<close> and \<open>known_ptrs h21\<close>
          \<open>h21 \<turnstile> forall_M remove host_children \<rightarrow>\<^sub>h h2a\<close> Cons(1)
        using Cons.prems(3) Cons.prems(4) Cons.prems(5) Cons.prems(6) heap_is_wellformed_def
          \<open>h2 \<turnstile> remove a \<rightarrow>\<^sub>h h21\<close> remove_removes_child
        by blast
    qed

    then
    have "h2b \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes"
      using \<open>h2a \<turnstile> forall_M (append_child (cast host)) shadow_root_children \<rightarrow>\<^sub>h h2b\<close>
      using \<open>h2a \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r shadow_root_children\<close>
      using \<open>heap_is_wellformed h2a\<close> \<open>type_wf h2a\<close> \<open>known_ptrs h2a\<close>
    proof(induct shadow_root_children arbitrary: h2a, simp)
      case (Cons a shadow_root_children)
      obtain h2a1 where "h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1" and
        "h2a1 \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host)) (shadow_root_children) \<rightarrow>\<^sub>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 \<open>heap_is_wellformed h2a\<close> and \<open>type_wf h2a\<close> and \<open>known_ptrs h2a\<close>
          \<open>h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1\<close>
        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
        using \<open>heap_is_wellformed h2a\<close> and \<open>type_wf h2a\<close> and \<open>known_ptrs h2a\<close>
          \<open>h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1\<close>
        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
        using \<open>heap_is_wellformed h2a\<close> and \<open>type_wf h2a\<close> and \<open>known_ptrs h2a\<close>
          \<open>h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1\<close>
        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
      moreover have "h2a1 \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r shadow_root_children"
        using \<open>h2a \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r a # shadow_root_children\<close>
        using insert_before_removes_child
          \<open>h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1\<close>[unfolded append_child_def]
        using \<open>heap_is_wellformed h2a\<close> \<open>type_wf h2a\<close> \<open>known_ptrs h2a\<close>
        using cast_document_ptr_not_node_ptr(2)
        using cast_shadow_root_ptr_not_node_ptr(2) by blast
      moreover have "h2a \<turnstile> get_parent a \<rightarrow>\<^sub>r Some (cast shadow_root_ptr)"
        using \<open>h2a \<turnstile> get_child_nodes (cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr) \<rightarrow>\<^sub>r a # shadow_root_children\<close>
        using \<open>heap_is_wellformed h2a\<close> \<open>type_wf h2a\<close> \<open>known_ptrs h2a\<close> child_parent_dual
        using heap_is_wellformed_def by auto
      then have "h2a1 \<turnstile> get_child_nodes (cast slot) \<rightarrow>\<^sub>r nodes"
        using \<open>h2a \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes\<close>
        using \<open>h2a \<turnstile> append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host) a \<rightarrow>\<^sub>h h2a1\<close> \<open>host \<noteq> slot\<close>
        apply(auto simp add:  set_disconnected_nodes_get_child_nodes append_child_def
            insert_before_locs_def adopt_node_locs_def adopt_node_locs_def remove_child_locs_def
            elim!: bind_returns_heap_E dest!: reads_writes_preserved[OF get_child_nodes_reads
              insert_before_writes])[1]
        using set_child_nodes_get_child_nodes_different_pointers cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject
          cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject cast_document_ptr_not_node_ptr(2)
        by (metis cast_shadow_root_ptr_not_node_ptr(2))+
      ultimately
      show ?case
        using Cons(1) \<open>h2a1 \<turnstile> forall_M (append_child (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host)) shadow_root_children \<rightarrow>\<^sub>h h2b\<close>
        by blast
    qed
    then
    have "h2c \<turnstile> get_child_nodes (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r slot) \<rightarrow>\<^sub>r nodes"
      using \<open>h2b \<turnstile> remove_shadow_root host \<rightarrow>\<^sub>h h2c\<close>
      apply(auto simp add: remove_shadow_root_get_child_nodes_different_pointers
          dest!: reads_writes_separate_forwards[OF get_child_nodes_reads remove_shadow_root_writes])[1]
      by (meson cast_shadow_root_ptr_not_node_ptr(2)
          local.remove_shadow_root_get_child_nodes_different_pointers)

    moreover
    have "h2a \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
      using h2a \<open>h2 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''\<close>
      apply(induct host_children arbitrary: h2)
      by(auto simp add: 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 remove_writes]
          elim!: bind_returns_heap_E)
    then
    have "h2b \<turnstile> get_tag_name slot \<rightarrow>\<^sub>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 adopt_node_locs_def
          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 \<turnstile> get_tag_name slot \<rightarrow>\<^sub>r ''slot''"
      using \<open>h2b \<turnstile> remove_shadow_root host \<rightarrow>\<^sub>h h2c\<close>
      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_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  type_wf get_tag_name get_tag_name_locs known_ptr get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs
  heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs
  get_disconnected_document get_disconnected_document_locs get_parent get_parent_locs
  get_mode get_mode_locs get_attribute get_attribute_locs first_in_tree_order find_slot
  assigned_slot known_ptrs to_tree_order assigned_nodes assigned_nodes_flatten flatten_dom
  get_root_node get_root_node_locs remove insert_before insert_before_locs append_child
  remove_shadow_root remove_shadow_root_locs set_shadow_root set_shadow_root_locs remove_child
  remove_child_locs get_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
  adopt_node adopt_node_locs set_child_nodes set_child_nodes_locs
  by(auto simp add: l_assigned_nodes_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_assigned_nodes_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]


subsubsection \<open>get\_owner\_document\<close>

locale l_get_owner_document_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
  l_get_owner_document_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
  l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma get_owner_document_is_component_unsafe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h \<turnstile> get_owner_document ptr \<rightarrow>\<^sub>r owner_document"
  assumes "\<not>is_document_ptr_kind |h \<turnstile> get_root_node ptr|\<^sub>r"
  shows "set |h \<turnstile> get_component ptr|\<^sub>r \<inter> set |h \<turnstile> get_component (cast owner_document)|\<^sub>r = {}"
proof -
  have "owner_document |\<in>| document_ptr_kinds h"
    using assms(1) assms(2) assms(3) assms(4) get_owner_document_owner_document_in_heap by blast
  have "ptr |\<in>| 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 \<turnstile> get_root_node ptr \<rightarrow>\<^sub>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 \<turnstile> to_tree_order root \<rightarrow>\<^sub>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 "\<forall>p \<in> set to. \<not>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 \<notin> set |h \<turnstile> get_component ptr|\<^sub>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_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.get_component_ok local.get_component_root_node_same
        local.get_root_node_not_node_same local.get_root_node_ptr_in_heap local.l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms
        node_ptr_no_document_ptr_cast returns_result_select_result root select_result_I2)
  then have "|h \<turnstile> get_component ptr|\<^sub>r \<noteq> |h \<turnstile> get_component (cast owner_document)|\<^sub>r"
    by (metis (no_types, lifting) \<open>owner_document |\<in>| document_ptr_kinds h\<close> assms(1) assms(2) assms(3)
        document_ptr_kinds_commutes l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.get_component_ok local.get_dom_component_ptr
        local.l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms returns_result_select_result)
  then show ?thesis
    by (meson \<open>owner_document |\<in>| document_ptr_kinds h\<close> \<open>ptr |\<in>| object_ptr_kinds h\<close> assms(1)
        assms(2) assms(3) document_ptr_kinds_commutes l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.get_dom_component_no_overlap
        l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.get_component_ok local.l_get_component\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms returns_result_select_result)
qed

end
interpretation i_get_owner_document_component?: l_get_owner_document_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
  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 get_root_node_si
  get_root_node_si_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_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_document get_disconnected_document_locs
  known_ptrs get_ancestors_si get_ancestors_si_locs to_tree_order get_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_owner_document_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_owner_document_component\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]

definition is_shadow_root_component :: "(_) object_ptr list \<Rightarrow> bool"
  where
    "is_shadow_root_component c = is_shadow_root_ptr_kind (hd c)"

end