11 \item boolean expressions contain arithmetic expressions because of |
11 \item boolean expressions contain arithmetic expressions because of |
12 comparisons like ``$m<n$''. |
12 comparisons like ``$m<n$''. |
13 \end{itemize} |
13 \end{itemize} |
14 In Isabelle this becomes% |
14 In Isabelle this becomes% |
15 \end{isamarkuptext}% |
15 \end{isamarkuptext}% |
16 \isacommand{datatype}~'a~aexp~=~IF~~~{"}'a~bexp{"}~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline |
16 \isacommand{datatype}\ 'a\ aexp\ =\ IF\ \ \ {"}'a\ bexp{"}\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline |
17 ~~~~~~~~~~~~~~~~~|~Sum~~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline |
17 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Sum\ \ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline |
18 ~~~~~~~~~~~~~~~~~|~Diff~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline |
18 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Diff\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline |
19 ~~~~~~~~~~~~~~~~~|~Var~'a\isanewline |
19 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Var\ 'a\isanewline |
20 ~~~~~~~~~~~~~~~~~|~Num~nat\isanewline |
20 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Num\ nat\isanewline |
21 \isakeyword{and}~~~~~~'a~bexp~=~Less~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline |
21 \isakeyword{and}\ \ \ \ \ \ 'a\ bexp\ =\ Less\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline |
22 ~~~~~~~~~~~~~~~~~|~And~~{"}'a~bexp{"}~{"}'a~bexp{"}\isanewline |
22 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ \ {"}'a\ bexp{"}\ {"}'a\ bexp{"}\isanewline |
23 ~~~~~~~~~~~~~~~~~|~Neg~~{"}'a~bexp{"}% |
23 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Neg\ \ {"}'a\ bexp{"}% |
24 \begin{isamarkuptext}% |
24 \begin{isamarkuptext}% |
25 \noindent |
25 \noindent |
26 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, |
26 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, |
27 except that we have fixed the values to be of type \isa{nat} and that we |
27 except that we have fixed the values to be of type \isa{nat} and that we |
28 have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean |
28 have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean |
29 expressions can be arithmetic comparisons, conjunctions and negations. |
29 expressions can be arithmetic comparisons, conjunctions and negations. |
30 The semantics is fixed via two evaluation functions% |
30 The semantics is fixed via two evaluation functions% |
31 \end{isamarkuptext}% |
31 \end{isamarkuptext}% |
32 \isacommand{consts}~~evala~::~{"}'a~aexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~nat{"}\isanewline |
32 \isacommand{consts}\ \ evala\ ::\ {"}'a\ aexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ nat{"}\isanewline |
33 ~~~~~~~~evalb~::~{"}'a~bexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~bool{"}% |
33 \ \ \ \ \ \ \ \ evalb\ ::\ {"}'a\ bexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ bool{"}% |
34 \begin{isamarkuptext}% |
34 \begin{isamarkuptext}% |
35 \noindent |
35 \noindent |
36 that take an expression and an environment (a mapping from variables \isa{'a} to values |
36 that take an expression and an environment (a mapping from variables \isa{'a} to values |
37 \isa{nat}) and return its arithmetic/boolean |
37 \isa{nat}) and return its arithmetic/boolean |
38 value. Since the datatypes are mutually recursive, so are functions that |
38 value. Since the datatypes are mutually recursive, so are functions that |
39 operate on them. Hence they need to be defined in a single \isacommand{primrec} |
39 operate on them. Hence they need to be defined in a single \isacommand{primrec} |
40 section:% |
40 section:% |
41 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
42 \isacommand{primrec}\isanewline |
42 \isacommand{primrec}\isanewline |
43 ~~{"}evala~(IF~b~a1~a2)~env~=\isanewline |
43 \ \ {"}evala\ (IF\ b\ a1\ a2)\ env\ =\isanewline |
44 ~~~~~(if~evalb~b~env~then~evala~a1~env~else~evala~a2~env){"}\isanewline |
44 \ \ \ \ \ (if\ evalb\ b\ env\ then\ evala\ a1\ env\ else\ evala\ a2\ env){"}\isanewline |
45 ~~{"}evala~(Sum~a1~a2)~env~=~evala~a1~env~+~evala~a2~env{"}\isanewline |
45 \ \ {"}evala\ (Sum\ a1\ a2)\ env\ =\ evala\ a1\ env\ +\ evala\ a2\ env{"}\isanewline |
46 ~~{"}evala~(Diff~a1~a2)~env~=~evala~a1~env~-~evala~a2~env{"}\isanewline |
46 \ \ {"}evala\ (Diff\ a1\ a2)\ env\ =\ evala\ a1\ env\ -\ evala\ a2\ env{"}\isanewline |
47 ~~{"}evala~(Var~v)~env~=~env~v{"}\isanewline |
47 \ \ {"}evala\ (Var\ v)\ env\ =\ env\ v{"}\isanewline |
48 ~~{"}evala~(Num~n)~env~=~n{"}\isanewline |
48 \ \ {"}evala\ (Num\ n)\ env\ =\ n{"}\isanewline |
49 \isanewline |
49 \isanewline |
50 ~~{"}evalb~(Less~a1~a2)~env~=~(evala~a1~env~<~evala~a2~env){"}\isanewline |
50 \ \ {"}evalb\ (Less\ a1\ a2)\ env\ =\ (evala\ a1\ env\ <\ evala\ a2\ env){"}\isanewline |
51 ~~{"}evalb~(And~b1~b2)~env~=~(evalb~b1~env~{\isasymand}~evalb~b2~env){"}\isanewline |
51 \ \ {"}evalb\ (And\ b1\ b2)\ env\ =\ (evalb\ b1\ env\ {\isasymand}\ evalb\ b2\ env){"}\isanewline |
52 ~~{"}evalb~(Neg~b)~env~=~({\isasymnot}~evalb~b~env){"}% |
52 \ \ {"}evalb\ (Neg\ b)\ env\ =\ ({\isasymnot}\ evalb\ b\ env){"}% |
53 \begin{isamarkuptext}% |
53 \begin{isamarkuptext}% |
54 \noindent |
54 \noindent |
55 In the same fashion we also define two functions that perform substitution:% |
55 In the same fashion we also define two functions that perform substitution:% |
56 \end{isamarkuptext}% |
56 \end{isamarkuptext}% |
57 \isacommand{consts}~substa~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~'b~aexp{"}\isanewline |
57 \isacommand{consts}\ substa\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ aexp\ {\isasymRightarrow}\ 'b\ aexp{"}\isanewline |
58 ~~~~~~~substb~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~'b~bexp{"}% |
58 \ \ \ \ \ \ \ substb\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ bexp\ {\isasymRightarrow}\ 'b\ bexp{"}% |
59 \begin{isamarkuptext}% |
59 \begin{isamarkuptext}% |
60 \noindent |
60 \noindent |
61 The first argument is a function mapping variables to expressions, the |
61 The first argument is a function mapping variables to expressions, the |
62 substitution. It is applied to all variables in the second argument. As a |
62 substitution. It is applied to all variables in the second argument. As a |
63 result, the type of variables in the expression may change from \isa{'a} |
63 result, the type of variables in the expression may change from \isa{'a} |
64 to \isa{'b}. Note that there are only arithmetic and no boolean variables.% |
64 to \isa{'b}. Note that there are only arithmetic and no boolean variables.% |
65 \end{isamarkuptext}% |
65 \end{isamarkuptext}% |
66 \isacommand{primrec}\isanewline |
66 \isacommand{primrec}\isanewline |
67 ~~{"}substa~s~(IF~b~a1~a2)~=\isanewline |
67 \ \ {"}substa\ s\ (IF\ b\ a1\ a2)\ =\isanewline |
68 ~~~~~IF~(substb~s~b)~(substa~s~a1)~(substa~s~a2){"}\isanewline |
68 \ \ \ \ \ IF\ (substb\ s\ b)\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline |
69 ~~{"}substa~s~(Sum~a1~a2)~=~Sum~(substa~s~a1)~(substa~s~a2){"}\isanewline |
69 \ \ {"}substa\ s\ (Sum\ a1\ a2)\ =\ Sum\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline |
70 ~~{"}substa~s~(Diff~a1~a2)~=~Diff~(substa~s~a1)~(substa~s~a2){"}\isanewline |
70 \ \ {"}substa\ s\ (Diff\ a1\ a2)\ =\ Diff\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline |
71 ~~{"}substa~s~(Var~v)~=~s~v{"}\isanewline |
71 \ \ {"}substa\ s\ (Var\ v)\ =\ s\ v{"}\isanewline |
72 ~~{"}substa~s~(Num~n)~=~Num~n{"}\isanewline |
72 \ \ {"}substa\ s\ (Num\ n)\ =\ Num\ n{"}\isanewline |
73 \isanewline |
73 \isanewline |
74 ~~{"}substb~s~(Less~a1~a2)~=~Less~(substa~s~a1)~(substa~s~a2){"}\isanewline |
74 \ \ {"}substb\ s\ (Less\ a1\ a2)\ =\ Less\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline |
75 ~~{"}substb~s~(And~b1~b2)~=~And~(substb~s~b1)~(substb~s~b2){"}\isanewline |
75 \ \ {"}substb\ s\ (And\ b1\ b2)\ =\ And\ (substb\ s\ b1)\ (substb\ s\ b2){"}\isanewline |
76 ~~{"}substb~s~(Neg~b)~=~Neg~(substb~s~b){"}% |
76 \ \ {"}substb\ s\ (Neg\ b)\ =\ Neg\ (substb\ s\ b){"}% |
77 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
78 Now we can prove a fundamental theorem about the interaction between |
78 Now we can prove a fundamental theorem about the interaction between |
79 evaluation and substitution: applying a substitution $s$ to an expression $a$ |
79 evaluation and substitution: applying a substitution $s$ to an expression $a$ |
80 and evaluating the result in an environment $env$ yields the same result as |
80 and evaluating the result in an environment $env$ yields the same result as |
81 evaluation $a$ in the environment that maps every variable $x$ to the value |
81 evaluation $a$ in the environment that maps every variable $x$ to the value |
82 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or |
82 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or |
83 boolean expressions (by induction), you find that you always need the other |
83 boolean expressions (by induction), you find that you always need the other |
84 theorem in the induction step. Therefore you need to state and prove both |
84 theorem in the induction step. Therefore you need to state and prove both |
85 theorems simultaneously:% |
85 theorems simultaneously:% |
86 \end{isamarkuptext}% |
86 \end{isamarkuptext}% |
87 \isacommand{lemma}~{"}evala~(substa~s~a)~env~=~evala~a~({\isasymlambda}x.~evala~(s~x)~env)~{\isasymand}\isanewline |
87 \isacommand{lemma}\ {"}evala\ (substa\ s\ a)\ env\ =\ evala\ a\ ({\isasymlambda}x.\ evala\ (s\ x)\ env)\ {\isasymand}\isanewline |
88 ~~~~~~~~evalb~(substb~s~b)~env~=~evalb~b~({\isasymlambda}x.~evala~(s~x)~env){"}\isanewline |
88 \ \ \ \ \ \ \ \ evalb\ (substb\ s\ b)\ env\ =\ evalb\ b\ ({\isasymlambda}x.\ evala\ (s\ x)\ env){"}\isanewline |
89 \isacommand{apply}(induct\_tac~a~\isakeyword{and}~b)% |
89 \isacommand{apply}(induct\_tac\ a\ \isakeyword{and}\ b)% |
90 \begin{isamarkuptxt}% |
90 \begin{isamarkuptxt}% |
91 \noindent |
91 \noindent |
92 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
92 The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
93 \end{isamarkuptxt}% |
93 \end{isamarkuptxt}% |
94 \isacommand{by}~auto% |
94 \isacommand{by}\ auto% |
95 \begin{isamarkuptext}% |
95 \begin{isamarkuptext}% |
96 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
96 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
97 an inductive proof expects a goal of the form |
97 an inductive proof expects a goal of the form |
98 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
98 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
99 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
99 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
100 \begin{ttbox} |
100 \begin{ttbox} |
101 apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\)); |
101 apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\)); |
102 \end{ttbox} |
102 \end{ttbox} |
103 |
103 |
104 \begin{exercise} |
104 \begin{exercise} |
105 Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that |
105 Define a function \isa{norma} of type \isa{'a\ aexp\ {\isasymRightarrow}\ 'a\ aexp} that |
106 replaces \isa{IF}s with complex boolean conditions by nested |
106 replaces \isa{IF}s with complex boolean conditions by nested |
107 \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and |
107 \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and |
108 \isa{Neg} should be eliminated completely. Prove that \isa{norma} |
108 \isa{Neg} should be eliminated completely. Prove that \isa{norma} |
109 preserves the value of an expression and that the result of \isa{norma} |
109 preserves the value of an expression and that the result of \isa{norma} |
110 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
110 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |