merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
--- 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)"
--- 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)
--- 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)
--- 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)
--- 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"
--- 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)
--- 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";
--- 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";
--- 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)
--- 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
--- 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)
--- 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
--- 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)
--- 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
--- /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
--- 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
--- 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
--- 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
--- 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