# Theory Girth_Chromatic_Misc

theory Girth_Chromatic_Misc
imports
Main

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"
proof (rule ccontr)
assume A: "~?thesis"

obtain n where Inf_conv: "Inf S = enat n" using assms by (auto simp: top_enat_def)
{ fix s assume "s  S"
then have "Inf S  s" by (rule complete_lattice_class.Inf_lower)
moreover have "Inf S  s" using A s  S by auto
ultimately have "Inf S < s" by simp
with Inf_conv have "enat (Suc n)  s" by (cases s) auto
}
then have "enat (Suc n)  Inf S" by (simp add: le_Inf_iff)
with Inf_conv show False by auto
qed

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"
proof -
from assms have "(INF x S. f x)  f ` S"
using enat_in_Inf [of "f ` S"] by auto
then obtain x where "x  S" "(INF x S. f x) = f x" by auto
then show ?thesis ..
qed

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)

lemma n_choose_2_nat:
fixes n :: nat shows "(n choose 2) = (n * (n - 1)) div 2"
proof -
show ?thesis
proof (cases "2  n")
case True
then obtain m where "n = Suc (Suc m)"
moreover have "(n choose 2) = (fact n div fact (n - 2)) div 2"
using 2  n by (simp add: binomial_altdef_nat
div_mult2_eq[symmetric] mult.commute numeral_2_eq_2)
ultimately show ?thesis by (simp add: algebra_simps)
qed (auto simp: binomial_eq_0)
qed

lemma powr_less_one:
fixes x::real
assumes "1 < x" "y < 0"
shows "x powr y < 1"
using assms less_log_iff by force

lemma powr_le_one_le: "x y::real. 0 < x  x  1  1  y  x powr y  x"
proof -
fix x y :: real
assume "0 < x" "x  1" "1  y"
have "x powr y = (1 / (1 / x)) powr y" using 0 < x by (simp add: field_simps)
also have " = 1 / (1 / x) powr y" using 0 < x by (simp add: powr_divide)
also have "  1 / (1 / x) powr 1" proof -
have "1  1 / x" using 0 < x x  1 by (auto simp: field_simps)
then have "(1 / x) powr 1   (1 / x) powr y" using 0 < x
using 1  y by ( simp only: powr_mono)
then show ?thesis
by (metis 1  1 / x 1  y neg_le_iff_le powr_minus_divide powr_mono)
qed
also have "  x" using 0 < x by (auto simp: field_simps)
finally show "?thesis x y" .
qed

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 eventually_le_le:
fixes P :: "'a => ('b :: preorder)"
assumes "eventually (λx. P x  Q x) net"
assumes "eventually (λx. Q x  R  x) net"
shows "eventually (λx. P x  R x) net"
using assms by eventually_elim (rule order_trans)

lemma LIMSEQ_neg_powr:
assumes s: "s < 0"
shows "(%x. (real x) powr s)  0"
by (rule tendsto_neg_powr[OF assms filterlim_real_sequentially])

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 (intro tendsto_divide_0[OF tendsto_const] filterlim_at_top_imp_at_infinity
filterlim_real_sequentially tendsto_divide_0)
show "0 < d" by (rule assms)
show "(λx. d)  d" by auto
qed

end