Theory Girth_Chromatic_Misc

theory Girth_Chromatic_Misc
imports
  Main
  "HOL-Library.Extended_Real"
begin

section ‹Auxilliary lemmas and setup›

text ‹
  This section contains facts about general concepts which are not directly
  connected to the proof of the Chromatic-Girth theorem. At some point in time,
  most of them could be moved to the Isabelle base library.

  Also, a little bit of setup happens.
›

subsection ‹Numbers›

lemma enat_in_Inf:
  fixes S :: "enat set"
  assumes "Inf S  top"
  shows "Inf S  S"
  using assms wellorder_InfI by auto

lemma enat_in_INF:
  fixes f :: "'a  enat"
  assumes "(INF xS. f x)  top"
  obtains x where "x  S" and "(INF xS. f x) = f x"
  by (meson assms enat_in_Inf imageE)

lemma enat_less_INF_I:
  fixes f :: "'a  enat"
  assumes not_inf: "x  " and less: "y. y  S  x < f y"
  shows "x < (INF yS. f y)"
  using assms by (auto simp: Suc_ile_eq[symmetric] INF_greatest)

lemma enat_le_Sup_iff:
  "enat k  Sup M  k = 0  (m  M. enat k  m)" (is "?L  ?R")
proof cases
  assume "k = 0" then show ?thesis by (auto simp: enat_0)
next
  assume "k  0"
  show ?thesis
  proof
    assume ?L
    then have "enat k  (if finite M then Max M else ); M  {}  mM. enat k  m"
      by (metis Max_in Sup_enat_def finite_enat_bounded linorder_linear)
    with k  0 and ?L show ?R
      unfolding Sup_enat_def
      by (cases "M={}") (auto simp add: enat_0[symmetric])
  next
    assume ?R then show ?L
      by (auto simp: enat_0 intro: complete_lattice_class.Sup_upper2)
  qed
qed

lemma enat_neq_zero_cancel_iff[simp]:
  "0  enat n  0  n"
  "enat n  0  n  0"
by (auto simp: enat_0[symmetric])


lemma natceiling_lessD: "nat(ceiling x) < n  x < real n"
  by linarith

lemma le_natceiling_iff:
  fixes n :: nat and r :: real
  shows "n  r  n  nat(ceiling r)"
  by linarith

lemma natceiling_le_iff:
  fixes n :: nat and r :: real
  shows "r  n  nat(ceiling r)  n"
  by linarith

lemma dist_real_noabs_less:
  fixes a b c :: real assumes "dist a b < c" shows "a - b < c"
using assms by (simp add: dist_real_def)

subsection ‹Lists and Sets›

lemma list_set_tl: "x  set (tl xs)  x  set xs"
  by (cases xs) auto

lemma list_exhaust3:
  obtains "xs = []" | x where "xs = [x]" | x y ys where "xs = x # y # ys"
  by (metis list.exhaust)

lemma card_Ex_subset:
  "k  card M  N. N  M  card N = k"
  by (induct rule: inc_induct) (auto simp: card_Suc_eq)



subsection ‹Limits and eventually›

text ‹
  We employ filters and the @{term eventually} predicate to deal with the
  @{term "N. nN. P n"} cases. To make this more convenient, introduce
  a shorter syntax.
›

abbreviation evseq :: "(nat  bool)  bool" (binder "" 10) where
  "evseq P  eventually P sequentially"

lemma LIMSEQ_neg_powr:
  assumes s: "s < 0"
  shows "(%x. (real x) powr s)  0"
  by (simp add: filterlim_real_sequentially s tendsto_neg_powr)

lemma LIMSEQ_inv_powr:
  assumes "0 < c" "0 < d"
  shows "(λn :: nat. (c / n) powr d)  0"
proof (rule tendsto_zero_powrI)
  from 0 < c have "x. 0 < x  0 < c / x" by simp
  then show "n. 0  c / real n"
    using assms(1) by auto
  show "(λx. c / real x)  0"
    by (simp add: lim_const_over_n)
qed (use assms in force)+

end