Theory Current_Aux

theory Current_Aux
imports Current Stack_Aux
begin

text ‹Specification functions:
➧ ‹list›: list abstraction for the originally contained elements of a deque end during transformation.
➧ ‹invar›: Is the stored number of newly added elements correct?
➧ ‹size›: The number of the originally contained elements.
➧ ‹size_new›: Number of elements which will be contained after the transformation is finished.›

fun list :: "'a current ⇒ 'a list" where
  "list (Current extra _ old _) = extra @ (Stack_Aux.list old)"

instantiation current::(type) invar
begin

fun invar_current :: "'a current ⇒ bool" where
  "invar (Current extra added _ _) ⟷ length extra = added"

instance..
end

instantiation current::(type) size
begin

fun size_current :: "'a current ⇒ nat" where
  "size (Current _ added old _) = added + size old"

instance..
end

instantiation current::(type) size_new
begin

fun size_new_current :: "'a current ⇒ nat" where
  "size_new (Current _ added _ remained) = added + remained"

instance..
end

end