# HG changeset patch
# User kleing
# Date 1102054999 -3600
# Node ID e6f595009734204340aaaec2c9e40d2b8f5fc0d0
# Parent  611c32b7f6e5a158b6ff80dd60feccec3d45c081
more sugar

diff -r 611c32b7f6e5 -r e6f595009734 doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy
--- a/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Thu Dec 02 16:02:29 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/LaTeXsugar.thy	Fri Dec 03 07:23:19 2004 +0100
@@ -46,13 +46,8 @@
 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)"
-*)
+(* DUMMY *)
+consts DUMMY :: 'a ("\<^raw:\_>")
 
 (* THEOREMS *)
 syntax (Rule output)
diff -r 611c32b7f6e5 -r e6f595009734 doc-src/LaTeXsugar/Sugar/OptionalSugar.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/OptionalSugar.thy	Fri Dec 03 07:23:19 2004 +0100
@@ -0,0 +1,39 @@
+theory OptionalSugar
+imports LaTeXsugar
+begin
+
+(* append *)
+syntax (latex output)
+  "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
+translations
+  "appendL xs ys" <= "xs @ ys" 
+  "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
+
+
+(* and *)
+syntax (latex output)
+  "_andL" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<^raw:\isasymand>" 35)
+translations
+  "_andL A B" <= "A \<and> B" 
+  "_andL (_andL A B) C" <= "_andL A (_andL B C)"
+
+
+(* aligning equations *)
+syntax (tab output)
+  "op =" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50)
+  "==" :: "prop \<Rightarrow> prop \<Rightarrow> prop" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
+
+(* Let *)
+translations 
+  "_bind (p,DUMMY) e" <= "_bind p (fst e)"
+  "_bind (DUMMY,p) e" <= "_bind p (snd e)"
+
+  "_tuple_args x (_tuple_args y z)" ==
+    "_tuple_args x (_tuple_arg (_tuple y z))"
+
+  "_bind (Some p) e" <= "_bind p (the e)"
+  "_bind (p#DUMMY) e" <= "_bind p (hd e)"
+  "_bind (DUMMY#p) e" <= "_bind p (tl e)"
+
+
+end
\ No newline at end of file
diff -r 611c32b7f6e5 -r e6f595009734 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Dec 02 16:02:29 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Dec 03 07:23:19 2004 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Sugar
-imports LaTeXsugar
+imports LaTeXsugar OptionalSugar
 begin
 (*>*)
 
@@ -32,7 +32,8 @@
 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. You merely need to import theory
-\texttt{LaTeXsugar} in the header of your own theory. You may also
+\texttt{LaTeXsugar} in the header of your own theory and copy the bits of 
+\texttt{OptionalSugar} that you want to use. You may also
 need additional \LaTeX\ packages. These should be included
 at the beginning of your \LaTeX\ document, typically in \texttt{root.tex}.
 *}
@@ -77,11 +78,15 @@
 \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"}
+\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, \texttt{OptionalSugar} contains syntax to group
+@{text"@"}-terms 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"}
+
+\item The same can be done for @{text"\<and>"}:
+@{term[display]"term\<^isub>0 \<and> term\<^isub>1 \<and> term\<^isub>2 \<and> term\<^isub>3 \<and> term\<^isub>4 \<and> term\<^isub>5 \<and> term\<^isub>6 \<and> term\<^isub>7 \<and> term\<^isub>9 \<and> term\<^isub>1\<^isub>0 \<and> term\<^isub>1\<^isub>1"}
 
 \end{itemize}
 *}
@@ -161,7 +166,155 @@
 \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}
+*}
 
+subsection {*Definitions and Equations*}
+
+text {*
+  The \verb!thm! antiquotation works nicely for proper theorems, but
+  sets of equations as used in defintions are more difficult to
+  typeset nicely: for some reason people tend to prefer aligned 
+  @{text "="} signs.
+
+  Isabelle2005 will have a nice mechanism for that, namely the two
+  antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
+
+  \begin{center}
+  \begin{tabular}{l@ {~~@{text "="}~~}l}
+  @{lhs foldl_Nil[no_vars]} & @{rhs foldl_Nil[no_vars]}\\
+  @{lhs foldl_Cons[no_vars]} & @{rhs foldl_Cons[no_vars]}
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  is produced by the following code:
+
+\begin{quote}
+  \verb!\begin{center}!\\
+  \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
+  \verb!@!\verb!{lhs foldl_Nil[no_vars]} & @!\verb!{rhs foldl_Nil[no_vars]}!\\
+  \verb!@!\verb!{lhs foldl_Cons[no_vars]} & @!\verb!{rhs foldl_Cons[no_vars]}!\\
+  \verb!\end{tabular}!\\
+  \verb!\end{center}!
+\end{quote}
+
+  \noindent
+  Note the space between \verb!@! and \verb!{! in the tabular argument.
+  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
+  as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}! 
+  try to be smart about the interpretation of the theorem they
+  print, they work just as well for meta equality @{text "\<equiv>"} and other
+  binary operators like @{text "<"}.
+
+  Should you lack both the development version of Isabelle and a time
+  machine, you can still try to simulate the effect using the equation syntax
+  in \texttt{sugar.sty} and \texttt{OptionalSugar}.
+  
+  \begin{center}
+  \begin{tabular}{l@ { }l@ { }l}
+  \setcounter{isatabs}{0}%
+  @{thm [mode=tab] foldl_Nil[no_vars]}\nl
+  @{thm [mode=tab] foldl_Cons[no_vars]}
+  \end{tabular}
+  \end{center}
+
+  \noindent 
+  is produced by:
+
+\begin{quote}
+  \verb!\begin{center}!\\
+  \verb!\begin{tabular}{l@ { }l@ { }l}!\\
+  \verb!\setcounter{isatabs}{0}%!\\
+  \verb!@!\verb!{thm [mode=tab] foldl_Nil[no_vars]}\nl!\\
+  \verb!@!\verb!{thm [mode=tab] foldl_Cons[no_vars]}!\\
+  \verb!\end{tabular}!\\
+  \verb!\end{center}!
+\end{quote}
+
+  \noindent
+  These \LaTeX\ macros are not as flexible as the antiquotations
+  above, they only work for proper equations and definitions and they
+  only work correctly if the left hand side does not contain any
+  @{text "="} signs.
+*}
+
+subsection "Patterns"
+
+text {*
+  Sometimes functions ignore one or more of their
+  arguments and some functional languages have nice 
+  syntax for that as in @{thm hd.simps [where xs=DUMMY,no_vars]}.
+
+  You can simulate this in Isabelle by instantiating the @{term xs} in
+  definition \mbox{@{thm hd.simps[no_vars]}} with a constant @{text DUMMY} that
+  is printed as @{term DUMMY}. The code for the pattern above is 
+  \verb!@!\verb!{thm hd.simps [where xs=DUMMY,novars]}!.
+
+  You can drive this game even further and extend the syntax of let
+  bindings such that certain functions like @{term fst}, @{term hd}, 
+  etc.\ are printed nicely. \texttt{OptionalSugar} provides the
+  following pretty printing patterns:
+  
+  \begin{center}
+  \begin{tabular}{l@ {~~produced by~~}l}
+  @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
+  @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
+  @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
+  @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
+  @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
+  \end{tabular}
+  \end{center}
+*}
+
+subsection "Proofs"
+
+text {*
+  Full proofs, even if written in beatiful Isar style, are likely to
+  be too long and detailed to be included in conference papers, but
+  some key lemmas might be of interest.
+
+  It is usually easiest to put them in figures like the one in Fig.\
+  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
+  command:
+*}
+text_raw {*
+  \begin{figure}
+  \begin{center}\begin{minipage}{0.6\textwidth}  
+  \begin{isabellebody}
+*}
+lemma True
+proof -
+  -- "pretty trivial"
+  show True by force
+qed
+text_raw {*  
+  \end{isabellebody}
+  \end{minipage}\end{center}
+  \caption{Example proof in a figure.}\label{fig:proof}
+  \end{figure}
+*}
+text {*
+
+\begin{quote}
+\small
+\verb!text_raw {!\verb!*!\\
+\verb!  \begin{figure}!\\
+\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
+\verb!  \begin{isabellebody}!\\
+\verb!*!\verb!}!\\
+\verb!lemma True!\\
+\verb!proof -!\\
+\verb!  -- "pretty trivial"!\\
+\verb!  show True by force!\\
+\verb!qed!\\
+\verb!text_raw {!\verb!*!\\
+\verb!  \end{isabellebody}!\\
+\verb!  \end{minipage}\end{center}!\\
+\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
+\verb!  \end{figure}!\\
+\verb!*!\verb!}!
+\end{quote}
+  
 *}
 
 (*<*)
diff -r 611c32b7f6e5 -r e6f595009734 doc-src/LaTeXsugar/Sugar/document/root.tex
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Thu Dec 02 16:02:29 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Fri Dec 03 07:23:19 2004 +0100
@@ -22,6 +22,7 @@
 %\usepackage{textcomp}                 % for \<cent>, \<currency>
 
 \usepackage{mathpartir}
+\usepackage{sugar}
 
 % this should be the last package used
 \usepackage{pdfsetup}
diff -r 611c32b7f6e5 -r e6f595009734 doc-src/LaTeXsugar/Sugar/document/sugar.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/LaTeXsugar/Sugar/document/sugar.sty	Fri Dec 03 07:23:19 2004 +0100
@@ -0,0 +1,13 @@
+\usepackage{ifthen}
+
+% ------------------------------------------
+% for typesetting equations in tabular envs
+
+\newcounter{isatabs}
+\newcommand{\putisatab}{%
+\ifthenelse{\value{isatabs}<2}{&\addtocounter{isatabs}{1}}{}}
+\newcommand{\nl}{\\\setcounter{isatabs}{0}}
+
+\newcommand{\isactrltab}{\putisatab}
+
+% ------------------------------------------