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