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 i1 i2 where "j. j  i1  x  S. P x j"
        and "j. j  i2  P x j"
        unfolding MOST_nat_le by auto
      hence "j. j  max i1 i2  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