Theory ShadowRootPointer

(***********************************************************************************
 * 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‹ShadowRoot›
text‹In this theory, we introduce the typed pointers for the class ShadowRoot. Note that, in
this document, we will not make use of ShadowRoots nor will we discuss their particular properties.
We only include them here, as they are required for future work and they cannot be added alter
following the object-oriented extensibility of our data model.›
theory ShadowRootPointer
  imports
    "DocumentPointer"
begin

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


definition castshadow_root_ptr2shadow_root_ptr :: "(_) shadow_root_ptr ⇒ (_) shadow_root_ptr"
  where
    "castshadow_root_ptr2shadow_root_ptr = id"

definition castshadow_root_ptr2document_ptr :: "(_) shadow_root_ptr ⇒ (_) document_ptr"
  where
    "castshadow_root_ptr2document_ptr ptr = document_ptr.Ext (Inl ptr)"

abbreviation castshadow_root_ptr2object_ptr :: "(_) shadow_root_ptr ⇒ (_) object_ptr"
  where
    "castshadow_root_ptr2object_ptr ptr ≡ castdocument_ptr2object_ptr (castshadow_root_ptr2document_ptr ptr)"

definition castdocument_ptr2shadow_root_ptr :: "(_) document_ptr ⇒ (_) shadow_root_ptr option"
  where
    "castdocument_ptr2shadow_root_ptr document_ptr = (case document_ptr of document_ptr.Ext (Inl shadow_root_ptr)
                                          ⇒ Some shadow_root_ptr | _ ⇒ None)"

abbreviation castobject_ptr2shadow_root_ptr :: "(_) object_ptr ⇒ (_) shadow_root_ptr option"
  where
    "castobject_ptr2shadow_root_ptr ptr ≡ (case castobject_ptr2document_ptr ptr of
                                  Some document_ptr ⇒ castdocument_ptr2shadow_root_ptr document_ptr
                                | None ⇒ None)"

adhoc_overloading cast castshadow_root_ptr2document_ptr castshadow_root_ptr2object_ptr
  castdocument_ptr2shadow_root_ptr castobject_ptr2shadow_root_ptr castshadow_root_ptr2shadow_root_ptr

consts is_shadow_root_ptr_kind :: 'a
definition is_shadow_root_ptr_kinddocument_ptr :: "(_) document_ptr ⇒ bool"
  where
    "is_shadow_root_ptr_kinddocument_ptr ptr =
(case castdocument_ptr2shadow_root_ptr ptr of Some _ ⇒ True | _ ⇒ False)"

abbreviation is_shadow_root_ptr_kindobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_shadow_root_ptr_kindobject_ptr ptr ≡ (case cast ptr of
                                 Some document_ptr ⇒ is_shadow_root_ptr_kinddocument_ptr document_ptr
                               | None ⇒ False)"

adhoc_overloading is_shadow_root_ptr_kind is_shadow_root_ptr_kindobject_ptr is_shadow_root_ptr_kinddocument_ptr
lemmas is_shadow_root_ptr_kind_def = is_shadow_root_ptr_kinddocument_ptr_def

consts is_shadow_root_ptr :: 'a
definition is_shadow_root_ptrshadow_root_ptr :: "(_) shadow_root_ptr ⇒ bool"
  where
    "is_shadow_root_ptrshadow_root_ptr ptr = (case ptr of shadow_root_ptr.Ref _ ⇒ True
                                                    | _ ⇒ False)"
abbreviation is_shadow_root_ptrdocument_ptr :: "(_) document_ptr ⇒ bool"
  where
    "is_shadow_root_ptrdocument_ptr ptr ≡ (case cast ptr of
                         Some shadow_root_ptr ⇒ is_shadow_root_ptrshadow_root_ptr shadow_root_ptr
                       | _ ⇒ False)"

abbreviation is_shadow_root_ptrobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_shadow_root_ptrobject_ptr ptr ≡ (case cast ptr of
                                    Some document_ptr ⇒ is_shadow_root_ptrdocument_ptr document_ptr
                                  | None ⇒ False)"

adhoc_overloading is_shadow_root_ptr is_shadow_root_ptrobject_ptr is_shadow_root_ptrdocument_ptr
  is_shadow_root_ptrshadow_root_ptr
lemmas is_shadow_root_ptr_def = is_shadow_root_ptrshadow_root_ptr_def

consts is_shadow_root_ptr_ext :: 'a
abbreviation "is_shadow_root_ptr_extshadow_root_ptr ptr ≡ ¬ is_shadow_root_ptrshadow_root_ptr ptr"

abbreviation "is_shadow_root_ptr_extdocument_ptr ptr ≡
is_shadow_root_ptr_kind ptr ∧ (¬ is_shadow_root_ptrdocument_ptr ptr)"

abbreviation "is_shadow_root_ptr_extobject_ptr ptr ≡
is_shadow_root_ptr_kind ptr ∧ (¬ is_shadow_root_ptrobject_ptr ptr)"
adhoc_overloading is_shadow_root_ptr_ext is_shadow_root_ptr_extobject_ptr is_shadow_root_ptr_extdocument_ptr


instantiation shadow_root_ptr :: (linorder) linorder
begin
definition
  less_eq_shadow_root_ptr :: "(_::linorder) shadow_root_ptr ⇒ (_) shadow_root_ptr ⇒ bool"
  where
    "less_eq_shadow_root_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_shadow_root_ptr :: "(_::linorder) shadow_root_ptr ⇒ (_) shadow_root_ptr ⇒ bool"
  where "less_shadow_root_ptr x y ≡ x ≤ y ∧ ¬ y ≤ x"
instance
  apply(standard)
  by(auto simp add: less_eq_shadow_root_ptr_def less_shadow_root_ptr_def
      split: shadow_root_ptr.splits)
end


lemma is_shadow_root_ptr_ref [simp]: "is_shadow_root_ptr (shadow_root_ptr.Ref n)"
  by(simp add: is_shadow_root_ptrshadow_root_ptr_def)

lemma shadow_root_ptr_casts_commute [simp]:
  "castdocument_ptr2shadow_root_ptr document_ptr =
Some shadow_root_ptr ⟷ castshadow_root_ptr2document_ptr shadow_root_ptr = document_ptr"
  unfolding castdocument_ptr2shadow_root_ptr_def castshadow_root_ptr2document_ptr_def
  by(auto split: document_ptr.splits sum.splits)

lemma shadow_root_ptr_casts_commute2 [simp]:
  "(castdocument_ptr2shadow_root_ptr (castshadow_root_ptr2document_ptr shadow_root_ptr) = Some shadow_root_ptr)"
  by simp

lemma shadow_root_ptr_casts_commute3 [simp]:
  assumes "is_shadow_root_ptr_kinddocument_ptr document_ptr"
  shows "castshadow_root_ptr2document_ptr (the (castdocument_ptr2shadow_root_ptr document_ptr)) = document_ptr"
  using assms
  by(auto simp add: is_shadow_root_ptr_kind_def castshadow_root_ptr2document_ptr_def castdocument_ptr2shadow_root_ptr_def
      split: document_ptr.splits sum.splits)

lemma is_shadow_root_ptr_kind_obtains:
  assumes "is_shadow_root_ptr_kind document_ptr"
  obtains shadow_root_ptr where "document_ptr = castshadow_root_ptr2document_ptr shadow_root_ptr"
  by (metis assms is_shadow_root_ptr_kind_def case_optionE shadow_root_ptr_casts_commute)

lemma is_shadow_root_ptr_kind_none:
  assumes "¬is_shadow_root_ptr_kind document_ptr"
  shows "castdocument_ptr2shadow_root_ptr document_ptr = None"
  using assms
  unfolding is_shadow_root_ptr_kind_def castdocument_ptr2shadow_root_ptr_def
  by(auto split: document_ptr.splits sum.splits)

lemma is_shadow_root_ptr_kind_cast [simp]:
  "is_shadow_root_ptr_kind (castshadow_root_ptr2document_ptr shadow_root_ptr)"
  by (metis shadow_root_ptr_casts_commute is_shadow_root_ptr_kind_none option.distinct(1))

lemma castshadow_root_ptr2document_ptr_inject [simp]:
  "castshadow_root_ptr2document_ptr x = castshadow_root_ptr2document_ptr y ⟷ x = y"
  by(simp add: castshadow_root_ptr2document_ptr_def)

lemma castdocument_ptr2shadow_root_ptr_ext_none [simp]:
  "castdocument_ptr2shadow_root_ptr (document_ptr.Ext (Inr (Inr document_ext_ptr))) = None"
  by(simp add: castdocument_ptr2shadow_root_ptr_def)

lemma is_shadow_root_ptr_implies_kind [dest]:
  "is_shadow_root_ptrdocument_ptr ptr ⟹ is_shadow_root_ptr_kinddocument_ptr ptr"
  by(auto split: option.splits)

lemma is_shadow_root_ptr_kind_not_document_ptr [simp]: "¬is_shadow_root_ptr_kind (document_ptr.Ref x)"
  by(simp add: is_shadow_root_ptr_kind_def castshadow_root_ptr2document_ptr_def split: option.splits)
end