src/HOL/Ring_and_Field.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 24748 ee0a0eb6b738 child 25062 af5ef0d4d655 permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:   HOL/Ring_and_Field.thy

     2     ID:      $Id$

     3     Author:  Gertrud Bauer, Steven Obua, Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel,

     4              with contributions by Jeremy Avigad

     5 *)

     6

     7 header {* (Ordered) Rings and Fields *}

     8

     9 theory Ring_and_Field

    10 imports OrderedGroup

    11 begin

    12

    13 text {*

    14   The theory of partially ordered rings is taken from the books:

    15   \begin{itemize}

    16   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

    17   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

    18   \end{itemize}

    19   Most of the used notions can also be looked up in

    20   \begin{itemize}

    21   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.

    22   \item \emph{Algebra I} by van der Waerden, Springer.

    23   \end{itemize}

    24 *}

    25

    26 class semiring = ab_semigroup_add + semigroup_mult +

    27   assumes left_distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"

    28   assumes right_distrib: "a \<^loc>* (b \<^loc>+ c) = a \<^loc>* b \<^loc>+ a \<^loc>* c"

    29

    30 class mult_zero = times + zero +

    31   assumes mult_zero_left [simp]: "\<^loc>0 \<^loc>* a = \<^loc>0"

    32   assumes mult_zero_right [simp]: "a \<^loc>* \<^loc>0 = \<^loc>0"

    33

    34 class semiring_0 = semiring + comm_monoid_add + mult_zero

    35

    36 class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add

    37

    38 instance semiring_0_cancel \<subseteq> semiring_0

    39 proof

    40   fix a :: 'a

    41   have "0 * a + 0 * a = 0 * a + 0"

    42     by (simp add: left_distrib [symmetric])

    43   thus "0 * a = 0"

    44     by (simp only: add_left_cancel)

    45

    46   have "a * 0 + a * 0 = a * 0 + 0"

    47     by (simp add: right_distrib [symmetric])

    48   thus "a * 0 = 0"

    49     by (simp only: add_left_cancel)

    50 qed

    51

    52 class comm_semiring = ab_semigroup_add + ab_semigroup_mult +

    53   assumes distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"

    54

    55 instance comm_semiring \<subseteq> semiring

    56 proof

    57   fix a b c :: 'a

    58   show "(a + b) * c = a * c + b * c" by (simp add: distrib)

    59   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)

    60   also have "... = b * a + c * a" by (simp only: distrib)

    61   also have "... = a * b + a * c" by (simp add: mult_ac)

    62   finally show "a * (b + c) = a * b + a * c" by blast

    63 qed

    64

    65 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero

    66

    67 instance comm_semiring_0 \<subseteq> semiring_0 ..

    68

    69 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add

    70

    71 instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..

    72

    73 instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..

    74

    75 class zero_neq_one = zero + one +

    76   assumes zero_neq_one [simp]: "\<^loc>0 \<noteq> \<^loc>1"

    77

    78 class semiring_1 = zero_neq_one + semiring_0 + monoid_mult

    79

    80 class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult

    81   (*previously almost_semiring*)

    82

    83 instance comm_semiring_1 \<subseteq> semiring_1 ..

    84

    85 class no_zero_divisors = zero + times +

    86   assumes no_zero_divisors: "a \<noteq> \<^loc>0 \<Longrightarrow> b \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* b \<noteq> \<^loc>0"

    87

    88 class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one

    89   + cancel_ab_semigroup_add + monoid_mult

    90

    91 instance semiring_1_cancel \<subseteq> semiring_0_cancel ..

    92

    93 instance semiring_1_cancel \<subseteq> semiring_1 ..

    94

    95 class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult

    96   + zero_neq_one + cancel_ab_semigroup_add

    97

    98 instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..

    99

   100 instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..

   101

   102 instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..

   103

   104 class ring = semiring + ab_group_add

   105

   106 instance ring \<subseteq> semiring_0_cancel ..

   107

   108 class comm_ring = comm_semiring + ab_group_add

   109

   110 instance comm_ring \<subseteq> ring ..

   111

   112 instance comm_ring \<subseteq> comm_semiring_0_cancel ..

   113

   114 class ring_1 = ring + zero_neq_one + monoid_mult

   115

   116 instance ring_1 \<subseteq> semiring_1_cancel ..

   117

   118 class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult

   119   (*previously ring*)

   120

   121 instance comm_ring_1 \<subseteq> ring_1 ..

   122

   123 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..

   124

   125 class ring_no_zero_divisors = ring + no_zero_divisors

   126

   127 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors

   128

   129 class idom = comm_ring_1 + no_zero_divisors

   130

   131 instance idom \<subseteq> ring_1_no_zero_divisors ..

   132

   133 class division_ring = ring_1 + inverse +

   134   assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"

   135   assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"

   136

   137 instance division_ring \<subseteq> ring_1_no_zero_divisors

   138 proof

   139   fix a b :: 'a

   140   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"

   141   show "a * b \<noteq> 0"

   142   proof

   143     assume ab: "a * b = 0"

   144     hence "0 = inverse a * (a * b) * inverse b"

   145       by simp

   146     also have "\<dots> = (inverse a * a) * (b * inverse b)"

   147       by (simp only: mult_assoc)

   148     also have "\<dots> = 1"

   149       using a b by simp

   150     finally show False

   151       by simp

   152   qed

   153 qed

   154

   155 class field = comm_ring_1 + inverse +

   156   assumes field_inverse:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"

   157   assumes divide_inverse: "a \<^loc>/ b = a \<^loc>* inverse b"

   158

   159 instance field \<subseteq> division_ring

   160 proof

   161   fix a :: 'a

   162   assume "a \<noteq> 0"

   163   thus "inverse a * a = 1" by (rule field_inverse)

   164   thus "a * inverse a = 1" by (simp only: mult_commute)

   165 qed

   166

   167 instance field \<subseteq> idom ..

   168

   169 class division_by_zero = zero + inverse +

   170   assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"

   171

   172

   173 subsection {* Distribution rules *}

   174

   175 text{*For the @{text combine_numerals} simproc*}

   176 lemma combine_common_factor:

   177      "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"

   178 by (simp add: left_distrib add_ac)

   179

   180 lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"

   181 apply (rule equals_zero_I)

   182 apply (simp add: left_distrib [symmetric])

   183 done

   184

   185 lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"

   186 apply (rule equals_zero_I)

   187 apply (simp add: right_distrib [symmetric])

   188 done

   189

   190 lemma minus_mult_minus [simp]: "(- a) * (- b) = a * (b::'a::ring)"

   191   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])

   192

   193 lemma minus_mult_commute: "(- a) * b = a * (- b::'a::ring)"

   194   by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])

   195

   196 lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"

   197 by (simp add: right_distrib diff_minus

   198               minus_mult_left [symmetric] minus_mult_right [symmetric])

   199

   200 lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"

   201 by (simp add: left_distrib diff_minus

   202               minus_mult_left [symmetric] minus_mult_right [symmetric])

   203

   204 lemmas ring_distribs =

   205   right_distrib left_distrib left_diff_distrib right_diff_distrib

   206

   207 text{*This list of rewrites simplifies ring terms by multiplying

   208 everything out and bringing sums and products into a canonical form

   209 (by ordered rewriting). As a result it decides ring equalities but

   210 also helps with inequalities. *}

   211 lemmas ring_simps = group_simps ring_distribs

   212

   213 class mult_mono = times + zero + ord +

   214   assumes mult_left_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"

   215   assumes mult_right_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> a \<^loc>* c \<^loc>\<le> b \<^loc>* c"

   216

   217 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   218

   219 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   220   + semiring + comm_monoid_add + cancel_ab_semigroup_add

   221

   222 instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..

   223

   224 instance pordered_cancel_semiring \<subseteq> pordered_semiring ..

   225

   226 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono

   227

   228 instance ordered_semiring \<subseteq> pordered_cancel_semiring ..

   229

   230 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

   231   assumes mult_strict_left_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"

   232   assumes mult_strict_right_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> a \<^loc>* c \<^loc>< b \<^loc>* c"

   233

   234 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..

   235

   236 instance ordered_semiring_strict \<subseteq> ordered_semiring

   237 proof

   238   fix a b c :: 'a

   239   assume A: "a \<le> b" "0 \<le> c"

   240   from A show "c * a \<le> c * b"

   241     unfolding order_le_less

   242     using mult_strict_left_mono by auto

   243   from A show "a * c \<le> b * c"

   244     unfolding order_le_less

   245     using mult_strict_right_mono by auto

   246 qed

   247

   248 class mult_mono1 = times + zero + ord +

   249   assumes mult_mono: "a \<^loc>\<le> b \<Longrightarrow> \<^loc>0 \<^loc>\<le> c \<Longrightarrow> c \<^loc>* a \<^loc>\<le> c \<^loc>* b"

   250

   251 class pordered_comm_semiring = comm_semiring_0

   252   + pordered_ab_semigroup_add + mult_mono1

   253

   254 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   255   + pordered_ab_semigroup_add + mult_mono1

   256

   257 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..

   258

   259 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

   260   assumes mult_strict_mono: "a \<^loc>< b \<Longrightarrow> \<^loc>0 \<^loc>< c \<Longrightarrow> c \<^loc>* a \<^loc>< c \<^loc>* b"

   261

   262 instance pordered_comm_semiring \<subseteq> pordered_semiring

   263 proof

   264   fix a b c :: 'a

   265   assume "a \<le> b" "0 \<le> c"

   266   thus "c * a \<le> c * b" by (rule mult_mono)

   267   thus "a * c \<le> b * c" by (simp only: mult_commute)

   268 qed

   269

   270 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..

   271

   272 instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict

   273 proof

   274   fix a b c :: 'a

   275   assume "a < b" "0 < c"

   276   thus "c * a < c * b" by (rule mult_strict_mono)

   277   thus "a * c < b * c" by (simp only: mult_commute)

   278 qed

   279

   280 instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring

   281 proof

   282   fix a b c :: 'a

   283   assume "a \<le> b" "0 \<le> c"

   284   thus "c * a \<le> c * b"

   285     unfolding order_le_less

   286     using mult_strict_mono by auto

   287 qed

   288

   289 class pordered_ring = ring + pordered_cancel_semiring

   290

   291 instance pordered_ring \<subseteq> pordered_ab_group_add ..

   292

   293 class lordered_ring = pordered_ring + lordered_ab_group_abs

   294

   295 instance lordered_ring \<subseteq> lordered_ab_group_meet ..

   296

   297 instance lordered_ring \<subseteq> lordered_ab_group_join ..

   298

   299 class abs_if = minus + ord + zero + abs +

   300   assumes abs_if: "abs a = (if a \<^loc>< \<^loc>0 then (uminus a) else a)"

   301

   302 class sgn_if = sgn + zero + one + minus + ord +

   303   assumes sgn_if: "sgn x = (if x = \<^loc>0 then \<^loc>0 else if \<^loc>0 \<^loc>< x then \<^loc>1 else uminus \<^loc>1)"

   304

   305 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.

   306    Basically, ordered_ring + no_zero_divisors = ordered_ring_strict.

   307  *)

   308 class ordered_ring = ring + ordered_semiring + lordered_ab_group + abs_if

   309

   310 instance ordered_ring \<subseteq> lordered_ring

   311 proof

   312   fix x :: 'a

   313   show "\<bar>x\<bar> = sup x (- x)"

   314     by (simp only: abs_if sup_eq_if)

   315 qed

   316

   317 class ordered_ring_strict =

   318   ring + ordered_semiring_strict + lordered_ab_group + abs_if

   319

   320 instance ordered_ring_strict \<subseteq> ordered_ring ..

   321

   322 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   323

   324 instance pordered_comm_ring \<subseteq> pordered_ring ..

   325

   326 instance pordered_comm_ring \<subseteq> pordered_cancel_comm_semiring ..

   327

   328 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   329   (*previously ordered_semiring*)

   330   assumes zero_less_one [simp]: "\<^loc>0 \<^loc>< \<^loc>1"

   331

   332 lemma pos_add_strict:

   333   fixes a b c :: "'a\<Colon>ordered_semidom"

   334   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"

   335   using add_strict_mono [of 0 a b c] by simp

   336

   337 class ordered_idom =

   338   comm_ring_1 +

   339   ordered_comm_semiring_strict +

   340   lordered_ab_group +

   341   abs_if + sgn_if

   342   (*previously ordered_ring*)

   343

   344 instance ordered_idom \<subseteq> ordered_ring_strict ..

   345

   346 instance ordered_idom \<subseteq> pordered_comm_ring ..

   347

   348 class ordered_field = field + ordered_idom

   349

   350 lemma linorder_neqE_ordered_idom:

   351   fixes x y :: "'a :: ordered_idom"

   352   assumes "x \<noteq> y" obtains "x < y" | "y < x"

   353   using assms by (rule linorder_neqE)

   354

   355 lemma eq_add_iff1:

   356   "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"

   357 by (simp add: ring_simps)

   358

   359 lemma eq_add_iff2:

   360   "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"

   361 by (simp add: ring_simps)

   362

   363 lemma less_add_iff1:

   364   "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::pordered_ring))"

   365 by (simp add: ring_simps)

   366

   367 lemma less_add_iff2:

   368   "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::pordered_ring))"

   369 by (simp add: ring_simps)

   370

   371 lemma le_add_iff1:

   372   "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::pordered_ring))"

   373 by (simp add: ring_simps)

   374

   375 lemma le_add_iff2:

   376   "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::pordered_ring))"

   377 by (simp add: ring_simps)

   378

   379

   380 subsection {* Ordering Rules for Multiplication *}

   381

   382 lemma mult_left_le_imp_le:

   383   "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"

   384 by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])

   385

   386 lemma mult_right_le_imp_le:

   387   "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring_strict)"

   388 by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])

   389

   390 lemma mult_left_less_imp_less:

   391   "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"

   392 by (force simp add: mult_left_mono linorder_not_le [symmetric])

   393

   394 lemma mult_right_less_imp_less:

   395   "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"

   396 by (force simp add: mult_right_mono linorder_not_le [symmetric])

   397

   398 lemma mult_strict_left_mono_neg:

   399   "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring_strict)"

   400 apply (drule mult_strict_left_mono [of _ _ "-c"])

   401 apply (simp_all add: minus_mult_left [symmetric])

   402 done

   403

   404 lemma mult_left_mono_neg:

   405   "[|b \<le> a; c \<le> 0|] ==> c * a \<le>  c * (b::'a::pordered_ring)"

   406 apply (drule mult_left_mono [of _ _ "-c"])

   407 apply (simp_all add: minus_mult_left [symmetric])

   408 done

   409

   410 lemma mult_strict_right_mono_neg:

   411   "[|b < a; c < 0|] ==> a * c < b * (c::'a::ordered_ring_strict)"

   412 apply (drule mult_strict_right_mono [of _ _ "-c"])

   413 apply (simp_all add: minus_mult_right [symmetric])

   414 done

   415

   416 lemma mult_right_mono_neg:

   417   "[|b \<le> a; c \<le> 0|] ==> a * c \<le>  (b::'a::pordered_ring) * c"

   418 apply (drule mult_right_mono [of _ _ "-c"])

   419 apply (simp)

   420 apply (simp_all add: minus_mult_right [symmetric])

   421 done

   422

   423

   424 subsection{* Products of Signs *}

   425

   426 lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"

   427 by (drule mult_strict_left_mono [of 0 b], auto)

   428

   429 lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"

   430 by (drule mult_left_mono [of 0 b], auto)

   431

   432 lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"

   433 by (drule mult_strict_left_mono [of b 0], auto)

   434

   435 lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"

   436 by (drule mult_left_mono [of b 0], auto)

   437

   438 lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0"

   439 by (drule mult_strict_right_mono[of b 0], auto)

   440

   441 lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0"

   442 by (drule mult_right_mono[of b 0], auto)

   443

   444 lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"

   445 by (drule mult_strict_right_mono_neg, auto)

   446

   447 lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"

   448 by (drule mult_right_mono_neg[of a 0 b ], auto)

   449

   450 lemma zero_less_mult_pos:

   451      "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"

   452 apply (cases "b\<le>0")

   453  apply (auto simp add: order_le_less linorder_not_less)

   454 apply (drule_tac mult_pos_neg [of a b])

   455  apply (auto dest: order_less_not_sym)

   456 done

   457

   458 lemma zero_less_mult_pos2:

   459      "[| 0 < b*a; 0 < a|] ==> 0 < (b::'a::ordered_semiring_strict)"

   460 apply (cases "b\<le>0")

   461  apply (auto simp add: order_le_less linorder_not_less)

   462 apply (drule_tac mult_pos_neg2 [of a b])

   463  apply (auto dest: order_less_not_sym)

   464 done

   465

   466 lemma zero_less_mult_iff:

   467      "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"

   468 apply (auto simp add: order_le_less linorder_not_less mult_pos_pos

   469   mult_neg_neg)

   470 apply (blast dest: zero_less_mult_pos)

   471 apply (blast dest: zero_less_mult_pos2)

   472 done

   473

   474 lemma mult_eq_0_iff [simp]:

   475   fixes a b :: "'a::ring_no_zero_divisors"

   476   shows "(a * b = 0) = (a = 0 \<or> b = 0)"

   477 by (cases "a = 0 \<or> b = 0", auto dest: no_zero_divisors)

   478

   479 instance ordered_ring_strict \<subseteq> ring_no_zero_divisors

   480 apply intro_classes

   481 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)

   482 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+

   483 done

   484

   485 lemma zero_le_mult_iff:

   486      "((0::'a::ordered_ring_strict) \<le> a*b) = (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

   487 by (auto simp add: eq_commute [of 0] order_le_less linorder_not_less

   488                    zero_less_mult_iff)

   489

   490 lemma mult_less_0_iff:

   491      "(a*b < (0::'a::ordered_ring_strict)) = (0 < a & b < 0 | a < 0 & 0 < b)"

   492 apply (insert zero_less_mult_iff [of "-a" b])

   493 apply (force simp add: minus_mult_left[symmetric])

   494 done

   495

   496 lemma mult_le_0_iff:

   497      "(a*b \<le> (0::'a::ordered_ring_strict)) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

   498 apply (insert zero_le_mult_iff [of "-a" b])

   499 apply (force simp add: minus_mult_left[symmetric])

   500 done

   501

   502 lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"

   503 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   504

   505 lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (0::_::pordered_cancel_semiring)"

   506 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   507

   508 lemma zero_le_square[simp]: "(0::'a::ordered_ring_strict) \<le> a*a"

   509 by (simp add: zero_le_mult_iff linorder_linear)

   510

   511 lemma not_square_less_zero[simp]: "\<not> (a * a < (0::'a::ordered_ring_strict))"

   512 by (simp add: not_less)

   513

   514 text{*Proving axiom @{text zero_less_one} makes all @{text ordered_semidom}

   515       theorems available to members of @{term ordered_idom} *}

   516

   517 instance ordered_idom \<subseteq> ordered_semidom

   518 proof

   519   have "(0::'a) \<le> 1*1" by (rule zero_le_square)

   520   thus "(0::'a) < 1" by (simp add: order_le_less)

   521 qed

   522

   523 instance ordered_idom \<subseteq> idom ..

   524

   525 text{*All three types of comparision involving 0 and 1 are covered.*}

   526

   527 lemmas one_neq_zero = zero_neq_one [THEN not_sym]

   528 declare one_neq_zero [simp]

   529

   530 lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \<le> 1"

   531   by (rule zero_less_one [THEN order_less_imp_le])

   532

   533 lemma not_one_le_zero [simp]: "~ (1::'a::ordered_semidom) \<le> 0"

   534 by (simp add: linorder_not_le)

   535

   536 lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0"

   537 by (simp add: linorder_not_less)

   538

   539

   540 subsection{*More Monotonicity*}

   541

   542 text{*Strict monotonicity in both arguments*}

   543 lemma mult_strict_mono:

   544      "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

   545 apply (cases "c=0")

   546  apply (simp add: mult_pos_pos)

   547 apply (erule mult_strict_right_mono [THEN order_less_trans])

   548  apply (force simp add: order_le_less)

   549 apply (erule mult_strict_left_mono, assumption)

   550 done

   551

   552 text{*This weaker variant has more natural premises*}

   553 lemma mult_strict_mono':

   554      "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"

   555 apply (rule mult_strict_mono)

   556 apply (blast intro: order_le_less_trans)+

   557 done

   558

   559 lemma mult_mono:

   560      "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|]

   561       ==> a * c  \<le>  b * (d::'a::pordered_semiring)"

   562 apply (erule mult_right_mono [THEN order_trans], assumption)

   563 apply (erule mult_left_mono, assumption)

   564 done

   565

   566 lemma mult_mono':

   567      "[|a \<le> b; c \<le> d; 0 \<le> a; 0 \<le> c|]

   568       ==> a * c  \<le>  b * (d::'a::pordered_semiring)"

   569 apply (rule mult_mono)

   570 apply (fast intro: order_trans)+

   571 done

   572

   573 lemma less_1_mult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::'a::ordered_semidom)"

   574 apply (insert mult_strict_mono [of 1 m 1 n])

   575 apply (simp add:  order_less_trans [OF zero_less_one])

   576 done

   577

   578 lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==>

   579     c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d"

   580   apply (subgoal_tac "a * c < b * c")

   581   apply (erule order_less_le_trans)

   582   apply (erule mult_left_mono)

   583   apply simp

   584   apply (erule mult_strict_right_mono)

   585   apply assumption

   586 done

   587

   588 lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==>

   589     c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d"

   590   apply (subgoal_tac "a * c <= b * c")

   591   apply (erule order_le_less_trans)

   592   apply (erule mult_strict_left_mono)

   593   apply simp

   594   apply (erule mult_right_mono)

   595   apply simp

   596 done

   597

   598

   599 subsection{*Cancellation Laws for Relationships With a Common Factor*}

   600

   601 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},

   602    also with the relations @{text "\<le>"} and equality.*}

   603

   604 text{*These disjunction'' versions produce two cases when the comparison is

   605  an assumption, but effectively four when the comparison is a goal.*}

   606

   607 lemma mult_less_cancel_right_disj:

   608     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

   609 apply (cases "c = 0")

   610 apply (auto simp add: linorder_neq_iff mult_strict_right_mono

   611                       mult_strict_right_mono_neg)

   612 apply (auto simp add: linorder_not_less

   613                       linorder_not_le [symmetric, of "a*c"]

   614                       linorder_not_le [symmetric, of a])

   615 apply (erule_tac [!] notE)

   616 apply (auto simp add: order_less_imp_le mult_right_mono

   617                       mult_right_mono_neg)

   618 done

   619

   620 lemma mult_less_cancel_left_disj:

   621     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"

   622 apply (cases "c = 0")

   623 apply (auto simp add: linorder_neq_iff mult_strict_left_mono

   624                       mult_strict_left_mono_neg)

   625 apply (auto simp add: linorder_not_less

   626                       linorder_not_le [symmetric, of "c*a"]

   627                       linorder_not_le [symmetric, of a])

   628 apply (erule_tac [!] notE)

   629 apply (auto simp add: order_less_imp_le mult_left_mono

   630                       mult_left_mono_neg)

   631 done

   632

   633

   634 text{*The conjunction of implication'' lemmas produce two cases when the

   635 comparison is a goal, but give four when the comparison is an assumption.*}

   636

   637 lemma mult_less_cancel_right:

   638   fixes c :: "'a :: ordered_ring_strict"

   639   shows      "(a*c < b*c) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"

   640 by (insert mult_less_cancel_right_disj [of a c b], auto)

   641

   642 lemma mult_less_cancel_left:

   643   fixes c :: "'a :: ordered_ring_strict"

   644   shows      "(c*a < c*b) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"

   645 by (insert mult_less_cancel_left_disj [of c a b], auto)

   646

   647 lemma mult_le_cancel_right:

   648      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

   649 by (simp add: linorder_not_less [symmetric] mult_less_cancel_right_disj)

   650

   651 lemma mult_le_cancel_left:

   652      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"

   653 by (simp add: linorder_not_less [symmetric] mult_less_cancel_left_disj)

   654

   655 lemma mult_less_imp_less_left:

   656       assumes less: "c*a < c*b" and nonneg: "0 \<le> c"

   657       shows "a < (b::'a::ordered_semiring_strict)"

   658 proof (rule ccontr)

   659   assume "~ a < b"

   660   hence "b \<le> a" by (simp add: linorder_not_less)

   661   hence "c*b \<le> c*a" using nonneg by (rule mult_left_mono)

   662   with this and less show False

   663     by (simp add: linorder_not_less [symmetric])

   664 qed

   665

   666 lemma mult_less_imp_less_right:

   667   assumes less: "a*c < b*c" and nonneg: "0 <= c"

   668   shows "a < (b::'a::ordered_semiring_strict)"

   669 proof (rule ccontr)

   670   assume "~ a < b"

   671   hence "b \<le> a" by (simp add: linorder_not_less)

   672   hence "b*c \<le> a*c" using nonneg by (rule mult_right_mono)

   673   with this and less show False

   674     by (simp add: linorder_not_less [symmetric])

   675 qed

   676

   677 text{*Cancellation of equalities with a common factor*}

   678 lemma mult_cancel_right [simp,noatp]:

   679   fixes a b c :: "'a::ring_no_zero_divisors"

   680   shows "(a * c = b * c) = (c = 0 \<or> a = b)"

   681 proof -

   682   have "(a * c = b * c) = ((a - b) * c = 0)"

   683     by (simp add: ring_distribs)

   684   thus ?thesis

   685     by (simp add: disj_commute)

   686 qed

   687

   688 lemma mult_cancel_left [simp,noatp]:

   689   fixes a b c :: "'a::ring_no_zero_divisors"

   690   shows "(c * a = c * b) = (c = 0 \<or> a = b)"

   691 proof -

   692   have "(c * a = c * b) = (c * (a - b) = 0)"

   693     by (simp add: ring_distribs)

   694   thus ?thesis

   695     by simp

   696 qed

   697

   698

   699 subsubsection{*Special Cancellation Simprules for Multiplication*}

   700

   701 text{*These also produce two cases when the comparison is a goal.*}

   702

   703 lemma mult_le_cancel_right1:

   704   fixes c :: "'a :: ordered_idom"

   705   shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"

   706 by (insert mult_le_cancel_right [of 1 c b], simp)

   707

   708 lemma mult_le_cancel_right2:

   709   fixes c :: "'a :: ordered_idom"

   710   shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"

   711 by (insert mult_le_cancel_right [of a c 1], simp)

   712

   713 lemma mult_le_cancel_left1:

   714   fixes c :: "'a :: ordered_idom"

   715   shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"

   716 by (insert mult_le_cancel_left [of c 1 b], simp)

   717

   718 lemma mult_le_cancel_left2:

   719   fixes c :: "'a :: ordered_idom"

   720   shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"

   721 by (insert mult_le_cancel_left [of c a 1], simp)

   722

   723 lemma mult_less_cancel_right1:

   724   fixes c :: "'a :: ordered_idom"

   725   shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"

   726 by (insert mult_less_cancel_right [of 1 c b], simp)

   727

   728 lemma mult_less_cancel_right2:

   729   fixes c :: "'a :: ordered_idom"

   730   shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"

   731 by (insert mult_less_cancel_right [of a c 1], simp)

   732

   733 lemma mult_less_cancel_left1:

   734   fixes c :: "'a :: ordered_idom"

   735   shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"

   736 by (insert mult_less_cancel_left [of c 1 b], simp)

   737

   738 lemma mult_less_cancel_left2:

   739   fixes c :: "'a :: ordered_idom"

   740   shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"

   741 by (insert mult_less_cancel_left [of c a 1], simp)

   742

   743 lemma mult_cancel_right1 [simp]:

   744   fixes c :: "'a :: ring_1_no_zero_divisors"

   745   shows "(c = b*c) = (c = 0 | b=1)"

   746 by (insert mult_cancel_right [of 1 c b], force)

   747

   748 lemma mult_cancel_right2 [simp]:

   749   fixes c :: "'a :: ring_1_no_zero_divisors"

   750   shows "(a*c = c) = (c = 0 | a=1)"

   751 by (insert mult_cancel_right [of a c 1], simp)

   752

   753 lemma mult_cancel_left1 [simp]:

   754   fixes c :: "'a :: ring_1_no_zero_divisors"

   755   shows "(c = c*b) = (c = 0 | b=1)"

   756 by (insert mult_cancel_left [of c 1 b], force)

   757

   758 lemma mult_cancel_left2 [simp]:

   759   fixes c :: "'a :: ring_1_no_zero_divisors"

   760   shows "(c*a = c) = (c = 0 | a=1)"

   761 by (insert mult_cancel_left [of c a 1], simp)

   762

   763

   764 text{*Simprules for comparisons where common factors can be cancelled.*}

   765 lemmas mult_compare_simps =

   766     mult_le_cancel_right mult_le_cancel_left

   767     mult_le_cancel_right1 mult_le_cancel_right2

   768     mult_le_cancel_left1 mult_le_cancel_left2

   769     mult_less_cancel_right mult_less_cancel_left

   770     mult_less_cancel_right1 mult_less_cancel_right2

   771     mult_less_cancel_left1 mult_less_cancel_left2

   772     mult_cancel_right mult_cancel_left

   773     mult_cancel_right1 mult_cancel_right2

   774     mult_cancel_left1 mult_cancel_left2

   775

   776

   777 subsection {* Fields *}

   778

   779 lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"

   780 proof

   781   assume neq: "b \<noteq> 0"

   782   {

   783     hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)

   784     also assume "a / b = 1"

   785     finally show "a = b" by simp

   786   next

   787     assume "a = b"

   788     with neq show "a / b = 1" by (simp add: divide_inverse)

   789   }

   790 qed

   791

   792 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"

   793 by (simp add: divide_inverse)

   794

   795 lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"

   796   by (simp add: divide_inverse)

   797

   798 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"

   799 by (simp add: divide_inverse)

   800

   801 lemma divide_self_if [simp]:

   802      "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"

   803   by (simp add: divide_self)

   804

   805 lemma divide_zero_left [simp]: "0/a = (0::'a::field)"

   806 by (simp add: divide_inverse)

   807

   808 lemma inverse_eq_divide: "inverse (a::'a::field) = 1/a"

   809 by (simp add: divide_inverse)

   810

   811 lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"

   812 by (simp add: divide_inverse ring_distribs)

   813

   814 (* what ordering?? this is a straight instance of mult_eq_0_iff

   815 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement

   816       of an ordering.*}

   817 lemma field_mult_eq_0_iff [simp]:

   818   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"

   819 by simp

   820 *)

   821 (* subsumed by mult_cancel lemmas on ring_no_zero_divisors

   822 text{*Cancellation of equalities with a common factor*}

   823 lemma field_mult_cancel_right_lemma:

   824       assumes cnz: "c \<noteq> (0::'a::division_ring)"

   825          and eq:  "a*c = b*c"

   826         shows "a=b"

   827 proof -

   828   have "(a * c) * inverse c = (b * c) * inverse c"

   829     by (simp add: eq)

   830   thus "a=b"

   831     by (simp add: mult_assoc cnz)

   832 qed

   833

   834 lemma field_mult_cancel_right [simp]:

   835      "(a*c = b*c) = (c = (0::'a::division_ring) | a=b)"

   836 by simp

   837

   838 lemma field_mult_cancel_left [simp]:

   839      "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"

   840 by simp

   841 *)

   842 lemma nonzero_imp_inverse_nonzero:

   843   "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"

   844 proof

   845   assume ianz: "inverse a = 0"

   846   assume "a \<noteq> 0"

   847   hence "1 = a * inverse a" by simp

   848   also have "... = 0" by (simp add: ianz)

   849   finally have "1 = (0::'a::division_ring)" .

   850   thus False by (simp add: eq_commute)

   851 qed

   852

   853

   854 subsection{*Basic Properties of @{term inverse}*}

   855

   856 lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::division_ring)"

   857 apply (rule ccontr)

   858 apply (blast dest: nonzero_imp_inverse_nonzero)

   859 done

   860

   861 lemma inverse_nonzero_imp_nonzero:

   862    "inverse a = 0 ==> a = (0::'a::division_ring)"

   863 apply (rule ccontr)

   864 apply (blast dest: nonzero_imp_inverse_nonzero)

   865 done

   866

   867 lemma inverse_nonzero_iff_nonzero [simp]:

   868    "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"

   869 by (force dest: inverse_nonzero_imp_nonzero)

   870

   871 lemma nonzero_inverse_minus_eq:

   872       assumes [simp]: "a\<noteq>0"

   873       shows "inverse(-a) = -inverse(a::'a::division_ring)"

   874 proof -

   875   have "-a * inverse (- a) = -a * - inverse a"

   876     by simp

   877   thus ?thesis

   878     by (simp only: mult_cancel_left, simp)

   879 qed

   880

   881 lemma inverse_minus_eq [simp]:

   882    "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"

   883 proof cases

   884   assume "a=0" thus ?thesis by (simp add: inverse_zero)

   885 next

   886   assume "a\<noteq>0"

   887   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   888 qed

   889

   890 lemma nonzero_inverse_eq_imp_eq:

   891       assumes inveq: "inverse a = inverse b"

   892 	  and anz:  "a \<noteq> 0"

   893 	  and bnz:  "b \<noteq> 0"

   894 	 shows "a = (b::'a::division_ring)"

   895 proof -

   896   have "a * inverse b = a * inverse a"

   897     by (simp add: inveq)

   898   hence "(a * inverse b) * b = (a * inverse a) * b"

   899     by simp

   900   thus "a = b"

   901     by (simp add: mult_assoc anz bnz)

   902 qed

   903

   904 lemma inverse_eq_imp_eq:

   905   "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"

   906 apply (cases "a=0 | b=0")

   907  apply (force dest!: inverse_zero_imp_zero

   908               simp add: eq_commute [of "0::'a"])

   909 apply (force dest!: nonzero_inverse_eq_imp_eq)

   910 done

   911

   912 lemma inverse_eq_iff_eq [simp]:

   913   "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"

   914 by (force dest!: inverse_eq_imp_eq)

   915

   916 lemma nonzero_inverse_inverse_eq:

   917       assumes [simp]: "a \<noteq> 0"

   918       shows "inverse(inverse (a::'a::division_ring)) = a"

   919   proof -

   920   have "(inverse (inverse a) * inverse a) * a = a"

   921     by (simp add: nonzero_imp_inverse_nonzero)

   922   thus ?thesis

   923     by (simp add: mult_assoc)

   924   qed

   925

   926 lemma inverse_inverse_eq [simp]:

   927      "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"

   928   proof cases

   929     assume "a=0" thus ?thesis by simp

   930   next

   931     assume "a\<noteq>0"

   932     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

   933   qed

   934

   935 lemma inverse_1 [simp]: "inverse 1 = (1::'a::division_ring)"

   936   proof -

   937   have "inverse 1 * 1 = (1::'a::division_ring)"

   938     by (rule left_inverse [OF zero_neq_one [symmetric]])

   939   thus ?thesis  by simp

   940   qed

   941

   942 lemma inverse_unique:

   943   assumes ab: "a*b = 1"

   944   shows "inverse a = (b::'a::division_ring)"

   945 proof -

   946   have "a \<noteq> 0" using ab by auto

   947   moreover have "inverse a * (a * b) = inverse a" by (simp add: ab)

   948   ultimately show ?thesis by (simp add: mult_assoc [symmetric])

   949 qed

   950

   951 lemma nonzero_inverse_mult_distrib:

   952       assumes anz: "a \<noteq> 0"

   953           and bnz: "b \<noteq> 0"

   954       shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"

   955   proof -

   956   have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)"

   957     by (simp add: anz bnz)

   958   hence "inverse(a*b) * a = inverse(b)"

   959     by (simp add: mult_assoc bnz)

   960   hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)"

   961     by simp

   962   thus ?thesis

   963     by (simp add: mult_assoc anz)

   964   qed

   965

   966 text{*This version builds in division by zero while also re-orienting

   967       the right-hand side.*}

   968 lemma inverse_mult_distrib [simp]:

   969      "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"

   970   proof cases

   971     assume "a \<noteq> 0 & b \<noteq> 0"

   972     thus ?thesis

   973       by (simp add: nonzero_inverse_mult_distrib mult_commute)

   974   next

   975     assume "~ (a \<noteq> 0 & b \<noteq> 0)"

   976     thus ?thesis

   977       by force

   978   qed

   979

   980 lemma division_ring_inverse_add:

   981   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]

   982    ==> inverse a + inverse b = inverse a * (a+b) * inverse b"

   983 by (simp add: ring_simps)

   984

   985 lemma division_ring_inverse_diff:

   986   "[|(a::'a::division_ring) \<noteq> 0; b \<noteq> 0|]

   987    ==> inverse a - inverse b = inverse a * (b-a) * inverse b"

   988 by (simp add: ring_simps)

   989

   990 text{*There is no slick version using division by zero.*}

   991 lemma inverse_add:

   992   "[|a \<noteq> 0;  b \<noteq> 0|]

   993    ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"

   994 by (simp add: division_ring_inverse_add mult_ac)

   995

   996 lemma inverse_divide [simp]:

   997   "inverse (a/b) = b / (a::'a::{field,division_by_zero})"

   998 by (simp add: divide_inverse mult_commute)

   999

  1000

  1001 subsection {* Calculations with fractions *}

  1002

  1003 text{* There is a whole bunch of simp-rules just for class @{text

  1004 field} but none for class @{text field} and @{text nonzero_divides}

  1005 because the latter are covered by a simproc. *}

  1006

  1007 lemma nonzero_mult_divide_mult_cancel_left[simp,noatp]:

  1008 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"

  1009 proof -

  1010   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"

  1011     by (simp add: divide_inverse nonzero_inverse_mult_distrib)

  1012   also have "... =  a * inverse b * (inverse c * c)"

  1013     by (simp only: mult_ac)

  1014   also have "... =  a * inverse b"

  1015     by simp

  1016     finally show ?thesis

  1017     by (simp add: divide_inverse)

  1018 qed

  1019

  1020 lemma mult_divide_mult_cancel_left:

  1021   "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"

  1022 apply (cases "b = 0")

  1023 apply (simp_all add: nonzero_mult_divide_mult_cancel_left)

  1024 done

  1025

  1026 lemma nonzero_mult_divide_mult_cancel_right [noatp]:

  1027   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"

  1028 by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left)

  1029

  1030 lemma mult_divide_mult_cancel_right:

  1031   "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"

  1032 apply (cases "b = 0")

  1033 apply (simp_all add: nonzero_mult_divide_mult_cancel_right)

  1034 done

  1035

  1036 lemma divide_1 [simp]: "a/1 = (a::'a::field)"

  1037 by (simp add: divide_inverse)

  1038

  1039 lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"

  1040 by (simp add: divide_inverse mult_assoc)

  1041

  1042 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"

  1043 by (simp add: divide_inverse mult_ac)

  1044

  1045 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1046

  1047 lemma divide_divide_eq_right [simp,noatp]:

  1048   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"

  1049 by (simp add: divide_inverse mult_ac)

  1050

  1051 lemma divide_divide_eq_left [simp,noatp]:

  1052   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"

  1053 by (simp add: divide_inverse mult_assoc)

  1054

  1055 lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1056     x / y + w / z = (x * z + w * y) / (y * z)"

  1057 apply (subgoal_tac "x / y = (x * z) / (y * z)")

  1058 apply (erule ssubst)

  1059 apply (subgoal_tac "w / z = (w * y) / (y * z)")

  1060 apply (erule ssubst)

  1061 apply (rule add_divide_distrib [THEN sym])

  1062 apply (subst mult_commute)

  1063 apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])

  1064 apply assumption

  1065 apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])

  1066 apply assumption

  1067 done

  1068

  1069

  1070 subsubsection{*Special Cancellation Simprules for Division*}

  1071

  1072 lemma mult_divide_mult_cancel_left_if[simp,noatp]:

  1073 fixes c :: "'a :: {field,division_by_zero}"

  1074 shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"

  1075 by (simp add: mult_divide_mult_cancel_left)

  1076

  1077 lemma nonzero_mult_divide_cancel_right[simp,noatp]:

  1078   "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"

  1079 using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp

  1080

  1081 lemma nonzero_mult_divide_cancel_left[simp,noatp]:

  1082   "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"

  1083 using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp

  1084

  1085

  1086 lemma nonzero_divide_mult_cancel_right[simp,noatp]:

  1087   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"

  1088 using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp

  1089

  1090 lemma nonzero_divide_mult_cancel_left[simp,noatp]:

  1091   "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"

  1092 using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp

  1093

  1094

  1095 lemma nonzero_mult_divide_mult_cancel_left2[simp,noatp]:

  1096   "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"

  1097 using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)

  1098

  1099 lemma nonzero_mult_divide_mult_cancel_right2[simp,noatp]:

  1100   "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"

  1101 using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)

  1102

  1103

  1104 subsection {* Division and Unary Minus *}

  1105

  1106 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"

  1107 by (simp add: divide_inverse minus_mult_left)

  1108

  1109 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"

  1110 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1111

  1112 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"

  1113 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1114

  1115 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"

  1116 by (simp add: divide_inverse minus_mult_left [symmetric])

  1117

  1118 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"

  1119 by (simp add: divide_inverse minus_mult_right [symmetric])

  1120

  1121

  1122 text{*The effect is to extract signs from divisions*}

  1123 lemmas divide_minus_left = minus_divide_left [symmetric]

  1124 lemmas divide_minus_right = minus_divide_right [symmetric]

  1125 declare divide_minus_left [simp]   divide_minus_right [simp]

  1126

  1127 text{*Also, extract signs from products*}

  1128 lemmas mult_minus_left = minus_mult_left [symmetric]

  1129 lemmas mult_minus_right = minus_mult_right [symmetric]

  1130 declare mult_minus_left [simp]   mult_minus_right [simp]

  1131

  1132 lemma minus_divide_divide [simp]:

  1133   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"

  1134 apply (cases "b=0", simp)

  1135 apply (simp add: nonzero_minus_divide_divide)

  1136 done

  1137

  1138 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"

  1139 by (simp add: diff_minus add_divide_distrib)

  1140

  1141 lemma add_divide_eq_iff:

  1142   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"

  1143 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1144

  1145 lemma divide_add_eq_iff:

  1146   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"

  1147 by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)

  1148

  1149 lemma diff_divide_eq_iff:

  1150   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"

  1151 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1152

  1153 lemma divide_diff_eq_iff:

  1154   "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"

  1155 by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)

  1156

  1157 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"

  1158 proof -

  1159   assume [simp]: "c\<noteq>0"

  1160   have "(a = b/c) = (a*c = (b/c)*c)" by simp

  1161   also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)

  1162   finally show ?thesis .

  1163 qed

  1164

  1165 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"

  1166 proof -

  1167   assume [simp]: "c\<noteq>0"

  1168   have "(b/c = a) = ((b/c)*c = a*c)"  by simp

  1169   also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc)

  1170   finally show ?thesis .

  1171 qed

  1172

  1173 lemma eq_divide_eq:

  1174   "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"

  1175 by (simp add: nonzero_eq_divide_eq)

  1176

  1177 lemma divide_eq_eq:

  1178   "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"

  1179 by (force simp add: nonzero_divide_eq_eq)

  1180

  1181 lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>

  1182     b = a * c ==> b / c = a"

  1183   by (subst divide_eq_eq, simp)

  1184

  1185 lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>

  1186     a * c = b ==> a = b / c"

  1187   by (subst eq_divide_eq, simp)

  1188

  1189

  1190 lemmas field_eq_simps = ring_simps

  1191   (* pull / out*)

  1192   add_divide_eq_iff divide_add_eq_iff

  1193   diff_divide_eq_iff divide_diff_eq_iff

  1194   (* multiply eqn *)

  1195   nonzero_eq_divide_eq nonzero_divide_eq_eq

  1196 (* is added later:

  1197   times_divide_eq_left times_divide_eq_right

  1198 *)

  1199

  1200 text{*An example:*}

  1201 lemma fixes a b c d e f :: "'a::field"

  1202 shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"

  1203 apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")

  1204  apply(simp add:field_eq_simps)

  1205 apply(simp)

  1206 done

  1207

  1208

  1209 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1210     x / y - w / z = (x * z - w * y) / (y * z)"

  1211 by (simp add:field_eq_simps times_divide_eq)

  1212

  1213 lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>

  1214     (x / y = w / z) = (x * z = w * y)"

  1215 by (simp add:field_eq_simps times_divide_eq)

  1216

  1217

  1218 subsection {* Ordered Fields *}

  1219

  1220 lemma positive_imp_inverse_positive:

  1221 assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"

  1222 proof -

  1223   have "0 < a * inverse a"

  1224     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)

  1225   thus "0 < inverse a"

  1226     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)

  1227 qed

  1228

  1229 lemma negative_imp_inverse_negative:

  1230   "a < 0 ==> inverse a < (0::'a::ordered_field)"

  1231 by (insert positive_imp_inverse_positive [of "-a"],

  1232     simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1233

  1234 lemma inverse_le_imp_le:

  1235 assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"

  1236 shows "b \<le> (a::'a::ordered_field)"

  1237 proof (rule classical)

  1238   assume "~ b \<le> a"

  1239   hence "a < b"  by (simp add: linorder_not_le)

  1240   hence bpos: "0 < b"  by (blast intro: apos order_less_trans)

  1241   hence "a * inverse a \<le> a * inverse b"

  1242     by (simp add: apos invle order_less_imp_le mult_left_mono)

  1243   hence "(a * inverse a) * b \<le> (a * inverse b) * b"

  1244     by (simp add: bpos order_less_imp_le mult_right_mono)

  1245   thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)

  1246 qed

  1247

  1248 lemma inverse_positive_imp_positive:

  1249 assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"

  1250 shows "0 < (a::'a::ordered_field)"

  1251 proof -

  1252   have "0 < inverse (inverse a)"

  1253     using inv_gt_0 by (rule positive_imp_inverse_positive)

  1254   thus "0 < a"

  1255     using nz by (simp add: nonzero_inverse_inverse_eq)

  1256 qed

  1257

  1258 lemma inverse_positive_iff_positive [simp]:

  1259   "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"

  1260 apply (cases "a = 0", simp)

  1261 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1262 done

  1263

  1264 lemma inverse_negative_imp_negative:

  1265 assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"

  1266 shows "a < (0::'a::ordered_field)"

  1267 proof -

  1268   have "inverse (inverse a) < 0"

  1269     using inv_less_0 by (rule negative_imp_inverse_negative)

  1270   thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)

  1271 qed

  1272

  1273 lemma inverse_negative_iff_negative [simp]:

  1274   "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"

  1275 apply (cases "a = 0", simp)

  1276 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1277 done

  1278

  1279 lemma inverse_nonnegative_iff_nonnegative [simp]:

  1280   "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"

  1281 by (simp add: linorder_not_less [symmetric])

  1282

  1283 lemma inverse_nonpositive_iff_nonpositive [simp]:

  1284   "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"

  1285 by (simp add: linorder_not_less [symmetric])

  1286

  1287 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"

  1288 proof

  1289   fix x::'a

  1290   have m1: "- (1::'a) < 0" by simp

  1291   from add_strict_right_mono[OF m1, where c=x]

  1292   have "(- 1) + x < x" by simp

  1293   thus "\<exists>y. y < x" by blast

  1294 qed

  1295

  1296 lemma ordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::ordered_field)"

  1297 proof

  1298   fix x::'a

  1299   have m1: " (1::'a) > 0" by simp

  1300   from add_strict_right_mono[OF m1, where c=x]

  1301   have "1 + x > x" by simp

  1302   thus "\<exists>y. y > x" by blast

  1303 qed

  1304

  1305 subsection{*Anti-Monotonicity of @{term inverse}*}

  1306

  1307 lemma less_imp_inverse_less:

  1308 assumes less: "a < b" and apos:  "0 < a"

  1309 shows "inverse b < inverse (a::'a::ordered_field)"

  1310 proof (rule ccontr)

  1311   assume "~ inverse b < inverse a"

  1312   hence "inverse a \<le> inverse b"

  1313     by (simp add: linorder_not_less)

  1314   hence "~ (a < b)"

  1315     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])

  1316   thus False

  1317     by (rule notE [OF _ less])

  1318 qed

  1319

  1320 lemma inverse_less_imp_less:

  1321   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"

  1322 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])

  1323 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1324 done

  1325

  1326 text{*Both premises are essential. Consider -1 and 1.*}

  1327 lemma inverse_less_iff_less [simp,noatp]:

  1328   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

  1329 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1330

  1331 lemma le_imp_inverse_le:

  1332   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"

  1333 by (force simp add: order_le_less less_imp_inverse_less)

  1334

  1335 lemma inverse_le_iff_le [simp,noatp]:

  1336  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1337 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1338

  1339

  1340 text{*These results refer to both operands being negative.  The opposite-sign

  1341 case is trivial, since inverse preserves signs.*}

  1342 lemma inverse_le_imp_le_neg:

  1343   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"

  1344 apply (rule classical)

  1345 apply (subgoal_tac "a < 0")

  1346  prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)

  1347 apply (insert inverse_le_imp_le [of "-b" "-a"])

  1348 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1349 done

  1350

  1351 lemma less_imp_inverse_less_neg:

  1352    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"

  1353 apply (subgoal_tac "a < 0")

  1354  prefer 2 apply (blast intro: order_less_trans)

  1355 apply (insert less_imp_inverse_less [of "-b" "-a"])

  1356 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1357 done

  1358

  1359 lemma inverse_less_imp_less_neg:

  1360    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"

  1361 apply (rule classical)

  1362 apply (subgoal_tac "a < 0")

  1363  prefer 2

  1364  apply (force simp add: linorder_not_less intro: order_le_less_trans)

  1365 apply (insert inverse_less_imp_less [of "-b" "-a"])

  1366 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1367 done

  1368

  1369 lemma inverse_less_iff_less_neg [simp,noatp]:

  1370   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

  1371 apply (insert inverse_less_iff_less [of "-b" "-a"])

  1372 apply (simp del: inverse_less_iff_less

  1373             add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1374 done

  1375

  1376 lemma le_imp_inverse_le_neg:

  1377   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"

  1378 by (force simp add: order_le_less less_imp_inverse_less_neg)

  1379

  1380 lemma inverse_le_iff_le_neg [simp,noatp]:

  1381  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1382 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1383

  1384

  1385 subsection{*Inverses and the Number One*}

  1386

  1387 lemma one_less_inverse_iff:

  1388   "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"

  1389 proof cases

  1390   assume "0 < x"

  1391     with inverse_less_iff_less [OF zero_less_one, of x]

  1392     show ?thesis by simp

  1393 next

  1394   assume notless: "~ (0 < x)"

  1395   have "~ (1 < inverse x)"

  1396   proof

  1397     assume "1 < inverse x"

  1398     also with notless have "... \<le> 0" by (simp add: linorder_not_less)

  1399     also have "... < 1" by (rule zero_less_one)

  1400     finally show False by auto

  1401   qed

  1402   with notless show ?thesis by simp

  1403 qed

  1404

  1405 lemma inverse_eq_1_iff [simp]:

  1406   "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"

  1407 by (insert inverse_eq_iff_eq [of x 1], simp)

  1408

  1409 lemma one_le_inverse_iff:

  1410   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"

  1411 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1412                     eq_commute [of 1])

  1413

  1414 lemma inverse_less_1_iff:

  1415   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"

  1416 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)

  1417

  1418 lemma inverse_le_1_iff:

  1419   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"

  1420 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)

  1421

  1422

  1423 subsection{*Simplification of Inequalities Involving Literal Divisors*}

  1424

  1425 lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"

  1426 proof -

  1427   assume less: "0<c"

  1428   hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"

  1429     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1430   also have "... = (a*c \<le> b)"

  1431     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1432   finally show ?thesis .

  1433 qed

  1434

  1435 lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"

  1436 proof -

  1437   assume less: "c<0"

  1438   hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"

  1439     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1440   also have "... = (b \<le> a*c)"

  1441     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1442   finally show ?thesis .

  1443 qed

  1444

  1445 lemma le_divide_eq:

  1446   "(a \<le> b/c) =

  1447    (if 0 < c then a*c \<le> b

  1448              else if c < 0 then b \<le> a*c

  1449              else  a \<le> (0::'a::{ordered_field,division_by_zero}))"

  1450 apply (cases "c=0", simp)

  1451 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1452 done

  1453

  1454 lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"

  1455 proof -

  1456   assume less: "0<c"

  1457   hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"

  1458     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1459   also have "... = (b \<le> a*c)"

  1460     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1461   finally show ?thesis .

  1462 qed

  1463

  1464 lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"

  1465 proof -

  1466   assume less: "c<0"

  1467   hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"

  1468     by (simp add: mult_le_cancel_right order_less_not_sym [OF less])

  1469   also have "... = (a*c \<le> b)"

  1470     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1471   finally show ?thesis .

  1472 qed

  1473

  1474 lemma divide_le_eq:

  1475   "(b/c \<le> a) =

  1476    (if 0 < c then b \<le> a*c

  1477              else if c < 0 then a*c \<le> b

  1478              else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"

  1479 apply (cases "c=0", simp)

  1480 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1481 done

  1482

  1483 lemma pos_less_divide_eq:

  1484      "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"

  1485 proof -

  1486   assume less: "0<c"

  1487   hence "(a < b/c) = (a*c < (b/c)*c)"

  1488     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1489   also have "... = (a*c < b)"

  1490     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1491   finally show ?thesis .

  1492 qed

  1493

  1494 lemma neg_less_divide_eq:

  1495  "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"

  1496 proof -

  1497   assume less: "c<0"

  1498   hence "(a < b/c) = ((b/c)*c < a*c)"

  1499     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1500   also have "... = (b < a*c)"

  1501     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1502   finally show ?thesis .

  1503 qed

  1504

  1505 lemma less_divide_eq:

  1506   "(a < b/c) =

  1507    (if 0 < c then a*c < b

  1508              else if c < 0 then b < a*c

  1509              else  a < (0::'a::{ordered_field,division_by_zero}))"

  1510 apply (cases "c=0", simp)

  1511 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1512 done

  1513

  1514 lemma pos_divide_less_eq:

  1515      "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"

  1516 proof -

  1517   assume less: "0<c"

  1518   hence "(b/c < a) = ((b/c)*c < a*c)"

  1519     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1520   also have "... = (b < a*c)"

  1521     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)

  1522   finally show ?thesis .

  1523 qed

  1524

  1525 lemma neg_divide_less_eq:

  1526  "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"

  1527 proof -

  1528   assume less: "c<0"

  1529   hence "(b/c < a) = (a*c < (b/c)*c)"

  1530     by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])

  1531   also have "... = (a*c < b)"

  1532     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)

  1533   finally show ?thesis .

  1534 qed

  1535

  1536 lemma divide_less_eq:

  1537   "(b/c < a) =

  1538    (if 0 < c then b < a*c

  1539              else if c < 0 then a*c < b

  1540              else 0 < (a::'a::{ordered_field,division_by_zero}))"

  1541 apply (cases "c=0", simp)

  1542 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1543 done

  1544

  1545

  1546 subsection{*Field simplification*}

  1547

  1548 text{* Lemmas @{text field_simps} multiply with denominators in

  1549 in(equations) if they can be proved to be non-zero (for equations) or

  1550 positive/negative (for inequations). *}

  1551

  1552 lemmas field_simps = field_eq_simps

  1553   (* multiply ineqn *)

  1554   pos_divide_less_eq neg_divide_less_eq

  1555   pos_less_divide_eq neg_less_divide_eq

  1556   pos_divide_le_eq neg_divide_le_eq

  1557   pos_le_divide_eq neg_le_divide_eq

  1558

  1559 text{* Lemmas @{text sign_simps} is a first attempt to automate proofs

  1560 of positivity/negativity needed for @{text field_simps}. Have not added @{text

  1561 sign_simps} to @{text field_simps} because the former can lead to case

  1562 explosions. *}

  1563

  1564 lemmas sign_simps = group_simps

  1565   zero_less_mult_iff  mult_less_0_iff

  1566

  1567 (* Only works once linear arithmetic is installed:

  1568 text{*An example:*}

  1569 lemma fixes a b c d e f :: "'a::ordered_field"

  1570 shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>

  1571  ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <

  1572  ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"

  1573 apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")

  1574  prefer 2 apply(simp add:sign_simps)

  1575 apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")

  1576  prefer 2 apply(simp add:sign_simps)

  1577 apply(simp add:field_simps)

  1578 done

  1579 *)

  1580

  1581

  1582 subsection{*Division and Signs*}

  1583

  1584 lemma zero_less_divide_iff:

  1585      "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"

  1586 by (simp add: divide_inverse zero_less_mult_iff)

  1587

  1588 lemma divide_less_0_iff:

  1589      "(a/b < (0::'a::{ordered_field,division_by_zero})) =

  1590       (0 < a & b < 0 | a < 0 & 0 < b)"

  1591 by (simp add: divide_inverse mult_less_0_iff)

  1592

  1593 lemma zero_le_divide_iff:

  1594      "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =

  1595       (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"

  1596 by (simp add: divide_inverse zero_le_mult_iff)

  1597

  1598 lemma divide_le_0_iff:

  1599      "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =

  1600       (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"

  1601 by (simp add: divide_inverse mult_le_0_iff)

  1602

  1603 lemma divide_eq_0_iff [simp,noatp]:

  1604      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"

  1605 by (simp add: divide_inverse)

  1606

  1607 lemma divide_pos_pos:

  1608   "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"

  1609 by(simp add:field_simps)

  1610

  1611

  1612 lemma divide_nonneg_pos:

  1613   "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"

  1614 by(simp add:field_simps)

  1615

  1616 lemma divide_neg_pos:

  1617   "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"

  1618 by(simp add:field_simps)

  1619

  1620 lemma divide_nonpos_pos:

  1621   "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"

  1622 by(simp add:field_simps)

  1623

  1624 lemma divide_pos_neg:

  1625   "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"

  1626 by(simp add:field_simps)

  1627

  1628 lemma divide_nonneg_neg:

  1629   "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0"

  1630 by(simp add:field_simps)

  1631

  1632 lemma divide_neg_neg:

  1633   "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"

  1634 by(simp add:field_simps)

  1635

  1636 lemma divide_nonpos_neg:

  1637   "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"

  1638 by(simp add:field_simps)

  1639

  1640

  1641 subsection{*Cancellation Laws for Division*}

  1642

  1643 lemma divide_cancel_right [simp,noatp]:

  1644      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"

  1645 apply (cases "c=0", simp)

  1646 apply (simp add: divide_inverse)

  1647 done

  1648

  1649 lemma divide_cancel_left [simp,noatp]:

  1650      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"

  1651 apply (cases "c=0", simp)

  1652 apply (simp add: divide_inverse)

  1653 done

  1654

  1655

  1656 subsection {* Division and the Number One *}

  1657

  1658 text{*Simplify expressions equated with 1*}

  1659 lemma divide_eq_1_iff [simp,noatp]:

  1660      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"

  1661 apply (cases "b=0", simp)

  1662 apply (simp add: right_inverse_eq)

  1663 done

  1664

  1665 lemma one_eq_divide_iff [simp,noatp]:

  1666      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"

  1667 by (simp add: eq_commute [of 1])

  1668

  1669 lemma zero_eq_1_divide_iff [simp,noatp]:

  1670      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"

  1671 apply (cases "a=0", simp)

  1672 apply (auto simp add: nonzero_eq_divide_eq)

  1673 done

  1674

  1675 lemma one_divide_eq_0_iff [simp,noatp]:

  1676      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"

  1677 apply (cases "a=0", simp)

  1678 apply (insert zero_neq_one [THEN not_sym])

  1679 apply (auto simp add: nonzero_divide_eq_eq)

  1680 done

  1681

  1682 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}

  1683 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1684 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1685 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1686 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1687

  1688 declare zero_less_divide_1_iff [simp]

  1689 declare divide_less_0_1_iff [simp,noatp]

  1690 declare zero_le_divide_1_iff [simp]

  1691 declare divide_le_0_1_iff [simp,noatp]

  1692

  1693

  1694 subsection {* Ordering Rules for Division *}

  1695

  1696 lemma divide_strict_right_mono:

  1697      "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"

  1698 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1699               positive_imp_inverse_positive)

  1700

  1701 lemma divide_right_mono:

  1702      "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"

  1703 by (force simp add: divide_strict_right_mono order_le_less)

  1704

  1705 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b

  1706     ==> c <= 0 ==> b / c <= a / c"

  1707 apply (drule divide_right_mono [of _ _ "- c"])

  1708 apply auto

  1709 done

  1710

  1711 lemma divide_strict_right_mono_neg:

  1712      "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"

  1713 apply (drule divide_strict_right_mono [of _ _ "-c"], simp)

  1714 apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])

  1715 done

  1716

  1717 text{*The last premise ensures that @{term a} and @{term b}

  1718       have the same sign*}

  1719 lemma divide_strict_left_mono:

  1720   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"

  1721 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)

  1722

  1723 lemma divide_left_mono:

  1724   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"

  1725 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)

  1726

  1727 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b

  1728     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"

  1729   apply (drule divide_left_mono [of _ _ "- c"])

  1730   apply (auto simp add: mult_commute)

  1731 done

  1732

  1733 lemma divide_strict_left_mono_neg:

  1734   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"

  1735 by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)

  1736

  1737

  1738 text{*Simplify quotients that are compared with the value 1.*}

  1739

  1740 lemma le_divide_eq_1 [noatp]:

  1741   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1742   shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"

  1743 by (auto simp add: le_divide_eq)

  1744

  1745 lemma divide_le_eq_1 [noatp]:

  1746   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1747   shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"

  1748 by (auto simp add: divide_le_eq)

  1749

  1750 lemma less_divide_eq_1 [noatp]:

  1751   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1752   shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"

  1753 by (auto simp add: less_divide_eq)

  1754

  1755 lemma divide_less_eq_1 [noatp]:

  1756   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1757   shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"

  1758 by (auto simp add: divide_less_eq)

  1759

  1760

  1761 subsection{*Conditional Simplification Rules: No Case Splits*}

  1762

  1763 lemma le_divide_eq_1_pos [simp,noatp]:

  1764   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1765   shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"

  1766 by (auto simp add: le_divide_eq)

  1767

  1768 lemma le_divide_eq_1_neg [simp,noatp]:

  1769   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1770   shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"

  1771 by (auto simp add: le_divide_eq)

  1772

  1773 lemma divide_le_eq_1_pos [simp,noatp]:

  1774   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1775   shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"

  1776 by (auto simp add: divide_le_eq)

  1777

  1778 lemma divide_le_eq_1_neg [simp,noatp]:

  1779   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1780   shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"

  1781 by (auto simp add: divide_le_eq)

  1782

  1783 lemma less_divide_eq_1_pos [simp,noatp]:

  1784   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1785   shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"

  1786 by (auto simp add: less_divide_eq)

  1787

  1788 lemma less_divide_eq_1_neg [simp,noatp]:

  1789   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1790   shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"

  1791 by (auto simp add: less_divide_eq)

  1792

  1793 lemma divide_less_eq_1_pos [simp,noatp]:

  1794   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1795   shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"

  1796 by (auto simp add: divide_less_eq)

  1797

  1798 lemma divide_less_eq_1_neg [simp,noatp]:

  1799   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1800   shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"

  1801 by (auto simp add: divide_less_eq)

  1802

  1803 lemma eq_divide_eq_1 [simp,noatp]:

  1804   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1805   shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"

  1806 by (auto simp add: eq_divide_eq)

  1807

  1808 lemma divide_eq_eq_1 [simp,noatp]:

  1809   fixes a :: "'a :: {ordered_field,division_by_zero}"

  1810   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"

  1811 by (auto simp add: divide_eq_eq)

  1812

  1813

  1814 subsection {* Reasoning about inequalities with division *}

  1815

  1816 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1

  1817     ==> x * y <= x"

  1818   by (auto simp add: mult_compare_simps);

  1819

  1820 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1

  1821     ==> y * x <= x"

  1822   by (auto simp add: mult_compare_simps);

  1823

  1824 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>

  1825     x / y <= z";

  1826   by (subst pos_divide_le_eq, assumption+);

  1827

  1828 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>

  1829     z <= x / y"

  1830 by(simp add:field_simps)

  1831

  1832 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>

  1833     x / y < z"

  1834 by(simp add:field_simps)

  1835

  1836 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>

  1837     z < x / y"

  1838 by(simp add:field_simps)

  1839

  1840 lemma frac_le: "(0::'a::ordered_field) <= x ==>

  1841     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"

  1842   apply (rule mult_imp_div_pos_le)

  1843   apply simp;

  1844   apply (subst times_divide_eq_left);

  1845   apply (rule mult_imp_le_div_pos, assumption)

  1846   apply (rule mult_mono)

  1847   apply simp_all

  1848 done

  1849

  1850 lemma frac_less: "(0::'a::ordered_field) <= x ==>

  1851     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"

  1852   apply (rule mult_imp_div_pos_less)

  1853   apply simp;

  1854   apply (subst times_divide_eq_left);

  1855   apply (rule mult_imp_less_div_pos, assumption)

  1856   apply (erule mult_less_le_imp_less)

  1857   apply simp_all

  1858 done

  1859

  1860 lemma frac_less2: "(0::'a::ordered_field) < x ==>

  1861     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"

  1862   apply (rule mult_imp_div_pos_less)

  1863   apply simp_all

  1864   apply (subst times_divide_eq_left);

  1865   apply (rule mult_imp_less_div_pos, assumption)

  1866   apply (erule mult_le_less_imp_less)

  1867   apply simp_all

  1868 done

  1869

  1870 text{*It's not obvious whether these should be simprules or not.

  1871   Their effect is to gather terms into one big fraction, like

  1872   a*b*c / x*y*z. The rationale for that is unclear, but many proofs

  1873   seem to need them.*}

  1874

  1875 declare times_divide_eq [simp]

  1876

  1877

  1878 subsection {* Ordered Fields are Dense *}

  1879

  1880 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"

  1881 proof -

  1882   have "a+0 < (a+1::'a::ordered_semidom)"

  1883     by (blast intro: zero_less_one add_strict_left_mono)

  1884   thus ?thesis by simp

  1885 qed

  1886

  1887 lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"

  1888 by (blast intro: order_less_trans zero_less_one less_add_one)

  1889

  1890 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"

  1891 by (simp add: field_simps zero_less_two)

  1892

  1893 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"

  1894 by (simp add: field_simps zero_less_two)

  1895

  1896 instance ordered_field < dense_linear_order

  1897 proof

  1898   fix x y :: 'a

  1899   have "x < x + 1" by simp

  1900   then show "\<exists>y. x < y" ..

  1901   have "x - 1 < x" by simp

  1902   then show "\<exists>y. y < x" ..

  1903   show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)

  1904 qed

  1905

  1906

  1907 subsection {* Absolute Value *}

  1908

  1909 lemma mult_sgn_abs: "sgn x * abs x = (x::'a::{ordered_idom,linorder})"

  1910 using less_linear[of x 0]

  1911 by(auto simp: sgn_if abs_if)

  1912

  1913 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"

  1914 by (simp add: abs_if zero_less_one [THEN order_less_not_sym])

  1915

  1916 lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lordered_ring))"

  1917 proof -

  1918   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"

  1919   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"

  1920   have a: "(abs a) * (abs b) = ?x"

  1921     by (simp only: abs_prts[of a] abs_prts[of b] ring_simps)

  1922   {

  1923     fix u v :: 'a

  1924     have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>

  1925               u * v = pprt a * pprt b + pprt a * nprt b +

  1926                       nprt a * pprt b + nprt a * nprt b"

  1927       apply (subst prts[of u], subst prts[of v])

  1928       apply (simp add: ring_simps)

  1929       done

  1930   }

  1931   note b = this[OF refl[of a] refl[of b]]

  1932   note addm = add_mono[of "0::'a" _ "0::'a", simplified]

  1933   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]

  1934   have xy: "- ?x <= ?y"

  1935     apply (simp)

  1936     apply (rule_tac y="0::'a" in order_trans)

  1937     apply (rule addm2)

  1938     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1939     apply (rule addm)

  1940     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1941     done

  1942   have yx: "?y <= ?x"

  1943     apply (simp add:diff_def)

  1944     apply (rule_tac y=0 in order_trans)

  1945     apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)

  1946     apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)

  1947     done

  1948   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)

  1949   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)

  1950   show ?thesis

  1951     apply (rule abs_leI)

  1952     apply (simp add: i1)

  1953     apply (simp add: i2[simplified minus_le_iff])

  1954     done

  1955 qed

  1956

  1957 lemma abs_eq_mult:

  1958   assumes "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"

  1959   shows "abs (a*b) = abs a * abs (b::'a::lordered_ring)"

  1960 proof -

  1961   have s: "(0 <= a*b) | (a*b <= 0)"

  1962     apply (auto)

  1963     apply (rule_tac split_mult_pos_le)

  1964     apply (rule_tac contrapos_np[of "a*b <= 0"])

  1965     apply (simp)

  1966     apply (rule_tac split_mult_neg_le)

  1967     apply (insert prems)

  1968     apply (blast)

  1969     done

  1970   have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"

  1971     by (simp add: prts[symmetric])

  1972   show ?thesis

  1973   proof cases

  1974     assume "0 <= a * b"

  1975     then show ?thesis

  1976       apply (simp_all add: mulprts abs_prts)

  1977       apply (insert prems)

  1978       apply (auto simp add:

  1979 	ring_simps

  1980 	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]

  1981 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])

  1982 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)

  1983 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)

  1984       done

  1985   next

  1986     assume "~(0 <= a*b)"

  1987     with s have "a*b <= 0" by simp

  1988     then show ?thesis

  1989       apply (simp_all add: mulprts abs_prts)

  1990       apply (insert prems)

  1991       apply (auto simp add: ring_simps)

  1992       apply(drule (1) mult_nonneg_nonneg[of a b],simp)

  1993       apply(drule (1) mult_nonpos_nonpos[of a b],simp)

  1994       done

  1995   qed

  1996 qed

  1997

  1998 lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)"

  1999 by (simp add: abs_eq_mult linorder_linear)

  2000

  2001 lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"

  2002 by (simp add: abs_if)

  2003

  2004 lemma nonzero_abs_inverse:

  2005      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"

  2006 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  2007                       negative_imp_inverse_negative)

  2008 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  2009 done

  2010

  2011 lemma abs_inverse [simp]:

  2012      "abs (inverse (a::'a::{ordered_field,division_by_zero})) =

  2013       inverse (abs a)"

  2014 apply (cases "a=0", simp)

  2015 apply (simp add: nonzero_abs_inverse)

  2016 done

  2017

  2018 lemma nonzero_abs_divide:

  2019      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"

  2020 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  2021

  2022 lemma abs_divide [simp]:

  2023      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"

  2024 apply (cases "b=0", simp)

  2025 apply (simp add: nonzero_abs_divide)

  2026 done

  2027

  2028 lemma abs_mult_less:

  2029      "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_idom)"

  2030 proof -

  2031   assume ac: "abs a < c"

  2032   hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)

  2033   assume "abs b < d"

  2034   thus ?thesis by (simp add: ac cpos mult_strict_mono)

  2035 qed

  2036

  2037 lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_idom))"

  2038 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)

  2039

  2040 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"

  2041 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)

  2042

  2043 lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_idom))"

  2044 apply (simp add: order_less_le abs_le_iff)

  2045 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)

  2046 apply (simp add: le_minus_self_iff linorder_neq_iff)

  2047 done

  2048

  2049 lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==>

  2050     (abs y) * x = abs (y * x)";

  2051   apply (subst abs_mult);

  2052   apply simp;

  2053 done;

  2054

  2055 lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==>

  2056     abs x / y = abs (x / y)";

  2057   apply (subst abs_divide);

  2058   apply (simp add: order_less_imp_le);

  2059 done;

  2060

  2061

  2062 subsection {* Bounds of products via negative and positive Part *}

  2063

  2064 lemma mult_le_prts:

  2065   assumes

  2066   "a1 <= (a::'a::lordered_ring)"

  2067   "a <= a2"

  2068   "b1 <= b"

  2069   "b <= b2"

  2070   shows

  2071   "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"

  2072 proof -

  2073   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"

  2074     apply (subst prts[symmetric])+

  2075     apply simp

  2076     done

  2077   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"

  2078     by (simp add: ring_simps)

  2079   moreover have "pprt a * pprt b <= pprt a2 * pprt b2"

  2080     by (simp_all add: prems mult_mono)

  2081   moreover have "pprt a * nprt b <= pprt a1 * nprt b2"

  2082   proof -

  2083     have "pprt a * nprt b <= pprt a * nprt b2"

  2084       by (simp add: mult_left_mono prems)

  2085     moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"

  2086       by (simp add: mult_right_mono_neg prems)

  2087     ultimately show ?thesis

  2088       by simp

  2089   qed

  2090   moreover have "nprt a * pprt b <= nprt a2 * pprt b1"

  2091   proof -

  2092     have "nprt a * pprt b <= nprt a2 * pprt b"

  2093       by (simp add: mult_right_mono prems)

  2094     moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"

  2095       by (simp add: mult_left_mono_neg prems)

  2096     ultimately show ?thesis

  2097       by simp

  2098   qed

  2099   moreover have "nprt a * nprt b <= nprt a1 * nprt b1"

  2100   proof -

  2101     have "nprt a * nprt b <= nprt a * nprt b1"

  2102       by (simp add: mult_left_mono_neg prems)

  2103     moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"

  2104       by (simp add: mult_right_mono_neg prems)

  2105     ultimately show ?thesis

  2106       by simp

  2107   qed

  2108   ultimately show ?thesis

  2109     by - (rule add_mono | simp)+

  2110 qed

  2111

  2112 lemma mult_ge_prts:

  2113   assumes

  2114   "a1 <= (a::'a::lordered_ring)"

  2115   "a <= a2"

  2116   "b1 <= b"

  2117   "b <= b2"

  2118   shows

  2119   "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"

  2120 proof -

  2121   from prems have a1:"- a2 <= -a" by auto

  2122   from prems have a2: "-a <= -a1" by auto

  2123   from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]

  2124   have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp

  2125   then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"

  2126     by (simp only: minus_le_iff)

  2127   then show ?thesis by simp

  2128 qed

  2129

  2130

  2131 subsection {* Theorems for proof tools *}

  2132

  2133 lemma add_mono_thms_ordered_semiring [noatp]:

  2134   fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"

  2135   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  2136     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  2137     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"

  2138     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"

  2139 by (rule add_mono, clarify+)+

  2140

  2141 lemma add_mono_thms_ordered_field [noatp]:

  2142   fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"

  2143   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"

  2144     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"

  2145     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"

  2146     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"

  2147     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"

  2148 by (auto intro: add_strict_right_mono add_strict_left_mono

  2149   add_less_le_mono add_le_less_mono add_strict_mono)

  2150

  2151 end