--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Aug 16 13:42:21 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Aug 16 13:42:23 2005 +0200
@@ -1,7 +1,20 @@
%
\begin{isabellebody}%
\def\isabellecontext{Documents}%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
%
\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
}
@@ -41,10 +54,10 @@
case of mixfixes. The following example of the exclusive-or
operation on boolean values illustrates typical infix declarations.%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
@@ -142,13 +155,23 @@
\medskip Replacing our definition of \isa{xor} by the following
specifies an Isabelle symbol for the new operator:%
\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
-\isamarkupfalse%
+\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent The X-Symbol package within Proof~General provides several
@@ -162,8 +185,19 @@
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
consider the following hybrid declaration of \isa{xor}:%
\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
@@ -171,8 +205,7 @@
\isanewline
\isamarkupfalse%
\isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
-\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
-\isamarkupfalse%
+\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue%
%
\begin{isamarkuptext}%
The \commdx{syntax} command introduced here acts like
@@ -199,12 +232,12 @@
priorities --- just some literal syntax. The following example
associates common symbols with the constructors of a datatype.%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
-\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
+\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent Here the mixfix annotations on the rightmost column happen
@@ -243,7 +276,7 @@
relational notation for membership in a set of pair, replacing \
\isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{consts}\isanewline
\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
\isanewline
@@ -252,7 +285,7 @@
\ \ {\isachardoublequote}{\isacharunderscore}sim{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isasymapprox}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{translations}\isanewline
-\ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
+\ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
@@ -267,10 +300,10 @@
as \isa{{\isasymnoteq}} for negated equalities. The following declaration
stems from Isabelle/HOL itself:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{syntax}\ {\isachardoublequote}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymnoteq}{\isasymignore}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent Normally one would introduce derived concepts like this
@@ -309,17 +342,17 @@
Here is an example to illustrate the idea of Isabelle document
preparation.%
\end{isamarkuptext}%
-\isamarkuptrue%
%
\begin{quotation}
+\isamarkuptrue%
%
\begin{isamarkuptext}%
The following datatype definition of \isa{{\isacharprime}a\ bintree} models
binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
-\ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
+\ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent The datatype induction rule generated here is of the form
@@ -330,9 +363,9 @@
\isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
\end{isabelle}%
\end{isamarkuptext}%
-\isamarkuptrue%
%
\end{quotation}
+\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent The above document output has been produced as follows:
@@ -576,7 +609,7 @@
marginal comments may be given at the same time. Here is a simple
example:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
\ \ %
\isamarkupcmt{a triviality of propositional logic%
@@ -586,11 +619,24 @@
\isamarkupcmt{(should not really bother)%
}
\isanewline
-\ \ \isamarkupfalse%
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
\isamarkupcmt{implicit assumption step involved here%
}
-\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent The above output has been produced as follows:
@@ -812,10 +858,23 @@
than they really were. For example, this ``fully automatic'' proof
is actually a fake:%
\end{isamarkuptext}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
%
\begin{isamarkuptext}%
\noindent Here the real source of the proof has been as follows:
@@ -846,8 +905,19 @@
close parentheses need to be inserted carefully; it is easy to hide
the wrong parts, especially after rearranging the theory text.%
\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex