diff --git a/thys/Real_Time_Deque/Big_Aux.thy b/thys/Real_Time_Deque/Big_Aux.thy --- a/thys/Real_Time_Deque/Big_Aux.thy +++ b/thys/Real_Time_Deque/Big_Aux.thy @@ -1,73 +1,73 @@ theory Big_Aux imports Big Common_Aux begin text \\<^noindent> Functions: \<^descr> \size_new\: Returns the size that the deque end will have after the transformation is finished. \<^descr> \size\: 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 []) + let reversed = take_rev count (Stack_Aux.list big) @ aux in + extra @ (take_rev remained reversed) )" fun list_current :: "'a state \ 'a list" where "list_current (Common common) = Common_Aux.list_current common" | "list_current (Reverse current _ _ _) = Current_Aux.list current" 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)) + rev (take remained (take_rev 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,320 +1,322 @@ section "Big Proofs" theory Big_Proof imports Big_Aux Common_Proof begin lemma step_list [simp]: "invar big \ list (step big) = list big" proof(induction big rule: step_state.induct) 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_Aux.list big) aux)" + then have [simp]: "remained - Suc 0 < length (take_rev count (Stack_Aux.list big) @ aux)" by(auto simp: le_diff_conv) (* TODO: *) then have " \0 < size old; 0 < remained; added = 0; remained - count \ length aux; count \ size big; Stack_Aux.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack_Aux.list big)))) = rev (take (remained - count) aux) @ rev (take remained (rev (take count (Stack_Aux.list big))))\ \ hd (rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big)))) = (rev (take count (Stack_Aux.list big)) @ aux) ! (remained - Suc 0)" - by (smt (verit) Suc_pred hd_drop_conv_nth hd_rev hd_take last_snoc length_rev length_take min.absorb2 rev_append reverseN_def size_list_length take_append take_hd_drop) + by (smt (verit) Suc_pred hd_drop_conv_nth hd_rev hd_take last_snoc length_rev length_take min.absorb2 rev_append take_rev_def size_list_length take_append take_hd_drop) - with 1 have [simp]: "Stack.first old = reverseN count (Stack_Aux.list big) aux ! (remained - Suc 0)" + with 1 have [simp]: "Stack.first old = (take_rev count (Stack_Aux.list big) @ aux) ! (remained - Suc 0)" by(auto simp: take_hd_drop first_hd) from 1 show ?case - using reverseN_nth[of - "remained - Suc 0" "reverseN count (Stack_Aux.list big) aux" "Stack.first old" "[]" + using take_rev_nth[of + "remained - Suc 0" "take_rev count (Stack_Aux.list big) @ aux" "Stack.first old" "[]" ] by auto next case 2 then show ?case by auto qed lemma size_list [simp]: " \0 < size big; invar big; list big = []\ \ False" 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; 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_Aux.list old = rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))); take remained (rev (take (size old - size big) aux)) @ take (remained - min (length aux) (size old - size big)) (rev (take (size old) (rev (Stack_Aux.list big)))) = rev (take remained 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) + by(auto simp: take_rev_drop drop_rev) next case (3 current big aux count) then have "0 < size big" by(auto split: current.splits) then have big_not_empty: "Stack_Aux.list big \ []" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) with 3 have a: " rev (Stack_Aux.list big) @ aux = rev (Stack_Aux.list (Stack.pop big)) @ Stack.first big # aux" by(auto simp: rev_tl_hd first_hd split: current.splits) from 3 have "0 < size big" by(auto split: current.splits) from 3 big_not_empty have " - 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] + take_rev (Suc count) (Stack_Aux.list big) @ aux = + take_rev count (Stack_Aux.list (Stack.pop big)) @ (Stack.first big # aux)" + using take_rev_tl_hd[of "Suc count" "Stack_Aux.list big" aux] by(auto simp: Stack_Proof.list_not_empty split: current.splits) with 3 a show ?case by(auto split: current.splits) qed lemma invar_push: "invar big \ invar (push x big)" by(induction x big rule: push.induct)(auto simp: invar_push split: current.splits) (* TODO: *) lemma invar_pop: "\ 0 < size big; invar big; pop big = (x, big') \ \ invar big'" proof(induction big arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: invar_pop split: prod.splits) next case (2 current big aux count) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) have linarith: "\x y z. x - y \ z \ x - (Suc y) \ z" by linarith have a: " \remained \ count + length aux; 0 < remained; added = 0; x = Stack.first old; big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; count \ size big; Stack_Aux.list old = rev aux @ Stack_Aux.list big; take remained (rev aux) @ take (remained - length aux) (Stack_Aux.list big) = drop (count + length aux - remained) (rev aux) @ drop (count - remained) (take count (Stack_Aux.list big)); \ size old \ length aux + size big\ \ tl (rev aux @ Stack_Aux.list big) = rev aux @ Stack_Aux.list big" by (metis le_refl length_append length_rev size_list_length) - have b: "\remained \ length (reverseN count (Stack_Aux.list big) aux); 0 < size old; + have b: "\remained \ length (take_rev count (Stack_Aux.list big) @ aux); 0 < size old; 0 < remained; added = 0; x = Stack.first old; big' = Reverse (Current [] 0 (Stack.pop old) (remained - Suc 0)) big aux count; remained - count \ length aux; count \ size big; Stack_Aux.list old = drop (length aux - (size old - size big)) (rev aux) @ drop (size big - size old) (Stack_Aux.list big); take remained (drop (length aux - (size old - size big)) (rev aux)) @ take (remained + (length aux - (size old - size big)) - length aux) (drop (size big - size old) (Stack_Aux.list big)) = - drop (length (reverseN count (Stack_Aux.list big) aux) - remained) - (rev (reverseN count (Stack_Aux.list big) aux))\ + drop (length (take_rev count (Stack_Aux.list big) @ aux) - remained) + (rev (take_rev count (Stack_Aux.list big) @ aux))\ \ tl (drop (length aux - (size old - size big)) (rev aux) @ drop (size big - size old) (Stack_Aux.list big)) = drop (length aux - (size old - Suc (size big))) (rev aux) @ drop (Suc (size big) - size old) (Stack_Aux.list big)" apply(cases "size old - size big \ length aux"; cases "size old \ size big") by(auto simp: tl_drop_2 Suc_diff_le le_diff_conv le_refl a) - from 1 have "remained \ length (reverseN count (Stack_Aux.list big) aux)" + from 1 have "remained \ length (take_rev count (Stack_Aux.list big) @ aux)" by(auto) with 1 show ?case - apply(auto simp: rev_take take_tl drop_Suc Suc_diff_le tl_drop linarith simp del: reverseN_def) - using b by simp + apply(auto simp: rev_take take_tl drop_Suc Suc_diff_le tl_drop linarith simp del: take_rev_def) + using b + apply (metis \remained \ length (take_rev count (Stack_Aux.list big) @ aux)\ rev_append rev_take take_append) + by (smt (verit, del_insts) Nat.diff_cancel tl_append_if Suc_diff_le append_self_conv2 diff_add_inverse diff_diff_cancel diff_is_0_eq diff_le_mono drop_eq_Nil2 length_rev nle_le not_less_eq_eq plus_1_eq_Suc tl_drop_2) next case (2 x xs added old remained) then show ?case by auto qed qed lemma push_list_current [simp]: "list_current (push x big) = x # list_current big" by(induction x big rule: push.induct) auto lemma pop_list_current [simp]: "\invar big; 0 < size big; Big.pop big = (x, big')\ \ x # list_current big' = list_current big" proof(induction big arbitrary: x rule: pop.induct) case (1 state) then show ?case by(auto simp: pop_list_current split: prod.splits) next case (2 current big aux count) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "rev (take (size old - size big) aux) @ rev (take (size old) (rev (Stack_Aux.list big))) \ []" using order_less_le_trans[of 0 "size old" "size big"] order_less_le_trans[of 0 count "size big"] by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) with 1 show ?case by(auto simp: first_hd) next case (2 x xs added old remained) then show ?case by auto qed qed lemma list_current_size: "\0 < size big; list_current big = []; invar big\ \ False" proof(induction big rule: list_current.induct) case 1 then show ?case using list_current_size by simp next case (2 current uu uv uw) then show ?case apply(cases current) by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_empty) qed lemma step_size: "invar (big :: 'a state) \ size big = size (step big)" by(induction big rule: step_state.induct)(auto split: current.splits) lemma 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,64 +1,63 @@ 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> \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 \ + 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))" end diff --git a/thys/Real_Time_Deque/Common_Aux.thy b/thys/Real_Time_Deque/Common_Aux.thy --- a/thys/Real_Time_Deque/Common_Aux.thy +++ b/thys/Real_Time_Deque/Common_Aux.thy @@ -1,79 +1,79 @@ theory Common_Aux imports Common Current_Aux Idle_Aux begin text\ \<^noindent> Functions: \<^descr> \list\: List abstraction of the elements which this end will contain after the transformation is finished \<^descr> \list_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" +definition take_rev where +[simp]: "take_rev n xs = rev (take n xs)" 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" + = extra @ take_rev (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) + \ take remained (Stack_Aux.list old) = take (size old) (take_rev (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,473 +1,475 @@ section "Common Proofs" theory Common_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 take_rev_drop: "take_rev n xs @ acc = drop (length xs - n) (rev xs) @ acc" + unfolding take_rev_def using rev_take by blast -lemma reverseN_step: "xs \ [] \ reverseN n (tl xs) (hd xs # acc) = reverseN (Suc n) xs acc" +lemma take_rev_step: "xs \ [] \ take_rev n (tl xs) @ (hd xs # acc) = take_rev (Suc n) xs @ acc" by (simp add: take_Suc) -lemma reverseN_finish: "reverseN n [] acc = acc" - by (simp) +lemma take_rev_empty [simp]: "take_rev n [] = []" + 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 take_rev_tl_hd: + "0 < n \ xs \ [] \ take_rev n xs @ ys = take_rev (n - (Suc 0)) (tl xs) @ (hd xs #ys)" + by (simp add: take_rev_step del: take_rev_def) -lemma reverseN_nth: "n < length xs \ x = xs ! n \ x # reverseN n xs ys = reverseN (Suc n) xs ys" +lemma take_rev_nth: + "n < length xs \ x = xs ! n \ x # take_rev n xs @ ys = take_rev (Suc n) xs @ ys" by (simp add: take_Suc_conv_app_nth) lemma step_list [simp]: "invar common \ list (step common) = list common" proof(induction common rule: step_state.induct) 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) + by(auto simp: aux_not_empty take_rev_step Suc_diff_Suc simp del: take_rev_def) qed qed qed lemma step_list_current [simp]: "invar common \ list_current (step common) = list_current common" by(cases common)(auto split: current.splits) lemma push_list [simp]: "list (push x common) = x # list common" proof(induction x common rule: push.induct) case (1 x stack stackSize) then show ?case by auto next case (2 x current aux new moved) then show ?case by(induction x current rule: Current.push.induct) auto qed lemma invar_step: "invar (common :: 'a state) \ invar (step common)" proof(induction "common" rule: invar_state.induct) case (1 idle) then show ?case by auto next case (2 current aux new moved) then show ?case proof(cases current) case (Current extra added old remained) then show ?thesis proof(cases "aux = []") case True with 2 Current show ?thesis by auto next case False note AUX_NOT_EMPTY = False then show ?thesis proof(cases "remained \ Suc (length new)") case True with 2 Current False have "take (Suc (length new)) (Stack_Aux.list old) = take (size old) (hd aux # new)" by(auto simp: le_Suc_eq take_Cons') with 2 Current True show ?thesis by auto next case False with 2 Current AUX_NOT_EMPTY show ?thesis - by(auto simp: reverseN_step Suc_diff_Suc simp del: reverseN_def) + by(auto simp: take_rev_step Suc_diff_Suc simp del: take_rev_def) qed qed qed qed lemma invar_push: "invar common \ invar (push x common)" proof(induction x common rule: push.induct) case (1 x current stack stackSize) then show ?case proof(induction x current rule: Current.push.induct) case (1 x extra added old remained) then show ?case proof(induction x stack rule: Stack.push.induct) case (1 x left right) then show ?case by auto qed qed next case (2 x current aux new moved) then show ?case proof(induction x current rule: Current.push.induct) case (1 x extra added old remained) then show ?case by auto qed qed lemma invar_pop: "\ 0 < size common; invar common; pop common = (x, common') \ \ invar common'" proof(induction common arbitrary: x rule: pop.induct) case (1 current idle) then obtain idle' where idle: "Idle.pop idle = (x, idle')" by(auto split: prod.splits) obtain current' where current: "drop_first current = current'" by auto from 1 current idle show ?case using Idle_Proof.size_pop[of idle x idle', symmetric] size_new_pop[of current] size_pop_sub[of current _ current'] by(auto simp: Idle_Proof.invar_pop invar_pop eq_snd_iff take_tl size_not_empty) next case (2 current aux new moved) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case proof(cases "remained - Suc 0 \ length new") case True with 1 have [simp]: "0 < size old" "Stack_Aux.list old \ []" "aux \ []" "length new = remained - Suc 0" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) then have [simp]: "Suc 0 \ size old" by linarith from 1 have "0 < remained" by auto then have "take remained (Stack_Aux.list old) = hd (Stack_Aux.list old) # take (remained - Suc 0) (tl (Stack_Aux.list old))" by (metis Suc_pred \Stack_Aux.list old \ []\ list.collapse take_Suc_Cons) with 1 True show ?thesis using Stack_Proof.pop_list[of old] by(auto simp: Stack_Proof.size_not_empty) next case False with 1 have "remained - Suc 0 \ length aux + length new" by auto with 1 False show ?thesis using Stack_Proof.pop_list[of old] apply(auto simp: Suc_diff_Suc take_tl Stack_Proof.size_not_empty tl_append_if) by (simp add: Suc_diff_le rev_take tl_drop_2 tl_take) qed next case (2 x xs added old remained) then show ?case by auto qed qed lemma push_list_current [simp]: "list_current (push x left) = x # list_current left" by(induction x left rule: push.induct) auto lemma pop_list [simp]: "invar common \ 0 < size common \ pop common = (x, common') \ x # list common' = list common" proof(induction common arbitrary: x rule: pop.induct) case 1 then show ?case by(auto simp: size_not_empty split: prod.splits) next case (2 current aux new moved) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then show ?case proof(cases "remained - Suc 0 \ length new") case True from 1 True have [simp]: "aux \ []" "0 < remained" "Stack_Aux.list old \ []" "remained - length new = 1" by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) then have "take remained (Stack_Aux.list old) = hd aux # take (size old - Suc 0) new \ Stack.first old = hd aux" by (metis first_hd hd_take list.sel(1)) with 1 True take_hd[of aux] show ?thesis by(auto simp: Suc_leI) next case False then show ?thesis proof(cases "remained - length new = length aux") case True then have length_minus_1: "remained - Suc (length new) = length aux - 1" by simp from 1 have not_empty: "0 < remained" "0 < size old" "aux \ []" "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) from 1 True not_empty have "take 1 (Stack_Aux.list old) = take 1 (rev aux)" using take_1[of remained "size old" "Stack_Aux.list old" "(rev aux) @ take (size old + length new - remained) new" ] by(simp) then have "[last aux] = [Stack.first old]" using take_last first_take not_empty by fastforce then have "last aux = Stack.first old" by auto with 1 True False show ?thesis using not_empty last_drop_rev[of aux] - by(auto simp: reverseN_drop length_minus_1 simp del: reverseN_def) + by(auto simp: take_rev_drop length_minus_1 simp del: take_rev_def) next case False with 1 have a: "take (remained - length new) aux \ []" by auto from 1 False have b: "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) from 1 have c: "remained - Suc (length new) < length aux" by auto from 1 have not_empty: "0 < remained" "0 < size old" "0 < remained - length new" "0 < length aux" by auto with False have "take remained (Stack_Aux.list old) = - take (size old) (reverseN (remained - length new) aux new) + take (size old) (take_rev (remained - length new) aux @ new) \ take (Suc 0) (Stack_Aux.list old) = take (Suc 0) (rev (take (remained - length new) aux))" using take_1[of remained "size old" "Stack_Aux.list old" - " (reverseN (remained - length new) aux new)" + " (take_rev (remained - length new) aux @ new)" ] by(auto simp: not_empty Suc_le_eq) with 1 False have "take 1 (Stack_Aux.list old) = take 1 (rev (take (remained - length new) aux))" by auto then have d: "[Stack.first old] = [last (take (remained - length new) aux)]" using take_last first_take a b by metis have "last (take (remained - length new) aux) # rev (take (remained - Suc (length new)) aux) = rev (take (remained - length new) aux)" using Suc_diff_Suc c not_empty by (metis a drop_drop last_drop_rev plus_1_eq_Suc rev_take zero_less_diff) with 1(1) 1(3) False not_empty d show ?thesis by(cases "remained - length new = 1") (auto) qed qed next case 2 then show ?case by auto qed qed lemma pop_list_current: "invar common \ 0 < size common \ pop common = (x, common') \ x # list_current common' = list_current common" proof(induction common arbitrary: x rule: pop.induct) case (1 current idle) then show ?case proof(induction idle rule: Idle.pop.induct) case (1 stack stackSize) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "Stack.first old = Stack.first stack" using take_first[of old stack] by auto with 1 show ?case by(auto simp: Stack_Proof.size_not_empty Stack_Proof.list_not_empty) next case (2 x xs added old remained) then have "0 < size stack" by auto with Stack_Proof.size_not_empty Stack_Proof.list_not_empty have not_empty: "\ is_empty stack" "Stack_Aux.list stack \ []" by auto with 2 have "hd (Stack_Aux.list stack) = x" using take_hd'[of "Stack_Aux.list stack" x "xs @ Stack_Aux.list old"] by auto with 2 show ?case using first_list[of stack] not_empty by auto qed qed next case (2 current) then show ?case proof(induction current rule: Current.pop.induct) case (1 added old remained) then have "\ is_empty old" by(auto simp: Stack_Proof.size_not_empty) with 1 show ?case using first_pop by(auto simp: Stack_Proof.list_not_empty) next case 2 then show ?case by auto qed qed lemma list_current_size [simp]: "\0 < size common; list_current common = []; invar common\ \ False" proof(induction common rule: invar_state.induct) case 1 then show ?case using list_size by auto next case (2 current) then have "invar current" "Current_Aux.list current = []" "0 < size current" by(auto split: current.splits) then show ?case using list_size by auto qed lemma list_size [simp]: "\0 < size common; list common = []; invar common\ \ False" proof(induction common rule: invar_state.induct) case 1 then show ?case using list_size Idle_Proof.size_empty by auto next case (2 current aux new moved) then have "invar current" "Current_Aux.list current = []" "0 < size current" by(auto split: current.splits) then show ?case using list_size by auto qed lemma step_size [simp]: "invar (common :: 'a state) \ size (step common) = size common" proof(induction common rule: step_state.induct) 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,30 +1,32 @@ section \Current Stack\ theory Current imports Stack begin text \ \noindent This data structure is composed of: \<^item> the newly added elements to one end of a deque during the transformation phase \<^item> the 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 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)" + "pop (Current [] added old remained) = + (first old, Current [] added (Stack.pop old) (remained - 1))" +| "pop (Current (x#xs) added old remained) = + (x, Current xs (added - 1) old remained)" fun first :: "'a current \ 'a" where "first current = fst (pop current)" abbreviation drop_first :: "'a current \ 'a current" where "drop_first current \ snd (pop current)" end diff --git a/thys/Real_Time_Deque/RTD_Util.thy b/thys/Real_Time_Deque/RTD_Util.thy --- a/thys/Real_Time_Deque/RTD_Util.thy +++ b/thys/Real_Time_Deque/RTD_Util.thy @@ -1,62 +1,58 @@ section \Basic Lemma Library\ theory RTD_Util imports Main begin -(* remove - is in Isabelle after 2021-1 *) -lemma tl_append_if: "tl (xs @ ys) = (if xs = [] then tl ys else tl xs @ ys)" - by (simp) - lemma take_last_length: "\take (Suc 0) (rev xs) = [last xs]\ \ Suc 0 \ length xs" by(induction xs) auto lemma take_last: "xs \ [] \ take 1 (rev xs) = [last xs]" by(induction xs)(auto simp: take_last_length) lemma take_hd [simp]: "xs \ [] \ take (Suc 0) xs = [hd xs]" by(induction xs) auto lemma cons_tl: "x # xs = ys \ xs = tl ys" by auto lemma cons_hd: "x # xs = ys \ x = hd ys" by auto lemma take_hd': "ys \ [] \ take (size ys) (x # xs) = take (Suc (size xs)) ys \ hd ys = x" by(induction ys) auto lemma rev_app_single: "rev xs @ [x] = rev (x # xs)" by auto lemma hd_drop_1 [simp]: "xs \ [] \ hd xs # drop (Suc 0) xs = xs" by(induction xs) auto lemma hd_drop [simp]: "n < length xs \ hd (drop n xs) # drop (Suc n) xs = drop n xs" by(induction xs)(auto simp: list.expand tl_drop) lemma take_1: "0 < x \ 0 < y \ take x xs = take y ys \ take 1 xs = take 1 ys" by (metis One_nat_def bot_nat_0.not_eq_extremum hd_take take_Suc take_eq_Nil) lemma last_drop_rev: "xs \ [] \ last xs # drop 1 (rev xs) = rev xs" by (metis One_nat_def hd_drop_1 hd_rev rev.simps(1) rev_rev_ident) lemma Suc_min [simp]: "0 < x \ 0 < y \ Suc (min (x - Suc 0) (y - Suc 0)) = min x y" by auto lemma rev_tl_hd: "xs \ [] \ rev (tl xs) @ [hd xs] = rev xs" by (simp add: rev_app_single) lemma app_rev: "as @ rev bs = cs @ rev ds \ bs @ rev as = ds @ rev cs" by (metis rev_append rev_rev_ident) lemma tl_drop_2: "tl (drop n xs) = drop (Suc n) xs" by (simp add: drop_Suc tl_drop) lemma Suc_sub: "Suc n = m \ n = m - 1" by simp lemma length_one_hd: "length xs = 1 \ xs = [hd xs]" by(induction xs) auto end diff --git a/thys/Real_Time_Deque/RealTimeDeque.thy b/thys/Real_Time_Deque/RealTimeDeque.thy --- a/thys/Real_Time_Deque/RealTimeDeque.thy +++ b/thys/Real_Time_Deque/RealTimeDeque.thy @@ -1,192 +1,192 @@ section \Real-Time Deque Implementation\ theory RealTimeDeque imports States begin text\ The real-time deque can be in the following states: \<^descr> \Empty\: No values stored. No dequeue operation possible. \<^descr> \One\: One element in the deque. \<^descr> \Two\: Two elements in the deque. \<^descr> \Three\: Three elements in the deque. \<^descr> \Idle\: Deque with a left and a right end, fulfilling the following invariant: \<^item> 3 * size of left end \\\ size of right end \<^item> 3 * size of right end \\\ size of left end \<^item> Neither of the ends is empty \<^descr> \Transforming\: Deque which violated the invariant of the \idle\ state by non-balanced dequeue and enqueue operations. The invariants during in this state are: \<^item> The transformation is not done yet. The deque needs to be in \idle\ state otherwise. \<^item> The transformation is in a valid state (Defined in theory \States\) \<^item> The two ends of the deque are in a size window, such that after finishing the transformation the invariant of the \idle\ state will be met. 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" + "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 )" end diff --git a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy --- a/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy +++ b/thys/Real_Time_Deque/RealTimeDeque_Dequeue_Proof.thy @@ -1,471 +1,471 @@ section "Dequeue Proofs" theory RealTimeDeque_Dequeue_Proof imports Deque RealTimeDeque_Aux States_Proof begin lemma list_deqL' [simp]: "\invar deque; listL deque \ []; deqL' deque = (x, deque')\ \ x # listL deque' = listL deque" proof(induction deque arbitrary: x rule: deqL'.induct) case (4 left right length_right) then obtain left' where pop_left[simp]: "Idle.pop left = (x, left')" by(auto simp: Let_def split: if_splits stack.splits prod.splits idle.splits) then obtain stack_left' length_left' where left'[simp]: "left' = idle.Idle stack_left' length_left'" using idle.exhaust by blast from 4 have invar_left': "invar left'" using Idle_Proof.invar_pop[of left] by auto then have size_left' [simp]: "size stack_left' = length_left'" by auto have size_left'_size_left [simp]: "size stack_left' = (size left) - 1" using Idle_Proof.size_pop_sub[of left x left'] by auto show ?case proof(cases "3 * length_left' \ length_right") case True with 4 pop_left show ?thesis using Idle_Proof.pop_list[of left x left'] by auto next case False note Start_Transformation = False 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) + by (auto simp del: take_rev_def) with invar have "States_Aux.listL ((step^^6) ?states) = tl (Idle_Aux.list left) @ rev (Stack_Aux.list right)" using step_n_listL[of ?states 6] by presburger with 4 Start_Transformation True show ?thesis 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/Small_Aux.thy b/thys/Real_Time_Deque/Small_Aux.thy --- a/thys/Real_Time_Deque/Small_Aux.thy +++ b/thys/Real_Time_Deque/Small_Aux.thy @@ -1,68 +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)" + extra @ (take_rev (remained - (count + size big)) aux) @ (rev (Stack_Aux.list big) @ new)" fun list_current :: "'a state \ 'a list" where "list_current (Common common) = Common_Aux.list_current common" | "list_current (Reverse2 current _ _ _ _) = Current_Aux.list current" | "list_current (Reverse1 current _ _) = Current_Aux.list current" 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/Stack.thy b/thys/Real_Time_Deque/Stack.thy --- a/thys/Real_Time_Deque/Stack.thy +++ b/thys/Real_Time_Deque/Stack.thy @@ -1,35 +1,34 @@ 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.\ +It has the operations \push\, \pop\ and \first\.\ datatype (plugins del: size) 'a stack = Stack "'a list" "'a list" 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" instantiation stack ::(type) is_empty begin fun is_empty_stack where "is_empty_stack (Stack [] []) = True" | "is_empty_stack _ = False" 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 --- a/thys/Real_Time_Deque/Stack_Aux.thy +++ b/thys/Real_Time_Deque/Stack_Aux.thy @@ -1,17 +1,19 @@ theory Stack_Aux imports Stack begin +text\The function \list\ appends the two lists and is needed for the list abstraction of the deque.\ + 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/States_Aux.thy b/thys/Real_Time_Deque/States_Aux.thy --- a/thys/Real_Time_Deque/States_Aux.thy +++ b/thys/Real_Time_Deque/States_Aux.thy @@ -1,88 +1,89 @@ 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 + | 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) + Small_Aux.list (Reverse2 currentS (take_rev count (Stack_Aux.list small) @ auxS) ((Stack.pop ^^ count) big) [] 0) )" | "lists (States _ big small) = (Big_Aux.list big, Small_Aux.list small)" fun list_small_first :: "'a states \ 'a list" where "list_small_first states = (let (big, small) = lists states in small @ (rev big))" fun list_big_first :: "'a states \ 'a list" where "list_big_first states = (let (big, small) = lists states in big @ (rev small))" fun lists_current :: "'a states \ 'a list * 'a list" where "lists_current (States _ big small) = (Big_Aux.list_current big, Small_Aux.list_current small)" fun list_current_small_first :: "'a states \ 'a list" where "list_current_small_first states = (let (big, small) = lists_current states in small @ (rev big))" fun list_current_big_first :: "'a states \ 'a list" where "list_current_big_first states = (let (big, small) = lists_current states in big @ (rev small))" fun listL :: "'a states \ 'a list" where "listL (States Left big small) = list_small_first (States Left big small)" | "listL (States Right big small) = list_big_first (States Right big small)" instantiation states::(type) invar begin fun invar_states :: "'a states \ bool" where "invar (States dir big small) \ ( invar big \ invar small \ list_small_first (States dir big small) = list_current_small_first (States dir big small) \ (case (big, small) of (Reverse _ big _ count, Reverse1 (Current _ _ old remained) small _) \ 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,1202 @@ section "Big + Small Proofs" theory States_Proof imports States_Aux Big_Proof Small_Proof begin lemmas state_splits = idle.splits Common.state.splits Small.state.splits Big.state.splits lemmas 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_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_Aux.list big" count' auxB] + take_rev_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) + apply (cases currentB) + by(auto simp: first_hd funpow_swap1 take_rev_step simp del: take_rev_def) qed next case ("2_1" dir common small) then show ?case using Small_Proof.step_list_reverse2[of small] by(auto split: Small.state.splits) 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) + by(auto split: Small.state.splits current.splits) qed qed lemma remaining_steps_push_big [simp]: "invar (States dir big small) \ remaining_steps (States dir (Big.push x big) small) = remaining_steps (States dir big small)" by(induction x big rule: Big.push.induct)(auto split: Small.state.splits current.splits) lemma step_4_remaining_steps_push_big [simp]: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'\ \ remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big ) lemma step_4_remaining_steps_push_small [simp]: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small' \ \ remaining_steps (States dir' big' small') = remaining_steps (States dir big small) - 4" by (metis invar_push_small remaining_steps_n_steps_sub remaining_steps_push_small) lemma step_4_remaining_steps_pop_big: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); (step^^4) (States dir bigP small) = States dir' big' small' \ \ remaining_steps (States dir' big' small') \ remaining_steps (States dir big small) - 4" by (metis add_le_imp_le_diff invar_pop_big remaining_steps_pop_big remaining_steps_n_steps_plus) lemma step_4_remaining_steps_pop_small: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small' \ \ remaining_steps (States dir' big' small') \ remaining_steps (States dir big small) - 4" by (metis add_le_imp_le_diff invar_pop_small remaining_steps_n_steps_plus remaining_steps_pop_small) lemma step_4_pop_small_size_ok_1: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) add.left_commute add.right_neutral add_le_cancel_left distrib_left_numeral dual_order.trans invar_pop_small le_add_diff_inverse2 mult.right_neutral plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_small) lemma step_4_pop_big_size_ok_1: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); (step^^4) (States dir bigP small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) add_leE add_le_cancel_right invar_pop_big order_trans remaining_steps_pop_big step_n_size_small remaining_steps_n_steps_plus) lemma step_4_pop_small_size_ok_2: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); (step^^4) (States dir big smallP) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (smt (z3) add.commute add_leE invar_pop_small le_add_diff_inverse2 nat_add_left_cancel_le remaining_steps_n_steps_sub step_n_size_big remaining_steps_pop_small) lemma step_4_pop_big_size_ok_2: assumes "invar (States dir big small)" "0 < size big" "Big.pop big = (x, bigP)" "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = States dir' big' small'" "remaining_steps (States dir big small) + 1 \ 4 * size big" shows "remaining_steps (States dir' big' small') + 1 \ 4 * size big'" proof - from assms have "remaining_steps (States dir bigP small) + 1 \ 4 * size big" by (meson add_le_cancel_right order.trans remaining_steps_pop_big) with assms show ?thesis by (smt (z3) Suc_diff_le Suc_eq_plus1 add_mult_distrib2 diff_diff_add diff_is_0_eq invar_pop_big mult_numeral_1_right numerals(1) plus_1_eq_Suc remaining_steps_n_steps_sub step_n_pop_size_big) qed lemma step_4_pop_small_size_ok_3: assumes "invar (States dir big small)" "0 < size small" "Small.pop small = (x, smallP)" "remaining_steps (States dir big smallP) \ 4" "((step ^^ 4) (States dir big smallP)) = States dir' big' small'" "size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big" shows "size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" by (smt (verit, best) add_leD2 add_mono_thms_linordered_semiring(1) add_mono_thms_linordered_semiring(3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) invar_pop_small le_add2 le_add_diff_inverse order_trans plus_1_eq_Suc remaining_steps_n_steps_sub remaining_steps_pop_small step_n_pop_size_new_small step_n_size_new_big) lemma step_4_pop_big_size_ok_3_aux: "\ 0 < size big; 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new big - 1)" by linarith lemma step_4_pop_big_size_ok_3: assumes "invar (States dir big small)" "0 < size big" "Big.pop big = (x, bigP) " "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')" "size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big" shows "size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" proof- from assms have "size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new big - 1)" by (meson dual_order.trans remaining_steps_pop_big step_4_pop_big_size_ok_3_aux) then have "size_new small + remaining_steps (States dir' big' small') + 2 \ 3 * (size_new big - 1)" by (smt (verit, ccfv_SIG) add_le_mono assms(1) assms(2) assms(3) assms(4) assms(5) dual_order.trans le_antisym less_or_eq_imp_le nat_less_le step_4_remaining_steps_pop_big) with assms show ?thesis by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big) qed lemma step_4_pop_small_size_ok_4_aux: "\ 0 < size small; 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new small - 1)" by linarith lemma step_4_pop_small_size_ok_4: assumes "invar (States dir big small)" "0 < size small" "Small.pop small = (x, smallP)" "remaining_steps (States dir big smallP) \ 4" "((step ^^ 4) (States dir big smallP)) = (States dir' big' small')" "size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small" shows "size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" proof- from assms step_4_pop_small_size_ok_4_aux have "size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * (size_new small - 1)" by (smt (verit, best) add_leE le_add_diff_inverse remaining_steps_pop_small) with assms have "size_new big + remaining_steps (States dir' big' small') + 2 \ 3 * (size_new small - 1)" by (smt (verit, best) add_le_cancel_left add_mono_thms_linordered_semiring(3) diff_le_mono invar_pop_small order_trans remaining_steps_n_steps_sub remaining_steps_pop_small) with assms show ?thesis by (metis diff_Suc_1 invar_pop_small step_n_size_new_big step_n_pop_size_new_small) qed lemma step_4_pop_big_size_ok_4_aux: "\ 0 < size big; 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big - 1 + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" by linarith lemma step_4_pop_big_size_ok_4: assumes "invar (States dir big small)" "0 < size big " "Big.pop big = (x, bigP)" "remaining_steps (States dir bigP small) \ 4" "((step ^^ 4) (States dir bigP small)) = (States dir' big' small')" "size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small" shows "size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" proof - from assms step_4_pop_big_size_ok_4_aux have "(size_new big - 1) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" by linarith with assms have "(size_new big - 1) + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small" by (meson add_le_mono dual_order.eq_iff order_trans step_4_remaining_steps_pop_big) with assms show ?thesis by (metis diff_Suc_1 invar_pop_big step_n_size_new_small step_n_pop_size_new_big) qed lemma step_4_push_small_size_ok_1: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (z3) add.commute add_leD1 add_le_mono le_add1 le_add_diff_inverse2 mult_Suc_right nat_1_add_1 numeral_Bit0 step_n_push_size_small step_4_remaining_steps_push_small) lemma step_4_push_big_size_ok_1: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size small \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size small'" by (smt (verit, ccfv_SIG) Nat.le_diff_conv2 add_leD2 invar_push_big le_add1 le_add_diff_inverse2 remaining_steps_n_steps_sub remaining_steps_push_big step_n_size_small) lemma step_4_push_small_size_ok_2: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (metis (full_types) Suc_diff_le Suc_eq_plus1 invar_push_small less_Suc_eq_le less_imp_diff_less step_4_remaining_steps_push_small step_n_size_big) lemma step_4_push_big_size_ok_2: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; remaining_steps (States dir big small) + 1 \ 4 * size big \ \ remaining_steps (States dir' big' small') + 1 \ 4 * size big'" by (smt (verit, ccfv_SIG) add.commute add_diff_cancel_left' add_leD1 add_le_mono invar_push_big mult_Suc_right nat_le_iff_add one_le_numeral remaining_steps_n_steps_sub remaining_steps_push_big step_n_push_size_big) lemma step_4_push_small_size_ok_3_aux: "\ 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ Suc (size_new small) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new big" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_small_size_ok_3: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" using step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small by (metis invar_push_small step_4_push_small_size_ok_3_aux) lemma step_4_push_big_size_ok_3_aux: "\ 4 \ remaining_steps (States dir big small); size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small + (remaining_steps (States dir big small) - 4) + 2 \ 3 * Suc (size_new big)" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_big_size_ok_3: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; size_new small + remaining_steps (States dir big small) + 2 \ 3 * size_new big \ \ size_new small' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new big'" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_3_aux step_n_push_size_new_big step_n_size_new_small) lemma step_4_push_small_size_ok_4_aux: "\ 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big + (remaining_steps (States dir big small) - 4) + 2 \ 3 * Suc (size_new small)" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_small_size_ok_4: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir big (Small.push x small)) = States dir' big' small'; size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" by (metis invar_push_small step_n_size_new_big step_n_push_size_new_small step_4_remaining_steps_push_small step_4_push_small_size_ok_4_aux) lemma step_4_push_big_size_ok_4_aux: "\ 4 \ remaining_steps (States dir big small); size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ Suc (size_new big) + (remaining_steps (States dir big small) - 4) + 2 \ 3 * size_new small" using distrib_left dual_order.trans le_add_diff_inverse2 by force lemma step_4_push_big_size_ok_4: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); (step^^4) (States dir (Big.push x big) small) = States dir' big' small'; size_new big + remaining_steps (States dir big small) + 2 \ 3 * size_new small \ \ size_new big' + remaining_steps (States dir' big' small') + 2 \ 3 * size_new small'" by (metis invar_push_big remaining_steps_n_steps_sub remaining_steps_push_big step_4_push_big_size_ok_4_aux step_n_push_size_new_big step_n_size_new_small) lemma step_4_push_small_size_ok: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir big (Small.push x small)))" using step_4_push_small_size_ok_1 step_4_push_small_size_ok_2 step_4_push_small_size_ok_3 step_4_push_small_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma step_4_push_big_size_ok: "\ invar (States dir big small); 4 \ remaining_steps (States dir big small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir (Big.push x big) small))" using step_4_push_big_size_ok_1 step_4_push_big_size_ok_2 step_4_push_big_size_ok_3 step_4_push_big_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma step_4_pop_small_size_ok: "\ invar (States dir big small); 0 < size small; Small.pop small = (x, smallP); 4 \ remaining_steps (States dir big smallP); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir big smallP))" by (smt (verit) size_ok'.elims(3) size_ok'.simps step_4_pop_small_size_ok_1 step_4_pop_small_size_ok_2 step_4_pop_small_size_ok_3 step_4_pop_small_size_ok_4) lemma step_4_pop_big_size_ok: "\ invar (States dir big small); 0 < size big; Big.pop big = (x, bigP); 4 \ remaining_steps (States dir bigP small); size_ok (States dir big small) \ \ size_ok ((step^^4) (States dir bigP small))" using step_4_pop_big_size_ok_1 step_4_pop_big_size_ok_2 step_4_pop_big_size_ok_3 step_4_pop_big_size_ok_4 by (smt (verit) size_ok'.elims(3) size_ok'.simps) lemma size_ok_size_small: "size_ok (States dir big small) \ 0 < size small" by auto lemma size_ok_size_big: "size_ok (States dir big small) \ 0 < size big" by auto lemma size_ok_size_new_small: "size_ok (States dir big small) \ 0 < size_new small" by auto lemma size_ok_size_new_big: "size_ok (States dir big small) \ 0 < size_new big" by auto lemma step_size_ok': "\invar states; size_ok' states n\ \ size_ok' (step states) n" by (smt (verit, ccfv_SIG) size_ok'.elims(2) size_ok'.elims(3) step_size_big step_size_new_big step_size_new_small step_size_small) lemma step_same: "step (States dir big small) = States dir' big' small' \ dir = dir'" by(induction "States dir big small" rule: step_states.induct) auto lemma step_n_same: "(step^^n) (States dir big small) = States dir' big' small' \ dir = dir'" proof(induction n arbitrary: big small big' small') case 0 then show ?case by simp next case (Suc n) obtain big'' small'' where "step (States dir big small) = States dir big'' small''" by (metis states.exhaust step_same) with Suc show ?case by(auto simp: funpow_swap1) qed lemma step_listL: "invar states \ listL (step states) = listL states" proof(induction states rule: listL.induct) case (1 big small) then have "list_small_first (States Left big small) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by auto then have "list_small_first (step (States Left big small)) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" using 1 step_lists by fastforce then have "listL (step (States Left big small)) = Small_Aux.list_current small @ rev (Big_Aux.list_current big)" by (smt (verit, ccfv_SIG) "1" invar_states.elims(2) States_Proof.invar_step listL.simps(1) step_same) with 1 show ?case by auto next case (2 big small) then have a: "list_big_first (States Right big small) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using invar_list_big_first[of "States Right big small"] by auto then have "list_big_first (step (States Right big small)) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" using 2 step_lists by fastforce then have "listL (step (States Right big small)) = Big_Aux.list_current big @ rev (Small_Aux.list_current small)" by (metis(full_types) listL.cases listL.simps(2) step_same) with 2 show ?case using a by force qed lemma step_n_listL: "invar states \ listL ((step^^n) states) = listL states" using step_consistent[of listL states] step_listL by metis lemma listL_remaining_steps: assumes "listL states = []" "0 < remaining_steps states" "invar states" "size_ok states" shows "False" proof(cases states) case (States dir big small) with assms show ?thesis using Small_Proof.list_current_size size_ok_size_small by(cases dir; cases "lists (States dir big small)") auto qed lemma invar_step_n: "invar (states :: 'a states) \ invar ((step^^n) states)" by (simp add: invar_step step_consistent_2) lemma step_n_size_ok': "\invar states; size_ok' states x\ \ size_ok' ((step ^^ n) states) x" proof(induction n arbitrary: states x) case 0 then show ?case by auto next case Suc then show ?case using invar_step_n step_size_ok' by fastforce qed lemma size_ok_steps: "\ invar states; 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