Quelle Big.thy

Sprache: Isabelle

section ‹Bigger End of Deque›

theory Big
imports Common
begin

text ‹🪙 The bigger end of the deque during rebalancing can be in two phases:

🪙 ‹Big1›: Using the ‹step› function the originally contained elements,
which will be kept in this end, are reversed.
🪙 ‹Big2›: Specified in theory ‹Common›. Is used to reverse the elements from the previous phase
again to get them in the original order.

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

datatype (plugins del: size) 'a big_state =
     Big1 "'a current" "'a stack" "'a list" nat
   | Big2 "'a common_state"

text ‹🪙 Functions:

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

instantiation big_state ::(type) step
begin

fun step_big_state :: "'a big_state ==> 'a big_state" where
  "step (Big2 state) = Big2 (step state)"
| "step (Big1 current _ aux 0) = Big2 (normalize (Copy current aux [] 0))"
| "step (Big1 current big aux count) =
     Big1 current (Stack.pop big) ((Stack.first big)#aux) (count - 1)"

instance..
end

fun push :: "'a ==> 'a big_state ==> 'a big_state" where
  "push x (Big2 state) = Big2 (Common.push x state)"
| "push x (Big1 current big aux count) = Big1 (Current.push x current) big aux count"

fun pop :: "'a big_state ==> 'a * 'a big_state" where
  "pop (Big2 state) = (let (x, state) = Common.pop state in (x, Big2 state))"
| "pop (Big1 current big aux count) =
    (first current, Big1 (drop_first current) big aux count)"

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.