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 ('object_ptr, 'node_ptr, 'element_ptr, 'character_data_ptr, 
    'document_ptr, 'shadow_root_ptr) object_ptr
  = "('shadow_root_ptr shadow_root_ptr + 'object_ptr, 'node_ptr, 'element_ptr, 
      'character_data_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_ptr2object_ptr :: "(_)shadow_root_ptr ⇒ (_) object_ptr"
  where
    "castshadow_root_ptr2object_ptr ptr = object_ptr.Ext (Inr (Inr (Inl ptr)))"

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

adhoc_overloading cast castshadow_root_ptr2object_ptr castobject_ptr2shadow_root_ptr castshadow_root_ptr2shadow_root_ptr


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

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_ptrobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_shadow_root_ptrobject_ptr ptr ≡ (case castobject_ptr2shadow_root_ptr ptr of
      Some shadow_root_ptr ⇒ is_shadow_root_ptrshadow_root_ptr shadow_root_ptr
    | None ⇒ False)"
adhoc_overloading is_shadow_root_ptr is_shadow_root_ptrobject_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_extobject_ptr ptr ≡ (case castobject_ptr2shadow_root_ptr ptr of
  Some shadow_root_ptr ⇒ is_shadow_root_ptr_extshadow_root_ptr shadow_root_ptr
| None ⇒ False)"
adhoc_overloading is_shadow_root_ptr_ext is_shadow_root_ptr_extobject_ptr is_shadow_root_ptr_extshadow_root_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 is_shadow_root_ptr_not_node_ptr[simp]: "¬is_shadow_root_ptr (castnode_ptr2object_ptr node_ptr)"
  by(simp add: is_shadow_root_ptr_def castnode_ptr2object_ptr_def castobject_ptr2shadow_root_ptr_def)

lemma cast_shadow_root_ptr_not_node_ptr [simp]:
  "castshadow_root_ptr2object_ptr shadow_root_ptr ≠ castnode_ptr2object_ptr node_ptr"
  "castnode_ptr2object_ptr node_ptr ≠ castshadow_root_ptr2object_ptr shadow_root_ptr"
  unfolding castshadow_root_ptr2object_ptr_def castnode_ptr2object_ptr_def by auto

lemma cast_shadow_root_ptr_not_document_ptr [simp]:
  "castshadow_root_ptr2object_ptr shadow_root_ptr ≠ castdocument_ptr2object_ptr document_ptr"
  "castdocument_ptr2object_ptr document_ptr ≠ castshadow_root_ptr2object_ptr shadow_root_ptr"
  unfolding castshadow_root_ptr2object_ptr_def castdocument_ptr2object_ptr_def by auto

lemma shadow_root_ptr_no_node_ptr_cast [simp]: 
  "¬ is_shadow_root_ptr_kind (castnode_ptr2object_ptr node_ptr)"
  by(simp add: castnode_ptr2object_ptr_def castobject_ptr2shadow_root_ptr_def is_shadow_root_ptr_kind_def)
lemma node_ptr_no_shadow_root_ptr_cast [simp]: 
  "¬ is_node_ptr_kind (castshadow_root_ptr2object_ptr shadow_root_ptr)"
  using is_node_ptr_kind_obtains by fastforce

lemma shadow_root_ptr_no_document_ptr_cast [simp]: 
  "¬ is_shadow_root_ptr_kind (castdocument_ptr2object_ptr document_ptr)"
  by(simp add: castdocument_ptr2object_ptr_def castobject_ptr2shadow_root_ptr_def is_shadow_root_ptr_kind_def)
lemma document_ptr_no_shadow_root_ptr_cast [simp]: 
  "¬ is_document_ptr_kind (castshadow_root_ptr2object_ptr shadow_root_ptr)"
  using is_document_ptr_kind_obtains by fastforce

lemma shadow_root_ptr_shadow_root_ptr_cast [simp]: 
  "is_shadow_root_ptr_kind (castshadow_root_ptr2object_ptr shadow_root_ptr)"
  by (simp add: castshadow_root_ptr2object_ptr_def castobject_ptr2shadow_root_ptr_def is_shadow_root_ptr_kind_def)

lemma shadow_root_ptr_casts_commute [simp]:
  "castobject_ptr2shadow_root_ptr ptr = Some shadow_root_ptr ⟷ castshadow_root_ptr2object_ptr shadow_root_ptr = ptr"
  unfolding castobject_ptr2shadow_root_ptr_def castshadow_root_ptr2object_ptr_def
  by(auto split: object_ptr.splits sum.splits)

lemma shadow_root_ptr_casts_commute2 [simp]: 
  "(castobject_ptr2shadow_root_ptr (castshadow_root_ptr2object_ptr shadow_root_ptr) = Some shadow_root_ptr)"
  by simp

lemma shadow_root_ptr_casts_commute3 [simp]:
  assumes "is_shadow_root_ptr_kind ptr"
  shows "castshadow_root_ptr2object_ptr (the (castobject_ptr2shadow_root_ptr ptr)) = ptr"
  using assms
  by(auto simp add: is_shadow_root_ptr_kind_def castshadow_root_ptr2object_ptr_def castobject_ptr2shadow_root_ptr_def
      split: object_ptr.splits sum.splits)

lemma is_shadow_root_ptr_kind_obtains:
  assumes "is_shadow_root_ptr_kind ptr"
  obtains shadow_root_ptr where "ptr = castshadow_root_ptr2object_ptr shadow_root_ptr"
  using assms is_shadow_root_ptr_kind_def
  by (metis case_optionE shadow_root_ptr_casts_commute)

lemma is_shadow_root_ptr_kind_none:
  assumes "¬is_shadow_root_ptr_kind ptr"
  shows "castobject_ptr2shadow_root_ptr ptr = None"
  using assms
  unfolding is_shadow_root_ptr_kind_def castobject_ptr2shadow_root_ptr_def
  by (auto split: object_ptr.splits sum.splits)

lemma castshadow_root_ptr2object_ptr_inject [simp]: 
  "castshadow_root_ptr2object_ptr x = castshadow_root_ptr2object_ptr y ⟷ x = y"
  by(simp add: castshadow_root_ptr2object_ptr_def)

lemma castobject_ptr2shadow_root_ptr_ext_none [simp]: 
  "castobject_ptr2shadow_root_ptr (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
  by(simp add: castobject_ptr2shadow_root_ptr_def)

lemma is_shadow_root_ptr_kind_simp1 [dest]: "is_document_ptr_kind ptr ⟹ ¬is_shadow_root_ptr_kind ptr"
  by (metis document_ptr_no_shadow_root_ptr_cast shadow_root_ptr_casts_commute3)

lemma is_shadow_root_ptr_kind_simp2 [dest]: "is_node_ptr_kind ptr ⟹ ¬is_shadow_root_ptr_kind ptr"
  by (metis node_ptr_no_shadow_root_ptr_cast shadow_root_ptr_casts_commute3)

end