Theory NodeClass

(***********************************************************************************
 * 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 types for the Node class.›

theory NodeClass
  imports
    ObjectClass
    "../pointers/NodePointer"
begin

subsubsection‹Node›

record RNode = RObject
  + nothing :: unit
register_default_tvars "'Node RNode_ext" 
type_synonym 'Node Node = "'Node RNode_scheme"
register_default_tvars "'Node Node" 
type_synonym ('Object, 'Node) Object = "('Node RNode_ext + 'Object) Object"
register_default_tvars "('Object, 'Node) Object" 

type_synonym ('object_ptr, 'node_ptr, 'Object, 'Node) heap
  = "('node_ptr node_ptr + 'object_ptr, 'Node RNode_ext + 'Object) heap"
register_default_tvars
  "('object_ptr, 'node_ptr, 'Object, 'Node) heap" 
type_synonym heapfinal = "(unit, unit, unit, unit) heap"


definition node_ptr_kinds :: "(_) heap ⇒ (_) node_ptr fset"
  where
    "node_ptr_kinds heap = 
    (the |`| (castobject_ptr2node_ptr |`| (ffilter is_node_ptr_kind (object_ptr_kinds heap))))"

lemma node_ptr_kinds_simp [simp]: 
  "node_ptr_kinds (Heap (fmupd (cast node_ptr) node (the_heap h))) 
       = {|node_ptr|} |∪| node_ptr_kinds h"
  by (auto simp add: node_ptr_kinds_def)

definition castObject2Node :: "(_) Object ⇒ (_) Node option"
  where
    "castObject2Node obj = (case RObject.more obj of Inl node 
    ⇒ Some (RObject.extend (RObject.truncate obj) node) | _ ⇒ None)"
adhoc_overloading cast castObject2Node

definition castNode2Object:: "(_) Node ⇒ (_) Object"
  where
    "castNode2Object node = (RObject.extend (RObject.truncate node) (Inl (RObject.more node)))"
adhoc_overloading cast castNode2Object

definition is_node_kind :: "(_) Object ⇒ bool"
  where
    "is_node_kind ptr ⟷ castObject2Node ptr ≠ None"

definition getNode :: "(_) node_ptr ⇒ (_) heap ⇒ (_) Node option"
  where                             
    "getNode node_ptr h = Option.bind (get (cast node_ptr) h) cast"
adhoc_overloading get getNode

locale l_type_wf_defNode
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = (ObjectClass.type_wf h 
                    ∧ (∀node_ptr ∈ fset( node_ptr_kinds h). getNode node_ptr h ≠ None))"
end
global_interpretation l_type_wf_defNode defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfNode = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfNode: "type_wf h ⟹ NodeClass.type_wf h"

sublocale l_type_wfNode ⊆ l_type_wfObject
  apply(unfold_locales)
  using ObjectClass.a_type_wf_def by auto

locale l_getNode_lemmas = l_type_wfNode
begin
sublocale l_getObject_lemmas by unfold_locales
lemma getNode_type_wf:
  assumes "type_wf h"
  shows "node_ptr |∈| node_ptr_kinds h ⟷ getNode node_ptr h ≠ None"
  using l_type_wfNode_axioms assms
  apply(simp add: type_wf_defs getNode_def l_type_wfNode_def)
  by (metis bind_eq_None_conv ffmember_filter fimage_eqI is_node_ptr_kind_cast 
            getObject_type_wf node_ptr_casts_commute2 node_ptr_kinds_def option.sel option.simps(3))
end

global_interpretation l_getNode_lemmas type_wf
  by unfold_locales

definition putNode :: "(_) node_ptr ⇒ (_) Node ⇒ (_) heap ⇒ (_) heap"
  where
    "putNode node_ptr node = put (cast node_ptr) (cast node)"
adhoc_overloading put putNode

lemma putNode_ptr_in_heap:
  assumes "putNode node_ptr node h = h'"
  shows "node_ptr |∈| node_ptr_kinds h'"
  using assms
  unfolding putNode_def node_ptr_kinds_def
  by (metis ffmember_filter fimage_eqI is_node_ptr_kind_cast node_ptr_casts_commute2 
      option.sel putObject_ptr_in_heap)

lemma putNode_put_ptrs:
  assumes "putNode node_ptr node h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|cast node_ptr|}"
  using assms
  by (simp add: putNode_def putObject_put_ptrs)

lemma node_ptr_kinds_commutes [simp]: 
  "cast node_ptr |∈| object_ptr_kinds h ⟷ node_ptr |∈| node_ptr_kinds h"
proof (rule iffI)
  show "cast node_ptr |∈| object_ptr_kinds h ⟹ node_ptr |∈| node_ptr_kinds h"
    by (metis ffmember_filter fimage.rep_eq image_eqI is_node_ptr_kind_cast node_ptr_casts_commute2
        node_ptr_kinds_def option.sel)
next
  show "node_ptr |∈| node_ptr_kinds h ⟹ cast node_ptr |∈| object_ptr_kinds h"
    by (auto simp: node_ptr_kinds_def)
qed

lemma node_empty [simp]: 
  "⦇RObject.nothing = (), RNode.nothing = (), … = RNode.more node⦈ = node"
  by simp

lemma castNode2Object_inject [simp]: "castNode2Object x = castNode2Object y ⟷ x = y"
  apply(simp add: castNode2Object_def RObject.extend_def)
  by (metis (full_types) RObject.surjective old.unit.exhaust)

lemma castObject2Node_none [simp]: 
  "castObject2Node obj = None ⟷ ¬ (∃node. castNode2Object node = obj)"
  apply(auto simp add: castObject2Node_def castNode2Object_def RObject.extend_def split: sum.splits)[1]
  by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)

lemma castObject2Node_some [simp]: "castObject2Node obj = Some node ⟷ cast node = obj"
  by(auto simp add: castObject2Node_def castNode2Object_def RObject.extend_def split: sum.splits)

lemma castObject2Node_inv [simp]: "castObject2Node (castNode2Object node) = Some node"
  by simp

locale l_known_ptrNode
begin
definition a_known_ptr :: "(_) object_ptr ⇒ bool"
  where
    "a_known_ptr ptr = False"
end
global_interpretation l_known_ptrNode defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def


locale l_known_ptrsNode = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr ⇒ bool"
begin
definition a_known_ptrs :: "(_) heap ⇒ bool"
  where
    "a_known_ptrs h = (∀ptr ∈ fset (object_ptr_kinds h). known_ptr ptr)"

lemma known_ptrs_known_ptr: "a_known_ptrs h ⟹ ptr |∈| object_ptr_kinds h ⟹ known_ptr ptr"
  by (simp add: a_known_ptrs_def)

lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h' ⟹ a_known_ptrs h = a_known_ptrs h'"
  by(auto simp add: a_known_ptrs_def)
lemma known_ptrs_subset:
  "object_ptr_kinds h' |⊆| object_ptr_kinds h ⟹ a_known_ptrs h ⟹ a_known_ptrs h'"
  by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|} ⟹ known_ptr new_ptr ⟹
a_known_ptrs h ⟹ a_known_ptrs h'"
  by(simp add: a_known_ptrs_def)
end
global_interpretation l_known_ptrsNode known_ptr defines known_ptrs = a_known_ptrs .
lemmas known_ptrs_defs = a_known_ptrs_def

lemma known_ptrs_is_l_known_ptrs: "l_known_ptrs known_ptr known_ptrs"
  using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset
    known_ptrs_new_ptr
  by blast

lemma get_node_ptr_simp1 [simp]: "getNode node_ptr (putNode node_ptr node h) = Some node"
  by(auto simp add: getNode_def putNode_def)
lemma get_node_ptr_simp2 [simp]: 
  "node_ptr ≠ node_ptr' ⟹ getNode node_ptr (putNode node_ptr' node h) = getNode node_ptr h"
  by(auto simp add: getNode_def putNode_def)

end