# HG changeset patch
# User huffman
# Date 1126820782 -7200
# Node ID e8d6ed3aacfeaf84df98883624391942c02c7c9a
# Parent  8a2de150b5f1846ab897792ecf59080f3c6da8b5
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up

diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Complex/NSCA.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -133,12 +133,7 @@
 
 lemma SComplex_hcmod_SReal: 
       "z \<in> SComplex ==> hcmod z \<in> Reals"
-apply (simp add: SComplex_def SReal_def)
-apply (cases z)
-apply (auto simp add: hcmod star_of_def cmod_def star_n_eq_iff)
-apply (rule_tac x = "cmod r" in exI)
-apply (simp add: cmod_def, ultra)
-done
+by (auto simp add: SComplex_def SReal_def hcmod_def)
 
 lemma SComplex_zero [simp]: "0 \<in> SComplex"
 by (simp add: SComplex_def)
@@ -815,15 +810,11 @@
 
 lemma eq_Abs_star_EX:
      "(\<exists>t. P t) = (\<exists>X. P (star_n X))"
-apply auto
-apply (rule_tac x = t in star_cases, auto)
-done
+by (rule ex_star_eq)
 
 lemma eq_Abs_star_Bex:
      "(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))"
-apply auto
-apply (rule_tac x = t in star_cases, auto)
-done
+by (simp add: Bex_def ex_star_eq)
 
 (* Here we go - easy proof now!! *)
 lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t"
@@ -1136,9 +1127,7 @@
 
 lemma SComplex_SReal_hcomplex_of_hypreal:
      "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
-apply (cases x)
-apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff star_n_zero_num [symmetric])
-done
+by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def)
 
 lemma stc_hcomplex_of_hypreal: 
  "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -21,16 +21,16 @@
   (*--- real and Imaginary parts ---*)
 
   hRe :: "hcomplex => hypreal"
-  "hRe(z) == ( *f* Re) z"
+  "hRe == *f* Re"
 
   hIm :: "hcomplex => hypreal"
-  "hIm(z) == ( *f* Im) z"
+  "hIm == *f* Im"
 
 
   (*----------- modulus ------------*)
 
   hcmod :: "hcomplex => hypreal"
-  "hcmod z == ( *f* cmod) z"
+  "hcmod == *f* cmod"
 
   (*------ imaginary unit ----------*)
 
@@ -40,41 +40,39 @@
   (*------- complex conjugate ------*)
 
   hcnj :: "hcomplex => hcomplex"
-  "hcnj z == ( *f* cnj) z"
+  "hcnj == *f* cnj"
 
   (*------------ Argand -------------*)
 
   hsgn :: "hcomplex => hcomplex"
-  "hsgn z == ( *f* sgn) z"
+  "hsgn == *f* sgn"
 
   harg :: "hcomplex => hypreal"
-  "harg z == ( *f* arg) z"
+  "harg == *f* arg"
 
   (* abbreviation for (cos a + i sin a) *)
   hcis :: "hypreal => hcomplex"
-  "hcis a == ( *f* cis) a"
+  "hcis == *f* cis"
 
   (*----- injection from hyperreals -----*)
 
   hcomplex_of_hypreal :: "hypreal => hcomplex"
-  "hcomplex_of_hypreal r == ( *f* complex_of_real) r"
+  "hcomplex_of_hypreal == *f* complex_of_real"
 
   (* abbreviation for r*(cos a + i sin a) *)
   hrcis :: "[hypreal, hypreal] => hcomplex"
-(*  "hrcis r a == hcomplex_of_hypreal r * hcis a" *)
-  "hrcis r a == Ifun2_of rcis r a"
+  "hrcis == *f2* rcis"
 
   (*------------ e ^ (x + iy) ------------*)
 
   hexpi :: "hcomplex => hcomplex"
-(*  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"*)
-  "hexpi z == ( *f* expi) z"
+  "hexpi == *f* expi"
 
   HComplex :: "[hypreal,hypreal] => hcomplex"
-  "HComplex == Ifun2_of Complex"
+  "HComplex == *f2* Complex"
 
   hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80)
-  "(z::hcomplex) hcpow (n::hypnat) == Ifun2_of (op ^) z n"
+  "(z::hcomplex) hcpow (n::hypnat) == ( *f2* op ^) z n"
 
 lemmas hcomplex_defs [transfer_unfold] =
   hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
@@ -436,7 +434,7 @@
 subsection{*A Few Nonlinear Theorems*}
 
 lemma hcpow: "star_n X hcpow star_n Y = star_n (%n. X n ^ Y n)"
-by (simp add: hcpow_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: hcpow_def starfun2_star_n)
 
 lemma hcomplex_of_hypreal_hyperpow:
      "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
@@ -503,7 +501,7 @@
 by (blast intro: ccontr dest: hcpow_not_zero)
 
 lemma star_n_divide: "star_n X / star_n Y = star_n (%n. X n / Y n)"
-by (simp add: star_divide_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: star_divide_def starfun2_star_n)
 
 subsection{*The Function @{term hsgn}*}
 
@@ -633,7 +631,7 @@
 by (transfer, simp add: cis_def)
 
 lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))"
-by (simp add: hrcis_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: hrcis_def starfun2_star_n)
 
 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
 by (transfer, rule rcis_Ex)
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Complex/ex/NSPrimes.thy
--- a/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -96,7 +96,7 @@
 by (simp add: hdvd_def starP2)
 
 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
-by (subst hypnat_of_nat_zero [symmetric], auto)
+by (transfer, simp)
 declare hypnat_of_nat_le_zero_iff [simp]
 
 
@@ -113,7 +113,7 @@
 apply (drule_tac x = whn in spec, auto)
 apply (rule exI, auto)
 apply (drule_tac x = "hypnat_of_nat n" in spec)
-apply (auto simp add: linorder_not_less hypnat_of_nat_zero_iff)
+apply (auto simp add: linorder_not_less star_of_eq_0)
 done
 
 
@@ -211,7 +211,7 @@
 
 lemma range_subset_mem_starsetNat:
    "range f <= A ==> star_n f \<in> *s* A"
-apply (simp add: Iset_of_def star_of_def Iset_star_n)
+apply (simp add: starset_def star_of_def Iset_star_n)
 apply (subgoal_tac "\<forall>n. f n \<in> A", auto)
 done
 
@@ -278,8 +278,6 @@
 lemma hypnat_infinite_has_nonstandard:
      "~ finite A ==> hypnat_of_nat ` A < ( *s* A)"
 apply auto
-apply (rule subsetD)
-apply (rule STAR_star_of_image_subset, auto)
 apply (subgoal_tac "A \<noteq> {}")
 prefer 2 apply force
 apply (drule infinite_set_has_order_preserving_inj)
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -21,16 +21,16 @@
 constdefs
 
     powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
-    "x powhr a == Ifun2_of (op powr) x a"
+    "x powhr a == starfun2 (op powr) x a"
   
     hlog :: "[hypreal,hypreal] => hypreal"
-    "hlog a x == Ifun2_of log a x"
+    "hlog a x == starfun2 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)
+by (simp add: powhr_def starfun2_star_n)
 
 lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
 by (transfer, simp)
@@ -81,7 +81,7 @@
 lemma hlog:
      "hlog (star_n X) (star_n Y) =  
       star_n (%n. log (X n) (Y n))"
-by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: hlog_def starfun2_star_n)
 
 lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
 by (transfer, rule log_ln)
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -14,12 +14,7 @@
 constdefs 
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    "sumhr == 
-      %(M,N,f). Ifun2_of (%m n. setsum f {m..<n}) M N"
-(*
-   "sumhr p == 
-      (%(M,N,f). Abs_star(\<Union>X \<in> Rep_star(M). \<Union>Y \<in> Rep_star(N).  
-                             starrel ``{%n::nat. setsum f {X n..<Y n}})) p"
-*)
+      %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N"
 
   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
    "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
@@ -34,7 +29,7 @@
 lemma sumhr:
      "sumhr(star_n M, star_n N, f) =  
       star_n (%n. setsum f {M n..<N n})"
-by (simp add: sumhr_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: sumhr_def starfun2_star_n)
 
 text{*Base case in definition of @{term sumr}*}
 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -43,7 +43,7 @@
 
 constdefs
   hypreal_of_nat   :: "nat => hypreal"
-   "hypreal_of_nat m  == of_nat m"
+   "hypreal_of_nat m == of_nat m"
 
 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
 by (force simp add: hypreal_of_nat_def Nats_def) 
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -17,14 +17,6 @@
 syntax hypreal_of_real :: "real => real star"
 translations "hypreal_of_real" => "star_of :: real => real star"
 
-typed_print_translation {*
-  let
-    fun hr_tr' _ (Type ("fun", (Type ("real", []) :: _))) [t] =
-          Syntax.const "hypreal_of_real" $ t
-      | hr_tr' _ _ _ = raise Match;
-  in [("star_of", hr_tr')] end
-*}
-
 constdefs
 
   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
@@ -42,34 +34,13 @@
   epsilon :: hypreal   ("\<epsilon>")
 
 
-subsection{*The Set of Naturals is not Finite*}
-
-(*** based on James' proof that the set of naturals is not finite ***)
-lemma finite_exhausts [rule_format]:
-     "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)"
-apply (rule impI)
-apply (erule_tac F = A in finite_induct)
-apply (blast, erule exE)
-apply (rule_tac x = "n + x" in exI)
-apply (rule allI, erule_tac x = "x + m" in allE)
-apply (auto simp add: add_ac)
-done
-
-lemma finite_not_covers [rule_format (no_asm)]:
-     "finite (A :: nat set) --> (\<exists>n. n \<notin>A)"
-by (rule impI, drule finite_exhausts, blast)
-
-lemma not_finite_nat: "~ finite(UNIV:: nat set)"
-by (fast dest!: finite_exhausts)
-
-
 subsection{*Existence of Free Ultrafilter over the Naturals*}
 
 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: 
 an arbitrary free ultrafilter*}
 
 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
-by (rule not_finite_nat [THEN freeultrafilter_Ex])
+by (rule nat_infinite [THEN freeultrafilter_Ex])
 
 lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
 apply (unfold FreeUltrafilterNat_def)
@@ -170,7 +141,7 @@
 text{*Proving that @{term starrel} is an equivalence relation*}
 
 lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
-by (simp add: starrel_def)
+by (rule StarDef.starrel_iff)
 
 lemma starrel_refl: "(x,x) \<in> starrel"
 by (simp add: starrel_def)
@@ -183,7 +154,7 @@
 by (simp add: starrel_def, ultra)
 
 lemma equiv_starrel: "equiv UNIV starrel"
-by (rule StarType.equiv_starrel)
+by (rule StarDef.equiv_starrel)
 
 (* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
 lemmas equiv_starrel_iff =
@@ -194,7 +165,6 @@
 
 declare Abs_star_inject [simp] Abs_star_inverse [simp]
 declare equiv_starrel [THEN eq_equiv_class_iff, simp]
-declare starrel_iff [iff]
 
 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
 
@@ -215,10 +185,6 @@
 lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
 by (rule inj_onI, simp)
 
-lemma eq_Abs_star:
-    "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P"
-by (fold star_n_def, auto intro: star_cases)
-
 lemma Rep_star_star_n_iff [simp]:
   "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
 by (simp add: star_n_def)
@@ -226,57 +192,52 @@
 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
 by simp
 
-subsection{*Hyperreal Addition*}
+subsection{* Properties of @{term star_n} *}
 
 lemma star_n_add:
   "star_n X + star_n Y = star_n (%n. X n + Y n)"
-by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n)
-
-subsection{*Additive inverse on @{typ hypreal}*}
+by (simp only: star_add_def starfun2_star_n)
 
 lemma star_n_minus:
    "- star_n X = star_n (%n. -(X n))"
-by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n)
+by (simp only: star_minus_def starfun_star_n)
 
 lemma star_n_diff:
      "star_n X - star_n Y = star_n (%n. X n - Y n)"
-by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n)
-
-
-subsection{*Hyperreal Multiplication*}
+by (simp only: star_diff_def starfun2_star_n)
 
 lemma star_n_mult:
   "star_n X * star_n Y = star_n (%n. X n * Y n)"
-by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n)
-
-
-subsection{*Multiplicative Inverse on @{typ hypreal} *}
+by (simp only: star_mult_def starfun2_star_n)
 
 lemma star_n_inverse:
-      "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))"
-apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
-apply (rule_tac f=star_n in arg_cong)
-apply (rule ext)
-apply simp
-done
-
-lemma star_n_inverse2:
       "inverse (star_n X) = star_n (%n. inverse(X n))"
-by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
-
-
-subsection{*Properties of The @{text "\<le>"} Relation*}
+by (simp only: star_inverse_def starfun_star_n)
 
 lemma star_n_le:
       "star_n X \<le> star_n Y =  
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
+by (simp only: star_le_def starP2_star_n)
+
+lemma star_n_less:
+      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+by (simp only: star_less_def starP2_star_n)
+
+lemma star_n_zero_num: "0 = star_n (%n. 0)"
+by (simp only: star_zero_def star_of_def)
+
+lemma star_n_one_num: "1 = star_n (%n. 1)"
+by (simp only: star_one_def star_of_def)
+
+lemma star_n_abs:
+     "abs (star_n X) = star_n (%n. abs (X n))"
+by (simp only: star_abs_def starfun_star_n)
+
+subsection{*Misc Others*}
 
 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
 by (auto)
 
-subsection{*The Hyperreals Form an Ordered Field*}
-
 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
 by auto
 
@@ -286,27 +247,8 @@
 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
 by auto
 
-
-subsection{*Misc Others*}
-
-lemma star_n_less:
-      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
-
-lemma star_n_zero_num: "0 = star_n (%n. 0)"
-by (simp add: star_zero_def star_of_def)
-
-lemma star_n_one_num: "1 = star_n (%n. 1)"
-by (simp add: star_one_def star_of_def)
-
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-apply (simp only: omega_def star_zero_def star_less_def star_of_def)
-apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
-done
-
-lemma star_n_abs:
-     "abs (star_n X) = star_n (%n. abs (X n))"
-by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n)
+by (simp add: omega_def star_n_zero_num star_n_less)
 
 subsection{*Existence of Infinite Hyperreal Number*}
 
@@ -357,9 +299,7 @@
          del: star_of_zero)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
-apply (simp add: epsilon_def omega_def star_inverse_def)
-apply (simp add: Ifun_of_def star_of_def Ifun_star_n)
-done
+by (simp add: epsilon_def omega_def star_n_inverse)
 
 
 ML
@@ -367,9 +307,6 @@
 val omega_def = thm "omega_def";
 val epsilon_def = thm "epsilon_def";
 
-val finite_exhausts = thm "finite_exhausts";
-val finite_not_covers = thm "finite_not_covers";
-val not_finite_nat = thm "not_finite_nat";
 val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
 val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
 val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
@@ -394,7 +331,7 @@
 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
 val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-val eq_Abs_star = thm "eq_Abs_star";
+(* val eq_Abs_star = thm "eq_Abs_star"; *)
 val star_n_minus = thm "star_n_minus";
 val star_n_add = thm "star_n_add";
 val star_n_diff = thm "star_n_diff";
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -145,45 +145,15 @@
 
 
 lemma hypnat_of_nat_def: "hypnat_of_nat m == of_nat m"
-by (transfer star_of_nat_def) simp
-
-lemma hypnat_of_nat_add:
-      "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
-by simp
-
-lemma hypnat_of_nat_mult:
-      "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
-by simp
-
-lemma hypnat_of_nat_less_iff:
-      "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
-by simp
-
-lemma hypnat_of_nat_le_iff:
-      "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
-by simp
-
-lemma hypnat_of_nat_eq_iff:
-      "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
-by simp
+by (transfer, simp)
 
 lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
 by simp
 
-lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
-by simp
-
-lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
-by simp
-
 lemma hypnat_of_nat_Suc [simp]:
      "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
 by (simp add: hypnat_of_nat_def)
 
-lemma hypnat_of_nat_minus:
-      "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
-by simp
-
 
 subsection{*Existence of an infinite hypernatural number*}
 
@@ -217,9 +187,7 @@
 
 lemma hypnat_of_nat_eq:
      "hypnat_of_nat m  = star_n (%n::nat. m)"
-apply (induct m) 
-apply (simp_all add: star_n_zero_num star_n_one_num star_n_add)
-done
+by (simp add: star_of_def)
 
 lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
 by (force simp add: hypnat_of_nat_def Nats_def) 
@@ -436,7 +404,6 @@
 
 val starrel_iff = thm "starrel_iff";
 val lemma_starrel_refl = thm "lemma_starrel_refl";
-val eq_Abs_star = thm "eq_Abs_star";
 val hypnat_minus_zero = thm "hypnat_minus_zero";
 val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
 val hypnat_add_is_0 = thm "hypnat_add_is_0";
@@ -461,16 +428,8 @@
 val hypnat_neq0_conv = thm "hypnat_neq0_conv";
 val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
 val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
-val hypnat_of_nat_add = thm "hypnat_of_nat_add";
-val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
-val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
-val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
-val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
-val hypnat_of_nat_eq = thm"hypnat_of_nat_eq"
 val SHNat_eq = thm"SHNat_eq"
 val hypnat_of_nat_one = thm "hypnat_of_nat_one";
-val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
-val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
 val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
 val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
 val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -25,7 +25,7 @@
 
   (* hypernatural powers of hyperreals *)
   hyperpow_def [transfer_unfold]:
-  "(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
+  "(R::hypreal) pow (N::hypnat) == ( *f2* op ^) R N"
 
 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
 by simp
@@ -101,7 +101,7 @@
 subsection{*Powers with Hypernatural Exponents*}
 
 lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
-by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
+by (simp add: hyperpow_def starfun2_star_n)
 
 lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
 by (transfer, simp)
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -1777,7 +1777,7 @@
 lemma FreeUltrafilterNat_Rep_hypreal:
      "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
       ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-by (rule_tac z = x in eq_Abs_star, auto, ultra)
+by (cases x, unfold star_n_def, auto, ultra)
 
 lemma HFinite_FreeUltrafilterNat:
     "x \<in> HFinite 
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -113,11 +113,7 @@
   @{term real_of_nat} *}
 
 lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
-apply (unfold hypreal_of_hypnat_def)
-apply (rule ext)
-apply (rule_tac z = x in eq_Abs_star)
-apply (simp add: hypreal_of_hypnat starfun)
-done
+by (transfer, rule refl)
 
 lemma starfun_inverse_real_of_nat_eq:
      "N \<in> HNatInfinite
@@ -225,24 +221,13 @@
 
 subsection{*Nonstandard Characterization of Induction*}
 
-syntax
-  starP :: "('a => bool) => 'a star => bool" ("*p* _" [80] 80)
-  starP2 :: "('a => 'b => bool) => 'a star => 'b star => bool"
-               ("*p2* _" [80] 80)
-
-translations
-  "starP" == "Ipred_of"
-  "starP2" == "Ipred2_of"
 
 constdefs
   hSuc :: "hypnat => hypnat"
   "hSuc n == n + 1"
 
 lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"
-by (simp add: Ipred_of_def star_of_def Ifun_star_n unstar_star_n)
-
-lemma starP_star_of [simp]: "( *p* P) (star_of n) = P n"
-by (transfer, rule refl)
+by (rule starP_star_n)
 
 lemma hypnat_induct_obj:
     "!!n. (( *p* P) (0::hypnat) &
@@ -259,7 +244,7 @@
 lemma starP2:
 "(( *p2* P) (star_n X) (star_n Y)) =
       ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
-by (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
+by (rule starP2_star_n)
 
 lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
 by (transfer, rule refl)
@@ -267,11 +252,6 @@
 lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
 by (simp add: starP2_eq_iff)
 
-lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_star(starrel `` {x})))"
-apply auto
-apply (rule_tac z = h in eq_Abs_star, auto)
-done
-
 lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
 by (simp add: hSuc_def)
 
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -70,7 +70,7 @@
 lemma SEQ_Infinitesimal:
       "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
-apply (simp add: star_n_inverse2)
+apply (simp add: star_n_inverse)
 apply (rule bexI [OF _ Rep_star_star_n])
 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
 done
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -10,13 +10,6 @@
 imports NSA
 begin
 
-(* nonstandard extension of sets *)
-syntax starset :: "'a set => 'a star set" ("*s* _" [80] 80)
-translations "starset" == "Iset_of"
-
-syntax starfun :: "('a => 'b) => 'a star => 'b star" ("*f* _" [80] 80)
-translations "starfun" == "Ifun_of"
-
 constdefs
     (* internal sets *)
     starset_n :: "(nat => 'a set) => 'a star set"        ("*sn* _" [80] 80)
@@ -54,10 +47,10 @@
 
 subsection{*Properties of the Star-transform Applied to Sets of Reals*}
 
-lemma STAR_UNIV_set [simp]: "*s*(UNIV::'a set) = (UNIV::'a star set)"
+lemma STAR_UNIV_set: "*s*(UNIV::'a set) = (UNIV::'a star set)"
 by (transfer UNIV_def, rule refl)
 
-lemma STAR_empty_set [simp]: "*s* {} = {}"
+lemma STAR_empty_set: "*s* {} = {}"
 by (transfer empty_def, rule refl)
 
 lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
@@ -98,13 +91,10 @@
 
 lemma STAR_real_seq_to_hypreal:
     "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
-apply (unfold Iset_of_def star_of_def)
+apply (unfold starset_def star_of_def)
 apply (simp add: Iset_star_n)
 done
 
-lemma STAR_insert [simp]: "*s* (insert x A) = insert (star_of x) ( *s* A)"
-by (transfer insert_def Un_def, rule refl)
-
 lemma STAR_singleton: "*s* {x} = {star_of x}"
 by simp
 
@@ -119,7 +109,7 @@
 
 lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
 apply (drule expand_fun_eq [THEN iffD2])
-apply (simp add: starset_n_def Iset_of_def star_of_def)
+apply (simp add: starset_n_def starset_def star_of_def)
 done
 
 
@@ -134,7 +124,7 @@
 
 lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
 apply (drule expand_fun_eq [THEN iffD2])
-apply (simp add: starfun_n_def Ifun_of_def star_of_def)
+apply (simp add: starfun_n_def starfun_def star_of_def)
 done
 
 
@@ -148,34 +138,31 @@
 
 lemma hrabs_is_starext_rabs: "is_starext abs abs"
 apply (simp add: is_starext_def, safe)
-apply (rule_tac z = x in eq_Abs_star)
-apply (rule_tac z = y in eq_Abs_star, auto)
+apply (rule_tac x=x in star_cases)
+apply (rule_tac x=y in star_cases)
+apply (unfold star_n_def, auto)
 apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (rule bexI, rule_tac [2] lemma_starrel_refl)
 apply (fold star_n_def)
-apply (unfold star_abs_def Ifun_of_def star_of_def)
+apply (unfold star_abs_def starfun_def star_of_def)
 apply (simp add: Ifun_star_n star_n_eq_iff)
 done
 
 lemma Rep_star_FreeUltrafilterNat:
      "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
       ==> {n. X n = Y n} : FreeUltrafilterNat"
-apply (rule_tac z = z in eq_Abs_star)
-apply (auto, ultra)
-done
+by (rule FreeUltrafilterNat_Rep_hypreal)
 
 text{*Nonstandard extension of functions*}
 
 lemma starfun:
       "( *f* f) (star_n X) = star_n (%n. f (X n))"
-by (simp add: Ifun_of_def star_of_def Ifun_star_n)
+by (simp add: starfun_def star_of_def Ifun_star_n)
 
 lemma starfun_if_eq:
-     "w \<noteq> hypreal_of_real x
+     "!!w. w \<noteq> star_of x
        ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
-apply (cases w)
-apply (simp add: star_of_def starfun star_n_eq_iff, ultra)
-done
+by (transfer, simp)
 
 (*-------------------------------------------
   multiplication: ( *f) x ( *g) = *(f x g)
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -6,7 +6,7 @@
 header {* Class Instances *}
 
 theory StarClasses
-imports Transfer
+imports StarDef
 begin
 
 subsection {* Syntactic classes *}
@@ -26,18 +26,18 @@
   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"
+  star_add_def:     "(op +) \<equiv> *f2* (op +)"
+  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+  star_minus_def:   "uminus \<equiv> *f* uminus"
+  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
+  star_divide_def:  "(op /) \<equiv> *f2* (op /)"
+  star_inverse_def: "inverse \<equiv> *f* inverse"
+  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
+  star_less_def:    "(op <) \<equiv> *p2* (op <)"
+  star_abs_def:     "abs \<equiv> *f* abs"
+  star_div_def:     "(op div) \<equiv> *f2* (op div)"
+  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
+  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
 
 lemmas star_class_defs [transfer_unfold] =
   star_zero_def     star_one_def      star_number_def
@@ -173,12 +173,12 @@
 *}
 
 lemma ex_star_fun:
-  "\<exists>f::('a \<Rightarrow> 'b) star. P (Ifun f)
+  "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
    \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
 by (erule exE, erule exI)
 
 lemma ex_star_fun2:
-  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (Ifun2 f)
+  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
    \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
 by (erule exE, erule exI)
 
@@ -198,13 +198,13 @@
 
 instance star :: (lorder) lorder ..
 
-lemma star_join_def [transfer_unfold]: "join \<equiv> Ifun2_of join"
- apply (rule is_join_unique[OF is_join_join, THEN eq_reflection])
+lemma star_join_def [transfer_unfold]: "join \<equiv> *f2* 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 [transfer_unfold]: "meet \<equiv> Ifun2_of meet"
- apply (rule is_meet_unique[OF is_meet_meet, THEN eq_reflection])
+lemma star_meet_def [transfer_unfold]: "meet \<equiv> *f2* meet"
+ apply (rule is_meet_unique [OF is_meet_meet, THEN eq_reflection])
  apply (transfer is_meet_def, rule is_meet_meet)
 done
 
@@ -266,7 +266,7 @@
 instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
 by (intro_classes, transfer, rule abs_lattice)
 
-text "Ring-and-Field.thy"
+subsection {* Ring and field classes *}
 
 instance star :: (semiring) semiring
 apply (intro_classes)
@@ -390,4 +390,16 @@
 instance star :: (number_ring) number_ring
 by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
 
+subsection {* Finite class *}
+
+lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
+by (erule finite_induct, simp_all)
+
+instance star :: (finite) finite
+apply (intro_classes)
+apply (subst starset_UNIV [symmetric])
+apply (subst starset_finite [OF finite])
+apply (rule finite_imageI [OF finite])
+done
+
 end
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/StarDef.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/StarDef.thy	Thu Sep 15 23:46:22 2005 +0200
@@ -0,0 +1,373 @@
+(*  Title       : HOL/Hyperreal/StarDef.thy
+    ID          : $Id$
+    Author      : Jacques D. Fleuriot and Brian Huffman
+*)
+
+header {* Construction of Star Types Using Ultrafilters *}
+
+theory StarDef
+imports Filter
+uses ("transfer.ML")
+begin
+
+subsection {* A Free Ultrafilter over the Naturals *}
+
+constdefs
+  FreeUltrafilterNat :: "nat set set"  ("\<U>")
+    "\<U> \<equiv> SOME U. freeultrafilter U"
+
+lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
+ apply (unfold FreeUltrafilterNat_def)
+ apply (rule someI_ex)
+ apply (rule freeultrafilter_Ex)
+ apply (rule nat_infinite)
+done
+
+lemmas ultrafilter_FUFNat =
+  freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter]
+
+lemmas filter_FUFNat =
+  freeultrafilter_FUFNat [THEN freeultrafilter.filter]
+
+lemmas FUFNat_empty [iff] =
+  filter_FUFNat [THEN filter.empty]
+
+lemmas FUFNat_UNIV [iff] =
+  filter_FUFNat [THEN filter.UNIV]
+
+text {* This rule takes the place of the old ultra tactic *}
+
+lemma ultra:
+  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
+by (simp add: Collect_imp_eq
+    ultrafilter_FUFNat [THEN ultrafilter.Un_iff]
+    ultrafilter_FUFNat [THEN ultrafilter.Compl_iff])
+
+
+subsection {* Definition of @{text star} type constructor *}
+
+constdefs
+  starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
+    "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
+
+typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
+by (auto intro: quotientI)
+
+constdefs
+  star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
+  "star_n X \<equiv> Abs_star (starrel `` {X})"
+
+theorem star_cases [case_names star_n, cases type: star]:
+  "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
+by (cases x, unfold star_n_def star_def, erule quotientE, fast)
+
+lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
+by (auto, rule_tac x=x in star_cases, simp)
+
+lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
+by (auto, rule_tac x=x in star_cases, auto)
+
+text {* Proving that @{term starrel} is an equivalence relation *}
+
+lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
+by (simp add: starrel_def)
+
+lemma equiv_starrel: "equiv UNIV starrel"
+proof (rule equiv.intro)
+  show "reflexive starrel" by (simp add: refl_def)
+  show "sym starrel" by (simp add: sym_def eq_commute)
+  show "trans starrel" by (auto intro: transI elim!: ultra)
+qed
+
+lemmas equiv_starrel_iff =
+  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
+
+lemma starrel_in_star: "starrel``{x} \<in> star"
+by (simp add: star_def quotientI)
+
+lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
+by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
+
+
+subsection {* Transfer principle *}
+
+text {* This introduction rule starts each transfer proof. *}
+lemma transfer_start:
+  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
+
+text {*Initialize transfer tactic.*}
+use "transfer.ML"
+setup Transfer.setup
+
+text {* Transfer introduction rules. *}
+
+lemma transfer_ex [transfer_intro]:
+  "\<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 [transfer_intro]:
+  "\<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 ultrafilter.Collect_all [OF ultrafilter_FUFNat])
+
+lemma transfer_not [transfer_intro]:
+  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
+by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
+
+lemma transfer_conj [transfer_intro]:
+  "\<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: filter.Collect_conj [OF filter_FUFNat])
+
+lemma transfer_disj [transfer_intro]:
+  "\<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: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
+
+lemma transfer_imp [transfer_intro]:
+  "\<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: imp_conv_disj transfer_disj transfer_not)
+
+lemma transfer_iff [transfer_intro]:
+  "\<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: iff_conv_conj_imp transfer_conj transfer_imp)
+
+lemma transfer_if_bool [transfer_intro]:
+  "\<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: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
+
+lemma transfer_eq [transfer_intro]:
+  "\<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: star_n_eq_iff)
+
+lemma transfer_if [transfer_intro]:
+  "\<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)"
+apply (rule eq_reflection)
+apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
+done
+
+lemma transfer_fun_eq [transfer_intro]:
+  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
+    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
+      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
+by (simp only: expand_fun_eq transfer_all)
+
+lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
+by (rule reflexive)
+
+lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
+by (simp add: atomize_eq)
+
+
+subsection {* Standard elements *}
+
+constdefs
+  star_of :: "'a \<Rightarrow> 'a star"
+  "star_of x \<equiv> star_n (\<lambda>n. x)"
+
+text {* Transfer tactic should remove occurrences of @{term star_of} *}
+setup {* [Transfer.add_const "StarDef.star_of"] *}
+declare star_of_def [transfer_intro]
+
+lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
+by (transfer, rule refl)
+
+
+subsection {* Internal functions *}
+
+constdefs
+  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
+  "Ifun f \<equiv> \<lambda>x. Abs_star
+       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
+
+lemma Ifun_congruent2:
+  "(\<lambda>F X. starrel``{\<lambda>n. F n (X n)}) respects2 starrel"
+by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
+
+lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
+by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
+    UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
+
+text {* Transfer tactic should remove occurrences of @{term Ifun} *}
+setup {* [Transfer.add_const "StarDef.Ifun"] *}
+
+lemma transfer_Ifun [transfer_intro]:
+  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
+by (simp only: Ifun_star_n)
+
+lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
+by (transfer, rule refl)
+
+text {* Nonstandard extensions of functions *}
+
+constdefs
+  starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
+    ("*f* _" [80] 80)
+  "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
+
+  starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
+    ("*f2* _" [80] 80)
+  "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
+
+declare starfun_def [transfer_unfold]
+declare starfun2_def [transfer_unfold]
+
+lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))"
+by (simp only: starfun_def star_of_def Ifun_star_n)
+
+lemma starfun2_star_n:
+  "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))"
+by (simp only: starfun2_def star_of_def Ifun_star_n)
+
+lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)"
+by (transfer, rule refl)
+
+lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
+by (transfer, rule refl)
+
+
+subsection {* Internal predicates *}
+
+constdefs
+  unstar :: "bool star \<Rightarrow> bool"
+  "unstar b \<equiv> b = star_of True"
+
+lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
+by (simp add: unstar_def star_of_def star_n_eq_iff)
+
+lemma unstar_star_of [simp]: "unstar (star_of p) = p"
+by (simp add: unstar_def star_of_inject)
+
+text {* Transfer tactic should remove occurrences of @{term unstar} *}
+setup {* [Transfer.add_const "StarDef.unstar"] *}
+
+lemma transfer_unstar [transfer_intro]:
+  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
+by (simp only: unstar_star_n)
+
+constdefs
+  starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
+    ("*p* _" [80] 80)
+  "*p* P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
+
+  starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
+    ("*p2* _" [80] 80)
+  "*p2* P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
+
+declare starP_def [transfer_unfold]
+declare starP2_def [transfer_unfold]
+
+lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
+by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
+
+lemma starP2_star_n:
+  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
+by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
+
+lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
+by (transfer, rule refl)
+
+lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x"
+by (transfer, rule refl)
+
+
+subsection {* Internal sets *}
+
+constdefs
+  Iset :: "'a set star \<Rightarrow> 'a star set"
+  "Iset A \<equiv> {x. ( *p2* op \<in>) x A}"
+
+lemma Iset_star_n:
+  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
+by (simp add: Iset_def starP2_star_n)
+
+text {* Transfer tactic should remove occurrences of @{term Iset} *}
+setup {* [Transfer.add_const "StarDef.Iset"] *}
+
+lemma transfer_mem [transfer_intro]:
+  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
+    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
+by (simp only: Iset_star_n)
+
+lemma transfer_Collect [transfer_intro]:
+  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
+by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
+
+lemma transfer_set_eq [transfer_intro]:
+  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
+    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
+by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
+
+lemma transfer_ball [transfer_intro]:
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
+by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
+
+lemma transfer_bex [transfer_intro]:
+  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
+    \<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)
+
+lemma transfer_Iset [transfer_intro]:
+  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
+by simp
+
+text {* Nonstandard extensions of sets. *}
+constdefs
+  starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80)
+  "starset A \<equiv> Iset (star_of A)"
+
+declare starset_def [transfer_unfold]
+
+lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)"
+by (transfer, rule refl)
+
+lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)"
+by (transfer UNIV_def, rule refl)
+
+lemma starset_empty: "*s* {} = {}"
+by (transfer empty_def, rule refl)
+
+lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)"
+by (transfer insert_def Un_def, rule refl)
+
+lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B"
+by (transfer Un_def, rule refl)
+
+lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B"
+by (transfer Int_def, rule refl)
+
+lemma starset_Compl: "*s* -A = -( *s* A)"
+by (transfer Compl_def, rule refl)
+
+lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
+by (transfer set_diff_def, rule refl)
+
+lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
+by (transfer image_def, rule refl)
+
+lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)"
+by (transfer vimage_def, rule refl)
+
+lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
+by (transfer subset_def, rule refl)
+
+lemma starset_eq: "( *s* A = *s* B) = (A = B)"
+by (transfer, rule refl)
+
+lemmas starset_simps [simp] =
+  starset_mem     starset_UNIV
+  starset_empty   starset_insert
+  starset_Un      starset_Int
+  starset_Compl   starset_diff
+  starset_image   starset_vimage
+  starset_subset  starset_eq
+
+end
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/StarType.thy
--- a/src/HOL/Hyperreal/StarType.thy	Thu Sep 15 23:16:04 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,205 +0,0 @@
-(*  Title       : HOL/Hyperreal/StarType.thy
-    ID          : $Id$
-    Author      : Jacques D. Fleuriot and Brian Huffman
-*)
-
-header {* Construction of Star Types Using Ultrafilters *}
-
-theory StarType
-imports Filter
-begin
-
-subsection {* A Free Ultrafilter over the Naturals *}
-
-constdefs
-  FreeUltrafilterNat :: "nat set set"  ("\<U>")
-    "\<U> \<equiv> SOME U. freeultrafilter U"
-
-lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
- apply (unfold FreeUltrafilterNat_def)
- apply (rule someI_ex)
- apply (rule freeultrafilter_Ex)
- apply (rule nat_infinite)
-done
-
-lemmas ultrafilter_FUFNat =
-  freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter]
-
-lemmas filter_FUFNat =
-  freeultrafilter_FUFNat [THEN freeultrafilter.filter]
-
-lemmas FUFNat_empty [iff] =
-  filter_FUFNat [THEN filter.empty]
-
-lemmas FUFNat_UNIV [iff] =
-  filter_FUFNat [THEN filter.UNIV]
-
-text {* This rule takes the place of the old ultra tactic *}
-
-lemma ultra:
-  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
-by (simp add: Collect_imp_eq
-    ultrafilter_FUFNat [THEN ultrafilter.Un_iff]
-    ultrafilter_FUFNat [THEN ultrafilter.Compl_iff])
-
-
-subsection {* Definition of @{text star} type constructor *}
-
-constdefs
-  starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
-    "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
-
-typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
-by (auto intro: quotientI)
-
-text {* Proving that @{term starrel} is an equivalence relation *}
-
-lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
-by (simp add: starrel_def)
-
-lemma equiv_starrel: "equiv UNIV starrel"
-proof (rule equiv.intro)
-  show "reflexive starrel" by (simp add: refl_def)
-  show "sym starrel" by (simp add: sym_def eq_commute)
-  show "trans starrel" by (auto intro: transI elim!: ultra)
-qed
-
-lemmas equiv_starrel_iff =
-  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
-  -- {* @{term "(starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel)"} *}
-
-lemma starrel_in_star: "starrel``{x} \<in> star"
-by (simp add: star_def starrel_def quotient_def, fast)
-
-lemma eq_Abs_star:
-  "(\<And>x. z = Abs_star (starrel``{x}) \<Longrightarrow> P) \<Longrightarrow> P"
- apply (rule_tac x=z in Abs_star_cases)
- apply (unfold star_def)
- apply (erule quotientE)
- apply simp
-done
-
-
-subsection {* Constructors for type @{typ "'a star"} *}
-
-constdefs
-  star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
-  "star_n X \<equiv> Abs_star (starrel `` {X})"
-
-  star_of :: "'a \<Rightarrow> 'a star"
-  "star_of x \<equiv> star_n (\<lambda>n. x)"
-
-theorem star_cases [case_names star_n, cases type: star]:
-  "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
-by (unfold star_n_def, rule eq_Abs_star[of x], blast)
-
-lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
-by (auto, rule_tac x=x in star_cases, simp)
-
-lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
-by (auto, rule_tac x=x in star_cases, auto)
-
-lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
- apply (unfold star_n_def)
- apply (simp add: Abs_star_inject starrel_in_star equiv_starrel_iff)
-done
-
-lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
-by (simp add: star_of_def star_n_eq_iff)
-
-
-subsection {* Internal functions *}
-
-constdefs
-  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
-  "Ifun f \<equiv> \<lambda>x. Abs_star
-       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
-
-lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
- apply (unfold Ifun_def star_n_def)
- apply (simp add: Abs_star_inverse starrel_in_star)
- apply (rule_tac f=Abs_star in arg_cong)
- apply safe
-  apply (erule ultra)+
-  apply simp
- apply force
-done
-
-lemma Ifun [simp]: "star_of f \<star> star_of x = star_of (f x)"
-by (simp only: star_of_def Ifun_star_n)
-
-
-subsection {* Testing lifted booleans *}
-
-constdefs
-  unstar :: "bool star \<Rightarrow> bool"
-  "unstar b \<equiv> b = star_of True"
-
-lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
-by (simp add: unstar_def star_of_def star_n_eq_iff)
-
-lemma unstar [simp]: "unstar (star_of p) = p"
-by (simp add: unstar_def star_of_inject)
-
-
-subsection {* Internal functions and predicates *}
-
-constdefs
-  Ifun_of :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
-  "Ifun_of f \<equiv> Ifun (star_of f)"
-
-  Ifun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
-  "Ifun2 f \<equiv> \<lambda>x y. f \<star> x \<star> y"
-
-  Ifun2_of :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
-  "Ifun2_of f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
-
-  Ipred :: "('a \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> bool)"
-  "Ipred P \<equiv> \<lambda>x. unstar (P \<star> x)"
-
-  Ipred_of :: "('a \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> bool)"
-  "Ipred_of P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
-
-  Ipred2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
-  "Ipred2 P \<equiv> \<lambda>x y. unstar (P \<star> x \<star> y)"
-
-  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)
-
-lemma Ifun2_of [simp]:
-  "Ifun2_of f (star_of x) (star_of y) = star_of (f x y)"
-by (simp only: Ifun2_of_def Ifun)
-
-lemma Ipred_of [simp]:
-  "Ipred_of P (star_of x) = P x"
-by (simp only: Ipred_of_def Ifun unstar)
-
-lemma Ipred2_of [simp]:
-  "Ipred2_of P (star_of x) (star_of y) = P x y"
-by (simp only: Ipred2_of_def Ifun unstar)
-
-
-subsection {* Internal sets *}
-
-constdefs
-  Iset :: "'a set star \<Rightarrow> 'a star set"
-  "Iset A \<equiv> {x. Ipred2_of (op \<in>) x A}"
-
-  Iset_of :: "'a set \<Rightarrow> 'a star set"
-  "Iset_of A \<equiv> Iset (star_of A)"
-
-lemma Iset_star_n:
-  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
-by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
-
-
-
-end
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/Transfer.thy
--- a/src/HOL/Hyperreal/Transfer.thy	Thu Sep 15 23:16:04 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,217 +0,0 @@
-(*  Title       : HOL/Hyperreal/Transfer.thy
-    ID          : $Id$
-    Author      : Brian Huffman
-*)
-
-header {* Transfer Principle *}
-
-theory Transfer
-imports StarType
-uses ("transfer.ML")
-begin
-
-subsection {* Starting the transfer proof *}
-
-text {*
-  A transfer theorem asserts an equivalence @{prop "P \<equiv> P'"}
-  between two related propositions. Proposition @{term P} may
-  refer to constants having star types, like @{typ "'a star"}.
-  Proposition @{term P'} is syntactically similar, but only
-  refers to ordinary types (i.e. @{term P'} is the un-starred
-  version of @{term P}).
-*}
-
-text {* This introduction rule starts each transfer proof. *}
-
-lemma transfer_start:
-  "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 {*
-  The proof of a transfer theorem is completely syntax-directed.
-  At each step in the proof, the top-level connective determines
-  which introduction rule to apply. Each argument to the top-level
-  connective generates a new subgoal.
-*}
-
-text {*
-  Subgoals in a transfer proof always have the form of an equivalence.
-  The left side can be any term, and may contain references to star
-  types. The form of the right side depends on its type. At type
-  @{typ bool} it takes the form @{term "{n. P n} \<in> \<U>"}. At type
-  @{typ "'a star"} it takes the form @{term "star_n (\<lambda>n. X n)"}. At type
-  @{typ "'a star set"} it looks like @{term "Iset (star_n (\<lambda>n. A n))"}.
-  And at type @{typ "'a star \<Rightarrow> 'b star"} it has the form
-  @{term "Ifun (star_n (\<lambda>n. F n))"}.
-*}
-
-subsubsection {* Boolean operators *}
-
-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: 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: 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: 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: 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: 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: 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: 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)"
-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 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>
-    \<Longrightarrow> \<exists>!x. p x \<equiv> {n. \<exists>!x. P n x} \<in> \<U>"
-by (simp only: Ex1_def transfer_ex transfer_conj
-   transfer_all transfer_imp transfer_eq)
-
-subsubsection {* Functions *}
-
-lemma transfer_Ifun:
-  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk>
-    \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
-by (simp only: Ifun_star_n)
-
-lemma transfer_fun_eq:
-  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
-    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
-      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
-by (simp only: expand_fun_eq transfer_all)
-
-subsubsection {* Sets *}
-
-lemma transfer_Iset:
-  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
-by simp
-
-lemma transfer_Collect:
-  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
-by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
-
-lemma transfer_mem:
-  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
-    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
-by (simp only: Iset_star_n)
-
-lemma transfer_set_eq:
-  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
-    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
-by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
-
-lemma transfer_ball:
-  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
-by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
-
-lemma transfer_bex:
-  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
-    \<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 [transfer_intro] =
-  transfer_star_n
-  transfer_star_of
-  transfer_Ifun
-  transfer_fun_eq
-
-  transfer_not
-  transfer_conj
-  transfer_disj
-  transfer_imp
-  transfer_iff
-  transfer_if_bool
-
-  transfer_all
-  transfer_ex
-
-  transfer_unstar
-  transfer_bool
-  transfer_eq
-  transfer_if
-
-  transfer_set_eq
-  transfer_Iset
-  transfer_Collect
-  transfer_mem
-  transfer_ball
-  transfer_bex
-
-text {* Sample theorems *}
-
-lemma Ifun_inject: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
-by transfer (rule refl)
-
-lemma unstar_inject: "\<And>x y. (unstar x = unstar y) = (x = y)"
-by transfer (rule refl)
-
-lemma Iset_inject: "\<And>A B. (Iset A = Iset B) = (A = B)"
-by transfer (rule refl)
-
-end
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/fuf.ML
--- a/src/HOL/Hyperreal/fuf.ML	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/fuf.ML	Thu Sep 15 23:46:22 2005 +0200
@@ -22,10 +22,10 @@
 |   get_fuf_hyps (x::xs) zs =
         case (concl_of x) of
         (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
-             Const ("StarType.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
+             Const ("StarDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
                                               ((x RS FreeUltrafilterNat_Compl_mem)::zs)
        |(_ $ (Const ("op :",_) $ _ $
-             Const ("StarType.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
+             Const ("StarDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
        | _ => get_fuf_hyps xs zs;
 
 fun inter_prems [] = raise FUFempty
diff -r 8a2de150b5f1 -r e8d6ed3aacfe src/HOL/Hyperreal/transfer.ML
--- a/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:16:04 2005 +0200
+++ b/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:46:22 2005 +0200
@@ -8,17 +8,13 @@
 signature TRANSFER_TAC =
 sig
   val transfer_tac: thm list -> int -> tactic
+  val add_const: string -> theory -> theory
   val setup: (theory -> theory) list
 end;
 
 structure Transfer: TRANSFER_TAC =
 struct
 
-(* TODO: make this list extensible *)
-val star_consts =
-  [ "StarType.star_of", "StarType.Ifun"
-  , "StarType.unstar", "StarType.Iset" ]
-
 structure TransferData = TheoryDataFun
 (struct
   val name = "HOL/transfer";
@@ -28,7 +24,7 @@
     refolds: thm list,
     consts: string list
   };
-  val empty = {intros = [], unfolds = [], refolds = [], consts = star_consts};
+  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
   val copy = I;
   val extend = I;
   fun merge _
@@ -45,7 +41,7 @@
 
 val transfer_start = thm "transfer_start"
 
-fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
+fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
   | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
   | unstar_typ T = T
 
@@ -102,10 +98,6 @@
 fun map_refolds f = TransferData.map
   (fn {intros,unfolds,refolds,consts} =>
     {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
-
-fun map_consts f = TransferData.map
-  (fn {intros,unfolds,refolds,consts} =>
-    {intros=intros, unfolds=unfolds, refolds=refolds, consts=f consts})
 in
 fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm);
 fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm);
@@ -117,6 +109,10 @@
 fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm);
 end
 
+fun add_const c = TransferData.map
+  (fn {intros,unfolds,refolds,consts} =>
+    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})
+
 local
   val undef_local =
     Attrib.add_del_args