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 ?caseby (simp) next case (2 q) thus ?caseby(cases q) (simp) next case (3 q) thus ?caseby(cases q) (simp add: itrev_Nil) next case (4 q) thus ?caseby(cases q) (auto simp: neq_Nil_conv) next case (5 q) thus ?caseby(cases q) (auto) next case 6 show ?caseby(simp) next case (7 q) thus ?caseby(cases q) (simp) next case (8 q) thus ?caseby(cases q) (simp) qed
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.
