Theory DocumentPointer

(***********************************************************************************
 * 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 typed pointers for the class Document.›   
theory DocumentPointer
  imports
    CharacterDataPointer
begin

datatype 'document_ptr document_ptr = Ref (the_ref: ref) | Ext 'document_ptr
register_default_tvars "'document_ptr document_ptr" 
type_synonym ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr) object_ptr
  = "('document_ptr document_ptr + 'object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 'document_ptr) object_ptr" 

definition castdocument_ptr2object_ptr :: "(_)document_ptr ⇒ (_) object_ptr"
  where
    "castdocument_ptr2object_ptr ptr = object_ptr.Ext (Inr (Inl ptr))"

definition castobject_ptr2document_ptr :: "(_) object_ptr ⇒ (_) document_ptr option"
  where
    "castobject_ptr2document_ptr ptr = (case ptr of 
                    object_ptr.Ext (Inr (Inl document_ptr)) ⇒ Some document_ptr 
                  | _ ⇒ None)"

adhoc_overloading cast castdocument_ptr2object_ptr castobject_ptr2document_ptr


definition is_document_ptr_kind :: "(_) object_ptr ⇒ bool"
  where
    "is_document_ptr_kind ptr = (case castobject_ptr2document_ptr ptr of 
                                     Some _ ⇒ True | None ⇒ False)"

consts is_document_ptr :: 'a
definition is_document_ptrdocument_ptr :: "(_) document_ptr ⇒ bool"
  where
    "is_document_ptrdocument_ptr ptr = (case ptr of document_ptr.Ref _ ⇒ True | _ ⇒ False)"

abbreviation is_document_ptrobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_document_ptrobject_ptr ptr ≡ (case castobject_ptr2document_ptr ptr of
      Some document_ptr ⇒ is_document_ptrdocument_ptr document_ptr
    | None ⇒ False)"
adhoc_overloading is_document_ptr is_document_ptrobject_ptr is_document_ptrdocument_ptr
lemmas is_document_ptr_def = is_document_ptrdocument_ptr_def

consts is_document_ptr_ext :: 'a
abbreviation "is_document_ptr_extdocument_ptr ptr ≡ ¬ is_document_ptrdocument_ptr ptr"

abbreviation "is_document_ptr_extobject_ptr ptr ≡ (case castobject_ptr2document_ptr ptr of
  Some document_ptr ⇒ is_document_ptr_extdocument_ptr document_ptr
| None ⇒ False)"
adhoc_overloading is_document_ptr_ext is_document_ptr_extobject_ptr is_document_ptr_extdocument_ptr

instantiation document_ptr :: (linorder) linorder
begin
definition less_eq_document_ptr :: "(_::linorder) document_ptr ⇒ (_) document_ptr ⇒ bool"
  where "less_eq_document_ptr x y ≡ (case x of Ext i ⇒ (case y of Ext j ⇒ i ≤ j | Ref _ ⇒ False)
                                             | Ref i ⇒ (case y of Ext _ ⇒ True | Ref j ⇒ i ≤ j))"
definition less_document_ptr :: "(_::linorder) document_ptr ⇒ (_) document_ptr ⇒ bool"
  where "less_document_ptr x y ≡ x ≤ y ∧ ¬ y ≤ x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_document_ptr_def less_document_ptr_def split: document_ptr.splits)
end

lemma is_document_ptr_ref [simp]: "is_document_ptr (document_ptr.Ref n)"
  by(simp add: is_document_ptrdocument_ptr_def)

lemma cast_document_ptr_not_node_ptr [simp]:
  "castdocument_ptr2object_ptr document_ptr ≠ castnode_ptr2object_ptr node_ptr"
  "castnode_ptr2object_ptr node_ptr ≠ castdocument_ptr2object_ptr document_ptr"
  unfolding castdocument_ptr2object_ptr_def castnode_ptr2object_ptr_def 
  by auto

lemma document_ptr_no_node_ptr_cast [simp]: 
  "¬ is_document_ptr_kind (castnode_ptr2object_ptr node_ptr)"
  by(simp add: castnode_ptr2object_ptr_def castobject_ptr2document_ptr_def is_document_ptr_kind_def)
lemma node_ptr_no_document_ptr_cast [simp]: 
  "¬ is_node_ptr_kind (castdocument_ptr2object_ptr document_ptr)"
  using is_node_ptr_kind_obtains by fastforce

lemma document_ptr_document_ptr_cast [simp]: 
  "is_document_ptr_kind (castdocument_ptr2object_ptr document_ptr)"
  by (simp add: castdocument_ptr2object_ptr_def castobject_ptr2document_ptr_def is_document_ptr_kind_def)

lemma document_ptr_casts_commute [simp]:
  "castobject_ptr2document_ptr ptr = Some document_ptr ⟷ castdocument_ptr2object_ptr document_ptr = ptr"
  unfolding castobject_ptr2document_ptr_def castdocument_ptr2object_ptr_def
  by(auto split: object_ptr.splits sum.splits)

lemma document_ptr_casts_commute2 [simp]: 
  "(castobject_ptr2document_ptr (castdocument_ptr2object_ptr document_ptr) = Some document_ptr)"
  by simp

lemma document_ptr_casts_commute3 [simp]:
  assumes "is_document_ptr_kind ptr"
  shows "castdocument_ptr2object_ptr (the (castobject_ptr2document_ptr ptr)) = ptr"
  using assms
  by(auto simp add: is_document_ptr_kind_def castdocument_ptr2object_ptr_def castobject_ptr2document_ptr_def
      split: object_ptr.splits sum.splits)

lemma is_document_ptr_kind_obtains:
  assumes "is_document_ptr_kind ptr"
  obtains document_ptr where "ptr = castdocument_ptr2object_ptr document_ptr"
  using assms is_document_ptr_kind_def
  by (metis case_optionE document_ptr_casts_commute)

lemma is_document_ptr_kind_none:
  assumes "¬is_document_ptr_kind ptr"
  shows "castobject_ptr2document_ptr ptr = None"
  using assms
  unfolding is_document_ptr_kind_def castobject_ptr2document_ptr_def
  by (auto split: object_ptr.splits sum.splits)

lemma castdocument_ptr2object_ptr_inject [simp]: 
  "castdocument_ptr2object_ptr x = castdocument_ptr2object_ptr y ⟷ x = y"
  by(simp add: castdocument_ptr2object_ptr_def)

lemma castobject_ptr2document_ptr_ext_none [simp]: 
  "castobject_ptr2document_ptr (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
  by(simp add: castobject_ptr2document_ptr_def)

lemma is_document_ptr_kind_not_element_ptr_kind [dest]:
  "is_document_ptr_kind ptr ⟹ ¬ is_element_ptr_kind ptr"
  by(auto simp add:  split: option.splits)
end