diff -r 1b2d4f995b13 -r f789d2490669 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 21 19:17:07 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 21 19:29:27 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{theory}\ ToyList\ =\ PreList:% +\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}% \begin{isamarkuptext}% \noindent HOL already has a predefined theory of lists called \isa{List} --- @@ -9,8 +9,8 @@ theory that contains pretty much everything but lists, thus avoiding ambiguities caused by defining lists twice.% \end{isamarkuptext}% -\isacommand{datatype}\ 'a\ list\ =\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}[]{"})\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Cons\ 'a\ {"}'a\ list{"}\ \ \ \ \ \ \ \ \ \ \ \ (\isakeyword{infixr}\ {"}\#{"}\ 65)% +\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}% \begin{isamarkuptext}% \noindent The datatype\index{*datatype} \isaindexbold{list} introduces two @@ -22,11 +22,11 @@ datatype declaration is annotated with an alternative syntax: instead of \isa{Nil} and \isa{Cons x xs} we can write \isa{[]}\index{$HOL2list@\texttt{[]}|bold} and -\isa{\mbox{x}\ \#\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this +\isa{\mbox{x}\ {\isacharhash}\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this alternative syntax is the standard syntax. Thus the list \isa{Cons True -(Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation +(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation \isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to -the right, i.e.\ the term \isa{\mbox{x}\ \#\ \mbox{y}\ \#\ \mbox{z}} is read as \isa{x +the right, i.e.\ the term \isa{\mbox{x}\ {\isacharhash}\ \mbox{y}\ {\isacharhash}\ \mbox{z}} is read as \isa{x \# (y \# z)} and not as \isa{(x \# y) \# z}. \begin{warn} @@ -38,8 +38,8 @@ \end{warn} Next, two functions \isa{app} and \isaindexbold{rev} are declared:% \end{isamarkuptext}% -\isacommand{consts}\ app\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\ \ \ (\isakeyword{infixr}\ {"}@{"}\ 65)\isanewline -\ \ \ \ \ \ \ rev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}% +\isacommand{consts}\ app\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharat}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}\isanewline +\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}% \begin{isamarkuptext}% \noindent In contrast to ML, Isabelle insists on explicit declarations of all functions @@ -47,16 +47,16 @@ restriction, the order of items in a theory file is unconstrained.) Function \isa{app} is annotated with concrete syntax too. Instead of the prefix syntax \isa{app xs ys} the infix -\isa{\mbox{xs}\ @\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred +\isa{\mbox{xs}\ {\isacharat}\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred form. Both functions are defined recursively:% \end{isamarkuptext}% \isacommand{primrec}\isanewline -{"}[]\ @\ ys\ \ \ \ \ \ \ =\ ys{"}\isanewline -{"}(x\ \#\ xs)\ @\ ys\ =\ x\ \#\ (xs\ @\ ys){"}\isanewline +{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline +{\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline \isanewline \isacommand{primrec}\isanewline -{"}rev\ []\ \ \ \ \ \ \ \ =\ []{"}\isanewline -{"}rev\ (x\ \#\ xs)\ \ =\ (rev\ xs)\ @\ (x\ \#\ []){"}% +{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline +{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent The equations for \isa{app} and \isa{rev} hardly need comments: @@ -94,7 +94,7 @@ To lessen this burden, quotation marks around a single identifier can be dropped, unless the identifier happens to be a keyword, as in% \end{isamarkuptext}% -\isacommand{consts}\ {"}end{"}\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}% +\isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}% \begin{isamarkuptext}% \noindent When Isabelle prints a syntax error message, it refers to the HOL syntax as @@ -114,7 +114,7 @@ Our goal is to show that reversing a list twice produces the original list. The input line% \end{isamarkuptext}% -\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}% +\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}% \begin{isamarkuptxt}% \index{*theorem|bold}\index{*simp (attribute)|bold} \begin{itemize} @@ -160,7 +160,7 @@ defined functions are best established by induction. In this case there is not much choice except to induct on \isa{xs}:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac\ xs)% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% \begin{isamarkuptxt}% \noindent\index{*induct_tac}% This tells Isabelle to perform induction on variable \isa{xs}. The suffix @@ -183,7 +183,7 @@ The {\it assumptions} are the local assumptions for this subgoal and {\it conclusion} is the actual proposition to be proved. Typical proof steps that add new assumptions are induction or case distinction. In our example -the only assumption is the induction hypothesis \isa{rev\ (rev\ \mbox{list})\ =\ \mbox{list}}, where \isa{list} is a variable name chosen by Isabelle. If there +the only assumption is the induction hypothesis \isa{rev\ {\isacharparenleft}rev\ \mbox{list}{\isacharparenright}\ {\isacharequal}\ \mbox{list}}, where \isa{list} is a variable name chosen by Isabelle. If there are multiple assumptions, they are enclosed in the bracket pair \indexboldpos{\isasymlbrakk}{$Isabrl} and \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. @@ -191,7 +191,7 @@ %FIXME indent! Let us try to solve both goals automatically:% \end{isamarkuptxt}% -\isacommand{apply}(auto)% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptxt}% \noindent This command tells Isabelle to apply a proof strategy called @@ -212,7 +212,7 @@ proof}\indexbold{proof!abandon} (at the shell level type \isacommand{oops}\indexbold{*oops}) we start a new proof:% \end{isamarkuptext}% -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}% +\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent The keywords \isacommand{theorem}\index{*theorem} and \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate @@ -224,12 +224,12 @@ \isa{ys}. Because \isa{\at} is defined by recursion on the first argument, \isa{xs} is the correct one:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac\ xs)% +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}% \begin{isamarkuptxt}% \noindent This time not even the base case is solved automatically:% \end{isamarkuptxt}% -\isacommand{apply}(auto)% +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabellepar}% ~1.~rev~ys~=~rev~ys~@~[]\isanewline @@ -245,9 +245,9 @@ This time the canonical proof procedure% \end{isamarkuptext}% -\isacommand{lemma}\ app\_Nil2\ [simp]:\ {"}xs\ @\ []\ =\ xs{"}\isanewline -\isacommand{apply}(induct\_tac\ xs)\isanewline -\isacommand{apply}(auto)% +\isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptxt}% \noindent leads to the desired message \isa{No subgoals!}: @@ -258,7 +258,7 @@ We still need to confirm that the proof is now finished:% \end{isamarkuptxt}% -\isacommand{.}% +\isacommand{{\isachardot}}% \begin{isamarkuptext}% \noindent\indexbold{$Isar@\texttt{.}}% As a result of that final dot, Isabelle associates the lemma @@ -271,9 +271,9 @@ Going back to the proof of the first lemma% \end{isamarkuptext}% -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline -\isacommand{apply}(induct\_tac\ xs)\isanewline -\isacommand{apply}(auto)% +\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptxt}% \noindent we find that this time \isa{auto} solves the base case, but the @@ -299,25 +299,25 @@ \begin{comment} \isacommand{oops}% \end{comment} -\isacommand{lemma}\ app\_assoc\ [simp]:\ {"}(xs\ @\ ys)\ @\ zs\ =\ xs\ @\ (ys\ @\ zs){"}\isanewline -\isacommand{apply}(induct\_tac\ xs)\isanewline -\isacommand{by}(auto)% +\isacommand{lemma}\ app{\isacharunderscore}assoc\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptext}% \noindent succeeds without further ado. Now we can go back and prove the first lemma% \end{isamarkuptext}% -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline -\isacommand{apply}(induct\_tac\ xs)\isanewline -\isacommand{by}(auto)% +\isacommand{lemma}\ rev{\isacharunderscore}app\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptext}% \noindent and then solve our main theorem:% \end{isamarkuptext}% -\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}\isanewline -\isacommand{apply}(induct\_tac\ xs)\isanewline -\isacommand{by}(auto)% +\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}% \begin{isamarkuptext}% \noindent The final \isa{end} tells Isabelle to close the current theory because