--- a/src/HOL/GCD.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/GCD.thy Wed Dec 30 11:37:29 2015 +0100
@@ -2232,6 +2232,6 @@
\<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
and (Haskell) "Prelude.gcd"
and (Scala) "_.gcd'((_)')"
- -- \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
+ \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
end
--- a/src/HOL/Library/ContNotDenum.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Wed Dec 30 11:37:29 2015 +0100
@@ -148,8 +148,8 @@
assumes "a < b" and "countable A"
shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
proof -
- from `countable A` have "countable (A \<inter> {a<..<b})" by auto
- moreover with `a < b` have "\<not> countable {a<..<b}"
+ from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto
+ moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
by (simp add: uncountable_open_interval)
ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
hence "A \<inter> {a<..<b} \<subset> {a<..<b}"
--- a/src/HOL/Library/Discrete.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Library/Discrete.thy Wed Dec 30 11:37:29 2015 +0100
@@ -20,7 +20,7 @@
assumes one: "P 1"
assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
shows "P n"
-using `n > 0` proof (induct n rule: log.induct)
+using \<open>n > 0\<close> proof (induct n rule: log.induct)
fix n
assume "\<not> n < 2 \<Longrightarrow>
0 < n div 2 \<Longrightarrow> P (n div 2)"
@@ -30,7 +30,7 @@
proof (cases "n = 1")
case True with one show ?thesis by simp
next
- case False with `n > 0` have "n \<ge> 2" by auto
+ case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
moreover with * have "P (n div 2)" .
ultimately show ?thesis by (rule double)
qed
@@ -82,7 +82,7 @@
with mn2 have "n \<ge> 2" by arith
from True have m2_0: "m div 2 \<noteq> 0" by arith
with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
- from `\<not> m < 2` "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
+ from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
qed
@@ -100,9 +100,9 @@
with log_mono have "log n \<ge> Suc 0"
by (simp add: log.simps)
assume "2 ^ log (n div 2) \<le> n div 2"
- with `n \<ge> 2` have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
+ with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
- with `log n \<ge> Suc 0` have "2 ^ log n \<le> n div 2 * 2"
+ with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2"
unfolding power_add [symmetric] by simp
also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
finally show "2 ^ log n \<le> n" .
--- a/src/HOL/Library/Function_Growth.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Library/Function_Growth.thy Wed Dec 30 11:37:29 2015 +0100
@@ -37,7 +37,7 @@
proof -
def q == "m - n"
moreover with assms have "m = q + n" by (simp add: q_def)
- ultimately show ?thesis using `a \<noteq> 0` by (simp add: power_add)
+ ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
qed
@@ -335,14 +335,14 @@
proof
show "(\<lambda>n. f n + k) \<lesssim> f"
proof
- from `\<exists>n. f n > 0` obtain n where "f n > 0" ..
+ from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
have "\<forall>m>n. f m + k \<le> Suc k * f m"
proof (rule allI, rule impI)
fix m
assume "n < m"
- with `mono f` have "f n \<le> f m"
+ with \<open>mono f\<close> have "f n \<le> f m"
using less_imp_le_nat monoE by blast
- with `0 < f n` have "0 < f m" by auto
+ with \<open>0 < f n\<close> have "0 < f m" by auto
then obtain l where "f m = Suc l" by (cases "f m") simp_all
then show "f m + k \<le> Suc k * f m" by simp
qed
@@ -366,7 +366,7 @@
assume "\<not> (\<exists>n. 0 < f n)"
then have "\<And>n. f n = 0" by simp
then have "f 0 = f 1" by simp
- moreover from `strict_mono f` have "f 0 < f 1"
+ moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
by (simp add: strict_mono_def)
ultimately show False by simp
qed
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Wed Dec 30 11:37:29 2015 +0100
@@ -2,7 +2,7 @@
Author: Fabian Immler, TU München
*)
-section {* Bounded Linear Function *}
+section \<open>Bounded Linear Function\<close>
theory Bounded_Linear_Function
imports
@@ -10,7 +10,7 @@
Operator_Norm
begin
-subsection {* Intro rules for @{term bounded_linear} *}
+subsection \<open>Intro rules for @{term bounded_linear}\<close>
named_theorems bounded_linear_intros
@@ -218,7 +218,7 @@
proof (rule CauchyI)
fix e::real
assume "0 < e"
- from CauchyD[OF `Cauchy X` `0 < e`] obtain M
+ from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
by auto
show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
@@ -230,7 +230,7 @@
also have "\<dots> \<le> norm (X m - X n) * norm x"
by (rule norm_blinfun)
also have "\<dots> \<le> norm (X m - X n) * 1"
- using `norm x \<le> 1` norm_ge_zero by (rule mult_left_mono)
+ using \<open>norm x \<le> 1\<close> norm_ge_zero by (rule mult_left_mono)
also have "\<dots> = norm (X m - X n)" by simp
also have "\<dots> < e" using le by fact
finally show "norm (X m x - X n x) < e" .
@@ -257,7 +257,7 @@
proof (rule CauchyI)
fix e::real
assume "e > 0"
- from CauchyD[OF `Cauchy X` `0 < e`] obtain M
+ from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
by auto
show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
@@ -297,8 +297,8 @@
proof (rule LIMSEQ_I)
fix r::real assume "r > 0"
def r' \<equiv> "r / 2"
- have "0 < r'" "r' < r" using `r > 0` by (simp_all add: r'_def)
- from CauchyD[OF `Cauchy X` `r' > 0`]
+ have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
+ from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
by metis
show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
@@ -324,16 +324,16 @@
by (auto intro!: tendsto_intros Bv)
show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
- qed (simp add: `0 < r'` less_imp_le)
+ qed (simp add: \<open>0 < r'\<close> less_imp_le)
thus "norm (X n - Blinfun v) < r"
- by (metis `r' < r` le_less_trans)
+ by (metis \<open>r' < r\<close> le_less_trans)
qed
qed
thus "convergent X"
by (rule convergentI)
qed
-subsection {* On Euclidean Space *}
+subsection \<open>On Euclidean Space\<close>
lemma Zfun_setsum:
assumes "finite s"
@@ -462,7 +462,7 @@
"(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
by auto
-text {* TODO: generalize this and @{thm compact_lemma}?! *}
+text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close>
lemma compact_blinfun_lemma:
fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
assumes "bounded (range f)"
@@ -484,7 +484,7 @@
have k[intro]: "k \<in> Basis"
using insert by auto
have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
- using `bounded (range f)`
+ using \<open>bounded (range f)\<close>
by (auto intro!: bounded_linear_image bounded_linear_intros)
obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
@@ -506,9 +506,9 @@
{
fix e::real
assume "e > 0"
- from lr1 `e > 0` have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
+ from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
by blast
- from lr2 `e > 0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) k) l2 < e) sequentially"
+ from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) k) l2 < e) sequentially"
by (rule tendstoD)
from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) i) (l1 i) < e) sequentially"
by (rule eventually_subseq)
@@ -538,7 +538,7 @@
apply (simp add: blinfun.bilinear_simps)
done
-text {* TODO: generalize (via @{thm compact_cball})? *}
+text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
instance blinfun :: (euclidean_space, euclidean_space) heine_borel
proof
fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Dec 30 11:37:29 2015 +0100
@@ -6049,7 +6049,7 @@
apply (clarsimp simp del: divide_const_simps)
apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
done
- --\<open>Replacing @{term r} and the original (weak) premises\<close>
+ \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close>
obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
apply (rule that [of "(r + dist w z) / 2"])
apply (simp_all add: fh')
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Dec 30 11:37:29 2015 +0100
@@ -261,7 +261,7 @@
subsection\<open>Holomorphic functions\<close>
-text{*Could be generalized to real normed fields, but in practice that would only include the reals*}
+text\<open>Could be generalized to real normed fields, but in practice that would only include the reals\<close>
definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
(infixr "(complex'_differentiable)" 50)
where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Dec 30 11:37:29 2015 +0100
@@ -2471,7 +2471,7 @@
unfolding has_vector_derivative_def has_derivative_iff_norm
using assms by (intro conj_cong Lim_cong_within refl) auto
then show ?thesis
- using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
+ using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
qed
lemma has_vector_derivative_transform_within:
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Wed Dec 30 11:37:29 2015 +0100
@@ -189,13 +189,13 @@
by (metis bounded_linear_mult_const f)
from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
- using `f \<noteq> 0`
+ using \<open>f \<noteq> 0\<close>
by (simp add: inverse_eq_divide)
also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
by (rule onorm_bound)
(auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
- using `f \<noteq> 0`
+ using \<open>f \<noteq> 0\<close>
by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
qed
qed (simp add: onorm_zero)
--- a/src/HOL/NSA/CLim.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/CLim.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,7 +4,7 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-section{*Limits, Continuity and Differentiation for Complex Functions*}
+section\<open>Limits, Continuity and Differentiation for Complex Functions\<close>
theory CLim
imports CStar
@@ -18,7 +18,7 @@
"x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
by (simp add: numeral_2_eq_2)
-text{*Changing the quantified variable. Install earlier?*}
+text\<open>Changing the quantified variable. Install earlier?\<close>
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"
apply auto
apply (drule_tac x="x+a" in spec)
@@ -34,7 +34,7 @@
done
-subsection{*Limit of Complex to Complex Function*}
+subsection\<open>Limit of Complex to Complex Function\<close>
lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
@@ -108,13 +108,13 @@
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
-subsection{*Continuity*}
+subsection\<open>Continuity\<close>
lemma NSLIM_isContc_iff:
"(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
by (rule NSLIM_h_iff)
-subsection{*Functions from Complex to Reals*}
+subsection\<open>Functions from Complex to Reals\<close>
lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
by (auto intro: approx_hnorm
@@ -134,7 +134,7 @@
shows "isCont f a ==> isCont (%x. Im (f x)) a"
by (simp add: isCont_def LIM_Im)
-subsection{* Differentiation of Natural Number Powers*}
+subsection\<open>Differentiation of Natural Number Powers\<close>
lemma CDERIV_pow [simp]:
"DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
@@ -145,11 +145,11 @@
apply (auto simp add: ac_simps)
done
-text{*Nonstandard version*}
+text\<open>Nonstandard version\<close>
lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)
-text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
+text\<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero\<close>
lemma NSCDERIV_inverse:
"(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
unfolding numeral_2_eq_2
@@ -161,7 +161,7 @@
by (rule DERIV_inverse)
-subsection{*Derivative of Reciprocals (Function @{term inverse})*}
+subsection\<open>Derivative of Reciprocals (Function @{term inverse})\<close>
lemma CDERIV_inverse_fun:
"[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
@@ -176,7 +176,7 @@
by (rule NSDERIV_inverse_fun)
-subsection{* Derivative of Quotient*}
+subsection\<open>Derivative of Quotient\<close>
lemma CDERIV_quotient:
"[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
@@ -191,7 +191,7 @@
by (rule NSDERIV_quotient)
-subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
+subsection\<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
lemma CARAT_CDERIVD:
"(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
--- a/src/HOL/NSA/CStar.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/CStar.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,14 +3,14 @@
Copyright : 2001 University of Edinburgh
*)
-section{*Star-transforms in NSA, Extending Sets of Complex Numbers
- and Complex Functions*}
+section\<open>Star-transforms in NSA, Extending Sets of Complex Numbers
+ and Complex Functions\<close>
theory CStar
imports NSCA
begin
-subsection{*Properties of the *-Transform Applied to Sets of Reals*}
+subsection\<open>Properties of the *-Transform Applied to Sets of Reals\<close>
lemma STARC_hcomplex_of_complex_Int:
"*s* X Int SComplex = hcomplex_of_complex ` X"
@@ -20,7 +20,7 @@
"x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
by auto
-subsection{*Theorems about Nonstandard Extensions of Functions*}
+subsection\<open>Theorems about Nonstandard Extensions of Functions\<close>
lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
by transfer (rule refl)
@@ -28,7 +28,7 @@
lemma starfunCR_cmod: "*f* cmod = hcmod"
by transfer (rule refl)
-subsection{*Internal Functions - Some Redundancy With *f* Now*}
+subsection\<open>Internal Functions - Some Redundancy With *f* Now\<close>
(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
(*
--- a/src/HOL/NSA/Examples/NSPrimes.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,14 +4,14 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-section{*The Nonstandard Primes as an Extension of the Prime Numbers*}
+section\<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
theory NSPrimes
imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal"
begin
-text{*These can be used to derive an alternative proof of the infinitude of
-primes by considering a property of nonstandard sets.*}
+text\<open>These can be used to derive an alternative proof of the infinitude of
+primes by considering a property of nonstandard sets.\<close>
definition
starprime :: "hypnat set" where
@@ -55,8 +55,8 @@
done
-text{*The nonstandard extension of the set prime numbers consists of precisely
-those hypernaturals exceeding 1 that have no nontrivial factors*}
+text\<open>The nonstandard extension of the set prime numbers consists of precisely
+those hypernaturals exceeding 1 that have no nontrivial factors\<close>
(* Goldblatt: Exercise 5.11(3a) - p 57 *)
lemma starprime:
@@ -73,7 +73,7 @@
by (rule starset_finite)
-subsection{*Another characterization of infinite set of natural numbers*}
+subsection\<open>Another characterization of infinite set of natural numbers\<close>
lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))"
apply (erule_tac F = N in finite_induct, auto)
@@ -103,7 +103,7 @@
by (auto simp add: finite_nat_set_bounded_iff2 not_le)
-subsection{*An injective function cannot define an embedded natural number*}
+subsection\<open>An injective function cannot define an embedded natural number\<close>
lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m
==> {n. f n = N} = {} | (\<exists>m. {n. f n = N} = {m})"
@@ -197,7 +197,7 @@
apply (rule_tac [4] injf_max_order_preserving, auto)
done
-text{*Only need the existence of an injective function from N to A for proof*}
+text\<open>Only need the existence of an injective function from N to A for proof\<close>
lemma hypnat_infinite_has_nonstandard:
"~ finite A ==> hypnat_of_nat ` A < ( *s* A)"
@@ -223,7 +223,7 @@
apply (auto simp add: finite_starsetNat_iff [symmetric])
done
-subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
+subsection\<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close>
lemma lemma_not_dvd_hypnat_one [simp]: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
apply auto
@@ -259,7 +259,7 @@
lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
by (transfer, rule gcd_lcm_complete_lattice_nat.le_bot)
-text{*Already proved as @{text primes_infinite}, but now using non-standard naturals.*}
+text\<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
theorem not_finite_prime: "~ finite {p::nat. prime p}"
apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
using hypnat_dvd_all_hypnat_of_nat
--- a/src/HOL/NSA/Free_Ultrafilter.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/Free_Ultrafilter.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,15 +4,15 @@
Author: Brian Huffman
*)
-section {* Filters and Ultrafilters *}
+section \<open>Filters and Ultrafilters\<close>
theory Free_Ultrafilter
imports "~~/src/HOL/Library/Infinite_Set"
begin
-subsection {* Definitions and basic properties *}
+subsection \<open>Definitions and basic properties\<close>
-subsubsection {* Ultrafilters *}
+subsubsection \<open>Ultrafilters\<close>
locale ultrafilter =
fixes F :: "'a filter"
@@ -43,17 +43,17 @@
end
-subsection {* Maximal filter = Ultrafilter *}
+subsection \<open>Maximal filter = Ultrafilter\<close>
-text {*
+text \<open>
A filter F is an ultrafilter iff it is a maximal filter,
i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
-*}
-text {*
+\<close>
+text \<open>
Lemmas that shows existence of an extension to what was assumed to
be a maximal filter. Will be used to derive contradiction in proof of
property of ultrafilter.
-*}
+\<close>
lemma extend_filter:
"frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
@@ -92,7 +92,7 @@
intro!: eventually_frequently G proper)
qed fact
-subsection {* Ultrafilter Theorem *}
+subsection \<open>Ultrafilter Theorem\<close>
text "A local context makes proof of ultrafilter Theorem more modular"
@@ -124,7 +124,7 @@
unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
with c have 1: "Inf c \<noteq> bot"
by (simp add: bot_notin_R)
- from `c \<noteq> {}` obtain x where "x \<in> c" by auto
+ from \<open>c \<noteq> {}\<close> obtain x where "x \<in> c" by auto
with c have 2: "Inf c \<le> F"
by (auto intro!: Inf_lower2[of x] simp: Chains_def)
note 1 2 }
@@ -148,9 +148,9 @@
by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
qed
-subsubsection {* Free Ultrafilters *}
+subsubsection \<open>Free Ultrafilters\<close>
-text {* There exists a free ultrafilter on any infinite set *}
+text \<open>There exists a free ultrafilter on any infinite set\<close>
locale freeultrafilter = ultrafilter +
assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
@@ -190,7 +190,7 @@
with proper have "frequently P U"
by (rule eventually_frequently)
then have "frequently P cofinite"
- using `U \<le> cofinite` by (simp add: le_filter_frequently)
+ using \<open>U \<le> cofinite\<close> by (simp add: le_filter_frequently)
then show "infinite {x. P x}"
by (simp add: frequently_cofinite)
qed
--- a/src/HOL/NSA/HDeriv.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,13 +4,13 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-section{* Differentiation (Nonstandard) *}
+section\<open>Differentiation (Nonstandard)\<close>
theory HDeriv
imports HLim
begin
-text{*Nonstandard Definitions*}
+text\<open>Nonstandard Definitions\<close>
definition
nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
@@ -30,7 +30,7 @@
inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
-subsection {* Derivatives *}
+subsection \<open>Derivatives\<close>
lemma DERIV_NS_iff:
"(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
@@ -66,9 +66,9 @@
apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
done
-text {*First NSDERIV in terms of NSLIM*}
+text \<open>First NSDERIV in terms of NSLIM\<close>
-text{*first equivalence *}
+text\<open>first equivalence\<close>
lemma NSDERIV_NSLIM_iff:
"(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
apply (simp add: nsderiv_def NSLIM_def, auto)
@@ -78,7 +78,7 @@
apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
done
-text{*second equivalence *}
+text\<open>second equivalence\<close>
lemma NSDERIV_NSLIM_iff2:
"(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D)"
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
@@ -136,8 +136,8 @@
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
done
-text{*Differentiability implies continuity
- nice and simple "algebraic" proof*}
+text\<open>Differentiability implies continuity
+ nice and simple "algebraic" proof\<close>
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
apply (drule approx_minus_iff [THEN iffD1])
@@ -155,16 +155,16 @@
intro: approx_trans approx_minus_iff [THEN iffD2])
done
-text{*Differentiation rules for combinations of functions
+text\<open>Differentiation rules for combinations of functions
follow from clear, straightforard, algebraic
- manipulations*}
-text{*Constant function*}
+ manipulations\<close>
+text\<open>Constant function\<close>
(* use simple constant nslimit theorem *)
lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)"
by (simp add: NSDERIV_NSLIM_iff)
-text{*Sum of functions- proved easily*}
+text\<open>Sum of functions- proved easily\<close>
lemma NSDERIV_add: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |]
==> NSDERIV (%x. f x + g x) x :> Da + Db"
@@ -174,8 +174,8 @@
apply (auto simp add: ac_simps algebra_simps)
done
-text{*Product of functions - Proof is trivial but tedious
- and long due to rearrangement of terms*}
+text\<open>Product of functions - Proof is trivial but tedious
+ and long due to rearrangement of terms\<close>
lemma lemma_nsderiv1:
fixes a b c d :: "'a::comm_ring star"
@@ -216,7 +216,7 @@
simp add: add.assoc [symmetric])
done
-text{*Multiplying by a constant*}
+text\<open>Multiplying by a constant\<close>
lemma NSDERIV_cmult: "NSDERIV f x :> D
==> NSDERIV (%x. c * f x) x :> c*D"
apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
@@ -224,7 +224,7 @@
apply (erule NSLIM_const [THEN NSLIM_mult])
done
-text{*Negation of function*}
+text\<open>Negation of function\<close>
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
proof (simp add: NSDERIV_NSLIM_iff)
assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
@@ -238,7 +238,7 @@
(\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
qed
-text{*Subtraction*}
+text\<open>Subtraction\<close>
lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"
by (blast dest: NSDERIV_add NSDERIV_minus)
@@ -246,12 +246,12 @@
"NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da-Db"
using NSDERIV_add_minus [of f x Da g Db] by simp
-text{* Similarly to the above, the chain rule admits an entirely
+text\<open>Similarly to the above, the chain rule admits an entirely
straightforward derivation. Compare this with Harrison's
HOL proof of the chain rule, which proved to be trickier and
required an alternative characterisation of differentiability-
the so-called Carathedory derivative. Our main problem is
- manipulation of terms.*}
+ manipulation of terms.\<close>
(* lemmas *)
@@ -312,7 +312,7 @@
thus ?thesis by (simp add: mult.assoc)
qed
-text{*This proof uses both definitions of differentiability.*}
+text\<open>This proof uses both definitions of differentiability.\<close>
lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
==> NSDERIV (f o g) x :> Da * Db"
apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
@@ -331,7 +331,7 @@
apply (blast intro: NSDERIVD2)
done
-text{*Differentiation of natural number powers*}
+text\<open>Differentiation of natural number powers\<close>
lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
@@ -340,7 +340,7 @@
lemma NSDERIV_inverse:
fixes x :: "'a::real_normed_field"
- assumes "x \<noteq> 0" -- {* can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero *}
+ assumes "x \<noteq> 0" \<comment> \<open>can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero\<close>
shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
proof -
{ fix h :: "'a star"
@@ -355,7 +355,7 @@
dest!: hypreal_of_real_HFinite_diff_Infinitesimal
simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
done
- moreover from not_0 `h \<noteq> 0` assms
+ moreover from not_0 \<open>h \<noteq> 0\<close> assms
have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
(inverse (star_of x + h) - inverse (star_of x)) / h"
apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
@@ -370,12 +370,12 @@
} then show ?thesis by (simp add: nsderiv_def)
qed
-subsubsection {* Equivalence of NS and Standard definitions *}
+subsubsection \<open>Equivalence of NS and Standard definitions\<close>
lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
by (simp add: divide_inverse mult.commute)
-text{*Now equivalence between NSDERIV and DERIV*}
+text\<open>Now equivalence between NSDERIV and DERIV\<close>
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
@@ -383,7 +383,7 @@
lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
by (simp add: NSDERIV_DERIV_iff DERIV_pow)
-text{*Derivative of inverse*}
+text\<open>Derivative of inverse\<close>
lemma NSDERIV_inverse_fun:
fixes x :: "'a::{real_normed_field}"
@@ -391,7 +391,7 @@
==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
-text{*Derivative of quotient*}
+text\<open>Derivative of quotient\<close>
lemma NSDERIV_quotient:
fixes x :: "'a::{real_normed_field}"
@@ -422,7 +422,7 @@
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
qed
-subsubsection {* Differentiability predicate *}
+subsubsection \<open>Differentiability predicate\<close>
lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
by (simp add: NSdifferentiable_def)
@@ -431,7 +431,7 @@
by (force simp add: NSdifferentiable_def)
-subsection {*(NS) Increment*}
+subsection \<open>(NS) Increment\<close>
lemma incrementI:
"f NSdifferentiable x ==>
increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
--- a/src/HOL/NSA/HLim.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HLim.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson
*)
-section{* Limits and Continuity (Nonstandard) *}
+section\<open>Limits and Continuity (Nonstandard)\<close>
theory HLim
imports Star
begin
-text{*Nonstandard Definitions*}
+text\<open>Nonstandard Definitions\<close>
definition
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
@@ -19,7 +19,7 @@
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
- --{*NS definition dispenses with limit notions*}
+ \<comment>\<open>NS definition dispenses with limit notions\<close>
"isNSCont f a = (\<forall>y. y @= star_of a -->
( *f* f) y @= star_of (f a))"
@@ -28,7 +28,7 @@
"isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
-subsection {* Limits of Functions *}
+subsection \<open>Limits of Functions\<close>
lemma NSLIM_I:
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
@@ -40,8 +40,8 @@
\<Longrightarrow> starfun f x \<approx> star_of L"
by (simp add: NSLIM_def)
-text{*Proving properties of limits using nonstandard definition.
- The properties hold for standard limits as well!*}
+text\<open>Proving properties of limits using nonstandard definition.
+ The properties hold for standard limits as well!\<close>
lemma NSLIM_mult:
fixes l m :: "'a::real_normed_algebra"
@@ -133,7 +133,7 @@
lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
by (simp add: NSLIM_def)
-subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
+subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
lemma LIM_NSLIM:
assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
@@ -194,7 +194,7 @@
by (blast intro: LIM_NSLIM NSLIM_LIM)
-subsection {* Continuity *}
+subsection \<open>Continuity\<close>
lemma isNSContD:
"\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
@@ -208,32 +208,32 @@
apply (case_tac "y = star_of a", auto)
done
-text{*NS continuity can be defined using NS Limit in
- similar fashion to standard def of continuity*}
+text\<open>NS continuity can be defined using NS Limit in
+ similar fashion to standard def of continuity\<close>
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
-text{*Hence, NS continuity can be given
- in terms of standard limit*}
+text\<open>Hence, NS continuity can be given
+ in terms of standard limit\<close>
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
-text{*Moreover, it's trivial now that NS continuity
- is equivalent to standard continuity*}
+text\<open>Moreover, it's trivial now that NS continuity
+ is equivalent to standard continuity\<close>
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
apply (simp add: isCont_def)
apply (rule isNSCont_LIM_iff)
done
-text{*Standard continuity ==> NS continuity*}
+text\<open>Standard continuity ==> NS continuity\<close>
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
by (erule isNSCont_isCont_iff [THEN iffD2])
-text{*NS continuity ==> Standard continuity*}
+text\<open>NS continuity ==> Standard continuity\<close>
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
by (erule isNSCont_isCont_iff [THEN iffD1])
-text{*Alternative definition of continuity*}
+text\<open>Alternative definition of continuity\<close>
(* Prove equivalence between NS limits - *)
(* seems easier than using standard def *)
@@ -269,7 +269,7 @@
done
-subsection {* Uniform Continuity *}
+subsection \<open>Uniform Continuity\<close>
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
by (simp add: isNSUCont_def)
--- a/src/HOL/NSA/HLog.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HLog.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,7 +3,7 @@
Copyright : 2000,2001 University of Edinburgh
*)
-section{*Logarithms: Non-Standard Version*}
+section\<open>Logarithms: Non-Standard Version\<close>
theory HLog
imports HTranscendental
--- a/src/HOL/NSA/HSEQ.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HSEQ.thy Wed Dec 30 11:37:29 2015 +0100
@@ -6,7 +6,7 @@
Additional contributions by Jeremy Avigad and Brian Huffman
*)
-section {* Sequences and Convergence (Nonstandard) *}
+section \<open>Sequences and Convergence (Nonstandard)\<close>
theory HSEQ
imports Limits NatStar
@@ -15,30 +15,30 @@
definition
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
- --{*Nonstandard definition of convergence of sequence*}
+ \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
"X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
definition
nslim :: "(nat => 'a::real_normed_vector) => 'a" where
- --{*Nonstandard definition of limit using choice operator*}
+ \<comment>\<open>Nonstandard definition of limit using choice operator\<close>
"nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
definition
NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
- --{*Nonstandard definition of convergence*}
+ \<comment>\<open>Nonstandard definition of convergence\<close>
"NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
definition
NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
- --{*Nonstandard definition for bounded sequence*}
+ \<comment>\<open>Nonstandard definition for bounded sequence\<close>
"NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
definition
NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
- --{*Nonstandard definition*}
+ \<comment>\<open>Nonstandard definition\<close>
"NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
-subsection {* Limits of Sequences *}
+subsection \<open>Limits of Sequences\<close>
lemma NSLIMSEQ_iff:
"(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
@@ -102,7 +102,7 @@
lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
-text{*Uniqueness of limit*}
+text\<open>Uniqueness of limit\<close>
lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
apply (simp add: NSLIMSEQ_def)
apply (drule HNatInfinite_whn [THEN [2] bspec])+
@@ -116,8 +116,8 @@
apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
done
-text{*We can now try and derive a few properties of sequences,
- starting with the limit comparison property for sequences.*}
+text\<open>We can now try and derive a few properties of sequences,
+ starting with the limit comparison property for sequences.\<close>
lemma NSLIMSEQ_le:
"[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
@@ -138,9 +138,9 @@
lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
-text{*Shift a convergent series by 1:
+text\<open>Shift a convergent series by 1:
By the equivalence between Cauchiness and convergence and because
- the successor of an infinite hypernatural is also infinite.*}
+ the successor of an infinite hypernatural is also infinite.\<close>
lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
apply (unfold NSLIMSEQ_def, safe)
@@ -159,7 +159,7 @@
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
-subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
+subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
lemma LIMSEQ_NSLIMSEQ:
assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
@@ -202,17 +202,17 @@
theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
-subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
+subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
-text{*We prove the NS version from the standard one, since the NS proof
- seems more complicated than the standard one above!*}
+text\<open>We prove the NS version from the standard one, since the NS proof
+ seems more complicated than the standard one above!\<close>
lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
-text{*Generalization to other limits*}
+text\<open>Generalization to other limits\<close>
lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
apply (simp add: NSLIMSEQ_def)
apply (auto intro: approx_hrabs
@@ -240,7 +240,7 @@
using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
-subsection {* Convergence *}
+subsection \<open>Convergence\<close>
lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
apply (simp add: nslim_def)
@@ -263,7 +263,7 @@
by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
-subsection {* Bounded Monotonic Sequences *}
+subsection \<open>Bounded Monotonic Sequences\<close>
lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *f* X) N : HFinite"
by (simp add: NSBseq_def)
@@ -281,7 +281,7 @@
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
by (simp add: NSBseq_def)
-text{*The standard definition implies the nonstandard definition*}
+text\<open>The standard definition implies the nonstandard definition\<close>
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
proof (unfold NSBseq_def, safe)
@@ -295,7 +295,7 @@
thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
qed
-text{*The nonstandard definition implies the standard definition*}
+text\<open>The nonstandard definition implies the standard definition\<close>
lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
apply (insert HInfinite_omega)
@@ -326,27 +326,27 @@
by (simp add: HFinite_HInfinite_iff)
qed
-text{* Equivalence of nonstandard and standard definitions
- for a bounded sequence*}
+text\<open>Equivalence of nonstandard and standard definitions
+ for a bounded sequence\<close>
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
-text{*A convergent sequence is bounded:
+text\<open>A convergent sequence is bounded:
Boundedness as a necessary condition for convergence.
- The nonstandard version has no existential, as usual *}
+ The nonstandard version has no existential, as usual\<close>
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
done
-text{*Standard Version: easily now proved using equivalence of NS and
- standard definitions *}
+text\<open>Standard Version: easily now proved using equivalence of NS and
+ standard definitions\<close>
lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
-subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
+subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
@@ -354,11 +354,11 @@
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
-subsubsection{*A Bounded and Monotonic Sequence Converges*}
+subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
-text{* The best of both worlds: Easier to prove this result as a standard
+text\<open>The best of both worlds: Easier to prove this result as a standard
theorem and then use equivalence to "transfer" it into the
- equivalent nonstandard form if needed!*}
+ equivalent nonstandard form if needed!\<close>
lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
@@ -370,7 +370,7 @@
Bseq_NSBseq_iff [symmetric])
-subsection {* Cauchy Sequences *}
+subsection \<open>Cauchy Sequences\<close>
lemma NSCauchyI:
"(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
@@ -382,7 +382,7 @@
\<Longrightarrow> starfun X M \<approx> starfun X N"
by (simp add: NSCauchy_def)
-subsubsection{*Equivalence Between NS and Standard*}
+subsubsection\<open>Equivalence Between NS and Standard\<close>
lemma Cauchy_NSCauchy:
assumes X: "Cauchy X" shows "NSCauchy X"
@@ -430,16 +430,16 @@
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
-subsubsection {* Cauchy Sequences are Bounded *}
+subsubsection \<open>Cauchy Sequences are Bounded\<close>
-text{*A Cauchy sequence is bounded -- nonstandard version*}
+text\<open>A Cauchy sequence is bounded -- nonstandard version\<close>
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
-subsubsection {* Cauchy Sequences are Convergent *}
+subsubsection \<open>Cauchy Sequences are Convergent\<close>
-text{*Equivalence of Cauchy criterion and convergence:
+text\<open>Equivalence of Cauchy criterion and convergence:
We will prove this using our NS formulation which provides a
much easier proof than using the standard definition. We do not
need to use properties of subsequences such as boundedness,
@@ -447,7 +447,7 @@
in HOL which is much longer and more complicated. Of course, we do
not have problems which he encountered with guessing the right
instantiations for his 'espsilon-delta' proof(s) in this case
- since the NS formulations do not involve existential quantifiers.*}
+ since the NS formulations do not involve existential quantifiers.\<close>
lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
@@ -479,13 +479,13 @@
by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
-subsection {* Power Sequences *}
+subsection \<open>Power Sequences\<close>
-text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
+text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and
- also fact that bounded and monotonic sequence converges.*}
+ also fact that bounded and monotonic sequence converges.\<close>
-text{* We now use NS criterion to bring proof of theorem through *}
+text\<open>We now use NS criterion to bring proof of theorem through\<close>
lemma NSLIMSEQ_realpow_zero:
"[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
--- a/src/HOL/NSA/HSeries.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy Wed Dec 30 11:37:29 2015 +0100
@@ -5,7 +5,7 @@
Converted to Isar and polished by lcp
*)
-section{*Finite Summation and Infinite Series for Hyperreals*}
+section\<open>Finite Summation and Infinite Series for Hyperreals\<close>
theory HSeries
imports HSEQ
@@ -31,11 +31,11 @@
lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N"
by (simp add: sumhr_def)
-text{*Base case in definition of @{term sumr}*}
+text\<open>Base case in definition of @{term sumr}\<close>
lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
unfolding sumhr_app by transfer simp
-text{*Recursive case in definition of @{term sumr}*}
+text\<open>Recursive case in definition of @{term sumr}\<close>
lemma sumhr_if:
"!!m n. sumhr(m,n+1,f) =
(if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
@@ -71,7 +71,7 @@
lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
unfolding sumhr_app by transfer (rule setsum_abs)
-text{* other general version also needed *}
+text\<open>other general version also needed\<close>
lemma sumhr_fun_hypnat_eq:
"(\<forall>r. m \<le> r & r < n --> f r = g r) -->
sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
@@ -94,10 +94,10 @@
unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl)
-subsection{*Nonstandard Sums*}
+subsection\<open>Nonstandard Sums\<close>
-text{*Infinite sums are obtained by summing to some infinite hypernatural
- (such as @{term whn})*}
+text\<open>Infinite sums are obtained by summing to some infinite hypernatural
+ (such as @{term whn})\<close>
lemma sumhr_hypreal_of_hypnat_omega:
"sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
by (simp add: sumhr_const)
@@ -179,7 +179,7 @@
simp add: sumhr_split_diff atLeast0LessThan[symmetric])
done
-text{*Terms of a convergent series tend to zero*}
+text\<open>Terms of a convergent series tend to zero\<close>
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
apply (drule bspec, auto)
@@ -187,7 +187,7 @@
apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
done
-text{*Nonstandard comparison test*}
+text\<open>Nonstandard comparison test\<close>
lemma NSsummable_comparison_test:
"[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
apply (fold summable_NSsummable_iff)
--- a/src/HOL/NSA/HTranscendental.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Wed Dec 30 11:37:29 2015 +0100
@@ -5,7 +5,7 @@
Converted to Isar and polished by lcp
*)
-section{*Nonstandard Extensions of Transcendental Functions*}
+section\<open>Nonstandard Extensions of Transcendental Functions\<close>
theory HTranscendental
imports Transcendental HSeries HDeriv
@@ -13,7 +13,7 @@
definition
exphr :: "real => hypreal" where
- --{*define exponential function using standard part *}
+ \<comment>\<open>define exponential function using standard part\<close>
"exphr x = st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
definition
@@ -25,7 +25,7 @@
"coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
-subsection{*Nonstandard Extension of Square Root Function*}
+subsection\<open>Nonstandard Extension of Square Root Function\<close>
lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
by (simp add: starfun star_n_zero_num)
@@ -592,7 +592,7 @@
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
-text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
+text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
lemma STAR_cos_Infinitesimal_approx:
fixes x :: "'a::{real_normed_field,banach} star"
@@ -603,7 +603,7 @@
done
lemma STAR_cos_Infinitesimal_approx2:
- fixes x :: hypreal --{*perhaps could be generalised, like many other hypreal results*}
+ fixes x :: hypreal \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
--- a/src/HOL/NSA/HyperDef.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HyperDef.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,7 +4,7 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)
-section{*Construction of Hyperreals Using Ultrafilters*}
+section\<open>Construction of Hyperreals Using Ultrafilters\<close>
theory HyperDef
imports Complex_Main HyperNat
@@ -22,12 +22,12 @@
definition
omega :: hypreal where
- -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
+ \<comment> \<open>an infinite number \<open>= [<1,2,3,...>]\<close>\<close>
"omega = star_n (\<lambda>n. real (Suc n))"
definition
epsilon :: hypreal where
- -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
+ \<comment> \<open>an infinitesimal number \<open>= [<1,1/2,1/3,...>]\<close>\<close>
"epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
notation (xsymbols)
@@ -35,7 +35,7 @@
epsilon ("\<epsilon>")
-subsection {* Real vector class instances *}
+subsection \<open>Real vector class instances\<close>
instantiation star :: (scaleR) scaleR
begin
@@ -103,7 +103,7 @@
by (simp add: Reals_def Standard_def)
-subsection {* Injection from @{typ hypreal} *}
+subsection \<open>Injection from @{typ hypreal}\<close>
definition
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
@@ -153,7 +153,7 @@
by transfer (rule of_real_eq_0_iff)
-subsection{*Properties of @{term starrel}*}
+subsection\<open>Properties of @{term starrel}\<close>
lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
by (simp add: starrel_def)
@@ -164,8 +164,8 @@
declare Abs_star_inject [simp] Abs_star_inverse [simp]
declare equiv_starrel [THEN eq_equiv_class_iff, simp]
-subsection{*@{term hypreal_of_real}:
- the Injection from @{typ real} to @{typ hypreal}*}
+subsection\<open>@{term hypreal_of_real}:
+ the Injection from @{typ real} to @{typ hypreal}\<close>
lemma inj_star_of: "inj star_of"
by (rule inj_onI, simp)
@@ -180,7 +180,7 @@
lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
by simp
-subsection{* Properties of @{term star_n} *}
+subsection\<open>Properties of @{term star_n}\<close>
lemma star_n_add:
"star_n X + star_n Y = star_n (%n. X n + Y n)"
@@ -222,13 +222,13 @@
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
by (simp add: omega_def star_n_zero_num star_n_less)
-subsection{*Existence of Infinite Hyperreal Number*}
+subsection\<open>Existence of Infinite Hyperreal Number\<close>
-text{*Existence of infinite number not corresponding to any real number.
-Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
+text\<open>Existence of infinite number not corresponding to any real number.
+Use assumption that member @{term FreeUltrafilterNat} is not finite.\<close>
-text{*A few lemmas first*}
+text\<open>A few lemmas first\<close>
lemma lemma_omega_empty_singleton_disj:
"{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
@@ -249,8 +249,8 @@
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
by (insert not_ex_hypreal_of_real_eq_omega, auto)
-text{*Existence of infinitesimal number also not corresponding to any
- real number*}
+text\<open>Existence of infinitesimal number also not corresponding to any
+ real number\<close>
lemma lemma_epsilon_empty_singleton_disj:
"{n::nat. x = inverse(real(Suc n))} = {} |
@@ -277,7 +277,7 @@
lemma hypreal_epsilon_gt_zero: "0 < epsilon"
by (simp add: hypreal_epsilon_inverse_omega)
-subsection{*Absolute Value Function for the Hyperreals*}
+subsection\<open>Absolute Value Function for the Hyperreals\<close>
lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)"
by (simp add: abs_if split: split_if_asm)
@@ -292,7 +292,7 @@
by (simp add: abs_if split add: split_if_asm)
-subsection{*Embedding the Naturals into the Hyperreals*}
+subsection\<open>Embedding the Naturals into the Hyperreals\<close>
abbreviation
hypreal_of_nat :: "nat => hypreal" where
@@ -309,20 +309,20 @@
lemma hypreal_of_nat: "hypreal_of_nat m = star_n (%n. real m)"
by (simp add: star_of_def [symmetric])
-declaration {*
+declaration \<open>
K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
@{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
#> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
@{thm star_of_numeral}, @{thm star_of_add},
@{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
#> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
-*}
+\<close>
simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
- {* K Lin_Arith.simproc *}
+ \<open>K Lin_Arith.simproc\<close>
-subsection {* Exponentials on the Hyperreals *}
+subsection \<open>Exponentials on the Hyperreals\<close>
lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
by (rule power_0)
@@ -349,7 +349,7 @@
by arith
-text{*FIXME: DELETE THESE*}
+text\<open>FIXME: DELETE THESE\<close>
lemma hypreal_three_squares_add_zero_iff:
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
@@ -397,7 +397,7 @@
done
*)
-subsection{*Powers with Hypernatural Exponents*}
+subsection\<open>Powers with Hypernatural Exponents\<close>
definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
@@ -478,7 +478,7 @@
"\<bar>x::'a::{linordered_idom} star\<bar> pow 2 = x pow 2"
by (simp add: hyperpow_hrabs)
-text{*The precondition could be weakened to @{term "0\<le>x"}*}
+text\<open>The precondition could be weakened to @{term "0\<le>x"}\<close>
lemma hypreal_mult_less_mono:
"[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y"
by (simp add: mult_strict_mono order_less_imp_le)
--- a/src/HOL/NSA/HyperNat.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/HyperNat.thy Wed Dec 30 11:37:29 2015 +0100
@@ -5,7 +5,7 @@
Converted to Isar and polished by lcp
*)
-section{*Hypernatural numbers*}
+section\<open>Hypernatural numbers\<close>
theory HyperNat
imports StarDef
@@ -21,7 +21,7 @@
hSuc :: "hypnat => hypnat" where
hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
-subsection{*Properties Transferred from Naturals*}
+subsection\<open>Properties Transferred from Naturals\<close>
lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
by transfer (rule Suc_not_Zero)
@@ -128,7 +128,7 @@
lemma hypnat_diff_split:
"P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
- -- {* elimination of @{text -} on @{text hypnat} *}
+ \<comment> \<open>elimination of \<open>-\<close> on \<open>hypnat\<close>\<close>
proof (cases "a<b" rule: case_split)
case True
thus ?thesis
@@ -140,7 +140,7 @@
by (auto simp add: linorder_not_less dest: order_le_less_trans)
qed
-subsection{*Properties of the set of embedded natural numbers*}
+subsection\<open>Properties of the set of embedded natural numbers\<close>
lemma of_nat_eq_star_of [simp]: "of_nat = star_of"
proof
@@ -173,7 +173,7 @@
by (simp add: Nats_eq_Standard)
-subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
+subsection\<open>Infinite Hypernatural Numbers -- @{term HNatInfinite}\<close>
definition
(* the set of infinite hypernatural numbers *)
@@ -209,7 +209,7 @@
lemma star_of_le_HNatInfinite: "N \<in> HNatInfinite \<Longrightarrow> star_of n \<le> N"
by (rule star_of_less_HNatInfinite [THEN order_less_imp_le])
-subsubsection {* Closure Rules *}
+subsubsection \<open>Closure Rules\<close>
lemma Nats_less_HNatInfinite: "\<lbrakk>x \<in> Nats; y \<in> HNatInfinite\<rbrakk> \<Longrightarrow> x < y"
by (auto simp add: Nats_def star_of_less_HNatInfinite)
@@ -266,7 +266,7 @@
done
-subsection{*Existence of an infinite hypernatural number*}
+subsection\<open>Existence of an infinite hypernatural number\<close>
definition
(* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
@@ -315,9 +315,9 @@
by (simp add: Nats_less_whn)
-subsubsection{*Alternative characterization of the set of infinite hypernaturals*}
+subsubsection\<open>Alternative characterization of the set of infinite hypernaturals\<close>
-text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
+text\<open>@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}\<close>
(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
lemma HNatInfinite_FreeUltrafilterNat_lemma:
@@ -337,8 +337,8 @@
done
-subsubsection{*Alternative Characterization of @{term HNatInfinite} using
-Free Ultrafilter*}
+subsubsection\<open>Alternative Characterization of @{term HNatInfinite} using
+Free Ultrafilter\<close>
lemma HNatInfinite_FreeUltrafilterNat:
"star_n X \<in> HNatInfinite ==> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
@@ -356,7 +356,7 @@
by (rule iffI [OF HNatInfinite_FreeUltrafilterNat
FreeUltrafilterNat_HNatInfinite])
-subsection {* Embedding of the Hypernaturals into other types *}
+subsection \<open>Embedding of the Hypernaturals into other types\<close>
definition
of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
--- a/src/HOL/NSA/NSA.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, University of Cambridge
*)
-section{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
+section\<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
theory NSA
imports HyperDef "~~/src/HOL/Library/Lub_Glb"
@@ -27,12 +27,12 @@
definition
approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
- --{*the `infinitely close' relation*}
+ \<comment>\<open>the `infinitely close' relation\<close>
"(x @= y) = ((x - y) \<in> Infinitesimal)"
definition
st :: "hypreal => hypreal" where
- --{*the standard part of a hyperreal*}
+ \<comment>\<open>the standard part of a hyperreal\<close>
"st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
definition
@@ -49,7 +49,7 @@
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 *}
+subsection \<open>Nonstandard Extension of the Norm Function\<close>
definition
scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
@@ -171,7 +171,7 @@
apply (simp add: mult_strict_mono')
done
-subsection{*Closure Laws for the Standard Reals*}
+subsection\<open>Closure Laws for the Standard Reals\<close>
lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
apply auto
@@ -190,7 +190,7 @@
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*}
+text\<open>epsilon 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])
@@ -225,7 +225,7 @@
apply (drule dense, auto)
done
-text{*Completeness of Reals, but both lemmas are unused.*}
+text\<open>Completeness of Reals, but both lemmas are unused.\<close>
lemma SReal_sup_lemma:
"P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
@@ -244,7 +244,7 @@
done
-subsection{* Set of Finite Elements is a Subring of the Extended Reals*}
+subsection\<open>Set of Finite Elements is a Subring of the Extended Reals\<close>
lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
apply (simp add: HFinite_def)
@@ -315,7 +315,7 @@
done
-subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}
+subsection\<open>Set of Infinitesimals is a Subring of the Hyperreals\<close>
lemma InfinitesimalI:
"(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal"
@@ -609,7 +609,7 @@
by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])
-subsection{*The Infinitely Close Relation*}
+subsection\<open>The Infinitely Close Relation\<close>
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
by (simp add: Infinitesimal_def approx_def)
@@ -651,7 +651,7 @@
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
simproc_setup approx_reorient_simproc
("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
-{*
+\<open>
let val rule = @{thm approx_reorient} RS eq_reflection
fun proc phi ss ct =
case Thm.term_of ct of
@@ -659,7 +659,7 @@
else if can HOLogic.dest_number t then SOME rule else NONE
| _ => NONE
in proc end
-*}
+\<close>
lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
@@ -901,7 +901,7 @@
qed
-subsection{* Zero is the Only Infinitesimal that is also a Real*}
+subsection\<open>Zero is the Only Infinitesimal that is also a Real\<close>
lemma Infinitesimal_less_SReal:
"[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
@@ -1004,7 +1004,7 @@
close to a unique real number (i.e a member of Reals)
------------------------------------------------------------------*)
-subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
+subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
apply safe
@@ -1061,9 +1061,9 @@
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
-subsection{* Existence of Unique Real Infinitely Close*}
+subsection\<open>Existence of Unique Real Infinitely Close\<close>
-subsubsection{*Lifting of the Ub and Lub Properties*}
+subsubsection\<open>Lifting of the Ub and Lub Properties\<close>
lemma hypreal_of_real_isUb_iff:
"(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
@@ -1255,7 +1255,7 @@
-text{*Existence of real and Standard Part Theorem*}
+text\<open>Existence of real and Standard Part Theorem\<close>
lemma lemma_st_part_Ex:
"(x::hypreal) \<in> HFinite
==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
@@ -1270,14 +1270,14 @@
apply (drule lemma_st_part_Ex, auto)
done
-text{*There is a unique real infinitely close*}
+text\<open>There is a unique real infinitely close\<close>
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)
done
-subsection{* Finite, Infinite and Infinitesimal*}
+subsection\<open>Finite, Infinite and Infinitesimal\<close>
lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
apply (simp add: HFinite_def HInfinite_def)
@@ -1487,7 +1487,7 @@
by (cut_tac x = x in hrabs_disj, auto)
-subsection{*Theorems about Monads*}
+subsection\<open>Theorems about Monads\<close>
lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)"
by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
@@ -1514,7 +1514,7 @@
by (simp add: monad_def)
-subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*}
+subsection\<open>Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}\<close>
lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
apply (simp (no_asm))
@@ -1609,7 +1609,7 @@
apply (auto intro: approx_trans2)
done
-subsection {* More @{term HFinite} and @{term Infinitesimal} Theorems *}
+subsection \<open>More @{term HFinite} and @{term Infinitesimal} Theorems\<close>
(* interesting slightly counterintuitive theorem: necessary
for proving that an open interval is an NS open set
@@ -1753,7 +1753,7 @@
done
-subsection{* Theorems about Standard Part*}
+subsection\<open>Theorems about Standard Part\<close>
lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
apply (simp add: st_def)
@@ -1909,9 +1909,9 @@
-subsection {* Alternative Definitions using Free Ultrafilter *}
+subsection \<open>Alternative Definitions using Free Ultrafilter\<close>
-subsubsection {* @{term HFinite} *}
+subsubsection \<open>@{term HFinite}\<close>
lemma HFinite_FreeUltrafilterNat:
"star_n X \<in> HFinite
@@ -1936,7 +1936,7 @@
"(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
-subsubsection {* @{term HInfinite} *}
+subsubsection \<open>@{term HInfinite}\<close>
lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}"
by auto
@@ -1996,7 +1996,7 @@
"(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
-subsubsection {* @{term Infinitesimal} *}
+subsubsection \<open>@{term Infinitesimal}\<close>
lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
by (unfold SReal_def, auto)
@@ -2050,9 +2050,9 @@
done
-subsection{*Proof that @{term omega} is an infinite number*}
+subsection\<open>Proof that @{term omega} is an infinite number\<close>
-text{*It will follow that epsilon is an infinitesimal number.*}
+text\<open>It will follow that epsilon 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,7 +2100,7 @@
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{*@{term omega} is a member of @{term HInfinite}*}
+text\<open>@{term omega} is a member of @{term HInfinite}\<close>
theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
apply (simp add: omega_def)
@@ -2176,21 +2176,21 @@
by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
(simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
-text{* Example of an hypersequence (i.e. an extended standard sequence)
+text\<open>Example of an hypersequence (i.e. an extended standard sequence)
whose term with an hypernatural suffix is an infinitesimal i.e.
- the whn'nth term of the hypersequence is a member of Infinitesimal*}
+ the whn'nth term of the hypersequence is a member of Infinitesimal\<close>
lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
-text{* Example where we get a hyperreal from a real sequence
+text\<open>Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
used in proofs about equivalence of nonstandard and
standard neighbourhoods. Also used for equivalence of
nonstandard ans standard definitions of pointwise
- limit.*}
+ limit.\<close>
(*-----------------------------------------------------
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
--- a/src/HOL/NSA/NSCA.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/NSCA.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,7 +3,7 @@
Copyright : 2001,2002 University of Edinburgh
*)
-section{*Non-Standard Complex Analysis*}
+section\<open>Non-Standard Complex Analysis\<close>
theory NSCA
imports NSComplex HTranscendental
@@ -14,12 +14,12 @@
SComplex :: "hcomplex set" where
"SComplex \<equiv> Standard"
-definition --{* standard part map*}
+definition \<comment>\<open>standard part map\<close>
stc :: "hcomplex => hcomplex" where
"stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
-subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
+subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
by (auto, drule Standard_minus, auto)
@@ -68,7 +68,7 @@
done
-subsection{*The Finite Elements form a Subring*}
+subsection\<open>The Finite Elements form a Subring\<close>
lemma HFinite_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) \<in> HFinite"
@@ -82,7 +82,7 @@
by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
-subsection{*The Complex Infinitesimals form a Subring*}
+subsection\<open>The Complex Infinitesimals form a Subring\<close>
lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
by auto
@@ -121,7 +121,7 @@
by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
-subsection{*The ``Infinitely Close'' Relation*}
+subsection\<open>The ``Infinitely Close'' Relation\<close>
(*
Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
@@ -183,7 +183,7 @@
done
-subsection{*Zero is the Only Infinitesimal Complex Number*}
+subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>
lemma Infinitesimal_less_SComplex:
"[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
@@ -229,7 +229,7 @@
"[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
-subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}
+subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
@@ -360,13 +360,13 @@
hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
-subsection{*Theorems About Monads*}
+subsection\<open>Theorems About Monads\<close>
lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"
by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
-subsection{*Theorems About Standard Part*}
+subsection\<open>Theorems About Standard Part\<close>
lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
apply (simp add: stc_def)
--- a/src/HOL/NSA/NSComplex.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy Wed Dec 30 11:37:29 2015 +0100
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson
*)
-section{*Nonstandard Complex Numbers*}
+section\<open>Nonstandard Complex Numbers\<close>
theory NSComplex
imports NSA
@@ -118,7 +118,7 @@
by (rule hnorm_def)
-subsection{*Properties of Nonstandard Real and Imaginary Parts*}
+subsection\<open>Properties of Nonstandard Real and Imaginary Parts\<close>
lemma hcomplex_hRe_hIm_cancel_iff:
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
@@ -141,7 +141,7 @@
by transfer simp
-subsection{*Addition for Nonstandard Complex Numbers*}
+subsection\<open>Addition for Nonstandard Complex Numbers\<close>
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
by transfer simp
@@ -149,7 +149,7 @@
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
by transfer simp
-subsection{*More Minus Laws*}
+subsection\<open>More Minus Laws\<close>
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
by transfer (rule uminus_complex.sel)
@@ -173,7 +173,7 @@
by transfer (rule complex_i_not_zero)
-subsection{*More Multiplication Laws*}
+subsection\<open>More Multiplication Laws\<close>
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
by simp
@@ -190,14 +190,14 @@
by simp
-subsection{*Subraction and Division*}
+subsection\<open>Subraction and Division\<close>
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
(* TODO: delete *)
by (rule diff_eq_eq)
-subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
+subsection\<open>Embedding Properties for @{term hcomplex_of_hypreal} Map\<close>
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
by transfer (rule Re_complex_of_real)
@@ -209,7 +209,7 @@
"hcomplex_of_hypreal epsilon \<noteq> 0"
by (simp add: hypreal_epsilon_not_zero)
-subsection{*HComplex theorems*}
+subsection\<open>HComplex theorems\<close>
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
by transfer simp
@@ -225,7 +225,7 @@
by (rule hcomplex_surj [THEN subst], blast)
-subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
+subsection\<open>Modulus (Absolute Value) of Nonstandard Complex Number\<close>
lemma hcomplex_of_hypreal_abs:
"hcomplex_of_hypreal \<bar>x\<bar> =
@@ -282,7 +282,7 @@
by transfer (rule complex_of_real_i)
-subsection{*Conjugation*}
+subsection\<open>Conjugation\<close>
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
by transfer (rule complex_cnj_cancel_iff)
@@ -329,7 +329,7 @@
by transfer (rule complex_mult_cnj)
-subsection{*More Theorems about the Function @{term hcmod}*}
+subsection\<open>More Theorems about the Function @{term hcmod}\<close>
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
@@ -350,7 +350,7 @@
by transfer (rule norm_diff_ineq)
-subsection{*Exponentiation*}
+subsection\<open>Exponentiation\<close>
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)"
by (rule power_0)
@@ -392,7 +392,7 @@
"r pow n = (0::hcomplex) ==> r = 0"
by (blast intro: ccontr dest: hcpow_not_zero)
-subsection{*The Function @{term hsgn}*}
+subsection\<open>The Function @{term hsgn}\<close>
lemma hsgn_zero [simp]: "hsgn 0 = 0"
by transfer (rule sgn_zero)
@@ -466,7 +466,7 @@
by transfer (rule of_real_eq_0_iff)
-subsection{*Polar Form for Nonstandard Complex Numbers*}
+subsection\<open>Polar Form for Nonstandard Complex Numbers\<close>
lemma complex_split_polar2:
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))"
@@ -599,8 +599,8 @@
by transfer (rule exp_add)
-subsection{*@{term hcomplex_of_complex}: the Injection from
- type @{typ complex} to to @{typ hcomplex}*}
+subsection\<open>@{term hcomplex_of_complex}: the Injection from
+ type @{typ complex} to to @{typ hcomplex}\<close>
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
by (rule iii_def)
@@ -618,7 +618,7 @@
by transfer (rule refl)
-subsection{*Numerals and Arithmetic*}
+subsection\<open>Numerals and Arithmetic\<close>
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
"hcomplex_of_hypreal (hypreal_of_real x) =
--- a/src/HOL/NSA/NatStar.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/NatStar.thy Wed Dec 30 11:37:29 2015 +0100
@@ -5,7 +5,7 @@
Converted to Isar and polished by lcp
*)
-section{*Star-transforms for the Hypernaturals*}
+section\<open>Star-transforms for the Hypernaturals\<close>
theory NatStar
imports Star
@@ -72,10 +72,10 @@
by (auto intro: InternalSets_Compl)
-subsection{*Nonstandard Extensions of Functions*}
+subsection\<open>Nonstandard Extensions of Functions\<close>
-text{* Example of transfer of a property from reals to hyperreals
- --- used for limit comparison of sequences*}
+text\<open>Example of transfer of a property from reals to hyperreals
+ --- used for limit comparison of sequences\<close>
lemma starfun_le_mono:
"\<forall>n. N \<le> n --> f n \<le> g n
@@ -88,18 +88,18 @@
==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
by transfer
-text{*Nonstandard extension when we increment the argument by one*}
+text\<open>Nonstandard extension when we increment the argument by one\<close>
lemma starfun_shift_one:
"!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
by (transfer, simp)
-text{*Nonstandard extension with absolute value*}
+text\<open>Nonstandard extension with absolute value\<close>
lemma starfun_abs: "!!N. ( *f* (%n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
by (transfer, rule refl)
-text{*The hyperpow function as a nonstandard extension of realpow*}
+text\<open>The hyperpow function as a nonstandard extension of realpow\<close>
lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
by (transfer, rule refl)
@@ -111,8 +111,8 @@
lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
by (transfer, rule refl)
-text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
- @{term real_of_nat} *}
+text\<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
+ @{term real_of_nat}\<close>
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
by transfer (simp add: fun_eq_iff)
@@ -125,12 +125,12 @@
apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
done
-text{*Internal functions - some redundancy with *f* now*}
+text\<open>Internal functions - some redundancy with *f* now\<close>
lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
by (simp add: starfun_n_def Ifun_star_n)
-text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
+text\<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
lemma starfun_n_mult:
"( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
@@ -138,7 +138,7 @@
apply (simp add: starfun_n star_n_mult)
done
-text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
+text\<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
lemma starfun_n_add:
"( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
@@ -146,7 +146,7 @@
apply (simp add: starfun_n star_n_add)
done
-text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
+text\<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
lemma starfun_n_add_minus:
"( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
@@ -155,7 +155,7 @@
done
-text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
+text\<open>Composition: \<open>( *fn) o ( *gn) = *(fn o gn)\<close>\<close>
lemma starfun_n_const_fun [simp]:
"( *fn* (%i x. k)) z = star_of k"
@@ -183,7 +183,7 @@
done
-subsection{*Nonstandard Characterization of Induction*}
+subsection\<open>Nonstandard Characterization of Induction\<close>
lemma hypnat_induct_obj:
"!!n. (( *p* P) (0::hypnat) &
@@ -221,7 +221,7 @@
apply (erule nonempty_set_star_has_least)
done
-text{* Goldblatt page 129 Thm 11.3.2*}
+text\<open>Goldblatt page 129 Thm 11.3.2\<close>
lemma internal_induct_lemma:
"!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
==> Iset X = (UNIV:: hypnat set)"
--- a/src/HOL/NSA/Star.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/Star.thy Wed Dec 30 11:37:29 2015 +0100
@@ -4,7 +4,7 @@
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
*)
-section{*Star-Transforms in Non-Standard Analysis*}
+section\<open>Star-Transforms in Non-Standard Analysis\<close>
theory Star
imports NSA
@@ -48,7 +48,7 @@
apply (blast intro: LeastI)
done
-subsection{*Properties of the Star-transform Applied to Sets of Reals*}
+subsection\<open>Properties of the Star-transform Applied to Sets of Reals\<close>
lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
by auto
@@ -83,8 +83,8 @@
lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
by (erule rev_subsetD, simp)
-text{*Nonstandard extension of a set (defined using a constant
- sequence) as a special case of an internal set*}
+text\<open>Nonstandard extension of a set (defined using a constant
+ sequence) as a special case of an internal set\<close>
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
apply (drule fun_eq_iff [THEN iffD2])
@@ -127,7 +127,7 @@
apply (simp add: Ifun_star_n star_n_eq_iff)
done
-text{*Nonstandard extension of functions*}
+text\<open>Nonstandard extension of functions\<close>
lemma starfun:
"( *f* f) (star_n X) = star_n (%n. f (X n))"
@@ -178,11 +178,11 @@
lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
by (transfer o_def, rule refl)
-text{*NS extension of constant function*}
+text\<open>NS extension of constant function\<close>
lemma starfun_const_fun [simp]: "!!x. ( *f* (%x. k)) x = star_of k"
by (transfer, rule refl)
-text{*the NS extension of the identity function*}
+text\<open>the NS extension of the identity function\<close>
lemma starfun_Id [simp]: "!!x. ( *f* (%x. x)) x = x"
by (transfer, rule refl)
@@ -192,7 +192,7 @@
"x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
by (simp only: starfun_Id)
-text{*The Star-function is a (nonstandard) extension of the function*}
+text\<open>The Star-function is a (nonstandard) extension of the function\<close>
lemma is_starext_starfun: "is_starext ( *f* f) f"
apply (simp add: is_starext_def, auto)
@@ -202,7 +202,7 @@
simp add: starfun star_n_eq_iff)
done
-text{*Any nonstandard extension is in fact the Star-function*}
+text\<open>Any nonstandard extension is in fact the Star-function\<close>
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
apply (simp add: is_starext_def)
@@ -218,9 +218,9 @@
lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
by (blast intro: is_starfun_starext is_starext_starfun)
-text{*extented function has same solution as its standard
+text\<open>extented function has same solution as its standard
version for real arguments. i.e they are the same
- for all real arguments*}
+ for all real arguments\<close>
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
by (rule starfun_star_of)
@@ -249,8 +249,8 @@
|] ==> ( *f* (%x. f x + g x)) x @= l + m"
by (auto intro: approx_add)
-text{*Examples: hrabs is nonstandard extension of rabs
- inverse is nonstandard extension of inverse*}
+text\<open>Examples: hrabs is nonstandard extension of rabs
+ inverse is nonstandard extension of inverse\<close>
(* can be proved easily using theorem "starfun" and *)
(* properties of ultrafilter as for inverse below we *)
@@ -273,22 +273,22 @@
lemma starfun_inverse2: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
by (transfer, rule refl)
-text{*General lemma/theorem needed for proofs in elementary
- topology of the reals*}
+text\<open>General lemma/theorem needed for proofs in elementary
+ topology of the reals\<close>
lemma starfun_mem_starset:
"!!x. ( *f* f) x : *s* A ==> x : *s* {x. f x \<in> A}"
by (transfer, simp)
-text{*Alternative definition for hrabs with rabs function
+text\<open>Alternative definition for hrabs with rabs function
applied entrywise to equivalence class representative.
- This is easily proved using starfun and ns extension thm*}
+ This is easily proved using starfun and ns extension thm\<close>
lemma hypreal_hrabs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
by (simp only: starfun_rabs_hrabs [symmetric] starfun)
-text{*nonstandard extension of set through nonstandard extension
+text\<open>nonstandard extension of set through nonstandard extension
of rabs function i.e hrabs. A more general result should be
where we replace rabs by some arbitrary function f and hrabs
- by its NS extenson. See second NS set extension below.*}
+ by its NS extenson. See second NS set extension below.\<close>
lemma STAR_rabs_add_minus:
"*s* {x. \<bar>x + - y\<bar> < r} = {x. \<bar>x + -star_of y\<bar> < star_of r}"
by (transfer, rule refl)
@@ -298,9 +298,9 @@
{x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
by (transfer, rule refl)
-text{*Another characterization of Infinitesimal and one of @= relation.
- In this theory since @{text hypreal_hrabs} proved here. Maybe
- move both theorems??*}
+text\<open>Another characterization of Infinitesimal and one of @= relation.
+ In this theory since \<open>hypreal_hrabs\<close> proved here. Maybe
+ move both theorems??\<close>
lemma Infinitesimal_FreeUltrafilterNat_iff2:
"(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
--- a/src/HOL/NSA/StarDef.thy Wed Dec 30 11:32:56 2015 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Dec 30 11:37:29 2015 +0100
@@ -2,13 +2,13 @@
Author : Jacques D. Fleuriot and Brian Huffman
*)
-section {* Construction of Star Types Using Ultrafilters *}
+section \<open>Construction of Star Types Using Ultrafilters\<close>
theory StarDef
imports Free_Ultrafilter
begin
-subsection {* A Free Ultrafilter over the Naturals *}
+subsection \<open>A Free Ultrafilter over the Naturals\<close>
definition
FreeUltrafilterNat :: "nat filter" ("\<U>") where
@@ -24,7 +24,7 @@
interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
by (rule freeultrafilter_FreeUltrafilterNat)
-subsection {* Definition of @{text star} type constructor *}
+subsection \<open>Definition of \<open>star\<close> type constructor\<close>
definition
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
@@ -49,7 +49,7 @@
lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
by (auto, rule_tac x=x in star_cases, auto)
-text {* Proving that @{term starrel} is an equivalence relation *}
+text \<open>Proving that @{term starrel} is an equivalence relation\<close>
lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
by (simp add: starrel_def)
@@ -71,23 +71,23 @@
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
-subsection {* Transfer principle *}
+subsection \<open>Transfer principle\<close>
-text {* This introduction rule starts each transfer proof. *}
+text \<open>This introduction rule starts each transfer proof.\<close>
lemma transfer_start:
"P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
by (simp add: FreeUltrafilterNat.proper)
-text {*Initialize transfer tactic.*}
+text \<open>Initialize transfer tactic.\<close>
ML_file "transfer.ML"
-method_setup transfer = {*
+method_setup transfer = \<open>
Attrib.thms >> (fn ths => fn ctxt =>
SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
-*} "transfer principle"
+\<close> "transfer principle"
-text {* Transfer introduction rules. *}
+text \<open>Transfer introduction rules.\<close>
lemma transfer_ex [transfer_intro]:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
@@ -152,7 +152,7 @@
by (simp add: FreeUltrafilterNat.proper)
-subsection {* Standard elements *}
+subsection \<open>Standard elements\<close>
definition
star_of :: "'a \<Rightarrow> 'a star" where
@@ -162,8 +162,8 @@
Standard :: "'a star set" where
"Standard = range star_of"
-text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* Transfer_Principle.add_const @{const_name star_of} *}
+text \<open>Transfer tactic should remove occurrences of @{term star_of}\<close>
+setup \<open>Transfer_Principle.add_const @{const_name star_of}\<close>
declare star_of_def [transfer_intro]
@@ -174,7 +174,7 @@
by (simp add: Standard_def)
-subsection {* Internal functions *}
+subsection \<open>Internal functions\<close>
definition
Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
@@ -189,8 +189,8 @@
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
-text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* Transfer_Principle.add_const @{const_name Ifun} *}
+text \<open>Transfer tactic should remove occurrences of @{term Ifun}\<close>
+setup \<open>Transfer_Principle.add_const @{const_name Ifun}\<close>
lemma transfer_Ifun [transfer_intro]:
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -203,7 +203,7 @@
"\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard"
by (auto simp add: Standard_def)
-text {* Nonstandard extensions of functions *}
+text \<open>Nonstandard extensions of functions\<close>
definition
starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)" ("*f* _" [80] 80) where
@@ -285,7 +285,7 @@
qed
-subsection {* Internal predicates *}
+subsection \<open>Internal predicates\<close>
definition unstar :: "bool star \<Rightarrow> bool" where
"unstar b \<longleftrightarrow> b = star_of True"
@@ -296,8 +296,8 @@
lemma unstar_star_of [simp]: "unstar (star_of p) = p"
by (simp add: unstar_def star_of_inject)
-text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* Transfer_Principle.add_const @{const_name unstar} *}
+text \<open>Transfer tactic should remove occurrences of @{term unstar}\<close>
+setup \<open>Transfer_Principle.add_const @{const_name unstar}\<close>
lemma transfer_unstar [transfer_intro]:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
@@ -328,7 +328,7 @@
by (transfer, rule refl)
-subsection {* Internal sets *}
+subsection \<open>Internal sets\<close>
definition
Iset :: "'a set star \<Rightarrow> 'a star set" where
@@ -338,8 +338,8 @@
"(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
by (simp add: Iset_def starP2_star_n)
-text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* Transfer_Principle.add_const @{const_name Iset} *}
+text \<open>Transfer tactic should remove occurrences of @{term Iset}\<close>
+setup \<open>Transfer_Principle.add_const @{const_name Iset}\<close>
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
@@ -370,7 +370,7 @@
"\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
by simp
-text {* Nonstandard extensions of sets. *}
+text \<open>Nonstandard extensions of sets.\<close>
definition
starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80) where
@@ -423,7 +423,7 @@
starset_subset starset_eq
-subsection {* Syntactic classes *}
+subsection \<open>Syntactic classes\<close>
instantiation star :: (zero) zero
begin
@@ -557,7 +557,7 @@
star_le_def star_less_def star_abs_def star_sgn_def
star_mod_def
-text {* Class operations preserve standard elements *}
+text \<open>Class operations preserve standard elements\<close>
lemma Standard_zero: "0 \<in> Standard"
by (simp add: star_zero_def)
@@ -595,7 +595,7 @@
Standard_mult Standard_divide Standard_inverse
Standard_abs Standard_mod
-text {* @{term star_of} preserves class operations *}
+text \<open>@{term star_of} preserves class operations\<close>
lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
by transfer (rule refl)
@@ -621,7 +621,7 @@
lemma star_of_abs: "star_of \<bar>x\<bar> = \<bar>star_of x\<bar>"
by transfer (rule refl)
-text {* @{term star_of} preserves numerals *}
+text \<open>@{term star_of} preserves numerals\<close>
lemma star_of_zero: "star_of 0 = 0"
by transfer (rule refl)
@@ -629,7 +629,7 @@
lemma star_of_one: "star_of 1 = 1"
by transfer (rule refl)
-text {* @{term star_of} preserves orderings *}
+text \<open>@{term star_of} preserves orderings\<close>
lemma star_of_less: "(star_of x < star_of y) = (x < y)"
by transfer (rule refl)
@@ -640,7 +640,7 @@
lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
by transfer (rule refl)
-text{*As above, for 0*}
+text\<open>As above, for 0\<close>
lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
lemmas star_of_0_le = star_of_le [of 0, simplified star_of_zero]
@@ -650,7 +650,7 @@
lemmas star_of_le_0 = star_of_le [of _ 0, simplified star_of_zero]
lemmas star_of_eq_0 = star_of_eq [of _ 0, simplified star_of_zero]
-text{*As above, for 1*}
+text\<open>As above, for 1\<close>
lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
lemmas star_of_1_le = star_of_le [of 1, simplified star_of_one]
@@ -671,7 +671,7 @@
star_of_1_less star_of_1_le star_of_1_eq
star_of_less_1 star_of_le_1 star_of_eq_1
-subsection {* Ordering and lattice classes *}
+subsection \<open>Ordering and lattice classes\<close>
instance star :: (order) order
apply (intro_classes)
@@ -752,7 +752,7 @@
by transfer (rule refl)
-subsection {* Ordered group classes *}
+subsection \<open>Ordered group classes\<close>
instance star :: (semigroup_add) semigroup_add
by (intro_classes, transfer, rule add.assoc)
@@ -815,7 +815,7 @@
instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
-subsection {* Ring and field classes *}
+subsection \<open>Ring and field classes\<close>
instance star :: (semiring) semiring
by (intro_classes; transfer) (fact distrib_right distrib_left)+
@@ -913,7 +913,7 @@
instance star :: (linordered_idom) linordered_idom ..
instance star :: (linordered_field) linordered_field ..
-subsection {* Power *}
+subsection \<open>Power\<close>
lemma star_power_def [transfer_unfold]:
"(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
@@ -940,7 +940,7 @@
by transfer (rule refl)
-subsection {* Number classes *}
+subsection \<open>Number classes\<close>
instance star :: (numeral) numeral ..
@@ -1046,7 +1046,7 @@
declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
-subsection {* Finite class *}
+subsection \<open>Finite class\<close>
lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
by (erule finite_induct, simp_all)