Theory Extra_Ordered_Fields

section ‹‹Extra_Ordered_Fields› -- Additional facts about ordered fields›

theory Extra_Ordered_Fields
  imports Complex_Main "HOL-Library.Complex_Order"
begin


subsection‹Ordered Fields›
text ‹In this section we introduce some type classes for ordered rings/fields/etc.
that are weakenings of existing classes. Most theorems in this section are
copies of the eponymous theorems from Isabelle/HOL, except that they are now proven
requiring weaker type classes (usually the need for a total order is removed).

Since the lemmas are identical to the originals except for weaker type constraints,
we use the same names as for the original lemmas. (In fact, the new lemmas could replace
the original ones in Isabelle/HOL with at most minor incompatibilities.›

subsection ‹Missing from Orderings.thy›

text ‹This class is analogous to \<^class>‹unbounded_dense_linorder›, except that it does not require a total order›

class unbounded_dense_order = dense_order + no_top + no_bot

instance unbounded_dense_linorder ⊆ unbounded_dense_order ..

subsection ‹Missing from Rings.thy›

text ‹The existing class \<^class>‹abs_if› requires \<^term>‹¦a¦ = (if a < 0 then - a else a)›.
However, if \<^term>‹(<)› is not a total order, this condition is too strong when \<^term>‹a›
is incomparable with \<^term>‹0›. (Namely, it requires the absolute value to be
the identity on such elements. E.g., the absolute value for complex numbers does not
satisfy this.) The following class ‹partial_abs_if› is analogous to \<^class>‹abs_if›
but does not require anything if \<^term>‹a› is incomparable with \<^term>‹0›.›


class partial_abs_if = minus + uminus + ord + zero + abs +
  assumes abs_neg: "a ≤ 0 ⟹ abs a = -a"
  assumes abs_pos: "a ≥ 0 ⟹ abs a = a"

class ordered_semiring_1 = ordered_semiring + semiring_1
  ― ‹missing class analogous to \<^class>‹linordered_semiring_1› without requiring a total order›
begin

lemma convex_bound_le:
  assumes "x ≤ a" and "y ≤ a" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
  shows "u * x + v * y ≤ a"
proof-
  from assms have "u * x + v * y ≤ u * a + v * a"
    by (simp add: add_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1) ordered_semiring_1 ..

class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
  ― ‹missing class analogous to \<^class>‹linordered_semiring_strict› without requiring a total order›
  assumes mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
  assumes mult_strict_right_mono: "a < b ⟹ 0 < c ⟹ a * c < b * c"
begin

subclass semiring_0_cancel ..

subclass ordered_semiring
proof
  fix a b c :: 'a
  assume t1: "a ≤ b" and t2: "0 ≤ c"
  thus "c * a ≤ c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
  from t2 show "a * c ≤ b * c"
    unfolding le_less
    by (metis local.antisym_conv2 local.mult_not_zero local.mult_strict_right_mono t1)
qed

lemma mult_pos_pos[simp]: "0 < a ⟹ 0 < b ⟹ 0 < a * b"
  using mult_strict_left_mono [of 0 b a] by simp

lemma mult_pos_neg: "0 < a ⟹ b < 0 ⟹ a * b < 0"
  using mult_strict_left_mono [of b 0 a] by simp

lemma mult_neg_pos: "a < 0 ⟹ 0 < b ⟹ a * b < 0"
  using mult_strict_right_mono [of a 0 b] by simp

text ‹Strict monotonicity in both arguments›
lemma mult_strict_mono:
  assumes t1: "a < b" and t2: "c < d" and t3: "0 < b" and t4: "0 ≤ c"
  shows "a * c < b * d"
proof-
  have "a * c < b * d"
    by (metis local.dual_order.order_iff_strict local.dual_order.strict_trans2
        local.mult_strict_left_mono local.mult_strict_right_mono local.mult_zero_right t1 t2 t3 t4)
  thus ?thesis
    using assms by blast
qed


text ‹This weaker variant has more natural premises›
lemma mult_strict_mono':
  assumes "a < b" and "c < d" and "0 ≤ a" and "0 ≤ c"
  shows "a * c < b * d"
  by (rule mult_strict_mono) (insert assms, auto)

lemma mult_less_le_imp_less:
  assumes t1: "a < b" and t2: "c ≤ d" and t3: "0 ≤ a" and t4: "0 < c"
  shows "a * c < b * d"
  using local.mult_strict_mono' local.mult_strict_right_mono local.order.order_iff_strict
    t1 t2 t3 t4 by auto

lemma mult_le_less_imp_less:
  assumes "a ≤ b" and "c < d" and "0 < a" and "0 ≤ c"
  shows "a * c < b * d"
  by (metis assms(1) assms(2) assms(3) assms(4) local.antisym_conv2 local.dual_order.strict_trans1
      local.mult_strict_left_mono local.mult_strict_mono)

end

subclass (in linordered_semiring_strict) ordered_semiring_strict
  apply standard
  by (auto simp: mult_strict_left_mono mult_strict_right_mono)

class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
  ― ‹missing class analogous to \<^class>‹linordered_semiring_1_strict› without requiring
  a total order›
begin

subclass ordered_semiring_1 ..

lemma convex_bound_lt:
  assumes "x < a" and "y < a" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
  shows "u * x + v * y < a"
proof -
  from assms have "u * x + v * y < u * a + v * a"
    by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1_strict) ordered_semiring_1_strict ..

class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
  ― ‹missing class analogous to \<^class>‹linordered_comm_semiring_strict› without requiring a total order›
  assumes comm_mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
begin

subclass ordered_semiring_strict
proof
  fix a b c :: 'a
  assume "a < b" and "0 < c"
  thus "c * a < c * b"
    by (rule comm_mult_strict_left_mono)
  thus "a * c < b * c"
    by (simp only: mult.commute)
qed

subclass ordered_cancel_comm_semiring
proof
  fix a b c :: 'a
  assume "a ≤ b" and "0 ≤ c"
  thus "c * a ≤ c * b"
    unfolding le_less
    using mult_strict_left_mono by (cases "c = 0") auto
qed

end

subclass (in linordered_comm_semiring_strict) ordered_comm_semiring_strict
  apply standard
  by (simp add: local.mult_strict_left_mono)

class ordered_ring_strict = ring + ordered_semiring_strict
  + ordered_ab_group_add + partial_abs_if
  ― ‹missing class analogous to \<^class>‹linordered_ring_strict› without requiring a total order›
begin

subclass ordered_ring ..

lemma mult_strict_left_mono_neg: "b < a ⟹ c < 0 ⟹ c * a < c * b"
  using mult_strict_left_mono [of b a "- c"] by simp

lemma mult_strict_right_mono_neg: "b < a ⟹ c < 0 ⟹ a * c < b * c"
  using mult_strict_right_mono [of b a "- c"] by simp

lemma mult_neg_neg: "a < 0 ⟹ b < 0 ⟹ 0 < a * b"
  using mult_strict_right_mono_neg [of a 0 b] by simp

end

lemmas mult_sign_intros =
  mult_nonneg_nonneg mult_nonneg_nonpos
  mult_nonpos_nonneg mult_nonpos_nonpos
  mult_pos_pos mult_pos_neg
  mult_neg_pos mult_neg_neg


subsection ‹Ordered fields›

class ordered_field = field + order + ordered_comm_semiring_strict + ordered_ab_group_add
  + partial_abs_if
  ― ‹missing class analogous to \<^class>‹linordered_field› without requiring a total order›
begin

lemma frac_less_eq:
  "y ≠ 0 ⟹ z ≠ 0 ⟹ x / y < w / z ⟷ (x * z - w * y) / (y * z) < 0"
  by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )

lemma frac_le_eq:
  "y ≠ 0 ⟹ z ≠ 0 ⟹ x / y ≤ w / z ⟷ (x * z - w * y) / (y * z) ≤ 0"
  by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )

lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff

lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff

text‹Simplify expressions equated with 1›

lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a ⟷ a = 0"
  by (cases "a = 0") (auto simp: field_simps)

lemma one_divide_eq_0_iff [simp]: "1 / a = 0 ⟷ a = 0"
  using zero_eq_1_divide_iff[of a] by simp

text‹Simplify expressions such as ‹0 < 1/x› to ‹0 < x››

text‹Simplify quotients that are compared with the value 1.›

text ‹Conditional Simplification Rules: No Case Splits›

lemma eq_divide_eq_1 [simp]:
  "(1 = b/a) = ((a ≠ 0 & a = b))"
  by (auto simp add: eq_divide_eq)

lemma divide_eq_eq_1 [simp]:
  "(b/a = 1) = ((a ≠ 0 & a = b))"
  by (auto simp add: divide_eq_eq)

end (* class ordered_field *)


text ‹The following type class intends to capture some important properties
  that are common both to the real and the complex numbers. The purpose is
  to be able to state and prove lemmas that apply both to the real and the complex
  numbers without needing to state the lemma twice.
›

class nice_ordered_field = ordered_field + zero_less_one + idom_abs_sgn +
  assumes positive_imp_inverse_positive: "0 < a ⟹ 0 < inverse a"
    and inverse_le_imp_le: "inverse a ≤ inverse b ⟹ 0 < a ⟹ b ≤ a"
    and dense_le: "(⋀x. x < y ⟹ x ≤ z) ⟹ y ≤ z"
    and nn_comparable: "0 ≤ a ⟹ 0 ≤ b ⟹ a ≤ b ∨ b ≤ a"
    and abs_nn: "¦x¦ ≥ 0"
begin

subclass (in linordered_field) nice_ordered_field
proof
  show "¦a¦ = - a"
    if "a ≤ 0"
    for a :: 'a
    using that
    by simp
  show "¦a¦ = a"
    if "0 ≤ a"
    for a :: 'a
    using that
    by simp
  show "0 < inverse a"
    if "0 < a"
    for a :: 'a
    using that
    by simp
  show "b ≤ a"
    if "inverse a ≤ inverse b"
      and "0 < a"
    for a :: 'a
      and b
    using that
    using local.inverse_le_imp_le by blast
  show "y ≤ z"
    if "⋀x::'a. x < y ⟹ x ≤ z"
    for y
      and z
    using that
    using local.dense_le by blast
  show "a ≤ b ∨ b ≤ a"
    if "0 ≤ a"
      and "0 ≤ b"
    for a :: 'a
      and b
    using that
    by auto
  show "0 ≤ ¦x¦"
    for x :: 'a
    by simp
qed

lemma comparable:
  assumes h1: "a ≤ c ∨ a ≥ c"
    and h2: "b ≤ c ∨ b ≥ c"
  shows "a ≤ b ∨ b ≤ a"
proof-
  have "a ≤ b"
    if t1: "¬ b ≤ a" and t2: "a ≤ c" and t3: "b ≤ c"
  proof-
    have "0 ≤ c-a"
      by (simp add: t2)
    moreover have "0 ≤ c-b"
      by (simp add: t3)
    ultimately have "c-a ≤ c-b ∨ c-a ≥ c-b" by (rule nn_comparable)
    hence "-a ≤ -b ∨ -a ≥ -b"
      using local.add_le_imp_le_right local.uminus_add_conv_diff by presburger
    thus ?thesis
      by (simp add: t1)
  qed
  moreover have "a ≤ b"
    if t1: "¬ b ≤ a" and t2: "c ≤ a" and t3: "b ≤ c"
  proof-
    have "b ≤ a"
      using local.dual_order.trans t2 t3 by blast
    thus ?thesis
      using t1 by auto
  qed
  moreover have "a ≤ b"
    if t1: "¬ b ≤ a" and t2: "c ≤ a" and t3: "c ≤ b"
  proof-
    have "0 ≤ a-c"
      by (simp add: t2)
    moreover have "0 ≤ b-c"
      by (simp add: t3)
    ultimately have "a-c ≤ b-c ∨ a-c ≥ b-c" by (rule nn_comparable)
    hence "a ≤ b ∨ a ≥ b"
      by (simp add: local.le_diff_eq)
    thus ?thesis
      by (simp add: t1)
  qed
  ultimately show ?thesis using assms by auto
qed

lemma negative_imp_inverse_negative:
  "a < 0 ⟹ inverse a < 0"
  by (insert positive_imp_inverse_positive [of "-a"],
      simp add: nonzero_inverse_minus_eq less_imp_not_eq)

lemma inverse_positive_imp_positive:
  assumes inv_gt_0: "0 < inverse a" and nz: "a ≠ 0"
  shows "0 < a"
proof -
  have "0 < inverse (inverse a)"
    using inv_gt_0 by (rule positive_imp_inverse_positive)
  thus "0 < a"
    using nz by (simp add: nonzero_inverse_inverse_eq)
qed

lemma inverse_negative_imp_negative:
  assumes inv_less_0: "inverse a < 0" and nz: "a ≠ 0"
  shows "a < 0"
proof-
  have "inverse (inverse a) < 0"
    using inv_less_0 by (rule negative_imp_inverse_negative)
  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
qed

lemma linordered_field_no_lb:
  "∀x. ∃y. y < x"
proof
  fix x::'a
  have m1: "- (1::'a) < 0" by simp
  from add_strict_right_mono[OF m1, where c=x]
  have "(- 1) + x < x" by simp
  thus "∃y. y < x" by blast
qed

lemma linordered_field_no_ub:
  "∀x. ∃y. y > x"
proof
  fix x::'a
  have m1: " (1::'a) > 0" by simp
  from add_strict_right_mono[OF m1, where c=x]
  have "1 + x > x" by simp
  thus "∃y. y > x" by blast
qed

lemma less_imp_inverse_less:
  assumes less: "a < b" and apos:  "0 < a"
  shows "inverse b < inverse a"
  using assms by (metis local.dual_order.strict_iff_order
      local.inverse_inverse_eq local.inverse_le_imp_le local.positive_imp_inverse_positive)

lemma inverse_less_imp_less:
  "inverse a < inverse b ⟹ 0 < a ⟹ b < a"
  using local.inverse_le_imp_le local.order.strict_iff_order by blast

text‹Both premises are essential. Consider -1 and 1.›
lemma inverse_less_iff_less [simp]:
  "0 < a ⟹ 0 < b ⟹ inverse a < inverse b ⟷ b < a"
  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

lemma le_imp_inverse_le:
  "a ≤ b ⟹ 0 < a ⟹ inverse b ≤ inverse a"
  by (force simp add: le_less less_imp_inverse_less)

lemma inverse_le_iff_le [simp]:
  "0 < a ⟹ 0 < b ⟹ inverse a ≤ inverse b ⟷ b ≤ a"
  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)


text‹These results refer to both operands being negative.  The opposite-sign
case is trivial, since inverse preserves signs.›
lemma inverse_le_imp_le_neg:
  "inverse a ≤ inverse b ⟹ b < 0 ⟹ b ≤ a"
  by (metis local.inverse_le_imp_le local.inverse_minus_eq local.neg_0_less_iff_less
      local.neg_le_iff_le)

lemma inverse_less_imp_less_neg:
  "inverse a < inverse b ⟹ b < 0 ⟹ b < a"
  using local.dual_order.strict_iff_order local.inverse_le_imp_le_neg by blast

lemma inverse_less_iff_less_neg [simp]:
  "a < 0 ⟹ b < 0 ⟹ inverse a < inverse b ⟷ b < a"
  by (metis local.antisym_conv2 local.inverse_less_imp_less_neg local.negative_imp_inverse_negative
      local.nonzero_inverse_inverse_eq local.order.strict_implies_order)

lemma le_imp_inverse_le_neg:
  "a ≤ b ⟹ b < 0 ⟹ inverse b ≤ inverse a"
  by (force simp add: le_less less_imp_inverse_less_neg)

lemma inverse_le_iff_le_neg [simp]:
  "a < 0 ⟹ b < 0 ⟹ inverse a ≤ inverse b ⟷ b ≤ a"
  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

lemma one_less_inverse:
  "0 < a ⟹ a < 1 ⟹ 1 < inverse a"
  using less_imp_inverse_less [of a 1, unfolded inverse_1] .

lemma one_le_inverse:
  "0 < a ⟹ a ≤ 1 ⟹ 1 ≤ inverse a"
  using le_imp_inverse_le [of a 1, unfolded inverse_1] .

lemma pos_le_divide_eq [field_simps]:
  assumes "0 < c"
  shows "a ≤ b / c ⟷ a * c ≤ b"
  using assms by (metis local.divide_eq_imp local.divide_inverse_commute
      local.dual_order.order_iff_strict local.dual_order.strict_iff_order
      local.mult_right_mono local.mult_strict_left_mono local.nonzero_divide_eq_eq
      local.order.strict_implies_order local.positive_imp_inverse_positive)

lemma pos_less_divide_eq [field_simps]:
  assumes "0 < c"
  shows "a < b / c ⟷ a * c < b"
  using assms local.dual_order.strict_iff_order local.nonzero_divide_eq_eq local.pos_le_divide_eq
  by auto

lemma neg_less_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a < b / c ⟷ b < a * c"
  by (metis assms local.minus_divide_divide local.mult_minus_right local.neg_0_less_iff_less
      local.neg_less_iff_less local.pos_less_divide_eq)

lemma neg_le_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a ≤ b / c ⟷ b ≤ a * c"
  by (metis assms local.dual_order.order_iff_strict local.dual_order.strict_iff_order
      local.neg_less_divide_eq local.nonzero_divide_eq_eq)

lemma pos_divide_le_eq [field_simps]:
  assumes "0 < c"
  shows "b / c ≤ a ⟷ b ≤ a * c"
  by (metis assms local.dual_order.strict_iff_order local.nonzero_eq_divide_eq
      local.pos_le_divide_eq)

lemma pos_divide_less_eq [field_simps]:
  assumes "0 < c"
  shows "b / c < a ⟷ b < a * c"
  by (metis assms local.minus_divide_left local.mult_minus_left local.neg_less_iff_less
      local.pos_less_divide_eq)

lemma neg_divide_le_eq [field_simps]:
  assumes "c < 0"
  shows "b / c ≤ a ⟷ a * c ≤ b"
  by (metis assms local.minus_divide_left local.mult_minus_left local.neg_le_divide_eq
      local.neg_le_iff_le)

lemma neg_divide_less_eq [field_simps]:
  assumes "c < 0"
  shows "b / c < a ⟷ a * c < b"
  using assms local.dual_order.strict_iff_order local.neg_divide_le_eq by auto

text‹The following ‹field_simps› rules are necessary, as minus is always moved atop of
division but we want to get rid of division.›

lemma pos_le_minus_divide_eq [field_simps]: "0 < c ⟹ a ≤ - (b / c) ⟷ a * c ≤ - b"
  unfolding minus_divide_left by (rule pos_le_divide_eq)

lemma neg_le_minus_divide_eq [field_simps]: "c < 0 ⟹ a ≤ - (b / c) ⟷ - b ≤ a * c"
  unfolding minus_divide_left by (rule neg_le_divide_eq)

lemma pos_less_minus_divide_eq [field_simps]: "0 < c ⟹ a < - (b / c) ⟷ a * c < - b"
  unfolding minus_divide_left by (rule pos_less_divide_eq)

lemma neg_less_minus_divide_eq [field_simps]: "c < 0 ⟹ a < - (b / c) ⟷ - b < a * c"
  unfolding minus_divide_left by (rule neg_less_divide_eq)

lemma pos_minus_divide_less_eq [field_simps]: "0 < c ⟹ - (b / c) < a ⟷ - b < a * c"
  unfolding minus_divide_left by (rule pos_divide_less_eq)

lemma neg_minus_divide_less_eq [field_simps]: "c < 0 ⟹ - (b / c) < a ⟷ a * c < - b"
  unfolding minus_divide_left by (rule neg_divide_less_eq)

lemma pos_minus_divide_le_eq [field_simps]: "0 < c ⟹ - (b / c) ≤ a ⟷ - b ≤ a * c"
  unfolding minus_divide_left by (rule pos_divide_le_eq)

lemma neg_minus_divide_le_eq [field_simps]: "c < 0 ⟹ - (b / c) ≤ a ⟷ a * c ≤ - b"
  unfolding minus_divide_left by (rule neg_divide_le_eq)

lemma frac_less_eq:
  "y ≠ 0 ⟹ z ≠ 0 ⟹ x / y < w / z ⟷ (x * z - w * y) / (y * z) < 0"
  by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )

lemma frac_le_eq:
  "y ≠ 0 ⟹ z ≠ 0 ⟹ x / y ≤ w / z ⟷ (x * z - w * y) / (y * z) ≤ 0"
  by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )


text‹Lemmas ‹sign_simps› is a first attempt to automate proofs
of positivity/negativity needed for ‹field_simps›. Have not added ‹sign_simps› to ‹field_simps›
  because the former can lead to case explosions.›

lemma divide_pos_pos[simp]:
  "0 < x ⟹ 0 < y ⟹ 0 < x / y"
  by(simp add:field_simps)

lemma divide_nonneg_pos:
  "0 ≤ x ⟹ 0 < y ⟹ 0 ≤ x / y"
  by(simp add:field_simps)

lemma divide_neg_pos:
  "x < 0 ⟹ 0 < y ⟹ x / y < 0"
  by(simp add:field_simps)

lemma divide_nonpos_pos:
  "x ≤ 0 ⟹ 0 < y ⟹ x / y ≤ 0"
  by(simp add:field_simps)

lemma divide_pos_neg:
  "0 < x ⟹ y < 0 ⟹ x / y < 0"
  by(simp add:field_simps)

lemma divide_nonneg_neg:
  "0 ≤ x ⟹ y < 0 ⟹ x / y ≤ 0"
  by(simp add:field_simps)

lemma divide_neg_neg:
  "x < 0 ⟹ y < 0 ⟹ 0 < x / y"
  by(simp add:field_simps)

lemma divide_nonpos_neg:
  "x ≤ 0 ⟹ y < 0 ⟹ 0 ≤ x / y"
  by(simp add:field_simps)

lemma divide_strict_right_mono:
  "a < b ⟹ 0 < c ⟹ a / c < b / c"
  by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
      positive_imp_inverse_positive)


lemma divide_strict_right_mono_neg:
  "b < a ⟹ c < 0 ⟹ a / c < b / c"
  by (simp add: local.neg_less_divide_eq)

text‹The last premise ensures that \<^term>‹a› and \<^term>‹b›
      have the same sign›
lemma divide_strict_left_mono:
  "b < a ⟹ 0 < c ⟹ 0 < a*b ⟹ c / a < c / b"
  by (metis local.divide_neg_pos local.dual_order.strict_iff_order local.frac_less_eq local.less_iff_diff_less_0 local.mult_not_zero local.mult_strict_left_mono)

lemma divide_left_mono:
  "b ≤ a ⟹ 0 ≤ c ⟹ 0 < a*b ⟹ c / a ≤ c / b"
  using local.divide_cancel_left local.divide_strict_left_mono local.dual_order.order_iff_strict by auto

lemma divide_strict_left_mono_neg:
  "a < b ⟹ c < 0 ⟹ 0 < a*b ⟹ c / a < c / b"
  by (metis local.divide_strict_left_mono local.minus_divide_left local.neg_0_less_iff_less local.neg_less_iff_less mult_commute)

lemma mult_imp_div_pos_le: "0 < y ⟹ x ≤ z * y ⟹ x / y ≤ z"
  by (subst pos_divide_le_eq, assumption+)

lemma mult_imp_le_div_pos: "0 < y ⟹ z * y ≤ x ⟹ z ≤ x / y"
  by(simp add:field_simps)

lemma mult_imp_div_pos_less: "0 < y ⟹ x < z * y ⟹ x / y < z"
  by(simp add:field_simps)

lemma mult_imp_less_div_pos: "0 < y ⟹ z * y < x ⟹ z < x / y"
  by(simp add:field_simps)

lemma frac_le: "0 ≤ x ⟹ x ≤ y ⟹ 0 < w ⟹ w ≤ z  ⟹ x / z ≤ y / w"
  using local.mult_imp_div_pos_le local.mult_imp_le_div_pos local.mult_mono by auto

lemma frac_less: "0 ≤ x ⟹ x < y ⟹ 0 < w ⟹ w ≤ z ⟹ x / z < y / w"
proof-
  assume a1: "w ≤ z"
  assume a2: "0 < w"
  assume a3: "0 ≤ x"
  assume a4: "x < y"
  have f5: "a = 0 ∨ (b = c / a) = (b * a = c)"
    for a b c::'a
    by (meson local.nonzero_eq_divide_eq)
  have f6: "0 < z"
    using a2 a1 less_le_trans by blast
  have "z ≠ 0"
    using a2 a1 by (meson local.leD)
  moreover have "x / z ≠ y / w"
    using a1 a2 a3 a4 local.frac_eq_eq local.mult_less_le_imp_less by fastforce
  ultimately have "x / z ≠ y / w"
    using f5 by (metis (no_types))
  thus ?thesis
    using a4 a3 a2 a1 by (meson local.frac_le local.order.not_eq_order_implies_strict
        local.order.strict_implies_order)
qed


lemma frac_less2: "0 < x ⟹ x ≤ y ⟹ 0 < w ⟹ w < z  ⟹ x / z < y / w"
  by (metis local.antisym_conv2 local.divide_cancel_left local.dual_order.strict_implies_order
      local.frac_le local.frac_less)

lemma less_half_sum: "a < b ⟹ a < (a+b) / (1+1)"
  by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_less_div_pos local.semiring_normalization_rules(4) local.zero_less_one mult_commute)

lemma gt_half_sum: "a < b ⟹ (a+b)/(1+1) < b"
  by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_div_pos_less local.semiring_normalization_rules(24) local.semiring_normalization_rules(4) local.zero_less_one mult_commute)

subclass unbounded_dense_order
proof
  fix x y :: 'a
  have less_add_one: "a < a + 1" for a::'a by auto
  from less_add_one show "∃y. x < y"
    by blast

  from less_add_one have "x + (- 1) < (x + 1) + (- 1)"
    by (rule add_strict_right_mono)
  hence "x - 1 < x + 1 - 1" by simp
  hence "x - 1 < x" by (simp add: algebra_simps)
  thus "∃y. y < x" ..
  show "x < y ⟹ ∃z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
qed


lemma dense_le_bounded:
  fixes x y z :: 'a
  assumes "x < y"
    and *: "⋀w. ⟦ x < w ; w < y ⟧ ⟹ w ≤ z"
  shows "y ≤ z"
proof (rule dense_le)
  fix w assume "w < y"
  from dense[OF ‹x < y›] obtain u where "x < u" "u < y" by safe
  have "u ≤ w ∨ w ≤ u"
    using ‹u < y› ‹w < y› comparable local.order.strict_implies_order by blast
  thus "w ≤ z"
    using "*" ‹u < y› ‹w < y› ‹x < u› local.dual_order.trans local.order.strict_trans2 by blast
qed

subclass field_abs_sgn ..


lemma nonzero_abs_inverse:
  "a ≠ 0 ⟹ ¦inverse a¦ = inverse ¦a¦"
  by (rule abs_inverse)

lemma nonzero_abs_divide:
  "b ≠ 0 ⟹ ¦a / b¦ = ¦a¦ / ¦b¦"
  by (rule abs_divide)

lemma field_le_epsilon:
  assumes e: "⋀e. 0 < e ⟹ x ≤ y + e"
  shows "x ≤ y"
proof (rule dense_le)
  fix t assume "t < x"
  hence "0 < x - t" by (simp add: less_diff_eq)
  from e [OF this] have "x + 0 ≤ x + (y - t)" by (simp add: algebra_simps)
  hence "0 ≤ y - t" by (simp only: add_le_cancel_left)
  thus "t ≤ y" by (simp add: algebra_simps)
qed

lemma inverse_positive_iff_positive [simp]:
  "(0 < inverse a) = (0 < a)"
  using local.positive_imp_inverse_positive by fastforce

lemma inverse_negative_iff_negative [simp]:
  "(inverse a < 0) = (a < 0)"
  using local.negative_imp_inverse_negative by fastforce

lemma inverse_nonnegative_iff_nonnegative [simp]:
  "0 ≤ inverse a ⟷ 0 ≤ a"
  by (simp add: local.dual_order.order_iff_strict)

lemma inverse_nonpositive_iff_nonpositive [simp]:
  "inverse a ≤ 0 ⟷ a ≤ 0"
  using local.inverse_nonnegative_iff_nonnegative local.neg_0_le_iff_le by fastforce

lemma one_less_inverse_iff: "1 < inverse x ⟷ 0 < x ∧ x < 1"
  using less_trans[of 1 x 0 for x]
  by (metis local.dual_order.strict_trans local.inverse_1 local.inverse_less_imp_less local.inverse_positive_iff_positive local.one_less_inverse local.zero_less_one)

lemma one_le_inverse_iff: "1 ≤ inverse x ⟷ 0 < x ∧ x ≤ 1"
  by (metis local.dual_order.strict_trans1 local.inverse_1 local.inverse_le_imp_le local.inverse_positive_iff_positive local.one_le_inverse local.zero_less_one)

lemma inverse_less_1_iff: "inverse x < 1 ⟷ x ≤ 0 ∨ 1 < x"
proof (rule)
  assume invx1: "inverse x < 1"
  have "inverse x ≤ 0 ∨ inverse x ≥ 0"
    using comparable invx1 local.order.strict_implies_order local.zero_less_one by blast
  then consider (leq0) "inverse x ≤ 0" | (pos) "inverse x > 0" | (zero) "inverse x = 0"
    using local.antisym_conv1 by blast
  thus "x ≤ 0 ∨ 1 < x"
    by (metis invx1 local.eq_refl local.inverse_1 inverse_less_imp_less
              inverse_nonpositive_iff_nonpositive inverse_positive_iff_positive)
next
  assume "x ≤ 0 ∨ 1 < x"
  then consider (neg) "x ≤ 0" | (g1) "1 < x" by auto
  thus "inverse x < 1"
    by (metis local.dual_order.not_eq_order_implies_strict local.dual_order.strict_trans
        local.inverse_1 local.inverse_negative_iff_negative local.inverse_zero
        local.less_imp_inverse_less local.zero_less_one)
qed

lemma inverse_le_1_iff: "inverse x ≤ 1 ⟷ x ≤ 0 ∨ 1 ≤ x"
  by (metis local.dual_order.order_iff_strict local.inverse_1 local.inverse_le_iff_le
      local.inverse_less_1_iff local.one_le_inverse_iff)

text‹Simplify expressions such as ‹0 < 1/x› to ‹0 < x››

lemma zero_le_divide_1_iff [simp]:
  "0 ≤ 1 / a ⟷ 0 ≤ a"
  using local.dual_order.order_iff_strict local.inverse_eq_divide
    local.inverse_positive_iff_positive by auto

lemma zero_less_divide_1_iff [simp]:
  "0 < 1 / a ⟷ 0 < a"
  by (simp add: local.dual_order.strict_iff_order)

lemma divide_le_0_1_iff [simp]:
  "1 / a ≤ 0 ⟷ a ≤ 0"
  by (smt local.abs_0 local.abs_1 local.abs_divide local.abs_neg local.abs_nn
      local.divide_cancel_left local.le_minus_iff local.minus_divide_right local.zero_neq_one)

lemma divide_less_0_1_iff [simp]:
  "1 / a < 0 ⟷ a < 0"
  using local.dual_order.strict_iff_order by auto

lemma divide_right_mono:
  "a ≤ b ⟹ 0 ≤ c ⟹ a/c ≤ b/c"
  using local.divide_cancel_right local.divide_strict_right_mono local.dual_order.order_iff_strict by blast

lemma divide_right_mono_neg: "a ≤ b
    ⟹ c ≤ 0 ⟹ b / c ≤ a / c"
  by (metis local.divide_cancel_right local.divide_strict_right_mono_neg local.dual_order.strict_implies_order local.eq_refl local.le_imp_less_or_eq)

lemma divide_left_mono_neg: "a ≤ b
    ⟹ c ≤ 0 ⟹ 0 < a * b ⟹ c / a ≤ c / b"
  by (metis local.divide_left_mono local.minus_divide_left local.neg_0_le_iff_le local.neg_le_iff_le mult_commute)

lemma divide_nonneg_nonneg [simp]:
  "0 ≤ x ⟹ 0 ≤ y ⟹ 0 ≤ x / y"
  using local.divide_eq_0_iff local.divide_nonneg_pos local.dual_order.order_iff_strict by blast

lemma divide_nonpos_nonpos:
  "x ≤ 0 ⟹ y ≤ 0 ⟹ 0 ≤ x / y"
  using local.divide_nonpos_neg local.dual_order.order_iff_strict by auto

lemma divide_nonneg_nonpos:
  "0 ≤ x ⟹ y ≤ 0 ⟹ x / y ≤ 0"
  by (metis local.divide_eq_0_iff local.divide_nonneg_neg local.dual_order.order_iff_strict)

lemma divide_nonpos_nonneg:
  "x ≤ 0 ⟹ 0 ≤ y ⟹ x / y ≤ 0"
  using local.divide_nonpos_pos local.dual_order.order_iff_strict by auto

text ‹Conditional Simplification Rules: No Case Splits›

lemma le_divide_eq_1_pos [simp]:
  "0 < a ⟹ (1 ≤ b/a) = (a ≤ b)"
  by (simp add: local.pos_le_divide_eq)

lemma le_divide_eq_1_neg [simp]:
  "a < 0 ⟹ (1 ≤ b/a) = (b ≤ a)"
  by (metis local.le_divide_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less local.neg_le_iff_le)

lemma divide_le_eq_1_pos [simp]:
  "0 < a ⟹ (b/a ≤ 1) = (b ≤ a)"
  using local.pos_divide_le_eq by auto

lemma divide_le_eq_1_neg [simp]:
  "a < 0 ⟹ (b/a ≤ 1) = (a ≤ b)"
  by (metis local.divide_le_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less
      local.neg_le_iff_le)

lemma less_divide_eq_1_pos [simp]:
  "0 < a ⟹ (1 < b/a) = (a < b)"
  by (simp add: local.dual_order.strict_iff_order)

lemma less_divide_eq_1_neg [simp]:
  "a < 0 ⟹ (1 < b/a) = (b < a)"
  using local.dual_order.strict_iff_order by auto

lemma divide_less_eq_1_pos [simp]:
  "0 < a ⟹ (b/a < 1) = (b < a)"
  using local.divide_le_eq_1_pos local.dual_order.strict_iff_order by auto

lemma divide_less_eq_1_neg [simp]:
  "a < 0 ⟹ b/a < 1 ⟷ a < b"
  using local.dual_order.strict_iff_order by auto

lemma abs_div_pos: "0 < y ⟹
    ¦x¦ / y = ¦x / y¦"
  by (simp add: local.abs_pos)

lemma zero_le_divide_abs_iff [simp]: "(0 ≤ a / ¦b¦) = (0 ≤ a | b = 0)"
proof
  assume assm: "0 ≤ a / ¦b¦"
  have absb: "abs b ≥ 0" by (fact abs_nn)
  thus "0 ≤ a ∨ b = 0"
    using absb assm local.abs_eq_0_iff local.mult_nonneg_nonneg by fastforce
next
  assume "0 ≤ a ∨ b = 0"
  then consider (a) "0 ≤ a" | (b) "b = 0" by atomize_elim auto
  thus "0 ≤ a / ¦b¦"
    by (metis local.abs_eq_0_iff local.abs_nn local.divide_eq_0_iff local.divide_nonneg_nonneg)
qed


lemma divide_le_0_abs_iff [simp]: "(a / ¦b¦ ≤ 0) = (a ≤ 0 | b = 0)"
  by (metis local.minus_divide_left local.neg_0_le_iff_le local.zero_le_divide_abs_iff)

text‹For creating values between \<^term>‹u› and \<^term>‹v›.›
lemma scaling_mono:
  assumes "u ≤ v" and "0 ≤ r" and "r ≤ s"
  shows "u + r * (v - u) / s ≤ v"
proof -
  have "r/s ≤ 1" using assms
    by (metis local.divide_le_eq_1_pos local.division_ring_divide_zero
        local.dual_order.order_iff_strict local.dual_order.trans local.zero_less_one)
  hence "(r/s) * (v - u) ≤ 1 * (v - u)"
    using assms(1) local.diff_ge_0_iff_ge local.mult_right_mono by blast
  thus ?thesis
    by (simp add: field_simps)
qed

end (* class nice_ordered_field *)


code_identifier
  code_module Ordered_Fields ⇀ (SML) Arith and (OCaml) Arith and (Haskell) Arith

subsection ‹Ordering on complex numbers›

instantiation complex :: nice_ordered_field begin
instance
proof intro_classes
  note defs = less_eq_complex_def less_complex_def abs_complex_def
  fix x y z a b c :: complex
  show "a ≤ 0 ⟹ ¦a¦ = - a" unfolding defs
    by (simp add: cmod_eq_Re complex_is_Real_iff)
  show "0 ≤ a ⟹ ¦a¦ = a"
    unfolding defs
    by (metis abs_of_nonneg cmod_eq_Re comp_apply complex.exhaust_sel complex_of_real_def zero_complex.simps(1) zero_complex.simps(2))
  show "a < b ⟹ 0 < c ⟹ c * a < c * b" unfolding defs by auto
  show "0 < (1::complex)" unfolding defs by simp
  show "0 < a ⟹ 0 < inverse a" unfolding defs by auto
  define ra ia rb ib rc ic where "ra = Re a" "ia = Im a" "rb = Re b" "ib = Im b" "rc = Re c" "ic = Im c"
  note ri = this[symmetric]
  hence "a = Complex ra ia" "b = Complex rb ib" "c = Complex rc ic" by auto
  note ri = this ri
  have "rb ≤ ra"
    if "1 / ra ≤ (if rb = 0 then 0 else 1 / rb)"
      and "ia = 0" and "0 < ra" and "ib = 0"
  proof(cases "rb = 0")
    case True
    thus ?thesis
      using that(3) by auto
  next
    case False
    thus ?thesis
      by (smt nice_ordered_field_class.frac_less2 that(1) that(3))
  qed
  thus "inverse a ≤ inverse b ⟹ 0 < a ⟹ b ≤ a" unfolding defs ri
    by (auto simp: power2_eq_square)
  show "(⋀a. a < b ⟹ a ≤ c) ⟹ b ≤ c" unfolding defs ri
    by (metis complex.sel(1) complex.sel(2) dense less_le_not_le
        nice_ordered_field_class.linordered_field_no_lb not_le_imp_less)
  show "0 ≤ a ⟹ 0 ≤ b ⟹ a ≤ b ∨ b ≤ a" unfolding defs by auto
  show "0 ≤ ¦x¦" unfolding defs by auto
qed
end

lemma less_eq_complexI: "Re x ≤ Re y ⟹ Im x = Im y ⟹ x≤y" unfolding less_eq_complex_def
  by simp
lemma less_complexI: "Re x < Re y ⟹ Im x = Im y ⟹ x<y" unfolding less_complex_def
  by simp

lemma complex_of_real_mono:
  "x ≤ y ⟹ complex_of_real x ≤ complex_of_real y"
  unfolding less_eq_complex_def by auto

lemma complex_of_real_mono_iff[simp]:
  "complex_of_real x ≤ complex_of_real y ⟷ x ≤ y"
  unfolding less_eq_complex_def by auto

lemma complex_of_real_strict_mono_iff[simp]:
  "complex_of_real x < complex_of_real y ⟷ x < y"
  unfolding less_complex_def by auto

lemma complex_of_real_nn_iff[simp]:
  "0 ≤ complex_of_real y ⟷ 0 ≤ y"
  unfolding less_eq_complex_def by auto

lemma complex_of_real_pos_iff[simp]:
  "0 < complex_of_real y ⟷ 0 < y"
  unfolding less_complex_def by auto

lemma Re_mono: "x ≤ y ⟹ Re x ≤ Re y"
  unfolding less_eq_complex_def by simp

lemma comp_Im_same: "x ≤ y ⟹ Im x = Im y"
  unfolding less_eq_complex_def by simp

lemma Re_strict_mono: "x < y ⟹ Re x < Re y"
  unfolding less_complex_def by simp

lemma complex_of_real_cmod: assumes "x ≥ 0" shows "complex_of_real (cmod x) = x"
  by (metis Reals_cases abs_of_nonneg assms comp_Im_same complex_is_Real_iff complex_of_real_nn_iff norm_of_real zero_complex.simps(2))


end