Theory Core_DOM_Functions

(***********************************************************************************
 * 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‹Querying and Modifying the DOM›
text‹In this theory, we are formalizing the functions for querying and modifying 
the DOM.›

theory Core_DOM_Functions
imports
  "monads/DocumentMonad"
begin

text ‹If we do not declare show\_variants, then all abbreviations that contain
  constants that are overloaded by using adhoc\_overloading get immediately unfolded.›
declare [[show_variants]]

subsection ‹Various Functions›

lemma insort_split: "x  set (insort y xs)  (x = y  x  set xs)"
  apply(induct xs)
  by(auto)

lemma concat_map_distinct: 
  "distinct (concat (map f xs))  y  set (concat (map f xs))  ∃!x  set xs. y  set (f x)"
  apply(induct xs) 
  by(auto)

lemma concat_map_all_distinct: "distinct (concat (map f xs))  x  set xs  distinct (f x)"
  apply(induct xs)
  by(auto)

lemma distinct_concat_map_I:
  assumes "distinct xs"
    and "x. x  set xs  distinct (f x)"
and "x y. x  set xs  y  set xs  x  y  (set (f x))  (set (f y)) = {}"
shows "distinct (concat ((map f xs)))"
  using assms
  apply(induct xs) 
  by(auto)

lemma distinct_concat_map_E:
  assumes "distinct (concat ((map f xs)))"
  shows "x y. x  set xs  y  set xs  x  y  (set (f x))  (set (f y)) = {}"
    and "x. x  set xs  distinct (f x)"
  using assms
  apply(induct xs) 
  by(auto)

lemma bind_is_OK_E3 [elim]:
  assumes "h  ok (f  g)" and "pure f h"
  obtains x where "h  f r x"  and "h  ok (g x)"
  using assms 
  by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def pure_def
               split: sum.splits)


subsection ‹Basic Functions›

subsubsection ‹get\_child\_nodes›

locale l_get_child_nodesCore_DOM_defs
begin

definition get_child_nodeselement_ptr :: "(_) element_ptr  unit  (_, (_) node_ptr list) dom_prog"
  where
    "get_child_nodeselement_ptr element_ptr _ = get_M element_ptr RElement.child_nodes"

definition get_child_nodescharacter_data_ptr :: "(_) character_data_ptr  unit  (_, (_) node_ptr list) dom_prog"
  where
    "get_child_nodescharacter_data_ptr _ _ = return []"

definition get_child_nodesdocument_ptr :: "(_) document_ptr  unit  (_, (_) node_ptr list) dom_prog"
  where
    "get_child_nodesdocument_ptr document_ptr _ = do {
    doc_elem  get_M document_ptr document_element;
    (case doc_elem of
      Some element_ptr  return [cast element_ptr]
    | None  return [])
  }"

definition a_get_child_nodes_tups :: "(((_) object_ptr  bool) × ((_) object_ptr  unit
   (_, (_) node_ptr list) dom_prog)) list"
  where
    "a_get_child_nodes_tups = [
        (is_element_ptr, get_child_nodeselement_ptr  the  cast),
        (is_character_data_ptr, get_child_nodescharacter_data_ptr  the  cast),
        (is_document_ptr, get_child_nodesdocument_ptr  the  cast)
     ]"

definition a_get_child_nodes :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog"
  where
    "a_get_child_nodes ptr = invoke a_get_child_nodes_tups ptr ()"

definition a_get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
  where
    "a_get_child_nodes_locs ptr  
      (if is_element_ptr_kind ptr then {preserved (get_M (the (cast ptr)) RElement.child_nodes)} else {}) 
      (if is_document_ptr_kind ptr then {preserved (get_M (the (cast ptr)) RDocument.document_element)} else {}) 
      {preserved (get_M ptr RObject.nothing)}"

definition first_child :: "(_) object_ptr  (_, (_) node_ptr option) dom_prog"
  where
    "first_child ptr = do {
      children  a_get_child_nodes ptr;
      return (case children of []  None | child#_  Some child)}"
end

locale l_get_child_nodes_defs =
  fixes get_child_nodes :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog"
  fixes get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"

locale l_get_child_nodesCore_DOM =
  l_type_wf type_wf +
  l_known_ptr known_ptr + 
  l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
  l_get_child_nodesCore_DOM_defs
  for type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  and get_child_nodes :: "(_) object_ptr  (_, (_) node_ptr list) dom_prog"
  and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set" +
  assumes known_ptr_impl: "known_ptr = DocumentClass.known_ptr"
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes get_child_nodes_impl: "get_child_nodes = a_get_child_nodes"
  assumes get_child_nodes_locs_impl: "get_child_nodes_locs = a_get_child_nodes_locs"
begin
lemmas get_child_nodes_def = get_child_nodes_impl[unfolded a_get_child_nodes_def]
lemmas get_child_nodes_locs_def = get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def]

lemma get_child_nodes_split:
  "P (invoke (a_get_child_nodes_tups @ xs) ptr ()) =
    ((known_ptr ptr  P (get_child_nodes ptr))
     (¬(known_ptr ptr)  P (invoke xs ptr ())))"
  by(auto simp add: known_ptr_impl get_child_nodes_impl a_get_child_nodes_def a_get_child_nodes_tups_def 
                     known_ptr_defs CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs 
                     NodeClass.known_ptr_defs 
          split: invoke_splits)

lemma get_child_nodes_split_asm:
  "P (invoke (a_get_child_nodes_tups @ xs) ptr ()) =
    (¬((known_ptr ptr  ¬P (get_child_nodes ptr))
     (¬(known_ptr ptr)  ¬P (invoke xs ptr ()))))"
  by(auto simp add: known_ptr_impl get_child_nodes_impl a_get_child_nodes_def 
                    a_get_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs 
                    ElementClass.known_ptr_defs NodeClass.known_ptr_defs 
          split: invoke_splits)

lemmas get_child_nodes_splits = get_child_nodes_split get_child_nodes_split_asm

lemma get_child_nodes_ok [simp]:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "ptr |∈| object_ptr_kinds h"
  shows "h  ok (get_child_nodes ptr)"
  using assms(1) assms(2) assms(3)
  apply(auto simp add:  known_ptr_impl type_wf_impl get_child_nodes_def a_get_child_nodes_tups_def)[1]
  apply(split invoke_splits, rule conjI)+
     apply((rule impI)+, drule(1) known_ptr_not_document_ptr, drule(1) known_ptr_not_character_data_ptr, 
                         drule(1) known_ptr_not_element_ptr)
     apply(auto simp add: NodeClass.known_ptr_defs)[1]
    apply(auto simp add: get_child_nodesdocument_ptr_def dest: get_MDocument_ok 
               split: list.splits option.splits intro!: bind_is_OK_I2)[1]
   apply(auto simp add: get_child_nodescharacter_data_ptr_def)[1]                                                    
  apply (auto simp add: get_child_nodeselement_ptr_def  CharacterDataClass.type_wf_defs 
                        DocumentClass.type_wf_defs intro!: bind_is_OK_I2 split: option.splits)[1]
  using get_MElement_ok type_wf h[unfolded type_wf_impl] by blast

lemma get_child_nodes_ptr_in_heap [simp]:
  assumes "h  get_child_nodes ptr r children"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  by(auto simp add: get_child_nodes_impl a_get_child_nodes_def invoke_ptr_in_heap 
          dest: is_OK_returns_result_I)

lemma get_child_nodes_pure [simp]:
  "pure (get_child_nodes ptr) h"
  apply (auto simp add: get_child_nodes_impl a_get_child_nodes_def a_get_child_nodes_tups_def)[1]
  apply(split invoke_splits, rule conjI)+
  by(auto simp add: get_child_nodesdocument_ptr_def get_child_nodescharacter_data_ptr_def 
                   get_child_nodeselement_ptr_def intro!: bind_pure_I split: option.splits)

lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
  apply(simp add: get_child_nodes_locs_impl get_child_nodes_impl a_get_child_nodes_def 
      a_get_child_nodes_tups_def a_get_child_nodes_locs_def) 
  apply(split invoke_splits, rule conjI)+
     apply(auto)[1] 
    apply(auto simp add: get_child_nodesdocument_ptr_def intro: reads_subset[OF reads_singleton] 
      reads_subset[OF check_in_heap_reads]  
      intro!: reads_bind_pure  reads_subset[OF return_reads] split: option.splits)[1] (* slow: ca 1min *)
   apply(auto simp add: get_child_nodescharacter_data_ptr_def intro: reads_subset[OF check_in_heap_reads] 
      intro!: reads_bind_pure  reads_subset[OF return_reads] )[1]
  apply(auto simp add: get_child_nodeselement_ptr_def intro: reads_subset[OF reads_singleton] 
      reads_subset[OF check_in_heap_reads] intro!: reads_bind_pure  reads_subset[OF return_reads] 
      split: option.splits)[1]
  done
end

locale l_get_child_nodes = l_type_wf + l_known_ptr + l_get_child_nodes_defs +
  assumes get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
  assumes get_child_nodes_ok: "type_wf h  known_ptr ptr  ptr |∈| object_ptr_kinds h 
                                          h  ok (get_child_nodes ptr)"
  assumes get_child_nodes_ptr_in_heap: "h  ok (get_child_nodes ptr)  ptr |∈| object_ptr_kinds h"
  assumes get_child_nodes_pure [simp]: "pure (get_child_nodes ptr) h"

global_interpretation l_get_child_nodesCore_DOM_defs defines
  get_child_nodes = l_get_child_nodesCore_DOM_defs.a_get_child_nodes and
  get_child_nodes_locs = l_get_child_nodesCore_DOM_defs.a_get_child_nodes_locs
  .

interpretation
  i_get_child_nodes?: l_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  by(auto simp add: l_get_child_nodesCore_DOM_def get_child_nodes_def get_child_nodes_locs_def)
declare l_get_child_nodesCore_DOM_axioms[instances]

lemma get_child_nodes_is_l_get_child_nodes [instances]: 
  "l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  apply(unfold_locales)
  using get_child_nodes_reads get_child_nodes_ok get_child_nodes_ptr_in_heap get_child_nodes_pure
  by blast+


paragraph ‹new\_element›

locale l_new_element_get_child_nodesCore_DOM =
  l_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  for type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  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 get_child_nodes_new_element: 
  "ptr'  cast new_element_ptr  h  new_element r new_element_ptr  h  new_element h h' 
      r  get_child_nodes_locs ptr'  r h h'"
  by (auto simp add: get_child_nodes_locs_def new_element_get_MObject new_element_get_MElement 
                     new_element_get_MDocument split: prod.splits if_splits option.splits 
           elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)

lemma new_element_no_child_nodes:
  "h  new_element r new_element_ptr  h  new_element h h' 
    h'  get_child_nodes (cast new_element_ptr) r []"
  apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def 
      split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
  apply(split invoke_splits, rule conjI)+
     apply(auto intro: new_element_is_element_ptr)[1]
  by(auto simp add: new_element_ptr_in_heap get_child_nodeselement_ptr_def check_in_heap_def 
      new_element_child_nodes intro!: bind_pure_returns_result_I 
      intro: new_element_is_element_ptr elim!: new_element_ptr_in_heap)
end

locale l_new_element_get_child_nodes = l_new_element + l_get_child_nodes +
  assumes get_child_nodes_new_element:  
          "ptr'  cast new_element_ptr  h  new_element r new_element_ptr 
             h  new_element h h'  r  get_child_nodes_locs ptr'  r h h'"
        assumes new_element_no_child_nodes: 
          "h  new_element r new_element_ptr  h  new_element h h' 
             h'  get_child_nodes (cast new_element_ptr) r []"

interpretation i_new_element_get_child_nodes?:
  l_new_element_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  by(unfold_locales)
declare l_new_element_get_child_nodesCore_DOM_axioms[instances]

lemma new_element_get_child_nodes_is_l_new_element_get_child_nodes [instances]: 
  "l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  using new_element_is_l_new_element get_child_nodes_is_l_get_child_nodes
  apply(auto simp add: l_new_element_get_child_nodes_def l_new_element_get_child_nodes_axioms_def)[1]
  using get_child_nodes_new_element new_element_no_child_nodes
  by fast+


paragraph ‹new\_character\_data›

locale l_new_character_data_get_child_nodesCore_DOM =
  l_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  for type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  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 get_child_nodes_new_character_data: 
  "ptr'  cast new_character_data_ptr  h  new_character_data r new_character_data_ptr 
    h  new_character_data h h'  r  get_child_nodes_locs ptr'  r h h'"
  by (auto simp add: get_child_nodes_locs_def new_character_data_get_MObject 
                     new_character_data_get_MElement new_character_data_get_MDocument 
           split: prod.splits if_splits option.splits 
           elim!: bind_returns_result_E bind_returns_heap_E 
           intro: is_character_data_ptr_kind_obtains)

lemma new_character_data_no_child_nodes:
  "h  new_character_data r new_character_data_ptr  h  new_character_data h h' 
   h'  get_child_nodes (cast new_character_data_ptr) r []"
  apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def 
             split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
  apply(split invoke_splits, rule conjI)+
     apply(auto intro: new_character_data_is_character_data_ptr)[1]
  by(auto simp add: new_character_data_ptr_in_heap get_child_nodescharacter_data_ptr_def 
                    check_in_heap_def new_character_data_child_nodes 
          intro!: bind_pure_returns_result_I 
          intro: new_character_data_is_character_data_ptr elim!: new_character_data_ptr_in_heap)
end

locale l_new_character_data_get_child_nodes = l_new_character_data + l_get_child_nodes +
  assumes get_child_nodes_new_character_data:  
   "ptr'  cast new_character_data_ptr  h  new_character_data r new_character_data_ptr 
        h  new_character_data h h'  r  get_child_nodes_locs ptr'  r h h'"
 assumes new_character_data_no_child_nodes: 
  "h  new_character_data r new_character_data_ptr  h  new_character_data h h' 
        h'  get_child_nodes (cast new_character_data_ptr) r []"

interpretation i_new_character_data_get_child_nodes?:
  l_new_character_data_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  by(unfold_locales)
declare l_new_character_data_get_child_nodesCore_DOM_axioms[instances]

lemma new_character_data_get_child_nodes_is_l_new_character_data_get_child_nodes [instances]: 
  "l_new_character_data_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  using new_character_data_is_l_new_character_data get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_new_character_data_get_child_nodes_def l_new_character_data_get_child_nodes_axioms_def)
  using get_child_nodes_new_character_data new_character_data_no_child_nodes
  by fast



paragraph ‹new\_document›

locale l_new_document_get_child_nodesCore_DOM =
  l_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  for type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  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 get_child_nodes_new_document: 
  "ptr'  cast new_document_ptr  h  new_document r new_document_ptr 
      h  new_document h h'  r  get_child_nodes_locs ptr'  r h h'"
  by (auto simp add: get_child_nodes_locs_def new_document_get_MObject new_document_get_MElement
                     new_document_get_MDocument split: prod.splits if_splits option.splits 
           elim!: bind_returns_result_E bind_returns_heap_E 
           intro: is_document_ptr_kind_obtains)

lemma new_document_no_child_nodes:
  "h  new_document r new_document_ptr  h  new_document h h' 
      h'  get_child_nodes (cast new_document_ptr) r []"
  apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def 
      split: prod.splits 
      elim!: bind_returns_result_E bind_returns_heap_E)[1]
  apply(split invoke_splits, rule conjI)+
     apply(auto intro: new_document_is_document_ptr)[1]
  by(auto simp add: new_document_ptr_in_heap get_child_nodesdocument_ptr_def check_in_heap_def 
      new_document_document_element 
      intro!: bind_pure_returns_result_I 
      intro: new_document_is_document_ptr elim!: new_document_ptr_in_heap split: option.splits)
end

locale l_new_document_get_child_nodes = l_new_document + l_get_child_nodes +
  assumes get_child_nodes_new_document:  
   "ptr'  cast new_document_ptr  h  new_document r new_document_ptr 
      h  new_document h h'  r  get_child_nodes_locs ptr'  r h h'"
 assumes new_document_no_child_nodes: 
   "h  new_document r new_document_ptr  h  new_document h h' 
      h'  get_child_nodes (cast new_document_ptr) r []"

interpretation i_new_document_get_child_nodes?:
  l_new_document_get_child_nodesCore_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
  by(unfold_locales)
declare l_new_document_get_child_nodesCore_DOM_axioms[instances]

lemma new_document_get_child_nodes_is_l_new_document_get_child_nodes [instances]: 
  "l_new_document_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
  using new_document_is_l_new_document get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_new_document_get_child_nodes_def l_new_document_get_child_nodes_axioms_def)
  using get_child_nodes_new_document new_document_no_child_nodes
  by fast

subsubsection ‹set\_child\_nodes›

locale l_set_child_nodesCore_DOM_defs
begin
definition set_child_nodeselement_ptr :: 
  "(_) element_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
  "set_child_nodeselement_ptr element_ptr children = put_M element_ptr RElement.child_nodes_update children"

definition set_child_nodescharacter_data_ptr :: 
  "(_) character_data_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
    "set_child_nodescharacter_data_ptr _ _ =  error HierarchyRequestError"

definition set_child_nodesdocument_ptr :: "(_) document_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
    "set_child_nodesdocument_ptr document_ptr children = do {
      (case children of
        []  put_M document_ptr document_element_update None
      | child # []  (case cast child of
          Some element_ptr  put_M document_ptr document_element_update (Some element_ptr)
        | None  error HierarchyRequestError)
      | _  error HierarchyRequestError)
    }"

definition a_set_child_nodes_tups :: 
  "(((_) object_ptr  bool) × ((_) object_ptr  (_) node_ptr list  (_, unit) dom_prog)) list"
  where
    "a_set_child_nodes_tups  [
        (is_element_ptr, set_child_nodeselement_ptr  the  cast),
        (is_character_data_ptr, set_child_nodescharacter_data_ptr  the  cast),
        (is_document_ptr, set_child_nodesdocument_ptr  the  cast)
     ]"

definition a_set_child_nodes :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
    "a_set_child_nodes ptr children = invoke a_set_child_nodes_tups ptr (children)"
lemmas set_child_nodes_defs = a_set_child_nodes_def

definition a_set_child_nodes_locs :: "(_) object_ptr  (_, unit) dom_prog set"
  where
    "a_set_child_nodes_locs ptr  
      (if is_element_ptr_kind ptr 
          then all_args (put_MElement (the (cast ptr)) RElement.child_nodes_update) else {}) 
      (if is_document_ptr_kind ptr 
          then all_args (put_MDocument (the (cast ptr)) document_element_update) else {})"
end

locale l_set_child_nodes_defs =
  fixes set_child_nodes :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
  fixes set_child_nodes_locs :: "(_) object_ptr  (_, unit) dom_prog set"

locale l_set_child_nodesCore_DOM =
  l_type_wf type_wf +
  l_known_ptr known_ptr + 
  l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
  l_set_child_nodesCore_DOM_defs 
  for type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  and set_child_nodes :: "(_) object_ptr  (_) node_ptr list  (_, unit) dom_prog"
  and set_child_nodes_locs :: "(_) object_ptr  (_, unit) dom_prog set" +
  assumes known_ptr_impl: "known_ptr = DocumentClass.known_ptr"
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes set_child_nodes_impl: "set_child_nodes = a_set_child_nodes"
  assumes set_child_nodes_locs_impl: "set_child_nodes_locs = a_set_child_nodes_locs"
begin
lemmas set_child_nodes_def = set_child_nodes_impl[unfolded a_set_child_nodes_def]
lemmas set_child_nodes_locs_def = set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def]

lemma set_child_nodes_split:
  "P (invoke (a_set_child_nodes_tups @ xs) ptr (children)) =
    ((known_ptr ptr  P (set_child_nodes ptr children))
     (¬(known_ptr ptr)  P (invoke xs ptr (children))))"
  by(auto simp add: known_ptr_impl set_child_nodes_impl a_set_child_nodes_def 
          a_set_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs 
          ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: invoke_splits)

lemma set_child_nodes_split_asm:
  "P (invoke (a_set_child_nodes_tups @ xs) ptr (children)) =
    (¬((known_ptr ptr  ¬P (set_child_nodes ptr children))
     (¬(known_ptr ptr)  ¬P (invoke xs ptr (children)))))"
  by(auto simp add: known_ptr_impl set_child_nodes_impl a_set_child_nodes_def 
             a_set_child_nodes_tups_def known_ptr_defs CharacterDataClass.known_ptr_defs 
             ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: invoke_splits)[1]
lemmas set_child_nodes_splits = set_child_nodes_split set_child_nodes_split_asm

lemma set_child_nodes_writes: "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
  apply(simp add: set_child_nodes_locs_impl set_child_nodes_impl a_set_child_nodes_def 
      a_set_child_nodes_tups_def a_set_child_nodes_locs_def)
  apply(split invoke_splits, rule conjI)+
     apply(auto)[1]
    apply(auto simp add: set_child_nodesdocument_ptr_def intro!: writes_bind_pure 
      intro: writes_union_right_I split: list.splits)[1] 
        apply(auto intro: writes_union_right_I split: option.splits)[1]
       apply(auto intro: writes_union_right_I split: option.splits)[1]
      apply(auto intro: writes_union_right_I split: option.splits)[1]
     apply(auto intro: writes_union_right_I split: option.splits)[1]
    apply(auto intro: writes_union_right_I split: option.splits)[1]
   apply(auto intro: writes_union_right_I split: option.splits)[1] (*slow: ca. 1min *)
  apply(auto simp add: set_child_nodescharacter_data_ptr_def intro!: writes_bind_pure)[1]
  apply(auto simp add: set_child_nodeselement_ptr_def intro: writes_union_left_I 
      intro!: writes_bind_pure split: list.splits option.splits)[1]
  done

lemma set_child_nodes_pointers_preserved:
  assumes "w  set_child_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: set_child_nodes_locs_impl all_args_def a_set_child_nodes_locs_def 
          split: if_splits)

lemma set_child_nodes_typess_preserved:
  assumes "w  set_child_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: set_child_nodes_locs_impl type_wf_impl all_args_def a_set_child_nodes_locs_def
          split: if_splits)
end

locale l_set_child_nodes = l_type_wf + l_set_child_nodes_defs +
  assumes set_child_nodes_writes: 
   "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
 assumes set_child_nodes_pointers_preserved: 
   "w  set_child_nodes_locs object_ptr  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
 assumes set_child_nodes_types_preserved: 
   "w  set_child_nodes_locs object_ptr  h  w h h'  type_wf h = type_wf h'"

global_interpretation l_set_child_nodesCore_DOM_defs defines
  set_child_nodes = l_set_child_nodesCore_DOM_defs.a_set_child_nodes and
  set_child_nodes_locs = l_set_child_nodesCore_DOM_defs.a_set_child_nodes_locs .

interpretation
  i_set_child_nodes?: l_set_child_nodesCore_DOM type_wf known_ptr set_child_nodes set_child_nodes_locs
  apply(unfold_locales)
  by (auto simp add: set_child_nodes_def set_child_nodes_locs_def)
declare l_set_child_nodesCore_DOM_axioms[instances]


lemma set_child_nodes_is_l_set_child_nodes [instances]: 
  "l_set_child_nodes type_wf set_child_nodes set_child_nodes_locs"
  apply(unfold_locales)
  using set_child_nodes_pointers_preserved set_child_nodes_typess_preserved set_child_nodes_writes
  by blast+


paragraph ‹get\_child\_nodes›

locale l_set_child_nodes_get_child_nodesCore_DOM = l_get_child_nodesCore_DOM + l_set_child_nodesCore_DOM
begin

lemma set_child_nodes_get_child_nodes:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "h  set_child_nodes ptr children h h'"
  shows "h'  get_child_nodes ptr r children"
proof -
  have "h  check_in_heap ptr r ()"
    using assms set_child_nodes_impl[unfolded a_set_child_nodes_def] invoke_ptr_in_heap
    by (metis (full_types) check_in_heap_ptr_in_heap is_OK_returns_heap_I is_OK_returns_result_E 
        old.unit.exhaust)
  then have ptr_in_h: "ptr |∈| object_ptr_kinds h"
    by (simp add: check_in_heap_ptr_in_heap is_OK_returns_result_I)

  have "type_wf h'"
    apply(unfold type_wf_impl)
    apply(rule subst[where P=id, OF type_wf_preserved[OF set_child_nodes_writes assms(3), 
            unfolded all_args_def], simplified])
    by(auto simp add: all_args_def assms(2)[unfolded type_wf_impl] 
        set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def]
        split: if_splits)
  have "h'  check_in_heap ptr r ()"
    using check_in_heap_reads set_child_nodes_writes assms(3) h  check_in_heap ptr r () 
    apply(rule reads_writes_separate_forwards)
    by(auto simp add: all_args_def set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def])
  then have "ptr |∈| object_ptr_kinds h'"
    using check_in_heap_ptr_in_heap by blast
  with assms ptr_in_h type_wf h' show ?thesis
    apply(auto simp add: get_child_nodes_impl set_child_nodes_impl type_wf_impl known_ptr_impl  
        a_get_child_nodes_def a_get_child_nodes_tups_def a_set_child_nodes_def 
        a_set_child_nodes_tups_def 
        del: bind_pure_returns_result_I2 
        intro!: bind_pure_returns_result_I2)[1]
    apply(split invoke_splits, rule conjI)
     apply(split invoke_splits, rule conjI)
      apply(split invoke_splits, rule conjI)
       apply(auto simp add: NodeClass.known_ptr_defs 
        dest!: known_ptr_not_document_ptr known_ptr_not_character_data_ptr 
        known_ptr_not_element_ptr)[1]                                                                                                                             
      apply(auto simp add: NodeClass.known_ptr_defs 
        dest!: known_ptr_not_document_ptr known_ptr_not_character_data_ptr 
        known_ptr_not_element_ptr)[1]                                                                                                                             
      apply(auto simp add: get_child_nodesdocument_ptr_def set_child_nodesdocument_ptr_def get_MDocument_ok
        split: list.splits option.splits 
        intro!: bind_pure_returns_result_I2 
        dest: get_MDocument_ok; auto dest: returns_result_eq 
        dest!: document_put_get[where getter = document_element])[1] (* slow, ca 1min *)
     apply(auto simp add: get_child_nodescharacter_data_ptr_def set_child_nodescharacter_data_ptr_def)[1]
    by(auto simp add: get_child_nodeselement_ptr_def set_child_nodeselement_ptr_def dest: element_put_get)
qed

lemma set_child_nodes_get_child_nodes_different_pointers: 
  assumes "ptr  ptr'"
  assumes "w  set_child_nodes_locs ptr"
  assumes "h  w h h'"   
  assumes "r  get_child_nodes_locs ptr'"
  shows "r h h'"
  using assms
  apply(auto simp add: get_child_nodes_locs_impl set_child_nodes_locs_impl all_args_def 
      a_set_child_nodes_locs_def a_get_child_nodes_locs_def 
      split: if_splits option.splits )[1] 
   apply(rule is_document_ptr_kind_obtains) 
    apply(simp)
   apply(rule is_document_ptr_kind_obtains) 
    apply(auto)[1]
   apply(auto)[1]
  apply(rule is_element_ptr_kind_obtains) 
   apply(auto)[1]
  apply(auto)[1]
  apply(rule is_element_ptr_kind_obtains) 
   apply(auto)[1]
  apply(auto)[1]
  done

lemma set_child_nodes_element_ok [simp]:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "is_element_ptr_kind ptr"
  shows "h  ok (set_child_nodes ptr children)"
proof -
  have "is_element_ptr ptr"
    using known_ptr ptr assms(4)
    by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
  then show ?thesis
    using assms
    apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodeselement_ptr_def
        split: option.splits)[1]
    by (simp add: DocumentMonad.put_MElement_ok local.type_wf_impl)
qed

lemma set_child_nodes_document1_ok [simp]:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "is_document_ptr_kind ptr"
  assumes "children = []"
  shows "h  ok (set_child_nodes ptr children)"
proof -
  have "is_document_ptr ptr"
    using known_ptr ptr assms(4)
    by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
  then show ?thesis
    using assms
    apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodesdocument_ptr_def
        split: option.splits)[1]
    by (simp add: DocumentMonad.put_MDocument_ok local.type_wf_impl)
qed

lemma set_child_nodes_document2_ok [simp]:
  assumes "known_ptr ptr"
  assumes "type_wf h"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "is_document_ptr_kind ptr"
  assumes "children = [child]"
  assumes "is_element_ptr_kind child"
  shows "h  ok (set_child_nodes ptr children)"
proof -
  have "is_document_ptr ptr"
    using known_ptr ptr assms(4)
    by(auto simp add: known_ptr_impl known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs NodeClass.known_ptr_defs split: option.splits)
  then show ?thesis
    using assms
    apply(auto simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodesdocument_ptr_def)[1]
    apply(split invoke_splits, rule conjI)+
       apply(auto simp add: is_element_ptr_kindnode_ptr_def set_child_nodesdocument_ptr_def split: option.splits)[1]
      apply(auto simp add: is_element_ptr_kindnode_ptr_def set_child_nodesdocument_ptr_def split: option.splits)[1]
      apply (simp add: local.type_wf_impl put_MDocument_ok)
     apply(auto simp add: is_element_ptr_kindnode_ptr_def set_child_nodesdocument_ptr_def split: option.splits)[1]
    by(auto simp add: is_element_ptr_kindnode_ptr_def set_child_nodesdocument_ptr_def split: option.splits)[1]
qed
end

locale l_set_child_nodes_get_child_nodes = l_get_child_nodes + l_set_child_nodes +
  assumes set_child_nodes_get_child_nodes: 
    "type_wf h  known_ptr ptr 
                h  set_child_nodes ptr children h h'  h'  get_child_nodes ptr r children"
  assumes set_child_nodes_get_child_nodes_different_pointers: 
    "ptr  ptr'  w  set_child_nodes_locs ptr  h  w h h' 
                 r  get_child_nodes_locs ptr'  r h h'"

interpretation
  i_set_child_nodes_get_child_nodes?: l_set_child_nodes_get_child_nodesCore_DOM type_wf 
  known_ptr get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs
  by unfold_locales
declare l_set_child_nodes_get_child_nodesCore_DOM_axioms[instances]

lemma set_child_nodes_get_child_nodes_is_l_set_child_nodes_get_child_nodes [instances]: 
  "l_set_child_nodes_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs 
                                     set_child_nodes set_child_nodes_locs"
  using get_child_nodes_is_l_get_child_nodes set_child_nodes_is_l_set_child_nodes
  apply(auto simp add: l_set_child_nodes_get_child_nodes_def l_set_child_nodes_get_child_nodes_axioms_def)[1]
  using set_child_nodes_get_child_nodes apply blast
  using set_child_nodes_get_child_nodes_different_pointers apply metis
  done


subsubsection ‹get\_attribute›

locale l_get_attributeCore_DOM_defs
begin
definition a_get_attribute :: "(_) element_ptr  attr_key  (_, attr_value option) dom_prog"
  where
    "a_get_attribute ptr k = do {m  get_M ptr attrs; return (fmlookup m k)}"
lemmas get_attribute_defs = a_get_attribute_def

definition a_get_attribute_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
  where
    "a_get_attribute_locs element_ptr = {preserved (get_M element_ptr attrs)}"
end

locale l_get_attribute_defs =
  fixes get_attribute :: "(_) element_ptr  attr_key  (_, attr_value option) dom_prog"
  fixes get_attribute_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"

locale l_get_attributeCore_DOM =
  l_type_wf type_wf +
  l_get_attribute_defs get_attribute get_attribute_locs +
  l_get_attributeCore_DOM_defs
  for type_wf :: "(_) heap  bool"
  and get_attribute :: "(_) element_ptr  attr_key  (_, attr_value option) dom_prog"
  and get_attribute_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes get_attribute_impl: "get_attribute = a_get_attribute"
  assumes get_attribute_locs_impl: "get_attribute_locs = a_get_attribute_locs"
begin
lemma get_attribute_pure [simp]: "pure (get_attribute ptr k) h"
  by (auto simp add: bind_pure_I get_attribute_impl[unfolded a_get_attribute_def])

lemma get_attribute_ok: 
  "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_attribute element_ptr k)"
  apply(unfold type_wf_impl)
  unfolding get_attribute_impl[unfolded a_get_attribute_def] using get_MElement_ok
  by (metis bind_is_OK_pure_I return_ok ElementMonad.get_M_pure)
    
lemma get_attribute_ptr_in_heap: 
  "h  ok (get_attribute element_ptr k)  element_ptr |∈| element_ptr_kinds h"
  unfolding get_attribute_impl[unfolded a_get_attribute_def]
  by (meson DocumentMonad.get_MElement_ptr_in_heap bind_is_OK_E is_OK_returns_result_I)

lemma get_attribute_reads: 
  "reads (get_attribute_locs element_ptr) (get_attribute element_ptr k) h h'"
  by(auto simp add: get_attribute_impl[unfolded a_get_attribute_def] 
                    get_attribute_locs_impl[unfolded a_get_attribute_locs_def] 
                    reads_insert_writes_set_right 
          intro!: reads_bind_pure)
end

locale l_get_attribute = l_type_wf + l_get_attribute_defs +
assumes get_attribute_reads: 
  "reads (get_attribute_locs element_ptr) (get_attribute element_ptr k) h h'"
assumes get_attribute_ok: 
  "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_attribute element_ptr k)"
assumes get_attribute_ptr_in_heap: 
  "h  ok (get_attribute element_ptr k)  element_ptr |∈| element_ptr_kinds h"
assumes get_attribute_pure [simp]: "pure (get_attribute element_ptr k) h"

global_interpretation l_get_attributeCore_DOM_defs defines
  get_attribute = l_get_attributeCore_DOM_defs.a_get_attribute and
  get_attribute_locs = l_get_attributeCore_DOM_defs.a_get_attribute_locs .

interpretation
  i_get_attribute?: l_get_attributeCore_DOM type_wf get_attribute get_attribute_locs
  apply(unfold_locales)
  by (auto simp add: get_attribute_def get_attribute_locs_def)
declare l_get_attributeCore_DOM_axioms[instances]

lemma get_attribute_is_l_get_attribute [instances]: 
  "l_get_attribute type_wf get_attribute get_attribute_locs"
  apply(unfold_locales)
  using get_attribute_reads get_attribute_ok get_attribute_ptr_in_heap get_attribute_pure
  by blast+


subsubsection ‹set\_attribute›

locale l_set_attributeCore_DOM_defs
begin

definition 
  a_set_attribute :: "(_) element_ptr  attr_key  attr_value option  (_, unit) dom_prog"
  where
    "a_set_attribute ptr k v = do {
      m  get_M ptr attrs;
      put_M ptr attrs_update (if v = None then fmdrop k m else fmupd k (the v) m)
    }"

definition a_set_attribute_locs :: "(_) element_ptr  (_, unit) dom_prog set"
  where
    "a_set_attribute_locs element_ptr  all_args (put_M element_ptr attrs_update)"
end

locale l_set_attribute_defs =
  fixes set_attribute :: "(_) element_ptr  attr_key  attr_value option  (_, unit) dom_prog"
  fixes set_attribute_locs :: "(_) element_ptr  (_, unit) dom_prog set"

locale l_set_attributeCore_DOM =
  l_type_wf type_wf +
  l_set_attribute_defs set_attribute set_attribute_locs +
  l_set_attributeCore_DOM_defs
  for type_wf :: "(_) heap  bool"
  and set_attribute :: "(_) element_ptr  attr_key  attr_value option  (_, unit) dom_prog"
  and set_attribute_locs :: "(_) element_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes set_attribute_impl: "set_attribute = a_set_attribute"
  assumes set_attribute_locs_impl: "set_attribute_locs = a_set_attribute_locs"
begin
lemmas set_attribute_def = set_attribute_impl[folded a_set_attribute_def]
lemmas set_attribute_locs_def = set_attribute_locs_impl[unfolded a_set_attribute_locs_def]

lemma set_attribute_ok: "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_attribute element_ptr k v)"
  apply(unfold type_wf_impl)
  unfolding set_attribute_impl[unfolded a_set_attribute_def] using get_MElement_ok put_MElement_ok
  by(metis (no_types, lifting) DocumentClass.type_wfElement ElementMonad.get_M_pure bind_is_OK_E 
                               bind_is_OK_pure_I is_OK_returns_result_I)

lemma set_attribute_writes: 
  "writes (set_attribute_locs element_ptr) (set_attribute element_ptr k v) h h'"
  by(auto simp add: set_attribute_impl[unfolded a_set_attribute_def] 
                    set_attribute_locs_impl[unfolded a_set_attribute_locs_def] 
          intro: writes_bind_pure)
end

locale l_set_attribute = l_type_wf + l_set_attribute_defs +
  assumes set_attribute_writes: 
    "writes (set_attribute_locs element_ptr) (set_attribute element_ptr k v) h h'"
  assumes set_attribute_ok: 
    "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_attribute element_ptr k v)"

global_interpretation l_set_attributeCore_DOM_defs defines
  set_attribute = l_set_attributeCore_DOM_defs.a_set_attribute and
  set_attribute_locs = l_set_attributeCore_DOM_defs.a_set_attribute_locs .
interpretation 
  i_set_attribute?: l_set_attributeCore_DOM type_wf set_attribute set_attribute_locs
  apply(unfold_locales)
  by (auto simp add: set_attribute_def set_attribute_locs_def)
declare l_set_attributeCore_DOM_axioms[instances]

lemma set_attribute_is_l_set_attribute [instances]: 
  "l_set_attribute type_wf set_attribute set_attribute_locs"
  apply(unfold_locales)
  using set_attribute_ok set_attribute_writes
  by blast+


paragraph ‹get\_attribute›

locale l_set_attribute_get_attributeCore_DOM =
  l_get_attributeCore_DOM +
  l_set_attributeCore_DOM
begin

lemma set_attribute_get_attribute:
  "h  set_attribute ptr k v h h'  h'  get_attribute ptr k r v"
  by(auto simp add: set_attribute_impl[unfolded a_set_attribute_def] 
                    get_attribute_impl[unfolded a_get_attribute_def] 
          elim!: bind_returns_heap_E2 
          intro!: bind_pure_returns_result_I 
          elim: element_put_get)
end

locale l_set_attribute_get_attribute = l_get_attribute + l_set_attribute +
  assumes set_attribute_get_attribute:
    "h  set_attribute ptr k v h h'  h'  get_attribute ptr k r v"

interpretation
  i_set_attribute_get_attribute?: l_set_attribute_get_attributeCore_DOM type_wf 
                                  get_attribute get_attribute_locs set_attribute set_attribute_locs
  by(unfold_locales)
declare l_set_attribute_get_attributeCore_DOM_axioms[instances]

lemma set_attribute_get_attribute_is_l_set_attribute_get_attribute [instances]: 
  "l_set_attribute_get_attribute type_wf get_attribute get_attribute_locs set_attribute set_attribute_locs"
  using get_attribute_is_l_get_attribute set_attribute_is_l_set_attribute
  apply(simp add: l_set_attribute_get_attribute_def l_set_attribute_get_attribute_axioms_def)
  using set_attribute_get_attribute
  by blast

paragraph ‹get\_child\_nodes›

locale l_set_attribute_get_child_nodesCore_DOM =
  l_set_attributeCore_DOM +
  l_get_child_nodesCore_DOM
begin
lemma set_attribute_get_child_nodes:
  "w  set_attribute_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_attribute_locs_def get_child_nodes_locs_def all_args_def 
          intro: element_put_get_preserved[where setter=attrs_update])
end

locale l_set_attribute_get_child_nodes =
  l_set_attribute +
  l_get_child_nodes +
  assumes set_attribute_get_child_nodes: 
         "w  set_attribute_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

interpretation
  i_set_attribute_get_child_nodes?: l_set_attribute_get_child_nodesCore_DOM type_wf 
                    set_attribute set_attribute_locs known_ptr get_child_nodes get_child_nodes_locs
  by unfold_locales
declare l_set_attribute_get_child_nodesCore_DOM_axioms[instances]

lemma set_attribute_get_child_nodes_is_l_set_attribute_get_child_nodes [instances]:
  "l_set_attribute_get_child_nodes type_wf set_attribute set_attribute_locs known_ptr 
                                   get_child_nodes get_child_nodes_locs"
  using set_attribute_is_l_set_attribute get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_attribute_get_child_nodes_def l_set_attribute_get_child_nodes_axioms_def)
  using set_attribute_get_child_nodes
  by blast


subsubsection ‹get\_disconnected\_nodes›

locale l_get_disconnected_nodesCore_DOM_defs
begin
definition a_get_disconnected_nodes :: "(_) document_ptr
     (_, (_) node_ptr list) dom_prog"
  where
    "a_get_disconnected_nodes document_ptr = get_M document_ptr disconnected_nodes"
lemmas get_disconnected_nodes_defs = a_get_disconnected_nodes_def

definition a_get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"
  where
    "a_get_disconnected_nodes_locs document_ptr = {preserved (get_M document_ptr disconnected_nodes)}"
end

locale l_get_disconnected_nodes_defs = 
  fixes get_disconnected_nodes :: "(_) document_ptr  (_, (_) node_ptr list) dom_prog"
  fixes get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"

locale l_get_disconnected_nodesCore_DOM =
  l_type_wf type_wf +
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_get_disconnected_nodesCore_DOM_defs
  for 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" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes get_disconnected_nodes_impl: "get_disconnected_nodes = a_get_disconnected_nodes"
  assumes get_disconnected_nodes_locs_impl: "get_disconnected_nodes_locs = a_get_disconnected_nodes_locs"
begin
lemmas 
  get_disconnected_nodes_def = get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def]
lemmas 
  get_disconnected_nodes_locs_def = get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def]

lemma get_disconnected_nodes_ok: 
  "type_wf h  document_ptr |∈| document_ptr_kinds h  h  ok (get_disconnected_nodes document_ptr)"
  apply(unfold type_wf_impl)
  unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def] using get_MDocument_ok
  by fast

lemma get_disconnected_nodes_ptr_in_heap: 
  "h  ok (get_disconnected_nodes document_ptr)  document_ptr |∈| document_ptr_kinds h"
  unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def]
  by (simp add: DocumentMonad.get_M_ptr_in_heap)

lemma get_disconnected_nodes_pure [simp]: "pure (get_disconnected_nodes document_ptr) h"
  unfolding get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def] by simp

lemma get_disconnected_nodes_reads: 
  "reads (get_disconnected_nodes_locs document_ptr) (get_disconnected_nodes document_ptr) h h'"
  by(simp add: get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def] 
               get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def] 
               reads_bind_pure reads_insert_writes_set_right)
end

locale l_get_disconnected_nodes = l_type_wf + l_get_disconnected_nodes_defs +
  assumes get_disconnected_nodes_reads: 
    "reads (get_disconnected_nodes_locs document_ptr) (get_disconnected_nodes document_ptr) h h'"
  assumes get_disconnected_nodes_ok: 
    "type_wf h  document_ptr |∈| document_ptr_kinds h  h  ok (get_disconnected_nodes document_ptr)"
  assumes get_disconnected_nodes_ptr_in_heap: 
    "h  ok (get_disconnected_nodes document_ptr)  document_ptr |∈| document_ptr_kinds h"
  assumes get_disconnected_nodes_pure [simp]: 
   "pure (get_disconnected_nodes document_ptr) h"

global_interpretation l_get_disconnected_nodesCore_DOM_defs defines
  get_disconnected_nodes = l_get_disconnected_nodesCore_DOM_defs.a_get_disconnected_nodes and
  get_disconnected_nodes_locs = l_get_disconnected_nodesCore_DOM_defs.a_get_disconnected_nodes_locs .
interpretation 
  i_get_disconnected_nodes?: l_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes 
                             get_disconnected_nodes_locs
  apply(unfold_locales)
  by (auto simp add: get_disconnected_nodes_def get_disconnected_nodes_locs_def)
declare l_get_disconnected_nodesCore_DOM_axioms[instances]

lemma get_disconnected_nodes_is_l_get_disconnected_nodes [instances]: 
  "l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs"
  apply(simp add: l_get_disconnected_nodes_def)
  using get_disconnected_nodes_reads get_disconnected_nodes_ok get_disconnected_nodes_ptr_in_heap 
        get_disconnected_nodes_pure
  by blast+


paragraph ‹set\_child\_nodes›

locale l_set_child_nodes_get_disconnected_nodesCore_DOM =
  l_set_child_nodesCore_DOM +
  CD: l_get_disconnected_nodesCore_DOM
begin
lemma set_child_nodes_get_disconnected_nodes: 
  "w  a_set_child_nodes_locs ptr. (h  w h h'  (r  a_get_disconnected_nodes_locs ptr'. r h h'))"
  by(auto simp add: a_set_child_nodes_locs_def a_get_disconnected_nodes_locs_def all_args_def)
end

locale l_set_child_nodes_get_disconnected_nodes = l_set_child_nodes + l_get_disconnected_nodes +
  assumes set_child_nodes_get_disconnected_nodes: 
  "w  set_child_nodes_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"

interpretation
  i_set_child_nodes_get_disconnected_nodes?: l_set_child_nodes_get_disconnected_nodesCore_DOM type_wf 
                                             known_ptr set_child_nodes set_child_nodes_locs 
                                             get_disconnected_nodes get_disconnected_nodes_locs
  by(unfold_locales)
declare l_set_child_nodes_get_disconnected_nodesCore_DOM_axioms[instances]

lemma set_child_nodes_get_disconnected_nodes_is_l_set_child_nodes_get_disconnected_nodes [instances]:
  "l_set_child_nodes_get_disconnected_nodes type_wf set_child_nodes set_child_nodes_locs 
                                            get_disconnected_nodes get_disconnected_nodes_locs"
  using set_child_nodes_is_l_set_child_nodes get_disconnected_nodes_is_l_get_disconnected_nodes
  apply(simp add: l_set_child_nodes_get_disconnected_nodes_def 
                  l_set_child_nodes_get_disconnected_nodes_axioms_def)
  using set_child_nodes_get_disconnected_nodes
  by fast


paragraph ‹set\_attribute›

locale l_set_attribute_get_disconnected_nodesCore_DOM =
  l_set_attributeCore_DOM +
  l_get_disconnected_nodesCore_DOM
begin
lemma set_attribute_get_disconnected_nodes: 
  "w  a_set_attribute_locs ptr. (h  w h h'  (r  a_get_disconnected_nodes_locs ptr'. r h h'))"
  by(auto simp add: a_set_attribute_locs_def a_get_disconnected_nodes_locs_def all_args_def)
end

locale l_set_attribute_get_disconnected_nodes = l_set_attribute + l_get_disconnected_nodes +
  assumes set_attribute_get_disconnected_nodes: 
  "w  set_attribute_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"

interpretation
  i_set_attribute_get_disconnected_nodes?: l_set_attribute_get_disconnected_nodesCore_DOM type_wf 
                set_attribute set_attribute_locs get_disconnected_nodes get_disconnected_nodes_locs
  by(unfold_locales)
declare l_set_attribute_get_disconnected_nodesCore_DOM_axioms[instances]

lemma set_attribute_get_disconnected_nodes_is_l_set_attribute_get_disconnected_nodes [instances]:
  "l_set_attribute_get_disconnected_nodes type_wf set_attribute set_attribute_locs 
                                          get_disconnected_nodes get_disconnected_nodes_locs"
  using set_attribute_is_l_set_attribute get_disconnected_nodes_is_l_get_disconnected_nodes
  apply(simp add: l_set_attribute_get_disconnected_nodes_def 
                  l_set_attribute_get_disconnected_nodes_axioms_def)
  using set_attribute_get_disconnected_nodes
  by fast


paragraph ‹new\_element›

locale l_new_element_get_disconnected_nodesCore_DOM =
  l_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes get_disconnected_nodes_locs
  for 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"
begin
lemma get_disconnected_nodes_new_element:  
   "h  new_element r new_element_ptr  h  new_element h h'
         r  get_disconnected_nodes_locs ptr'  r h h'"
  by(auto simp add: get_disconnected_nodes_locs_def new_element_get_MDocument)
end

locale l_new_element_get_disconnected_nodes = l_get_disconnected_nodes_defs +
  assumes get_disconnected_nodes_new_element:  
   "h  new_element r new_element_ptr  h  new_element h h'
         r  get_disconnected_nodes_locs ptr'  r h h'"

interpretation i_new_element_get_disconnected_nodes?: 
  l_new_element_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes 
  get_disconnected_nodes_locs
  by unfold_locales
declare l_new_element_get_disconnected_nodesCore_DOM_axioms[instances]

lemma new_element_get_disconnected_nodes_is_l_new_element_get_disconnected_nodes [instances]:
  "l_new_element_get_disconnected_nodes get_disconnected_nodes_locs"
  by (simp add: get_disconnected_nodes_new_element l_new_element_get_disconnected_nodes_def)


paragraph ‹new\_character\_data›

locale l_new_character_data_get_disconnected_nodesCore_DOM =
  l_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes get_disconnected_nodes_locs
  for 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"
begin
lemma get_disconnected_nodes_new_character_data:  
  "h  new_character_data r new_character_data_ptr  h  new_character_data h h'
        r  get_disconnected_nodes_locs ptr'  r h h'"
  by(auto simp add: get_disconnected_nodes_locs_def new_character_data_get_MDocument)
end

locale l_new_character_data_get_disconnected_nodes = l_get_disconnected_nodes_defs +
  assumes get_disconnected_nodes_new_character_data:  
  "h  new_character_data r new_character_data_ptr  h  new_character_data h h'
        r  get_disconnected_nodes_locs ptr'  r h h'"

interpretation i_new_character_data_get_disconnected_nodes?: 
  l_new_character_data_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes 
                                                    get_disconnected_nodes_locs
  by unfold_locales
declare l_new_character_data_get_disconnected_nodesCore_DOM_axioms[instances]

lemma new_character_data_get_disconnected_nodes_is_l_new_character_data_get_disconnected_nodes [instances]:
  "l_new_character_data_get_disconnected_nodes get_disconnected_nodes_locs"
  by (simp add: get_disconnected_nodes_new_character_data l_new_character_data_get_disconnected_nodes_def)


paragraph ‹new\_document›

locale l_new_document_get_disconnected_nodesCore_DOM =
  l_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes get_disconnected_nodes_locs
  for 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"
begin
lemma get_disconnected_nodes_new_document_different_pointers:  
  "new_document_ptr  ptr'  h  new_document r new_document_ptr  h  new_document h h'
     r  get_disconnected_nodes_locs ptr'  r h h'"
  by(auto simp add: get_disconnected_nodes_locs_def new_document_get_MDocument)

lemma new_document_no_disconnected_nodes:
  "h  new_document r new_document_ptr  h  new_document h h' 
      h'  get_disconnected_nodes new_document_ptr r []"
  by(simp add: get_disconnected_nodes_def new_document_disconnected_nodes)
  
end

interpretation i_new_document_get_disconnected_nodes?: 
  l_new_document_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes get_disconnected_nodes_locs
  by unfold_locales
declare l_new_document_get_disconnected_nodesCore_DOM_axioms[instances]

locale l_new_document_get_disconnected_nodes = l_get_disconnected_nodes_defs +
  assumes get_disconnected_nodes_new_document_different_pointers:  
  "new_document_ptr  ptr'  h  new_document r new_document_ptr  h  new_document h h'
     r  get_disconnected_nodes_locs ptr'  r h h'"
  assumes new_document_no_disconnected_nodes:
  "h  new_document r new_document_ptr  h  new_document h h' 
     h'  get_disconnected_nodes new_document_ptr r []"

lemma new_document_get_disconnected_nodes_is_l_new_document_get_disconnected_nodes [instances]:
  "l_new_document_get_disconnected_nodes get_disconnected_nodes get_disconnected_nodes_locs"
  apply (auto simp add: l_new_document_get_disconnected_nodes_def)[1]
  using get_disconnected_nodes_new_document_different_pointers apply fast
  using new_document_no_disconnected_nodes apply blast
  done



subsubsection ‹set\_disconnected\_nodes›

locale l_set_disconnected_nodesCore_DOM_defs
begin

definition a_set_disconnected_nodes :: "(_) document_ptr  (_) node_ptr list  (_, unit) dom_prog"
  where
    "a_set_disconnected_nodes document_ptr disc_nodes =
put_M document_ptr disconnected_nodes_update disc_nodes"
lemmas set_disconnected_nodes_defs = a_set_disconnected_nodes_def

definition a_set_disconnected_nodes_locs :: "(_) document_ptr  (_, unit) dom_prog set"
  where
    "a_set_disconnected_nodes_locs document_ptr  all_args (put_M document_ptr disconnected_nodes_update)"
end

locale l_set_disconnected_nodes_defs =
  fixes set_disconnected_nodes :: "(_) document_ptr  (_) node_ptr list  (_, unit) dom_prog"
  fixes set_disconnected_nodes_locs :: "(_) document_ptr  (_, unit) dom_prog set"

locale l_set_disconnected_nodesCore_DOM =
  l_type_wf type_wf + 
  l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs +
  l_set_disconnected_nodesCore_DOM_defs
  for type_wf :: "(_) heap  bool"
  and set_disconnected_nodes :: "(_) document_ptr  (_) node_ptr list  (_, unit) dom_prog"
  and set_disconnected_nodes_locs :: "(_) document_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes set_disconnected_nodes_impl: "set_disconnected_nodes = a_set_disconnected_nodes"
  assumes set_disconnected_nodes_locs_impl: "set_disconnected_nodes_locs = a_set_disconnected_nodes_locs"
begin
lemmas set_disconnected_nodes_def = set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def]
lemmas set_disconnected_nodes_locs_def =
  set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def]
lemma set_disconnected_nodes_ok:
  "type_wf h  document_ptr |∈| document_ptr_kinds h 
h  ok (set_disconnected_nodes document_ptr node_ptrs)"
  by (simp add: type_wf_impl put_MDocument_ok
      set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def])

lemma set_disconnected_nodes_ptr_in_heap: 
  "h  ok (set_disconnected_nodes document_ptr disc_nodes)  document_ptr |∈| document_ptr_kinds h"
  by (simp add: set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def] 
                DocumentMonad.put_M_ptr_in_heap)

lemma set_disconnected_nodes_writes: 
  "writes (set_disconnected_nodes_locs document_ptr) (set_disconnected_nodes document_ptr disc_nodes) h h'"
  by(auto simp add: set_disconnected_nodes_impl[unfolded a_set_disconnected_nodes_def] 
                    set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def] 
          intro: writes_bind_pure)

lemma set_disconnected_nodes_pointers_preserved:
  assumes "w  set_disconnected_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def  set_disconnected_nodes_locs_impl[unfolded 
                    a_set_disconnected_nodes_locs_def] 
          split: if_splits)

lemma set_disconnected_nodes_typess_preserved:
  assumes "w  set_disconnected_nodes_locs object_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  apply(unfold type_wf_impl)
  by(auto simp add: all_args_def 
                    set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def] 
          split: if_splits)
end

locale l_set_disconnected_nodes = l_type_wf + l_set_disconnected_nodes_defs +
  assumes set_disconnected_nodes_writes: 
    "writes (set_disconnected_nodes_locs document_ptr)
(set_disconnected_nodes document_ptr disc_nodes) h h'"
  assumes set_disconnected_nodes_ok: 
    "type_wf h  document_ptr |∈| document_ptr_kinds h 
h  ok (set_disconnected_nodes document_ptr disc_noded)"
  assumes set_disconnected_nodes_ptr_in_heap: 
    "h  ok (set_disconnected_nodes document_ptr disc_noded) 
document_ptr |∈| document_ptr_kinds h"
  assumes set_disconnected_nodes_pointers_preserved: 
    "w  set_disconnected_nodes_locs document_ptr  h  w h h' 
object_ptr_kinds h = object_ptr_kinds h'"
 assumes set_disconnected_nodes_types_preserved: 
   "w  set_disconnected_nodes_locs document_ptr  h  w h h'  type_wf h = type_wf h'"

global_interpretation l_set_disconnected_nodesCore_DOM_defs defines
  set_disconnected_nodes = l_set_disconnected_nodesCore_DOM_defs.a_set_disconnected_nodes and
  set_disconnected_nodes_locs = l_set_disconnected_nodesCore_DOM_defs.a_set_disconnected_nodes_locs .
interpretation 
  i_set_disconnected_nodes?: l_set_disconnected_nodesCore_DOM type_wf set_disconnected_nodes 
                             set_disconnected_nodes_locs
  apply unfold_locales
  by (auto simp add: set_disconnected_nodes_def set_disconnected_nodes_locs_def)
declare l_set_disconnected_nodesCore_DOM_axioms[instances]

lemma set_disconnected_nodes_is_l_set_disconnected_nodes [instances]: 
  "l_set_disconnected_nodes type_wf set_disconnected_nodes set_disconnected_nodes_locs"
  apply(simp add: l_set_disconnected_nodes_def)
  using set_disconnected_nodes_ok set_disconnected_nodes_writes
    set_disconnected_nodes_pointers_preserved
        set_disconnected_nodes_ptr_in_heap set_disconnected_nodes_typess_preserved
  by blast+


paragraph ‹get\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_disconnected_nodesCore_DOM = l_get_disconnected_nodesCore_DOM 
                                                             + l_set_disconnected_nodesCore_DOM
begin
lemma set_disconnected_nodes_get_disconnected_nodes:
  assumes "h  a_set_disconnected_nodes document_ptr disc_nodes h h'"
  shows "h'  a_get_disconnected_nodes document_ptr r disc_nodes"
  using assms 
  by(auto simp add: a_get_disconnected_nodes_def a_set_disconnected_nodes_def)

lemma set_disconnected_nodes_get_disconnected_nodes_different_pointers: 
  assumes "ptr  ptr'"
  assumes "w  a_set_disconnected_nodes_locs ptr"
  assumes "h  w h h'"   
  assumes "r  a_get_disconnected_nodes_locs ptr'"
  shows "r h h'"
  using assms
  by(auto simp add: all_args_def a_set_disconnected_nodes_locs_def a_get_disconnected_nodes_locs_def 
             split: if_splits option.splits )
end

locale l_set_disconnected_nodes_get_disconnected_nodes = l_get_disconnected_nodes 
                                                       + l_set_disconnected_nodes +
  assumes set_disconnected_nodes_get_disconnected_nodes: 
  "h  set_disconnected_nodes document_ptr disc_nodes h h' 
      h'  get_disconnected_nodes document_ptr r disc_nodes"
  assumes set_disconnected_nodes_get_disconnected_nodes_different_pointers: 
  "ptr  ptr'  w  set_disconnected_nodes_locs ptr  h  w h h' 
     r  get_disconnected_nodes_locs ptr'  r h h'"

interpretation i_set_disconnected_nodes_get_disconnected_nodes?:
  l_set_disconnected_nodes_get_disconnected_nodesCore_DOM type_wf get_disconnected_nodes 
                     get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
  by unfold_locales
declare l_set_disconnected_nodes_get_disconnected_nodesCore_DOM_axioms[instances]

lemma set_disconnected_nodes_get_disconnected_nodes_is_l_set_disconnected_nodes_get_disconnected_nodes
  [instances]:
  "l_set_disconnected_nodes_get_disconnected_nodes  type_wf get_disconnected_nodes get_disconnected_nodes_locs 
                                                    set_disconnected_nodes set_disconnected_nodes_locs"
  using set_disconnected_nodes_is_l_set_disconnected_nodes get_disconnected_nodes_is_l_get_disconnected_nodes
  apply(simp add: l_set_disconnected_nodes_get_disconnected_nodes_def 
                  l_set_disconnected_nodes_get_disconnected_nodes_axioms_def)
  using set_disconnected_nodes_get_disconnected_nodes 
        set_disconnected_nodes_get_disconnected_nodes_different_pointers
  by fast+


paragraph ‹get\_child\_nodes›

locale l_set_disconnected_nodes_get_child_nodesCore_DOM =
  l_set_disconnected_nodesCore_DOM +
  l_get_child_nodesCore_DOM
begin
lemma set_disconnected_nodes_get_child_nodes: 
  "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_disconnected_nodes_locs_impl[unfolded a_set_disconnected_nodes_locs_def] 
                    get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def] all_args_def)
end

locale l_set_disconnected_nodes_get_child_nodes = l_set_disconnected_nodes_defs + l_get_child_nodes_defs +
  assumes set_disconnected_nodes_get_child_nodes [simp]: 
    "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

interpretation
  i_set_disconnected_nodes_get_child_nodes?: l_set_disconnected_nodes_get_child_nodesCore_DOM 
                                             type_wf 
                                             set_disconnected_nodes set_disconnected_nodes_locs 
                                             known_ptr get_child_nodes get_child_nodes_locs
  by unfold_locales
declare l_set_disconnected_nodes_get_child_nodesCore_DOM_axioms[instances]

lemma set_disconnected_nodes_get_child_nodes_is_l_set_disconnected_nodes_get_child_nodes [instances]:
  "l_set_disconnected_nodes_get_child_nodes set_disconnected_nodes_locs get_child_nodes_locs"
  using set_disconnected_nodes_is_l_set_disconnected_nodes get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_disconnected_nodes_get_child_nodes_def)
  using set_disconnected_nodes_get_child_nodes
  by fast


subsubsection ‹get\_tag\_name›

locale l_get_tag_nameCore_DOM_defs
begin
definition a_get_tag_name :: "(_) element_ptr  (_, tag_name) dom_prog"
  where
    "a_get_tag_name element_ptr = get_M element_ptr tag_name"

definition a_get_tag_name_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
  where
    "a_get_tag_name_locs element_ptr  {preserved (get_M element_ptr tag_name)}"
end

locale l_get_tag_name_defs =
  fixes get_tag_name :: "(_) element_ptr  (_, tag_name) dom_prog"
  fixes get_tag_name_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"

locale l_get_tag_nameCore_DOM =
  l_type_wf type_wf +
  l_get_tag_name_defs get_tag_name get_tag_name_locs +
  l_get_tag_nameCore_DOM_defs 
  for type_wf :: "(_) heap  bool"
    and get_tag_name :: "(_) element_ptr  (_, tag_name) dom_prog"
  and get_tag_name_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes get_tag_name_impl: "get_tag_name = a_get_tag_name"
  assumes get_tag_name_locs_impl: "get_tag_name_locs = a_get_tag_name_locs"
begin
lemmas get_tag_name_def = get_tag_name_impl[unfolded a_get_tag_name_def]
lemmas get_tag_name_locs_def = get_tag_name_locs_impl[unfolded a_get_tag_name_locs_def]



lemma get_tag_name_ok: 
  "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_tag_name element_ptr)"
  apply(unfold type_wf_impl get_tag_name_impl[unfolded a_get_tag_name_def])
  using get_MElement_ok
  by blast

lemma get_tag_name_pure [simp]: "pure (get_tag_name element_ptr) h"
  unfolding get_tag_name_impl[unfolded a_get_tag_name_def]
  by simp

lemma get_tag_name_ptr_in_heap [simp]:
  assumes "h  get_tag_name element_ptr r children"
  shows "element_ptr |∈| element_ptr_kinds h"
  using assms
  by(auto simp add: get_tag_name_impl[unfolded a_get_tag_name_def] get_MElement_ptr_in_heap 
          dest: is_OK_returns_result_I)

lemma get_tag_name_reads: "reads (get_tag_name_locs element_ptr) (get_tag_name element_ptr) h h'"
  by(simp add: get_tag_name_impl[unfolded a_get_tag_name_def] 
               get_tag_name_locs_impl[unfolded a_get_tag_name_locs_def] reads_bind_pure 
               reads_insert_writes_set_right)
end

locale l_get_tag_name = l_type_wf + l_get_tag_name_defs +
  assumes get_tag_name_reads: 
    "reads (get_tag_name_locs element_ptr) (get_tag_name element_ptr) h h'"
  assumes get_tag_name_ok: 
    "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (get_tag_name element_ptr)"
  assumes get_tag_name_ptr_in_heap: 
    "h  ok (get_tag_name element_ptr)  element_ptr |∈| element_ptr_kinds h"
  assumes get_tag_name_pure [simp]: 
    "pure (get_tag_name element_ptr) h"


global_interpretation l_get_tag_nameCore_DOM_defs defines
  get_tag_name = l_get_tag_nameCore_DOM_defs.a_get_tag_name and
  get_tag_name_locs = l_get_tag_nameCore_DOM_defs.a_get_tag_name_locs .

interpretation
  i_get_tag_name?: l_get_tag_nameCore_DOM type_wf get_tag_name get_tag_name_locs
  apply(unfold_locales)
  by (auto simp add: get_tag_name_def get_tag_name_locs_def)
declare l_get_tag_nameCore_DOM_axioms[instances]

lemma get_tag_name_is_l_get_tag_name [instances]: 
  "l_get_tag_name type_wf get_tag_name get_tag_name_locs"
  apply(unfold_locales)
  using get_tag_name_reads get_tag_name_ok get_tag_name_ptr_in_heap get_tag_name_pure
  by blast+


paragraph ‹set\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_tag_nameCore_DOM =
  l_set_disconnected_nodesCore_DOM +
  l_get_tag_nameCore_DOM
begin
lemma set_disconnected_nodes_get_tag_name: 
  "w  a_set_disconnected_nodes_locs ptr. (h  w h h'  (r  a_get_tag_name_locs ptr'. r h h'))"
  by(auto simp add: a_set_disconnected_nodes_locs_def a_get_tag_name_locs_def all_args_def)
end

locale l_set_disconnected_nodes_get_tag_name = l_set_disconnected_nodes + l_get_tag_name +
  assumes set_disconnected_nodes_get_tag_name: 
  "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_tag_name_locs ptr'. r h h'))"

interpretation
  i_set_disconnected_nodes_get_tag_name?: l_set_disconnected_nodes_get_tag_nameCore_DOM type_wf 
                                          set_disconnected_nodes set_disconnected_nodes_locs 
                                          get_tag_name get_tag_name_locs
  by unfold_locales
declare l_set_disconnected_nodes_get_tag_nameCore_DOM_axioms[instances]

lemma set_disconnected_nodes_get_tag_name_is_l_set_disconnected_nodes_get_tag_name [instances]:
  "l_set_disconnected_nodes_get_tag_name type_wf set_disconnected_nodes set_disconnected_nodes_locs 
                                         get_tag_name get_tag_name_locs"
  using set_disconnected_nodes_is_l_set_disconnected_nodes get_tag_name_is_l_get_tag_name
  apply(simp add: l_set_disconnected_nodes_get_tag_name_def l_set_disconnected_nodes_get_tag_name_axioms_def)
  using set_disconnected_nodes_get_tag_name
  by fast


paragraph ‹set\_child\_nodes›

locale l_set_child_nodes_get_tag_nameCore_DOM =
  l_set_child_nodesCore_DOM +
  l_get_tag_nameCore_DOM
begin
lemma set_child_nodes_get_tag_name: 
  "w  set_child_nodes_locs ptr. (h  w h h'  (r  get_tag_name_locs ptr'. r h h'))"
  by(auto simp add: set_child_nodes_locs_def get_tag_name_locs_def all_args_def 
      intro: element_put_get_preserved[where getter=tag_name and setter=child_nodes_update])
end

locale l_set_child_nodes_get_tag_name = l_set_child_nodes + l_get_tag_name +
  assumes set_child_nodes_get_tag_name: 
    "w  set_child_nodes_locs ptr. (h  w h h'  (r  get_tag_name_locs ptr'. r h h'))"

interpretation
  i_set_child_nodes_get_tag_name?: l_set_child_nodes_get_tag_nameCore_DOM type_wf known_ptr 
                                   set_child_nodes set_child_nodes_locs get_tag_name get_tag_name_locs
  by unfold_locales
declare l_set_child_nodes_get_tag_nameCore_DOM_axioms[instances]

lemma set_child_nodes_get_tag_name_is_l_set_child_nodes_get_tag_name [instances]:
  "l_set_child_nodes_get_tag_name type_wf set_child_nodes set_child_nodes_locs get_tag_name get_tag_name_locs"
  using set_child_nodes_is_l_set_child_nodes get_tag_name_is_l_get_tag_name
  apply(simp add: l_set_child_nodes_get_tag_name_def l_set_child_nodes_get_tag_name_axioms_def)
  using set_child_nodes_get_tag_name
  by fast


subsubsection ‹set\_tag\_type›

locale l_set_tag_nameCore_DOM_defs
begin

definition a_set_tag_name :: "(_) element_ptr  tag_name  (_, unit) dom_prog"
  where
    "a_set_tag_name ptr tag = do {
      m  get_M ptr attrs;
      put_M ptr tag_name_update tag
    }"
lemmas set_tag_name_defs = a_set_tag_name_def

definition a_set_tag_name_locs :: "(_) element_ptr  (_, unit) dom_prog set"
  where
    "a_set_tag_name_locs element_ptr  all_args (put_M element_ptr tag_name_update)"
end

locale l_set_tag_name_defs =
  fixes set_tag_name :: "(_) element_ptr  tag_name  (_, unit) dom_prog"
  fixes set_tag_name_locs :: "(_) element_ptr  (_, unit) dom_prog set"

locale l_set_tag_nameCore_DOM =
  l_type_wf type_wf +
  l_set_tag_name_defs set_tag_name set_tag_name_locs +
  l_set_tag_nameCore_DOM_defs
  for type_wf :: "(_) heap  bool"
    and set_tag_name :: "(_) element_ptr  char list  (_, unit) dom_prog"
    and set_tag_name_locs :: "(_) element_ptr  (_, unit) dom_prog set" +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes set_tag_name_impl: "set_tag_name = a_set_tag_name"
  assumes set_tag_name_locs_impl: "set_tag_name_locs = a_set_tag_name_locs"
begin

lemma set_tag_name_ok:
  "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_tag_name element_ptr tag)"
  apply(unfold type_wf_impl)
  unfolding set_tag_name_impl[unfolded a_set_tag_name_def] using get_MElement_ok put_MElement_ok
  by (metis (no_types, lifting) DocumentClass.type_wfElement ElementMonad.get_M_pure bind_is_OK_E 
                                bind_is_OK_pure_I is_OK_returns_result_I)

lemma set_tag_name_writes:
  "writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
  by(auto simp add: set_tag_name_impl[unfolded a_set_tag_name_def]
      set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def] intro: writes_bind_pure)

lemma set_tag_name_pointers_preserved:
  assumes "w  set_tag_name_locs element_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
          split: if_splits)

lemma set_tag_name_typess_preserved:
  assumes "w  set_tag_name_locs element_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  apply(unfold type_wf_impl)
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
          split: if_splits)
end

locale l_set_tag_name = l_type_wf + l_set_tag_name_defs +
  assumes set_tag_name_writes:
    "writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
  assumes set_tag_name_ok:
    "type_wf h  element_ptr |∈| element_ptr_kinds h  h  ok (set_tag_name element_ptr tag)"
  assumes set_tag_name_pointers_preserved:
    "w  set_tag_name_locs element_ptr  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes set_tag_name_types_preserved:
    "w  set_tag_name_locs element_ptr  h  w h h'  type_wf h = type_wf h'"


global_interpretation l_set_tag_nameCore_DOM_defs defines
  set_tag_name = l_set_tag_nameCore_DOM_defs.a_set_tag_name and
  set_tag_name_locs = l_set_tag_nameCore_DOM_defs.a_set_tag_name_locs .
interpretation 
  i_set_tag_name?: l_set_tag_nameCore_DOM type_wf set_tag_name set_tag_name_locs
  apply(unfold_locales)
  by (auto simp add: set_tag_name_def set_tag_name_locs_def)
declare l_set_tag_nameCore_DOM_axioms[instances]

lemma set_tag_name_is_l_set_tag_name [instances]:
  "l_set_tag_name type_wf set_tag_name set_tag_name_locs"
  apply(simp add: l_set_tag_name_def)
  using set_tag_name_ok set_tag_name_writes set_tag_name_pointers_preserved
    set_tag_name_typess_preserved
  by blast

paragraph ‹get\_child\_nodes›

locale l_set_tag_name_get_child_nodesCore_DOM =
  l_set_tag_nameCore_DOM +
  l_get_child_nodesCore_DOM
begin
lemma set_tag_name_get_child_nodes:
  "w  set_tag_name_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
                    get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def] all_args_def 
      intro: element_put_get_preserved[where setter=tag_name_update and getter=child_nodes])
end

locale l_set_tag_name_get_child_nodes = l_set_tag_name + l_get_child_nodes +
  assumes set_tag_name_get_child_nodes:
    "w  set_tag_name_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

interpretation
  i_set_tag_name_get_child_nodes?: l_set_tag_name_get_child_nodesCore_DOM type_wf
  set_tag_name set_tag_name_locs known_ptr
                                   get_child_nodes get_child_nodes_locs
  by unfold_locales
declare l_set_tag_name_get_child_nodesCore_DOM_axioms[instances]

lemma set_tag_name_get_child_nodes_is_l_set_tag_name_get_child_nodes [instances]:
  "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"
  using set_tag_name_is_l_set_tag_name get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_tag_name_get_child_nodes_def l_set_tag_name_get_child_nodes_axioms_def)
  using set_tag_name_get_child_nodes
  by fast


paragraph ‹get\_disconnected\_nodes›

locale l_set_tag_name_get_disconnected_nodesCore_DOM =
  l_set_tag_nameCore_DOM +
  l_get_disconnected_nodesCore_DOM
begin
lemma set_tag_name_get_disconnected_nodes:
  "w  set_tag_name_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_tag_name_locs_impl[unfolded a_set_tag_name_locs_def]
                    get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def] 
                    all_args_def)
end

locale l_set_tag_name_get_disconnected_nodes = l_set_tag_name + l_get_disconnected_nodes +
  assumes set_tag_name_get_disconnected_nodes:
    "w  set_tag_name_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"

interpretation
  i_set_tag_name_get_disconnected_nodes?: l_set_tag_name_get_disconnected_nodesCore_DOM type_wf
  set_tag_name set_tag_name_locs get_disconnected_nodes
                                          get_disconnected_nodes_locs
  by unfold_locales
declare l_set_tag_name_get_disconnected_nodesCore_DOM_axioms[instances]

lemma set_tag_name_get_disconnected_nodes_is_l_set_tag_name_get_disconnected_nodes [instances]:
  "l_set_tag_name_get_disconnected_nodes type_wf set_tag_name set_tag_name_locs get_disconnected_nodes
                                         get_disconnected_nodes_locs"
  using set_tag_name_is_l_set_tag_name get_disconnected_nodes_is_l_get_disconnected_nodes
  apply(simp add: l_set_tag_name_get_disconnected_nodes_def
      l_set_tag_name_get_disconnected_nodes_axioms_def)
  using set_tag_name_get_disconnected_nodes
  by fast


paragraph ‹get\_tag\_type›

locale l_set_tag_name_get_tag_nameCore_DOM = l_get_tag_nameCore_DOM
  + l_set_tag_nameCore_DOM
begin
lemma set_tag_name_get_tag_name:
  assumes "h  a_set_tag_name element_ptr tag h h'"
  shows "h'  a_get_tag_name element_ptr r tag"
  using assms
  by(auto simp add: a_get_tag_name_def a_set_tag_name_def)

lemma set_tag_name_get_tag_name_different_pointers:
  assumes "ptr  ptr'"
  assumes "w  a_set_tag_name_locs ptr"
  assumes "h  w h h'"
  assumes "r  a_get_tag_name_locs ptr'"
  shows "r h h'"
  using assms
  by(auto simp add: all_args_def a_set_tag_name_locs_def a_get_tag_name_locs_def
      split: if_splits option.splits )
end

locale l_set_tag_name_get_tag_name = l_get_tag_name + l_set_tag_name +
  assumes set_tag_name_get_tag_name:
    "h  set_tag_name element_ptr tag h h'
      h'  get_tag_name element_ptr r tag"
  assumes set_tag_name_get_tag_name_different_pointers:
    "ptr  ptr'  w  set_tag_name_locs ptr  h  w h h'
     r  get_tag_name_locs ptr'  r h h'"

interpretation i_set_tag_name_get_tag_name?:
  l_set_tag_name_get_tag_nameCore_DOM type_wf get_tag_name
  get_tag_name_locs set_tag_name set_tag_name_locs
  by unfold_locales
declare l_set_tag_name_get_tag_nameCore_DOM_axioms[instances]

lemma set_tag_name_get_tag_name_is_l_set_tag_name_get_tag_name [instances]:
  "l_set_tag_name_get_tag_name  type_wf get_tag_name get_tag_name_locs
                                                    set_tag_name set_tag_name_locs"
  using set_tag_name_is_l_set_tag_name get_tag_name_is_l_get_tag_name
  apply(simp add: l_set_tag_name_get_tag_name_def
      l_set_tag_name_get_tag_name_axioms_def)
  using set_tag_name_get_tag_name
    set_tag_name_get_tag_name_different_pointers
  by fast+
subsubsection ‹set\_val›

locale l_set_valCore_DOM_defs
begin

definition a_set_val :: "(_) character_data_ptr  DOMString  (_, unit) dom_prog"
  where
    "a_set_val ptr v = do {
      m  get_M ptr val;
      put_M ptr val_update v
    }"
lemmas set_val_defs = a_set_val_def

definition a_set_val_locs :: "(_) character_data_ptr  (_, unit) dom_prog set"
  where
    "a_set_val_locs character_data_ptr  all_args (put_M character_data_ptr val_update)"
end

locale l_set_val_defs =
  fixes set_val :: "(_) character_data_ptr  DOMString  (_, unit) dom_prog"
  fixes set_val_locs :: "(_) character_data_ptr  (_, unit) dom_prog set"

locale l_set_valCore_DOM =
  l_type_wf type_wf +
  l_set_val_defs set_val set_val_locs +
  l_set_valCore_DOM_defs
  for type_wf :: "(_) heap  bool"
  and set_val :: "(_) character_data_ptr  char list  (_, unit) dom_prog"
  and set_val_locs :: "(_) character_data_ptr  (_, unit) dom_prog set"  +
  assumes type_wf_impl: "type_wf = DocumentClass.type_wf"
  assumes set_val_impl: "set_val = a_set_val"
  assumes set_val_locs_impl: "set_val_locs = a_set_val_locs"
begin

lemma set_val_ok: 
  "type_wf h  character_data_ptr |∈| character_data_ptr_kinds h  h  ok (set_val character_data_ptr tag)"
  apply(unfold type_wf_impl)
  unfolding set_val_impl[unfolded a_set_val_def] using get_MCharacterData_ok put_MCharacterData_ok
  by (metis (no_types, lifting) DocumentClass.type_wfCharacterData CharacterDataMonad.get_M_pure 
            bind_is_OK_E bind_is_OK_pure_I is_OK_returns_result_I)

lemma set_val_writes: "writes (set_val_locs character_data_ptr) (set_val character_data_ptr tag) h h'"
  by(auto simp add: set_val_impl[unfolded a_set_val_def] set_val_locs_impl[unfolded a_set_val_locs_def] 
               intro: writes_bind_pure)

lemma set_val_pointers_preserved:
  assumes "w  set_val_locs character_data_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_val_locs_impl[unfolded a_set_val_locs_def] split: if_splits)

lemma set_val_typess_preserved:
  assumes "w  set_val_locs character_data_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  apply(unfold type_wf_impl)
  using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
  by(auto simp add: all_args_def set_val_locs_impl[unfolded a_set_val_locs_def] split: if_splits)
end

locale l_set_val = l_type_wf + l_set_val_defs +
  assumes set_val_writes: 
    "writes (set_val_locs character_data_ptr) (set_val character_data_ptr tag) h h'"
  assumes set_val_ok: 
    "type_wf h  character_data_ptr |∈| character_data_ptr_kinds h  h  ok (set_val character_data_ptr tag)"
  assumes set_val_pointers_preserved: 
    "w  set_val_locs character_data_ptr  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes set_val_types_preserved: 
    "w  set_val_locs character_data_ptr  h  w h h'  type_wf h = type_wf h'"


global_interpretation l_set_valCore_DOM_defs defines
  set_val = l_set_valCore_DOM_defs.a_set_val and
  set_val_locs = l_set_valCore_DOM_defs.a_set_val_locs .
interpretation 
  i_set_val?: l_set_valCore_DOM type_wf set_val set_val_locs
  apply(unfold_locales)
  by (auto simp add: set_val_def set_val_locs_def)
declare l_set_valCore_DOM_axioms[instances]

lemma set_val_is_l_set_val [instances]: "l_set_val type_wf set_val set_val_locs"
  apply(simp add: l_set_val_def)
  using set_val_ok set_val_writes set_val_pointers_preserved set_val_typess_preserved
  by blast

paragraph ‹get\_child\_nodes›

locale l_set_val_get_child_nodesCore_DOM =
  l_set_valCore_DOM +
  l_get_child_nodesCore_DOM
begin
lemma set_val_get_child_nodes: 
  "w  set_val_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_val_locs_impl[unfolded a_set_val_locs_def] 
                    get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def] all_args_def)
end

locale l_set_val_get_child_nodes = l_set_val + l_get_child_nodes +
  assumes set_val_get_child_nodes: 
    "w  set_val_locs ptr. (h  w h h'  (r  get_child_nodes_locs ptr'. r h h'))"

interpretation
  i_set_val_get_child_nodes?: l_set_val_get_child_nodesCore_DOM type_wf set_val set_val_locs known_ptr 
                              get_child_nodes get_child_nodes_locs
  by unfold_locales
declare l_set_val_get_child_nodesCore_DOM_axioms[instances]

lemma set_val_get_child_nodes_is_l_set_val_get_child_nodes [instances]:
  "l_set_val_get_child_nodes type_wf set_val set_val_locs known_ptr get_child_nodes get_child_nodes_locs"
  using set_val_is_l_set_val get_child_nodes_is_l_get_child_nodes
  apply(simp add: l_set_val_get_child_nodes_def l_set_val_get_child_nodes_axioms_def)
  using set_val_get_child_nodes
  by fast


paragraph ‹get\_disconnected\_nodes›

locale l_set_val_get_disconnected_nodesCore_DOM =
  l_set_valCore_DOM +
  l_get_disconnected_nodesCore_DOM
begin
lemma set_val_get_disconnected_nodes: 
  "w  set_val_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"
  by(auto simp add: set_val_locs_impl[unfolded a_set_val_locs_def] 
                    get_disconnected_nodes_locs_impl[unfolded a_get_disconnected_nodes_locs_def] 
                    all_args_def)
end

locale l_set_val_get_disconnected_nodes = l_set_val + l_get_disconnected_nodes +
  assumes set_val_get_disconnected_nodes: 
   "w  set_val_locs ptr. (h  w h h'  (r  get_disconnected_nodes_locs ptr'. r h h'))"

interpretation
  i_set_val_get_disconnected_nodes?: l_set_val_get_disconnected_nodesCore_DOM type_wf set_val 
                                     set_val_locs get_disconnected_nodes get_disconnected_nodes_locs
  by unfold_locales
declare l_set_val_get_disconnected_nodesCore_DOM_axioms[instances]

lemma set_val_get_disconnected_nodes_is_l_set_val_get_disconnected_nodes [instances]:
  "l_set_val_get_disconnected_nodes type_wf set_val set_val_locs get_disconnected_nodes
get_disconnected_nodes_locs"
  using set_val_is_l_set_val get_disconnected_nodes_is_l_get_disconnected_nodes
  apply(simp add: l_set_val_get_disconnected_nodes_def l_set_val_get_disconnected_nodes_axioms_def)
  using set_val_get_disconnected_nodes
  by fast



subsubsection ‹get\_parent›

locale l_get_parentCore_DOM_defs =
  l_get_child_nodes_defs get_child_nodes get_child_nodes_locs
  for get_child_nodes :: "(_::linorder) object_ptr  (_, (_) node_ptr list) dom_prog"
  and get_child_nodes_locs :: "(_) object_ptr  ((_) heap  (_) heap  bool) set"
begin
definition a_get_parent :: "(_) node_ptr  (_, (_::linorder) object_ptr option) dom_prog"
  where
    "a_get_parent node_ptr = do {
      check_in_heap (cast node_ptr);
      parent_ptrs  object_ptr_kinds_M  filter_M (λptr. do {
        children  get_child_nodes ptr;
        return (node_ptr  set children)
      });
      (if parent_ptrs = []
        then return None
        else return (Some (hd parent_ptrs)))
    }"

definition 
  "a_get_parent_locs  (ptr. get_child_nodes_locs ptr  {preserved (get_MObject  ptr RObject.nothing)})"
end

locale l_get_parent_defs =
  fixes get_parent :: "(_) node_ptr  (_, (_::linorder) object_ptr option) dom_prog"
  fixes get_parent_locs :: "((_) heap  (_) heap  bool) set"

locale l_get_parentCore_DOM =
  l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
  l_known_ptrs known_ptr known_ptrs +
  l_get_parentCore_DOM_defs get_child_nodes get_child_nodes_locs +
  l_get_parent_defs get_parent get_parent_locs
  for known_ptr :: "(_::linorder) object_ptr  bool"
  and type_wf :: "(_) heap  bool"
  and get_child_nodes (* :: "(_) object_ptr ⇒ (_, (_) node_ptr list) dom_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" *) +
  assumes get_parent_impl: "get_parent = a_get_parent"
  assumes get_parent_locs_impl: "get_parent_locs = a_get_parent_locs"
begin
lemmas get_parent_def = get_parent_impl[unfolded a_get_parent_def]
lemmas get_parent_locs_def = get_parent_locs_impl[unfolded a_get_parent_locs_def]

lemma get_parent_pure [simp]: "pure (get_parent ptr) h"
  using get_child_nodes_pure
  by(auto simp add: get_parent_def intro!: bind_pure_I filter_M_pure_I)

lemma get_parent_ok [simp]:
  assumes "type_wf h"
  assumes "known_ptrs h"
  assumes "ptr |∈| node_ptr_kinds h"
  shows "h  ok (get_parent ptr)"
  using assms get_child_nodes_ok get_child_nodes_pure
  by(auto simp add: get_parent_impl[unfolded a_get_parent_def] known_ptrs_known_ptr 
          intro!: bind_is_OK_pure_I filter_M_pure_I filter_M_is_OK_I bind_pure_I)

lemma get_parent_ptr_in_heap [simp]: "h  ok (get_parent node_ptr)  node_ptr |∈| node_ptr_kinds h"
  using get_parent_def is_OK_returns_result_I check_in_heap_ptr_in_heap
  by (metis (no_types, lifting) bind_returns_heap_E get_parent_pure node_ptr_kinds_commutes pure_pure)

lemma get_parent_parent_in_heap:
  assumes "h  get_parent child_node r Some parent"
  shows "parent |∈| object_ptr_kinds h"
  using assms get_child_nodes_pure
  by(auto simp add: get_parent_def elim!: bind_returns_result_E2 
          dest!: filter_M_not_more_elements[where x=parent] 
          intro!: filter_M_pure_I bind_pure_I 
          split: if_splits)

lemma get_parent_child_dual:
  assumes "h  get_parent child r Some ptr"
  obtains children where "h  get_child_nodes ptr r children" and "child  set children"
  using assms get_child_nodes_pure
  by(auto simp add: get_parent_def bind_pure_I 
          dest!: filter_M_holds_for_result 
          elim!: bind_returns_result_E2 
          intro!: filter_M_pure_I 
          split: if_splits)

lemma get_parent_reads: "reads get_parent_locs (get_parent node_ptr) h h'"
  using get_child_nodes_reads[unfolded reads_def]
  by(auto simp add: get_parent_def get_parent_locs_def 
          intro!: reads_bind_pure reads_subset[OF check_in_heap_reads] 
                  reads_subset[OF get_child_nodes_reads] reads_subset[OF return_reads] 
                  reads_subset[OF object_ptr_kinds_M_reads] filter_M_reads filter_M_pure_I bind_pure_I)

lemma get_parent_reads_pointers: "preserved (get_MObject ptr RObject.nothing)  get_parent_locs"
  by(auto simp add: get_parent_locs_def)
end

locale l_get_parent = l_type_wf + l_known_ptrs + l_get_parent_defs + l_get_child_nodes +
  assumes get_parent_reads: 
    "reads get_parent_locs (get_parent node_ptr) h h'"
  assumes get_parent_ok: 
    "type_wf h  known_ptrs h  node_ptr |∈| node_ptr_kinds h  h  ok (get_parent node_ptr)"
  assumes get_parent_ptr_in_heap: 
    "h  ok (get_parent node_ptr)  node_ptr |∈| node_ptr_kinds h"
  assumes get_parent_pure [simp]: 
    "pure (get_parent node_ptr) h"
  assumes get_parent_parent_in_heap: 
    "h  get_parent child_node r Some parent  parent |∈| object_ptr_kinds h"
  assumes get_parent_child_dual: 
    "h  get_parent child r Some ptr  (children. h  get_child_nodes ptr r children 
          child  set children  thesis)  thesis"
  assumes get_parent_reads_pointers: 
    "preserved (get_MObject ptr RObject.nothing)  get_parent_locs"

global_interpretation l_get_parentCore_DOM_defs get_child_nodes get_child_nodes_locs defines      
  get_parent = "l_get_parentCore_DOM_defs.a_get_parent get_child_nodes" and
  get_parent_locs = "l_get_parentCore_DOM_defs.a_get_parent_locs get_child_nodes_locs" .

interpretation 
  i_get_parent?: l_get_parentCore_DOM known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs 
                 get_parent get_parent_locs
  using instances
  apply(simp add: l_get_parentCore_DOM_def l_get_parentCore_DOM_axioms_def)
  apply(simp add: get_parent_def get_parent_locs_def)
  done
declare l_get_parentCore_DOM_axioms[instances]

lemma get_parent_is_l_get_parent [instances]: 
  "l_get_parent type_wf known_ptr known_ptrs get_parent get_parent_locs get_child_nodes get_child_nodes_locs"
  using instances
  apply(auto simp add: l_get_parent_def l_get_parent_axioms_def)[1]
  using get_parent_reads get_parent_ok get_parent_ptr_in_heap get_parent_pure 
        get_parent_parent_in_heap get_parent_child_dual
  using get_parent_reads_pointers
  by blast+


paragraph ‹set\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_parentCore_DOM =
  l_set_disconnected_nodes_get_child_nodes
    set_disconnected_nodes set_disconnected_nodes_locs get_child_nodes get_child_nodes_locs
  + l_set_disconnected_nodesCore_DOM
    type_wf set_disconnected_nodes set_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
  for known_ptr :: "(_::linorder) object_ptr  bool"
  and type_wf :: "(_) heap  bool"
  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 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"
begin
lemma set_disconnected_nodes_get_parent [simp]: 
  "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_parent_locs. r h h'))"
  by(auto simp add: get_parent_locs_def set_disconnected_nodes_locs_def all_args_def)
end

locale l_set_disconnected_nodes_get_parent = l_set_disconnected_nodes_defs + l_get_parent_defs +
  assumes set_disconnected_nodes_get_parent [simp]: 
     "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_parent_locs. r h h'))"

interpretation i_set_disconnected_nodes_get_parent?:
  l_set_disconnected_nodes_get_parentCore_DOM known_ptr type_wf set_disconnected_nodes 
  set_disconnected_nodes_locs get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  using instances
  by (simp add: l_set_disconnected_nodes_get_parentCore_DOM_def)
declare l_set_disconnected_nodes_get_parentCore_DOM_axioms[instances]

lemma set_disconnected_nodes_get_parent_is_l_set_disconnected_nodes_get_parent [instances]:
  "l_set_disconnected_nodes_get_parent set_disconnected_nodes_locs get_parent_locs"
  by(simp add: l_set_disconnected_nodes_get_parent_def)



subsubsection ‹get\_root\_node›

locale l_get_root_nodeCore_DOM_defs =
  l_get_parent_defs get_parent get_parent_locs
  for get_parent :: "(_) node_ptr  ((_) heap, exception, (_::linorder) object_ptr option) prog"
  and get_parent_locs :: "((_) heap  (_) heap  bool) set"
begin
partial_function (dom_prog) 
  a_get_ancestors :: "(_::linorder) object_ptr  (_, (_) object_ptr list) dom_prog"
  where
    "a_get_ancestors ptr = do {
      check_in_heap ptr;
      ancestors  (case castobject_ptr2node_ptr ptr of
        Some node_ptr  do {
          parent_ptr_opt  get_parent node_ptr;
          (case parent_ptr_opt of
            Some parent_ptr  a_get_ancestors parent_ptr
          | None  return [])
        }
      | None  return []);
      return (ptr # ancestors)
    }"

definition "a_get_ancestors_locs = get_parent_locs"

definition a_get_root_node :: "(_) object_ptr  (_, (_) object_ptr) dom_prog"
  where
    "a_get_root_node ptr = do {
      ancestors  a_get_ancestors ptr;
      return (last ancestors)
    }"
definition "a_get_root_node_locs = a_get_ancestors_locs"
end

locale l_get_ancestors_defs =
  fixes get_ancestors :: "(_::linorder) object_ptr  (_, (_) object_ptr list) dom_prog"
  fixes get_ancestors_locs :: "((_) heap  (_) heap  bool) set"

locale l_get_root_node_defs = 
  fixes get_root_node :: "(_) object_ptr  (_, (_) object_ptr) dom_prog"
  fixes get_root_node_locs :: "((_) heap  (_) heap  bool) set"

locale l_get_root_nodeCore_DOM =
  l_get_parent +
  l_get_root_nodeCore_DOM_defs +
  l_get_ancestors_defs +
  l_get_root_node_defs +
  assumes get_ancestors_impl: "get_ancestors = a_get_ancestors"
  assumes get_ancestors_locs_impl: "get_ancestors_locs = a_get_ancestors_locs"
  assumes get_root_node_impl: "get_root_node = a_get_root_node"
  assumes get_root_node_locs_impl: "get_root_node_locs = a_get_root_node_locs"
begin
lemmas get_ancestors_def = a_get_ancestors.simps[folded get_ancestors_impl]
lemmas get_ancestors_locs_def = a_get_ancestors_locs_def[folded get_ancestors_locs_impl]
lemmas get_root_node_def = a_get_root_node_def[folded get_root_node_impl get_ancestors_impl]
lemmas get_root_node_locs_def = a_get_root_node_locs_def[folded get_root_node_locs_impl  
                                                         get_ancestors_locs_impl]

lemma get_ancestors_pure [simp]:
  "pure (get_ancestors ptr) h"
proof -
  have "ptr h h' x. h  get_ancestors ptr r x  h  get_ancestors ptr h h'  h = h'"
  proof (induct rule: a_get_ancestors.fixp_induct[folded get_ancestors_impl])
    case 1
    then show ?case
      by(rule admissible_dom_prog)
  next
    case 2
    then show ?case
      by simp
  next
    case (3 f)
    then show ?case
      using get_parent_pure
      apply(auto simp add: pure_returns_heap_eq pure_def 
                 split: option.splits 
                 elim!: bind_returns_heap_E bind_returns_result_E 
                 dest!: pure_returns_heap_eq[rotated, OF check_in_heap_pure])[1]
      apply (meson option.simps(3) returns_result_eq)
      by (metis get_parent_pure pure_returns_heap_eq)
  qed
  then show ?thesis
    by (meson pure_eq_iff)
qed


lemma get_root_node_pure [simp]: "pure (get_root_node ptr) h"
  by(auto simp add: get_root_node_def bind_pure_I)


lemma get_ancestors_ptr_in_heap:
  assumes "h  ok (get_ancestors ptr)"
  shows "ptr |∈| object_ptr_kinds h"
  using assms 
  by(auto simp add: get_ancestors_def check_in_heap_ptr_in_heap 
          elim!: bind_is_OK_E  dest: is_OK_returns_result_I)

lemma get_ancestors_ptr:
  assumes "h  get_ancestors ptr r ancestors"
  shows "ptr  set ancestors"
  using assms
  apply(simp add: get_ancestors_def) 
  by(auto  elim!: bind_returns_result_E2 split: option.splits intro!: bind_pure_I)

lemma get_ancestors_not_node:
  assumes "h  get_ancestors ptr r ancestors"
  assumes "¬is_node_ptr_kind ptr"
  shows "ancestors = [ptr]"
  using assms
  apply(simp add: get_ancestors_def) 
  by(auto elim!: bind_returns_result_E2 split: option.splits)

lemma get_root_node_no_parent: 
  "h  get_parent node_ptr r None  h  get_root_node (cast node_ptr) r cast node_ptr"
  apply(auto simp add: check_in_heap_def get_root_node_def get_ancestors_def 
             intro!: bind_pure_returns_result_I )[1]
  using get_parent_ptr_in_heap by blast

end

locale l_get_ancestors = l_get_ancestors_defs +
  assumes get_ancestors_pure [simp]: "pure (get_ancestors node_ptr) h"
  assumes get_ancestors_ptr_in_heap: "h  ok (get_ancestors ptr)  ptr |∈| object_ptr_kinds h"
  assumes get_ancestors_ptr: "h  get_ancestors ptr r ancestors  ptr  set ancestors"

locale l_get_root_node = l_get_root_node_defs + l_get_parent_defs +
  assumes get_root_node_pure[simp]: 
   "pure (get_root_node ptr) h"
  assumes get_root_node_no_parent: 
   "h  get_parent node_ptr r None  h  get_root_node (cast node_ptr) r cast node_ptr"

global_interpretation l_get_root_nodeCore_DOM_defs get_parent get_parent_locs
  defines get_root_node = "l_get_root_nodeCore_DOM_defs.a_get_root_node get_parent"
      and get_root_node_locs = "l_get_root_nodeCore_DOM_defs.a_get_root_node_locs get_parent_locs"
      and get_ancestors = "l_get_root_nodeCore_DOM_defs.a_get_ancestors get_parent"
      and get_ancestors_locs = "l_get_root_nodeCore_DOM_defs.a_get_ancestors_locs get_parent_locs"
  .
declare a_get_ancestors.simps [code]

interpretation 
  i_get_root_node?: 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
  using instances
  apply(simp add: l_get_root_nodeCore_DOM_def l_get_root_nodeCore_DOM_axioms_def)
  by(simp add: get_root_node_def get_root_node_locs_def get_ancestors_def get_ancestors_locs_def)
declare l_get_root_nodeCore_DOM_axioms[instances]

lemma get_ancestors_is_l_get_ancestors [instances]: "l_get_ancestors get_ancestors"
  unfolding l_get_ancestors_def
  using get_ancestors_pure get_ancestors_ptr get_ancestors_ptr_in_heap
  by blast

lemma get_root_node_is_l_get_root_node [instances]: "l_get_root_node get_root_node get_parent"
  apply(simp add: l_get_root_node_def)
  using get_root_node_no_parent
  by fast


paragraph ‹set\_disconnected\_nodes›

locale l_set_disconnected_nodes_get_ancestorsCore_DOM =
  l_set_disconnected_nodes_get_parent
    set_disconnected_nodes set_disconnected_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
  + l_set_disconnected_nodesCore_DOM
     type_wf set_disconnected_nodes set_disconnected_nodes_locs
  for known_ptr :: "(_::linorder) object_ptr  bool"
  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 get_child_nodes :: "(_) object_ptr  ((_) heap, exception, (_) node_ptr list) prog"
  and get_child_nodes_locs :: "(_) object_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 type_wf :: "(_) heap  bool"
  and known_ptrs :: "(_) heap  bool"
  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 set_disconnected_nodes_get_ancestors: 
  "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_ancestors_locs. r h h'))"
  by(auto simp add: get_parent_locs_def set_disconnected_nodes_locs_def get_ancestors_locs_def 
                    all_args_def)
end

locale l_set_disconnected_nodes_get_ancestors = l_set_disconnected_nodes_defs + l_get_ancestors_defs +
  assumes set_disconnected_nodes_get_ancestors: 
    "w  set_disconnected_nodes_locs ptr. (h  w h h'  (r  get_ancestors_locs. r h h'))"

interpretation
  i_set_disconnected_nodes_get_ancestors?: l_set_disconnected_nodes_get_ancestorsCore_DOM known_ptr 
                                           set_disconnected_nodes set_disconnected_nodes_locs 
                                           get_child_nodes get_child_nodes_locs get_parent 
                                           get_parent_locs type_wf known_ptrs get_ancestors 
                                           get_ancestors_locs get_root_node get_root_node_locs
  using instances
  by (simp add: l_set_disconnected_nodes_get_ancestorsCore_DOM_def)           
declare l_set_disconnected_nodes_get_ancestorsCore_DOM_axioms[instances]


lemma set_disconnected_nodes_get_ancestors_is_l_set_disconnected_nodes_get_ancestors [instances]:
  "l_set_disconnected_nodes_get_ancestors set_disconnected_nodes_locs get_ancestors_locs"
  using instances
  apply(simp add: l_set_disconnected_nodes_get_ancestors_def)
  using set_disconnected_nodes_get_ancestors
  by fast



subsubsection ‹get\_owner\_document›
                                                                            
locale l_get_owner_documentCore_DOM_defs =
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_get_root_node_defs get_root_node get_root_node_locs
  for get_root_node :: "(_::linorder) object_ptr  ((_) heap, exception, (_) object_ptr) prog"
  and get_root_node_locs :: "((_) 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_get_owner_documentnode_ptr :: "(_) node_ptr  unit  (_, (_) document_ptr) dom_prog"
  where                                                                                   
    "a_get_owner_documentnode_ptr node_ptr _ = do {
      root  get_root_node (cast node_ptr);
      (case cast root of
        Some document_ptr  return document_ptr
      | None  do {
        ptrs  document_ptr_kinds_M;
        candidates  filter_M (λdocument_ptr. do {
          disconnected_nodes  get_disconnected_nodes document_ptr;
          return (root  cast ` set disconnected_nodes)
        }) ptrs;
        return (hd candidates)
      })
    }"

definition 
  a_get_owner_documentdocument_ptr :: "(_) document_ptr  unit  (_, (_) document_ptr) dom_prog"
  where
    "a_get_owner_documentdocument_ptr document_ptr _ = do {
      document_ptrs  document_ptr_kinds_M;
      (if document_ptr  set document_ptrs then return document_ptr else error SegmentationFault)}"

definition 
  a_get_owner_document_tups :: "(((_) object_ptr  bool) × ((_) object_ptr  unit 
                                                  (_, (_) document_ptr) dom_prog)) list"
  where
     "a_get_owner_document_tups = [
        (is_element_ptr, a_get_owner_documentnode_ptr  the  cast),
        (is_character_data_ptr, a_get_owner_documentnode_ptr  the  cast),
        (is_document_ptr, a_get_owner_documentdocument_ptr  the  cast)
      ]"

definition a_get_owner_document :: "(_) object_ptr  (_, (_) document_ptr) dom_prog"
  where
    "a_get_owner_document ptr = invoke a_get_owner_document_tups ptr ()"
end

locale l_get_owner_document_defs =
  fixes get_owner_document :: "(_::linorder) object_ptr  (_, (_) document_ptr) dom_prog"
                                                     
locale l_get_owner_documentCore_DOM =
  l_known_ptr known_ptr +
  l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
  l_get_root_node get_root_node get_root_node_locs +
  l_get_owner_documentCore_DOM_defs get_root_node get_root_node_locs get_disconnected_nodes 
                                  get_disconnected_nodes_locs +
  l_get_owner_document_defs get_owner_document
  for known_ptr :: "(_::linorder) 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 get_root_node :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr) prog"
  and get_root_node_locs :: "((_) heap  (_) heap  bool) set"
  and get_owner_document :: "(_) object_ptr  ((_) heap, exception, (_) document_ptr) prog" +
  assumes known_ptr_impl: "known_ptr = a_known_ptr"
  assumes get_owner_document_impl: "get_owner_document = a_get_owner_document"
begin
lemmas known_ptr_def = known_ptr_impl[unfolded a_known_ptr_def]
lemmas get_owner_document_def = a_get_owner_document_def[folded get_owner_document_impl]

lemma get_owner_document_split:
  "P (invoke (a_get_owner_document_tups @ xs) ptr ()) =
    ((known_ptr ptr  P (get_owner_document ptr))
     (¬(known_ptr ptr)  P (invoke xs ptr ())))"
  by(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_def 
                    CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs 
                    NodeClass.known_ptr_defs 
          split: invoke_splits option.splits)

lemma get_owner_document_split_asm:
  "P (invoke (a_get_owner_document_tups @ xs) ptr ()) =
    (¬((known_ptr ptr  ¬P (get_owner_document ptr))
     (¬(known_ptr ptr)  ¬P (invoke xs ptr ()))))"
  by(auto simp add: get_owner_document_def a_get_owner_document_tups_def known_ptr_def 
                    CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs 
                    NodeClass.known_ptr_defs 
          split: invoke_splits)
lemmas get_owner_document_splits = get_owner_document_split get_owner_document_split_asm

lemma get_owner_document_pure [simp]:
  "pure (get_owner_document ptr) h"
proof -
  have "node_ptr. pure (a_get_owner_documentnode_ptr node_ptr ()) h"
    by(auto simp add: a_get_owner_documentnode_ptr_def 
                 intro!: bind_pure_I filter_M_pure_I 
                 split: option.splits)
  moreover have "document_ptr. pure (a_get_owner_documentdocument_ptr document_ptr ()) h"
    by(auto simp add: a_get_owner_documentdocument_ptr_def bind_pure_I)
  ultimately show ?thesis
    by(auto simp add: get_owner_document_def a_get_owner_document_tups_def 
            intro!: bind_pure_I 
            split: invoke_splits)
qed

lemma get_owner_document_ptr_in_heap:
  assumes "h  ok (get_owner_document ptr)"
  shows "ptr |∈| object_ptr_kinds h"
  using assms 
  by(auto simp add: get_owner_document_def invoke_ptr_in_heap dest: is_OK_returns_heap_I)
end

locale l_get_owner_document = l_get_owner_document_defs +
  assumes get_owner_document_ptr_in_heap: 
    "h  ok (get_owner_document ptr)  ptr |∈| object_ptr_kinds h"
  assumes get_owner_document_pure [simp]: 
    "pure (get_owner_document ptr) h"

global_interpretation l_get_owner_documentCore_DOM_defs get_root_node get_root_node_locs 
                                                      get_disconnected_nodes get_disconnected_nodes_locs
  defines get_owner_document_tups = 
          "l_get_owner_documentCore_DOM_defs.a_get_owner_document_tups get_root_node get_disconnected_nodes"
     and get_owner_document = 
         "l_get_owner_documentCore_DOM_defs.a_get_owner_document get_root_node get_disconnected_nodes"
     and get_owner_documentnode_ptr = 
         "l_get_owner_documentCore_DOM_defs.a_get_owner_documentnode_ptr get_root_node get_disconnected_nodes"
  .
interpretation
  i_get_owner_document?: l_get_owner_documentCore_DOM get_parent get_parent_locs known_ptr type_wf 
                         get_disconnected_nodes get_disconnected_nodes_locs get_root_node 
                         get_root_node_locs get_owner_document
  using instances
     apply(auto simp add: l_get_owner_documentCore_DOM_def l_get_owner_documentCore_DOM_axioms_def)[1]
  by(auto simp add: get_owner_document_tups_def get_owner_document_def get_owner_documentnode_ptr_def)[1]
declare l_get_owner_documentCore_DOM_axioms[instances]

lemma get_owner_document_is_l_get_owner_document [instances]: 
  "l_get_owner_document get_owner_document"
  using get_owner_document_ptr_in_heap
  by(auto simp add: l_get_owner_document_def)

subsubsection ‹remove\_child›

locale l_remove_childCore_DOM_defs =
  l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
  l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
  l_get_parent_defs get_parent get_parent_locs +
  l_get_owner_document_defs get_owner_document +
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes_defs set_disconnected_nodes set_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 set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
  and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
  and get_parent :: "(_) node_ptr  ((_) heap, exception, (_) object_ptr option) prog"
  and get_parent_locs :: "((_) heap  (_) heap  bool) set"
  and get_owner_document :: "(_) object_ptr  ((_) heap, exception, (_) document_ptr) prog"
  and get_disconnected_nodes :: "(_) document_ptr  ((_) heap, exception, (_) node_ptr list) prog"
  and get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"
  and set_disconnected_nodes :: "(_) document_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
  and set_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap, exception, unit) prog set"
begin
definition a_remove_child :: "(_) object_ptr  (_) node_ptr  (_, unit) dom_prog"
  where
    "a_remove_child ptr child = do {
      children  get_child_nodes ptr;
      if child  set children then
        error NotFoundError
      else do {
        owner_document  get_owner_document (cast child);
        disc_nodes  get_disconnected_nodes owner_document;
        set_disconnected_nodes owner_document (child # disc_nodes);
        set_child_nodes ptr (remove1 child children)
      }
    }"

definition a_remove_child_locs :: "(_) object_ptr  (_) document_ptr  (_, unit) dom_prog set"
  where
    "a_remove_child_locs ptr owner_document = set_child_nodes_locs ptr 
                                               set_disconnected_nodes_locs owner_document"

definition a_remove :: "(_) node_ptr  (_, unit) dom_prog"
  where
    "a_remove node_ptr = do {
      parent_opt  get_parent node_ptr;
      (case parent_opt of
        Some parent  do {
          a_remove_child parent node_ptr;
          return ()
        }
      | None  return ())
    }"
end

locale l_remove_child_defs =
  fixes remove_child :: "(_::linorder) object_ptr  (_) node_ptr  (_, unit) dom_prog"
  fixes remove_child_locs :: "(_) object_ptr  (_) document_ptr  (_, unit) dom_prog set"

locale l_remove_defs = 
  fixes remove :: "(_) node_ptr  (_, unit) dom_prog"

locale l_remove_childCore_DOM =
  l_remove_childCore_DOM_defs +
  l_remove_child_defs +
  l_remove_defs +
  l_get_parent +
  l_get_owner_document +
  l_set_child_nodes_get_child_nodes +
  l_set_child_nodes_get_disconnected_nodes +
  l_set_disconnected_nodes_get_disconnected_nodes +
  l_set_disconnected_nodes_get_child_nodes +
  assumes remove_child_impl: "remove_child = a_remove_child"
  assumes remove_child_locs_impl: "remove_child_locs = a_remove_child_locs"
  assumes remove_impl: "remove = a_remove"
begin
lemmas remove_child_def = a_remove_child_def[folded remove_child_impl]
lemmas remove_child_locs_def = a_remove_child_locs_def[folded remove_child_locs_impl]
lemmas remove_def = a_remove_def[folded remove_child_impl remove_impl]

lemma remove_child_ptr_in_heap:
  assumes "h  ok (remove_child ptr child)"
  shows "ptr |∈| object_ptr_kinds h"
proof -
  obtain children where children: "h  get_child_nodes ptr r children"
    using assms
    by(auto simp add: remove_child_def)
  moreover have "children  []"
    using assms calculation
    by(auto simp add: remove_child_def elim!: bind_is_OK_E2)
  ultimately show ?thesis
    using assms(1) get_child_nodes_ptr_in_heap by blast 
qed


lemma remove_child_child_in_heap:
  assumes "h  remove_child ptr' child h h'"
  shows "child |∈| node_ptr_kinds h"
  using assms
  apply(auto simp add: remove_child_def
      elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
      split: if_splits)[1]
  by (meson is_OK_returns_result_I local.get_owner_document_ptr_in_heap node_ptr_kinds_commutes)


lemma remove_child_in_disconnected_nodes:
  (* assumes "known_ptrs h" *)
  assumes "h  remove_child ptr child h h'"
  assumes "h  get_owner_document (cast child) r owner_document"
  assumes "h'  get_disconnected_nodes owner_document r disc_nodes"
  shows "child  set disc_nodes"
proof -
  obtain prev_disc_nodes h2 children where
    disc_nodes: "h  get_disconnected_nodes owner_document r prev_disc_nodes" and
    h2: "h  set_disconnected_nodes owner_document (child # prev_disc_nodes) h h2" and
    h': "h2  set_child_nodes ptr (remove1 child children) h h'"
    using assms(1)
    apply(auto simp add: remove_child_def 
               elim!: bind_returns_heap_E 
        dest!: returns_result_eq[OF assms(2)]
        pure_returns_heap_eq[rotated, OF get_owner_document_pure]
                      pure_returns_heap_eq[rotated, OF get_child_nodes_pure] 
               split: if_splits)[1]
    by (metis get_disconnected_nodes_pure pure_returns_heap_eq)
  have "h2  get_disconnected_nodes owner_document r disc_nodes"
    apply(rule reads_writes_separate_backwards[OF get_disconnected_nodes_reads 
               set_child_nodes_writes h' assms(3)])
    by (simp add: set_child_nodes_get_disconnected_nodes)
  then show ?thesis
    by (metis (no_types, lifting) h2 set_disconnected_nodes_get_disconnected_nodes 
                                  list.set_intros(1) select_result_I2)
qed

lemma remove_child_writes [simp]: 
  "writes (remove_child_locs ptr |h  get_owner_document (cast child)|r) (remove_child ptr child) h h'"
  apply(auto simp add: remove_child_def intro!: writes_bind_pure[OF get_child_nodes_pure] 
                       writes_bind_pure[OF get_owner_document_pure] 
                       writes_bind_pure[OF get_disconnected_nodes_pure])[1]
  by(auto simp add: remove_child_locs_def set_disconnected_nodes_writes writes_union_right_I 
                    set_child_nodes_writes writes_union_left_I 
          intro!: writes_bind)

lemma remove_writes: 
  "writes (remove_child_locs (the |h  get_parent child|r) |h  get_owner_document (cast child)|r)
(remove child) h h'"
  by(auto simp add: remove_def intro!: writes_bind_pure split: option.splits)

lemma remove_child_children_subset:
  assumes "h  remove_child parent child h h'"
    and "h  get_child_nodes ptr r children"
    and "h'  get_child_nodes ptr r children'"
    and known_ptrs: "known_ptrs h"
    and type_wf: "type_wf h"
  shows "set children'  set children"
proof -
  obtain ptr_children owner_document h2 disc_nodes where
    owner_document: "h  get_owner_document (cast child) r owner_document" and
    ptr_children: "h  get_child_nodes parent r ptr_children" and
    disc_nodes: "h  get_disconnected_nodes owner_document r disc_nodes" and
    h2: "h  set_disconnected_nodes owner_document (child # disc_nodes) h h2" and
    h': "h2  set_child_nodes parent (remove1 child ptr_children) h h'"
    using assms(1)
    by(auto simp add: remove_child_def 
                 elim!: bind_returns_heap_E 
                 dest!: pure_returns_heap_eq[rotated, OF get_owner_document_pure] 
                        pure_returns_heap_eq[rotated, OF get_disconnected_nodes_pure] 
                        pure_returns_heap_eq[rotated, OF get_child_nodes_pure] 
                 split: if_splits)
  have "parent |∈| object_ptr_kinds h"
    using get_child_nodes_ptr_in_heap ptr_children by blast
  have "object_ptr_kinds h = object_ptr_kinds h2"
    apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'", 
                                      OF set_disconnected_nodes_writes h2])
    using set_disconnected_nodes_pointers_preserved set_child_nodes_pointers_preserved 
    by (auto simp add: reflp_def transp_def)
  have "type_wf h2"
    using type_wf writes_small_big[where P="λh h'. type_wf h  type_wf h'", 
                                         OF set_disconnected_nodes_writes h2]
      using  set_disconnected_nodes_types_preserved  
      by(auto simp add: reflp_def transp_def)
  have "h2  get_child_nodes ptr r children"
   using get_child_nodes_reads set_disconnected_nodes_writes h2 assms(2)
      apply(rule reads_writes_separate_forwards)
      by (simp add: set_disconnected_nodes_get_child_nodes)
  moreover have "h2  get_child_nodes parent r ptr_children"
    using get_child_nodes_reads set_disconnected_nodes_writes h2 ptr_children
      apply(rule reads_writes_separate_forwards)
      by (simp add: set_disconnected_nodes_get_child_nodes)
    moreover have 
      "ptr  parent  h2  get_child_nodes ptr r children = h'  get_child_nodes ptr r children"
      using get_child_nodes_reads set_child_nodes_writes h'
      apply(rule reads_writes_preserved)
      by (metis set_child_nodes_get_child_nodes_different_pointers)
  moreover have "h'  get_child_nodes parent r remove1 child ptr_children"
    using h' set_child_nodes_get_child_nodes  known_ptrs type_wf known_ptrs_known_ptr 
              parent |∈| object_ptr_kinds h object_ptr_kinds h = object_ptr_kinds h2 type_wf h2 
              by fast
  moreover have "set ( remove1 child ptr_children)  set ptr_children"
    by (simp add: set_remove1_subset)
  ultimately show ?thesis
    by (metis assms(3) order_refl returns_result_eq)
qed


lemma remove_child_pointers_preserved:
  assumes "w  remove_child_locs ptr owner_document"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms
  using set_child_nodes_pointers_preserved
  using set_disconnected_nodes_pointers_preserved
  unfolding remove_child_locs_def
  by auto

lemma remove_child_types_preserved:
  assumes "w  remove_child_locs ptr owner_document"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  using assms
  using set_child_nodes_types_preserved
  using set_disconnected_nodes_types_preserved
  unfolding remove_child_locs_def
  by auto
end

locale l_remove_child = l_type_wf + l_known_ptrs + l_remove_child_defs + l_get_owner_document_defs 
                      + l_get_child_nodes_defs + l_get_disconnected_nodes_defs +
  assumes remove_child_writes: 
    "writes (remove_child_locs object_ptr |h  get_owner_document (cast child)|r)
(remove_child object_ptr child) h h'"
  assumes remove_child_pointers_preserved: 
  "w  remove_child_locs ptr owner_document  h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes remove_child_types_preserved: 
  "w  remove_child_locs ptr owner_document  h  w h h'  type_wf h = type_wf h'"
  assumes remove_child_in_disconnected_nodes:
    "known_ptrs h  h  remove_child ptr child h h'
     h  get_owner_document (cast child) r owner_document
     h'  get_disconnected_nodes owner_document r disc_nodes
     child  set disc_nodes"
  assumes remove_child_ptr_in_heap: "h  ok (remove_child ptr child)  ptr |∈| object_ptr_kinds h"
  assumes remove_child_child_in_heap: "h  remove_child ptr' child h h'  child |∈| node_ptr_kinds h"
  assumes remove_child_children_subset:
    "known_ptrs h  type_wf h  h  remove_child parent child h h'
     h  get_child_nodes ptr r children
     h'  get_child_nodes ptr r children'
     set children'  set children"

locale l_remove


global_interpretation l_remove_childCore_DOM_defs get_child_nodes get_child_nodes_locs set_child_nodes 
                                                set_child_nodes_locs get_parent get_parent_locs 
                                                get_owner_document get_disconnected_nodes 
                                                get_disconnected_nodes_locs set_disconnected_nodes 
                                                set_disconnected_nodes_locs
  defines remove = 
    "l_remove_childCore_DOM_defs.a_remove get_child_nodes set_child_nodes get_parent get_owner_document 
                                        get_disconnected_nodes set_disconnected_nodes"
  and remove_child = 
    "l_remove_childCore_DOM_defs.a_remove_child get_child_nodes set_child_nodes get_owner_document 
                                              get_disconnected_nodes set_disconnected_nodes"
  and remove_child_locs = 
    "l_remove_childCore_DOM_defs.a_remove_child_locs set_child_nodes_locs set_disconnected_nodes_locs"
  .                                                                
interpretation
  i_remove_child?: l_remove_childCore_DOM get_child_nodes get_child_nodes_locs set_child_nodes 
                   set_child_nodes_locs get_parent get_parent_locs get_owner_document 
                   get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes 
                   set_disconnected_nodes_locs remove_child remove_child_locs remove type_wf 
                   known_ptr known_ptrs
  using instances
  apply(simp add: l_remove_childCore_DOM_def l_remove_childCore_DOM_axioms_def)
  by(simp add: remove_child_def remove_child_locs_def remove_def)
declare l_remove_childCore_DOM_axioms[instances]

lemma remove_child_is_l_remove_child [instances]: 
  "l_remove_child type_wf known_ptr known_ptrs remove_child remove_child_locs get_owner_document 
                  get_child_nodes get_disconnected_nodes"
  using instances
  apply(auto simp add: l_remove_child_def l_remove_child_axioms_def)[1] (*slow, ca 1min *)
  using remove_child_pointers_preserved apply(blast)
  using remove_child_pointers_preserved apply(blast)
  using remove_child_types_preserved apply(blast)
  using remove_child_types_preserved apply(blast)
  using remove_child_in_disconnected_nodes apply(blast)
  using remove_child_ptr_in_heap  apply(blast)
  using remove_child_child_in_heap  apply(blast)
  using remove_child_children_subset  apply(blast)
  done



subsubsection ‹adopt\_node›

locale l_adopt_nodeCore_DOM_defs =
  l_get_owner_document_defs get_owner_document +
  l_get_parent_defs get_parent get_parent_locs +
  l_remove_child_defs remove_child remove_child_locs +
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs
  for get_owner_document :: "(_::linorder) object_ptr  ((_) heap, exception, (_) document_ptr) prog"
  and get_parent :: "(_) node_ptr  ((_) heap, exception, (_) object_ptr option) prog"
  and get_parent_locs :: "((_) heap  (_) heap  bool) set"
  and remove_child :: "(_) object_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and remove_child_locs :: "(_) object_ptr  (_) document_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"
begin
definition a_adopt_node :: "(_) document_ptr  (_) node_ptr  (_, unit) dom_prog"
  where
    "a_adopt_node document node = do {
      old_document  get_owner_document (cast node);
      parent_opt  get_parent node;
      (case parent_opt of
        Some parent  do {
          remove_child parent node
        } | None  do {
          return ()
        });
      (if document  old_document then do {
        old_disc_nodes  get_disconnected_nodes old_document;
        set_disconnected_nodes old_document (remove1 node old_disc_nodes);
        disc_nodes  get_disconnected_nodes document;
        set_disconnected_nodes document (node # disc_nodes)
      } else do {
        return ()
      })
    }"

definition 
  a_adopt_node_locs :: "(_) object_ptr option  (_) document_ptr  (_) document_ptr  (_, unit) dom_prog set"
  where
    "a_adopt_node_locs parent owner_document document_ptr = 
    ((if parent = None 
      then {} 
      else remove_child_locs (the parent) owner_document)  set_disconnected_nodes_locs document_ptr 
                                                           set_disconnected_nodes_locs owner_document)"
end

locale l_adopt_node_defs =
  fixes 
  adopt_node :: "(_) document_ptr  (_) node_ptr  (_, unit) dom_prog"
  fixes 
  adopt_node_locs :: "(_) object_ptr option  (_) document_ptr  (_) document_ptr  (_, unit) dom_prog set"

global_interpretation l_adopt_nodeCore_DOM_defs get_owner_document get_parent get_parent_locs remove_child 
                                              remove_child_locs get_disconnected_nodes 
                                              get_disconnected_nodes_locs set_disconnected_nodes 
                                              set_disconnected_nodes_locs
  defines adopt_node = "l_adopt_nodeCore_DOM_defs.a_adopt_node get_owner_document get_parent remove_child 
                                                             get_disconnected_nodes set_disconnected_nodes"
      and adopt_node_locs = "l_adopt_nodeCore_DOM_defs.a_adopt_node_locs 
                                                      remove_child_locs set_disconnected_nodes_locs"
  .

locale l_adopt_nodeCore_DOM =
  l_adopt_nodeCore_DOM_defs
    get_owner_document get_parent get_parent_locs remove_child remove_child_locs get_disconnected_nodes 
                       get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
  + l_adopt_node_defs
    adopt_node adopt_node_locs
  + l_get_owner_document
    get_owner_document
  + l_get_parentCore_DOM
    known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  + l_remove_childCore_DOM
    get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs get_parent 
    get_parent_locs get_owner_document get_disconnected_nodes get_disconnected_nodes_locs 
    set_disconnected_nodes set_disconnected_nodes_locs remove_child remove_child_locs remove type_wf 
    known_ptr known_ptrs
  + l_set_disconnected_nodes_get_disconnected_nodes
    type_wf get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes 
    set_disconnected_nodes_locs
  for get_owner_document :: "(_::linorder) object_ptr  ((_) heap, exception, (_) document_ptr) prog"
  and get_parent :: "(_) node_ptr  ((_) heap, exception, (_) object_ptr option) prog"
  and get_parent_locs :: "((_) heap  (_) heap  bool) set"
  and remove_child :: "(_) object_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and remove_child_locs :: "(_) object_ptr  (_) document_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 adopt_node :: "(_) document_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and adopt_node_locs :: "(_) object_ptr option  (_) document_ptr  (_) document_ptr 
                           ((_) heap, exception, unit) prog set"
  and known_ptr :: "(_) 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 set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
  and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
  and remove :: "(_) node_ptr  ((_) heap, exception, unit) prog" +
  assumes adopt_node_impl: "adopt_node = a_adopt_node"
  assumes adopt_node_locs_impl: "adopt_node_locs = a_adopt_node_locs"
begin
lemmas adopt_node_def = a_adopt_node_def[folded adopt_node_impl]
lemmas adopt_node_locs_def = a_adopt_node_locs_def[folded adopt_node_locs_impl]

lemma adopt_node_writes:
  shows "writes (adopt_node_locs |h  get_parent node|r |h 
          get_owner_document (cast node)|r document_ptr) (adopt_node document_ptr node) h h'"
  apply(auto simp add: adopt_node_def adopt_node_locs_def 
             intro!: writes_bind_pure[OF get_owner_document_pure] writes_bind_pure[OF get_parent_pure] 
                     writes_bind_pure[OF get_disconnected_nodes_pure] 
             split: option.splits)[1]
  apply(auto intro!: writes_bind)[1]
  apply (simp add: set_disconnected_nodes_writes writes_union_right_I)
    apply (simp add: set_disconnected_nodes_writes writes_union_left_I writes_union_right_I)
   apply(auto intro!: writes_bind)[1]
  apply (metis (no_types, lifting) remove_child_writes select_result_I2 writes_union_left_I)
    apply (simp add: set_disconnected_nodes_writes writes_union_right_I)
  by(auto intro: writes_subset[OF set_disconnected_nodes_writes] writes_subset[OF remove_child_writes])

lemma adopt_node_children_subset:
  assumes "h  adopt_node owner_document node h h'"
    and "h  get_child_nodes ptr r children"
    and "h'  get_child_nodes ptr r children'"
    and known_ptrs: "known_ptrs h"
    and type_wf: "type_wf h"
  shows "set children'  set children"
proof -
  obtain old_document parent_opt h2 where
    old_document: "h  get_owner_document (cast node) r old_document" and
    parent_opt: "h  get_parent node r parent_opt" and
    h2: "h  (case parent_opt of Some parent  do { remove_child parent node } |
None  do { return ()}) h h2"
    and
    h': "h2  (if owner_document  old_document then do {
        old_disc_nodes  get_disconnected_nodes old_document;
        set_disconnected_nodes old_document (remove1 node old_disc_nodes);
        disc_nodes  get_disconnected_nodes owner_document;
        set_disconnected_nodes owner_document (node # disc_nodes)
      } else do { return () }) h h'"
    using assms(1)
    by(auto simp add: adopt_node_def 
            elim!: bind_returns_heap_E 
            dest!: pure_returns_heap_eq[rotated, OF get_owner_document_pure] 
                   pure_returns_heap_eq[rotated, OF get_parent_pure])

  have "h2  get_child_nodes ptr r children'"
  proof (cases "owner_document  old_document")
    case True
    then obtain h3 old_disc_nodes disc_nodes where
      old_disc_nodes: "h2  get_disconnected_nodes old_document r old_disc_nodes" and
      h3: "h2  set_disconnected_nodes old_document (remove1 node old_disc_nodes) h h3" and
      old_disc_nodes: "h3  get_disconnected_nodes owner_document r disc_nodes" and
      h': "h3  set_disconnected_nodes owner_document (node # disc_nodes) h h'"
      using h'
      by(auto elim!: bind_returns_heap_E 
                     bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] ) 
    have "h3  get_child_nodes ptr r children'"
      using get_child_nodes_reads set_disconnected_nodes_writes h' assms(3)
      apply(rule reads_writes_separate_backwards)
      by (simp add: set_disconnected_nodes_get_child_nodes)
    show ?thesis
      using get_child_nodes_reads set_disconnected_nodes_writes h3 h3  get_child_nodes ptr r children'
      apply(rule reads_writes_separate_backwards)
      by (simp add: set_disconnected_nodes_get_child_nodes)
  next
    case False
    then show ?thesis
      using h' assms(3) by(auto)
  qed

  show ?thesis
  proof (insert h2, induct parent_opt)
    case None
    then show ?case
      using assms
      by(auto dest!: returns_result_eq[OF h2  get_child_nodes ptr r children'])
  next
    case (Some option)
    then show ?case 
      using assms(2) h2  get_child_nodes ptr r children' remove_child_children_subset known_ptrs
        type_wf
      by simp
  qed
qed

lemma adopt_node_child_in_heap:
  assumes "h  ok (adopt_node document_ptr child)"
  shows "child |∈| node_ptr_kinds h"
  using assms
  apply(auto simp add: adopt_node_def elim!: bind_is_OK_E)[1]
  using get_owner_document_pure get_parent_ptr_in_heap pure_returns_heap_eq
  by fast

lemma adopt_node_pointers_preserved:
  assumes "w  adopt_node_locs parent owner_document document_ptr"
  assumes "h  w h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms
  using set_disconnected_nodes_pointers_preserved
  using remove_child_pointers_preserved
  unfolding adopt_node_locs_def
  by (auto split: if_splits)

lemma adopt_node_types_preserved:
  assumes "w  adopt_node_locs parent owner_document document_ptr"
  assumes "h  w h h'"
  shows "type_wf h = type_wf h'"
  using assms
  using remove_child_types_preserved
  using set_disconnected_nodes_types_preserved
  unfolding adopt_node_locs_def
  by (auto split: if_splits)
end

locale l_adopt_node = l_type_wf + l_known_ptrs + l_get_parent_defs + l_adopt_node_defs +
  l_get_child_nodes_defs + l_get_owner_document_defs +
  assumes adopt_node_writes: 
  "writes (adopt_node_locs |h  get_parent node|r 
           |h  get_owner_document (cast node)|r document_ptr) (adopt_node document_ptr node) h h'"
  assumes adopt_node_pointers_preserved: 
  "w  adopt_node_locs parent owner_document document_ptr 
    h  w h h'  object_ptr_kinds h = object_ptr_kinds h'"
  assumes adopt_node_types_preserved: 
  "w  adopt_node_locs parent owner_document document_ptr 
    h  w h h'  type_wf h = type_wf h'"
  assumes adopt_node_child_in_heap: 
  "h  ok (adopt_node document_ptr child)  child |∈| node_ptr_kinds h"
  assumes adopt_node_children_subset:
  "h  adopt_node owner_document node h h'  h  get_child_nodes ptr r children 
      h'  get_child_nodes ptr r children' 
      known_ptrs h  type_wf h  set children'  set children"

interpretation
  i_adopt_node?: l_adopt_nodeCore_DOM get_owner_document get_parent get_parent_locs remove_child 
                 remove_child_locs get_disconnected_nodes get_disconnected_nodes_locs 
                 set_disconnected_nodes set_disconnected_nodes_locs adopt_node adopt_node_locs 
                 known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs set_child_nodes 
                 set_child_nodes_locs remove
  apply(unfold_locales)
  by(auto simp add: adopt_node_def adopt_node_locs_def)                     
declare l_adopt_nodeCore_DOM_axioms[instances]


lemma adopt_node_is_l_adopt_node [instances]: 
  "l_adopt_node type_wf known_ptr known_ptrs get_parent adopt_node adopt_node_locs get_child_nodes 
                get_owner_document"
  using instances
  by (simp add: l_adopt_node_axioms_def adopt_node_child_in_heap adopt_node_children_subset 
                adopt_node_pointers_preserved adopt_node_types_preserved adopt_node_writes 
                l_adopt_node_def)



subsubsection ‹insert\_before›
                                                       
locale l_insert_beforeCore_DOM_defs =
  l_get_parent_defs get_parent get_parent_locs
  + l_get_child_nodes_defs get_child_nodes get_child_nodes_locs
  + l_set_child_nodes_defs set_child_nodes set_child_nodes_locs
  + l_get_ancestors_defs get_ancestors get_ancestors_locs
  + l_adopt_node_defs adopt_node adopt_node_locs
  + l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs
  + l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs
  + l_get_owner_document_defs get_owner_document
  for get_parent :: "(_) node_ptr  ((_) heap, exception, (_::linorder) 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 set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
  and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
  and get_ancestors :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
  and get_ancestors_locs :: "((_) heap  (_) heap  bool) set"
  and adopt_node :: "(_) document_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and adopt_node_locs :: "(_) object_ptr option  (_) document_ptr  (_) document_ptr 
                                                 ((_) heap, exception, unit) prog 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 get_disconnected_nodes :: "(_) document_ptr  ((_) heap, exception, (_) node_ptr list) prog"
  and get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"
  and get_owner_document :: "(_) object_ptr  ((_) heap, exception, (_) document_ptr) prog"
begin

definition a_next_sibling :: "(_) node_ptr  (_, (_) node_ptr option) dom_prog"
  where
    "a_next_sibling node_ptr = do {
      parent_opt  get_parent node_ptr;
      (case parent_opt of
        Some parent  do {
          children  get_child_nodes parent;
          (case (dropWhile (λptr. ptr = node_ptr) (dropWhile (λptr. ptr  node_ptr) children)) of
            x#_  return (Some x)
          | []  return None)}
      | None  return None)
    }"

fun insert_before_list :: "'xyz  'xyz option  'xyz list  'xyz list"
  where
    "insert_before_list v (Some reference) (x#xs) = (if reference = x
      then v#x#xs else x # insert_before_list v (Some reference) xs)"
    | "insert_before_list v (Some _) [] = [v]"
    | "insert_before_list v None xs = xs @ [v]"

definition a_insert_node :: "(_) object_ptr  (_) node_ptr  (_) node_ptr option
   (_, unit) dom_prog"
  where
    "a_insert_node ptr new_child reference_child_opt = do {
      children  get_child_nodes ptr;
      set_child_nodes ptr (insert_before_list new_child reference_child_opt children)
    }"

definition a_ensure_pre_insertion_validity :: "(_) node_ptr  (_) object_ptr
   (_) node_ptr option  (_, unit) dom_prog"
  where
    "a_ensure_pre_insertion_validity node parent child_opt = do {
      (if is_character_data_ptr_kind parent
        then error HierarchyRequestError else return ());
      ancestors  get_ancestors parent;
      (if cast node  set ancestors then error HierarchyRequestError else return ());
      (case child_opt of
        Some child  do {
          child_parent  get_parent child;
          (if child_parent  Some parent then error NotFoundError else return ())}
      | None  return ());
      children  get_child_nodes parent;
      (if children  []  is_document_ptr parent
        then error HierarchyRequestError else return ());
      (if is_character_data_ptr node  is_document_ptr parent
        then error HierarchyRequestError else return ())
    }"

definition a_insert_before :: "(_) object_ptr  (_) node_ptr
   (_) node_ptr option  (_, unit) dom_prog"
  where
    "a_insert_before ptr node child = do {
      a_ensure_pre_insertion_validity node ptr child;
      reference_child  (if Some node = child
        then a_next_sibling node                                         
        else return child);
      owner_document  get_owner_document ptr;
      adopt_node owner_document node;
      disc_nodes  get_disconnected_nodes owner_document;
      set_disconnected_nodes owner_document (remove1 node disc_nodes);
      a_insert_node ptr node reference_child
    }"

definition a_insert_before_locs :: "(_) object_ptr  (_) object_ptr option  (_) document_ptr 
                                                    (_) document_ptr  (_, unit) dom_prog set"
  where
    "a_insert_before_locs ptr old_parent child_owner_document ptr_owner_document =
      adopt_node_locs old_parent child_owner_document ptr_owner_document 
      set_child_nodes_locs ptr 
      set_disconnected_nodes_locs ptr_owner_document"
end

locale l_insert_before_defs =
  fixes insert_before :: "(_) object_ptr  (_) node_ptr  (_) node_ptr option  (_, unit) dom_prog"
  fixes insert_before_locs :: "(_) object_ptr  (_) object_ptr option  (_) document_ptr 
                                               (_) document_ptr  (_, unit) dom_prog set"

locale l_append_childCore_DOM_defs =
  l_insert_before_defs
begin
definition "a_append_child ptr child = insert_before ptr child None"
end

locale l_append_child_defs =
  fixes append_child :: "(_) object_ptr  (_) node_ptr  (_, unit) dom_prog"
                                                                 
locale l_insert_beforeCore_DOM =
  l_insert_beforeCore_DOM_defs
    get_parent get_parent_locs get_child_nodes get_child_nodes_locs set_child_nodes 
    set_child_nodes_locs get_ancestors get_ancestors_locs adopt_node adopt_node_locs 
    set_disconnected_nodes set_disconnected_nodes_locs get_disconnected_nodes 
    get_disconnected_nodes_locs get_owner_document
  + l_insert_before_defs
    insert_before insert_before_locs
  + l_append_child_defs
    append_child
  + l_set_child_nodes_get_child_nodes
    type_wf known_ptr get_child_nodes get_child_nodes_locs set_child_nodes set_child_nodes_locs
  + l_get_ancestors
    get_ancestors get_ancestors_locs
  + l_adopt_node
    type_wf known_ptr known_ptrs get_parent get_parent_locs adopt_node adopt_node_locs 
    get_child_nodes get_child_nodes_locs get_owner_document
  + l_set_disconnected_nodes
    type_wf set_disconnected_nodes set_disconnected_nodes_locs
  + l_get_disconnected_nodes
    type_wf get_disconnected_nodes get_disconnected_nodes_locs
  + l_get_owner_document
    get_owner_document
  + l_get_parentCore_DOM
    known_ptr type_wf get_child_nodes get_child_nodes_locs known_ptrs get_parent get_parent_locs
  + l_set_disconnected_nodes_get_child_nodes
    set_disconnected_nodes set_disconnected_nodes_locs get_child_nodes get_child_nodes_locs
  for get_parent :: "(_) node_ptr  ((_) heap, exception, (_::linorder) 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 set_child_nodes :: "(_) object_ptr  (_) node_ptr list  ((_) heap, exception, unit) prog"
  and set_child_nodes_locs :: "(_) object_ptr  ((_) heap, exception, unit) prog set"
  and get_ancestors :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
  and get_ancestors_locs :: "((_) heap  (_) heap  bool) set"
  and adopt_node :: "(_) document_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and adopt_node_locs :: "(_) object_ptr option  (_) document_ptr  (_) document_ptr 
                                                 ((_) heap, exception, unit) prog 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 get_disconnected_nodes :: "(_) document_ptr  ((_) heap, exception, (_) node_ptr list) prog"
  and get_disconnected_nodes_locs :: "(_) document_ptr  ((_) heap  (_) heap  bool) set"
  and get_owner_document :: "(_) object_ptr  ((_) heap, exception, (_) document_ptr) prog"
    and insert_before ::
    "(_) object_ptr  (_) node_ptr  (_) node_ptr option  ((_) heap, exception, unit) prog"
  and insert_before_locs :: "(_) object_ptr  (_) object_ptr option  (_) document_ptr 
                                             (_) document_ptr  (_, unit) dom_prog set"
  and append_child :: "(_) object_ptr  (_) node_ptr  ((_) heap, exception, unit) prog"
  and type_wf :: "(_) heap  bool"
  and known_ptr :: "(_) object_ptr  bool"
  and known_ptrs :: "(_) heap  bool" +
  assumes insert_before_impl: "insert_before = a_insert_before"
  assumes insert_before_locs_impl: "insert_before_locs = a_insert_before_locs"
begin
lemmas insert_before_def = a_insert_before_def[folded insert_before_impl]
lemmas insert_before_locs_def = a_insert_before_locs_def[folded insert_before_locs_impl]

lemma next_sibling_pure [simp]:
  "pure (a_next_sibling new_child) h"
  by(auto simp add: a_next_sibling_def get_parent_pure intro!: bind_pure_I split: option.splits list.splits)

lemma insert_before_list_in_set: "x  set (insert_before_list v ref xs)  x = v  x  set xs"
  apply(induct v ref xs rule: insert_before_list.induct)
  by(auto)

lemma insert_before_list_distinct: "x  set xs  distinct xs  distinct (insert_before_list x ref xs)"
  apply(induct x ref xs rule: insert_before_list.induct)
  by(auto simp add: insert_before_list_in_set)

lemma insert_before_list_subset: "set xs  set (insert_before_list x ref xs)"
  apply(induct x ref xs rule: insert_before_list.induct)
  by(auto)

lemma insert_before_list_node_in_set: "x  set (insert_before_list x ref xs)"
  apply(induct x ref xs rule: insert_before_list.induct)
  by(auto)

lemma insert_node_writes: 
  "writes (set_child_nodes_locs ptr) (a_insert_node ptr new_child reference_child_opt) h h'"
  by(auto simp add: a_insert_node_def set_child_nodes_writes 
          intro!: writes_bind_pure[OF get_child_nodes_pure])

lemma ensure_pre_insertion_validity_pure [simp]:
  "pure (a_ensure_pre_insertion_validity node ptr child) h"
  by(auto simp add: a_ensure_pre_insertion_validity_def 
          intro!: bind_pure_I 
          split: option.splits)

lemma insert_before_reference_child_not_in_children:
  assumes "h  get_parent child r Some parent"
    and "ptr  parent"
    and "¬is_character_data_ptr_kind ptr"
    and "h  get_ancestors ptr r ancestors"
    and "cast node  set ancestors"
  shows "h  insert_before ptr node (Some child) e NotFoundError"
proof -
  have "h  a_ensure_pre_insertion_validity node ptr (Some child) e NotFoundError"
    using assms unfolding insert_before_def a_ensure_pre_insertion_validity_def
    by auto (simp | rule bind_returns_error_I2)+
  then show ?thesis
    unfolding insert_before_def by auto
qed

lemma insert_before_ptr_in_heap:
  assumes "h  ok (insert_before ptr node reference_child)"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  apply(auto simp add: insert_before_def elim!: bind_is_OK_E)[1]
  by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_result_I
      local.get_owner_document_ptr_in_heap next_sibling_pure pure_returns_heap_eq return_returns_heap)

lemma insert_before_child_in_heap:
  assumes "h  ok (insert_before ptr node reference_child)"
  shows "node |∈| node_ptr_kinds h"
  using assms
  apply(auto simp add: insert_before_def elim!: bind_is_OK_E)[1]
  by (metis (mono_tags, lifting) ensure_pre_insertion_validity_pure is_OK_returns_heap_I 
            l_get_owner_document.get_owner_document_pure local.adopt_node_child_in_heap 
            local.l_get_owner_document_axioms next_sibling_pure pure_returns_heap_eq return_pure)

lemma insert_node_children_remain_distinct:
    assumes insert_node: "h  a_insert_node ptr new_child reference_child_opt h h2"
    and "h  get_child_nodes ptr r children"
    and "new_child  set children"
    and "ptr children. h  get_child_nodes ptr r children  distinct children"
    and known_ptr: "known_ptr ptr"
    and type_wf: "type_wf h"
  shows "ptr children. h2  get_child_nodes ptr r children  distinct children"
proof -
  fix ptr' children'
  assume a1: "h2  get_child_nodes ptr' r children'"
  then show "distinct children'"
  proof (cases "ptr = ptr'")
    case True
    have "h2  get_child_nodes ptr r (insert_before_list new_child reference_child_opt children)"
      using assms(1) assms(2) apply(auto simp add: a_insert_node_def elim!: bind_returns_heap_E)[1]
      using returns_result_eq set_child_nodes_get_child_nodes known_ptr type_wf
      using pure_returns_heap_eq by fastforce
    then show ?thesis
      using True a1 assms(2) assms(3) assms(4) insert_before_list_distinct returns_result_eq 
      by fastforce
  next
    case False
    have "h  get_child_nodes ptr' r children'"
      using  get_child_nodes_reads insert_node_writes insert_node a1
      apply(rule reads_writes_separate_backwards)
      by (meson False set_child_nodes_get_child_nodes_different_pointers)
    then show ?thesis
      using assms(4) by blast
  qed
qed
                                               
lemma insert_before_writes: 
  "writes (insert_before_locs ptr |h  get_parent child|r 
       |h  get_owner_document (cast child)|r |h  get_owner_document ptr|r) (insert_before ptr child ref) h h'"
  apply(auto simp add: insert_before_def insert_before_locs_def a_insert_node_def 
      intro!: writes_bind)[1]
       apply (metis (no_types, opaque_lifting) ensure_pre_insertion_validity_pure local.adopt_node_writes 
                    local.get_owner_document_pure next_sibling_pure pure_returns_heap_eq 
                    select_result_I2 sup_commute writes_union_right_I)
      apply (metis (no_types, opaque_lifting) ensure_pre_insertion_validity_pure next_sibling_pure 
                   pure_returns_heap_eq select_result_I2 set_disconnected_nodes_writes 
                   writes_union_right_I)
     apply (simp add: set_child_nodes_writes writes_union_left_I writes_union_right_I)
    apply (metis (no_types, opaque_lifting) adopt_node_writes ensure_pre_insertion_validity_pure 
                 get_owner_document_pure pure_returns_heap_eq select_result_I2 writes_union_left_I)
   apply (metis (no_types, opaque_lifting) ensure_pre_insertion_validity_pure pure_returns_heap_eq 
                select_result_I2 set_disconnected_nodes_writes writes_union_right_I)
  by (simp add: set_child_nodes_writes writes_union_left_I writes_union_right_I)                      
end


locale l_append_childCore_DOM =
  l_append_child_defs +
  l_append_childCore_DOM_defs +     
  assumes append_child_impl: "append_child = a_append_child"
begin

lemmas append_child_def = a_append_child_def[folded append_child_impl]
end

locale l_insert_before = l_insert_before_defs

locale l_append_child = l_append_child_defs

global_interpretation l_insert_beforeCore_DOM_defs get_parent get_parent_locs get_child_nodes 
   get_child_nodes_locs set_child_nodes set_child_nodes_locs get_ancestors get_ancestors_locs 
   adopt_node adopt_node_locs set_disconnected_nodes set_disconnected_nodes_locs 
   get_disconnected_nodes get_disconnected_nodes_locs get_owner_document
  defines
    next_sibling = "l_insert_beforeCore_DOM_defs.a_next_sibling get_parent get_child_nodes" and
    insert_node = "l_insert_beforeCore_DOM_defs.a_insert_node get_child_nodes set_child_nodes" and
    ensure_pre_insertion_validity = "l_insert_beforeCore_DOM_defs.a_ensure_pre_insertion_validity 
                                                     get_parent get_child_nodes get_ancestors" and
    insert_before = "l_insert_beforeCore_DOM_defs.a_insert_before get_parent get_child_nodes 
                                   set_child_nodes get_ancestors adopt_node set_disconnected_nodes 
                                   get_disconnected_nodes get_owner_document" and
    insert_before_locs = "l_insert_beforeCore_DOM_defs.a_insert_before_locs set_child_nodes_locs 
                                                        adopt_node_locs set_disconnected_nodes_locs"
  .

global_interpretation l_append_childCore_DOM_defs insert_before
  defines append_child = "l_append_childCore_DOM_defs.a_append_child insert_before"
  .

interpretation                                           
  i_insert_before?: l_insert_beforeCore_DOM get_parent get_parent_locs get_child_nodes 
  get_child_nodes_locs set_child_nodes set_child_nodes_locs get_ancestors get_ancestors_locs 
  adopt_node adopt_node_locs set_disconnected_nodes set_disconnected_nodes_locs get_disconnected_nodes 
  get_disconnected_nodes_locs get_owner_document insert_before insert_before_locs append_child 
  type_wf known_ptr known_ptrs
  apply(simp add: l_insert_beforeCore_DOM_def l_insert_beforeCore_DOM_axioms_def instances)
  by (simp add: insert_before_def insert_before_locs_def)
declare l_insert_beforeCore_DOM_axioms[instances]

interpretation i_append_child?: l_append_childCore_DOM append_child insert_before insert_before_locs
  apply(simp add: l_append_childCore_DOM_def instances append_child_def)
  done
declare l_append_childCore_DOM_axioms[instances]




subsubsection ‹create\_element›

locale l_create_elementCore_DOM_defs =
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs +
  l_set_tag_name_defs set_tag_name set_tag_name_locs
  for 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"
begin
definition a_create_element :: "(_) document_ptr  tag_name  (_, (_) element_ptr) dom_prog"
  where
    "a_create_element document_ptr tag = do {
      new_element_ptr  new_element;
      set_tag_name new_element_ptr tag;
      disc_nodes  get_disconnected_nodes document_ptr;
      set_disconnected_nodes document_ptr (cast new_element_ptr # disc_nodes);
      return new_element_ptr
    }"
end

locale l_create_element_defs =
  fixes create_element :: "(_) document_ptr  tag_name  (_, (_) element_ptr) dom_prog"

global_interpretation l_create_elementCore_DOM_defs get_disconnected_nodes get_disconnected_nodes_locs 
                                                  set_disconnected_nodes set_disconnected_nodes_locs 
  set_tag_name set_tag_name_locs
  defines 
  create_element = "l_create_elementCore_DOM_defs.a_create_element get_disconnected_nodes 
                                                                set_disconnected_nodes set_tag_name"
  .

locale l_create_elementCore_DOM =
  l_create_elementCore_DOM_defs get_disconnected_nodes get_disconnected_nodes_locs
  set_disconnected_nodes set_disconnected_nodes_locs set_tag_name set_tag_name_locs +
  l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_tag_name type_wf set_tag_name set_tag_name_locs +
  l_create_element_defs create_element +
  l_known_ptr known_ptr
  for 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 type_wf :: "(_) heap  bool"
  and create_element :: "(_) document_ptr  char list  ((_) heap, exception, (_) element_ptr) prog"
  and known_ptr :: "(_) object_ptr  bool" +
  assumes known_ptr_impl: "known_ptr = a_known_ptr"
  assumes create_element_impl: "create_element = a_create_element"
begin
lemmas create_element_def = a_create_element_def[folded create_element_impl]

lemma create_element_document_in_heap:
  assumes "h  ok (create_element document_ptr tag)"
  shows "document_ptr |∈| document_ptr_kinds h"
proof -
  obtain h' where "h  create_element document_ptr tag h h'"
    using assms(1)
    by auto
  then
  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'"
    by(auto simp add: create_element_def
            elim!: bind_returns_heap_E 
                   bind_returns_heap_E2[rotated, OF get_disconnected_nodes_pure, rotated] )

  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
  
  moreover 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)
  moreover have "document_ptr |∈| document_ptr_kinds h3"
    by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)

  ultimately show ?thesis
    by (auto simp add: document_ptr_kinds_def)
qed

lemma create_element_known_ptr:
  assumes "h  create_element document_ptr tag r new_element_ptr"
  shows "known_ptr (cast new_element_ptr)"
proof -
  have "is_element_ptr new_element_ptr"
    using assms
    apply(auto simp add: create_element_def elim!: bind_returns_result_E)[1]
    using new_element_is_element_ptr
    by blast
  then show ?thesis
    by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs)
qed
end

locale l_create_element = l_create_element_defs

interpretation
  i_create_element?: l_create_elementCore_DOM 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
  by(auto simp add: l_create_elementCore_DOM_def l_create_elementCore_DOM_axioms_def create_element_def instances)
declare l_create_elementCore_DOM_axioms[instances]


subsubsection ‹create\_character\_data›

locale l_create_character_dataCore_DOM_defs =
  l_set_val_defs set_val set_val_locs +
  l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_disconnected_nodes_defs set_disconnected_nodes set_disconnected_nodes_locs
  for 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"
begin
definition a_create_character_data :: "(_) document_ptr  string  (_, (_) character_data_ptr) dom_prog"
  where
    "a_create_character_data document_ptr text = do {
      new_character_data_ptr  new_character_data;
      set_val new_character_data_ptr text;
      disc_nodes  get_disconnected_nodes document_ptr;
      set_disconnected_nodes document_ptr (cast new_character_data_ptr # disc_nodes);
      return new_character_data_ptr
    }"
end

locale l_create_character_data_defs =
  fixes create_character_data :: "(_) document_ptr  string  (_, (_) character_data_ptr) dom_prog"

global_interpretation l_create_character_dataCore_DOM_defs set_val set_val_locs get_disconnected_nodes 
                     get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
  defines create_character_data = "l_create_character_dataCore_DOM_defs.a_create_character_data 
                                             set_val get_disconnected_nodes set_disconnected_nodes"
  .

locale l_create_character_dataCore_DOM =
  l_create_character_dataCore_DOM_defs set_val set_val_locs get_disconnected_nodes
  get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs +
  l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
  l_set_val type_wf set_val set_val_locs +
  l_create_character_data_defs create_character_data +
  l_known_ptr known_ptr
  for 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_val :: "(_) character_data_ptr  char list  ((_) heap, exception, unit) prog"
  and set_val_locs :: "(_) character_data_ptr  ((_) heap, exception, unit) prog set"
  and type_wf :: "(_) heap  bool"
  and create_character_data :: "(_) document_ptr  char list  ((_) heap, exception, (_) character_data_ptr) prog"
  and known_ptr :: "(_) object_ptr  bool" +
  assumes known_ptr_impl: "known_ptr = a_known_ptr"
  assumes create_character_data_impl: "create_character_data = a_create_character_data"
begin
lemmas create_character_data_def = a_create_character_data_def[folded create_character_data_impl] 

lemma create_character_data_document_in_heap:
  assumes "h  ok (create_character_data document_ptr text)"
  shows "document_ptr |∈| document_ptr_kinds h"
proof -
  obtain h' where "h  create_character_data document_ptr text h h'"
    using assms(1)
    by auto
  then
  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'"
    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 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
  
  moreover 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)
  moreover have "document_ptr |∈| document_ptr_kinds h3"
    by (meson disc_nodes_h3 is_OK_returns_result_I local.get_disconnected_nodes_ptr_in_heap)

  ultimately show ?thesis
    by (auto simp add: document_ptr_kinds_def)
qed

lemma create_character_data_known_ptr:
  assumes "h  create_character_data document_ptr text r new_character_data_ptr"
  shows "known_ptr (cast new_character_data_ptr)"
proof -
  have "is_character_data_ptr new_character_data_ptr"
    using assms
    apply(auto simp add: create_character_data_def elim!: bind_returns_result_E)[1]
    using new_character_data_is_character_data_ptr
    by blast
  then show ?thesis
    by(auto simp add: known_ptr_impl DocumentClass.known_ptr_defs CharacterDataClass.known_ptr_defs
        ElementClass.known_ptr_defs)
qed
end

locale l_create_character_data = l_create_character_data_defs

interpretation
  i_create_character_data?: l_create_character_dataCore_DOM 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
  by(auto simp add: l_create_character_dataCore_DOM_def l_create_character_dataCore_DOM_axioms_def
      create_character_data_def instances)
declare l_create_character_dataCore_DOM_axioms [instances]



subsubsection ‹create\_character\_data›

locale l_create_documentCore_DOM_defs
begin
definition a_create_document :: "(_, (_) document_ptr) dom_prog"
  where
    "a_create_document = new_document"
end

locale l_create_document_defs =
  fixes create_document :: "(_, (_) document_ptr) dom_prog"

global_interpretation l_create_documentCore_DOM_defs
  defines create_document = "l_create_documentCore_DOM_defs.a_create_document"
  .

locale l_create_documentCore_DOM =
  l_create_documentCore_DOM_defs +
  l_create_document_defs +
  assumes create_document_impl: "create_document = a_create_document"
begin
lemmas 
  create_document_def = create_document_impl[unfolded create_document_def, unfolded a_create_document_def]
end

locale l_create_document = l_create_document_defs

interpretation
  i_create_document?: l_create_documentCore_DOM create_document
  by(simp add: l_create_documentCore_DOM_def)
declare l_create_documentCore_DOM_axioms [instances]


subsubsection ‹tree\_order›

locale l_to_tree_orderCore_DOM_defs =
  l_get_child_nodes_defs get_child_nodes get_child_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"
begin
partial_function (dom_prog) a_to_tree_order :: "(_) object_ptr  (_, (_) object_ptr list) dom_prog"
  where
    "a_to_tree_order ptr = (do {
      children  get_child_nodes ptr;
      treeorders  map_M a_to_tree_order (map (cast) children);
      return (ptr # concat treeorders)
    })"
end

locale l_to_tree_order_defs =
  fixes to_tree_order :: "(_) object_ptr  (_, (_) object_ptr list) dom_prog"

global_interpretation l_to_tree_orderCore_DOM_defs get_child_nodes get_child_nodes_locs defines
  to_tree_order = "l_to_tree_orderCore_DOM_defs.a_to_tree_order get_child_nodes" .
declare a_to_tree_order.simps [code]

locale l_to_tree_orderCore_DOM =
  l_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs +
  l_to_tree_orderCore_DOM_defs get_child_nodes get_child_nodes_locs +
  l_to_tree_order_defs to_tree_order
  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 to_tree_order :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog" +
  assumes to_tree_order_impl: "to_tree_order = a_to_tree_order"
begin
lemmas to_tree_order_def = a_to_tree_order.simps[folded to_tree_order_impl]

lemma to_tree_order_pure [simp]: "pure (to_tree_order ptr) h"
proof -
  have "ptr h h' x. h  to_tree_order ptr r x  h  to_tree_order ptr h h'  h = h'"
  proof (induct rule: a_to_tree_order.fixp_induct[folded to_tree_order_impl])
    case 1
    then show ?case
      by (rule admissible_dom_prog)
  next
    case 2
    then show ?case
      by simp
  next
    case (3 f)
    then have "x h. pure (f x) h"
      by (metis is_OK_returns_heap_E is_OK_returns_result_E pure_def)
    then have "xs h. pure (map_M f xs) h"
      by(rule map_M_pure_I)
    then show ?case
      by(auto elim!: bind_returns_heap_E2)
  qed
  then show ?thesis
    unfolding pure_def
    by (metis is_OK_returns_heap_E is_OK_returns_result_E)
qed
end

locale l_to_tree_order =
  fixes to_tree_order :: "(_) object_ptr  (_, (_) object_ptr list) dom_prog"
  assumes to_tree_order_pure [simp]: "pure (to_tree_order ptr) h"

interpretation 
  i_to_tree_order?: l_to_tree_orderCore_DOM known_ptr type_wf get_child_nodes get_child_nodes_locs 
                    to_tree_order
  apply(unfold_locales)
  by (simp add: to_tree_order_def)
declare l_to_tree_orderCore_DOM_axioms[instances]

lemma to_tree_order_is_l_to_tree_order [instances]: "l_to_tree_order to_tree_order"
  using to_tree_order_pure l_to_tree_order_def by blast



subsubsection ‹first\_in\_tree\_order›

locale l_first_in_tree_orderCore_DOM_defs =
  l_to_tree_order_defs to_tree_order
  for to_tree_order :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
begin
definition a_first_in_tree_order :: "(_) object_ptr  ((_) object_ptr 
                                 (_, 'result option) dom_prog)  (_, 'result option) dom_prog"
  where
    "a_first_in_tree_order ptr f = (do {
      tree_order  to_tree_order ptr;
      results  map_filter_M f tree_order;
      (case results of
        []  return None
      | x#_ return (Some x))
    })"
end

locale l_first_in_tree_order_defs =
  fixes first_in_tree_order :: "(_) object_ptr  ((_) object_ptr  (_, 'result option) dom_prog) 
                                                (_, 'result option) dom_prog"

global_interpretation l_first_in_tree_orderCore_DOM_defs to_tree_order defines
  first_in_tree_order = "l_first_in_tree_orderCore_DOM_defs.a_first_in_tree_order to_tree_order" .

locale l_first_in_tree_orderCore_DOM =
  l_first_in_tree_orderCore_DOM_defs to_tree_order +
  l_first_in_tree_order_defs first_in_tree_order
  for to_tree_order :: "(_) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
  and first_in_tree_order :: "(_) object_ptr  ((_) object_ptr  ((_) heap, exception, 'result option) prog) 
                                              ((_) heap, exception, 'result option) prog" +
assumes first_in_tree_order_impl: "first_in_tree_order = a_first_in_tree_order"
begin
lemmas first_in_tree_order_def = first_in_tree_order_impl[unfolded a_first_in_tree_order_def]
end

locale l_first_in_tree_order

interpretation i_first_in_tree_order?:
  l_first_in_tree_orderCore_DOM to_tree_order first_in_tree_order
  by unfold_locales (simp add: first_in_tree_order_def)
declare l_first_in_tree_orderCore_DOM_axioms[instances]



subsubsection ‹get\_element\_by›

locale l_get_element_byCore_DOM_defs =
  l_first_in_tree_order_defs first_in_tree_order +
  l_to_tree_order_defs to_tree_order +
  l_get_attribute_defs get_attribute get_attribute_locs
  for to_tree_order :: "(_::linorder) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
  and first_in_tree_order :: "(_) object_ptr  ((_) object_ptr 
                               ((_) heap, exception, (_) element_ptr option) prog) 
                               ((_) heap, exception, (_) element_ptr option) prog"
  and get_attribute :: "(_) element_ptr  char list  ((_) heap, exception, char list option) prog"
  and get_attribute_locs :: "(_) element_ptr  ((_) heap  (_) heap  bool) set"
begin
definition a_get_element_by_id :: "(_) object_ptr  attr_value  (_, (_) element_ptr option) dom_prog"
  where
    "a_get_element_by_id ptr iden = first_in_tree_order ptr (λptr. (case cast ptr of
      Some element_ptr  do {
        id_opt  get_attribute element_ptr ''id'';
        (if id_opt = Some iden then return (Some element_ptr) else return None)
      }
    | _  return None
    ))"

definition a_get_elements_by_class_name :: "(_) object_ptr  attr_value  (_, (_) element_ptr list) dom_prog"
  where
    "a_get_elements_by_class_name ptr class_name = to_tree_order ptr 
      map_filter_M (λptr. (case cast ptr of
        Some element_ptr  do {
          class_name_opt  get_attribute element_ptr ''class'';
          (if class_name_opt = Some class_name then return (Some element_ptr) else return None)
        }
      | _  return None))"

definition a_get_elements_by_tag_name :: "(_) object_ptr  attr_value  (_, (_) element_ptr list) dom_prog"
  where
    "a_get_elements_by_tag_name ptr tag = to_tree_order ptr 
      map_filter_M (λptr. (case cast ptr of
        Some element_ptr  do {
          this_tag_name  get_M element_ptr tag_name;
          (if this_tag_name = tag then return (Some element_ptr) else return None)
        }
      | _  return None))"
end

locale l_get_element_by_defs =
  fixes get_element_by_id :: "(_) object_ptr  attr_value  (_, (_) element_ptr option) dom_prog"
  fixes get_elements_by_class_name :: "(_) object_ptr  attr_value  (_, (_) element_ptr list) dom_prog"
  fixes get_elements_by_tag_name :: "(_) object_ptr  attr_value  (_, (_) element_ptr list) dom_prog"

global_interpretation 
l_get_element_byCore_DOM_defs to_tree_order first_in_tree_order get_attribute get_attribute_locs 
defines                      
  get_element_by_id = "l_get_element_byCore_DOM_defs.a_get_element_by_id first_in_tree_order get_attribute" 
and
    get_elements_by_class_name = "l_get_element_byCore_DOM_defs.a_get_elements_by_class_name
to_tree_order get_attribute"
and
  get_elements_by_tag_name = "l_get_element_byCore_DOM_defs.a_get_elements_by_tag_name to_tree_order" .

locale l_get_element_byCore_DOM =
  l_get_element_byCore_DOM_defs to_tree_order first_in_tree_order get_attribute get_attribute_locs +
  l_get_element_by_defs get_element_by_id get_elements_by_class_name get_elements_by_tag_name +
  l_first_in_tree_orderCore_DOM to_tree_order first_in_tree_order +
  l_to_tree_order to_tree_order +
  l_get_attribute type_wf get_attribute get_attribute_locs
  for to_tree_order :: "(_::linorder) object_ptr  ((_) heap, exception, (_) object_ptr list) prog"
    and first_in_tree_order ::
    "(_) object_ptr  ((_) object_ptr  ((_) heap, exception, (_) element_ptr option) prog)
                                              ((_) heap, exception, (_) element_ptr option) prog"
  and get_attribute :: "(_) element_ptr  char list  ((_) heap, exception, char list option) prog"
  and get_attribute_locs :: "(_) element_ptr  ((_) 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 type_wf :: "(_) heap  bool" +
  assumes get_element_by_id_impl: "get_element_by_id = a_get_element_by_id"
  assumes get_elements_by_class_name_impl: "get_elements_by_class_name = a_get_elements_by_class_name"
  assumes get_elements_by_tag_name_impl: "get_elements_by_tag_name = a_get_elements_by_tag_name"
begin
lemmas 
  get_element_by_id_def = get_element_by_id_impl[unfolded a_get_element_by_id_def]
lemmas 
  get_elements_by_class_name_def = get_elements_by_class_name_impl[unfolded a_get_elements_by_class_name_def]
lemmas 
  get_elements_by_tag_name_def = get_elements_by_tag_name_impl[unfolded a_get_elements_by_tag_name_def]

lemma get_element_by_id_result_in_tree_order:
  assumes "h  get_element_by_id ptr iden r Some element_ptr"
  assumes "h  to_tree_order ptr r to"
  shows "cast element_ptr  set to"
  using assms 
  by(auto simp add: get_element_by_id_def first_in_tree_order_def  
               elim!: map_filter_M_pure_E[where y=element_ptr]  bind_returns_result_E2 
               dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] 
               intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
               split: option.splits list.splits if_splits)

lemma get_elements_by_class_name_result_in_tree_order:
  assumes "h  get_elements_by_class_name ptr name r results"
  assumes "h  to_tree_order ptr r to"
  assumes "element_ptr  set results"
  shows "cast element_ptr  set to"
  using assms 
  by(auto simp add: get_elements_by_class_name_def first_in_tree_order_def  
               elim!: map_filter_M_pure_E[where y=element_ptr]  bind_returns_result_E2 
               dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] 
               intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
               split: option.splits list.splits if_splits)

lemma get_elements_by_tag_name_result_in_tree_order:
  assumes "h  get_elements_by_tag_name ptr name r results"
  assumes "h  to_tree_order ptr r to"
  assumes "element_ptr  set results"
  shows "cast element_ptr  set to"
  using assms 
  by(auto simp add: get_elements_by_tag_name_def first_in_tree_order_def  
               elim!: map_filter_M_pure_E[where y=element_ptr]  bind_returns_result_E2 
               dest!: bind_returns_result_E3[rotated, OF assms(2), rotated] 
               intro!: map_filter_M_pure map_M_pure_I bind_pure_I 
               split: option.splits list.splits if_splits)

lemma get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag) h"
  by(auto simp add: get_elements_by_tag_name_def 
          intro!: bind_pure_I map_filter_M_pure 
          split: option.splits)
end

locale l_get_element_by = l_get_element_by_defs + l_to_tree_order_defs +
  assumes get_element_by_id_result_in_tree_order: 
          "h  get_element_by_id ptr iden r Some element_ptr  h  to_tree_order ptr r to 
                cast element_ptr  set to"
  assumes get_elements_by_tag_name_pure [simp]: "pure (get_elements_by_tag_name ptr tag) h"

interpretation 
  i_get_element_by?: l_get_element_byCore_DOM to_tree_order first_in_tree_order get_attribute 
                     get_attribute_locs get_element_by_id get_elements_by_class_name
                     get_elements_by_tag_name type_wf
  using instances
  apply(simp add: l_get_element_byCore_DOM_def l_get_element_byCore_DOM_axioms_def)
  by(simp add: get_element_by_id_def get_elements_by_class_name_def get_elements_by_tag_name_def)
declare l_get_element_byCore_DOM_axioms[instances]

lemma get_element_by_is_l_get_element_by [instances]: 
  "l_get_element_by get_element_by_id get_elements_by_tag_name to_tree_order"
  apply(unfold_locales)
  using get_element_by_id_result_in_tree_order get_elements_by_tag_name_pure
  by fast+
end