diff --git a/thys/Real_Time_Deque/Big.thy b/thys/Real_Time_Deque/Big.thy --- a/thys/Real_Time_Deque/Big.thy +++ b/thys/Real_Time_Deque/Big.thy @@ -1,47 +1,47 @@ section \Bigger End of Deque\ theory Big imports Common begin -text \\<^noindent> The bigger end of the deque during transformation can be in two phases: +text \\<^noindent> The bigger end of the deque during rebalancing can be in two phases: \<^descr> \Reverse\: Using the \step\ function the originally contained elements, which will be kept in this end, are reversed. \<^descr> \Common\: Specified in theory \Common\. Is used to reverse the elements from the previous phase again to get them in the original order. \<^noindent> Each phase contains a \current\ state, which holds the original elements of the deque end. \ datatype (plugins del: size) 'a big_state = Reverse "'a current" "'a stack" "'a list" nat | Common "'a common_state" text \\<^noindent> Functions: \<^descr> \push\, \pop\: Add and remove elements using the \current\ state. -\<^descr> \step\: Executes one step of the transformation\ +\<^descr> \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 (Common state) = Common (step state)" | "step (Reverse current _ aux 0) = Common (normalize (Copy current aux [] 0))" | "step (Reverse current big aux count) = Reverse current (Stack.pop big) ((Stack.first big)#aux) (count - 1)" instance.. end fun push :: "'a \ 'a big_state \ 'a big_state" where "push x (Common state) = Common (Common.push x state)" | "push x (Reverse current big aux count) = Reverse (Current.push x current) big aux count" fun pop :: "'a big_state \ 'a * 'a big_state" where "pop (Common state) = (let (x, state) = Common.pop state in (x, Common state))" | "pop (Reverse current big aux count) = (first current, Reverse (drop_first current) big aux count)" end diff --git a/thys/Real_Time_Deque/Big_Aux.thy b/thys/Real_Time_Deque/Big_Aux.thy --- a/thys/Real_Time_Deque/Big_Aux.thy +++ b/thys/Real_Time_Deque/Big_Aux.thy @@ -1,73 +1,73 @@ theory Big_Aux imports Big Common_Aux begin text \\<^noindent> Functions: -\<^descr> \size_new\: Returns the size that the deque end will have after the transformation is finished. +\<^descr> \size_new\: Returns the size that the deque end will have after the rebalancing is finished. \<^descr> \size\: Minimum of \size_new\ and the number of elements contained in the current state. -\<^descr> \remaining_steps\: Returns how many steps are left until the transformation is finished. -\<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished +\<^descr> \remaining_steps\: Returns how many steps are left until the rebalancing is finished. +\<^descr> \list\: List abstraction of the elements which this end will contain after the rebalancing is finished \<^descr> \list_current\: List abstraction of the elements currently in this deque end.\ fun list :: "'a big_state \ 'a list" where "list (Common common) = Common_Aux.list common" | "list (Reverse (Current extra _ _ remained) big aux count) = ( let reversed = take_rev count (Stack_Aux.list big) @ aux in extra @ (take_rev remained reversed) )" fun list_current :: "'a big_state \ 'a list" where "list_current (Common common) = Common_Aux.list_current common" | "list_current (Reverse current _ _ _) = Current_Aux.list current" instantiation big_state ::(type) invar begin fun invar_big_state :: "'a big_state \ bool" where "invar (Common state) \ invar state" | "invar (Reverse current big aux count) \ ( case current of Current extra added old remained \ invar current \ List.length aux \ remained - count \ count \ size big \ Stack_Aux.list old = rev (take (size old) ((rev (Stack_Aux.list big)) @ aux)) \ take remained (Stack_Aux.list old) = rev (take remained (take_rev count (Stack_Aux.list big) @ aux)) )" instance.. end instantiation big_state ::(type) size begin fun size_big_state :: "'a big_state \ nat" where "size (Common state) = size state" | "size (Reverse current _ _ _) = min (size current) (size_new current)" instance.. end instantiation big_state ::(type) size_new begin fun size_new_big_state :: "'a big_state \ nat" where "size_new (Common state) = size_new state" | "size_new (Reverse current _ _ _) = size_new current" instance.. end instantiation big_state ::(type) remaining_steps begin fun remaining_steps_big_state :: "'a big_state \ nat" where "remaining_steps (Common state) = remaining_steps state" | "remaining_steps (Reverse (Current _ _ _ remaining) _ _ count) = count + remaining + 1" instance.. end end diff --git a/thys/Real_Time_Deque/Common.thy b/thys/Real_Time_Deque/Common.thy --- a/thys/Real_Time_Deque/Common.thy +++ b/thys/Real_Time_Deque/Common.thy @@ -1,63 +1,63 @@ section \Common\ theory Common imports Current Idle begin text \ -\<^noindent> The last two phases of both deque ends during transformation: +\<^noindent> The last two phases of both deque ends during rebalancing: \<^descr> \Copy\: Using the \step\ function the new elements of this deque end are brought back into the original order. - \<^descr> \Idle\: The transformation of the deque end is finished. + \<^descr> \Idle\: The rebalancing of the deque end is finished. \<^noindent> Each phase contains a \current\ state, that holds the original elements of the deque end. \ datatype (plugins del: size)'a common_state = Copy "'a current" "'a list" "'a list" nat | Idle "'a current" "'a idle" text\ \<^noindent> Functions: \<^descr> \push\, \pop\: Add and remove elements using the \current\ state. -\<^descr> \step\: Executes one step of the transformation, while keeping the invariant.\ +\<^descr> \step\: Executes one step of the rebalancing, while keeping the invariant.\ (* TODO: Maybe inline function? *) fun normalize :: "'a common_state \ 'a common_state" where "normalize (Copy current old new moved) = ( case current of Current extra added _ remained \ if moved \ remained then Idle current (idle.Idle (Stack extra new) (added + moved)) else Copy current old new moved )" instantiation common_state ::(type) step begin fun step_common_state :: "'a common_state \ 'a common_state" where "step (Idle current idle) = Idle current idle" | "step (Copy current aux new moved) = ( case current of Current _ _ _ remained \ normalize ( if moved < remained then Copy current (tl aux) ((hd aux)#new) (moved + 1) else Copy current aux new moved ) )" instance.. end fun push :: "'a \ 'a common_state \ 'a common_state" where "push x (Idle current (idle.Idle stack stackSize)) = Idle (Current.push x current) (idle.Idle (Stack.push x stack) (Suc stackSize))" | "push x (Copy current aux new moved) = Copy (Current.push x current) aux new moved" fun pop :: "'a common_state \ 'a * 'a common_state" where "pop (Idle current idle) = (let (x, idle) = Idle.pop idle in (x, Idle (drop_first current) idle))" | "pop (Copy current aux new moved) = (first current, normalize (Copy (drop_first current) aux new moved))" end diff --git a/thys/Real_Time_Deque/Common_Aux.thy b/thys/Real_Time_Deque/Common_Aux.thy --- a/thys/Real_Time_Deque/Common_Aux.thy +++ b/thys/Real_Time_Deque/Common_Aux.thy @@ -1,79 +1,79 @@ theory Common_Aux imports Common Current_Aux Idle_Aux begin text\ \<^noindent> Functions: -\<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished +\<^descr> \list\: List abstraction of the elements which this end will contain after the rebalancing is finished \<^descr> \list_current\: List abstraction of the elements currently in this deque end. -\<^descr> \remaining_steps\: Returns how many steps are left until the transformation is finished. -\<^descr> \size_new\: Returns the size, that the deque end will have after the transformation is finished. +\<^descr> \remaining_steps\: Returns how many steps are left until the rebalancing is finished. +\<^descr> \size_new\: Returns the size, that the deque end will have after the rebalancing is finished. \<^descr> \size\: Minimum of \size_new\ and the number of elements contained in the \current\ state.\ definition take_rev where [simp]: "take_rev n xs = rev (take n xs)" fun list :: "'a common_state \ 'a list" where "list (Idle _ idle) = Idle_Aux.list idle" | "list (Copy (Current extra _ _ remained) old new moved) = extra @ take_rev (remained - moved) old @ new" fun list_current :: "'a common_state \ 'a list" where "list_current (Idle current _) = Current_Aux.list current" | "list_current (Copy current _ _ _) = Current_Aux.list current" instantiation common_state::(type) invar begin fun invar_common_state :: "'a common_state \ bool" where "invar (Idle current idle) \ invar idle \ invar current \ size_new current = size idle \ take (size idle) (Current_Aux.list current) = take (size current) (Idle_Aux.list idle)" | "invar (Copy current aux new moved) \ ( case current of Current _ _ old remained \ moved < remained \ moved = length new \ remained \ length aux + moved \ invar current \ take remained (Stack_Aux.list old) = take (size old) (take_rev (remained - moved) aux @ new) )" instance.. end instantiation common_state::(type) size begin fun size_common_state :: "'a common_state \ nat" where "size (Idle current idle) = min (size current) (size idle)" | "size (Copy current _ _ _) = min (size current) (size_new current)" instance.. end instantiation common_state::(type) size_new begin fun size_new_common_state :: "'a common_state \ nat" where "size_new (Idle current _) = size_new current" | "size_new (Copy current _ _ _) = size_new current" instance.. end instantiation common_state::(type) remaining_steps begin fun remaining_steps_common_state :: "'a common_state \ nat" where "remaining_steps (Idle _ _) = 0" | "remaining_steps (Copy (Current _ _ _ remained) aux new moved) = remained - moved" instance.. end end diff --git a/thys/Real_Time_Deque/Current.thy b/thys/Real_Time_Deque/Current.thy --- a/thys/Real_Time_Deque/Current.thy +++ b/thys/Real_Time_Deque/Current.thy @@ -1,32 +1,32 @@ section \Current Stack\ theory Current imports Stack begin text \ \noindent This data structure is composed of: -\<^item> the newly added elements to one end of a deque during the transformation phase +\<^item> the newly added elements to one end of a deque during the rebalancing phase \<^item> the number of these newly added elements \<^item> the originally contained elements -\<^item> the number of elements which will be contained after the transformation is finished. +\<^item> the number of elements which will be contained after the rebalancing is finished. \ datatype (plugins del: size) 'a current = Current "'a list" nat "'a stack" nat fun push :: "'a \ 'a current \ 'a current" where "push x (Current extra added old remained) = Current (x#extra) (added + 1) old remained" fun pop :: "'a current \ 'a * 'a current" where "pop (Current [] added old remained) = (first old, Current [] added (Stack.pop old) (remained - 1))" | "pop (Current (x#xs) added old remained) = (x, Current xs (added - 1) old remained)" fun first :: "'a current \ 'a" where "first current = fst (pop current)" abbreviation drop_first :: "'a current \ 'a current" where "drop_first current \ snd (pop current)" end diff --git a/thys/Real_Time_Deque/RealTimeDeque.thy b/thys/Real_Time_Deque/RealTimeDeque.thy --- a/thys/Real_Time_Deque/RealTimeDeque.thy +++ b/thys/Real_Time_Deque/RealTimeDeque.thy @@ -1,192 +1,192 @@ section \Real-Time Deque Implementation\ theory RealTimeDeque imports States begin text\ The real-time deque can be in the following states: \<^descr> \Empty\: No values stored. No dequeue operation possible. \<^descr> \One\: One element in the deque. \<^descr> \Two\: Two elements in the deque. \<^descr> \Three\: Three elements in the deque. \<^descr> \Idle\: Deque with a left and a right end, fulfilling the following invariant: \<^item> 3 * size of left end \\\ size of right end \<^item> 3 * size of right end \\\ size of left end \<^item> Neither of the ends is empty - \<^descr> \Transforming\: Deque which violated the invariant of the \idle\ state by non-balanced dequeue and enqueue operations. The invariants during in this state are: - \<^item> The transformation is not done yet. The deque needs to be in \idle\ state otherwise. - \<^item> The transformation is in a valid state (Defined in theory \States\) - \<^item> The two ends of the deque are in a size window, such that after finishing the transformation the invariant of the \idle\ state will be met. + \<^descr> \Rebal\: Deque which violated the invariant of the \idle\ state by non-balanced dequeue and enqueue operations. The invariants during in this state are: + \<^item> The rebalancing is not done yet. The deque needs to be in \idle\ state otherwise. + \<^item> The rebalancing is in a valid state (Defined in theory \States\) + \<^item> The two ends of the deque are in a size window, such that after finishing the rebalancing the invariant of the \idle\ state will be met. Functions: \<^descr> \is_empty\: Checks if a deque is in the \Empty\ state - \<^descr> \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 \transformation\ is started or if there are 3 or less elements left the respective states are used. On \transformation\ start, six steps are executed initially. During \transformation\ state four steps are executed and if it is finished the deque returns to \idle\ state. + \<^descr> \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. \<^descr> \deqL\: Removes one element on the left end and only returns the new deque. \<^descr> \firstL\: Removes one element on the left end and only returns the element. - \<^descr> \enqL\: Enqueues an element on the left and returns the resulting deque. Like in \deqL'\ when violating the size invariant in \idle\ state, a \transformation\ with six initial steps is started. During \transformation\ state four steps are executed and if it is finished the deque returns to \idle\ state. + \<^descr> \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. \<^descr> \swap\: The two ends of the deque are swapped. \<^descr> \deqR’\, \deqR\, \firstR\, \enqR\: Same behaviour as the left-counterparts. Implemented using the left-counterparts by swapping the deque before and after the operation. \<^descr> \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 | Idle "'a idle" "'a idle" - | Transforming "'a states" + | 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 (Idle left right) = Idle right left" -| "swap (Transforming (States Left big small)) = (Transforming (States Right big small))" -| "swap (Transforming (States Right big small)) = (Transforming (States Left big small))" +| "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' (Idle 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, Idle (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 = Reverse1 (Current [] 0 left length_left') left [] in let big = Reverse (Current [] 0 right length_right') right [] length_right' in let states = States Left big small in let states = (step^^6) states in - (x, Transforming states) + (x, Rebal states) else case right of Stack r1 r2 \ (x, small_deque r1 r2) )" -| "deqL' (Transforming (States Left big small)) = ( +| "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 (Big.Common (Common.Idle _ big)) (Small.Common (Common.Idle _ small)) \ (x, Idle small big) - | _ \ (x, Transforming states) + | _ \ (x, Rebal states) )" -| "deqL' (Transforming (States Right big small)) = ( +| "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 (Big.Common (Common.Idle _ big)) (Small.Common (Common.Idle _ small)) \ (x, Idle big small) - | _ \ (x, Transforming states) + | _ \ (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) = Idle (idle.Idle (Stack [x, a] []) 2) (idle.Idle (Stack [c, b] []) 2)" | "enqL x (Idle left (idle.Idle right length_right)) = ( case Idle.push x left of idle.Idle left length_left \ if 3 * length_right \ length_left then Idle (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 = Reverse (Current [] 0 left length_left) left [] length_left in let small = Reverse1 (Current [] 0 right length_right) right [] in let states = States Right big small in let states = (step^^6) states in - Transforming states + Rebal states )" -| "enqL x (Transforming (States Left big small)) = ( +| "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 (Big.Common (Common.Idle _ big)) (Small.Common (Common.Idle _ small)) \ Idle small big - | _ \ Transforming states + | _ \ Rebal states )" -| "enqL x (Transforming (States Right big small)) = ( +| "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 (Big.Common (Common.Idle _ big)) (Small.Common (Common.Idle _ small)) \ Idle big small - | _ \ Transforming states + | _ \ Rebal states )" fun enqR :: "'a \ 'a deque \ 'a deque" where "enqR x deque = ( let deque = enqL x (swap deque) in swap deque )" end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Aux.thy b/thys/Real_Time_Deque/RealTimeDeque_Aux.thy --- a/thys/Real_Time_Deque/RealTimeDeque_Aux.thy +++ b/thys/Real_Time_Deque/RealTimeDeque_Aux.thy @@ -1,46 +1,46 @@ theory RealTimeDeque_Aux imports RealTimeDeque States_Aux begin text\ \<^descr> \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 (Idle left right) = Idle_Aux.list left @ (rev (Idle_Aux.list right))" -| "listL (Transforming states) = States_Aux.listL states" +| "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 (Idle left right) \ invar left \ invar right \ \ is_empty left \ \ is_empty right \ 3 * size right \ size left \ 3 * size left \ size right " -| "invar (Transforming states) \ +| "invar (Rebal states) \ invar states \ size_ok states \ 0 < remaining_steps states " instance.. end end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy --- a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy +++ b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy @@ -1,471 +1,471 @@ section "Dequeue Proofs" theory RealTimeDeque_Dequeue_Proof imports Deque RealTimeDeque_Aux States_Proof begin lemma list_deqL' [simp]: "\invar deque; listL deque \ []; deqL' deque = (x, deque')\ \ x # listL deque' = listL deque" proof(induction deque arbitrary: x rule: deqL'.induct) case (4 left right length_right) then obtain left' where pop_left[simp]: "Idle.pop left = (x, left')" by(auto simp: Let_def split: if_splits stack.splits prod.splits idle.splits) then obtain stack_left' length_left' where left'[simp]: "left' = idle.Idle stack_left' length_left'" using idle.exhaust by blast from 4 have invar_left': "invar left'" using Idle_Proof.invar_pop[of left] by auto then have size_left' [simp]: "size stack_left' = length_left'" by auto have size_left'_size_left [simp]: "size stack_left' = (size left) - 1" using Idle_Proof.size_pop_sub[of left x left'] by auto show ?case proof(cases "3 * length_left' \ length_right") case True with 4 pop_left show ?thesis using Idle_Proof.pop_list[of left x left'] by auto next case False - note Start_Transformation = False + note Start_Rebalancing = False then show ?thesis proof(cases "length_left' \ 1") case True let ?big = "Reverse (Current [] 0 right (size right - Suc length_left')) right [] (size right - Suc length_left')" let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" let ?states = "States Left ?big ?small" - from 4 Start_Transformation True invar_left' have invar: "invar ?states" + from 4 Start_Rebalancing True invar_left' have invar: "invar ?states" by(auto simp: Let_def rev_take rev_drop) - with 4 Start_Transformation True invar_left' + with 4 Start_Rebalancing True invar_left' have "States_Aux.listL ?states = tl (Idle_Aux.list left) @ rev (Stack_Aux.list right)" using pop_list_tl'[of left x left'] by (auto simp del: take_rev_def) with invar have "States_Aux.listL ((step^^6) ?states) = tl (Idle_Aux.list left) @ rev (Stack_Aux.list right)" using step_n_listL[of ?states 6] by presburger - with 4 Start_Transformation True show ?thesis + with 4 Start_Rebalancing True show ?thesis by(auto simp: Let_def) next case False - from False Start_Transformation 4 have [simp]:"size left = 1" + from False Start_Rebalancing 4 have [simp]:"size left = 1" using size_left' size_left'_size_left by auto - with False Start_Transformation 4 have [simp]: "Idle_Aux.list left = [x]" + with False Start_Rebalancing 4 have [simp]: "Idle_Aux.list left = [x]" by(induction left)(auto simp: length_one_hd split: stack.splits) obtain right1 right2 where "right = Stack right1 right2" using Stack_Aux.list.cases by blast - with False Start_Transformation 4 show ?thesis + with False Start_Rebalancing 4 show ?thesis by(induction right1 right2 rule: small_deque.induct) auto qed qed next case (5 big small) then have start_invar: "invar (States Left big small)" by auto from 5 have small_invar: "invar small" by auto from 5 have small_size: "0 < size small" by auto with 5(3) obtain small' where pop: "Small.pop small = (x, small')" by(cases small) (auto simp: Let_def split: states.splits direction.splits state_splits prod.splits) let ?states_new = "States Left big small'" let ?states_stepped = "(step^^4) ?states_new" have invar: "invar ?states_new" using pop start_invar small_size invar_pop_small[of Left big small x small'] by auto have "x # Small_Aux.list_current small' = Small_Aux.list_current small" using small_invar small_size pop Small_Proof.pop_list_current[of small x small'] by auto then have listL: "x # States_Aux.listL ?states_new = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" using invar small_size Small_Proof.pop_list_current[of small x small'] 5(1) by auto from invar have "invar ?states_stepped" using invar_step_n by blast then have states_listL_list_current [simp]: "x # States_Aux.listL ?states_stepped = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" using States_Proof.step_n_listL invar listL by metis - then have "listL (deqL (Transforming (States Left big small))) = States_Aux.listL ?states_stepped" + then have "listL (deqL (Rebal (States Left big small))) = States_Aux.listL ?states_stepped" by(auto simp: Let_def pop split: prod.splits direction.splits states.splits state_splits) then have states_listL_list_current: - "x # listL (deqL (Transforming (States Left big small))) = + "x # listL (deqL (Rebal (States Left big small))) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by auto - with 5(1) have "listL (Transforming (States Left big small)) = + with 5(1) have "listL (Rebal (States Left big small)) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by auto with states_listL_list_current - have "x # listL (deqL (Transforming (States Left big small))) = - listL (Transforming (States Left big small))" + have "x # listL (deqL (Rebal (States Left big small))) = + listL (Rebal (States Left big small))" by auto with 5 show ?case by auto next case (6 big small) then have start_invar: "invar (States Right big small)" by auto from 6 have big_invar: "invar big" by auto from 6 have big_size: "0 < size big" by auto with 6(3) obtain big' where pop: "Big.pop big = (x, big')" by(cases big) (auto simp: Let_def split: prod.splits direction.splits states.splits state_splits) let ?states_new = "States Right big' small" let ?states_stepped = "(step^^4) ?states_new" have invar: "invar ?states_new" using pop start_invar big_size invar_pop_big[of Right big small] by auto have big_list_current: "x # Big_Aux.list_current big' = Big_Aux.list_current big" using big_invar big_size pop by auto then have listL: "x # States_Aux.listL ?states_new = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" proof(cases "States_Aux.lists ?states_new") case (Pair bigs smalls) with invar big_list_current show ?thesis using app_rev[of smalls bigs] by(auto split: prod.splits) qed from invar have four_steps: "invar ?states_stepped" using invar_step_n by blast then have [simp]: "x # States_Aux.listL ?states_stepped = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using States_Proof.step_n_listL[of ?states_new 4] invar listL by auto - then have "listL (deqL (Transforming (States Right big small))) = + then have "listL (deqL (Rebal (States Right big small))) = States_Aux.listL ?states_stepped" by(auto simp: Let_def pop split: prod.splits direction.splits states.splits state_splits) then have listL_list_current: - "x # listL (deqL (Transforming (States Right big small))) = + "x # listL (deqL (Rebal (States Right big small))) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" by auto - with 6(1) have "listL (Transforming (States Right big small)) = + with 6(1) have "listL (Rebal (States Right big small)) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using invar_list_big_first[of "States Right big small"] by fastforce with listL_list_current have - "x # listL (deqL (Transforming (States Right big small))) = - listL (Transforming (States Right big small))" + "x # listL (deqL (Rebal (States Right big small))) = + listL (Rebal (States Right big small))" by auto with 6 show ?case by auto qed auto lemma list_deqL [simp]: "\invar deque; listL deque \ []\ \ listL (deqL deque) = tl (listL deque)" using cons_tl[of "fst (deqL' deque)" "listL (deqL deque)" "listL deque"] by(auto split: prod.splits) lemma list_firstL [simp]: "\invar deque; listL deque \ []\ \ firstL deque = hd (listL deque)" using cons_hd[of "fst (deqL' deque)" "listL (deqL deque)" "listL deque"] by(auto split: prod.splits) lemma invar_deqL: "\invar deque; \ is_empty deque\ \ invar (deqL deque)" proof(induction deque rule: deqL'.induct) case (4 left right length_right) then obtain x left' where pop_left[simp]: "Idle.pop left = (x, left')" by fastforce then obtain stack_left' length_left' where left'[simp]: "left' = idle.Idle stack_left' length_left'" using idle.exhaust by blast from 4 have invar_left': "invar left'" "invar left" using Idle_Proof.invar_pop by fastforce+ have [simp]: "size stack_left' = size left - 1" by (metis Idle_Proof.size_pop_sub left' pop_left size_idle.simps) have [simp]: "length_left' = size left - 1" using invar_left' by auto from 4 have list: "x # Idle_Aux.list left' = Idle_Aux.list left" using Idle_Proof.pop_list[of left x left'] by auto show ?case proof(cases "length_right \ 3 * size left'") case True with 4 invar_left' show ?thesis by(auto simp: Stack_Proof.size_empty[symmetric]) next case False - note Start_Transformation = False + note Start_Rebalancing = False then show ?thesis proof(cases "1 \ size left'") case True let ?big = "Reverse (Current [] 0 right (size right - Suc length_left')) right [] (size right - Suc length_left')" let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" let ?states = "States Left ?big ?small" - from 4 Start_Transformation True invar_left' + from 4 Start_Rebalancing True invar_left' have invar: "invar ?states" by(auto simp: Let_def rev_take rev_drop) then have invar_stepped: "invar ((step^^6) ?states)" using invar_step_n by blast - from 4 Start_Transformation True + from 4 Start_Rebalancing True have remaining_steps: "6 < remaining_steps ?states" by auto then have remaining_steps_end: "0 < remaining_steps ((step^^6) ?states)" by(simp only: remaining_steps_n_steps_sub[of ?states 6] invar) - from 4 Start_Transformation True + from 4 Start_Rebalancing True have size_ok': "size_ok' ?states (remaining_steps ?states - 6)" by auto then have size_ok: "size_ok ((step^^6) ?states)" using invar remaining_steps size_ok_steps by blast - from True Start_Transformation 4 show ?thesis + from True Start_Rebalancing 4 show ?thesis using remaining_steps_end size_ok invar_stepped by(auto simp: Let_def) next case False - from False Start_Transformation 4 have [simp]: "size left = 1" + from False Start_Rebalancing 4 have [simp]: "size left = 1" by auto - with False Start_Transformation 4 have [simp]: "Idle_Aux.list left = [x]" + with False Start_Rebalancing 4 have [simp]: "Idle_Aux.list left = [x]" using list[symmetric] by(auto simp: list Stack_Proof.list_empty_size) obtain right1 right2 where "right = Stack right1 right2" using Stack_Aux.list.cases by blast - with False Start_Transformation 4 show ?thesis + with False Start_Rebalancing 4 show ?thesis by(induction right1 right2 rule: small_deque.induct) auto qed qed next case (5 big small) obtain x small' where small' [simp]: "Small.pop small = (x, small')" by fastforce let ?states = "States Left big small'" let ?states_stepped = "(step^^4) ?states" obtain big_stepped small_stepped where stepped [simp]: "?states_stepped = States Left big_stepped small_stepped" by (metis remaining_steps_states.cases step_n_same) from 5 have invar: "invar ?states" using invar_pop_small[of Left big small x small'] by auto then have invar_stepped: "invar ?states_stepped" using invar_step_n by blast show ?case proof(cases "4 < remaining_steps ?states") case True then have remaining_steps: "0 < remaining_steps ?states_stepped" using invar remaining_steps_n_steps_sub[of ?states 4] by simp from True have size_ok: "size_ok ?states_stepped" using step_4_pop_small_size_ok[of Left big small x small'] 5(1) by auto from remaining_steps size_ok invar_stepped show ?thesis by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: common_state.split) next case False then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" using invar by(auto simp del: stepped) then obtain small_current small_idle big_current big_idle where idle [simp]: " States Left big_stepped small_stepped = States Left (big_state.Common (common_state.Idle big_current big_idle)) (small_state.Common (common_state.Idle small_current small_idle)) " using remaining_steps_idle' invar_stepped remaining_steps_stepped by fastforce have size_new_small : "1 < size_new small" using 5 by auto have [simp]: "size_new small = Suc (size_new small')" using 5 by auto have [simp]: "size_new small' = size_new small_stepped" using invar step_n_size_new_small stepped by metis have [simp]: "size_new small_stepped = size small_idle" using idle invar_stepped by(cases small_stepped) auto have [simp]: "\is_empty small_idle" using size_new_small by (simp add: Idle_Proof.size_not_empty) have [simp]: "size_new big = size_new big_stepped" by (metis invar step_n_size_new_big stepped) have [simp]: "size_new big_stepped = size big_idle" using idle invar_stepped by(cases big_stepped) auto have "0 < size big_idle" using 5 by auto then have [simp]: "\is_empty big_idle" by (auto simp: Idle_Proof.size_not_empty) have [simp]: "size small_idle \ 3 * size big_idle" using 5 by auto have [simp]: "size big_idle \ 3 * size small_idle" using 5 by auto show ?thesis using invar_stepped by auto qed next case (6 big small) obtain x big' where big' [simp]: "Big.pop big = (x, big')" by fastforce let ?states = "States Right big' small" let ?states_stepped = "(step^^4) ?states" obtain big_stepped small_stepped where stepped [simp]: "?states_stepped = States Right big_stepped small_stepped" by (metis remaining_steps_states.cases step_n_same) from 6 have invar: "invar ?states" using invar_pop_big[of Right big small x big'] by auto then have invar_stepped: "invar ?states_stepped" using invar_step_n by blast show ?case proof(cases "4 < remaining_steps ?states") case True then have remaining_steps: "0 < remaining_steps ?states_stepped" using invar remaining_steps_n_steps_sub[of ?states 4] by simp from True have size_ok: "size_ok ?states_stepped" using step_4_pop_big_size_ok[of Right big small x big'] 6(1) by auto from remaining_steps size_ok invar_stepped show ?thesis by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: common_state.split) next case False then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" using invar by(auto simp del: stepped) then obtain small_current small_idle big_current big_idle where idle [simp]: " States Right big_stepped small_stepped = States Right (big_state.Common (common_state.Idle big_current big_idle)) (small_state.Common (common_state.Idle small_current small_idle)) " using remaining_steps_idle' invar_stepped remaining_steps_stepped by fastforce have size_new_big : "1 < size_new big" using 6 by auto have [simp]: "size_new big = Suc (size_new big')" using 6 by auto have [simp]: "size_new big' = size_new big_stepped" using invar step_n_size_new_big stepped by metis have [simp]: "size_new big_stepped = size big_idle" using idle invar_stepped by(cases big_stepped) auto have [simp]: "\is_empty big_idle" using size_new_big by (simp add: Idle_Proof.size_not_empty) have [simp]: "size_new small = size_new small_stepped" by (metis invar step_n_size_new_small stepped) have [simp]: "size_new small_stepped = size small_idle" using idle invar_stepped by(cases small_stepped) auto have "0 < size small_idle" using 6 by auto then have [simp]: "\is_empty small_idle" by (auto simp: Idle_Proof.size_not_empty) have [simp]: "size big_idle \ 3 * size small_idle" using 6 by auto have [simp]: "size small_idle \ 3 * size big_idle" using 6 by auto show ?thesis using invar_stepped by auto qed qed auto end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Proof.thy --- a/thys/Real_Time_Deque/RealTimeDeque_Proof.thy +++ b/thys/Real_Time_Deque/RealTimeDeque_Proof.thy @@ -1,130 +1,130 @@ section \Top-Level Proof\ theory RealTimeDeque_Proof imports RealTimeDeque_Dequeue_Proof RealTimeDeque_Enqueue_Proof begin lemma swap_lists_left: "invar (States Left big small) \ States_Aux.listL (States Left big small) = rev (States_Aux.listL (States Right big small))" by(auto split: prod.splits big_state.splits small_state.splits) lemma swap_lists_right: "invar (States Right big small) \ States_Aux.listL (States Right big small) = rev (States_Aux.listL (States Left big small))" by(auto split: prod.splits big_state.splits small_state.splits) lemma swap_list [simp]: "invar q \ listR (swap q) = listL q" proof(induction q) - case (Transforming states) + case (Rebal states) then show ?case apply(cases states) using swap_lists_left swap_lists_right by (metis (full_types) RealTimeDeque_Aux.listL.simps(6) direction.exhaust invar_deque.simps(6) swap.simps(6) swap.simps(7)) qed auto lemma swap_list': "invar q \ listL (swap q) = listR q" using swap_list rev_swap by blast lemma lists_same: "lists (States Left big small) = lists (States Right big small)" by(induction "States Left big small" rule: lists.induct) auto lemma invar_swap: "invar q \ invar (swap q)" by(induction q rule: swap.induct) (auto simp: lists_same split: prod.splits) lemma listL_is_empty: "invar deque \ is_empty deque = (listL deque = [])" using Idle_Proof.list_empty listL_remaining_steps by(cases deque) auto interpretation RealTimeDeque: Deque where empty = empty and enqL = enqL and enqR = enqR and firstL = firstL and firstR = firstR and deqL = deqL and deqR = deqR and is_empty = is_empty and listL = listL and invar = invar proof (standard, goal_cases) case 1 then show ?case by (simp add: empty_def) next case 2 then show ?case by(simp add: list_enqL) next case (3 q x) then have "listL (enqL x (swap q)) = x # listR q" by (simp add: list_enqL invar_swap swap_list') with 3 show ?case by (simp add: invar_enqL invar_swap) next case 4 then show ?case using list_deqL by simp next case (5 q) then have "listL (deqL (swap q)) = tl (listR q)" using 5 list_deqL swap_list' invar_swap by fastforce then have "listR (swap (deqL (swap q))) = tl (listR q)" using 5 swap_list' invar_deqL invar_swap listL_is_empty swap_list by metis then show ?case by(auto split: prod.splits) next case 6 then show ?case using list_firstL by simp next case (7 q) from 7 have [simp]: "listR q = listL (swap q)" by (simp add: invar_swap swap_list') from 7 have [simp]: "firstR q = firstL (swap q)" by(auto split: prod.splits) from 7 have "listL (swap q) \ []" by auto with 7 have "firstL (swap q) = hd (listL (swap q))" using invar_swap list_firstL by blast then show ?case using \firstR q = firstL (swap q)\ by auto next case 8 then show ?case using listL_is_empty by auto next case 9 then show ?case by (simp add: empty_def) next case 10 then show ?case by(simp add: invar_enqL) next case 11 then show ?case by (simp add: invar_enqL invar_swap) next case 12 then show ?case using invar_deqL by simp next case (13 q) then have "invar (swap (deqL (swap q)))" by (metis invar_deqL invar_swap listL_is_empty rev.simps(1) swap_list) then show ?case by (auto split: prod.splits) qed end diff --git a/thys/Real_Time_Deque/Small.thy b/thys/Real_Time_Deque/Small.thy --- a/thys/Real_Time_Deque/Small.thy +++ b/thys/Real_Time_Deque/Small.thy @@ -1,62 +1,62 @@ section \Smaller End of Deque\ theory Small imports Common begin text \ -\<^noindent> The smaller end of the deque during \transformation\ can be in one three phases: +\<^noindent> The smaller end of the deque during \Rebalancing\ can be in one three phases: \<^descr> \Reverse1\: Using the \step\ function the originally contained elements are reversed. \<^descr> \Reverse2\: Using the \step\ function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase. \<^descr> \Common\: See theory \Common\. Is used to reverse the elements from the two previous phases again to get them again in the original order. \<^noindent> Each phase contains a \current\ state, which holds the original elements of the deque end. \ datatype (plugins del: size) 'a small_state = Reverse1 "'a current" "'a stack" "'a list" | Reverse2 "'a current" "'a list" "'a stack" "'a list" nat | Common "'a common_state" text \\<^noindent> Functions: \<^descr> \push\, \pop\: Add and remove elements using the \current\ state. - \<^descr> \step\: Executes one step of the transformation, while keeping the invariant.\ + \<^descr> \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 (Common state) = Common (step state)" | "step (Reverse1 current small auxS) = ( if is_empty small then Reverse1 current small auxS else Reverse1 current (Stack.pop small) ((Stack.first small)#auxS) )" | "step (Reverse2 current auxS big newS count) = ( if is_empty big then Common (normalize (Copy current auxS newS count)) else Reverse2 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 (Common state) = Common (Common.push x state)" | "push x (Reverse1 current small auxS) = Reverse1 (Current.push x current) small auxS" | "push x (Reverse2 current auxS big newS count) = Reverse2 (Current.push x current) auxS big newS count" fun pop :: "'a small_state \ 'a * 'a small_state" where "pop (Common state) = ( let (x, state) = Common.pop state in (x, Common state) )" | "pop (Reverse1 current small auxS) = (first current, Reverse1 (drop_first current) small auxS)" | "pop (Reverse2 current auxS big newS count) = (first current, Reverse2 (drop_first current) auxS big newS count)" end \ No newline at end of file diff --git a/thys/Real_Time_Deque/Small_Aux.thy b/thys/Real_Time_Deque/Small_Aux.thy --- a/thys/Real_Time_Deque/Small_Aux.thy +++ b/thys/Real_Time_Deque/Small_Aux.thy @@ -1,67 +1,67 @@ theory Small_Aux imports Small Common_Aux begin text \\<^noindent> Functions: - \<^descr> \size_new\: Returns the size, that the deque end will have after the transformation is finished. + \<^descr> \size_new\: Returns the size, that the deque end will have after the rebalancing is finished. \<^descr> \size\: Minimum of \size_new\ and the number of elements contained in the `current` state. - \<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished. The first phase is not covered, since the elements, which will be transferred from the bigger deque end are not known yet. + \<^descr> \list\: List abstraction of the elements which this end will contain after the rebalancing is finished. The first phase is not covered, since the elements, which will be transferred from the bigger deque end are not known yet. \<^descr> \list_current\: List abstraction of the elements currently in this deque end.\ fun list :: "'a small_state \ 'a list" where "list (Common common) = Common_Aux.list common" | "list (Reverse2 (Current extra _ _ remained) aux big new count) = extra @ (take_rev (remained - (count + size big)) aux) @ (rev (Stack_Aux.list big) @ new)" fun list_current :: "'a small_state \ 'a list" where "list_current (Common common) = Common_Aux.list_current common" | "list_current (Reverse2 current _ _ _ _) = Current_Aux.list current" | "list_current (Reverse1 current _ _) = Current_Aux.list current" instantiation small_state::(type) invar begin fun invar_small_state :: "'a small_state \ bool" where "invar (Common state) = invar state" | "invar (Reverse2 current auxS big newS count) = ( case current of Current _ _ old remained \ remained = count + size big + size old \ count = List.length newS \ invar current \ List.length auxS \ size old \ Stack_Aux.list old = rev (take (size old) auxS) )" | "invar (Reverse1 current small auxS) = ( case current of Current _ _ old remained \ invar current \ remained \ size old \ size small + List.length auxS \ size old \ Stack_Aux.list old = rev (take (size old) (rev (Stack_Aux.list small) @ auxS)) )" instance.. end instantiation small_state::(type) size begin fun size_small_state :: "'a small_state \ nat" where "size (Common state) = size state" | "size (Reverse2 current _ _ _ _) = min (size current) (size_new current)" | "size (Reverse1 current _ _) = min (size current) (size_new current)" instance.. end instantiation small_state::(type) size_new begin fun size_new_small_state :: "'a small_state \ nat" where "size_new (Common state) = size_new state" | "size_new (Reverse2 current _ _ _ _) = size_new current" | "size_new (Reverse1 current _ _) = size_new current" instance.. end end