Theory NodePointer

(***********************************************************************************
 * 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‹Node›
text‹In this theory, we introduce the typed pointers for the class Node.›   
theory NodePointer
  imports
    ObjectPointer
begin

datatype 'node_ptr node_ptr = Ext 'node_ptr
register_default_tvars "'node_ptr node_ptr" 

type_synonym ('object_ptr, 'node_ptr) object_ptr = "('node_ptr node_ptr + 'object_ptr) object_ptr"
register_default_tvars "('object_ptr, 'node_ptr) object_ptr" 

definition castnode_ptr2object_ptr :: "(_) node_ptr  ⇒ (_) object_ptr"
  where
    "castnode_ptr2object_ptr ptr = object_ptr.Ext (Inl ptr)"

definition castobject_ptr2node_ptr :: "(_) object_ptr ⇒ (_) node_ptr option"
  where
    "castobject_ptr2node_ptr object_ptr = (case object_ptr of object_ptr.Ext (Inl node_ptr) 
                                           ⇒ Some node_ptr | _ ⇒ None)"

adhoc_overloading cast castnode_ptr2object_ptr castobject_ptr2node_ptr

definition is_node_ptr_kind :: "(_) object_ptr ⇒ bool"
  where
    "is_node_ptr_kind ptr = (castobject_ptr2node_ptr ptr ≠ None)"

instantiation node_ptr :: (linorder) linorder
begin
definition less_eq_node_ptr :: "(_::linorder) node_ptr ⇒ (_) node_ptr ⇒ bool"
  where "less_eq_node_ptr x y ≡ (case x of Ext i ⇒ (case y of Ext j ⇒ i ≤ j))"
definition less_node_ptr :: "(_::linorder) node_ptr ⇒ (_) node_ptr ⇒ bool"
  where "less_node_ptr x y ≡ x ≤ y ∧ ¬ y ≤ x"
instance 
  apply(standard)
  by(auto simp add: less_eq_node_ptr_def less_node_ptr_def split: node_ptr.splits)
end

lemma node_ptr_casts_commute [simp]: 
  "castobject_ptr2node_ptr ptr = Some node_ptr ⟷ castnode_ptr2object_ptr node_ptr = ptr"
  unfolding castobject_ptr2node_ptr_def castnode_ptr2object_ptr_def
  by(auto split: object_ptr.splits sum.splits)

lemma node_ptr_casts_commute2 [simp]: 
  "castobject_ptr2node_ptr (castnode_ptr2object_ptr node_ptr) = Some node_ptr"
  by simp

lemma node_ptr_casts_commute3 [simp]:
  assumes "is_node_ptr_kind ptr"
  shows "castnode_ptr2object_ptr (the (castobject_ptr2node_ptr ptr)) = ptr"
  using assms
  by(auto simp add: is_node_ptr_kind_def castnode_ptr2object_ptr_def castobject_ptr2node_ptr_def 
      split: object_ptr.splits sum.splits)

lemma is_node_ptr_kind_obtains:
  assumes "is_node_ptr_kind ptr"
  obtains node_ptr where "castobject_ptr2node_ptr ptr = Some node_ptr"
  using assms is_node_ptr_kind_def by auto

lemma is_node_ptr_kind_none:
  assumes "¬is_node_ptr_kind ptr"
  shows "castobject_ptr2node_ptr ptr = None"
  using assms
  unfolding is_node_ptr_kind_def castobject_ptr2node_ptr_def
  by auto

lemma is_node_ptr_kind_cast [simp]: "is_node_ptr_kind (castnode_ptr2object_ptr node_ptr)"
  unfolding is_node_ptr_kind_def by simp

lemma castnode_ptr2object_ptr_inject [simp]: 
  "castnode_ptr2object_ptr x = castnode_ptr2object_ptr y ⟷ x = y"
  by(simp add: castnode_ptr2object_ptr_def)

lemma castobject_ptr2node_ptr_ext_none [simp]: 
  "castobject_ptr2node_ptr (object_ptr.Ext (Inr (Inr (Inr object_ext_ptr)))) = None"
  by(simp add: castobject_ptr2node_ptr_def)

lemma node_ptr_inclusion [simp]: 
  "castnode_ptr2object_ptr node_ptr ∈ castnode_ptr2object_ptr ` node_ptrs ⟷ node_ptr ∈ node_ptrs"
  by auto
end