7.4. Arithmetic Expressions 173
Case[x]
The left hand side of equation (7.20) equals eval.f;n/by this base case in
Definition 7.4.3 of the substitution function, and the right hand side also
equals eval.f;n/by this base case in Definition 7.4.2 of eval.
Case[k].
The left hand side of equation (7.20) equalskby this base case in Defini-
tions 7.4.3 and 7.4.2 of the substitution and evaluation functions. Likewise,
the right hand side equalskby two applications of this base case in the Def-
inition 7.4.2 of eval.Constructor cases:
Case[[e 1 Ce 2 ]]
By the structural induction hypothesis (7.20), we may assume that for all
f 2 Aexp andn 2 Z,eval.subst.f;ei/;n/Deval.ei;eval.f;n// (7.21)
foriD1;2. We wish to prove that
eval.subst.f;[e 1 Ce 2 ]/;n/Deval.[e 1 Ce 2 ];eval.f;n// (7.22)
But the left hand side of (7.22) equals
eval.[subst.f;e 1 /Csubst.f;e 2 /];n/
by Definition 7.4.3.7.16 of substitution into a sum expression. But this equals
eval.subst.f;e 1 /;n/Ceval.subst.f;e 2 /;n/
by Definition 7.4.2.(7.11) of eval for a sum expression. By induction hypoth-
esis (7.21), this in turn equals
eval.e 1 ;eval.f;n//Ceval.e 2 ;eval.f;n//:
Finally, this last expression equals the right hand side of (7.22) by Defini-
tion 7.4.2.(7.11) of eval for a sum expression. This proves (7.22) in this case. Case[[e 1 e 2 ]] Similar.
Case[ [e 1 ]] Even easier.
This covers all the constructor cases, and so completes the proof by structural
induction.