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.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.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.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.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.291
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.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.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.313 +apply (rule_tac z = z in eq_Abs_hypreal)
1.314 +apply (rule_tac z = w in eq_Abs_hypreal)
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.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.327  done
1.328
1.329  (*For AC rewriting*)
1.330 @@ -423,32 +381,26 @@
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.340  done
1.341
1.342 -lemma hypreal_add_zero_right: "z + (0::hypreal) = z"
1.344 -done
1.345 +lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
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.354  done
1.355
1.356 -lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
1.358 -done
1.359 -
1.362 +lemma hypreal_add_minus_left [simp]: "-z + z = (0::hypreal)"
1.364
1.365  lemma hypreal_minus_ex: "\<exists>y. (x::hypreal) + y = 0"
1.367 -done
1.369
1.370  lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0"
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.398  done
1.400
1.401  lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
1.403 -done
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.411  done
1.412
1.413  lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)"
1.415 -done
1.417
1.418 -lemma hypreal_add_minus_cancelA: "z + ((- z) + w) = (w::hypreal)"
1.420 -done
1.421 +lemma hypreal_add_minus_cancelA [simp]: "z + ((- z) + w) = (w::hypreal)"
1.423
1.424 -lemma hypreal_minus_add_cancelA: "(-z) + (z + w) = (w::hypreal)"
1.426 -done
1.427 -
1.429 +lemma hypreal_minus_add_cancelA [simp]: "(-z) + (z + w) = (w::hypreal)"
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.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.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.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.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.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.550 -done
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.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.562  done
1.563
1.564  lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"
1.566 -done
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.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.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.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.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.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.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.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.891
1.892  lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
1.894 -done
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.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.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.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.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.1023       "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2"
1.1024  apply (unfold hypreal_of_real_def)
1.1027  done
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.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.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.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.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.1178 -done
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.1199  done
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.1207  done
1.1209
1.1210 -lemma hypreal_add_self_zero_cancel2a: "(x + (x + y) = y) = (x = (0::hypreal))"
1.1212 -done
1.1214 +lemma hypreal_add_self_zero_cancel2a [simp]: "(x + (x + y) = y) = (x = (0::hypreal))"
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.1224 -done
1.1225 -declare hypreal_minus_eq_cancel [simp]
1.1226 +lemma hypreal_minus_eq_cancel [simp]: "(-b = -a) = (b = (a::hypreal))"
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.1236 -done
1.1238
1.1239  lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)"
1.1241 -done
1.1243
1.1244  lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))"
1.1246 -done
1.1248
1.1249  lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)"
1.1251 -done
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.1258 +apply (rule_tac y1 = z in hypreal_less_eq_diff [THEN ssubst])
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.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.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.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.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  {*
```