--- a/doc-src/TutorialI/Types/Numbers.thy Sat Dec 13 09:33:52 2003 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Mon Dec 15 16:38:25 2003 +0100
@@ -200,8 +200,8 @@
@{thm[display] realpow_abs[no_vars]}
\rulename{realpow_abs}
-@{thm[display] real_dense[no_vars]}
-\rulename{real_dense}
+@{thm[display] dense[no_vars]}
+\rulename{dense}
@{thm[display] realpow_abs[no_vars]}
\rulename{realpow_abs}
@@ -218,16 +218,16 @@
@{thm[display] divide_divide_eq_left[no_vars]}
\rulename{divide_divide_eq_left}
-@{thm[display] real_minus_divide_eq[no_vars]}
-\rulename{real_minus_divide_eq}
+@{thm[display] minus_divide_left[no_vars]}
+\rulename{minus_divide_left}
-@{thm[display] real_divide_minus_eq[no_vars]}
-\rulename{real_divide_minus_eq}
+@{thm[display] minus_divide_right[no_vars]}
+\rulename{minus_divide_right}
This last NOT a simprule
-@{thm[display] real_add_divide_distrib[no_vars]}
-\rulename{real_add_divide_distrib}
+@{thm[display] add_divide_distrib[no_vars]}
+\rulename{add_divide_distrib}
*}
lemma "3/4 < (7/8 :: real)"
--- a/doc-src/TutorialI/Types/document/Numbers.tex Sat Dec 13 09:33:52 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Dec 15 16:38:25 2003 +0100
@@ -277,7 +277,7 @@
\rulename{zmod_zmult2_eq}
\begin{isabelle}%
-{\isasymbar}x\ {\isacharasterisk}\ y{\isasymbar}\ {\isacharequal}\ {\isasymbar}x{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}y{\isasymbar}%
+{\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
\end{isabelle}
\rulename{abs_mult}%
\end{isamarkuptext}%
@@ -325,9 +325,9 @@
\rulename{realpow_abs}
\begin{isabelle}%
-x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ x\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ y%
+a\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isasymexists}r{\isachardot}\ a\ {\isacharless}\ r\ {\isasymand}\ r\ {\isacharless}\ b%
\end{isabelle}
-\rulename{real_dense}
+\rulename{dense}
\begin{isabelle}%
{\isasymbar}r\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}r{\isasymbar}\ {\isacharcircum}\ n%
@@ -355,21 +355,21 @@
\rulename{divide_divide_eq_left}
\begin{isabelle}%
-{\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
+{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b%
\end{isabelle}
-\rulename{real_minus_divide_eq}
+\rulename{minus_divide_left}
\begin{isabelle}%
-x\ {\isacharslash}\ {\isacharminus}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
+{\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b%
\end{isabelle}
-\rulename{real_divide_minus_eq}
+\rulename{minus_divide_right}
This last NOT a simprule
\begin{isabelle}%
-{\isacharparenleft}x\ {\isacharplus}\ y{\isacharparenright}\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ z\ {\isacharplus}\ y\ {\isacharslash}\ z%
+{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c%
\end{isabelle}
-\rulename{real_add_divide_distrib}%
+\rulename{add_divide_distrib}%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequote}\isanewline
--- a/doc-src/TutorialI/Types/numerics.tex Sat Dec 13 09:33:52 2003 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Dec 15 16:38:25 2003 +0100
@@ -397,7 +397,7 @@
Density, however, is trivial to express:
\begin{isabelle}
x\ <\ y\ \isasymLongrightarrow \ \isasymexists r.\ x\ <\ r\ \isasymand \ r\ <\ y%
-\rulename{real_dense}
+\rulename{dense}
\end{isabelle}
Here is a selection of rules about the division operator. The following
@@ -417,17 +417,17 @@
Signs are extracted from quotients in the hope that complementary terms can
then be cancelled:
\begin{isabelle}
--\ x\ /\ y\ =\ -\ (x\ /\ y)
-\rulename{real_minus_divide_eq}\isanewline
-x\ /\ -\ y\ =\ -\ (x\ /\ y)
-\rulename{real_divide_minus_eq}
+-\ (a\ /\ b)\ =\ -\ a\ /\ b
+\rulename{minus_divide_left}\isanewline
+-\ (a\ /\ b)\ =\ a\ /\ -\ b
+\rulename{minus_divide_right}
\end{isabelle}
The following distributive law is available, but it is not installed as a
simplification rule.
\begin{isabelle}
-(x\ +\ y)\ /\ z\ =\ x\ /\ z\ +\ y\ /\ z%
-\rulename{real_add_divide_distrib}
+(a\ +\ b)\ /\ c\ =\ a\ /\ c\ +\ b\ /\ c%
+\rulename{add_divide_distrib}
\end{isabelle}
As with the other numeric types, the simplifier can sort the operands of
--- a/src/HOL/HOL.thy Sat Dec 13 09:33:52 2003 +0100
+++ b/src/HOL/HOL.thy Mon Dec 15 16:38:25 2003 +0100
@@ -645,6 +645,9 @@
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50)
+lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
+by blast
+
subsubsection {* Monotonicity *}
locale mono =
@@ -716,6 +719,9 @@
apply (erule contrapos_np, simp)
done
+lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)"
+by (blast intro: order_antisym)
+
text {* Transitivity. *}
--- a/src/HOL/Integ/IntArith.thy Sat Dec 13 09:33:52 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Mon Dec 15 16:38:25 2003 +0100
@@ -93,7 +93,8 @@
but arith_tac is not parameterized by such simp rules
*)
-lemma zabs_split: "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
+lemma zabs_split [arith_split]:
+ "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
by (simp add: zabs_def)
lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
@@ -104,8 +105,6 @@
z is an integer literal.*}
declare int_eq_iff [of _ "number_of v", standard, simp]
-declare zabs_split [arith_split]
-
lemma zabs_eq_iff:
"(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
by (auto simp add: zabs_def)
@@ -113,7 +112,7 @@
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
by simp
-lemma split_nat[arith_split]:
+lemma split_nat [arith_split]:
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
proof (cases "i < 0")
--- a/src/HOL/Real/RealArith.thy Sat Dec 13 09:33:52 2003 +0100
+++ b/src/HOL/Real/RealArith.thy Mon Dec 15 16:38:25 2003 +0100
@@ -76,14 +76,12 @@
subsection{*Absolute Value Function for the Reals*}
-lemma abs_nat_number_of:
+lemma abs_nat_number_of [simp]:
"abs (number_of v :: real) =
(if neg (number_of v) then number_of (bin_minus v)
else number_of v)"
-apply (simp add: real_abs_def bin_arith_simps minus_real_number_of le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff)
-done
-
-declare abs_nat_number_of [simp]
+by (simp add: real_abs_def bin_arith_simps minus_real_number_of
+ le_real_number_of_eq_not_less less_real_number_of real_of_int_le_iff)
(*----------------------------------------------------------------------------
@@ -101,85 +99,30 @@
lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
by (unfold real_abs_def real_le_def, simp)
-lemma abs_mult_inverse: "abs (x * inverse y) = (abs x) * inverse (abs (y::real))"
-by (simp add: abs_mult abs_inverse)
-
-text{*Much easier to prove using arithmetic than abstractly!!*}
-lemma abs_triangle_ineq: "abs(x+y) \<le> abs x + abs (y::real)"
-by (unfold real_abs_def, simp)
-
-(*Unused, but perhaps interesting as an example*)
-lemma abs_triangle_ineq_four: "abs(w + x + y + z) \<le> abs(w) + abs(x) + abs(y) + abs(z::real)"
-by (simp add: abs_triangle_ineq [THEN order_trans])
-
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
by (unfold real_abs_def, simp)
-lemma abs_triangle_minus_ineq: "abs(x + (-y)) \<le> abs x + abs (y::real)"
-by (unfold real_abs_def, simp)
-
-lemma abs_add_less [rule_format (no_asm)]: "abs x < r --> abs y < s --> abs(x+y) < r+(s::real)"
-by (unfold real_abs_def, simp)
-
-lemma abs_add_minus_less:
- "abs x < r --> abs y < s --> abs(x+ (-y)) < r+(s::real)"
-by (unfold real_abs_def, simp)
-
lemma abs_minus_one [simp]: "abs (-1) = (1::real)"
by (unfold real_abs_def, simp)
lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
-by (unfold real_abs_def, auto)
+by (force simp add: Ring_and_Field.abs_less_iff)
lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
-by (unfold real_abs_def, auto)
+by (force simp add: Ring_and_Field.abs_le_iff)
-lemma abs_add_pos_gt_zero: "(0::real) < k ==> 0 < k + abs(x)"
+lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
by (unfold real_abs_def, auto)
-lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
-by (unfold real_abs_def, auto)
-declare abs_add_one_gt_zero [simp]
+lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
+by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
-lemma abs_circle: "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)"
-by (auto intro: abs_triangle_ineq [THEN order_le_less_trans])
-
-lemma abs_real_of_nat_cancel: "abs (real x) = real (x::nat)"
-by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
-declare abs_real_of_nat_cancel [simp]
-
-lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
+lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
apply (rule real_leD)
apply (auto intro: abs_ge_self [THEN order_trans])
done
-declare abs_add_one_not_less_self [simp]
-(* used in vector theory *)
-lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) \<le> abs(w) + abs(x) + abs(y)"
-by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_mono
- simp add: real_add_assoc)
-
-lemma abs_diff_less_imp_gt_zero: "abs(x - y) < y ==> (0::real) < y"
-apply (unfold real_abs_def)
-apply (case_tac "0 \<le> x - y", auto)
-done
-
-lemma abs_diff_less_imp_gt_zero2: "abs(x - y) < x ==> (0::real) < x"
-apply (unfold real_abs_def)
-apply (case_tac "0 \<le> x - y", auto)
-done
-
-lemma abs_diff_less_imp_gt_zero3: "abs(x - y) < y ==> (0::real) < x"
-by (auto simp add: abs_interval_iff)
-
-lemma abs_diff_less_imp_gt_zero4: "abs(x - y) < -y ==> x < (0::real)"
-by (auto simp add: abs_interval_iff)
-
-lemma abs_triangle_ineq_minus_cancel:
- "abs(x) \<le> abs(x + (-y)) + abs((y::real))"
-apply (unfold real_abs_def, auto)
-done
-
+text{*Used only in Hyperreal/Lim.ML*}
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
apply (simp add: real_add_assoc)
apply (rule_tac x1 = y in real_add_left_commute [THEN ssubst])
@@ -220,29 +163,16 @@
val abs_ge_minus_self = thm"abs_ge_minus_self";
val abs_mult = thm"abs_mult";
val abs_inverse = thm"abs_inverse";
-val abs_mult_inverse = thm"abs_mult_inverse";
val abs_triangle_ineq = thm"abs_triangle_ineq";
-val abs_triangle_ineq_four = thm"abs_triangle_ineq_four";
val abs_minus_cancel = thm"abs_minus_cancel";
val abs_minus_add_cancel = thm"abs_minus_add_cancel";
-val abs_triangle_minus_ineq = thm"abs_triangle_minus_ineq";
-val abs_add_less = thm"abs_add_less";
-val abs_add_minus_less = thm"abs_add_minus_less";
val abs_minus_one = thm"abs_minus_one";
val abs_interval_iff = thm"abs_interval_iff";
val abs_le_interval_iff = thm"abs_le_interval_iff";
-val abs_add_pos_gt_zero = thm"abs_add_pos_gt_zero";
val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
-val abs_circle = thm"abs_circle";
val abs_le_zero_iff = thm"abs_le_zero_iff";
val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel";
val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
-val abs_triangle_ineq_three = thm"abs_triangle_ineq_three";
-val abs_diff_less_imp_gt_zero = thm"abs_diff_less_imp_gt_zero";
-val abs_diff_less_imp_gt_zero2 = thm"abs_diff_less_imp_gt_zero2";
-val abs_diff_less_imp_gt_zero3 = thm"abs_diff_less_imp_gt_zero3";
-val abs_diff_less_imp_gt_zero4 = thm"abs_diff_less_imp_gt_zero4";
-val abs_triangle_ineq_minus_cancel = thm"abs_triangle_ineq_minus_cancel";
val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
val abs_mult_less = thm"abs_mult_less";
--- a/src/HOL/Ring_and_Field.thy Sat Dec 13 09:33:52 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Dec 15 16:38:25 2003 +0100
@@ -1434,11 +1434,55 @@
apply (simp add: nonzero_abs_divide)
done
-(*TOO DIFFICULT: 6 CASES
+lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::ordered_ring)"
+by (simp add: abs_if)
+
+lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::ordered_ring))"
+proof
+ assume ale: "a \<le> -a"
+ show "a\<le>0"
+ apply (rule classical)
+ apply (simp add: linorder_not_le)
+ apply (blast intro: ale order_trans order_less_imp_le
+ neg_0_le_iff_le [THEN iffD1])
+ done
+next
+ assume "a\<le>0"
+ hence "0 \<le> -a" by (simp only: neg_0_le_iff_le)
+ thus "a \<le> -a" by (blast intro: prems order_trans)
+qed
+
+lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::ordered_ring))"
+by (insert le_minus_self_iff [of "-a"], simp)
+
+lemma eq_minus_self_iff: "(a = -a) = (a = (0::'a::ordered_ring))"
+by (force simp add: order_eq_iff le_minus_self_iff minus_le_self_iff)
+
+lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_ring))"
+by (simp add: order_less_le le_minus_self_iff eq_minus_self_iff)
+
+lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::ordered_ring)"
+apply (simp add: abs_if split: split_if_asm)
+apply (rule order_trans [of _ "-a"])
+ apply (simp add: less_minus_self_iff order_less_imp_le, assumption)
+done
+
+lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::ordered_ring)"
+by (insert abs_le_D1 [of "-a"], simp)
+
+lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::ordered_ring))"
+by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
+
+lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::ordered_ring))"
+apply (simp add: order_less_le abs_le_iff)
+apply (auto simp add: abs_if minus_le_self_iff eq_minus_self_iff)
+ apply (simp add: linorder_not_less [symmetric])
+apply (simp add: le_minus_self_iff linorder_neq_iff)
+apply (simp add: linorder_not_less [symmetric])
+done
+
lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
-apply (simp add: abs_if)
-apply (auto );
-*)
+by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)
lemma abs_mult_less:
"[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"