Theory ElementPointer

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

datatype 'element_ptr element_ptr = Ref (the_ref: ref) | Ext 'element_ptr
register_default_tvars "'element_ptr element_ptr" 

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


definition castelement_ptr2element_ptr :: "(_) element_ptr ⇒ (_) element_ptr"
  where
    "castelement_ptr2element_ptr = id"

definition castelement_ptr2node_ptr :: "(_) element_ptr ⇒ (_) node_ptr"
  where
    "castelement_ptr2node_ptr ptr = node_ptr.Ext (Inl ptr)"

abbreviation castelement_ptr2object_ptr :: "(_) element_ptr ⇒ (_) object_ptr"
  where
    "castelement_ptr2object_ptr ptr ≡ castnode_ptr2object_ptr (castelement_ptr2node_ptr ptr)"

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

abbreviation castobject_ptr2element_ptr :: "(_) object_ptr ⇒ (_) element_ptr option"
  where
    "castobject_ptr2element_ptr ptr ≡ (case castobject_ptr2node_ptr ptr of 
                                  Some node_ptr ⇒ castnode_ptr2element_ptr node_ptr 
                                | None ⇒ None)"

adhoc_overloading cast castelement_ptr2node_ptr castelement_ptr2object_ptr 
  castnode_ptr2element_ptr castobject_ptr2element_ptr castelement_ptr2element_ptr

consts is_element_ptr_kind :: 'a
definition is_element_ptr_kindnode_ptr :: "(_) node_ptr ⇒ bool"
  where
    "is_element_ptr_kindnode_ptr ptr = (case castnode_ptr2element_ptr ptr of Some _ ⇒ True | _ ⇒ False)"

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

adhoc_overloading is_element_ptr_kind is_element_ptr_kindobject_ptr is_element_ptr_kindnode_ptr
lemmas is_element_ptr_kind_def = is_element_ptr_kindnode_ptr_def

consts is_element_ptr :: 'a
definition is_element_ptrelement_ptr :: "(_) element_ptr ⇒ bool"
  where
    "is_element_ptrelement_ptr ptr = (case ptr of element_ptr.Ref _ ⇒ True | _ ⇒ False)"

abbreviation is_element_ptrnode_ptr :: "(_) node_ptr ⇒ bool"
  where
    "is_element_ptrnode_ptr ptr ≡ (case cast ptr of 
                                   Some element_ptr ⇒ is_element_ptrelement_ptr element_ptr 
                                 | _ ⇒ False)"

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

adhoc_overloading is_element_ptr is_element_ptrobject_ptr is_element_ptrnode_ptr is_element_ptrelement_ptr
lemmas is_element_ptr_def = is_element_ptrelement_ptr_def

consts is_element_ptr_ext :: 'a
abbreviation "is_element_ptr_extelement_ptr ptr ≡ ¬ is_element_ptrelement_ptr ptr"

abbreviation "is_element_ptr_extnode_ptr ptr ≡ is_element_ptr_kind ptr ∧ (¬ is_element_ptrnode_ptr ptr)"

abbreviation "is_element_ptr_extobject_ptr ptr ≡ is_element_ptr_kind ptr ∧ (¬ is_element_ptrobject_ptr ptr)"
adhoc_overloading is_element_ptr_ext is_element_ptr_extobject_ptr is_element_ptr_extnode_ptr


instantiation element_ptr :: (linorder) linorder
begin
definition 
  less_eq_element_ptr :: "(_::linorder) element_ptr ⇒ (_)element_ptr ⇒ bool"
  where 
    "less_eq_element_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_element_ptr :: "(_::linorder) element_ptr ⇒ (_) element_ptr ⇒ bool"
  where "less_element_ptr x y ≡ x ≤ y ∧ ¬ y ≤ x"
instance 
  apply(standard) 
  by(auto simp add: less_eq_element_ptr_def less_element_ptr_def split: element_ptr.splits)
end

lemma is_element_ptr_ref [simp]: "is_element_ptr (element_ptr.Ref n)"
  by(simp add: is_element_ptrelement_ptr_def)

lemma element_ptr_casts_commute [simp]:
  "castnode_ptr2element_ptr node_ptr = Some element_ptr ⟷ castelement_ptr2node_ptr element_ptr = node_ptr"
  unfolding castnode_ptr2element_ptr_def castelement_ptr2node_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma element_ptr_casts_commute2 [simp]: 
  "(castnode_ptr2element_ptr (castelement_ptr2node_ptr element_ptr) = Some element_ptr)"
  by simp

lemma element_ptr_casts_commute3 [simp]:
  assumes "is_element_ptr_kindnode_ptr node_ptr"
  shows "castelement_ptr2node_ptr (the (castnode_ptr2element_ptr node_ptr)) = node_ptr"
  using assms
  by(auto simp add: is_element_ptr_kind_def castelement_ptr2node_ptr_def castnode_ptr2element_ptr_def 
      split: node_ptr.splits sum.splits)

lemma is_element_ptr_kind_obtains:
  assumes "is_element_ptr_kind node_ptr"
  obtains element_ptr where "node_ptr = castelement_ptr2node_ptr element_ptr"
  by (metis assms is_element_ptr_kind_def case_optionE element_ptr_casts_commute)

lemma is_element_ptr_kind_none:
  assumes "¬is_element_ptr_kind node_ptr"
  shows "castnode_ptr2element_ptr node_ptr = None"
  using assms
  unfolding is_element_ptr_kind_def castnode_ptr2element_ptr_def
  by(auto split: node_ptr.splits sum.splits)

lemma is_element_ptr_kind_cast [simp]: 
  "is_element_ptr_kind (castelement_ptr2node_ptr element_ptr)"
  by (metis element_ptr_casts_commute is_element_ptr_kind_none option.distinct(1))

lemma castelement_ptr2node_ptr_inject [simp]: 
  "castelement_ptr2node_ptr x = castelement_ptr2node_ptr y ⟷ x = y"
  by(simp add: castelement_ptr2node_ptr_def)

lemma castnode_ptr2element_ptr_ext_none [simp]: 
  "castnode_ptr2element_ptr (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None"
  by(simp add: castnode_ptr2element_ptr_def)

lemma is_element_ptr_implies_kind [dest]: "is_element_ptrnode_ptr ptr ⟹ is_element_ptr_kindnode_ptr ptr"
  by(auto split: option.splits)

end