--- a/src/HOL/Analysis/Bochner_Integration.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Tue Jan 17 13:59:10 2017 +0100
@@ -1931,9 +1931,9 @@
integral\<^sup>L M f \<le> integral\<^sup>L M g"
by (intro integral_mono_AE) auto
-text {*The next two statements are useful to bound Lebesgue integrals, as they avoid one
+text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
integrability assumption. The price to pay is that the upper function has to be nonnegative,
-but this is often true and easy to check in computations.*}
+but this is often true and easy to check in computations.\<close>
lemma integral_mono_AE':
fixes f::"_ \<Rightarrow> real"
@@ -2047,20 +2047,20 @@
shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
proof -
have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
- by (rule nn_integral_mono_AE, auto simp add: `c>0` less_eq_real_def)
+ by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
also have "... = (\<integral>x. u x \<partial>M)"
by (rule nn_integral_eq_integral, auto simp add: assms)
finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
by simp
have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
- using `c>0` by (auto simp: ennreal_mult'[symmetric])
+ using \<open>c>0\<close> by (auto simp: ennreal_mult'[symmetric])
then have "emeasure M {x \<in> space M. u x \<ge> c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M))"
by simp
also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
by (rule nn_integral_Markov_inequality) (auto simp add: assms)
also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
- apply (rule mult_left_mono) using * `c>0` by auto
+ apply (rule mult_left_mono) using * \<open>c>0\<close> by auto
finally show ?thesis
using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
qed
@@ -2121,8 +2121,8 @@
then show ?thesis using Lim_null by auto
qed
-text {*The next lemma asserts that, if a sequence of functions converges in $L^1$, then
-it admits a subsequence that converges almost everywhere.*}
+text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
+it admits a subsequence that converges almost everywhere.\<close>
lemma tendsto_L1_AE_subseq:
fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -2146,8 +2146,8 @@
have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
proof -
- have "r0 n \<ge> n" using `subseq r0` by (simp add: seq_suble)
- have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF `r0 n \<ge> n`], auto)
+ have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
+ have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
@@ -2168,13 +2168,13 @@
also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
apply (rule nn_integral_mono) using * by auto
also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
- apply (rule nn_integral_cmult) using `e > 0` by auto
+ apply (rule nn_integral_cmult) using \<open>e > 0\<close> by auto
also have "... < (1/e) * ennreal((1/2)^n)"
- using I[of n] `e > 0` by (intro ennreal_mult_strict_left_mono) auto
+ using I[of n] \<open>e > 0\<close> by (intro ennreal_mult_strict_left_mono) auto
finally show ?thesis by simp
qed
have A_fin: "emeasure M (A n) < \<infinity>" for n
- using `e > 0` A_bound[of n]
+ using \<open>e > 0\<close> A_bound[of n]
by (auto simp add: ennreal_mult less_top[symmetric])
have A_sum: "summable (\<lambda>n. measure M (A n))"
@@ -2219,7 +2219,7 @@
by (simp add: tendsto_norm_zero_iff)
}
ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
- then show ?thesis using `subseq r` by auto
+ then show ?thesis using \<open>subseq r\<close> by auto
qed
subsection \<open>Restricted measure spaces\<close>
--- a/src/HOL/Analysis/Borel_Space.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Tue Jan 17 13:59:10 2017 +0100
@@ -2126,7 +2126,7 @@
shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
unfolding powr_def by auto
-text {* The next one is a variation around \verb+measurable_restrict_space+.*}
+text \<open>The next one is a variation around \verb+measurable_restrict_space+.\<close>
lemma measurable_restrict_space3:
assumes "f \<in> measurable M N" and
@@ -2138,7 +2138,7 @@
measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
qed
-text {* The next one is a variation around \verb+measurable_piecewise_restrict+.*}
+text \<open>The next one is a variation around \verb+measurable_piecewise_restrict+.\<close>
lemma measurable_piecewise_restrict2:
assumes [measurable]: "\<And>n. A n \<in> sets M"
@@ -2162,8 +2162,8 @@
fix x assume "x \<in> space M"
then obtain n where "x \<in> A n" using assms(2) by blast
obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
- then have "f x = h x" using `x \<in> A n` by blast
- moreover have "h x \<in> space N" by (metis measurable_space `x \<in> space M` `h \<in> measurable M N`)
+ then have "f x = h x" using \<open>x \<in> A n\<close> by blast
+ moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
ultimately show "f x \<in> space N" by simp
qed
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 17 13:59:10 2017 +0100
@@ -2572,7 +2572,7 @@
moreover have False if "1 < dd (x - a)"
using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
by (auto simp: rel_frontier_def)
- ultimately have "dd (x - a) = 1" --\<open>similar to another proof above\<close>
+ ultimately have "dd (x - a) = 1" \<comment>\<open>similar to another proof above\<close>
by fastforce
with that show ?thesis
by (simp add: rel_frontier_def)
--- a/src/HOL/Analysis/Function_Topology.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Tue Jan 17 13:59:10 2017 +0100
@@ -7,9 +7,9 @@
begin
-section {*Product topology*}
+section \<open>Product topology\<close>
-text {*We want to define the product topology.
+text \<open>We want to define the product topology.
The product topology on a product of topological spaces is generated by
the sets which are products of open sets along finitely many coordinates, and the whole
@@ -60,18 +60,18 @@
topology, even when the product is not finite (or even countable).
I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
-*}
+\<close>
-subsection {*Topology without type classes*}
+subsection \<open>Topology without type classes\<close>
-subsubsection {*The topology generated by some (open) subsets*}
+subsubsection \<open>The topology generated by some (open) subsets\<close>
-text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
+text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
and is never a problem in proofs, so I prefer to write it down explicitly.
We do not require UNIV to be an open set, as this will not be the case in applications. (We are
-thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)*}
+thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
inductive generate_topology_on for S where
Empty: "generate_topology_on S {}"
@@ -83,8 +83,8 @@
"istopology (generate_topology_on S)"
unfolding istopology_def by (auto intro: generate_topology_on.intros)
-text {*The basic property of the topology generated by a set $S$ is that it is the
-smallest topology containing all the elements of $S$:*}
+text \<open>The basic property of the topology generated by a set $S$ is that it is the
+smallest topology containing all the elements of $S$:\<close>
lemma generate_topology_on_coarsest:
assumes "istopology T"
@@ -127,10 +127,10 @@
"s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
-subsubsection {*Continuity*}
+subsubsection \<open>Continuity\<close>
-text {*We will need to deal with continuous maps in terms of topologies and not in terms
-of type classes, as defined below.*}
+text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
+of type classes, as defined below.\<close>
definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-`U \<inter> topspace(T1)))
@@ -206,15 +206,15 @@
using assms unfolding continuous_on_topo_def by auto
-subsubsection {*Pullback topology*}
+subsubsection \<open>Pullback topology\<close>
-text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
+text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
a special case of this notion, pulling back by the identity. We introduce the general notion as
we will need it to define the strong operator topology on the space of continuous linear operators,
-by pulling back the product topology on the space of all functions.*}
+by pulling back the product topology on the space of all functions.\<close>
-text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
-the set $A$.*}
+text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
+the set $A$.\<close>
definition pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
@@ -253,7 +253,7 @@
also have "... = f-`(g-`U \<inter> topspace T1) \<inter> A "
by auto
also have "openin (pullback_topology A f T1) (...)"
- unfolding openin_pullback_topology using `openin T1 (g-\`U \<inter> topspace T1)` by auto
+ unfolding openin_pullback_topology using \<open>openin T1 (g-`U \<inter> topspace T1)\<close> by auto
finally show "openin (pullback_topology A f T1) ((g \<circ> f) -` U \<inter> topspace (pullback_topology A f T1))"
by auto
next
@@ -281,23 +281,23 @@
also have "... = (f o g)-`V \<inter> topspace T1"
using assms(2) by auto
also have "openin T1 (...)"
- using assms(1) `openin T2 V` by auto
+ using assms(1) \<open>openin T2 V\<close> by auto
finally show "openin T1 (g -` U \<inter> topspace T1)" by simp
next
fix x assume "x \<in> topspace T1"
have "(f o g) x \<in> topspace T2"
- using assms(1) `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+ using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
then have "g x \<in> f-`(topspace T2)"
unfolding comp_def by blast
- moreover have "g x \<in> A" using assms(2) `x \<in> topspace T1` by blast
+ moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
ultimately show "g x \<in> topspace (pullback_topology A f T2)"
unfolding topspace_pullback_topology by blast
qed
-subsection {*The product topology*}
+subsection \<open>The product topology\<close>
-text {*We can now define the product topology, as generated by
+text \<open>We can now define the product topology, as generated by
the sets which are products of open sets along finitely many coordinates, and the whole
space along the other coordinates. Equivalently, it is generated by sets which are one open
set along one single coordinate, and the whole space along other coordinates. In fact, this is only
@@ -306,14 +306,14 @@
point, equal to \verb+undefined+ along all coordinates.
So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
-*}
+\<close>
definition product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
where "product_topology T I =
topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
-text {*The total set of the product topology is the product of the total sets
-along each coordinate.*}
+text \<open>The total set of the product topology is the product of the total sets
+along each coordinate.\<close>
lemma product_topology_topspace:
"topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
@@ -367,15 +367,15 @@
then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
by blast
then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
- using `k \<in> K` by auto
+ using \<open>k \<in> K\<close> by auto
then show ?case
by auto
qed auto
- then show ?thesis using `x \<in> U` by auto
+ then show ?thesis using \<open>x \<in> U\<close> by auto
qed
-text {*The basic property of the product topology is the continuity of projections:*}
+text \<open>The basic property of the product topology is the continuity of projections:\<close>
lemma continuous_on_topo_product_coordinates [simp]:
assumes "i \<in> I"
@@ -385,10 +385,10 @@
fix U assume "openin (T i) U"
define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
then have *: "(\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
- unfolding X_def using assms openin_subset[OF `openin (T i) U`]
+ unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
by (auto simp add: PiE_iff, auto, metis subsetCE)
have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
- unfolding X_def using `openin (T i) U` by auto
+ unfolding X_def using \<open>openin (T i) U\<close> by auto
have "openin (product_topology T I) ((\<lambda>x. x i) -` U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
unfolding product_topology_def
apply (rule topology_generated_by_Basis)
@@ -417,11 +417,11 @@
have "f-`U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
by (subst H(1), auto simp add: PiE_iff assms)
also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
- using * `J \<subseteq> I` by auto
+ using * \<open>J \<subseteq> I\<close> by auto
also have "openin T1 (...)"
apply (rule openin_INT)
- apply (simp add: `finite J`)
- using H(2) assms(1) `J \<subseteq> I` by auto
+ apply (simp add: \<open>finite J\<close>)
+ using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
next
show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
@@ -441,17 +441,17 @@
have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
also have "continuous_on_topo T1 (T i) (...)"
apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
- using assms `i \<in> I` by auto
+ using assms \<open>i \<in> I\<close> by auto
ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
by simp
next
fix i x assume "i \<notin> I" "x \<in> topspace T1"
have "f x \<in> topspace (product_topology T I)"
- using assms `x \<in> topspace T1` unfolding continuous_on_topo_def by auto
+ using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
using product_topology_topspace by metis
then show "f x i = undefined"
- using `i \<notin> I` by (auto simp add: PiE_iff extensional_def)
+ using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
qed
lemma continuous_on_restrict:
@@ -461,7 +461,7 @@
fix i assume "i \<in> J"
then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
- using `i \<in> J` `J \<subseteq> I` by auto
+ using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
next
fix i assume "i \<notin> J"
then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
@@ -469,7 +469,7 @@
qed
-subsubsection {*Powers of a single topological space as a topological space, using type classes*}
+subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
instantiation "fun" :: (type, topological_space) topological_space
begin
@@ -521,8 +521,8 @@
ultimately show ?thesis by simp
qed
-text {*The results proved in the general situation of products of possibly different
-spaces have their counterparts in this simpler setting.*}
+text \<open>The results proved in the general situation of products of possibly different
+spaces have their counterparts in this simpler setting.\<close>
lemma continuous_on_product_coordinates [simp]:
"continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
@@ -545,11 +545,11 @@
"continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
by (auto intro: continuous_on_product_then_coordinatewise)
-subsubsection {*Topological countability for product spaces*}
+subsubsection \<open>Topological countability for product spaces\<close>
-text {*The next two lemmas are useful to prove first or second countability
+text \<open>The next two lemmas are useful to prove first or second countability
of product spaces, but they have more to do with countability and could
-be put in the corresponding theory.*}
+be put in the corresponding theory.\<close>
lemma countable_nat_product_event_const:
fixes F::"'a set" and a::'a
@@ -563,7 +563,7 @@
proof (induction N)
case 0
have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
- using `a \<in> F` by auto
+ using \<open>a \<in> F\<close> by auto
then show ?case by auto
next
case (Suc N)
@@ -576,7 +576,7 @@
have "f (y, x N) = x"
unfolding f_def y_def by auto
moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
- unfolding y_def using H `a \<in> F` by auto
+ unfolding y_def using H \<open>a \<in> F\<close> by auto
ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
by (metis (no_types, lifting) image_eqI)
qed
@@ -616,7 +616,7 @@
by auto
qed
then show ?thesis
- using countable_nat_product_event_const[OF `b \<in> G` `countable G`]
+ using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
by (meson countable_image countable_subset)
qed
@@ -629,7 +629,7 @@
"\<And>x i. open (A x i)"
"\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
by metis
- text {*$B i$ is a countable basis of neighborhoods of $x_i$.*}
+ text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
have "countable (B i)" for i unfolding B_def by auto
@@ -638,7 +638,7 @@
unfolding K_def B_def by auto
then have "K \<noteq> {}" by auto
have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
- apply (rule countable_product_event_const) using `\<And>i. countable (B i)` by auto
+ apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have "countable K" by auto
@@ -652,7 +652,7 @@
have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
proof -
have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
- using `open U \<and> x \<in> U` unfolding open_fun_def by auto
+ using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
with product_topology_open_contains_basis[OF this]
have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
unfolding topspace_euclidean open_openin by simp
@@ -685,12 +685,12 @@
apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
- then show ?thesis using `Pi\<^sub>E UNIV Y \<in> K` by auto
+ then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
qed
show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
apply (rule first_countableI[of K])
- using `countable K` `\<And>k. k \<in> K \<Longrightarrow> x \<in> k` `\<And>k. k \<in> K \<Longrightarrow> open k` Inc by auto
+ using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
qed
lemma product_topology_countable_basis:
@@ -709,10 +709,10 @@
define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
- unfolding K_def using `\<And>U. U \<in> B2 \<Longrightarrow> open U` by auto
+ unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
- apply (rule countable_product_event_const) using `countable B2` by auto
+ apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
unfolding K_def by auto
ultimately have ii: "countable K" by auto
@@ -722,7 +722,7 @@
fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
unfolding open_fun_def by auto
- with product_topology_open_contains_basis[OF this `x \<in> U`]
+ with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
unfolding topspace_euclidean open_openin by simp
then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
@@ -734,7 +734,7 @@
define I where "I = {i. X i \<noteq> UNIV}"
define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
- unfolding B2_def using B `open (X i)` `x i \<in> X i` by (meson UnCI topological_basisE)
+ unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
using someI_ex[OF *]
apply (cases "i \<in> I")
@@ -758,13 +758,13 @@
using ** by auto
show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
- using `Pi\<^sub>E UNIV Y \<in> K` `Pi\<^sub>E UNIV Y \<subseteq> U` `x \<in> Pi\<^sub>E UNIV Y` by auto
+ using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
next
fix U assume "U \<in> K"
show "open U"
- using `U \<in> K` unfolding open_fun_def K_def apply (auto)
+ using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
apply (rule product_topology_basis)
- using `\<And>V. V \<in> B2 \<Longrightarrow> open V` open_UNIV unfolding topspace_euclidean open_openin[symmetric]
+ using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
by auto
qed
@@ -776,9 +776,9 @@
using product_topology_countable_basis topological_basis_imp_subbasis by auto
-subsection {*The strong operator topology on continuous linear operators*}
+subsection \<open>The strong operator topology on continuous linear operators\<close>
-text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
+text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
(the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
@@ -795,7 +795,7 @@
weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
canonical embedding of a space into its bidual. We do not define it there, although it could also be
defined analogously.
-*}
+\<close>
definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
@@ -847,7 +847,7 @@
show "continuous_on_topo T strong_operator_topology f"
unfolding strong_operator_topology_def
apply (rule continuous_on_topo_pullback')
- by (auto simp add: `continuous_on_topo T euclidean (blinfun_apply o f)`)
+ by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
qed
lemma strong_operator_topology_weaker_than_euclidean:
@@ -856,10 +856,10 @@
auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
-subsection {*Metrics on product spaces*}
+subsection \<open>Metrics on product spaces\<close>
-text {*In general, the product topology is not metrizable, unless the index set is countable.
+text \<open>In general, the product topology is not metrizable, unless the index set is countable.
When the index set is countable, essentially any (convergent) combination of the metrics on the
factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
for instance.
@@ -870,7 +870,7 @@
The proofs below would work verbatim for general countable products of metric spaces. However,
since distances are only implemented in terms of type classes, we only develop the theory
-for countable products of the same space.*}
+for countable products of the same space.\<close>
instantiation "fun" :: (countable, metric_space) metric_space
begin
@@ -881,10 +881,10 @@
definition uniformity_fun_def:
"(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
-text {*Except for the first one, the auxiliary lemmas below are only useful when proving the
+text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
instance: once it is proved, they become trivial consequences of the general theory of metric
spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
-to do this.*}
+to do this.\<close>
lemma dist_fun_le_dist_first_terms:
"dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
@@ -947,18 +947,18 @@
"\<And>i. openin euclidean (X i)"
"finite {i. X i \<noteq> topspace euclidean}"
"x \<in> Pi\<^sub>E UNIV X"
- using product_topology_open_contains_basis[OF * `x \<in> U`] by auto
+ using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
define I where "I = {i. X i \<noteq> topspace euclidean}"
have "finite I" unfolding I_def using H(3) by auto
{
fix i
- have "x i \<in> X i" using `x \<in> U` H by auto
+ have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
- using `openin euclidean (X i)` open_openin open_contains_ball by blast
+ using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
define f where "f = min e (1/2)"
- have "f>0" "f<1" unfolding f_def using `e>0` by auto
- moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using `ball (x i) e \<subseteq> X i` by auto
+ have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
+ moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
} note * = this
have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
@@ -967,7 +967,7 @@
by blast
define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
have "m > 0" if "I\<noteq>{}"
- unfolding m_def apply (rule Min_grI) using `finite I` `I \<noteq> {}` `\<And>i. e i > 0` by auto
+ unfolding m_def apply (rule Min_grI) using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
moreover have "{y. dist x y < m} \<subseteq> U"
proof (auto)
fix y assume "dist x y < m"
@@ -977,19 +977,19 @@
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
define n where "n = to_nat i"
have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
- using `dist x y < m` unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
+ using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
- using `n = to_nat i` by auto
+ using \<open>n = to_nat i\<close> by auto
also have "... \<le> (1/2)^(to_nat i) * e i"
- unfolding m_def apply (rule Min_le) using `finite I` `i \<in> I` by auto
+ unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
ultimately have "min (dist (x i) (y i)) 1 < e i"
by (auto simp add: divide_simps)
then have "dist (x i) (y i) < e i"
- using `e i < 1` by auto
- then show "y i \<in> X i" using `ball (x i) (e i) \<subseteq> X i` by auto
+ using \<open>e i < 1\<close> by auto
+ then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
qed
then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
- then show "y \<in> U" using `Pi\<^sub>E UNIV X \<subseteq> U` by auto
+ then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
qed
ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
@@ -1021,14 +1021,14 @@
define U where "U = Pi\<^sub>E UNIV X"
have "open U"
unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
- unfolding U_def using `\<And>i. openin euclidean (X i)` `finite {i. X i \<noteq> topspace euclidean}`
+ unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
by auto
moreover have "x \<in> U"
unfolding U_def X_def by (auto simp add: PiE_iff)
moreover have "dist x y < e" if "y \<in> U" for y
proof -
have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
- using `y \<in> U` unfolding U_def apply (auto simp add: PiE_iff)
+ using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
apply (rule Max.boundedI) using * by auto
@@ -1036,7 +1036,7 @@
have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
by (rule dist_fun_le_dist_first_terms)
also have "... \<le> 2 * f + e / 8"
- apply (rule add_mono) using ** `2^N > 8/e` by(auto simp add: algebra_simps divide_simps)
+ apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
also have "... \<le> e/2 + e/8"
unfolding f_def by auto
also have "... < e"
@@ -1053,7 +1053,7 @@
assume "open U"
fix x assume "x \<in> U"
then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
- using open_fun_contains_ball_aux[OF `open U` `x \<in> U`] by auto
+ using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
next
assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
define K where "K = {V. open V \<and> V \<subseteq> U}"
@@ -1061,10 +1061,10 @@
fix x assume "x \<in> U"
then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
- using ball_fun_contains_open_aux[OF `e>0`, of x] by auto
+ using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
have "V \<in> K"
unfolding K_def using e(2) V(1) V(3) by auto
- then have "x \<in> (\<Union>K)" using `x \<in> V` by auto
+ then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
}
then have "(\<Union>K) = U"
unfolding K_def by auto
@@ -1077,13 +1077,13 @@
fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
proof
assume "x = y"
- then show "dist x y = 0" unfolding dist_fun_def using `x = y` by auto
+ then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
next
assume "dist x y = 0"
have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
- using `dist x y = 0` unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
+ using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
zero_eq_1_divide_iff zero_neq_numeral)
@@ -1095,9 +1095,9 @@
by auto
qed
next
- text{*The proof of the triangular inequality is trivial, modulo the fact that we are dealing
+ text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
with infinite series, hence we should justify the convergence at each step. In this
- respect, the following simplification rule is extremely handy.*}
+ respect, the following simplification rule is extremely handy.\<close>
have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
fix x y z::"'a \<Rightarrow> 'b"
@@ -1134,11 +1134,11 @@
finally show "dist x y \<le> dist x z + dist y z"
by simp
next
- text{*Finally, we show that the topology generated by the distance and the product
+ text\<open>Finally, we show that the topology generated by the distance and the product
topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
except that the condition to prove is expressed with filters. To deal with this,
we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
- \verb+Real_Vector_Spaces.thy+*}
+ \verb+Real_Vector_Spaces.thy+\<close>
fix U::"('a \<Rightarrow> 'b) set"
have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
unfolding uniformity_fun_def apply (subst eventually_INF_base)
@@ -1149,9 +1149,9 @@
end
-text {*Nice properties of spaces are preserved under countable products. In addition
+text \<open>Nice properties of spaces are preserved under countable products. In addition
to first countability, second countability and metrizability, as we have seen above,
-completeness is also preserved, and therefore being Polish.*}
+completeness is also preserved, and therefore being Polish.\<close>
instance "fun" :: (countable, complete_space) complete_space
proof
@@ -1161,9 +1161,9 @@
fix e assume "e>(0::real)"
obtain k where "i = from_nat k"
using from_nat_to_nat[of i] by metis
- have "(1/2)^k * min e 1 > 0" using `e>0` by auto
+ have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
- using `Cauchy u` unfolding cauchy_def by blast
+ using \<open>Cauchy u\<close> unfolding cauchy_def by blast
then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
by blast
have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
@@ -1171,14 +1171,14 @@
fix m n::nat assume "m \<ge> N" "n \<ge> N"
have "(1/2)^k * min (dist (u m i) (u n i)) 1
= sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
- using `i = from_nat k` by auto
+ using \<open>i = from_nat k\<close> by auto
also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
apply (rule sum_le_suminf)
by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
also have "... = dist (u m) (u n)"
unfolding dist_fun_def by auto
also have "... < (1/2)^k * min e 1"
- using C `m \<ge> N` `n \<ge> N` by auto
+ using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
finally have "min (dist (u m i) (u n i)) 1 < min e 1"
by (auto simp add: algebra_simps divide_simps)
then show "dist (u m i) (u n i) < e" by auto
@@ -1210,8 +1210,8 @@
have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
proof -
have "K (from_nat n) \<le> L"
- unfolding L_def apply (rule Max_ge) using `n \<le> N` by auto
- then have "k \<ge> K (from_nat n)" using `k \<ge> L` by auto
+ unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
+ then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
then show ?thesis using K less_imp_le by auto
qed
have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
@@ -1220,7 +1220,7 @@
using dist_fun_le_dist_first_terms by auto
also have "... \<le> 2 * e/4 + e/4"
apply (rule add_mono)
- using ** `2^N > 4/e` less_imp_le by (auto simp add: algebra_simps divide_simps)
+ using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
also have "... < e" by auto
finally show ?thesis by simp
qed
@@ -1233,9 +1233,9 @@
by standard
-subsection {*Measurability*}
+subsection \<open>Measurability\<close>
-text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
+text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
generated by open sets in the product, and the product sigma algebra, countably generated by
products of measurable sets along finitely many coordinates. The second one is defined and studied
in \verb+Finite_Product_Measure.thy+.
@@ -1249,7 +1249,7 @@
In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
compare it with the product sigma algebra as explained above.
-*}
+\<close>
lemma measurable_product_coordinates [measurable (raw)]:
"(\<lambda>x. x i) \<in> measurable borel borel"
@@ -1265,9 +1265,9 @@
then show ?thesis by simp
qed
-text {*To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
+text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
of the product sigma algebra that is more similar to the one we used above for the product
-topology.*}
+topology.\<close>
lemma sets_PiM_finite:
"sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
@@ -1281,7 +1281,7 @@
have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
- unfolding Y_def apply (rule sets_PiM_I) using `finite J` `J \<subseteq> I` * by auto
+ unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
by (auto simp add: PiE_iff, blast)
@@ -1297,10 +1297,10 @@
proof -
define X where "X = (\<lambda>j. if j = i then A else space (M j))"
have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
- unfolding X_def using sets.sets_into_space[OF `A \<in> sets (M i)`] `i \<in> I`
+ unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
moreover have "X j \<in> sets (M j)" for j
- unfolding X_def using `A \<in> sets (M i)` by auto
+ unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
moreover have "finite {j. X j \<noteq> space (M j)}"
unfolding X_def by simp
ultimately show ?thesis by auto
@@ -1322,7 +1322,7 @@
have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-`(X i) \<inter> space borel) \<inter> space borel"
unfolding I_def by auto
also have "... \<in> sets borel"
- using that `finite I` by measurable
+ using that \<open>finite I\<close> by measurable
finally show ?thesis by simp
qed
then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
@@ -1340,17 +1340,17 @@
have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
proof -
obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
- using K(3)[OF `k \<in> K`] by blast
+ using K(3)[OF \<open>k \<in> K\<close>] by blast
show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
qed
have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
proof -
obtain B where "B \<subseteq> K" "U = (\<Union>B)"
- using `open U` `topological_basis K` by (metis topological_basis_def)
- have "countable B" using `B \<subseteq> K` `countable K` countable_subset by blast
+ using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
+ have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
- using `B \<subseteq> K` * that by auto
- ultimately show ?thesis unfolding `U = (\<Union>B)` by auto
+ using \<open>B \<subseteq> K\<close> * that by auto
+ ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
qed
have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
apply (rule sets.sigma_sets_subset') using ** by auto
--- a/src/HOL/Analysis/Further_Topology.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Jan 17 13:59:10 2017 +0100
@@ -4350,7 +4350,7 @@
qed
qed
-text\<open>The proof is a duplicate of that of @{text Borsukian_open_Un}.\<close>
+text\<open>The proof is a duplicate of that of \<open>Borsukian_open_Un\<close>.\<close>
lemma Borsukian_closed_Un:
fixes S :: "'a::real_normed_vector set"
assumes cloS: "closedin (subtopology euclidean (S \<union> T)) S"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jan 17 13:59:10 2017 +0100
@@ -109,7 +109,7 @@
fixes a :: "'a::euclidean_space"
assumes "k \<in> Basis"
shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
- -- \<open>Prove using measure theory\<close>
+ \<comment> \<open>Prove using measure theory\<close>
proof cases
note simps = interval_split[OF assms] content_cbox_cases
have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
--- a/src/HOL/Analysis/Measure_Space.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Tue Jan 17 13:59:10 2017 +0100
@@ -1092,9 +1092,9 @@
qed
qed
-text {*The next lemma is convenient to combine with a lemma whose conclusion is of the
+text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
-but using \<open>AE_symmetric[OF...]\<close> will replace it.*}
+but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
(* depricated replace by laws about eventually *)
lemma
@@ -1361,19 +1361,19 @@
where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
using sigma_finite_incseq by blast
define B where "B = (\<lambda>i. W \<inter> A i)"
- have B_meas: "\<And>i. B i \<in> sets M" using W_meas `range A \<subseteq> sets M` B_def by blast
+ have B_meas: "\<And>i. B i \<in> sets M" using W_meas \<open>range A \<subseteq> sets M\<close> B_def by blast
have b: "\<And>i. B i \<subseteq> W" using B_def by blast
{ fix i
have "emeasure M (B i) \<le> emeasure M (A i)"
using A by (intro emeasure_mono) (auto simp: B_def)
also have "emeasure M (A i) < \<infinity>"
- using `\<And>i. emeasure M (A i) \<noteq> \<infinity>` by (simp add: less_top)
+ using \<open>\<And>i. emeasure M (A i) \<noteq> \<infinity>\<close> by (simp add: less_top)
finally have "emeasure M (B i) < \<infinity>" . }
note c = this
- have "W = (\<Union>i. B i)" using B_def `(\<Union>i. A i) = space M` W_meas by auto
- moreover have "incseq B" using B_def `incseq A` by (simp add: incseq_def subset_eq)
+ have "W = (\<Union>i. B i)" using B_def \<open>(\<Union>i. A i) = space M\<close> W_meas by auto
+ moreover have "incseq B" using B_def \<open>incseq A\<close> by (simp add: incseq_def subset_eq)
ultimately have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> emeasure M W" using W_meas B_meas
by (simp add: B_meas Lim_emeasure_incseq image_subset_iff)
then have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> \<infinity>" using W_inf by simp
--- a/src/HOL/Analysis/Path_Connected.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Jan 17 13:59:10 2017 +0100
@@ -7099,7 +7099,7 @@
subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
-subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}\<close>
+subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
lemma homeomorphism_moving_point_1:
fixes a :: "'a::euclidean_space"
@@ -7521,7 +7521,7 @@
qed
-subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}\<close>
+subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
lemma homeomorphism_grouping_point_1:
fixes a::real and c::real
--- a/src/HOL/Analysis/Radon_Nikodym.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy Tue Jan 17 13:59:10 2017 +0100
@@ -44,9 +44,9 @@
qed
qed fact
-text {*An equivalent characterization of sigma-finite spaces is the existence of integrable
+text \<open>An equivalent characterization of sigma-finite spaces is the existence of integrable
positive functions (or, still equivalently, the existence of a probability measure which is in
-the same measure class as the original measure).*}
+the same measure class as the original measure).\<close>
lemma (in sigma_finite_measure) obtain_positive_integrable_function:
obtains f::"'a \<Rightarrow> real" where
@@ -69,7 +69,7 @@
have g_pos: "g x > 0" if "x \<in> space M" for x
unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
- obtain i where "x \<in> A i" using `(\<Union>i. A i) = space M` `x \<in> space M` by auto
+ obtain i where "x \<in> A i" using \<open>(\<Union>i. A i) = space M\<close> \<open>x \<in> space M\<close> by auto
then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
@@ -81,7 +81,7 @@
unfolding g_def proof (rule integrable_suminf)
fix n
show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
- using `emeasure M (A n) \<noteq> \<infinity>`
+ using \<open>emeasure M (A n) \<noteq> \<infinity>\<close>
by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
next
show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
@@ -97,7 +97,7 @@
moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto
moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto
moreover have "integrable M f"
- apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using `integrable M g` by auto
+ apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \<open>integrable M g\<close> by auto
ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis"
by (meson that)
qed
@@ -314,7 +314,7 @@
let ?f = "\<lambda>x. f x + b"
have "nn_integral M f \<noteq> top"
- using `f \<in> G`[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
+ using \<open>f \<in> G\<close>[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f"
by (intro finite_measureI)
(auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff
--- a/src/HOL/Analysis/Set_Integral.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Tue Jan 17 13:59:10 2017 +0100
@@ -14,7 +14,7 @@
lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
using surj_f_inv_f[of p] by (auto simp add: bij_def)
-subsection {*Fun.thy*}
+subsection \<open>Fun.thy\<close>
lemma inj_fn:
fixes f::"'a \<Rightarrow> 'a"
@@ -129,7 +129,7 @@
shows "Inf K \<in> K"
by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
-subsection {*Liminf-Limsup.thy*}
+subsection \<open>Liminf-Limsup.thy\<close>
lemma limsup_shift:
"limsup (\<lambda>n. u (n+1)) = limsup u"
@@ -140,7 +140,7 @@
have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
apply (rule INF_eq) using Suc_le_D by auto
have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
- apply (rule INF_eq) using `decseq v` decseq_Suc_iff by auto
+ apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
@@ -164,7 +164,7 @@
have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
apply (rule SUP_eq) using Suc_le_D by (auto)
have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
- apply (rule SUP_eq) using `incseq v` incseq_Suc_iff by auto
+ apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
@@ -188,8 +188,8 @@
then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
qed
-text {* The next lemma is extremely useful, as it often makes it possible to reduce statements
-about limsups to statements about limits.*}
+text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
+about limsups to statements about limits.\<close>
lemma limsup_subseq_lim:
fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
@@ -203,12 +203,12 @@
define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
- then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ `subseq r`)
+ then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
then have "umax o r = u o r" unfolding o_def by simp
then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
- then show ?thesis using `subseq r` by blast
+ then show ?thesis using \<open>subseq r\<close> by blast
next
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
@@ -219,18 +219,18 @@
have "Max {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Max_in) using a by (auto)
then obtain p where "p \<in> {N<..x}" and upmax: "u p = Max{u i |i. i \<in> {N<..x}}" by auto
define U where "U = {m. m > p \<and> u p < u m}"
- have "U \<noteq> {}" unfolding U_def using N[of p] `p \<in> {N<..x}` by auto
+ have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
define y where "y = Inf U"
- then have "y \<in> U" using `U \<noteq> {}` by (simp add: Inf_nat_def1)
+ then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<le> u p"
proof -
fix i assume "i \<in> {N<..x}"
then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
then show "u i \<le> u p" using upmax by simp
qed
- moreover have "u p < u y" using `y \<in> U` U_def by auto
+ moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
ultimately have "y \<notin> {N<..x}" using not_le by blast
- moreover have "y > N" using `y \<in> U` U_def `p \<in> {N<..x}` by auto
+ moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
ultimately have "y > x" by auto
have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<le> u y"
@@ -241,7 +241,7 @@
then show ?thesis by simp
next
assume "\<not>(i=y)"
- then have i:"i \<in> {N<..<y}" using `i \<in> {N<..y}` by simp
+ then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
have "u i \<le> u p"
proof (cases)
assume "i \<le> x"
@@ -250,15 +250,15 @@
next
assume "\<not>(i \<le> x)"
then have "i > x" by simp
- then have *: "i > p" using `p \<in> {N<..x}` by simp
+ then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
have "i < Inf U" using i y_def by simp
then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
then show ?thesis using U_def * by auto
qed
- then show "u i \<le> u y" using `u p < u y` by auto
+ then show "u i \<le> u y" using \<open>u p < u y\<close> by auto
qed
qed
- then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using `y > x` `y > N` by auto
+ then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
qed (auto)
then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
@@ -266,12 +266,12 @@
have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
- moreover have "limsup (u o r) \<le> limsup u" using `subseq r` by (simp add: limsup_subseq_mono)
+ moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
{
fix i assume i: "i \<in> {N<..}"
- obtain n where "i < r (Suc n)" using `subseq r` using Suc_le_eq seq_suble by blast
+ obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
then have "i \<in> {N<..r(Suc n)}" using i by simp
then have "u i \<le> u (r(Suc n))" using r by simp
then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
@@ -279,9 +279,9 @@
then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
- then have "limsup u = (SUP n. (u o r) n)" using `(SUP n. (u o r) n) \<le> limsup u` by simp
- then have "(u o r) \<longlonglongrightarrow> limsup u" using `(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)` by simp
- then show ?thesis using `subseq r` by auto
+ then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
+ then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
+ then show ?thesis using \<open>subseq r\<close> by auto
qed
lemma liminf_subseq_lim:
@@ -296,12 +296,12 @@
define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
- then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ `subseq r`)
+ then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
then have "umin o r = u o r" unfolding o_def by simp
then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
- then show ?thesis using `subseq r` by blast
+ then show ?thesis using \<open>subseq r\<close> by blast
next
assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
@@ -312,18 +312,18 @@
have "Min {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Min_in) using a by (auto)
then obtain p where "p \<in> {N<..x}" and upmin: "u p = Min{u i |i. i \<in> {N<..x}}" by auto
define U where "U = {m. m > p \<and> u p > u m}"
- have "U \<noteq> {}" unfolding U_def using N[of p] `p \<in> {N<..x}` by auto
+ have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
define y where "y = Inf U"
- then have "y \<in> U" using `U \<noteq> {}` by (simp add: Inf_nat_def1)
+ then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<ge> u p"
proof -
fix i assume "i \<in> {N<..x}"
then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
then show "u i \<ge> u p" using upmin by simp
qed
- moreover have "u p > u y" using `y \<in> U` U_def by auto
+ moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
ultimately have "y \<notin> {N<..x}" using not_le by blast
- moreover have "y > N" using `y \<in> U` U_def `p \<in> {N<..x}` by auto
+ moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
ultimately have "y > x" by auto
have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<ge> u y"
@@ -334,7 +334,7 @@
then show ?thesis by simp
next
assume "\<not>(i=y)"
- then have i:"i \<in> {N<..<y}" using `i \<in> {N<..y}` by simp
+ then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
have "u i \<ge> u p"
proof (cases)
assume "i \<le> x"
@@ -343,15 +343,15 @@
next
assume "\<not>(i \<le> x)"
then have "i > x" by simp
- then have *: "i > p" using `p \<in> {N<..x}` by simp
+ then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
have "i < Inf U" using i y_def by simp
then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
then show ?thesis using U_def * by auto
qed
- then show "u i \<ge> u y" using `u p > u y` by auto
+ then show "u i \<ge> u y" using \<open>u p > u y\<close> by auto
qed
qed
- then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using `y > x` `y > N` by auto
+ then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
qed (auto)
then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
@@ -359,12 +359,12 @@
have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
- moreover have "liminf (u o r) \<ge> liminf u" using `subseq r` by (simp add: liminf_subseq_mono)
+ moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
{
fix i assume i: "i \<in> {N<..}"
- obtain n where "i < r (Suc n)" using `subseq r` using Suc_le_eq seq_suble by blast
+ obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
then have "i \<in> {N<..r(Suc n)}" using i by simp
then have "u i \<ge> u (r(Suc n))" using r by simp
then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
@@ -372,15 +372,15 @@
then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
- then have "liminf u = (INF n. (u o r) n)" using `(INF n. (u o r) n) \<ge> liminf u` by simp
- then have "(u o r) \<longlonglongrightarrow> liminf u" using `(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)` by simp
- then show ?thesis using `subseq r` by auto
+ then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
+ then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
+ then show ?thesis using \<open>subseq r\<close> by auto
qed
-subsection {*Extended-Real.thy*}
+subsection \<open>Extended-Real.thy\<close>
-text{* The proof of this one is copied from \verb+ereal_add_mono+. *}
+text\<open>The proof of this one is copied from \verb+ereal_add_mono+.\<close>
lemma ereal_add_strict_mono2:
fixes a b c d :: ereal
assumes "a < b"
@@ -392,7 +392,7 @@
apply (cases rule: ereal3_cases[of b c d], auto)
done
-text {* The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.*}
+text \<open>The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.\<close>
lemma ereal_mult_mono:
fixes a b c d::ereal
@@ -411,7 +411,7 @@
assumes "b > 0" "c > 0" "a < b" "c < d"
shows "a * c < b * d"
proof -
- have "c < \<infinity>" using `c < d` by auto
+ have "c < \<infinity>" using \<open>c < d\<close> by auto
then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
ultimately show ?thesis by simp
@@ -465,13 +465,13 @@
qed
-subsubsection {*Continuity of addition*}
+subsubsection \<open>Continuity of addition\<close>
-text {*The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
+text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
in \verb+tendsto_add_ereal_general+ which essentially says that the addition
is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
It is much more convenient in many situations, see for instance the proof of
-\verb+tendsto_sum_ereal+ below. *}
+\verb+tendsto_sum_ereal+ below.\<close>
lemma tendsto_add_ereal_PInf:
fixes y :: ereal
@@ -507,9 +507,9 @@
then show ?thesis by (simp add: tendsto_PInfty)
qed
-text{* One would like to deduce the next lemma from the previous one, but the fact
+text\<open>One would like to deduce the next lemma from the previous one, but the fact
that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
-so it is more efficient to copy the previous proof.*}
+so it is more efficient to copy the previous proof.\<close>
lemma tendsto_add_ereal_MInf:
fixes y :: ereal
@@ -574,8 +574,8 @@
ultimately show ?thesis by simp
qed
-text {* The next lemma says that the addition is continuous on ereal, except at
-the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$. *}
+text \<open>The next lemma says that the addition is continuous on ereal, except at
+the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
lemma tendsto_add_ereal_general [tendsto_intros]:
fixes x y :: ereal
@@ -596,11 +596,11 @@
then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
qed
-subsubsection {*Continuity of multiplication*}
+subsubsection \<open>Continuity of multiplication\<close>
-text {* In the same way as for addition, we prove that the multiplication is continuous on
+text \<open>In the same way as for addition, we prove that the multiplication is continuous on
ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
-starting with specific situations.*}
+starting with specific situations.\<close>
lemma tendsto_mult_real_ereal:
assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
@@ -631,15 +631,15 @@
shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
proof -
obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
- have *: "eventually (\<lambda>x. f x > a) F" using `a < l` assms(1) by (simp add: order_tendsto_iff)
+ have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
{
fix K::real
define M where "M = max K 1"
then have "M > 0" by simp
- then have "ereal(M/a) > 0" using `ereal a > 0` by simp
+ then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
then have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > ereal a * ereal(M/a))"
- using ereal_mult_mono_strict'[where ?c = "M/a", OF `0 < ereal a`] by auto
- moreover have "ereal a * ereal(M/a) = M" using `ereal a > 0` by simp
+ using ereal_mult_mono_strict'[where ?c = "M/a", OF \<open>0 < ereal a\<close>] by auto
+ moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
ultimately have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > M)" by simp
moreover have "M \<ge> K" unfolding M_def by simp
ultimately have Imp: "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > K)"
@@ -674,13 +674,13 @@
assume "\<not>(l = \<infinity> \<or> m = \<infinity>)"
then have "l < \<infinity>" "m < \<infinity>" by auto
then obtain lr mr where "l = ereal lr" "m = ereal mr"
- using `l>0` `m>0` by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
+ using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
then show ?thesis using tendsto_mult_real_ereal assms by auto
qed
-text {*We reduce the general situation to the positive case by multiplying by suitable signs.
+text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
-give the bare minimum we need.*}
+give the bare minimum we need.\<close>
lemma ereal_sgn_abs:
fixes l::ereal
@@ -720,9 +720,9 @@
have "((\<lambda>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \<longlongrightarrow> (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
by (rule tendsto_cmult_ereal, auto simp add: sgn_finite2 *)
moreover have "\<And>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
- by (metis mult.left_neutral sgn_squared_ereal[OF `l \<noteq> 0`] sgn_squared_ereal[OF `m \<noteq> 0`] mult.assoc mult.commute)
+ by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
- by (metis mult.left_neutral sgn_squared_ereal[OF `l \<noteq> 0`] sgn_squared_ereal[OF `m \<noteq> 0`] mult.assoc mult.commute)
+ by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
ultimately show ?thesis by auto
qed
@@ -733,7 +733,7 @@
by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
-subsubsection {*Continuity of division*}
+subsubsection \<open>Continuity of division\<close>
lemma tendsto_inverse_ereal_PInf:
fixes u::"_ \<Rightarrow> ereal"
@@ -747,9 +747,9 @@
moreover
{
fix z::ereal assume "z>1/e"
- then have "z>0" using `e>0` using less_le_trans not_le by fastforce
+ then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
then have "1/z \<ge> 0" by auto
- moreover have "1/z < e" using `e>0` `z>1/e`
+ moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
apply (cases z) apply auto
by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
@@ -765,11 +765,11 @@
fix a::ereal assume "a>0"
then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
then have "eventually (\<lambda>n. 1/u n < e) F" using *(1) by auto
- then show "eventually (\<lambda>n. 1/u n < a) F" using `a>e` by (metis (mono_tags, lifting) eventually_mono less_trans)
+ then show "eventually (\<lambda>n. 1/u n < a) F" using \<open>a>e\<close> by (metis (mono_tags, lifting) eventually_mono less_trans)
qed
qed
-text {* The next lemma deserves to exist by itself, as it is so common and useful. *}
+text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>
lemma tendsto_inverse_real [tendsto_intros]:
fixes u::"_ \<Rightarrow> real"
@@ -836,7 +836,7 @@
qed
-subsubsection {*Further limits*}
+subsubsection \<open>Further limits\<close>
lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
"(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
@@ -860,8 +860,8 @@
proof (rule ccontr)
assume "\<not>(N > C)"
have "u N \<le> Max {u n| n. n \<le> C}"
- apply (rule Max_ge) using `\<not>(N > C)` by auto
- then show False using `u N \<ge> n` `n \<ge> M` unfolding M_def by auto
+ apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
+ then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
qed
then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
have "Inf {N. u N \<ge> n} \<ge> C"
@@ -981,7 +981,7 @@
ultimately show ?thesis using MInf by auto
qed (simp add: assms)
-text {* the next one is copied from \verb+tendsto_sum+. *}
+text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
lemma tendsto_sum_ereal [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
@@ -992,7 +992,7 @@
by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
qed(simp)
-subsubsection {*Limsups and liminfs*}
+subsubsection \<open>Limsups and liminfs\<close>
lemma limsup_finite_then_bounded:
fixes u::"nat \<Rightarrow> real"
@@ -1017,7 +1017,7 @@
assume "\<not>(n \<le> N)"
then have "n \<ge> N" by simp
then have "u n < C" using N by auto
- then have "u n < real_of_ereal C" using `C = ereal(real_of_ereal C)` less_ereal.simps(1) by fastforce
+ then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
then show "u n \<le> D" unfolding D_def by linarith
qed
qed
@@ -1047,7 +1047,7 @@
assume "\<not>(n \<le> N)"
then have "n \<ge> N" by simp
then have "u n > C" using N by auto
- then have "u n > real_of_ereal C" using `C = ereal(real_of_ereal C)` less_ereal.simps(1) by fastforce
+ then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
then show "u n \<ge> D" unfolding D_def by linarith
qed
qed
@@ -1060,9 +1060,9 @@
shows "\<exists>N>k. u N < l"
by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)
-text {* The following statement about limsups is reduced to a statement about limits using
+text \<open>The following statement about limsups is reduced to a statement about limits using
subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
-\verb+tendsto_add_ereal_general+.*}
+\verb+tendsto_add_ereal_general+.\<close>
lemma ereal_limsup_add_mono:
fixes u v::"nat \<Rightarrow> ereal"
@@ -1091,9 +1091,9 @@
done
have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
- then have a: "limsup (u o r) \<noteq> \<infinity>" using `limsup u < \<infinity>` by auto
+ then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
- then have b: "limsup (v o r o s) \<noteq> \<infinity>" using `limsup v < \<infinity>` by auto
+ then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
using l tendsto_add_ereal_general a b by fastforce
@@ -1101,13 +1101,13 @@
ultimately have "(w o a) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)" by simp
then have "limsup w = limsup (u o r) + limsup (v o r o s)" using l(1) LIMSEQ_unique by blast
then have "limsup w \<le> limsup u + limsup v"
- using `limsup (u o r) \<le> limsup u` `limsup (v o r o s) \<le> limsup v` ereal_add_mono by simp
+ using \<open>limsup (u o r) \<le> limsup u\<close> \<open>limsup (v o r o s) \<le> limsup v\<close> ereal_add_mono by simp
then show ?thesis unfolding w_def by simp
qed
-text {* There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
+text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
This explains why there are more assumptions in the next lemma dealing with liminfs that in the
-previous one about limsups.*}
+previous one about limsups.\<close>
lemma ereal_liminf_add_mono:
fixes u v::"nat \<Rightarrow> ereal"
@@ -1137,9 +1137,9 @@
done
have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
- then have a: "liminf (u o r) \<noteq> -\<infinity>" using `liminf u > -\<infinity>` by auto
+ then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
- then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using `liminf v > -\<infinity>` by auto
+ then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
using l tendsto_add_ereal_general a b by fastforce
@@ -1147,7 +1147,7 @@
ultimately have "(w o a) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)" by simp
then have "liminf w = liminf (u o r) + liminf (v o r o s)" using l(1) LIMSEQ_unique by blast
then have "liminf w \<ge> liminf u + liminf v"
- using `liminf (u o r) \<ge> liminf u` `liminf (v o r o s) \<ge> liminf v` ereal_add_mono by simp
+ using \<open>liminf (u o r) \<ge> liminf u\<close> \<open>liminf (v o r o s) \<ge> liminf v\<close> ereal_add_mono by simp
then show ?thesis unfolding w_def by simp
qed
@@ -1162,7 +1162,7 @@
have "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
by (rule ereal_limsup_add_mono)
- then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using `limsup u = a` by simp
+ then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using \<open>limsup u = a\<close> by simp
have a: "limsup (\<lambda>n. (u n + v n) + (-u n)) \<le> limsup (\<lambda>n. u n + v n) + limsup (\<lambda>n. -u n)"
by (rule ereal_limsup_add_mono)
@@ -1177,7 +1177,7 @@
ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
using eventually_mono by force
then have "limsup v = limsup (\<lambda>n. u n + v n + (-u n))" using Limsup_eq by force
- then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a `limsup (\<lambda>n. -u n) = -a` by (simp add: minus_ereal_def)
+ then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a \<open>limsup (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
then have "limsup (\<lambda>n. u n + v n) \<ge> a + limsup v" using assms(2) by (metis add.commute ereal_le_minus)
then show ?thesis using up by simp
qed
@@ -1255,7 +1255,7 @@
have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
apply (rule ereal_liminf_add_mono) using * by auto
- then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using `liminf u = a` by simp
+ then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
apply (rule ereal_liminf_add_mono) using ** by auto
@@ -1270,7 +1270,7 @@
ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
using eventually_mono by force
then have "liminf v = liminf (\<lambda>n. u n + v n + (-u n))" using Liminf_eq by force
- then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a `liminf (\<lambda>n. -u n) = -a` by (simp add: minus_ereal_def)
+ then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a \<open>liminf (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
then have "liminf (\<lambda>n. u n + v n) \<le> a + liminf v" using assms(2) by (metis add.commute ereal_minus_le)
then show ?thesis using up by simp
qed
@@ -1302,15 +1302,15 @@
have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
- then have b: "limsup (v o r o s) < \<infinity>" using `limsup v < \<infinity>` by auto
+ then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
- apply (rule tendsto_add_ereal_general) using b `liminf u < \<infinity>` l(1) l(3) by force+
+ apply (rule tendsto_add_ereal_general) using b \<open>liminf u < \<infinity>\<close> l(1) l(3) by force+
moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
ultimately have "(w o a) \<longlonglongrightarrow> liminf u + limsup (v o r o s)" by simp
then have "liminf (w o r) = liminf u + limsup (v o r o s)" using l(2) using LIMSEQ_unique by blast
then have "liminf w \<le> liminf u + limsup v"
- using `liminf (w o r) \<ge> liminf w` `limsup (v o r o s) \<le> limsup v`
+ using \<open>liminf (w o r) \<ge> liminf w\<close> \<open>limsup (v o r o s) \<le> limsup v\<close>
by (metis add_mono_thms_linordered_semiring(2) le_less_trans not_less)
then show ?thesis unfolding w_def by simp
qed
@@ -1858,8 +1858,8 @@
by (rule set_borel_measurable_continuous[OF _ assms]) simp
-text{* This notation is from Sébastien Gouëzel: His use is not directly in line with the
-notations in this file, they are more in line with sum, and more readable he thinks. *}
+text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
+notations in this file, they are more in line with sum, and more readable he thinks.\<close>
abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
@@ -1921,7 +1921,7 @@
assume "x \<in> (\<Union>n. B n)"
then obtain n where "x \<in> B n" by blast
have a: "finite {n}" by simp
- have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using `x \<in> B n` assms(3) disjoint_family_on_def
+ have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using \<open>x \<in> B n\<close> assms(3) disjoint_family_on_def
by (metis IntI UNIV_I empty_iff)
then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
@@ -1932,14 +1932,14 @@
by (metis sums_unique[OF sums_finite[OF a]])
then have "(\<Sum>i. h i) = h n" by simp
then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
- then have "(\<Sum>n. f x * indicator (B n) x) = f x" using `x \<in> B n` indicator_def by simp
- then show ?thesis using `x \<in> (\<Union>n. B n)` by auto
+ then have "(\<Sum>n. f x * indicator (B n) x) = f x" using \<open>x \<in> B n\<close> indicator_def by simp
+ then show ?thesis using \<open>x \<in> (\<Union>n. B n)\<close> by auto
next
assume "x \<notin> (\<Union>n. B n)"
then have "\<And>n. f x * indicator (B n) x = 0" by simp
have "(\<Sum>n. f x * indicator (B n) x) = 0"
- by (simp add: `\<And>n. f x * indicator (B n) x = 0`)
- then show ?thesis using `x \<notin> (\<Union>n. B n)` by auto
+ by (simp add: \<open>\<And>n. f x * indicator (B n) x = 0\<close>)
+ then show ?thesis using \<open>x \<notin> (\<Union>n. B n)\<close> by auto
qed
ultimately show ?thesis by simp
qed
@@ -2035,14 +2035,14 @@
proof -
have "AE x in M. indicator A x * f x = 0"
apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
- using assms integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+ using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
then have "AE x\<in>A in M. f x = 0" by auto
then have "AE x\<in>A in M. False" using assms(3) by auto
then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
qed
-text{*The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
-for nonnegative set integrals introduced earlier.*}
+text\<open>The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
+for nonnegative set integrals introduced earlier.\<close>
lemma (in sigma_finite_measure) density_unique2:
assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
@@ -2054,9 +2054,9 @@
qed (auto simp add: assms)
-text {* The next lemma implies the same statement for Banach-space valued functions
+text \<open>The next lemma implies the same statement for Banach-space valued functions
using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
-only formulate it for real-valued functions.*}
+only formulate it for real-valued functions.\<close>
lemma density_unique_real:
fixes f f'::"_ \<Rightarrow> real"
@@ -2067,7 +2067,7 @@
define A where "A = {x \<in> space M. f x < f' x}"
then have [measurable]: "A \<in> sets M" by simp
have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
- using `A \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
+ using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
then have "A \<in> null_sets M"
using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
@@ -2078,7 +2078,7 @@
define B where "B = {x \<in> space M. f' x < f x}"
then have [measurable]: "B \<in> sets M" by simp
have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
- using `B \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
+ using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
then have "B \<in> null_sets M"
using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
@@ -2088,13 +2088,13 @@
then show ?thesis using * by auto
qed
-text {* The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
+text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
variations) are known as Scheffe lemma.
The formalization is more painful as one should jump back and forth between reals and ereals and justify
-all the time positivity or integrability (thankfully, measurability is handled more or less automatically).*}
+all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
lemma Scheffe_lemma1:
assumes "\<And>n. integrable M (F n)" "integrable M f"
--- a/src/HOL/Analysis/Tagged_Division.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Tue Jan 17 13:59:10 2017 +0100
@@ -1312,7 +1312,7 @@
subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
- @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
+ \<open>operative_division\<close>. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
@{typ bool}.\<close>
paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
@@ -2565,10 +2565,10 @@
have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
using of_nat_less_iff less_imp_of_nat_less by fastforce
have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
- for m n --\<open>The symmetry argument requires a single HOL formula\<close>
+ for m n \<comment>\<open>The symmetry argument requires a single HOL formula\<close>
proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
fix v w m and n::nat
- assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
+ assume "m \<le> n" \<comment>\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
apply (simp add: subset_box disjoint_interval)
apply (rule ccontr)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 17 13:59:10 2017 +0100
@@ -499,9 +499,9 @@
proof -
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}"
- then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
- then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y
proof (cases)
assume "\<exists>z. x < z \<and> z < y"
@@ -509,27 +509,27 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
+ ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
- then have "w \<in> V" using `z \<in> V` by (metis someI2)
- then have "x < w \<and> w \<le> y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce
- moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto
+ then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
+ then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
+ moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. x < z \<and> z < y)"
then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto
define U where "U = {x<..}"
then have "open U" by simp
- moreover have "y \<in> U" using `x < y` U_def by simp
- ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
- have "U = {y..}" unfolding U_def using * `x < y` by auto
- then have "V \<subseteq> {y..}" using `V \<subseteq> U` by simp
- then have "(LEAST w. w \<in> V) = y" using `y \<in> V` by (meson Least_equality atLeast_iff subsetCE)
- then have "y \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto
- moreover have "x < y \<and> y \<le> y" using `x < y` by simp
+ moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
+ ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
+ then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
+ then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
+ then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
+ moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp
ultimately show ?thesis by auto
qed
- moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp
+ moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
ultimately show ?thesis by auto
qed
@@ -538,9 +538,9 @@
proof -
obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}"
- then have "countable B1" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
- then have "countable B2" using `countable A` by (simp add: Setcompr_eq_image)
+ then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y
proof (cases)
assume "\<exists>z. x < z \<and> z < y"
@@ -548,27 +548,27 @@
define U where "U = {x<..<y}"
then have "open U" by simp
moreover have "z \<in> U" using z U_def by simp
- ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
+ ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
define w where "w = (SOME x. x \<in> V)"
- then have "w \<in> V" using `z \<in> V` by (metis someI2)
- then have "x \<le> w \<and> w < y" using `w \<in> V` `V \<subseteq> U` U_def by fastforce
- moreover have "w \<in> B1 \<union> B2" using w_def B2_def `V \<in> A` by auto
+ then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
+ then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
+ moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. x < z \<and> z < y)"
then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast
define U where "U = {..<y}"
then have "open U" by simp
- moreover have "x \<in> U" using `x < y` U_def by simp
- ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF `topological_basis A`] by auto
- have "U = {..x}" unfolding U_def using * `x < y` by auto
- then have "V \<subseteq> {..x}" using `V \<subseteq> U` by simp
- then have "(GREATEST x. x \<in> V) = x" using `x \<in> V` by (meson Greatest_equality atMost_iff subsetCE)
- then have "x \<in> B1 \<union> B2" using `V \<in> A` B1_def by auto
- moreover have "x \<le> x \<and> x < y" using `x < y` by simp
+ moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
+ ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
+ have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
+ then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
+ then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
+ then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
+ moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp
ultimately show ?thesis by auto
qed
- moreover have "countable (B1 \<union> B2)" using `countable B1` `countable B2` by simp
+ moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
ultimately show ?thesis by auto
qed
@@ -579,10 +579,10 @@
using countable_separating_set_linorder1 by auto
have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y
proof -
- obtain z where "x < z" "z < y" using `x < y` dense by blast
+ obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast
then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto
- then have "x < b \<and> b < y" using `z < y` by auto
- then show ?thesis using `b \<in> B` by auto
+ then have "x < b \<and> b < y" using \<open>z < y\<close> by auto
+ then show ?thesis using \<open>b \<in> B\<close> by auto
qed
then show ?thesis using B(1) by auto
qed
@@ -680,7 +680,7 @@
shows "openin T (\<Inter>i \<in> I. U i)"
proof -
have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
- using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
+ using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
then show ?thesis
using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
qed
--- a/src/HOL/Analysis/ex/Circle_Area.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Analysis/ex/Circle_Area.thy Tue Jan 17 13:59:10 2017 +0100
@@ -4,7 +4,7 @@
A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
*)
-section {* The area of a circle *}
+section \<open>The area of a circle\<close>
theory Circle_Area
imports Complex_Main Interval_Integral
@@ -157,13 +157,13 @@
also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
proof (rule nn_integral_cong)
fix x from R show "(\<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel) = R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel"
- by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all
+ by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
qed
also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
using R by (intro nn_integral_cmult) simp_all
also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) =
R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel"
- by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all
+ by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
also {
fix x y
have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Tue Jan 17 13:59:10 2017 +0100
@@ -268,7 +268,7 @@
context bourbaki_witt_fixpoint begin
-lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}.\<close>
+lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close>
assumes "M \<in> Chains leq"
and "M \<noteq> {}"
and "finite M"
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Tue Jan 17 13:59:10 2017 +0100
@@ -773,8 +773,8 @@
shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
proof -
have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
- using `alw (HLD s) \<omega>` by (simp add: alw_iff_sdrop HLD_iff)
- from pigeonhole_infinite_rel[OF infinite_UNIV_nat `finite s` this]
+ using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
+ from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
show ?thesis
by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
qed
--- a/src/HOL/Library/Multiset.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Jan 17 13:59:10 2017 +0100
@@ -2805,7 +2805,7 @@
case (add z Z)
obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}"
"\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
- using mult_implies_one_step[OF `trans s` add(2)] by auto
+ using mult_implies_one_step[OF \<open>trans s\<close> add(2)] by auto
consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
thus ?case
@@ -2813,9 +2813,9 @@
case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
next
- case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) `irrefl s`
+ case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) \<open>irrefl s\<close>
by (auto simp: irrefl_def)
- moreover from this transD[OF `trans s` _ this(2)]
+ moreover from this transD[OF \<open>trans s\<close> _ this(2)]
have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x'
using 2 *(4)[rule_format, of x'] by auto
ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2
@@ -2825,7 +2825,7 @@
next
assume ?R then obtain I J K
where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s"
- using mult_implies_one_step[OF `trans s`] by blast
+ using mult_implies_one_step[OF \<open>trans s\<close>] by blast
thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed
@@ -2887,7 +2887,7 @@
proof -
{ assume "N \<noteq> M" "M - M \<inter># N = {#}"
then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
- then have "\<exists>y. count M y < count N y" using `M - M \<inter># N = {#}`
+ then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
}
then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
--- a/src/HOL/Library/Perm.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Perm.thy Tue Jan 17 13:59:10 2017 +0100
@@ -12,7 +12,7 @@
Grieviously missing are cycles since these would require more
elaboration, e.g. the concept of distinct lists equivalent
under rotation, which maybe would also deserve its own theory.
- But see theory @{text "src/HOL/ex/Perm_Fragments.thy"} for
+ But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for
fragments on that.
\<close>
--- a/src/HOL/Library/Polynomial_FPS.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Polynomial_FPS.thy Tue Jan 17 13:59:10 2017 +0100
@@ -163,7 +163,7 @@
The following simproc can reduce the equality of two polynomial FPSs two equality of the
respective polynomials. A polynomial FPS is one that only has finitely many non-zero
coefficients and can therefore be written as @{term "fps_of_poly p"} for some
- polynomial @{text "p"}.
+ polynomial \<open>p\<close>.
This may sound trivial, but it covers a number of annoying side conditions like
@{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.
--- a/src/HOL/Library/Polynomial_Factorial.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy Tue Jan 17 13:59:10 2017 +0100
@@ -52,7 +52,7 @@
subsection \<open>Lifting elements into the field of fractions\<close>
definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
- -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
+ \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
lemma to_fract_0 [simp]: "to_fract 0 = 0"
by (simp add: to_fract_def eq_fract Zero_fract_def)
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Jan 17 13:59:10 2017 +0100
@@ -187,7 +187,7 @@
proof -
show "class.factorial_semiring divide plus minus zero times one
unit_factor normalize"
- proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
+ proof (standard, rule factorial_semiring_altI_aux) \<comment> \<open>FIXME rule\<close>
fix x assume "x \<noteq> 0"
thus "finite {p. p dvd x \<and> normalize p = p}"
proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
--- a/src/HOL/Number_Theory/Primes.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Tue Jan 17 13:59:10 2017 +0100
@@ -310,7 +310,7 @@
"prime (numeral m :: nat) \<longleftrightarrow>
(1::nat) < numeral m \<and>
(\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)"
- by (fact prime_nat_simp) -- \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
+ by (fact prime_nat_simp) \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
text\<open>A bit of regression testing:\<close>
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Tue Jan 17 11:26:21 2017 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Tue Jan 17 13:59:10 2017 +0100
@@ -4,7 +4,7 @@
imports Gauss
begin
-text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *}
+text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>
locale QR =
fixes p :: "nat"