remove redundant lemmas
authorhuffman
Mon May 14 09:33:18 2007 +0200 (2007-05-14)
changeset 229624bb05ba38939
parent 22961 e499ded5d0fc
child 22963 509b1da3cee1
remove redundant lemmas
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon May 14 09:27:24 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Mon May 14 09:33:18 2007 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5    real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)"
     1.6  
     1.7 -  real_abs_def:  "abs (r::real) == (if 0 \<le> r then r else -r)"
     1.8 +  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
     1.9  
    1.10  
    1.11  
    1.12 @@ -293,9 +293,6 @@
    1.13    show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
    1.14  qed
    1.15  
    1.16 -lemma real_mult_1_right: "z * (1::real) = z"
    1.17 -  by (rule OrderedGroup.mult_1_right)
    1.18 -
    1.19  
    1.20  subsection{*The @{text "\<le>"} Ordering*}
    1.21  
    1.22 @@ -418,11 +415,6 @@
    1.23  apply (simp add: right_distrib)
    1.24  done
    1.25  
    1.26 -text{*lemma for proving @{term "0<(1::real)"}*}
    1.27 -lemma real_zero_le_one: "0 \<le> (1::real)"
    1.28 -by (simp add: real_zero_def real_one_def real_le 
    1.29 -                 preal_self_less_add_left order_less_imp_le)
    1.30 -
    1.31  instance real :: distrib_lattice
    1.32    "inf x y \<equiv> min x y"
    1.33    "sup x y \<equiv> max x y"
    1.34 @@ -435,9 +427,8 @@
    1.35  proof
    1.36    fix x y z :: real
    1.37    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
    1.38 -  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
    1.39 -  show "\<bar>x\<bar> = (if x < 0 then -x else x)"
    1.40 -    by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le)
    1.41 +  show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2)
    1.42 +  show "\<bar>x\<bar> = (if x < 0 then -x else x)" by (simp only: real_abs_def)
    1.43  qed
    1.44  
    1.45  text{*The function @{term real_of_preal} requires many proofs, but it seems
    1.46 @@ -537,13 +528,6 @@
    1.47  lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
    1.48  by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
    1.49  
    1.50 -lemma real_add_less_le_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::real)"
    1.51 -  by (rule OrderedGroup.add_less_le_mono)
    1.52 -
    1.53 -lemma real_add_le_less_mono:
    1.54 -     "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
    1.55 -  by (rule OrderedGroup.add_le_less_mono)
    1.56 -
    1.57  lemma real_le_square [simp]: "(0::real) \<le> x*x"
    1.58   by (rule Ring_and_Field.zero_le_square)
    1.59  
    1.60 @@ -573,11 +557,6 @@
    1.61  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
    1.62  by(simp add:mult_commute)
    1.63  
    1.64 -text{*Only two uses?*}
    1.65 -lemma real_mult_less_mono':
    1.66 -     "[| x < y;  r1 < r2;  (0::real) \<le> r1;  0 \<le> x|] ==> r1 * x < r2 * y"
    1.67 - by (rule Ring_and_Field.mult_strict_mono')
    1.68 -
    1.69  text{*FIXME: delete or at least combine the next two lemmas*}
    1.70  lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    1.71  apply (drule OrderedGroup.equals_zero_I [THEN sym])
     2.1 --- a/src/HOL/Real/RealPow.thy	Mon May 14 09:27:24 2007 +0200
     2.2 +++ b/src/HOL/Real/RealPow.thy	Mon May 14 09:33:18 2007 +0200
     2.3 @@ -28,9 +28,6 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0"
     2.8 -  by (rule field_power_not_zero)
     2.9 -
    2.10  lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
    2.11  by simp
    2.12  
    2.13 @@ -59,16 +56,13 @@
    2.14  apply (induct "n")
    2.15  apply (auto simp add: real_of_nat_Suc)
    2.16  apply (subst mult_2)
    2.17 -apply (rule real_add_less_le_mono)
    2.18 +apply (rule add_less_le_mono)
    2.19  apply (auto simp add: two_realpow_ge_one)
    2.20  done
    2.21  
    2.22  lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
    2.23  by (insert power_decreasing [of 1 "Suc n" r], simp)
    2.24  
    2.25 -lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
    2.26 -by (rule power_Suc_less_one)
    2.27 -
    2.28  lemma realpow_minus_mult [rule_format]:
    2.29       "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
    2.30  apply (simp split add: nat_diff_split)
    2.31 @@ -103,21 +97,12 @@
    2.32  apply (auto simp add: real_of_nat_mult zero_less_mult_iff)
    2.33  done
    2.34  
    2.35 +(* used by AFP Integration theory *)
    2.36  lemma realpow_increasing:
    2.37       "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
    2.38    by (rule power_le_imp_le_base)
    2.39  
    2.40  
    2.41 -lemma zero_less_realpow_abs_iff [simp]:
    2.42 -     "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
    2.43 -apply (induct "n")
    2.44 -apply (auto simp add: zero_less_mult_iff)
    2.45 -done
    2.46 -
    2.47 -lemma zero_le_realpow_abs [simp]: "(0::real) \<le> (abs x)^n"
    2.48 -by (rule zero_le_power_abs)
    2.49 -
    2.50 -
    2.51  subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
    2.52  
    2.53  lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
     3.1 --- a/src/HOL/Real/real_arith.ML	Mon May 14 09:27:24 2007 +0200
     3.2 +++ b/src/HOL/Real/real_arith.ML	Mon May 14 09:33:18 2007 +0200
     3.3 @@ -20,7 +20,6 @@
     3.4  val real_mult_commute = thm"real_mult_commute";
     3.5  val real_mult_assoc = thm"real_mult_assoc";
     3.6  val real_mult_1 = thm"real_mult_1";
     3.7 -val real_mult_1_right = thm"real_mult_1_right";
     3.8  val preal_le_linear = thm"preal_le_linear";
     3.9  val real_mult_inverse_left = thm"real_mult_inverse_left";
    3.10  val real_not_refl2 = thm"real_not_refl2";
    3.11 @@ -43,8 +42,6 @@
    3.12  val real_less_all_real2 = thm "real_less_all_real2";
    3.13  val real_of_preal_le_iff = thm "real_of_preal_le_iff";
    3.14  val real_mult_order = thm "real_mult_order";
    3.15 -val real_add_less_le_mono = thm "real_add_less_le_mono";
    3.16 -val real_add_le_less_mono = thm "real_add_le_less_mono";
    3.17  val real_add_order = thm "real_add_order";
    3.18  val real_le_add_order = thm "real_le_add_order";
    3.19  val real_le_square = thm "real_le_square";
    3.20 @@ -54,7 +51,6 @@
    3.21  val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
    3.22  val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
    3.23  val real_mult_less_mono = thm "real_mult_less_mono";
    3.24 -val real_mult_less_mono' = thm "real_mult_less_mono'";
    3.25  val real_sum_squares_cancel = thm "real_sum_squares_cancel";
    3.26  val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
    3.27