Quelle Queue_2Lists.thy Sprache: Isabelle

(* Author: Tobias Nipkow *)

section \<open>Queue Implementation via 2 Lists\<close>

theory Queue_2Lists
imports
  Queue_Spec
  "HOL-Library.Time_Functions"
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>

time_fun norm
time_fun enq
time_fun deq

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) \ 2"
by(auto simp: T_itrev)

lemma a_deq: "T_deq (fs,rs) + \(deq (fs,rs)) - \(fs,rs) \ 1"
by(auto simp: T_itrev T_tl)

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.