theory Readme

imports Base

begin

chapter {* Comments for Authors *}

text {*

  \begin{itemize}

  \item This tutorial can be compiled on the command-line with:

  @{text [display] "$ isabelle make"}

  You very likely need a recent snapshot of Isabelle in order to compile

  the tutorial. Some parts of the tutorial also rely on compilation with

  PolyML.

  \item You can include references to other Isabelle manuals using the 

  reference names from those manuals. To do this the following

  four \LaTeX{} commands are defined:

  \begin{center}

  \begin{tabular}{l|c|c}

   & Chapters & Sections\\\hline

  Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\

  Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\

  \end{tabular}

  \end{center}

  So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic 

  in the implementation manual, namely \ichcite{ch:logic}.

  \item There are various document antiquotations defined for the 

  tutorial. They allow to check the written text against the current

  Isabelle code and also allow to show responses of the ML-compiler.

  Therefore authors are strongly encouraged to use antiquotations wherever

  appropriate.

  The following antiquotations are defined:

  \begin{itemize}

  \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used

  for displaying any ML-ex\-pression, because the antiquotation checks whether

  the expression is valid ML-code. The @{text "for"}- and @{text

  "in"}-arguments are optional. The former is used for evaluating open

  expressions by giving a list of free variables. The latter is used to

  indicate in which structure or structures the ML-expression should be

  evaluated. Examples are:

  \begin{center}\small

  \begin{tabular}{lll}

  @{text "@{ML \"1 + 3\"}"}         &                 & @{ML "1 + 3"}\\

  @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\

  @{text "@{ML Ident in OuterLex}"} &                 & @{ML Ident in OuterLex}\\

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to

  display ML-expressions and their response.  The first expression is checked

  like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern

  that specifies the result the first expression produces. This pattern can

  contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the

  first expression will be checked against this pattern. Examples are:

  \begin{center}\small

  \begin{tabular}{l}

  @{text "@{ML_response \"1+2\" \"3\"}"}\\

  @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}

  \end{tabular}

  \end{center}

  which produce respectively

  \begin{center}\small

  \begin{tabular}{p{3cm}p{3cm}}

  @{ML_response "1+2" "3"} &  

  @{ML_response "(1+2,3)" "(3,\<dots>)"}

  \end{tabular}

  \end{center}

  Note that this antiquotation can only be used when the result can be

  constructed: it does not work when the code produces an exception or returns 

  an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).

  \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just

  like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,

  except that the result-specification is not checked. Use this antiquotation

  when the result cannot be constructed or the code generates an

  exception. Examples are:

  \begin{center}\small

  \begin{tabular}{ll}

  @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\

                               & @{text "\"a + b = c\"}"}\smallskip\\ 

  @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ 

                               & @{text "\"Exception FAIL raised\"}"}

  \end{tabular}

  \end{center}

  which produce respectively

  \begin{center}\small

  \begin{tabular}{p{7.2cm}}

  @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\

  @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}

  \end{tabular}

  \end{center}

  This output mimics to some extend what the user sees when running the

  code.

  \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be

  used to show erroneous code. Neither the code nor the response will be

  checked. An example is:

  \begin{center}\small

  \begin{tabular}{ll}

  @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\

                                    & @{text "\"Type unification failed \<dots>\"}"}

  \end{tabular}

  \end{center}

  \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when

  referring to a file. It checks whether the file exists.  An example

  is 

  @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}

  \end{itemize}

  The listed antiquotations honour options including @{text "[display]"} and 

  @{text "[quotes]"}. For example

  \begin{center}\small

  @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}

  \end{center}

  whereas

  \begin{center}\small

  @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}

  \end{center}

  \item Functions and value bindings cannot be defined inside antiquotations; they need

  to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}

  environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 

  the tutorial, however, ensures that the environment markers are not printed.

  \item Line numbers can be printed using 

  \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}

  for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The

  tag is \isa{\%linenosgray} when the numbered text should be gray. 

  \end{itemize}

*}

end