--- a/NEWS Thu Sep 22 13:17:14 2011 -0700
+++ b/NEWS Thu Sep 22 14:12:16 2011 -0700
@@ -180,6 +180,26 @@
* Theory Complex_Main: Several redundant theorems have been removed or
replaced by more general versions. INCOMPATIBILITY.
+ real_diff_def ~> minus_real_def
+ real_divide_def ~> divide_real_def
+ real_less_def ~> less_le
+ real_abs_def ~> abs_real_def
+ real_sgn_def ~> sgn_real_def
+ real_mult_commute ~> mult_commute
+ real_mult_assoc ~> mult_assoc
+ real_mult_1 ~> mult_1_left
+ real_add_mult_distrib ~> left_distrib
+ real_zero_not_eq_one ~> zero_neq_one
+ real_mult_inverse_left ~> left_inverse
+ INVERSE_ZERO ~> inverse_zero
+ real_le_refl ~> order_refl
+ real_le_antisym ~> order_antisym
+ real_le_trans ~> order_trans
+ real_le_linear ~> linear
+ real_le_eq_diff ~> le_iff_diff_le_0
+ real_add_left_mono ~> add_left_mono
+ real_mult_order ~> mult_pos_pos
+ real_mult_less_mono2 ~> mult_strict_left_mono
real_of_int_real_of_nat ~> real_of_int_of_nat_eq
real_0_le_divide_iff ~> zero_le_divide_iff
realpow_two_disj ~> power2_eq_iff
--- a/src/HOL/Deriv.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/Deriv.thy Thu Sep 22 14:12:16 2011 -0700
@@ -1247,7 +1247,7 @@
by auto
with A have "a < b" "f b < f a" by auto
with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
- (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
+ (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl)
with assms z show False
by (metis DERIV_unique order_less_imp_le)
qed
--- a/src/HOL/Import/HOLLightReal.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/Import/HOLLightReal.thy Thu Sep 22 14:12:16 2011 -0700
@@ -233,7 +233,7 @@
lemma REAL_SUB_INV:
"(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
- by (simp add: division_ring_inverse_diff real_divide_def)
+ by (simp add: division_ring_inverse_diff divide_real_def)
lemma REAL_DOWN:
"0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 22 14:12:16 2011 -0700
@@ -2225,12 +2225,12 @@
by(auto simp add:euclidean_eq[where 'a='a] field_simps)
also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
also have "... < d" using as[unfolded dist_norm] and `e>0`
- by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
+ by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
finally have "y : S" apply(subst *)
apply(rule assms(1)[unfolded convex_alt,rule_format])
apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto
} hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto
-moreover have "0 < e*d" using `0<e` `0<d` using real_mult_order by auto
+moreover have "0 < e*d" using `0<e` `0<d` by (rule mult_pos_pos)
moreover have "c : S" using assms rel_interior_subset by auto
moreover hence "x - e *\<^sub>R (x - c) : S"
using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto
@@ -2439,7 +2439,7 @@
using assms RealVector.bounded_linear.pos_bounded[of f] by auto
def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)"
using K_def pos_le_divide_eq[of e1] by auto
- def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto
+ def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
{ fix y assume y_def: "y : cball x e Int affine hull S"
from this have h1: "f y : affine hull (f ` S)"
using affine_hull_linear_image[of f S] assms by auto
@@ -2469,7 +2469,7 @@
from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))"
using assms injective_imp_isometric[of "span S" f]
subspace_span[of S] closed_subspace[of "span S"] by auto
- def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto
+ def e == "e1 * e2" hence "e>0" using e1_def e2_def mult_pos_pos by auto
{ fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)"
from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto
from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto
@@ -4291,7 +4291,7 @@
finally show "0 < ?a $$ i" by auto
next have "setsum (op $$ ?a) ?D = setsum (\<lambda>i. inverse (2 * real (card d))) ?D"
by(rule setsum_cong2, rule **)
- also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat real_divide_def[THEN sym]
+ also have "\<dots> < 1" unfolding setsum_constant real_eq_of_nat divide_real_def[THEN sym]
by (auto simp add:field_simps)
finally show "setsum (op $$ ?a) ?D < 1" by auto
next fix i assume "i<DIM('a)" and "i~:d"
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Thu Sep 22 14:12:16 2011 -0700
@@ -667,7 +667,7 @@
using a[rule_format, of "{B<..}"] mono_greaterThan by auto
{ fix y assume "y:(S Int ball x d - {x})"
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
- by (metis dist_eq_0_iff real_less_def zero_le_dist)
+ by (metis dist_eq_0_iff less_le zero_le_dist)
hence "B <= f y" using d_def by auto
} hence "B <= INFI (S Int ball x d - {x}) f" apply (subst INF_greatest) by auto
also have "...<=?l" apply (subst SUP_upper) using d_def by auto
@@ -714,7 +714,7 @@
using a[rule_format, of "{..<B}"] by auto
{ fix y assume "y:(S Int ball x d - {x})"
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
- by (metis dist_eq_0_iff real_less_def zero_le_dist)
+ by (metis dist_eq_0_iff less_le zero_le_dist)
hence "f y <= B" using d_def by auto
} hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_least) by auto
moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_lower) using d_def by auto
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 22 14:12:16 2011 -0700
@@ -5634,7 +5634,7 @@
proof(cases "d = 0")
case True
have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
- by (metis mult_zero_left real_mult_commute real_mult_le_cancel_iff1)
+ by (metis mult_zero_left mult_commute real_mult_le_cancel_iff1)
from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def
by (simp add: *)
thus ?thesis using `e>0` by auto
--- a/src/HOL/RealDef.thy Thu Sep 22 13:17:14 2011 -0700
+++ b/src/HOL/RealDef.thy Thu Sep 22 14:12:16 2011 -0700
@@ -1049,33 +1049,6 @@
declare Abs_real_induct [induct del]
declare Abs_real_cases [cases del]
-subsection {* Legacy theorem names *}
-
-text {* TODO: Could we have a way to mark theorem names as deprecated,
-and have Isabelle issue a warning and display the preferred name? *}
-
-lemmas real_diff_def = minus_real_def [of "r" "s", standard]
-lemmas real_divide_def = divide_real_def [of "R" "S", standard]
-lemmas real_less_def = less_le [of "x::real" "y", standard]
-lemmas real_abs_def = abs_real_def [of "r", standard]
-lemmas real_sgn_def = sgn_real_def [of "x", standard]
-lemmas real_mult_commute = mult_commute [of "z::real" "w", standard]
-lemmas real_mult_assoc = mult_assoc [of "z1::real" "z2" "z3", standard]
-lemmas real_mult_1 = mult_1_left [of "z::real", standard]
-lemmas real_add_mult_distrib = left_distrib [of "z1::real" "z2" "w", standard]
-lemmas real_zero_not_eq_one = zero_neq_one [where 'a=real]
-lemmas real_mult_inverse_left = left_inverse [of "x::real", standard]
-lemmas INVERSE_ZERO = inverse_zero [where 'a=real]
-lemmas real_le_refl = order_refl [of "w::real", standard]
-lemmas real_le_antisym = order_antisym [of "z::real" "w", standard]
-lemmas real_le_trans = order_trans [of "i::real" "j" "k", standard]
-lemmas real_le_linear = linear [of "z::real" "w", standard]
-lemmas real_le_eq_diff = le_iff_diff_le_0 [of "x::real" "y", standard]
-lemmas real_add_left_mono = add_left_mono [of "x::real" "y" "z", standard]
-lemmas real_mult_order = mult_pos_pos [of "x::real" "y", standard]
-lemmas real_mult_less_mono2 =
- mult_strict_left_mono [of "x::real" "y" "z", COMP swap_prems_rl, standard]
-
subsection{*More Lemmas*}
text {* BH: These lemmas should not be necessary; they should be