Quelle Fields.thy Sprache: Isabelle

(*  Title:      HOL/Fields.thy
    Author:     Gertrud Bauer
    Author:     Steven Obua
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
*)

section \<open>Fields\<close>

theory Fields
imports Nat
begin

subsection \<open>Division rings\<close>

text \<open>
  A division ring is like a field, but without the commutativity requirement.
\<close>

class inverse = divide +
  fixes inverse :: "'a \ 'a"
begin

abbreviation inverse_divide :: "'a \ 'a \ 'a" (infixl \'/\ 70)
where
  "inverse_divide \ divide"

end

text \<open>Setup for linear arithmetic prover\<close>

ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close>
ML_file \<open>Tools/lin_arith.ML\<close>
setup \<open>Lin_Arith.global_setup\<close>
declaration \<open>K (
  Lin_Arith.init_arith_data
  #> Lin_Arith.add_discrete_type \<^type_name>\<open>nat\<close>
  #> Lin_Arith.add_lessD @{thm Suc_leI}
  #> Lin_Arith.add_simps @{thms simp_thms ring_distribs if_True if_False
      minus_diff_eq
      add_0_left add_0_right order_less_irrefl
      zero_neq_one zero_less_one zero_le_one
      zero_neq_one [THEN not_sym] not_one_le_zero not_one_less_zero
      add_Suc add_Suc_right nat.inject
      Suc_le_mono Suc_less_eq Zero_not_Suc
      Suc_not_Zero le_0_eq One_nat_def}
  #> Lin_Arith.add_simprocs [\<^simproc>\<open>group_cancel_add\<close>, \<^simproc>\<open>group_cancel_diff\<close>,
      \<^simproc>\<open>group_cancel_eq\<close>, \<^simproc>\<open>group_cancel_le\<close>,
      \<^simproc>\<open>group_cancel_less\<close>,
      \<^simproc>\<open>nateq_cancel_sums\<close>,\<^simproc>\<open>natless_cancel_sums\<close>,
      \<^simproc>\<open>natle_cancel_sums\<close>])\<close>

simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \ n" | "(m::nat) = n") =
  \<open>K Lin_Arith.simproc\<close> \<comment> \<open>Because of this simproc, the arithmetic solver is
   really only useful to detect inconsistencies among the premises for subgoals which are
   \<^emph>\<open>not\<close> themselves (in)equalities, because the latter activate
   \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
   solver all the time rather than add the additional check.\<close>

lemmas [linarith_split] = nat_diff_split split_min split_max abs_split

text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>

named_theorems divide_simps "rewrite rules to eliminate divisions"

class division_ring = ring_1 + inverse +
  assumes left_inverse [simp]:  "a \ 0 \ inverse a * a = 1"
  assumes right_inverse [simp]: "a \ 0 \ a * inverse a = 1"
  assumes divide_inverse: "a / b = a * inverse b"
  assumes inverse_zero [simp]: "inverse 0 = 0"
begin

subclass ring_1_no_zero_divisors
proof
  fix a b :: 'a
  assume a: "a \ 0" and b: "b \ 0"
  show "a * b \ 0"
  proof
    assume ab: "a * b = 0"
    hence "0 = inverse a * (a * b) * inverse b" by simp
    also have "\ = (inverse a * a) * (b * inverse b)"
      by (simp only: mult.assoc)
    also have "\ = 1" using a b by simp
    finally show False by simp
  qed
qed

lemma nonzero_imp_inverse_nonzero:
  "a \ 0 \ inverse a \ 0"
proof
  assume ianz: "inverse a = 0"
  assume "a \ 0"
  hence "1 = a * inverse a" by simp
  also have "... = 0" by (simp add: ianz)
  finally have "1 = 0" .
  thus False by (simp add: eq_commute)
qed

lemma inverse_zero_imp_zero:
  assumes "inverse a = 0" shows "a = 0"
proof (rule ccontr)
  assume "a \ 0"
  then have "inverse a \ 0"
    by (simp add: nonzero_imp_inverse_nonzero)
  with assms show False
    by auto
qed

lemma inverse_unique:
  assumes ab: "a * b = 1"
  shows "inverse a = b"
proof -
  have "a \ 0" using ab by (cases "a = 0") simp_all
  moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)
  ultimately show ?thesis by (simp add: mult.assoc [symmetric])
qed

lemma nonzero_inverse_minus_eq:
  "a \ 0 \ inverse (- a) = - inverse a"
by (rule inverse_unique) simp

lemma nonzero_inverse_inverse_eq:
  "a \ 0 \ inverse (inverse a) = a"
by (rule inverse_unique) simp

lemma nonzero_inverse_eq_imp_eq:
  assumes "inverse a = inverse b" and "a \ 0" and "b \ 0"
  shows "a = b"
proof -
  from \<open>inverse a = inverse b\<close>
  have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong)
  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> show "a = b"
    by (simp add: nonzero_inverse_inverse_eq)
qed

lemma inverse_1 [simp]: "inverse 1 = 1"
  by (rule inverse_unique) simp

subclass divide_trivial
  by standard (simp_all add: divide_inverse)

lemma nonzero_inverse_mult_distrib:
  assumes "a \ 0" and "b \ 0"
  shows "inverse (a * b) = inverse b * inverse a"
proof -
  have "a * (b * inverse b) * inverse a = 1" using assms by simp
  hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult.assoc)
  thus ?thesis by (rule inverse_unique)
qed

lemma division_ring_inverse_add:
  "a \ 0 \ b \ 0 \ inverse a + inverse b = inverse a * (a + b) * inverse b"
by (simp add: algebra_simps)

lemma division_ring_inverse_diff:
  "a \ 0 \ b \ 0 \ inverse a - inverse b = inverse a * (b - a) * inverse b"
by (simp add: algebra_simps)

lemma right_inverse_eq: "b \ 0 \ a / b = 1 \ a = b"
proof
  assume neq: "b \ 0"
  {
    hence "a = (a / b) * b" by (simp add: divide_inverse mult.assoc)
    also assume "a / b = 1"
    finally show "a = b" by simp
  next
    assume "a = b"
    with neq show "a / b = 1" by (simp add: divide_inverse)
  }
qed

lemma nonzero_inverse_eq_divide: "a \ 0 \ inverse a = 1 / a"
by (simp add: divide_inverse)

lemma divide_self [simp]: "a \ 0 \ a / a = 1"
by (simp add: divide_inverse)

lemma inverse_eq_divide [field_simps, field_split_simps, divide_simps]: "inverse a = 1 / a"
by (simp add: divide_inverse)

lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
by (simp add: divide_inverse algebra_simps)

lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
  by (simp add: divide_inverse mult.assoc)

lemma minus_divide_left: "- (a / b) = (-a) / b"
  by (simp add: divide_inverse)

lemma nonzero_minus_divide_right: "b \ 0 \ - (a / b) = a / (- b)"
  by (simp add: divide_inverse nonzero_inverse_minus_eq)

lemma nonzero_minus_divide_divide: "b \ 0 \ (-a) / (-b) = a / b"
  by (simp add: divide_inverse nonzero_inverse_minus_eq)

lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
  by (simp add: divide_inverse)

lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
  using add_divide_distrib [of a "- b" c] by simp

lemma nonzero_eq_divide_eq [field_simps]: "c \ 0 \ a = b / c \ a * c = b"
proof -
  assume [simp]: "c \ 0"
  have "a = b / c \ a * c = (b / c) * c" by simp
  also have "... \ a * c = b" by (simp add: divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma nonzero_divide_eq_eq [field_simps]: "c \ 0 \ b / c = a \ b = a * c"
proof -
  assume [simp]: "c \ 0"
  have "b / c = a \ (b / c) * c = a * c" by simp
  also have "... \ b = a * c" by (simp add: divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma nonzero_neg_divide_eq_eq [field_simps]: "b \ 0 \ - (a / b) = c \ - a = c * b"
  using nonzero_divide_eq_eq[of b "-a" c] by simp

lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \ 0 \ c = - (a / b) \ c * b = - a"
  using nonzero_neg_divide_eq_eq[of b a c] by auto

lemma divide_eq_imp: "c \ 0 \ b = a * c \ b / c = a"
  by (simp add: divide_inverse mult.assoc)

lemma eq_divide_imp: "c \ 0 \ a * c = b \ a = b / c"
  by (drule sym) (simp add: divide_inverse mult.assoc)

lemma add_divide_eq_iff [field_simps]:
  "z \ 0 \ x + y / z = (x * z + y) / z"
  by (simp add: add_divide_distrib nonzero_eq_divide_eq)

lemma divide_add_eq_iff [field_simps]:
  "z \ 0 \ x / z + y = (x + y * z) / z"
  by (simp add: add_divide_distrib nonzero_eq_divide_eq)

lemma diff_divide_eq_iff [field_simps]:
  "z \ 0 \ x - y / z = (x * z - y) / z"
  by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)

lemma minus_divide_add_eq_iff [field_simps]:
  "z \ 0 \ - (x / z) + y = (- x + y * z) / z"
  by (simp add: add_divide_distrib diff_divide_eq_iff)

lemma divide_diff_eq_iff [field_simps]:
  "z \ 0 \ x / z - y = (x - y * z) / z"
  by (simp add: field_simps)

lemma minus_divide_diff_eq_iff [field_simps]:
  "z \ 0 \ - (x / z) - y = (- x - y * z) / z"
  by (simp add: divide_diff_eq_iff[symmetric])

lemma division_ring_divide_zero:
  "a / 0 = 0"
  by (fact div_by_0)

lemma divide_self_if [simp]:
  "a / a = (if a = 0 then 0 else 1)"
  by simp

lemma inverse_nonzero_iff_nonzero [simp]:
  "inverse a = 0 \ a = 0"
  by (rule iffI) (fact inverse_zero_imp_zero, simp)

lemma inverse_minus_eq [simp]:
  "inverse (- a) = - inverse a"
proof cases
  assume "a=0" thus ?thesis by simp
next
  assume "a\0"
  thus ?thesis by (simp add: nonzero_inverse_minus_eq)
qed

lemma inverse_inverse_eq [simp]:
  "inverse (inverse a) = a"
proof cases
  assume "a=0" thus ?thesis by simp
next
  assume "a\0"
  thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
qed

lemma inverse_eq_imp_eq:
  "inverse a = inverse b \ a = b"
  by (drule arg_cong [where f="inverse"], simp)

lemma inverse_eq_iff_eq [simp]:
  "inverse a = inverse b \ a = b"
  by (force dest!: inverse_eq_imp_eq)

lemma mult_commute_imp_mult_inverse_commute:
  assumes "y * x = x * y"
  shows   "inverse y * x = x * inverse y"
proof (cases "y=0")
  case False
  hence "x * inverse y = inverse y * y * x * inverse y"
    by simp
  also have "\ = inverse y * (x * y * inverse y)"
    by (simp add: mult.assoc assms)
  finally show ?thesis by (simp add: mult.assoc False)
qed simp

lemmas mult_inverse_of_nat_commute =
  mult_commute_imp_mult_inverse_commute[OF mult_of_nat_commute]

lemma divide_divide_eq_left':
  "(a / b) / c = a / (c * b)"
  by (cases "b = 0 \ c = 0")
     (auto simp: divide_inverse mult.assoc nonzero_inverse_mult_distrib)

lemma add_divide_eq_if_simps [field_split_simps, divide_simps]:
    "a + b / z = (if z = 0 then a else (a * z + b) / z)"
    "a / z + b = (if z = 0 then b else (a + b * z) / z)"
    "- (a / z) + b = (if z = 0 then b else (-a + b * z) / z)"
    "a - b / z = (if z = 0 then a else (a * z - b) / z)"
    "a / z - b = (if z = 0 then -b else (a - b * z) / z)"
    "- (a / z) - b = (if z = 0 then -b else (- a - b * z) / z)"
  by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff
      minus_divide_diff_eq_iff)

lemma [field_split_simps, divide_simps]:
  shows divide_eq_eq: "b / c = a \ (if c \ 0 then b = a * c else a = 0)"
    and eq_divide_eq: "a = b / c \ (if c \ 0 then a * c = b else a = 0)"
    and minus_divide_eq_eq: "- (b / c) = a \ (if c \ 0 then - b = a * c else a = 0)"
    and eq_minus_divide_eq: "a = - (b / c) \ (if c \ 0 then a * c = - b else a = 0)"
  by (auto simp add:  field_simps)

end

subsection \<open>Fields\<close>

class field = comm_ring_1 + inverse +
  assumes field_inverse: "a \ 0 \ inverse a * a = 1"
  assumes field_divide_inverse: "a / b = a * inverse b"
  assumes field_inverse_zero: "inverse 0 = 0"
begin

subclass division_ring
proof
  fix a :: 'a
  assume "a \ 0"
  thus "inverse a * a = 1" by (rule field_inverse)
  thus "a * inverse a = 1" by (simp only: mult.commute)
next
  fix a b :: 'a
  show "a / b = a * inverse b" by (rule field_divide_inverse)
next
  show "inverse 0 = 0"
    by (fact field_inverse_zero)
qed

subclass idom_divide
proof
  fix b a
  assume "b \ 0"
  then show "a * b / b = a"
    by (simp add: divide_inverse ac_simps)
next
  fix a
  show "a / 0 = 0"
    by (simp add: divide_inverse)
qed

text\<open>There is no slick version using division by zero.\<close>
lemma inverse_add:
  "a \ 0 \ b \ 0 \ inverse a + inverse b = (a + b) * inverse a * inverse b"
  by (simp add: division_ring_inverse_add ac_simps)

lemma nonzero_mult_divide_mult_cancel_left [simp]:
  assumes [simp]: "c \ 0"
  shows "(c * a) / (c * b) = a / b"
proof (cases "b = 0")
  case True then show ?thesis by simp
next
  case False
  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
  also have "... = a * inverse b * (inverse c * c)"
    by (simp only: ac_simps)
  also have "... = a * inverse b" by simp
    finally show ?thesis by (simp add: divide_inverse)
qed

lemma nonzero_mult_divide_mult_cancel_right [simp]:
  "c \ 0 \ (a * c) / (b * c) = a / b"
  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)

lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
  by (simp add: divide_inverse ac_simps)

lemma divide_inverse_commute: "a / b = inverse b * a"
  by (simp add: divide_inverse mult.commute)

lemma add_frac_eq:
  assumes "y \ 0" and "z \ 0"
  shows "x / y + w / z = (x * z + w * y) / (y * z)"
proof -
  have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)"
    using assms by simp
  also have "\ = (x * z + y * w) / (y * z)"
    by (simp only: add_divide_distrib)
  finally show ?thesis
    by (simp only: mult.commute)
qed

text\<open>Special Cancellation Simprules for Division\<close>

lemma nonzero_divide_mult_cancel_right [simp]:
  "b \ 0 \ b / (a * b) = 1 / a"
  using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp

lemma nonzero_divide_mult_cancel_left [simp]:
  "a \ 0 \ a / (a * b) = 1 / b"
  using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp

lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
  "c \ 0 \ (c * a) / (b * c) = a / b"
  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)

lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
  "c \ 0 \ (a * c) / (c * b) = a / b"
  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)

lemma diff_frac_eq:
  "y \ 0 \ z \ 0 \ x / y - w / z = (x * z - w * y) / (y * z)"
  by (simp add: field_simps)

lemma frac_eq_eq:
  "y \ 0 \ z \ 0 \ (x / y = w / z) = (x * z = w * y)"
  by (simp add: field_simps)

lemma divide_minus1 [simp]: "x / - 1 = - x"
  using nonzero_minus_divide_right [of "1" x] by simp

text\<open>This version builds in division by zero while also re-orienting
      the right-hand side.\<close>
lemma inverse_mult_distrib [simp]:
  "inverse (a * b) = inverse a * inverse b"
proof cases
  assume "a \ 0 \ b \ 0"
  thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
next
  assume "\ (a \ 0 \ b \ 0)"
  thus ?thesis by force
qed

lemma inverse_divide [simp]:
  "inverse (a / b) = b / a"
  by (simp add: divide_inverse mult.commute)

text \<open>Calculations with fractions\<close>

text\<open>There is a whole bunch of simp-rules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close>
because the latter are covered by a simproc.\<close>

lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left

lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right

lemma divide_divide_eq_right [simp]:
  "a / (b / c) = (a * c) / b"
  by (simp add: divide_inverse ac_simps)

lemma divide_divide_eq_left [simp]:
  "(a / b) / c = a / (b * c)"
  by (simp add: divide_inverse mult.assoc)

lemma divide_divide_times_eq:
  "(x / y) / (z / w) = (x * w) / (y * z)"
  by simp

text \<open>Special Cancellation Simprules for Division\<close>

lemma mult_divide_mult_cancel_left_if [simp]:
  shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
  by simp

text \<open>Division and Unary Minus\<close>

lemma minus_divide_right:
  "- (a / b) = a / - b"
  by (simp add: divide_inverse)

lemma divide_minus_right [simp]:
  "a / - b = - (a / b)"
  by (simp add: divide_inverse)

lemma minus_divide_divide:
  "(- a) / (- b) = a / b"
  by (cases "b=0") (simp_all add: nonzero_minus_divide_divide)

lemma inverse_eq_1_iff [simp]:
  "inverse x = 1 \ x = 1"
  using inverse_eq_iff_eq [of x 1] by simp

lemma divide_eq_0_iff [simp]:
  "a / b = 0 \ a = 0 \ b = 0"
  by (simp add: divide_inverse)

lemma divide_cancel_right [simp]:
  "a / c = b / c \ c = 0 \ a = b"
  by (cases "c=0") (simp_all add: divide_inverse)

lemma divide_cancel_left [simp]:
  "c / a = c / b \ c = 0 \ a = b"
  by (cases "c=0") (simp_all add: divide_inverse)

lemma divide_eq_1_iff [simp]:
  "a / b = 1 \ b \ 0 \ a = b"
  by (cases "b=0") (simp_all add: right_inverse_eq)

lemma one_eq_divide_iff [simp]:
  "1 = a / b \ b \ 0 \ a = b"
  by (simp add: eq_commute [of 1])

lemma divide_eq_minus_1_iff:
   "(a / b = - 1) \ b \ 0 \ a = - b"
using divide_eq_1_iff by fastforce

lemma times_divide_times_eq:
  "(x / y) * (z / w) = (x * z) / (y * w)"
  by simp

lemma add_frac_num:
  "y \ 0 \ x / y + z = (x + z * y) / y"
  by (simp add: add_divide_distrib)

lemma add_num_frac:
  "y \ 0 \ z + x / y = (x + z * y) / y"
  by (simp add: add_divide_distrib add.commute)

lemma dvd_field_iff:
  "a dvd b \ (a = 0 \ b = 0)"
proof (cases "a = 0")
  case False
  then have "b = a * (b / a)"
    by (simp add: field_simps)
  then have "a dvd b" ..
  with False show ?thesis
    by simp
qed simp

lemma inj_divide_right [simp]:
  "inj (\b. b / a) \ a \ 0"
proof -
  have "(\b. b / a) = (*) (inverse a)"
    by (simp add: field_simps fun_eq_iff)
  then have "inj (\y. y / a) \ inj ((*) (inverse a))"
    by simp
  also have "\ \ inverse a \ 0"
    by simp
  also have "\ \ a \ 0"
    by simp
  finally show ?thesis
    by simp
qed

end

class field_char_0 = field + ring_char_0

subsection \<open>Ordered fields\<close>

class field_abs_sgn = field + idom_abs_sgn
begin

lemma sgn_inverse [simp]:
  "sgn (inverse a) = inverse (sgn a)"
proof (cases "a = 0")
  case True then show ?thesis by simp
next
  case False
  then have "a * inverse a = 1"
    by simp
  then have "sgn (a * inverse a) = sgn 1"
    by simp
  then have "sgn a * sgn (inverse a) = 1"
    by (simp add: sgn_mult)
  then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1"
    by simp
  then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)"
    by (simp add: ac_simps)
  with False show ?thesis
    by (simp add: sgn_eq_0_iff)
qed

lemma abs_inverse [simp]:
  "\inverse a\ = inverse \a\"
proof -
  from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a]
  have "inverse (sgn a) * \inverse a\ = inverse (sgn a * \a\)"
    by simp
  then show ?thesis by (auto simp add: sgn_eq_0_iff)
qed

lemma sgn_divide [simp]:
  "sgn (a / b) = sgn a / sgn b"
  unfolding divide_inverse sgn_mult by simp

lemma abs_divide [simp]:
  "\a / b\ = \a\ / \b\"
  unfolding divide_inverse abs_mult by simp

end

class linordered_field = field + linordered_idom
begin

lemma positive_imp_inverse_positive:
  assumes a_gt_0: "0 < a"
  shows "0 < inverse a"
proof -
  have "0 < a * inverse a"
    by (simp add: a_gt_0 [THEN less_imp_not_eq2])
  thus "0 < inverse a"
    by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
qed

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

lemma inverse_le_imp_le:
  assumes invle: "inverse a \ inverse b" and apos: "0 < a"
  shows "b \ a"
proof (rule classical)
  assume "\ b \ a"
  hence "a < b"  by (simp add: linorder_not_le)
  hence bpos: "0 < b"  by (blast intro: apos less_trans)
  hence "a * inverse a \ a * inverse b"
    by (simp add: apos invle less_imp_le mult_left_mono)
  hence "(a * inverse a) * b \ (a * inverse b) * b"
    by (simp add: bpos less_imp_le mult_right_mono)
  thus "b \ a" by (simp add: mult.assoc apos bpos less_imp_not_eq2)
qed

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"
proof (rule ccontr)
  assume "\ inverse b < inverse a"
  hence "inverse a \ inverse b" by simp
  hence "\ (a < b)"
    by (simp add: not_less inverse_le_imp_le [OF _ apos])
  thus False by (rule notE [OF _ less])
qed

lemma inverse_less_imp_less:
  assumes "inverse a < inverse b" "0 < a"
  shows "b < a"
proof -
  have "a \ b"
    using assms by (simp add: less_le)
  moreover have "b \ a"
    using assms by (force simp: less_le dest: inverse_le_imp_le)
  ultimately show ?thesis
    by (simp add: less_le)
qed

text\<open>Both premises are essential. Consider -1 and 1.\<close>
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\<open>These results refer to both operands being negative.  The opposite-sign
case is trivial, since inverse preserves signs.\<close>
lemma inverse_le_imp_le_neg:
  assumes "inverse a \ inverse b" "b < 0"
  shows "b \ a"
proof (rule classical)
  assume "\ b \ a"
  with \<open>b < 0\<close> have "a < 0"
    by force
  with assms show "b \ a"
    using inverse_le_imp_le [of "-b" "-a"] by (simp add: nonzero_inverse_minus_eq)
qed

lemma less_imp_inverse_less_neg:
  assumes "a < b" "b < 0"
  shows "inverse b < inverse a"
proof -
  have "a < 0"
    using assms by (blast intro: less_trans)
  with less_imp_inverse_less [of "-b" "-a"] show ?thesis
    by (simp add: nonzero_inverse_minus_eq assms)
qed

lemma inverse_less_imp_less_neg:
  assumes "inverse a < inverse b" "b < 0"
  shows "b < a"
proof (rule classical)
  assume "\ b < a"
  with \<open>b < 0\<close> have "a < 0"
    by force
  with inverse_less_imp_less [of "-b" "-a"] show ?thesis
    by (simp add: nonzero_inverse_minus_eq assms)
qed

lemma inverse_less_iff_less_neg [simp]:
  "a < 0 \ b < 0 \ inverse a < inverse b \ b < a"
  using inverse_less_iff_less [of "-b" "-a"]
  by (simp del: inverse_less_iff_less add: nonzero_inverse_minus_eq)

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"
proof -
  from assms have "a \ b / c \ a * c \ (b / c) * c"
    using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps)
  also have "... \ a * c \ b"
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma pos_less_divide_eq [field_simps]:
  assumes "0 < c"
  shows "a < b / c \ a * c < b"
proof -
  from assms have "a < b / c \ a * c < (b / c) * c"
    using mult_less_cancel_right [of a c "b / c"] by auto
  also have "... = (a*c < b)"
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma neg_less_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a < b / c \ b < a * c"
proof -
  from assms have "a < b / c \ (b / c) * c < a * c"
    using mult_less_cancel_right [of "b / c" c a] by auto
  also have "... \ b < a * c"
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma neg_le_divide_eq [field_simps]:
  assumes "c < 0"
  shows "a \ b / c \ b \ a * c"
proof -
  from assms have "a \ b / c \ (b / c) * c \ a * c"
    using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps)
  also have "... \ b \ a * c"
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma pos_divide_le_eq [field_simps]:
  assumes "0 < c"
  shows "b / c \ a \ b \ a * c"
proof -
  from assms have "b / c \ a \ (b / c) * c \ a * c"
    using mult_le_cancel_right [of "b / c" c a] by auto
  also have "... \ b \ a * c"
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma pos_divide_less_eq [field_simps]:
  assumes "0 < c"
  shows "b / c < a \ b < a * c"
proof -
  from assms have "b / c < a \ (b / c) * c < a * c"
    using mult_less_cancel_right [of "b / c" c a] by auto
  also have "... \ b < a * c"
    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma neg_divide_le_eq [field_simps]:
  assumes "c < 0"
  shows "b / c \ a \ a * c \ b"
proof -
  from assms have "b / c \ a \ a * c \ (b / c) * c"
    using mult_le_cancel_right [of a c "b / c"] by auto
  also have "... \ a * c \ b"
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

lemma neg_divide_less_eq [field_simps]:
  assumes "c < 0"
  shows "b / c < a \ a * c < b"
proof -
  from assms have "b / c < a \ a * c < b / c * c"
    using mult_less_cancel_right [of a c "b / c"] by auto
  also have "... \ a * c < b"
    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
  finally show ?thesis .
qed

text\<open>The following \<open>field_simps\<close> rules are necessary, as minus is always moved atop of
division but we want to get rid of division.\<close>

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 )

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:
  assumes "b < a" "c < 0" shows "a / c < b / c"
proof -
  have "b / - c < a / - c"
    by (rule divide_strict_right_mono) (use assms in auto)
  then show ?thesis
    by (simp add: less_imp_not_eq)
qed

text\<open>The last premise ensures that \<^term>\<open>a\<close> and \<^term>\<open>b\<close>
      have the same sign\<close>
lemma divide_strict_left_mono:
  "\b < a; 0 < c; 0 < a*b\ \ c / a < c / b"
  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)

lemma divide_left_mono:
  "\b \ a; 0 \ c; 0 < a*b\ \ c / a \ c / b"
  by (auto simp: field_simps zero_less_mult_iff mult_right_mono)

lemma divide_strict_left_mono_neg:
  "\a < b; c < 0; 0 < a*b\ \ c / a < c / b"
  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)

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:
  assumes "0 \ y" "x \ y" "0 < w" "w \ z"
  shows "x / z \ y / w"
proof (rule mult_imp_div_pos_le)
  show "z > 0"
    using assms by simp
  have "x \ y * z / w"
  proof (rule mult_imp_le_div_pos [OF \<open>0 < w\<close>])
    show "x * w \ y * z"
      using assms by (auto intro: mult_mono)
  qed
  also have "... = y / w * z"
    by simp
  finally show "x \ y / w * z" .
qed

lemma frac_less:
  assumes "0 \ x" "x < y" "0 < w" "w \ z"
  shows "x / z < y / w"
proof (rule mult_imp_div_pos_less)
  show "z > 0"
    using assms by simp
  have "x < y * z / w"
  proof (rule mult_imp_less_div_pos [OF \<open>0 < w\<close>])
    show "x * w < y * z"
      using assms by (auto intro: mult_less_le_imp_less)
  qed
  also have "... = y / w * z"
    by simp
  finally show "x < y / w * z" .
qed

lemma frac_less2:
  assumes "0 < x" "x \ y" "0 < w" "w < z"
  shows "x / z < y / w"
proof (rule mult_imp_div_pos_less)
  show "z > 0"
    using assms by simp
  show "x < y / w * z"
    using assms by (force intro: mult_imp_less_div_pos mult_le_less_imp_less)
qed

text \<open>As above, with a better name\<close>
lemma divide_mono:
  "\b \ a; c \ d; 0 < b; 0 \ c\ \ c / a \ d / b"
  by (simp add: frac_le)

lemma less_half_sum: "a < b \ a < (a+b) / (1+1)"
  by (simp add: field_simps zero_less_two)

lemma gt_half_sum: "a < b \ (a+b)/(1+1) < b"
  by (simp add: field_simps zero_less_two)

subclass unbounded_dense_linorder
proof
  fix x y :: 'a
  from less_add_one show "\y. x < y" ..
  from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
  then have "x - 1 < x + 1 - 1" by simp
  then have "x - 1 < x" by (simp add: algebra_simps)
  then show "\y. y < x" ..
  show "x < y \ \z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
qed

subclass field_abs_sgn ..

lemma inverse_sgn [simp]:
  "inverse (sgn a) = sgn a"
  by (cases a 0 rule: linorder_cases) simp_all

lemma divide_sgn [simp]:
  "a / sgn b = a * sgn b"
  by (cases b 0 rule: linorder_cases) simp_all

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)
  then have "0 \ y - t" by (simp only: add_le_cancel_left)
  then show "t \ y" by (simp add: algebra_simps)
qed

lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < a)"
proof (cases "a = 0")
  case False
  then show ?thesis
    by (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
qed auto

lemma inverse_negative_iff_negative [simp]: "(inverse a < 0) = (a < 0)"
proof (cases "a = 0")
  case False
  then show ?thesis
    by (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
qed auto

lemma inverse_nonnegative_iff_nonnegative [simp]: "0 \ inverse a \ 0 \ a"
  by (simp add: not_less [symmetric])

lemma inverse_nonpositive_iff_nonpositive [simp]: "inverse a \ 0 \ a \ 0"
  by (simp add: not_less [symmetric])

lemma one_less_inverse_iff: "1 < inverse x \ 0 < x \ x < 1"
  using less_trans[of 1 x 0 for x]
  by (cases x 0 rule: linorder_cases) (auto simp add: field_simps)

lemma one_le_inverse_iff: "1 \ inverse x \ 0 < x \ x \ 1"
proof (cases "x = 1")
  case True then show ?thesis by simp
next
  case False then have "inverse x \ 1" by simp
  then have "1 \ inverse x" by blast
  then have "1 \ inverse x \ 1 < inverse x" by (simp add: le_less)
  with False show ?thesis by (auto simp add: one_less_inverse_iff)
qed

lemma inverse_less_1_iff: "inverse x < 1 \ x \ 0 \ 1 < x"
  by (simp add: not_le [symmetric] one_le_inverse_iff)

lemma inverse_le_1_iff: "inverse x \ 1 \ x \ 0 \ 1 \ x"
  by (simp add: not_less [symmetric] one_less_inverse_iff)

lemma [field_split_simps, divide_simps]:
  shows le_divide_eq: "a \ b / c \ (if 0 < c then a * c \ b else if c < 0 then b \ a * c else a \ 0)"
    and divide_le_eq: "b / c \ a \ (if 0 < c then b \ a * c else if c < 0 then a * c \ b else 0 \ a)"
    and less_divide_eq: "a < b / c \ (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
    and divide_less_eq: "b / c < a \ (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
    and le_minus_divide_eq: "a \ - (b / c) \ (if 0 < c then a * c \ - b else if c < 0 then - b \ a * c else a \ 0)"
    and minus_divide_le_eq: "- (b / c) \ a \ (if 0 < c then - b \ a * c else if c < 0 then a * c \ - b else 0 \ a)"
    and less_minus_divide_eq: "a < - (b / c) \ (if 0 < c then a * c < - b else if c < 0 then - b < a * c else a < 0)"
    and minus_divide_less_eq: "- (b / c) < a \ (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
  by (auto simp: field_simps not_less dest: order.antisym)

text \<open>Division and Signs\<close>

lemma
  shows zero_less_divide_iff: "0 < a / b \ 0 < a \ 0 < b \ a < 0 \ b < 0"
    and divide_less_0_iff: "a / b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b"
    and zero_le_divide_iff: "0 \ a / b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0"
    and divide_le_0_iff: "a / b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b"
  by (auto simp add: field_split_simps)

text \<open>Division and the Number One\<close>

text\<open>Simplify expressions equated with 1\<close>

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\<open>Simplify expressions such as \<open>0 < 1/x\<close> to \<open>0 < x\<close>\<close>

lemma zero_le_divide_1_iff [simp]:
  "0 \ 1 / a \ 0 \ a"
  by (simp add: zero_le_divide_iff)

lemma zero_less_divide_1_iff [simp]:
  "0 < 1 / a \ 0 < a"
  by (simp add: zero_less_divide_iff)

lemma divide_le_0_1_iff [simp]:
  "1 / a \ 0 \ a \ 0"
  by (simp add: divide_le_0_iff)

lemma divide_less_0_1_iff [simp]:
  "1 / a < 0 \ a < 0"
  by (simp add: divide_less_0_iff)

lemma divide_right_mono:
  "\a \ b; 0 \ c\ \ a/c \ b/c"
  by (force simp add: divide_strict_right_mono le_less)

lemma divide_right_mono_neg: "a \ b \ c \ 0 \ b / c \ a / c"
  by (auto dest: divide_right_mono [of _ _ "- c"])

lemma divide_left_mono_neg: "a \ b \ c \ 0 \ 0 < a * b \ c / a \ c / b"
  by (auto simp add: mult.commute dest: divide_left_mono [of _ _ "- c"])

lemma inverse_le_iff: "inverse a \ inverse b \ (0 < a * b \ b \ a) \ (a * b \ 0 \ a \ b)"
  by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
     (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff)

lemma inverse_less_iff: "inverse a < inverse b \ (0 < a * b \ b < a) \ (a * b \ 0 \ a < b)"
  by (subst less_le) (auto simp: inverse_le_iff)

lemma divide_le_cancel: "a / c \ b / c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)"
  by (simp add: divide_inverse mult_le_cancel_right)

lemma divide_less_cancel: "a / c < b / c \ (0 < c \ a < b) \ (c < 0 \ b < a) \ c \ 0"
  by (auto simp add: divide_inverse mult_less_cancel_right)

text\<open>Simplify quotients that are compared with the value 1.\<close>

lemma le_divide_eq_1:
  "(1 \ b / a) = ((0 < a \ a \ b) \ (a < 0 \ b \ a))"
  by (auto simp add: le_divide_eq)

lemma divide_le_eq_1:
  "(b / a \ 1) = ((0 < a \ b \ a) \ (a < 0 \ a \ b) \ a=0)"
  by (auto simp add: divide_le_eq)

lemma less_divide_eq_1:
  "(1 < b / a) = ((0 < a \ a < b) \ (a < 0 \ b < a))"
  by (auto simp add: less_divide_eq)

lemma divide_less_eq_1:
  "(b / a < 1) = ((0 < a \ b < a) \ (a < 0 \ a < b) \ a=0)"
  by (auto simp add: divide_less_eq)

lemma divide_nonneg_nonneg [simp]:
  "0 \ x \ 0 \ y \ 0 \ x / y"
  by (auto simp add: field_split_simps)

lemma divide_nonpos_nonpos:
  "x \ 0 \ y \ 0 \ 0 \ x / y"
  by (auto simp add: field_split_simps)

lemma divide_nonneg_nonpos:
  "0 \ x \ y \ 0 \ x / y \ 0"
  by (auto simp add: field_split_simps)

lemma divide_nonpos_nonneg:
  "x \ 0 \ 0 \ y \ x / y \ 0"
  by (auto simp add: field_split_simps)

text \<open>Conditional Simplification Rules: No Case Splits\<close>

lemma le_divide_eq_1_pos [simp]:
  "0 < a \ (1 \ b/a) = (a \ b)"
  by (auto simp add: le_divide_eq)

lemma le_divide_eq_1_neg [simp]:
  "a < 0 \ (1 \ b/a) = (b \ a)"
  by (auto simp add: le_divide_eq)

lemma divide_le_eq_1_pos [simp]:
  "0 < a \ (b/a \ 1) = (b \ a)"
  by (auto simp add: divide_le_eq)

lemma divide_le_eq_1_neg [simp]:
  "a < 0 \ (b/a \ 1) = (a \ b)"
  by (auto simp add: divide_le_eq)

lemma less_divide_eq_1_pos [simp]:
  "0 < a \ (1 < b/a) = (a < b)"
  by (auto simp add: less_divide_eq)

lemma less_divide_eq_1_neg [simp]:
  "a < 0 \ (1 < b/a) = (b < a)"
  by (auto simp add: less_divide_eq)

lemma divide_less_eq_1_pos [simp]:
  "0 < a \ (b/a < 1) = (b < a)"
  by (auto simp add: divide_less_eq)

lemma divide_less_eq_1_neg [simp]:
  "a < 0 \ b/a < 1 \ a < b"
  by (auto simp add: divide_less_eq)

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)

lemma abs_div_pos: "0 < y \ \x\ / y = \x / y\"
  by (simp add: order_less_imp_le)

lemma zero_le_divide_abs_iff [simp]: "(0 \ a / \b\) = (0 \ a \ b = 0)"
  by (auto simp: zero_le_divide_iff)

lemma divide_le_0_abs_iff [simp]: "(a / \b\ \ 0) = (a \ 0 \ b = 0)"
  by (auto simp: divide_le_0_iff)

lemma field_le_mult_one_interval:
  assumes *: "\z. \ 0 < z ; z < 1 \ \ z * x \ y"
  shows "x \ y"
proof (cases "0 < x")
  assume "0 < x"
  thus ?thesis
    using dense_le_bounded[of 0 1 "y/x"] *
    unfolding le_divide_eq if_P[OF \<open>0 < x\<close>] by simp
next
  assume "\0 < x" hence "x \ 0" by simp
  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1::'a"] by auto
  hence "x \ s * x" using mult_le_cancel_right[of 1 x s] \x \ 0\ by auto
  also note *[OF s]
  finally show ?thesis .
qed

text\<open>For creating values between \<^term>\<open>u\<close> and \<^term>\<open>v\<close>.\<close>
lemma scaling_mono:
  assumes "u \ v" "0 \ r" "r \ s"
  shows "u + r * (v - u) / s \ v"
proof -
  have "r/s \ 1" using assms
    using divide_le_eq_1 by fastforce
  moreover have "0 \ v - u"
    using assms by simp
  ultimately have "(r/s) * (v - u) \ 1 * (v - u)"
    by (rule mult_right_mono)
  then show ?thesis
    by (simp add: field_simps)
qed

end

text \<open>Min/max Simplification Rules\<close>

lemma min_mult_distrib_left:
  fixes x::"'a::linordered_idom"
  shows "p * min x y = (if 0 \ p then min (p*x) (p*y) else max (p*x) (p*y))"
by (auto simp add: min_def max_def mult_le_cancel_left)

lemma min_mult_distrib_right:
  fixes x::"'a::linordered_idom"
  shows "min x y * p = (if 0 \ p then min (x*p) (y*p) else max (x*p) (y*p))"
by (auto simp add: min_def max_def mult_le_cancel_right)

lemma min_divide_distrib_right:
  fixes x::"'a::linordered_field"
  shows "min x y / p = (if 0 \ p then min (x/p) (y/p) else max (x/p) (y/p))"
by (simp add: min_mult_distrib_right divide_inverse)

lemma max_mult_distrib_left:
  fixes x::"'a::linordered_idom"
  shows "p * max x y = (if 0 \ p then max (p*x) (p*y) else min (p*x) (p*y))"
by (auto simp add: min_def max_def mult_le_cancel_left)

lemma max_mult_distrib_right:
  fixes x::"'a::linordered_idom"
  shows "max x y * p = (if 0 \ p then max (x*p) (y*p) else min (x*p) (y*p))"
by (auto simp add: min_def max_def mult_le_cancel_right)

lemma max_divide_distrib_right:
  fixes x::"'a::linordered_field"
  shows "max x y / p = (if 0 \ p then max (x/p) (y/p) else min (x/p) (y/p))"
by (simp add: max_mult_distrib_right divide_inverse)

hide_fact (open) field_inverse field_divide_inverse field_inverse_zero

code_identifier
  code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

end

quality99%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.