# Theory Girth_Chromatic.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 x∈S. f x) ≠ top"
obtains x where "x ∈ S" and "(INF x∈S. 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 y∈S. 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 ≠ {}⟧ ⟹ ∃m∈M. 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. ∀n≥N. 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"
qed (use assms in force)+

end
```