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:
  "∃x∈set 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