Theory Suffix_Array

theory Suffix_Array
  imports
    "../util/Sorting_Util"
    "../order/List_Lexorder_Util"
    "../order/Suffix"
    "../order/Valid_List"
    "../order/List_Permutation_Util"
begin

section ‹Axiomatic Suffix Array Specification›

locale Suffix_Array_General =
  fixes sa :: "('a  :: {linorder, order_bot}) list ⇒ nat list"
  assumes sa_g_permutation: "sa s <~~> [0..<length s]"
    and sa_g_sorted: "strict_sorted (map (suffix s) (sa s))"

locale Suffix_Array_Restricted =
  fixes sa :: "nat list ⇒ nat list"
  assumes sa_r_permutation: "valid_list s ⟹ sa s <~~> [0..<length s]"
    and sa_r_sorted: "valid_list s ⟹ strict_sorted (map (suffix s) (sa s))"

section ‹Wrapper for Natural Number String only Algorithm›

definition sa_nat_wrapper ::
  "('a :: linorder list ⇒ 'a ⇒ nat) ⇒ (nat list ⇒ nat list) ⇒ 'a :: linorder list ⇒ nat list"
where
  "sa_nat_wrapper α sa xs = 
  tl (sa ((map (λx. Suc (α xs x)) xs) @ [bot]))"

end