Theory DocumentClass

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

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

record ('node_ptr, 'element_ptr, 'character_data_ptr) RDocument = RObject +
  nothing :: unit
  doctype :: doctype
  document_element :: "(_) element_ptr option"
  disconnected_nodes :: "('node_ptr, 'element_ptr, 'character_data_ptr) node_ptr list"
type_synonym 
  ('node_ptr, 'element_ptr, 'character_data_ptr, 'Document) Document
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'Document option) RDocument_scheme"
register_default_tvars 
  "('node_ptr, 'element_ptr, 'character_data_ptr, 'Document) Document"
type_synonym 
  ('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 'Object, 'Node, 
    'Element, 'CharacterData, 'Document) Object
  = "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 
        ('node_ptr, 'element_ptr, 'character_data_ptr, 'Document option)
    RDocument_ext + 'Object, 'Node, 'Element, 'CharacterData) Object"
register_default_tvars "('node_ptr, 'element_ptr, 'character_data_ptr, 'shadow_root_ptr, 
     'Object, 'Node, 'Element, 'CharacterData, 'Document) Object" 

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


definition document_ptr_kinds :: "(_) heap ⇒ (_) document_ptr fset"
  where
    "document_ptr_kinds heap = the |`| (castobject_ptr2document_ptr |`| 
                               (ffilter is_document_ptr_kind (object_ptr_kinds heap)))"

definition document_ptrs :: "(_) heap ⇒ (_) document_ptr fset"
  where
    "document_ptrs heap = ffilter is_document_ptr (document_ptr_kinds heap)"

definition castObject2Document :: "(_) Object ⇒ (_) Document option"
  where
    "castObject2Document obj = (case RObject.more obj of
      Inr (Inl document) ⇒ Some (RObject.extend (RObject.truncate obj) document)
    | _ ⇒ None)"
adhoc_overloading cast castObject2Document

definition castDocument2Object:: "(_) Document ⇒ (_) Object"
  where
    "castDocument2Object document = (RObject.extend (RObject.truncate document) 
                                          (Inr (Inl (RObject.more document))))"
adhoc_overloading cast castDocument2Object

definition is_document_kind :: "(_) Object ⇒ bool"
  where
    "is_document_kind ptr ⟷ castObject2Document ptr ≠ None"

lemma document_ptr_kinds_simp [simp]: 
  "document_ptr_kinds (Heap (fmupd (cast document_ptr) document (the_heap h))) 
          = {|document_ptr|} |∪| document_ptr_kinds h"
  by (auto simp add: document_ptr_kinds_def)

lemma document_ptr_kinds_commutes [simp]: 
  "cast document_ptr |∈| object_ptr_kinds h ⟷ document_ptr |∈| document_ptr_kinds h"
proof (rule iffI)
  show "cast document_ptr |∈| object_ptr_kinds h ⟹ document_ptr |∈| document_ptr_kinds h"
    by (metis (no_types, opaque_lifting) document_ptr_casts_commute2 document_ptr_document_ptr_cast
        document_ptr_kinds_def ffmember_filter fimage_eqI option.sel)
next
  show "document_ptr |∈| document_ptr_kinds h ⟹ cast document_ptr |∈| object_ptr_kinds h"
    by (auto simp: document_ptr_kinds_def)
qed

definition getDocument :: "(_) document_ptr ⇒ (_) heap ⇒ (_) Document option"
  where                             
    "getDocument document_ptr h = Option.bind (get (cast document_ptr) h) cast"
adhoc_overloading get getDocument

locale l_type_wf_defDocument
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = (CharacterDataClass.type_wf h ∧ 
    (∀document_ptr ∈ fset (document_ptr_kinds h). getDocument document_ptr h ≠ None))"
end
global_interpretation l_type_wf_defDocument defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfDocument = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfDocument: "type_wf h ⟹ DocumentClass.type_wf h"

sublocale l_type_wfDocument ⊆ l_type_wfCharacterData
  apply(unfold_locales)
  by (metis (full_types) type_wf_defs l_type_wfDocument_axioms l_type_wfDocument_def)

locale l_getDocument_lemmas = l_type_wfDocument
begin
sublocale l_getCharacterData_lemmas by unfold_locales
lemma getDocument_type_wf:
  assumes "type_wf h"
  shows "document_ptr |∈| document_ptr_kinds h ⟷ getDocument document_ptr h ≠ None"
  using l_type_wfDocument_axioms assms
  apply(simp add: type_wf_defs getDocument_def l_type_wfDocument_def)
  by (metis document_ptr_kinds_commutes is_none_bind is_none_simps(1)
      is_none_simps(2) local.getObject_type_wf)
end

global_interpretation l_getDocument_lemmas type_wf by unfold_locales

definition putDocument :: "(_) document_ptr ⇒ (_) Document ⇒ (_) heap ⇒ (_) heap"
  where
    "putDocument document_ptr document = put (cast document_ptr) (cast document)"
adhoc_overloading put putDocument

lemma putDocument_ptr_in_heap:
  assumes "putDocument document_ptr document h = h'"
  shows "document_ptr |∈| document_ptr_kinds h'"
  using assms
  unfolding putDocument_def
  by (metis document_ptr_kinds_commutes putObject_ptr_in_heap)

lemma putDocument_put_ptrs:
  assumes "putDocument document_ptr document h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast document_ptr|}"
  using assms
  by (simp add: putDocument_def putObject_put_ptrs)


lemma castDocument2Object_inject [simp]: "castDocument2Object x = castDocument2Object y ⟷ x = y"
  apply(simp add: castDocument2Object_def RObject.extend_def)
  by (metis (full_types) RObject.surjective old.unit.exhaust)

lemma castObject2Document_none [simp]: 
  "castObject2Document obj = None ⟷ ¬ (∃document. castDocument2Object document = obj)"
  apply(auto simp add: castObject2Document_def castDocument2Object_def RObject.extend_def 
      split: sum.splits)[1]
  by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)

lemma castObject2Document_some [simp]: 
  "castObject2Document obj = Some document ⟷ cast document = obj"
  by(auto simp add: castObject2Document_def castDocument2Object_def RObject.extend_def 
      split: sum.splits)

lemma castObject2Document_inv [simp]: "castObject2Document (castDocument2Object document) = Some document"
  by simp

lemma cast_document_not_node [simp]:
  "castDocument2Object document ≠ castNode2Object node"
  "castNode2Object node ≠ castDocument2Object document"
  by(auto simp add: castDocument2Object_def castNode2Object_def RObject.extend_def)

lemma get_document_ptr_simp1 [simp]: 
  "getDocument document_ptr (putDocument document_ptr document h) = Some document"
  by(auto simp add: getDocument_def putDocument_def)
lemma get_document_ptr_simp2 [simp]: 
  "document_ptr ≠ document_ptr' 
   ⟹ getDocument document_ptr (putDocument document_ptr' document h) = getDocument document_ptr h"
  by(auto simp add: getDocument_def putDocument_def)


lemma get_document_ptr_simp3 [simp]: 
  "getElement element_ptr (putDocument document_ptr f h) = getElement element_ptr h"
  by(auto simp add: getElement_def getNode_def putDocument_def)
lemma get_document_ptr_simp4 [simp]:
  "getDocument document_ptr (putElement element_ptr f h) = getDocument document_ptr h"
  by(auto simp add: getDocument_def putElement_def putNode_def)
lemma get_document_ptr_simp5 [simp]: 
  "getCharacterData character_data_ptr (putDocument document_ptr f h) = getCharacterData character_data_ptr h"
  by(auto simp add: getCharacterData_def getNode_def putDocument_def)
lemma get_document_ptr_simp6 [simp]:
  "getDocument document_ptr (putCharacterData character_data_ptr f h) = getDocument document_ptr h"
  by(auto simp add: getDocument_def putCharacterData_def putNode_def)

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

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



abbreviation 
  create_document_obj :: "char list ⇒ (_) element_ptr option ⇒ (_) node_ptr list ⇒ (_) Document"
  where
    "create_document_obj doctype_arg document_element_arg disconnected_nodes_arg
  ≡ ⦇ RObject.nothing = (), RDocument.nothing = (), doctype = doctype_arg, 
      document_element = document_element_arg,
      disconnected_nodes = disconnected_nodes_arg, … = None ⦈"

definition newDocument :: "(_)heap ⇒ ((_) document_ptr × (_) heap)"
  where
    "newDocument h = 
     (let new_document_ptr = document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| (document_ptrs h))))) 
        in
         (new_document_ptr, put new_document_ptr (create_document_obj '''' None []) h))"

lemma newDocument_ptr_in_heap:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "new_document_ptr |∈| document_ptr_kinds h'"
  using assms
  unfolding newDocument_def Let_def
  using putDocument_ptr_in_heap by blast

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

lemma newDocument_ptr_not_in_heap:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "new_document_ptr |∉| document_ptr_kinds h"
  using assms
  unfolding newDocument_def
  by (metis Pair_inject document_ptrs_def fMax_finsert fempty_iff ffmember_filter 
      fimage_is_fempty is_document_ptr_ref max_0L new_document_ptr_new)

lemma newDocument_new_ptr:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast new_document_ptr|}"
  using assms
  by (metis Pair_inject newDocument_def putDocument_put_ptrs)

lemma newDocument_is_document_ptr:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "is_document_ptr new_document_ptr"
  using assms
  by(auto simp add: newDocument_def Let_def)

lemma newDocument_getObject [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  assumes "ptr ≠ cast new_document_ptr"
  shows "getObject ptr h = getObject ptr h'"
  using assms
  by(auto simp add: newDocument_def Let_def putDocument_def)

lemma newDocument_getNode [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "getNode ptr h = getNode ptr h'"
  using assms
  apply(simp add: newDocument_def Let_def putDocument_def)
  by(auto simp add: getNode_def)

lemma newDocument_getElement [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "getElement ptr h = getElement ptr h'"
  using assms
  by(auto simp add: newDocument_def Let_def)

lemma newDocument_getCharacterData [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  shows "getCharacterData ptr h = getCharacterData ptr h'"
  using assms
  by(auto simp add: newDocument_def Let_def)

lemma newDocument_getDocument [simp]:
  assumes "newDocument h = (new_document_ptr, h')"
  assumes "ptr ≠ new_document_ptr"
  shows "getDocument ptr h = getDocument ptr h'"
  using assms
  by(auto simp add: newDocument_def Let_def)


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

lemma known_ptr_not_document_ptr: "¬is_document_ptr ptr ⟹ a_known_ptr ptr ⟹ known_ptr ptr"
  by(simp add: a_known_ptr_def)
end
global_interpretation l_known_ptrDocument defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def


locale l_known_ptrsDocument = 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_ptrsDocument known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

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

end