summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 19 Dec 2017 13:58:12 +0100 | |

changeset 67226 | ec32cdaab97b |

parent 67225 | cb34f5f49a08 |

child 67227 | 6f6b26557ea9 |

child 67228 | 7c7b76695c90 |

isabelle update_cartouches -c -t;

--- 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"