Theory Induce_S_Verification

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

section "Induce S Refinement"

lemma abs_induce_s_step_to_r0:
  shows "induce_s_step_r0 (B, SA, i) (α, T) = abs_induce_s_step (B, SA, i) (α, T)"
proof (cases i)
  case 0
  then show ?thesis
    by simp
next
  case (Suc n)
  assume "i = Suc n"
  then show ?thesis
  proof (cases "Suc n < length SA")
    assume "Suc n < length SA"
    show ?thesis
    proof (cases "SA ! Suc n < length T")
      assume "SA ! Suc n < length T"
      show ?thesis
      proof (cases "SA ! Suc n")
        case 0
        then show ?thesis
          by (clarsimp simp: ‹i = _› ‹Suc n < length _›  ‹SA ! _ < _›)
      next
        case (Suc j)
        assume "SA ! Suc n = Suc j"
        hence "Suc j < length T"
          using ‹SA ! Suc n < length T› by auto
        then show ?thesis
          by (clarsimp simp: ‹i = _› ‹Suc n < length _›  ‹SA ! _ < _›)
      qed
    next
      assume "¬ SA ! Suc n < length T"
      then show ?thesis
        by simp
    qed
  next
    assume "¬ Suc n < length SA"
    show ?thesis
      by (clarsimp simp: ‹i = _› ‹¬ _›)
  qed
qed

lemma induce_s_step_r0_to_r1:
  assumes "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
shows "induce_s_step_r1 (B, SA, i) (α, T, ST) = induce_s_step_r0 (B, SA, i) (α, T)"
proof (cases i)
  case 0
  then show ?thesis
    by auto
next
  case (Suc n)
  assume "i = Suc n"
  then show ?thesis
  proof (cases "Suc n < length SA ∧ SA ! Suc n < length T")
    assume "Suc n < length SA ∧ SA ! Suc n < length T"
    hence "Suc n < length SA" "SA ! Suc n < length T"
      by blast+
    then show ?thesis
    proof (cases "SA ! Suc n")
      case 0
      then show ?thesis
        by (clarsimp simp: ‹i = _› ‹Suc n < length _› ‹SA ! _ < _›)
    next
      case (Suc j)
      assume "SA ! Suc n = Suc j"
      hence "ST ! j = suffix_type T j"
        using ‹SA ! Suc n < length T› assms(1,2) by force
      then show ?thesis
        by (clarsimp simp: ‹i = _› ‹Suc n < length _› ‹SA ! _ < _› ‹SA ! _ = _›)
    qed
  next
    assume "¬ (Suc n < length SA ∧ SA ! Suc n < length T)"
    show ?thesis
      by (simp add: ‹¬ _›‹i = Suc n›)
  qed
qed

lemma abs_induce_s_step_to_r1:
  assumes "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
shows "induce_s_step_r1 (B, SA, i) (α, T, ST) = abs_induce_s_step (B, SA, i) (α, T)"
  by (metis assms induce_s_step_r0_to_r1 abs_induce_s_step_to_r0)

lemma induce_s_step_r1_to_r2:
  assumes "s_perm_inv α T B SA0 SA i"
  shows "induce_s_step_r2 (B, SA, i) (α, T, ST) = induce_s_step_r1 (B, SA, i) (α, T, ST)"
proof (cases i)
  case 0
  then show ?thesis
    by simp
next
  case (Suc n)
  then show ?thesis
  proof (cases "Suc n < length SA")
    assume "Suc n < length SA"
    moreover
    have "SA ! Suc n < length T"
      by (metis Suc assms calculation dual_order.refl s_perm_inv_elims(5) s_seen_invD(1))
    ultimately show ?thesis
    proof (cases "SA ! Suc n")
      case 0
      then show ?thesis
        using ‹i = Suc n› ‹Suc n < length SA› ‹SA ! Suc n < length T›
        by simp
    next
      case (Suc j)
      assume "SA ! Suc n = Suc j"
      then show ?thesis
      proof (cases "ST ! j")
        assume "ST ! j = S_type"
        then show ?thesis
          using ‹i = Suc n› ‹Suc n < length SA› ‹SA ! Suc n < length T› ‹SA ! Suc n = Suc j›
          by (clarsimp simp: Let_def)
      next
        assume "ST ! j = L_type"
        then show ?thesis
          using ‹i = Suc n› ‹Suc n < length SA› ‹SA ! Suc n < length T› ‹SA ! Suc n = Suc j›
          by (clarsimp simp: Let_def)
        qed
    qed
  next
    assume "i = Suc n" "¬Suc n < length SA"
    then show ?thesis
      by simp
  qed
qed

lemma abs_induce_s_step_to_r2:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
shows "induce_s_step_r2 (B, SA, i) (α, T, ST) = abs_induce_s_step (B, SA, i) (α, T)"
  by (metis assms induce_s_step_r1_to_r2 induce_s_step_r0_to_r1 abs_induce_s_step_to_r0)

lemma induce_s_step_r2_to:
  "i < length SA ⟹ induce_s_step (B, SA, i) (α, T, ST) = induce_s_step_r2 (B, SA, i) (α, T, ST)"
  by (clarsimp simp: Let_def split: nat.splits)

lemma abs_induce_s_step_to:
  assumes "s_perm_inv α T B SA0 SA i"
  and     "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
  and     "i < length SA"
shows "induce_s_step (B, SA, i) (α, T, ST) = abs_induce_s_step (B, SA, i) (α, T)"
  by (metis abs_induce_s_step_to_r2 assms induce_s_step_r2_to)

lemma abs_induce_s_base_to':
  assumes "s_perm_inv α T B SA0 SA n"
  and     "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
  and     "n < length SA"
shows "repeat m induce_s_step (B, SA, n) (α, T, ST) = repeat m abs_induce_s_step (B, SA, n) (α, T)"
  using assms(1,4)
proof (induct m arbitrary: B SA n)
  case 0
  then show ?case
    by (simp add: repeat_0)
next
  case (Suc m)
  note IH = this and
       R0 = repeat_step[of m abs_induce_s_step "(B, SA, n)" "(α, T)"] and
       R1 = repeat_step[of m induce_s_step "(B, SA, n)" "(α, T, ST)"]

  from repeat_abs_induce_s_step_index[of m B SA n α T]
  obtain B' SA' where S: 
    "repeat m abs_induce_s_step (B, SA, n) (α, T) = (B', SA', n - m)"
    "length SA' = length SA"
    "length B' = length B"
    by blast

  have "n - m < length SA"
    using Suc.prems(2) by auto
  hence "n - m < length SA'"
    using S(2) by fastforce

  from IH(1)[OF IH(2,3)] R1 S
  have "repeat (Suc m) induce_s_step (B, SA, n) (α, T, ST)
          = induce_s_step (B', SA', n - m) (α, T, ST)"
    by simp
  moreover
  from IH(1)[OF IH(2)] R0 S
  have "repeat (Suc m) abs_induce_s_step (B, SA, n) (α, T)
          = abs_induce_s_step (B', SA', n - m) (α, T)"
    by simp
  moreover
  let ?P = "λ(B, SA, i). s_perm_inv α T B SA0 SA i"
  have "s_perm_inv α T B' SA0 SA' (n - m)"
    by (rule repeat_maintain_inv[of ?P abs_induce_s_step "(α, T)" "(B, SA, n)" m,
                                  simplified S, simplified, OF _ IH(2)];
        clarsimp simp del: abs_induce_s_step.simps;
        erule (1) abs_induce_s_perm_step)
  with abs_induce_s_step_to[OF _ assms(2,3) `n - m < length SA'`, of α B' SA0]
  have "induce_s_step (B', SA', n - m) (α, T, ST) = abs_induce_s_step (B', SA', n - m) (α, T)"
    by blast
  ultimately show ?case 
    by simp
qed

lemma repeat_abs_induce_step_gre_length:
  assumes "length SA = length T"
  shows
    "length T ≤ Suc n ⟹
     repeat (Suc m) abs_induce_s_step (B, SA, Suc n) (α, T)
      = repeat m abs_induce_s_step (B, SA, n) (α, T)"
proof (induct m arbitrary: n)
  case 0
  then show ?case
    by (simp add: repeat_0 repeat_step Let_def assms)
next
  case (Suc m)
  note IH = this

  from repeat_step[of "Suc m" abs_induce_s_step "(B, SA, Suc n)" "(α, T)"]
       IH(1)[OF IH(2)]
  have "repeat (Suc (Suc m)) abs_induce_s_step (B, SA, Suc n) (α, T)
          = abs_induce_s_step (repeat m abs_induce_s_step (B, SA, n) (α, T)) (α, T)"
    by presburger
  with repeat_step[of m abs_induce_s_step "(B, SA, n)" "(α, T)"]
  show ?case
    by presburger
qed

lemma abs_induce_s_base_to:
  assumes "s_perm_pre α T B SA (length T)"
  and     "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
shows "induce_s_base α T ST B SA = abs_induce_s_base α T B SA"
proof -
  note A = assms(1)[simplified s_perm_pre_def]

  from assms(1)[simplified s_perm_pre_def]
  have "s_perm_inv α T B SA SA (length T)"
    by (simp add: s_perm_inv_established)
  with abs_induce_s_base_to'[OF _ assms(2-)]
  have "repeat (length T - Suc 0) induce_s_step (B, SA, length T - Suc 0) (α, T, ST)
        = repeat (length T - Suc 0) abs_induce_s_step (B, SA, length T - Suc 0) (α, T)"
    by (metis Suc_lessD Suc_pred A diff_Suc_less s_perm_inv_maintained_step_c1)
  moreover
  have "repeat (length T) abs_induce_s_step (B, SA, length T) (α, T)
        = repeat (length T - Suc 0) abs_induce_s_step (B, SA, length T - Suc 0) (α, T)"
    by (metis Suc_lessD Suc_pred A repeat_abs_induce_step_gre_length)
  ultimately show ?thesis
    by (simp add: abs_induce_s_base_def induce_s_base_def)
qed

lemma abs_induce_s_eq:
  assumes "s_perm_pre α T B SA (length T)"
  and     "length ST = length T"
  and     "∀k < length ST. ST ! k = suffix_type T k"
shows "abs_induce_s α T B SA = induce_s α T ST B SA"
  by (simp add: assms abs_induce_s_base_to abs_induce_s_def induce_s_def)

end