Theory HOL-Data_Structures.Array_Specs

theory Array_Specs
imports Main
begin

text ‹Array Specifications›

locale Array =
fixes lookup :: "'ar  nat  'a"
fixes update :: "nat  'a  'ar  'ar"
fixes len :: "'ar  nat"
fixes array :: "'a list  'ar"

fixes list :: "'ar  'a list"
fixes invar :: "'ar  bool"

assumes lookup: "invar ar  n < len ar  lookup ar n = list ar ! n"
assumes update: "invar ar  n < len ar  list(update n x ar) = (list ar)[n:=x]"
assumes len_array: "invar ar  len ar = length (list ar)"
assumes array: "list (array xs) = xs"

assumes invar_update: "invar ar  n < len ar  invar(update n x ar)"
assumes invar_array: "invar(array xs)"

locale Array_Flex = Array +
fixes add_lo :: "'a  'ar  'ar"
fixes del_lo :: "'ar  'ar"
fixes add_hi :: "'a  'ar  'ar"
fixes del_hi :: "'ar  'ar"

assumes add_lo: "invar ar  list(add_lo a ar) = a # list ar"
assumes del_lo: "invar ar  list(del_lo ar) = tl (list ar)"
assumes add_hi: "invar ar  list(add_hi a ar) = list ar @ [a]"
assumes del_hi: "invar ar  list(del_hi ar) = butlast (list ar)"

assumes invar_add_lo: "invar ar  invar (add_lo a ar)"
assumes invar_del_lo: "invar ar  invar (del_lo ar)"
assumes invar_add_hi: "invar ar  invar (add_hi a ar)"
assumes invar_del_hi: "invar ar  invar (del_hi ar)"

end