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,121 +1,44 @@ 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: \<^descr> \Reverse\: Using the \step\ function the originally contained elements, which will be kept in this end, are reversed. \<^descr> \Common\: Specified in theory \Common\. Is used to reverse the elements from the previous phase again to get them in the original order. \<^noindent> Each phase contains a \current\ state, which holds the original elements of the deque end. \ datatype (plugins del: size) 'a state = Reverse "'a current" "'a stack" "'a list" nat | Common "'a Common.state" text \\<^noindent> Functions: -\<^descr> \step\: Executes one step of the transformation -\<^descr> \size_new\: Returns the size that the deque end will have after the transformation 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> \list_current\: List abstraction of the elements currently in this deque end. -\ - -fun list :: "'a state \ 'a list" where - "list (Common common) = Common.list common" -| "list (Reverse (Current extra _ _ remained) big aux count) = ( - let reversed = reverseN count (Stack.list big) aux in - extra @ (reverseN remained reversed []) - )" - -fun list_current :: "'a state \ 'a list" where - "list_current (Common common) = Common.list_current common" -| "list_current (Reverse current _ _ _) = Current.list current" +\<^descr> \push\, \pop\: Add and remove elements using the \current\ state. +\<^descr> \step\: Executes one step of the transformation\ instantiation 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)" 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 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)" -instantiation state ::(type) is_empty -begin - -fun is_empty_state :: "'a state \ bool" where - "is_empty (Common state) = is_empty state" -| "is_empty (Reverse current _ _ count) = ( - case current of Current extra added old remained \ - is_empty current \ remained \ count -)" - -instance.. -end - -instantiation state ::(type) invar -begin - -fun invar_state :: "'a state \ bool" where - "invar (Common state) \ invar state" -| "invar (Reverse current big aux count) \ ( - case current of Current extra added old remained \ - invar current - \ List.length aux \ remained - count - - \ count \ size big - \ Stack.list old = rev (take (size old) ((rev (Stack.list big)) @ aux)) - \ take remained (Stack.list old) = rev (take remained (reverseN count (Stack.list big) aux)) -)" - -instance.. -end - -instantiation 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)" - -instance.. -end - -instantiation 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" - -instance.. -end - -instantiation 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" - -instance.. -end - end \ No newline at end of file diff --git a/thys/Real_Time_Deque/Big_Aux.thy b/thys/Real_Time_Deque/Big_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Big_Aux.thy @@ -0,0 +1,73 @@ +theory Big_Aux +imports Big Common_Aux +begin + +text \\<^noindent> Functions: + +\<^descr> \size_new\: Returns the size that the deque end will have after the transformation is finished. +\<^descr> \size\: 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> \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) = ( + let reversed = reverseN count (Stack_Aux.list big) aux in + extra @ (reverseN 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" + +instantiation state ::(type) invar +begin + +fun invar_state :: "'a state \ bool" where + "invar (Common state) \ invar state" +| "invar (Reverse current big aux count) \ ( + case current of Current extra added old remained \ + invar current + \ List.length aux \ remained - count + + \ count \ size big + \ Stack_Aux.list old = rev (take (size old) ((rev (Stack_Aux.list big)) @ aux)) + \ take remained (Stack_Aux.list old) = + rev (take remained (reverseN count (Stack_Aux.list big) aux)) +)" + +instance.. +end + +instantiation 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)" + +instance.. +end + +instantiation 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" + +instance.. +end + +instantiation 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" + +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,332 +1,320 @@ section "Big Proofs" theory Big_Proof -imports Big Common_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) 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) 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)" proof(induction current rule: Current.pop.induct) case (1 added old remained) - then have [simp]: "remained - Suc 0 < length (reverseN count (Stack.list big) aux)" + then have [simp]: "remained - Suc 0 < length (reverseN 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.list old = - rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list 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.list big)))) = - rev (take (remained - count) aux) @ rev (take remained (rev (take count (Stack.list big))))\ - \ hd (rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list big)))) = - (rev (take count (Stack.list big)) @ aux) ! (remained - Suc 0)" + (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 reverseN_def size_list_length take_append take_hd_drop) - with 1 have [simp]: "Stack.first old = reverseN count (Stack.list big) aux ! (remained - Suc 0)" + with 1 have [simp]: "Stack.first old = reverseN count (Stack_Aux.list big) aux ! (remained - Suc 0)" by(auto simp: take_hd_drop first_hd) from 1 show ?case using reverseN_nth[of - "remained - Suc 0" "reverseN count (Stack.list big) aux" "Stack.first old" "[]" + "remained - Suc 0" "reverseN 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" 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) 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) qed -lemma pop_list_tl: "\0 < size big; invar big; Big.pop big = (x, big')\ - \ Big.list big' = tl (Big.list big)" +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) 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; - Stack.list old = - rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack.list 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.list 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: reverseN_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.list big \ []" + 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.list big) @ aux = - rev (Stack.list (Stack.pop big)) @ Stack.first big # aux" + 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 " - reverseN (Suc count) (Stack.list big) aux = - reverseN count (Stack.list (Stack.pop big)) (Stack.first big # aux)" - using reverseN_tl_hd[of "Suc count" "Stack.list big" aux] + reverseN (Suc count) (Stack_Aux.list big) aux = + reverseN count (Stack_Aux.list (Stack.pop big)) (Stack.first big # aux)" + using reverseN_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; - count \ size big; Stack.list old = rev aux @ Stack.list big; - take remained (rev aux) @ take (remained - length aux) (Stack.list big) = + 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.list big)); + drop (count - remained) (take count (Stack_Aux.list big)); \ size old \ length aux + size big\ - \ tl (rev aux @ Stack.list big) = rev aux @ Stack.list 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 (reverseN count (Stack.list big) aux); 0 < size old; + have b: "\remained \ length (reverseN 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; remained - count \ length aux; count \ size big; - Stack.list old = + Stack_Aux.list old = drop (length aux - (size old - size big)) (rev aux) @ - drop (size big - size old) (Stack.list big); + 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.list big)) = - drop (length (reverseN count (Stack.list big) aux) - remained) - (rev (reverseN count (Stack.list big) aux))\ + (drop (size big - size old) (Stack_Aux.list big)) = + drop (length (reverseN count (Stack_Aux.list big) aux) - remained) + (rev (reverseN count (Stack_Aux.list big) aux))\ \ tl (drop (length aux - (size old - size big)) (rev aux) @ - drop (size big - size old) (Stack.list big)) = + 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.list big)" + 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 (reverseN count (Stack.list big) aux)" + from 1 have "remained \ length (reverseN 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: reverseN_def) using b by simp 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 # Big.list_current big' = Big.list_current 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.list big))) \ []" + "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 size_empty: "\invar (big :: 'a state); size big = 0\ \ is_empty big" -proof(induction big) - case Reverse - then show ?case - by(auto simp: min_def Stack_Proof.list_empty split: if_splits current.splits) -next - case Common - then show ?case - by(auto simp: size_empty) -qed - lemma remaining_steps_step [simp]: "\invar (big :: 'a state); remaining_steps big > 0\ \ Suc (remaining_steps (step big)) = remaining_steps big" by(induction big rule: step_state.induct)(auto split: current.splits) lemma remaining_steps_step_0 [simp]: "\invar (big :: 'a 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; 0 < size 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" 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,150 +1,64 @@ section \Common\ theory Common imports Current Idle begin text \ \<^noindent> The last two phases of both deque ends during transformation: \<^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. \<^noindent> Each phase contains a \current\ state, that holds the original elements of the deque end. \ datatype (plugins del: size)'a 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> \list\: List abstraction of the elements which this end will contain after the transformation is finished -\<^descr> \list_current\: List abstraction of the elements currently in this deque end. -\<^descr> \step\: Executes one step of the transformation, while keeping the invariant. -\<^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> \size\: Minimum of \size_new\ and the number of elements contained in the \current\ state. -\ -(* -fun reverseN :: "nat \ 'a list \ 'a list \ 'a list" where - "reverseN 0 xs acc = acc" -| "reverseN n [] acc = acc" -| "reverseN (Suc n) (x#xs) acc = reverseN n xs (x#acc)" -*) -definition reverseN where -[simp]: "reverseN n xs acc \ rev (take n xs) @ acc" - -fun list :: "'a state \ 'a list" where - "list (Idle _ idle) = Idle.list idle" -| "list (Copy (Current extra _ _ remained) old new moved) - = extra @ reverseN (remained - moved) old new" - -fun list_current :: "'a state \ 'a list" where - "list_current (Idle current _) = Current.list current" -| "list_current (Copy current _ _ _) = Current.list current" +\<^descr> \step\: Executes one step of the transformation, while keeping the invariant.\ (* TODO: Maybe inline function? *) fun normalize :: "'a state \ 'a 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 )" | "normalize state = state" instantiation state ::(type) step begin fun step_state :: "'a state \ 'a 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 "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 "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))" -instantiation state ::(type) is_empty -begin - -fun is_empty_state :: "'a state \ bool" where - "is_empty (Idle current idle) \ is_empty current \ is_empty idle" -| "is_empty (Copy current _ _ _) \ is_empty current" - -instance.. -end - -instantiation state::(type) invar -begin - -fun invar_state :: "'a state \ bool" where - "invar (Idle current idle) \ - invar idle - \ invar current - \ size_new current = size idle - \ take (size idle) (Current.list current) = - take (size current) (Idle.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.list old) = take (size old) (reverseN (remained - moved) aux new) - )" - -instance.. end - -instantiation state::(type) size -begin - -(* Use size for emptiness? *) -fun size_state :: "'a 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 -begin - -fun size_new_state :: "'a state \ nat" where - "size_new (Idle current _) = size_new current" -| "size_new (Copy current _ _ _) = size_new current" - -instance.. -end - -instantiation state::(type) remaining_steps -begin - -fun remaining_steps_state :: "'a 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_Aux.thy b/thys/Real_Time_Deque/Common_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Common_Aux.thy @@ -0,0 +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_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> \size\: Minimum of \size_new\ and the number of elements contained in the \current\ state.\ + +definition reverseN where +[simp]: "reverseN n xs acc \ rev (take n xs) @ acc" + +fun list :: "'a state \ 'a list" where + "list (Idle _ idle) = Idle_Aux.list idle" +| "list (Copy (Current extra _ _ remained) old new moved) + = extra @ reverseN (remained - moved) old new" + +fun list_current :: "'a state \ 'a list" where + "list_current (Idle current _) = Current_Aux.list current" +| "list_current (Copy current _ _ _) = Current_Aux.list current" + +instantiation state::(type) invar +begin + +fun invar_state :: "'a 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) (reverseN (remained - moved) aux new) + )" + +instance.. +end + +instantiation state::(type) size +begin + +fun size_state :: "'a 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 +begin + +fun size_new_state :: "'a state \ nat" where + "size_new (Idle current _) = size_new current" +| "size_new (Copy current _ _ _) = size_new current" + +instance.. +end + +instantiation state::(type) remaining_steps +begin + +fun remaining_steps_state :: "'a 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,484 +1,473 @@ section "Common Proofs" theory Common_Proof -imports Common Idle_Proof Current_Proof +imports Common_Aux Idle_Proof Current_Proof begin lemma reverseN_drop: "reverseN n xs acc = drop (length xs - n) (rev xs) @ acc" unfolding reverseN_def using rev_take by blast lemma reverseN_step: "xs \ [] \ reverseN n (tl xs) (hd xs # acc) = reverseN (Suc n) xs acc" by (simp add: take_Suc) lemma reverseN_finish: "reverseN n [] acc = acc" by (simp) lemma reverseN_tl_hd: "0 < n \ xs \ [] \ reverseN n xs ys = reverseN (n - (Suc 0)) (tl xs) (hd xs #ys)" by (simp add: reverseN_step del: reverseN_def) lemma reverseN_nth: "n < length xs \ x = xs ! n \ x # reverseN n xs ys = reverseN (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) 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: ) next case False with Current show ?thesis by(auto simp: aux_not_empty reverseN_step Suc_diff_Suc simp del: reverseN_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) 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.list old) = take (size old) (hd aux # new)" + 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: reverseN_step Suc_diff_Suc simp del: reverseN_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_size_pop eq_snd_iff take_tl size_not_empty) + 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.list 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.list old) - = hd (Stack.list old) # take (remained - Suc 0) (tl (Stack.list old))" - by (metis Suc_pred \Stack.list old \ []\ list.collapse take_Suc_Cons) + 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.list old \ []" "remained - length new = 1" + "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.list old) = hd aux # take (size old - Suc 0) new + 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.list old) = take 1 (rev aux)" + from 1 True not_empty have "take 1 (Stack_Aux.list old) = take 1 (rev aux)" using take_1[of remained "size old" - "Stack.list 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: reverseN_drop length_minus_1 simp del: reverseN_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" by auto - with False have " - take remained (Stack.list old) = take (size old) (reverseN (remained - length new) aux new) - \ take (Suc 0) (Stack.list old) = take (Suc 0) (rev (take (remained - length new) aux))" + with False have + "take remained (Stack_Aux.list old) = + take (size old) (reverseN (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.list old" + "Stack_Aux.list old" " (reverseN (remained - length new) aux new)" ] by(auto simp: not_empty Suc_le_eq) - with 1 False have "take 1 (Stack.list old) = take 1 (rev (take (remained - length new) aux))" + 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.list stack \ []" + have not_empty: "\ is_empty stack" "Stack_Aux.list stack \ []" by auto - with 2 have "hd (Stack.list stack) = x" - using take_hd'[of "Stack.list stack" x "xs @ Stack.list old"] + 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) case 1 then show ?case using list_size by auto next case (2 current) then have "invar current" - "Current.list 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) 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.list current = []" + "Current_Aux.list current = []" "0 < size current" by(auto split: current.splits) then show ?case using list_size by auto qed - -lemma size_empty: "invar (common :: 'a state) \ size common = 0 \ is_empty common" -proof(induction common rule: is_empty_state.induct) - case 1 - then show ?case - by(auto simp: min_def size_empty size_new_empty split: if_splits) -next - case (2 current) - then have "invar current" - by(auto split: current.splits) - - with 2 show ?case - by(auto simp: min_def size_empty size_new_empty split: if_splits) -qed lemma step_size [simp]: "invar (common :: 'a state) \ size (step common) = size common" proof(induction common rule: step_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) \ size_new (step common) = size_new common" proof(induction common rule: step_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\ \ 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)\ \ 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\ \ 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; 0 < size 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" 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,77 +1,30 @@ 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 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. \ datatype (plugins del: size) 'a current = Current "'a list" nat "'a stack" nat -text \Specification functions: -\<^descr> \list\: list abstraction for the originally contained elements of a deque end during transformation. -\<^descr> \invar\: Is the stored number of newly added elements correct? -\<^descr> \size\: The number of the originally contained elements. -\<^descr> \size_new\: Number of elements which will be contained after the transformation is finished. -\ - 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)" -fun list :: "'a current \ 'a list" where - "list (Current extra _ old _) = extra @ (Stack.list old)" - -instantiation current::(type) is_empty -begin - -(* TODO: Actually it should be "added + remained = 0" Maybe directly base it on size? *) -fun is_empty_current :: "'a current \ bool" where - "is_empty (Current extra _ old remained) \ is_empty old \ extra = [] \ remained = 0" - -instance.. end - -instantiation current::(type) invar -begin - -fun invar_current :: "'a current \ bool" where - "invar (Current extra added _ _) \ length extra = added" - -instance.. -end - -instantiation current::(type) size -begin - -fun size_current :: "'a current \ nat" where - "size (Current _ added old _) = added + size old" - -instance.. -end - -instantiation current::(type) size_new -begin - -fun size_new_current :: "'a current \ nat" where - "size_new (Current _ added _ remained) = added + remained" - -instance.. -end - -end diff --git a/thys/Real_Time_Deque/Current_Aux.thy b/thys/Real_Time_Deque/Current_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Current_Aux.thy @@ -0,0 +1,41 @@ +theory Current_Aux +imports Current Stack_Aux +begin + +text \Specification functions: +\<^descr> \list\: list abstraction for the originally contained elements of a deque end during transformation. +\<^descr> \invar\: Is the stored number of newly added elements correct? +\<^descr> \size\: The number of the originally contained elements. +\<^descr> \size_new\: Number of elements which will be contained after the transformation is finished.\ + +fun list :: "'a current \ 'a list" where + "list (Current extra _ old _) = extra @ (Stack_Aux.list old)" + +instantiation current::(type) invar +begin + +fun invar_current :: "'a current \ bool" where + "invar (Current extra added _ _) \ length extra = added" + +instance.. +end + +instantiation current::(type) size +begin + +fun size_current :: "'a current \ nat" where + "size (Current _ added old _) = added + size old" + +instance.. +end + +instantiation current::(type) size_new +begin + +fun size_new_current :: "'a current \ nat" where + "size_new (Current _ added _ remained) = added + remained" + +instance.. +end + +end diff --git a/thys/Real_Time_Deque/Current_Proof.thy b/thys/Real_Time_Deque/Current_Proof.thy --- a/thys/Real_Time_Deque/Current_Proof.thy +++ b/thys/Real_Time_Deque/Current_Proof.thy @@ -1,90 +1,58 @@ section "Current Proofs" theory Current_Proof -imports Current Stack_Proof +imports Current_Aux Stack_Proof begin lemma push_list [simp]: "list (push x current) = x # list current" by(induction x current rule: push.induct) auto -lemma pop_list: "\\ is_empty current; pop current = (x, current')\ - \ x # list current' = list current" - by(induction current arbitrary: x rule: pop.induct)(auto simp: list_not_empty) - -lemma pop_list_size: "\invar current; 0 < size current; pop current = (x, current')\ - \ x # list current' = list current" - by(induction current arbitrary: x rule: pop.induct)(auto simp: size_not_empty list_not_empty) - -lemma drop_first_list [simp]: - "\ is_empty current \ list (drop_first current) = tl (list current)" - by(induction current rule: pop.induct)(auto simp: drop_Suc) - -lemma pop_list_2 [simp]: +lemma pop_list [simp]: "\0 < size current; invar current\ \ fst (pop current) # tl (list current) = list current" by(induction current rule: pop.induct)(auto simp: size_not_empty list_not_empty) -lemma drop_first_list_size [simp]: "\invar current; 0 < size current\ +lemma drop_first_list [simp]: "\invar current; 0 < size current\ \ list (drop_first current) = tl (list current)" by(induction current rule: pop.induct)(auto simp: drop_Suc) lemma invar_push: "invar current \ invar (push x current)" by(induction x current rule: push.induct) auto -lemma invar_pop: "\\ is_empty current; invar current; pop current = (x, current')\ - \ invar current'" - by(induction current arbitrary: x rule: pop.induct) auto - -lemma invar_size_pop: "\0 < size current; invar current; pop current = (x, current')\ +lemma invar_pop: "\0 < size current; invar current; pop current = (x, current')\ \ invar current'" by(induction current arbitrary: x rule: pop.induct) auto -lemma invar_size_drop_first: "\0 < size current; invar current\ \ invar (drop_first current)" - using invar_size_pop +lemma invar_drop_first: "\0 < size current; invar current\ \ invar (drop_first current)" + using invar_pop by (metis eq_snd_iff) -lemma invar_drop_first: "\\ is_empty current; invar current\ \ invar (drop_first current)" - by(induction current rule: pop.induct) auto - -lemma push_not_empty [simp]: "\\ is_empty current; is_empty (push x current)\ \ False" - by(induction x current rule: push.induct) auto - -(* TODO: not optimal with only one direction (Is it really needed?) *) -lemma size_empty: "invar (current :: 'a current) \ size current = 0 \ is_empty current" - by(induction current)(auto simp: size_empty) - -lemma size_new_empty: "invar (current :: 'a current) \ size_new current = 0 \ is_empty current" - by(induction current)(auto simp: size_empty) - -lemma list_not_empty [simp]: "\list current = []; \is_empty current\ \ False" - by(induction current)(auto simp: list_empty) - lemma list_size [simp]: "\invar current; list current = []; 0 < size current\ \ False" by(induction current)(auto simp: size_not_empty list_empty) lemma size_new_push [simp]: "invar current \ size_new (push x current) = Suc (size_new current)" by(induction x current rule: push.induct) auto lemma size_push [simp]: "size (push x current) = Suc (size current)" by(induction x current rule: push.induct) auto lemma size_new_pop [simp]: "\0 < size_new current; invar current \ \ Suc (size_new (drop_first current)) = size_new current" by(induction current rule: pop.induct) auto lemma size_pop [simp]: "\0 < size current; invar current \ \ Suc (size (drop_first current)) = size current" by(induction current rule: pop.induct) auto lemma size_pop_suc [simp]: "\0 < size current; invar current; pop current = (x, current') \ \ Suc (size current') = size current" by(induction current rule: pop.induct) auto lemma size_pop_sub: "\0 < size current; invar current; pop current = (x, current') \ \ size current' = size current - 1" by(induction current rule: pop.induct) auto lemma size_drop_first_sub: "\0 < size current; invar current \ \ size (drop_first current) = size current - 1" by(induction current rule: pop.induct) auto end \ No newline at end of file diff --git a/thys/Real_Time_Deque/Idle.thy b/thys/Real_Time_Deque/Idle.thy --- a/thys/Real_Time_Deque/Idle.thy +++ b/thys/Real_Time_Deque/Idle.thy @@ -1,48 +1,18 @@ section \Idle\ theory Idle imports Stack begin text \Represents the `idle' state of one deque end. It contains a \stack\ and its size as a natural number.\ datatype (plugins del: size) 'a idle = Idle "'a stack" nat -fun list :: "'a idle \ 'a list" where - "list (Idle stack _) = Stack.list stack" - fun push :: "'a \ 'a idle \ 'a idle" where "push x (Idle stack stackSize) = Idle (Stack.push x stack) (Suc stackSize)" fun pop :: "'a idle \ ('a * 'a idle)" where "pop (Idle stack stackSize) = (Stack.first stack, Idle (Stack.pop stack) (stackSize - 1))" - -instantiation idle :: (type) size -begin - -fun size_idle :: "'a idle \ nat" where - "size (Idle stack _) = size stack" - -instance.. -end - -instantiation idle :: (type) is_empty -begin - -fun is_empty_idle :: "'a idle \ bool" where - "is_empty (Idle stack _) \ is_empty stack" - -instance.. -end - -instantiation idle ::(type) invar -begin - -fun invar_idle :: "'a idle \ bool" where - "invar (Idle stack stackSize) \ size stack = stackSize" - -instance.. -end end diff --git a/thys/Real_Time_Deque/Idle_Aux.thy b/thys/Real_Time_Deque/Idle_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Idle_Aux.thy @@ -0,0 +1,35 @@ +theory Idle_Aux +imports Idle Stack_Aux +begin + +fun list :: "'a idle \ 'a list" where + "list (Idle stack _) = Stack_Aux.list stack" + +instantiation idle :: (type) size +begin + +fun size_idle :: "'a idle \ nat" where + "size (Idle stack _) = size stack" + +instance.. +end + +instantiation idle :: (type) is_empty +begin + +fun is_empty_idle :: "'a idle \ bool" where + "is_empty (Idle stack _) \ is_empty stack" + +instance.. +end + +instantiation idle ::(type) invar +begin + +fun invar_idle :: "'a idle \ bool" where + "invar (Idle stack stackSize) \ size stack = stackSize" + +instance.. +end + +end diff --git a/thys/Real_Time_Deque/Idle_Proof.thy b/thys/Real_Time_Deque/Idle_Proof.thy --- a/thys/Real_Time_Deque/Idle_Proof.thy +++ b/thys/Real_Time_Deque/Idle_Proof.thy @@ -1,71 +1,71 @@ section "Idle Proofs" theory Idle_Proof - imports Idle Stack_Proof + imports Idle_Aux Stack_Proof begin lemma push_list [simp]: "list (push x idle) = x # list idle" by(induction idle arbitrary: x) auto lemma pop_list [simp]: "\\ is_empty idle; pop idle = (x, idle')\ \ x # list idle' = list idle" by(induction idle arbitrary: x)(auto simp: list_not_empty) lemma pop_list_tl [simp]: "\\ is_empty idle; pop idle = (x, idle')\ \ x # (tl (list idle)) = list idle" by(induction idle arbitrary: x) (auto simp: list_not_empty) lemma pop_list_tl' [simp]: "\pop idle = (x, idle')\ \ list idle' = tl (list idle)" by(induction idle arbitrary: x)(auto simp: drop_Suc) lemma size_push [simp]: "size (push x idle) = Suc (size idle)" by(induction idle arbitrary: x) auto lemma size_pop [simp]: "\\is_empty idle; pop idle = (x, idle')\ \ Suc (size idle') = size idle" by(induction idle arbitrary: x)(auto simp: size_not_empty) lemma size_pop_sub: "\pop idle = (x, idle')\ \ size idle' = size idle - 1" by(induction idle arbitrary: x) auto lemma invar_push: "invar idle \ invar (push x idle)" by(induction x idle rule: push.induct) auto lemma invar_pop: "\\ is_empty idle; invar idle; pop idle = (x, idle')\ \ invar idle'" by(induction idle arbitrary: x rule: pop.induct) auto lemma size_empty: "size idle = 0 \ is_empty (idle :: 'a idle)" by(induction idle)(auto simp: size_empty) lemma size_not_empty: "0 < size idle \ \is_empty (idle :: 'a idle)" by(induction idle)(auto simp: size_not_empty) lemma size_empty_2 [simp]: "\\is_empty (idle :: 'a idle); 0 = size idle\ \ False" by (simp add: size_empty) lemma size_not_empty_2 [simp]: "\is_empty (idle :: 'a idle); 0 < size idle\ \ False" by (simp add: size_not_empty) lemma list_empty: "list idle = [] \ is_empty idle" by(induction idle)(simp add: list_empty) lemma list_not_empty: "list idle \ [] \ \ is_empty idle" by(induction idle)(simp add: list_not_empty) lemma list_empty_2 [simp]: "\list idle = []; \is_empty (idle :: 'a idle)\ \ False" using list_empty by blast lemma list_not_empty_2 [simp]: "\list idle \ []; is_empty (idle :: 'a idle)\ \ False" using list_not_empty by blast lemma list_empty_size: "list idle = [] \ 0 = size idle" by (simp add: list_empty size_empty) lemma list_not_empty_size: "list idle \ [] \ 0 < size idle" by (simp add: list_empty_size) lemma list_empty_size_2 [simp]: "\list idle \ []; 0 = size idle\ \ False" by (simp add: list_empty size_empty) lemma list_not_empty_size_2 [simp]: "\list idle = []; 0 < size idle\ \ False" by (simp add: list_empty_size) 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,228 +1,192 @@ section \Real-Time Deque Implementation\ theory RealTimeDeque imports States begin text\ The real-time deque can be in the following states: \<^descr> \Empty\: No values stored. No dequeue operation possible. \<^descr> \One\: One element in the deque. \<^descr> \Two\: Two elements in the deque. \<^descr> \Three\: Three elements in the deque. \<^descr> \Idle\: Deque with a left and a right end, fulfilling the following invariant: \<^item> 3 * size of left end \\\ size of right end \<^item> 3 * size of right end \\\ size of left end \<^item> Neither of the ends is empty \<^descr> \Transforming\: Deque which violated the invariant of the \idle\ state by non-balanced dequeue and enqueue operations. The invariants during in this state are: \<^item> The transformation is not done yet. The deque needs to be in \idle\ state otherwise. \<^item> The transformation is in a valid state (Defined in theory \States\) \<^item> The two ends of the deque are in a size window, such that after finishing the transformation the invariant of the \idle\ state will be met. 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\: 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> \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" 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))" fun small_deque :: "'a list \ 'a list \ 'a deque" where "small_deque [] [] = Empty" | "small_deque (x#[]) [] = One x" | "small_deque [] (x#[]) = One x" | "small_deque (x#[])(y#[]) = Two y x" | "small_deque (x#y#[]) [] = Two y x" | "small_deque [] (x#y#[])= Two y x" | "small_deque [] (x#y#z#[]) = Three z y x" | "small_deque (x#y#z#[]) [] = Three z y x" | "small_deque (x#y#[]) (z#[]) = Three z y x" | "small_deque (x#[]) (y#z#[]) = Three z y x" fun deqL' :: "'a deque \ 'a * 'a deque" where "deqL' (One x) = (x, Empty)" | "deqL' (Two x y) = (x, One y)" | "deqL' (Three x y z) = (x, Two y z)" | "deqL' (Idle left (idle.Idle right length_right)) = ( case Idle.pop left of (x, (idle.Idle left length_left)) \ if 3 * length_left \ length_right then (x, Idle (idle.Idle left length_left) (idle.Idle right length_right)) else if length_left \ 1 then let length_left' = 2 * length_left + 1 in let length_right' = length_right - length_left - 1 in let small = Reverse1 (Current [] 0 left length_left') left [] in let big = Reverse (Current [] 0 right length_right') right [] length_right' in let states = States Left big small in let states = (step^^6) states in (x, Transforming states) else case right of Stack r1 r2 \ (x, small_deque r1 r2) )" | "deqL' (Transforming (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) )" | "deqL' (Transforming (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) )" fun deqR' :: "'a deque \ 'a * 'a deque" where "deqR' deque = ( let (x, deque) = deqL' (swap deque) in (x, swap deque) )" fun deqL :: "'a deque \ 'a deque" where "deqL deque = (let (_, deque) = deqL' deque in deque)" fun deqR :: "'a deque \ 'a deque" where "deqR deque = (let (_, deque) = deqR' deque in deque)" fun firstL :: "'a deque \ 'a" where "firstL deque = (let (x, _) = deqL' deque in x)" fun firstR :: "'a deque \ 'a" where "firstR deque = (let (x, _) = deqR' deque in x)" fun enqL :: "'a \ 'a deque \ 'a deque" where "enqL x Empty = One x" | "enqL x (One y) = Two x y" | "enqL x (Two y z) = Three x y z" | "enqL x (Three a b c) = Idle (idle.Idle (Stack [x, a] []) 2) (idle.Idle (Stack [c, b] []) 2)" | "enqL x (Idle left (idle.Idle right length_right)) = ( case Idle.push x left of idle.Idle left length_left \ if 3 * length_right \ length_left then Idle (idle.Idle left length_left) (idle.Idle right length_right) else let length_left = length_left - length_right - 1 in let length_right = 2 * length_right + 1 in let big = Reverse (Current [] 0 left length_left) left [] length_left in let small = Reverse1 (Current [] 0 right length_right) right [] in let states = States Right big small in let states = (step^^6) states in Transforming states )" | "enqL x (Transforming (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 )" | "enqL x (Transforming (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 )" fun enqR :: "'a \ 'a deque \ 'a deque" where "enqR x deque = ( let deque = enqL x (swap deque) in swap deque )" - -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.list left @ (rev (Idle.list right))" -| "listL (Transforming states) = States.listL states" - -abbreviation listR :: "'a deque \ 'a list" where - "listR deque \ rev (listL deque)" - -instantiation deque::(type) invar -begin - -fun invar_deque :: "'a deque \ bool" where - "invar Empty = True" -| "invar (One _) = True" -| "invar (Two _ _) = True" -| "invar (Three _ _ _) = True" -| "invar (Idle left right) \ - invar left \ - invar right \ - \ is_empty left \ - \ is_empty right \ - 3 * size right \ size left \ - 3 * size left \ size right - " -| "invar (Transforming states) \ - invar states \ - size_ok states \ - 0 < remaining_steps states - " - -instance.. -end end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Aux.thy b/thys/Real_Time_Deque/RealTimeDeque_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/RealTimeDeque_Aux.thy @@ -0,0 +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" + +abbreviation listR :: "'a deque \ 'a list" where + "listR deque \ rev (listL deque)" + +instantiation deque::(type) invar +begin + +fun invar_deque :: "'a deque \ bool" where + "invar Empty = True" +| "invar (One _) = True" +| "invar (Two _ _) = True" +| "invar (Three _ _ _) = True" +| "invar (Idle left right) \ + invar left \ + invar right \ + \ is_empty left \ + \ is_empty right \ + 3 * size right \ size left \ + 3 * size left \ size right + " +| "invar (Transforming states) \ + invar states \ + size_ok states \ + 0 < remaining_steps states + " + +instance.. +end + +end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Dequeue.thy b/thys/Real_Time_Deque/RealTimeDeque_Dequeue.thy deleted file mode 100644 --- a/thys/Real_Time_Deque/RealTimeDeque_Dequeue.thy +++ /dev/null @@ -1,466 +0,0 @@ -section "Dequeue Proofs" - -theory RealTimeDeque_Dequeue -imports Deque RealTimeDeque 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 - - then show ?thesis - proof(cases "length_left' \ 1") - case True - let ?big = "Reverse (Current [] 0 right (size right - Suc length_left')) - right [] (size right - Suc length_left')" - let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" - let ?states = "States Left ?big ?small" - - from 4 Start_Transformation True invar_left' have invar: "invar ?states" - by(auto simp: Let_def rev_take rev_drop) - - with 4 Start_Transformation True invar_left' - have "States.listL ?states = tl (Idle.list left) @ rev (Stack.list right)" - using pop_list_tl'[of left x left'] - by (auto simp del: reverseN_def) - - with invar - have "States.listL ((step^^6) ?states) = tl (Idle.list left) @ rev (Stack.list right)" - using step_n_listL[of ?states 6] - by presburger - - with 4 Start_Transformation True show ?thesis - by(auto simp: Let_def) - next - case False - from False Start_Transformation 4 have [simp]:"size left = 1" - using size_left' size_left'_size_left by auto - - with False Start_Transformation 4 have [simp]: "Idle.list left = [x]" - by(induction left)(auto simp: length_one_hd split: stack.splits) - - obtain right1 right2 where "right = Stack right1 right2" - using Stack.list.cases by blast - - with False Start_Transformation 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.list_current small' = Small.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.listL ?states_new = Small.list_current small @ rev (Big.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.listL ?states_stepped = - Small.list_current small @ rev (Big.list_current big)" - using States_Proof.step_n_listL invar listL by metis - - then have "listL (deqL (Transforming (States Left big small))) = States.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))) = - Small.list_current small @ rev (Big.list_current big)" - by auto - - with 5(1) have "listL (Transforming (States Left big small)) = - Small.list_current small @ rev (Big.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))" - 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.list_current big' = Big.list_current big" - using big_invar big_size pop by auto - - then have listL: - "x # States.listL ?states_new = Big.list_current big @ rev (Small.list_current small)" - proof(cases "States.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.listL ?states_stepped = Big.list_current big @ rev (Small.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))) = States.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))) = - Big.list_current big @ rev (Small.list_current small)" - by auto - - with 6(1) have "listL (Transforming (States Right big small)) = - Big.list_current big @ rev (Small.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))" - 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.list left' = Idle.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 - then show ?thesis - proof(cases "1 \ size left'") - case True - let ?big = - "Reverse - (Current [] 0 right (size right - Suc length_left')) - right [] (size right - Suc length_left')" - let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" - let ?states = "States Left ?big ?small" - - from 4 Start_Transformation True invar_left' - 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 - 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 - 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 - 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" - by auto - - with False Start_Transformation 4 have [simp]: "Idle.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.list.cases by blast - - with False Start_Transformation 4 show ?thesis - by(induction right1 right2 rule: small_deque.induct) auto - qed - qed -next - case (5 big small) - - obtain x small' where small' [simp]: "Small.pop small = (x, small')" - by fastforce - - let ?states = "States Left big small'" - let ?states_stepped = "(step^^4) ?states" - - obtain big_stepped small_stepped where stepped [simp]: - "?states_stepped = States Left big_stepped small_stepped" - by (metis remaining_steps_states.cases step_n_same) - - from 5 have invar: "invar ?states" - using invar_pop_small[of Left big small x small'] - by auto - - then have invar_stepped: "invar ?states_stepped" - using invar_step_n by blast - - show ?case - proof(cases "4 < remaining_steps ?states") - case True - - then have remaining_steps: "0 < remaining_steps ?states_stepped" - using invar remaining_steps_n_steps_sub[of ?states 4] - by simp - - from True have size_ok: "size_ok ?states_stepped" - using step_4_pop_small_size_ok[of Left big small x small'] 5(1) - by auto - - from remaining_steps size_ok invar_stepped show ?thesis - by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split) - next - case False - then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" - using invar by(auto simp del: stepped) - - then obtain small_current small_idle big_current big_idle where idle [simp]: " - States Left big_stepped small_stepped = - States Left - (Big.state.Common (state.Idle big_current big_idle)) - (Small.state.Common (state.Idle small_current small_idle)) - " - using remaining_steps_idle' invar_stepped remaining_steps_stepped - by fastforce - - have size_new_small : "1 < size_new small" - using 5 by auto - - have [simp]: "size_new small = Suc (size_new small')" - using 5 by auto - - have [simp]: "size_new small' = size_new small_stepped" - using invar step_n_size_new_small stepped - by metis - - have [simp]: "size_new small_stepped = size small_idle" - using idle invar_stepped - by(cases small_stepped) auto - - have [simp]: "\is_empty small_idle" - using size_new_small - by (simp add: Idle_Proof.size_not_empty) - - have [simp]: "size_new big = size_new big_stepped" - by (metis invar step_n_size_new_big stepped) - - have [simp]: "size_new big_stepped = size big_idle" - using idle invar_stepped - by(cases big_stepped) auto - - have "0 < size big_idle" - using 5 by auto - - then have [simp]: "\is_empty big_idle" - by (auto simp: Idle_Proof.size_not_empty) - - have [simp]: "size small_idle \ 3 * size big_idle" - using 5 by auto - - have [simp]: "size big_idle \ 3 * size small_idle" - using 5 by auto - - show ?thesis - using invar_stepped by auto - qed -next - case (6 big small) - - obtain x big' where big' [simp]: "Big.pop big = (x, big')" - by fastforce - - let ?states = "States Right big' small" - let ?states_stepped = "(step^^4) ?states" - - obtain big_stepped small_stepped where stepped [simp]: - "?states_stepped = States Right big_stepped small_stepped" - by (metis remaining_steps_states.cases step_n_same) - - from 6 have invar: "invar ?states" - using invar_pop_big[of Right big small x big'] - by auto - - then have invar_stepped: "invar ?states_stepped" - using invar_step_n by blast - - show ?case - proof(cases "4 < remaining_steps ?states") - case True - - then have remaining_steps: "0 < remaining_steps ?states_stepped" - using invar remaining_steps_n_steps_sub[of ?states 4] - by simp - - from True have size_ok: "size_ok ?states_stepped" - using step_4_pop_big_size_ok[of Right big small x big'] 6(1) - by auto - - from remaining_steps size_ok invar_stepped show ?thesis - by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split) - next - case False - then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" - using invar by(auto simp del: stepped) - - then obtain small_current small_idle big_current big_idle where idle [simp]: " - States Right big_stepped small_stepped = - States Right - (Big.state.Common (state.Idle big_current big_idle)) - (Small.state.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_Dequeue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy @@ -0,0 +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 + + then show ?thesis + proof(cases "length_left' \ 1") + case True + let ?big = "Reverse (Current [] 0 right (size right - Suc length_left')) + right [] (size right - Suc length_left')" + let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" + let ?states = "States Left ?big ?small" + + from 4 Start_Transformation True invar_left' have invar: "invar ?states" + by(auto simp: Let_def rev_take rev_drop) + + with 4 Start_Transformation 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: reverseN_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 + by(auto simp: Let_def) + next + case False + from False Start_Transformation 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]" + 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 + 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" + 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))) = + Small_Aux.list_current small @ rev (Big_Aux.list_current big)" + by auto + + with 5(1) have "listL (Transforming (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))" + 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))) = + 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))) = + Big_Aux.list_current big @ rev (Small_Aux.list_current small)" + by auto + + with 6(1) have "listL (Transforming (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))" + 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 + then show ?thesis + proof(cases "1 \ size left'") + case True + let ?big = + "Reverse + (Current [] 0 right (size right - Suc length_left')) + right [] (size right - Suc length_left')" + let ?small = "Reverse1 (Current [] 0 stack_left' (Suc (2 * length_left'))) stack_left' []" + let ?states = "States Left ?big ?small" + + from 4 Start_Transformation True invar_left' + 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 + 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 + 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 + 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" + by auto + + with False Start_Transformation 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 + by(induction right1 right2 rule: small_deque.induct) auto + qed + qed +next + case (5 big small) + + obtain x small' where small' [simp]: "Small.pop small = (x, small')" + by fastforce + + let ?states = "States Left big small'" + let ?states_stepped = "(step^^4) ?states" + + obtain big_stepped small_stepped where stepped [simp]: + "?states_stepped = States Left big_stepped small_stepped" + by (metis remaining_steps_states.cases step_n_same) + + from 5 have invar: "invar ?states" + using invar_pop_small[of Left big small x small'] + by auto + + then have invar_stepped: "invar ?states_stepped" + using invar_step_n by blast + + show ?case + proof(cases "4 < remaining_steps ?states") + case True + + then have remaining_steps: "0 < remaining_steps ?states_stepped" + using invar remaining_steps_n_steps_sub[of ?states 4] + by simp + + from True have size_ok: "size_ok ?states_stepped" + using step_4_pop_small_size_ok[of Left big small x small'] 5(1) + by auto + + from remaining_steps size_ok invar_stepped show ?thesis + by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split) + next + case False + then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" + using invar by(auto simp del: stepped) + + then obtain small_current small_idle big_current big_idle where idle [simp]: " + States Left big_stepped small_stepped = + States Left + (Big.state.Common (state.Idle big_current big_idle)) + (Small.state.Common (state.Idle small_current small_idle)) + " + using remaining_steps_idle' invar_stepped remaining_steps_stepped + by fastforce + + have size_new_small : "1 < size_new small" + using 5 by auto + + have [simp]: "size_new small = Suc (size_new small')" + using 5 by auto + + have [simp]: "size_new small' = size_new small_stepped" + using invar step_n_size_new_small stepped + by metis + + have [simp]: "size_new small_stepped = size small_idle" + using idle invar_stepped + by(cases small_stepped) auto + + have [simp]: "\is_empty small_idle" + using size_new_small + by (simp add: Idle_Proof.size_not_empty) + + have [simp]: "size_new big = size_new big_stepped" + by (metis invar step_n_size_new_big stepped) + + have [simp]: "size_new big_stepped = size big_idle" + using idle invar_stepped + by(cases big_stepped) auto + + have "0 < size big_idle" + using 5 by auto + + then have [simp]: "\is_empty big_idle" + by (auto simp: Idle_Proof.size_not_empty) + + have [simp]: "size small_idle \ 3 * size big_idle" + using 5 by auto + + have [simp]: "size big_idle \ 3 * size small_idle" + using 5 by auto + + show ?thesis + using invar_stepped by auto + qed +next + case (6 big small) + + obtain x big' where big' [simp]: "Big.pop big = (x, big')" + by fastforce + + let ?states = "States Right big' small" + let ?states_stepped = "(step^^4) ?states" + + obtain big_stepped small_stepped where stepped [simp]: + "?states_stepped = States Right big_stepped small_stepped" + by (metis remaining_steps_states.cases step_n_same) + + from 6 have invar: "invar ?states" + using invar_pop_big[of Right big small x big'] + by auto + + then have invar_stepped: "invar ?states_stepped" + using invar_step_n by blast + + show ?case + proof(cases "4 < remaining_steps ?states") + case True + + then have remaining_steps: "0 < remaining_steps ?states_stepped" + using invar remaining_steps_n_steps_sub[of ?states 4] + by simp + + from True have size_ok: "size_ok ?states_stepped" + using step_4_pop_big_size_ok[of Right big small x big'] 6(1) + by auto + + from remaining_steps size_ok invar_stepped show ?thesis + by(cases big_stepped; cases small_stepped) (auto simp: Let_def split!: Common.state.split) + next + case False + then have remaining_steps_stepped: "remaining_steps ?states_stepped = 0" + using invar by(auto simp del: stepped) + + then obtain small_current small_idle big_current big_idle where idle [simp]: " + States Right big_stepped small_stepped = + States Right + (Big.state.Common (state.Idle big_current big_idle)) + (Small.state.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.thy b/thys/Real_Time_Deque/RealTimeDeque_Enqueue.thy deleted file mode 100644 --- a/thys/Real_Time_Deque/RealTimeDeque_Enqueue.thy +++ /dev/null @@ -1,322 +0,0 @@ -section "Enqueue Proofs" - -theory RealTimeDeque_Enqueue -imports Deque RealTimeDeque 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 ?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.listL ?states = x # Idle.list left @ rev (Stack.list right)" - using Idle_Proof.push_list[of x left] - by(auto) - - then have "States.listL ?states_stepped = x # Idle.list left @ rev (Stack.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.listL ?states_stepped = x # Small.list_current small @ rev (Big.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) -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.listL ?states = x # Big.list_current big @ rev (Small.list_current small)" - using app_rev[of _ _ _ "x # Big.list_current big"] - by(auto split: prod.split) - - then have " - States.listL ?states_stepped = x # Big.list_current big @ rev (Small.list_current small)" - by (metis invar step_n_listL) - - with list_invar show ?case - using app_rev[of "Small.list_current small" "Big.list_current big"] - by(cases big_stepped; cases small_stepped) - (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 [])" - 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) - 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)) - " - 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) - 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)) - " - 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_Enqueue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/RealTimeDeque_Enqueue_Proof.thy @@ -0,0 +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 ?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) +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) +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 [])" + 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) + 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)) + " + 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) + 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)) + " + 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 Deque RealTimeDeque States_Proof RealTimeDeque_Dequeue RealTimeDeque_Enqueue +imports RealTimeDeque_Dequeue_Proof RealTimeDeque_Enqueue_Proof begin lemma swap_lists_left: "invar (States Left big small) \ - States.listL (States Left big small) = rev (States.listL (States Right big small))" + States_Aux.listL (States Left big small) = rev (States_Aux.listL (States Right big small))" by(auto split: prod.splits Big.state.splits Small.state.splits) lemma swap_lists_right: "invar (States Right big small) \ - States.listL (States Right big small) = rev (States.listL (States Left big small))" + States_Aux.listL (States Right big small) = rev (States_Aux.listL (States Left big small))" by(auto split: prod.splits Big.state.splits Small.state.splits) lemma swap_list [simp]: "invar q \ listR (swap q) = listL q" proof(induction q) case (Transforming states) then show ?case apply(cases states) using swap_lists_left swap_lists_right - by (metis (full_types) RealTimeDeque.listL.simps(6) direction.exhaust invar_deque.simps(6) swap.simps(6) swap.simps(7)) + 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,135 +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: \<^descr> \Reverse1\: Using the \step\ function the originally contained elements are reversed. \<^descr> \Reverse2\: Using the \step\ function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase. \<^descr> \Common\: See theory \Common\. Is used to reverse the elements from the two previous phases again to get them again in the original order. \<^noindent> Each phase contains a \current\ state, which holds the original elements of the deque end. \ datatype (plugins del: size) 'a state = Reverse1 "'a current" "'a stack" "'a list" | Reverse2 "'a current" "'a list" "'a stack" "'a list" nat | Common "'a Common.state" text \\<^noindent> Functions: \<^descr> \push\, \pop\: Add and remove elements using the \current\ state. - \<^descr> \step\: Executes one step of the transformation, while keeping the invariant. - \<^descr> \size_new\: Returns the size, that the deque end will have after the transformation 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_current\: List abstraction of the elements currently in this deque end. -\ - -fun list :: "'a state \ 'a list" where - "list (Common common) = Common.list common" -| "list (Reverse2 (Current extra _ _ remained) aux big new count) = - extra @ reverseN (remained - (count + size big)) aux (rev (Stack.list big) @ new)" - -fun list_current :: "'a state \ 'a list" where - "list_current (Common common) = Common.list_current common" -| "list_current (Reverse2 current _ _ _ _) = Current.list current" -| "list_current (Reverse1 current _ _) = Current.list current" + \<^descr> \step\: Executes one step of the transformation, while keeping the invariant.\ instantiation state::(type) step begin fun step_state :: "'a state \ 'a state" where "step (Common state) = Common (step state)" | "step (Reverse1 current small auxS) = ( if is_empty small then Reverse1 current small auxS else Reverse1 current (Stack.pop small) ((Stack.first small)#auxS) )" | "step (Reverse2 current auxS big newS count) = ( if is_empty big then Common (normalize (Copy current auxS newS count)) else Reverse2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1) )" instance.. end fun push :: "'a \ 'a 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 pop :: "'a state \ 'a * 'a state" where "pop (Common state) = ( let (x, state) = Common.pop state in (x, Common state) )" | "pop (Reverse1 current small auxS) = (first current, Reverse1 (drop_first current) small auxS)" | "pop (Reverse2 current auxS big newS count) = (first current, Reverse2 (drop_first current) auxS big newS count)" -instantiation state::(type) is_empty -begin - -fun is_empty_state :: "'a state \ bool" where - "is_empty (Common state) = is_empty state" -| "is_empty (Reverse1 current _ _) = is_empty current" -| "is_empty (Reverse2 current _ _ _ _) = is_empty current" - -instance.. -end - -instantiation state::(type) invar -begin - -fun invar_state :: "'a state \ bool" where - "invar (Common state) = invar state" -| "invar (Reverse2 current auxS big newS count) = ( - case current of Current _ _ old remained \ - remained = count + size big + size old - \ remained \ size old - \ count = List.length newS - \ invar current - \ List.length auxS \ size old - \ Stack.list old = rev (take (size old) auxS) - )" -| "invar (Reverse1 current small auxS) = ( - case current of Current _ _ old remained \ - invar current - \ remained \ size old - \ size small + List.length auxS \ size old - \ Stack.list old = rev (take (size old) (rev (Stack.list small) @ auxS)) - )" - -instance.. -end - -instantiation 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)" - -instance.. -end - -instantiation 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" - -instance.. -end - 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 new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Small_Aux.thy @@ -0,0 +1,68 @@ +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\: 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_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) = + extra @ reverseN (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" + +instantiation state::(type) invar +begin + +fun invar_state :: "'a state \ bool" where + "invar (Common state) = invar state" +| "invar (Reverse2 current auxS big newS count) = ( + case current of Current _ _ old remained \ + remained = count + size big + size old + \ remained \ size old + \ count = List.length newS + \ invar current + \ List.length auxS \ size old + \ Stack_Aux.list old = rev (take (size old) auxS) + )" +| "invar (Reverse1 current small auxS) = ( + case current of Current _ _ old remained \ + invar current + \ remained \ size old + \ size small + List.length auxS \ size old + \ Stack_Aux.list old = rev (take (size old) (rev (Stack_Aux.list small) @ auxS)) + )" + +instance.. +end + +instantiation 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)" + +instance.. +end + +instantiation 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" + +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,255 +1,229 @@ section "Small Proofs" theory Small_Proof -imports Common_Proof Small +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 size_empty: "invar (small :: 'a state) \ size small = 0 \ is_empty small" - by(induction small) - (auto simp: Common_Proof.size_empty Stack_Proof.list_empty 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" 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) lemma step_list_common [simp]: "\small = Common common; invar small\ \ list (step small) = list small" by auto lemma step_list_reverse2 [simp]: assumes "small = (Reverse2 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.list (Stack.pop big)) @ [Stack.first big] = rev (Stack.list 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) 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.list small) @ aux = - rev (Stack.list (Stack.pop small)) @ Stack.first small # aux" + 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" by auto -lemma push_list_reverse2 [simp]: "small = (Reverse2 current auxS big newS count) - \ list (push x small) = x # list small" - by(induction x current rule: Current.push.induct) auto - -lemma pop_list_Reverse2 [simp]: "\ - small = (Reverse2 current auxS big newS count); - \is_empty small; - invar small; - pop small = (x, small') -\ \ x # list small' = list small" -proof(induction current arbitrary: x rule: Current.pop.induct) - case (1 added old remained) - then have "0 < size old" - by(auto simp: Stack_Proof.size_not_empty) - - with 1 show ?case - by(auto simp: rev_take Cons_nth_drop_Suc Suc_diff_le hd_drop_conv_nth) -next - case (2 x xs added old remained) - then show ?case by auto -qed - 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) then have "invar current" by(auto split: current.splits) with Reverse1 show ?case using Current_Proof.list_size by auto next case Reverse2 then show ?case by(auto split: current.splits) next case Common 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) \ \ - fst (Current.pop current) # Small.list (Reverse2 (drop_first current) auxS big newS count) = - Small.list (Reverse2 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)" 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/Stack.thy b/thys/Real_Time_Deque/Stack.thy --- a/thys/Real_Time_Deque/Stack.thy +++ b/thys/Real_Time_Deque/Stack.thy @@ -1,51 +1,35 @@ section \Stack\ theory Stack imports Type_Classes begin text \A datatype encapsulating two lists. Is used as a base data-structure in different places. It has the operations \push\, \pop\ and \first\. The function \list\ appends the two lists and is needed for the list abstraction of the deque.\ datatype (plugins del: size) 'a stack = Stack "'a list" "'a list" -(* TODO: Move into emptyable? *) -definition empty where - "empty \ Stack [] []" - fun push :: "'a \ 'a stack \ 'a stack" where "push x (Stack left right) = Stack (x#left) right" fun pop :: "'a stack \ 'a stack" where "pop (Stack [] []) = Stack [] []" | "pop (Stack (x#left) right) = Stack left right" | "pop (Stack [] (x#right)) = Stack [] right" fun first :: "'a stack \ 'a" where "first (Stack (x#left) right) = x" | "first (Stack [] (x#right)) = x" -fun list :: "'a stack \ 'a list" where - "list (Stack left right) = left @ right" - instantiation stack ::(type) is_empty begin fun is_empty_stack where "is_empty_stack (Stack [] []) = True" | "is_empty_stack _ = False" instance.. end -instantiation stack ::(type) size -begin - -fun size_stack :: "'a stack \ nat" where - "size (Stack left right) = length left + length right" - -instance.. -end - end \ No newline at end of file diff --git a/thys/Real_Time_Deque/Stack_Aux.thy b/thys/Real_Time_Deque/Stack_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/Stack_Aux.thy @@ -0,0 +1,17 @@ +theory Stack_Aux +imports Stack +begin + +fun list :: "'a stack \ 'a list" where + "list (Stack left right) = left @ right" + +instantiation stack ::(type) size +begin + +fun size_stack :: "'a stack \ nat" where + "size (Stack left right) = length left + length right" + +instance.. +end + +end diff --git a/thys/Real_Time_Deque/Stack_Proof.thy b/thys/Real_Time_Deque/Stack_Proof.thy --- a/thys/Real_Time_Deque/Stack_Proof.thy +++ b/thys/Real_Time_Deque/Stack_Proof.thy @@ -1,104 +1,104 @@ section "Stack Proofs" theory Stack_Proof -imports Stack RTD_Util +imports Stack_Aux RTD_Util begin lemma push_list [simp]: "list (push x stack) = x # list stack" by(cases stack) auto lemma pop_list [simp]: "\ is_empty stack \ list (pop stack) = tl (list stack)" by(induction stack rule: pop.induct) auto lemma first_list [simp]: "\ is_empty stack \ first stack = hd (list stack)" by(induction stack rule: first.induct) auto lemma list_empty: "list stack = [] \ is_empty stack" by(induction stack rule: is_empty_stack.induct) auto lemma list_not_empty: "list stack \ [] \ \ is_empty stack" by(induction stack rule: is_empty_stack.induct) auto lemma list_empty_2 [simp]: "\list stack \ []; is_empty stack\ \ False" by (simp add: list_empty) lemma list_not_empty_2 [simp]:"\list stack = []; \ is_empty stack\ \ False" by (simp add: list_empty) lemma list_empty_size: "list stack = [] \ size stack = 0" by(induction stack) auto lemma list_not_empty_size:"list stack \ [] \ 0 < size stack" by(induction stack) auto lemma list_empty_size_2 [simp]: "\list stack \ []; size stack = 0\ \ False" by (simp add: list_empty_size) lemma list_not_empty_size_2 [simp]:"\list stack = []; 0 < size stack\ \ False" by (simp add: list_empty_size) lemma size_push [simp]: "size (push x stack) = Suc (size stack)" by(cases stack) auto lemma size_pop [simp]: "size (pop stack) = size stack - Suc 0" by(induction stack rule: pop.induct) auto lemma size_empty: "size (stack :: 'a stack) = 0 \ is_empty stack" by(induction stack rule: is_empty_stack.induct) auto lemma size_not_empty: "size (stack :: 'a stack) > 0 \ \ is_empty stack" by(induction stack rule: is_empty_stack.induct) auto lemma size_empty_2[simp]: "\size (stack :: 'a stack) = 0; \is_empty stack\ \ False" by (simp add: size_empty) lemma size_not_empty_2[simp]: "\0 < size (stack :: 'a stack); is_empty stack\ \ False" by (simp add: size_not_empty) lemma size_list_length [simp]: "length (list stack) = size stack" by(cases stack) auto lemma first_pop [simp]: "\ is_empty stack \ first stack # list (pop stack) = list stack" by(induction stack rule: pop.induct) auto lemma push_not_empty [simp]: "\\ is_empty stack; is_empty (push x stack)\ \ False" by(induction x stack rule: push.induct) auto lemma pop_list_length [simp]: "\ is_empty stack \ Suc (length (list (pop stack))) = length (list stack)" by(induction stack rule: pop.induct) auto -lemma first_take: "\is_empty stack \ [first stack] = take 1 (Stack.list stack)" +lemma first_take: "\is_empty stack \ [first stack] = take 1 (list stack)" by (simp add: list_empty) lemma first_take_tl [simp]: "0 < size big \ (first big # take count (tl (list big))) = take (Suc count) (list big)" by(induction big rule: Stack.first.induct) auto lemma first_take_pop [simp]: "\\is_empty stack; 0 < x\ \ first stack # take (x - Suc 0) (list (pop stack)) = take x (list stack)" by(induction stack rule: pop.induct) (auto simp: take_Cons') lemma [simp]: "first (Stack [] []) = undefined" by (meson first.elims list.distinct(1) stack.inject) -lemma first_hd: "Stack.first stack = hd (Stack.list stack)" +lemma first_hd: "first stack = hd (list stack)" by(induction stack rule: first.induct)(auto simp: hd_def) lemma pop_tl [simp]: "list (pop stack) = tl (list stack)" by(induction stack rule: pop.induct) auto lemma pop_drop: "list (pop stack) = drop 1 (list stack)" by (simp add: drop_Suc) lemma popN_drop [simp]: "list ((pop ^^ n) stack) = drop n (list stack)" by(induction n)(auto simp: drop_Suc tl_drop) lemma popN_size [simp]: "size ((pop ^^ n) stack) = (size stack) - n" by(induction n) auto lemma take_first: "\0 < size s1; 0 < size s2; take (size s1) (list s2) = take (size s2) (list s1)\ \ first s1 = first s2" by(induction s1 rule: first.induct; induction s2 rule: first.induct) auto end 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,114 +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" 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 left right) = States dir (step left) (step right)" instance.. end -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 - )" - -instance.. end - -fun lists :: "'a states \ 'a list * 'a list" where - "lists (States _ (Reverse currentB big auxB count) (Reverse1 currentS small auxS)) = ( - Big.list (Reverse currentB big auxB count), - Small.list (Reverse2 currentS (reverseN count (Stack.list small) auxS) ((Stack.pop ^^ count) big) [] 0) - )" -| "lists (States _ big small) = (Big.list big, Small.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.list_current big, Small.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 _) \ - size big - count = remained - size old \ count \ size small - | (_, Reverse1 _ _ _) \ False - | (Reverse _ _ _ _, _) \ 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)" - -instantiation states::(type) is_empty -begin - -fun is_empty_states :: "'a states \ bool" where - "is_empty (States _ big small) \ is_empty big \ is_empty small" - -instance.. -end - -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_Aux.thy b/thys/Real_Time_Deque/States_Aux.thy new file mode 100644 --- /dev/null +++ b/thys/Real_Time_Deque/States_Aux.thy @@ -0,0 +1,88 @@ +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 + )" + +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 (reverseN 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 _) \ + size big - count = remained - size old \ count \ size small + | (_, Reverse1 _ _ _) \ False + | (Reverse _ _ _ _, _) \ 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,1201 +1,1201 @@ section "Big + Small Proofs" theory States_Proof -imports States Big_Proof Small_Proof +imports States_Aux Big_Proof Small_Proof begin 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))" 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.list big \ []" + 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 - reverseN_step[of "Stack.list big" count' auxB] + reverseN_step[of "Stack_Aux.list big" count' auxB] Stack_Proof.list_empty[symmetric, of small] by (cases currentB)(auto simp: first_hd funpow_swap1 reverseN_step reverseN_finish simp del: reverseN_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) 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"] 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) = (big', small')\ \ lists (States dir big (Small.push x small)) = (big', x # small')" by(induction "States dir big (Small.push x small)" rule: lists.induct) (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 _) \ size big - count = remained - size old \ count \ size small | (_, Reverse1 _ _ _) \ False | (Reverse _ _ _ _, _) \ False | _ \ True )" 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 _) \ size big - count = remained - size old \ count \ size small | (_, Reverse1 _ _ _) \ False | (Reverse _ _ _ _, _) \ 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) 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) next case 2 then show ?case by(auto split: Big.state.splits) qed next case 3 then show ?case 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) 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) next case (2 x current small auxS) then show ?case 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) 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)" by auto with 1 have invar_big: "invar big" using Big_Proof.invar_step[of "Reverse 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))"] 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"] 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 _)) \ size big - count = remained - size old \ count \ size small | (States _ _ (Reverse1 _ _ _)) \ False | (States _ (Reverse _ _ _ _) _) \ 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) 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) 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) 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) 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) 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 then show ?case by auto next case Common 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) next case "2_2" then show ?case 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) next case "2_4" then show ?case 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) next case "2_2" then show ?case by(auto split: Small.state.splits current.splits) next case "2_3" then show ?case by(auto split: current.splits Big.state.splits) next case "2_4" then show ?case 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) 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) next case (2 current aux new moved) then show ?case 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) next case 2 then show ?case by(auto split: Small.state.splits current.splits simp del: reverseN_def) 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) 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.list_current small @ rev (Big.list_current big)" + Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by auto then have "list_small_first (step (States Left big small)) = - Small.list_current small @ rev (Big.list_current big)" + 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.list_current small @ rev (Big.list_current big)" + 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.list_current big @ rev (Small.list_current 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.list_current big @ rev (Small.list_current 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.list_current big @ rev (Small.list_current 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; n < remaining_steps 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 | _ \ False) " by(cases states) (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))" using remaining_steps_idle[of "States dir big small"] by(cases big; cases small) (auto split!: Common.state.splits) end