# HG changeset patch
# User wenzelm
# Date 1451494543 -3600
# Node ID 1b5845c62fa029db717e878c2685287420fea502
# Parent  6b780867d4260848197afd451f4f699ec46e884c
more symbols;

diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HDeriv.thy
--- 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)
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HLim.thy
--- 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)
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HLog.thy
--- 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
 
 
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HSeries.thy
--- 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)
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HTranscendental.thy
--- 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:
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HyperDef.thy
--- 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>
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/HyperNat.thy
--- 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)"
 
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/NSA.thy
--- 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
 
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/NSCA.thy
--- 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
diff -r 6b780867d426 -r 1b5845c62fa0 src/HOL/NSA/NSComplex.thy
--- 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>