Theory Induce_L

theory Induce_L
  imports 
    "../../util/Repeat" 
     "../prop/Buckets"
begin 
section "Induce L Refinement"

fun induce_l_step_r0 ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list ⇒
   nat list × nat list × nat"
  where
"induce_l_step_r0 (B, SA, i) (α, T) =
  (if SA ! i < length T
   then
     (case SA ! i of
        Suc j ⇒
          (case suffix_type T j of 
             L_type ⇒
               (let k = α (T ! j);
                    l = B ! k
                in (B[k := Suc l], SA[l := j], Suc i))
             | _ ⇒ (B, SA, Suc i))
        | _ ⇒ (B, SA, Suc i))
   else (B, SA, Suc i))"
(*
lemma abs_induce_l_step_to_r0:
  "i < length SA ⟹ abs_induce_l_step (B, SA, i) (α, T) = induce_l_step_r0 (B, SA, i) (α, T)"
  by (clarsimp simp: Let_def split: prod.splits nat.splits SL_types.splits)
*)
fun induce_l_step ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list × SL_types list⇒
   nat list × nat list × nat"
  where
"induce_l_step (B, SA, i) (α, T, ST) =
  (if SA ! i < length T
   then
     (case SA ! i of
        Suc j ⇒
          (case ST ! j of 
             L_type ⇒
               (let k = α (T ! j);
                    l = B ! k
                in (B[k := Suc (B ! k)], SA[l := j], Suc i))
             | _ ⇒ (B, SA, Suc i))
        | _ ⇒ (B, SA, Suc i))
   else (B, SA, Suc i))"

definition induce_l_base :: 
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   SL_types list ⇒
   nat list ⇒
   nat list ⇒
   nat list × nat list × nat"
  where
"induce_l_base α T ST B SA = repeat (length T) induce_l_step (B, SA, 0) (α, T, ST)"

definition induce_l :: 
  "(('a :: {linorder, order_bot}) ⇒ nat) ⇒
   'a list ⇒
   SL_types list ⇒
   nat list ⇒
   nat list ⇒
   nat list"
  where
"induce_l α T ST B SA = (let (B', SA', i) = induce_l_base α T ST B SA in SA')"

end