src/HOL/Hyperreal/HyperDef.thy
changeset 14301 48dc606749bd
parent 14299 0b5c0b0a3eba
child 14305 f17ca9f6dc8c
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Dec 18 08:20:36 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Dec 18 15:06:24 2003 +0100
     1.3 @@ -91,21 +91,18 @@
     1.4  (*** based on James' proof that the set of naturals is not finite ***)
     1.5  lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)"
     1.6  apply (rule impI)
     1.7 -apply (erule_tac F = "A" in finite_induct)
     1.8 -apply (blast , erule exE)
     1.9 +apply (erule_tac F = A in finite_induct)
    1.10 +apply (blast, erule exE)
    1.11  apply (rule_tac x = "n + x" in exI)
    1.12 -apply (rule allI , erule_tac x = "x + m" in allE)
    1.13 +apply (rule allI, erule_tac x = "x + m" in allE)
    1.14  apply (auto simp add: add_ac)
    1.15  done
    1.16  
    1.17  lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\<exists>n. n \<notin>A)"
    1.18 -apply (rule impI , drule finite_exhausts)
    1.19 -apply blast
    1.20 -done
    1.21 +by (rule impI, drule finite_exhausts, blast)
    1.22  
    1.23  lemma not_finite_nat: "~ finite(UNIV:: nat set)"
    1.24 -apply (fast dest!: finite_exhausts)
    1.25 -done
    1.26 +by (fast dest!: finite_exhausts)
    1.27  
    1.28  (*------------------------------------------------------------------------
    1.29     Existence of free ultrafilter over the naturals and proof of various 
    1.30 @@ -113,36 +110,32 @@
    1.31   ------------------------------------------------------------------------*)
    1.32  
    1.33  lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)"
    1.34 -apply (rule not_finite_nat [THEN FreeUltrafilter_Ex])
    1.35 -done
    1.36 +by (rule not_finite_nat [THEN FreeUltrafilter_Ex])
    1.37  
    1.38 -lemma FreeUltrafilterNat_mem: 
    1.39 +lemma FreeUltrafilterNat_mem [simp]: 
    1.40       "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)"
    1.41  apply (unfold FreeUltrafilterNat_def)
    1.42  apply (rule FreeUltrafilterNat_Ex [THEN exE])
    1.43 -apply (rule someI2)
    1.44 -apply assumption+
    1.45 +apply (rule someI2, assumption+)
    1.46  done
    1.47 -declare FreeUltrafilterNat_mem [simp]
    1.48  
    1.49  lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
    1.50  apply (unfold FreeUltrafilterNat_def)
    1.51  apply (rule FreeUltrafilterNat_Ex [THEN exE])
    1.52 -apply (rule someI2 , assumption)
    1.53 +apply (rule someI2, assumption)
    1.54  apply (blast dest: mem_FreeUltrafiltersetD1)
    1.55  done
    1.56  
    1.57  lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x"
    1.58 -apply (blast dest: FreeUltrafilterNat_finite)
    1.59 -done
    1.60 +by (blast dest: FreeUltrafilterNat_finite)
    1.61  
    1.62 -lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat"
    1.63 +lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat"
    1.64  apply (unfold FreeUltrafilterNat_def)
    1.65  apply (rule FreeUltrafilterNat_Ex [THEN exE])
    1.66 -apply (rule someI2 , assumption)
    1.67 -apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter Filter_empty_not_mem)
    1.68 +apply (rule someI2, assumption)
    1.69 +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter 
    1.70 +                   Filter_empty_not_mem)
    1.71  done
    1.72 -declare FreeUltrafilterNat_empty [simp]
    1.73  
    1.74  lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]   
    1.75        ==> X Int Y \<in> FreeUltrafilterNat"
    1.76 @@ -157,53 +150,39 @@
    1.77  done
    1.78  
    1.79  lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
    1.80 -apply (safe)
    1.81 -apply (drule FreeUltrafilterNat_Int , assumption)
    1.82 -apply auto
    1.83 +apply safe
    1.84 +apply (drule FreeUltrafilterNat_Int, assumption, auto)
    1.85  done
    1.86  
    1.87  lemma FreeUltrafilterNat_Compl_mem: "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
    1.88  apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]])
    1.89 -apply (safe , drule_tac x = "X" in bspec)
    1.90 +apply (safe, drule_tac x = X in bspec)
    1.91  apply (auto simp add: UNIV_diff_Compl)
    1.92  done
    1.93  
    1.94  lemma FreeUltrafilterNat_Compl_iff1: "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)"
    1.95 -apply (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem)
    1.96 -done
    1.97 +by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem)
    1.98  
    1.99  lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
   1.100 -apply (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
   1.101 -done
   1.102 +by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
   1.103  
   1.104 -lemma FreeUltrafilterNat_UNIV: "(UNIV::nat set) \<in> FreeUltrafilterNat"
   1.105 -apply (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
   1.106 -done
   1.107 -declare FreeUltrafilterNat_UNIV [simp]
   1.108 +lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
   1.109 +by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
   1.110  
   1.111 -lemma FreeUltrafilterNat_Nat_set: "UNIV \<in> FreeUltrafilterNat"
   1.112 -apply auto
   1.113 -done
   1.114 -declare FreeUltrafilterNat_Nat_set [simp]
   1.115 +lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat"
   1.116 +by auto
   1.117  
   1.118 -lemma FreeUltrafilterNat_Nat_set_refl: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
   1.119 -apply (simp (no_asm))
   1.120 -done
   1.121 -declare FreeUltrafilterNat_Nat_set_refl [intro]
   1.122 +lemma FreeUltrafilterNat_Nat_set_refl [intro]: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
   1.123 +by simp
   1.124  
   1.125  lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P"
   1.126 -apply (rule ccontr)
   1.127 -apply simp
   1.128 -done
   1.129 +by (rule ccontr, simp)
   1.130  
   1.131  lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)"
   1.132 -apply (rule ccontr)
   1.133 -apply simp
   1.134 -done
   1.135 +by (rule ccontr, simp)
   1.136  
   1.137  lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat"
   1.138 -apply (auto intro: FreeUltrafilterNat_Nat_set)
   1.139 -done
   1.140 +by (auto intro: FreeUltrafilterNat_Nat_set)
   1.141  
   1.142  (*-------------------------------------------------------
   1.143       Define and use Ultrafilter tactics
   1.144 @@ -231,7 +210,7 @@
   1.145  lemma FreeUltrafilterNat_Un: "X Un Y: FreeUltrafilterNat  
   1.146        ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"
   1.147  apply auto
   1.148 -apply (ultra)
   1.149 +apply ultra
   1.150  done
   1.151  
   1.152  (*-------------------------------------------------------
   1.153 @@ -242,9 +221,7 @@
   1.154  (** Natural deduction for hyprel **)
   1.155  
   1.156  lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
   1.157 -apply (unfold hyprel_def)
   1.158 -apply fast
   1.159 -done
   1.160 +by (unfold hyprel_def, fast)
   1.161  
   1.162  lemma hyprel_refl: "(x,x): hyprel"
   1.163  apply (unfold hyprel_def)
   1.164 @@ -252,14 +229,11 @@
   1.165  done
   1.166  
   1.167  lemma hyprel_sym [rule_format (no_asm)]: "(x,y): hyprel --> (y,x):hyprel"
   1.168 -apply (simp add: hyprel_def eq_commute) 
   1.169 -done
   1.170 +by (simp add: hyprel_def eq_commute)
   1.171  
   1.172  lemma hyprel_trans: 
   1.173        "[|(x,y): hyprel; (y,z):hyprel|] ==> (x,z):hyprel"
   1.174 -apply (unfold hyprel_def)
   1.175 -apply auto
   1.176 -apply (ultra)
   1.177 +apply (unfold hyprel_def, auto, ultra)
   1.178  done
   1.179  
   1.180  lemma equiv_hyprel: "equiv UNIV hyprel"
   1.181 @@ -271,10 +245,8 @@
   1.182  lemmas equiv_hyprel_iff =
   1.183      eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] 
   1.184  
   1.185 -lemma hyprel_in_hypreal: "hyprel``{x}:hypreal"
   1.186 -apply (unfold hypreal_def hyprel_def quotient_def)
   1.187 -apply blast
   1.188 -done
   1.189 +lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
   1.190 +by (unfold hypreal_def hyprel_def quotient_def, blast)
   1.191  
   1.192  lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal"
   1.193  apply (rule inj_on_inverseI)
   1.194 @@ -282,7 +254,7 @@
   1.195  done
   1.196  
   1.197  declare inj_on_Abs_hypreal [THEN inj_on_iff, simp] 
   1.198 -        hyprel_in_hypreal [simp] Abs_hypreal_inverse [simp]
   1.199 +        Abs_hypreal_inverse [simp]
   1.200  
   1.201  declare equiv_hyprel [THEN eq_equiv_class_iff, simp]
   1.202  
   1.203 @@ -295,27 +267,19 @@
   1.204  apply (rule Rep_hypreal_inverse)
   1.205  done
   1.206  
   1.207 -lemma lemma_hyprel_refl: "x \<in> hyprel `` {x}"
   1.208 -apply (unfold hyprel_def)
   1.209 -apply (safe)
   1.210 +lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
   1.211 +apply (unfold hyprel_def, safe)
   1.212  apply (auto intro!: FreeUltrafilterNat_Nat_set)
   1.213  done
   1.214  
   1.215 -declare lemma_hyprel_refl [simp]
   1.216 -
   1.217 -lemma hypreal_empty_not_mem: "{} \<notin> hypreal"
   1.218 +lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
   1.219  apply (unfold hypreal_def)
   1.220  apply (auto elim!: quotientE equalityCE)
   1.221  done
   1.222  
   1.223 -declare hypreal_empty_not_mem [simp]
   1.224 +lemma Rep_hypreal_nonempty [simp]: "Rep_hypreal x \<noteq> {}"
   1.225 +by (cut_tac x = x in Rep_hypreal, auto)
   1.226  
   1.227 -lemma Rep_hypreal_nonempty: "Rep_hypreal x \<noteq> {}"
   1.228 -apply (cut_tac x = "x" in Rep_hypreal)
   1.229 -apply auto
   1.230 -done
   1.231 -
   1.232 -declare Rep_hypreal_nonempty [simp]
   1.233  
   1.234  (*------------------------------------------------------------------------
   1.235     hypreal_of_real: the injection from real to hypreal
   1.236 @@ -334,7 +298,7 @@
   1.237  lemma eq_Abs_hypreal:
   1.238      "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
   1.239  apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
   1.240 -apply (drule_tac f = "Abs_hypreal" in arg_cong)
   1.241 +apply (drule_tac f = Abs_hypreal in arg_cong)
   1.242  apply (force simp add: Rep_hypreal_inverse)
   1.243  done
   1.244  
   1.245 @@ -347,44 +311,38 @@
   1.246  lemma hypreal_minus: 
   1.247     "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
   1.248  apply (unfold hypreal_minus_def)
   1.249 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   1.250 -apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   1.251 +apply (rule_tac f = Abs_hypreal in arg_cong)
   1.252 +apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   1.253                 UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
   1.254  done
   1.255  
   1.256 -lemma hypreal_minus_minus: "- (- z) = (z::hypreal)"
   1.257 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.258 -apply (simp (no_asm_simp) add: hypreal_minus)
   1.259 +lemma hypreal_minus_minus [simp]: "- (- z) = (z::hypreal)"
   1.260 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.261 +apply (simp add: hypreal_minus)
   1.262  done
   1.263  
   1.264 -declare hypreal_minus_minus [simp]
   1.265 -
   1.266  lemma inj_hypreal_minus: "inj(%r::hypreal. -r)"
   1.267  apply (rule inj_onI)
   1.268 -apply (drule_tac f = "uminus" in arg_cong)
   1.269 +apply (drule_tac f = uminus in arg_cong)
   1.270  apply (simp add: hypreal_minus_minus)
   1.271  done
   1.272  
   1.273 -lemma hypreal_minus_zero: "- 0 = (0::hypreal)"
   1.274 +lemma hypreal_minus_zero [simp]: "- 0 = (0::hypreal)"
   1.275  apply (unfold hypreal_zero_def)
   1.276 -apply (simp (no_asm) add: hypreal_minus)
   1.277 +apply (simp add: hypreal_minus)
   1.278  done
   1.279 -declare hypreal_minus_zero [simp]
   1.280  
   1.281 -lemma hypreal_minus_zero_iff: "(-x = 0) = (x = (0::hypreal))"
   1.282 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.283 +lemma hypreal_minus_zero_iff [simp]: "(-x = 0) = (x = (0::hypreal))"
   1.284 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.285  apply (auto simp add: hypreal_zero_def hypreal_minus)
   1.286  done
   1.287 -declare hypreal_minus_zero_iff [simp]
   1.288  
   1.289  
   1.290  (**** hyperreal addition: hypreal_add  ****)
   1.291  
   1.292  lemma hypreal_add_congruent2: 
   1.293      "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})"
   1.294 -apply (unfold congruent2_def)
   1.295 -apply (auto ); 
   1.296 -apply ultra
   1.297 +apply (unfold congruent2_def, auto, ultra)
   1.298  done
   1.299  
   1.300  lemma hypreal_add: 
   1.301 @@ -396,20 +354,20 @@
   1.302  
   1.303  lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =  
   1.304        Abs_hypreal(hyprel``{%n. X n - Y n})"
   1.305 -apply (simp (no_asm) add: hypreal_diff_def hypreal_minus hypreal_add)
   1.306 +apply (simp add: hypreal_diff_def hypreal_minus hypreal_add)
   1.307  done
   1.308  
   1.309  lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
   1.310 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.311 -apply (rule_tac z = "w" in eq_Abs_hypreal)
   1.312 -apply (simp (no_asm_simp) add: real_add_ac hypreal_add)
   1.313 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.314 +apply (rule_tac z = w in eq_Abs_hypreal)
   1.315 +apply (simp add: real_add_ac hypreal_add)
   1.316  done
   1.317  
   1.318  lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
   1.319 -apply (rule_tac z = "z1" in eq_Abs_hypreal)
   1.320 -apply (rule_tac z = "z2" in eq_Abs_hypreal)
   1.321 -apply (rule_tac z = "z3" in eq_Abs_hypreal)
   1.322 -apply (simp (no_asm_simp) add: hypreal_add real_add_assoc)
   1.323 +apply (rule_tac z = z1 in eq_Abs_hypreal)
   1.324 +apply (rule_tac z = z2 in eq_Abs_hypreal)
   1.325 +apply (rule_tac z = z3 in eq_Abs_hypreal)
   1.326 +apply (simp add: hypreal_add real_add_assoc)
   1.327  done
   1.328  
   1.329  (*For AC rewriting*)
   1.330 @@ -423,32 +381,26 @@
   1.331  lemmas hypreal_add_ac =
   1.332         hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute
   1.333  
   1.334 -lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
   1.335 +lemma hypreal_add_zero_left [simp]: "(0::hypreal) + z = z"
   1.336  apply (unfold hypreal_zero_def)
   1.337 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.338 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.339  apply (simp add: hypreal_add)
   1.340  done
   1.341  
   1.342 -lemma hypreal_add_zero_right: "z + (0::hypreal) = z"
   1.343 -apply (simp (no_asm) add: hypreal_add_zero_left hypreal_add_commute)
   1.344 -done
   1.345 +lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
   1.346 +by (simp add: hypreal_add_zero_left hypreal_add_commute)
   1.347  
   1.348 -lemma hypreal_add_minus: "z + -z = (0::hypreal)"
   1.349 +lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
   1.350  apply (unfold hypreal_zero_def)
   1.351 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.352 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.353  apply (simp add: hypreal_minus hypreal_add)
   1.354  done
   1.355  
   1.356 -lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
   1.357 -apply (simp (no_asm) add: hypreal_add_commute hypreal_add_minus)
   1.358 -done
   1.359 -
   1.360 -declare hypreal_add_minus [simp] hypreal_add_minus_left [simp]
   1.361 -    hypreal_add_zero_left [simp] hypreal_add_zero_right [simp] 
   1.362 +lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)"
   1.363 +by (simp add: hypreal_add_commute hypreal_add_minus)
   1.364  
   1.365  lemma hypreal_minus_ex: "\<exists>y. (x::hypreal) + y = 0"
   1.366 -apply (fast intro: hypreal_add_minus)
   1.367 -done
   1.368 +by (fast intro: hypreal_add_minus)
   1.369  
   1.370  lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0"
   1.371  apply (auto intro: hypreal_add_minus)
   1.372 @@ -465,55 +417,44 @@
   1.373  done
   1.374  
   1.375  lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
   1.376 -apply (cut_tac z = "y" in hypreal_add_minus_left)
   1.377 -apply (rule_tac x1 = "y" in hypreal_minus_left_ex1 [THEN ex1E])
   1.378 -apply blast
   1.379 +apply (cut_tac z = y in hypreal_add_minus_left)
   1.380 +apply (rule_tac x1 = y in hypreal_minus_left_ex1 [THEN ex1E], blast)
   1.381  done
   1.382  
   1.383  lemma hypreal_as_add_inverse_ex: "\<exists>y::hypreal. x = -y"
   1.384 -apply (cut_tac x = "x" in hypreal_minus_ex)
   1.385 -apply (erule exE , drule hypreal_add_minus_eq_minus)
   1.386 -apply fast
   1.387 +apply (cut_tac x = x in hypreal_minus_ex)
   1.388 +apply (erule exE, drule hypreal_add_minus_eq_minus, fast)
   1.389  done
   1.390  
   1.391 -lemma hypreal_minus_add_distrib: "-(x + (y::hypreal)) = -x + -y"
   1.392 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.393 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.394 +lemma hypreal_minus_add_distrib [simp]: "-(x + (y::hypreal)) = -x + -y"
   1.395 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.396 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.397  apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib)
   1.398  done
   1.399 -declare hypreal_minus_add_distrib [simp]
   1.400  
   1.401  lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
   1.402 -apply (simp (no_asm) add: hypreal_add_commute)
   1.403 -done
   1.404 +by (simp add: hypreal_add_commute)
   1.405  
   1.406  lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)"
   1.407 -apply (safe)
   1.408 +apply safe
   1.409  apply (drule_tac f = "%t.-x + t" in arg_cong)
   1.410  apply (simp add: hypreal_add_assoc [symmetric])
   1.411  done
   1.412  
   1.413  lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)"
   1.414 -apply (simp (no_asm) add: hypreal_add_commute hypreal_add_left_cancel)
   1.415 -done
   1.416 +by (simp add: hypreal_add_commute hypreal_add_left_cancel)
   1.417  
   1.418 -lemma hypreal_add_minus_cancelA: "z + ((- z) + w) = (w::hypreal)"
   1.419 -apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
   1.420 -done
   1.421 +lemma hypreal_add_minus_cancelA [simp]: "z + ((- z) + w) = (w::hypreal)"
   1.422 +by (simp add: hypreal_add_assoc [symmetric])
   1.423  
   1.424 -lemma hypreal_minus_add_cancelA: "(-z) + (z + w) = (w::hypreal)"
   1.425 -apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
   1.426 -done
   1.427 -
   1.428 -declare hypreal_add_minus_cancelA [simp] hypreal_minus_add_cancelA [simp]
   1.429 +lemma hypreal_minus_add_cancelA [simp]: "(-z) + (z + w) = (w::hypreal)"
   1.430 +by (simp add: hypreal_add_assoc [symmetric])
   1.431  
   1.432  (**** hyperreal multiplication: hypreal_mult  ****)
   1.433  
   1.434  lemma hypreal_mult_congruent2: 
   1.435      "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})"
   1.436 -apply (unfold congruent2_def)
   1.437 -apply auto
   1.438 -apply (ultra)
   1.439 +apply (unfold congruent2_def, auto, ultra)
   1.440  done
   1.441  
   1.442  lemma hypreal_mult: 
   1.443 @@ -524,16 +465,16 @@
   1.444  done
   1.445  
   1.446  lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
   1.447 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.448 -apply (rule_tac z = "w" in eq_Abs_hypreal)
   1.449 -apply (simp (no_asm_simp) add: hypreal_mult real_mult_ac)
   1.450 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.451 +apply (rule_tac z = w in eq_Abs_hypreal)
   1.452 +apply (simp add: hypreal_mult real_mult_ac)
   1.453  done
   1.454  
   1.455  lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
   1.456 -apply (rule_tac z = "z1" in eq_Abs_hypreal)
   1.457 -apply (rule_tac z = "z2" in eq_Abs_hypreal)
   1.458 -apply (rule_tac z = "z3" in eq_Abs_hypreal)
   1.459 -apply (simp (no_asm_simp) add: hypreal_mult real_mult_assoc)
   1.460 +apply (rule_tac z = z1 in eq_Abs_hypreal)
   1.461 +apply (rule_tac z = z2 in eq_Abs_hypreal)
   1.462 +apply (rule_tac z = z3 in eq_Abs_hypreal)
   1.463 +apply (simp add: hypreal_mult real_mult_assoc)
   1.464  done
   1.465  
   1.466  lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   1.467 @@ -546,88 +487,74 @@
   1.468  lemmas hypreal_mult_ac =
   1.469         hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute
   1.470  
   1.471 -lemma hypreal_mult_1: "(1::hypreal) * z = z"
   1.472 +lemma hypreal_mult_1 [simp]: "(1::hypreal) * z = z"
   1.473  apply (unfold hypreal_one_def)
   1.474 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.475 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.476  apply (simp add: hypreal_mult)
   1.477  done
   1.478 -declare hypreal_mult_1 [simp]
   1.479 +
   1.480 +lemma hypreal_mult_1_right [simp]: "z * (1::hypreal) = z"
   1.481 +by (simp add: hypreal_mult_commute hypreal_mult_1)
   1.482  
   1.483 -lemma hypreal_mult_1_right: "z * (1::hypreal) = z"
   1.484 -apply (simp (no_asm) add: hypreal_mult_commute hypreal_mult_1)
   1.485 -done
   1.486 -declare hypreal_mult_1_right [simp]
   1.487 -
   1.488 -lemma hypreal_mult_0: "0 * z = (0::hypreal)"
   1.489 +lemma hypreal_mult_0 [simp]: "0 * z = (0::hypreal)"
   1.490  apply (unfold hypreal_zero_def)
   1.491 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.492 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.493  apply (simp add: hypreal_mult)
   1.494  done
   1.495 -declare hypreal_mult_0 [simp]
   1.496  
   1.497 -lemma hypreal_mult_0_right: "z * 0 = (0::hypreal)"
   1.498 -apply (simp (no_asm) add: hypreal_mult_commute)
   1.499 -done
   1.500 -declare hypreal_mult_0_right [simp]
   1.501 +lemma hypreal_mult_0_right [simp]: "z * 0 = (0::hypreal)"
   1.502 +by (simp add: hypreal_mult_commute)
   1.503  
   1.504  lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)"
   1.505 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.506 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.507 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.508 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.509  apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac)
   1.510  done
   1.511  
   1.512  lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y"
   1.513 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.514 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.515 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.516 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.517  apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac)
   1.518  done
   1.519  
   1.520  (*Pull negations out*)
   1.521 -declare hypreal_minus_mult_eq2 [symmetric, simp] hypreal_minus_mult_eq1 [symmetric, simp]
   1.522 +declare hypreal_minus_mult_eq2 [symmetric, simp] 
   1.523 +        hypreal_minus_mult_eq1 [symmetric, simp]
   1.524  
   1.525 -lemma hypreal_mult_minus_1: "(- (1::hypreal)) * z = -z"
   1.526 -apply (simp (no_asm))
   1.527 -done
   1.528 -declare hypreal_mult_minus_1 [simp]
   1.529 +lemma hypreal_mult_minus_1 [simp]: "(- (1::hypreal)) * z = -z"
   1.530 +by simp
   1.531  
   1.532 -lemma hypreal_mult_minus_1_right: "z * (- (1::hypreal)) = -z"
   1.533 -apply (subst hypreal_mult_commute)
   1.534 -apply (simp (no_asm))
   1.535 -done
   1.536 -declare hypreal_mult_minus_1_right [simp]
   1.537 +lemma hypreal_mult_minus_1_right [simp]: "z * (- (1::hypreal)) = -z"
   1.538 +by (subst hypreal_mult_commute, simp)
   1.539  
   1.540  lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y"
   1.541 -apply auto
   1.542 -done
   1.543 +by auto
   1.544  
   1.545  (*-----------------------------------------------------------------------------
   1.546      A few more theorems
   1.547   ----------------------------------------------------------------------------*)
   1.548  lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   1.549 -apply (simp (no_asm_simp) add: hypreal_add_assoc [symmetric])
   1.550 -done
   1.551 +by (simp add: hypreal_add_assoc [symmetric])
   1.552  
   1.553  lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
   1.554 -apply (rule_tac z = "z1" in eq_Abs_hypreal)
   1.555 -apply (rule_tac z = "z2" in eq_Abs_hypreal)
   1.556 -apply (rule_tac z = "w" in eq_Abs_hypreal)
   1.557 -apply (simp (no_asm_simp) add: hypreal_mult hypreal_add real_add_mult_distrib)
   1.558 +apply (rule_tac z = z1 in eq_Abs_hypreal)
   1.559 +apply (rule_tac z = z2 in eq_Abs_hypreal)
   1.560 +apply (rule_tac z = w in eq_Abs_hypreal)
   1.561 +apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib)
   1.562  done
   1.563  
   1.564  lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"
   1.565 -apply (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib)
   1.566 -done
   1.567 +by (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib)
   1.568  
   1.569  
   1.570  lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)"
   1.571  
   1.572  apply (unfold hypreal_diff_def)
   1.573 -apply (simp (no_asm) add: hypreal_add_mult_distrib)
   1.574 +apply (simp add: hypreal_add_mult_distrib)
   1.575  done
   1.576  
   1.577  lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)"
   1.578 -apply (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib)
   1.579 -done
   1.580 +by (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib)
   1.581  
   1.582  (*** one and zero are distinct ***)
   1.583  lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
   1.584 @@ -641,55 +568,49 @@
   1.585  lemma hypreal_inverse_congruent: 
   1.586    "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
   1.587  apply (unfold congruent_def)
   1.588 -apply (auto , ultra)
   1.589 +apply (auto, ultra)
   1.590  done
   1.591  
   1.592  lemma hypreal_inverse: 
   1.593        "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
   1.594         Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
   1.595  apply (unfold hypreal_inverse_def)
   1.596 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   1.597 -apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   1.598 +apply (rule_tac f = Abs_hypreal in arg_cong)
   1.599 +apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   1.600             UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
   1.601  done
   1.602  
   1.603  lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
   1.604 -apply (simp (no_asm) add: hypreal_inverse hypreal_zero_def)
   1.605 -done
   1.606 +by (simp add: hypreal_inverse hypreal_zero_def)
   1.607  
   1.608  lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0"
   1.609 -apply (simp (no_asm) add: hypreal_divide_def HYPREAL_INVERSE_ZERO)
   1.610 +by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO)
   1.611 +
   1.612 +lemma hypreal_inverse_inverse [simp]: "inverse (inverse (z::hypreal)) = z"
   1.613 +apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO)
   1.614 +apply (rule_tac z = z in eq_Abs_hypreal)
   1.615 +apply (simp add: hypreal_inverse hypreal_zero_def)
   1.616  done
   1.617  
   1.618 -lemma hypreal_inverse_inverse: "inverse (inverse (z::hypreal)) = z"
   1.619 -apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO)
   1.620 -apply (rule_tac z = "z" in eq_Abs_hypreal)
   1.621 -apply (simp add: hypreal_inverse hypreal_zero_def)
   1.622 +lemma hypreal_inverse_1 [simp]: "inverse((1::hypreal)) = (1::hypreal)"
   1.623 +apply (unfold hypreal_one_def)
   1.624 +apply (simp add: hypreal_inverse real_zero_not_eq_one [THEN not_sym])
   1.625  done
   1.626 -declare hypreal_inverse_inverse [simp]
   1.627 -
   1.628 -lemma hypreal_inverse_1: "inverse((1::hypreal)) = (1::hypreal)"
   1.629 -apply (unfold hypreal_one_def)
   1.630 -apply (simp (no_asm_use) add: hypreal_inverse real_zero_not_eq_one [THEN not_sym])
   1.631 -done
   1.632 -declare hypreal_inverse_1 [simp]
   1.633  
   1.634  
   1.635  (*** existence of inverse ***)
   1.636  
   1.637 -lemma hypreal_mult_inverse: 
   1.638 +lemma hypreal_mult_inverse [simp]: 
   1.639       "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
   1.640 -
   1.641  apply (unfold hypreal_one_def hypreal_zero_def)
   1.642 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.643 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.644  apply (simp add: hypreal_inverse hypreal_mult)
   1.645  apply (drule FreeUltrafilterNat_Compl_mem)
   1.646  apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset)
   1.647  done
   1.648  
   1.649 -lemma hypreal_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
   1.650 -apply (simp (no_asm_simp) add: hypreal_mult_inverse hypreal_mult_commute)
   1.651 -done
   1.652 +lemma hypreal_mult_inverse_left [simp]: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
   1.653 +by (simp add: hypreal_mult_inverse hypreal_mult_commute)
   1.654  
   1.655  lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
   1.656  apply auto
   1.657 @@ -698,46 +619,42 @@
   1.658  done
   1.659      
   1.660  lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
   1.661 -apply (safe)
   1.662 +apply safe
   1.663  apply (drule_tac f = "%x. x*inverse c" in arg_cong)
   1.664  apply (simp add: hypreal_mult_inverse hypreal_mult_ac)
   1.665  done
   1.666  
   1.667  lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0"
   1.668  apply (unfold hypreal_zero_def)
   1.669 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.670 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.671  apply (simp add: hypreal_inverse hypreal_mult)
   1.672  done
   1.673  
   1.674 -declare hypreal_mult_inverse [simp] hypreal_mult_inverse_left [simp]
   1.675  
   1.676  lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)"
   1.677 -apply (safe)
   1.678 +apply safe
   1.679  apply (drule_tac f = "%z. inverse x*z" in arg_cong)
   1.680  apply (simp add: hypreal_mult_assoc [symmetric])
   1.681  done
   1.682  
   1.683  lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0"
   1.684 -apply (auto intro: ccontr dest: hypreal_mult_not_0)
   1.685 -done
   1.686 +by (auto intro: ccontr dest: hypreal_mult_not_0)
   1.687  
   1.688  lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)"
   1.689  apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO)
   1.690 -apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1]) 
   1.691 -apply (simp add: ); 
   1.692 -apply (subst hypreal_mult_inverse_left)
   1.693 -apply auto
   1.694 +apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1], simp) 
   1.695 +apply (subst hypreal_mult_inverse_left, auto)
   1.696  done
   1.697  
   1.698  lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)"
   1.699  apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO)
   1.700  apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO)
   1.701 -apply (frule_tac y = "y" in hypreal_mult_not_0 , assumption)
   1.702 -apply (rule_tac c1 = "x" in hypreal_mult_left_cancel [THEN iffD1])
   1.703 +apply (frule_tac y = y in hypreal_mult_not_0, assumption)
   1.704 +apply (rule_tac c1 = x in hypreal_mult_left_cancel [THEN iffD1])
   1.705  apply (auto simp add: hypreal_mult_assoc [symmetric])
   1.706 -apply (rule_tac c1 = "y" in hypreal_mult_left_cancel [THEN iffD1])
   1.707 +apply (rule_tac c1 = y in hypreal_mult_left_cancel [THEN iffD1])
   1.708  apply (auto simp add: hypreal_mult_left_commute)
   1.709 -apply (simp (no_asm_simp) add: hypreal_mult_assoc [symmetric])
   1.710 +apply (simp add: hypreal_mult_assoc [symmetric])
   1.711  done
   1.712  
   1.713  (*------------------------------------------------------------------
   1.714 @@ -751,16 +668,14 @@
   1.715                                Y \<in> Rep_hypreal(Q) &  
   1.716                                {n. X n < Y n} \<in> FreeUltrafilterNat)"
   1.717  
   1.718 -apply (unfold hypreal_less_def)
   1.719 -apply fast
   1.720 +apply (unfold hypreal_less_def, fast)
   1.721  done
   1.722  
   1.723  lemma hypreal_lessI: 
   1.724   "[| {n. X n < Y n} \<in> FreeUltrafilterNat;  
   1.725            X \<in> Rep_hypreal(P);  
   1.726            Y \<in> Rep_hypreal(Q) |] ==> P < (Q::hypreal)"
   1.727 -apply (unfold hypreal_less_def)
   1.728 -apply fast
   1.729 +apply (unfold hypreal_less_def, fast)
   1.730  done
   1.731  
   1.732  
   1.733 @@ -771,22 +686,19 @@
   1.734            !!Y. Y \<in> Rep_hypreal(R2) ==> P |]  
   1.735        ==> P"
   1.736  
   1.737 -apply (unfold hypreal_less_def)
   1.738 -apply auto
   1.739 +apply (unfold hypreal_less_def, auto)
   1.740  done
   1.741  
   1.742  lemma hypreal_lessD: 
   1.743   "R1 < (R2::hypreal) ==> (\<exists>X Y. {n. X n < Y n} \<in> FreeUltrafilterNat &  
   1.744                                     X \<in> Rep_hypreal(R1) &  
   1.745                                     Y \<in> Rep_hypreal(R2))"
   1.746 -apply (unfold hypreal_less_def)
   1.747 -apply fast
   1.748 +apply (unfold hypreal_less_def, fast)
   1.749  done
   1.750  
   1.751  lemma hypreal_less_not_refl: "~ (R::hypreal) < R"
   1.752 -apply (rule_tac z = "R" in eq_Abs_hypreal)
   1.753 -apply (auto simp add: hypreal_less_def)
   1.754 -apply (ultra)
   1.755 +apply (rule_tac z = R in eq_Abs_hypreal)
   1.756 +apply (auto simp add: hypreal_less_def, ultra)
   1.757  done
   1.758  
   1.759  (*** y < y ==> P ***)
   1.760 @@ -794,19 +706,17 @@
   1.761  declare hypreal_less_irrefl [elim!]
   1.762  
   1.763  lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
   1.764 -apply (auto simp add: hypreal_less_not_refl)
   1.765 -done
   1.766 +by (auto simp add: hypreal_less_not_refl)
   1.767  
   1.768  lemma hypreal_less_trans: "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"
   1.769 -apply (rule_tac z = "R1" in eq_Abs_hypreal)
   1.770 -apply (rule_tac z = "R2" in eq_Abs_hypreal)
   1.771 -apply (rule_tac z = "R3" in eq_Abs_hypreal)
   1.772 -apply (auto intro!: exI simp add: hypreal_less_def)
   1.773 -apply ultra
   1.774 +apply (rule_tac z = R1 in eq_Abs_hypreal)
   1.775 +apply (rule_tac z = R2 in eq_Abs_hypreal)
   1.776 +apply (rule_tac z = R3 in eq_Abs_hypreal)
   1.777 +apply (auto intro!: exI simp add: hypreal_less_def, ultra)
   1.778  done
   1.779  
   1.780  lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"
   1.781 -apply (drule hypreal_less_trans , assumption)
   1.782 +apply (drule hypreal_less_trans, assumption)
   1.783  apply (simp add: hypreal_less_not_refl)
   1.784  done
   1.785  
   1.786 @@ -820,8 +730,7 @@
   1.787              Abs_hypreal(hyprel``{%n. Y n})) =  
   1.788         ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   1.789  apply (unfold hypreal_less_def)
   1.790 -apply (auto intro!: lemma_hyprel_refl)
   1.791 -apply (ultra)
   1.792 +apply (auto intro!: lemma_hyprel_refl, ultra)
   1.793  done
   1.794  
   1.795  (*----------------------------------------------------------------------------
   1.796 @@ -831,32 +740,27 @@
   1.797  lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}"
   1.798  
   1.799  apply (unfold hyprel_def)
   1.800 -apply (rule_tac x = "%n. 0" in exI)
   1.801 -apply (safe)
   1.802 +apply (rule_tac x = "%n. 0" in exI, safe)
   1.803  apply (auto intro!: FreeUltrafilterNat_Nat_set)
   1.804  done
   1.805  
   1.806  lemma hypreal_trichotomy: "0 <  x | x = 0 | x < (0::hypreal)"
   1.807  apply (unfold hypreal_zero_def)
   1.808 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.809 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.810  apply (auto simp add: hypreal_less_def)
   1.811 -apply (cut_tac lemma_hyprel_0_mem , erule exE)
   1.812 -apply (drule_tac x = "xa" in spec)
   1.813 -apply (drule_tac x = "x" in spec)
   1.814 -apply (cut_tac x = "x" in lemma_hyprel_refl)
   1.815 -apply auto
   1.816 -apply (drule_tac x = "x" in spec)
   1.817 -apply (drule_tac x = "xa" in spec)
   1.818 -apply auto
   1.819 -apply (ultra)
   1.820 +apply (cut_tac lemma_hyprel_0_mem, erule exE)
   1.821 +apply (drule_tac x = xa in spec)
   1.822 +apply (drule_tac x = x in spec)
   1.823 +apply (cut_tac x = x in lemma_hyprel_refl, auto)
   1.824 +apply (drule_tac x = x in spec)
   1.825 +apply (drule_tac x = xa in spec, auto, ultra)
   1.826  done
   1.827  
   1.828  lemma hypreal_trichotomyE:
   1.829       "[| (0::hypreal) < x ==> P;  
   1.830           x = 0 ==> P;  
   1.831           x < 0 ==> P |] ==> P"
   1.832 -apply (insert hypreal_trichotomy [of x])
   1.833 -apply (blast intro: elim:); 
   1.834 +apply (insert hypreal_trichotomy [of x], blast) 
   1.835  done
   1.836  
   1.837  (*----------------------------------------------------------------------------
   1.838 @@ -864,72 +768,59 @@
   1.839   ----------------------------------------------------------------------------*)
   1.840  
   1.841  lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)"
   1.842 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.843 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.844 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.845 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.846  apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less)
   1.847  done
   1.848  
   1.849  lemma hypreal_less_minus_iff2: "((x::hypreal) < y) = (x + -y < 0)"
   1.850 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   1.851 -apply (rule_tac z = "y" in eq_Abs_hypreal)
   1.852 +apply (rule_tac z = x in eq_Abs_hypreal)
   1.853 +apply (rule_tac z = y in eq_Abs_hypreal)
   1.854  apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less)
   1.855  done
   1.856  
   1.857  lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
   1.858  apply auto
   1.859 -apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1])
   1.860 -apply auto
   1.861 +apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1], auto)
   1.862  done
   1.863  
   1.864  lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)"
   1.865  apply auto
   1.866 -apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1])
   1.867 -apply auto
   1.868 +apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1], auto)
   1.869  done
   1.870  
   1.871  (* 07/00 *)
   1.872 -lemma hypreal_diff_zero: "(0::hypreal) - x = -x"
   1.873 -apply (simp (no_asm) add: hypreal_diff_def)
   1.874 -done
   1.875 +lemma hypreal_diff_zero [simp]: "(0::hypreal) - x = -x"
   1.876 +by (simp add: hypreal_diff_def)
   1.877  
   1.878 -lemma hypreal_diff_zero_right: "x - (0::hypreal) = x"
   1.879 -apply (simp (no_asm) add: hypreal_diff_def)
   1.880 -done
   1.881 +lemma hypreal_diff_zero_right [simp]: "x - (0::hypreal) = x"
   1.882 +by (simp add: hypreal_diff_def)
   1.883  
   1.884 -lemma hypreal_diff_self: "x - x = (0::hypreal)"
   1.885 -apply (simp (no_asm) add: hypreal_diff_def)
   1.886 -done
   1.887 -
   1.888 -declare hypreal_diff_zero [simp] hypreal_diff_zero_right [simp] hypreal_diff_self [simp]
   1.889 +lemma hypreal_diff_self [simp]: "x - x = (0::hypreal)"
   1.890 +by (simp add: hypreal_diff_def)
   1.891  
   1.892  lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
   1.893 -apply (auto simp add: hypreal_add_assoc)
   1.894 -done
   1.895 +by (auto simp add: hypreal_add_assoc)
   1.896  
   1.897  lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))"
   1.898 -apply (auto dest: hypreal_eq_minus_iff [THEN iffD2])
   1.899 -done
   1.900 +by (auto dest: hypreal_eq_minus_iff [THEN iffD2])
   1.901  
   1.902  
   1.903  (*** linearity ***)
   1.904  
   1.905  lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x"
   1.906  apply (subst hypreal_eq_minus_iff2)
   1.907 -apply (rule_tac x1 = "x" in hypreal_less_minus_iff [THEN ssubst])
   1.908 -apply (rule_tac x1 = "y" in hypreal_less_minus_iff2 [THEN ssubst])
   1.909 -apply (rule hypreal_trichotomyE)
   1.910 -apply auto
   1.911 +apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst])
   1.912 +apply (rule_tac x1 = y in hypreal_less_minus_iff2 [THEN ssubst])
   1.913 +apply (rule hypreal_trichotomyE, auto)
   1.914  done
   1.915  
   1.916  lemma hypreal_neq_iff: "((w::hypreal) \<noteq> z) = (w<z | z<w)"
   1.917 -apply (cut_tac hypreal_linear)
   1.918 -apply blast
   1.919 -done
   1.920 +by (cut_tac hypreal_linear, blast)
   1.921  
   1.922  lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P;  x = y ==> P;  
   1.923             y < x ==> P |] ==> P"
   1.924 -apply (cut_tac x = "x" and y = "y" in hypreal_linear)
   1.925 -apply auto
   1.926 +apply (cut_tac x = x and y = y in hypreal_linear, auto)
   1.927  done
   1.928  
   1.929  (*------------------------------------------------------------------------------
   1.930 @@ -950,24 +841,19 @@
   1.931  (*---------------------------------------------------------*)
   1.932  lemma hypreal_leI: 
   1.933       "~(w < z) ==> z <= (w::hypreal)"
   1.934 -apply (unfold hypreal_le_def)
   1.935 -apply assumption
   1.936 +apply (unfold hypreal_le_def, assumption)
   1.937  done
   1.938  
   1.939  lemma hypreal_leD: 
   1.940        "z<=w ==> ~(w<(z::hypreal))"
   1.941 -apply (unfold hypreal_le_def)
   1.942 -apply assumption
   1.943 +apply (unfold hypreal_le_def, assumption)
   1.944  done
   1.945  
   1.946  lemma hypreal_less_le_iff: "(~(w < z)) = (z <= (w::hypreal))"
   1.947 -apply (fast intro!: hypreal_leI hypreal_leD)
   1.948 -done
   1.949 +by (fast intro!: hypreal_leI hypreal_leD)
   1.950  
   1.951  lemma not_hypreal_leE: "~ z <= w ==> w<(z::hypreal)"
   1.952 -apply (unfold hypreal_le_def)
   1.953 -apply fast
   1.954 -done
   1.955 +by (unfold hypreal_le_def, fast)
   1.956  
   1.957  lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x <= y ==> x < y | x = y"
   1.958  apply (unfold hypreal_le_def)
   1.959 @@ -987,14 +873,12 @@
   1.960  lemmas hypreal_le_less = hypreal_le_eq_less_or_eq
   1.961  
   1.962  lemma hypreal_le_refl: "w <= (w::hypreal)"
   1.963 -apply (simp (no_asm) add: hypreal_le_eq_less_or_eq)
   1.964 -done
   1.965 +by (simp add: hypreal_le_eq_less_or_eq)
   1.966  
   1.967  (* Axiom 'linorder_linear' of class 'linorder': *)
   1.968  lemma hypreal_le_linear: "(z::hypreal) <= w | w <= z"
   1.969 -apply (simp (no_asm) add: hypreal_le_less)
   1.970 -apply (cut_tac hypreal_linear)
   1.971 -apply blast
   1.972 +apply (simp add: hypreal_le_less)
   1.973 +apply (cut_tac hypreal_linear, blast)
   1.974  done
   1.975  
   1.976  lemma hypreal_le_trans: "[| i <= j; j <= k |] ==> i <= (k::hypreal)"
   1.977 @@ -1017,158 +901,119 @@
   1.978  
   1.979  (* Axiom 'order_less_le' of class 'order': *)
   1.980  lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)"
   1.981 -apply (simp (no_asm) add: hypreal_le_def hypreal_neq_iff)
   1.982 +apply (simp add: hypreal_le_def hypreal_neq_iff)
   1.983  apply (blast intro: hypreal_less_asym)
   1.984  done
   1.985  
   1.986 -lemma hypreal_minus_zero_less_iff: "(0 < -R) = (R < (0::hypreal))"
   1.987 -apply (rule_tac z = "R" in eq_Abs_hypreal)
   1.988 +lemma hypreal_minus_zero_less_iff [simp]: "(0 < -R) = (R < (0::hypreal))"
   1.989 +apply (rule_tac z = R in eq_Abs_hypreal)
   1.990  apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus)
   1.991  done
   1.992 -declare hypreal_minus_zero_less_iff [simp]
   1.993  
   1.994 -lemma hypreal_minus_zero_less_iff2: "(-R < 0) = ((0::hypreal) < R)"
   1.995 -apply (rule_tac z = "R" in eq_Abs_hypreal)
   1.996 +lemma hypreal_minus_zero_less_iff2 [simp]: "(-R < 0) = ((0::hypreal) < R)"
   1.997 +apply (rule_tac z = R in eq_Abs_hypreal)
   1.998  apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus)
   1.999  done
  1.1000 -declare hypreal_minus_zero_less_iff2 [simp]
  1.1001  
  1.1002 -lemma hypreal_minus_zero_le_iff: "((0::hypreal) <= -r) = (r <= 0)"
  1.1003 +lemma hypreal_minus_zero_le_iff [simp]: "((0::hypreal) <= -r) = (r <= 0)"
  1.1004  apply (unfold hypreal_le_def)
  1.1005 -apply (simp (no_asm) add: hypreal_minus_zero_less_iff2)
  1.1006 +apply (simp add: hypreal_minus_zero_less_iff2)
  1.1007  done
  1.1008 -declare hypreal_minus_zero_le_iff [simp]
  1.1009  
  1.1010 -lemma hypreal_minus_zero_le_iff2: "(-r <= (0::hypreal)) = (0 <= r)"
  1.1011 +lemma hypreal_minus_zero_le_iff2 [simp]: "(-r <= (0::hypreal)) = (0 <= r)"
  1.1012  apply (unfold hypreal_le_def)
  1.1013 -apply (simp (no_asm) add: hypreal_minus_zero_less_iff2)
  1.1014 +apply (simp add: hypreal_minus_zero_less_iff2)
  1.1015  done
  1.1016 -declare hypreal_minus_zero_le_iff2 [simp]
  1.1017  
  1.1018  (*----------------------------------------------------------
  1.1019    hypreal_of_real preserves field and order properties
  1.1020   -----------------------------------------------------------*)
  1.1021 -lemma hypreal_of_real_add: 
  1.1022 +lemma hypreal_of_real_add [simp]: 
  1.1023       "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2"
  1.1024  apply (unfold hypreal_of_real_def)
  1.1025 -apply (simp (no_asm) add: hypreal_add hypreal_add_mult_distrib)
  1.1026 +apply (simp add: hypreal_add hypreal_add_mult_distrib)
  1.1027  done
  1.1028 -declare hypreal_of_real_add [simp]
  1.1029  
  1.1030 -lemma hypreal_of_real_mult: 
  1.1031 +lemma hypreal_of_real_mult [simp]: 
  1.1032       "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2"
  1.1033  apply (unfold hypreal_of_real_def)
  1.1034 -apply (simp (no_asm) add: hypreal_mult hypreal_add_mult_distrib2)
  1.1035 +apply (simp add: hypreal_mult hypreal_add_mult_distrib2)
  1.1036  done
  1.1037 -declare hypreal_of_real_mult [simp]
  1.1038  
  1.1039 -lemma hypreal_of_real_less_iff: 
  1.1040 +lemma hypreal_of_real_less_iff [simp]: 
  1.1041       "(hypreal_of_real z1 <  hypreal_of_real z2) = (z1 < z2)"
  1.1042 -apply (unfold hypreal_less_def hypreal_of_real_def)
  1.1043 -apply auto
  1.1044 -apply (rule_tac [2] x = "%n. z1" in exI)
  1.1045 -apply (safe)
  1.1046 -apply (rule_tac [3] x = "%n. z2" in exI)
  1.1047 -apply auto
  1.1048 -apply (rule FreeUltrafilterNat_P)
  1.1049 -apply (ultra)
  1.1050 +apply (unfold hypreal_less_def hypreal_of_real_def, auto)
  1.1051 +apply (rule_tac [2] x = "%n. z1" in exI, safe)
  1.1052 +apply (rule_tac [3] x = "%n. z2" in exI, auto)
  1.1053 +apply (rule FreeUltrafilterNat_P, ultra)
  1.1054  done
  1.1055 -declare hypreal_of_real_less_iff [simp]
  1.1056  
  1.1057 -lemma hypreal_of_real_le_iff: 
  1.1058 +lemma hypreal_of_real_le_iff [simp]: 
  1.1059       "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)"
  1.1060 -apply (unfold hypreal_le_def real_le_def)
  1.1061 -apply auto
  1.1062 +apply (unfold hypreal_le_def real_le_def, auto)
  1.1063  done
  1.1064 -declare hypreal_of_real_le_iff [simp]
  1.1065  
  1.1066 -lemma hypreal_of_real_eq_iff: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)"
  1.1067 -apply (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
  1.1068 -done
  1.1069 -declare hypreal_of_real_eq_iff [simp]
  1.1070 +lemma hypreal_of_real_eq_iff [simp]: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)"
  1.1071 +by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
  1.1072  
  1.1073 -lemma hypreal_of_real_minus: "hypreal_of_real (-r) = - hypreal_of_real  r"
  1.1074 +lemma hypreal_of_real_minus [simp]: "hypreal_of_real (-r) = - hypreal_of_real  r"
  1.1075  apply (unfold hypreal_of_real_def)
  1.1076  apply (auto simp add: hypreal_minus)
  1.1077  done
  1.1078 -declare hypreal_of_real_minus [simp]
  1.1079  
  1.1080 -lemma hypreal_of_real_one: "hypreal_of_real 1 = (1::hypreal)"
  1.1081 -apply (unfold hypreal_of_real_def hypreal_one_def)
  1.1082 -apply (simp (no_asm))
  1.1083 -done
  1.1084 -declare hypreal_of_real_one [simp]
  1.1085 +lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
  1.1086 +by (unfold hypreal_of_real_def hypreal_one_def, simp)
  1.1087  
  1.1088 -lemma hypreal_of_real_zero: "hypreal_of_real 0 = 0"
  1.1089 -apply (unfold hypreal_of_real_def hypreal_zero_def)
  1.1090 -apply (simp (no_asm))
  1.1091 -done
  1.1092 -declare hypreal_of_real_zero [simp]
  1.1093 +lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
  1.1094 +by (unfold hypreal_of_real_def hypreal_zero_def, simp)
  1.1095  
  1.1096  lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)"
  1.1097 -apply (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set)
  1.1098 -done
  1.1099 +by (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set)
  1.1100  
  1.1101 -lemma hypreal_of_real_inverse: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
  1.1102 +lemma hypreal_of_real_inverse [simp]: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
  1.1103  apply (case_tac "r=0")
  1.1104 -apply (simp (no_asm_simp) add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO)
  1.1105 +apply (simp add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO)
  1.1106  apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1])
  1.1107  apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric])
  1.1108  done
  1.1109 -declare hypreal_of_real_inverse [simp]
  1.1110  
  1.1111 -lemma hypreal_of_real_divide: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2"
  1.1112 -apply (simp (no_asm) add: hypreal_divide_def real_divide_def)
  1.1113 -done
  1.1114 -declare hypreal_of_real_divide [simp]
  1.1115 +lemma hypreal_of_real_divide [simp]: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2"
  1.1116 +by (simp add: hypreal_divide_def real_divide_def)
  1.1117  
  1.1118  
  1.1119  (*** Division lemmas ***)
  1.1120  
  1.1121  lemma hypreal_zero_divide: "(0::hypreal)/x = 0"
  1.1122 -apply (simp (no_asm) add: hypreal_divide_def)
  1.1123 -done
  1.1124 +by (simp add: hypreal_divide_def)
  1.1125  
  1.1126  lemma hypreal_divide_one: "x/(1::hypreal) = x"
  1.1127 -apply (simp (no_asm) add: hypreal_divide_def)
  1.1128 -done
  1.1129 +by (simp add: hypreal_divide_def)
  1.1130  declare hypreal_zero_divide [simp] hypreal_divide_one [simp]
  1.1131  
  1.1132 -lemma hypreal_times_divide1_eq: "(x::hypreal) * (y/z) = (x*y)/z"
  1.1133 -apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_assoc)
  1.1134 -done
  1.1135 +lemma hypreal_times_divide1_eq [simp]: "(x::hypreal) * (y/z) = (x*y)/z"
  1.1136 +by (simp add: hypreal_divide_def hypreal_mult_assoc)
  1.1137  
  1.1138 -lemma hypreal_times_divide2_eq: "(y/z) * (x::hypreal) = (y*x)/z"
  1.1139 -apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_ac)
  1.1140 -done
  1.1141 +lemma hypreal_times_divide2_eq [simp]: "(y/z) * (x::hypreal) = (y*x)/z"
  1.1142 +by (simp add: hypreal_divide_def hypreal_mult_ac)
  1.1143  
  1.1144 -declare hypreal_times_divide1_eq [simp] hypreal_times_divide2_eq [simp]
  1.1145  
  1.1146 -lemma hypreal_divide_divide1_eq: "(x::hypreal) / (y/z) = (x*z)/y"
  1.1147 -apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac)
  1.1148 -done
  1.1149 +lemma hypreal_divide_divide1_eq [simp]: "(x::hypreal) / (y/z) = (x*z)/y"
  1.1150 +by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac)
  1.1151  
  1.1152 -lemma hypreal_divide_divide2_eq: "((x::hypreal) / y) / z = x/(y*z)"
  1.1153 -apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc)
  1.1154 -done
  1.1155 +lemma hypreal_divide_divide2_eq [simp]: "((x::hypreal) / y) / z = x/(y*z)"
  1.1156 +by (simp add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc)
  1.1157  
  1.1158 -declare hypreal_divide_divide1_eq [simp] hypreal_divide_divide2_eq [simp]
  1.1159  
  1.1160  (** As with multiplication, pull minus signs OUT of the / operator **)
  1.1161  
  1.1162 -lemma hypreal_minus_divide_eq: "(-x) / (y::hypreal) = - (x/y)"
  1.1163 -apply (simp (no_asm) add: hypreal_divide_def)
  1.1164 -done
  1.1165 -declare hypreal_minus_divide_eq [simp]
  1.1166 +lemma hypreal_minus_divide_eq [simp]: "(-x) / (y::hypreal) = - (x/y)"
  1.1167 +by (simp add: hypreal_divide_def)
  1.1168  
  1.1169 -lemma hypreal_divide_minus_eq: "(x / -(y::hypreal)) = - (x/y)"
  1.1170 -apply (simp (no_asm) add: hypreal_divide_def hypreal_minus_inverse)
  1.1171 -done
  1.1172 -declare hypreal_divide_minus_eq [simp]
  1.1173 +lemma hypreal_divide_minus_eq [simp]: "(x / -(y::hypreal)) = - (x/y)"
  1.1174 +by (simp add: hypreal_divide_def hypreal_minus_inverse)
  1.1175  
  1.1176  lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z"
  1.1177 -apply (simp (no_asm) add: hypreal_divide_def hypreal_add_mult_distrib)
  1.1178 -done
  1.1179 +by (simp add: hypreal_divide_def hypreal_add_mult_distrib)
  1.1180  
  1.1181  lemma hypreal_inverse_add: "[|(x::hypreal) \<noteq> 0;  y \<noteq> 0 |]   
  1.1182        ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"
  1.1183 @@ -1179,37 +1024,29 @@
  1.1184  done
  1.1185  
  1.1186  lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)"
  1.1187 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1188 -apply (auto simp add: hypreal_minus hypreal_zero_def)
  1.1189 -apply (ultra)
  1.1190 +apply (rule_tac z = x in eq_Abs_hypreal)
  1.1191 +apply (auto simp add: hypreal_minus hypreal_zero_def, ultra)
  1.1192  done
  1.1193  
  1.1194 -lemma hypreal_add_self_zero_cancel: "(x + x = 0) = (x = (0::hypreal))"
  1.1195 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  1.1196 +lemma hypreal_add_self_zero_cancel [simp]: "(x + x = 0) = (x = (0::hypreal))"
  1.1197 +apply (rule_tac z = x in eq_Abs_hypreal)
  1.1198  apply (auto simp add: hypreal_add hypreal_zero_def)
  1.1199  done
  1.1200 -declare hypreal_add_self_zero_cancel [simp]
  1.1201  
  1.1202 -lemma hypreal_add_self_zero_cancel2: "(x + x + y = y) = (x = (0::hypreal))"
  1.1203 +lemma hypreal_add_self_zero_cancel2 [simp]: "(x + x + y = y) = (x = (0::hypreal))"
  1.1204  apply auto
  1.1205  apply (drule hypreal_eq_minus_iff [THEN iffD1])
  1.1206  apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero)
  1.1207  done
  1.1208 -declare hypreal_add_self_zero_cancel2 [simp]
  1.1209  
  1.1210 -lemma hypreal_add_self_zero_cancel2a: "(x + (x + y) = y) = (x = (0::hypreal))"
  1.1211 -apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
  1.1212 -done
  1.1213 -declare hypreal_add_self_zero_cancel2a [simp]
  1.1214 +lemma hypreal_add_self_zero_cancel2a [simp]: "(x + (x + y) = y) = (x = (0::hypreal))"
  1.1215 +by (simp add: hypreal_add_assoc [symmetric])
  1.1216  
  1.1217  lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))"
  1.1218 -apply auto
  1.1219 -done
  1.1220 +by auto
  1.1221  
  1.1222 -lemma hypreal_minus_eq_cancel: "(-b = -a) = (b = (a::hypreal))"
  1.1223 -apply (simp add: hypreal_minus_eq_swap)
  1.1224 -done
  1.1225 -declare hypreal_minus_eq_cancel [simp]
  1.1226 +lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))"
  1.1227 +by (simp add: hypreal_minus_eq_swap)
  1.1228  
  1.1229  lemma hypreal_less_eq_diff: "(x<y) = (x-y < (0::hypreal))"
  1.1230  apply (unfold hypreal_diff_def)
  1.1231 @@ -1219,41 +1056,37 @@
  1.1232  (*** Subtraction laws ***)
  1.1233  
  1.1234  lemma hypreal_add_diff_eq: "x + (y - z) = (x + y) - (z::hypreal)"
  1.1235 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1236 -done
  1.1237 +by (simp add: hypreal_diff_def hypreal_add_ac)
  1.1238  
  1.1239  lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)"
  1.1240 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1241 -done
  1.1242 +by (simp add: hypreal_diff_def hypreal_add_ac)
  1.1243  
  1.1244  lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))"
  1.1245 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1246 -done
  1.1247 +by (simp add: hypreal_diff_def hypreal_add_ac)
  1.1248  
  1.1249  lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)"
  1.1250 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1251 -done
  1.1252 +by (simp add: hypreal_diff_def hypreal_add_ac)
  1.1253  
  1.1254  lemma hypreal_diff_less_eq: "(x-y < z) = (x < z + (y::hypreal))"
  1.1255  apply (subst hypreal_less_eq_diff)
  1.1256 -apply (rule_tac y1 = "z" in hypreal_less_eq_diff [THEN ssubst])
  1.1257 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1258 +apply (rule_tac y1 = z in hypreal_less_eq_diff [THEN ssubst])
  1.1259 +apply (simp add: hypreal_diff_def hypreal_add_ac)
  1.1260  done
  1.1261  
  1.1262  lemma hypreal_less_diff_eq: "(x < z-y) = (x + (y::hypreal) < z)"
  1.1263  apply (subst hypreal_less_eq_diff)
  1.1264  apply (rule_tac y1 = "z-y" in hypreal_less_eq_diff [THEN ssubst])
  1.1265 -apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  1.1266 +apply (simp add: hypreal_diff_def hypreal_add_ac)
  1.1267  done
  1.1268  
  1.1269  lemma hypreal_diff_le_eq: "(x-y <= z) = (x <= z + (y::hypreal))"
  1.1270  apply (unfold hypreal_le_def)
  1.1271 -apply (simp (no_asm) add: hypreal_less_diff_eq)
  1.1272 +apply (simp add: hypreal_less_diff_eq)
  1.1273  done
  1.1274  
  1.1275  lemma hypreal_le_diff_eq: "(x <= z-y) = (x + (y::hypreal) <= z)"
  1.1276  apply (unfold hypreal_le_def)
  1.1277 -apply (simp (no_asm) add: hypreal_diff_less_eq)
  1.1278 +apply (simp add: hypreal_diff_less_eq)
  1.1279  done
  1.1280  
  1.1281  lemma hypreal_diff_eq_eq: "(x-y = z) = (x = z + (y::hypreal))"
  1.1282 @@ -1272,13 +1105,12 @@
  1.1283  
  1.1284  lemma hypreal_less_eqI: "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')"
  1.1285  apply (subst hypreal_less_eq_diff)
  1.1286 -apply (rule_tac y1 = "y" in hypreal_less_eq_diff [THEN ssubst])
  1.1287 -apply (simp (no_asm_simp))
  1.1288 +apply (rule_tac y1 = y in hypreal_less_eq_diff [THEN ssubst], simp)
  1.1289  done
  1.1290  
  1.1291  lemma hypreal_le_eqI: "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')"
  1.1292  apply (drule hypreal_less_eqI)
  1.1293 -apply (simp (no_asm_simp) add: hypreal_le_def)
  1.1294 +apply (simp add: hypreal_le_def)
  1.1295  done
  1.1296  
  1.1297  lemma hypreal_eq_eqI: "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"
  1.1298 @@ -1287,18 +1119,15 @@
  1.1299  done
  1.1300  
  1.1301  lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
  1.1302 -apply (simp (no_asm) add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
  1.1303 -done
  1.1304 +by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
  1.1305  
  1.1306  lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})"
  1.1307 -apply (simp (no_asm) add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
  1.1308 -done
  1.1309 +by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
  1.1310  
  1.1311 -lemma hypreal_omega_gt_zero: "0 < omega"
  1.1312 +lemma hypreal_omega_gt_zero [simp]: "0 < omega"
  1.1313  apply (unfold omega_def)
  1.1314  apply (auto simp add: hypreal_less hypreal_zero_num)
  1.1315  done
  1.1316 -declare hypreal_omega_gt_zero [simp]
  1.1317  
  1.1318  ML
  1.1319  {*