| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Real_Time_Deque/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
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 th again to get them in the original order. 🚫 Each phase contains a ‹current› state, which holds the original elements of t 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 co 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
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01