Theory Induce_S

theory Induce_S
  imports "../abs-proof/Abs_Induce_S_Verification"
begin

section "Induce S Refinement"

fun induce_s_step_r0 ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list ⇒
   nat list × nat list × nat"
  where
"induce_s_step_r0 (B, SA, i) (α, T) =
  (case i of 
    Suc n ⇒
      (if Suc n < length SA ∧ SA ! Suc n < length T then
        (case SA ! Suc n of
          Suc j ⇒
            (case suffix_type T j of
              S_type ⇒
                (let b = α (T ! j);
                     k = B ! b - Suc 0
                 in (B[b := k], SA[k := j], n)
                )
              | _ ⇒ (B, SA, n)
            )
          | _ ⇒ (B, SA, n)
        )
        else
          (B, SA, n)
       )
    | _   ⇒ (B, SA, 0)
  )"

fun induce_s_step_r1 ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list × SL_types list ⇒
   nat list × nat list × nat"
  where
"induce_s_step_r1 (B, SA, i) (α, T, ST) =
  (case i of 
    Suc n ⇒
      (if Suc n < length SA ∧ SA ! Suc n < length T then
        (case SA ! Suc n of
          Suc j ⇒
            (case ST ! j of
              S_type ⇒
                (let b = α (T ! j);
                     k = B ! b - Suc 0
                 in (B[b := k], SA[k := j], n)
                )
              | _ ⇒ (B, SA, n)
            )
          | _ ⇒ (B, SA, n)
        )
        else
          (B, SA, n)
       )
    | _   ⇒ (B, SA, 0)
  )"

fun induce_s_step_r2 ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list × SL_types list ⇒
   nat list × nat list × nat"
  where
"induce_s_step_r2 (B, SA, i) (α, T, ST) =
  (case i of 
    Suc n ⇒
      (if Suc n < length SA  then
        (case SA ! Suc n of
          Suc j ⇒
            (case ST ! j of
              S_type ⇒
                (let b = α (T ! j);
                     k = B ! b - Suc 0
                 in (B[b := k], SA[k := j], n)
                )
              | _ ⇒ (B, SA, n)
            )
          | _ ⇒ (B, SA, n)
        )
        else
          (B, SA, n)
       )
    | _   ⇒ (B, SA, 0)
  )"

fun induce_s_step ::
  "nat list × nat list × nat ⇒
   (('a :: {linorder, order_bot}) ⇒ nat) × 'a list × SL_types list ⇒
   nat list × nat list × nat"
  where
"induce_s_step (B, SA, i) (α, T, ST) =
  (case i of 
    Suc n ⇒
    (case SA ! Suc n of
        Suc j ⇒
          (case ST ! j of
            S_type ⇒
              (let b = α (T ! j);
                   k = B ! b - Suc 0
               in (B[b := k], SA[k := j], n)
              )
            | _ ⇒ (B, SA, n)
          )
        | _ ⇒ (B, SA, n)
      )
    | _   ⇒ (B, SA, 0)
  )"

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

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

end