--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 18:17:26 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Oct 29 18:53:58 2009 +0100
@@ -132,18 +132,19 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. @{text"x1"}, are still
-printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
+e.g. @{text"x1.0"}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML"Unsynchronized.reset show_question_marks"(*>*)
+(*<*)ML"show_question_marks := false"(*>*)
subsection {*Qualified names*}
@@ -415,7 +416,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -430,16 +431,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- @{thm [show_types] hd_Cons_tl}
+ @{thm hd_Cons_tl}
\end{center}
To print just the conclusion,
\begin{center}
- @{thm [show_types] (concl) hd_Cons_tl}
+ @{thm (concl) hd_Cons_tl}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 18:17:26 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Oct 29 18:53:58 2009 +0100
@@ -173,16 +173,17 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{verbatim}
-reset show_question_marks;
+show_question_marks := false;
\end{verbatim}
at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.
+The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Resetting \verb!show_question_marks! only suppresses question
-marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
-printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
-internal index. This can be avoided by turning the last digit into a
-subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
+suppresses question marks; variables that end in digits,
+e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}},
+e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
+turning the last digit into a subscript: write \verb!x\<^isub>1! and
+obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -537,7 +538,7 @@
\begin{quote}
\verb!\begin{center}!\\
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}!\\
+ \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
\verb!\end{tabular}!\\
\verb!\end{center}!
@@ -552,16 +553,16 @@
Likewise, \verb!concl! may be used as a style to show just the
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
\begin{center}
- \isa{{\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
To print just the conclusion,
\begin{center}
- \isa{hd\ {\isacharparenleft}xs\ {\isasymColon}\ {\isacharprime}a\ list{\isacharparenright}{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
+ \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
\end{center}
type
\begin{quote}
\verb!\begin{center}!\\
- \verb!@!\verb!{thm [show_types] (concl) hd_Cons_tl}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
\end{quote}
Beware that any options must be placed \emph{before}
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 18:17:26 2009 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Thu Oct 29 18:53:58 2009 +0100
@@ -33,7 +33,7 @@
\hyphenation{Isa-belle}
\begin{document}
-\title{\LaTeX\ Sugar for Isabelle documents}
+\title{\LaTeX\ Sugar for Isabelle Documents}
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
\maketitle
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 29 18:17:26 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Oct 29 18:53:58 2009 +0100
@@ -507,7 +507,7 @@
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
unfolding islimpt_approachable
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
- by metis (* FIXME: VERY slow! *)
+ by metis
class perfect_space =
(* FIXME: perfect_space should inherit from topological_space *)
@@ -746,7 +746,7 @@
{ fix x
have "x \<in> interior S \<longleftrightarrow> x \<in> UNIV - (closure (UNIV - S))"
unfolding interior_def closure_def islimpt_def
- by blast (* FIXME: VERY slow! *)
+ by auto
}
thus ?thesis
by blast
@@ -911,7 +911,7 @@
hence ?rhse using `?lhs`
unfolding frontier_closures closure_def islimpt_def
using open_ball[of a e] `e > 0`
- by (auto, erule_tac x = "ball a e" in allE, auto) (* FIXME: VERY slow! *)
+ by simp (metis centre_in_ball mem_ball open_ball)
}
ultimately have ?rhse by auto
}
@@ -1052,10 +1052,7 @@
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
unfolding eventually_within
-apply safe
-apply (rule_tac x="d/2" in exI, simp)
-apply (rule_tac x="d" in exI, simp)
-done
+by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl)
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
unfolding eventually_def trivial_limit_def
@@ -4404,28 +4401,20 @@
hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps) }
note * = this
{ fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
- have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
- apply auto (*FIXME: something horrible has happened here!*)
- apply atomize
- apply safe
- apply metis +
- done
- have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto }
+ have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
+ by simp (blast intro!: Sup_upper *) }
moreover
{ fix d::real assume "d>0" "d < diameter s"
hence "s\<noteq>{}" unfolding diameter_def by auto
- hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def
- apply auto (*FIXME: something horrible has happened here!*)
- apply atomize
- apply safe
- apply metis +
- done
have "\<exists>d' \<in> ?D. d' > d"
proof(rule ccontr)
assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
- hence as:"\<forall>d'\<in>?D. d' \<le> d" apply auto apply(erule_tac x="norm (x - y)" in allE) by auto
- hence "isUb UNIV ?D d" unfolding isUb_def unfolding setle_def by auto
- thus False using `d < diameter s` `s\<noteq>{}` isLub_le_isUb[OF lub, of d] unfolding diameter_def by auto
+ hence "\<forall>d'\<in>?D. d' \<le> d" by auto (metis not_leE)
+ thus False using `d < diameter s` `s\<noteq>{}`
+ apply (auto simp add: diameter_def)
+ apply (drule Sup_real_iff [THEN [2] rev_iffD2])
+ apply (auto, force)
+ done
qed
hence "\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d" by auto }
ultimately show "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
@@ -4445,7 +4434,8 @@
then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
hence "diameter s \<le> norm (x - y)"
by (force simp add: diameter_def intro!: Sup_least)
- thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
+ thus ?thesis
+ by (metis b diameter_bounded_bound order_antisym xys)
qed
text{* Related results with closure as the conclusion. *}
@@ -5291,7 +5281,7 @@
"s homeomorphic t \<longleftrightarrow> t homeomorphic s"
unfolding homeomorphic_def
unfolding homeomorphism_def
-by blast (* FIXME: slow *)
+by blast
lemma homeomorphic_trans:
assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
@@ -5459,7 +5449,7 @@
shows "complete(f ` s)"
proof-
{ fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
- then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" unfolding image_iff and Bex_def
+ then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)"
using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
hence x:"\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" by auto
hence "f \<circ> x = g" unfolding expand_fun_eq by auto