added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
authorhuffman
Mon Sep 12 23:14:41 2005 +0200 (2005-09-12 ago)
changeset 173324910cf8c0cd2
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
src/HOL/Hyperreal/Filter.thy
src/HOL/Hyperreal/HLog.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Hyperreal/StarType.thy
src/HOL/Hyperreal/Transfer.thy
src/HOL/Hyperreal/transfer.ML
     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.39  by (simp add: hcomplex_hRe_hIm_cancel_iff)
    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.45 +by (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.49 +by (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.61  lemma hcomplex_add_minus_eq_minus:
    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.84  lemma hcomplex_of_hypreal_add [simp]:
    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.130  lemma HComplex_add [simp]:
   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.155  apply (simp add: complex_of_real_def)
   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.202 +by (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.266  lemma hcmod_add_squared_eq:
   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.269 +by (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.300  lemma hcmod_add_less:
   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.303 +by (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.36 +by (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.10  by (simp add: hypreal_of_nat_def) 
    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.22  lemma hypreal_of_hypnat_add [simp]:
    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.25 +by (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.34 +by (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.21 +defs (overloaded)
    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.40 +  star_add_def      star_diff_def     star_minus_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.136 +  star_of_add     star_of_diff    star_of_minus
   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.181  instance star :: (semigroup_add) semigroup_add
   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.239 -by (simp add: star_of_nat_def)
   8.240 -
   8.241 -lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
   8.242 -by (simp add: star_of_int_def)
   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.42 -defs (overloaded)
    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.61 -  star_add_def      star_diff_def     star_minus_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.69 -by (simp add: star_add_def)
    9.70 -
    9.71 -lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
    9.72 -by (simp add: star_diff_def)
    9.73 -
    9.74 -lemma star_of_minus: "star_of (-x) = - star_of x"
    9.75 -by (simp add: star_minus_def)
    9.76 -
    9.77 -lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
    9.78 -by (simp add: star_mult_def)
    9.79 -
    9.80 -lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
    9.81 -by (simp add: star_divide_def)
    9.82 -
    9.83 -lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
    9.84 -by (simp add: star_inverse_def)
    9.85 -
    9.86 -lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
    9.87 -by (simp add: star_div_def)
    9.88 -
    9.89 -lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
    9.90 -by (simp add: star_mod_def)
    9.91 -
    9.92 -lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
    9.93 -by (simp add: star_power_def)
    9.94 -
    9.95 -lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
    9.96 -by (simp add: star_abs_def)
    9.97 -
    9.98 -text {* @{term star_of} preserves numerals *}
    9.99 -
   9.100 -lemma star_of_zero: "star_of 0 = 0"
   9.101 -by (simp add: star_zero_def)
   9.102 -
   9.103 -lemma star_of_one: "star_of 1 = 1"
   9.104 -by (simp add: star_one_def)
   9.105 -
   9.106 -lemma star_of_number_of: "star_of (number_of x) = number_of x"
   9.107 -by (simp add: star_number_def)
   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.112 -by (simp add: star_less_def)
   9.113 -
   9.114 -lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
   9.115 -by (simp add: star_le_def)
   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.157 -  star_of_add     star_of_diff    star_of_minus
   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.186  by (simp add: atomize_eq)
  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.8 -  , Attrib.add_attributes
    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.13 -  , Method.add_method
   11.14 +  [ TransferData.init,
   11.15 +    Attrib.add_attributes
   11.16 +    [ ("transfer_intro", intro_attr,
   11.17 +       "declaration of transfer introduction rule"),
   11.18 +      ("transfer_unfold", unfold_attr,
   11.19 +       "declaration of transfer unfolding rule"),
   11.20 +      ("transfer_refold", refold_attr,
   11.21 +       "declaration of transfer refolding rule")
   11.22 +    ],
   11.23 +    Method.add_method
   11.24      ("transfer", Method.thms_args transfer_method, "transfer principle")
   11.25    ];
   11.26