removed redundant thms
authorpaulson
Fri Mar 19 10:50:06 2004 +0100 (2004-03-19)
changeset 14476758e7acdea2f
parent 14475 aa973ba84f69
child 14477 cc61fd03e589
removed redundant thms
src/HOL/Real/RComplete.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Real/RComplete.thy	Fri Mar 19 10:48:22 2004 +0100
     1.2 +++ b/src/HOL/Real/RComplete.thy	Fri Mar 19 10:50:06 2004 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4  lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
     1.5  apply (frule isLub_isUb)
     1.6  apply (frule_tac x = y in isLub_isUb)
     1.7 -apply (blast intro!: real_le_anti_sym dest!: isLub_le_isUb)
     1.8 +apply (blast intro!: order_antisym dest!: isLub_le_isUb)
     1.9  done
    1.10  
    1.11  lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"
     2.1 --- a/src/HOL/Real/RealDef.thy	Fri Mar 19 10:48:22 2004 +0100
     2.2 +++ b/src/HOL/Real/RealDef.thy	Fri Mar 19 10:50:06 2004 +0100
     2.3 @@ -204,9 +204,6 @@
     2.4  apply (simp add: real_add preal_add_ac)
     2.5  done
     2.6  
     2.7 -lemma real_add_zero_right: "z + (0::real) = z"
     2.8 -by (simp add: real_add_zero_left real_add_commute)
     2.9 -
    2.10  instance real :: plus_ac0
    2.11    by (intro_classes,
    2.12        (assumption | 
    2.13 @@ -634,9 +631,6 @@
    2.14       "!!z z'::real. [| w'\<le>w; z'<z |] ==> w' + z' < w + z"
    2.15    by (rule Ring_and_Field.add_le_less_mono)
    2.16  
    2.17 -lemma real_zero_less_one: "0 < (1::real)"
    2.18 -  by (rule Ring_and_Field.zero_less_one)
    2.19 -
    2.20  lemma real_le_square [simp]: "(0::real) \<le> x*x"
    2.21   by (rule Ring_and_Field.zero_le_square)
    2.22  
    2.23 @@ -676,12 +670,12 @@
    2.24  lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
    2.25  apply (drule Ring_and_Field.equals_zero_I [THEN sym])
    2.26  apply (cut_tac x = y in real_le_square) 
    2.27 -apply (auto, drule real_le_anti_sym, auto)
    2.28 +apply (auto, drule order_antisym, auto)
    2.29  done
    2.30  
    2.31  lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
    2.32  apply (rule_tac y = x in real_sum_squares_cancel)
    2.33 -apply (simp add: real_add_commute)
    2.34 +apply (simp add: add_commute)
    2.35  done
    2.36  
    2.37  lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y"
    2.38 @@ -905,9 +899,6 @@
    2.39  lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
    2.40    by auto
    2.41  
    2.42 -lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
    2.43 -  by (rule Ring_and_Field.dense)
    2.44 -
    2.45  
    2.46  subsection{*Absolute Value Function for the Reals*}
    2.47  
    2.48 @@ -965,7 +956,6 @@
    2.49  val real_lbound_gt_zero = thm"real_lbound_gt_zero";
    2.50  val real_less_half_sum = thm"real_less_half_sum";
    2.51  val real_gt_half_sum = thm"real_gt_half_sum";
    2.52 -val real_dense = thm"real_dense";
    2.53  
    2.54  val abs_eqI1 = thm"abs_eqI1";
    2.55  val abs_eqI2 = thm"abs_eqI2";
     3.1 --- a/src/HOL/Real/real_arith.ML	Fri Mar 19 10:48:22 2004 +0100
     3.2 +++ b/src/HOL/Real/real_arith.ML	Fri Mar 19 10:50:06 2004 +0100
     3.3 @@ -34,7 +34,6 @@
     3.4  val real_add_commute = thm"real_add_commute";
     3.5  val real_add_assoc = thm"real_add_assoc";
     3.6  val real_add_zero_left = thm"real_add_zero_left";
     3.7 -val real_add_zero_right = thm"real_add_zero_right";
     3.8  
     3.9  val real_mult = thm"real_mult";
    3.10  val real_mult_commute = thm"real_mult_commute";
    3.11 @@ -54,7 +53,6 @@
    3.12  val real_le_refl = thm"real_le_refl";
    3.13  val real_le_linear = thm"real_le_linear";
    3.14  val real_le_trans = thm"real_le_trans";
    3.15 -val real_le_anti_sym = thm"real_le_anti_sym";
    3.16  val real_less_le = thm"real_less_le";
    3.17  val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
    3.18  val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
    3.19 @@ -64,7 +62,6 @@
    3.20  val real_less_all_real2 = thm "real_less_all_real2";
    3.21  val real_of_preal_le_iff = thm "real_of_preal_le_iff";
    3.22  val real_mult_order = thm "real_mult_order";
    3.23 -val real_zero_less_one = thm "real_zero_less_one";
    3.24  val real_add_less_le_mono = thm "real_add_less_le_mono";
    3.25  val real_add_le_less_mono = thm "real_add_le_less_mono";
    3.26  val real_add_order = thm "real_add_order";