src/HOL/Ring_and_Field.thy
 author haftmann Fri Mar 09 08:45:50 2007 +0100 (2007-03-09) changeset 22422 ee19cdb07528 parent 22390 378f34b1e380 child 22452 8a86fd2a1bf0 permissions -rw-r--r--
stepping towards uniform lattice theory development in HOL
     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 axclass lordered_ring \<subseteq> 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

   278

   279 instance ordered_ring_strict \<subseteq> lordered_ab_group ..

   280

   281 instance ordered_ring_strict \<subseteq> lordered_ring

   282   by intro_classes (simp add: abs_if sup_eq_if)

   283

   284 class pordered_comm_ring = comm_ring + pordered_comm_semiring

   285

   286 class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +

   287   (*previously ordered_semiring*)

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

   289

   290 class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if

   291   (*previously ordered_ring*)

   292

   293 instance ordered_idom \<subseteq> ordered_ring_strict ..

   294

   295 class ordered_field = field + ordered_idom

   296

   297 lemmas linorder_neqE_ordered_idom =

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

   299

   300 lemma eq_add_iff1:

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

   302 apply (simp add: diff_minus left_distrib)

   303 apply (simp add: diff_minus left_distrib add_ac)

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

   305 done

   306

   307 lemma eq_add_iff2:

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

   309 apply (simp add: diff_minus left_distrib add_ac)

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

   311 done

   312

   313 lemma less_add_iff1:

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

   315 apply (simp add: diff_minus left_distrib add_ac)

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

   317 done

   318

   319 lemma less_add_iff2:

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

   321 apply (simp add: diff_minus left_distrib add_ac)

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

   323 done

   324

   325 lemma le_add_iff1:

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

   327 apply (simp add: diff_minus left_distrib add_ac)

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

   329 done

   330

   331 lemma le_add_iff2:

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

   333 apply (simp add: diff_minus left_distrib add_ac)

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

   335 done

   336

   337 subsection {* Ordering Rules for Multiplication *}

   338

   339 lemma mult_left_le_imp_le:

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

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

   342

   343 lemma mult_right_le_imp_le:

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

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

   346

   347 lemma mult_left_less_imp_less:

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

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

   350

   351 lemma mult_right_less_imp_less:

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

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

   354

   355 lemma mult_strict_left_mono_neg:

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

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

   358 apply (simp_all add: minus_mult_left [symmetric])

   359 done

   360

   361 lemma mult_left_mono_neg:

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

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

   364 apply (simp_all add: minus_mult_left [symmetric])

   365 done

   366

   367 lemma mult_strict_right_mono_neg:

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

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

   370 apply (simp_all add: minus_mult_right [symmetric])

   371 done

   372

   373 lemma mult_right_mono_neg:

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

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

   376 apply (simp)

   377 apply (simp_all add: minus_mult_right [symmetric])

   378 done

   379

   380 subsection{* Products of Signs *}

   381

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

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

   384

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

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

   387

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

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

   390

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

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

   393

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

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

   396

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

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

   399

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

   401 by (drule mult_strict_right_mono_neg, auto)

   402

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

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

   405

   406 lemma zero_less_mult_pos:

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

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

   409  apply (auto simp add: order_le_less linorder_not_less)

   410 apply (drule_tac mult_pos_neg [of a b])

   411  apply (auto dest: order_less_not_sym)

   412 done

   413

   414 lemma zero_less_mult_pos2:

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

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

   417  apply (auto simp add: order_le_less linorder_not_less)

   418 apply (drule_tac mult_pos_neg2 [of a b])

   419  apply (auto dest: order_less_not_sym)

   420 done

   421

   422 lemma zero_less_mult_iff:

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

   424 apply (auto simp add: order_le_less linorder_not_less mult_pos_pos

   425   mult_neg_neg)

   426 apply (blast dest: zero_less_mult_pos)

   427 apply (blast dest: zero_less_mult_pos2)

   428 done

   429

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

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

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

   433 apply (cases "a < 0")

   434 apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)

   435 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono)+

   436 done

   437

   438 lemma zero_le_mult_iff:

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

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

   441                    zero_less_mult_iff)

   442

   443 lemma mult_less_0_iff:

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

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

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

   447 done

   448

   449 lemma mult_le_0_iff:

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

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

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

   453 done

   454

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

   456 by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)

   457

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

   459 by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)

   460

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

   462 by (simp add: zero_le_mult_iff linorder_linear)

   463

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

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

   466

   467 instance ordered_idom \<subseteq> ordered_semidom

   468 proof

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

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

   471 qed

   472

   473 instance ordered_ring_strict \<subseteq> no_zero_divisors

   474 by (intro_classes, simp)

   475

   476 instance ordered_idom \<subseteq> idom ..

   477

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

   479

   480 lemmas one_neq_zero = zero_neq_one [THEN not_sym]

   481 declare one_neq_zero [simp]

   482

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

   484   by (rule zero_less_one [THEN order_less_imp_le])

   485

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

   487 by (simp add: linorder_not_le)

   488

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

   490 by (simp add: linorder_not_less)

   491

   492 subsection{*More Monotonicity*}

   493

   494 text{*Strict monotonicity in both arguments*}

   495 lemma mult_strict_mono:

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

   497 apply (cases "c=0")

   498  apply (simp add: mult_pos_pos)

   499 apply (erule mult_strict_right_mono [THEN order_less_trans])

   500  apply (force simp add: order_le_less)

   501 apply (erule mult_strict_left_mono, assumption)

   502 done

   503

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

   505 lemma mult_strict_mono':

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

   507 apply (rule mult_strict_mono)

   508 apply (blast intro: order_le_less_trans)+

   509 done

   510

   511 lemma mult_mono:

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

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

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

   515 apply (erule mult_left_mono, assumption)

   516 done

   517

   518 lemma mult_mono':

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

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

   521 apply (rule mult_mono)

   522 apply (fast intro: order_trans)+

   523 done

   524

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

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

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

   528 done

   529

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

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

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

   533   apply (erule order_less_le_trans)

   534   apply (erule mult_left_mono)

   535   apply simp

   536   apply (erule mult_strict_right_mono)

   537   apply assumption

   538 done

   539

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

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

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

   543   apply (erule order_le_less_trans)

   544   apply (erule mult_strict_left_mono)

   545   apply simp

   546   apply (erule mult_right_mono)

   547   apply simp

   548 done

   549

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

   551

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

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

   554

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

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

   557

   558 lemma mult_less_cancel_right_disj:

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

   560 apply (cases "c = 0")

   561 apply (auto simp add: linorder_neq_iff mult_strict_right_mono

   562                       mult_strict_right_mono_neg)

   563 apply (auto simp add: linorder_not_less

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

   565                       linorder_not_le [symmetric, of a])

   566 apply (erule_tac [!] notE)

   567 apply (auto simp add: order_less_imp_le mult_right_mono

   568                       mult_right_mono_neg)

   569 done

   570

   571 lemma mult_less_cancel_left_disj:

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

   573 apply (cases "c = 0")

   574 apply (auto simp add: linorder_neq_iff mult_strict_left_mono

   575                       mult_strict_left_mono_neg)

   576 apply (auto simp add: linorder_not_less

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

   578                       linorder_not_le [symmetric, of a])

   579 apply (erule_tac [!] notE)

   580 apply (auto simp add: order_less_imp_le mult_left_mono

   581                       mult_left_mono_neg)

   582 done

   583

   584

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

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

   587

   588 lemma mult_less_cancel_right:

   589   fixes c :: "'a :: ordered_ring_strict"

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

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

   592

   593 lemma mult_less_cancel_left:

   594   fixes c :: "'a :: ordered_ring_strict"

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

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

   597

   598 lemma mult_le_cancel_right:

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

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

   601

   602 lemma mult_le_cancel_left:

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

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

   605

   606 lemma mult_less_imp_less_left:

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

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

   609 proof (rule ccontr)

   610   assume "~ a < b"

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

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

   613   with this and less show False

   614     by (simp add: linorder_not_less [symmetric])

   615 qed

   616

   617 lemma mult_less_imp_less_right:

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

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

   620 proof (rule ccontr)

   621   assume "~ a < b"

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

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

   624   with this and less show False

   625     by (simp add: linorder_not_less [symmetric])

   626 qed

   627

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

   629 lemma mult_cancel_right [simp]:

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

   631 apply (cut_tac linorder_less_linear [of 0 c])

   632 apply (force dest: mult_strict_right_mono_neg mult_strict_right_mono

   633              simp add: linorder_neq_iff)

   634 done

   635

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

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

   638 lemma mult_cancel_left [simp]:

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

   640 apply (cut_tac linorder_less_linear [of 0 c])

   641 apply (force dest: mult_strict_left_mono_neg mult_strict_left_mono

   642              simp add: linorder_neq_iff)

   643 done

   644

   645

   646 subsubsection{*Special Cancellation Simprules for Multiplication*}

   647

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

   649

   650 lemma mult_le_cancel_right1:

   651   fixes c :: "'a :: ordered_idom"

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

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

   654

   655 lemma mult_le_cancel_right2:

   656   fixes c :: "'a :: ordered_idom"

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

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

   659

   660 lemma mult_le_cancel_left1:

   661   fixes c :: "'a :: ordered_idom"

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

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

   664

   665 lemma mult_le_cancel_left2:

   666   fixes c :: "'a :: ordered_idom"

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

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

   669

   670 lemma mult_less_cancel_right1:

   671   fixes c :: "'a :: ordered_idom"

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

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

   674

   675 lemma mult_less_cancel_right2:

   676   fixes c :: "'a :: ordered_idom"

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

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

   679

   680 lemma mult_less_cancel_left1:

   681   fixes c :: "'a :: ordered_idom"

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

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

   684

   685 lemma mult_less_cancel_left2:

   686   fixes c :: "'a :: ordered_idom"

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

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

   689

   690 lemma mult_cancel_right1 [simp]:

   691 fixes c :: "'a :: ordered_idom"

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

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

   694

   695 lemma mult_cancel_right2 [simp]:

   696 fixes c :: "'a :: ordered_idom"

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

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

   699

   700 lemma mult_cancel_left1 [simp]:

   701 fixes c :: "'a :: ordered_idom"

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

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

   704

   705 lemma mult_cancel_left2 [simp]:

   706 fixes c :: "'a :: ordered_idom"

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

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

   709

   710

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

   712 lemmas mult_compare_simps =

   713     mult_le_cancel_right mult_le_cancel_left

   714     mult_le_cancel_right1 mult_le_cancel_right2

   715     mult_le_cancel_left1 mult_le_cancel_left2

   716     mult_less_cancel_right mult_less_cancel_left

   717     mult_less_cancel_right1 mult_less_cancel_right2

   718     mult_less_cancel_left1 mult_less_cancel_left2

   719     mult_cancel_right mult_cancel_left

   720     mult_cancel_right1 mult_cancel_right2

   721     mult_cancel_left1 mult_cancel_left2

   722

   723

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

   725 lemmas ring_eq_simps =

   726 (*  mult_ac*)

   727   left_distrib right_distrib left_diff_distrib right_diff_distrib

   728   group_eq_simps

   729 (*  add_ac

   730   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   731   diff_eq_eq eq_diff_eq *)

   732

   733 subsection {* Fields *}

   734

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

   736 proof

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

   738   {

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

   740     also assume "a / b = 1"

   741     finally show "a = b" by simp

   742   next

   743     assume "a = b"

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

   745   }

   746 qed

   747

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

   749 by (simp add: divide_inverse)

   750

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

   752   by (simp add: divide_inverse)

   753

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

   755 by (simp add: divide_inverse)

   756

   757 lemma divide_self_if [simp]:

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

   759   by (simp add: divide_self)

   760

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

   762 by (simp add: divide_inverse)

   763

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

   765 by (simp add: divide_inverse)

   766

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

   768 by (simp add: divide_inverse left_distrib)

   769

   770

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

   772       of an ordering.*}

   773 lemma field_mult_eq_0_iff [simp]:

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

   775 proof cases

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

   777 next

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

   779   { assume "a * b = 0"

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

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

   782   thus ?thesis by force

   783 qed

   784

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

   786 lemma field_mult_cancel_right_lemma:

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

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

   789         shows "a=b"

   790 proof -

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

   792     by (simp add: eq)

   793   thus "a=b"

   794     by (simp add: mult_assoc cnz)

   795 qed

   796

   797 lemma field_mult_cancel_right [simp]:

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

   799 proof -

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

   801     by simp

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

   803      by (simp only: left_diff_distrib)

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

   805      by (simp add: disj_commute)

   806   finally show ?thesis .

   807 qed

   808

   809 lemma field_mult_cancel_left [simp]:

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

   811 proof -

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

   813     by simp

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

   815      by (simp only: right_diff_distrib)

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

   817      by simp

   818   finally show ?thesis .

   819 qed

   820

   821 lemma nonzero_imp_inverse_nonzero:

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

   823 proof

   824   assume ianz: "inverse a = 0"

   825   assume "a \<noteq> 0"

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

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

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

   829   thus False by (simp add: eq_commute)

   830 qed

   831

   832

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

   834

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

   836 apply (rule ccontr)

   837 apply (blast dest: nonzero_imp_inverse_nonzero)

   838 done

   839

   840 lemma inverse_nonzero_imp_nonzero:

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

   842 apply (rule ccontr)

   843 apply (blast dest: nonzero_imp_inverse_nonzero)

   844 done

   845

   846 lemma inverse_nonzero_iff_nonzero [simp]:

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

   848 by (force dest: inverse_nonzero_imp_nonzero)

   849

   850 lemma nonzero_inverse_minus_eq:

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

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

   853 proof -

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

   855     by simp

   856   thus ?thesis

   857     by (simp only: field_mult_cancel_left, simp)

   858 qed

   859

   860 lemma inverse_minus_eq [simp]:

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

   862 proof cases

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

   864 next

   865   assume "a\<noteq>0"

   866   thus ?thesis by (simp add: nonzero_inverse_minus_eq)

   867 qed

   868

   869 lemma nonzero_inverse_eq_imp_eq:

   870       assumes inveq: "inverse a = inverse b"

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

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

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

   874 proof -

   875   have "a * inverse b = a * inverse a"

   876     by (simp add: inveq)

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

   878     by simp

   879   thus "a = b"

   880     by (simp add: mult_assoc anz bnz)

   881 qed

   882

   883 lemma inverse_eq_imp_eq:

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

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

   886  apply (force dest!: inverse_zero_imp_zero

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

   888 apply (force dest!: nonzero_inverse_eq_imp_eq)

   889 done

   890

   891 lemma inverse_eq_iff_eq [simp]:

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

   893 by (force dest!: inverse_eq_imp_eq)

   894

   895 lemma nonzero_inverse_inverse_eq:

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

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

   898   proof -

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

   900     by (simp add: nonzero_imp_inverse_nonzero)

   901   thus ?thesis

   902     by (simp add: mult_assoc)

   903   qed

   904

   905 lemma inverse_inverse_eq [simp]:

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

   907   proof cases

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

   909   next

   910     assume "a\<noteq>0"

   911     thus ?thesis by (simp add: nonzero_inverse_inverse_eq)

   912   qed

   913

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

   915   proof -

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

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

   918   thus ?thesis  by simp

   919   qed

   920

   921 lemma inverse_unique:

   922   assumes ab: "a*b = 1"

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

   924 proof -

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

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

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

   928 qed

   929

   930 lemma nonzero_inverse_mult_distrib:

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

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

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

   934   proof -

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

   936     by (simp add: field_mult_eq_0_iff anz bnz)

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

   938     by (simp add: mult_assoc bnz)

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

   940     by simp

   941   thus ?thesis

   942     by (simp add: mult_assoc anz)

   943   qed

   944

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

   946       the right-hand side.*}

   947 lemma inverse_mult_distrib [simp]:

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

   949   proof cases

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

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

   952   next

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

   954     thus ?thesis  by force

   955   qed

   956

   957 lemma division_ring_inverse_add:

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

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

   960 by (simp add: right_distrib left_distrib mult_assoc)

   961

   962 lemma division_ring_inverse_diff:

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

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

   965 by (simp add: right_diff_distrib left_diff_distrib mult_assoc)

   966

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

   968 lemma inverse_add:

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

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

   971 by (simp add: division_ring_inverse_add mult_ac)

   972

   973 lemma inverse_divide [simp]:

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

   975   by (simp add: divide_inverse mult_commute)

   976

   977 subsection {* Calculations with fractions *}

   978

   979 lemma nonzero_mult_divide_cancel_left:

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

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

   982 proof -

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

   984     by (simp add: field_mult_eq_0_iff divide_inverse

   985                   nonzero_inverse_mult_distrib)

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

   987     by (simp only: mult_ac)

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

   989     by simp

   990     finally show ?thesis

   991     by (simp add: divide_inverse)

   992 qed

   993

   994 lemma mult_divide_cancel_left:

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

   996 apply (cases "b = 0")

   997 apply (simp_all add: nonzero_mult_divide_cancel_left)

   998 done

   999

  1000 lemma nonzero_mult_divide_cancel_right:

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

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

  1003

  1004 lemma mult_divide_cancel_right:

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

  1006 apply (cases "b = 0")

  1007 apply (simp_all add: nonzero_mult_divide_cancel_right)

  1008 done

  1009

  1010 (*For ExtractCommonTerm*)

  1011 lemma mult_divide_cancel_eq_if:

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

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

  1014   by (simp add: mult_divide_cancel_left)

  1015

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

  1017   by (simp add: divide_inverse)

  1018

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

  1020 by (simp add: divide_inverse mult_assoc)

  1021

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

  1023 by (simp add: divide_inverse mult_ac)

  1024

  1025 lemma divide_divide_eq_right [simp]:

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

  1027 by (simp add: divide_inverse mult_ac)

  1028

  1029 lemma divide_divide_eq_left [simp]:

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

  1031 by (simp add: divide_inverse mult_assoc)

  1032

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

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

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

  1036   apply (erule ssubst)

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

  1038   apply (erule ssubst)

  1039   apply (rule add_divide_distrib [THEN sym])

  1040   apply (subst mult_commute)

  1041   apply (erule nonzero_mult_divide_cancel_left [THEN sym])

  1042   apply assumption

  1043   apply (erule nonzero_mult_divide_cancel_right [THEN sym])

  1044   apply assumption

  1045 done

  1046

  1047 subsubsection{*Special Cancellation Simprules for Division*}

  1048

  1049 lemma mult_divide_cancel_left_if [simp]:

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

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

  1052 by (simp add: mult_divide_cancel_left)

  1053

  1054 lemma mult_divide_cancel_right_if [simp]:

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

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

  1057 by (simp add: mult_divide_cancel_right)

  1058

  1059 lemma mult_divide_cancel_left_if1 [simp]:

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

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

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

  1063 apply (simp del: mult_divide_cancel_left_if)

  1064 done

  1065

  1066 lemma mult_divide_cancel_left_if2 [simp]:

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

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

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

  1070 apply (simp del: mult_divide_cancel_left_if)

  1071 done

  1072

  1073 lemma mult_divide_cancel_right_if1 [simp]:

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

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

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

  1077 apply (simp del: mult_divide_cancel_right_if)

  1078 done

  1079

  1080 lemma mult_divide_cancel_right_if2 [simp]:

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

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

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

  1084 apply (simp del: mult_divide_cancel_right_if)

  1085 done

  1086

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

  1088

  1089 lemma times_divide_self_right [simp]:

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

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

  1092 by (simp add: times_divide_eq_right)

  1093

  1094 lemma times_divide_self_left [simp]:

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

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

  1097 by (simp add: times_divide_eq_left)

  1098

  1099

  1100 subsection {* Division and Unary Minus *}

  1101

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

  1103 by (simp add: divide_inverse minus_mult_left)

  1104

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

  1106 by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)

  1107

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

  1109 by (simp add: divide_inverse nonzero_inverse_minus_eq)

  1110

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

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

  1113

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

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

  1116

  1117

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

  1119 lemmas divide_minus_left = minus_divide_left [symmetric]

  1120 lemmas divide_minus_right = minus_divide_right [symmetric]

  1121 declare divide_minus_left [simp]   divide_minus_right [simp]

  1122

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

  1124 lemmas mult_minus_left = minus_mult_left [symmetric]

  1125 lemmas mult_minus_right = minus_mult_right [symmetric]

  1126 declare mult_minus_left [simp]   mult_minus_right [simp]

  1127

  1128 lemma minus_divide_divide [simp]:

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

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

  1131 apply (simp add: nonzero_minus_divide_divide)

  1132 done

  1133

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

  1135 by (simp add: diff_minus add_divide_distrib)

  1136

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

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

  1139   apply (subst diff_def)+

  1140   apply (subst minus_divide_left)

  1141   apply (subst add_frac_eq)

  1142   apply simp_all

  1143 done

  1144

  1145 subsection {* Ordered Fields *}

  1146

  1147 lemma positive_imp_inverse_positive:

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

  1149   proof -

  1150   have "0 < a * inverse a"

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

  1152   thus "0 < inverse a"

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

  1154   qed

  1155

  1156 lemma negative_imp_inverse_negative:

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

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

  1159       simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)

  1160

  1161 lemma inverse_le_imp_le:

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

  1163 	  and apos:  "0 < a"

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

  1165   proof (rule classical)

  1166   assume "~ b \<le> a"

  1167   hence "a < b"

  1168     by (simp add: linorder_not_le)

  1169   hence bpos: "0 < b"

  1170     by (blast intro: apos order_less_trans)

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

  1172     by (simp add: apos invle order_less_imp_le mult_left_mono)

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

  1174     by (simp add: bpos order_less_imp_le mult_right_mono)

  1175   thus "b \<le> a"

  1176     by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)

  1177   qed

  1178

  1179 lemma inverse_positive_imp_positive:

  1180       assumes inv_gt_0: "0 < inverse a"

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

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

  1183   proof -

  1184   have "0 < inverse (inverse a)"

  1185     by (rule positive_imp_inverse_positive)

  1186   thus "0 < a"

  1187     by (simp add: nonzero_inverse_inverse_eq)

  1188   qed

  1189

  1190 lemma inverse_positive_iff_positive [simp]:

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

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

  1193 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)

  1194 done

  1195

  1196 lemma inverse_negative_imp_negative:

  1197       assumes inv_less_0: "inverse a < 0"

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

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

  1200   proof -

  1201   have "inverse (inverse a) < 0"

  1202     by (rule negative_imp_inverse_negative)

  1203   thus "a < 0"

  1204     by (simp add: nonzero_inverse_inverse_eq)

  1205   qed

  1206

  1207 lemma inverse_negative_iff_negative [simp]:

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

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

  1210 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)

  1211 done

  1212

  1213 lemma inverse_nonnegative_iff_nonnegative [simp]:

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

  1215 by (simp add: linorder_not_less [symmetric])

  1216

  1217 lemma inverse_nonpositive_iff_nonpositive [simp]:

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

  1219 by (simp add: linorder_not_less [symmetric])

  1220

  1221

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

  1223

  1224 lemma less_imp_inverse_less:

  1225       assumes less: "a < b"

  1226 	  and apos:  "0 < a"

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

  1228   proof (rule ccontr)

  1229   assume "~ inverse b < inverse a"

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

  1231     by (simp add: linorder_not_less)

  1232   hence "~ (a < b)"

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

  1234   thus False

  1235     by (rule notE [OF _ less])

  1236   qed

  1237

  1238 lemma inverse_less_imp_less:

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

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

  1241 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)

  1242 done

  1243

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

  1245 lemma inverse_less_iff_less [simp]:

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

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

  1248 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

  1249

  1250 lemma le_imp_inverse_le:

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

  1252   by (force simp add: order_le_less less_imp_inverse_less)

  1253

  1254 lemma inverse_le_iff_le [simp]:

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

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

  1257 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

  1258

  1259

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

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

  1262 lemma inverse_le_imp_le_neg:

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

  1264   apply (rule classical)

  1265   apply (subgoal_tac "a < 0")

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

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

  1268   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1269   done

  1270

  1271 lemma less_imp_inverse_less_neg:

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

  1273   apply (subgoal_tac "a < 0")

  1274    prefer 2 apply (blast intro: order_less_trans)

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

  1276   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1277   done

  1278

  1279 lemma inverse_less_imp_less_neg:

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

  1281   apply (rule classical)

  1282   apply (subgoal_tac "a < 0")

  1283    prefer 2

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

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

  1286   apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1287   done

  1288

  1289 lemma inverse_less_iff_less_neg [simp]:

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

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

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

  1293   apply (simp del: inverse_less_iff_less

  1294 	      add: order_less_imp_not_eq nonzero_inverse_minus_eq)

  1295   done

  1296

  1297 lemma le_imp_inverse_le_neg:

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

  1299   by (force simp add: order_le_less less_imp_inverse_less_neg)

  1300

  1301 lemma inverse_le_iff_le_neg [simp]:

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

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

  1304 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

  1305

  1306

  1307 subsection{*Inverses and the Number One*}

  1308

  1309 lemma one_less_inverse_iff:

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

  1311   assume "0 < x"

  1312     with inverse_less_iff_less [OF zero_less_one, of x]

  1313     show ?thesis by simp

  1314 next

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

  1316   have "~ (1 < inverse x)"

  1317   proof

  1318     assume "1 < inverse x"

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

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

  1321     finally show False by auto

  1322   qed

  1323   with notless show ?thesis by simp

  1324 qed

  1325

  1326 lemma inverse_eq_1_iff [simp]:

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

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

  1329

  1330 lemma one_le_inverse_iff:

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

  1332 by (force simp add: order_le_less one_less_inverse_iff zero_less_one

  1333                     eq_commute [of 1])

  1334

  1335 lemma inverse_less_1_iff:

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

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

  1338

  1339 lemma inverse_le_1_iff:

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

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

  1342

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

  1344

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

  1346 proof -

  1347   assume less: "0<c"

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

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

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

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

  1352   finally show ?thesis .

  1353 qed

  1354

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

  1356 proof -

  1357   assume less: "c<0"

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

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

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

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

  1362   finally show ?thesis .

  1363 qed

  1364

  1365 lemma le_divide_eq:

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

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

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

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

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

  1371 apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)

  1372 done

  1373

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

  1375 proof -

  1376   assume less: "0<c"

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

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

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

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

  1381   finally show ?thesis .

  1382 qed

  1383

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

  1385 proof -

  1386   assume less: "c<0"

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

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

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

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

  1391   finally show ?thesis .

  1392 qed

  1393

  1394 lemma divide_le_eq:

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

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

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

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

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

  1400 apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)

  1401 done

  1402

  1403 lemma pos_less_divide_eq:

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

  1405 proof -

  1406   assume less: "0<c"

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

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

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

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

  1411   finally show ?thesis .

  1412 qed

  1413

  1414 lemma neg_less_divide_eq:

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

  1416 proof -

  1417   assume less: "c<0"

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

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

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

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

  1422   finally show ?thesis .

  1423 qed

  1424

  1425 lemma less_divide_eq:

  1426   "(a < b/c) =

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

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

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

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

  1431 apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)

  1432 done

  1433

  1434 lemma pos_divide_less_eq:

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

  1436 proof -

  1437   assume less: "0<c"

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

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

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

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

  1442   finally show ?thesis .

  1443 qed

  1444

  1445 lemma neg_divide_less_eq:

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

  1447 proof -

  1448   assume less: "c<0"

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

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

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

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

  1453   finally show ?thesis .

  1454 qed

  1455

  1456 lemma divide_less_eq:

  1457   "(b/c < a) =

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

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

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

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

  1462 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)

  1463 done

  1464

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

  1466 proof -

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

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

  1469     by (simp add: field_mult_cancel_right)

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

  1471     by (simp add: divide_inverse mult_assoc)

  1472   finally show ?thesis .

  1473 qed

  1474

  1475 lemma eq_divide_eq:

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

  1477 by (simp add: nonzero_eq_divide_eq)

  1478

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

  1480 proof -

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

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

  1483     by (simp add: field_mult_cancel_right)

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

  1485     by (simp add: divide_inverse mult_assoc)

  1486   finally show ?thesis .

  1487 qed

  1488

  1489 lemma divide_eq_eq:

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

  1491 by (force simp add: nonzero_divide_eq_eq)

  1492

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

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

  1495   by (subst divide_eq_eq, simp)

  1496

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

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

  1499   by (subst eq_divide_eq, simp)

  1500

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

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

  1503   apply (subst nonzero_eq_divide_eq)

  1504   apply assumption

  1505   apply (subst times_divide_eq_left)

  1506   apply (erule nonzero_divide_eq_eq)

  1507 done

  1508

  1509 subsection{*Division and Signs*}

  1510

  1511 lemma zero_less_divide_iff:

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

  1513 by (simp add: divide_inverse zero_less_mult_iff)

  1514

  1515 lemma divide_less_0_iff:

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

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

  1518 by (simp add: divide_inverse mult_less_0_iff)

  1519

  1520 lemma zero_le_divide_iff:

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

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

  1523 by (simp add: divide_inverse zero_le_mult_iff)

  1524

  1525 lemma divide_le_0_iff:

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

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

  1528 by (simp add: divide_inverse mult_le_0_iff)

  1529

  1530 lemma divide_eq_0_iff [simp]:

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

  1532 by (simp add: divide_inverse field_mult_eq_0_iff)

  1533

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

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

  1536   apply (subst pos_less_divide_eq)

  1537   apply assumption

  1538   apply simp

  1539 done

  1540

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

  1542     0 <= x / y"

  1543   apply (subst pos_le_divide_eq)

  1544   apply assumption

  1545   apply simp

  1546 done

  1547

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

  1549   apply (subst pos_divide_less_eq)

  1550   apply assumption

  1551   apply simp

  1552 done

  1553

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

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

  1556   apply (subst pos_divide_le_eq)

  1557   apply assumption

  1558   apply simp

  1559 done

  1560

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

  1562   apply (subst neg_divide_less_eq)

  1563   apply assumption

  1564   apply simp

  1565 done

  1566

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

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

  1569   apply (subst neg_divide_le_eq)

  1570   apply assumption

  1571   apply simp

  1572 done

  1573

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

  1575   apply (subst neg_less_divide_eq)

  1576   apply assumption

  1577   apply simp

  1578 done

  1579

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

  1581     0 <= x / y"

  1582   apply (subst neg_le_divide_eq)

  1583   apply assumption

  1584   apply simp

  1585 done

  1586

  1587 subsection{*Cancellation Laws for Division*}

  1588

  1589 lemma divide_cancel_right [simp]:

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

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

  1592 apply (simp add: divide_inverse field_mult_cancel_right)

  1593 done

  1594

  1595 lemma divide_cancel_left [simp]:

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

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

  1598 apply (simp add: divide_inverse field_mult_cancel_left)

  1599 done

  1600

  1601 subsection {* Division and the Number One *}

  1602

  1603 text{*Simplify expressions equated with 1*}

  1604 lemma divide_eq_1_iff [simp]:

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

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

  1607 apply (simp add: right_inverse_eq)

  1608 done

  1609

  1610 lemma one_eq_divide_iff [simp]:

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

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

  1613

  1614 lemma zero_eq_1_divide_iff [simp]:

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

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

  1617 apply (auto simp add: nonzero_eq_divide_eq)

  1618 done

  1619

  1620 lemma one_divide_eq_0_iff [simp]:

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

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

  1623 apply (insert zero_neq_one [THEN not_sym])

  1624 apply (auto simp add: nonzero_divide_eq_eq)

  1625 done

  1626

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

  1628 lemmas zero_less_divide_1_iff = zero_less_divide_iff [of 1, simplified]

  1629 lemmas divide_less_0_1_iff = divide_less_0_iff [of 1, simplified]

  1630 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]

  1631 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]

  1632

  1633 declare zero_less_divide_1_iff [simp]

  1634 declare divide_less_0_1_iff [simp]

  1635 declare zero_le_divide_1_iff [simp]

  1636 declare divide_le_0_1_iff [simp]

  1637

  1638 subsection {* Ordering Rules for Division *}

  1639

  1640 lemma divide_strict_right_mono:

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

  1642 by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono

  1643               positive_imp_inverse_positive)

  1644

  1645 lemma divide_right_mono:

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

  1647   by (force simp add: divide_strict_right_mono order_le_less)

  1648

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

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

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

  1652   apply auto

  1653 done

  1654

  1655 lemma divide_strict_right_mono_neg:

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

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

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

  1659 done

  1660

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

  1662       have the same sign*}

  1663 lemma divide_strict_left_mono:

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

  1665 by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono

  1666       order_less_imp_not_eq order_less_imp_not_eq2

  1667       less_imp_inverse_less less_imp_inverse_less_neg)

  1668

  1669 lemma divide_left_mono:

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

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

  1672    prefer 2

  1673    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)

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

  1675   apply (force simp add: divide_strict_left_mono order_le_less)

  1676   done

  1677

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

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

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

  1681   apply (auto simp add: mult_commute)

  1682 done

  1683

  1684 lemma divide_strict_left_mono_neg:

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

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

  1687    prefer 2

  1688    apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)

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

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

  1691   done

  1692

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

  1694

  1695 lemma le_divide_eq_1:

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

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

  1698 by (auto simp add: le_divide_eq)

  1699

  1700 lemma divide_le_eq_1:

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

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

  1703 by (auto simp add: divide_le_eq)

  1704

  1705 lemma less_divide_eq_1:

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

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

  1708 by (auto simp add: less_divide_eq)

  1709

  1710 lemma divide_less_eq_1:

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

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

  1713 by (auto simp add: divide_less_eq)

  1714

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

  1716

  1717 lemma le_divide_eq_1_pos [simp]:

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

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

  1720 by (auto simp add: le_divide_eq)

  1721

  1722 lemma le_divide_eq_1_neg [simp]:

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

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

  1725 by (auto simp add: le_divide_eq)

  1726

  1727 lemma divide_le_eq_1_pos [simp]:

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

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

  1730 by (auto simp add: divide_le_eq)

  1731

  1732 lemma divide_le_eq_1_neg [simp]:

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

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

  1735 by (auto simp add: divide_le_eq)

  1736

  1737 lemma less_divide_eq_1_pos [simp]:

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

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

  1740 by (auto simp add: less_divide_eq)

  1741

  1742 lemma less_divide_eq_1_neg [simp]:

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

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

  1745 by (auto simp add: less_divide_eq)

  1746

  1747 lemma divide_less_eq_1_pos [simp]:

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

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

  1750 by (auto simp add: divide_less_eq)

  1751

  1752 lemma divide_less_eq_1_neg [simp]:

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

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

  1755 by (auto simp add: divide_less_eq)

  1756

  1757 lemma eq_divide_eq_1 [simp]:

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

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

  1760 by (auto simp add: eq_divide_eq)

  1761

  1762 lemma divide_eq_eq_1 [simp]:

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

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

  1765 by (auto simp add: divide_eq_eq)

  1766

  1767 subsection {* Reasoning about inequalities with division *}

  1768

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

  1770     ==> x * y <= x"

  1771   by (auto simp add: mult_compare_simps);

  1772

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

  1774     ==> y * x <= x"

  1775   by (auto simp add: mult_compare_simps);

  1776

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

  1778     x / y <= z";

  1779   by (subst pos_divide_le_eq, assumption+);

  1780

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

  1782     z <= x / y";

  1783   by (subst pos_le_divide_eq, assumption+)

  1784

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

  1786     x / y < z"

  1787   by (subst pos_divide_less_eq, assumption+)

  1788

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

  1790     z < x / y"

  1791   by (subst pos_less_divide_eq, assumption+)

  1792

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

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

  1795   apply (rule mult_imp_div_pos_le)

  1796   apply simp;

  1797   apply (subst times_divide_eq_left);

  1798   apply (rule mult_imp_le_div_pos, assumption)

  1799   apply (rule mult_mono)

  1800   apply simp_all

  1801 done

  1802

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

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

  1805   apply (rule mult_imp_div_pos_less)

  1806   apply simp;

  1807   apply (subst times_divide_eq_left);

  1808   apply (rule mult_imp_less_div_pos, assumption)

  1809   apply (erule mult_less_le_imp_less)

  1810   apply simp_all

  1811 done

  1812

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

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

  1815   apply (rule mult_imp_div_pos_less)

  1816   apply simp_all

  1817   apply (subst times_divide_eq_left);

  1818   apply (rule mult_imp_less_div_pos, assumption)

  1819   apply (erule mult_le_less_imp_less)

  1820   apply simp_all

  1821 done

  1822

  1823 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left

  1824

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

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

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

  1828   seem to need them.*}

  1829

  1830 declare times_divide_eq [simp]

  1831

  1832 subsection {* Ordered Fields are Dense *}

  1833

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

  1835 proof -

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

  1837     by (blast intro: zero_less_one add_strict_left_mono)

  1838   thus ?thesis by simp

  1839 qed

  1840

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

  1842   by (blast intro: order_less_trans zero_less_one less_add_one)

  1843

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

  1845 by (simp add: zero_less_two pos_less_divide_eq right_distrib)

  1846

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

  1848 by (simp add: zero_less_two pos_divide_less_eq right_distrib)

  1849

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

  1851 by (blast intro!: less_half_sum gt_half_sum)

  1852

  1853

  1854 subsection {* Absolute Value *}

  1855

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

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

  1858

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

  1860 proof -

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

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

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

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

  1865   {

  1866     fix u v :: 'a

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

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

  1869                       nprt a * pprt b + nprt a * nprt b"

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

  1871       apply (simp add: left_distrib right_distrib add_ac)

  1872       done

  1873   }

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

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

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

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

  1878     apply (simp)

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

  1880     apply (rule addm2)

  1881     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1882     apply (rule addm)

  1883     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)

  1884     done

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

  1886     apply (simp add:diff_def)

  1887     apply (rule_tac y=0 in order_trans)

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

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

  1890     done

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

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

  1893   show ?thesis

  1894     apply (rule abs_leI)

  1895     apply (simp add: i1)

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

  1897     done

  1898 qed

  1899

  1900 lemma abs_eq_mult:

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

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

  1903 proof -

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

  1905     apply (auto)

  1906     apply (rule_tac split_mult_pos_le)

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

  1908     apply (simp)

  1909     apply (rule_tac split_mult_neg_le)

  1910     apply (insert prems)

  1911     apply (blast)

  1912     done

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

  1914     by (simp add: prts[symmetric])

  1915   show ?thesis

  1916   proof cases

  1917     assume "0 <= a * b"

  1918     then show ?thesis

  1919       apply (simp_all add: mulprts abs_prts)

  1920       apply (insert prems)

  1921       apply (auto simp add:

  1922 	ring_eq_simps

  1923 	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]

  1924 	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])

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

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

  1927       done

  1928   next

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

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

  1931     then show ?thesis

  1932       apply (simp_all add: mulprts abs_prts)

  1933       apply (insert prems)

  1934       apply (auto simp add: ring_eq_simps)

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

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

  1937       done

  1938   qed

  1939 qed

  1940

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

  1942 by (simp add: abs_eq_mult linorder_linear)

  1943

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

  1945 by (simp add: abs_if)

  1946

  1947 lemma nonzero_abs_inverse:

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

  1949 apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq

  1950                       negative_imp_inverse_negative)

  1951 apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)

  1952 done

  1953

  1954 lemma abs_inverse [simp]:

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

  1956       inverse (abs a)"

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

  1958 apply (simp add: nonzero_abs_inverse)

  1959 done

  1960

  1961 lemma nonzero_abs_divide:

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

  1963 by (simp add: divide_inverse abs_mult nonzero_abs_inverse)

  1964

  1965 lemma abs_divide [simp]:

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

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

  1968 apply (simp add: nonzero_abs_divide)

  1969 done

  1970

  1971 lemma abs_mult_less:

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

  1973 proof -

  1974   assume ac: "abs a < c"

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

  1976   assume "abs b < d"

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

  1978 qed

  1979

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

  1981 by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)

  1982

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

  1984 by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)

  1985

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

  1987 apply (simp add: order_less_le abs_le_iff)

  1988 apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)

  1989 apply (simp add: le_minus_self_iff linorder_neq_iff)

  1990 done

  1991

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

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

  1994   apply (subst abs_mult);

  1995   apply simp;

  1996 done;

  1997

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

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

  2000   apply (subst abs_divide);

  2001   apply (simp add: order_less_imp_le);

  2002 done;

  2003

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

  2005

  2006 lemma mult_le_prts:

  2007   assumes

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

  2009   "a <= a2"

  2010   "b1 <= b"

  2011   "b <= b2"

  2012   shows

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

  2014 proof -

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

  2016     apply (subst prts[symmetric])+

  2017     apply simp

  2018     done

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

  2020     by (simp add: ring_eq_simps)

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

  2022     by (simp_all add: prems mult_mono)

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

  2024   proof -

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

  2026       by (simp add: mult_left_mono prems)

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

  2028       by (simp add: mult_right_mono_neg prems)

  2029     ultimately show ?thesis

  2030       by simp

  2031   qed

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

  2033   proof -

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

  2035       by (simp add: mult_right_mono prems)

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

  2037       by (simp add: mult_left_mono_neg prems)

  2038     ultimately show ?thesis

  2039       by simp

  2040   qed

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

  2042   proof -

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

  2044       by (simp add: mult_left_mono_neg prems)

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

  2046       by (simp add: mult_right_mono_neg prems)

  2047     ultimately show ?thesis

  2048       by simp

  2049   qed

  2050   ultimately show ?thesis

  2051     by - (rule add_mono | simp)+

  2052 qed

  2053

  2054 lemma mult_ge_prts:

  2055   assumes

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

  2057   "a <= a2"

  2058   "b1 <= b"

  2059   "b <= b2"

  2060   shows

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

  2062 proof -

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

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

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

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

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

  2068     by (simp only: minus_le_iff)

  2069   then show ?thesis by simp

  2070 qed

  2071

  2072 ML {*

  2073 val left_distrib = thm "left_distrib";

  2074 val right_distrib = thm "right_distrib";

  2075 val mult_commute = thm "mult_commute";

  2076 val distrib = thm "distrib";

  2077 val zero_neq_one = thm "zero_neq_one";

  2078 val no_zero_divisors = thm "no_zero_divisors";

  2079 val left_inverse = thm "left_inverse";

  2080 val divide_inverse = thm "divide_inverse";

  2081 val mult_zero_left = thm "mult_zero_left";

  2082 val mult_zero_right = thm "mult_zero_right";

  2083 val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";

  2084 val inverse_zero = thm "inverse_zero";

  2085 val ring_distrib = thms "ring_distrib";

  2086 val combine_common_factor = thm "combine_common_factor";

  2087 val minus_mult_left = thm "minus_mult_left";

  2088 val minus_mult_right = thm "minus_mult_right";

  2089 val minus_mult_minus = thm "minus_mult_minus";

  2090 val minus_mult_commute = thm "minus_mult_commute";

  2091 val right_diff_distrib = thm "right_diff_distrib";

  2092 val left_diff_distrib = thm "left_diff_distrib";

  2093 val mult_left_mono = thm "mult_left_mono";

  2094 val mult_right_mono = thm "mult_right_mono";

  2095 val mult_strict_left_mono = thm "mult_strict_left_mono";

  2096 val mult_strict_right_mono = thm "mult_strict_right_mono";

  2097 val mult_mono = thm "mult_mono";

  2098 val mult_strict_mono = thm "mult_strict_mono";

  2099 val abs_if = thm "abs_if";

  2100 val zero_less_one = thm "zero_less_one";

  2101 val eq_add_iff1 = thm "eq_add_iff1";

  2102 val eq_add_iff2 = thm "eq_add_iff2";

  2103 val less_add_iff1 = thm "less_add_iff1";

  2104 val less_add_iff2 = thm "less_add_iff2";

  2105 val le_add_iff1 = thm "le_add_iff1";

  2106 val le_add_iff2 = thm "le_add_iff2";

  2107 val mult_left_le_imp_le = thm "mult_left_le_imp_le";

  2108 val mult_right_le_imp_le = thm "mult_right_le_imp_le";

  2109 val mult_left_less_imp_less = thm "mult_left_less_imp_less";

  2110 val mult_right_less_imp_less = thm "mult_right_less_imp_less";

  2111 val mult_strict_left_mono_neg = thm "mult_strict_left_mono_neg";

  2112 val mult_left_mono_neg = thm "mult_left_mono_neg";

  2113 val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";

  2114 val mult_right_mono_neg = thm "mult_right_mono_neg";

  2115 (*

  2116 val mult_pos = thm "mult_pos";

  2117 val mult_pos_le = thm "mult_pos_le";

  2118 val mult_pos_neg = thm "mult_pos_neg";

  2119 val mult_pos_neg_le = thm "mult_pos_neg_le";

  2120 val mult_pos_neg2 = thm "mult_pos_neg2";

  2121 val mult_pos_neg2_le = thm "mult_pos_neg2_le";

  2122 val mult_neg = thm "mult_neg";

  2123 val mult_neg_le = thm "mult_neg_le";

  2124 *)

  2125 val zero_less_mult_pos = thm "zero_less_mult_pos";

  2126 val zero_less_mult_pos2 = thm "zero_less_mult_pos2";

  2127 val zero_less_mult_iff = thm "zero_less_mult_iff";

  2128 val mult_eq_0_iff = thm "mult_eq_0_iff";

  2129 val zero_le_mult_iff = thm "zero_le_mult_iff";

  2130 val mult_less_0_iff = thm "mult_less_0_iff";

  2131 val mult_le_0_iff = thm "mult_le_0_iff";

  2132 val split_mult_pos_le = thm "split_mult_pos_le";

  2133 val split_mult_neg_le = thm "split_mult_neg_le";

  2134 val zero_le_square = thm "zero_le_square";

  2135 val zero_le_one = thm "zero_le_one";

  2136 val not_one_le_zero = thm "not_one_le_zero";

  2137 val not_one_less_zero = thm "not_one_less_zero";

  2138 val mult_left_mono_neg = thm "mult_left_mono_neg";

  2139 val mult_right_mono_neg = thm "mult_right_mono_neg";

  2140 val mult_strict_mono = thm "mult_strict_mono";

  2141 val mult_strict_mono' = thm "mult_strict_mono'";

  2142 val mult_mono = thm "mult_mono";

  2143 val less_1_mult = thm "less_1_mult";

  2144 val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";

  2145 val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";

  2146 val mult_less_cancel_right = thm "mult_less_cancel_right";

  2147 val mult_less_cancel_left = thm "mult_less_cancel_left";

  2148 val mult_le_cancel_right = thm "mult_le_cancel_right";

  2149 val mult_le_cancel_left = thm "mult_le_cancel_left";

  2150 val mult_less_imp_less_left = thm "mult_less_imp_less_left";

  2151 val mult_less_imp_less_right = thm "mult_less_imp_less_right";

  2152 val mult_cancel_right = thm "mult_cancel_right";

  2153 val mult_cancel_left = thm "mult_cancel_left";

  2154 val ring_eq_simps = thms "ring_eq_simps";

  2155 val right_inverse = thm "right_inverse";

  2156 val right_inverse_eq = thm "right_inverse_eq";

  2157 val nonzero_inverse_eq_divide = thm "nonzero_inverse_eq_divide";

  2158 val divide_self = thm "divide_self";

  2159 val divide_zero = thm "divide_zero";

  2160 val divide_zero_left = thm "divide_zero_left";

  2161 val inverse_eq_divide = thm "inverse_eq_divide";

  2162 val add_divide_distrib = thm "add_divide_distrib";

  2163 val field_mult_eq_0_iff = thm "field_mult_eq_0_iff";

  2164 val field_mult_cancel_right_lemma = thm "field_mult_cancel_right_lemma";

  2165 val field_mult_cancel_right = thm "field_mult_cancel_right";

  2166 val field_mult_cancel_left = thm "field_mult_cancel_left";

  2167 val nonzero_imp_inverse_nonzero = thm "nonzero_imp_inverse_nonzero";

  2168 val inverse_zero_imp_zero = thm "inverse_zero_imp_zero";

  2169 val inverse_nonzero_imp_nonzero = thm "inverse_nonzero_imp_nonzero";

  2170 val inverse_nonzero_iff_nonzero = thm "inverse_nonzero_iff_nonzero";

  2171 val nonzero_inverse_minus_eq = thm "nonzero_inverse_minus_eq";

  2172 val inverse_minus_eq = thm "inverse_minus_eq";

  2173 val nonzero_inverse_eq_imp_eq = thm "nonzero_inverse_eq_imp_eq";

  2174 val inverse_eq_imp_eq = thm "inverse_eq_imp_eq";

  2175 val inverse_eq_iff_eq = thm "inverse_eq_iff_eq";

  2176 val nonzero_inverse_inverse_eq = thm "nonzero_inverse_inverse_eq";

  2177 val inverse_inverse_eq = thm "inverse_inverse_eq";

  2178 val inverse_1 = thm "inverse_1";

  2179 val nonzero_inverse_mult_distrib = thm "nonzero_inverse_mult_distrib";

  2180 val inverse_mult_distrib = thm "inverse_mult_distrib";

  2181 val inverse_add = thm "inverse_add";

  2182 val inverse_divide = thm "inverse_divide";

  2183 val nonzero_mult_divide_cancel_left = thm "nonzero_mult_divide_cancel_left";

  2184 val mult_divide_cancel_left = thm "mult_divide_cancel_left";

  2185 val nonzero_mult_divide_cancel_right = thm "nonzero_mult_divide_cancel_right";

  2186 val mult_divide_cancel_right = thm "mult_divide_cancel_right";

  2187 val mult_divide_cancel_eq_if = thm "mult_divide_cancel_eq_if";

  2188 val divide_1 = thm "divide_1";

  2189 val times_divide_eq_right = thm "times_divide_eq_right";

  2190 val times_divide_eq_left = thm "times_divide_eq_left";

  2191 val divide_divide_eq_right = thm "divide_divide_eq_right";

  2192 val divide_divide_eq_left = thm "divide_divide_eq_left";

  2193 val nonzero_minus_divide_left = thm "nonzero_minus_divide_left";

  2194 val nonzero_minus_divide_right = thm "nonzero_minus_divide_right";

  2195 val nonzero_minus_divide_divide = thm "nonzero_minus_divide_divide";

  2196 val minus_divide_left = thm "minus_divide_left";

  2197 val minus_divide_right = thm "minus_divide_right";

  2198 val minus_divide_divide = thm "minus_divide_divide";

  2199 val diff_divide_distrib = thm "diff_divide_distrib";

  2200 val positive_imp_inverse_positive = thm "positive_imp_inverse_positive";

  2201 val negative_imp_inverse_negative = thm "negative_imp_inverse_negative";

  2202 val inverse_le_imp_le = thm "inverse_le_imp_le";

  2203 val inverse_positive_imp_positive = thm "inverse_positive_imp_positive";

  2204 val inverse_positive_iff_positive = thm "inverse_positive_iff_positive";

  2205 val inverse_negative_imp_negative = thm "inverse_negative_imp_negative";

  2206 val inverse_negative_iff_negative = thm "inverse_negative_iff_negative";

  2207 val inverse_nonnegative_iff_nonnegative = thm "inverse_nonnegative_iff_nonnegative";

  2208 val inverse_nonpositive_iff_nonpositive = thm "inverse_nonpositive_iff_nonpositive";

  2209 val less_imp_inverse_less = thm "less_imp_inverse_less";

  2210 val inverse_less_imp_less = thm "inverse_less_imp_less";

  2211 val inverse_less_iff_less = thm "inverse_less_iff_less";

  2212 val le_imp_inverse_le = thm "le_imp_inverse_le";

  2213 val inverse_le_iff_le = thm "inverse_le_iff_le";

  2214 val inverse_le_imp_le_neg = thm "inverse_le_imp_le_neg";

  2215 val less_imp_inverse_less_neg = thm "less_imp_inverse_less_neg";

  2216 val inverse_less_imp_less_neg = thm "inverse_less_imp_less_neg";

  2217 val inverse_less_iff_less_neg = thm "inverse_less_iff_less_neg";

  2218 val le_imp_inverse_le_neg = thm "le_imp_inverse_le_neg";

  2219 val inverse_le_iff_le_neg = thm "inverse_le_iff_le_neg";

  2220 val one_less_inverse_iff = thm "one_less_inverse_iff";

  2221 val inverse_eq_1_iff = thm "inverse_eq_1_iff";

  2222 val one_le_inverse_iff = thm "one_le_inverse_iff";

  2223 val inverse_less_1_iff = thm "inverse_less_1_iff";

  2224 val inverse_le_1_iff = thm "inverse_le_1_iff";

  2225 val zero_less_divide_iff = thm "zero_less_divide_iff";

  2226 val divide_less_0_iff = thm "divide_less_0_iff";

  2227 val zero_le_divide_iff = thm "zero_le_divide_iff";

  2228 val divide_le_0_iff = thm "divide_le_0_iff";

  2229 val divide_eq_0_iff = thm "divide_eq_0_iff";

  2230 val pos_le_divide_eq = thm "pos_le_divide_eq";

  2231 val neg_le_divide_eq = thm "neg_le_divide_eq";

  2232 val le_divide_eq = thm "le_divide_eq";

  2233 val pos_divide_le_eq = thm "pos_divide_le_eq";

  2234 val neg_divide_le_eq = thm "neg_divide_le_eq";

  2235 val divide_le_eq = thm "divide_le_eq";

  2236 val pos_less_divide_eq = thm "pos_less_divide_eq";

  2237 val neg_less_divide_eq = thm "neg_less_divide_eq";

  2238 val less_divide_eq = thm "less_divide_eq";

  2239 val pos_divide_less_eq = thm "pos_divide_less_eq";

  2240 val neg_divide_less_eq = thm "neg_divide_less_eq";

  2241 val divide_less_eq = thm "divide_less_eq";

  2242 val nonzero_eq_divide_eq = thm "nonzero_eq_divide_eq";

  2243 val eq_divide_eq = thm "eq_divide_eq";

  2244 val nonzero_divide_eq_eq = thm "nonzero_divide_eq_eq";

  2245 val divide_eq_eq = thm "divide_eq_eq";

  2246 val divide_cancel_right = thm "divide_cancel_right";

  2247 val divide_cancel_left = thm "divide_cancel_left";

  2248 val divide_eq_1_iff = thm "divide_eq_1_iff";

  2249 val one_eq_divide_iff = thm "one_eq_divide_iff";

  2250 val zero_eq_1_divide_iff = thm "zero_eq_1_divide_iff";

  2251 val one_divide_eq_0_iff = thm "one_divide_eq_0_iff";

  2252 val divide_strict_right_mono = thm "divide_strict_right_mono";

  2253 val divide_right_mono = thm "divide_right_mono";

  2254 val divide_strict_left_mono = thm "divide_strict_left_mono";

  2255 val divide_left_mono = thm "divide_left_mono";

  2256 val divide_strict_left_mono_neg = thm "divide_strict_left_mono_neg";

  2257 val divide_strict_right_mono_neg = thm "divide_strict_right_mono_neg";

  2258 val less_add_one = thm "less_add_one";

  2259 val zero_less_two = thm "zero_less_two";

  2260 val less_half_sum = thm "less_half_sum";

  2261 val gt_half_sum = thm "gt_half_sum";

  2262 val dense = thm "dense";

  2263 val abs_one = thm "abs_one";

  2264 val abs_le_mult = thm "abs_le_mult";

  2265 val abs_eq_mult = thm "abs_eq_mult";

  2266 val abs_mult = thm "abs_mult";

  2267 val abs_mult_self = thm "abs_mult_self";

  2268 val nonzero_abs_inverse = thm "nonzero_abs_inverse";

  2269 val abs_inverse = thm "abs_inverse";

  2270 val nonzero_abs_divide = thm "nonzero_abs_divide";

  2271 val abs_divide = thm "abs_divide";

  2272 val abs_mult_less = thm "abs_mult_less";

  2273 val eq_minus_self_iff = thm "eq_minus_self_iff";

  2274 val less_minus_self_iff = thm "less_minus_self_iff";

  2275 val abs_less_iff = thm "abs_less_iff";

  2276 *}

  2277

  2278 end