Theory Simplex_Algebra

(* Authors: F. Maric, M. Spasic *)
section ‹Linearly Ordered Rational Vectors›
theory Simplex_Algebra
  imports 
    HOL.Rat 
    HOL.Real_Vector_Spaces
begin

class scaleRat =
  fixes scaleRat :: "rat ⇒ 'a ⇒ 'a" (infixr ‹*R› 75)
begin

abbreviation
  divideRat :: "'a ⇒ rat ⇒ 'a" (infixl ‹'/R› 70)
  where
    "x /R r == scaleRat (inverse r) x"
end

class rational_vector = scaleRat + ab_group_add + 
  assumes scaleRat_right_distrib: "scaleRat a (x + y) = scaleRat a x + scaleRat a y"
    and scaleRat_left_distrib: "scaleRat (a + b) x = scaleRat a x + scaleRat b x"
    and scaleRat_scaleRat: "scaleRat a (scaleRat b x) = scaleRat (a * b) x"
    and scaleRat_one: "scaleRat 1 x = x" 

interpretation rational_vector:
  vector_space "scaleRat :: rat ⇒ 'a ⇒ 'a::rational_vector"
  by (unfold_locales) (simp_all add: scaleRat_right_distrib  scaleRat_left_distrib scaleRat_scaleRat scaleRat_one)

class ordered_rational_vector = rational_vector + order

class linordered_rational_vector = ordered_rational_vector + linorder +
  assumes plus_less: "(a::'a) < b ⟹ a + c < b + c" and
    scaleRat_less1: "⟦(a::'a) < b; k > 0⟧ ⟹ (k *R a) < (k *R b)" and 
    scaleRat_less2: "⟦(a::'a) < b; k < 0⟧ ⟹ (k *R a) > (k *R b)"
begin 

lemma scaleRat_leq1: "⟦ a ≤ b; k > 0⟧ ⟹ k *R a ≤ k *R b"
  unfolding le_less
  using scaleRat_less1[of a b k]
  by auto

lemma scaleRat_leq2: "⟦ a ≤ b; k < 0⟧ ⟹ k *R a ≥ k *R b"
  unfolding le_less
  using scaleRat_less2[of a b k]
  by auto

lemma zero_scaleRat
  [simp]: "0 *R v = zero"
  using scaleRat_left_distrib[of 0 0 v]
  by auto

lemma scaleRat_zero
  [simp]: "a *R (0::'a) = 0"
  using scaleRat_right_distrib[of a 0 0]
  by auto

lemma scaleRat_uminus [simp]:
  "-1 *R x = - (x :: 'a)"
proof-
  have "0  = -1 *R x + x"
    using scaleRat_left_distrib[of "-1" 1 x]
    by (simp add: scaleRat_one)
  have "-x = 0 - x"
    by simp
  then have "-x = -1 *R x + x - x"
    using ‹0  = -1 *R x + x›
    by simp
  then show ?thesis
    by (simp add: add_assoc)
qed

lemma minus_lt: "(a::'a) < b ⟷ a - b < 0"
  using plus_less[of a b "-b"]
  using plus_less[of "a - b" 0 b]
  by (auto simp add: add_assoc)

lemma minus_gt: "(a::'a) < b ⟷ 0 < b - a"
  using plus_less[of a b "-a"]
  using plus_less[of 0 "b-a" a]
  by (auto simp add: add_assoc)

lemma minus_leq:
  "(a::'a) ≤ b ⟷ a - b ≤ 0"
proof-
  have *: "a ≤ b ⟹ a - b ≤ (0 :: 'a)"
    using minus_gt[of a b]
    using scaleRat_less2[of 0 "b-a" "-1"]
    by (auto simp add: not_less_iff_gr_or_eq)
  have **: "a - b ≤ 0 ⟹ a ≤ b"
  proof-
    assume "a - b ≤ 0"
    show ?thesis
    proof(cases "a - b < 0")
      case True
      then show ?thesis
        using plus_less[of "a - b" 0 b]
        by (simp add: add_assoc )
    next
      case False
      then show ?thesis
        using ‹a - b ≤ 0›
        by (simp add:antisym_conv1)
    qed
  qed
  show ?thesis
    using * **
    by auto
qed

lemma minus_geq: "(a::'a) ≤ b ⟷ 0 ≤ b - a"
proof-
  have *: "a ≤ b ⟹ 0 ≤ b - a"
    using minus_gt[of a b]
    by (auto simp add: not_less_iff_gr_or_eq)
  have **: "0 ≤ b - a ⟹ a ≤ b"
  proof-
    assume "0 ≤ b - a"
    show ?thesis
    proof(cases "0 < b - a")
      case True
      then show ?thesis
        using plus_less[of 0 "b - a" a]
        by (simp add: add_assoc)
    next
      case False
      then show ?thesis
        using ‹0 ≤ b - a›
        using order.eq_iff[of "b - a" 0]
        by auto
    qed
  qed
  show ?thesis
    using * **
    by auto
qed

lemma divide_lt:
  "⟦c *R (a::'a) < b; (c::rat) > 0 ⟧ ⟹ a < (1/c) *R b"
  using scaleRat_less1[of "c *R a" b "1/c"]
  by (simp add: scaleRat_one scaleRat_scaleRat)

lemma divide_gt:
  "⟦c *R (a::'a) > b;(c::rat) > 0⟧ ⟹ a > (1/c) *R b"
  using scaleRat_less1[of b "c *R a" "1/c"]
  by (simp add: scaleRat_one scaleRat_scaleRat)

lemma divide_leq:
  "⟦c *R (a::'a) ≤  b; (c::rat) > 0⟧ ⟹ a ≤ (1/c) *R b"
proof(cases "c *R a < b")
  assume "c > 0"
  case True
  then show ?thesis
    using divide_lt[of c a b]
    using ‹c > 0›
    by simp
next
  assume "c *R a ≤  b" "c > 0"
  case False
  then have *: "c *R a = b"
    using ‹c *R a ≤ b›
    by simp
  then show ?thesis
    using ‹c > 0›
    by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_geq:
  "⟦c *R (a::'a) ≥ b; (c::rat) > 0⟧ ⟹ a ≥ (1/c) *R b"
proof(cases "c *R a > b")
  assume "c > 0"
  case True
  then show ?thesis
    using divide_gt[of b c a]
    using ‹c > 0›
    by simp
next
  assume "c *R a ≥ b" "c > 0"
  case False
  then have *: "c *R a = b"
    using ‹c *R a ≥ b›
    by simp
  then show ?thesis
    using ‹c > 0›
    by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_lt1:
  "⟦c *R (a::'a) < b; (c::rat) < 0⟧ ⟹ a > (1/c) *R b"
  using scaleRat_less2[of "c *R a" b "1/c"]
  by (simp add: scaleRat_scaleRat scaleRat_one)

lemma divide_gt1:
  "⟦c *R (a::'a) > b; (c::rat) < 0 ⟧ ⟹  a < (1/c) *R b"
  using scaleRat_less2[of b "c *R a" "1/c"]
  by (simp add: scaleRat_scaleRat scaleRat_one)

lemma divide_leq1:
  "⟦c *R (a::'a) ≤  b; (c::rat) < 0⟧ ⟹ a ≥ (1/c) *R b"
proof(cases "c *R a < b")
  assume "c < 0"
  case True
  then show ?thesis
    using divide_lt1[of c a b]
    using ‹c < 0›
    by simp
next
  assume "c *R a ≤  b" "c < 0"
  case False
  then have *: "c *R a = b"
    using ‹c *R a ≤ b›
    by simp
  then show ?thesis
    using ‹c < 0›
    by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

lemma divide_geq1:
  "⟦c *R (a::'a) ≥ b; (c::rat) < 0⟧ ⟹ a ≤ (1/c) *R b"
proof(cases "c *R a > b")
  assume "c < 0"
  case True
  then show ?thesis
    using divide_gt1[of b c a]
    using ‹c < 0›
    by simp
next
  assume "c *R a ≥ b" "c < 0"
  case False
  then have *: "c *R a = b"
    using ‹c *R a ≥ b›
    by simp
  then show ?thesis
    using ‹c < 0›
    by (auto simp add: scaleRat_one scaleRat_scaleRat)
qed

end

class lrv = linordered_rational_vector + one +
  assumes zero_neq_one: "0 ≠ 1"

subclass (in linordered_rational_vector) ordered_ab_semigroup_add
proof
  fix a b c
  assume "a ≤ b"
  then show "c + a ≤ c + b"
    using plus_less[of a b c]
    by (auto simp add: add_ac le_less)
qed

instantiation rat :: rational_vector
begin
definition scaleRat_rat :: "rat ⇒ rat ⇒ rat" where
  [simp]: "x *R y = x * y"
instance by standard (auto simp add: field_simps)
end

instantiation rat :: ordered_rational_vector
begin
instance ..
end

instantiation rat :: linordered_rational_vector
begin
instance by standard (auto simp add: field_simps)
end

instantiation rat :: lrv
begin
instance by standard (auto simp add: field_simps)
end

lemma uminus_less_lrv[simp]: fixes a b :: "'a :: lrv"
  shows "- a < - b ⟷ b < a" 
proof -
  have "(- a < - b) = (-1 *R a < -1 *R b)" by simp
  also have "… ⟷ (b < a)" 
    using scaleRat_less2[of _ _ "-1"] scaleRat_less2[of "-1 *R a" "-1 *R b" "-1"] by auto 
  finally show ?thesis .
qed

end