# HG changeset patch
# User nipkow
# Date 1101750575 -3600
# Node ID 13bd3d12ec2fdda0636343dcb068fedf7977e6e7
# Parent  254f6f00b60e4f2ed98d5eb6fecd269f71fd7f4c
*** empty log message ***

diff -r 254f6f00b60e -r 13bd3d12ec2f doc-src/LaTeXsugar/IsaMakefile
--- a/doc-src/LaTeXsugar/IsaMakefile	Mon Nov 29 14:02:55 2004 +0100
+++ b/doc-src/LaTeXsugar/IsaMakefile	Mon Nov 29 18:49:35 2004 +0100
@@ -21,7 +21,7 @@
 
 Sugar: $(LOG)/HOL-Sugar.gz
 
-$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/*.thy
+$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/document/root.bib Sugar/*.thy
 	@$(USEDIR) HOL Sugar
 
 
diff -r 254f6f00b60e -r 13bd3d12ec2f doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Mon Nov 29 18:49:35 2004 +0100
@@ -0,0 +1,86 @@
+theory LaTeXsugar
+imports Main
+begin
+
+(* LOGIC *)
+syntax (latex output)
+  If            :: "[bool, 'a, 'a] => 'a"
+  ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10)
+
+  "_Let"        :: "[letbinds, 'a] => 'a"
+  ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10)
+
+  "_case_syntax":: "['a, cases_syn] => 'b"
+  ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
+
+(* SETS *)
+
+(* empty set *)
+syntax (latex output)
+  "_emptyset" :: "'a set"              ("\<emptyset>")
+translations
+  "_emptyset"      <= "{}"
+
+(* insert *)
+translations 
+  "{x} \<union> A" <= "insert x A"
+  "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
+
+(* set comprehension *)
+syntax (latex output)
+  "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
+translations
+  "_Collect p P"      <= "{p. P}"
+
+(* LISTS *)
+
+(* Cons *)
+syntax (latex)
+  Cons :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_\<cdot>/_" [66,65] 65)
+
+(* length *)
+syntax (latex output)
+  length :: "'a list \<Rightarrow> nat" ("|_|")
+
+(* nth *)
+syntax (latex output)
+  nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" ("_\<^raw:$_{[\mathit{>_\<^raw:}]}$>" [1000,0] 1000)
+
+(* append
+syntax (latex output)
+  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ \<^raw:\isacharat>/ _" [65,66] 65)
+translations
+  "appendL xs ys" <= "xs @ ys" 
+  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+*)
+
+(* THEOREMS *)
+syntax (Rule output)
+  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("_\<^raw:\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+syntax (IfThen output)
+  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+syntax (IfThenNoBox output)
+  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+end
\ No newline at end of file
diff -r 254f6f00b60e -r 13bd3d12ec2f doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Nov 29 14:02:55 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Nov 29 18:49:35 2004 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Sugar
-imports Main
+imports LaTeXsugar
 begin
 (*>*)
 
@@ -12,9 +12,9 @@
 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
 and seeing Isabelle typeset it for them:
 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
-No typos, no omissions, no sweat!
-If you have not experienced that joy, read chapter 4, \emph{Presenting
-Theories}, of \cite{LNCS2283} first.
+No typos, no omissions, no sweat.
+If you have not experienced that joy, read Chapter 4, \emph{Presenting
+Theories}, \cite{LNCS2283} first.
 
 If you have mastered the art of Isabelle's \emph{antiquotations},
 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
@@ -26,59 +26,91 @@
 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin
-that must be punished by immediate rejection.
+that must be punished by instant rejection.
 
 
 This document shows you how to make Isabelle and \LaTeX\ cooperate to
 produce ordinary looking mathematics that hides the fact that it was
-typeset by a machine. This involves additional syntax-related
-declarations for your theory file and corresponding \LaTeX\ macros. We
-explain how to use them but show neither. They can be downloaded from
-the web.
+typeset by a machine. You merely need to import theory
+\texttt{LaTeXsugar} in the header of your own theory. You may also
+need additional \LaTeX\ packages. These should be included
+at the beginning of your \LaTeX\ document, typically in \texttt{root.tex}.
+*}
+
+section{* HOL syntax*}
+
+subsection{* Logic *}
+
+text{* The predefined constructs @{text"if"}, @{text"let"} and
+@{text"case"} are set in sans serif font to distinguish them from
+other functions. This improves readability:
+\begin{itemize}
+\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"}.
+\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
+\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
+      @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
+\end{itemize}
+*}
+
+subsection{* Sets *}
 
+text{* Although set syntax in HOL is already close to
+standard, we provide a few further improvements:
+\begin{itemize}
+\item @{term"{x. P}"} instead of @{text"{x. P}"}.
+\item @{term"{}"} instead of @{text"{}"}.
+\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
+\end{itemize}
+*}
+
+subsection{* Lists *}
+
+text{* If lists are used heavily, the following notations increase readability:
+\begin{itemize}
+\item @{term"x # xs"} instead of @{text"x # xs"}.
+      Exceptionally, @{term"x # xs"} is also input syntax.
+If you prefer more space around the $\cdot$ you have to redefine
+\verb!\isasymcdot! in \LaTeX:
+\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
+
+\item @{term"length xs"} instead of @{text"length xs"}.
+\item @{term"nth xs n"} instead of @{text"nth xs i"},
+      the $n$th element of @{text xs}.
+
+%\item The @ {text"@"} operation associates implicitly to the right,
+%which leads to unpleasant line breaks if the term is too long for one
+%line. To avoid this, @ {text"@"}-terms are grouped to the left before
+%printing, which leads to better line breaking behaviour:
+%@ {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"}
+
+\end{itemize}
 *}
 
 section "Printing theorems"
 
 subsection "Inference rules"
 
-(*<*)
-syntax (Rule output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
-
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
-
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("_\<^raw:\\>/ _")
-
-  "_asm" :: "prop \<Rightarrow> asms" ("_")
-(*>*)
-
-text{* To print theorems as inference rules you need to include the
-\texttt{Rule} output syntax declarations in your theory and Didier
-Remy's \texttt{mathpartir} package for typesetting inference rules in
-your \LaTeX\ file.
+text{* To print theorems as inference rules you need to include Didier
+R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
+for typesetting inference rules in your \LaTeX\ file.
 
 Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
 @{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
-The standard \texttt{display} attribute, i.e.\ writing
-\verb![mode=Rule,display]! instead of \verb![mode=Rule]!,
-displays the rule on a separate line using a smaller font:
-@{thm[mode=Rule,display] conjI[no_vars]}
-Centering a display does not work directly. Instead you can enclose the
-non-displayed variant in a \texttt{center} environment:
-
+If you prefer your inference rule on a separate line, maybe with a name,
+\begin{center}
+@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
+\end{center}
+is produced by
 \begin{quote}
 \verb!\begin{center}!\\
 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
 \verb!\end{center}!
 \end{quote}
-also adds a label to the rule and yields
-\begin{center}
-@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
-\end{center}
+It is not recommended to use the standard \texttt{display} attribute
+together with \texttt{Rule} because centering does not work and because
+the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
+clash.
+
 Of course you can display multiple rules in this fashion:
 \begin{quote}
 \verb!\begin{center}\isastyle!\\
@@ -96,7 +128,42 @@
 Note that we included \verb!\isastyle! to obtain
 the smaller font that otherwise comes only with \texttt{display}.
 
+The \texttt{mathpartir} package copes well if there are too many
+premises for one line:
+\begin{center}
+@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
+ G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
+\end{center}
+
+Limitations: premises and conclusion must each not be longer than the line.
 *}
+
+subsection{*If-then*}
+
+text{* If you prefer a fake ``natural language'' style you can produce
+the body of
+\newtheorem{theorem}{Theorem}
+\begin{theorem}
+@{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]}
+\end{theorem}
+by typing
+\begin{quote}
+\verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}!
+\end{quote}
+
+In order to prevent odd line breaks, the premises are put into boxes.
+At times this is too drastic:
+\begin{theorem}
+@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+In which case you should use \texttt{mode=IfThenNoBox} instead of
+\texttt{mode=IfThen}:
+\begin{theorem}
+@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
+\end{theorem}
+
+*}
+
 (*<*)
 end
 (*>*)
\ No newline at end of file
diff -r 254f6f00b60e -r 13bd3d12ec2f doc-src/LaTeXsugar/Sugar/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/root.bib	Mon Nov 29 18:49:35 2004 +0100
@@ -0,0 +1,7 @@
+@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
+title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
+publisher=Springer,series=LNCS,volume=2283,year=2002,
+note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
+
+@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
+note={\url{http://cristal.inria.fr/~remy/latex/}}}
\ No newline at end of file
diff -r 254f6f00b60e -r 13bd3d12ec2f doc-src/LaTeXsugar/Sugar/document/root.tex
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Mon Nov 29 14:02:55 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Mon Nov 29 18:49:35 2004 +0100
@@ -30,11 +30,11 @@
 \urlstyle{rm}
 \isabellestyle{it}
 
-
+\hyphenation{Isa-belle}
 \begin{document}
 
-\title{\LaTeX\ Sugar for Isabelle/HOL}
-\author{Tobias Nipkow, Norbert Schirmer}
+\title{\LaTeX\ Sugar for Isabelle documents}
+\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
 \maketitle
 
 \begin{abstract}
@@ -45,11 +45,11 @@
 \tableofcontents
 
 % generated text of all theories
-\input{session}
+\input{Sugar.tex}
 
 % optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{abbrv}
+\bibliography{root}
 
 \end{document}