# HG changeset patch
# User huffman
# Date 1316725936 25200
# Node ID c478d187637140d40aeaeef38be8b063f2043952
# Parent  f65593159ee816f761b489fe0b524d72d2b5dc07
discontinued legacy theorem names from RealDef.thy

diff -r f65593159ee8 -r c478d1876371 NEWS
--- 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
diff -r f65593159ee8 -r c478d1876371 src/HOL/Deriv.thy
--- 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
diff -r f65593159ee8 -r c478d1876371 src/HOL/Import/HOLLightReal.thy
--- 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)"
diff -r f65593159ee8 -r c478d1876371 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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"
diff -r f65593159ee8 -r c478d1876371 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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
diff -r f65593159ee8 -r c478d1876371 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r f65593159ee8 -r c478d1876371 src/HOL/RealDef.thy
--- 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