Theory ListSpec

header {* \isaheader{Specification of Sequences} *}
theory ListSpec 
imports Main 
  "../common/Misc" 
  "../iterator/SetIteratorOperations" 
  "../iterator/SetIteratorGA"
begin

(*@intf List
  @abstype 'a list
  This interface specifies sequences.
*)

subsection "Definition"
locale list =
  -- "Abstraction to HOL-lists"
  fixes α :: "'s => 'x list"
  -- "Invariant"
  fixes invar :: "'s => bool"

subsection "Functions"

locale list_empty = list +
  constrains α :: "'s => 'x list"
  fixes empty :: "unit => 's"
  assumes empty_correct:
    "α (empty ()) = []"
    "invar (empty ())"


locale list_isEmpty = list +
  constrains α :: "'s => 'x list"
  fixes isEmpty :: "'s => bool"
  assumes isEmpty_correct:
    "invar s ==> isEmpty s <-> α s = []"

locale list_iteratei = list +
  constrains α :: "'s => 'x list"
  fixes iteratei :: "'s => ('x,'σ) set_iterator"
  assumes iteratei_correct:
    "invar s ==> iteratei s = foldli (α s)"
begin
  lemma iteratei_no_sel_rule:
    "invar s ==> distinct (α s) ==> set_iterator (iteratei s) (set (α s))"
    by (simp add: iteratei_correct set_iterator_foldli_correct)
end

lemma list_iteratei_iteratei_linord_rule:
  "list_iteratei α invar iteratei ==> invar s ==> distinct (α s) ==> sorted (α s) ==>
   set_iterator_linord (iteratei s) (set (α s))"
  by (simp add: list_iteratei_def set_iterator_linord_foldli_correct)

lemma list_iteratei_iteratei_rev_linord_rule:
  "list_iteratei α invar iteratei ==> invar s ==> distinct (α s) ==> sorted (rev (α s)) ==>
   set_iterator_rev_linord (iteratei s) (set (α s))"
  by (simp add: list_iteratei_def set_iterator_rev_linord_foldli_correct)


locale list_reverse_iteratei = list +
  constrains α :: "'s => 'x list"
  fixes reverse_iteratei :: "'s => ('x,'σ) set_iterator"
  assumes reverse_iteratei_correct:
    "invar s ==> reverse_iteratei s = foldri (α s)"
begin
  lemma reverse_iteratei_no_sel_rule:
    "invar s ==> distinct (α s) ==> set_iterator (reverse_iteratei s) (set (α s))"
    by (simp add: reverse_iteratei_correct set_iterator_foldri_correct)
end

lemma list_reverse_iteratei_iteratei_linord_rule:
  "list_reverse_iteratei α invar iteratei ==> invar s ==> distinct (α s) ==> sorted (rev (α s)) ==>
   set_iterator_linord (iteratei s) (set (α s))"
  by (simp add: list_reverse_iteratei_def set_iterator_linord_foldri_correct)

lemma list_reverse_iteratei_iteratei_rev_linord_rule:
  "list_reverse_iteratei α invar iteratei ==> invar s ==> distinct (α s) ==> sorted (α s) ==>
   set_iterator_rev_linord (iteratei s) (set (α s))"
  by (simp add: list_reverse_iteratei_def set_iterator_rev_linord_foldri_correct)


locale list_size = list +
  constrains α :: "'s => 'x list"
  fixes size :: "'s => nat"
  assumes size_correct:
    "invar s ==> size s = length (α s)"
  
subsubsection "Stack"

locale list_push = list +
  constrains α :: "'s => 'x list"
  fixes push :: "'x => 's => 's"
  assumes push_correct:
    "invar s ==> α (push x s) = x#α s"
    "invar s ==> invar (push x s)"

locale list_pop = list +
  constrains α :: "'s => 'x list"
  fixes pop :: "'s => ('x × 's)"
  assumes pop_correct:
    "[|invar s; α s ≠ []|] ==> fst (pop s) = hd (α s)"
    "[|invar s; α s ≠ []|] ==> α (snd (pop s)) = tl (α s)"
    "[|invar s; α s ≠ []|] ==> invar (snd (pop s))"
begin
  lemma popE: 
    assumes I: "invar s" "α s ≠ []" 
    obtains s' where "pop s = (hd (α s), s')" "invar s'" "α s' = tl (α s)"
  proof -
    from pop_correct(1,2,3)[OF I] have 
      C: "fst (pop s) = hd (α s)"
         "α (snd (pop s)) = tl (α s)"
         "invar (snd (pop s))" .
    from that[of "snd (pop s)", OF _ C(3,2), folded C(1)] show thesis
      by simp
  qed

  text {* The following shortcut notations are not meant for generating efficient code,
    but solely to simplify reasoning *}
  definition "head s == fst (pop s)"
  definition "tail s == snd (pop s)"

  lemma tail_correct: "[|invar F; α F ≠ []|] ==> α (tail F) = tl (α F)"
    by (simp add: tail_def pop_correct)

  lemma head_correct: "[|invar F; α F ≠ []|] ==> (head F) = hd (α F)"
    by (simp add: head_def pop_correct)

  lemma pop_split: "pop F = (head F, tail F)"
    apply (cases "pop F")
    apply (simp add: head_def tail_def)
    done

end

locale list_top = list +
  constrains α :: "'s => 'x list"
  fixes top :: "'s => 'x"
  assumes top_correct:
    "[|invar s; α s ≠ []|] ==> top s = hd (α s)"

subsubsection {* Queue *}
locale list_enqueue = list +
  constrains α :: "'s => 'x list"
  fixes enqueue :: "'x => 's => 's"
  assumes enqueue_correct: 
    "invar s ==> α (enqueue x s) = α s @ [x]"
    "invar s ==> invar (enqueue x s)"

  -- "Same specification as pop"
locale list_dequeue = list_pop
begin
  lemmas dequeue_correct = pop_correct
  lemmas dequeueE = popE
  lemmas dequeue_split=pop_split
end

  -- "Same specification as top"
locale list_next = list_top
begin
  lemmas next_correct = top_correct
end

subsubsection "Indexing"
locale list_get = list +
  constrains α :: "'s => 'x list"
  fixes get :: "'s => nat => 'x"
  assumes get_correct:
    "[|invar s; i<length (α s)|] ==> get s i = α s ! i"

locale list_set = list +
  constrains α :: "'s => 'x list"
  fixes set :: "'s => nat => 'x => 's"
  assumes set_correct:
    "[|invar s; i<length (α s)|] ==> α (set s i x) = α s [i := x]"
    "[|invar s; i<length (α s)|] ==> invar (set s i x)"

  -- "Same specification as enqueue"
locale list_add = list_enqueue
begin
  lemmas add_correct = enqueue_correct
end

    
end