Theory CharacterDataClass

(***********************************************************************************
 * 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‹CharacterData›
text‹In this theory, we introduce the types for the CharacterData class.›
theory CharacterDataClass
  imports
    ElementClass
begin

subsubsection‹CharacterData›

text‹The type @{type "DOMString"} is a type synonym for @{type "string"}, defined 
     \autoref{sec:Core_DOM_Basic_Datatypes}.›

record RCharacterData = RNode +
  nothing :: unit
  val :: DOMString
register_default_tvars "'CharacterData RCharacterData_ext" 
type_synonym 'CharacterData CharacterData = "'CharacterData option RCharacterData_scheme"
register_default_tvars "'CharacterData CharacterData" 
type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 
    'Element, 'CharacterData) Node
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 
      'CharacterData option RCharacterData_ext + 'Node, 'Element) Node"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Node, 
                         'Element, 'CharacterData) Node" 
type_synonym ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 
    'Element, 'CharacterData) Object
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 
      'CharacterData option RCharacterData_ext + 'Node,
      'Element) Object"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 
                         'Node, 'Element, 'CharacterData) Object" 

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


definition character_data_ptr_kinds :: "(_) heap ⇒ (_) character_data_ptr fset"
  where                                                                                           
    "character_data_ptr_kinds heap = the |`| (cast |`| (ffilter is_character_data_ptr_kind 
                                                                (node_ptr_kinds heap)))"

lemma character_data_ptr_kinds_simp [simp]:
  "character_data_ptr_kinds (Heap (fmupd (cast character_data_ptr) character_data (the_heap h))) 
              = {|character_data_ptr|} |∪| character_data_ptr_kinds h"
  by (auto simp add: character_data_ptr_kinds_def)

definition character_data_ptrs :: "(_) heap ⇒ _ character_data_ptr fset"
  where
    "character_data_ptrs heap = ffilter is_character_data_ptr (character_data_ptr_kinds heap)"

abbreviation "character_data_ptr_exts heap ≡ character_data_ptr_kinds heap - character_data_ptrs heap"

definition castNode2CharacterData :: "(_) Node ⇒ (_) CharacterData option"
  where
    "castNode2CharacterData node = (case RNode.more node of
          Inr (Inl character_data) ⇒ Some (RNode.extend (RNode.truncate node) character_data)
        | _ ⇒ None)"
adhoc_overloading cast castNode2CharacterData

abbreviation castObject2CharacterData :: "(_) Object ⇒ (_) CharacterData  option"
  where
    "castObject2CharacterData obj ≡ (case castObject2Node obj of Some node ⇒ castNode2CharacterData node 
                                                       | None ⇒ None)"
adhoc_overloading cast castObject2CharacterData

definition castCharacterData2Node :: "(_) CharacterData ⇒ (_) Node"
  where
    "castCharacterData2Node character_data = RNode.extend (RNode.truncate character_data)
                                                      (Inr (Inl (RNode.more character_data)))"
adhoc_overloading cast castCharacterData2Node

abbreviation castCharacterData2Object :: "(_) CharacterData ⇒ (_) Object"
  where
    "castCharacterData2Object ptr ≡ castNode2Object (castCharacterData2Node ptr)"
adhoc_overloading cast castCharacterData2Object

consts is_character_data_kind :: 'a
definition is_character_data_kindNode :: "(_) Node ⇒ bool"
  where
    "is_character_data_kindNode ptr ⟷ castNode2CharacterData ptr ≠ None"

adhoc_overloading is_character_data_kind is_character_data_kindNode
lemmas is_character_data_kind_def = is_character_data_kindNode_def

abbreviation is_character_data_kindObject :: "(_) Object ⇒ bool"
  where
    "is_character_data_kindObject ptr ≡ castObject2CharacterData ptr ≠ None"
adhoc_overloading is_character_data_kind is_character_data_kindObject

lemma character_data_ptr_kinds_commutes [simp]:
  "cast character_data_ptr |∈| node_ptr_kinds h 
       ⟷ character_data_ptr |∈| character_data_ptr_kinds h"
proof (rule iffI)
  show "cast character_data_ptr |∈| node_ptr_kinds h ⟹
    character_data_ptr |∈| character_data_ptr_kinds h"
    by (metis (no_types, opaque_lifting) character_data_ptr_casts_commute2
        character_data_ptr_kinds_def ffmember_filter fimage_eqI is_character_data_ptr_kind_cast
        option.sel)
next
  show "character_data_ptr |∈| character_data_ptr_kinds h ⟹
      cast character_data_ptr |∈| node_ptr_kinds h"
    by (auto simp add: character_data_ptr_kinds_def)
qed

definition getCharacterData :: "(_) character_data_ptr ⇒ (_) heap ⇒ (_) CharacterData option"
  where                             
    "getCharacterData character_data_ptr h = Option.bind (getNode (cast character_data_ptr) h) cast"
adhoc_overloading get getCharacterData

locale l_type_wf_defCharacterData
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = (ElementClass.type_wf h
                 ∧ (∀character_data_ptr ∈ fset (character_data_ptr_kinds h).
                     getCharacterData character_data_ptr h ≠ None))"
end
global_interpretation l_type_wf_defCharacterData defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfCharacterData = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfCharacterData: "type_wf h ⟹ CharacterDataClass.type_wf h"

sublocale l_type_wfCharacterData ⊆ l_type_wfElement
  apply(unfold_locales)
  using ElementClass.a_type_wf_def
  by (meson CharacterDataClass.a_type_wf_def l_type_wfCharacterData_axioms l_type_wfCharacterData_def)

locale l_getCharacterData_lemmas = l_type_wfCharacterData
begin
sublocale l_getElement_lemmas by unfold_locales

lemma getCharacterData_type_wf:
  assumes "type_wf h"
  shows "character_data_ptr |∈| character_data_ptr_kinds h 
          ⟷ getCharacterData character_data_ptr h ≠ None"
  using l_type_wfCharacterData_axioms assms
  apply(simp add: type_wf_defs getCharacterData_def l_type_wfCharacterData_def)
  by (metis assms bind.bind_lzero character_data_ptr_kinds_commutes
      local.getNode_type_wf option.exhaust option.simps(3))
end

global_interpretation l_getCharacterData_lemmas type_wf
  by unfold_locales

definition putCharacterData :: "(_) character_data_ptr ⇒ (_) CharacterData ⇒ (_) heap ⇒ (_) heap"
  where
    "putCharacterData character_data_ptr character_data = putNode (cast character_data_ptr) 
                   (cast character_data)"
adhoc_overloading put putCharacterData

lemma putCharacterData_ptr_in_heap:
  assumes "putCharacterData character_data_ptr character_data h = h'"
  shows "character_data_ptr |∈| character_data_ptr_kinds h'"
  using assms putNode_ptr_in_heap
  unfolding putCharacterData_def character_data_ptr_kinds_def
  by (metis character_data_ptr_kinds_commutes character_data_ptr_kinds_def putNode_ptr_in_heap)

lemma putCharacterData_put_ptrs:
  assumes "putCharacterData character_data_ptr character_data h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast character_data_ptr|}"
  using assms
  by (simp add: putCharacterData_def putNode_put_ptrs)


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

lemma castNode2CharacterData_none [simp]:
  "castNode2CharacterData node = None ⟷ ¬ (∃character_data. castCharacterData2Node character_data = node)"
  apply(auto simp add: castNode2CharacterData_def castCharacterData2Node_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 castNode2CharacterData_some [simp]: 
  "castNode2CharacterData node = Some character_data ⟷ castCharacterData2Node character_data = node"
  by(auto simp add: castNode2CharacterData_def castCharacterData2Node_def RObject.extend_def RNode.extend_def 
      split: sum.splits)

lemma castNode2CharacterData_inv [simp]: 
  "castNode2CharacterData (castCharacterData2Node character_data) = Some character_data"
  by simp

lemma cast_element_not_character_data [simp]:
  "(castElement2Node element ≠ castCharacterData2Node character_data)"
  "(castCharacterData2Node character_data ≠ castElement2Node element)"
  by(auto simp add: castCharacterData2Node_def castElement2Node_def RNode.extend_def)

lemma get_CharacterData_simp1 [simp]: 
  "getCharacterData character_data_ptr (putCharacterData character_data_ptr character_data h) 
       = Some character_data"
  by(auto simp add: getCharacterData_def putCharacterData_def)
lemma get_CharacterData_simp2 [simp]: 
  "character_data_ptr ≠ character_data_ptr' ⟹ getCharacterData character_data_ptr 
         (putCharacterData character_data_ptr' character_data h) = getCharacterData character_data_ptr h"
  by(auto simp add: getCharacterData_def putCharacterData_def)

lemma get_CharacterData_simp3 [simp]: 
  "getElement element_ptr (putCharacterData character_data_ptr f h) = getElement element_ptr h"
  by(auto simp add: getElement_def putCharacterData_def)
lemma get_CharacterData_simp4 [simp]: 
  "getCharacterData element_ptr (putElement character_data_ptr f h) = getCharacterData element_ptr h"
  by(auto simp add: getCharacterData_def putElement_def)

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



abbreviation "create_character_data_obj val_arg
  ≡ ⦇ RObject.nothing = (), RNode.nothing = (), RCharacterData.nothing = (), val = val_arg, … = None ⦈"

definition newCharacterData :: "(_) heap ⇒ ((_) character_data_ptr × (_) heap)"
  where
    "newCharacterData h =
      (let new_character_data_ptr = character_data_ptr.Ref (Suc (fMax (character_data_ptr.the_ref 
            |`| (character_data_ptrs h)))) in
        (new_character_data_ptr, put new_character_data_ptr (create_character_data_obj '''') h))"

lemma newCharacterData_ptr_in_heap:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "new_character_data_ptr |∈| character_data_ptr_kinds h'"
  using assms
  unfolding newCharacterData_def Let_def
  using putCharacterData_ptr_in_heap by blast

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

lemma newCharacterData_ptr_not_in_heap:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "new_character_data_ptr |∉| character_data_ptr_kinds h"
  using assms
  unfolding newCharacterData_def
  by (metis Pair_inject character_data_ptrs_def fMax_finsert fempty_iff ffmember_filter
      fimage_is_fempty is_character_data_ptr_ref max_0L new_character_data_ptr_new)

lemma newCharacterData_new_ptr:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_character_data_ptr|}"
  using assms
  by (metis Pair_inject newCharacterData_def putCharacterData_put_ptrs)

lemma newCharacterData_is_character_data_ptr:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "is_character_data_ptr new_character_data_ptr"
  using assms
  by(auto simp add: newCharacterData_def Let_def)

lemma newCharacterData_getObject [simp]:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  assumes "ptr ≠ cast new_character_data_ptr"
  shows "getObject ptr h = getObject ptr h'"
  using assms
  by(auto simp add: newCharacterData_def Let_def putCharacterData_def putNode_def)

lemma newCharacterData_getNode [simp]:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  assumes "ptr ≠ cast new_character_data_ptr"
  shows "getNode ptr h = getNode ptr h'"
  using assms
  by(auto simp add: newCharacterData_def Let_def putCharacterData_def)

lemma newCharacterData_getElement [simp]:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  shows "getElement ptr h = getElement ptr h'"
  using assms
  by(auto simp add: newCharacterData_def Let_def)

lemma newCharacterData_getCharacterData [simp]:
  assumes "newCharacterData h = (new_character_data_ptr, h')"
  assumes "ptr ≠ new_character_data_ptr"
  shows "getCharacterData ptr h = getCharacterData ptr h'"
  using assms
  by(auto simp add: newCharacterData_def Let_def)


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

lemma known_ptr_not_character_data_ptr: 
  "¬is_character_data_ptr ptr ⟹ a_known_ptr ptr ⟹ known_ptr ptr"
  by(simp add: a_known_ptr_def)
end
global_interpretation l_known_ptrCharacterData defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def


locale l_known_ptrsCharacterData = 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: "a_known_ptrs h ⟹ ptr |∈| object_ptr_kinds 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_ptrsCharacterData 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