merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
authorhuffman
Thu Sep 15 23:46:22 2005 +0200 (2005-09-15 ago)
changeset 17429e8d6ed3aacfe
parent 17428 8a2de150b5f1
child 17430 72325ec8fd8e
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/ex/NSPrimes.thy
src/HOL/Hyperreal/HLog.thy
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/HyperArith.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Star.thy
src/HOL/Hyperreal/StarClasses.thy
src/HOL/Hyperreal/StarDef.thy
src/HOL/Hyperreal/StarType.thy
src/HOL/Hyperreal/Transfer.thy
src/HOL/Hyperreal/fuf.ML
src/HOL/Hyperreal/transfer.ML
     1.1 --- a/src/HOL/Complex/NSCA.thy	Thu Sep 15 23:16:04 2005 +0200
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Sep 15 23:46:22 2005 +0200
     1.3 @@ -133,12 +133,7 @@
     1.4  
     1.5  lemma SComplex_hcmod_SReal: 
     1.6        "z \<in> SComplex ==> hcmod z \<in> Reals"
     1.7 -apply (simp add: SComplex_def SReal_def)
     1.8 -apply (cases z)
     1.9 -apply (auto simp add: hcmod star_of_def cmod_def star_n_eq_iff)
    1.10 -apply (rule_tac x = "cmod r" in exI)
    1.11 -apply (simp add: cmod_def, ultra)
    1.12 -done
    1.13 +by (auto simp add: SComplex_def SReal_def hcmod_def)
    1.14  
    1.15  lemma SComplex_zero [simp]: "0 \<in> SComplex"
    1.16  by (simp add: SComplex_def)
    1.17 @@ -815,15 +810,11 @@
    1.18  
    1.19  lemma eq_Abs_star_EX:
    1.20       "(\<exists>t. P t) = (\<exists>X. P (star_n X))"
    1.21 -apply auto
    1.22 -apply (rule_tac x = t in star_cases, auto)
    1.23 -done
    1.24 +by (rule ex_star_eq)
    1.25  
    1.26  lemma eq_Abs_star_Bex:
    1.27       "(\<exists>t \<in> A. P t) = (\<exists>X. star_n X \<in> A & P (star_n X))"
    1.28 -apply auto
    1.29 -apply (rule_tac x = t in star_cases, auto)
    1.30 -done
    1.31 +by (simp add: Bex_def ex_star_eq)
    1.32  
    1.33  (* Here we go - easy proof now!! *)
    1.34  lemma stc_part_Ex: "x:CFinite ==> \<exists>t \<in> SComplex. x @c= t"
    1.35 @@ -1136,9 +1127,7 @@
    1.36  
    1.37  lemma SComplex_SReal_hcomplex_of_hypreal:
    1.38       "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
    1.39 -apply (cases x)
    1.40 -apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff star_n_zero_num [symmetric])
    1.41 -done
    1.42 +by (auto simp add: SReal_def SComplex_def hcomplex_of_hypreal_def)
    1.43  
    1.44  lemma stc_hcomplex_of_hypreal: 
    1.45   "z \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Sep 15 23:16:04 2005 +0200
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Sep 15 23:46:22 2005 +0200
     2.3 @@ -21,16 +21,16 @@
     2.4    (*--- real and Imaginary parts ---*)
     2.5  
     2.6    hRe :: "hcomplex => hypreal"
     2.7 -  "hRe(z) == ( *f* Re) z"
     2.8 +  "hRe == *f* Re"
     2.9  
    2.10    hIm :: "hcomplex => hypreal"
    2.11 -  "hIm(z) == ( *f* Im) z"
    2.12 +  "hIm == *f* Im"
    2.13  
    2.14  
    2.15    (*----------- modulus ------------*)
    2.16  
    2.17    hcmod :: "hcomplex => hypreal"
    2.18 -  "hcmod z == ( *f* cmod) z"
    2.19 +  "hcmod == *f* cmod"
    2.20  
    2.21    (*------ imaginary unit ----------*)
    2.22  
    2.23 @@ -40,41 +40,39 @@
    2.24    (*------- complex conjugate ------*)
    2.25  
    2.26    hcnj :: "hcomplex => hcomplex"
    2.27 -  "hcnj z == ( *f* cnj) z"
    2.28 +  "hcnj == *f* cnj"
    2.29  
    2.30    (*------------ Argand -------------*)
    2.31  
    2.32    hsgn :: "hcomplex => hcomplex"
    2.33 -  "hsgn z == ( *f* sgn) z"
    2.34 +  "hsgn == *f* sgn"
    2.35  
    2.36    harg :: "hcomplex => hypreal"
    2.37 -  "harg z == ( *f* arg) z"
    2.38 +  "harg == *f* arg"
    2.39  
    2.40    (* abbreviation for (cos a + i sin a) *)
    2.41    hcis :: "hypreal => hcomplex"
    2.42 -  "hcis a == ( *f* cis) a"
    2.43 +  "hcis == *f* cis"
    2.44  
    2.45    (*----- injection from hyperreals -----*)
    2.46  
    2.47    hcomplex_of_hypreal :: "hypreal => hcomplex"
    2.48 -  "hcomplex_of_hypreal r == ( *f* complex_of_real) r"
    2.49 +  "hcomplex_of_hypreal == *f* complex_of_real"
    2.50  
    2.51    (* abbreviation for r*(cos a + i sin a) *)
    2.52    hrcis :: "[hypreal, hypreal] => hcomplex"
    2.53 -(*  "hrcis r a == hcomplex_of_hypreal r * hcis a" *)
    2.54 -  "hrcis r a == Ifun2_of rcis r a"
    2.55 +  "hrcis == *f2* rcis"
    2.56  
    2.57    (*------------ e ^ (x + iy) ------------*)
    2.58  
    2.59    hexpi :: "hcomplex => hcomplex"
    2.60 -(*  "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)"*)
    2.61 -  "hexpi z == ( *f* expi) z"
    2.62 +  "hexpi == *f* expi"
    2.63  
    2.64    HComplex :: "[hypreal,hypreal] => hcomplex"
    2.65 -  "HComplex == Ifun2_of Complex"
    2.66 +  "HComplex == *f2* Complex"
    2.67  
    2.68    hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80)
    2.69 -  "(z::hcomplex) hcpow (n::hypnat) == Ifun2_of (op ^) z n"
    2.70 +  "(z::hcomplex) hcpow (n::hypnat) == ( *f2* op ^) z n"
    2.71  
    2.72  lemmas hcomplex_defs [transfer_unfold] =
    2.73    hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
    2.74 @@ -436,7 +434,7 @@
    2.75  subsection{*A Few Nonlinear Theorems*}
    2.76  
    2.77  lemma hcpow: "star_n X hcpow star_n Y = star_n (%n. X n ^ Y n)"
    2.78 -by (simp add: hcpow_def Ifun2_of_def star_of_def Ifun_star_n)
    2.79 +by (simp add: hcpow_def starfun2_star_n)
    2.80  
    2.81  lemma hcomplex_of_hypreal_hyperpow:
    2.82       "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
    2.83 @@ -503,7 +501,7 @@
    2.84  by (blast intro: ccontr dest: hcpow_not_zero)
    2.85  
    2.86  lemma star_n_divide: "star_n X / star_n Y = star_n (%n. X n / Y n)"
    2.87 -by (simp add: star_divide_def Ifun2_of_def star_of_def Ifun_star_n)
    2.88 +by (simp add: star_divide_def starfun2_star_n)
    2.89  
    2.90  subsection{*The Function @{term hsgn}*}
    2.91  
    2.92 @@ -633,7 +631,7 @@
    2.93  by (transfer, simp add: cis_def)
    2.94  
    2.95  lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))"
    2.96 -by (simp add: hrcis_def Ifun2_of_def star_of_def Ifun_star_n)
    2.97 +by (simp add: hrcis_def starfun2_star_n)
    2.98  
    2.99  lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
   2.100  by (transfer, rule rcis_Ex)
     3.1 --- a/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 15 23:16:04 2005 +0200
     3.2 +++ b/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 15 23:46:22 2005 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4  by (simp add: hdvd_def starP2)
     3.5  
     3.6  lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
     3.7 -by (subst hypnat_of_nat_zero [symmetric], auto)
     3.8 +by (transfer, simp)
     3.9  declare hypnat_of_nat_le_zero_iff [simp]
    3.10  
    3.11  
    3.12 @@ -113,7 +113,7 @@
    3.13  apply (drule_tac x = whn in spec, auto)
    3.14  apply (rule exI, auto)
    3.15  apply (drule_tac x = "hypnat_of_nat n" in spec)
    3.16 -apply (auto simp add: linorder_not_less hypnat_of_nat_zero_iff)
    3.17 +apply (auto simp add: linorder_not_less star_of_eq_0)
    3.18  done
    3.19  
    3.20  
    3.21 @@ -211,7 +211,7 @@
    3.22  
    3.23  lemma range_subset_mem_starsetNat:
    3.24     "range f <= A ==> star_n f \<in> *s* A"
    3.25 -apply (simp add: Iset_of_def star_of_def Iset_star_n)
    3.26 +apply (simp add: starset_def star_of_def Iset_star_n)
    3.27  apply (subgoal_tac "\<forall>n. f n \<in> A", auto)
    3.28  done
    3.29  
    3.30 @@ -278,8 +278,6 @@
    3.31  lemma hypnat_infinite_has_nonstandard:
    3.32       "~ finite A ==> hypnat_of_nat ` A < ( *s* A)"
    3.33  apply auto
    3.34 -apply (rule subsetD)
    3.35 -apply (rule STAR_star_of_image_subset, auto)
    3.36  apply (subgoal_tac "A \<noteq> {}")
    3.37  prefer 2 apply force
    3.38  apply (drule infinite_set_has_order_preserving_inj)
     4.1 --- a/src/HOL/Hyperreal/HLog.thy	Thu Sep 15 23:16:04 2005 +0200
     4.2 +++ b/src/HOL/Hyperreal/HLog.thy	Thu Sep 15 23:46:22 2005 +0200
     4.3 @@ -21,16 +21,16 @@
     4.4  constdefs
     4.5  
     4.6      powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
     4.7 -    "x powhr a == Ifun2_of (op powr) x a"
     4.8 +    "x powhr a == starfun2 (op powr) x a"
     4.9    
    4.10      hlog :: "[hypreal,hypreal] => hypreal"
    4.11 -    "hlog a x == Ifun2_of log a x"
    4.12 +    "hlog a x == starfun2 log a x"
    4.13  
    4.14  declare powhr_def [transfer_unfold]
    4.15  declare hlog_def [transfer_unfold]
    4.16  
    4.17  lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
    4.18 -by (simp add: powhr_def Ifun2_of_def star_of_def Ifun_star_n)
    4.19 +by (simp add: powhr_def starfun2_star_n)
    4.20  
    4.21  lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
    4.22  by (transfer, simp)
    4.23 @@ -81,7 +81,7 @@
    4.24  lemma hlog:
    4.25       "hlog (star_n X) (star_n Y) =  
    4.26        star_n (%n. log (X n) (Y n))"
    4.27 -by (simp add: hlog_def Ifun2_of_def star_of_def Ifun_star_n)
    4.28 +by (simp add: hlog_def starfun2_star_n)
    4.29  
    4.30  lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
    4.31  by (transfer, rule log_ln)
     5.1 --- a/src/HOL/Hyperreal/HSeries.thy	Thu Sep 15 23:16:04 2005 +0200
     5.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Thu Sep 15 23:46:22 2005 +0200
     5.3 @@ -14,12 +14,7 @@
     5.4  constdefs 
     5.5    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
     5.6     "sumhr == 
     5.7 -      %(M,N,f). Ifun2_of (%m n. setsum f {m..<n}) M N"
     5.8 -(*
     5.9 -   "sumhr p == 
    5.10 -      (%(M,N,f). Abs_star(\<Union>X \<in> Rep_star(M). \<Union>Y \<in> Rep_star(N).  
    5.11 -                             starrel ``{%n::nat. setsum f {X n..<Y n}})) p"
    5.12 -*)
    5.13 +      %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N"
    5.14  
    5.15    NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
    5.16     "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
    5.17 @@ -34,7 +29,7 @@
    5.18  lemma sumhr:
    5.19       "sumhr(star_n M, star_n N, f) =  
    5.20        star_n (%n. setsum f {M n..<N n})"
    5.21 -by (simp add: sumhr_def Ifun2_of_def star_of_def Ifun_star_n)
    5.22 +by (simp add: sumhr_def starfun2_star_n)
    5.23  
    5.24  text{*Base case in definition of @{term sumr}*}
    5.25  lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
     6.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Thu Sep 15 23:16:04 2005 +0200
     6.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Thu Sep 15 23:46:22 2005 +0200
     6.3 @@ -43,7 +43,7 @@
     6.4  
     6.5  constdefs
     6.6    hypreal_of_nat   :: "nat => hypreal"
     6.7 -   "hypreal_of_nat m  == of_nat m"
     6.8 +   "hypreal_of_nat m == of_nat m"
     6.9  
    6.10  lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
    6.11  by (force simp add: hypreal_of_nat_def Nats_def) 
     7.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 15 23:16:04 2005 +0200
     7.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 15 23:46:22 2005 +0200
     7.3 @@ -17,14 +17,6 @@
     7.4  syntax hypreal_of_real :: "real => real star"
     7.5  translations "hypreal_of_real" => "star_of :: real => real star"
     7.6  
     7.7 -typed_print_translation {*
     7.8 -  let
     7.9 -    fun hr_tr' _ (Type ("fun", (Type ("real", []) :: _))) [t] =
    7.10 -          Syntax.const "hypreal_of_real" $ t
    7.11 -      | hr_tr' _ _ _ = raise Match;
    7.12 -  in [("star_of", hr_tr')] end
    7.13 -*}
    7.14 -
    7.15  constdefs
    7.16  
    7.17    omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
    7.18 @@ -42,34 +34,13 @@
    7.19    epsilon :: hypreal   ("\<epsilon>")
    7.20  
    7.21  
    7.22 -subsection{*The Set of Naturals is not Finite*}
    7.23 -
    7.24 -(*** based on James' proof that the set of naturals is not finite ***)
    7.25 -lemma finite_exhausts [rule_format]:
    7.26 -     "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)"
    7.27 -apply (rule impI)
    7.28 -apply (erule_tac F = A in finite_induct)
    7.29 -apply (blast, erule exE)
    7.30 -apply (rule_tac x = "n + x" in exI)
    7.31 -apply (rule allI, erule_tac x = "x + m" in allE)
    7.32 -apply (auto simp add: add_ac)
    7.33 -done
    7.34 -
    7.35 -lemma finite_not_covers [rule_format (no_asm)]:
    7.36 -     "finite (A :: nat set) --> (\<exists>n. n \<notin>A)"
    7.37 -by (rule impI, drule finite_exhausts, blast)
    7.38 -
    7.39 -lemma not_finite_nat: "~ finite(UNIV:: nat set)"
    7.40 -by (fast dest!: finite_exhausts)
    7.41 -
    7.42 -
    7.43  subsection{*Existence of Free Ultrafilter over the Naturals*}
    7.44  
    7.45  text{*Also, proof of various properties of @{term FreeUltrafilterNat}: 
    7.46  an arbitrary free ultrafilter*}
    7.47  
    7.48  lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
    7.49 -by (rule not_finite_nat [THEN freeultrafilter_Ex])
    7.50 +by (rule nat_infinite [THEN freeultrafilter_Ex])
    7.51  
    7.52  lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
    7.53  apply (unfold FreeUltrafilterNat_def)
    7.54 @@ -170,7 +141,7 @@
    7.55  text{*Proving that @{term starrel} is an equivalence relation*}
    7.56  
    7.57  lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
    7.58 -by (simp add: starrel_def)
    7.59 +by (rule StarDef.starrel_iff)
    7.60  
    7.61  lemma starrel_refl: "(x,x) \<in> starrel"
    7.62  by (simp add: starrel_def)
    7.63 @@ -183,7 +154,7 @@
    7.64  by (simp add: starrel_def, ultra)
    7.65  
    7.66  lemma equiv_starrel: "equiv UNIV starrel"
    7.67 -by (rule StarType.equiv_starrel)
    7.68 +by (rule StarDef.equiv_starrel)
    7.69  
    7.70  (* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
    7.71  lemmas equiv_starrel_iff =
    7.72 @@ -194,7 +165,6 @@
    7.73  
    7.74  declare Abs_star_inject [simp] Abs_star_inverse [simp]
    7.75  declare equiv_starrel [THEN eq_equiv_class_iff, simp]
    7.76 -declare starrel_iff [iff]
    7.77  
    7.78  lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
    7.79  
    7.80 @@ -215,10 +185,6 @@
    7.81  lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
    7.82  by (rule inj_onI, simp)
    7.83  
    7.84 -lemma eq_Abs_star:
    7.85 -    "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P"
    7.86 -by (fold star_n_def, auto intro: star_cases)
    7.87 -
    7.88  lemma Rep_star_star_n_iff [simp]:
    7.89    "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)"
    7.90  by (simp add: star_n_def)
    7.91 @@ -226,57 +192,52 @@
    7.92  lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
    7.93  by simp
    7.94  
    7.95 -subsection{*Hyperreal Addition*}
    7.96 +subsection{* Properties of @{term star_n} *}
    7.97  
    7.98  lemma star_n_add:
    7.99    "star_n X + star_n Y = star_n (%n. X n + Y n)"
   7.100 -by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n)
   7.101 -
   7.102 -subsection{*Additive inverse on @{typ hypreal}*}
   7.103 +by (simp only: star_add_def starfun2_star_n)
   7.104  
   7.105  lemma star_n_minus:
   7.106     "- star_n X = star_n (%n. -(X n))"
   7.107 -by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n)
   7.108 +by (simp only: star_minus_def starfun_star_n)
   7.109  
   7.110  lemma star_n_diff:
   7.111       "star_n X - star_n Y = star_n (%n. X n - Y n)"
   7.112 -by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n)
   7.113 -
   7.114 -
   7.115 -subsection{*Hyperreal Multiplication*}
   7.116 +by (simp only: star_diff_def starfun2_star_n)
   7.117  
   7.118  lemma star_n_mult:
   7.119    "star_n X * star_n Y = star_n (%n. X n * Y n)"
   7.120 -by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n)
   7.121 -
   7.122 -
   7.123 -subsection{*Multiplicative Inverse on @{typ hypreal} *}
   7.124 +by (simp only: star_mult_def starfun2_star_n)
   7.125  
   7.126  lemma star_n_inverse:
   7.127 -      "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))"
   7.128 -apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
   7.129 -apply (rule_tac f=star_n in arg_cong)
   7.130 -apply (rule ext)
   7.131 -apply simp
   7.132 -done
   7.133 -
   7.134 -lemma star_n_inverse2:
   7.135        "inverse (star_n X) = star_n (%n. inverse(X n))"
   7.136 -by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
   7.137 -
   7.138 -
   7.139 -subsection{*Properties of The @{text "\<le>"} Relation*}
   7.140 +by (simp only: star_inverse_def starfun_star_n)
   7.141  
   7.142  lemma star_n_le:
   7.143        "star_n X \<le> star_n Y =  
   7.144         ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
   7.145 -by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
   7.146 +by (simp only: star_le_def starP2_star_n)
   7.147 +
   7.148 +lemma star_n_less:
   7.149 +      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   7.150 +by (simp only: star_less_def starP2_star_n)
   7.151 +
   7.152 +lemma star_n_zero_num: "0 = star_n (%n. 0)"
   7.153 +by (simp only: star_zero_def star_of_def)
   7.154 +
   7.155 +lemma star_n_one_num: "1 = star_n (%n. 1)"
   7.156 +by (simp only: star_one_def star_of_def)
   7.157 +
   7.158 +lemma star_n_abs:
   7.159 +     "abs (star_n X) = star_n (%n. abs (X n))"
   7.160 +by (simp only: star_abs_def starfun_star_n)
   7.161 +
   7.162 +subsection{*Misc Others*}
   7.163  
   7.164  lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
   7.165  by (auto)
   7.166  
   7.167 -subsection{*The Hyperreals Form an Ordered Field*}
   7.168 -
   7.169  lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
   7.170  by auto
   7.171  
   7.172 @@ -286,27 +247,8 @@
   7.173  lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
   7.174  by auto
   7.175  
   7.176 -
   7.177 -subsection{*Misc Others*}
   7.178 -
   7.179 -lemma star_n_less:
   7.180 -      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   7.181 -by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
   7.182 -
   7.183 -lemma star_n_zero_num: "0 = star_n (%n. 0)"
   7.184 -by (simp add: star_zero_def star_of_def)
   7.185 -
   7.186 -lemma star_n_one_num: "1 = star_n (%n. 1)"
   7.187 -by (simp add: star_one_def star_of_def)
   7.188 -
   7.189  lemma hypreal_omega_gt_zero [simp]: "0 < omega"
   7.190 -apply (simp only: omega_def star_zero_def star_less_def star_of_def)
   7.191 -apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
   7.192 -done
   7.193 -
   7.194 -lemma star_n_abs:
   7.195 -     "abs (star_n X) = star_n (%n. abs (X n))"
   7.196 -by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n)
   7.197 +by (simp add: omega_def star_n_zero_num star_n_less)
   7.198  
   7.199  subsection{*Existence of Infinite Hyperreal Number*}
   7.200  
   7.201 @@ -357,9 +299,7 @@
   7.202           del: star_of_zero)
   7.203  
   7.204  lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
   7.205 -apply (simp add: epsilon_def omega_def star_inverse_def)
   7.206 -apply (simp add: Ifun_of_def star_of_def Ifun_star_n)
   7.207 -done
   7.208 +by (simp add: epsilon_def omega_def star_n_inverse)
   7.209  
   7.210  
   7.211  ML
   7.212 @@ -367,9 +307,6 @@
   7.213  val omega_def = thm "omega_def";
   7.214  val epsilon_def = thm "epsilon_def";
   7.215  
   7.216 -val finite_exhausts = thm "finite_exhausts";
   7.217 -val finite_not_covers = thm "finite_not_covers";
   7.218 -val not_finite_nat = thm "not_finite_nat";
   7.219  val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
   7.220  val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
   7.221  val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
   7.222 @@ -394,7 +331,7 @@
   7.223  val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
   7.224  val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
   7.225  val inj_hypreal_of_real = thm "inj_hypreal_of_real";
   7.226 -val eq_Abs_star = thm "eq_Abs_star";
   7.227 +(* val eq_Abs_star = thm "eq_Abs_star"; *)
   7.228  val star_n_minus = thm "star_n_minus";
   7.229  val star_n_add = thm "star_n_add";
   7.230  val star_n_diff = thm "star_n_diff";
     8.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:16:04 2005 +0200
     8.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Sep 15 23:46:22 2005 +0200
     8.3 @@ -145,45 +145,15 @@
     8.4  
     8.5  
     8.6  lemma hypnat_of_nat_def: "hypnat_of_nat m == of_nat m"
     8.7 -by (transfer star_of_nat_def) simp
     8.8 -
     8.9 -lemma hypnat_of_nat_add:
    8.10 -      "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
    8.11 -by simp
    8.12 -
    8.13 -lemma hypnat_of_nat_mult:
    8.14 -      "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
    8.15 -by simp
    8.16 -
    8.17 -lemma hypnat_of_nat_less_iff:
    8.18 -      "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
    8.19 -by simp
    8.20 -
    8.21 -lemma hypnat_of_nat_le_iff:
    8.22 -      "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
    8.23 -by simp
    8.24 -
    8.25 -lemma hypnat_of_nat_eq_iff:
    8.26 -      "(hypnat_of_nat z = hypnat_of_nat w) = (z = w)"
    8.27 -by simp
    8.28 +by (transfer, simp)
    8.29  
    8.30  lemma hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) = (1::hypnat)"
    8.31  by simp
    8.32  
    8.33 -lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
    8.34 -by simp
    8.35 -
    8.36 -lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
    8.37 -by simp
    8.38 -
    8.39  lemma hypnat_of_nat_Suc [simp]:
    8.40       "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
    8.41  by (simp add: hypnat_of_nat_def)
    8.42  
    8.43 -lemma hypnat_of_nat_minus:
    8.44 -      "hypnat_of_nat ((j::nat) - k) = hypnat_of_nat j - hypnat_of_nat k"
    8.45 -by simp
    8.46 -
    8.47  
    8.48  subsection{*Existence of an infinite hypernatural number*}
    8.49  
    8.50 @@ -217,9 +187,7 @@
    8.51  
    8.52  lemma hypnat_of_nat_eq:
    8.53       "hypnat_of_nat m  = star_n (%n::nat. m)"
    8.54 -apply (induct m) 
    8.55 -apply (simp_all add: star_n_zero_num star_n_one_num star_n_add)
    8.56 -done
    8.57 +by (simp add: star_of_def)
    8.58  
    8.59  lemma SHNat_eq: "Nats = {n. \<exists>N. n = hypnat_of_nat N}"
    8.60  by (force simp add: hypnat_of_nat_def Nats_def) 
    8.61 @@ -436,7 +404,6 @@
    8.62  
    8.63  val starrel_iff = thm "starrel_iff";
    8.64  val lemma_starrel_refl = thm "lemma_starrel_refl";
    8.65 -val eq_Abs_star = thm "eq_Abs_star";
    8.66  val hypnat_minus_zero = thm "hypnat_minus_zero";
    8.67  val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
    8.68  val hypnat_add_is_0 = thm "hypnat_add_is_0";
    8.69 @@ -461,16 +428,8 @@
    8.70  val hypnat_neq0_conv = thm "hypnat_neq0_conv";
    8.71  val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
    8.72  val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
    8.73 -val hypnat_of_nat_add = thm "hypnat_of_nat_add";
    8.74 -val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
    8.75 -val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
    8.76 -val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
    8.77 -val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
    8.78 -val hypnat_of_nat_eq = thm"hypnat_of_nat_eq"
    8.79  val SHNat_eq = thm"SHNat_eq"
    8.80  val hypnat_of_nat_one = thm "hypnat_of_nat_one";
    8.81 -val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
    8.82 -val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
    8.83  val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
    8.84  val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
    8.85  val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
     9.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Sep 15 23:16:04 2005 +0200
     9.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Sep 15 23:46:22 2005 +0200
     9.3 @@ -25,7 +25,7 @@
     9.4  
     9.5    (* hypernatural powers of hyperreals *)
     9.6    hyperpow_def [transfer_unfold]:
     9.7 -  "(R::hypreal) pow (N::hypnat) == Ifun2_of (op ^) R N"
     9.8 +  "(R::hypreal) pow (N::hypnat) == ( *f2* op ^) R N"
     9.9  
    9.10  lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
    9.11  by simp
    9.12 @@ -101,7 +101,7 @@
    9.13  subsection{*Powers with Hypernatural Exponents*}
    9.14  
    9.15  lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)"
    9.16 -by (simp add: hyperpow_def Ifun2_of_def star_of_def Ifun_star_n)
    9.17 +by (simp add: hyperpow_def starfun2_star_n)
    9.18  
    9.19  lemma hyperpow_zero [simp]: "!!n. (0::hypreal) pow (n + (1::hypnat)) = 0"
    9.20  by (transfer, simp)
    10.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Sep 15 23:16:04 2005 +0200
    10.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu Sep 15 23:46:22 2005 +0200
    10.3 @@ -1777,7 +1777,7 @@
    10.4  lemma FreeUltrafilterNat_Rep_hypreal:
    10.5       "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
    10.6        ==> {n. X n = Y n} \<in> FreeUltrafilterNat"
    10.7 -by (rule_tac z = x in eq_Abs_star, auto, ultra)
    10.8 +by (cases x, unfold star_n_def, auto, ultra)
    10.9  
   10.10  lemma HFinite_FreeUltrafilterNat:
   10.11      "x \<in> HFinite 
    11.1 --- a/src/HOL/Hyperreal/NatStar.thy	Thu Sep 15 23:16:04 2005 +0200
    11.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Thu Sep 15 23:46:22 2005 +0200
    11.3 @@ -113,11 +113,7 @@
    11.4    @{term real_of_nat} *}
    11.5  
    11.6  lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
    11.7 -apply (unfold hypreal_of_hypnat_def)
    11.8 -apply (rule ext)
    11.9 -apply (rule_tac z = x in eq_Abs_star)
   11.10 -apply (simp add: hypreal_of_hypnat starfun)
   11.11 -done
   11.12 +by (transfer, rule refl)
   11.13  
   11.14  lemma starfun_inverse_real_of_nat_eq:
   11.15       "N \<in> HNatInfinite
   11.16 @@ -225,24 +221,13 @@
   11.17  
   11.18  subsection{*Nonstandard Characterization of Induction*}
   11.19  
   11.20 -syntax
   11.21 -  starP :: "('a => bool) => 'a star => bool" ("*p* _" [80] 80)
   11.22 -  starP2 :: "('a => 'b => bool) => 'a star => 'b star => bool"
   11.23 -               ("*p2* _" [80] 80)
   11.24 -
   11.25 -translations
   11.26 -  "starP" == "Ipred_of"
   11.27 -  "starP2" == "Ipred2_of"
   11.28  
   11.29  constdefs
   11.30    hSuc :: "hypnat => hypnat"
   11.31    "hSuc n == n + 1"
   11.32  
   11.33  lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"
   11.34 -by (simp add: Ipred_of_def star_of_def Ifun_star_n unstar_star_n)
   11.35 -
   11.36 -lemma starP_star_of [simp]: "( *p* P) (star_of n) = P n"
   11.37 -by (transfer, rule refl)
   11.38 +by (rule starP_star_n)
   11.39  
   11.40  lemma hypnat_induct_obj:
   11.41      "!!n. (( *p* P) (0::hypnat) &
   11.42 @@ -259,7 +244,7 @@
   11.43  lemma starP2:
   11.44  "(( *p2* P) (star_n X) (star_n Y)) =
   11.45        ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
   11.46 -by (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
   11.47 +by (rule starP2_star_n)
   11.48  
   11.49  lemma starP2_eq_iff: "( *p2* (op =)) = (op =)"
   11.50  by (transfer, rule refl)
   11.51 @@ -267,11 +252,6 @@
   11.52  lemma starP2_eq_iff2: "( *p2* (%x y. x = y)) X Y = (X = Y)"
   11.53  by (simp add: starP2_eq_iff)
   11.54  
   11.55 -lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_star(starrel `` {x})))"
   11.56 -apply auto
   11.57 -apply (rule_tac z = h in eq_Abs_star, auto)
   11.58 -done
   11.59 -
   11.60  lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
   11.61  by (simp add: hSuc_def)
   11.62  
    12.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:16:04 2005 +0200
    12.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Sep 15 23:46:22 2005 +0200
    12.3 @@ -70,7 +70,7 @@
    12.4  lemma SEQ_Infinitesimal:
    12.5        "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
    12.6  apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
    12.7 -apply (simp add: star_n_inverse2)
    12.8 +apply (simp add: star_n_inverse)
    12.9  apply (rule bexI [OF _ Rep_star_star_n])
   12.10  apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
   12.11  done
    13.1 --- a/src/HOL/Hyperreal/Star.thy	Thu Sep 15 23:16:04 2005 +0200
    13.2 +++ b/src/HOL/Hyperreal/Star.thy	Thu Sep 15 23:46:22 2005 +0200
    13.3 @@ -10,13 +10,6 @@
    13.4  imports NSA
    13.5  begin
    13.6  
    13.7 -(* nonstandard extension of sets *)
    13.8 -syntax starset :: "'a set => 'a star set" ("*s* _" [80] 80)
    13.9 -translations "starset" == "Iset_of"
   13.10 -
   13.11 -syntax starfun :: "('a => 'b) => 'a star => 'b star" ("*f* _" [80] 80)
   13.12 -translations "starfun" == "Ifun_of"
   13.13 -
   13.14  constdefs
   13.15      (* internal sets *)
   13.16      starset_n :: "(nat => 'a set) => 'a star set"        ("*sn* _" [80] 80)
   13.17 @@ -54,10 +47,10 @@
   13.18  
   13.19  subsection{*Properties of the Star-transform Applied to Sets of Reals*}
   13.20  
   13.21 -lemma STAR_UNIV_set [simp]: "*s*(UNIV::'a set) = (UNIV::'a star set)"
   13.22 +lemma STAR_UNIV_set: "*s*(UNIV::'a set) = (UNIV::'a star set)"
   13.23  by (transfer UNIV_def, rule refl)
   13.24  
   13.25 -lemma STAR_empty_set [simp]: "*s* {} = {}"
   13.26 +lemma STAR_empty_set: "*s* {} = {}"
   13.27  by (transfer empty_def, rule refl)
   13.28  
   13.29  lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
   13.30 @@ -98,13 +91,10 @@
   13.31  
   13.32  lemma STAR_real_seq_to_hypreal:
   13.33      "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
   13.34 -apply (unfold Iset_of_def star_of_def)
   13.35 +apply (unfold starset_def star_of_def)
   13.36  apply (simp add: Iset_star_n)
   13.37  done
   13.38  
   13.39 -lemma STAR_insert [simp]: "*s* (insert x A) = insert (star_of x) ( *s* A)"
   13.40 -by (transfer insert_def Un_def, rule refl)
   13.41 -
   13.42  lemma STAR_singleton: "*s* {x} = {star_of x}"
   13.43  by simp
   13.44  
   13.45 @@ -119,7 +109,7 @@
   13.46  
   13.47  lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
   13.48  apply (drule expand_fun_eq [THEN iffD2])
   13.49 -apply (simp add: starset_n_def Iset_of_def star_of_def)
   13.50 +apply (simp add: starset_n_def starset_def star_of_def)
   13.51  done
   13.52  
   13.53  
   13.54 @@ -134,7 +124,7 @@
   13.55  
   13.56  lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
   13.57  apply (drule expand_fun_eq [THEN iffD2])
   13.58 -apply (simp add: starfun_n_def Ifun_of_def star_of_def)
   13.59 +apply (simp add: starfun_n_def starfun_def star_of_def)
   13.60  done
   13.61  
   13.62  
   13.63 @@ -148,34 +138,31 @@
   13.64  
   13.65  lemma hrabs_is_starext_rabs: "is_starext abs abs"
   13.66  apply (simp add: is_starext_def, safe)
   13.67 -apply (rule_tac z = x in eq_Abs_star)
   13.68 -apply (rule_tac z = y in eq_Abs_star, auto)
   13.69 +apply (rule_tac x=x in star_cases)
   13.70 +apply (rule_tac x=y in star_cases)
   13.71 +apply (unfold star_n_def, auto)
   13.72  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
   13.73  apply (rule bexI, rule_tac [2] lemma_starrel_refl)
   13.74  apply (fold star_n_def)
   13.75 -apply (unfold star_abs_def Ifun_of_def star_of_def)
   13.76 +apply (unfold star_abs_def starfun_def star_of_def)
   13.77  apply (simp add: Ifun_star_n star_n_eq_iff)
   13.78  done
   13.79  
   13.80  lemma Rep_star_FreeUltrafilterNat:
   13.81       "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
   13.82        ==> {n. X n = Y n} : FreeUltrafilterNat"
   13.83 -apply (rule_tac z = z in eq_Abs_star)
   13.84 -apply (auto, ultra)
   13.85 -done
   13.86 +by (rule FreeUltrafilterNat_Rep_hypreal)
   13.87  
   13.88  text{*Nonstandard extension of functions*}
   13.89  
   13.90  lemma starfun:
   13.91        "( *f* f) (star_n X) = star_n (%n. f (X n))"
   13.92 -by (simp add: Ifun_of_def star_of_def Ifun_star_n)
   13.93 +by (simp add: starfun_def star_of_def Ifun_star_n)
   13.94  
   13.95  lemma starfun_if_eq:
   13.96 -     "w \<noteq> hypreal_of_real x
   13.97 +     "!!w. w \<noteq> star_of x
   13.98         ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
   13.99 -apply (cases w)
  13.100 -apply (simp add: star_of_def starfun star_n_eq_iff, ultra)
  13.101 -done
  13.102 +by (transfer, simp)
  13.103  
  13.104  (*-------------------------------------------
  13.105    multiplication: ( *f) x ( *g) = *(f x g)
    14.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 15 23:16:04 2005 +0200
    14.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 15 23:46:22 2005 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  header {* Class Instances *}
    14.5  
    14.6  theory StarClasses
    14.7 -imports Transfer
    14.8 +imports StarDef
    14.9  begin
   14.10  
   14.11  subsection {* Syntactic classes *}
   14.12 @@ -26,18 +26,18 @@
   14.13    star_zero_def:    "0 \<equiv> star_of 0"
   14.14    star_one_def:     "1 \<equiv> star_of 1"
   14.15    star_number_def:  "number_of b \<equiv> star_of (number_of b)"
   14.16 -  star_add_def:     "(op +) \<equiv> Ifun2_of (op +)"
   14.17 -  star_diff_def:    "(op -) \<equiv> Ifun2_of (op -)"
   14.18 -  star_minus_def:   "uminus \<equiv> Ifun_of uminus"
   14.19 -  star_mult_def:    "(op *) \<equiv> Ifun2_of (op *)"
   14.20 -  star_divide_def:  "(op /) \<equiv> Ifun2_of (op /)"
   14.21 -  star_inverse_def: "inverse \<equiv> Ifun_of inverse"
   14.22 -  star_le_def:      "(op \<le>) \<equiv> Ipred2_of (op \<le>)"
   14.23 -  star_less_def:    "(op <) \<equiv> Ipred2_of (op <)"
   14.24 -  star_abs_def:     "abs \<equiv> Ifun_of abs"
   14.25 -  star_div_def:     "(op div) \<equiv> Ifun2_of (op div)"
   14.26 -  star_mod_def:     "(op mod) \<equiv> Ifun2_of (op mod)"
   14.27 -  star_power_def:   "(op ^) \<equiv> \<lambda>x n. Ifun_of (\<lambda>x. x ^ n) x"
   14.28 +  star_add_def:     "(op +) \<equiv> *f2* (op +)"
   14.29 +  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
   14.30 +  star_minus_def:   "uminus \<equiv> *f* uminus"
   14.31 +  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
   14.32 +  star_divide_def:  "(op /) \<equiv> *f2* (op /)"
   14.33 +  star_inverse_def: "inverse \<equiv> *f* inverse"
   14.34 +  star_le_def:      "(op \<le>) \<equiv> *p2* (op \<le>)"
   14.35 +  star_less_def:    "(op <) \<equiv> *p2* (op <)"
   14.36 +  star_abs_def:     "abs \<equiv> *f* abs"
   14.37 +  star_div_def:     "(op div) \<equiv> *f2* (op div)"
   14.38 +  star_mod_def:     "(op mod) \<equiv> *f2* (op mod)"
   14.39 +  star_power_def:   "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
   14.40  
   14.41  lemmas star_class_defs [transfer_unfold] =
   14.42    star_zero_def     star_one_def      star_number_def
   14.43 @@ -173,12 +173,12 @@
   14.44  *}
   14.45  
   14.46  lemma ex_star_fun:
   14.47 -  "\<exists>f::('a \<Rightarrow> 'b) star. P (Ifun f)
   14.48 +  "\<exists>f::('a \<Rightarrow> 'b) star. P (\<lambda>x. f \<star> x)
   14.49     \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star. P f"
   14.50  by (erule exE, erule exI)
   14.51  
   14.52  lemma ex_star_fun2:
   14.53 -  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (Ifun2 f)
   14.54 +  "\<exists>f::('a \<Rightarrow> 'b \<Rightarrow> 'c) star. P (\<lambda>x y. f \<star> x \<star> y)
   14.55     \<Longrightarrow> \<exists>f::'a star \<Rightarrow> 'b star \<Rightarrow> 'c star. P f"
   14.56  by (erule exE, erule exI)
   14.57  
   14.58 @@ -198,13 +198,13 @@
   14.59  
   14.60  instance star :: (lorder) lorder ..
   14.61  
   14.62 -lemma star_join_def [transfer_unfold]: "join \<equiv> Ifun2_of join"
   14.63 - apply (rule is_join_unique[OF is_join_join, THEN eq_reflection])
   14.64 +lemma star_join_def [transfer_unfold]: "join \<equiv> *f2* join"
   14.65 + apply (rule is_join_unique [OF is_join_join, THEN eq_reflection])
   14.66   apply (transfer is_join_def, rule is_join_join)
   14.67  done
   14.68  
   14.69 -lemma star_meet_def [transfer_unfold]: "meet \<equiv> Ifun2_of meet"
   14.70 - apply (rule is_meet_unique[OF is_meet_meet, THEN eq_reflection])
   14.71 +lemma star_meet_def [transfer_unfold]: "meet \<equiv> *f2* meet"
   14.72 + apply (rule is_meet_unique [OF is_meet_meet, THEN eq_reflection])
   14.73   apply (transfer is_meet_def, rule is_meet_meet)
   14.74  done
   14.75  
   14.76 @@ -266,7 +266,7 @@
   14.77  instance star :: (lordered_ab_group_abs) lordered_ab_group_abs
   14.78  by (intro_classes, transfer, rule abs_lattice)
   14.79  
   14.80 -text "Ring-and-Field.thy"
   14.81 +subsection {* Ring and field classes *}
   14.82  
   14.83  instance star :: (semiring) semiring
   14.84  apply (intro_classes)
   14.85 @@ -390,4 +390,16 @@
   14.86  instance star :: (number_ring) number_ring
   14.87  by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
   14.88  
   14.89 +subsection {* Finite class *}
   14.90 +
   14.91 +lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
   14.92 +by (erule finite_induct, simp_all)
   14.93 +
   14.94 +instance star :: (finite) finite
   14.95 +apply (intro_classes)
   14.96 +apply (subst starset_UNIV [symmetric])
   14.97 +apply (subst starset_finite [OF finite])
   14.98 +apply (rule finite_imageI [OF finite])
   14.99 +done
  14.100 +
  14.101  end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Hyperreal/StarDef.thy	Thu Sep 15 23:46:22 2005 +0200
    15.3 @@ -0,0 +1,373 @@
    15.4 +(*  Title       : HOL/Hyperreal/StarDef.thy
    15.5 +    ID          : $Id$
    15.6 +    Author      : Jacques D. Fleuriot and Brian Huffman
    15.7 +*)
    15.8 +
    15.9 +header {* Construction of Star Types Using Ultrafilters *}
   15.10 +
   15.11 +theory StarDef
   15.12 +imports Filter
   15.13 +uses ("transfer.ML")
   15.14 +begin
   15.15 +
   15.16 +subsection {* A Free Ultrafilter over the Naturals *}
   15.17 +
   15.18 +constdefs
   15.19 +  FreeUltrafilterNat :: "nat set set"  ("\<U>")
   15.20 +    "\<U> \<equiv> SOME U. freeultrafilter U"
   15.21 +
   15.22 +lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
   15.23 + apply (unfold FreeUltrafilterNat_def)
   15.24 + apply (rule someI_ex)
   15.25 + apply (rule freeultrafilter_Ex)
   15.26 + apply (rule nat_infinite)
   15.27 +done
   15.28 +
   15.29 +lemmas ultrafilter_FUFNat =
   15.30 +  freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter]
   15.31 +
   15.32 +lemmas filter_FUFNat =
   15.33 +  freeultrafilter_FUFNat [THEN freeultrafilter.filter]
   15.34 +
   15.35 +lemmas FUFNat_empty [iff] =
   15.36 +  filter_FUFNat [THEN filter.empty]
   15.37 +
   15.38 +lemmas FUFNat_UNIV [iff] =
   15.39 +  filter_FUFNat [THEN filter.UNIV]
   15.40 +
   15.41 +text {* This rule takes the place of the old ultra tactic *}
   15.42 +
   15.43 +lemma ultra:
   15.44 +  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
   15.45 +by (simp add: Collect_imp_eq
   15.46 +    ultrafilter_FUFNat [THEN ultrafilter.Un_iff]
   15.47 +    ultrafilter_FUFNat [THEN ultrafilter.Compl_iff])
   15.48 +
   15.49 +
   15.50 +subsection {* Definition of @{text star} type constructor *}
   15.51 +
   15.52 +constdefs
   15.53 +  starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
   15.54 +    "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
   15.55 +
   15.56 +typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
   15.57 +by (auto intro: quotientI)
   15.58 +
   15.59 +constdefs
   15.60 +  star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
   15.61 +  "star_n X \<equiv> Abs_star (starrel `` {X})"
   15.62 +
   15.63 +theorem star_cases [case_names star_n, cases type: star]:
   15.64 +  "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
   15.65 +by (cases x, unfold star_n_def star_def, erule quotientE, fast)
   15.66 +
   15.67 +lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
   15.68 +by (auto, rule_tac x=x in star_cases, simp)
   15.69 +
   15.70 +lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
   15.71 +by (auto, rule_tac x=x in star_cases, auto)
   15.72 +
   15.73 +text {* Proving that @{term starrel} is an equivalence relation *}
   15.74 +
   15.75 +lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
   15.76 +by (simp add: starrel_def)
   15.77 +
   15.78 +lemma equiv_starrel: "equiv UNIV starrel"
   15.79 +proof (rule equiv.intro)
   15.80 +  show "reflexive starrel" by (simp add: refl_def)
   15.81 +  show "sym starrel" by (simp add: sym_def eq_commute)
   15.82 +  show "trans starrel" by (auto intro: transI elim!: ultra)
   15.83 +qed
   15.84 +
   15.85 +lemmas equiv_starrel_iff =
   15.86 +  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
   15.87 +
   15.88 +lemma starrel_in_star: "starrel``{x} \<in> star"
   15.89 +by (simp add: star_def quotientI)
   15.90 +
   15.91 +lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
   15.92 +by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
   15.93 +
   15.94 +
   15.95 +subsection {* Transfer principle *}
   15.96 +
   15.97 +text {* This introduction rule starts each transfer proof. *}
   15.98 +lemma transfer_start:
   15.99 +  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
  15.100 +by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
  15.101 +
  15.102 +text {*Initialize transfer tactic.*}
  15.103 +use "transfer.ML"
  15.104 +setup Transfer.setup
  15.105 +
  15.106 +text {* Transfer introduction rules. *}
  15.107 +
  15.108 +lemma transfer_ex [transfer_intro]:
  15.109 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  15.110 +    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
  15.111 +by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat])
  15.112 +
  15.113 +lemma transfer_all [transfer_intro]:
  15.114 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  15.115 +    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
  15.116 +by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat])
  15.117 +
  15.118 +lemma transfer_not [transfer_intro]:
  15.119 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
  15.120 +by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
  15.121 +
  15.122 +lemma transfer_conj [transfer_intro]:
  15.123 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
  15.124 +    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
  15.125 +by (simp only: filter.Collect_conj [OF filter_FUFNat])
  15.126 +
  15.127 +lemma transfer_disj [transfer_intro]:
  15.128 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
  15.129 +    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
  15.130 +by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
  15.131 +
  15.132 +lemma transfer_imp [transfer_intro]:
  15.133 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
  15.134 +    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
  15.135 +by (simp only: imp_conv_disj transfer_disj transfer_not)
  15.136 +
  15.137 +lemma transfer_iff [transfer_intro]:
  15.138 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
  15.139 +    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
  15.140 +by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
  15.141 +
  15.142 +lemma transfer_if_bool [transfer_intro]:
  15.143 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
  15.144 +    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
  15.145 +by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
  15.146 +
  15.147 +lemma transfer_eq [transfer_intro]:
  15.148 +  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
  15.149 +by (simp only: star_n_eq_iff)
  15.150 +
  15.151 +lemma transfer_if [transfer_intro]:
  15.152 +  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
  15.153 +    \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
  15.154 +apply (rule eq_reflection)
  15.155 +apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
  15.156 +done
  15.157 +
  15.158 +lemma transfer_fun_eq [transfer_intro]:
  15.159 +  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
  15.160 +    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
  15.161 +      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
  15.162 +by (simp only: expand_fun_eq transfer_all)
  15.163 +
  15.164 +lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
  15.165 +by (rule reflexive)
  15.166 +
  15.167 +lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>"
  15.168 +by (simp add: atomize_eq)
  15.169 +
  15.170 +
  15.171 +subsection {* Standard elements *}
  15.172 +
  15.173 +constdefs
  15.174 +  star_of :: "'a \<Rightarrow> 'a star"
  15.175 +  "star_of x \<equiv> star_n (\<lambda>n. x)"
  15.176 +
  15.177 +text {* Transfer tactic should remove occurrences of @{term star_of} *}
  15.178 +setup {* [Transfer.add_const "StarDef.star_of"] *}
  15.179 +declare star_of_def [transfer_intro]
  15.180 +
  15.181 +lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
  15.182 +by (transfer, rule refl)
  15.183 +
  15.184 +
  15.185 +subsection {* Internal functions *}
  15.186 +
  15.187 +constdefs
  15.188 +  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
  15.189 +  "Ifun f \<equiv> \<lambda>x. Abs_star
  15.190 +       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
  15.191 +
  15.192 +lemma Ifun_congruent2:
  15.193 +  "(\<lambda>F X. starrel``{\<lambda>n. F n (X n)}) respects2 starrel"
  15.194 +by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra)
  15.195 +
  15.196 +lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
  15.197 +by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
  15.198 +    UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
  15.199 +
  15.200 +text {* Transfer tactic should remove occurrences of @{term Ifun} *}
  15.201 +setup {* [Transfer.add_const "StarDef.Ifun"] *}
  15.202 +
  15.203 +lemma transfer_Ifun [transfer_intro]:
  15.204 +  "\<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))"
  15.205 +by (simp only: Ifun_star_n)
  15.206 +
  15.207 +lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)"
  15.208 +by (transfer, rule refl)
  15.209 +
  15.210 +text {* Nonstandard extensions of functions *}
  15.211 +
  15.212 +constdefs
  15.213 +  starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
  15.214 +    ("*f* _" [80] 80)
  15.215 +  "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
  15.216 +
  15.217 +  starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
  15.218 +    ("*f2* _" [80] 80)
  15.219 +  "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
  15.220 +
  15.221 +declare starfun_def [transfer_unfold]
  15.222 +declare starfun2_def [transfer_unfold]
  15.223 +
  15.224 +lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))"
  15.225 +by (simp only: starfun_def star_of_def Ifun_star_n)
  15.226 +
  15.227 +lemma starfun2_star_n:
  15.228 +  "( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))"
  15.229 +by (simp only: starfun2_def star_of_def Ifun_star_n)
  15.230 +
  15.231 +lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)"
  15.232 +by (transfer, rule refl)
  15.233 +
  15.234 +lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x"
  15.235 +by (transfer, rule refl)
  15.236 +
  15.237 +
  15.238 +subsection {* Internal predicates *}
  15.239 +
  15.240 +constdefs
  15.241 +  unstar :: "bool star \<Rightarrow> bool"
  15.242 +  "unstar b \<equiv> b = star_of True"
  15.243 +
  15.244 +lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
  15.245 +by (simp add: unstar_def star_of_def star_n_eq_iff)
  15.246 +
  15.247 +lemma unstar_star_of [simp]: "unstar (star_of p) = p"
  15.248 +by (simp add: unstar_def star_of_inject)
  15.249 +
  15.250 +text {* Transfer tactic should remove occurrences of @{term unstar} *}
  15.251 +setup {* [Transfer.add_const "StarDef.unstar"] *}
  15.252 +
  15.253 +lemma transfer_unstar [transfer_intro]:
  15.254 +  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
  15.255 +by (simp only: unstar_star_n)
  15.256 +
  15.257 +constdefs
  15.258 +  starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
  15.259 +    ("*p* _" [80] 80)
  15.260 +  "*p* P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
  15.261 +
  15.262 +  starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
  15.263 +    ("*p2* _" [80] 80)
  15.264 +  "*p2* P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
  15.265 +
  15.266 +declare starP_def [transfer_unfold]
  15.267 +declare starP2_def [transfer_unfold]
  15.268 +
  15.269 +lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)"
  15.270 +by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n)
  15.271 +
  15.272 +lemma starP2_star_n:
  15.273 +  "( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)"
  15.274 +by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n)
  15.275 +
  15.276 +lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x"
  15.277 +by (transfer, rule refl)
  15.278 +
  15.279 +lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x"
  15.280 +by (transfer, rule refl)
  15.281 +
  15.282 +
  15.283 +subsection {* Internal sets *}
  15.284 +
  15.285 +constdefs
  15.286 +  Iset :: "'a set star \<Rightarrow> 'a star set"
  15.287 +  "Iset A \<equiv> {x. ( *p2* op \<in>) x A}"
  15.288 +
  15.289 +lemma Iset_star_n:
  15.290 +  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
  15.291 +by (simp add: Iset_def starP2_star_n)
  15.292 +
  15.293 +text {* Transfer tactic should remove occurrences of @{term Iset} *}
  15.294 +setup {* [Transfer.add_const "StarDef.Iset"] *}
  15.295 +
  15.296 +lemma transfer_mem [transfer_intro]:
  15.297 +  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
  15.298 +    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
  15.299 +by (simp only: Iset_star_n)
  15.300 +
  15.301 +lemma transfer_Collect [transfer_intro]:
  15.302 +  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  15.303 +    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
  15.304 +by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
  15.305 +
  15.306 +lemma transfer_set_eq [transfer_intro]:
  15.307 +  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
  15.308 +    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
  15.309 +by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
  15.310 +
  15.311 +lemma transfer_ball [transfer_intro]:
  15.312 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  15.313 +    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
  15.314 +by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
  15.315 +
  15.316 +lemma transfer_bex [transfer_intro]:
  15.317 +  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  15.318 +    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
  15.319 +by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
  15.320 +
  15.321 +lemma transfer_Iset [transfer_intro]:
  15.322 +  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
  15.323 +by simp
  15.324 +
  15.325 +text {* Nonstandard extensions of sets. *}
  15.326 +constdefs
  15.327 +  starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80)
  15.328 +  "starset A \<equiv> Iset (star_of A)"
  15.329 +
  15.330 +declare starset_def [transfer_unfold]
  15.331 +
  15.332 +lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)"
  15.333 +by (transfer, rule refl)
  15.334 +
  15.335 +lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)"
  15.336 +by (transfer UNIV_def, rule refl)
  15.337 +
  15.338 +lemma starset_empty: "*s* {} = {}"
  15.339 +by (transfer empty_def, rule refl)
  15.340 +
  15.341 +lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)"
  15.342 +by (transfer insert_def Un_def, rule refl)
  15.343 +
  15.344 +lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B"
  15.345 +by (transfer Un_def, rule refl)
  15.346 +
  15.347 +lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B"
  15.348 +by (transfer Int_def, rule refl)
  15.349 +
  15.350 +lemma starset_Compl: "*s* -A = -( *s* A)"
  15.351 +by (transfer Compl_def, rule refl)
  15.352 +
  15.353 +lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
  15.354 +by (transfer set_diff_def, rule refl)
  15.355 +
  15.356 +lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
  15.357 +by (transfer image_def, rule refl)
  15.358 +
  15.359 +lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)"
  15.360 +by (transfer vimage_def, rule refl)
  15.361 +
  15.362 +lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
  15.363 +by (transfer subset_def, rule refl)
  15.364 +
  15.365 +lemma starset_eq: "( *s* A = *s* B) = (A = B)"
  15.366 +by (transfer, rule refl)
  15.367 +
  15.368 +lemmas starset_simps [simp] =
  15.369 +  starset_mem     starset_UNIV
  15.370 +  starset_empty   starset_insert
  15.371 +  starset_Un      starset_Int
  15.372 +  starset_Compl   starset_diff
  15.373 +  starset_image   starset_vimage
  15.374 +  starset_subset  starset_eq
  15.375 +
  15.376 +end
    16.1 --- a/src/HOL/Hyperreal/StarType.thy	Thu Sep 15 23:16:04 2005 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,205 +0,0 @@
    16.4 -(*  Title       : HOL/Hyperreal/StarType.thy
    16.5 -    ID          : $Id$
    16.6 -    Author      : Jacques D. Fleuriot and Brian Huffman
    16.7 -*)
    16.8 -
    16.9 -header {* Construction of Star Types Using Ultrafilters *}
   16.10 -
   16.11 -theory StarType
   16.12 -imports Filter
   16.13 -begin
   16.14 -
   16.15 -subsection {* A Free Ultrafilter over the Naturals *}
   16.16 -
   16.17 -constdefs
   16.18 -  FreeUltrafilterNat :: "nat set set"  ("\<U>")
   16.19 -    "\<U> \<equiv> SOME U. freeultrafilter U"
   16.20 -
   16.21 -lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
   16.22 - apply (unfold FreeUltrafilterNat_def)
   16.23 - apply (rule someI_ex)
   16.24 - apply (rule freeultrafilter_Ex)
   16.25 - apply (rule nat_infinite)
   16.26 -done
   16.27 -
   16.28 -lemmas ultrafilter_FUFNat =
   16.29 -  freeultrafilter_FUFNat [THEN freeultrafilter.ultrafilter]
   16.30 -
   16.31 -lemmas filter_FUFNat =
   16.32 -  freeultrafilter_FUFNat [THEN freeultrafilter.filter]
   16.33 -
   16.34 -lemmas FUFNat_empty [iff] =
   16.35 -  filter_FUFNat [THEN filter.empty]
   16.36 -
   16.37 -lemmas FUFNat_UNIV [iff] =
   16.38 -  filter_FUFNat [THEN filter.UNIV]
   16.39 -
   16.40 -text {* This rule takes the place of the old ultra tactic *}
   16.41 -
   16.42 -lemma ultra:
   16.43 -  "\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>"
   16.44 -by (simp add: Collect_imp_eq
   16.45 -    ultrafilter_FUFNat [THEN ultrafilter.Un_iff]
   16.46 -    ultrafilter_FUFNat [THEN ultrafilter.Compl_iff])
   16.47 -
   16.48 -
   16.49 -subsection {* Definition of @{text star} type constructor *}
   16.50 -
   16.51 -constdefs
   16.52 -  starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
   16.53 -    "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
   16.54 -
   16.55 -typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
   16.56 -by (auto intro: quotientI)
   16.57 -
   16.58 -text {* Proving that @{term starrel} is an equivalence relation *}
   16.59 -
   16.60 -lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)"
   16.61 -by (simp add: starrel_def)
   16.62 -
   16.63 -lemma equiv_starrel: "equiv UNIV starrel"
   16.64 -proof (rule equiv.intro)
   16.65 -  show "reflexive starrel" by (simp add: refl_def)
   16.66 -  show "sym starrel" by (simp add: sym_def eq_commute)
   16.67 -  show "trans starrel" by (auto intro: transI elim!: ultra)
   16.68 -qed
   16.69 -
   16.70 -lemmas equiv_starrel_iff =
   16.71 -  eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I]
   16.72 -  -- {* @{term "(starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel)"} *}
   16.73 -
   16.74 -lemma starrel_in_star: "starrel``{x} \<in> star"
   16.75 -by (simp add: star_def starrel_def quotient_def, fast)
   16.76 -
   16.77 -lemma eq_Abs_star:
   16.78 -  "(\<And>x. z = Abs_star (starrel``{x}) \<Longrightarrow> P) \<Longrightarrow> P"
   16.79 - apply (rule_tac x=z in Abs_star_cases)
   16.80 - apply (unfold star_def)
   16.81 - apply (erule quotientE)
   16.82 - apply simp
   16.83 -done
   16.84 -
   16.85 -
   16.86 -subsection {* Constructors for type @{typ "'a star"} *}
   16.87 -
   16.88 -constdefs
   16.89 -  star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
   16.90 -  "star_n X \<equiv> Abs_star (starrel `` {X})"
   16.91 -
   16.92 -  star_of :: "'a \<Rightarrow> 'a star"
   16.93 -  "star_of x \<equiv> star_n (\<lambda>n. x)"
   16.94 -
   16.95 -theorem star_cases [case_names star_n, cases type: star]:
   16.96 -  "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
   16.97 -by (unfold star_n_def, rule eq_Abs_star[of x], blast)
   16.98 -
   16.99 -lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))"
  16.100 -by (auto, rule_tac x=x in star_cases, simp)
  16.101 -
  16.102 -lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
  16.103 -by (auto, rule_tac x=x in star_cases, auto)
  16.104 -
  16.105 -lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)"
  16.106 - apply (unfold star_n_def)
  16.107 - apply (simp add: Abs_star_inject starrel_in_star equiv_starrel_iff)
  16.108 -done
  16.109 -
  16.110 -lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
  16.111 -by (simp add: star_of_def star_n_eq_iff)
  16.112 -
  16.113 -
  16.114 -subsection {* Internal functions *}
  16.115 -
  16.116 -constdefs
  16.117 -  Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
  16.118 -  "Ifun f \<equiv> \<lambda>x. Abs_star
  16.119 -       (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
  16.120 -
  16.121 -lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))"
  16.122 - apply (unfold Ifun_def star_n_def)
  16.123 - apply (simp add: Abs_star_inverse starrel_in_star)
  16.124 - apply (rule_tac f=Abs_star in arg_cong)
  16.125 - apply safe
  16.126 -  apply (erule ultra)+
  16.127 -  apply simp
  16.128 - apply force
  16.129 -done
  16.130 -
  16.131 -lemma Ifun [simp]: "star_of f \<star> star_of x = star_of (f x)"
  16.132 -by (simp only: star_of_def Ifun_star_n)
  16.133 -
  16.134 -
  16.135 -subsection {* Testing lifted booleans *}
  16.136 -
  16.137 -constdefs
  16.138 -  unstar :: "bool star \<Rightarrow> bool"
  16.139 -  "unstar b \<equiv> b = star_of True"
  16.140 -
  16.141 -lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
  16.142 -by (simp add: unstar_def star_of_def star_n_eq_iff)
  16.143 -
  16.144 -lemma unstar [simp]: "unstar (star_of p) = p"
  16.145 -by (simp add: unstar_def star_of_inject)
  16.146 -
  16.147 -
  16.148 -subsection {* Internal functions and predicates *}
  16.149 -
  16.150 -constdefs
  16.151 -  Ifun_of :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
  16.152 -  "Ifun_of f \<equiv> Ifun (star_of f)"
  16.153 -
  16.154 -  Ifun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
  16.155 -  "Ifun2 f \<equiv> \<lambda>x y. f \<star> x \<star> y"
  16.156 -
  16.157 -  Ifun2_of :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
  16.158 -  "Ifun2_of f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
  16.159 -
  16.160 -  Ipred :: "('a \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> bool)"
  16.161 -  "Ipred P \<equiv> \<lambda>x. unstar (P \<star> x)"
  16.162 -
  16.163 -  Ipred_of :: "('a \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> bool)"
  16.164 -  "Ipred_of P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
  16.165 -
  16.166 -  Ipred2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) star \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
  16.167 -  "Ipred2 P \<equiv> \<lambda>x y. unstar (P \<star> x \<star> y)"
  16.168 -
  16.169 -  Ipred2_of :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> bool)"
  16.170 -  "Ipred2_of P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
  16.171 -
  16.172 -lemmas Ifun_defs =
  16.173 -  Ifun_of_def Ifun2_def Ifun2_of_def
  16.174 -  Ipred_def Ipred_of_def Ipred2_def Ipred2_of_def
  16.175 -
  16.176 -lemma Ifun_of [simp]:
  16.177 -  "Ifun_of f (star_of x) = star_of (f x)"
  16.178 -by (simp only: Ifun_of_def Ifun)
  16.179 -
  16.180 -lemma Ifun2_of [simp]:
  16.181 -  "Ifun2_of f (star_of x) (star_of y) = star_of (f x y)"
  16.182 -by (simp only: Ifun2_of_def Ifun)
  16.183 -
  16.184 -lemma Ipred_of [simp]:
  16.185 -  "Ipred_of P (star_of x) = P x"
  16.186 -by (simp only: Ipred_of_def Ifun unstar)
  16.187 -
  16.188 -lemma Ipred2_of [simp]:
  16.189 -  "Ipred2_of P (star_of x) (star_of y) = P x y"
  16.190 -by (simp only: Ipred2_of_def Ifun unstar)
  16.191 -
  16.192 -
  16.193 -subsection {* Internal sets *}
  16.194 -
  16.195 -constdefs
  16.196 -  Iset :: "'a set star \<Rightarrow> 'a star set"
  16.197 -  "Iset A \<equiv> {x. Ipred2_of (op \<in>) x A}"
  16.198 -
  16.199 -  Iset_of :: "'a set \<Rightarrow> 'a star set"
  16.200 -  "Iset_of A \<equiv> Iset (star_of A)"
  16.201 -
  16.202 -lemma Iset_star_n:
  16.203 -  "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
  16.204 -by (simp add: Iset_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
  16.205 -
  16.206 -
  16.207 -
  16.208 -end
    17.1 --- a/src/HOL/Hyperreal/Transfer.thy	Thu Sep 15 23:16:04 2005 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,217 +0,0 @@
    17.4 -(*  Title       : HOL/Hyperreal/Transfer.thy
    17.5 -    ID          : $Id$
    17.6 -    Author      : Brian Huffman
    17.7 -*)
    17.8 -
    17.9 -header {* Transfer Principle *}
   17.10 -
   17.11 -theory Transfer
   17.12 -imports StarType
   17.13 -uses ("transfer.ML")
   17.14 -begin
   17.15 -
   17.16 -subsection {* Starting the transfer proof *}
   17.17 -
   17.18 -text {*
   17.19 -  A transfer theorem asserts an equivalence @{prop "P \<equiv> P'"}
   17.20 -  between two related propositions. Proposition @{term P} may
   17.21 -  refer to constants having star types, like @{typ "'a star"}.
   17.22 -  Proposition @{term P'} is syntactically similar, but only
   17.23 -  refers to ordinary types (i.e. @{term P'} is the un-starred
   17.24 -  version of @{term P}).
   17.25 -*}
   17.26 -
   17.27 -text {* This introduction rule starts each transfer proof. *}
   17.28 -
   17.29 -lemma transfer_start:
   17.30 -  "P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
   17.31 -by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq)
   17.32 -
   17.33 -use "transfer.ML"
   17.34 -setup Transfer.setup
   17.35 -
   17.36 -declare Ifun_defs [transfer_unfold]
   17.37 -declare Iset_of_def [transfer_unfold]
   17.38 -
   17.39 -subsection {* Transfer introduction rules *}
   17.40 -
   17.41 -text {*
   17.42 -  The proof of a transfer theorem is completely syntax-directed.
   17.43 -  At each step in the proof, the top-level connective determines
   17.44 -  which introduction rule to apply. Each argument to the top-level
   17.45 -  connective generates a new subgoal.
   17.46 -*}
   17.47 -
   17.48 -text {*
   17.49 -  Subgoals in a transfer proof always have the form of an equivalence.
   17.50 -  The left side can be any term, and may contain references to star
   17.51 -  types. The form of the right side depends on its type. At type
   17.52 -  @{typ bool} it takes the form @{term "{n. P n} \<in> \<U>"}. At type
   17.53 -  @{typ "'a star"} it takes the form @{term "star_n (\<lambda>n. X n)"}. At type
   17.54 -  @{typ "'a star set"} it looks like @{term "Iset (star_n (\<lambda>n. A n))"}.
   17.55 -  And at type @{typ "'a star \<Rightarrow> 'b star"} it has the form
   17.56 -  @{term "Ifun (star_n (\<lambda>n. F n))"}.
   17.57 -*}
   17.58 -
   17.59 -subsubsection {* Boolean operators *}
   17.60 -
   17.61 -lemma transfer_not:
   17.62 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>"
   17.63 -by (simp only: ultrafilter.Collect_not [OF ultrafilter_FUFNat])
   17.64 -
   17.65 -lemma transfer_conj:
   17.66 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   17.67 -    \<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>"
   17.68 -by (simp only: filter.Collect_conj [OF filter_FUFNat])
   17.69 -
   17.70 -lemma transfer_disj:
   17.71 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   17.72 -    \<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>"
   17.73 -by (simp only: ultrafilter.Collect_disj [OF ultrafilter_FUFNat])
   17.74 -
   17.75 -lemma transfer_imp:
   17.76 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   17.77 -    \<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>"
   17.78 -by (simp only: imp_conv_disj transfer_disj transfer_not)
   17.79 -
   17.80 -lemma transfer_iff:
   17.81 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk>
   17.82 -    \<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>"
   17.83 -by (simp only: iff_conv_conj_imp transfer_conj transfer_imp)
   17.84 -
   17.85 -lemma transfer_if_bool:
   17.86 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk>
   17.87 -    \<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>"
   17.88 -by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not)
   17.89 -
   17.90 -subsubsection {* Equals, If *}
   17.91 -
   17.92 -lemma transfer_eq:
   17.93 -  "\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>"
   17.94 -by (simp only: star_n_eq_iff)
   17.95 -
   17.96 -lemma transfer_if:
   17.97 -  "\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk>
   17.98 -    \<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)"
   17.99 -apply (rule eq_reflection)
  17.100 -apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra)
  17.101 -done
  17.102 -
  17.103 -subsubsection {* Quantifiers *}
  17.104 -
  17.105 -lemma transfer_ex:
  17.106 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.107 -    \<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>"
  17.108 -by (simp only: ex_star_eq filter.Collect_ex [OF filter_FUFNat])
  17.109 -
  17.110 -lemma transfer_all:
  17.111 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.112 -    \<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>"
  17.113 -by (simp only: all_star_eq ultrafilter.Collect_all [OF ultrafilter_FUFNat])
  17.114 -
  17.115 -lemma transfer_ex1:
  17.116 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.117 -    \<Longrightarrow> \<exists>!x. p x \<equiv> {n. \<exists>!x. P n x} \<in> \<U>"
  17.118 -by (simp only: Ex1_def transfer_ex transfer_conj
  17.119 -   transfer_all transfer_imp transfer_eq)
  17.120 -
  17.121 -subsubsection {* Functions *}
  17.122 -
  17.123 -lemma transfer_Ifun:
  17.124 -  "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk>
  17.125 -    \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
  17.126 -by (simp only: Ifun_star_n)
  17.127 -
  17.128 -lemma transfer_fun_eq:
  17.129 -  "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
  17.130 -    \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
  17.131 -      \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
  17.132 -by (simp only: expand_fun_eq transfer_all)
  17.133 -
  17.134 -subsubsection {* Sets *}
  17.135 -
  17.136 -lemma transfer_Iset:
  17.137 -  "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
  17.138 -by simp
  17.139 -
  17.140 -lemma transfer_Collect:
  17.141 -  "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.142 -    \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
  17.143 -by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
  17.144 -
  17.145 -lemma transfer_mem:
  17.146 -  "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
  17.147 -    \<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>"
  17.148 -by (simp only: Iset_star_n)
  17.149 -
  17.150 -lemma transfer_set_eq:
  17.151 -  "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
  17.152 -    \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
  17.153 -by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
  17.154 -
  17.155 -lemma transfer_ball:
  17.156 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.157 -    \<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>"
  17.158 -by (simp only: Ball_def transfer_all transfer_imp transfer_mem)
  17.159 -
  17.160 -lemma transfer_bex:
  17.161 -  "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
  17.162 -    \<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>"
  17.163 -by (simp only: Bex_def transfer_ex transfer_conj transfer_mem)
  17.164 -
  17.165 -
  17.166 -subsubsection {* Miscellaneous *}
  17.167 -
  17.168 -lemma transfer_unstar:
  17.169 -  "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
  17.170 -by (simp only: unstar_star_n)
  17.171 -
  17.172 -lemma transfer_star_of: "star_of x \<equiv> star_n (\<lambda>n. x)"
  17.173 -by (rule star_of_def)
  17.174 -
  17.175 -lemma transfer_star_n: "star_n X \<equiv> star_n (\<lambda>n. X n)"
  17.176 -by (rule reflexive)
  17.177 -
  17.178 -lemma transfer_bool: "p \<equiv> {n. p} \<in> \<U>"
  17.179 -by (simp add: atomize_eq)
  17.180 -
  17.181 -lemmas transfer_intros [transfer_intro] =
  17.182 -  transfer_star_n
  17.183 -  transfer_star_of
  17.184 -  transfer_Ifun
  17.185 -  transfer_fun_eq
  17.186 -
  17.187 -  transfer_not
  17.188 -  transfer_conj
  17.189 -  transfer_disj
  17.190 -  transfer_imp
  17.191 -  transfer_iff
  17.192 -  transfer_if_bool
  17.193 -
  17.194 -  transfer_all
  17.195 -  transfer_ex
  17.196 -
  17.197 -  transfer_unstar
  17.198 -  transfer_bool
  17.199 -  transfer_eq
  17.200 -  transfer_if
  17.201 -
  17.202 -  transfer_set_eq
  17.203 -  transfer_Iset
  17.204 -  transfer_Collect
  17.205 -  transfer_mem
  17.206 -  transfer_ball
  17.207 -  transfer_bex
  17.208 -
  17.209 -text {* Sample theorems *}
  17.210 -
  17.211 -lemma Ifun_inject: "\<And>f g. (Ifun f = Ifun g) = (f = g)"
  17.212 -by transfer (rule refl)
  17.213 -
  17.214 -lemma unstar_inject: "\<And>x y. (unstar x = unstar y) = (x = y)"
  17.215 -by transfer (rule refl)
  17.216 -
  17.217 -lemma Iset_inject: "\<And>A B. (Iset A = Iset B) = (A = B)"
  17.218 -by transfer (rule refl)
  17.219 -
  17.220 -end
    18.1 --- a/src/HOL/Hyperreal/fuf.ML	Thu Sep 15 23:16:04 2005 +0200
    18.2 +++ b/src/HOL/Hyperreal/fuf.ML	Thu Sep 15 23:46:22 2005 +0200
    18.3 @@ -22,10 +22,10 @@
    18.4  |   get_fuf_hyps (x::xs) zs =
    18.5          case (concl_of x) of
    18.6          (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
    18.7 -             Const ("StarType.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
    18.8 +             Const ("StarDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
    18.9                                                ((x RS FreeUltrafilterNat_Compl_mem)::zs)
   18.10         |(_ $ (Const ("op :",_) $ _ $
   18.11 -             Const ("StarType.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
   18.12 +             Const ("StarDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
   18.13         | _ => get_fuf_hyps xs zs;
   18.14  
   18.15  fun inter_prems [] = raise FUFempty
    19.1 --- a/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:16:04 2005 +0200
    19.2 +++ b/src/HOL/Hyperreal/transfer.ML	Thu Sep 15 23:46:22 2005 +0200
    19.3 @@ -8,17 +8,13 @@
    19.4  signature TRANSFER_TAC =
    19.5  sig
    19.6    val transfer_tac: thm list -> int -> tactic
    19.7 +  val add_const: string -> theory -> theory
    19.8    val setup: (theory -> theory) list
    19.9  end;
   19.10  
   19.11  structure Transfer: TRANSFER_TAC =
   19.12  struct
   19.13  
   19.14 -(* TODO: make this list extensible *)
   19.15 -val star_consts =
   19.16 -  [ "StarType.star_of", "StarType.Ifun"
   19.17 -  , "StarType.unstar", "StarType.Iset" ]
   19.18 -
   19.19  structure TransferData = TheoryDataFun
   19.20  (struct
   19.21    val name = "HOL/transfer";
   19.22 @@ -28,7 +24,7 @@
   19.23      refolds: thm list,
   19.24      consts: string list
   19.25    };
   19.26 -  val empty = {intros = [], unfolds = [], refolds = [], consts = star_consts};
   19.27 +  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
   19.28    val copy = I;
   19.29    val extend = I;
   19.30    fun merge _
   19.31 @@ -45,7 +41,7 @@
   19.32  
   19.33  val transfer_start = thm "transfer_start"
   19.34  
   19.35 -fun unstar_typ (Type ("StarType.star",[t])) = unstar_typ t
   19.36 +fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
   19.37    | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
   19.38    | unstar_typ T = T
   19.39  
   19.40 @@ -102,10 +98,6 @@
   19.41  fun map_refolds f = TransferData.map
   19.42    (fn {intros,unfolds,refolds,consts} =>
   19.43      {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
   19.44 -
   19.45 -fun map_consts f = TransferData.map
   19.46 -  (fn {intros,unfolds,refolds,consts} =>
   19.47 -    {intros=intros, unfolds=unfolds, refolds=refolds, consts=f consts})
   19.48  in
   19.49  fun intro_add_global (thy, thm) = (map_intros (Drule.add_rule thm) thy, thm);
   19.50  fun intro_del_global (thy, thm) = (map_intros (Drule.del_rule thm) thy, thm);
   19.51 @@ -117,6 +109,10 @@
   19.52  fun refold_del_global (thy, thm) = (map_refolds (Drule.del_rule thm) thy, thm);
   19.53  end
   19.54  
   19.55 +fun add_const c = TransferData.map
   19.56 +  (fn {intros,unfolds,refolds,consts} =>
   19.57 +    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})
   19.58 +
   19.59  local
   19.60    val undef_local =
   19.61      Attrib.add_del_args