doc-src/LaTeXsugar/Sugar/Sugar.thy
changeset 15917 cd4983c76548
parent 15689 621bd0d8048f
child 15953 902b556e4bc0
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 10:25:30 2005 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 10:32:32 2005 +0200
     1.3 @@ -195,45 +195,6 @@
     1.4  \end{theorem}
     1.5  *}
     1.6  
     1.7 -subsection {*Definitions and Equations*}
     1.8 -
     1.9 -text {*
    1.10 -  The \verb!thm! antiquotation works nicely for proper theorems, but
    1.11 -  sets of equations as used in definitions are more difficult to
    1.12 -  typeset nicely: for some reason people tend to prefer aligned 
    1.13 -  @{text "="} signs.
    1.14 -
    1.15 -  Isabelle2005 has a nice mechanism for this, namely the two
    1.16 -  antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
    1.17 -
    1.18 -  \begin{center}
    1.19 -  \begin{tabular}{l@ {~~@{text "="}~~}l}
    1.20 -  @{lhs foldl_Nil} & @{rhs foldl_Nil}\\
    1.21 -  @{lhs foldl_Cons} & @{rhs foldl_Cons}
    1.22 -  \end{tabular}
    1.23 -  \end{center}
    1.24 -
    1.25 -  \noindent 
    1.26 -  is produced by the following code:
    1.27 -
    1.28 -\begin{quote}
    1.29 -  \verb!\begin{center}!\\
    1.30 -  \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
    1.31 -  \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\
    1.32 -  \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\
    1.33 -  \verb!\end{tabular}!\\
    1.34 -  \verb!\end{center}!
    1.35 -\end{quote}
    1.36 -
    1.37 -  \noindent
    1.38 -  Note the space between \verb!@! and \verb!{! in the tabular argument.
    1.39 -  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
    1.40 -  as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}! 
    1.41 -  try to be smart about the interpretation of the theorem they
    1.42 -  print, they work just as well for meta equality @{text "\<equiv>"} and other
    1.43 -  binary operators like @{text "<"}.
    1.44 -*}
    1.45 -
    1.46  subsection "Patterns"
    1.47  
    1.48  text {*
    1.49 @@ -311,6 +272,105 @@
    1.50    
    1.51  *}
    1.52  
    1.53 +subsection "Styles"
    1.54 +
    1.55 +text {*
    1.56 +  The \verb!thm! antiquotation works nicely for proper theorems, but
    1.57 +  sets of equations as used in definitions are more difficult to
    1.58 +  typeset nicely: for some reason people tend to prefer aligned 
    1.59 +  @{text "="} signs.
    1.60 +
    1.61 +  To deal with such cases where it is desirable to dive into the structure
    1.62 +  of terms and theorems, Isabelle offers two antiquotations featuring
    1.63 +  ``styles'':
    1.64 +
    1.65 +    \begin{quote}
    1.66 +    \verb!@!\verb!{thm_style stylename thm}!\\
    1.67 +    \verb!@!\verb!{term_style stylename term}!
    1.68 +    \end{quote}
    1.69 +
    1.70 +  A ``style'' is a transformation of terms; there are three predefined
    1.71 +  styles, named \verb!lhs!, \verb!rhs! and \verb!concl!, which obvious
    1.72 +  meanings, e.~g.~the output
    1.73 +
    1.74 +  \begin{center}
    1.75 +  \begin{tabular}{l@ {~~@{text "="}~~}l}
    1.76 +  @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
    1.77 +  @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
    1.78 +  \end{tabular}
    1.79 +  \end{center}
    1.80 +
    1.81 +  \noindent 
    1.82 +  is produced by the following code:
    1.83 +
    1.84 +  \begin{quote}
    1.85 +    \verb!\begin{center}!\\
    1.86 +    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
    1.87 +    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
    1.88 +    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
    1.89 +    \verb!\end{tabular}!\\
    1.90 +    \verb!\end{center}!
    1.91 +  \end{quote}
    1.92 +
    1.93 +  \noindent
    1.94 +  Note the space between \verb!@! and \verb!{! in the tabular argument.
    1.95 +  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
    1.96 +  as antiquotation. Both styles \verb!lhs! and \verb!rhs! 
    1.97 +  try to be smart about the interpretation of the theorem they transform
    1.98 +  they work just as well for meta equality @{text "\<equiv>"} and other
    1.99 +  binary operators like @{text "<"}.
   1.100 +
   1.101 +  Likewise \verb!conclusion! may be used as style to show just the conclusion
   1.102 +  of a formula:
   1.103 +
   1.104 +  \begin{center}
   1.105 +    @{thm_style conclusion hd_Cons_tl}
   1.106 +  \end{center}
   1.107 +
   1.108 +  \noindent 
   1.109 +  is produced by
   1.110 +
   1.111 +  \begin{quote}
   1.112 +    \verb!\begin{center}!\\
   1.113 +    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
   1.114 +    \verb!\end{center}!
   1.115 +  \end{quote}
   1.116 +
   1.117 +  If you aren't afraid about ML, you may also define your own styles;
   1.118 +  a style is simply implemented by a ML function \verb!Term.term -> Term.term!.
   1.119 +  Have a look at the following example (which indeed shows just the way the
   1.120 +  \verb!lhs! style is implemented):
   1.121 +
   1.122 +  \begin{quote}
   1.123 +    \verb!setup {!\verb!*!\\
   1.124 +    \verb!!\\
   1.125 +    \verb!let!\\
   1.126 +    \verb!  fun my_lhs (Const ("==", _) $ t $ _) = t!\\
   1.127 +    \verb!    | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\
   1.128 +    \verb!    | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\
   1.129 +    \verb!    | my_lhs (_ $ t $ _) = t!\\
   1.130 +    \verb!    | my_lhs _ = error ("Binary operator expected")!\\
   1.131 +    \verb!  in [Style.put_style "new_lhs" my_lhs]!\\
   1.132 +    \verb!end;!\\
   1.133 +    \verb!!\\
   1.134 +    \verb!*!\verb!}!\\
   1.135 +  \end{quote}
   1.136 +
   1.137 +  Like in this example, it is recommended to put the definition of the style
   1.138 +  function into a \verb!let! expression, in order not to pollute the
   1.139 +  ML global namespace. The mapping from identifier name to the style function
   1.140 +  is done by the \verb!Style.put_style! expression which expects the desired
   1.141 +  style name and the style function as arguments. After this \verb!setup!,
   1.142 +  there will be a new style available named \verb!new_lhs!, then allowing
   1.143 +  antiquoations like \verb!@!\verb!{term_style new_lhs rev_map}!
   1.144 +  yielding \verb!rev (map f xs)!.
   1.145 +
   1.146 +  The example above may be used as as a ``copy-and-paste'' pattern to write
   1.147 +  your own styles; for a description of the constructs used, please refer
   1.148 +  to the Isabelle reference manual.
   1.149 +
   1.150 +*}
   1.151 +
   1.152  (*<*)
   1.153  end
   1.154  (*>*)
   1.155 \ No newline at end of file