# HG changeset patch
# User huffman
# Date 1126559681 -7200
# Node ID 4910cf8c0cd26c62f6a812df18831720faab9a20
# Parent  6b8b27894133a0e5c844b4ee35370208fe9e4ea5
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging

diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -68,21 +68,15 @@
   hexpi :: "hcomplex => hcomplex"
   "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"
 
-
-constdefs
   HComplex :: "[hypreal,hypreal] => hcomplex"
-(*   "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y"*)
-   "HComplex == Ifun2_of Complex"
-
+  "HComplex == Ifun2_of Complex"
 
-consts
-  "hcpow"  :: "[hcomplex,hypnat] => hcomplex"     (infixr "hcpow" 80)
+  hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80)
+  "(z::hcomplex) hcpow (n::hypnat) == Ifun2_of (op ^) z n"
 
-defs
-  (* hypernatural powers of nonstandard complex numbers *)
-  hcpow_def:
-  "(z::hcomplex) hcpow (n::hypnat)
-      == Ifun2_of (op ^) z n"
+lemmas hcomplex_defs [transfer_unfold] =
+  hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
+  hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def
 
 
 subsection{*Properties of Nonstandard Real and Imaginary Parts*}
@@ -95,7 +89,7 @@
 
 lemma hcomplex_hRe_hIm_cancel_iff:
      "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
-by (unfold hRe_def hIm_def, transfer, rule complex_Re_Im_cancel_iff)
+by (transfer, rule complex_Re_Im_cancel_iff)
 
 lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w"
 by (simp add: hcomplex_hRe_hIm_cancel_iff)
@@ -116,18 +110,18 @@
 subsection{*Addition for Nonstandard Complex Numbers*}
 
 lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
-by (unfold hRe_def, transfer, rule complex_Re_add)
+by (transfer, rule complex_Re_add)
 
 lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
-by (unfold hIm_def, transfer, rule complex_Im_add)
+by (transfer, rule complex_Im_add)
 
 subsection{*More Minus Laws*}
 
 lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
-by (unfold hRe_def, transfer, rule complex_Re_minus)
+by (transfer, rule complex_Re_minus)
 
 lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
-by (unfold hIm_def, transfer, rule complex_Im_minus)
+by (transfer, rule complex_Im_minus)
 
 lemma hcomplex_add_minus_eq_minus:
       "x + y = (0::hcomplex) ==> x = -y"
@@ -179,7 +173,7 @@
 
 lemma hcomplex_of_hypreal_cancel_iff [iff]:
      "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
 by (simp add: hcomplex_of_hypreal star_n_one_num)
@@ -189,31 +183,31 @@
 
 lemma hcomplex_of_hypreal_minus [simp]:
      "!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_inverse [simp]:
      "!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_add [simp]:
      "!!x y. hcomplex_of_hypreal (x + y) =
       hcomplex_of_hypreal x + hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_diff [simp]:
      "!!x y. hcomplex_of_hypreal (x - y) =
       hcomplex_of_hypreal x - hcomplex_of_hypreal y "
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_mult [simp]:
      "!!x y. hcomplex_of_hypreal (x * y) =
       hcomplex_of_hypreal x * hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_of_hypreal_divide [simp]:
      "!!x y. hcomplex_of_hypreal(x/y) =
       hcomplex_of_hypreal x / hcomplex_of_hypreal y"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
 apply (cases z)
@@ -233,10 +227,10 @@
 subsection{*HComplex theorems*}
 
 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
-by (unfold hRe_def HComplex_def, transfer, simp)
+by (transfer, simp)
 
 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
-by (unfold hIm_def HComplex_def, transfer, simp)
+by (transfer, simp)
 
 text{*Relates the two nonstandard constructions*}
 lemma HComplex_eq_Abs_star_Complex:
@@ -275,28 +269,28 @@
 
 lemma HComplex_inject [simp]:
   "!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
 
 lemma HComplex_add [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
 
 lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
-by (unfold HComplex_def, transfer, simp)
+by (transfer, simp)
 
 lemma HComplex_diff [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
-by (unfold HComplex_def, transfer, rule complex_diff)
+by (transfer, rule complex_diff)
 
 lemma HComplex_mult [simp]:
   "!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
    HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
-by (unfold HComplex_def, transfer, rule complex_mult)
+by (transfer, rule complex_mult)
 
 (*HComplex_inverse is proved below*)
 
 lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
-apply (unfold hcomplex_of_hypreal_def HComplex_def, transfer)
+apply (transfer)
 apply (simp add: complex_of_real_def)
 done
 
@@ -318,11 +312,11 @@
 
 lemma i_hcomplex_of_hypreal [simp]:
      "!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
-by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule i_complex_of_real)
+by (transfer, rule i_complex_of_real)
 
 lemma hcomplex_of_hypreal_i [simp]:
      "!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
-by (unfold iii_def hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_of_real_i)
+by (transfer, rule complex_of_real_i)
 
 
 subsection{*Conjugation*}
@@ -331,56 +325,54 @@
 by (simp add: hcnj_def starfun)
 
 lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
-by (unfold hcnj_def, transfer, rule complex_cnj_cancel_iff)
+by (transfer, rule complex_cnj_cancel_iff)
 
 lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
-by (unfold hcnj_def, transfer, rule complex_cnj_cnj)
+by (transfer, rule complex_cnj_cnj)
 
 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
      "!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-by (unfold hcnj_def hcomplex_of_hypreal_def, transfer, rule complex_cnj_complex_of_real)
+by (transfer, rule complex_cnj_complex_of_real)
 
 lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
-by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_cnj)
+by (transfer, rule complex_mod_cnj)
 
 lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
-by (unfold hcnj_def, transfer, rule complex_cnj_minus)
+by (transfer, rule complex_cnj_minus)
 
 lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_inverse)
+by (transfer, rule complex_cnj_inverse)
 
 lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_add)
+by (transfer, rule complex_cnj_add)
 
 lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_diff)
+by (transfer, rule complex_cnj_diff)
 
 lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_mult)
+by (transfer, rule complex_cnj_mult)
 
 lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
-by (unfold hcnj_def, transfer, rule complex_cnj_divide)
+by (transfer, rule complex_cnj_divide)
 
 lemma hcnj_one [simp]: "hcnj 1 = 1"
-by (unfold hcnj_def, transfer, rule complex_cnj_one)
+by (transfer, rule complex_cnj_one)
 
 lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
-by (unfold hcnj_def, transfer, rule complex_cnj_zero)
+by (transfer, rule complex_cnj_zero)
 
 lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
-by (unfold hcnj_def, transfer, rule complex_cnj_zero_iff)
+by (transfer, rule complex_cnj_zero_iff)
 
 lemma hcomplex_mult_hcnj:
      "!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
-apply (unfold hcnj_def hcomplex_of_hypreal_def hRe_def hIm_def)
-apply (transfer, rule complex_mult_cnj)
-done
+by (transfer, rule complex_mult_cnj)
 
 
 subsection{*More Theorems about the Function @{term hcmod}*}
 
 lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)"
-by (unfold hcmod_def, transfer, rule complex_mod_eq_zero_cancel)
+by (transfer, rule complex_mod_eq_zero_cancel)
 
 lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
      "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
@@ -391,57 +383,57 @@
 by (simp add: abs_if linorder_not_less)
 
 lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)"
-by (unfold hcmod_def, transfer, rule complex_mod_minus)
+by (transfer, rule complex_mod_minus)
 
 lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
-by (unfold hcmod_def hcnj_def, transfer, rule complex_mod_mult_cnj)
+by (transfer, rule complex_mod_mult_cnj)
 
 lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \<le> hcmod x"
-by (unfold hcmod_def, transfer, rule complex_mod_ge_zero)
+by (transfer, rule complex_mod_ge_zero)
 
 lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
 by (simp add: abs_if linorder_not_less)
 
 lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)"
-by (unfold hcmod_def, transfer, rule complex_mod_mult)
+by (transfer, rule complex_mod_mult)
 
 lemma hcmod_add_squared_eq:
   "!!x y. hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, rule complex_mod_add_squared_eq)
+by (transfer, rule complex_mod_add_squared_eq)
 
 lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]:
   "!!x y. hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]:
   "!!x y. hRe(x * hcnj y) \<le> hcmod(x * y)"
-by (unfold hcmod_def hcnj_def hRe_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_triangle_squared [simp]:
   "!!x y. hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_triangle_ineq [simp]:
   "!!x y. hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_triangle_ineq2 [simp]:
   "!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)"
-by (unfold hcmod_def, transfer, rule complex_mod_diff_commute)
+by (transfer, rule complex_mod_diff_commute)
 
 lemma hcmod_add_less:
   "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-by (unfold hcmod_def, transfer, rule complex_mod_add_less)
+by (transfer, rule complex_mod_add_less)
 
 lemma hcmod_mult_less:
   "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-by (unfold hcmod_def, transfer, rule complex_mod_mult_less)
+by (transfer, rule complex_mod_mult_less)
 
 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
-by (unfold hcmod_def, transfer, simp)
+by (transfer, simp)
 
 
 subsection{*A Few Nonlinear Theorems*}
@@ -451,15 +443,13 @@
 
 lemma hcomplex_of_hypreal_hyperpow:
      "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (unfold hcomplex_of_hypreal_def hyperpow_def hcpow_def)
-apply (transfer, rule complex_of_real_pow)
-done
+by (transfer, rule complex_of_real_pow)
 
 lemma hcmod_hcpow: "!!x n. hcmod(x hcpow n) = hcmod(x) pow n"
-by (unfold hcmod_def hcpow_def hyperpow_def, transfer, rule complex_mod_complexpow)
+by (transfer, rule complex_mod_complexpow)
 
 lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)"
-by (unfold hcmod_def, transfer, rule complex_mod_inverse)
+by (transfer, rule complex_mod_inverse)
 
 lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
 by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse)
@@ -496,11 +486,11 @@
 lemma hcpow_minus:
      "!!x n. (-x::hcomplex) hcpow n =
       (if ( *p* even) n then (x hcpow n) else -(x hcpow n))"
-by (unfold hcpow_def, transfer, rule neg_power_if)
+by (transfer, rule neg_power_if)
 
 lemma hcpow_mult:
   "!!r s n. ((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-by (unfold hcpow_def, transfer, rule power_mult_distrib)
+by (transfer, rule power_mult_distrib)
 
 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
 apply (simp add: star_n_zero_num star_n_one_num, cases n)
@@ -587,25 +577,23 @@
      "!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-apply (unfold hcomplex_of_hypreal_def iii_def)
-apply (transfer, rule complex_inverse_complex_split)
-done
+by (transfer, rule complex_inverse_complex_split)
 
 lemma HComplex_inverse:
      "!!x y. inverse (HComplex x y) =
       HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
-by (unfold HComplex_def, transfer, rule complex_inverse)
+by (transfer, rule complex_inverse)
 
 lemma hRe_mult_i_eq[simp]:
     "!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
-by (unfold hRe_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hIm_mult_i_eq [simp]:
     "!!y. hIm (iii * hcomplex_of_hypreal y) = y"
-by (unfold hIm_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
-by (unfold hcmod_def iii_def hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
 by (simp only: hcmod_mult_i mult_commute)
@@ -619,11 +607,11 @@
 
 lemma cos_harg_i_mult_zero_pos:
      "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_pos)
+by (transfer, rule cos_arg_i_mult_zero_pos)
 
 lemma cos_harg_i_mult_zero_neg:
      "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-by (unfold harg_def HComplex_def, transfer, rule cos_arg_i_mult_zero_neg)
+by (transfer, rule cos_arg_i_mult_zero_neg)
 
 lemma cos_harg_i_mult_zero [simp]:
      "y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
@@ -632,7 +620,7 @@
 
 lemma hcomplex_of_hypreal_zero_iff [simp]:
      "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
-by (unfold hcomplex_of_hypreal_def, transfer, simp)
+by (transfer, simp)
 
 
 subsection{*Polar Form for Nonstandard Complex Numbers*}
@@ -651,7 +639,7 @@
 
 lemma hcomplex_split_polar:
   "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
-by (unfold hcomplex_of_hypreal_def HComplex_def, transfer, rule complex_split_polar)
+by (transfer, rule complex_split_polar)
 
 lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))"
 by (simp add: hcis_def starfun)
@@ -691,7 +679,7 @@
 
 lemma hcmod_unit_one [simp]:
      "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-by (unfold hcmod_def HComplex_def, transfer, simp)
+by (transfer, simp)
 
 lemma hcmod_complex_polar [simp]:
      "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
@@ -873,11 +861,7 @@
 subsection{*Numerals and Arithmetic*}
 
 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
-apply (rule eq_reflection)
-apply (unfold star_number_def star_of_int_def)
-apply (rule star_of_inject [THEN iffD2])
-apply (rule number_of_eq)
-done
+by (transfer, rule number_of_eq [THEN eq_reflection])
 
 lemma hcomplex_of_complex_of_nat:
      "hcomplex_of_complex (of_nat n) = of_nat n"
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/Filter.thy
--- a/src/HOL/Hyperreal/Filter.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/Filter.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -60,7 +60,7 @@
  apply (auto elim: subset)
 done
 
-subsubsection {* Free ultrafilters *}
+subsubsection {* Free Ultrafilters *}
 
 locale freeultrafilter = ultrafilter +
   assumes infinite: "A \<in> F \<Longrightarrow> infinite A"
@@ -73,7 +73,40 @@
 lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
 by (rule ultrafilter.intro)
 
-subsection {* Maximal filter = ultrafilter *}
+subsection {* Collect properties *}
+
+lemma (in filter) Collect_ex:
+  "({n. \<exists>x. P n x} \<in> F) = (\<exists>X. {n. P n (X n)} \<in> F)"
+proof
+  assume "{n. \<exists>x. P n x} \<in> F"
+  hence "{n. P n (SOME x. P n x)} \<in> F"
+    by (auto elim: someI subset)
+  thus "\<exists>X. {n. P n (X n)} \<in> F" by fast
+next
+  show "\<exists>X. {n. P n (X n)} \<in> F \<Longrightarrow> {n. \<exists>x. P n x} \<in> F"
+    by (auto elim: subset)
+qed
+
+lemma (in filter) Collect_conj:
+  "({n. P n \<and> Q n} \<in> F) = ({n. P n} \<in> F \<and> {n. Q n} \<in> F)"
+by (subst Collect_conj_eq, rule Int_iff)
+
+lemma (in ultrafilter) Collect_not:
+  "({n. \<not> P n} \<in> F) = ({n. P n} \<notin> F)"
+by (subst Collect_neg_eq, rule Compl_iff)
+
+lemma (in ultrafilter) Collect_disj:
+  "({n. P n \<or> Q n} \<in> F) = ({n. P n} \<in> F \<or> {n. Q n} \<in> F)"
+by (subst Collect_disj_eq, rule Un_iff)
+
+lemma (in ultrafilter) Collect_all:
+  "({n. \<forall>x. P n x} \<in> F) = (\<forall>X. {n. P n (X n)} \<in> F)"
+apply (rule Not_eq_iff [THEN iffD1])
+apply (simp add: Collect_not [symmetric])
+apply (rule Collect_ex)
+done
+
+subsection {* Maximal filter = Ultrafilter *}
 
 text {*
    A filter F is an ultrafilter iff it is a maximal filter,
@@ -150,7 +183,7 @@
   qed
 qed
 
-subsection {* ultrafilter Theorem *}
+subsection {* Ultrafilter Theorem *}
 
 text "A locale makes proof of ultrafilter Theorem more modular"
 locale (open) UFT =
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -26,47 +26,49 @@
     hlog :: "[hypreal,hypreal] => hypreal"
     "hlog a x == Ifun2_of log a x"
 
+declare powhr_def [transfer_unfold]
+declare hlog_def [transfer_unfold]
 
 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
 by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
 
 lemma powhr_mult:
   "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-by (unfold powhr_def, transfer, rule powr_mult)
+by (transfer, rule powr_mult)
 
 lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
 
 lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
 by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
 
 lemma powhr_divide:
   "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-by (unfold powhr_def, transfer, rule powr_divide)
+by (transfer, rule powr_divide)
 
 lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
-by (unfold powhr_def, transfer, rule powr_add)
+by (transfer, rule powr_add)
 
 lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
-by (unfold powhr_def, transfer, rule powr_powr)
+by (transfer, rule powr_powr)
 
 lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
-by (unfold powhr_def, transfer, rule powr_powr_swap)
+by (transfer, rule powr_powr_swap)
 
 lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
-by (unfold powhr_def, transfer, rule powr_minus)
+by (transfer, rule powr_minus)
 
 lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
 by (simp add: divide_inverse powhr_minus)
 
 lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
 
 lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
-by (unfold powhr_def, transfer, simp)
+by (transfer, simp)
 
 lemma powhr_less_cancel_iff [simp]:
      "1 < x ==> (x powhr a < x powhr b) = (a < b)"
@@ -82,32 +84,32 @@
 by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
-by (unfold hlog_def, transfer, rule log_ln)
+by (transfer, rule log_ln)
 
 lemma powhr_hlog_cancel [simp]:
      "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-by (unfold powhr_def hlog_def, transfer, simp)
+by (transfer, simp)
 
 lemma hlog_powhr_cancel [simp]:
      "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-by (unfold powhr_def hlog_def, transfer, simp)
+by (transfer, simp)
 
 lemma hlog_mult:
      "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
       ==> hlog a (x * y) = hlog a x + hlog a y"
-by (unfold powhr_def hlog_def, transfer, rule log_mult)
+by (transfer, rule log_mult)
 
 lemma hlog_as_starfun:
      "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (unfold hlog_def, transfer, simp add: log_def)
+by (transfer, simp add: log_def)
 
 lemma hlog_eq_div_starfun_ln_mult_hlog:
      "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
       ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-by (unfold hlog_def, transfer, rule log_eq_div_ln_mult_log)
+by (transfer, rule log_eq_div_ln_mult_log)
 
 lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-by (unfold powhr_def, transfer, simp add: powr_def)
+by (transfer, simp add: powr_def)
 
 lemma HInfinite_powhr:
      "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
@@ -131,10 +133,10 @@
 by (rule hlog_as_starfun, auto)
 
 lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
-by (unfold hlog_def, transfer, simp)
+by (transfer, simp)
 
 lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-by (unfold hlog_def, transfer, rule log_eq_one)
+by (transfer, rule log_eq_one)
 
 lemma hlog_inverse:
      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
@@ -148,7 +150,7 @@
 
 lemma hlog_less_cancel_iff [simp]:
      "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-by (unfold hlog_def, transfer, simp)
+by (transfer, simp)
 
 lemma hlog_le_cancel_iff [simp]:
      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -131,7 +131,7 @@
 
 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
      "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
 apply (rule HFinite_square_iff [THEN iffD1])
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -373,6 +373,7 @@
   hypreal_of_hypnat :: "hypnat => hypreal"
    "hypreal_of_hypnat == *f* real"
 
+declare hypreal_of_hypnat_def [transfer_unfold]
 
 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
 by (simp add: hypreal_of_nat_def) 
@@ -383,7 +384,7 @@
 
 lemma hypreal_of_hypnat_inject [simp]:
      "!!m n. (hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
 
 lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
 by (simp add: star_n_zero_num hypreal_of_hypnat)
@@ -393,22 +394,22 @@
 
 lemma hypreal_of_hypnat_add [simp]:
      "!!m n. hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_add)
+by (transfer, rule real_of_nat_add)
 
 lemma hypreal_of_hypnat_mult [simp]:
      "!!m n. hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, rule real_of_nat_mult)
+by (transfer, rule real_of_nat_mult)
 
 lemma hypreal_of_hypnat_less_iff [simp]:
      "!!m n. (hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
 
 lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
 by (simp add: hypreal_of_hypnat_zero [symmetric])
 declare hypreal_of_hypnat_eq_zero_iff [simp]
 
 lemma hypreal_of_hypnat_ge_zero [simp]: "!!n. 0 \<le> hypreal_of_hypnat n"
-by (unfold hypreal_of_hypnat_def, transfer, simp)
+by (transfer, simp)
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -24,7 +24,7 @@
 defs
 
   (* hypernatural powers of hyperreals *)
-  hyperpow_def:
+  hyperpow_def [transfer_unfold]:
   "(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
 
 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
@@ -104,46 +104,46 @@
 by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_not_zero: "!!r n. r \<noteq> (0::hypreal) ==> r pow n \<noteq> 0"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_inverse:
      "!!r n. r \<noteq> (0::hypreal) ==> inverse(r pow n) = (inverse r) pow n"
-by (unfold hyperpow_def, transfer, rule power_inverse)
+by (transfer, rule power_inverse)
 
 lemma hyperpow_hrabs: "!!r n. abs r pow n = abs (r pow n)"
-by (unfold hyperpow_def, transfer, rule power_abs [symmetric])
+by (transfer, rule power_abs [symmetric])
 
 lemma hyperpow_add: "!!r n m. r pow (n + m) = (r pow n) * (r pow m)"
-by (unfold hyperpow_def, transfer, rule power_add)
+by (transfer, rule power_add)
 
 lemma hyperpow_one [simp]: "!!r. r pow (1::hypnat) = r"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_two:
      "!!r. r pow ((1::hypnat) + (1::hypnat)) = r * r"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_gt_zero: "!!r n. (0::hypreal) < r ==> 0 < r pow n"
-by (unfold hyperpow_def, transfer, rule zero_less_power)
+by (transfer, rule zero_less_power)
 
 lemma hyperpow_ge_zero: "!!r n. (0::hypreal) \<le> r ==> 0 \<le> r pow n"
-by (unfold hyperpow_def, transfer, rule zero_le_power)
+by (transfer, rule zero_le_power)
 
 lemma hyperpow_le:
   "!!x y n. [|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-by (unfold hyperpow_def, transfer, rule power_mono [OF _ order_less_imp_le])
+by (transfer, rule power_mono [OF _ order_less_imp_le])
 
 lemma hyperpow_eq_one [simp]: "!!n. 1 pow n = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hrabs_hyperpow_minus_one [simp]: "!!n. abs(-1 pow n) = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_mult: "!!r s n. (r * s) pow n = (r pow n) * (s pow n)"
-by (unfold hyperpow_def, transfer, rule power_mult_distrib)
+by (transfer, rule power_mult_distrib)
 
 lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
 by (auto simp add: hyperpow_two zero_le_mult_iff)
@@ -176,11 +176,11 @@
 
 lemma hyperpow_minus_one2 [simp]:
      "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
-by (unfold hyperpow_def, transfer, simp)
+by (transfer, simp)
 
 lemma hyperpow_less_le:
      "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-by (unfold hyperpow_def, transfer, rule power_decreasing [OF order_less_imp_le])
+by (transfer, rule power_decreasing [OF order_less_imp_le])
 
 lemma hyperpow_SHNat_le:
      "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -13,7 +13,7 @@
 
 lemma starset_n_Un: "*sn* (%n. (A n) Un (B n)) = *sn* A Un *sn* B"
 apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_disj)
+apply (simp add: Iset_star_n ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
 done
 
 lemma InternalSets_Un:
@@ -24,7 +24,7 @@
 lemma starset_n_Int:
       "*sn* (%n. (A n) Int (B n)) = *sn* A Int *sn* B"
 apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_conj)
+apply (simp add: Iset_star_n filter.Collect_conj [OF filter_FUFNat])
 done
 
 lemma InternalSets_Int:
@@ -34,7 +34,7 @@
 
 lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
 apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_not)
+apply (simp add: Iset_star_n ultrafilter.Collect_not [OF ultrafilter_FUFNat])
 done
 
 lemma InternalSets_Compl: "X \<in> InternalSets ==> -X \<in> InternalSets"
@@ -42,7 +42,8 @@
 
 lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
 apply (simp add: starset_n_def expand_set_eq all_star_eq)
-apply (simp add: Iset_star_n fuf_conj fuf_not)
+apply (simp add: Iset_star_n  filter.Collect_conj [OF filter_FUFNat]
+                 ultrafilter.Collect_not [OF ultrafilter_FUFNat])
 done
 
 lemma InternalSets_diff:
@@ -99,14 +100,14 @@
 text{*The hyperpow function as a nonstandard extension of realpow*}
 
 lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
 
 lemma starfun_pow2:
      "!!N. ( *f* (%n. (X n) ^ m)) N = ( *f* X) N pow hypnat_of_nat m"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
 
 lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
-by (unfold hyperpow_def, transfer, rule refl)
+by (transfer, rule refl)
 
 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
   @{term real_of_nat} *}
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -9,7 +9,148 @@
 imports Transfer
 begin
 
-subsection "HOL.thy"
+subsection {* Syntactic classes *}
+
+instance star :: (ord) ord ..
+instance star :: (zero) zero ..
+instance star :: (one) one ..
+instance star :: (plus) plus ..
+instance star :: (times) times ..
+instance star :: (minus) minus ..
+instance star :: (inverse) inverse ..
+instance star :: (number) number ..
+instance star :: ("Divides.div") "Divides.div" ..
+instance star :: (power) power ..
+
+defs (overloaded)
+  star_zero_def:    "0 \<equiv> star_of 0"
+  star_one_def:     "1 \<equiv> star_of 1"
+  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
+  star_add_def:     "(op +) \<equiv> Ifun2_of (op +)"
+  star_diff_def:    "(op -) \<equiv> Ifun2_of (op -)"
+  star_minus_def:   "uminus \<equiv> Ifun_of uminus"
+  star_mult_def:    "(op *) \<equiv> Ifun2_of (op *)"
+  star_divide_def:  "(op /) \<equiv> Ifun2_of (op /)"
+  star_inverse_def: "inverse \<equiv> Ifun_of inverse"
+  star_le_def:      "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
+  star_less_def:    "(op <) \<equiv> Ipred2_of (op <)"
+  star_abs_def:     "abs \<equiv> Ifun_of abs"
+  star_div_def:     "(op div) \<equiv> Ifun2_of (op div)"
+  star_mod_def:     "(op mod) \<equiv> Ifun2_of (op mod)"
+  star_power_def:   "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
+
+lemmas star_class_defs [transfer_unfold] =
+  star_zero_def     star_one_def      star_number_def
+  star_add_def      star_diff_def     star_minus_def
+  star_mult_def     star_divide_def   star_inverse_def
+  star_le_def       star_less_def     star_abs_def
+  star_div_def      star_mod_def      star_power_def
+
+text {* @{term star_of} preserves class operations *}
+
+lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
+by transfer (rule refl)
+
+lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
+by transfer (rule refl)
+
+lemma star_of_minus: "star_of (-x) = - star_of x"
+by transfer (rule refl)
+
+lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
+by transfer (rule refl)
+
+lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
+by transfer (rule refl)
+
+lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
+by transfer (rule refl)
+
+lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
+by transfer (rule refl)
+
+lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
+by transfer (rule refl)
+
+lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
+by transfer (rule refl)
+
+lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
+by transfer (rule refl)
+
+text {* @{term star_of} preserves numerals *}
+
+lemma star_of_zero: "star_of 0 = 0"
+by transfer (rule refl)
+
+lemma star_of_one: "star_of 1 = 1"
+by transfer (rule refl)
+
+lemma star_of_number_of: "star_of (number_of x) = number_of x"
+by transfer (rule refl)
+
+text {* @{term star_of} preserves orderings *}
+
+lemma star_of_less: "(star_of x < star_of y) = (x < y)"
+by transfer (rule refl)
+
+lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
+by transfer (rule refl)
+
+lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
+by transfer (rule refl)
+
+text{*As above, for 0*}
+
+lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
+lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
+lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
+
+lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
+lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
+lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
+
+text{*As above, for 1*}
+
+lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
+lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
+lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
+
+lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
+lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
+lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
+
+text{*As above, for numerals*}
+
+lemmas star_of_number_less =
+  star_of_less [of "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_number_le   =
+  star_of_le   [of "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_number_eq   =
+  star_of_eq   [of "number_of w", standard, simplified star_of_number_of]
+
+lemmas star_of_less_number =
+  star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_le_number   =
+  star_of_le   [of _ "number_of w", standard, simplified star_of_number_of]
+lemmas star_of_eq_number   =
+  star_of_eq   [of _ "number_of w", standard, simplified star_of_number_of]
+
+lemmas star_of_simps [simp] =
+  star_of_add     star_of_diff    star_of_minus
+  star_of_mult    star_of_divide  star_of_inverse
+  star_of_div     star_of_mod
+  star_of_power   star_of_abs
+  star_of_zero    star_of_one     star_of_number_of
+  star_of_less    star_of_le      star_of_eq
+  star_of_0_less  star_of_0_le    star_of_0_eq
+  star_of_less_0  star_of_le_0    star_of_eq_0
+  star_of_1_less  star_of_1_le    star_of_1_eq
+  star_of_less_1  star_of_le_1    star_of_eq_1
+  star_of_number_less star_of_number_le star_of_number_eq
+  star_of_less_number star_of_le_number star_of_eq_number
+
+subsection {* Ordering classes *}
 
 instance star :: (order) order
 apply (intro_classes)
@@ -23,7 +164,7 @@
 by (intro_classes, transfer, rule linorder_linear)
 
 
-subsection "LOrder.thy"
+subsection {* Lattice ordering classes *}
 
 text {*
   Some extra trouble is necessary because the class axioms 
@@ -57,17 +198,17 @@
 
 instance star :: (lorder) lorder ..
 
-lemma star_join_def: "join \<equiv> Ifun2_of join"
+lemma star_join_def [transfer_unfold]: "join \<equiv> Ifun2_of join"
  apply (rule is_join_unique[OF is_join_join, THEN eq_reflection])
  apply (transfer is_join_def, rule is_join_join)
 done
 
-lemma star_meet_def: "meet \<equiv> Ifun2_of meet"
+lemma star_meet_def [transfer_unfold]: "meet \<equiv> Ifun2_of meet"
  apply (rule is_meet_unique[OF is_meet_meet, THEN eq_reflection])
  apply (transfer is_meet_def, rule is_meet_meet)
 done
 
-subsection "OrderedGroup.thy"
+subsection {* Ordered group classes *}
 
 instance star :: (semigroup_add) semigroup_add
 by (intro_classes, transfer, rule add_assoc)
@@ -123,9 +264,7 @@
 instance star :: (lordered_ab_group) lordered_ab_group ..
 
 instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
-apply (intro_classes)
-apply (transfer star_join_def, rule abs_lattice)
-done
+by (intro_classes, transfer, rule abs_lattice)
 
 text "Ring-and-Field.thy"
 
@@ -207,7 +346,7 @@
 instance star :: (ordered_idom) ordered_idom ..
 instance star :: (ordered_field) ordered_field ..
 
-subsection "Power.thy"
+subsection {* Power classes *}
 
 text {*
   Proving the class axiom @{thm [source] power_Suc} for type
@@ -227,11 +366,14 @@
     by transfer (rule power_Suc)
 qed
 
-subsection "Integ/Number.thy"
+subsection {* Number classes *}
 
-lemma star_of_nat_def: "of_nat n \<equiv> star_of (of_nat n)"
+lemma star_of_nat_def [transfer_unfold]: "of_nat n \<equiv> star_of (of_nat n)"
 by (rule eq_reflection, induct_tac n, simp_all)
 
+lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
+by transfer (rule refl)
+
 lemma int_diff_cases:
 assumes prem: "\<And>m n. z = int m - int n \<Longrightarrow> P" shows "P"
  apply (rule_tac z=z in int_cases)
@@ -239,19 +381,13 @@
  apply (rule_tac m=0 and n="Suc n" in prem, simp)
 done -- "Belongs in Integ/IntDef.thy"
 
-lemma star_of_int_def: "of_int z \<equiv> star_of (of_int z)"
- apply (rule eq_reflection)
- apply (rule_tac z=z in int_diff_cases)
- apply (simp add: star_of_nat_def)
-done
+lemma star_of_int_def [transfer_unfold]: "of_int z \<equiv> star_of (of_int z)"
+by (rule eq_reflection, rule_tac z=z in int_diff_cases, simp)
+
+lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
+by transfer (rule refl)
 
 instance star :: (number_ring) number_ring
 by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
 
-lemma star_of_of_nat [simp]: "star_of (of_nat n) = of_nat n"
-by (simp add: star_of_nat_def)
-
-lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
-by (simp add: star_of_int_def)
-
 end
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/StarType.thy
--- a/src/HOL/Hyperreal/StarType.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/StarType.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -166,6 +166,10 @@
   Ipred2_of :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
   "Ipred2_of P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
 
+lemmas Ifun_defs =
+  Ifun_of_def Ifun2_def Ifun2_of_def
+  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
+
 lemma Ifun_of [simp]:
   "Ifun_of f (star_of x) = star_of (f x)"
 by (simp only: Ifun_of_def Ifun)
@@ -182,10 +186,6 @@
   "Ipred2_of P (star_of x) (star_of y) = P x y"
 by (simp only: Ipred2_of_def Ifun unstar)
 
-lemmas Ifun_defs =
-  star_of_def Ifun_of_def Ifun2_def Ifun2_of_def
-  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
-
 
 subsection {* Internal sets *}
 
@@ -201,147 +201,5 @@
 by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 
 
-subsection {* Class constants *}
-
-instance star :: (ord) ord ..
-instance star :: (zero) zero ..
-instance star :: (one) one ..
-instance star :: (plus) plus ..
-instance star :: (times) times ..
-instance star :: (minus) minus ..
-instance star :: (inverse) inverse ..
-instance star :: (number) number ..
-instance star :: ("Divides.div") "Divides.div" ..
-instance star :: (power) power ..
-
-defs (overloaded)
-  star_zero_def:    "0 \<equiv> star_of 0"
-  star_one_def:     "1 \<equiv> star_of 1"
-  star_number_def:  "number_of b \<equiv> star_of (number_of b)"
-  star_add_def:     "(op +) \<equiv> Ifun2_of (op +)"
-  star_diff_def:    "(op -) \<equiv> Ifun2_of (op -)"
-  star_minus_def:   "uminus \<equiv> Ifun_of uminus"
-  star_mult_def:    "(op *) \<equiv> Ifun2_of (op *)"
-  star_divide_def:  "(op /) \<equiv> Ifun2_of (op /)"
-  star_inverse_def: "inverse \<equiv> Ifun_of inverse"
-  star_le_def:      "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
-  star_less_def:    "(op <) \<equiv> Ipred2_of (op <)"
-  star_abs_def:     "abs \<equiv> Ifun_of abs"
-  star_div_def:     "(op div) \<equiv> Ifun2_of (op div)"
-  star_mod_def:     "(op mod) \<equiv> Ifun2_of (op mod)"
-  star_power_def:   "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
-
-lemmas star_class_defs =
-  star_zero_def     star_one_def      star_number_def
-  star_add_def      star_diff_def     star_minus_def
-  star_mult_def     star_divide_def   star_inverse_def
-  star_le_def       star_less_def     star_abs_def
-  star_div_def      star_mod_def      star_power_def
-
-text {* @{term star_of} preserves class operations *}
-
-lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
-by (simp add: star_add_def)
-
-lemma star_of_diff: "star_of (x - y) = star_of x - star_of y"
-by (simp add: star_diff_def)
-
-lemma star_of_minus: "star_of (-x) = - star_of x"
-by (simp add: star_minus_def)
-
-lemma star_of_mult: "star_of (x * y) = star_of x * star_of y"
-by (simp add: star_mult_def)
-
-lemma star_of_divide: "star_of (x / y) = star_of x / star_of y"
-by (simp add: star_divide_def)
-
-lemma star_of_inverse: "star_of (inverse x) = inverse (star_of x)"
-by (simp add: star_inverse_def)
-
-lemma star_of_div: "star_of (x div y) = star_of x div star_of y"
-by (simp add: star_div_def)
-
-lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
-by (simp add: star_mod_def)
-
-lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
-by (simp add: star_power_def)
-
-lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
-by (simp add: star_abs_def)
-
-text {* @{term star_of} preserves numerals *}
-
-lemma star_of_zero: "star_of 0 = 0"
-by (simp add: star_zero_def)
-
-lemma star_of_one: "star_of 1 = 1"
-by (simp add: star_one_def)
-
-lemma star_of_number_of: "star_of (number_of x) = number_of x"
-by (simp add: star_number_def)
-
-text {* @{term star_of} preserves orderings *}
-
-lemma star_of_less: "(star_of x < star_of y) = (x < y)"
-by (simp add: star_less_def)
-
-lemma star_of_le: "(star_of x \<le> star_of y) = (x \<le> y)"
-by (simp add: star_le_def)
-
-lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
-by (rule star_of_inject)
-
-text{*As above, for 0*}
-
-lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
-lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
-lemmas star_of_0_eq   = star_of_eq   [of 0, simplified star_of_zero]
-
-lemmas star_of_less_0 = star_of_less [of _ 0, simplified star_of_zero]
-lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
-lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
-
-text{*As above, for 1*}
-
-lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
-lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
-lemmas star_of_1_eq   = star_of_eq   [of 1, simplified star_of_one]
-
-lemmas star_of_less_1 = star_of_less [of _ 1, simplified star_of_one]
-lemmas star_of_le_1   = star_of_le   [of _ 1, simplified star_of_one]
-lemmas star_of_eq_1   = star_of_eq   [of _ 1, simplified star_of_one]
-
-text{*As above, for numerals*}
-
-lemmas star_of_number_less =
-  star_of_less [of "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_number_le   =
-  star_of_le   [of "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_number_eq   =
-  star_of_eq   [of "number_of b", simplified star_of_number_of, standard]
-
-lemmas star_of_less_number =
-  star_of_less [of _ "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_le_number   =
-  star_of_le   [of _ "number_of b", simplified star_of_number_of, standard]
-lemmas star_of_eq_number   =
-  star_of_eq   [of _ "number_of b", simplified star_of_number_of, standard]
-
-lemmas star_of_simps =
-  star_of_add     star_of_diff    star_of_minus
-  star_of_mult    star_of_divide  star_of_inverse
-  star_of_div     star_of_mod
-  star_of_power   star_of_abs
-  star_of_zero    star_of_one     star_of_number_of
-  star_of_less    star_of_le      star_of_eq
-  star_of_0_less  star_of_0_le    star_of_0_eq
-  star_of_less_0  star_of_le_0    star_of_eq_0
-  star_of_1_less  star_of_1_le    star_of_1_eq
-  star_of_less_1  star_of_le_1    star_of_eq_1
-  star_of_number_less star_of_number_le star_of_number_eq
-  star_of_less_number star_of_le_number star_of_eq_number
-
-declare star_of_simps [simp]
 
 end
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/Transfer.thy
--- a/src/HOL/Hyperreal/Transfer.thy	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/Transfer.thy	Mon Sep 12 23:14:41 2005 +0200
@@ -7,70 +7,9 @@
 
 theory Transfer
 imports StarType
+uses ("transfer.ML")
 begin
 
-subsection {* Preliminaries *}
-
-text {* These transform expressions like @{term "{n. f (P n)} \<in> \<U>"} *}
-
-lemma fuf_ex:
-  "({n. \<exists>x. P n x} \<in> \<U>) = (\<exists>X. {n. P n (X n)} \<in> \<U>)"
-proof
-  assume "{n. \<exists>x. P n x} \<in> \<U>"
-  hence "{n. P n (SOME x. P n x)} \<in> \<U>"
-    by (auto elim: someI filter.subset [OF filter_FUFNat])
-  thus "\<exists>X. {n. P n (X n)} \<in> \<U>" by fast
-next
-  show "\<exists>X. {n. P n (X n)} \<in> \<U> \<Longrightarrow> {n. \<exists>x. P n x} \<in> \<U>"
-    by (auto elim: filter.subset [OF filter_FUFNat])
-qed
-
-lemma fuf_not: "({n. \<not> P n} \<in> \<U>) = ({n. P n} \<notin> \<U>)"
- apply (subst Collect_neg_eq)
- apply (rule ultrafilter.Compl_iff [OF ultrafilter_FUFNat])
-done
-
-lemma fuf_conj:
-  "({n. P n \<and> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<and> {n. Q n} \<in> \<U>)"
- apply (subst Collect_conj_eq)
- apply (rule filter.Int_iff [OF filter_FUFNat])
-done
-
-lemma fuf_disj:
-  "({n. P n \<or> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<or> {n. Q n} \<in> \<U>)"
- apply (subst Collect_disj_eq)
- apply (rule ultrafilter.Un_iff [OF ultrafilter_FUFNat])
-done
-
-lemma fuf_imp:
-  "({n. P n \<longrightarrow> Q n} \<in> \<U>) = ({n. P n} \<in> \<U> \<longrightarrow> {n. Q n} \<in> \<U>)"
-by (simp only: imp_conv_disj fuf_disj fuf_not)
-
-lemma fuf_iff:
-  "({n. P n = Q n} \<in> \<U>) = (({n. P n} \<in> \<U>) = ({n. Q n} \<in> \<U>))"
-by (simp add: iff_conv_conj_imp fuf_conj fuf_imp)
-
-lemma fuf_all:
-  "({n. \<forall>x. P n x} \<in> \<U>) = (\<forall>X. {n. P n (X n)} \<in> \<U>)"
- apply (rule Not_eq_iff [THEN iffD1])
- apply (simp add: fuf_not [symmetric])
- apply (rule fuf_ex)
-done
-
-lemma fuf_if_bool:
-  "({n. if P n then Q n else R n} \<in> \<U>) =
-    (if {n. P n} \<in> \<U> then {n. Q n} \<in> \<U> else {n. R n} \<in> \<U>)"
-by (simp add: if_bool_eq_conj fuf_conj fuf_imp fuf_not)
-
-lemma fuf_eq:
-  "({n. X n = Y n} \<in> \<U>) = (star_n X = star_n Y)"
-by (rule star_n_eq_iff [symmetric])
-
-lemma fuf_if:
-  "star_n (\<lambda>n. if P n then X n else Y n) =
-    (if {n. P n} \<in> \<U> then star_n X else star_n Y)"
-by (auto simp add: star_n_eq_iff fuf_not [symmetric] elim: ultra)
-
 subsection {* Starting the transfer proof *}
 
 text {*
@@ -88,6 +27,12 @@
   "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
 by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
 
+use "transfer.ML"
+setup Transfer.setup
+
+declare Ifun_defs [transfer_unfold]
+declare Iset_of_def [transfer_unfold]
+
 subsection {* Transfer introduction rules *}
 
 text {*
@@ -112,63 +57,57 @@
 
 lemma transfer_not:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
-by (simp only: fuf_not)
+by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
 
 lemma transfer_conj:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
-by (simp only: fuf_conj)
+by (simp only: filter.Collect_conj [OF filter_FUFNat])
 
 lemma transfer_disj:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
-by (simp only: fuf_disj)
+by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
 
 lemma transfer_imp:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
-by (simp only: fuf_imp)
+by (simp only: imp_conv_disj transfer_disj transfer_not)
 
 lemma transfer_iff:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
-by (simp only: fuf_iff)
+by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
 
 lemma transfer_if_bool:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
     \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
-by (simp only: fuf_if_bool)
-
-lemma transfer_all_bool:
-  "\<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>"
-by (simp only: all_bool_eq fuf_conj)
-
-lemma transfer_ex_bool:
-  "\<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>"
-by (simp only: ex_bool_eq fuf_disj)
+by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
 
 subsubsection {* Equals, If *}
 
 lemma transfer_eq:
   "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
-by (simp only: fuf_eq)
+by (simp only: star_n_eq_iff)
 
 lemma transfer_if:
   "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
     \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
-by (simp only: fuf_if)
+apply (rule eq_reflection)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
+done
 
 subsubsection {* Quantifiers *}
 
+lemma transfer_ex:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
+by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat])
+
 lemma transfer_all:
   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
     \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
-by (simp only: all_star_eq fuf_all)
-
-lemma transfer_ex:
-  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
-by (simp only: ex_star_eq fuf_ex)
+by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat])
 
 lemma transfer_ex1:
   "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
@@ -220,20 +159,25 @@
     \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
 by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
 
+
 subsubsection {* Miscellaneous *}
 
 lemma transfer_unstar:
   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
 by (simp only: unstar_star_n)
 
+lemma transfer_star_of: "star_of x \<equiv> star_n (\<lambda>n. x)"
+by (rule star_of_def)
+
 lemma transfer_star_n: "star_n X \<equiv> star_n (\<lambda>n. X n)"
 by (rule reflexive)
 
 lemma transfer_bool: "p \<equiv> {n. p} \<in> \<U>"
 by (simp add: atomize_eq)
 
-lemmas transfer_intros =
+lemmas transfer_intros [transfer_intro] =
   transfer_star_n
+  transfer_star_of
   transfer_Ifun
   transfer_fun_eq
 
@@ -243,8 +187,6 @@
   transfer_imp
   transfer_iff
   transfer_if_bool
-  transfer_all_bool
-  transfer_ex_bool
 
   transfer_all
   transfer_ex
@@ -261,148 +203,6 @@
   transfer_ball
   transfer_bex
 
-subsection {* Transfer tactic *}
-
-text {*
-  We start by giving ML bindings for the theorems that
-  will used by the transfer tactic. Ideally, some of the
-  lists of theorems should be expandable.
-  To @{text star_class_defs} we would like to add theorems
-  about @{term nat_of}, @{term int_of}, @{term meet},
-  @{term join}, etc.
-  Also, we would like to create introduction rules for new
-  constants.
-*}
-
-ML_setup {*
-val atomizers = map thm ["atomize_all", "atomize_imp", "atomize_eq"]
-val Ifun_defs = thms "Ifun_defs" @ [thm "Iset_of_def"]
-val star_class_defs = thms "star_class_defs"
-val transfer_defs = atomizers @ Ifun_defs @ star_class_defs
-
-val transfer_start = thm "transfer_start"
-val transfer_intros = thms "transfer_intros"
-val transfer_Ifun = thm "transfer_Ifun"
-*}
-
-text {*
-  Next we define the ML function @{text unstar_term}.
-  This function takes a term, and gives back an equivalent
-  term that does not contain any references to the @{text star}
-  type constructor. Hopefully the resulting term will still be
-  type-correct: Any constant whose type contains @{text star}
-  should either be polymorphic (so that it will still work at
-  the un-starred instance) or listed in @{text star_consts}
-  (so it can be removed).
-  Maybe @{text star_consts} should be extensible?
-*}
-
-ML_setup {*
-local
-  fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
-    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
-    | unstar_typ T = T
-
-  val star_consts =
-    [ "StarType.star_of", "StarType.Ifun"
-    , "StarType.Ifun_of", "StarType.Ifun2"
-    , "StarType.Ifun2_of", "StarType.Ipred"
-    , "StarType.Ipred_of", "StarType.Ipred2"
-    , "StarType.Ipred2_of", "StarType.Iset"
-    , "StarType.Iset_of", "StarType.unstar" ]
-
-  fun is_star_const a = exists (fn x => x = a) star_consts
-in
-  fun unstar_term (Const(a,T) $ x) = if (is_star_const a)
-                     then (unstar_term x)
-                     else (Const(a,unstar_typ T) $ unstar_term x)
-    | unstar_term (f $ t) = unstar_term f $ unstar_term t
-    | unstar_term (Const(a,T)) = Const(a,unstar_typ T)
-    | unstar_term (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar_term t) 
-    | unstar_term t = t
-end
-*}
-
-text {*
-  The @{text transfer_thm_of} function takes a term that
-  represents a proposition, and proves that it is logically
-  equivalent to the un-starred version. Assuming all goes
-  well, it returns a theorem asserting the equivalence.
-*}
-
-text {*
-  TODO: We need some error messages for when things go
-  wrong. Errors may be caused by constants that don't have
-  matching introduction rules, or quantifiers over wrong types.
-*}
-
-ML_setup {*
-local
-  val tacs =
-    [ match_tac [transitive_thm] 1
-    , resolve_tac [transfer_start] 1
-    , REPEAT_ALL_NEW (resolve_tac transfer_intros) 1
-    , match_tac [reflexive_thm] 1 ]
-in
-  fun transfer_thm_of sg ths t =
-      let val u = unstar_term t
-          val e = Const("==", propT --> propT --> propT)
-          val c = cterm_of sg (e $ t $ u)
-      in prove_goalw_cterm (transfer_defs @ ths) c (fn _ => tacs)
-      end
-end
-*}
-
-text {*
-  Instead of applying the @{thm [source] transfer_start} rule
-  right away, the proof of each transfer theorem starts with the
-  transitivity rule @{text "\<lbrakk>P \<equiv> ?Q; ?Q \<equiv> P'\<rbrakk> \<Longrightarrow> P \<equiv> P'"}, which
-  introduces a new unbound schematic variable @{text ?Q}. The first
-  premise @{text "P \<equiv> ?Q"} is solved by recursively using 
-  @{thm [source] transfer_start} and @{thm [source] transfer_intros}.
-  Each rule application adds constraints to the form of @{text ?Q};
-  by the time the first premise is proved, @{text ?Q} is completely
-  bound to the value of @{term P'}. Finally, the second premise is
-  resolved with the reflexivity rule @{text "P' \<equiv> P'"}.
-*}
-
-text {*
-  The delayed binding is necessary for the correct operation of the
-  introduction rule @{thm [source] transfer_Ifun}:
-  @{thm transfer_Ifun[of f _ x]}. With a subgoal of the form
-  @{term "f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"}, we would like to bind @{text ?F}
-  to @{text F} and @{text ?X} to @{term X}. Unfortunately, higher-order
-  unification finds more than one possible match, and binds @{text ?F}
-  to @{term "\<lambda>x. x"} by default. If the right-hand side of the subgoal
-  contains an unbound schematic variable instead of the explicit
-  application @{term "F n (X n)"}, then we can ensure that there is
-  only one possible way to match the rule.
-*}
-
-ML_setup {*
-fun transfer_tac ths =
-    SUBGOAL (fn (t,i) =>
-        (fn th =>
-            let val tr = transfer_thm_of (sign_of_thm th) ths t
-            in rewrite_goals_tac [tr] th
-            end
-        )
-    )
-*}
-
-text {*
-  Finally we set up the @{text transfer} method. It takes
-  an optional list of definitions as arguments; they are
-  passed along to @{text transfer_thm_of}, which expands
-  the definitions before attempting to prove the transfer
-  theorem.
-*}
-
-method_setup transfer = {*
-  Method.thms_args
-    (fn ths => Method.SIMPLE_METHOD' HEADGOAL (transfer_tac ths))
-*} "transfer principle"
-
 text {* Sample theorems *}
 
 lemma Ifun_inject: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
diff -r 6b8b27894133 -r 4910cf8c0cd2 src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:13:46 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Mon Sep 12 23:14:41 2005 +0200
@@ -127,13 +127,16 @@
 val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
 
 val setup =
-  [ TransferData.init
-  , Attrib.add_attributes
-    [ ("transfer_intro", intro_attr, "transfer introduction rule")
-    , ("transfer_unfold", unfold_attr, "transfer unfolding rule")
-    , ("transfer_refold", refold_attr, "transfer refolding rule")
-    ]
-  , Method.add_method
+  [ TransferData.init,
+    Attrib.add_attributes
+    [ ("transfer_intro", intro_attr,
+       "declaration of transfer introduction rule"),
+      ("transfer_unfold", unfold_attr,
+       "declaration of transfer unfolding rule"),
+      ("transfer_refold", refold_attr,
+       "declaration of transfer refolding rule")
+    ],
+    Method.add_method
     ("transfer", Method.thms_args transfer_method, "transfer principle")
   ];