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" by (simp add: lim_const_over_n) qed (use assms in force)+ end