--- a/src/HOL/Complex/NSComplex.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed Sep 07 00:48:50 2005 +0200
@@ -127,7 +127,7 @@
(* hypernatural powers of nonstandard complex numbers *)
hcpow_def:
"(z::hcomplex) hcpow (n::hypnat)
- == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
+ == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_star(n).
hcomplexrel `` {%n. (X n) ^ (Y n)})"
@@ -817,7 +817,7 @@
lemma hcpow:
"Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
- Abs_hypnat(hypnatrel``{%n. Y n}) =
+ Abs_star(starrel``{%n. Y n}) =
Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
apply (simp add: hcpow_def)
apply (rule_tac f = Abs_hcomplex in arg_cong)
@@ -826,12 +826,12 @@
lemma hcomplex_of_hypreal_hyperpow:
"hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (rule_tac z=x in eq_Abs_star, cases n)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
done
lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
-apply (cases x, cases n)
+apply (cases x, rule_tac z=n in eq_Abs_star)
apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
done
@@ -882,18 +882,18 @@
lemma hcpow_minus:
"(-x::hcomplex) hcpow n =
(if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
-apply (cases x, cases n)
+apply (cases x, rule_tac z=n in eq_Abs_star)
apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
apply (auto simp add: neg_power_if, ultra)
done
lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-apply (cases r, cases s, cases n)
+apply (cases r, cases s, rule_tac z=n in eq_Abs_star)
apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
done
lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
-apply (simp add: hcomplex_zero_def hypnat_one_def, cases n)
+apply (simp add: hcomplex_zero_def hypnat_one_def, rule_tac z=n in eq_Abs_star)
apply (simp add: hcpow hypnat_add)
done
@@ -901,7 +901,7 @@
by (simp add: hSuc_def)
lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
-apply (cases r, cases n)
+apply (cases r, rule_tac z=n in eq_Abs_star)
apply (auto simp add: hcpow hcomplex_zero_def, ultra)
done
@@ -1194,12 +1194,12 @@
lemma hcis_hypreal_of_hypnat_Suc_mult:
"hcis (hypreal_of_hypnat (n + 1) * a) =
hcis a * hcis (hypreal_of_hypnat n * a)"
-apply (rule_tac z=a in eq_Abs_star, cases n)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
done
lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-apply (rule_tac z=a in eq_Abs_star, cases n)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
done
--- a/src/HOL/Hyperreal/HSeries.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Wed Sep 07 00:48:50 2005 +0200
@@ -14,7 +14,7 @@
constdefs
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
"sumhr p ==
- (%(M,N,f). Abs_star(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).
+ (%(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"
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80)
@@ -28,8 +28,8 @@
lemma sumhr:
- "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),
- Abs_hypnat(hypnatrel``{%n. N n}), f) =
+ "sumhr(Abs_star(starrel``{%n. M n}),
+ Abs_star(starrel``{%n. N n}), f) =
Abs_star(starrel `` {%n. setsum f {M n..<N n}})"
apply (simp add: sumhr_def)
apply (rule arg_cong [where f = Abs_star])
@@ -38,7 +38,7 @@
text{*Base case in definition of @{term sumr}*}
lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (cases m)
+apply (rule_tac z=m in eq_Abs_star)
apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
done
@@ -46,43 +46,43 @@
lemma sumhr_if:
"sumhr(m,n+1,f) =
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
hypreal_add hypreal_zero_def, ultra+)
done
lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
done
lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypreal_zero_def)
done
lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
-apply (cases m)
+apply (rule_tac z=m in eq_Abs_star)
apply (simp add: sumhr hypnat_one_def hypnat_add starfunNat)
done
lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (cases m, cases k)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=k in eq_Abs_star)
apply (simp add: sumhr hypnat_add hypreal_zero_def)
done
lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypreal_add setsum_addf)
done
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypreal_of_real_def star_of_def star_n_def hypreal_mult setsum_mult)
done
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (cases n, cases p)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=p in eq_Abs_star)
apply (auto elim!: FreeUltrafilterNat_subset simp
add: hypnat_zero_def sumhr hypreal_add hypnat_less setsum_add_nat_ivl)
done
@@ -91,7 +91,7 @@
by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (cases n, cases m)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=m in eq_Abs_star)
apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs)
done
@@ -105,26 +105,26 @@
lemma sumhr_const:
"sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat
star_of_def star_n_def
hypreal_mult real_of_nat_def)
done
lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (auto elim: FreeUltrafilterNat_subset
simp add: sumhr hypnat_less hypreal_zero_def)
done
lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypreal_minus setsum_negf)
done
lemma sumhr_shift_bounds:
"sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: sumhr hypnat_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
done
@@ -156,7 +156,7 @@
real_of_nat_def star_of_def star_n_def hypreal_mult cong: setsum_ivl_cong)
lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
apply (simp add: hypnat_zero_def starfunNat sumhr)
done
--- a/src/HOL/Hyperreal/HTranscendental.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Wed Sep 07 00:48:50 2005 +0200
@@ -266,10 +266,8 @@
lemma coshr_zero [simp]: "coshr 0 = 1"
apply (simp add: coshr_def sumhr_split_add
[OF hypnat_one_less_hypnat_omega, symmetric])
-apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def
- hypnat_add hypnat_omega_def st_add [symmetric]
- hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
- del: hypnat_add_zero_left)
+apply (simp add: sumhr hypnat_zero_def hypnat_one_def hypnat_omega_def)
+apply (simp add: hypreal_one_def [symmetric] hypreal_zero_def [symmetric])
done
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
@@ -301,6 +299,7 @@
apply (rule st_hypreal_of_real [THEN subst])
apply (rule approx_st_eq, auto)
apply (rule approx_minus_iff [THEN iffD2])
+apply (simp only: mem_infmal_iff [symmetric])
apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
apply (insert exp_converges [of x])
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Wed Sep 07 00:48:50 2005 +0200
@@ -11,6 +11,8 @@
imports Star
begin
+types hypnat = "nat star"
+(*
constdefs
hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
"hypnatrel == {p. \<exists>X Y. p = ((X::nat=>nat),Y) &
@@ -20,20 +22,26 @@
by (auto simp add: quotient_def)
instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
-
+*)
consts whn :: hypnat
-defs (overloaded)
+defs
+ (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+ hypnat_omega_def: "whn == Abs_star(starrel``{%n::nat. n})"
+
+lemma hypnat_zero_def: "0 == Abs_star(starrel``{%n::nat. 0})"
+by (simp only: star_zero_def star_of_def star_n_def)
+
+lemma hypnat_one_def: "1 == Abs_star(starrel``{%n::nat. 1})"
+by (simp only: star_one_def star_of_def star_n_def)
(** hypernatural arithmetic **)
-
+(*
hypnat_zero_def: "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
hypnat_one_def: "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
-
- (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
- hypnat_omega_def: "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
-
+*)
+(*
hypnat_add_def:
"P + Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
hypnatrel``{%n::nat. X n + Y n})"
@@ -45,15 +53,9 @@
hypnat_minus_def:
"P - Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
hypnatrel``{%n::nat. X n - Y n})"
-
- hypnat_le_def:
- "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) & Y \<in> Rep_hypnat(Q) &
- {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
+*)
- hypnat_less_def: "(x < (y::hypnat)) == (x \<le> y & x \<noteq> y)"
-
-
-
+(*
subsection{*Properties of @{term hypnatrel}*}
text{*Proving that @{term hypnatrel} is an equivalence relation*}
@@ -78,8 +80,9 @@
apply (simp add: equiv_def refl_def sym_def trans_def hypnatrel_refl)
apply (blast intro: hypnatrel_sym hypnatrel_trans)
done
-
+*)
(* (hypnatrel `` {x} = hypnatrel `` {y}) = ((x,y) \<in> hypnatrel) *)
+(*
lemmas equiv_hypnatrel_iff =
eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
@@ -118,156 +121,124 @@
theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
"(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
by (rule eq_Abs_hypnat [of z], blast)
-
+*)
subsection{*Hypernat Addition*}
-
+(*
lemma hypnat_add_congruent2:
"(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
-
+*)
lemma hypnat_add:
- "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
- Abs_hypnat(hypnatrel``{%n. X n + Y n})"
-by (simp add: hypnat_add_def
- UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_add_congruent2])
+ "Abs_star(starrel``{%n. X n}) + Abs_star(starrel``{%n. Y n}) =
+ Abs_star(starrel``{%n. X n + Y n})"
+by (rule hypreal_add)
lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
-apply (cases z, cases w)
-apply (simp add: add_ac hypnat_add)
-done
+by (rule add_commute)
lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypnat_add nat_add_assoc)
-done
+by (rule add_assoc)
lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
-apply (cases z)
-apply (simp add: hypnat_zero_def hypnat_add)
-done
+by (rule comm_monoid_add_class.add_0)
+(*
instance hypnat :: comm_monoid_add
by intro_classes
(assumption |
rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
-
+*)
subsection{*Subtraction inverse on @{typ hypreal}*}
-
+(*
lemma hypnat_minus_congruent2:
- "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
+ "(%X Y. starrel``{%n. X n - Y n}) respects2 starrel"
by (simp add: congruent2_def, auto, ultra)
-
+*)
lemma hypnat_minus:
- "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
- Abs_hypnat(hypnatrel``{%n. X n - Y n})"
-by (simp add: hypnat_minus_def
- UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_minus_congruent2])
+ "Abs_star(starrel``{%n. X n}) - Abs_star(starrel``{%n. Y n}) =
+ Abs_star(starrel``{%n. X n - Y n})"
+by (rule hypreal_diff)
-lemma hypnat_minus_zero: "z - z = (0::hypnat)"
-apply (cases z)
-apply (simp add: hypnat_zero_def hypnat_minus)
-done
+lemma hypnat_minus_zero: "!!z. z - z = (0::hypnat)"
+by transfer (rule diff_self_eq_0)
-lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
-apply (cases n)
-apply (simp add: hypnat_minus hypnat_zero_def)
-done
+lemma hypnat_diff_0_eq_0: "!!n. (0::hypnat) - n = 0"
+by transfer (rule diff_0_eq_0)
declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
-lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
-apply (cases m, cases n)
-apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
-done
+lemma hypnat_add_is_0: "!!m n. (m+n = (0::hypnat)) = (m=0 & n=0)"
+by transfer (rule add_is_0)
declare hypnat_add_is_0 [iff]
-lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
-apply (cases i, cases j, cases k)
-apply (simp add: hypnat_minus hypnat_add diff_diff_left)
-done
+lemma hypnat_diff_diff_left: "!!i j k. (i::hypnat) - j - k = i - (j+k)"
+by transfer (rule diff_diff_left)
-lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
-by (simp add: hypnat_diff_diff_left hypnat_add_commute)
+lemma hypnat_diff_commute: "!!i j k. (i::hypnat) - j - k = i-k-j"
+by transfer (rule diff_commute)
-lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_inverse: "!!m n. ((n::hypnat) + m) - n = m"
+by transfer (rule diff_add_inverse)
declare hypnat_diff_add_inverse [simp]
-lemma hypnat_diff_add_inverse2: "((m::hypnat) + n) - n = m"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_inverse2: "!!m n. ((m::hypnat) + n) - n = m"
+by transfer (rule diff_add_inverse2)
declare hypnat_diff_add_inverse2 [simp]
-lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
-apply (cases k, cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_cancel: "!!k m n. ((k::hypnat) + m) - (k+n) = m - n"
+by transfer (rule diff_cancel)
declare hypnat_diff_cancel [simp]
-lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
-by (simp add: hypnat_add_commute [of _ k])
+lemma hypnat_diff_cancel2: "!!k m n. ((m::hypnat) + k) - (n+k) = m - n"
+by transfer (rule diff_cancel2)
declare hypnat_diff_cancel2 [simp]
-lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
-apply (cases m, cases n)
-apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_0: "!!m n. (n::hypnat) - (n+m) = (0::hypnat)"
+by transfer (rule diff_add_0)
declare hypnat_diff_add_0 [simp]
subsection{*Hyperreal Multiplication*}
-
+(*
lemma hypnat_mult_congruent2:
- "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
+ "(%X Y. starrel``{%n. X n * Y n}) respects2 starrel"
by (simp add: congruent2_def, auto, ultra)
-
+*)
lemma hypnat_mult:
- "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
- Abs_hypnat(hypnatrel``{%n. X n * Y n})"
-by (simp add: hypnat_mult_def
- UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_mult_congruent2])
+ "Abs_star(starrel``{%n. X n}) * Abs_star(starrel``{%n. Y n}) =
+ Abs_star(starrel``{%n. X n * Y n})"
+by (rule hypreal_mult)
lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-by (cases z, cases w, simp add: hypnat_mult mult_ac)
+by (rule mult_commute)
lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypnat_mult mult_assoc)
-done
+by (rule mult_assoc)
lemma hypnat_mult_1: "(1::hypnat) * z = z"
-apply (cases z)
-apply (simp add: hypnat_mult hypnat_one_def)
-done
+by (rule mult_1_left)
-lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
-apply (cases k, cases m, cases n)
-apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
-done
+lemma hypnat_diff_mult_distrib: "!!k m n. ((m::hypnat) - n) * k = (m * k) - (n * k)"
+by transfer (rule diff_mult_distrib)
-lemma hypnat_diff_mult_distrib2: "(k::hypnat) * (m - n) = (k * m) - (k * n)"
-by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
+lemma hypnat_diff_mult_distrib2: "!!k m n. (k::hypnat) * (m - n) = (k * m) - (k * n)"
+by transfer (rule diff_mult_distrib2)
lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
-apply (cases z1, cases z2, cases w)
-apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
-done
+by (rule left_distrib)
lemma hypnat_add_mult_distrib2: "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)"
-by (simp add: hypnat_mult_commute [of w] hypnat_add_mult_distrib)
+by (rule right_distrib)
text{*one and zero are distinct*}
lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)"
-by (auto simp add: hypnat_zero_def hypnat_one_def)
+by (rule zero_neq_one)
declare hypnat_zero_not_eq_one [THEN not_sym, simp]
-
+(*
text{*The hypernaturals form a @{text comm_semiring_1_cancel}: *}
instance hypnat :: comm_semiring_1_cancel
proof
@@ -281,64 +252,50 @@
hence "(k+i) - k = (k+j) - k" by simp
thus "i=j" by simp
qed
-
+*)
subsection{*Properties of The @{text "\<le>"} Relation*}
lemma hypnat_le:
- "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
+ "(Abs_star(starrel``{%n. X n}) \<le> Abs_star(starrel``{%n. Y n})) =
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (simp add: hypnat_le_def)
-apply (auto intro!: lemma_hypnatrel_refl, ultra)
-done
+by (rule hypreal_le)
lemma hypnat_le_refl: "w \<le> (w::hypnat)"
-apply (cases w)
-apply (simp add: hypnat_le)
-done
+by (rule order_refl)
lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
-apply (cases i, cases j, cases k)
-apply (simp add: hypnat_le, ultra)
-done
+by (rule order_trans)
lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
-apply (cases z, cases w)
-apply (simp add: hypnat_le, ultra)
-done
+by (rule order_antisym)
(* Axiom 'order_less_le' of class 'order': *)
lemma hypnat_less_le: "((w::hypnat) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: hypnat_less_def)
+by (rule order_less_le)
+(*
instance hypnat :: order
by intro_classes
(assumption |
rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
-
+*)
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
-apply (cases z, cases w)
-apply (auto simp add: hypnat_le, ultra)
-done
-
+by (rule linorder_linear)
+(*
instance hypnat :: linorder
by intro_classes (rule hypnat_le_linear)
-
+*)
lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypnat_le hypnat_add)
-done
+by (rule add_left_mono)
lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
-apply (cases x, cases y, cases z)
-apply (simp add: hypnat_zero_def hypnat_mult linorder_not_le [symmetric])
-apply (auto simp add: hypnat_le, ultra)
-done
+by (rule mult_strict_left_mono)
subsection{*The Hypernaturals Form an Ordered @{text comm_semiring_1_cancel} *}
-
+(*
instance hypnat :: ordered_semidom
proof
fix x y z :: hypnat
@@ -350,62 +307,48 @@
show "x < y ==> 0 < z ==> z * x < z * y"
by (simp add: hypnat_mult_less_mono2)
qed
-
-lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
-apply (cases n)
-apply (simp add: hypnat_zero_def hypnat_le)
-done
+*)
+lemma hypnat_le_zero_cancel [iff]: "!!n. (n \<le> (0::hypnat)) = (n = 0)"
+by transfer (rule le_0_eq)
-lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
-apply (cases m, cases n)
-apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
-done
+lemma hypnat_mult_is_0 [simp]: "!!m n. (m*n = (0::hypnat)) = (m=0 | n=0)"
+by transfer (rule mult_is_0)
-lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
-apply (cases m, cases n)
-apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
-done
+lemma hypnat_diff_is_0_eq [simp]: "!!m n. ((m::hypnat) - n = 0) = (m \<le> n)"
+by transfer (rule diff_is_0_eq)
subsection{*Theorems for Ordering*}
lemma hypnat_less:
- "(Abs_hypnat(hypnatrel``{%n. X n}) < Abs_hypnat(hypnatrel``{%n. Y n})) =
+ "(Abs_star(starrel``{%n. X n}) < Abs_star(starrel``{%n. Y n})) =
({n. X n < Y n} \<in> FreeUltrafilterNat)"
-apply (auto simp add: hypnat_le linorder_not_le [symmetric])
-apply (ultra+)
-done
+by (rule hypreal_less)
-lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
-apply (cases n)
-apply (auto simp add: hypnat_zero_def hypnat_less)
-done
+lemma hypnat_not_less0 [iff]: "!!n. ~ n < (0::hypnat)"
+by transfer (rule not_less0)
lemma hypnat_less_one [iff]:
- "(n < (1::hypnat)) = (n=0)"
-apply (cases n)
-apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
-done
+ "!!n. (n < (1::hypnat)) = (n=0)"
+by transfer (rule less_one)
+
+lemma hypnat_add_diff_inverse: "!!m n. ~ m<n ==> n+(m-n) = (m::hypnat)"
+by transfer (rule add_diff_inverse)
-lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
-done
+lemma hypnat_le_add_diff_inverse [simp]: "!!m n. n \<le> m ==> n+(m-n) = (m::hypnat)"
+by transfer (rule le_add_diff_inverse)
-lemma hypnat_le_add_diff_inverse [simp]: "n \<le> m ==> n+(m-n) = (m::hypnat)"
-by (simp add: hypnat_add_diff_inverse linorder_not_less [symmetric])
-
-lemma hypnat_le_add_diff_inverse2 [simp]: "n\<le>m ==> (m-n)+n = (m::hypnat)"
-by (simp add: hypnat_le_add_diff_inverse hypnat_add_commute)
+lemma hypnat_le_add_diff_inverse2 [simp]: "!!m n. n\<le>m ==> (m-n)+n = (m::hypnat)"
+by transfer (rule le_add_diff_inverse2)
declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]
-lemma hypnat_le0 [iff]: "(0::hypnat) \<le> n"
-by (simp add: linorder_not_less [symmetric])
+lemma hypnat_le0 [iff]: "!!n. (0::hypnat) \<le> n"
+by transfer (rule le0)
-lemma hypnat_add_self_le [simp]: "(x::hypnat) \<le> n + x"
-by (insert add_right_mono [of 0 n x], simp)
+lemma hypnat_add_self_le [simp]: "!!x n. (x::hypnat) \<le> n + x"
+by transfer (rule le_add2)
lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
by (insert add_strict_left_mono [OF zero_less_one], auto)
@@ -494,10 +437,10 @@
subsection{*Existence of an infinite hypernatural number*}
-lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
+lemma hypnat_omega: "starrel``{%n::nat. n} \<in> star"
by auto
-lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"
+lemma Rep_star_omega: "Rep_star(whn) \<in> star"
by (simp add: hypnat_omega_def)
text{*Existence of infinite number not corresponding to any natural number
@@ -530,7 +473,7 @@
lemma hypnat_of_nat_eq:
- "hypnat_of_nat m = Abs_hypnat(hypnatrel``{%n::nat. m})"
+ "hypnat_of_nat m = Abs_star(starrel``{%n::nat. m})"
apply (induct m)
apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add)
done
@@ -540,13 +483,7 @@
lemma hypnat_omega_gt_SHNat:
"n \<in> Nats ==> n < whn"
-apply (auto simp add: hypnat_of_nat_eq hypnat_less_def hypnat_le_def
- hypnat_omega_def SHNat_eq)
- prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
-apply (auto intro!: exI)
-apply (rule cofinite_mem_FreeUltrafilterNat)
-apply (simp add: Compl_Collect_le finite_nat_segment)
-done
+by (auto simp add: hypnat_of_nat_eq hypnat_less hypnat_omega_def SHNat_eq)
(* Infinite hypernatural not in embedded Nats *)
lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
@@ -595,7 +532,7 @@
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
simp add: hypnat_less FreeUltrafilterNat_Compl_iff1
Collect_neg_eq [symmetric])
@@ -607,24 +544,24 @@
lemma HNatInfinite_FreeUltrafilterNat:
"x \<in> HNatInfinite
- ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
-apply (cases x)
+ ==> \<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat"
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify)
+apply (rule bexI [OF _ lemma_starrel_refl], clarify)
apply (auto simp add: hypnat_of_nat_def hypnat_less)
done
lemma FreeUltrafilterNat_HNatInfinite:
- "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
+ "\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat
==> x \<in> HNatInfinite"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
apply (drule spec, ultra, auto)
done
lemma HNatInfinite_FreeUltrafilterNat_iff:
"(x \<in> HNatInfinite) =
- (\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}: FreeUltrafilterNat)"
+ (\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}: FreeUltrafilterNat)"
by (blast intro: HNatInfinite_FreeUltrafilterNat
FreeUltrafilterNat_HNatInfinite)
@@ -692,7 +629,7 @@
constdefs
hypreal_of_hypnat :: "hypnat => hypreal"
"hypreal_of_hypnat N ==
- Abs_star(\<Union>X \<in> Rep_hypnat(N). starrel``{%n::nat. real (X n)})"
+ Abs_star(\<Union>X \<in> Rep_star(N). starrel``{%n::nat. real (X n)})"
lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
@@ -704,7 +641,7 @@
by force
lemma hypreal_of_hypnat:
- "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
+ "hypreal_of_hypnat (Abs_star(starrel``{%n. X n})) =
Abs_star(starrel `` {%n. real (X n)})"
apply (simp add: hypreal_of_hypnat_def)
apply (rule_tac f = Abs_star in arg_cong)
@@ -714,7 +651,7 @@
lemma hypreal_of_hypnat_inject [simp]:
"(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypreal_of_hypnat)
done
@@ -726,19 +663,19 @@
lemma hypreal_of_hypnat_add [simp]:
"hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
done
lemma hypreal_of_hypnat_mult [simp]:
"hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
done
lemma hypreal_of_hypnat_less_iff [simp]:
"(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
done
@@ -747,13 +684,13 @@
declare hypreal_of_hypnat_eq_zero_iff [simp]
lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
done
lemma HNatInfinite_inverse_Infinitesimal [simp]:
"n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypreal_of_hypnat hypreal_inverse
HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
@@ -776,17 +713,17 @@
val hypnat_one_def = thm"hypnat_one_def";
val hypnat_omega_def = thm"hypnat_omega_def";
-val hypnatrel_iff = thm "hypnatrel_iff";
-val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
-val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
-val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
-val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
-val eq_Abs_hypnat = thm "eq_Abs_hypnat";
+val starrel_iff = thm "starrel_iff";
+(* val starrel_in_hypnat = thm "starrel_in_hypnat"; *)
+val lemma_starrel_refl = thm "lemma_starrel_refl";
+(* val hypnat_empty_not_mem = thm "hypnat_empty_not_mem"; *)
+(* val Rep_star_nonempty = thm "Rep_star_nonempty"; *)
+val eq_Abs_star = thm "eq_Abs_star";
val hypnat_add = thm "hypnat_add";
val hypnat_add_commute = thm "hypnat_add_commute";
val hypnat_add_assoc = thm "hypnat_add_assoc";
val hypnat_add_zero_left = thm "hypnat_add_zero_left";
-val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2";
+(* val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2"; *)
val hypnat_minus = thm "hypnat_minus";
val hypnat_minus_zero = thm "hypnat_minus_zero";
val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
@@ -798,7 +735,7 @@
val hypnat_diff_cancel = thm "hypnat_diff_cancel";
val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
-val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2";
+(* val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2"; *)
val hypnat_mult = thm "hypnat_mult";
val hypnat_mult_commute = thm "hypnat_mult_commute";
val hypnat_mult_assoc = thm "hypnat_mult_assoc";
@@ -841,7 +778,7 @@
val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
val hypnat_omega = thm "hypnat_omega";
-val Rep_hypnat_omega = thm "Rep_hypnat_omega";
+val Rep_star_omega = thm "Rep_star_omega";
val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
--- a/src/HOL/Hyperreal/HyperPow.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Wed Sep 07 00:48:50 2005 +0200
@@ -41,7 +41,7 @@
(* hypernatural powers of hyperreals *)
hyperpow_def:
"(R::hypreal) pow (N::hypnat) ==
- Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_hypnat(N).
+ Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_star(N).
starrel``{%n::nat. (X n) ^ (Y n)})"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
@@ -125,7 +125,7 @@
by (auto simp add: congruent_def intro!: ext, fuf+)
lemma hyperpow:
- "Abs_star(starrel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
+ "Abs_star(starrel``{%n. X n}) pow Abs_star(starrel``{%n. Y n}) =
Abs_star(starrel``{%n. X n ^ Y n})"
apply (unfold hyperpow_def)
apply (rule_tac f = Abs_star in arg_cong)
@@ -137,33 +137,33 @@
lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
apply (unfold hypnat_one_def)
apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
apply (auto simp add: hyperpow hypnat_add)
done
declare hyperpow_zero [simp]
lemma hyperpow_not_zero [rule_format (no_asm)]:
"r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow)
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
lemma hyperpow_inverse:
"r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
apply (rule FreeUltrafilterNat_subset)
apply (auto dest: realpow_not_zero intro: power_inverse)
done
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (cases n, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
done
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (cases n, cases m, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=m in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
done
@@ -179,38 +179,38 @@
done
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
simp add: hyperpow hypreal_less hypreal_le)
done
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
simp add: hyperpow hypreal_le)
done
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_le hypreal_less)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
apply (auto intro: power_mono)
done
lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypreal_one_def hyperpow)
done
lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)"
apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
apply simp
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
done
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (cases n, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
done
@@ -247,14 +247,14 @@
"-1 pow ((1 + 1)*n) = (1::hypreal)"
apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
apply simp
-apply (simp only: hypreal_one_def, cases n)
+apply (simp only: hypreal_one_def, rule_tac z=n in eq_Abs_star)
apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
- left_distrib)
+ hypnat_mult left_distrib)
done
lemma hyperpow_less_le:
"[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (cases n, cases N, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=N in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
hypreal_zero_def hypreal_one_def)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
--- a/src/HOL/Hyperreal/NatStar.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Wed Sep 07 00:48:50 2005 +0200
@@ -20,11 +20,11 @@
starsetNat :: "nat set => hypnat set" ("*sNat* _" [80] 80)
"*sNat* A ==
- {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
+ {x. \<forall>X\<in>Rep_star(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
starsetNat_n :: "(nat => nat set) => hypnat set" ("*sNatn* _" [80] 80)
"*sNatn* As ==
- {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
+ {x. \<forall>X\<in>Rep_star(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
InternalNatSets :: "hypnat set set"
"InternalNatSets == {X. \<exists>As. X = *sNatn* As}"
@@ -33,12 +33,12 @@
starfunNat :: "(nat => real) => hypnat => hypreal"
("*fNat* _" [80] 80)
- "*fNat* f == (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. f (X n)}))"
+ "*fNat* f == (%x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. f (X n)}))"
starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
("*fNatn* _" [80] 80)
"*fNatn* F ==
- (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. (F n)(X n)}))"
+ (%x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. (F n)(X n)}))"
InternalNatFuns :: "(hypnat => hypreal) set"
"InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
@@ -47,12 +47,12 @@
starfunNat2 :: "(nat => nat) => hypnat => hypnat"
("*fNat2* _" [80] 80)
- "*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})"
+ "*fNat2* f == %x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. f (X n)})"
starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat"
("*fNat2n* _" [80] 80)
"*fNat2n* F ==
- %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})"
+ %x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. (F n)(X n)})"
InternalNatFuns2 :: "(hypnat => hypnat) set"
"InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}"
@@ -70,13 +70,13 @@
prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
apply (drule FreeUltrafilterNat_Compl_mem)
apply (drule bspec, assumption)
-apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra)
+apply (rule_tac z = x in eq_Abs_star, auto, ultra)
done
lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B"
apply (auto simp add: starsetNat_n_def)
apply (drule_tac x = Xa in bspec)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_star)
apply (auto dest!: bspec, ultra+)
done
@@ -104,15 +104,15 @@
lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)"
apply (auto simp add: starsetNat_def)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac [2] z = x in eq_Abs_star)
apply (auto dest!: bspec, ultra+)
done
lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)"
apply (auto simp add: starsetNat_n_def)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac [2] z = x in eq_Abs_star)
apply (auto dest!: bspec, ultra+)
done
@@ -121,8 +121,8 @@
lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"
apply (auto simp add: starsetNat_n_def)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
-apply (rule_tac [3] z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_star)
+apply (rule_tac [3] z = x in eq_Abs_star)
apply (auto dest!: bspec, ultra+)
done
@@ -154,7 +154,7 @@
apply (simp add: hypnat_of_nat_eq [symmetric])
apply (rule imageI, rule ccontr)
apply (drule bspec)
-apply (rule lemma_hypnatrel_refl)
+apply (rule lemma_starrel_refl)
prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
done
@@ -186,14 +186,14 @@
lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
by (simp add: starfunNat2_n_def starfunNat2_def)
-lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel"
+lemma starfunNat_congruent: "(%X. starrel``{%n. f (X n)}) respects starrel"
apply (simp add: congruent_def, safe)
apply (ultra+)
done
(* f::nat=>real *)
lemma starfunNat:
- "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+ "( *fNat* f) (Abs_star(starrel``{%n. X n})) =
Abs_star(starrel `` {%n. f (X n)})"
apply (simp add: starfunNat_def)
apply (rule arg_cong [where f = Abs_star])
@@ -202,25 +202,25 @@
(* f::nat=>nat *)
lemma starfunNat2:
- "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
- Abs_hypnat(hypnatrel `` {%n. f (X n)})"
+ "( *fNat2* f) (Abs_star(starrel``{%n. X n})) =
+ Abs_star(starrel `` {%n. f (X n)})"
apply (simp add: starfunNat2_def)
-apply (rule arg_cong [where f = Abs_hypnat])
-apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse]
- UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent])
+apply (rule arg_cong [where f = Abs_star])
+apply (simp add: starrel_in_hypreal [THEN Abs_star_inverse]
+ UN_equiv_class [OF equiv_starrel starfunNat_congruent])
done
subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*}
lemma starfunNat_mult:
"( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat hypreal_mult)
done
lemma starfunNat2_mult:
"( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat2 hypnat_mult)
done
@@ -228,19 +228,19 @@
lemma starfunNat_add:
"( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat hypreal_add)
done
lemma starfunNat2_add:
"( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat2 hypnat_add)
done
lemma starfunNat2_minus:
"( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat2 hypnat_minus)
done
@@ -251,7 +251,7 @@
lemma starfunNatNat2_o:
"( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (simp add: starfunNat2 starfunNat)
done
@@ -264,7 +264,7 @@
(***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****)
lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (simp add: starfunNat2)
done
@@ -272,7 +272,7 @@
lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (simp add: starfunNat starfun)
done
@@ -286,23 +286,23 @@
text{*NS extension of constant function*}
lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat hypreal_of_real_def star_of_def star_n_def)
done
lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat2 hypnat_of_nat_eq)
done
lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfunNat hypreal_minus)
done
lemma starfunNat_inverse:
"inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfunNat hypreal_inverse)
done
@@ -330,7 +330,7 @@
"\<forall>n. N \<le> n --> f n \<le> g n
==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n"
apply safe
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
done
@@ -339,7 +339,7 @@
"\<forall>n. N \<le> n --> f n < g n
==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n"
apply safe
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
done
@@ -347,27 +347,27 @@
lemma starfunNat_shift_one:
"( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
apply (simp add: starfunNat hypnat_one_def hypnat_add)
done
text{*Nonstandard extension with absolute value*}
lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
apply (simp add: starfunNat hypreal_hrabs)
done
text{*The hyperpow function as a nonstandard extension of realpow*}
lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
apply (simp add: hyperpow hypreal_of_real_def star_of_def star_n_def starfunNat)
done
lemma starfunNat_pow2:
"( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
done
@@ -381,7 +381,7 @@
lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (simp add: hypreal_of_hypnat starfunNat)
done
@@ -396,11 +396,11 @@
text{*Internal functions - some redundancy with *fNat* now*}
lemma starfunNat_n_congruent:
- "(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel"
+ "(%X. starrel``{%n. f n (X n)}) respects starrel"
by (auto simp add: congruent_def, ultra+)
lemma starfunNat_n:
- "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+ "( *fNatn* f) (Abs_star(starrel``{%n. X n})) =
Abs_star(starrel `` {%n. f n (X n)})"
apply (simp add: starfunNat_n_def)
apply (rule_tac f = Abs_star in arg_cong, auto, ultra)
@@ -410,7 +410,7 @@
lemma starfunNat_n_mult:
"( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat_n hypreal_mult)
done
@@ -418,7 +418,7 @@
lemma starfunNat_n_add:
"( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat_n hypreal_add)
done
@@ -426,7 +426,7 @@
lemma starfunNat_n_add_minus:
"( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat_n hypreal_minus hypreal_add)
done
@@ -435,12 +435,12 @@
lemma starfunNat_n_const_fun [simp]:
"( *fNatn* (%i x. k)) z = hypreal_of_real k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunNat_n hypreal_of_real_def star_of_def star_n_def)
done
lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfunNat_n hypreal_minus)
done
@@ -539,13 +539,13 @@
constdefs
starPNat :: "(nat => bool) => hypnat => bool" ("*pNat* _" [80] 80)
- "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
+ "*pNat* P == (%x. \<exists>X. (X \<in> Rep_star(x) &
{n. P(X n)} \<in> FreeUltrafilterNat))"
starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
("*pNat2* _" [80] 80)
- "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
+ "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_star(x) & Y \<in> Rep_star(y) &
{n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
hSuc :: "hypnat => hypnat"
@@ -553,7 +553,7 @@
lemma starPNat:
- "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
+ "(( *pNat* P) (Abs_star(starrel``{%n. X n}))) =
({n. P (X n)} \<in> FreeUltrafilterNat)"
by (auto simp add: starPNat_def, ultra)
@@ -564,7 +564,7 @@
"(( *pNat* P) 0 &
(\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
--> ( *pNat* P)(n)"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
apply (erule nat_induct)
apply (drule_tac x = "hypnat_of_nat n" in spec)
@@ -579,8 +579,8 @@
by (insert hypnat_induct_obj [of P n], auto)
lemma starPNat2:
-"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
- (Abs_hypnat(hypnatrel``{%n. Y n}))) =
+"(( *pNat2* P) (Abs_star(starrel``{%n. X n}))
+ (Abs_star(starrel``{%n. Y n}))) =
({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
by (auto simp add: starPNat2_def, ultra)
@@ -588,17 +588,17 @@
apply (simp add: starPNat2_def)
apply (rule ext)
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac z = y in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
apply (auto, ultra)
done
lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
by (simp add: starPNat2_eq_iff)
-lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
+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_hypnat, auto)
+apply (rule_tac z = h in eq_Abs_star, auto)
done
lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
@@ -615,7 +615,7 @@
lemma nonempty_InternalNatSet_has_least:
"[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto dest!: bspec simp add: hypnat_le)
apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
apply (ultra, force dest: nonempty_nat_set_Least_mem)
--- a/src/HOL/Hyperreal/SEQ.thy Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Wed Sep 07 00:48:50 2005 +0200
@@ -92,7 +92,7 @@
"X ----> L ==> X ----NS> L"
apply (simp add: LIMSEQ_def NSLIMSEQ_def)
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_star)
apply (rule approx_minus_iff [THEN iffD2])
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
star_of_def star_n_def
@@ -145,9 +145,9 @@
text{* thus, the sequence defines an infinite hypernatural! *}
lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
- ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite"
+ ==> Abs_star (starrel `` {f}) : HNatInfinite"
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
apply (erule FreeUltrafilterNat_NSLIMSEQ)
done
@@ -161,7 +161,7 @@
by auto
lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
- ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
+ ( *fNat* X) (Abs_star (starrel `` {f})) +
- hypreal_of_real L \<approx> 0 |] ==> False"
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
apply (rename_tac "Y")
@@ -179,7 +179,7 @@
apply (rule ccontr, simp, safe)
txt{* skolemization step *}
apply (drule choice, safe)
-apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec)
+apply (drule_tac x = "Abs_star (starrel``{f}) " in bspec)
apply (drule_tac [2] approx_minus_iff [THEN iffD1])
apply (simp_all add: linorder_not_less)
apply (blast intro: HNatInfinite_NSLIMSEQ)
@@ -504,7 +504,7 @@
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
apply (simp add: Bseq_def NSBseq_def, safe)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_star)
apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff
HNatInfinite_FreeUltrafilterNat_iff)
apply (rule bexI [OF _ lemma_starrel_refl])
@@ -567,9 +567,9 @@
lemma HNatInfinite_skolem_f:
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
- ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite"
+ ==> Abs_star(starrel``{f}) : HNatInfinite"
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE])
apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
@@ -762,7 +762,7 @@
subsubsection{*Standard Implies Nonstandard*}
lemma lemmaCauchy1:
- "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
+ "Abs_star (starrel `` {x}) : HNatInfinite
==> {n. M \<le> x n} : FreeUltrafilterNat"
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
apply (drule_tac x = M in spec, ultra)
@@ -776,8 +776,8 @@
lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
apply (simp add: Cauchy_def NSCauchy_def, safe)
-apply (rule_tac z = M in eq_Abs_hypnat)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = M in eq_Abs_star)
+apply (rule_tac z = N in eq_Abs_star)
apply (rule approx_minus_iff [THEN iffD2])
apply (rule mem_infmal_iff [THEN iffD1])
apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
@@ -797,7 +797,7 @@
apply (rule ccontr, simp)
apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)
apply (drule bspec, assumption)
-apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec);
+apply (drule_tac x = "Abs_star (starrel `` {fa}) " in bspec);
apply (auto simp add: starfunNat)
apply (drule approx_minus_iff [THEN iffD1])
apply (drule mem_infmal_iff [THEN iffD2])