44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Readme
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports Base
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
chapter {* Comments for Authors *}
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
text {*
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
\begin{itemize}
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
\item This tutorial can be compiled on the command-line with:
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
|
65
|
12 |
@{text [display] "$ isabelle make"}
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
13 |
|
59
|
14 |
You very likely need a recent snapshot of Isabelle in order to compile
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
the tutorial. Some parts of the tutorial also rely on compilation with
|
64
9a6e5e0c4906
deleted old files and added code to give a special tag to the command ML
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
PolyML.
|
59
|
17 |
|
49
|
18 |
\item You can include references to other Isabelle manuals using the
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
reference names from those manuals. To do this the following
|
54
|
20 |
four \LaTeX{} commands are defined:
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
\begin{center}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
\begin{tabular}{l|c|c}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
& Chapters & Sections\\\hline
|
58
|
25 |
Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\
|
|
26 |
Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
\end{tabular}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
\end{center}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
58
|
30 |
So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
in the implementation manual, namely \ichcite{ch:logic}.
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
\item There are various document antiquotations defined for the
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
tutorial. They allow to check the written text against the current
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
Isabelle code and also allow to show responses of the ML-compiler.
|
52
|
36 |
Therefore authors are strongly encouraged to use antiquotations wherever
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
appropriate.
|
52
|
38 |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
The following antiquotations are defined:
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
\begin{itemize}
|
58
|
42 |
\item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used
|
|
43 |
for displaying any ML-ex\-pression, because the antiquotation checks whether
|
|
44 |
the expression is valid ML-code. The @{text "for"}- and @{text
|
|
45 |
"in"}-arguments are optional. The former is used for evaluating open
|
|
46 |
expressions by giving a list of free variables. The latter is used to
|
|
47 |
indicate in which structure or structures the ML-expression should be
|
|
48 |
evaluated. Examples are:
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
|
54
|
50 |
\begin{center}\small
|
58
|
51 |
\begin{tabular}{lll}
|
59
|
52 |
@{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\
|
|
53 |
@{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\
|
|
54 |
@{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\
|
58
|
55 |
\end{tabular}
|
|
56 |
\end{center}
|
|
57 |
|
|
58 |
\item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to
|
|
59 |
display ML-expressions and their response. The first expression is checked
|
|
60 |
like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern
|
|
61 |
that specifies the result the first expression produces. This pattern can
|
59
|
62 |
contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
|
58
|
63 |
first expression will be checked against this pattern. Examples are:
|
|
64 |
|
|
65 |
\begin{center}\small
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
\begin{tabular}{l}
|
58
|
67 |
@{text "@{ML_response \"1+2\" \"3\"}"}\\
|
|
68 |
@{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
\end{tabular}
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
\end{center}
|
52
|
71 |
|
58
|
72 |
which produce respectively
|
|
73 |
|
|
74 |
\begin{center}\small
|
|
75 |
\begin{tabular}{p{3cm}p{3cm}}
|
|
76 |
@{ML_response "1+2" "3"} &
|
|
77 |
@{ML_response "(1+2,3)" "(3,\<dots>)"}
|
|
78 |
\end{tabular}
|
|
79 |
\end{center}
|
|
80 |
|
|
81 |
Note that this antiquotation can only be used when the result can be
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
constructed: it does not work when the code produces an exception or returns
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
|
49
|
84 |
|
58
|
85 |
\item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just
|
|
86 |
like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,
|
|
87 |
except that the result-specification is not checked. Use this antiquotation
|
|
88 |
when the result cannot be constructed or the code generates an
|
|
89 |
exception. Examples are:
|
|
90 |
|
|
91 |
\begin{center}\small
|
|
92 |
\begin{tabular}{ll}
|
59
|
93 |
@{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\
|
|
94 |
& @{text "\"a + b = c\"}"}\smallskip\\
|
|
95 |
@{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\
|
|
96 |
& @{text "\"Exception FAIL raised\"}"}
|
58
|
97 |
\end{tabular}
|
|
98 |
\end{center}
|
|
99 |
|
59
|
100 |
which produce respectively
|
|
101 |
|
|
102 |
\begin{center}\small
|
|
103 |
\begin{tabular}{p{7.2cm}}
|
|
104 |
@{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
|
|
105 |
@{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
|
|
106 |
\end{tabular}
|
|
107 |
\end{center}
|
54
|
108 |
|
59
|
109 |
This output mimics to some extend what the user sees when running the
|
|
110 |
code.
|
|
111 |
|
58
|
112 |
\item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be
|
54
|
113 |
used to show erroneous code. Neither the code nor the response will be
|
58
|
114 |
checked. An example is:
|
52
|
115 |
|
58
|
116 |
\begin{center}\small
|
|
117 |
\begin{tabular}{ll}
|
|
118 |
@{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\
|
|
119 |
& @{text "\"Type unification failed \<dots>\"}"}
|
|
120 |
\end{tabular}
|
|
121 |
\end{center}
|
|
122 |
|
|
123 |
\item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
|
59
|
124 |
referring to a file. It checks whether the file exists. An example
|
|
125 |
is
|
|
126 |
|
|
127 |
@{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
\end{itemize}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
|
58
|
130 |
The listed antiquotations honour options including @{text "[display]"} and
|
|
131 |
@{text "[quotes]"}. For example
|
|
132 |
|
|
133 |
\begin{center}\small
|
|
134 |
@{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
|
|
135 |
\end{center}
|
|
136 |
|
59
|
137 |
whereas
|
58
|
138 |
|
|
139 |
\begin{center}\small
|
|
140 |
@{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
|
|
141 |
\end{center}
|
|
142 |
|
49
|
143 |
\item Functions and value bindings cannot be defined inside antiquotations; they need
|
85
|
144 |
to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
|
58
|
145 |
environments. In this way they are also checked by the compiler. Some \LaTeX-hack in
|
106
bdd82350cf22
renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
146 |
the tutorial, however, ensures that the environment markers are not printed.
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
148 |
\item Line numbers can be printed using
|
114
|
149 |
\isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}
|
|
150 |
for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The
|
|
151 |
tag is \isa{\%linenosgray} when the numbered text should be gray.
|
52
|
152 |
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
\end{itemize}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
154 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
*}
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
|
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
|
49
|
158 |
|
44
dee4b3e66dfe
added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
end |