# HG changeset patch # User avigad # Date 1121183763 -7200 # Node ID c1b87ef4a1c3119b8d022e2ef51799912249e9c4 # Parent 515b6020cf5d532ef88842bb4ff02bfeb17c40b9 added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy diff -r 515b6020cf5d -r c1b87ef4a1c3 etc/settings --- a/etc/settings Tue Jul 12 12:49:46 2005 +0200 +++ b/etc/settings Tue Jul 12 17:56:03 2005 +0200 @@ -63,7 +63,7 @@ ### Compilation options (cf. isatool usedir) ### -ISABELLE_USEDIR_OPTIONS="-v true" +ISABELLE_USEDIR_OPTIONS="-v true -i true" # Specifically for the HOL image HOL_USEDIR_OPTIONS="" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Finite_Set.thy Tue Jul 12 17:56:03 2005 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/Finite_Set.thy ID: $Id$ Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel - Additions by Jeremy Avigad in Feb 2004 + with contributions by Jeremy Avigad *) header {* Finite sets *} @@ -1137,6 +1137,26 @@ finally show ?thesis . qed +lemma setsum_mono3: "finite B ==> A <= B ==> + ALL x: B - A. + 0 <= ((f x)::'a::{comm_monoid_add,pordered_ab_semigroup_add}) ==> + setsum f A <= setsum f B" + apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)") + apply (erule ssubst) + apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)") + apply simp + apply (rule add_left_mono) + apply (erule setsum_nonneg) + apply (subst setsum_Un_disjoint [THEN sym]) + apply (erule finite_subset, assumption) + apply (rule finite_subset) + prefer 2 + apply assumption + apply auto + apply (rule setsum_cong) + apply auto +done + (* FIXME: this is distributitivty, name as such! *) lemma setsum_mult: @@ -1197,7 +1217,8 @@ case (insert a A) hence "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp also have "\ = \\f a\ + \\a\A. \f a\\\" using insert by simp - also have "\ = \f a\ + \\a\A. \f a\\" by simp + also have "\ = \f a\ + \\a\A. \f a\\" + by (simp del: abs_of_nonneg) also have "\ = (\a\insert a A. \f a\)" using insert by simp finally show ?case . qed diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/HOL.thy Tue Jul 12 17:56:03 2005 +0200 @@ -9,6 +9,7 @@ imports CPure uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML") ("~~/src/Provers/eqsubst.ML") + begin subsection {* Primitive logic *} diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Tue Jul 12 17:56:03 2005 +0200 @@ -429,7 +429,7 @@ prefer 2 apply simp apply (erule_tac [!] V= "\x'. x' ~= x & \x' + - x\ < s --> ?P x'" in thin_rl) apply (drule_tac x = v in spec, simp add: times_divide_eq) -apply (drule_tac x = u in spec, auto, arith) +apply (drule_tac x = u in spec, auto) apply (subgoal_tac "\f u - f x - f' x * (u - x)\ = \f x - f u - f' x * (x - u)\") apply (rule order_trans) apply (auto simp add: abs_le_interval_iff) diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Jul 12 17:56:03 2005 +0200 @@ -600,7 +600,7 @@ apply (drule lemma_odd_mod_4_div_2) apply (simp add: numeral_2_eq_2 divide_inverse) apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono - simp add: est mult_pos_le mult_ac divide_inverse + simp add: est mult_nonneg_nonneg mult_ac divide_inverse power_abs [symmetric]) done qed diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Tue Jul 12 17:56:03 2005 +0200 @@ -1393,7 +1393,7 @@ apply (simp add: Infinitesimal_approx_hrabs) apply (rule linorder_cases [of 0 x]) apply (frule lemma_approx_gt_zero [of x y]) -apply (auto simp add: lemma_approx_less_zero [of x y]) +apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg) done lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue Jul 12 17:56:03 2005 +0200 @@ -115,7 +115,7 @@ lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" apply (simp (no_asm) add: right_distrib) apply (rule add_less_cancel_left [of "-r", THEN iffD1]) -apply (auto intro: mult_pos +apply (auto intro: mult_pos_pos simp add: add_assoc [symmetric] neg_less_0_iff_less) done diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Tue Jul 12 17:56:03 2005 +0200 @@ -592,7 +592,7 @@ apply (subgoal_tac "summable (%n. \diffs (diffs c) n\ * (r ^ n))") apply (rule_tac [2] x = K in powser_insidea, auto) apply (subgoal_tac [2] "\r\ = r", auto) -apply (rule_tac [2] y1 = "\x\" in order_trans [THEN abs_eq], auto) +apply (rule_tac [2] y1 = "\x\" in order_trans [THEN abs_of_nonneg], auto) apply (simp add: diffs_def mult_assoc [symmetric]) apply (subgoal_tac "\n. real (Suc n) * real (Suc (Suc n)) * \c (Suc (Suc n))\ * (r ^ n) @@ -2418,7 +2418,7 @@ lemma real_sqrt_ge_abs1 [simp]: "\x\ \ sqrt (x\ + y\)" apply (rule_tac n = 1 in realpow_increasing) -apply (auto simp add: numeral_2_eq_2 [symmetric]) +apply (auto simp add: numeral_2_eq_2 [symmetric] power2_abs) done lemma real_sqrt_ge_abs2 [simp]: "\y\ \ sqrt (x\ + y\)" @@ -2463,7 +2463,7 @@ apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono) done -declare real_sqrt_sum_squares_ge_zero [THEN abs_eq, simp] +declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp] subsection{*A Few Theorems Involving Ln, Derivatives, etc.*} diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Import/HOL/arithmetic.imp --- a/src/HOL/Import/HOL/arithmetic.imp Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Import/HOL/arithmetic.imp Tue Jul 12 17:56:03 2005 +0200 @@ -162,7 +162,7 @@ "LESS_OR" > "Nat.Suc_leI" "LESS_NOT_SUC" > "HOL4Base.arithmetic.LESS_NOT_SUC" "LESS_MULT_MONO" > "Nat.Suc_mult_less_cancel1" - "LESS_MULT2" > "Ring_and_Field.mult_pos" + "LESS_MULT2" > "Ring_and_Field.mult_pos_pos" "LESS_MONO_REV" > "Nat.Suc_less_SucD" "LESS_MONO_MULT" > "Nat.mult_le_mono1" "LESS_MONO_EQ" > "Nat.Suc_less_eq" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Import/HOL/real.imp --- a/src/HOL/Import/HOL/real.imp Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Import/HOL/real.imp Tue Jul 12 17:56:03 2005 +0200 @@ -160,7 +160,7 @@ "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less" "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE" "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'" - "REAL_LT_MUL" > "Ring_and_Field.mult_pos" + "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono" "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0" "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL" @@ -217,7 +217,7 @@ "REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le" "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le" "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2" - "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le" + "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg" "REAL_LE_LT" > "Orderings.order_le_less" "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff" "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Import/HOL/realax.imp --- a/src/HOL/Import/HOL/realax.imp Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Import/HOL/realax.imp Tue Jul 12 17:56:03 2005 +0200 @@ -98,7 +98,7 @@ "REAL_LT_TRANS" > "Set.basic_trans_rules_21" "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL" "REAL_LT_REFL" > "Orderings.order_less_irrefl" - "REAL_LT_MUL" > "Ring_and_Field.mult_pos" + "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos" "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono" "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2" "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Integ/NatBin.thy Tue Jul 12 17:56:03 2005 +0200 @@ -274,40 +274,49 @@ lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\ = 1" by (simp add: power2_eq_square) +lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x" + apply (subgoal_tac "3 = Suc (Suc (Suc 0))") + apply (erule ssubst) + apply (simp add: power_Suc mult_ac) + apply (unfold nat_number_of_def) + apply (subst nat_eq_iff) + apply simp +done + text{*Squares of literal numerals will be evaluated.*} declare power2_eq_square [of "number_of w", standard, simp] -lemma zero_le_power2 [simp]: "0 \ (a\::'a::{ordered_idom,recpower})" +lemma zero_le_power2: "0 \ (a\::'a::{ordered_idom,recpower})" by (simp add: power2_eq_square zero_le_square) -lemma zero_less_power2 [simp]: +lemma zero_less_power2: "(0 < a\) = (a \ (0::'a::{ordered_idom,recpower}))" by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) -lemma power2_less_0 [simp]: +lemma power2_less_0: fixes a :: "'a::{ordered_idom,recpower}" shows "~ (a\ < 0)" by (force simp add: power2_eq_square mult_less_0_iff) -lemma zero_eq_power2 [simp]: +lemma zero_eq_power2: "(a\ = 0) = (a = (0::'a::{ordered_idom,recpower}))" by (force simp add: power2_eq_square mult_eq_0_iff) -lemma abs_power2 [simp]: +lemma abs_power2: "abs(a\) = (a\::'a::{ordered_idom,recpower})" by (simp add: power2_eq_square abs_mult abs_mult_self) -lemma power2_abs [simp]: +lemma power2_abs: "(abs a)\ = (a\::'a::{ordered_idom,recpower})" by (simp add: power2_eq_square abs_mult_self) -lemma power2_minus [simp]: +lemma power2_minus: "(- a)\ = (a\::'a::{comm_ring_1,recpower})" by (simp add: power2_eq_square) lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" apply (induct "n") -apply (auto simp add: power_Suc power_add) +apply (auto simp add: power_Suc power_add power2_minus) done lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" @@ -320,7 +329,7 @@ "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)" by (simp add: power_minus1_even power_minus [of a]) -lemma zero_le_even_power: +lemma zero_le_even_power': "0 \ (a::'a::{ordered_idom,recpower}) ^ (2*n)" proof (induct "n") case 0 @@ -343,7 +352,7 @@ have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" by (simp add: mult_ac power_add power2_eq_square Power.power_Suc) thus ?case - by (simp add: prems mult_less_0_iff mult_neg) + by (simp add: prems mult_less_0_iff mult_neg_neg) qed lemma odd_0_le_power_imp_0_le: @@ -758,7 +767,7 @@ val power2_minus = thm "power2_minus"; val power_minus1_even = thm "power_minus1_even"; val power_minus_even = thm "power_minus_even"; -val zero_le_even_power = thm "zero_le_even_power"; +(* val zero_le_even_power = thm "zero_le_even_power"; *) val odd_power_less_zero = thm "odd_power_less_zero"; val odd_0_le_power_imp_0_le = thm "odd_0_le_power_imp_0_le"; @@ -815,7 +824,7 @@ val nat_mult_div_cancel_disj = thm"nat_mult_div_cancel_disj"; val power_minus_even = thm"power_minus_even"; -val zero_le_even_power = thm"zero_le_even_power"; +(* val zero_le_even_power = thm"zero_le_even_power"; *) *} end diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Integ/NatSimprocs.thy --- a/src/HOL/Integ/NatSimprocs.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Integ/NatSimprocs.thy Tue Jul 12 17:56:03 2005 +0200 @@ -243,28 +243,6 @@ lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] -text{*Simplify quotients that are compared with the value 1.*} - -lemma le_divide_eq_1: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" -by (auto simp add: le_divide_eq) - -lemma divide_le_eq_1: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" -by (auto simp add: divide_le_eq) - -lemma less_divide_eq_1: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" -by (auto simp add: less_divide_eq) - -lemma divide_less_eq_1: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" -by (auto simp add: divide_less_eq) - text{*Not good as automatic simprules because they cause case splits.*} lemmas divide_const_simps = @@ -272,55 +250,6 @@ divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 - -subsection{*Conditional Simplification Rules: No Case Splits*} - -lemma le_divide_eq_1_pos [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "0 < a \ (1 \ b / a) = (a \ b)" -by (auto simp add: le_divide_eq) - -lemma le_divide_eq_1_neg [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "a < 0 \ (1 \ b / a) = (b \ a)" -by (auto simp add: le_divide_eq) - -lemma divide_le_eq_1_pos [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "0 < a \ (b / a \ 1) = (b \ a)" -by (auto simp add: divide_le_eq) - -lemma divide_le_eq_1_neg [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "a < 0 \ (b / a \ 1) = (a \ b)" -by (auto simp add: divide_le_eq) - -lemma less_divide_eq_1_pos [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "0 < a \ (1 < b / a) = (a < b)" -by (auto simp add: less_divide_eq) - -lemma less_divide_eq_1_neg [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "a < 0 \ (1 < b / a) = (b < a)" -by (auto simp add: less_divide_eq) - -lemma divide_less_eq_1_pos [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "0 < a \ (b / a < 1) = (b < a)" -by (auto simp add: divide_less_eq) - -lemma eq_divide_eq_1 [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(1 = b / a) = ((a \ 0 & a = b))" -by (auto simp add: eq_divide_eq) - -lemma divide_eq_eq_1 [simp]: - fixes a :: "'a :: {ordered_field,division_by_zero}" - shows "(b / a = 1) = ((a \ 0 & a = b))" -by (auto simp add: divide_eq_eq) - - subsubsection{*Division By @{term "-1"}*} lemma divide_minus1 [simp]: @@ -337,9 +266,6 @@ lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp] - - - ML {* val divide_minus1 = thm "divide_minus1"; diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Integ/Parity.thy --- a/src/HOL/Integ/Parity.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Integ/Parity.thy Tue Jul 12 17:56:03 2005 +0200 @@ -152,9 +152,6 @@ lemma even_nat_Suc: "even (Suc x) = odd x" by (simp add: even_nat_def) -text{*Compatibility, in case Avigad uses this*} -lemmas even_nat_suc = even_nat_Suc - lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)" by (simp add: even_nat_def int_power) @@ -225,7 +222,25 @@ apply (erule odd_nat_div_two_times_two_plus_one [THEN sym], auto) done -subsection {* Powers of negative one *} +subsection {* Parity and powers *} + +lemma minus_one_even_odd_power: + "(even x --> (- 1::'a::{comm_ring_1,recpower})^x = 1) & + (odd x --> (- 1::'a)^x = - 1)" + apply (induct x) + apply (rule conjI) + apply simp + apply (insert even_nat_zero, blast) + apply (simp add: power_Suc) +done + +lemma minus_one_even_power [simp]: + "even x ==> (- 1::'a::{comm_ring_1,recpower})^x = 1" + by (rule minus_one_even_odd_power [THEN conjunct1, THEN mp], assumption) + +lemma minus_one_odd_power [simp]: + "odd x ==> (- 1::'a::{comm_ring_1,recpower})^x = - 1" + by (rule minus_one_even_odd_power [THEN conjunct2, THEN mp], assumption) lemma neg_one_even_odd_power: "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & @@ -247,6 +262,119 @@ (if even n then (x ^ n) else -(x ^ n))" by (induct n, simp_all split: split_if_asm add: power_Suc) +lemma zero_le_even_power: "even n ==> + 0 <= (x::'a::{recpower,ordered_ring_strict}) ^ n" + apply (simp add: even_nat_equiv_def2) + apply (erule exE) + apply (erule ssubst) + apply (subst power_add) + apply (rule zero_le_square) + done + +lemma zero_le_odd_power: "odd n ==> + (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)" + apply (simp add: odd_nat_equiv_def2) + apply (erule exE) + apply (erule ssubst) + apply (subst power_Suc) + apply (subst power_add) + apply (subst zero_le_mult_iff) + apply auto + apply (subgoal_tac "x = 0 & 0 < y") + apply (erule conjE, assumption) + apply (subst power_eq_0_iff [THEN sym]) + apply (subgoal_tac "0 <= x^y * x^y") + apply simp + apply (rule zero_le_square)+ +done + +lemma zero_le_power_eq: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) = + (even n | (odd n & 0 <= x))" + apply auto + apply (subst zero_le_odd_power [THEN sym]) + apply assumption+ + apply (erule zero_le_even_power) + apply (subst zero_le_odd_power) + apply assumption+ +done + +lemma zero_less_power_eq: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) = + (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" + apply (rule iffI) + apply clarsimp + apply (rule conjI) + apply clarsimp + apply (rule ccontr) + apply (subgoal_tac "~ (0 <= x^n)") + apply simp + apply (subst zero_le_odd_power) + apply assumption + apply simp + apply (rule notI) + apply (simp add: power_0_left) + apply (rule notI) + apply (simp add: power_0_left) + apply auto + apply (subgoal_tac "0 <= x^n") + apply (frule order_le_imp_less_or_eq) + apply simp + apply (erule zero_le_even_power) + apply (subgoal_tac "0 <= x^n") + apply (frule order_le_imp_less_or_eq) + apply auto + apply (subst zero_le_odd_power) + apply assumption + apply (erule order_less_imp_le) +done + +lemma power_less_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n < 0) = + (odd n & x < 0)" + apply (subst linorder_not_le [THEN sym])+ + apply (subst zero_le_power_eq) + apply auto +done + +lemma power_le_zero_eq: "((x::'a::{recpower,ordered_idom}) ^ n <= 0) = + (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" + apply (subst linorder_not_less [THEN sym])+ + apply (subst zero_less_power_eq) + apply auto +done + +lemma power_even_abs: "even n ==> + (abs (x::'a::{recpower,ordered_idom}))^n = x^n" + apply (subst power_abs [THEN sym]) + apply (simp add: zero_le_even_power) +done + +lemma zero_less_power_nat_eq: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" + apply (induct n) + apply simp + apply auto +done + +lemma power_minus_even [simp]: "even n ==> + (- x)^n = (x^n::'a::{recpower,comm_ring_1})" + apply (subst power_minus) + apply simp +done + +lemma power_minus_odd [simp]: "odd n ==> + (- x)^n = - (x^n::'a::{recpower,comm_ring_1})" + apply (subst power_minus) + apply simp +done + +(* Simplify, when the exponent is a numeral *) + +declare power_0_left [of "number_of w", standard, simp] +declare zero_le_power_eq [of _ "number_of w", standard, simp] +declare zero_less_power_eq [of _ "number_of w", standard, simp] +declare power_le_zero_eq [of _ "number_of w", standard, simp] +declare power_less_zero_eq [of _ "number_of w", standard, simp] +declare zero_less_power_nat_eq [of _ "number_of w", standard, simp] +declare power_eq_0_iff [of _ "number_of w", standard, simp] +declare power_even_abs [of "number_of w" _, standard, simp] subsection {* An Equivalence for @{term "0 \ a^n"} *} diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/NumberTheory/Gauss.thy --- a/src/HOL/NumberTheory/Gauss.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/NumberTheory/Gauss.thy Tue Jul 12 17:56:03 2005 +0200 @@ -180,7 +180,7 @@ lemma (in GAUSS) B_greater_zero: "x \ B ==> 0 < x"; apply (insert a_nonzero) -by (auto simp add: B_def mult_pos A_greater_zero) +by (auto simp add: B_def mult_pos_pos A_greater_zero) lemma (in GAUSS) C_ncong_p: "x \ C ==> ~[x = 0](mod p)"; apply (auto simp add: C_def) @@ -505,4 +505,4 @@ by (auto simp add: p_g_2 one_not_neg_one_mod_m zcong_sym) qed -end \ No newline at end of file +end diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/OrderedGroup.thy Tue Jul 12 17:56:03 2005 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/OrderedGroup.thy ID: $Id$ - Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel + Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel, + with contributions by Jeremy Avigad *) header {* Ordered Groups *} @@ -466,6 +467,72 @@ diff_less_eq less_diff_eq diff_le_eq le_diff_eq diff_eq_eq eq_diff_eq +subsection {* Support for reasoning about signs *} + +lemma add_pos_pos: "0 < + (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) + ==> 0 < y ==> 0 < x + y" +apply (subgoal_tac "0 + 0 < x + y") +apply simp +apply (erule add_less_le_mono) +apply (erule order_less_imp_le) +done + +lemma add_pos_nonneg: "0 < + (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) + ==> 0 <= y ==> 0 < x + y" +apply (subgoal_tac "0 + 0 < x + y") +apply simp +apply (erule add_less_le_mono, assumption) +done + +lemma add_nonneg_pos: "0 <= + (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) + ==> 0 < y ==> 0 < x + y" +apply (subgoal_tac "0 + 0 < x + y") +apply simp +apply (erule add_le_less_mono, assumption) +done + +lemma add_nonneg_nonneg: "0 <= + (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) + ==> 0 <= y ==> 0 <= x + y" +apply (subgoal_tac "0 + 0 <= x + y") +apply simp +apply (erule add_mono, assumption) +done + +lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) + < 0 ==> y < 0 ==> x + y < 0" +apply (subgoal_tac "x + y < 0 + 0") +apply simp +apply (erule add_less_le_mono) +apply (erule order_less_imp_le) +done + +lemma add_neg_nonpos: + "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0 + ==> y <= 0 ==> x + y < 0" +apply (subgoal_tac "x + y < 0 + 0") +apply simp +apply (erule add_less_le_mono, assumption) +done + +lemma add_nonpos_neg: + "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 + ==> y < 0 ==> x + y < 0" +apply (subgoal_tac "x + y < 0 + 0") +apply simp +apply (erule add_le_less_mono, assumption) +done + +lemma add_nonpos_nonpos: + "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 + ==> y <= 0 ==> x + y <= 0" +apply (subgoal_tac "x + y <= 0 + 0") +apply simp +apply (erule add_mono, assumption) +done subsection{*Lemmas for the @{text cancel_numerals} simproc*} @@ -702,16 +769,6 @@ show ?thesis by (simp add: abs_lattice join_eq_if) qed -lemma abs_eq [simp]: - fixes a :: "'a::{lordered_ab_group_abs, linorder}" - shows "0 \ a ==> abs a = a" -by (simp add: abs_if_lattice linorder_not_less [symmetric]) - -lemma abs_minus_eq [simp]: - fixes a :: "'a::{lordered_ab_group_abs, linorder}" - shows "a < 0 ==> abs a = -a" -by (simp add: abs_if_lattice linorder_not_less [symmetric]) - lemma abs_ge_zero[simp]: "0 \ abs (a::'a::lordered_ab_group_abs)" proof - have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le) @@ -800,12 +857,19 @@ lemma iff2imp: "(A=B) \ (A \ B)" by (simp) -lemma imp_abs_id: "0 \ a \ abs a = (a::'a::lordered_ab_group_abs)" +lemma abs_of_nonneg [simp]: "0 \ a \ abs a = (a::'a::lordered_ab_group_abs)" by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts) -lemma imp_abs_neg_id: "a \ 0 \ abs a = -(a::'a::lordered_ab_group_abs)" +lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x"; +by (rule abs_of_nonneg, rule order_less_imp_le); + +lemma abs_of_nonpos [simp]: "a \ 0 \ abs a = -(a::'a::lordered_ab_group_abs)" by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts) +lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) < 0 ==> + abs x = - x" +by (rule abs_of_nonpos, rule order_less_imp_le) + lemma abs_leI: "[|a \ b; -a \ b|] ==> abs a \ (b::'a::lordered_ab_group_abs)" by (simp add: abs_lattice join_imp_le) @@ -847,6 +911,36 @@ with g[symmetric] show ?thesis by simp qed +lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) - + abs b <= abs (a - b)" + apply (simp add: compare_rls) + apply (subgoal_tac "abs a = abs (a - b + b)") + apply (erule ssubst) + apply (rule abs_triangle_ineq) + apply (rule arg_cong);back; + apply (simp add: compare_rls) +done + +lemma abs_triangle_ineq3: + "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)" + apply (subst abs_le_iff) + apply auto + apply (rule abs_triangle_ineq2) + apply (subst abs_minus_commute) + apply (rule abs_triangle_ineq2) +done + +lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <= + abs a + abs b" +proof -; + have "abs(a - b) = abs(a + - b)" + by (subst diff_minus, rule refl) + also have "... <= abs a + abs (- b)" + by (rule abs_triangle_ineq) + finally show ?thesis + by simp +qed + lemma abs_diff_triangle_ineq: "\(a::'a::lordered_ab_group_abs) + b - (c+d)\ \ \a-c\ + \b-d\" proof - @@ -927,14 +1021,6 @@ show ?thesis by (rule le_add_right_mono[OF 2 3]) qed -lemma abs_of_ge_0: "0 <= (y::'a::lordered_ab_group_abs) \ abs y = y" -proof - - assume 1:"0 <= y" - have 2:"-y <= 0" by (simp add: 1) - from 1 2 have 3:"-y <= y" by (simp only:) - show ?thesis by (simp add: abs_lattice ge_imp_join_eq[OF 3]) -qed - ML {* val add_zero_left = thm"add_0"; val add_zero_right = thm"add_0_right"; @@ -1068,8 +1154,8 @@ val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id"; val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id"; val iff2imp = thm "iff2imp"; -val imp_abs_id = thm "imp_abs_id"; -val imp_abs_neg_id = thm "imp_abs_neg_id"; +(* val imp_abs_id = thm "imp_abs_id"; +val imp_abs_neg_id = thm "imp_abs_neg_id"; *) val abs_leI = thm "abs_leI"; val le_minus_self_iff = thm "le_minus_self_iff"; val minus_le_self_iff = thm "minus_le_self_iff"; diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Power.thy --- a/src/HOL/Power.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Power.thy Tue Jul 12 17:56:03 2005 +0200 @@ -50,7 +50,7 @@ lemma zero_less_power: "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" apply (induct "n") -apply (simp_all add: power_Suc zero_less_one mult_pos) +apply (simp_all add: power_Suc zero_less_one mult_pos_pos) done lemma zero_le_power: @@ -165,6 +165,12 @@ apply (auto simp add: power_Suc inverse_mult_distrib) done +lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n = + (1 / a)^n" +apply (simp add: divide_inverse) +apply (rule power_inverse) +done + lemma nonzero_power_divide: "b \ 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)" by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse) diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Real/PReal.thy Tue Jul 12 17:56:03 2005 +0200 @@ -372,7 +372,7 @@ obtain y where [simp]: "0 < y" "y \ B" by blast show ?thesis proof (intro exI conjI) - show "0 < x*y" by (simp add: mult_pos) + show "0 < x*y" by (simp add: mult_pos_pos) show "x * y \ mult_set A B" proof - { fix u::rat and v::rat @@ -398,7 +398,7 @@ proof show "mult_set A B \ {r. 0 < r}" by (force simp add: mult_set_def - intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos) + intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos) next show "mult_set A B \ {r. 0 < r}" by (insert preal_not_mem_mult_set_Ex [OF A B], blast) @@ -491,7 +491,8 @@ have vpos: "0 A" - by (force intro: preal_downwards_closed [OF A v] mult_pos upos vpos) + by (force intro: preal_downwards_closed [OF A v] mult_pos_pos + upos vpos) qed next show "A \ ?lhs" diff -r 515b6020cf5d -r c1b87ef4a1c3 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Tue Jul 12 12:49:46 2005 +0200 +++ b/src/HOL/Ring_and_Field.thy Tue Jul 12 17:56:03 2005 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/Ring_and_Field.thy ID: $Id$ - Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel + Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel, + with contributions by Jeremy Avigad *) header {* (Ordered) Rings and Fields *} @@ -330,28 +331,28 @@ subsection{* Products of Signs *} -lemma mult_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b" +lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b" by (drule mult_strict_left_mono [of 0 b], auto) -lemma mult_pos_le: "[| (0::'a::pordered_cancel_semiring) \ a; 0 \ b |] ==> 0 \ a*b" +lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \ a; 0 \ b |] ==> 0 \ a*b" by (drule mult_left_mono [of 0 b], auto) lemma mult_pos_neg: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> a*b < 0" by (drule mult_strict_left_mono [of b 0], auto) -lemma mult_pos_neg_le: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> a*b \ 0" +lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> a*b \ 0" by (drule mult_left_mono [of b 0], auto) lemma mult_pos_neg2: "[| (0::'a::ordered_semiring_strict) < a; b < 0 |] ==> b*a < 0" by (drule mult_strict_right_mono[of b 0], auto) -lemma mult_pos_neg2_le: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> b*a \ 0" +lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \ a; b \ 0 |] ==> b*a \ 0" by (drule mult_right_mono[of b 0], auto) -lemma mult_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b" +lemma mult_neg_neg: "[| a < (0::'a::ordered_ring_strict); b < 0 |] ==> 0 < a*b" by (drule mult_strict_right_mono_neg, auto) -lemma mult_neg_le: "[| a \ (0::'a::pordered_ring); b \ 0 |] ==> 0 \ a*b" +lemma mult_nonpos_nonpos: "[| a \ (0::'a::pordered_ring); b \ 0 |] ==> 0 \ a*b" by (drule mult_right_mono_neg[of a 0 b ], auto) lemma zero_less_mult_pos: @@ -372,7 +373,8 @@ lemma zero_less_mult_iff: "((0::'a::ordered_ring_strict) < a*b) = (0 < a & 0 < b | a < 0 & b < 0)" -apply (auto simp add: order_le_less linorder_not_less mult_pos mult_neg) +apply (auto simp add: order_le_less linorder_not_less mult_pos_pos + mult_neg_neg) apply (blast dest: zero_less_mult_pos) apply (blast dest: zero_less_mult_pos2) done @@ -403,10 +405,10 @@ done lemma split_mult_pos_le: "(0 \ a & 0 \ b) | (a \ 0 & b \ 0) \ 0 \ a * (b::_::pordered_ring)" -by (auto simp add: mult_pos_le mult_neg_le) +by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) lemma split_mult_neg_le: "(0 \ a & b \ 0) | (a \ 0 & 0 \ b) \ a * b \ (0::_::pordered_cancel_semiring)" -by (auto simp add: mult_pos_neg_le mult_pos_neg2_le) +by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) lemma zero_le_square: "(0::'a::ordered_ring_strict) \ a*a" by (simp add: zero_le_mult_iff linorder_linear) @@ -444,7 +446,7 @@ lemma mult_strict_mono: "[|ac|] ==> a * c < b * (d::'a::ordered_semiring_strict)" apply (case_tac "c=0") - apply (simp add: mult_pos) + apply (simp add: mult_pos_pos) apply (erule mult_strict_right_mono [THEN order_less_trans]) apply (force simp add: order_le_less) apply (erule mult_strict_left_mono, assumption) @@ -469,6 +471,26 @@ apply (simp add: order_less_trans [OF zero_less_one]) done +lemma mult_less_le_imp_less: "(a::'a::ordered_semiring_strict) < b ==> + c <= d ==> 0 <= a ==> 0 < c ==> a * c < b * d" + apply (subgoal_tac "a * c < b * c") + apply (erule order_less_le_trans) + apply (erule mult_left_mono) + apply simp + apply (erule mult_strict_right_mono) + apply assumption +done + +lemma mult_le_less_imp_less: "(a::'a::ordered_semiring_strict) <= b ==> + c < d ==> 0 < a ==> 0 <= c ==> a * c < b * d" + apply (subgoal_tac "a * c <= b * c") + apply (erule order_le_less_trans) + apply (erule mult_strict_left_mono) + apply simp + apply (erule mult_right_mono) + apply simp +done + subsection{*Cancellation Laws for Relationships With a Common Factor*} text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, @@ -774,7 +796,7 @@ qed lemma inverse_minus_eq [simp]: - "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"; + "inverse(-a) = -inverse(a::'a::{field,division_by_zero})" proof cases assume "a=0" thus ?thesis by (simp add: inverse_zero) next @@ -882,6 +904,8 @@ "inverse (a/b) = b / (a::'a::{field,division_by_zero})" by (simp add: divide_inverse mult_commute) +subsection {* Calculations with fractions *} + lemma nonzero_mult_divide_cancel_left: assumes [simp]: "b\0" and [simp]: "c\0" shows "(c*a)/(c*b) = a/(b::'a::field)" @@ -936,6 +960,19 @@ "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)" by (simp add: divide_inverse mult_assoc) +lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> + x / y + w / z = (x * z + w * y) / (y * z)" + apply (subgoal_tac "x / y = (x * z) / (y * z)") + apply (erule ssubst) + apply (subgoal_tac "w / z = (w * y) / (y * z)") + apply (erule ssubst) + apply (rule add_divide_distrib [THEN sym]) + apply (subst mult_commute) + apply (erule nonzero_mult_divide_cancel_left [THEN sym]) + apply assumption + apply (erule nonzero_mult_divide_cancel_right [THEN sym]) + apply assumption +done subsubsection{*Special Cancellation Simprules for Division*} @@ -1025,6 +1062,13 @@ lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c" by (simp add: diff_minus add_divide_distrib) +lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> + x / y - w / z = (x * z - w * y) / (y * z)" + apply (subst diff_def)+ + apply (subst minus_divide_left) + apply (subst add_frac_eq) + apply simp_all +done subsection {* Ordered Fields *} @@ -1224,33 +1268,6 @@ "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{ordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) - -subsection{*Division and Signs*} - -lemma zero_less_divide_iff: - "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" -by (simp add: divide_inverse zero_less_mult_iff) - -lemma divide_less_0_iff: - "(a/b < (0::'a::{ordered_field,division_by_zero})) = - (0 < a & b < 0 | a < 0 & 0 < b)" -by (simp add: divide_inverse mult_less_0_iff) - -lemma zero_le_divide_iff: - "((0::'a::{ordered_field,division_by_zero}) \ a/b) = - (0 \ a & 0 \ b | a \ 0 & b \ 0)" -by (simp add: divide_inverse zero_le_mult_iff) - -lemma divide_le_0_iff: - "(a/b \ (0::'a::{ordered_field,division_by_zero})) = - (0 \ a & b \ 0 | a \ 0 & 0 \ b)" -by (simp add: divide_inverse mult_le_0_iff) - -lemma divide_eq_0_iff [simp]: - "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" -by (simp add: divide_inverse field_mult_eq_0_iff) - - subsection{*Simplification of Inequalities Involving Literal Divisors*} lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \ b/c) = (a*c \ b)" @@ -1263,7 +1280,6 @@ finally show ?thesis . qed - lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \ b/c) = (b \ a*c)" proof - assume less: "c<0" @@ -1312,7 +1328,6 @@ apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff) done - lemma pos_less_divide_eq: "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)" proof - @@ -1403,6 +1418,99 @@ "(b/c = (a::'a::{field,division_by_zero})) = (if c\0 then b = a*c else a=0)" by (force simp add: nonzero_divide_eq_eq) +lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> + b = a * c ==> b / c = a" + by (subst divide_eq_eq, simp) + +lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==> + a * c = b ==> a = b / c" + by (subst eq_divide_eq, simp) + +lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==> + (x / y = w / z) = (x * z = w * y)" + apply (subst nonzero_eq_divide_eq) + apply assumption + apply (subst times_divide_eq_left) + apply (erule nonzero_divide_eq_eq) +done + +subsection{*Division and Signs*} + +lemma zero_less_divide_iff: + "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)" +by (simp add: divide_inverse zero_less_mult_iff) + +lemma divide_less_0_iff: + "(a/b < (0::'a::{ordered_field,division_by_zero})) = + (0 < a & b < 0 | a < 0 & 0 < b)" +by (simp add: divide_inverse mult_less_0_iff) + +lemma zero_le_divide_iff: + "((0::'a::{ordered_field,division_by_zero}) \ a/b) = + (0 \ a & 0 \ b | a \ 0 & b \ 0)" +by (simp add: divide_inverse zero_le_mult_iff) + +lemma divide_le_0_iff: + "(a/b \ (0::'a::{ordered_field,division_by_zero})) = + (0 \ a & b \ 0 | a \ 0 & 0 \ b)" +by (simp add: divide_inverse mult_le_0_iff) + +lemma divide_eq_0_iff [simp]: + "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))" +by (simp add: divide_inverse field_mult_eq_0_iff) + +lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==> + 0 < y ==> 0 < x / y" + apply (subst pos_less_divide_eq) + apply assumption + apply simp +done + +lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==> + 0 <= x / y" + apply (subst pos_le_divide_eq) + apply assumption + apply simp +done + +lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0" + apply (subst pos_divide_less_eq) + apply assumption + apply simp +done + +lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==> + 0 < y ==> x / y <= 0" + apply (subst pos_divide_le_eq) + apply assumption + apply simp +done + +lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0" + apply (subst neg_divide_less_eq) + apply assumption + apply simp +done + +lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==> + y < 0 ==> x / y <= 0" + apply (subst neg_divide_le_eq) + apply assumption + apply simp +done + +lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y" + apply (subst neg_less_divide_eq) + apply assumption + apply simp +done + +lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==> + 0 <= x / y" + apply (subst neg_le_divide_eq) + apply assumption + apply simp +done subsection{*Cancellation Laws for Division*} @@ -1427,7 +1535,6 @@ apply (simp add: right_inverse_eq) done - lemma one_eq_divide_iff [simp]: "(1 = a/b) = (b \ 0 & a = (b::'a::{field,division_by_zero}))" by (simp add: eq_commute [of 1]) @@ -1451,7 +1558,6 @@ declare zero_le_divide_iff [of "1", simp] declare divide_le_0_iff [of "1", simp] - subsection {* Ordering Rules for Division *} lemma divide_strict_right_mono: @@ -1463,6 +1569,17 @@ "[|a \ b; 0 \ c|] ==> a/c \ b/(c::'a::{ordered_field,division_by_zero})" by (force simp add: divide_strict_right_mono order_le_less) +lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b + ==> c <= 0 ==> b / c <= a / c" + apply (drule divide_right_mono [of _ _ "- c"]) + apply auto +done + +lemma divide_strict_right_mono_neg: + "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)" +apply (drule divide_strict_right_mono [of _ _ "-c"], simp) +apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) +done text{*The last premise ensures that @{term a} and @{term b} have the same sign*} @@ -1481,6 +1598,12 @@ apply (force simp add: divide_strict_left_mono order_le_less) done +lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b + ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" + apply (drule divide_left_mono [of _ _ "- c"]) + apply (auto simp add: mult_commute) +done + lemma divide_strict_left_mono_neg: "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)" apply (subgoal_tac "a \ 0 & b \ 0") @@ -1490,12 +1613,139 @@ apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) done -lemma divide_strict_right_mono_neg: - "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)" -apply (drule divide_strict_right_mono [of _ _ "-c"], simp) -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) +text{*Simplify quotients that are compared with the value 1.*} + +lemma le_divide_eq_1: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(1 \ b / a) = ((0 < a & a \ b) | (a < 0 & b \ a))" +by (auto simp add: le_divide_eq) + +lemma divide_le_eq_1: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(b / a \ 1) = ((0 < a & b \ a) | (a < 0 & a \ b) | a=0)" +by (auto simp add: divide_le_eq) + +lemma less_divide_eq_1: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" +by (auto simp add: less_divide_eq) + +lemma divide_less_eq_1: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" +by (auto simp add: divide_less_eq) + +subsection{*Conditional Simplification Rules: No Case Splits*} + +lemma le_divide_eq_1_pos [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "0 < a \ (1 \ b / a) = (a \ b)" +by (auto simp add: le_divide_eq) + +lemma le_divide_eq_1_neg [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "a < 0 \ (1 \ b / a) = (b \ a)" +by (auto simp add: le_divide_eq) + +lemma divide_le_eq_1_pos [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "0 < a \ (b / a \ 1) = (b \ a)" +by (auto simp add: divide_le_eq) + +lemma divide_le_eq_1_neg [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "a < 0 \ (b / a \ 1) = (a \ b)" +by (auto simp add: divide_le_eq) + +lemma less_divide_eq_1_pos [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "0 < a \ (1 < b / a) = (a < b)" +by (auto simp add: less_divide_eq) + +lemma less_divide_eq_1_neg [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "a < 0 \ (1 < b / a) = (b < a)" +by (auto simp add: less_divide_eq) + +lemma divide_less_eq_1_pos [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "0 < a \ (b / a < 1) = (b < a)" +by (auto simp add: divide_less_eq) + +lemma eq_divide_eq_1 [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(1 = b / a) = ((a \ 0 & a = b))" +by (auto simp add: eq_divide_eq) + +lemma divide_eq_eq_1 [simp]: + fixes a :: "'a :: {ordered_field,division_by_zero}" + shows "(b / a = 1) = ((a \ 0 & a = b))" +by (auto simp add: divide_eq_eq) + +subsection {* Reasoning about inequalities with division *} + +lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 + ==> x * y <= x" + by (auto simp add: mult_compare_simps); + +lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 + ==> y * x <= x" + by (auto simp add: mult_compare_simps); + +lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==> + x / y <= z"; + by (subst pos_divide_le_eq, assumption+); + +lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==> + z <= x / y"; + by (subst pos_le_divide_eq, assumption+) + +lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==> + x / y < z" + by (subst pos_divide_less_eq, assumption+) + +lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==> + z < x / y" + by (subst pos_less_divide_eq, assumption+) + +lemma frac_le: "(0::'a::ordered_field) <= x ==> + x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" + apply (rule mult_imp_div_pos_le) + apply simp; + apply (subst times_divide_eq_left); + apply (rule mult_imp_le_div_pos, assumption) + apply (rule mult_mono) + apply simp_all done +lemma frac_less: "(0::'a::ordered_field) <= x ==> + x < y ==> 0 < w ==> w <= z ==> x / z < y / w" + apply (rule mult_imp_div_pos_less) + apply simp; + apply (subst times_divide_eq_left); + apply (rule mult_imp_less_div_pos, assumption) + apply (erule mult_less_le_imp_less) + apply simp_all +done + +lemma frac_less2: "(0::'a::ordered_field) < x ==> + x <= y ==> 0 < w ==> w < z ==> x / z < y / w" + apply (rule mult_imp_div_pos_less) + apply simp_all + apply (subst times_divide_eq_left); + apply (rule mult_imp_less_div_pos, assumption) + apply (erule mult_le_less_imp_less) + apply simp_all +done + +lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left + +text{*It's not obvious whether these should be simprules or not. + Their effect is to gather terms into one big fraction, like + a*b*c / x*y*z. The rationale for that is unclear, but many proofs + seem to need them.*} + +declare times_divide_eq [simp] subsection {* Ordered Fields are Dense *} @@ -1519,16 +1769,6 @@ by (blast intro!: less_half_sum gt_half_sum) -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left - -text{*It's not obvious whether these should be simprules or not. - Their effect is to gather terms into one big fraction, like - a*b*c / x*y*z. The rationale for that is unclear, but many proofs - seem to need them.*} - -declare times_divide_eq [simp] - - subsection {* Absolute Value *} lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)" @@ -1556,15 +1796,15 @@ apply (simp) apply (rule_tac y="0::'a" in order_trans) apply (rule addm2) - apply (simp_all add: mult_pos_le mult_neg_le) + apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos) apply (rule addm) - apply (simp_all add: mult_pos_le mult_neg_le) + apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos) done have yx: "?y <= ?x" apply (simp add:diff_def) apply (rule_tac y=0 in order_trans) - apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+) - apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+) + apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+) + apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+) done have i1: "a*b <= abs a * abs b" by (simp only: a b yx) have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy) @@ -1600,8 +1840,8 @@ ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id]) - apply(drule (1) mult_pos_neg_le[of a b], simp) - apply(drule (1) mult_pos_neg2_le[of b a], simp) + apply(drule (1) mult_nonneg_nonpos[of a b], simp) + apply(drule (1) mult_nonneg_nonpos2[of b a], simp) done next assume "~(0 <= a*b)" @@ -1610,8 +1850,8 @@ apply (simp_all add: mulprts abs_prts) apply (insert prems) apply (auto simp add: ring_eq_simps) - apply(drule (1) mult_pos_le[of a b],simp) - apply(drule (1) mult_neg_le[of a b],simp) + apply(drule (1) mult_nonneg_nonneg[of a b],simp) + apply(drule (1) mult_nonpos_nonpos[of a b],simp) done qed qed @@ -1667,6 +1907,20 @@ apply (simp add: le_minus_self_iff linorder_neq_iff) done +lemma abs_mult_pos: "(0::'a::ordered_idom) <= x ==> + (abs y) * x = abs (y * x)"; + apply (subst abs_mult); + apply simp; +done; + +lemma abs_div_pos: "(0::'a::{division_by_zero,ordered_field}) < y ==> + abs x / y = abs (x / y)"; + apply (subst abs_divide); + apply (simp add: order_less_imp_le); +done; + +subsection {* Miscellaneous *} + lemma linprog_dual_estimate: assumes "A * x \ (b::'a::lordered_ring)" @@ -1712,7 +1966,7 @@ by (simp) show ?thesis apply (rule_tac le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"]) - apply (simp_all only: 5 14[simplified abs_of_ge_0[of y, simplified prems]]) + apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]]) done qed @@ -1727,7 +1981,7 @@ have 1: "A - A1 = A + (- A1)" by simp show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems]) qed - then have "abs (A-A1) = A-A1" by (rule abs_of_ge_0) + then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg) with prems show "abs (A-A1) <= (A2-A1)" by simp qed @@ -1856,6 +2110,7 @@ val mult_left_mono_neg = thm "mult_left_mono_neg"; val mult_strict_right_mono_neg = thm "mult_strict_right_mono_neg"; val mult_right_mono_neg = thm "mult_right_mono_neg"; +(* val mult_pos = thm "mult_pos"; val mult_pos_le = thm "mult_pos_le"; val mult_pos_neg = thm "mult_pos_neg"; @@ -1864,6 +2119,7 @@ val mult_pos_neg2_le = thm "mult_pos_neg2_le"; val mult_neg = thm "mult_neg"; val mult_neg_le = thm "mult_neg_le"; +*) val zero_less_mult_pos = thm "zero_less_mult_pos"; val zero_less_mult_pos2 = thm "zero_less_mult_pos2"; val zero_less_mult_iff = thm "zero_less_mult_iff";