# Theory Preliminaries2

theory Preliminaries2
imports Infinite_Set
```(*
Author:      Salomon Sickert
*)

section ‹Auxiliary Facts›

theory Preliminaries2
imports Main "HOL-Library.Infinite_Set"
begin

subsection ‹Finite and Infinite Sets›

lemma finite_product:
assumes fst: "finite (fst ` A)"
and     snd: "finite (snd ` A)"
shows   "finite A"
proof -
have "A ⊆ (fst ` A) × (snd ` A)"
by force
thus ?thesis
using snd fst finite_subset by blast
qed

subsection ‹Cofinite Filters›

lemma almost_all_commutative:
"finite S ⟹ (∀x ∈ S. ∀⇩∞i. P x (i::nat)) = (∀⇩∞i. ∀x ∈ S. P x i)"
proof (induction rule: finite_induct)
case (insert x S)
{
assume "∀x ∈ insert x S. ∀⇩∞i. P x i"
hence "∀⇩∞i. ∀x ∈ S. P x i" and "∀⇩∞i. P x i"
using insert by simp+
then obtain i⇩1 i⇩2 where "⋀j. j ≥ i⇩1 ⟹ ∀x ∈ S. P x j"
and "⋀j. j ≥ i⇩2 ⟹ P x j"
unfolding MOST_nat_le by auto
hence "⋀j. j ≥ max i⇩1 i⇩2 ⟹ ∀x ∈ S ∪ {x}. P x j"
by simp
hence "∀⇩∞i. ∀x ∈ insert x S. P x i"
unfolding MOST_nat_le by blast
}
moreover
have "∀⇩∞i. ∀x ∈ insert x S. P x i ⟹ ∀x ∈ insert x S. ∀⇩∞i. P x i"
unfolding MOST_nat_le by auto
ultimately
show ?case
by blast
qed simp

lemma almost_all_commutative':
"finite S ⟹ (⋀x. x ∈ S ⟹ ∀⇩∞i. P x (i::nat)) ⟹ (∀⇩∞i. ∀x ∈ S. P x i)"
using almost_all_commutative by blast

fun index
where
"index P = (if ∀⇩∞i. P i then Some (LEAST i. ∀j ≥ i. P j) else None)"

lemma index_properties:
fixes i :: nat
shows "index P = Some i ⟹ 0 < i ⟹ ¬ P (i - 1)"
and "index P = Some i ⟹ j ≥ i ⟹ P j"
proof -
assume "index P = Some i"
moreover
hence i_def: "i = (LEAST i. ∀j ≥ i. P j)" and "∀⇩∞i. P i"
unfolding index.simps using option.distinct(2) option.sel
by (metis (erased, lifting))+
then obtain i' where "∀j ≥ i'.  P j"
unfolding MOST_nat_le by blast
ultimately
show "⋀j. j ≥ i ⟹ P j"
using LeastI[of "λi. ∀j ≥ i. P j"] by (metis i_def)
{
assume "0 < i"
then obtain j where "i = Suc j" and "j < i"
using lessE by blast
hence "⋀j'. j' > j ⟹ P j'"
using ‹⋀j. j ≥ i ⟹ P j› by force
hence "¬ P j"
using not_less_Least[OF ‹j < i›[unfolded i_def]] by (metis leI le_antisym)
thus "¬ P (i - 1)"
unfolding ‹i = Suc j› by simp
}
qed

end
```