# HG changeset patch # User wenzelm # Date 1413921345 -7200 # Node ID e55fe82f3803ba8b64f7298a7c0d3b1a1a078149 # Parent cb9d84d3e7f270c8541484cc248abfa08a9a0e8a# Parent 790ff9eb2578dd0077290540aab50147c945a018 merged diff -r cb9d84d3e7f2 -r e55fe82f3803 NEWS --- a/NEWS Tue Oct 21 21:10:44 2014 +0200 +++ b/NEWS Tue Oct 21 21:55:45 2014 +0200 @@ -20,6 +20,10 @@ * Improved folding mode "isabelle" based on Isar syntax. Alternatively, the "sidekick" mode may be used for document structure. +* Extended bracket matching based on Isar language structure. System +option jedit_structure_limit determines maximum number of lines to +scan in the buffer. + * Support for BibTeX files: context menu, context-sensitive token marker, SideKick parser. diff -r cb9d84d3e7f2 -r e55fe82f3803 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Tue Oct 21 21:10:44 2014 +0200 +++ b/src/Doc/Implementation/Prelim.thy Tue Oct 21 21:55:45 2014 +0200 @@ -1048,10 +1048,9 @@ text \\medskip That position can be also printed in a message as follows:\ -ML_command \ - writeln - ("Look here" ^ Position.here (Binding.pos_of @{binding here})) -\ +ML_command + \writeln + ("Look here" ^ Position.here (Binding.pos_of @{binding here}))\ text \This illustrates a key virtue of formalized bindings as opposed to raw specifications of base names: the system can use this @@ -1062,8 +1061,6 @@ directly, which is occasionally useful for experimentation and diagnostic purposes:\ -ML_command \ - warning ("Look here" ^ Position.here @{here}) -\ +ML_command \warning ("Look here" ^ Position.here @{here})\ end diff -r cb9d84d3e7f2 -r e55fe82f3803 src/HOL/Hahn_Banach/Bounds.thy --- a/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 21:10:44 2014 +0200 +++ b/src/HOL/Hahn_Banach/Bounds.thy Tue Oct 21 21:55:45 2014 +0200 @@ -2,7 +2,7 @@ Author: Gertrud Bauer, TU Munich *) -header {* Bounds *} +header \Bounds\ theory Bounds imports Main "~~/src/HOL/Library/ContNotDenum" @@ -15,12 +15,9 @@ lemmas [elim?] = lub.least lub.upper -definition the_lub :: "'a::order set \ 'a" +definition the_lub :: "'a::order set \ 'a" ("\_" [90] 90) where "the_lub A = The (lub A)" -notation (xsymbols) - the_lub ("\_" [90] 90) - lemma the_lub_equality [elim?]: assumes "lub A x" shows "\A = (x::'a::order)" @@ -28,7 +25,7 @@ interpret lub A x by fact show ?thesis proof (unfold the_lub_def) - from `lub A x` show "The (lub A) = x" + from \lub A x\ show "The (lub A) = x" proof fix x' assume lub': "lub A x'" show "x' = x" diff -r cb9d84d3e7f2 -r e55fe82f3803 src/HOL/Hahn_Banach/Function_Norm.thy --- a/src/HOL/Hahn_Banach/Function_Norm.thy Tue Oct 21 21:10:44 2014 +0200 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy Tue Oct 21 21:55:45 2014 +0200 @@ -2,15 +2,15 @@ Author: Gertrud Bauer, TU Munich *) -header {* The norm of a function *} +header \The norm of a function\ theory Function_Norm imports Normed_Space Function_Order begin -subsection {* Continuous linear forms*} +subsection \Continuous linear forms\ -text {* +text \ A linear form @{text f} on a normed vector space @{text "(V, \\\)"} is \emph{continuous}, iff it is bounded, i.e. \begin{center} @@ -19,7 +19,7 @@ In our application no other functions than linear forms are considered, so we can define continuous linear forms as bounded linear forms: -*} +\ locale continuous = linearform + fixes norm :: "_ \ real" ("\_\") @@ -39,9 +39,9 @@ qed -subsection {* The norm of a linear form *} +subsection \The norm of a linear form\ -text {* +text \ The least real number @{text c} for which holds \begin{center} @{text "\x \ V. \f x\ \ c \ \x\"} @@ -70,7 +70,7 @@ @{text fn_norm} is equal to the supremum of @{text B}, if the supremum exists (otherwise it is undefined). -*} +\ locale fn_norm = fixes norm :: "_ \ real" ("\_\") @@ -83,34 +83,34 @@ lemma (in fn_norm) B_not_empty [intro]: "0 \ B V f" by (simp add: B_def) -text {* +text \ The following lemma states that every continuous linear form on a normed space @{text "(V, \\\)"} has a function norm. -*} +\ lemma (in normed_vectorspace_with_fn_norm) fn_norm_works: assumes "continuous V f norm" shows "lub (B V f) (\f\\V)" proof - interpret continuous V f norm by fact - txt {* The existence of the supremum is shown using the + txt \The existence of the supremum is shown using the completeness of the reals. Completeness means, that every - non-empty bounded set of reals has a supremum. *} + non-empty bounded set of reals has a supremum.\ have "\a. lub (B V f) a" proof (rule real_complete) - txt {* First we have to show that @{text B} is non-empty: *} + txt \First we have to show that @{text B} is non-empty:\ have "0 \ B V f" .. then show "\x. x \ B V f" .. - txt {* Then we have to show that @{text B} is bounded: *} + txt \Then we have to show that @{text B} is bounded:\ show "\c. \y \ B V f. y \ c" proof - - txt {* We know that @{text f} is bounded by some value @{text c}. *} + txt \We know that @{text f} is bounded by some value @{text c}.\ from bounded obtain c where c: "\x \ V. \f x\ \ c * \x\" .. - txt {* To prove the thesis, we have to show that there is some + txt \To prove the thesis, we have to show that there is some @{text b}, such that @{text "y \ b"} for all @{text "y \ - B"}. Due to the definition of @{text B} there are two cases. *} + B"}. Due to the definition of @{text B} there are two cases.\ def b \ "max c 0" have "\y \ B V f. y \ b" @@ -121,16 +121,16 @@ assume "y = 0" then show ?thesis unfolding b_def by arith next - txt {* The second case is @{text "y = \f x\ / \x\"} for some - @{text "x \ V"} with @{text "x \ 0"}. *} + txt \The second case is @{text "y = \f x\ / \x\"} for some + @{text "x \ V"} with @{text "x \ 0"}.\ assume "y \ 0" with y obtain x where y_rep: "y = \f x\ * inverse \x\" and x: "x \ V" and neq: "x \ 0" by (auto simp add: B_def divide_inverse) from x neq have gt: "0 < \x\" .. - txt {* The thesis follows by a short calculation using the - fact that @{text f} is bounded. *} + txt \The thesis follows by a short calculation using the + fact that @{text f} is bounded.\ note y_rep also have "\f x\ * inverse \x\ \ (c * \x\) * inverse \x\" @@ -162,7 +162,7 @@ proof - interpret continuous V f norm by fact have "lub (B V f) (\f\\V)" - using `continuous V f norm` by (rule fn_norm_works) + using \continuous V f norm\ by (rule fn_norm_works) from this and b show ?thesis .. qed @@ -173,32 +173,32 @@ proof - interpret continuous V f norm by fact have "lub (B V f) (\f\\V)" - using `continuous V f norm` by (rule fn_norm_works) + using \continuous V f norm\ by (rule fn_norm_works) from this and b show ?thesis .. qed -text {* The norm of a continuous function is always @{text "\ 0"}. *} +text \The norm of a continuous function is always @{text "\ 0"}.\ lemma (in normed_vectorspace_with_fn_norm) fn_norm_ge_zero [iff]: assumes "continuous V f norm" shows "0 \ \f\\V" proof - interpret continuous V f norm by fact - txt {* The function norm is defined as the supremum of @{text B}. + txt \The function norm is defined as the supremum of @{text B}. So it is @{text "\ 0"} if all elements in @{text B} are @{text "\ - 0"}, provided the supremum exists and @{text B} is not empty. *} + 0"}, provided the supremum exists and @{text B} is not empty.\ have "lub (B V f) (\f\\V)" - using `continuous V f norm` by (rule fn_norm_works) + using \continuous V f norm\ by (rule fn_norm_works) moreover have "0 \ B V f" .. ultimately show ?thesis .. qed -text {* +text \ \medskip The fundamental property of function norms is: \begin{center} @{text "\f x\ \ \f\ \ \x\"} \end{center} -*} +\ lemma (in normed_vectorspace_with_fn_norm) fn_norm_le_cong: assumes "continuous V f norm" "linearform V f" @@ -214,7 +214,7 @@ also have "f 0 = 0" by rule unfold_locales also have "\\\ = 0" by simp also have a: "0 \ \f\\V" - using `continuous V f norm` by (rule fn_norm_ge_zero) + using \continuous V f norm\ by (rule fn_norm_ge_zero) from x have "0 \ norm x" .. with a have "0 \ \f\\V * \x\" by (simp add: zero_le_mult_iff) finally show "\f x\ \ \f\\V * \x\" . @@ -227,20 +227,20 @@ from x show "0 \ \x\" .. from x and neq have "\f x\ * inverse \x\ \ B V f" by (auto simp add: B_def divide_inverse) - with `continuous V f norm` show "\f x\ * inverse \x\ \ \f\\V" + with \continuous V f norm\ show "\f x\ * inverse \x\ \ \f\\V" by (rule fn_norm_ub) qed finally show ?thesis . qed qed -text {* +text \ \medskip The function norm is the least positive real number for which the following inequation holds: \begin{center} @{text "\f x\ \ c \ \x\"} \end{center} -*} +\ lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]: assumes "continuous V f norm" @@ -274,7 +274,7 @@ qed finally show ?thesis . qed - qed (insert `continuous V f norm`, simp_all add: continuous_def) + qed (insert \continuous V f norm\, simp_all add: continuous_def) qed end diff -r cb9d84d3e7f2 -r e55fe82f3803 src/HOL/Hahn_Banach/Function_Order.thy --- a/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 21:10:44 2014 +0200 +++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 21:55:45 2014 +0200 @@ -2,15 +2,15 @@ Author: Gertrud Bauer, TU Munich *) -header {* An order on functions *} +header \An order on functions\ theory Function_Order imports Subspace Linearform begin -subsection {* The graph of a function *} +subsection \The graph of a function\ -text {* +text \ We define the \emph{graph} of a (real) function @{text f} with domain @{text F} as the set \begin{center} @@ -19,7 +19,7 @@ So we are modeling partial functions by specifying the domain and the mapping function. We use the term ``function'' also for its graph. -*} +\ type_synonym 'a graph = "('a \ real) set" @@ -38,12 +38,12 @@ using assms unfolding graph_def by blast -subsection {* Functions ordered by domain extension *} +subsection \Functions ordered by domain extension\ -text {* +text \ A function @{text h'} is an extension of @{text h}, iff the graph of @{text h} is a subset of the graph of @{text h'}. -*} +\ lemma graph_extI: "(\x. x \ H \ h x = h' x) \ H \ H' @@ -57,12 +57,12 @@ unfolding graph_def by blast -subsection {* Domain and function of a graph *} +subsection \Domain and function of a graph\ -text {* +text \ The inverse functions to @{text graph} are @{text domain} and @{text funct}. -*} +\ definition domain :: "'a graph \ 'a set" where "domain g = {x. \y. (x, y) \ g}" @@ -70,10 +70,10 @@ definition funct :: "'a graph \ ('a \ real)" where "funct g = (\x. (SOME y. (x, y) \ g))" -text {* +text \ The following lemma states that @{text g} is the graph of a function if the relation induced by @{text g} is unique. -*} +\ lemma graph_domain_funct: assumes uniq: "\x y z. (x, y) \ g \ (x, z) \ g \ z = y" @@ -91,18 +91,18 @@ qed -subsection {* Norm-preserving extensions of a function *} +subsection \Norm-preserving extensions of a function\ -text {* +text \ Given a linear form @{text f} on the space @{text F} and a seminorm @{text p} on @{text E}. The set of all linear extensions of @{text f}, to superspaces @{text H} of @{text F}, which are bounded by @{text p}, is defined as follows. -*} +\ definition norm_pres_extensions :: - "'a::{plus, minus, uminus, zero} set \ ('a \ real) \ 'a set \ ('a \ real) + "'a::{plus,minus,uminus,zero} set \ ('a \ real) \ 'a set \ ('a \ real) \ 'a graph set" where "norm_pres_extensions E p F f diff -r cb9d84d3e7f2 -r e55fe82f3803 src/HOL/Hahn_Banach/Hahn_Banach.thy --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 21 21:10:44 2014 +0200 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Tue Oct 21 21:55:45 2014 +0200 @@ -2,20 +2,20 @@ Author: Gertrud Bauer, TU Munich *) -header {* The Hahn-Banach Theorem *} +header \The Hahn-Banach Theorem\ theory Hahn_Banach imports Hahn_Banach_Lemmas begin -text {* +text \ We present the proof of two different versions of the Hahn-Banach Theorem, closely following @{cite \\S36\ "Heuser:1986"}. -*} +\ -subsection {* The Hahn-Banach Theorem for vector spaces *} +subsection \The Hahn-Banach Theorem for vector spaces\ -text {* +text \ \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real vector space @{text E}, let @{text p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on @{text F} such that @{text @@ -51,16 +51,16 @@ \end{itemize} \end{enumerate} -*} +\ theorem Hahn_Banach: assumes E: "vectorspace E" and "subspace F E" and "seminorm E p" and "linearform F f" assumes fp: "\x \ F. f x \ p x" shows "\h. linearform E h \ (\x \ F. h x = f x) \ (\x \ E. h x \ p x)" - -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *} - -- {* and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p}, *} - -- {* then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp *} + -- \Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\ + -- \and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\ + -- \then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp\ proof - interpret vectorspace E by fact interpret subspace F E by fact @@ -69,12 +69,12 @@ def M \ "norm_pres_extensions E p F f" then have M: "M = \" by (simp only:) from E have F: "vectorspace F" .. - note FE = `F \ E` + note FE = \F \ E\ { fix c assume cM: "c \ chains M" and ex: "\x. x \ c" have "\c \ M" - -- {* Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}: *} - -- {* @{text "\c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\c \ M"}. *} + -- \Show that every non-empty chain @{text c} of @{text M} has an upper bound in @{text M}:\ + -- \@{text "\c"} is greater than any element of the chain @{text c}, so it suffices to show @{text "\c \ M"}.\ unfolding M_def proof (rule norm_pres_extensionI) let ?H = "domain (\c)" @@ -104,9 +104,9 @@ qed } then have "\g \ M. \x \ M. g \ x \ x = g" - -- {* With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp *} + -- \With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp\ proof (rule Zorn's_Lemma) - -- {* We show that @{text M} is non-empty: *} + -- \We show that @{text M} is non-empty:\ show "graph F f \ M" unfolding M_def proof (rule norm_pres_extensionI2) @@ -125,18 +125,18 @@ and HE: "H \ E" and FH: "F \ H" and graphs: "graph F f \ graph H h" and hp: "\x \ H. h x \ p x" unfolding M_def .. - -- {* @{text g} is a norm-preserving extension of @{text f}, in other words: *} - -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *} - -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *} + -- \@{text g} is a norm-preserving extension of @{text f}, in other words:\ + -- \@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\ + -- \and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp\ from HE E have H: "vectorspace H" by (rule subspace.vectorspace) have HE_eq: "H = E" - -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *} + -- \We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp\ proof (rule classical) assume neq: "H \ E" - -- {* Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended *} - -- {* in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp *} + -- \Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\ + -- \in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp\ have "\g' \ M. g \ g' \ g \ g'" proof - from HE have "H \ E" .. @@ -147,12 +147,12 @@ proof assume "x' = 0" with H have "x' \ H" by (simp only: vectorspace.zero) - with `x' \ H` show False by contradiction + with \x' \ H\ show False by contradiction qed qed def H' \ "H + lin x'" - -- {* Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp *} + -- \Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp\ have HH': "H \ H'" proof (unfold H'_def) from x'E have "vectorspace (lin x')" .. @@ -162,9 +162,9 @@ obtain xi where xi: "\y \ H. - p (y + x') - h y \ xi \ xi \ p (y + x') - h y" - -- {* Pick a real number @{text \} that fulfills certain inequations; this will *} - -- {* be used to establish that @{text h'} is a norm-preserving extension of @{text h}. - \label{ex-xi-use}\skp *} + -- \Pick a real number @{text \} that fulfills certain inequations; this will\ + -- \be used to establish that @{text h'} is a norm-preserving extension of @{text h}. + \label{ex-xi-use}\skp\ proof - from H have "\xi. \y \ H. - p (y + x') - h y \ xi \ xi \ p (y + x') - h y" @@ -191,10 +191,10 @@ def h' \ "\x. let (y, a) = SOME (y, a). x = y + a \ x' \ y \ H in h y + a * xi" - -- {* Define the extension @{text h'} of @{text h} to @{text H'} using @{text \}. \skp *} + -- \Define the extension @{text h'} of @{text h} to @{text H'} using @{text \}. \skp\ have "g \ graph H' h' \ g \ graph H' h'" - -- {* @{text h'} is an extension of @{text h} \dots \skp *} + -- \@{text h'} is an extension of @{text h} \dots \skp\ proof show "g \ graph H' h'" proof - @@ -202,7 +202,7 @@ proof (rule graph_extI) fix t assume t: "t \ H" from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" - using `x' \ H` `x' \