Theory Bucket_Insert

theory Bucket_Insert
  imports 
    "../../util/Repeat"
begin
section "Bucket Insert"

fun bucket_insert_step ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list × nat list ⇒
   nat list × nat list × nat"
  where
"bucket_insert_step (B, SA, i) (α, T, LMS) =
  (let b = α (T ! (LMS ! i));
       k = B ! b - Suc 0
   in (B[b := k], SA[k := LMS ! i], Suc i))"

definition bucket_insert_base ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat list ⇒
   nat list × nat list × nat"
  where
"bucket_insert_base α T B SA LMS = repeat (length LMS) bucket_insert_step (B, SA, 0) (α, T, LMS)"

definition bucket_insert ::
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ nat list ⇒ nat list ⇒
   nat list"
  where
"bucket_insert α T B SA LMS =
  (let (B', SA', i) = bucket_insert_base α T B SA LMS
   in SA')"

end