Theory AnnotatedListSpec

header {*\isaheader{Specification of Annotated Lists}*}
theory AnnotatedListSpec
imports Main
begin

(*@intf AnnotatedList
  @abstype ('e × 'a::monoid_add) list
  Lists with annotated elements. The annotations form a monoid, and there is
  a split operation to split the list according to its annotations. This is the
  abstract concept implemented by finger trees.
*)

subsection "Introduction"
text {*
  We define lists with annotated elements. The annotations form a monoid.

  We provide standard list operations and the split-operation, that
  splits the list according to its annotations.
*}
locale al =
  --"Annotated lists are abstracted to lists of pairs of elements and annotations."
  fixes α :: "'s => ('e × 'a::monoid_add) list"
  fixes invar :: "'s => bool"
  

subsection "Basic Annotated List Operations"

subsubsection "Empty Annotated List"
locale al_empty = al +
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes empty :: "unit => 's"
  assumes empty_correct: 
    "invar (empty ())" 
    "α (empty ()) = Nil" 

subsubsection "Emptiness Check"
locale al_isEmpty = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes isEmpty :: "'s => bool"
  assumes isEmpty_correct: 
    "invar s ==> isEmpty s <-> α s = Nil" 

subsubsection "Counting Elements"
locale al_count = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes count :: "'s => nat"
  assumes count_correct: 
    "invar s ==> count s = length(α s)" 

subsubsection "Appending an Element from the Left"
locale al_consl = al +
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes consl :: "'e => 'a => 's => 's"
  assumes consl_correct:
    "invar s ==> invar (consl e a s)"
    "invar s ==> (α (consl e a s)) = (e,a) # (α s)"

subsubsection "Appending an Element from the Right"
locale al_consr = al +
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes consr :: "'s => 'e => 'a => 's"
  assumes consr_correct:
    "invar s ==> invar (consr s e a)"
    "invar s ==> (α (consr s e a)) = (α s) @ [(e,a)]"
  
subsubsection "Take the First Element"
locale al_head = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes head :: "'s => ('e × 'a)"
  assumes head_correct:
    "[|invar s; α s ≠ Nil|] ==> head s = hd (α s)"

subsubsection "Drop the First Element"
locale al_tail = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes tail :: "'s => 's"
  assumes tail_correct:
    "[|invar s; α s ≠ Nil|] ==> α (tail s) = tl (α s)"
    "[|invar s; α s ≠ Nil|] ==> invar (tail s)"

subsubsection "Take the Last Element"
locale al_headR = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes headR :: "'s => ('e × 'a)"
  assumes headR_correct:
    "[|invar s; α s ≠ Nil|] ==> headR s = last (α s)"

subsubsection "Drop the Last Element"
locale al_tailR = al +   
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes tailR :: "'s => 's"
  assumes tailR_correct:
    "[|invar s; α s ≠ Nil|] ==> α (tailR s) = butlast (α s)"
    "[|invar s; α s ≠ Nil|] ==> invar (tailR s)"

subsubsection "Fold a Function over the Elements from the Left"
locale al_foldl = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes foldl :: "('z => 'e × 'a => 'z) => 'z => 's => 'z"
  assumes foldl_correct:
    "invar s ==> foldl f σ s = List.foldl f σ (α s)"

subsubsection "Fold a Function over the Elements from the Right"
locale al_foldr = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes foldr :: "('e × 'a => 'z => 'z) => 's => 'z => 'z"
  assumes foldr_correct:
    "invar s ==> foldr f s σ = List.foldr f (α s) σ"
    
subsubsection "Concatenation of Two Annotated Lists"
locale al_app = al +
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes app :: "'s => 's => 's"
  assumes app_correct:
    "[|invar s;invar s'|] ==> α (app s s') = (α s) @ (α s')"
    "[|invar s;invar s'|] ==> invar (app s s')"

subsubsection "Readout the Summed up Annotations"
locale al_annot = al +
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes annot :: "'s => 'a"
  assumes annot_correct:
    "invar s ==> (annot s) = (listsum (map snd (α s)))"

subsubsection "Split by Monotone Predicate"
locale al_splits = al + 
  constrains α :: "'s => ('e × 'a::monoid_add) list"
  fixes splits :: "('a => bool) => 'a => 's => 
                                ('s × ('e × 'a) × 's)"
  assumes splits_correct:
    "[|invar s;
       ∀a b. p a --> p (a + b);
       ¬ p i; 
       p (i + listsum (map snd (α s)));
       (splits p i s) = (l, (e,a), r)|] 
      ==> 
        (α s) = (α l) @ (e,a) # (α r)  ∧
        ¬ p (i + listsum (map snd (α l)))  ∧
        p (i + listsum (map snd (α l)) + a)  ∧
        invar l  ∧
        invar r
    "
begin
  lemma splitsE:
    assumes 
    invar: "invar s" and
    mono: "∀a b. p a --> p (a + b)" and
    init_ff: "¬ p i" and
    sum_tt: "p (i + listsum (map snd (α s)))"
    obtains l e a r where
    "(splits p i s) = (l, (e,a), r)"
    "(α s) = (α l) @ (e,a) # (α r)"
    "¬ p (i + listsum (map snd (α l)))"
    "p (i + listsum (map snd (α l)) + a)"
    "invar l"
    "invar r"
    using assms
    apply (cases "splits p i s")
    apply (case_tac b)
    apply (drule_tac i = i and p = p 
      and l = a and r = c and e = aa and a = ba in  splits_correct)
    apply (simp_all)
    apply blast
    done
end    

subsection "Record Based Interface"
record ('e,'a,'s) alist_ops =
  alist_op_α ::"'s => ('e × 'a::monoid_add) list"
  alist_op_invar :: "'s => bool"
  alist_op_empty :: "unit => 's"
  alist_op_isEmpty :: "'s => bool"
  alist_op_count :: "'s => nat"
  alist_op_consl :: "'e => 'a => 's => 's"
  alist_op_consr :: "'s => 'e => 'a => 's"
  alist_op_head :: "'s => ('e × 'a)"
  alist_op_tail :: "'s => 's"
  alist_op_headR :: "'s => ('e × 'a)"
  alist_op_tailR :: "'s => 's"
  alist_op_app :: "'s => 's => 's"
  alist_op_annot :: "'s => 'a"
  alist_op_splits :: "('a => bool) => 'a => 's => ('s × ('e × 'a) × 's)"

locale StdALDefs =
  fixes ops :: "('e,'a::monoid_add,'s,'more) alist_ops_scheme"
begin
  abbreviation α where "α == alist_op_α ops"
  abbreviation invar where "invar == alist_op_invar ops "
  abbreviation empty where "empty == alist_op_empty ops "
  abbreviation isEmpty where "isEmpty == alist_op_isEmpty ops "
  abbreviation count where "count == alist_op_count ops"
  abbreviation consl where "consl == alist_op_consl ops "
  abbreviation consr where "consr == alist_op_consr ops "
  abbreviation head where "head == alist_op_head ops "
  abbreviation tail where "tail == alist_op_tail ops "
  abbreviation headR where "headR == alist_op_headR ops "
  abbreviation tailR where "tailR == alist_op_tailR ops "
  abbreviation app where "app == alist_op_app ops "
  abbreviation annot where "annot == alist_op_annot ops "
  abbreviation splits where "splits == alist_op_splits ops "
end

locale StdAL = StdALDefs ops +
  al α invar +
  al_empty α invar empty +
  al_isEmpty α invar isEmpty +
  al_count α invar count +
  al_consl α invar consl +
  al_consr α invar consr +
  al_head α invar head +
  al_tail α invar tail +
  al_headR α invar headR +
  al_tailR α invar tailR +
  al_app α invar app +
  al_annot α invar annot +
  al_splits α invar splits
  for ops
begin
  lemmas correct =
    empty_correct 
    isEmpty_correct
    count_correct
    consl_correct
    consr_correct
    head_correct
    tail_correct
    headR_correct
    tailR_correct
    app_correct
    annot_correct      
end

end