Theory ElementClass

(***********************************************************************************
 * 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 types for the Element  class.›
theory ElementClass
  imports
    "NodeClass"
    "ShadowRootPointer"
begin
text‹The type @{type "DOMString"} is a type synonym for @{type "string"}, define
     in \autoref{sec:Core_DOM_Basic_Datatypes}.›
type_synonym attr_key = DOMString
type_synonym attr_value = DOMString
type_synonym attrs = "(attr_key, attr_value) fmap"
type_synonym tag_name = DOMString
record ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr) RElement = RNode +
  nothing :: unit
  tag_name :: tag_name
  child_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
  attrs :: attrs
  shadow_root_opt :: "'shadow_root_ptr shadow_root_ptr option"
type_synonym
  ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element) Element
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_scheme"
register_default_tvars
  "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element) Element"
type_synonym
  ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 'Element) Node
  = "(('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option) RElement_ext + 'Node) Node"
register_default_tvars
  "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 'Element) Node"
type_synonym
  ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) Object
  = "('Object, ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option)
RElement_ext + 'Node) Object"
register_default_tvars
  "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 'Element) Object"

type_synonym
  ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
    'Object, 'Node, 'Element) heap
  = "(('document_ptr, 'shadow_root_ptr) document_ptr + 'object_ptr, 'element_ptr element_ptr +
'character_data_ptr character_data_ptr + 'node_ptr, 'Object,
      ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Element option)
RElement_ext + 'Node) heap"
register_default_tvars
  "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr, 'shadow_root_ptr,
'Object, 'Node, 'Element) heap"
type_synonym heapfinal = "(unit, unit, unit, unit, unit, unit, unit, unit, unit) heap"

definition element_ptr_kinds :: "(_) heap ⇒ (_) element_ptr fset"
  where
    "element_ptr_kinds heap = the |`| (castnode_ptr2element_ptr |`|
(ffilter is_element_ptr_kind (node_ptr_kinds heap)))"

lemma element_ptr_kinds_simp [simp]:
  "element_ptr_kinds (Heap (fmupd (cast element_ptr) element (the_heap h))) =
{|element_ptr|} |∪| element_ptr_kinds h"
  by (auto simp add: element_ptr_kinds_def)

definition element_ptrs :: "(_) heap ⇒ (_) element_ptr fset"
  where
    "element_ptrs heap = ffilter is_element_ptr (element_ptr_kinds heap)"

definition castNode2Element :: "(_) Node ⇒ (_) Element option"
  where
    "castNode2Element node = (case RNode.more node of Inl element ⇒
Some (RNode.extend (RNode.truncate node) element) | _ ⇒ None)"
adhoc_overloading cast castNode2Element

abbreviation castObject2Element :: "(_) Object ⇒ (_) Element option"
  where
    "castObject2Element obj ≡ (case castObject2Node obj of Some node ⇒ castNode2Element node | None ⇒ None)"
adhoc_overloading cast castObject2Element

definition castElement2Node :: "(_) Element ⇒ (_) Node"
  where
    "castElement2Node element = RNode.extend (RNode.truncate element) (Inl (RNode.more element))"
adhoc_overloading cast castElement2Node

abbreviation castElement2Object :: "(_) Element ⇒ (_) Object"
  where
    "castElement2Object ptr ≡ castNode2Object (castElement2Node ptr)"
adhoc_overloading cast castElement2Object

consts is_element_kind :: 'a
definition is_element_kindNode :: "(_) Node ⇒ bool"
  where
    "is_element_kindNode ptr ⟷ castNode2Element ptr ≠ None"

adhoc_overloading is_element_kind is_element_kindNode
lemmas is_element_kind_def = is_element_kindNode_def

abbreviation is_element_kindObject :: "(_) Object ⇒ bool"
  where
    "is_element_kindObject ptr ≡ castObject2Element ptr ≠ None"
adhoc_overloading is_element_kind is_element_kindObject

lemma element_ptr_kinds_commutes [simp]:
  "cast element_ptr |∈| node_ptr_kinds h ⟷ element_ptr |∈| element_ptr_kinds h"
proof (rule iffI)
  show "cast element_ptr |∈| node_ptr_kinds h ⟹ element_ptr |∈| element_ptr_kinds h"
    by (metis (no_types, opaque_lifting) element_ptr_casts_commute2 element_ptr_kinds_def
        ffmember_filter fimage_eqI is_element_ptr_kind_cast option.sel)
next
  show "element_ptr |∈| element_ptr_kinds h ⟹ cast element_ptr |∈| node_ptr_kinds h"
    by (auto simp: element_ptr_kinds_def)
qed

definition getElement :: "(_) element_ptr ⇒ (_) heap ⇒ (_) Element option"
  where
    "getElement element_ptr h = Option.bind (getNode (cast element_ptr) h) cast"
adhoc_overloading get getElement

locale l_type_wf_defElement
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = (NodeClass.type_wf h ∧ (∀element_ptr ∈ fset (element_ptr_kinds h).
                                                                  getElement element_ptr h ≠ None))"
end
global_interpretation l_type_wf_defElement defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfElement = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfElement: "type_wf h ⟹ ElementClass.type_wf h"

sublocale l_type_wfElement ⊆ l_type_wfNode
  apply(unfold_locales)
  using NodeClass.a_type_wf_def
  by (meson ElementClass.a_type_wf_def l_type_wfElement_axioms l_type_wfElement_def)

locale l_getElement_lemmas = l_type_wfElement
begin
sublocale l_getNode_lemmas by unfold_locales

lemma getElement_type_wf:
  assumes "type_wf h"
  shows "element_ptr |∈| element_ptr_kinds h ⟷ getElement element_ptr h ≠ None"
  using l_type_wfElement_axioms assms
  apply(simp add: type_wf_defs getElement_def l_type_wfElement_def)
  by (metis NodeClass.getNode_type_wf bind_eq_None_conv element_ptr_kinds_commutes
      option.distinct(1))
end

global_interpretation l_getElement_lemmas type_wf
  by unfold_locales

definition putElement :: "(_) element_ptr ⇒ (_) Element ⇒ (_) heap ⇒ (_) heap"
  where
    "putElement element_ptr element = putNode (cast element_ptr) (cast element)"
adhoc_overloading put putElement

lemma putElement_ptr_in_heap:
  assumes "putElement element_ptr element h = h'"
  shows "element_ptr |∈| element_ptr_kinds h'"
  using assms
  unfolding putElement_def element_ptr_kinds_def
  by (metis element_ptr_kinds_commutes element_ptr_kinds_def putNode_ptr_in_heap)

lemma putElement_put_ptrs:
  assumes "putElement element_ptr element h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast element_ptr|}"
  using assms
  by (simp add: putElement_def putNode_put_ptrs)



lemma castElement2Node_inject [simp]:
  "castElement2Node x = castElement2Node y ⟷ x = y"
  apply(simp add: castElement2Node_def RObject.extend_def RNode.extend_def)
  by (metis (full_types) RNode.surjective old.unit.exhaust)

lemma castNode2Element_none [simp]:
  "castNode2Element node = None ⟷ ¬ (∃element. castElement2Node element = node)"
  apply(auto simp add: castNode2Element_def castElement2Node_def RObject.extend_def RNode.extend_def
      split: sum.splits)[1]
  by (metis (full_types) RNode.select_convs(2) RNode.surjective old.unit.exhaust)

lemma castNode2Element_some [simp]:
  "castNode2Element node = Some element ⟷ castElement2Node element = node"
  by(auto simp add: castNode2Element_def castElement2Node_def RObject.extend_def RNode.extend_def
      split: sum.splits)

lemma castNode2Element_inv [simp]: "castNode2Element (castElement2Node element) = Some element"
  by simp

lemma get_elment_ptr_simp1 [simp]:
  "getElement element_ptr (putElement element_ptr element h) = Some element"
  by(auto simp add: getElement_def putElement_def)
lemma get_elment_ptr_simp2 [simp]:
  "element_ptr ≠ element_ptr'
  ⟹ getElement element_ptr (putElement element_ptr' element h) = getElement element_ptr h"
  by(auto simp add: getElement_def putElement_def)


abbreviation "create_element_obj tag_name_arg child_nodes_arg attrs_arg shadow_root_opt_arg
  ≡ ⦇ RObject.nothing = (), RNode.nothing = (), RElement.nothing = (),
      tag_name = tag_name_arg, Element.child_nodes = child_nodes_arg, attrs = attrs_arg,
      shadow_root_opt = shadow_root_opt_arg, … = None ⦈"

definition newElement :: "(_) heap ⇒ ((_) element_ptr × (_) heap)"
  where
    "newElement h =
      (let new_element_ptr = element_ptr.Ref (Suc (fMax (finsert 0 (element_ptr.the_ref
                                 |`| (element_ptrs h)))))
       in
      (new_element_ptr, put new_element_ptr (create_element_obj '''' [] fmempty None) h))"

lemma newElement_ptr_in_heap:
  assumes "newElement h = (new_element_ptr, h')"
  shows "new_element_ptr |∈| element_ptr_kinds h'"
  using assms
  unfolding newElement_def Let_def
  using putElement_ptr_in_heap by blast

lemma new_element_ptr_new:
  "element_ptr.Ref (Suc (fMax (finsert 0 (element_ptr.the_ref |`| element_ptrs h)))) |∉| element_ptrs h"
  by (metis Suc_n_not_le_n element_ptr.sel(1) fMax_ge fimage_finsert finsertI1 finsertI2 set_finsert)

lemma newElement_ptr_not_in_heap:
  assumes "newElement h = (new_element_ptr, h')"
  shows "new_element_ptr |∉| element_ptr_kinds h"
  using assms
  unfolding newElement_def
  by (metis Pair_inject element_ptrs_def ffmember_filter new_element_ptr_new is_element_ptr_ref)

lemma newElement_new_ptr:
  assumes "newElement h = (new_element_ptr, h')"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_element_ptr|}"
  using assms
  by (metis Pair_inject newElement_def putElement_put_ptrs)

lemma newElement_is_element_ptr:
  assumes "newElement h = (new_element_ptr, h')"
  shows "is_element_ptr new_element_ptr"
  using assms
  by(auto simp add: newElement_def Let_def)

lemma newElement_getObject [simp]:
  assumes "newElement h = (new_element_ptr, h')"
  assumes "ptr ≠ cast new_element_ptr"
  shows "getObject ptr h = getObject ptr h'"
  using assms
  by(auto simp add: newElement_def Let_def putElement_def putNode_def)

lemma newElement_getNode [simp]:
  assumes "newElement h = (new_element_ptr, h')"
  assumes "ptr ≠ cast new_element_ptr"
  shows "getNode ptr h = getNode ptr h'"
  using assms
  by(auto simp add: newElement_def Let_def putElement_def)

lemma newElement_getElement [simp]:
  assumes "newElement h = (new_element_ptr, h')"
  assumes "ptr ≠ new_element_ptr"
  shows "getElement ptr h = getElement ptr h'"
  using assms
  by(auto simp add: newElement_def Let_def)

locale l_known_ptrElement
begin
definition a_known_ptr :: "(_) object_ptr ⇒ bool"
  where
    "a_known_ptr ptr = (known_ptr ptr ∨ is_element_ptr ptr)"

lemma known_ptr_not_element_ptr: "¬is_element_ptr ptr ⟹ a_known_ptr ptr ⟹ known_ptr ptr"
  by(simp add: a_known_ptr_def)
end
global_interpretation l_known_ptrElement defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def


locale l_known_ptrsElement = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr ⇒ bool"
begin
definition a_known_ptrs :: "(_) heap ⇒ bool"
  where
    "a_known_ptrs h = (∀ptr ∈ fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr:
  "ptr |∈| object_ptr_kinds h ⟹ a_known_ptrs h ⟹ known_ptr ptr"
  by (simp add: a_known_ptrs_def)

lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h' ⟹ a_known_ptrs h = a_known_ptrs h'"
  by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
  "object_ptr_kinds h' |⊆| object_ptr_kinds h ⟹ a_known_ptrs h ⟹ a_known_ptrs h'"
  by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|} ⟹ known_ptr new_ptr ⟹
a_known_ptrs h ⟹ a_known_ptrs h'"
  by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrsElement known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
  using known_ptrs_known_ptr known_ptrs_preserved  known_ptrs_subset known_ptrs_new_ptr l_known_ptrs_def
  by blast

end