Theory AnnotatedListSpec

section ‹\isaheader{Specification of Annotated Lists}›
theory AnnotatedListSpec
imports ICF_Spec_Base
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"
  
locale al_no_invar = al +
  assumes invar[simp, intro!]: "⋀l. invar l"

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) σ"

locale poly_al_fold = al +
  constrains α :: "'s ⇒ ('e × 'a::monoid_add) list"
begin
  definition foldl where 
    foldl_correct[code_unfold]: "foldl f σ s = List.foldl f σ (α s)"
  definition foldr where 
    foldr_correct[code_unfold]: "foldr f s σ = List.foldr f (α s) σ"
end
    
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) = (sum_list (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 + sum_list (map snd (α s)));
       (splits p i s) = (l, (e,a), r)⟧ 
      ⟹ 
        (α s) = (α l) @ (e,a) # (α r)  ∧
        ¬ p (i + sum_list (map snd (α l)))  ∧
        p (i + sum_list (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 + sum_list (map snd (α s)))"
    obtains l e a r where
    "(splits p i s) = (l, (e,a), r)"
    "(α s) = (α l) @ (e,a) # (α r)"
    "¬ p (i + sum_list (map snd (α l)))"
    "p (i + sum_list (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)
    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 = poly_al_fold "alist_op_α ops" "alist_op_invar ops"
  for 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      
    foldl_correct
    foldr_correct
end

locale StdAL_no_invar = StdAL + al_no_invar α invar


end