Theory Collections.Fifo

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section ‹\isaheader{Fifo Queue by Pair of Lists}›
theory Fifo
imports 
  "../gen_algo/ListGA"
  "../tools/Record_Intf"
  "../tools/Locale_Code"
begin
text_raw ‹\label{thy:Fifo}›

(* TODO: Move to Misc *)
lemma rev_tl_rev: "rev (tl (rev l)) = butlast l"
  by (induct l) auto


(*@impl List
  @type 'a fifo
  @abbrv fifo
  Fifo-Queues implemented by two stacks.
*)

text ‹
  A fifo-queue is implemented by a pair of two lists (stacks). 
  New elements are pushed on the first stack, and elements are popped from 
  the second stack. If the second stack is empty, the first stack is reversed
  and replaces the second stack.

  If list reversal is implemented efficiently (what is the case in Isabelle/HOL, 
  cf @{thm [source] List.rev_conv_fold})
  the amortized time per buffer operation is constant.

  Moreover, this fifo implementation also supports efficient push and pop operations.
›

subsection ‹Definitions›
type_synonym 'a fifo = "'a list × 'a list"

text "Abstraction of the fifo to a list. The next element to be got is at 
      the head of the list, and new elements are appended at the end of the
      list"
definition fifo_α :: "'a fifo ⇒ 'a list" 
  where "fifo_α F == snd F @ rev (fst F)"

text "This fifo implementation has no invariants, any pair of lists is a 
  valid fifo"
definition [simp, intro!]: "fifo_invar x = True"


  ― ‹The empty fifo›
definition fifo_empty :: "unit ⇒ 'a fifo" 
  where "fifo_empty == λ_::unit. ([],[])"

  ― ‹True, iff the fifo is empty›
definition fifo_isEmpty :: "'a fifo ⇒ bool" where "fifo_isEmpty F == F=([],[])"

definition fifo_size :: "'a fifo ⇒ nat" where 
  "fifo_size F ≡ length (fst F) + length (snd F)"

  ― ‹Add an element to the fifo›
definition fifo_appendr :: "'a ⇒ 'a fifo ⇒ 'a fifo" 
  where "fifo_appendr a F == (a#fst F, snd F)"

definition fifo_appendl :: "'a ⇒ 'a fifo ⇒ 'a fifo"
  where "fifo_appendl x F == case F of (e,d) ⇒ (e,x#d)"

― ‹Get an element from the fifo›
definition fifo_remover :: "'a fifo ⇒ ('a fifo × 'a)" where 
  "fifo_remover F ==
    case fst F of
      (a#l) ⇒ ((l,snd F),a) |
      [] ⇒ let rp=rev (snd F) in
        ((tl rp,[]),hd rp)"

definition fifo_removel :: "'a fifo ⇒ ('a × 'a fifo)" where 
  "fifo_removel F ==
    case snd F of
      (a#l) ⇒ (a, (fst F, l)) |
      [] ⇒ let rp=rev (fst F) in
        (hd rp, ([], tl rp))
"

definition fifo_leftmost :: "'a fifo ⇒ 'a" where
  "fifo_leftmost F ≡ case F of (_,x#_) ⇒ x | (l,[]) ⇒ last l"

definition fifo_rightmost :: "'a fifo ⇒ 'a" where
  "fifo_rightmost F ≡ case F of (x#_,_) ⇒ x | ([],l) ⇒ last l"

definition "fifo_iteratei F ≡ foldli (fifo_α F)"
definition "fifo_rev_iteratei F ≡ foldri (fifo_α F)"

definition "fifo_get F i ≡ 
  let
    l2 = length (snd F)
  in
    if i < l2 then 
      snd F!i 
    else
      (fst F)!(length (fst F) - Suc (i - l2))
  "

definition "fifo_set F i a ≡ case F of (f1,f2) ⇒
  let
    l2 = length f2
  in
    if i < l2 then 
      (f1,f2[i:=a])
    else
      (f1[length (fst F) - Suc (i - l2) := a],f2)"

subsection "Correctness"

lemma fifo_empty_impl: "list_empty fifo_α fifo_invar fifo_empty"
  apply (unfold_locales)
  by (auto simp add: fifo_α_def fifo_empty_def)

lemma fifo_isEmpty_impl: "list_isEmpty fifo_α fifo_invar fifo_isEmpty"
  apply (unfold_locales)
  by (case_tac s) (auto simp add: fifo_isEmpty_def fifo_α_def)

lemma fifo_size_impl: "list_size fifo_α fifo_invar fifo_size"
  apply unfold_locales
  by (auto simp add: fifo_size_def fifo_α_def)
  
lemma fifo_appendr_impl: "list_appendr fifo_α fifo_invar fifo_appendr"
  apply (unfold_locales)
  by (auto simp add: fifo_appendr_def fifo_α_def)

lemma fifo_appendl_impl: "list_appendl fifo_α fifo_invar fifo_appendl"
  apply (unfold_locales)
  by (auto simp add: fifo_appendl_def fifo_α_def)

lemma fifo_removel_impl: "list_removel fifo_α fifo_invar fifo_removel"
  apply (unfold_locales)
  apply (case_tac s)
  apply (case_tac b)
  apply (auto simp add: fifo_removel_def fifo_α_def Let_def) [2]
  apply (case_tac s)
  apply (case_tac "b")
  apply (auto simp add: fifo_removel_def fifo_α_def Let_def)
  done

lemma fifo_remover_impl: "list_remover fifo_α fifo_invar fifo_remover"
  apply (unfold_locales)
  unfolding fifo_remover_def fifo_α_def Let_def
  by (auto split: list.split simp: hd_rev rev_tl_rev butlast_append)

lemma fifo_leftmost_impl: "list_leftmost fifo_α fifo_invar fifo_leftmost"
  apply unfold_locales
  by (auto simp: fifo_leftmost_def fifo_α_def hd_rev split: list.split)

lemma fifo_rightmost_impl: "list_rightmost fifo_α fifo_invar fifo_rightmost"
  apply unfold_locales
  by (auto simp: fifo_rightmost_def fifo_α_def hd_rev split: list.split)

lemma fifo_get_impl: "list_get fifo_α fifo_invar fifo_get"
  apply unfold_locales
  apply (auto simp: fifo_α_def fifo_get_def Let_def nth_append rev_nth)
  done

lemma fifo_set_impl: "list_set fifo_α fifo_invar fifo_set"
  apply unfold_locales
  apply (auto simp: fifo_α_def fifo_set_def Let_def list_update_append
    rev_update)
  done

definition [icf_rec_def]: "fifo_ops ≡ ⦇
  list_op_α = fifo_α,
  list_op_invar = fifo_invar,
  list_op_empty = fifo_empty,
  list_op_isEmpty = fifo_isEmpty,
  list_op_size = fifo_size,
  list_op_appendl = fifo_appendl,
  list_op_removel = fifo_removel,
  list_op_leftmost = fifo_leftmost,
  list_op_appendr = fifo_appendr,
  list_op_remover = fifo_remover,
  list_op_rightmost = fifo_rightmost,
  list_op_get = fifo_get,
  list_op_set = fifo_set
  ⦈"

setup Locale_Code.open_block
interpretation fifo: StdList fifo_ops
  apply (rule StdList.intro)
  apply (simp_all add: icf_rec_unf)
  apply (rule 
    fifo_empty_impl
    fifo_isEmpty_impl
    fifo_size_impl
    fifo_appendl_impl
    fifo_removel_impl
    fifo_leftmost_impl
    fifo_appendr_impl
    fifo_remover_impl
    fifo_rightmost_impl
    fifo_get_impl
    fifo_set_impl)+
  done
interpretation fifo: StdList_no_invar fifo_ops
  by unfold_locales (simp add: icf_rec_unf)
setup Locale_Code.close_block
setup ‹ICF_Tools.revert_abbrevs "fifo"›

definition test_codegen where "test_codegen ≡ 
  (
    fifo.empty,
    fifo.isEmpty,
    fifo.size,
    fifo.appendl,
    fifo.removel,
    fifo.leftmost,
    fifo.appendr,
    fifo.remover,
    fifo.rightmost,
    fifo.get,
    fifo.set,
    fifo.iteratei,
    fifo.rev_iteratei
  )"

export_code test_codegen checking SML

end