# HG changeset patch
# User huffman
# Date 1273452463 25200
# Node ID be5461582d0f92acb7bfac4d94268dff0b8369d3
# Parent  c137ae7673d3f6c3585273e1ba1ae74d7465b68e
avoid using real-specific versions of generic lemmas

diff -r c137ae7673d3 -r be5461582d0f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Complex.thy	Sun May 09 17:47:43 2010 -0700
@@ -676,12 +676,12 @@
 by (simp add: divide_inverse rcis_def)
 
 lemma cis_divide: "cis a / cis b = cis (a - b)"
-by (simp add: complex_divide_def cis_mult real_diff_def)
+by (simp add: complex_divide_def cis_mult diff_def)
 
 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
 apply (simp add: complex_divide_def)
 apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult real_diff_def)
+apply (simp add: rcis_inverse rcis_mult diff_def)
 done
 
 lemma Re_cis [simp]: "Re(cis a) = cos a"
diff -r c137ae7673d3 -r be5461582d0f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Deriv.thy	Sun May 09 17:47:43 2010 -0700
@@ -482,8 +482,7 @@
   shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
 apply (rule linorder_not_less [THEN iffD1])
 apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
-apply (drule real_less_sum_gt_zero)
-apply (drule_tac x = "f n + - lim f" in spec, safe)
+apply (drule_tac x = "f n - lim f" in spec, clarsimp)
 apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
 apply (subgoal_tac "lim f \<le> f (no + n) ")
 apply (drule_tac no=no and m=n in lemma_f_mono_add)
@@ -706,7 +705,7 @@
 apply safe
 apply simp_all
 apply (rename_tac x xa ya M Ma)
-apply (metis linorder_not_less order_le_less real_le_trans)
+apply (metis linorder_not_less order_le_less order_trans)
 apply (case_tac "a \<le> x & x \<le> b")
  prefer 2
  apply (rule_tac x = 1 in exI, force)
@@ -1235,16 +1234,16 @@
       using assms
       apply auto
       apply (metis DERIV_isCont)
-     apply (metis differentiableI real_less_def)
+     apply (metis differentiableI less_le)
     done
   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
     by auto
   
   from prems have "~(l > 0)"
-    by (metis linorder_not_le mult_le_0_iff real_le_eq_diff)
+    by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
   with prems show False
-    by (metis DERIV_unique real_less_def)
+    by (metis DERIV_unique less_le)
 qed
 
 lemma DERIV_nonneg_imp_nonincreasing:
@@ -1264,13 +1263,13 @@
     apply (rule MVT)
       apply auto
       apply (metis DERIV_isCont)
-     apply (metis differentiableI real_less_def)
+     apply (metis differentiableI less_le)
     done
   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
     by auto
   from prems have "~(l >= 0)"
-    by (metis diff_self le_eqI le_iff_diff_le_0 real_le_antisym real_le_linear
+    by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
               split_mult_pos_le)
   with prems show False
     by (metis DERIV_unique order_less_imp_le)
diff -r c137ae7673d3 -r be5461582d0f src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Ln.thy	Sun May 09 17:47:43 2010 -0700
@@ -206,7 +206,7 @@
     apply auto
     done
   also have "... = exp (-x)"
-    by (auto simp add: exp_minus real_divide_def)
+    by (auto simp add: exp_minus divide_inverse)
   finally have "1 - x <= exp (- x)" .
   also have "1 - x = exp (ln (1 - x))"
   proof -
diff -r c137ae7673d3 -r be5461582d0f src/HOL/Log.thy
--- a/src/HOL/Log.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Log.thy	Sun May 09 17:47:43 2010 -0700
@@ -64,7 +64,7 @@
 by (simp add: powr_def)
 
 lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
-by (simp add: powr_powr real_mult_commute)
+by (simp add: powr_powr mult_commute)
 
 lemma powr_minus: "x powr (-a) = inverse (x powr a)"
 by (simp add: powr_def exp_minus [symmetric])
diff -r c137ae7673d3 -r be5461582d0f src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/RealPow.thy	Sun May 09 17:47:43 2010 -0700
@@ -95,7 +95,7 @@
 by (intro add_nonneg_nonneg zero_le_power2)
 
 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
-by (rule_tac j = 0 in real_le_trans, auto)
+by (rule_tac y = 0 in order_trans, auto)
 
 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
 by (auto simp add: power2_eq_square)
@@ -145,7 +145,7 @@
      "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
       ==> inverse x * y < inverse x1 * u"
 apply (rule_tac c=x in mult_less_imp_less_left) 
-apply (auto simp add: real_mult_assoc [symmetric])
+apply (auto simp add: mult_assoc [symmetric])
 apply (simp (no_asm) add: mult_ac)
 apply (rule_tac c=x1 in mult_less_imp_less_right) 
 apply (auto simp add: mult_ac)
diff -r c137ae7673d3 -r be5461582d0f src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/SupInf.thy	Sun May 09 17:47:43 2010 -0700
@@ -74,7 +74,7 @@
 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
   fixes x :: real
   shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
-  by (metis Sup_upper real_le_trans)
+  by (metis Sup_upper order_trans)
 
 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
   fixes z :: real
@@ -86,7 +86,7 @@
   shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
         \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
   by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
-        insert_not_empty real_le_antisym)
+        insert_not_empty order_antisym)
 
 lemma Sup_le:
   fixes S :: "real set"
@@ -109,28 +109,28 @@
     apply (simp add: max_def)
     apply (rule Sup_eq_maximum)
     apply (rule insertI1)
-    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
+    apply (metis Sup_upper [OF _ z] insertE linear order_trans)
     done
 next
   case False
   hence 1:"a < Sup X" by simp
   have "Sup X \<le> Sup (insert a X)"
     apply (rule Sup_least)
-    apply (metis empty_psubset_nonempty psubset_eq x)
+    apply (metis ex_in_conv x)
     apply (rule Sup_upper_EX) 
     apply blast
-    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+    apply (metis insert_iff linear order_refl order_trans z)
     done
   moreover 
   have "Sup (insert a X) \<le> Sup X"
     apply (rule Sup_least)
     apply blast
-    apply (metis False Sup_upper insertE real_le_linear z) 
+    apply (metis False Sup_upper insertE linear z)
     done
   ultimately have "Sup (insert a X) = Sup X"
     by (blast intro:  antisym )
   thus ?thesis
-    by (metis 1 min_max.le_iff_sup real_less_def)
+    by (metis 1 min_max.le_iff_sup less_le)
 qed
 
 lemma Sup_insert_if: 
@@ -177,7 +177,7 @@
   fixes S :: "real set"
   assumes fS: "finite S" and Se: "S \<noteq> {}"
   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
 
 lemma Sup_finite_gt_iff: 
   fixes S :: "real set"
@@ -291,19 +291,19 @@
 lemma Inf_lower2:
   fixes x :: real
   shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
-  by (metis Inf_lower real_le_trans)
+  by (metis Inf_lower order_trans)
 
 lemma Inf_real_iff:
   fixes z :: real
   shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
-  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
+  by (metis Inf_greatest Inf_lower less_le_not_le linear
             order_less_le_trans)
 
 lemma Inf_eq:
   fixes a :: real
   shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
   by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
-        insert_absorb insert_not_empty real_le_antisym)
+        insert_absorb insert_not_empty order_antisym)
 
 lemma Inf_ge: 
   fixes S :: "real set"
@@ -324,27 +324,27 @@
   case True
   thus ?thesis
     by (simp add: min_def)
-       (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
+       (blast intro: Inf_eq_minimum order_trans z)
 next
   case False
   hence 1:"Inf X < a" by simp
   have "Inf (insert a X) \<le> Inf X"
     apply (rule Inf_greatest)
-    apply (metis empty_psubset_nonempty psubset_eq x)
+    apply (metis ex_in_conv x)
     apply (rule Inf_lower_EX)
     apply (erule insertI2)
-    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+    apply (metis insert_iff linear order_refl order_trans z)
     done
   moreover 
   have "Inf X \<le> Inf (insert a X)"
     apply (rule Inf_greatest)
     apply blast
-    apply (metis False Inf_lower insertE real_le_linear z) 
+    apply (metis False Inf_lower insertE linear z) 
     done
   ultimately have "Inf (insert a X) = Inf X"
     by (blast intro:  antisym )
   thus ?thesis
-    by (metis False min_max.inf_absorb2 real_le_linear)
+    by (metis False min_max.inf_absorb2 linear)
 qed
 
 lemma Inf_insert_if: 
@@ -377,13 +377,13 @@
 lemma Inf_finite_ge_iff: 
   fixes S :: "real set"
   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
+by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
 
 lemma Inf_finite_le_iff:
   fixes S :: "real set"
   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
-          real_le_antisym real_le_linear)
+          order_antisym linear)
 
 lemma Inf_finite_gt_iff: 
   fixes S :: "real set"
@@ -417,7 +417,7 @@
   also have "... \<le> e" 
     apply (rule Sup_asclose) 
     apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
+    apply (metis abs_minus_add_cancel b add_commute diff_def)
     done
   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   thus ?thesis
@@ -474,13 +474,13 @@
 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
     by (rule SupInf.Sup_upper [where z=b], auto)
-       (metis `a < b` `\<not> P b` real_le_linear real_less_def)
+       (metis `a < b` `\<not> P b` linear less_le)
 next
   show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
     apply (rule SupInf.Sup_least) 
     apply (auto simp add: )
     apply (metis less_le_not_le)
-    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
+    apply (metis `a<b` `~ P b` linear less_le)
     done
 next
   fix x
@@ -495,7 +495,7 @@
     assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
     thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
       by (rule_tac z="b" in SupInf.Sup_upper, auto) 
-         (metis `a<b` `~ P b` real_le_linear real_less_def) 
+         (metis `a<b` `~ P b` linear less_le)
 qed
 
 end
diff -r c137ae7673d3 -r be5461582d0f src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun May 09 14:21:44 2010 -0700
+++ b/src/HOL/Transcendental.thy	Sun May 09 17:47:43 2010 -0700
@@ -779,7 +779,7 @@
             finally show "\<bar>\<Sum>p = 0..<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>" unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF `0 < R'`]]] .
             show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult[symmetric] by auto
           qed
-          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
+          also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult mult_assoc[symmetric] by algebra
           finally show ?thesis .
         qed }
       { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
@@ -792,7 +792,7 @@
           show "\<bar>f n * x ^ n\<bar> \<le> norm (f n * real (Suc n) * x ^ n)" unfolding real_norm_def abs_mult
             by (rule mult_right_mono, auto simp add: le[unfolded mult_1_right])
         qed
-        from this[THEN summable_mult2[where c=x], unfolded real_mult_assoc, unfolded real_mult_commute]
+        from this[THEN summable_mult2[where c=x], unfolded mult_assoc, unfolded mult_commute]
         show "summable (?f x)" by auto }
       show "summable (?f' x0)" using converges[OF `x0 \<in> {-R <..< R}`] .
       show "x0 \<in> {-R' <..< R'}" using `x0 \<in> {-R' <..< R'}` .
@@ -1022,7 +1022,7 @@
 lemma exp_ge_add_one_self_aux: "0 \<le> (x::real) ==> (1 + x) \<le> exp(x)"
 apply (drule order_le_imp_less_or_eq, auto)
 apply (simp add: exp_def)
-apply (rule real_le_trans)
+apply (rule order_trans)
 apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
 apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
 done
@@ -1228,7 +1228,7 @@
     have "1 / x = 1 / (1 - (1 - x))" by auto
     also have "\<dots> = (\<Sum> n. (1 - x)^n)" using geometric_sums[OF `norm (1 - x) < 1`] by (rule sums_unique)
     also have "\<dots> = suminf (?f' x)" unfolding power_mult_distrib[symmetric] by (rule arg_cong[where f=suminf], rule arg_cong[where f="op ^"], auto)
-    finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding real_divide_def by auto
+    finally have "DERIV ln x :> suminf (?f' x)" using DERIV_ln[OF `0 < x`] unfolding divide_inverse by auto
     moreover
     have repos: "\<And> h x :: real. h - 1 + x = h + x - 1" by auto
     have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> (\<Sum>n. (-1)^n * (1 / real (n + 1)) * real (Suc n) * (x - 1) ^ n)"
@@ -1388,7 +1388,7 @@
 
 lemma DERIV_sin_realpow2 [simp]:
      "DERIV (%x. (sin x)\<twosuperior>) x :> cos(x) * sin(x) + cos(x) * sin(x)"
-by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
+by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
 
 lemma DERIV_sin_realpow2a [simp]:
      "DERIV (%x. (sin x)\<twosuperior>) x :> 2 * cos(x) * sin(x)"
@@ -1406,7 +1406,7 @@
 
 lemma DERIV_cos_realpow2 [simp]:
      "DERIV (%x. (cos x)\<twosuperior>) x :> -sin(x) * cos(x) + -sin(x) * cos(x)"
-by (auto simp add: numeral_2_eq_2 real_mult_assoc [symmetric])
+by (auto simp add: numeral_2_eq_2 mult_assoc [symmetric])
 
 lemma DERIV_cos_realpow2a [simp]:
      "DERIV (%x. (cos x)\<twosuperior>) x :> -2 * cos(x) * sin(x)"
@@ -1705,8 +1705,8 @@
 apply (drule_tac f = cos in Rolle)
 apply (drule_tac [5] f = cos in Rolle)
 apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
-apply (metis order_less_le_trans real_less_def sin_gt_zero)
-apply (metis order_less_le_trans real_less_def sin_gt_zero)
+apply (metis order_less_le_trans less_le sin_gt_zero)
+apply (metis order_less_le_trans less_le sin_gt_zero)
 done
 
 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
@@ -2138,9 +2138,9 @@
 apply (auto simp add: tan_def)
 apply (rule inverse_less_iff_less [THEN iffD1])
 apply (auto simp add: divide_inverse)
-apply (rule real_mult_order) 
+apply (rule mult_pos_pos)
 apply (subgoal_tac [3] "0 < sin e & 0 < cos e")
-apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute) 
+apply (auto intro: cos_gt_zero sin_gt_zero2 simp add: mult_commute)
 done
 
 lemma tan_total_pos: "0 \<le> y ==> \<exists>x. 0 \<le> x & x < pi/2 & tan x = y"
@@ -2193,7 +2193,7 @@
   hence "0 < cos z" using cos_gt_zero_pi by auto
   hence inv_pos: "0 < inverse ((cos z)\<twosuperior>)" by auto
   have "0 < x - y" using `y < x` by auto
-  from real_mult_order[OF this inv_pos]
+  from mult_pos_pos [OF this inv_pos]
   have "0 < tan x - tan y" unfolding tan_diff by auto
   thus ?thesis by auto
 qed
@@ -2226,7 +2226,7 @@
 lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x" 
 proof (induct n arbitrary: x)
   case (Suc n)
-  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
   show ?case unfolding split_pi_off using Suc by auto
 qed auto
 
@@ -2439,7 +2439,7 @@
 apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
 apply (erule (1) isCont_inverse_function2 [where f=tan])
 apply (metis arctan_tan order_le_less_trans order_less_le_trans)
-apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans real_less_def)
+apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
 done
 
 lemma DERIV_arcsin:
@@ -2953,7 +2953,7 @@
       }
       hence "\<forall> x \<in> { 0 <..< 1 }. 0 \<le> ?a x n - ?diff x n" by auto
       moreover have "\<And>x. isCont (\<lambda> x. ?a x n - ?diff x n) x"
-        unfolding real_diff_def divide_inverse
+        unfolding diff_def divide_inverse
         by (auto intro!: isCont_add isCont_rabs isCont_ident isCont_minus isCont_arctan isCont_inverse isCont_mult isCont_power isCont_const isCont_setsum)
       ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
       hence "?diff 1 n \<le> ?a 1 n" by auto
@@ -2969,7 +2969,7 @@
         have "norm (?diff 1 n - 0) < r" by auto }
       thus "\<exists> N. \<forall> n \<ge> N. norm (?diff 1 n - 0) < r" by blast
     qed
-    from this[unfolded LIMSEQ_rabs_zero real_diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
+    from this[unfolded LIMSEQ_rabs_zero diff_def add_commute[of "arctan 1"], THEN LIMSEQ_add_const, of "- arctan 1", THEN LIMSEQ_minus]
     have "(?c 1) sums (arctan 1)" unfolding sums_def by auto
     hence "arctan 1 = (\<Sum> i. ?c 1 i)" by (rule sums_unique)