# Theory Word_Lib.Even_More_List

```(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
*)

section ‹Lemmas on list operations›

theory Even_More_List
imports Main
begin

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]›

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]›
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
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
```