# HG changeset patch # User nipkow # Date 1115883954 -7200 # Node ID 902b556e4bc06c4089780f7675fad28c2d0031ca # Parent ad9e27c1b2c80f697058310e3c4e0bd0a0188dc8 fixed a few things and added Haftmann as author diff -r ad9e27c1b2c8 -r 902b556e4bc0 doc-src/LaTeXsugar/Sugar/Sugar.thy --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed May 11 17:45:38 2005 +0200 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu May 12 09:45:54 2005 +0200 @@ -275,7 +275,7 @@ subsection "Styles" text {* - The \verb!thm! antiquotation works nicely for proper theorems, but + The \verb!thm! antiquotation works nicely for single theorems, but sets of equations as used in definitions are more difficult to typeset nicely: for some reason people tend to prefer aligned @{text "="} signs. @@ -289,20 +289,16 @@ \verb!@!\verb!{term_style stylename term}! \end{quote} - A ``style'' is a transformation of terms; there are three predefined - styles, named \verb!lhs!, \verb!rhs! and \verb!concl!, which obvious - meanings, e.~g.~the output - + A ``style'' is a transformation of terms. There are three predefined + styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious + meanings. For example, the output \begin{center} \begin{tabular}{l@ {~~@{text "="}~~}l} @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\ @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons} \end{tabular} \end{center} - - \noindent is produced by the following code: - \begin{quote} \verb!\begin{center}!\\ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ @@ -311,39 +307,31 @@ \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. Both styles \verb!lhs! and \verb!rhs! + as an antiquotation. Both styles \verb!lhs! and \verb!rhs! try to be smart about the interpretation of the theorem they transform they work just as well for meta equality @{text "\"} and other binary operators like @{text "<"}. Likewise \verb!conclusion! may be used as style to show just the conclusion of a formula: - \begin{center} @{thm_style conclusion hd_Cons_tl} \end{center} - - \noindent is produced by - \begin{quote} \verb!\begin{center}!\\ \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ \verb!\end{center}! \end{quote} - If you aren't afraid about ML, you may also define your own styles; - a style is simply implemented by a ML function \verb!Term.term -> Term.term!. + If you are not afraid of ML, you may also define your own styles. + A style is simply implemented by an ML function of type \verb!term -> term!. Have a look at the following example (which indeed shows just the way the \verb!lhs! style is implemented): - \begin{quote} \verb!setup {!\verb!*!\\ - \verb!!\\ \verb!let!\\ \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ @@ -352,18 +340,18 @@ \verb! | my_lhs _ = error ("Binary operator expected")!\\ \verb! in [Style.put_style "new_lhs" my_lhs]!\\ \verb!end;!\\ - \verb!!\\ \verb!*!\verb!}!\\ \end{quote} - + This code must go into your theory file, not as part of your + \LaTeX\ text but as a separate command in front of it. Like in this example, it is recommended to put the definition of the style function into a \verb!let! expression, in order not to pollute the ML global namespace. The mapping from identifier name to the style function is done by the \verb!Style.put_style! expression which expects the desired style name and the style function as arguments. After this \verb!setup!, - there will be a new style available named \verb!new_lhs!, then allowing - antiquoations like \verb!@!\verb!{term_style new_lhs rev_map}! - yielding \verb!rev (map f xs)!. + there will be a new style available named \verb!new_lhs! allowing + antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! + yielding @{thm_style lhs rev_map}. The example above may be used as as a ``copy-and-paste'' pattern to write your own styles; for a description of the constructs used, please refer diff -r ad9e27c1b2c8 -r 902b556e4bc0 doc-src/LaTeXsugar/Sugar/document/Sugar.tex --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Wed May 11 17:45:38 2005 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu May 12 09:45:54 2005 +0200 @@ -226,48 +226,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsubsection{Definitions and Equations% -} -\isamarkuptrue% -% -\begin{isamarkuptext}% -The \verb!thm! antiquotation works nicely for proper theorems, but - sets of equations as used in definitions are more difficult to - typeset nicely: for some reason people tend to prefer aligned - \isa{{\isacharequal}} signs. - - Isabelle2005 has a nice mechanism for this, namely the two - antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!. - - \begin{center} - \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l} - \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\ - \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs} - \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} & @!\verb!{rhs foldl_Nil}!\\ - \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\ - \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 \isa{{\isasymequiv}} and other - binary operators like \isa{{\isacharless}}.% -\end{isamarkuptext}% -\isamarkuptrue% -% \isamarkupsubsection{Patterns% } \isamarkuptrue% @@ -355,6 +313,95 @@ \end{quote}% \end{isamarkuptext}% \isamarkuptrue% +% +\isamarkupsubsection{Styles% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \verb!thm! antiquotation works nicely for single theorems, but + sets of equations as used in definitions are more difficult to + typeset nicely: for some reason people tend to prefer aligned + \isa{{\isacharequal}} signs. + + To deal with such cases where it is desirable to dive into the structure + of terms and theorems, Isabelle offers two antiquotations featuring + ``styles'': + + \begin{quote} + \verb!@!\verb!{thm_style stylename thm}!\\ + \verb!@!\verb!{term_style stylename term}! + \end{quote} + + A ``style'' is a transformation of terms. There are three predefined + styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious + meanings. For example, the output + \begin{center} + \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l} + \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\ + \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs} + \end{tabular} + \end{center} + is produced by the following code: + \begin{quote} + \verb!\begin{center}!\\ + \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ + \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\ + \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\ + \verb!\end{tabular}!\\ + \verb!\end{center}! + \end{quote} + Note the space between \verb!@! and \verb!{! in the tabular argument. + It prevents Isabelle from interpreting \verb!@ {~~...~~}! + as an antiquotation. Both styles \verb!lhs! and \verb!rhs! + try to be smart about the interpretation of the theorem they transform + they work just as well for meta equality \isa{{\isasymequiv}} and other + binary operators like \isa{{\isacharless}}. + + Likewise \verb!conclusion! may be used as style to show just the conclusion + of a formula: + \begin{center} + \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} + \end{center} + is produced by + \begin{quote} + \verb!\begin{center}!\\ + \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ + \verb!\end{center}! + \end{quote} + + If you are not afraid of ML, you may also define your own styles. + A style is simply implemented by an ML function of type \verb!term -> term!. + Have a look at the following example (which indeed shows just the way the + \verb!lhs! style is implemented): + \begin{quote} + \verb!setup {!\verb!*!\\ + \verb!let!\\ + \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ + \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ + \verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ + \verb! | my_lhs (_ $ t $ _) = t!\\ + \verb! | my_lhs _ = error ("Binary operator expected")!\\ + \verb! in [Style.put_style "new_lhs" my_lhs]!\\ + \verb!end;!\\ + \verb!*!\verb!}!\\ + \end{quote} + This code must go into your theory file, not as part of your + \LaTeX\ text but as a separate command in front of it. + Like in this example, it is recommended to put the definition of the style + function into a \verb!let! expression, in order not to pollute the + ML global namespace. The mapping from identifier name to the style function + is done by the \verb!Style.put_style! expression which expects the desired + style name and the style function as arguments. After this \verb!setup!, + there will be a new style available named \verb!new_lhs! allowing + antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! + yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}. + + The example above may be used as as a ``copy-and-paste'' pattern to write + your own styles; for a description of the constructs used, please refer + to the Isabelle reference manual.% +\end{isamarkuptext}% +\isamarkuptrue% \isamarkupfalse% \end{isabellebody}% %%% Local Variables: diff -r ad9e27c1b2c8 -r 902b556e4bc0 doc-src/LaTeXsugar/Sugar/document/root.tex --- a/doc-src/LaTeXsugar/Sugar/document/root.tex Wed May 11 17:45:38 2005 +0200 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Thu May 12 09:45:54 2005 +0200 @@ -34,7 +34,7 @@ \begin{document} \title{\LaTeX\ Sugar for Isabelle documents} -\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer} +\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer} \maketitle \begin{abstract}