author wenzelm Mon, 21 Aug 2000 19:29:27 +0200 changeset 9674 f789d2490669 parent 9673 1b2d4f995b13 child 9675 0fe0dce56bd8
updated;
--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -15,14 +15,14 @@
you are trying to establish holds for the left-hand side provided it holds
for all recursive calls on the right-hand side. Here is a simple example%
\end{isamarkuptext}%
-\isacommand{lemma}\ {"}map\ f\ (sep(x,xs))\ =\ sep(f\ x,\ map\ f\ xs){"}%
+\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
involving the predefined \isa{map} functional on lists: \isa{map f xs}
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
this lemma by recursion induction w.r.t. \isa{sep}:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac\ x\ xs\ rule:\ sep.induct)%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
The resulting proof state has three subgoals corresponding to the three
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -3,30 +3,30 @@
\begin{isamarkuptext}%
Here is a simple example, the Fibonacci function:%
\end{isamarkuptext}%
-\isacommand{consts}\ fib\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ fib\ {"}measure({\isasymlambda}n.\ n){"}\isanewline
-\ \ {"}fib\ 0\ =\ 0{"}\isanewline
-\ \ {"}fib\ 1\ =\ 1{"}\isanewline
-\ \ {"}fib\ (Suc(Suc\ x))\ =\ fib\ x\ +\ fib\ (Suc\ x){"}%
+\isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
The definition of \isa{fib} is accompanied by a \bfindex{measure function}
-\isa{{\isasymlambda}\mbox{n}.\ \mbox{n}} which maps the argument of \isa{fib} to a
+\isa{{\isasymlambda}\mbox{n}{\isachardot}\ \mbox{n}} which maps the argument of \isa{fib} to a
natural number. The requirement is that in each equation the measure of the
argument on the left-hand side is strictly greater than the measure of the
argument of each recursive call. In the case of \isa{fib} this is
obviously true because the measure function is the identity and
-\isa{Suc\ (Suc\ \mbox{x})} is strictly greater than both \isa{x} and
+\isa{Suc\ {\isacharparenleft}Suc\ \mbox{x}{\isacharparenright}} is strictly greater than both \isa{x} and
\isa{Suc\ \mbox{x}}.

Slightly more interesting is the insertion of a fixed element
between any two elements of a list:%
\end{isamarkuptext}%
-\isacommand{consts}\ sep\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
-\ \ {"}sep(a,\ [])\ \ \ \ \ =\ []{"}\isanewline
-\ \ {"}sep(a,\ [x])\ \ \ \ =\ [x]{"}\isanewline
-\ \ {"}sep(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep(a,y\#zs){"}%
+\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
This time the measure is the length of the list, which decreases with the
@@ -34,18 +34,18 @@

Pattern matching need not be exhaustive:%
\end{isamarkuptext}%
-\isacommand{consts}\ last\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}\isanewline
-\isacommand{recdef}\ last\ {"}measure\ ({\isasymlambda}xs.\ length\ xs){"}\isanewline
-\ \ {"}last\ [x]\ \ \ \ \ \ =\ x{"}\isanewline
-\ \ {"}last\ (x\#y\#zs)\ =\ last\ (y\#zs){"}%
+\isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
Overlapping patterns are disambiguated by taking the order of equations into
account, just as in functional programming:%
\end{isamarkuptext}%
-\isacommand{consts}\ sep1\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep1\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
-\ \ {"}sep1(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep1(a,y\#zs){"}\isanewline
-\ \ {"}sep1(a,\ xs)\ \ \ \ \ =\ xs{"}%
+\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
This defines exactly the same function as \isa{sep} above, i.e.\
@@ -60,18 +60,18 @@
arguments as in the following definition:
\end{warn}%
\end{isamarkuptext}%
-\isacommand{consts}\ sep2\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ sep2\ {"}measure\ length{"}\isanewline
-\ \ {"}sep2\ (x\#y\#zs)\ =\ ({\isasymlambda}a.\ x\ \#\ a\ \#\ sep2\ zs\ a){"}\isanewline
-\ \ {"}sep2\ xs\ \ \ \ \ \ \ =\ ({\isasymlambda}a.\ xs){"}%
+\isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{2}\ zs\ a{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}sep\isadigit{2}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
for the definition of non-recursive functions:%
\end{isamarkuptext}%
-\isacommand{consts}\ swap12\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
-\isacommand{recdef}\ swap12\ {"}{\isabraceleft}{\isabraceright}{"}\isanewline
-\ \ {"}swap12\ (x\#y\#zs)\ =\ y\#x\#zs{"}\isanewline
-\ \ {"}swap12\ zs\ \ \ \ \ \ \ =\ zs{"}%
+\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
For non-recursive functions the termination measure degenerates to the empty
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -8,9 +8,9 @@
terminate because of automatic splitting of \isa{if}.
Let us look at an example:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ gcd\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
-\ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n)){"}%
+\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}\isadigit{0}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
According to the measure function, the second argument should decrease with
@@ -18,7 +18,7 @@
\begin{quote}

\begin{isabelle}%
-\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ <\ \mbox{n}
+\mbox{n}\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ {\isacharless}\ \mbox{n}
\end{isabelle}%

\end{quote}
@@ -33,7 +33,7 @@
\begin{quote}

\begin{isabelle}%
-gcd\ (\mbox{m},\ \mbox{n})\ =\ \mbox{k}
+gcd\ {\isacharparenleft}\mbox{m}{\isacharcomma}\ \mbox{n}{\isacharparenright}\ {\isacharequal}\ \mbox{k}
\end{isabelle}%

\end{quote}
@@ -41,7 +41,7 @@
\begin{quote}

\begin{isabelle}%
-(if\ \mbox{n}\ =\ 0\ then\ \mbox{m}\ else\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n}))\ =\ \mbox{k}
+{\isacharparenleft}if\ \mbox{n}\ {\isacharequal}\ \isadigit{0}\ then\ \mbox{m}\ else\ gcd\ {\isacharparenleft}\mbox{n}{\isacharcomma}\ \mbox{m}\ mod\ \mbox{n}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ \mbox{k}
\end{isabelle}%

\end{quote}
@@ -49,11 +49,11 @@
\begin{quote}

\begin{isabelle}%
-(\mbox{n}\ =\ 0\ {\isasymlongrightarrow}\ \mbox{m}\ =\ \mbox{k})\ {\isasymand}\ (\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})\ =\ \mbox{k})
+{\isacharparenleft}\mbox{n}\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ \mbox{m}\ {\isacharequal}\ \mbox{k}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}\mbox{n}\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}\mbox{n}{\isacharcomma}\ \mbox{m}\ mod\ \mbox{n}{\isacharparenright}\ {\isacharequal}\ \mbox{k}{\isacharparenright}
\end{isabelle}%

\end{quote}
-Since the recursive call \isa{gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})} is no longer protected by
+Since the recursive call \isa{gcd\ {\isacharparenleft}\mbox{n}{\isacharcomma}\ \mbox{m}\ mod\ \mbox{n}{\isacharparenright}} is no longer protected by
an \isa{if}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.
@@ -68,10 +68,10 @@
rather than \isa{if} on the right. In the case of \isa{gcd} the
following alternative definition suggests itself:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd1\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ gcd1\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
-\ \ {"}gcd1\ (m,\ 0)\ =\ m{"}\isanewline
-\ \ {"}gcd1\ (m,\ n)\ =\ gcd1(n,\ m\ mod\ n){"}%
+\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\begin{isamarkuptext}%
\noindent
Note that the order of equations is important and hides the side condition
@@ -81,9 +81,9 @@
A very simple alternative is to replace \isa{if} by \isa{case}, which
is also available for \isa{bool} but is not split automatically:%
\end{isamarkuptext}%
-\isacommand{consts}\ gcd2\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ gcd2\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
-\ \ {"}gcd2(m,n)\ =\ (case\ n=0\ of\ True\ {\isasymRightarrow}\ m\ |\ False\ {\isasymRightarrow}\ gcd2(n,m\ mod\ n)){"}%
+\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\begin{isamarkuptext}%
\noindent
In fact, this is probably the neatest solution next to pattern matching.
@@ -91,15 +91,15 @@
A final alternative is to replace the offending simplification rules by
derived conditional ones. For \isa{gcd} it means we have to prove%
\end{isamarkuptext}%
-\isacommand{lemma}\ [simp]:\ {"}gcd\ (m,\ 0)\ =\ m{"}\isanewline
-\isacommand{by}(simp)\isanewline
-\isacommand{lemma}\ [simp]:\ {"}n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ gcd(m,\ n)\ =\ gcd(n,\ m\ mod\ n){"}\isanewline
-\isacommand{by}(simp)%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp{\isacharparenright}\isanewline
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
after which we can disable the original simplification rule:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ [simp\ del]\ =\ gcd.simps\isanewline
+\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
\end{isabelle}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -15,9 +15,9 @@
(there is one for each recursive call) automatically. For example,
termination of the following artificial function%
\end{isamarkuptext}%
-\isacommand{consts}\ f\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ f\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
-\ \ {"}f(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ f(x,y+1)){"}%
+\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
is not proved automatically (although maybe it should be). Isabelle prints a
@@ -25,30 +25,30 @@
have to prove it as a separate lemma before you attempt the definition
of your function once more. In our case the required lemma is the obvious one:%
\end{isamarkuptext}%
-\isacommand{lemma}\ termi\_lem[simp]:\ {"}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ -\ Suc\ y\ <\ x\ -\ y{"}%
+\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
It was not proved automatically because of the special nature of \isa{-}
on \isa{nat}. This requires more arithmetic than is tried by default:%
\end{isamarkuptxt}%
-\isacommand{by}(arith)%
+\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
Because \isacommand{recdef}'s termination prover involves simplification,
we have turned our lemma into a simplification rule. Therefore our second
attempt to define our function will automatically take it into account:%
\end{isamarkuptext}%
-\isacommand{consts}\ g\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ g\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
-\ \ {"}g(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ g(x,y+1)){"}%
+\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
This time everything works fine. Now \isa{g.simps} contains precisely the
stated recursion equation for \isa{g} and they are simplification
rules. Thus we can automatically prove%
\end{isamarkuptext}%
-\isacommand{theorem}\ wow:\ {"}g(1,0)\ =\ g(1,1){"}\isanewline
-\isacommand{by}(simp)%
+\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
More exciting theorems require induction, which is discussed below.
@@ -57,7 +57,7 @@
simplification rule for the sake of the termination proof, we may want to
disable it again:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ [simp\ del]\ =\ termi\_lem%
+\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem%
\begin{isamarkuptext}%
The attentive reader may wonder why we chose to call our function \isa{g}
rather than \isa{f} the second time around. The reason is that, despite
@@ -76,11 +76,11 @@
allows arbitrary wellfounded relations. For example, termination of
Ackermann's function requires the lexicographic product \isa{<*lex*>}:%
\end{isamarkuptext}%
-\isacommand{consts}\ ack\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
-\isacommand{recdef}\ ack\ {"}measure(\%m.\ m)\ <*lex*>\ measure(\%n.\ n){"}\isanewline
-\ \ {"}ack(0,n)\ \ \ \ \ \ \ \ \ =\ Suc\ n{"}\isanewline
-\ \ {"}ack(Suc\ m,0)\ \ \ \ \ =\ ack(m,\ 1){"}\isanewline
-\ \ {"}ack(Suc\ m,Suc\ n)\ =\ ack(m,ack(Suc\ m,n)){"}%
+\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isacharpercent}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
For details see the manual~\cite{isabelle-HOL} and the examples in the
--- 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

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
--- a/doc-src/TutorialI/Trie/document/Option2.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Option2.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -1,6 +1,6 @@
\begin{isabelle}%
\isanewline
-\isacommand{datatype}\ 'a\ option\ =\ None\ |\ Some\ 'a\end{isabelle}%
+\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
--- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 21 19:17:07 2000 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 21 19:29:27 2000 +0200
@@ -7,7 +7,7 @@
list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
values \isa{'v} we define a trie as follows:%
\end{isamarkuptext}%
-\isacommand{datatype}\ ('a,'v)trie\ =\ Trie\ \ {"}'v\ option{"}\ \ {"}('a\ *\ ('a,'v)trie)list{"}%
+\isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isacharequal}\ Trie\ \ {\isachardoublequote}{\isacharprime}v\ option{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isacharparenright}list{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
The first component is the optional value, the second component the
@@ -15,48 +15,48 @@
which is fine because products are datatypes as well.
We define two selector functions:%
\end{isamarkuptext}%
-\isacommand{consts}\ value\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'v\ option{"}\isanewline
-\ \ \ \ \ \ \ alist\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ ('a\ *\ ('a,'v)trie)list{"}\isanewline
-\isacommand{primrec}\ {"}value(Trie\ ov\ al)\ =\ ov{"}\isanewline
-\isacommand{primrec}\ {"}alist(Trie\ ov\ al)\ =\ al{"}%
+\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ alist\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isacharparenright}list{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}value{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}alist{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
Association lists come with a generic lookup function:%
\end{isamarkuptext}%
-\isacommand{consts}\ \ \ assoc\ ::\ {"}('key\ *\ 'val)list\ {\isasymRightarrow}\ 'key\ {\isasymRightarrow}\ 'val\ option{"}\isanewline
-\isacommand{primrec}\ {"}assoc\ []\ x\ =\ None{"}\isanewline
-\ \ \ \ \ \ \ \ {"}assoc\ (p\#ps)\ x\ =\isanewline
-\ \ \ \ \ \ \ \ \ \ \ (let\ (a,b)\ =\ p\ in\ if\ a=x\ then\ Some\ b\ else\ assoc\ ps\ x){"}%
+\isacommand{consts}\ \ \ assoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a{\isacharequal}x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
Now we can define the lookup function for tries. It descends into the trie
examining the letters of the search string one by one. As
recursion on lists is simpler than on tries, let us express this as primitive
recursion on the search string argument:%
\end{isamarkuptext}%
-\isacommand{consts}\ \ \ lookup\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'v\ option{"}\isanewline
-\isacommand{primrec}\ {"}lookup\ t\ []\ =\ value\ t{"}\isanewline
-\ \ \ \ \ \ \ \ {"}lookup\ t\ (a\#as)\ =\ (case\ assoc\ (alist\ t)\ a\ of\isanewline
+\isacommand{consts}\ \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
+\isacommand{primrec}\ {\isachardoublequote}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequote}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as){"}%
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
As a first simple property we prove that looking up a string in the empty
trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
distinguishes the two cases whether the search string is empty or not:%
\end{isamarkuptext}%
-\isacommand{lemma}\ [simp]:\ {"}lookup\ (Trie\ None\ [])\ as\ =\ None{"}\isanewline
-\isacommand{by}(case\_tac\ as,\ auto)%
+\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
\begin{isamarkuptext}%
Things begin to get interesting with the definition of an update function
that adds a new (string,value) pair to a trie, overwriting the old value
associated with that string:%
\end{isamarkuptext}%
-\isacommand{consts}\ update\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ ('a,'v)trie{"}\isanewline
+\isacommand{consts}\ update\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie{\isachardoublequote}\isanewline
\isacommand{primrec}\isanewline
-\ \ {"}update\ t\ []\ \ \ \ \ v\ =\ Trie\ (Some\ v)\ (alist\ t){"}\isanewline
-\ \ {"}update\ t\ (a\#as)\ v\ =\isanewline
-\ \ \ \ \ (let\ tt\ =\ (case\ assoc\ (alist\ t)\ a\ of\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ []\ |\ Some\ at\ {\isasymRightarrow}\ at)\isanewline
-\ \ \ \ \ \ in\ Trie\ (value\ t)\ ((a,update\ tt\ as\ v)\#alist\ t)){"}%
+\ \ {\isachardoublequote}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
+\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}{\isacharhash}alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
The base case is obvious. In the recursive case the subtrie
@@ -70,8 +70,8 @@
expand all \isa{let}s and to split all \isa{case}-constructs over
options:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ [simp]\ =\ Let\_def\isanewline
-\isacommand{lemmas}\ [split]\ =\ option.split%
+\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline
+\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split%
\begin{isamarkuptext}%
\noindent
The reason becomes clear when looking (probably after a failed proof
@@ -81,8 +81,8 @@
Our main goal is to prove the correct interaction of \isa{update} and
\isa{lookup}:%
\end{isamarkuptext}%
-\isacommand{theorem}\ {"}{\isasymforall}t\ v\ bs.\ lookup\ (update\ t\ as\ v)\ bs\ =\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (if\ as=bs\ then\ Some\ v\ else\ lookup\ t\ bs){"}%
+\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptxt}%
\noindent
Our plan is to induct on \isa{as}; hence the remaining variables are
@@ -93,7 +93,7 @@
\isa{as} is instantiated.
The start of the proof is completely conventional:%
\end{isamarkuptxt}%
-\isacommand{apply}(induct\_tac\ as,\ auto)%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
Unfortunately, this time we are left with three intimidating looking subgoals:
@@ -106,7 +106,7 @@
well now. It turns out that instead of induction, case distinction
suffices:%
\end{isamarkuptxt}%
-\isacommand{by}(case\_tac[!]\ bs,\ auto)%
+\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
All methods ending in \isa{tac} take an optional first argument that