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"
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 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)

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)"
      by (metis add_Suc le_Suc_ex numeral_2_eq_2)
    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. ∀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 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