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