Theory Core_DOM_Heap_WF

(***********************************************************************************
 * Copyright (c) 2016-2018 The University of Sheffield, 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‹Wellformedness›
text‹In this theory, we discuss the wellformedness of the DOM. First, we define
wellformedness and, second, we show for all functions for querying and modifying the
DOM to what extend they preserve wellformendess.›

theory Core_DOM_Heap_WF
  imports
    "Core_DOM_Functions"
begin

locale l_heap_is_wellformedCore_DOM_defs =
  l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs
  for get_child_nodes :: "(_::linorder) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
definition a_owner_document_valid :: "(_) heap ⇒ bool"
  where
    "a_owner_document_valid h ⟷ (∀node_ptr ∈ fset (node_ptr_kinds h).
      ((∃document_ptr. document_ptr |∈| document_ptr_kinds h
         ∧ node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|r)
    ∨ (∃parent_ptr. parent_ptr |∈| object_ptr_kinds h
            ∧ node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|r)))"

lemma a_owner_document_valid_code [code]: "a_owner_document_valid h ⟷ node_ptr_kinds h |⊆|
  fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|r)
(sorted_list_of_fset (object_ptr_kinds h)) @ map (λparent. |h ⊢ get_disconnected_nodes parent|r)
(sorted_list_of_fset (document_ptr_kinds h))))
"
  apply(auto simp add: a_owner_document_valid_def
      l_heap_is_wellformedCore_DOM_defs.a_owner_document_valid_def)[1]
proof -
  fix x
  assume 1: " ∀node_ptr∈fset (node_ptr_kinds h).
            (∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|r) ∨
            (∃parent_ptr. parent_ptr |∈| object_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|r)"
  assume 2: "x |∈| node_ptr_kinds h"
  assume 3: "x |∉| fset_of_list (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|r)
(sorted_list_of_fset (document_ptr_kinds h))))"
  have "¬(∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
x ∈ set |h ⊢ get_disconnected_nodes document_ptr|r)"
    using 1 2 3
    by (smt (verit) UN_I fset_of_list_elem image_eqI set_concat set_map sorted_list_of_fset_simps(1))
  then
  have "(∃parent_ptr. parent_ptr |∈| object_ptr_kinds h ∧ x ∈ set |h ⊢ get_child_nodes parent_ptr|r)"
    using 1 2
    by auto
  then obtain parent_ptr where parent_ptr:
    "parent_ptr |∈| object_ptr_kinds h ∧ x ∈ set |h ⊢ get_child_nodes parent_ptr|r"
    by auto
  moreover have "parent_ptr ∈ set (sorted_list_of_fset (object_ptr_kinds h))"
    using parent_ptr by auto
  moreover have "|h ⊢ get_child_nodes parent_ptr|r ∈ set (map (λparent. |h ⊢ get_child_nodes parent|r)
(sorted_list_of_fset (object_ptr_kinds h)))"
    using calculation(2) by auto
  ultimately
  show "x |∈| fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|r)
(sorted_list_of_fset (object_ptr_kinds h))))"
    using fset_of_list_elem by fastforce
next
  fix node_ptr
  assume 1: "node_ptr_kinds h |⊆| fset_of_list (concat (map (λparent. |h ⊢ get_child_nodes parent|r)
(sorted_list_of_fset (object_ptr_kinds h)))) |∪|
fset_of_list (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|r)
(sorted_list_of_fset (document_ptr_kinds h))))"
  assume 2: "node_ptr |∈| node_ptr_kinds h"
  assume 3: "∀parent_ptr. parent_ptr |∈| object_ptr_kinds h ⟶
node_ptr ∉ set |h ⊢ get_child_nodes parent_ptr|r"
  have "node_ptr ∈ set (concat (map (λparent. |h ⊢ get_child_nodes parent|r)
(sorted_list_of_fset (object_ptr_kinds h)))) ∨
node_ptr ∈ set (concat (map (λparent. |h ⊢ get_disconnected_nodes parent|r)
(sorted_list_of_fset (document_ptr_kinds h))))"
    using 1 2
    by (meson fin_mono fset_of_list_elem funion_iff)
  then
  show "∃document_ptr. document_ptr |∈| document_ptr_kinds h ∧
node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|r"
    using 3
    by auto
qed

definition a_parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
  where
    "a_parent_child_rel h = {(parent, child). parent |∈| object_ptr_kinds h
                            ∧ child ∈ cast ` set |h ⊢ get_child_nodes parent|r}"

lemma a_parent_child_rel_code [code]: "a_parent_child_rel h = set (concat (map
  (λparent. map
    (λchild. (parent, castnode_ptr2object_ptr child))
    |h ⊢ get_child_nodes parent|r)
  (sorted_list_of_fset (object_ptr_kinds h)))
)"
  by(auto simp add: a_parent_child_rel_def)

definition a_acyclic_heap :: "(_) heap ⇒ bool"
  where
    "a_acyclic_heap h = acyclic (a_parent_child_rel h)"

definition a_all_ptrs_in_heap :: "(_) heap ⇒ bool"
  where
    "a_all_ptrs_in_heap h ⟷
      (∀ptr ∈ fset (object_ptr_kinds h). set |h ⊢ get_child_nodes ptr|r ⊆ fset (node_ptr_kinds h)) ∧
      (∀document_ptr ∈ fset (document_ptr_kinds h).
set |h ⊢ get_disconnected_nodes document_ptr|r ⊆ fset (node_ptr_kinds h))"

definition a_distinct_lists :: "(_) heap ⇒ bool"
  where
    "a_distinct_lists h = distinct (concat (
      (map (λptr. |h ⊢ get_child_nodes ptr|r) |h ⊢ object_ptr_kinds_M|r)
   @ (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|r) |h ⊢ document_ptr_kinds_M|r)
    ))"

definition a_heap_is_wellformed :: "(_) heap ⇒ bool"
  where
    "a_heap_is_wellformed h ⟷
      a_acyclic_heap h ∧ a_all_ptrs_in_heap h ∧ a_distinct_lists h ∧ a_owner_document_valid h"
end

locale l_heap_is_wellformed_defs =
  fixes heap_is_wellformed :: "(_) heap ⇒ bool"
  fixes parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"

global_interpretation l_heap_is_wellformedCore_DOM_defs get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs
  defines heap_is_wellformed = "l_heap_is_wellformedCore_DOM_defs.a_heap_is_wellformed get_child_nodes
                     get_disconnected_nodes"
    and parent_child_rel = "l_heap_is_wellformedCore_DOM_defs.a_parent_child_rel get_child_nodes"
    and acyclic_heap = a_acyclic_heap
    and all_ptrs_in_heap = a_all_ptrs_in_heap
    and distinct_lists = a_distinct_lists
    and owner_document_valid = a_owner_document_valid
  .

locale l_heap_is_wellformedCore_DOM =
  l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs
  + l_heap_is_wellformedCore_DOM_defs get_child_nodes get_child_nodes_locs get_disconnected_nodes
  get_disconnected_nodes_locs
  + l_heap_is_wellformed_defs heap_is_wellformed parent_child_rel
  + l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and type_wf :: "(_) heap ⇒ bool"
    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_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set" +
  assumes heap_is_wellformed_impl: "heap_is_wellformed = a_heap_is_wellformed"
  assumes parent_child_rel_impl: "parent_child_rel = a_parent_child_rel"
begin
lemmas heap_is_wellformed_def = heap_is_wellformed_impl[unfolded a_heap_is_wellformed_def]
lemmas parent_child_rel_def = parent_child_rel_impl[unfolded a_parent_child_rel_def]
lemmas acyclic_heap_def = a_acyclic_heap_def[folded parent_child_rel_impl]

lemma parent_child_rel_node_ptr:
  "(parent, child) ∈ parent_child_rel h ⟹ is_node_ptr_kind child"
  by(auto simp add: parent_child_rel_def)

lemma parent_child_rel_child_nodes:
  assumes "known_ptr parent"
    and "h ⊢ get_child_nodes parent →r children"
    and "child ∈ set children"
  shows "(parent, cast child) ∈ parent_child_rel h"
  using assms
  apply(auto simp add: parent_child_rel_def is_OK_returns_result_I )[1]
  using get_child_nodes_ptr_in_heap by blast

lemma parent_child_rel_child_nodes2:
  assumes "known_ptr parent"
    and "h ⊢ get_child_nodes parent →r children"
    and "child ∈ set children"
    and "castnode_ptr2object_ptr child = child_obj"
  shows "(parent, child_obj) ∈ parent_child_rel h"
  using assms parent_child_rel_child_nodes by blast


lemma parent_child_rel_finite: "finite (parent_child_rel h)"
proof -
  have "parent_child_rel h = (⋃ptr ∈ set |h ⊢ object_ptr_kinds_M|r.
                 (⋃child ∈ set |h ⊢ get_child_nodes ptr|r. {(ptr, cast child)}))"
    by(auto simp add: parent_child_rel_def)
  moreover have "finite (⋃ptr ∈ set |h ⊢ object_ptr_kinds_M|r.
                    (⋃child ∈ set |h ⊢ get_child_nodes ptr|r. {(ptr, castnode_ptr2object_ptr child)}))"
    by simp
  ultimately show ?thesis
    by simp
qed

lemma distinct_lists_no_parent:
  assumes "a_distinct_lists h"
  assumes "h ⊢ get_disconnected_nodes document_ptr →r disc_nodes"
  assumes "node_ptr ∈ set disc_nodes"
  shows "¬(∃parent_ptr. parent_ptr |∈| object_ptr_kinds h
                ∧ node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|r)"
  using assms
  apply(auto simp add: a_distinct_lists_def)[1]
proof -
  fix parent_ptr :: "(_) object_ptr"
  assume a1: "parent_ptr |∈| object_ptr_kinds h"
  assume a2: "(⋃x∈fset (object_ptr_kinds h).
              set |h ⊢ get_child_nodes x|r) ∩ (⋃x∈fset (document_ptr_kinds h).
                  set |h ⊢ get_disconnected_nodes x|r) = {}"
  assume a3: "h ⊢ get_disconnected_nodes document_ptr →r disc_nodes"
  assume a4: "node_ptr ∈ set disc_nodes"
  assume a5: "node_ptr ∈ set |h ⊢ get_child_nodes parent_ptr|r"
  have f6: "parent_ptr ∈ fset (object_ptr_kinds h)"
    using a1 by auto
  have f7: "document_ptr ∈ fset (document_ptr_kinds h)"
    using a3 by (meson get_disconnected_nodes_ptr_in_heap is_OK_returns_result_I)
  have "|h ⊢ get_disconnected_nodes document_ptr|r = disc_nodes"
    using a3 by simp
  then show False
    using f7 f6 a5 a4 a2 by blast
qed


lemma distinct_lists_disconnected_nodes:
  assumes "a_distinct_lists h"
    and "h ⊢ get_disconnected_nodes document_ptr →r disc_nodes"
  shows "distinct disc_nodes"
proof -
  have h1: "distinct (concat (map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|r)
                             |h ⊢ document_ptr_kinds_M|r))"
    using assms(1)
    by(simp add: a_distinct_lists_def)
  then show ?thesis
    using concat_map_all_distinct[OF h1] assms(2) is_OK_returns_result_I get_disconnected_nodes_ok
    by (metis (no_types, lifting) DocumentMonad.ptr_kinds_ptr_kinds_M
        l_get_disconnected_nodes.get_disconnected_nodes_ptr_in_heap
        l_get_disconnected_nodes_axioms select_result_I2)
qed

lemma distinct_lists_children:
  assumes "a_distinct_lists h"
    and "known_ptr ptr"
    and "h ⊢ get_child_nodes ptr →r children"
  shows "distinct children"
proof (cases "children = []", simp)
  assume "children ≠ []"
  have h1: "distinct (concat ((map (λptr. |h ⊢ get_child_nodes ptr|r) |h ⊢ object_ptr_kinds_M|r)))"
    using assms(1)
    by(simp add: a_distinct_lists_def)
  show ?thesis
    using concat_map_all_distinct[OF h1] assms(2) assms(3)
    by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M get_child_nodes_ptr_in_heap
        is_OK_returns_result_I select_result_I2)
qed

lemma heap_is_wellformed_children_in_heap:
  assumes "heap_is_wellformed h"
  assumes "h ⊢ get_child_nodes ptr →r children"
  assumes "child ∈ set children"
  shows "child |∈| node_ptr_kinds h"
  using assms
  apply(auto simp add: heap_is_wellformed_def a_all_ptrs_in_heap_def)[1]
  by (metis (no_types, opaque_lifting) is_OK_returns_result_I
      local.get_child_nodes_ptr_in_heap select_result_I2 subsetD)

lemma heap_is_wellformed_one_parent:
  assumes "heap_is_wellformed h"
  assumes "h ⊢ get_child_nodes ptr →r children"
  assumes "h ⊢ get_child_nodes ptr' →r children'"
  assumes "set children ∩ set children' ≠ {}"
  shows "ptr = ptr'"
  using assms
proof (auto simp add: heap_is_wellformed_def a_distinct_lists_def)[1]
  fix x :: "(_) node_ptr"
  assume a1: "ptr ≠ ptr'"
  assume a2: "h ⊢ get_child_nodes ptr →r children"
  assume a3: "h ⊢ get_child_nodes ptr' →r children'"
  assume a4: "distinct (concat (map (λptr. |h ⊢ get_child_nodes ptr|r)
                                     (sorted_list_of_set (fset (object_ptr_kinds h)))))"
  have f5: "|h ⊢ get_child_nodes ptr|r = children"
    using a2 by simp
  have "|h ⊢ get_child_nodes ptr'|r = children'"
    using a3 by (meson select_result_I2)
  then have "ptr ∉ set (sorted_list_of_set (fset (object_ptr_kinds h)))
          ∨ ptr' ∉ set (sorted_list_of_set (fset (object_ptr_kinds h)))
          ∨ set children ∩ set children' = {}"
    using f5 a4 a1 by (meson distinct_concat_map_E(1))
  then show False
    using a3 a2 by (metis (no_types) assms(4) finite_fset is_OK_returns_result_I
        local.get_child_nodes_ptr_in_heap set_sorted_list_of_set)
qed

lemma parent_child_rel_child:
  "h ⊢ get_child_nodes ptr →r children ⟹
child ∈ set children ⟷ (ptr, cast child) ∈ parent_child_rel h"
  by (simp add: is_OK_returns_result_I get_child_nodes_ptr_in_heap parent_child_rel_def)

lemma parent_child_rel_acyclic: "heap_is_wellformed h ⟹ acyclic (parent_child_rel h)"
  by (simp add: acyclic_heap_def local.heap_is_wellformed_def)

lemma heap_is_wellformed_disconnected_nodes_distinct:
  "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes ⟹
distinct disc_nodes"
  using distinct_lists_disconnected_nodes local.heap_is_wellformed_def by blast

lemma parent_child_rel_parent_in_heap:
  "(parent, child_ptr) ∈ parent_child_rel h ⟹ parent |∈| object_ptr_kinds h"
  using local.parent_child_rel_def by blast

lemma parent_child_rel_child_in_heap:
  "heap_is_wellformed h ⟹ type_wf h ⟹ known_ptr parent
    ⟹ (parent, child_ptr) ∈ parent_child_rel h ⟹ child_ptr |∈| object_ptr_kinds h"
  apply(auto simp add: heap_is_wellformed_def parent_child_rel_def a_all_ptrs_in_heap_def)[1]
  using get_child_nodes_ok
  by (meson subsetD)

lemma heap_is_wellformed_disc_nodes_in_heap:
  "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
   ⟹ node ∈ set disc_nodes ⟹ node |∈| node_ptr_kinds h"
  by (metis (no_types, opaque_lifting) is_OK_returns_result_I local.a_all_ptrs_in_heap_def
      local.get_disconnected_nodes_ptr_in_heap local.heap_is_wellformed_def select_result_I2 subsetD)

lemma heap_is_wellformed_one_disc_parent:
  "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
   ⟹ h ⊢ get_disconnected_nodes document_ptr' →r disc_nodes'
   ⟹ set disc_nodes ∩ set disc_nodes' ≠ {} ⟹ document_ptr = document_ptr'"
  using DocumentMonad.ptr_kinds_ptr_kinds_M concat_append distinct_append distinct_concat_map_E(1)
    is_OK_returns_result_I local.a_distinct_lists_def local.get_disconnected_nodes_ptr_in_heap
    local.heap_is_wellformed_def select_result_I2
proof -
  assume a1: "heap_is_wellformed h"
  assume a2: "h ⊢ get_disconnected_nodes document_ptr →r disc_nodes"
  assume a3: "h ⊢ get_disconnected_nodes document_ptr' →r disc_nodes'"
  assume a4: "set disc_nodes ∩ set disc_nodes' ≠ {}"
  have f5: "|h ⊢ get_disconnected_nodes document_ptr|r = disc_nodes"
    using a2 by (meson select_result_I2)
  have f6: "|h ⊢ get_disconnected_nodes document_ptr'|r = disc_nodes'"
    using a3 by (meson select_result_I2)
  have "⋀nss nssa. ¬ distinct (concat (nss @ nssa)) ∨ distinct (concat nssa::(_) node_ptr list)"
    by (metis (no_types) concat_append distinct_append)
  then have "distinct (concat (map (λd. |h ⊢ get_disconnected_nodes d|r) |h ⊢ document_ptr_kinds_M|r))"
    using a1 local.a_distinct_lists_def local.heap_is_wellformed_def by blast
  then show ?thesis
    using f6 f5 a4 a3 a2 by (meson DocumentMonad.ptr_kinds_ptr_kinds_M distinct_concat_map_E(1)
        is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)
qed

lemma heap_is_wellformed_children_disc_nodes_different:
  "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children
    ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
   ⟹ set children ∩ set disc_nodes = {}"
  by (metis (no_types, opaque_lifting) disjoint_iff_not_equal distinct_lists_no_parent
      is_OK_returns_result_I local.get_child_nodes_ptr_in_heap
      local.heap_is_wellformed_def select_result_I2)

lemma heap_is_wellformed_children_disc_nodes:
  "heap_is_wellformed h ⟹ node_ptr |∈| node_ptr_kinds h
   ⟹  ¬(∃parent ∈ fset (object_ptr_kinds h). node_ptr ∈ set |h ⊢ get_child_nodes parent|r)
   ⟹ (∃document_ptr ∈ fset (document_ptr_kinds h). node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|r)"
  by (auto simp add: heap_is_wellformed_def a_distinct_lists_def a_owner_document_valid_def)

lemma heap_is_wellformed_children_distinct:
  "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children ⟹ distinct children"
  by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M concat_append distinct_append
      distinct_concat_map_E(2) is_OK_returns_result_I local.a_distinct_lists_def
      local.get_child_nodes_ptr_in_heap local.heap_is_wellformed_def
      select_result_I2)
end

locale l_heap_is_wellformed = l_type_wf + l_known_ptr + l_heap_is_wellformed_defs
  + l_get_child_nodes_defs + l_get_disconnected_nodes_defs +
  assumes heap_is_wellformed_children_in_heap:
    "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children ⟹ child ∈ set children
                        ⟹ child |∈| node_ptr_kinds h"
  assumes heap_is_wellformed_disc_nodes_in_heap:
    "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
                        ⟹ node ∈ set disc_nodes ⟹ node |∈| node_ptr_kinds h"
  assumes heap_is_wellformed_one_parent:
    "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children
                        ⟹ h ⊢ get_child_nodes ptr' →r children'
                        ⟹ set children ∩ set children' ≠ {} ⟹ ptr = ptr'"
  assumes heap_is_wellformed_one_disc_parent:
    "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
                        ⟹ h ⊢ get_disconnected_nodes document_ptr' →r disc_nodes'
                        ⟹ set disc_nodes ∩ set disc_nodes' ≠ {} ⟹ document_ptr = document_ptr'"
  assumes heap_is_wellformed_children_disc_nodes_different:
    "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children
                        ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
                        ⟹ set children ∩ set disc_nodes = {}"
  assumes heap_is_wellformed_disconnected_nodes_distinct:
    "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes document_ptr →r disc_nodes
                        ⟹ distinct disc_nodes"
  assumes heap_is_wellformed_children_distinct:
    "heap_is_wellformed h ⟹ h ⊢ get_child_nodes ptr →r children ⟹ distinct children"
  assumes heap_is_wellformed_children_disc_nodes:
    "heap_is_wellformed h ⟹ node_ptr |∈| node_ptr_kinds h
   ⟹  ¬(∃parent ∈ fset (object_ptr_kinds h). node_ptr ∈ set |h ⊢ get_child_nodes parent|r)
   ⟹ (∃document_ptr ∈ fset (document_ptr_kinds h). node_ptr ∈ set |h ⊢ get_disconnected_nodes document_ptr|r)"
  assumes parent_child_rel_child:
    "h ⊢ get_child_nodes ptr →r children
   ⟹ child ∈ set children ⟷ (ptr, cast child) ∈ parent_child_rel h"
  assumes parent_child_rel_finite:
    "heap_is_wellformed h ⟹ finite (parent_child_rel h)"
  assumes parent_child_rel_acyclic:
    "heap_is_wellformed h ⟹ acyclic (parent_child_rel h)"
  assumes parent_child_rel_node_ptr:
    "(parent, child_ptr) ∈ parent_child_rel h ⟹ is_node_ptr_kind child_ptr"
  assumes parent_child_rel_parent_in_heap:
    "(parent, child_ptr) ∈ parent_child_rel h ⟹ parent |∈| object_ptr_kinds h"
  assumes parent_child_rel_child_in_heap:
    "heap_is_wellformed h ⟹ type_wf h ⟹ known_ptr parent
   ⟹ (parent, child_ptr) ∈ parent_child_rel h ⟹ child_ptr |∈| object_ptr_kinds h"

interpretation i_heap_is_wellformed?: l_heap_is_wellformedCore_DOM known_ptr type_wf get_child_nodes
  get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
  heap_is_wellformed parent_child_rel
  apply(unfold_locales)
  by(auto simp add: heap_is_wellformed_def parent_child_rel_def)
declare l_heap_is_wellformedCore_DOM_axioms[instances]


lemma heap_is_wellformed_is_l_heap_is_wellformed [instances]:
  "l_heap_is_wellformed type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes
                        get_disconnected_nodes"
  apply(auto simp add: l_heap_is_wellformed_def)[1]
  using heap_is_wellformed_children_in_heap
                apply blast
  using heap_is_wellformed_disc_nodes_in_heap
               apply blast
  using heap_is_wellformed_one_parent
              apply blast
  using heap_is_wellformed_one_disc_parent
             apply blast
  using heap_is_wellformed_children_disc_nodes_different
            apply blast
  using heap_is_wellformed_disconnected_nodes_distinct
           apply blast
  using heap_is_wellformed_children_distinct
          apply blast
  using heap_is_wellformed_children_disc_nodes
         apply blast
  using parent_child_rel_child
        apply (blast)
  using parent_child_rel_child
       apply(blast)
  using parent_child_rel_finite
      apply blast
  using parent_child_rel_acyclic
     apply blast
  using parent_child_rel_node_ptr
    apply blast
  using parent_child_rel_parent_in_heap
   apply blast
  using parent_child_rel_child_in_heap
  apply blast
  done

subsection ‹get\_parent›

locale l_get_parent_wfCore_DOM =
  l_get_parentCore_DOM
  known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  + l_heap_is_wellformed
  type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and type_wf :: "(_) heap ⇒ bool"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and known_ptrs :: "(_) heap ⇒ bool"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma child_parent_dual:
  assumes heap_is_wellformed: "heap_is_wellformed h"
  assumes "h ⊢ get_child_nodes ptr →r children"
  assumes "child ∈ set children"
  assumes "known_ptrs h"
  assumes type_wf: "type_wf h"
  shows "h ⊢ get_parent child →r Some ptr"
proof -
  obtain ptrs where ptrs: "h ⊢ object_ptr_kinds_M →r ptrs"
    by(simp add: object_ptr_kinds_M_defs)
  then have h1: "ptr ∈ set ptrs"
    using get_child_nodes_ok assms(2) is_OK_returns_result_I
    by (metis (no_types, opaque_lifting) ObjectMonad.ptr_kinds_ptr_kinds_M
        ‹⋀thesis. (⋀ptrs. h ⊢ object_ptr_kinds_M →r ptrs ⟹ thesis) ⟹ thesis›
        get_child_nodes_ptr_in_heap returns_result_eq select_result_I2)

  let ?P = "(λptr. get_child_nodes ptr ⤜ (λchildren. return (child ∈ set children)))"
  let ?filter = "filter_M ?P ptrs"

  have "h ⊢ ok ?filter"
    using ptrs type_wf
    using get_child_nodes_ok
    apply(auto intro!: filter_M_is_OK_I bind_is_OK_pure_I get_child_nodes_ok simp add: bind_pure_I)[1]
    using assms(4) local.known_ptrs_known_ptr by blast
  then obtain parent_ptrs where parent_ptrs: "h ⊢ ?filter →r parent_ptrs"
    by auto

  have h5: "∃!x. x ∈ set ptrs ∧ h ⊢ Heap_Error_Monad.bind (get_child_nodes x)
                  (λchildren. return (child ∈ set children)) →r True"
    apply(auto intro!: bind_pure_returns_result_I)[1]
    using heap_is_wellformed_one_parent
  proof -
    have "h ⊢ (return (child ∈ set children)::((_) heap, exception, bool) prog) →r True"
      by (simp add: assms(3))
    then show
      "∃z. z ∈ set ptrs ∧ h ⊢ Heap_Error_Monad.bind (get_child_nodes z)
                               (λns. return (child ∈ set ns)) →r True"
      by (metis (no_types) assms(2) bind_pure_returns_result_I2 h1 is_OK_returns_result_I
          local.get_child_nodes_pure select_result_I2)
  next
    fix x y
    assume 0: "x ∈ set ptrs"
      and 1: "h ⊢ Heap_Error_Monad.bind (get_child_nodes x)
                  (λchildren. return (child ∈ set children)) →r True"
      and 2: "y ∈ set ptrs"
      and 3: "h ⊢ Heap_Error_Monad.bind (get_child_nodes y)
                  (λchildren. return (child ∈ set children)) →r True"
      and 4: "(⋀h ptr children ptr' children'. heap_is_wellformed h
              ⟹ h ⊢ get_child_nodes ptr →r children ⟹ h ⊢ get_child_nodes ptr' →r children'
              ⟹ set children ∩ set children' ≠ {} ⟹ ptr = ptr')"
    then show "x = y"
      by (metis (no_types, lifting) bind_returns_result_E disjoint_iff_not_equal heap_is_wellformed
          return_returns_result)
  qed

  have "child |∈| node_ptr_kinds h"
    using heap_is_wellformed_children_in_heap heap_is_wellformed assms(2) assms(3)
    by fast
  moreover have "parent_ptrs = [ptr]"
    apply(rule filter_M_ex1[OF parent_ptrs h1 h5])
    using ptrs assms(2) assms(3)
    by(auto simp add: object_ptr_kinds_M_defs bind_pure_I intro!: bind_pure_returns_result_I)
  ultimately  show ?thesis
    using ptrs parent_ptrs
    by(auto simp add: bind_pure_I get_parent_def
        elim!: bind_returns_result_E2
        intro!: bind_pure_returns_result_I filter_M_pure_I) (*slow, ca 1min *)
qed

lemma parent_child_rel_parent:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_parent child_node →r Some parent"
  shows "(parent, cast child_node) ∈ parent_child_rel h"
  using assms parent_child_rel_child get_parent_child_dual by auto

lemma heap_wellformed_induct [consumes 1, case_names step]:
  assumes "heap_is_wellformed h"
    and step: "⋀parent. (⋀children child. h ⊢ get_child_nodes parent →r children
               ⟹ child ∈ set children ⟹ P (cast child)) ⟹ P parent"
  shows "P ptr"
proof -
  fix ptr
  have "wf ((parent_child_rel h)¯)"
    by (simp add: assms(1) finite_acyclic_wf_converse parent_child_rel_acyclic parent_child_rel_finite)
  then show "?thesis"
  proof (induct rule: wf_induct_rule)
    case (less parent)
    then show ?case
      using assms parent_child_rel_child
      by (meson converse_iff)
  qed
qed

lemma heap_wellformed_induct2 [consumes 3, case_names not_in_heap empty_children step]:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
    and not_in_heap: "⋀parent. parent |∉| object_ptr_kinds h ⟹ P parent"
    and empty_children: "⋀parent. h ⊢ get_child_nodes parent →r [] ⟹ P parent"
    and step: "⋀parent children child. h ⊢ get_child_nodes parent →r children
               ⟹ child ∈ set children ⟹ P (cast child) ⟹ P parent"
  shows "P ptr"
proof(insert assms(1), induct rule: heap_wellformed_induct)
  case (step parent)
  then show ?case
  proof(cases "parent |∈| object_ptr_kinds h")
    case True
    then obtain children where children: "h ⊢ get_child_nodes parent →r children"
      using get_child_nodes_ok assms(2) assms(3)
      by (meson is_OK_returns_result_E local.known_ptrs_known_ptr)
    then show ?thesis
    proof (cases "children = []")
      case True
      then show ?thesis
        using children empty_children
        by simp
    next
      case False
      then show ?thesis
        using assms(6) children last_in_set step.hyps by blast
    qed
  next
    case False
    then show ?thesis
      by (simp add: not_in_heap)
  qed
qed

lemma heap_wellformed_induct_rev [consumes 1, case_names step]:
  assumes "heap_is_wellformed h"
    and step: "⋀child. (⋀parent child_node. cast child_node = child
               ⟹ h ⊢ get_parent child_node →r Some parent ⟹ P parent) ⟹ P child"
  shows "P ptr"
proof -
  fix ptr
  have "wf ((parent_child_rel h))"
    by (simp add: assms(1) local.parent_child_rel_acyclic local.parent_child_rel_finite
        wf_iff_acyclic_if_finite)

  then show "?thesis"
  proof (induct rule: wf_induct_rule)
    case (less child)
    show ?case
      using assms get_parent_child_dual
      by (metis less.hyps parent_child_rel_parent)
  qed
qed
end

interpretation i_get_parent_wf?: l_get_parent_wfCore_DOM known_ptr type_wf get_child_nodes
  get_child_nodes_locs known_ptrs get_parent get_parent_locs heap_is_wellformed
  parent_child_rel get_disconnected_nodes
  using instances
  by(simp add: l_get_parent_wfCore_DOM_def)
declare l_get_parent_wfCore_DOM_axioms[instances]


locale l_get_parent_wf2Core_DOM =
  l_get_parent_wfCore_DOM
  known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  heap_is_wellformed parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs
  + l_heap_is_wellformedCore_DOM
  known_ptr type_wf get_child_nodes get_child_nodes_locs get_disconnected_nodes
  get_disconnected_nodes_locs heap_is_wellformed parent_child_rel
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and type_wf :: "(_) heap ⇒ bool"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and known_ptrs :: "(_) heap ⇒ bool"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and get_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin
lemma preserves_wellformedness_writes_needed:
  assumes heap_is_wellformed: "heap_is_wellformed h"
    and "h ⊢ f →h h'"
    and "writes SW f h h'"
    and preserved_get_child_nodes:
    "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h'
                      ⟹ ∀object_ptr. ∀r ∈ get_child_nodes_locs object_ptr. r h h'"
    and preserved_get_disconnected_nodes:
    "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h'
                      ⟹ ∀document_ptr. ∀r ∈ get_disconnected_nodes_locs document_ptr. r h h'"
    and preserved_object_pointers:
    "⋀h h' w. w ∈ SW ⟹ h ⊢ w →h h'
                     ⟹ ∀object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "heap_is_wellformed h'"
proof -
  have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
    using assms(2) assms(3) object_ptr_kinds_preserved preserved_object_pointers by blast
  then have object_ptr_kinds_eq:
    "⋀ptrs. h ⊢ object_ptr_kinds_M →r ptrs = h' ⊢ object_ptr_kinds_M →r ptrs"
    unfolding object_ptr_kinds_M_defs by simp
  then have object_ptr_kinds_eq2: "|h ⊢ object_ptr_kinds_M|r = |h' ⊢ object_ptr_kinds_M|r"
    using select_result_eq by force
  then have node_ptr_kinds_eq2: "|h ⊢ node_ptr_kinds_M|r = |h' ⊢ node_ptr_kinds_M|r"
    using node_ptr_kinds_M_eq by auto
  then have node_ptr_kinds_eq3: "node_ptr_kinds h = node_ptr_kinds h'"
    by auto
  have document_ptr_kinds_eq2: "|h ⊢ document_ptr_kinds_M|r = |h' ⊢ document_ptr_kinds_M|r"
    using object_ptr_kinds_eq2 document_ptr_kinds_M_eq by auto
  then have document_ptr_kinds_eq3: "document_ptr_kinds h = document_ptr_kinds h'"
    by auto
  have children_eq:
    "⋀ptr children. h ⊢ get_child_nodes ptr →r children = h' ⊢ get_child_nodes ptr →r children"
    apply(rule reads_writes_preserved[OF get_child_nodes_reads assms(3) assms(2)])
    using preserved_get_child_nodes by fast
  then have children_eq2: "⋀ptr. |h ⊢ get_child_nodes ptr|r = |h' ⊢ get_child_nodes ptr|r"
    using select_result_eq by force
  have disconnected_nodes_eq:
    "⋀document_ptr disconnected_nodes.
        h ⊢ get_disconnected_nodes document_ptr →r disconnected_nodes
                             = h' ⊢ get_disconnected_nodes document_ptr →r disconnected_nodes"
    apply(rule reads_writes_preserved[OF get_disconnected_nodes_reads assms(3) assms(2)])
    using preserved_get_disconnected_nodes by fast
  then have disconnected_nodes_eq2:
    "⋀document_ptr. |h ⊢ get_disconnected_nodes document_ptr|r
                            = |h' ⊢ get_disconnected_nodes document_ptr|r"
    using select_result_eq by force
  have get_parent_eq: "⋀ptr parent. h ⊢ get_parent ptr →r parent = h' ⊢ get_parent ptr →r parent"
    apply(rule reads_writes_preserved[OF get_parent_reads assms(3) assms(2)])
    using preserved_get_child_nodes preserved_object_pointers unfolding get_parent_locs_def by fast
  have "a_acyclic_heap h"
    using heap_is_wellformed by (simp add: heap_is_wellformed_def)
  have "parent_child_rel h' ⊆ parent_child_rel h"
  proof
    fix x
    assume "x ∈ parent_child_rel h'"
    then show "x ∈ parent_child_rel h"
      by(simp add: parent_child_rel_def  children_eq2 object_ptr_kinds_eq3)
  qed
  then have "a_acyclic_heap h'"
    using ‹a_acyclic_heap h› acyclic_heap_def acyclic_subset by blast

  moreover have "a_all_ptrs_in_heap h"
    using heap_is_wellformed by (simp add: heap_is_wellformed_def)
  then have "a_all_ptrs_in_heap h'"
    by (simp add: children_eq2 disconnected_nodes_eq2 document_ptr_kinds_eq3
        l_heap_is_wellformedCore_DOM_defs.a_all_ptrs_in_heap_def node_ptr_kinds_eq3 object_ptr_kinds_eq3)

  moreover have h0: "a_distinct_lists h"
    using heap_is_wellformed by (simp add: heap_is_wellformed_def)
  have h1: "map (λptr. |h ⊢ get_child_nodes ptr|r) (sorted_list_of_set (fset (object_ptr_kinds h)))
         = map (λptr. |h' ⊢ get_child_nodes ptr|r) (sorted_list_of_set (fset (object_ptr_kinds h')))"
    by (simp add: children_eq2 object_ptr_kinds_eq3)
  have h2: "map (λdocument_ptr. |h ⊢ get_disconnected_nodes document_ptr|r)
               (sorted_list_of_set (fset (document_ptr_kinds h)))
          = map (λdocument_ptr. |h' ⊢ get_disconnected_nodes document_ptr|r)
                (sorted_list_of_set (fset (document_ptr_kinds h')))"
    using disconnected_nodes_eq document_ptr_kinds_eq2 select_result_eq by force
  have "a_distinct_lists h'"
    using h0
    by(simp add: a_distinct_lists_def h1 h2)

  moreover have "a_owner_document_valid h"
    using heap_is_wellformed by (simp add: heap_is_wellformed_def)
  then have "a_owner_document_valid h'"
    by(auto simp add: a_owner_document_valid_def children_eq2 disconnected_nodes_eq2
        object_ptr_kinds_eq3 node_ptr_kinds_eq3 document_ptr_kinds_eq3)
  ultimately show ?thesis
    by (simp add: heap_is_wellformed_def)
qed
end

interpretation i_get_parent_wf2?: l_get_parent_wf2Core_DOM known_ptr type_wf get_child_nodes
  get_child_nodes_locs known_ptrs get_parent get_parent_locs
  heap_is_wellformed parent_child_rel get_disconnected_nodes
  get_disconnected_nodes_locs
  using l_get_parent_wfCore_DOM_axioms l_heap_is_wellformedCore_DOM_axioms
  by (simp add: l_get_parent_wf2Core_DOM_def)

declare l_get_parent_wf2Core_DOM_axioms[instances]
locale l_get_parent_wf = l_type_wf + l_known_ptrs  + l_heap_is_wellformed_defs
  + l_get_child_nodes_defs + l_get_parent_defs +
  assumes child_parent_dual:
    "heap_is_wellformed h
    ⟹ type_wf h
    ⟹ known_ptrs h
    ⟹ h ⊢ get_child_nodes ptr →r children
    ⟹ child ∈ set children
    ⟹ h ⊢ get_parent child →r Some ptr"
  assumes heap_wellformed_induct [consumes 1, case_names step]:
    "heap_is_wellformed h
    ⟹ (⋀parent. (⋀children child. h ⊢ get_child_nodes parent →r children
    ⟹ child ∈ set children ⟹ P (cast child)) ⟹ P parent)
    ⟹ P ptr"
  assumes heap_wellformed_induct_rev [consumes 1, case_names step]:
    "heap_is_wellformed h
    ⟹ (⋀child. (⋀parent child_node. cast child_node = child
    ⟹ h ⊢ get_parent child_node →r Some parent ⟹ P parent) ⟹ P child)
    ⟹ P ptr"
  assumes parent_child_rel_parent: "heap_is_wellformed h
    ⟹ h ⊢ get_parent child_node →r Some parent
    ⟹ (parent, cast child_node) ∈ parent_child_rel h"

lemma get_parent_wf_is_l_get_parent_wf [instances]:
  "l_get_parent_wf type_wf known_ptr known_ptrs heap_is_wellformed parent_child_rel
  get_child_nodes get_parent"
  using known_ptrs_is_l_known_ptrs
  apply(auto simp add: l_get_parent_wf_def l_get_parent_wf_axioms_def)[1]
  using child_parent_dual heap_wellformed_induct heap_wellformed_induct_rev parent_child_rel_parent
  by metis+



subsection ‹get\_disconnected\_nodes›



subsection ‹set\_disconnected\_nodes›


subsubsection ‹get\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM =
  l_set_disconnected_nodes_get_disconnected_nodes
  type_wf get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
  set_disconnected_nodes_locs
  + l_heap_is_wellformed
  type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs
  for known_ptr :: "(_) object_ptr ⇒ bool"
    and type_wf :: "(_) heap ⇒ bool"
    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 heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) set"
    and get_child_nodes :: "(_) object_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_child_nodes_locs :: "(_) object_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
begin

lemma remove_from_disconnected_nodes_removes:
  assumes "heap_is_wellformed h"
  assumes "h ⊢ get_disconnected_nodes ptr →r disc_nodes"
  assumes "h ⊢ set_disconnected_nodes ptr (remove1 node_ptr disc_nodes) →h h'"
  assumes "h' ⊢ get_disconnected_nodes ptr →r disc_nodes'"
  shows "node_ptr ∉ set disc_nodes'"
  using assms
  by (metis distinct_remove1_removeAll heap_is_wellformed_disconnected_nodes_distinct
      set_disconnected_nodes_get_disconnected_nodes member_remove remove_code(1)
      returns_result_eq)
end

locale l_set_disconnected_nodes_get_disconnected_nodes_wf = l_heap_is_wellformed
  + l_set_disconnected_nodes_get_disconnected_nodes +
  assumes remove_from_disconnected_nodes_removes:
    "heap_is_wellformed h ⟹ h ⊢ get_disconnected_nodes ptr →r disc_nodes
                          ⟹ h ⊢ set_disconnected_nodes ptr (remove1 node_ptr disc_nodes) →h h'
                          ⟹ h' ⊢ get_disconnected_nodes ptr →r disc_nodes'
                          ⟹ node_ptr ∉ set disc_nodes'"

interpretation i_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM?:
  l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM  known_ptr type_wf get_disconnected_nodes
  get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs heap_is_wellformed
  parent_child_rel get_child_nodes
  using instances
  by (simp add: l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM_def)
declare l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM_axioms[instances]

lemma set_disconnected_nodes_get_disconnected_nodes_wf_is_l_set_disconnected_nodes_get_disconnected_nodes_wf [instances]:
  "l_set_disconnected_nodes_get_disconnected_nodes_wf type_wf known_ptr heap_is_wellformed parent_child_rel
   get_child_nodes get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
      set_disconnected_nodes_locs"
  apply(auto simp add: l_set_disconnected_nodes_get_disconnected_nodes_wf_def
      l_set_disconnected_nodes_get_disconnected_nodes_wf_axioms_def instances)[1]
  using remove_from_disconnected_nodes_removes apply fast
  done


subsection ‹get\_root\_node›

locale l_get_root_node_wfCore_DOM =
  l_heap_is_wellformed
  type_wf known_ptr heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs
  get_disconnected_nodes get_disconnected_nodes_locs
  + l_get_parentCore_DOM
  known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  + l_get_parent_wf
  type_wf known_ptr known_ptrs heap_is_wellformed parent_child_rel get_child_nodes
  get_child_nodes_locs get_parent get_parent_locs
  + l_get_root_nodeCore_DOM
  type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs
  get_ancestors get_ancestors_locs get_root_node get_root_node_locs
  for known_ptr :: "(_::linorder) object_ptr ⇒ bool"
    and type_wf :: "(_) heap ⇒ bool"
    and known_ptrs :: "(_) heap ⇒ bool"
    and heap_is_wellformed :: "(_) heap ⇒ bool"
    and parent_child_rel :: "(_) heap ⇒ ((_) object_ptr × (_) object_ptr) 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_disconnected_nodes :: "(_) document_ptr ⇒ ((_) heap, exception, (_) node_ptr list) prog"
    and get_disconnected_nodes_locs :: "(_) document_ptr ⇒ ((_) heap ⇒ (_) heap ⇒ bool) set"
    and get_parent :: "(_) node_ptr ⇒ ((_) heap, exception, (_) object_ptr option) prog"
    and get_parent_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_root_node :: "(_) object_ptr ⇒ ((_) heap, exception, (_) object_ptr) prog"
    and get_root_node_locs :: "((_) heap ⇒ (_) heap ⇒ bool) set"

begin
lemma get_ancestors_reads:
  assumes "heap_is_wellformed h"
  shows "reads get_ancestors_locs (get_ancestors node_ptr) h h'"
proof (insert assms(1), induct rule: heap_wellformed_induct_rev)
  case (step child)
  then show ?case
    using [[simproc del: Product_Type.unit_eq]] get_parent_reads[unfolded reads_def]
    apply(simp (no_asm) add: get_ancestors_def)
    by(auto simp add: get_ancestors_locs_def reads_subset[OF return_reads] get_parent_reads_pointers
        intro!: reads_bind_pure reads_subset[OF check_in_heap_reads]
        reads_subset[OF get_parent_reads] reads_subset[OF get_child_nodes_reads]
        split: option.splits)
qed

lemma get_ancestors_ok:
  assumes "heap_is_wellformed h"
    and "ptr |∈| object_ptr_kinds h"
    and "known_ptrs h"
    and type_wf: "type_wf h"
  shows "h ⊢ ok (get_ancestors ptr)"
proof (insert assms(1) assms(2), induct rule: heap_wellformed_induct_rev)
  case (step child)
  then show ?case
    using assms(3) assms(4)
    apply(simp (no_asm) add: get_ancestors_def)
    apply(simp add: assms(1) get_parent_parent_in_heap)
    by(auto intro!: bind_is_OK_pure_I bind_pure_I get_parent_ok split: option.splits)
qed

lemma get_root_node_ptr_in_heap:
  assumes "h ⊢ ok (get_root_node ptr)"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  unfolding get_root_node_def
  using get_ancestors_ptr_in_heap
  by auto


lemma get_root_node_ok:
  assumes "heap_is_wellformed h" "known_ptrs h" "type_wf h"
    and "ptr |∈| object_ptr_kinds h"
  shows "h ⊢ ok (get_root_node ptr)"
  unfolding get_root_node_def
  using assms get_ancestors_ok
  by auto


lemma get_ancestors_parent:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_parent child →r Some parent"
  shows "h ⊢ get_ancestors (cast child) →r (cast child) # parent # ancestors
     ⟷ h ⊢ get_ancestors parent →r parent # ancestors"
proof
  assume a1: "h ⊢ get_ancestors (castnode_ptr2object_ptr child) →r
castnode_ptr2object_ptr child # parent # ancestors"
  then have "h ⊢ Heap_Error_Monad.bind (check_in_heap (castnode_ptr2object_ptr child))
          (λ_. Heap_Error_Monad.bind (get_parent child)
              (λx. Heap_Error_Monad.bind (case x of None ⇒ return [] | Some x ⇒ get_ancestors x)
               (λancestors. return (castnode_ptr2object_ptr child # ancestors))))
        →r castnode_ptr2object_ptr child # parent # ancestors"
    by(simp add: get_ancestors_def)
  then show "h ⊢ get_ancestors parent →r parent # ancestors"
    using assms(2) apply(auto elim!: bind_returns_result_E2 split: option.splits)[1]
    using returns_result_eq by fastforce
next
  assume "h ⊢ get_ancestors parent →r parent # ancestors"
  then show "h ⊢ get_ancestors (castnode_ptr2object_ptr child) →r castnode_ptr2object_ptr child # parent # ancestors"
    using assms(2)
    apply(simp (no_asm) add: get_ancestors_def)
    apply(auto intro!: bind_pure_returns_result_I split: option.splits)[1]
    by (metis (full_types) assms(2) check_in_heap_ptr_in_heap is_OK_returns_result_I
        local.get_parent_ptr_in_heap node_ptr_kinds_commutes old.unit.exhaust
        select_result_I)
qed


lemma get_ancestors_never_empty:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_ancestors child →r ancestors"
  shows "ancestors ≠ []"
proof(insert assms(2), induct arbitrary: ancestors rule: heap_wellformed_induct_rev[OF assms(1)])
  case (1 child)
  then show ?case
  proof (induct "castobject_ptr2node_ptr child")
    case None
    then show ?case
      apply(simp add: get_ancestors_def)
      by(auto elim!: bind_returns_result_E2 split: option.splits)
  next
    case (Some child_node)
    then obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →r parent_opt"
      apply(simp add: get_ancestors_def)
      by(auto elim!: bind_returns_result_E2 split: option.splits)
    with Some show ?case
    proof(induct parent_opt)
      case None
      then show ?case
        apply(simp add: get_ancestors_def)
        by(auto elim!: bind_returns_result_E2 split: option.splits)
    next
      case (Some option)
      then show ?case
        apply(simp add: get_ancestors_def)
        by(auto elim!: bind_returns_result_E2 split: option.splits)
    qed
  qed
qed



lemma get_ancestors_subset:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_ancestors ptr →r ancestors"
    and "ancestor ∈ set ancestors"
    and "h ⊢ get_ancestors ancestor →r ancestor_ancestors"
    and type_wf: "type_wf h"
    and known_ptrs: "known_ptrs h"
  shows "set ancestor_ancestors ⊆ set ancestors"
proof (insert assms(1) assms(2) assms(3), induct ptr arbitrary: ancestors
    rule: heap_wellformed_induct_rev)
  case (step child)
  have "child |∈| object_ptr_kinds h"
    using get_ancestors_ptr_in_heap step(2) by auto
      (*  then have "h ⊢ check_in_heap child →r ()"
    using returns_result_select_result by force *)
  show ?case
  proof (induct "castobject_ptr2node_ptr child")
    case None
    then have "ancestors = [child]"
      using step(2) step(3)
      by(auto simp add: get_ancestors_def elim!: bind_returns_result_E2)
    show ?case
      using step(2) step(3)
      apply(auto simp add: ‹ancestors = [child]›)[1]
      using assms(4) returns_result_eq by fastforce
  next
    case (Some child_node)
    note s1 = Some
    obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →r parent_opt"
      using ‹child |∈| object_ptr_kinds h› assms(1) Some[symmetric]
        get_parent_ok[OF type_wf known_ptrs]
      by (metis (no_types, lifting) is_OK_returns_result_E known_ptrs get_parent_ok
          l_get_parentCore_DOM_axioms node_ptr_casts_commute node_ptr_kinds_commutes)
    then show ?case
    proof (induct parent_opt)
      case None
      then have "ancestors = [child]"
        using step(2) step(3) s1
        apply(simp add: get_ancestors_def)
        by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
      show ?case
        using step(2) step(3)
        apply(auto simp add: ‹ancestors = [child]›)[1]
        using assms(4) returns_result_eq by fastforce
    next
      case (Some parent)
      have "h ⊢ Heap_Error_Monad.bind (check_in_heap child)
          (λ_. Heap_Error_Monad.bind
                 (case castobject_ptr2node_ptr child of None ⇒ return []
                  | Some node_ptr ⇒ Heap_Error_Monad.bind (get_parent node_ptr)
                                         (λparent_ptr_opt. case parent_ptr_opt of None ⇒ return []
                                                                        | Some x ⇒ get_ancestors x))
                 (λancestors. return (child # ancestors)))
    →r  ancestors"
        using step(2)
        by(simp add: get_ancestors_def)
      moreover obtain tl_ancestors where tl_ancestors: "ancestors = child # tl_ancestors"
        using calculation
        by(auto elim!: bind_returns_result_E2 split: option.splits)
      ultimately have "h ⊢ get_ancestors parent →r tl_ancestors"
        using s1 Some
        by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
      show ?case
        using step(1)[OF s1[symmetric, simplified] Some ‹h ⊢ get_ancestors parent →r tl_ancestors›]
          step(3)
        apply(auto simp add: tl_ancestors)[1]
        by (metis assms(4) insert_iff list.simps(15) local.step(2) returns_result_eq tl_ancestors)
    qed
  qed
qed

lemma get_ancestors_also_parent:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_ancestors some_ptr →r ancestors"
    and "cast child ∈ set ancestors"
    and "h ⊢ get_parent child →r Some parent"
    and type_wf: "type_wf h"
    and known_ptrs: "known_ptrs h"
  shows "parent ∈ set ancestors"
proof -
  obtain child_ancestors where child_ancestors: "h ⊢ get_ancestors (cast child) →r child_ancestors"
    by (meson assms(1) assms(4) get_ancestors_ok is_OK_returns_result_I known_ptrs
        local.get_parent_ptr_in_heap node_ptr_kinds_commutes returns_result_select_result
        type_wf)
  then have "parent ∈ set child_ancestors"
    apply(simp add: get_ancestors_def)
    by(auto elim!: bind_returns_result_E2 split: option.splits dest!: returns_result_eq[OF assms(4)]
        get_ancestors_ptr)
  then show ?thesis
    using assms child_ancestors get_ancestors_subset by blast
qed

lemma get_ancestors_obtains_children:
  assumes "heap_is_wellformed h"
    and "ancestor ≠ ptr"
    and "ancestor ∈ set ancestors"
    and "h ⊢ get_ancestors ptr →r ancestors"
    and type_wf: "type_wf h"
    and known_ptrs: "known_ptrs h"
  obtains children ancestor_child where "h ⊢ get_child_nodes ancestor →r children"
    and "ancestor_child ∈ set children" and "cast ancestor_child ∈ set ancestors"
proof -
  assume 0: "(⋀children ancestor_child.
        h ⊢ get_child_nodes ancestor →r children ⟹
        ancestor_child ∈ set children ⟹ castnode_ptr2object_ptr ancestor_child ∈ set ancestors
        ⟹ thesis)"
  have "∃child. h ⊢ get_parent child →r Some ancestor ∧ cast child ∈ set ancestors"
  proof (insert assms(1) assms(2) assms(3) assms(4), induct ptr arbitrary: ancestors
      rule: heap_wellformed_induct_rev)
    case (step child)
    have "child |∈| object_ptr_kinds h"
      using get_ancestors_ptr_in_heap step(4) by auto
    show ?case
    proof (induct "castobject_ptr2node_ptr child")
      case None
      then have "ancestors = [child]"
        using step(3) step(4)
        by(auto simp add: get_ancestors_def elim!: bind_returns_result_E2)
      show ?case
        using step(2) step(3) step(4)
        by(auto simp add: ‹ancestors = [child]›)
    next
      case (Some child_node)
      note s1 = Some
      obtain parent_opt where parent_opt: "h ⊢ get_parent child_node →r parent_opt"
        using ‹child |∈| object_ptr_kinds h› assms(1) Some[symmetric]
        using get_parent_ok known_ptrs type_wf
        by (metis (no_types, lifting) is_OK_returns_result_E node_ptr_casts_commute
            node_ptr_kinds_commutes)
      then show ?case
      proof (induct parent_opt)
        case None
        then have "ancestors = [child]"
          using step(2) step(3) step(4) s1
          apply(simp add: get_ancestors_def)
          by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
        show ?case
          using step(2) step(3) step(4)
          by(auto simp add: ‹ancestors = [child]›)
      next
        case (Some parent)
        have "h ⊢ Heap_Error_Monad.bind (check_in_heap child)
            (λ_. Heap_Error_Monad.bind
                   (case castobject_ptr2node_ptr child of None ⇒ return []
                    | Some node_ptr ⇒ Heap_Error_Monad.bind (get_parent node_ptr)
                       (λparent_ptr_opt. case parent_ptr_opt of None ⇒ return []
                                                              | Some x ⇒ get_ancestors x))
                   (λancestors. return (child # ancestors)))
      →r  ancestors"
          using step(4)
          by(simp add: get_ancestors_def)
        moreover obtain tl_ancestors where tl_ancestors: "ancestors = child # tl_ancestors"
          using calculation
          by(auto elim!: bind_returns_result_E2 split: option.splits)
        ultimately have "h ⊢ get_ancestors parent →r tl_ancestors"
          using s1 Some
          by(auto elim!: bind_returns_result_E2 split: option.splits dest: returns_result_eq)
            (* have "ancestor ≠ parent" *)
        have "ancestor ∈ set tl_ancestors"
          using tl_ancestors step(2) step(3) by auto
        show ?case
        proof (cases "ancestor ≠ parent")
          case True
          show ?thesis
            using step(1)[OF s1[symmetric, simplified] Some True
                ‹ancestor ∈ set tl_ancestors› ‹h ⊢ get_ancestors parent →r tl_ancestors›]
            using tl_ancestors by auto
        next
          case False
          have "child ∈ set ancestors"
            using step(4) get_ancestors_ptr by simp
          then show ?thesis
            using Some False s1[symmetric] by(auto)
        qed
      qed
    qed
  qed
  then obtain child where child: "h ⊢ get_parent child →r Some ancestor"
    and in_ancestors: "cast child ∈ set ancestors"
    by auto
  then obtain children where
    children: "h ⊢ get_child_nodes ancestor →r children" and
    child_in_children: "child ∈ set children"
    using get_parent_child_dual by blast
  show thesis
    using 0[OF children child_in_children] child assms(3) in_ancestors by blast
qed

lemma get_ancestors_parent_child_rel:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_ancestors child →r ancestors"
    and known_ptrs: "known_ptrs h"
    and type_wf: "type_wf h"
  shows "(ptr, child) ∈ (parent_child_rel h)* ⟷ ptr ∈ set ancestors"
proof (safe)
  assume 3: "(ptr, child) ∈ (parent_child_rel h)*"
  show "ptr ∈ set ancestors"
  proof (insert 3, induct ptr rule: heap_wellformed_induct[OF assms(1)])
    case (1 ptr)
    then show ?case
    proof (cases "ptr = child")
      case True
      then show ?thesis
        by (metis (no_types, lifting) assms(2) bind_returns_result_E get_ancestors_def
            in_set_member member_rec(1) return_returns_result)
    next
      case False
      obtain ptr_child where
        ptr_child: "(ptr, ptr_child) ∈ (parent_child_rel h) ∧ (ptr_child, child) ∈ (parent_child_rel h)*"
        using converse_rtranclE[OF 1(2)] ‹ptr ≠ child›
        by metis
      then obtain ptr_child_node
        where ptr_child_ptr_child_node: "ptr_child = castnode_ptr2object_ptr ptr_child_node"
        using ptr_child node_ptr_casts_commute3 parent_child_rel_node_ptr
        by (metis )
      then obtain children where
        children: "h ⊢ get_child_nodes ptr →r children" and
        ptr_child_node: "ptr_child_node ∈ set children"
      proof -
        assume a1: "⋀children. ⟦h ⊢ get_child_nodes ptr →r children; ptr_child_node ∈ set children⟧
                   ⟹ thesis"

        have "ptr |∈| object_ptr_kinds h"
          using local.parent_child_rel_parent_in_heap ptr_child by blast
        moreover have "ptr_child_node ∈ set |h ⊢ get_child_nodes ptr|r"
          by (metis calculation known_ptrs local.get_child_nodes_ok local.known_ptrs_known_ptr
              local.parent_child_rel_child ptr_child ptr_child_ptr_child_node
              returns_result_select_result type_wf)
        ultimately show ?thesis
          using a1 get_child_nodes_ok type_wf known_ptrs
          by (meson local.known_ptrs_known_ptr returns_result_select_result)
      qed
      moreover have "(castnode_ptr2object_ptr ptr_child_node, child) ∈ (parent_child_rel h)*"
        using ptr_child ptr_child_ptr_child_node by auto
      ultimately have "castnode_ptr2object_ptr ptr_child_node ∈ set ancestors"
        using 1 by auto
      moreover have "h ⊢ get_parent ptr_child_node →r Some ptr"
        using assms(1) children ptr_child_node child_parent_dual
        using known_ptrs type_wf by blast
      ultimately show ?thesis
        using get_ancestors_also_parent assms type_wf by blast
    qed
  qed
next
  assume 3: "ptr ∈ set ancestors"
  show "(ptr, child) ∈ (parent_child_rel h)*"
  proof (insert 3, induct ptr rule: heap_wellformed_induct[OF assms(1)])
    case (1 ptr)
    then show ?case
    proof (cases "ptr = child")
      case True
      then show ?thesis
        by simp
    next
      case False
      then obtain children ptr_child_node where
        children: "h ⊢ get_child_nodes ptr →r children" and
        ptr_child_node: "ptr_child_node ∈ set children" and
        ptr_child_node_in_ancestors: "cast ptr_child_node ∈ set ancestors"
        using 1(2) assms(2) get_ancestors_obtains_children assms(1)
        using known_ptrs type_wf by blast
      then have "(castnode_ptr2object_ptr ptr_child_node, child) ∈ (parent_child_rel h)*"
        using 1(1) by blast

      moreover have "(ptr, cast ptr_child_node) ∈ parent_child_rel h"
        using children ptr_child_node assms(1) parent_child_rel_child_nodes2
        using child_parent_dual known_ptrs parent_child_rel_parent type_wf
        by blast

      ultimately show ?thesis
        by auto
    qed
  qed
qed

lemma get_root_node_parent_child_rel:
  assumes "heap_is_wellformed h"
    and "h ⊢ get_root_node child →r root"
    and known_ptrs: "known_ptrs h"
    and type_wf: "type_wf h"
  shows "(root, child) ∈ (parent_child_rel h)*"
  using assms get_ancestors_parent_child_rel
  apply(auto simp add: get_root_node_def elim!: bind_returns_result_E2)[1]
  using get_ancestors_never_empty last_in_set by blast


lemma get_ancestors_eq:
  assumes "heap_is_wellformed h"
    and "heap_is_wellformed h'"
    and "⋀object_ptr w. object_ptr ≠ ptr ⟹ w ∈ get_child_nodes_locs object_ptr ⟹ w h h'"
    and pointers_preserved: "⋀object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
    and known_ptrs: "known_ptrs h"
    and known_ptrs': "known_ptrs h'"
    and "h ⊢ get_ancestors ptr →r ancestors"
    and type_wf: "type_wf h"
    and type_wf': "type_wf h'"
  shows "h' ⊢ get_ancestors ptr →r ancestors"
proof -
  have object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
    using pointers_preserved object_ptr_kinds_preserved_small by blast
  then have object_ptr_kinds_M_eq:
    "⋀ptrs. h ⊢ object_ptr_kinds_M →r ptrs = h' ⊢ object_ptr_kinds_M →r ptrs"
    by(simp add: object_ptr_kinds_M_defs)
  then have object_ptr_kinds_eq: "|h ⊢ object_ptr_kinds_M|r = |h' ⊢ object_ptr_kinds_M|r"
    by(simp)
  have "h' ⊢ ok (get_ancestors ptr)"
    using get_ancestors_ok get_ancestors_ptr_in_heap object_ptr_kinds_eq3 assms(1) known_ptrs
      known_ptrs' assms(2) assms(7) type_wf'
    by blast
  then obtain ancestors' where ancestors': "h' ⊢ get_ancestors ptr →r ancestors'"
    by auto

  obtain root where root: "h ⊢ get_root_node ptr →r root"
  proof -
    assume 0: "(⋀root. h ⊢ get_root_node ptr →r root ⟹ thesis)"
    show thesis
      apply(rule 0)
      using assms(7)
      by(auto simp add: get_root_node_def elim!: bind_returns_result_E2 split: option.splits)
  qed

  have children_eq:
    "⋀p children. p ≠ ptr ⟹ h ⊢ get_child_nodes p →r children = h' ⊢ get_child_nodes p →r children"
    using get_child_nodes_reads assms(3)
    apply(simp add: reads_def reflp_def transp_def preserved_def)
    by blast

  have "acyclic (parent_child_rel h)"
    using assms(1) local.parent_child_rel_acyclic by auto
  have "acyclic (parent_child_rel h')"
    using assms(2) local.parent_child_rel_acyclic by blast
  have 2: "⋀c parent_opt. castnode_ptr2object_ptr c ∈ set ancestors ∩ set ancestors'
          ⟹ h ⊢ get_parent c →r parent_opt = h' ⊢ get_parent c →r parent_opt"
  proof -
    fix c parent_opt
    assume 1: " castnode_ptr2object_ptr c ∈ set ancestors ∩ set ancestors'"

    obtain ptrs where ptrs: "h ⊢ object_ptr_kinds_M →r ptrs"
      by simp

    let ?P = "(λptr. Heap_Error_Monad.bind (get_child_nodes ptr) (λchildren. return (c ∈ set children)))"
    have children_eq_True: "⋀p. p ∈ set ptrs ⟹ h ⊢ ?P p →r True ⟷ h' ⊢ ?P p →r True"
    proof -
      fix p
      assume "p ∈ set ptrs"
      then show "h ⊢ ?P p →r True ⟷ h' ⊢ ?P p →r True"
      proof (cases "p = ptr")
        case True
        have "(castnode_ptr2object_ptr c, ptr) ∈ (parent_child_rel h)*"
          using get_ancestors_parent_child_rel 1 assms by blast
        then have "(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h)"
        proof (cases "cast c = ptr")
          case True
          then show ?thesis
            using ‹acyclic (parent_child_rel h)› by(auto simp add: acyclic_def)
        next
          case False
          then have "(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h)*"
            using ‹acyclic (parent_child_rel h)› False rtrancl_eq_or_trancl rtrancl_trancl_trancl
              ‹(castnode_ptr2object_ptr c, ptr) ∈ (parent_child_rel h)*›
            by (metis acyclic_def)
          then show ?thesis
            using r_into_rtrancl by auto
        qed
        obtain children where children: "h ⊢ get_child_nodes ptr →r children"
          using type_wf
          by (metis ‹h' ⊢ ok get_ancestors ptr› assms(1) get_ancestors_ptr_in_heap get_child_nodes_ok
              heap_is_wellformed_def is_OK_returns_result_E known_ptrs local.known_ptrs_known_ptr
              object_ptr_kinds_eq3)
        then have "c ∉ set children"
          using ‹(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h)› assms(1)
          using parent_child_rel_child_nodes2
          using child_parent_dual known_ptrs parent_child_rel_parent
            type_wf by blast
        with children have "h ⊢ ?P p →r False"
          by(auto simp add: True)

        moreover have "(castnode_ptr2object_ptr c, ptr) ∈ (parent_child_rel h')*"
          using get_ancestors_parent_child_rel assms(2) ancestors' 1 known_ptrs' type_wf
            type_wf' by blast
        then have "(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h')"
        proof (cases "cast c = ptr")
          case True
          then show ?thesis
            using ‹acyclic (parent_child_rel h')› by(auto simp add: acyclic_def)
        next
          case False
          then have "(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h')*"
            using ‹acyclic (parent_child_rel h')› False rtrancl_eq_or_trancl rtrancl_trancl_trancl
              ‹(castnode_ptr2object_ptr c, ptr) ∈ (parent_child_rel h')*›
            by (metis acyclic_def)
          then show ?thesis
            using r_into_rtrancl by auto
        qed
        then have "(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h')"
          using r_into_rtrancl by auto
        obtain children' where children': "h' ⊢ get_child_nodes ptr →r children'"
          using  type_wf  type_wf'
          by (meson ‹h' ⊢ ok (get_ancestors ptr)› assms(2) get_ancestors_ptr_in_heap
              get_child_nodes_ok is_OK_returns_result_E known_ptrs'
              local.known_ptrs_known_ptr)
        then have "c ∉ set children'"
          using ‹(ptr, castnode_ptr2object_ptr c) ∉ (parent_child_rel h')› assms(2)  type_wf  type_wf'
          using parent_child_rel_child_nodes2 child_parent_dual known_ptrs' parent_child_rel_parent
          by auto
        with children' have "h' ⊢ ?P p →r False"
          by(auto simp add: True)

        ultimately show ?thesis
          by (metis returns_result_eq)
      next
        case False
        then show ?thesis
          using children_eq ptrs
          by (metis (no_types, lifting) bind_pure_returns_result_I bind_returns_result_E
              get_child_nodes_pure return_returns_result)
      qed
    qed
    have "⋀pa. pa ∈ set ptrs ⟹ h ⊢ ok (get_child_nodes pa
                     ⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
                     ⤜ (λchildren. return (c ∈ set children)))"
      using assms(1) assms(2) object_ptr_kinds_eq ptrs type_wf  type_wf'
      by (metis (no_types, lifting) ObjectMonad.ptr_kinds_ptr_kinds_M bind_is_OK_pure_I
          get_child_nodes_ok get_child_nodes_pure known_ptrs'
          local.known_ptrs_known_ptr return_ok select_result_I2)
    have children_eq_False:
      "⋀pa. pa ∈ set ptrs ⟹ h ⊢ get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children)) →r False = h' ⊢ get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children)) →r False"
    proof
      fix pa
      assume "pa ∈ set ptrs"
        and "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
      have "h ⊢ ok (get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))
           ⟹ h' ⊢ ok ( get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))"
        using ‹pa ∈ set ptrs› ‹⋀pa. pa ∈ set ptrs ⟹ h ⊢ ok (get_child_nodes pa
                    ⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
                    ⤜ (λchildren. return (c ∈ set children)))›
        by auto
      moreover have "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False
        ⟹ h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
        by (metis (mono_tags, lifting) ‹⋀pa. pa ∈ set ptrs
              ⟹ h ⊢ get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children)) →r True = h' ⊢ get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children)) →r True› ‹pa ∈ set ptrs›
            calculation is_OK_returns_result_I returns_result_eq returns_result_select_result)
      ultimately show "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
        using ‹h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False›
        by auto
    next
      fix pa
      assume "pa ∈ set ptrs"
        and "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
      have "h' ⊢ ok (get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))
            ⟹ h ⊢ ok ( get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)))"
        using ‹pa ∈ set ptrs› ‹⋀pa. pa ∈ set ptrs
              ⟹ h ⊢ ok (get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children))) = h' ⊢ ok ( get_child_nodes pa
                  ⤜ (λchildren. return (c ∈ set children)))›
        by auto
      moreover have "h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False
                  ⟹ h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
        by (metis (mono_tags, lifting)
            ‹⋀pa. pa ∈ set ptrs ⟹ h ⊢ get_child_nodes pa
                        ⤜ (λchildren. return (c ∈ set children)) →r True = h' ⊢ get_child_nodes pa
                        ⤜ (λchildren. return (c ∈ set children)) →r True› ‹pa ∈ set ptrs›
            calculation is_OK_returns_result_I returns_result_eq returns_result_select_result)
      ultimately show "h ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False"
        using ‹h' ⊢ get_child_nodes pa ⤜ (λchildren. return (c ∈ set children)) →r False› by blast
    qed

    have filter_eq: "⋀xs. h ⊢ filter_M ?P ptrs →r xs = h' ⊢ filter_M ?P ptrs →r xs"
    proof (rule filter_M_eq)
      show
        "⋀xs x. pure (Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children))) h"
        by(auto intro!: bind_pure_I)
    next
      show
        "⋀xs x. pure (Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children))) h'"
        by(auto intro!: bind_pure_I)
    next
      fix xs b x
      assume 0: "x ∈ set ptrs"
      then show "h ⊢ Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children)) →r b
              = h' ⊢ Heap_Error_Monad.bind (get_child_nodes x) (λchildren. return (c ∈ set children)) →r b"
        apply(induct b)
        using children_eq_True apply blast
        using children_eq_False apply blast
        done
    qed

    show "h ⊢ get_parent c →r parent_opt = h' ⊢ get_parent c →r parent_opt"
      apply(simp add: get_parent_def)
      apply(rule bind_cong_2)
         apply(simp)
        apply(simp)
       apply(simp add: check_in_heap_def node_ptr_kinds_def object_ptr_kinds_eq3)
      apply(rule bind_cong_2)
         apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
        apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
       apply(auto simp add: object_ptr_kinds_M_eq object_ptr_kinds_eq3)[1]
      apply(rule bind_cong_2)
         apply(auto intro!: filter_M_pure_I bind_pure_I)[1]
        apply(auto intro!: filter_M_pure_I bind_pure_I)[1]
       apply(auto simp add: filter_eq (* dest!: returns_result_eq[OF ptrs] *))[1]
      using filter_eq ptrs apply auto[1]
      using filter_eq ptrs by auto
  qed

  have "ancestors = ancestors'"
  proof(insert assms(1) assms(7) ancestors' 2, induct ptr arbitrary: ancestors ancestors'
      rule: heap_wellformed_induct_rev)
    case (step child)
    show ?case
      using step(2) step(3) step(4)
      apply(simp add: get_ancestors_def)
      apply(auto intro!: elim!: bind_returns_result_E2 split: option.splits)[1]
      using returns_result_eq apply fastforce
       apply (meson option.simps(3) returns_result_eq)
      by (metis IntD1 IntD2 option.inject returns_result_eq step.hyps)
  qed
  then show ?thesis
    using assms(5) ancestors'
    by simp
qed

lemma get_ancestors_remains_not_in_ancestors:
  assumes "heap_is_wellformed h"
    and "heap_is_wellformed h'"
    and "h ⊢ get_ancestors ptr →r ancestors"
    and "h' ⊢ get_ancestors ptr →r ancestors'"
    and "⋀p children children'. h ⊢ get_child_nodes p →r children
        ⟹ h' ⊢ get_child_nodes p →r children' ⟹ set children' ⊆ set children"
    and "node ∉ set ancestors"
    and object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
    and known_ptrs: "known_ptrs h"
    and type_wf: "type_wf h"
    and type_wf': "type_wf h'"
  shows "node ∉ set ancestors'"
proof -
  have object_ptr_kinds_M_eq:
    "⋀ptrs. h ⊢ object_ptr_kinds_M →r ptrs = h' ⊢ object_ptr_kinds_M →r ptrs"
    using object_ptr_kinds_eq3
    by(simp add: object_ptr_kinds_M_defs)
  then have object_ptr_kinds_eq: "|h ⊢ object_ptr_kinds_M|r = |h' ⊢ object_ptr_kinds_M|r"
    by(simp)

  show ?thesis
  proof (insert assms(1) assms(3) assms(4) assms(6), induct ptr arbitrary: ancestors ancestors'
      rule: heap_wellformed_induct_rev)
    case (step child)
    have 1: "⋀p parent. h' ⊢ get_parent p →r Some parent ⟹ h ⊢ get_parent p →r Some parent"
    proof -
      fix p parent
      assume "h' ⊢ get_parent p →r Some parent"
      then obtain children' where
        children': "h' ⊢ get_child_nodes parent →r children'" and
        p_in_children': "p ∈ set children'"
        using get_parent_child_dual by blast
      obtain children where children: "h ⊢ get_child_nodes parent →r children"
        using get_child_nodes_ok assms(1) get_child_nodes_ptr_in_heap object_ptr_kinds_eq children'
          known_ptrs
        using  type_wf type_wf'
        by (metis ‹h' ⊢ get_parent p →r Some parent› get_parent_parent_in_heap is_OK_returns_result_E
            local.known_ptrs_known_ptr object_ptr_kinds_eq3)
      have "p ∈ set children"
        using assms(5) children children' p_in_children'
        by blast
      then show "h ⊢ get_parent p →r Some parent"
        using child_parent_dual assms(1) children known_ptrs  type_wf  by blast
    qed
    have "node ≠ child"
      using assms(1) get_ancestors_parent_child_rel step.prems(1) step.prems(3) known_ptrs
      using type_wf type_wf'
      by blast
    then show ?case
      using step(2) step(3)
      apply(simp add: get_ancestors_def)
      using step(4)
      apply(auto elim!: bind_returns_result_E2 split: option.splits)[1]
      using 1
       apply (meson option.distinct(1) returns_result_eq)
      by (metis "1" option.inject returns_result_eq step.hyps)
  qed
qed

lemma get_ancestors_ptrs_in_heap:
  assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
  assumes "h ⊢ get_ancestors ptr →r ancestors"
  assumes "ptr' ∈ set ancestors"
  shows "ptr' |∈| object_ptr_kinds h"
proof (insert