Theory Idle

section ‹Idle›

theory Idle
imports Stack
begin

text ‹Represents the `idle' state of one deque end.
It contains a ‹stack› and its size as a natural number.›

datatype (plugins del: size) 'a idle = Idle "'a stack" nat

fun push :: "'a ⇒ 'a idle ⇒ 'a idle" where
  "push x (Idle stack stackSize) = Idle (Stack.push x stack) (Suc stackSize)"

fun pop :: "'a idle ⇒ ('a * 'a idle)" where
  "pop (Idle stack stackSize) = (Stack.first stack, Idle (Stack.pop stack) (stackSize - 1))"
  
end