theory Convexity
imports Complex_Main
begin

text {* Real interval *}

definition
  real_interval :: "real set => bool" where
  "real_interval S \<longleftrightarrow>
    (\<forall>x y alpha. 0 \<le> alpha & alpha \<le> 1 & x : S & y : S \<longrightarrow>
      alpha * x + (1 - alpha) * y : S)"

lemma real_intervalI:
  "(\<And>x y alpha. 0 \<le> alpha \<Longrightarrow> alpha \<le> 1 \<Longrightarrow> x : S \<Longrightarrow> y : S \<Longrightarrow>
      alpha * x + (1 - alpha) * y : S) \<Longrightarrow> real_interval S"
  unfolding real_interval_def by simp

lemma real_intervalE:
  "real_interval S \<Longrightarrow>
    0 \<le> alpha \<Longrightarrow> alpha \<le> 1 \<Longrightarrow> x : S \<Longrightarrow> y : S \<Longrightarrow>
    alpha * x + (1 - alpha) * y : S"
  unfolding real_interval_def by simp


lemmas real_simps = Ring_and_Field.mult_mono_class.mult_left_mono
  Ring_and_Field.mult_mono_class.mult_right_mono
  RealVector.mult.diff_right RealVector.mult.diff_left


text {* Real interval -- Continuity properties *}

lemma cont_interval:
  fixes a b x :: "real"
  fixes S :: "real set"
  assumes 1: "real_interval S"
  assumes 2: "a : S" "b : S"
  assumes 3: "a <= x" "x <= b"
  shows "x : S"
proof (rule linorder_cases)
  assume "a = b"
  with 3 have "x = a" by auto
  with `a : S` show ?thesis by simp
next
  assume 4: "a < b"
  def alpha == "(b - x) / (b - a)"
  then have "0 <= alpha" and "alpha <= 1" using 3 4
    by (simp_all add: real_0_le_divide_iff)
  with 1 have "(alpha * a + (1 - alpha) * b) : S" using 2
    by (rule real_intervalE)
  moreover
  have "alpha * (b - a) = b - x" using alpha_def 4 by simp
  then have "x = alpha * a + (1 - alpha) * b" by (simp add: real_simps)
  ultimately show "x : S" by metis
next
  assume "a > b"
  with 3 have False by simp
  then show ?thesis ..
qed


end