(* Author: Tobias Nipkow *)
section \<open>Queue Implementation via 2 Lists\<close>
theory Queue_2Lists
imports
Queue_Spec
Reverse
begin
text \<open>Definitions:\<close>
type_synonym 'a queue = "'a list \<times> 'a list"
fun norm :: "'a queue \ 'a queue" where
"norm (fs,rs) = (if fs = [] then (itrev rs [], []) else (fs,rs))"
fun enq :: "'a \ 'a queue \ 'a queue" where
"enq a (fs,rs) = norm(fs, a # rs)"
fun deq :: "'a queue \ 'a queue" where
"deq (fs,rs) = (if fs = [] then (fs,rs) else norm(tl fs,rs))"
fun first :: "'a queue \ 'a" where
"first (a # fs,rs) = a"
fun is_empty :: "'a queue \ bool" where
"is_empty (fs,rs) = (fs = [])"
fun list :: "'a queue \ 'a list" where
"list (fs,rs) = fs @ rev rs"
fun invar :: "'a queue \ bool" where
"invar (fs,rs) = (fs = [] \ rs = [])"
text \<open>Implementation correctness:\<close>
interpretation Queue
where empty = "([],[])" and enq = enq and deq = deq and first = first
and is_empty = is_empty and list = list and invar = invar
proof (standard, goal_cases)
case 1 show ?case by (simp)
next
case (2 q) thus ?case by(cases q) (simp)
next
case (3 q) thus ?case by(cases q) (simp add: itrev_Nil)
next
case (4 q) thus ?case by(cases q) (auto simp: neq_Nil_conv)
next
case (5 q) thus ?case by(cases q) (auto)
next
case 6 show ?case by(simp)
next
case (7 q) thus ?case by(cases q) (simp)
next
case (8 q) thus ?case by(cases q) (simp)
qed
text \<open>Running times:\<close>
fun T_norm :: "'a queue \ nat" where
"T_norm (fs,rs) = (if fs = [] then T_itrev rs [] else 0) + 1"
fun T_enq :: "'a \ 'a queue \ nat" where
"T_enq a (fs,rs) = T_norm(fs, a # rs) + 1"
fun T_deq :: "'a queue \ nat" where
"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs)) + 1"
fun T_first :: "'a queue \ nat" where
"T_first (a # fs,rs) = 1"
fun T_is_empty :: "'a queue \ nat" where
"T_is_empty (fs,rs) = 1"
text \<open>Amortized running times:\<close>
fun \<Phi> :: "'a queue \<Rightarrow> nat" where
"\(fs,rs) = length rs"
lemma a_enq: "T_enq a (fs,rs) + \(enq a (fs,rs)) - \(fs,rs) \ 4"
by(auto simp: T_itrev)
lemma a_deq: "T_deq (fs,rs) + \(deq (fs,rs)) - \(fs,rs) \ 3"
by(auto simp: T_itrev)
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
