26 | Neg "'a bexp"; |
26 | Neg "'a bexp"; |
27 |
27 |
28 text{*\noindent |
28 text{*\noindent |
29 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, |
29 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, |
30 except that we have fixed the values to be of type @{typ"nat"} and that we |
30 except that we have fixed the values to be of type @{typ"nat"} and that we |
31 have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean |
31 have fixed the two binary operations @{text Sum} and @{term"Diff"}. Boolean |
32 expressions can be arithmetic comparisons, conjunctions and negations. |
32 expressions can be arithmetic comparisons, conjunctions and negations. |
33 The semantics is fixed via two evaluation functions |
33 The semantics is fixed via two evaluation functions |
34 *} |
34 *} |
35 |
35 |
36 consts evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat" |
36 consts evala :: "'a aexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" |
37 evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool"; |
37 evalb :: "'a bexp \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"; |
38 |
38 |
39 text{*\noindent |
39 text{*\noindent |
40 that take an expression and an environment (a mapping from variables @{typ"'a"} to values |
40 that take an expression and an environment (a mapping from variables @{typ"'a"} to values |
41 @{typ"nat"}) and return its arithmetic/boolean |
41 @{typ"nat"}) and return its arithmetic/boolean |
42 value. Since the datatypes are mutually recursive, so are functions that |
42 value. Since the datatypes are mutually recursive, so are functions that |
51 "evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
51 "evala (Diff a1 a2) env = evala a1 env - evala a2 env" |
52 "evala (Var v) env = env v" |
52 "evala (Var v) env = env v" |
53 "evala (Num n) env = n" |
53 "evala (Num n) env = n" |
54 |
54 |
55 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
55 "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" |
56 "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)" |
56 "evalb (And b1 b2) env = (evalb b1 env \<and> evalb b2 env)" |
57 "evalb (Neg b) env = (\\<not> evalb b env)" |
57 "evalb (Neg b) env = (\<not> evalb b env)" |
58 |
58 |
59 text{*\noindent |
59 text{*\noindent |
60 In the same fashion we also define two functions that perform substitution: |
60 In the same fashion we also define two functions that perform substitution: |
61 *} |
61 *} |
62 |
62 |
63 consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp" |
63 consts substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp" |
64 substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp"; |
64 substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"; |
65 |
65 |
66 text{*\noindent |
66 text{*\noindent |
67 The first argument is a function mapping variables to expressions, the |
67 The first argument is a function mapping variables to expressions, the |
68 substitution. It is applied to all variables in the second argument. As a |
68 substitution. It is applied to all variables in the second argument. As a |
69 result, the type of variables in the expression may change from @{typ"'a"} |
69 result, the type of variables in the expression may change from @{typ"'a"} |
91 boolean expressions (by induction), you find that you always need the other |
91 boolean expressions (by induction), you find that you always need the other |
92 theorem in the induction step. Therefore you need to state and prove both |
92 theorem in the induction step. Therefore you need to state and prove both |
93 theorems simultaneously: |
93 theorems simultaneously: |
94 *} |
94 *} |
95 |
95 |
96 lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and> |
96 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and> |
97 evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)"; |
97 evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"; |
98 apply(induct_tac a and b); |
98 apply(induct_tac a and b); |
99 |
99 |
100 txt{*\noindent |
100 txt{*\noindent |
101 The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
101 The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
102 *} |
102 *} |
108 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
108 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
109 an inductive proof expects a goal of the form |
109 an inductive proof expects a goal of the form |
110 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
110 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
111 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
111 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
112 \begin{isabelle} |
112 \begin{isabelle} |
113 \isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"} |
113 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text")"} |
114 \end{isabelle} |
114 \end{isabelle} |
115 |
115 |
116 \begin{exercise} |
116 \begin{exercise} |
117 Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that |
117 Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that |
118 replaces @{term"IF"}s with complex boolean conditions by nested |
118 replaces @{term"IF"}s with complex boolean conditions by nested |