--- a/src/HOL/NSA/HDeriv.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy Wed Dec 30 17:55:43 2015 +0100
@@ -57,7 +57,7 @@
lemma NSDeriv_unique:
"[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E"
-apply (subgoal_tac "( *f* of_real) epsilon \<in> Infinitesimal - {0::'a star}")
+apply (subgoal_tac "( *f* of_real) \<epsilon> \<in> Infinitesimal - {0::'a star}")
apply (simp only: nsderiv_def)
apply (drule (1) bspec)+
apply (drule (1) approx_trans3)
--- a/src/HOL/NSA/HLim.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HLim.thy Wed Dec 30 17:55:43 2015 +0100
@@ -102,7 +102,7 @@
fixes a :: "'a::real_normed_algebra_1"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
apply (simp add: NSLIM_def)
-apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
+apply (rule_tac x="star_of a + of_hypreal \<epsilon>" in exI)
apply (simp add: hypreal_epsilon_not_zero approx_def)
done
@@ -170,10 +170,10 @@
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
\<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
proof (rule exI, safe)
- show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
+ show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero)
next
fix x assume neq: "x \<noteq> star_of a"
- assume "hnorm (x - star_of a) < epsilon"
+ assume "hnorm (x - star_of a) < \<epsilon>"
with Infinitesimal_epsilon
have "x - star_of a \<in> Infinitesimal"
by (rule hnorm_less_Infinitesimal)
@@ -309,10 +309,10 @@
have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
\<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
proof (rule exI, safe)
- show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
+ show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero)
next
fix x y :: "'a star"
- assume "hnorm (x - y) < epsilon"
+ assume "hnorm (x - y) < \<epsilon>"
with Infinitesimal_epsilon
have "x - y \<in> Infinitesimal"
by (rule hnorm_less_Infinitesimal)
--- a/src/HOL/NSA/HLog.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HLog.thy Wed Dec 30 17:55:43 2015 +0100
@@ -11,10 +11,10 @@
(* should be in NSA.ML *)
-lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
+lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
by (simp add: epsilon_def star_n_zero_num star_n_le)
-lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
+lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
by auto
--- a/src/HOL/NSA/HSeries.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy Wed Dec 30 17:55:43 2015 +0100
@@ -102,10 +102,10 @@
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
by (simp add: sumhr_const)
-lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
+lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = \<omega> - 1"
apply (simp add: sumhr_const)
-(* FIXME: need lemma: hypreal_of_hypnat whn = omega - 1 *)
-(* maybe define omega = hypreal_of_hypnat whn + 1 *)
+(* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
+(* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
apply (unfold star_class_defs omega_def hypnat_omega_def
of_hypnat_def star_of_def)
apply (simp add: starfun_star_n starfun2_star_n)
--- a/src/HOL/NSA/HTranscendental.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Wed Dec 30 17:55:43 2015 +0100
@@ -260,7 +260,7 @@
apply (auto simp add: mem_infmal_iff)
done
-lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
+lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> @= 1"
by (auto intro: STAR_exp_Infinitesimal)
lemma STAR_exp_add:
--- a/src/HOL/NSA/HyperDef.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Wed Dec 30 17:55:43 2015 +0100
@@ -21,18 +21,14 @@
"hypreal_of_hypnat \<equiv> of_hypnat"
definition
- omega :: hypreal where
+ omega :: hypreal ("\<omega>") where
\<comment> \<open>an infinite number \<open>= [<1,2,3,...>]\<close>\<close>
- "omega = star_n (\<lambda>n. real (Suc n))"
+ "\<omega> = star_n (\<lambda>n. real (Suc n))"
definition
- epsilon :: hypreal where
+ epsilon :: hypreal ("\<epsilon>") where
\<comment> \<open>an infinitesimal number \<open>= [<1,1/2,1/3,...>]\<close>\<close>
- "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
-
-notation (xsymbols)
- omega ("\<omega>") and
- epsilon ("\<epsilon>")
+ "\<epsilon> = star_n (\<lambda>n. inverse (real (Suc n)))"
subsection \<open>Real vector class instances\<close>
@@ -219,7 +215,7 @@
lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
by (simp only: star_abs_def starfun_star_n)
-lemma hypreal_omega_gt_zero [simp]: "0 < omega"
+lemma hypreal_omega_gt_zero [simp]: "0 < \<omega>"
by (simp add: omega_def star_n_zero_num star_n_less)
subsection\<open>Existence of Infinite Hyperreal Number\<close>
@@ -238,7 +234,7 @@
using lemma_omega_empty_singleton_disj [of x] by auto
lemma not_ex_hypreal_of_real_eq_omega:
- "~ (\<exists>x. hypreal_of_real x = omega)"
+ "~ (\<exists>x. hypreal_of_real x = \<omega>)"
apply (simp add: omega_def star_of_def star_n_eq_iff)
apply clarify
apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE])
@@ -246,7 +242,7 @@
apply auto
done
-lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
+lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>"
by (insert not_ex_hypreal_of_real_eq_omega, auto)
text\<open>Existence of infinitesimal number also not corresponding to any
@@ -260,21 +256,21 @@
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
-lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
+lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = \<epsilon>)"
by (auto simp add: epsilon_def star_of_def star_n_eq_iff
lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: of_nat_Suc)
-lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
+lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>"
by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
-lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
+lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper
del: star_of_zero)
-lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
+lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
by (simp add: epsilon_def omega_def star_n_inverse)
-lemma hypreal_epsilon_gt_zero: "0 < epsilon"
+lemma hypreal_epsilon_gt_zero: "0 < \<epsilon>"
by (simp add: hypreal_epsilon_inverse_omega)
subsection\<open>Absolute Value Function for the Hyperreals\<close>
--- a/src/HOL/NSA/HyperNat.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/HyperNat.thy Wed Dec 30 17:55:43 2015 +0100
@@ -269,7 +269,7 @@
subsection\<open>Existence of an infinite hypernatural number\<close>
definition
- (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+ (* \<omega> is in fact an infinite hypernatural number = [<1,2,3,...>] *)
whn :: hypnat where
hypnat_omega_def: "whn = star_n (%n::nat. n)"
--- a/src/HOL/NSA/NSA.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Wed Dec 30 17:55:43 2015 +0100
@@ -190,13 +190,13 @@
lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
by simp
-text\<open>epsilon is not in Reals because it is an infinitesimal\<close>
-lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>"
+text \<open>\<open>\<epsilon>\<close> is not in Reals because it is an infinitesimal\<close>
+lemma SReal_epsilon_not_mem: "\<epsilon> \<notin> \<real>"
apply (simp add: SReal_def)
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
done
-lemma SReal_omega_not_mem: "omega \<notin> \<real>"
+lemma SReal_omega_not_mem: "\<omega> \<notin> \<real>"
apply (simp add: SReal_def)
apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
done
@@ -2050,9 +2050,9 @@
done
-subsection\<open>Proof that @{term omega} is an infinite number\<close>
+subsection\<open>Proof that \<open>\<omega>\<close> is an infinite number\<close>
-text\<open>It will follow that epsilon is an infinitesimal number.\<close>
+text\<open>It will follow that \<open>\<epsilon>\<close> is an infinitesimal number.\<close>
lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
by (auto simp add: less_Suc_eq)
@@ -2100,9 +2100,9 @@
lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
by (auto dest!: order_le_less_trans simp add: linorder_not_le)
-text\<open>@{term omega} is a member of @{term HInfinite}\<close>
+text\<open>@{term \<omega>} is a member of @{term HInfinite}\<close>
-theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
+theorem HInfinite_omega [simp]: "\<omega> \<in> HInfinite"
apply (simp add: omega_def)
apply (rule FreeUltrafilterNat_HInfinite)
apply clarify
@@ -2114,13 +2114,13 @@
Epsilon is a member of Infinitesimal
-----------------------------------------------*)
-lemma Infinitesimal_epsilon [simp]: "epsilon \<in> Infinitesimal"
+lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal"
by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega)
-lemma HFinite_epsilon [simp]: "epsilon \<in> HFinite"
+lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
-lemma epsilon_approx_zero [simp]: "epsilon @= 0"
+lemma epsilon_approx_zero [simp]: "\<epsilon> @= 0"
apply (simp (no_asm) add: mem_infmal_iff [symmetric])
done
--- a/src/HOL/NSA/NSCA.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/NSCA.thy Wed Dec 30 17:55:43 2015 +0100
@@ -509,7 +509,7 @@
by (simp add: Infinitesimal_hcmod_iff)
lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:
- "hcomplex_of_hypreal epsilon \<in> Infinitesimal"
+ "hcomplex_of_hypreal \<epsilon> \<in> Infinitesimal"
by (simp add: Infinitesimal_hcmod_iff)
end
--- a/src/HOL/NSA/NSComplex.thy Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy Wed Dec 30 17:55:43 2015 +0100
@@ -206,7 +206,7 @@
by transfer (rule Im_complex_of_real)
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
- "hcomplex_of_hypreal epsilon \<noteq> 0"
+ "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
by (simp add: hypreal_epsilon_not_zero)
subsection\<open>HComplex theorems\<close>