Theory ObjectClass

(***********************************************************************************
 * 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‹Object›
text‹In this theory, we introduce the definition of the class Object. This class is the 
common superclass of our class model.›

theory ObjectClass
  imports
    BaseClass
    "../pointers/ObjectPointer"
begin

record RObject =
  nothing :: unit
register_default_tvars "'Object RObject_ext" 
type_synonym 'Object Object = "'Object RObject_scheme"
register_default_tvars "'Object Object" 

datatype ('object_ptr, 'Object) heap = Heap (the_heap: "((_) object_ptr, (_) Object) fmap")
register_default_tvars "('object_ptr, 'Object) heap"  
type_synonym heapfinal = "(unit, unit) heap"

definition object_ptr_kinds :: "(_) heap ⇒ (_) object_ptr fset"
  where
    "object_ptr_kinds = fmdom ∘ the_heap"

lemma object_ptr_kinds_simp [simp]: 
  "object_ptr_kinds (Heap (fmupd object_ptr object (the_heap h))) 
           = {|object_ptr|} |∪| object_ptr_kinds h"
  by(auto simp add: object_ptr_kinds_def)

definition getObject :: "(_) object_ptr ⇒ (_) heap ⇒ (_) Object option"
  where
    "getObject ptr h = fmlookup (the_heap h) ptr"
adhoc_overloading get getObject 

locale l_type_wf_defObject
begin
definition a_type_wf :: "(_) heap ⇒ bool"
  where
    "a_type_wf h = True"
end
global_interpretation l_type_wf_defObject defines type_wf = a_type_wf .
lemmas type_wf_defs = a_type_wf_def

locale l_type_wfObject = l_type_wf type_wf for type_wf :: "((_) heap ⇒ bool)" +
  assumes type_wfObject: "type_wf h ⟹ ObjectClass.type_wf h"

locale l_getObject_lemmas = l_type_wfObject
begin
lemma getObject_type_wf:
  assumes "type_wf h"
  shows "object_ptr |∈| object_ptr_kinds h ⟷ getObject object_ptr h ≠ None"
  using l_type_wfObject_axioms assms
  apply(simp add: type_wf_def getObject_def)
  by (simp add: fmlookup_dom_iff object_ptr_kinds_def)
end

global_interpretation l_getObject_lemmas type_wf
  by (simp add: l_getObject_lemmas.intro l_type_wfObject.intro)

definition putObject :: "(_) object_ptr ⇒ (_) Object ⇒ (_) heap ⇒ (_) heap"
  where
    "putObject ptr obj h = Heap (fmupd ptr obj (the_heap h))"
adhoc_overloading put putObject

lemma putObject_ptr_in_heap:
  assumes "putObject object_ptr object h = h'"
  shows "object_ptr |∈| object_ptr_kinds h'"
  using assms
  unfolding putObject_def
  by auto

lemma putObject_put_ptrs:
  assumes "putObject object_ptr object h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |∪| {|object_ptr|}"
  using assms
  by (metis comp_apply fmdom_fmupd funion_finsert_right heap.sel object_ptr_kinds_def 
      sup_bot.right_neutral putObject_def)

lemma object_more_extend_id [simp]: "more (extend x y) = y"
  by(simp add: extend_def)

lemma object_empty [simp]: "⦇nothing = (), … = more x⦈ = x"
  by simp

locale l_known_ptrObject
begin
definition a_known_ptr :: "(_) object_ptr ⇒ bool"
  where
    "a_known_ptr ptr = False"

lemma known_ptr_not_object_ptr: 
  "a_known_ptr ptr ⟹ ¬is_object_ptr ptr ⟹ known_ptr ptr"
  by(simp add: a_known_ptr_def)
end
global_interpretation l_known_ptrObject defines known_ptr = a_known_ptr .
lemmas known_ptr_defs = a_known_ptr_def

locale l_known_ptrs = l_known_ptr known_ptr for known_ptr :: "(_) object_ptr ⇒ bool" +
  fixes known_ptrs :: "(_) heap ⇒ bool"
  assumes known_ptrs_known_ptr: "known_ptrs h ⟹ ptr |∈| object_ptr_kinds h ⟹ known_ptr ptr"
  assumes known_ptrs_preserved:
    "object_ptr_kinds h = object_ptr_kinds h' ⟹ known_ptrs h = known_ptrs h'"
  assumes known_ptrs_subset:
    "object_ptr_kinds h' |⊆| object_ptr_kinds h ⟹ known_ptrs h ⟹ known_ptrs h'"
  assumes known_ptrs_new_ptr:
    "object_ptr_kinds h' = object_ptr_kinds h |∪| {|new_ptr|} ⟹ known_ptr new_ptr ⟹
known_ptrs h ⟹ known_ptrs h'"

locale l_known_ptrsObject = 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_ptrsObject 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_object_ptr_simp1 [simp]: "getObject object_ptr (putObject object_ptr object h) = Some object"
  by(simp add: getObject_def putObject_def)
lemma get_object_ptr_simp2 [simp]: 
  "object_ptr ≠ object_ptr' 
   ⟹ getObject object_ptr (putObject object_ptr' object h) = getObject object_ptr h"
  by(simp add: getObject_def putObject_def)


subsection‹Limited Heap Modifications›

definition heap_unchanged_except :: "(_) object_ptr set ⇒ (_) heap ⇒ (_) heap ⇒ bool"
  where
    "heap_unchanged_except S h h' = (∀ptr ∈ (fset (object_ptr_kinds h) 
                                   ∪ (fset (object_ptr_kinds h'))) - S. get ptr h = get ptr h')"

definition deleteObject :: "(_) object_ptr ⇒ (_) heap ⇒ (_) heap option" where
  "deleteObject ptr h = (if ptr |∈| object_ptr_kinds h then Some (Heap (fmdrop ptr (the_heap h))) 
                                                      else None)"

lemma deleteObject_pointer_removed:
  assumes "deleteObject ptr h = Some h'"
  shows "ptr |∉| object_ptr_kinds h'"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)

lemma deleteObject_pointer_ptr_in_heap:
  assumes "deleteObject ptr h = Some h'"
  shows "ptr |∈| object_ptr_kinds h"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)

lemma deleteObject_ok:
  assumes "ptr |∈| object_ptr_kinds h"
  shows "deleteObject ptr h ≠ None"
  using assms
  by(auto simp add: deleteObject_def object_ptr_kinds_def split: if_splits)


subsection ‹Code Generator Setup›

definition "create_heap xs = Heap (fmap_of_list xs)"

code_datatype ObjectClass.heap.Heap create_heap

lemma object_ptr_kinds_code3 [code]: 
  "fmlookup (the_heap (create_heap xs)) x = map_of xs x"
  by(auto simp add: create_heap_def fmlookup_of_list)

lemma object_ptr_kinds_code4 [code]: 
  "the_heap (create_heap xs) = fmap_of_list xs"
  by(simp add: create_heap_def)

lemma object_ptr_kinds_code5 [code]: 
  "the_heap (Heap x) = x"
  by simp


end