(* * 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