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
--- 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=""
--- 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 "\<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
also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp
- also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
+ also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
+ by (simp del: abs_of_nonneg)
also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
finally show ?case .
qed
--- 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 *}
--- 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= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < 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 "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
apply (rule order_trans)
apply (auto simp add: abs_le_interval_iff)
--- 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
--- 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"
--- 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
--- 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. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
apply (rule_tac [2] x = K in powser_insidea, auto)
apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_eq], auto)
+apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
apply (simp add: diffs_def mult_assoc [symmetric])
apply (subgoal_tac
"\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n)
@@ -2418,7 +2418,7 @@
lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
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]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
@@ -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.*}
--- 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"
--- 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"
--- 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"
--- 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})\<twosuperior> = 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 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
+lemma zero_le_power2: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
by (simp add: power2_eq_square zero_le_square)
-lemma zero_less_power2 [simp]:
+lemma zero_less_power2:
"(0 < a\<twosuperior>) = (a \<noteq> (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\<twosuperior> < 0)"
by (force simp add: power2_eq_square mult_less_0_iff)
-lemma zero_eq_power2 [simp]:
+lemma zero_eq_power2:
"(a\<twosuperior> = 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\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
by (simp add: power2_eq_square abs_mult abs_mult_self)
-lemma power2_abs [simp]:
+lemma power2_abs:
"(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
by (simp add: power2_eq_square abs_mult_self)
-lemma power2_minus [simp]:
+lemma power2_minus:
"(- a)\<twosuperior> = (a\<twosuperior>::'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 \<le> (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
--- 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 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
-by (auto simp add: le_divide_eq)
-
-lemma divide_le_eq_1:
- fixes a :: "'a :: {ordered_field,division_by_zero}"
- shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> 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 \<Longrightarrow> (1 \<le> b / a) = (a \<le> 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 \<Longrightarrow> (1 \<le> b / a) = (b \<le> 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 \<Longrightarrow> (b / a \<le> 1) = (b \<le> 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 \<Longrightarrow> (b / a \<le> 1) = (a \<le> 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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<noteq> 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 \<noteq> 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";
--- 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 \<le> a^n"} *}
--- 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 \<in> 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 \<in> 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
--- 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 \<le> 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 \<le> 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) \<Longrightarrow> (A \<Longrightarrow> B)"
by (simp)
-lemma imp_abs_id: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
+lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> 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 \<le> 0 \<Longrightarrow> 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 \<le> 0 \<Longrightarrow> 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 \<le> b; -a \<le> b|] ==> abs a \<le> (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:
"\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
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) \<Longrightarrow> 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";
--- 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 \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
--- 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 \<notin> 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 \<notin> mult_set A B"
proof -
{ fix u::rat and v::rat
@@ -398,7 +398,7 @@
proof
show "mult_set A B \<subseteq> {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 \<noteq> {r. 0 < r}"
by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
@@ -491,7 +491,8 @@
have vpos: "0<v" by (rule preal_imp_pos [OF A v])
hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
thus "u * v \<in> 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 \<subseteq> ?lhs"
--- 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) \<le> a; 0 \<le> b |] ==> 0 \<le> a*b"
+lemma mult_nonneg_nonneg: "[| (0::'a::pordered_cancel_semiring) \<le> a; 0 \<le> b |] ==> 0 \<le> 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) \<le> a; b \<le> 0 |] ==> a*b \<le> 0"
+lemma mult_nonneg_nonpos: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> a*b \<le> 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) \<le> a; b \<le> 0 |] ==> b*a \<le> 0"
+lemma mult_nonneg_nonpos2: "[| (0::'a::pordered_cancel_semiring) \<le> a; b \<le> 0 |] ==> b*a \<le> 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 \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> a*b"
+lemma mult_nonpos_nonpos: "[| a \<le> (0::'a::pordered_ring); b \<le> 0 |] ==> 0 \<le> 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 \<le> a & 0 \<le> b) | (a \<le> 0 & b \<le> 0) \<Longrightarrow> 0 \<le> 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 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> (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) \<le> a*a"
by (simp add: zero_le_mult_iff linorder_linear)
@@ -444,7 +446,7 @@
lemma mult_strict_mono:
"[|a<b; c<d; 0<b; 0\<le>c|] ==> 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\<noteq>0" and [simp]: "c\<noteq>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 \<le> 1) = (x \<le> 0 | 1 \<le> (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}) \<le> a/b) =
- (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse zero_le_mult_iff)
-
-lemma divide_le_0_iff:
- "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
- (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> 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 \<le> b/c) = (a*c \<le> b)"
@@ -1263,7 +1280,6 @@
finally show ?thesis .
qed
-
lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> 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\<noteq>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}) \<le> a/b) =
+ (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
+by (simp add: divide_inverse zero_le_mult_iff)
+
+lemma divide_le_0_iff:
+ "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
+ (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> 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 \<noteq> 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 \<le> b; 0 \<le> c|] ==> a/c \<le> 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 \<noteq> 0 & b \<noteq> 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 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
+by (auto simp add: le_divide_eq)
+
+lemma divide_le_eq_1:
+ fixes a :: "'a :: {ordered_field,division_by_zero}"
+ shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> 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 \<Longrightarrow> (1 \<le> b / a) = (a \<le> 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 \<Longrightarrow> (1 \<le> b / a) = (b \<le> 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 \<Longrightarrow> (b / a \<le> 1) = (b \<le> 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 \<Longrightarrow> (b / a \<le> 1) = (a \<le> 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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<Longrightarrow> (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 \<noteq> 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 \<noteq> 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 \<le> (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";