author huffman Mon Sep 12 23:14:41 2005 +0200 (2005-09-12 ago) changeset 17332 4910cf8c0cd2 parent 17331 6b8b27894133 child 17333 605c97701833
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
 src/HOL/Complex/NSComplex.thy file | annotate | diff | revisions src/HOL/Hyperreal/Filter.thy file | annotate | diff | revisions src/HOL/Hyperreal/HLog.thy file | annotate | diff | revisions src/HOL/Hyperreal/HTranscendental.thy file | annotate | diff | revisions src/HOL/Hyperreal/HyperNat.thy file | annotate | diff | revisions src/HOL/Hyperreal/HyperPow.thy file | annotate | diff | revisions src/HOL/Hyperreal/NatStar.thy file | annotate | diff | revisions src/HOL/Hyperreal/StarClasses.thy file | annotate | diff | revisions src/HOL/Hyperreal/StarType.thy file | annotate | diff | revisions src/HOL/Hyperreal/Transfer.thy file | annotate | diff | revisions src/HOL/Hyperreal/transfer.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complex/NSComplex.thy	Mon Sep 12 23:13:46 2005 +0200
1.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Sep 12 23:14:41 2005 +0200
1.3 @@ -68,21 +68,15 @@
1.4    hexpi :: "hcomplex => hcomplex"
1.5    "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
1.6
1.7 -
1.8 -constdefs
1.9    HComplex :: "[hypreal,hypreal] => hcomplex"
1.10 -(*   "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"*)
1.11 -   "HComplex == Ifun2_of Complex"
1.12 -
1.13 +  "HComplex == Ifun2_of Complex"
1.14
1.15 -consts
1.16 -  "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr "hcpow" 80)
1.17 +  hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80)
1.18 +  "(z::hcomplex) hcpow (n::hypnat) == Ifun2_of (op ^) z n"
1.19
1.20 -defs
1.21 -  (* hypernatural powers of nonstandard complex numbers *)
1.22 -  hcpow_def:
1.23 -  "(z::hcomplex) hcpow (n::hypnat)
1.24 -      == Ifun2_of (op ^) z n"
1.25 +lemmas hcomplex_defs [transfer_unfold] =
1.26 +  hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
1.27 +  hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def
1.28
1.29
1.30  subsection{*Properties of Nonstandard Real and Imaginary Parts*}
1.31 @@ -95,7 +89,7 @@
1.32
1.33  lemma hcomplex_hRe_hIm_cancel_iff:
1.34       "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
1.35 -by (unfold hRe_def hIm_def, transfer, rule complex_Re_Im_cancel_iff)
1.36 +by (transfer, rule complex_Re_Im_cancel_iff)
1.37
1.38  lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
1.40 @@ -116,18 +110,18 @@
1.41  subsection{*Addition for Nonstandard Complex Numbers*}
1.42
1.43  lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
1.44 -by (unfold hRe_def, transfer, rule complex_Re_add)
1.46
1.47  lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
1.48 -by (unfold hIm_def, transfer, rule complex_Im_add)
1.50
1.51  subsection{*More Minus Laws*}
1.52
1.53  lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
1.54 -by (unfold hRe_def, transfer, rule complex_Re_minus)
1.55 +by (transfer, rule complex_Re_minus)
1.56
1.57  lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
1.58 -by (unfold hIm_def, transfer, rule complex_Im_minus)
1.59 +by (transfer, rule complex_Im_minus)
1.60
1.62        "x + y = (0::hcomplex) ==> x = -y"
1.63 @@ -179,7 +173,7 @@
1.64
1.65  lemma hcomplex_of_hypreal_cancel_iff [iff]:
1.66       "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
1.67 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.68 +by (transfer, simp)
1.69
1.70  lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
1.71  by (simp add: hcomplex_of_hypreal star_n_one_num)
1.72 @@ -189,31 +183,31 @@
1.73
1.74  lemma hcomplex_of_hypreal_minus [simp]:
1.75       "!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
1.76 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.77 +by (transfer, simp)
1.78
1.79  lemma hcomplex_of_hypreal_inverse [simp]:
1.80       "!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
1.81 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.82 +by (transfer, simp)
1.83
1.85       "!!x y. hcomplex_of_hypreal (x + y) =
1.86        hcomplex_of_hypreal x + hcomplex_of_hypreal y"
1.87 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.88 +by (transfer, simp)
1.89
1.90  lemma hcomplex_of_hypreal_diff [simp]:
1.91       "!!x y. hcomplex_of_hypreal (x - y) =
1.92        hcomplex_of_hypreal x - hcomplex_of_hypreal y "
1.93 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.94 +by (transfer, simp)
1.95
1.96  lemma hcomplex_of_hypreal_mult [simp]:
1.97       "!!x y. hcomplex_of_hypreal (x * y) =
1.98        hcomplex_of_hypreal x * hcomplex_of_hypreal y"
1.99 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.100 +by (transfer, simp)
1.101
1.102  lemma hcomplex_of_hypreal_divide [simp]:
1.103       "!!x y. hcomplex_of_hypreal(x/y) =
1.104        hcomplex_of_hypreal x / hcomplex_of_hypreal y"
1.105 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.106 +by (transfer, simp)
1.107
1.108  lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
1.109  apply (cases z)
1.110 @@ -233,10 +227,10 @@
1.111  subsection{*HComplex theorems*}
1.112
1.113  lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
1.114 -by (unfold hRe_def HComplex_def, transfer, simp)
1.115 +by (transfer, simp)
1.116
1.117  lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
1.118 -by (unfold hIm_def HComplex_def, transfer, simp)
1.119 +by (transfer, simp)
1.120
1.121  text{*Relates the two nonstandard constructions*}
1.122  lemma HComplex_eq_Abs_star_Complex:
1.123 @@ -275,28 +269,28 @@
1.124
1.125  lemma HComplex_inject [simp]:
1.126    "!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
1.127 -by (unfold HComplex_def, transfer, simp)
1.128 +by (transfer, simp)
1.129
1.131    "!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
1.132 -by (unfold HComplex_def, transfer, simp)
1.133 +by (transfer, simp)
1.134
1.135  lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
1.136 -by (unfold HComplex_def, transfer, simp)
1.137 +by (transfer, simp)
1.138
1.139  lemma HComplex_diff [simp]:
1.140    "!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
1.141 -by (unfold HComplex_def, transfer, rule complex_diff)
1.142 +by (transfer, rule complex_diff)
1.143
1.144  lemma HComplex_mult [simp]:
1.145    "!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
1.146     HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
1.147 -by (unfold HComplex_def, transfer, rule complex_mult)
1.148 +by (transfer, rule complex_mult)
1.149
1.150  (*HComplex_inverse is proved below*)
1.151
1.152  lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
1.153 -apply (unfold hcomplex_of_hypreal_def HComplex_def, transfer)
1.154 +apply (transfer)
1.156  done
1.157
1.158 @@ -318,11 +312,11 @@
1.159
1.160  lemma i_hcomplex_of_hypreal [simp]:
1.161       "!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
1.162 -by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule i_complex_of_real)
1.163 +by (transfer, rule i_complex_of_real)
1.164
1.165  lemma hcomplex_of_hypreal_i [simp]:
1.166       "!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
1.167 -by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_of_real_i)
1.168 +by (transfer, rule complex_of_real_i)
1.169
1.170
1.171  subsection{*Conjugation*}
1.172 @@ -331,56 +325,54 @@
1.173  by (simp add: hcnj_def starfun)
1.174
1.175  lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
1.176 -by (unfold hcnj_def, transfer, rule complex_cnj_cancel_iff)
1.177 +by (transfer, rule complex_cnj_cancel_iff)
1.178
1.179  lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
1.180 -by (unfold hcnj_def, transfer, rule complex_cnj_cnj)
1.181 +by (transfer, rule complex_cnj_cnj)
1.182
1.183  lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
1.184       "!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
1.185 -by (unfold hcnj_def hcomplex_of_hypreal_def, transfer, rule complex_cnj_complex_of_real)
1.186 +by (transfer, rule complex_cnj_complex_of_real)
1.187
1.188  lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
1.189 -by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_cnj)
1.190 +by (transfer, rule complex_mod_cnj)
1.191
1.192  lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
1.193 -by (unfold hcnj_def, transfer, rule complex_cnj_minus)
1.194 +by (transfer, rule complex_cnj_minus)
1.195
1.196  lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
1.197 -by (unfold hcnj_def, transfer, rule complex_cnj_inverse)
1.198 +by (transfer, rule complex_cnj_inverse)
1.199
1.200  lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
1.201 -by (unfold hcnj_def, transfer, rule complex_cnj_add)
1.203
1.204  lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
1.205 -by (unfold hcnj_def, transfer, rule complex_cnj_diff)
1.206 +by (transfer, rule complex_cnj_diff)
1.207
1.208  lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
1.209 -by (unfold hcnj_def, transfer, rule complex_cnj_mult)
1.210 +by (transfer, rule complex_cnj_mult)
1.211
1.212  lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
1.213 -by (unfold hcnj_def, transfer, rule complex_cnj_divide)
1.214 +by (transfer, rule complex_cnj_divide)
1.215
1.216  lemma hcnj_one [simp]: "hcnj 1 = 1"
1.217 -by (unfold hcnj_def, transfer, rule complex_cnj_one)
1.218 +by (transfer, rule complex_cnj_one)
1.219
1.220  lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
1.221 -by (unfold hcnj_def, transfer, rule complex_cnj_zero)
1.222 +by (transfer, rule complex_cnj_zero)
1.223
1.224  lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
1.225 -by (unfold hcnj_def, transfer, rule complex_cnj_zero_iff)
1.226 +by (transfer, rule complex_cnj_zero_iff)
1.227
1.228  lemma hcomplex_mult_hcnj:
1.229       "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
1.230 -apply (unfold hcnj_def hcomplex_of_hypreal_def hRe_def hIm_def)
1.231 -apply (transfer, rule complex_mult_cnj)
1.232 -done
1.233 +by (transfer, rule complex_mult_cnj)
1.234
1.235
1.236  subsection{*More Theorems about the Function @{term hcmod}*}
1.237
1.238  lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)"
1.239 -by (unfold hcmod_def, transfer, rule complex_mod_eq_zero_cancel)
1.240 +by (transfer, rule complex_mod_eq_zero_cancel)
1.241
1.242  lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
1.243       "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
1.244 @@ -391,57 +383,57 @@
1.245  by (simp add: abs_if linorder_not_less)
1.246
1.247  lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)"
1.248 -by (unfold hcmod_def, transfer, rule complex_mod_minus)
1.249 +by (transfer, rule complex_mod_minus)
1.250
1.251  lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
1.252 -by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_mult_cnj)
1.253 +by (transfer, rule complex_mod_mult_cnj)
1.254
1.255  lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \<le> hcmod x"
1.256 -by (unfold hcmod_def, transfer, rule complex_mod_ge_zero)
1.257 +by (transfer, rule complex_mod_ge_zero)
1.258
1.259  lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
1.260  by (simp add: abs_if linorder_not_less)
1.261
1.262  lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)"
1.263 -by (unfold hcmod_def, transfer, rule complex_mod_mult)
1.264 +by (transfer, rule complex_mod_mult)
1.265
1.267    "!!x y. hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
1.268 -by (unfold hcmod_def hcnj_def hRe_def, transfer, rule complex_mod_add_squared_eq)
1.270
1.271  lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]:
1.272    "!!x y. hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
1.273 -by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
1.274 +by (transfer, simp)
1.275
1.276  lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]:
1.277    "!!x y. hRe(x * hcnj y) \<le> hcmod(x * y)"
1.278 -by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
1.279 +by (transfer, simp)
1.280
1.281  lemma hcmod_triangle_squared [simp]:
1.282    "!!x y. hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
1.283 -by (unfold hcmod_def, transfer, simp)
1.284 +by (transfer, simp)
1.285
1.286  lemma hcmod_triangle_ineq [simp]:
1.287    "!!x y. hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
1.288 -by (unfold hcmod_def, transfer, simp)
1.289 +by (transfer, simp)
1.290
1.291  lemma hcmod_triangle_ineq2 [simp]:
1.292    "!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
1.293 -by (unfold hcmod_def, transfer, simp)
1.294 +by (transfer, simp)
1.295
1.296  lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)"
1.297 -by (unfold hcmod_def, transfer, rule complex_mod_diff_commute)
1.298 +by (transfer, rule complex_mod_diff_commute)
1.299
1.301    "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
1.302 -by (unfold hcmod_def, transfer, rule complex_mod_add_less)
1.304
1.305  lemma hcmod_mult_less:
1.306    "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
1.307 -by (unfold hcmod_def, transfer, rule complex_mod_mult_less)
1.308 +by (transfer, rule complex_mod_mult_less)
1.309
1.310  lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
1.311 -by (unfold hcmod_def, transfer, simp)
1.312 +by (transfer, simp)
1.313
1.314
1.315  subsection{*A Few Nonlinear Theorems*}
1.316 @@ -451,15 +443,13 @@
1.317
1.318  lemma hcomplex_of_hypreal_hyperpow:
1.319       "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
1.320 -apply (unfold hcomplex_of_hypreal_def hyperpow_def hcpow_def)
1.321 -apply (transfer, rule complex_of_real_pow)
1.322 -done
1.323 +by (transfer, rule complex_of_real_pow)
1.324
1.325  lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n"
1.326 -by (unfold hcmod_def hcpow_def hyperpow_def, transfer, rule complex_mod_complexpow)
1.327 +by (transfer, rule complex_mod_complexpow)
1.328
1.329  lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)"
1.330 -by (unfold hcmod_def, transfer, rule complex_mod_inverse)
1.331 +by (transfer, rule complex_mod_inverse)
1.332
1.333  lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
1.334  by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse)
1.335 @@ -496,11 +486,11 @@
1.336  lemma hcpow_minus:
1.337       "!!x n. (-x::hcomplex) hcpow n =
1.338        (if ( *p* even) n then (x hcpow n) else -(x hcpow n))"
1.339 -by (unfold hcpow_def, transfer, rule neg_power_if)
1.340 +by (transfer, rule neg_power_if)
1.341
1.342  lemma hcpow_mult:
1.343    "!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
1.344 -by (unfold hcpow_def, transfer, rule power_mult_distrib)
1.345 +by (transfer, rule power_mult_distrib)
1.346
1.347  lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
1.348  apply (simp add: star_n_zero_num star_n_one_num, cases n)
1.349 @@ -587,25 +577,23 @@
1.350       "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
1.351        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
1.352        iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
1.353 -apply (unfold hcomplex_of_hypreal_def iii_def)
1.354 -apply (transfer, rule complex_inverse_complex_split)
1.355 -done
1.356 +by (transfer, rule complex_inverse_complex_split)
1.357
1.358  lemma HComplex_inverse:
1.359       "!!x y. inverse (HComplex x y) =
1.360        HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
1.361 -by (unfold HComplex_def, transfer, rule complex_inverse)
1.362 +by (transfer, rule complex_inverse)
1.363
1.364  lemma hRe_mult_i_eq[simp]:
1.365      "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
1.366 -by (unfold hRe_def iii_def hcomplex_of_hypreal_def, transfer, simp)
1.367 +by (transfer, simp)
1.368
1.369  lemma hIm_mult_i_eq [simp]:
1.370      "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
1.371 -by (unfold hIm_def iii_def hcomplex_of_hypreal_def, transfer, simp)
1.372 +by (transfer, simp)
1.373
1.374  lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
1.375 -by (unfold hcmod_def iii_def hcomplex_of_hypreal_def, transfer, simp)
1.376 +by (transfer, simp)
1.377
1.378  lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
1.379  by (simp only: hcmod_mult_i mult_commute)
1.380 @@ -619,11 +607,11 @@
1.381
1.382  lemma cos_harg_i_mult_zero_pos:
1.383       "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
1.384 -by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_pos)
1.385 +by (transfer, rule cos_arg_i_mult_zero_pos)
1.386
1.387  lemma cos_harg_i_mult_zero_neg:
1.388       "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
1.389 -by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_neg)
1.390 +by (transfer, rule cos_arg_i_mult_zero_neg)
1.391
1.392  lemma cos_harg_i_mult_zero [simp]:
1.393       "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
1.394 @@ -632,7 +620,7 @@
1.395
1.396  lemma hcomplex_of_hypreal_zero_iff [simp]:
1.397       "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
1.398 -by (unfold hcomplex_of_hypreal_def, transfer, simp)
1.399 +by (transfer, simp)
1.400
1.401
1.402  subsection{*Polar Form for Nonstandard Complex Numbers*}
1.403 @@ -651,7 +639,7 @@
1.404
1.405  lemma hcomplex_split_polar:
1.406    "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
1.407 -by (unfold hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_split_polar)
1.408 +by (transfer, rule complex_split_polar)
1.409
1.410  lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))"
1.411  by (simp add: hcis_def starfun)
1.412 @@ -691,7 +679,7 @@
1.413
1.414  lemma hcmod_unit_one [simp]:
1.415       "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
1.416 -by (unfold hcmod_def HComplex_def, transfer, simp)
1.417 +by (transfer, simp)
1.418
1.419  lemma hcmod_complex_polar [simp]:
1.420       "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
1.421 @@ -873,11 +861,7 @@
1.422  subsection{*Numerals and Arithmetic*}
1.423
1.424  lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
1.425 -apply (rule eq_reflection)
1.426 -apply (unfold star_number_def star_of_int_def)
1.427 -apply (rule star_of_inject [THEN iffD2])
1.428 -apply (rule number_of_eq)
1.429 -done
1.430 +by (transfer, rule number_of_eq [THEN eq_reflection])
1.431
1.432  lemma hcomplex_of_complex_of_nat:
1.433       "hcomplex_of_complex (of_nat n) = of_nat n"
```
```     2.1 --- a/src/HOL/Hyperreal/Filter.thy	Mon Sep 12 23:13:46 2005 +0200
2.2 +++ b/src/HOL/Hyperreal/Filter.thy	Mon Sep 12 23:14:41 2005 +0200
2.3 @@ -60,7 +60,7 @@
2.4   apply (auto elim: subset)
2.5  done
2.6
2.7 -subsubsection {* Free ultrafilters *}
2.8 +subsubsection {* Free Ultrafilters *}
2.9
2.10  locale freeultrafilter = ultrafilter +
2.11    assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
2.12 @@ -73,7 +73,40 @@
2.13  lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
2.14  by (rule ultrafilter.intro)
2.15
2.16 -subsection {* Maximal filter = ultrafilter *}
2.17 +subsection {* Collect properties *}
2.18 +
2.19 +lemma (in filter) Collect_ex:
2.20 +  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
2.21 +proof
2.22 +  assume "{n. \<exists>x. P n x} \<in> F"
2.23 +  hence "{n. P n (SOME x. P n x)} \<in> F"
2.24 +    by (auto elim: someI subset)
2.25 +  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
2.26 +next
2.27 +  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
2.28 +    by (auto elim: subset)
2.29 +qed
2.30 +
2.31 +lemma (in filter) Collect_conj:
2.32 +  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
2.33 +by (subst Collect_conj_eq, rule Int_iff)
2.34 +
2.35 +lemma (in ultrafilter) Collect_not:
2.36 +  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
2.37 +by (subst Collect_neg_eq, rule Compl_iff)
2.38 +
2.39 +lemma (in ultrafilter) Collect_disj:
2.40 +  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
2.41 +by (subst Collect_disj_eq, rule Un_iff)
2.42 +
2.43 +lemma (in ultrafilter) Collect_all:
2.44 +  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
2.45 +apply (rule Not_eq_iff [THEN iffD1])
2.46 +apply (simp add: Collect_not [symmetric])
2.47 +apply (rule Collect_ex)
2.48 +done
2.49 +
2.50 +subsection {* Maximal filter = Ultrafilter *}
2.51
2.52  text {*
2.53     A filter F is an ultrafilter iff it is a maximal filter,
2.54 @@ -150,7 +183,7 @@
2.55    qed
2.56  qed
2.57
2.58 -subsection {* ultrafilter Theorem *}
2.59 +subsection {* Ultrafilter Theorem *}
2.60
2.61  text "A locale makes proof of ultrafilter Theorem more modular"
2.62  locale (open) UFT =
```
```     3.1 --- a/src/HOL/Hyperreal/HLog.thy	Mon Sep 12 23:13:46 2005 +0200
3.2 +++ b/src/HOL/Hyperreal/HLog.thy	Mon Sep 12 23:14:41 2005 +0200
3.3 @@ -26,47 +26,49 @@
3.4      hlog :: "[hypreal,hypreal] => hypreal"
3.5      "hlog a x == Ifun2_of log a x"
3.6
3.7 +declare powhr_def [transfer_unfold]
3.8 +declare hlog_def [transfer_unfold]
3.9
3.10  lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
3.11  by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n)
3.12
3.13  lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
3.14 -by (unfold powhr_def, transfer, simp)
3.15 +by (transfer, simp)
3.16
3.17  lemma powhr_mult:
3.18    "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
3.19 -by (unfold powhr_def, transfer, rule powr_mult)
3.20 +by (transfer, rule powr_mult)
3.21
3.22  lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
3.23 -by (unfold powhr_def, transfer, simp)
3.24 +by (transfer, simp)
3.25
3.26  lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
3.27  by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
3.28
3.29  lemma powhr_divide:
3.30    "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
3.31 -by (unfold powhr_def, transfer, rule powr_divide)
3.32 +by (transfer, rule powr_divide)
3.33
3.34  lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
3.35 -by (unfold powhr_def, transfer, rule powr_add)
3.37
3.38  lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
3.39 -by (unfold powhr_def, transfer, rule powr_powr)
3.40 +by (transfer, rule powr_powr)
3.41
3.42  lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
3.43 -by (unfold powhr_def, transfer, rule powr_powr_swap)
3.44 +by (transfer, rule powr_powr_swap)
3.45
3.46  lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
3.47 -by (unfold powhr_def, transfer, rule powr_minus)
3.48 +by (transfer, rule powr_minus)
3.49
3.50  lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
3.51  by (simp add: divide_inverse powhr_minus)
3.52
3.53  lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
3.54 -by (unfold powhr_def, transfer, simp)
3.55 +by (transfer, simp)
3.56
3.57  lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
3.58 -by (unfold powhr_def, transfer, simp)
3.59 +by (transfer, simp)
3.60
3.61  lemma powhr_less_cancel_iff [simp]:
3.62       "1 < x ==> (x powhr a < x powhr b) = (a < b)"
3.63 @@ -82,32 +84,32 @@
3.64  by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n)
3.65
3.66  lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
3.67 -by (unfold hlog_def, transfer, rule log_ln)
3.68 +by (transfer, rule log_ln)
3.69
3.70  lemma powhr_hlog_cancel [simp]:
3.71       "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
3.72 -by (unfold powhr_def hlog_def, transfer, simp)
3.73 +by (transfer, simp)
3.74
3.75  lemma hlog_powhr_cancel [simp]:
3.76       "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
3.77 -by (unfold powhr_def hlog_def, transfer, simp)
3.78 +by (transfer, simp)
3.79
3.80  lemma hlog_mult:
3.81       "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]
3.82        ==> hlog a (x * y) = hlog a x + hlog a y"
3.83 -by (unfold powhr_def hlog_def, transfer, rule log_mult)
3.84 +by (transfer, rule log_mult)
3.85
3.86  lemma hlog_as_starfun:
3.87       "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
3.88 -by (unfold hlog_def, transfer, simp add: log_def)
3.89 +by (transfer, simp add: log_def)
3.90
3.91  lemma hlog_eq_div_starfun_ln_mult_hlog:
3.92       "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
3.93        ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
3.94 -by (unfold hlog_def, transfer, rule log_eq_div_ln_mult_log)
3.95 +by (transfer, rule log_eq_div_ln_mult_log)
3.96
3.97  lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
3.98 -by (unfold powhr_def, transfer, simp add: powr_def)
3.99 +by (transfer, simp add: powr_def)
3.100
3.101  lemma HInfinite_powhr:
3.102       "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;
3.103 @@ -131,10 +133,10 @@
3.104  by (rule hlog_as_starfun, auto)
3.105
3.106  lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
3.107 -by (unfold hlog_def, transfer, simp)
3.108 +by (transfer, simp)
3.109
3.110  lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
3.111 -by (unfold hlog_def, transfer, rule log_eq_one)
3.112 +by (transfer, rule log_eq_one)
3.113
3.114  lemma hlog_inverse:
3.115       "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
3.116 @@ -148,7 +150,7 @@
3.117
3.118  lemma hlog_less_cancel_iff [simp]:
3.119       "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
3.120 -by (unfold hlog_def, transfer, simp)
3.121 +by (transfer, simp)
3.122
3.123  lemma hlog_le_cancel_iff [simp]:
3.124       "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
```
```     4.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Sep 12 23:13:46 2005 +0200
4.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Sep 12 23:14:41 2005 +0200
4.3 @@ -131,7 +131,7 @@
4.4
4.5  lemma hypreal_sqrt_hyperpow_hrabs [simp]:
4.6       "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
4.7 -by (unfold hyperpow_def, transfer, simp)
4.8 +by (transfer, simp)
4.9
4.10  lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
4.11  apply (rule HFinite_square_iff [THEN iffD1])
```
```     5.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Mon Sep 12 23:13:46 2005 +0200
5.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Sep 12 23:14:41 2005 +0200
5.3 @@ -373,6 +373,7 @@
5.4    hypreal_of_hypnat :: "hypnat => hypreal"
5.5     "hypreal_of_hypnat == *f* real"
5.6
5.7 +declare hypreal_of_hypnat_def [transfer_unfold]
5.8
5.9  lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
5.11 @@ -383,7 +384,7 @@
5.12
5.13  lemma hypreal_of_hypnat_inject [simp]:
5.14       "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
5.15 -by (unfold hypreal_of_hypnat_def, transfer, simp)
5.16 +by (transfer, simp)
5.17
5.18  lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
5.19  by (simp add: star_n_zero_num hypreal_of_hypnat)
5.20 @@ -393,22 +394,22 @@
5.21
5.23       "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
5.24 -by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_add)
5.26
5.27  lemma hypreal_of_hypnat_mult [simp]:
5.28       "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
5.29 -by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_mult)
5.30 +by (transfer, rule real_of_nat_mult)
5.31
5.32  lemma hypreal_of_hypnat_less_iff [simp]:
5.33       "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
5.34 -by (unfold hypreal_of_hypnat_def, transfer, simp)
5.35 +by (transfer, simp)
5.36
5.37  lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
5.38  by (simp add: hypreal_of_hypnat_zero [symmetric])
5.39  declare hypreal_of_hypnat_eq_zero_iff [simp]
5.40
5.41  lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n"
5.42 -by (unfold hypreal_of_hypnat_def, transfer, simp)
5.43 +by (transfer, simp)
5.44
5.45  lemma HNatInfinite_inverse_Infinitesimal [simp]:
5.46       "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
```
```     6.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Mon Sep 12 23:13:46 2005 +0200
6.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Sep 12 23:14:41 2005 +0200
6.3 @@ -24,7 +24,7 @@
6.4  defs
6.5
6.6    (* hypernatural powers of hyperreals *)
6.7 -  hyperpow_def:
6.8 +  hyperpow_def [transfer_unfold]:
6.9    "(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
6.10
6.11  lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
6.12 @@ -104,46 +104,46 @@
6.13  by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
6.14
6.15  lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
6.16 -by (unfold hyperpow_def, transfer, simp)
6.17 +by (transfer, simp)
6.18
6.19  lemma hyperpow_not_zero: "!!r n. r \<noteq> (0::hypreal) ==> r pow n \<noteq> 0"
6.20 -by (unfold hyperpow_def, transfer, simp)
6.21 +by (transfer, simp)
6.22
6.23  lemma hyperpow_inverse:
6.24       "!!r n. r \<noteq> (0::hypreal) ==> inverse(r pow n) = (inverse r) pow n"
6.25 -by (unfold hyperpow_def, transfer, rule power_inverse)
6.26 +by (transfer, rule power_inverse)
6.27
6.28  lemma hyperpow_hrabs: "!!r n. abs r pow n = abs (r pow n)"
6.29 -by (unfold hyperpow_def, transfer, rule power_abs [symmetric])
6.30 +by (transfer, rule power_abs [symmetric])
6.31
6.32  lemma hyperpow_add: "!!r n m. r pow (n + m) = (r pow n) * (r pow m)"
6.33 -by (unfold hyperpow_def, transfer, rule power_add)
6.35
6.36  lemma hyperpow_one [simp]: "!!r. r pow (1::hypnat) = r"
6.37 -by (unfold hyperpow_def, transfer, simp)
6.38 +by (transfer, simp)
6.39
6.40  lemma hyperpow_two:
6.41       "!!r. r pow ((1::hypnat) + (1::hypnat)) = r * r"
6.42 -by (unfold hyperpow_def, transfer, simp)
6.43 +by (transfer, simp)
6.44
6.45  lemma hyperpow_gt_zero: "!!r n. (0::hypreal) < r ==> 0 < r pow n"
6.46 -by (unfold hyperpow_def, transfer, rule zero_less_power)
6.47 +by (transfer, rule zero_less_power)
6.48
6.49  lemma hyperpow_ge_zero: "!!r n. (0::hypreal) \<le> r ==> 0 \<le> r pow n"
6.50 -by (unfold hyperpow_def, transfer, rule zero_le_power)
6.51 +by (transfer, rule zero_le_power)
6.52
6.53  lemma hyperpow_le:
6.54    "!!x y n. [|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
6.55 -by (unfold hyperpow_def, transfer, rule power_mono [OF _ order_less_imp_le])
6.56 +by (transfer, rule power_mono [OF _ order_less_imp_le])
6.57
6.58  lemma hyperpow_eq_one [simp]: "!!n. 1 pow n = (1::hypreal)"
6.59 -by (unfold hyperpow_def, transfer, simp)
6.60 +by (transfer, simp)
6.61
6.62  lemma hrabs_hyperpow_minus_one [simp]: "!!n. abs(-1 pow n) = (1::hypreal)"
6.63 -by (unfold hyperpow_def, transfer, simp)
6.64 +by (transfer, simp)
6.65
6.66  lemma hyperpow_mult: "!!r s n. (r * s) pow n = (r pow n) * (s pow n)"
6.67 -by (unfold hyperpow_def, transfer, rule power_mult_distrib)
6.68 +by (transfer, rule power_mult_distrib)
6.69
6.70  lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
6.71  by (auto simp add: hyperpow_two zero_le_mult_iff)
6.72 @@ -176,11 +176,11 @@
6.73
6.74  lemma hyperpow_minus_one2 [simp]:
6.75       "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
6.76 -by (unfold hyperpow_def, transfer, simp)
6.77 +by (transfer, simp)
6.78
6.79  lemma hyperpow_less_le:
6.80       "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
6.81 -by (unfold hyperpow_def, transfer, rule power_decreasing [OF order_less_imp_le])
6.82 +by (transfer, rule power_decreasing [OF order_less_imp_le])
6.83
6.84  lemma hyperpow_SHNat_le:
6.85       "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
```
```     7.1 --- a/src/HOL/Hyperreal/NatStar.thy	Mon Sep 12 23:13:46 2005 +0200
7.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Mon Sep 12 23:14:41 2005 +0200
7.3 @@ -13,7 +13,7 @@
7.4
7.5  lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
7.6  apply (simp add: starset_n_def expand_set_eq all_star_eq)
7.7 -apply (simp add: Iset_star_n fuf_disj)
7.8 +apply (simp add: Iset_star_n ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
7.9  done
7.10
7.11  lemma InternalSets_Un:
7.12 @@ -24,7 +24,7 @@
7.13  lemma starset_n_Int:
7.14        "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
7.15  apply (simp add: starset_n_def expand_set_eq all_star_eq)
7.16 -apply (simp add: Iset_star_n fuf_conj)
7.17 +apply (simp add: Iset_star_n filter.Collect_conj [OF filter_FUFNat])
7.18  done
7.19
7.20  lemma InternalSets_Int:
7.21 @@ -34,7 +34,7 @@
7.22
7.23  lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
7.24  apply (simp add: starset_n_def expand_set_eq all_star_eq)
7.25 -apply (simp add: Iset_star_n fuf_not)
7.26 +apply (simp add: Iset_star_n ultrafilter.Collect_not [OF ultrafilter_FUFNat])
7.27  done
7.28
7.29  lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
7.30 @@ -42,7 +42,8 @@
7.31
7.32  lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
7.33  apply (simp add: starset_n_def expand_set_eq all_star_eq)
7.34 -apply (simp add: Iset_star_n fuf_conj fuf_not)
7.35 +apply (simp add: Iset_star_n  filter.Collect_conj [OF filter_FUFNat]
7.36 +                 ultrafilter.Collect_not [OF ultrafilter_FUFNat])
7.37  done
7.38
7.39  lemma InternalSets_diff:
7.40 @@ -99,14 +100,14 @@
7.41  text{*The hyperpow function as a nonstandard extension of realpow*}
7.42
7.43  lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
7.44 -by (unfold hyperpow_def, transfer, rule refl)
7.45 +by (transfer, rule refl)
7.46
7.47  lemma starfun_pow2:
7.48       "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
7.49 -by (unfold hyperpow_def, transfer, rule refl)
7.50 +by (transfer, rule refl)
7.51
7.52  lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
7.53 -by (unfold hyperpow_def, transfer, rule refl)
7.54 +by (transfer, rule refl)
7.55
7.56  text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
7.57    @{term real_of_nat} *}
```
```     8.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Mon Sep 12 23:13:46 2005 +0200
8.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Mon Sep 12 23:14:41 2005 +0200
8.3 @@ -9,7 +9,148 @@
8.4  imports Transfer
8.5  begin
8.6
8.7 -subsection "HOL.thy"
8.8 +subsection {* Syntactic classes *}
8.9 +
8.10 +instance star :: (ord) ord ..
8.11 +instance star :: (zero) zero ..
8.12 +instance star :: (one) one ..
8.13 +instance star :: (plus) plus ..
8.14 +instance star :: (times) times ..
8.15 +instance star :: (minus) minus ..
8.16 +instance star :: (inverse) inverse ..
8.17 +instance star :: (number) number ..
8.18 +instance star :: ("Divides.div") "Divides.div" ..
8.19 +instance star :: (power) power ..
8.20 +
8.22 +  star_zero_def:    "0 \<equiv> star_of 0"
8.23 +  star_one_def:     "1 \<equiv> star_of 1"
8.24 +  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
8.25 +  star_add_def:     "(op +) \<equiv> Ifun2_of (op +)"
8.26 +  star_diff_def:    "(op -) \<equiv> Ifun2_of (op -)"
8.27 +  star_minus_def:   "uminus \<equiv> Ifun_of uminus"
8.28 +  star_mult_def:    "(op *) \<equiv> Ifun2_of (op *)"
8.29 +  star_divide_def:  "(op /) \<equiv> Ifun2_of (op /)"
8.30 +  star_inverse_def: "inverse \<equiv> Ifun_of inverse"
8.31 +  star_le_def:      "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
8.32 +  star_less_def:    "(op <) \<equiv> Ipred2_of (op <)"
8.33 +  star_abs_def:     "abs \<equiv> Ifun_of abs"
8.34 +  star_div_def:     "(op div) \<equiv> Ifun2_of (op div)"
8.35 +  star_mod_def:     "(op mod) \<equiv> Ifun2_of (op mod)"
8.36 +  star_power_def:   "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
8.37 +
8.38 +lemmas star_class_defs [transfer_unfold] =
8.39 +  star_zero_def     star_one_def      star_number_def
8.41 +  star_mult_def     star_divide_def   star_inverse_def
8.42 +  star_le_def       star_less_def     star_abs_def
8.43 +  star_div_def      star_mod_def      star_power_def
8.44 +
8.45 +text {* @{term star_of} preserves class operations *}
8.46 +
8.47 +lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
8.48 +by transfer (rule refl)
8.49 +
8.50 +lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
8.51 +by transfer (rule refl)
8.52 +
8.53 +lemma star_of_minus: "star_of (-x) = - star_of x"
8.54 +by transfer (rule refl)
8.55 +
8.56 +lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
8.57 +by transfer (rule refl)
8.58 +
8.59 +lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
8.60 +by transfer (rule refl)
8.61 +
8.62 +lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
8.63 +by transfer (rule refl)
8.64 +
8.65 +lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
8.66 +by transfer (rule refl)
8.67 +
8.68 +lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
8.69 +by transfer (rule refl)
8.70 +
8.71 +lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
8.72 +by transfer (rule refl)
8.73 +
8.74 +lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
8.75 +by transfer (rule refl)
8.76 +
8.77 +text {* @{term star_of} preserves numerals *}
8.78 +
8.79 +lemma star_of_zero: "star_of 0 = 0"
8.80 +by transfer (rule refl)
8.81 +
8.82 +lemma star_of_one: "star_of 1 = 1"
8.83 +by transfer (rule refl)
8.84 +
8.85 +lemma star_of_number_of: "star_of (number_of x) = number_of x"
8.86 +by transfer (rule refl)
8.87 +
8.88 +text {* @{term star_of} preserves orderings *}
8.89 +
8.90 +lemma star_of_less: "(star_of x < star_of y) = (x < y)"
8.91 +by transfer (rule refl)
8.92 +
8.93 +lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
8.94 +by transfer (rule refl)
8.95 +
8.96 +lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
8.97 +by transfer (rule refl)
8.98 +
8.99 +text{*As above, for 0*}
8.100 +
8.101 +lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
8.102 +lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
8.103 +lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
8.104 +
8.105 +lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
8.106 +lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
8.107 +lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
8.108 +
8.109 +text{*As above, for 1*}
8.110 +
8.111 +lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
8.112 +lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
8.113 +lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
8.114 +
8.115 +lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
8.116 +lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
8.117 +lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
8.118 +
8.119 +text{*As above, for numerals*}
8.120 +
8.121 +lemmas star_of_number_less =
8.122 +  star_of_less [of "number_of w", standard, simplified star_of_number_of]
8.123 +lemmas star_of_number_le   =
8.124 +  star_of_le   [of "number_of w", standard, simplified star_of_number_of]
8.125 +lemmas star_of_number_eq   =
8.126 +  star_of_eq   [of "number_of w", standard, simplified star_of_number_of]
8.127 +
8.128 +lemmas star_of_less_number =
8.129 +  star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
8.130 +lemmas star_of_le_number   =
8.131 +  star_of_le   [of _ "number_of w", standard, simplified star_of_number_of]
8.132 +lemmas star_of_eq_number   =
8.133 +  star_of_eq   [of _ "number_of w", standard, simplified star_of_number_of]
8.134 +
8.135 +lemmas star_of_simps [simp] =
8.137 +  star_of_mult    star_of_divide  star_of_inverse
8.138 +  star_of_div     star_of_mod
8.139 +  star_of_power   star_of_abs
8.140 +  star_of_zero    star_of_one     star_of_number_of
8.141 +  star_of_less    star_of_le      star_of_eq
8.142 +  star_of_0_less  star_of_0_le    star_of_0_eq
8.143 +  star_of_less_0  star_of_le_0    star_of_eq_0
8.144 +  star_of_1_less  star_of_1_le    star_of_1_eq
8.145 +  star_of_less_1  star_of_le_1    star_of_eq_1
8.146 +  star_of_number_less star_of_number_le star_of_number_eq
8.147 +  star_of_less_number star_of_le_number star_of_eq_number
8.148 +
8.149 +subsection {* Ordering classes *}
8.150
8.151  instance star :: (order) order
8.152  apply (intro_classes)
8.153 @@ -23,7 +164,7 @@
8.154  by (intro_classes, transfer, rule linorder_linear)
8.155
8.156
8.157 -subsection "LOrder.thy"
8.158 +subsection {* Lattice ordering classes *}
8.159
8.160  text {*
8.161    Some extra trouble is necessary because the class axioms
8.162 @@ -57,17 +198,17 @@
8.163
8.164  instance star :: (lorder) lorder ..
8.165
8.166 -lemma star_join_def: "join \<equiv> Ifun2_of join"
8.167 +lemma star_join_def [transfer_unfold]: "join \<equiv> Ifun2_of join"
8.168   apply (rule is_join_unique[OF is_join_join, THEN eq_reflection])
8.169   apply (transfer is_join_def, rule is_join_join)
8.170  done
8.171
8.172 -lemma star_meet_def: "meet \<equiv> Ifun2_of meet"
8.173 +lemma star_meet_def [transfer_unfold]: "meet \<equiv> Ifun2_of meet"
8.174   apply (rule is_meet_unique[OF is_meet_meet, THEN eq_reflection])
8.175   apply (transfer is_meet_def, rule is_meet_meet)
8.176  done
8.177
8.178 -subsection "OrderedGroup.thy"
8.179 +subsection {* Ordered group classes *}
8.180
8.182  by (intro_classes, transfer, rule add_assoc)
8.183 @@ -123,9 +264,7 @@
8.184  instance star :: (lordered_ab_group) lordered_ab_group ..
8.185
8.186  instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
8.187 -apply (intro_classes)
8.188 -apply (transfer star_join_def, rule abs_lattice)
8.189 -done
8.190 +by (intro_classes, transfer, rule abs_lattice)
8.191
8.192  text "Ring-and-Field.thy"
8.193
8.194 @@ -207,7 +346,7 @@
8.195  instance star :: (ordered_idom) ordered_idom ..
8.196  instance star :: (ordered_field) ordered_field ..
8.197
8.198 -subsection "Power.thy"
8.199 +subsection {* Power classes *}
8.200
8.201  text {*
8.202    Proving the class axiom @{thm [source] power_Suc} for type
8.203 @@ -227,11 +366,14 @@
8.204      by transfer (rule power_Suc)
8.205  qed
8.206
8.207 -subsection "Integ/Number.thy"
8.208 +subsection {* Number classes *}
8.209
8.210 -lemma star_of_nat_def: "of_nat n \<equiv> star_of (of_nat n)"
8.211 +lemma star_of_nat_def [transfer_unfold]: "of_nat n \<equiv> star_of (of_nat n)"
8.212  by (rule eq_reflection, induct_tac n, simp_all)
8.213
8.214 +lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
8.215 +by transfer (rule refl)
8.216 +
8.217  lemma int_diff_cases:
8.218  assumes prem: "\<And>m n. z = int m - int n \<Longrightarrow> P" shows "P"
8.219   apply (rule_tac z=z in int_cases)
8.220 @@ -239,19 +381,13 @@
8.221   apply (rule_tac m=0 and n="Suc n" in prem, simp)
8.222  done -- "Belongs in Integ/IntDef.thy"
8.223
8.224 -lemma star_of_int_def: "of_int z \<equiv> star_of (of_int z)"
8.225 - apply (rule eq_reflection)
8.226 - apply (rule_tac z=z in int_diff_cases)
8.227 - apply (simp add: star_of_nat_def)
8.228 -done
8.229 +lemma star_of_int_def [transfer_unfold]: "of_int z \<equiv> star_of (of_int z)"
8.230 +by (rule eq_reflection, rule_tac z=z in int_diff_cases, simp)
8.231 +
8.232 +lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
8.233 +by transfer (rule refl)
8.234
8.235  instance star :: (number_ring) number_ring
8.236  by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
8.237
8.238 -lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
8.240 -
8.241 -lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
8.243 -
8.244  end
```
```     9.1 --- a/src/HOL/Hyperreal/StarType.thy	Mon Sep 12 23:13:46 2005 +0200
9.2 +++ b/src/HOL/Hyperreal/StarType.thy	Mon Sep 12 23:14:41 2005 +0200
9.3 @@ -166,6 +166,10 @@
9.4    Ipred2_of :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
9.5    "Ipred2_of P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
9.6
9.7 +lemmas Ifun_defs =
9.8 +  Ifun_of_def Ifun2_def Ifun2_of_def
9.9 +  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
9.10 +
9.11  lemma Ifun_of [simp]:
9.12    "Ifun_of f (star_of x) = star_of (f x)"
9.13  by (simp only: Ifun_of_def Ifun)
9.14 @@ -182,10 +186,6 @@
9.15    "Ipred2_of P (star_of x) (star_of y) = P x y"
9.16  by (simp only: Ipred2_of_def Ifun unstar)
9.17
9.18 -lemmas Ifun_defs =
9.19 -  star_of_def Ifun_of_def Ifun2_def Ifun2_of_def
9.20 -  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
9.21 -
9.22
9.23  subsection {* Internal sets *}
9.24
9.25 @@ -201,147 +201,5 @@
9.26  by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
9.27
9.28
9.29 -subsection {* Class constants *}
9.30 -
9.31 -instance star :: (ord) ord ..
9.32 -instance star :: (zero) zero ..
9.33 -instance star :: (one) one ..
9.34 -instance star :: (plus) plus ..
9.35 -instance star :: (times) times ..
9.36 -instance star :: (minus) minus ..
9.37 -instance star :: (inverse) inverse ..
9.38 -instance star :: (number) number ..
9.39 -instance star :: ("Divides.div") "Divides.div" ..
9.40 -instance star :: (power) power ..
9.41 -
9.43 -  star_zero_def:    "0 \<equiv> star_of 0"
9.44 -  star_one_def:     "1 \<equiv> star_of 1"
9.45 -  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
9.46 -  star_add_def:     "(op +) \<equiv> Ifun2_of (op +)"
9.47 -  star_diff_def:    "(op -) \<equiv> Ifun2_of (op -)"
9.48 -  star_minus_def:   "uminus \<equiv> Ifun_of uminus"
9.49 -  star_mult_def:    "(op *) \<equiv> Ifun2_of (op *)"
9.50 -  star_divide_def:  "(op /) \<equiv> Ifun2_of (op /)"
9.51 -  star_inverse_def: "inverse \<equiv> Ifun_of inverse"
9.52 -  star_le_def:      "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
9.53 -  star_less_def:    "(op <) \<equiv> Ipred2_of (op <)"
9.54 -  star_abs_def:     "abs \<equiv> Ifun_of abs"
9.55 -  star_div_def:     "(op div) \<equiv> Ifun2_of (op div)"
9.56 -  star_mod_def:     "(op mod) \<equiv> Ifun2_of (op mod)"
9.57 -  star_power_def:   "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
9.58 -
9.59 -lemmas star_class_defs =
9.60 -  star_zero_def     star_one_def      star_number_def
9.62 -  star_mult_def     star_divide_def   star_inverse_def
9.63 -  star_le_def       star_less_def     star_abs_def
9.64 -  star_div_def      star_mod_def      star_power_def
9.65 -
9.66 -text {* @{term star_of} preserves class operations *}
9.67 -
9.68 -lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
9.70 -
9.71 -lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
9.73 -
9.74 -lemma star_of_minus: "star_of (-x) = - star_of x"
9.76 -
9.77 -lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
9.79 -
9.80 -lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
9.82 -
9.83 -lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
9.85 -
9.86 -lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
9.88 -
9.89 -lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
9.91 -
9.92 -lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
9.94 -
9.95 -lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
9.97 -
9.98 -text {* @{term star_of} preserves numerals *}
9.99 -
9.100 -lemma star_of_zero: "star_of 0 = 0"
9.102 -
9.103 -lemma star_of_one: "star_of 1 = 1"
9.105 -
9.106 -lemma star_of_number_of: "star_of (number_of x) = number_of x"
9.108 -
9.109 -text {* @{term star_of} preserves orderings *}
9.110 -
9.111 -lemma star_of_less: "(star_of x < star_of y) = (x < y)"
9.113 -
9.114 -lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
9.116 -
9.117 -lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
9.118 -by (rule star_of_inject)
9.119 -
9.120 -text{*As above, for 0*}
9.121 -
9.122 -lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
9.123 -lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
9.124 -lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
9.125 -
9.126 -lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
9.127 -lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
9.128 -lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
9.129 -
9.130 -text{*As above, for 1*}
9.131 -
9.132 -lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
9.133 -lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
9.134 -lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
9.135 -
9.136 -lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
9.137 -lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
9.138 -lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
9.139 -
9.140 -text{*As above, for numerals*}
9.141 -
9.142 -lemmas star_of_number_less =
9.143 -  star_of_less [of "number_of b", simplified star_of_number_of, standard]
9.144 -lemmas star_of_number_le   =
9.145 -  star_of_le   [of "number_of b", simplified star_of_number_of, standard]
9.146 -lemmas star_of_number_eq   =
9.147 -  star_of_eq   [of "number_of b", simplified star_of_number_of, standard]
9.148 -
9.149 -lemmas star_of_less_number =
9.150 -  star_of_less [of _ "number_of b", simplified star_of_number_of, standard]
9.151 -lemmas star_of_le_number   =
9.152 -  star_of_le   [of _ "number_of b", simplified star_of_number_of, standard]
9.153 -lemmas star_of_eq_number   =
9.154 -  star_of_eq   [of _ "number_of b", simplified star_of_number_of, standard]
9.155 -
9.156 -lemmas star_of_simps =
9.158 -  star_of_mult    star_of_divide  star_of_inverse
9.159 -  star_of_div     star_of_mod
9.160 -  star_of_power   star_of_abs
9.161 -  star_of_zero    star_of_one     star_of_number_of
9.162 -  star_of_less    star_of_le      star_of_eq
9.163 -  star_of_0_less  star_of_0_le    star_of_0_eq
9.164 -  star_of_less_0  star_of_le_0    star_of_eq_0
9.165 -  star_of_1_less  star_of_1_le    star_of_1_eq
9.166 -  star_of_less_1  star_of_le_1    star_of_eq_1
9.167 -  star_of_number_less star_of_number_le star_of_number_eq
9.168 -  star_of_less_number star_of_le_number star_of_eq_number
9.169 -
9.170 -declare star_of_simps [simp]
9.171
9.172  end
```
```    10.1 --- a/src/HOL/Hyperreal/Transfer.thy	Mon Sep 12 23:13:46 2005 +0200
10.2 +++ b/src/HOL/Hyperreal/Transfer.thy	Mon Sep 12 23:14:41 2005 +0200
10.3 @@ -7,70 +7,9 @@
10.4
10.5  theory Transfer
10.6  imports StarType
10.7 +uses ("transfer.ML")
10.8  begin
10.9
10.10 -subsection {* Preliminaries *}
10.11 -
10.12 -text {* These transform expressions like @{term "{n. f (P n)} \<in> \<U>"} *}
10.13 -
10.14 -lemma fuf_ex:
10.15 -  "({n. \<exists>x. P n x} \<in> \<U>) = (\<exists>X. {n. P n (X n)} \<in> \<U>)"
10.16 -proof
10.17 -  assume "{n. \<exists>x. P n x} \<in> \<U>"
10.18 -  hence "{n. P n (SOME x. P n x)} \<in> \<U>"
10.19 -    by (auto elim: someI filter.subset [OF filter_FUFNat])
10.20 -  thus "\<exists>X. {n. P n (X n)} \<in> \<U>" by fast
10.21 -next
10.22 -  show "\<exists>X. {n. P n (X n)} \<in> \<U> \<Longrightarrow> {n. \<exists>x. P n x} \<in> \<U>"
10.23 -    by (auto elim: filter.subset [OF filter_FUFNat])
10.24 -qed
10.25 -
10.26 -lemma fuf_not: "({n. \<not> P n} \<in> \<U>) = ({n. P n} \<notin> \<U>)"
10.27 - apply (subst Collect_neg_eq)
10.28 - apply (rule ultrafilter.Compl_iff [OF ultrafilter_FUFNat])
10.29 -done
10.30 -
10.31 -lemma fuf_conj:
10.32 -  "({n. P n \<and> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<and> {n. Q n} \<in> \<U>)"
10.33 - apply (subst Collect_conj_eq)
10.34 - apply (rule filter.Int_iff [OF filter_FUFNat])
10.35 -done
10.36 -
10.37 -lemma fuf_disj:
10.38 -  "({n. P n \<or> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<or> {n. Q n} \<in> \<U>)"
10.39 - apply (subst Collect_disj_eq)
10.40 - apply (rule ultrafilter.Un_iff [OF ultrafilter_FUFNat])
10.41 -done
10.42 -
10.43 -lemma fuf_imp:
10.44 -  "({n. P n \<longrightarrow> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<longrightarrow> {n. Q n} \<in> \<U>)"
10.45 -by (simp only: imp_conv_disj fuf_disj fuf_not)
10.46 -
10.47 -lemma fuf_iff:
10.48 -  "({n. P n = Q n} \<in> \<U>) = (({n. P n} \<in> \<U>) = ({n. Q n} \<in> \<U>))"
10.49 -by (simp add: iff_conv_conj_imp fuf_conj fuf_imp)
10.50 -
10.51 -lemma fuf_all:
10.52 -  "({n. \<forall>x. P n x} \<in> \<U>) = (\<forall>X. {n. P n (X n)} \<in> \<U>)"
10.53 - apply (rule Not_eq_iff [THEN iffD1])
10.54 - apply (simp add: fuf_not [symmetric])
10.55 - apply (rule fuf_ex)
10.56 -done
10.57 -
10.58 -lemma fuf_if_bool:
10.59 -  "({n. if P n then Q n else R n} \<in> \<U>) =
10.60 -    (if {n. P n} \<in> \<U> then {n. Q n} \<in> \<U> else {n. R n} \<in> \<U>)"
10.61 -by (simp add: if_bool_eq_conj fuf_conj fuf_imp fuf_not)
10.62 -
10.63 -lemma fuf_eq:
10.64 -  "({n. X n = Y n} \<in> \<U>) = (star_n X = star_n Y)"
10.65 -by (rule star_n_eq_iff [symmetric])
10.66 -
10.67 -lemma fuf_if:
10.68 -  "star_n (\<lambda>n. if P n then X n else Y n) =
10.69 -    (if {n. P n} \<in> \<U> then star_n X else star_n Y)"
10.70 -by (auto simp add: star_n_eq_iff fuf_not [symmetric] elim: ultra)
10.71 -
10.72  subsection {* Starting the transfer proof *}
10.73
10.74  text {*
10.75 @@ -88,6 +27,12 @@
10.76    "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
10.77  by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
10.78
10.79 +use "transfer.ML"
10.80 +setup Transfer.setup
10.81 +
10.82 +declare Ifun_defs [transfer_unfold]
10.83 +declare Iset_of_def [transfer_unfold]
10.84 +
10.85  subsection {* Transfer introduction rules *}
10.86
10.87  text {*
10.88 @@ -112,63 +57,57 @@
10.89
10.90  lemma transfer_not:
10.91    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
10.92 -by (simp only: fuf_not)
10.93 +by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
10.94
10.95  lemma transfer_conj:
10.96    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
10.97      \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
10.98 -by (simp only: fuf_conj)
10.99 +by (simp only: filter.Collect_conj [OF filter_FUFNat])
10.100
10.101  lemma transfer_disj:
10.102    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
10.103      \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
10.104 -by (simp only: fuf_disj)
10.105 +by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
10.106
10.107  lemma transfer_imp:
10.108    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
10.109      \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
10.110 -by (simp only: fuf_imp)
10.111 +by (simp only: imp_conv_disj transfer_disj transfer_not)
10.112
10.113  lemma transfer_iff:
10.114    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
10.115      \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
10.116 -by (simp only: fuf_iff)
10.117 +by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
10.118
10.119  lemma transfer_if_bool:
10.120    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
10.121      \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
10.122 -by (simp only: fuf_if_bool)
10.123 -
10.124 -lemma transfer_all_bool:
10.125 -  "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<forall>x::bool. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
10.126 -by (simp only: all_bool_eq fuf_conj)
10.127 -
10.128 -lemma transfer_ex_bool:
10.129 -  "\<lbrakk>\<And>x. p x \<equiv> {n. P n x} \<in> \<U>\<rbrakk> \<Longrightarrow> \<exists>x::bool. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
10.130 -by (simp only: ex_bool_eq fuf_disj)
10.131 +by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
10.132
10.133  subsubsection {* Equals, If *}
10.134
10.135  lemma transfer_eq:
10.136    "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
10.137 -by (simp only: fuf_eq)
10.138 +by (simp only: star_n_eq_iff)
10.139
10.140  lemma transfer_if:
10.141    "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
10.142      \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
10.143 -by (simp only: fuf_if)
10.144 +apply (rule eq_reflection)
10.145 +apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
10.146 +done
10.147
10.148  subsubsection {* Quantifiers *}
10.149
10.150 +lemma transfer_ex:
10.151 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
10.152 +    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
10.153 +by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat])
10.154 +
10.155  lemma transfer_all:
10.156    "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
10.157      \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
10.158 -by (simp only: all_star_eq fuf_all)
10.159 -
10.160 -lemma transfer_ex:
10.161 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
10.162 -    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
10.163 -by (simp only: ex_star_eq fuf_ex)
10.164 +by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat])
10.165
10.166  lemma transfer_ex1:
10.167    "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
10.168 @@ -220,20 +159,25 @@
10.169      \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
10.170  by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
10.171
10.172 +
10.173  subsubsection {* Miscellaneous *}
10.174
10.175  lemma transfer_unstar:
10.176    "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
10.177  by (simp only: unstar_star_n)
10.178
10.179 +lemma transfer_star_of: "star_of x \<equiv> star_n (\<lambda>n. x)"
10.180 +by (rule star_of_def)
10.181 +
10.182  lemma transfer_star_n: "star_n X \<equiv> star_n (\<lambda>n. X n)"
10.183  by (rule reflexive)
10.184
10.185  lemma transfer_bool: "p \<equiv> {n. p} \<in> \<U>"
10.187
10.188 -lemmas transfer_intros =
10.189 +lemmas transfer_intros [transfer_intro] =
10.190    transfer_star_n
10.191 +  transfer_star_of
10.192    transfer_Ifun
10.193    transfer_fun_eq
10.194
10.195 @@ -243,8 +187,6 @@
10.196    transfer_imp
10.197    transfer_iff
10.198    transfer_if_bool
10.199 -  transfer_all_bool
10.200 -  transfer_ex_bool
10.201
10.202    transfer_all
10.203    transfer_ex
10.204 @@ -261,148 +203,6 @@
10.205    transfer_ball
10.206    transfer_bex
10.207
10.208 -subsection {* Transfer tactic *}
10.209 -
10.210 -text {*
10.211 -  We start by giving ML bindings for the theorems that
10.212 -  will used by the transfer tactic. Ideally, some of the
10.213 -  lists of theorems should be expandable.
10.214 -  To @{text star_class_defs} we would like to add theorems
10.215 -  about @{term nat_of}, @{term int_of}, @{term meet},
10.216 -  @{term join}, etc.
10.217 -  Also, we would like to create introduction rules for new
10.218 -  constants.
10.219 -*}
10.220 -
10.221 -ML_setup {*
10.222 -val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
10.223 -val Ifun_defs = thms "Ifun_defs" @ [thm "Iset_of_def"]
10.224 -val star_class_defs = thms "star_class_defs"
10.225 -val transfer_defs = atomizers @ Ifun_defs @ star_class_defs
10.226 -
10.227 -val transfer_start = thm "transfer_start"
10.228 -val transfer_intros = thms "transfer_intros"
10.229 -val transfer_Ifun = thm "transfer_Ifun"
10.230 -*}
10.231 -
10.232 -text {*
10.233 -  Next we define the ML function @{text unstar_term}.
10.234 -  This function takes a term, and gives back an equivalent
10.235 -  term that does not contain any references to the @{text star}
10.236 -  type constructor. Hopefully the resulting term will still be
10.237 -  type-correct: Any constant whose type contains @{text star}
10.238 -  should either be polymorphic (so that it will still work at
10.239 -  the un-starred instance) or listed in @{text star_consts}
10.240 -  (so it can be removed).
10.241 -  Maybe @{text star_consts} should be extensible?
10.242 -*}
10.243 -
10.244 -ML_setup {*
10.245 -local
10.246 -  fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
10.247 -    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
10.248 -    | unstar_typ T = T
10.249 -
10.250 -  val star_consts =
10.251 -    [ "StarType.star_of", "StarType.Ifun"
10.252 -    , "StarType.Ifun_of", "StarType.Ifun2"
10.253 -    , "StarType.Ifun2_of", "StarType.Ipred"
10.254 -    , "StarType.Ipred_of", "StarType.Ipred2"
10.255 -    , "StarType.Ipred2_of", "StarType.Iset"
10.256 -    , "StarType.Iset_of", "StarType.unstar" ]
10.257 -
10.258 -  fun is_star_const a = exists (fn x => x = a) star_consts
10.259 -in
10.260 -  fun unstar_term (Const(a,T) \$ x) = if (is_star_const a)
10.261 -                     then (unstar_term x)
10.262 -                     else (Const(a,unstar_typ T) \$ unstar_term x)
10.263 -    | unstar_term (f \$ t) = unstar_term f \$ unstar_term t
10.264 -    | unstar_term (Const(a,T)) = Const(a,unstar_typ T)
10.265 -    | unstar_term (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar_term t)
10.266 -    | unstar_term t = t
10.267 -end
10.268 -*}
10.269 -
10.270 -text {*
10.271 -  The @{text transfer_thm_of} function takes a term that
10.272 -  represents a proposition, and proves that it is logically
10.273 -  equivalent to the un-starred version. Assuming all goes
10.274 -  well, it returns a theorem asserting the equivalence.
10.275 -*}
10.276 -
10.277 -text {*
10.278 -  TODO: We need some error messages for when things go
10.279 -  wrong. Errors may be caused by constants that don't have
10.280 -  matching introduction rules, or quantifiers over wrong types.
10.281 -*}
10.282 -
10.283 -ML_setup {*
10.284 -local
10.285 -  val tacs =
10.286 -    [ match_tac [transitive_thm] 1
10.287 -    , resolve_tac [transfer_start] 1
10.288 -    , REPEAT_ALL_NEW (resolve_tac transfer_intros) 1
10.289 -    , match_tac [reflexive_thm] 1 ]
10.290 -in
10.291 -  fun transfer_thm_of sg ths t =
10.292 -      let val u = unstar_term t
10.293 -          val e = Const("==", propT --> propT --> propT)
10.294 -          val c = cterm_of sg (e \$ t \$ u)
10.295 -      in prove_goalw_cterm (transfer_defs @ ths) c (fn _ => tacs)
10.296 -      end
10.297 -end
10.298 -*}
10.299 -
10.300 -text {*
10.301 -  Instead of applying the @{thm [source] transfer_start} rule
10.302 -  right away, the proof of each transfer theorem starts with the
10.303 -  transitivity rule @{text "\<lbrakk>P \<equiv> ?Q; ?Q \<equiv> P'\<rbrakk> \<Longrightarrow> P \<equiv> P'"}, which
10.304 -  introduces a new unbound schematic variable @{text ?Q}. The first
10.305 -  premise @{text "P \<equiv> ?Q"} is solved by recursively using
10.306 -  @{thm [source] transfer_start} and @{thm [source] transfer_intros}.
10.307 -  Each rule application adds constraints to the form of @{text ?Q};
10.308 -  by the time the first premise is proved, @{text ?Q} is completely
10.309 -  bound to the value of @{term P'}. Finally, the second premise is
10.310 -  resolved with the reflexivity rule @{text "P' \<equiv> P'"}.
10.311 -*}
10.312 -
10.313 -text {*
10.314 -  The delayed binding is necessary for the correct operation of the
10.315 -  introduction rule @{thm [source] transfer_Ifun}:
10.316 -  @{thm transfer_Ifun[of f _ x]}. With a subgoal of the form
10.317 -  @{term "f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"}, we would like to bind @{text ?F}
10.318 -  to @{text F} and @{text ?X} to @{term X}. Unfortunately, higher-order
10.319 -  unification finds more than one possible match, and binds @{text ?F}
10.320 -  to @{term "\<lambda>x. x"} by default. If the right-hand side of the subgoal
10.321 -  contains an unbound schematic variable instead of the explicit
10.322 -  application @{term "F n (X n)"}, then we can ensure that there is
10.323 -  only one possible way to match the rule.
10.324 -*}
10.325 -
10.326 -ML_setup {*
10.327 -fun transfer_tac ths =
10.328 -    SUBGOAL (fn (t,i) =>
10.329 -        (fn th =>
10.330 -            let val tr = transfer_thm_of (sign_of_thm th) ths t
10.331 -            in rewrite_goals_tac [tr] th
10.332 -            end
10.333 -        )
10.334 -    )
10.335 -*}
10.336 -
10.337 -text {*
10.338 -  Finally we set up the @{text transfer} method. It takes
10.339 -  an optional list of definitions as arguments; they are
10.340 -  passed along to @{text transfer_thm_of}, which expands
10.341 -  the definitions before attempting to prove the transfer
10.342 -  theorem.
10.343 -*}
10.344 -
10.345 -method_setup transfer = {*
10.346 -  Method.thms_args
10.347 -    (fn ths => Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ths))
10.348 -*} "transfer principle"
10.349 -
10.350  text {* Sample theorems *}
10.351
10.352  lemma Ifun_inject: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
```
```    11.1 --- a/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:13:46 2005 +0200
11.2 +++ b/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:14:41 2005 +0200
11.3 @@ -127,13 +127,16 @@
11.4  val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
11.5
11.6  val setup =
11.7 -  [ TransferData.init
11.9 -    [ ("transfer_intro", intro_attr, "transfer introduction rule")
11.10 -    , ("transfer_unfold", unfold_attr, "transfer unfolding rule")
11.11 -    , ("transfer_refold", refold_attr, "transfer refolding rule")
11.12 -    ]
11.14 +  [ TransferData.init,