src/HOL/Data_Structures/Queue_2Lists.thy

more robust;

(* Author: Tobias Nipkow *)

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

theory Queue_2Lists
imports Queue_Spec
begin

text \<open>Definitions:\<close>

type_synonym 'a queue = "'a list \<times> 'a list"

fun norm :: "'a queue \<Rightarrow> 'a queue" where
"norm (os,is) = (if os = [] then (rev is, []) else (os,is))"

fun enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
"enq a (os,is) = norm(os, a # is)"

fun deq :: "'a queue \<Rightarrow> 'a queue" where
"deq (os,is) = (if os = [] then (os,is) else norm(tl os,is))"

fun front :: "'a queue \<Rightarrow> 'a" where
"front (a # os,is) = a"

fun is_empty :: "'a queue \<Rightarrow> bool" where
"is_empty (os,is) = (os = [])"

fun list :: "'a queue \<Rightarrow> 'a list" where
"list (os,is) = os @ rev is"

fun invar :: "'a queue \<Rightarrow> bool" where
"invar (os,is) = (os = [] \<longrightarrow> is = [])"


text \<open>Implementation correctness:\<close>

interpretation Queue
where empty = "([],[])" and enq = enq and deq = deq and front = front
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)
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 \<Rightarrow> nat" where
"t_norm (os,is) = (if os = [] then length is else 0) + 1"

fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
"t_enq a (os,is) = t_norm(os, a # is)"

fun t_deq :: "'a queue \<Rightarrow> nat" where
"t_deq (os,is) = (if os = [] then 0 else t_norm(tl os,is)) + 1"

fun t_front :: "'a queue \<Rightarrow> nat" where
"t_front (a # os,is) = 1"

fun t_is_empty :: "'a queue \<Rightarrow> nat" where
"t_is_empty (os,is) = 1"

text \<open>Amortized running times:\<close>

fun \<Phi> :: "'a queue \<Rightarrow> nat" where
"\<Phi>(os,is) = length is"

lemma a_enq: "t_enq a (os,is) + \<Phi>(enq a (os,is)) - \<Phi>(os,is) \<le> 2"
by(auto)

lemma a_deq: "t_deq (os,is) + \<Phi>(deq (os,is)) - \<Phi>(os,is) \<le> 2"
by(auto)

end