--- a/doc-src/TutorialI/Advanced/document/simp.tex Fri Nov 28 12:09:37 2003 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Tue Dec 02 11:48:15 2003 +0100
@@ -160,7 +160,7 @@
Each occurrence of an unknown is of the form
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
variables. Thus all ordinary rewrite rules, where all unknowns are
-of base type, for example \isa{{\isacharquery}m\ {\isacharplus}\ {\isacharquery}n\ {\isacharplus}\ {\isacharquery}k\ {\isacharequal}\ {\isacharquery}m\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}n\ {\isacharplus}\ {\isacharquery}k{\isacharparenright}}, are acceptable: if an unknown is
+of base type, for example \isa{{\isacharquery}a\ {\isacharplus}\ {\isacharquery}b\ {\isacharplus}\ {\isacharquery}c\ {\isacharequal}\ {\isacharquery}a\ {\isacharplus}\ {\isacharparenleft}{\isacharquery}b\ {\isacharplus}\ {\isacharquery}c{\isacharparenright}}, are acceptable: if an unknown is
of base type, it cannot have any arguments. Additionally, the rule
\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymand}\ {\isacharquery}Q\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ {\isacharquery}Q\ x{\isacharparenright}{\isacharparenright}} is also acceptable, in
both directions: all arguments of the unknowns \isa{{\isacharquery}P} and
--- a/doc-src/TutorialI/Types/document/Numbers.tex Fri Nov 28 12:09:37 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Dec 02 11:48:15 2003 +0100
@@ -57,17 +57,17 @@
\rulename{add_2_eq_Suc'}
\begin{isabelle}%
-m\ {\isacharplus}\ n\ {\isacharplus}\ k\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n\ {\isacharplus}\ k{\isacharparenright}%
+a\ {\isacharplus}\ b\ {\isacharplus}\ c\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}%
\end{isabelle}
\rulename{add_assoc}
\begin{isabelle}%
-m\ {\isacharplus}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m%
+a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a%
\end{isabelle}
\rulename{add_commute}
\begin{isabelle}%
-x\ {\isacharplus}\ {\isacharparenleft}y\ {\isacharplus}\ z{\isacharparenright}\ {\isacharequal}\ y\ {\isacharplus}\ {\isacharparenleft}x\ {\isacharplus}\ z{\isacharparenright}%
+a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}%
\end{isabelle}
\rulename{add_left_commute}
--- a/doc-src/TutorialI/Types/document/Records.tex Fri Nov 28 12:09:37 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Tue Dec 02 11:48:15 2003 +0100
@@ -166,8 +166,8 @@
\medskip
\begin{tabular}{l}
- \isa{point}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isasymrparr}} \\
- \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isasymlparr}Xcoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ Ycoord\ {\isacharcolon}{\isacharcolon}\ int{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a{\isasymrparr}} \\
+ \isa{point}~\isa{{\isacharequal}}~\isa{point} \\
+ \isa{{\isacharprime}a\ point{\isacharunderscore}scheme}~\isa{{\isacharequal}}~\isa{{\isacharprime}a\ point{\isacharunderscore}scheme} \\
\end{tabular}
\medskip
--- a/src/HOL/Hyperreal/HyperOrd.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.ML Tue Dec 02 11:48:15 2003 +0100
@@ -382,7 +382,7 @@
Goalw [omega_def,hypreal_of_real_def]
"~ (EX x. hypreal_of_real x = omega)";
by (auto_tac (claset(),
- simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym,
+ simpset() addsimps [real_of_nat_Suc, diff_eq_eq RS sym,
lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
qed "not_ex_hypreal_of_real_eq_omega";
--- a/src/HOL/Hyperreal/Lim.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Tue Dec 02 11:48:15 2003 +0100
@@ -1791,7 +1791,7 @@
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> isCont (%x. inverse(M - f x)) x" 1);
by Safe_tac;
by (EVERY[rtac isCont_inverse 2, rtac isCont_diff 2, rtac notI 4]);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [real_diff_eq_eq])));
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [diff_eq_eq])));
by (Blast_tac 2);
by (subgoal_tac
"\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1);
@@ -1800,7 +1800,7 @@
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> 0 < inverse(M - f(x))" 1);
by (Asm_full_simp_tac 1);
by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [real_less_diff_eq]) 2);
+by (asm_full_simp_tac (simpset() addsimps [less_diff_eq]) 2);
by (subgoal_tac
"\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1);
by Safe_tac;
@@ -1815,7 +1815,7 @@
by (dres_inst_tac [("P", "%N. N<M --> ?Q N"),
("x","M - inverse(k + 1)")] spec 1);
by (Step_tac 1 THEN dtac real_leI 1);
-by (dtac (real_le_diff_eq RS iffD1) 1);
+by (dtac (le_diff_eq RS iffD1) 1);
by (REPEAT(dres_inst_tac [("x","a")] spec 1));
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac
@@ -1956,7 +1956,7 @@
by (res_inst_tac [("x","x - a")] exI 1);
by (res_inst_tac [("x","b - x")] exI 2);
by Auto_tac;
-by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
+by (auto_tac (claset(),simpset() addsimps [less_diff_eq]));
qed "lemma_interval_lt";
Goal "[| a < x; x < b |] ==> \
@@ -2098,7 +2098,7 @@
by (dtac MVT 1 THEN assume_tac 1);
by (blast_tac (claset() addIs [differentiableI]) 1);
by (auto_tac (claset() addSDs [DERIV_unique],simpset()
- addsimps [real_diff_eq_eq]));
+ addsimps [diff_eq_eq]));
qed "DERIV_isconst_end";
Goal "[| a < b; \
--- a/src/HOL/Hyperreal/NSA.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Hyperreal/NSA.ML Tue Dec 02 11:48:15 2003 +0100
@@ -2174,7 +2174,7 @@
by (rtac bexI 1);
by (rtac lemma_hyprel_refl 2);
by Auto_tac;
-by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
+by (simp_tac (simpset() addsimps [real_of_nat_Suc, diff_less_eq RS sym,
FreeUltrafilterNat_omega]) 1);
qed "HInfinite_omega";
Addsimps [HInfinite_omega];
@@ -2218,7 +2218,7 @@
Goal "0 < u ==> finite {n. u < inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1);
by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc,
- real_less_diff_eq RS sym]) 1);
+ less_diff_eq RS sym]) 1);
by (rtac finite_real_of_nat_less_real 1);
qed "finite_inverse_real_of_posnat_gt_real";
@@ -2246,7 +2246,7 @@
by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1);
by (cut_inst_tac [("x","inverse u - 1")] lemma_finite_omega_set 1);
by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc,
- real_diff_eq_eq RS sym, eq_commute]) 1);
+ diff_eq_eq RS sym, eq_commute]) 1);
qed "lemma_finite_omega_set2";
Goal "0 < u ==> finite {n. u <= inverse(real(Suc n))}";
--- a/src/HOL/Hyperreal/SEQ.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Tue Dec 02 11:48:15 2003 +0100
@@ -503,7 +503,7 @@
by (Force_tac 1);
by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
by (auto_tac (claset() addIs [finite_real_of_nat_less_real],
- simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym]));
+ simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym]));
val lemma_finite_NSBseq2 = result();
Goal "ALL N. real(Suc N) < abs (X (f N)) \
@@ -1130,7 +1130,7 @@
by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD2],
- simpset() delsimps [real_inverse_inverse]));
+ simpset() delsimps [thm"Ring_and_Field.inverse_inverse_eq"]));
qed "LIMSEQ_inverse_zero";
Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
--- a/src/HOL/Hyperreal/Transcendental.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Tue Dec 02 11:48:15 2003 +0100
@@ -680,7 +680,7 @@
by (asm_full_simp_tac (simpset() addsimps [LIM_def]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","abs K - abs x")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
+by (auto_tac (claset(),simpset() addsimps [less_diff_eq]));
by (dtac (abs_triangle_ineq RS order_le_less_trans) 1);
by (res_inst_tac [("y","0")] order_le_less_trans 1);
by Auto_tac;
@@ -703,7 +703,7 @@
by (asm_full_simp_tac (simpset() addsimps [LIM_def]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","abs K - abs x")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [real_less_diff_eq]));
+by (auto_tac (claset(),simpset() addsimps [less_diff_eq]));
by (dtac (abs_triangle_ineq RS order_le_less_trans) 1);
by (res_inst_tac [("y","0")] order_le_less_trans 1);
by Auto_tac;
@@ -1097,9 +1097,9 @@
Goal "1 <= y ==> EX x. 0 <= x & x <= y - 1 & exp(x) = y";
by (rtac IVT 1);
-by (auto_tac (claset() addIs [DERIV_exp RS DERIV_isCont],simpset()
- addsimps [real_le_diff_eq]));
-by (dtac (CLAIM_SIMP "x <= y ==> (0::real) <= y - x" [real_le_diff_eq]) 1);
+by (auto_tac (claset() addIs [DERIV_exp RS DERIV_isCont],
+ simpset() addsimps [le_diff_eq]));
+by (dtac (CLAIM_SIMP "x <= y ==> (0::real) <= y - x" [le_diff_eq]) 1);
by (dtac exp_ge_add_one_self 1);
by (Asm_full_simp_tac 1);
qed "lemma_exp_total";
@@ -2051,10 +2051,13 @@
Goalw [tan_def,real_divide_def]
"[| cos x ~= 0; cos y ~= 0 |] \
\ ==> 1 - tan(x)*tan(y) = cos (x + y)/(cos x * cos y)";
-by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib RS sym]
- @ real_mult_ac));
+by (auto_tac (claset(),
+ simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"]
+ addsimps [real_inverse_distrib RS sym] @ real_mult_ac));
by (res_inst_tac [("c1","cos x * cos y")] (real_mult_right_cancel RS subst) 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_assoc,
+by (auto_tac (claset(),
+ simpset() delsimps [thm"Ring_and_Field.inverse_mult_distrib"]
+ addsimps [real_mult_assoc,
real_mult_not_zero,real_diff_mult_distrib,cos_add]));
val lemma_tan_add1 = result();
Addsimps [lemma_tan_add1];
--- a/src/HOL/Real/RComplete.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Real/RComplete.ML Tue Dec 02 11:48:15 2003 +0100
@@ -161,7 +161,7 @@
by (dres_inst_tac [("y","(y + (- X) + 1)")] isLub_le_isUb 2
THEN assume_tac 2);
by (full_simp_tac
- (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
+ (simpset() addsimps [real_diff_def, diff_le_eq RS sym] @
real_add_ac) 2);
by (rtac (setleI RS isUbI) 1);
by (Step_tac 1);
@@ -217,7 +217,7 @@
[real_of_nat_Suc, real_add_mult_distrib2]) 1);
by (blast_tac (claset() addIs [isLubD2]) 2);
by (asm_full_simp_tac
- (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
+ (simpset() addsimps [le_diff_eq RS sym, real_diff_def]) 1);
by (subgoal_tac "isUb (UNIV::real set) \
\ {z. EX n. z = x*(real (Suc n))} (t + (-x))" 1);
by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
--- a/src/HOL/Real/RealArith.thy Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Real/RealArith.thy Tue Dec 02 11:48:15 2003 +0100
@@ -181,7 +181,8 @@
(* used in vector theory *)
lemma abs_triangle_ineq_three: "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)"
-by (auto intro!: abs_triangle_ineq [THEN order_trans] real_add_left_le_mono1 simp add: real_add_assoc)
+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)
--- a/src/HOL/Real/RealBin.ML Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Real/RealBin.ML Tue Dec 02 11:48:15 2003 +0100
@@ -194,16 +194,12 @@
(** Combining of literal coefficients in sums of products **)
-Goal "(x < y) = (x-y < (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
-qed "real_less_iff_diff_less_0";
-
Goal "(x = y) = (x-y = (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1);
+by (simp_tac (simpset() addsimps compare_rls) 1);
qed "real_eq_iff_diff_eq_0";
Goal "(x <= y) = (x-y <= (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1);
+by (simp_tac (simpset() addsimps compare_rls) 1);
qed "real_le_iff_diff_le_0";
@@ -217,10 +213,10 @@
(** For cancel_numerals **)
val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
- [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
+ [real_less_eq_diff, real_eq_iff_diff_eq_0,
real_le_iff_diff_le_0] @
map (inst "y" "n")
- [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
+ [real_less_eq_diff, real_eq_iff_diff_eq_0,
real_le_iff_diff_le_0];
Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
@@ -610,7 +606,7 @@
Addsimprocs [Real_Times_Assoc.conv];
(*Simplification of x-y < 0, etc.*)
-AddIffs [real_less_iff_diff_less_0 RS sym];
+AddIffs [real_less_eq_diff RS sym];
AddIffs [real_eq_iff_diff_eq_0 RS sym];
AddIffs [real_le_iff_diff_le_0 RS sym];
--- a/src/HOL/Real/RealDef.thy Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Real/RealDef.thy Tue Dec 02 11:48:15 2003 +0100
@@ -7,11 +7,26 @@
theory RealDef = PReal:
+(*MOVE TO THEORY PREAL*)
instance preal :: order
proof qed
(assumption |
rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
+instance preal :: order
+ by (intro_classes,
+ (assumption |
+ rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
+
+lemma preal_le_linear: "x <= y | y <= (x::preal)"
+apply (insert preal_linear [of x y])
+apply (auto simp add: order_less_le)
+done
+
+instance preal :: linorder
+ by (intro_classes, rule preal_le_linear)
+
+
constdefs
realrel :: "((preal * preal) * (preal * preal)) set"
"realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
@@ -99,7 +114,8 @@
(*** Proving that realrel is an equivalence relation ***)
-lemma preal_trans_lemma: "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |]
+lemma preal_trans_lemma:
+ "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |]
==> x1 + y3 = x3 + y1"
apply (rule_tac C = y2 in preal_add_right_cancel)
apply (rotate_tac 1, drule sym)
@@ -109,8 +125,6 @@
apply (simp add: preal_add_ac)
done
-(** Natural deduction for realrel **)
-
lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)"
by (unfold realrel_def, blast)
@@ -284,70 +298,6 @@
declare real_add_minus_left [simp]
-lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)"
-by (simp add: real_add_assoc [symmetric])
-
-lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)"
-by (simp add: real_add_assoc [symmetric])
-
-declare real_add_minus_cancel [simp] real_minus_add_cancel [simp]
-
-lemma real_minus_ex: "\<exists>y. (x::real) + y = 0"
-by (blast intro: real_add_minus)
-
-lemma real_minus_ex1: "EX! y. (x::real) + y = 0"
-apply (auto intro: real_add_minus)
-apply (drule_tac f = "%x. ya+x" in arg_cong)
-apply (simp add: real_add_assoc [symmetric])
-apply (simp add: real_add_commute)
-done
-
-lemma real_minus_left_ex1: "EX! y. y + (x::real) = 0"
-apply (auto intro: real_add_minus_left)
-apply (drule_tac f = "%x. x+ya" in arg_cong)
-apply (simp add: real_add_assoc)
-apply (simp add: real_add_commute)
-done
-
-lemma real_add_minus_eq_minus: "x + y = (0::real) ==> x = -y"
-apply (cut_tac z = y in real_add_minus_left)
-apply (rule_tac x1 = y in real_minus_left_ex1 [THEN ex1E], blast)
-done
-
-lemma real_as_add_inverse_ex: "\<exists>(y::real). x = -y"
-apply (cut_tac x = x in real_minus_ex)
-apply (erule exE, drule real_add_minus_eq_minus, fast)
-done
-
-lemma real_minus_add_distrib: "-(x + y) = (-x) + (- y :: real)"
-apply (rule_tac z = x in eq_Abs_REAL)
-apply (rule_tac z = y in eq_Abs_REAL)
-apply (auto simp add: real_minus real_add)
-done
-
-declare real_minus_add_distrib [simp]
-
-lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)"
-apply safe
-apply (drule_tac f = "%t. (-x) + t" in arg_cong)
-apply (simp add: real_add_assoc [symmetric])
-done
-
-lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)"
-by (simp add: real_add_commute real_add_left_cancel)
-
-lemma real_diff_0: "(0::real) - x = -x"
-by (simp add: real_diff_def)
-
-lemma real_diff_0_right: "x - (0::real) = x"
-by (simp add: real_diff_def)
-
-lemma real_diff_self: "x - x = (0::real)"
-by (simp add: real_diff_def)
-
-declare real_diff_0 [simp] real_diff_0_right [simp] real_diff_self [simp]
-
-
(*** Congruence property for multiplication ***)
lemma real_mult_congruent2_lemma: "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
@@ -491,22 +441,6 @@
apply (auto simp add: preal_add_commute)
done
-
-(*MOVE UP*)
-instance preal :: order
- by (intro_classes,
- (assumption |
- rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
-
-lemma preal_le_linear: "x <= y | y <= (x::preal)"
-apply (insert preal_linear [of x y])
-apply (auto simp add: order_less_le)
-done
-
-instance preal :: linorder
- by (intro_classes, rule preal_le_linear)
-
-
lemma real_mult_inv_right_ex:
"!!(x::real). x ~= 0 ==> \<exists>y. x*y = (1::real)"
apply (unfold real_zero_def real_one_def)
@@ -772,11 +706,15 @@
declare real_of_preal_minus_less_rev_iff [simp]
-(*** linearity ***)
+
+subsection{*Linearity of the Ordering*}
+
lemma real_linear: "(x::real) < y | x = y | y < x"
apply (rule_tac x = x in real_of_preal_trichotomyE)
apply (rule_tac [!] x = y in real_of_preal_trichotomyE)
-apply (auto dest!: preal_le_anti_sym simp add: preal_less_le_iff real_of_preal_minus_less_zero real_of_preal_zero_less real_of_preal_minus_less_all)
+apply (auto dest!: preal_le_anti_sym
+ simp add: preal_less_le_iff real_of_preal_minus_less_zero
+ real_of_preal_zero_less real_of_preal_minus_less_all)
done
lemma real_neq_iff: "!!w::real. (w ~= z) = (w<z | z<w)"
@@ -788,76 +726,6 @@
apply (cut_tac x = R1 and y = R2 in real_linear, auto)
done
-(*** Properties of <= ***)
-
-lemma real_leI: "~(w < z) ==> z \<le> (w::real)"
-
-apply (unfold real_le_def, assumption)
-done
-
-lemma real_leD: "z\<le>w ==> ~(w<(z::real))"
-by (unfold real_le_def, assumption)
-
-lemmas real_leE = real_leD [elim_format]
-
-lemma real_less_le_iff: "(~(w < z)) = (z \<le> (w::real))"
-by (blast intro!: real_leI real_leD)
-
-lemma not_real_leE: "~ z \<le> w ==> w<(z::real)"
-by (unfold real_le_def, blast)
-
-lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
-apply (unfold real_le_def)
-apply (cut_tac real_linear)
-apply (blast elim: real_less_irrefl real_less_asym)
-done
-
-lemma real_less_or_eq_imp_le: "z<w | z=w ==> z \<le>(w::real)"
-apply (unfold real_le_def)
-apply (cut_tac real_linear)
-apply (fast elim: real_less_irrefl real_less_asym)
-done
-
-lemma real_le_less: "(x \<le> (y::real)) = (x < y | x=y)"
-by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq)
-
-lemma real_le_refl: "w \<le> (w::real)"
-by (simp add: real_le_less)
-
-lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
-apply (drule real_le_imp_less_or_eq)
-apply (drule real_le_imp_less_or_eq)
-apply (rule real_less_or_eq_imp_le)
-apply (blast intro: real_less_trans)
-done
-
-lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
-apply (drule real_le_imp_less_or_eq)
-apply (drule real_le_imp_less_or_eq)
-apply (fast elim: real_less_irrefl real_less_asym)
-done
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma real_less_le: "((w::real) < z) = (w \<le> z & w ~= z)"
-apply (simp add: real_le_def real_neq_iff)
-apply (blast elim!: real_less_asym)
-done
-
-instance real :: order
- by (intro_classes,
- (assumption |
- rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
-apply (simp add: real_le_less)
-apply (cut_tac real_linear, blast)
-done
-
-instance real :: linorder
- by (intro_classes, rule real_le_linear)
-
-
lemma real_minus_zero_less_iff: "(0 < -R) = (R < (0::real))"
apply (rule_tac x = R in real_of_preal_trichotomyE)
apply (auto simp add: real_of_preal_not_minus_gt_zero real_of_preal_not_less_zero real_of_preal_zero_less real_of_preal_minus_less_zero)
@@ -870,123 +738,6 @@
done
declare real_minus_zero_less_iff2 [simp]
-(*Alternative definition for real_less*)
-lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
-apply (rule_tac x = R in real_of_preal_trichotomyE)
-apply (rule_tac [!] x = S in real_of_preal_trichotomyE)
-apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero)
-apply (rule_tac x = "real_of_preal D" in exI)
-apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI)
-apply (rule_tac [3] x = "real_of_preal D" in exI)
-apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc)
-done
-
-(** change naff name(s)! **)
-lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
-apply (drule real_less_add_positive_left_Ex)
-apply (auto simp add: real_add_minus real_add_zero_right real_add_ac)
-done
-
-lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)"
-by (simp add: real_add_ac)
-
-(* FIXME: long! *)
-lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
-apply (rule ccontr)
-apply (drule real_leI [THEN real_le_imp_less_or_eq])
-apply (auto simp add: real_less_not_refl)
-apply (drule real_less_add_positive_left_Ex, clarify, simp)
-apply (drule real_lemma_change_eq_subj, auto)
-apply (drule real_less_sum_gt_zero)
-apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac)
-done
-
-lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)"
-by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less)
-
-
-lemma real_less_eq_diff: "(x<y) = (x-y < (0::real))"
-apply (unfold real_diff_def)
-apply (subst real_minus_zero_less_iff [symmetric])
-apply (simp add: real_add_commute real_less_sum_gt_0_iff)
-done
-
-
-(*** Subtraction laws ***)
-
-lemma real_add_diff_eq: "x + (y - z) = (x + y) - (z::real)"
-by (simp add: real_diff_def real_add_ac)
-
-lemma real_diff_add_eq: "(x - y) + z = (x + z) - (y::real)"
-by (simp add: real_diff_def real_add_ac)
-
-lemma real_diff_diff_eq: "(x - y) - z = x - (y + (z::real))"
-by (simp add: real_diff_def real_add_ac)
-
-lemma real_diff_diff_eq2: "x - (y - z) = (x + z) - (y::real)"
-by (simp add: real_diff_def real_add_ac)
-
-lemma real_diff_less_eq: "(x-y < z) = (x < z + (y::real))"
-apply (subst real_less_eq_diff)
-apply (rule_tac y1 = z in real_less_eq_diff [THEN ssubst])
-apply (simp add: real_diff_def real_add_ac)
-done
-
-lemma real_less_diff_eq: "(x < z-y) = (x + (y::real) < z)"
-apply (subst real_less_eq_diff)
-apply (rule_tac y1 = "z-y" in real_less_eq_diff [THEN ssubst])
-apply (simp add: real_diff_def real_add_ac)
-done
-
-lemma real_diff_le_eq: "(x-y \<le> z) = (x \<le> z + (y::real))"
-apply (unfold real_le_def)
-apply (simp add: real_less_diff_eq)
-done
-
-lemma real_le_diff_eq: "(x \<le> z-y) = (x + (y::real) \<le> z)"
-apply (unfold real_le_def)
-apply (simp add: real_diff_less_eq)
-done
-
-lemma real_diff_eq_eq: "(x-y = z) = (x = z + (y::real))"
-apply (unfold real_diff_def)
-apply (auto simp add: real_add_assoc)
-done
-
-lemma real_eq_diff_eq: "(x = z-y) = (x + (y::real) = z)"
-apply (unfold real_diff_def)
-apply (auto simp add: real_add_assoc)
-done
-
-(*This list of rewrites simplifies (in)equalities by bringing subtractions
- to the top and then moving negative terms to the other side.
- Use with real_add_ac*)
-lemmas real_compare_rls =
- real_diff_def [symmetric]
- real_add_diff_eq real_diff_add_eq real_diff_diff_eq real_diff_diff_eq2
- real_diff_less_eq real_less_diff_eq real_diff_le_eq real_le_diff_eq
- real_diff_eq_eq real_eq_diff_eq
-
-
-(** For the cancellation simproc.
- The idea is to cancel like terms on opposite sides by subtraction **)
-
-lemma real_less_eqI: "(x::real) - y = x' - y' ==> (x<y) = (x'<y')"
-apply (subst real_less_eq_diff)
-apply (rule_tac y1 = y in real_less_eq_diff [THEN ssubst], simp)
-done
-
-lemma real_le_eqI: "(x::real) - y = x' - y' ==> (y\<le>x) = (y'\<le>x')"
-apply (drule real_less_eqI)
-apply (simp add: real_le_def)
-done
-
-lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
-apply safe
-apply (simp_all add: real_eq_diff_eq real_diff_eq_eq)
-done
-
-
ML
{*
val real_le_def = thm "real_le_def";
@@ -1020,122 +771,9 @@
val real_add_zero_right = thm"real_add_zero_right";
val real_add_minus = thm"real_add_minus";
val real_add_minus_left = thm"real_add_minus_left";
-val real_add_minus_cancel = thm"real_add_minus_cancel";
-val real_minus_add_cancel = thm"real_minus_add_cancel";
-val real_minus_ex = thm"real_minus_ex";
-val real_minus_ex1 = thm"real_minus_ex1";
-val real_minus_left_ex1 = thm"real_minus_left_ex1";
-val real_add_minus_eq_minus = thm"real_add_minus_eq_minus";
-val real_as_add_inverse_ex = thm"real_as_add_inverse_ex";
-val real_minus_add_distrib = thm"real_minus_add_distrib";
-val real_add_left_cancel = thm"real_add_left_cancel";
-val real_add_right_cancel = thm"real_add_right_cancel";
-val real_diff_0 = thm"real_diff_0";
-val real_diff_0_right = thm"real_diff_0_right";
-val real_diff_self = thm"real_diff_self";
-val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma";
-val real_mult_congruent2 = thm"real_mult_congruent2";
-val real_mult = thm"real_mult";
-val real_mult_commute = thm"real_mult_commute";
-val real_mult_assoc = thm"real_mult_assoc";
-val real_mult_left_commute = thm"real_mult_left_commute";
-val real_mult_1 = thm"real_mult_1";
-val real_mult_1_right = thm"real_mult_1_right";
-val real_mult_0 = thm"real_mult_0";
-val real_mult_0_right = thm"real_mult_0_right";
-val real_mult_minus_eq1 = thm"real_mult_minus_eq1";
-val real_minus_mult_eq1 = thm"real_minus_mult_eq1";
-val real_mult_minus_eq2 = thm"real_mult_minus_eq2";
-val real_minus_mult_eq2 = thm"real_minus_mult_eq2";
-val real_mult_minus_1 = thm"real_mult_minus_1";
-val real_mult_minus_1_right = thm"real_mult_minus_1_right";
-val real_minus_mult_cancel = thm"real_minus_mult_cancel";
-val real_minus_mult_commute = thm"real_minus_mult_commute";
-val real_add_assoc_cong = thm"real_add_assoc_cong";
-val real_add_mult_distrib = thm"real_add_mult_distrib";
-val real_add_mult_distrib2 = thm"real_add_mult_distrib2";
-val real_diff_mult_distrib = thm"real_diff_mult_distrib";
-val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2";
-val real_zero_not_eq_one = thm"real_zero_not_eq_one";
-val real_zero_iff = thm"real_zero_iff";
-val preal_le_linear = thm"preal_le_linear";
-val real_mult_inv_right_ex = thm"real_mult_inv_right_ex";
-val real_mult_inv_left_ex = thm"real_mult_inv_left_ex";
-val real_mult_inv_left = thm"real_mult_inv_left";
-val real_mult_inv_right = thm"real_mult_inv_right";
-val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum";
-val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel";
-val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl";
-val real_less_not_refl = thm"real_less_not_refl";
-val real_less_irrefl = thm"real_less_irrefl";
-val real_not_refl2 = thm"real_not_refl2";
-val preal_lemma_trans = thm"preal_lemma_trans";
-val real_less_trans = thm"real_less_trans";
-val real_less_not_sym = thm"real_less_not_sym";
-val real_less_asym = thm"real_less_asym";
-val real_of_preal_add = thm"real_of_preal_add";
-val real_of_preal_mult = thm"real_of_preal_mult";
-val real_of_preal_ExI = thm"real_of_preal_ExI";
-val real_of_preal_ExD = thm"real_of_preal_ExD";
-val real_of_preal_iff = thm"real_of_preal_iff";
-val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
-val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE";
-val real_of_preal_lessD = thm"real_of_preal_lessD";
-val real_of_preal_lessI = thm"real_of_preal_lessI";
-val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1";
-val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self";
-val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
-val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
-val real_of_preal_zero_less = thm"real_of_preal_zero_less";
-val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero";
-val real_minus_minus_zero_less = thm"real_minus_minus_zero_less";
-val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less";
-val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all";
-val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all";
-val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1";
-val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2";
-val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff";
-val real_linear = thm"real_linear";
-val real_neq_iff = thm"real_neq_iff";
-val real_linear_less2 = thm"real_linear_less2";
-val real_leI = thm"real_leI";
-val real_leD = thm"real_leD";
-val real_leE = thm"real_leE";
-val real_less_le_iff = thm"real_less_le_iff";
-val not_real_leE = thm"not_real_leE";
-val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
-val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le";
-val real_le_less = thm"real_le_less";
-val real_le_refl = thm"real_le_refl";
-val real_le_linear = thm"real_le_linear";
-val real_le_trans = thm"real_le_trans";
-val real_le_anti_sym = thm"real_le_anti_sym";
-val real_less_le = thm"real_less_le";
-val real_minus_zero_less_iff = thm"real_minus_zero_less_iff";
-val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2";
-val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex";
-val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
-val real_lemma_change_eq_subj = thm"real_lemma_change_eq_subj";
-val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
-val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
-val real_less_eq_diff = thm"real_less_eq_diff";
-val real_add_diff_eq = thm"real_add_diff_eq";
-val real_diff_add_eq = thm"real_diff_add_eq";
-val real_diff_diff_eq = thm"real_diff_diff_eq";
-val real_diff_diff_eq2 = thm"real_diff_diff_eq2";
-val real_diff_less_eq = thm"real_diff_less_eq";
-val real_less_diff_eq = thm"real_less_diff_eq";
-val real_diff_le_eq = thm"real_diff_le_eq";
-val real_le_diff_eq = thm"real_le_diff_eq";
-val real_diff_eq_eq = thm"real_diff_eq_eq";
-val real_eq_diff_eq = thm"real_eq_diff_eq";
-val real_less_eqI = thm"real_less_eqI";
-val real_le_eqI = thm"real_le_eqI";
-val real_eq_eqI = thm"real_eq_eqI";
val real_add_ac = thms"real_add_ac";
val real_mult_ac = thms"real_mult_ac";
-val real_compare_rls = thms"real_compare_rls";
*}
--- a/src/HOL/Real/RealOrd.thy Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Tue Dec 02 11:48:15 2003 +0100
@@ -13,7 +13,388 @@
-subsection{* The Simproc @{text abel_cancel}*}
+subsection{*Properties of Less-Than Or Equals*}
+
+lemma real_leI: "~(w < z) ==> z \<le> (w::real)"
+apply (unfold real_le_def, assumption)
+done
+
+lemma real_leD: "z\<le>w ==> ~(w<(z::real))"
+by (unfold real_le_def, assumption)
+
+lemmas real_leE = real_leD [elim_format]
+
+lemma real_less_le_iff: "(~(w < z)) = (z \<le> (w::real))"
+by (blast intro!: real_leI real_leD)
+
+lemma not_real_leE: "~ z \<le> w ==> w<(z::real)"
+by (unfold real_le_def, blast)
+
+lemma real_le_imp_less_or_eq: "!!(x::real). x \<le> y ==> x < y | x = y"
+apply (unfold real_le_def)
+apply (cut_tac real_linear)
+apply (blast elim: real_less_irrefl real_less_asym)
+done
+
+lemma real_less_or_eq_imp_le: "z<w | z=w ==> z \<le>(w::real)"
+apply (unfold real_le_def)
+apply (cut_tac real_linear)
+apply (fast elim: real_less_irrefl real_less_asym)
+done
+
+lemma real_le_less: "(x \<le> (y::real)) = (x < y | x=y)"
+by (blast intro!: real_less_or_eq_imp_le dest!: real_le_imp_less_or_eq)
+
+lemma real_le_refl: "w \<le> (w::real)"
+by (simp add: real_le_less)
+
+lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
+apply (drule real_le_imp_less_or_eq)
+apply (drule real_le_imp_less_or_eq)
+apply (rule real_less_or_eq_imp_le)
+apply (blast intro: real_less_trans)
+done
+
+lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
+apply (drule real_le_imp_less_or_eq)
+apply (drule real_le_imp_less_or_eq)
+apply (fast elim: real_less_irrefl real_less_asym)
+done
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma real_less_le: "((w::real) < z) = (w \<le> z & w ~= z)"
+apply (simp add: real_le_def real_neq_iff)
+apply (blast elim!: real_less_asym)
+done
+
+instance real :: order
+ by (intro_classes,
+ (assumption |
+ rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+)
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
+apply (simp add: real_le_less)
+apply (cut_tac real_linear, blast)
+done
+
+instance real :: linorder
+ by (intro_classes, rule real_le_linear)
+
+
+subsection{*Theorems About the Ordering*}
+
+lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
+apply (auto simp add: real_of_preal_zero_less)
+apply (cut_tac x = x in real_of_preal_trichotomy)
+apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE])
+done
+
+lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
+by (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
+ intro: real_gt_zero_preal_Ex [THEN iffD1])
+
+lemma real_ge_preal_preal_Ex: "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
+by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
+
+lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
+by (auto elim: order_le_imp_less_or_eq [THEN disjE]
+ intro: real_of_preal_zero_less [THEN [2] real_less_trans]
+ simp add: real_of_preal_zero_less)
+
+lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
+by (blast intro!: real_less_all_preal real_leI)
+
+lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
+apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
+apply (drule order_le_less_trans, assumption)
+apply (erule preal_less_irrefl)
+done
+
+
+subsection{*Monotonicity of Addition*}
+
+lemma real_add_left_cancel: "((x::real) + y = x + z) = (y = z)"
+apply safe
+apply (drule_tac f = "%t. (-x) + t" in arg_cong)
+apply (simp add: real_add_assoc [symmetric])
+done
+
+
+lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
+apply (auto simp add: real_gt_zero_preal_Ex)
+apply (rule_tac x = "y*ya" in exI)
+apply (simp (no_asm_use) add: real_of_preal_mult)
+done
+
+lemma real_minus_add_distrib [simp]: "-(x + y) = (-x) + (- y :: real)"
+apply (rule_tac z = x in eq_Abs_REAL)
+apply (rule_tac z = y in eq_Abs_REAL)
+apply (auto simp add: real_minus real_add)
+done
+
+(*Alternative definition for real_less*)
+lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
+apply (rule_tac x = R in real_of_preal_trichotomyE)
+apply (rule_tac [!] x = S in real_of_preal_trichotomyE)
+apply (auto dest!: preal_less_add_left_Ex simp add: real_of_preal_not_minus_gt_all real_of_preal_add real_of_preal_not_less_zero real_less_not_refl real_of_preal_not_minus_gt_zero)
+apply (rule_tac x = "real_of_preal D" in exI)
+apply (rule_tac [2] x = "real_of_preal m+real_of_preal ma" in exI)
+apply (rule_tac [3] x = "real_of_preal D" in exI)
+apply (auto simp add: real_of_preal_zero_less real_of_preal_sum_zero_less real_add_assoc)
+apply (simp add: real_add_assoc [symmetric])
+done
+
+lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))"
+apply (drule real_less_add_positive_left_Ex)
+apply (auto simp add: real_add_minus real_add_zero_right real_add_ac)
+done
+
+lemma real_lemma_change_eq_subj: "!!S::real. T = S + W ==> S = T + (-W)"
+by (simp add: real_add_ac)
+
+(* FIXME: long! *)
+lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
+apply (rule ccontr)
+apply (drule real_leI [THEN real_le_imp_less_or_eq])
+apply (auto simp add: real_less_not_refl)
+apply (drule real_less_add_positive_left_Ex, clarify, simp)
+apply (drule real_lemma_change_eq_subj, auto)
+apply (drule real_less_sum_gt_zero)
+apply (auto elim: real_less_asym simp add: real_add_left_commute [of W] real_add_ac)
+done
+
+lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
+apply (rule real_sum_gt_zero_less)
+apply (drule real_less_sum_gt_zero [of x y])
+apply (drule real_mult_order, assumption)
+apply (simp add: real_add_mult_distrib2)
+done
+
+(** For the cancellation simproc.
+ The idea is to cancel like terms on opposite sides by subtraction **)
+
+lemma real_less_sum_gt_0_iff: "(0 < S + (-W::real)) = (W < S)"
+by (blast intro: real_less_sum_gt_zero real_sum_gt_zero_less)
+
+lemma real_less_eq_diff: "(x<y) = (x-y < (0::real))"
+apply (unfold real_diff_def)
+apply (subst real_minus_zero_less_iff [symmetric])
+apply (simp add: real_add_commute real_less_sum_gt_0_iff)
+done
+
+lemma real_less_eqI: "(x::real) - y = x' - y' ==> (x<y) = (x'<y')"
+apply (subst real_less_eq_diff)
+apply (rule_tac y1 = y in real_less_eq_diff [THEN ssubst], simp)
+done
+
+lemma real_le_eqI: "(x::real) - y = x' - y' ==> (y\<le>x) = (y'\<le>x')"
+apply (drule real_less_eqI)
+apply (simp add: real_le_def)
+done
+
+lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)"
+apply (rule real_le_eqI [THEN iffD1])
+ prefer 2 apply assumption;
+apply (simp add: real_diff_def real_add_ac);
+done
+
+
+subsection{*The Reals Form an Ordered Field*}
+
+instance real :: inverse ..
+
+instance real :: ordered_field
+proof
+ fix x y z :: real
+ show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
+ show "x + y = y + x" by (rule real_add_commute)
+ show "0 + x = x" by simp
+ show "- x + x = 0" by simp
+ show "x - y = x + (-y)" by (simp add: real_diff_def)
+ show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
+ show "x * y = y * x" by (rule real_mult_commute)
+ show "1 * x = x" by simp
+ show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
+ show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
+ show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
+ show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
+ show "\<bar>x\<bar> = (if x < 0 then -x else x)"
+ by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
+ show "x \<noteq> 0 ==> inverse x * x = 1" by simp
+ show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
+qed
+
+
+lemma real_zero_less_one: "0 < (1::real)"
+ by (rule Ring_and_Field.zero_less_one)
+
+lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)"
+ by (rule Ring_and_Field.add_strict_mono)
+
+lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
+ by (rule Ring_and_Field.add_mono)
+
+lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
+ by (rule Ring_and_Field.neg_le_iff_le)
+
+lemma real_le_square [simp]: "(0::real) \<le> x*x"
+ by (rule Ring_and_Field.zero_le_square)
+
+
+subsection{*Division Lemmas*}
+
+(** Inverse of zero! Useful to simplify certain equations **)
+
+lemma INVERSE_ZERO: "inverse 0 = (0::real)"
+apply (unfold real_inverse_def)
+apply (rule someI2)
+apply (auto simp add: real_zero_not_eq_one)
+done
+
+lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0"
+ by (simp add: real_divide_def INVERSE_ZERO)
+
+instance real :: division_by_zero
+proof
+ fix x :: real
+ show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
+ show "x/0 = 0" by (rule DIVISION_BY_ZERO)
+qed
+
+lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)"
+by auto
+
+lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)"
+by auto
+
+lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b"
+by auto
+
+lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b"
+by auto
+
+lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0"
+ by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
+
+lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
+by simp
+
+lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
+ by (rule Ring_and_Field.inverse_inverse_eq)
+
+lemma real_inverse_1: "inverse((1::real)) = (1::real)"
+ by (rule Ring_and_Field.inverse_1)
+
+lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)"
+ by (rule Ring_and_Field.inverse_minus_eq)
+
+lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
+ by (rule Ring_and_Field.inverse_mult_distrib)
+
+lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
+by (simp add: real_divide_def real_mult_assoc)
+
+lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
+by (simp add: real_divide_def real_mult_ac)
+
+declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
+
+lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
+by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
+
+lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
+by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
+
+declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
+
+(** As with multiplication, pull minus signs OUT of the / operator **)
+
+lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
+by (simp add: real_divide_def)
+declare real_minus_divide_eq [simp]
+
+lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)"
+by (simp add: real_divide_def real_minus_inverse)
+declare real_divide_minus_eq [simp]
+
+lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z"
+by (simp add: real_divide_def real_add_mult_distrib)
+
+(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
+ leads to cancellations in x or y, but is also prevents "multiplying out"
+ the 2 in e.g. (x+y)/2 = 5.
+
+Addsimps [inst "z" "number_of ?w" real_add_divide_distrib]
+**)
+
+
+
+subsection{*More Lemmas*}
+
+lemma real_add_right_cancel: "(y + (x::real)= z + x) = (y = z)"
+ by (rule Ring_and_Field.add_right_cancel)
+
+lemma real_add_less_mono1: "v < (w::real) ==> v + z < w + z"
+ by (rule Ring_and_Field.add_strict_right_mono)
+
+lemma real_add_le_mono1: "v \<le> (w::real) ==> v + z \<le> w + z"
+ by (rule Ring_and_Field.add_right_mono)
+
+lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
+apply (erule add_strict_right_mono [THEN order_less_le_trans])
+apply (erule add_left_mono)
+done
+
+lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
+apply (erule add_right_mono [THEN order_le_less_trans])
+apply (erule add_strict_left_mono)
+done
+
+lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
+ by (rule Ring_and_Field.add_less_imp_less_right)
+
+lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
+ by (rule Ring_and_Field.add_less_imp_less_left)
+
+lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
+ by (rule Ring_and_Field.add_le_imp_le_right)
+
+ lemma add_le_imp_le_left:
+ "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
+ by simp
+
+lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
+ by (rule (*Ring_and_Field.*)add_le_imp_le_left)
+
+lemma real_minus_diff_eq: "- (z - y) = y - (z::real)"
+ by (rule Ring_and_Field.minus_diff_eq)
+
+lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
+ by (rule Ring_and_Field.add_less_cancel_right)
+
+lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
+ by (rule Ring_and_Field.add_less_cancel_left)
+
+lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
+ by (rule Ring_and_Field.add_le_cancel_right)
+
+lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
+ by (rule Ring_and_Field.add_le_cancel_left)
+
+
+subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
+
+lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
+apply safe
+apply (simp_all add: eq_diff_eq diff_eq_eq)
+done
+
+lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)"
+by (simp add: real_add_assoc [symmetric])
+
+lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)"
+by (simp add: real_add_assoc [symmetric])
(*Deletion of other terms in the formula, seeking the -x at the front of z*)
lemma real_add_cancel_21: "((x::real) + (y + z) = y + u) = ((x + z) = u)"
@@ -26,7 +407,7 @@
lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)"
apply (subst real_add_left_commute)
apply (rule_tac t = y in real_add_zero_right [THEN subst], subst real_add_left_cancel)
-apply (simp add: real_eq_diff_eq [symmetric])
+apply (simp add: real_diff_def eq_diff_eq [symmetric])
done
@@ -34,6 +415,14 @@
{*
val real_add_cancel_21 = thm "real_add_cancel_21";
val real_add_cancel_end = thm "real_add_cancel_end";
+val real_add_left_cancel = thm"real_add_left_cancel";
+val real_eq_diff_eq = thm"eq_diff_eq";
+val real_less_eqI = thm"real_less_eqI";
+val real_le_eqI = thm"real_le_eqI";
+val real_eq_eqI = thm"real_eq_eqI";
+val real_add_minus_cancel = thm"real_add_minus_cancel";
+val real_minus_add_cancel = thm"real_minus_add_cancel";
+val real_minus_add_distrib = thm"real_minus_add_distrib";
structure Real_Cancel_Data =
struct
@@ -72,245 +461,6 @@
Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
*}
-lemma real_minus_diff_eq [simp]: "- (z - y) = y - (z::real)"
-by simp
-
-
-subsection{*Theorems About the Ordering*}
-
-lemma real_gt_zero_preal_Ex: "(0 < x) = (\<exists>y. x = real_of_preal y)"
-apply (auto simp add: real_of_preal_zero_less)
-apply (cut_tac x = x in real_of_preal_trichotomy)
-apply (blast elim!: real_less_irrefl real_of_preal_not_minus_gt_zero [THEN notE])
-done
-
-lemma real_gt_preal_preal_Ex: "real_of_preal z < x ==> \<exists>y. x = real_of_preal y"
-by (blast dest!: real_of_preal_zero_less [THEN real_less_trans]
- intro: real_gt_zero_preal_Ex [THEN iffD1])
-
-lemma real_ge_preal_preal_Ex: "real_of_preal z \<le> x ==> \<exists>y. x = real_of_preal y"
-by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex)
-
-lemma real_less_all_preal: "y \<le> 0 ==> \<forall>x. y < real_of_preal x"
-by (auto elim: order_le_imp_less_or_eq [THEN disjE]
- intro: real_of_preal_zero_less [THEN [2] real_less_trans]
- simp add: real_of_preal_zero_less)
-
-lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
-by (blast intro!: real_less_all_preal real_leI)
-
-lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
-apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
-apply (drule order_le_less_trans, assumption)
-apply (erule preal_less_irrefl)
-done
-
-subsection{*Monotonicity of Addition*}
-
-lemma real_add_right_cancel_less [simp]: "(v+z < w+z) = (v < (w::real))"
-by simp
-
-lemma real_add_left_cancel_less [simp]: "(z+v < z+w) = (v < (w::real))"
-by simp
-
-lemma real_add_right_cancel_le [simp]: "(v+z \<le> w+z) = (v \<le> (w::real))"
-by simp
-
-lemma real_add_left_cancel_le [simp]: "(z+v \<le> z+w) = (v \<le> (w::real))"
-by simp
-
-lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y"
-apply (auto simp add: real_gt_zero_preal_Ex)
-apply (rule_tac x = "y*ya" in exI)
-apply (simp (no_asm_use) add: real_of_preal_mult)
-done
-
-lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
-apply (rule real_sum_gt_zero_less)
-apply (drule real_less_sum_gt_zero [of x y])
-apply (drule real_mult_order, assumption)
-apply (simp add: real_add_mult_distrib2)
-done
-
-
-subsection{*The Reals Form an Ordered Field*}
-
-instance real :: inverse ..
-
-instance real :: ordered_field
-proof
- fix x y z :: real
- show "(x + y) + z = x + (y + z)" by (rule real_add_assoc)
- show "x + y = y + x" by (rule real_add_commute)
- show "0 + x = x" by simp
- show "- x + x = 0" by simp
- show "x - y = x + (-y)" by (simp add: real_diff_def)
- show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
- show "x * y = y * x" by (rule real_mult_commute)
- show "1 * x = x" by simp
- show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
- show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
- show "x \<le> y ==> z + x \<le> z + y" by simp
- show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
- show "\<bar>x\<bar> = (if x < 0 then -x else x)"
- by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
- show "x \<noteq> 0 ==> inverse x * x = 1" by simp
- show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
-qed
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas real_add_less_mono1 = real_add_right_cancel_less [THEN iffD2, standard]
-
-(*"v\<le>w ==> v+z \<le> w+z"*)
-lemmas real_add_le_mono1 = real_add_right_cancel_le [THEN iffD2, standard]
-
-lemma real_add_less_le_mono: "!!z z'::real. [| w'<w; z'\<le>z |] ==> w' + z' < w + z"
-by (erule real_add_less_mono1 [THEN order_less_le_trans], simp)
-
-lemma real_add_le_less_mono: "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
-by (erule real_add_le_mono1 [THEN order_le_less_trans], simp)
-
-lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
-by simp
-
-lemma real_less_add_right_cancel: "!!(A::real). A + C < B + C ==> A < B"
-apply simp
-done
-
-lemma real_less_add_left_cancel: "!!(A::real). C + A < C + B ==> A < B"
-apply simp
-done
-
-lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B"
-apply simp
-done
-
-lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B"
-apply simp
-done
-
-lemma real_zero_less_one: "0 < (1::real)"
- by (rule Ring_and_Field.zero_less_one)
-
-lemma real_add_less_mono: "[| R1 < S1; R2 < S2 |] ==> R1+R2 < S1+(S2::real)"
- by (rule Ring_and_Field.add_strict_mono)
-
-lemma real_add_left_le_mono1: "!!(q1::real). q1 \<le> q2 ==> x + q1 \<le> x + q2"
-by simp
-
-lemma real_add_le_mono: "[|i\<le>j; k\<le>l |] ==> i + k \<le> j + (l::real)"
- by (rule Ring_and_Field.add_mono)
-
-lemma real_le_minus_iff: "(-s \<le> -r) = ((r::real) \<le> s)"
- by (rule Ring_and_Field.neg_le_iff_le)
-
-lemma real_le_square [simp]: "(0::real) \<le> x*x"
- by (rule Ring_and_Field.zero_le_square)
-
-
-subsection{*Division Lemmas*}
-
-(** Inverse of zero! Useful to simplify certain equations **)
-
-lemma INVERSE_ZERO [simp]: "inverse 0 = (0::real)"
-apply (unfold real_inverse_def)
-apply (rule someI2)
-apply (auto simp add: real_zero_not_eq_one)
-done
-
-lemma DIVISION_BY_ZERO [simp]: "a / (0::real) = 0"
-by (simp add: real_divide_def INVERSE_ZERO)
-
-lemma real_mult_left_cancel: "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)"
-apply auto
-done
-
-lemma real_mult_right_cancel: "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)"
-apply (auto );
-done
-
-lemma real_mult_left_cancel_ccontr: "c*a ~= c*b ==> a ~= b"
-by auto
-
-lemma real_mult_right_cancel_ccontr: "a*c ~= b*c ==> a ~= b"
-by auto
-
-lemma real_inverse_not_zero: "x ~= 0 ==> inverse(x::real) ~= 0"
- by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
-
-lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
-apply (simp add: );
-done
-
-lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
-apply (case_tac "x=0", simp)
-apply (rule_tac c1 = "inverse x" in real_mult_right_cancel [THEN iffD1])
-apply (erule real_inverse_not_zero)
-apply (auto dest: real_inverse_not_zero)
-done
-declare real_inverse_inverse [simp]
-
-lemma real_inverse_1: "inverse((1::real)) = (1::real)"
-apply (unfold real_inverse_def)
-apply (cut_tac real_zero_not_eq_one [THEN not_sym, THEN real_mult_inv_left_ex])
-apply (auto simp add: real_zero_not_eq_one [THEN not_sym])
-done
-declare real_inverse_1 [simp]
-
-lemma real_minus_inverse: "inverse(-x) = -inverse(x::real)"
-apply (case_tac "x=0", simp)
-apply (rule_tac c1 = "-x" in real_mult_right_cancel [THEN iffD1])
- prefer 2 apply (subst real_mult_inv_left, auto)
-done
-
-lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
-apply (case_tac "x=0", simp)
-apply (case_tac "y=0", simp)
-apply (frule_tac y = y in real_mult_not_zero, assumption)
-apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1])
-apply (auto simp add: real_mult_assoc [symmetric])
-apply (rule_tac c1 = y in real_mult_left_cancel [THEN iffD1])
-apply (auto simp add: real_mult_left_commute)
-apply (simp add: real_mult_assoc [symmetric])
-done
-
-lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
-by (simp add: real_divide_def real_mult_assoc)
-
-lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
-by (simp add: real_divide_def real_mult_ac)
-
-declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
-
-lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
-by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
-
-lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
-by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
-
-declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
-
-(** As with multiplication, pull minus signs OUT of the / operator **)
-
-lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
-by (simp add: real_divide_def)
-declare real_minus_divide_eq [simp]
-
-lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)"
-by (simp add: real_divide_def real_minus_inverse)
-declare real_divide_minus_eq [simp]
-
-lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z"
-by (simp add: real_divide_def real_add_mult_distrib)
-
-(*The following would e.g. convert (x+y)/2 to x/2 + y/2. Sometimes that
- leads to cancellations in x or y, but is also prevents "multiplying out"
- the 2 in e.g. (x+y)/2 = 5.
-
-Addsimps [inst "z" "number_of ?w" real_add_divide_distrib]
-**)
-
-
subsection{*An Embedding of the Naturals in the Reals*}
@@ -356,7 +506,7 @@
lemma real_of_nat_add [simp]:
"real (m + n) = real (m::nat) + real n"
-apply (simp add: real_of_nat_def real_add_assoc)
+apply (simp add: real_of_nat_def add_ac)
apply (simp add: real_of_posnat_add real_add_assoc [symmetric])
done
@@ -409,20 +559,11 @@
qed
lemma real_of_nat_neg_int [simp]: "neg z ==> real (nat z) = 0"
-apply (simp add: neg_nat real_of_nat_zero)
-done
+by (simp add: neg_nat real_of_nat_zero)
subsection{*Inverse and Division*}
-instance real :: division_by_zero
-proof
- fix x :: real
- show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
- show "x/0 = 0" by (rule DIVISION_BY_ZERO)
-qed
-
-
lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
by (rule Ring_and_Field.inverse_gt_0)
@@ -483,8 +624,8 @@
done
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-apply (drule real_add_minus_eq_minus)
-apply (cut_tac x = x in real_le_square)
+apply (drule Ring_and_Field.equals_zero_I [THEN sym])
+apply (cut_tac x = y in real_le_square)
apply (auto, drule real_le_anti_sym, auto)
done
@@ -510,10 +651,12 @@
subsection{*Hardly Used Theorems to be Deleted*}
+lemma real_add_less_mono2: "!!(A::real). A < B ==> C + A < C + B"
+by simp
+
lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
apply (erule order_less_trans)
-apply (drule real_add_less_mono2)
-apply simp
+apply (drule real_add_less_mono2, simp)
done
lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
@@ -531,8 +674,7 @@
lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
apply (unfold real_of_posnat_def)
-apply (rule real_gt_zero_preal_Ex [THEN iffD2])
-apply blast
+apply (rule real_gt_zero_preal_Ex [THEN iffD2], blast)
done
declare real_of_posnat_gt_zero [simp]
@@ -544,8 +686,7 @@
declare real_of_posnat_ge_zero [simp]
lemma real_of_posnat_not_eq_zero: "real_of_posnat n ~= 0"
-apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
-done
+by (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym])
declare real_of_posnat_not_eq_zero [simp]
declare real_of_posnat_not_eq_zero [THEN real_mult_inv_left, simp]
@@ -580,14 +721,14 @@
lemma real_of_posnat_inv_Ex_iff: "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)"
apply safe
-apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
+apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1])
apply (auto simp add: real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_assoc)
done
lemma real_of_posnat_inv_iff: "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)"
apply safe
-apply (drule_tac n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
+apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1])
apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1])
apply (auto simp add: real_mult_assoc)
done
@@ -607,37 +748,32 @@
lemma real_of_posnat_less_iff:
"(real_of_posnat n < real_of_posnat m) = (n < m)"
-apply (unfold real_of_posnat_def)
-apply auto
+apply (unfold real_of_posnat_def, auto)
done
declare real_of_posnat_less_iff [simp]
lemma real_of_posnat_le_iff: "(real_of_posnat n <= real_of_posnat m) = (n <= m)"
-apply (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq)
-done
+by (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq)
declare real_of_posnat_le_iff [simp]
lemma real_mult_less_cancel3: "[| (0::real)<z; x*z<y*z |] ==> x<y"
-apply auto
-done
+by auto
lemma real_mult_less_cancel4: "[| (0::real)<z; z*x<z*y |] ==> x<y"
-apply auto
-done
+by auto
lemma real_of_posnat_less_inv_iff: "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))"
apply safe
apply (rule_tac n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_cancel3])
-apply (rule_tac [2] x1 = "u" in real_inverse_gt_0 [THEN real_mult_less_cancel3])
+apply (rule_tac [2] x1 = u in real_inverse_gt_0 [THEN real_mult_less_cancel3])
apply (auto simp add: real_not_refl2 [THEN not_sym])
-apply (rule_tac z = "u" in real_mult_less_cancel4)
-apply (rule_tac [3] n1 = "n" in real_of_posnat_gt_zero [THEN real_mult_less_cancel4])
+apply (rule_tac z = u in real_mult_less_cancel4)
+apply (rule_tac [3] n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_cancel4])
apply (auto simp add: real_not_refl2 [THEN not_sym] real_mult_assoc [symmetric])
done
lemma real_of_posnat_inv_eq_iff: "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)"
-apply auto
-done
+by auto
lemma real_add_one_minus_inv_ge_zero: "0 <= 1 + -inverse(real_of_posnat n)"
apply (rule_tac C = "inverse (real_of_posnat n) " in real_le_add_right_cancel)
@@ -645,30 +781,23 @@
done
lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))"
-apply (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1])
-apply auto
-done
+by (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1], auto)
lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x"
apply (case_tac "x ~= 0")
-apply (rule_tac c1 = "x" in real_mult_left_cancel [THEN iffD1])
-apply auto
+apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto)
done
lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
-apply (auto dest: real_inverse_less_swap)
-done
+by (auto dest: real_inverse_less_swap)
lemma real_of_nat_gt_zero_cancel_iff: "(0 < real (n::nat)) = (0 < n)"
-apply (rule real_of_nat_less_iff [THEN subst])
-apply auto
-done
+by (rule real_of_nat_less_iff [THEN subst], auto)
declare real_of_nat_gt_zero_cancel_iff [simp]
lemma real_of_nat_le_zero_cancel_iff: "(real (n::nat) <= 0) = (n = 0)"
apply (rule real_of_nat_zero [THEN subst])
-apply (subst real_of_nat_le_iff)
-apply auto
+apply (subst real_of_nat_le_iff, auto)
done
declare real_of_nat_le_zero_cancel_iff [simp]
@@ -689,19 +818,98 @@
apply (auto simp add: real_of_nat_Suc)
done
-(*RING AND FIELD*)
- lemma mult_less_imp_less_left:
- "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
- by (force elim: order_less_asym simp add: mult_less_cancel_left)
-
- lemma mult_less_imp_less_right:
- "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
- by (force elim: order_less_asym simp add: mult_less_cancel_right)
-
ML
{*
val real_abs_def = thm "real_abs_def";
+val real_less_eq_diff = thm "real_less_eq_diff";
+
+val real_add_right_cancel = thm"real_add_right_cancel";
+val real_mult_congruent2_lemma = thm"real_mult_congruent2_lemma";
+val real_mult_congruent2 = thm"real_mult_congruent2";
+val real_mult = thm"real_mult";
+val real_mult_commute = thm"real_mult_commute";
+val real_mult_assoc = thm"real_mult_assoc";
+val real_mult_left_commute = thm"real_mult_left_commute";
+val real_mult_1 = thm"real_mult_1";
+val real_mult_1_right = thm"real_mult_1_right";
+val real_mult_0 = thm"real_mult_0";
+val real_mult_0_right = thm"real_mult_0_right";
+val real_mult_minus_eq1 = thm"real_mult_minus_eq1";
+val real_minus_mult_eq1 = thm"real_minus_mult_eq1";
+val real_mult_minus_eq2 = thm"real_mult_minus_eq2";
+val real_minus_mult_eq2 = thm"real_minus_mult_eq2";
+val real_mult_minus_1 = thm"real_mult_minus_1";
+val real_mult_minus_1_right = thm"real_mult_minus_1_right";
+val real_minus_mult_cancel = thm"real_minus_mult_cancel";
+val real_minus_mult_commute = thm"real_minus_mult_commute";
+val real_add_assoc_cong = thm"real_add_assoc_cong";
+val real_add_mult_distrib = thm"real_add_mult_distrib";
+val real_add_mult_distrib2 = thm"real_add_mult_distrib2";
+val real_diff_mult_distrib = thm"real_diff_mult_distrib";
+val real_diff_mult_distrib2 = thm"real_diff_mult_distrib2";
+val real_zero_not_eq_one = thm"real_zero_not_eq_one";
+val real_zero_iff = thm"real_zero_iff";
+val preal_le_linear = thm"preal_le_linear";
+val real_mult_inv_right_ex = thm"real_mult_inv_right_ex";
+val real_mult_inv_left_ex = thm"real_mult_inv_left_ex";
+val real_mult_inv_left = thm"real_mult_inv_left";
+val real_mult_inv_right = thm"real_mult_inv_right";
+val preal_lemma_eq_rev_sum = thm"preal_lemma_eq_rev_sum";
+val preal_add_left_commute_cancel = thm"preal_add_left_commute_cancel";
+val preal_lemma_for_not_refl = thm"preal_lemma_for_not_refl";
+val real_less_not_refl = thm"real_less_not_refl";
+val real_less_irrefl = thm"real_less_irrefl";
+val real_not_refl2 = thm"real_not_refl2";
+val preal_lemma_trans = thm"preal_lemma_trans";
+val real_less_trans = thm"real_less_trans";
+val real_less_not_sym = thm"real_less_not_sym";
+val real_less_asym = thm"real_less_asym";
+val real_of_preal_add = thm"real_of_preal_add";
+val real_of_preal_mult = thm"real_of_preal_mult";
+val real_of_preal_ExI = thm"real_of_preal_ExI";
+val real_of_preal_ExD = thm"real_of_preal_ExD";
+val real_of_preal_iff = thm"real_of_preal_iff";
+val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
+val real_of_preal_trichotomyE = thm"real_of_preal_trichotomyE";
+val real_of_preal_lessD = thm"real_of_preal_lessD";
+val real_of_preal_lessI = thm"real_of_preal_lessI";
+val real_of_preal_less_iff1 = thm"real_of_preal_less_iff1";
+val real_of_preal_minus_less_self = thm"real_of_preal_minus_less_self";
+val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
+val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
+val real_of_preal_zero_less = thm"real_of_preal_zero_less";
+val real_of_preal_not_less_zero = thm"real_of_preal_not_less_zero";
+val real_minus_minus_zero_less = thm"real_minus_minus_zero_less";
+val real_of_preal_sum_zero_less = thm"real_of_preal_sum_zero_less";
+val real_of_preal_minus_less_all = thm"real_of_preal_minus_less_all";
+val real_of_preal_not_minus_gt_all = thm"real_of_preal_not_minus_gt_all";
+val real_of_preal_minus_less_rev1 = thm"real_of_preal_minus_less_rev1";
+val real_of_preal_minus_less_rev2 = thm"real_of_preal_minus_less_rev2";
+val real_of_preal_minus_less_rev_iff = thm"real_of_preal_minus_less_rev_iff";
+val real_linear = thm"real_linear";
+val real_neq_iff = thm"real_neq_iff";
+val real_linear_less2 = thm"real_linear_less2";
+val real_leI = thm"real_leI";
+val real_leD = thm"real_leD";
+val real_leE = thm"real_leE";
+val real_less_le_iff = thm"real_less_le_iff";
+val not_real_leE = thm"not_real_leE";
+val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
+val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le";
+val real_le_less = thm"real_le_less";
+val real_le_refl = thm"real_le_refl";
+val real_le_linear = thm"real_le_linear";
+val real_le_trans = thm"real_le_trans";
+val real_le_anti_sym = thm"real_le_anti_sym";
+val real_less_le = thm"real_less_le";
+val real_minus_zero_less_iff = thm"real_minus_zero_less_iff";
+val real_minus_zero_less_iff2 = thm"real_minus_zero_less_iff2";
+val real_less_add_positive_left_Ex = thm"real_less_add_positive_left_Ex";
+val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
+val real_sum_gt_zero_less = thm"real_sum_gt_zero_less";
+val real_less_sum_gt_0_iff = thm"real_less_sum_gt_0_iff";
+
val real_minus_diff_eq = thm "real_minus_diff_eq";
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
@@ -727,7 +935,6 @@
val real_add_order = thm "real_add_order";
val real_le_add_order = thm "real_le_add_order";
val real_add_less_mono = thm "real_add_less_mono";
-val real_add_left_le_mono1 = thm "real_add_left_le_mono1";
val real_add_le_mono = thm "real_add_le_mono";
val real_le_minus_iff = thm "real_le_minus_iff";
val real_le_square = thm "real_le_square";
@@ -820,6 +1027,13 @@
val real_minus_divide_eq = thm"real_minus_divide_eq";
val real_divide_minus_eq = thm"real_divide_minus_eq";
val real_add_divide_distrib = thm"real_add_divide_distrib";
+
+val diff_less_eq = thm"diff_less_eq";
+val less_diff_eq = thm"less_diff_eq";
+val diff_eq_eq = thm"diff_eq_eq";
+val diff_le_eq = thm"diff_le_eq";
+val le_diff_eq = thm"le_diff_eq";
+val compare_rls = thms "compare_rls";
*}
end
--- a/src/HOL/Ring_and_Field.thy Fri Nov 28 12:09:37 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Tue Dec 02 11:48:15 2003 +0100
@@ -50,7 +50,7 @@
divide_zero [simp]: "a / 0 = 0"
-subsection {* Derived rules for addition *}
+subsection {* Derived Rules for Addition *}
lemma right_zero [simp]: "a + 0 = (a::'a::semiring)"
proof -
@@ -81,9 +81,6 @@
thus "a - b = 0" by (simp add: diff_minus)
qed
-lemma diff_self [simp]: "a - (a::'a::ring) = 0"
- by (simp add: diff_minus)
-
lemma add_left_cancel [simp]:
"(a + b = a + c) = (b = (c::'a::ring))"
proof
@@ -114,6 +111,15 @@
lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
by (simp add: equals_zero_I)
+lemma diff_self [simp]: "a - (a::'a::ring) = 0"
+ by (simp add: diff_minus)
+
+lemma diff_0 [simp]: "(0::'a::ring) - a = -a"
+by (simp add: diff_minus)
+
+lemma diff_0_right [simp]: "a - (0::'a::ring) = a"
+by (simp add: diff_minus)
+
lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
proof
assume "- a = - b"
@@ -147,7 +153,7 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
lemma right_inverse [simp]:
- assumes not0: "a ~= 0" shows "a * inverse (a::'a::field) = 1"
+ assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
proof -
have "a * inverse a = inverse a * a" by (simp add: mult_ac)
also have "... = 1" using not0 by simp
@@ -215,8 +221,11 @@
by (simp add: right_distrib diff_minus
minus_mult_left [symmetric] minus_mult_right [symmetric])
+lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)"
+by (simp add: diff_minus add_commute)
-subsection {* Ordering rules *}
+
+subsection {* Ordering Rules for Addition *}
lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
by (simp add: add_commute [of _ c] add_left_mono)
@@ -241,6 +250,47 @@
apply (erule add_strict_left_mono)
done
+lemma add_less_imp_less_left:
+ assumes less: "c + a < c + b" shows "a < (b::'a::ordered_ring)"
+ proof -
+ have "-c + (c + a) < -c + (c + b)"
+ by (rule add_strict_left_mono [OF less])
+ thus "a < b" by (simp add: add_assoc [symmetric])
+ qed
+
+lemma add_less_imp_less_right:
+ "a + c < b + c ==> a < (b::'a::ordered_ring)"
+apply (rule add_less_imp_less_left [of c])
+apply (simp add: add_commute)
+done
+
+lemma add_less_cancel_left [simp]:
+ "(c+a < c+b) = (a < (b::'a::ordered_ring))"
+by (blast intro: add_less_imp_less_left add_strict_left_mono)
+
+lemma add_less_cancel_right [simp]:
+ "(a+c < b+c) = (a < (b::'a::ordered_ring))"
+by (blast intro: add_less_imp_less_right add_strict_right_mono)
+
+lemma add_le_cancel_left [simp]:
+ "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_ring))"
+by (simp add: linorder_not_less [symmetric])
+
+lemma add_le_cancel_right [simp]:
+ "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_ring))"
+by (simp add: linorder_not_less [symmetric])
+
+lemma add_le_imp_le_left:
+ "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
+by simp
+
+lemma add_le_imp_le_right:
+ "a + c \<le> b + c ==> a \<le> (b::'a::ordered_ring)"
+by simp
+
+
+subsection {* Ordering Rules for Unary Minus *}
+
lemma le_imp_neg_le:
assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
proof -
@@ -280,6 +330,67 @@
lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
by (subst neg_less_iff_less [symmetric], simp)
+
+subsection{*Subtraction Laws*}
+
+lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ring)"
+by (simp add: diff_minus add_ac)
+
+lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ring)"
+by (simp add: diff_minus add_ac)
+
+lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ring))"
+by (auto simp add: diff_minus add_assoc)
+
+lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ring) = c)"
+by (auto simp add: diff_minus add_assoc)
+
+lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ring))"
+by (simp add: diff_minus add_ac)
+
+lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ring)"
+by (simp add: diff_minus add_ac)
+
+text{*Further subtraction laws for ordered rings*}
+
+lemma less_eq_diff: "(a < b) = (a - b < (0::'a::ordered_ring))"
+proof -
+ have "(a < b) = (a + (- b) < b + (-b))"
+ by (simp only: add_less_cancel_right)
+ also have "... = (a - b < 0)" by (simp add: diff_minus)
+ finally show ?thesis .
+qed
+
+lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))"
+apply (subst less_eq_diff)
+apply (rule less_eq_diff [of _ c, THEN ssubst])
+apply (simp add: diff_minus add_ac)
+done
+
+lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)"
+apply (subst less_eq_diff)
+apply (rule less_eq_diff [of _ "c-b", THEN ssubst])
+apply (simp add: diff_minus add_ac)
+done
+
+lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::ordered_ring))"
+by (simp add: linorder_not_less [symmetric] less_diff_eq)
+
+lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::ordered_ring) \<le> c)"
+by (simp add: linorder_not_less [symmetric] diff_less_eq)
+
+text{*This list of rewrites simplifies (in)equalities by bringing subtractions
+ to the top and then moving negative terms to the other side.
+ Use with @{text add_ac}*}
+lemmas compare_rls =
+ diff_minus [symmetric]
+ add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
+ diff_less_eq less_diff_eq diff_le_eq le_diff_eq
+ diff_eq_eq eq_diff_eq
+
+
+subsection {* Ordering Rules for Multiplication *}
+
lemma mult_strict_right_mono:
"[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_semiring)"
by (simp add: mult_commute [of _ c] mult_strict_left_mono)
@@ -484,6 +595,21 @@
subsection {* Fields *}
+text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
+ of an ordering.*}
+lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
+ proof cases
+ assume "a=0" thus ?thesis by simp
+ next
+ assume anz [simp]: "a\<noteq>0"
+ thus ?thesis
+ proof auto
+ assume "a * b = 0"
+ hence "inverse a * (a * b) = 0" by simp
+ thus "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])
+ qed
+ qed
+
text{*Cancellation of equalities with a common factor*}
lemma field_mult_cancel_right_lemma:
assumes cnz: "c \<noteq> (0::'a::field)"
@@ -578,6 +704,67 @@
"(inverse a = inverse b) = (a = (b::'a::{field,division_by_zero}))"
by (force dest!: inverse_eq_imp_eq)
+lemma nonzero_inverse_inverse_eq:
+ assumes [simp]: "a \<noteq> 0" shows "inverse(inverse (a::'a::field)) = a"
+ proof -
+ have "(inverse (inverse a) * inverse a) * a = a"
+ by (simp add: nonzero_imp_inverse_nonzero)
+ thus ?thesis
+ by (simp add: mult_assoc)
+ qed
+
+lemma inverse_inverse_eq [simp]:
+ "inverse(inverse (a::'a::{field,division_by_zero})) = a"
+ proof cases
+ assume "a=0" thus ?thesis by simp
+ next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
+ qed
+
+lemma inverse_1 [simp]: "inverse 1 = (1::'a::field)"
+ proof -
+ have "inverse 1 * 1 = (1::'a::field)"
+ by (rule left_inverse [OF zero_neq_one [symmetric]])
+ thus ?thesis by simp
+ qed
+
+lemma nonzero_inverse_mult_distrib:
+ assumes anz: "a \<noteq> 0"
+ and bnz: "b \<noteq> 0"
+ shows "inverse(a*b) = inverse(b) * inverse(a::'a::field)"
+ proof -
+ have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)"
+ by (simp add: field_mult_eq_0_iff anz bnz)
+ hence "inverse(a*b) * a = inverse(b)"
+ by (simp add: mult_assoc bnz)
+ hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)"
+ by simp
+ thus ?thesis
+ by (simp add: mult_assoc anz)
+ qed
+
+text{*This version builds in division by zero while also re-orienting
+ the right-hand side.*}
+lemma inverse_mult_distrib [simp]:
+ "inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
+ proof cases
+ assume "a \<noteq> 0 & b \<noteq> 0"
+ thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
+ next
+ assume "~ (a \<noteq> 0 & b \<noteq> 0)"
+ thus ?thesis by force
+ qed
+
+text{*There is no slick version using division by zero.*}
+lemma inverse_add:
+ "[|a \<noteq> 0; b \<noteq> 0|]
+ ==> inverse a + inverse b = (a+b) * inverse a * inverse (b::'a::field)"
+apply (simp add: left_distrib mult_assoc)
+apply (simp add: mult_commute [of "inverse a"])
+apply (simp add: mult_assoc [symmetric] add_commute)
+done
+
subsection {* Ordered Fields *}