Aded Queues

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Wed Oct 07 17:34:24 2020 +0200
@@ -0,0 +1,86 @@
+(* 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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Queue_Spec.thy	Wed Oct 07 17:34:24 2020 +0200
@@ -0,0 +1,28 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>Queue Specification\<close>
+
+theory Queue_Spec
+imports Main
+begin
+
+text \<open>The basic queue interface with \<open>list\<close>-based specification:\<close>
+
+locale Queue =
+fixes empty :: "'q"
+fixes enq :: "'a \<Rightarrow> 'q \<Rightarrow> 'q"
+fixes front :: "'q \<Rightarrow> 'a"
+fixes deq :: "'q \<Rightarrow> 'q"
+fixes is_empty :: "'q \<Rightarrow> bool"
+fixes list :: "'q \<Rightarrow> 'a list"
+fixes invar :: "'q \<Rightarrow> bool"
+assumes list_empty:    "list empty = []"
+assumes list_enq:      "invar q \<Longrightarrow> list(enq x q) = list q @ [x]"
+assumes list_deq:      "invar q \<Longrightarrow> list(deq q) = tl(list q)"
+assumes list_front:    "invar q \<Longrightarrow> \<not> list q = [] \<Longrightarrow> front q = hd(list q)"
+assumes list_is_empty: "invar q \<Longrightarrow> is_empty q = (list q = [])"
+assumes invar_empty:   "invar empty"
+assumes invar_enq:     "invar q \<Longrightarrow> invar(enq x q)"
+assumes invar_deq:     "invar q \<Longrightarrow> invar(deq q)"
+
+end

--- a/src/HOL/ROOT	Wed Oct 07 10:39:14 2020 +0200
+++ b/src/HOL/ROOT	Wed Oct 07 17:34:24 2020 +0200
@@ -282,6 +282,7 @@
     Trie_Fun
     Trie_Map
     Tries_Binary
+    Queue_2Lists
     Leftist_Heap
     Binomial_Heap
   document_files "root.tex" "root.bib"