Theory Heap

(*<*)
theory Heap
imports
  Ix
  "ConcurrentHOL.ConcurrentHOL"
begin

(*>*)
section‹ A polymorphic heap\label{sec:CImperativeHOL-heap} ›

text‹

We model a heap as a partial map from opaque addresses to structured objects.
 ▪ we use this extra structure to handle buffered writes (see \S\ref{sec:tso})
 ▪ allocation is non-deterministic and partial
 ▪ supports explicit deallocation

Limitations:
 ▪ does not support polymorphic sum types such as \<^typ>‹'a + 'b› and \<^typ>‹'a option› or products or lists
 ▪ the class of representable types is too small to represent processes

Source materials:
 ▪ 🗏‹$ISABELLE_HOME/src/HOL/Imperative_HOL/Heap.thy›
  ▪ that model of heaps includes a ‹lim› field to support deterministic allocation
  ▪ it uses distinct heaps for arrays and references

›

setup ‹Sign.mandatory_path "heap"›

type_synonym addr = nat ―‹ untyped heap addresses ›

datatype rep ―‹ the concrete representation of heap values ›
  = Addr nat heap.addr ―‹ metadata paired with an address ›
  | Val nat

datatype "write" = Write heap.addr nat heap.rep

type_synonym t = "heap.addr ⇀ heap.rep list" ―‹ partial map from addresses to structured encoded values ›

abbreviation empty :: "heap.t" where
  "empty ≡ Map.empty"

primrec apply_write :: "heap.write ⇒ heap.t ⇒ heap.t" where
  "apply_write (heap.Write addr i x) s = s(addr ↦ (the (s addr))[i := x])"

(* the free tyvar warning is the same as for ‹countable› *)
class rep = ―‹ the class of representable types ›
  assumes ex_inj: "∃to_heap_rep :: 'a ⇒ heap.rep. inj to_heap_rep"

setup ‹Sign.mandatory_path "rep"›

lemma countable_classI[intro!]:
  shows "OFCLASS('a::countable, heap.rep_class)"
by intro_classes (simp add: inj_on_def exI[where x="heap.Val ∘ to_nat"])

definition to :: "'a::heap.rep ⇒ heap.rep" where
  "to = (SOME f. inj f)"

definition "from" :: "heap.rep ⇒ 'a::heap.rep" where
  "from = inv (heap.rep.to :: 'a ⇒ heap.rep)"

lemmas inj_to[simp] = someI_ex[OF heap.ex_inj, folded heap.rep.to_def]

lemma inj_on_to[simp, intro]: "inj_on heap.rep.to S"
using heap.rep.inj_to by (auto simp: inj_on_def)

lemma surj_from[simp]: "surj heap.rep.from"
unfolding heap.rep.from_def by (simp add: inj_imp_surj_inv)

lemma to_split[simp]: "heap.rep.to x = heap.rep.to y ⟷ x = y"
using injD[OF heap.rep.inj_to] by auto

lemma from_to[simp]:
  shows "heap.rep.from (heap.rep.to x) = x"
by (simp add: heap.rep.from_def)

instance unit :: heap.rep ..

instance bool :: heap.rep ..

instance nat :: heap.rep ..

instance int :: heap.rep ..

instance char :: heap.rep ..

instance String.literal :: heap.rep ..

instance typerep :: heap.rep ..

setup ‹Sign.parent_path›

text‹

User-facing heap types typically carry more information than an
(untyped) address, such as (phantom) typing and a representation
invariant that guarantees the soundness of the encoding (for the given
value at the given address only). We abstract over that here and provide
some generic operations.

Notes:
 ▪ intuitively ‹addr_of› should be surjective but we do not enforce this
 ▪ we use sets here but these are not very flexible: all refs must have the same type
  ▪ this means some intutive facts involving ‹UNIV› cannot be stated

›

class addr_of =
  fixes addr_of :: "'a ⇒ heap.addr"
  fixes rep_val_inv :: "'a ⇒ heap.rep list pred"

definition obj_at :: "heap.rep list pred ⇒ heap.addr ⇒ heap.t pred" where
  "obj_at P r s = (case s r of None ⇒ False | Some v ⇒ P v)"

abbreviation (input) present :: "'a::heap.addr_of ⇒ heap.t pred" where
  "present r ≡ heap.obj_at ⟨True⟩ (heap.addr_of r)"

abbreviation (input) rep_inv :: "'a::heap.addr_of ⇒ heap.t pred" where
  "rep_inv r ≡ heap.obj_at (heap.rep_val_inv r) (heap.addr_of r)"

abbreviation (input) rep_inv_set :: "'a::heap.addr_of ⇒ heap.t set" where
  "rep_inv_set r ≡ Collect (heap.rep_inv r)"

―‹ allows arbitrary transitions provided the ‹rep_inv› of ‹r› is respected ›
abbreviation (input) rep_inv_rel :: "'a::heap.addr_of ⇒ heap.t rel" where
  "rep_inv_rel r ≡ heap.rep_inv_set r × heap.rep_inv_set r"

―‹ totality models the idea that all dereferences are ``valid'' but only some are reasonable ›
definition get :: "'a::heap.addr_of ⇒ heap.t ⇒ 'v::heap.rep list" where
  "get r s = map heap.rep.from (the (s (heap.addr_of r)))"

definition set :: "'a::heap.addr_of ⇒ 'v::heap.rep list ⇒ heap.t ⇒ heap.t" where
  "set r v s = s(heap.addr_of r ↦ map heap.rep.to v)"

definition dealloc :: "'a::heap.addr_of ⇒ heap.t ⇒ heap.t" where
  "dealloc r s = s |` {heap.addr_of r}"

―‹ allows no changes to ‹rs›, asserts the ‹rep_inv› of ‹rs› is valid, arbitrary changes to ‹-rs› ›
definition Id_on :: "'a::heap.addr_of set ⇒ heap.t rel" ("heap.Id⇘_⇙") where
  "heap.Id⇘rs⇙ = (⋂r∈rs. heap.rep_inv_rel r ∩ Id⇘λs. s (heap.addr_of r)⇙)"

―‹ allows arbitrary changes to ‹rs› provided the ‹rep_inv› of ‹rs› is respected.
    requires addresses in ‹-heap.addr_of ` rs› to be unchanged ›
definition modifies :: "'a::heap.addr_of set ⇒ heap.t rel" ("heap.modifies⇘_⇙") where
  "heap.modifies⇘rs⇙ = (⋂r∈rs. heap.rep_inv_rel r) ∩ {(s, s'). ∀r∈-heap.addr_of ` rs. s r = s' r}"

setup ‹Sign.mandatory_path "get"›

lemma cong:
  assumes "s (heap.addr_of r) = s' (heap.addr_of r')"
  shows "heap.get r s = heap.get r' s'"
by (simp add: assms heap.get_def)

lemma Id_on_proj_cong:
  assumes "(s, s') ∈ heap.Id⇘{r}⇙"
  shows "heap.get r s = heap.get r s'"
using assms by (simp add: heap.Id_on_def heap.get_def)

lemma fun_upd:
  shows "heap.get r (fun_upd s a (Some w))
      = (if heap.addr_of r = a then map heap.rep.from w else heap.get r s)"
by (simp add: heap.get_def)

lemma set_eq:
  shows "heap.get r (heap.set r v s) = v"
by (simp add: heap.get_def heap.set_def comp_def)

lemma set_neq:
  assumes "heap.addr_of r ≠ heap.addr_of r'"
  shows "heap.get r (heap.set r' v s) = heap.get r s"
by (simp add: heap.get_def heap.set_def assms)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "set"›

lemma cong:
  assumes "heap.addr_of r = heap.addr_of r'"
  assumes "v = v'"
  assumes "⋀r'. r' ≠ heap.addr_of r ⟹ s r' = s' r'"
  shows "heap.set r v s = heap.set r' v' s'"
by (simp add: assms heap.set_def fun_eq_iff)

lemma empty:
  shows "heap.set r v (heap.empty) = [heap.addr_of r ↦ map heap.rep.to v]"
by (simp add: heap.set_def)

lemma fun_upd:
  shows "heap.set r v (fun_upd s a w) = (fun_upd s a w)(heap.addr_of r ↦ map heap.rep.to v)"
by (simp add: heap.set_def)

lemma same:
  shows "heap.set r v (heap.set r w s) = heap.set r v s"
by (simp add: heap.set_def)

lemma twist:
  assumes "heap.addr_of r ≠ heap.addr_of r'"
  shows "heap.set r v (heap.set r' w s) = heap.set r' w (heap.set r v s)"
using assms by (simp add: heap.set_def fun_eq_iff)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "obj_at"›

lemma cong[cong]:
  fixes P :: "heap.rep list pred"
  assumes "⋀v. s r = Some v ⟹ P v = P' v"
  assumes "r = r'"
  assumes "s r = s' r'"
  shows "heap.obj_at P r s ⟷ heap.obj_at P' r' s'"
using assms by (simp add: heap.obj_at_def cong: option.case_cong)

lemma split:
  shows "Q (heap.obj_at P r s) ⟷ (s r = None ⟶ Q False) ∧ (∀v. s r = Some v ⟶ Q (P v))"
by (simp add: heap.obj_at_def split: option.splits)

lemma split_asm:
  shows "Q (heap.obj_at P r s) ⟷ ¬ ((s r = None ∧ ¬Q False) ∨ (∃v. s r = Some v ∧ ¬ Q (P v)))"
by (simp add: heap.obj_at_def split: option.splits)

lemmas splits = heap.obj_at.split heap.obj_at.split_asm

lemma empty:
  shows "¬heap.obj_at P r heap.empty"
by (simp add: heap.obj_at_def)

lemma set:
  shows "heap.obj_at P r (heap.set r' v s)
    ⟷ (r = heap.addr_of r' ∧ P (map heap.rep.to v)) ∨ (r ≠ heap.addr_of r' ∧ heap.obj_at P r s)"
by (simp add: comp_def heap.set_def split: heap.obj_at.split)

lemma fun_upd:
  shows "heap.obj_at P r (fun_upd s a (Some w)) = (if r = a then P w else heap.obj_at P r s)"
by (simp split: heap.obj_at.split)

setup ‹Sign.parent_path›

lemmas simps = ―‹ objective: reduce manifest heaps ›
  heap.get.set_eq
  heap.get.fun_upd
  heap.set.empty
  heap.set.same
  heap.set.fun_upd
  heap.obj_at.empty
  heap.obj_at.fun_upd

setup ‹Sign.mandatory_path "Id_on"›

lemma empty[simp]:
  shows "heap.Id⇘{}⇙ = UNIV"
by (simp add: heap.Id_on_def)

lemma sup:
  shows "heap.Id⇘X ∪ Y⇙ = heap.Id⇘X⇙ ∩ heap.Id⇘Y⇙"
unfolding heap.Id_on_def by blast

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "modifies"›

lemma empty[simp]:
  shows "heap.modifies⇘{}⇙ = Id"
by (auto simp: heap.modifies_def)

lemma rep_inv_rel_le:
  shows "heap.modifies⇘rs⇙ ⊆ (⋂r∈rs. heap.rep_inv_rel r)"
by (simp add: heap.modifies_def)

lemma rep_inv:
  assumes "(s, s') ∈ heap.modifies⇘{a}⇙"
  shows "heap.rep_inv a s"
    and "heap.rep_inv a s'"
using assms by (simp_all add: heap.modifies_def split: heap.obj_at.split)

lemma Id_conv:
  shows "(s, s) ∈ heap.modifies⇘rs⇙ ⟷ (∀r∈rs. (s, s) ∈ heap.rep_inv_rel r)"
by (simp add: heap.modifies_def)

lemma eqI:
  assumes "(s, s') ∈ heap.modifies⇘rs⇙"
  assumes "⋀r. ⟦r ∈ rs; heap.rep_inv r s; heap.rep_inv r s'⟧ ⟹ s (heap.addr_of r) = s' (heap.addr_of r)"
  shows "s = s'"
using assms by (simp add: heap.modifies_def) blast

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable.heap"›

lemma Id_on_frame_cong:
  assumes "⋀s s'. (⋀r. r ∈ rs ⟹ heap.rep_inv r s ∧ heap.rep_inv r s' ∧ s (heap.addr_of r) = s' (heap.addr_of r)) ⟹ P s ⟷ P' s'"
  shows "stable heap.Id⇘rs⇙ P ⟷ stable heap.Id⇘rs⇙ P'"
using assms by (auto 10 0 simp: stable_def monotone_def heap.Id_on_def)

lemma Id_on_frameI:
  assumes "⋀s s'. (⋀r. r ∈ rs ⟹ heap.rep_inv r s ∧ heap.rep_inv r s' ∧ s (heap.addr_of r) = s' (heap.addr_of r)) ⟹ P s ⟷ P s'"
  shows "stable heap.Id⇘rs⇙ P"
using assms by (auto simp: stable_def monotone_def heap.Id_on_def)

lemma Id_on_rep_invI[stable.intro]:
  assumes "r ∈ rs"
  shows "stable heap.Id⇘rs⇙ (heap.rep_inv r)"
using assms by (blast intro: stable.heap.Id_on_frameI)

setup ‹Sign.parent_path›


subsection‹ References\label{sec:CImperativeHOL-heap-refs} ›

datatype 'a ref = Ref (addr_of: heap.addr)

instantiation ref :: (heap.rep) heap.addr_of
begin

definition addr_of_ref :: "'a ref ⇒ heap.addr" where
  "addr_of_ref = ref.addr_of"

definition rep_val_inv_ref :: "'a ref ⇒ heap.rep list pred" where
  "rep_val_inv_ref r vs ⟷ (case vs of [v] ⇒ heap.rep.to (heap.rep.from v :: 'a) = v | _⇒ False)"

instance ..

end

instance ref :: (heap.rep) heap.rep
by standard (simp add: inj_on_def ref.expand exI[where x="heap.Addr 0 ∘ ref.addr_of"])

setup ‹Sign.mandatory_path "Ref"›

definition get :: "'a::heap.rep ref ⇒ heap.t ⇒ 'a" where
  "get r s = hd (heap.get r s)"

definition set :: "'a::heap.rep ref ⇒ 'a ⇒ heap.t ⇒ heap.t" where
  "set r v s = heap.set r [v] s"

definition alloc :: "'a ⇒ heap.t ⇒ ('a::heap.rep ref × heap.t) set" where
  "alloc v s = {(r, Ref.set r v s) |r. ¬heap.present r s}"

lemma addr_of:
  shows "heap.addr_of (Ref r) = r"
by (simp add: addr_of_ref_def)

setup ‹Sign.mandatory_path "get"›

lemma fun_upd:
  shows "Ref.get r (fun_upd s a (Some [w]))
      = (if heap.addr_of r = a then heap.rep.from w else Ref.get r s)"
by (simp add: Ref.get_def heap.simps)

lemma set_eq:
  shows "Ref.get r (Ref.set r v s) = v"
by (simp add: Ref.get_def Ref.set_def heap.simps)

lemma set_neq:
  fixes r :: "'a::heap.rep ref"
  fixes r' :: "'b::heap.rep ref"
  assumes "addr_of r ≠ addr_of r'"
  shows "Ref.get r (Ref.set r' v s) = Ref.get r s"
using assms by (simp add: Ref.get_def Ref.set_def addr_of_ref_def heap.get.set_neq)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "set"›

lemma empty:
  shows "Ref.set r v (heap.empty) = [heap.addr_of r ↦ [heap.rep.to v]]"
by (simp add: Ref.set_def heap.simps)

lemma fun_upd:
  shows "Ref.set r v (fun_upd s a w) = (fun_upd s a w)(heap.addr_of r ↦ [heap.rep.to v])"
by (simp add: Ref.set_def heap.simps)

lemma same:
  shows "Ref.set r v (Ref.set r w s) = Ref.set r v s"
by (simp add: Ref.set_def heap.set_def)

lemma obj_at_conv:
  fixes a :: "heap.addr"
  fixes r :: "'a::heap.rep ref"
  fixes v :: "'a"
  fixes P :: "heap.rep list pred"
  shows "heap.obj_at P a (Ref.set r v s) ⟷ (a = heap.addr_of r ∧ P [heap.rep.to v])
                                           ∨ (a ≠ heap.addr_of r ∧ heap.obj_at P a s)"
by (simp add: Ref.set_def heap.set_def split: heap.obj_at.split)

setup ‹Sign.parent_path›

lemmas simps[simp] =
  Ref.addr_of
  Ref.get.set_eq
  Ref.get.set_neq
  Ref.get.fun_upd
  Ref.set.same
  Ref.set.empty
  Ref.set.fun_upd
  Ref.set.obj_at_conv

setup ‹Sign.parent_path›


subsection‹ Arrays\label{sec:CImperativeHOL-heap-arrays} ›


subsubsection‹ Code generation constants: one-dimensional arrays ›

text‹

We ask that targets of the code generator provide implementations of one-dimensional arrays
and the associated operations.

Notes:
 ▪ user-facing arrays make use of \<^class>‹Ix›
 ▪ due to the lack of bounds there is no ‹rep_val_inv›

›

datatype 'a one_dim_array = Array (addr_of: heap.addr)

instantiation one_dim_array :: (type) heap.addr_of
begin

definition addr_of_one_dim_array :: "'a one_dim_array ⇒ heap.addr" where
  "addr_of_one_dim_array = addr_of"

definition rep_val_inv_one_dim_array :: "'a one_dim_array ⇒ heap.rep list pred" where
[simp]: "rep_val_inv_one_dim_array a vs ⟷ True"

instance ..

end

setup ‹Sign.mandatory_path "ODArray"›

definition get :: "'a::heap.rep one_dim_array ⇒ nat ⇒ heap.t ⇒ 'a" where
  "get a i s = heap.get a s ! i"

definition set :: "'a::heap.rep one_dim_array ⇒ nat ⇒ 'a ⇒ heap.t ⇒ heap.t" where
  "set a i v s = heap.set a ((heap.get a s)[i:=v]) s"

definition alloc :: "'a list ⇒ heap.t ⇒ ('a::heap.rep one_dim_array × heap.t) set" where
  "alloc av s = {(a, heap.set a av s) |a. ¬heap.present a s}"

definition list_for :: "'a::heap.rep one_dim_array ⇒ heap.t ⇒ 'a list" where
  "list_for a = heap.get a"

setup ‹Sign.mandatory_path "get"›

lemma weak_cong:
  assumes "i = i'"
  assumes "a = a'"
  assumes "s (heap.addr_of a) = s' (heap.addr_of a')"
  shows "ODArray.get a i s = ODArray.get a' i' s'"
using assms by (simp add: ODArray.get_def cong: heap.get.cong)

lemma weak_Id_on_proj_cong:
  assumes "i = i'"
  assumes "a = a'"
  assumes "(s, s') ∈ heap.Id⇘{a'}⇙"
  shows "ODArray.get a i s = ODArray.get a' i' s'"
using assms by (simp add: ODArray.get_def cong: heap.get.Id_on_proj_cong)

lemma set_eq:
  assumes "i < length (the (s (heap.addr_of a)))"
  shows "ODArray.get a i (ODArray.set a i v s) = v"
using assms by (simp add: ODArray.get_def ODArray.set_def heap.get.set_eq) (simp add: heap.get_def)

lemma set_neq:
  assumes "i ≠ j"
  shows "ODArray.get a i (ODArray.set a j v s) = ODArray.get a i s"
using assms by (simp add: ODArray.get_def ODArray.set_def heap.get.set_eq)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsubsection‹ User-facing arrays ›

datatype ('i, 'a) array = Array (bounds: "('i × 'i)") (arr: "'a one_dim_array")

hide_const (open) bounds arr

instantiation array :: (Ix, heap.rep) heap.addr_of
begin

definition addr_of_array :: "('a, 'b) array ⇒ heap.addr" where
  "addr_of_array = addr_of ∘ array.arr"

definition rep_val_inv_array :: "('a, 'b) array ⇒ heap.rep list pred" where
  "rep_val_inv_array a vs ⟷
      length vs = length (Ix.interval (array.bounds a))
    ∧ (∀v∈set vs. heap.rep.to (heap.rep.from v :: 'b) = v)"

instance ..

end

instance array :: (countable, type) heap.rep
by standard
   (rule exI[where x="λa. heap.Addr (to_nat (array.bounds a)) (addr_of (array.arr a))"],
         rule injI, simp add: array.expand one_dim_array.expand)

setup ‹Sign.mandatory_path "Array"›

abbreviation (input) square :: "('i::Ix × 'i, 'a) array ⇒ bool" where
  "square a ≡ Ix.square (array.bounds a)"

abbreviation (input) index :: "('i::Ix, 'a) array ⇒ 'i ⇒ nat" where
  "index a ≡ Ix.index (array.bounds a)"

abbreviation (input) interval :: "('i::Ix, 'a) array ⇒ 'i list" where
  "interval a ≡ Ix.interval (array.bounds a)"

definition get :: "('i::Ix, 'a::heap.rep) array ⇒ 'i ⇒ heap.t ⇒ 'a" where
  "get a i = ODArray.get (array.arr a) (Array.index a i)"

definition set :: "('i::Ix, 'a::heap.rep) array ⇒ 'i ⇒ 'a ⇒ heap.t ⇒ heap.t" where
  "set a i v = ODArray.set (array.arr a) (Array.index a i) v"

definition list_for :: "('i::Ix, 'a::heap.rep) array ⇒ heap.t ⇒ 'a list" where
  "list_for a = ODArray.list_for (array.arr a)"

―‹ can coerce any indexing regime into any other provided the contents fit ›
definition coerce :: "('i::Ix, 'a::heap.rep) array ⇒ ('j × 'j) ⇒ ('j::Ix, 'a::heap.rep) array option" where
  "coerce a b = (if length (Array.interval a) = length (Ix.interval b)
                 then Some (Array b (array.arr a))
                 else None)"

definition Id_on :: "('i::Ix, 'a::heap.rep) array ⇒ 'i set ⇒ heap.t rel" ("Array.Id⇘_, _⇙") where
  "Array.Id⇘a, is⇙ = heap.rep_inv_rel a ∩ {(s, s'). ∀i∈is. Array.get a i s = Array.get a i s'}"

definition modifies :: "('i::Ix, 'a::heap.rep) array ⇒ 'i set ⇒ heap.t rel" ("Array.modifies⇘_, _⇙") where
  "Array.modifies⇘a, is⇙
    = heap.modifies⇘{a}⇙ ∩ {(s, s'). ∀i∈set (Array.interval a) - is. Array.get a i s = Array.get a i s'}"

lemma simps[simp]:
  shows "heap.addr_of (array.arr a) = heap.addr_of a"
    and "heap.addr_of ∘ array.arr = heap.addr_of"
by (simp_all add: addr_of_array_def addr_of_one_dim_array_def)

setup ‹Sign.mandatory_path "get"›

lemma set_eq:
  assumes "heap.rep_inv a s"
  assumes "i ∈ set (Array.interval a)"
  shows "Array.get a i (Array.set a i v s) = v"
using assms
by (simp add: Array.get_def Array.set_def ODArray.get.set_eq index_length rep_val_inv_array_def
       split: heap.obj_at.split_asm)

lemma set_neq:
  assumes "i ∈ set (Array.interval a)"
  assumes "j ∈ set (Array.interval a)"
  assumes "i ≠ j"
  shows "Array.get a j (Array.set a i v s) = Array.get a j s"
using assms by (simp add: Array.get_def Array.set_def ODArray.get.set_neq index_eq_conv)

lemma Id_on_proj_cong:
  assumes "a = a'"
  assumes "i = i'"
  assumes "(s, s') ∈ Array.Id⇘a', {i'}⇙"
  assumes "i' ∈ set (Array.interval a)"
  shows "Array.get a i s = Array.get a' i' s'"
using assms by (simp add: Array.get_def Array.Id_on_def)

lemma weak_cong:
  assumes "a = a'"
  assumes "i = i'"
  assumes "s (heap.addr_of a) = s' (heap.addr_of a')"
  shows "Array.get a i s = Array.get a' i' s'"
using assms unfolding Array.get_def by (simp cong: ODArray.get.weak_cong)

lemma weak_Id_on_proj_cong:
  assumes "i = i'"
  assumes "a = a'"
  assumes "(s, s') ∈ heap.Id⇘{a'}⇙"
  shows "Array.get a i s = Array.get a' i' s'"
using assms unfolding Array.get_def
by (simp add: heap.Id_on_def  ODArray.get.weak_Id_on_proj_cong split: heap.obj_at.splits)

lemma ext:
  assumes "heap.rep_inv a s"
  assumes "heap.rep_inv a s'"
  assumes "∀i∈set (Ix_class.interval (array.bounds a)). Array.get a i s = Array.get a i s'"
  shows "s (heap.addr_of a) = s' (heap.addr_of a)"
using assms
by (simp add: Array.get_def ODArray.get_def heap.get_def rep_val_inv_array_def
       split: heap.obj_at.splits)
   (rule nth_equalityI, simp, metis index_forE nth_map nth_mem)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "set"›

lemma cong_deref:
  assumes "a = a'"
  assumes "i = i'"
  assumes "v = v'"
  assumes "s r = s' r'"
  assumes "r = r'"
  shows "Array.set a i v s r = Array.set a' i' v' s' r'"
using assms by (clarsimp simp: Array.set_def ODArray.set_def heap.set_def heap.get_def)

lemma same:
  shows "Array.set a i v (Array.set a i v' s) = Array.set a i v s"
by (simp add: Array.set_def ODArray.set_def heap.simps)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "coerce"›

lemma ex_bij_betw:
  fixes a :: "('i::Ix, 'a::heap.rep) array"
  fixes b :: "'j::Ix × 'j"
  assumes "Array.coerce a b = Some a'"
  obtains f where "map f (Array.interval a) = Ix.interval b"
using assms unfolding Array.coerce_def by (metis interval map_map map_nth not_None_eq)

lemma ex_bij_betw2:
  fixes a :: "('i::Ix, 'a::heap.rep) array"
  fixes b :: "'j::Ix × 'j"
  assumes "Array.coerce a b = Some a'"
  obtains f where "map f (Ix.interval b) = Array.interval a"
using assms by (metis Array.coerce_def Array.coerce.ex_bij_betw array.sel(1) option.distinct(1))

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "rep_inv"›

lemma set:
  assumes "heap.rep_inv a s"
  shows "heap.rep_inv a (Array.set a i v s)"
using assms
by (simp add: Array.set_def ODArray.set_def rep_val_inv_array_def heap.set_def heap.get_def
       split: heap.obj_at.splits)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "modifies"›

lemma heap_modifies_le:
  shows "Array.modifies⇘a, is⇙ ⊆ heap.modifies⇘{a}⇙"
by (simp add: Array.modifies_def)

lemma heap_rep_inv_rel_le:
  shows "Array.modifies⇘a, is⇙ ⊆ heap.rep_inv_rel a"
using heap.modifies.rep_inv_rel_le[where rs="{a}"] by (auto simp: Array.modifies_def)

lemma empty:
  shows "Array.modifies⇘a, {}⇙ = Id ∩ heap.rep_inv_rel a" (is "?lhs = ?rhs")
by (auto simp: Array.modifies_def heap.modifies.Id_conv heap.modifies.rep_inv
         elim: heap.modifies.eqI Array.get.ext)

lemma mono:
  assumes "is ⊆ js"
  shows "Array.modifies⇘a, is⇙ ⊆ Array.modifies⇘a, js⇙"
using assms by (auto simp: Array.modifies_def)

lemma INTER:
  shows "Array.modifies⇘a, ⋂x∈X. f x⇙ = (⋂x∈X. Array.modifies⇘a, f x⇙) ∩ heap.modifies⇘{a}⇙"
by (auto simp: Array.modifies_def)

lemma Inter:
  shows "Array.modifies⇘a, ⋂X⇙ = (⋂x∈X. Array.modifies⇘a, x⇙) ∩ heap.modifies⇘{a}⇙"
by (auto simp: Array.modifies_def)

lemma inter:
  shows "Array.modifies⇘a, is⇙ ∩ Array.modifies⇘a, js⇙ = Array.modifies⇘a, is ∩ js⇙"
by (auto simp: Array.modifies_def)

lemma UNION_subseteq:
  shows "(⋃x∈X. Array.modifies⇘a, I x⇙) ⊆ Array.modifies⇘a, (⋃x∈X. I x)⇙"
by (simp add: Array.modifies.mono Sup_upper UN_least)

lemma union_subseteq:
  shows "Array.modifies⇘a, is⇙ ∪ Array.modifies⇘a, js⇙ ⊆ Array.modifies⇘a, is ∪ js⇙"
by (simp add: Array.modifies.mono)

lemma Diag_subseteq:
  assumes "⋀s. P s ⟹ heap.rep_inv a s"
  shows "Diag P ⊆ Array.modifies⇘a, is⇙"
using assms by (auto simp: Array.modifies_def heap.modifies_def Diag_def)

lemma get:
  assumes "(s, s') ∈ Array.modifies⇘a, is⇙"
  assumes "i ∈ set (Array.interval a) - is"
  shows "Array.get a i s' = Array.get a i s"
using assms by (simp add: Array.modifies_def)

lemma set:
  assumes "heap.rep_inv a s"
  shows "(s, Array.set a i v s) ∈ heap.modifies⇘{a}⇙"
using assms
by (simp add: heap.modifies_def Array.set_def ODArray.set_def heap.set_def heap.get_def rep_val_inv_array_def 
       split: heap.obj_at.splits)

lemma Array_set:
  assumes "heap.rep_inv a s"
  assumes "i ∈ set (Array.interval a) ∩ is"
  shows "(s, Array.set a i v s) ∈ Array.modifies⇘a, is⇙"
using assms
by (auto simp: Array.modifies_def Array.rep_inv.set Array.modifies.set
        intro: Array.get.set_neq[symmetric])

lemma Array_set_conv:
  assumes "i ∈ set (Array.interval a) ∩ is"
  shows "(s, Array.set a i v s) ∈ Array.modifies⇘a, is⇙ ⟷ heap.rep_inv a s" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
   using heap.modifies.rep_inv_rel_le[of "{a}", simplified] by (auto simp: Array.modifies_def)
  from assms show "?rhs ⟹ ?lhs"
    by (simp add: Array.modifies.Array_set)
qed

setup ‹Sign.parent_path›

lemmas simps' =
  Array.rep_inv.set
  Array.get.set_eq

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "heap.Id_on.Array"›

lemma Id_on_le:
  shows "heap.Id⇘{a}⇙ ⊆ Array.Id⇘a, is⇙"
by (auto simp: Array.Id_on_def heap.Id_on_def Array.get_def ODArray.get_def heap.get_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "Array.Id_on"›

lemma empty:
  shows "Array.Id⇘a, {}⇙ = heap.rep_inv_rel a"
by (simp add: Array.Id_on_def)

lemma mono:
  assumes "is ⊆ js"
  shows "Array.Id⇘a, js⇙ ⊆ Array.Id⇘a, is⇙"
using assms by (auto simp: Array.Id_on_def)

lemma insert:
  shows "Array.Id⇘a, insert i is⇙ = Array.Id⇘a, {i}⇙ ∩ Array.Id⇘a, is⇙"
by (fastforce simp: Array.Id_on_def)

lemma union:
  shows "Array.Id⇘a, is ∪ js⇙ = Array.Id⇘a, is⇙ ∩ Array.Id⇘a, js⇙"
by (fastforce simp: Array.Id_on_def)

lemma rep_inv_rel:
  shows "Array.Id⇘a, is⇙ ⊆ heap.rep_inv_rel a"
by (simp add: Array.Id_on_def)

lemma eq_heap_Id_on:
  assumes "set (Array.interval a) ⊆ is"
  shows "Array.Id⇘a, is⇙ = heap.Id⇘{a}⇙"
by (rule antisym[OF _ heap.Id_on.Array.Id_on_le])
   (use assms in ‹force simp: Array.Id_on_def heap.Id_on_def elim: Array.get.ext›)

setup ‹Sign.parent_path›


subsubsection‹ Stability\label{sec:CImperativeHOL-heap-stability} ›

setup ‹Sign.mandatory_path "stable.heap.Id_on.Array"›

lemma get[stable.intro]:
  assumes "a ∈ as"
  shows "stable heap.Id⇘as⇙ (λs. P (Array.get a i s))"
using assms by (auto simp: stable_def monotone_def heap.Id_on_def cong: Array.get.weak_cong)

lemma get_chain: ―‹ difficult to apply ›
  assumes "⋀v. stable heap.Id⇘as⇙ (P v)"
  assumes "a ∈ as"
  shows "stable heap.Id⇘as⇙ (λs. P (Array.get a i s) s)"
using assms by (auto simp: stable_def monotone_def heap.Id_on_def cong: Array.get.weak_cong)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable.Array.Id_on.Array"›

lemma get[stable.intro]:
  assumes "i ∈ is"
  shows "stable Array.Id⇘a, is⇙ (λs. P (Array.get a i s))"
using assms by (auto simp: stable_def monotone_def Array.Id_on_def)

lemma get_chain: ―‹ difficult to apply ›
  assumes "⋀v. stable Array.Id⇘a, is⇙ (P v)"
  assumes "i ∈ is"
  shows "stable Array.Id⇘a, is⇙ (λs. P (Array.get a i s) s)"
using assms by (auto simp: stable_def monotone_def Array.Id_on_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable.heap.Array.Id_on.heap"›

lemma rep_inv[stable.intro]:
  shows "stable Array.Id⇘a, is⇙ (heap.rep_inv a)"
by (simp add: stable_def monotone_def Array.Id_on_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable.heap.Array.modifies.heap"›

lemma rep_inv[stable.intro]:
  shows "stable Array.modifies⇘a, is⇙ (heap.rep_inv a)"
by (simp add: stable_def monotone_def Array.modifies_def heap.modifies_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable.heap.Array.modifies.Array"›

lemma get[stable.intro]:
  assumes "i ∈ set (Array.interval a) - is"
  shows "stable Array.modifies⇘a, is⇙ (λs. P (Array.get a i s))"
using assms by (simp add: stable_def monotone_def Array.modifies_def)

lemma get_chain: ―‹ difficult to apply ›
  assumes "⋀v. stable Array.modifies⇘a, is⇙ (P v)"
  assumes "i ∈ set (Array.interval a) - is"
  shows "stable Array.modifies⇘a, is⇙ (λs. P (Array.get a i s) s)"
using assms by (simp add: stable_def monotone_def Array.modifies_def)

setup ‹Sign.parent_path›
(*<*)

end
(*>*)