--- a/src/HOL/Algebra/Complete_Lattice.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy Tue Dec 19 13:58:12 2017 +0100
@@ -543,7 +543,7 @@
end
-subsection \<open>Complete lattices where @{text eq} is the Equality\<close>
+subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>
locale complete_lattice = partial_order +
assumes sup_exists:
--- a/src/HOL/Algebra/Lattice.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Algebra/Lattice.thy Tue Dec 19 13:58:12 2017 +0100
@@ -52,11 +52,11 @@
definition
LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
- "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}" --\<open>least fixed point\<close>
+ "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}" \<comment>\<open>least fixed point\<close>
definition
GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
- "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}" --\<open>greatest fixed point\<close>
+ "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}" \<comment>\<open>greatest fixed point\<close>
subsection \<open>Dual operators\<close>
--- a/src/HOL/Algebra/Multiplicative_Group.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Tue Dec 19 13:58:12 2017 +0100
@@ -13,8 +13,8 @@
UnivPoly
begin
-section {* Simplification Rules for Polynomials *}
-text_raw {* \label{sec:simp-rules} *}
+section \<open>Simplification Rules for Polynomials\<close>
+text_raw \<open>\label{sec:simp-rules}\<close>
lemma (in ring_hom_cring) hom_sub[simp]:
assumes "x \<in> carrier R" "y \<in> carrier R"
@@ -114,13 +114,13 @@
-section {* Properties of the Euler @{text \<phi>}-function *}
-text_raw {* \label{sec:euler-phi} *}
+section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>
+text_raw \<open>\label{sec:euler-phi}\<close>
-text{*
+text\<open>
In this section we prove that for every positive natural number the equation
$\sum_{d | n}^n \varphi(d) = n$ holds.
-*}
+\<close>
lemma dvd_div_ge_1 :
fixes a b :: nat
@@ -156,7 +156,7 @@
lemma dvd_div_eq_1:
fixes a b c :: nat
assumes "c dvd a" "c dvd b" "a div c = b div c"
- shows "a = b" using assms dvd_mult_div_cancel[OF `c dvd a`] dvd_mult_div_cancel[OF `c dvd b`]
+ shows "a = b" using assms dvd_mult_div_cancel[OF \<open>c dvd a\<close>] dvd_mult_div_cancel[OF \<open>c dvd b\<close>]
by presburger
lemma dvd_div_eq_2:
@@ -167,7 +167,7 @@
have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto
have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
- finally show "a = b" using `c>0` dvd_div_ge_1[OF _ `a dvd c`] by fastforce
+ finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce
qed
lemma div_mult_mono:
@@ -179,7 +179,7 @@
thus ?thesis using assms by force
qed
-text{*
+text\<open>
We arrive at the main result of this section:
For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
@@ -208,7 +208,7 @@
and by showing
@{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}
(this is our counting argument) the thesis follows.
-*}
+\<close>
lemma sum_phi'_factors :
fixes n :: nat
assumes "n > 0"
@@ -220,19 +220,19 @@
proof (rule card_bij_eq)
{ fix a b assume "a * n div d = b * n div d"
hence "a * (n div d) = b * (n div d)"
- using dvd_div_mult[OF `d dvd n`] by (fastforce simp add: mult.commute)
- hence "a = b" using dvd_div_ge_1[OF _ `d dvd n`] `n>0`
+ using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
+ hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
by (simp add: mult.commute nat_mult_eq_cancel1)
} thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
{ fix a assume a:"a\<in>?RF"
- hence "a * (n div d) \<ge> 1" using `n>0` dvd_div_ge_1[OF _ `d dvd n`] by simp
- hence ge_1:"a * n div d \<ge> 1" by (simp add: `d dvd n` div_mult_swap)
+ hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
+ hence ge_1:"a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
have le_n:"a * n div d \<le> n" using div_mult_mono a by simp
have "gcd (a * n div d) n = n div d * gcd a d"
by (simp add: gcd_mult_distrib_nat q ac_simps)
hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
hence "a * n div d \<in> ?F"
- using ge_1 le_n by (fastforce simp add: `d dvd n`)
+ using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
} thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
{ fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
@@ -245,7 +245,7 @@
qed force+
} hence phi'_eq:"\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
unfolding phi'_def by presburger
- have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF `n>0`] by force
+ have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
have "(\<Sum>d | d dvd n. phi' d)
= card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq
@@ -262,8 +262,8 @@
finally show ?thesis by force
qed
-section {* Order of an Element of a Group *}
-text_raw {* \label{sec:order-elem} *}
+section \<open>Order of an Element of a Group\<close>
+text_raw \<open>\label{sec:order-elem}\<close>
context group begin
@@ -365,8 +365,8 @@
hence y_x:"y - x \<in> {d \<in> {1.. order G}. a (^) d = \<one>}" using y_x_range by blast
have "min (y - x) (ord a) = ord a"
- using Min.in_idem[OF `finite {d \<in> {1 .. order G} . a (^) d = \<one>}` y_x] ord_def by auto
- with `y - x < ord a` have False by linarith
+ using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a (^) d = \<one>}\<close> y_x] ord_def by auto
+ with \<open>y - x < ord a\<close> have False by linarith
}
note X = this
@@ -392,13 +392,13 @@
moreover
{ assume "x = ord a" "y < ord a"
hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
- hence "y=0" using ord_inj[OF assms] `y < ord a` unfolding inj_on_def by force
+ hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
moreover
{ assume "y = ord a" "x < ord a"
hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
- hence "x=0" using ord_inj[OF assms] `x < ord a` unfolding inj_on_def by force
+ hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
ultimately show False using A by force
@@ -418,7 +418,7 @@
hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)
have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
- hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using `y=a(^)r` by blast
+ hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a(^)r\<close> by blast
}
thus "?L \<subseteq> ?R" by auto
qed
@@ -434,7 +434,7 @@
hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)
hence "a(^)r = \<one>" using assms(3) by simp
have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
- hence "r = 0" using `a(^)r = \<one>` ord_def[of a] ord_min[of r a] assms(1-2) by linarith
+ hence "r = 0" using \<open>a(^)r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
thus ?thesis using q by simp
qed
@@ -463,13 +463,13 @@
have ge_1:"ord a div gcd n (ord a) \<ge> 1"
proof -
have "gcd n (ord a) dvd ord a" by blast
- thus ?thesis by (rule dvd_div_ge_1[OF `ord a \<ge> 1`])
+ thus ?thesis by (rule dvd_div_ge_1[OF \<open>ord a \<ge> 1\<close>])
qed
have "ord a \<le> order G" by (simp add: ord_le_group_order)
have "ord a div gcd n (ord a) \<le> order G"
proof -
have "ord a div gcd n (ord a) \<le> ord a" by simp
- thus ?thesis using `ord a \<le> order G` by linarith
+ thus ?thesis using \<open>ord a \<le> order G\<close> by linarith
qed
hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
using ge_1 pow_eq_1 by force
@@ -537,7 +537,7 @@
hence x_in_carrier: "x \<in> carrier G" by auto
then obtain d::nat where d:"x (^) d = \<one>" and "d\<ge>1"
using finite_group_elem_finite_ord by auto
- have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using `d\<ge>1` d nat_pow_Suc[of x "d - 1"] by simp
+ have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using \<open>d\<ge>1\<close> d nat_pow_Suc[of x "d - 1"] by simp
have elem:"x (^) (d - 1) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
proof -
obtain i::nat where i:"x = a(^)i" using x by auto
@@ -567,8 +567,8 @@
end
-section {* Number of Roots of a Polynomial *}
-text_raw {* \label{sec:number-roots} *}
+section \<open>Number of Roots of a Polynomial\<close>
+text_raw \<open>\label{sec:number-roots}\<close>
definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
@@ -674,15 +674,15 @@
\<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
have subs:"{a \<in> carrier R . eval R R id a f = \<zero>}
\<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
- using a_carrier `q \<in> _`
+ using a_carrier \<open>q \<in> _\<close>
by (auto simp: evalRR_simps lin_fac R.integral_iff)
have "{a \<in> carrier R . eval R R id a f = \<zero>} \<subseteq> insert a {a \<in> carrier R . eval R R id a q = \<zero>}"
using subs by auto
hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>
card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
- also have "\<dots> \<le> deg R f" using q_IH `Suc x = _`
+ also have "\<dots> \<le> deg R f" using q_IH \<open>Suc x = _\<close>
by (simp add: card_insert_if)
- finally show ?thesis using q_IH `Suc x = _` using finite by force
+ finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force
next
case False
hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto
@@ -712,20 +712,20 @@
by (auto simp: R.evalRR_simps)
then have "card {x \<in> carrier R. x (^) d = \<one>} \<le>
card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
- thus ?thesis using `deg R ?f = d` roots_bound by linarith
+ thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
qed
-section {* The Multiplicative Group of a Field *}
-text_raw {* \label{sec:mult-group} *}
+section \<open>The Multiplicative Group of a Field\<close>
+text_raw \<open>\label{sec:mult-group}\<close>
-text {*
+text \<open>
In this section we show that the multiplicative group of a finite field
is generated by a single element, i.e. it is cyclic. The proof is inspired
by the first proof given in the survey~\cite{conrad-cyclicity}.
-*}
+\<close>
lemma (in group) pow_order_eq_1:
assumes "finite (carrier G)" "x \<in> carrier G" shows "x (^) order G = \<one>"
@@ -789,8 +789,8 @@
using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
have "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {x \<in> carrier R. x (^) d = \<one>}"
using finite by (auto intro: card_mono)
- also have "\<dots> \<le> d" using `0 < order (mult_of R)` num_roots_le_deg[OF finite, of d]
- by (simp add : dvd_pos_nat[OF _ `d dvd order (mult_of R)`])
+ also have "\<dots> \<le> d" using \<open>0 < order (mult_of R)\<close> num_roots_le_deg[OF finite, of d]
+ by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)
qed
qed
@@ -811,7 +811,7 @@
hence "card ((\<lambda>n. a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d})
= card {k \<in> {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"
using card_image by blast
- thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' `a \<in> _`, unfolded ord_a]
+ thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \<open>a \<in> _\<close>, unfolded ord_a]
by (simp add: phi'_def)
qed
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Tue Dec 19 13:58:12 2017 +0100
@@ -496,7 +496,7 @@
cond_application_beta sum.delta' euclidean_representation
cong: if_cong)
-text \<open>TODO: generalize (via @{text compact_cball})?\<close>
+text \<open>TODO: generalize (via \<open>compact_cball\<close>)?\<close>
instance blinfun :: (euclidean_space, euclidean_space) heine_borel
proof
fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
--- a/src/HOL/Auth/Yahalom.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Auth/Yahalom.thy Tue Dec 19 13:58:12 2017 +0100
@@ -234,9 +234,9 @@
apply (erule yahalom.induct, force,
drule_tac [6] YM4_analz_knows_Spy)
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
- subgoal --\<open>Fake\<close> by spy_analz
- subgoal --\<open>YM3\<close> by blast
- subgoal --\<open>Oops\<close> by (blast dest: unique_session_keys)
+ subgoal \<comment>\<open>Fake\<close> by spy_analz
+ subgoal \<comment>\<open>YM3\<close> by blast
+ subgoal \<comment>\<open>Oops\<close> by (blast dest: unique_session_keys)
done
text\<open>Final version\<close>
@@ -314,8 +314,8 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
- subgoal --\<open>Fake\<close> by blast
- subgoal --\<open>YM3\<close> by blast
+ subgoal \<comment>\<open>Fake\<close> by blast
+ subgoal \<comment>\<open>YM3\<close> by blast
txt\<open>YM4. A is uncompromised because NB is secure
A's certificate guarantees the existence of the Server message\<close>
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
@@ -397,10 +397,10 @@
@{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
evs"}; then simplification can apply the induction hypothesis with
@{term "KK = {K}"}.\<close>
- subgoal --\<open>Fake\<close> by spy_analz
- subgoal --\<open>YM2\<close> by blast
- subgoal --\<open>YM3\<close> by blast
- subgoal --\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close>
+ subgoal \<comment>\<open>Fake\<close> by spy_analz
+ subgoal \<comment>\<open>YM2\<close> by blast
+ subgoal \<comment>\<open>YM3\<close> by blast
+ subgoal \<comment>\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close>
by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
done
@@ -484,13 +484,13 @@
frule_tac [6] YM4_analz_knows_Spy)
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
analz_insert_freshK)
- subgoal --\<open>Fake\<close> by spy_analz
- subgoal --\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast
- subgoal --\<open>YM2\<close> by blast
- subgoal --\<open>YM3: because no NB can also be an NA\<close>
+ subgoal \<comment>\<open>Fake\<close> by spy_analz
+ subgoal \<comment>\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast
+ subgoal \<comment>\<open>YM2\<close> by blast
+ subgoal \<comment>\<open>YM3: because no NB can also be an NA\<close>
by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
- subgoal --\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
- --\<open>Case analysis on whether Aa is bad;
+ subgoal \<comment>\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
+ \<comment>\<open>Case analysis on whether Aa is bad;
use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close>
apply clarify
apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
@@ -498,7 +498,7 @@
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
Spy_not_see_encrypted_key)
done
- subgoal --\<open>Oops case: if the nonce is betrayed now, show that the Oops event is
+ subgoal \<comment>\<open>Oops case: if the nonce is betrayed now, show that the Oops event is
covered by the quantified Oops assumption.\<close>
apply clarsimp
apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
@@ -596,10 +596,10 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
- subgoal --\<open>Fake\<close> by blast
- subgoal --\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
+ subgoal \<comment>\<open>Fake\<close> by blast
+ subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
by (force dest!: Crypt_imp_keysFor)
- subgoal --\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
+ subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
otherwise by unicity of session keys\<close>
by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
--- a/src/HOL/Auth/Yahalom2.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Tue Dec 19 13:58:12 2017 +0100
@@ -144,9 +144,9 @@
apply (erule rev_mp)
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy, simp_all)
-subgoal --\<open>Fake\<close> by (force dest!: keysFor_parts_insert)
-subgoal --\<open>YM3 \<close>by blast
-subgoal --\<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
+subgoal \<comment>\<open>Fake\<close> by (force dest!: keysFor_parts_insert)
+subgoal \<comment>\<open>YM3 \<close>by blast
+subgoal \<comment>\<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
done
@@ -400,10 +400,10 @@
apply (erule yahalom.induct, force,
frule_tac [6] YM4_parts_knows_Spy)
apply (analz_mono_contra, simp_all)
- subgoal --\<open>Fake\<close> by blast
- subgoal --\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
+ subgoal \<comment>\<open>Fake\<close> by blast
+ subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
by (force dest!: Crypt_imp_keysFor)
- subgoal --\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
+ subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
otherwise by unicity of session keys\<close>
by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
done
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue Dec 19 13:58:12 2017 +0100
@@ -35,7 +35,7 @@
text \<open>
If code generation fails with a message like
- @{text \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>},
+ \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>,
feel free to add an RBT implementation for the corrsponding operation
of delete that code equation (see above).
\<close>
--- a/src/HOL/Divides.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Divides.thy Tue Dec 19 13:58:12 2017 +0100
@@ -1327,7 +1327,7 @@
then show ?thesis ..
qed
-lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
+lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
lemma mod_2_not_eq_zero_eq_one_nat:
fixes n :: nat
--- a/src/HOL/Fun.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Fun.thy Tue Dec 19 13:58:12 2017 +0100
@@ -154,7 +154,7 @@
abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "surj f \<equiv> range f = UNIV"
-translations -- \<open>The negated case:\<close>
+translations \<comment> \<open>The negated case:\<close>
"\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
--- a/src/HOL/Power.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Power.thy Tue Dec 19 13:58:12 2017 +0100
@@ -651,7 +651,7 @@
lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
by (force simp add: power2_eq_square mult_less_0_iff)
-lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" \<comment> \<open>FIXME simp?\<close>
by (induct n) (simp_all add: abs_mult)
lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Dec 19 13:58:12 2017 +0100
@@ -125,7 +125,7 @@
code_pred predicate_where_argument_is_neg_condition_and_in_equation .
-text {* Another related example that required slight adjustment of the proof procedure *}
+text \<open>Another related example that required slight adjustment of the proof procedure\<close>
inductive if_as_predicate :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
--- a/src/HOL/Probability/Conditional_Expectation.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Conditional_Expectation.thy Tue Dec 19 13:58:12 2017 +0100
@@ -8,7 +8,7 @@
imports Probability_Measure
begin
-subsection {*Restricting a measure to a sub-sigma-algebra*}
+subsection \<open>Restricting a measure to a sub-sigma-algebra\<close>
definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
"subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))"
@@ -83,7 +83,7 @@
then have "U \<in> sets F" by simp
then have "U \<in> sets M" using assms(1) by (meson subalgebra_def subsetD)
then have "U \<in> null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast
- then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] `U \<in> sets F` by auto
+ then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] \<open>U \<in> sets F\<close> by auto
then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg)
qed
@@ -119,9 +119,9 @@
shows "f \<in> measurable M N"
using assms unfolding measurable_def subalgebra_def by auto
-text{*The following is the direct transposition of \verb+nn_integral_subalgebra+
+text\<open>The following is the direct transposition of \verb+nn_integral_subalgebra+
(from \verb+Nonnegative_Lebesgue_Integration+) in the
-current notations, with the removal of the useless assumption $f \geq 0$.*}
+current notations, with the removal of the useless assumption $f \geq 0$.\<close>
lemma nn_integral_subalgebra2:
assumes "subalgebra M F" and [measurable]: "f \<in> borel_measurable F"
@@ -135,8 +135,8 @@
by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)])
qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
-text{*The following is the direct transposition of \verb+integral_subalgebra+
-(from \verb+Bochner_Integration+) in the current notations.*}
+text\<open>The following is the direct transposition of \verb+integral_subalgebra+
+(from \verb+Bochner_Integration+) in the current notations.\<close>
lemma integral_subalgebra2:
fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
@@ -177,9 +177,9 @@
finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) < \<infinity>" by simp
qed
-subsection {*Nonnegative conditional expectation*}
+subsection \<open>Nonnegative conditional expectation\<close>
-text {* The conditional expectation of a function $f$, on a measure space $M$, with respect to a
+text \<open>The conditional expectation of a function $f$, on a measure space $M$, with respect to a
sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any
$F$-set coincides with the integral of $f$.
Such a function is uniquely defined almost everywhere.
@@ -192,7 +192,7 @@
In this paragraph, we develop the definition and basic properties for nonnegative functions,
as the basics of the general case. As in the definition of integrals, the nonnegative case is done
with ennreal-valued functions, without any integrability assumption.
-*}
+\<close>
definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
where
@@ -207,11 +207,11 @@
by (simp_all add: nn_cond_exp_def)
(metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def)
-text {* The good setting for conditional expectations is the situation where the subalgebra $F$
+text \<open>The good setting for conditional expectations is the situation where the subalgebra $F$
gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
-This means that a positive integrable function can have no meaningful conditional expectation.*}
+This means that a positive integrable function can have no meaningful conditional expectation.\<close>
locale sigma_finite_subalgebra =
fixes M F::"'a measure"
@@ -230,15 +230,15 @@
have "A \<subseteq> sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce
then have "A \<subseteq> sets M" using subalg subalgebra_def by force
moreover have "\<Union>A = space M" using Ap space_restr_to_subalg by simp
- moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] `A \<subseteq> sets F` Ap)
+ moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] \<open>A \<subseteq> sets F\<close> Ap)
ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)" using Ap by auto
qed
sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure
using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
-text {* Conditional expectations are very often used in probability spaces. This is a special case
-of the previous one, as we prove now. *}
+text \<open>Conditional expectations are very often used in probability spaces. This is a special case
+of the previous one, as we prove now.\<close>
locale finite_measure_subalgebra = finite_measure +
fixes F::"'a measure"
@@ -268,14 +268,14 @@
context sigma_finite_subalgebra
begin
-text{* The next lemma is arguably the most fundamental property of conditional expectation:
+text\<open>The next lemma is arguably the most fundamental property of conditional expectation:
when computing an expectation against an $F$-measurable function, it is equivalent to work
with a function or with its $F$-conditional expectation.
This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
From this point on, we will only work with it, and forget completely about
the definition using Radon-Nikodym derivatives.
-*}
+\<close>
lemma nn_cond_exp_intg:
assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
@@ -371,7 +371,7 @@
fix A assume [measurable]: "A \<in> sets F"
then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
have "\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
- by (rule nn_set_integral_add) (auto simp add: assms `A \<in> sets M`)
+ by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>)
also have "... = (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F g x \<partial>M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
also have "... = (\<integral>\<^sup>+x. indicator A x * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * g x \<partial>M)"
@@ -379,7 +379,7 @@
also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
by (metis (no_types, lifting) mult.commute nn_integral_cong)
also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
- by (rule nn_set_integral_add[symmetric]) (auto simp add: assms `A \<in> sets M`)
+ by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>)
finally show "\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M = \<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M"
by simp
qed (auto simp add: assms)
@@ -450,14 +450,14 @@
end
-subsection {*Real conditional expectation*}
+subsection \<open>Real conditional expectation\<close>
-text {*Once conditional expectations of positive functions are defined, the definition for real-valued functions
+text \<open>Once conditional expectations of positive functions are defined, the definition for real-valued functions
follows readily, by taking the difference of positive and negative parts.
One could also define a conditional expectation of vector-space valued functions, as in
\verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I
concentrate on it. (It is also essential for the case of the most general Pettis integral.)
-*}
+\<close>
definition real_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where
"real_cond_exp M F f =
@@ -497,7 +497,7 @@
then show ?thesis using eq by simp
qed
-text{* The next lemma shows that the conditional expectation
+text\<open>The next lemma shows that the conditional expectation
is an $F$-measurable function whose average against an $F$-measurable
function $f$ coincides with the average of the original function against $f$.
It is obtained as a consequence of the same property for the positive conditional
@@ -511,7 +511,7 @@
Once this lemma is available, we will use it to characterize the conditional expectation,
and never come back to the original technical definition, as we did in the case of the
nonnegative conditional expectation.
-*}
+\<close>
lemma real_cond_exp_intg_fpos:
assumes "integrable M (\<lambda>x. f x * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
@@ -738,7 +738,7 @@
shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)"
proof -
have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
- have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+ have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
qed
@@ -789,12 +789,12 @@
proof (rule real_cond_exp_charact)
fix A assume "A \<in> sets F"
then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
- have [measurable]: "A \<in> sets M" using subalg by (meson `A \<in> sets F` subalgebra_def subsetD)
+ have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
by (simp add: mult.commute mult.left_commute)
also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
- using integrable_mult_indicator[OF `A \<in> sets M` assms(3)] by (simp add: mult.commute mult.left_commute)
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
by (simp add: mult.commute mult.left_commute)
finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
@@ -812,22 +812,22 @@
fix A assume [measurable]: "A \<in> sets F"
then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
have intAf: "integrable M (\<lambda>x. indicator A x * f x)"
- using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
- using integrable_mult_indicator[OF `A \<in> sets M` assms(2)] by auto
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
apply (rule set_integral_add, auto simp add: assms)
- using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]]
- integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(2)]] by simp_all
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
+ integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)"
by auto
also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
- using real_cond_exp_intg(2) assms `A \<in> sets F` intAf intAg by auto
+ using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
by auto
also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
- by (rule set_integral_add(2)[symmetric]) (auto simp add: assms `A \<in> sets M` intAf intAg)
+ by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
by simp
qed (auto simp add: assms)
@@ -924,7 +924,7 @@
have "emeasure (restr_to_subalg M F) X = emeasure M X"
by (simp add: emeasure_restr_to_subalg subalg)
then have "emeasure (restr_to_subalg M F) X > 0"
- using `\<not>(emeasure M X) = 0` gr_zeroI by auto
+ using \<open>\<not>(emeasure M X) = 0\<close> gr_zeroI by auto
then obtain A where "A \<in> sets (restr_to_subalg M F)" "A \<subseteq> X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < \<infinity>"
using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans
not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
@@ -933,16 +933,16 @@
have Ic: "set_integrable M A (\<lambda>x. c)"
using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
have If: "set_integrable M A f"
- by (rule integrable_mult_indicator, auto simp add: `integrable M f`)
+ by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
proof (rule antisym)
show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
- by (rule real_cond_exp_intA, auto simp add: `integrable M f`)
+ by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
apply (rule set_integral_mono)
- apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF `integrable M f`])
+ apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
using Ic X_def \<open>A \<subseteq> X\<close> by auto
finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
qed
@@ -952,10 +952,10 @@
then have "AE x\<in>A in M. c = f x" by auto
then have "AE x\<in>A in M. False" using assms(2) by auto
have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>)
- then show False using `emeasure (restr_to_subalg M F) A > 0`
+ then show False using \<open>emeasure (restr_to_subalg M F) A > 0\<close>
by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
qed
- then show ?thesis using AE_iff_null_sets[OF `X \<in> sets M`] unfolding X_def by auto
+ then show ?thesis using AE_iff_null_sets[OF \<open>X \<in> sets M\<close>] unfolding X_def by auto
qed
lemma real_cond_exp_less_c:
@@ -964,7 +964,7 @@
shows "AE x in M. real_cond_exp M F f x < c"
proof -
have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
- using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
+ using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x > -c"
apply (rule real_cond_exp_gr_c) using assms by auto
ultimately show ?thesis by auto
@@ -978,7 +978,7 @@
obtain u::"nat \<Rightarrow> real" where u: "\<And>n. u n < c" "u \<longlonglongrightarrow> c"
using approx_from_below_dense_linorder[of "c-1" c] by auto
have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat
- apply (rule real_cond_exp_gr_c) using assms `u n < c` by auto
+ apply (rule real_cond_exp_gr_c) using assms \<open>u n < c\<close> by auto
have "AE x in M. \<forall>n. real_cond_exp M F f x > u n"
by (subst AE_all_countable, auto simp add: *)
moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x
@@ -995,7 +995,7 @@
shows "AE x in M. real_cond_exp M F f x \<le> c"
proof -
have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
- using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
+ using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x \<ge> -c"
apply (rule real_cond_exp_ge_c) using assms by auto
ultimately show ?thesis by auto
@@ -1038,9 +1038,9 @@
fix A assume [measurable]: "A \<in> sets F"
then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
- using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
- using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]] by auto
+ using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]] by auto
have inti: "(\<integral>x. indicator A x * f i x \<partial>M) = (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M)" for i
by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
@@ -1057,8 +1057,8 @@
finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto
qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
-text {*Jensen's inequality, describing the behavior of the integral under a convex function, admits
-a version for the conditional expectation, as follows.*}
+text \<open>Jensen's inequality, describing the behavior of the integral under a convex function, admits
+a version for the conditional expectation, as follows.\<close>
theorem real_cond_exp_jensens_inequality:
fixes q :: "real \<Rightarrow> real"
@@ -1075,14 +1075,14 @@
have **: "q (X x) \<ge> q (real_cond_exp M F X x) + phi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
unfolding phi_def apply (rule convex_le_Inf_differential)
- using `convex_on I q` that `interior I = I` by auto
- text {*It is not clear that the function $\phi$ is measurable. We replace it by a version which
- is better behaved.*}
+ using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto
+ text \<open>It is not clear that the function $\phi$ is measurable. We replace it by a version which
+ is better behaved.\<close>
define psi where "psi = (\<lambda>x. phi x * indicator I x)"
have A: "psi y = phi y" if "y \<in> I" for y unfolding psi_def indicator_def using that by auto
have *: "q (X x) \<ge> q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
- unfolding A[OF `real_cond_exp M F X x \<in> I`] using ** that by auto
+ unfolding A[OF \<open>real_cond_exp M F X x \<in> I\<close>] using ** that by auto
note I
moreover have "AE x in M. real_cond_exp M F X x > a" if "I \<subseteq> {a <..}" for a
@@ -1094,12 +1094,12 @@
then have main_ineq: "AE x in M. q (X x) \<ge> q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
using * X(2) by auto
- text {*Then, one wants to take the conditional expectation of this inequality. On the left, one gets
+ text \<open>Then, one wants to take the conditional expectation of this inequality. On the left, one gets
the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one
is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only
works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The
trick is to multiply by a $F$-measurable function which is small enough to make
- everything integrable.*}
+ everything integrable.\<close>
obtain f::"'a \<Rightarrow> real" where [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
"integrable (restr_to_subalg M F) f"
@@ -1123,31 +1123,31 @@
then have main_G: "AE x in M. g x * q (X x) \<ge> g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)"
unfolding G_def by (auto simp add: algebra_simps)
- text {*To proceed, we need to know that $\psi$ is measurable.*}
+ text \<open>To proceed, we need to know that $\psi$ is measurable.\<close>
have phi_mono: "phi x \<le> phi y" if "x \<le> y" "x \<in> I" "y \<in> I" for x y
proof (cases "x < y")
case True
have "q x + phi x * (y-x) \<le> q y"
- unfolding phi_def apply (rule convex_le_Inf_differential) using `convex_on I q` that `interior I = I` by auto
+ unfolding phi_def apply (rule convex_le_Inf_differential) using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto
then have "phi x \<le> (q x - q y) / (x - y)"
- using that `x < y` by (auto simp add: divide_simps algebra_simps)
+ using that \<open>x < y\<close> by (auto simp add: divide_simps algebra_simps)
moreover have "(q x - q y)/(x - y) \<le> phi y"
unfolding phi_def proof (rule cInf_greatest, auto)
fix t assume "t \<in> I" "y < t"
have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
- apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
+ apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
also have "... \<le> (q y - q t) / (y - t)"
- apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
+ apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
next
- obtain e where "0 < e" "ball y e \<subseteq> I" using `open I` `y \<in> I` openE by blast
+ obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> openE by blast
then have "y + e/2 \<in> {y<..} \<inter> I" by (auto simp: dist_real_def)
then show "{y<..} \<inter> I = {} \<Longrightarrow> False" by auto
qed
ultimately show "phi x \<le> phi y" by auto
next
case False
- then have "x = y" using `x \<le> y` by auto
+ then have "x = y" using \<open>x \<le> y\<close> by auto
then show ?thesis by auto
qed
have [measurable]: "psi \<in> borel_measurable borel"
@@ -1161,27 +1161,27 @@
"G \<in> borel_measurable F" "G \<in> borel_measurable M"
using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto
have int1: "integrable (restr_to_subalg M F) (\<lambda>x. g x * q (real_cond_exp M F X x))"
- apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg `integrable (restr_to_subalg M F) f`)
+ apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg \<open>integrable (restr_to_subalg M F) f\<close>)
unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps)
have int2: "integrable M (\<lambda>x. G x * (X x - real_cond_exp M F X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>X x\<bar> + \<bar>real_cond_exp M F X x\<bar>"])
- apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int `integrable M X` AE_I2)
+ apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int \<open>integrable M X\<close> AE_I2)
using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le)
have int3: "integrable M (\<lambda>x. g x * q (X x))"
apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. q(X x)"], auto simp add: q(1) abs_mult)
using g by (simp add: less_imp_le mult_left_le_one_le)
- text {*Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
- the following.*}
+ text \<open>Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
+ the following.\<close>
have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x \<ge> real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x"
apply (rule real_cond_exp_mono[OF main_G])
apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]])
using int2 int3 by auto
- text {*This reduces to the desired inequality thanks to the properties of conditional expectation,
+ text \<open>This reduces to the desired inequality thanks to the properties of conditional expectation,
i.e., the conditional expectation of an $F$-measurable function is this function, and one can
multiply an $F$-measurable function outside of conditional expectations.
Since all these equalities only hold almost everywhere, we formulate them separately,
- and then combine all of them to simplify the above equation, again almost everywhere.*}
+ and then combine all of them to simplify the above equation, again almost everywhere.\<close>
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x = g x * real_cond_exp M F (\<lambda>x. q (X x)) x"
by (rule real_cond_exp_mult, auto simp add: int3)
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x
@@ -1192,16 +1192,16 @@
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. G x * (X x - real_cond_exp M F X x)) x = G x * real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x"
by (rule real_cond_exp_mult, auto simp add: int2)
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x = real_cond_exp M F X x - real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x"
- by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int `integrable M X`)
+ by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
moreover have "AE x in M. real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x = real_cond_exp M F X x "
- by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int `integrable M X`)
+ by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
ultimately have "AE x in M. g x * real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> g x * q (real_cond_exp M F X x)"
by auto
then show "AE x in M. real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> q (real_cond_exp M F X x)"
using g(1) by (auto simp add: divide_simps)
qed
-text {*Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
+text \<open>Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
bound for it. Indeed, this is not true in general, as the following counterexample shows:
on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
@@ -1214,7 +1214,7 @@
However, this counterexample is essentially the only situation where this function is not
integrable, as shown by the next lemma.
-*}
+\<close>
lemma integrable_convex_cond_exp:
fixes q :: "real \<Rightarrow> real"
@@ -1242,12 +1242,12 @@
interpret finite_measure M using 2 by (auto intro!: finite_measureI)
have "I \<noteq> {}"
- using `AE x in M. X x \<in> I` 2 eventually_mono integral_less_AE_space by fastforce
+ using \<open>AE x in M. X x \<in> I\<close> 2 eventually_mono integral_less_AE_space by fastforce
then obtain z where "z \<in> I" by auto
define A where "A = Inf ((\<lambda>t. (q z - q t) / (z - t)) ` ({z<..} \<inter> I))"
have "q y \<ge> q z + A * (y - z)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
- using `z \<in> I` `y \<in> I` `interior I = I` q(2) by auto
+ using \<open>z \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto
then have "AE x in M. q (real_cond_exp M F X x) \<ge> q z + A * (real_cond_exp M F X x - z)"
using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
@@ -1271,8 +1271,8 @@
define e where "e = \<bar>q(0)\<bar> / 2"
then have "e > 0" using * by auto
have "continuous (at 0) q"
- using q(2) `0 \<in> I` `open I` \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
- then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using `e > 0`
+ using q(2) \<open>0 \<in> I\<close> \<open>open I\<close> \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
+ then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using \<open>e > 0\<close>
by (metis continuous_at_real_range real_norm_def)
then have *: "\<bar>q(y)\<bar> > e" if "\<bar>y\<bar> < d" for y
proof -
@@ -1282,7 +1282,7 @@
then show ?thesis unfolding e_def by simp
qed
have "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} \<le> emeasure M ({x \<in> space M. 1 \<le> ennreal(1/e) * \<bar>q(X x)\<bar>} \<inter> space M)"
- by (rule emeasure_mono, auto simp add: * `e>0` less_imp_le ennreal_mult''[symmetric])
+ by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> less_imp_le ennreal_mult''[symmetric])
also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)"
by (rule nn_integral_Markov_inequality, auto)
also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto
@@ -1293,7 +1293,7 @@
finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp
have "{x \<in> space M. \<bar>X x\<bar> \<ge> d} = {x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M"
- by (auto simp add: `d>0` ennreal_mult''[symmetric])
+ by (auto simp add: \<open>d>0\<close> ennreal_mult''[symmetric])
then have "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} = emeasure M ({x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M)"
by auto
also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)"
@@ -1311,13 +1311,13 @@
also have "... \<le> emeasure M {x \<in> space M. \<bar>X x\<bar> < d} + emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d}"
by (auto intro!: emeasure_subadditive)
also have "... < \<infinity>" using A B by auto
- finally show False using `emeasure M (space M) = \<infinity>` by auto
+ finally show False using \<open>emeasure M (space M) = \<infinity>\<close> by auto
qed
define A where "A = Inf ((\<lambda>t. (q 0 - q t) / (0 - t)) ` ({0<..} \<inter> I))"
have "q y \<ge> q 0 + A * (y - 0)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
- using `0 \<in> I` `y \<in> I` `interior I = I` q(2) by auto
- then have "q y \<ge> A * y" if "y \<in> I" for y using `q 0 = 0` that by auto
+ using \<open>0 \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto
+ then have "q y \<ge> A * y" if "y \<in> I" for y using \<open>q 0 = 0\<close> that by auto
then have "AE x in M. q (real_cond_exp M F X x) \<ge> A * real_cond_exp M F X x"
using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
--- a/src/HOL/Probability/Essential_Supremum.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Essential_Supremum.thy Tue Dec 19 13:58:12 2017 +0100
@@ -10,12 +10,12 @@
lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
by (simp add: AE_iff_measurable trivial_limit_def)
-section {*The essential supremum*}
+section \<open>The essential supremum\<close>
-text {*In this paragraph, we define the essential supremum and give its basic properties. The
+text \<open>In this paragraph, we define the essential supremum and give its basic properties. The
essential supremum of a function is its maximum value if one is allowed to throw away a set
of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
-it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*}
+it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close>
definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)"
@@ -56,14 +56,14 @@
have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
proof -
have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
- using `z > esssup M f` f by (auto simp: esssup_eq Inf_less_iff)
+ using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff)
then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto
then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto
- have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using `w < z` by auto
+ have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using \<open>w < z\<close> by auto
show ?thesis using null_sets_subset[OF a _ b] by simp
qed
obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
- using approx_from_above_dense_linorder[OF `esssup M f < top`] by auto
+ using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto
have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})"
using u apply auto
apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
--- a/src/HOL/Probability/Giry_Monad.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Tue Dec 19 13:58:12 2017 +0100
@@ -1746,19 +1746,19 @@
shows "bind M f = bind N g"
proof cases
assume "space N = {}" then show ?thesis
- using `M = N` by (simp add: bind_empty)
+ using \<open>M = N\<close> by (simp add: bind_empty)
next
assume "space N \<noteq> {}"
- show ?thesis unfolding `M = N`
+ show ?thesis unfolding \<open>M = N\<close>
proof (rule measure_eqI)
have *: "sets (N \<bind> f) = sets B"
- using sets_bind[OF sets_kernel[OF f] `space N \<noteq> {}`] by simp
+ using sets_bind[OF sets_kernel[OF f] \<open>space N \<noteq> {}\<close>] by simp
then show "sets (N \<bind> f) = sets (N \<bind> g)"
- using sets_bind[OF sets_kernel[OF g] `space N \<noteq> {}`] by auto
+ using sets_bind[OF sets_kernel[OF g] \<open>space N \<noteq> {}\<close>] by auto
fix A assume "A \<in> sets (N \<bind> f)"
then have "A \<in> sets B"
unfolding * .
- with ae f g `space N \<noteq> {}` show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A"
+ with ae f g \<open>space N \<noteq> {}\<close> show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A"
by (subst (1 2) emeasure_bind[where N=B]) (auto intro!: nn_integral_cong_AE)
qed
qed
--- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Dec 19 13:58:12 2017 +0100
@@ -808,7 +808,7 @@
finally show ?thesis .
qed
-lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
+lemma continuous_on_LINT_pmf: \<comment> \<open>This is dominated convergence!?\<close>
fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::{banach, second_countable_topology}"
assumes f: "\<And>i. i \<in> set_pmf M \<Longrightarrow> continuous_on A (f i)"
and bnd: "\<And>a i. a \<in> A \<Longrightarrow> i \<in> set_pmf M \<Longrightarrow> norm (f i a) \<le> B"
--- a/src/HOL/Probability/Stopping_Time.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Probability/Stopping_Time.thy Tue Dec 19 13:58:12 2017 +0100
@@ -1,6 +1,6 @@
(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
-section {* Stopping times *}
+section \<open>Stopping times\<close>
theory Stopping_Time
imports "HOL-Analysis.Analysis"
--- a/src/HOL/Real.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Real.thy Tue Dec 19 13:58:12 2017 +0100
@@ -23,7 +23,7 @@
subsection \<open>Preliminary lemmas\<close>
-text{*Useful in convergence arguments*}
+text\<open>Useful in convergence arguments\<close>
lemma inverse_of_nat_le:
fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
by (simp add: frac_le)
--- a/src/HOL/Rings.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Rings.thy Tue Dec 19 13:58:12 2017 +0100
@@ -1273,7 +1273,7 @@
and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
- -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
+ \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
fixes normalize :: "'a \<Rightarrow> 'a"
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Tue Dec 19 13:58:12 2017 +0100
@@ -380,7 +380,7 @@
using assms by (metis mult_le_0_iff)
-subsection {* Linear arithmetic for natural numbers *}
+subsection \<open>Linear arithmetic for natural numbers\<close>
declare [[smt_nat_as_int]]
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Dec 19 13:58:12 2017 +0100
@@ -222,7 +222,7 @@
by smt+
-section {* Natural numbers *}
+section \<open>Natural numbers\<close>
declare [[smt_nat_as_int]]
--- a/src/HOL/Topological_Spaces.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Dec 19 13:58:12 2017 +0100
@@ -1486,10 +1486,10 @@
by (metis first_countable_topology_class.countable_basis)
define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z > x)"
have "\<exists>z. z \<in> U \<and> x < z" if "x \<in> U" "open U" for U
- using open_right[OF `open U` `x \<in> U` `x < y`]
+ using open_right[OF \<open>open U\<close> \<open>x \<in> U\<close> \<open>x < y\<close>]
by (meson atLeastLessThan_iff dense less_imp_le subset_eq)
then have *: "u n \<in> A n \<and> x < u n" for n
- using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
+ using \<open>x \<in> A n\<close> \<open>open (A n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
then have "u \<longlonglongrightarrow> x" using A(3) by simp
then show ?thesis using * by auto
qed
@@ -1504,10 +1504,10 @@
by (metis first_countable_topology_class.countable_basis)
define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z < x)"
have "\<exists>z. z \<in> U \<and> z < x" if "x \<in> U" "open U" for U
- using open_left[OF `open U` `x \<in> U` `x > y`]
+ using open_left[OF \<open>open U\<close> \<open>x \<in> U\<close> \<open>x > y\<close>]
by (meson dense greaterThanAtMost_iff less_imp_le subset_eq)
then have *: "u n \<in> A n \<and> u n < x" for n
- using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
+ using \<open>x \<in> A n\<close> \<open>open (A n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
then have "u \<longlonglongrightarrow> x" using A(3) by simp
then show ?thesis using * by auto
qed
@@ -3478,7 +3478,7 @@
by (auto simp add: separation_t2)
define T where "T = U \<times> V"
have "open T" using * open_Times T_def by auto
- moreover have "t \<in> T" unfolding T_def using `t = (x,y)` * by auto
+ moreover have "t \<in> T" unfolding T_def using \<open>t = (x,y)\<close> * by auto
moreover have "T \<subseteq> {(x, y) | x y. x \<noteq> y}" unfolding T_def using * by auto
ultimately show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {(x, y) | x y. x \<noteq> y}" by auto
qed
@@ -3501,18 +3501,18 @@
then obtain z where z: "y < z \<and> z < x" by blast
define T where "T = {z<..} \<times> {..<z}"
have "open T" unfolding T_def by (simp add: open_Times)
- moreover have "t \<in> T" using T_def z `t = (x,y)` by auto
+ moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto
moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. y < z \<and> z < x)"
then have *: "{x ..} = {y<..}" "{..< x} = {..y}"
- using `x > y` apply auto using leI by blast
+ using \<open>x > y\<close> apply auto using leI by blast
define T where "T = {x ..} \<times> {.. y}"
then have "T = {y<..} \<times> {..< x}" using * by simp
then have "open T" unfolding T_def by (simp add: open_Times)
- moreover have "t \<in> T" using T_def `t = (x,y)` by auto
- moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def using `x > y` by auto
+ moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto
+ moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def using \<open>x > y\<close> by auto
ultimately show ?thesis by auto
qed
qed
@@ -3535,18 +3535,18 @@
then obtain z where z: "y > z \<and> z > x" by blast
define T where "T = {..<z} \<times> {z<..}"
have "open T" unfolding T_def by (simp add: open_Times)
- moreover have "t \<in> T" using T_def z `t = (x,y)` by auto
+ moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto
moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def by auto
ultimately show ?thesis by auto
next
assume "\<not>(\<exists>z. y > z \<and> z > x)"
then have *: "{..x} = {..<y}" "{x<..} = {y..}"
- using `x < y` apply auto using leI by blast
+ using \<open>x < y\<close> apply auto using leI by blast
define T where "T = {..x} \<times> {y..}"
then have "T = {..<y} \<times> {x<..}" using * by simp
then have "open T" unfolding T_def by (simp add: open_Times)
- moreover have "t \<in> T" using T_def `t = (x,y)` by auto
- moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def using `x < y` by auto
+ moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto
+ moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def using \<open>x < y\<close> by auto
ultimately show ?thesis by auto
qed
qed
--- a/src/HOL/ex/Perm_Fragments.thy Tue Dec 19 14:51:27 2017 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy Tue Dec 19 13:58:12 2017 +0100
@@ -97,7 +97,7 @@
lemma orbit_cycle_elem:
assumes "distinct as" and "a \<in> set as"
shows "orbit \<langle>as\<rangle> a = set as"
- oops -- \<open>(we need rotation here\<close>
+ oops \<comment> \<open>(we need rotation here\<close>
lemma order_cycle_elem:
assumes "distinct as" and "a \<in> set as"