1.1 --- a/doc-src/LaTeXsugar/IsaMakefile Mon Nov 29 14:02:55 2004 +0100
1.2 +++ b/doc-src/LaTeXsugar/IsaMakefile Mon Nov 29 18:49:35 2004 +0100
1.3 @@ -21,7 +21,7 @@
1.4
1.5 Sugar: $(LOG)/HOL-Sugar.gz
1.6
1.7 -$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/*.thy
1.8 +$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/document/root.bib Sugar/*.thy
1.9 @$(USEDIR) HOL Sugar
1.10
1.11
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy Mon Nov 29 18:49:35 2004 +0100
2.3 @@ -0,0 +1,86 @@
2.4 +theory LaTeXsugar
2.5 +imports Main
2.6 +begin
2.7 +
2.8 +(* LOGIC *)
2.9 +syntax (latex output)
2.10 + If :: "[bool, 'a, 'a] => 'a"
2.11 + ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
2.12 +
2.13 + "_Let" :: "[letbinds, 'a] => 'a"
2.14 + ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
2.15 +
2.16 + "_case_syntax":: "['a, cases_syn] => 'b"
2.17 + ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
2.18 +
2.19 +(* SETS *)
2.20 +
2.21 +(* empty set *)
2.22 +syntax (latex output)
2.23 + "_emptyset" :: "'a set" ("\<emptyset>")
2.24 +translations
2.25 + "_emptyset" <= "{}"
2.26 +
2.27 +(* insert *)
2.28 +translations
2.29 + "{x} \<union> A" <= "insert x A"
2.30 + "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
2.31 +
2.32 +(* set comprehension *)
2.33 +syntax (latex output)
2.34 + "_Collect" :: "pttrn => bool => 'a set" ("(1{_ | _})")
2.35 +translations
2.36 + "_Collect p P" <= "{p. P}"
2.37 +
2.38 +(* LISTS *)
2.39 +
2.40 +(* Cons *)
2.41 +syntax (latex)
2.42 + Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
2.43 +
2.44 +(* length *)
2.45 +syntax (latex output)
2.46 + length :: "'a list \<Rightarrow> nat" ("|_|")
2.47 +
2.48 +(* nth *)
2.49 +syntax (latex output)
2.50 + nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:$_{[\mathit{>_\<^raw:}]}$>" [1000,0] 1000)
2.51 +
2.52 +(* append
2.53 +syntax (latex output)
2.54 + "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ \<^raw:\isacharat>/ _" [65,66] 65)
2.55 +translations
2.56 + "appendL xs ys" <= "xs @ ys"
2.57 + "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
2.58 +*)
2.59 +
2.60 +(* THEOREMS *)
2.61 +syntax (Rule output)
2.62 + "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
2.63 + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
2.64 +
2.65 + "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
2.66 + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
2.67 +
2.68 + "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
2.69 + ("_\<^raw:\\>/ _")
2.70 +
2.71 + "_asm" :: "prop \<Rightarrow> asms" ("_")
2.72 +
2.73 +syntax (IfThen output)
2.74 + "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
2.75 + ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
2.76 + "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
2.77 + ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
2.78 + "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
2.79 + "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
2.80 +
2.81 +syntax (IfThenNoBox output)
2.82 + "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
2.83 + ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
2.84 + "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
2.85 + ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
2.86 + "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
2.87 + "_asm" :: "prop \<Rightarrow> asms" ("_")
2.88 +
2.89 +end
2.90 \ No newline at end of file
3.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Nov 29 14:02:55 2004 +0100
3.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Nov 29 18:49:35 2004 +0100
3.3 @@ -1,6 +1,6 @@
3.4 (*<*)
3.5 theory Sugar
3.6 -imports Main
3.7 +imports LaTeXsugar
3.8 begin
3.9 (*>*)
3.10
3.11 @@ -12,9 +12,9 @@
3.12 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
3.13 and seeing Isabelle typeset it for them:
3.14 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
3.15 -No typos, no omissions, no sweat!
3.16 -If you have not experienced that joy, read chapter 4, \emph{Presenting
3.17 -Theories}, of \cite{LNCS2283} first.
3.18 +No typos, no omissions, no sweat.
3.19 +If you have not experienced that joy, read Chapter 4, \emph{Presenting
3.20 +Theories}, \cite{LNCS2283} first.
3.21
3.22 If you have mastered the art of Isabelle's \emph{antiquotations},
3.23 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
3.24 @@ -26,59 +26,91 @@
3.25 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
3.26 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
3.27 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin
3.28 -that must be punished by immediate rejection.
3.29 +that must be punished by instant rejection.
3.30
3.31
3.32 This document shows you how to make Isabelle and \LaTeX\ cooperate to
3.33 produce ordinary looking mathematics that hides the fact that it was
3.34 -typeset by a machine. This involves additional syntax-related
3.35 -declarations for your theory file and corresponding \LaTeX\ macros. We
3.36 -explain how to use them but show neither. They can be downloaded from
3.37 -the web.
3.38 +typeset by a machine. You merely need to import theory
3.39 +\texttt{LaTeXsugar} in the header of your own theory. You may also
3.40 +need additional \LaTeX\ packages. These should be included
3.41 +at the beginning of your \LaTeX\ document, typically in \texttt{root.tex}.
3.42 +*}
3.43
3.44 +section{* HOL syntax*}
3.45 +
3.46 +subsection{* Logic *}
3.47 +
3.48 +text{* The predefined constructs @{text"if"}, @{text"let"} and
3.49 +@{text"case"} are set in sans serif font to distinguish them from
3.50 +other functions. This improves readability:
3.51 +\begin{itemize}
3.52 +\item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
3.53 +\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
3.54 +\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
3.55 + @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
3.56 +\end{itemize}
3.57 +*}
3.58 +
3.59 +subsection{* Sets *}
3.60 +
3.61 +text{* Although set syntax in HOL is already close to
3.62 +standard, we provide a few further improvements:
3.63 +\begin{itemize}
3.64 +\item @{term"{x. P}"} instead of @{text"{x. P}"}.
3.65 +\item @{term"{}"} instead of @{text"{}"}.
3.66 +\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
3.67 +\end{itemize}
3.68 +*}
3.69 +
3.70 +subsection{* Lists *}
3.71 +
3.72 +text{* If lists are used heavily, the following notations increase readability:
3.73 +\begin{itemize}
3.74 +\item @{term"x # xs"} instead of @{text"x # xs"}.
3.75 + Exceptionally, @{term"x # xs"} is also input syntax.
3.76 +If you prefer more space around the $\cdot$ you have to redefine
3.77 +\verb!\isasymcdot! in \LaTeX:
3.78 +\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
3.79 +
3.80 +\item @{term"length xs"} instead of @{text"length xs"}.
3.81 +\item @{term"nth xs n"} instead of @{text"nth xs i"},
3.82 + the $n$th element of @{text xs}.
3.83 +
3.84 +%\item The @ {text"@"} operation associates implicitly to the right,
3.85 +%which leads to unpleasant line breaks if the term is too long for one
3.86 +%line. To avoid this, @ {text"@"}-terms are grouped to the left before
3.87 +%printing, which leads to better line breaking behaviour:
3.88 +%@ {term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
3.89 +
3.90 +\end{itemize}
3.91 *}
3.92
3.93 section "Printing theorems"
3.94
3.95 subsection "Inference rules"
3.96
3.97 -(*<*)
3.98 -syntax (Rule output)
3.99 - "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
3.100 - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
3.101 -
3.102 - "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
3.103 - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
3.104 -
3.105 - "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
3.106 - ("_\<^raw:\\>/ _")
3.107 -
3.108 - "_asm" :: "prop \<Rightarrow> asms" ("_")
3.109 -(*>*)
3.110 -
3.111 -text{* To print theorems as inference rules you need to include the
3.112 -\texttt{Rule} output syntax declarations in your theory and Didier
3.113 -Remy's \texttt{mathpartir} package for typesetting inference rules in
3.114 -your \LaTeX\ file.
3.115 +text{* To print theorems as inference rules you need to include Didier
3.116 +R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
3.117 +for typesetting inference rules in your \LaTeX\ file.
3.118
3.119 Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
3.120 @{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
3.121 -The standard \texttt{display} attribute, i.e.\ writing
3.122 -\verb![mode=Rule,display]! instead of \verb![mode=Rule]!,
3.123 -displays the rule on a separate line using a smaller font:
3.124 -@{thm[mode=Rule,display] conjI[no_vars]}
3.125 -Centering a display does not work directly. Instead you can enclose the
3.126 -non-displayed variant in a \texttt{center} environment:
3.127 -
3.128 +If you prefer your inference rule on a separate line, maybe with a name,
3.129 +\begin{center}
3.130 +@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
3.131 +\end{center}
3.132 +is produced by
3.133 \begin{quote}
3.134 \verb!\begin{center}!\\
3.135 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
3.136 \verb!\end{center}!
3.137 \end{quote}
3.138 -also adds a label to the rule and yields
3.139 -\begin{center}
3.140 -@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
3.141 -\end{center}
3.142 +It is not recommended to use the standard \texttt{display} attribute
3.143 +together with \texttt{Rule} because centering does not work and because
3.144 +the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
3.145 +clash.
3.146 +
3.147 Of course you can display multiple rules in this fashion:
3.148 \begin{quote}
3.149 \verb!\begin{center}\isastyle!\\
3.150 @@ -96,7 +128,42 @@
3.151 Note that we included \verb!\isastyle! to obtain
3.152 the smaller font that otherwise comes only with \texttt{display}.
3.153
3.154 +The \texttt{mathpartir} package copes well if there are too many
3.155 +premises for one line:
3.156 +\begin{center}
3.157 +@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
3.158 + G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
3.159 +\end{center}
3.160 +
3.161 +Limitations: premises and conclusion must each not be longer than the line.
3.162 *}
3.163 +
3.164 +subsection{*If-then*}
3.165 +
3.166 +text{* If you prefer a fake ``natural language'' style you can produce
3.167 +the body of
3.168 +\newtheorem{theorem}{Theorem}
3.169 +\begin{theorem}
3.170 +@{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]}
3.171 +\end{theorem}
3.172 +by typing
3.173 +\begin{quote}
3.174 +\verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}!
3.175 +\end{quote}
3.176 +
3.177 +In order to prevent odd line breaks, the premises are put into boxes.
3.178 +At times this is too drastic:
3.179 +\begin{theorem}
3.180 +@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
3.181 +\end{theorem}
3.182 +In which case you should use \texttt{mode=IfThenNoBox} instead of
3.183 +\texttt{mode=IfThen}:
3.184 +\begin{theorem}
3.185 +@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
3.186 +\end{theorem}
3.187 +
3.188 +*}
3.189 +
3.190 (*<*)
3.191 end
3.192 (*>*)
3.193 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.bib Mon Nov 29 18:49:35 2004 +0100
4.3 @@ -0,0 +1,7 @@
4.4 +@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
4.5 +title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
4.6 +publisher=Springer,series=LNCS,volume=2283,year=2002,
4.7 +note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
4.8 +
4.9 +@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
4.10 +note={\url{http://cristal.inria.fr/~remy/latex/}}}
4.11 \ No newline at end of file
5.1 --- a/doc-src/LaTeXsugar/Sugar/document/root.tex Mon Nov 29 14:02:55 2004 +0100
5.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Mon Nov 29 18:49:35 2004 +0100
5.3 @@ -30,11 +30,11 @@
5.4 \urlstyle{rm}
5.5 \isabellestyle{it}
5.6
5.7 -
5.8 +\hyphenation{Isa-belle}
5.9 \begin{document}
5.10
5.11 -\title{\LaTeX\ Sugar for Isabelle/HOL}
5.12 -\author{Tobias Nipkow, Norbert Schirmer}
5.13 +\title{\LaTeX\ Sugar for Isabelle documents}
5.14 +\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
5.15 \maketitle
5.16
5.17 \begin{abstract}
5.18 @@ -45,11 +45,11 @@
5.19 \tableofcontents
5.20
5.21 % generated text of all theories
5.22 -\input{session}
5.23 +\input{Sugar.tex}
5.24
5.25 % optional bibliography
5.26 -%\bibliographystyle{abbrv}
5.27 -%\bibliography{root}
5.28 +\bibliographystyle{abbrv}
5.29 +\bibliography{root}
5.30
5.31 \end{document}
5.32