type hypreal is an ordered field
authorpaulson
Fri Dec 19 10:38:39 2003 +0100 (2003-12-19)
changeset 14303995212a00a50
parent 14302 6c24235e8d5d
child 14304 cc0b4bbfbc43
type hypreal is an ordered field
src/HOL/Hyperreal/HyperArith0.ML
src/HOL/Hyperreal/HyperOrd.thy
src/HOL/Hyperreal/NSA.ML
     1.1 --- a/src/HOL/Hyperreal/HyperArith0.ML	Fri Dec 19 04:28:45 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperArith0.ML	Fri Dec 19 10:38:39 2003 +0100
     1.3 @@ -15,8 +15,6 @@
     1.4  
     1.5  Goal "((x * y = 0) = (x = 0 | y = (0::hypreal)))";
     1.6  by Auto_tac;
     1.7 -by (cut_inst_tac [("x","x"),("y","y")] hypreal_mult_zero_disj 1);
     1.8 -by Auto_tac;
     1.9  qed "hypreal_mult_is_0";
    1.10  AddIffs [hypreal_mult_is_0];
    1.11  
    1.12 @@ -495,20 +493,6 @@
    1.13                                    hypreal_eq_divide_eq, hypreal_mult_eq_cancel1]));
    1.14  qed "hypreal_divide_eq_cancel1";
    1.15  
    1.16 -Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)";
    1.17 -by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
    1.18 -by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
    1.19 -by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
    1.20 -by (auto_tac (claset() addIs [hypreal_inverse_less_swap],
    1.21 -              simpset() delsimps [hypreal_inverse_inverse]
    1.22 -                        addsimps [hypreal_inverse_gt_0]));
    1.23 -qed "hypreal_inverse_less_iff";
    1.24 -
    1.25 -Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::hypreal))";
    1.26 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
    1.27 -                                      hypreal_inverse_less_iff]) 1);
    1.28 -qed "hypreal_inverse_le_iff";
    1.29 -
    1.30  (** Division by 1, -1 **)
    1.31  
    1.32  Goal "(x::hypreal)/1 = x";
     2.1 --- a/src/HOL/Hyperreal/HyperOrd.thy	Fri Dec 19 04:28:45 2003 +0100
     2.2 +++ b/src/HOL/Hyperreal/HyperOrd.thy	Fri Dec 19 10:38:39 2003 +0100
     2.3 @@ -134,7 +134,7 @@
     2.4  apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
     2.5  done
     2.6  
     2.7 -lemma hypreal_add_order_le: "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"
     2.8 +lemma hypreal_add_order_le: "[| 0 < x; 0 \<le> y |] ==> (0::hypreal) < x + y"
     2.9  by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order)
    2.10  
    2.11  lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"
    2.12 @@ -163,7 +163,7 @@
    2.13  apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set)
    2.14  done
    2.15  
    2.16 -lemma hypreal_le_add_order: "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"
    2.17 +lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
    2.18  apply (drule order_le_imp_less_or_eq)+
    2.19  apply (auto intro: hypreal_add_order order_less_imp_le)
    2.20  done
    2.21 @@ -181,11 +181,11 @@
    2.22  declare hypreal_add_right_cancel_less [simp] 
    2.23          hypreal_add_left_cancel_less [simp]
    2.24  
    2.25 -lemma hypreal_add_right_cancel_le: "(v+z <= w+z) = (v <= (w::hypreal))"
    2.26 +lemma hypreal_add_right_cancel_le: "(v+z \<le> w+z) = (v \<le> (w::hypreal))"
    2.27  apply (simp (no_asm))
    2.28  done
    2.29  
    2.30 -lemma hypreal_add_left_cancel_le: "(z+v <= z+w) = (v <= (w::hypreal))"
    2.31 +lemma hypreal_add_left_cancel_le: "(z+v \<le> z+w) = (v \<le> (w::hypreal))"
    2.32  apply (simp (no_asm))
    2.33  done
    2.34  
    2.35 @@ -201,23 +201,23 @@
    2.36                hypreal_add_ac simp del: hypreal_minus_add_distrib)
    2.37  done
    2.38  
    2.39 -lemma hypreal_add_left_le_mono1: "(q1::hypreal) <= q2  ==> x + q1 <= x + q2"
    2.40 +lemma hypreal_add_left_le_mono1: "(q1::hypreal) \<le> q2  ==> x + q1 \<le> x + q2"
    2.41  apply (drule order_le_imp_less_or_eq)
    2.42  apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute)
    2.43  done
    2.44  
    2.45 -lemma hypreal_add_le_mono1: "(q1::hypreal) <= q2  ==> q1 + x <= q2 + x"
    2.46 +lemma hypreal_add_le_mono1: "(q1::hypreal) \<le> q2  ==> q1 + x \<le> q2 + x"
    2.47  by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute)
    2.48  
    2.49 -lemma hypreal_add_le_mono: "[|(i::hypreal)<=j;  k<=l |] ==> i + k <= j + l"
    2.50 +lemma hypreal_add_le_mono: "[|(i::hypreal)\<le>j;  k\<le>l |] ==> i + k \<le> j + l"
    2.51  apply (erule hypreal_add_le_mono1 [THEN order_trans])
    2.52  apply (simp (no_asm))
    2.53  done
    2.54  
    2.55 -lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j;  k<=l |] ==> i + k < j + l"
    2.56 +lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j;  k\<le>l |] ==> i + k < j + l"
    2.57  by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
    2.58  
    2.59 -lemma hypreal_add_le_less_mono: "[|(i::hypreal)<=j;  k<l |] ==> i + k < j + l"
    2.60 +lemma hypreal_add_le_less_mono: "[|(i::hypreal)\<le>j;  k<l |] ==> i + k < j + l"
    2.61  by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono)
    2.62  
    2.63  lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
    2.64 @@ -228,26 +228,26 @@
    2.65  apply (simp (no_asm_use))
    2.66  done
    2.67  
    2.68 -lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) <= y|] ==> r < x + y"
    2.69 +lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x + y"
    2.70  by (auto dest: hypreal_add_less_le_mono)
    2.71  
    2.72 -lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C <= B + C ==> A <= B"
    2.73 +lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C \<le> B + C ==> A \<le> B"
    2.74  apply (drule_tac x = "-C" in hypreal_add_le_mono1)
    2.75  apply (simp add: hypreal_add_assoc)
    2.76  done
    2.77  
    2.78 -lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A <= C + B ==> A <= B"
    2.79 +lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A \<le> C + B ==> A \<le> B"
    2.80  apply (drule_tac x = "-C" in hypreal_add_left_le_mono1)
    2.81  apply (simp add: hypreal_add_assoc [symmetric])
    2.82  done
    2.83  
    2.84 -lemma hypreal_le_square: "(0::hypreal) <= x*x"
    2.85 +lemma hypreal_le_square: "(0::hypreal) \<le> x*x"
    2.86  apply (rule_tac x = 0 and y = x in hypreal_linear_less2)
    2.87  apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le)
    2.88  done
    2.89  declare hypreal_le_square [simp]
    2.90  
    2.91 -lemma hypreal_less_minus_square: "- (x*x) <= (0::hypreal)"
    2.92 +lemma hypreal_less_minus_square: "- (x*x) \<le> (0::hypreal)"
    2.93  apply (unfold hypreal_le_def)
    2.94  apply (auto dest!: hypreal_le_square [THEN order_le_less_trans] 
    2.95              simp add: hypreal_minus_zero_less_iff)
    2.96 @@ -270,69 +270,41 @@
    2.97  apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1)
    2.98  done
    2.99  
   2.100 -lemma hypreal_mult_le_less_mono1: "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"
   2.101 -apply (rule hypreal_less_or_eq_imp_le)
   2.102 -apply (drule order_le_imp_less_or_eq)
   2.103 -apply (auto intro: hypreal_mult_less_mono1)
   2.104 -done
   2.105 +subsection{*The Hyperreals Form an Ordered Field*}
   2.106  
   2.107 -lemma hypreal_mult_le_less_mono2: "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"
   2.108 -apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_le_less_mono1)
   2.109 -done
   2.110 +instance hypreal :: inverse ..
   2.111  
   2.112 -lemma hypreal_mult_less_mono: "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
   2.113 -apply (erule hypreal_mult_less_mono1 [THEN order_less_trans], assumption)
   2.114 -apply (erule hypreal_mult_less_mono2, assumption)
   2.115 -done
   2.116 +instance hypreal :: ordered_field
   2.117 +proof
   2.118 +  fix x y z :: hypreal
   2.119 +  show "(x + y) + z = x + (y + z)" by (rule hypreal_add_assoc)
   2.120 +  show "x + y = y + x" by (rule hypreal_add_commute)
   2.121 +  show "0 + x = x" by simp
   2.122 +  show "- x + x = 0" by simp
   2.123 +  show "x - y = x + (-y)" by (simp add: hypreal_diff_def)
   2.124 +  show "(x * y) * z = x * (y * z)" by (rule hypreal_mult_assoc)
   2.125 +  show "x * y = y * x" by (rule hypreal_mult_commute)
   2.126 +  show "1 * x = x" by simp
   2.127 +  show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
   2.128 +  show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
   2.129 +  show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1)
   2.130 +  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2)
   2.131 +  show "\<bar>x\<bar> = (if x < 0 then -x else x)"
   2.132 +    by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
   2.133 +  show "x \<noteq> 0 ==> inverse x * x = 1" by simp
   2.134 +  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
   2.135 +qed
   2.136  
   2.137 -(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
   2.138 -lemma hypreal_mult_less_mono': "[| x < y;  r1 < r2;  (0::hypreal) <= r1;  0 <= x|] ==> r1 * x < r2 * y"
   2.139 -apply (subgoal_tac "0<r2")
   2.140 -prefer 2 apply (blast intro: order_le_less_trans)
   2.141 -apply (case_tac "x=0")
   2.142 -apply (auto dest!: order_le_imp_less_or_eq intro: hypreal_mult_less_mono hypreal_mult_order)
   2.143 -done
   2.144 +text{*The precondition could be weakened to @{term "0\<le>x"}*}
   2.145 +lemma hypreal_mult_less_mono:
   2.146 +     "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
   2.147 + by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
   2.148  
   2.149  lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
   2.150 -apply (rule ccontr) 
   2.151 -apply (drule hypreal_leI) 
   2.152 -apply (frule hypreal_minus_zero_less_iff2 [THEN iffD2])
   2.153 -apply (frule hypreal_not_refl2 [THEN not_sym])
   2.154 -apply (drule hypreal_not_refl2 [THEN not_sym, THEN hypreal_inverse_not_zero])
   2.155 -apply (drule order_le_imp_less_or_eq, safe) 
   2.156 -apply (drule hypreal_mult_less_zero1, assumption)
   2.157 -apply (auto intro: hypreal_zero_less_one [THEN hypreal_less_asym]
   2.158 -            simp add: hypreal_minus_zero_less_iff)
   2.159 -done
   2.160 +  by (rule Ring_and_Field.positive_imp_inverse_positive)
   2.161  
   2.162  lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
   2.163 -apply (frule hypreal_not_refl2)
   2.164 -apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
   2.165 -apply (rule hypreal_minus_zero_less_iff [THEN iffD1])
   2.166 -apply (subst hypreal_minus_inverse [symmetric])
   2.167 -apply (auto intro: hypreal_inverse_gt_0)
   2.168 -done
   2.169 -
   2.170 -lemma hypreal_self_le_add_pos: "(x::hypreal)*x <= x*x + y*y"
   2.171 -apply (rule_tac z = x in eq_Abs_hypreal)
   2.172 -apply (rule_tac z = y in eq_Abs_hypreal)
   2.173 -apply (auto simp add: hypreal_mult hypreal_add hypreal_le)
   2.174 -done
   2.175 -declare hypreal_self_le_add_pos [simp]
   2.176 -
   2.177 -(*lcp: new lemma unfortunately needed...*)
   2.178 -lemma minus_square_le_square: "-(x*x) <= (y*y::real)"
   2.179 -apply (rule order_trans)
   2.180 -apply (rule_tac [2] real_le_square, auto)
   2.181 -done
   2.182 -
   2.183 -lemma hypreal_self_le_add_pos2: "(x::hypreal)*x <= x*x + y*y + z*z"
   2.184 -apply (rule_tac z = x in eq_Abs_hypreal)
   2.185 -apply (rule_tac z = y in eq_Abs_hypreal)
   2.186 -apply (rule_tac z = z in eq_Abs_hypreal)
   2.187 -apply (auto simp add: hypreal_mult hypreal_add hypreal_le minus_square_le_square)
   2.188 -done
   2.189 -declare hypreal_self_le_add_pos2 [simp]
   2.190 +  by (rule Ring_and_Field.negative_imp_inverse_negative)
   2.191  
   2.192  
   2.193  (*----------------------------------------------------------------------------
   2.194 @@ -394,75 +366,43 @@
   2.195  by (simp add: hypreal_inverse omega_def epsilon_def)
   2.196  
   2.197  
   2.198 -(* this proof is so much simpler than one for reals!! *)
   2.199 -lemma hypreal_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"
   2.200 -apply (rule_tac z = x in eq_Abs_hypreal)
   2.201 -apply (rule_tac z = r in eq_Abs_hypreal)
   2.202 -apply (auto simp add: hypreal_inverse hypreal_less hypreal_zero_def, ultra)
   2.203 -done
   2.204 +subsection{*Routine Properties*}
   2.205  
   2.206 -lemma hypreal_inverse_less_iff: "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"
   2.207 -apply (auto intro: hypreal_inverse_less_swap)
   2.208 -apply (rule_tac t = r in hypreal_inverse_inverse [THEN subst])
   2.209 -apply (rule_tac t = x in hypreal_inverse_inverse [THEN subst])
   2.210 -apply (rule hypreal_inverse_less_swap)
   2.211 -apply (auto simp add: hypreal_inverse_gt_0)
   2.212 -done
   2.213 +(* this proof is so much simpler than one for reals!! *)
   2.214 +lemma hypreal_inverse_less_swap:
   2.215 +     "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"
   2.216 +  by (rule Ring_and_Field.less_imp_inverse_less)
   2.217  
   2.218 -lemma hypreal_mult_inverse_less_mono1: "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)"
   2.219 -by (blast intro!: hypreal_mult_less_mono1 hypreal_inverse_gt_0)
   2.220 -
   2.221 -lemma hypreal_mult_inverse_less_mono2: "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y"
   2.222 -by (blast intro!: hypreal_mult_less_mono2 hypreal_inverse_gt_0)
   2.223 -
   2.224 -lemma hypreal_less_mult_right_cancel: "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"
   2.225 -apply (frule_tac x = "x*z" in hypreal_mult_inverse_less_mono1)
   2.226 -apply (drule_tac [2] hypreal_not_refl2 [THEN not_sym])
   2.227 -apply (auto dest!: hypreal_mult_inverse simp add: hypreal_mult_ac)
   2.228 -done
   2.229 +lemma hypreal_inverse_less_iff:
   2.230 +     "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)"
   2.231 +by (rule Ring_and_Field.inverse_less_iff_less)
   2.232  
   2.233 -lemma hypreal_less_mult_left_cancel: "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"
   2.234 -by (auto intro: hypreal_less_mult_right_cancel simp add: hypreal_mult_commute)
   2.235 +lemma hypreal_inverse_le_iff:
   2.236 +     "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::hypreal))"
   2.237 +by (rule Ring_and_Field.inverse_le_iff_le)
   2.238  
   2.239 -lemma hypreal_mult_less_gt_zero: "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y"
   2.240 -apply (frule_tac y = r in order_less_trans)
   2.241 -apply (drule_tac [2] z = ra and x = r in hypreal_mult_less_mono1)
   2.242 -apply (drule_tac [3] z = x and x = ra in hypreal_mult_less_mono2)
   2.243 -apply (auto intro: order_less_trans)
   2.244 -done
   2.245  
   2.246 -lemma hypreal_mult_le_ge_zero: "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y"
   2.247 -apply (drule order_le_imp_less_or_eq)+
   2.248 -apply (rule hypreal_less_or_eq_imp_le)
   2.249 -apply (auto intro: hypreal_mult_less_mono1 hypreal_mult_less_mono2 hypreal_mult_less_gt_zero)
   2.250 -done
   2.251 +subsection{*Convenient Biconditionals for Products of Signs*}
   2.252  
   2.253 -(*----------------------------------------------------------------------------
   2.254 -     Some convenient biconditionals for products of signs 
   2.255 - ----------------------------------------------------------------------------*)
   2.256 +lemma hypreal_0_less_mult_iff:
   2.257 +     "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
   2.258 +  by (rule Ring_and_Field.zero_less_mult_iff) 
   2.259  
   2.260 -lemma hypreal_0_less_mult_iff: "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
   2.261 - apply (auto simp add: order_le_less linorder_not_less hypreal_mult_order hypreal_mult_less_zero1)
   2.262 -apply (rule_tac [!] ccontr)
   2.263 -apply (auto simp add: order_le_less linorder_not_less)
   2.264 -apply (erule_tac [!] rev_mp)
   2.265 -apply (drule_tac [!] hypreal_mult_less_zero) 
   2.266 -apply (auto dest: order_less_not_sym simp add: hypreal_mult_commute)
   2.267 -done
   2.268 -
   2.269 -lemma hypreal_0_le_mult_iff: "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"
   2.270 -by (auto dest: hypreal_mult_zero_disj simp add: order_le_less linorder_not_less hypreal_0_less_mult_iff)
   2.271 +lemma hypreal_0_le_mult_iff: "((0::hypreal) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
   2.272 +  by (rule Ring_and_Field.zero_le_mult_iff) 
   2.273  
   2.274  lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"
   2.275 -apply (auto simp add: hypreal_0_le_mult_iff linorder_not_le [symmetric])
   2.276 -apply (auto dest: order_less_not_sym simp add: linorder_not_le)
   2.277 -done
   2.278 +  by (rule Ring_and_Field.mult_less_0_iff) 
   2.279 +
   2.280 +lemma hypreal_mult_le_0_iff: "(x*y \<le> (0::hypreal)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
   2.281 +  by (rule Ring_and_Field.mult_le_0_iff) 
   2.282 +
   2.283  
   2.284 -lemma hypreal_mult_le_0_iff: "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"
   2.285 -by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric])
   2.286 -
   2.287 -lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0"
   2.288 -by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero)
   2.289 +lemma hypreal_mult_self_sum_ge_zero: "(0::hypreal) \<le> x*x + y*y"
   2.290 +proof -
   2.291 +  have "0 + 0 \<le> x*x + y*y" by (blast intro: add_mono zero_le_square)
   2.292 +  thus ?thesis by simp
   2.293 +qed
   2.294  
   2.295  (*TO BE DELETED*)
   2.296  ML
   2.297 @@ -513,15 +453,9 @@
   2.298  val hypreal_mult_0_less = thm"hypreal_mult_0_less";
   2.299  val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1";
   2.300  val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
   2.301 -val hypreal_mult_le_less_mono1 = thm"hypreal_mult_le_less_mono1";
   2.302 -val hypreal_mult_le_less_mono2 = thm"hypreal_mult_le_less_mono2";
   2.303  val hypreal_mult_less_mono = thm"hypreal_mult_less_mono";
   2.304 -val hypreal_mult_less_mono' = thm"hypreal_mult_less_mono'";
   2.305  val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0";
   2.306  val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0";
   2.307 -val hypreal_self_le_add_pos = thm"hypreal_self_le_add_pos";
   2.308 -val minus_square_le_square = thm"minus_square_le_square";
   2.309 -val hypreal_self_le_add_pos2 = thm"hypreal_self_le_add_pos2";
   2.310  val Rep_hypreal_omega = thm"Rep_hypreal_omega";
   2.311  val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
   2.312  val lemma_finite_omega_set = thm"lemma_finite_omega_set";
   2.313 @@ -536,17 +470,12 @@
   2.314  val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
   2.315  val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap";
   2.316  val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff";
   2.317 -val hypreal_mult_inverse_less_mono1 = thm"hypreal_mult_inverse_less_mono1";
   2.318 -val hypreal_mult_inverse_less_mono2 = thm"hypreal_mult_inverse_less_mono2";
   2.319 -val hypreal_less_mult_right_cancel = thm"hypreal_less_mult_right_cancel";
   2.320 -val hypreal_less_mult_left_cancel = thm"hypreal_less_mult_left_cancel";
   2.321 -val hypreal_mult_less_gt_zero = thm"hypreal_mult_less_gt_zero";
   2.322 -val hypreal_mult_le_ge_zero = thm"hypreal_mult_le_ge_zero";
   2.323 +val hypreal_inverse_le_iff = thm"hypreal_inverse_le_iff";
   2.324  val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff";
   2.325  val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff";
   2.326  val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff";
   2.327  val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff";
   2.328 -val hypreal_mult_less_zero2 = thm"hypreal_mult_less_zero2";
   2.329 +val hypreal_mult_self_sum_ge_zero = thm "hypreal_mult_self_sum_ge_zero";
   2.330  *}
   2.331  
   2.332  end
     3.1 --- a/src/HOL/Hyperreal/NSA.ML	Fri Dec 19 04:28:45 2003 +0100
     3.2 +++ b/src/HOL/Hyperreal/NSA.ML	Fri Dec 19 10:38:39 2003 +0100
     3.3 @@ -1560,16 +1560,15 @@
     3.4  Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
     3.5  by (rtac Infinitesimal_interval2 1);
     3.6  by (rtac hypreal_le_square 3);
     3.7 -by (rtac hypreal_self_le_add_pos 3);
     3.8 +by (assume_tac 1);
     3.9  by Auto_tac;
    3.10  qed "Infinitesimal_square_cancel";
    3.11  Addsimps [Infinitesimal_square_cancel];
    3.12  
    3.13  Goal "x*x + y*y : HFinite ==> x*x : HFinite";
    3.14  by (rtac HFinite_bounded 1);
    3.15 -by (rtac hypreal_self_le_add_pos 2);
    3.16 -by (rtac (hypreal_le_square) 2);
    3.17  by (assume_tac 1);
    3.18 +by Auto_tac;
    3.19  qed "HFinite_square_cancel";
    3.20  Addsimps [HFinite_square_cancel];
    3.21  
    3.22 @@ -1588,15 +1587,23 @@
    3.23  Addsimps [HFinite_square_cancel2];
    3.24  
    3.25  Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal";
    3.26 -by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
    3.27 -    Infinitesimal_interval2, hypreal_le_square]) 1);
    3.28 +by (rtac Infinitesimal_interval2 1);
    3.29 +by (assume_tac 1);
    3.30 +by (rtac hypreal_le_square 2);
    3.31 +by (Asm_full_simp_tac 1);
    3.32 +by (cut_inst_tac [("a","y")] (thm"zero_le_square") 1);
    3.33 +by (cut_inst_tac [("a","z")] (thm"zero_le_square") 1);
    3.34 +by (asm_simp_tac (simpset() addsimps []) 1); 
    3.35  qed "Infinitesimal_sum_square_cancel";
    3.36  Addsimps [Infinitesimal_sum_square_cancel];
    3.37  
    3.38  Goal "x*x + y*y + z*z : HFinite ==> x*x : HFinite";
    3.39 -by (blast_tac (claset() addIs [hypreal_self_le_add_pos2, HFinite_bounded,
    3.40 -                               hypreal_le_square,
    3.41 -                               HFinite_number_of]) 1);
    3.42 +by (rtac HFinite_bounded 1);
    3.43 +by (assume_tac 1);
    3.44 +by (rtac hypreal_le_square 2);
    3.45 +by (cut_inst_tac [("a","y")] (thm"zero_le_square") 1);
    3.46 +by (cut_inst_tac [("a","z")] (thm"zero_le_square") 1);
    3.47 +by (asm_simp_tac (simpset() addsimps []) 1); 
    3.48  qed "HFinite_sum_square_cancel";
    3.49  Addsimps [HFinite_sum_square_cancel];
    3.50