3 \def\isabellecontext{ABexpr}%
6 Sometimes it is necessary to define two datatypes that depend on each
7 other. This is called \textbf{mutual recursion}. As an example consider a
8 language of arithmetic and boolean expressions where
10 \item arithmetic expressions contain boolean expressions because there are
11 conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
13 \item boolean expressions contain arithmetic expressions because of
14 comparisons like ``$m<n$''.
16 In Isabelle this becomes%
18 \isacommand{datatype}\ {\isacharprime}a\ aexp\ {\isacharequal}\ IF\ \ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
19 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Sum\ \ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
20 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Diff\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
21 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Var\ {\isacharprime}a\isanewline
22 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Num\ nat\isanewline
23 \isakeyword{and}\ \ \ \ \ \ {\isacharprime}a\ bexp\ {\isacharequal}\ Less\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ aexp{\isachardoublequote}\isanewline
24 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}\isanewline
25 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Neg\ \ {\isachardoublequote}{\isacharprime}a\ bexp{\isachardoublequote}%
26 \begin{isamarkuptext}%
28 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
29 except that we have fixed the values to be of type \isa{nat} and that we
30 have fixed the two binary operations \isa{aexp{\isachardot}Sum} and \isa{Diff}. Boolean
31 expressions can be arithmetic comparisons, conjunctions and negations.
32 The semantics is fixed via two evaluation functions%
34 \isacommand{consts}\ \ evala\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
35 \ \ \ \ \ \ \ \ evalb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}%
36 \begin{isamarkuptext}%
38 that take an expression and an environment (a mapping from variables \isa{{\isacharprime}a} to values
39 \isa{nat}) and return its arithmetic/boolean
40 value. Since the datatypes are mutually recursive, so are functions that
41 operate on them. Hence they need to be defined in a single \isacommand{primrec}
44 \isacommand{primrec}\isanewline
45 \ \ {\isachardoublequote}evala\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ env\ {\isacharequal}\isanewline
46 \ \ \ \ \ {\isacharparenleft}if\ evalb\ b\ env\ then\ evala\ a\isadigit{1}\ env\ else\ evala\ a\isadigit{2}\ env{\isacharparenright}{\isachardoublequote}\isanewline
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
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
49 \ \ {\isachardoublequote}evala\ {\isacharparenleft}Var\ v{\isacharparenright}\ env\ {\isacharequal}\ env\ v{\isachardoublequote}\isanewline
50 \ \ {\isachardoublequote}evala\ {\isacharparenleft}Num\ n{\isacharparenright}\ env\ {\isacharequal}\ n{\isachardoublequote}\isanewline
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
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
54 \ \ {\isachardoublequote}evalb\ {\isacharparenleft}Neg\ b{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ evalb\ b\ env{\isacharparenright}{\isachardoublequote}%
55 \begin{isamarkuptext}%
57 In the same fashion we also define two functions that perform substitution:%
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
60 \ \ \ \ \ \ \ substb\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ aexp{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ bexp\ {\isasymRightarrow}\ {\isacharprime}b\ bexp{\isachardoublequote}%
61 \begin{isamarkuptext}%
63 The first argument is a function mapping variables to expressions, the
64 substitution. It is applied to all variables in the second argument. As a
65 result, the type of variables in the expression may change from \isa{{\isacharprime}a}
66 to \isa{{\isacharprime}b}. Note that there are only arithmetic and no boolean variables.%
68 \isacommand{primrec}\isanewline
69 \ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}IF\ b\ a\isadigit{1}\ a\isadigit{2}{\isacharparenright}\ {\isacharequal}\isanewline
70 \ \ \ \ \ IF\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{1}{\isacharparenright}\ {\isacharparenleft}substa\ s\ a\isadigit{2}{\isacharparenright}{\isachardoublequote}\isanewline
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
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
73 \ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Var\ v{\isacharparenright}\ {\isacharequal}\ s\ v{\isachardoublequote}\isanewline
74 \ \ {\isachardoublequote}substa\ s\ {\isacharparenleft}Num\ n{\isacharparenright}\ {\isacharequal}\ Num\ n{\isachardoublequote}\isanewline
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
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
78 \ \ {\isachardoublequote}substb\ s\ {\isacharparenleft}Neg\ b{\isacharparenright}\ {\isacharequal}\ Neg\ {\isacharparenleft}substb\ s\ b{\isacharparenright}{\isachardoublequote}%
79 \begin{isamarkuptext}%
80 Now we can prove a fundamental theorem about the interaction between
81 evaluation and substitution: applying a substitution $s$ to an expression $a$
82 and evaluating the result in an environment $env$ yields the same result as
83 evaluation $a$ in the environment that maps every variable $x$ to the value
84 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
85 boolean expressions (by induction), you find that you always need the other
86 theorem in the induction step. Therefore you need to state and prove both
87 theorems simultaneously:%
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
90 \ \ \ \ \ \ \ \ evalb\ {\isacharparenleft}substb\ s\ b{\isacharparenright}\ env\ {\isacharequal}\ evalb\ b\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ evala\ {\isacharparenleft}s\ x{\isacharparenright}\ env{\isacharparenright}{\isachardoublequote}\isanewline
91 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ a\ \isakeyword{and}\ b{\isacharparenright}%
94 The resulting 8 goals (one for each constructor) are proved in one fell swoop:%
96 \isacommand{apply}\ simp{\isacharunderscore}all%
97 \begin{isamarkuptext}%
98 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
99 an inductive proof expects a goal of the form
100 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
101 where each variable $x@i$ is of type $\tau@i$. Induction is started by
103 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isa{and} \dots\ \isa{and} $x@n$\isa{{\isacharparenright}}
107 Define a function \isa{norma} of type \isa{{\isacharprime}a\ aexp\ {\isasymRightarrow}\ {\isacharprime}a\ aexp} that
108 replaces \isa{IF}s with complex boolean conditions by nested
109 \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
110 \isa{Neg} should be eliminated completely. Prove that \isa{norma}
111 preserves the value of an expression and that the result of \isa{norma}
112 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
113 it. ({\em Hint:} proceed as in \S\ref{sec:boolex}).
119 %%% TeX-master: "root"