1.1 --- a/etc/settings	Tue Jul 12 12:49:46 2005 +0200
     1.2 +++ b/etc/settings	Tue Jul 12 17:56:03 2005 +0200
     1.3 @@ -63,7 +63,7 @@
     1.4  ### Compilation options (cf. isatool usedir)
     1.5  ###
     1.6  
     1.7 -ISABELLE_USEDIR_OPTIONS="-v true"
     1.8 +ISABELLE_USEDIR_OPTIONS="-v true -i true"
     1.9  
    1.10  # Specifically for the HOL image
    1.11  HOL_USEDIR_OPTIONS=""

     2.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 12 12:49:46 2005 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 12 17:56:03 2005 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOL/Finite_Set.thy
     2.5      ID:         $Id$
     2.6      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     2.7 -                Additions by Jeremy Avigad in Feb 2004
     2.8 +                with contributions by Jeremy Avigad
     2.9  *)
    2.10  
    2.11  header {* Finite sets *}
    2.12 @@ -1137,6 +1137,26 @@
    2.13    finally show ?thesis .
    2.14  qed
    2.15  
    2.16 +lemma setsum_mono3: "finite B ==> A <= B ==> 
    2.17 +    ALL x: B - A. 
    2.18 +      0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==>
    2.19 +        setsum f A <= setsum f B"
    2.20 +  apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
    2.21 +  apply (erule ssubst)
    2.22 +  apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
    2.23 +  apply simp
    2.24 +  apply (rule add_left_mono)
    2.25 +  apply (erule setsum_nonneg)
    2.26 +  apply (subst setsum_Un_disjoint [THEN sym])
    2.27 +  apply (erule finite_subset, assumption)
    2.28 +  apply (rule finite_subset)
    2.29 +  prefer 2
    2.30 +  apply assumption
    2.31 +  apply auto
    2.32 +  apply (rule setsum_cong)
    2.33 +  apply auto
    2.34 +done
    2.35 +
    2.36  (* FIXME: this is distributitivty, name as such! *)
    2.37  
    2.38  lemma setsum_mult: 
    2.39 @@ -1197,7 +1217,8 @@
    2.40      case (insert a A)
    2.41      hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
    2.42      also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
    2.43 -    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
    2.44 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
    2.45 +      by (simp del: abs_of_nonneg)
    2.46      also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
    2.47      finally show ?case .
    2.48    qed

     3.1 --- a/src/HOL/HOL.thy	Tue Jul 12 12:49:46 2005 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Jul 12 17:56:03 2005 +0200
     3.3 @@ -9,6 +9,7 @@
     3.4  imports CPure
     3.5  uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
     3.6        ("~~/src/Provers/eqsubst.ML")
     3.7 +
     3.8  begin
     3.9  
    3.10  subsection {* Primitive logic *}

     4.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Jul 12 12:49:46 2005 +0200
     4.2 +++ b/src/HOL/Hyperreal/Integration.thy	Tue Jul 12 17:56:03 2005 +0200
     4.3 @@ -429,7 +429,7 @@
     4.4   prefer 2 apply simp
     4.5  apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
     4.6  apply (drule_tac x = v in spec, simp add: times_divide_eq)
     4.7 -apply (drule_tac x = u in spec, auto, arith)
     4.8 +apply (drule_tac x = u in spec, auto)
     4.9  apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
    4.10  apply (rule order_trans)
    4.11  apply (auto simp add: abs_le_interval_iff)

     5.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 12 12:49:46 2005 +0200
     5.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Jul 12 17:56:03 2005 +0200
     5.3 @@ -600,7 +600,7 @@
     5.4      apply (drule lemma_odd_mod_4_div_2)
     5.5      apply (simp add: numeral_2_eq_2 divide_inverse)
     5.6      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
     5.7 -                   simp add: est mult_pos_le mult_ac divide_inverse
     5.8 +                   simp add: est mult_nonneg_nonneg mult_ac divide_inverse
     5.9                            power_abs [symmetric])
    5.10      done
    5.11  qed

     6.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Jul 12 12:49:46 2005 +0200
     6.2 +++ b/src/HOL/Hyperreal/NSA.thy	Tue Jul 12 17:56:03 2005 +0200
     6.3 @@ -1393,7 +1393,7 @@
     6.4  apply (simp add: Infinitesimal_approx_hrabs)
     6.5  apply (rule linorder_cases [of 0 x])  
     6.6  apply (frule lemma_approx_gt_zero [of x y]) 
     6.7 -apply (auto simp add: lemma_approx_less_zero [of x y])  
     6.8 +apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg)
     6.9  done
    6.10  
    6.11  lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0"

     7.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Tue Jul 12 12:49:46 2005 +0200
     7.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Tue Jul 12 17:56:03 2005 +0200
     7.3 @@ -115,7 +115,7 @@
     7.4  lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r"
     7.5  apply (simp (no_asm) add: right_distrib)
     7.6  apply (rule add_less_cancel_left [of "-r", THEN iffD1])
     7.7 -apply (auto intro: mult_pos
     7.8 +apply (auto intro: mult_pos_pos
     7.9              simp add: add_assoc [symmetric] neg_less_0_iff_less)
    7.10  done
    7.11  

     8.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jul 12 12:49:46 2005 +0200
     8.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jul 12 17:56:03 2005 +0200
     8.3 @@ -592,7 +592,7 @@
     8.4  apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
     8.5  apply (rule_tac [2] x = K in powser_insidea, auto)
     8.6  apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
     8.7 -apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eq], auto)
     8.8 +apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
     8.9  apply (simp add: diffs_def mult_assoc [symmetric])
    8.10  apply (subgoal_tac
    8.11          "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
    8.12 @@ -2418,7 +2418,7 @@
    8.13  
    8.14  lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    8.15  apply (rule_tac n = 1 in realpow_increasing)
    8.16 -apply (auto simp add: numeral_2_eq_2 [symmetric])
    8.17 +apply (auto simp add: numeral_2_eq_2 [symmetric] power2_abs)
    8.18  done
    8.19  
    8.20  lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
    8.21 @@ -2463,7 +2463,7 @@
    8.22  apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
    8.23  done
    8.24  
    8.25 -declare real_sqrt_sum_squares_ge_zero [THEN abs_eq, simp]
    8.26 +declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
    8.27  
    8.28  
    8.29  subsection{*A Few Theorems Involving Ln, Derivatives, etc.*}

     9.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Tue Jul 12 12:49:46 2005 +0200
     9.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Tue Jul 12 17:56:03 2005 +0200
     9.3 @@ -162,7 +162,7 @@
     9.4    "LESS_OR" > "Nat.Suc_leI"
     9.5    "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC"
     9.6    "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1"
     9.7 -  "LESS_MULT2" > "Ring_and_Field.mult_pos"
     9.8 +  "LESS_MULT2" > "Ring_and_Field.mult_pos_pos"
     9.9    "LESS_MONO_REV" > "Nat.Suc_less_SucD"
    9.10    "LESS_MONO_MULT" > "Nat.mult_le_mono1"
    9.11    "LESS_MONO_EQ" > "Nat.Suc_less_eq"

    10.1 --- a/src/HOL/Import/HOL/real.imp	Tue Jul 12 12:49:46 2005 +0200
    10.2 +++ b/src/HOL/Import/HOL/real.imp	Tue Jul 12 17:56:03 2005 +0200
    10.3 @@ -160,7 +160,7 @@
    10.4    "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less"
    10.5    "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
    10.6    "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'"
    10.7 -  "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
    10.8 +  "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
    10.9    "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono"
   10.10    "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
   10.11    "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
   10.12 @@ -217,7 +217,7 @@
   10.13    "REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le"
   10.14    "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le"
   10.15    "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
   10.16 -  "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le"
   10.17 +  "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg"
   10.18    "REAL_LE_LT" > "Orderings.order_le_less"
   10.19    "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
   10.20    "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"

    11.1 --- a/src/HOL/Import/HOL/realax.imp	Tue Jul 12 12:49:46 2005 +0200
    11.2 +++ b/src/HOL/Import/HOL/realax.imp	Tue Jul 12 17:56:03 2005 +0200
    11.3 @@ -98,7 +98,7 @@
    11.4    "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
    11.5    "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
    11.6    "REAL_LT_REFL" > "Orderings.order_less_irrefl"
    11.7 -  "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
    11.8 +  "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
    11.9    "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
   11.10    "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
   11.11    "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"

    12.1 --- a/src/HOL/Integ/NatBin.thy	Tue Jul 12 12:49:46 2005 +0200
    12.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Jul 12 17:56:03 2005 +0200
    12.3 @@ -274,40 +274,49 @@
    12.4  lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
    12.5    by (simp add: power2_eq_square)
    12.6  
    12.7 +lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"
    12.8 +  apply (subgoal_tac "3 = Suc (Suc (Suc 0))")
    12.9 +  apply (erule ssubst)
   12.10 +  apply (simp add: power_Suc mult_ac)
   12.11 +  apply (unfold nat_number_of_def)
   12.12 +  apply (subst nat_eq_iff)
   12.13 +  apply simp
   12.14 +done
   12.15 +
   12.16  text{*Squares of literal numerals will be evaluated.*}
   12.17  declare power2_eq_square [of "number_of w", standard, simp]
   12.18  
   12.19 -lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   12.20 +lemma zero_le_power2: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   12.21    by (simp add: power2_eq_square zero_le_square)
   12.22  
   12.23 -lemma zero_less_power2 [simp]:
   12.24 +lemma zero_less_power2:
   12.25       "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   12.26    by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   12.27  
   12.28 -lemma power2_less_0 [simp]:
   12.29 +lemma power2_less_0:
   12.30    fixes a :: "'a::{ordered_idom,recpower}"
   12.31    shows "~ (a\<twosuperior> < 0)"
   12.32  by (force simp add: power2_eq_square mult_less_0_iff) 
   12.33  
   12.34 -lemma zero_eq_power2 [simp]:
   12.35 +lemma zero_eq_power2:
   12.36       "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   12.37    by (force simp add: power2_eq_square mult_eq_0_iff)
   12.38  
   12.39 -lemma abs_power2 [simp]:
   12.40 +lemma abs_power2:
   12.41       "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   12.42    by (simp add: power2_eq_square abs_mult abs_mult_self)
   12.43  
   12.44 -lemma power2_abs [simp]:
   12.45 +lemma power2_abs:
   12.46       "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   12.47    by (simp add: power2_eq_square abs_mult_self)
   12.48  
   12.49 -lemma power2_minus [simp]:
   12.50 +lemma power2_minus:
   12.51       "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   12.52    by (simp add: power2_eq_square)
   12.53  
   12.54  lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   12.55  apply (induct "n")
   12.56 -apply (auto simp add: power_Suc power_add)
   12.57 +apply (auto simp add: power_Suc power_add power2_minus)
   12.58  done
   12.59  
   12.60  lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   12.61 @@ -320,7 +329,7 @@
   12.62       "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   12.63  by (simp add: power_minus1_even power_minus [of a]) 
   12.64  
   12.65 -lemma zero_le_even_power:
   12.66 +lemma zero_le_even_power':
   12.67       "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   12.68  proof (induct "n")
   12.69    case 0
   12.70 @@ -343,7 +352,7 @@
   12.71      have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" 
   12.72        by (simp add: mult_ac power_add power2_eq_square Power.power_Suc)
   12.73      thus ?case
   12.74 -      by (simp add: prems mult_less_0_iff mult_neg)
   12.75 +      by (simp add: prems mult_less_0_iff mult_neg_neg)
   12.76  qed
   12.77  
   12.78  lemma odd_0_le_power_imp_0_le:
   12.79 @@ -758,7 +767,7 @@
   12.80  val power2_minus = thm "power2_minus";
   12.81  val power_minus1_even = thm "power_minus1_even";
   12.82  val power_minus_even = thm "power_minus_even";
   12.83 -val zero_le_even_power = thm "zero_le_even_power";
   12.84 +(* val zero_le_even_power = thm "zero_le_even_power"; *)
   12.85  val odd_power_less_zero = thm "odd_power_less_zero";
   12.86  val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le";
   12.87  
   12.88 @@ -815,7 +824,7 @@
   12.89  val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj";
   12.90  
   12.91  val power_minus_even = thm"power_minus_even";
   12.92 -val zero_le_even_power = thm"zero_le_even_power";
   12.93 +(* val zero_le_even_power = thm"zero_le_even_power"; *)
   12.94  *}
   12.95  
   12.96  end

    13.1 --- a/src/HOL/Integ/NatSimprocs.thy	Tue Jul 12 12:49:46 2005 +0200
    13.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Tue Jul 12 17:56:03 2005 +0200
    13.3 @@ -243,28 +243,6 @@
    13.4  lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
    13.5  lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
    13.6  
    13.7 -text{*Simplify quotients that are compared with the value 1.*}
    13.8 -
    13.9 -lemma le_divide_eq_1:
   13.10 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.11 -  shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   13.12 -by (auto simp add: le_divide_eq)
   13.13 -
   13.14 -lemma divide_le_eq_1:
   13.15 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.16 -  shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   13.17 -by (auto simp add: divide_le_eq)
   13.18 -
   13.19 -lemma less_divide_eq_1:
   13.20 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.21 -  shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   13.22 -by (auto simp add: less_divide_eq)
   13.23 -
   13.24 -lemma divide_less_eq_1:
   13.25 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.26 -  shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   13.27 -by (auto simp add: divide_less_eq)
   13.28 -
   13.29  
   13.30  text{*Not good as automatic simprules because they cause case splits.*}
   13.31  lemmas divide_const_simps =
   13.32 @@ -272,55 +250,6 @@
   13.33    divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
   13.34    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
   13.35  
   13.36 -
   13.37 -subsection{*Conditional Simplification Rules: No Case Splits*}
   13.38 -
   13.39 -lemma le_divide_eq_1_pos [simp]:
   13.40 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.41 -  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
   13.42 -by (auto simp add: le_divide_eq)
   13.43 -
   13.44 -lemma le_divide_eq_1_neg [simp]:
   13.45 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.46 -  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
   13.47 -by (auto simp add: le_divide_eq)
   13.48 -
   13.49 -lemma divide_le_eq_1_pos [simp]:
   13.50 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.51 -  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
   13.52 -by (auto simp add: divide_le_eq)
   13.53 -
   13.54 -lemma divide_le_eq_1_neg [simp]:
   13.55 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.56 -  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
   13.57 -by (auto simp add: divide_le_eq)
   13.58 -
   13.59 -lemma less_divide_eq_1_pos [simp]:
   13.60 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.61 -  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
   13.62 -by (auto simp add: less_divide_eq)
   13.63 -
   13.64 -lemma less_divide_eq_1_neg [simp]:
   13.65 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.66 -  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
   13.67 -by (auto simp add: less_divide_eq)
   13.68 -
   13.69 -lemma divide_less_eq_1_pos [simp]:
   13.70 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.71 -  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
   13.72 -by (auto simp add: divide_less_eq)
   13.73 -
   13.74 -lemma eq_divide_eq_1 [simp]:
   13.75 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.76 -  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
   13.77 -by (auto simp add: eq_divide_eq)
   13.78 -
   13.79 -lemma divide_eq_eq_1 [simp]:
   13.80 -  fixes a :: "'a :: {ordered_field,division_by_zero}"
   13.81 -  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
   13.82 -by (auto simp add: divide_eq_eq)
   13.83 -
   13.84 -
   13.85  subsubsection{*Division By @{term "-1"}*}
   13.86  
   13.87  lemma divide_minus1 [simp]:
   13.88 @@ -337,9 +266,6 @@
   13.89  
   13.90  lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
   13.91  
   13.92 -
   13.93 -
   13.94 -
   13.95  ML
   13.96  {*
   13.97  val divide_minus1 = thm "divide_minus1";

    14.1 --- a/src/HOL/Integ/Parity.thy	Tue Jul 12 12:49:46 2005 +0200
    14.2 +++ b/src/HOL/Integ/Parity.thy	Tue Jul 12 17:56:03 2005 +0200
    14.3 @@ -152,9 +152,6 @@
    14.4  lemma even_nat_Suc: "even (Suc x) = odd x"
    14.5    by (simp add: even_nat_def)
    14.6  
    14.7 -text{*Compatibility, in case Avigad uses this*}
    14.8 -lemmas even_nat_suc = even_nat_Suc
    14.9 -
   14.10  lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
   14.11    by (simp add: even_nat_def int_power)
   14.12  
   14.13 @@ -225,7 +222,25 @@
   14.14    apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto)
   14.15    done
   14.16  
   14.17 -subsection {* Powers of negative one *}
   14.18 +subsection {* Parity and powers *}
   14.19 +
   14.20 +lemma minus_one_even_odd_power:
   14.21 +     "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & 
   14.22 +      (odd x --> (- 1::'a)^x = - 1)"
   14.23 +  apply (induct x)
   14.24 +  apply (rule conjI)
   14.25 +  apply simp
   14.26 +  apply (insert even_nat_zero, blast)
   14.27 +  apply (simp add: power_Suc)
   14.28 +done
   14.29 +
   14.30 +lemma minus_one_even_power [simp]:
   14.31 +     "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1"
   14.32 +  by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
   14.33 +
   14.34 +lemma minus_one_odd_power [simp]:
   14.35 +     "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1"
   14.36 +  by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
   14.37  
   14.38  lemma neg_one_even_odd_power:
   14.39       "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & 
   14.40 @@ -247,6 +262,119 @@
   14.41        (if even n then (x ^ n) else -(x ^ n))"
   14.42    by (induct n, simp_all split: split_if_asm add: power_Suc) 
   14.43  
   14.44 +lemma zero_le_even_power: "even n ==> 
   14.45 +    0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n"
   14.46 +  apply (simp add: even_nat_equiv_def2)
   14.47 +  apply (erule exE)
   14.48 +  apply (erule ssubst)
   14.49 +  apply (subst power_add)
   14.50 +  apply (rule zero_le_square)
   14.51 +  done
   14.52 +
   14.53 +lemma zero_le_odd_power: "odd n ==> 
   14.54 +    (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
   14.55 +  apply (simp add: odd_nat_equiv_def2)
   14.56 +  apply (erule exE)
   14.57 +  apply (erule ssubst)
   14.58 +  apply (subst power_Suc)
   14.59 +  apply (subst power_add)
   14.60 +  apply (subst zero_le_mult_iff)
   14.61 +  apply auto
   14.62 +  apply (subgoal_tac "x = 0 & 0 < y")
   14.63 +  apply (erule conjE, assumption)
   14.64 +  apply (subst power_eq_0_iff [THEN sym])
   14.65 +  apply (subgoal_tac "0 <= x^y * x^y")
   14.66 +  apply simp
   14.67 +  apply (rule zero_le_square)+
   14.68 +done
   14.69 +
   14.70 +lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = 
   14.71 +    (even n | (odd n & 0 <= x))"
   14.72 +  apply auto
   14.73 +  apply (subst zero_le_odd_power [THEN sym])
   14.74 +  apply assumption+
   14.75 +  apply (erule zero_le_even_power)
   14.76 +  apply (subst zero_le_odd_power) 
   14.77 +  apply assumption+
   14.78 +done
   14.79 +
   14.80 +lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = 
   14.81 +    (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))"
   14.82 +  apply (rule iffI)
   14.83 +  apply clarsimp
   14.84 +  apply (rule conjI)
   14.85 +  apply clarsimp
   14.86 +  apply (rule ccontr)
   14.87 +  apply (subgoal_tac "~ (0 <= x^n)")
   14.88 +  apply simp
   14.89 +  apply (subst zero_le_odd_power)
   14.90 +  apply assumption 
   14.91 +  apply simp
   14.92 +  apply (rule notI)
   14.93 +  apply (simp add: power_0_left)
   14.94 +  apply (rule notI)
   14.95 +  apply (simp add: power_0_left)
   14.96 +  apply auto
   14.97 +  apply (subgoal_tac "0 <= x^n")
   14.98 +  apply (frule order_le_imp_less_or_eq)
   14.99 +  apply simp
  14.100 +  apply (erule zero_le_even_power)
  14.101 +  apply (subgoal_tac "0 <= x^n")
  14.102 +  apply (frule order_le_imp_less_or_eq)
  14.103 +  apply auto
  14.104 +  apply (subst zero_le_odd_power)
  14.105 +  apply assumption
  14.106 +  apply (erule order_less_imp_le)
  14.107 +done
  14.108 +
  14.109 +lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
  14.110 +    (odd n & x < 0)" 
  14.111 +  apply (subst linorder_not_le [THEN sym])+
  14.112 +  apply (subst zero_le_power_eq)
  14.113 +  apply auto
  14.114 +done
  14.115 +
  14.116 +lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) =
  14.117 +    (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))"
  14.118 +  apply (subst linorder_not_less [THEN sym])+
  14.119 +  apply (subst zero_less_power_eq)
  14.120 +  apply auto
  14.121 +done
  14.122 +
  14.123 +lemma power_even_abs: "even n ==> 
  14.124 +    (abs (x::'a::{recpower,ordered_idom}))^n = x^n"
  14.125 +  apply (subst power_abs [THEN sym])
  14.126 +  apply (simp add: zero_le_even_power)
  14.127 +done
  14.128 +
  14.129 +lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
  14.130 +  apply (induct n)
  14.131 +  apply simp
  14.132 +  apply auto
  14.133 +done
  14.134 +
  14.135 +lemma power_minus_even [simp]: "even n ==> 
  14.136 +    (- x)^n = (x^n::'a::{recpower,comm_ring_1})"
  14.137 +  apply (subst power_minus)
  14.138 +  apply simp
  14.139 +done
  14.140 +
  14.141 +lemma power_minus_odd [simp]: "odd n ==> 
  14.142 +    (- x)^n = - (x^n::'a::{recpower,comm_ring_1})"
  14.143 +  apply (subst power_minus)
  14.144 +  apply simp
  14.145 +done
  14.146 +
  14.147 +(* Simplify, when the exponent is a numeral *)
  14.148 +
  14.149 +declare power_0_left [of "number_of w", standard, simp]
  14.150 +declare zero_le_power_eq [of _ "number_of w", standard, simp]
  14.151 +declare zero_less_power_eq [of _ "number_of w", standard, simp]
  14.152 +declare power_le_zero_eq [of _ "number_of w", standard, simp]
  14.153 +declare power_less_zero_eq [of _ "number_of w", standard, simp]
  14.154 +declare zero_less_power_nat_eq [of _ "number_of w", standard, simp]
  14.155 +declare power_eq_0_iff [of _ "number_of w", standard, simp]
  14.156 +declare power_even_abs [of "number_of w" _, standard, simp]
  14.157  
  14.158  subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
  14.159  

    15.1 --- a/src/HOL/NumberTheory/Gauss.thy	Tue Jul 12 12:49:46 2005 +0200
    15.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Tue Jul 12 17:56:03 2005 +0200
    15.3 @@ -180,7 +180,7 @@
    15.4  
    15.5  lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x";
    15.6    apply (insert a_nonzero)
    15.7 -by (auto simp add: B_def mult_pos A_greater_zero)
    15.8 +by (auto simp add: B_def mult_pos_pos A_greater_zero)
    15.9  
   15.10  lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)";
   15.11    apply (auto simp add: C_def)
   15.12 @@ -505,4 +505,4 @@
   15.13      by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym)
   15.14  qed
   15.15  
   15.16 -end
   15.17 \ No newline at end of file
   15.18 +end

    16.1 --- a/src/HOL/OrderedGroup.thy	Tue Jul 12 12:49:46 2005 +0200
    16.2 +++ b/src/HOL/OrderedGroup.thy	Tue Jul 12 17:56:03 2005 +0200
    16.3 @@ -1,6 +1,7 @@
    16.4  (*  Title:   HOL/OrderedGroup.thy
    16.5      ID:      $Id$
    16.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel
    16.7 +    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
    16.8 +             with contributions by Jeremy Avigad
    16.9  *)
   16.10  
   16.11  header {* Ordered Groups *}
   16.12 @@ -466,6 +467,72 @@
   16.13         diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   16.14         diff_eq_eq eq_diff_eq
   16.15  
   16.16 +subsection {* Support for reasoning about signs *}
   16.17 +
   16.18 +lemma add_pos_pos: "0 < 
   16.19 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   16.20 +      ==> 0 < y ==> 0 < x + y"
   16.21 +apply (subgoal_tac "0 + 0 < x + y")
   16.22 +apply simp
   16.23 +apply (erule add_less_le_mono)
   16.24 +apply (erule order_less_imp_le)
   16.25 +done
   16.26 +
   16.27 +lemma add_pos_nonneg: "0 < 
   16.28 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   16.29 +      ==> 0 <= y ==> 0 < x + y"
   16.30 +apply (subgoal_tac "0 + 0 < x + y")
   16.31 +apply simp
   16.32 +apply (erule add_less_le_mono, assumption)
   16.33 +done
   16.34 +
   16.35 +lemma add_nonneg_pos: "0 <= 
   16.36 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   16.37 +      ==> 0 < y ==> 0 < x + y"
   16.38 +apply (subgoal_tac "0 + 0 < x + y")
   16.39 +apply simp
   16.40 +apply (erule add_le_less_mono, assumption)
   16.41 +done
   16.42 +
   16.43 +lemma add_nonneg_nonneg: "0 <= 
   16.44 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
   16.45 +      ==> 0 <= y ==> 0 <= x + y"
   16.46 +apply (subgoal_tac "0 + 0 <= x + y")
   16.47 +apply simp
   16.48 +apply (erule add_mono, assumption)
   16.49 +done
   16.50 +
   16.51 +lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
   16.52 +    < 0 ==> y < 0 ==> x + y < 0"
   16.53 +apply (subgoal_tac "x + y < 0 + 0")
   16.54 +apply simp
   16.55 +apply (erule add_less_le_mono)
   16.56 +apply (erule order_less_imp_le)
   16.57 +done
   16.58 +
   16.59 +lemma add_neg_nonpos: 
   16.60 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0 
   16.61 +      ==> y <= 0 ==> x + y < 0"
   16.62 +apply (subgoal_tac "x + y < 0 + 0")
   16.63 +apply simp
   16.64 +apply (erule add_less_le_mono, assumption)
   16.65 +done
   16.66 +
   16.67 +lemma add_nonpos_neg: 
   16.68 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
   16.69 +      ==> y < 0 ==> x + y < 0"
   16.70 +apply (subgoal_tac "x + y < 0 + 0")
   16.71 +apply simp
   16.72 +apply (erule add_le_less_mono, assumption)
   16.73 +done
   16.74 +
   16.75 +lemma add_nonpos_nonpos: 
   16.76 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
   16.77 +      ==> y <= 0 ==> x + y <= 0"
   16.78 +apply (subgoal_tac "x + y <= 0 + 0")
   16.79 +apply simp
   16.80 +apply (erule add_mono, assumption)
   16.81 +done
   16.82  
   16.83  subsection{*Lemmas for the @{text cancel_numerals} simproc*}
   16.84  
   16.85 @@ -702,16 +769,6 @@
   16.86    show ?thesis by (simp add: abs_lattice join_eq_if)
   16.87  qed
   16.88  
   16.89 -lemma abs_eq [simp]:
   16.90 -  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
   16.91 -  shows  "0 \<le> a ==> abs a = a"
   16.92 -by (simp add: abs_if_lattice linorder_not_less [symmetric]) 
   16.93 -
   16.94 -lemma abs_minus_eq [simp]: 
   16.95 -  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
   16.96 -  shows "a < 0 ==> abs a = -a"
   16.97 -by (simp add: abs_if_lattice linorder_not_less [symmetric])
   16.98 -
   16.99  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
  16.100  proof -
  16.101    have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
  16.102 @@ -800,12 +857,19 @@
  16.103  lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
  16.104  by (simp)
  16.105  
  16.106 -lemma imp_abs_id: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
  16.107 +lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
  16.108  by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)
  16.109  
  16.110 -lemma imp_abs_neg_id: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
  16.111 +lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";
  16.112 +by (rule abs_of_nonneg, rule order_less_imp_le);
  16.113 +
  16.114 +lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
  16.115  by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)
  16.116  
  16.117 +lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==> 
  16.118 +  abs x = - x"
  16.119 +by (rule abs_of_nonpos, rule order_less_imp_le)
  16.120 +
  16.121  lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
  16.122  by (simp add: abs_lattice join_imp_le)
  16.123  
  16.124 @@ -847,6 +911,36 @@
  16.125    with g[symmetric] show ?thesis by simp
  16.126  qed
  16.127  
  16.128 +lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) - 
  16.129 +    abs b <= abs (a - b)"
  16.130 +  apply (simp add: compare_rls)
  16.131 +  apply (subgoal_tac "abs a = abs (a - b + b)")
  16.132 +  apply (erule ssubst)
  16.133 +  apply (rule abs_triangle_ineq)
  16.134 +  apply (rule arg_cong);back;
  16.135 +  apply (simp add: compare_rls)
  16.136 +done
  16.137 +
  16.138 +lemma abs_triangle_ineq3: 
  16.139 +    "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)"
  16.140 +  apply (subst abs_le_iff)
  16.141 +  apply auto
  16.142 +  apply (rule abs_triangle_ineq2)
  16.143 +  apply (subst abs_minus_commute)
  16.144 +  apply (rule abs_triangle_ineq2)
  16.145 +done
  16.146 +
  16.147 +lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <= 
  16.148 +    abs a + abs b"
  16.149 +proof -;
  16.150 +  have "abs(a - b) = abs(a + - b)"
  16.151 +    by (subst diff_minus, rule refl)
  16.152 +  also have "... <= abs a + abs (- b)"
  16.153 +    by (rule abs_triangle_ineq)
  16.154 +  finally show ?thesis
  16.155 +    by simp
  16.156 +qed
  16.157 +
  16.158  lemma abs_diff_triangle_ineq:
  16.159       "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
  16.160  proof -
  16.161 @@ -927,14 +1021,6 @@
  16.162    show ?thesis by (rule le_add_right_mono[OF 2 3])
  16.163  qed
  16.164  
  16.165 -lemma abs_of_ge_0: "0 <= (y::'a::lordered_ab_group_abs) \<Longrightarrow> abs y = y"
  16.166 -proof -
  16.167 -  assume 1:"0 <= y"
  16.168 -  have 2:"-y <= 0" by (simp add: 1)
  16.169 -  from 1 2 have 3:"-y <= y" by (simp only:)
  16.170 -  show ?thesis by (simp add: abs_lattice ge_imp_join_eq[OF 3])
  16.171 -qed
  16.172 -
  16.173  ML {*
  16.174  val add_zero_left = thm"add_0";
  16.175  val add_zero_right = thm"add_0_right";
  16.176 @@ -1068,8 +1154,8 @@
  16.177  val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
  16.178  val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
  16.179  val iff2imp = thm "iff2imp";
  16.180 -val imp_abs_id = thm "imp_abs_id";
  16.181 -val imp_abs_neg_id = thm "imp_abs_neg_id";
  16.182 +(* val imp_abs_id = thm "imp_abs_id";
  16.183 +val imp_abs_neg_id = thm "imp_abs_neg_id"; *)
  16.184  val abs_leI = thm "abs_leI";
  16.185  val le_minus_self_iff = thm "le_minus_self_iff";
  16.186  val minus_le_self_iff = thm "minus_le_self_iff";

    17.1 --- a/src/HOL/Power.thy	Tue Jul 12 12:49:46 2005 +0200
    17.2 +++ b/src/HOL/Power.thy	Tue Jul 12 17:56:03 2005 +0200
    17.3 @@ -50,7 +50,7 @@
    17.4  lemma zero_less_power:
    17.5       "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
    17.6  apply (induct "n")
    17.7 -apply (simp_all add: power_Suc zero_less_one mult_pos)
    17.8 +apply (simp_all add: power_Suc zero_less_one mult_pos_pos)
    17.9  done
   17.10  
   17.11  lemma zero_le_power:
   17.12 @@ -165,6 +165,12 @@
   17.13  apply (auto simp add: power_Suc inverse_mult_distrib)
   17.14  done
   17.15  
   17.16 +lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = 
   17.17 +    (1 / a)^n"
   17.18 +apply (simp add: divide_inverse)
   17.19 +apply (rule power_inverse)
   17.20 +done
   17.21 +
   17.22  lemma nonzero_power_divide:
   17.23      "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
   17.24  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)

    18.1 --- a/src/HOL/Real/PReal.thy	Tue Jul 12 12:49:46 2005 +0200
    18.2 +++ b/src/HOL/Real/PReal.thy	Tue Jul 12 17:56:03 2005 +0200
    18.3 @@ -372,7 +372,7 @@
    18.4    obtain y where [simp]: "0 < y" "y \<notin> B" by blast
    18.5    show ?thesis
    18.6    proof (intro exI conjI)
    18.7 -    show "0 < x*y" by (simp add: mult_pos)
    18.8 +    show "0 < x*y" by (simp add: mult_pos_pos)
    18.9      show "x * y \<notin> mult_set A B"
   18.10      proof -
   18.11        { fix u::rat and v::rat
   18.12 @@ -398,7 +398,7 @@
   18.13  proof
   18.14    show "mult_set A B \<subseteq> {r. 0 < r}"
   18.15      by (force simp add: mult_set_def
   18.16 -              intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos)
   18.17 +              intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
   18.18  next
   18.19    show "mult_set A B \<noteq> {r. 0 < r}"
   18.20      by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
   18.21 @@ -491,7 +491,8 @@
   18.22        have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   18.23        hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
   18.24        thus "u * v \<in> A"
   18.25 -        by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos)
   18.26 +        by (force intro: preal_downwards_closed [OF A v] mult_pos_pos 
   18.27 +          upos vpos)
   18.28      qed
   18.29    next
   18.30      show "A \<subseteq> ?lhs"

    19.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jul 12 12:49:46 2005 +0200
    19.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jul 12 17:56:03 2005 +0200
    19.3 @@ -1,6 +1,7 @@
    19.4  (*  Title:   HOL/Ring_and_Field.thy
    19.5      ID:      $Id$
    19.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel
    19.7 +    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
    19.8 +             with contributions by Jeremy Avigad
    19.9  *)
   19.10  
   19.11  header {* (Ordered) Rings and Fields *}
   19.12 @@ -330,28 +331,28 @@
   19.13  
   19.14  subsection{* Products of Signs *}
   19.15  
   19.16 -lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
   19.17 +lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b"
   19.18  by (drule mult_strict_left_mono [of 0 b], auto)
   19.19  
   19.20 -lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
   19.21 +lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
   19.22  by (drule mult_left_mono [of 0 b], auto)
   19.23  
   19.24  lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0"
   19.25  by (drule mult_strict_left_mono [of b 0], auto)
   19.26  
   19.27 -lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
   19.28 +lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
   19.29  by (drule mult_left_mono [of b 0], auto)
   19.30  
   19.31  lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" 
   19.32  by (drule mult_strict_right_mono[of b 0], auto)
   19.33  
   19.34 -lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 
   19.35 +lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 0" 
   19.36  by (drule mult_right_mono[of b 0], auto)
   19.37  
   19.38 -lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
   19.39 +lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b"
   19.40  by (drule mult_strict_right_mono_neg, auto)
   19.41  
   19.42 -lemma mult_neg_le: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
   19.43 +lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
   19.44  by (drule mult_right_mono_neg[of a 0 b ], auto)
   19.45  
   19.46  lemma zero_less_mult_pos:
   19.47 @@ -372,7 +373,8 @@
   19.48  
   19.49  lemma zero_less_mult_iff:
   19.50       "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)"
   19.51 -apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg)
   19.52 +apply (auto simp add: order_le_less linorder_not_less mult_pos_pos 
   19.53 +  mult_neg_neg)
   19.54  apply (blast dest: zero_less_mult_pos) 
   19.55  apply (blast dest: zero_less_mult_pos2)
   19.56  done
   19.57 @@ -403,10 +405,10 @@
   19.58  done
   19.59  
   19.60  lemma split_mult_pos_le: "(0 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> a * (b::_::pordered_ring)"
   19.61 -by (auto simp add: mult_pos_le mult_neg_le)
   19.62 +by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   19.63  
   19.64  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)" 
   19.65 -by (auto simp add: mult_pos_neg_le mult_pos_neg2_le)
   19.66 +by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
   19.67  
   19.68  lemma zero_le_square: "(0::'a::ordered_ring_strict) \<le> a*a"
   19.69  by (simp add: zero_le_mult_iff linorder_linear) 
   19.70 @@ -444,7 +446,7 @@
   19.71  lemma mult_strict_mono:
   19.72       "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring_strict)"
   19.73  apply (case_tac "c=0")
   19.74 - apply (simp add: mult_pos) 
   19.75 + apply (simp add: mult_pos_pos) 
   19.76  apply (erule mult_strict_right_mono [THEN order_less_trans])
   19.77   apply (force simp add: order_le_less) 
   19.78  apply (erule mult_strict_left_mono, assumption)
   19.79 @@ -469,6 +471,26 @@
   19.80  apply (simp add:  order_less_trans [OF zero_less_one]) 
   19.81  done
   19.82  
   19.83 +lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==>
   19.84 +    c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d"
   19.85 +  apply (subgoal_tac "a * c < b * c")
   19.86 +  apply (erule order_less_le_trans)
   19.87 +  apply (erule mult_left_mono)
   19.88 +  apply simp
   19.89 +  apply (erule mult_strict_right_mono)
   19.90 +  apply assumption
   19.91 +done
   19.92 +
   19.93 +lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==>
   19.94 +    c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d"
   19.95 +  apply (subgoal_tac "a * c <= b * c")
   19.96 +  apply (erule order_le_less_trans)
   19.97 +  apply (erule mult_strict_left_mono)
   19.98 +  apply simp
   19.99 +  apply (erule mult_right_mono)
  19.100 +  apply simp
  19.101 +done
  19.102 +
  19.103  subsection{*Cancellation Laws for Relationships With a Common Factor*}
  19.104  
  19.105  text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
  19.106 @@ -774,7 +796,7 @@
  19.107  qed
  19.108  
  19.109  lemma inverse_minus_eq [simp]:
  19.110 -   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})";
  19.111 +   "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"
  19.112  proof cases
  19.113    assume "a=0" thus ?thesis by (simp add: inverse_zero)
  19.114  next
  19.115 @@ -882,6 +904,8 @@
  19.116        "inverse (a/b) = b / (a::'a::{field,division_by_zero})"
  19.117    by (simp add: divide_inverse mult_commute)
  19.118  
  19.119 +subsection {* Calculations with fractions *}
  19.120 +
  19.121  lemma nonzero_mult_divide_cancel_left:
  19.122    assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
  19.123      shows "(c*a)/(c*b) = a/(b::'a::field)"
  19.124 @@ -936,6 +960,19 @@
  19.125       "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
  19.126  by (simp add: divide_inverse mult_assoc)
  19.127  
  19.128 +lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  19.129 +    x / y + w / z = (x * z + w * y) / (y * z)"
  19.130 +  apply (subgoal_tac "x / y = (x * z) / (y * z)")
  19.131 +  apply (erule ssubst)
  19.132 +  apply (subgoal_tac "w / z = (w * y) / (y * z)")
  19.133 +  apply (erule ssubst)
  19.134 +  apply (rule add_divide_distrib [THEN sym])
  19.135 +  apply (subst mult_commute)
  19.136 +  apply (erule nonzero_mult_divide_cancel_left [THEN sym])
  19.137 +  apply assumption
  19.138 +  apply (erule nonzero_mult_divide_cancel_right [THEN sym])
  19.139 +  apply assumption
  19.140 +done
  19.141  
  19.142  subsubsection{*Special Cancellation Simprules for Division*}
  19.143  
  19.144 @@ -1025,6 +1062,13 @@
  19.145  lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
  19.146  by (simp add: diff_minus add_divide_distrib) 
  19.147  
  19.148 +lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  19.149 +    x / y - w / z = (x * z - w * y) / (y * z)"
  19.150 +  apply (subst diff_def)+
  19.151 +  apply (subst minus_divide_left)
  19.152 +  apply (subst add_frac_eq)
  19.153 +  apply simp_all
  19.154 +done
  19.155  
  19.156  subsection {* Ordered Fields *}
  19.157  
  19.158 @@ -1224,33 +1268,6 @@
  19.159     "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
  19.160  by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
  19.161  
  19.162 -
  19.163 -subsection{*Division and Signs*}
  19.164 -
  19.165 -lemma zero_less_divide_iff:
  19.166 -     "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  19.167 -by (simp add: divide_inverse zero_less_mult_iff)
  19.168 -
  19.169 -lemma divide_less_0_iff:
  19.170 -     "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  19.171 -      (0 < a & b < 0 | a < 0 & 0 < b)"
  19.172 -by (simp add: divide_inverse mult_less_0_iff)
  19.173 -
  19.174 -lemma zero_le_divide_iff:
  19.175 -     "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  19.176 -      (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  19.177 -by (simp add: divide_inverse zero_le_mult_iff)
  19.178 -
  19.179 -lemma divide_le_0_iff:
  19.180 -     "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  19.181 -      (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  19.182 -by (simp add: divide_inverse mult_le_0_iff)
  19.183 -
  19.184 -lemma divide_eq_0_iff [simp]:
  19.185 -     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  19.186 -by (simp add: divide_inverse field_mult_eq_0_iff)
  19.187 -
  19.188 -
  19.189  subsection{*Simplification of Inequalities Involving Literal Divisors*}
  19.190  
  19.191  lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
  19.192 @@ -1263,7 +1280,6 @@
  19.193    finally show ?thesis .
  19.194  qed
  19.195  
  19.196 -
  19.197  lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
  19.198  proof -
  19.199    assume less: "c<0"
  19.200 @@ -1312,7 +1328,6 @@
  19.201  apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) 
  19.202  done
  19.203  
  19.204 -
  19.205  lemma pos_less_divide_eq:
  19.206       "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
  19.207  proof -
  19.208 @@ -1403,6 +1418,99 @@
  19.209    "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
  19.210  by (force simp add: nonzero_divide_eq_eq) 
  19.211  
  19.212 +lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  19.213 +    b = a * c ==> b / c = a"
  19.214 +  by (subst divide_eq_eq, simp)
  19.215 +
  19.216 +lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
  19.217 +    a * c = b ==> a = b / c"
  19.218 +  by (subst eq_divide_eq, simp)
  19.219 +
  19.220 +lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
  19.221 +    (x / y = w / z) = (x * z = w * y)"
  19.222 +  apply (subst nonzero_eq_divide_eq)
  19.223 +  apply assumption
  19.224 +  apply (subst times_divide_eq_left)
  19.225 +  apply (erule nonzero_divide_eq_eq) 
  19.226 +done
  19.227 +
  19.228 +subsection{*Division and Signs*}
  19.229 +
  19.230 +lemma zero_less_divide_iff:
  19.231 +     "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
  19.232 +by (simp add: divide_inverse zero_less_mult_iff)
  19.233 +
  19.234 +lemma divide_less_0_iff:
  19.235 +     "(a/b < (0::'a::{ordered_field,division_by_zero})) = 
  19.236 +      (0 < a & b < 0 | a < 0 & 0 < b)"
  19.237 +by (simp add: divide_inverse mult_less_0_iff)
  19.238 +
  19.239 +lemma zero_le_divide_iff:
  19.240 +     "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
  19.241 +      (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
  19.242 +by (simp add: divide_inverse zero_le_mult_iff)
  19.243 +
  19.244 +lemma divide_le_0_iff:
  19.245 +     "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
  19.246 +      (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
  19.247 +by (simp add: divide_inverse mult_le_0_iff)
  19.248 +
  19.249 +lemma divide_eq_0_iff [simp]:
  19.250 +     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
  19.251 +by (simp add: divide_inverse field_mult_eq_0_iff)
  19.252 +
  19.253 +lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==> 
  19.254 +    0 < y ==> 0 < x / y"
  19.255 +  apply (subst pos_less_divide_eq)
  19.256 +  apply assumption
  19.257 +  apply simp
  19.258 +done
  19.259 +
  19.260 +lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==> 
  19.261 +    0 <= x / y"
  19.262 +  apply (subst pos_le_divide_eq)
  19.263 +  apply assumption
  19.264 +  apply simp
  19.265 +done
  19.266 +
  19.267 +lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
  19.268 +  apply (subst pos_divide_less_eq)
  19.269 +  apply assumption
  19.270 +  apply simp
  19.271 +done
  19.272 +
  19.273 +lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==> 
  19.274 +    0 < y ==> x / y <= 0"
  19.275 +  apply (subst pos_divide_le_eq)
  19.276 +  apply assumption
  19.277 +  apply simp
  19.278 +done
  19.279 +
  19.280 +lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
  19.281 +  apply (subst neg_divide_less_eq)
  19.282 +  apply assumption
  19.283 +  apply simp
  19.284 +done
  19.285 +
  19.286 +lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==> 
  19.287 +    y < 0 ==> x / y <= 0"
  19.288 +  apply (subst neg_divide_le_eq)
  19.289 +  apply assumption
  19.290 +  apply simp
  19.291 +done
  19.292 +
  19.293 +lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
  19.294 +  apply (subst neg_less_divide_eq)
  19.295 +  apply assumption
  19.296 +  apply simp
  19.297 +done
  19.298 +
  19.299 +lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 
  19.300 +    0 <= x / y"
  19.301 +  apply (subst neg_le_divide_eq)
  19.302 +  apply assumption
  19.303 +  apply simp
  19.304 +done
  19.305  
  19.306  subsection{*Cancellation Laws for Division*}
  19.307  
  19.308 @@ -1427,7 +1535,6 @@
  19.309  apply (simp add: right_inverse_eq) 
  19.310  done
  19.311  
  19.312 -
  19.313  lemma one_eq_divide_iff [simp]:
  19.314       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  19.315  by (simp add: eq_commute [of 1])  
  19.316 @@ -1451,7 +1558,6 @@
  19.317  declare zero_le_divide_iff [of "1", simp]
  19.318  declare divide_le_0_iff [of "1", simp]
  19.319  
  19.320 -
  19.321  subsection {* Ordering Rules for Division *}
  19.322  
  19.323  lemma divide_strict_right_mono:
  19.324 @@ -1463,6 +1569,17 @@
  19.325       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
  19.326    by (force simp add: divide_strict_right_mono order_le_less) 
  19.327  
  19.328 +lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  19.329 +    ==> c <= 0 ==> b / c <= a / c"
  19.330 +  apply (drule divide_right_mono [of _ _ "- c"])
  19.331 +  apply auto
  19.332 +done
  19.333 +
  19.334 +lemma divide_strict_right_mono_neg:
  19.335 +     "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  19.336 +apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
  19.337 +apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
  19.338 +done
  19.339  
  19.340  text{*The last premise ensures that @{term a} and @{term b} 
  19.341        have the same sign*}
  19.342 @@ -1481,6 +1598,12 @@
  19.343    apply (force simp add: divide_strict_left_mono order_le_less) 
  19.344    done
  19.345  
  19.346 +lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
  19.347 +    ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
  19.348 +  apply (drule divide_left_mono [of _ _ "- c"])
  19.349 +  apply (auto simp add: mult_commute)
  19.350 +done
  19.351 +
  19.352  lemma divide_strict_left_mono_neg:
  19.353       "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
  19.354    apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
  19.355 @@ -1490,12 +1613,139 @@
  19.356     apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) 
  19.357    done
  19.358  
  19.359 -lemma divide_strict_right_mono_neg:
  19.360 -     "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
  19.361 -apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
  19.362 -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
  19.363 +text{*Simplify quotients that are compared with the value 1.*}
  19.364 +
  19.365 +lemma le_divide_eq_1:
  19.366 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.367 +  shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  19.368 +by (auto simp add: le_divide_eq)
  19.369 +
  19.370 +lemma divide_le_eq_1:
  19.371 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.372 +  shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  19.373 +by (auto simp add: divide_le_eq)
  19.374 +
  19.375 +lemma less_divide_eq_1:
  19.376 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.377 +  shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  19.378 +by (auto simp add: less_divide_eq)
  19.379 +
  19.380 +lemma divide_less_eq_1:
  19.381 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.382 +  shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  19.383 +by (auto simp add: divide_less_eq)
  19.384 +
  19.385 +subsection{*Conditional Simplification Rules: No Case Splits*}
  19.386 +
  19.387 +lemma le_divide_eq_1_pos [simp]:
  19.388 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.389 +  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
  19.390 +by (auto simp add: le_divide_eq)
  19.391 +
  19.392 +lemma le_divide_eq_1_neg [simp]:
  19.393 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.394 +  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
  19.395 +by (auto simp add: le_divide_eq)
  19.396 +
  19.397 +lemma divide_le_eq_1_pos [simp]:
  19.398 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.399 +  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
  19.400 +by (auto simp add: divide_le_eq)
  19.401 +
  19.402 +lemma divide_le_eq_1_neg [simp]:
  19.403 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.404 +  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
  19.405 +by (auto simp add: divide_le_eq)
  19.406 +
  19.407 +lemma less_divide_eq_1_pos [simp]:
  19.408 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.409 +  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
  19.410 +by (auto simp add: less_divide_eq)
  19.411 +
  19.412 +lemma less_divide_eq_1_neg [simp]:
  19.413 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.414 +  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
  19.415 +by (auto simp add: less_divide_eq)
  19.416 +
  19.417 +lemma divide_less_eq_1_pos [simp]:
  19.418 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.419 +  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
  19.420 +by (auto simp add: divide_less_eq)
  19.421 +
  19.422 +lemma eq_divide_eq_1 [simp]:
  19.423 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.424 +  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
  19.425 +by (auto simp add: eq_divide_eq)
  19.426 +
  19.427 +lemma divide_eq_eq_1 [simp]:
  19.428 +  fixes a :: "'a :: {ordered_field,division_by_zero}"
  19.429 +  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
  19.430 +by (auto simp add: divide_eq_eq)
  19.431 +
  19.432 +subsection {* Reasoning about inequalities with division *}
  19.433 +
  19.434 +lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  19.435 +    ==> x * y <= x"
  19.436 +  by (auto simp add: mult_compare_simps);
  19.437 +
  19.438 +lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
  19.439 +    ==> y * x <= x"
  19.440 +  by (auto simp add: mult_compare_simps);
  19.441 +
  19.442 +lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
  19.443 +    x / y <= z";
  19.444 +  by (subst pos_divide_le_eq, assumption+);
  19.445 +
  19.446 +lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
  19.447 +    z <= x / y";
  19.448 +  by (subst pos_le_divide_eq, assumption+)
  19.449 +
  19.450 +lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
  19.451 +    x / y < z"
  19.452 +  by (subst pos_divide_less_eq, assumption+)
  19.453 +
  19.454 +lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
  19.455 +    z < x / y"
  19.456 +  by (subst pos_less_divide_eq, assumption+)
  19.457 +
  19.458 +lemma frac_le: "(0::'a::ordered_field) <= x ==> 
  19.459 +    x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
  19.460 +  apply (rule mult_imp_div_pos_le)
  19.461 +  apply simp;
  19.462 +  apply (subst times_divide_eq_left);
  19.463 +  apply (rule mult_imp_le_div_pos, assumption)
  19.464 +  apply (rule mult_mono)
  19.465 +  apply simp_all
  19.466  done
  19.467  
  19.468 +lemma frac_less: "(0::'a::ordered_field) <= x ==> 
  19.469 +    x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
  19.470 +  apply (rule mult_imp_div_pos_less)
  19.471 +  apply simp;
  19.472 +  apply (subst times_divide_eq_left);
  19.473 +  apply (rule mult_imp_less_div_pos, assumption)
  19.474 +  apply (erule mult_less_le_imp_less)
  19.475 +  apply simp_all
  19.476 +done
  19.477 +
  19.478 +lemma frac_less2: "(0::'a::ordered_field) < x ==> 
  19.479 +    x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
  19.480 +  apply (rule mult_imp_div_pos_less)
  19.481 +  apply simp_all
  19.482 +  apply (subst times_divide_eq_left);
  19.483 +  apply (rule mult_imp_less_div_pos, assumption)
  19.484 +  apply (erule mult_le_less_imp_less)
  19.485 +  apply simp_all
  19.486 +done
  19.487 +
  19.488 +lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
  19.489 +
  19.490 +text{*It's not obvious whether these should be simprules or not. 
  19.491 +  Their effect is to gather terms into one big fraction, like
  19.492 +  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  19.493 +  seem to need them.*}
  19.494 +
  19.495 +declare times_divide_eq [simp]
  19.496  
  19.497  subsection {* Ordered Fields are Dense *}
  19.498  
  19.499 @@ -1519,16 +1769,6 @@
  19.500  by (blast intro!: less_half_sum gt_half_sum)
  19.501  
  19.502  
  19.503 -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
  19.504 -
  19.505 -text{*It's not obvious whether these should be simprules or not. 
  19.506 -  Their effect is to gather terms into one big fraction, like
  19.507 -  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
  19.508 -  seem to need them.*}
  19.509 -
  19.510 -declare times_divide_eq [simp]
  19.511 -
  19.512 -
  19.513  subsection {* Absolute Value *}
  19.514  
  19.515  lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
  19.516 @@ -1556,15 +1796,15 @@
  19.517      apply (simp)
  19.518      apply (rule_tac y="0::'a" in order_trans)
  19.519      apply (rule addm2)
  19.520 -    apply (simp_all add: mult_pos_le mult_neg_le)
  19.521 +    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  19.522      apply (rule addm)
  19.523 -    apply (simp_all add: mult_pos_le mult_neg_le)
  19.524 +    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
  19.525      done
  19.526    have yx: "?y <= ?x"
  19.527      apply (simp add:diff_def)
  19.528      apply (rule_tac y=0 in order_trans)
  19.529 -    apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
  19.530 -    apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
  19.531 +    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  19.532 +    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
  19.533      done
  19.534    have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
  19.535    have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
  19.536 @@ -1600,8 +1840,8 @@
  19.537  	ring_eq_simps 
  19.538  	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
  19.539  	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
  19.540 -	apply(drule (1) mult_pos_neg_le[of a b], simp)
  19.541 -	apply(drule (1) mult_pos_neg2_le[of b a], simp)
  19.542 +	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
  19.543 +	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
  19.544        done
  19.545    next
  19.546      assume "~(0 <= a*b)"
  19.547 @@ -1610,8 +1850,8 @@
  19.548        apply (simp_all add: mulprts abs_prts)
  19.549        apply (insert prems)
  19.550        apply (auto simp add: ring_eq_simps)
  19.551 -      apply(drule (1) mult_pos_le[of a b],simp)
  19.552 -      apply(drule (1) mult_neg_le[of a b],simp)
  19.553 +      apply(drule (1) mult_nonneg_nonneg[of a b],simp)
  19.554 +      apply(drule (1) mult_nonpos_nonpos[of a b],simp)
  19.555        done
  19.556    qed
  19.557  qed
  19.558 @@ -1667,6 +1907,20 @@
  19.559  apply (simp add: le_minus_self_iff linorder_neq_iff) 
  19.560  done
  19.561  
  19.562 +lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> 
  19.563 +    (abs y) * x = abs (y * x)";
  19.564 +  apply (subst abs_mult);
  19.565 +  apply simp;
  19.566 +done;
  19.567 +
  19.568 +lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> 
  19.569 +    abs x / y = abs (x / y)";
  19.570 +  apply (subst abs_divide);
  19.571 +  apply (simp add: order_less_imp_le);
  19.572 +done;
  19.573 +
  19.574 +subsection {* Miscellaneous *}
  19.575 +
  19.576  lemma linprog_dual_estimate:
  19.577    assumes
  19.578    "A * x \<le> (b::'a::lordered_ring)"
  19.579 @@ -1712,7 +1966,7 @@
  19.580      by (simp)
  19.581    show ?thesis 
  19.582      apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
  19.583 -    apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]])
  19.584 +    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
  19.585      done
  19.586  qed
  19.587  
  19.588 @@ -1727,7 +1981,7 @@
  19.589      have 1: "A - A1 = A + (- A1)" by simp
  19.590      show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
  19.591    qed
  19.592 -  then have "abs (A-A1) = A-A1" by (rule abs_of_ge_0)
  19.593 +  then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
  19.594    with prems show "abs (A-A1) <= (A2-A1)" by simp
  19.595  qed
  19.596  
  19.597 @@ -1856,6 +2110,7 @@
  19.598  val mult_left_mono_neg = thm "mult_left_mono_neg";
  19.599  val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg";
  19.600  val mult_right_mono_neg = thm "mult_right_mono_neg";
  19.601 +(*
  19.602  val mult_pos = thm "mult_pos";
  19.603  val mult_pos_le = thm "mult_pos_le";
  19.604  val mult_pos_neg = thm "mult_pos_neg";
  19.605 @@ -1864,6 +2119,7 @@
  19.606  val mult_pos_neg2_le = thm "mult_pos_neg2_le";
  19.607  val mult_neg = thm "mult_neg";
  19.608  val mult_neg_le = thm "mult_neg_le";
  19.609 +*)
  19.610  val zero_less_mult_pos = thm "zero_less_mult_pos";
  19.611  val zero_less_mult_pos2 = thm "zero_less_mult_pos2";
  19.612  val zero_less_mult_iff = thm "zero_less_mult_iff";