Theory Even_More_List

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section ‹Lemmas on list operations›

theory Even_More_List
  imports Main
begin

lemma upt_add_eq_append':
  assumes "i  j" and "j  k"
  shows "[i..<k] = [i..<j] @ [j..<k]"
  using assms le_Suc_ex upt_add_eq_append by blast

lemma map_idem_upt_eq:
  map f [m..<n] = [m..<n] if q. m  q  q < n  f q = q
proof (cases n  m)
  case False
  then show ?thesis
    by simp
next
  case True
  moreover define r where r = n - m
  ultimately have n = m + r
    by simp
  with that have q. m  q  q < m + r  f q = q
    by simp
  then have map f [m..<m + r] = [m..<m + r]
    by (induction r) simp_all
  with n = m + r show ?thesis
    by simp
qed

lemma upt_zero_numeral_unfold:
  [0..<numeral n] = [0..<pred_numeral n] @ [pred_numeral n]
  by (simp add: numeral_eq_Suc)

lemma length_takeWhile_less:
  "xset xs. ¬ P x  length (takeWhile P xs) < length xs"
  by (induct xs) (auto split: if_splits)

lemma Min_eq_length_takeWhile:
  Min {m. P m} = length (takeWhile (Not  P) ([0..<n]))
  if *: m. P m  m < n and m. P m
proof -
  from m. P m obtain r where P r ..
  have Min {m. P m} = q + length (takeWhile (Not  P) ([q..<n]))
    if q  n m. P m  q  m  m < n for q
  using that proof (induction rule: inc_induct)
    case base
    from base [of r] P r show ?case
      by simp
  next
    case (step q)
    from q < n have *: [q..<n] = q # [Suc q..<n]
      by (simp add: upt_rec)
    show ?case
    proof (cases P q)
      case False
      then have Suc q  m  m < n if P m for m
        using that step.prems [of m] by (auto simp add: Suc_le_eq less_le)
      with ¬ P q show ?thesis
        by (simp add: * step.IH)
    next
      case True
      have {a. P a}  {0..n}
        using step.prems by (auto simp add: less_imp_le_nat)
      moreover have finite {0..n}
        by simp
      ultimately have finite {a. P a}
        by (rule finite_subset)
      with P q step.prems show ?thesis
        by (auto intro: Min_eqI simp add: *)
    qed
  qed
  from this [of 0] and that show ?thesis
    by simp
qed

lemma Max_eq_length_takeWhile:
  Max {m. P m} = n - Suc (length (takeWhile (Not  P) (rev [0..<n])))
  if *: m. P m  m < n and m. P m
using * proof (induction n)
  case 0
  with m. P m show ?case
    by auto
next
  case (Suc n)
  show ?case
  proof (cases P n)
    case False
    then have m < n if P m for m
      using that Suc.prems [of m] by (auto simp add: less_le)
    with Suc.IH show ?thesis
      by auto
  next
    case True
    have {a. P a}  {0..n}
      using Suc.prems by (auto simp add: less_Suc_eq_le)
    moreover have finite {0..n}
      by simp
    ultimately have finite {a. P a}
      by (rule finite_subset)
    with P n Suc.prems show ?thesis
      by (auto intro: Max_eqI simp add: less_Suc_eq_le)
  qed
qed

end