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