doc-src/TutorialI/Datatype/document/ABexpr.tex
author nipkow
Wed Jan 24 12:29:10 2001 +0100 (2001-01-24)
changeset 10971 6852682eaf16
parent 10187 0376cccd9118
child 11309 d666f11ca2d4
permissions -rw-r--r--
*** empty log message ***
nipkow@9722
     1
%
nipkow@9722
     2
\begin{isabellebody}%
wenzelm@9924
     3
\def\isabellecontext{ABexpr}%
nipkow@8749
     4
%
nipkow@8749
     5
\begin{isamarkuptext}%
nipkow@8749
     6
Sometimes it is necessary to define two datatypes that depend on each
nipkow@8749
     7
other. This is called \textbf{mutual recursion}. As an example consider a
nipkow@8749
     8
language of arithmetic and boolean expressions where
nipkow@8749
     9
\begin{itemize}
nipkow@8749
    10
\item arithmetic expressions contain boolean expressions because there are
nipkow@8749
    11
  conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
nipkow@8749
    12
  and
nipkow@8749
    13
\item boolean expressions contain arithmetic expressions because of
nipkow@8749
    14
  comparisons like ``$m<n$''.
nipkow@8749
    15
\end{itemize}
nipkow@8749
    16
In Isabelle this becomes%
nipkow@8749
    17
\end{isamarkuptext}%
wenzelm@9673
    18
\isacommand{datatype}\ {\isacharprime}a\ aexp\ {\isacharequal}\ IF\ \ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
wenzelm@9673
    19
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Sum\ \ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
wenzelm@9673
    20
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Diff\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
wenzelm@9673
    21
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Var\ {\isacharprime}a\isanewline
wenzelm@9673
    22
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Num\ nat\isanewline
wenzelm@9673
    23
\isakeyword{and}\ \ \ \ \ \ {\isacharprime}a\ bexp\ {\isacharequal}\ Less\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
wenzelm@9673
    24
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\isanewline
wenzelm@9673
    25
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}%
nipkow@8749
    26
\begin{isamarkuptext}%
nipkow@8749
    27
\noindent
nipkow@8749
    28
Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
nipkow@8749
    29
except that we have fixed the values to be of type \isa{nat} and that we
nipkow@10971
    30
have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
nipkow@8749
    31
expressions can be arithmetic comparisons, conjunctions and negations.
nipkow@8749
    32
The semantics is fixed via two evaluation functions%
nipkow@8749
    33
\end{isamarkuptext}%
wenzelm@9673
    34
\isacommand{consts}\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
wenzelm@9673
    35
\ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}%
nipkow@8749
    36
\begin{isamarkuptext}%
nipkow@8749
    37
\noindent
nipkow@9792
    38
that take an expression and an environment (a mapping from variables \isa{{\isacharprime}a} to values
nipkow@8771
    39
\isa{nat}) and return its arithmetic/boolean
nipkow@8749
    40
value. Since the datatypes are mutually recursive, so are functions that
nipkow@8749
    41
operate on them. Hence they need to be defined in a single \isacommand{primrec}
nipkow@8749
    42
section:%
nipkow@8749
    43
\end{isamarkuptext}%
nipkow@8749
    44
\isacommand{primrec}\isanewline
nipkow@10187
    45
\ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\isanewline
nipkow@10187
    46
\ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a{\isadigit{1}}\ env\ else\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    47
\ \ {\isachardoublequote}evala\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharplus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequote}\isanewline
nipkow@10187
    48
\ \ {\isachardoublequote}evala\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ evala\ a{\isadigit{1}}\ env\ {\isacharminus}\ evala\ a{\isadigit{2}}\ env{\isachardoublequote}\isanewline
wenzelm@9673
    49
\ \ {\isachardoublequote}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequote}\isanewline
wenzelm@9673
    50
\ \ {\isachardoublequote}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequote}\isanewline
nipkow@8749
    51
\isanewline
nipkow@10187
    52
\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evala\ a{\isadigit{1}}\ env\ {\isacharless}\ evala\ a{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    53
\ \ {\isachardoublequote}evalb\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}evalb\ b{\isadigit{1}}\ env\ {\isasymand}\ evalb\ b{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@9673
    54
\ \ {\isachardoublequote}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequote}%
nipkow@8749
    55
\begin{isamarkuptext}%
nipkow@8749
    56
\noindent
nipkow@8749
    57
In the same fashion we also define two functions that perform substitution:%
nipkow@8749
    58
\end{isamarkuptext}%
wenzelm@9673
    59
\isacommand{consts}\ substa\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isachardoublequote}\isanewline
wenzelm@9673
    60
\ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequote}%
nipkow@8749
    61
\begin{isamarkuptext}%
nipkow@8749
    62
\noindent
nipkow@8749
    63
The first argument is a function mapping variables to expressions, the
nipkow@8749
    64
substitution. It is applied to all variables in the second argument. As a
nipkow@9792
    65
result, the type of variables in the expression may change from \isa{{\isacharprime}a}
nipkow@9792
    66
to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables.%
nipkow@8749
    67
\end{isamarkuptext}%
nipkow@8749
    68
\isacommand{primrec}\isanewline
nipkow@10187
    69
\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
nipkow@10187
    70
\ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    71
\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Sum\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    72
\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Diff\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@9673
    73
\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequote}\isanewline
wenzelm@9673
    74
\ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequote}\isanewline
nipkow@8749
    75
\isanewline
nipkow@10187
    76
\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ Less\ {\isacharparenleft}substa\ s\ a{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
nipkow@10187
    77
\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ And\ {\isacharparenleft}substb\ s\ b{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}substb\ s\ b{\isadigit{2}}{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@9673
    78
\ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequote}%
nipkow@8749
    79
\begin{isamarkuptext}%
nipkow@8749
    80
Now we can prove a fundamental theorem about the interaction between
nipkow@8749
    81
evaluation and substitution: applying a substitution $s$ to an expression $a$
nipkow@8749
    82
and evaluating the result in an environment $env$ yields the same result as
nipkow@8749
    83
evaluation $a$ in the environment that maps every variable $x$ to the value
nipkow@8749
    84
of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
nipkow@8749
    85
boolean expressions (by induction), you find that you always need the other
nipkow@8749
    86
theorem in the induction step. Therefore you need to state and prove both
nipkow@8749
    87
theorems simultaneously:%
nipkow@8749
    88
\end{isamarkuptext}%
wenzelm@9673
    89
\isacommand{lemma}\ {\isachardoublequote}evala\ {\isacharparenleft}substa\ s\ a{\isacharparenright}\ env\ {\isacharequal}\ evala\ a\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}\ {\isasymand}\isanewline
wenzelm@9673
    90
\ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@9673
    91
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}%
nipkow@8749
    92
\begin{isamarkuptxt}%
nipkow@8749
    93
\noindent
nipkow@8749
    94
The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
nipkow@8749
    95
\end{isamarkuptxt}%
nipkow@10171
    96
\isacommand{apply}\ simp{\isacharunderscore}all%
nipkow@8749
    97
\begin{isamarkuptext}%
nipkow@8749
    98
In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
nipkow@8749
    99
an inductive proof expects a goal of the form
nipkow@8749
   100
\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
nipkow@8749
   101
where each variable $x@i$ is of type $\tau@i$. Induction is started by
nipkow@9792
   102
\begin{isabelle}
nipkow@10971
   103
\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
nipkow@9792
   104
\end{isabelle}
nipkow@8749
   105
nipkow@8749
   106
\begin{exercise}
nipkow@9792
   107
  Define a function \isa{norma} of type \isa{{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}a\ aexp} that
nipkow@8749
   108
  replaces \isa{IF}s with complex boolean conditions by nested
nipkow@8749
   109
  \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
nipkow@8749
   110
  \isa{Neg} should be eliminated completely. Prove that \isa{norma}
nipkow@8749
   111
  preserves the value of an expression and that the result of \isa{norma}
nipkow@8749
   112
  is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
nipkow@8749
   113
  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
nipkow@8749
   114
\end{exercise}%
nipkow@8749
   115
\end{isamarkuptext}%
nipkow@9722
   116
\end{isabellebody}%
wenzelm@9145
   117
%%% Local Variables:
wenzelm@9145
   118
%%% mode: latex
wenzelm@9145
   119
%%% TeX-master: "root"
wenzelm@9145
   120
%%% End: