Theory RealTimeDeque

section ‹Real-Time Deque Implementation›

theory RealTimeDeque
imports States
begin

text‹
The real-time deque can be in the following states:

 ➧ ‹Empty›: No values stored. No dequeue operation possible.
 ➧ ‹One›: One element in the deque.
 ➧ ‹Two›: Two elements in the deque.
 ➧ ‹Three›: Three elements in the deque.
 ➧ ‹Idles›: Deque with a left and a right end, fulfilling the following invariant:
   ▪ 3 * size of left end ‹≥› size of right end
   ▪ 3 * size of right end ‹≥› size of left end
   ▪ Neither of the ends is empty
 ➧ ‹Rebal›: Deque which violated the invariant of the ‹Idles› state by non-balanced dequeue and enqueue operations. The invariants during in this state are:
   ▪ The rebalancing is not done yet. The deque needs to be in ‹Idles› state otherwise.
   ▪ The rebalancing is in a valid state (Defined in theory ‹States›)
   ▪ The two ends of the deque are in a size window, such that after finishing the rebalancing the invariant of the ‹Idles› state will be met. 

Functions:

 ➧ ‹is_empty›: Checks if a deque is in the ‹Empty› state
 ➧ ‹deqL'›: Dequeues an element on the left end and return the element and the deque without this element. If the deque is in ‹idle› state and the size invariant is violated either a ‹rebalancing› is started or if there are 3 or less elements left the respective states are used. On ‹rebalancing› start, six steps are executed initially. During ‹rebalancing› state four steps are executed and if it is finished the deque returns to ‹idle› state.
 ➧ ‹deqL›: Removes one element on the left end and only returns the new deque.
 ➧ ‹firstL›: Removes one element on the left end and only returns the element.
 ➧ ‹enqL›: Enqueues an element on the left and returns the resulting deque. Like in ‹deqL'› when violating the size invariant in ‹idle› state, a ‹rebalancing› with six initial steps is started. During ‹rebalancing› state four steps are executed and if it is finished the deque returns to ‹idle› state.
 ➧ ‹swap›: The two ends of the deque are swapped.
 ➧ ‹deqR'›, ‹deqR›, ‹firstR›, ‹enqR›: Same behaviour as the left-counterparts. Implemented using the left-counterparts by swapping the deque before and after the operation.
 ➧ ‹listL›, ‹listR›: Get all elements of the deque in a list starting at the left or right end. They are needed as list abstractions for the correctness proofs.
›

datatype 'a deque =
    Empty
  | One 'a
  | Two 'a 'a
  | Three 'a 'a 'a 
  | Idles "'a idle" "'a idle"
  | Rebal "'a states"

definition empty where
  "empty = Empty"

instantiation deque::(type) is_empty
begin

fun is_empty_deque :: "'a deque ⇒ bool" where
  "is_empty_deque Empty = True"
| "is_empty_deque _ = False"

instance..
end

fun swap :: "'a deque ⇒ 'a deque" where
  "swap Empty = Empty"  
| "swap (One x) = One x"
| "swap (Two x y) = Two y x"
| "swap (Three x y z) = Three z y x"
| "swap (Idles left right) = Idles right left"
| "swap (Rebal (States Left big small)) = (Rebal (States Right big small))"
| "swap (Rebal (States Right big small)) = (Rebal (States Left big small))"

fun small_deque :: "'a list ⇒ 'a list ⇒ 'a deque" where
  "small_deque []     [] = Empty"

| "small_deque (x#[]) [] = One x"
| "small_deque [] (x#[]) = One x"

| "small_deque (x#[])(y#[]) = Two y x"
| "small_deque (x#y#[]) [] = Two y x"
| "small_deque [] (x#y#[])= Two y x"

| "small_deque [] (x#y#z#[])   = Three z y x"
| "small_deque (x#y#z#[]) []   = Three z y x"
| "small_deque (x#y#[]) (z#[]) = Three z y x"
| "small_deque (x#[]) (y#z#[]) = Three z y x"

fun deqL' :: "'a deque ⇒ 'a * 'a deque" where
  "deqL' (One x) = (x, Empty)"
| "deqL' (Two x y) = (x, One y)"
| "deqL' (Three x y z) = (x, Two y z)"
| "deqL' (Idles left (idle.Idle right length_right)) = (
   case Idle.pop left of (x, (idle.Idle left length_left)) ⇒
    if 3 * length_left ≥ length_right 
    then 
      (x, Idles (idle.Idle left length_left) (idle.Idle right length_right))
    else if length_left ≥ 1
    then 
      let length_left' = 2 * length_left + 1 in
      let length_right' = length_right - length_left - 1 in

      let small  = Small1 (Current [] 0 left length_left') left [] in
      let big = Big1 (Current [] 0 right length_right') right [] length_right' in

      let states = States Left big small in
      let states = (step^^6) states in
      
      (x, Rebal states)
    else 
      case right of Stack r1 r2 ⇒ (x, small_deque r1 r2)
  )"
| "deqL' (Rebal (States Left big small)) = (
    let (x, small) = Small.pop small in 
    let states = (step^^4) (States Left big small) in
    case states of 
        States Left
          (Big2 (Common.Idle _ big))
          (Small3 (Common.Idle _ small)) 
           ⇒ (x, Idles small big)
     | _ ⇒ (x, Rebal states)
  )"
| "deqL' (Rebal (States Right big small)) = (
    let (x, big) = Big.pop big in 
    let states = (step^^4) (States Right big small) in
    case states of 
       States Right 
          (Big2 (Common.Idle _ big)) 
          (Small3 (Common.Idle _ small)) ⇒
            (x, Idles big small)
     | _ ⇒ (x, Rebal states)
  )"

fun deqR' :: "'a deque ⇒ 'a * 'a deque" where
  "deqR' deque = (
    let (x, deque) = deqL' (swap deque) 
    in (x, swap deque)
  )"

fun deqL :: "'a deque ⇒ 'a deque" where
  "deqL deque = (let (_, deque) = deqL' deque in deque)"

fun deqR :: "'a deque ⇒ 'a deque" where
  "deqR deque = (let (_, deque) = deqR' deque in deque)"

fun firstL :: "'a deque ⇒ 'a" where
  "firstL deque = (let (x, _) = deqL' deque in x)" 

fun firstR :: "'a deque ⇒ 'a" where
  "firstR deque = (let (x, _) = deqR' deque in x)" 

fun enqL :: "'a ⇒ 'a deque ⇒ 'a deque" where
  "enqL x Empty = One x"
| "enqL x (One y) = Two x y"
| "enqL x (Two y z) = Three x y z"
| "enqL x (Three a b c) = Idles (idle.Idle (Stack [x, a] []) 2) (idle.Idle (Stack [c, b] []) 2)"
| "enqL x (Idles left (idle.Idle right length_right)) = (
    case Idle.push x left of idle.Idle left length_left ⇒ 
      if 3 * length_right ≥ length_left
      then 
        Idles (idle.Idle left length_left) (idle.Idle right length_right)
      else 
        let length_left = length_left - length_right - 1 in
        let length_right = 2 * length_right + 1 in

        let big  = Big1  (Current [] 0 left length_left) left [] length_left in
        let small = Small1 (Current [] 0 right length_right) right [] in
  
        let states = States Right big small in
        let states = (step^^6) states in
        
        Rebal states
  )"
| "enqL x (Rebal (States Left big small)) = (
    let small = Small.push x small in 
    let states = (step^^4) (States Left big small) in
    case states of 
        States Left 
          (Big2 (Common.Idle _ big))
          (Small3 (Common.Idle _ small)) 
         ⇒ Idles small big
     | _ ⇒ Rebal states
  )"
| "enqL x (Rebal (States Right big small)) = (
    let big = Big.push x big in 
    let states = (step^^4) (States Right big small) in
    case states of 
        States Right 
          (Big2 (Common.Idle _ big)) 
          (Small3 (Common.Idle _ small)) 
         ⇒ Idles big small
     | _ ⇒ Rebal states
  )"

fun enqR :: "'a ⇒ 'a deque ⇒ 'a deque" where
  "enqR x deque = (
    let deque = enqL x (swap deque) 
    in swap deque
  )"    

end