Theory Core_DOM_DOM_Components

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

section ‹Core SC DOM Components›
theory Core_DOM_DOM_Components
  imports Core_SC_DOM.Core_DOM
begin

subsection ‹Components›

locale l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs =
  l_get_root_node_defs get_root_node get_root_node_locs +
  l_to_tree_order_defs to_tree_order
  for get_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and to_tree_order :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
begin

definition a_get_dom_component :: "(_) object_ptr ⇒ (_, (_) object_ptr list) dom_prog"
  where
    "a_get_dom_component ptr = do {
      root ← get_root_node ptr;
      to_tree_order root
    }"

definition a_is_strongly_dom_component_safe ::
  "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
  where
    "a_is_strongly_dom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h' = (
      let removed_pointers = fset (object_ptr_kinds h) - fset (object_ptr_kinds h') in
      let added_pointers = fset (object_ptr_kinds h') - fset (object_ptr_kinds h) in
      let arg_components =
        (⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_dom_component ptr|⇩r) ∩
        fset (object_ptr_kinds h).  set |h ⊢ a_get_dom_component ptr|⇩r) in
      let arg_components' =
        (⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_dom_component ptr|⇩r) ∩
        fset (object_ptr_kinds h').  set |h' ⊢ a_get_dom_component ptr|⇩r) in
      removed_pointers ⊆ arg_components ∧
      added_pointers ⊆ arg_components' ∧
      S⇩r⇩e⇩s⇩u⇩l⇩t ⊆ arg_components' ∧
      (∀outside_ptr ∈ fset (object_ptr_kinds h) ∩ fset (object_ptr_kinds h') -
        (⋃ptr ∈ S⇩a⇩r⇩g. set |h  ⊢ a_get_dom_component ptr|⇩r). preserved (get_M outside_ptr id) h h'))"

definition a_is_weakly_dom_component_safe ::
  "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
  where
    "a_is_weakly_dom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h' = (
      let removed_pointers = fset (object_ptr_kinds h) - fset (object_ptr_kinds h') in
      let added_pointers = fset (object_ptr_kinds h') - fset (object_ptr_kinds h) in
      let arg_components =
        (⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_dom_component ptr|⇩r) ∩
        fset (object_ptr_kinds h).  set |h ⊢ a_get_dom_component ptr|⇩r) in
      let arg_components' =
        (⋃ptr ∈ (⋃ptr ∈ S⇩a⇩r⇩g. set |h ⊢ a_get_dom_component ptr|⇩r) ∩
        fset (object_ptr_kinds h').  set |h' ⊢ a_get_dom_component ptr|⇩r) in
      removed_pointers ⊆ arg_components ∧
      S⇩r⇩e⇩s⇩u⇩l⇩t ⊆ arg_components' ∪ added_pointers  ∧
      (∀outside_ptr ∈ fset (object_ptr_kinds h) ∩ fset (object_ptr_kinds h') -
        (⋃ptr ∈ S⇩a⇩r⇩g. set |h  ⊢ a_get_dom_component ptr|⇩r). preserved (get_M outside_ptr id) h h'))"

lemma "a_is_strongly_dom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h' ⟹ a_is_weakly_dom_component_safe S⇩a⇩r⇩g S⇩r⇩e⇩s⇩u⇩l⇩t h h'"
  by(auto simp add: a_is_strongly_dom_component_safe_def a_is_weakly_dom_component_safe_def Let_def)

definition is_document_component :: "(_) object_ptr list ⇒ bool"
  where
    "is_document_component c = is_document_ptr_kind (hd c)"

definition is_disconnected_component :: "(_) object_ptr list ⇒ bool"
  where
    "is_disconnected_component c = is_node_ptr_kind (hd c)"
end

global_interpretation l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs get_root_node get_root_node_locs to_tree_order
  defines get_dom_component = a_get_dom_component
    and is_strongly_dom_component_safe = a_is_strongly_dom_component_safe
    and is_weakly_dom_component_safe = a_is_weakly_dom_component_safe
  .


locale l_get_dom_component_defs =
  fixes get_dom_component :: "(_) object_ptr ⇒ (_, (_) object_ptr list) dom_prog"
  fixes is_strongly_dom_component_safe ::
    "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
  fixes is_weakly_dom_component_safe ::
    "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"

locale l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_to_tree_order_wf +
  l_get_dom_component_defs +
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_defs +
  l_get_ancestors +
  l_get_ancestors_wf +
  l_get_root_node +
  l_get_root_node_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_parent +
  l_get_parent_wf +
  l_get_element_by +
  l_to_tree_order_wf_get_root_node_wf +
  (* l_to_tree_order_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M _ _ _ get_child_nodes +
  l_get_root_node_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M _ _ get_child_nodes+
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M _ _ "l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.a_to_tree_order get_child_nodes"
  for get_child_nodes :: "(_::linorder) object_ptr ⇒ (_, (_) node_ptr list) dom_prog" *)
  assumes get_dom_component_impl: "get_dom_component = a_get_dom_component"
  assumes is_strongly_dom_component_safe_impl:
    "is_strongly_dom_component_safe = a_is_strongly_dom_component_safe"
  assumes is_weakly_dom_component_safe_impl:
    "is_weakly_dom_component_safe = a_is_weakly_dom_component_safe"
begin
lemmas get_dom_component_def = a_get_dom_component_def[folded get_dom_component_impl]
lemmas is_strongly_dom_component_safe_def =
  a_is_strongly_dom_component_safe_def[folded is_strongly_dom_component_safe_impl]
lemmas is_weakly_dom_component_safe_def =
  a_is_weakly_dom_component_safe_def[folded is_weakly_dom_component_safe_impl]

lemma get_dom_component_ptr_in_heap:
  assumes "h ⊢ ok (get_dom_component ptr)"
  shows "ptr |∈| object_ptr_kinds h"
  using assms get_root_node_ptr_in_heap
  by(auto simp add: get_dom_component_def)

lemma get_dom_component_ok:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "ptr |∈| object_ptr_kinds h"
  shows "h ⊢ ok (get_dom_component ptr)"
  using assms
  apply(auto simp add: get_dom_component_def a_get_root_node_def intro!: bind_is_OK_pure_I)[1]
  using get_root_node_ok  to_tree_order_ok get_root_node_ptr_in_heap
   apply blast
  by (simp add: local.get_root_node_root_in_heap local.to_tree_order_ok)

lemma get_dom_component_ptr:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  shows "ptr ∈ set c"
proof(insert assms(1) assms(4), induct ptr rule: heap_wellformed_induct_rev )
  case (step child)
  then show ?case
  proof (cases "is_node_ptr_kind child")
    case True
    obtain node_ptr where
      node_ptr: "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr = child"
      using ‹is_node_ptr_kind child› node_ptr_casts_commute3 by blast
    have "child |∈| object_ptr_kinds h"
      using ‹h ⊢ get_dom_component child →⇩r c› get_dom_component_ptr_in_heap by fast
    with node_ptr have "node_ptr |∈| node_ptr_kinds h"
      by auto
    then obtain parent_opt where
      parent: "h ⊢ get_parent node_ptr →⇩r parent_opt"
      using get_parent_ok ‹type_wf h› ‹known_ptrs h›
      by fast
    then show ?thesis
    proof (induct parent_opt)
      case None
      then have "h ⊢ get_root_node (cast node_ptr) →⇩r cast node_ptr"
        by (simp add: local.get_root_node_no_parent)
      then show ?case
        using ‹type_wf h› ‹known_ptrs h› node_ptr step(2)
        apply(auto simp add: get_dom_component_def a_get_root_node_def elim!: bind_returns_result_E2)[1]
        using to_tree_order_ptr_in_result returns_result_eq by fastforce
    next
      case (Some parent_ptr)
      then have "h ⊢ get_dom_component parent_ptr →⇩r c"
        using step(2) node_ptr ‹type_wf h› ‹known_ptrs h› ‹heap_is_wellformed h›
          get_root_node_parent_same
        by(auto simp add: get_dom_component_def elim!: bind_returns_result_E2
            intro!: bind_pure_returns_result_I)
      then have "parent_ptr ∈ set c"
        using step node_ptr Some by blast
      then show ?case
        using  ‹type_wf h› ‹known_ptrs h› ‹heap_is_wellformed h› step(2) node_ptr Some
        apply(auto simp add: get_dom_component_def elim!: bind_returns_result_E2)[1]
        using to_tree_order_parent by blast
    qed
  next
    case False
    then show ?thesis
      using ‹type_wf h› ‹known_ptrs h› step(2)
      apply(auto simp add: get_dom_component_def elim!: bind_returns_result_E2)[1]
      by (metis is_OK_returns_result_I local.get_root_node_not_node_same
          local.get_root_node_ptr_in_heap local.to_tree_order_ptr_in_result returns_result_eq)
  qed
qed

lemma get_dom_component_parent_inside:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "cast node_ptr ∈ set c"
  assumes "h ⊢ get_parent node_ptr →⇩r Some parent"
  shows "parent ∈ set c"
proof -
  have "parent |∈| object_ptr_kinds h"
    using assms(6) get_parent_parent_in_heap by blast

  obtain root_ptr where root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr" and c: "h ⊢ to_tree_order root_ptr →⇩r c"
    using assms(4)
    by (metis (no_types, opaque_lifting) bind_returns_result_E2 get_dom_component_def get_root_node_pure)
  then have "h ⊢ get_root_node (cast node_ptr) →⇩r root_ptr"
    using assms(1) assms(2) assms(3) assms(5) to_tree_order_same_root by blast
  then have "h ⊢ get_root_node parent →⇩r root_ptr"
    using assms(6)  get_root_node_parent_same by blast
  then have "h ⊢ get_dom_component parent →⇩r c"
    using c get_dom_component_def by auto
  then show ?thesis
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
qed

lemma get_dom_component_subset:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "ptr' ∈ set c"
  shows "h ⊢ get_dom_component ptr' →⇩r c"
proof(insert assms(1) assms(5), induct ptr' rule: heap_wellformed_induct_rev )
  case (step child)
  then show ?case
  proof (cases "is_node_ptr_kind child")
    case True
    obtain node_ptr where
      node_ptr: "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr = child"
      using ‹is_node_ptr_kind child› node_ptr_casts_commute3 by blast
    have "child |∈| object_ptr_kinds h"
      using to_tree_order_ptrs_in_heap assms(1) assms(2) assms(3) assms(4) step(2)
      unfolding get_dom_component_def
      by (meson bind_returns_result_E2 get_root_node_pure)
    with node_ptr have "node_ptr |∈| node_ptr_kinds h"
      by auto
    then obtain parent_opt where
      parent: "h ⊢ get_parent node_ptr →⇩r parent_opt"
      using get_parent_ok ‹type_wf h› ‹known_ptrs h›
      by fast
    then show ?thesis
    proof (induct parent_opt)
      case None
      then have "h ⊢ get_root_node child →⇩r child"
        using assms(1) get_root_node_no_parent node_ptr by blast
      then show ?case
        using ‹type_wf h› ‹known_ptrs h› node_ptr step(2) assms(4) assms(1)
        by (metis (no_types) bind_pure_returns_result_I2 bind_returns_result_E2
            get_dom_component_def get_root_node_pure is_OK_returns_result_I returns_result_eq
            to_tree_order_same_root)
    next
      case (Some parent_ptr)
      then have "h ⊢ get_dom_component parent_ptr →⇩r c"
        using step get_dom_component_parent_inside assms node_ptr by blast
      then show ?case
        using Some node_ptr
        apply(auto simp add: get_dom_component_def elim!: bind_returns_result_E2
            del: bind_pure_returns_result_I intro!: bind_pure_returns_result_I)[1]
        using get_root_node_parent_same by blast
    qed
  next
    case False
    then have "child |∈| object_ptr_kinds h"
      using assms(1) assms(4) step(2)
      by (metis (no_types, lifting) assms(2) assms(3) bind_returns_result_E2 get_root_node_pure
          get_dom_component_def to_tree_order_ptrs_in_heap)
    then have "h ⊢ get_root_node child →⇩r child"
      using assms(1) False get_root_node_not_node_same by blast
    then show ?thesis
      using assms(1) assms(2) assms(3) assms(4) step.prems
      by (metis (no_types) False ‹child |∈| object_ptr_kinds h› bind_pure_returns_result_I2
          bind_returns_result_E2 get_dom_component_def get_root_node_ok get_root_node_pure returns_result_eq
          to_tree_order_node_ptrs)
  qed
qed

lemma get_dom_component_to_tree_order_subset:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ to_tree_order ptr →⇩r nodes"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  shows "set nodes ⊆ set c"
  using assms
  apply(auto simp add: get_dom_component_def elim!: bind_returns_result_E2)[1]
  by (meson to_tree_order_subset  assms(5) contra_subsetD get_dom_component_ptr)

lemma get_dom_component_to_tree_order:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ to_tree_order ptr' →⇩r to"
  assumes "ptr ∈ set to"
  shows "h ⊢ get_dom_component ptr' →⇩r c"
  by (metis (no_types, opaque_lifting) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6)
      get_dom_component_ok get_dom_component_subset get_dom_component_to_tree_order_subset
      is_OK_returns_result_E local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap
      select_result_I2 subsetCE)

lemma get_dom_component_root_node_same:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_root_node ptr →⇩r root_ptr"
  assumes "x ∈ set c"
  shows "h ⊢ get_root_node x →⇩r root_ptr"
proof(insert assms(1) assms(6), induct x rule: heap_wellformed_induct_rev )
  case (step child)
  then show ?case
  proof (cases "is_node_ptr_kind child")
    case True
    obtain node_ptr where
      node_ptr: "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r node_ptr = child"
      using ‹is_node_ptr_kind child› node_ptr_casts_commute3 by blast
    have "child |∈| object_ptr_kinds h"
      using to_tree_order_ptrs_in_heap assms(1) assms(2) assms(3) assms(4) step(2)
      unfolding get_dom_component_def
      by (meson bind_returns_result_E2 get_root_node_pure)
    with node_ptr have "node_ptr |∈| node_ptr_kinds h"
      by auto
    then obtain parent_opt where
      parent: "h ⊢ get_parent node_ptr →⇩r parent_opt"
      using get_parent_ok ‹type_wf h› ‹known_ptrs h›
      by fast
    then show ?thesis
    proof (induct parent_opt)
      case None
      then have "h ⊢ get_root_node child →⇩r child"
        using assms(1) get_root_node_no_parent  node_ptr by blast
      then show ?case
        using ‹type_wf h› ‹known_ptrs h› node_ptr step(2) assms(4) assms(1) assms(5)
        by (metis (no_types) ‹child |∈| object_ptr_kinds h› bind_pure_returns_result_I
            get_dom_component_def get_dom_component_ptr get_dom_component_subset get_root_node_pure
            is_OK_returns_result_E returns_result_eq to_tree_order_ok to_tree_order_same_root)
    next
      case (Some parent_ptr)
      then have "h ⊢ get_dom_component parent_ptr →⇩r c"
        using step get_dom_component_parent_inside assms node_ptr
        by (meson get_dom_component_subset)
      then show ?case
        using Some node_ptr
        apply(auto simp add: get_dom_component_def elim!: bind_returns_result_E2)[1]
        using get_root_node_parent_same
        using ‹h ⊢ get_dom_component parent_ptr →⇩r c› assms(1) assms(2) assms(3)
          get_dom_component_ptr step.hyps by blast
    qed
  next
    case False
    then have "child |∈| object_ptr_kinds h"
      using assms(1) assms(4) step(2)
      by (metis (no_types, lifting) assms(2) assms(3) bind_returns_result_E2 get_root_node_pure
          get_dom_component_def to_tree_order_ptrs_in_heap)
    then have "h ⊢ get_root_node child →⇩r child"
      using assms(1) False get_root_node_not_node_same by auto
    then show ?thesis
      using assms(1) assms(2) assms(3) assms(4) step.prems assms(5)
      by (metis (no_types, opaque_lifting) bind_returns_result_E2 get_dom_component_def
          get_root_node_pure returns_result_eq to_tree_order_same_root)
  qed
qed


lemma get_dom_component_no_overlap:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_dom_component ptr' →⇩r c'"
  shows "set c ∩ set c' = {} ∨ c = c'"
proof (rule ccontr, auto)
  fix x
  assume 1: "c ≠ c'" and 2: "x ∈ set c" and 3: "x ∈ set c'"
  obtain root_ptr where root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    using assms(4) unfolding get_dom_component_def
    by (meson bind_is_OK_E is_OK_returns_result_I)
  moreover obtain root_ptr' where root_ptr': "h ⊢ get_root_node ptr' →⇩r root_ptr'"
    using assms(5) unfolding get_dom_component_def
    by (meson bind_is_OK_E is_OK_returns_result_I)
  ultimately have "root_ptr ≠ root_ptr'"
    using 1 assms
    unfolding get_dom_component_def
    by (meson bind_returns_result_E3 get_root_node_pure returns_result_eq)

  moreover have "h ⊢ get_root_node x →⇩r root_ptr"
    using 2 root_ptr get_dom_component_root_node_same assms by blast
  moreover have "h ⊢ get_root_node x →⇩r root_ptr'"
    using 3 root_ptr' get_dom_component_root_node_same assms by blast
  ultimately show False
    using select_result_I2 by force
qed

lemma get_dom_component_separates_tree_order:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ to_tree_order ptr →⇩r to"
  assumes "h ⊢ get_dom_component ptr' →⇩r c'"
  assumes "ptr' ∉ set c"
  shows "set to ∩ set c' = {}"
proof -
  have "c ≠ c'"
    using assms get_dom_component_ptr by blast
  then have "set c ∩ set c' = {}"
    using assms get_dom_component_no_overlap by blast
  moreover have "set to ⊆ set c"
    using assms get_dom_component_to_tree_order_subset by blast
  ultimately show ?thesis
    by blast
qed

lemma get_dom_component_separates_tree_order_general:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ to_tree_order ptr'' →⇩r to''"
  assumes "ptr'' ∈ set c"
  assumes "h ⊢ get_dom_component ptr' →⇩r c'"
  assumes "ptr' ∉ set c"
  shows "set to'' ∩ set c' = {}"
proof -
  obtain root_ptr where root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    using assms(4)
    by (metis bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  then have c: "h ⊢ to_tree_order root_ptr →⇩r c"
    using assms(4) unfolding get_dom_component_def
    by (simp add: bind_returns_result_E3)
  with root_ptr show ?thesis
    using assms get_dom_component_separates_tree_order get_dom_component_subset
    by meson
qed
end

interpretation i_get_dom_component?: l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component_safe
  is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors get_ancestors_locs
  get_disconnected_nodes get_disconnected_nodes_locs get_element_by_id get_elements_by_class_name
  get_elements_by_tag_name
  by(auto simp add: l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms_def
      get_dom_component_def is_strongly_dom_component_safe_def is_weakly_dom_component_safe_def instances)
declare l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_child\_nodes›

locale l_get_dom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_child_nodes_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_child_nodes ptr' →⇩r children"
  assumes "child ∈ set children"
  shows "cast child ∈ set c ⟷ ptr' ∈ set c"
proof
  assume 1: "cast child ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  have "h ⊢ get_root_node (cast child) →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using assms(1) assms(2) assms(3) assms(5) assms(6) local.child_parent_dual
      local.get_root_node_parent_same by blast
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using "1" assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) local.child_parent_dual
      local.get_dom_component_parent_inside local.get_dom_component_subset by blast
  then show "ptr' ∈ set c"
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
next
  assume 1: "ptr' ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node (cast child) →⇩r root_ptr"
    using assms(1) assms(2) assms(3) assms(5) assms(6) local.child_parent_dual
      local.get_root_node_parent_same by blast
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using "1" assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) local.child_parent_dual
      local.get_dom_component_parent_inside local.get_dom_component_subset by blast
  then show "cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child ∈ set c"
    by (smt (verit) ‹h ⊢ get_root_node (cast⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r child) →⇩r root_ptr› assms(1) assms(2) assms(3)
        assms(5) assms(6) disjoint_iff_not_equal is_OK_returns_result_E is_OK_returns_result_I
        l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.get_dom_component_no_overlap local.child_parent_dual local.get_dom_component_ok
        local.get_dom_component_parent_inside local.get_dom_component_ptr local.get_root_node_ptr_in_heap
        local.l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms)
qed


lemma get_child_nodes_get_dom_component:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_child_nodes ptr →⇩r children"
  shows "cast ` set children ⊆ set c"
  using assms get_child_nodes_is_strongly_dom_component_safe
  using local.get_dom_component_ptr by auto


lemma
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_child_nodes ptr →⇩r children"
  assumes "h ⊢ get_child_nodes ptr →⇩h h'"
  shows "is_strongly_dom_component_safe {ptr} (cast ` set children) h h'"
proof -
  have "h = h'"
    using assms(5)
    by (meson local.get_child_nodes_pure pure_returns_heap_eq)
  then show ?thesis
    using assms
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def Bex_def)[1]
    by (smt (verit) IntI get_child_nodes_is_strongly_dom_component_safe
        is_OK_returns_result_I local.get_child_nodes_ptr_in_heap local.get_dom_component_impl
        local.get_dom_component_ok local.get_dom_component_ptr returns_result_select_result)

qed
end

interpretation i_get_dom_component_get_child_nodes?: l_get_dom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_child_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_parent›

locale l_get_dom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_parent_is_strongly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_parent ptr' →⇩r Some parent"
  shows "parent ∈ set c ⟷ cast ptr' ∈ set c"
  by (meson assms(1) assms(2) assms(3) assms(4) assms(5) is_OK_returns_result_E
      l_to_tree_order_wf.to_tree_order_parent local.get_dom_component_parent_inside
      local.get_dom_component_subset local.get_dom_component_to_tree_order_subset
      local.get_parent_parent_in_heap local.l_to_tree_order_wf_axioms local.to_tree_order_ok
      local.to_tree_order_ptr_in_result subsetCE)


lemma get_parent_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_parent node_ptr →⇩r Some parent"
  assumes "h ⊢ get_parent node_ptr →⇩h h'"
  shows "is_strongly_dom_component_safe {cast node_ptr} {parent} h h'"
proof -
  have "h = h'"
    using assms(5)
    by (meson local.get_parent_pure pure_returns_heap_eq)
  then show ?thesis
    using assms
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def)[1]
    by (metis IntI local.get_dom_component_impl local.get_dom_component_ok
        local.get_dom_component_parent_inside local.get_dom_component_ptr local.get_parent_parent_in_heap
        local.known_ptrs_known_ptr local.parent_child_rel_child_in_heap local.parent_child_rel_parent
        returns_result_select_result)
qed
end

interpretation i_get_dom_component_get_parent?: l_get_dom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_parent⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_root\_node›

locale l_get_dom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_root_node_is_strongly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_root_node ptr' →⇩r root"
  shows "root ∈ set c ⟷ ptr' ∈ set c"
proof
  assume 1: "root ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  have "h ⊢ get_root_node root →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  moreover have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    by (metis (no_types, lifting) calculation assms(1) assms(2) assms(3) assms(5)
        is_OK_returns_result_E local.get_root_node_root_in_heap local.to_tree_order_ok
        local.to_tree_order_ptr_in_result local.to_tree_order_same_root select_result_I2)
  ultimately have "h ⊢ get_dom_component ptr' →⇩r c"
    apply(auto simp add: get_dom_component_def)[1]
    using assms(4) bind_returns_result_E3 local.get_dom_component_def root_ptr by fastforce
  then show "ptr' ∈ set c"
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
next
  assume 1: "ptr' ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node root →⇩r root_ptr"
    by (metis assms(1) assms(2) assms(3) assms(5) is_OK_returns_result_E
        local.get_root_node_root_in_heap local.to_tree_order_ok local.to_tree_order_ptr_in_result
        local.to_tree_order_same_root returns_result_eq)
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using "1" assms(1) assms(2) assms(3) assms(4) local.get_dom_component_subset by blast
  then show "root ∈ set c"
    using assms(5) bind_returns_result_E3 local.get_dom_component_def local.to_tree_order_ptr_in_result
    by fastforce
qed

lemma get_root_node_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_root_node ptr →⇩r root"
  assumes "h ⊢ get_root_node ptr →⇩h h'"
  shows "is_strongly_dom_component_safe {ptr} {root} h h'"
proof -
  have "h = h'"
    using assms(5)
    by (meson local.get_root_node_pure pure_returns_heap_eq)
  then show ?thesis
    using assms
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def)[1]
    by (metis (no_types, opaque_lifting) IntI get_root_node_is_strongly_dom_component_safe_step
        is_OK_returns_result_I local.get_dom_component_impl local.get_dom_component_ok
        local.get_dom_component_ptr local.get_root_node_ptr_in_heap returns_result_select_result)
qed
end

interpretation i_get_dom_component_get_root_node?: l_get_dom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_root_node⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_element\_by\_id›

locale l_get_dom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_first_in_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_element_by_id_is_strongly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_element_by_id ptr' idd →⇩r Some result"
  shows "cast result ∈ set c ⟷ ptr' ∈ set c"
proof
  assume 1: "cast result ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  then have "h ⊢ to_tree_order root_ptr →⇩r c"
    using ‹h ⊢ get_dom_component ptr →⇩r c›
    by (simp add: get_dom_component_def bind_returns_result_E3)

  obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    using ‹h ⊢ get_element_by_id ptr' idd →⇩r Some result›
    apply(simp add: get_element_by_id_def first_in_tree_order_def)
    by (meson bind_is_OK_E is_OK_returns_result_I)
  then have "cast result ∈ set to'"
    using ‹h ⊢ get_element_by_id ptr' idd →⇩r Some result› get_element_by_id_result_in_tree_order
    by blast

  have "h ⊢ get_root_node (cast result) →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using ‹cast result ∈ set to'› ‹h ⊢ to_tree_order ptr' →⇩r to'›
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_ptr get_dom_component_root_node_same
      get_dom_component_subset get_dom_component_to_tree_order
    by blast
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using ‹h ⊢ to_tree_order root_ptr →⇩r c›
    using get_dom_component_def by auto
  then show "ptr' ∈ set c"
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
next
  assume "ptr' ∈ set c"
  moreover obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    by (meson assms(1) assms(2) assms(3) assms(4) calculation get_dom_component_ptr_in_heap
        get_dom_component_subset is_OK_returns_result_E is_OK_returns_result_I to_tree_order_ok)
  ultimately have "set to' ⊆ set c"
    using assms(1) assms(2) assms(3) assms(4) get_dom_component_subset
      get_dom_component_to_tree_order_subset
    by blast
  moreover have "cast result ∈ set to'"
    using assms(5) get_element_by_id_result_in_tree_order to' by blast
  ultimately show "cast result ∈ set c"
    by blast
qed


lemma get_element_by_id_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_element_by_id ptr idd →⇩r Some result"
  assumes "h ⊢ get_element_by_id ptr idd →⇩h h'"
  shows "is_strongly_dom_component_safe {ptr} {cast result} h h'"
proof -
  have "h = h'"
    using assms(5)
    by(auto simp add: preserved_def get_element_by_id_def first_in_tree_order_def
        elim!: bind_returns_heap_E2 intro!: map_filter_M_pure bind_pure_I
        split: option.splits list.splits)
  have "ptr |∈| object_ptr_kinds h"
    using assms(4)
    apply(auto simp add: get_element_by_id_def)[1]
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
        local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
  obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
    by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
        local.to_tree_order_ok)
  then have "cast result ∈ set to"
    using assms(4) local.get_element_by_id_result_in_tree_order by auto
  obtain c where c: "h ⊢ a_get_dom_component ptr →⇩r c"
    using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_dom_component_impl
      local.get_dom_component_ok by blast

  then show ?thesis
    using assms ‹h = h'›
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def get_element_by_id_def
        first_in_tree_order_def elim!: bind_returns_result_E2 intro!: map_filter_M_pure bind_pure_I
        split: option.splits list.splits)[1]
    by (metis (no_types, opaque_lifting) Int_iff ‹ptr |∈| object_ptr_kinds h› assms(4)
        get_element_by_id_is_strongly_dom_component_safe_step local.get_dom_component_impl
        local.get_dom_component_ptr select_result_I2)
qed
end

interpretation i_get_dom_component_get_element_by_id?: l_get_dom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_element_by_id⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]

subsubsection ‹get\_elements\_by\_class\_name›

locale l_get_dom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_first_in_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_elements_by_class_name_is_strongly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_elements_by_class_name ptr' idd →⇩r results"
  assumes "result ∈ set results"
  shows "cast result ∈ set c ⟷ ptr' ∈ set c"
proof
  assume 1: "cast result ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  then have "h ⊢ to_tree_order root_ptr →⇩r c"
    using ‹h ⊢ get_dom_component ptr →⇩r c›
    by (simp add: get_dom_component_def bind_returns_result_E3)

  obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    using assms(5)
    apply(simp add: get_elements_by_class_name_def first_in_tree_order_def)
    by (meson bind_is_OK_E is_OK_returns_result_I)
  then have "cast result ∈ set to'"
    using assms get_elements_by_class_name_result_in_tree_order by blast

  have "h ⊢ get_root_node (cast result) →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using ‹cast result ∈ set to'› ‹h ⊢ to_tree_order ptr' →⇩r to'›
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_ptr get_dom_component_root_node_same
      get_dom_component_subset get_dom_component_to_tree_order
    by blast
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using ‹h ⊢ to_tree_order root_ptr →⇩r c›
    using get_dom_component_def by auto
  then show "ptr' ∈ set c"
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
next
  assume "ptr' ∈ set c"
  moreover obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    by (meson assms(1) assms(2) assms(3) assms(4) calculation get_dom_component_ptr_in_heap
        get_dom_component_subset is_OK_returns_result_E is_OK_returns_result_I to_tree_order_ok)
  ultimately have "set to' ⊆ set c"
    using assms(1) assms(2) assms(3) assms(4) get_dom_component_subset
      get_dom_component_to_tree_order_subset
    by blast
  moreover have "cast result ∈ set to'"
    using assms get_elements_by_class_name_result_in_tree_order to' by blast
  ultimately show "cast result ∈ set c"
    by blast
qed

lemma get_elements_by_class_name_pure [simp]:
  "pure (get_elements_by_class_name ptr name) h"
  by(auto simp add: get_elements_by_class_name_def intro!: bind_pure_I map_filter_M_pure
      split: option.splits)

lemma get_elements_by_class_name_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_elements_by_class_name ptr name →⇩r results"
  assumes "h ⊢ get_elements_by_class_name ptr name →⇩h h'"
  shows "is_strongly_dom_component_safe {ptr} (cast ` set results) h h'"
proof -
  have "h = h'"
    using assms(5)
    by (meson get_elements_by_class_name_pure pure_returns_heap_eq)
  have "ptr |∈| object_ptr_kinds h"
    using assms(4)
    apply(auto simp add: get_elements_by_class_name_def)[1]
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
        local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
  obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
    by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
        local.to_tree_order_ok)
  then have "cast ` set results ⊆ set to"
    using assms(4) local.get_elements_by_class_name_result_in_tree_order by auto
  obtain c where c: "h ⊢ a_get_dom_component ptr →⇩r c"
    using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_dom_component_impl
      local.get_dom_component_ok by blast

  then show ?thesis
    using assms ‹h = h'›
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def
        get_elements_by_class_name_def first_in_tree_order_def elim!: bind_returns_result_E2
        intro!: map_filter_M_pure bind_pure_I split: option.splits list.splits)[1]
    by (metis (no_types, opaque_lifting) Int_iff ‹ptr |∈| object_ptr_kinds h› assms(4)
        get_elements_by_class_name_is_strongly_dom_component_safe_step local.get_dom_component_impl
        local.get_dom_component_ptr select_result_I2)
qed
end

interpretation i_get_dom_component_get_elements_by_class_name?:
  l_get_dom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_elements_by_class_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹get\_elements\_by\_tag\_name›

locale l_get_dom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_first_in_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_to_tree_order⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M +
  l_get_element_by⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M
begin

lemma get_elements_by_tag_name_is_strongly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_dom_component ptr →⇩r c"
  assumes "h ⊢ get_elements_by_tag_name ptr' idd →⇩r results"
  assumes "result ∈ set results"
  shows "cast result ∈ set c ⟷ ptr' ∈ set c"
proof
  assume 1: "cast result ∈ set c"
  obtain root_ptr where
    root_ptr: "h ⊢ get_root_node ptr →⇩r root_ptr"
    by (metis assms(4) bind_is_OK_E get_dom_component_def is_OK_returns_result_I)
  then have "h ⊢ to_tree_order root_ptr →⇩r c"
    using ‹h ⊢ get_dom_component ptr →⇩r c›
    by (simp add: get_dom_component_def bind_returns_result_E3)

  obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    using assms(5)
    apply(simp add: get_elements_by_tag_name_def first_in_tree_order_def)
    by (meson bind_is_OK_E is_OK_returns_result_I)
  then have "cast result ∈ set to'"
    using assms get_elements_by_tag_name_result_in_tree_order by blast

  have "h ⊢ get_root_node (cast result) →⇩r root_ptr"
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_root_node_same root_ptr
    by blast
  then have "h ⊢ get_root_node ptr' →⇩r root_ptr"
    using ‹cast result ∈ set to'› ‹h ⊢ to_tree_order ptr' →⇩r to'›
    using "1" assms(1) assms(2) assms(3) assms(4) get_dom_component_ptr
      get_dom_component_root_node_same get_dom_component_subset get_dom_component_to_tree_order
    by blast
  then have "h ⊢ get_dom_component ptr' →⇩r c"
    using ‹h ⊢ to_tree_order root_ptr →⇩r c›
    using get_dom_component_def by auto
  then show "ptr' ∈ set c"
    using assms(1) assms(2) assms(3) get_dom_component_ptr by blast
next
  assume "ptr' ∈ set c"
  moreover obtain to' where to': "h ⊢ to_tree_order ptr' →⇩r to'"
    by (meson assms(1) assms(2) assms(3) assms(4) calculation get_dom_component_ptr_in_heap
        get_dom_component_subset is_OK_returns_result_E is_OK_returns_result_I to_tree_order_ok)
  ultimately have "set to' ⊆ set c"
    using assms(1) assms(2) assms(3) assms(4) get_dom_component_subset
      get_dom_component_to_tree_order_subset
    by blast
  moreover have "cast result ∈ set to'"
    using assms get_elements_by_tag_name_result_in_tree_order to' by blast
  ultimately show "cast result ∈ set c"
    by blast
qed

lemma get_elements_by_tag_name_is_strongly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_elements_by_tag_name ptr name →⇩r results"
  assumes "h ⊢ get_elements_by_tag_name ptr name →⇩h h'"
  shows "is_strongly_dom_component_safe {ptr} (cast ` set results) h h'"
proof -
  have "h = h'"
    using assms(5)
    by (meson get_elements_by_tag_name_pure pure_returns_heap_eq)
  have "ptr |∈| object_ptr_kinds h"
    using assms(4)
    apply(auto simp add: get_elements_by_tag_name_def)[1]
    by (metis (no_types, lifting) assms(1) assms(2) assms(3) bind_is_OK_E is_OK_returns_result_I
        local.first_in_tree_order_def local.to_tree_order_ptr_in_result local.to_tree_order_ptrs_in_heap)
  obtain to where to: "h ⊢ to_tree_order ptr →⇩r to"
    by (meson ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) is_OK_returns_result_E
        local.to_tree_order_ok)
  then have "cast ` set results ⊆ set to"
    using assms(4) local.get_elements_by_tag_name_result_in_tree_order by auto
  obtain c where c: "h ⊢ a_get_dom_component ptr →⇩r c"
    using ‹ptr |∈| object_ptr_kinds h› assms(1) assms(2) assms(3) local.get_dom_component_impl
      local.get_dom_component_ok by blast

  then show ?thesis
    using assms ‹h = h'›
    apply(auto simp add: is_strongly_dom_component_safe_def Let_def preserved_def
        get_elements_by_class_name_def first_in_tree_order_def elim!: bind_returns_result_E2
        intro!: map_filter_M_pure bind_pure_I split: option.splits list.splits)[1]
    by (metis (no_types, opaque_lifting) IntI ‹ptr |∈| object_ptr_kinds h›
        get_elements_by_tag_name_is_strongly_dom_component_safe_step local.get_dom_component_impl
        local.get_dom_component_ptr select_result_I2)
qed
end

interpretation i_get_dom_component_get_elements_by_tag_name?:
  l_get_dom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_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 first_in_tree_order get_attribute get_attribute_locs
  by(auto simp add: l_get_dom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_get_elements_by_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹remove\_child›

lemma remove_child_unsafe: "¬(∀(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}) heap
  ) h' ptr child. heap_is_wellformed h ⟶ type_wf h ⟶ known_ptrs h ⟶
h ⊢ remove_child ptr child →⇩h h' ⟶ is_weakly_dom_component_safe {ptr, cast child} {} h h')"
proof -
  obtain h document_ptr e1 e2 where h: "Inr ((document_ptr, e1, e2), h) = (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}) heap
    ) ⊢ (do {
      document_ptr ← create_document;
      e1 ← create_element document_ptr ''div'';
      e2 ← create_element document_ptr ''div'';
      append_child (cast e1) (cast e2);
      return (document_ptr, e1, e2)
  })"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then obtain h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    h': "h ⊢ remove_child (cast e1) (cast e2) →⇩h h'" and
    "¬(is_weakly_dom_component_safe {cast e1, cast e2} {} h h')"
    apply(code_simp)
    apply(clarify)
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then show ?thesis
    by auto
qed


subsubsection ‹adopt\_node›

lemma adopt_node_unsafe: "¬(∀(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}) heap
  ) h' document_ptr child. heap_is_wellformed h ⟶ type_wf h ⟶ known_ptrs h ⟶ h ⊢ adopt_node document_ptr child →⇩h h' ⟶ is_weakly_dom_component_safe {cast document_ptr, cast child} {} h h')"
proof -
  obtain h document_ptr document_ptr2 e1 where h: "Inr ((document_ptr, document_ptr2, e1), h) = (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}) heap
    ) ⊢ (do {
      document_ptr ← create_document;
      document_ptr2 ← create_document;
      e1 ← create_element document_ptr ''div'';
      adopt_node document_ptr2 (cast e1);
      return (document_ptr, document_ptr2, e1)
  })"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then obtain h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    h': "h ⊢ adopt_node document_ptr (cast e1) →⇩h h'" and
    "¬(is_weakly_dom_component_safe {cast document_ptr, cast e1} {} h h')"
    apply(code_simp)
    apply(clarify)
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then show ?thesis
    by auto
qed


subsubsection ‹create\_element›

lemma create_element_not_strongly_dom_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder}, 'element_ptr::{equal,linorder},
'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}) heap" and
    h' and document_ptr and new_element_ptr and tag where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h ⊢ create_element document_ptr tag →⇩r new_element_ptr →⇩h h'" and
    "¬ is_strongly_dom_component_safe {cast document_ptr} {cast new_element_ptr} h h'"
proof -
  let ?h0 = "Heap fmempty ::('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder}, 'document_ptr::{equal,linorder},
'shadow_root_ptr::{equal,linorder}, 'Object::{equal,linorder}, 'Node::{equal,linorder},
'Element::{equal,linorder}, 'CharacterData::{equal,linorder}, 'Document::{equal,linorder}) heap"
  let ?P = "create_document"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?document_ptr = "|?h0 ⊢ ?P|⇩r"

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


locale l_get_dom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component_safe is_weakly_dom_component_safe get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_disconnected_nodes get_disconnected_nodes_locs get_element_by_id
  get_elements_by_class_name get_elements_by_tag_name +
  l_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
  set_disconnected_nodes_locs set_tag_name set_tag_name_locs type_wf create_element known_ptr +
  l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_disconnected_nodes set_disconnected_nodes_locs +
  l_set_tag_name⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_tag_name set_tag_name_locs +
  l_new_element_get_disconnected_nodes get_disconnected_nodes get_disconnected_nodes_locs +
  l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
  l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr
  get_child_nodes get_child_nodes_locs +
  l_create_element_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr known_ptrs type_wf get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs heap_is_wellformed parent_child_rel set_tag_name
  set_tag_name_locs
  set_disconnected_nodes set_disconnected_nodes_locs create_element
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and type_wf :: "(_) heap ⇒ bool"
    and known_ptrs :: "(_) heap ⇒ bool"
    and to_tree_order :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_dom_component :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and is_strongly_dom_component_safe :: "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and is_weakly_dom_component_safe :: "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and get_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_ancestors :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_ancestors_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_element_by_id :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr option) prog"
    and get_elements_by_class_name :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and get_elements_by_tag_name :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ ((_) heap, exception, unit) prog"
    and set_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap, exception, unit) prog set"
    and set_tag_name :: "(_) element_ptr ⇒ char list ⇒ ((_) heap, exception, unit) prog"
    and set_tag_name_locs :: "(_) element_ptr ⇒ ((_) heap, exception, unit) prog set"
    and create_element :: "(_) document_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr) prog"
begin

lemma create_element_is_weakly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_element document_ptr tag →⇩h h'"
  assumes "ptr ∉ set |h ⊢ get_dom_component (cast document_ptr)|⇩r"
  assumes "ptr ≠ cast |h ⊢ create_element document_ptr tag|⇩r"
  shows "preserved (get_M ptr getter) h h'"
proof -
  obtain new_element_ptr h2 h3 disc_nodes where
    new_element_ptr: "h ⊢ new_element →⇩r new_element_ptr" and
    h2: "h ⊢ new_element →⇩h h2" and
    h3: "h2 ⊢set_tag_name new_element_ptr tag →⇩h h3" and
    disc_nodes: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes" and
    h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes) →⇩h h'"
    using assms(4)
    by(auto simp add: create_element_def
        elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated])
  have "h ⊢ create_element document_ptr tag →⇩r new_element_ptr"
    using new_element_ptr h2 h3 disc_nodes h'
    apply(auto simp add: create_element_def intro!: bind_returns_result_I
        bind_pure_returns_result_I[OF get_disconnected_nodes_pure])[1]
     apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
    by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
  have "preserved (get_M ptr getter) h h2"
    using h2 new_element_ptr
    apply(rule new_element_get_M⇩O⇩b⇩j⇩e⇩c⇩t)
    using new_element_ptr assms(6) ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr›
    by simp

  have "preserved (get_M ptr getter) h2 h3"
    using set_tag_name_writes h3
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_tag_name_locs_impl a_set_tag_name_locs_def all_args_def)[1]
    by (metis (no_types, lifting) ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› assms(6)
        get_M_Element_preserved8 select_result_I2)

  have "document_ptr |∈| document_ptr_kinds h"
    using create_element_document_in_heap
    using assms(4)
    by blast
  then
  have "ptr ≠ (cast document_ptr)"
    using assms(5) assms(1) assms(2) assms(3) local.get_dom_component_ok local.get_dom_component_ptr
    by auto
  have "preserved (get_M ptr getter) h3 h'"
    using set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_disconnected_nodes_locs_def all_args_def)[1]
    by (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)

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


lemma create_element_is_weakly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_element document_ptr tag →⇩r result"
  assumes "h ⊢ create_element document_ptr tag →⇩h h'"
  shows "is_weakly_dom_component_safe {cast document_ptr} {cast result} h h'"
proof -

  obtain new_element_ptr h2 h3 disc_nodes_h3 where
    new_element_ptr: "h ⊢ new_element →⇩r new_element_ptr" and
    h2: "h ⊢ new_element →⇩h h2" and
    h3: "h2 ⊢ set_tag_name new_element_ptr tag →⇩h h3" and
    disc_nodes_h3: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3" and
    h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes_h3) →⇩h h'"
    using assms(5)
    by(auto simp add: create_element_def
        elim!: bind_returns_heap_E
        bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
  then have "h ⊢ create_element document_ptr tag →⇩r new_element_ptr"
    apply(auto simp add: create_element_def intro!: bind_returns_result_I)[1]
      apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
     apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure
        pure_returns_heap_eq)
    by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)

  have "new_element_ptr ∉ set |h ⊢ element_ptr_kinds_M|⇩r"
    using new_element_ptr ElementMonad.ptr_kinds_ptr_kinds_M h2
    using new_element_ptr_not_in_heap by blast
  then have "cast new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r"
    by simp
  then have "cast new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r"
    by simp

  have object_ptr_kinds_eq_h: "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
    using new_element_new_ptr h2 new_element_ptr by blast
  then have node_ptr_kinds_eq_h: "node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_element_ptr|}"
    apply(simp add: node_ptr_kinds_def)
    by force
  then have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h |∪| {|new_element_ptr|}"
    apply(simp add: element_ptr_kinds_def)
    by force
  have character_data_ptr_kinds_eq_h: "character_data_ptr_kinds h2 = character_data_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: node_ptr_kinds_def character_data_ptr_kinds_def)
  have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: document_ptr_kinds_def)

  have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_tag_name_writes h3])
    using set_tag_name_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
    using object_ptr_kinds_eq_h2
    by(auto simp add: node_ptr_kinds_def)

  have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_disconnected_nodes_writes h'])
    using set_disconnected_nodes_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
    using object_ptr_kinds_eq_h3
    by(auto simp add: node_ptr_kinds_def)

  have "known_ptr (cast new_element_ptr)"
    using ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› local.create_element_known_ptr
    by blast
  then
  have "known_ptrs h2"
    using known_ptrs_new_ptr object_ptr_kinds_eq_h ‹known_ptrs h› h2
    by blast
  then
  have "known_ptrs h3"
    using known_ptrs_preserved object_ptr_kinds_eq_h2 by blast
  then
  have "known_ptrs h'"
    using known_ptrs_preserved object_ptr_kinds_eq_h3 by blast


  have "document_ptr |∈| document_ptr_kinds h"
    using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
      get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
    by (metis is_OK_returns_result_I)

  have children_eq_h: "⋀(ptr'::(_) object_ptr) children. ptr' ≠ cast new_element_ptr
              ⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads h2 get_child_nodes_new_element[rotated, OF new_element_ptr h2]
    apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
    by blast+
  then have children_eq2_h: "⋀ptr'. ptr' ≠ cast new_element_ptr
                                    ⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force

  have "h2 ⊢ get_child_nodes (cast new_element_ptr) →⇩r []"
    using new_element_ptr h2 new_element_ptr_in_heap[OF h2 new_element_ptr]
      new_element_is_element_ptr[OF new_element_ptr] new_element_no_child_nodes
    by blast
  have disconnected_nodes_eq_h:
    "⋀doc_ptr disc_nodes. h ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                                             = h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads h2 get_disconnected_nodes_new_element[OF new_element_ptr h2]
    apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
    by blast+
  then have disconnected_nodes_eq2_h:
    "⋀doc_ptr. |h ⊢ get_disconnected_nodes doc_ptr|⇩r = |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have children_eq_h2:
    "⋀ptr' children. h2 ⊢ get_child_nodes ptr' →⇩r children = h3 ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads set_tag_name_writes h3
    apply(rule reads_writes_preserved)
    by(auto simp add: set_tag_name_get_child_nodes)
  then have children_eq2_h2: "⋀ptr'. |h2 ⊢ get_child_nodes ptr'|⇩r = |h3 ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force
  have disconnected_nodes_eq_h2:
    "⋀doc_ptr disc_nodes. h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                                               = h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads set_tag_name_writes h3
    apply(rule reads_writes_preserved)
    by(auto simp add: set_tag_name_get_disconnected_nodes)
  then have disconnected_nodes_eq2_h2:
    "⋀doc_ptr. |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have "type_wf h2"
    using ‹type_wf h› new_element_types_preserved h2 by blast
  then have "type_wf h3"
    using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_tag_name_writes h3]
    using  set_tag_name_types_preserved
    by(auto simp add: reflp_def transp_def)
  then have "type_wf h'"
    using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h']
    using  set_disconnected_nodes_types_preserved
    by(auto simp add: reflp_def transp_def)

  have children_eq_h3:
    "⋀ptr' children. h3 ⊢ get_child_nodes ptr' →⇩r children = h' ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved)
    by(auto simp add: set_disconnected_nodes_get_child_nodes)
  then have children_eq2_h3: "⋀ptr'. |h3 ⊢ get_child_nodes ptr'|⇩r = |h' ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force
  have disconnected_nodes_eq_h3:
    "⋀doc_ptr disc_nodes. document_ptr ≠ doc_ptr
       ⟹ h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                                               = h' ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved)
    by(auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
  then have disconnected_nodes_eq2_h3:
    "⋀doc_ptr. document_ptr ≠ doc_ptr
                ⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have disc_nodes_document_ptr_h2: "h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
    using disconnected_nodes_eq_h2 disc_nodes_h3 by auto
  then have disc_nodes_document_ptr_h: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
    using disconnected_nodes_eq_h by auto
  then have "cast new_element_ptr ∉ set disc_nodes_h3"
    using ‹heap_is_wellformed h›
    using ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r›
      a_all_ptrs_in_heap_def heap_is_wellformed_def
    using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast

  have "acyclic (parent_child_rel h)"
    using ‹heap_is_wellformed h›
    by (simp add: heap_is_wellformed_def acyclic_heap_def)
  also have "parent_child_rel h = parent_child_rel h2"
  proof(auto simp add: parent_child_rel_def)[1]
    fix a x
    assume 0: "a |∈| object_ptr_kinds h"
      and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
    then show "a |∈| object_ptr_kinds h2"
      by (simp add: object_ptr_kinds_eq_h)
  next
    fix a x
    assume 0: "a |∈| object_ptr_kinds h"
      and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
    then show "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
      by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
          ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r› children_eq2_h)
  next
    fix a x
    assume 0: "a |∈| object_ptr_kinds h2"
      and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
    then show "a |∈| object_ptr_kinds h"
      using object_ptr_kinds_eq_h ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []›
      by(auto)
  next
    fix a x
    assume 0: "a |∈| object_ptr_kinds h2"
      and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
    then show "x ∈ set |h ⊢ get_child_nodes a|⇩r"
      by (metis (no_types, lifting)
          ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []›
          children_eq2_h empty_iff empty_set image_eqI select_result_I2)
  qed
  also have "… = parent_child_rel h3"
    by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h2 children_eq2_h2)
  also have "… = parent_child_rel h'"
    by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h3 children_eq2_h3)
  finally have "a_acyclic_heap h'"
    by (simp add: acyclic_heap_def)

  have "a_all_ptrs_in_heap h"
    using ‹heap_is_wellformed h›  by (simp add: heap_is_wellformed_def)
  then have "a_all_ptrs_in_heap h2"
    apply(auto simp add: a_all_ptrs_in_heap_def)[1]
     apply (metis ‹known_ptrs h2› ‹parent_child_rel h = parent_child_rel h2› ‹type_wf h2› assms
        funion_iff local.get_child_nodes_ok local.known_ptrs_known_ptr local.parent_child_rel_child_in_heap
        local.parent_child_rel_child_nodes2 node_ptr_kinds_commutes node_ptr_kinds_eq_h
        returns_result_select_result)
    by (metis assms disconnected_nodes_eq2_h document_ptr_kinds_eq_h funion_iff
        local.get_disconnected_nodes_ok local.heap_is_wellformed_disc_nodes_in_heap node_ptr_kinds_eq_h
        returns_result_select_result)
  then have "a_all_ptrs_in_heap h3"
    by (simp add: children_eq2_h2 disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2
        local.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 object_ptr_kinds_eq_h2)
  then have "a_all_ptrs_in_heap h'"
    using assms(1) assms(2) assms(3) assms(5) local.create_element_preserves_wellformedness(1) local.heap_is_wellformed_def
    by blast

  have "⋀p. p |∈| object_ptr_kinds h ⟹ cast new_element_ptr ∉ set |h ⊢ get_child_nodes p|⇩r"
    using ‹heap_is_wellformed h› ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r›
      heap_is_wellformed_children_in_heap
    by (meson NodeMonad.ptr_kinds_ptr_kinds_M a_all_ptrs_in_heap_def assms fset_mp
        fset_of_list_elem get_child_nodes_ok known_ptrs_known_ptr returns_result_select_result)
  then have "⋀p. p |∈| object_ptr_kinds h2 ⟹ cast new_element_ptr ∉ set |h2 ⊢ get_child_nodes p|⇩r"
    using children_eq2_h
    apply(auto simp add: object_ptr_kinds_eq_h)[1]
    using ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []› apply auto[1]
    by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
        ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r›)
  then have "⋀p. p |∈| object_ptr_kinds h3 ⟹ cast new_element_ptr ∉ set |h3 ⊢ get_child_nodes p|⇩r"
    using object_ptr_kinds_eq_h2 children_eq2_h2 by auto
  then have new_element_ptr_not_in_any_children:
    "⋀p. p |∈| object_ptr_kinds h' ⟹ cast new_element_ptr ∉ set |h' ⊢ get_child_nodes p|⇩r"
    using object_ptr_kinds_eq_h3 children_eq2_h3 by auto

  have "a_distinct_lists h"
    using ‹heap_is_wellformed h›
    by (simp add: heap_is_wellformed_def)
  then have "a_distinct_lists h2"

    using ‹h2 ⊢ get_child_nodes (cast new_element_ptr) →⇩r []›
    apply(auto simp add: a_distinct_lists_def object_ptr_kinds_eq_h document_ptr_kinds_eq_h
        disconnected_nodes_eq2_h intro!: distinct_concat_map_I)[1]
       apply (metis distinct_sorted_list_of_set finite_fset sorted_list_of_set_insert_remove)
      apply(case_tac "x=cast new_element_ptr")
       apply(auto simp add: children_eq2_h[symmetric] insort_split dest: distinct_concat_map_E(2))[1]
      apply(auto simp add: children_eq2_h[symmetric] insort_split dest: distinct_concat_map_E(2))[1]
     apply(auto simp add: children_eq2_h[symmetric] insort_split dest: distinct_concat_map_E(2))[1]
     apply (metis IntI assms empty_iff local.get_child_nodes_ok
        local.heap_is_wellformed_one_parent local.known_ptrs_known_ptr returns_result_select_result)
    apply(auto simp add: children_eq2_h[symmetric] insort_split dest: distinct_concat_map_E(2))[1]
    by (metis ‹local.a_distinct_lists h› ‹type_wf h2› disconnected_nodes_eq_h document_ptr_kinds_eq_h
        local.distinct_lists_no_parent local.get_disconnected_nodes_ok returns_result_select_result)

  then have "a_distinct_lists h3"
    by(auto simp add: a_distinct_lists_def disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2
        children_eq2_h2 object_ptr_kinds_eq_h2)
  then have "a_distinct_lists h'"
  proof(auto simp add: a_distinct_lists_def disconnected_nodes_eq2_h3 children_eq2_h3
      object_ptr_kinds_eq_h3 document_ptr_kinds_eq_h3
      intro!: distinct_concat_map_I)[1]
    fix x
    assume "distinct (concat (map (λdocument_ptr. |h3 ⊢ get_disconnected_nodes document_ptr|⇩r)
                                              (sorted_list_of_set (fset (document_ptr_kinds h3)))))"
      and "x |∈| document_ptr_kinds h3"
    then show "distinct |h' ⊢ get_disconnected_nodes x|⇩r"
      using document_ptr_kinds_eq_h3 disconnected_nodes_eq_h3 h' set_disconnected_nodes_get_disconnected_nodes
      by (metis (no_types, lifting) ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set disc_nodes_h3›
          ‹a_distinct_lists h3› ‹type_wf h'› disc_nodes_h3 distinct.simps(2)
          distinct_lists_disconnected_nodes get_disconnected_nodes_ok returns_result_eq
          returns_result_select_result)
  next
    fix x y xa
    assume "distinct (concat (map (λdocument_ptr. |h3 ⊢ get_disconnected_nodes document_ptr|⇩r)
                                            (sorted_list_of_set (fset (document_ptr_kinds h3)))))"
      and "x |∈| document_ptr_kinds h3"
      and "y |∈| document_ptr_kinds h3"
      and "x ≠ y"
      and "xa ∈ set |h' ⊢ get_disconnected_nodes x|⇩r"
      and "xa ∈ set |h' ⊢ get_disconnected_nodes y|⇩r"
    moreover have "set |h3 ⊢ get_disconnected_nodes x|⇩r ∩ set |h3 ⊢ get_disconnected_nodes y|⇩r = {}"
      using calculation by(auto dest: distinct_concat_map_E(1))
    ultimately show "False"
      apply(-)
      apply(cases "x = document_ptr")
       apply (metis (mono_tags, lifting) Int_Collect Int_iff ‹type_wf h'› assms(1) assms(2) assms(3)
               assms(5) bot_set_def document_ptr_kinds_eq_h3 empty_Collect_eq
               l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.get_disconnected_nodes_ok
               l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M.heap_is_wellformed_one_disc_parent
               local.create_element_preserves_wellformedness(1)
               local.l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms
               local.l_heap_is_wellformed⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms returns_result_select_result)
      by (metis (no_types, opaque_lifting) ‹type_wf h'› assms(1) assms(2) assms(3) assms(5)
          disjoint_iff document_ptr_kinds_eq_h3 local.create_element_preserves_wellformedness(1)
          local.get_disconnected_nodes_ok local.heap_is_wellformed_one_disc_parent
          returns_result_select_result)
  next
    fix x xa xb
    assume 2: "(⋃x∈fset (object_ptr_kinds h3). set |h' ⊢ get_child_nodes x|⇩r)
                   ∩ (⋃x∈fset (document_ptr_kinds h3). set |h3 ⊢ get_disconnected_nodes x|⇩r) = {}"
      and 3: "xa |∈| object_ptr_kinds h3"
      and 4: "x ∈ set |h' ⊢ get_child_nodes xa|⇩r"
      and 5: "xb |∈| document_ptr_kinds h3"
      and 6: "x ∈ set |h' ⊢ get_disconnected_nodes xb|⇩r"
    show "False"
      using disc_nodes_document_ptr_h disconnected_nodes_eq2_h3
      apply -
      apply(cases "xb = document_ptr")
       apply (metis (no_types, opaque_lifting) "3" "4" "6"
          ‹⋀p. p |∈| object_ptr_kinds h3
                      ⟹ cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h3 ⊢ get_child_nodes p|⇩r›
          ‹a_distinct_lists h3› children_eq2_h3 disc_nodes_h3 distinct_lists_no_parent h'
          select_result_I2 set_ConsD set_disconnected_nodes_get_disconnected_nodes)
      by (metis "3" "4" "5" "6" ‹a_distinct_lists h3› ‹type_wf h3› children_eq2_h3
          distinct_lists_no_parent get_disconnected_nodes_ok returns_result_select_result)
  qed

  have "a_owner_document_valid h"
    using ‹heap_is_wellformed h›  by (simp add: heap_is_wellformed_def)
  then have "a_owner_document_valid h'"
    using disc_nodes_h3 ‹document_ptr |∈| document_ptr_kinds h›
    apply(auto simp add: a_owner_document_valid_def)[1]
    apply(auto simp add:  object_ptr_kinds_eq_h object_ptr_kinds_eq_h3 )[1]
    apply(auto simp add: object_ptr_kinds_eq_h2)[1]
    apply(auto simp add:  document_ptr_kinds_eq_h document_ptr_kinds_eq_h3 )[1]
    apply(auto simp add: document_ptr_kinds_eq_h2)[1]
    apply(auto simp add:  node_ptr_kinds_eq_h node_ptr_kinds_eq_h3 )[1]
    apply(auto simp add: node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h )[1]
     apply(auto simp add: children_eq2_h2[symmetric] children_eq2_h3[symmetric]
        disconnected_nodes_eq2_h disconnected_nodes_eq2_h2
        disconnected_nodes_eq2_h3)[1]
     apply (metis (no_types, lifting) document_ptr_kinds_eq_h h' list.set_intros(1)
        local.set_disconnected_nodes_get_disconnected_nodes select_result_I2)
    apply(simp add: object_ptr_kinds_eq_h)
    by(metis (no_types, opaque_lifting) NodeMonad.ptr_kinds_ptr_kinds_M
        ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩n⇩o⇩d⇩e⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r› children_eq2_h
        children_eq2_h2 children_eq2_h3 disconnected_nodes_eq2_h disconnected_nodes_eq2_h2
        disconnected_nodes_eq2_h3 document_ptr_kinds_eq_h h'
        l_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
        list.set_intros(2) local.l_set_disconnected_nodes_get_disconnected_nodes_axioms
        node_ptr_kinds_commutes select_result_I2)


  have "parent_child_rel h = parent_child_rel h'"
  proof -
    have "parent_child_rel h = parent_child_rel h2"
    proof(auto simp add: parent_child_rel_def)[1]
      fix a x
      assume 0: "a |∈| object_ptr_kinds h"
        and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
      then show "a |∈| object_ptr_kinds h2"
        by (simp add: object_ptr_kinds_eq_h)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h"
        and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
      then show "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
        by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
            ‹cast new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r› children_eq2_h)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h2"
        and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
      then show "a |∈| object_ptr_kinds h"
        using object_ptr_kinds_eq_h ‹h2 ⊢ get_child_nodes (cast new_element_ptr) →⇩r []›
        by(auto)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h2"
        and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
      then show "x ∈ set |h ⊢ get_child_nodes a|⇩r"
        by (metis (no_types, lifting) ‹h2 ⊢ get_child_nodes (cast new_element_ptr) →⇩r []›
            children_eq2_h empty_iff empty_set image_eqI select_result_I2)
    qed
    also have "… = parent_child_rel h3"
      by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h2 children_eq2_h2)
    also have "… = parent_child_rel h'"
      by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h3 children_eq2_h3)
    finally show ?thesis
      by simp
  qed
  have root: "h ⊢ get_root_node (cast document_ptr) →⇩r cast document_ptr"
    by (simp add: ‹document_ptr |∈| document_ptr_kinds h› local.get_root_node_not_node_same)
  then
  have root': "h' ⊢ get_root_node (cast document_ptr) →⇩r cast document_ptr"
    by (simp add: ‹document_ptr |∈| document_ptr_kinds h› document_ptr_kinds_eq_h
        local.get_root_node_not_node_same object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3)

  have "heap_is_wellformed h'" and "known_ptrs h'"
    using create_element_preserves_wellformedness assms
    by blast+

  have "cast result |∉| object_ptr_kinds h"
    using ‹cast new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r›
    by (metis (full_types) ObjectMonad.ptr_kinds_ptr_kinds_M
        ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› assms(4) returns_result_eq)

  obtain to where to: "h ⊢ to_tree_order (cast document_ptr) →⇩r to"
    by (meson ‹document_ptr |∈| document_ptr_kinds h› assms(1) assms(2) assms(3)
        document_ptr_kinds_commutes is_OK_returns_result_E local.to_tree_order_ok)
  then
  have "h ⊢ a_get_dom_component (cast document_ptr) →⇩r to"
    using root
    by(auto simp add: a_get_dom_component_def)
  moreover
  obtain to' where to': "h' ⊢ to_tree_order (cast document_ptr) →⇩r to'"
    by (meson ‹heap_is_wellformed h'› ‹known_ptrs h'› ‹type_wf h'› is_OK_returns_result_E
        local.get_root_node_root_in_heap local.to_tree_order_ok root')
  then
  have "h' ⊢ a_get_dom_component (cast document_ptr) →⇩r to'"
    using root'
    by(auto simp add: a_get_dom_component_def)
  moreover
  have "⋀child. child ∈ set to ⟷ child ∈ set to'"
    by (metis ‹heap_is_wellformed h'› ‹known_ptrs h'› ‹parent_child_rel h = parent_child_rel h'›
        ‹type_wf h'› assms(1) assms(2) assms(3) local.to_tree_order_parent_child_rel to to')
  ultimately
  have "set |h ⊢ local.a_get_dom_component (cast document_ptr)|⇩r =
set |h' ⊢ local.a_get_dom_component (cast document_ptr)|⇩r"
    by(auto simp add: a_get_dom_component_def)

  show ?thesis
    apply(auto simp add: is_weakly_dom_component_safe_def Let_def)[1]
    using ‹h2 ⊢ get_child_nodes (cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr) →⇩r []› assms(2) assms(3)
      children_eq_h local.get_child_nodes_ok local.get_child_nodes_ptr_in_heap local.known_ptrs_known_ptr
      object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 returns_result_select_result
       apply (metis is_OK_returns_result_I)
      apply (metis ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr› assms(4)
        element_ptr_kinds_commutes h2 new_element_ptr new_element_ptr_in_heap node_ptr_kinds_eq_h2
        node_ptr_kinds_eq_h3 returns_result_eq returns_result_heap_def)
    using ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r result |∉| object_ptr_kinds h› element_ptr_kinds_commutes
      node_ptr_kinds_commutes apply blast
    using assms(1) assms(2) assms(3) ‹h ⊢ create_element document_ptr tag →⇩h h'›
    apply(rule create_element_is_weakly_dom_component_safe_step)
     apply (simp add: local.get_dom_component_impl)
    using ‹cast⇩e⇩l⇩e⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_element_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r›
      ‹h ⊢ create_element document_ptr tag →⇩r new_element_ptr›
    by auto

qed
end

interpretation i_get_dom_component_create_element?: l_get_dom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component is_strongly_dom_component_safe
  is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors get_ancestors_locs
  get_element_by_id get_elements_by_class_name get_elements_by_tag_name get_disconnected_nodes
  get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_name
  set_tag_name_locs create_element
  by(auto simp add: l_get_dom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_create_element⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]



subsubsection ‹create\_character\_data›

lemma create_character_data_not_strongly_dom_component_safe:
  obtains
    h :: "('object_ptr::{equal,linorder}, 'node_ptr::{equal,linorder},
'element_ptr::{equal,linorder}, 'character_data_ptr::{equal,linorder},
'document_ptr::{equal,linorder}, 'shadow_root_ptr::{equal,linorder},
'Object::{equal,linorder}, 'Node::{equal,linorder}, 'Element::{equal,linorder},
'CharacterData::{equal,linorder}, 'Document::{equal,linorder}) heap" and
    h' and document_ptr and create_character_datanew_character_data_ptr and tag where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h ⊢ create_character_data document_ptr tag →⇩r create_character_datanew_character_data_ptr →⇩h h'" and
    "¬ is_strongly_dom_component_safe {cast document_ptr} {cast create_character_datanew_character_data_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}) heap"
  let ?P = "create_document"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?document_ptr = "|?h0 ⊢ ?P|⇩r"

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

locale l_get_dom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component_safe is_weakly_dom_component_safe get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_disconnected_nodes get_disconnected_nodes_locs
  get_element_by_id get_elements_by_class_name get_elements_by_tag_name +
  l_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
  set_disconnected_nodes_locs set_val set_val_locs type_wf create_character_data known_ptr +
  l_get_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_disconnected_nodes set_disconnected_nodes_locs +
  l_set_val⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M type_wf set_val set_val_locs +
  l_create_character_data_wf⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M known_ptr type_wf get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs heap_is_wellformed parent_child_rel set_val
  set_val_locs set_disconnected_nodes set_disconnected_nodes_locs
  create_character_data known_ptrs
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and type_wf :: "(_) heap ⇒ bool"
    and known_ptrs :: "(_) heap ⇒ bool"
    and to_tree_order :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_dom_component :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and is_strongly_dom_component_safe :: "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and is_weakly_dom_component_safe :: "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and get_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_ancestors :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_ancestors_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_element_by_id :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr option) prog"
    and get_elements_by_class_name :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and get_elements_by_tag_name :: "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and set_val :: "(_) character_data_ptr ⇒ char list ⇒ ((_) heap, exception, unit) prog"
    and set_val_locs :: "(_) character_data_ptr ⇒ ((_) heap, exception, unit) prog set"
    and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and set_disconnected_nodes :: "(_) document_ptr ⇒ (_) node_ptr list ⇒ ((_) heap, exception, unit) prog"
    and set_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap, exception, unit) prog set"
    and create_character_data :: "(_) document_ptr ⇒ char list ⇒ ((_) heap, exception, (_) character_data_ptr) prog"
begin

lemma create_character_data_is_weakly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_character_data document_ptr text →⇩h h'"
  assumes "ptr ∉ set |h ⊢ get_dom_component (cast document_ptr)|⇩r"
  assumes "ptr ≠ cast |h ⊢ create_character_data document_ptr text|⇩r"
  shows "preserved (get_M ptr getter) h h'"
proof -
  obtain new_character_data_ptr h2 h3 disc_nodes where
    new_character_data_ptr: "h ⊢ new_character_data →⇩r new_character_data_ptr" and
    h2: "h ⊢ new_character_data →⇩h h2" and
    h3: "h2 ⊢ set_val new_character_data_ptr text →⇩h h3" and
    disc_nodes: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes" and
    h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_character_data_ptr # disc_nodes) →⇩h h'"
    using assms(4)
    by(auto simp add: create_character_data_def elim!: bind_returns_heap_E
        bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated])

  have "h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr"
    using new_character_data_ptr h2 h3 disc_nodes h'
    apply(auto simp add: create_character_data_def intro!: bind_returns_result_I
        bind_pure_returns_result_I[OF get_disconnected_nodes_pure])[1]
     apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
    by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
  have "preserved (get_M ptr getter) h h2"
    using h2 new_character_data_ptr
    apply(rule new_character_data_get_M⇩O⇩b⇩j⇩e⇩c⇩t)
    using new_character_data_ptr assms(6)
      ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr›
    by simp

  have "preserved (get_M ptr getter) h2 h3"
    using set_val_writes h3
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_val_locs_impl a_set_val_locs_def all_args_def)[1]
    by (metis (mono_tags) CharacterData_simp11
        ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr› assms(4) assms(6)
        is_OK_returns_heap_I is_OK_returns_result_E returns_result_eq select_result_I2)

  have "document_ptr |∈| document_ptr_kinds h"
    using create_character_data_document_in_heap
    using assms(4)
    by blast
  then
  have "ptr ≠ (cast document_ptr)"
    using assms(5) assms(1) assms(2) assms(3) local.get_dom_component_ok local.get_dom_component_ptr
    by auto
  have "preserved (get_M ptr getter) h3 h'"
    using set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved2)
    apply(auto simp add: set_disconnected_nodes_locs_def all_args_def)[1]
    by (metis ‹ptr ≠ cast⇩d⇩o⇩c⇩u⇩m⇩e⇩n⇩t⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r document_ptr› get_M_Mdocument_preserved3)

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

lemma create_character_data_is_weakly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_character_data document_ptr text →⇩r result"
  assumes "h ⊢ create_character_data document_ptr text →⇩h h'"
  shows "is_weakly_dom_component_safe {cast document_ptr} {cast result} h h'"
proof -


  obtain new_character_data_ptr h2 h3 disc_nodes_h3 where
    new_character_data_ptr: "h ⊢ new_character_data →⇩r new_character_data_ptr" and
    h2: "h ⊢ new_character_data →⇩h h2" and
    h3: "h2 ⊢ set_val new_character_data_ptr text →⇩h h3" and
    disc_nodes_h3: "h3 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3" and
    h': "h3 ⊢ set_disconnected_nodes document_ptr (cast new_character_data_ptr # disc_nodes_h3) →⇩h h'"
    using assms(5)
    by(auto simp add: create_character_data_def
        elim!: bind_returns_heap_E
        bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )
  then
  have "h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr"
    apply(auto simp add: create_character_data_def intro!: bind_returns_result_I)[1]
      apply (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)
     apply (metis is_OK_returns_heap_E is_OK_returns_result_I local.get_disconnected_nodes_pure
        pure_returns_heap_eq)
    by (metis is_OK_returns_heap_I is_OK_returns_result_E old.unit.exhaust)

  have "new_character_data_ptr ∉ set |h ⊢ character_data_ptr_kinds_M|⇩r"
    using new_character_data_ptr CharacterDataMonad.ptr_kinds_ptr_kinds_M h2
    using new_character_data_ptr_not_in_heap by blast
  then have "cast new_character_data_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r"
    by simp
  then have "cast new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r"
    by simp



  have object_ptr_kinds_eq_h:
    "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
    using new_character_data_new_ptr h2 new_character_data_ptr by blast
  then have node_ptr_kinds_eq_h:
    "node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
    apply(simp add: node_ptr_kinds_def)
    by force
  then have character_data_ptr_kinds_eq_h:
    "character_data_ptr_kinds h2 = character_data_ptr_kinds h |∪| {|new_character_data_ptr|}"
    apply(simp add: character_data_ptr_kinds_def)
    by force
  have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: node_ptr_kinds_def element_ptr_kinds_def)
  have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: document_ptr_kinds_def)

  have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_val_writes h3])
    using set_val_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
    using object_ptr_kinds_eq_h2
    by(auto simp add: node_ptr_kinds_def)

  have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_disconnected_nodes_writes h'])
    using set_disconnected_nodes_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
    using object_ptr_kinds_eq_h3
    by(auto simp add: node_ptr_kinds_def)


  have "document_ptr |∈| document_ptr_kinds h"
    using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
      get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
    by (metis is_OK_returns_result_I)

  have children_eq_h: "⋀(ptr'::(_) object_ptr) children. ptr' ≠ cast new_character_data_ptr
                  ⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads h2 get_child_nodes_new_character_data[rotated, OF new_character_data_ptr h2]
    apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
    by blast+
  then have children_eq2_h:
    "⋀ptr'. ptr' ≠ cast new_character_data_ptr
      ⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force
  have object_ptr_kinds_eq_h:
    "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
    using new_character_data_new_ptr h2 new_character_data_ptr by blast
  then have node_ptr_kinds_eq_h:
    "node_ptr_kinds h2 = node_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
    apply(simp add: node_ptr_kinds_def)
    by force
  then have character_data_ptr_kinds_eq_h:
    "character_data_ptr_kinds h2 = character_data_ptr_kinds h |∪| {|new_character_data_ptr|}"
    apply(simp add: character_data_ptr_kinds_def)
    by force
  have element_ptr_kinds_eq_h: "element_ptr_kinds h2 = element_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: node_ptr_kinds_def element_ptr_kinds_def)
  have document_ptr_kinds_eq_h: "document_ptr_kinds h2 = document_ptr_kinds h"
    using object_ptr_kinds_eq_h
    by(auto simp add: document_ptr_kinds_def)

  have object_ptr_kinds_eq_h2: "object_ptr_kinds h3 = object_ptr_kinds h2"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_val_writes h3])
    using set_val_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h2: "document_ptr_kinds h3 = document_ptr_kinds h2"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h2: "node_ptr_kinds h3 = node_ptr_kinds h2"
    using object_ptr_kinds_eq_h2
    by(auto simp add: node_ptr_kinds_def)

  have object_ptr_kinds_eq_h3: "object_ptr_kinds h' = object_ptr_kinds h3"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h' = object_ptr_kinds h",
          OF set_disconnected_nodes_writes h'])
    using set_disconnected_nodes_pointers_preserved
    by (auto simp add: reflp_def transp_def)
  then have document_ptr_kinds_eq_h3: "document_ptr_kinds h' = document_ptr_kinds h3"
    by (auto simp add: document_ptr_kinds_def)
  have node_ptr_kinds_eq_h3: "node_ptr_kinds h' = node_ptr_kinds h3"
    using object_ptr_kinds_eq_h3
    by(auto simp add: node_ptr_kinds_def)


  have "document_ptr |∈| document_ptr_kinds h"
    using disc_nodes_h3 document_ptr_kinds_eq_h object_ptr_kinds_eq_h2
      get_disconnected_nodes_ptr_in_heap ‹type_wf h› document_ptr_kinds_def
    by (metis is_OK_returns_result_I)

  have children_eq_h: "⋀(ptr'::(_) object_ptr) children. ptr' ≠ cast new_character_data_ptr
                ⟹ h ⊢ get_child_nodes ptr' →⇩r children = h2 ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads h2 get_child_nodes_new_character_data[rotated, OF new_character_data_ptr h2]
    apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
    by blast+
  then have children_eq2_h: "⋀ptr'. ptr' ≠ cast new_character_data_ptr
                                 ⟹ |h ⊢ get_child_nodes ptr'|⇩r = |h2 ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force

  have "h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []"
    using new_character_data_ptr h2 new_character_data_ptr_in_heap[OF h2 new_character_data_ptr]
      new_character_data_is_character_data_ptr[OF new_character_data_ptr]
      new_character_data_no_child_nodes
    by blast
  have disconnected_nodes_eq_h:
    "⋀doc_ptr disc_nodes. h ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                                             = h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads h2
      get_disconnected_nodes_new_character_data[OF new_character_data_ptr h2]
    apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
    by blast+
  then have disconnected_nodes_eq2_h:
    "⋀doc_ptr. |h ⊢ get_disconnected_nodes doc_ptr|⇩r = |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have children_eq_h2:
    "⋀ptr' children. h2 ⊢ get_child_nodes ptr' →⇩r children = h3 ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads set_val_writes h3
    apply(rule reads_writes_preserved)
    by(auto simp add: set_val_get_child_nodes)
  then have children_eq2_h2:
    "⋀ptr'. |h2 ⊢ get_child_nodes ptr'|⇩r = |h3 ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force
  have disconnected_nodes_eq_h2:
    "⋀doc_ptr disc_nodes. h2 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                                              = h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads set_val_writes h3
    apply(rule reads_writes_preserved)
    by(auto simp add: set_val_get_disconnected_nodes)
  then have disconnected_nodes_eq2_h2:
    "⋀doc_ptr. |h2 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have "type_wf h2"
    using ‹type_wf h› new_character_data_types_preserved h2 by blast
  then have "type_wf h3"
    using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_val_writes h3]
    using  set_val_types_preserved
    by(auto simp add: reflp_def transp_def)
  then have "type_wf h'"
    using writes_small_big[where P="λh h'. type_wf h ⟶ type_wf h'", OF set_disconnected_nodes_writes h']
    using  set_disconnected_nodes_types_preserved
    by(auto simp add: reflp_def transp_def)

  have children_eq_h3:
    "⋀ptr' children. h3 ⊢ get_child_nodes ptr' →⇩r children = h' ⊢ get_child_nodes ptr' →⇩r children"
    using get_child_nodes_reads set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved)
    by(auto simp add: set_disconnected_nodes_get_child_nodes)
  then have children_eq2_h3:
    " ⋀ptr'. |h3 ⊢ get_child_nodes ptr'|⇩r = |h' ⊢ get_child_nodes ptr'|⇩r"
    using select_result_eq by force
  have disconnected_nodes_eq_h3: "⋀doc_ptr disc_nodes. document_ptr ≠ doc_ptr
    ⟹ h3 ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes
                            = h' ⊢ get_disconnected_nodes doc_ptr →⇩r disc_nodes"
    using get_disconnected_nodes_reads set_disconnected_nodes_writes h'
    apply(rule reads_writes_preserved)
    by(auto simp add: set_disconnected_nodes_get_disconnected_nodes_different_pointers)
  then have disconnected_nodes_eq2_h3: "⋀doc_ptr. document_ptr ≠ doc_ptr
             ⟹ |h3 ⊢ get_disconnected_nodes doc_ptr|⇩r = |h' ⊢ get_disconnected_nodes doc_ptr|⇩r"
    using select_result_eq by force

  have disc_nodes_document_ptr_h2: "h2 ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
    using disconnected_nodes_eq_h2 disc_nodes_h3 by auto
  then have disc_nodes_document_ptr_h: "h ⊢ get_disconnected_nodes document_ptr →⇩r disc_nodes_h3"
    using disconnected_nodes_eq_h by auto
  then have "cast new_character_data_ptr ∉ set disc_nodes_h3"
    using ‹heap_is_wellformed h› using ‹cast new_character_data_ptr ∉ set |h ⊢ node_ptr_kinds_M|⇩r›
      a_all_ptrs_in_heap_def heap_is_wellformed_def
    using NodeMonad.ptr_kinds_ptr_kinds_M local.heap_is_wellformed_disc_nodes_in_heap by blast

  have "parent_child_rel h = parent_child_rel h'"
  proof -
    have "parent_child_rel h = parent_child_rel h2"
    proof(auto simp add: parent_child_rel_def)[1]
      fix a x
      assume 0: "a |∈| object_ptr_kinds h"
        and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
      then show "a |∈| object_ptr_kinds h2"
        by (simp add: object_ptr_kinds_eq_h)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h"
        and 1: "x ∈ set |h ⊢ get_child_nodes a|⇩r"
      then show "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
        by (metis ObjectMonad.ptr_kinds_ptr_kinds_M
            ‹cast new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r› children_eq2_h)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h2"
        and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
      then show "a |∈| object_ptr_kinds h"
        using object_ptr_kinds_eq_h ‹h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›
        by(auto)
    next
      fix a x
      assume 0: "a |∈| object_ptr_kinds h2"
        and 1: "x ∈ set |h2 ⊢ get_child_nodes a|⇩r"
      then show "x ∈ set |h ⊢ get_child_nodes a|⇩r"
        by (metis (no_types, lifting) ‹h2 ⊢ get_child_nodes (cast new_character_data_ptr) →⇩r []›
            children_eq2_h empty_iff empty_set image_eqI select_result_I2)
    qed
    also have "… = parent_child_rel h3"
      by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h2 children_eq2_h2)
    also have "… = parent_child_rel h'"
      by(auto simp add: parent_child_rel_def object_ptr_kinds_eq_h3 children_eq2_h3)
    finally show ?thesis
      by simp
  qed
  have root: "h ⊢ get_root_node (cast document_ptr) →⇩r cast document_ptr"
    by (simp add: ‹document_ptr |∈| document_ptr_kinds h› local.get_root_node_not_node_same)
  then
  have root': "h' ⊢ get_root_node (cast document_ptr) →⇩r cast document_ptr"
    by (simp add: ‹document_ptr |∈| document_ptr_kinds h› document_ptr_kinds_eq_h
        local.get_root_node_not_node_same object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3)


  have "heap_is_wellformed h'" and "known_ptrs h'"
    using create_character_data_preserves_wellformedness assms
    by blast+

  have "cast result |∉| object_ptr_kinds h"
    using ‹cast new_character_data_ptr ∉ set |h ⊢ object_ptr_kinds_M|⇩r›
    by (metis (full_types) ObjectMonad.ptr_kinds_ptr_kinds_M
        ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr› assms(4) returns_result_eq)

  obtain to where to: "h ⊢ to_tree_order (cast document_ptr) →⇩r to"
    by (meson ‹document_ptr |∈| document_ptr_kinds h› assms(1) assms(2) assms(3)
        document_ptr_kinds_commutes is_OK_returns_result_E local.to_tree_order_ok)
  then
  have "h ⊢ a_get_dom_component (cast document_ptr) →⇩r to"
    using root
    by(auto simp add: a_get_dom_component_def)
  moreover
  obtain to' where to': "h' ⊢ to_tree_order (cast document_ptr) →⇩r to'"
    by (meson ‹heap_is_wellformed h'› ‹known_ptrs h'› ‹type_wf h'› is_OK_returns_result_E
        local.get_root_node_root_in_heap local.to_tree_order_ok root')
  then
  have "h' ⊢ a_get_dom_component (cast document_ptr) →⇩r to'"
    using root'
    by(auto simp add: a_get_dom_component_def)
  moreover
  have "⋀child. child ∈ set to ⟷ child ∈ set to'"
    by (metis ‹heap_is_wellformed h'› ‹known_ptrs h'› ‹parent_child_rel h = parent_child_rel h'›
        ‹type_wf h'› assms(1) assms(2) assms(3) local.to_tree_order_parent_child_rel to to')
  ultimately
  have "set |h ⊢ local.a_get_dom_component (cast document_ptr)|⇩r =
set |h' ⊢ local.a_get_dom_component (cast document_ptr)|⇩r"
    by(auto simp add: a_get_dom_component_def)

  show ?thesis
    apply(auto simp add: is_weakly_dom_component_safe_def Let_def)[1]
    using  assms(2) assms(3) children_eq_h local.get_child_nodes_ok
      local.get_child_nodes_ptr_in_heap local.known_ptrs_known_ptr object_ptr_kinds_eq_h2
      object_ptr_kinds_eq_h3 returns_result_select_result
       apply (metis ‹h2 ⊢ get_child_nodes (cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_character_data_ptr) →⇩r []›
        is_OK_returns_result_I)

      apply (metis ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr› assms(4)
        character_data_ptr_kinds_commutes h2 new_character_data_ptr new_character_data_ptr_in_heap
        node_ptr_kinds_eq_h2 node_ptr_kinds_eq_h3 returns_result_eq)
    using ‹h ⊢ create_character_data document_ptr text →⇩r new_character_data_ptr›
      ‹new_character_data_ptr ∉ set |h ⊢ character_data_ptr_kinds_M|⇩r› assms(4) returns_result_eq
     apply fastforce
    using  assms(2) assms(3) children_eq_h local.get_child_nodes_ok local.get_child_nodes_ptr_in_heap
      local.known_ptrs_known_ptr object_ptr_kinds_eq_h2 object_ptr_kinds_eq_h3 returns_result_select_result
    apply (smt (verit, best) ObjectMonad.ptr_kinds_ptr_kinds_M
            ‹cast⇩c⇩h⇩a⇩r⇩a⇩c⇩t⇩e⇩r⇩_⇩d⇩a⇩t⇩a⇩_⇩p⇩t⇩r⇩2⇩o⇩b⇩j⇩e⇩c⇩t⇩_⇩p⇩t⇩r new_character_data_ptr ∉ set |h
              ⊢ object_ptr_kinds_M|⇩r› ‹h ⊢ create_character_data document_ptr text →⇩r
              new_character_data_ptr› assms(1) assms(5)
            create_character_data_is_weakly_dom_component_safe_step local.a_get_dom_component_def
            local.get_dom_component_def select_result_I2)
    done
qed

end

interpretation i_get_dom_component_create_character_data?: l_get_dom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component is_strongly_dom_component_safe
  is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors get_ancestors_locs
  get_element_by_id get_elements_by_class_name get_elements_by_tag_name set_val set_val_locs
  get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
  create_character_data
  by(auto simp add: l_get_dom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_create_character_data⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹create\_document›

lemma create_document_unsafe: "¬(∀(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}) heap
  ) h' new_document_ptr. heap_is_wellformed h ⟶ type_wf h ⟶ known_ptrs h ⟶
h ⊢ create_document →⇩r new_document_ptr ⟶ h ⊢ create_document →⇩h h' ⟶
is_strongly_dom_component_safe {} {cast new_document_ptr} h h')"
proof -
  obtain h document_ptr where h: "Inr (document_ptr, h) = (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}) heap
    ) ⊢ (do {
      document_ptr ← create_document;
      return (document_ptr)
  })"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then obtain h' new_document_ptr where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    h': "h ⊢ create_document →⇩r new_document_ptr" and
    h': "h ⊢ create_document →⇩h h'" and
    "¬(is_strongly_dom_component_safe {} {cast new_document_ptr} h h')"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then show ?thesis
    by blast
qed

locale l_get_dom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M =
  l_get_dom_component⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component_safe is_weakly_dom_component_safe get_root_node get_root_node_locs
  get_ancestors get_ancestors_locs get_disconnected_nodes get_disconnected_nodes_locs get_element_by_id
  get_elements_by_class_name get_elements_by_tag_name +
  l_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M create_document
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and type_wf :: "(_) heap ⇒ bool"
    and known_ptrs :: "(_) heap ⇒ bool"
    and to_tree_order :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_dom_component :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and is_strongly_dom_component_safe ::
    "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and is_weakly_dom_component_safe ::
    "(_) object_ptr set ⇒ (_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
    and get_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_ancestors :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr list) prog"
    and get_ancestors_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_element_by_id ::
    "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr option) prog"
    and get_elements_by_class_name ::
    "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and get_elements_by_tag_name ::
    "(_) object_ptr ⇒ char list ⇒ ((_) heap, exception, (_) element_ptr list) prog"
    and create_document :: "((_) heap, exception, (_) document_ptr) prog"
begin

lemma create_document_is_weakly_dom_component_safe_step:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_document →⇩h h'"
  assumes "ptr ≠ cast |h ⊢ create_document|⇩r"
  shows "preserved (get_M⇩O⇩b⇩j⇩e⇩c⇩t ptr getter) h h'"
  using assms
  apply(auto simp add: create_document_def)[1]
  by (metis assms(4) assms(5) is_OK_returns_heap_I local.create_document_def new_document_get_M⇩O⇩b⇩j⇩e⇩c⇩t
      select_result_I)

lemma create_document_is_weakly_dom_component_safe:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ create_document →⇩r result"
  assumes "h ⊢ create_document →⇩h h'"
  shows "is_weakly_dom_component_safe {} {cast result} h h'"
proof -
  have "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast result|}"
    using assms(4) assms(5) local.create_document_def new_document_new_ptr by auto
  moreover have "result |∉| document_ptr_kinds h"
    using assms(4) assms(5) local.create_document_def new_document_ptr_not_in_heap by auto
  ultimately show ?thesis
    using assms
    apply(auto simp add: is_weakly_dom_component_safe_def Let_def local.create_document_def
        new_document_ptr_not_in_heap)[1]
    by (metis ‹result |∉| document_ptr_kinds h› document_ptr_kinds_commutes new_document_get_M⇩O⇩b⇩j⇩e⇩c⇩t)
qed
end

interpretation i_get_dom_component_create_document?: l_get_dom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩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_dom_component is_strongly_dom_component_safe
  is_weakly_dom_component_safe get_root_node get_root_node_locs get_ancestors get_ancestors_locs
  get_element_by_id get_elements_by_class_name get_elements_by_tag_name create_document
  by(auto simp add: l_get_dom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_def instances)
declare l_get_dom_component_create_document⇩C⇩o⇩r⇩e⇩_⇩D⇩O⇩M_axioms [instances]


subsubsection ‹insert\_before›

lemma insert_before_unsafe: "¬(∀(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}) heap
  ) h' ptr child. heap_is_wellformed h ⟶ type_wf h ⟶ known_ptrs h ⟶
h ⊢ insert_before ptr child None →⇩h h' ⟶ is_weakly_dom_component_safe {ptr, cast child} {} h h')"
proof -
  obtain h document_ptr e1 e2 where h: "Inr ((document_ptr, e1, e2), h) = (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}) heap
    ) ⊢ (do {
      document_ptr ← create_document;
      e1 ← create_element document_ptr ''div'';
      e2 ← create_element document_ptr ''div'';
      return (document_ptr, e1, e2)
  })"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then obtain h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    h': "h ⊢ insert_before (cast e1) (cast e2) None →⇩h h'" and
    "¬(is_weakly_dom_component_safe {cast e1, cast e2} {} h h')"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then show ?thesis
    by auto
qed

lemma insert_before_unsafe2: "¬(∀(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}) heap
  ) h' ptr child ref. heap_is_wellformed h ⟶ type_wf h ⟶ known_ptrs h ⟶
h ⊢ insert_before ptr child (Some ref) →⇩h h' ⟶
is_weakly_dom_component_safe {ptr, cast child, cast ref} {} h h')"
proof -
  obtain h document_ptr e1 e2 e3 where h: "Inr ((document_ptr, e1, e2, e3), h) = (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}) heap
    ) ⊢ (do {
      document_ptr ← create_document;
      e1 ← create_element document_ptr ''div'';
      e2 ← create_element document_ptr ''div'';
      e3 ← create_element document_ptr ''div'';
      append_child (cast e1) (cast e2);
      return (document_ptr, e1, e2, e3)
  })"
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then obtain h' where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    h': "h ⊢ insert_before (cast e1) (cast e3) (Some (cast e2)) →⇩h h'" and
    "¬(is_weakly_dom_component_safe {cast e1, cast e3, cast e2} {} h h')"
    apply(code_simp)
    apply(clarify)
    by(code_simp, auto simp add: equal_eq List.member_def)+
  then show ?thesis
    by fast
qed


lemma append_child_unsafe:
  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}) heap" and
    h' and ptr and child where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h ⊢ append_child ptr child →⇩h h'" and
    "¬ is_weakly_dom_component_safe {ptr, cast child} {} 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}) heap"
  let ?P = "do {
      document_ptr ← create_document;
      e1 ← create_element document_ptr ''div'';
      e2 ← create_element document_ptr ''div'';
      return (e1, e2)
  }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?e1 = "fst |?h0 ⊢ ?P|⇩r"
  let ?e2 = "snd |?h0 ⊢ ?P|⇩r"

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


subsubsection ‹get\_owner\_document›

lemma get_owner_document_unsafe:
  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}) heap" and
    h' and ptr and owner_document where
    "heap_is_wellformed h" and "type_wf h" and "known_ptrs h" and
    "h ⊢ get_owner_document ptr →⇩r owner_document →⇩h h'" and
    "¬is_weakly_dom_component_safe {ptr} {cast owner_document} 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}) heap"
  let ?P = "do {
      document_ptr ← create_document;
      e1 ← create_element document_ptr ''div'';
      return (document_ptr, e1)
  }"
  let ?h1 = "|?h0 ⊢ ?P|⇩h"
  let ?document_ptr = "fst |?h0 ⊢ ?P|⇩r"
  let ?e1 = "snd |?h0 ⊢ ?P|⇩r"

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

end