Theory RealTimeDeque_Aux

theory RealTimeDeque_Aux
  imports RealTimeDeque States_Aux
begin

text‹
 ➧ ‹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.
›

fun listL :: "'a deque ⇒ 'a list" where
  "listL Empty = []"
| "listL (One x) = [x]"
| "listL (Two x y) = [x, y]"
| "listL (Three x y z) = [x, y, z]"
| "listL (Idles left right) = Idle_Aux.list left @ (rev (Idle_Aux.list right))"
| "listL (Rebal states) = States_Aux.listL states"

abbreviation listR :: "'a deque ⇒ 'a list" where
  "listR deque ≡ rev (listL deque)"

instantiation deque::(type) invar
begin

fun invar_deque :: "'a deque ⇒ bool" where
  "invar Empty = True"
| "invar (One _) = True"
| "invar (Two _ _) = True"
| "invar (Three _ _ _) = True"
| "invar (Idles left right) ⟷
   invar left  ∧
   invar right ∧
   ¬ is_empty left  ∧ 
   ¬ is_empty right ∧
   3 * size right ≥ size left ∧
   3 * size left ≥ size right
  "
| "invar (Rebal states) ⟷ 
   invar states ∧
   size_ok states ∧
   0 < remaining_steps states
  "

instance..
end

end