Theory ListSpec

header {* \isaheader{Specification of Sequences} *}
theory ListSpec 
imports ICF_Spec_Base
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"

locale list_no_invar = list +
  assumes invar[simp, intro!]: "!!l. invar l"

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 poly_list_iteratei = list +
  constrains α :: "'s => 'x list"
begin  
  definition iteratei where
    iteratei_correct[code_unfold]: "iteratei s ≡ foldli (α s)"
  definition iterate where
    iterate_correct[code_unfold]: "iterate s ≡ foldli (α s) (λ_. True)"
end

locale poly_list_rev_iteratei = list +
  constrains α :: "'s => 'x list"
begin  
  definition rev_iteratei where
    rev_iteratei_correct[code_unfold]: "rev_iteratei s ≡ foldri (α s)"
  definition rev_iterate where
    rev_iterate_correct[code_unfold]: "rev_iterate s ≡ foldri (α s) (λ_. True)"
end

(*
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)"
  
locale list_appendl = list +
  constrains α :: "'s => 'x list"
  fixes appendl :: "'x => 's => 's"
  assumes appendl_correct:
    "invar s ==> α (appendl x s) = x#α s"
    "invar s ==> invar (appendl x s)"
begin
  abbreviation (input) "push ≡ appendl" 
  lemmas push_correct = appendl_correct
end

locale list_removel = list +
  constrains α :: "'s => 'x list"
  fixes removel :: "'s => ('x × 's)"
  assumes removel_correct:
    "[|invar s; α s ≠ []|] ==> fst (removel s) = hd (α s)"
    "[|invar s; α s ≠ []|] ==> α (snd (removel s)) = tl (α s)"
    "[|invar s; α s ≠ []|] ==> invar (snd (removel s))"
begin
  lemma removelE: 
    assumes I: "invar s" "α s ≠ []" 
    obtains s' where "removel s = (hd (α s), s')" "invar s'" "α s' = tl (α s)"
  proof -
    from removel_correct(1,2,3)[OF I] have 
      C: "fst (removel s) = hd (α s)"
         "α (snd (removel s)) = tl (α s)"
         "invar (snd (removel s))" .
    from that[of "snd (removel 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 *}
  (* TODO: Is this actually used somewhere ? *)
  (*
  definition "head s == fst (removef s)"
  definition "tail s == snd (removef s)"

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

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

  lemma removef_split: "removef F = (head F, tail F)"
    apply (cases "removef F")
    apply (simp add: head_def tail_def)
    done
    *)
      
  abbreviation (input) "pop ≡ removel"
  lemmas pop_correct = removel_correct

  abbreviation (input) "dequeue ≡ removel"
  lemmas dequeue_correct = removel_correct
end

locale list_leftmost = list +
  constrains α :: "'s => 'x list"
  fixes leftmost :: "'s => 'x"
  assumes leftmost_correct:
    "[|invar s; α s ≠ []|] ==> leftmost s = hd (α s)"
begin
  abbreviation (input) top where "top ≡ leftmost"
  lemmas top_correct = leftmost_correct
end

locale list_appendr = list +
  constrains α :: "'s => 'x list"
  fixes appendr :: "'x => 's => 's"
  assumes appendr_correct: 
    "invar s ==> α (appendr x s) = α s @ [x]"
    "invar s ==> invar (appendr x s)"
begin
  abbreviation (input) "enqueue ≡ appendr"
  lemmas enqueue_correct = appendr_correct
end

locale list_remover = list +
  constrains α :: "'s => 'x list"
  fixes remover :: "'s => 's × 'x"
  assumes remover_correct: 
    "[|invar s; α s ≠ []|] ==> α (fst (remover s)) = butlast (α s)"
    "[|invar s; α s ≠ []|] ==> snd (remover s) = last (α s)"
    "[|invar s; α s ≠ []|] ==> invar (fst (remover s))"

locale list_rightmost = list +
  constrains α :: "'s => 'x list"
  fixes rightmost :: "'s => 'x"
  assumes rightmost_correct:
    "[|invar s; α s ≠ []|] ==> rightmost s = List.last (α s)"
begin
  abbreviation (input) bot where "bot ≡ rightmost"
  lemmas bot_correct = rightmost_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)"

record ('a,'s) list_ops = 
  list_op_α :: "'s => 'a list"
  list_op_invar :: "'s => bool"
  list_op_empty :: "unit => 's"
  list_op_isEmpty :: "'s => bool"
  list_op_size :: "'s => nat"
  list_op_appendl :: "'a => 's => 's"
  list_op_removel :: "'s => 'a × 's"
  list_op_leftmost :: "'s => 'a"
  list_op_appendr :: "'a => 's => 's"
  list_op_remover :: "'s => 's × 'a"
  list_op_rightmost :: "'s => 'a"
  list_op_get :: "'s => nat => 'a"
  list_op_set :: "'s => nat => 'a => 's"

locale StdListDefs = 
  poly_list_iteratei "list_op_α ops" "list_op_invar ops"
  + poly_list_rev_iteratei "list_op_α ops" "list_op_invar ops"
  for ops :: "('a,'s,'more) list_ops_scheme"
begin
  abbreviation α where "α ≡ list_op_α ops"
  abbreviation invar where "invar ≡ list_op_invar ops"
  abbreviation empty where "empty ≡ list_op_empty ops"
  abbreviation isEmpty where "isEmpty ≡ list_op_isEmpty ops"
  abbreviation size where "size ≡ list_op_size ops"
  abbreviation appendl where "appendl ≡ list_op_appendl ops"
  abbreviation removel where "removel ≡ list_op_removel ops"
  abbreviation leftmost where "leftmost ≡ list_op_leftmost ops"
  abbreviation appendr where "appendr ≡ list_op_appendr ops"
  abbreviation remover where "remover ≡ list_op_remover ops"
  abbreviation rightmost where "rightmost ≡ list_op_rightmost ops"
  abbreviation get where "get ≡ list_op_get ops"
  abbreviation set where "set ≡ list_op_set ops"
end

locale StdList = StdListDefs ops
  + list α invar
  + list_empty α invar empty 
  + list_isEmpty α invar isEmpty 
  + list_size α invar size 
  + list_appendl α invar appendl 
  + list_removel α invar removel 
  + list_leftmost α invar leftmost 
  + list_appendr α invar appendr 
  + list_remover α invar remover 
  + list_rightmost α invar rightmost 
  + list_get α invar get 
  + list_set α invar set 
  for ops :: "('a,'s,'more) list_ops_scheme"
begin
  lemmas correct = 
    empty_correct
    isEmpty_correct
    size_correct
    appendl_correct
    removel_correct
    leftmost_correct
    appendr_correct
    remover_correct
    rightmost_correct
    get_correct
    set_correct

end

locale StdList_no_invar = StdList + list_no_invar α invar
    
end