Theory Chebyshev_Polynomials_Library
section ‹Missing Library Material›
theory Chebyshev_Polynomials_Library
imports "HOL-Computational_Algebra.Polynomial" "HOL-Library.FuncSet"
begin
text ‹
The following two lemmas give a full characterisation of the \<^const>‹filter› function:
The list \<^term>‹filter P xs› is the only list ‹ys› for which there exists a strictly increasing
function $f : \{0,\ldots,|\text{ys}|-1\} \to \{0,\ldots,|\text{xs}|-1\}$ such that:
▪ $\text{ys}_i = \text{xs}_{f(i)}$
▪ $P(\text{xs}_i) \longleftrightarrow \exists j{<}n.\ f(j) = i$, i.e.\ the range of $f$
are precisely the indices of the elements of ‹xs› that satisfy ‹P›.
›
lemma filterE:
fixes P :: "'a ⇒ bool" and xs :: "'a list"
assumes "length (filter P xs) = n"
obtains f :: "nat ⇒ nat" where
"strict_mono_on {..<n} f"
"⋀i. i < n ⟹ f i < length xs"
"⋀i. i < n ⟹ filter P xs ! i = xs ! f i"
"⋀i. i < length xs ⟹ P (xs ! i) ⟷ (∃j. j < n ∧ f j = i)"
using assms(1)
proof (induction xs arbitrary: n thesis)
case Nil
thus ?case
using that[of "λ_. 0"] by auto
next
case (Cons x xs)
define n' where "n' = (if P x then n - 1 else n)"
obtain f :: "nat ⇒ nat" where f:
"strict_mono_on {..<n'} f"
"⋀i. i < n'⟹ f i < length xs"
"⋀i. i < n' ⟹ filter P xs ! i = xs ! f i"
"⋀i. i < length xs ⟹ P (xs ! i) ⟷ (∃j. j < n' ∧ f j = i)"
proof (rule Cons.IH[where n = n'])
show "length (filter P xs) = n'"
using Cons.prems(2) by (auto simp: n'_def)
qed auto
define f' where "f' = (λi. if P x then case i of 0 ⇒ 0 | Suc j ⇒ Suc (f j) else Suc (f i))"
show ?case
proof (rule Cons.prems(1))
show "strict_mono_on {..<n} f'"
by (auto simp: f'_def strict_mono_on_def n'_def strict_mono_onD[OF f(1)] split: nat.splits)
show "f' i < length (x # xs)" if "i < n" for i
using that f(2) by (auto simp: f'_def n'_def split: nat.splits)
show "filter P (x # xs) ! i = (x # xs) ! f' i" if "i < n" for i
using that f(3) by (auto simp: f'_def n'_def split: nat.splits)
show "P ((x # xs) ! i) ⟷ (∃j<n. f' j = i)" if "i < length (x # xs)" for i
proof (cases i)
case [simp]: 0
show ?thesis using that Cons.prems(2)
by (auto simp: f'_def intro!: exI[of _ 0])
next
case [simp]: (Suc i')
have "P ((x # xs) ! i) ⟷ P (xs ! i')"
by simp
also have "… ⟷ (∃j<n'. f j = i')"
using that by (subst f(4)) simp_all
also have "… ⟷ {j∈{..<n'}. f j = i'} ≠ {}"
by blast
also have "bij_betw (λj. if P x then j+1 else j) {j∈{..<n'}. f j = i'} {j∈{..<n}. f' j = i}"
proof (intro bij_betwI[of _ _ _ "λj. if P x then j-1 else j"], goal_cases)
case 2
have "(if P x then j - 1 else j) < n'"
if "j < n" "f' j = i" for j
using that by (auto simp: n'_def f'_def split: nat.splits)
moreover have "f (if P x then j - 1 else j) = i'" if "j < n" "f' j = i" for j
using that by (auto simp: n'_def f'_def split: nat.splits if_splits)
ultimately show ?case by auto
qed (auto simp: n'_def f'_def split: nat.splits)
hence "{j∈{..<n'}. f j = i'} ≠ {} ⟷ {j∈{..<n}. f' j = i} ≠ {}"
unfolding bij_betw_def by blast
also have "… ⟷ (∃j<n. f' j = i)"
by auto
finally show ?thesis .
qed
qed
qed
text ‹
The following lemma shows the uniqueness of the above property.
It is very useful for finding a ``closed form'' for \<^term>‹filter P xs› in some concrete
situation.
For example, if we know that exactly every other element of ‹xs› satisfies ‹P›,
we can use it to prove that
\<^prop>‹filter P xs = map (λi. 2 * i) [0..<length xs div 2]›
›
lemma filter_eqI:
fixes f :: "nat ⇒ nat" and xs ys :: "'a list"
defines "n ≡ length ys"
assumes "strict_mono_on {..<n} f"
assumes "⋀i. i < n ⟹ f i < length xs"
assumes "⋀i. i < n ⟹ ys ! i = xs ! f i"
assumes "⋀i. i < length xs ⟹ P (xs ! i) ⟷ (∃j. j < n ∧ f j = i)"
shows "filter P xs = ys"
using assms(2-) unfolding n_def
proof (induction xs arbitrary: ys f)
case Nil
thus ?case by auto
next
case (Cons x xs ys f)
show ?case
proof (cases "P x")
case False
have "filter P xs = ys"
proof (rule Cons.IH)
have pos: "f i > 0" if "i < length ys" for i
using Cons.prems(4)[of "f i"] Cons.prems(2,3)[of i] that False
by (auto intro!: Nat.gr0I)
show "strict_mono_on {..<length ys} ((λx. x - 1) ∘ f)"
proof (intro strict_mono_onI)
fix i j assume ij: "i ∈ {..<length ys}" "j ∈ {..<length ys}" "i < j"
thus "((λx. x - 1) ∘ f) i < ((λx. x - 1) ∘ f) j"
using Cons.prems(1) pos[of i] pos[of j]
by (auto simp: strict_mono_on_def diff_less_mono)
qed
show "((λx. x - 1) ∘ f) i < length xs" if "i < length ys" for i
using Cons.prems(2)[of i] pos[of i] that by auto
show "ys ! i = xs ! ((λx. x - 1) ∘ f) i" if "i < length ys" for i
using Cons.prems(3)[of i] pos[of i] that by auto
show "P (xs ! i) ⟷ (∃j<length ys. ((λx. x - 1) ∘ f) j = i)" if "i < length xs" for i
using Cons.prems(4)[of "Suc i"] that pos by (auto split: if_splits)
qed
thus ?thesis
using False by simp
next
case True
have "ys ≠ []"
using Cons.prems(4)[of 0] True by auto
have [simp]: "f 0 = 0"
proof -
obtain j where "j < length ys" "f j = 0"
using Cons.prems(4)[of 0] True by auto
with strict_mono_onD[OF Cons.prems(1)] have "j = 0"
by (metis gr_implies_not_zero lessThan_iff less_antisym zero_less_Suc)
with ‹f j = 0› show ?thesis
by simp
qed
have pos: "f j > 0" if "j > 0" "j < length ys" for j
using strict_mono_onD[OF Cons.prems(1), of 0 j] that ‹ys ≠ []› by auto
have f_eq_Suc_imp_pos: "j > 0" if "f j = Suc k" for j k
by (rule Nat.gr0I) (use that in auto)
define f' where "f' = (λn. f (Suc n) - 1)"
have "filter P xs = tl ys"
proof (rule Cons.IH)
show "strict_mono_on {..<length (tl ys)} f'"
proof (intro strict_mono_onI)
fix i j assume ij: "i ∈ {..<length (tl ys)}" "j ∈ {..<length (tl ys)}" "i < j"
from ij have "Suc i < length ys" "Suc j < length ys"
by auto
thus "f' i < f' j"
using strict_mono_onD[OF Cons.prems(1), of "Suc i" "Suc j"]
pos[of "Suc i"] pos[of "Suc j"] ‹ys ≠ []› ‹i < j›
by (auto simp: strict_mono_on_def diff_less_mono f'_def)
qed
show "f' i < length xs" and "tl ys ! i = xs ! f' i" if "i < length (tl ys)" for i
proof -
have "Suc i < length ys"
using that by auto
thus "f' i < length xs"
using Cons.prems(2)[of "Suc i"] pos[of "Suc i"] that by (auto simp: f'_def)
show "tl ys ! i = xs ! f' i"
using ‹Suc i < length ys› that Cons.prems(3)[of "Suc i"] pos[of "Suc i"]
by (auto simp: nth_tl nth_Cons f'_def split: nat.splits)
qed
show "P (xs ! i) ⟷ (∃j<length (tl ys). f' j = i)" if "i < length xs" for i
proof -
have "P (xs ! i) ⟷ P ((x # xs) ! Suc i)"
by simp
also have "… ⟷ {j ∈ {..<length ys}. f j = Suc i} ≠ {}"
using that by (subst Cons.prems(4)) auto
also have "bij_betw (λx. x - 1) {j ∈ {..<length ys}. f j = Suc i}
{j ∈ {..<length (tl ys)}. f' j = i}"
by (rule bij_betwI[of _ _ _ Suc])
(auto simp: f'_def Suc_diff_Suc f_eq_Suc_imp_pos diff_less_mono Suc_leI pos)
hence "{j ∈ {..<length ys}. f j = Suc i} ≠ {} ⟷ {j ∈ {..<length (tl ys)}. f' j = i} ≠ {}"
unfolding bij_betw_def by blast
also have "… ⟷ (∃j<length (tl ys). f' j = i)"
by blast
finally show ?thesis .
qed
qed
moreover have "hd ys = x"
using True ‹f 0 = 0› ‹ys ≠ []› Cons.prems(3)[of 0] by (auto simp: hd_conv_nth)
ultimately show ?thesis
using ‹ys ≠ []› True by force
qed
qed
lemma filter_eq_iff:
"filter P xs = ys ⟷
(∃f. strict_mono_on {..<length ys} f ∧
(∀i<length ys. f i < length xs ∧ ys ! i = xs ! f i) ∧
(∀i<length xs. P (xs ! i) ⟷ (∃j. j < length ys ∧ f j = i)))"
(is "?lhs = ?rhs")
proof
show ?rhs if ?lhs
unfolding that [symmetric] by (rule filterE[OF refl, of P xs]) blast
show ?lhs if ?rhs
using that filter_eqI[of ys _ xs P] by blast
qed
end