--- a/src/HOL/Archimedean_Field.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy Mon Aug 31 21:28:08 2015 +0200
@@ -546,14 +546,14 @@
lemma frac_lt_1: "frac x < 1"
by (simp add: frac_def) linarith
-lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
+lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>"
by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
lemma frac_ge_0 [simp]: "frac x \<ge> 0"
unfolding frac_def
by linarith
-lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
+lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>"
by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
lemma frac_of_int [simp]: "frac (of_int z) = 0"
@@ -582,7 +582,7 @@
lemma frac_unique_iff:
fixes x :: "'a::floor_ceiling"
- shows "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
+ shows "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
apply (auto simp: Ints_def frac_def)
apply linarith
apply linarith
@@ -593,7 +593,7 @@
lemma frac_neg:
fixes x :: "'a::floor_ceiling"
- shows "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
+ shows "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
apply (auto simp add: frac_unique_iff)
apply (simp add: frac_def)
by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
--- a/src/HOL/Int.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Int.thy Mon Aug 31 21:28:08 2015 +0200
@@ -623,11 +623,8 @@
context ring_1
begin
-definition Ints :: "'a set" where
- "Ints = range of_int"
-
-notation (xsymbols)
- Ints ("\<int>")
+definition Ints :: "'a set" ("\<int>")
+ where "\<int> = range of_int"
lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
by (simp add: Ints_def)
@@ -687,7 +684,7 @@
text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
lemma Ints_double_eq_0_iff:
- assumes in_Ints: "a \<in> Ints"
+ assumes in_Ints: "a \<in> \<int>"
shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
@@ -706,7 +703,7 @@
qed
lemma Ints_odd_nonzero:
- assumes in_Ints: "a \<in> Ints"
+ assumes in_Ints: "a \<in> \<int>"
shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
@@ -720,11 +717,11 @@
qed
qed
-lemma Nats_numeral [simp]: "numeral w \<in> Nats"
+lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
using of_nat_in_Nats [of "numeral w"] by simp
lemma Ints_odd_less_0:
- assumes in_Ints: "a \<in> Ints"
+ assumes in_Ints: "a \<in> \<int>"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
proof -
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
--- a/src/HOL/Library/Convex.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Library/Convex.thy Mon Aug 31 21:28:08 2015 +0200
@@ -137,7 +137,7 @@
by (simp only: convex_Int 3 4)
qed
-lemma convex_Reals: "convex Reals"
+lemma convex_Reals: "convex \<real>"
by (simp add: convex_def scaleR_conv_of_real)
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Aug 31 21:28:08 2015 +0200
@@ -242,9 +242,9 @@
by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
isCont_Im continuous_ident continuous_const)+
-lemma closed_complex_Reals: "closed (Reals :: complex set)"
+lemma closed_complex_Reals: "closed (\<real> :: complex set)"
proof -
- have "(Reals :: complex set) = {z. Im z = 0}"
+ have "(\<real> :: complex set) = {z. Im z = 0}"
by (auto simp: complex_is_Real_iff)
then show ?thesis
by (metis closed_halfspace_Im_eq)
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Aug 31 21:28:08 2015 +0200
@@ -211,7 +211,7 @@
by (auto simp: exp_eq abs_mult)
lemma exp_integer_2pi:
- assumes "n \<in> Ints"
+ assumes "n \<in> \<int>"
shows "exp((2 * n * pi) * ii) = 1"
proof -
have "exp((2 * n * pi) * ii) = exp 0"
@@ -751,15 +751,15 @@
by blast
qed
-lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
+lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
proof (cases "z=0")
case True then show ?thesis
by simp
next
case False
- have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
+ have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
by (metis Arg_eq)
- also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+ also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
using False
by (simp add: zero_le_mult_iff)
also have "... \<longleftrightarrow> Arg z = 0"
@@ -955,7 +955,7 @@
corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
by (simp add: Ln_of_real)
-lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
+lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
using Ln_of_real by force
lemma Ln_1: "ln 1 = (0::complex)"
@@ -1565,10 +1565,10 @@
using lim_Ln_over_power [of 1]
by simp
-lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
+lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
using Ln_of_real by force
-lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
+lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
by (simp add: powr_of_real)
lemma lim_ln_over_power:
--- a/src/HOL/NSA/HyperDef.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Mon Aug 31 21:28:08 2015 +0200
@@ -103,7 +103,7 @@
by transfer simp
qed
-lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
+lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard"
by (simp add: Reals_def Standard_def)
@@ -539,7 +539,7 @@
by transfer (rule refl)
lemma hyperpow_SReal [simp]:
- "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
+ "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>"
by (simp add: Reals_eq_Standard)
lemma hyperpow_zero_HNatInfinite [simp]:
--- a/src/HOL/NSA/NSA.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/NSA.thy Mon Aug 31 21:28:08 2015 +0200
@@ -33,7 +33,7 @@
definition
st :: "hypreal => hypreal" where
--{*the standard part of a hyperreal*}
- "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
+ "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
definition
monad :: "'a::real_normed_vector star => 'a star set" where
@@ -49,7 +49,7 @@
notation (HTML output)
approx (infixl "\<approx>" 50)
-lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
by (simp add: Reals_def image_def)
subsection {* Nonstandard Extension of the Norm Function *}
@@ -176,54 +176,54 @@
subsection{*Closure Laws for the Standard Reals*}
-lemma Reals_minus_iff [simp]: "(-x \<in> Reals) = (x \<in> Reals)"
+lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
apply auto
apply (drule Reals_minus, auto)
done
-lemma Reals_add_cancel: "\<lbrakk>x + y \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
by (drule (1) Reals_diff, simp)
-lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
+lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> abs x \<in> \<real>"
by (simp add: Reals_eq_Standard)
-lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
+lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
by (simp add: Reals_eq_Standard)
-lemma SReal_divide_numeral: "r \<in> Reals ==> r/(numeral w::hypreal) \<in> Reals"
+lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
by simp
text{*epsilon is not in Reals because it is an infinitesimal*}
-lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
+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> Reals"
+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
-lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
+lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> \<real>} = (UNIV::real set)"
by simp
-lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
+lemma SReal_iff: "(x \<in> \<real>) = (\<exists>y. x = hypreal_of_real y)"
by (simp add: SReal_def)
-lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
+lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>"
by (simp add: Reals_eq_Standard Standard_def)
-lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
+lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV"
apply (auto simp add: SReal_def)
apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
done
lemma SReal_hypreal_of_real_image:
- "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
+ "[| \<exists>x. x: P; P \<subseteq> \<real> |] ==> \<exists>Q. P = hypreal_of_real ` Q"
by (simp add: SReal_def image_def, blast)
lemma SReal_dense:
- "[| (x::hypreal) \<in> Reals; y \<in> Reals; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
+ "[| (x::hypreal) \<in> \<real>; y \<in> \<real>; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
apply (auto simp add: SReal_def)
apply (drule dense, auto)
done
@@ -231,12 +231,12 @@
text{*Completeness of Reals, but both lemmas are unused.*}
lemma SReal_sup_lemma:
- "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
+ "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
(\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
by (blast dest!: SReal_iff [THEN iffD1])
lemma SReal_sup_lemma2:
- "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
+ "[| P \<subseteq> \<real>; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
(\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
apply (rule conjI)
@@ -277,7 +277,7 @@
apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
done
-lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
+lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite"
by (auto simp add: SReal_def)
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
@@ -850,29 +850,29 @@
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
lemma approx_SReal_mult_cancel_zero:
- "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
-lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
-lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
lemma approx_mult_SReal_zero_cancel_iff [simp]:
- "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+ "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
lemma approx_SReal_mult_cancel:
- "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
lemma approx_SReal_mult_cancel_iff1 [simp]:
- "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
intro: approx_SReal_mult_cancel)
@@ -907,7 +907,7 @@
subsection{* Zero is the Only Infinitesimal that is also a Real*}
lemma Infinitesimal_less_SReal:
- "[| (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
+ "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
apply (simp add: Infinitesimal_def)
apply (rule abs_ge_self [THEN order_le_less_trans], auto)
done
@@ -917,29 +917,29 @@
by (blast intro: Infinitesimal_less_SReal)
lemma SReal_not_Infinitesimal:
- "[| 0 < y; (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal"
+ "[| 0 < y; (y::hypreal) \<in> \<real>|] ==> y \<notin> Infinitesimal"
apply (simp add: Infinitesimal_def)
apply (auto simp add: abs_if)
done
lemma SReal_minus_not_Infinitesimal:
- "[| y < 0; (y::hypreal) \<in> Reals |] ==> y \<notin> Infinitesimal"
+ "[| y < 0; (y::hypreal) \<in> \<real> |] ==> y \<notin> Infinitesimal"
apply (subst Infinitesimal_minus_iff [symmetric])
apply (rule SReal_not_Infinitesimal, auto)
done
-lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}"
+lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}"
apply auto
apply (cut_tac x = x and y = 0 in linorder_less_linear)
apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done
lemma SReal_Infinitesimal_zero:
- "[| (x::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
+ "[| (x::hypreal) \<in> \<real>; x \<in> Infinitesimal|] ==> x = 0"
by (cut_tac SReal_Int_Infinitesimal_zero, blast)
lemma SReal_HFinite_diff_Infinitesimal:
- "[| (x::hypreal) \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
+ "[| (x::hypreal) \<in> \<real>; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
lemma hypreal_of_real_HFinite_diff_Infinitesimal:
@@ -971,7 +971,7 @@
done
lemma approx_SReal_not_zero:
- "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+ "[| (y::hypreal) \<in> \<real>; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done
@@ -996,7 +996,7 @@
done
lemma Infinitesimal_SReal_divide:
- "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
+ "[| (x::hypreal) \<in> Infinitesimal; y \<in> \<real> |] ==> x/y \<in> Infinitesimal"
apply (simp add: divide_inverse)
apply (auto intro!: Infinitesimal_HFinite_mult
dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
@@ -1018,7 +1018,7 @@
done
lemma SReal_approx_iff:
- "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
+ "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)"
apply auto
apply (simp add: approx_def)
apply (drule (1) Reals_diff)
@@ -1060,7 +1060,7 @@
by (simp_all add: star_of_approx_iff [symmetric])
lemma approx_unique_real:
- "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+ "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s"
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
@@ -1069,12 +1069,12 @@
subsubsection{*Lifting of the Ub and Lub Properties*}
lemma hypreal_of_real_isUb_iff:
- "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+ "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
(isUb (UNIV :: real set) Q Y)"
by (simp add: isUb_def setle_def)
lemma hypreal_of_real_isLub1:
- "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
+ "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)
==> isLub (UNIV :: real set) Q Y"
apply (simp add: isLub_def leastP_def)
apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
@@ -1083,30 +1083,30 @@
lemma hypreal_of_real_isLub2:
"isLub (UNIV :: real set) Q Y
- ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
+ ==> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)"
apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
lemma hypreal_of_real_isLub_iff:
- "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+ "(isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
(isLub (UNIV :: real set) Q Y)"
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
lemma lemma_isUb_hypreal_of_real:
- "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
+ "isUb \<real> P Y ==> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)"
by (auto simp add: SReal_iff isUb_def)
lemma lemma_isLub_hypreal_of_real:
- "isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)"
+ "isLub \<real> P Y ==> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)"
by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
lemma lemma_isLub_hypreal_of_real2:
- "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
+ "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) ==> \<exists>Y. isLub \<real> P Y"
by (auto simp add: isLub_def leastP_def isUb_def)
lemma SReal_complete:
- "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y |]
- ==> \<exists>t::hypreal. isLub Reals P t"
+ "[| P \<subseteq> \<real>; \<exists>x. x \<in> P; \<exists>Y. isUb \<real> P Y |]
+ ==> \<exists>t::hypreal. isLub \<real> P t"
apply (frule SReal_hypreal_of_real_image)
apply (auto, drule lemma_isUb_hypreal_of_real)
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
@@ -1116,14 +1116,14 @@
(* lemma about lubs *)
lemma lemma_st_part_ub:
- "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
+ "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb \<real> {s. s \<in> \<real> & s < x} u"
apply (drule HFiniteD, safe)
apply (rule exI, rule isUbI)
apply (auto intro: setleI isUbI simp add: abs_less_iff)
done
lemma lemma_st_part_nonempty:
- "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
+ "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> \<real> & s < x}"
apply (drule HFiniteD, safe)
apply (drule Reals_minus)
apply (rule_tac x = "-t" in exI)
@@ -1131,12 +1131,12 @@
done
lemma lemma_st_part_lub:
- "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
+ "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub \<real> {s. s \<in> \<real> & s < x} t"
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
lemma lemma_st_part_le1:
- "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |] ==> x \<le> t + r"
+ "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |] ==> x \<le> t + r"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD2])
apply (drule (1) Reals_add)
@@ -1156,8 +1156,8 @@
done
lemma lemma_st_part_gt_ub:
- "[| (x::hypreal) \<in> HFinite; x < y; y \<in> Reals |]
- ==> isUb Reals {s. s \<in> Reals & s < x} y"
+ "[| (x::hypreal) \<in> HFinite; x < y; y \<in> \<real> |]
+ ==> isUb \<real> {s. s \<in> \<real> & s < x} y"
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
@@ -1167,8 +1167,8 @@
lemma lemma_st_part_le2:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> t + -r \<le> x"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD1])
@@ -1181,8 +1181,8 @@
lemma lemma_st_part1a:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> x + -t \<le> r"
apply (subgoal_tac "x \<le> t+r")
apply (auto intro: lemma_st_part_le1)
@@ -1190,8 +1190,8 @@
lemma lemma_st_part2a:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> -(x + -t) \<le> r"
apply (subgoal_tac "(t + -r \<le> x)")
apply simp
@@ -1200,11 +1200,11 @@
done
lemma lemma_SReal_ub:
- "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
+ "(x::hypreal) \<in> \<real> ==> isUb \<real> {s. s \<in> \<real> & s < x} x"
by (auto intro: isUbI setleI order_less_imp_le)
lemma lemma_SReal_lub:
- "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
+ "(x::hypreal) \<in> \<real> ==> isLub \<real> {s. s \<in> \<real> & s < x} x"
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
apply (frule isUbD2a)
apply (rule_tac x = x and y = y in linorder_cases)
@@ -1216,8 +1216,8 @@
lemma lemma_st_part_not_eq1:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> x + -t \<noteq> r"
apply auto
apply (frule isLubD1a [THEN Reals_minus])
@@ -1228,8 +1228,8 @@
lemma lemma_st_part_not_eq2:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> -(x + -t) \<noteq> r"
apply (auto)
apply (frule isLubD1a)
@@ -1240,8 +1240,8 @@
lemma lemma_st_part_major:
"[| (x::hypreal) \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |]
+ isLub \<real> {s. s \<in> \<real> & s < x} t;
+ r \<in> \<real>; 0 < r |]
==> abs (x - t) < r"
apply (frule lemma_st_part1a)
apply (frule_tac [4] lemma_st_part2a, auto)
@@ -1250,7 +1250,7 @@
done
lemma lemma_st_part_major2:
- "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
+ "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
by (blast dest!: lemma_st_part_major)
@@ -1271,7 +1271,7 @@
done
text{*There is a unique real infinitely close*}
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
apply (drule st_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
apply (auto intro!: approx_unique_real)
@@ -1471,7 +1471,7 @@
done
lemma HInfinite_gt_SReal:
- "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
+ "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> \<real> |] ==> y < x"
by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)
lemma HInfinite_gt_zero_gt_one:
@@ -1762,7 +1762,7 @@
apply (auto intro: approx_sym)
done
-lemma st_SReal: "x \<in> HFinite ==> st x \<in> Reals"
+lemma st_SReal: "x \<in> HFinite ==> st x \<in> \<real>"
apply (simp add: st_def)
apply (frule st_part_Ex, safe)
apply (rule someI2)
@@ -1780,7 +1780,7 @@
apply (auto intro: approx_unique_real)
done
-lemma st_SReal_eq: "x \<in> Reals ==> st x = x"
+lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
by (metis approx_refl st_unique)
lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
@@ -1793,7 +1793,7 @@
assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
shows "st x = st y"
proof -
- have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
+ have "st x @= x" "st y @= y" "st x \<in> \<real>" "st y \<in> \<real>"
by (simp_all add: st_approx_self st_SReal x y)
with xy show ?thesis
by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
@@ -1805,13 +1805,13 @@
by (blast intro: approx_st_eq st_eq_approx)
lemma st_Infinitesimal_add_SReal:
- "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
+ "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(x + e) = x"
apply (erule st_unique)
apply (erule Infinitesimal_add_approx_self)
done
lemma st_Infinitesimal_add_SReal2:
- "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x"
+ "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(e + x) = x"
apply (erule st_unique)
apply (erule Infinitesimal_add_approx_self2)
done
--- a/src/HOL/NSA/NSCA.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/NSCA.thy Mon Aug 31 21:28:08 2015 +0200
@@ -29,13 +29,13 @@
by (drule (1) Standard_diff, simp)
lemma SReal_hcmod_hcomplex_of_complex [simp]:
- "hcmod (hcomplex_of_complex r) \<in> Reals"
+ "hcmod (hcomplex_of_complex r) \<in> \<real>"
by (simp add: Reals_eq_Standard)
-lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> Reals"
+lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> \<real>"
by (simp add: Reals_eq_Standard)
-lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
+lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> \<real>"
by (simp add: Reals_eq_Standard)
lemma SComplex_divide_numeral:
@@ -482,7 +482,7 @@
by (simp add: hcomplex_HFinite_iff)
lemma SComplex_SReal_hcomplex_of_hypreal:
- "x \<in> Reals ==> hcomplex_of_hypreal x \<in> SComplex"
+ "x \<in> \<real> ==> hcomplex_of_hypreal x \<in> SComplex"
apply (rule Standard_of_hypreal)
apply (simp add: Reals_eq_Standard)
done
--- a/src/HOL/NSA/Star.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/Star.thy Mon Aug 31 21:28:08 2015 +0200
@@ -53,7 +53,7 @@
lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
by auto
-lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
+lemma STAR_hypreal_of_real_Int: "*s* X Int \<real> = hypreal_of_real ` X"
by (auto simp add: SReal_def)
lemma STAR_star_of_Int: "*s* X Int Standard = star_of ` X"
--- a/src/HOL/Nat.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Nat.thy Mon Aug 31 21:28:08 2015 +0200
@@ -1588,11 +1588,8 @@
context semiring_1
begin
-definition Nats :: "'a set" where
- "Nats = range of_nat"
-
-notation (xsymbols)
- Nats ("\<nat>")
+definition Nats :: "'a set" ("\<nat>")
+ where "\<nat> = range of_nat"
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
by (simp add: Nats_def)
--- a/src/HOL/Rat.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Rat.thy Mon Aug 31 21:28:08 2015 +0200
@@ -808,58 +808,54 @@
context field_char_0
begin
-definition
- Rats :: "'a set" where
- "Rats = range of_rat"
-
-notation (xsymbols)
- Rats ("\<rat>")
+definition Rats :: "'a set" ("\<rat>")
+ where "\<rat> = range of_rat"
end
-lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
+lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
by (simp add: Rats_def)
-lemma Rats_of_int [simp]: "of_int z \<in> Rats"
+lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
-lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
+lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
-lemma Rats_number_of [simp]: "numeral w \<in> Rats"
+lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
-lemma Rats_0 [simp]: "0 \<in> Rats"
+lemma Rats_0 [simp]: "0 \<in> \<rat>"
apply (unfold Rats_def)
apply (rule range_eqI)
apply (rule of_rat_0 [symmetric])
done
-lemma Rats_1 [simp]: "1 \<in> Rats"
+lemma Rats_1 [simp]: "1 \<in> \<rat>"
apply (unfold Rats_def)
apply (rule range_eqI)
apply (rule of_rat_1 [symmetric])
done
-lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
+lemma Rats_add [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a + b \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_add [symmetric])
done
-lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
+lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_minus [symmetric])
done
-lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
+lemma Rats_diff [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a - b \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_diff [symmetric])
done
-lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
+lemma Rats_mult [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a * b \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_mult [symmetric])
@@ -867,7 +863,7 @@
lemma nonzero_Rats_inverse:
fixes a :: "'a::field_char_0"
- shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
+ shows "\<lbrakk>a \<in> \<rat>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (erule nonzero_of_rat_inverse [symmetric])
@@ -875,7 +871,7 @@
lemma Rats_inverse [simp]:
fixes a :: "'a::{field_char_0, field}"
- shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
+ shows "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_inverse [symmetric])
@@ -883,7 +879,7 @@
lemma nonzero_Rats_divide:
fixes a b :: "'a::field_char_0"
- shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
+ shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (erule nonzero_of_rat_divide [symmetric])
@@ -891,7 +887,7 @@
lemma Rats_divide [simp]:
fixes a b :: "'a::{field_char_0, field}"
- shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
+ shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_divide [symmetric])
@@ -899,7 +895,7 @@
lemma Rats_power [simp]:
fixes a :: "'a::field_char_0"
- shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
+ shows "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
apply (rule of_rat_power [symmetric])
--- a/src/HOL/Real.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Real.thy Mon Aug 31 21:28:08 2015 +0200
@@ -1163,7 +1163,7 @@
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
-lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
unfolding real_of_int_def by (rule Ints_of_int)
@@ -1300,10 +1300,10 @@
apply (simp only: real_of_int_of_nat_eq)
done
-lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> \<nat>"
unfolding real_of_nat_def by (rule of_nat_in_Nats)
-lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> \<int>"
unfolding real_of_nat_def by (rule Ints_of_nat)
subsection \<open>The Archimedean Property of the Reals\<close>
--- a/src/HOL/Real_Vector_Spaces.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Aug 31 21:28:08 2015 +0200
@@ -358,55 +358,52 @@
subsection \<open>The Set of Real Numbers\<close>
-definition Reals :: "'a::real_algebra_1 set" where
- "Reals = range of_real"
+definition Reals :: "'a::real_algebra_1 set" ("\<real>")
+ where "\<real> = range of_real"
-notation (xsymbols)
- Reals ("\<real>")
-
-lemma Reals_of_real [simp]: "of_real r \<in> Reals"
+lemma Reals_of_real [simp]: "of_real r \<in> \<real>"
by (simp add: Reals_def)
-lemma Reals_of_int [simp]: "of_int z \<in> Reals"
+lemma Reals_of_int [simp]: "of_int z \<in> \<real>"
by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
-lemma Reals_of_nat [simp]: "of_nat n \<in> Reals"
+lemma Reals_of_nat [simp]: "of_nat n \<in> \<real>"
by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
-lemma Reals_numeral [simp]: "numeral w \<in> Reals"
+lemma Reals_numeral [simp]: "numeral w \<in> \<real>"
by (subst of_real_numeral [symmetric], rule Reals_of_real)
-lemma Reals_0 [simp]: "0 \<in> Reals"
+lemma Reals_0 [simp]: "0 \<in> \<real>"
apply (unfold Reals_def)
apply (rule range_eqI)
apply (rule of_real_0 [symmetric])
done
-lemma Reals_1 [simp]: "1 \<in> Reals"
+lemma Reals_1 [simp]: "1 \<in> \<real>"
apply (unfold Reals_def)
apply (rule range_eqI)
apply (rule of_real_1 [symmetric])
done
-lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals"
+lemma Reals_add [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a + b \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_add [symmetric])
done
-lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow> - a \<in> Reals"
+lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_minus [symmetric])
done
-lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a - b \<in> Reals"
+lemma Reals_diff [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a - b \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_diff [symmetric])
done
-lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals"
+lemma Reals_mult [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a * b \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_mult [symmetric])
@@ -414,7 +411,7 @@
lemma nonzero_Reals_inverse:
fixes a :: "'a::real_div_algebra"
- shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals"
+ shows "\<lbrakk>a \<in> \<real>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (erule nonzero_of_real_inverse [symmetric])
@@ -422,7 +419,7 @@
lemma Reals_inverse:
fixes a :: "'a::{real_div_algebra, division_ring}"
- shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
+ shows "a \<in> \<real> \<Longrightarrow> inverse a \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_inverse [symmetric])
@@ -435,7 +432,7 @@
lemma nonzero_Reals_divide:
fixes a b :: "'a::real_field"
- shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
+ shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (erule nonzero_of_real_divide [symmetric])
@@ -443,7 +440,7 @@
lemma Reals_divide [simp]:
fixes a b :: "'a::{real_field, field}"
- shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
+ shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_divide [symmetric])
@@ -451,7 +448,7 @@
lemma Reals_power [simp]:
fixes a :: "'a::{real_algebra_1}"
- shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
+ shows "a \<in> \<real> \<Longrightarrow> a ^ n \<in> \<real>"
apply (auto simp add: Reals_def)
apply (rule range_eqI)
apply (rule of_real_power [symmetric])
--- a/src/HOL/Transcendental.thy Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Transcendental.thy Mon Aug 31 21:28:08 2015 +0200
@@ -3759,7 +3759,7 @@
using sin_cos_squared_add [of x, unfolded assms]
by simp
-lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
+lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> \<int>"
by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
lemma cos_one_2pi:
@@ -3875,10 +3875,10 @@
lemma sin_30: "sin (pi / 6) = 1 / 2"
by (simp add: sin_cos_eq cos_60)
-lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
+lemma cos_integer_2pi: "n \<in> \<int> \<Longrightarrow> cos(2*pi * n) = 1"
by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
-lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
+lemma sin_integer_2pi: "n \<in> \<int> \<Longrightarrow> sin(2*pi * n) = 0"
by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"