Theory CharacterDataPointer

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

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

definition castcharacter_data_ptr2node_ptr :: "(_) character_data_ptr ⇒ (_) node_ptr"
  where
    "castcharacter_data_ptr2node_ptr ptr = node_ptr.Ext (Inr (Inl ptr))"

abbreviation castcharacter_data_ptr2object_ptr :: "(_) character_data_ptr ⇒ (_) object_ptr"
  where
    "castcharacter_data_ptr2object_ptr ptr ≡ castnode_ptr2object_ptr (castcharacter_data_ptr2node_ptr ptr)"

definition castnode_ptr2character_data_ptr :: "(_) node_ptr ⇒ (_) character_data_ptr option"
  where
    "castnode_ptr2character_data_ptr node_ptr = (case node_ptr of 
                        node_ptr.Ext (Inr (Inl character_data_ptr)) ⇒ Some character_data_ptr
                       | _ ⇒ None)"

abbreviation castobject_ptr2character_data_ptr :: "(_) object_ptr ⇒ (_) character_data_ptr option"
  where
    "castobject_ptr2character_data_ptr ptr ≡ (case castobject_ptr2node_ptr ptr of
                               Some node_ptr ⇒ castnode_ptr2character_data_ptr node_ptr
                             | None ⇒ None)"

adhoc_overloading cast castcharacter_data_ptr2node_ptr castcharacter_data_ptr2object_ptr 
  castnode_ptr2character_data_ptr castobject_ptr2character_data_ptr

consts is_character_data_ptr_kind :: 'a
definition is_character_data_ptr_kindnode_ptr :: "(_) node_ptr ⇒ bool"
  where
    "is_character_data_ptr_kindnode_ptr ptr = (case castnode_ptr2character_data_ptr ptr 
                                             of Some _ ⇒ True | _ ⇒ False)"

abbreviation is_character_data_ptr_kindobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_character_data_ptr_kindobject_ptr ptr ≡ (case cast ptr of 
                        Some node_ptr ⇒ is_character_data_ptr_kindnode_ptr node_ptr
                      | None ⇒ False)"

adhoc_overloading is_character_data_ptr_kind is_character_data_ptr_kindobject_ptr 
  is_character_data_ptr_kindnode_ptr
lemmas is_character_data_ptr_kind_def = is_character_data_ptr_kindnode_ptr_def

consts is_character_data_ptr :: 'a
definition is_character_data_ptrcharacter_data_ptr :: "(_) character_data_ptr ⇒ bool"
  where
    "is_character_data_ptrcharacter_data_ptr ptr = (case ptr 
                                 of character_data_ptr.Ref _ ⇒ True | _ ⇒ False)"

abbreviation is_character_data_ptrnode_ptr :: "(_) node_ptr ⇒ bool"
  where
    "is_character_data_ptrnode_ptr ptr ≡ (case cast ptr of
      Some character_data_ptr ⇒ is_character_data_ptrcharacter_data_ptr character_data_ptr
    | _ ⇒ False)"

abbreviation is_character_data_ptrobject_ptr :: "(_) object_ptr ⇒ bool"
  where
    "is_character_data_ptrobject_ptr ptr ≡ (case castobject_ptr2node_ptr ptr of
      Some node_ptr ⇒ is_character_data_ptrnode_ptr node_ptr
    | None ⇒ False)"

adhoc_overloading is_character_data_ptr
  is_character_data_ptrobject_ptr is_character_data_ptrnode_ptr is_character_data_ptrcharacter_data_ptr
lemmas is_character_data_ptr_def = is_character_data_ptrcharacter_data_ptr_def

consts is_character_data_ptr_ext :: 'a
abbreviation 
  "is_character_data_ptr_extcharacter_data_ptr ptr ≡ ¬ is_character_data_ptrcharacter_data_ptr ptr"

abbreviation "is_character_data_ptr_extnode_ptr ptr ≡ (case castnode_ptr2character_data_ptr ptr of
  Some character_data_ptr ⇒ is_character_data_ptr_extcharacter_data_ptr character_data_ptr
| None ⇒ False)"

abbreviation "is_character_data_ptr_extobject_ptr ptr ≡ (case castobject_ptr2node_ptr ptr of
  Some node_ptr ⇒ is_character_data_ptr_extnode_ptr node_ptr
| None ⇒ False)"

adhoc_overloading is_character_data_ptr_ext
  is_character_data_ptr_extobject_ptr is_character_data_ptr_extnode_ptr is_character_data_ptr_extcharacter_data_ptr

instantiation character_data_ptr :: (linorder) linorder
begin
definition 
  less_eq_character_data_ptr :: "(_::linorder) character_data_ptr ⇒ (_) character_data_ptr ⇒ bool"
  where 
    "less_eq_character_data_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_character_data_ptr :: "(_::linorder) character_data_ptr ⇒ (_) character_data_ptr ⇒ bool"
  where "less_character_data_ptr x y ≡ x ≤ y ∧ ¬ y ≤ x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_character_data_ptr_def less_character_data_ptr_def 
      split: character_data_ptr.splits)
end

lemma is_character_data_ptr_ref [simp]: "is_character_data_ptr (character_data_ptr.Ref n)"
  by(simp add: is_character_data_ptrcharacter_data_ptr_def)

lemma cast_element_ptr_not_character_data_ptr [simp]:
  "(castelement_ptr2node_ptr element_ptr ≠ castcharacter_data_ptr2node_ptr character_data_ptr)"
  "(castcharacter_data_ptr2node_ptr character_data_ptr ≠ castelement_ptr2node_ptr element_ptr)"
  unfolding castelement_ptr2node_ptr_def castcharacter_data_ptr2node_ptr_def 
  by(auto)

lemma is_character_data_ptr_kind_not_element_ptr [simp]: 
  "¬ is_character_data_ptr_kind (castelement_ptr2node_ptr element_ptr)"
  unfolding is_character_data_ptr_kind_def castelement_ptr2node_ptr_def castnode_ptr2character_data_ptr_def
  by auto
lemma is_element_ptr_kind_not_character_data_ptr [simp]: 
  "¬ is_element_ptr_kind (castcharacter_data_ptr2node_ptr character_data_ptr)"
  using is_element_ptr_kind_obtains by fastforce

lemma is_character_data_ptr_kind_cast [simp]: 
  "is_character_data_ptr_kind (castcharacter_data_ptr2node_ptr character_data_ptr)"
  by (simp add: castcharacter_data_ptr2node_ptr_def castnode_ptr2character_data_ptr_def 
      is_character_data_ptr_kindnode_ptr_def)

lemma character_data_ptr_casts_commute [simp]:
  "castnode_ptr2character_data_ptr node_ptr = Some character_data_ptr
   ⟷ castcharacter_data_ptr2node_ptr character_data_ptr = node_ptr"
  unfolding castnode_ptr2character_data_ptr_def castcharacter_data_ptr2node_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma character_data_ptr_casts_commute2 [simp]:
  "(castnode_ptr2character_data_ptr (castcharacter_data_ptr2node_ptr character_data_ptr) = Some character_data_ptr)"
  by simp

lemma character_data_ptr_casts_commute3 [simp]:
  assumes "is_character_data_ptr_kindnode_ptr node_ptr"
  shows "castcharacter_data_ptr2node_ptr (the (castnode_ptr2character_data_ptr node_ptr)) = node_ptr"
  using assms
  by(auto simp add: is_character_data_ptr_kindnode_ptr_def castnode_ptr2character_data_ptr_def 
      castcharacter_data_ptr2node_ptr_def
      split: node_ptr.splits sum.splits)

lemma is_character_data_ptr_kind_obtains:
  assumes "is_character_data_ptr_kindnode_ptr node_ptr"
  obtains character_data_ptr where "castcharacter_data_ptr2node_ptr character_data_ptr = node_ptr"
  by (metis assms is_character_data_ptr_kindnode_ptr_def case_optionE 
      character_data_ptr_casts_commute)

lemma is_character_data_ptr_kind_none:
  assumes "¬is_character_data_ptr_kindnode_ptr node_ptr"
  shows "castnode_ptr2character_data_ptr node_ptr = None"
  using assms
  unfolding is_character_data_ptr_kindnode_ptr_def castnode_ptr2character_data_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma castcharacter_data_ptr2node_ptr_inject [simp]: 
  "castcharacter_data_ptr2node_ptr x = castcharacter_data_ptr2node_ptr y ⟷ x = y"
  by(simp add: castcharacter_data_ptr2node_ptr_def)

lemma castnode_ptr2character_data_ptr_ext_none [simp]: 
  "castnode_ptr2character_data_ptr (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None"
  by(simp add: castnode_ptr2character_data_ptr_def)

end