removed some [iff] declarations from RealDef.thy, concerning inequalities
authorpaulson
Thu Jul 29 16:14:42 2004 +0200 (2004-07-29)
changeset 150855693a977a767
parent 15084 07f7b158ef32
child 15086 e6a2a98d5ef5
removed some [iff] declarations from RealDef.thy, concerning inequalities
src/HOL/Complex/CSeries.thy
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Log.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Complex/CSeries.thy	Thu Jul 29 16:14:06 2004 +0200
     1.2 +++ b/src/HOL/Complex/CSeries.thy	Thu Jul 29 16:14:42 2004 +0200
     1.3 @@ -146,28 +146,12 @@
     1.4  ***)
     1.5  
     1.6  lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
     1.7 -apply (induct_tac "n", auto)
     1.8 -apply (rule_tac j = 0 in real_le_trans, auto)
     1.9 -done
    1.10 +by (induct_tac "n", auto simp add: add_increasing) 
    1.11  
    1.12  lemma rabs_sumc_cmod_cancel [simp]:
    1.13       "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
    1.14  by (simp add: abs_if linorder_not_less)
    1.15  
    1.16 -lemma sumc_zero:
    1.17 -     "\<forall>n. N \<le> n --> f n = 0  
    1.18 -      ==> \<forall>m n. N \<le> m --> sumc m n f = 0"
    1.19 -apply safe
    1.20 -apply (induct_tac "n", auto)
    1.21 -done
    1.22 -
    1.23 -lemma fun_zero_sumc_zero:
    1.24 -     "\<forall>n. N \<le> n --> f (Suc n) = 0  
    1.25 -      ==> \<forall>m n. Suc N \<le> m --> sumc m n f = 0"
    1.26 -apply (rule sumc_zero, safe)
    1.27 -apply (drule_tac x = "n - 1" in spec, auto, arith)
    1.28 -done
    1.29 -
    1.30  lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
    1.31  apply (induct_tac "n")
    1.32  apply (case_tac [2] "n", auto)
    1.33 @@ -210,8 +194,6 @@
    1.34  val sumc_interval_const2 = thm "sumc_interval_const2";
    1.35  val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero";
    1.36  val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel";
    1.37 -val sumc_zero = thm "sumc_zero";
    1.38 -val fun_zero_sumc_zero = thm "fun_zero_sumc_zero";
    1.39  val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero";
    1.40  val sumc_diff = thm "sumc_diff";
    1.41  val sumc_subst = thm "sumc_subst";
     2.1 --- a/src/HOL/Complex/Complex.thy	Thu Jul 29 16:14:06 2004 +0200
     2.2 +++ b/src/HOL/Complex/Complex.thy	Thu Jul 29 16:14:42 2004 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  header {* Complex Numbers: Rectangular and Polar Representations *}
     2.6  
     2.7 -theory Complex = HLog:
     2.8 +theory Complex = "../Hyperreal/HLog":
     2.9  
    2.10  datatype complex = Complex real real
    2.11  
    2.12 @@ -440,7 +440,8 @@
    2.13  
    2.14  lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)"
    2.15  apply (induct x)
    2.16 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2
    2.17 +apply (auto iff: real_0_le_add_iff 
    2.18 +            intro: real_sum_squares_cancel real_sum_squares_cancel2
    2.19              simp add: complex_mod complex_zero_def power2_eq_square)
    2.20  done
    2.21  
    2.22 @@ -453,7 +454,7 @@
    2.23  
    2.24  lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
    2.25  apply (induct z, simp add: complex_mod complex_cnj complex_mult)
    2.26 -apply (simp add: power2_eq_square abs_if linorder_not_less)
    2.27 +apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff)
    2.28  done
    2.29  
    2.30  lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
    2.31 @@ -510,7 +511,7 @@
    2.32  lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)"
    2.33  apply (rule_tac n = 1 in realpow_increasing)
    2.34  apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
    2.35 -            simp add: power2_eq_square [symmetric])
    2.36 +            simp add: add_increasing power2_eq_square [symmetric])
    2.37  done
    2.38  
    2.39  lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
     3.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Jul 29 16:14:06 2004 +0200
     3.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Jul 29 16:14:42 2004 +0200
     3.3 @@ -988,8 +988,9 @@
     3.4  apply (simp add: hsgn hcmod hIm hypreal_divide)
     3.5  done
     3.6  
     3.7 +(*????move to RealDef????*)
     3.8  lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
     3.9 -by (auto intro: real_sum_squares_cancel)
    3.10 +by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
    3.11  
    3.12  lemma hcomplex_inverse_complex_split:
    3.13       "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
     4.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 29 16:14:06 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 29 16:14:42 2004 +0200
     4.3 @@ -7,7 +7,7 @@
     4.4  
     4.5  header{*Construction of Hyperreals Using Ultrafilters*}
     4.6  
     4.7 -theory HyperDef = Filter + Real
     4.8 +theory HyperDef = Filter + "../Real/Real"
     4.9  files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
    4.10  
    4.11  
     5.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Jul 29 16:14:06 2004 +0200
     5.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Jul 29 16:14:42 2004 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  header{*Exponentials on the Hyperreals*}
     5.6  
     5.7 -theory HyperPow = HyperArith + HyperNat + RealPow:
     5.8 +theory HyperPow = HyperArith + HyperNat + "../Real/RealPow":
     5.9  
    5.10  instance hypreal :: power ..
    5.11  
     6.1 --- a/src/HOL/Hyperreal/Log.thy	Thu Jul 29 16:14:06 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/Log.thy	Thu Jul 29 16:14:42 2004 +0200
     6.3 @@ -127,6 +127,61 @@
     6.4  by (simp add: linorder_not_less [symmetric])
     6.5  
     6.6  
     6.7 +subsection{*Further Results Courtesy Jeremy Avigad*}
     6.8 +
     6.9 +lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
    6.10 +  apply (induct n, simp)
    6.11 +  apply (subgoal_tac "real(Suc n) = real n + 1")
    6.12 +  apply (erule ssubst)
    6.13 +  apply (subst powr_add, simp, simp)
    6.14 +done
    6.15 +
    6.16 +lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0
    6.17 +  else x powr (real n))"
    6.18 +  apply (case_tac "x = 0", simp, simp)
    6.19 +  apply (rule powr_realpow [THEN sym], simp)
    6.20 +done
    6.21 +
    6.22 +lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    6.23 +by (unfold powr_def, simp)
    6.24 +
    6.25 +lemma ln_bound: "1 <= x ==> ln x <= x"
    6.26 +  apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
    6.27 +  apply simp
    6.28 +  apply (rule ln_add_one_self_le_self, simp)
    6.29 +done
    6.30 +
    6.31 +lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
    6.32 +  apply (case_tac "x = 1", simp)
    6.33 +  apply (case_tac "a = b", simp)
    6.34 +  apply (rule order_less_imp_le)
    6.35 +  apply (rule powr_less_mono, auto)
    6.36 +done
    6.37 +
    6.38 +lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
    6.39 +  apply (subst powr_zero_eq_one [THEN sym])
    6.40 +  apply (rule powr_mono, assumption+)
    6.41 +done
    6.42 +
    6.43 +lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a <
    6.44 +    y powr a"
    6.45 +  apply (unfold powr_def)
    6.46 +  apply (rule exp_less_mono)
    6.47 +  apply (rule mult_strict_left_mono)
    6.48 +  apply (subst ln_less_cancel_iff, assumption)
    6.49 +  apply (rule order_less_trans)
    6.50 +  prefer 2
    6.51 +  apply assumption+
    6.52 +done
    6.53 +
    6.54 +lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a";
    6.55 +  apply (case_tac "a = 0", simp)
    6.56 +  apply (case_tac "x = y", simp)
    6.57 +  apply (rule order_less_imp_le)
    6.58 +  apply (rule powr_less_mono2, auto)
    6.59 +done
    6.60 +
    6.61 +
    6.62  
    6.63  ML
    6.64  {*
     7.1 --- a/src/HOL/Hyperreal/NatStar.thy	Thu Jul 29 16:14:06 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Thu Jul 29 16:14:42 2004 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  
     7.5  header{*Star-transforms for the Hypernaturals*}
     7.6  
     7.7 -theory NatStar = RealPow + HyperPow:
     7.8 +theory NatStar = "../Real/RealPow" + HyperPow:
     7.9  
    7.10  
    7.11  text{*Extends sets of nats, and functions from the nats to nats or reals*}
     8.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Thu Jul 29 16:14:06 2004 +0200
     8.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Thu Jul 29 16:14:42 2004 +0200
     8.3 @@ -76,7 +76,8 @@
     8.4           0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n"
     8.5  apply safe
     8.6  apply (frule lemma_nth_realpow_seq, safe)
     8.7 -apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric])
     8.8 +apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric]
     8.9 +            iff: real_0_less_add_iff) --{*legacy iff rule!*}
    8.10  apply (simp add: linorder_not_less)
    8.11  apply (rule order_less_trans [of _ 0])
    8.12  apply (auto intro: lemma_nth_realpow_isLub_gt_zero)
    8.13 @@ -118,8 +119,7 @@
    8.14  
    8.15  lemma real_mult_add_one_minus_ge_zero:
    8.16       "0 < r ==>  0 <= r*(1 + -inverse(real (Suc n)))"
    8.17 -apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff)
    8.18 -done
    8.19 +by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff)
    8.20  
    8.21  lemma lemma_nth_realpow_isLub_le:
    8.22       "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;  
     9.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Jul 29 16:14:06 2004 +0200
     9.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Jul 29 16:14:42 2004 +0200
     9.3 @@ -796,7 +796,7 @@
     9.4  apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
     9.5  apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
     9.6  apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
     9.7 -apply (auto elim!: lemma_Nat_covered, arith+)
     9.8 +apply (auto elim!: lemma_Nat_covered)
     9.9  done
    9.10  
    9.11  text{*A Cauchy sequence is bounded -- nonstandard version*}
    10.1 --- a/src/HOL/Hyperreal/Series.thy	Thu Jul 29 16:14:06 2004 +0200
    10.2 +++ b/src/HOL/Hyperreal/Series.thy	Thu Jul 29 16:14:42 2004 +0200
    10.3 @@ -270,7 +270,8 @@
    10.4  apply (drule summable_sums)
    10.5  apply (auto simp add: sums_def LIMSEQ_def)
    10.6  apply (drule_tac x = "f (n) + f (n + 1) " in spec)
    10.7 -apply auto
    10.8 +apply (auto iff: real_0_less_add_iff)
    10.9 +   --{*legacy proof: not necessarily better!*}
   10.10  apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
   10.11  apply (frule_tac [2] no=no in sumr_pos_lt_pair_lemma) 
   10.12  apply (drule_tac x = 0 in spec, simp)
   10.13 @@ -291,11 +292,9 @@
   10.14  apply (auto simp add: linorder_not_less [symmetric])
   10.15  done
   10.16  
   10.17 -
   10.18 +text{*A summable series of positive terms has limit that is at least as
   10.19 +great as any partial sum.*}
   10.20  
   10.21 -(*-----------------------------------------------------------------
   10.22 -   Summable series of positive terms has limit >= any partial sum 
   10.23 - ----------------------------------------------------------------*)
   10.24  lemma series_pos_le: 
   10.25       "[| summable f; \<forall>m. n \<le> m --> 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
   10.26  apply (drule summable_sums)
   10.27 @@ -314,9 +313,7 @@
   10.28  apply (drule_tac x = m in spec, auto)
   10.29  done
   10.30  
   10.31 -(*-------------------------------------------------------------------
   10.32 -                    sum of geometric progression                 
   10.33 - -------------------------------------------------------------------*)
   10.34 +text{*Sum of a geometric progression.*}
   10.35  
   10.36  lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
   10.37  apply (induct_tac "n", auto)
   10.38 @@ -334,9 +331,8 @@
   10.39  apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
   10.40  done
   10.41  
   10.42 -(*-------------------------------------------------------------------
   10.43 -    Cauchy-type criterion for convergence of series (c.f. Harrison)
   10.44 - -------------------------------------------------------------------*)
   10.45 +text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   10.46 +
   10.47  lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
   10.48  by (simp add: summable_def sums_def convergent_def)
   10.49  
   10.50 @@ -355,14 +351,8 @@
   10.51              simp add: sumr_split_add_minus abs_minus_add_cancel)
   10.52  done
   10.53  
   10.54 -(*-------------------------------------------------------------------
   10.55 -     Terms of a convergent series tend to zero
   10.56 -     > Goalw [LIMSEQ_def] "summable f ==> f ----> 0"
   10.57 -     Proved easily in HSeries after proving nonstandard case.
   10.58 - -------------------------------------------------------------------*)
   10.59 -(*-------------------------------------------------------------------
   10.60 -                    Comparison test
   10.61 - -------------------------------------------------------------------*)
   10.62 +text{*Comparison test*}
   10.63 +
   10.64  lemma summable_comparison_test:
   10.65       "[| \<exists>N. \<forall>n. N \<le> n --> abs(f n) \<le> g n; summable g |] ==> summable f"
   10.66  apply (auto simp add: summable_Cauchy)
   10.67 @@ -384,9 +374,8 @@
   10.68  apply (auto simp add: abs_idempotent)
   10.69  done
   10.70  
   10.71 -(*------------------------------------------------------------------*)
   10.72 -(*       Limit comparison property for series (c.f. jrh)            *)
   10.73 -(*------------------------------------------------------------------*)
   10.74 +text{*Limit comparison property for series (c.f. jrh)*}
   10.75 +
   10.76  lemma summable_le:
   10.77       "[|\<forall>n. f n \<le> g n; summable f; summable g |] ==> suminf f \<le> suminf g"
   10.78  apply (drule summable_sums)+
   10.79 @@ -402,9 +391,7 @@
   10.80  apply (simp add: abs_le_interval_iff)
   10.81  done
   10.82  
   10.83 -(*-------------------------------------------------------------------
   10.84 -         Absolute convergence imples normal convergence
   10.85 - -------------------------------------------------------------------*)
   10.86 +text{*Absolute convergence imples normal convergence*}
   10.87  lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
   10.88  apply (auto simp add: sumr_rabs summable_Cauchy)
   10.89  apply (drule spec, auto)
   10.90 @@ -414,9 +401,7 @@
   10.91  apply (auto intro: sumr_rabs)
   10.92  done
   10.93  
   10.94 -(*-------------------------------------------------------------------
   10.95 -         Absolute convergence of series
   10.96 - -------------------------------------------------------------------*)
   10.97 +text{*Absolute convergence of series*}
   10.98  lemma summable_rabs:
   10.99       "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
  10.100  by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
  10.101 @@ -469,9 +454,7 @@
  10.102  done
  10.103  
  10.104  
  10.105 -(*--------------------------------------------------------------------------*)
  10.106 -(* Differentiation of finite sum                                            *)
  10.107 -(*--------------------------------------------------------------------------*)
  10.108 +text{*Differentiation of finite sum*}
  10.109  
  10.110  lemma DERIV_sumr [rule_format (no_asm)]:
  10.111       "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
    11.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 29 16:14:06 2004 +0200
    11.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 29 16:14:42 2004 +0200
    11.3 @@ -9,8 +9,6 @@
    11.4  
    11.5  theory Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim:
    11.6  
    11.7 -(*????FOR RING_AND_FIELD*)
    11.8 -
    11.9  constdefs
   11.10      root :: "[nat,real] => real"
   11.11      "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
   11.12 @@ -664,7 +662,7 @@
   11.13  apply (auto simp add: add_commute)
   11.14  apply (drule_tac x="(\<lambda>n. c n * (xa + x) ^ n)" in sums_diff, assumption) 
   11.15  apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult)
   11.16 -apply (rule sums_unique [symmetric])
   11.17 +apply (rule sums_unique)
   11.18  apply (simp add: diff_def divide_inverse add_ac mult_ac)
   11.19  apply (rule LIM_zero_cancel)
   11.20  apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans)
   11.21 @@ -690,7 +688,6 @@
   11.22  apply (simp add: sums_summable [THEN suminf_mult2])
   11.23  apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff)
   11.24  apply assumption
   11.25 -apply (subst minus_equation_iff, simp (no_asm))  
   11.26  apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac)
   11.27  apply (rule_tac f = suminf in arg_cong)
   11.28  apply (rule ext)
   11.29 @@ -1268,35 +1265,39 @@
   11.30  lemma sin_add: "sin (x + y) = sin x * cos y + cos x * sin y"
   11.31  apply (cut_tac x = x and y = y in sin_cos_add)
   11.32  apply (auto dest!: real_sum_squares_cancel_a 
   11.33 -            simp add: numeral_2_eq_2 simp del: sin_cos_add)
   11.34 +            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
   11.35  done
   11.36  
   11.37  lemma cos_add: "cos (x + y) = cos x * cos y - sin x * sin y"
   11.38  apply (cut_tac x = x and y = y in sin_cos_add)
   11.39  apply (auto dest!: real_sum_squares_cancel_a
   11.40 -            simp add: numeral_2_eq_2 simp del: sin_cos_add)
   11.41 +            simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_add)
   11.42  done
   11.43  
   11.44 -lemma lemma_DERIV_sin_cos_minus: "\<forall>x.  
   11.45 -          DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
   11.46 +lemma lemma_DERIV_sin_cos_minus:
   11.47 +    "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
   11.48  apply (safe, rule lemma_DERIV_subst)
   11.49  apply (best intro!: DERIV_intros intro: DERIV_chain2) 
   11.50  apply (auto simp add: real_diff_def left_distrib right_distrib mult_ac add_ac)
   11.51  done
   11.52  
   11.53 -lemma sin_cos_minus [simp]: "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
   11.54 -apply (cut_tac y = 0 and x = x in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
   11.55 +lemma sin_cos_minus [simp]: 
   11.56 +    "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
   11.57 +apply (cut_tac y = 0 and x = x 
   11.58 +       in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all])
   11.59  apply (auto simp add: numeral_2_eq_2)
   11.60  done
   11.61  
   11.62  lemma sin_minus [simp]: "sin (-x) = -sin(x)"
   11.63  apply (cut_tac x = x in sin_cos_minus)
   11.64 -apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)
   11.65 +apply (auto dest!: real_sum_squares_cancel_a 
   11.66 +       simp add: numeral_2_eq_2 real_add_eq_0_iff simp del: sin_cos_minus)
   11.67  done
   11.68  
   11.69  lemma cos_minus [simp]: "cos (-x) = cos(x)"
   11.70  apply (cut_tac x = x in sin_cos_minus)
   11.71 -apply (auto dest!: real_sum_squares_cancel_a simp add: numeral_2_eq_2 simp del: sin_cos_minus)
   11.72 +apply (auto dest!: real_sum_squares_cancel_a 
   11.73 +                   simp add: numeral_2_eq_2 simp del: sin_cos_minus)
   11.74  done
   11.75  
   11.76  lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y"
   11.77 @@ -1368,7 +1369,7 @@
   11.78  apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
   11.79  apply (subgoal_tac "x*x < 2*3", simp) 
   11.80  apply (rule mult_strict_mono)
   11.81 -apply (auto simp add: real_of_nat_Suc simp del: fact_Suc)
   11.82 +apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
   11.83  apply (subst fact_Suc)
   11.84  apply (subst fact_Suc)
   11.85  apply (subst fact_Suc)
   11.86 @@ -1430,7 +1431,8 @@
   11.87  apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
   11.88  apply (rule sumr_pos_lt_pair)
   11.89  apply (erule sums_summable, safe)
   11.90 -apply (simp (no_asm) add: divide_inverse mult_assoc [symmetric] del: fact_Suc)
   11.91 +apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
   11.92 +            del: fact_Suc)
   11.93  apply (rule real_mult_inverse_cancel2)
   11.94  apply (rule real_of_nat_fact_gt_zero)+
   11.95  apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
   11.96 @@ -1692,9 +1694,8 @@
   11.97  apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
   11.98   apply (clarify, rule_tac x = "n - 1" in exI)
   11.99   apply (force simp add: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib)
  11.100 -apply (rule cos_zero_lemma, clarify) 
  11.101 -apply (rule minus_le_iff [THEN iffD1])  
  11.102 -apply (rule_tac y=0 in order_trans, auto)
  11.103 +apply (rule cos_zero_lemma)
  11.104 +apply (simp_all add: add_increasing)  
  11.105  done
  11.106  
  11.107  
  11.108 @@ -1992,12 +1993,14 @@
  11.109          simp del: realpow_Suc)
  11.110  done
  11.111  
  11.112 -lemma lemma_sin_cos_eq [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  
  11.113 +text{*NEEDED??*}
  11.114 +lemma [simp]: "sin (xa + 1 / 2 * real (Suc m) * pi) =  
  11.115        cos (xa + 1 / 2 * real  (m) * pi)"
  11.116  apply (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
  11.117  done
  11.118  
  11.119 -lemma lemma_sin_cos_eq2 [simp]: "sin (xa + real (Suc m) * pi / 2) =  
  11.120 +text{*NEEDED??*}
  11.121 +lemma [simp]: "sin (xa + real (Suc m) * pi / 2) =  
  11.122        cos (xa + real (m) * pi / 2)"
  11.123  apply (simp only: cos_add sin_add divide_inverse real_of_nat_Suc left_distrib right_distrib, auto)
  11.124  done
  11.125 @@ -2333,8 +2336,8 @@
  11.126           1 - (cos xa)\<twosuperior> = (y / sqrt (x * x + y * y)) ^ 2 |]
  11.127        ==> (cos xa)\<twosuperior> = (x / sqrt (x * x + y * y)) ^ 2"
  11.128  apply (auto simp add: realpow_divide power2_eq_square [symmetric])
  11.129 -apply (rule add_commute [THEN subst])
  11.130 -apply (rule lemma_divide_rearrange, simp)
  11.131 +apply (subst add_commute)
  11.132 +apply (rule lemma_divide_rearrange, simp add: real_add_eq_0_iff)
  11.133  apply (simp add: add_commute)
  11.134  done
  11.135  
  11.136 @@ -2395,22 +2398,24 @@
  11.137  done
  11.138  
  11.139  lemma real_sum_squares_cancel2a: "x * x = -(y * y) ==> y = (0::real)"
  11.140 -by (auto intro: real_sum_squares_cancel)
  11.141 +by (auto intro: real_sum_squares_cancel iff: real_add_eq_0_iff)
  11.142  
  11.143  lemma polar_ex2: "[| x \<noteq> 0; y < 0 |] ==> \<exists>r a. x = r * cos a & y = r * sin a"
  11.144  apply (cut_tac x = 0 and y = x in linorder_less_linear, auto)
  11.145  apply (rule_tac x = "sqrt (x\<twosuperior> + y\<twosuperior>) " in exI)
  11.146  apply (rule_tac x = "arcsin (y / sqrt (x * x + y * y))" in exI)
  11.147 -apply (auto dest: real_sum_squares_cancel2a simp add: power2_eq_square)
  11.148 +apply (auto dest: real_sum_squares_cancel2a 
  11.149 +            simp add: power2_eq_square real_0_le_add_iff real_add_eq_0_iff)
  11.150  apply (unfold arcsin_def)
  11.151  apply (cut_tac x1 = x and y1 = y 
  11.152         in sin_total [OF cos_x_y_ge_minus_one1a cos_x_y_le_one2])
  11.153  apply (rule someI2_ex, blast)
  11.154  apply (erule_tac V = "EX! xa. - (pi/2) \<le> xa & xa \<le> pi/2 & sin xa = y / sqrt (x * x + y * y) " in thin_rl)
  11.155 -apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast, auto)
  11.156 +apply (cut_tac x=x and y=y in cos_x_y_disj, simp, blast)
  11.157 +apply (auto simp add: real_0_le_add_iff real_add_eq_0_iff)
  11.158  apply (drule cos_ge_zero, force)
  11.159  apply (drule_tac x = y in real_sqrt_divide_less_zero)
  11.160 -apply (auto simp add: real_add_commute)
  11.161 +apply (auto simp add: add_commute)
  11.162  apply (insert polar_ex1 [of x "-y"], simp, clarify) 
  11.163  apply (rule_tac x = r in exI)
  11.164  apply (rule_tac x = "-a" in exI, simp) 
  11.165 @@ -2539,8 +2544,7 @@
  11.166  apply (drule_tac d = e in isCont_inj_range)
  11.167  prefer 2 apply (assumption, assumption, safe)
  11.168  apply (rule_tac x = ea in exI, auto)
  11.169 -apply (rotate_tac 4)
  11.170 -apply (drule_tac x = "f (x) + xa" in spec)
  11.171 +apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)
  11.172  apply auto
  11.173  apply (drule sym, auto, arith)
  11.174  done
  11.175 @@ -2867,7 +2871,6 @@
  11.176  val cos_x_y_disj = thm "cos_x_y_disj";
  11.177  val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";
  11.178  val polar_ex1 = thm "polar_ex1";
  11.179 -val real_sum_squares_cancel2a = thm "real_sum_squares_cancel2a";
  11.180  val polar_ex2 = thm "polar_ex2";
  11.181  val polar_Ex = thm "polar_Ex";
  11.182  val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";
    12.1 --- a/src/HOL/Real/RealDef.thy	Thu Jul 29 16:14:06 2004 +0200
    12.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jul 29 16:14:42 2004 +0200
    12.3 @@ -765,19 +765,19 @@
    12.4  lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" 
    12.5  by arith
    12.6  
    12.7 -lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
    12.8 +lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
    12.9  by auto
   12.10  
   12.11 -lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
   12.12 +lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"
   12.13  by auto
   12.14  
   12.15 -lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
   12.16 +lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"
   12.17  by auto
   12.18  
   12.19 -lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
   12.20 +lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> -x)"
   12.21  by auto
   12.22  
   12.23 -lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
   12.24 +lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
   12.25  by auto
   12.26  
   12.27  
   12.28 @@ -860,12 +860,6 @@
   12.29  ML
   12.30  {*
   12.31  val real_0_le_divide_iff = thm"real_0_le_divide_iff";
   12.32 -val real_add_minus_iff = thm"real_add_minus_iff";
   12.33 -val real_add_eq_0_iff = thm"real_add_eq_0_iff";
   12.34 -val real_add_less_0_iff = thm"real_add_less_0_iff";
   12.35 -val real_0_less_add_iff = thm"real_0_less_add_iff";
   12.36 -val real_add_le_0_iff = thm"real_add_le_0_iff";
   12.37 -val real_0_le_add_iff = thm"real_0_le_add_iff";
   12.38  val real_0_less_diff_iff = thm"real_0_less_diff_iff";
   12.39  val real_0_le_diff_iff = thm"real_0_le_diff_iff";
   12.40  val real_lbound_gt_zero = thm"real_lbound_gt_zero";
    13.1 --- a/src/HOL/Real/RealPow.thy	Thu Jul 29 16:14:06 2004 +0200
    13.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jul 29 16:14:42 2004 +0200
    13.3 @@ -140,7 +140,9 @@
    13.4  
    13.5  text{*Used several times in Hyperreal/Transcendental.ML*}
    13.6  lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
    13.7 -  by (auto intro: real_sum_squares_cancel)
    13.8 +  apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
    13.9 +  apply (auto dest: real_sum_squares_cancel simp add: add_commute)
   13.10 +  done
   13.11  
   13.12  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
   13.13  by (auto simp add: left_distrib right_distrib real_diff_def)