src/HOL/Ring_and_Field.thy
 author haftmann Sun May 06 21:49:29 2007 +0200 (2007-05-06) changeset 22842 6d2fd4e0f984 parent 22548 6ce4bddf3bcb child 22987 550709aa8e66 permissions -rw-r--r--
added auxiliary lemmas for proof tools
     1 (*  Title:   HOL/Ring_and_Field.thy

     2     ID:      $Id$

     3     Author:  Gertrud Bauer, Steven Obua, 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 idom = comm_ring_1 + no_zero_divisors

   126

   127 class division_ring = ring_1 + inverse +

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

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

   130

   131 class field = comm_ring_1 + inverse +

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

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

   134

   135 lemma field_right_inverse:

   136   assumes not0: "a \<noteq> 0"

   137   shows "a * inverse (a::'a::field) = 1"

   138 proof -

   139   have "a * inverse a = inverse a * a" by (rule mult_commute)

   140   also have "... = 1" using not0 by (rule field_left_inverse)

   141   finally show ?thesis .

   142 qed

   143

   144 instance field \<subseteq> division_ring

   145 by (intro_classes, erule field_left_inverse, erule field_right_inverse)

   146

   147 lemma field_mult_eq_0_iff [simp]:

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

   149 proof cases

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

   151 next

   152   assume anz [simp]: "a\<noteq>0"

   153   { assume "a * b = 0"

   154     hence "inverse a * (a * b) = 0" by simp

   155     hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}

   156   thus ?thesis by force

   157 qed

   158

   159 instance field \<subseteq> idom

   160 by (intro_classes, simp)

   161

   162 class division_by_zero = zero + inverse +

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

   164

   165 subsection {* Distribution rules *}

   166

   167 theorems ring_distrib = right_distrib left_distrib

   168

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

   170 lemma combine_common_factor:

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

   172 by (simp add: left_distrib add_ac)

   173

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

   175 apply (rule equals_zero_I)

   176 apply (simp add: left_distrib [symmetric])

   177 done

   178

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

   180 apply (rule equals_zero_I)

   181 apply (simp add: right_distrib [symmetric])

   182 done

   183

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

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

   186

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

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

   189

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

   191 by (simp add: right_distrib diff_minus

   192               minus_mult_left [symmetric] minus_mult_right [symmetric])

   193

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

   195 by (simp add: left_distrib diff_minus

   196               minus_mult_left [symmetric] minus_mult_right [symmetric])

   197

   198 class mult_mono = times + zero + ord +

   199   assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"

   200   assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"

   201

   202 class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add

   203

   204 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add

   205   + semiring + comm_monoid_add + pordered_ab_semigroup_add

   206   + cancel_ab_semigroup_add

   207

   208 instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..

   209

   210 instance pordered_cancel_semiring \<subseteq> pordered_semiring ..

   211

   212 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +

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

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

   215

   216 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..

   217

   218 instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring

   219 apply intro_classes

   220 apply (cases "a < b & 0 < c")

   221 apply (auto simp add: mult_strict_left_mono order_less_le)

   222 apply (auto simp add: mult_strict_left_mono order_le_less)

   223 apply (simp add: mult_strict_right_mono)

   224 done

   225

   226 class mult_mono1 = times + zero + ord +

   227   assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"

   228

   229 class pordered_comm_semiring = comm_semiring_0

   230   + pordered_ab_semigroup_add + mult_mono1

   231

   232 class pordered_cancel_comm_semiring = comm_semiring_0_cancel

   233   + pordered_ab_semigroup_add + mult_mono1

   234

   235 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..

   236

   237 class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +

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

   239

   240 instance pordered_comm_semiring \<subseteq> pordered_semiring

   241 proof

   242   fix a b c :: 'a

   243   assume A: "a <= b" "0 <= c"

   244   with mult_mono show "c * a <= c * b" .

   245

   246   from mult_commute have "a * c = c * a" ..

   247   also from mult_mono A have "\<dots> <= c * b" .

   248   also from mult_commute have "c * b = b * c" ..

   249   finally show "a * c <= b * c" .

   250 qed

   251

   252 instance pordered_cancel_comm_semiring \<subseteq> pordered_cancel_semiring ..

   253

   254 instance ordered_comm_semiring_strict \<subseteq> ordered_semiring_strict

   255 by (intro_classes, insert mult_strict_mono, simp_all add: mult_commute, blast+)

   256

   257 instance ordered_comm_semiring_strict \<subseteq> pordered_cancel_comm_semiring

   258 apply (intro_classes)

   259 apply (cases "a < b & 0 < c")

   260 apply (auto simp add: mult_strict_left_mono order_less_le)

   261 apply (auto simp add: mult_strict_left_mono order_le_less)

   262 done

   263

   264 class pordered_ring = ring + pordered_cancel_semiring

   265

   266 instance pordered_ring \<subseteq> pordered_ab_group_add ..

   267

   268 class lordered_ring = pordered_ring + lordered_ab_group_abs

   269

   270 instance lordered_ring \<subseteq> lordered_ab_group_meet ..

   271

   272 instance lordered_ring \<subseteq> lordered_ab_group_join ..

   273

   274 class abs_if = minus + ord + zero +

   275   assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"

   276

   277 class ordered_ring_strict = ring + ordered_semiring_strict + abs_if + lordered_ab_group

   278

   279 instance ordered_ring_strict \<subseteq> lordered_ring

   280   by intro_classes (simp add: abs_if sup_eq_if)

   281

   282 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   283

   284 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   285   (*previously ordered_semiring*)

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

   287

   288 class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if + lordered_ab_group

   289   (*previously ordered_ring*)

   290

   291 instance ordered_idom \<subseteq> ordered_ring_strict ..

   292

   293 class ordered_field = field + ordered_idom

   294

   295 lemmas linorder_neqE_ordered_idom =

   296  linorder_neqE[where 'a = "?'b::ordered_idom"]

   297

   298 lemma eq_add_iff1:

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

   300 apply (simp add: diff_minus left_distrib)

   301 apply (simp add: diff_minus left_distrib add_ac)

   302 apply (simp add: compare_rls minus_mult_left [symmetric])

   303 done

   304

   305 lemma eq_add_iff2:

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

   307 apply (simp add: diff_minus left_distrib add_ac)

   308 apply (simp add: compare_rls minus_mult_left [symmetric])

   309 done

   310

   311 lemma less_add_iff1:

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

   313 apply (simp add: diff_minus left_distrib add_ac)

   314 apply (simp add: compare_rls minus_mult_left [symmetric])

   315 done

   316

   317 lemma less_add_iff2:

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

   319 apply (simp add: diff_minus left_distrib add_ac)

   320 apply (simp add: compare_rls minus_mult_left [symmetric])

   321 done

   322

   323 lemma le_add_iff1:

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

   325 apply (simp add: diff_minus left_distrib add_ac)

   326 apply (simp add: compare_rls minus_mult_left [symmetric])

   327 done

   328

   329 lemma le_add_iff2:

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

   331 apply (simp add: diff_minus left_distrib add_ac)

   332 apply (simp add: compare_rls minus_mult_left [symmetric])

   333 done

   334

   335 subsection {* Ordering Rules for Multiplication *}

   336

   337 lemma mult_left_le_imp_le:

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

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

   340

   341 lemma mult_right_le_imp_le:

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

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

   344

   345 lemma mult_left_less_imp_less:

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

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

   348

   349 lemma mult_right_less_imp_less:

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

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

   352

   353 lemma mult_strict_left_mono_neg:

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

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

   356 apply (simp_all add: minus_mult_left [symmetric])

   357 done

   358

   359 lemma mult_left_mono_neg:

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

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

   362 apply (simp_all add: minus_mult_left [symmetric])

   363 done

   364

   365 lemma mult_strict_right_mono_neg:

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

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

   368 apply (simp_all add: minus_mult_right [symmetric])

   369 done

   370

   371 lemma mult_right_mono_neg:

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

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

   374 apply (simp)

   375 apply (simp_all add: minus_mult_right [symmetric])

   376 done

   377

   378 subsection{* Products of Signs *}

   379

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

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

   382

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

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

   385

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

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

   388

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

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

   391

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

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

   394

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

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

   397

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

   399 by (drule mult_strict_right_mono_neg, auto)

   400

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

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

   403

   404 lemma zero_less_mult_pos:

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

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

   407  apply (auto simp add: order_le_less linorder_not_less)

   408 apply (drule_tac mult_pos_neg [of a b])

   409  apply (auto dest: order_less_not_sym)

   410 done

   411

   412 lemma zero_less_mult_pos2:

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

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

   415  apply (auto simp add: order_le_less linorder_not_less)

   416 apply (drule_tac mult_pos_neg2 [of a b])

   417  apply (auto dest: order_less_not_sym)

   418 done

   419

   420 lemma zero_less_mult_iff:

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

   422 apply (auto simp add: order_le_less linorder_not_less mult_pos_pos

   423   mult_neg_neg)

   424 apply (blast dest: zero_less_mult_pos)

   425 apply (blast dest: zero_less_mult_pos2)

   426 done

   427

   428 text{*A field has no "zero divisors", and this theorem holds without the

   429       assumption of an ordering.  See @{text field_mult_eq_0_iff} below.*}

   430 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring_strict)) = (a = 0 | b = 0)"

   431 apply (cases "a < 0")

   432 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)

   433 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+

   434 done

   435

   436 lemma zero_le_mult_iff:

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

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

   439                    zero_less_mult_iff)

   440

   441 lemma mult_less_0_iff:

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

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

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

   445 done

   446

   447 lemma mult_le_0_iff:

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

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

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

   451 done

   452

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

   454 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   455

   456 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)"

   457 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   458

   459 lemma zero_le_square: "(0::'a::ordered_ring_strict) \<le> a*a"

   460 by (simp add: zero_le_mult_iff linorder_linear)

   461

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

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

   464

   465 instance ordered_idom \<subseteq> ordered_semidom

   466 proof

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

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

   469 qed

   470

   471 instance ordered_ring_strict \<subseteq> no_zero_divisors

   472 by (intro_classes, simp)

   473

   474 instance ordered_idom \<subseteq> idom ..

   475

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

   477

   478 lemmas one_neq_zero = zero_neq_one [THEN not_sym]

   479 declare one_neq_zero [simp]

   480

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

   482   by (rule zero_less_one [THEN order_less_imp_le])

   483

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

   485 by (simp add: linorder_not_le)

   486

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

   488 by (simp add: linorder_not_less)

   489

   490 subsection{*More Monotonicity*}

   491

   492 text{*Strict monotonicity in both arguments*}

   493 lemma mult_strict_mono:

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

   495 apply (cases "c=0")

   496  apply (simp add: mult_pos_pos)

   497 apply (erule mult_strict_right_mono [THEN order_less_trans])

   498  apply (force simp add: order_le_less)

   499 apply (erule mult_strict_left_mono, assumption)

   500 done

   501

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

   503 lemma mult_strict_mono':

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

   505 apply (rule mult_strict_mono)

   506 apply (blast intro: order_le_less_trans)+

   507 done

   508

   509 lemma mult_mono:

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

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

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

   513 apply (erule mult_left_mono, assumption)

   514 done

   515

   516 lemma mult_mono':

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

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

   519 apply (rule mult_mono)

   520 apply (fast intro: order_trans)+

   521 done

   522

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

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

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

   526 done

   527

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

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

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

   531   apply (erule order_less_le_trans)

   532   apply (erule mult_left_mono)

   533   apply simp

   534   apply (erule mult_strict_right_mono)

   535   apply assumption

   536 done

   537

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

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

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

   541   apply (erule order_le_less_trans)

   542   apply (erule mult_strict_left_mono)

   543   apply simp

   544   apply (erule mult_right_mono)

   545   apply simp

   546 done

   547

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

   549

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

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

   552

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

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

   555

   556 lemma mult_less_cancel_right_disj:

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

   558 apply (cases "c = 0")

   559 apply (auto simp add: linorder_neq_iff mult_strict_right_mono

   560                       mult_strict_right_mono_neg)

   561 apply (auto simp add: linorder_not_less

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

   563                       linorder_not_le [symmetric, of a])

   564 apply (erule_tac [!] notE)

   565 apply (auto simp add: order_less_imp_le mult_right_mono

   566                       mult_right_mono_neg)

   567 done

   568

   569 lemma mult_less_cancel_left_disj:

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

   571 apply (cases "c = 0")

   572 apply (auto simp add: linorder_neq_iff mult_strict_left_mono

   573                       mult_strict_left_mono_neg)

   574 apply (auto simp add: linorder_not_less

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

   576                       linorder_not_le [symmetric, of a])

   577 apply (erule_tac [!] notE)

   578 apply (auto simp add: order_less_imp_le mult_left_mono

   579                       mult_left_mono_neg)

   580 done

   581

   582

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

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

   585

   586 lemma mult_less_cancel_right:

   587   fixes c :: "'a :: ordered_ring_strict"

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

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

   590

   591 lemma mult_less_cancel_left:

   592   fixes c :: "'a :: ordered_ring_strict"

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

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

   595

   596 lemma mult_le_cancel_right:

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

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

   599

   600 lemma mult_le_cancel_left:

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

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

   603

   604 lemma mult_less_imp_less_left:

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

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

   607 proof (rule ccontr)

   608   assume "~ a < b"

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

   610   hence "c*b \<le> c*a" by (rule mult_left_mono)

   611   with this and less show False

   612     by (simp add: linorder_not_less [symmetric])

   613 qed

   614

   615 lemma mult_less_imp_less_right:

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

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

   618 proof (rule ccontr)

   619   assume "~ a < b"

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

   621   hence "b*c \<le> a*c" by (rule mult_right_mono)

   622   with this and less show False

   623     by (simp add: linorder_not_less [symmetric])

   624 qed

   625

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

   627 lemma mult_cancel_right [simp]:

   628      "(a*c = b*c) = (c = (0::'a::ordered_ring_strict) | a=b)"

   629 apply (cut_tac linorder_less_linear [of 0 c])

   630 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono

   631              simp add: linorder_neq_iff)

   632 done

   633

   634 text{*These cancellation theorems require an ordering. Versions are proved

   635       below that work for fields without an ordering.*}

   636 lemma mult_cancel_left [simp]:

   637      "(c*a = c*b) = (c = (0::'a::ordered_ring_strict) | a=b)"

   638 apply (cut_tac linorder_less_linear [of 0 c])

   639 apply (force dest: mult_strict_left_mono_neg mult_strict_left_mono

   640              simp add: linorder_neq_iff)

   641 done

   642

   643

   644 subsubsection{*Special Cancellation Simprules for Multiplication*}

   645

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

   647

   648 lemma mult_le_cancel_right1:

   649   fixes c :: "'a :: ordered_idom"

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

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

   652

   653 lemma mult_le_cancel_right2:

   654   fixes c :: "'a :: ordered_idom"

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

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

   657

   658 lemma mult_le_cancel_left1:

   659   fixes c :: "'a :: ordered_idom"

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

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

   662

   663 lemma mult_le_cancel_left2:

   664   fixes c :: "'a :: ordered_idom"

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

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

   667

   668 lemma mult_less_cancel_right1:

   669   fixes c :: "'a :: ordered_idom"

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

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

   672

   673 lemma mult_less_cancel_right2:

   674   fixes c :: "'a :: ordered_idom"

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

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

   677

   678 lemma mult_less_cancel_left1:

   679   fixes c :: "'a :: ordered_idom"

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

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

   682

   683 lemma mult_less_cancel_left2:

   684   fixes c :: "'a :: ordered_idom"

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

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

   687

   688 lemma mult_cancel_right1 [simp]:

   689 fixes c :: "'a :: ordered_idom"

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

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

   692

   693 lemma mult_cancel_right2 [simp]:

   694 fixes c :: "'a :: ordered_idom"

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

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

   697

   698 lemma mult_cancel_left1 [simp]:

   699 fixes c :: "'a :: ordered_idom"

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

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

   702

   703 lemma mult_cancel_left2 [simp]:

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

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

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

   707

   708

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

   710 lemmas mult_compare_simps =

   711     mult_le_cancel_right mult_le_cancel_left

   712     mult_le_cancel_right1 mult_le_cancel_right2

   713     mult_le_cancel_left1 mult_le_cancel_left2

   714     mult_less_cancel_right mult_less_cancel_left

   715     mult_less_cancel_right1 mult_less_cancel_right2

   716     mult_less_cancel_left1 mult_less_cancel_left2

   717     mult_cancel_right mult_cancel_left

   718     mult_cancel_right1 mult_cancel_right2

   719     mult_cancel_left1 mult_cancel_left2

   720

   721

   722 text{*This list of rewrites decides ring equalities by ordered rewriting.*}

   723 lemmas ring_eq_simps =

   724 (*  mult_ac*)

   725   left_distrib right_distrib left_diff_distrib right_diff_distrib

   726   group_eq_simps

   727 (*  add_ac

   728   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   729   diff_eq_eq eq_diff_eq *)

   730

   731 subsection {* Fields *}

   732

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

   734 proof

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

   736   {

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

   738     also assume "a / b = 1"

   739     finally show "a = b" by simp

   740   next

   741     assume "a = b"

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

   743   }

   744 qed

   745

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

   747 by (simp add: divide_inverse)

   748

   749 lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"

   750   by (simp add: divide_inverse)

   751

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

   753 by (simp add: divide_inverse)

   754

   755 lemma divide_self_if [simp]:

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

   757   by (simp add: divide_self)

   758

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

   760 by (simp add: divide_inverse)

   761

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

   763 by (simp add: divide_inverse)

   764

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

   766 by (simp add: divide_inverse left_distrib)

   767

   768

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

   770       of an ordering.*}

   771 lemma field_mult_eq_0_iff [simp]:

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

   773 proof cases

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

   775 next

   776   assume anz [simp]: "a\<noteq>0"

   777   { assume "a * b = 0"

   778     hence "inverse a * (a * b) = 0" by simp

   779     hence "b = 0"  by (simp (no_asm_use) add: mult_assoc [symmetric])}

   780   thus ?thesis by force

   781 qed

   782

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

   784 lemma field_mult_cancel_right_lemma:

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

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

   787         shows "a=b"

   788 proof -

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

   790     by (simp add: eq)

   791   thus "a=b"

   792     by (simp add: mult_assoc cnz)

   793 qed

   794

   795 lemma field_mult_cancel_right [simp]:

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

   797 proof -

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

   799     by simp

   800   also have "\<dots> = ((a - b)*c = 0)"

   801      by (simp only: left_diff_distrib)

   802   also have "\<dots> = (c = 0 \<or> a = b)"

   803      by (simp add: disj_commute)

   804   finally show ?thesis .

   805 qed

   806

   807 lemma field_mult_cancel_left [simp]:

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

   809 proof -

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

   811     by simp

   812   also have "\<dots> = (c*(a - b) = 0)"

   813      by (simp only: right_diff_distrib)

   814   also have "\<dots> = (c = 0 \<or> a = b)"

   815      by simp

   816   finally show ?thesis .

   817 qed

   818

   819 lemma nonzero_imp_inverse_nonzero:

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

   821 proof

   822   assume ianz: "inverse a = 0"

   823   assume "a \<noteq> 0"

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

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

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

   827   thus False by (simp add: eq_commute)

   828 qed

   829

   830

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

   832

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

   834 apply (rule ccontr)

   835 apply (blast dest: nonzero_imp_inverse_nonzero)

   836 done

   837

   838 lemma inverse_nonzero_imp_nonzero:

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

   840 apply (rule ccontr)

   841 apply (blast dest: nonzero_imp_inverse_nonzero)

   842 done

   843

   844 lemma inverse_nonzero_iff_nonzero [simp]:

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

   846 by (force dest: inverse_nonzero_imp_nonzero)

   847

   848 lemma nonzero_inverse_minus_eq:

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

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

   851 proof -

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

   853     by simp

   854   thus ?thesis

   855     by (simp only: field_mult_cancel_left, simp)

   856 qed

   857

   858 lemma inverse_minus_eq [simp]:

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

   860 proof cases

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

   862 next

   863   assume "a\<noteq>0"

   864   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   865 qed

   866

   867 lemma nonzero_inverse_eq_imp_eq:

   868       assumes inveq: "inverse a = inverse b"

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

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

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

   872 proof -

   873   have "a * inverse b = a * inverse a"

   874     by (simp add: inveq)

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

   876     by simp

   877   thus "a = b"

   878     by (simp add: mult_assoc anz bnz)

   879 qed

   880

   881 lemma inverse_eq_imp_eq:

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

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

   884  apply (force dest!: inverse_zero_imp_zero

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

   886 apply (force dest!: nonzero_inverse_eq_imp_eq)

   887 done

   888

   889 lemma inverse_eq_iff_eq [simp]:

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

   891 by (force dest!: inverse_eq_imp_eq)

   892

   893 lemma nonzero_inverse_inverse_eq:

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

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

   896   proof -

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

   898     by (simp add: nonzero_imp_inverse_nonzero)

   899   thus ?thesis

   900     by (simp add: mult_assoc)

   901   qed

   902

   903 lemma inverse_inverse_eq [simp]:

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

   905   proof cases

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

   907   next

   908     assume "a\<noteq>0"

   909     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

   910   qed

   911

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

   913   proof -

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

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

   916   thus ?thesis  by simp

   917   qed

   918

   919 lemma inverse_unique:

   920   assumes ab: "a*b = 1"

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

   922 proof -

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

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

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

   926 qed

   927

   928 lemma nonzero_inverse_mult_distrib:

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

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

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

   932   proof -

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

   934     by (simp add: field_mult_eq_0_iff anz bnz)

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

   936     by (simp add: mult_assoc bnz)

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

   938     by simp

   939   thus ?thesis

   940     by (simp add: mult_assoc anz)

   941   qed

   942

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

   944       the right-hand side.*}

   945 lemma inverse_mult_distrib [simp]:

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

   947   proof cases

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

   949     thus ?thesis  by (simp add: nonzero_inverse_mult_distrib mult_commute)

   950   next

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

   952     thus ?thesis  by force

   953   qed

   954

   955 lemma division_ring_inverse_add:

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

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

   958 by (simp add: right_distrib left_distrib mult_assoc)

   959

   960 lemma division_ring_inverse_diff:

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

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

   963 by (simp add: right_diff_distrib left_diff_distrib mult_assoc)

   964

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

   966 lemma inverse_add:

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

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

   969 by (simp add: division_ring_inverse_add mult_ac)

   970

   971 lemma inverse_divide [simp]:

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

   973   by (simp add: divide_inverse mult_commute)

   974

   975 subsection {* Calculations with fractions *}

   976

   977 lemma nonzero_mult_divide_cancel_left:

   978   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0"

   979     shows "(c*a)/(c*b) = a/(b::'a::field)"

   980 proof -

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

   982     by (simp add: field_mult_eq_0_iff divide_inverse

   983                   nonzero_inverse_mult_distrib)

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

   985     by (simp only: mult_ac)

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

   987     by simp

   988     finally show ?thesis

   989     by (simp add: divide_inverse)

   990 qed

   991

   992 lemma mult_divide_cancel_left:

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

   994 apply (cases "b = 0")

   995 apply (simp_all add: nonzero_mult_divide_cancel_left)

   996 done

   997

   998 lemma nonzero_mult_divide_cancel_right:

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

  1000 by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left)

  1001

  1002 lemma mult_divide_cancel_right:

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

  1004 apply (cases "b = 0")

  1005 apply (simp_all add: nonzero_mult_divide_cancel_right)

  1006 done

  1007

  1008 (*For ExtractCommonTerm*)

  1009 lemma mult_divide_cancel_eq_if:

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

  1011       (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"

  1012   by (simp add: mult_divide_cancel_left)

  1013

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

  1015   by (simp add: divide_inverse)

  1016

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

  1018 by (simp add: divide_inverse mult_assoc)

  1019

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

  1021 by (simp add: divide_inverse mult_ac)

  1022

  1023 lemma divide_divide_eq_right [simp]:

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

  1025 by (simp add: divide_inverse mult_ac)

  1026

  1027 lemma divide_divide_eq_left [simp]:

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

  1029 by (simp add: divide_inverse mult_assoc)

  1030

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

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

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

  1034   apply (erule ssubst)

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

  1036   apply (erule ssubst)

  1037   apply (rule add_divide_distrib [THEN sym])

  1038   apply (subst mult_commute)

  1039   apply (erule nonzero_mult_divide_cancel_left [THEN sym])

  1040   apply assumption

  1041   apply (erule nonzero_mult_divide_cancel_right [THEN sym])

  1042   apply assumption

  1043 done

  1044

  1045 subsubsection{*Special Cancellation Simprules for Division*}

  1046

  1047 lemma mult_divide_cancel_left_if [simp]:

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

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

  1050 by (simp add: mult_divide_cancel_left)

  1051

  1052 lemma mult_divide_cancel_right_if [simp]:

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

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

  1055 by (simp add: mult_divide_cancel_right)

  1056

  1057 lemma mult_divide_cancel_left_if1 [simp]:

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

  1059   shows "c / (c*b) = (if c=0 then 0 else 1/b)"

  1060 apply (insert mult_divide_cancel_left_if [of c 1 b])

  1061 apply (simp del: mult_divide_cancel_left_if)

  1062 done

  1063

  1064 lemma mult_divide_cancel_left_if2 [simp]:

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

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

  1067 apply (insert mult_divide_cancel_left_if [of c a 1])

  1068 apply (simp del: mult_divide_cancel_left_if)

  1069 done

  1070

  1071 lemma mult_divide_cancel_right_if1 [simp]:

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

  1073   shows "c / (b*c) = (if c=0 then 0 else 1/b)"

  1074 apply (insert mult_divide_cancel_right_if [of 1 c b])

  1075 apply (simp del: mult_divide_cancel_right_if)

  1076 done

  1077

  1078 lemma mult_divide_cancel_right_if2 [simp]:

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

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

  1081 apply (insert mult_divide_cancel_right_if [of a c 1])

  1082 apply (simp del: mult_divide_cancel_right_if)

  1083 done

  1084

  1085 text{*Two lemmas for cancelling the denominator*}

  1086

  1087 lemma times_divide_self_right [simp]:

  1088   fixes a :: "'a :: {field,division_by_zero}"

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

  1090 by (simp add: times_divide_eq_right)

  1091

  1092 lemma times_divide_self_left [simp]:

  1093   fixes a :: "'a :: {field,division_by_zero}"

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

  1095 by (simp add: times_divide_eq_left)

  1096

  1097

  1098 subsection {* Division and Unary Minus *}

  1099

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

  1101 by (simp add: divide_inverse minus_mult_left)

  1102

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

  1104 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1105

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

  1107 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1108

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

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

  1111

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

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

  1114

  1115

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

  1117 lemmas divide_minus_left = minus_divide_left [symmetric]

  1118 lemmas divide_minus_right = minus_divide_right [symmetric]

  1119 declare divide_minus_left [simp]   divide_minus_right [simp]

  1120

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

  1122 lemmas mult_minus_left = minus_mult_left [symmetric]

  1123 lemmas mult_minus_right = minus_mult_right [symmetric]

  1124 declare mult_minus_left [simp]   mult_minus_right [simp]

  1125

  1126 lemma minus_divide_divide [simp]:

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

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

  1129 apply (simp add: nonzero_minus_divide_divide)

  1130 done

  1131

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

  1133 by (simp add: diff_minus add_divide_distrib)

  1134

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

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

  1137   apply (subst diff_def)+

  1138   apply (subst minus_divide_left)

  1139   apply (subst add_frac_eq)

  1140   apply simp_all

  1141 done

  1142

  1143 subsection {* Ordered Fields *}

  1144

  1145 lemma positive_imp_inverse_positive:

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

  1147   proof -

  1148   have "0 < a * inverse a"

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

  1150   thus "0 < inverse a"

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

  1152   qed

  1153

  1154 lemma negative_imp_inverse_negative:

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

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

  1157       simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1158

  1159 lemma inverse_le_imp_le:

  1160       assumes invle: "inverse a \<le> inverse b"

  1161 	  and apos:  "0 < a"

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

  1163   proof (rule classical)

  1164   assume "~ b \<le> a"

  1165   hence "a < b"

  1166     by (simp add: linorder_not_le)

  1167   hence bpos: "0 < b"

  1168     by (blast intro: apos order_less_trans)

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

  1170     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1172     by (simp add: bpos order_less_imp_le mult_right_mono)

  1173   thus "b \<le> a"

  1174     by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)

  1175   qed

  1176

  1177 lemma inverse_positive_imp_positive:

  1178       assumes inv_gt_0: "0 < inverse a"

  1179           and [simp]:   "a \<noteq> 0"

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

  1181   proof -

  1182   have "0 < inverse (inverse a)"

  1183     by (rule positive_imp_inverse_positive)

  1184   thus "0 < a"

  1185     by (simp add: nonzero_inverse_inverse_eq)

  1186   qed

  1187

  1188 lemma inverse_positive_iff_positive [simp]:

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

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

  1191 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1192 done

  1193

  1194 lemma inverse_negative_imp_negative:

  1195       assumes inv_less_0: "inverse a < 0"

  1196           and [simp]:   "a \<noteq> 0"

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

  1198   proof -

  1199   have "inverse (inverse a) < 0"

  1200     by (rule negative_imp_inverse_negative)

  1201   thus "a < 0"

  1202     by (simp add: nonzero_inverse_inverse_eq)

  1203   qed

  1204

  1205 lemma inverse_negative_iff_negative [simp]:

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

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

  1208 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1209 done

  1210

  1211 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1213 by (simp add: linorder_not_less [symmetric])

  1214

  1215 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1217 by (simp add: linorder_not_less [symmetric])

  1218

  1219

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

  1221

  1222 lemma less_imp_inverse_less:

  1223       assumes less: "a < b"

  1224 	  and apos:  "0 < a"

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

  1226   proof (rule ccontr)

  1227   assume "~ inverse b < inverse a"

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

  1229     by (simp add: linorder_not_less)

  1230   hence "~ (a < b)"

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

  1232   thus False

  1233     by (rule notE [OF _ less])

  1234   qed

  1235

  1236 lemma inverse_less_imp_less:

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

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

  1239 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1240 done

  1241

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

  1243 lemma inverse_less_iff_less [simp]:

  1244      "[|0 < a; 0 < b|]

  1245       ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

  1246 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1247

  1248 lemma le_imp_inverse_le:

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

  1250   by (force simp add: order_le_less less_imp_inverse_less)

  1251

  1252 lemma inverse_le_iff_le [simp]:

  1253      "[|0 < a; 0 < b|]

  1254       ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1255 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1256

  1257

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

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

  1260 lemma inverse_le_imp_le_neg:

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

  1262   apply (rule classical)

  1263   apply (subgoal_tac "a < 0")

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

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

  1266   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1267   done

  1268

  1269 lemma less_imp_inverse_less_neg:

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

  1271   apply (subgoal_tac "a < 0")

  1272    prefer 2 apply (blast intro: order_less_trans)

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

  1274   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1275   done

  1276

  1277 lemma inverse_less_imp_less_neg:

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

  1279   apply (rule classical)

  1280   apply (subgoal_tac "a < 0")

  1281    prefer 2

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

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

  1284   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1285   done

  1286

  1287 lemma inverse_less_iff_less_neg [simp]:

  1288      "[|a < 0; b < 0|]

  1289       ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"

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

  1291   apply (simp del: inverse_less_iff_less

  1292 	      add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1293   done

  1294

  1295 lemma le_imp_inverse_le_neg:

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

  1297   by (force simp add: order_le_less less_imp_inverse_less_neg)

  1298

  1299 lemma inverse_le_iff_le_neg [simp]:

  1300      "[|a < 0; b < 0|]

  1301       ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"

  1302 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1303

  1304

  1305 subsection{*Inverses and the Number One*}

  1306

  1307 lemma one_less_inverse_iff:

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

  1309   assume "0 < x"

  1310     with inverse_less_iff_less [OF zero_less_one, of x]

  1311     show ?thesis by simp

  1312 next

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

  1314   have "~ (1 < inverse x)"

  1315   proof

  1316     assume "1 < inverse x"

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

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

  1319     finally show False by auto

  1320   qed

  1321   with notless show ?thesis by simp

  1322 qed

  1323

  1324 lemma inverse_eq_1_iff [simp]:

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

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

  1327

  1328 lemma one_le_inverse_iff:

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

  1330 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1331                     eq_commute [of 1])

  1332

  1333 lemma inverse_less_1_iff:

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

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

  1336

  1337 lemma inverse_le_1_iff:

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

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

  1340

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

  1342

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

  1344 proof -

  1345   assume less: "0<c"

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

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

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

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

  1350   finally show ?thesis .

  1351 qed

  1352

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

  1354 proof -

  1355   assume less: "c<0"

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

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

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

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

  1360   finally show ?thesis .

  1361 qed

  1362

  1363 lemma le_divide_eq:

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

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

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

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

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

  1369 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1370 done

  1371

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

  1373 proof -

  1374   assume less: "0<c"

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

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

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

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

  1379   finally show ?thesis .

  1380 qed

  1381

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

  1383 proof -

  1384   assume less: "c<0"

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

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

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

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

  1389   finally show ?thesis .

  1390 qed

  1391

  1392 lemma divide_le_eq:

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

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

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

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

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

  1398 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1399 done

  1400

  1401 lemma pos_less_divide_eq:

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

  1403 proof -

  1404   assume less: "0<c"

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

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

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

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

  1409   finally show ?thesis .

  1410 qed

  1411

  1412 lemma neg_less_divide_eq:

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

  1414 proof -

  1415   assume less: "c<0"

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

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

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

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

  1420   finally show ?thesis .

  1421 qed

  1422

  1423 lemma less_divide_eq:

  1424   "(a < b/c) =

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

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

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

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

  1429 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1430 done

  1431

  1432 lemma pos_divide_less_eq:

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

  1434 proof -

  1435   assume less: "0<c"

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

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

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

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

  1440   finally show ?thesis .

  1441 qed

  1442

  1443 lemma neg_divide_less_eq:

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

  1445 proof -

  1446   assume less: "c<0"

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

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

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

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

  1451   finally show ?thesis .

  1452 qed

  1453

  1454 lemma divide_less_eq:

  1455   "(b/c < a) =

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

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

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

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

  1460 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1461 done

  1462

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

  1464 proof -

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

  1466   have "(a = b/c) = (a*c = (b/c)*c)"

  1467     by (simp add: field_mult_cancel_right)

  1468   also have "... = (a*c = b)"

  1469     by (simp add: divide_inverse mult_assoc)

  1470   finally show ?thesis .

  1471 qed

  1472

  1473 lemma eq_divide_eq:

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

  1475 by (simp add: nonzero_eq_divide_eq)

  1476

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

  1478 proof -

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

  1480   have "(b/c = a) = ((b/c)*c = a*c)"

  1481     by (simp add: field_mult_cancel_right)

  1482   also have "... = (b = a*c)"

  1483     by (simp add: divide_inverse mult_assoc)

  1484   finally show ?thesis .

  1485 qed

  1486

  1487 lemma divide_eq_eq:

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

  1489 by (force simp add: nonzero_divide_eq_eq)

  1490

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

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

  1493   by (subst divide_eq_eq, simp)

  1494

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

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

  1497   by (subst eq_divide_eq, simp)

  1498

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

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

  1501   apply (subst nonzero_eq_divide_eq)

  1502   apply assumption

  1503   apply (subst times_divide_eq_left)

  1504   apply (erule nonzero_divide_eq_eq)

  1505 done

  1506

  1507 subsection{*Division and Signs*}

  1508

  1509 lemma zero_less_divide_iff:

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

  1511 by (simp add: divide_inverse zero_less_mult_iff)

  1512

  1513 lemma divide_less_0_iff:

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

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

  1516 by (simp add: divide_inverse mult_less_0_iff)

  1517

  1518 lemma zero_le_divide_iff:

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

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

  1521 by (simp add: divide_inverse zero_le_mult_iff)

  1522

  1523 lemma divide_le_0_iff:

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

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

  1526 by (simp add: divide_inverse mult_le_0_iff)

  1527

  1528 lemma divide_eq_0_iff [simp]:

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

  1530 by (simp add: divide_inverse field_mult_eq_0_iff)

  1531

  1532 lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==>

  1533     0 < y ==> 0 < x / y"

  1534   apply (subst pos_less_divide_eq)

  1535   apply assumption

  1536   apply simp

  1537 done

  1538

  1539 lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==>

  1540     0 <= x / y"

  1541   apply (subst pos_le_divide_eq)

  1542   apply assumption

  1543   apply simp

  1544 done

  1545

  1546 lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"

  1547   apply (subst pos_divide_less_eq)

  1548   apply assumption

  1549   apply simp

  1550 done

  1551

  1552 lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==>

  1553     0 < y ==> x / y <= 0"

  1554   apply (subst pos_divide_le_eq)

  1555   apply assumption

  1556   apply simp

  1557 done

  1558

  1559 lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"

  1560   apply (subst neg_divide_less_eq)

  1561   apply assumption

  1562   apply simp

  1563 done

  1564

  1565 lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==>

  1566     y < 0 ==> x / y <= 0"

  1567   apply (subst neg_divide_le_eq)

  1568   apply assumption

  1569   apply simp

  1570 done

  1571

  1572 lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"

  1573   apply (subst neg_less_divide_eq)

  1574   apply assumption

  1575   apply simp

  1576 done

  1577

  1578 lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==>

  1579     0 <= x / y"

  1580   apply (subst neg_le_divide_eq)

  1581   apply assumption

  1582   apply simp

  1583 done

  1584

  1585 subsection{*Cancellation Laws for Division*}

  1586

  1587 lemma divide_cancel_right [simp]:

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

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

  1590 apply (simp add: divide_inverse field_mult_cancel_right)

  1591 done

  1592

  1593 lemma divide_cancel_left [simp]:

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

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

  1596 apply (simp add: divide_inverse field_mult_cancel_left)

  1597 done

  1598

  1599 subsection {* Division and the Number One *}

  1600

  1601 text{*Simplify expressions equated with 1*}

  1602 lemma divide_eq_1_iff [simp]:

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

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

  1605 apply (simp add: right_inverse_eq)

  1606 done

  1607

  1608 lemma one_eq_divide_iff [simp]:

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

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

  1611

  1612 lemma zero_eq_1_divide_iff [simp]:

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

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

  1615 apply (auto simp add: nonzero_eq_divide_eq)

  1616 done

  1617

  1618 lemma one_divide_eq_0_iff [simp]:

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

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

  1621 apply (insert zero_neq_one [THEN not_sym])

  1622 apply (auto simp add: nonzero_divide_eq_eq)

  1623 done

  1624

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

  1626 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1627 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1628 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1629 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1630

  1631 declare zero_less_divide_1_iff [simp]

  1632 declare divide_less_0_1_iff [simp]

  1633 declare zero_le_divide_1_iff [simp]

  1634 declare divide_le_0_1_iff [simp]

  1635

  1636 subsection {* Ordering Rules for Division *}

  1637

  1638 lemma divide_strict_right_mono:

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

  1640 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1641               positive_imp_inverse_positive)

  1642

  1643 lemma divide_right_mono:

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

  1645   by (force simp add: divide_strict_right_mono order_le_less)

  1646

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

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

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

  1650   apply auto

  1651 done

  1652

  1653 lemma divide_strict_right_mono_neg:

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

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

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

  1657 done

  1658

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

  1660       have the same sign*}

  1661 lemma divide_strict_left_mono:

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

  1663 by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono

  1664       order_less_imp_not_eq order_less_imp_not_eq2

  1665       less_imp_inverse_less less_imp_inverse_less_neg)

  1666

  1667 lemma divide_left_mono:

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

  1669   apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")

  1670    prefer 2

  1671    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)

  1672   apply (cases "c=0", simp add: divide_inverse)

  1673   apply (force simp add: divide_strict_left_mono order_le_less)

  1674   done

  1675

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

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

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

  1679   apply (auto simp add: mult_commute)

  1680 done

  1681

  1682 lemma divide_strict_left_mono_neg:

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

  1684   apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")

  1685    prefer 2

  1686    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)

  1687   apply (drule divide_strict_left_mono [of _ _ "-c"])

  1688    apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric])

  1689   done

  1690

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

  1692

  1693 lemma le_divide_eq_1:

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

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

  1696 by (auto simp add: le_divide_eq)

  1697

  1698 lemma divide_le_eq_1:

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

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

  1701 by (auto simp add: divide_le_eq)

  1702

  1703 lemma less_divide_eq_1:

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

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

  1706 by (auto simp add: less_divide_eq)

  1707

  1708 lemma divide_less_eq_1:

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

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

  1711 by (auto simp add: divide_less_eq)

  1712

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

  1714

  1715 lemma le_divide_eq_1_pos [simp]:

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

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

  1718 by (auto simp add: le_divide_eq)

  1719

  1720 lemma le_divide_eq_1_neg [simp]:

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

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

  1723 by (auto simp add: le_divide_eq)

  1724

  1725 lemma divide_le_eq_1_pos [simp]:

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

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

  1728 by (auto simp add: divide_le_eq)

  1729

  1730 lemma divide_le_eq_1_neg [simp]:

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

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

  1733 by (auto simp add: divide_le_eq)

  1734

  1735 lemma less_divide_eq_1_pos [simp]:

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

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

  1738 by (auto simp add: less_divide_eq)

  1739

  1740 lemma less_divide_eq_1_neg [simp]:

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

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

  1743 by (auto simp add: less_divide_eq)

  1744

  1745 lemma divide_less_eq_1_pos [simp]:

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

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

  1748 by (auto simp add: divide_less_eq)

  1749

  1750 lemma divide_less_eq_1_neg [simp]:

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

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

  1753 by (auto simp add: divide_less_eq)

  1754

  1755 lemma eq_divide_eq_1 [simp]:

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

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

  1758 by (auto simp add: eq_divide_eq)

  1759

  1760 lemma divide_eq_eq_1 [simp]:

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

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

  1763 by (auto simp add: divide_eq_eq)

  1764

  1765 subsection {* Reasoning about inequalities with division *}

  1766

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

  1768     ==> x * y <= x"

  1769   by (auto simp add: mult_compare_simps);

  1770

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

  1772     ==> y * x <= x"

  1773   by (auto simp add: mult_compare_simps);

  1774

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

  1776     x / y <= z";

  1777   by (subst pos_divide_le_eq, assumption+);

  1778

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

  1780     z <= x / y";

  1781   by (subst pos_le_divide_eq, assumption+)

  1782

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

  1784     x / y < z"

  1785   by (subst pos_divide_less_eq, assumption+)

  1786

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

  1788     z < x / y"

  1789   by (subst pos_less_divide_eq, assumption+)

  1790

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

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

  1793   apply (rule mult_imp_div_pos_le)

  1794   apply simp;

  1795   apply (subst times_divide_eq_left);

  1796   apply (rule mult_imp_le_div_pos, assumption)

  1797   apply (rule mult_mono)

  1798   apply simp_all

  1799 done

  1800

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

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

  1803   apply (rule mult_imp_div_pos_less)

  1804   apply simp;

  1805   apply (subst times_divide_eq_left);

  1806   apply (rule mult_imp_less_div_pos, assumption)

  1807   apply (erule mult_less_le_imp_less)

  1808   apply simp_all

  1809 done

  1810

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

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

  1813   apply (rule mult_imp_div_pos_less)

  1814   apply simp_all

  1815   apply (subst times_divide_eq_left);

  1816   apply (rule mult_imp_less_div_pos, assumption)

  1817   apply (erule mult_le_less_imp_less)

  1818   apply simp_all

  1819 done

  1820

  1821 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1822

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

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

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

  1826   seem to need them.*}

  1827

  1828 declare times_divide_eq [simp]

  1829

  1830 subsection {* Ordered Fields are Dense *}

  1831

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

  1833 proof -

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

  1835     by (blast intro: zero_less_one add_strict_left_mono)

  1836   thus ?thesis by simp

  1837 qed

  1838

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

  1840   by (blast intro: order_less_trans zero_less_one less_add_one)

  1841

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

  1843 by (simp add: zero_less_two pos_less_divide_eq right_distrib)

  1844

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

  1846 by (simp add: zero_less_two pos_divide_less_eq right_distrib)

  1847

  1848 lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"

  1849 by (blast intro!: less_half_sum gt_half_sum)

  1850

  1851

  1852 subsection {* Absolute Value *}

  1853

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

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

  1856

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

  1858 proof -

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

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

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

  1862     by (simp only: abs_prts[of a] abs_prts[of b] ring_eq_simps)

  1863   {

  1864     fix u v :: 'a

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

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

  1867                       nprt a * pprt b + nprt a * nprt b"

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

  1869       apply (simp add: left_distrib right_distrib add_ac)

  1870       done

  1871   }

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

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

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

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

  1876     apply (simp)

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

  1878     apply (rule addm2)

  1879     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1880     apply (rule addm)

  1881     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1882     done

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

  1884     apply (simp add:diff_def)

  1885     apply (rule_tac y=0 in order_trans)

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

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

  1888     done

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

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

  1891   show ?thesis

  1892     apply (rule abs_leI)

  1893     apply (simp add: i1)

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

  1895     done

  1896 qed

  1897

  1898 lemma abs_eq_mult:

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

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

  1901 proof -

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

  1903     apply (auto)

  1904     apply (rule_tac split_mult_pos_le)

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

  1906     apply (simp)

  1907     apply (rule_tac split_mult_neg_le)

  1908     apply (insert prems)

  1909     apply (blast)

  1910     done

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

  1912     by (simp add: prts[symmetric])

  1913   show ?thesis

  1914   proof cases

  1915     assume "0 <= a * b"

  1916     then show ?thesis

  1917       apply (simp_all add: mulprts abs_prts)

  1918       apply (insert prems)

  1919       apply (auto simp add:

  1920 	ring_eq_simps

  1921 	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]

  1922 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])

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

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

  1925       done

  1926   next

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

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

  1929     then show ?thesis

  1930       apply (simp_all add: mulprts abs_prts)

  1931       apply (insert prems)

  1932       apply (auto simp add: ring_eq_simps)

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

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

  1935       done

  1936   qed

  1937 qed

  1938

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

  1940 by (simp add: abs_eq_mult linorder_linear)

  1941

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

  1943 by (simp add: abs_if)

  1944

  1945 lemma nonzero_abs_inverse:

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

  1947 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  1948                       negative_imp_inverse_negative)

  1949 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  1950 done

  1951

  1952 lemma abs_inverse [simp]:

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

  1954       inverse (abs a)"

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

  1956 apply (simp add: nonzero_abs_inverse)

  1957 done

  1958

  1959 lemma nonzero_abs_divide:

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

  1961 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  1962

  1963 lemma abs_divide [simp]:

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

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

  1966 apply (simp add: nonzero_abs_divide)

  1967 done

  1968

  1969 lemma abs_mult_less:

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

  1971 proof -

  1972   assume ac: "abs a < c"

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

  1974   assume "abs b < d"

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

  1976 qed

  1977

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

  1979 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)

  1980

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

  1982 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)

  1983

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

  1985 apply (simp add: order_less_le abs_le_iff)

  1986 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)

  1987 apply (simp add: le_minus_self_iff linorder_neq_iff)

  1988 done

  1989

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

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

  1992   apply (subst abs_mult);

  1993   apply simp;

  1994 done;

  1995

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

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

  1998   apply (subst abs_divide);

  1999   apply (simp add: order_less_imp_le);

  2000 done;

  2001

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

  2003

  2004 lemma mult_le_prts:

  2005   assumes

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

  2007   "a <= a2"

  2008   "b1 <= b"

  2009   "b <= b2"

  2010   shows

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

  2012 proof -

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

  2014     apply (subst prts[symmetric])+

  2015     apply simp

  2016     done

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

  2018     by (simp add: ring_eq_simps)

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

  2020     by (simp_all add: prems mult_mono)

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

  2022   proof -

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

  2024       by (simp add: mult_left_mono prems)

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

  2026       by (simp add: mult_right_mono_neg prems)

  2027     ultimately show ?thesis

  2028       by simp

  2029   qed

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

  2031   proof -

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

  2033       by (simp add: mult_right_mono prems)

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

  2035       by (simp add: mult_left_mono_neg prems)

  2036     ultimately show ?thesis

  2037       by simp

  2038   qed

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

  2040   proof -

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

  2042       by (simp add: mult_left_mono_neg prems)

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

  2044       by (simp add: mult_right_mono_neg prems)

  2045     ultimately show ?thesis

  2046       by simp

  2047   qed

  2048   ultimately show ?thesis

  2049     by - (rule add_mono | simp)+

  2050 qed

  2051

  2052 lemma mult_ge_prts:

  2053   assumes

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

  2055   "a <= a2"

  2056   "b1 <= b"

  2057   "b <= b2"

  2058   shows

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

  2060 proof -

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

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

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

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

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

  2066     by (simp only: minus_le_iff)

  2067   then show ?thesis by simp

  2068 qed

  2069

  2070 subsection {* Theorems for proof tools *}

  2071

  2072 lemma add_mono_thms_ordered_semiring:

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

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

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

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

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

  2078 by (rule add_mono, clarify+)+

  2079

  2080 lemma add_mono_thms_ordered_field:

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

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

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

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

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

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

  2087 by (auto intro: add_strict_right_mono add_strict_left_mono

  2088   add_less_le_mono add_le_less_mono add_strict_mono)

  2089

  2090 end