(*  Author: Ata Keskin, TU München 
*)

theory Slope
imports "HOL.Archimedean_Field"
begin

section ‹Slopes›

subsection ‹Bounded Functions›

definition bounded :: "('a → int) → bool" where
  "bounded f ⟷ bdd_above ((λz. ∣f z∣) ` UNIV)"

lemma boundedI:
  assumes "∧z. ∣f z∣ ≤ C"
  shows "bounded f"
  unfolding bounded_def by (rule bdd_aboveI2, force intro: assms)

lemma boundedE[elim]:
  assumes "bounded f" "∃C. (∀z. ∣f z∣ ≤ C) ∧ 0 ≤ C ==> P"
  shows P
  using assms unfolding bounded_def bdd_above_def by fastforce

lemma boundedE_strict:
  assumes "bounded f" "∃C. (∀z. ∣f z∣ < C) ∧ 0 < C ==> P"
  shows P
  by (meson bounded_def bdd_above_def assms boundedE gt_ex order.strict_trans1)

lemma bounded_alt_def: "bounded f ⟷ (∃C. ∀z. ∣f z∣ ≤ C)" using boundedI boundedE by meson

lemma bounded_iff_finite_range: "bounded f ⟷ finite (range f)"
proof
  assume "bounded f"
  then obtain C where bound: "∣z∣ ≤ C" if "z ∈ range f" for z by blast
  have "range f ⊆ {z. z ≤ C ∧ -z ≤ C}" using abs_le_D1[OF bound] abs_le_D2[OF bound] by blast
  also have "... = {(-C)..C}" by force
  finally show "finite (range f)" using finite_subset finite_atLeastAtMost_int by blast
next
  assume "finite (range f)"
  hence "∣f z∣ ≤ max (abs (Sup (range f))) (abs (Inf (range f)))" for z 
    using cInf_lower[OF _ bdd_below_finite, of "f z" "range f"] cSup_upper[OF _ bdd_above_finite, of "f z" "range f"] by force
  thus "bounded f" by (rule boundedI)
qed

lemma bounded_constant:
  shows "bounded (λ_. c)"
  by (rule boundedI[of _ "∣c∣"], blast)

lemma bounded_add:
  assumes "bounded f" "bounded g"
  shows "bounded (λz. f z + g z)"
proof -
  obtain C_f C_g where "∣f z∣ ≤ C_f" "∣g z∣ ≤ C_g" for z using assms by blast
  hence "∣f z + g z∣ ≤ C_f + C_g" for z by (meson abs_triangle_ineq add_mono dual_order.trans)
  thus ?thesis by (blast intro: boundedI)
qed

lemma bounded_mult:
  assumes "bounded f" "bounded g"
  shows "bounded (λz. f z * g z)"
proof -
  obtain C where bound: "∣f z∣ ≤ C" and C_nonneg: "0 ≤ C" for z using assms by blast
  obtain C' where bound': "∣g z∣ ≤ C'" for z using assms by blast
  show ?thesis using mult_mono[OF bound bound' C_nonneg abs_ge_zero] by (simp only: boundedI[of "λz. f z * g z" "C * C'"] abs_mult)
qed

lemma bounded_mult_const:
  assumes "bounded f"
  shows "bounded (λz. c * f z)"
  by (rule bounded_mult[OF bounded_constant[of c] assms])

lemma bounded_uminus:
  assumes "bounded f"
  shows "bounded (λx. - f x)"
  using bounded_mult_const[OF assms, of "- 1"] by simp

lemma bounded_comp:
  assumes "bounded f"
  shows "bounded (f o g)" and "bounded (g o f)"
proof -
  show "bounded (f o g)" using assms boundedI comp_def boundedE by metis
next
  have "range (g o f) = g ` range f" by fastforce
  thus "bounded (g o f)" using assms by (fastforce simp: bounded_iff_finite_range)
qed

subsection ‹Properties of Slopes›

definition slope :: "(int → int) → bool" where
  "slope f ⟷ bounded (λ(m, n). f (m + n) - (f m + f n))"

lemma bounded_slopeI:
  assumes "bounded f"
  shows "slope f"
proof -
  obtain C where "∣f x∣ ≤ C" for x using assms by blast
  hence "∣f (m + n) - (f m + f n)∣ ≤ C + (C + C)" for m n
    using abs_triangle_ineq4[of "f (m + n)" "f m + f n"] abs_triangle_ineq[of "f m" "f n"] by (meson add_mono order_trans)
  thus ?thesis unfolding slope_def by (fast intro: boundedI)
qed

lemma slopeE[elim]:
  assumes "slope f"
  obtains C where "∧m n. ∣f (m + n) - (f m + f n)∣ ≤ C" "0 ≤ C" using assms unfolding slope_def by fastforce

lemma slope_add:
  assumes "slope f" "slope g"
  shows "slope (λz. f z + g z)"
proof -
  obtain C where bound: "∣f (m + n) - (f m + f n)∣ ≤ C" for m n using assms by fast
  obtain C' where bound': "∣g (m + n) - (g m + g n)∣ ≤ C'" for m n using assms by fast
  have "∣f (m + n) - (f m + f n)∣ + ∣g (m + n) - (g m + g n)∣ ≤ C + C'" for m n using add_mono_thms_linordered_semiring(1) bound bound' by fast
  moreover have "∣(λz. f z + g z) (m + n) - ((λz. f z + g z) m + (λz. f z + g z) n)∣ ≤ ∣f (m + n) - (f m + f n)∣ + ∣g (m + n) - (g m + g n)∣" for m n by linarith
  ultimately have "∣(λz. f z + g z) (m + n) - ((λz. f z + g z) m + (λz. f z + g z) n)∣ ≤ C + C'" for m n using order_trans by fast
  thus "slope (λz. f z + g z)" unfolding slope_def by (fast intro: boundedI)
qed

lemma slope_symmetric_bound:
  assumes "slope f"
  obtains C where "∧p q. ∣p * f q - q * f p∣ ≤ (∣p∣ + ∣q∣ + 2) * C" "0 ≤ C"
proof -
  obtain C where bound: "∣f (m + n) - (f m + f n)∣ ≤ C" and C_nonneg: "0 ≤ C" for m n using assms by fast
  
  have *: "∣f (p * q) - p * f q∣ ≤ (∣p∣ + 1) * C" for p q
  proof (induction p rule: int_induct[where ?k=0])
    case base
    then show ?case using bound[of 0 0] by force
  next
    case (step1 p)
    have "∣f ((p + 1) * q) - f (p * q) - f q∣ ≤ C" using bound[of "p * q" q]  by (auto simp: distrib_left mult.commute)
    hence "∣f ((p + 1) * q) - f q - p * f q∣ ≤ C + (∣p∣ + 1) * C" using step1 by fastforce
    thus ?case using step1 by (auto simp add: distrib_left mult.commute)
  next
    case (step2 p)
    have "∣f ((p - 1) * q) + f q - f (p * q)∣ ≤ C" using bound[of "p * q - q" "q"] by (auto simp: mult.commute right_diff_distrib')
    hence "∣f ((p - 1) * q) + f q - p * f q∣ ≤ C + (∣p∣ + 1) * C" using step2 by force
    hence "∣f ((p - 1) * q) - (p - 1) * f q∣ ≤ C + (∣p - 1∣) * C" using step2 by (auto simp: mult.commute right_diff_distrib')
    thus ?case by (auto simp add: distrib_left mult.commute)
  qed

  have "∣p * f q - q * f p∣ ≤ (∣p∣ + ∣q∣ + 2) * C" for p q
  proof -
    have "∣p * f q - q * f p∣ ≤ ∣f (p * q) - p * f q∣ + ∣f (q * p) - q * f p∣" by (fastforce simp: mult.commute)
    also have "... ≤ (∣p∣ + 1) * C + (∣q∣ + 1) * C" using *[of p q] *[of q p] by fastforce
    also have "... = (∣p∣ + ∣q∣ + 2) * C" by algebra
    finally show ?thesis .
  qed
  thus ?thesis using that C_nonneg by blast
qed

lemma slope_linear_bound:
  assumes "slope f"
  obtains A B where "∀n. ∣f n∣ ≤ A * ∣n∣ + B" "0 ≤ A" "0 ≤ B"
proof -
  obtain C where bound: "∣p * f q - q * f p∣ ≤ (∣p∣ + ∣q∣ + 2) * C" "0 ≤ C" for p q using assms slope_symmetric_bound by blast

  have "∣f p∣ ≤ (C + ∣f 1∣) * ∣p∣ + 3 * C" for p
  proof -
    have "∣p * f 1 - f p∣ ≤ (∣p∣ + 3) * C" using bound(1)[of _ 1] by (simp add: add.commute)
    hence "∣f p - p * f 1∣ ≤ (∣p∣ + 3) * C" by (subst abs_minus[of "f p - p * f 1", symmetric], simp)
    hence "∣f p∣ ≤ (∣p∣ + 3) * C + ∣p * f 1∣" using dual_order.trans abs_triangle_ineq2 diff_le_eq by fast
    hence "∣f p∣ ≤ ∣p∣ * C + 3 * C + ∣p∣ * ∣f 1∣" by (simp add: abs_mult int_distrib(2) mult.commute)
    hence "∣f p∣ ≤ ∣p∣ * (C + ∣f 1∣) + 3 * C" by (simp add: ring_class.ring_distribs(1))
    thus ?thesis using mult.commute by metis
  qed
  thus ?thesis using that bound(2) by fastforce
qed

lemma slope_comp:
  assumes "slope f" "slope g"
  shows "slope (f o g)"
proof-
  obtain C where bound: "∣f (m + n) - (f m + f n)∣ ≤ C" for m n using assms by fast
  obtain C' where bound': "∣g (m + n) - (g m + g n)∣ ≤ C'" for m n using assms by fast
  obtain A B where f_linear_bound: "∣f n∣ ≤ A * ∣n∣ + B" "0 ≤ A" "0 ≤ B" for n using slope_linear_bound[OF assms(1)] by blast
  {
    fix m n
    have "∣f (g (m + n)) - (f (g m) + f (g n))∣ ≤ (∣f (g (m + n)) - f (g m + g n)∣ + ∣f (g m + g n) - (f (g m) + f (g n))∣ :: int)" by linarith
    also have "... ≤ ∣f (g (m + n)) - f (g m + g n)∣ + C" using bound[of "g m" "g n"] by auto
    also have "... ≤ ∣f (g (m + n)) - f (g m + g n) - f(g (m + n) - (g m + g n))∣ + ∣f (g (m + n) - (g m + g n))∣ + C" by fastforce
    also have "... ≤ ∣f (g (m + n) - (g m + g n))∣ + 2 * C" using bound[of "g (m + n) - (g m + g n)" "(g m + g n)"] by fastforce
    also have "... ≤ A * ∣g (m + n) - (g m + g n)∣ + B + 2 * C" using f_linear_bound(1)[of "g (m + n) - (g m + g n)"] by linarith
    also have "... ≤ A * C' + B + 2 * C" using mult_left_mono[OF bound'[of m n], OF f_linear_bound(2)] by presburger
    finally have "∣f (g (m + n)) - (f (g m) + f (g n))∣ ≤ A * C' + B + 2 * C" by blast
  }
  thus "slope (f o g)" unfolding comp_def slope_def by (fast intro: boundedI)
qed

lemma slope_scale: "slope ((*) a)" by (auto simp add: slope_def distrib_left intro: boundedI)

lemma slope_zero: "slope (λ_. 0)" using slope_scale[of 0] by (simp add: lambda_zero)

lemma slope_one: "slope id" using slope_scale[of 1] by (simp add: slope_def)

lemma slope_uminus: "slope uminus" using slope_scale[of "-1"] by (simp add: slope_def)

lemma slope_uminus':
  assumes "slope f"
  shows "slope (λx. - f x)"
  using slope_comp[OF slope_uminus assms] by (simp add: slope_def)

lemma slope_minus:
  assumes "slope f" "slope g"
  shows "slope (λx. f x - g x)"
  using slope_add[OF assms(1) slope_uminus', OF assms(2)] by simp

lemma slope_comp_commute:
  assumes "slope f" "slope g"
  shows "bounded (λz. (f o g) z - (g o f) z)"
proof -
  obtain C where bound: "∣z * f (g z) - (g z) * (f z)∣ ≤ (∣z∣ + ∣g z∣ + 2) * C" "0 ≤ C" for z using slope_symmetric_bound[OF assms(1)] by metis
  obtain C' where bound': "∣(f z) * (g z) - z * g (f z)∣ ≤ (∣f z∣ + ∣z∣ + 2) * C'" "0 ≤ C'" for z using slope_symmetric_bound[OF assms(2)] by metis

  obtain A B where f_lbound: "∣f z∣ ≤ A * ∣z∣ + B" "0 ≤ A" "0 ≤ B" for z using slope_linear_bound[OF assms(1)] by blast
  obtain A' B' where g_lbound: "∣g z∣ ≤ A' * ∣z∣ + B'" "0 ≤ A'" "0 ≤ B'" for z using slope_linear_bound[OF assms(2)] by blast

  have combined_bound: "∣z * f (g z) - z * g (f z)∣ ≤ (∣z∣ + ∣g z∣ + 2) * C + (∣f z∣ + ∣z∣ + 2) * C'" for z 
    by (intro order_trans[OF _ add_mono[OF bound(1) bound'(1)]]) (fastforce simp add: mult.commute[of "f z" "g z"])

  {
    fix z
    define D E where "D = (C + C' + A' * C + A * C')" and "E = (2 + B') * C + (2 + B) * C'"
    have E_nonneg: "0 ≤ E" unfolding E_def using g_lbound bound f_lbound bound' by simp
    have D_nonneg: "0 ≤ D" unfolding D_def using g_lbound bound f_lbound bound' by simp

    have "(∣z∣ + ∣g z∣ + 2) * C + (∣f z∣ + ∣z∣ + 2) * C' = ∣z∣ * (C + C') + ∣g z∣ * C + ∣f z∣ * C' + 2 * C + 2 * C'" by algebra
    hence "∣z∣ * ∣f (g z) - g (f z)∣ ≤ ∣z∣ * (C + C') + ∣g z∣ * C + ∣f z∣ * C' + 2 * C + 2 * C'" using combined_bound right_diff_distrib abs_mult by metis
    also have "... ≤ ∣z∣ * (C + C') + (A' * ∣z∣ + B') * C + ∣f z∣ * C' + 2 * C + 2 * C'" using mult_right_mono[OF g_lbound(1)[of z] bound(2)] by presburger
    also have "... ≤ ∣z∣ * (C + C') + (A' * ∣z∣ + B') * C + (A * ∣z∣ + B) * C' + 2 * C + 2 * C'" using mult_right_mono[OF f_lbound(1)[of z] bound'(2)] by presburger
    also have "... = ∣z∣ * (C + C' + A' * C + A * C') + (2 + B') * C + (2 + B) * C'" by algebra
    finally have *: "∣z∣ * ∣f (g z) - g (f z)∣ ≤ ∣z∣ * D + E" unfolding D_def E_def by presburger
    have "∣f (g z) - g (f z)∣ ≤ D + E + ∣f (g 0) - g (f 0)∣"
    proof (cases "z = 0")
      case True
      then show ?thesis using D_nonneg E_nonneg by fastforce
    next
      case False
      have "∣z∣ * ∣f (g z) - g (f z)∣ ≤ ∣z∣ * (D + E)" 
        using mult_right_mono[OF Ints_nonzero_abs_ge1[OF _ False] E_nonneg] distrib_left[of "∣z∣" D E] *
        by (simp add: Ints_def)
      hence "∣f (g z) - g (f z)∣ ≤ D + E" using False by simp
      thus ?thesis by linarith
    qed
  }
  thus ?thesis by (fastforce intro: boundedI)
qed

lemma int_set_infiniteI:
  assumes "∧C. C ≥ 0 ==> ∃N≥C. N ∈ (A :: int set)" 
  shows "infinite A"
  by (meson assms abs_ge_zero abs_le_iff gt_ex le_cSup_finite linorder_not_less order_less_le_trans)

lemma int_set_infiniteD:
  assumes "infinite (A :: int set)" "C ≥ 0"
  obtains z where "z ∈ A" "C ≤ ∣z∣"
proof -
  {
    assume asm: "∀z ∈ A. C > ∣z∣"
    let ?f = "λz. (if z ∈ A then z else (0::int))"
    have bounded: "∀z ∈ A. ∣?f z∣ ≤ C" using asm by fastforce
    moreover have "∀z ∈ UNIV - A. ∣?f z∣ ≤ C" using assms by fastforce
    ultimately have "bounded ?f" by (blast intro: boundedI)
    hence False using bounded_iff_finite_range assms by force
  }
  thus ?thesis using that by fastforce
qed

lemma bounded_odd:
  fixes f :: "int → int"
  assumes "∧z. z < 0 ==> f z = -f (-z)" "∧n. n > 0 ==> ∣f n∣ ≤ C"
  shows "bounded f"
proof -
  have "∣f n∣ ≤ C + ∣f 0∣" if "n ≥ 0" for n using assms by (metis abs_ge_zero abs_of_nonneg add_increasing2 le_add_same_cancel2 that zero_less_abs_iff)
  hence "∣f n∣ ≤ C + ∣f 0∣" for n using assms by (cases "0 ≤ n") fastforce+
  thus ?thesis by (rule boundedI)
qed

lemma slope_odd: 
  assumes "∧z. z < 0 ==> f z = - f (- z)" 
          "∧m n. [m > 0; n > 0] ==> ∣f (m + n) - (f m + f n)∣ ≤ C"
  shows "slope f"
proof -
  define C' where "C' = C + ∣f 0∣"
  have "C ≥ 0" using assms(2)[of 1 1] by simp
  hence bound: "∣f (m + n) - (f m + f n)∣ ≤ C'" if "m ≥ 0" "n ≥ 0" for m n 
    unfolding C'_def using assms(2) that 
    by (cases "m = 0 ∨ n = 0") (force, metis abs_ge_zero add_increasing2 order_le_less)
  {
    fix m n
    have "∣f (m + n) - (f m + f n)∣ ≤ C'"
    proof (cases "m ≥ 0")
      case m_nonneg: True
      show ?thesis
      proof (cases "n ≥ 0")
        case True
        thus ?thesis using bound m_nonneg by fast
      next
        case False
        hence f_n: "f n = - f (- n)" using assms by simp
        show ?thesis
        proof (cases "m + n ≥ 0")
          case True
          have "∣f (m + n) - (f m + f n)∣ = ∣f (m + n + -n) - (f (m + n) + f (-n))∣" using f_n by auto
          thus ?thesis using bound[OF True] by (metis False neg_0_le_iff_le nle_le)
        next
          case False
          hence "f (m + n) = - f (- (m + n))" using assms by force
          hence "∣f (m + n) - (f m + f n)∣ = ∣f (- (m + n) + m) - (f (- (m + n)) + f m)∣" using f_n by force
          thus ?thesis using m_nonneg bound[of "- (m + n)" m] False by simp
        qed
      qed
    next
      case m_neg: False
      hence f_m: "f m = - f (- m)" using assms by simp
      show ?thesis
      proof (cases "n ≥ 0")
        case True
        show ?thesis
        proof (cases "m + n ≥ 0")
          case True
          have "∣f (m + n) - (f m + f n)∣ = ∣f (m + n + -m) - (f (m + n) + f (-m))∣" using f_m by force
          thus ?thesis using bound[OF True, of "- m"] m_neg by simp
        next
          case False
          hence "f (m + n) = - f (- (m + n))" using assms by force
          hence"∣f (m + n) - (f m + f n)∣ = ∣f (- (m + n) + n) - (f (- (m + n)) + f n)∣" using f_m by force
          thus ?thesis using bound[of "- (m + n)" n] True False by simp
        qed
      next
        case False
        hence f_n: "f n = - f (- n)" using assms by simp
        have "f (m + n) = - f (- m + - n)" using m_neg False assms by fastforce
        hence "∣f (m + n) - (f m + f n)∣ = ∣- f (- m + -n) - (- f (-m) + - f(- n))∣" using f_m f_n by argo
        also have "... = ∣f (-m + -n) - (f (-m) + f(-n))∣" by linarith
        finally show ?thesis using bound[of "- m" "- n"] False m_neg by simp
      qed
    qed
  }
  thus ?thesis unfolding slope_def by (fast intro: boundedI)
qed

lemma slope_bounded_comp_right_abs:
  assumes "slope f" "bounded (f o abs)"
  shows "bounded f"
proof -
  obtain B where "∀z. ∣f ∣z∣∣ ≤ B" and B_nonneg: "0 ≤ B" using assms by fastforce
  hence B_bound: "∀z ≥ 0. ∣f z∣ ≤ B" by (metis abs_of_nonneg)

  obtain D where D_bound: "∣f (m + n) - (f m + f n)∣ ≤ D" and D_nonneg: "0 ≤ D" for m n using assms by fast

  have bound: "∣f (-m)∣ ≤ ∣f 0∣ + B + D" if "m ≥ 0" for m using D_bound[of "-m" m] B_bound that by auto

  have "∣f z∣ ≤ ∣f 0∣ + B + D" for z using B_bound B_nonneg D_nonneg bound[of "-z"] by (cases "z ≥ 0") fastforce+
  thus "bounded f" by (rule boundedI)
qed

corollary slope_finite_range_iff:
  assumes "slope f"
  shows "finite (range f) ⟷ finite (f ` {0..})" (is "?lhs ⟷ ?rhs")
proof (rule iffI)
  assume asm: ?rhs
  have "range (f o abs) = f ` {0..}" unfolding comp_def atLeast_def image_def by (metis UNIV_I abs_ge_zero abs_of_nonneg mem_Collect_eq)
  thus ?lhs using slope_bounded_comp_right_abs[OF assms] asm by (fastforce simp add: bounded_iff_finite_range)
qed (metis image_subsetI rangeI finite_subset)

lemma slope_positive_lower_bound:
  assumes "slope f" "infinite (f ` {0..} ∩ {0<..})" "D > 0"
  obtains M where "M > 0" "∧m. m > 0 ==> (m + 1) * D ≤ f (m * M)"
proof -
  {
    have D_nonneg: "D ≥ 0" using assms by force
    obtain C where C_bound: "∣f (m + n) - (f m + f n)∣ ≤ C" and C_nonneg: "0 ≤ C" for m n using assms by fast

    obtain f_M where "2 * (C + D) ≤ ∣f_M∣" "f_M ∈ (f ` {0..} ∩ {0<..})" using mult_left_mono[of "C + D" _ 2] D_nonneg by (metis assms(2) abs_ge_zero abs_le_D1 int_set_infiniteD)
    then obtain M where M_bound: "2 * (C + D) ≤ ∣f M∣" "0 < f M" and M_nonneg: "0 ≤ M" by blast
  
    have neg_bound: "(f (m * M + M) - (f (m * M) + f M)) ≥ -C" for m by (metis C_bound abs_diff_le_iff minus_int_code(1,2))
    hence neg_bound': "(f (m * M + M) - (f (m * M) + f M)) ≥ -(C + D)" for m by (meson D_nonneg add_increasing2 minus_le_iff)
  
    have *: "m > 0 ==> f (m * M) ≥ (m + 1) * (C + D)" for m
    proof (induction m rule: int_induct[where ?k=1])
      case base
      show ?case using M_bound by fastforce
    next
      case (step1 m)
      have "(m + 1 + 1) * (C + D) = (m + 1) * (C + D) + 2 * (C + D) - (C + D)" by algebra
      also have "... ≤ (m + 1) * (C + D) + f M + - (C + D)" using M_bound by fastforce
      also have "... ≤ f (m * M) + f M + - (C + D)" using step1 by simp
      also have "... ≤ (f (m * M) + f M) + (f (m * M + M) - (f (m * M) + f M))" using add_left_mono[OF neg_bound'] by blast
      also have "... = f ((m + 1) * M)" by (simp add: distrib_right)
      finally show ?case by blast
    next
      case (step2 i)
      then show ?case by linarith
    qed
  
    have *: "f (m * M) ≥ (m + 1) * D" if "m > 0" for m using *[OF that] mult_left_mono[of D "C + D" "m + 1"] that C_nonneg D_nonneg by linarith
    moreover have "M ≠ 0" using M_bound add1_zle_eq assms neg_bound by force
    ultimately have "∃M>0. ∀m>0. (m + 1) * D ≤ f (m * M) " using M_nonneg by force
  }
  thus ?thesis using that by blast
qed

subsection ‹Set Membership of term‹Inf› and term‹Sup› on Integers›

lemma int_Inf_mem:
  fixes S :: "int set"
  assumes "S ≠ {}" "bdd_below S"
  shows "Inf S ∈ S"
proof -
  have nonneg: "Inf ({0..} ∩ A) ∈ ({0..} ∩ A)" if asm: "({(0::int)..} ∩ A) ≠ {}" for A
  proof -
    have "nat ` ({0..} ∩ A) ≠ {}" using asm by blast
    hence "int (Inf (nat ` ({0..} ∩ A))) ∈ int ` nat ` ({0..} ∩ A)" using wellorder_InfI[of _ "nat ` ({0..} ∩ A)"] by fast
    moreover have "int ` nat ` ({0..} ∩ A) = {0..} ∩ A" by force
    moreover have "Inf ({0..} ∩ A) = int (Inf (nat ` ({0..} ∩ A)))" 
      using calculation by (intro cInf_eq_minimum) (argo, metis IntD2 Int_commute atLeast_iff imageI le_nat_iff wellorder_Inf_le1)
    ultimately show ?thesis by argo
  qed
  have **: "Inf ({b..} ∩ A) ∈ ({b..} ∩ A)" if asm: "({(b::int)..} ∩ A) ≠ {}" for A b
  proof (cases "b ≥ 0")
    case True
    hence "({b..} ∩ A) = {0..} ∩ ({b..} ∩ A)" by fastforce
    thus ?thesis using asm nonneg by metis
  next
    case False
    hence partition: "({b..} ∩ A) = ({0..} ∩ A) ∪ ({b..<0} ∩ A)" by fastforce
    have bdd_below: "bdd_below ({0..} ∩ A)" "bdd_below ({b..<0} ∩ A)" by simp+
    thus ?thesis 
    proof (cases "({0..} ∩ A) ≠ {} ∧ ({b..<0} ∩ A) ≠ {}")
      case True
      have finite: "finite ({b..<0} ∩ A)" by blast
      have "(x :: int) ≤ y ==> inf x y = x" for x y by (simp add: inf.order_iff)
      have "Inf ({b..} ∩ A) = inf (Inf ({0..} ∩ A)) (Inf ({b..<0} ∩ A))" by (metis cInf_union_distrib True bdd_below partition)
      moreover have "Inf ({b..<0} ∩ A) ∈ ({b..} ∩ A)" using Min_in[OF finite] cInf_eq_Min[OF finite] True partition by simp
      moreover have "Inf ({0..} ∩ A) ∈ ({b..} ∩ A)" using nonneg True partition by blast
      moreover have "inf (Inf ({0..} ∩ A)) (Inf ({b..<0} ∩ A)) ∈ {Inf ({0..} ∩ A), Inf ({b..<0} ∩ A)}" by (metis inf.commute inf.order_iff insertI1 insertI2 nle_le)
      ultimately show ?thesis by force
    next
      case False
      hence "({b..} ∩ A) = ({0..} ∩ A) ∨ ({b..} ∩ A) = ({b..<0} ∩ A)" using partition by auto
      thus ?thesis using Min_in[of "{b..} ∩ A"] cInf_eq_Min[of "{b..} ∩ A"] by (metis asm nonneg finite_Int finite_atLeastLessThan_int)
    qed
  qed
  obtain b where "S = {b..} ∩ S" using assms unfolding bdd_below_def by blast
  thus ?thesis using ** assms by metis
qed

lemma int_Sup_mem:
  fixes S :: "int set"
  assumes "S ≠ {}" "bdd_above S"
  shows "Sup S ∈ S"
proof -
  have "Sup S = (- Inf (uminus ` S))" unfolding Inf_int_def image_comp by simp
  moreover have "bdd_below (uminus ` S)" using assms unfolding bdd_below_def bdd_above_def by (metis imageE neg_le_iff_le)
  moreover have "Inf (uminus ` S) ∈ (uminus ` S)" using int_Inf_mem assms by simp
  ultimately show ?thesis by force
qed

end