Theory ElementMonad

(***********************************************************************************
 * 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‹Element›
text‹In this theory, we introduce the monadic method setup for the Element class.›
theory ElementMonad
  imports
    NodeMonad
    "ElementClass"
begin

type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 
    'shadow_root_ptr, 'Object, 'Node, 'Element,'result) dom_prog
  = "((_) heap, exception, 'result) prog"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 
                        'document_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element,'result) dom_prog" 


global_interpretation l_ptr_kinds_M element_ptr_kinds defines element_ptr_kinds_M = a_ptr_kinds_M .
lemmas element_ptr_kinds_M_defs = a_ptr_kinds_M_def


lemma element_ptr_kinds_M_eq:
  assumes "|h  node_ptr_kinds_M|r = |h'  node_ptr_kinds_M|r"
  shows "|h  element_ptr_kinds_M|r = |h'  element_ptr_kinds_M|r"
  using assms 
  by(auto simp add: element_ptr_kinds_M_defs node_ptr_kinds_M_defs element_ptr_kinds_def)

lemma element_ptr_kinds_M_reads: 
  "reads (element_ptr. {preserved (get_MObject element_ptr RObject.nothing)}) element_ptr_kinds_M h h'"
  apply (simp add: reads_def node_ptr_kinds_M_defs element_ptr_kinds_M_defs element_ptr_kinds_def
    node_ptr_kinds_M_reads preserved_def cong del: image_cong_simp)
  apply (metis (mono_tags, opaque_lifting) node_ptr_kinds_small old.unit.exhaust preserved_def)
  done

global_interpretation l_dummy defines get_MElement = "l_get_M.a_get_M getElement" .
lemma get_M_is_l_get_M: "l_get_M getElement type_wf element_ptr_kinds"
  apply(simp add: getElement_type_wf l_get_M_def)
  by (metis (no_types, lifting) ObjectClass.getObject_type_wf ObjectClass.type_wf_defs 
      bind_eq_Some_conv bind_eq_Some_conv element_ptr_kinds_commutes getElement_def 
      getNode_def getObject_def node_ptr_kinds_commutes option.simps(3))
lemmas get_M_defs = get_MElement_def[unfolded l_get_M.a_get_M_def[OF get_M_is_l_get_M]]

adhoc_overloading get_M get_MElement

locale l_get_MElement_lemmas = l_type_wfElement
begin
sublocale l_get_MNode_lemmas by unfold_locales

interpretation l_get_M getElement type_wf element_ptr_kinds
  apply(unfold_locales)
   apply (simp add: getElement_type_wf local.type_wfElement)
  by (meson ElementMonad.get_M_is_l_get_M l_get_M_def)
lemmas get_MElement_ok = get_M_ok[folded get_MElement_def]
lemmas get_MElement_ptr_in_heap = get_M_ptr_in_heap[folded get_MElement_def]
end

global_interpretation l_get_MElement_lemmas type_wf by unfold_locales


global_interpretation l_put_M type_wf element_ptr_kinds getElement putElement 
  rewrites "a_get_M = get_MElement" 
  defines put_MElement = a_put_M
   apply (simp add: get_M_is_l_get_M l_put_M_def)
  by (simp add: get_MElement_def)

lemmas put_M_defs = a_put_M_def
adhoc_overloading put_M put_MElement


locale l_put_MElement_lemmas = l_type_wfElement
begin
sublocale l_put_MNode_lemmas by unfold_locales

interpretation l_put_M type_wf element_ptr_kinds getElement putElement
  apply(unfold_locales)
   apply (simp add: getElement_type_wf local.type_wfElement)
  by (meson ElementMonad.get_M_is_l_get_M l_get_M_def)

lemmas put_MElement_ok = put_M_ok[folded put_MElement_def]
end

global_interpretation l_put_MElement_lemmas type_wf by unfold_locales


lemma element_put_get [simp]: 
  "h  put_MElement element_ptr setter v h h'  (x. getter (setter (λ_. v) x) = v) 
   h'  get_MElement element_ptr getter r v"
  by(auto simp add: put_M_defs get_M_defs split: option.splits)
lemma get_M_Element_preserved1 [simp]: 
  "element_ptr  element_ptr'  h  put_MElement element_ptr setter v h h' 
      preserved (get_MElement element_ptr' getter) h h'"
  by(auto simp add: put_M_defs get_M_defs preserved_def split: option.splits dest: get_heap_E)
lemma element_put_get_preserved [simp]: 
  "(x. getter (setter (λ_. v) x) = getter x)  h  put_MElement element_ptr setter v h h' 
     preserved (get_MElement element_ptr' getter) h h'"
  apply(cases "element_ptr = element_ptr'") 
  by(auto simp add: put_M_defs get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma  get_M_Element_preserved3 [simp]: 
  "(x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
     h  put_MElement element_ptr setter v h h'  preserved (get_MObject object_ptr getter) h h'"
  apply(cases "cast element_ptr = object_ptr") 
  by (auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs getElement_def 
      getNode_def preserved_def putElement_def putNode_def bind_eq_Some_conv 
      split: option.splits)
lemma  get_M_Element_preserved4 [simp]: 
  "(x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
      h  put_MElement element_ptr setter v h h'  preserved (get_MNode node_ptr getter) h h'"
  apply(cases "cast element_ptr = node_ptr") 
  by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs NodeMonad.get_M_defs getElement_def 
      getNode_def preserved_def putElement_def putNode_def bind_eq_Some_conv 
      split: option.splits)

lemma  get_M_Element_preserved5 [simp]: 
  "cast element_ptr  node_ptr  h  put_MElement element_ptr setter v h h' 
   preserved (get_MNode node_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs getElement_def putElement_def NodeMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma  get_M_Element_preserved6 [simp]: 
  "h  put_MElement element_ptr setter v h h' 
     (x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
     preserved (get_MNode node_ptr getter) h h'"
  apply(cases "cast element_ptr  node_ptr")
  by(auto simp add: put_M_defs get_M_defs getElement_def putElement_def NodeMonad.get_M_defs preserved_def 
      split: option.splits bind_splits dest: get_heap_E)

lemma  get_M_Element_preserved7 [simp]: 
  "cast element_ptr  node_ptr  h  put_MNode node_ptr setter v h h' 
     preserved (get_MElement element_ptr getter) h h'"
  by(auto simp add: NodeMonad.put_M_defs get_M_defs getElement_def NodeMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)

lemma  get_M_Element_preserved8 [simp]: 
  "cast element_ptr  object_ptr  h  put_MElement element_ptr setter v h h' 
     preserved (get_MObject object_ptr getter) h h'"
  by(auto simp add: put_M_defs get_M_defs getElement_def getNode_def putNode_def putElement_def 
      ObjectMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)
lemma  get_M_Element_preserved9 [simp]: 
  "h  put_MElement element_ptr setter v h h' 
     (x. getter (cast (setter (λ_. v) x)) = getter (cast x)) 
    preserved (get_MObject object_ptr getter) h h'"
  apply(cases "cast element_ptr  object_ptr")
  by(auto simp add: put_M_defs get_M_defs getElement_def putElement_def getNode_def putNode_def 
      ObjectMonad.get_M_defs preserved_def 
      split: option.splits bind_splits dest: get_heap_E)

lemma  get_M_Element_preserved10 [simp]: 
  "cast element_ptr  object_ptr  h  put_MObject object_ptr setter v h h' 
     preserved (get_MElement element_ptr getter) h h'"
  by(auto simp add: ObjectMonad.put_M_defs get_M_defs getElement_def getNode_def putNode_def 
      ObjectMonad.get_M_defs preserved_def 
      split: option.splits dest: get_heap_E)

subsection‹Creating Elements›

definition new_element :: "(_, (_) element_ptr) dom_prog"
  where
    "new_element = do {
      h  get_heap;
      (new_ptr, h')  return (newElement h);
      return_heap h';
      return new_ptr
    }"

lemma new_element_ok [simp]:
  "h  ok new_element"
  by(auto simp add: new_element_def split: prod.splits)

lemma new_element_ptr_in_heap:
  assumes "h  new_element h h'"
    and "h  new_element r new_element_ptr"
  shows "new_element_ptr |∈| element_ptr_kinds h'"
  using assms
  unfolding new_element_def
  by(auto simp add: new_element_def newElement_def Let_def putElement_ptr_in_heap is_OK_returns_result_I
      elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_element_ptr_not_in_heap:
  assumes "h  new_element h h'"
    and "h  new_element r new_element_ptr"
  shows "new_element_ptr |∉| element_ptr_kinds h"
  using assms newElement_ptr_not_in_heap
  by(auto simp add: new_element_def split: prod.splits elim!: bind_returns_result_E 
      bind_returns_heap_E)

lemma new_element_new_ptr:
  assumes "h  new_element h h'"
    and "h  new_element r new_element_ptr"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
  using assms newElement_new_ptr
  by(auto simp add: new_element_def split: prod.splits elim!: bind_returns_result_E 
      bind_returns_heap_E)

lemma new_element_is_element_ptr:
  assumes "h  new_element r new_element_ptr"
  shows "is_element_ptr new_element_ptr"
  using assms newElement_is_element_ptr
  by(auto simp add: new_element_def elim!: bind_returns_result_E split: prod.splits)

lemma new_element_child_nodes:
  assumes "h  new_element h h'"
  assumes "h  new_element r new_element_ptr"
  shows "h'  get_M new_element_ptr child_nodes r []"
  using assms
  by(auto simp add: get_M_defs new_element_def newElement_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_element_tag_name:
  assumes "h  new_element h h'"
  assumes "h  new_element r new_element_ptr"
  shows "h'  get_M new_element_ptr tag_name r ''''"
  using assms
  by(auto simp add: get_M_defs new_element_def newElement_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_element_attrs:
  assumes "h  new_element h h'"
  assumes "h  new_element r new_element_ptr"
  shows "h'  get_M new_element_ptr attrs r fmempty"
  using assms
  by(auto simp add: get_M_defs new_element_def newElement_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_element_shadow_root_opt:
  assumes "h  new_element h h'"
  assumes "h  new_element r new_element_ptr"
  shows "h'  get_M new_element_ptr shadow_root_opt r None"
  using assms
  by(auto simp add: get_M_defs new_element_def newElement_def Let_def 
      split: option.splits prod.splits elim!: bind_returns_result_E bind_returns_heap_E)

lemma new_element_get_MObject: 
  "h  new_element h h'  h  new_element r new_element_ptr  ptr  cast new_element_ptr 
    preserved (get_MObject ptr getter) h h'"
  by(auto simp add: new_element_def ObjectMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_element_get_MNode: 
  "h  new_element h h'  h  new_element r new_element_ptr  ptr  cast new_element_ptr 
     preserved (get_MNode ptr getter) h h'"
  by(auto simp add: new_element_def NodeMonad.get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)
lemma new_element_get_MElement: 
  "h  new_element h h'  h  new_element r new_element_ptr  ptr  new_element_ptr 
     preserved (get_MElement ptr getter) h h'"
  by(auto simp add: new_element_def get_M_defs preserved_def 
      split: prod.splits option.splits elim!: bind_returns_result_E bind_returns_heap_E)

subsection‹Modified Heaps›

lemma get_Element_ptr_simp [simp]: 
  "getElement element_ptr (putObject ptr obj h) 
      = (if ptr = cast element_ptr then cast obj else get element_ptr h)"
  by(auto simp add: getElement_def split: option.splits Option.bind_splits)


lemma element_ptr_kinds_simp [simp]: 
  "element_ptr_kinds (putObject ptr obj h) 
      = element_ptr_kinds h |∪| (if is_element_ptr_kind ptr then {|the (cast ptr)|} else {||})"
  by(auto simp add: element_ptr_kinds_def is_node_ptr_kind_def split: option.splits)

lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "NodeClass.type_wf (putObject ptr obj h)"
  assumes "is_element_ptr_kind ptr  is_element_kind obj"
  shows "type_wf (putObject ptr obj h)"
  using assms
  by(auto simp add: type_wf_defs split: option.splits)

lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∉| object_ptr_kinds h"
  shows "type_wf h"
  using assms
  apply(auto simp add: type_wf_defs elim!: NodeMonad.type_wf_put_ptr_not_in_heap_E 
                                    split: option.splits if_splits)[1]
  using assms(2) node_ptr_kinds_commutes by blast

lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (putObject ptr obj h)"
  assumes "ptr |∈| object_ptr_kinds h"
  assumes "NodeClass.type_wf h"
  assumes "is_element_ptr_kind ptr  is_element_kind (the (get ptr h))"
  shows "type_wf h"
  using assms
  apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
  by (metis (no_types, lifting) NodeClass.l_getObject_lemmas_axioms assms(2) bind.bind_lunit
            castNode2Element_inv castObject2Node_inv getElement_def getNode_def
            l_getObject_lemmas.getObject_type_wf option.collapse)

subsection‹Preserving Types›

lemma new_element_type_wf_preserved [simp]: "h  new_element h h'  type_wf h = type_wf h'"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs newElement_def 
      new_element_def Let_def putElement_def putNode_def putObject_def getElement_def 
      getNode_def getObject_def
      split: prod.splits if_splits elim!: bind_returns_heap_E)[1]
     apply (metis element_ptr_kinds_commutes element_ptrs_def fempty_iff ffmember_filter
      is_element_ptr_ref)
    apply (metis element_ptrs_def fempty_iff ffmember_filter is_element_ptr_ref)
   apply (metis (no_types, opaque_lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptr_kinds_commutes
                element_ptrs_def fMax_ge ffmember_filter fimage_eqI is_element_ptr_ref)
  apply (metis (no_types, lifting) Suc_n_not_le_n element_ptr.sel(1) element_ptrs_def
               fMax_ge ffmember_filter fimage_eqI is_element_ptr_ref)
  done

locale l_new_element = l_type_wf +
  assumes new_element_types_preserved: "h  new_element h h'  type_wf h = type_wf h'"

lemma new_element_is_l_new_element: "l_new_element type_wf"
  using l_new_element.intro new_element_type_wf_preserved
  by blast

lemma put_MElement_tag_name_type_wf_preserved [simp]:
  "h  put_M element_ptr tag_name_update v h h'  type_wf h = type_wf h'"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
      Let_def put_M_defs get_M_defs putElement_def putNode_def putObject_def 
      getElement_def getNode_def getObject_def 
      split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
   apply (metis option.inject)
  apply (metis castObject2Node_inv option.sel)
  done

lemma put_MElement_child_nodes_type_wf_preserved [simp]: 
  "h  put_M element_ptr child_nodes_update v h h'  type_wf h = type_wf h'"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
      Let_def put_M_defs get_M_defs putElement_def putNode_def putObject_def 
      getElement_def getNode_def getObject_def 
      split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
   apply (metis option.inject)
  apply (metis castObject2Node_inv option.sel)
  done

lemma put_MElement_attrs_type_wf_preserved [simp]: 
  "h  put_M element_ptr attrs_update v h h'  type_wf h = type_wf h'"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  Let_def 
      put_M_defs get_M_defs putElement_def putNode_def putObject_def getElement_def 
      getNode_def getObject_def 
      split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
   apply (metis option.inject)
  apply (metis castObject2Node_inv option.sel)
  done

lemma put_MElement_shadow_root_opt_type_wf_preserved [simp]: 
  "h  put_M element_ptr shadow_root_opt_update v h h'  type_wf h = type_wf h'"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs  
      Let_def put_M_defs get_M_defs putElement_def putNode_def putObject_def 
      getElement_def getNode_def getObject_def 
      split: prod.splits option.splits Option.bind_splits elim!: bind_returns_heap_E)[1]
   apply (metis option.inject)
  apply (metis castObject2Node_inv option.sel)
  done

lemma put_M_pointers_preserved:
  assumes "h  put_MElement element_ptr setter v h h'"
  shows "object_ptr_kinds h = object_ptr_kinds h'"
  using assms 
  apply(auto simp add: put_M_defs putElement_def putNode_def putObject_def 
      elim!: bind_returns_heap_E2 dest!: get_heap_E)[1]
  by (meson get_MElement_ptr_in_heap is_OK_returns_result_I)

lemma element_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h'. w  SW. h  w h h' 
                     (object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h')"
  shows "element_ptr_kinds h = element_ptr_kinds h'"
  using writes_small_big[OF assms]
  apply(simp add: reflp_def transp_def preserved_def element_ptr_kinds_def)
  by (metis assms node_ptr_kinds_preserved)


lemma element_ptr_kinds_small:
  assumes "object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  shows "element_ptr_kinds h = element_ptr_kinds h'"
  by(simp add: element_ptr_kinds_def node_ptr_kinds_def preserved_def 
      object_ptr_kinds_preserved_small[OF assms])

lemma type_wf_preserved_small:
  assumes "object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  assumes "node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  assumes "element_ptr. preserved (get_MElement element_ptr RElement.nothing) h h'"
  shows "type_wf h = type_wf h'"
  using type_wf_preserved_small[OF assms(1) assms(2)] allI[OF assms(3), of id, simplified]
  apply(auto simp add: type_wf_defs )[1]
   apply(auto simp add: preserved_def get_M_defs element_ptr_kinds_small[OF assms(1)] 
      split: option.splits,force)[1]
  by(auto simp add: preserved_def get_M_defs element_ptr_kinds_small[OF assms(1)] 
      split: option.splits,force)

lemma type_wf_preserved:
  assumes "writes SW setter h h'"
  assumes "h  setter h h'"
  assumes "h h' w. w  SW  h  w h h' 
            object_ptr. preserved (get_MObject object_ptr RObject.nothing) h h'"
  assumes "h h' w. w  SW  h  w h h' 
            node_ptr. preserved (get_MNode node_ptr RNode.nothing) h h'"
  assumes "h h' w. w  SW  h  w h h' 
            element_ptr. preserved (get_MElement element_ptr RElement.nothing) h h'"
  shows "type_wf h = type_wf h'"
proof -
  have "h h' w. w  SW  h  w h h'  type_wf h = type_wf h'"
    using assms type_wf_preserved_small by fast
  with assms(1) assms(2) show ?thesis
    apply(rule writes_small_big)
    by(auto simp add: reflp_def transp_def)
qed

lemma type_wf_drop: "type_wf h  type_wf (Heap (fmdrop ptr (the_heap h)))"
  apply(auto simp add: type_wf_defs NodeClass.type_wf_defs ObjectClass.type_wf_defs 
      node_ptr_kinds_def object_ptr_kinds_def is_node_ptr_kind_def 
      getElement_def getNode_def getObject_def)[1]
   apply (metis (no_types, lifting) element_ptr_kinds_commutes fmdom_notD fmdom_notI
                fmlookup_drop heap.sel node_ptr_kinds_commutes o_apply object_ptr_kinds_def)
  by (metis element_ptr_kinds_commutes fmdom_notI fmdrop_lookup heap.sel node_ptr_kinds_commutes
            o_apply object_ptr_kinds_def)

end