(* Author: Tobias Nipkow *)

section ‹Queue Implementation via 2 Lists›

theory Queue_2Lists
imports
  Queue_Spec
  "HOL-Library.Time_Functions"
begin

text ‹Definitions:›

type_synonym 'a queue = "'a list × '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 ‹Implementation correctness:›

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 ‹Running times:›

time_fun norm
time_fun enq
time_fun deq

text ‹Amortized running times:›

fun Φ :: "'a queue → 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