Quelle  CArrays.thy

section "Arrays without bounds"
theory CArrays imports Main begin

text ‹For these arrays there is no
 built-in protection against reading or writing out-of-bounds.›

type_synonym 'a cArray = "nat => 'a"

definition makeCArray :: "nat => 'a => 'a cArray" where
  "makeCArray arraySize fillValue index ==
   if index < arraySize then fillValue else undefined"

definition readCArray :: "'a cArray => nat => 'a" where
  "readCArray array index == array index"

definition writeCArray :: "'a cArray => nat => 'a => 'a cArray" where
  "writeCArray array index value == array(index := value)"

(* ---------------------------------------------------------------*)

lemma makeCArrayCorrect:
  "index < arraySize ==>
   readCArray (makeCArray arraySize fillValue) index = fillValue"
by (simp add: readCArray_def makeCArray_def)

lemma writeCArrayCorrect1:
  "readCArray (writeCArray array index value) index = value"
by (simp add: readCArray_def writeCArray_def)

lemma writeCArrayCorrect2:
  "index1 ~= index2 ==>
   readCArray (writeCArray array index1 value) index2 =
   readCArray array index2"
by (simp add: readCArray_def writeCArray_def)

end