updated;
authorwenzelm
Mon Aug 21 19:29:27 2000 +0200 (2000-08-21)
changeset 9674f789d2490669
parent 9673 1b2d4f995b13
child 9675 0fe0dce56bd8
updated;
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/document/Option2.tex
doc-src/TutorialI/Trie/document/Trie.tex
     1.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 21 19:17:07 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Mon Aug 21 19:29:27 2000 +0200
     1.3 @@ -15,14 +15,14 @@
     1.4  you are trying to establish holds for the left-hand side provided it holds
     1.5  for all recursive calls on the right-hand side. Here is a simple example%
     1.6  \end{isamarkuptext}%
     1.7 -\isacommand{lemma}\ {"}map\ f\ (sep(x,xs))\ =\ sep(f\ x,\ map\ f\ xs){"}%
     1.8 +\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
     1.9  \begin{isamarkuptxt}%
    1.10  \noindent
    1.11  involving the predefined \isa{map} functional on lists: \isa{map f xs}
    1.12  is the result of applying \isa{f} to all elements of \isa{xs}. We prove
    1.13  this lemma by recursion induction w.r.t. \isa{sep}:%
    1.14  \end{isamarkuptxt}%
    1.15 -\isacommand{apply}(induct\_tac\ x\ xs\ rule:\ sep.induct)%
    1.16 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
    1.17  \begin{isamarkuptxt}%
    1.18  \noindent
    1.19  The resulting proof state has three subgoals corresponding to the three
     2.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:17:07 2000 +0200
     2.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Aug 21 19:29:27 2000 +0200
     2.3 @@ -3,30 +3,30 @@
     2.4  \begin{isamarkuptext}%
     2.5  Here is a simple example, the Fibonacci function:%
     2.6  \end{isamarkuptext}%
     2.7 -\isacommand{consts}\ fib\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline
     2.8 -\isacommand{recdef}\ fib\ {"}measure({\isasymlambda}n.\ n){"}\isanewline
     2.9 -\ \ {"}fib\ 0\ =\ 0{"}\isanewline
    2.10 -\ \ {"}fib\ 1\ =\ 1{"}\isanewline
    2.11 -\ \ {"}fib\ (Suc(Suc\ x))\ =\ fib\ x\ +\ fib\ (Suc\ x){"}%
    2.12 +\isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    2.13 +\isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
    2.14 +\ \ {\isachardoublequote}fib\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
    2.15 +\ \ {\isachardoublequote}fib\ \isadigit{1}\ {\isacharequal}\ \isadigit{1}{\isachardoublequote}\isanewline
    2.16 +\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
    2.17  \begin{isamarkuptext}%
    2.18  \noindent
    2.19  The definition of \isa{fib} is accompanied by a \bfindex{measure function}
    2.20 -\isa{{\isasymlambda}\mbox{n}.\ \mbox{n}} which maps the argument of \isa{fib} to a
    2.21 +\isa{{\isasymlambda}\mbox{n}{\isachardot}\ \mbox{n}} which maps the argument of \isa{fib} to a
    2.22  natural number. The requirement is that in each equation the measure of the
    2.23  argument on the left-hand side is strictly greater than the measure of the
    2.24  argument of each recursive call. In the case of \isa{fib} this is
    2.25  obviously true because the measure function is the identity and
    2.26 -\isa{Suc\ (Suc\ \mbox{x})} is strictly greater than both \isa{x} and
    2.27 +\isa{Suc\ {\isacharparenleft}Suc\ \mbox{x}{\isacharparenright}} is strictly greater than both \isa{x} and
    2.28  \isa{Suc\ \mbox{x}}.
    2.29  
    2.30  Slightly more interesting is the insertion of a fixed element
    2.31  between any two elements of a list:%
    2.32  \end{isamarkuptext}%
    2.33 -\isacommand{consts}\ sep\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
    2.34 -\isacommand{recdef}\ sep\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
    2.35 -\ \ {"}sep(a,\ [])\ \ \ \ \ =\ []{"}\isanewline
    2.36 -\ \ {"}sep(a,\ [x])\ \ \ \ =\ [x]{"}\isanewline
    2.37 -\ \ {"}sep(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep(a,y\#zs){"}%
    2.38 +\isacommand{consts}\ sep\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    2.39 +\isacommand{recdef}\ sep\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    2.40 +\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    2.41 +\ \ {\isachardoublequote}sep{\isacharparenleft}a{\isacharcomma}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ \ \ \ {\isacharequal}\ {\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}\isanewline
    2.42 +\ \ {\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}%
    2.43  \begin{isamarkuptext}%
    2.44  \noindent
    2.45  This time the measure is the length of the list, which decreases with the
    2.46 @@ -34,18 +34,18 @@
    2.47  
    2.48  Pattern matching need not be exhaustive:%
    2.49  \end{isamarkuptext}%
    2.50 -\isacommand{consts}\ last\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}\isanewline
    2.51 -\isacommand{recdef}\ last\ {"}measure\ ({\isasymlambda}xs.\ length\ xs){"}\isanewline
    2.52 -\ \ {"}last\ [x]\ \ \ \ \ \ =\ x{"}\isanewline
    2.53 -\ \ {"}last\ (x\#y\#zs)\ =\ last\ (y\#zs){"}%
    2.54 +\isacommand{consts}\ last\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
    2.55 +\isacommand{recdef}\ last\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}xs{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    2.56 +\ \ {\isachardoublequote}last\ {\isacharbrackleft}x{\isacharbrackright}\ \ \ \ \ \ {\isacharequal}\ x{\isachardoublequote}\isanewline
    2.57 +\ \ {\isachardoublequote}last\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ last\ {\isacharparenleft}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}%
    2.58  \begin{isamarkuptext}%
    2.59  Overlapping patterns are disambiguated by taking the order of equations into
    2.60  account, just as in functional programming:%
    2.61  \end{isamarkuptext}%
    2.62 -\isacommand{consts}\ sep1\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
    2.63 -\isacommand{recdef}\ sep1\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline
    2.64 -\ \ {"}sep1(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep1(a,y\#zs){"}\isanewline
    2.65 -\ \ {"}sep1(a,\ xs)\ \ \ \ \ =\ xs{"}%
    2.66 +\isacommand{consts}\ sep\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    2.67 +\isacommand{recdef}\ sep\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}a{\isacharcomma}xs{\isacharparenright}{\isachardot}\ length\ xs{\isacharparenright}{\isachardoublequote}\isanewline
    2.68 +\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}y{\isacharhash}zs{\isacharparenright}{\isachardoublequote}\isanewline
    2.69 +\ \ {\isachardoublequote}sep\isadigit{1}{\isacharparenleft}a{\isacharcomma}\ xs{\isacharparenright}\ \ \ \ \ {\isacharequal}\ xs{\isachardoublequote}%
    2.70  \begin{isamarkuptext}%
    2.71  \noindent
    2.72  This defines exactly the same function as \isa{sep} above, i.e.\
    2.73 @@ -60,18 +60,18 @@
    2.74    arguments as in the following definition:
    2.75  \end{warn}%
    2.76  \end{isamarkuptext}%
    2.77 -\isacommand{consts}\ sep2\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
    2.78 -\isacommand{recdef}\ sep2\ {"}measure\ length{"}\isanewline
    2.79 -\ \ {"}sep2\ (x\#y\#zs)\ =\ ({\isasymlambda}a.\ x\ \#\ a\ \#\ sep2\ zs\ a){"}\isanewline
    2.80 -\ \ {"}sep2\ xs\ \ \ \ \ \ \ =\ ({\isasymlambda}a.\ xs){"}%
    2.81 +\isacommand{consts}\ sep\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    2.82 +\isacommand{recdef}\ sep\isadigit{2}\ {\isachardoublequote}measure\ length{\isachardoublequote}\isanewline
    2.83 +\ \ {\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
    2.84 +\ \ {\isachardoublequote}sep\isadigit{2}\ xs\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}a{\isachardot}\ xs{\isacharparenright}{\isachardoublequote}%
    2.85  \begin{isamarkuptext}%
    2.86  Because of its pattern-matching syntax, \isacommand{recdef} is also useful
    2.87  for the definition of non-recursive functions:%
    2.88  \end{isamarkuptext}%
    2.89 -\isacommand{consts}\ swap12\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline
    2.90 -\isacommand{recdef}\ swap12\ {"}{\isabraceleft}{\isabraceright}{"}\isanewline
    2.91 -\ \ {"}swap12\ (x\#y\#zs)\ =\ y\#x\#zs{"}\isanewline
    2.92 -\ \ {"}swap12\ zs\ \ \ \ \ \ \ =\ zs{"}%
    2.93 +\isacommand{consts}\ swap\isadigit{1}\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
    2.94 +\isacommand{recdef}\ swap\isadigit{1}\isadigit{2}\ {\isachardoublequote}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequote}\isanewline
    2.95 +\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ y{\isacharhash}x{\isacharhash}zs{\isachardoublequote}\isanewline
    2.96 +\ \ {\isachardoublequote}swap\isadigit{1}\isadigit{2}\ zs\ \ \ \ \ \ \ {\isacharequal}\ zs{\isachardoublequote}%
    2.97  \begin{isamarkuptext}%
    2.98  \noindent
    2.99  For non-recursive functions the termination measure degenerates to the empty
     3.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 21 19:17:07 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Aug 21 19:29:27 2000 +0200
     3.3 @@ -8,9 +8,9 @@
     3.4  terminate because of automatic splitting of \isa{if}.
     3.5  Let us look at an example:%
     3.6  \end{isamarkuptext}%
     3.7 -\isacommand{consts}\ gcd\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
     3.8 -\isacommand{recdef}\ gcd\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
     3.9 -\ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n)){"}%
    3.10 +\isacommand{consts}\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    3.11 +\isacommand{recdef}\ gcd\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
    3.12 +\ \ {\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}%
    3.13  \begin{isamarkuptext}%
    3.14  \noindent
    3.15  According to the measure function, the second argument should decrease with
    3.16 @@ -18,7 +18,7 @@
    3.17  \begin{quote}
    3.18  
    3.19  \begin{isabelle}%
    3.20 -\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ <\ \mbox{n}
    3.21 +\mbox{n}\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ \mbox{m}\ mod\ \mbox{n}\ {\isacharless}\ \mbox{n}
    3.22  \end{isabelle}%
    3.23  
    3.24  \end{quote}
    3.25 @@ -33,7 +33,7 @@
    3.26  \begin{quote}
    3.27  
    3.28  \begin{isabelle}%
    3.29 -gcd\ (\mbox{m},\ \mbox{n})\ =\ \mbox{k}
    3.30 +gcd\ {\isacharparenleft}\mbox{m}{\isacharcomma}\ \mbox{n}{\isacharparenright}\ {\isacharequal}\ \mbox{k}
    3.31  \end{isabelle}%
    3.32  
    3.33  \end{quote}
    3.34 @@ -41,7 +41,7 @@
    3.35  \begin{quote}
    3.36  
    3.37  \begin{isabelle}%
    3.38 -(if\ \mbox{n}\ =\ 0\ then\ \mbox{m}\ else\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n}))\ =\ \mbox{k}
    3.39 +{\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}
    3.40  \end{isabelle}%
    3.41  
    3.42  \end{quote}
    3.43 @@ -49,11 +49,11 @@
    3.44  \begin{quote}
    3.45  
    3.46  \begin{isabelle}%
    3.47 -(\mbox{n}\ =\ 0\ {\isasymlongrightarrow}\ \mbox{m}\ =\ \mbox{k})\ {\isasymand}\ (\mbox{n}\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})\ =\ \mbox{k})
    3.48 +{\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}
    3.49  \end{isabelle}%
    3.50  
    3.51  \end{quote}
    3.52 -Since the recursive call \isa{gcd\ (\mbox{n},\ \mbox{m}\ mod\ \mbox{n})} is no longer protected by
    3.53 +Since the recursive call \isa{gcd\ {\isacharparenleft}\mbox{n}{\isacharcomma}\ \mbox{m}\ mod\ \mbox{n}{\isacharparenright}} is no longer protected by
    3.54  an \isa{if}, it is unfolded again, which leads to an infinite chain of
    3.55  simplification steps. Fortunately, this problem can be avoided in many
    3.56  different ways.
    3.57 @@ -68,10 +68,10 @@
    3.58  rather than \isa{if} on the right. In the case of \isa{gcd} the
    3.59  following alternative definition suggests itself:%
    3.60  \end{isamarkuptext}%
    3.61 -\isacommand{consts}\ gcd1\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
    3.62 -\isacommand{recdef}\ gcd1\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
    3.63 -\ \ {"}gcd1\ (m,\ 0)\ =\ m{"}\isanewline
    3.64 -\ \ {"}gcd1\ (m,\ n)\ =\ gcd1(n,\ m\ mod\ n){"}%
    3.65 +\isacommand{consts}\ gcd\isadigit{1}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    3.66 +\isacommand{recdef}\ gcd\isadigit{1}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
    3.67 +\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
    3.68 +\ \ {\isachardoublequote}gcd\isadigit{1}\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ gcd\isadigit{1}{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequote}%
    3.69  \begin{isamarkuptext}%
    3.70  \noindent
    3.71  Note that the order of equations is important and hides the side condition
    3.72 @@ -81,9 +81,9 @@
    3.73  A very simple alternative is to replace \isa{if} by \isa{case}, which
    3.74  is also available for \isa{bool} but is not split automatically:%
    3.75  \end{isamarkuptext}%
    3.76 -\isacommand{consts}\ gcd2\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
    3.77 -\isacommand{recdef}\ gcd2\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline
    3.78 -\ \ {"}gcd2(m,n)\ =\ (case\ n=0\ of\ True\ {\isasymRightarrow}\ m\ |\ False\ {\isasymRightarrow}\ gcd2(n,m\ mod\ n)){"}%
    3.79 +\isacommand{consts}\ gcd\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    3.80 +\isacommand{recdef}\ gcd\isadigit{2}\ {\isachardoublequote}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}{\isachardot}n{\isacharparenright}{\isachardoublequote}\isanewline
    3.81 +\ \ {\isachardoublequote}gcd\isadigit{2}{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ n{\isacharequal}\isadigit{0}\ of\ True\ {\isasymRightarrow}\ m\ {\isacharbar}\ False\ {\isasymRightarrow}\ gcd\isadigit{2}{\isacharparenleft}n{\isacharcomma}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    3.82  \begin{isamarkuptext}%
    3.83  \noindent
    3.84  In fact, this is probably the neatest solution next to pattern matching.
    3.85 @@ -91,15 +91,15 @@
    3.86  A final alternative is to replace the offending simplification rules by
    3.87  derived conditional ones. For \isa{gcd} it means we have to prove%
    3.88  \end{isamarkuptext}%
    3.89 -\isacommand{lemma}\ [simp]:\ {"}gcd\ (m,\ 0)\ =\ m{"}\isanewline
    3.90 -\isacommand{by}(simp)\isanewline
    3.91 -\isacommand{lemma}\ [simp]:\ {"}n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ gcd(m,\ n)\ =\ gcd(n,\ m\ mod\ n){"}\isanewline
    3.92 -\isacommand{by}(simp)%
    3.93 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ \isadigit{0}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
    3.94 +\isacommand{by}{\isacharparenleft}simp{\isacharparenright}\isanewline
    3.95 +\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
    3.96 +\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
    3.97  \begin{isamarkuptext}%
    3.98  \noindent
    3.99  after which we can disable the original simplification rule:%
   3.100  \end{isamarkuptext}%
   3.101 -\isacommand{lemmas}\ [simp\ del]\ =\ gcd.simps\isanewline
   3.102 +\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ gcd{\isachardot}simps\isanewline
   3.103  \end{isabelle}%
   3.104  %%% Local Variables:
   3.105  %%% mode: latex
     4.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 21 19:17:07 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Mon Aug 21 19:29:27 2000 +0200
     4.3 @@ -15,9 +15,9 @@
     4.4  (there is one for each recursive call) automatically. For example,
     4.5  termination of the following artificial function%
     4.6  \end{isamarkuptext}%
     4.7 -\isacommand{consts}\ f\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
     4.8 -\isacommand{recdef}\ f\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
     4.9 -\ \ {"}f(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ f(x,y+1)){"}%
    4.10 +\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    4.11 +\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
    4.12 +\ \ {\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}%
    4.13  \begin{isamarkuptext}%
    4.14  \noindent
    4.15  is not proved automatically (although maybe it should be). Isabelle prints a
    4.16 @@ -25,30 +25,30 @@
    4.17  have to prove it as a separate lemma before you attempt the definition
    4.18  of your function once more. In our case the required lemma is the obvious one:%
    4.19  \end{isamarkuptext}%
    4.20 -\isacommand{lemma}\ termi\_lem[simp]:\ {"}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ -\ Suc\ y\ <\ x\ -\ y{"}%
    4.21 +\isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
    4.22  \begin{isamarkuptxt}%
    4.23  \noindent
    4.24  It was not proved automatically because of the special nature of \isa{-}
    4.25  on \isa{nat}. This requires more arithmetic than is tried by default:%
    4.26  \end{isamarkuptxt}%
    4.27 -\isacommand{by}(arith)%
    4.28 +\isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
    4.29  \begin{isamarkuptext}%
    4.30  \noindent
    4.31  Because \isacommand{recdef}'s termination prover involves simplification,
    4.32  we have turned our lemma into a simplification rule. Therefore our second
    4.33  attempt to define our function will automatically take it into account:%
    4.34  \end{isamarkuptext}%
    4.35 -\isacommand{consts}\ g\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
    4.36 -\isacommand{recdef}\ g\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline
    4.37 -\ \ {"}g(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ g(x,y+1)){"}%
    4.38 +\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    4.39 +\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
    4.40 +\ \ {\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}%
    4.41  \begin{isamarkuptext}%
    4.42  \noindent
    4.43  This time everything works fine. Now \isa{g.simps} contains precisely the
    4.44  stated recursion equation for \isa{g} and they are simplification
    4.45  rules. Thus we can automatically prove%
    4.46  \end{isamarkuptext}%
    4.47 -\isacommand{theorem}\ wow:\ {"}g(1,0)\ =\ g(1,1){"}\isanewline
    4.48 -\isacommand{by}(simp)%
    4.49 +\isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
    4.50 +\isacommand{by}{\isacharparenleft}simp{\isacharparenright}%
    4.51  \begin{isamarkuptext}%
    4.52  \noindent
    4.53  More exciting theorems require induction, which is discussed below.
    4.54 @@ -57,7 +57,7 @@
    4.55  simplification rule for the sake of the termination proof, we may want to
    4.56  disable it again:%
    4.57  \end{isamarkuptext}%
    4.58 -\isacommand{lemmas}\ [simp\ del]\ =\ termi\_lem%
    4.59 +\isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ termi{\isacharunderscore}lem%
    4.60  \begin{isamarkuptext}%
    4.61  The attentive reader may wonder why we chose to call our function \isa{g}
    4.62  rather than \isa{f} the second time around. The reason is that, despite
    4.63 @@ -76,11 +76,11 @@
    4.64  allows arbitrary wellfounded relations. For example, termination of
    4.65  Ackermann's function requires the lexicographic product \isa{<*lex*>}:%
    4.66  \end{isamarkuptext}%
    4.67 -\isacommand{consts}\ ack\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline
    4.68 -\isacommand{recdef}\ ack\ {"}measure(\%m.\ m)\ <*lex*>\ measure(\%n.\ n){"}\isanewline
    4.69 -\ \ {"}ack(0,n)\ \ \ \ \ \ \ \ \ =\ Suc\ n{"}\isanewline
    4.70 -\ \ {"}ack(Suc\ m,0)\ \ \ \ \ =\ ack(m,\ 1){"}\isanewline
    4.71 -\ \ {"}ack(Suc\ m,Suc\ n)\ =\ ack(m,ack(Suc\ m,n)){"}%
    4.72 +\isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    4.73 +\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
    4.74 +\ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
    4.75 +\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
    4.76 +\ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    4.77  \begin{isamarkuptext}%
    4.78  \noindent
    4.79  For details see the manual~\cite{isabelle-HOL} and the examples in the
     5.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 21 19:17:07 2000 +0200
     5.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Mon Aug 21 19:29:27 2000 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4  \begin{isabelle}%
     5.5 -\isacommand{theory}\ ToyList\ =\ PreList:%
     5.6 +\isacommand{theory}\ ToyList\ {\isacharequal}\ PreList{\isacharcolon}%
     5.7  \begin{isamarkuptext}%
     5.8  \noindent
     5.9  HOL already has a predefined theory of lists called \isa{List} ---
    5.10 @@ -9,8 +9,8 @@
    5.11  theory that contains pretty much everything but lists, thus avoiding
    5.12  ambiguities caused by defining lists twice.%
    5.13  \end{isamarkuptext}%
    5.14 -\isacommand{datatype}\ 'a\ list\ =\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}[]{"})\isanewline
    5.15 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Cons\ 'a\ {"}'a\ list{"}\ \ \ \ \ \ \ \ \ \ \ \ (\isakeyword{infixr}\ {"}\#{"}\ 65)%
    5.16 +\isacommand{datatype}\ {\isacharprime}a\ list\ {\isacharequal}\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}{\isacharparenright}\isanewline
    5.17 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Cons\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}a\ list{\isachardoublequote}\ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequote}{\isacharhash}{\isachardoublequote}\ \isadigit{6}\isadigit{5}{\isacharparenright}%
    5.18  \begin{isamarkuptext}%
    5.19  \noindent
    5.20  The datatype\index{*datatype} \isaindexbold{list} introduces two
    5.21 @@ -22,11 +22,11 @@
    5.22  datatype declaration is annotated with an alternative syntax: instead of
    5.23  \isa{Nil} and \isa{Cons x xs} we can write
    5.24  \isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
    5.25 -\isa{\mbox{x}\ \#\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
    5.26 +\isa{\mbox{x}\ {\isacharhash}\ \mbox{xs}}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
    5.27  alternative syntax is the standard syntax. Thus the list \isa{Cons True
    5.28 -(Cons False Nil)} becomes \isa{True\ \#\ False\ \#\ []}. The annotation
    5.29 +(Cons False Nil)} becomes \isa{True\ {\isacharhash}\ False\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}}. The annotation
    5.30  \isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
    5.31 -the right, i.e.\ the term \isa{\mbox{x}\ \#\ \mbox{y}\ \#\ \mbox{z}} is read as \isa{x
    5.32 +the right, i.e.\ the term \isa{\mbox{x}\ {\isacharhash}\ \mbox{y}\ {\isacharhash}\ \mbox{z}} is read as \isa{x
    5.33  \# (y \# z)} and not as \isa{(x \# y) \# z}.
    5.34  
    5.35  \begin{warn}
    5.36 @@ -38,8 +38,8 @@
    5.37  \end{warn}
    5.38  Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
    5.39  \end{isamarkuptext}%
    5.40 -\isacommand{consts}\ app\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\ \ \ (\isakeyword{infixr}\ {"}@{"}\ 65)\isanewline
    5.41 -\ \ \ \ \ \ \ rev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}%
    5.42 +\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
    5.43 +\ \ \ \ \ \ \ rev\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}%
    5.44  \begin{isamarkuptext}%
    5.45  \noindent
    5.46  In contrast to ML, Isabelle insists on explicit declarations of all functions
    5.47 @@ -47,16 +47,16 @@
    5.48  restriction, the order of items in a theory file is unconstrained.) Function
    5.49  \isa{app} is annotated with concrete syntax too. Instead of the prefix
    5.50  syntax \isa{app xs ys} the infix
    5.51 -\isa{\mbox{xs}\ @\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
    5.52 +\isa{\mbox{xs}\ {\isacharat}\ \mbox{ys}}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
    5.53  form. Both functions are defined recursively:%
    5.54  \end{isamarkuptext}%
    5.55  \isacommand{primrec}\isanewline
    5.56 -{"}[]\ @\ ys\ \ \ \ \ \ \ =\ ys{"}\isanewline
    5.57 -{"}(x\ \#\ xs)\ @\ ys\ =\ x\ \#\ (xs\ @\ ys){"}\isanewline
    5.58 +{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ ys\ \ \ \ \ \ \ {\isacharequal}\ ys{\isachardoublequote}\isanewline
    5.59 +{\isachardoublequote}{\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ {\isacharat}\ ys\ {\isacharequal}\ x\ {\isacharhash}\ {\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}{\isachardoublequote}\isanewline
    5.60  \isanewline
    5.61  \isacommand{primrec}\isanewline
    5.62 -{"}rev\ []\ \ \ \ \ \ \ \ =\ []{"}\isanewline
    5.63 -{"}rev\ (x\ \#\ xs)\ \ =\ (rev\ xs)\ @\ (x\ \#\ []){"}%
    5.64 +{\isachardoublequote}rev\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
    5.65 +{\isachardoublequote}rev\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ \ {\isacharequal}\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}x\ {\isacharhash}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequote}%
    5.66  \begin{isamarkuptext}%
    5.67  \noindent
    5.68  The equations for \isa{app} and \isa{rev} hardly need comments:
    5.69 @@ -94,7 +94,7 @@
    5.70  To lessen this burden, quotation marks around a single identifier can be
    5.71  dropped, unless the identifier happens to be a keyword, as in%
    5.72  \end{isamarkuptext}%
    5.73 -\isacommand{consts}\ {"}end{"}\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}%
    5.74 +\isacommand{consts}\ {\isachardoublequote}end{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
    5.75  \begin{isamarkuptext}%
    5.76  \noindent
    5.77  When Isabelle prints a syntax error message, it refers to the HOL syntax as
    5.78 @@ -114,7 +114,7 @@
    5.79  Our goal is to show that reversing a list twice produces the original
    5.80  list. The input line%
    5.81  \end{isamarkuptext}%
    5.82 -\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}%
    5.83 +\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
    5.84  \begin{isamarkuptxt}%
    5.85  \index{*theorem|bold}\index{*simp (attribute)|bold}
    5.86  \begin{itemize}
    5.87 @@ -160,7 +160,7 @@
    5.88  defined functions are best established by induction. In this case there is
    5.89  not much choice except to induct on \isa{xs}:%
    5.90  \end{isamarkuptxt}%
    5.91 -\isacommand{apply}(induct\_tac\ xs)%
    5.92 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
    5.93  \begin{isamarkuptxt}%
    5.94  \noindent\index{*induct_tac}%
    5.95  This tells Isabelle to perform induction on variable \isa{xs}. The suffix
    5.96 @@ -183,7 +183,7 @@
    5.97  The {\it assumptions} are the local assumptions for this subgoal and {\it
    5.98    conclusion} is the actual proposition to be proved. Typical proof steps
    5.99  that add new assumptions are induction or case distinction. In our example
   5.100 -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
   5.101 +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
   5.102  are multiple assumptions, they are enclosed in the bracket pair
   5.103  \indexboldpos{\isasymlbrakk}{$Isabrl} and
   5.104  \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
   5.105 @@ -191,7 +191,7 @@
   5.106  %FIXME indent!
   5.107  Let us try to solve both goals automatically:%
   5.108  \end{isamarkuptxt}%
   5.109 -\isacommand{apply}(auto)%
   5.110 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
   5.111  \begin{isamarkuptxt}%
   5.112  \noindent
   5.113  This command tells Isabelle to apply a proof strategy called
   5.114 @@ -212,7 +212,7 @@
   5.115  proof}\indexbold{proof!abandon} (at the shell level type
   5.116  \isacommand{oops}\indexbold{*oops}) we start a new proof:%
   5.117  \end{isamarkuptext}%
   5.118 -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}%
   5.119 +\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}%
   5.120  \begin{isamarkuptxt}%
   5.121  \noindent The keywords \isacommand{theorem}\index{*theorem} and
   5.122  \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
   5.123 @@ -224,12 +224,12 @@
   5.124  \isa{ys}. Because \isa{\at} is defined by recursion on
   5.125  the first argument, \isa{xs} is the correct one:%
   5.126  \end{isamarkuptxt}%
   5.127 -\isacommand{apply}(induct\_tac\ xs)%
   5.128 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}%
   5.129  \begin{isamarkuptxt}%
   5.130  \noindent
   5.131  This time not even the base case is solved automatically:%
   5.132  \end{isamarkuptxt}%
   5.133 -\isacommand{apply}(auto)%
   5.134 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
   5.135  \begin{isamarkuptxt}%
   5.136  \begin{isabellepar}%
   5.137  ~1.~rev~ys~=~rev~ys~@~[]\isanewline
   5.138 @@ -245,9 +245,9 @@
   5.139  
   5.140  This time the canonical proof procedure%
   5.141  \end{isamarkuptext}%
   5.142 -\isacommand{lemma}\ app\_Nil2\ [simp]:\ {"}xs\ @\ []\ =\ xs{"}\isanewline
   5.143 -\isacommand{apply}(induct\_tac\ xs)\isanewline
   5.144 -\isacommand{apply}(auto)%
   5.145 +\isacommand{lemma}\ app{\isacharunderscore}Nil\isadigit{2}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   5.146 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   5.147 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
   5.148  \begin{isamarkuptxt}%
   5.149  \noindent
   5.150  leads to the desired message \isa{No subgoals!}:
   5.151 @@ -258,7 +258,7 @@
   5.152  
   5.153  We still need to confirm that the proof is now finished:%
   5.154  \end{isamarkuptxt}%
   5.155 -\isacommand{.}%
   5.156 +\isacommand{{\isachardot}}%
   5.157  \begin{isamarkuptext}%
   5.158  \noindent\indexbold{$Isar@\texttt{.}}%
   5.159  As a result of that final dot, Isabelle associates the lemma
   5.160 @@ -271,9 +271,9 @@
   5.161  
   5.162  Going back to the proof of the first lemma%
   5.163  \end{isamarkuptext}%
   5.164 -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
   5.165 -\isacommand{apply}(induct\_tac\ xs)\isanewline
   5.166 -\isacommand{apply}(auto)%
   5.167 +\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
   5.168 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   5.169 +\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}%
   5.170  \begin{isamarkuptxt}%
   5.171  \noindent
   5.172  we find that this time \isa{auto} solves the base case, but the
   5.173 @@ -299,25 +299,25 @@
   5.174  \begin{comment}
   5.175  \isacommand{oops}%
   5.176  \end{comment}
   5.177 -\isacommand{lemma}\ app\_assoc\ [simp]:\ {"}(xs\ @\ ys)\ @\ zs\ =\ xs\ @\ (ys\ @\ zs){"}\isanewline
   5.178 -\isacommand{apply}(induct\_tac\ xs)\isanewline
   5.179 -\isacommand{by}(auto)%
   5.180 +\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
   5.181 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   5.182 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   5.183  \begin{isamarkuptext}%
   5.184  \noindent
   5.185  succeeds without further ado.
   5.186  
   5.187  Now we can go back and prove the first lemma%
   5.188  \end{isamarkuptext}%
   5.189 -\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline
   5.190 -\isacommand{apply}(induct\_tac\ xs)\isanewline
   5.191 -\isacommand{by}(auto)%
   5.192 +\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
   5.193 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   5.194 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   5.195  \begin{isamarkuptext}%
   5.196  \noindent
   5.197  and then solve our main theorem:%
   5.198  \end{isamarkuptext}%
   5.199 -\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}\isanewline
   5.200 -\isacommand{apply}(induct\_tac\ xs)\isanewline
   5.201 -\isacommand{by}(auto)%
   5.202 +\isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
   5.203 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline
   5.204 +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}%
   5.205  \begin{isamarkuptext}%
   5.206  \noindent
   5.207  The final \isa{end} tells Isabelle to close the current theory because
     6.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex	Mon Aug 21 19:17:07 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex	Mon Aug 21 19:29:27 2000 +0200
     6.3 @@ -1,6 +1,6 @@
     6.4  \begin{isabelle}%
     6.5  \isanewline
     6.6 -\isacommand{datatype}\ 'a\ option\ =\ None\ |\ Some\ 'a\end{isabelle}%
     6.7 +\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a\end{isabelle}%
     6.8  %%% Local Variables:
     6.9  %%% mode: latex
    6.10  %%% TeX-master: "root"
     7.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 21 19:17:07 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Mon Aug 21 19:29:27 2000 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
     7.5  values \isa{'v} we define a trie as follows:%
     7.6  \end{isamarkuptext}%
     7.7 -\isacommand{datatype}\ ('a,'v)trie\ =\ Trie\ \ {"}'v\ option{"}\ \ {"}('a\ *\ ('a,'v)trie)list{"}%
     7.8 +\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}%
     7.9  \begin{isamarkuptext}%
    7.10  \noindent
    7.11  The first component is the optional value, the second component the
    7.12 @@ -15,48 +15,48 @@
    7.13  which is fine because products are datatypes as well.
    7.14  We define two selector functions:%
    7.15  \end{isamarkuptext}%
    7.16 -\isacommand{consts}\ value\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'v\ option{"}\isanewline
    7.17 -\ \ \ \ \ \ \ alist\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ ('a\ *\ ('a,'v)trie)list{"}\isanewline
    7.18 -\isacommand{primrec}\ {"}value(Trie\ ov\ al)\ =\ ov{"}\isanewline
    7.19 -\isacommand{primrec}\ {"}alist(Trie\ ov\ al)\ =\ al{"}%
    7.20 +\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
    7.21 +\ \ \ \ \ \ \ 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
    7.22 +\isacommand{primrec}\ {\isachardoublequote}value{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ ov{\isachardoublequote}\isanewline
    7.23 +\isacommand{primrec}\ {\isachardoublequote}alist{\isacharparenleft}Trie\ ov\ al{\isacharparenright}\ {\isacharequal}\ al{\isachardoublequote}%
    7.24  \begin{isamarkuptext}%
    7.25  \noindent
    7.26  Association lists come with a generic lookup function:%
    7.27  \end{isamarkuptext}%
    7.28 -\isacommand{consts}\ \ \ assoc\ ::\ {"}('key\ *\ 'val)list\ {\isasymRightarrow}\ 'key\ {\isasymRightarrow}\ 'val\ option{"}\isanewline
    7.29 -\isacommand{primrec}\ {"}assoc\ []\ x\ =\ None{"}\isanewline
    7.30 -\ \ \ \ \ \ \ \ {"}assoc\ (p\#ps)\ x\ =\isanewline
    7.31 -\ \ \ \ \ \ \ \ \ \ \ (let\ (a,b)\ =\ p\ in\ if\ a=x\ then\ Some\ b\ else\ assoc\ ps\ x){"}%
    7.32 +\isacommand{consts}\ \ \ assoc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}key\ {\isacharasterisk}\ {\isacharprime}val{\isacharparenright}list\ {\isasymRightarrow}\ {\isacharprime}key\ {\isasymRightarrow}\ {\isacharprime}val\ option{\isachardoublequote}\isanewline
    7.33 +\isacommand{primrec}\ {\isachardoublequote}assoc\ {\isacharbrackleft}{\isacharbrackright}\ x\ {\isacharequal}\ None{\isachardoublequote}\isanewline
    7.34 +\ \ \ \ \ \ \ \ {\isachardoublequote}assoc\ {\isacharparenleft}p{\isacharhash}ps{\isacharparenright}\ x\ {\isacharequal}\isanewline
    7.35 +\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}let\ {\isacharparenleft}a{\isacharcomma}b{\isacharparenright}\ {\isacharequal}\ p\ in\ if\ a{\isacharequal}x\ then\ Some\ b\ else\ assoc\ ps\ x{\isacharparenright}{\isachardoublequote}%
    7.36  \begin{isamarkuptext}%
    7.37  Now we can define the lookup function for tries. It descends into the trie
    7.38  examining the letters of the search string one by one. As
    7.39  recursion on lists is simpler than on tries, let us express this as primitive
    7.40  recursion on the search string argument:%
    7.41  \end{isamarkuptext}%
    7.42 -\isacommand{consts}\ \ \ lookup\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'v\ option{"}\isanewline
    7.43 -\isacommand{primrec}\ {"}lookup\ t\ []\ =\ value\ t{"}\isanewline
    7.44 -\ \ \ \ \ \ \ \ {"}lookup\ t\ (a\#as)\ =\ (case\ assoc\ (alist\ t)\ a\ of\isanewline
    7.45 +\isacommand{consts}\ \ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}trie\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}v\ option{\isachardoublequote}\isanewline
    7.46 +\isacommand{primrec}\ {\isachardoublequote}lookup\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ value\ t{\isachardoublequote}\isanewline
    7.47 +\ \ \ \ \ \ \ \ {\isachardoublequote}lookup\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
    7.48  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ None\isanewline
    7.49 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as){"}%
    7.50 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ lookup\ at\ as{\isacharparenright}{\isachardoublequote}%
    7.51  \begin{isamarkuptext}%
    7.52  As a first simple property we prove that looking up a string in the empty
    7.53  trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
    7.54  distinguishes the two cases whether the search string is empty or not:%
    7.55  \end{isamarkuptext}%
    7.56 -\isacommand{lemma}\ [simp]:\ {"}lookup\ (Trie\ None\ [])\ as\ =\ None{"}\isanewline
    7.57 -\isacommand{by}(case\_tac\ as,\ auto)%
    7.58 +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}lookup\ {\isacharparenleft}Trie\ None\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ as\ {\isacharequal}\ None{\isachardoublequote}\isanewline
    7.59 +\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
    7.60  \begin{isamarkuptext}%
    7.61  Things begin to get interesting with the definition of an update function
    7.62  that adds a new (string,value) pair to a trie, overwriting the old value
    7.63  associated with that string:%
    7.64  \end{isamarkuptext}%
    7.65 -\isacommand{consts}\ update\ ::\ {"}('a,'v)trie\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ ('a,'v)trie{"}\isanewline
    7.66 +\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
    7.67  \isacommand{primrec}\isanewline
    7.68 -\ \ {"}update\ t\ []\ \ \ \ \ v\ =\ Trie\ (Some\ v)\ (alist\ t){"}\isanewline
    7.69 -\ \ {"}update\ t\ (a\#as)\ v\ =\isanewline
    7.70 -\ \ \ \ \ (let\ tt\ =\ (case\ assoc\ (alist\ t)\ a\ of\isanewline
    7.71 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ []\ |\ Some\ at\ {\isasymRightarrow}\ at)\isanewline
    7.72 -\ \ \ \ \ \ in\ Trie\ (value\ t)\ ((a,update\ tt\ as\ v)\#alist\ t)){"}%
    7.73 +\ \ {\isachardoublequote}update\ t\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ \ v\ {\isacharequal}\ Trie\ {\isacharparenleft}Some\ v{\isacharparenright}\ {\isacharparenleft}alist\ t{\isacharparenright}{\isachardoublequote}\isanewline
    7.74 +\ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
    7.75 +\ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
    7.76 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
    7.77 +\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}{\isacharhash}alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    7.78  \begin{isamarkuptext}%
    7.79  \noindent
    7.80  The base case is obvious. In the recursive case the subtrie
    7.81 @@ -70,8 +70,8 @@
    7.82  expand all \isa{let}s and to split all \isa{case}-constructs over
    7.83  options:%
    7.84  \end{isamarkuptext}%
    7.85 -\isacommand{lemmas}\ [simp]\ =\ Let\_def\isanewline
    7.86 -\isacommand{lemmas}\ [split]\ =\ option.split%
    7.87 +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ Let{\isacharunderscore}def\isanewline
    7.88 +\isacommand{lemmas}\ {\isacharbrackleft}split{\isacharbrackright}\ {\isacharequal}\ option{\isachardot}split%
    7.89  \begin{isamarkuptext}%
    7.90  \noindent
    7.91  The reason becomes clear when looking (probably after a failed proof
    7.92 @@ -81,8 +81,8 @@
    7.93  Our main goal is to prove the correct interaction of \isa{update} and
    7.94  \isa{lookup}:%
    7.95  \end{isamarkuptext}%
    7.96 -\isacommand{theorem}\ {"}{\isasymforall}t\ v\ bs.\ lookup\ (update\ t\ as\ v)\ bs\ =\isanewline
    7.97 -\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (if\ as=bs\ then\ Some\ v\ else\ lookup\ t\ bs){"}%
    7.98 +\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}t\ v\ bs{\isachardot}\ lookup\ {\isacharparenleft}update\ t\ as\ v{\isacharparenright}\ bs\ {\isacharequal}\isanewline
    7.99 +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}if\ as{\isacharequal}bs\ then\ Some\ v\ else\ lookup\ t\ bs{\isacharparenright}{\isachardoublequote}%
   7.100  \begin{isamarkuptxt}%
   7.101  \noindent
   7.102  Our plan is to induct on \isa{as}; hence the remaining variables are
   7.103 @@ -93,7 +93,7 @@
   7.104  \isa{as} is instantiated.
   7.105  The start of the proof is completely conventional:%
   7.106  \end{isamarkuptxt}%
   7.107 -\isacommand{apply}(induct\_tac\ as,\ auto)%
   7.108 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ as{\isacharcomma}\ auto{\isacharparenright}%
   7.109  \begin{isamarkuptxt}%
   7.110  \noindent
   7.111  Unfortunately, this time we are left with three intimidating looking subgoals:
   7.112 @@ -106,7 +106,7 @@
   7.113  well now. It turns out that instead of induction, case distinction
   7.114  suffices:%
   7.115  \end{isamarkuptxt}%
   7.116 -\isacommand{by}(case\_tac[!]\ bs,\ auto)%
   7.117 +\isacommand{by}{\isacharparenleft}case{\isacharunderscore}tac{\isacharbrackleft}{\isacharbang}{\isacharbrackright}\ bs{\isacharcomma}\ auto{\isacharparenright}%
   7.118  \begin{isamarkuptext}%
   7.119  \noindent
   7.120  All methods ending in \isa{tac} take an optional first argument that