Theory Preliminaries2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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