fixed a few things and added Haftmann as author
authornipkow
Thu May 12 09:45:54 2005 +0200 (2005-05-12)
changeset 15953902b556e4bc0
parent 15952 ad9e27c1b2c8
child 15954 dd516176043a
fixed a few things and added Haftmann as author
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
doc-src/LaTeXsugar/Sugar/document/root.tex
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed May 11 17:45:38 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu May 12 09:45:54 2005 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4  subsection "Styles"
     1.5  
     1.6  text {*
     1.7 -  The \verb!thm! antiquotation works nicely for proper theorems, but
     1.8 +  The \verb!thm! antiquotation works nicely for single theorems, but
     1.9    sets of equations as used in definitions are more difficult to
    1.10    typeset nicely: for some reason people tend to prefer aligned 
    1.11    @{text "="} signs.
    1.12 @@ -289,20 +289,16 @@
    1.13      \verb!@!\verb!{term_style stylename term}!
    1.14      \end{quote}
    1.15  
    1.16 -  A ``style'' is a transformation of terms; there are three predefined
    1.17 -  styles, named \verb!lhs!, \verb!rhs! and \verb!concl!, which obvious
    1.18 -  meanings, e.~g.~the output
    1.19 -
    1.20 +  A ``style'' is a transformation of terms. There are three predefined
    1.21 +  styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious
    1.22 +  meanings. For example, the output
    1.23    \begin{center}
    1.24    \begin{tabular}{l@ {~~@{text "="}~~}l}
    1.25    @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
    1.26    @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
    1.27    \end{tabular}
    1.28    \end{center}
    1.29 -
    1.30 -  \noindent 
    1.31    is produced by the following code:
    1.32 -
    1.33    \begin{quote}
    1.34      \verb!\begin{center}!\\
    1.35      \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
    1.36 @@ -311,39 +307,31 @@
    1.37      \verb!\end{tabular}!\\
    1.38      \verb!\end{center}!
    1.39    \end{quote}
    1.40 -
    1.41 -  \noindent
    1.42    Note the space between \verb!@! and \verb!{! in the tabular argument.
    1.43    It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
    1.44 -  as antiquotation. Both styles \verb!lhs! and \verb!rhs! 
    1.45 +  as an antiquotation. Both styles \verb!lhs! and \verb!rhs! 
    1.46    try to be smart about the interpretation of the theorem they transform
    1.47    they work just as well for meta equality @{text "\<equiv>"} and other
    1.48    binary operators like @{text "<"}.
    1.49  
    1.50    Likewise \verb!conclusion! may be used as style to show just the conclusion
    1.51    of a formula:
    1.52 -
    1.53    \begin{center}
    1.54      @{thm_style conclusion hd_Cons_tl}
    1.55    \end{center}
    1.56 -
    1.57 -  \noindent 
    1.58    is produced by
    1.59 -
    1.60    \begin{quote}
    1.61      \verb!\begin{center}!\\
    1.62      \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
    1.63      \verb!\end{center}!
    1.64    \end{quote}
    1.65  
    1.66 -  If you aren't afraid about ML, you may also define your own styles;
    1.67 -  a style is simply implemented by a ML function \verb!Term.term -> Term.term!.
    1.68 +  If you are not afraid of ML, you may also define your own styles.
    1.69 +  A style is simply implemented by an ML function of type \verb!term -> term!.
    1.70    Have a look at the following example (which indeed shows just the way the
    1.71    \verb!lhs! style is implemented):
    1.72 -
    1.73    \begin{quote}
    1.74      \verb!setup {!\verb!*!\\
    1.75 -    \verb!!\\
    1.76      \verb!let!\\
    1.77      \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
    1.78      \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
    1.79 @@ -352,18 +340,18 @@
    1.80      \verb!    | my_lhs _ = error ("Binary operator expected")!\\
    1.81      \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
    1.82      \verb!end;!\\
    1.83 -    \verb!!\\
    1.84      \verb!*!\verb!}!\\
    1.85    \end{quote}
    1.86 -
    1.87 +  This code must go into your theory file, not as part of your
    1.88 +  \LaTeX\ text but as a separate command in front of it.
    1.89    Like in this example, it is recommended to put the definition of the style
    1.90    function into a \verb!let! expression, in order not to pollute the
    1.91    ML global namespace. The mapping from identifier name to the style function
    1.92    is done by the \verb!Style.put_style! expression which expects the desired
    1.93    style name and the style function as arguments. After this \verb!setup!,
    1.94 -  there will be a new style available named \verb!new_lhs!, then allowing
    1.95 -  antiquoations like \verb!@!\verb!{term_style new_lhs rev_map}!
    1.96 -  yielding \verb!rev (map f xs)!.
    1.97 +  there will be a new style available named \verb!new_lhs! allowing
    1.98 +  antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
    1.99 +  yielding @{thm_style lhs rev_map}.
   1.100  
   1.101    The example above may be used as as a ``copy-and-paste'' pattern to write
   1.102    your own styles; for a description of the constructs used, please refer
     2.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed May 11 17:45:38 2005 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu May 12 09:45:54 2005 +0200
     2.3 @@ -226,48 +226,6 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsubsection{Definitions and Equations%
     2.8 -}
     2.9 -\isamarkuptrue%
    2.10 -%
    2.11 -\begin{isamarkuptext}%
    2.12 -The \verb!thm! antiquotation works nicely for proper theorems, but
    2.13 -  sets of equations as used in definitions are more difficult to
    2.14 -  typeset nicely: for some reason people tend to prefer aligned 
    2.15 -  \isa{{\isacharequal}} signs.
    2.16 -
    2.17 -  Isabelle2005 has a nice mechanism for this, namely the two
    2.18 -  antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
    2.19 -
    2.20 -  \begin{center}
    2.21 -  \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
    2.22 -  \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
    2.23 -  \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs}
    2.24 -  \end{tabular}
    2.25 -  \end{center}
    2.26 -
    2.27 -  \noindent 
    2.28 -  is produced by the following code:
    2.29 -
    2.30 -\begin{quote}
    2.31 -  \verb!\begin{center}!\\
    2.32 -  \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
    2.33 -  \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\
    2.34 -  \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\
    2.35 -  \verb!\end{tabular}!\\
    2.36 -  \verb!\end{center}!
    2.37 -\end{quote}
    2.38 -
    2.39 -  \noindent
    2.40 -  Note the space between \verb!@! and \verb!{! in the tabular argument.
    2.41 -  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
    2.42 -  as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}! 
    2.43 -  try to be smart about the interpretation of the theorem they
    2.44 -  print, they work just as well for meta equality \isa{{\isasymequiv}} and other
    2.45 -  binary operators like \isa{{\isacharless}}.%
    2.46 -\end{isamarkuptext}%
    2.47 -\isamarkuptrue%
    2.48 -%
    2.49  \isamarkupsubsection{Patterns%
    2.50  }
    2.51  \isamarkuptrue%
    2.52 @@ -355,6 +313,95 @@
    2.53  \end{quote}%
    2.54  \end{isamarkuptext}%
    2.55  \isamarkuptrue%
    2.56 +%
    2.57 +\isamarkupsubsection{Styles%
    2.58 +}
    2.59 +\isamarkuptrue%
    2.60 +%
    2.61 +\begin{isamarkuptext}%
    2.62 +The \verb!thm! antiquotation works nicely for single theorems, but
    2.63 +  sets of equations as used in definitions are more difficult to
    2.64 +  typeset nicely: for some reason people tend to prefer aligned 
    2.65 +  \isa{{\isacharequal}} signs.
    2.66 +
    2.67 +  To deal with such cases where it is desirable to dive into the structure
    2.68 +  of terms and theorems, Isabelle offers two antiquotations featuring
    2.69 +  ``styles'':
    2.70 +
    2.71 +    \begin{quote}
    2.72 +    \verb!@!\verb!{thm_style stylename thm}!\\
    2.73 +    \verb!@!\verb!{term_style stylename term}!
    2.74 +    \end{quote}
    2.75 +
    2.76 +  A ``style'' is a transformation of terms. There are three predefined
    2.77 +  styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious
    2.78 +  meanings. For example, the output
    2.79 +  \begin{center}
    2.80 +  \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
    2.81 +  \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
    2.82 +  \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs}
    2.83 +  \end{tabular}
    2.84 +  \end{center}
    2.85 +  is produced by the following code:
    2.86 +  \begin{quote}
    2.87 +    \verb!\begin{center}!\\
    2.88 +    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
    2.89 +    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
    2.90 +    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
    2.91 +    \verb!\end{tabular}!\\
    2.92 +    \verb!\end{center}!
    2.93 +  \end{quote}
    2.94 +  Note the space between \verb!@! and \verb!{! in the tabular argument.
    2.95 +  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
    2.96 +  as an antiquotation. Both styles \verb!lhs! and \verb!rhs! 
    2.97 +  try to be smart about the interpretation of the theorem they transform
    2.98 +  they work just as well for meta equality \isa{{\isasymequiv}} and other
    2.99 +  binary operators like \isa{{\isacharless}}.
   2.100 +
   2.101 +  Likewise \verb!conclusion! may be used as style to show just the conclusion
   2.102 +  of a formula:
   2.103 +  \begin{center}
   2.104 +    \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
   2.105 +  \end{center}
   2.106 +  is produced by
   2.107 +  \begin{quote}
   2.108 +    \verb!\begin{center}!\\
   2.109 +    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
   2.110 +    \verb!\end{center}!
   2.111 +  \end{quote}
   2.112 +
   2.113 +  If you are not afraid of ML, you may also define your own styles.
   2.114 +  A style is simply implemented by an ML function of type \verb!term -> term!.
   2.115 +  Have a look at the following example (which indeed shows just the way the
   2.116 +  \verb!lhs! style is implemented):
   2.117 +  \begin{quote}
   2.118 +    \verb!setup {!\verb!*!\\
   2.119 +    \verb!let!\\
   2.120 +    \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
   2.121 +    \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
   2.122 +    \verb!    | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\
   2.123 +    \verb!    | my_lhs (_ $ t $ _) = t!\\
   2.124 +    \verb!    | my_lhs _ = error ("Binary operator expected")!\\
   2.125 +    \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
   2.126 +    \verb!end;!\\
   2.127 +    \verb!*!\verb!}!\\
   2.128 +  \end{quote}
   2.129 +  This code must go into your theory file, not as part of your
   2.130 +  \LaTeX\ text but as a separate command in front of it.
   2.131 +  Like in this example, it is recommended to put the definition of the style
   2.132 +  function into a \verb!let! expression, in order not to pollute the
   2.133 +  ML global namespace. The mapping from identifier name to the style function
   2.134 +  is done by the \verb!Style.put_style! expression which expects the desired
   2.135 +  style name and the style function as arguments. After this \verb!setup!,
   2.136 +  there will be a new style available named \verb!new_lhs! allowing
   2.137 +  antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
   2.138 +  yielding \isa{rev\ {\isacharparenleft}map\ f\ xs{\isacharparenright}}.
   2.139 +
   2.140 +  The example above may be used as as a ``copy-and-paste'' pattern to write
   2.141 +  your own styles; for a description of the constructs used, please refer
   2.142 +  to the Isabelle reference manual.%
   2.143 +\end{isamarkuptext}%
   2.144 +\isamarkuptrue%
   2.145  \isamarkupfalse%
   2.146  \end{isabellebody}%
   2.147  %%% Local Variables:
     3.1 --- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Wed May 11 17:45:38 2005 +0200
     3.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex	Thu May 12 09:45:54 2005 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4  \begin{document}
     3.5  
     3.6  \title{\LaTeX\ Sugar for Isabelle documents}
     3.7 -\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
     3.8 +\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
     3.9  \maketitle
    3.10  
    3.11  \begin{abstract}