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,44 +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. + \<^descr> \Big1\: Using the \step\ function the originally contained elements, + which will be kept in this end, are reversed. + \<^descr> \Big2\: 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 state = - Reverse "'a current" "'a stack" "'a list" nat - | Common "'a Common.state" +datatype (plugins del: size) 'a big_state = + Big1 "'a current" "'a stack" "'a list" nat + | Big2 "'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 state ::(type) step +instantiation big_state ::(type) step begin -fun step_state :: "'a state \ 'a 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)" +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 state \ 'a 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 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 state \ 'a * 'a 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)" +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 \ No newline at end of file +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,72 @@ 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 state \ 'a list" where - "list (Common common) = Common_Aux.list common" -| "list (Reverse (Current extra _ _ remained) big aux count) = ( +fun list :: "'a big_state \ 'a list" where + "list (Big2 common) = Common_Aux.list common" +| "list (Big1 (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 state \ 'a list" where - "list_current (Common common) = Common_Aux.list_current common" -| "list_current (Reverse current _ _ _) = Current_Aux.list current" +fun list_current :: "'a big_state \ 'a list" where + "list_current (Big2 common) = Common_Aux.list_current common" +| "list_current (Big1 current _ _ _) = Current_Aux.list current" -instantiation state ::(type) invar +instantiation big_state ::(type) invar begin -fun invar_state :: "'a state \ bool" where - "invar (Common state) \ invar state" -| "invar (Reverse current big aux count) \ ( +fun invar_big_state :: "'a big_state \ bool" where + "invar (Big2 state) \ invar state" +| "invar (Big1 current big aux count) \ ( case current of Current extra added old remained \ invar current - \ List.length aux \ remained - count - + \ remained \ length aux + 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 state ::(type) size +instantiation big_state ::(type) size begin -fun size_state :: "'a state \ nat" where - "size (Common state) = size state" -| "size (Reverse current _ _ _) = min (size current) (size_new current)" +fun size_big_state :: "'a big_state \ nat" where + "size (Big2 state) = size state" +| "size (Big1 current _ _ _) = min (size current) (size_new current)" instance.. end -instantiation state ::(type) size_new +instantiation big_state ::(type) size_new begin -fun size_new_state :: "'a state \ nat" where - "size_new (Common state) = size_new state" -| "size_new (Reverse current _ _ _) = size_new current" +fun size_new_big_state :: "'a big_state \ nat" where + "size_new (Big2 state) = size_new state" +| "size_new (Big1 current _ _ _) = size_new current" instance.. end -instantiation state ::(type) remaining_steps +instantiation big_state ::(type) remaining_steps begin -fun remaining_steps_state :: "'a state \ nat" where - "remaining_steps (Common state) = remaining_steps state" -| "remaining_steps (Reverse (Current _ _ _ remaining) _ _ count) = count + remaining + 1" +fun remaining_steps_big_state :: "'a big_state \ nat" where + "remaining_steps (Big2 state) = remaining_steps state" +| "remaining_steps (Big1 (Current _ _ _ remaining) _ _ count) = count + remaining + 1" instance.. end end diff --git a/thys/Real_Time_Deque/Big_Proof.thy b/thys/Real_Time_Deque/Big_Proof.thy --- a/thys/Real_Time_Deque/Big_Proof.thy +++ b/thys/Real_Time_Deque/Big_Proof.thy @@ -1,322 +1,324 @@ section "Big Proofs" theory Big_Proof imports Big_Aux Common_Proof begin lemma step_list [simp]: "invar big \ list (step big) = list big" -proof(induction big rule: step_state.induct) +proof(induction big rule: step_big_state.induct) case 1 then show ?case by auto next case 2 then show ?case by(auto split: current.splits) next case 3 then show ?case by(auto simp: rev_take take_drop drop_Suc tl_take rev_drop split: current.splits) qed lemma step_list_current [simp]: "invar big \ list_current (step big) = list_current big" - by(induction big rule: step_state.induct)(auto split: current.splits) + by(induction big rule: step_big_state.induct)(auto split: current.splits) lemma push_list [simp]: "list (push x big) = x # list big" proof(induction x big rule: push.induct) case (1 x state) then show ?case by auto next case (2 x current big aux count) then show ?case by(induction x current rule: Current.push.induct) auto qed -lemma list_Reverse: "\ - 0 < size (Reverse current big aux count); - invar (Reverse current big aux count) -\ \ first current # list (Reverse (drop_first current) big aux count) = - list (Reverse current big aux count)" +lemma list_Big1: "\ + 0 < size (Big1 current big aux count); + invar (Big1 current big aux count) +\ \ first current # list (Big1 (drop_first current) big aux count) = + list (Big1 current big aux count)" proof(induction current rule: Current.pop.induct) case (1 added old remained) then have [simp]: "remained - Suc 0 < length (take_rev count (Stack_Aux.list big) @ aux)" by(auto simp: le_diff_conv) (* TODO: *) then have " \0 < size old; 0 < remained; added = 0; remained - count \ length aux; count \ size big; Stack_Aux.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack_Aux.list big)))) = rev (take (remained - count) aux) @ rev (take remained (rev (take count (Stack_Aux.list big))))\ \ hd (rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big)))) = (rev (take count (Stack_Aux.list big)) @ aux) ! (remained - Suc 0)" by (smt (verit) Suc_pred hd_drop_conv_nth hd_rev hd_take last_snoc length_rev length_take min.absorb2 rev_append take_rev_def size_list_length take_append take_hd_drop) with 1 have [simp]: "Stack.first old = (take_rev count (Stack_Aux.list big) @ aux) ! (remained - Suc 0)" by(auto simp: take_hd_drop first_hd) from 1 show ?case using take_rev_nth[of "remained - Suc 0" "take_rev count (Stack_Aux.list big) @ aux" "Stack.first old" "[]" ] by auto next case 2 then show ?case by auto qed -lemma size_list [simp]: " \0 < size big; invar big; list big = []\ \ False" +lemma size_list [simp]: "\0 < size big; invar big; list big = []\ \ False" proof(induction big rule: list.induct) case 1 then show ?case using list_size by auto next case 2 then show ?case - by (metis list.distinct(1) list_Reverse) + by (metis list.distinct(1) list_Big1) qed lemma pop_list [simp]: "\0 < size big; invar big; Big.pop big = (x, big')\ \ x # list big' = list big" proof(induction big arbitrary: x rule: list.induct) case 1 then show ?case by(auto split: prod.splits) next case 2 then show ?case - by (metis Big.pop.simps(2) list_Reverse prod.inject) + by (metis Big.pop.simps(2) list_Big1 prod.inject) qed lemma pop_list_tl: "\0 < size big; invar big; pop big = (x, big')\ \ list big' = tl (list big)" using pop_list cons_tl[of x "list big'" "list big"] by force (* TODO: *) -lemma invar_step: "invar (big :: 'a state) \ invar (step big)" -proof(induction big rule: step_state.induct) +lemma invar_step: "invar (big :: 'a big_state) \ invar (step big)" +proof(induction big rule: step_big_state.induct) case 1 then show ?case by(auto simp: invar_step) next case (2 current big aux) then obtain extra old remained where current: "current = Current extra (length extra) old remained" by(auto split: current.splits) (* TODO: *) - with 2 have "\current = Current extra (length extra) old remained; remained \ length aux; + with 2 have "\ + current = Current extra (length extra) old remained; + remained \ length aux; Stack_Aux.list old = - rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))); + rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack_Aux.list big)))) = rev (take remained aux)\ \ remained \ size old" by(metis length_rev length_take min.absorb_iff2 size_list_length take_append) with 2 current have "remained - size old = 0" by auto with current 2 show ?case by(auto simp: take_rev_drop drop_rev) next case (3 current big aux count) then have "0 < size big" by(auto split: current.splits) then have big_not_empty: "Stack_Aux.list big \ []" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) with 3 have a: " rev (Stack_Aux.list big) @ aux = rev (Stack_Aux.list (Stack.pop big)) @ Stack.first big # aux" by(auto simp: rev_tl_hd first_hd split: current.splits) from 3 have "0 < size big" by(auto split: current.splits) from 3 big_not_empty have " take_rev (Suc count) (Stack_Aux.list big) @ aux = take_rev count (Stack_Aux.list (Stack.pop big)) @ (Stack.first big # aux)" using take_rev_tl_hd[of "Suc count" "Stack_Aux.list big" aux] by(auto simp: Stack_Proof.list_not_empty split: current.splits) with 3 a show ?case by(auto split: current.splits) qed lemma invar_push: "invar big \ invar (push x big)" by(induction x big rule: push.induct)(auto simp: invar_push split: current.splits) (* TODO: *) lemma invar_pop: "\ 0 < size big; invar big; pop big = (x, big') \ \ invar big'" proof(induction big arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: invar_pop split: prod.splits) next case (2 current big aux count) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) have linarith: "\x y z. x - y \ z \ x - (Suc y) \ z" by linarith have a: " \remained \ count + length aux; 0 < remained; added = 0; x = Stack.first old; - big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; + big' = Big1 (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; count \ size big; Stack_Aux.list old = rev aux @ Stack_Aux.list big; take remained (rev aux) @ take (remained - length aux) (Stack_Aux.list big) = drop (count + length aux - remained) (rev aux) @ drop (count - remained) (take count (Stack_Aux.list big)); \ size old \ length aux + size big\ \ tl (rev aux @ Stack_Aux.list big) = rev aux @ Stack_Aux.list big" by (metis le_refl length_append length_rev size_list_length) have b: "\remained \ length (take_rev count (Stack_Aux.list big) @ aux); 0 < size old; 0 < remained; added = 0; x = Stack.first old; - big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; + big' = Big1 (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; remained - count \ length aux; count \ size big; Stack_Aux.list old = - drop (length aux - (size old - size big)) (rev aux) @ - drop (size big - size old) (Stack_Aux.list big); + drop (length aux - (size old - size big)) (rev aux) @ + drop (size big - size old) (Stack_Aux.list big); take remained (drop (length aux - (size old - size big)) (rev aux)) @ take (remained + (length aux - (size old - size big)) - length aux) (drop (size big - size old) (Stack_Aux.list big)) = drop (length (take_rev count (Stack_Aux.list big) @ aux) - remained) (rev (take_rev count (Stack_Aux.list big) @ aux))\ \ tl (drop (length aux - (size old - size big)) (rev aux) @ drop (size big - size old) (Stack_Aux.list big)) = drop (length aux - (size old - Suc (size big))) (rev aux) @ drop (Suc (size big) - size old) (Stack_Aux.list big)" apply(cases "size old - size big \ length aux"; cases "size old \ size big") by(auto simp: tl_drop_2 Suc_diff_le le_diff_conv le_refl a) from 1 have "remained \ length (take_rev count (Stack_Aux.list big) @ aux)" by(auto) with 1 show ?case apply(auto simp: rev_take take_tl drop_Suc Suc_diff_le tl_drop linarith simp del: take_rev_def) using b - apply (metis \remained \ length (take_rev count (Stack_Aux.list big) @ aux)\ rev_append rev_take take_append) + apply (metis \remained \ length (take_rev count (Stack_Aux.list big) @ aux)\ le_diff_conv rev_append rev_take take_append) by (smt (verit, del_insts) Nat.diff_cancel tl_append_if Suc_diff_le append_self_conv2 diff_add_inverse diff_diff_cancel diff_is_0_eq diff_le_mono drop_eq_Nil2 length_rev nle_le not_less_eq_eq plus_1_eq_Suc tl_drop_2) next case (2 x xs added old remained) then show ?case by auto qed qed lemma push_list_current [simp]: "list_current (push x big) = x # list_current big" by(induction x big rule: push.induct) auto lemma pop_list_current [simp]: "\invar big; 0 < size big; Big.pop big = (x, big')\ \ x # list_current big' = list_current big" proof(induction big arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: pop_list_current split: prod.splits) next case (2 current big aux count) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))) \ []" using order_less_le_trans[of 0 "size old" "size big"] order_less_le_trans[of 0 count "size big"] by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) with 1 show ?case by(auto simp: first_hd) next case (2 x xs added old remained) then show ?case by auto qed qed lemma list_current_size: "\0 < size big; list_current big = []; invar big\ \ False" proof(induction big rule: list_current.induct) case 1 then show ?case using list_current_size by simp next case (2 current uu uv uw) then show ?case apply(cases current) by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_empty) qed -lemma step_size: "invar (big :: 'a state) \ size big = size (step big)" - by(induction big rule: step_state.induct)(auto split: current.splits) +lemma step_size: "invar (big :: 'a big_state) \ size big = size (step big)" + by(induction big rule: step_big_state.induct)(auto split: current.splits) -lemma remaining_steps_step [simp]: "\invar (big :: 'a state); remaining_steps big > 0\ +lemma remaining_steps_step [simp]: "\invar (big :: 'a big_state); remaining_steps big > 0\ \ Suc (remaining_steps (step big)) = remaining_steps big" - by(induction big rule: step_state.induct)(auto split: current.splits) + by(induction big rule: step_big_state.induct)(auto split: current.splits) -lemma remaining_steps_step_0 [simp]: "\invar (big :: 'a state); remaining_steps big = 0\ +lemma remaining_steps_step_0 [simp]: "\invar (big :: 'a big_state); remaining_steps big = 0\ \ remaining_steps (step big) = 0" by(induction big)(auto split: current.splits) lemma remaining_steps_push: "invar big \ remaining_steps (push x big) = remaining_steps big" by(induction x big rule: push.induct)(auto split: current.splits) lemma remaining_steps_pop: "\invar big; pop big = (x, big')\ \ remaining_steps big' \ remaining_steps big" proof(induction big rule: pop.induct) case (1 state) then show ?case by(auto simp: remaining_steps_pop split: prod.splits) next case (2 current big aux count) then show ?case by(induction current rule: Current.pop.induct) auto qed lemma size_push [simp]: "invar big \ size (push x big) = Suc (size big)" by(induction x big rule: push.induct)(auto split: current.splits) lemma size_new_push [simp]: "invar big \ size_new (push x big) = Suc (size_new big)" by(induction x big rule: Big.push.induct)(auto split: current.splits) lemma size_pop [simp]: "\invar big; 0 < size big; pop big = (x, big')\ \ Suc (size big') = size big" proof(induction big rule: pop.induct) case 1 then show ?case by(auto split: prod.splits) next case (2 current big aux count) then show ?case by(induction current rule: Current.pop.induct) auto qed lemma size_new_pop [simp]: "\invar big; 0 < size_new big; pop big = (x, big')\ \ Suc (size_new big') = size_new big" proof(induction big rule: pop.induct) case 1 then show ?case by(auto split: prod.splits) next case (2 current big aux count) then show ?case by(induction current rule: Current.pop.induct) auto qed -lemma size_size_new: "\invar (big :: 'a state); 0 < size big\ \ 0 < size_new big" +lemma size_size_new: "\invar (big :: 'a big_state); 0 < size big\ \ 0 < size_new big" by(induction big)(auto simp: size_size_new) 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 state = +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 state \ 'a state" where +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 state ::(type) step +instantiation common_state ::(type) step begin -fun step_state :: "'a state \ 'a state" where +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 state \ 'a state" where +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 state \ 'a * 'a state" where +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 state \ 'a list" where +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 state \ 'a list" where +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 state::(type) invar +instantiation common_state::(type) invar begin -fun invar_state :: "'a state \ bool" where +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 state::(type) size +instantiation common_state::(type) size begin -fun size_state :: "'a state \ nat" where +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 state::(type) size_new +instantiation common_state::(type) size_new begin -fun size_new_state :: "'a state \ nat" where +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 state::(type) remaining_steps +instantiation common_state::(type) remaining_steps begin -fun remaining_steps_state :: "'a state \ nat" where +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/Common_Proof.thy b/thys/Real_Time_Deque/Common_Proof.thy --- a/thys/Real_Time_Deque/Common_Proof.thy +++ b/thys/Real_Time_Deque/Common_Proof.thy @@ -1,475 +1,479 @@ section "Common Proofs" theory Common_Proof imports Common_Aux Idle_Proof Current_Proof begin lemma take_rev_drop: "take_rev n xs @ acc = drop (length xs - n) (rev xs) @ acc" unfolding take_rev_def using rev_take by blast lemma take_rev_step: "xs \ [] \ take_rev n (tl xs) @ (hd xs # acc) = take_rev (Suc n) xs @ acc" by (simp add: take_Suc) lemma take_rev_empty [simp]: "take_rev n [] = []" by simp lemma take_rev_tl_hd: "0 < n \ xs \ [] \ take_rev n xs @ ys = take_rev (n - (Suc 0)) (tl xs) @ (hd xs #ys)" by (simp add: take_rev_step del: take_rev_def) lemma take_rev_nth: "n < length xs \ x = xs ! n \ x # take_rev n xs @ ys = take_rev (Suc n) xs @ ys" by (simp add: take_Suc_conv_app_nth) lemma step_list [simp]: "invar common \ list (step common) = list common" -proof(induction common rule: step_state.induct) +proof(induction common rule: step_common_state.induct) case (1 idle) then show ?case by auto next case (2 current aux new moved) then show ?case proof(cases current) case (Current extra added old remained) with 2 have aux_not_empty: "aux \ []" by auto from 2 Current show ?thesis proof(cases "remained \ Suc moved") case True with 2 Current have "remained - length new = 1" by auto with True Current 2 aux_not_empty show ?thesis - by(auto simp: ) + by auto next case False with Current show ?thesis by(auto simp: aux_not_empty take_rev_step Suc_diff_Suc simp del: take_rev_def) qed qed qed lemma step_list_current [simp]: "invar common \ list_current (step common) = list_current common" by(cases common)(auto split: current.splits) lemma push_list [simp]: "list (push x common) = x # list common" proof(induction x common rule: push.induct) case (1 x stack stackSize) then show ?case by auto next case (2 x current aux new moved) then show ?case by(induction x current rule: Current.push.induct) auto qed -lemma invar_step: "invar (common :: 'a state) \ invar (step common)" -proof(induction "common" rule: invar_state.induct) +lemma invar_step: "invar (common :: 'a common_state) \ invar (step common)" +proof(induction "common" rule: invar_common_state.induct) case (1 idle) then show ?case by auto next case (2 current aux new moved) then show ?case proof(cases current) case (Current extra added old remained) then show ?thesis proof(cases "aux = []") case True with 2 Current show ?thesis by auto next case False note AUX_NOT_EMPTY = False then show ?thesis proof(cases "remained \ Suc (length new)") case True with 2 Current False have "take (Suc (length new)) (Stack_Aux.list old) = take (size old) (hd aux # new)" by(auto simp: le_Suc_eq take_Cons') with 2 Current True show ?thesis by auto next case False with 2 Current AUX_NOT_EMPTY show ?thesis by(auto simp: take_rev_step Suc_diff_Suc simp del: take_rev_def) qed qed qed qed lemma invar_push: "invar common \ invar (push x common)" proof(induction x common rule: push.induct) case (1 x current stack stackSize) then show ?case proof(induction x current rule: Current.push.induct) case (1 x extra added old remained) then show ?case proof(induction x stack rule: Stack.push.induct) case (1 x left right) then show ?case by auto qed qed next case (2 x current aux new moved) then show ?case proof(induction x current rule: Current.push.induct) case (1 x extra added old remained) then show ?case by auto qed qed lemma invar_pop: "\ 0 < size common; invar common; pop common = (x, common') \ \ invar common'" proof(induction common arbitrary: x rule: pop.induct) case (1 current idle) then obtain idle' where idle: "Idle.pop idle = (x, idle')" by(auto split: prod.splits) obtain current' where current: "drop_first current = current'" by auto from 1 current idle show ?case using Idle_Proof.size_pop[of idle x idle', symmetric] size_new_pop[of current] size_pop_sub[of current _ current'] by(auto simp: Idle_Proof.invar_pop invar_pop eq_snd_iff take_tl size_not_empty) next case (2 current aux new moved) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case proof(cases "remained - Suc 0 \ length new") case True with 1 have [simp]: "0 < size old" "Stack_Aux.list old \ []" "aux \ []" "length new = remained - Suc 0" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) then have [simp]: "Suc 0 \ size old" by linarith from 1 have "0 < remained" by auto then have "take remained (Stack_Aux.list old) = hd (Stack_Aux.list old) # take (remained - Suc 0) (tl (Stack_Aux.list old))" by (metis Suc_pred \Stack_Aux.list old \ []\ list.collapse take_Suc_Cons) with 1 True show ?thesis using Stack_Proof.pop_list[of old] by(auto simp: Stack_Proof.size_not_empty) next case False with 1 have "remained - Suc 0 \ length aux + length new" by auto with 1 False show ?thesis using Stack_Proof.pop_list[of old] apply(auto simp: Suc_diff_Suc take_tl Stack_Proof.size_not_empty tl_append_if) by (simp add: Suc_diff_le rev_take tl_drop_2 tl_take) qed next case (2 x xs added old remained) then show ?case by auto qed qed lemma push_list_current [simp]: "list_current (push x left) = x # list_current left" by(induction x left rule: push.induct) auto lemma pop_list [simp]: "invar common \ 0 < size common \ pop common = (x, common') \ x # list common' = list common" proof(induction common arbitrary: x rule: pop.induct) case 1 then show ?case by(auto simp: size_not_empty split: prod.splits) next case (2 current aux new moved) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case proof(cases "remained - Suc 0 \ length new") case True from 1 True have [simp]: "aux \ []" "0 < remained" "Stack_Aux.list old \ []" "remained - length new = 1" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) then have "take remained (Stack_Aux.list old) = hd aux # take (size old - Suc 0) new \ Stack.first old = hd aux" by (metis first_hd hd_take list.sel(1)) with 1 True take_hd[of aux] show ?thesis by(auto simp: Suc_leI) next case False then show ?thesis proof(cases "remained - length new = length aux") case True then have length_minus_1: "remained - Suc (length new) = length aux - 1" by simp from 1 have not_empty: "0 < remained" "0 < size old" "aux \ []" "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) from 1 True not_empty have "take 1 (Stack_Aux.list old) = take 1 (rev aux)" using take_1[of remained "size old" "Stack_Aux.list old" "(rev aux) @ take (size old + length new - remained) new" ] by(simp) then have "[last aux] = [Stack.first old]" using take_last first_take not_empty by fastforce then have "last aux = Stack.first old" by auto with 1 True False show ?thesis using not_empty last_drop_rev[of aux] by(auto simp: take_rev_drop length_minus_1 simp del: take_rev_def) next case False with 1 have a: "take (remained - length new) aux \ []" by auto from 1 False have b: "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) from 1 have c: "remained - Suc (length new) < length aux" by auto - from 1 have not_empty: "0 < remained" "0 < size old" "0 < remained - length new" "0 < length aux" + from 1 have not_empty: + "0 < remained" + "0 < size old" + "0 < remained - length new" + "0 < length aux" by auto with False have "take remained (Stack_Aux.list old) = take (size old) (take_rev (remained - length new) aux @ new) \ take (Suc 0) (Stack_Aux.list old) = take (Suc 0) (rev (take (remained - length new) aux))" using take_1[of remained "size old" "Stack_Aux.list old" " (take_rev (remained - length new) aux @ new)" ] by(auto simp: not_empty Suc_le_eq) with 1 False have "take 1 (Stack_Aux.list old) = take 1 (rev (take (remained - length new) aux))" by auto then have d: "[Stack.first old] = [last (take (remained - length new) aux)]" using take_last first_take a b by metis have "last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)" using Suc_diff_Suc c not_empty by (metis a drop_drop last_drop_rev plus_1_eq_Suc rev_take zero_less_diff) with 1(1) 1(3) False not_empty d show ?thesis by(cases "remained - length new = 1") (auto) qed qed next case 2 then show ?case by auto qed qed lemma pop_list_current: "invar common \ 0 < size common \ pop common = (x, common') \ x # list_current common' = list_current common" proof(induction common arbitrary: x rule: pop.induct) case (1 current idle) then show ?case proof(induction idle rule: Idle.pop.induct) case (1 stack stackSize) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "Stack.first old = Stack.first stack" using take_first[of old stack] by auto with 1 show ?case by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) next case (2 x xs added old remained) then have "0 < size stack" by auto with Stack_Proof.size_not_empty Stack_Proof.list_not_empty have not_empty: "\ is_empty stack" "Stack_Aux.list stack \ []" by auto with 2 have "hd (Stack_Aux.list stack) = x" using take_hd'[of "Stack_Aux.list stack" x "xs @ Stack_Aux.list old"] by auto with 2 show ?case using first_list[of stack] not_empty by auto qed qed next case (2 current) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) with 1 show ?case using first_pop by(auto simp: Stack_Proof.list_not_empty) next case 2 then show ?case by auto qed qed lemma list_current_size [simp]: "\0 < size common; list_current common = []; invar common\ \ False" -proof(induction common rule: invar_state.induct) +proof(induction common rule: invar_common_state.induct) case 1 then show ?case using list_size by auto next case (2 current) then have "invar current" "Current_Aux.list current = []" "0 < size current" by(auto split: current.splits) then show ?case using list_size by auto qed lemma list_size [simp]: "\0 < size common; list common = []; invar common\ \ False" -proof(induction common rule: invar_state.induct) +proof(induction common rule: invar_common_state.induct) case 1 then show ?case using list_size Idle_Proof.size_empty by auto next case (2 current aux new moved) then have "invar current" "Current_Aux.list current = []" "0 < size current" by(auto split: current.splits) then show ?case using list_size by auto qed -lemma step_size [simp]: "invar (common :: 'a state) \ size (step common) = size common" -proof(induction common rule: step_state.induct) +lemma step_size [simp]: "invar (common :: 'a common_state) \ size (step common) = size common" +proof(induction common rule: step_common_state.induct) case 1 then show ?case by auto next case 2 then show ?case by(auto simp: min_def split: current.splits) qed -lemma step_size_new [simp]: "invar (common :: 'a state) +lemma step_size_new [simp]: "invar (common :: 'a common_state) \ size_new (step common) = size_new common" -proof(induction common rule: step_state.induct) +proof(induction common rule: step_common_state.induct) case (1 current idle) then show ?case by auto next case (2 current aux new moved) then show ?case by(auto split: current.splits) qed -lemma remaining_steps_step [simp]: "\invar (common :: 'a state); remaining_steps common > 0\ +lemma remaining_steps_step [simp]: "\invar (common :: 'a common_state); remaining_steps common > 0\ \ Suc (remaining_steps (step common)) = remaining_steps common" by(induction common)(auto split: current.splits) -lemma remaining_steps_step_sub [simp]: "\invar (common :: 'a state)\ +lemma remaining_steps_step_sub [simp]: "\invar (common :: 'a common_state)\ \ remaining_steps (step common) = remaining_steps common - 1" by(induction common)(auto split: current.splits) -lemma remaining_steps_step_0 [simp]: "\invar (common :: 'a state); remaining_steps common = 0\ +lemma remaining_steps_step_0 [simp]: "\invar (common :: 'a common_state); remaining_steps common = 0\ \ remaining_steps (step common) = 0" by(induction common)(auto split: current.splits) lemma remaining_steps_push [simp]: "invar common \ remaining_steps (push x common) = remaining_steps common" by(induction x common rule: Common.push.induct)(auto split: current.splits) lemma remaining_steps_pop: "\invar common; pop common = (x, common')\ \ remaining_steps common' \ remaining_steps common" proof(induction common rule: pop.induct) case (1 current idle) then show ?case proof(induction idle rule: Idle.pop.induct) case 1 then show ?case by(induction current rule: Current.pop.induct) auto qed next case (2 current aux new moved) then show ?case by(induction current rule: Current.pop.induct) auto qed lemma size_push [simp]: "invar common \ size (push x common) = Suc (size common)" by(induction x common rule: push.induct) (auto split: current.splits) lemma size_new_push [simp]: "invar common \ size_new (push x common) = Suc (size_new common)" by(induction x common rule: Common.push.induct) (auto split: current.splits) lemma size_pop [simp]: "\invar common; 0 < size common; pop common = (x, common')\ \ Suc (size common') = size common" proof(induction common rule: Common.pop.induct) case (1 current idle) then show ?case using size_drop_first_sub[of current] Idle_Proof.size_pop_sub[of idle] by(auto simp: size_not_empty split: prod.splits) next case (2 current aux new moved) then show ?case by(induction current rule: Current.pop.induct) auto qed lemma size_new_pop [simp]: "\invar common; 0 < size_new common; pop common = (x, common')\ \ Suc (size_new common') = size_new common" proof(induction common rule: Common.pop.induct) case (1 current idle) then show ?case using size_new_pop[of current] by(auto split: prod.splits) next case (2 current aux new moved) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case by auto next case (2 x xs added old remained) then show ?case by auto qed qed -lemma size_size_new: "\invar (common :: 'a state); 0 < size common\ \ 0 < size_new common" +lemma size_size_new: "\invar (common :: 'a common_state); 0 < size common\ \ 0 < size_new common" by(cases common) auto end \ No newline at end of file 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: + \<^descr> \Idles\: 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 \Idles\ 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 \Idles\ 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 \Idles\ 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" + | 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 (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 (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' (Idle left (idle.Idle right length_right)) = ( +| "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, Idle (idle.Idle left length_left) (idle.Idle right length_right)) + (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 = Reverse1 (Current [] 0 left length_left') left [] in - let big = Reverse (Current [] 0 right length_right') right [] length_right' 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, 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) + (Big2 (Common.Idle _ big)) + (Small3 (Common.Idle _ small)) + \ (x, Idles small big) + | _ \ (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) + (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) = Idle (idle.Idle (Stack [x, a] []) 2) (idle.Idle (Stack [c, b] []) 2)" -| "enqL x (Idle left (idle.Idle right length_right)) = ( +| "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 - Idle (idle.Idle left length_left) (idle.Idle right length_right) + 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 = Reverse (Current [] 0 left length_left) left [] length_left in - let small = Reverse1 (Current [] 0 right length_right) right [] 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 - 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 + (Big2 (Common.Idle _ big)) + (Small3 (Common.Idle _ small)) + \ Idles small big + | _ \ 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 + (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 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 (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 (Idle left right) \ +| "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 (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')) + let ?big = "Big1 (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 ?small = "Small1 (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 + "Big1 (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 ?small = "Small1 (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) + 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 (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle)) + (Big2 (common_state.Idle big_current big_idle)) + (Small3 (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) + 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 (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle)) + (Big2 (common_state.Idle big_current big_idle)) + (Small3 (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_Enqueue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy --- a/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy +++ b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy @@ -1,324 +1,324 @@ section "Enqueue Proofs" theory RealTimeDeque_Enqueue_Proof imports Deque RealTimeDeque_Aux States_Proof begin lemma list_enqL: "invar deque \ listL (enqL x deque) = x # listL deque" proof(induction x deque rule: enqL.induct) case (5 x left right length_right) obtain left' length_left' where pushed [simp]: "Idle.push x left = idle.Idle left' length_left'" using is_empty_idle.cases by blast then have invar_left': "invar (idle.Idle left' length_left')" using Idle_Proof.invar_push[of left x] 5 by auto show ?case proof(cases "length_left' \ 3 * length_right") case True then show ?thesis using Idle_Proof.push_list[of x left] by(auto simp: Let_def) next case False let ?length_left = "length_left' - length_right - 1" let ?length_right = "2 * length_right + 1" - let ?big = "Reverse (Current [] 0 left' ?length_left) left' [] ?length_left" - let ?small = "Reverse1 (Current [] 0 right ?length_right) right []" + let ?big = "Big1 (Current [] 0 left' ?length_left) left' [] ?length_left" + let ?small = "Small1 (Current [] 0 right ?length_right) right []" let ?states = "States Right ?big ?small" let ?states_stepped = "(step^^6) ?states" from False 5 invar_left' have invar: "invar ?states" by(auto simp: rev_drop rev_take) then have "States_Aux.listL ?states = x # Idle_Aux.list left @ rev (Stack_Aux.list right)" using Idle_Proof.push_list[of x left] by(auto) then have "States_Aux.listL ?states_stepped = x # Idle_Aux.list left @ rev (Stack_Aux.list right)" by (metis invar step_n_listL) with False show ?thesis by(auto simp: Let_def) qed next case (6 x big small) let ?small = "Small.push x small" let ?states = "States Left big ?small" let ?states_stepped = "(step^^4) ?states" obtain big_stepped small_stepped where stepped: "?states_stepped = States Left big_stepped small_stepped" by (metis remaining_steps_states.cases step_n_same) from 6 have "invar ?states" using invar_push_small[of Left big small x] by auto then have "States_Aux.listL ?states_stepped = x # Small_Aux.list_current small @ rev (Big_Aux.list_current big)" using step_n_listL by fastforce with 6 show ?case by(cases big_stepped; cases small_stepped) - (auto simp: Let_def stepped split!: Common.state.split) + (auto simp: Let_def stepped split!: common_state.split) next case (7 x big small) let ?big = "Big.push x big" let ?states = "States Right ?big small" let ?states_stepped = "(step^^4) ?states" obtain big_stepped small_stepped where stepped: "?states_stepped = States Right big_stepped small_stepped" by (metis remaining_steps_states.cases step_n_same) from 7 have list_invar: "list_current_small_first (States Right big small) = list_small_first (States Right big small)" by auto from 7 have invar: "invar ?states" using invar_push_big[of Right big small x] by auto then have "States_Aux.listL ?states = x # Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using app_rev[of _ _ _ "x # Big_Aux.list_current big"] by(auto split: prod.split) then have "States_Aux.listL ?states_stepped = x # Big_Aux.list_current big @ rev (Small_Aux.list_current small)" by (metis invar step_n_listL) with list_invar show ?case using app_rev[of "Small_Aux.list_current small" "Big_Aux.list_current big"] by(cases big_stepped; cases small_stepped) - (auto simp: Let_def stepped split!: prod.split Common.state.split) + (auto simp: Let_def stepped split!: prod.split common_state.split) qed auto lemma invar_enqL: "invar deque \ invar (enqL x deque)" proof(induction x deque rule: enqL.induct) case (5 x left right length_right) obtain left' length_left' where pushed [simp]: "Idle.push x left = idle.Idle left' length_left'" using is_empty_idle.cases by blast then have invar_left': "invar (idle.Idle left' length_left')" using Idle_Proof.invar_push[of left x] 5 by auto have [simp]: "size left' = Suc (size left)" using Idle_Proof.size_push[of x left] by auto show ?case proof(cases "length_left' \ 3 * length_right") case True with 5 show ?thesis using invar_left' Idle_Proof.size_push[of x left] Stack_Proof.size_not_empty[of left'] by auto next case False let ?length_left = "length_left' - length_right - 1" let ?length_right = "Suc (2 * length_right)" let ?states = "States Right - (Reverse (Current [] 0 left' ?length_left) left' [] ?length_left) - (Reverse1 (Current [] 0 right ?length_right) right [])" + (Big1 (Current [] 0 left' ?length_left) left' [] ?length_left) + (Small1 (Current [] 0 right ?length_right) right [])" let ?states_stepped = "(step^^6) ?states" from invar_left' 5 False have invar: "invar ?states" by(auto simp: rev_drop rev_take) then have invar_stepped: "invar ?states_stepped" using invar_step_n by blast from False invar_left' 5 have remaining_steps: "6 < remaining_steps ?states" using Stack_Proof.size_not_empty[of right] by auto then have remaining_steps_stepped: "0 < remaining_steps ?states_stepped" using invar remaining_steps_n_steps_sub by (metis zero_less_diff) from False invar_left' 5 have "size_ok' ?states (remaining_steps ?states - 6)" using Stack_Proof.size_not_empty[of right] size_not_empty by auto then have size_ok_stepped: "size_ok ?states_stepped" using size_ok_steps[of ?states 6] remaining_steps invar by blast from False show ?thesis using invar_stepped remaining_steps_stepped size_ok_stepped by(auto simp: Let_def) qed next case (6 x big small) let ?small = "Small.push x small" let ?states = "States Left big ?small" let ?states_stepped = "(step^^4) ?states" from 6 have invar: "invar ?states" using invar_push_small[of Left big small x] 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 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 True have remaining_steps: "0 < remaining_steps ?states_stepped" using invar remaining_steps_n_steps_sub[of ?states 4] by simp from True 6(1) have size_ok: "size_ok ?states_stepped" using step_4_push_small_size_ok[of Left big small x] remaining_steps_push_small[of Left big small x] 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) + (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 then obtain small_current small_idle big_current big_idle where idle [simp]: " ?states_stepped = States Left - (Big.state.Common (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle)) + (Big2 (common_state.Idle big_current big_idle)) + (Small3 (common_state.Idle small_current small_idle)) " using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same by (smt (verit) invar_states.elims(2)) from 6 have [simp]: "size_new (Small.push x small) = Suc (size_new small)" using Small_Proof.size_new_push by auto have [simp]: "size small_idle = size_new (Small.push x small)" using invar invar_stepped step_n_size_new_small[of Left big "Small.push x small" 4] by auto then have [simp]: "\is_empty small_idle" using Idle_Proof.size_not_empty[of small_idle] by auto have size_new_big [simp]: "0 < size_new big" using 6 by auto then have [simp]: "size big_idle = size_new big" using invar invar_stepped step_n_size_new_big[of Left big "Small.push x small" 4] by auto then have [simp]: "\is_empty big_idle" using Idle_Proof.size_not_empty size_new_big by metis have size_ok_1: "size small_idle \ 3 * size big_idle" using 6 by auto have size_ok_2: "size big_idle \ 3 * size small_idle" using 6 by auto from False show ?thesis using invar_stepped size_ok_1 size_ok_2 by auto qed next case (7 x big small) let ?big = "Big.push x big" let ?states = "States Right ?big small" let ?states_stepped = "(step^^4) ?states" from 7 have invar: "invar ?states" using invar_push_big[of Right big small x] 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 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 True have remaining_steps: "0 < remaining_steps ?states_stepped" using invar remaining_steps_n_steps_sub[of ?states 4] by simp from True 7(1) have size_ok: "size_ok ?states_stepped" using step_4_push_big_size_ok[of Right big small x] remaining_steps_push_big[of Right big small x] 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) + (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 then obtain small_current small_idle big_current big_idle where idle [simp]: " ?states_stepped = States Right - (Big.state.Common (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle)) + (Big2 (common_state.Idle big_current big_idle)) + (Small3 (common_state.Idle small_current small_idle)) " using remaining_steps_idle' invar_stepped remaining_steps_stepped step_n_same by (smt (verit) invar_states.elims(2)) from 7 have [simp]: "size_new (Big.push x big) = Suc (size_new big)" using Big_Proof.size_new_push by auto have [simp]: "size big_idle = size_new (Big.push x big)" using invar invar_stepped step_n_size_new_big[of Right "Big.push x big" small 4] by auto then have [simp]: "\is_empty big_idle" using Idle_Proof.size_not_empty[of big_idle] by auto have size_new_small [simp]: "0 < size_new small" using 7 by auto then have [simp]: "size small_idle = size_new small" using invar invar_stepped step_n_size_new_small[of Right "Big.push x big" small 4] by auto then have [simp]: "\is_empty small_idle" using Idle_Proof.size_not_empty size_new_small by metis have size_ok_1: "size small_idle \ 3 * size big_idle" using 7 by auto have size_ok_2: "size big_idle \ 3 * size small_idle" using 7 by auto from False show ?thesis using invar_stepped size_ok_1 size_ok_2 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) + 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) + 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. + \<^descr> \Small1\: Using the \step\ function the originally contained elements are reversed. + \<^descr> \Small2\: 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> \Small3\: 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 state = - Reverse1 "'a current" "'a stack" "'a list" - | Reverse2 "'a current" "'a list" "'a stack" "'a list" nat - | Common "'a Common.state" +datatype (plugins del: size) 'a small_state = + Small1 "'a current" "'a stack" "'a list" + | Small2 "'a current" "'a list" "'a stack" "'a list" nat + | Small3 "'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 state::(type) step +instantiation small_state::(type) step begin -fun step_state :: "'a state \ 'a state" where - "step (Common state) = Common (step state)" -| "step (Reverse1 current small auxS) = ( +fun step_small_state :: "'a small_state \ 'a small_state" where + "step (Small3 state) = Small3 (step state)" +| "step (Small1 current small auxS) = ( if is_empty small - then Reverse1 current small auxS - else Reverse1 current (Stack.pop small) ((Stack.first small)#auxS) + then Small1 current small auxS + else Small1 current (Stack.pop small) ((Stack.first small)#auxS) )" -| "step (Reverse2 current auxS big newS count) = ( +| "step (Small2 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) + then Small3 (normalize (Copy current auxS newS count)) + else Small2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1) )" instance.. end -fun push :: "'a \ 'a state \ 'a 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 push :: "'a \ 'a small_state \ 'a small_state" where + "push x (Small3 state) = Small3 (Common.push x state)" +| "push x (Small1 current small auxS) = Small1 (Current.push x current) small auxS" +| "push x (Small2 current auxS big newS count) = + Small2 (Current.push x current) auxS big newS count" -fun pop :: "'a state \ 'a * 'a state" where - "pop (Common state) = ( +fun pop :: "'a small_state \ 'a * 'a small_state" where + "pop (Small3 state) = ( let (x, state) = Common.pop state - in (x, Common state) + in (x, Small3 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)" +| "pop (Small1 current small auxS) = + (first current, Small1 (drop_first current) small auxS)" +| "pop (Small2 current auxS big newS count) = + (first current, Small2 (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 state \ 'a list" where - "list (Common common) = Common_Aux.list common" -| "list (Reverse2 (Current extra _ _ remained) aux big new count) = +fun list :: "'a small_state \ 'a list" where + "list (Small3 common) = Common_Aux.list common" +| "list (Small2 (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 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" +fun list_current :: "'a small_state \ 'a list" where + "list_current (Small3 common) = Common_Aux.list_current common" +| "list_current (Small2 current _ _ _ _) = Current_Aux.list current" +| "list_current (Small1 current _ _) = Current_Aux.list current" -instantiation state::(type) invar +instantiation small_state::(type) invar begin -fun invar_state :: "'a state \ bool" where - "invar (Common state) = invar state" -| "invar (Reverse2 current auxS big newS count) = ( +fun invar_small_state :: "'a small_state \ bool" where + "invar (Small3 state) = invar state" +| "invar (Small2 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) = ( +| "invar (Small1 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 state::(type) size +instantiation small_state::(type) size begin -fun size_state :: "'a 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)" +fun size_small_state :: "'a small_state \ nat" where + "size (Small3 state) = size state" +| "size (Small2 current _ _ _ _) = min (size current) (size_new current)" +| "size (Small1 current _ _) = min (size current) (size_new current)" instance.. end -instantiation state::(type) size_new +instantiation small_state::(type) size_new begin -fun size_new_state :: "'a state \ nat" where - "size_new (Common state) = size_new state" -| "size_new (Reverse2 current _ _ _ _) = size_new current" -| "size_new (Reverse1 current _ _) = size_new current" +fun size_new_small_state :: "'a small_state \ nat" where + "size_new (Small3 state) = size_new state" +| "size_new (Small2 current _ _ _ _) = size_new current" +| "size_new (Small1 current _ _) = size_new current" instance.. end end diff --git a/thys/Real_Time_Deque/Small_Proof.thy b/thys/Real_Time_Deque/Small_Proof.thy --- a/thys/Real_Time_Deque/Small_Proof.thy +++ b/thys/Real_Time_Deque/Small_Proof.thy @@ -1,232 +1,233 @@ section "Small Proofs" theory Small_Proof imports Common_Proof Small_Aux begin -lemma step_size [simp]: "invar (small :: 'a state) \ size (step small) = size small" - by(induction small rule: step_state.induct)(auto split: current.splits) +lemma step_size [simp]: "invar (small :: 'a small_state) \ size (step small) = size small" + by(induction small rule: step_small_state.induct)(auto split: current.splits) -lemma step_size_new [simp]: "invar (small :: 'a state) \ size_new (step small) = size_new small" - by(induction small rule: step_state.induct)(auto split: current.splits) +lemma step_size_new [simp]: + "invar (small :: 'a small_state) \ size_new (step small) = size_new small" + by(induction small rule: step_small_state.induct)(auto split: current.splits) lemma size_push [simp]: "invar small \ size (push x small) = Suc (size small)" by(induction x small rule: push.induct) (auto split: current.splits) lemma size_new_push [simp]: "invar small \ size_new (push x small) = Suc (size_new small)" by(induction x small rule: push.induct) (auto split: current.splits) lemma size_pop [simp]: "\invar small; 0 < size small; pop small = (x, small')\ \ Suc (size small') = size small" proof(induction small rule: pop.induct) case (1 state) then show ?case by(auto split: prod.splits) next case (2 current small auxS) then show ?case using Current_Proof.size_pop[of current] by(induction current rule: Current.pop.induct) auto next case (3 current auxS big newS count) then show ?case using Current_Proof.size_pop[of current] by(induction current rule: Current.pop.induct) auto qed lemma size_new_pop [simp]: "\invar small; 0 < size_new small; pop small = (x, small')\ \ Suc (size_new small') = size_new small" proof(induction small rule: pop.induct) case (1 state) then show ?case by(auto split: prod.splits) next case (2 current small auxS) then show ?case by(induction current rule: Current.pop.induct) auto next case (3 current auxS big newS count) then show ?case by(induction current rule: Current.pop.induct) auto qed -lemma size_size_new: "\invar (small :: 'a state); 0 < size small\ \ 0 < size_new small" +lemma size_size_new: "\invar (small :: 'a small_state); 0 < size small\ \ 0 < size_new small" by(induction small)(auto simp: size_size_new) lemma step_list_current [simp]: "invar small \ list_current (step small) = list_current small" - by(induction small rule: step_state.induct)(auto split: current.splits) + by(induction small rule: step_small_state.induct)(auto split: current.splits) lemma step_list_common [simp]: - "\small = Common common; invar small\ \ list (step small) = list small" + "\small = Small3 common; invar small\ \ list (step small) = list small" by auto -lemma step_list_reverse2 [simp]: +lemma step_list_Small2 [simp]: assumes - "small = (Reverse2 current aux big new count)" + "small = (Small2 current aux big new count)" "invar small" shows "list (step small) = list small" proof - have size_not_empty: "(0 < size big) = (\ is_empty big)" by (simp add: Stack_Proof.size_not_empty) have "\ is_empty big \ rev (Stack_Aux.list (Stack.pop big)) @ [Stack.first big] = rev (Stack_Aux.list big)" by(induction big rule: Stack.pop.induct) auto with assms show ?thesis using Stack_Proof.size_pop[of big] size_not_empty by(auto simp: Stack_Proof.list_empty split: current.splits) qed -lemma invar_step: "invar (small :: 'a state) \ invar (step small)" -proof(induction small rule: step_state.induct) +lemma invar_step: "invar (small :: 'a small_state) \ invar (step small)" +proof(induction small rule: step_small_state.induct) case (1 state) then show ?case by(auto simp: invar_step) next case (2 current small aux) then show ?case proof(cases "is_empty small") case True with 2 show ?thesis by auto next case False with 2 have "rev (Stack_Aux.list small) @ aux = rev (Stack_Aux.list (Stack.pop small)) @ Stack.first small # aux" by(auto simp: rev_app_single Stack_Proof.list_not_empty) with 2 show ?thesis by(auto split: current.splits) qed next case (3 current auxS big newS count) then show ?case proof(cases "is_empty big") case True then have big_size [simp]: "size big = 0" by (simp add: Stack_Proof.size_empty) with True 3 show ?thesis proof(cases current) case (Current extra added old remained) with 3 True show ?thesis proof(cases "remained \ count") case True with 3 Current show ?thesis using Stack_Proof.size_empty[of big] by auto next case False with True 3 Current show ?thesis by(auto) qed qed next case False with 3 show ?thesis using Stack_Proof.size_pop[of big] by(auto simp: Stack_Proof.size_not_empty split: current.splits) qed qed lemma invar_push: "invar small \ invar (push x small)" by(induction x small rule: push.induct)(auto simp: invar_push split: current.splits) lemma invar_pop: "\ 0 < size small; invar small; pop small = (x, small') \ \ invar small'" proof(induction small arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: invar_pop split: prod.splits) next case (2 current small auxS) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case by(cases "size small < size old") (auto simp: rev_take Suc_diff_le drop_Suc tl_drop) next case 2 then show ?case by auto qed next case (3 current auxS big newS count) then show ?case by (induction current rule: Current.pop.induct) (auto simp: rev_take Suc_diff_le drop_Suc tl_drop) qed -lemma push_list_common [simp]: "small = Common common \ list (push x small) = x # list small" +lemma push_list_common [simp]: "small = Small3 common \ list (push x small) = x # list small" by auto lemma push_list_current [simp]: "list_current (push x small) = x # list_current small" by(induction x small rule: push.induct) auto lemma pop_list_current [simp]: "\invar small; 0 < size small; Small.pop small = (x, small')\ \ x # list_current small' = list_current small" proof(induction small arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: pop_list_current split: prod.splits) next case (2 current small auxS) then have "invar current" by(auto split: current.splits) with 2 show ?case by auto next case (3 current auxS big newS count) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "\is_empty old" by(auto simp: Stack_Proof.size_not_empty) with 1 show ?case by(auto simp: rev_take drop_Suc drop_tl) next case 2 then show ?case by auto qed qed lemma list_current_size [simp]: "\0 < size small; list_current small = []; invar small\ \ False" proof(induction small) - case (Reverse1 current) + case (Small1 current) then have "invar current" by(auto split: current.splits) - with Reverse1 show ?case + with Small1 show ?case using Current_Proof.list_size by auto next - case Reverse2 + case Small2 then show ?case by(auto split: current.splits) next - case Common + case Small3 then show ?case using list_current_size by auto qed -lemma list_Reverse2 [simp]: "\ - 0 < size (Reverse2 current auxS big newS count); - invar (Reverse2 current auxS big newS count) +lemma list_Small2 [simp]: "\ + 0 < size (Small2 current auxS big newS count); + invar (Small2 current auxS big newS count) \ \ - fst (Current.pop current) # list (Reverse2 (drop_first current) auxS big newS count) = - list (Reverse2 current auxS big newS count)" + fst (Current.pop current) # list (Small2 (drop_first current) auxS big newS count) = + list (Small2 current auxS big newS count)" by(induction current rule: Current.pop.induct) (auto simp: first_hd rev_take Suc_diff_le) end \ No newline at end of file diff --git a/thys/Real_Time_Deque/States.thy b/thys/Real_Time_Deque/States.thy --- a/thys/Real_Time_Deque/States.thy +++ b/thys/Real_Time_Deque/States.thy @@ -1,22 +1,22 @@ section \Combining Big and Small\ theory States imports Big Small begin datatype direction = Left | Right -datatype 'a states = States direction "'a Big.state" "'a Small.state" +datatype 'a states = States direction "'a big_state" "'a small_state" instantiation states::(type) step begin fun step_states :: "'a states \ 'a states" where - "step (States dir (Reverse currentB big auxB 0) (Reverse1 currentS _ auxS)) = - States dir (step (Reverse currentB big auxB 0)) (Reverse2 currentS auxS big [] 0)" + "step (States dir (Big1 currentB big auxB 0) (Small1 currentS _ auxS)) = + States dir (step (Big1 currentB big auxB 0)) (Small2 currentS auxS big [] 0)" | "step (States dir left right) = States dir (step left) (step right)" instance.. end end diff --git a/thys/Real_Time_Deque/States_Aux.thy b/thys/Real_Time_Deque/States_Aux.thy --- a/thys/Real_Time_Deque/States_Aux.thy +++ b/thys/Real_Time_Deque/States_Aux.thy @@ -1,89 +1,87 @@ theory States_Aux imports States Big_Aux Small_Aux begin instantiation states::(type) remaining_steps begin fun remaining_steps_states :: "'a states \ nat" where "remaining_steps (States _ big small) = max (remaining_steps big) (case small of - Small.Common common \ remaining_steps common - | Reverse2 (Current _ _ _ remaining) _ big _ count \ - (remaining - (count + size big)) + size big + 1 - | Reverse1 (Current _ _ _ remaining) _ _ \ - case big of - Reverse currentB big auxB count \ size big + (remaining + count - size big) + 2 + Small3 common \ remaining_steps common + | Small2 (Current _ _ _ remaining) _ big _ count \ remaining - count + 1 + | Small1 (Current _ _ _ remaining) _ _ \ + case big of Big1 currentB big auxB count \ remaining + count + 2 )" instance.. end fun lists :: "'a states \ 'a list * 'a list" where - "lists (States _ (Reverse currentB big auxB count) (Reverse1 currentS small auxS)) = ( - Big_Aux.list (Reverse currentB big auxB count), - Small_Aux.list (Reverse2 currentS (take_rev count (Stack_Aux.list small) @ auxS) ((Stack.pop ^^ count) big) [] 0) + "lists (States _ (Big1 currentB big auxB count) (Small1 currentS small auxS)) = ( + Big_Aux.list (Big1 currentB big auxB count), + Small_Aux.list (Small2 currentS (take_rev count (Stack_Aux.list small) @ auxS) ((Stack.pop ^^ count) big) [] 0) )" | "lists (States _ big small) = (Big_Aux.list big, Small_Aux.list small)" fun list_small_first :: "'a states \ 'a list" where "list_small_first states = (let (big, small) = lists states in small @ (rev big))" fun list_big_first :: "'a states \ 'a list" where "list_big_first states = (let (big, small) = lists states in big @ (rev small))" fun lists_current :: "'a states \ 'a list * 'a list" where "lists_current (States _ big small) = (Big_Aux.list_current big, Small_Aux.list_current small)" fun list_current_small_first :: "'a states \ 'a list" where "list_current_small_first states = (let (big, small) = lists_current states in small @ (rev big))" fun list_current_big_first :: "'a states \ 'a list" where "list_current_big_first states = (let (big, small) = lists_current states in big @ (rev small))" fun listL :: "'a states \ 'a list" where "listL (States Left big small) = list_small_first (States Left big small)" | "listL (States Right big small) = list_big_first (States Right big small)" instantiation states::(type) invar begin fun invar_states :: "'a states \ bool" where "invar (States dir big small) \ ( invar big \ invar small \ list_small_first (States dir big small) = list_current_small_first (States dir big small) \ (case (big, small) of - (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \ + (Big1 _ big _ count, Small1 (Current _ _ old remained) small _) \ size big - count = remained - size old \ count \ size small - | (_, Reverse1 _ _ _) \ False - | (Reverse _ _ _ _, _) \ False + | (_, Small1 _ _ _) \ False + | (Big1 _ _ _ _, _) \ False | _ \ True ))" instance.. end fun size_ok' :: "'a states \ nat \ bool" where "size_ok' (States _ big small) steps \ size_new small + steps + 2 \ 3 * size_new big \ size_new big + steps + 2 \ 3 * size_new small \ steps + 1 \ 4 * size small \ steps + 1 \ 4 * size big " abbreviation size_ok :: "'a states \ bool" where "size_ok states \ size_ok' states (remaining_steps states)" abbreviation size_small where "size_small states \ case states of States _ _ small \ size small" abbreviation size_new_small where "size_new_small states \ case states of States _ _ small \ size_new small" abbreviation size_big where "size_big states \ case states of States _ big _ \ size big" abbreviation size_new_big where "size_new_big states \ case states of States _ big _ \ size_new big" end diff --git a/thys/Real_Time_Deque/States_Proof.thy b/thys/Real_Time_Deque/States_Proof.thy --- a/thys/Real_Time_Deque/States_Proof.thy +++ b/thys/Real_Time_Deque/States_Proof.thy @@ -1,1202 +1,1203 @@ section "Big + Small Proofs" theory States_Proof imports States_Aux Big_Proof Small_Proof begin -lemmas state_splits = idle.splits Common.state.splits Small.state.splits Big.state.splits +lemmas state_splits = idle.splits common_state.splits small_state.splits big_state.splits lemmas invar_steps = Big_Proof.invar_step Common_Proof.invar_step Small_Proof.invar_step lemma invar_list_big_first: "invar states \ list_big_first states = list_current_big_first states" using app_rev by(cases states)(auto split: prod.splits) lemma step_lists [simp]: "invar states \ lists (step states) = lists states" proof(induction states rule: lists.induct) case (1 dir currentB big auxB count currentS small auxS) then show ?case proof(induction - "(States dir (Reverse currentB big auxB count) (Reverse1 currentS small auxS))" + "(States dir (Big1 currentB big auxB count) (Small1 currentS small auxS))" rule: step_states.induct) case 1 then show ?case by(cases currentB) auto next case ("2_1" count') then have "0 < size big" by(cases currentB) auto then have big_not_empty: "Stack_Aux.list big \ []" by (simp add: Stack_Proof.size_not_empty Stack_Proof.list_empty) with "2_1" show ?case using take_rev_step[of "Stack_Aux.list big" count' auxB] Stack_Proof.list_empty[symmetric, of small] apply (cases currentB) by(auto simp: first_hd funpow_swap1 take_rev_step simp del: take_rev_def) qed next case ("2_1" dir common small) then show ?case - using Small_Proof.step_list_reverse2[of small] - by(auto split: Small.state.splits) + using step_list_Small2[of small] + by(auto split: small_state.splits) next case ("2_2" dir big current auxS big newS count) then show ?case - using Small_Proof.step_list_reverse2[of "Reverse2 current auxS big newS count"] + using step_list_Small2[of "Small2 current auxS big newS count"] by auto next case ("2_3" dir big common) then show ?case by auto qed lemma step_lists_current [simp]: "invar states \ lists_current (step states) = lists_current states" by(induction states rule: step_states.induct)(auto split: current.splits) lemma push_big: "lists (States dir big small) = (big', small') \ lists (States dir (Big.push x big) small) = (x # big', small')" proof(induction "States dir (Big.push x big) small" rule: lists.induct) case 1 then show ?case proof(induction x big rule: Big.push.induct) case 1 then show ?case by auto next case (2 x current big aux count) then show ?case by(cases current) auto qed next case "2_1" then show ?case by(cases big) auto qed auto lemma push_small_lists: " invar (States dir big small) \ lists (States dir big (Small.push x small)) = (big', x # small') \ lists (States dir big small) = (big', small')" apply(induction "States dir big (Small.push x small)" rule: lists.induct) - by (auto split: current.splits Small.state.splits) + by (auto split: current.splits small_state.splits) lemma list_small_big: " list_small_first (States dir big small) = list_current_small_first (States dir big small) \ list_big_first (States dir big small) = list_current_big_first (States dir big small)" using app_rev by(auto split: prod.splits) lemma list_big_first_pop_big [simp]: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ x # list_big_first (States dir big' small) = list_big_first (States dir big small)" by(induction "States dir big small" rule: lists.induct)(auto split: prod.splits) lemma list_current_big_first_pop_big [simp]: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ x # list_current_big_first (States dir big' small) = list_current_big_first (States dir big small)" by auto lemma lists_big_first_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ list_big_first (States dir big' small) = list_current_big_first (States dir big' small)" by (metis invar_list_big_first list_big_first_pop_big list_current_big_first_pop_big list.sel(3)) lemma lists_small_first_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ list_small_first (States dir big' small) = list_current_small_first (States dir big' small)" by (meson lists_big_first_pop_big list_small_big) lemma list_small_first_pop_small [simp]: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small')\ \ x # list_small_first (States dir big small') = list_small_first (States dir big small)" proof(induction "States dir big small" rule: lists.induct) case (1 currentB big auxB count currentS small auxS) then show ?case by(cases currentS)(auto simp: Cons_eq_appendI) next case ("2_1" common) then show ?case proof(induction small rule: Small.pop.induct) case (1 common) then show ?case by(cases "Common.pop common")(auto simp: Cons_eq_appendI) next case 2 then show ?case by auto next case 3 then show ?case by(cases "Common.pop common")(auto simp: Cons_eq_appendI) qed next case ("2_2" current) then show ?case by(induction current rule: Current.pop.induct) (auto simp: first_hd rev_take Suc_diff_le) next case ("2_3" common) then show ?case by(cases "Common.pop common")(auto simp: Cons_eq_appendI) qed lemma list_current_small_first_pop_small [simp]: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small')\ \ x # list_current_small_first (States dir big small') = list_current_small_first (States dir big small)" by auto lemma lists_small_first_pop_small: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small')\ \ list_small_first (States dir big small') = list_current_small_first (States dir big small')" by (metis (no_types, opaque_lifting) invar_states.simps list.sel(3) list_current_small_first_pop_small list_small_first_pop_small) lemma invars_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ invar big' \ invar small" by(auto simp: Big_Proof.invar_pop) lemma invar_pop_big_aux: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ (case (big', small) of - (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \ + (Big1 _ big _ count, Small1 (Current _ _ old remained) small _) \ size big - count = remained - size old \ count \ size small - | (_, Reverse1 _ _ _) \ False - | (Reverse _ _ _ _, _) \ False + | (_, Small1 _ _ _) \ False + | (Big1 _ _ _ _, _) \ False | _ \ True )" - by(auto split: Big.state.splits Small.state.splits prod.splits) + by(auto split: big_state.splits small_state.splits prod.splits) lemma invar_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, big')\ \ invar (States dir big' small)" using invars_pop_big[of dir big small x big'] lists_small_first_pop_big[of dir big small x big'] invar_pop_big_aux[of dir big small x big'] by auto lemma invars_pop_small: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small')\ \ invar big \ invar small'" by(auto simp: Small_Proof.invar_pop) lemma invar_pop_small_aux: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small')\ \ (case (big, small') of - (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \ + (Big1 _ big _ count, Small1 (Current _ _ old remained) small _) \ size big - count = remained - size old \ count \ size small - | (_, Reverse1 _ _ _) \ False - | (Reverse _ _ _ _, _) \ False + | (_, Small1 _ _ _) \ False + | (Big1 _ _ _ _, _) \ False | _ \ True )" proof(induction small rule: Small.pop.induct) case 1 then show ?case - by(auto split: Big.state.splits Small.state.splits prod.splits) + by(auto split: big_state.splits small_state.splits prod.splits) next case (2 current) then show ?case proof(induction current rule: Current.pop.induct) case 1 then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) next case 2 then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) qed next case 3 then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) qed lemma invar_pop_small: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, small') \ \ invar (States dir big small')" using invars_pop_small[of dir big small x small'] lists_small_first_pop_small[of dir big small x small'] invar_pop_small_aux[of dir big small x small'] by fastforce lemma invar_push_big: "invar (States dir big small) \ invar (States dir (Big.push x big) small)" proof(induction x big arbitrary: small rule: Big.push.induct) case 1 then show ?case by(auto simp: Common_Proof.invar_push) next case (2 x current big aux count) then show ?case - by(cases current)(auto split: prod.splits Small.state.splits) + by(cases current)(auto split: prod.splits small_state.splits) qed lemma invar_push_small: "invar (States dir big small) \ invar (States dir big (Small.push x small))" proof(induction x small arbitrary: big rule: Small.push.induct) case (1 x state) then show ?case - by(auto simp: Common_Proof.invar_push split: Big.state.splits) + by(auto simp: Common_Proof.invar_push split: big_state.splits) next case (2 x current small auxS) then show ?case - by(induction x current rule: Current.push.induct)(auto split: Big.state.splits) + by(induction x current rule: Current.push.induct)(auto split: big_state.splits) next case (3 x current auxS big newS count) then show ?case - by(induction x current rule: Current.push.induct)(auto split: Big.state.splits) + by(induction x current rule: Current.push.induct)(auto split: big_state.splits) qed lemma step_invars:"\invar states; step states = States dir big small\ \ invar big \ invar small" proof(induction states rule: step_states.induct) case (1 dir currentB big' auxB currentS small' auxS) - with Big_Proof.invar_step have "invar (Reverse currentB big' auxB 0)" + with Big_Proof.invar_step have "invar (Big1 currentB big' auxB 0)" by auto with 1 have invar_big: "invar big" - using Big_Proof.invar_step[of "Reverse currentB big' auxB 0"] + using Big_Proof.invar_step[of "Big1 currentB big' auxB 0"] by auto from 1 have invar_small: "invar small" using Stack_Proof.list_empty_size[of small'] by(cases currentS) auto from invar_small invar_big show ?case by simp next case ("2_1" dir current big aux count small) then show ?case - using Big_Proof.invar_step[of "(Reverse current big aux (Suc count))"] + using Big_Proof.invar_step[of "Big1 current big aux (Suc count)"] Small_Proof.invar_step[of small] by simp next case "2_2" then show ?case by(auto simp: Common_Proof.invar_step Small_Proof.invar_step) next case ("2_3" dir big current auxS big' newS count) then show ?case using Big_Proof.invar_step[of big] - Small_Proof.invar_step[of "Reverse2 current auxS big' newS count"] + Small_Proof.invar_step[of "Small2 current auxS big' newS count"] by auto next case "2_4" then show ?case by(auto simp: Common_Proof.invar_step Big_Proof.invar_step) qed lemma step_lists_small_first: "invar states \ list_small_first (step states) = list_current_small_first (step states)" using step_lists_current step_lists invar_states.elims(2) by fastforce lemma invar_step_aux: "invar states \(case step states of - (States _ (Reverse _ big _ count) (Reverse1 (Current _ _ old remained) small _)) \ + (States _ (Big1 _ big _ count) (Small1 (Current _ _ old remained) small _)) \ size big - count = remained - size old \ count \ size small - | (States _ _ (Reverse1 _ _ _)) \ False - | (States _ (Reverse _ _ _ _) _) \ False + | (States _ _ (Small1 _ _ _)) \ False + | (States _ (Big1 _ _ _ _) _) \ False | _ \ True )" proof(induction states rule: step_states.induct) case ("2_1" dir current big aux count small) then show ?case proof(cases small) - case (Reverse1 current small auxS) + case (Small1 current small auxS) with "2_1" show ?thesis using Stack_Proof.size_empty[symmetric, of small] by(auto split: current.splits) qed auto -qed (auto split: Big.state.splits Small.state.splits) +qed (auto split: big_state.splits small_state.splits) lemma invar_step: "invar (states :: 'a states) \ invar (step states)" using invar_step_aux[of states] step_lists_small_first[of states] by(cases "step states")(auto simp: step_invars) lemma step_consistent [simp]: "\\states. invar (states :: 'a states) \ P (step states) = P states; invar states\ \ P states = P ((step ^^n) states)" by(induction n arbitrary: states) (auto simp: States_Proof.invar_step funpow_swap1) lemma step_consistent_2: "\\states. \invar (states :: 'a states); P states\ \ P (step states); invar states; P states\ \ P ((step ^^n) states)" by(induction n arbitrary: states) (auto simp: States_Proof.invar_step funpow_swap1) lemma size_ok'_Suc: "size_ok' states (Suc steps) \ size_ok' states steps" by(induction states steps rule: size_ok'.induct) auto lemma size_ok'_decline: "size_ok' states x \ x \ y \ size_ok' states y" by(induction states x rule: size_ok'.induct) auto lemma remaining_steps_0 [simp]: "\invar (states :: 'a states); remaining_steps states = 0\ \ remaining_steps (step states) = 0" - by(induction states rule: step_states.induct) (auto split: current.splits Small.state.splits) + by(induction states rule: step_states.induct) + (auto split: current.splits small_state.splits) lemma remaining_steps_0': "\invar (states :: 'a states); remaining_steps states = 0\ \ remaining_steps ((step ^^ n) states) = 0" by(induction n arbitrary: states)(auto simp: invar_step funpow_swap1) lemma remaining_steps_decline_Suc: "\invar (states :: 'a states); 0 < remaining_steps states\ \ Suc (remaining_steps (step states)) = remaining_steps states" proof(induction states rule: step_states.induct) case 1 then show ?case - by(auto simp: max_def split: Big.state.splits Small.state.splits current.splits) + by(auto simp: max_def split: big_state.splits small_state.splits current.splits) next case ("2_1" _ _ _ _ _ small) then show ?case by(cases small)(auto split: current.splits) next case ("2_2" dir big small) then show ?case proof(cases small) - case (Reverse2 current auxS big newS count) + case (Small2 current auxS big newS count) with "2_2" show ?thesis using Stack_Proof.size_empty_2[of big] by(cases current) auto qed auto next case ("2_3" dir big current auxS big' newS count) then show ?case proof(induction big) - case Reverse + case Big1 then show ?case by auto next - case Common + case Big2 then show ?case using Stack_Proof.size_empty_2[of big'] by(cases current) auto qed next case ("2_4" _ big) then show ?case by(cases big) auto qed lemma remaining_steps_decline_sub [simp]: "invar (states :: 'a states) \ remaining_steps (step states) = remaining_steps states - 1" using Suc_sub[of "remaining_steps (step states)" "remaining_steps states"] by(cases "0 < remaining_steps states") (auto simp: remaining_steps_decline_Suc) lemma remaining_steps_decline: "invar (states :: 'a states) \ remaining_steps (step states) \ remaining_steps states" using remaining_steps_decline_sub[of states] by auto lemma remaining_steps_decline_n_steps [simp]: "\invar (states :: 'a states); remaining_steps states \ n\ \ remaining_steps ((step ^^ n) states) = 0" by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step) lemma remaining_steps_n_steps_plus [simp]: "\n \ remaining_steps states; invar (states :: 'a states)\ \ remaining_steps ((step ^^ n) states) + n = remaining_steps states" by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step) lemma remaining_steps_n_steps_sub [simp]: "invar (states :: 'a states) \ remaining_steps ((step ^^ n) states) = remaining_steps states - n" by(induction n arbitrary: states)(auto simp: funpow_swap1 invar_step) lemma step_size_new_small [simp]: "\invar (States dir big small); step (States dir big small) = States dir' big' small'\ \ size_new small' = size_new small" proof(induction "States dir big small" rule: step_states.induct) case 1 then show ?case by auto next case "2_1" then show ?case - by(auto split: Small.state.splits) + by(auto split: small_state.splits) next case "2_2" then show ?case - by(auto split: Small.state.splits current.splits) + by(auto split: small_state.splits current.splits) next case "2_3" then show ?case by(auto split: current.splits) next case "2_4" then show ?case by auto qed lemma step_size_new_small_2 [simp]: "invar states \ size_new_small (step states) = size_new_small states" by(cases states; cases "step states") auto lemma step_size_new_big [simp]: "\invar (States dir big small); step (States dir big small) = States dir' big' small'\ \ size_new big' = size_new big" proof(induction "States dir big small" rule: step_states.induct) case 1 then show ?case by(auto split: current.splits) next case "2_1" then show ?case by auto next case "2_2" then show ?case by auto next case "2_3" then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) next case "2_4" then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) qed lemma step_size_new_big_2 [simp]: "invar states \ size_new_big (step states) = size_new_big states" by(cases states; cases "step states") auto lemma step_size_small [simp]: "\invar (States dir big small); step (States dir big small) = States dir' big' small'\ \ size small' = size small" proof(induction "States dir big small" rule: step_states.induct) case "2_3" then show ?case by(auto split: current.splits) qed auto lemma step_size_small_2 [simp]: "invar states \ size_small (step states) = size_small states" by(cases states; cases "step states") auto lemma step_size_big [simp]: "\invar (States dir big small); step (States dir big small) = States dir' big' small'\ \ size big' = size big" proof(induction "States dir big small" rule: step_states.induct) case 1 then show ?case by(auto split: current.splits) next case "2_1" then show ?case - by(auto split: Small.state.splits current.splits) + by(auto split: small_state.splits current.splits) next case "2_2" then show ?case - by(auto split: Small.state.splits current.splits) + by(auto split: small_state.splits current.splits) next case "2_3" then show ?case - by(auto split: current.splits Big.state.splits) + by(auto split: current.splits big_state.splits) next case "2_4" then show ?case - by(auto split: Big.state.splits) + by(auto split: big_state.splits) qed lemma step_size_big_2 [simp]: "invar states \ size_big (step states) = size_big states" by(cases states; cases "step states") auto lemma step_size_ok_1: "\ invar (States dir big small); step (States dir big small) = States dir' big' small'; size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" using step_size_new_small step_size_new_big remaining_steps_decline by (smt (verit, ccfv_SIG) add.commute le_trans nat_add_left_cancel_le) lemma step_size_ok_2: "\ invar (States dir big small); step (States dir big small) = States dir' big' small'; size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" using remaining_steps_decline step_size_new_small step_size_new_big by (smt (verit, best) add_le_mono le_refl le_trans) lemma step_size_ok_3: "\ invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" using remaining_steps_decline step_size_small by (metis Suc_eq_plus1 Suc_le_mono le_trans) lemma step_size_ok_4: "\ invar (States dir big small); step (States dir big small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" using remaining_steps_decline step_size_big by (metis (no_types, lifting) add_mono_thms_linordered_semiring(3) order.trans) lemma step_size_ok: "\invar states; size_ok states\ \ size_ok (step states)" using step_size_ok_1 step_size_ok_2 step_size_ok_3 step_size_ok_4 by (smt (verit) invar_states.elims(1) size_ok'.elims(3) size_ok'.simps) lemma step_n_size_ok: "\invar states; size_ok states\ \ size_ok ((step ^^ n) states)" using step_consistent_2[of size_ok states n] step_size_ok by blast lemma step_push_size_small [simp]: "\ invar (States dir big small); step (States dir big (Small.push x small)) = States dir' big' small' \ \ size small' = Suc (size small)" using invar_push_small[of dir big small x] step_size_small[of dir big "Small.push x small" dir' big' small'] size_push[of small x] by simp lemma step_push_size_new_small [simp]: "\ invar (States dir big small); step (States dir big (Small.push x small)) = States dir' big' small' \ \ size_new small' = Suc (size_new small)" using invar_push_small[of dir big small x] step_size_new_small[of dir big "Small.push x small" dir' big' small'] size_new_push[of small x] by simp lemma step_push_size_big [simp]: "\ invar (States dir big small); step (States dir (Big.push x big) small) = States dir' big' small' \ \ size big' = Suc (size big)" using invar_push_big[of dir big small x] Big_Proof.size_push[of big] step_size_big[of dir "Big.push x big" small dir' big' small'] by simp lemma step_push_size_new_big [simp]: "\ invar (States dir big small); step (States dir (Big.push x big) small) = States dir' big' small' \ \ size_new big' = Suc (size_new big)" using invar_push_big[of dir big small x] step_size_new_big[of dir "Big.push x big" small dir' big' small'] Big_Proof.size_new_push[of big x] by simp lemma step_pop_size_big [simp]: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); step (States dir bigP small) = States dir' big' small' \ \ Suc (size big') = size big" using invar_pop_big[of dir big small x bigP] step_size_big[of dir bigP small dir' big' small'] Big_Proof.size_pop[of big x bigP] by simp lemma step_pop_size_new_big [simp]: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); step (States dir bigP small) = States dir' big' small' \ \ Suc (size_new big') = size_new big" using invar_pop_big[of dir big small x bigP] Big_Proof.size_size_new[of big] step_size_new_big[of dir bigP small dir' big' small'] Big_Proof.size_new_pop[of big x bigP] by simp lemma step_n_size_small [simp]: "\ invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small' \ \ size small' = size small" using step_consistent[of size_small "States dir big small" n] by simp lemma step_n_size_big [simp]: "\invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\ \ size big' = size big" using step_consistent[of size_big "States dir big small" n] by simp lemma step_n_size_new_small [simp]: "\invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\ \ size_new small' = size_new small" using step_consistent[of size_new_small "States dir big small" n] by simp lemma step_n_size_new_big [simp]: "\invar (States dir big small); (step ^^ n) (States dir big small) = States dir' big' small'\ \ size_new big' = size_new big" using step_consistent[of size_new_big "States dir big small" n] by simp lemma step_n_push_size_small [simp]: "\ invar (States dir big small); (step ^^ n) (States dir big (Small.push x small)) = States dir' big' small' \ \ size small' = Suc (size small)" using step_n_size_small invar_push_small Small_Proof.size_push by (metis invar_states.simps) lemma step_n_push_size_new_small [simp]: "\ invar (States dir big small); (step ^^ n) (States dir big (Small.push x small)) = States dir' big' small' \ \ size_new small' = Suc (size_new small)" by (metis Small_Proof.size_new_push invar_states.simps invar_push_small step_n_size_new_small) lemma step_n_push_size_big [simp]: "\ invar (States dir big small); (step ^^ n) (States dir (Big.push x big) small) = States dir' big' small' \ \ size big' = Suc (size big)" by (metis Big_Proof.size_push invar_states.simps invar_push_big step_n_size_big) lemma step_n_push_size_new_big [simp]: "\ invar (States dir big small); (step ^^ n) (States dir (Big.push x big) small) = States dir' big' small' \ \ size_new big' = Suc (size_new big)" by (metis Big_Proof.size_new_push invar_states.simps invar_push_big step_n_size_new_big) lemma step_n_pop_size_small [simp]: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); (step ^^ n) (States dir big smallP) = States dir' big' small' \ \ Suc (size small') = size small" using invar_pop_small size_pop step_n_size_small by (metis (no_types, opaque_lifting) invar_states.simps) lemma step_n_pop_size_new_small [simp]: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); (step ^^ n) (States dir big smallP) = States dir' big' small' \ \ Suc (size_new small') = size_new small" using invar_pop_small size_new_pop step_n_size_new_small size_size_new by (metis (no_types, lifting) invar_states.simps) lemma step_n_pop_size_big [simp]: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); (step ^^ n) (States dir bigP small) = States dir' big' small' \ \ Suc (size big') = size big" using invar_pop_big Big_Proof.size_pop step_n_size_big by fastforce lemma step_n_pop_size_new_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); (step ^^ n) (States dir bigP small) = States dir' big' small' \ \ Suc (size_new big') = size_new big" using invar_pop_big Big_Proof.size_new_pop step_n_size_new_big Big_Proof.size_size_new by (metis (no_types, lifting) invar_states.simps) lemma remaining_steps_push_small [simp]: "invar (States dir big small) \ remaining_steps (States dir big small) = remaining_steps (States dir big (Small.push x small))" by(induction x small rule: Small.push.induct)(auto split: current.splits) lemma remaining_steps_pop_small: "\invar (States dir big small); 0 < size small; Small.pop small = (x, smallP)\ \ remaining_steps (States dir big smallP) \ remaining_steps (States dir big small)" proof(induction small rule: Small.pop.induct) case 1 then show ?case by(auto simp: Common_Proof.remaining_steps_pop max.coboundedI2 split: prod.splits) next case (2 current small auxS) then show ?case - by(induction current rule: Current.pop.induct)(auto split: Big.state.splits) + by(induction current rule: Current.pop.induct)(auto split: big_state.splits) next case (3 current auxS big newS count) then show ?case by(induction current rule: Current.pop.induct) auto qed lemma remaining_steps_pop_big: "\invar (States dir big small); 0 < size big; Big.pop big = (x, bigP)\ \ remaining_steps (States dir bigP small) \ remaining_steps (States dir big small)" proof(induction big rule: Big.pop.induct) case (1 state) then show ?case proof(induction state rule: Common.pop.induct) case (1 current idle) then show ?case - by(cases idle)(auto split: Small.state.splits) + by(cases idle)(auto split: small_state.splits) next case (2 current aux new moved) then show ?case - by(induction current rule: Current.pop.induct)(auto split: Small.state.splits) + by(induction current rule: Current.pop.induct)(auto split: small_state.splits) qed next case (2 current big aux count) then show ?case proof(induction current rule: Current.pop.induct) case 1 then show ?case - by(auto split: Small.state.splits current.splits) + by(auto split: small_state.splits current.splits) next case 2 then show ?case - by(auto split: Small.state.splits current.splits) + by(auto split: small_state.splits current.splits) qed qed lemma remaining_steps_push_big [simp]: "invar (States dir big small) \ remaining_steps (States dir (Big.push x big) small) = remaining_steps (States dir big small)" - by(induction x big rule: Big.push.induct)(auto split: Small.state.splits current.splits) + by(induction x big rule: Big.push.induct)(auto split: small_state.splits current.splits) lemma step_4_remaining_steps_push_big [simp]: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'\ \ remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big ) lemma step_4_remaining_steps_push_small [simp]: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small' \ \ remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4" by (metis invar_push_small remaining_steps_n_steps_sub remaining_steps_push_small) lemma step_4_remaining_steps_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); (step^^4) (States dir bigP small) = States dir' big' small' \ \ remaining_steps (States dir' big' small') \ remaining_steps (States dir big small) - 4" by (metis add_le_imp_le_diff invar_pop_big remaining_steps_pop_big remaining_steps_n_steps_plus) lemma step_4_remaining_steps_pop_small: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small' \ \ remaining_steps (States dir' big' small') \ remaining_steps (States dir big small) - 4" by (metis add_le_imp_le_diff invar_pop_small remaining_steps_n_steps_plus remaining_steps_pop_small) lemma step_4_pop_small_size_ok_1: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) add.left_commute add.right_neutral add_le_cancel_left distrib_left_numeral dual_order.trans invar_pop_small le_add_diff_inverse2 mult.right_neutral plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_small) lemma step_4_pop_big_size_ok_1: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); (step^^4) (States dir bigP small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) add_leE add_le_cancel_right invar_pop_big order_trans remaining_steps_pop_big step_n_size_small remaining_steps_n_steps_plus) lemma step_4_pop_small_size_ok_2: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (smt (z3) add.commute add_leE invar_pop_small le_add_diff_inverse2 nat_add_left_cancel_le remaining_steps_n_steps_sub step_n_size_big remaining_steps_pop_small) lemma step_4_pop_big_size_ok_2: assumes "invar (States dir big small)" "0 < size big" "Big.pop big = (x, bigP)" "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = States dir' big' small'" "remaining_steps (States dir big small) + 1 \ 4 * size big" shows "remaining_steps (States dir' big' small') + 1 \ 4 * size big'" proof - from assms have "remaining_steps (States dir bigP small) + 1 \ 4 * size big" by (meson add_le_cancel_right order.trans remaining_steps_pop_big) with assms show ?thesis by (smt (z3) Suc_diff_le Suc_eq_plus1 add_mult_distrib2 diff_diff_add diff_is_0_eq invar_pop_big mult_numeral_1_right numerals(1) plus_1_eq_Suc remaining_steps_n_steps_sub step_n_pop_size_big) qed lemma step_4_pop_small_size_ok_3: assumes "invar (States dir big small)" "0 < size small" "Small.pop small = (x, smallP)" "remaining_steps (States dir big smallP) \ 4" "((step ^^ 4) (States dir big smallP)) = States dir' big' small'" "size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big" shows "size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" by (smt (verit, best) add_leD2 add_mono_thms_linordered_semiring(1) add_mono_thms_linordered_semiring(3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) invar_pop_small le_add2 le_add_diff_inverse order_trans plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_new_small step_n_size_new_big) lemma step_4_pop_big_size_ok_3_aux: "\ 0 < size big; 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new big - 1)" by linarith lemma step_4_pop_big_size_ok_3: assumes "invar (States dir big small)" "0 < size big" "Big.pop big = (x, bigP) " "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')" "size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big" shows "size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" proof- from assms have "size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new big - 1)" by (meson dual_order.trans remaining_steps_pop_big step_4_pop_big_size_ok_3_aux) then have "size_new small + remaining_steps (States dir' big' small') + 2 \ 3 * (size_new big - 1)" by (smt (verit, ccfv_SIG) add_le_mono assms(1) assms(2) assms(3) assms(4) assms(5) dual_order.trans le_antisym less_or_eq_imp_le nat_less_le step_4_remaining_steps_pop_big) with assms show ?thesis by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big) qed lemma step_4_pop_small_size_ok_4_aux: "\ 0 < size small; 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new small - 1)" by linarith lemma step_4_pop_small_size_ok_4: assumes "invar (States dir big small)" "0 < size small" "Small.pop small = (x, smallP)" "remaining_steps (States dir big smallP) \ 4" "((step ^^ 4) (States dir big smallP)) = (States dir' big' small')" "size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small" shows "size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" proof- from assms step_4_pop_small_size_ok_4_aux have "size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new small - 1)" by (smt (verit, best) add_leE le_add_diff_inverse remaining_steps_pop_small) with assms have "size_new big + remaining_steps (States dir' big' small') + 2 \ 3 * (size_new small - 1)" by (smt (verit, best) add_le_cancel_left add_mono_thms_linordered_semiring(3) diff_le_mono invar_pop_small order_trans remaining_steps_n_steps_sub remaining_steps_pop_small) with assms show ?thesis by (metis diff_Suc_1 invar_pop_small step_n_size_new_big step_n_pop_size_new_small) qed lemma step_4_pop_big_size_ok_4_aux: "\ 0 < size big; 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big - 1 + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" by linarith lemma step_4_pop_big_size_ok_4: assumes "invar (States dir big small)" "0 < size big " "Big.pop big = (x, bigP)" "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')" "size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small" shows "size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" proof - from assms step_4_pop_big_size_ok_4_aux have "(size_new big - 1) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" by linarith with assms have "(size_new big - 1) + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small" by (meson add_le_mono dual_order.eq_iff order_trans step_4_remaining_steps_pop_big) with assms show ?thesis by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big) qed lemma step_4_push_small_size_ok_1: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (z3) add.commute add_leD1 add_le_mono le_add1 le_add_diff_inverse2 mult_Suc_right nat_1_add_1 numeral_Bit0 step_n_push_size_small step_4_remaining_steps_push_small) lemma step_4_push_big_size_ok_1: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) Nat.le_diff_conv2 add_leD2 invar_push_big le_add1 le_add_diff_inverse2 remaining_steps_n_steps_sub remaining_steps_push_big step_n_size_small) lemma step_4_push_small_size_ok_2: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (metis (full_types) Suc_diff_le Suc_eq_plus1 invar_push_small less_Suc_eq_le less_imp_diff_less step_4_remaining_steps_push_small step_n_size_big) lemma step_4_push_big_size_ok_2: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (smt (verit, ccfv_SIG) add.commute add_diff_cancel_left' add_leD1 add_le_mono invar_push_big mult_Suc_right nat_le_iff_add one_le_numeral remaining_steps_n_steps_sub remaining_steps_push_big step_n_push_size_big) lemma step_4_push_small_size_ok_3_aux: "\ 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ Suc (size_new small) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new big" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_small_size_ok_3: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" using step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small by (metis invar_push_small step_4_push_small_size_ok_3_aux) lemma step_4_push_big_size_ok_3_aux: "\ 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * Suc (size_new big)" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_big_size_ok_3: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_3_aux step_n_push_size_new_big step_n_size_new_small) lemma step_4_push_small_size_ok_4_aux: "\ 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * Suc (size_new small)" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_small_size_ok_4: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" by (metis invar_push_small step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small step_4_push_small_size_ok_4_aux) lemma step_4_push_big_size_ok_4_aux: "\ 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ Suc (size_new big) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_big_size_ok_4: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_4_aux step_n_push_size_new_big step_n_size_new_small) lemma step_4_push_small_size_ok: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir big (Small.push x small)))" using step_4_push_small_size_ok_1 step_4_push_small_size_ok_2 step_4_push_small_size_ok_3 step_4_push_small_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma step_4_push_big_size_ok: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir (Big.push x big) small))" using step_4_push_big_size_ok_1 step_4_push_big_size_ok_2 step_4_push_big_size_ok_3 step_4_push_big_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma step_4_pop_small_size_ok: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir big smallP))" by (smt (verit) size_ok'.elims(3) size_ok'.simps step_4_pop_small_size_ok_1 step_4_pop_small_size_ok_2 step_4_pop_small_size_ok_3 step_4_pop_small_size_ok_4) lemma step_4_pop_big_size_ok: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir bigP small))" using step_4_pop_big_size_ok_1 step_4_pop_big_size_ok_2 step_4_pop_big_size_ok_3 step_4_pop_big_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma size_ok_size_small: "size_ok (States dir big small) \ 0 < size small" by auto lemma size_ok_size_big: "size_ok (States dir big small) \ 0 < size big" by auto lemma size_ok_size_new_small: "size_ok (States dir big small) \ 0 < size_new small" by auto lemma size_ok_size_new_big: "size_ok (States dir big small) \ 0 < size_new big" by auto lemma step_size_ok': "\invar states; size_ok' states n\ \ size_ok' (step states) n" by (smt (verit, ccfv_SIG) size_ok'.elims(2) size_ok'.elims(3) step_size_big step_size_new_big step_size_new_small step_size_small) lemma step_same: "step (States dir big small) = States dir' big' small' \ dir = dir'" by(induction "States dir big small" rule: step_states.induct) auto lemma step_n_same: "(step^^n) (States dir big small) = States dir' big' small' \ dir = dir'" proof(induction n arbitrary: big small big' small') case 0 then show ?case by simp next case (Suc n) obtain big'' small'' where "step (States dir big small) = States dir big'' small''" by (metis states.exhaust step_same) with Suc show ?case by(auto simp: funpow_swap1) qed lemma step_listL: "invar states \ listL (step states) = listL states" proof(induction states rule: listL.induct) case (1 big small) then have "list_small_first (States Left big small) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by auto then have "list_small_first (step (States Left big small)) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" using 1 step_lists by fastforce then have "listL (step (States Left big small)) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by (smt (verit, ccfv_SIG) "1" invar_states.elims(2) States_Proof.invar_step listL.simps(1) step_same) with 1 show ?case by auto next case (2 big small) then have a: "list_big_first (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 auto then have "list_big_first (step (States Right big small)) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using 2 step_lists by fastforce then have "listL (step (States Right big small)) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" by (metis(full_types) listL.cases listL.simps(2) step_same) with 2 show ?case using a by force qed lemma step_n_listL: "invar states \ listL ((step^^n) states) = listL states" using step_consistent[of listL states] step_listL by metis lemma listL_remaining_steps: assumes "listL states = []" "0 < remaining_steps states" "invar states" "size_ok states" shows "False" proof(cases states) case (States dir big small) with assms show ?thesis using Small_Proof.list_current_size size_ok_size_small by(cases dir; cases "lists (States dir big small)") auto qed lemma invar_step_n: "invar (states :: 'a states) \ invar ((step^^n) states)" by (simp add: invar_step step_consistent_2) lemma step_n_size_ok': "\invar states; size_ok' states x\ \ size_ok' ((step ^^ n) states) x" proof(induction n arbitrary: states x) case 0 then show ?case by auto next case Suc then show ?case using invar_step_n step_size_ok' by fastforce qed lemma size_ok_steps: "\ invar states; size_ok' states (remaining_steps states - n) \ \ size_ok ((step ^^ n) states)" by (simp add: step_n_size_ok') lemma remaining_steps_idle: "invar states \ remaining_steps states = 0 \ ( case states of - States _ (Big.Common (Common.Idle _ _)) (Small.Common (Common.Idle _ _)) \ True + States _ (Big2 (Common.Idle _ _)) (Small3 (Common.Idle _ _)) \ True | _ \ False) " by(cases states) - (auto split: Big.state.split Small.state.split Common.state.split current.splits) + (auto split: big_state.split small_state.split common_state.split current.splits) lemma remaining_steps_idle': "\invar (States dir big small); remaining_steps (States dir big small) = 0\ \ \big_current big_idle small_current small_idle. States dir big small = States dir - (Big.state.Common (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle))" + (Big2 (common_state.Idle big_current big_idle)) + (Small3 (common_state.Idle small_current small_idle))" using remaining_steps_idle[of "States dir big small"] - by(cases big; cases small) (auto split!: Common.state.splits) + by(cases big; cases small) (auto split!: common_state.splits) end