SSL Small.thy

section ‹Smaller End of Deque›

theory Small
imports Common
begin

text ‹
 🪙 The smaller end of the deque during ‹Rebalancing› can be in one three phases:

 🪙 ‹Small1›: Using the ‹step› function the originally contained elements are reversed.
 🪙 ‹Small2›: Using the ‹step› function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase.
 🪙 ‹Small3›: See theory ‹Common›. Is used to reverse the elements from the two previous phases again to get them again in the original order.

 🪙 Each phase contains a ‹current› state, which holds the original elements of the deque end.
 ›

datatype (plugins del: size) 'a small_state =
   Small1 "'a current" "'a stack" "'a list"
 | Small2 "'a current" "'a list" "'a stack" "'a list" nat
 | Small3 "'a common_state"

text ‹🪙 Functions:

 🪙 ‹push›, ‹pop›: Add and remove elements using the ‹current› state.
 🪙 ‹step›: Executes one step of the rebalancing, while keeping the invariant.›

instantiation small_state::(type) step
begin

fun step_small_state :: "'a small_state ==> 'a small_state" where
  "step (Small3 state) = Small3 (step state)"
| "step (Small1 current small auxS) = (
    if is_empty small
    then Small1 current small auxS
    else Small1 current (Stack.pop small) ((Stack.first small)#auxS)
  )"
| "step (Small2 current auxS big newS count) = (
    if is_empty big
    then Small3 (normalize (Copy current auxS newS count))
    else Small2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1)
  )"

instance..
end

fun push :: "'a ==> 'a small_state ==> 'a small_state" where
  "push x (Small3 state) = Small3 (Common.push x state)"
| "push x (Small1 current small auxS) = Small1 (Current.push x current) small auxS"
| "push x (Small2 current auxS big newS count) =
    Small2 (Current.push x current) auxS big newS count"

fun pop :: "'a small_state ==> 'a * 'a small_state" where
  "pop (Small3 state) = (
    let (x, state) = Common.pop state
    in (x, Small3 state)
  )"
| "pop (Small1 current small auxS) =
    (first current, Small1 (drop_first current) small auxS)"
| "pop (Small2 current auxS big newS count) =
    (first current, Small2 (drop_first current) auxS big newS count)"

end